Abstract
The semantics of a hardware description language is usually given in terms of how a simulator should behave. This paper adopts a different strategy by first listing a collection of equational laws expressing algebraic properties of VERILOG programs. It outlines some techniques of formal derivation of operational model and denotational presentation of the language VERILOG from its algebraic definition.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Bawankule, R.: Alternative Verilog FAQ (1997–1999), http://www.angelfire.com/in/verilogfaq/
Brock, B.C., Hunt, W.A.: Formal Analysis of the Motorola CAP DSP?. In: Industrial-strength Formal Methods in Practice, pp. 81–116 (1999)
Bowen, J.: Animating the Semantics of VERILOG using Prolog. UNU/IIST technical Report 176 (1999)
Bowen, J.P., Hinchey, M.G.: High-Integrity System Specification and Design. Springer, Heidelberg (1999)
Delgado Kloos, C., Breuer, P.T. (eds.): Formal Semantics for VHDL. Kluwer Academic Publishers, Dordrecht (1995)
Golze, U.: VLSI Chip Design with Hardware Description Language VERILOG. Springer, Heidelberg (1996)
Gordon, M.: The Semantic Challenge of VERILOG HDL. In: The proceedings of Tenth Annual IEEE Symposium on Logic in Computer Science (LICS 1995), San Diego, California (1995)
Gordon, M.: Event and Cyclic Semantics of Hardware Description Languages Technical Report of the VERILOG Formal Equivalence Project of Cambridge Computing Laboratory (1995)
Jifeng, H., Page, I., Bowen, J.P.: Towards a Provably Correct Hardware Implementation of Occam. In: Milne, G.J., Pierre, L. (eds.) CHARME 1993. LNCS, vol. 683, pp. 214–225. Springer, Heidelberg (1993)
Jifeng, H.: A Behavioural Model For Co-design. In: Woodcock, J.C.P., Davies, J., Wing, J.M. (eds.) FM 1999. LNCS, vol. 1709, p. 1420. Springer, Heidelberg (1999)
Jifeng, H.: A Common Framework for Mixed Hardware/Software Systems. In: Proceedings of IFM 1999, pp. 1–25. Springer, Heidelberg (1999)
Jifeng, H., Qiwen, X.: An Advance Features of DC and their applications. In: Davies, J., Roscoe, B., Woodcock, J. (eds.) Millennial Perspective in Computer Science, pp. 133–147 (1999)
Jifeng, H., Qiwen, X.: An Operational Semantics of a Simulator Algorithm. In: Proceedings of PDPTA 2000, pp. 203–209 (2000)
Jifeng, H.: An Integrated Approach to Hardware/Software Co-design. In: Proceedings of 16th World Computer Congress 2000, pp. 5–19 (2000)
Jifeng, H.: Formalising VERILOG. In: Proceedings of the 7th IEEE International Conference on Electronics, Circuits and Systems (ICECS 2000), pp. 412–416, IEEE Catelog number: 00EX445 (2000)
Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)
Hoare, C.A.R., Jifeng, H.: Unifying Theories of Programming. Prentice-Hall, Englewood Cliffs (1998)
IEEE Standard VHDL Language Reference Manual. IEEE Standard 1076-1993, URL: http://www.ieee.org/catalog/design.html#1076-1993
IEEE Standard Hardware Description Language Based on the VERILOG Hardware Description Language. IEEE Standard 1364-1995, URL: http://standards.ieee.org/catalog/design/html#1364-1995
Iyoda, J., Sampaio, A., Silva, L.: ParTS: A Partitioning Transformation System. In: Woodcock, J.C.P., Davies, J., Wing, J.M. (eds.) FM 1999. LNCS, vol. 1709, p. 1400. Springer, Heidelberg (1999)
Iyoda, J., Jifeng, H.: Towards an Algebraic Synthesis of Verilog. In: Proceedings of the 2001 International Conference on Engineering of Reconfigurable systems and algorithms (ERSA 2001), Las Vegas, USA, pp. 15–21 (2001)
Jian, L.Y., Jifeng, H.: Formalising Verilog. In: Proceedings of the International Conference on Applied Informatics (AI 2001), Innsbruck, Austria (2001)
Open VERILOG International (OVI). VERILOG Hardware Description Language Reference Manual. Version 1 (1994)
Shengchao, Q., Jifeng, H.: An Algebraic Approach to Hardware/Software Partitioning. In: Proceedings of ICECS2000, pp. 273–277 (2000)
Thomas, D.E., Moorby, P.: The VERILOG Hardware Description Language. Kluwer Publisher, Dordrecht (1991)
Tran, V.D., Jifeng, H.: A Theory of Combinational Programs. In: Proceedings of APSEC2001 (2001)
Wirth, N.: Hardware Compilation: Translating Programs into Circuits. IEEE Computer 31(6), 25–31 (1998)
Huibiao, Z., Bowen, J., Jifeng, H.: Deriving Operational Semantics from Denotational Semantics for Verilog. In: CHARME 2001. LNCS, vol. 2144 (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Jifeng, H. (2003). An Algebraic Approach to the VERILOG Programming. In: Aichernig, B.K., Maibaum, T. (eds) Formal Methods at the Crossroads. From Panacea to Foundational Support. Lecture Notes in Computer Science, vol 2757. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-40007-3_5
Download citation
DOI: https://doi.org/10.1007/978-3-540-40007-3_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20527-2
Online ISBN: 978-3-540-40007-3
eBook Packages: Springer Book Archive