Checking netlists for equivalence

[varun7rs at gmail.com]

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!"