Verification of arithmetic circuits by comparing two similar circuits

Recently there have been a lot of progress in technologies for comparing two structurally similar large circuits [2, 14, 13]. Circuits having more than 10,000 gates, whose BDD cannot be built, have been verified in several minutes. However, arithmetic circuit verification with respect to specification is still a hard problem. As shown in [16] some arithmetic circuits, such as multipliers, square function. cube functions, etc., must satisfy some recurrence equations, such as f(x + 1,y=f(x,y) + y where f(x,y)=xy, and those equations can be used for verification. In this paper, we use such recurrence equations in order to drive Boolean comparison problems of structurally similar circuits. That is, left hand sides and right hand sides of equations are realized as separated circuits and then compared. Using the recurrence equation properly, these circuits have many internal equivalent signals and many implications among signals, by which Boolean comparison programs, such as [2, 14, 13], can work very effectively. Using the proposed method, 16-bit multipliers, such as C6288 of ISCAS85 benchmark circuits, are verified within 12 minutes.