# Algebraic Verification Method for SEREs Properties via Groebner Bases Approaches

Authors: Ning Zhou; Jinzhao Wu; Xinyan Gao
Journal: Journal of Applied Mathematics
 (2013)

---

## Abstract

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.


---

## Body

## 1. Introduction

With the complexity of circuits increases, it becomes an important issue to find efficient ways to express and verify design properties. Actually, verification is a very difficult and computationally intensive task. Although great advances have been made over the past decades, all these verification methods suffer from this problem in some way.Currently, assertion based verification (ABV) has emerged as a promising solution for this problem. In particularly, an assertion specifying language named Property Specification Language (PSL) [1–3] has now become an IEEE standard and accepted by a wide variety of companies. PSL has totally changed the way how designers specify and verify functional requirements and properties of digital systems. Moreover, PSL based ABV has recently been supported by most EDA companies in their tools for both formal and runtime verification.So far, there have been many efforts in assertion checking solvers including model checking, theorem proving (e.g., HOL [4]), and runtime verification. In [5], an efficient approach to model check safety properties expressed in PSL property has been studied. While in [6], a temporal tester was introduced as a compositional basis for the construction of automata corresponding to temporal formulas in the PSL logic for PSL assertion run-time checking.As well known, the conventional simulation for assertion checking is a well-understood and the most commonly used technique, but only feasible for very small scale systems and cannot provide exhaustive checking, while symbolic simulation proposed by Darringer [7] as early as 1979 can provide exhaustive checking by covering many conditions with a single simulation sequence but could not handle large circuits due to exponential symbolic expressions.In our work, to address this functional verification challenge, we propose an alternative implementation mechanism based on algebra symbolic computation combining with symbolic simulation for PSL assertion checking.Earlier work in applications of symbolic manipulation and algebra computation has gained significant extensions and improvements. In [8], a technique framework on Groebner bases was demonstrated that computer algebra geometry method can be used to perform symbolic model checking by using an encoding of boolean sets as the common zeros of sets of polynomials. In [9], a similar technique framework based Wu's Method has been further extended to bit level symbolic model checking. In [10], an improved framework for multi-valued model checking via Groebner bases approached was proposed, which is based on a canonical polynomial representation of the multivalued logics.All these existing articles just mainly focus on model checking via algebraic symbolic computation approaches. In our research, instead of static analysis or model checking, we extend this algebraic approach to the area of simulation-based runtime verification methods over polynomial representation models and towards PSL assertions checking.Our aim is to verify a given temporal property holds or not on the traces produced after several cycles running over a given sequential circuit model.The idea is that, for any pure combinational circuit model, we can derive its data-flow-based polynomial representation named PM. Meanwhile, for any sequential circuit model and a given running cycle numbern, we can also derive its equivalent polynomial representation PM[n] by unrolling this sequential circuit n times and translating it into a pure combinational model. In a similar way, we can get polynomial set representation PS for any temporal assertion.By suitable restrictions of Boolean and SERE temporal layer of PSL and redefining a hierarchy of PSL assertions, we can guarantee the availability of above polynomial set model. Based on these polynomial set models, symbolic simulation can be performed to produce symbolic traces and temporal relationship constraints of signal variables as well. We then apply symbolic algebra approach to check the zeros set inclusion relationship between their polynomialsPM[n] and PS and determine whether the temporal assertion holds or not under current running cycle n.


## 2. Preliminaries

In this section, we will give some preliminary knowledge throughout this paper.


### 2.1. Cycle-Based Symbolic Simulation

We will firstly sketch the underlying system model for simulation used in our work.The system model we used is a cycle-based symbolic simulation model that is performed on a cycle-by-cycle basis for synchronous digital systems.Here, the termcycle is defined as one iteration of the evaluation process, during which the state of the design is recomputed and may change. In other words, a cycle is the smallest granularity of time.Intuitively, cycle-based symbolic simulation is a hybrid approach in the sense that the values that are propagated through the network can be both symbolic expressions or constant Boolean values. It assumes that there exists one unified clock signal in the circuit and all inputs of the systems remain unchanged while evaluating their values in each simulation cycle. The results of simulation report only the final values of the output signals or states in the current simulation cycle.By convention, we give the model structure definition for symbolic simulation as follows.Definition 1 (simulation model).
The symbolicSimulation Model for synchronous digital system is a tuple Σ=(X0,X,Y,M,S,F,n), where (i)
X0 is a finite set of input assignment including numeric value and symbolic value, Boolean or integer;(ii)
X is a finite set of primary input variables;(iii)
Y={yi∣1≤i≤NY} is a finite set of primary output variables;(iv)
M={mi∣1≤i≤NM} is a finite set of intermediate variables;(v)
n is the sequential depth of the network or running cycles;(vi)
F={y1,y2,…,ym} is a finite output function regarding input or intermediate variables, and note that each yi=fi(x1,x2,…,xn,@)(1≤i≤n) is defined on X⋃M.
Given sequential depthn of the network, a synchronous sequential logic network can be transformed into a pure combinational function of delayed input variables with delay less than or equal to n, that is,
(1)Y=F(X,X@1,…,X@n,M,M@1,…,M@n).
The behavior of a circuit is defined by its excitation functionY that serves a role similar to the transition relation or next-state functions of temporal logic model checkers.
The simulation process can be described as follows.
Firstly, cycle-based symbolic simulation is initialized by setting the state of the circuit to the initial vector (X0). Each of the primary input signals will be assigned a distinct symbolic variable or a symbolic constant. Then, at the end of a simulation step, the expressions representing the next-state functions generally undergo a parametric transformation based optimization. After parameterization, the newly generated functions are used as present state for the next state of simulation.
In this paper, simulation based verification is to check whether the given assertion is satisfied or not after running a few cycles.


### 2.2. PSL Preliminary

PSL is a hierarchical language and its syntax is very declarative and structural. Generally, PSL contains four layers: Boolean, temporal, verification, and modeling layers.(i) Modeling Layer. Modeling layer is needed to define the verification environment specially for formal verification tools. This layer is used to model behavior of design inputs and to model auxiliary parts of the design that are needed for verification.(ii) Verification Layer. Verification layer is more related to the description of verification tools where notions like assume and guarantee are present. This layer is used to tell the verification tool what to do with the properties described by the temporal layer.(iii) Temporal Layer. Temporal layer is the essence of PSL where complex temporal relations between signals can be expressed. This layer can describe properties that involve complex temporal relations which are evaluated over a series of evaluation cycles.(iv) Boolean Layer. Boolean layer is used to build expressions for the other layers, specifically the temporal layer. Boolean expressions are evaluated in a single evaluation cycle.PSL allows the engineer to define assertions describing the system's behavior once and reuse them between different forms of formal, semiformal, or functional verification. With PSL, it is possible to perform assertion based runtime verifications of the design while simulation properties are checked.According to PSL specification [1, 3, 11], every assertion written in PSL can be broken down into parts that can be attributed to one of those four layers.The Boolean layer comprises all Boolean expressions including signal names as well as HDL expressions and PSL expressions (especially all built-in function calls like, e.g.,prev(b) and rose(b) and the logical implication and other operators).The Boolean layer forms an underlying basis for the whole assertion architecture. In this paper, we will limit our discussion only to a special subset of the Boolean layer for our purpose. We then further build a restricted simple subset of SERE layer for temporal property specification and verification over this constrained Boolean layer.


## 2.1. Cycle-Based Symbolic Simulation

