A guiding heuristic for the semi-formal verification of high-level designs

Functional verification of complex designs is still a major bottleneck in the VLSI design cycle. Despite the recent advancements in formal methods, the use of formal verification at the higher levels of abstraction is not yet well established. At these levels, assertions are typically combined with simulation for checking the properties of the HDL descriptions at runtime. Several works have proposed methods for checking assertions in simulation based environments, but the quality of the input test cases is yet a problem of great relevance. This work presents a novel approach for the search for counterexamples of assertions in the validation of HDL descriptions. The executable model of the system is combined with heuristic functions to assess how close an input vector is from violating a property of the DUV. Using this guiding heuristic as the objective function, the search can be formulated as an optimization problem. The formal definition for this method is presented along with illustrative examples.