A symbolic simulation-based verification system for synchronous circuits

technical reportThis thesis addresses the issues related to the symbolic simulation-based verification of synchronous circuits. A prototype verification system, based on a two-level verification approach for synchronous circuits, has been implemented that embodies the ideas of parametric Boolean expressions for efficient symbolic simulation-based verification. The specification for the verification of a circuit consists of a collection of state transitions or transition sequences. This specification is used to derive the constraints on the state and input variables of the circuit. The constraint expressions can involve Boolean operations (e.g., -, |, ), relational operators (e.g.,<, ≥, ≠), arithmetic operations (+, âˆ'), and logical connectives (∧, ∨). The solution for these constraints is obtained in the form of parametric Boolean expressions. Some new algorithms based on hierarchical constraint solving approach have been developed and implemented to generate parametric Boolean expressions from the given constraints. These new algorithms have been compared against other known methods, namely, Boole's aud Löwenheim's method, and it has been found that the new algorithms perform significantly better than the other two methods in terms of the sizes of the parametric Boolean expressions generated for the given constraints and the symbolic simulation and verification time with the generated parametric Boolean expressions. The algorithms required to automate the generation of symbolic simulation vectors have been implemented in the C programming language, along with the binary decision diagram (BDD) package. It has been observed, based on the verification of a variety of example circuits, that the technique of using parametric Boolean expressions vastly reduces the number of symbolic simulation vectors and the time for verification