We will firstly sketch the underlying system model for simulation used in our work.The system model we used is a cycle-based symbolic simulation model that is performed on a cycle-by-cycle basis for synchronous digital systems.Here, the termcycle is defined as one iteration of the evaluation process, during which the state of the design is recomputed and may change. In other words, a cycle is the smallest granularity of time.Intuitively, cycle-based symbolic simulation is a hybrid approach in the sense that the values that are propagated through the network can be both symbolic expressions or constant Boolean values. It assumes that there exists one unified clock signal in the circuit and all inputs of the systems remain unchanged while evaluating their values in each simulation cycle. The results of simulation report only the final values of the output signals or states in the current simulation cycle.By convention, we give the model structure definition for symbolic simulation as follows.Definition 1 (simulation model).
The symbolicSimulation Model for synchronous digital system is a tuple Σ=(X0,X,Y,M,S,F,n), where (i)
X0 is a finite set of input assignment including numeric value and symbolic value, Boolean or integer;(ii)
X is a finite set of primary input variables;(iii)
Y={yi∣1≤i≤NY} is a finite set of primary output variables;(iv)
M={mi∣1≤i≤NM} is a finite set of intermediate variables;(v)
n is the sequential depth of the network or running cycles;(vi)
F={y1,y2,…,ym} is a finite output function regarding input or intermediate variables, and note that each yi=fi(x1,x2,…,xn,@)(1≤i≤n) is defined on X⋃M.
Given sequential depthn of the network, a synchronous sequential logic network can be transformed into a pure combinational function of delayed input variables with delay less than or equal to n, that is,
(1)Y=F(X,X@1,…,X@n,M,M@1,…,M@n).
The behavior of a circuit is defined by its excitation functionY that serves a role similar to the transition relation or next-state functions of temporal logic model checkers.
The simulation process can be described as follows.
Firstly, cycle-based symbolic simulation is initialized by setting the state of the circuit to the initial vector (X0). Each of the primary input signals will be assigned a distinct symbolic variable or a symbolic constant. Then, at the end of a simulation step, the expressions representing the next-state functions generally undergo a parametric transformation based optimization. After parameterization, the newly generated functions are used as present state for the next state of simulation.
In this paper, simulation based verification is to check whether the given assertion is satisfied or not after running a few cycles.


## 2.2. PSL Preliminary

PSL is a hierarchical language and its syntax is very declarative and structural. Generally, PSL contains four layers: Boolean, temporal, verification, and modeling layers.(i) Modeling Layer. Modeling layer is needed to define the verification environment specially for formal verification tools. This layer is used to model behavior of design inputs and to model auxiliary parts of the design that are needed for verification.(ii) Verification Layer. Verification layer is more related to the description of verification tools where notions like assume and guarantee are present. This layer is used to tell the verification tool what to do with the properties described by the temporal layer.(iii) Temporal Layer. Temporal layer is the essence of PSL where complex temporal relations between signals can be expressed. This layer can describe properties that involve complex temporal relations which are evaluated over a series of evaluation cycles.(iv) Boolean Layer. Boolean layer is used to build expressions for the other layers, specifically the temporal layer. Boolean expressions are evaluated in a single evaluation cycle.PSL allows the engineer to define assertions describing the system's behavior once and reuse them between different forms of formal, semiformal, or functional verification. With PSL, it is possible to perform assertion based runtime verifications of the design while simulation properties are checked.According to PSL specification [1, 3, 11], every assertion written in PSL can be broken down into parts that can be attributed to one of those four layers.The Boolean layer comprises all Boolean expressions including signal names as well as HDL expressions and PSL expressions (especially all built-in function calls like, e.g.,prev(b) and rose(b) and the logical implication and other operators).The Boolean layer forms an underlying basis for the whole assertion architecture. In this paper, we will limit our discussion only to a special subset of the Boolean layer for our purpose. We then further build a restricted simple subset of SERE layer for temporal property specification and verification over this constrained Boolean layer.


## 3. System Polynomial Representation Model

In this section, we will discuss polynomial modeling for combinational and sequential circuits. Previous work [12] has shown that any combinational circuit can be uniquely represented by a minimum order polynomial. Here, we give an alternative data-flow based polynomial set representation model for our assertions checking purpose whose zero set can make such a data-flow model work well.


### 3.1. Arithmetic and Logic Unit Modeling

In this paper, we only focus on arithmetic unit for calculating fixed-point operations. For any arithmetic unit, integer arithmetic operations (addition, subtraction, multiplication, and division) can be constructed by the following polynomials:(1)
y=a+b⇒(y-a-b),(2)
y=a-b⇒(y-a+b),(3)
y=a*b⇒(y-a*b),(4)
y=a/b⇒(y*b-a).The basic logic operations [13] like “AND,” “OR,” and “NOT” can be modeled by the following forms:
(2)y=NOTx⟹(1-x-y),y=x1ANDx2⟹(x1*x2-y),y=x1ORx2⟹(x1+x2-x1*x2-y).Furthermore, we can extend the above rule to other logic operators. For example,y=x1⊕x2 (or y=x1XORx2) ⇒(y-(x1+x2-x1*x2)*(1-x1*x2)).For all bit level variablexi(0≤i≤n), a limitation xi*xi-xi should be added.


### 3.2. Branch and Sequential Unit Modeling

Basically, multiway branch is an important control structure in digital system. It provides a set of condition bits,bi(0≤i≤B), a set of target identifiers, (0,…,T-1), and a mapping from condition bit values to target identifiers. This mapping takes the form of a condition tree. For any binary signal x, its value should be limited to {1,0} by adding x*x-x,
(3)y=MUX(x0,x1,…,xn,s),i=s⟹y=xi,(0≤i≤n)⟹y-∑i=1n-1‍(∏j∈{0,1,…,n-1}{i}‍((s-j)(i-j)))*xi,with∏i=0n-1(s-i)=0.Each flip-flop (FF) in the circuit can be modeled as a multiplexer, as illustrated in Figure1. We have the following proposition to state this model.Figure 1
Flip-flop model.Proposition 2.
For aD FF model (D′ is the next state), with an enable signal c, its equivalent combinational formal is y′=MUX(D,D′,s):i=s→y′=xi(0≤i<2,x0=D,x1=D′), whose polynomial algebraic model can be described as
(4)(y′-D)*(c-1),(y′-D′)*c,(y′-D)*(y′-D′),ory′-D*(c-1)-D′*c.Proof.
LetD be the current state and let y′ denote the next state of the flip-flop. When the clock value is 0, y′ has the same value as D so that the FF maintains its present state; when the clock value is 1, y′ takes a new value from the D′ input (where D′ denotes the new value next state of the FF). Therefore, we have the 2-value multiway branch model and its polynomial set representation for FF.Proposition 3.
LetD be a FF model (D′ is the next state), without enable signal; then its equivalent combinational formal polynomial algebraic model can be described as (y′-D).


### 3.3. Sequential Unrolling

Generally, for a sequential circuit, one time frame of a sequential circuit is viewed as a combinational circuit in which each flip-flop will be converted into two corresponding signals: a pseudo primary input (PPI) and a pseudo primary output (PPO).Symbolical simulation of a sequential circuit forn cycles can be regarded as unrolling the circuit n times. The unrolled circuit is still a pure combinational circuit, and the ith copy of the circuit represents the circuit at cycle i. Thus, the unrolled circuit contains all the symbolic results from the n cycles.To illustrate the sequential modeling for a given cycle number clearly, we define anindexed polynomial set representationfor the ith cycle.For example,PM[i] is defined as follows. PM[i]={(x1[i]-m2[i]-y3[i]),…}, where x1 denotes signal variable name while x1[i] denotes variable state in ith simulation cycle. If the given running cycle is n, then we have the system representation: PM={⋃i=0nPM[i]}.Letxi[l](0≤i≤r) denote the input signals for the lth clock, let mi[l](0≤i≤s) denote the intermediate signals, and let yi[l](0≤i≤t) denote the output signals. We then have the following time frame expansion model for the sequential circuit:
(5)FM={⋃i=0n‍FM[i]},
where FM[i]=C(x1[i],…,m1[i],…,m1[i],…,x1[i+1],…,m1[i+1],…,y1[i+1],…) denotes the ith time frame model.Time frame expansion is achieved by connecting the PPIs (e.g.,x1[i+1] from FM[i+1]) of the time frame to the corresponding PPOs (x1[i+1] from FM[i]) of the previous time frame.


### 3.4. Sequence Operator Modeling

