Chapter 3. Proposed Approach
3.9 A More Complete Example of Assertion Checking
In this section, we use a complete example to demonstrate our approach, and explain its process step by step. First at all, as shown in Figure 3.20, there are six assertions in the input.
rtion . For each assertion group, a
Figure 3.19 Verify Assertions with SMV
assert A1 always {@a; @b; @c} => ev
In our approach, we partition the input assertions into assertion groups. According to the partitioning algorithm, the six are assertions are partitioned into two groups, Assertion Group 1 and Assertion Group 2, as Figure 3.21 shows.
mposed into primitive
Figure 3.21 Partitioning Result Figure 3.20 Input of the Example
We take Assertion Group 1 to demonstrate the process. In the step 1, it is deco
quences and temporal operators, and the conversion template is applied according to the decomposed result. It is illustrated in Figure 3.22.
Then at step 2, the primitive DFA are built according to decomposed primitive sequence . At step3, composite DFA is assembled by each primitive DFA and temporal operators. The converted DFA of Assertion Group 1 is depicted in Figure 3.23.
Similarly, assertion A3, assertion A5 and assertion A6 are shown in the Figure 3.24, 3.25 and 3.26 respectively.
Figure 3.23 Converted DFA from Assertion A1
A1: always {@a; @b; @c} => eventually {@x; @y; @z};
Figure 3.22 Decomposed Assertions of Assertion Group 1 y; @z};
Figure 3.24 Converted DFA from Assertion A3
Figure 3.25 Converted DFA from Assertion A5
Figure 3.26 Converted DFA from Assertion A6 A3: never {@b; [2:5]; @x};
At the step 4 and step 5, CTL formula are built and then properties are assembled with them. The onverted properties are illustrated in the following.
After the conversion is done, the converted DFA and properties are fed into SMV for checking. The port is shown in Figure 3.27.
As the Figure 3.27 shows, there are four conflicts found in this assertion group. They are DFA1
gainst Property3, DFA1 against Property5, DFA3 against Property6, and DFA6 against Property3.
ccording to our analysis from the checking results of SMV, where (DFA1,Property3) and
(DFA Property) are unilateral conflict, so they are suspected conflicts alert. That means it could be Property of assertion A1:
SPEC !EF(EG(a=T & EX(b=T & EX(c=T & !AF(x=T & AX(y=T & AX(z=T))))));
Property of assertion A3:
SPEC !EF(b=T & EX(EX(EX(x=T | EX(x=T | EX(x=T | EX(x=T)))))));
Property of assertion A5:SPEC !EF state=Fail;
Property of assertion A6:
SPEC EG((a=T | q=T) -> AX(w=T & AX(w=T & AX(w=T & AX(x=T)))));
Unilateral conflicts, suspected conflicts alerted
Mutual conflicts, definite conflicts reported
Figure 3.27 Checking Result
a A
ind
rtions. The other two, (DFA3, Property6), are m lict. That means they are definite conflicts.
eed conflict or either one of two is redundant. Therefore, users who perform our approach can inspect the result to identify the errors among the asse
utual conf
Chapter 4 Case Study
4.1 Case Description
We choose the assertions for the Bus Transaction Protocol of PCI Local Bus Specification as our case. The assertions cover Bus Transfer Control, Addressing, Byte Lane and Byte Enable, Bus Driving and Turnaround, as well as Transaction Ordering and Posting [26].
In general, the assertions consist of two parts: PCI master and PCI target. There are 41 assertions in this case study.
4.2 Experimental Environment
We implement our approach in C program and some shell scripts. They are executed on Sun Sparc Workstation with 1 GB memory on 400MHz speed.
4.3 Experimental Result
We partition the input assertions into 5 and 4 assertion groups for PCI master and PCI target pectively.
ected conflicts alerted), 1 mutual conflicts, (definite conflicts reported).
The experimental result is depicted on Table. 4.1.
Case No. of
After execution, it found:
4 unilateral conflicts (susp
PCI Master 25 5 2 1 92
PCI Target 16 4 1 0 41
Table 4.1 Experimental Result of Case Study
Chapter 5
Conclusions and Future Works
5.1 ions
We check esign assert by means of converting assertion into
corresponding DFA and pr the others using SMV.
The major features of our approach are:
Without referring the design, only the assertions required, Without need of simulation and test patterns,
Stand-alone, off-line processing, may check assertions prior to design verification, Greatly alleviating the state explosion problem of SMV.
operties and then checking each of them against
Conclus
propose a technique to d ions
5.2 Discussion
Ensuring a set of assertions without any conflict can increase our confidence in the correctness of specification modeling. Not necessary all potential conflicts could be found by using our approach.
onflicts are guaranteed to be definite conflicts. According to our
experience, we found it is hard to detect redundancy of assertions merely by static formal checking
m assertions.
of correlation stimulation of assertions under certain combinations in the input assertions. Under this cumstances, the assertions cannot contribute stimulus correlation to argue against each others. For
rtions in an assertion group illustrated below.
Even and @c), but the two assertions
are b nnot contribute stimulation for each other. It
revea rrelative.
That
Furthermore, the definition of our acceptable input assertion language must be very clear and definite without any ambiguity; otherwise, it tends to induce problem caused by different interpretation the
But all detected mutual assertion c
fro
The most serious hurdle to apply this approach to find out all possible conflicts is lack
cir
example, there are two asse
assert never {@a; @b; @c};
assert never (@a; and @b) or (@a and @c);
the above two assertions share all common variables (@a, @b oth with the same "passive" attribute. So they ca
ls that the ideal input set is the assertions with variety of event attributes and highly co provides enough assertive statement against each others.
of language.
As for the computational complexity, our experiences showed that runtime is acceptable for up to hundreds of input assertions in an assertion group.
In summary, symbolic model checking, in its purest basis at least, is feasible to apply conflict checking for assertion without design model and test patterns. Even it is more difficult than anticipated during the developing process, particularly on coping with versatile combination of input assertions, the
ctions such as Logic Reasoning techniques may be considered to enhance our apability of checking. Next, we will input the simulation results or waveforms to augment the
formation about assertions. By this way, we can clearly identify conflicts and redundancy among idea has been shown conceptually correct and furthermore this approach could be practically implemented for the industrial usage.
5.3 Future Works
Some research dire c
in
assertions and also check assertion violations.
Furthermore, by adding certain converting process, we may convert counterexample of SMV into industrial standard Value Change Dump (VCD) format. That information can help user quickly identify the problem pointed out by SMV.
As for input language, we should accept the full set of common-used language by enlarging the conversion templates for remaining types of that language constructs and enriching the conversion rules for all temporal operators.
A
Grammar of PSL-like Assertion Language
Compilation := Assertion_Collection
ppendices
Appendix A: The BNF
;
Assertion_Collection := Assertion
| Assertion_Collection Assertion ;
Assertion := "assert" Assertion_Name Temporal_Assertion_Kinds ";" ; Assertion_Name := IDENTIFIER ;
Temporal_Assertion_Kinds := Once_Assertion
| Always_Assertion
| Never_Assertion
| Eventually_Assertion ;
Once_Assertion := "once" Temporal_Or_Expression
| "once" Temporal_And_Expression "until" Temporal_And_Expression ;
Always_Assertion := "always" Temporal_Or_Expression
| "always" Temporal_Or_Expression "=>" Temporal_And_Expression
| "always" Temporal_Or_Expression "=>" "eventually" Temporal_And_Expression | "always" Temporal_And_Expression "<=>" Temporal_And_Expression
| "always" Temporal_And_Expression "before" Temporal_And_Expression ; Never_Assertion := "never" Temporal_Or_Expression ;
Eventually_Assertion := "eventually" Temporal_Or_Expression ; Temporal_Or_Expression := Temporal_And_Expression
| Temporal_Or_Expression "or" Temporal_And_Expression ;
| Temporal_And_Expression "and" Temporal_Compound_Expression ; mporal_Compound_Expression := Temporal_Repeat_Expression
Te
| "not" Temporal_Compound_Expression ;
Temporal_Repeat_Expression := Temporal_Primitive
| Repaet_Times Temporal_Repeat_Opt
| Repaet_Times ;
epaet_Times := "[" Repaet_Range"]"
um R
| "[" Repaet_N "]" ; INTLITERAL
Repaet_Range := ":" INTLITERAL ;
epaet_Num := INTLITERAL
R ;
emporal_Repeat_Opt := "*" Temporal_Compound_Expression
T ;
Temporal_Primitive := Event
| "(" Temporal_Or_Expression ")"
| "{" Temporal_Sequence "}" ;
Temporal_Sequence := Temporal_Or_Expression
| Temporal_Sequence ";" Temporal_Or_Expression ; Event := "@" Event_Name ;
Event_Name := "CYC"
| IDENTIFIER ;
IDENTIFIER := Letter(Letter|Digit|_)* ;
TLITERAL := Digit
IN + ;
etter := [A-Za-z] ;
L
Digit := [0-9] ;
Appendix B: Proving of Assertion Conversion
The conversion processing of our approach consists of two parts. One is converting assertion to CTL property. The correctness of this part is comprehensive. Since PSL-like language and CTL property have similar temporal semantics in temporal specification in terms of language feature. The other is converting assertion into DFA. The most crucial part in our approach is assembling the whole DFA with pieces of DFA. Now, we would like to explain its correctness below.
1. A sequence is part of language clause which follows regular expression grammar (RE
grammar).
2. Sequences and sequence operators belong to regular language set.
3. A temporal expression can be decomposed to primitive sequences and operators.
4. By Kleene’s Theorem, each primitive sequence has its corresponding finite automaton.
5. A larger finite automaton can be composed of pieces of small finite automata by applying our
approach which belong to operations of RE grammar.
6. So, the combined larger finite automaton can represent the collection of DFA pieces which are converted from original assertion.
Why assembling a composite DFA from piece sequences in our approach is correct in theory? Let's explain it in more detail. First of all, we may see that the most primitive item operated by our approach is a sequence, which describes single- or multi-cycle behavior built from a series of Boolean
expressions over time. The most atomic is a Boolean expression. In Property Specification Language SL), the sequence named as Sequential Extended Regular Expressions (SEREs)[24], that extends the
is part of the regular lang
concate nion, and repetition which follow regular expression definition.In our approach, we
dec heorem in formal language,
wh utomaton, or
tran o , every
lang
means primitive sequence. This is just what we
do
DFA w the composing rule which belong to regular expression set.
(P
set of regular expression (RE) by definition for some additional temporal operations.
A sequence defined in our language is same as the sequence in PSL except pruning out some non-necessary sequence operations without losing capability for behavior specification. It keeps all our operations applied on sequences belonging to regular expression set.
By definition from formal languages, a sequence of our PSL-like language
uage grammar, which is also a context free grammar. The basic operations in our approach are nation and u
ompose an assertion down to some primitive sequences. By Kleene’s T
ich states that any language which can be defined by regular expression, or finite a siti n graph can be defined by all three methods. It implies the subordinate proposition
uage that can be defined by a regular expression can also be defined by a finite automaton. That we can find a corresponding finite automaton for each
to convert primitive sequence to a piece finite automaton. Then, we assemble the whole composite ith those primitive DFA by applying
So, the composed larger DFA can represent the collection of DFA pieces, and which are converted from the original assertion. Then, we can prove our approach is correct.
Fig. B-1 Proving Our Approach
Bibliography
[1] Thomas Kropf, and Robert Bosch GmbH, “Introduction to Formal Hardware Verification”, Springger-Verlag Berlin Heidelberg, Germany, 1999.
[2] Harry D. Foster, "Property Specification: The Key to an Assertion-Based Verification Platform", Verplex Systems, Inc., 2000.
[3] Harry D. Foster, Adam C. Krolnik, and David J. Lacey, “Assertion-Based Design “ 2nd ed., Kluwer Accademic Publishers, 2004.
[4] Ben Cohen, “Using PSL/Sugar with Verilog and VHDL, Guide to Property Specification Language for ABV”.
[5] Carnegie Mellon University, http://www-2.cs.cmu.edu/~modelcheck/.
[6] ITC-IRST, Trento, Italy; SCS, Carnegie-Mellon University, Pittsburgh, PA, USA; DSI, University of Milano, Milano, Italy, "NuSMV: a new Symbolic Model Verifier",
http://nusmv.irst.itc.it/NuSMV/papers/cav99/html/index.html.
[7] Roberto Cavada, Alessandro Cimatti, Emanuele Olivetti, Gavin Keighren, Marco Pistore and Marco Roveri, "NuSMV v2.2 User Manual", http://nusmv.irst.itc.it/NuSMV/.
[8] Roberto Cavada, Alessandro Cimatti, Gavin Keighren, Emanuele Olivetti, Marco Pistore, and Marco Roveri, "NuSMV 2.2 Tutorial", http://nusmv.irst.itc.it/NuSMV/.
[9] K. L. McMillan, "The SMV language", Cadence Berkeley Labs version of SMV, http://www.cis.ksu.edu/santos/smv-doc/language/language.html.
0] Edmund M. Clarke, Orna Grumberg, and Doron A. Peled, “Model Checking”, The MIT Press,
[11] Model Checking”, Kluwer Academic
[12] Robert C. Koons , “Doxastic Paradox and Reputation Effects in Iterated Games”, Proceedings of the
[13] ong, and Melissa Smartt, “Assertional Checking and Symbolic
ER, January 1979.
tons for Branching Time
[15] oncurrent Systems in CESAR", In
[1
Cambridge, 1999.
Kenneth L. McMillan, Edmund M. Clarke, “Symbolic Publishers, 1993.
4th conference on Theoretical aspects of reasoning about knowledge, March 1992.
J. Mack Adams, James Armstr
Execution: An Effective Combination for Debugging”, Proceedings of the 1979 annual conference,
ACM/CSC-[14] E. M. Clarke and E. A. Emerson, "Synthesis of Synchronization Skele
Temporal Logic", in logic of programs: workshop, Yorktown Heights, NY, May 1981, volume 131 of Lecture Notes in Computer Science.Springer-Verlag, 1981.
J.P. Quielle and J. Sifakis, "Specification and Verification of C
Proceedings of the Fifth International Symposium in Programming, volume 137 of Lecture Notes in Computer Science.Springer-Verlag, 1981.
[16] Thomas Kropf, "Formal Hardware Verification - Methods and Systems in Comparison", Springger-Verlag, Berlin Heidelberg, Germany, 1997.
[17] Accellera Organization, "Property Specification Language Reference Manual", V 2004.
ersion 1.1, June 9,
[19] ., “e Language Reference Manual” V4.3, 2004,
[20] esign Verification with e", Prentice Hall Modern Semiconductor Design Series,
[21]
[23] GNU, "Flex reference Manual", Version 2.5.31, GNU, Free Software Foundation, Inc.,, 27 March
[24]
[25] rd Ed., 2001.
[18] Synopsys, Inc., "OpenVera 1.0 Language Reference Manual Version 1.0", March 2001.
Verisity Design, Inc
(http://www.ieee1647.org/downloads/prelim_e_lib.pdf) Samir Palnitkar, "D
2003.
Charles N. Fischer, Richard J. LeBlanc, Jr., “Crafting A Compiler with C”, 1991.
[22] GNU, "Bison reference Manual", version 1.875, GNU, Free Software Foundation, Inc., 28 December 2002.
2003.
Daniel I. A. Cohen, “Introduction to Computer Theory", 2nd Ed., Oct. 25, 1996.
Peter Linz, "An Introduction to Formal languages and Automata", 3
[26] PCI Special Interest Group, "PCI Local Bus Specification", Revision 2.3, 1998.
Vita
ia-Yua
Ch n Uang receiverd the B.S. degree in electronics engineering from National Taiwan Institute
T aboratories
(C with Maojet Technology Corp.
from 1 tion, RTL synthesis, and timing analysis.
echnology. From 1989 to 1996, he worked for Computer and Communications Research L CL) of Industrial Technology Research Institute (ITRI). He has worked
996 to date. His major experiences are on design verifica