A Meta Hardware Description Language Melasy for Model-Checking Systems

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 t...

Full description

Saved in:
Bibliographic Details
Main Authors: Iwasaki, N., Wasaki, K.
Format: Conference Proceeding
Language:English
Subjects:
Algorithm design and analysis
Circuits
Costs
Design engineering
Design-for-test
Digital systems
Hardware Compilers
Hardware design languages
Hardware/Software co-design and co-verification
Haskell
High level languages
Information technology
Maintenance
Model Checking
Safety
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
DOI:10.1109/ITNG.2008.135