Towards verifying large(r) systems: A strategy and an experiment

  • P. A. Subrahmanyam
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 683)


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.


  1. [1]
    R. E. Bryant. Graph-Based Algorithms for Boolean Function Manipulation. In IEEE Transactions on Computers, volume C-35, pages 677–691, August 1986.Google Scholar
  2. [2]
    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.Google Scholar
  3. [3]
    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.Google Scholar
  4. [4]
    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.Google Scholar
  5. [5]
    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.Google Scholar
  6. [6]
    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.Google Scholar
  7. [7]
    S. Devadas, K. Keutzer, A.S. Krishnakumar. Design verification and reachability analysis using algebraic manipulations. In Proc.ICCD, pages 250–258, October 1991.Google Scholar
  8. [8]
    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.Google Scholar
  9. [9]
    G. Gratzer. Universal Algebra. Second Edition, Springer Verlag, 1979.Google Scholar
  10. [10]
    R. Kurshan. Analysis of Discrete Event Coordination Springer Verlag LNCS, 1990.Google Scholar
  11. [11]
    VHDL. IEEE Standard 1076. VHDL Language Reference Manual. IEEE Press.Google Scholar
  12. [12]
    D. Lee and M. Yannakakis. Online Minimization of Transition Systems. Personal Communication. (Also, preprint, Proc. Symp. Theory of Computing, 1992.)Google Scholar
  13. [13]
    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.Google Scholar
  14. [14]
    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.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1993

Authors and Affiliations

  • P. A. Subrahmanyam
    • 1
  1. 1.AT&T Bell LaboratoriesHolmdel

Personalised recommendations