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

Authors: Katsumi Wasaki, Naoki Iwasaki

Abstract:

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.

Keywords: meta description language, software/hardware codesign, co-verification, formal verification, hardware compiler, modelchecking.

Digital Object Identifier (DOI): doi.org/10.5281/zenodo.1332168

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.