from pyabc import *
import pyabc_split
import redirect
import sys
import os
import time
import math
import main
global G_C,G_T,latches_before_abs,latches_before_pba,n_pos_before,x_factor,methods,last_winner
global last_cex,JV,JP, cex_list,max_bmc, last_cx, pord_on
"""
The functions that are currently available from module _abc are:
int n_ands();
int n_pis();
int n_pos();
int n_latches();
int n_bmc_frames();
int prob_status(); 1 = unsat, 0 = sat, -1 = unsolved
int cex_get()
int cex_put()
int run_command(char* cmd);
bool has_comb_model();
bool has_seq_model();
bool is_true_cex();
bool is_valid_cex();
return 1 if the number of PIs in the current network and in the current counter-example are equal
int n_cex_pis();
return the number of PIs in the current counter-example
int n_cex_regs();
return the number of flops in the current counter-example
int cex_po();
returns the zero-based output PO number that is SAT by cex
int cex_frame();
return the zero-based frame number where the outputs is SAT
The last four APIs return -1, if the counter-example is not defined.
"""
#global variables
#________________________________________________
stackno_gabs = stackno_gore = stackno_greg= 0
STATUS_UNKNOWN = -1
STATUS_SAT = 0
STATUS_UNSAT = 1
RESULT = ('SAT' , 'SAT', 'UNSAT', 'UNDECIDED', 'UNDECIDED,', 'UNDECIDED' )
Sat = Sat_reg = 0
Sat_true = 1
Unsat = 2
Undecided = Undecided_reduction = 3
Undecided_no_reduction = 4
Error = 5
Restart = 6
xfi = x_factor = 1 #set this to higher for larger problems or if you want to try harder during abstraction
max_bmc = -1
last_time = 0
j_last = 0
seed = 113
init_simp = 1
K_backup = init_time = 0
last_verify_time = 20
last_cex = last_winner = 'None'
last_cx = 0
trim_allowed = True
pord_on = False
sec_sw = False
sec_options = ''
cex_list = []
TERM = 'USL'
t_init = 2 #initial time for poor man's concurrency.
methods = ['PDR', 'INTRP', 'BMC',
'SIM', 'REACHX',
'PRE_SIMP', 'SUPER_PROVE2', 'PDRM', 'REACHM', 'BMC3','Min_Retime',
'For_Retime','REACHP','REACHN','PDRsd','prove_part_2',
'prove_part_3','verify','sleep','PDRMm','prove_part_1',
'run_parallel','INTRPb', 'INTRPm', 'REACHY', 'REACHYc','RareSim','simplify', 'speculate',
'quick_sec', 'BMC_J']
#'0.PDR', '1.INTERPOLATION', '2.BMC', '3.SIMULATION',
#'4.REACHX', '5.PRE_SIMP', '6.SUPER_PROVE', '7.PDRM', '8.REACHM', 9.BMC3'
# 10. Min_ret, 11. For_ret, 12. REACHP, 13. REACHN 14. PDRseed 15.prove_part_2,
#16.prove_part_3, 17.verify, 18.sleep, 19.PDRMm, 20.prove_part_1,
#21.run_parallel, 22.INTRP_bwd, 23. Interp_m 24. REACHY 25. REACHYc 26. Rarity Sim 27. simplify
#28. speculate, 29. quick_sec, 30 bmc3 -S
win_list = [(0,.1),(1,.1),(2,.1),(3,.1),(4,.1),(5,-1),(6,-1),(7,.1)]
FUNCS = ["(pyabc_split.defer(abc)('&get;,pdr -vt=%f'%t))",
"(pyabc_split.defer(abc)('&get;,imc -vt=%f'%(t)))",
"(pyabc_split.defer(abc)('&get;,bmc -vt=%f'%t))",
"(pyabc_split.defer(simulate)(t))",
"(pyabc_split.defer(abc)('reachx -t %d'%t))",
"(pyabc_split.defer(pre_simp)())",
"(pyabc_split.defer(super_prove)(2))",
"(pyabc_split.defer(pdrm)(t))",
"(pyabc_split.defer(abc)('&get;&reachm -vcs -T %d'%t))",
"(pyabc_split.defer(abc)('bmc3 -C 1000000 -T %f'%t))",
"(pyabc_split.defer(abc)('dr;&get;&lcorr;&dc2;&scorr;&put;dr'))",
"(pyabc_split.defer(abc)('dr -m;&get;&lcorr;&dc2;&scorr;&put;dr'))",
"(pyabc_split.defer(abc)('&get;&reachp -vr -T %d'%t))",
"(pyabc_split.defer(abc)('&get;&reachn -vr -T %d'%t))",
"(pyabc_split.defer(abc)('&get;,pdr -vt=%f -seed=521'%t))",
"(pyabc_split.defer(prove_part_2)(K))",
"(pyabc_split.defer(prove_part_3)(K))",
"(pyabc_split.defer(verify)(JV,t))",
"(pyabc_split.defer(sleep)(t))",
"(pyabc_split.defer(pdrmm)(t))",
"(pyabc_split.defer(prove_part_1)'(%d)'%(K))",
"(pyabc_split.defer(run_parallel)(JP,t,'TERM'))",
"(pyabc_split.defer(abc)('&get;,imc -bwd -vt=%f'%t))",
"(pyabc_split.defer(abc)('int -C 1000000 -F 10000 -K 2 -T %f'%t))",
"(pyabc_split.defer(abc)('&get;&reachy -v -T %d'%t))",
"(pyabc_split.defer(abc)('&get;&reachy -cv -T %d'%t))",
"(pyabc_split.defer(simulate2)(t))",
"(pyabc_split.defer(simplify)())",
"(pyabc_split.defer(speculate)())",
"(pyabc_split.defer(quick_sec)(t))",
"(pyabc_split.defer(bmc_s)(t))"
]
## "(pyabc_split.defer(abc)('bmc3 -C 1000000 -T %f -S %d'%(t,int(1.5*max_bmc))))"
#note: interp given 1/2 the time.
allreachs = [4,8,12,13,24,25]
reachs = [24]
allpdrs = [0,7,14,19]
pdrs = [0,7]
allbmcs = [2,9,30]
exbmcs = [2,9]
bmcs = [9,30]
allintrps = [1,22,23]
bestintrps = [23]
intrps = [23]
allsims = [3,26]
sims = [3]
allslps = [18]
slps = [18]
JVprove = [7,1,4,24]
JV = pdrs+intrps+bmcs+sims #sets what is run in parallel '17. verify' above
JP = JV + [27] # sets what is run in '21. run_parallel' above 27 simplify should be last because it can't time out.
#_____________________________________________________________
# Function definitions:
# simple functions: ________________________________________________________________________
# set_globals, abc, q, x, has_any_model, is_sat, is_unsat, push, pop
# ALIASES
def initialize():
global xfi, max_bmc, last_time,j_last, seed, init_simp, K_backup, last_verify_time
global init_time, last_cex, last_winner, trim_allowed, t_init, sec_options, sec_sw
global n_pos_before, n_pos_proved, last_cx, pord_on
xfi = x_factor = 1 #set this to higher for larger problems or if you want to try harder during abstraction
max_bmc = -1
last_time = 0
j_last = 0
seed = 113
init_simp = 1
K_backup = init_time = 0
last_verify_time = 20
last_cex = last_winner = 'None'
last_cx = 0
trim_allowed = True
pord_on = False
t_init = 2 #this will start sweep time in find_cex_par to 2*t_init here
sec_sw = False
sec_options = ''
cex_list = []
n_pos_before = n_pos()
n_pos_proved = 0
def ps():
print_circuit_stats()
def n_real_inputs():
"""This gives the number of 'real' inputs. This is determined by trimming away inputs that
have no connection to the logic. This is done by the ABC alias 'trm', which changes the current
circuit. In some applications we do not want to change the circuit, but just to know how may inputs
would go away if we did this. So the current circuit is saved and then restored afterwards."""
## abc('w %s_savetempreal.aig; logic; trim; st ;addpi'%f_name)
abc('w %s_savetempreal.aig'%f_name)
with redirect.redirect( redirect.null_file, sys.stdout ):
## with redirect.redirect( redirect.null_file, sys.stderr ):
reparam()
n = n_pis()
abc('r %s_savetempreal.aig'%f_name)
return n
def timer(t):
btime = time.clock()
time.sleep(t)
print t
return time.clock() - btime
def sleep(t):
time.sleep(t)
return Undecided
def abc(cmd):
abc_redirect_all(cmd)
def abc_redirect( cmd, dst = redirect.null_file, src = sys.stdout ):
"""This is our main way of calling an ABC function. Redirect, means that we suppress any output from ABC"""
with redirect.redirect( dst, src ):
return run_command( cmd )
def abc_redirect_all( cmd ):
"""This is our main way of calling an ABC function. Redirect, means that we suppress any output from ABC, including error printouts"""
with redirect.redirect( redirect.null_file, sys.stdout ):
with redirect.redirect( redirect.null_file, sys.stderr ):
return run_command( cmd )
def convert(t):
t = int(t*100)
return str(float(t)/100)
def set_engines(N=0):
"""
Sets the MC engines that are used in verification according to
if there are 4 or 8 processors.
"""
global reachs,pdrs,sims,intrps,bmcs
if N == 0:
N = os.sysconf(os.sysconf_names["SC_NPROCESSORS_ONLN"])
if N == 1:
reachs = [24]
pdrs = [7]
## bmcs = [30]
bmcs = [9]
intrps = []
sims = []
slps = [18]
elif N == 2:
reachs = [24]
pdrs = [7]
bmcs = [30]
intrps = []
sims = []
slps = [18]
elif N == 4:
reachs = [24]
pdrs = [7]
bmcs = [9,30]
intrps = [23]
sims = []
slps = [18]
elif N == 8:
reachs = [24]
pdrs = [0,7]
bmcs = [9,30]
intrps = [23]
sims = [3]
slps = [18]
def set_globals():
"""This sets global parameters that are used to limit the resources used by all the operations
bmc, interpolation BDDs, abstract etc. There is a global factor 'x_factor' that can
control all of the various resource limiting parameters"""
global G_C,G_T,x_factor
nl=n_latches()
na=n_ands()
np = n_pis()
#G_C = min(500000,(3*na+500*(nl+np)))
G_C = x_factor * min(100000,(3*na+500*(nl+np)))
#G_T = min(250,G_C/2000)
G_T = x_factor * min(75,G_C/2000)
G_T = max(1,G_T)
#print('Global values: BMC conflicts = %d, Max time = %d sec.'%(G_C,G_T))
def a():
"""this puts the system into direct abc input mode"""
print "Entering ABC direct-input mode. Type q to quit ABC-mode"
n = 0
while True:
print ' abc %d> '%n,
n = n+1
s = raw_input()
if s == "q":
break
run_command(s)
def remove_spaces(s):
y = ''
for t in s:
if not t == ' ':
y = y + t
return y
def read_file_quiet(fname=None):
"""This is the main program used for reading in a new circuit. The global file name is stored (f_name)
Sometimes we want to know the initial starting name. The file name can have the .aig extension left off
and it will assume that the .aig extension is implied. This should not be used for .blif files.
Any time we want to process a new circuit, we should use this since otherwise we would not have the
correct f_name."""
global max_bmc, f_name, d_name, initial_f_name, x_factor, init_initial_f_name, win_list,seed, sec_options
global win_list, init_simp, po_map
set_engines(4) #temporary
ps()
init_simp = 1
win_list = [(0,.1),(1,.1),(2,.1),(3,.1),(4,.1),(5,-1),(6,-1),(7,.1)] #initialize winning engine list
po_map = range(n_pos())
initialize()
## x_factor = 1
## seed = 223
## max_bmc = -1
if fname is None:
print 'Type in the name of the aig file to be read in'
s = raw_input()
s = remove_spaces(s)
else:
s = fname
if s[-4:] == '.aig':
f_name = s[:-4]
else:
f_name = s
s = s+'.aig'
## run_command(s)
run_command('&r %s;&put'%s)
set_globals()
initial_f_name = f_name
init_initial_f_name = f_name
abc('addpi')
def read_file():
global win_list, init_simp, po_map
read_file_quiet()
## ps()
## init_simp = 1
## win_list = [(0,.1),(1,.1),(2,.1),(3,.1),(4,.1),(5,-1),(6,-1),(7,.1)] #initialize winning engine list
## po_map = range(n_pos())
def rf():
## set_engines(4) #temporary
read_file()
def write_file(s):
"""this is the main method for writing the current circuit to an AIG file on disk.
It manages the name of the file, by giving an extension (s). The file name 'f_name'
keeps increasing as more extensions are written. A typical sequence is
name, name_smp, name_smp_abs, name_smp_abs_spec, name_smp_abs_spec_final"""
global f_name
"""Writes out the current file as an aig file using f_name appended with argument"""
f_name = '%s_%s'%(f_name,s)
ss = '%s.aig'%(f_name)
print 'WRITING %s: '%ss,
ps()
abc('w '+ss)
def bmc_depth():
""" Finds the number of BMC frames that the latest operation has used. The operation could be BMC, reachability
interpolation, abstract, speculate. max_bmc is continually increased. It reflects the maximum depth of any version of the circuit
including g ones, for which it is known that there is not cex out to that depth."""
global max_bmc
c = cex_frame()
if c > 0:
b = c-1
else:
b = n_bmc_frames()
max_bmc = max(b,max_bmc)
return max_bmc
def set_max_bmc(b):
""" Keeps increasing max_bmc which is the maximum number of time frames for
which the current circuit is known to be UNSAT for"""
global max_bmc
max_bmc = max(b,max_bmc)
def print_circuit_stats():
"""Stardard way of outputting statistice about the current circuit"""
global max_bmc
i = n_pis()
o = n_pos()
l = n_latches()
a = n_ands()
b = max(max_bmc,bmc_depth())
c = cex_frame()
if b>= 0:
if c>=0:
print 'PIs=%d,POs=%d,FF=%d,ANDs=%d,max depth=%d,CEX depth=%d'%(i,o,l,a,b,c)
elif is_unsat():
print 'PIs=%d,POs=%d,FF=%d,ANDs=%d,max depth = infinity'%(i,o,l,a)
else:
print 'PIs=%d,POs=%d,FF=%d,ANDs=%d,max depth=%d'%(i,o,l,a,b)
else:
if c>=0:
print 'PIs=%d,POs=%d,FF=%d,ANDs=%d,CEX depth=%d'%(i,o,l,a,c)
else:
print 'PIs=%d,POs=%d,FF=%d,ANDs=%d'%(i,o,l,a)
def q():
exit()
def is_unsat():
if prob_status() == 1:
return True
else:
return False
def is_sat():
if prob_status() == 0:
return True
else:
return False
def wc(file):
"""writes <file> so that costraints are preserved explicitly"""
abc('&get;&w %s'%file)
def rc(file):
"""reads <file> so that if constraints are explicit, it will preserve them"""
abc('&r %s;&put'%file)
#more complex functions: ________________________________________________________
#, abstract, pba, speculate, final_verify, dprove3
def timer(s):
btime = time.clock()
abc(s)
print 'time = %f'%(time.clock() - btime)
def med_simp():
x = time.time()
abc("&get;&scl;&dc2;&lcorr;&dc2;&scorr;&fraig;&dc2;&put;dr")
#abc("dc2rs")
ps()
print 'time = %f'%(time.time() - x)
def simplify():
"""Our standard simplification of logic routine. What it does depende on the problem size.
For large problems, we use the &methods which use a simple circuit based SAT solver. Also problem
size dictates the level of k-step induction done in 'scorr' The stongest simplification is done if
n_ands < 20000. Then it used the clause based solver and k-step induction where |k| depends
on the problem size """
set_globals()
abc('&get;&scl;&lcorr;&put')
n =n_ands()
p_40 = False
if (40000 < n and n < 100000):
p_40 = True
abc("&get;&dc2;&put;dr;&get;&lcorr;&dc2;&put;dr;&get;&scorr;&fraig;&dc2;&put;dr")
n = n_ands()
if n<60000:
abc("&get;&scorr -F 2;&put;dc2rs")
else: # n between 60K and 100K
abc("dc2rs")
n = n_ands()
if (30000 < n and n <= 40000):
if not p_40:
abc("&get;&dc2;&put;dr;&get;&lcorr;&dc2;&put;dr;&get;&scorr;&fraig;&dc2;&put;dr")
abc("&get;&scorr -F 2;&put;dc2rs")
else:
abc("dc2rs")
n = n_ands()
if n <= 30000:
abc('scl -m;drw;dr;lcorr;drw;dr')
nn = max(1,n)
m = int(min( 60000/nn, 16))
if m >= 1:
j = 1
while j <= m:
set_size()
if j<8:
abc('dc2')
else:
abc('dc2rs')
abc('scorr -C 5000 -F %d'%j)
if check_size():
break
j = 2*j
continue
return get_status()
def simulate2(t):
"""Does rarity simulation. Simulation is restricted by the amount
of memory it might use. At first wide but shallow simulation is done, followed by
successively more narrow but deeper simulation.
seed is globally initiallized to 113 when a new design is read in"""
global x_factor, f_name, tme, seed
btime = time.clock()
diff = 0
while True:
f = 5
w = 255
for k in range(9): #this controls how deep we go
f = min(f *2, 3500)
w = max(((w+1)/2)-1,1)
abc('sim3 -m -F %d -W %d -R %d'%(f,w,seed))
seed = seed+23
if is_sat():
return 'SAT'
if ((time.clock()-btime) > t):
return 'UNDECIDED'
def simulate(t):
abc('&get')
result = eq_simulate(t)
return result
def eq_simulate(t):
"""Simulation is restricted by the amount
of memory it might use. At first wide but shallow simulation is done, followed by
successively more narrow but deeper simulation. The aig to be simulated must be in the & space
If there are equivalences, it will refine them. Otherwise it is a normal similation
seed is globally initiallized to 113 when a new design is read in"""
global x_factor, f_name, tme, seed
btime = time.clock()
diff = 0
while True:
f = 5
w = 255
for k in range(9):
f = min(f *2, 3500)
r = f/20
w = max(((w+1)/2)-1,1)
## abc('&sim3 -R %d -W %d -N %d'%(r,w,seed))
abc('&sim -F %d -W %d -R %d'%(f,w,seed))
seed = seed+23
if is_sat():
return 'SAT'
if ((time.clock()-btime) > t):
return 'UNDECIDED'
def generate_abs(n):
"""generates an abstracted model (gabs) from the greg file. The gabs file is automatically
generated in the & space by &abs_derive. We store it away using the f_name of the problem
being solved at the moment. The f_name keeps changing with an extension given by the latest
operation done - e.g. smp, abs, spec, final, group. """
global f_name
#we have a cex and we use this generate a new gabs file
abc('&r %s_greg.aig; &abs_derive; &put; w %s_gabs.aig'%(f_name,f_name)) # do we still need the gabs file
if n == 1:
#print 'New abstraction: ',
ps()
return
def refine_with_cex():
"""Refines the greg (which contains the original problem with the set of FF's that have been abstracted).
This uses the current cex to modify the greg file to reflect which regs are in the
new current abstraction"""
global f_name
#print 'CEX in frame %d for output %d'%(cex_frame(),cex_po())
#abc('&r %s_greg.aig; &abs_refine -t; &w %s_greg.aig'%(f_name,f_name))
abc('&r %s_greg.aig;&w %s_greg_before.aig'%(f_name,f_name))
## run_command('&abs_refine -s -M 25; &w %s_greg.aig'%f_name)
run_command('&abs_refine -s; &w %s_greg.aig'%f_name)
#print ' %d FF'%n_latches()
return
def abstraction_refinement(latches_before,NBF):
"""Subroutine of 'abstract' which does the refinement of the abstracted model,
using counterexamples found by BMC or BDD reachability"""
global x_factor, f_name, last_verify_time, x, win_list, last_winner, last_cex, t_init, j_last, sweep_time
global cex_list, last_cx
sweep_time = 2
if NBF == -1:
F = 2000
else:
F = 2*NBF
print '\nIterating abstraction refinement'
J = slps+intrps+pdrs+bmcs+sims
print sublist(methods,J)
last_verify_time = t = x_factor*max(50,max(1,2.5*G_T))
initial_verify_time = last_verify_time = t
reg_verify = True
print 'Verify time set to %d'%last_verify_time
while True: #cex based refinement
generate_abs(1) #generate new gabs file from refined greg file
set_globals()
latches_after = n_latches()
if rel_cost_t([pis_before_abs,latches_before_abs, ands_before_abs])> -.1:
break
if latches_after >= .90*latches_before:
break
t = last_verify_time
yy = time.time()
abc('w %s_beforerpm.aig'%f_name)
rep_change = reparam() #new - must do reconcile after to make cex compatible
abc('w %s_afterrpm.aig'%f_name)
if reg_verify:
status = verify(J,t)
else:
status = pord_1_2(t)
###############
if status == Sat_true:
print 'Found true cex'
reconcile(rep_change)
return Sat_true
if status == Unsat:
return status
if status == Sat:
reconcile(rep_change) # makes the cex compatible with original before reparam and puts original in work space
abc('write_status %s_before.status'%f_name)
refine_with_cex()
if is_sat(): # if cex can't refine, status is set to Sat_true
print 'Found true cex in output %d'%cex_po()
return Sat_true
else:
continue
else:
break
print '**** Latches reduced from %d to %d'%(latches_before, n_latches())
return Undecided_reduction
def abstract():
""" abstracts using N Een's method 3 - cex/proof based abstraction. The result is further refined using
simulation, BMC or BDD reachability"""
global G_C, G_T, latches_before_abs, x_factor, last_verify_time, x, win_list, j_last, sims
global latches_before_abs, ands_before_abs, pis_before_abs
j_last = 0
set_globals()
#win_list = []
latches_before_abs = n_latches()
ands_before_abs = n_ands()
pis_before_abs = n_real_inputs()
abc('w %s_before_abs.aig'%f_name)
print 'Start: ',
ps()
funcs = [eval('(pyabc_split.defer(initial_abstract)())')]
# fork off BMC3 and PDRm along with initial abstraction
t = 10000 #want to run as long as initial abstract takes.
## J = sims+pdrs+bmcs+intrps
J = pdrs+bmcs+bestintrps
if n_latches() < 80:
J = J + [4]
funcs = create_funcs(J,t) + funcs
mtds = sublist(methods,J) + ['initial_abstract'] #important that initial_abstract goes last
m,NBF = fork_last(funcs,mtds)
if is_sat():
print 'Found true counterexample in frame %d'%cex_frame()
return Sat_true
if is_unsat():
return Unsat
set_max_bmc(NBF)
NBF = bmc_depth()
print 'Abstraction good to %d frames'%max_bmc
#note when things are done in parallel, the &aig is not restored!!!
abc('&r %s_greg.aig; &w initial_greg.aig; &abs_derive; &put; w initial_gabs.aig; w %s_gabs.aig'%(f_name,f_name))
set_max_bmc(NBF)
print 'Initial abstraction: ',
ps()
abc('w %s_init_abs.aig'%f_name)
latches_after = n_latches()
## if latches_after >= .90*latches_before_abs:
if ((rel_cost_t([pis_before_abs, latches_before_abs, ands_before_abs])> -.1) or (latches_after >= .90*latches_before_abs)):
abc('r %s_before_abs.aig'%f_name)
print "Little reduction!"
return Undecided_no_reduction
sims_old = sims
sims=sims[:1] #make it so that rarity sim is not used since it can't find a cex
result = abstraction_refinement(latches_before_abs, NBF)
sims = sims_old
if result <= Unsat:
return result
## if n_latches() >= .90*latches_before_abs:
if ((rel_cost_t([pis_before_abs, latches_before_abs, ands_before_abs])> -.1) or (latches_after >= .90*latches_before_abs)):
## if rel_cost_t([pis_before_abs,latches_before_abs, ands_before_abs])> -.1:
abc('r %s_before_abs.aig'%f_name) #restore original file before abstract.
print "Little reduction!"
result = Undecided_no_reduction
return result
def initial_abstract_old():
global G_C, G_T, latches_before_abs, x_factor, last_verify_time, x, win_list
set_globals()
time = max(1,.1*G_T)
abc('&get;,bmc -vt=%f'%time)
set_max_bmc(bmc_depth())
c = 2*G_C
f = max(2*max_bmc,20)
b = min(max(10,max_bmc),200)
t = x_factor*max(1,2*G_T)
s = min(max(3,c/30000),10) # stability between 3 and 10
cmd = '&get;,abs -bob=%d -stable=%d -timeout=%d -vt=%d -depth=%d'%(b,s,t,t,f)
## print cmd
print 'Running initial_abstract with bob=%d,stable=%d,time=%d,depth=%d'%(b,s,t,f)
abc(cmd)
abc('&w %s_greg.aig'%f_name)
## ps()
def initial_abstract():
global G_C, G_T, latches_before_abs, x_factor, last_verify_time, x, win_list, max_bmc
set_globals()
time = max(1,.1*G_T)
abc('&get;,bmc -vt=%f'%time)
set_max_bmc(bmc_depth())
c = 2*G_C
f = max(2*max_bmc,20)
b = min(max(10,max_bmc),200)
t = x_factor*max(1,2*G_T)
s = min(max(3,c/30000),10) # stability between 3 and 10
cmd = '&get;,abs -bob=%d -stable=%d -timeout=%d -vt=%d -depth=%d'%(b,s,t,t,f)
## print cmd
print 'Running initial_abstract with bob=%d,stable=%d,time=%d,depth=%d'%(b,s,t,f)
abc(cmd)
bmc_depth()
## pba_loop(max_bmc+1)
abc('&w %s_greg.aig'%f_name)
return max_bmc
def abs_m():
set_globals()
y = time.time()
nl = n_abs_latches() #initial set of latches
c = 2*G_C
t = x_factor*max(1,2*G_T) #total time
bmd = bmc_depth()
if bmd < 0:
abc('bmc3 -T 2') #get initial depth estimate
bmd = bmc_depth()
f = bmd
abc('&get')
y = time.time()
cmd = '&abs_cba -v -C %d -T %0.2f -F %d'%(c,.8*t,bmd) #initial absraction
## print '\n%s'%cmd
abc(cmd)
b_old = b = n_bmc_frames()
f = min(2*bmd,max(bmd,1.6*b))
print 'cba: latches = %d, depth = %d'%(n_abs_latches(),b)
## print n_bmc_frames()
while True:
if (time.time() - y) > .9*t:
break
nal = n_abs_latches()
cmd = '&abs_cba -v -C %d -T %0.2f -F %d'%(c,.8*t,f) #f is 2*bmd and is the maximum number of frames allowed
## print '\n%s'%cmd
abc(cmd)
## print n_bmc_frames()
b_old = b
b = n_bmc_frames()
nal_old = nal
nal = n_abs_latches() #nal - nal_old is the number of latches added by cba
#b - b_old is the additional time frames added by cba
f = min(2*bmd,max(bmd,1.6*b)) #may be this should just be bmd
f = max(f,1.5*bmd)
print 'cba: latches = %d, depth = %d'%(nal,b)
if ((nal == nal_old) and (b >= 1.5*b_old) and b >= 1.5*bmd):
"""
Went at least bmd depth and saw too many frames without a cex
(ideally should know how many frames without a cex)
"""
print 'Too many frames without cex'
break
if b > b_old: #if increased depth
continue
if nal > .9*nl: # try to minimize latches
## cmd = '&abs_pba -v -S %d -F %d -T %0.2f'%(b,b+2,.2*t)
cmd = '&abs_pba -v -F %d -T %0.2f'%(b+2,.2*t)
## print '\n%s'%cmd
abc(cmd)
b = n_bmc_frames()
nal_old = nal
nal = n_abs_latches()
print 'pba: latches = %d, depth = %d'%(nal,b)
## print n_bmc_frames()
if nal_old < nal: #if latches increased there was a cex
continue
if nal > .9*nl: # if still too big
return
continue
## b = n_bmc_frames()
cmd = '&abs_pba -v -F %d -T %0.2f'%(b+2,.2*t)
## print '\n%s'%cmd
abc(cmd)
b = n_bmc_frames()
print 'pba: latches = %d, depth = %d'%(n_abs_latches(),b)
## print n_bmc_frames()
print 'Total time = %0.2f'%(time.time()-y)
def n_abs_latches():
abc('&w pba_temp.aig') #save the &space
abc('&abs_derive;&put')
abc('&r pba_temp.aig')
return n_latches()
def pba_loop(F):
n = n_abs_latches()
while True:
run_command('&abs_pba -v -C 100000 -F %d'%F)
abc('&w pba_temp.aig')
abc('&abs_derive;&put')
abc('&r pba_temp.aig')
N = n_latches()
## if n == N or n == N+1:
## break
## elif N > n:
if N > n:
print 'cex found'
break
## else:
## break
##def sec_m(options):
## """
## This assumes that a miter has been loaded into the workspace. The miter has been
## constructed using &miter. Then we demiter it using command 'demiter'
## This produces parts 0 and 1, renamed A_name, and B_name.
## We then do speculate immediately. Options are passed to &srm2 using the
## options given by sec_options
## """
## global f_name,sec_sw, A_name, B_name, sec_options
## A_name = f_name+'_part0'
## B_name = f_name+'_part1'
## run_command('demiter')
## #simplify parts A and B here?
## abc('r %s_part1.aig;scl;dc2;&get;&lcorr;&scorr;&put;dc2;dc2;w %s_part1.aig'%(f_name,f_name))
## ps()
## abc('r %s_part0.aig;scl;dc2;&get;&lcorr;&scorr;&put;dc2;dc2;w %s_part0.aig'%(f_name,f_name))
## ps()
## #simplify done
## f_name = A_name
## return sec(B_name,options)
def ss(options):
"""Alias for super_sec"""
global max_bmc, init_initial_f_name, initial_f_name,win_list, last_verify_time, sec_options
sec_options = options
print 'Executing speculate'
result = speculate()
return result
def quick_sec(t):
## fb_name = f_name[:-3]+'New'
## abc('&get;&miter -s %s.aig;&put'%fb_name)
## abc('w %s.%s_miter.aig'%(f_name,fb_name))
quick_simp()
verify(slps+ pdrs+bmcs+intrps,t)
if is_unsat():
return 'UNSAT'
if is_sat():
return 'SAT'
else:
return'UNDECIDED'
def pp_sec():
print 'First file: ',
read_file_quiet()
ps()
abc('&w original_secOld.aig')
print 'Second file: ',
read_file_quiet()
ps()
abc('&w original_secNew.aig')
def sup_sec():
global TERM
"""
form miter of original_sec(Old,New), and then run in parallel quick_sec(28), speculate(29), and
run_parallel(21) with JP set to
"""
global f_name,sec_sw, A_name, B_name, sec_options
#preprocess files to get rid of dangling FF
abc('&r original_secOld.aig;&scl -ce;&w Old.aig')
abc('&r original_secNew.aig;&scl -ce;&w New.aig')
#done preprocessing
read_file_quiet('Old')
abc('&get;&miter -s New.aig;&put')
set_globals()
yy = time.time()
A_name = f_name # Just makes it so that we can refer to A_name later in &srm2
B_name = 'New'
f_name = 'miter'
abc('w %s.aig'%f_name)
sec_options = 'l'
sec_sw = True
JP = [18,27] # sleep and simplify. JP sets the things run in parallel in method 21.
#TERM sets the stopping condition
TERM = 'USL' #Sat, Unsat or Last
print sublist(methods,[27,21,28,29]+JV)
t = 100 #this is the amount of time to run
#18 is controlled by t, 28(speculate) is not, 29(quick_sec) does quick_simp and then controlled by t
run_parallel([21,28,29],t,'US') #21 is run_parallel with JP and TERM.
#run simplify for t sec, speculate,
#and quick_sec (quick_simp and then verify(JV) for t)
if is_unsat():
return 'UNSAT'
if is_sat():
return 'SAT'
else:
return 'UNDECIDED' # should do sp or something
def sec(B_part,options):
"""
This assumes that the original aig (renamed A_name below) is already read into the working space.
Then we form a miter using &miter between two circuits, A_name, and B_name.
We then do speculate immediately. Optionally we could simplify A and B
and then form the miter and start from there. The only difference in speculate
is that &srm2 is used, which only looks at equivalences where one comes from A and
one from B. Options are -a and -b which says use only flops in A or in B or both. The
switch sec_sw controls what speculate does when it generates the SRM.
"""
global f_name,sec_sw, A_name, B_name, sec_options
yy = time.time()
A_name = f_name # Just makes it so that we can refer to A_name later in &srm2
B_name = B_part
run_command('&get; &miter -s %s.aig; &put'%B_name)
## abc('orpos')
f_name = A_name+'.'+B_name+'_miter' # reflect that we are working on a miter.
abc('w %s.aig'%f_name)
print 'Miter = ',
ps()
## result = pre_simp()
## write_file('smp')
## if result <= Unsat:
## return RESULT[result]
sec_options = options
if sec_options == 'ab':
sec_options = 'l' #it will be changed to 'ab' after &equiv
sec_sw = True
result = speculate() #should do super_sec here.
sec_options = ''
sec_sw = False
if result <= Unsat:
result = RESULT[result]
else:
result = sp()
print 'Total time = %d'%(time.time() - yy)
return result
def filter(opts):
global A_name,B_name
""" This is for filter which effectively only recognizes options -f -g"""
if (opts == '' or opts == 'l'): #if 'l' this is used only for initial &equiv2 to get initial equiv creation
return
if opts == 'ab':
run_command('&filter -f %s.aig %s.aig'%(A_name,B_name))
return
if not opts == 'f':
opts = 'g'
run_command('&filter -%s'%opts)
def check_if_spec_first():
global sec_sw, A_name, B_name, sec_options, po_map
set_globals()
t = max(1,.5*G_T)
r = max(1,int(t))
abc('w check_save.aig')
abc('&w check_and.aig')
abc("&get; &equiv3 -v -F 20 -T %f -R %d"%(t,5*r))
filter('g')
abc("&srm; r gsrm.aig")
print 'Estimated # POs = %d for initial speculation'%n_pos()
result = n_pos() > max(50,.25*n_latches())
abc('r check_save.aig')
abc('&r check_and.aig')
return result
def initial_speculate():
global sec_sw, A_name, B_name, sec_options, po_map
set_globals()
t = max(1,.5*G_T)
r = max(1,int(t))
## print 'Running &equiv3'
## abc('&w before3.aig')
if sec_options == 'l':
cmd = "&get; &equiv3 -lv -F 20 -T %f -R %d"%(3*t,15*r)
else:
cmd = "&get; &equiv3 -v -F 20 -T %f -R %d"%(3*t,15*r)
## print cmd
abc(cmd)
## print 'AND space after &equiv3: ',
## run_command('&ps')
if (sec_options == 'l'):
if sec_sw:
sec_options = 'ab'
else:
sec_options = 'f'
print sec_options
filter(sec_options)
abc('&w initial_gore.aig')
## print 'Running &srm'
if sec_sw:
cmd = "&srm2 -%s %s.aig %s.aig; r gsrm.aig; w %s_gsrm.aig; &w %s_gore.aig"%(sec_options,A_name,B_name,f_name,f_name)
abc(cmd)
po_map = range(n_pos())
return
else:
cmd = "&srm; r gsrm.aig; w %s_gsrm.aig; &w %s_gore.aig"%(f_name,f_name)
abc(cmd)
if (n_pos() > 100):
sec_options = 'g'
print 'sec_option changed to "g"'
filter(sec_options)
abc(cmd)
po_map = range(n_pos())
def test_against_original():
'''tests whether we have a cex hitting an original PO'''
abc('&w %s_save.aig'%f_name) #we oreserve whatever was in the & space
abc('&r %s_gore.aig'%f_name)
abc('testcex')
PO = cex_po()
abc('&r %s_save.aig'%f_name)
if PO > -1:
## print 'cex fails an original PO'
return True
else:
return False
def set_cex_po(n=0):
"""
if cex falsifies a non-real PO return that PO first,
else see if cex_po is one of the original, then take it next
else return -1 which means that the cex is not valid and hence an error.
parameter n = 1 means test the &-space
"""
global n_pos_before, n_pos_proved #these refer to real POs
if n == 0:
abc('testcex -a -O %d'%(n_pos_before-n_pos_proved))
else:
abc('testcex -O %d'%(n_pos_before-n_pos_proved))
PO = cex_po()
if PO >= (n_pos_before - n_pos_proved): #cex_po is not an original
## print 'cex PO = %d'%PO
return PO # after original so take it.
if n == 0:
abc('testcex -a')
else:
abc('testcex')
PO = cex_po()
cx = cex_get()
if PO > -1:
if test_against_original(): #this double checks that it is really an original PO
cex_put(cx)
return PO
else:
return -1 #error
## if PO < 0 or PO >= (n_pos_before - n_pos_proved): # not a valid cex because already tested outside original.
## PO = -1 #error
return PO
## print 'cex PO = %d'%PO
def speculate():
"""Main speculative reduction routine. Finds candidate sequential equivalences and refines them by simulation, BMC, or reachability
using any cex found. """
global G_C,G_T,n_pos_before, x_factor, n_latches_before, last_verify_time, trim_allowed, n_pos_before
global t_init, j_last, sec_sw, A_name, B_name, sec_options, po_map, sweep_time, sims, cex_list, n_pos_proved,ifpord1
global last_cx
last_cx = 0
ifpord1 = 1
if sec_sw:
print 'A_name = %s, B_name = %s, f_name = %s, sec_options = %s'%(A_name, B_name, f_name, sec_options)
elif n_ands()> 6000 and sec_options == '':
sec_options = 'g'
print 'sec_options set to "g"'
def refine_with_cex():
"""Refines the gore file to reflect equivalences that go away because of cex"""
global f_name
## print 'Refining',
## abc('&r %s_gore.aig;&w %s_gore_before.aig'%(f_name,f_name))
abc('write_status %s_before.status'%f_name)
abc('&r %s_gore.aig; &resim -m'%f_name)
filter(sec_options)
run_command('&w %s_gore.aig'%f_name)
return
## def refine_with_cexs():
## """Refines the gore file to reflect equivalences that go away because of cexs in cex_list"""
## global f_name, cex_list
## print 'Multiple refining'
## abc('&r %s_gore.aig'%f_name)
#### run_command('&ps')
## for j in range(len(cex_list)):
## cx = cex_list[j]
## if cx == None:
## continue
## cex_put(cx)
## run_command('&resim -m') #put the jth cex into the cex space and use it to refine the equivs
## filter(sec_options)
## abc('&w %s_gore.aig'%f_name)
#### run_command('&ps')
## cex_list = [] #done with this list.
## return
def set_cex(lst):
""" assumes only one in lst """
for j in range(len(lst)):
cx = lst[j]
if cx == None:
continue
else:
cex_put(cx)
break
## def test_all_cexs(lst):
## """tests all cex"s to see if any violate original POs
## if it does, return the original PO number
## if not return -1
## """
## global n_pos_before, cex_list
## run_command('&r %s_gore.aig'%f_name)
## for j in range(len(cex_list)):
## cx = lst[j]
## if cx == None:
## continue
## cex_put(cx)
## PO = set_cex_po() #if cex falsifies non-real PO it will set this first
## if PO == -1: # there is a problem with cex since it does not falsify any PO
## continue #we continue because there may be another valid cex in list
## return PO #we will only process one cex for now.
## return -1 #a real PO is not falsified by any of the cexs
def generate_srm():
"""generates a speculated reduced model (srm) from the gore file"""
global f_name, po_map, sec_sw, A_name, B_name, sec_options, n_pos_proved
## print 'Generating'
pos = n_pos()
ab = n_ands()
if sec_sw:
run_command('&r %s_gore.aig; &srm2 -%s %s.aig %s.aig; r gsrm.aig; w %s_gsrm.aig'%(f_name,sec_options,A_name,B_name,f_name))
else:
abc('&r %s_gore.aig; &srm ; r gsrm.aig; w %s_gsrm.aig'%(f_name,f_name)) #do we still need to write the gsrm file
## ps()
po_map = range(n_pos())
## cmd = '&get;&lcorr;&scorr;&trim -i;&put;w %s_gsrm.aig'%f_name
## cmd = 'lcorr;&get;&trim -i;&put;w %s_gsrm.aig'%f_name
## print 'Executing %s'%cmd
## abc(cmd)
ps()
n_pos_proved = 0
return 'OK'
n_pos_before = n_pos()
n_pos_proved = 0
n_latches_before = n_latches()
set_globals()
t = max(1,.5*G_T)#irrelevant
r = max(1,int(t))
j_last = 0
J = sims+pdrs+bmcs+intrps
funcs = [eval('(pyabc_split.defer(initial_speculate)())')]
funcs = create_funcs(J,10000)+funcs #want other functins to run until initial speculate stops
mtds = sublist(methods,J) + ['initial_speculate'] #important that initial_speculate goes last
fork_last(funcs,mtds)
## ps()
if is_unsat():
return Unsat
if is_sat():
return Sat_true
if n_pos_before == n_pos():
print 'No new outputs. Quitting speculate'
return Undecided_no_reduction # return result is unknown
## cmd = 'lcorr;&get;&trim -i;&put;w %s_gsrm.aig'%f_name
#print 'Executing %s'%cmd
abc('w initial_gsrm.aig')
## ps()
## abc(cmd)
print 'Initial speculation: ',
ps()
if n_latches() == 0:
return check_sat()
if sec_options == 'l' and sec_sw:
sec_options = 'ab' #finished with initial speculate with the 'l' option
print "sec_options set to 'ab'"
elif sec_options == 'l':
sec_options = 'f'
print "sec_options set to 'f'"
po_map = range(n_pos()) #we need this because the initial_speculate is done in parallel and po_map is not passed back.
npi = n_pis()
set_globals()
if is_sat():
return Sat_true
simp_sw = init = True
print '\nIterating speculation refinement'
sims_old = sims
sims = sims[:1] #make it so rarity simulation is not used since it can't find a cex.
J = slps+sims+pdrs+intrps+bmcs
print sublist(methods,J)
t = max(50,max(1,2*G_T))
last_verify_time = t
print 'Verify time set to %d'%last_verify_time
reg_verify = True
ref_time = time.time()
sweep_time = 2
ifpord1=1
while True: # refinement loop
set_globals()
yy = time.time()
if not init:
abc('r %s_gsrm.aig'%f_name) #this is done only to set the size of the previous gsrm.
abc('w %s_gsrm_before.aig'%f_name)
set_size()
result = generate_srm()
yy = time.time()
# if the size of the gsrm did not change after generating a new gsrm
# and if the cex is valid for the gsrm, then the only way this can happen is if
# the cex_po is an original one.
if check_size(): #same size before and after
if check_cex(): #valid cex failed to refine possibly
if 0 <= cex_po() and cex_po() < (n_pos_before - n_pos_proved): #original PO
print 'Found cex in original output = %d'%cex_po()
print 'Refinement time = %s'%convert(time.time() - ref_time)
return Sat_true
elif check_same_gsrm(f_name): #if two gsrms are same, then failed to refine
print 'CEX failed to refine'
return Error
else:
print 'not a valid cex'
return Error
if n_latches() == 0:
print 'Refinement time = %s'%convert(time.time() - ref_time)
return check_sat()
init = False # make it so that next time it is not the first time through
if not t == last_verify_time: # heuristic that if increased last verify time,
# then try pord_all
t = last_verify_time
if reg_verify:
t_init = (time.time() - yy)/2 #start poor man's concurrency at last cex fime found
t_init = min(10,t_init)
reg_verify = False #will cause pord_all to be used next
print 'pord_all turned on'
t = last_verify_time
print 'Verify time set to %d'%t
abc('w %s_beforerpm.aig'%f_name)
rep_change = reparam() #must be paired with reconcile below if cex
abc('w %s_afterrpm.aig'%f_name)
if reg_verify:
result = verify(J,t)
else:
result = pord_1_2(t)
if result == Unsat:
print 'UNSAT'
print 'Refinement time = %s'%convert(time.time() - ref_time)
return Unsat
if result < Unsat:
if not reg_verify:
set_cex(cex_list)
## if reg_verify:
reconcile(rep_change) #end of pairing with reparam()
assert (npi == n_cex_pis()),'ERROR: #pi = %d, #cex_pi = %d'%(npi,n_cex_pis())
abc('&r %s_gore.aig;&w %s_gore_before.aig'%(f_name,f_name)) #we are making sure that none of the original POs fail
PO = set_cex_po() #testing the &space
if (-1 < PO and PO < (n_pos_before-n_pos_proved)):
print 'Found cex in original output = %d'%cex_po()
print 'Refinement time = %s'%convert(time.time() - ref_time)
return Sat_true
if PO == -1:
return Error
refine_with_cex() #change the number of equivalences
continue
## else: # we used pord_all()
## cex_list = reconcile_all(cex_list, rep_change) #end of pairing with reparam()
## PO = test_all_cexs(cex_list) #we have to make sure that none of the cex's fail the original POs.
## if 0 <= PO and PO < (n_pos_before - n_pos_proved):
## print 'PO = %d, n_pos_before = %d, n_pos_proved = %d'%(PO,n_pos_before, n_pos_proved)
## print 'Found one of cexs in original output = %d'%cex_po()
## print 'Refinement time = %0.2f'%(time.time() - ref_time)
## return Sat_true
## if PO == -1:
## return Error
## refine_with_cexs()
## continue
elif (is_unsat() or n_pos() == 0):
print 'UNSAT'
print 'Refinement time = %s'%convert(time.time() - ref_time)
return Unsat
else: #if undecided, record last verification time
print 'Refinement returned undecided in %d sec.'%t
last_verify_time = t
#########################added
if reg_verify: #try one last time with parallel POs cex detection (find_cex_par) if not already tried
abc('r %s_beforerpm.aig'%f_name) # to continue refinement, need to restore original
t_init = min(last_verify_time,(time.time() - yy)/2) #start poor man's concurrency at last cex fime found
t_init = min(10,t_init)
reg_verify = False
t = last_verify_time # = 2*last_verify_time
abc('w %s_beforerpm.aig'%f_name)
rep_change = reparam() #must be paired with reconcile()below
abc('w %s_afterrpm.aig'%f_name)
result = pord_1_2(t) #main call to verification
if result == Unsat:
print 'UNSAT'
print 'Refinement time = %s'%convert(time.time() - ref_time)
return Unsat
if is_sat():
assert result == get_status(),'result: %d, status: %d'%(result,get_status())
set_cex(cex_list)
reconcile(rep_change)
PO = set_cex_po() #testing the &space
if (-1 < PO and PO < (n_pos_before-n_pos_proved)):
print 'Found cex in original output = %d'%cex_po()
print 'Refinement time = %s'%convert(time.time() - ref_time)
return Sat_true
if PO == -1:
return Error
refine_with_cex() #change the number of equivalences
continue
## cex_list = reconcile_all(cex_list, rep_change) #end of pairing with reparam()
## PO = test_all_cexs(cex_list) #we have to make sure that none of the cex's fail the original POs.
## if 0 <= PO and PO < (n_pos_before - n_pos_proved):
## print 'found SAT in true output = %d'%cex_po()
## print 'Refinement time = %s'%convert(time.time() - ref_time)
## return Sat_true
## if PO == -1:
## return Error
## refine_with_cexs()#change the number of equivalences
## continue
elif is_unsat():
print 'UNSAT'
print 'Refinement time = %s'%convert(time.time() - ref_time)
return Unsat
else: #if undecided, record last verification time
last_verify_time = t
print 'UNDECIDED'
break
################### added
else:
break
sims = sims_old
print 'UNDECIDED'
print 'Refinement time = %s'%convert(time.time() - ref_time)
write_file('spec')
if n_pos_before == n_pos():
return Undecided_no_reduction
else:
return Undecided_reduction
def simple_bip(t=1000):
y = time.time()
J = [0,1,2,30,5] #5 is pre_simp
funcs = create_funcs(J,t)
mtds =sublist(methods,J)
fork_last(funcs,mtds)
result = get_status()
if result > Unsat:
write_file('smp')
result = verify(slps+[0,1,2,30],t)
print 'Time for simple_bip = %0.2f'%(time.time()-y)
return RESULT[result]
def simple_prove(t=1000):
y = time.time()
J = [7,9,23,30,5]
funcs = create_funcs(J,t)
mtds =sublist(methods,J)
fork_last(funcs,mtds)
result = get_status()
if result > Unsat:
write_file('smp')
result = verify(slps+[7,9,23,30],t)
print 'Time for simple_prove = %0.2f'%(time.time()-y)
return RESULT[result]
def check_same_gsrm(f):
## return False #disable the temporarily until can figure out why this is there
"""checks gsrm miters before and after refinement and if equal there is an error"""
global f_name
abc('r %s_gsrm.aig'%f)
## ps()
run_command('miter -c %s_gsrm_before.aig'%f)
## ps()
abc('&get; ,bmc -timeout=5')
result = True #if the same
if is_sat(): #if different
result = False
abc('r %s_gsrm.aig'%f)
## ps()
return result
def check_cex():
""" check if the last cex still asserts one of the outputs.
If it does then we have an error"""
global f_name
abc('read_status %s_before.status'%f_name)
abc('&r %s_gsrm_before.aig'%f_name)
## abc('&r %s_gsrm.aig'%f_name)
run_command('testcex')
print 'cex po = %d'%cex_po()
return cex_po() >=0
## if cex_po() == -1: # means gsrm changes after refinement - no output is asserted.
## return False
## else:
## return True
def set_size():
"""Stores the problem size of the current design.
Size is defined as (PIs, POs, ANDS, FF)"""
global npi, npo, nands, nff, nmd
npi = n_pis()
npo = n_pos()
nands = n_ands()
nff = n_latches()
nmd = max_bmc
#print npi,npo,nands,nff
def check_size():
"""Assumes the problem size has been set by set_size before some operation.
This checks if the size was changed
Size is defined as (PIs, POs, ANDS, FF, max_bmc)
Returns TRUE is size is the same"""
global npi, npo, nands, nff, nmd
#print n_pis(),n_pos(),n_ands(),n_latches()
result = ((npi == n_pis()) and (npo == n_pos()) and (nands == n_ands()) and (nff == n_latches()) )
return result
def inferior_size():
"""Assumes the problem size has been set by set_size beore some operation.
This checks if the new size is inferior (larger) to the old one
Size is defined as (PIs, POs, ANDS, FF)"""
global npi, npo, nands, nff
result = ((npi < n_pis()) or (npo < n_pos()) or (nands < n_ands()) )
return result
def quick_verify(n):
"""Low resource version of final_verify n = 1 means to do an initial
simplification first. Also more time is allocated if n =1"""
global last_verify_time
trim()
if n == 1:
simplify()
if n_latches == 0:
return check_sat()
trim()
if is_sat():
return Sat_true
#print 'After trimming: ',
#ps()
set_globals()
last_verify_time = t = max(1,.4*G_T)
if n == 1:
last_verify_time = t = max(1,2*G_T)
print 'Verify time set to %d '%last_verify_time
J = [18] + intrps+bmcs+pdrs+sims
status = verify(J,t)
return status
##def process_status():
## if n_latches() == 0:
## status = check_sat()
## else:
## status = get_status()
## return status
def process_status(status):
""" if there are no FF, the problem is combinational and we still have to check if UNSAT"""
if n_latches() == 0:
return check_sat()
return status
def get_status():
"""this simply translates the problem status encoding done by ABC
(-1,0,1)=(undecided,SAT,UNSAT) into the status code used by our
python code. -1,0,1 => 3,0,2
"""
if n_latches() == 0:
return check_sat()
status = prob_status() #interrogates ABC for the current status of the problem.
# 0 = SAT i.e. Sat_reg = 0 so does not have to be changed.
if status == 1:
status = Unsat
if status == -1: #undecided
status = Undecided
return status
def reparam():
"""eliminates PIs which if used in abstraction or speculation must be restored by
reconcile and the cex made compatible with file beforerpm"""
## return
rep_change = False
n = n_pis()
## abc('w t1.aig')
abc('&get;,reparam -aig=%s_rpm.aig; r %s_rpm.aig'%(f_name,f_name))
## abc('w t2.aig')
## abc('testcex')
if n_pis() == 0:
print 'Number of PIs reduced to 0. Added a dummy PI'
abc('addpi')
nn = n_pis()
if nn < n:
print 'Reparam: PIs %d => %d'%(n,nn)
rep_change = True
return rep_change
def reconcile(rep_change):
"""used to make current cex compatible with file before reparam() was done.
However, the cex may have come
from extracting a single output and verifying this.
Then the cex_po is 0 but the PO it fails could be anything.
So testcex rectifies this."""
global n_pos_before, n_pos_proved
## print 'rep_change = %s'%rep_change
if rep_change == False:
return
abc('&r %s_beforerpm.aig; &w tt_before.aig'%f_name)
abc('write_status %s_after.status;write_status tt_after.status'%f_name)
abc('&r %s_afterrpm.aig;&w tt_after.aig'%f_name)
POa = set_cex_po(1) #this should set cex_po() to correct PO. A 1 here means it uses &space to check
abc('reconcile %s_beforerpm.aig %s_afterrpm.aig'%(f_name,f_name))
# reconcile modifies cex and restores work AIG to beforerpm
abc('write_status %s_before.status;write_status tt_before.status'%f_name)
POb = set_cex_po()
## assert POa == POb, 'cex PO afterrpm = %d, cex PO beforerpm = %d'%(POa,POb)
if POa != POb:
abc('&r %s_beforerpm.aig; &w tt_before.aig'%f_name)
abc('&r %s_afterrpm.aig; &w tt_after.aig'%f_name)
print 'cex PO afterrpm = %d, cex PO beforerpm = %d'%(POa,POb)
## assert POa == POb, 'cex PO afterrpm = %d, cex PO beforerpm = %d'%(POa,POb)
def reconcile_all(lst, rep_change):
"""reconciles the list of cex's"""
global f_name, n_pos_before, n_pos_proved
if rep_change == False:
return lst
list = []
for j in range(len(lst)):
cx = lst[j]
if cx == None:
continue
cex_put(cx)
reconcile(rep_change)
list = list + [cex_get()]
return list
def try_rpm():
"""rpm is a cheap way of doing reparameterization and is an abstraction method, so may introduce false cex's.
It finds a minimum cut between the PIs and the main sequential logic and replaces this cut by free inputs.
A quick BMC is then done, and if no cex is found, we assume the abstraction is valid. Otherwise we revert back
to the original problem before rpm was tried."""
global x_factor
if n_ands() > 30000:
return
set_globals()
pis_before = n_pis()
abc('w %s_savetemp.aig'%f_name)
abc('rpm')
result = 0
if n_pis() < .5*pis_before:
bmc_before = bmc_depth()
#print 'running quick bmc to see if rpm is OK'
t = max(1,.1*G_T)
#abc('bmc3 -C %d, -T %f'%(.1*G_C, t))
abc('&get;,bmc -vt=%f'%t)
if is_sat(): #rpm made it sat by bmc test, so undo rpm
abc('r %s_savetemp.aig'%f_name)
else:
trim()
print 'WARNING: rpm reduced PIs to %d. May make SAT.'%n_pis()
result = 1
else:
abc('r %s_savetemp.aig'%f_name)
return result
def verify(J,t):
"""This method is used for finding a cex during refinement, but can also
be used for proving the property. t is the maximum time to be used by
each engine J is the list of methods to run in parallel. See FUNCS for list"""
global x_factor, final_verify_time, last_verify_time, methods
set_globals()
t = int(max(1,t))
N = bmc_depth()
L = n_latches()
I = n_real_inputs()
## mtds = sublist(methods,J)
#heuristic that if bmc went deep, then reachability might also
if ( ((I+L<350)&(N>100)) or (I+L<260) or (L<80) ):
J = J+reachs
J = remove_intrps(J)
if L < 80:
J=J+[4]
mtds = sublist(methods,J)
print mtds
#print J,t
F = create_funcs(J,t)
(m,result) = fork(F,mtds) #FORK here
assert result == get_status(),'result: %d, status: %d'%(result,get_status())
return result
def check_sat():
"""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"""
if not n_latches() == 0:
print 'circuit is not combinational'
return Undecided
## print 'Circuit is combinational - checking with dsat'
abc('&get') #save the current circuit
abc('orpos;dsat -C %d'%G_C)
if is_sat():
return Sat_true
elif is_unsat():
return Unsat
else:
abc('&put') #restore
return Undecided_no_reduction
def try_era(s):
"""era is explicit state enumeration that ABC has. It only works if the number of PIs is small,
but there are cases where it works and nothing else does"""
if n_pis() > 12:
return
cmd = '&get;&era -mv -S %d;&put'%s
print 'Running %s'%cmd
run_command(cmd)
def try_induction(C):
"""Sometimes proving the property directly using induction works but not very often.
For 'ind' to work, it must have only 1 output, so all outputs are or'ed together temporarily"""
return Undecided_reduction
print '\n***Running induction'
abc('w %s_temp.aig'%f_name)
abc('orpos; ind -uv -C %d -F 10'%C)
abc('r %s_savetemp.aig'%f_name)
status = prob_status()
if not status == 1:
return Undecided_reduction
print 'Induction succeeded'
return Unsat
def final_verify_recur(K):
"""During prove we make backups as we go. These backups have increasing abstractions done, which can cause
non-verification by allowing false counterexamples. If an abstraction fails with a cex, we can back up to
the previous design before the last abstraction and try to proceed from there. K is the backup number we
start with and this decreases as the backups fails. For each backup, we just try final_verify.
If ever we back up to 0, which is the backup just after simplify, we then try speculate on this. This often works
well if the problem is a SEC problem where there are a lot of equivalences across the two designs."""
global last_verify_time
#print 'Proving final_verify_recur(%d)'%K
last_verify_time = 2*last_verify_time
print 'Verify time increased to %d'%last_verify_time
for j in range(K):
i = K-(j+1)
abc('r %s_backup_%d.aig'%(initial_f_name,i))
if ((i == 0) or (i ==2)): #don't try final verify on original last one
status = prob_status()
break
print '\nVerifying backup number %d:'%i,
#abc('r %s_backup_%d.aig'%(initial_f_name,i))
ps()
#J = [18,0,1,2,3,7,14]
J = slps+sims+intrps+bmcs+pdrs
t = last_verify_time
status = verify(J,t)
if status >= Unsat:
return status
if i > 0:
print 'SAT returned, Running less abstract backup'
continue
break
if ((i == 0) and (status > Unsat) and (n_ands() > 0)):
print '\n***Running speculate on initial backup number %d:'%i,
abc('r %s_backup_%d.aig'%(initial_f_name,i))
ps()
if n_ands() < 20000:
## pre_simp()
status = speculate()
if ((status <= Unsat) or (status == Error)):
return status
#J = [18,0,1,2,3,7,14]
J = slps+sims+intrps+bmcs+pdrs
t = 2*last_verify_time
print 'Verify time increased to %d'%last_verify_time
status = verify(J,t)
if status == Unsat:
return status
else:
return Undecided_reduction
def smp():
abc('smp')
write_file('smp')
def dprove():
abc('dprove -cbjupr')
def trim():
global trim_allowed
if not trim_allowed:
return
## abc('trm;addpi')
reparam()
## print 'exiting trim'
def prs():
y = time.clock()
pre_simp()
print 'Time = %s'%convert(time.clock() - y)
write_file('smp')
def pre_simp():
"""This uses a set of simplification algorithms which preprocesses a design.
Includes forward retiming, quick simp, signal correspondence with constraints, trimming away
PIs, and strong simplify"""
global trim_allowed
set_globals()
abc('&get; &scl; &put')
if (n_ands() > 200000 or n_latches() > 50000 or n_pis() > 40000):
print 'Problem too large, simplification skipped'
return 'Undecided'
if ((n_ands() > 0) or (n_latches()>0)):
trim()
## ps()
if n_latches() == 0:
return check_sat()
best_fwrd_min([10,11])
ps()
status = try_scorr_constr()
if ((n_ands() > 0) or (n_latches()>0)):
trim()
if n_latches() == 0:
return check_sat()
status = process_status(status)
if status <= Unsat:
return status
simplify()
print 'Simplify: ',
ps()
if n_latches() == 0:
return check_sat()
if trim_allowed:
t = min(15,.3*G_T)
## try_tempor(t)
try_temps(15)
if n_latches() == 0:
return check_sat()
try_phase()
if n_latches() == 0:
return check_sat()
if ((n_ands() > 0) or (n_latches()>0)):
trim()
status = process_status(status)
if status <= Unsat:
return status
return process_status(status)
def try_scorr_constr():
set_size()
abc('w %s_savetemp.aig'%f_name)
status = scorr_constr()
if inferior_size():
abc('r %s_savetemp.aig'%f_name)
return status
def factors(n):
l = [1,]
nn = n
while n > 1:
for i in (2,3,5,7,11,13,17,19,23,29,31,37,41,43,47,53):
if not i <nn:
break
if n%i == 0:
l = l + [i,]
n = n/i
if not n == 1:
l = l + [n,]
break
return sorted(l)
def select(x,y):
z = []
for i in range(len(x)):
if x[i]:
z = z + [y[i],]
return z
def ok_phases(n):
""" only try those where the resulting n_ands does not exceed 60000"""
f = factors(n)
sp = subproducts(f)
s = map(lambda m:m*n_ands()< 90000,sp)
z = select(s,sp)
return z
def subproducts(ll):
ss = (product(ll),)
#print ll
n = len(ll)
if n == 1:
return ss
for i in range(n):
kk = drop(i,ll)
#print kk
ss = ss+(product(kk),)
#print ss
ss = ss+subproducts(kk)
#print ss
result =tuple(set(ss))
#result.sort()
return tuple(sorted(result))
def product(ll):
n = len(ll)
p = 1
if n == 1:
return ll[0]
for i in range(n):
p = p*ll[i]
return p
def drop(i,ll):
return ll[:i]+ll[i+1:]
def try_phase():
"""Tries phase abstraction. ABC returns the maximum clock phase it found using n_phases.
Then unnrolling is tried up to that phase and the unrolled model is quickly
simplified (with retiming to see if there is a significant reduction.
If not, then revert back to original"""
global init_simp
trim()
n = n_phases()
## if ((n == 1) or (n_ands() > 45000) or init_simp == 0):
if ((n == 1) or (n_ands() > 45000)):
return
## init_simp = 0
print 'Trying phase abstraction - Max phase = %d'%n,
#ps()
## trim()
#ps()
abc('w %s_phase_temp.aig'%f_name)
na = n_ands()
nl = n_latches()
ni = n_pis()
no = n_pos()
z = ok_phases(n)
print z,
if len(z) == 1:
return
#p = choose_phase()
p = z[1]
abc('phase -F %d'%p)
## ps()
#print z
if no == n_pos(): #nothing happened because p is not mod period
print 'Phase %d is incompatible'%p
abc('r %s_phase_temp.aig'%f_name)
if len(z)< 3:
return
else:
p = z[2]
#print 'Trying phase = %d: '%p,
abc('phase -F %d'%p)
if no == n_pos(): #nothing happened because p is not mod period
print 'Phase %d is incompatible'%p
abc('r %s_phase_temp.aig'%f_name)
return
#print 'Trying phase = %d: '%p,
print 'Simplifying with %d phases: => '%p,
simplify()
trim()
ps()
cost = rel_cost([ni,nl,na])
print 'New relative cost = %f'%(cost)
if cost < -.01:
abc('w %s_phase_temp.aig'%f_name)
if ((n_latches() == 0) or (n_ands() == 0)):
return
if n_phases() == 1: #this bombs out if no latches
return
else:
try_phase()
return
elif len(z)>2: #Try the next eligible phase.
abc('r %s_phase_temp.aig'%f_name)
if p == z[2]: #already tried this
return
p = z[2]
print 'Trying phase = %d: => '%p,
abc('phase -F %d'%p)
if no == n_pos(): #nothing happened because p is not mod period
print 'Phase = %d is not compatible'%p
return
ps()
print 'Simplify with %d phases: '%p,
simplify()
trim()
ps()
cost = rel_cost([ni,nl,na])
print 'New relative cost = %f'%(cost)
if cost < -.01:
print 'Phase abstraction with %d phases obtained:'%p,
print_circuit_stats()
abc('w %s_phase_temp.aig'%f_name)
if ((n_latches() == 0) or (n_ands() == 0)):
return
if n_phases() == 1: # this bombs out if no latches
return
else:
try_phase()
return
abc('r %s_phase_temp.aig'%f_name)
#ps()
return
def try_temp(t=15):
btime = time.clock()
trim()
print'Trying temporal decomposition - for max %s sec. '%convert(t),
abc('w %s_best.aig'%f_name)
ni = n_pis()
nl = n_latches()
na = n_ands()
best = [ni,nl,na]
F = create_funcs([18],t) #create a timer function
F = F + [eval('(pyabc_split.defer(abc)("tempor -s; trm; scr; trm; tempor; trm; scr; trm"))')]
for i,res in pyabc_split.abc_split_all(F):
break
cost = rel_cost(best)
print 'Cost = %0.2f'%cost
if cost < .01:
ps()
return
else:
abc('r %s_best.aig'%f_name)
def try_temps(t=15):
best = (n_pis(),n_latches(),n_ands())
while True:
try_temp(t)
if ((best == (n_pis(),n_latches(),n_ands())) or n_ands() > .9 * best[2] ):
break
elif n_latches() == 0:
break
else:
best = (n_pis(),n_latches(),n_ands())
def try_tempor(t):
btime = time.clock()
trim()
print'Trying temporal decomposition - for max %s sec. '%convert(t),
abc('w %s_best.aig'%f_name)
ni = n_pis()
nl = n_latches()
na = n_ands()
best = [ni,nl,na]
F = create_funcs([18],t) #create a timer function
#Caution: trm done in the following removes POs and PIs
## F = F + [eval('(pyabc_split.defer(abc)("tempor -s -C %d; trm; lcr; scr; trm"))'%(2*na))]
## F = F + [eval('(pyabc_split.defer(abc)("tempor -C %d; trm; lcr; scr; trm"))'%(2*na))]
F = F + [eval('(pyabc_split.defer(abc)("tempor -s; trm; lcr; scr; trm"))')]
F = F + [eval('(pyabc_split.defer(abc)("tempor -C; trm; lcr; scr; trm"))')]
n_done = 0
new_best = 0
## debug_here()
for i,res in pyabc_split.abc_split_all(F):
if i == 0:
break
else:
cost = rel_cost(best)
print 'Cost = %0.2f'%cost
if cost < .01:
abc('w %s_best.aig'%f_name)
best = [n_pis(),n_latches(),n_ands()]
new_best = 1
n_done = n_done+1
if n_done == 2:
break
else:
continue
abc('r %s_best.aig'%f_name)
ps()
if new_best == 0: #nothing new
print 'No reduction or timeout occurred'
return
if n_latches() == 0:
return
abc('scr;smp')
trim()
cost = rel_cost_t([ni,nl,na]) #see how much it improved
## print 'rel_cost_t = %0.2f'%cost
if (cost < -.01):
print 'time = %f: '%(time.clock() - btime),
if cost < -1:
print 'Trying second tempor'
try_tempor(t)
print 'Reduction: time=%f'%(time.clock() - btime)
return
else:
print 'No reduction'
return
def rel_cost_t(J):
""" weighted relative costs versus previous stats."""
if n_latches() == 0:
return -10
nli = J[0]+J[1]
na = J[2]
if ((nli == 0) or (na == 0)):
return 100
nri = n_real_inputs()
#ri = (float(nri)-float(ni))/float(ni)
rli = (float(n_latches()+nri)-float(nli))/float(nli)
ra = (float(n_ands())-float(na))/float(na)
## cost = 10*rli + .1*ra
cost = 10*rli + .5*ra
## print 'cost = %0.2f'%c
## print 'cost = %0.2f'%cost
return cost
def rel_cost(J):
""" weighted relative costs versus previous stats."""
global f_name
if n_latches() == 0:
return -10
nri = n_real_inputs()
ni = J[0]
nl = J[1]
na = J[2]
if (ni == 0 or na == 0 or nl == 0):
return 100
ri = (float(nri)-float(ni))/float(ni)
rl = (float(n_latches())-float(nl))/float(nl)
ra = (float(n_ands())-float(na))/float(na)
cost = 1*ri + 10*rl + .1*ra
## print 'Relative cost = %0.2f'%cost
return cost
def best_fwrd_min(J):
global f_name, methods
mtds = sublist(methods,J)
F = create_funcs(J,0)
#print 'Trying forward retiming: running %s in parallel'%(mtds)
(m,result) = fork_best(F,mtds) #FORK here
print '%s: '%mtds[m],
def try_forward():
"""Attempts most forward retiming, and latch correspondence there. If attempt fails to help simplify, then we revert back to the original design
This can be effective for equivalence checking problems where synthesis used retiming"""
abc('w %s_savetemp.aig'%f_name)
if n_ands() < 30000:
abc('dr')
abc('lcorr')
nl = n_latches()
na = n_ands()
abc('w %s_savetemp0.aig'%f_name)
abc('r %s_savetemp.aig'%f_name)
abc('dr -m')
abc('lcorr')
abc('dr')
if ((n_latches() <= nl) and (n_ands() < na)):
print 'Forward retiming reduced size to: ',
print_circuit_stats()
return
else:
abc('r %s_savetemp0.aig'%f_name)
return
return
def quick_simp():
"""A few quick ways to simplify a problem before more expensive methods are applied.
Uses & commands if problem is large. These commands use the new circuit based SAT solver"""
na = n_ands()
if na < 30000:
abc('scl -m;lcorr;drw')
else:
abc('&get;&scl;&lcorr;&put;drw')
def scorr_constr():
"""Extracts implicit constraints and uses them in signal correspondence
Constraints that are found are folded back when done"""
##################### Temporary
# return Undecided_no_reduction
#####################
na = max(1,n_ands())
n_pos_before = n_pos()
if ((na > 40000) or n_pos()>1):
return Undecided_no_reduction
abc('w %s_savetemp.aig'%f_name)
if n_ands() < 3000:
cmd = 'unfold -a -F 2'
else:
cmd = 'unfold'
abc(cmd)
if n_pos() == n_pos_before:
print 'No constraints found'
return Undecided_no_reduction
if (n_ands() > na): #no constraints found
abc('r %s_savetemp.aig'%f_name)
return Undecided_no_reduction
#print_circuit_stats()
na = max(1,n_ands())
## f = 1
f = 18000/na
f = min(f,4)
f = max(1,f)
print 'Number of constraints = %d, frames = %d'%((n_pos() - n_pos_before),f)
abc('scorr -c -F %d'%f)
abc('fold')
trim()
ps()
return Undecided_no_reduction
def try_scorr_c(f):
""" Trying multiple frames because current version has a bug."""
set_globals()
abc('unfold -F %d'%f)
abc('scorr -c -F %d'%f)
abc('fold')
t = max(1,.1*G_T)
abc('&get;,bmc3 -vt=%f'%t)
if is_sat():
return 0
else:
trim()
return 1
def input_x_factor():
"""Sets the global x_factor according to user input"""
global x_factor, xfi
print 'Type in x_factor:',
xfi = x_factor = input()
print 'x_factor set to %f'%x_factor
##def prove_sec():
## """
## Like 'prove' proves all the outputs together. Speculation is done first
## If undecided, the do super_prove.
## """
## global x_factor,xfi,f_name, last_verify_time,K_backup, sec_options
## max_bmc = -1
## K_backup = K = 0
## result = prove_part_1(K) #initial simplification here
## if n_latches() == 0:
## return 1,result
## K = K_backup
## if ((result == 'SAT') or (result == 'UNSAT')):
## return 1,result
## assert K==1, 'K = %d'%K
## result = prove_part_3(K) #speculation done here
## if ((result == 'SAT') or (result == 'UNSAT')):
## return 1,result
## else:
## return 1,super_prove(0)
##
## #################### End of ss
## K = K_backup
## #print 'after speculate'
## status = get_status()
## assert 0<K and K<4, 'K = %d'%K
## if K > 1: # for K = 1, we will leave final verification for later
## print 'Entering final_verify_recur(%d) from prove()'%K
## status = final_verify_recur(K) # will start verifying with final verify
## #starting at backup number K-1 (either K = 2 or 3 here
## #1 if spec found true sat on abs, 2 can happen if abstraction
## #did not work but speculation worked,
## #3 if still undecided after spec)
## else: #K=1 means that abstraction did not work and was proved wrong by speculation
## if a == 0:
## result = prove_spec_first()
## if ((result == 'SAT') or (result == 'UNSAT')):
## return 1,result
## write_file('final')
## return (not K == 1),RESULT[status]
def prove(a):
"""Proves all the outputs together. If ever an abstraction
was done then if SAT is returned,
we make RESULT return "undecided".
If a == 1 skip speculate. K is the number of the next backup
if a == 2 skip initial simplify and speculate"""
global x_factor,xfi,f_name, last_verify_time,K_backup, t_init, sec_options
spec_first = False
max_bmc = -1
K_backup = K = 0
if a == 2: #skip initial simplification
print 'Using quick simplification',
abc('lcorr;drw')
status = process_status(get_status())
if status <= Unsat:
result = RESULT[status]
else:
ps()
write_file('smp')
abc('w %s_backup_%d.aig'%(initial_f_name,K)) #writing backup 0
K_backup = K = K+1
result = 'UNDECIDED'
else:
result = prove_part_1(K) #initial simplification here
if ((result == 'SAT') or (result == 'UNSAT')):
return 1,result
if n_latches() == 0:
return 1,result
if a == 0:
spec_first = False
## spec_first = check_if_spec_first()
if spec_first:
sec_options = 'g'
print 'sec_options set to "g"'
if n_latches() == 0:
return 1,result
K = K_backup
if ((result == 'SAT') or (result == 'UNSAT')):
return 1,result
assert K==1, 'K = %d'%K
t_init = 2
if spec_first and a == 0:
result = prove_part_3(K)
else:
result = prove_part_2(K) #abstraction done here
K = K_backup
if ((result == 'SAT') or (result == 'UNSAT')):
return 1,result
assert 0<K and K<3, 'K = %d'%K
if a == 0:
t_init = 2
if spec_first:
result = prove_part_2(K) #speculation 2one here
else:
result = prove_part_3(K)
if ((result == 'SAT') or (result == 'UNSAT')):
return 1,result
K = K_backup
#print 'after speculate'
status = get_status()
assert 0<K and K<4, 'K = %d'%K
if (((K > 2) and (n_pos()>1)) or ((K == 2) and spec_first)): # for K = 1, we will leave final verification for later
print 'Entering final_verify_recur(%d) from prove()'%K
status = final_verify_recur(K) # will start verifying with final verify
#starting at backup number K-1 (either K = 2 or 3 here
#1 if spec found true sat on abs, 2 can happen if abstraction
#did not work but speculation worked,
#3 if still undecided after spec)
#K=1 or 2 and not spec_first means that abstraction did not work and was proved wrong by speculation
elif ((a == 0) and K == 1):
t_init = 2
result = prove_spec_first()
if ((result == 'SAT') or (result == 'UNSAT')):
return 1,result
write_file('final')
return (not K == 1),RESULT[status]
def psf():
x = time.time()
result = prove_spec_first()
print 'Total clock time for %s = %f sec.'%(init_initial_f_name,(time.time() - x))
return result
def prove_spec_first():
"""Proves all the outputs together. If ever an abstraction
was done then if SAT is returned,
we make RESULT return "undecided".
"""
global x_factor,xfi,f_name, last_verify_time,K_backup
max_bmc = -1
K_backup = K = 1
## result = prove_part_1(K) #initial simplification here
## if n_latches() == 0:
## return result
## K = K_backup
## if ((result == 'SAT') or (result == 'UNSAT')):
## return result
## assumes that initial simplification has been done already.
assert K==1, 'K = %d'%K
result = prove_part_3(K) #speculation done here
K = K_backup
if ((result == 'SAT') or (result == 'UNSAT')):
return result
assert 0<K and K<3, 'K = %d'%K
K = K_backup #K = 1 => speculation did not do anything
if K == 1: # so don't try abstraction because it did not work the first time
return 'UNDECIDED'
result = prove_part_2(K) #abstraction done here
if result == 'UNSAT':
return result
if result == 'SAT': # abstraction proved speculation wrong.
K = 2
assert 0<K and K<4, 'K = %d'%K
if K > 1: # for K = 1, we will leave final verification for later
print 'Entering final_verify_recur(%d) from prove()'%K
status = final_verify_recur(K) # will start verifying with final verify
#starting at backup number K-1 (either K = 2 or 3 here
#1 if spec found true sat on abs, 2 can happen if
#speculation worked but abstraction proved it wrong,
#3 if still undecided after spec and abstraction)
write_file('final')
return RESULT[status]
def prove_part_1(K):
global x_factor,xfi,f_name, last_verify_time,K_backup
#K=0
print 'Initial: ',
print_circuit_stats()
x_factor = xfi
print 'x_factor = %f'%x_factor
print '\n***Running pre_simp'
set_globals()
if n_latches() > 0:
## status = pre_simp()
set_globals()
t = 1000
funcs = [eval('(pyabc_split.defer(pre_simp)())')]
## J = sims+pdrs+bmcs+intrps
J = pdrs+bmcs+bestintrps
funcs = create_funcs(J,t)+ funcs #important that pre_simp goes last
mtds =sublist(methods,J) + ['pre_simplify']
fork_last(funcs,mtds)
## funcs = [eval(FUNCS[3])] + [eval(FUNCS[0])] + [eval(FUNCS[1])] + [eval(FUNCS[2])] + [eval(FUNCS[9])] + [eval(FUNCS[7])] + funcs
## fork_last(funcs,['SIM', 'PDR','INTRP','BMC', 'BMC3', 'PDRm','pre_simp'])
status = get_status()
else:
status = check_sat()
if ((status <= Unsat) or (n_latches() == 0)):
return RESULT[status]
if n_ands() == 0:
abc('&get;,bmc -vt=2')
if is_sat():
return 'SAT'
trim()
write_file('smp')
abc('w %s_backup_%d.aig'%(initial_f_name,K)) #writing backup 0
K_backup = K = K+1
#K=1
set_globals()
return 'UNDECIDED'
def prove_part_2(K):
"""does the abstraction part of prove"""
global x_factor,xfi,f_name, last_verify_time,K_backup, trim_allowed
print'\n***Running abstract'
nl_b = n_latches()
status = abstract() #ABSTRACTION done here
## write_file('abs')
## print 'Abstract finished'
if status == Undecided_no_reduction:
K_backup = K = K-1 #K = 0
if status == Unsat:
write_file('abs')
return RESULT[status]
## trim()
#just added in
if status < Unsat:
write_file('abs')
print 'CEX in frame %d'%cex_frame()
return RESULT[status]
if K > 0:
t_old = trim_allowed
if pord_on:
trim_allowed = False
pre_simp()
trime_allowed = t_old
#end of added in
write_file('abs')
status = process_status(status)
if ((status <= Unsat) or status == Error):
if status < Unsat:
print 'CEX in frame %d'%cex_frame()
return RESULT[status]
return RESULT[status]
abc('w %s_backup_%d.aig'%(initial_f_name,K)) # writing backup 1 (or 0) after abstraction
K_backup = K = K+1
#K = 1 or 2 here
return 'UNDECIDED'
def prove_part_3(K):
"""does the speculation part of prove"""
global x_factor,xfi,f_name, last_verify_time,K_backup, init_initial_f_name
global max_bmc, sec_options
#K_backup = K = K +1 #K = 1 or 2 K =1 means that abstraction did not reduce
assert 0 < K and K < 3, 'K = %d'%K
if ((n_ands() > 10000) and sec_options == ''):
sec_options = 'g'
print 'sec_options set to "g"'
if n_ands() == 0:
print 'Speculation skipped because no AND nodes'
else:
print '\n***Running speculate'
## pre_simp()
status = speculate() #SPECULATION done here
if status == Unsat:
return RESULT[status]
old_f_name = f_name
## if not status < Unsat:
## pre_simp()
## write_file('spec1')
## #we do not do the continuation of speculation right now so the following is not needed.
## #abc('&r %s_gore.aig;&w %s_gore.aig'%(old_f_name,f_name)) #very subtle -needed for continuing spec refinement
status = process_status(status)
if status == Unsat:
return RESULT[status]
elif ((status < Unsat) or (status == Error)):
print 'CEX in frame %d'%cex_frame()
if K == 1: #if K = 1 then abstraction was not done.
print 'speculate found cex on original'
return RESULT[status] # speculate found cex on original
K_backup = K = K-1 #since spec found a true cex, then result of abstract was wrong
print 'cex means that abstraction was invalid'
print 'Initial simplified AIG restored => ',
abc('r %s_smp.aig'%init_initial_f_name)
max_bmc = -1
ps()
assert K == 1, 'K = %d'%K
else:
trim()
print 'Problem still undecided'
abc('w %s_backup_%d.aig'%(initial_f_name,K)) # writing backup 2 or 1
# 2 after speculation and abstraction
# 1 if abstraction did not reduce
K_backup = K = K+1
assert 1<K and K<4, 'K = %d'%K
## write_file('spec2')
trim()
return 'UNDECIDED'
def prove_all(dir,t):
"""Prove all aig files in this directory using super_prove and record the results in results.txt"""
## t = 1000 #This is the timeoout value
xtime = time.time()
## dir = main.list_aig('')
results = []
f =open('results_%d.txt'%len(dir), 'w')
for name in dir:
read_file_quiet(name)
print '\n **** %s:'%name,
ps()
F = create_funcs([18,6],t) #create timer function as i = 0 Here is the timer
for i,res in pyabc_split.abc_split_all(F):
break
tt = time.time()
if i == 0:
res = 'Timeout'
str = '%s: %s, time = %s'%(name,res,convert(tt-xtime))
if res == 'SAT':
str = str + ', cex_frame = %d'%cex_frame()
str = str +'\n'
f.write(str)
f.flush()
results = results + ['%s: %s, time = %s'%(name,res,convert(tt-xtime))]
xtime = tt
## print results
f.close()
return results
def prove_g_pos(a):
"""Proves the outputs clustered by a parameter a.
a is the disallowed increase in latch support Clusters must be contiguous
If a = 0 then outputs are proved individually. Clustering is done from last to first
Output 0 is attempted to be proved inductively using other outputs as constraints.
Proved outputs are removed if all the outputs have not been proved.
If ever one of the proofs returns SAT, we stop and do not try any other outputs."""
global f_name, max_bmc,x_factor,x
x = time.time()
#input_x_factor()
init_f_name = f_name
print 'Beginning prove_g_pos'
prove_all_ind()
print 'Number of outputs reduced to %d by fast induction with constraints'%n_pos()
print '\n****Running second level prove****************\n'
reparam()
## try_rpm()
## k,result = prove(1) # 1 here means do not try speculate.
## if result == 'UNSAT':
## print 'Second prove returned UNSAT'
## return result
## if result == 'SAT':
## print 'CEX found'
## return result
print '\n********** Proving each output separately ************'
#prove_all_ind()
#print 'Number of outputs reduced to %d by fast induction with constraints'%n_pos()
f_name = init_f_name
abc('w %s_osavetemp.aig'%f_name)
n = n_pos()
print 'Number of outputs = %d'%n
#count = 0
#Now prove each remaining output separately.
pos_proved = []
J = 0
jnext = n-1
while jnext >= 0:
max_bmc = -1
f_name = init_f_name
abc('r %s_osavetemp.aig'%f_name)
#Do in reverse order
jnext_old = jnext
if a == 0: # do not group
extract(jnext,jnext)
jnext = jnext -1
else:
jnext = group(a,jnext)
if jnext_old > jnext+1:
print '\nProving outputs [%d-%d]'%(jnext + 1,jnext_old)
else:
print '\nProving output %d'%(jnext_old)
#ps()
f_name = f_name + '_%d'%jnext_old
result = prove_1()
if result == 'UNSAT':
if jnext_old > jnext+1:
print '******** PROVED OUTPUTS [%d-%d] ******** '%(jnext+1,jnext_old)
else:
print '******** PROVED OUTPUT %d ******** '%(jnext_old)
pos_proved = pos_proved + range(jnext +1,jnext_old+1)
continue
if result == 'SAT':
print 'One of output in (%d to %d) is SAT'%(jnext + 1,jnext_old)
return result
else:
print '******** UNDECIDED on OUTPUTS %d thru %d ******** '%(jnext+1,jnext_old)
f_name = init_f_name
abc('r %s_osavetemp.aig'%f_name)
if not len(pos_proved) == n:
print 'Eliminating %d proved outputs'%(len(pos_proved))
remove(pos_proved)
trim()
write_file('group')
result = 'UNDECIDED'
else:
print 'Proved all outputs. The problem is proved UNSAT'
result = 'UNSAT'
print 'Total clock time for prove_g_pos = %f sec.'%(time.time() - x)
return result
def prove_pos(i):
"""
i=1 means to execute prove_all_ind first
Proved outputs are removed if all the outputs have not been proved.
If ever one of the proofs returns SAT, we continue and try to resolve other outputs."""
global f_name, max_bmc,x_factor,x
x = time.time()
#input_x_factor()
init_f_name = f_name
print 'Beginning prove_pos'
remove_0_pos()
if i:
prove_all_ind()
print 'Number of outputs reduced to %d by quick induction with constraints'%n_pos()
print '********** Proving each output separately ************'
f_name = init_f_name
abc('w %s_osavetemp.aig'%f_name)
n = n_pos()
print 'Number of outputs = %d'%n
pos_proved = []
pos_disproved = []
J = 0
jnext = n-1
while jnext >= 0:
max_bmc = -1
f_name = init_f_name
abc('r %s_osavetemp.aig'%f_name)
#Do in reverse order
jnext_old = jnext
extract(jnext,jnext)
jnext = jnext -1
print '\nProving output %d'%(jnext_old)
f_name = f_name + '_%d'%jnext_old
## result = prove_1()
result = super_prove(2) #do not do initial simplification
if result == 'UNSAT':
print '******** PROVED OUTPUT %d ******** '%(jnext_old)
pos_proved = pos_proved + range(jnext +1,jnext_old+1)
continue
if result == 'SAT':
print '******** DISPROVED OUTPUT %d ******** '%(jnext_old)
pos_disproved = pos_disproved + range(jnext +1,jnext_old+1)
continue
else:
print '******** UNDECIDED on OUTPUT %d ******** '%(jnext_old)
f_name = init_f_name
abc('r %s_osavetemp.aig'%f_name)
list = pos_proved + pos_disproved
print 'Proved the following outputs: %s'%pos_proved
print 'Disproved the following outputs: %s'%pos_disproved
if not len(list) == n:
print 'Eliminating %d resolved outputs'%(len(list))
remove(list)
trim()
write_file('group')
result = 'UNRESOLVED'
else:
print 'Proved or disproved all outputs. The problem is proved RESOLVED'
result = 'RESOLVED'
print 'Total clock time for prove_pos = %f sec.'%(time.time() - x)
return result
def remove_pos(lst):
"""Takes a list of pairs where the first part of a pair is the PO number and
the second is the result 1 = disproved, 2 = proved, 3 = unresolved. Then removes
the proved and disproved outputs and returns the aig with the unresolved
outputs"""
proved = disproved = unresolved = []
for j in range(len(lst)):
jj = lst[j]
if jj[1] == 2:
proved = proved + [jj[0]]
if (jj[1] == 1 or (jj[1] == 0)):
disproved = disproved +[jj[0]]
if jj[1] > 2:
unresolved = unresolved +[jj[0]]
print '%d outputs proved'%len(proved)
## print disproved
## abc('w xxx__yyy.aig')
if not proved == []:
if ((max(proved)>n_pos()-1) or min(proved)< 0):
print proved
remove(proved)
#functions for proving multiple outputs in parallel
#__________________________________________________
def prove_only(j):
""" extract the jth output and try to prove it"""
global max_bmc, init_initial_f_name, initial_f_name, f_name,x
#abc('w %s__xsavetemp.aig'%f_name)
extract(j,j)
set_globals()
ps()
print '\nProving output %d'%(j)
f_name = f_name + '_%d'%j
result = prove_1()
#abc('r %s__xsavetemp.aig'%f_name)
if result == 'UNSAT':
print '******** PROVED OUTPUT %d ******** '%(j)
return Unsat
if result == 'SAT':
print '******** DISPROVED OUTPUT %d ******** '%(j)
return Sat
else:
print '******** UNDECIDED on OUTPUT %d ******** '%(j)
return Undecided
def verify_only(j,t):
""" extract the jth output and try to prove it"""
global max_bmc, init_initial_f_name, initial_f_name, f_name,x, reachs, last_cex, last_winner, methods
## ps()
## print 'Output = %d'%j
extract(j,j)
## ps()
set_globals()
if n_latches() == 0:
result = check_sat()
else:
f_name = f_name + '_%d'%j
# make it so that jabc is not used here
reachs_old = reachs
reachs = reachs[1:] #just remove jabc from this.
res = verify(slps+sims+pdrs+bmcs+intrps,t) #keep the number running at the same time as small as possible.
## res = verify(sims+pdrs+bmcs+intrps,t) #keep the number running at the same time as small as possible.
reachs = reachs_old
result = get_status()
assert res == result,'result: %d, status: %d'%(res,get_status())
if result > Unsat:
## print result
## print '******* %d is undecided ***********'%j
return result
elif result == Unsat:
## print '******** PROVED OUTPUT %d ******** '%(j)
return result
elif ((result < Unsat) and (not result == None)):
print '******** %s DISPROVED OUTPUT %d ******** '%(last_cex,j)
## print ('writing %d.status'%j), result, get_status()
abc('write_status %d.status'%j)
last_winner = last_cex
return result
else:
print '****** %d result is %d'%(j,result)
return result
def verify_range(j,k,t):
""" extract the jth thru kth output and try to prove their OR"""
global max_bmc, init_initial_f_name, initial_f_name, f_name,x, reachs, last_cex, last_winner, methods
extract(j,k)
abc('orpos')
set_globals()
if n_latches() == 0:
result = check_sat()
else:
f_name = f_name + '_%d'%j
# make it so that jabc is not used here
reachs_old = reachs
reachs = reachs[1:] #just remove jabc from this.
res = verify(sims+pdrs+bmcs+intrps,t) #keep the number running at the sme time as small as possible.
reachs = reachs_old
result = get_status()
assert res == result,'result: %d, status: %d'%(res,get_status())
if result > Unsat:
## print result
## print '******* %d is undecided ***********'%j
return result
elif result == Unsat:
## print '******** PROVED OUTPUT %d ******** '%(j)
return result
elif ((result < Unsat) and (not result == None)):
print '******** %s DISPROVED OUTPUT %d ******** '%(last_cex,j)
## print ('writing %d.status'%j), result, get_status()
abc('write_status %d.status'%j)
last_winner = last_cex
return result
else:
print '****** %d result is %d'%(j,result)
return result
def prove_n_par(n,j):
"""prove n outputs in parallel starting at j"""
F = []
for i in range(n):
F = F + [eval('(pyabc_split.defer(prove_only)(%s))'%(j+i))]
#print S
#F = eval(S)
result = []
print 'Proving outputs %d thru %d in parallel'%(j,j+n-1)
for i,res in pyabc_split.abc_split_all(F):
result = result +[(j+i,res)]
#print result
return result
def prove_pos_par(t,BREAK):
"""Prove all outputs in parallel and break on BREAK"""
return run_parallel([],t,BREAK)
def prove_pos_par0(n):
""" Group n POs grouped and prove in parallel until all outputs have been proved"""
f_name = initial_f_name
abc('w %s__xsavetemp.aig'%f_name)
result = []
j = 0
N = n_pos()
while j < N-n:
abc('r %s__xsavetemp.aig'%f_name)
result = result + prove_n_par(n,j)
j = j+n
if N > j:
result = result + prove_n_par(N-j,j)
abc('r %s__xsavetemp.aig'%initial_f_name)
ps()
print result
remove_pos(result)
write_file('group')
return
def prop_decomp():
"""decompose a single property into multiple ones (only for initial single output),
by finding single and double literal primes of the outputs."""
if n_pos()>1:
return
run_command('outdec -v -L 2')
if n_pos()>1:
ps()
def distribute(N,div):
"""
we are going to verify outputs in groups
"""
n = N/div
rem = N - (div * (N/div))
result = []
for j in range(div):
if rem >0:
result = result +[n+1]
rem = rem -1
else:
result = result + [n]
return result
def find_cex_par(tt):
"""prove n outputs at once and quit at first cex. Otherwise if no cex found return aig
with the unproved outputs"""
global trim_allowed,last_winner, last_cex, n_pos_before, t_init, j_last, sweep_time
b_time = time.time() #Wall clock time
n = n_pos()
remove_0_pos()
N = n_pos()
full_time = all_proc = False
print 'Number of POs: %d => %d'%(n,N)
if N == 0:
return Unsat
## inc = 5 #******* increment for grouping for sweep set here *************
## inc = min(12,max(inc, int(.1*N)))
inc = 1+N/100
## if N <1.5*inc: # if near the increment for grouping try to get it below.
## prove_all_ind()
## N = n_pos()
if inc == 1:
prove_all_ind()
N = n_pos()
T = int(tt) #this is the total time to be taken in final verification run before quitting speculation
## if inc == 10:
## t_init = 10
## t = max(t_init/2,T/20)
## if N <= inc:
## t = T
## print "inc = %d, Sweep time = %s, j_group = %d"%(inc,convert(t),j_last)
t = sweep_time/2 #start sweeping at last time where cex was found.
## it used to be t = 1 here but it did not make sense although seemed to work.
## inc = 2
while True: #poor man's concurrency
N = n_pos()
if N == 0:
return Unsat
#sweep_time controls so that when sweep starts after a cex, it starts at the last sweep time
t = max(2,2*t) #double sweep time
if t > .75*T:
t = T
full_time = True
if ((N <= inc) or (N < 13)):
t = sweep_time = T
full_time = True
inc = 1
## sweep_time = 2*sweep_time
if not t == T:
t= sweep_time = max(t,sweep_time)
## t = sweep_time
##new heuristic
if (all_proc and sweep_time > 8): #stop poor man's concurrency and jump to full time.
t = sweep_time = T
full_time - True #this might be used to stop speculation when t = T and the last sweep
## found no cex and we do not prove Unsat on an output
abc('w %s__ysavetemp.aig'%f_name)
ps()
if N < 50:
inc = 1
print "inc = %d, Sweep time = %s, j_last = %d"%(inc,convert(t),j_last)
F = []
## G = []
#make new lambda functions since after the last pass some of the functions may have been proved and eliminated.
for i in range(N):
F = F + [eval('(pyabc_split.defer(verify_only)(%d,%s))'%(i,convert(T)))] #make time large and let sleep timer control timeouts
## G = G + [range(i,i+1)]
######
result = []
outcome = ''
N = len(F)
rng = range(1+(N-1)/inc)
rng = rng[j_last:]+rng[:j_last] #pick up in range where last found cex.
## print 'rng = ',
## print rng
k = -1
bb_time = time.time()
for j in rng:
k = k+1 #keeps track of how many groups we have processed.
j_last = j
J = j*inc
JJ = J+inc
JJ = min(N,JJ)
if J == JJ-1:
print 'Function = %d '%J,
else:
print 'Functions = [%d,%d]'%(J,JJ-1)
Fj = create_funcs([18],t+1) #create timer function as i = 0 Here is the timer
Fj = Fj + F[J:JJ]
count = 0
fj_time = time.time()
abc('r %s__ysavetemp.aig'%f_name) #important need to restore aig here so the F refers to right thing when doing verify_only.
## # because verify_only changes the aig.
## ps()
for i,res in pyabc_split.abc_split_all(Fj):
count = count+1
Ji = J+i-1 #gives output number
if ((res == 0) or (res == 1)):
abc('read_status %d.status'%Ji)
res = get_status()
outcome = 'CEX: Frame = %d, PO = %d, Time = %s'%(cex_frame(),Ji,convert((time.time() - fj_time)))
break
if i == 0: #sleep timer expired
outcome = '*** Time expired in %s sec. Next group = %d to %d ***'%(convert(time.time() - fj_time),JJ,min(N,JJ+inc))
break
elif res == None: #this should not happen
print res
print Ji,RESULT[res],
else: # output Ji was proved
result = result + [[Ji,res]]
if count >= inc:
outcome = '--- all group processed without cex ---'
all_proc = True
break
continue #this can only happen if inc > 1
# end of for i loop
if ((res < Unsat) and (not res == None)):
break
else:
continue # continue j loop
#end of for j loop
if k < len(rng):
t_init = t/2 #next time start with this time.
else:
j_last = j_last+1 #this was last j and we did not find cex, so start at next group
print outcome + ' => ' ,
if ((res < Unsat) and (not res == None)):
t_init = t/2
abc('read_status %d.status'%Ji) #make sure we got the right status file.
#actually if doing abstraction we could remove proved outputs now, but we do not. -**inefficiency**
return res
else: #This implies that no outputs were disproved. Thus can remove proved outputs.
abc('r %s__ysavetemp.aig'%f_name) #restore original aig
if not result == []:
res = []
for j in range(len(result)):
k = result[j]
if k[1] == 2:
res = res + [k[0]]
## print res
## result = mapp(res,G)
result = res
## print result
remove(result) #remove the outputs that were proved UNSAT.
#This is OK for both abstract and speculate
print 'Number of POs reduced to %d'%n_pos()
if n_pos() == 0:
return Unsat
if t>=T:
return Undecided
else:
continue
return Undecided
def remap_pos():
""" maintains a map of current outputs to original outputs"""
global po_map
k = j = 0
new = []
assert n_pos() == len(po_map), 'length of po_map, %d, and current # POs, %d, don"t agree'%(len(po_map),n_pos())
for j in range(len(po_map)):
N = n_pos()
abc('removepo -N %d'%k) # this removes the output if it is 0 driven
if n_pos() == N:
new = new + [po_map[j]]
k = k+1
if len(new) < len(po_map):
## print 'New map = ',
## print new
po_map = new
def prove_mapped():
"""
assumes that srm is in workspace and takes the unsolved outputs and proves
them by using proved outputs as constraints.
"""
global po_map
## print po_map
po_map.sort() #make sure mapped outputs are in order
for j in po_map: #put unsolved outputs first
run_command('swappos -N %d'%j)
print j
N = n_pos()
assert N > len(po_map), 'n_pos = %d, len(po_map) = %d'%(N, len(po_map))
run_command('constr -N %d'%(N-len(po_map))) #make the other outputs constraints
run_command('fold') #fold constraints into remaining outputs.
ps()
prove_all_mtds(100)
def mapp(R,G):
result = []
for j in range(len(R)):
result = result + G[R[j]]
return result
#_______________________________________
def prove_g_pos_split():
"""like prove_g_pos but quits when any output is undecided"""
global f_name, max_bmc,x_factor,x
x = time.clock()
#input_x_factor()
init_f_name = f_name
print 'Beginning prove_g_pos_split'
prove_all_ind()
print 'Number of outputs reduced to %d by fast induction with constraints'%n_pos()
reparam()
## try_rpm()
print '********** Proving each output separately ************'
f_name = init_f_name
abc('w %s_osavetemp.aig'%f_name)
n = n_pos()
print 'Number of outputs = %d'%n
pos_proved = []
J = 0
jnext = n-1
while jnext >= 0:
max_bmc = -1
f_name = init_f_name
abc('r %s_osavetemp.aig'%f_name)
jnext_old = jnext
extract(jnext,jnext)
jnext = jnext -1
print '\nProving output %d'%(jnext_old)
f_name = f_name + '_%d'%jnext_old
result = prove_1()
if result == 'UNSAT':
if jnext_old > jnext+1:
print '******** PROVED OUTPUTS [%d-%d] ******** '%(jnext+1,jnext_old)
else:
print '******** PROVED OUTPUT %d ******** '%(jnext_old)
pos_proved = pos_proved + range(jnext +1,jnext_old+1)
continue
if result == 'SAT':
print 'One of output in (%d to %d) is SAT'%(jnext + 1,jnext_old)
return result
else:
print '******** UNDECIDED on OUTPUTS %d thru %d ******** '%(jnext+1,jnext_old)
print 'Eliminating %d proved outputs'%(len(pos_proved))
# remove outputs proved and return
f_name = init_f_name
abc('r %s_osavetemp.aig'%f_name)
remove(pos_proved)
trim()
write_file('group')
return 'UNDECIDED'
f_name = init_f_name
abc('r %s_osavetemp.aig'%f_name)
if not len(pos_proved) == n:
print 'Eliminating %d proved outputs'%(len(pos_proved))
remove(pos_proved)
trim()
write_file('group')
result = 'UNDECIDED'
else:
print 'Proved all outputs. The problem is proved UNSAT'
result = 'UNSAT'
print 'Total time = %f sec.'%(time.clock() - x)
return result
def group(a,n):
"""Groups together outputs beginning at output n and any contiguous preceeding output
that does not increase the latch support by a or more"""
global f_name, max_bmc
nlt = n_latches()
extract(n,n)
nli = n_latches()
if n == 0:
return n-1
for J in range(1,n+1):
abc('r %s_osavetemp.aig'%f_name)
j = n-J
#print 'Running %d to %d'%(j,n)
extract(j,n)
#print 'n_latches = %d'%n_latches()
#if n_latches() >= nli + (nlt - nli)/2:
if n_latches() == nli:
continue
if n_latches() > nli+a:
break
abc('r %s_osavetemp.aig'%f_name)
## if j == 1:
## j = j-1
print 'extracting [%d-%d]'%(j,n)
extract(j,n)
ps()
return j-1
def extract(n1,n2):
"""Extracts outputs n1 through n2"""
no = n_pos()
if n2 > no:
return 'range exceeds number of POs'
abc('cone -s -O %d -R %d'%(n1, 1+n2-n1))
#abc('scl') # eliminated because need to keep same number of inputs.
def remove_intrps(J):
JJ = []
for i in J:
if i in allintrps:
continue
else:
JJ = JJ +[i]
return JJ
def remove(lst):
"""Removes outputs in list"""
global po_map
n_before = n_pos()
zero(lst)
## remap_pos()
remove_0_pos()
print 'list',
lst
print 'n_before = %d, n_list = %d, n_after = %d'%(n_before, len(lst), n_pos())
def zero(list):
"""Zeros out POs in list"""
for j in list:
run_command('zeropo -N %d'%j)
def remove_0_pos():
global po_map
"""removes the 0 pos, but no pis because we might get cexs and need the correct number of pis
Should keep tract of if original POs are 0 and are removed.
Can this happen outside of prove_all_ind or
pord_all which can set proved outputs to 0???
"""
run_command('&get; &trim -i; &put; addpi') #adds a pi only if there are none
po_map = range(n_pos())
## # gone back to original method of removing pos. Thus po_map is irrelevant
## remap_pos()
## abc('addpi')
def psp():
quick_simp()
result = run_parallel([6,21],500,'US') #runs 'run_parallel' and sp() in parallel. run_parallel uses
#JP and TERM to terminate.
return result
def sp():
"""Alias for super_prove"""
print 'Executing super_prove'
result = super_prove(0)
return result
##def super_sec(options):
## """Main proof technique now for seq eq checking. 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
## to be proved, or any output that is proved SAT"""
## global max_bmc, init_initial_f_name, initial_f_name,win_list, last_verify_time, sec_options
## sec_options = options
## init_initial_f_name = initial_f_name
## if x_factor > 1:
## print 'x_factor = %f'%x_factor
## input_x_factor()
## max_bmc = -1
## x = time.time()
## k = 2
## K,result = prove_sec()
## if ((result == 'SAT') or (result == 'UNSAT')):
## print '%s: total clock time taken by super_prove = %f sec.'%(result,(time.time() - x))
## return
## elif ((result[:3] == 'UND') and (n_latches() == 0)):
## return result
## print '%s: total clock time taken by super_prove = %f sec.'%(result,(time.time() - x))
## if n_pos() > 1:
## print 'Entering prove_g_pos'
## result = prove_g_pos(0)
## print result
## if result == 'UNSAT':
## print 'Total clock time taken by super_prove = %f sec.'%(time.time() - x)
## return result
## if result == 'SAT':
## k = 1 #Don't try to prove UNSAT on an abstraction that had SAT
## # should go back to backup 1 since probably spec was bad.
## if check_abs(): #if same as abstract version, check original simplified version
## k = 0
## y = time.time()
## if K == 0: #K = 0 means that speculate found cex in abstraction.
## k=0
## print 'Entering BMC_VER_result(%d)'%k
## result = BMC_VER_result(k)
## #print 'win_list = ',win_list
## print 'Total clock time taken by last gasp verification = %f sec.'%(time.time() - y)
## print 'Total clock time for %s = %f sec.'%(init_initial_f_name,(time.time() - x))
## return result
def super_prove(n=0):
"""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
to be proved, or any output that is proved SAT
n controls call to prove(n)
n = 2 means skip initial simplify and speculate,
n=1 skip initial simp.
"""
global max_bmc, init_initial_f_name, initial_f_name,win_list, last_verify_time
init_initial_f_name = initial_f_name
if x_factor > 1:
print 'x_factor = %f'%x_factor
input_x_factor()
max_bmc = -1
x = time.time()
k = 2
if n == 2:
K,result = prove(2)
else:
K,result = prove(0)
if ((result == 'SAT') or (result == 'UNSAT')):
print '%s: total clock time taken by super_prove = %f sec.'%(result,(time.time() - x))
return result
elif ((result[:3] == 'UND') and (n_latches() == 0)):
return result
print '%s: total clock time taken by super_prove = %f sec.'%(result,(time.time() - x))
y = time.time()
if K == 0: #K = 0 means that speculate found cex in abstraction.
k=0
if n == 2:
print 'Entering BMC_VER()'
result = BMC_VER() #typically called from a super_prove run in parallel.
if result == 'SAT': #this is because we have done an abstraction and cex is invalid.
result = 'UNDECIDED'
else:
print 'Entering BMC_VER_result(%d)'%k
result = BMC_VER_result(k)
#print 'win_list = ',win_list
print result
print 'Total clock time taken by last gasp verification = %f sec.'%(time.time() - y)
print 'Total clock time for %s = %f sec.'%(init_initial_f_name,(time.time() - x))
return result
def reachm(t):
x = time.clock()
#print 'trying reachm'
abc('&get;&reachm -vcs -T %d'%t)
print 'reachm done in time = %f'%(time.clock() - x)
return get_status()
def reachp(t):
x = time.clock()
#print 'trying reachm2'
abc('&get;&reachp -rv -T %d'%t)
print 'reachm2 done in time = %f'%(time.clock() - x)
return get_status()
def reachn(t):
x = time.clock()
#print 'trying reachm3'
abc('&get;&reachn -rv -T %d'%t)
print 'reachm3 done in time = %f'%(time.clock() - x)
return get_status()
def reachx(t):
x = time.time()
#print 'trying reachx'
abc('reachx -t %d'%t)
print 'reachx done in time = %f'%(time.time() - x)
return get_status()
def reachy(t):
x = time.clock()
#print 'trying reachy'
abc('&get;&reachy -v -T %d'%t)
print 'reachy done in time = %f'%(time.clock() - x)
return get_status()
def create_funcs(J,t):
"""evaluates strings indexed by J in methods given by FUNCS
Returns a list of lambda functions for the strings in FUNCs
If J = [], then create provers for all POs"""
funcs = []
for j in range(len(J)):
k=J[j]
funcs = funcs + [eval(FUNCS[k])]
return funcs
def check_abs():
global init_initial_f_name
abc('w %s_save.aig'%init_initial_f_name)
ni = n_pis()
nl = n_latches()
na = n_ands()
abc('r %s_smp_abs.aig'%init_initial_f_name)
if ((ni == n_pis()) and (nl == n_latches()) and (na == n_ands())):
return True
else:
abc('r %s_save.aig'%init_initial_f_name)
return False
"""make a special version of BMC_VER_result that just works on the current network"""
def BMC_VER():
global init_initial_f_name, methods, last_verify_time
#print init_initial_f_name
xt = time.time()
result = 5
t = max(2*last_verify_time,100)
print 'Verify time set to %d'%t
N = bmc_depth()
L = n_latches()
I = n_real_inputs()
X = pyabc_split.defer(abc)
J = slps + pdrs + [23] + bmcs
if ( ((I+L<350)&(N>100)) or (I+L<260) or (L<80) ):
J = J+reachs # add all reach methods
if L < 80:
J = J + [4]
F = create_funcs(J,t)
mtds = sublist(methods,J)
print '%s'%mtds
(m,result) = fork_break(F,mtds,'US')
print '(m,result) = %d,%s'%(m,result)
result = RESULT[result]
print 'BMC_VER() result = %s'%result
return result
def BMC_VER_result(n):
global init_initial_f_name, methods, last_verify_time
#print init_initial_f_name
xt = time.time()
result = 5
if n == 0:
abc('r %s_smp.aig'%init_initial_f_name)
print '\n***Running proof on initial simplified circuit\n',
ps()
elif n == 1:
abc('r %s_smp_abs.aig'%init_initial_f_name)
print '\n***Running proof on abstracted circuit',
ps()
else: # n was 2
print '\n***Running proof on final unproved circuit',
ps()
t = max(2*last_verify_time,1000)
print 'Verify time set to %d'%t
#status = verify(J,t)
N = bmc_depth()
L = n_latches()
I = n_real_inputs()
X = pyabc_split.defer(abc)
J = slps + pdrs + [23] +bmcs
## [0,1,7,14] # try pdr, interpolation, and pdrm
## if n == 0:
## J = J+ bmcs #add BMC #eveen if n =1 or 2 we want to find a cex
#heuristic that if bmc went deep, then reachability might also
if ( ((I+L<350)&(N>100)) or (I+L<260) or (L<80) ):
#J = J+[4,13] #add reachx and reachn
J = J+reachs # add all reach methods
if L < 80:
J = J + [4]
#F = eval(S)
F = create_funcs(J,t)
mtds = sublist(methods,J)
print '%s'%mtds
(m,result) = fork(F,mtds)
result = get_status()
if result == Unsat:
return 'UNSAT'
if n == 0:
if result < Unsat:
return 'SAT'
if result > Unsat: #still undefined
return 'UNDECIDED'
elif n == 1: #just tried abstract version - try initial simplified version
if result < Unsat:
return BMC_VER_result(0)
else: #if undecided on good abstracted version, does not make sense to try initial one
return 'UNDECIDED'
else: # n was 2, just tried final unresolved version - now try abstract version
if result < Unsat:
return BMC_VER_result(1) #try abstract version
else: #undecided on final unproved circuit. Probably can't do better.
return 'UNDECIDED'
def try_split():
abc('w %s_savetemp.aig'%f_name)
na = n_ands()
split(3)
if n_ands()> 2*na:
abc('r %s_savetemp.aig'%f_name)
def time_diff():
global last_time
new_time = time.clock()
diff = new_time - last_time
last_time = new_time
result = 'Lapsed time = %.2f sec.'%diff
return result
def prove_all_ind():
"""Tries to prove output k by induction, using other outputs as constraints.
If ever an output is proved
it is set to 0 so it can't be used in proving another output to break circularity.
Finally all zero'ed ooutputs are removed.
Prints out unproved outputs Finally removes 0 outputs
"""
global n_pos_proved, n_pos_before
n_proved = 0
N = n_pos()
## remove_0_pos()
## print '0 valued output removal changed POs from %d to %d'%(N,n_pos())
if n_pos() == 1:
return
abc('w %s_osavetemp.aig'%f_name)
lst = range(n_pos())
## list.reverse()
## for j in list[1:]:
for j in lst:
## abc('zeropo -N 0')
abc('swappos -N %d'%j)
## remove_0_pos() #may not have to do this if constr works well with 0'ed outputs
abc('constr -N %d'%(n_pos()-1))
abc('fold')
n = max(1,n_ands())
f = max(1,min(40000/n,16))
f = int(f)
abc('ind -ux -C 10000 -F %d'%f)
## run_command('print_status')
status = get_status()
abc('r %s_osavetemp.aig'%f_name)
if status == Unsat:
## print '+',
abc('zeropo -N %d'%j)
abc('w %s_osavetemp.aig'%f_name) #if changed, store it permanently
if j < n_pos_before - n_pos_proved:
n_proved = n_proved + 1 # keeps track of real POs proved.
elif status < Unsat:
print '-%d'%j,
else:
print '*%d'%j,
remove_0_pos()
n_pos_proved = n_pos_proved + n_proved
print '\nThe number of POs reduced from %d to %d'%(N,n_pos())
#return status
def prove_all_mtds(t):
"""
Tries to prove output k with multiple methods in parallel,
using other outputs as constraints. If ever an output is proved
it is set to 0 so it can't be used in proving another output to break circularity.
Finally all zero'ed ooutputs are removed.
"""
N = n_pos()
## remove_0_pos()
## print '0 valued output removal changed POs from %d to %d'%(N,n_pos())
abc('w %s_osavetemp.aig'%f_name)
list = range(n_pos())
for j in list:
run_command('swappos -N %d'%j)
## remove_0_pos() #may not have to do this if constr works well with 0'ed outputs
abc('constr -N %d'%(n_pos()-1))
abc('fold')
## cmd = '&get;,pdr -vt=%d'%t #put in parallel.
## abc(cmd)
verify(pdrs+bmcs+intrps+sims,t)
status = get_status()
abc('r %s_osavetemp.aig'%f_name)
if status == Unsat:
print '+',
abc('zeropo -N %d'%j)
abc('w %s_osavetemp.aig'%f_name) #if changed, store it permanently
print '%d'%j,
assert not is_sat(), 'one of the POs is SAT' #we can do better than this
remove_0_pos()
print '\nThe number of POs reduced from %d to %d'%(N,n_pos())
#return status
def prove_all_pdr(t):
"""Tries to prove output k by pdr, using other outputs as constraints. If ever an output is proved
it is set to 0 so it can't be used in proving another output to break circularity.
Finally all zero'ed ooutputs are removed. """
N = n_pos()
## remove_0_pos()
print '0 valued output removal changed POs from %d to %d'%(N,n_pos())
abc('w %s_osavetemp.aig'%f_name)
list = range(n_pos())
for j in list:
abc('swappos -N %d'%j)
## remove_0_pos() #may not have to do this if constr works well with 0'ed outputs
abc('constr -N %d'%(n_pos()-1))
abc('fold')
cmd = '&get;,pdr -vt=%d'%t #put in parallel.
abc(cmd)
status = get_status()
abc('r %s_osavetemp.aig'%f_name)
if status == Unsat:
print '+',
abc('zeropo -N %d'%j)
abc('w %s_osavetemp.aig'%f_name) #if changed, store it permanently
print '%d'%j,
remove_0_pos()
print '\nThe number of POs reduced from %d to %d'%(N,n_pos())
#return status
def prove_each_ind():
"""Tries to prove output k by induction, """
N = n_pos()
remove_0_pos()
print '0 valued output removal changed POs from %d to %d'%(N,n_pos())
abc('w %s_osavetemp.aig'%f_name)
list = range(n_pos())
for j in list:
abc('cone -s -O %d'%j)
n = max(1,n_ands())
f = max(1,min(40000/n,16))
f = int(f)
abc('ind -u -C 10000 -F %d'%f)
status = get_status()
abc('r %s_osavetemp.aig'%f_name)
if status == Unsat:
print '+',
abc('zeropo -N %d'%j)
abc('w %s_osavetemp.aig'%f_name) #if changed, store it permanently
print '%d'%j,
remove_0_pos()
print '\nThe number of POs reduced from %d to %d'%(N,n_pos())
#return status
def prove_each_pdr(t):
"""Tries to prove output k by PDR. If ever an output is proved
it is set to 0. Finally all zero'ed ooutputs are removed. """
N = n_pos()
remove_0_pos()
print '0 valued output removal changed POs from %d to %d'%(N,n_pos())
abc('w %s_osavetemp.aig'%f_name)
list = range(n_pos())
for j in list:
abc('cone -O %d -s'%j)
abc('scl -m')
abc('&get;,pdr -vt=%d'%t)
status = get_status()
abc('r %s_osavetemp.aig'%f_name)
if status == Unsat:
print '+',
abc('zeropo -N %d'%j)
abc('w %s_osavetemp.aig'%f_name) #if changed, store it permanently
print '%d'%j,
remove_0_pos()
print '\nThe number of POs reduced from %d to %d'%(N,n_pos())
#return status
def disprove_each_bmc(t):
"""Tries to prove output k by PDR. If ever an output is proved
it is set to 0. Finally all zero'ed ooutputs are removed. """
N = n_pos()
remove_0_pos()
print '0 valued output removal changed POs from %d to %d'%(N,n_pos())
abc('w %s_osavetemp.aig'%f_name)
list = range(n_pos())
for j in list:
abc('cone -O %d -s'%j)
abc('scl -m')
abc('bmc3 -T %d'%t)
status = get_status()
abc('r %s_osavetemp.aig'%f_name)
if status == Sat:
print '+',
abc('zeropo -N %d'%j)
abc('w %s_osavetemp.aig'%f_name) #if changed, store it permanently
print '%d'%j,
remove_0_pos()
print '\nThe number of POs reduced from %d to %d'%(N,n_pos())
#return status
def pord_1_2(t):
""" two phase pord. First one tries with 10% of the time. If not solved then try with full time"""
global n_pos_proved, ifpord1, pord_on
pord_on = True # make sure that we do not reparameterize after abstract in prove_2
n_pos_proved = 0
if ifpord1:
print 'Trying each output for %0.2f sec'%(.1*t)
result = pord_all(.1*t) #we want to make sure that there is no easy cex.
if (result <= Unsat):
return result
ifpord1 = 0
print 'Trying each output for %0.2f sec'%t
result = pord_all(t+2*G_T) #make sure there is enough time to abstract
pord_on = False #done with pord
return result
def pord_all(t):
"""Tries to prove or disprove each output j by PDRM BMC3 or SIM. in time t"""
global cex_list, n_pos_proved, last_cx, pord_on, ifpord1
print 'last_cx = %d'%last_cx
btime = time.time()
N = n_pos()
## remove_0_pos()
print '0 valued output removal changed POs from %d to %d'%(N,n_pos())
## bmc_ss(t)
## if is_sat():
## cex_list = cex_get_vector()
## return Sat
prove_all_ind() ############ change this to keep track of n_pos_proved
nn = n_pos()
abc('w %s_osavetemp.aig'%f_name)
if nn < 4: #Just cut to the chase immediately.
return Undecided
lst = range(n_pos())
proved = disproved = []
## abc('&get') #using this space to save original file
## with redirect.redirect( redirect.null_file, sys.stdout ):
## with redirect.redirect( redirect.null_file, sys.stderr ):
cx_list = []
n_proved = 0
lcx = last_cx + 1
lst = lst[lcx:]+lst[:lcx]
lst.reverse()
n_und = 0
for j in lst:
print ''
print j,
abc('&put; cone -O %d -s'%j)
abc('scl -m')
## ps()
## run_parallel(slps+sims+bmcs+pdrs+[6],t,'US')
result = run_sp2_par(t)
print 'run_sp2_par result is %s'%result
if result == 'UNDECIDED':
n_und = n_und + 1
status = Undecided
if ((n_und > 1) and not ifpord1):
break
elif result == 'SAT':
status = Sat
disproved = disproved + [j]
last_cx = j
cx = cex_get()
cx_list = cx_list + [cx]
assert len(cx_list) == len(disproved), cx_list
if len(cx_list) > 0:
break
else: #is unsat here
status = Unsat
proved = proved + [j]
if j < n_pos_before - n_pos_proved:
n_proved = n_proved +1
n_pos_proved = n_pos_proved + n_proved
print '\nProved %d outputs'%len(proved)
print 'Disproved %d outputs'%len(disproved)
print 'Time for pord_all was %0.2f'%(time.time() - btime)
NN = len(proved+disproved)
cex_list = cx_list
if len(disproved)>0:
assert status == Sat, 'status = %d'%status
return Sat
else:
abc('r %s_osavetemp.aig'%f_name)
## abc('&put') # returning original to work spece
remove(proved)
print '\nThe number of unproved POs reduced from %d to %d'%(N,n_pos())
if n_pos() > 0:
return Undecided
else:
return Unsat
def bmc_ss(t):
"""
finds a set cexs in t seconds starting at 2*N where N is depth of bmc -T 1
The cexs are put in the global cex_list
"""
global cex_list
x = time.time()
tt = min(10,max(1,.05*t))
abc('bmc3 -T %0.2f'%tt)
N = n_bmc_frames()
if N <= max_bmc:
return Undecided
## print bmc_depth()
## abc('bmc3 -C 1000000 -T %f -S %d'%(t,int(1.5*max(3,max_bmc))))
run_command('bmc3 -vs -C 1000000 -T %f -S %d'%(t,2*N))
if is_sat():
cex_list = cex_get_vector() #does this get returned from a concurrent process?
n = count_non_None(cex_list)
print '%d cexs found in %0.2f sec at frame %d'%(n,(time.time()-x),cex_frame())
return get_status()
def list_non_None(lst):
""" return [i for i,s in enumerate(cex_list) if not s == None]"""
L = []
for i in range(len(lst)):
if not lst[i] == None:
L = L + [i]
return L
def count_non_None(lst):
#return len([i for i,s in enumerate(cex_list) if not s == None]
count = 0
for i in range(len(lst)):
if not lst[i] == None:
count = count + 1
return count
def remove_disproved_pos(lst):
for i in range(len(lst)):
if not lst[i] == None:
abc('zeropo -N %d'%i)
remove_0_pos()
def bmc_s(t):
""" finds a cex in t seconds starting at 2*N where N is depth of bmc -T 1"""
x = time.time()
tt = min(5,max(1,.05*t))
abc('bmc3 -T %0.2f'%tt)
if is_sat():
print 'cex found in %0.2f sec at frame %d'%((time.time()-x),cex_frame())
return get_status()
## abc('bmc3 -T 1')
N = n_bmc_frames()
## print bmc_depth()
## abc('bmc3 -C 1000000 -T %f -S %d'%(t,int(1.5*max(3,max_bmc))))
cmd = 'bmc3 -J 2 -D 4000 -C 1000000 -T %f -S %d'%(t,2*N)
## print cmd
abc(cmd)
if is_sat():
print 'cex found in %0.2f sec at frame %d'%((time.time()-x),cex_frame())
return get_status()
def pdr(t):
abc('&get; ,pdr -vt=%f'%t)
return RESULT[get_status()]
def pdrm(t):
abc('pdr -v -C 0 -T %f'%t)
return RESULT[get_status()]
def pdrmm(t):
abc('pdr -mv -C 0 -T %f'%t)
return RESULT[get_status()]
def split(n):
abc('orpos;&get')
abc('&posplit -v -N %d;&put;dc2'%n)
trim()
def keep_splitting():
for j in range(5):
split(5+j)
no = n_pos()
status = prove_g_pos_split()
if status <= Unsat:
return status
if no == n_pos():
return Undecided
def drill(n):
run_command('&get; &reachm -vcs -H 5 -S %d -T 50 -C 40'%n)
def prove_1():
"""
A version of prove(). Called only during prove_pos or prove_g_pos or prove_only when we
have speculated and produced multiple outputs. Does speculation only in final_verify_recur.
Proves all the outputs together. If ever an abstraction was done then
if SAT is returned,we make RESULT return "undecided".
"""
global x_factor,xfi,f_name,x, initial_f_name
x = time.time()
max_bmc = -1
K = 0
print 'Initial: ',
ps()
x_factor = xfi
print 'x_factor = %f'%x_factor
write_file('smp')
initial_f_name_save = initial_f_name #needed because we are making local backups here.
initial_f_name = '%s_temp'%initial_f_name
abc('w %s_backup_%d.aig'%(initial_f_name,K)) #backup 0
K = K +1 #K = 1 is next backup
set_globals()
print'\n***Running abstract'
nl_b = n_latches()
status = abstract()
trim()
write_file('abs')
status = process_status(status)
if ((status <= Unsat) or status == Error):
if status < Unsat:
print 'CEX in frame %d'%cex_frame(),
print 'abstract found a cex in unabstacted circuit'
print 'Time for proof = %f sec.'%(time.time() - x)
initial_f_name = initial_f_name_save
return RESULT[status]
print 'Time for proof = %f sec.'%(time.time() - x)
initial_f_name = initial_f_name_save
return RESULT[status]
abc('w %s_backup_%d.aig'%(initial_f_name,K)) #backup 1
print 'Entering final_verify_recur(2) from prove_1()'
status = final_verify_recur(2)
trim()
write_file('final')
print 'Time for proof = %f sec.'%(time.time() - x)
initial_f_name = initial_f_name_save
return RESULT[status]
def pre_reduce():
x = time.clock()
pre_simp()
write_file('smp')
abstract()
write_file('abs')
print 'Time = %f'%(time.clock() - x)
def sublist(L,I):
# return [s for i,s in enumerate(L) if i in I]
z = []
for i in range(len(I)):
s = L[I[i]],
s = list(s)
z = z + s
return z
#PARALLEL FUNCTIONS
""" funcs should look like
funcs = [pyabc_split.defer(abc)('&get;,bmc -vt=50;&put'),pyabc_split.defer(super_prove)()]
After this is executed funcs becomes a special list of lambda functions
which are given to abc_split_all to be executed as in below.
It has been set up so that each of the functions works on the current aig and
possibly transforms it. The new aig and status is always read into the master when done
"""
def tf():
result = top_fork()
return result
def top_fork(J,t):
global x_factor, final_verify_time, last_verify_time, methods
set_globals()
mtds = sublist(methods,J)
F = create_funcs(J,t)
print 'Running %s in parallel for max %d sec.'%(mtds,t)
(m,result) = fork_last(F,mtds) #FORK here
return get_status()
def run_sp2_par(t):
""" Runs the single method super_prove(2), timed for t seconds."""
global cex_list,methods
J = slps+[6]
funcs = create_funcs(J,t)
y = time.time()
for i,res in pyabc_split.abc_split_all(funcs):
#print 'i,res = %d,%s'%(i,res)
t = time.time()-y
if i == 0:
print 'sleep timer expired in %0.2f'%t
return 'UNDECIDED'
else:
if res == 'UNSAT':
print 'SUPER_PROVE2 proved UNSAT in %0.2f sec.'%t
return 'UNSAT'
elif res == 'UNDECIDED':
print 'SUPER_PROVE2 proved UNDECIDED in %0.2f sec.'%t
return 'UNDECIDED'
else:
print 'SUPER_PROVE2 found cex in %0.2f sec.'%t
return 'SAT'
def run_parallel(J,t,BREAK):
""" Runs the listed methods J, each for time = t, in parallel and
breaks according to BREAK = subset of '?USLB'"""
global cex_list, methods
mtds = sublist(methods,J)
F = create_funcs(J,t) #if J = [] we are going to create functions that process each output separately.
#if 18, then these are run in parallel with sleep
if ((J == []) ):
result = fork_break(F,mtds,BREAK)
## #redirect here to suppress printouts.
## with redirect.redirect( redirect.null_file, sys.stdout ):
## with redirect.redirect( redirect.null_file, sys.stderr ):
## result = fork_break(F,mtds,BREAK)
elif 'L' in BREAK:
result = fork_last(F,mtds)
elif 'B' in BREAK:
result = fork_best(F,mtds)
else:
result = fork_break(F,mtds,BREAK)
return result
def fork_all(funcs,mtds):
"""Runs funcs in parallel and continue running until all are done"""
global methods
y = time.time()
for i,res in pyabc_split.abc_split_all(funcs):
status = prob_status()
t = time.time()-y
if not status == -1: #solved here
if status == 1: #unsat
print '%s proved UNSAT in %f sec.'%(mtds[i],t)
else:
print '%s found cex in %f sec. - '%(mtds[i],t),
if not mtds[i] == 'REACHM':
print 'cex depth at %d'%cex_frame()
else:
print ' '
continue
else:
print '%s was undecided in %f sec. '%(mtds[i],t)
return i,res
def fork_break(funcs,mtds,BREAK):
"""
Runs funcs in parallel and breaks according to BREAK <= '?US'
If mtds = 'sleep' or [], we are proving outputs in parallel
Saves cex's found in cex_list in case we are proving POs.
"""
global methods,last_verify_time,seed,cex_list,last_winner,last_cex
seed = seed + 3 # since parallel processes do not chenge the seed in the prime process, we need to change it here
cex_list = lst = []
y = time.time() #use wall clock time because parent fork process does not use up compute time.
for i,res in pyabc_split.abc_split_all(funcs):
status = get_status()
t = time.time()-y
lm = len(mtds)
if ((lm < 2) and not i == 0): # the only single mtds case is where it is 'sleep'
M = 'Output %d'%(i-lm)
else:
M = mtds[i]
last_winner = M
if M == 'sleep':
print 'sleep: time expired in %s sec.'%convert(t)
assert status >= Unsat,'status = %d'%status
break
if ((status > Unsat) and '?' in BREAK): #undecided
break
elif status == Unsat: #unsat
print '%s: UNSAT in %s sec.'%(M,convert(t))
if 'U' in BREAK:
break
elif status < Unsat: #status == 0 - cex found
if M in methods:
if methods.index(M) in exbmcs+allreachs+allpdrs+[1]: #set the known best depth so far. [1] is interp
set_max_bmc(n_bmc_frames())
last_cex = M
print '%s: -- cex in %0.2f sec. at depth %d => '%(M,t,cex_frame()),
cex_list = cex_list+[cex_get()] #accumulates multiple cex's and puts them on list.
if len(cex_list)>1:
print 'len(cex_list): %d'%len(cex_list)
if 'S' in BREAK:
break
else:
continue
return i,status
def fork_best(funcs,mts):
""" fork the functions, If not solved, take the best result in terms of AIG size"""
global f_name
n = len(mts)-1
y = time.time()
m_best = -1
best_size = [n_pis(),n_latches(),n_ands()]
## print best_size
abc('w %s_best_aig.aig'%f_name)
for i,res in pyabc_split.abc_split_all(funcs):
status = prob_status()
## print i,
## ps()
## print i,res,
#ps()
if not status == -1: #solved here
m = i
t = time.time()-y
if status == 1: #unsat
print '%s proved UNSAT in %f sec.'%(mtds[i],t)
else:
print '%s found cex in %f sec. - '%(mtds[i],t),
break
else:
cost = rel_cost(best_size)
## print i,cost
if cost < 0:
best_size = [n_pis(),n_latches(),n_ands()]
## print best_size
m_best = i
## print m_best
abc('w %s_best_aig.aig'%f_name)
abc('r %s_best_aig.aig'%f_name)
return m_best,res
def fork_last(funcs,mtds):
""" fork the functions, and take first definitive answer, but
if last method ends first, then kill others"""
n = len(mtds)-1
m = -1
y = time.time()
lst = ''
print mtds
for i,res in pyabc_split.abc_split_all(funcs):
status = prob_status()
if not status == -1: #solved here
m = i
t = int(time.time()-y)
if status == 1: #unsat
print '%s proved UNSAT in %d sec.'%(mtds[i],t)
else:
print '%s found cex in %s sec. - '%(mtds[i],convert(t)),
break
elif i == n:
t = int(time.time()-y)
m = i
print '%s: %d sec.'%(mtds[i],t)
ps()
break
elif mtds[i] == 'sleep':
t = time.time()-y
print 'sleep timer expired in %0.2f'%t
break
lst = lst + ', '+mtds[i]
return m,res
def fork(funcs,mtds):
""" runs funcs in parallel This keeps track of the verify time
when a cex was found, and if the time to find
the cex was > 1/2 allowed time, then last_verify_time is increased by 2"""
global win_list, methods, last_verify_time,seed
beg_time = time.time()
i,res = fork_break(funcs,mtds,'US') #break on Unsat of Sat.
t = time.time()-beg_time #wall clock time because fork does not take any compute time.
if t > .4*last_verify_time:
## if t > .15*last_verify_time: ##### temp
t = last_verify_time = last_verify_time + .1*t
#print 'verify time increased to %s'%convert(t)
assert res == get_status(),'res: %d, status: %d'%(res,get_status())
return i,res
def save_time(M,t):
global win_list,methods
j = methods.index(M)
win_list = win_list + [(j,t)]
#print win_list
def summarize(lst):
result = [0]*10
for j in range(len(lst)):
k = lst[j]
result[k[0]]=result[k[0]]+k[1]
return result
def top_n(lst,n):
result = []
ll = list(lst) #makes a copy
m = min(n,len(ll))
for i in range(m):
mx_index = ll.index(max(ll))
result = result + [mx_index]
ll[mx_index] = -1
return result
def super_pre_simp():
while True:
nff = n_latches()
print 'Calling pre_simp'
pre_simp()
if n_latches() == nff:
break
#______________________________
#new synthesis command
def synculate(t):
"""
Finds candidate sequential equivalences and refines them by simulation, BMC, or reachability
using any cex found. If any are proved, then they are used to reduce the circuit. The final aig
is a new synthesized circuit where all the proved equivalences are merged.
If we put this in a loop with increasing verify times, then each time we work with a simpler model
and new equivalences. Should approach srm. If in a loop, we can remember the cex_list so that we don't
have to deal with disproved equivalences. Then use refine_with_cexs to trim the initial equivalences.
If used in synthesis, need to distinguish between
original outputs and new ones. Things to take care of: 1. a PO should not go away until it has been processes by merged_proved_equivalences
2. Note that &resim does not use the -m option where as in speculation - m is used. It means that if
an original PO isfound to be SAT, the computation quits becasue one of the output
miters has been disproved.
"""
global G_C,G_T,n_pos_before, x_factor, n_latches_before, last_verify_time, f_name,cex_list, max_verify_time
def refine_with_cexs():
"""Refines the gores file to reflect equivalences that go away because of cexs in cex_list"""
global f_name
abc('&r %s_gores.aig'%f_name)
for j in range(len(cex_list)):
cex_put(cex_list[j])
run_command('&resim') #put the jth cex into the cex space and use it to refine the equivs
abc('&w %s_gores.aig'%f_name)
return
def generate_srms():
"""generates a synthesized reduced model (srms) from the gores file"""
global f_name, po_map
abc('&r %s_gores.aig; &srm -sf; r gsrms.aig; w %s_gsrms.aig'%(f_name,f_name))
print 'New srms = ',ps()
po_map = range(n_pos())
return 'OK'
def merge_proved_equivalences():
#this only changes the gores file.
run_command('&r %s_gores.aig; &equiv_mark -vf %s_gsrms.aig; &reduce -v; &w %s_gores.aig'%(f_name,f_name,f_name))
return
def generate_equivalences():
set_globals()
t = max(1,.5*G_T)
r = max(1,int(t))
cmd = "&get; &equiv2 -C %d -F 200 -T %f -S 1 -R %d"%((G_C),t,r)
abc(cmd)
#run_command('&ps')
eq_simulate(.5*t)
#run_command('&ps')
cmd = '&semi -W 63 -S 5 -C 500 -F 20 -T %d'%(.5*t)
abc(cmd)
#run_command('&ps')
run_command('&w %s_gores.aig'%f_name)
remove_0_pos() #makes sure no 0 pos to start
cex_list = []
n_pos_before = n_pos()
n_latches_before = n_latches()
## print 'Generating equivalences'
generate_equivalences()
## print 'Generating srms file'
generate_srms() #this should not create new 0 pos
## if n_pos()>100:
## removed
remove_0_pos()
n_pos_last = n_pos()
if n_pos_before == n_pos():
print 'No equivalences found. Quitting synculate'
return Undecided_no_reduction
print 'Initial synculation: ',ps()
## ps()
set_globals()
simp_sw = init = True
simp_sw = False #temporary
print '\nIterating synculation refinement'
abc('w initial_sync.aig')
max_verify_time = t
print 'max_verify_time = %d'%max_verify_time
"""
in the following loop we increase max_verify_time by twice time spent to find last cexs or Unsat's
We iterate only when we have proved cex + unsat > 1/2 n_pos. Then we update srms and repeat.
"""
while True: # refinement loop
t = max_verify_time #this may have been increased since the last loop
## print 'max_verify_time = %d'%max_verify_time
set_globals()
if not init:
generate_srms() #generates a new gsrms file and leaves it in workspace
## print 'generate_srms done'
if n_pos() == n_pos_before:
break
if n_pos() == n_pos_last: #if nothing new, then quit if max_verification time is reached.
if t > max_verify_time:
break
if simp_sw: #Warning: If this holds then simplify could create some 0 pos
na = n_ands()
simplify()
while True:
npo = n_pos()
## print 'npos = %d'%npo
merge_proved_equivalences() #So we need to merge them here. Can merging create more???
generate_srms()
if npo == n_pos():
break
if n_ands() > .7*na: #if not significant reduction, stop simplification
simp_sw = False #simplify only once.
if n_latches() == 0:
return check_sat()
n_pos_last = n_pos()
init = False # make it so that next time it is not the first time through
syn_par(t)
if (len(cex_list)+len(result)) == 0: #nothing happened aand ran out of time.
break
abc('w %s_gsrms.aig'%f_name)
#print 'No. of cexs after syn_parallel = %d'%len(cex_list)
merge_proved_equivalences() #changes the underlying gores file by merging fanouts of proved eqs
#print 'merge done'
refine_with_cexs() #changes the gores file by refining the equivalences in it using cex_list.
#print 'refine_with_cexs done'
continue
extract(0,n_pos_before) #get rid of unproved outputs
return
def syn_par(t):
"""prove n outputs at once and quit at first cex. Otherwise if no cex found return aig
with the unproved outputs"""
global trim_allowed,max_verify_time, n_pos_before
global cex_list, result
b_time = time.time()
n = n_pos()
if n == n_pos_before:
return
mx = n_pos()
if n_pos() - n_pos_before > 50:
mx = n_pos_before + 50
r = range(n_pos_before, mx)
N = max(1,(mx-n_pos_before)/2)
abc('w %s__ysavetemp.aig'%f_name)
F = [eval(FUNCS[18])] #create a timer function
#print r
for i in r:
F = F + [eval('(pyabc_split.defer(verify_only)(%d,%d))'%(i,t))]
cex_list = result = []
outcome = ''
#redirect printout here
## with redirect.redirect( redirect.null_file, sys.stdout ):
## with redirect.redirect( redirect.null_file, sys.stderr ):
for i,res in pyabc_split.abc_split_all(F):
status = get_status()
## print i
if i == 0: #timed out
outcome = 'time expired after = %d'%(time.time() - b_time)
break
if status < Unsat:
cex_list = cex_list + [cex_get()]
if status == Unsat:
result = result + [r[i-1]]
if (len(result)+len(cex_list))>= N:
T = time.time() - b_time
if T > max_verify_time/2:
max_verify_time = 2*T
break
continue
if not outcome == '':
print outcome
## print 'cex_list,prove_list = ',cex_list,result
abc('r %s__ysavetemp.aig'%f_name) #restore initial aig so that pos can be 0'ed out
if not result == []: # found some unsat's
## min_r = min(result)
## max_r = max(result)
## no = n_pos()
## assert (0 <= min_r and max_r < no), 'min_r, max_r, length = %d, %d, %d'%(min_r,max_r,len(result))
zero(result)
return
#print "Number PO's proved = %d"%len(result)
def absec(n):
#abc('w t.aig')
for j in range(n):
print '\nFrame %d'%(j+1)
run_command('absec -F %d'%(j+1))
if is_unsat():
print 'UNSAT'
break
"""
we might be proving some original pos as we go, and on the other hand we might have some equivalences that we
can't prove. There are two uses, in verification
verification - we want to remove the proved pos whether they are original or not. But if a cex for an original, then need to
remember this.
synthesis - the original outputs need to be kept and ignored in terms of cex's - supposedly they can't be proved.
"""
""" Experimental"""
def csec():
global f_name
if os.path.exists('%s_part0.aig'%f_name):
os.remove('%s_part0.aig'%f_name)
run_command('demiter')
if not os.path.exists('%s_part0.aig'%f_name):
return
run_command('r %s_part0.aig'%f_name)
ps()
run_command('comb')
ps()
abc('w %s_part0comb.aig'%f_name)
run_command('r %s_part1.aig'%f_name)
ps()
run_command('comb')
ps()
abc('w %s_part1comb.aig'%f_name)
run_command('&get; &cec %s_part0comb.aig'%(f_name))
if is_sat():
return 'SAT'
if is_unsat():
return 'UNSAT'
else:
return 'UNDECIDED'
###########################
#### we will verify outputs ORed in groups of g[i]
#### here we take div = N so no ORing
## div = max(1,N/1)
## g = distribute(N,div)
## if len(g) <= 1:
## t = tt
## g.reverse()
#### print g
## x = 0
## G = []
## for i in range(div):
## y = x+g[i]
## F = F + [eval('(pyabc_split.defer(verify_range)(%d,%d,%s))'%(x,y,convert(t)))]
## G = G + [range(x,y)]
## x = y
#### print G
###########################
def sop_balance(k):
abc('st; if -K %d;ps'%k)
for i in range(2):
run_command('st; if -K %d;ps'%k)
run_command('st; if g -C %d -K %d;ps'%(k+4,k+4))
for i in range(3):
run_command('st;&get; &dch; &put; if -K %d;ps'%k)
def map_lut_dch(k):
for i in range(5):
run_command('st;if -a -K %d; ps; st; dch; ps; if -a -K %d; ps; mfs ;ps; lutpack; ps'%(k,k))
def map_lut(k):
for i in range(5):
run_command('st; if -e -K %d; ps; mfs ;ps; lutpack -L 50; ps'%(k))