Checking netlists for equivalence
varun7rs at gmail.com
varun7rs at gmail.com
Fri Jul 18 07:53:02 EDT 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
readfile_1 = open(file_1, "r")
readfile_2 = open(file_2, "r")
sum_a = int(readfile_1.readline())
sum_b = int(readfile_2.readline())
inputs_1 = readfile_1.readline().split()
inputs_1.sort()
inputs_2 = readfile_2.readline().split()
inputs_2.sort()
outputs_1 = readfile_1.readline().split()
outputs_1.sort()
outputs_2 = readfile_2.readline().split()
outputs_2.sort()
inputmap_1 = {}
inputmap_2 = {}
outputmap_1 = []
outputmap_2 = []
while True:
line = readfile_1.readline().strip()
if not line:
break
net,item = line.split()
inputmap_1[item] = int(net)
while True:
line = readfile_2.readline().strip()
if not line:
break
net,item = line.split()
inputmap_2[item] = int(net)
for line in readfile_1.readlines():
inp1 = line.split()
gate = inp1.pop(0)
mapping = map(int, inp1)
outputmap_1.extend([(gate, mapping)])
for line in readfile_2.readlines():
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!"
More information about the Python-list
mailing list