DocumentCode :
1122278
Title :
Efficient symbolic simulation-based verification using the parametric form of Boolean expressions
Author :
Jain, Prabhat ; Gopalakrishnan, Ganesh
Author_Institution :
Dept. of Comput. Sci., Utah Univ., Salt Lake City, UT, USA
Volume :
13
Issue :
8
fYear :
1994
fDate :
8/1/1994 12:00:00 AM
Firstpage :
1005
Lastpage :
1015
Abstract :
Symbolic simulation has been proposed as a way to formally verify the correct operation of an MOS circuit. By allowing nonground expressions as values, a symbolic simulator avoids the complexity of exhaustive simulation. The symbolic expressions chosen for initializing the state- and input-variables must cover all valid test cases while avoiding those that violate circuit constraints. In this paper, we present a new approach to symbolic simulation-based verification that hinges on the use of parametric forms of Boolean expressions. A parametric form of a Boolean expression E is an equivalent expression in which the variables in E are expressed in terms of expressions over new variables called parametric variables. In our approach, Boolean expressions representing the operating constraints on the circuit node values are first converted into the parametric form, and the resulting parametric expressions are used as initial (symbolic) node values prior to each simulation step. In addition to the proposal to use the parametric form, we make the following additional contributions. We present a new method for generating the parametric form of a Boolean expression that exploits (among other things) the structural recursion involved in defining commonly used arithmetic/relational operators. Our method generates parametric forms that are more compact, as well as more balanced in terms of term-sizes than generated by the following existing methods: Boole´s, Lowenheim´s, and the generalized cofactor method. We have also developed a variety of example-specific techniques to deal with circuit constraints. All algorithms discussed in this paper have been implemented in a verification prototype system. Experimental results obtained using the COSMOS symbolic simulator are also reported
Keywords :
Boolean functions; MOS integrated circuits; circuit analysis computing; symbol manipulation; Boolean expressions; COSMOS symbolic simulator; MOS circuit; algorithms; arithmetic operators; circuit constraints; circuit node; parametric variables; relational operators; structural recursion; symbolic simulation; verification; Circuit simulation; Circuit testing; Computational modeling; Computer science; Fasteners; Formal verification; Hardware; Proposals; Prototypes; Very large scale integration;
fLanguage :
English
Journal_Title :
Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on
Publisher :
ieee
ISSN :
0278-0070
Type :
jour
DOI :
10.1109/43.298036
Filename :
298036
Link To Document :
بازگشت