In this paper, only a so-called simple subset of PSL will be considered, which subsumes the properties in which time advances monotonically, from left to right through the property: if an entity (a Boolean Expression or a SERE) needs to be evaluated at a given time, all other entities right of it do so far not need to be known. Many properties not in the simple subset can be rewritten by the simple subset. The most properties to be verified can be expressed within the bounds of the simple subset.For SEREs, only the following features are supported by our modeling method:(1)
standard Boolean expressions,(2)
fixed length Kleene closure,(3)
SERE concatenation,(4)
SERE fusion,(5)
SERE disjunction,(6)
length-matching SERE conjunction.By the constrained simple subset of PSL, the user can specify a safety property using only nonnegated weak operators. Intuitively, a safety property is used to ensure that “something bad does not happen” which is important in formal verification. Because safety properties are easier to verify, this approach is only able to deal with safety properties.(1)
Next OperatorIt indicates that the property will hold if its operand holds at the next cycle. For example,(6)assert(req->nextack)states that if signalreq is asserted then ack will be asserted at next cycle:⇒Ni(req)andNi+1(ack).(2)
Semicolons OperatorSemicolons operator, a semicolon(;), is used to join two SEREs (or twoAL expressions, or a AL expression and a SERE) in such a way that the right-hand SERE starts the cycle after the left-hand SERE ends.For example,G={assert(req;ack)} states that when signal req is asserted then ack will be asserted at next cycle:⇒Ni(req)andNi+1(ack)⇔Ni(reqisH)andNi+1(ackisH¯),where(0≤i≤dep(G)).(3)
Fusion OperatorThe fusion operator, a colon (:), is used to join two SEREs (or twoAL expressions, or a AL expression and a SERE) in such a way that there is a single cycle of overlap between them: the right-hand SERE just starts the same cycle that the left-hand SERE ends.For example,G={assertalways(req:ack;gnt)} states that when signal req is asserted then ack and gnt will be asserted at next cycle:⇒Ni(reqisH)andNi(ackisH)andNi+1(gntisH),where(0≤i≤dep(G)).(4)
Repeat OperatorRepeat operators allow the user to build more sophisticated SEREs, using variations on the SERE repetition operators[*n], [=n], and so forth. Consecutive repetition operators provide a shortcut to typing the same sub-SERE a number of times.In this paper, we only consider fixed times repeat operator[=n].For example,G={assert(req[n];ack)} states that when signal req is asserted n times then ack will be asserted at next cycle. We then have⇒N1(reqisH)and⋯andNn(reqisH)andNn+1(ackisH).


## 3.1. Arithmetic and Logic Unit Modeling

In this paper, we only focus on arithmetic unit for calculating fixed-point operations. For any arithmetic unit, integer arithmetic operations (addition, subtraction, multiplication, and division) can be constructed by the following polynomials:(1)
y=a+b⇒(y-a-b),(2)
y=a-b⇒(y-a+b),(3)
y=a*b⇒(y-a*b),(4)
y=a/b⇒(y*b-a).The basic logic operations [13] like “AND,” “OR,” and “NOT” can be modeled by the following forms:
(2)y=NOTx⟹(1-x-y),y=x1ANDx2⟹(x1*x2-y),y=x1ORx2⟹(x1+x2-x1*x2-y).Furthermore, we can extend the above rule to other logic operators. For example,y=x1⊕x2 (or y=x1XORx2) ⇒(y-(x1+x2-x1*x2)*(1-x1*x2)).For all bit level variablexi(0≤i≤n), a limitation xi*xi-xi should be added.


## 3.2. Branch and Sequential Unit Modeling

Basically, multiway branch is an important control structure in digital system. It provides a set of condition bits,bi(0≤i≤B), a set of target identifiers, (0,…,T-1), and a mapping from condition bit values to target identifiers. This mapping takes the form of a condition tree. For any binary signal x, its value should be limited to {1,0} by adding x*x-x,
(3)y=MUX(x0,x1,…,xn,s),i=s⟹y=xi,(0≤i≤n)⟹y-∑i=1n-1‍(∏j∈{0,1,…,n-1}{i}‍((s-j)(i-j)))*xi,with∏i=0n-1(s-i)=0.Each flip-flop (FF) in the circuit can be modeled as a multiplexer, as illustrated in Figure1. We have the following proposition to state this model.Figure 1
Flip-flop model.Proposition 2.
For aD FF model (D′ is the next state), with an enable signal c, its equivalent combinational formal is y′=MUX(D,D′,s):i=s→y′=xi(0≤i<2,x0=D,x1=D′), whose polynomial algebraic model can be described as
(4)(y′-D)*(c-1),(y′-D′)*c,(y′-D)*(y′-D′),ory′-D*(c-1)-D′*c.Proof.
LetD be the current state and let y′ denote the next state of the flip-flop. When the clock value is 0, y′ has the same value as D so that the FF maintains its present state; when the clock value is 1, y′ takes a new value from the D′ input (where D′ denotes the new value next state of the FF). Therefore, we have the 2-value multiway branch model and its polynomial set representation for FF.Proposition 3.
LetD be a FF model (D′ is the next state), without enable signal; then its equivalent combinational formal polynomial algebraic model can be described as (y′-D).


## 3.3. Sequential Unrolling

Generally, for a sequential circuit, one time frame of a sequential circuit is viewed as a combinational circuit in which each flip-flop will be converted into two corresponding signals: a pseudo primary input (PPI) and a pseudo primary output (PPO).Symbolical simulation of a sequential circuit forn cycles can be regarded as unrolling the circuit n times. The unrolled circuit is still a pure combinational circuit, and the ith copy of the circuit represents the circuit at cycle i. Thus, the unrolled circuit contains all the symbolic results from the n cycles.To illustrate the sequential modeling for a given cycle number clearly, we define anindexed polynomial set representationfor the ith cycle.For example,PM[i] is defined as follows. PM[i]={(x1[i]-m2[i]-y3[i]),…}, where x1 denotes signal variable name while x1[i] denotes variable state in ith simulation cycle. If the given running cycle is n, then we have the system representation: PM={⋃i=0nPM[i]}.Letxi[l](0≤i≤r) denote the input signals for the lth clock, let mi[l](0≤i≤s) denote the intermediate signals, and let yi[l](0≤i≤t) denote the output signals. We then have the following time frame expansion model for the sequential circuit:
(5)FM={⋃i=0n‍FM[i]},
where FM[i]=C(x1[i],…,m1[i],…,m1[i],…,x1[i+1],…,m1[i+1],…,y1[i+1],…) denotes the ith time frame model.Time frame expansion is achieved by connecting the PPIs (e.g.,x1[i+1] from FM[i+1]) of the time frame to the corresponding PPOs (x1[i+1] from FM[i]) of the previous time frame.


## 3.4. Sequence Operator Modeling

In this paper, only a so-called simple subset of PSL will be considered, which subsumes the properties in which time advances monotonically, from left to right through the property: if an entity (a Boolean Expression or a SERE) needs to be evaluated at a given time, all other entities right of it do so far not need to be known. Many properties not in the simple subset can be rewritten by the simple subset. The most properties to be verified can be expressed within the bounds of the simple subset.For SEREs, only the following features are supported by our modeling method:(1)
standard Boolean expressions,(2)
fixed length Kleene closure,(3)
SERE concatenation,(4)
SERE fusion,(5)
SERE disjunction,(6)
length-matching SERE conjunction.By the constrained simple subset of PSL, the user can specify a safety property using only nonnegated weak operators. Intuitively, a safety property is used to ensure that “something bad does not happen” which is important in formal verification. Because safety properties are easier to verify, this approach is only able to deal with safety properties.(1)
Next OperatorIt indicates that the property will hold if its operand holds at the next cycle. For example,(6)assert(req->nextack)states that if signalreq is asserted then ack will be asserted at next cycle:⇒Ni(req)andNi+1(ack).(2)
Semicolons OperatorSemicolons operator, a semicolon(;), is used to join two SEREs (or twoAL expressions, or a AL expression and a SERE) in such a way that the right-hand SERE starts the cycle after the left-hand SERE ends.For example,G={assert(req;ack)} states that when signal req is asserted then ack will be asserted at next cycle:⇒Ni(req)andNi+1(ack)⇔Ni(reqisH)andNi+1(ackisH¯),where(0≤i≤dep(G)).(3)
Fusion OperatorThe fusion operator, a colon (:), is used to join two SEREs (or twoAL expressions, or a AL expression and a SERE) in such a way that there is a single cycle of overlap between them: the right-hand SERE just starts the same cycle that the left-hand SERE ends.For example,G={assertalways(req:ack;gnt)} states that when signal req is asserted then ack and gnt will be asserted at next cycle:⇒Ni(reqisH)andNi(ackisH)andNi+1(gntisH),where(0≤i≤dep(G)).(4)
Repeat OperatorRepeat operators allow the user to build more sophisticated SEREs, using variations on the SERE repetition operators[*n], [=n], and so forth. Consecutive repetition operators provide a shortcut to typing the same sub-SERE a number of times.In this paper, we only consider fixed times repeat operator[=n].For example,G={assert(req[n];ack)} states that when signal req is asserted n times then ack will be asserted at next cycle. We then have⇒N1(reqisH)and⋯andNn(reqisH)andNn+1(ackisH).


## 4. Translation of SERE

In this section, we will mainly discuss the hierarchical modeling method of SERE. The temporal layer contains “Sequential Extended Regular Expressions” (SEREs) which allow describing the relation between Boolean layer expressions over time.Firstly, we discuss the general algebraization process of SERE from a symbolic computation point of view.


### 4.1. Algebraization Process

The algebraization process of SERE properties can be demonstrated in Figure2. The properties written in SERE will be unrolled and checked against the design for bounded time steps in our method. Note that only a constrained subset of SERE can be supported by our method (unspecified upper bound time range and first-match operator are excluded).Figure 2
Algebraization steps of SEREs.Firstly, we translate the properties described by the constrained subset of SERE into flat sequences according to the semantics of each supported operator.Secondly, the unrolled flat sequences will be added temporal constraints to form proportional formulas with logical connectives   (∨, ∧, and ¬).Finally, the resulted proportional formulas will be translated into equivalent polynomial set.In summary, the verification problem is reduced to proving zero set inclusion relationship which can be resolved by Groebner bases approaches.


### 4.2. Boolean Layer Modeling

The PSL Boolean layer forms an underlying basis for the whole assertion architecture. In this paper, we limit our discussion only to the Boolean layer and a special constrained subset of it.While the Boolean layer consists of Boolean expressions that hold or do not hold at a given cycle, the temporal layer provides a way to describe relationships between Boolean expressions over time.In this paper, we distinguish between signal logic and Boolean proposition logic.Therefore, we have the following two definitions.Definition 4 (signal logic).
In digital circuit systems, signal logic (SL, for short) is defined as follows:(i)
if a signals is active-high (H, for short), then its signal value is defined as 1;(ii)
if a signals is active-low (L, for short), then its signal value is defined as 0;(iii)
if a signals is assigned a symbolic value, then its signal value is defined as U.Definition 5 (symbolic trajectory logic).
The definition of trajectory evaluation logic (TEL) is extended as the following grammar:(7)f::=nis0∣nis1∣wisN∣f1andf2∣P→f∣N(f),
where “is” is used to state the value of a Boolean or word-level node in the circuit. Defined recursively over V, where p is a Boolean expression over V; n is a node or variable name; f, f1, f2 are TEL formulas; N is the next-time operator.
For example, a symbolic trajectory assertion, assumeV={a}, then [(in  is  a) ∧  N(true) =⇒N(out  is  a¯)].
Let numeric subscript denote time frame number for each variable, then we havein[0]isa,out[1]isa¯.
In this paper, all temporal operators in PSL SEREs specification will be modeled by next operatorN.
We will introduce a notion of symbolic constant to PSL inspired from GSTE [14].Definition 6 (symbolic constant).
Asymbolic constant [14] is a rigid Boolean or integer variable that forever holds the same boolean value. The notion of symbolic constant is introduced in an assertion for two purposes:(1)
to encode an arbitrary Boolean constraints among a set of circuit nodes in a parametric form;(2)
to encode all possible scalar values for a set of nodes.
Considerassertion(reqisH¯)  and (ackisH) as an example. According to our definitions, req and ack are signals belonging to signal logic, while both (reqisH¯) and (ackisH) themselves are of assertion logic.
Here, we provide a formal syntax definition for assertion proposition logic, namely,Assertion Boolean Logic.
Ifx1, x2, m, and n are of SL, then we have x1=x2, m=x1&x2, m=x1∥x2, m=!x2, and (m=x1)∧(n=x2) are all of valid AL and can also be verified by using polynomial model.Definition 7 (assertion Boolean logic layer syntax).
Ifa∈SL and H∈BC, then a=H is an atom Boolean formula; [AtomBooleanFormula].
Built-in functions:stable(), rose(), fell(), isunknown(), onehot(), andonehot0() are of atom Boolean formulas.
Ifa is an integer signal logic variable (denoted by a∈ISL) and symbolic constant I∈IC, then a=I is also an atom Boolean formula; [AtomBooleanFormula].
Ifa1 and a2 are atom Boolean formulas, then(1)
a1&&a2[Standard Logic “AND”],(2)
a1∥a2[Standard Logic “OR”],(3)
!a1[Standard Logic “NOT”],(4)
a1->a2[Standard Logic “Implication”] are Boolean formulas.
Assertion proposition logic (AL) for PSL is defined as standard Boolean logic. A Boolean expression of AL is an expression that is evaluated in a single cycle and has the value true or false. Boolean connectives for AL are interpreted in the standard.
For example, assertion(a[15:0]==b[15:0]), given in the Verilog flavor of PSL, is a valid Boolean expression which means a[15:0] and b[15:0] are equal.
The state of a signal variable can be viewed as a zero of a set of polynomials. We have the following.(1)
For any signalx holds at a given time step i; thus, the state of x==1 (x is active-high at cycle i) can be represented by polynomial {x[i]-1}.(2)
Alternatively, the state ofx==0 (x is active-low at cycle i ) can be represented by polynomial {x[i]}.(3)
Symbolically, the state ofx==H (x is active-high H at the ith cycle) can be modeled as {x[i]-H}.


## 4.1. Algebraization Process

The algebraization process of SERE properties can be demonstrated in Figure2. The properties written in SERE will be unrolled and checked against the design for bounded time steps in our method. Note that only a constrained subset of SERE can be supported by our method (unspecified upper bound time range and first-match operator are excluded).Figure 2
Algebraization steps of SEREs.Firstly, we translate the properties described by the constrained subset of SERE into flat sequences according to the semantics of each supported operator.Secondly, the unrolled flat sequences will be added temporal constraints to form proportional formulas with logical connectives   (∨, ∧, and ¬).Finally, the resulted proportional formulas will be translated into equivalent polynomial set.In summary, the verification problem is reduced to proving zero set inclusion relationship which can be resolved by Groebner bases approaches.


## 4.2. Boolean Layer Modeling

The PSL Boolean layer forms an underlying basis for the whole assertion architecture. In this paper, we limit our discussion only to the Boolean layer and a special constrained subset of it.While the Boolean layer consists of Boolean expressions that hold or do not hold at a given cycle, the temporal layer provides a way to describe relationships between Boolean expressions over time.In this paper, we distinguish between signal logic and Boolean proposition logic.Therefore, we have the following two definitions.Definition 4 (signal logic).
In digital circuit systems, signal logic (SL, for short) is defined as follows:(i)
if a signals is active-high (H, for short), then its signal value is defined as 1;(ii)
if a signals is active-low (L, for short), then its signal value is defined as 0;(iii)
if a signals is assigned a symbolic value, then its signal value is defined as U.Definition 5 (symbolic trajectory logic).
The definition of trajectory evaluation logic (TEL) is extended as the following grammar:(7)f::=nis0∣nis1∣wisN∣f1andf2∣P→f∣N(f),
where “is” is used to state the value of a Boolean or word-level node in the circuit. Defined recursively over V, where p is a Boolean expression over V; n is a node or variable name; f, f1, f2 are TEL formulas; N is the next-time operator.
For example, a symbolic trajectory assertion, assumeV={a}, then [(in  is  a) ∧  N(true) =⇒N(out  is  a¯)].
Let numeric subscript denote time frame number for each variable, then we havein[0]isa,out[1]isa¯.
In this paper, all temporal operators in PSL SEREs specification will be modeled by next operatorN.
We will introduce a notion of symbolic constant to PSL inspired from GSTE [14].Definition 6 (symbolic constant).
Asymbolic constant [14] is a rigid Boolean or integer variable that forever holds the same boolean value. The notion of symbolic constant is introduced in an assertion for two purposes:(1)
to encode an arbitrary Boolean constraints among a set of circuit nodes in a parametric form;(2)
to encode all possible scalar values for a set of nodes.
Considerassertion(reqisH¯)  and (ackisH) as an example. According to our definitions, req and ack are signals belonging to signal logic, while both (reqisH¯) and (ackisH) themselves are of assertion logic.
Here, we provide a formal syntax definition for assertion proposition logic, namely,Assertion Boolean Logic.
Ifx1, x2, m, and n are of SL, then we have x1=x2, m=x1&x2, m=x1∥x2, m=!x2, and (m=x1)∧(n=x2) are all of valid AL and can also be verified by using polynomial model.Definition 7 (assertion Boolean logic layer syntax).
Ifa∈SL and H∈BC, then a=H is an atom Boolean formula; [AtomBooleanFormula].
Built-in functions:stable(), rose(), fell(), isunknown(), onehot(), andonehot0() are of atom Boolean formulas.
Ifa is an integer signal logic variable (denoted by a∈ISL) and symbolic constant I∈IC, then a=I is also an atom Boolean formula; [AtomBooleanFormula].
Ifa1 and a2 are atom Boolean formulas, then(1)
a1&&a2[Standard Logic “AND”],(2)
a1∥a2[Standard Logic “OR”],(3)
!a1[Standard Logic “NOT”],(4)
a1->a2[Standard Logic “Implication”] are Boolean formulas.
Assertion proposition logic (AL) for PSL is defined as standard Boolean logic. A Boolean expression of AL is an expression that is evaluated in a single cycle and has the value true or false. Boolean connectives for AL are interpreted in the standard.
For example, assertion(a[15:0]==b[15:0]), given in the Verilog flavor of PSL, is a valid Boolean expression which means a[15:0] and b[15:0] are equal.
The state of a signal variable can be viewed as a zero of a set of polynomials. We have the following.(1)
For any signalx holds at a given time step i; thus, the state of x==1 (x is active-high at cycle i) can be represented by polynomial {x[i]-1}.(2)
Alternatively, the state ofx==0 (x is active-low at cycle i ) can be represented by polynomial {x[i]}.(3)
Symbolically, the state ofx==H (x is active-high H at the ith cycle) can be modeled as {x[i]-H}.


## 5. Algorithm Framework

In this section, we will describe how an assertion is checked using Groebner basis approach.As we all know, in traditional numeric simulation [15], PSL assertion checking process can be described as follows. Firstly, the design file with PSL codes is compiled into local executable binary code via simulation tools (such as, QuestaSim or ModelSim). The designer then provides a testbench file to set input values, running cycles, and other parameters. Finally, the designer performs simulation by starting “run” command to produce traces for assertion checking.Firstly, we will sketch some of the key notions of Groebner bases theory [16, 17] and symbolic computation.


### 5.1. Groebner Bases Preliminary

We begin by listing some general facts and establishing notations.Letk be an algebraically closed field, and let k[x1,…,xn] be the polynomial ring in variables x1,x2,…,xn with coefficient in k, under addition and multiplication of polynomial.Here, letI⊆k[x1,…,xn] be an ideal. As we all know, the following theorem holds.Theorem 8 (Hilbert basis theorem).
Every idealI⊂k[x1,…,xn] has a finite generating set. That is, I=〈g1,…,gt〉 for some g1,…,gt∈I.Then, by the Hilbert basis theorem, there exist finitely many polynomialsf1,…,fm such that I=〈f1,…,fm〉. A polynomial f⊆k[x1,…,xn] defines a map f:kn→k via evaluation (a1,…,an)↦f(a1,…,an).The setV(I):=a∈kn∣∀f∈I:f(a)=0⊆kn is called the variety associated with I.IfV1=V(I1) and V2=V(I2) are the varieties defined by ideals I1 and I2, then we have V1∩V2=V(〈I1,I2〉) and V1∪V2=V(I1×I2), where I1×I2=〈f1f2∣f1∈I1,f2∈I2〉. If I1=〈f1,…,fr〉 and I2=〈h1,…,hs〉, then I1×I2=〈fi×gj∣1≤i≤r,1≤j≤s〉.Any set of points inkn can be regarded as the variety of some ideal. Note that there will be more than one ideal defining a given variety. For example, the ideals 〈x0〉 and 〈x0,x1x0-1〉 both define the variety V(x0). In order to perform verification, we need to be able to determine when two ideals represent the same set of points. That is to say, we need a canonical representation for any ideal. Groebner bases can be used for this purpose.Definition 9 (Groebner basis).
Fix a monomial order. A finite subsetG={g1,…,gt} of an ideal I is said to be a Groebner basis (or standard basis) if 〈LT(g1),…,LT(gt)〉=〈LT(I)〉.
Equivalently, but more informally, a set{g1,…,gt}⊂I is a Groebner basis of I if and only if the leading term of any element of I is divisible by one of the LT(gi).
In work [18], Buchberger provided an algorithm for constructing a Groebner basis for a given ideal. This algorithm can also be used to determine whether a polynomial belongs to a given ideal.
Areduced Groebner basisG is a Groebner basis where the leading coefficients of polynomials in G are all 1, and no monomial of an element of G lies in the ideal generated by the leading terms of other elements of G:∀g∈G, no monomial of g is in 〈LT(G-{g})〉.
The important result is that, for a fixed monomial ordering, any nonzero ideal has a unique reduced Groebner basis. The algorithm for finding a Groebner basis can easily be extended to output its reduced Groebner basis. Thus we will have a canonical symbolic representation for any ideal.Theorem 10 (the elimination theorem).
LetI⊂k[x1,…,xn] be an ideal and let G be a Groebner basis of I with respect to lex order where x1≻x2≻⋯≻xn. Then, for every 0≤l≤n, the set
(8)Gl=G∩k[xl+1,…,xn]
is a Groebner basis of the lth elimination ideal Il.Theorem 11.
LetG be a Groebner basis for an ideal I⊂k[x1,…,xn] and let f∈k[x1,…,xn]. Then f∈I if and only if the remainder on division of f by G is zero, denoted by, remd(f,G)=0.The property given in Theorem11 can also be taken as the definition of a Groebner basis. Then we will get an efficient algorithm for solving the ideal membership problem. Assumed that we know a Groebner basis G for the ideal in question, we only need to compute a remainder with respect to G to determine whether f∈I.


### 5.2. Verification Principle Based Theorem Proving

As just mentioned in previous section, our checking method is based on algebraic geometry theory. Algebraic geometry is the study of the geometric objects arising as the common zeros of collections of polynomials. Our aim is to find polynomials whose zeros correspond to system states in which the appropriate assignments are made.In our method, we regard any set of points inkn as the variety of some ideal. We can use the ideal or any basis for the ideal as a way of encoding the set of states. The verification problem is then transformed into ideal membership problem that can be solved by computation algorithms.From Groebner Bases theory [16, 18] every nonzero ideal I⊂k[x1,…,xn] has a Groebner basis and the following proposition evidently holds.Proposition 12.
LetC and S be polynomial sets of k[x1,…,xn], and 〈GS〉 is a Groebner basis for 〈S〉, then one has 〈C〉⊆〈S〉⇔∀c∈C:remd(c,GS)=0.All supported SEREs properties can be classified into two categories.(1)
Implication-typed: Properties of this type have an explicit antecedent that can be taken as an initial precondition. If the precondition is conflict with the system model, this property will be viewed as false. Otherwise, further checking process will be performed.(2)
Sequence-typed: Properties of this type have no explicit antecedent, and therefore an initial condition should be provided by the testbench. If the precondition is in conflict with the system model, this sequence property will also be viewed as false. Otherwise, further checking process will be performed.Theorem 13.
Suppose thatG (If G=[A⇒C] is an implication-typed property, then A denotes the antecedent; otherwise, G is a sequence-typed property, then A is the precondition) and M is a system model. Let PA and PM be the polynomial set representations for A and M, respectively, constructed by previous mentioned rules. Let H=PA∪PM={h1,h2,…,hs}⊆k[x1,…,xn], I=〈H〉  (where  〈H〉 denotes the ideal generated by H), {c1,c2,…,cr} denotes the polynomial set representation for C, GBH=gbasis(H,≺), then one has((1∉GBH)andremd(C,GBH)==0)⇔((1∉GBH)and⋀i=0r(remd(ci,GBH)==0))⇔(M∣=G).Proof.
By Hilbert’s Nullstellensatz theory and previously mentioned notions, it is easy to have the conclusion.


### 5.3. Checking Algorithm

