Abstract
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 can be 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 detailed behavior. These maps may involve temporal transformations, including delay. The approach is supported by a verification tool based on symbolic model checking.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
R. Alur and T. A. Henzinger. Reactive modules. In 11th annual IEEE symp. Logic in Computer Science (LICS '96), 1996.
D. L. Beatty and R. E. Bryant. Formally verifying a microprocessor using a simulation methodology. In 31st Design Automation Conference, pages 596–602, 1994.
J. R. Burch and D. L. Dill. Automatic verification of pipelined microprocessor control. In D. L. Dill, editor, Conf. Computer-Aided Verification (CAV '94), volume 818 of LNCS. Springer-Verlag, 1994.
S. Bose and A. Fisher. Verifying pipelined hardware using symbolic logic simulation. In IEEE International Conference on Computer Design, 1989.
D. Cyrluk. Inverting the abstraction mapping: a methodology for hardware verification. In M. Srivas and A. Camilleri, editors, Formal Methods in Computer-Aided Design (FMCAD '96), volume 1166 of LNCS. Springer-Verlag, 1996.
O. Grümberg and D. E. Long. Model checking and modular verification. ACM Trans. Programming Languages and Systems, 16(3):843–871, 1994.
R. B. Jones, D. L. Dill, and J. R. Burch. Efficient validity checking for processor verification. In IEEE/ACM Int. Conf. on Computer Aided Design (ICCAD '95), 1995.
R. P. Kurshan. Reducibility in analysis of coordination. In LNCS, volume 103, pages 19–39. Springer-Verlag, 1987.
R. P. Kurshan. Computer-Aided Verification of Coordinating Processes. Princeton, 1994.
L. Lamport. Specifying concurrent program modules. ACM Trans. Programming Languages and Systems, 5:190–222, 1983.
K. L. McMillan. Symbolic Model Checking. Kluwer, 1993.
A. Pnueli. In transition from global to modular temporal reasoning about programs. In K. Apt, editor, Logics and Models of Concurrent Systems, pages 123–144. Springer-Verlag, 1985.
P. Wolper. Temporal logic can be more expressive. Information and Control, 56:72–99, 1983.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
McMillan, K.L. (1997). A compositional rule for hardware design refinement. In: Grumberg, O. (eds) Computer Aided Verification. CAV 1997. Lecture Notes in Computer Science, vol 1254. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63166-6_6
Download citation
DOI: https://doi.org/10.1007/3-540-63166-6_6
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63166-8
Online ISBN: 978-3-540-69195-2
eBook Packages: Springer Book Archive