Fifth International Conference on Information Technology: New Generations (itng 2008) A Meta Hardware Description Language Melasy for Model-Checking Systems April 07-April 09 ISBN: 978-0-7695-3099-4
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/ITNG.2008.135
Model-checking tools such as Symbolic Model Verifier (SMV) and NuSMVare 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.
Index Terms:
Hardware Compilers, Model Checking, Design-for-test, Hardware/Software co-design and co-verification, Haskell
Citation:
Naoki Iwasaki, Katsumi Wasaki, "A Meta Hardware Description Language Melasy for Model-Checking Systems," itng, pp.273-278, Fifth International Conference on Information Technology: New Generations (itng 2008), 2008 Usage of this product signifies your acceptance of the Terms of Use. | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb