
For FullText PDF, please login, if you are a member of IEICE,
or go to Pay Per View on menu list, if you are a nonmember of IEICE.

Formal Design Verification of Combinational Circuits Specified by Recurrence Equations
Hiroyuki OCHI Shuzo YAJIMA
Publication
IEICE TRANSACTIONS on Information and Systems
Vol.E79D
No.10
pp.14311435 Publication Date: 1996/10/25
Online ISSN:
DOI:
Print ISSN: 09168532 Type of Manuscript: Special Section PAPER (Special Issue on Synthesis and Verification of Hardware Design) Category: Design Verification Keyword: formal design verification, binary decision diagram, arithmetic circuits, specification, recurrence equations,
Full Text: PDF>>
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 OBDDbased 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 errorfree specification for arithmetic circuits. To perform verification efficiently using an ordinary OBDD package, an efficient truthvalue rotation algorithm is developed. The truthvalue 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 secs to generate an OBDD for designed circuit of 23bit square function, and additional 60 secs is sufficient to finish verifying that it satisfies the specification given by recurrence equations.

