Formal boolean manipulations for the verification of sequential machines

ABSTRACT

This paper addresses the problem of verifying synchronous sequential machines. It first shows that there is a certain class of temporal properties that can be verified by proving two sequential machines equivalent. It then explains that the equivalence of two sequential machines can be checked without building any state diagram. It is sufficient to observe all the valid states of a machine, which can be done by traversing its state diagram. It finally presents the symbolic manipulations used to perform the traversal of a state diagram in a more efficient than the usual traversal technique based on enumeration.

REFERENCES

• 1: James R. Armstrong, Chip-level modeling with VHDL, Prentice-Hall, Inc., Upper Saddle River, NJ, 1988
• 2: J. P. Billon, "Perfect Normal Forms for Discrete Functions", BULL Research Report No 87019, June 1987.
• 3: J. P. Billon, J. C. Madre, "Original Concepts of PRIAM, an Industrial Tool for Efficient Formal Verification of Combinational Circuits", in The Fusion of Hardware Design and Verification, G. J. Milne Editor, North Holland, 1988.
• 4: S. Bose, A. Fisher, "Automatic Verification of Synchronous Circuits Using Symbolic Logic Simulation and Temporal Logic", IFIP International Workshop, Applied Formal Methods for Correct VLSI Design, Leuven, November 1989.
• 5: E. M. Clarke, O. Grumbreg, "Research on Automatic Verification of Finite-State Concurrent Systems", Annual Revue Computing Science, vol. 2, pp 269--290, 1987.
• 6: O. Coudert, C. Berthet, J. C. Madre, "Verification of Sequential Machines Using Boolean Functional Vectors", IFIP International Workshop, Applied Formal Methods for Correct VLSI Design, Leuven, November 1989.
• 7: S. Devadas, H. K. Ma, and R. Newton, "On the Verification of Sequential Machines at Differing Levels of Abstraction", IEEE Transactions on CAD, Vol. 7, No. 6, June 1988.
• 8: G. J. Holtzman, "Algorithms for Automated Protocol Validation", Proc: Workshop on Automatic Verification Methods for Finite State Systems, Grenoble, June 1989.
• 9: Z. Kovahi, Switching and Finite Automata Theory, McGraw-Hill Book Edition, 1978.
• 10: J. C. Madre, O. Coudert, "Formal Verification of Digital Circuits Using a Propositional Theorem Prover", IFIP Working Conference on the CAD Systems Using AI Techniques, Tokyo, June 1989.
• 11: J. P. Queille, J. Sifakis, "Faimess and Related Properties in Transition Systems", Acta Informatica, 19, pp 195--220, 1983.