Model abstraction via semantic extraction of behavioral vhdl descriptions for formal verification
Steven P. Levitan, Yee-Wing Hsieh · 2000
Validating a design using formal verification methods is inherently demanding of memory and computation resources. As a result, in general only small designs can be directly formally verified. To handle large designs, model abstraction is necessary. Model abstraction takes a model and replaces it with a high-level description of non-deterministic automata that encapsulates the behavior of the model it replaces. Using this high-level abstract representation, model abstraction reduces the number of states necessary to perform formal verification and thus reduces the state space to be explored by formal verification tools. This dissertation presents a model abstraction methodology for improving the performance of formal verification of digital system designs. We have built a system which analyzes the semantics of a behavioral VHDL model of a design and its design specifications to be verified. Abstract models consisting of non-deterministic finite state machines (NFSMs) are generated through matching of extracted semantic attributes against known abstraction templates. Using NFSM models for counters, comparators and registers, this model abstraction methodology can yield many orders of magnitude reductions in state space size and substantial improvements in performance of formal verification runs. Furthermore, since abstractions are performed at the VHDL source code level, the abstraction methodology is independent of the formal verification tool and the abstraction techniques presented in the dissertation can be combined with other techniques to achieve further improvement in formal verification performance.