A COMPOSITIONAL RULE FOR HARDWARE DESIGN REFINEMENT
We present an approach to designing verified digital systems by a sequence
of small local refinements. Refinements in this approach are not limited to
a library of predefined transformations for which theorems have been previously
established. Rather, the approach relies on localizing the refinement steps in such a way that they are
verified efficiently by model checking. Toward this end, a compositional rule
is proposed by which each design refinement may be verified independently, in
an abstract environment. This rule supports the use of downward refinement maps,
which translate abstract behavior to detailed behavior. These maps may involve
temporal transformations, including delay. The approach is supported by a
verification tool based on symbolic model checking.
Relevant PapersK. L. McMillan, "A compositional rule for hardware design refinement"
TransparenciesThe transparencies in Postscript format
|©2002-2018 U.C. Regents|