Name
Title | ||
|---|---|---|
Functional vector generation for HDL models using linear programming and 3-satisfiability |
Abstract | ||
|---|---|---|
Our strategy for automatic generation of functional vectors is based on exercising selected paths in the given hardware description language (HDL) model. The HDL model describes interconnections of arithmetic, logic and memory modules. Given a path in the HDL model, the search for input stimuli that exercise the path can be converted into a standard satisfiability checking problem by expanding the arithmetic modules into logic-gates. However, this approach is not very efficient. We present a new HDL-satisfiability checking algorithm that works directly on the HDL model. The primary feature of our algorithm is a seamless integration of linear-programming techniques for feasibility checking of arithmetic equations that govern the behavior of datapath modules, and 3-SAT checking for logic equations that govern the behavior of control modules. This feature is critically important to efficiency, since it avoids module expansion and allows us to work with logic and arithmetic equations whose cardinality tracks the size of the HDL model. We describe the details of the HDL-satisfiability checking algorithm in this paper. Experimental results which show significant speedups over state-of-the-art gate-level satisfiability checking methods are included. |
Year | DOI | Venue |
|---|---|---|
1998 | 10.1145/277044.277187 | DAC |
Keywords | Field | DocType |
3-satisfiability,new hdl-satisfiability checking algorithm,arithmetic equation,state-of-the-art gate-level satisfiability checking,hdl model,mpeg4,logic equation,gate-level satisfiability,synthesis,functional vector generation,arithmetic module,hardware description languages,3-sat checking,hdl models,hdl-satisfiability checking algorithm,standard satisfiability checking problem,linear programming,voltage scaling,placement,computability,vector generation,low power,feasibility checking,level converters,flip-flops,codec,hdl-satisfiability checking,hardware description language,design automatian,satisfiability,vectors,logic programming,linear program,logic gate,arithmetic | Abstraction model checking,Datapath,Model checking,Computer science,Satisfiability,Cardinality,Theoretical computer science,Computability,Logic programming,Hardware description language | Conference |
ISBN | Citations | PageRank |
0-89791-964-5 | 67 | 4.18 |
References | Authors | |
18 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Farzan Fallah | 1 | 557 | 43.73 |
| Srinivas Devadas | 2 | 8606 | 1146.30 |
| Kurt Keutzer | 3 | 5040 | 801.67 |