APPLICATION OF MIXED INTEGER LINEAR PROGRAMMING IN THE GENERATION OF VECTORS WITH MAXIMUM DATAPATH COVERAGE FOR COMBINATIONAL LOGIC CIRCUITS
Abstract
In this paper, we present a novel methodology for vector generation that maximizes the metric of datapath coverage for a given combinational logic circuit. The proposed methodology is based on Mixed Integer Linear Programming (MILP). The search of input vectors based on the datapath coverage metric is a satisfiability (SAT) problem. In order to obtain maximum coverage vectors, we use a novel model for the Boolean logic gates to translate the original SAT problem into an MILP optimization problem. Next, the new problem is solved following the MILP optimization environment and an exhaustive search strategy. We compare our proposed methodology with the exhaustive search algorithm. Experimental results and performance comparisons based on the large set of MCNC'91 suite of benchmark circuits are presented. They show significant speedups of MILP methodology against the exhaustive search algorithm for the complex circuits.
This paper was recommended by Regional Editor Majid Ahmadi.
References
-
P. Rashihkar , P. Paterson and L. Singh , System-on-a-Chip Verification — Methodology and Techniques ( Kluwer Academic Publishers , 2001 ) . Google Scholar -
H. B. Carter and S. G. Hemmady , Metric Driven Design Verification: An Engineer's and Executive's Guide to First Pass Success ( Springer-Verlag , 2007 ) . Crossref, Google Scholar - IEEE Des. Test of Comput. 18, 36 (2001), DOI: 10.1109/54.936247. Crossref, ISI, Google Scholar
M. Kantrowitz and Lisa M. Noack , I'm done simulating; now what? Verification coverage analysis and correctness checking of the DECchip 21164 Alpha microprocessor, Proc. Design Automation Conference (DAC) (1996) pp. 325–330. Google ScholarV. Jerinic , New Methods and Coverage Metrics for Functional Verification, Proc. Design, Automation and Test in Europe (DATE) (2006) pp. 1–6. Google ScholarH. Mangassarian , Maximum circuit activity estimation using pseudo-Boolean satisfiability, Proc. Design, Automation and Test in Europe Conference (DATE) (2007) pp. 1–6. Google ScholarP. Mishra and N. Dutt , Functional coverage driven test generation for validation of pipelined processors, Proc. Design, Automation and Test in Europe' (DATE)2 (2005) pp. 678–683. Google ScholarJohn R. Wallack and Ramaswami Dandapani , Coverage metrics for functional test, Proc. 12th IEEE VLSI Test Symposium (1994) pp. 176–181. Google Scholar- IEEE Trans. Comput.-Aided Des. Integr. Circuits System 27, 1305 (2008), DOI: 10.1109/TCAD.2008.925790. Crossref, ISI, Google Scholar
O. Guzey , Functional test selection based on unsupervised support vector analysis, Proc. 45th ACM/IEEE Design Automation Conference (DAC) (2008) pp. 262–267. Google Scholar- S. Yang, Logic Synthesis and Optimization Benchmarks User Guide version 3.0, Rep. Microelectronics Center of North Carolina, (1991) . Google Scholar
Z. Zeng , P. Kalla and M. Ciesielski , LPSAT: A unified approach to RTL satisfiability, Proc. on Design, Automation and Test in Europe (2001) pp. 398–402. Google Scholar-
A. Makhorin , GNU Linear Programming Kit Reference Manual ( Department for Applied Informatics, Moscow Aviation Institute , 2003 ) . Google Scholar -
N. A. Sherwani , Algorithms for VLSI Physical Design Automation ( Kluwer Academic Publishers , 1993 ) . Crossref, Google Scholar - ILOG Inc., ILOG CPLEX: Using the CPLEX Linear Optimizer and Mixed Integer Optimizer (ILOG CPLEX Division, Sunnyvale, CA, 2008) . Google Scholar
R. K. Brayton ,Lecture Notes in Computer Science 1102 (Springer-Verlag, 1996) pp. 428–432. Google Scholar
