Formal analysis of correctness of behavioral transformations | Formal Methods in System Design
Skip to main content
Springer Nature Link
Log in

Formal analysis of correctness of behavioral transformations

  • Published:
Formal Methods in System Design Aims and scope Submit manuscript

Abstract

Much has been said about the importance of formal verification in hardware synthesis, but little has been done. Where it has been applied at all, it has only been used on simple, idealized examples. This paper describes the application of formal semantic analysis and verification to part of a working high-level synthesis system. The process revealed several significant errors in that system, errors that had previously been undetected. This experience leads to some reflections on the need for a rigorous, formal basis for hardware specification and synthesis, and on the value of formal techniques.

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

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (Japan)

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. L. Nowak and P. Marwedel. Verification of hardware descriptions by retargetable code generation.Proceedings of the 26th Design Automation Conference, ACM/IEEE, 1989, pp. 441–447.

  2. G.M. Brown and M.E. Leeser. From programs to transistors: Verifying hardware synthesis tools. pp. 129–151. InHardware Specification, Verification and Synthesis: Mathematical Aspects, Lecture Notes in Computer Science, 408: 129–151, 1989.

  3. M. Genoe, L. Claesen, E. Verlind, F. Proesmans, and H. De Man. Illustration of the SFG-tracing multi-level behavioral verification methodology, by the correctness proof of a high to low level synthesis application in CATHEDRAL-II. InProceedings of the International Conference on Computer Design, IEEE, 1991, pp. 338–341.

  4. G.J. Milne. The Correctness of a Simple Silicon Compiler. In6th IFIP International Symposium on Computer Hardware Description Languages and their Application 1983, pp. 1–12.

  5. P.A. Subrahmanyam. The algebraic basis of an expert system for VLSI design. InFormal Aspects of VLSI Design, G. J. Milne and P.A. Subrahmanyam (eds.) North-Holland, New York, 1986.

    Google Scholar 

  6. S.D. Johnson.Synthesis of Digital Designs from Recursion Equations, Ph. D. thesis Indiana University, MIT Press, Cambridge, MA, 1984.

    Google Scholar 

  7. R. Milner.A calculus of communicating systems. Lecture Notes in Computer Science, 92, 1980.

  8. M.C. McFarland and A.C. Parker: An abstract model of behavior for hardware descriptions.IEEE Transactions on Computers C-32(7): 621–36, 1983.

    Google Scholar 

  9. R. Vemuri. How to prove the completeness of a set of register level design transformations. InProceedings of the 27th Design Automation Conference, ACM/IEEE, 1990, pp. 207–212.

  10. R. Camposano. Behavior-preserving transformations for high-level synthesis. InHardware Specification, Verification and Synthesis: Mathematical Aspects, Lecture Notes in Computer Science, 408: 1989.

  11. D.W. Knapp and M. Winslett. A formalization of correctness for linked representations of datapath hardware. InProceedings of the 1989 IFIP WG 10.2/WG 10.5 Conference on Applied Formal Methods for Correct VLSI Design, IFIP, 1989.

  12. M.D. Aagaard and M.L. Leeser. A formally verified system for logic synthesis. InProceedings of the International Conference on Computer Design, IEEE, 1991.

  13. A.J. Martin. Programming in VLSI: From Communicating Processes to Delay-Insensitive Circuits. InUT Year of Programming Institute on Concurrent Programming, C.A.R. Hoare (ed.). Addision-Wesley, Reading, MA, 1989.

    Google Scholar 

  14. D.E. Thomas, E.M. Dirkes, R.A. Walker, J.V. Rajan, J.A. Nestor. and R.L. Blackburn. The system architect's workbench. InProceedings of the 25th Design Automation Conference, ACM/IEEE, pp. 337–343. 1988.

  15. E.D. Lagnese and D.E. Thomas. Architectural partitioning for system level design. InProceedings of the 26th Design Automation Conference, ACM/IEEE, 1989, pp. 62–67.

  16. R.C. Sarma, M.D. Dooley, N.C. Newman, and G. Hetherington. High-level synthesis: Technology transfer to industry. InProceedings of the 27th Design Automation Conference ACM/IEEE, 1990, pp. 549–554.

  17. T.E. Fuhrman. Industrial extensions to university high level synthesis tools: Making it work in the real world. InProceedings of the 28th Design Automation Conference ACM/IEEE, 1991, pp. 520–525.

  18. M.R. Barbacci. Instruction set processor specifications (ISPS): The notation and its applications.IEEE Transactions on Computers, C-30(1):, 1981. 24–40.

    Google Scholar 

  19. M.C. McFarland.Mathematical Models for Verification in a Design Automation System. Ph. D. thesis, Carnegie-Mellon University, 1981.

  20. R.W. Floyd. Assigning meaning to programs. InProceedings of the Symposium on Applied Mathematics 19, American Mathematical Society, 1967, pp. 19–32.

  21. M.C. McFarland. The VT: A database for Automated digital design. DRC-01-4-80, Design Research Centre, Carnegie-Mellon University, 1978.

  22. M.R. Barbacci, G.E. Barnes, R.G. Cattell, and D.P. Siewiorek. The ISPS computer description language. Tech Report, Department of Computer Science, Carnegie-Mellon University, 1979.

  23. M.C. McFarland. A Formal Definition of ISPS for Proving Properties of Hardware Descriptions, Department of Electrical Engineering, Carnegie-Mellon University, 1980.

  24. A. Camilleri, M. Gordon, and T. Melham. Hardware verification using high-order logic:From HDL Descriptions to Guaranteed Correct Circuit Designs, D. Borrione, (ed.). North-Holland, New York, 1987.

    Google Scholar 

  25. D.J. Howe. Computational Metatheory in Nuprl. InProceedings of the 9th International Conference on Automated Deduction, Springer-Verlag, 1989, pp. 238–257.

  26. E.A. Snow.Automation of Module Set Independent Register-Transfer Level Design. Ph.D. thesis, Carnegie-Mellon University, 1978.

  27. E.A. Snow, D.P. Siewiorek, and D.E. Thomas. A technology-relative computer-aided design system: Abstract representations, transformations, and design tradeoffs. InProceedings of the 15th Design Automation Conference, ACM/IEEE, 1978, pp. 220–226.

  28. T.A. Standish, D.C. Harriman, D.F. Kibler, and J.M. Neighbors. The Irvine program transformation catalogue — A stock of ideas for improving programs using source-to-source transformations. Report No. 161, University of California, Irvine, 1976.

    Google Scholar 

  29. D.E. Thomas, C.Y. III Hitchcock, T.J. Kowalski, J.V. Rajan, and R. Walker. Automatic data path synthesis.Computer 16(12): 59–70, 1983.

    Google Scholar 

  30. R.A. Walker and D.E. Thomas. Behavioral transformations for algorithmic level IC design.IEEE Transactions on Computer-Aided Design, 8(10): 1115–1128, 1989.

    Google Scholar 

  31. J.D. Oakley.Symbolic Execution of Formal Machine Descriptions, Ph.D. thesis, Carnegie-Mellon University, 1979.

  32. M.C. McFarland, and T.J. Kowalski. Assisting DAA: The use of global analysis in an expert system. InProceedings of the International Conference on Computer Design, IEEE 1986, pp. 482–485.

  33. J.A. Nestor. Specification & synthesis of digital systems with interfaces. CMUCAD-87-10, Department of Electrical and Computer Engineering, Carnegie-Mellon University, 1987.

Download references

Author information

Authors and Affiliations

  1. Boston College, 02167, Chestnut Hill, MA

    Michael C. McFarland (SJ)

Authors
  1. Michael C. McFarland
    View author publications

    You can also search for this author in PubMed Google Scholar

Rights and permissions

Reprints and permissions

About this article

Cite this article

McFarland, M.C. Formal analysis of correctness of behavioral transformations. Form Method Syst Des 2, 231–257 (1993). https://doi.org/10.1007/BF01384133

Download citation

  • Received:

  • Revised:

  • Issue Date:

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

Keywords

Search

Navigation