Chapter 5 Conclusions and Future Works
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