Skip to main content
SpringerLink
Log in

The Implementation and Proof of a Boolean Simplification System

  • Conference paper
Designing Correct Circuits

Part of the book series: Workshops in Computing ((WORKSHOPS COMP.))

Abstract

We have implemented and proved a Boolean simplification system. Our algorithm is based on the weak division algorithm used in MIS; our implementation is in the programming language ML. We began with a proof of the algorithm presented previously and extended it to a level of detail sufficient for proving the implementation of the system. In the process of developing the proof we clarified many definitions presented in previous accounts of the algorithm, and discovered several errors in our implementation. The result is that the designs generated by our implementation can be claimed to be correct by construction, since we have proved the correctness of our system.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Mario Benedicty and Frank R. Sledge. Discrete Mathematical Structures. Harcourt Brace Jovanovich, 1987.

    Google Scholar 

  2. D. Bostick, G. D. Hachtel, R. Jacoby, M. R. Lightner, et al. The Boulder optimal logic design system. In International Conference on Computer-Aided Design, pages 62–65, 1987.

    Google Scholar 

  3. R. K. Brayton, G. D. Hachtel, C. T. McMullen, and A. L. Sangiovanni-Vincentelli. Logic Minimization Algorithms for VLSI Synthesis. Kluwer Academic Publishers, 1984.

    Book  MATH  Google Scholar 

  4. R. K. Brayton and C. McMullen. Decomposition and factorization of boolean expressions. In International Symposium on Circuits and Systems, 1982.

    Google Scholar 

  5. R. K. Brayton, R. Rudell, et al. MIS: A multiple-level logic optimization system. IEEE Transactions on Computer-Aided Design, CAD-6(6), 1987.

    Google Scholar 

  6. R. K. Brayton, R. Rudell, et al. Multi-level logic optimization and the rectangular covering problem. In International Conference on Computer-Aided Design, pages 66–69, November 1987.

    Google Scholar 

  7. Shiu-Kai Chin. Combining engineering vigor with mathematical rigor. In Miriam Leeser and Geoffrey Brown, editors, Proceedings of the MSI Workshop on Hardware Specification, Verification, and Synthesis: Mathematical Aspects. Springer Verlag, 1990. LNCS 408.

    Google Scholar 

  8. R. L. Constable et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice Hall, 1986.

    Google Scholar 

  9. J. A. Darringer et al. LSS: A system for production logic synthesis. IBM Journal of Research and Development, 28(5):537–545, September 1984.

    Article  Google Scholar 

  10. A. de Geus and W. Cohen. A rule-based system for optimizing combinational logic. IEEE Design and Test of Computers, 2(4):22–32, 1985.

    Article  Google Scholar 

  11. F. K. Hanna, M. Longley, and N. Daeche. Formal synthesis of digital systems. In L. J. M. Claesen, editor, Applied Formal Methods for Correct VLSI Design. IMEC-IFIP, North-Holland, 1990.

    Google Scholar 

  12. A. J. Martin. The design of a delay-insensitive microprocessor: An example of circuit synthesis by program transformation. In Miriam Leeser and Geoffrey Brown, editors, Proceedings of the MSI Workshop on Hardware Specification, Verification, and Synthesis: Mathematical Aspects. Springer Verlag, 1990. LNCS 408.

    Google Scholar 

  13. Alexander Saldanha, Albert R. Wang, and Robert K Brayton. Multi-level logic simplification using don’t cares and filters. In 26th Design Automation Conference, pages 277–282. ACM/IEEE, June 1989.

    Google Scholar 

  14. Mary Sheeran. Categories for the working hardware designer. In Miriam Leeser and Geoffrey Brown, editors, Proceedings of the MSI Workshop on Hardware Specification, Verification, and Synthesis: Mathematical Aspects. Springer Verlag, 1990. LNCS 408.

    Google Scholar 

  15. Ake Wikstrom. Functional Programming Using Standard ML. Prentice Hall, 1987.

    MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Electrical Engineering, Cornell University, Ithaca, NY, 14853, USA

    Mark Aagaard & Miriam Leeser

Authors
  1. Mark Aagaard
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Miriam Leeser
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Oxford University Computing Laboratory, 11 Keble Road, OX1 3QD, Oxford, England

    Geraint Jones

  2. Department of Computing Science, University of Glasgow, G12 8QQ, Glasgow, Scotland

    Mary Sheeran

Rights and permissions

Reprints and permissions

Copyright information

© 1991 Springer-Verlag London

About this paper

Cite this paper

Aagaard, M., Leeser, M. (1991). The Implementation and Proof of a Boolean Simplification System. In: Jones, G., Sheeran, M. (eds) Designing Correct Circuits. Workshops in Computing. Springer, London. https://doi.org/10.1007/978-1-4471-3544-9_10

Download citation

  • DOI: https://doi.org/10.1007/978-1-4471-3544-9_10

  • Publisher Name: Springer, London

  • Print ISBN: 978-3-540-19659-4

  • Online ISBN: 978-1-4471-3544-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation