luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

post-HWMCC13 changes to par.py

This commit is contained in:
Baruch Sterin 2013-10-08 17:15:06 -07:00
parent 88f75c00ad
commit e0de796242
1 changed files with 100 additions and 80 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

180
scripts/par.py
View File

@ -78,7 +78,7 @@ cex_list = []
TERM = 'USL' TERM = 'USL'
last_gasp_time = 10000 last_gasp_time = 10000
last_gasp_time = 500 last_gasp_time = 500
last_gasp_time = 900 #set to conform to hwmcc12 last_gasp_time = 2001 #set to conform to hwmcc12
use_pms = True use_pms = True
#gabs = False #use the gate refinement method after vta #gabs = False #use the gate refinement method after vta
@ -250,10 +250,10 @@ def initialize():
cex_list = [] cex_list = []
n_pos_before = n_pos() n_pos_before = n_pos()
n_pos_proved = 0 n_pos_proved = 0
abs_time = 150 abs_time = 150 #timeout for abstraction
abs_ref_time = 50 #number of sec. allowed for abstraction refinement. abs_ref_time = 50 #number of sec. allowed for abstraction refinement.
total_spec_refine_time = 150 total_spec_refine_time = 150 # timeout for speculation refinement
abs_ratio = .5 abs_ratio = .5
hist = [] hist = []
skip_spec = False skip_spec = False
t_iter_start = 0 t_iter_start = 0
@ -377,14 +377,16 @@ def set_engines(N=0):
""" """
global reachs,pdrs,sims,intrps,bmcs,n_proc,abs_ratio,ifbip,bmcs1, if_no_bip, allpdrs,allbmcs global reachs,pdrs,sims,intrps,bmcs,n_proc,abs_ratio,ifbip,bmcs1, if_no_bip, allpdrs,allbmcs
bmcs1 = [9] #BMC3 bmcs1 = [9] #BMC3
#for HWMCC we want to set N = 8 ## #for HWMCC we want to set N = 8
N = 8 ## N = 8
if N == 0: if N == 0:
N = n_proc = 1+os.sysconf(os.sysconf_names["SC_NPROCESSORS_ONLN"]) N = n_proc = 1+os.sysconf(os.sysconf_names["SC_NPROCESSORS_ONLN"])
## N = n_proc = 8 ### simulate 4 processors for HWMCC - turn this off a hwmcc. ## N = n_proc = 8 ### simulate 4 processors for HWMCC - turn this off a hwmcc.
else: else:
n_proc = N n_proc = N
## print 'n_proc = %d'%n_proc ## print 'n_proc = %d'%n_proc
#strategy is to use 2x number of processors
N = n_proc = -1+2*N
if N <= 1: if N <= 1:
reachs = [24] reachs = [24]
pdrs = [7] pdrs = [7]
@ -733,6 +735,7 @@ def set_max_bmc(b):
report_bmc_depth(max_bmc) report_bmc_depth(max_bmc)
def report_bmc_depth(m): def report_bmc_depth(m):
return #for non hwmcc applications
print 'u%d'%m print 'u%d'%m
def print_circuit_stats(): def print_circuit_stats():
@ -941,7 +944,7 @@ def simplify(M=0,N=0):
print '\n' print '\n'
return get_status() return get_status()
def simulate2(t=900): def simulate2(t=2001):
"""Does rarity simulation. Simulation is restricted by the amount """Does rarity simulation. Simulation is restricted by the amount
of memory it might use. At first wide but shallow simulation is done, followed by of memory it might use. At first wide but shallow simulation is done, followed by
successively more narrow but deeper simulation. successively more narrow but deeper simulation.
@ -966,7 +969,7 @@ def simulate2(t=900):
if ((time.clock()-btime) > t): if ((time.clock()-btime) > t):
return 'UNDECIDED' return 'UNDECIDED'
def simulate(t=900): def simulate(t=2001):
abc('&get') abc('&get')
result = eq_simulate(t) result = eq_simulate(t)
return result return result
@ -2094,7 +2097,7 @@ def speculate(t=0):
write_file('spec') write_file('spec')
return Undecided_reduction return Undecided_reduction
def simple_sat(t=900): def simple_sat(t=2001):
""" """
aimed at trying harder to prove SAT aimed at trying harder to prove SAT
""" """
@ -2455,7 +2458,7 @@ def dsat_all(t=100,c=100000):
break break
print 'Total time = %0.2f'%(time.time() - ttt) print 'Total time = %0.2f'%(time.time() - ttt)
def check_sat(t=900): def check_sat(t=2001):
"""This is called if all the FF have disappeared, but there is still some logic left. In this case, """This is called if all the FF have disappeared, but there is still some logic left. In this case,
the remaining logic may be UNSAT, which is usually the case, but this has to be proved. The ABC command 'dsat' is used fro combinational problems""" the remaining logic may be UNSAT, which is usually the case, but this has to be proved. The ABC command 'dsat' is used fro combinational problems"""
global smp_trace global smp_trace
@ -3659,7 +3662,7 @@ def unmap_cex():
## print 'cex matches original aig' ## print 'cex matches original aig'
def sp(n=0,t=900,check_trace=False): def sp(n=0,t=2001,check_trace=False):
"""Alias for super_prove, but also resolves cex to initial aig""" """Alias for super_prove, but also resolves cex to initial aig"""
global initial_f_name global initial_f_name
print 'Executing super_prove' print 'Executing super_prove'
@ -3797,7 +3800,7 @@ def remove_v(ss,v):
s = s + [ss[i]] s = s + [ss[i]]
return s return s
def multi_prove(op='simple',tt=900,n_fast=0, final_map=[]): def multi_prove(op='simple',tt=2001,n_fast=0, final_map=[]):
"""two phase prove process for multiple output functions""" """two phase prove process for multiple output functions"""
global max_bmc, init_initial_f_name, initial_f_name,win_list, last_verify_time global max_bmc, init_initial_f_name, initial_f_name,win_list, last_verify_time
global f_name_save,nam_save,_L_last,file_out global f_name_save,nam_save,_L_last,file_out
@ -3809,7 +3812,7 @@ def multi_prove(op='simple',tt=900,n_fast=0, final_map=[]):
#handle single output case differently #handle single output case differently
_L_last = [-1]*n_pos() _L_last = [-1]*n_pos()
if n_pos() == 1: if n_pos() == 1:
result = sp(2000) result = sp(2001)
## abc('w %s_unsolved.aig'%init_initial_f_name) ## abc('w %s_unsolved.aig'%init_initial_f_name)
rs=result[0] rs=result[0]
if rs == 'SAT': if rs == 'SAT':
@ -3825,6 +3828,7 @@ def multi_prove(op='simple',tt=900,n_fast=0, final_map=[]):
L = [2] L = [2]
res = sumsize(L) res = sumsize(L)
rr = '\n@@@@ Time = %d '%(time.time() - t_iter_start) + res rr = '\n@@@@ Time = %d '%(time.time() - t_iter_start) + res
rr = '%s: '%init_initial_f_name + rr
print rr print rr
file_out.write(rr+ '\n') file_out.write(rr+ '\n')
file_out.flush() file_out.flush()
@ -3841,6 +3845,7 @@ def multi_prove(op='simple',tt=900,n_fast=0, final_map=[]):
rr = '\n@@@@ Time = %.2f: '%(time.time() - t_iter_start) rr = '\n@@@@ Time = %.2f: '%(time.time() - t_iter_start)
report_L(lst0,0) ########## report_L(lst0,0) ##########
rr = rr + res rr = rr + res
rr = '%s: '%init_initial_f_name + rr
print rr print rr
file_out.write(rr + '\n') file_out.write(rr + '\n')
file_out.flush() file_out.flush()
@ -3858,14 +3863,14 @@ def multi_prove(op='simple',tt=900,n_fast=0, final_map=[]):
## print S,lst1 ## print S,lst1
#put 0 values into lst0 #put 0 values into lst0
lst10 = indices(s,0) #new unsat POs in local indices (with lst0 removed) lst10 = indices(s,0) #new unsat POs in local indices (with lst0 removed)
if not lst10 == []: ## if not lst10 == []:
print 'lst10 = %s'%str(lst10) ## print 'lst10 = %s'%str(lst10)
lst11 = indices(s,1) #local variables lst11 = indices(s,1) #local variables
ss = expand(s,lst0,0) #ss will reflect original indices ss = expand(s,lst0,0) #ss will reflect original indices
report_s(ss) report_s(ss)
lst0_old = lst0 lst0_old = lst0
lst0 = indices(ss,0) #additional unsat POs added to initial lst0 (in original indices) lst0 = indices(ss,0) #additional unsat POs added to initial lst0 (in original indices)
print 'lst0 = %s'%str(lst0) ## print 'lst0 = %s'%str(lst0)
assert len(lst0) == len(lst0_old)+len(lst10), 'lst0 = %s, lst0_old = %s, lst10 = %s'%(str(lst0),str(lst0_old),str(lst10)) assert len(lst0) == len(lst0_old)+len(lst10), 'lst0 = %s, lst0_old = %s, lst10 = %s'%(str(lst0),str(lst0_old),str(lst10))
sss = remove_v(ss,0) #remove the 0's from ss sss = remove_v(ss,0) #remove the 0's from ss
assert len(sss) == len(ss)-len(lst0), 'len(sss) = %d, len(ss) = %d, len(lst0) = %d'%(len(sss),len(ss),len(lst0)) assert len(sss) == len(ss)-len(lst0), 'len(sss) = %d, len(ss) = %d, len(lst0) = %d'%(len(sss),len(ss),len(lst0))
@ -3874,24 +3879,25 @@ def multi_prove(op='simple',tt=900,n_fast=0, final_map=[]):
#done with new code #done with new code
assert len(lst1_1) == len(lst1), 'mismatch, lst1 = %d, lst1_1 = %d'%(len(lst1),len(lst1_1)) assert len(lst1_1) == len(lst1), 'mismatch, lst1 = %d, lst1_1 = %d'%(len(lst1),len(lst1_1))
lst1 = lst1_1 #lst1 should be in original minus lst0 lst1 = lst1_1 #lst1 should be in original minus lst0
print 'Found %d SAT POs'%len(lst1) ## print 'Found %d SAT POs'%len(lst1)
print 'Found %d UNSAT POs'%len(lst10) ## print 'Found %d UNSAT POs'%len(lst10)
res = 'SAT = %d, UNSAT = %d, UNDECIDED = %d'%(len(lst1),len(lst0),NNN-(len(lst1)+len(lst0))) res = 'SAT = %d, UNSAT = %d, UNDECIDED = %d'%(len(lst1),len(lst0),NNN-(len(lst1)+len(lst0)))
rr = '\n@@@@ Time = %.2f: '%(time.time() - t_iter_start) rr = '\n@@@@ Time = %.2f: '%(time.time() - t_iter_start)
rr = rr + res rr = rr + res
rr = '%s: '%init_initial_f_name + rr
print rr print rr
file_out.write(rr + '\n') file_out.write(rr + '\n')
file_out.flush() file_out.flush()
N = n_pos() N = n_pos()
print len(lst10),n_pos() ## print len(lst10),n_pos()
if not len(lst10) == n_pos() and len(lst10) > 0: if not len(lst10) == n_pos() and len(lst10) > 0:
remove(lst10,1) #remove 0 POs remove(lst10,1) #remove 0 POs
print 'Removed %d UNSAT POs'%len(lst10) print 'Removed %d UNSAT POs'%len(lst10)
N = n_pos() N = n_pos()
elif len(lst10) == n_pos(): elif len(lst10) == n_pos():
N = 0 #can't remove all POs. Must proceed as if there are no POs. But all POs are UNSAT. N = 0 #can't remove all POs. Must proceed as if there are no POs. But all POs are UNSAT.
print len(lst1),N,S #note: have not removed the lst1 POs. ## print len(lst1),N,S #note: have not removed the lst1 POs.
if len(lst1) == N or S == 'UNSAT' or N == 0: #all POs are SAT if len(lst1) == N or S == 'UNSAT' or N == 0: #all POs are solved
L = [0]*N #could just put L as all 1's. If N = 0, all POs are UNSAT and lst1 = [] L = [0]*N #could just put L as all 1's. If N = 0, all POs are UNSAT and lst1 = []
for i in range(len(lst1)): #put 1's in SAT POs for i in range(len(lst1)): #put 1's in SAT POs
L[lst1[i]]=1 L[lst1[i]]=1
@ -3911,7 +3917,7 @@ def multi_prove(op='simple',tt=900,n_fast=0, final_map=[]):
else: else:
N = 0 N = 0
if N == 1: #this was wrong. Need to report in original indices??? if N == 1: #this was wrong. Need to report in original indices???
result = sp(2000) result = sp(2001)
rs=result[0] rs=result[0]
#need to find out original index of remaining PO #need to find out original index of remaining PO
if rs == 'SAT': if rs == 'SAT':
@ -3928,6 +3934,7 @@ def multi_prove(op='simple',tt=900,n_fast=0, final_map=[]):
report_results(L) report_results(L)
res = sumsize(L) res = sumsize(L)
rr = '\n@@@@ Time = %d '%(time.time() - t_iter_start) + res rr = '\n@@@@ Time = %d '%(time.time() - t_iter_start) + res
rr = '%s: '%init_initial_f_name + rr
print rr print rr
file_out.write(rr+ '\n') file_out.write(rr+ '\n')
file_out.flush() file_out.flush()
@ -3945,7 +3952,7 @@ def multi_prove(op='simple',tt=900,n_fast=0, final_map=[]):
map1 = create_map(leq,N) #creates map into original map1 = create_map(leq,N) #creates map into original
## print map1 ## print map1
if not count_less(L,0) == N: if not count_less(L,0) == N:
print L print 'L = %s'%sumsize(L)
L1 = [-1]*n_pos() L1 = [-1]*n_pos()
## L1 = pass_down(L,list(L1),map1) # no need to pass down because L will have no values at this point. ## L1 = pass_down(L,list(L1),map1) # no need to pass down because L will have no values at this point.
else: else:
@ -3986,7 +3993,7 @@ def multi_prove(op='simple',tt=900,n_fast=0, final_map=[]):
## write_file('1') ## write_file('1')
## L = output(list(L),list(L1),L2,map1,map2,lst0,lst1,NP) ## L = output(list(L),list(L1),L2,map1,map2,lst0,lst1,NP)
L = output2(list(L2),map1,map2,lst0,lst1,NP) L = output2(list(L2),map1,map2,lst0,lst1,NP)
result = simple(2000,1) result = simple(2001,1)
Ss = rs = result[0] Ss = rs = result[0]
if rs == 'SAT': if rs == 'SAT':
L2 = [1] L2 = [1]
@ -4030,7 +4037,7 @@ def multi_prove(op='simple',tt=900,n_fast=0, final_map=[]):
ttt = 20 ttt = 20
abc('w %s_before_mprove2.aig'%f_name) abc('w %s_before_mprove2.aig'%f_name)
print '%s_before_mprove2.aig written'%f_name print '%s_before_mprove2.aig written'%f_name
print 'L2 = %s'%str(L2) ## print 'L2 = %s'%str(L2)
print 'Entering first mprove2 for %d sec.'%ttt, print 'Entering first mprove2 for %d sec.'%ttt,
Ss,L2 = mprove2(list(L2),op,ttt,1) #populates L2 with results Ss,L2 = mprove2(list(L2),op,ttt,1) #populates L2 with results
## print Ss,L2 ## print Ss,L2
@ -4104,7 +4111,7 @@ def multi_prove(op='simple',tt=900,n_fast=0, final_map=[]):
remove_proved_pos(L2) remove_proved_pos(L2)
simplify() simplify()
write_file('save') write_file('save')
result = simple(2000,1) result = simple(2001,1)
if_found = False if_found = False
if result[0] == 'UNSAT': if result[0] == 'UNSAT':
for i in range(N): for i in range(N):
@ -4147,6 +4154,7 @@ def multi_prove_iter():
s = count_less(L,2) - (d+u) s = count_less(L,2) - (d+u)
rr = '\n@@@@@ %s: Final time = %.2f '%(init_initial_f_name,(time.time() - t_iter_start)) rr = '\n@@@@@ %s: Final time = %.2f '%(init_initial_f_name,(time.time() - t_iter_start))
rr = rr + 'SAT = %d, UNSAT = %d, UNDECIDED = %d '%(s,u,d) rr = rr + 'SAT = %d, UNSAT = %d, UNDECIDED = %d '%(s,u,d)
rr = '%s: '%init_initial_f_name + rr
print rr print rr
file_out.write(rr) file_out.write(rr)
res = PO_results(L) res = PO_results(L)
@ -4534,6 +4542,7 @@ def report_results(L,final_map=[],if_final=False):
print '\n' print '\n'
def report_result(POn, REn, final_map=[]): def report_result(POn, REn, final_map=[]):
return #for non hwmcc application
if final_map == []: if final_map == []:
print 'PO = %d, Result = %d: '%(POn, REn), print 'PO = %d, Result = %d: '%(POn, REn),
else: else:
@ -4608,7 +4617,7 @@ def scorr_T(t=10000):
smp_trace = smp_trace + ['%s'%mtds[m_best]] smp_trace = smp_trace + ['%s'%mtds[m_best]]
abc('r %s_best_T.aig'%f_name) abc('r %s_best_T.aig'%f_name)
def pscorr(t=900): def pscorr(t=2001):
result = par_scorr(t) result = par_scorr(t)
if n_ands() == 0: if n_ands() == 0:
return result return result
@ -4738,9 +4747,9 @@ def mprove2(L=0,op='simple',t=100,nn=0):
v = -1 v = -1
skip_spec_old = skip_spec skip_spec_old = skip_spec
skip_spec = True skip_spec = True
result = simple(2000,1) result = simple(2001,1)
ff_name == f_name ff_name == f_name
result = sp(0,2000) #warning sp() can change f_name. 0 means simplify result = sp(0,2001) #warning sp() can change f_name. 0 means simplify
f_name = ff_name f_name = ff_name
skip_spec = skip_spec_old skip_spec = skip_spec_old
res = result[0] res = result[0]
@ -4784,7 +4793,7 @@ def mprove2(L=0,op='simple',t=100,nn=0):
N = n_pos() N = n_pos()
tb = min(N,50) tb = min(N,50)
## print 'Trying par_multi_sat for %d sec.'%tb ## print 'Trying par_multi_sat for %d sec.'%tb
S,lst1,s = par_multi_sat(tb,1,1,0) #this gives a list of SAT POs S,lst1,s = par_multi_sat(tb,1,1,1) #this gives a list of SAT POs
L2 = s10 = s L2 = s10 = s
n_solved = n_pos() - count_less(s10,0) n_solved = n_pos() - count_less(s10,0)
if 1 in s10 or 0 in s10: #something solved if 1 in s10 or 0 in s10: #something solved
@ -4802,14 +4811,16 @@ def mprove2(L=0,op='simple',t=100,nn=0):
#iterate here as long as more than 1 PO is found SAT #iterate here as long as more than 1 PO is found SAT
n_solved = n_pos() - count_less(s210,0) n_solved = n_pos() - count_less(s210,0)
while n_solved > 0: while n_solved > 0:
print 'n_solved = %d'%n_solved
gap = int(1+1.2*gap) gap = int(1+1.2*gap)
print 'gap = %.2f'%gap print 'gap = %.2f'%gap
pre_simp(1) #warning this may create const-0 pos pre_simp(1) #warning this may create const-0 pos
S,lst2,s = par_multi_sat(tb,gap,1,0) #this can find UNSAT POs S,lst2,s = par_multi_sat(tb,gap,1,1) #this can find UNSAT POs
s210 = s s210 = s
n_solved = n_pos() - count_less(s210,0) n_solved = n_pos() - count_less(s210,0)
s10 = put(s210,list(s10)) #put the new values found into s10 s10 = put(s210,list(s10)) #put the new values found into s10
if count_less(s10,0) == 0 or n_solved == 0: #all solved or nothing solved if count_less(s10,0) == 0 or n_solved == 0: #all solved or nothing solved
print 's210 = %s'%sumsize(s210)
break #s10 has the results break #s10 has the results
else: else:
out = '\n@@@@ Time = %.2f: additional POs found SAT = %d'%((time.time()- t_iter_start),len(lst2)) out = '\n@@@@ Time = %.2f: additional POs found SAT = %d'%((time.time()- t_iter_start),len(lst2))
@ -4821,7 +4832,7 @@ def mprove2(L=0,op='simple',t=100,nn=0):
remove(rem,1) #this zeros the l210 and then removes ALL const-1 POs. remove(rem,1) #this zeros the l210 and then removes ALL const-1 POs.
#If there are more than lst2 removed, it fires an assertion. #If there are more than lst2 removed, it fires an assertion.
continue continue
L2 = s10 #put results in s10 L2 = s10 #put results of s10 into L2
else: #lst1 is empty or S == SAT' else: #lst1 is empty or S == SAT'
print 'no cex found or S = UNSAT' print 'no cex found or S = UNSAT'
else: #all solved else: #all solved
@ -4833,7 +4844,7 @@ def mprove2(L=0,op='simple',t=100,nn=0):
if -1 in s10: if -1 in s10:
print 'Entering solve_all ', print 'Entering solve_all ',
ps() ps()
S,s210 = solve_all([-1]*n_pos(),900) #solve_all calls sp() or simple but preserves the aig and f_name S,s210 = solve_all([-1]*n_pos(),2001) #solve_all calls sp() or simple but preserves the aig and f_name
## else: zzz ## else: zzz
if -1 in s210: #then no POs were solved by solve_all if -1 in s210: #then no POs were solved by solve_all
## abc('r %s_smp2_2.aig'%f_name) ## abc('r %s_smp2_2.aig'%f_name)
@ -4846,7 +4857,7 @@ def mprove2(L=0,op='simple',t=100,nn=0):
s210 = [-1]*n_pos() s210 = [-1]*n_pos()
print 's210 after mprove and before inject 1 %s:'%sumsize(s210) print 's210 after mprove and before inject 1 %s:'%sumsize(s210)
L2 = put(s210,s10) L2 = put(s210,s10)
print 'L2 after inject 1 %s:'%sumsize(L2) ## print 'L2 after inject 1 %s:'%sumsize(L2)
else: #all POs solved else: #all POs solved
L2 = s10 L2 = s10
assert NP == 1, 'NP > 1: ERROR' assert NP == 1, 'NP > 1: ERROR'
@ -4857,7 +4868,7 @@ def mprove2(L=0,op='simple',t=100,nn=0):
print 'L1 after unmap of map3: ', print 'L1 after unmap of map3: ',
print sumsize(L1) print sumsize(L1)
else: else:
print 'L2 = %s'%str(L2) ## print 'L2 = %s'%str(L2)
L1 = L2 L1 = L2
L1 = inject(list(L1),Llst0,0) L1 = inject(list(L1),Llst0,0)
print 'L1 after inject of Llst0 0s: %s:'%sumsize(L1) print 'L1 after inject of Llst0 0s: %s:'%sumsize(L1)
@ -4969,10 +4980,10 @@ def solve_all(L2,t):
## ps() ## ps()
skip_spec_old = skip_spec skip_spec_old = skip_spec
skip_spec = True skip_spec = True
tt = max(t,900) tt = max(t,2001)
print 'Entering simple for %d sec.'%tt print 'Entering simple for %d sec.'%tt
result = simple(tt,1) #### temporary 1 means do not simplify ## result = simple(tt,1) #### temporary 1 means do not simplify
## result = sp(0,t) #warning sp() may change f_name result = sp(0,t) #warning sp() may change f_name. Changed from HWMCC13 submission
skip_spec = skip_spec_old skip_spec = skip_spec_old
## print 'solve_all: result = %s'%result ## print 'solve_all: result = %s'%result
if result[0] == 'UNSAT': if result[0] == 'UNSAT':
@ -5147,7 +5158,7 @@ def mprove(L,op='simple',tt=1000):
## sec_options = options ## sec_options = options
## return super_prove(1) ## return super_prove(1)
def super_prove(n=0,t=900): def super_prove(n=0,t=2001):
"""Main proof technique now. Does original prove and if after speculation there are multiple output left """Main proof technique now. Does original prove and if after speculation there are multiple output left
if will try to prove each output separately, in reverse order. It will quit at the first output that fails if will try to prove each output separately, in reverse order. It will quit at the first output that fails
to be proved, or any output that is proved SAT to be proved, or any output that is proved SAT
@ -5358,13 +5369,13 @@ def reachn(t):
print 'reachm3 done in time = %f'%(time.clock() - x) print 'reachm3 done in time = %f'%(time.clock() - x)
return get_status() return get_status()
def reachx(t=900): def reachx(t=2001):
x = time.time() x = time.time()
abc('reachx -t %d'%t) abc('reachx -t %d'%t)
print 'reachx done in time = %f'%(time.time() - x) print 'reachx done in time = %f'%(time.time() - x)
return get_status() return get_status()
def reachy(t=900): def reachy(t=2001):
x = time.clock() x = time.clock()
abc('&get;&reachy -v -T %d'%t) abc('&get;&reachy -v -T %d'%t)
## print 'reachy done in time = %f'%(time.clock() - x) ## print 'reachy done in time = %f'%(time.clock() - x)
@ -6033,18 +6044,18 @@ def par_multi_sat(t=10,gap=0,m=1,H=0):
t = gt t = gt
last_gap = gt last_gap = gt
## H = max(100, t/n_pos()+1) ## H = max(100, t/n_pos()+1)
if not H == 0: if not H == 0: #se timeout peer output
H = (gt*1000)/n_pos() H = (gt*1000)/n_pos()
H = max(min(H,1000*gt),100) H = max(min(H,1000*gt),100)
tme = time.time() tme = time.time()
list0 = listr_0_pos() #reduces POs list0 = listr_0_pos() #reduces POs
list0.sort() list0.sort()
## print 'list0 = %s'%str(list0) ## print 'list0 = %s'%str(list0)
if len(list0)>0: ## if len(list0)>0:
print 'temporarily removed %d cost-0 POs'%len(list0) ## print 'removed %d cost-0 POs'%len(list0)
ps() ## ps()
if len(list0)> 0: if len(list0)> 0:
print 'Found %d const-0 POs, but not removed'%len(list0) print 'Found initial %d const-0 POs'%len(list0)
## print ll ## print ll
print 'par_multi_sat entered for %.2f sec. and gap = %.2f sec., H = %.2f'%(t,gt,H) print 'par_multi_sat entered for %.2f sec. and gap = %.2f sec., H = %.2f'%(t,gt,H)
base = m*1000 base = m*1000
@ -6054,10 +6065,10 @@ def par_multi_sat(t=10,gap=0,m=1,H=0):
mx = 1000000000/max(1,n_latches()) mx = 1000000000/max(1,n_latches())
N = n_pos() N = n_pos()
na = n_ands() na = n_ands()
F = [eval('(pyabc_split.defer(bmc3az)(t,gt,%d,H))'%(0*base))] F = [eval('(pyabc_split.defer(bmc3az)(t,gt,%d,H))'%(0))]
## if na < 50000: ## if na < 50000:
F = F + [eval('(pyabc_split.defer(pdraz)(t,gt,H))')] #need pdr in?? F = F + [eval('(pyabc_split.defer(pdraz)(t,gt,H))')] #need pdr in??
F = F + [eval('(pyabc_split.defer(sim3az)(t,gt,%d,4,0))'%(0*base))] F = F + [eval('(pyabc_split.defer(sim3az)(t,gt,%d,4,0))'%(0))]
F = F + [eval('(pyabc_split.defer(sleep)(t))')] F = F + [eval('(pyabc_split.defer(sleep)(t))')]
F = F + [eval('(pyabc_split.defer(sim3az)(t,gt,%d,4,0))'%(100))] F = F + [eval('(pyabc_split.defer(sim3az)(t,gt,%d,4,0))'%(100))]
F = F + [eval('(pyabc_split.defer(bmc3az)(t,gt,%d,0))'%(100))] F = F + [eval('(pyabc_split.defer(bmc3az)(t,gt,%d,0))'%(100))]
@ -6087,8 +6098,8 @@ def par_multi_sat(t=10,gap=0,m=1,H=0):
nn = len(F) nn = len(F)
for i,res in pyabc_split.abc_split_all(F): for i,res in pyabc_split.abc_split_all(F):
ii = ii + [i] ii = ii + [i]
if len(ii) == len(F)-1: #all done but sleep ## if len(ii) == len(F)-1: #all done but sleep
break ## break
if i == 3: #sleep timeout if i == 3: #sleep timeout
print 'sleep timeout' print 'sleep timeout'
break break
@ -6097,15 +6108,15 @@ def par_multi_sat(t=10,gap=0,m=1,H=0):
#### print i #### print i
if i == 0: if i == 0:
zero_done = True # bmc with start at 0 is done zero_done = True # bmc with start at 0 is done
if i == 2: if i == 2: #sim3 with start 0 is done
two_done = True two_done = True
if res == None: #this can happen if one of the methods bombs out if res == None: #this can happen if one of the methods bombs out
print 'Method %d returned None'%i print 'Method %d returned None'%i
continue continue
## print res ## print res
s1 = switch(res[1]) #res[1]= s s1 = switch(list(res[1])) #res[1]= s
s = merge_s(list(s),s1) s = merge_s(list(s),s1)
print sumsize(s) ## print sumsize(s)
ss = ss + [s1] ss = ss + [s1]
## LL = LL + [res[0]] ## LL = LL + [res[0]]
## L = L + res[0] ## L = L + res[0]
@ -6127,25 +6138,27 @@ def par_multi_sat(t=10,gap=0,m=1,H=0):
r = ss2[0] r = ss2[0]
if r == ss2[1] and count_less(r,1) < len(r): #at least 1 SAT PO found if r == ss2[1] and count_less(r,1) < len(r): #at least 1 SAT PO found
break break
if len(ii) == len(F)-1: #all done but sleep
break
## if len(LL) > 1 and zero_done and two_done: ## if len(LL) > 1 and zero_done and two_done:
## ll2 = LL[-2:] #checking if last 2 results agree ## ll2 = LL[-2:] #checking if last 2 results agree
## if ll2[0] == ll2[1] and ll2[0] > 0: ## if ll2[0] == ll2[1] and ll2[0] > 0:
## break ## break
print 'Found %d SAT POs in '%(len(L)), ## print 'Found %d SAT POs in '%(len(L)),
print 'time = %.2f'%(time.time()-tme) print 'time = %.2f'%(time.time()-tme)
print sumsize(s) ## print sumsize(s)
## L.sort() ## L.sort()
## print 'L_before = %s'%(str(L)) ## print 'L_before = %s'%(str(L))
#### check_None_status(L,s,1) #now 1 in s means sat. s can have 0 in it, meaning it found some POs unsat. #### check_None_status(L,s,1) #now 1 in s means sat. s can have 0 in it, meaning it found some POs unsat.
## L = merge(list(list0),list(L),1) #shift L according to list0 but do not include list0. ## L = merge(list(list0),list(L),1) #shift L according to list0 but do not include list0.
## print 'L_shifted = %s'%(str(L)) ## print 'L_shifted = %s'%(str(L))
## # Need to return only SAT POs have to do the same for s ## # Need to return only SAT POs have to do the same for s
print 'len(s) = %d, len(list0) = %d'%(len(s),len(list0)) ## print 'len(s) = %d, len(list0) = %d'%(len(s),len(list0))
ss = expand(s,list0,0) ss = expand(s,list0,0)
## assert list0 == indices(ss,0) ## assert list0 == indices(ss,0)
print sumsize(ss) print '\n Par_multi_sat result = %s'%sumsize(ss)
## assert check_consistancy(L,ss), 'inconsistant' ## assert check_consistancy(L,ss), 'inconsistant'
abc('r %s_save.aig'%f_name) abc('r %s_save.aig'%f_name) #restore initial aig
return S,[],ss return S,[],ss
@ -6334,7 +6347,7 @@ def remove_proved_pos(lst):
def bmc_j(t=900): def bmc_j(t=2001):
""" finds a cex in t seconds starting at 2*N where N is depth of bmc -T 1""" """ finds a cex in t seconds starting at 2*N where N is depth of bmc -T 1"""
x = time.time() x = time.time()
tt = min(5,max(1,.05*t)) tt = min(5,max(1,.05*t))
@ -6354,7 +6367,7 @@ def bmc_j(t=900):
## print 'cex found in %0.2f sec at frame %d'%((time.time()-x),cex_frame()) ## print 'cex found in %0.2f sec at frame %d'%((time.time()-x),cex_frame())
return RESULT[get_status()] return RESULT[get_status()]
def pdrseed(t=900): def pdrseed(t=2001):
"""uses the abstracted version now""" """uses the abstracted version now"""
## abc('&get;,treb -rlim=60 -coi=3 -te=1 -vt=%f -seed=521'%t) ## abc('&get;,treb -rlim=60 -coi=3 -te=1 -vt=%f -seed=521'%t)
abc('&get;,treb -rlim=100 -vt=%f -seed=521'%t) abc('&get;,treb -rlim=100 -vt=%f -seed=521'%t)
@ -6364,20 +6377,20 @@ def pdrold(t):
abc('&get; ,pdr -vt=%f'%t) abc('&get; ,pdr -vt=%f'%t)
return RESULT[get_status()] return RESULT[get_status()]
def pdr(t=900): def pdr(t=2001):
abc('&get; ,treb -vt=%f'%t) abc('&get; ,treb -vt=%f'%t)
return RESULT[get_status()] return RESULT[get_status()]
def pdr0(t=900): def pdr0(t=2001):
abc('&get; ,pdr -rlim=100 -vt=%f'%t) abc('&get; ,pdr -rlim=100 -vt=%f'%t)
return RESULT[get_status()] return RESULT[get_status()]
def pdra(t=900): def pdra(t=2001):
## abc('&get; ,treb -rlim=100 -ssize -pre-cubes=3 -vt=%f'%t) ## abc('&get; ,treb -rlim=100 -ssize -pre-cubes=3 -vt=%f'%t)
abc('&get; ,treb -abs -rlim=100 -sat=abc -vt=%f'%t) abc('&get; ,treb -abs -rlim=100 -sat=abc -vt=%f'%t)
return RESULT[get_status()] return RESULT[get_status()]
def pdrm(t=900): def pdrm(t=2001):
abc('pdr -C 0 -T %f'%t) abc('pdr -C 0 -T %f'%t)
return RESULT[get_status()] return RESULT[get_status()]
@ -6389,30 +6402,37 @@ def bmc2(t):
abc('bmc2 -C 1000000 -T %f'%t) abc('bmc2 -C 1000000 -T %f'%t)
return RESULT[get_status()] return RESULT[get_status()]
def bmc(t=900): def bmc(t=2001):
abc('&get; ,bmc -vt=%d'%t) abc('&get; ,bmc -vt=%d'%t)
return RESULT[get_status()] return RESULT[get_status()]
def intrp(t=900): def intrp(t=2001):
abc('&get; ,imc -vt=%d'%t) abc('&get; ,imc -vt=%d'%t)
return RESULT[get_status()] return RESULT[get_status()]
def bmc3az(t=900,gt=10,C=999,H=0): def bmc3az(t=2001,gt=10,C=999,H=0):
t_init = time.time() t_init = time.time()
if C > 999: if not C == 0:
abc('&get; &cycle -F %d; &put'%C) abc('&get; &cycle -F %d; &put'%C)
abc('bmc3 -az -C 1000000 -T %d -G %d -H %.2f'%(t,gt,H)) abc('bmc3 -az -C 1000000 -T %.2f -G %.2f -H %.2f'%(t,gt,H))
cex_list = cex_get_vector() cex_list = cex_get_vector()
L = list_non_None(cex_list) L = list_non_None(cex_list)
## check_None_status(L) ## check_None_status(L)
print 'bmc3az(%.2f,%.2f,%d,%d): CEXs = %d, time = %.2f'%(t,gt,C,H,len(L),(time.time()-t_init)) print '\nbmc3az(%.2f,%.2f,%d,%d): CEXs = %d, time = %.2f'%(t,gt,C,H,len(L),(time.time()-t_init))
## s = status_get_vector() print 'Length CEXs = %d'%(len(L))
s = [-1]*n_pos() s = status_get_vector()
for j in L: if len(s) == 0: #error if this happens check with Alan
s[j]=0 #0 here means SAT. It will be switched in par_multi_sat s = [-1]*n_pos()
sss = switch(list(s))
print 's_status = %s'%sumsize(sss)
## s = [-1]*n_pos()
## for j in L:
## s[j]=0 #0 here means SAT. It will be switched in par_multi_sat
## sss = switch(list(s))
## print 's = %s'%sumsize(sss)
return L,s return L,s
def pdraz(t=900,gt=10,H=0): def pdraz(t=2001,gt=10,H=0):
print 'pdraz entered with t = %.2f, gt = %.2f, H = %.2f'%(t,gt,H) print 'pdraz entered with t = %.2f, gt = %.2f, H = %.2f'%(t,gt,H)
t_init = time.time() t_init = time.time()
run_command('pdr -az -T %d -G %d -H %.2f'%(t,gt,H)) run_command('pdr -az -T %d -G %d -H %.2f'%(t,gt,H))
@ -6427,10 +6447,10 @@ def pdraz(t=900,gt=10,H=0):
print 'pdraz(%.2f,%.2f,%d): CEXs = %d, time = %.2f'%(t,gt,H,len(L),(time.time()-t_init)) print 'pdraz(%.2f,%.2f,%d): CEXs = %d, time = %.2f'%(t,gt,H,len(L),(time.time()-t_init))
return L,s return L,s
def sim3az(t=900,gt=10,C=1000,W=5,N=0): def sim3az(t=2001,gt=10,C=1000,W=5,N=0):
""" N = random seed, gt is gap time, W = # words, F = #frames""" """ N = random seed, gt is gap time, W = # words, F = #frames"""
t_init = time.time() t_init = time.time()
if C > 1000: if not C == 0:
abc('&get; &cycle -F %d; &put'%C) abc('&get; &cycle -F %d; &put'%C)
abc('sim3 -az -T %.2f -G %.2f -F 40 -W %d -N %d'%(t,gt,W,N)) abc('sim3 -az -T %.2f -G %.2f -F 40 -W %d -N %d'%(t,gt,W,N))
cex_list = cex_get_vector() cex_list = cex_get_vector()
@ -6442,11 +6462,11 @@ def sim3az(t=900,gt=10,C=1000,W=5,N=0):
print 'sim3az(%.2f,%.2f,%d,%d,%d): CEXs=%d, time = %.2f'%(t,gt,C,W,N,len(L),(time.time()-t_init)) print 'sim3az(%.2f,%.2f,%d,%d,%d): CEXs=%d, time = %.2f'%(t,gt,C,W,N,len(L),(time.time()-t_init))
return L,s return L,s
def bmc3(t=900): def bmc3(t=2001):
abc('bmc3 -C 1000000 -T %d'%t) abc('bmc3 -C 1000000 -T %d'%t)
return RESULT[get_status()] return RESULT[get_status()]
def intrpm(t=900): def intrpm(t=2001):
abc('int -C 1000000 -F 10000 -K 1 -T %d'%t) abc('int -C 1000000 -F 10000 -K 1 -T %d'%t)
print 'intrpm: status = %d'%get_status() print 'intrpm: status = %d'%get_status()
return RESULT[get_status()] return RESULT[get_status()]