Excellence in Research and Innovation for Humanity

Katsumi Wasaki

Publications

1

Publications

1
4385
Development of A Meta Description Language for Software/Hardware Cooperative Design and Verification for Model-Checking Systems
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.