For a practical assertion checking process, it needs to build complicated syntax analysis tree for a given assertion and call the basic checking functions to perform checking. For simplicity, we only provide the core decision algorithms and the basic process flow.Firstly, the original circuit is sliced with respect to the given assertionG. Polynomial representation for sliced circuit model, antecedent, and consequent will then be built, respectively. Finally, we calculate the hypothesis set and its Groebner bases to determine whether the assertion holds or not.From the above discussion, we have the process steps and detailed algorithm description in Algorithm1.Algorithm 1:Assertion checking: AssChk(C,G).
Input: Circuit model C, an assertion G=[𝒜⇒𝒞];
Output: Boolean: true or false;
BEGIN
/* Step 0: initialize input signals via testbench */
(
0
)
I
n
i
t
S
i
g
n
a
l
s
(
X
0
→
);
(
1
)
S=∅;M=∅;PSA=∅;H=∅;PSC=∅;
/* Step 1: build polynomial model */
(
2
)
M=BuildPS(S);
/* Step 3: build polynomial set for antecedent 𝒜 */
(
3
)
PS𝒜=BuildPS(𝒜);
/* Step 3: build polynomial set for consequent 𝒞 */
(
4
)
PS𝒞=BuildPS(𝒞);
/* Step 4: calculate the PS𝒜∪M */
(
5
)
H=PS𝒜∪M;
/* Step 5: calculate the Groebner base of 〈H〉 */
(
6
)
GBH:=gbasis(H,≺);
/* Step 6: calculate the Groebner base of 〈H〉 */
(
7
)  if(1∈GBH){
(
8
)      return false; }
(
9
)   if(remd(PS𝒞,GBH)≠0){
(
10
)    return false; }
(
11
)
return true; /* Assertion does hold */
END;An important advantage of our algorithm is that it only requires a comparatively small amount of state variables to verify a given assertion due to slicing reduction.From the above discussion, we have the process steps and detailed algorithm description in Algorithm2.Algorithm 2:Assertion checking: TemporalAssChk(C,s,cycles).
Input: Circuit model C, a temporal assertion s, running cycles cycles;
Output: Boolean: true or false;
BEGIN
(
1
)  i=0;
(
2
)  switch(operator(s)){
(
3
)   casealways:{
(
4
)    while(i<cycles){
(
5
)     if(!AssChk(C,s,i)){;
(
6
)       return false;}
(
7
)     i+=dep(s)}
(
8
)    } /* end while */
(
9
)   caseeventually:{
(
10
)   while(i<cycles){
(
11
)    if(AssChk(C,s,i)){;
(
12
)      return true;}
(
13
)    i+=dep(s)}
(
14
)   } /* end while */
(
15
)  }/* end case */
(
16
)  casenever:{
(
17
)   while(i<cycles){
(
18
)    if(AssChk(C,s,i)){;
(
19
)      return false;}
(
20
)    i+=dep(s)}
(
21
)   } /* end while */
(
22
)  }/* end case */
(
23
)   deafult:{
(
24
)   returnAssChk(C,s,i);
(
25
)   }/* end switch */
(
26
)  }
END;Firstly, the original circuit is transformed into a normal polynomial representation and the assertion as well. Then, calculate Groebner bases using the Buchberger algorithm [19] and their elimination ideals. Finally, examine the relation between elimination ideals and determine whether the assertion holds or not.


## 5.1. Groebner Bases Preliminary

We begin by listing some general facts and establishing notations.Letk be an algebraically closed field, and let k[x1,…,xn] be the polynomial ring in variables x1,x2,…,xn with coefficient in k, under addition and multiplication of polynomial.Here, letI⊆k[x1,…,xn] be an ideal. As we all know, the following theorem holds.Theorem 8 (Hilbert basis theorem).
Every idealI⊂k[x1,…,xn] has a finite generating set. That is, I=〈g1,…,gt〉 for some g1,…,gt∈I.Then, by the Hilbert basis theorem, there exist finitely many polynomialsf1,…,fm such that I=〈f1,…,fm〉. A polynomial f⊆k[x1,…,xn] defines a map f:kn→k via evaluation (a1,…,an)↦f(a1,…,an).The setV(I):=a∈kn∣∀f∈I:f(a)=0⊆kn is called the variety associated with I.IfV1=V(I1) and V2=V(I2) are the varieties defined by ideals I1 and I2, then we have V1∩V2=V(〈I1,I2〉) and V1∪V2=V(I1×I2), where I1×I2=〈f1f2∣f1∈I1,f2∈I2〉. If I1=〈f1,…,fr〉 and I2=〈h1,…,hs〉, then I1×I2=〈fi×gj∣1≤i≤r,1≤j≤s〉.Any set of points inkn can be regarded as the variety of some ideal. Note that there will be more than one ideal defining a given variety. For example, the ideals 〈x0〉 and 〈x0,x1x0-1〉 both define the variety V(x0). In order to perform verification, we need to be able to determine when two ideals represent the same set of points. That is to say, we need a canonical representation for any ideal. Groebner bases can be used for this purpose.Definition 9 (Groebner basis).
Fix a monomial order. A finite subsetG={g1,…,gt} of an ideal I is said to be a Groebner basis (or standard basis) if 〈LT(g1),…,LT(gt)〉=〈LT(I)〉.
Equivalently, but more informally, a set{g1,…,gt}⊂I is a Groebner basis of I if and only if the leading term of any element of I is divisible by one of the LT(gi).
In work [18], Buchberger provided an algorithm for constructing a Groebner basis for a given ideal. This algorithm can also be used to determine whether a polynomial belongs to a given ideal.
Areduced Groebner basisG is a Groebner basis where the leading coefficients of polynomials in G are all 1, and no monomial of an element of G lies in the ideal generated by the leading terms of other elements of G:∀g∈G, no monomial of g is in 〈LT(G-{g})〉.
The important result is that, for a fixed monomial ordering, any nonzero ideal has a unique reduced Groebner basis. The algorithm for finding a Groebner basis can easily be extended to output its reduced Groebner basis. Thus we will have a canonical symbolic representation for any ideal.Theorem 10 (the elimination theorem).
LetI⊂k[x1,…,xn] be an ideal and let G be a Groebner basis of I with respect to lex order where x1≻x2≻⋯≻xn. Then, for every 0≤l≤n, the set
(8)Gl=G∩k[xl+1,…,xn]
is a Groebner basis of the lth elimination ideal Il.Theorem 11.
LetG be a Groebner basis for an ideal I⊂k[x1,…,xn] and let f∈k[x1,…,xn]. Then f∈I if and only if the remainder on division of f by G is zero, denoted by, remd(f,G)=0.The property given in Theorem11 can also be taken as the definition of a Groebner basis. Then we will get an efficient algorithm for solving the ideal membership problem. Assumed that we know a Groebner basis G for the ideal in question, we only need to compute a remainder with respect to G to determine whether f∈I.


## 5.2. Verification Principle Based Theorem Proving

As just mentioned in previous section, our checking method is based on algebraic geometry theory. Algebraic geometry is the study of the geometric objects arising as the common zeros of collections of polynomials. Our aim is to find polynomials whose zeros correspond to system states in which the appropriate assignments are made.In our method, we regard any set of points inkn as the variety of some ideal. We can use the ideal or any basis for the ideal as a way of encoding the set of states. The verification problem is then transformed into ideal membership problem that can be solved by computation algorithms.From Groebner Bases theory [16, 18] every nonzero ideal I⊂k[x1,…,xn] has a Groebner basis and the following proposition evidently holds.Proposition 12.
LetC and S be polynomial sets of k[x1,…,xn], and 〈GS〉 is a Groebner basis for 〈S〉, then one has 〈C〉⊆〈S〉⇔∀c∈C:remd(c,GS)=0.All supported SEREs properties can be classified into two categories.(1)
Implication-typed: Properties of this type have an explicit antecedent that can be taken as an initial precondition. If the precondition is conflict with the system model, this property will be viewed as false. Otherwise, further checking process will be performed.(2)
Sequence-typed: Properties of this type have no explicit antecedent, and therefore an initial condition should be provided by the testbench. If the precondition is in conflict with the system model, this sequence property will also be viewed as false. Otherwise, further checking process will be performed.Theorem 13.
Suppose thatG (If G=[A⇒C] is an implication-typed property, then A denotes the antecedent; otherwise, G is a sequence-typed property, then A is the precondition) and M is a system model. Let PA and PM be the polynomial set representations for A and M, respectively, constructed by previous mentioned rules. Let H=PA∪PM={h1,h2,…,hs}⊆k[x1,…,xn], I=〈H〉  (where  〈H〉 denotes the ideal generated by H), {c1,c2,…,cr} denotes the polynomial set representation for C, GBH=gbasis(H,≺), then one has((1∉GBH)andremd(C,GBH)==0)⇔((1∉GBH)and⋀i=0r(remd(ci,GBH)==0))⇔(M∣=G).Proof.
By Hilbert’s Nullstellensatz theory and previously mentioned notions, it is easy to have the conclusion.


