# Wu’s Characteristic Set Method for SystemVerilog Assertions Verification

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

---

## Abstract

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.


---

## Body

## 1. Introduction

Currently, functional verification becomes an intensive challenge phase in the state-of-the-art digital systems development process. Assertion-based verification (ABV) has emerged as a promising solution to express and verify design properties.SystemVerilog [1–3], the industry’s first unified hardware description and verification language (HDVL), was developed originally by Accellera and can be viewed as an extension of the Verilog language with the added benefit of supporting object orientated constructs and assertions.SystemVerilog was adopted as IEEE Standard 1800–2005 firstly in 2005, and the latest version is IEEE standard 1800–2009, the current version. SystemVerilog has been accepted by a wide variety of companies and has been supported by most EDA companies in their tools in practice which has totally changed the way designers specify and verify functional requirements and properties of digital systems.Many efforts have been devoted to assertion checking solvers in recent years including model checking [4], theorem proving [5], and other simulation-based checking methods. In [6], an efficient approach to model check safety properties expressed in assertion property is studied. Proving SVA safety properties using induction-based BMC is studied in [7]. All these methods can be classified into two categories: formal and informal aspects.On the one hand, formal method such as model checking often suffers from “state explosion” problem and cannot be applied to large scale cases. Model checking of SVAs is PSPACE complete even for a “simple subset.” If more elaborated features, like intersection of regular expressions or instantiation of properties, are used, the problem becomes EXPSPACE complete.On the other hand, informal methods such as conventional simulation for assertion checking is a well-understood and most commonly used technique, but only feasible for very small scale systems and cannot provide exhaustive checking.A promising semiformal technique, symbolic simulation, proposed by Darringer [8] as early as 1979, can provide exhaustive checking by covering many conditions with a single simulation sequence.In our work, to address the challenge, we propose an alternative implementation mechanism based on Wu’s characteristic set by combining symbolic computation with symbolic simulation for assertions checking. This paper aims to verify whether an expected SVA property holds or not on the finite traces produced after several cycles running over a given sequential circuit.The underlying idea is that, for any combinational circuit model, we can derive its data flow based on polynomial representation model. Meanwhile, for any sequential circuit model and a given running cycle number, we can also derive its polynomial representation by unrolling this sequential circuit for several times into a pure combinational model. In a similar way, we can get polynomial set representation model of a temporal assertion written in SVA.By suitable restrictions of SVA and defining a constrained subset of SVA, we can get the polynomial set representations of the subset. Based on the polynomial set model, cycle-based symbolic simulation can be performed to produce symbolic traces. We then apply Wu’s method symbolic algebra approach to check the zeros set relation between their polynomial representations and determine whether the expected assertion holds or not at current running cycle.The rest of this paper is structured as follows. Preliminary knowledge with regarding to SystemVerilog used throughout this paper is introduced in Section2. Section 3 introduces polynomial representation modeling for synchronous digital systems. Section 4 describes the cycle-based model and sequential unrolling. Section 5 will discuss sequential assertions modeling with polynomials. In Section 6, we will propose a complete verification algorithm framework based on Wu’s characteristic set. Section 7 will demonstrate an example using MMP tool based on our method. In the last section, we make a short summary of our research and discuss the future work.


## 2. SystemVerilog Preliminary

In this section, we will give some preliminary knowledge which may be used in later sections of the paper.SystemVerilog, as an IEEE approved hardware description language, has combined many of the best features of both VHDL and Verilog and provided superior capabilities for system architecture, design, and verification.Therefore, on the one hand, VHDL users will recognize many of the SystemVerilog constructs, such as enumerated types, records, and multidimensional arrays.On the other hand, Verilog users can reuse existing designs: SystemVerilog is a superset of Verilog so no modification of existing Verilog code is required.SystemVerilog provides special language constructs and assertions [9, 10], to verify design behavior. An assertion is a statement that a specific condition, or sequence of conditions, in a design is true. If the condition or sequence is not true, the assertion statement will generate an error message.One important capability of SystemVerilog is the ability to define assertions outside of the Verilog modules and then bind them to a specific module or module instance. This feature allows test engineers to add assertions to existing Verilog models, without having to change the model in any way. One of the goals of SystemVerilog assertions is to provide a common semantic meaning for assertions so that they can be used to drive various design and verification tools.In SystemVerilog, there are two types of assertions: immediate assertions and concurrent assertions.Immediate assertions are primarily intended to be used with simulation and evaluate using simulation event-based semantics. While concurrent assertions are based on clock semantics and use sampled values of variables.Concurrent assertions can be used in always block or initial block as a statement, a module as a concurrent block, an interface block as a concurrent block, a program block as a concurrent block.An example of a property using sequence and formal argument is demonstrated as the following.propertytest[(ready,done,m_bus,x_bus)];intv_data;(ready,v_data=m_bus)##[3:5](done&&x_bus==v_data);endproperty[:test]The propertytest states that if ready holds then local variable v_data gets assigned the value of m_bus. Then within 3 to 5 cycles later, done is TRUE and x_bus should be equal to the contents of the saved local variable v_data. The property fails if ready is FALSE or if it follows a successful ready; the expression “done&&x_bus==v_data” fails to be TRUE within the range from 3 to 5 cycles after ready.As shown in this example, a concurrent assertion property in SystemVerilog will never be evaluated by itself except it is invoked by a verification statement. Therefore, only the statementassert propertytest(a,b,c,d) can cause the checker to perform assertion checking.The verification statement in SVA has three forms: assert, assume, and cover. In this paper, onlyassume and assert are involved: the statement assert to specify the property as a checker to ensure that the property holds for the design; the statement assume to specify the property as an assumption for the environment. The purpose of the assume statement is to allow properties to be considered as assumptions for formal analysis as well as for dynamic simulation tools.Basically, SVA has four language layers: Boolean, sequence, property, and statement.(1)
Boolean layer. The boolean layer consists of boolean expressions in which each variable referenced is either a design variable or a local variable of the assertion.(2)
Sequence layer. The sequence layer consists of regular expressions over the boolean layer.(3)
Property layer. The property layer combines sequences to create temporal logic formulas.(4)
Statement layer. The statement layer defines whether a property is to be evaluated as an obligation, an assumption, or a coverage goal.Moreover, SVA provides local variables as one of its distinguishing features. A local variable is used to capture the value of an expression at one point within a property and hold it for later reference, after which the local variable may be reassigned. We will provide an efficient way to handle this feature in later section of this paper.


## 3. Synchronous Digital System and Its Polynomial Representation

In this section, we will discuss polynomial set expressions for elementary units of combinational and sequential circuits.We mainly focus on the register transfer level (RTL) description of the circuit systems. Previous work [11, 12] has shown that any combinational circuit can be uniquely represented by a minimum order polynomial.Here, we give an alternative dataflow-based polynomial set representation model for our assertions checking purpose whose zero set can make such a data-flow model work well.


### 3.1. Combinational Logic 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) and basic logical operations, like “AND”, “OR”, and “NOT”, can be modeled by the following polynomial forms in Table 1.Table 1
Polynomial representation for arithmetic and logical units.
Arithmetic or logical operation
Polynomial set representation
y
=
a
+
b
{
y
-
a
-
b
}
y
=
a
-
b
{
y
-
a
+
b
}
y
=
a
*
b
{
y
-
a
*
b
}
y
=
a
/
b
{
y
*
b
-
a
}
y
=
N
O
T
x
{
1
-
x
-
y
}
y
=
x
1
A
N
D
x
2
{
x
1
*
x
2
-
y
}
y
=
x
1
O
R
x
2
{
x
1
+
x
2
-
x
1
*
x
2
-
y
}We will then discuss another important control structure in digital system, multiplexer, which can be used to join many small datapaths together to make bigger datapaths.Basically, multiplexer 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: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 ∏n-1i=0(s-i)=0.Note that for any bit-level variablexi(0≤i≤n), a limitation {xi*xi-xi} should be added for each.


### 3.2. Sequential Unit Modeling

In sequential circuits, flip-flops (FF) and latches are fundamental building blocks which are used as data storage elements. In this paper, we will reduce all sequential units to a simple unified model described below.The flip-flop can be equivalently modeled as a multiplexer. We have the following proposition to state this model.Proposition 1.
For aD-typed flip-flop model (D′ is the next state of D and y is the output signal of the flip-flop) with an enable signal c, then its equivalent combinational formal is y′=MUX(D,D′,s):i=s→y′=xi, (0≤i<2,x0=D,x1=D′), whose polynomial representation form can be described as{(y′-D)*(c-1), (y′-D′)*c, (y′-D)*(y′-D′)}  or{y′-D*(c-1)-D′*c}.Proof.
LetD be the current state and y′ denote the next state of the flip-flop. When the signal c is 0, y′ has the same value as D so that the FF maintains its present state; when the signal c is 1, y′ takes a new value from the D′ input (where D′ denotes the new value of next state of the FF). Therefore, we have the 2-value multiway branch model and its polynomial set representation for FF.
This establishes the proposition.Proposition 2.
LetD be an FF model (D′ is the next state of D and y is the output signal of the flip-flop) without enable signal; then its equivalent combinational formal polynomial algebraic model can be described as {y′-D}.Proof.
Straightforward.Proposition 3.
LetD be an FF model (D′ is the next state of D and y is the output signal of the flip-flop) with a reset signal; then its equivalent combinational formal polynomial algebraic model can be described as {y′-D*(1-reset)}.Proof.
Straightforward.


## 3.1. Combinational Logic 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) and basic logical operations, like “AND”, “OR”, and “NOT”, can be modeled by the following polynomial forms in Table 1.Table 1
Polynomial representation for arithmetic and logical units.
Arithmetic or logical operation
Polynomial set representation
y
=
a
+
b
{
y
-
a
-
b
}
y
=
a
-
b
{
y
-
a
+
b
}
y
=
a
*
b
{
y
-
a
*
b
}
y
=
a
/
b
{
y
*
b
-
a
}
y
=
N
O
T
x
{
1
-
x
-
y
}
y
=
x
1
A
N
D
x
2
{
x
1
*
x
2
-
y
}
y
=
x
1
O
R
x
2
{
x
1
+
x
2
-
x
1
*
x
2
-
y
}We will then discuss another important control structure in digital system, multiplexer, which can be used to join many small datapaths together to make bigger datapaths.Basically, multiplexer 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: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 ∏n-1i=0(s-i)=0.Note that for any bit-level variablexi(0≤i≤n), a limitation {xi*xi-xi} should be added for each.


## 3.2. Sequential Unit Modeling

