scholarly journals Groebner Bases Based Verification Solution for SystemVerilog Concurrent Assertions

2014 ◽  
Vol 2014 ◽  
pp. 1-15
Author(s):  
Ning Zhou ◽  
Xinyan Gao ◽  
Jinzhao Wu ◽  
Jianchao Wei ◽  
Dakui Li
Keyword(s):  
Case Studies ◽  
Symbolic Computation ◽  
Computer Algebra ◽  
Polynomial Ring ◽  
Digital Circuit ◽  
Groebner Bases ◽  
Symbolic Representations ◽  
Polynomial Modeling ◽  
Algorithm Framework ◽  
Algebraic Representations

We introduce an approach exploiting the power of polynomial ring algebra to perform SystemVerilog assertion verification over digital circuit systems. This method is based on Groebner bases theory and sequential properties checking. We define a constrained subset of SVAs so that an efficient polynomial modeling mechanism for both circuit descriptions and assertions can be applied. We present an algorithm framework based on the algebraic representations using Groebner bases for concurrent SVAs checking. Case studies show that computer algebra can provide canonical symbolic representations for both assertions and circuit designs and can act as a novel solver engine from the viewpoint of symbolic computation.

scholarly journals Algebraic Verification Method for SEREs Properties via Groebner Bases Approaches

2013 ◽  
Vol 2013 ◽  
pp. 1-10 ◽  
Author(s):  
Ning Zhou ◽  
Jinzhao Wu ◽  
Xinyan Gao
Keyword(s):  
Algebraic Approach ◽  
Digital Systems ◽  
Groebner Bases ◽  
Symbolic Simulation ◽  
Verification Method ◽  
Symbolic Representations ◽  
Temporal Properties ◽  
Verification Methods ◽  
Algorithm Framework ◽  
Algebraic Representations

This work presents an efficient solution using computer algebra system to perform linear temporal properties verification for synchronous digital systems. The method is essentially based on both Groebner bases approaches and symbolic simulation. A mechanism for constructing canonical polynomial set based symbolic representations for both circuit descriptions and assertions is studied. We then present a complete checking algorithm framework based on these algebraic representations by using Groebner bases. The computational experience result in this work shows that the algebraic approach is a quite competitive checking method and will be a useful supplement to the existent verification methods based on simulation.

scholarly journals Wu’s Characteristic Set Method for SystemVerilog Assertions Verification

2013 ◽  
Vol 2013 ◽  
pp. 1-14 ◽  
Author(s):  
Xinyan Gao ◽  
Ning Zhou ◽  
Jinzhao Wu ◽  
Dakui Li
Keyword(s):  
Polynomial System ◽  
Algebraic Approach ◽  
Digital Circuit ◽  
Characteristic Set ◽  
Wu's Method ◽  
Verification Methods ◽  
Polynomial Modeling ◽  
Characteristic Set Method ◽  
Algorithm Framework ◽  
Algebraic Representations

We propose a verification solution based on characteristic set of Wu’s method towards SystemVerilog assertion checking over digital circuit systems. We define a suitable subset of SVAs so that an efficient polynomial modeling mechanism for both circuit descriptions and assertions can be applied. We present an algorithm framework based on the algebraic representations using characteristic set of polynomial system. This symbolic algebraic approach is a useful supplement to the existent verification methods based on simulation.

The TOPAS symbolic computation system

2011 ◽  
Vol 26 (S1) ◽  
pp. S22-S25 ◽  
Author(s):  
A. A. Coelho ◽  
J. Evans ◽  
I. Evans ◽  
A. Kern ◽  
S. Parsons
Keyword(s):  
Developmental Stage ◽  
Rietveld Refinement ◽  
Symbolic Computation ◽  
Computer Algebra ◽  
Symbolic System ◽  
Symbolic Form ◽  
Functional Changes ◽  
Low Level ◽  
Run Time

Computer algebra removes much of the drudgery from mathematics; it allows users to formulate models by using the language of mathematics and to have those models evaluated with little effort. This symbolic form of representation is often thought of as being separate to dedicated computational programs such as Rietveld refinement. These dedicated programs are often written in low level languages; they are relatively inflexible in what they do and modifying them to change functionality in a small manner is often a major programming task. This paper describes a symbolic system that is integrated into the dedicated Rietveld refinement program called TOPAS. The symbolic component allows large functional changes to be made at run time and with a relatively small amount of effort. In addition, the system as a whole reduces the programming complexity at the developmental stage.

scholarly journals Learning a gradient grammar of French liaison

2020 ◽  
Vol 8 ◽  
Author(s):  
Paul Smolensky ◽  
Eric Rosen ◽  
Matthew Goldrick
Keyword(s):  
Symbolic Computation ◽  
Learning Algorithm ◽  
General Algorithm ◽  
Complex Pattern ◽  
Symbolic Representations ◽  
Weighted Constraints ◽  
Grammatical Analysis ◽  
French Words

In certain French words, an orthgraphically-final consonant is unpronounced except, in certain environments, when it precedes a vowel. This phenomenon, liaison, shows significant interactions with several other patterns in French (including h-aspiré, schwa deletion, and the presence of other morphemes in the liaison context). We present a learning algorithm that acquires a grammar that accounts for these patterns and their interactions. The learned grammar employs Gradient Symbolic Computation (GSC), incorporating weighted constraints and partially-activated symbolic representations. Grammatical analysis in the GSC framework includes the challenging determination of the numerical strength of symbolic constituent activations (as well as constraints). Here we present the first general algorithm for learning these quantities from empirical examples: the Error-Driven Gradient Activation Readjustment (EDGAR). Smolensky and Goldrick (2016) proposed a GSC analysis, with hand-determined numerical strengths, in which liaison derives from the coalescence of partially-activated input consonants. EDGAR allows us to extend this work to a wider range of liaison phenomena by automatically determining the more comprehensive set of numerical strengths required to generate the complex pattern of overall liaison behaviour.

scholarly journals Dynamic geometry: An agent for the reunification of algebra and geometry

Pythagoras ◽  
2005 ◽  
Vol 0 (61) ◽  
Author(s):  
Meira Hockman
Keyword(s):  
Problem Solving ◽  
Case Studies ◽  
Tertiary Education ◽  
Dynamic Geometry ◽  
Algebraic Methods ◽  
Degree Of Separation ◽  
Cultural Forms ◽  
Algebraic Concepts ◽  
Modes Of Thought ◽  
Algebraic Representations

This paper investigates the degree of separation or unity between the algebraic and geometric modes of thought of students in tertiary education. Case studies indicate that as a student is inducted into the use of algebra the insightful and visual components of geometrical and graphical modes of thought are sidelined. Based on Vygotsky’s taxonomy of the psychogenesis of cultural forms of behaviour, I suggest that this separation occurs because the algebraic methods remain fixed at a naïve or algorithmic stage. The algebraic concepts may fail to be internalised because the stage of instrumental functioning of algebra as a ‘tool’ or ‘method’ of geometry is not successfully transitioned.  I suggest that this stage of instrumental functioning may be stimulated by using dynamic geometry programs to promote the formation of images in conjunction with algebraic representations in problem solving. In this way the modes of thought in algebra and geometry in mathematics may be reunified.

Sign in / Sign up

Export Citation Format

Share Document