An Algebraic Approach to the VERILOG Programming

  • He Jifeng
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2757)


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.


Operational Semantic Algebraic Approach Input Event Algebraic Semantic Left Zero 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Bawankule, R.: Alternative Verilog FAQ (1997–1999),
  2. 2.
    Brock, B.C., Hunt, W.A.: Formal Analysis of the Motorola CAP DSP?. In: Industrial-strength Formal Methods in Practice, pp. 81–116 (1999)Google Scholar
  3. 3.
    Bowen, J.: Animating the Semantics of VERILOG using Prolog. UNU/IIST technical Report 176 (1999)Google Scholar
  4. 4.
    Bowen, J.P., Hinchey, M.G.: High-Integrity System Specification and Design. Springer, Heidelberg (1999)Google Scholar
  5. 5.
    Delgado Kloos, C., Breuer, P.T. (eds.): Formal Semantics for VHDL. Kluwer Academic Publishers, Dordrecht (1995)MATHGoogle Scholar
  6. 6.
    Golze, U.: VLSI Chip Design with Hardware Description Language VERILOG. Springer, Heidelberg (1996)Google Scholar
  7. 7.
    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)Google Scholar
  8. 8.
    Gordon, M.: Event and Cyclic Semantics of Hardware Description Languages Technical Report of the VERILOG Formal Equivalence Project of Cambridge Computing Laboratory (1995)Google Scholar
  9. 9.
    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)CrossRefGoogle Scholar
  10. 10.
    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)Google Scholar
  11. 11.
    Jifeng, H.: A Common Framework for Mixed Hardware/Software Systems. In: Proceedings of IFM 1999, pp. 1–25. Springer, Heidelberg (1999)Google Scholar
  12. 12.
    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)Google Scholar
  13. 13.
    Jifeng, H., Qiwen, X.: An Operational Semantics of a Simulator Algorithm. In: Proceedings of PDPTA 2000, pp. 203–209 (2000)Google Scholar
  14. 14.
    Jifeng, H.: An Integrated Approach to Hardware/Software Co-design. In: Proceedings of 16th World Computer Congress 2000, pp. 5–19 (2000)Google Scholar
  15. 15.
    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)Google Scholar
  16. 16.
    Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)MATHGoogle Scholar
  17. 17.
    Hoare, C.A.R., Jifeng, H.: Unifying Theories of Programming. Prentice-Hall, Englewood Cliffs (1998)Google Scholar
  18. 18.
    IEEE Standard VHDL Language Reference Manual. IEEE Standard 1076-1993, URL:
  19. 19.
    IEEE Standard Hardware Description Language Based on the VERILOG Hardware Description Language. IEEE Standard 1364-1995, URL:
  20. 20.
    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)Google Scholar
  21. 21.
    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)Google Scholar
  22. 22.
    Jian, L.Y., Jifeng, H.: Formalising Verilog. In: Proceedings of the International Conference on Applied Informatics (AI 2001), Innsbruck, Austria (2001)Google Scholar
  23. 23.
    Open VERILOG International (OVI). VERILOG Hardware Description Language Reference Manual. Version 1 (1994)Google Scholar
  24. 24.
    Shengchao, Q., Jifeng, H.: An Algebraic Approach to Hardware/Software Partitioning. In: Proceedings of ICECS2000, pp. 273–277 (2000)Google Scholar
  25. 25.
    Thomas, D.E., Moorby, P.: The VERILOG Hardware Description Language. Kluwer Publisher, Dordrecht (1991)Google Scholar
  26. 26.
    Tran, V.D., Jifeng, H.: A Theory of Combinational Programs. In: Proceedings of APSEC2001 (2001)Google Scholar
  27. 27.
    Wirth, N.: Hardware Compilation: Translating Programs into Circuits. IEEE Computer 31(6), 25–31 (1998)Google Scholar
  28. 28.
    Huibiao, Z., Bowen, J., Jifeng, H.: Deriving Operational Semantics from Denotational Semantics for Verilog. In: CHARME 2001. LNCS, vol. 2144 (2001)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • He Jifeng
    • 1
  1. 1.United Nations University International Institute For Software TechnologyMacau

Personalised recommendations