Formal Design Verification of Combinational Circuits Specified by Recurrence Equations

Hiroyuki OCHI, Shuzo YAJIMA

Summary :

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 truthvalue rotation algorithm efficiently generates an OBDD representing f(x + 1 (mod 2ⁿ)) from a given OBDD representing f(x). By experiments on SPARC station 10 model 51, it takes 180 secs to 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.

• Publication: IEICE TRANSACTIONS on Information Vol.E79-D No.10 pp.1431-1435
• Publication Date: 1996/10/25
• Type of Manuscript: Special Section PAPER (Special Issue on Synthesis and Verification of Hardware Design)
• Category: Design Verification

Authors

Hiroyuki OCHI
Shuzo YAJIMA

Keyword

formal design verification,  binary decision diagram,  arithmetic circuits,  specification,  recurrence equations