Abstract
A new approach for the automatic equivalence checking of behavioral or structural descriptions of designs with complex control is presented. The verification tool combines symbolic simulation with a hierarchy of equivalence checking methods, including decision-diagram based techniques, with increasing accuracy in order to optimize overall verification time without giving false negatives. The equivalence checker is able to cope with different numbers of control steps and different implementational details in the two descriptions to be compared.
Acknowledgement
The authors would like to thank the anonymous reviewers for helpful comments.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
C. W. Barrett, D.L. Dill, and J. R. Levitt: Validity checking for combinations of theories with equality. In Proc. FMCAD’96,Springer LNCS 1166, 1996.
C. W. Barrett, D. L. Dill, and J. R. Levitt: A decision procedure for bit-vector arithmetic. In Proc. DAC’98, 1998.
D. L. Beatty and R. E. Bryant: Formally verifying a microprocessor using a simulation methodology. In Proc. DAC’94, 1994.
B. Brock, W. A. Hunt, and M. Kaufmann: The FM9001 microprocessor proof. Technical Report 86, Computational Logic Inc., 1994.
B. Brock, M. Kaufmann, and J. S. Moore: ACL2 theorems about commercial microprocessors. In Proc. FMCAD’96, Springer LNCS 1166, 1996.
R. E. Bryant: Graph-based algorithms for Boolean function manipulation. In IEEE Trans. on Computers, Vol. C-35, No. 8, pages 677–691, 1986.
R. E. Bryant and Y.-A. Chen: Verification of arithmetic functions with binary moment diagrams. Technical Report CMU-CS-94-160, Carnegie Mellon University, 1994.
R. E. Bryant and Y.-A. Chen: Verification of arithmetic circuits with binary moment diagrams. In Proc. DAC’95, 1995.
J. R Burch: Techniques for verifying superscalar microprocessors. In Proc. DAC7#x2019;96, 1996.
J. R. Burch, E. Clarke, K. McMillan, and D. Dill: Sequential circuit verification using symbolic model checking. In Proc. DAC’90, 1990.
J. R. Burch and D. L. Dill: Automatic verification of pipelined microprocessor control. In Proc. CAV’94. Springer LNCS 818, 1994.
O. Coudert, C. Berthet, and J.-C. Madre: Verification of synchronous sequential machines based on symbolic execution. In Proc. Automatic Verification Methods for Finite State Systems, Springer LNCS 407, 1989.
D. A. Greve: Symbolic simulation of the JEM1 microprocessor. In Proc. FMCAD’98, Springer LNCS 1522, 1998.
J. L. Hennessy, D. A. Patterson: Computer architecture: a quantitative approach. Morgan Kaufman, CA, second edition, 1996.
H. Hinrichsen, H. Eveking, and G. Ritter: Formal synthesis for pipeline design. In Proc. DMTCS+CATS’99, Auckland, 1999.
S. Höreth: Implementation of a multiple-domain decision diagram package. In Proc. CHARME’97, pp. 185–202, 1997.
S. Höreth:Hybrid Graph Manipulation Package Demo. URL:http://www.rs. etechnik.tu-darmstadt.de/~sth/demo.html,Darmstadt 1998.
R. Hosabettu, M. Srivas, and G. Gopalakrishnan: Decomposing the proof of correctness of pipelined microprocessors. In Proc. CAV’98, Springer LNCS 1427, 1998.
R. B. Jones, D. L. Dill, and J. R. Burch: Efficient validity checking for processor verification. In Proc. ICCAD’95, November 1995.
R. B. Jones, J. U. Skakkebæk, and D. L. Dill: Reducing manual abstraction in formal verification of out-of-order execution. In Proc. FMCAD’98, Springer LNCS 1522, 1998.
J. S. Moore: Symbolic simulation: an ACL2 approach. In Proc. FMCAD’98, Springer LNCS 1522, 1998.
J. U. Skakkebæk, R. B. Jones, and D. L. Dill: Formal verification of out-of-order execution using incremental flushing. In Proc. CAV’98, Springer LNCS 1427, 1998.
M. Srivas and S. P. Miller: Applying formal verification to a commercial microprocessor. In Computer Hardware Description Language, August 1995.
M. N. Velev and R. E. Bryant: Bit-level abstraction in the verification of pipelined microprocessors by correspondence checking. In FMCAD’98, Springer LNCS 1522, 1998.
P. J. Windley and J. R. Burch: Mechanically checking a lemma used in an automatic verification tool. In Proc. FMCAD’96, November 1996.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ritter, G., Eveking, H., Hinrichsen, H. (1999). Formal Verification of Designs with Complex Control by Symbolic Simulation. In: Pierre, L., Kropf, T. (eds) Correct Hardware Design and Verification Methods. CHARME 1999. Lecture Notes in Computer Science, vol 1703. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48153-2_18
Download citation
DOI: https://doi.org/10.1007/3-540-48153-2_18
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66559-5
Online ISBN: 978-3-540-48153-9
eBook Packages: Springer Book Archive