satcomp07.benchmark-description.jarvisalo

Description

Equivalence checking hardware multiplier designs⁄Matti J˜arvisalobAbstract o is enforced by introducing gateseq a bWe generate SAT benchmarks encoding the o = equiv(o ;o )i i iproblem of equivalence checking two difierentfor i=1:::2n.industrial hardware designs for integer multipli-cation.† As a single output gate introduceeq eqout= and(o ;:::;o ):1 2n1 Problem† Constrain out to 0 (false).Our goal is to generate interesting SAT bench-marks based on real-life hardware designs. WeSince the multiplier designs produce equivalentconsider the problem of checking whether tworesultsforanytwomultiplicants,wearriveatandifierent hardware designs for integer multipli-unsatisflable equivalence checking instance.cationareequivalentinthesensethatbothpro-The Boolean circuit descriptions of the mul-duce the same output on all inputs.tiplier designs are produced by the genfacbmThe designs we use are the adder tree andgenerator [7] for SAT benchmarks based on in-Braun multipliers[1]. Foraflxed n, bothmulti-tegerfactoringinthe BCSatBooleancircuitfor-plierstakeasinputtwointegersa=(a ;:::;a )1 nmat [3], see [6] for details.and b = (b ;:::;b ) in binary, and output1 nthe product o = (o ;:::;o ). Both designs1 2n2consist of O(n ) gates, using nots and binary 2 CNF Encodingands, ors, and xors. The propagation delays(maxmax height from inputs to outputs) are For the CNF encoding, we apply the bc2cnfO(n) for Braun, and O(log(nlogn)) for adder Boolean circuit simplifler/clausifler ...

Informations

• Publié par: Vewyir
• Nombre de lectures: 12
• Langue: English

Extrait

Equivalence checking hardware multiplier designs

∗ MattiJ¨arvisalo

b Abstract ois enforced by introducing gates eq a b We generate SAT benchmarks encoding the o=equiv(o ,o) i ii problem of equivalence checking two different fori= 1. . .2n. industrial hardware designs for integer multipli- cation. •As a single output gate introduce eq eq out=and(. . . , oo ,). 1 2n 1 Problem Our goal is to generate interesting SAT bench- •Constrainoutto 0 (false). marks based on real-life hardware designs.We Since the multiplier designs produce equivalent consider the problem of checking whether two results for any two multiplicants, we arrive at an different hardware designs for integer multipli- unsatisfiableequivalence checking instance. cation are equivalent in the sense that both pro- The Boolean circuit descriptions of the mul- duce the same output on all inputs. tiplier designs are produced by thegenfacbm The designs we use are theadder treeand generator [7] for SAT benchmarks based on in- BraunFor a fixedmultipliers [1].n, both multi- teger factoring in theBCSatBoolean circuit for- pliers take as input two integersa= (a 1 , . . . , a n ) mat [3], see [6] for details. andb= (b 1 , . . . , b n ) in binary, and output the producto= (o 1 , . . . , o 2n designs). Both 2 consist ofO(n) gates, usingnots and binary 2 CNFEncoding ands,ors, andxors. Thepropagation delays (max maxheight from inputs to outputs) are For the CNF encoding, we apply thebc2cnf O(n) for Braun, andO(log(nlogn)) for adder Boolean circuit simplifier/clausifier [4].The tree. WhileBraun consists of a grid of full- bc2cnftool applies structure sharing and simpli- adders, adder tree applies adders in a tree-like fication (Boolean propagation, cone-of-influence fashion, summing up partial products. reduction, monotone input gate rule) techniques We will construct a Boolean circuit describ- to the circuit, and translates the simplified cir- ing an instance of the equivalence checking prob- cuit into CNF in a standard waya laTseitin [8] lem for givenn-bit adder tree (output bits (however,nots are interpreted as negated liter- a aa o= (. . . , oo ,)) and Braun multipliers (out- 1 2n als). Thisresults in a linear translation with b bb put bitso= (. . . , oo ,)) as follows: 1 2n respect to the simplified circuit. •The inputs of the multipliers are made equivalent by sharing the input gates 3 Instances a 1 , . . . , a n , b 1 , . . . , b n . The following set of benchmarks are available at •No other gates are shared between the multiplier circuits. http://www.tcs.hut.fi/~mjj/benchmarks/. a •Bit-wise equivalence of the outputsoand •eq.atree.braun.[n].unsat.cnf unsatisfiable instances for multiplicant ∗ Address: HelsinkiUniversity of Technology, Laboratory for Theoretical Computer Science, bit-widthsn= 7. . .13 P.O. Box 5400, FI-02015 TKK, Finland.Email: [e-mail].

1