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 interconnectionsof 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 presenta new HDL-satisfiability checkingalgorithm 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...

• Type: Conference
• Year: 1998
• Where: DAC
• Authors: Farzan Fallah, Srinivas Devadas, Kurt Keutzer
• Keywords: DAC 1998, Design Automation, HDL Model, Satisfiability Checking Methods, Satisfiability Checking Problem