Functional vector generation for HDL models using linear programming and Boolean satisfiability

Our strategy for automatic generation of functional vectors is based on exe rcising selected paths in the given hardware description language (HDL) mod el. The HDL model describes interconnections of arithmetic, logic, and memo ry modules. Given a path in the HDL model, the search for input stimuli tha t exercise the path can be converted into a standard satisfiability (SAT) c hecking problem by expanding the arithmetic modules into logic gates, Howev er, this approach is not very efficient. We present a new HDL-SAT checking algorithm that works directly on the HDL model. The primary feature of our algorithm is a seamless integration of linear-programming techniques for fe asibility checking of arithmetic equations that govern the behavior of data -path modules and SAT checking for logic equations that govern the behavior of control modules. This feature is critically important to efficiency, si nce it avoids module expansion and allows us to work with logic and arithme tic equations whose cardinality tracks the size of the HDL model. We descri be the details of the HDL-SAT checking algorithm in this paper. Experimenta l results that show significant speedups over state-of-the-art gate-level S AT checking methods are included.