|
Published Articles >> Table of Contents >> Abstract
April/June 1992 (Vol. 9, No. 2)
pp. 42-56
Formal Verification of VHDL Descriptions in the Prevail Environment
Dominique D. Borrione
Laurence V. Pierre
Ashrak M. Salem
Full Article Text:
  
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/54.143145
Send link to a friend
| Abstract |
|
Prevail, a formal verification environment for proving the equivalence of two very-high-speed integrated circuit hardware description language (VHDL) design architectures, is described. For simple bit-level combinational descriptions, the environment calls upon a tautology checker. For parameterized repetitive structures and for more abstract sequential designs, the program translates descriptions into recursive functions according to predefined templates and generates a theorem acceptable to the Bover-Moore theorem prover. The specification, implementation, and functional representation of a sequential example are presented.
|
 References
|
[1] J.C. Madre and J.P. Billon, "Proving Circuit Correctness Using Formal Comparison Between Expected and Extracted Behavior,"Proc. 25th Design Automation Conf., IEEE Computer Society Press, Los Alamitos, Calif., June 1988, pp. 205-210.
[2] R. E. Bryant, "Graph-based algorithms for Boolean function manipulation,"IEEE Trans. Comput., vol. C-35, no. 8, pp. 677-691, Aug. 1986.
[3] O. Coudert, C. Berthet, and J. C. Madre, "Verification of synchronous sequential machines based on symbolic execution," inInternational Workshop on Automatic Verification Methods for Finite State Systems, LNCS 407. New York: Springer Verlag, 1989.
[4] J.R. Burch et al., "Sequential Circuit Verification Using Symbolic Model Checking,"Proc. 27th Design Automation Conf., IEEE CS Press, 1990, pp. 46-51.
[5] M. Gordon, "The Denotational Semantics of Sequential Machines,"Information Processing Letters, Vol. 10, No. 1, Feb. 1980, pp. 1-3.
[6] W.A. Hunt, "FM8501: A Verified Micropro cessor," Tech. Report 47, Institute for Computing Science, Univ. of Texas, Austin, Feb. 1986.
[7] S.D. Johnson,Synthesis of Digital Designs From Recursion Equations, MIT Press, Cambridge, Mass., 1984.
[8] G. Kahn, "The Semantics of a Simple Language for Parallel Programming,"Proc. IFIP Congress, Amsterdam, 1974, pp. 993-998.
[9] M. Gordon, "Why Higher Order Logic Is a Good Formalism for Specifying and Verifying Hardware,"Proc. Edinburgh Workshop Formal Aspects of VLSI Design, 1985, North-Holland, 1986, pp. 153-177.
[10] D. Borrione and J.L. Paillet, "An Approach to the Formal Verification of VHDL De scriptions," Research Report 683-1, Laboratoire Imag-Artemis, Grenoble, France, Nov. 1987.
[11] D. Verkest, L. Claesen, and H. de Man, "Correctness Proof of Parameterized Hardware Modules in the Cathedral-II Synthesis Environment,"Proc. European Design Automation Conf., Mar. 1990, pp. 62-66.
[12] C. Bayol and J.L. Paillet, "Using Tache for Proving Circuits,"Proc. IFIP WG 10.2 Int'l Workshop, Nov. 1989; also inFormal VISI Correctness Verification, L. Claesen, ed., North-Holland, Amsterdam, 1990, pp. 83-88.
[13] A. Bartsch, et al., "LOVERT--A Logic Verifier of Register-Transfer Descriptions," inFormal VLSI Correctness Verification, L. Claesen, ed., North-Holland, 1990, pp. 247-256.
[14] R. S. Boyer and J. S. Moore,A Computational Logic Handbook. Boston, MA: Academic, 1988.
[15] L. Pierre, "Representation fonctionnelle et preuve automatise de circuits digitaux [Functional Representation and Auto mated Proof of Digital Circuits]," PhD the sis, Universite de Provence, Marseille, France. Dec. 1990.
[16] L. Pierre, "One Aspect of Mechanizing Formal Proof of Hardware: the Generalization of Partial Specifications,"Proc. ACM Int'l Workshop Formal Methods in VLSI Design, Jan. 1991.
[17] D. Borrione, L. Pierre, and A. Salem, "PREVAIL: A Proof Environment for VHDL De scriptions,"Proc. Advanced Research Workshop Correct Hardware Design Methodologies, 1991, pp. 169-193.
[18] L. Pierre, "The Formal Proof of the 'Min-max' Sequential Benchmark Described in CASCADE Using the Boyer-Moore Theorem Prover,"Proc. IFIP WC 10.2 Int'l Workshop, Nov. 1989; also inFormal VLSI Correctness Veritication, L. Claesen, ed., North-Holland, 1990, pp. 329-348.
[19] "VHDL Tool Integration Platform (VTIP)," CAD Language Systems, Inc., Rockville, Md., Apr. 1990.
[20] H. Eveking,Verifikation digitaler Systeme [Digital Verification System], B.G. Teubner, Stuttgart, Germany, 1991.
|
 Additional Information
|
Citation:
Dominique D. Borrione, Laurence V. Pierre, Ashrak M. Salem,
"Formal Verification of VHDL Descriptions in the Prevail Environment,"
IEEE Design and Test of Computers,
vol. 09,
no. 2,
pp. 42-56,
April/June,
1992
|
|
RSS Feed