Predicate Abstraction and Refinement for Model Checking VHDL State Machines

In this paper we present an automatic combination of abstraction-refinement by which we translate a VHDL model describing a state system to an initial equivalent abstract system described by SMV to explore its state space to verify CTL properties. We present the method implemented to compute automatically abstractions using decision procedures. This method can handle different kinds of infinite state systems including systems composed of concurrent components and it can be extended for more complex VHDL concepts. Abstract models may admit spurious counterexamples (false negative results) which are executions at the abstract level with no corresponding executions at the concrete level. We devise a new algorithm which analyzes such counterexamples and refine the abstract model correspondingly by eliminating gradually the false negative results. We illustrate our approach on an example and we confirm its effectiveness on a large design.