Automatic datapath extraction for efficient usage of HDD
Hybrid Decision Diagrams (HDD) have been proven in Intel to be an important enabler for the formal verification of datapath intensive circuits and in particular the verification of arithmetic units. However, extensive user interaction with the formal verification tool was required in order to use the HDD technology efficiently. The user had to analyze the circuit and its specification and manually partition the signals and operations into control and datapath.
In this paper, we will demonstrate how we have made use of the automatic datapath extraction techniques widely used in the synthesis world in order to efficiently integrate HDDs to an SMV-based formal verification system. The intention of this paper is to illustrate how existing technology can help improve the usability and productivity of the formal verification process and enable efficient integration of new technology, in our case HDDs.
The system described in this paper, Prover, statically analyzes the model to be verified and partitions the representation of the logic to HDDs and Binary Decision Diagrams (BDDs). Moreover, the partitioning algorithm decides which vector operations will be represented more efficiently as word-level (i.e. using HDD) versus bit-level (i.e using BDD).
The new methodology of integrating HDD into the formal verification process increases the productivity of the verification process. At the same time, experiments with Prover show that verification is (both computation and memory usage wise) as efficient as the previously known manual method.
KeywordsModel Check Boolean Function Formal Verification Arithmetic Function Binary Decision Diagram
- R.E.Bryant and Y.A. Chen.Verification of Arithmetic Functions with Binary Moment Diagrams. In Proceedings of the 32nd ACM/IEEE Design Automation Conference, IEEE Computer Society PressGoogle Scholar
- E.Clarke, X.Zhao. Word Level Symbolic Model Checking, CMU-CS-95-161Google Scholar
- Y.Chen, E.Clarke, Pei-Hsin Ho, Y. Hoskote, T. Kam, M. Khaira, J. O'Leary, X. Zhao. Verification of All Circuits in a Floating-Point Unit Using Word-Level Model Checking, In Proceedings of the International Conference on Formal Methods in Computer-Aided Design, November 1996Google Scholar
- R.E.Bryant. Bit-level Analysis of an SRT Divider Circuit. Technical Report, Carnegie Mellon University, 1995Google Scholar
- R.E. Bryant. Graph-based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers, c-35(8):677–691, Aug. 1986Google Scholar
- Laurent Arditi. *BMDs Can Delay the Use of Theorem Proving for Verifying Arithmetic Assembly Instructions, In Proceedings of the International Conference on Formal Methods in Computer-Aided Design, November 1996Google Scholar
- R.Hojati, R.K.Brayton. Automatic Datapath Abstraction In Hardware Systems, In Proceedings of the International Conference on Computer-Aided Verification Conference, 1995Google Scholar
- A.Aziz et.al. HSIS: A BDD-Based Environment for Formal Verification, In Proceedings of the 31st Design Automation Conference, IEEE Computer Society PressGoogle Scholar
- K.Hamaguchi, A. Morita, and S.Yajima. Efficient Construction of Binary Moment Diagrams for Verifying Arithmetic Circuits. In Proceedings of the International Conference on Computer-Aided-Design, pages 78–82, San Jose, CA, November 1995.Google Scholar
- K.Ravi, A.Pardo, G.Hachtel, F.Somenzi. Modular Verification of Multipliers. In Proceedings of the International Conference on Formal Methods in Computer-Aided Design, Palo Alto, CA, November 1996Google Scholar
- M.Fujita. Verification of Arithmetic Circuits by Comparing Two Similiar Circuits. In Proceedings of the International Conference on Computer-Aided Verification, 1996Google Scholar
- K.S.Brace, R.L.Rudell, and R.E.Bryant. Efficient Implementation of a BDD Package. In Proceedings of the Design Automation Conference, pages 535–541, San Francisco, CA, June 1995.Google Scholar
- E.M.Clarke, M. Khaira, and X.Zhao. Word Level Model Checking — A New Approach for Verifying Arithmetic Circuits. In Proceedings of the 33rd ACM/IEEE Design Automation Conference. IEEE Computer Society Press, June 1996.Google Scholar
- D.E. Atkins. Higher-radix Division Using Estimates of the Divisor and Partial remainders. IEEE Transactions on Computers, C-17(10):925–934, October 1968.Google Scholar
- R. Enders. Note on the Complexity of Binary Moment Diagram Representations. unpublished paper, Siemens AG, Munich Germany, 1994.Google Scholar
- K.L.McMillan. Symbolic Model Checking, Kluwer Academic Publishers.Google Scholar