# Checking netlists for equivalence

varun7rs at gmail.com varun7rs at gmail.com
Fri Jul 18 13:53:02 CEST 2014

```Hello Everyone,

I have tried to understand a code but I'm finding it extremely difficult in getting it through my head. I'd be glad if any of you could help me. I understood the parsexml function and I'm trying to understand the rest but finding it very hard. If any of you could spare your valuable time in explaining this code to me,I'd be very grateful and I also can learn a lot from your explanations.
Thank You

import sys
import math
import copy

final_list = []

def sat(cnf):
while( len(cnf) > 1 ):
in_item = single_clause(cnf)
if in_item != None:
del_sat(cnf, in_item)
else:
break

for i in cnf:
if len(i) == 0:
cnf.remove(i)
return

if len(cnf) == 1:
final_list.extend( [cnf[0][0]] )
for i in range(0, len(final_list)):
#print final_list
if final_list[i] > 0:
print final_list[i]
print "Not equivalent!"
sys.exit(0)
return final_list

deep_copy = copy.deepcopy(cnf)
list2 = cnf[0][0]
del_sat(deep_copy,list2)
sat(deep_copy)

del_sat(cnf,-list2)
sat(cnf)
return

def parseXml(file_1, file_2):
global cnf

inputs_1.sort()
inputs_2.sort()

outputs_1.sort()
outputs_2.sort()

inputmap_1 = {}
inputmap_2 = {}
outputmap_1 = []
outputmap_2 = []

while True:
if not line:
break
net,item = line.split()
inputmap_1[item] = int(net)

while True:
if not line:
break
net,item = line.split()
inputmap_2[item] = int(net)

inp1 = line.split()
gate = inp1.pop(0)
mapping = map(int, inp1)
outputmap_1.extend([(gate, mapping)])

inp2 = line.split()
gate = inp2.pop(0)
mapping = map(int, inp2)
outputmap_2.extend([(gate, mapping)])

return inputs_1, inputs_2, outputs_1, outputs_2, inputmap_1, inputmap_2, outputmap_1, outputmap_2

def single_clause(cnf):
for i in cnf:
if len(i) == 1:
return i[0]
return None

def del_sat(cnf,in_item):
cnf2 = cnf[:]
for k in cnf2:
if k.count(in_item):
cnf.remove(k)
for i in cnf:
if i.count( -in_item):
i.remove(-in_item)

def cnf_out(miter):
miter_len = len(miter)
cnf = []
while (miter_len > 0):
x = miter.pop(0)
if ( x[0] == "and" ):
cnf.extend( [[x[1][0], -x[1][2]]] )
cnf.extend( [[x[1][1], -x[1][2]]] )
cnf.extend( [[-x[1][0], -x[1][1], x[1][2]]] )
elif ( x[0] == "or" ):
cnf.extend( [[x[1][0], x[1][1], -x[1][2]]] )
cnf.extend( [[-x[1][0], x[1][2]]] )
cnf.extend( [[-x[1][1], x[1][2]]] )
elif ( x[0] == "xor" ):
cnf.extend( [[x[1][0], x[1][1], -x[1][2]]] )
cnf.extend( [[-x[1][0], -x[1][1], -x[1][2]]] )
cnf.extend( [[-x[1][0], x[1][1], x[1][2]]] )
cnf.extend( [[x[1][0], -x[1][1], x[1][2]]] )
else:
cnf.extend( [[x[1][0], x[1][1]]] )
cnf.extend( [[-x[1][0], -x[1][1]]] )
miter_len = miter_len - 1

return cnf

inputs_1, inputs_2, outputs_1, outputs_2, inputmap_1, inputmap_2, outputmap_1, outputmap_2 = parseXml(sys.argv[1], sys.argv[2])

incoming1=[]
incoming2=[]
outgoing1=[]
outgoing2=[]

for i in inputs_1:
incoming1.extend([inputmap_1[i]])

for j in inputs_2:
incoming2.extend([inputmap_2[j]])

for k in outputs_1:
outgoing1.extend([inputmap_1[k]])

for l in outputs_2:
outgoing2.extend([inputmap_2[l]])

gate_num = 0
for output in outputmap_1:
for j in output[1]:
if gate_num < j:
gate_num = j

map2 = outputmap_2

num = len( map2 )

for i in range(1, num + 1):

j = len( map2[i-1][1] )
for k in range(0, j):
if map2[i-1][1][k] not in incoming2:
total = 0
for l in incoming2:
if map2[i-1][1][k] > l:
total = total + 1
map2[i-1][1][k] = map2[i-1][1][k] + gate_num - total

else:
x = incoming2.index( map2[i-1][1][k] )
map2[i-1][1][k] = incoming1[x]

miter = outputmap_1
miter.extend(map2)

out_len = len(outgoing1)
for i in range(out_len):
total = 0
for j in incoming2:
if outgoing2[i] > j:
total = total + 1
outgoing2[i] = outgoing2[i] + gate_num - total
xor_gate = [( 'xor', [outgoing1[i], outgoing2[i], 9000+i] )]
miter.extend(xor_gate)

if out_len > 1:
or_gate_1 = [( 'or', [9000, 9000+1, 9000 + out_len] )]
miter.extend(or_gate_1)
for i in range(out_len - 2):
or_gate=[( 'or', [9000 + out_len + i, 9000 +i + 2, 9000 + i + out_len + 1] )]
miter.extend(or_gate)

built_cnf = cnf_out(miter)
count = 0
built_len = len(built_cnf)
for i in range(0, built_len):
built_leni = len(built_cnf[i])
for j in range(0, built_leni):
if abs( built_cnf[i][j] ) > count:
count = abs( built_cnf[i][j])

value = sat(built_cnf)
print value
print "Equivalent!"

```