Functional test generation based on word -level satisfiability

• Main Author: Zeng, Zhihong
• Language: ENG
• Published: ScholarWorks@UMass Amherst 2003
• Subjects: Electrical engineering
• Online Access: https://scholarworks.umass.edu/dissertations/AAI3078730

The increase in size and functional complexity of digital designs necessitates the development of robust, efficient, automated verification tools. Despite recent advances in formal verification, such as symbolic model checking and theorem proving, simulation remains a dominant design validation approach in industry. Simulation techniques do not require expert knowledge in writing specifications. Furthermore, simulation, especially when coupled with modern symbolic techniques, scales well with the design complexity. However the efficiency of simulation in validating the design remains highly dependent on functional test sequences applied as design stimulus. This dissertation addresses the issue of functional test generation for designs specified at the register transfer level (RTL) or at the behavioral level, using hardware description languages (HDL), with the goal to increase efficiency of functional simulation. The generation of functional test vectors for design validation can be posed as a satisfiability (SAT) problem. Previous methods use BDDs and other Boolean representations of the underlying logic to formulate and solve the SAT problem. These approaches are not efficient, as they do not utilize the word-level information inherently present in the design, resulting in excessive run time. To overcome this limitation this work presents methods to enhance the capabilities of functional test generation by raising the level of abstraction of the design. It addresses the SAT problem on the level of abstraction that enables efficient handling of designs containing word-level arithmetic operators and bit-level Boolean logic. Two word-level SAT techniques are proposed that allow the arithmetic and Boolean portions of the design to be solved in a unified domain. First technique, LPSAT, is based on integer linear programming, while the second, CLP-SAT uses constraint logic programming to model the interaction between the arithmetic and Boolean parts of the design. Preliminary experimental results show that our unified approach is a promising improvement to Boolean SAT on designs with mixed datapath and control logic. In addition, in the hope of providing a comprehensive SAT solution to functional test generation and other verification applications, we illustrated several ideas in intelligently integrating different SAT methods.