In sequential circuits, flip-flops (FF) and latches are fundamental building blocks which are used as data storage elements. In this paper, we will reduce all sequential units to a simple unified model described below.The flip-flop can be equivalently modeled as a multiplexer. We have the following proposition to state this model.Proposition 1.
For aD-typed flip-flop model (D′ is the next state of D and y is the output signal of the flip-flop) with an enable signal c, then its equivalent combinational formal is y′=MUX(D,D′,s):i=s→y′=xi, (0≤i<2,x0=D,x1=D′), whose polynomial representation form can be described as{(y′-D)*(c-1), (y′-D′)*c, (y′-D)*(y′-D′)}  or{y′-D*(c-1)-D′*c}.Proof.
LetD be the current state and y′ denote the next state of the flip-flop. When the signal c is 0, y′ has the same value as D so that the FF maintains its present state; when the signal c is 1, y′ takes a new value from the D′ input (where D′ denotes the new value of next state of the FF). Therefore, we have the 2-value multiway branch model and its polynomial set representation for FF.
This establishes the proposition.Proposition 2.
LetD be an FF model (D′ is the next state of D and y is the output signal of the flip-flop) without enable signal; then its equivalent combinational formal polynomial algebraic model can be described as {y′-D}.Proof.
Straightforward.Proposition 3.
LetD be an FF model (D′ is the next state of D and y is the output signal of the flip-flop) with a reset signal; then its equivalent combinational formal polynomial algebraic model can be described as {y′-D*(1-reset)}.Proof.
Straightforward.


## 4. Cycle-Based Simulation and Sequential Unrolling

In this section, we will sketch the underlying system model for symbolic simulation used in our work.Basically, symbolic simulation takes in variables(x1,x2,…,xm), as shown in Figure 1, called free variables, as input and produces output expressions in terms of the variables (y1,y2,…,yn). The free variable can be either bit-level, integer, or constant 0 and 1. The symbolic simulator simulates simultaneously the entire set of the points that the input variables can take on.Figure 1
Symbolic simulation model.Cycle-based symbolical simulation of a circuit forn cycles can be regarded as unrolling the circuit n times. The unrolled circuit is a pure combinational one, and the ith copy of the circuit represents the circuit at cycle i. Thus, the unrolled circuit contains all the symbolic results for n cycles.The simulation process can be described as follows. Firstly, cycle-based symbolical simulation is initialized by setting the state of the circuit to the initial vector. 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 transformation-based optimization. Afterwards the newly generated functions are used as present state for the next state of simulation.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). Time-frame expansion is achieved by connecting the PPIs of the current time frame to the corresponding PPOs of the previous time frame.


## 5. SVA Expressions with Polynomial Set

In this section, we will discuss concurrent assertions and their temporal layer representation models.As mentioned previously, concurrent assertions express functional design intent and can be used to express assumed input behavior, expected output behavior, and forbidden behavior. That is, assertions define properties that the design must meet. Many properties can be expressed strictly from variables available in the design, while properties are often constructed out of sequential behaviors.We begin with the introduction of polynomial notions for various layers modeling.


### 5.1. Polynomial Notions and Algebraization

For clarity, we introduce the following symbolic notions for algebraic representation used in the rest of this paper.(1)
For any symbolic (circuit, unit, signal, sequence, property, etc.)f, its algebraic representation form is denoted by ⟦f⟧.(2)
If a running cyclet is given, its algebraic representation form can be denoted by ⟦f⟧[t].(3)
Furthermore, if a time range[m⋯n] is specified, its algebraic representation form can then be denoted by ⟦f⟧[t][m⋯n].Note that more detailed description of time range will be discussed in next subsection.For a given sequential circuit, to illustrate the sequential modeling for a given cycle number clearly, we will define the following indexed polynomial representation model for theith cycle by using the above notions.Definition 4 (indexed polynomial representation).
Letx[r][l](0≤r≤R,R∈N) denote the input signals for the lth clock cycle, m[s][l](0≤s≤S,S∈N) denote the intermediate signals, and y[t][l](0≤t≤T,T∈N) denote the output signals. We define the time-frame expansion model ⟦M⟧ as indexed polynomial representation for the sequential circuit C as the following:
(1)⟦M⟧={⋃i=0n‍⟦C⟧(…,⟦x[r][i]⟧,…,⟦m[s][i]⟧,…,⟦y[t][i]⟧,…)},
where, ⟦C⟧(…,⟦x[r][i]⟧,…,⟦m[s][i]⟧,…,⟦y[t][i]⟧,…) denotes the ith time-frame model of the original circuit and n denotes the number of clock cycle.In the following, we will discuss Boolean layer modeling based on above polynomial notions.The Boolean layer of SVA forms an underlying basis for the whole assertion architecture which consists of Boolean expressions that hold or do not hold at a given cycle.In SVA, the following are valid Boolean expressions:arrayA==arrayBarrayA!=arrayBarrayA[i]>=arrayB[j]arrayB[i][j+:2]==arrayA[k][m-:2](arrayA[i]&(arrayB[j]))==0For example, assertion(a[15:0]==b[15:0]) is also a valid Boolean expression stating that the 16-bit vectors a[15:0] and b[15:0] are equal.The state of a signal variable in current cyclei will be viewed as a zero of a set of polynomials. We have the zero set building rules.ZS-1: for any signal x which holds at a given time-frame i, thus, the state of x==1 (x is active high at cycle i) can be represented by polynomial {x[i]-1}. That is, ⟦x[i]⟧={x[i]-1}.ZS-2: alternatively, the state of x==0 (x is active low at time-frame i) can be represented by polynomial {x[i]}. That is, ⟦x[i]⟧={x[i]}.ZS-3: For any signal x and y, we have: ⟦x[i]∧y[j]⟧={(x[i]-1),(y[j]-1)} and ⟦x[i]∨y[j]⟧={(x[i]-1)(y[j]-1)} hold. Where i and j are time frames.


### 5.2. Time Range and Its Unrolled Model

We will then discuss the important feature of SVA, time range, and its signal constraint unrolled model.In SVA, for each sequence the earliest time step for the evaluation and the latest time step should be determined firstly. The sequence is then unrolled based on above information. Finally, the unrolled sequence will be modeled with polynomial set.In [7], a time range calculating algorithm is provided. Here, we will introduce some related definition and special handling for algebraization purpose. The syntax of “time range” can be described as follows:cycle_delay_const_range_expression::=constant_expression:constant_expression|constant_expression:$Note thatconstant_expression is computed at compiling time, must result in an integer value, and can only be 0 or greater.In this paper, we only focus on constant time range case. Thus, its form can be simplified as(1)
a##[m:n]b(m,n∈Nandn≥m≥0),(2)
S1##[m:n]S2(m,n∈Nandn≥m≥0),where,a, b are signals and S1, S2 are sequences.LetS:= “a##[m:n]b” (m,n∈Nandn≥m≥0) be a sequence; we will demonstrate how to equivalently derive its polynomial representation step by step through this example.Assume the starting time frame ist; then: the sequence S will start (n-m+1) sequences of evaluation which are
(2)⟹{a##mba##(m+1)b⋮a##(n-m+1)b,respectively.Correspondingly, we can derive their algebraic forms as follows:(3)⟹{⟦a##mb⟧[t]=⟦at∧bt+1⟧⟦a##(m+1)b⟧[t]=⟦at∧bt+2⟧⋮⟦a##(n-m+1)b⟧[t]=⟦at∧bt+n-m+1⟧,respectively.Then we have the equivalent form of above representation set as(4)⟹⟦S⟧[t]=⟦(at∧bt+m)∨⋯∨(at∧bt+n)⟧.Finally, we can have their polynomial set forms by following the zero set building rules discussed previously:ZS-1,ZS-2, and ZS-3.Similarly, we can also derive the equivalent algebraic representation of⟦S1##[m:n]S2⟧[t] by following the same steps.


### 5.3. Sequential Depth Calculation

The time range of a sequential is a time interval during which an operation or a terminal of a sequence has to be considered and is denoted by a closed bounded set of positive integers:(5)T=[l⋯h]={xl≤x≤h}(here,x,l,h∈N).Furthermore, the maximum of two intervalsT1 and T2 is defined by max(T1,T2)=[max(l1,l2)⋯max(h1,h2)].In the same manner, the sum of two time range, ofT1 and T2 is defined as T1+T2=[(l1+l2)⋯(h1+h2)].Definition 5 (maximum sequential depth).
The maximum sequential depth of a SVA expressionF or a sequence, written dep(F), is defined recursively:(1)
dep(a)=[1⋯1], if a is a signal;(2)
dep(¬a)=[1⋯1], if a is a signal;(3)
dep(F1##F2)=dep(F1)+dep(F2), if F1, F2 are sequences of SVA;(4)
dep(F1##[m:n]F2)=dep(F1)+dep(F2)+[m⋯n], if F1, F2 are sequences of SVA;(5)
dep(F1andF2)=max(dep(F1),dep(F2)), if F1, F2 are sequences of SVA;(6)
dep(F1orF2)=max(dep(F1),dep(F2)), if F1, F2 are sequences of SVA;(7)
dep(F1intersectF2)=dep(F1)+dep(F2)-1, if F1, F2 are sequences of SVA;(8)
dep(F[n])=n*dep(F), if F is a sequence of SVA.Note that ifdep(F)=[m⋯n], we have dep(F)·l=m and dep(F)·h=n.


### 5.4. Sequence Operator Modeling

Temporal assertions define not only the values of signals but also the relationship between signals over time. The sequences are the building blocks of temporal assertions and can express a set of linear behavior lasting one or more cycles. These sequences are usually used to specify and verify interface and bus protocols.A sequence is a regular expression over the boolean expressions that concisely specifies a set of linear sequences. The Boolean expressions must be true at those specific clock ticks for the sequence to be true over time.SystemVerilog provides several sequence composition operators to combine individual sequences in a variety of ways that enhance code writing and readability which can construct sequence expressions from Boolean expressions.In this paper,throughout operator, [1:$] operator, and the firstmatch operator are not supported by our method.In the following, we will discuss the algebraic representation of the supported sequence operators.(
1
)
c
y
c
l
e
d
e
l
a
y operator. In SystemVerilog, the ## construct is referred to as a cycle delay operator.“##1” and “##0” are concatenation operators: the former is the classical regular expression concatenation; the latter is a variant with one-letter overlapping. The cycle delay in SVA has two basic forms.(a)
A “##n” followed by a number n specifies the n cycles delay from the current clock cycle to the beginning of the sequence that follows.(b)
A “##[m⋯n]” followed by a rang [m⋯n] specifies the [m⋯n] cycles delay from the current clock cycle to the beginning of the sequence that follows.It is easy to derive the algebraic representation forms for this operator by following the method discussed in Section5.2.(
2
)
i
n
t
e
r
s
e
c
t operator. The two operands of intersect operator are sequences. The requirements for match of the intersect operation are as follows: (a)
both operands must match,(b)
the lengths of the two matches of the operand sequences must be the same.“R1intersectR2" denotes that R1 starts at the same time as R2. The intersection will match if R1, starting at the same time as R2, matches at the same time as R2 matches.The sequence length matching intersect operator constructs a sequence like theand nonlength matching operator, except that both sequences must complete in same cycle.(
3
)
a
n
d operator. This operation “R1andR2" states that R1 starts at the same time as R2 and the sequence expression matches with the later of R1 and R2 matching. This binary operator is used when both operands are expected to match, but the end times of the operand sequences can be different.That is, “R1andR2” denotes that both R1 and R2 hold for the same number cycles. Then, the matches of “R1andR2” must satisfy the following: (a)
the start point of the match ofR1 must not be earlier than the start point of the match of R2;(b)
the end point of the match ofR1 must not be later than the end point of the match of R2.The sequence nonlength matchingand operator constructs a sequence in which two sequences both hold at the current cycle regardless of whether they complete in the same cycle or in different cycles.(
4
)
o
r operator. The sequence or operator constructs a sequence in which one of two alternative sequences holds at the current cycle. Thus, the sequence “(a##1b)or(c##1d)” states that either sequence “a,b” or sequence “c,d” would satisfy the assertion.(
5
)
r
e
p
e
t
i
t
i
o
n operator. SystemVerilog allows the user to specify repetitions when defining sequences of Boolean expressions. The repetition counts can be specified as either a range of constants or a single constant expressions.The syntax of repetition operator can be illustrated as the following:non_consecutive_rep::=[=const_or_range_expr].The number of iterations of a repetition can be specified by exact count.From above discussion, we have the following rules for polynomial set-based representation.Rule 1.
Assume thatR, R1, and R2 are valid SVA sequences; the rules in Table 2 can be used to construct the corresponding polynomial set representations.Table 2
Polynomial representation for sequence operators.
NO.
Sequence
Polynomial set representation
1
a
#
#
n
b
(
{
⟦
a
⟧
[
t
]
,
⟦
b
⟧
[
t
+
n
]
}
)
a
#
#
[
m
⋯
n
]
b
∨
i
=
m
n
(
{
⟦
a
⟧
[
t
]
,
⟦
b
⟧
[
t
+
i
]
}
)
2
R
1
i
n
t
e
r
s
e
c
t
R
2
{
⟦
R
1
⟧
[
t
]
d
e
p
(
R
1
)
}
∧
{
⟦
R
2
⟧
[
t
]
d
e
p
(
R
1
)
}
3
R
1
a
n
d
R
2
∨
i
=
l
1
h
1
∨
j
=
l
2
h
2
(
{
⟦
R
1
⟧
[
t
]
i
}
∧
{
⟦
R
2
⟧
[
t
]
j
}
)
Here,li=dep(Ri)·l; hi=dep(Ri)·h
(
1
≤
i
≤
2
)
4
R
1
o
r
R
2
∨
i
=
l
1
h
1
∨
j
=
l
2
h
2
(
{
⟦
R
1
⟧
[
t
]
i
}
∨
{
⟦
R
2
⟧
[
t
]
j
}
)
Here,li=dep(Ri)·l; hi=dep(Ri)·h
(
1
≤
i
≤
2
)
5
R
[
=
n
]
∨
i
=
0
n
(
{
⟦
R
1
⟧
[
t
]
i
*
d
e
p
(
R
)
}
)


### 5.5. Local Variables Representation

An important feature in SVA is that variables can be used in assertions which is highly useful in pipelined designs. These local variables are optional and local to properties. They can be initialized, assigned or reassigned a value, operated on, and compared to other expressions.The dynamic creation of a variable and its assignment are achieved by using the local variable declaration in a sequence or property declaration and making an assignment in the sequence.A simple example of property with a local variable is specified below:propertydataout;logic[31:0]x;@(posedgeclk)($rose(load),x=data)∣=>##[0:5](ready&&dout&&data==x)∣=>##[0:3]done&&q==x;endpropertyThus, local variables of a sequence (or property) may be set to a value, which can be computed from a parameter or other objects (e.g., arguments. constants, or objects visible by the sequence (or property)).For the algebraization of SVA properties with local variables, in our method these local variables will be taken as common signal variables (symbolic constant) without any sequential information.Thus, the polynomial set representation for propertydataout will be translated in the following form:
(6)⟦dataout⟧[t]={⋯(⟦data⟧[t]-x),…,(⟦q⟧[t]-x)}.


### 5.6. Property Operator Modeling

In SVA, a property that is a sequence evaluates to true if, and only if, there is a nonempty match of the sequence. Property expressions are built using sequences, other sublevel properties, and simple Boolean expressions via property connectives.In general, property expressions are built using sequences, other sublevel properties, and simple Boolean expressions.These individual elements are combined using property operators which are listed as follows:P::=R (“sequence” form);|(P) (“parenthesis” form);|NOTP (“negation” form);|(P1ORP2) (“or” form);|(P1ANDP2) (“and” form);|(R∣->P) (“implication” form);|(R∣=>P) (“implication” form);|disableiff(b)P (“reset” form)Note thatdisable iff will not be supported in this paper. Property operators construct properties out of sequence expressions.(
1
)
I
m
p
l
i
c
a
t
i
o
n operators. The SystemVerilog implication operator supports sequence implication and provides two forms of implication: overlapped using operator |-> and nonoverlapped using operator |=>, respectively.The implication operator takes a sequence as its antecedent and a property as its consequent. For each successful match of the antecedent sequence, the consequence sequence is separately evaluated, beginning at the end point of the matched antecedent sequence. All matches of antecedent sequence require a match of the consequence sequence.(
2
)
N
O
T operator. “NOTP” states that the evaluation of the property returns the opposite of the evaluation of the underlying P.(
3
)
A
N
D operator. “P1ANDP2” states that the property evaluates to true if, and only if, both P1 and P2 evaluate to true.(
4
)
O
R operator. “P1ORP2” states that the property evaluates to true if, and only if, at least one of P1 and P2 evaluates to true.(
5
)
I
F
-
E
L
S
E operator. This operator has two valid forms which are listed as follows.(a)
IF(dist)P1. A property of this form evaluates to true if, and only if, either dist evaluates to false or P1 evaluates to true.(b)
IF(dist)P1ELSEP2. A property of this form evaluates to true if, and only if, either dist evaluates to true and P1 evaluates to true or dist evaluates to false and P2 evaluates to true.From the previous discussion, we have the checking rules for property reasoning.Rule 2.
Assume thatP, P1, and P2 are valid SVA properties, S denotes a SVA sequence, and M denotes the system model to be checked; the following transformation rules in Table 3 are used to construct the corresponding verification process, where AssChk(Model,Property):{ture,false} is a self-defined justification function which can take either polynomial sets or original models as input arguments and is used to determine wether a given Property holds or not with respect to a circuit model Model. Additionally, ¬, ∨, and ∧ are standard logical connectives.Table 3
Polynomial representation for property operators.
Property operation
Polynomial set representation
P
1  OR  P2
A
s
s
C
h
k
(
⟦
M
⟧
,
⟦
P
1
⟧
)
∨
A
s
s
C
h
k
(
⟦
M
⟧
,
⟦
P
2
⟧
)
P
1
A
N
D  P2
A
s
s
C
h
k
(
⟦
M
⟧
,
⟦
P
1
⟧
)
∧
A
s
s
C
h
k
(
⟦
M
⟧
,
⟦
P
2
⟧
)
N
O
T  P
¬
A
s
s
C
h
k
(
⟦
M
⟧
,
⟦
P
⟧
)
I
F  (dist)  P1
¬
A
s
s
C
h
k
(
⟦
M
⟧
,
d
i
s
t
)
∨
A
s
s
C
h
k
(
⟦
M
⟧
,
⟦
P
1
⟧
)
I
F  (dist)P1 ELSEP2
(
A
s
s
C
h
k
(
⟦
M
⟧
,
d
i
s
t
)
∧
A
s
s
C
h
k
(
⟦
M
⟧
,
⟦
P
1
⟧
)
)
∨
(
¬
A
s
s
C
h
k
(
⟦
M
⟧
,
d
i
s
t
)
∧
A
s
s
C
h
k
(
⟦
M
⟧
,
⟦
P
2
⟧
)
)
S
|
-
>  P
i
f  (¬AssChk(⟦M⟧,⟦S⟧))returntrue
e
l
s
e
(
A
s
s
C
h
k
(
⟦
M
⟧
,
⟦
S
⟧
[
t
]
)
∧
A
s
s
C
h
k
(
⟦
M
⟧
,
⟦
P
⟧
[
t
+
d
e
p
(
S
)
-
1
]
d
e
p
(
P
)
)
)
S
|
=
>  P
i
f  (¬AssChk(⟦M⟧,⟦S⟧))returntrue
e
l
s
e
(
A
s
s
C
h
k
(
⟦
M
⟧
,
⟦
S
⟧
[
t
]
)
∧
A
s
s
C
h
k
(
⟦
M
⟧
,
⟦
P
⟧
[
t
+
d
e
p
(
S
)
]
d
e
p
(
P
)
)
)


### 5.7. Constrained Subset of SVAs

SystemVerilog assertions formally define the syntax and grammar of an assertion language that can define design properties and constraints, including temporal (i.e., spread over several cycles) characteristics. The atoms of the SVA concurrent assertions are so called sequences. A sequence is a regular expression that describes the behavior of signals over time. A property of SVA is composed of sequences by property operators.As described in [13], the total set of SVA can be divided into 4 subgroups, namely, simple sequence expression (SSE), interval sequence expression (ISE), complex sequence expression (CSE), and unbounded sequence expression (USE). Here, in our method, only a subset of these groups can be supported.Formally, we will give the following definition for this subset.Definition 6 (constrained subset of SVA).
The constrained subset of SVA supported by algebraic symbolic polynomial representation is defined recursively as the following:(1)
R::=b|(v=e)|(R)|(R##m)|(R##[m⋯n]R)|(RorR)|(R1intersectR2)|R[=n]|(R1andR2),(2)
P::=R|(P)|NOTP|(P1ANDP2)|(P1ORP2|(R∣->P)|(R∣=>P)),
whereb denotes a Boolean expression and all Boolean operators are supported, R (R1, R2) denotes a sequence, P (P1, P2) denotes a property, v denotes a local variable name, and e denotes an expression.For sequence operators, unspecified upper bound time range andfirst-match operator are excluded from the constrained subset. Additionally, property operator disable iff will not be supported also.In this paper, only a constrained subset of SVA language defined above can be supported by our method.Firstly, we translate the properties described by the constrained subset of SVA 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 finite polynomial set.Then, the verification problem is reduced to proving zero set inclusion relationship which can be resolved by characteristic set-based algebraic approaches.


## 5.1. Polynomial Notions and Algebraization

For clarity, we introduce the following symbolic notions for algebraic representation used in the rest of this paper.(1)
For any symbolic (circuit, unit, signal, sequence, property, etc.)f, its algebraic representation form is denoted by ⟦f⟧.(2)
If a running cyclet is given, its algebraic representation form can be denoted by ⟦f⟧[t].(3)
Furthermore, if a time range[m⋯n] is specified, its algebraic representation form can then be denoted by ⟦f⟧[t][m⋯n].Note that more detailed description of time range will be discussed in next subsection.For a given sequential circuit, to illustrate the sequential modeling for a given cycle number clearly, we will define the following indexed polynomial representation model for theith cycle by using the above notions.Definition 4 (indexed polynomial representation).
Letx[r][l](0≤r≤R,R∈N) denote the input signals for the lth clock cycle, m[s][l](0≤s≤S,S∈N) denote the intermediate signals, and y[t][l](0≤t≤T,T∈N) denote the output signals. We define the time-frame expansion model ⟦M⟧ as indexed polynomial representation for the sequential circuit C as the following:
(1)⟦M⟧={⋃i=0n‍⟦C⟧(…,⟦x[r][i]⟧,…,⟦m[s][i]⟧,…,⟦y[t][i]⟧,…)},
where, ⟦C⟧(…,⟦x[r][i]⟧,…,⟦m[s][i]⟧,…,⟦y[t][i]⟧,…) denotes the ith time-frame model of the original circuit and n denotes the number of clock cycle.In the following, we will discuss Boolean layer modeling based on above polynomial notions.The Boolean layer of SVA forms an underlying basis for the whole assertion architecture which consists of Boolean expressions that hold or do not hold at a given cycle.In SVA, the following are valid Boolean expressions:arrayA==arrayBarrayA!=arrayBarrayA[i]>=arrayB[j]arrayB[i][j+:2]==arrayA[k][m-:2](arrayA[i]&(arrayB[j]))==0For example, assertion(a[15:0]==b[15:0]) is also a valid Boolean expression stating that the 16-bit vectors a[15:0] and b[15:0] are equal.The state of a signal variable in current cyclei will be viewed as a zero of a set of polynomials. We have the zero set building rules.ZS-1: for any signal x which holds at a given time-frame i, thus, the state of x==1 (x is active high at cycle i) can be represented by polynomial {x[i]-1}. That is, ⟦x[i]⟧={x[i]-1}.ZS-2: alternatively, the state of x==0 (x is active low at time-frame i) can be represented by polynomial {x[i]}. That is, ⟦x[i]⟧={x[i]}.ZS-3: For any signal x and y, we have: ⟦x[i]∧y[j]⟧={(x[i]-1),(y[j]-1)} and ⟦x[i]∨y[j]⟧={(x[i]-1)(y[j]-1)} hold. Where i and j are time frames.


## 5.2. Time Range and Its Unrolled Model

We will then discuss the important feature of SVA, time range, and its signal constraint unrolled model.In SVA, for each sequence the earliest time step for the evaluation and the latest time step should be determined firstly. The sequence is then unrolled based on above information. Finally, the unrolled sequence will be modeled with polynomial set.In [7], a time range calculating algorithm is provided. Here, we will introduce some related definition and special handling for algebraization purpose. The syntax of “time range” can be described as follows:cycle_delay_const_range_expression::=constant_expression:constant_expression|constant_expression:$Note thatconstant_expression is computed at compiling time, must result in an integer value, and can only be 0 or greater.In this paper, we only focus on constant time range case. Thus, its form can be simplified as(1)
a##[m:n]b(m,n∈Nandn≥m≥0),(2)
S1##[m:n]S2(m,n∈Nandn≥m≥0),where,a, b are signals and S1, S2 are sequences.LetS:= “a##[m:n]b” (m,n∈Nandn≥m≥0) be a sequence; we will demonstrate how to equivalently derive its polynomial representation step by step through this example.Assume the starting time frame ist; then: the sequence S will start (n-m+1) sequences of evaluation which are
(2)⟹{a##mba##(m+1)b⋮a##(n-m+1)b,respectively.Correspondingly, we can derive their algebraic forms as follows:(3)⟹{⟦a##mb⟧[t]=⟦at∧bt+1⟧⟦a##(m+1)b⟧[t]=⟦at∧bt+2⟧⋮⟦a##(n-m+1)b⟧[t]=⟦at∧bt+n-m+1⟧,respectively.Then we have the equivalent form of above representation set as(4)⟹⟦S⟧[t]=⟦(at∧bt+m)∨⋯∨(at∧bt+n)⟧.Finally, we can have their polynomial set forms by following the zero set building rules discussed previously:ZS-1,ZS-2, and ZS-3.Similarly, we can also derive the equivalent algebraic representation of⟦S1##[m:n]S2⟧[t] by following the same steps.


## 5.3. Sequential Depth Calculation

The time range of a sequential is a time interval during which an operation or a terminal of a sequence has to be considered and is denoted by a closed bounded set of positive integers:(5)T=[l⋯h]={xl≤x≤h}(here,x,l,h∈N).Furthermore, the maximum of two intervalsT1 and T2 is defined by max(T1,T2)=[max(l1,l2)⋯max(h1,h2)].In the same manner, the sum of two time range, ofT1 and T2 is defined as T1+T2=[(l1+l2)⋯(h1+h2)].Definition 5 (maximum sequential depth).
The maximum sequential depth of a SVA expressionF or a sequence, written dep(F), is defined recursively:(1)
dep(a)=[1⋯1], if a is a signal;(2)
dep(¬a)=[1⋯1], if a is a signal;(3)
dep(F1##F2)=dep(F1)+dep(F2), if F1, F2 are sequences of SVA;(4)
dep(F1##[m:n]F2)=dep(F1)+dep(F2)+[m⋯n], if F1, F2 are sequences of SVA;(5)
dep(F1andF2)=max(dep(F1),dep(F2)), if F1, F2 are sequences of SVA;(6)
dep(F1orF2)=max(dep(F1),dep(F2)), if F1, F2 are sequences of SVA;(7)
dep(F1intersectF2)=dep(F1)+dep(F2)-1, if F1, F2 are sequences of SVA;(8)
dep(F[n])=n*dep(F), if F is a sequence of SVA.Note that ifdep(F)=[m⋯n], we have dep(F)·l=m and dep(F)·h=n.


## 5.4. Sequence Operator Modeling

Temporal assertions define not only the values of signals but also the relationship between signals over time. The sequences are the building blocks of temporal assertions and can express a set of linear behavior lasting one or more cycles. These sequences are usually used to specify and verify interface and bus protocols.A sequence is a regular expression over the boolean expressions that concisely specifies a set of linear sequences. The Boolean expressions must be true at those specific clock ticks for the sequence to be true over time.SystemVerilog provides several sequence composition operators to combine individual sequences in a variety of ways that enhance code writing and readability which can construct sequence expressions from Boolean expressions.In this paper,throughout operator, [1:$] operator, and the firstmatch operator are not supported by our method.In the following, we will discuss the algebraic representation of the supported sequence operators.(
1
)
c
y
c
l
e
d
e
l
a
y operator. In SystemVerilog, the ## construct is referred to as a cycle delay operator.“##1” and “##0” are concatenation operators: the former is the classical regular expression concatenation; the latter is a variant with one-letter overlapping. The cycle delay in SVA has two basic forms.(a)
A “##n” followed by a number n specifies the n cycles delay from the current clock cycle to the beginning of the sequence that follows.(b)
A “##[m⋯n]” followed by a rang [m⋯n] specifies the [m⋯n] cycles delay from the current clock cycle to the beginning of the sequence that follows.It is easy to derive the algebraic representation forms for this operator by following the method discussed in Section5.2.(
2
)
i
n
t
e
r
s
e
c
t operator. The two operands of intersect operator are sequences. The requirements for match of the intersect operation are as follows: (a)
both operands must match,(b)
the lengths of the two matches of the operand sequences must be the same.“R1intersectR2" denotes that R1 starts at the same time as R2. The intersection will match if R1, starting at the same time as R2, matches at the same time as R2 matches.The sequence length matching intersect operator constructs a sequence like theand nonlength matching operator, except that both sequences must complete in same cycle.(
3
)
a
n
d operator. This operation “R1andR2" states that R1 starts at the same time as R2 and the sequence expression matches with the later of R1 and R2 matching. This binary operator is used when both operands are expected to match, but the end times of the operand sequences can be different.That is, “R1andR2” denotes that both R1 and R2 hold for the same number cycles. Then, the matches of “R1andR2” must satisfy the following: (a)
the start point of the match ofR1 must not be earlier than the start point of the match of R2;(b)
the end point of the match ofR1 must not be later than the end point of the match of R2.The sequence nonlength matchingand operator constructs a sequence in which two sequences both hold at the current cycle regardless of whether they complete in the same cycle or in different cycles.(
4
)
o
r operator. The sequence or operator constructs a sequence in which one of two alternative sequences holds at the current cycle. Thus, the sequence “(a##1b)or(c##1d)” states that either sequence “a,b” or sequence “c,d” would satisfy the assertion.(
5
)
r
e
p
e
t
i
t
i
o
n operator. SystemVerilog allows the user to specify repetitions when defining sequences of Boolean expressions. The repetition counts can be specified as either a range of constants or a single constant expressions.The syntax of repetition operator can be illustrated as the following:non_consecutive_rep::=[=const_or_range_expr].The number of iterations of a repetition can be specified by exact count.From above discussion, we have the following rules for polynomial set-based representation.Rule 1.
Assume thatR, R1, and R2 are valid SVA sequences; the rules in Table 2 can be used to construct the corresponding polynomial set representations.Table 2
Polynomial representation for sequence operators.
NO.
Sequence
Polynomial set representation
1
a
#
#
n
b
(
{
⟦
a
⟧
[
t
]
,
⟦
b
⟧
[
t
+
n
]
}
)
a
#
#
[
m
⋯
n
]
b
∨
i
=
m
n
(
{
⟦
a
⟧
[
t
]
,
⟦
b
⟧
[
t
+
i
]
}
)
2
R
1
i
n
t
e
r
s
e
c
t
R
2
{
⟦
R
1
⟧
[
t
]
d
e
p
(
R
1
)
}
∧
{
⟦
R
2
⟧
[
t
]
d
e
p
(
R
1
)
}
3
R
1
a
n
d
R
2
∨
i
=
l
1
h
1
∨
j
=
l
2
h
2
(
{
⟦
R
1
⟧
[
t
]
i
}
∧
{
⟦
R
2
⟧
[
t
]
j
}
)
Here,li=dep(Ri)·l; hi=dep(Ri)·h
(
1
≤
i
≤
2
)
4
R
1
o
r
R
2
∨
i
=
l
1
h
1
∨
j
=
l
2
h
2
(
{
⟦
R
1
⟧
[
t
]
i
}
∨
{
⟦
R
2
⟧
[
t
]
j
}
)
Here,li=dep(Ri)·l; hi=dep(Ri)·h
(
1
≤
i
≤
2
)
5
R
[
=
n
]
∨
i
=
0
n
(
{
⟦
R
1
⟧
[
t
]
i
*
d
e
p
(
R
)
}
)


## 5.5. Local Variables Representation

An important feature in SVA is that variables can be used in assertions which is highly useful in pipelined designs. These local variables are optional and local to properties. They can be initialized, assigned or reassigned a value, operated on, and compared to other expressions.The dynamic creation of a variable and its assignment are achieved by using the local variable declaration in a sequence or property declaration and making an assignment in the sequence.A simple example of property with a local variable is specified below:propertydataout;logic[31:0]x;@(posedgeclk)($rose(load),x=data)∣=>##[0:5](ready&&dout&&data==x)∣=>##[0:3]done&&q==x;endpropertyThus, local variables of a sequence (or property) may be set to a value, which can be computed from a parameter or other objects (e.g., arguments. constants, or objects visible by the sequence (or property)).For the algebraization of SVA properties with local variables, in our method these local variables will be taken as common signal variables (symbolic constant) without any sequential information.Thus, the polynomial set representation for propertydataout will be translated in the following form:
(6)⟦dataout⟧[t]={⋯(⟦data⟧[t]-x),…,(⟦q⟧[t]-x)}.


## 5.6. Property Operator Modeling

In SVA, a property that is a sequence evaluates to true if, and only if, there is a nonempty match of the sequence. Property expressions are built using sequences, other sublevel properties, and simple Boolean expressions via property connectives.In general, property expressions are built using sequences, other sublevel properties, and simple Boolean expressions.These individual elements are combined using property operators which are listed as follows:P::=R (“sequence” form);|(P) (“parenthesis” form);|NOTP (“negation” form);|(P1ORP2) (“or” form);|(P1ANDP2) (“and” form);|(R∣->P) (“implication” form);|(R∣=>P) (“implication” form);|disableiff(b)P (“reset” form)Note thatdisable iff will not be supported in this paper. Property operators construct properties out of sequence expressions.(
1
)
I
m
p
l
i
c
a
t
i
o
n operators. The SystemVerilog implication operator supports sequence implication and provides two forms of implication: overlapped using operator |-> and nonoverlapped using operator |=>, respectively.The implication operator takes a sequence as its antecedent and a property as its consequent. For each successful match of the antecedent sequence, the consequence sequence is separately evaluated, beginning at the end point of the matched antecedent sequence. All matches of antecedent sequence require a match of the consequence sequence.(
2
)
N
O
T operator. “NOTP” states that the evaluation of the property returns the opposite of the evaluation of the underlying P.(
3
)
A
N
D operator. “P1ANDP2” states that the property evaluates to true if, and only if, both P1 and P2 evaluate to true.(
4
)
O
R operator. “P1ORP2” states that the property evaluates to true if, and only if, at least one of P1 and P2 evaluates to true.(
5
)
I
F
-
E
L
S
E operator. This operator has two valid forms which are listed as follows.(a)
IF(dist)P1. A property of this form evaluates to true if, and only if, either dist evaluates to false or P1 evaluates to true.(b)
IF(dist)P1ELSEP2. A property of this form evaluates to true if, and only if, either dist evaluates to true and P1 evaluates to true or dist evaluates to false and P2 evaluates to true.From the previous discussion, we have the checking rules for property reasoning.Rule 2.
Assume thatP, P1, and P2 are valid SVA properties, S denotes a SVA sequence, and M denotes the system model to be checked; the following transformation rules in Table 3 are used to construct the corresponding verification process, where AssChk(Model,Property):{ture,false} is a self-defined justification function which can take either polynomial sets or original models as input arguments and is used to determine wether a given Property holds or not with respect to a circuit model Model. Additionally, ¬, ∨, and ∧ are standard logical connectives.Table 3
Polynomial representation for property operators.
Property operation
Polynomial set representation
P
1  OR  P2
A
s
s
C
h
k
(
⟦
M
⟧
,
⟦
P
1
⟧
)
∨
A
s
s
C
h
k
(
⟦
M
⟧
,
⟦
P
2
⟧
)
P
1
A
N
D  P2
A
s
s
C
h
k
(
⟦
M
⟧
,
⟦
P
1
⟧
)
∧
A
s
s
C
h
k
(
⟦
M
⟧
,
⟦
P
2
⟧
)
N
O
T  P
¬
A
s
s
C
h
k
(
⟦
M
⟧
,
⟦
P
⟧
)
I
F  (dist)  P1
¬
A
s
s
C
h
k
(
⟦
M
⟧
,
d
i
s
t
)
∨
A
s
s
C
h
k
(
⟦
M
⟧
,
⟦
P
1
⟧
)
I
F  (dist)P1 ELSEP2
(
A
s
s
C
h
k
(
⟦
M
⟧
,
d
i
s
t
)
∧
A
s
s
C
h
k
(
⟦
M
⟧
,
⟦
P
1
⟧
)
)
∨
(
¬
A
s
s
C
h
k
(
⟦
M
⟧
,
d
i
s
t
)
∧
A
s
s
C
h
k
(
⟦
M
⟧
,
⟦
P
2
⟧
)
)
S
|
-
>  P
i
f  (¬AssChk(⟦M⟧,⟦S⟧))returntrue
e
l
s
e
(
A
s
s
C
h
k
(
⟦
M
⟧
,
⟦
S
⟧
[
t
]
)
∧
A
s
s
C
h
k
(
⟦
M
⟧
,
⟦
P
⟧
[
t
+
d
e
p
(
S
)
-
1
]
d
e
p
(
P
)
)
)
S
|
=
>  P
i
f  (¬AssChk(⟦M⟧,⟦S⟧))returntrue
e
l
s
e
(
A
s
s
C
h
k
(
⟦
M
⟧
,
⟦
S
⟧
[
t
]
)
∧
A
s
s
C
h
k
(
⟦
M
⟧
,
⟦
P
⟧
[
t
+
d
e
p
(
S
)
]
d
e
p
(
P
)
)
)


## 5.7. Constrained Subset of SVAs

SystemVerilog assertions formally define the syntax and grammar of an assertion language that can define design properties and constraints, including temporal (i.e., spread over several cycles) characteristics. The atoms of the SVA concurrent assertions are so called sequences. A sequence is a regular expression that describes the behavior of signals over time. A property of SVA is composed of sequences by property operators.As described in [13], the total set of SVA can be divided into 4 subgroups, namely, simple sequence expression (SSE), interval sequence expression (ISE), complex sequence expression (CSE), and unbounded sequence expression (USE). Here, in our method, only a subset of these groups can be supported.Formally, we will give the following definition for this subset.Definition 6 (constrained subset of SVA).
The constrained subset of SVA supported by algebraic symbolic polynomial representation is defined recursively as the following:(1)
R::=b|(v=e)|(R)|(R##m)|(R##[m⋯n]R)|(RorR)|(R1intersectR2)|R[=n]|(R1andR2),(2)
P::=R|(P)|NOTP|(P1ANDP2)|(P1ORP2|(R∣->P)|(R∣=>P)),
whereb denotes a Boolean expression and all Boolean operators are supported, R (R1, R2) denotes a sequence, P (P1, P2) denotes a property, v denotes a local variable name, and e denotes an expression.For sequence operators, unspecified upper bound time range andfirst-match operator are excluded from the constrained subset. Additionally, property operator disable iff will not be supported also.In this paper, only a constrained subset of SVA language defined above can be supported by our method.Firstly, we translate the properties described by the constrained subset of SVA 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 finite polynomial set.Then, the verification problem is reduced to proving zero set inclusion relationship which can be resolved by characteristic set-based algebraic approaches.


## 6. Characteristic Set Based Verification Principle and Algorithm

In this section, we will discuss the checking algorithm based on Wu’s characteristic set. We first recall some fundamental knowledge in Wu’s method.


### 6.1. Wu’s Method Preliminary

Wu’s method [14, 15] is an efficient algorithm for solving multivariate polynomial equations introduced by Wen-Tsun Wu. It also has succeeded in mechanical geometry theorem proving. For further details and elementary introduction, we refer the reader to [16].LetPi=k[x1,…,xi] denote the polynomial ring in variables x1,x2,…,xi with coefficient k, for every i in the range {1,…,n}, and k is an algebraically closed field.In what follows, without loss of generality, we assume that the given variables ordering is fixed as(7)x1≺x2≺⋯≺xn.
Assume p∈k[x1,…,xn] and let deg(p,xi) be the maximum degree of p with respect to xi.Definition 7.
Letp∈Pi; the greatest variable v∈{x1,…,xi} is called the main variable of p such that deg(p,v)≠0, denoted by mvar(p). The biggest index i is called the class, denoted by class(p). If we assume p as a univariate polynomial with mvar(p)=xi, we can write p=cxid+r, where d=deg(p,xi). In this case, c and d are, respectively, the initial and the main degree and are denoted by init(p) and mdeg(p).Definition 8 (pseudo division).
For any two polynomialsf,g∈Pi, with class(f)=j. There exist a nonnegative number α and polynomials q and r, such that init(f)αg=qf+r. Where r is denoted by prem(g,f,xj). We denote the remainder r on pseudo division (pseudo remainder) of f by g with respect to the variable y by prem(f,g,y).Definition 9 (Wu’s characteristic set).
LetPS and CS be two polynomial system, and CS is a triangular set; a triangular set is called a characteristic set of PS if
(8)∀p∈PS,prem(p,CS)=0.Theorem 10 (zero decomposition theorem).
LetZero(PS) denote the zero set of PS and CS be a characteristic set of P; then
(9)Zero(PS)=Zero(CSinit(CS))∪Zero(PSi),
where PSi=PS∪init(CS)i.Now we briefly outline the essential steps about Wu’s method on geometry theorem proving [17].(
1
) Algebraize a geometric theorem by converting it into a system of algebraic equations. We will translate the theorem’s hypotheses into a set of hypotheses equations {f1,…,fr},
(10)f1=f1(x1,…,xn),f2=f2(x1,…,xn),⋮fr=fr(x1,…,xn),
and the theorem’s conclusion into a polynomial g(x1,…,xn).(
2
) Triangulize the system of hypotheses equations using pseudo-division. Then we will obtain the hypothesis equations denoted as
(11)f1=f1(u1,…,ud,x1),f2=f2(u1,…,ud,x1,x2),⋮fr=fr(u1,…,ud,x1,…,xr).(
3
) Perform successive pseudo division on the transformed hypotheses in triangular form {f1,f2,…,fr} by the conclusion equation g(x1,…,xn), yielding a final remainder r0:
(12)r0=prem(⋯prem(g,fr,xpr),…,f1,xp1).
If this final remainder r0≡0, we will say that the conclusion g follows from the hypotheses {f1,…,fr}.As mentioned above, the characteristic set of a polynomial system is a special triangular form. We can use the characteristic set of hypotheses equations as the triangular form, denoted bycharset(f1,…,fr). Roughly speaking, the soul of Wu’s method on theorem proving is to check whether the zero set of the expected consequent equations includes the zero set of hypotheses equations or not.Our checking method is based on algebraic geometry that studies of geometric objects arising as the common zeros of collections of polynomials. The aim is to find polynomials whose zeros correspond to pairs of states in which the appropriate assignments are made.Letzero(PC) and zero(PS) denote the zero set for circuit polynomial set PC and assertions polynomial set PS respectively. Let C⊨s denote that assertion s holds under model C.We aim to attempt to determine whether assertions holds or not. Therefore, we have
(13)(s⊨C)⟺Zero(PC)⊆Zero(PS).Theorem 11.
Suppose thatG=[𝒜⇒𝒞] is a property, 𝒜 is the precondition of 𝒞, and M is a system model. Let PA and PM be the polynomial set representations for 𝒜 and M, respectively, constructed by previous mentioned rules. PC is the polynomial set representation for 𝒞.
LetH=A∪M, PH=PA∪PM={h1,h2,…,hs}⊆k[x1,…,xn], CS=charset(PH); charset(PH) denotes the characteristic set of PH, and prem(PC,CS) is the function which computs the remainder by successive pseudo division; then we have
(14)prem(PC,CS)==0⟺(M∣=G).Proof.
Firstly, letzero(PA) and zero(PM) denote the zero sets for circuit polynomial set 𝒜 and assertions polynomial set M, respectively. Since PH=PA∪PM={h1,h2,…,hs}⊆k[x1,…,xn], let zero(PH) denote the zero sets for zero(PA∪PM={h1,h2,…,hs}). Let H⊨C denote that the assertion C holds under model H.
Our aim is to attempt to determine whether assertionC holds or not. Thus, we have
(15)(M⊨G)⟺(H⊨C)⟺zero(PH)⊆zero(PC).
As mentioned previously, Wu’s method can be used to determine the inclusion relationship of zero sets. Thus we have
(16)prem(PC,charset(PH))==0⟺zero(PH)⊆zero(PC).
LetCS=charset(PH), which denotes the characteristic set of PH; according to (15) and (16), we have
(17)(prem(PC,CS)==0)⟺(M∣=G).
This establishes the theorem.


### 6.2. Checking Algorithm

From above discussion, we have the following core decision algorithm.Algorithm 12 (Assertion Checking:AssChk(M,G)).
Input: Circuit model M, an assertion G=[𝒜⇒𝒞];
Output: Boolean: true or false;
BEGIN
/* Step 0: initialize input signals via testbench */
00InitSignals();
01M=∅;PSA=∅;H=∅;PSC=∅;
/* Step 1: build polynomial set for antecedent𝒜 */
02PS𝒜=BuildPS(𝒜);
/* Step 2: build polynomial set for consequent𝒞 */
03PS𝒞=BuildPS(𝒞);
/*Step 3: calculate thePS𝒜∪M */
04H=PS𝒜∪M;
/*Step 4: calculate the characteristic set ofH */
05CS:=Charset(H);
/*Step 5: check the final remainder by successive pseudo-division */
06 if(prem(PS𝒞,CS)≠0){
07 returnfalse;
}
08 returntrue; /* Assertion does hold */
END


## 6.1. Wu’s Method Preliminary

Wu’s method [14, 15] is an efficient algorithm for solving multivariate polynomial equations introduced by Wen-Tsun Wu. It also has succeeded in mechanical geometry theorem proving. For further details and elementary introduction, we refer the reader to [16].LetPi=k[x1,…,xi] denote the polynomial ring in variables x1,x2,…,xi with coefficient k, for every i in the range {1,…,n}, and k is an algebraically closed field.In what follows, without loss of generality, we assume that the given variables ordering is fixed as(7)x1≺x2≺⋯≺xn.
Assume p∈k[x1,…,xn] and let deg(p,xi) be the maximum degree of p with respect to xi.Definition 7.
Letp∈Pi; the greatest variable v∈{x1,…,xi} is called the main variable of p such that deg(p,v)≠0, denoted by mvar(p). The biggest index i is called the class, denoted by class(p). If we assume p as a univariate polynomial with mvar(p)=xi, we can write p=cxid+r, where d=deg(p,xi). In this case, c and d are, respectively, the initial and the main degree and are denoted by init(p) and mdeg(p).Definition 8 (pseudo division).
For any two polynomialsf,g∈Pi, with class(f)=j. There exist a nonnegative number α and polynomials q and r, such that init(f)αg=qf+r. Where r is denoted by prem(g,f,xj). We denote the remainder r on pseudo division (pseudo remainder) of f by g with respect to the variable y by prem(f,g,y).Definition 9 (Wu’s characteristic set).
LetPS and CS be two polynomial system, and CS is a triangular set; a triangular set is called a characteristic set of PS if
(8)∀p∈PS,prem(p,CS)=0.Theorem 10 (zero decomposition theorem).
LetZero(PS) denote the zero set of PS and CS be a characteristic set of P; then
(9)Zero(PS)=Zero(CSinit(CS))∪Zero(PSi),
where PSi=PS∪init(CS)i.Now we briefly outline the essential steps about Wu’s method on geometry theorem proving [17].(
1
) Algebraize a geometric theorem by converting it into a system of algebraic equations. We will translate the theorem’s hypotheses into a set of hypotheses equations {f1,…,fr},
(10)f1=f1(x1,…,xn),f2=f2(x1,…,xn),⋮fr=fr(x1,…,xn),
and the theorem’s conclusion into a polynomial g(x1,…,xn).(
2
) Triangulize the system of hypotheses equations using pseudo-division. Then we will obtain the hypothesis equations denoted as
(11)f1=f1(u1,…,ud,x1),f2=f2(u1,…,ud,x1,x2),⋮fr=fr(u1,…,ud,x1,…,xr).(
3
) Perform successive pseudo division on the transformed hypotheses in triangular form {f1,f2,…,fr} by the conclusion equation g(x1,…,xn), yielding a final remainder r0:
(12)r0=prem(⋯prem(g,fr,xpr),…,f1,xp1).
If this final remainder r0≡0, we will say that the conclusion g follows from the hypotheses {f1,…,fr}.As mentioned above, the characteristic set of a polynomial system is a special triangular form. We can use the characteristic set of hypotheses equations as the triangular form, denoted bycharset(f1,…,fr). Roughly speaking, the soul of Wu’s method on theorem proving is to check whether the zero set of the expected consequent equations includes the zero set of hypotheses equations or not.Our checking method is based on algebraic geometry that studies of geometric objects arising as the common zeros of collections of polynomials. The aim is to find polynomials whose zeros correspond to pairs of states in which the appropriate assignments are made.Letzero(PC) and zero(PS) denote the zero set for circuit polynomial set PC and assertions polynomial set PS respectively. Let C⊨s denote that assertion s holds under model C.We aim to attempt to determine whether assertions holds or not. Therefore, we have
(13)(s⊨C)⟺Zero(PC)⊆Zero(PS).Theorem 11.
Suppose thatG=[𝒜⇒𝒞] is a property, 𝒜 is the precondition of 𝒞, and M is a system model. Let PA and PM be the polynomial set representations for 𝒜 and M, respectively, constructed by previous mentioned rules. PC is the polynomial set representation for 𝒞.
LetH=A∪M, PH=PA∪PM={h1,h2,…,hs}⊆k[x1,…,xn], CS=charset(PH); charset(PH) denotes the characteristic set of PH, and prem(PC,CS) is the function which computs the remainder by successive pseudo division; then we have
(14)prem(PC,CS)==0⟺(M∣=G).Proof.
Firstly, letzero(PA) and zero(PM) denote the zero sets for circuit polynomial set 𝒜 and assertions polynomial set M, respectively. Since PH=PA∪PM={h1,h2,…,hs}⊆k[x1,…,xn], let zero(PH) denote the zero sets for zero(PA∪PM={h1,h2,…,hs}). Let H⊨C denote that the assertion C holds under model H.
Our aim is to attempt to determine whether assertionC holds or not. Thus, we have
(15)(M⊨G)⟺(H⊨C)⟺zero(PH)⊆zero(PC).
As mentioned previously, Wu’s method can be used to determine the inclusion relationship of zero sets. Thus we have
(16)prem(PC,charset(PH))==0⟺zero(PH)⊆zero(PC).
LetCS=charset(PH), which denotes the characteristic set of PH; according to (15) and (16), we have
(17)(prem(PC,CS)==0)⟺(M∣=G).
This establishes the theorem.


## 6.2. Checking Algorithm

From above discussion, we have the following core decision algorithm.Algorithm 12 (Assertion Checking:AssChk(M,G)).
Input: Circuit model M, an assertion G=[𝒜⇒𝒞];
Output: Boolean: true or false;
BEGIN
/* Step 0: initialize input signals via testbench */
00InitSignals();
01M=∅;PSA=∅;H=∅;PSC=∅;
/* Step 1: build polynomial set for antecedent𝒜 */
02PS𝒜=BuildPS(𝒜);
/* Step 2: build polynomial set for consequent𝒞 */
03PS𝒞=BuildPS(𝒞);
/*Step 3: calculate thePS𝒜∪M */
04H=PS𝒜∪M;
/*Step 4: calculate the characteristic set ofH */
05CS:=Charset(H);
/*Step 5: check the final remainder by successive pseudo-division */
06 if(prem(PS𝒞,CS)≠0){
07 returnfalse;
}
08 returntrue; /* Assertion does hold */
END


## 7. Case Study and Experiment

In this section, we will firstly study a simple circuit to show how the SVA properties are verified by polynomial representations and characteristic set computation-based approaches. We then show a scalable experiment with the classic synchronous arbiter circuit to evaluate the performance of our approach.


### 7.1. Circuit and Assertion Modeling

As an example, consider the synchronous circuit in Figure2, whose polynomial set can be constructed as follows:
(18)Setadder={f1={m3′-(1-m1)},f2={m2′-m3},f3={m1′-m2},f4={m4-(1-m1)*m3},f5={m5-(1-m3)*(1-m2)},f6={m6-m1*m2}}.Figure 2
A 3-stage johnson counter.Throughout this paper, an internal variable namem[i] refers to the corresponding signal m in the original circuit, and the subscript denotes the time-frame i (or the ith clock cycle). For convenient, variable m′ (i.e., m[i+1]) denotes the next state of m (m[i]) by omitting time-frame i.To illustrate the problem clearly, we define polynomial set representationPM[i] for the ith time frame as follows:
(19)⟦PM[i]⟧={f1[i],f2[i],f3[i],f4[i],f5[i],f6[i]}.Assume 8 cycles are needed to check; therefore, we then have the model representation:⟦PM⟧=⋃i=08⟦PM[i]⟧.For any boolean variable, we must add an extra constraint polynomial: for alla,𝒱(a)∈{0,1}:{a*a-a}.The circuit produces 3-phase nonoverlapping outputs, which can decode the overlapping outputsv1, v2, and v3 to nonoverlapping outputs A, B, and C as shown in Figure 3.Figure 3
A 3-stage johnson counter waveform.Assume the initial values of the registersA, B, and C are all 0, they will be {1,0,0}, respectively, after 1 cycle running and {1,1,0} after 2 cycles. This property can be specified by the following SVA assertions:propertyPA;(m3=0&&m2=0&&m1=0)|=>##1(m3==1&&m2==0&&m1==0)|=>##1(m3==1&&m2==1&&m1==0)|=>##1(m3==1&&m2==1&&m1==1);endpropertypropertyPB;m6|=>##2m5∣=>##2m4;endpropertypropertyPC;m5##!m5|=>##[1:3]!m5;endpropertyAfterward, we will demonstrate the verification process step by step.


### 7.2. Assertion Checking Using MMP

We ran this example by using MMP [18] (Mathematics Mechanization Platform). MMP is a group of symbolic computation and automated theorem proving softwares based on Wu’s Method. Before running, we manually translated all models into polynomials for this example.In this paper, all experiments are conducted on a PC with an intel 2.40 GHz CPU (intel i5 M450) and 1024 MB of memory.As shown in MMP outputs, the given circuit has been modeled as polynomial setCM (its characteristic set is denoted by cs), and the assertion results as (m3[2]-1). The checking process is listed below:[>CM:=[⋯];/*{f1[i],f2[i],f3[i],f4[i],f5[i],f6[i]} Circuit Model */[>vars:=(m1[0],m2[0],m3[0],m4[0],m5[0],m6[0],m1[1],m2[1],m3[1],m4[1],m5[1],m6[1],m1[2],m2[2],m3[2],m4[2],m5[2],m6[2],…[>cs:=charset(CM,vars);[>c1:=(m3[2]-1);[>ret:=premas(c1,cs,vars)=0From the running result, the return value ofret is 0 which means cs can be pseudo divided with no remainder by (m3[2]-1). Similarly, the expected polynomials (m2[2]-1) and (m1[2]) both return 0. Thus, from the previously mentioned verification principles, it is easy to conclude that the assertion holds under this circuit model after 2 cycles.The example took about 0.07 seconds and 810 KB of memory when applying Wu’s method in MMP environment. This case can be a fairly complete illustration of how the checking algorithm works.


### 7.3. Experiment with Classic Arbiter Circuit

The synchronous arbiter circuit [19], depicted in Figure 4, is one of the most popular test cases of model checkers. We also test our approach with this circuit currently to illustrate the performance of our approach. The convert algorithm which can automatically translate the circuit netlist into polynomial set has been implemented in C++.Figure 4
Chain of synchronous arbiter circuit.This arbiter circuit is used to grant access on each clock cycle to a single client among a number of clients contending for the use of common resources.Here, we briefly explain how the arbiter works. For more detailed information regards to the arbiter, please refer to [19]. The basic part of the arbiter is the colored cell which is repeated k times to form a round robin chain. Each cell has a request input reqi (1≤i≤k, here, k denotes the number of client) and an acknowledge output acki. The grant output of cell i is passed to cell i and indicates that no clients of index less than or equal to i are requesting. Hence a cell i may assert its acknowledge output acki if its grant input gii is asserted. Each cell has a register T which stores one when the token is present. The T registers form a circular shift register which shifts up one place each clock cycle.Each cell also has a registerW for waiting which is set to one when the request input is asserted and the token is present.The register remains set while the request persists until the token returns. At this time the cell’s overrideooi and acknowledge outputs acki are assertedFor clarity, we use the first subscript of a variable name which denotes the cell numberj and the second subscript which denotes the current time-frame i in this example.The corresponding polynomial set for each cellj(0≤j≤k-1) and time-frame i(1≤i≤n) can then be constructed as follows:
(20)f1:{w[j][i]+t[j][i]-w[j][i]*t[j][i]-m1[j][i]}f2:{m2[j][i]*req[j][i]-m2[j][i]}f3:{w[j][i]′-m2[j][i]}f4:{t[j][i]′-ti[j][i]}f5:{m3[j][i]-t[j][i]*w[j][i]}f6:{m3[j][i]+oi[j][i]-m3[j][i]*oi[j][i]-oo[j][i]}f7:{go[j][i]-(1-req[j][i])*oo[j][i]}f8:{gi[j][i]+m3[j][i]-gi[j][i]*m3[j][i]-m4[j][i]}f9:{ack[j][i]-m4[j][i]*req[j][i]}.Additionally, the chain relation between cells can be modeled as below:(21)l1:{go[j][i]-gi[j+1][i]}l2:{oi[j][i]-oo[j+1][i]}l3:{to[j][i]-ti[j+1][i]}l4:{to[k-1][i]-ti[0][i]}l5:{oo[0][i]-gi[o][i]}.The desired properties of the arbiter circuits can be described as follows:(1)
no two acknowledge outputs are asserted simultaneously,(2)
every persistent request is eventually acknowledged,(3)
acknowledgment is not asserted without request.In the following description, if clear from the context, the time-frame index will be omitted for convenience. Note thats,t(0≤s,t≤k-1) and ack[s],ack[t]∈{0,1}. Intuitively, properties expressed in CTL can be listed as follows:(1)
⋀s≠tAG¬(ack[s]∧ack[t]),(2)
⋀sAGAF(req[s]⇒ack[s]),(3)
⋀sAG(ack[s]∧req[s]).Note that the arbiter can handle the access ofn clients to a common resource. If a client asserts a request, the client will wait at most 2n clock cycles before it is served. Therefore, in our test, it is sufficient to verify the properties that the circuit is unrolled 2n time frames.Evidently, these properties can be equivalently expressed in SVA codes. In [7], the authors have provided a detailed assertion description for the case that client number is 3.In this example, we will follow their idea and explain how to translate them into algebraic polynomials as below:(22)⋀s≠tAG¬(ack[s]∧ack[t])⟺ack[0]+⋯+ack[s]+⋯+ack[k-1]=1or0⟺{ack[0]+⋯+ack[s]+⋯+ack[k-1]-1}or{ack[0]+⋯+ack[s]+⋯+ack[k-1]}.Let𝒞1={ack[0]+⋯+ack[s]+…+ack[k-1]-1} and 𝒞2={ack[0]+⋯+ack[s]+…+ack[k-1]}. The polynomial representation of consequent can then be formulated as 𝒞=𝒞1∨𝒞2.AssumeG=[𝒜⇒𝒞] and let G1=[𝒜⇒𝒞1] and G2=[𝒜⇒𝒞2]. If G1∨G2 holds, then G holds.Similarly, the precondition of this property is that only one single token is present in this circuit chain. We have the polynomial representation of antecedent:{t[0]+⋯+t[s]+⋯+t[k-1]-1} (t[i]∈{0,1}).More specifically, if the subscript for time frame is considered, we can define𝒞[k][n]:=⋀j=0k-1{(∑i=0n-1ack[j][i]-1)∨(∑i=0n-1ack[j][i])} and 𝒜[k][n]:=⋀j=0k-1{(∑i=0n-1t[j][i]-1)}; here, n denotes the number of time frames and k denotes the number of cells.In this experiment, we also tested the circuit with an artificial error that an “AND” gate is replaced by an “OR” gate by mistake, as shown in Figure 4. We mainly demonstrate whether or not our method is able to find bugs. The corresponding polynomial set model can be updated by replacing f7 with {go[j][i]+req[j][i]*oo[j][i]-req[j][i]-oo[j][i]}.Consequently, in our test with 3 cells, it took only 9.37 MB of memory and 10.5 seconds to find the resultret≠0 which means the circuit did not meet the required property. Then we concluded that there must be some design errors in the circuit.More detailed experimental results concerning polynomials and variables for safety property verification of the circuit are listed in Figure5.Figure 5
Polynomials and variables for safety property checking.


### 7.4. Discussion

So far, several methodologies are developed to address the verification problem. In this section, we will discuss these methods by the arbiter example shown in Figure4.(
1
) In [19], a BDD-based model checking is proposed. The performance of this method is fairly promising. The size of the transition relation increases linearly as the number of cells. But the OBDD representing the set of states grows exponentially in the number of cells. The performance of BDD-based symbolic model checking procedure is plotted in Figure 6. For more detailed information about this test case, please refer to [19].Performance-synchronous arbiter example.
(a)
(b)(
2
) Due to advances in SAT-solving techniques [20], SAT-based bounded model checking (for short, BMC) can often handle much larger designs than BDDs. In [7], the authors presented a SAT-based BMC to verify the arbiter circuit. They found that the size of the instance for the safety property is proportional to the number of arbiter clients and the liveness property has quadratic size.(
3
) In our method, the worst case complexity of our symbolic algebraic method checking is very high due to intermediate expression swell. As shown in Figure 5, the number of polynomials to be generated for liveness property checking has quadratic size of the number of cells k as well as the number of variables. Currently, from the runtime consumed, the SAT solver still shows better performance than our method. Fortunately, a great deal of optimization techniques can be applied to improve the performance.As an example, we will explain how to apply variable projection technique to optimize the calculating process. Assume the given circuit has been modeled as polynomial setCM and variable order list is tord (its projection for the zero set on pord⊆tord is denoted by PC). We will firstly calculate the projection to eliminate the unnecessary elements:
(23)PC=proj(CircuitModel,[],ord,pord,"alg")
and then the zero set: wsolve(PC,ord). Correspondingly, the performance will be improved greatly.


## 7.1. Circuit and Assertion Modeling

As an example, consider the synchronous circuit in Figure2, whose polynomial set can be constructed as follows:
(18)Setadder={f1={m3′-(1-m1)},f2={m2′-m3},f3={m1′-m2},f4={m4-(1-m1)*m3},f5={m5-(1-m3)*(1-m2)},f6={m6-m1*m2}}.Figure 2
A 3-stage johnson counter.Throughout this paper, an internal variable namem[i] refers to the corresponding signal m in the original circuit, and the subscript denotes the time-frame i (or the ith clock cycle). For convenient, variable m′ (i.e., m[i+1]) denotes the next state of m (m[i]) by omitting time-frame i.To illustrate the problem clearly, we define polynomial set representationPM[i] for the ith time frame as follows:
(19)⟦PM[i]⟧={f1[i],f2[i],f3[i],f4[i],f5[i],f6[i]}.Assume 8 cycles are needed to check; therefore, we then have the model representation:⟦PM⟧=⋃i=08⟦PM[i]⟧.For any boolean variable, we must add an extra constraint polynomial: for alla,𝒱(a)∈{0,1}:{a*a-a}.The circuit produces 3-phase nonoverlapping outputs, which can decode the overlapping outputsv1, v2, and v3 to nonoverlapping outputs A, B, and C as shown in Figure 3.Figure 3
A 3-stage johnson counter waveform.Assume the initial values of the registersA, B, and C are all 0, they will be {1,0,0}, respectively, after 1 cycle running and {1,1,0} after 2 cycles. This property can be specified by the following SVA assertions:propertyPA;(m3=0&&m2=0&&m1=0)|=>##1(m3==1&&m2==0&&m1==0)|=>##1(m3==1&&m2==1&&m1==0)|=>##1(m3==1&&m2==1&&m1==1);endpropertypropertyPB;m6|=>##2m5∣=>##2m4;endpropertypropertyPC;m5##!m5|=>##[1:3]!m5;endpropertyAfterward, we will demonstrate the verification process step by step.


## 7.2. Assertion Checking Using MMP

We ran this example by using MMP [18] (Mathematics Mechanization Platform). MMP is a group of symbolic computation and automated theorem proving softwares based on Wu’s Method. Before running, we manually translated all models into polynomials for this example.In this paper, all experiments are conducted on a PC with an intel 2.40 GHz CPU (intel i5 M450) and 1024 MB of memory.As shown in MMP outputs, the given circuit has been modeled as polynomial setCM (its characteristic set is denoted by cs), and the assertion results as (m3[2]-1). The checking process is listed below:[>CM:=[⋯];/*{f1[i],f2[i],f3[i],f4[i],f5[i],f6[i]} Circuit Model */[>vars:=(m1[0],m2[0],m3[0],m4[0],m5[0],m6[0],m1[1],m2[1],m3[1],m4[1],m5[1],m6[1],m1[2],m2[2],m3[2],m4[2],m5[2],m6[2],…[>cs:=charset(CM,vars);[>c1:=(m3[2]-1);[>ret:=premas(c1,cs,vars)=0From the running result, the return value ofret is 0 which means cs can be pseudo divided with no remainder by (m3[2]-1). Similarly, the expected polynomials (m2[2]-1) and (m1[2]) both return 0. Thus, from the previously mentioned verification principles, it is easy to conclude that the assertion holds under this circuit model after 2 cycles.The example took about 0.07 seconds and 810 KB of memory when applying Wu’s method in MMP environment. This case can be a fairly complete illustration of how the checking algorithm works.


## 7.3. Experiment with Classic Arbiter Circuit

The synchronous arbiter circuit [19], depicted in Figure 4, is one of the most popular test cases of model checkers. We also test our approach with this circuit currently to illustrate the performance of our approach. The convert algorithm which can automatically translate the circuit netlist into polynomial set has been implemented in C++.Figure 4
Chain of synchronous arbiter circuit.This arbiter circuit is used to grant access on each clock cycle to a single client among a number of clients contending for the use of common resources.Here, we briefly explain how the arbiter works. For more detailed information regards to the arbiter, please refer to [19]. The basic part of the arbiter is the colored cell which is repeated k times to form a round robin chain. Each cell has a request input reqi (1≤i≤k, here, k denotes the number of client) and an acknowledge output acki. The grant output of cell i is passed to cell i and indicates that no clients of index less than or equal to i are requesting. Hence a cell i may assert its acknowledge output acki if its grant input gii is asserted. Each cell has a register T which stores one when the token is present. The T registers form a circular shift register which shifts up one place each clock cycle.Each cell also has a registerW for waiting which is set to one when the request input is asserted and the token is present.The register remains set while the request persists until the token returns. At this time the cell’s overrideooi and acknowledge outputs acki are assertedFor clarity, we use the first subscript of a variable name which denotes the cell numberj and the second subscript which denotes the current time-frame i in this example.The corresponding polynomial set for each cellj(0≤j≤k-1) and time-frame i(1≤i≤n) can then be constructed as follows:
(20)f1:{w[j][i]+t[j][i]-w[j][i]*t[j][i]-m1[j][i]}f2:{m2[j][i]*req[j][i]-m2[j][i]}f3:{w[j][i]′-m2[j][i]}f4:{t[j][i]′-ti[j][i]}f5:{m3[j][i]-t[j][i]*w[j][i]}f6:{m3[j][i]+oi[j][i]-m3[j][i]*oi[j][i]-oo[j][i]}f7:{go[j][i]-(1-req[j][i])*oo[j][i]}f8:{gi[j][i]+m3[j][i]-gi[j][i]*m3[j][i]-m4[j][i]}f9:{ack[j][i]-m4[j][i]*req[j][i]}.Additionally, the chain relation between cells can be modeled as below:(21)l1:{go[j][i]-gi[j+1][i]}l2:{oi[j][i]-oo[j+1][i]}l3:{to[j][i]-ti[j+1][i]}l4:{to[k-1][i]-ti[0][i]}l5:{oo[0][i]-gi[o][i]}.The desired properties of the arbiter circuits can be described as follows:(1)
no two acknowledge outputs are asserted simultaneously,(2)
every persistent request is eventually acknowledged,(3)
acknowledgment is not asserted without request.In the following description, if clear from the context, the time-frame index will be omitted for convenience. Note thats,t(0≤s,t≤k-1) and ack[s],ack[t]∈{0,1}. Intuitively, properties expressed in CTL can be listed as follows:(1)
⋀s≠tAG¬(ack[s]∧ack[t]),(2)
⋀sAGAF(req[s]⇒ack[s]),(3)
⋀sAG(ack[s]∧req[s]).Note that the arbiter can handle the access ofn clients to a common resource. If a client asserts a request, the client will wait at most 2n clock cycles before it is served. Therefore, in our test, it is sufficient to verify the properties that the circuit is unrolled 2n time frames.Evidently, these properties can be equivalently expressed in SVA codes. In [7], the authors have provided a detailed assertion description for the case that client number is 3.In this example, we will follow their idea and explain how to translate them into algebraic polynomials as below:(22)⋀s≠tAG¬(ack[s]∧ack[t])⟺ack[0]+⋯+ack[s]+⋯+ack[k-1]=1or0⟺{ack[0]+⋯+ack[s]+⋯+ack[k-1]-1}or{ack[0]+⋯+ack[s]+⋯+ack[k-1]}.Let𝒞1={ack[0]+⋯+ack[s]+…+ack[k-1]-1} and 𝒞2={ack[0]+⋯+ack[s]+…+ack[k-1]}. The polynomial representation of consequent can then be formulated as 𝒞=𝒞1∨𝒞2.AssumeG=[𝒜⇒𝒞] and let G1=[𝒜⇒𝒞1] and G2=[𝒜⇒𝒞2]. If G1∨G2 holds, then G holds.Similarly, the precondition of this property is that only one single token is present in this circuit chain. We have the polynomial representation of antecedent:{t[0]+⋯+t[s]+⋯+t[k-1]-1} (t[i]∈{0,1}).More specifically, if the subscript for time frame is considered, we can define𝒞[k][n]:=⋀j=0k-1{(∑i=0n-1ack[j][i]-1)∨(∑i=0n-1ack[j][i])} and 𝒜[k][n]:=⋀j=0k-1{(∑i=0n-1t[j][i]-1)}; here, n denotes the number of time frames and k denotes the number of cells.In this experiment, we also tested the circuit with an artificial error that an “AND” gate is replaced by an “OR” gate by mistake, as shown in Figure 4. We mainly demonstrate whether or not our method is able to find bugs. The corresponding polynomial set model can be updated by replacing f7 with {go[j][i]+req[j][i]*oo[j][i]-req[j][i]-oo[j][i]}.Consequently, in our test with 3 cells, it took only 9.37 MB of memory and 10.5 seconds to find the resultret≠0 which means the circuit did not meet the required property. Then we concluded that there must be some design errors in the circuit.More detailed experimental results concerning polynomials and variables for safety property verification of the circuit are listed in Figure5.Figure 5
Polynomials and variables for safety property checking.


## 7.4. Discussion

So far, several methodologies are developed to address the verification problem. In this section, we will discuss these methods by the arbiter example shown in Figure4.(
1
) In [19], a BDD-based model checking is proposed. The performance of this method is fairly promising. The size of the transition relation increases linearly as the number of cells. But the OBDD representing the set of states grows exponentially in the number of cells. The performance of BDD-based symbolic model checking procedure is plotted in Figure 6. For more detailed information about this test case, please refer to [19].Performance-synchronous arbiter example.
(a)
(b)(
2
) Due to advances in SAT-solving techniques [20], SAT-based bounded model checking (for short, BMC) can often handle much larger designs than BDDs. In [7], the authors presented a SAT-based BMC to verify the arbiter circuit. They found that the size of the instance for the safety property is proportional to the number of arbiter clients and the liveness property has quadratic size.(
3
) In our method, the worst case complexity of our symbolic algebraic method checking is very high due to intermediate expression swell. As shown in Figure 5, the number of polynomials to be generated for liveness property checking has quadratic size of the number of cells k as well as the number of variables. Currently, from the runtime consumed, the SAT solver still shows better performance than our method. Fortunately, a great deal of optimization techniques can be applied to improve the performance.As an example, we will explain how to apply variable projection technique to optimize the calculating process. Assume the given circuit has been modeled as polynomial setCM and variable order list is tord (its projection for the zero set on pord⊆tord is denoted by PC). We will firstly calculate the projection to eliminate the unnecessary elements:
(23)PC=proj(CircuitModel,[],ord,pord,"alg")
and then the zero set: wsolve(PC,ord). Correspondingly, the performance will be improved greatly.


## 8. Conclusion

In this paper, we presented Wu’s method-based verification approach for SVA properties checking.Our approach is based on polynomial models construction for both circuit models and SVA assertions. This method is to eventually translate a simulation-based verification problem into a pure algebraic zero set determination problem by a series of proposed steps, which can be performed on MMP environment. For synchronous sequential circuits, we adapted a parameterized polynomial set modeling method based on time-frame expansion. We also defined a constrained subset of SVAs which is powerful enough for practical purpose and proposed a practical algebraization method for each sequence and property operator of this subset. This method allows users to deal with more than one state and many input combinations every cycle due to symbolic simulation. The advantage comes directly from the fact that many vectors are simulated at once using symbolic value.Basically, our approach may provide a useful supplement to existing methods based on OBDD or SAT and may also provide important theoretical insights by allowing the application of important results in symbolic computation to the assertion checking problems. We plan to extend the work presented in several directions.(
1
) We plan to optimize the solver based on Wu’s method. As we know, Wu’s method-based mathematics mechanization platform is a powerful computation environment for general purpose. On the one hand, we will apply variables projection and other mathematics approaches to improve the effectiveness of this algorithm. On the other hand, we also plan to implement our core steps by using the programming language in MMP.(
2
) In this paper, we only test some classic cases mentioned in previous papers to illustrated the feasibility of our method currently. In the future, we plan to test the benchmarks from ISCAS’89 and ISCAS’85 and other industrial examples to provide a comprehensive evaluation of our approach and compare to the state-of-the-art where circuits with several thousands of gates and dozens of input signals.(
3
) In this paper, we only concentrated our attention on the basic assertion checking algorithm, but the other important features such as counterexample generation were not discussed. We will also work on those issues in the future.Furthermore, in the field of symbolic computation, there is a rich collection of solutions to solving polynomials, methods for inclusion of zero sets, and so forth. We are interested in applying some of the useful results and methods to verification area.



---

*Source: 740194-2013-06-16.xml*