f(x + 1 (mod 2n)) 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." />


Formal Design Verification of Combinational Circuits Specified by Recurrence Equations

Hiroyuki OCHI  Shuzo YAJIMA  

Publication
IEICE TRANSACTIONS on Information and Systems   Vol.E79-D   No.10   pp.1431-1435
Publication Date: 1996/10/25
Online ISSN: 
DOI: 
Print ISSN: 0916-8532
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>>
Buy this Article




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 2n)) 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.