A refinement calculus for the synthesis of verified hardware descriptions in VHDL

ABSTRACT

A formal refinement calculus targeted at system-level descriptions in the IEEE standard hardware description language VHDL is described here. Refinement can be used to develop hardware description code that is “correct by construction”. the calculus is closely related to a Hoare-style programming logic for VHDL and real-time systems in general. That logic and a semantics for a core subset of VHDL are described. The programming logic and the associated refinement calculus are shown to be complete. This means that if there is a code that can be shown to implement a given specification, then it will be derivable from the specification via the calculus.

REFERENCES

• 1: BACK, R.-J. AND SERE, K. 1991. Stepwise refinement of action systems. Struct. Program. 12, 17-30.
• 2: Dominique Borrione , Ashraf Salem, Denotational semantics of a synchronous VHDL subset, Formal Methods in System Design, v.7 n.1-2, p.53-71, Aug. 1995 [doi>10.1007/BF01383873]
• 3: Dominique D. Borrione , Laurence V. Pierre , Ashrak M. Salem, Formal Verification of VHDL Descriptions in the Prevail Environment, IEEE Design & Test, v.9 n.2, p.42-56, April 1992 [doi>10.1109/54.143145]
• 4: Bhaskar Bose , Steven D. Johnson, DDD-FM9001: Derivation of a Verified Microprocessor, Proceedings of the IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, p.191-202, May 24-26, 1993
• 5: BREUER, P., MARTfNEZ MADRID, N., SJtNCHEZ, L., MARfN LOPEZ, A., AND DELGADO KLOOS, C. 1996a. A formal method for specification and refinement of real-time systems. In Proceedings of the 8th EuroMicro Workshop on Real Time Systems. IEEE Computer Society Press, Los Alamitos, Calif.
• 6: BREUER, P., MARTfNEZ MADRID, N., SANCHEZ, L., MARfN L(SPEZ, A., AND DELGADO KLOOS, C. 1996b. Putting logical time into a real-time language. In the Asia-Pacific Conference on Hardware Definition Languages. 107-111.
• 7: Peter T. Breuer , Luis Sánchez Fernández , Carlos Delgado Kloos, A simple denotational semantics, proof theory and a validation condition generator for unit-delay VHDL, Formal Methods in System Design, v.7 n.1-2, p.27-51, Aug. 1995 [doi>10.1007/BF01383872]
• 8: CHRISTIAN, F. 1994. Correct and robust programs. IEEE Trans. Softw. Eng. 10, 163-174.
• 9: David Déharbe , Dominique Borrione, Semantics of a verification-oriented subset of VHDL, Proceedings of the IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, p.293-310, October 02-04, 1995
• 10: Carlos Delgado Kloos , Peter T. Breuer, Formal Semantics for VHDL, Kluwer Academic Publishers, Norwell, MA, 1995
• 11: Colin J. Fidge, Real-Time Refinement, Proceedings of the First International Symposium of Formal Methods Europe on Industrial-Strength Formal Methods, p.314-331, April 19-23, 1993
• 12: Mike Gordon, The Semantic Challenge of Verilog HDL, Proceedings of the 10th Annual IEEE Symposium on Logic in Computer Science, p.136, June 26-29, 1995
• 13: M. J. C. Gordon , T. F. Melham, Introduction to HOL: a theorem proving environment for higher order logic, Cambridge University Press, New York, NY, 1993
• 14: IEEE. 1988. IEEE standard VHDL language reference manual. IEEE Std. 1076-1987. Institute of Electrical and Electronics Engineers, New York.
• 15: Steven D. Johnson , Paul S. Miner , Albert John Camilleri, Studies of the Single Pulser in Various Reasoning Systems, Proceedings of the Second International Conference on Theorem Provers in Circuit Design - Theory, Practice and Experience, p.126-145, September 26-28, 1994
• 16: C. B. Jones, Tentative steps toward a development method for interfering programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.5 n.4, p.596-619, Oct. 1983 [doi>10.1145/69575.69577]
• 17: KING, S. AND MORGAN, C. 1995. Exits in the refinement calculus. Formal Aspects Comput. 7, 54-76.
• 18: H. Kopetz , R. Zainlinger , G. Fohler , H. Kantz , P. Puschner , W. Schütz, The design of real-time systems: from specification to implementation and verification, Software Engineering Journal, v.6 n.3, p.72-82, May 1991
• 19: Thomas Kropf , Klaus Schneider , Ramayya Kumar, A Formal Framework for High Level Synthesis, Proceedings of the Second International Conference on Theorem Provers in Circuit Design - Theory, Practice and Experience, p.223-238, September 26-28, 1994
• 20: Proceedings of the Second International Conference on Theorem Provers in Circuit Design - Theory, Practice and Experience, September 1994
• 21: iV{AHONY, B. P. AND HAYES, I. J. 1991. Using continuous real functions to model timed histories. In Proceedings of the 6th Australian Software Engineering Conference (ASWEC91). Australian Computer Society, 257-270.
• 22: iV{AYGER, E., FRANCIS, iV{., HARRIS, R., iV{USGRAVE, G., AND FOURMAN, iV{. 1991. The need for a core method. In EuroMicro'91.
• 23: Jean P. Mermet, VHDL for Simulation, Synthesis, and Formal Proofs of Hardware, Kluwer Academic Publishers, Norwell, MA, 1992
• 24: Carroll Morgan, Programming from specifications (2nd ed.), Prentice Hall International (UK) Ltd., Hertfordshire, UK, 1994
• 25: Joseph M. Morris, A theoretical basis for stepwise refinement and the programming calculus, Science of Computer Programming, v.9 n.3, p.287-306, December 1, 1987 [doi>10.1016/0167-6423(87)90011-6]
• 26: Greg Nelson, A generalization of Dijkstra's calculus, ACM Transactions on Programming Languages and Systems (TOPLAS), v.11 n.4, p.517-561, Oct. 1989 [doi>10.1145/69558.69559]
• 27: SALEM, A. AND BORRIONE, D. 1992. Formal semantics of VHDL timing constructs. In VHDL for Simulation, Synthesis and Formal Proofs of Hardware, J. Mermet, Ed. Kluwer, Amsterdam.
• 28: A. C. Shaw, Reasoning About Time in Higher-Level Language Software, IEEE Transactions on Software Engineering, v.15 n.7, p.875-889, July 1989 [doi>10.1109/32.29487]
• 29: VAN TASSEL, J. 1990. The semantics of VHDL with VAL and HOL. Tech. Rep. 196, Computer Laboratory, Univ. of Cambridge, Cambridge, UK. June.
• 30: John Van Tassel, A Formalisation of the VHDL Simulation Cycle, Proceedings of the IFIP TC10/WG10.2 Workshop on Higher Order Logic Theorem Proving and its Applications, p.359-374, September 21-24, 1992
• 31: WILSEY, P. 1992. Developing a formal semantic definition of VHDL. In VHDL for Simulation, Synthesis and Formal Proofs of Hardware, J. Mermet, Ed. Kluwer, Amsterdam.
• 32: WORDSWORTH, J. 1992. Software Development with Z. Addison-Wesley, Reading, Mass.

INDEX TERMS

Primary Classification:
  B. Hardware
  B.6 LOGIC DESIGN
      B.6.3 Design Aids
          Subjects: Hardware description languages

Additional Classification:
  B. Hardware
  B.1 CONTROL STRUCTURES AND MICROPROGRAMMING
      B.1.4 Microprogram Design Aids
          Subjects: Languages and compilers

  D. Software
  D.1 PROGRAMMING TECHNIQUES

General Terms:
Design, Languages, Theory, Verification

Keywords:
VHDL, denotational semantics, digital circuits, formal verification, program logic, refinement, timed logic