The Implementation and Proof of a Boolean Simplification System

  • Mark Aagaard
  • Miriam Leeser
Part of the Workshops in Computing book series (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.

Keywords

Boulder Cond 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [1]
    Mario Benedicty and Frank R. Sledge. Discrete Mathematical Structures. Harcourt Brace Jovanovich, 1987.Google Scholar
  2. [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. [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.CrossRefMATHGoogle Scholar
  4. [4]
    R. K. Brayton and C. McMullen. Decomposition and factorization of boolean expressions. In International Symposium on Circuits and Systems, 1982.Google Scholar
  5. [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. [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. [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. [8]
    R. L. Constable et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice Hall, 1986.Google Scholar
  9. [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.CrossRefGoogle Scholar
  10. [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.CrossRefGoogle Scholar
  11. [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. [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. [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. [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. [15]
    Ake Wikstrom. Functional Programming Using Standard ML. Prentice Hall, 1987.MATHGoogle Scholar

Copyright information

© Springer-Verlag London 1991

Authors and Affiliations

  • Mark Aagaard
    • 1
  • Miriam Leeser
    • 1
  1. 1.School of Electrical EngineeringCornell UniversityIthacaUSA

Personalised recommendations