Abstract
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.
Chapter PDF
References
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 Press
E.Clarke, X.Zhao. Word Level Symbolic Model Checking, CMU-CS-95-161
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 1996
R.E.Bryant. Bit-level Analysis of an SRT Divider Circuit. Technical Report, Carnegie Mellon University, 1995
R.E. Bryant. Graph-based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers, c-35(8):677–691, Aug. 1986
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 1996
R.Hojati, R.K.Brayton. Automatic Datapath Abstraction In Hardware Systems, In Proceedings of the International Conference on Computer-Aided Verification Conference, 1995
A.Aziz et.al. HSIS: A BDD-Based Environment for Formal Verification, In Proceedings of the 31st Design Automation Conference, IEEE Computer Society Press
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.
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 1996
M.Fujita. Verification of Arithmetic Circuits by Comparing Two Similiar Circuits. In Proceedings of the International Conference on Computer-Aided Verification, 1996
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.
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.
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.
R. Enders. Note on the Complexity of Binary Moment Diagram Representations. unpublished paper, Siemens AG, Munich Germany, 1994.
K.L.McMillan. Symbolic Model Checking, Kluwer Academic Publishers.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kamhi, G., Weissberg, O., Fix, L., Binyamini, Z., Shtadler, Z. (1997). Automatic datapath extraction for efficient usage of HDD. In: Grumberg, O. (eds) Computer Aided Verification. CAV 1997. Lecture Notes in Computer Science, vol 1254. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63166-6_12
Download citation
DOI: https://doi.org/10.1007/3-540-63166-6_12
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63166-8
Online ISBN: 978-3-540-69195-2
eBook Packages: Springer Book Archive