satcomp07.benchmark-description.jarvisalo

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 ...