Formal Design Verification of Combinational Circuits Specified by Recurrence Equations (Special Issue on Synthesis and Verification of Hardware Design)
スポンサーリンク
概要
- 論文の詳細を見る
In order to apply formal design verification, it is necessary to describe formally and correctly the specification of the circuit under verification. Especially when we apply conventional OBDD-based logic comparison method for verifying combinational circuits, another "correct" logic circuits or Boolean formulae must be given as the specification. It is desired to develop an efficient automatic design verification method which interprets specification that can be described easier. This paper provides a new verification method which is useful for combinational circuits such as arithmetic circuits. The proposed method efficiently verifies whether a designed circuit satisfies a specification given by recurrence equations. This enables us to describe easily an error-free specification for arithmetic circuits. To perform verification efficiently using an ordinary OBDD package, an efficient truth-value rotation algorithm is developed. The truth-value rotation algorithm efficiently generates an OBDD representing f(x+1 (mod 2^n)) from a given OBDD representing f(x). By experiments on SPARC station 10 model 51, it takes 180 secstion generate an OBDD for designed circuit of 23-bit square function, and additional 60 secs is sufficient to finish verifying that it satisfies the specification given by recurrence equations.
- 社団法人電子情報通信学会の論文
- 1996-10-25
著者
-
YAJIMA Shuzo
Faculty of Information Science, Kyoto University
-
Ochi Hiroyuki
Faculty Of Information Sciences Hiroshima City University
-
Yajima Shuzo
Faculty Of Engineering Kyoto University
関連論文
- Computational Power of Nondeterministic Ordered Binary Decision Diagrams and Their Subclasses (Special Section on Discrete Mathematics and Its Applications)
- Formal Design Verification of Combinational Circuits Specified by Recurrence Equations (Special Issue on Synthesis and Verification of Hardware Design)
- Development of an IP Library of IEEE-754-Standard Single-Precision Floating-Point Dividers(IP Design)(VLSI Design and CAD Algorithms)
- Computational Complexity of Manipulating Binary Decision Diagrams
- On Parallel Computation Time of Unification for Restricted Terms
- On the Computational Power of Binary Decision Diagrams
- Hardware Algorithms and Logic Design Automation : An Overview and Progress Report
- Area-Time Efficient Evaluation of Elementary Functions
- Datapath-Layout-Driven Design for Low-Power Standard-Cell LSI Implementation(Special Section on VLSI Design and CAD Algorithms)
- Exponential Lower Bounds on the Size of Variants of OBDD Representing Integer Division
- Compaction of Test Sets for Combinatinal Circuits Based on Symbolic Fault Simulation (Special Issue on Synthesis and Verification of Hardware Design)