diff options
Diffstat (limited to 'scripts/abc_common.py')
| -rw-r--r-- | scripts/abc_common.py | 2007 |
1 files changed, 0 insertions, 2007 deletions
diff --git a/scripts/abc_common.py b/scripts/abc_common.py deleted file mode 100644 index df2b731b..00000000 --- a/scripts/abc_common.py +++ /dev/null @@ -1,2007 +0,0 @@ -from pyabc import * -import pyabc_split -import par -import redirect -import sys -import os -import time -import math - - -global G_C,G_T,latches_before_abs,latches_before_pba,n_pos_before,x_factor - -""" -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 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,', 'UNDCIDED' ) -Sat_reg = 0 -Sat_true = 1 -Unsat = 2 -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 - -# Function definitions: -# simple functions: ________________________________________________________________________ -# set_globals, abc, q, x, has_any_model, is_sat, is_unsat, push, pop - -# ALIASES -def p(): - return prove() - -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'%f_name) - n = n_pis() - abc('r %s_savetempreal.aig'%f_name) - return n - -def long(t): - if t<20: - t = t - else: - t = 20+(t-20)/3 - return max(10,t) - -def rif(): - """Not used""" - global f_name - print 'Type in the name of the aig file to be read in' - s = raw_input() - if s[-5:] == '.blif': - f_name = s[:-5] - else: - f_name = s - s = s+'.blif' - run_command(s) - x('st;constr -i') - print_circuit_stats() - a = n_ands() - f = max(1,30000/a) - f = min (f,16) - x('scorr -c -F %d'%f) - x('fold') - print_circuit_stats() - x('w %s_c.aig'%f_name) - -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 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 set_fname(name): - """ Another way to set an f_name, but currently this is not used""" - global f_name - s = name - if s[-4:] == '.aig': - f_name = s[:-4] - else: - f_name = s - s = s+'.aig' - #read in file - run_command(s) - #print_circuit_stats() - -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 - x_factor = 1 - max_bmc = -1 - - if fname is None: - print 'Type in the name of the aig file to be read in' - s = raw_input() - else: - s = fname - - if s[-4:] == '.aig': - f_name = s[:-4] - else: - f_name = s - s = s+'.aig' - - run_command(s) - initial_f_name = f_name - init_initial_f_name = f_name - -def read_file(): - read_file_quiet() - print_circuit_stats() - -def rf(): - 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, - print_circuit_stats() - abc('w '+ss) - -def wf(): - """Not used""" - print 'input type of file to be written' - s = raw_input() - write_file(s) - -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 - 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) - 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 x(s): - """execute an ABC command""" - print "RUNNING: ", s - run_command(s) - -def has_any_model(): - """ check if a satisfying assignment has been found""" - res = has_comb_model() or has_seq_model() - return res - -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) - - - -def fast_int(n): - """This is used to eliminate easy-to-prove outputs. Arg n is conflict limit to be used - in the interpolation routine. Typically n = 1 or 10""" - n_po = n_pos() - abc('int -k -C %d'%n) - print 'Reduced POs from %d to %d'%(n_po,n_pos()) - -def refine_with_cex(): - """Refines the greg (which contains the original problem with the set of FF's that have been abstracted). - This generates a new abstraction (gabs) and modifies the greg file to reflect which regs are in the - current abstraction""" - global f_name - print 'CEX in frame %d for output %d'%(cex_frame(),cex_po()) - abc('&r %s_greg.aig; &abs_refine; &w %s_greg.aig'%(f_name,f_name)) - return - -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: ', - print_circuit_stats() - return - - -#more complex functions: ________________________________________________________ -#, abstract, pba, speculate, final_verify, dprove3 - - -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() -## print 'simplify initial ', -## ps() - #abc('w t.aig') - n=n_ands() - abc('scl') - if n > 40000: - abc('&get;&scl;&put') - n = n_ands() - if n < 100000: - abc("&dc2;&put;dr;&get;&lcorr;&dc2;&put;dr;&get;&scorr;&fraig;&dc2;&put;dr") - run_command('ps') - print '.', - n = n_ands() - if n<60000: - abc("&get;&scorr -F 2;&put;dc2rs") - print '.', - #ps() - else: - abc("dc2rs") - print '.', - #ps() - n = n_ands() - n = n_ands() - if n <= 40000: - print '.', - #ps() - if n > 30000: - abc("dc2rs") - print '.', -## else: -## abc("scorr -F 2;dc2rs") -## print '.', -## ps() - n = max(1,n_ands()) - #ps() - if n < 30000: - abc('scl;rw;dr;lcorr;rw;dr') - m = int(min( 60000/n, 16)) - #print 'm = %d'%m - if m >= 1: - j = 1 - while j <= m: - set_size() - #print 'j - %d'%j - #abc('scl;dr;dc2;scorr -C 5000 -F %d'%j) - if j<8: - abc('dc2') - else: - abc('dc2rs') - abc('scorr -C 5000 -F %d'%j) - if check_size(): - break - j = 2*j - #ps() - continue - print '.', - - -def iterate_simulation(latches_before): - """Subroutine of 'abstract' which does the refinement of the abstracted model, - using counterexamples found by simulation. Simulation is controlled by the amount - of memory it might use. At first wide but shallow simulation is done, bollowed by - successively more narrow but deeper simulation""" - global x_factor, f_name -## print 'RUNNING simulation iteratively' - f = 5 - w = 255 - for k in range(9): - f = min(f *2, 3500) - w = max(((w+1)/2)-1,1) - print '.', - abc('sim -m -F %d -W %d'%(f,w)) - if not is_sat(): - continue - while True: - refine_with_cex() - if is_sat(): - print 'cex failed to refine abstraction ' - return Sat_true - generate_abs(0) - latches_after = n_latches() - print 'Latches increased to %d'%latches_after - if latches_after >= .99*latches_before: - abc('r %s_savetempabs.aig'%f_name) - print "No reduction!." - return Undecided_no_reduction - abc('sim -m -F %d -W %d'%(f,w)) - if not is_sat(): - break - -def simulate(): - """Simulation is controlled by the amount - of memory it might use. At first wide but shallow simulation is done, bollowed by - successively more narrow but deeper simulation""" - global x_factor, f_name -## print 'RUNNING simulation iteratively' - f = 5 - w = 255 - for k in range(9): - f = min(f *2, 3500) - w = max(((w+1)/2)-1,1) - print '.', - abc('sim -m -F %d -W %d'%(f,w)) - if is_sat(): - print 'cex found in frame %d'%cex_frame() - return 'SAT' - return 'UNDECIDED' - - -def iterate_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 - if NBF == -1: - F = 2000 - else: - F = 2*NBF - print '\nIterating BMC/PDR' - always_reach = 0 - cexf = 0 - reach_failed = 0 - while True: - #print 'Generating problem abstraction' - generate_abs(1) - set_globals() - latches_after = n_latches() - if latches_after >= .98*latches_before: -## print 'No reduction' -## abc('r &s_savetemp.aig'%f_name) - break - ri = n_real_inputs() # No. of inputs after trm - nlri = n_latches()+ri - #reach_allowed = ((nlri<150) or (((cexf>250))&(nlri<300))) - reach_allowed = ((nlri<75) or (((cexf>250))&(nlri<300))) - pdr_allowed = True - bmc = False - t = max(1,G_T) - if not F == -1: - F = int(1.5*max_bmc) - if (((reach_allowed or pdr_allowed ) and not reach_failed)): - #cmd = 'reach -B 200000 -F 3500 -T %f'%t - #cmd = 'reachx -e %d -t %d'%(int(long(t)),max(10,int(t))) - #cmd = 'reachx -t %d'%max(10,int(t)) - cmd = '&get;,pdr -vt=%f'%t - else: - #cmd = 'bmc3 -C %d -T %f -F %d'%(G_C,t,F) - bmc = True - cmd = '&get;,bmc -vt=%f'%(t) - #cmd = '&get;,pdr -vt=%f'%(t) - print '\n***RUNNING %s'%cmd - #run_command(cmd) - last_bmc = max_bmc - abc(cmd) - if prob_status() == 1: - #print 'Depth reached %d frames, '%n_bmc_frames() - print 'UNSAT' - return Unsat - cexf = cex_frame() - #print 'cex depth = %d'%cexf - #set_max_bmc(cexf -1) - if ((not is_sat()) ): - reach_failed = 1 # if ever reach failed, then we should not try it again on more refined models - if is_sat(): - #print 'CEX in frame %d for output %d'%(cex_frame(),cex_po()) - #set_max_bmc(cexf-1) - refine_with_cex() # if cex can't refine, status is set to Sat_true - if is_sat(): - print 'cex did not refine. Implies true_sat' - return Sat_true - else: - print "No CEX found in %d frames"%n_bmc_frames() - set_max_bmc(n_bmc_frames()) - if bmc: - break - elif max_bmc> 1.2*last_bmc: # if pdr increased significantly over abs, the assume OK - break - else: - continue - latches_after = n_latches() - if latches_after >= .98*latches_before: - abc('r %s_savetempabs.aig'%f_name) - print "No reduction!" - return Undecided_no_reduction - else: - 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 - set_globals() - latches_before_abs = n_latches() - abc('w %s_savetempabs.aig'%f_name) - print 'Start: ', - print_circuit_stats() - c = 1.5*G_C - #t = max(1,1.25*G_T) - t = 2*max(1,1.25*G_T) - s = min(max(3,c/30000),10) # stability between 3 and 10 - time = max(1,.01*G_T) - abc('&get;,bmc -vt=%f'%time) - print 'BMC went %d frames'%n_bmc_frames() - set_max_bmc(bmc_depth()) - f = max(2*max_bmc,20) - b = min(max(10,max_bmc),200) - cmd = '&get;,abs -bob=%d -stable=%d -timeout=%f -vt=%f -depth=%d'%(b,s,t,t,f) - print ' Running %s'%cmd - run_command(cmd) - if is_sat(): - print 'Found true counterexample in frame %d'%cex_frame() - return Sat_true - NBF = bmc_depth() - print 'Abstraction good to %d frames'%n_bmc_frames() - set_max_bmc(NBF) - abc('&w %s_greg.aig; &abs_derive; &put; w %s_gabs.aig'%(f_name,f_name)) -## print 'First abstraction: ', -## print_circuit_stats() - latches_after = n_latches() - #if latches_before_abs == latches_after: - if latches_after >= .98*latches_before_abs: - abc('r %s_savetempabs.aig'%f_name) - print "No reduction!" - return Undecided_no_reduction - # refinement loop - if (n_ands() + n_latches() + n_pis()) < 15000: - print '\n***Running simulation iteratively' - for i in range(5): - result = iterate_simulation(latches_before_abs) - if result == Restart: - return result - if result == Sat_true: - return result - result = iterate_abstraction_refinement(latches_before_abs, NBF) - #if the result is 'Restart' we return and the calling routine increase - #x_factor to try one more time. - return result - -def absv(n,v): - """This is a version of 'abstract' which can control the methods used in Een's abstraction code (method = n) - as well as whether we want to view the output of this (v = 1)""" - global G_C, G_T, latches_before_abs, x_factor - #input_x_factor() - #x_factor = 3 - set_globals() - latches_before_abs = n_latches() - print 'Start: ', - print_circuit_stats() - c = 1.5*G_C - t = max(1,1.25*G_T) - s = min(max(3,c/30000),10) # stability between 3 and 10 - if max_bmc == -1: - time = max(1,.01*G_T) - #abc('bmc3 -C %d -T %f -F 165'%(.01*G_C, time)) - abc('&get;,bmc -vt=%f'%time) - set_max_bmc(bmc_depth()) - f = min(250,1.5*max_bmc) - f = max(20, f) - f = 10*f - b = x_factor*20 - if not n == 0: - b = 10 - b = max(b,max_bmc+2) - b = b*2**(x_factor-1) - b = 2*b - print 'Neen abstraction params: Method #%d, %d conflicts, %d stable, %f sec.'%(n,c/3,s,t) - if v == 1: - run_command('&get; &abs_newstart -v -B %f -A %d -C %d -S %d -V %f'%(b,n,c/3,s,t)) - else: - abc('&get; &abs_newstart -v -B %f -A %d -C %d -S %d -T %f'%(b,n,c/3,s,t)) - set_max_bmc(n_bmc_frames()) - print 'Abstraction good to %d'%n_bmc_frames() - abc('&w %s_greg.aig; &abs_derive; &put; w %s_gabs.aig'%(f_name,f_name)) - print 'Final abstraction: ', - print_circuit_stats() - latches_after = n_latches() - if latches_after >= .98*latches_before_abs: - print "No reduction!" - return Undecided_no_reduction - return Undecided_reduction - -def spec(): - """Main speculative reduction routine. Finds candidate sequential equivalences and refines them by simulation, BMC, or reachability - using any cex found. """ - input_x_factor() - global G_C,G_T,n_pos_before, x_factor, n_latches_before - set_globals() - n_pos_before = n_pos() - n_latches_before = n_latches() - set_globals() - t = max(1,.5*G_T) - r = max(1,int(t)) - print '\n***Running &equiv2 with C = %d, T = %f sec., F = %d -S 1 -R %d'%(G_C,t,200,r) - abc("&get; &equiv2 -C %d -F 200 -T %f -S 1 -R %d; &semi -F 50; &speci -F 20 -C 1000;&srm; r gsrm.aig; w %s_gsrm.aig; &w %s_gore.aig"%((G_C),t,r,f_name,f_name)) - print 'Initial speculation: ', - print_circuit_stats() - print 'Speculation good to %d frames'%n_bmc_frames() - return - -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 - set_globals() - n_pos_before = n_pos() - - def refine_with_cex(): - """Refines the gore file to reflect equivalences that go away because of cex""" - global f_name - print 'CEX in frame %d for output %d'%(cex_frame(),cex_po()) - abc('&r %s_gore.aig; &resim -m; &w %s_gore.aig'%(f_name,f_name)) - #abc('&r %s_gore.aig; &equiv2 -vx ; &w %s_gore.aig'%(f_name,f_name)) - return - - def generate_srm(n): - """generates a speculated reduced model (srm) from the gore file""" - global f_name - pos = n_pos() - ab = n_ands() - 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 - if n == 0: - if ((pos == n_pos()) and (ab == n_ands())): - print 'Failed to refine' - return 'failed' - if n == 1: - print 'Spec. Red. Miter: ', - print_circuit_stats() - return 'OK' - - def run_simulation(n): - f = 5 - w = (256/n)-1 - for k in range(9): - f = min(f * 2, 3500) - w = max(((w+1)/2)-1,1) - print '.', - #generate_srm(0) - abc('sim -m -F %d -W %d'%(f,w)) - if not is_sat(): - continue - if cex_po() < n_pos_before: - print 'Sim found true cex: Output = %d, Frame = %d'%(cex_po(),cex_frame()) - return Sat_true - refine_with_cex() - if n_pos_before == n_pos(): - return Undecided_no_reduction - while True: - result = generate_srm(0) - if result == 'failed': - return Sat_true - abc('sim -m -F %d -W %d'%(f,w)) - if not is_sat(): - break - if cex_po() < n_pos_before: - print 'Sim found true cex: Output = %d, Frame = %d'%(cex_po(),cex_frame()) - return Sat_true - refine_with_cex() - if n_pos_before == n_pos(): - return Undecided_no_reduction - return Undecided_no_reduction - - n_pos_before = n_pos() - n_latches_before = n_latches() - set_globals() - t = max(1,.5*G_T) - r = max(1,int(t)) - abc('write spec_temp.aig') - print '\n***Running &equiv2 with C = %d, T = %f sec., F = %d -S 1 -R %d'%(G_C,t,200,r) -## abc("&get; &equiv2 -C %d -F 200 -T %f -S 1 -R %d; &semi -F 50; &speci -F 20 -C 1000;&srm; r gsrm.aig; w %s_gsrm.aig; &w %s_gore.aig"%((G_C),t,r,f_name,f_name)) - abc("&get; &equiv2 -C %d -F 200 -T %f -S 1 -R %d; &semi -W 63 -S 5 -C 500 -F 500; &speci -F 200 -C 5000;&srm; r gsrm.aig; w %s_gsrm.aig; &w %s_gore.aig"%((G_C),t,r,f_name,f_name)) - print 'Initial speculation: ', - print_circuit_stats() - #print 'Speculation good to %d frames'%n_bmc_frames() - #simplify() - if n_pos_before == n_pos(): - print 'No new outputs. Quitting speculate' - return Undecided_no_reduction # return result is unknown - if is_sat(): - #print '\nWARNING: if an abstraction was done, need to refine it further\n' - return Sat_true - if n_latches() > .98*n_latches_before: - pre_simp() - if n_latches() > .98*n_latches_before: - print 'Quitting speculation - not enough gain' - abc('r spec_temp.aig') - return Undecided_no_reduction # not worth it - k = n_ands() + n_latches() + n_pis() - n = 0 - if k < 15000: - n = 1 - elif k < 30000: - n = 2 - elif k < 60000: - n = 4 - elif k < 120000: - n = 8 - if n > 0: # simulation can run out of memory for too large designs, so be careful - print '\n***RUNNING simulation iteratively' - for i in range(5): - result = run_simulation(n) - if result == Sat_true: - return result - simp_sw = 1 - int_sw = 1 - reach_sw = 0 - cexf = 0 - reach_failed = 0 - init = 1 - run_command('write temptemp.aig') - print '\nIterating BMC or BDD reachability' - while True: # now try real hard to get the last cex. - set_globals() - if not init: - set_size() - result = generate_srm(1) - if check_size() == True: - print 'Failed to refine' - return Error - if result == 'failed': - return Sat_true - if simp_sw == 1: - na = n_ands() - simplify() - if n_ands() > .7*na: #if not significant reduction, stop simplification - simp_sw = 0 - if n_latches() == 0: - return check_sat() - init = 0 # make it so that next time it is not the first time through - time = max(1,G_T/(5*n_pos())) - if int_sw ==1: - npo = n_pos() - if n_pos() > .5*npo: # if not sufficient reduction, turn this off - int_sw = 0 - if is_sat(): #if fast interpolation found a cex - cexf = cex_frame() - set_max_bmc(cexf - 1) - if cex_po() < n_pos_before: - print 'Int found true cex: Output = %d, Frame = %d'%(cex_po(),cex_frame()) - return Sat_true - refine_with_cex() - if ((n_pos_before == n_pos()) or (n_latches_before == n_latches())): - abc('r temp_spec.aig') - return Undecided_no_reduction - if is_sat(): - print '1. cex failed to refine abstraction' - return Sat_true - continue - else: - if n_latches() == 0: - return check_sat() - ri = n_real_inputs() #seeing how many inputs would trm get rid of - nlri = n_latches() + ri - reach_allowed = ((nlri<75) or (((cexf>250)) and (nlri<300))) - pdr_allowed = True - bmc = False - if (((reach_allowed or pdr_allowed ) and not reach_failed)): - t = max(1,1.2*G_T) - f = max(3500, 2*max_bmc) - #cmd = 'reachx -t %d'%max(10,int(t)) - cmd ='&get;,pdr -vt=%f'%t - else: - t = max(1,1.5*G_T) - if max_bmc == -1: - f = 200 - else: - f = max_bmc - f = int(1.5*f) - #cmd = 'bmc3 -C %d -T %f -F %f'%(1.5*G_C,1.2*t,f) - bmc = True - cmd = '&get;,bmc -vt=%f'%(1.2*t) - print '\n***Running %s'%cmd - last_bmc = max_bmc - abc(cmd) - #run_command(cmd) - if is_sat(): - cexf = cex_frame() - #set_max_bmc(cexf - 1) - #This is a temporary fix since reachx always reports cex_ps = 0 - if ((cex_po() < n_pos_before) and (cmd[:4] == '&get')): - print 'BMC/PDR found true cex: Output = %d, Frame = %d'%(cex_po(),cex_frame()) - return Sat_true - #End of temporary fix - refine_with_cex()#change the number of equivalences - if n_pos_before == n_pos(): - return Undecided_no_reduction - continue - else: - set_max_bmc(n_bmc_frames()) - if prob_status() == 1: - #print 'Convergence reached in %d frames'%n_bmc_frames() - return Unsat - print 'No cex found in %d frames'%n_bmc_frames() - if bmc: - break - elif max_bmc > 1.2*last_bmc: - break - else: - reach_failed = 1 - init = 1 - continue - if n_pos_before == n_pos(): - return Undecided_no_reduction - else: - return Undecided_reduction - -def set_size(): - """Stores the problem size of the current design. Size is defined as (PIs, POs, ANDS, FF, max_bmc)""" - global npi, npo, nands, nff, nmd - npi = n_pis() - npo = n_pos() - nands = n_ands() - nff = n_latches() - nmd = max_bmc - -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 - result = ((npi == n_pis()) and (npo == n_pos()) and (nands == n_ands()) and (nff == n_latches()) and (nmd == max_bmc)) -## if result == 1: -## print 'Size unchanged' - 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""" - abc('trm') - if n == 1: - simplify() - if n_latches == 0: - return check_sat() - abc('trm') - if is_sat(): - return Sat_true - print 'After trimming: ', - print_circuit_stats() - #try_rpm() - set_globals() - t = max(1,.4*G_T) - print ' Running PDR for %d sec '%(t) - abc('&get;,pdr -vt=%f'%(t*.8)) - status = get_status() - if not status == Unsat: - print 'PDR went to %d frames, '%n_bmc_frames(), - print RESULT[status] - return status #temporary - if status <= Unsat: - return status - N = bmc_depth() - c = max(G_C/10, 1000) - t = max(1,.4*G_T) - print ' RUNNING interpolation with %d conflicts, max %d sec and 100 frames'%(c,t) - #abc('int -v -F 100 -C %d -T %f'%(c,t)) - abc(',imc -vt=%f '%t) - status = get_status() - if status <= Unsat: - print 'Interpolation went to %d frames, '%n_bmc_frames(), - print RESULT[status] - return status - L = n_latches() - I = n_real_inputs() - if ( ((I+L<200)&(N>100)) or (I+L<125) or L < 51 ): #heuristic that if bmc went deep, then reachability might also - t = max(1,.4*G_T) - cmd = 'reachx -t %d'%max(10,int(t)) - print ' Running %s'%cmd - abc(cmd) - status = get_status() - if status <= Unsat: - print 'Reachability went to %d frames, '%n_bmc_frames() - print RESULT[status] - return status - print 'BDD reachability aborted' - simplify() #why is this here - if n_latches() == 0: - print 'Simplified to 0 FF' - return check_sat() - set_max_bmc(bmc_depth()) # doesn't do anything - print 'No success, max_depth = %d'%max_bmc - return Undecided_reduction - -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.""" - status = prob_status() #interrogates ABC for the current status of the problem. - # 0 = SAT - if status == 1: - status = Unsat - if status == -1: #undecided - status = Undecided_no_reduction - return status - -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: - abc('trm') - 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 final_verify(): - """This is the final method for verifying anything is nothing else has worked. It first tries BDD reachability - if the problem is small enough. If this aborts or if the problem is too large, then interpolation is called.""" - global x_factor - set_globals() -## simplify() -## if n_latches() == 0: -## return check_sat() -## abc('trm') - #rpm_result = try_rpm() - set_globals() - N = bmc_depth() - L = n_latches() - I = n_real_inputs() - #try_induction(G_C) - c = max(G_C/5, 1000) - t = max(1,G_T) - print '\n***Running PDR for %d sec'%(t) - abc('&get;,pdr -vt=%f'%(t*.8)) - status = get_status() - if status <= Unsat: - print 'PDR went to %d frames, '%n_bmc_frames(), - print RESULT[status] - return status - if ( ((I+L<250)&(N>100)) or (I+L<200) or (L<51) ): #heuristic that if bmc went deep, then reachability might also - t = max(1,1.5*G_T) - #cmd = 'reach -v -B 1000000 -F 10000 -T %f'%t - #cmd = 'reachx -e %d'%int(long(t)) - #cmd = 'reachx -e %d -t %d'%(int(long(t)),max(10,int(t))) - cmd = 'reachx -t %d'%max(10,int(t)) - print '\n***Running %s'%cmd - abc(cmd) - status = get_status() - if status <= Unsat: - print 'Reachability went to %d frames, '%n_bmc_frames(), - print RESULT[status] - return status - print 'BDD reachability aborted' - return status #temporary - #f = max(100, bmc_depth()) - print '\n***RUNNING interpolation with %d conflicts, %d sec, max 100 frames'%(c,t) - #abc('int -v -F 100 -C %d -T %f'%(c,t)) - abc(',imc -vt=%f '%t) - status = get_status() - if status <= Unsat: - print 'Interpolation went to %d frames, '%n_bmc_frames(), - print RESULT[status] - return status - t = max(1,G_T) - simplify() - if n_latches() == 0: - return check_sat() - print 'Undecided' - return Undecided_reduction - -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 n_ands() == 0: -## return Unsat - abc('orpos;dsat -C %d'%G_C) - if is_sat(): - return Sat_true - elif is_unsat(): - return Unsat - else: - 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.""" - for j in range(K): - i = K-(j+1) - if i == 0: #don't try final verify on original - status = 3 - break - print '\nVerifying backup number %d:'%i, - abc('r %s_backup_%d.aig'%(initial_f_name,i)) - print_circuit_stats() - status = final_verify() - 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: - status = speculate() - if ((status <= Unsat) or (status == Error)): - return status - status = final_verify() - if status == Unsat: - return status - else: - return Undecided_reduction - - -def smp(): - pre_simp() - 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""" -## print "Trying BMC for 2 sec." -## abc("&get; ,bmc -vt=2") -## if is_sat(): -## return Sat_true - set_globals() - if n_latches == 0: - return check_sat() - #print '\n*** Running forward' - try_forward() - #print \n*** Running quick simp' - quick_simp() - #print 'Running_scorr_constr' - status = try_scorr_constr() - #status = 3 - #print 'Running trm' - if ((n_ands() > 0) or (n_latches()>0)): - abc('trm') - print 'Forward, quick_simp, scorr_constr,: ', - print_circuit_stats() - if n_latches() == 0: - return check_sat() - status = process_status(status) - if status <= Unsat: - return status - simplify() - print 'Simplify: ', - print_circuit_stats() - #abc('w temp_simp.aig') - if n_latches() == 0: - return check_sat() - try_phase() - if n_latches() == 0: - return check_sat() - #abc('trm') - if ((n_ands() > 0) or (n_latches()>0)): - abc('trm') - status = process_status(status) - if status <= Unsat: - return status - status = try_scorr_constr() - abc('trm') - 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 process(status): - """Checks if there are no FF and if so checks if the remaining combinational - problem is UNSAT""" - if n_latches() == 0: - return check_sat() - return status - -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""" - n = n_phases() - if ((n == 1) or (n_ands() > 40000)): - return - print 'Number of possible phases = %d'%n - abc('w %s_savetemp.aig'%f_name) - na = n_ands() - nl = n_latches() - ni = n_pis() - no = n_pos() - cost_init = (1*n_pis())+(2*n_latches())+1*n_ands() - cost_min = cost_init - cost = cost_init - abc('w %s_best.aig'%f_name) - for j in range(4): - abc('r %s_savetemp.aig'%f_name) - p = 2**(j+1) - if p > n: - break - abc('phase -F %d'%p) - if na == n_ands(): - break - abc('scl;rw') - if n_latches() > nl: #why would this ever happen - break - #print_circuit_stats() - abc('rw;lcorr;trm') - #print_circuit_stats() - cost = (1*n_pis())+(2*n_latches())+1*n_ands() - if cost < cost_min: - cost_min = cost - abc('w %s_best.aig'%f_name) - else: - break - if cost < cost_init: - abc('r %s_best.aig'%f_name) - simplify() - abc('trm') - print 'Phase abstraction obtained :', - print_circuit_stats() - return - abc('r %s_savetemp.aig'%f_name) - return - -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;rw') - elif na < 80000: - abc('&get;&scl;&put;rw') - -def scorr_constr(): - """Extracts implicit constraints and uses them in signal correspondence - Constraints that are found are folded back when done""" - na = max(1,n_ands()) - if ((na > 40000) or n_pos()>1): - return Undecided_no_reduction - f = 40000/na - f = min(f,16) - n_pos_before = n_pos() - f = 1 #temporary until bug fixed. - abc('w %s_savetemp.aig'%f_name) - if n_ands() < 3000: - cmd = 'unfold -a -F 2' - else: - cmd = 'unfold' - abc(cmd) - if ((n_ands() > na) or (n_pos() == n_pos_before)): - abc('r %s_savetemp.aig'%f_name) - return Undecided_no_reduction - print_circuit_stats() - print 'Number of constraints = %d'%(n_pos() - n_pos_before) - abc('scorr -c -F %d'%f) - abc('fold') - return Undecided_no_reduction - -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 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(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 do not run speculate""" - global x_factor,xfi,f_name - x = time.clock() - max_bmc = -1 - 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() - else: - status = check_sat() - if ((status <= Unsat) or (n_latches() == 0)): - print 'Time for proof = %f sec.'%(time.clock() - x) - return RESULT[status] - if n_ands() == 0: - #abc('bmc3 -T 2') - abc('&get;,bmc -vt=2') - if is_sat(): - return 'SAT' - abc('trm') - write_file('smp') - abc('w %s_backup_%d.aig'%(initial_f_name,K)) - K = K +1 - set_globals() -## if ((n_ands() < 30000) and (a == 1) and (n_latches() < 300)): - if ((n_ands() < 30000) and (n_latches() < 300)): - print '\n***Running quick_verify' - status = quick_verify(0) - if status <= Unsat: - if not status == Unsat: - print 'CEX in frame %d'%cex_frame() - print 'Time for proof = %f sec.'%(time.clock() - x) - return RESULT[status] - if n_ands() == 0: - #abc('bmc3 -T 2') - abc('&get;,bmc -vt=2') - if is_sat(): - return 'SAT' - print'\n***Running abstract' - nl_b = n_latches() - status = abstract() - abc('trm') - write_file('abs') - status = process_status(status) - if ((status <= Unsat) or status == Error): - if status < Unsat: - print 'CEX in frame %d'%cex_frame() -## status = final_verify_recur(K) -## write_file('final') - print 'Time for proof = %f sec.'%(time.clock() - x) - return RESULT[status] - print 'Time for proof = %f sec.'%(time.clock() - x) - return RESULT[status] - abc('w %s_backup_%d.aig'%(initial_f_name,K)) - K = K +1 - if ((n_ands() > 20000) or (a == 1)): - print 'Speculation skipped because either too large or already done' - K = 2 - elif n_ands() == 0: - print 'Speculation skipped because no AND nodes' - K = 2 - else: - print '\n***Running speculate' - status = speculate() - abc('trm') - write_file('spec') - status = process_status(status) - if status == Unsat: - print 'Time for proof = %f sec.'%(time.clock() - x) - return RESULT[status] - if ((status < Unsat) or (status == Error)): - print 'CEX in frame %d'%cex_frame() - K = K-1 #if spec found a true cex, then result of abstract was wrong - else: - abc('w %s_backup_%d.aig'%(initial_f_name,K)) - K = K +1 - status = final_verify_recur(K) - abc('trm') - write_file('final') - print 'Time for proof = %f sec.'%(time.clock() - x) - return RESULT[status] - -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 = time.clock() - #input_x_factor() - init_f_name = f_name - #fast_int(1) - print 'Beginning prove_g_pos' - prove_all_ind() - print 'Number of outputs reduced to %d by induction and fast interpolation'%n_pos() - print '\n************Running second level prove****************\n' - try_rpm() - result = prove(1) # 1 here means do not try speculate. - #result = prove_0_ind() - 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 induction and fast interpolation'%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 - 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() - #fast_int(1) - f_name = f_name + '_%d'%jnext_old - result = prove_1() - if result == 'UNSAT': - if jnext_old > jnext+1: - print '\n******** PROVED OUTPUTS [%d-%d] ******** \n\n'%(jnext+1,jnext_old) - else: - print '\n******** PROVED OUTPUT %d ******** \n\n'%(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 '\n******** UNDECIDED on OUTPUTS %d thru %d ******** \n\n'%(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) - abc('trm') - write_file('group') - result = 'UNDECIDED' - else: - print 'Proved all outputs. The problem is proved UNSAT' - result = 'UNSAT' - print 'Total time for prove_g_pos = %f sec.'%(time.clock() - x) - return result - -def prove_pos(): - """ - 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 = time.clock() - #input_x_factor() - init_f_name = f_name - #fast_int(1) - print 'Beginning prove_pos' - prove_all_ind() - print 'Number of outputs reduced to %d by induction and fast interpolation'%n_pos() - print '\n********** 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 - #count = 0 - 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() - if result == 'UNSAT': - print '\n******** PROVED OUTPUT %d ******** \n\n'%(jnext_old) - pos_proved = pos_proved + range(jnext +1,jnext_old+1) - continue - if result == 'SAT': - print '\n******** DISPROVED OUTPUT %d ******** \n\n'%(jnext_old) - pos_disproved = pos_disproved + range(jnext +1,jnext_old+1) - continue - else: - print '\n******** UNDECIDED on OUTPUT %d ******** \n\n'%(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) - abc('trm') - write_file('group') - result = 'UNRESOLVED' - else: - print 'Proved or disproved all outputs. The problem is proved RESOLVED' - result = 'RESOLVED' - print 'Total time for prove_pos = %f sec.'%(time.clock() - x) - 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 = time.clock() - #input_x_factor() - init_f_name = f_name - #fast_int(1) - print 'Beginning prove_g_pos_split' - prove_all_ind() - print 'Number of outputs reduced to %d by induction and fast interpolation'%n_pos() - try_rpm() - print '\n********** 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 '\n******** PROVED OUTPUTS [%d-%d] ******** \n\n'%(jnext+1,jnext_old) - else: - print '\n******** PROVED OUTPUT %d ******** \n\n'%(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 '\n******** UNDECIDED on OUTPUTS %d thru %d ******** \n\n'%(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) - abc('trm') - 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) - abc('trm') - 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') - -def prove_0_ind(): - """Uses all other outputs as constraints to try to prove output 0 by induction""" - abc('w %s_osavetemp.aig'%f_name) - #ps() - abc('constr -N %d'%(n_pos()-1)) - #ps() - abc('fold') - #ps() - abc('ind -u -C 1000000 -F 20') - status = get_status() - abc('r %s_osavetemp.aig'%f_name) - return status - -def remove(list): - """Removes outputs in list""" - zero(list) - abc('&get;&trim;&put') - #fast_int(1) - -def zero(list): - """Zeros out POs in list""" - for j in list: - run_command('zeropo -N %d'%j) - -def sp(): - """Alias for super_prove""" - print 'Executing super_prove' - result = super_prove() - return result - -def super_prove(): - """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""" - global max_bmc, init_initial_f_name, initial_f_name - init_initial_f_name = initial_f_name - if x_factor > 1: - print 'x_factor = %d'%x_factor - input_x_factor() - max_bmc = -1 - x = time.clock() - print "Trying BMC for 2 sec." - abc("&get; ,bmc -vt=2") - if is_sat(): - print 'Total time taken by super_prove = %f sec.'%(time.clock() - x) - return 'SAT' - result = prove(0) - if ((result[:3] == 'UND') and (n_latches() == 0)): - return result - k = 1 - print result - if not result[:3] == 'UND': - print 'Total time taken by super_prove = %f sec.'%(time.clock() - x) - return result - if n_pos() > 1: - result = prove_g_pos(0) - print result - if result == 'UNSAT': - print 'Total time taken by super_prove = %f sec.'%(time.clock() - x) - return result - if result == 'SAT': - k = 0 #Don't try to prove UNSAT on an abstraction that had SAT - # should go back to backup 1 since probably spec was bad. - y = time.clock() - result = BMC_VER_result(k) - print 'Total time taken by last gasp verification = %f sec.'%(time.clock() - y) - print 'Total time for %s = %f sec.'%(init_initial_f_name,(time.clock() - x)) - return result - -def reachm(t): - x = time.clock() - run_command('&get;&reach -vcs -T %d;&put'%t) - print 'Time = %f'%(time.clock() - x) - -def reachx(t): - x = time.clock() - run_command('reachx -t %d'%t) - print 'Time = %f'%(time.clock() - x) - -def BMC_VER_result(n): - global init_initial_f_name - #print init_initial_f_name - xt = time.clock() - result = 5 - T = 150 - if n == 0: - abc('r %s_smp.aig'%init_initial_f_name) - print '\n***Running proof on initial simplified circuit\n', - ps() - else: - print '\n***Running proof on final unproved circuit' - ps() - print ' Running PDR for %d sec'%T - abc('&get;,pdr -vt=%d'%(T*.8)) - result = get_status() - if result == Unsat: - return 'UNSAT' - if result > Unsat: #still undefined - if (n_pis()+n_latches() < 250): - print ' Running Reachability for 150 sec.' - abc('reachx -t 150') - #run_command('&get;&reach -vcs -T %d'%T) - result = get_status() - if result == Unsat: - return 'UNSAT' - if ((result > Unsat) and n ==1): - print ' Running interpolation for %f sec.'%T - abc(',imc -vt=%f'%T) - result = get_status() - if result == Unsat: - return 'UNSAT' - # if n=1 we are trying to prove result on abstracted circuit. If still undefined, then probably does - # not make sense to try pdr, reach, int on original simplified circuit, only BMC here. - if n == 1: - abc('r %s_smp.aig'%init_initial_f_name) #check if the initial circuit was SAT - #print 'Reading %s_smp'%init_initial_f_name, - #run_command('bmc3 -v -T %d -F 200000 -C 1000000'%T) - print '***Running BMC on initial simplified circuit' - ps() - print '\n' - abc('&get;,bmc -vt=%f'%T) - result = get_status() - if result < Unsat: - result = 'SAT' - print ' CEX found in frame %d'%cex_frame() - else: - result = 'UNDECIDED' - print 'Additional time taken by BMC/PDR/Reach = %f sec.'%(time.clock() - xt) - return result - -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. """ - 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('r %s_osavetemp.aig'%f_name) - 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 -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_all_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('r %s_osavetemp.aig'%f_name) - abc('cone -O %d -s'%j) - abc('scl') - 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 remove_0_pos(): - abc('&get; &trim; &put') - - -def prove_all_ind2(): - """Tries to prove output k by induction, using outputs > k as constraints. Removes proved outputs from POs.""" - abc('w %s_osavetemp.aig'%f_name) - plist = [] - list = range(n_pos()) -## if r == 1: -## list.reverse() - for j in list: - abc('r %s_osavetemp.aig'%f_name) - extract(j,n_pos()) - 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 -u -C 10000 -F %d'%f) - status = get_status() - if status == Unsat: - plist = plist + [j] - print '-', -## else: -## status = pdr(1) -## if status == Unsat: -## print '+', -## plist = plist + [j] - print '%d'%j, - print '\nOutputs proved = ', - print plist - abc('r %s_osavetemp.aig'%f_name) - remove(plist) #remove the outputs proved -## #the following did not work because abc command constr, allows only last set of outputs to be constraints -## abc('w %s_osavetemp.aig'%f_name) -## plist = [] -## list = range(n_pos()) -## list.reverse() -## for j in list: -## abc('r %s_osavetemp.aig'%f_name) -## extract(j,n_pos()) -## 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 -u -C 10000 -F %d'%f) -## status = get_status() -## if status == Unsat: -## plist = plist + [j] -## print '-', -#### else: -#### status = pdr(1) -#### if status == Unsat: -#### print '+', -#### plist = plist + [j] -## print '%d'%j, -## print '\nOutputs proved = ', -## print plist.reverse -## abc('r %s_osavetemp.aig'%f_name) -## remove(plist) #remove the outputs proved -## return status - -def pdr(t): - abc('&get; ,pdr -vt=%f'%t) - result = get_status() - -def split(n): - abc('orpos;&get') - abc('&posplit -v -N %d;&put;dc2;trm'%n) - -def keep_splitting(): - for j in range(5): - split(5+j) - no = n_pos() - status = prove_g_pos_split(0) - if status <= Unsat: - return status - if no == n_pos(): - return Undecided - -def drill(n): - run_command('&get; &reach -vcs -H 5 -S %d -T 50 -C 40'%n) - -def prove_1(): - """Proves all the outputs together. If ever an abstraction was done then if SAT is returned, - we make RESULT return "undecided". - """ - a = 1 - global x_factor,xfi,f_name - x = time.clock() - max_bmc = -1 - K = 0 - print 'Initial: ', - print_circuit_stats() - x_factor = xfi - print 'x_factor = %f'%x_factor - print '\n***Running pre_simp' - set_globals() - status = pre_simp() - if ((status <= Unsat) or (n_latches == 0)): - print 'Time for proof = %f sec.'%(time.clock() - x) - return RESULT[status] - abc('trm') - write_file('smp') - abc('w %s_backup_%d.aig'%(initial_f_name,K)) - K = K +1 - set_globals() - if ((n_ands() < 30000) and (a == 1) and (n_latches() < 300)): - print '\n***Running quick_verify' - status = quick_verify(0) - if status <= Unsat: - if not status == Unsat: - print 'CEX in frame %d'%cex_frame() - print 'Time for proof = %f sec.'%(time.clock() - x) - return RESULT[status] - print'\n***Running abstract' - nl_b = n_latches() - status = abstract() - abc('trm') - write_file('abs') - status = process_status(status) - if ((status <= Unsat) or status == Error): - if status < Unsat: - print 'CEX in frame %d'%cex_frame() - print 'Time for proof = %f sec.'%(time.clock() - x) - return RESULT[status] - print 'Time for proof = %f sec.'%(time.clock() - x) - return RESULT[status] - abc('w %s_backup_%d.aig'%(initial_f_name,K)) - status = final_verify_recur(2) - abc('trm') - write_file('final') - print 'Time for proof = %f sec.'%(time.clock() - x) - return RESULT[status] - -def qprove(): - global x_factor - x = time.clock() - x_factor = 3 - print '\n*********pre_simp**********\n' - pre_simp() - print '\n*********absv**********\n' - result = absv(3,1) - x_factor = 2 - print '\n*********absv**********\n' - result = absv(3,1) - print '\n*********speculate**********\n' - result = speculate() - if result <= Unsat: - return RESULT[result] - print '\n*********absv**********\n' - result = absv(3,1) - print '\n*********prove_pos**********\n' - result = prove_pos() - if result == 'UNDECIDED': - print '\n*********BMC_VER_result**********\n' - result = BMC_VER_result(1) - print 'Time for proof = %f sec.'%(time.clock() - x) - return result - -def pre_reduce(): - x = time.clock() - pre_simp() - write_file('smp') - abstract() - write_file('abs') - print 'Time = %f'%(time.clock() - x) - - -#PARALLEL FUNCTIONS -""" funcs should look like -funcs = [defer(abc)('&get;,bmc -vt=50;&put'),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 fork 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 fork(funcs): - """ runs funcs in parallel""" - for i,res in pyabc_split.abc_split_all(funcs): - status = prob_status() - if not status == -1: - print i,status - ps() - break - else: - print i,status - ps() - continue - return status - -def handler_s(res): - """ This serial handler returns True if the problem is solved by the first returning function, - in which case, the problem is replaced by the new aig and status. - """ - if not res == -1: - #replace_prob() - print ('UNSAT','SAT')[res] - return True - else: - return False - |