Functional Test Generation Using Constraint Logic Programming
Abstract
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 technique. The proposed SAT solver allows efficiently handling 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 LP-based SAT solvers.
Fichier principal
Zeng2002_Chapter_FunctionalTestGenerationUsingC.pdf (1.81 Mo)
Télécharger le fichier
Origin | Files produced by the author(s) |
---|