Abstract
We have proved a logic synthesis tool with the Nuprl proof development system. The logic synthesis tool, Pbs, implements the weak division algorithm, and is part of the Bedroc hardware synthesis system. Our goal was to develop a proven and usable implementation of a hardware synthesis tool. Pbs consists of approximately 1000 lines of code implemented in a functional subset of Standard ML. The program was verified by embedding this subset of SML in Nuprl and then verifying the correctness of the implementation of Pbs in Nuprl. In the process of doing the proof we learned many lessons which can be applied to efforts in verifying functional software. In particular, we were able to safely perform several optimizations to the program. In addition, we have invested effort into verifying software which will be used many times, rather than verifying the output of that software each time the program is used. The work required to verify hardware design tools and other similar software is worthwhile because the results of the proofs will be used many times.
Mark Aagaard is supported by a fellowship from Digital Equipment Corporation. This research was supported in part by the National Science Foundation under Award No. MIP-9100516.
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
Mark Aagaard. A verified system for logic synthesis. Master's thesis, Department of Electrical Engineering, Cornell University, January 1992.
Mark Aagaard and Miriam Leeser. The implementation and proof of a boolean simplification system. In Geraint Jones and Mary Sheeran, editors, Designing Correct Circuits, Oxford 1990. Springer-Verlag, 1991.
R. K. Brayton and C. McMullen. Decomposition and factorization of boolean expressions. In International Symposium on Circuits and Systems, 1982.
R. S. Boyer and J. S. Moore. A Computational Logic Handbook. Academic Press, 1988. Volume 23 of Perspectives in Computing.
R. K. Brayton, R. Rudell, et al. MIS: A multiple-level logic optimization system. IEEE Transactions on Computer-Aided Design, CAD-6(6), 1987.
R. L. Constable et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice Hall, 1986.
A. J. Camillieri, M. J. C. Gordon, and T. F. Melham. Hardware verification using higher-order logic. In D. Borrione, editor, From HDL Descriptions to Guaranteed Correct Circuit Designs. North Holland, September 1986.
Shiu-Kai Chin. Combining engineering vigor with mathematical rigor. In Proceedings of the MSI Workshop on Hardware Specification, Verification, and Synthesis: Mathematical Aspects. Springer Verlag, 1990. LNCS 408.
G. Hachtel, R. Jacoby, K. Keutzer, and C. Morrison. On the relationship between area optimization and multifault testability of multilevel logic. In International Conference on Computer Aided Design, pages 316–319. ACM/IEEE, 1989.
W. A. Hunt, Jr. FM8501: A Verified Microprocessor. PhD thesis, Institute for Computing Science, The University of Texas at Austin, 1986.
A. J. Martin. The design of a delay-insensitive microprocessor: An example of circuit synthesis by program transformation. In Proceedings of the MSI Workshop on Hardware Specification, Verification, and Synthesis: Mathematical Aspects. Springer Verlag, 1990. LNCS 408.
Michael C. McFarland. A practical application of verification to high-level synthesis. In International Workshop on Formal Methods in VLSI Design. ACM, 1991.
R. Harper R. Milner, M. Tofte. The Definition of Standard ML. The MIT Press, 1990.
D. E. Thomas, E. M. Dirkes, R. A. Walker, J. V. Rajan, J. A. Nestor, and R. L. Blackburn. The system architect's workbench. In 25th Design Automation Conference, pages 337–343. ACM/IEEE, 1988.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Aagaard, M., Leeser, M. (1993). Verifying a logic synthesis tool in Nuprl: A case study in software verification. In: von Bochmann, G., Probst, D.K. (eds) Computer Aided Verification. CAV 1992. Lecture Notes in Computer Science, vol 663. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-56496-9_7
Download citation
DOI: https://doi.org/10.1007/3-540-56496-9_7
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-56496-6
Online ISBN: 978-3-540-47572-9
eBook Packages: Springer Book Archive