Automatic datapath abstraction in hardware systems
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.
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.
KeywordsInteger Variable Reachable State Symbolic Execution Generalize Gate Linear Temporal Logic Formula
- [Bry86]R. E. Bryant, “Graph Based Algorithms for Boolean Function Manipulation”, IEEE Trans. on Computers, C-35(8):677–691, August 1986.Google Scholar
- [BD94]J. Burch, D. Dill, “Automated Verification of Pipelined Micro-processors”, Computer-Aided Verification, 1994.Google Scholar
- [CN94]D. Cyrluk, P. Narendran, “Ground Temporal Logic: A Logic for Hardware Verification”, Computer-Aided Verification, 1994.Google Scholar
- [HB95]R. Hojati, R. K. Brayton, “An Environment for Formal Verification Based On Symbolic Computations”, Journal of Formal Methods, 1995.Google Scholar
- [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
- [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
- [ID93]C. N. Ip, D. Dill, “Better Verification through Symmetry”, Symp. on Computer Hardware Description Languages and Their Application, 1993.Google Scholar
- [MPS92]E. Macii, B. Plessier, F. Somenzi, “Verification of Systems Containing Counters”, IEEE/ACM International Conference on Computer-Aided Design, 1992.Google Scholar
- [Kur92]R. P. Kurshan, “Automata-Theoretic Verification of Coordinating Processes”, UC Berkeley notes, 1992.Google Scholar
- [PVS93]N. Shankar, S. Owre, J. M. Rushby, “The PVS Specification and Verification System”, SRI International, 1993.Google Scholar
- [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
- [Wol86]P. Wolper, “Expressing Interesting Properties of Programs”, 13th Annual ACM Symp. on Principles of Prog. Languages, 1986.Google Scholar