Skip to main content
SpringerLink
Log in
Book cover

International Conference on Formal Methods in Computer-Aided Design

FMCAD 1996: Formal Methods in Computer-Aided Design pp 1–18Cite as

The need for formal methods for integrated circuit design

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1166))

Abstract

This paper has reviewed the typical rt1 and behavioral synthesis design flows and identified areas where formal methods can be applied. In particular, the problems of design and implementation verification were identified as amenable to formal techniques and a number of well-motivated areas for research were identified. These included:

  • Formalisms to discipline human reasoning during the generation of an rt1 or behavioral-level design;

  • Formal semantics for synthesizable subsets of existing hardware-design languages such as VHDL and Verilog;

  • Formal methods for specification which are intuitive and easy to use;

  • Formal means for expressing properties of integrated circuits;

  • Formal methods for verifying properties of integrated circuits;

  • Formal methods for verifying that an rt1 representation is consistent with a behavioral-level representation;

  • More robust methods for verifying that two sequential circuits are equivalent.

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. A. Eiriksson. Integrating formal verification methods with a conventional project design flow. In Proceedings of the 33rd ACM/IEEE Design Automation Conference, pages 666–671. IEEE Computer Society Press, Los Alamitos, CA, June 1996.

    Google Scholar 

  2. S. B. Akers. Binary Decision Diagrams. In IEEE Transactions on Computers, volume C-27, pages 509–516, June 1978.

    Google Scholar 

  3. G. Berry, S. Moisan, and J-P. Rigault. ESTEREL: Towards a synchronous and semantically sound high level language for real-time applications. In Proceedings of the Proceedings of the IEEE Real-Time Systems Symposium, pages 30–37. IEEE, New York, December 1983.

    Google Scholar 

  4. Archie Blake. Canonical expressions in Boolean algebra. PhD thesis, University of Chicago, March 1938.

    Google Scholar 

  5. K. Brace, R. Bryant, and R. Rudell. Efficient implementation of a bdd package. In Proceedings, 27th Design Automation Conference, June 1990.

    Google Scholar 

  6. R. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C35(8), August 1986.

    Google Scholar 

  7. R. Bryant. On the complexity of VLSI implementations and graph representations of boolean functions, with applications to integer multiplication. IEEE Transactions on Computers, C40(2):205–213, February 1991.

    Google Scholar 

  8. J. T. Buck, S. Ha, E. A. Lee, and D. G. Messerschmitt. Ptolemy: A framework for simulating and prototyping heterogeneous systems. International Journal in Computer Simulation, 4(2):155–182, 1994.

    Google Scholar 

  9. R. Camposano and W. Wolf. High-Level VLSI Synthesis. Kluwer Academic Publishers, Norwell, MA, 1991.

    Google Scholar 

  10. E. M. Clarke, J. R. Burch, and K. L. McMillan. Sequential circuit verification using symbolic model checking. In Proceedings, 27th Design Automation Conference. ACM/IEEE, June 1990.

    Google Scholar 

  11. O. Coudert, C. Berthet, and J. C. Madre. Verification of synchronous sequential machines using symbolic execution. In Proceedings of the International Workshop on Automatic Verification Methods for Finite State Systems, Grenoble, France, volume 407 of Lecture Notes in Computer Science, pages 365–373. Springer-Verlag, New York, June 1989.

    Google Scholar 

  12. D. Deharbe and D. Borrione. A qualitative finite subset of VHDL and semantics. In Correct Hardware Design and Verification Methods, volume 987 of Lecture Notes in Computer Science. Springer-Verlag, New York, 1995.

    Google Scholar 

  13. G. DeMicheli. Synthesis and Optimization of Digital Circuits. McGraw-Hill, New York, NY, 1994.

    Google Scholar 

  14. S. Devadas, A. Ghosh, and K. Keutzer. Logic Synthesis. McGraw-Hill Book Company, 1994.

    Google Scholar 

  15. S. Devadas and K. Keutzer. An automata-theoretic approach to behavioral equivalence. Integration, the VLSI Journal, 12:109–129, December 1991.

    Google Scholar 

  16. S. Devadas, H-K. T. Ma, and A. R. Newton. On the verification of sequential machines at differing levels of abstraction. In IEEE Transactions on Computer-Aided Design, pages 713–722, June 1988.

    Google Scholar 

  17. M. Fujita, H. Fujisawa, and N. Kawato. Evaluation and improvements of Boolean comparison method based on binary decision diagrams. In Proceedings of the Int'l Conference on Computer-Aided Design, pages 2–5, November 1988.

    Google Scholar 

  18. I. Gertner and R. P. Kurshan. Logical analysis of digital circuits. In M. R. Barbacci and C. J. Koomen, editors, Proceedings of the Eighth International Symposium on Computer Hardware Description Languages and their Applications, pages 47–67. IFIP, North-Holland, Amsterdam, 1987.

    Google Scholar 

  19. Mike Gordon. The semantic challenge of Verilog HDL. In Proceedings, Tenth Annual IEEE Symposium on Logic in Computer Science, pages 136–145, June 1995.

    Google Scholar 

  20. A. Gupta. Formal hardware verification methods: A survey. In R. K. Brayton, E. M. Clarke, and P. A. Subrahmanyam, editors, Formal Methods in System Design, volume 1 (Nos. 2/3). Kluwer Academic Publishers, Boston, October 1992.

    Google Scholar 

  21. K. Keutzer and P. Vanbekbergen. Computer-Aided Design of Electronic Circuits. In D. Christiansen, editor, Electronic Engineer's Handbook: Fourth Editon. McGraw-Hill, 1997. (to appear).

    Google Scholar 

  22. J. Kukula. A technique for verifying finite state machines. Technical Report 3A, IBM Technical Disclosure Bulletin, August 1989.

    Google Scholar 

  23. P. Loewenstein and D. L. Dill. Verification of a multiprocessor cache protocol using simulation relations and higher-order logic. In E. M. Clarke and R. P. Kurshan, editors, Proceedings of the Workshop on Computer-Aided Verification (CAV 90), volume 3 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science. American Mathematical Society, Springer-Verlag, New York, 1991.

    Google Scholar 

  24. J-C. Madre and J-P. Billon. Proving circuit correctness using formal comparison between expected and extracted behavior. In Proceedings, 25th Design Automation Conference. ACM/IEEE, June 1988.

    Google Scholar 

  25. S. Malik, A. R. Wang, R. Brayton, and A. Sangiovanni-Vincentelli. Logic Verification using Binary Decision Diagrams in a Logic Synthesis Environment. In Proceedings of the Int'l Conference on Computer-Aided Design, pages 6–9, November 1988.

    Google Scholar 

  26. Michael McFarland. A practical application of verification to high-level synthesis. In Proc. of the 1991 International Workshop on Formal Methods in VLSI Design, January 1991.

    Google Scholar 

  27. K. McMillan and J. Schwalbe. Formal verfication of the gigamax cache coherency protocol. Technical report, Carnegie Mellonn University, august 1990.

    Google Scholar 

  28. S. Muroga. VLSI System Design. Wiley-Interscience, New York, 1982.

    Google Scholar 

  29. Bryan T. Preas and Michael J. Lorenzetti, editors. Physical Design Automation of VLSI Systems. Benjamin-Cummings, 1988.

    Google Scholar 

  30. S. Ritz, M. Pankert, V. Zivojnovic, and H. Meyr. High level software synthesis for the design of communication systems. IEEE J. on Selected Areas in Communications, 11:348–358, April 1993.

    Google Scholar 

  31. Claude E. Shannon. The synthesis of two-terminal switching circuits. Bell System Technical Journal, 28:59–98, January 1949.

    Google Scholar 

  32. K. J. Supowit and S. J. Friedman. A New Method for Verifying Sequential Circuits. In Proceedings of the23rd Design Automation Conference, pages 200–207, June 1986.

    Google Scholar 

  33. T. Szymanski and C. Van-Wyck. GOALIE:a space-efficient system for VSLI artwork analysis. In IEEE Transactions on Computer-Aided Design, volume CAD-3, pages 278–280, 1984.

    Google Scholar 

  34. P. Zepter and T. Grotker. Generating synchronous timed descriptions of digital receivers from dynamic dataflow system level configurations. In Proc. of European Design and Test Conference, February 1994.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Synopsys, Inc., Mountain View, CA

    Kurt Keutzer

Authors
  1. Kurt Keutzer
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Mandayam Srivas Albert Camilleri

Rights and permissions

Reprints and permissions

Copyright information

© 1996 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Keutzer, K. (1996). The need for formal methods for integrated circuit design. In: Srivas, M., Camilleri, A. (eds) Formal Methods in Computer-Aided Design. FMCAD 1996. Lecture Notes in Computer Science, vol 1166. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0031796

Download citation

  • DOI: https://doi.org/10.1007/BFb0031796

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-61937-6

  • Online ISBN: 978-3-540-49567-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation