Formal verification of word-level specifications
Formal verification of word-level specifications
复制标题
字级规范的形式验证
DOI：
10.1109/date.1999.761096
复制
发表时间：
1999
期刊：
影响因子：
--
通讯作者：
R. Drechsler
中科院分区：
文献类型：
--
作者：
Stefan Höreth;R. Drechsler
形式化验证已成为电路设计中最重要的步骤之一。在这种情况下，验证高级硬件描述语言（HDL），如VHDL，变得越来越重要。在本文中，我们提出了一套完整的数据路径操作，可以正式验证基于字级决策图（WLDD）。我们的技术允许HDL结构直接翻译为WLDD。我们提出了新的算法WLDD的模运算和除法。这些行动使我们成为有效核查程序的核心。此外，我们证明了上界的表示大小的WLDD保证算法的有效性。我们的验证工具是完全自动的，实验结果证明了我们的方法的效率。
Formal verification has become one of the most important steps in circuit design. In this context the verification of high-level Hardware Description Languages (HDLs), like VHDL, becomes increasingly important. In this paper we present a complete set of datapath operations that can be formally verified based on Word-Level Decision Diagrams (WLDDs). Our techniques allow a direct translation of HDL constructs to WLDDs. We present new algorithms for WLDDs for modulo operation and division. These operations turn our to be the core of our efficient verification procedure. Furthermore, we prove upper bounds on the representation size of WLDDs guaranteeing effectiveness of the algorithms. Our verification tool is totally automatic and experimental results are given to demonstrate the efficiency of our approach.