Verifying VHDL Designs with Multiple Clocks in SMV

Investor logo
Investor logo

Warning

This publication doesn't include Faculty of Economics and Administration. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

SMRČKA Aleš ŘEHÁK Vojtěch VOJNAR Tomáš ŠAFRÁNEK David MATOUŠEK Petr ŘEHÁK Zdeněk

Year of publication 2007
Type Article in Proceedings
Conference Formal Methods Applications and Technology, 11th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2006, and 5th International Workshop on Parallel and Distributed Methods in Verification, PDMC 2006
MU Faculty or unit

Faculty of Informatics

Citation
Field Informatics
Keywords formal verification; model checking; VHDL; asynchronous clock domains
Description The paper considers the problem of model checking real-life VHDL- based hardware designs via their automated transformation to a model verifiable using the SMV model checker. In particular, model checking of asynchronous designs, i.e. designs driven by multiple clocks, is discussed. Two original approaches to compiling asynchronous VHDL designs to the SMV language such that errors possibly arising from the asynchronicity are preserved are proposed. The paper also presents results of experiments with using the proposed methods for verification of several real-life asynchronous components of an FPGA-based router being developed within the Liberouter project.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.