Abstract
Despite some of the impressive results quoted in recent verification literature, the verification of even modestly sized “real” industrial designs is not yet feasible on a routine basis. The goal of the work discussed here is to enable the verification of large(r) real systems than currently feasible with any one of the available techniques, and to dovetail the verification methodology with the an underlying design methodology. The specific design methodology considered here is targeted towards the custom design of digital signal processing architectures. Two important attributes of this class of designs are (1) custom-crafted leaf cells, and (2) significant data path components. Our strategy is to partition the subsystems involved into different categories that can be handled by different techniques, and use a divide-and-conquer paradigm. The complexity introduced by data paths is addressed by automating the abstraction of some of the natural equivalences induced, and exploiting this in the context of an extended finite state machine formalism. Specifically, we illustrate how it is possible to exploit the distinction between data and control in implicitly specified state machines (HDLs), and comment on useful abstractions in the presence of symmetry. We illustrate some aspects of the strategy via an example. We also suggest some evolutionary (rather than revolutionary) changes in the design methodology that enable the existing state of art in verification to be better exploited in practise.
Chapter PDF
References
R. E. Bryant. Graph-Based Algorithms for Boolean Function Manipulation. In IEEE Transactions on Computers, volume C-35, pages 677–691, August 1986.
R. E. Bryant. Formal Verification of Memory Circuits by switch-level simulation. In IEEE Transactions on Computer-Aided Design, 10(1), pages 94–102, January 1991.
R. E. Bryant, D. L. Beatty, and C.H.Seger. Formal Hardware Verification by symbolic ternary evaluation. In Proc. ACM/IEEE 23rd Design Automation Conference, pages 397–402, June 1991.
J. Burch, E. Clarke, K. McMillan, and D. Dill. Sequential Circuit Verification Using Symbolic Model Checking. In Proceedings of the 27th Design Automation Conference, pages 46–51, June 1990.
L. Claesen, F. Proesmans, E. Verlind, and H. De Man. SFG-Tracing: a Methodology for the Automatic Verification of MOS Transistor Level Implementations from High Level Behavioral Specifications. In Proceedings of International Workshop on Formal Methods in VLSI Designs, January 1991.
O. Coudert, C. Berthet, and J. C. Madre. Verification of Sequential Machines Using Boolean Functional Vectors. In IMEC-IFIP International Workshop on Applied Formal Methods for Correct VLSI Design, pages 111–128, November 1989.
S. Devadas, K. Keutzer, A.S. Krishnakumar. Design verification and reachability analysis using algebraic manipulations. In Proc.ICCD, pages 250–258, October 1991.
M. Gordon. HOL: A Proof Generating System for Higher Order Logic. In G.Birtwistle and P. A. Subrahmanyam, editors, VLSI Specification, Synthesis and Verification. Kluwer Academic Publishers, 1988.
G. Gratzer. Universal Algebra. Second Edition, Springer Verlag, 1979.
R. Kurshan. Analysis of Discrete Event Coordination Springer Verlag LNCS, 1990.
VHDL. IEEE Standard 1076. VHDL Language Reference Manual. IEEE Press.
D. Lee and M. Yannakakis. Online Minimization of Transition Systems. Personal Communication. (Also, preprint, Proc. Symp. Theory of Computing, 1992.)
T. Kam and P. A. Subrahmanyam. Comparing Layouts with HDL Models: A Formal Verification Technique. In Proceedings of International Conference on Computer Design, pages 588–591, October 1992.
S. Rao, M. Hatamian, and B. D. Ackland. A Design Environment for High Performance VLSI Signal Processing Circuits. In Proc. ICCD, pp. 147–152, October 1990.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Subrahmanyam, P.A. (1993). Towards verifying large(r) systems: A strategy and an experiment. In: Milne, G.J., Pierre, L. (eds) Correct Hardware Design and Verification Methods. CHARME 1993. Lecture Notes in Computer Science, vol 683. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0021720
Download citation
DOI: https://doi.org/10.1007/BFb0021720
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-56778-3
Online ISBN: 978-3-540-70655-7
eBook Packages: Springer Book Archive