Automatic datapath abstraction in hardware systems

  • Ramin Hojati
  • Robert K. Brayton
Session 4: Invited Talk
Part of the Lecture Notes in Computer Science book series (LNCS, volume 939)


The biggest stumbling block to make formal verification widely acceptable is the state space explosion problem. Abstraction is used to simplify a design so that the number of reachable states is reduced. In this paper, we first introduce a concurrency model, called integer combinational/sequential (ICS), capable of describing hardware systems at high and low levels of abstractions. ICS uses finite relations, interpreted and uninterpreted integer functions and predicates, interpreted memory functions, and supports non-determinism and fairness constraints. As a subset, it includes finite-state systems with general fairness constraints. Verification in this framework is performed using language containment as follows.
  1. 1.

    For a subclass of “control-intensive” ICS models, we prove that finite small instantiations can be used to decide the properties without sacrificing accuracy. A linear time algorithm for recognizing these subsets is given. These results also hold for the standard finite-state systems and thus also provide some generic methods for automatic data abstraction for such systems. Using these results, we are able to verify a memory model by reducing integer data values to binary, and unbounded memory addresses to a small number.

  2. 2.

    For verifying properties of circuits with complex datapaths, the model can be executed symbolically to find the reachable states. In some cases, the set of reachable states is finite, and the verification can be completed exactly. In other cases, given n, the verifier checks that no errors of length less than n exist.



Integer Variable Reachable State Symbolic Execution Generalize Gate Linear Temporal Logic Formula 
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.


  1. [Bry86]
    R. E. Bryant, “Graph Based Algorithms for Boolean Function Manipulation”, IEEE Trans. on Computers, C-35(8):677–691, August 1986.Google Scholar
  2. [BD94]
    J. Burch, D. Dill, “Automated Verification of Pipelined Micro-processors”, Computer-Aided Verification, 1994.Google Scholar
  3. [CN94]
    D. Cyrluk, P. Narendran, “Ground Temporal Logic: A Logic for Hardware Verification”, Computer-Aided Verification, 1994.Google Scholar
  4. [HB95]
    R. Hojati, R. K. Brayton, “An Environment for Formal Verification Based On Symbolic Computations”, Journal of Formal Methods, 1995.Google Scholar
  5. [HBK94]
    R. Hojati, S. Krishnan, R. K. Brayton, “Heuristic Algorithms for Early Quantification and Partial Product Minimization”, ERL Memorandum M94/11, March 1994, UC Berkeley.Google Scholar
  6. [HMLB95]
    R. Hojati, R. Mueller-Thuns, P. Lowenstein, R. K. Brayton, “Automatic Verification of Memory System Using Language Containment and Abstraction”, to be submitted to CHDL 95.Google Scholar
  7. [ID93]
    C. N. Ip, D. Dill, “Better Verification through Symmetry”, Symp. on Computer Hardware Description Languages and Their Application, 1993.Google Scholar
  8. [MPS92]
    E. Macii, B. Plessier, F. Somenzi, “Verification of Systems Containing Counters”, IEEE/ACM International Conference on Computer-Aided Design, 1992.Google Scholar
  9. [Kur92]
    R. P. Kurshan, “Automata-Theoretic Verification of Coordinating Processes”, UC Berkeley notes, 1992.Google Scholar
  10. [PVS93]
    N. Shankar, S. Owre, J. M. Rushby, “The PVS Specification and Verification System”, SRI International, 1993.Google Scholar
  11. [Sho79]
    R. E. Shostak, “A Practical Decision Procedure for Arithmetic With Function Symbols”, JACM Volume 26, No. 2, April 1979, pp. 351–360.Google Scholar
  12. [Wol86]
    P. Wolper, “Expressing Interesting Properties of Programs”, 13th Annual ACM Symp. on Principles of Prog. Languages, 1986.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • Ramin Hojati
  • Robert K. Brayton

There are no affiliations available

Personalised recommendations