WASET
	%0 Journal Article
	%A Katsumi Wasaki and  Naoki Iwasaki
	%D 2008
	%J International Journal of Computer and Information Engineering
	%B World Academy of Science, Engineering and Technology
	%I Open Science Index 18, 2008
	%T Development of A Meta Description Language for Software/Hardware Cooperative Design and Verification for Model-Checking Systems
	%U https://publications.waset.org/pdf/4385
	%V 18
	%X 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.
	%P 1807 - 1811