Abstract
The concept of Design for Verifiability is introduced as a means of attacking the complexity problem encountered when verifying the correctness of hardware designs using mathematical proof techniques. The inherent complexity of systems implemented as integrated circuits results in a comparable descriptive complexity when modelling them in any framework which supports formal verification. Performing formal verification then rapidly becomes intractable as a consequence of this descriptive complexity. In this paper we propose a strategy for dealing, at least in part, with this problem. We advocate the use of a particular design strategy involving the use of structural design rules which constrain the behaviour of a design resulting in a less complex design verification. The term Design for Verifiability is used to capture this concept in an analogous way to the term Design for Testability.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
A. Cohn, "A Proof of Correctness of the Viper microprocessor: the First Level". Technical Report 104, Computer Laboratory, University of Cambridge, January 1987.
B.S. Davie and G.J. Milne, "Contextual Constraints for Design and Verification". In VLSI Specification, Verification and Synthesis, Birtwistle and Subrahmanyam (Eds). Kluwer Academic Publishers, 1988.
B.S. Davie, "A Formal, Hierarchical Design and Validation Methodology for VLSI", Ph.D. thesis CST-55-88, Department of Computer Science, University of Edinburgh.
H. Eveking, "Formal Verification of Synchronous Systems". In Formal Aspects of VLSI Design, Milne and Subrahmanyam (eds). Elsevier North-Holland, 1986.
M. Gordon, "Why Higher-Order Logic is a Good Formalism for Specifying and Verifying Hardware". In Formal Aspects of VLSI Design, Milne and Subrahmanyam (eds). Elsevier North-Holland, 1986.
F.K. Hanna and N. Daeche, "Specification and Verification using Higher-Order Logic". Proc. 7th Int. Symp. on Computer Hardware Description Languages and their Applications (CHDL 85), Elsevier North-Holland, 1985.
G.J. Milne, "The Correctness of a Simple Silicon Compiler". Proc. 6th Int. Symp. on Computer Hardware Description Languages and their Applications (CHDL 83), Uehara and Barbacci (eds), Elsevier North-Holland, 1983.
G.J. Milne, "Towards Verifiably Correct VLSI Design". In Formal Apsects of VLSI Design, Milne and Subrahmanyam (eds), Elsevier North-Holland, 1986.
J. Siskind, J. Southard and K. Crouch, "Generating Custom High-Performance VLSI Designs from Succinct Algorithmic Descriptions". In Proc. MIT Conference on Advanced Research in VLSI, MIT, 1982.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1990 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Milne, G.J. (1990). Design for verifiability. In: Leeser, M., Brown, G. (eds) Hardware Specification, Verification and Synthesis: Mathematical Aspects. Lecture Notes in Computer Science, vol 408. Springer, New York, NY. https://doi.org/10.1007/0-387-97226-9_20
Download citation
DOI: https://doi.org/10.1007/0-387-97226-9_20
Published:
Publisher Name: Springer, New York, NY
Print ISBN: 978-0-387-97226-8
Online ISBN: 978-0-387-34801-8
eBook Packages: Springer Book Archive