Efficient symbolic simulation-based verification using the parametric form of Boolean expressions

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