Abstract
We present a symbolic simulation based verification approach which can be applied to large synchronous circuits. A new technique to encode the state and input constraints as parametric Boolean expressions over the state and input variables is used to make our symbolic simulation based verification approach efficient. The constraints which are encoded through parametric Boolean expressions can involve the Boolean connectives (·, +, ⌝), the relational operators (<, ≤, >, ≥, ≠, =), and logical connectives (∧, ∨). This technique of using parametric Boolean expressions vastly reduces the number of symbolic simulation vectors and the time for verification. Our verification approach can also be applied for efficient modular verification of large designs; the technique used is to verify each constituent sub-module separately, however in the context of the overall design. Since regular arrays are part of many large designs, we have developed an approach for the verification of regular arrays which combines formal verification at the high level and symbolic simulation at the low level(e.g., switch-level). We show the verification of a circuit called Minmax, a pipelined cache memory system, and an LRU array implementation of the least recently used block replacement policy, to illustrate our verification approach. The experimental results are obtained using the COSMOS symbolic simulator.
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
Derek L. Beatty, Randal E. Bryant, and Carl-Johan H.Seger. Synchronous circuit verification by symbolic simulation: An illustration. In Sixth MIT Conference on Advanced Research in VLSI, 1990. MIT Press, 1990.
Christian Berthet, Olivier Coudert, and Jean-Christophe Madre. New ideas on symbolic manipulations of finite state machines. In Proceedings of the ICCD, 1990, pages 224–227, 1990.
F. M. Brown. Boolean Reasoning. Kluwer Academic Publishers, 1990.
Randal E. Bryant. A methodology for hardware verification based on logic simulation. Technical Report CMU-CS-90-122, Computer Science, Carnegie Mellon University, March 1990. Accepted for publication in the JACM.
Randal E. Bryant. Formal verification of memory circuits by switch-level simulation. IEEE Transactions on Computer-Aided Design, 10(1):94–102, January 1991.
Randal E. Bryant, Derek L. Beatty, and Carl-Johan H. Seger. Formal hardware verification by symbolic ternary trajectory evaluation. In Proc. ACM/IEEE 28th Design Automation Conference, pages 397–402, June 1991.
Randal E. Bryant and Carl-Johan H. Seger. Formal verification of digital circuits using ternary system models. Technical Report CMU-CS-90-131, School of Computer Science, Carnegie Mellon University, May 1990. Also in the Proceedings of the Workshop on Computer-Aided Verification, Rutgers University, June, 1990.
Olivier Coudert, Christian Berthet, and Jean-Christophe Madre. Verification of sequential machines using boolean functional vectors. In Proceedings of the IMEC-IFIP Workshop on Applied Formal Methods for Correct VLSI Design, Leuven, Belgium, pages 179–196, November 1989.
Ganesh Gopalakrishnan. Hop: A formal model for synchronous circuits using communicating fundamental mode symbolic automata. Technical Report UUCS-TR-92-006, Dept. of Computer Science, University of Utah, Salt Lake City, UT 84112, 1992. Submitted to “Formal Methods in System Design”.
Ganesh Gopalakrishnan and Prabhat Jain. A practical approach to synchronous hardware verification. In Proc. VLSI Design '91: The Fourth CSI/IEEE International Symposium on VLSI Design, New Delhi, India, January 1991.
Ganesh Gopalakrishnan, Prabhat Jain, Venkatesh Akella, Luli Josephson, and Wen-Yan Kuo. Combining verification and simulation. In Carlo Sequin, editor, Advanced Research in VLSI: Proceedings of the 1991 University of California Santa Cruz Conference. The MIT Press, 1991. ISBN 0-262-19308-6.
Prabhat Jain and Ganesh Gopalakrishnan. Some techniques for efficient symbolic simulation based verification. Technical Report UUCS-TR-91-023, University of Utah, Department of Computer Science, October 1991.
Prabhat Jain, Ganesh Gopalakrishnan, and Prabhakar Kudva. Verification of regular arrays by symbolic simulation. Technical Report UUCS-TR-91-022, University of Utah, Department of Computer Science, October 1991.
Carl-Johan H. Seger and Jeffrey Joyce. A two-level formal verification methodology using HOL and COSMOS. Technical Report 91-10, Dept. of Computer Science, University of British Columbia, Vancouver, B.C., June 1991.
D. Verkest and L. Claesen. The minmax system benchmark, November 1989.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Jain, P., Kudva, P., Gopalakrishnan, G. (1993). Towards a verification technique for large synchronous circuits. In: von Bochmann, G., Probst, D.K. (eds) Computer Aided Verification. CAV 1992. Lecture Notes in Computer Science, vol 663. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-56496-9_10
Download citation
DOI: https://doi.org/10.1007/3-540-56496-9_10
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-56496-6
Online ISBN: 978-3-540-47572-9
eBook Packages: Springer Book Archive