Abstract
Our approach for verifying the equivalence of two VHDL architectures consists in translating these descriptions into functional forms and then in proving the equivalence of these functions. As far as replicated or parallel architectures are concerned, an induction-based method is used for verifying generic n-bit descriptions. This technique takes advantage of the regular structure of these devices and can give better results than the BDD-based approaches. However, induction requires complete specifications, whereas the designers usually supply partial specifications. Therefore, we propose a specialized automatic method for generalizing such incomplete statements, before the Boyer-Moore proof process.
Chapter PDF
Similar content being viewed by others
References
P. ASHAR, A. GHOSH, S. DEVADAS, A. NEWTON: “Combinational and sequential logic verification using general binary decision diagrams”. Proc. Int. Workshop on Logic Synthesis, Research Triangle Park (NC), May 1991.
R. AUBIN: “Mechanizing structural induction-Part II: Strategies”. Theoretical Computer Science 9. North-Holland, 1979. pp. 347–362.
R.S. BOYER, J. S. MOORE: “A Computational Logic”. ACM Monograph Series. Academic Press, Ins. 1979.
R.S. BOYER, J. S. MOORE: “A Computational Logic Handbook”. Perspectives in Computing, Vol. 23. Academic Press, Inc. 1988.
D. BORRIONE, L. PIERRE, A. SALEM: “Formal Verification of VHDL Descriptions in the PREVAIL Environment”. IEEE Design&Test magazine, vol. 9, n∘2, June 1992.
R.E. BRYANT: “Graph-based Algorithms for Boolean Function Manipulation”. IEEE Transactions on Computers, Vol. C-35, n∘8, August 1986.
R.E. BRYANT: “On the Complexity of VLSI Implementations and Graph Representations of Boolean Functions with Application to Integer Multiplication”. IEEE Transactions on Computers, Vol. 40, n∘2, February 1991.
J.R. BURCH: “Using BDDs to verify multipliers”. Proc. DAC'91, San Francisco (CA), June 1991.
P. CAMURATI, P. PRINETTO: “Formal Verification of Hardware Correctness: Introduction and Survey of Current Research”. IEEE Computer, Vol. 21, n∘7. July 1988.
M. FUJITA, H. FUJISAWA, N. KAWATO: “Evaluation and Improvements of Boolean Comparison Method based on Binary Decision Diagrams”. Proc. Int. Conference on Computer-Aided Design ICCAD'88, 1988.
W.A. HUNT: “FM8501: A verified microprocessor”. Institute for Computing Science, University of Texas, Austin (USA). Technical Report n∘47. February 1986.
K. HWANG: “Computer arithmetic: principles, architecture and design”, John Wiley & sons Inc., New-York, 1979.
IEEE Standard VHDL Language Reference Manual, IEEE. 1988.
T. KROPF: “Benchmark-Circuits for Hardware Verification, 2nd TPCD Conference”. 2nd Conference on Theorem Proving in Circuit Design, Bad Herrenalb (Germany), 1994.
J.S. MOORE: “Introducing Iteration into the Pure Lisp Theorem Prover”. IEEE Transactions on Software Engineering, Vol. SE-1, n∘3. September 1975.
Z. MANNA, R. WALDINGER: “Knowledge and Reasoning in Program Synthesis”. Artificial Intelligence Journal. Vol. 6, 2. 1975.
S. MALIK, A.R. WANG, R.K. BRAYTON, A. SANGIOVANNI-VINCENTELLI: “Logic Verification using Binary Decision Diagrams in a Logic Synthesis Environment”. Proc. Int. Conference on Computer-Aided Design ICCAD'88, 1988.
L. PIERRE: “The Formal Proof of the Min-Max sequential benchmark described in CASCADE using the Boyer-Moore Theorem Prover”. Proc. IFIP WG 10.2 Int. Workshop Nov. 1989. In “Formal VLSI Correctness Verification”, L. Claesen ed., North Holland, 1990.
L. PIERRE: “One Aspect of Mechanizing Formal Proof of Hardware: the Generalization of Partial Specifications”. Proc. ACM International Workshop on Formal Methods in VLSI Design. Miami (Fl). 9–11 January 1991.
L. PIERRE: “VHDL Description and Formal Verification of Systolic Multipliers”. In “CHDL and their Applications”, D. Agnew, L. Claesen & R. Camposano Eds., North Holland, 1993.
H. SIMONIS: “Formal verification of multipliers”. Proc. IFIP WG 10.2 Int. Workshop Nov. 1989. In “Formal VLSI Correctness Verification”, L. Claesen ed., North Holland, 1990.
D. VERKEST, L. CLAESEN, H. DE MAN: “Special Benchmark Session on Formal System Design”. Proc. IFIP WG 10.2 Int. Workshop Nov. 1989. In “Formal VLSI Correctness Verification”, L. Claesen ed., North Holland, 1990.
F. WAGNER: “Prevail-DM: a framework-based environment for formal hardware verification”. In “CHDL and their Applications”, D. Agnew, L. Claesen & R. Camposano Eds., North Holland, 1993.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Pierre, L. (1995). An automatic generalization method for the inductive proof of replicated and parallel architectures. In: Kumar, R., Kropf, T. (eds) Theorem Provers in Circuit Design. TPCD 1994. Lecture Notes in Computer Science, vol 901. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-59047-1_43
Download citation
DOI: https://doi.org/10.1007/3-540-59047-1_43
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-59047-7
Online ISBN: 978-3-540-49177-4
eBook Packages: Springer Book Archive