Environment modeling and efficient state reachability checking
Jacob A. Abraham, Richard Raimi · 1999
As the size and complexity of hardware designs increases and their time to market decreases, validation via case by case testing is more and more being seen as inadequate. Formal verification, which provide mathematically sound proofs about design properties, is increasingly being turned to. However, formal verification suffers from capacity limitations. Industrial designs must often be partitioned to meet these limitations, which creates a plethora of interfaces that need to be modeled. In this work, we focus on this modeling problem. Conducting verification in the presence of input constraints is the unifying theme of this thesis. Our first approach is to model hardware designs as networks of interacting, finite state machines (FSMs), and synthesize abstractions of these networks that preserve trace equivalence at the boundary of a given component machine. Verification can then be performed on that component composed with the abstract network. We reduce the concrete state space by computing a new type of simulation relation called a forward-backward relation, and choosing representative states on its basis. We make further reductions by removing component FSMs that exhibit language universality over their outputs while exhibiting input independence from certain of their inputs. We give algorithms for detecting both these conditions. In the second part of the thesis, we focus on low cost methods for determining state reachability. These techniques allow an incremental incorporation of a concrete environment, in contrast to abstracting it. We give algorithmic improvements for techniques known as bounded model checking, in which a propositional formula is created encoding all computation paths of a state transition system over a finite time interval, and satisfiability solving is used to derive witnesses or counterexamples for temporal logic specifications from the formula. We give experimental results which demonstrate the effectiveness of these techniques, not only for functional verification, but also in the areas of timing analysis and sequential fault test generation.