Functional Test Generation using Constraint Logic Programming

— Semi-formal verification based on symbolic simulation offers a good compromise between formal model checking and numerical simulation. The generation of functional test vectors, guided by miscellaneous coverage metrics to satisfy the simulation target, can be posed as a satisfiability problem (SAT). This paper presents a novel approach to solving SAT based on Constraint Logic Programming (CLP) technique. The proposed SAT solver allows to efficiently handle the designs with mixed word-level arithmetic operators and Boolean logic. It is applicable for designs specified at different levels, including HDL, RTL, and Boolean. The experimental results are quite encouraging compared with classical CNF-based, BDD-based, and LPbased SAT solvers. I. SATISFIABILITY IN SEMI-FORMAL VERIFICATION Numerical simulation remains a dominant design validation method in industry since it scales well with the design complexity. A typical design verification scenario includes random and pseudo-random ...

• Type: Conference
• Year: 2001
• Where: IFIP
• Authors: Zhihong Zeng, Maciej J. Ciesielski, Bruno Rouzeyre
• Keywords: Coverage Metrics, Functional Coverage, IFIP 2001, Miscellaneous Coverage Metrics, Programming Languages