Development of A Meta Description Language for Software/Hardware Cooperative Design and Verification for Model-Checking Systems

Model-checking tools such as Symbolic Model Verifier (SMV) and NuSMV are available for checking hardware designs. These tools can automatically check the formal legitimacy of a design. However, NuSMV is too low level for describing a complete hardware design. It is therefore necessary to translate the system definition, as designed in a language such as Verilog or VHDL, into a language such as NuSMV for validation. In this paper, we present a meta hardware description language, Melasy, that contains a code generator for existing hardware description languages (HDLs) and languages for model checking that solve this problem.

Authors:

• Katsumi Wasaki
• Naoki Iwasaki

Keywords:

• meta description language
• software/hardware codesign
• co-verification
• formal verification
• hardware compiler
• modelchecking.

References:

[1] N. Wirth. Digital Circuit Design. Springer, New York, NY, USA, 1985.
[2] Y. N. Patt, S. J. Patel, M. Evers, D. H. Friendly, and J. Stark. One billion
transistors, one uniprocessor, one chip. IEEE Computer, 30(9):51-57,
1997.
[3] A. V. Aho and J. D. Ullman. Principles of Compiler Design. Addison
Wesley, Boston, MA, USA, 1977.
[4] A. V. Aho, R. Sethi, and J. D. Ullman. Compilers: Principles,
Techniques, and Tools. Addison Wesley, Boston, MA, USA, 1986.
[5] H. Trickey. Flamel: A high-level hardware compiler. IEEE Trans. on
Comp.-Aided Design of Int. Circ. and Sys., 6(2):259-269, 1987.
[6] IEEE. VHDL (VHSIC Hardware Description Language). IEEE Design
Automation Standards Committee, 1076, 2002.
[7] D. E. Thomas and P. R. Moorby. The Verilog(r) Hardware Description
Language. Kluwer Academic Publishers, Norwell, MA, USA, 2002.
[8] T. Grotker. System Design with System-C. Kluwer Academic Publishers,
Norwell, MA, USA, 2002.
[9] E. M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press,
Boston, MA, USA, 2000.
[10] K. L. McMillan. The SMV system (Symbolic Model Verifier). Cadence
Berkeley Labs, Berkeley, CA, USA, 1999.
[11] A. Cimatti, E. M. Clarke, F. Giunchiglia, and M. Roveri. Nusmv: A new
symbolic model verifier. In Proc. of 11th Conference on Computer-Aided
Verification (CAV-99), pages 495-499, 1999.
[12] S. P. Jones, C. V. Hall, K. Hammond, and W. Partain. The glasgow
haskell compiler: A technical overview. In Proc. of the Joint Framework
for Information Technology Technical Conference, 1993.
[13] D. Leaden and E. Meier. Parsec: Direct style monadic parser combinatory
for the real world. Technical report, EU-CS-2001-35, Utrecht
University, Netherlands, 2001.
[14] HDCaml. http://www.confluent.org/wiki/doku.php/hdcaml.
[15] Confluence. http://www.confluent.org/wiki/doku.php/confluence.