A New Verification Method of Digital Circuits Based on Cone-Oriented Partitioning and Decision Diagrams

Abstract:

The formal verification is able to check whether the implementation of a circuit design is functionally equivalent to an earlier version described at the same level of abstraction, it can show the correctness of a circuit design. A new circuit verification method based on cone-oriented circuit partitioning and decision diagrams is presented in this paper. First of all, the structure level of every signal line in a circuit is computed. Secondly, the circuit is partitioned into a lot of cone structures. The multiple-valued decision diagram corresponding to every cone structure is generated. The verification procedure is to compare the equivalence of the multiple-valued decision diagrams of two types of cone structures. Experimental results on a lot of benchmark circuits show the method presented in this paper can effectively perform the equivalence checking of circuits.

• Periodical: Applied Mechanics and Materials (Volumes 29-32)
• Pages: 1040-1045
• DOI: https://doi.org/10.4028/www.scientific.net/AMM.29-32.1040
• Online since: August 2010
• Authors: Zhong Liang Pan, Ling Chen
• Keywords: Circuit Partitioning, Decision Diagram, Digital Circuit, Equivalence Checking, Formal Verification

References

[1] C. Kaihui, D.A. Papa, I.L. Markov, V. Bertacco. Incremental verification with error detection, diagnosis, and visualization. IEEE Design & Test of Computers, vol. 26, no. 2, pp.34-43, (2009).

DOI: 10.1109/mdt.2009.38

[2] G. Cabodi, S. Nocco, S. Quer. Strengthening model checking techniques with inductive invariants. IEEE Trans. on CAD, vol. 28, no. 1, pp.154-158, (2009).

DOI: 10.1109/tcad.2008.2009147

[3] W.S. Chieh, W.C. Yao, C.Y. Chih. Novel probabilistic combinational equivalence checking. IEEE Trans. on VLSI, vol. 16, no. 4, pp.365-375, (2008).

DOI: 10.1109/tvlsi.2008.917397

[4] S. Andrei, A.M. Cheng. Efficient verification and optimization of real time logic specified system. IEEE Trans. on Computers, vol. 58, no. 12, pp.1640-1653, (2009).

DOI: 10.1109/tc.2009.79

[5] S.K. Srinivasan, K. Sarker, R.S. Katti. Verification of synchronous elastic processors. IEEE Embedded Systems Letters, vol. 1, no. 1, pp.14-18, (2009).

DOI: 10.1109/les.2009.2028043

[6] K. Lata, S.K. Roy. Towards formal verification of analog mixed signal designs using SPICE circuit simulation traces. Asia Symposium on Quality Electronic Design, pp.162-172, (2009).

DOI: 10.1109/asqed.2009.5206276

[7] D. Walter, S. Little, C. Myers, N. Seegmiller, T. Yoneda. Verification of analog/mixed-signal circuits using symbolic methods. IEEE Trans. on CAD, vol. 27, no. 12, pp.2223-2235, (2008).

DOI: 10.1109/tcad.2008.2006159

[8] S.K. Tiwary, A. Gupta, J.R. Phillips. First steps towards SAT-based formal analog verification. IEEE/ACM International Conference on Computer-Aided Design, pp.1-8, (2009).

DOI: 10.1145/1687399.1687401

[9] R. Chakraborty, D.R. Chowdhury. Raising the level of abstraction for the timing verification of system-on-chips. IEEE Computer Society Annual Symposium on VLSI, pp.459-462, (2008).

DOI: 10.1109/isvlsi.2008.68

[10] W. Chunyao, T. Shingwu, J. Jingyang. Automatic interconnection rectification for SoC design verification based on port order fault model. IEEE Trans. CAD, vol. 22, no. 1, pp.104-114, (2003).

DOI: 10.1109/tcad.2002.805723

[11] A. Benso, S.D. Carlo, P. Prinetto, Y. Zorian. IEEE Standard 1500 compliance verification for embedded cores. IEEE Trans. on VLSI, vol. 16, no. 4, pp.397-407, (2008).

DOI: 10.1109/tvlsi.2008.917412

[12] I. Poliakov, A. Mokhov, A. Rafiev, D. Sokolov. Automated verification of asynchronous circuits using circuit Petri Nets. IEEE International Symposium on Asynchronous Circuits and Systems, pp.161-170, (2008).

DOI: 10.1109/async.2008.18

[13] K. Weinberger, S. Bulach, R. Bosch. Application of workflow Petri Nets to modeling of formal verification processes in design flow of digital integrated circuits. Design, Automation and Test in Europe, pp.937-938, (2008).

DOI: 10.1109/date.2008.4484798