Date Added: Jun 2009
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, the authors 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.