## 5.3. Checking Algorithm

For a practical assertion checking process, it needs to build complicated syntax analysis tree for a given assertion and call the basic checking functions to perform checking. For simplicity, we only provide the core decision algorithms and the basic process flow.Firstly, the original circuit is sliced with respect to the given assertionG. Polynomial representation for sliced circuit model, antecedent, and consequent will then be built, respectively. Finally, we calculate the hypothesis set and its Groebner bases to determine whether the assertion holds or not.From the above discussion, we have the process steps and detailed algorithm description in Algorithm1.Algorithm 1:Assertion checking: AssChk(C,G).
Input: Circuit model C, an assertion G=[𝒜⇒𝒞];
Output: Boolean: true or false;
BEGIN
/* Step 0: initialize input signals via testbench */
(
0
)
I
n
i
t
S
i
g
n
a
l
s
(
X
0
→
);
(
1
)
S=∅;M=∅;PSA=∅;H=∅;PSC=∅;
/* Step 1: build polynomial model */
(
2
)
M=BuildPS(S);
/* Step 3: build polynomial set for antecedent 𝒜 */
(
3
)
PS𝒜=BuildPS(𝒜);
/* Step 3: build polynomial set for consequent 𝒞 */
(
4
)
PS𝒞=BuildPS(𝒞);
/* Step 4: calculate the PS𝒜∪M */
(
5
)
H=PS𝒜∪M;
/* Step 5: calculate the Groebner base of 〈H〉 */
(
6
)
GBH:=gbasis(H,≺);
/* Step 6: calculate the Groebner base of 〈H〉 */
(
7
)  if(1∈GBH){
(
8
)      return false; }
(
9
)   if(remd(PS𝒞,GBH)≠0){
(
10
)    return false; }
(
11
)
return true; /* Assertion does hold */
END;An important advantage of our algorithm is that it only requires a comparatively small amount of state variables to verify a given assertion due to slicing reduction.From the above discussion, we have the process steps and detailed algorithm description in Algorithm2.Algorithm 2:Assertion checking: TemporalAssChk(C,s,cycles).
Input: Circuit model C, a temporal assertion s, running cycles cycles;
Output: Boolean: true or false;
BEGIN
(
1
)  i=0;
(
2
)  switch(operator(s)){
(
3
)   casealways:{
(
4
)    while(i<cycles){
(
5
)     if(!AssChk(C,s,i)){;
(
6
)       return false;}
(
7
)     i+=dep(s)}
(
8
)    } /* end while */
(
9
)   caseeventually:{
(
10
)   while(i<cycles){
(
11
)    if(AssChk(C,s,i)){;
(
12
)      return true;}
(
13
)    i+=dep(s)}
(
14
)   } /* end while */
(
15
)  }/* end case */
(
16
)  casenever:{
(
17
)   while(i<cycles){
(
18
)    if(AssChk(C,s,i)){;
(
19
)      return false;}
(
20
)    i+=dep(s)}
(
21
)   } /* end while */
(
22
)  }/* end case */
(
23
)   deafult:{
(
24
)   returnAssChk(C,s,i);
(
25
)   }/* end switch */
(
26
)  }
END;Firstly, the original circuit is transformed into a normal polynomial representation and the assertion as well. Then, calculate Groebner bases using the Buchberger algorithm [19] and their elimination ideals. Finally, examine the relation between elimination ideals and determine whether the assertion holds or not.


## 6. A Case Study

In this section, we will study a case to show how PSL SERE properties are verified by polynomial representation and algebra computation.


### 6.1. Circuit and PSL Modeling

As an example, consider the 3-bit synchronous counter circuitC in Figure 3, whose polynomial set can be constructed as follows. In this circuit, there exists a design bug that “AND” gate is replaced by “OR” gate incorrectly. Now, let us show how to check this error using our symbolic algebraic method:
(9)PSetcounter={(m3′-y3)(y1-(m1+m4-m1*m4)*(1-m1*m4)),(y2-(m2+m3-m2*m3)*(1-m2*m3)),(1-m3-y3),(1-m4-m3*m2),(m1′-y1)(m2′-y2)(m3′-y3)},
where x1′ denotes the next state of x1. For the ith cycle, we use x1[i] to denote variable name in current cycle.Figure 3
Synchronous counter.To illustrate the problem clearly, we define polynomial set representationPM[i] for ith cycle as follows:
(10)PM[i]={(y1[i]-(m1[i]+m4[i]-m1[i]*m)*(1-m1[i]*m4[i])),(y2[i]-(m2[i]+m3[i]-m2[i]*m3)*(1-m2[i]*m3[i])),(1-m3[i]-y3[i]),(1-m4[i]-m3[i]*m2[i]),(m1[i+1]-y1[i]),(m2[i+1]-y2[i]),(m3[i+1]-y3[i])}.Therefore, we havePM={⋃i=07PM[i]}.For any boolean variablea, we will impose an extra constraint: a*a-a. Thus, we should define the corresponding constraints set as follows: CNS[i]={a[i]*a[i]-a[i]} for all bit-level variables in the ith cycle.In the same manner, we haveCNS={⋃i=07CNS[i]}.The sequential properties of this counter circuit can be specified by the following assertions:G1={assertalways(m1=H¯&m2=H¯&m3=H¯)∣⇒(m1=H¯&m2=H¯&m3=H)},G2={assertalways(m1=H¯&m2=H¯&m3=H)∣⇒(m1=H¯&m2=H&m3=H¯)},G3={assertalways(m1=H¯&m2=H&m3=H¯)∣⇒(m1=H¯&m2=H&m3=H)}, and the rest may be deduced by analogy.Afterward, we will demonstrate the verification process step by step.Firstly, we calculate the sequential depth and havedep(G1)=2, dep(G2)=2, and dep(G2)=2.Secondly, to verify a given property hold or not, we have to build a system model with 8 cycles at most and checkdep(G1)=2 steps.The circuit model to be verified is below:(11)SM=PM⋃CNS.The properties of this counter can be specified as the following PSL assertions listed in Table1.Table 1
Polynomial representations for properties to be verified.
No.
Precondition
Expected consequent
0
m
1
[
0
], m2[0], m3[0]
N/A
Cycle1
N/A
(
m
1
[
1
]
,
m
2
[
1
]
,
m
3
[
1
]
-
1
)
Cycle2
N/A
(
m
1
[
2
]
,
m
2
[
2
]
-
1
,
m
3
[
2
]
)
Cycle3
N/A
(
m
1
[
3
]
,
m
2
[
3
]
-
1
,
m
3
[
3
]
-
1
)
Cycle4
N/A
(
m
1
[
4
]
-
1
,
m
2
[
4
]
,
m
3
[
4
]
)
Cycle5
N/A
(
m
1
[
5
]
-
1
,
m
2
[
5
]
,
m
3
[
5
]
-
1
)
Cycle6
N/A
(
m
1
[
6
]
-
1
,
m
2
[
6
]
-
1
,
m
3
[
6
]
)
Cycle7
N/A
(
m
1
[
7
]
-
1
,
m
2
[
7
]
-
1
,
m
3
[
7
]
-
1
)


### 6.2. Assertion Checking Using Maple

We run this example by using Maple 13 software. Before running, we manually translated all models into polynomials. The experiment is performed on a Computer with a 2.40 GHz CPU (Intel i5 M450) and 512 MB of memory. It took about 0.04 seconds and 0.81 MB of memory to find this error when applying Groebner method:[>with(Groebner)[>CM:=⋯ /* Circuit Model */[>TDEG:=tdeg(
m1[0],m2[0],m3[0],m4[0],m1[1],m2[1],m3[1],m4[1],m1[2],m2[2],m3[2],m4[2],y1[0],y1[1],y1[2],y2[0],y2[1],y2[2],y3[0],y3[1],y3[2])[>CGB:=Basis(G,TDEG)[>ret:=NormalForm(m3[0]-1,CGB,TDEG)[>ret=0.As shown in maple outputs, the given circuit has been modeled as polynomial setCM (its Groebner basis is denoted by CGB) and assertion representation as (m3[0]-1). From the running result, we have return value of NormalForm is 0 which means CGB be divided with no remainder by (m3[0]-1). Thus, from the previously mentioned verification principles, it is easy to conclude that the SERE assertion G1 holds under this circuit model after 1 cycle. Other results are shown in Table 2.Table 2
Result table.
Cycle no.
Polynomial
Result
Cycle1
m
1
[
0
]
,
m
2
[
0
]
,
m
3
[
0
]
-
1
r
e
t
=
0
Cycle2
m
1
[
1
]
,
m
2
[
1
]
-
1
,
m
3
[
1
]
r
e
t
≠
0, m1[1] fails
Cycle3
m
1
[
2
]
,
m
2
[
2
]
-
1
,
m
3
[
2
]
-
1
StopFrom Table2, when checking G2 assertion, the result ret:=NormalForm(m1[1],CGB,TDEG)=1≠0 so that we can conclude the assertion does not hold and there must exist some error in the original circuit. This case is a fairly complete illustration of how our checking algorithm works.


## 6.1. Circuit and PSL Modeling

As an example, consider the 3-bit synchronous counter circuitC in Figure 3, whose polynomial set can be constructed as follows. In this circuit, there exists a design bug that “AND” gate is replaced by “OR” gate incorrectly. Now, let us show how to check this error using our symbolic algebraic method:
(9)PSetcounter={(m3′-y3)(y1-(m1+m4-m1*m4)*(1-m1*m4)),(y2-(m2+m3-m2*m3)*(1-m2*m3)),(1-m3-y3),(1-m4-m3*m2),(m1′-y1)(m2′-y2)(m3′-y3)},
where x1′ denotes the next state of x1. For the ith cycle, we use x1[i] to denote variable name in current cycle.Figure 3
Synchronous counter.To illustrate the problem clearly, we define polynomial set representationPM[i] for ith cycle as follows:
(10)PM[i]={(y1[i]-(m1[i]+m4[i]-m1[i]*m)*(1-m1[i]*m4[i])),(y2[i]-(m2[i]+m3[i]-m2[i]*m3)*(1-m2[i]*m3[i])),(1-m3[i]-y3[i]),(1-m4[i]-m3[i]*m2[i]),(m1[i+1]-y1[i]),(m2[i+1]-y2[i]),(m3[i+1]-y3[i])}.Therefore, we havePM={⋃i=07PM[i]}.For any boolean variablea, we will impose an extra constraint: a*a-a. Thus, we should define the corresponding constraints set as follows: CNS[i]={a[i]*a[i]-a[i]} for all bit-level variables in the ith cycle.In the same manner, we haveCNS={⋃i=07CNS[i]}.The sequential properties of this counter circuit can be specified by the following assertions:G1={assertalways(m1=H¯&m2=H¯&m3=H¯)∣⇒(m1=H¯&m2=H¯&m3=H)},G2={assertalways(m1=H¯&m2=H¯&m3=H)∣⇒(m1=H¯&m2=H&m3=H¯)},G3={assertalways(m1=H¯&m2=H&m3=H¯)∣⇒(m1=H¯&m2=H&m3=H)}, and the rest may be deduced by analogy.Afterward, we will demonstrate the verification process step by step.Firstly, we calculate the sequential depth and havedep(G1)=2, dep(G2)=2, and dep(G2)=2.Secondly, to verify a given property hold or not, we have to build a system model with 8 cycles at most and checkdep(G1)=2 steps.The circuit model to be verified is below:(11)SM=PM⋃CNS.The properties of this counter can be specified as the following PSL assertions listed in Table1.Table 1
Polynomial representations for properties to be verified.
No.
Precondition
Expected consequent
0
m
1
[
0
], m2[0], m3[0]
N/A
Cycle1
N/A
(
m
1
[
1
]
,
m
2
[
1
]
,
m
3
[
1
]
-
1
)
Cycle2
N/A
(
m
1
[
2
]
,
m
2
[
2
]
-
1
,
m
3
[
2
]
)
Cycle3
N/A
(
m
1
[
3
]
,
m
2
[
3
]
-
1
,
m
3
[
3
]
-
1
)
Cycle4
N/A
(
m
1
[
4
]
-
1
,
m
2
[
4
]
,
m
3
[
4
]
)
Cycle5
N/A
(
m
1
[
5
]
-
1
,
m
2
[
5
]
,
m
3
[
5
]
-
1
)
Cycle6
N/A
(
m
1
[
6
]
-
1
,
m
2
[
6
]
-
1
,
m
3
[
6
]
)
Cycle7
N/A
(
m
1
[
7
]
-
1
,
m
2
[
7
]
-
1
,
m
3
[
7
]
-
1
)


## 6.2. Assertion Checking Using Maple

We run this example by using Maple 13 software. Before running, we manually translated all models into polynomials. The experiment is performed on a Computer with a 2.40 GHz CPU (Intel i5 M450) and 512 MB of memory. It took about 0.04 seconds and 0.81 MB of memory to find this error when applying Groebner method:[>with(Groebner)[>CM:=⋯ /* Circuit Model */[>TDEG:=tdeg(
m1[0],m2[0],m3[0],m4[0],m1[1],m2[1],m3[1],m4[1],m1[2],m2[2],m3[2],m4[2],y1[0],y1[1],y1[2],y2[0],y2[1],y2[2],y3[0],y3[1],y3[2])[>CGB:=Basis(G,TDEG)[>ret:=NormalForm(m3[0]-1,CGB,TDEG)[>ret=0.As shown in maple outputs, the given circuit has been modeled as polynomial setCM (its Groebner basis is denoted by CGB) and assertion representation as (m3[0]-1). From the running result, we have return value of NormalForm is 0 which means CGB be divided with no remainder by (m3[0]-1). Thus, from the previously mentioned verification principles, it is easy to conclude that the SERE assertion G1 holds under this circuit model after 1 cycle. Other results are shown in Table 2.Table 2
Result table.
Cycle no.
Polynomial
Result
Cycle1
m
1
[
0
]
,
m
2
[
0
]
,
m
3
[
0
]
-
1
r
e
t
=
0
Cycle2
m
1
[
1
]
,
m
2
[
1
]
-
1
,
m
3
[
1
]
r
e
t
≠
0, m1[1] fails
Cycle3
m
1
[
2
]
,
m
2
[
2
]
-
1
,
m
3
[
2
]
-
1
StopFrom Table2, when checking G2 assertion, the result ret:=NormalForm(m1[1],CGB,TDEG)=1≠0 so that we can conclude the assertion does not hold and there must exist some error in the original circuit. This case is a fairly complete illustration of how our checking algorithm works.


## 7. Conclusion

In this paper, we presented a new method for constrained SERE temporal assertions checking by combining symbolic simulation with symbolic algebraic approaches. We modified the original PSL specification to adapt our verification requirements and rebuilt a new constrained class of boolean and temporal layer.We first introduce a notion of symbolic constant for data path verification, which can gain great state coverage for simulation based verification. This method allows users to deal with more than one state and many input combinations at a time. This advantage comes directly from the fact that many vectors are simulated at once using symbolic value.We then defined a constrained simple subset of SERE and proposed an practical algebraization method for each temporal operator. For sequential circuits verification, we introduce a parameterized polynomial set modeling method based on time frame expansion.Our approach is based on polynomial models construction for both circuits and assertions. In other words, symbolic simulation is performed on data-flow model and its unrolled form in polynomial representation. Our method is to eventually translate a simulation based verification problem into a pure algebraic zero set determination problem by previously mentioned steps, which can be performed on any general symbolic algebraic tool. An experimental evaluation using maple has shown that the method is extremely efficient and useful.Furthermore, we can summarize the advantages of our checking method as follows:(1)
from the real case, we see that SERE properties verification can be achieved easier using symbolic algebraic than traditional method. Complex test bench or test vector is not essential for this approach;(2)
this advantage comes directly from the fact that many vectors are simulated at once using symbolic value;(3)
for assertion property verification, an efficient slicing reduction technique can be applied to gain performance improvement.Basically, our method can be taken as a useful theoretical insight for verification methodology.Finally, we plan to explore further tradeoffs and combine numeric computation with symbolic simulation for boosting performance, in particular, and to apply this method to more industrial case studies.



---

*Source: 272781-2013-04-30.xml*