Abstract
This paper presents an original method to compare two synchronous sequential machines. The method consists in a breadth first traversal of the product machine during which symbolic expressions of its observable behaviour are computed. The method uses formal manipulations on boolean functions to avoid the state enumeration and diagram construction. For this purpose, new algorithms on boolean functions represented by Typed Decision Graphs has been defined.
Chapter PDF
Similar content being viewed by others
References
F. Anceau, "Design Methodology for Large Custom Processors". Proc. of the 1986 ESSIR Conference, Delft.
J. R. Armstrong, Chip-Level Modeling with VHDL, Prentice Hall, 1989.
J. P. Billon, "Perfect Normal Forms for Discrete Functions", BULL Research Report N o 87019, June 1987.
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.
O. Coudert, J. C. Madre, "Logics over Finite Domain of Interpretation: Proof and Resolution Procedures", BULL Research Report to appear, 1989.
S. Devadas, H. K. Ma, R. Newton, "On the Verification of Sequential Machines at Differing Levels of Abstraction", IEEE Transactions on CAD, Vol. 7, No. 6, 1988.
D. Dietmeyer, Logic Design of Digital Systems, Allyn & Bacon, 2nd edition, 1978.
J. E. Hopcroft, J. D. Ullman, Introduction to Automata Theory, Langages and Computation, Addison-Wesley, Reading, Mass., 1979.
S. H. Hwang, A. R. Newton, "An efficient Design Correctness Checker of Finite State Machines", ICCAD 1987.
D. Jaillet, P. Mertens, LDS Reference Manual, BULL S.A., May 1987.
J. C. Madre, J. P. Billon, "Proving Circuit Correctness using Formal Comparison Between Expected and Extracted Behaviour", Proc. of the 25th Design Automation Conference, 1988.
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, June 1989.
J. Y. Murzin, "FAON A functional Abstractor of Netlist", Actes du Séminaire de Programmation Logique, Lannion, France, 1986.
K. J. Supowit, S. J. Friedman, "A new Method for Verifying Sequential Circuits", Proc. of the 23rd Design Automation Conference, 1986.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1990 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Coudert, O., Berthet, C., Madre, J.C. (1990). Verification of synchronous sequential machines based on symbolic execution. In: Sifakis, J. (eds) Automatic Verification Methods for Finite State Systems. CAV 1989. Lecture Notes in Computer Science, vol 407. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-52148-8_30
Download citation
DOI: https://doi.org/10.1007/3-540-52148-8_30
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-52148-8
Online ISBN: 978-3-540-46905-6
eBook Packages: Springer Book Archive