Automated formal verification for VHDL designs

被引:0
|
作者
Lin, FY
Li, HC
机构
关键词
D O I
暂无
中图分类号
TP39 [计算机的应用];
学科分类号
081203 ; 0835 ;
摘要
We present an approach to employ symbolic model checker (SMV) to model and verify VHDL specifications. This formalism, although mathematically simple, can model most of the properties of the finite transition system, and so play an important role in the study of their semantics. Hardware can be formally verified by describing both the specification and implementation using VHDL and SMV.
引用
收藏
页码:174 / 177
页数:4
相关论文
共 50 条
  • [1] Formal specification and verification of VHDL
    Bickford, M
    Jamsek, D
    FORMAL METHODS IN COMPUTER-AIDED DESIGN, 1996, 1166 : 310 - 326
  • [2] Formal specification in VHDL for hardware verification
    Reetz, R
    Schneider, K
    Kropf, T
    DESIGN, AUTOMATION AND TEST IN EUROPE, PROCEEDINGS, 1998, : 257 - 263
  • [3] Automated correctness condition generation for formal verification of synthesized RTL designs
    Mansouri, N
    Vemuri, R
    FORMAL METHODS IN SYSTEM DESIGN, 2000, 16 (01) : 59 - 91
  • [4] Tool Chain to Support Automated Formal Verification of Avionics Simulink Designs
    Barnat, Jiri
    Beran, Jan
    Brim, Lubos
    Kratochvila, Tomas
    Rockai, Petr
    FORMAL METHODS FOR INDUSTRIAL CRITICAL SYSTEMS (FMICS 2012), 2012, 7437 : 78 - 92
  • [5] Automated Correctness Condition Generation for Formal Verification of Synthesized RTL Designs
    Nazanin Mansouri
    Ranga Vemuri
    Formal Methods in System Design, 2000, 16 : 59 - 91
  • [6] FORMAL VERIFICATION OF VHDL DESCRIPTIONS IN THE PREVAIL ENVIRONMENT
    BORRIONE, DD
    PIERRE, LV
    SALEM, AM
    IEEE DESIGN & TEST OF COMPUTERS, 1992, 9 (02): : 42 - 56
  • [7] VHDL DESCRIPTION AND FORMAL VERIFICATION OF SYSTOLIC MULTIPLIERS
    PIERRE, L
    COMPUTER HARDWARE DESCRIPTION LANGUAGES AND THEIR APPLICATIONS, 1993, 32 : 225 - 242
  • [8] Products/news: VHDL support for formal verification
    Computer Design, 1997, 36 (05):
  • [9] Formal verification of VHDL - The model checker CV
    Deharbe, D
    Shankar, S
    Clarke, EM
    XI BRAZILIAN SYMPOSIUM ON INTEGRATED CIRCUIT DESIGN, PROCEEDINGS, 1998, : 95 - 98
  • [10] Improving a Design Methodology of Synthesizable VHDL With Formal Verification
    Perpetuo Costa Marques, Luis Gustavo
    de Queiroz, Max Hering
    Farines, Jean-Marie
    2016 IEEE 7TH LATIN AMERICAN SYMPOSIUM ON CIRCUITS & SYSTEMS (LASCAS), 2016, : 51 - 54