Skip to content

A
abc
Commit 89ac9abe by Baruch Sterin
Options

pyabc: updated Bob's scripts

parent 15d0d84b
Showing with 855 additions and 395 deletions
scripts/abc.rc
python new_abc_commands.py
python reachx_cmd.py
#python C:\Research\ABC\AIG\Python\reachx_cmd.py
load_plugin bip "Bip"
# global parameters
set check # checks intermediate networks
#set checkfio # prints warnings when fanins/fanouts are duplicated
set checkread # checks new networks after reading from file
set backup # saves backup networks retrived by "undo" and "recall"
set savesteps 1 # sets the maximum number of backup networks to save
set progressbar # display the progress bar
#set checkread # checks new networks after reading from file
#set backup # saves backup networks retrived by "undo" and "recall"
#set savesteps 1 # sets the maximum number of backup networks to save
#set progressbar # display the progress bar
# program names for internal calls
set dotwin dot.exe
......@@ -25,6 +26,10 @@ set gnuplotwin wgnuplot.exe
set gnuplotunix gnuplot
# standard aliases
alias srw "b; rw; b"
alias fix "ps; st; ps; srw; ps; plat; cycle -x -F 1; plat; logic; undc; st; zero; ps; scorr; ps"
alias fixp "st; srw; cycle -x -F 1; logic; undc; st; zero "
alias b balance
alias cl cleanup
alias clp collapse
......@@ -67,8 +72,8 @@ alias rvl read_verlib
alias rsup read_super mcnc5_old.super
alias rlib read_library
alias rlibc read_library cadence.genlib
alias rw rewrite
alias rwz rewrite -z
alias rw drw
alias rwz drw -z
alias rf refactor
alias rfz refactor -z
alias re restructure
......@@ -98,18 +103,18 @@ alias wv write_verilog
# standard scripts
alias share "b; multi; fx; b"
alias resyn "b; rw; rwz; b; rwz; b"
alias resyn2 "b; rw; rf; b; rw; rwz; b; rfz; rwz; b"
alias resyn2a "b; rw; b; rw; rwz; b; rwz; b"
alias resyn "b; drw; rwz; b; rwz; b"
alias resyn2 "b; drw; rf; b; drw; rwz; b; rfz; rwz; b"
alias resyn2a "b; drw; b; drw; rwz; b; rwz; b"
alias resyn3 "b; rs; rs -K 6; b; rsz; rsz -K 6; b; rsz -K 5; b"
alias compress "b -l; rw -l; rwz -l; b -l; rwz -l; b -l"
alias compress "b -l; drw -l; rwz -l; b -l; rwz -l; b -l"
alias compress2 "b -l; rw -l; rf -l; b -l; rw -l; rwz -l; b -l; rfz -l; rwz -l; b -l"
alias compress2 "b -l; drw -l; rf -l; b -l; drw -l; rwz -l; b -l; rfz -l; rwz -l; b -l"
alias choice "fraig_store; resyn; fraig_store; resyn2; fraig_store; fraig_restore"
alias choice2 "fraig_store; balance; fraig_store; resyn; fraig_store; resyn2; fraig_store; resyn2; fraig_store; fraig_restore"
alias rwsat "st; rw -l; b -l; rw -l; rf -l"
alias rwsat2 "st; rw -l; b -l; rw -l; rf -l; fraig; rw -l; b -l; rw -l; rf -l"
alias shake "st; ps; sat -C 5000; rw -l; ps; sat -C 5000; b -l; rf -l; ps; sat -C 5000; rfz -l; ps; sat -C 5000; rwz -l; ps; sat -C 5000; rfz -l; ps; sat -C 5000"
alias rwsat "st; drw -l; b -l; drw -l; rf -l"
alias rwsat2 "st; drw -l; b -l; drw -l; rf -l; fraig; drw -l; b -l; drw -l; rf -l"
alias shake "st; ps; sat -C 5000; drw -l; ps; sat -C 5000; b -l; rf -l; ps; sat -C 5000; rfz -l; ps; sat -C 5000; rwz -l; ps; sat -C 5000; rfz -l; ps; sat -C 5000"
alias snap fraig_store
alias unsnap fraig_restore
......@@ -126,24 +131,24 @@ alias icb "ic -M 2 -B 10 -s"
alias cs "care_set "
# resubstitution scripts for the IWLS paper
alias src_rw "st; rw -l; rwz -l; rwz -l"
alias src_rw "st; drw -l; rwz -l; rwz -l"
alias src_rs "st; rs -K 6 -N 2 -l; rs -K 9 -N 2 -l; rs -K 12 -N 2 -l"
alias src_rws "st; rw -l; rs -K 6 -N 2 -l; rwz -l; rs -K 9 -N 2 -l; rwz -l; rs -K 12 -N 2 -l"
alias resyn2rs "b; rs -K 6; rw; rs -K 6 -N 2; rf; rs -K 8; b; rs -K 8 -N 2; rw; rs -K 10; rwz; rs -K 10 -N 2; b; rs -K 12; rfz; rs -K 12 -N 2; rwz; b"
alias compress2rs "b -l; rs -K 6 -l; rw -l; rs -K 6 -N 2 -l; rf -l; rs -K 8 -l; b -l; rs -K 8 -N 2 -l; rw -l; rs -K 10 -l; rwz -l; rs -K 10 -N 2 -l; b -l; rs -K 12 -l; rfz -l; rs -K 12 -N 2 -l; rwz -l; b -l"
alias src_rws "st; drw -l; rs -K 6 -N 2 -l; rwz -l; rs -K 9 -N 2 -l; rwz -l; rs -K 12 -N 2 -l"
alias resyn2rs "b; rs -K 6; drw; rs -K 6 -N 2; rf; rs -K 8; b; rs -K 8 -N 2; drw; rs -K 10; rwz; rs -K 10 -N 2; b; rs -K 12; rfz; rs -K 12 -N 2; rwz; b"
alias compress2rs "b -l; rs -K 6 -l; drw -l; rs -K 6 -N 2 -l; rf -l; rs -K 8 -l; b -l; rs -K 8 -N 2 -l; drw -l; rs -K 10 -l; rwz -l; rs -K 10 -N 2 -l; b -l; rs -K 12 -l; rfz -l; rs -K 12 -N 2 -l; rwz -l; b -l"
alias c2 "ua; compress2rs; sa"
alias ic "indcut -v"
alias lp "lutpack"
alias c "ua; compress; sa"
alias c1 "ua; compress;b -l; rs -K 6 -l; rw -l; rs -K 6 -N 2 -l; rf -l; rs -K 8 -l; b -l; sa"
alias c1 "ua; compress;b -l; rs -K 6 -l; drw -l; rs -K 6 -N 2 -l; rf -l; rs -K 8 -l; b -l; sa"
alias dr dretime
alias ds dsec -v
alias dp dprove -v
# experimental implementation of don't-cares
alias resyn2rsdc "b; rs -K 6 -F 2; rw; rs -K 6 -N 2 -F 2; rf; rs -K 8 -F 2; b; rs -K 8 -N 2 -F 2; rw; rs -K 10 -F 2; rwz; rs -K 10 -N 2 -F 2; b; rs -K 12 -F 2; rfz; rs -K 12 -N 2 -F 2; rwz; b"
alias compress2rsdc "b -l; rs -K 6 -F 2 -l; rw -l; rs -K 6 -N 2 -F 2 -l; rf -l; rs -K 8 -F 2 -l; b -l; rs -K 8 -N 2 -F 2 -l; rw -l; rs -K 10 -F 2 -l; rwz -l; rs -K 10 -N 2 -F 2 -l; b -l; rs -K 12 -F 2 -l; rfz -l; rs -K 12 -N 2 -F 2 -l; rwz -l; b -l"
alias resyn2rsdc "b; rs -K 6 -F 2; drw; rs -K 6 -N 2 -F 2; rf; rs -K 8 -F 2; b; rs -K 8 -N 2 -F 2; drw; rs -K 10 -F 2; rwz; rs -K 10 -N 2 -F 2; b; rs -K 12 -F 2; rfz; rs -K 12 -N 2 -F 2; rwz; b"
alias compress2rsdc "b -l; rs -K 6 -F 2 -l; drw -l; rs -K 6 -N 2 -F 2 -l; rf -l; rs -K 8 -F 2 -l; b -l; rs -K 8 -N 2 -F 2 -l; drw -l; rs -K 10 -F 2 -l; rwz -l; rs -K 10 -N 2 -F 2 -l; b -l; rs -K 12 -F 2 -l; rfz -l; rs -K 12 -N 2 -F 2 -l; rwz -l; b -l"
# minimizing for FF literals
alias fflitmin "compress2rs; ren; sop; ps -f"
......@@ -222,9 +227,10 @@ alias lcr "&get; &lcorr; &put"
alias trm "logic;trim;st;ps"
alias smp "ua;ps;scl;ps;rw;dr;lcorr;rw;dr;ps;scorr;ps;fraig;ps;dc2;dr;scorr -F 2;ps;dc2rs;w temp.aig"
alias smp1 "ua;ps;scl;ps;rw;dr;lcorr;rw;dr;ps;scorr;ps;fraig;ps;dc2;dr;ps;dc2rs;w temp.aig"
alias smpf "ua;ps;scl;lcr;ps;rw;dr;ps;scr;ps;dc2;&get;&scorr -F 2;&put;dr;ps;dc2;ps;w temp.aig"
alias smp "ua;ps;scl;ps;drw;dr;lcorr;drw;dr;ps;scorr;ps;fraig;ps;dc2;dr;scorr -F 2;ps;dc2rs;w temp.aig"
alias smp1 "scl;drw;dr;lcorr;drw;dr;scorr;fraig;dc2rs"
alias smp2 "ua;ps;scl;ps;drw;dr;lcorr;drw;dr;ps;scorr;ps;fraig;ps;dc2;dr;ps;dc2rs;w temp.aig"
alias smpf "ua;ps;scl;lcr;ps;drw;dr;ps;scr;ps;dc2;&get;&scorr -F 2;&put;dr;ps;dc2;ps;w temp.aig"
alias &smp "ua;&get;&ps;&scl;&ps;&dc2;&put;dr;&get;&lcorr;&dc2;&put;dr;&get;&ps;&scorr;&ps;&fraig;&ps;&dc2;&put;dr;&get;&scorr -F 2;&ps;&dc2;&put;w temp.aig"
......@@ -233,7 +239,7 @@ alias smplite '&get;&scl;&dc2;&put;dr;&get;&lcorr;&dc2;&put;dr;&get;&scorr;&dc2;
alias &smp1 "ua;&get;&ps;&scl;&ps;&dc2;&put;dr;&get;&lcorr;&dc2;&put;dr;&get;&ps;&scorr;&ps;&fraig;&ps;&dc2;&put;dr;&get;&ps;&dc2;&put;w temp.aig"
alias &smpf "ua;ps;rw;&get;&ps;&scl;&ps;&put;dr;&get;&ps;&lcorr;&ps;&dc2;&ps;&scorr;&ps;&put;rw;ps;w temp.aig"
alias &smpf "ua;ps;drw;&get;&ps;&scl;&ps;&put;dr;&get;&ps;&lcorr;&ps;&dc2;&ps;&scorr;&ps;&put;drw;ps;w temp.aig"
#for each output separately
alias simpk "dprove -vrcbkmiu -B 10 -D 1000"
......@@ -323,7 +329,12 @@ alias %scr "%get;%st;%scorr;%put;st"
alias sc "fold;w tempc.aig;unfold -s"
alias uc "r tempc.aig;unfold -s"
alias smpc "scl;rw;ps;scorr -c;ps;fraig;ps;compress2rs;ps"
alias smpc "scl;drw;ps;scorr -c;ps;fraig;ps;compress2rs;ps"
alias abseen "&get;,abs -vt=60 -timeout=60 -bob=10 -aig=temp.aig;r temp.aig"
alias pdreen "&get;,pdr -vt=60"
alias inteen "&get;,imc -vt=60"
alias bmceen "&get;,bmc -vt=60"
......
scripts/abc_common.py
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
"""
......@@ -40,7 +44,7 @@ stackno_gabs = stackno_gore = stackno_greg= 0
STATUS_UNKNOWN = -1
STATUS_SAT = 0
STATUS_UNSAT = 1
RESULT = ('SAT' , 'SAT', 'UNSAT', 'UNDECIDED but reduced', 'UNDECIDED, no reduction', 'UNDCIDED but reduced' )
RESULT = ('SAT' , 'SAT', 'UNSAT', 'UNDECIDED', 'UNDECIDED,', 'UNDCIDED' )
Sat_reg = 0
Sat_true = 1
Unsat = 2
......@@ -190,29 +194,6 @@ def read_file():
def rf():
read_file()
##def read_file():
## """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
## x_factor = 1
## max_bmc = -1
## print 'Type in the name of the aig file to be read in'
## s = raw_input()
## if s[-4:] == '.aig':
## f_name = s[:-4]
## else:
## f_name = s
## s = s+'.aig'
## run_command(s)
## initial_f_name = f_name
## print_circuit_stats()
##
##def rf():
## """just an alias for read_file"""
## read_file()
def write_file(s):
"""this is the main method for writing the current circuit to an AIG file on disk.
......@@ -236,7 +217,7 @@ def wf():
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 abstract ones, for which it is known that there is not cex out to that depth."""
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)
......@@ -301,43 +282,7 @@ def rc(file):
"""reads <file> so that if constraints are explicit, it will preserve them"""
abc('&r %s;&put'%file)
##def push(file):
## """ saves <file>.aig in stack_x"""
## global stackno_gabs, stackno_gsrm, stackno_greg
## if 'gabs' in file:
## snm = 'gabs'
## elif 'gsrm' in file:
## snm = 'gsrm'
## elif 'x' in file:
## snm = 'greg'
## else:
## print 'wrong file name'
## return
## print snm
## sn = 'stackno_%s'%snm
## print sn
## exec 'sn += sn'
## print sn, eval(sn)
## run_command("r %s.aig"%file)
## run_command("w %s_%d.aig"%(file,eval(sn)))
##
##def pop(file):
## """ reads top <file>.aig in stack_1 and saves it in <file>.aig"""
## global stackno_gabs, stackno_gsrm, stackno_greg
## if 'gabs' in file:
## sn = 'gabs'
## if 'gsrm' in file:
## sn = 'gsrm'
## if 'x' in file:
## sn = 'greg'
## else:
## print 'wrong file name'
## return
## run_command("r %s_%d.aig"%(file,eval(sn)))
## run_command("w %s.aig"%file)
## os.remove("%s_%d.aig"%(file,eval(sn)))
## exec 'sn = sn-1'
## # need to protect against wrong stack count
def fast_int(n):
"""This is used to eliminate easy-to-prove outputs. Arg n is conflict limit to be used
......@@ -382,10 +327,10 @@ def simplify():
# set_globals()
## print 'simplify initial ',
## ps()
abc('w t.aig')
#abc('w t.aig')
n=n_ands()
abc('scl')
if n > 30000:
if n > 40000:
abc('&get;&scl;&put')
n = n_ands()
if n < 100000:
......@@ -393,7 +338,7 @@ def simplify():
run_command('ps')
print '.',
n = n_ands()
if n<45000:
if n<60000:
abc("&get;&scorr -F 2;&put;dc2rs")
print '.',
#ps()
......@@ -403,28 +348,34 @@ def simplify():
#ps()
n = n_ands()
n = n_ands()
if n <= 30000:
if n <= 40000:
print '.',
#ps()
if n > 15000:
if n > 30000:
abc("dc2rs")
print '.',
else:
abc("scorr -F 2;dc2rs")
print '.',
#ps()
## else:
## abc("scorr -F 2;dc2rs")
## print '.',
## ps()
n = max(1,n_ands())
ps()
if n < 20000:
#ps()
if n < 30000:
abc('scl;rw;dr;lcorr;rw;dr')
m = int(min( 60000/n, 16))
#print 'm = %d'%m
if m >= 4:
j = 4
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 check_size() == 1:
#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()
......@@ -464,6 +415,25 @@ def iterate_simulation(latches_before):
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"""
......@@ -472,8 +442,7 @@ def iterate_abstraction_refinement(latches_before,NBF):
F = 2000
else:
F = 2*NBF
print '\nIterating BMC or BDD reachability'
reach_sw = 0
print '\nIterating BMC/PDR'
always_reach = 0
cexf = 0
reach_failed = 0
......@@ -490,36 +459,47 @@ def iterate_abstraction_refinement(latches_before,NBF):
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 (reach_sw ==1)) and not reach_failed)):
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))
reach_sw = 1
#cmd = 'reachx -t %d'%max(10,int(t))
cmd = '&get;,pdr -vt=%f'%t
else:
reach_sw = 0
cmd = 'bmc3 -C %d -T %f -F %d'%(G_C,t,F)
print 'RUNNING %s'%cmd
#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 'Reachability went to %d frames, '%n_bmc_frames()
#print 'Depth reached %d frames, '%n_bmc_frames()
print 'UNSAT'
return Unsat
cexf = cex_frame()
set_max_bmc(cexf -1)
if ((not is_sat()) and (reach_sw == 1)):
#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():
set_max_bmc(cex_frame()-1)
#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()
if reach_sw == 0:
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
......@@ -543,29 +523,18 @@ def abstract():
print 'Start: ',
print_circuit_stats()
c = 1.5*G_C
#c = 20000
t = max(1,1.25*G_T)
method = 3
if n_ands() > 100000:
method = 0
#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
if max_bmc == -1:
time = max(1,.01*G_T)
abc('bmc3 -C %d -T %f -F 165'%(.01*G_C, time))
set_max_bmc(bmc_depth())
f = min(250,1.5*max_bmc)
f = max(20, f)
f = 10*f
if not method == 0:
b = 10
b = max(b,max_bmc+2)
b = b*2**(x_factor-1)
b = 2*b
print 'Neen abstraction params: Bob = %d, Method #%d, %d conflicts, %d stable, %d sec., %d frames'%(b,method,c/3,s,t,f)
abc('&get; &abs_newstart -v -B %f -A %d -C %d -S %d -V %f -F %d'%(b,method,c/3,s,t,f))
else:
abc('&get;&abs_start -v -C 500000 -R 1')
#abc('w abstemp.aig')
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
......@@ -573,8 +542,8 @@ def abstract():
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()
## print 'First abstraction: ',
## print_circuit_stats()
latches_after = n_latches()
#if latches_before_abs == latches_after:
if latches_after >= .98*latches_before_abs:
......@@ -583,7 +552,7 @@ def abstract():
return Undecided_no_reduction
# refinement loop
if (n_ands() + n_latches() + n_pis()) < 15000:
print 'Running simulation iteratively'
print '\n***Running simulation iteratively'
for i in range(5):
result = iterate_simulation(latches_before_abs)
if result == Restart:
......@@ -610,7 +579,8 @@ def absv(n,v):
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('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)
......@@ -648,7 +618,7 @@ def spec():
set_globals()
t = max(1,.5*G_T)
r = max(1,int(t))
print 'Running &equiv2 with C = %d, T = %f sec., F = %d -S 1 -R %d'%(G_C,t,200,r)
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()
......@@ -723,11 +693,13 @@ def speculate():
set_globals()
t = max(1,.5*G_T)
r = max(1,int(t))
print '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('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()
#print 'Speculation good to %d frames'%n_bmc_frames()
#simplify()
if n_pos_before == n_pos():
print 'No new outputs. Quitting speculate'
......@@ -735,6 +707,12 @@ def speculate():
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:
......@@ -746,7 +724,7 @@ def speculate():
elif k < 120000:
n = 8
if n > 0: # simulation can run out of memory for too large designs, so be careful
print 'RUNNING simulation iteratively'
print '\n***RUNNING simulation iteratively'
for i in range(5):
result = run_simulation(n)
if result == Sat_true:
......@@ -757,6 +735,7 @@ def speculate():
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()
......@@ -788,7 +767,8 @@ def speculate():
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():
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'
......@@ -800,11 +780,13 @@ def speculate():
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)))
if (((reach_allowed or (reach_sw == 1)) and not reach_failed)):
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))
reach_sw = 1
#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:
......@@ -812,16 +794,19 @@ def speculate():
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)
reach_sw = 0
print 'Running %s'%cmd
#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)
#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[:3] == 'bmc')):
print 'BMC found true cex: Output = %d, Frame = %d'%(cex_po(),cex_frame())
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
......@@ -829,14 +814,16 @@ def speculate():
return Undecided_no_reduction
continue
else:
set_max_bmc(bmc_depth())
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 reach_sw == 0:
if bmc:
break
elif max_bmc > 1.2*last_bmc:
break
else:
if prob_status() == 1:
print 'Reachability converged in %d frames'%n_bmc_frames()
return Unsat
reach_failed = 1
init = 1
continue
......@@ -880,28 +867,39 @@ def quick_verify(n):
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()
if is_sat():
return Sat_true
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))
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
N = bmc_depth()
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
print ' Running %s'%cmd
abc(cmd)
status = get_status()
if status <= Unsat:
......@@ -944,7 +942,8 @@ def try_rpm():
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('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:
......@@ -970,13 +969,22 @@ def final_verify():
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 'Running %s'%cmd
print '\n***Running %s'%cmd
abc(cmd)
status = get_status()
if status <= Unsat:
......@@ -984,16 +992,17 @@ def final_verify():
print RESULT[status]
return status
print 'BDD reachability aborted'
#f = max(100,bmc_depth())
c = max(G_C/5, 1000)
t = max(1,G_T)
print '\nRUNNING interpolation with %d conflicts, %d sec, max 100 frames'%(c,t)
abc('int -v -F 100 -C %d -T %f'%(c,t))
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()
......@@ -1005,7 +1014,7 @@ def check_sat():
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('dsat -C %d'%G_C)
abc('orpos;dsat -C %d'%G_C)
if is_sat():
return Sat_true
elif is_unsat():
......@@ -1026,7 +1035,7 @@ 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 '\nTrying induction'
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)
......@@ -1055,11 +1064,11 @@ def final_verify_recur(K):
if status >= Unsat:
return status
if i > 0:
print 'SAT returned, trying less abstract backup'
print 'SAT returned, Running less abstract backup'
continue
break
if ((i == 0) and (status > Unsat) and (n_ands() > 0)):
print '\nTrying speculate on initial backup number %d:'%i,
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:
......@@ -1073,29 +1082,42 @@ def final_verify_recur(K):
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()
#print 'trying forward'
if n_latches == 0:
return check_sat()
#print '\n*** Running forward'
try_forward()
#print 'trying quick simp'
#print \n*** Running quick simp'
quick_simp()
#print 'trying_scorr_constr'
#print 'Running_scorr_constr'
status = try_scorr_constr()
#status = 3
#print 'trying trm'
#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()
......@@ -1132,7 +1154,7 @@ def try_phase():
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() > 30000)):
if ((n == 1) or (n_ands() > 40000)):
return
print 'Number of possible phases = %d'%n
abc('w %s_savetemp.aig'%f_name)
......@@ -1140,7 +1162,7 @@ def try_phase():
nl = n_latches()
ni = n_pis()
no = n_pos()
cost_init = (1*n_pis())+(2*n_latches())+.05*n_ands()
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)
......@@ -1158,7 +1180,7 @@ def try_phase():
#print_circuit_stats()
abc('rw;lcorr;trm')
#print_circuit_stats()
cost = (1*n_pis())+(2*n_latches())+.05*n_ands()
cost = (1*n_pis())+(2*n_latches())+1*n_ands()
if cost < cost_min:
cost_min = cost
abc('w %s_best.aig'%f_name)
......@@ -1207,7 +1229,6 @@ def quick_simp():
abc('&get;&scl;&put;rw')
def scorr_constr():
#return Undecided_no_reduction #temporarily disable the for the moment
"""Extracts implicit constraints and uses them in signal correspondence
Constraints that are found are folded back when done"""
na = max(1,n_ands())
......@@ -1223,18 +1244,13 @@ def scorr_constr():
else:
cmd = 'unfold'
abc(cmd)
if ((n_ands() > na) or (n_pos() == 1)):
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 %dd'%f)
if n_pos_before == 1:
#abc('cone -s -O 0') #don't fold constraints back in
abc('fold')
else:
abc('fold')
## abc('fold')
abc('scorr -c -F %d'%f)
abc('fold')
return Undecided_no_reduction
def process_status(status):
......@@ -1253,7 +1269,7 @@ def input_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 = 0 we skip the first quick_verify"""
If a == 1 do not run speculate"""
global x_factor,xfi,f_name
x = time.clock()
max_bmc = -1
......@@ -1262,14 +1278,18 @@ def prove(a):
print_circuit_stats()
x_factor = xfi
print 'x_factor = %f'%x_factor
print '\nRunning pre_simp'
print '\n***Running pre_simp'
set_globals()
status = pre_simp()
if status <= Unsat:
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('bmc3 -T 2')
abc('&get;,bmc -vt=2')
if is_sat():
return 'SAT'
abc('trm')
......@@ -1277,8 +1297,9 @@ def prove(a):
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 '\nRunning quick_verify'
## 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:
......@@ -1286,10 +1307,11 @@ def prove(a):
print 'Time for proof = %f sec.'%(time.clock() - x)
return RESULT[status]
if n_ands() == 0:
abc('bmc3 -T 2')
#abc('bmc3 -T 2')
abc('&get;,bmc -vt=2')
if is_sat():
return 'SAT'
print'\nRunning abstract'
print'\n***Running abstract'
nl_b = n_latches()
status = abstract()
abc('trm')
......@@ -1306,27 +1328,14 @@ def prove(a):
return RESULT[status]
abc('w %s_backup_%d.aig'%(initial_f_name,K))
K = K +1
if status == Undecided_reduction:
print '\nRunning quick_verify'
status = quick_verify(1)
status = process_status(status)
if status <= Unsat:
if status < Unsat:
print 'CEX in frame %d'%cex_frame()
#print 'Time for proof = %f sec.'%(time.clock() - x)
status = final_verify_recur(K-1)
abc('trm')
write_file('final')
print 'Time for proof = %f sec.'%(time.clock() - x)
return RESULT[status]
if n_ands() > 20000:
print 'Speculation skipped because too large'
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'
print 'Speculation skipped because no AND nodes'
K = 2
else:
print '\nRunning speculate'
print '\n***Running speculate'
status = speculate()
abc('trm')
write_file('spec')
......@@ -1359,11 +1368,11 @@ def prove_g_pos(a):
init_f_name = f_name
#fast_int(1)
print 'Beginning prove_g_pos'
result = prove_all_ind()
prove_all_ind()
print 'Number of outputs reduced to %d by induction and fast interpolation'%n_pos()
print '\n************Trying second level prove****************\n'
print '\n************Running second level prove****************\n'
try_rpm()
result = prove(0)
result = prove(1) # 1 here means do not try speculate.
#result = prove_0_ind()
if result == 'UNSAT':
print 'Second prove returned UNSAT'
......@@ -1372,7 +1381,7 @@ def prove_g_pos(a):
print 'CEX found'
return result
print '\n********** Proving each output separately ************'
result = prove_all_ind()
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)
......@@ -1428,20 +1437,16 @@ def prove_g_pos(a):
return result
def prove_pos():
"""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
a=0
x = time.clock()
#input_x_factor()
init_f_name = f_name
#fast_int(1)
print 'Beginning prove_g_pos'
result = prove_all_ind()
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
......@@ -1450,6 +1455,7 @@ def prove_pos():
print 'Number of outputs = %d'%n
#count = 0
pos_proved = []
pos_disproved = []
J = 0
jnext = n-1
while jnext >= 0:
......@@ -1458,43 +1464,36 @@ def prove_pos():
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)
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)
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
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 OUTPUTS %d thru %d ******** \n\n'%(jnext+1,jnext_old)
print '\n******** UNDECIDED on OUTPUT %d ******** \n\n'%(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)
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 = 'UNDECIDED'
result = 'UNRESOLVED'
else:
print 'Proved all outputs. The problem is proved UNSAT'
result = 'UNSAT'
print 'Total time for prove_g_pos = %f sec.'%(time.clock() - x)
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
......@@ -1506,7 +1505,7 @@ def prove_g_pos_split():
init_f_name = f_name
#fast_int(1)
print 'Beginning prove_g_pos_split'
result = prove_all_ind()
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 ************'
......@@ -1575,7 +1574,7 @@ def group(a,n):
for J in range(1,n+1):
abc('r %s_osavetemp.aig'%f_name)
j = n-J
#print 'trying %d to %d'%(j,n)
#print 'Running %d to %d'%(j,n)
extract(j,n)
#print 'n_latches = %d'%n_latches()
#if n_latches() >= nli + (nlt - nli)/2:
......@@ -1613,10 +1612,10 @@ def prove_0_ind():
return status
def remove(list):
"""Removes outputs in list as well as easy output proved by fast interpolation"""
"""Removes outputs in list"""
zero(list)
abc('scl')
fast_int(1)
abc('&get;&trim;&put')
#fast_int(1)
def zero(list):
"""Zeros out POs in list"""
......@@ -1640,7 +1639,14 @@ def super_prove():
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':
......@@ -1662,60 +1668,64 @@ def super_prove():
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
if n == 0:
print '\nTrying proof on initial simplified and abstracted circuit\n'
abc('r %s_smp.abs.aig'%init_initial_f_name)
ps()
x = time.clock()
xt = time.clock()
result = 5
N = 0
T = 150
if (n_pis()+n_latches() < 250):
print ' Trying deep Reachability'
run_command('reachx -t 150')
#run_command('&get;&reach -vcs -T %d'%T)
result = get_status()
if result == Unsat:
return 'UNSAT'
if ((result < Unsat) and (n == 0)):
N = 1
if ((result >= Unsat) and (N == 0)):
print 'Trying deep interpolation'
run_command('int -v -F 30000 -C 1000000 -T %d'%T)
result = get_status()
if result == Unsat:
return 'UNSAT'
## try_split()
## if n_pos() > 1:
## result = prove_g_pos_split()
## if result[:5] == 'UNSAT':
## return result
#ps()
abc('r %s_smp.aig'%init_initial_f_name)
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()
if N == 1:
print '\nTrying deep interpolation on initial simplified circuit\n'
run_command('int -v -F 30000 -C 1000000 -T %d'%T)
result = get_status()
if result == Unsat:
return 'UNSAT'
if result < Unsat:
return 'SAT'
print '\nTrying deep BMC on initial simplified circuit\n'
run_command('bmc3 -v -T %d -F 200000 -C 1000000'%T)
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/ability = %f sec.'%(time.clock() - x)
print 'Additional time taken by BMC/PDR/Reach = %f sec.'%(time.clock() - xt)
return result
def try_split():
......@@ -1733,12 +1743,74 @@ def time_diff():
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 = []
for j in range(n_pos()):
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))
......@@ -1750,12 +1822,50 @@ def prove_all_ind():
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 inductively = ',
print '\nOutputs proved = ',
print plist
abc('r %s_osavetemp.aig'%f_name)
remove(plist) #remove the outputs proved
return status
## #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')
......@@ -1787,10 +1897,10 @@ def prove_1():
print_circuit_stats()
x_factor = xfi
print 'x_factor = %f'%x_factor
print '\nRunning pre_simp'
print '\n***Running pre_simp'
set_globals()
status = pre_simp()
if status <= Unsat:
if ((status <= Unsat) or (n_latches == 0)):
print 'Time for proof = %f sec.'%(time.clock() - x)
return RESULT[status]
abc('trm')
......@@ -1799,14 +1909,14 @@ def prove_1():
K = K +1
set_globals()
if ((n_ands() < 30000) and (a == 1) and (n_latches() < 300)):
print '\nRunning quick_verify'
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'\nRunning abstract'
print'\n***Running abstract'
nl_b = n_latches()
status = abstract()
abc('trm')
......@@ -1851,5 +1961,47 @@ def qprove():
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
scripts/main.py 0 → 100644
import os
##import par
##from abc_common import *
import abc_common
#this makes par the dominant module insteat of abc_common
from par import *
import sys
import math
import time
from pyabc_split import *
##import pdb
##from IPython.Debugger import Tracer; debug_here = Tracer()
#x('source ../../abc.rc')
#abc_common.x('source ../../abc.rc')
#IBM directories
# directories = ['ibmhard']
ibmhard = (33,34,36,37,28,40,42,44,48,5,49,50,52,53,58,59,6,64,66,67,68,\
69,70,71,72,73,74,75,76,78,79,80,81,82,83,84,86,9,87,89,90,0,10,\
11,12,14,15,16,2,19,20,29,31,32)
#directories = ['IBM_converted']
#ibm_convert = (3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,\
# 27,28,29,30,31,32,33,34,35,36,37,38,39,40,41)
#IBM_converted = range(42)[3:]
#the smaller files in ascending order
#IBM_converted = (26,38,21,15,22,23,20,27,16,19,24,28,18,9,8,7,6,25,17,3,4)
#the larger file in order (skipping 39)
#IBM_converted = (39,5,40,41,13,12,10,14,11,31,33,36,29,34,35,37,30)
IBM_converted = (5,40,41,13,12,10,14,11,31,33,36,29,34,35,37,30)
def scorriter():
""" apply scorr with increasing conflicts up to 100"""
x('time')
run_command('r p_0.aig')
n = 20
while n < 1000:
print_circuit_stats()
run_command('scorr -C %d'%n)
x('ind -C %d'%1000)
if is_unsat():
print 'n = %d'%n
break
n = 2*n
x('time')
def simplifyq():
# set_globals()
n=n_ands()
if n > 30000:
if n<45000:
abc("&get;&scl;&dc2;&put;dr;&get;&lcorr;&dc2;&put;dr;&get;&scorr;&fraig;&dc2;&put;dr;&get;&scorr -F 2;&dc2;&put;w temp.aig")
else:
abc("&get;&scl;&dc2;&put;dr;&get;&lcorr;&dc2;&put;dr;&get;&scorr;&fraig;&dc2;&put;dr;&get;&dc2;&put;w temp.aig")
n = n_ands()
if n < 30000:
if n > 15000:
abc("scl;rw;dr;lcorr;rw;dr;scorr;fraig;dc2;dr;dc2rs;w temp.aig")
else:
abc("scl;rw;dr;lcorr;rw;dr;scorr;fraig;dc2;dr;scorr -F 2;dc2rs;w temp.aig")
if n < 10000:
m = min( 30000/n, 8 )
if m > 2:
abc( "scorr -F %d"%m)
run_command("ps")
def constraints():
"""Determine if a set of files in a set of
directories has constraints and print out the results."""
for s in directories:
print("\ndirectory is "+s)
jj=eval(s)
print(jj)
for j in range(len(jj)):
x("\nr ../DIR/%s/p_%smp.aig"%(s,jj[j]))
print("structural:")
x('constr -s')
print("inductive constraints:")
x('constr ')
def strip():
"""Strip out each output of a multi-output example and write it
into a separate file"""
os.chdir('../DIR')
abc('r p_all_smp.aig')
po = n_pos()
print_circuit_stats()
for j in range(po):
abc('r p_all_smp.aig')
abc('cone -s -O %d'%j)
abc('scl;rw;trm')
abc('w p_%d.aig'%j)
print_circuit_stats()
def lst(list,match):
result = []
for j in range(len(list)):
if list[j][-len(match):] == match:
result.append(list[j])
return result
def lste(list,match,excp):
result = []
for j in range(len(list)):
if list[j][-len(match):] == match:
if excp in list[j]:
continue
result.append(list[j])
return result
def blif2aig():
""" converts blif files into aig files"""
#os.chdir('../ibm-web')
list_all = os.listdir('.')
l_blif = lst(list_all,'.blif')
for j in range(len(l_blif)):
name = l_blif[j][:-5]
print '%s '%name,
abc('r %s.blif'%name)
abc('st')
abc('fold')
abc('w %s.aig'%name)
ps()
def la():
return list_aig('')
def list_aig(s):
""" prnts out the sizes of aig files"""
#os.chdir('../ibm-web')
list_all = os.listdir('.')
dir = lst(list_all,'.aig')
dir.sort()
for j in range(len(dir)):
name = dir[j][:-4]
if not s in name:
continue
print '%s '%name,
abc('r %s.aig'%name)
ps()
return dir
def convert_ibm():
""" converts blif files (with constraints?) into aig files"""
os.chdir('../ibm-web')
list_ibm = os.listdir('.')
l_blif = lst(list_ibm,'.blif')
for j in range(len(l_blif)):
name = l_blif[j][:-5]
run_command('read_blif %s.blif'%name)
abc('undc')
abc('st -i')
abc('zero')
run_command('w %s.aig'%name)
"""if a<100000000:
f = min(8,max(1,40000/a))
#run_command('scorr -c -F %d'%f)
#print 'Result of scorr -F %d: '%f,
print_circuit_stats()
run_command('w p_%d.aig'%j)"""
def cl():
cleanup()
def cleanup():
list = os.listdir('.')
for j in range(len(list)):
name = list[j]
if (('_smp' in name) or ('_save' in name) or ('_backup' in name) or ('_osave' in name)
or ('_best' in name) or ('_gsrm' in name) or ('gore' in name) or
('_bip' in name) or ('sm0' in name) or ('gabs' in name)
or ('temp' in name) or ('__' in name) or ('greg' in name) or ('tf2' in name)
or ('gsrm' in name) or ('_rpm' in name ) or ('gsyn' in name) or ('beforerpm' in name)
or ('afterrpm' in name) or ('initabs' in name) or ('.status' in name) or ('_init' in name)
or ('_osave' in name) or ('tt_' in name) or ('_before' in name) or ('_after' in name)
or ('_and' in name) or ('_final' in name) or ('_spec' in name) or ('temp.a' in name) or ('_sync' in name)
):
os.remove(name)
def simp_mbi():
os.chdir('../mbi')
list_ibm = os.listdir('.')
l_aig = lst(list_ibm,'.aig')
for j in range(len(l_aig)):
name = l_aig[j][:-4]
run_command('r %s.aig'%name)
run_command('st')
print '\n%s: '%name
print_circuit_stats()
quick_simp()
scorr_comp()
simplify()
run_command('w %s_smp.aig'%name)
def strip_names():
os.chdir('../mbi')
list_ibm = os.listdir('.')
l_aig = lst(list_ibm,'.aig')
for j in range(len(l_aig)):
name = l_aig[j][:-4]
run_command('r %s.aig'%name)
run_command('st')
print '\n%s: '%name
print_circuit_stats()
quick_simp()
scorr_comp()
simplify()
run_command('w %s_smp.aig'%name)
def map_ibm():
os.chdir('../ibmmike2')
list_ibm = os.listdir('.')
l_blif = lst(list_ibm,'.blif')
result = []
print len(l_blif)
for j in range(len(l_blif)):
name = l_blif[j][:-5]
result.append('%s = %d'%(name,j))
return result
def absn(a,c,s):
""" testing Niklas abstraction with various conflict limits
a= method (0 - regular cba,
1 - pure pba,
2 - cba with pba at the end,
3 cba and pba interleaved at each step
c = conflict limit
s = No. of stable steps without cex"""
global G_C, G_T, latches_before_abs, x_factor, f_name
set_globals()
latches_before_abs = n_latches()
print 'Start: ',
print_circuit_stats()
print 'Een abstraction params: Method #%d, %d conflicts, %d stable'%(a,c,s)
run_command('&get; &abs_newstart -v -A %d -C %d -S %d'%(a,c,s))
bmcdepth = n_bmc_frames()
print 'BMC depth = %d'%n_bmc_frames()
abc('&w absn_greg.aig; &abs_derive; &put; w absn_gabs.aig')
print 'Final abstraction: ',
print_circuit_stats()
write_file('absn')
return "Done"
def xfiles():
global f_name
#output = sys.stdout
#iterate over all ESS files
#saveout = sys.stdout
#output = open("ibm_log.txt",'w')
# sys.stdout = output
os.chdir('../ess/f58m')
print 'Directories are %s'%directories
for s in directories:
sss= '../%s'%s
os.chdir(sss)
print "\nDirectory is %s\n"%s
jj=eval(s)
print (jj)
run_command('time')
for j in range(len(jj)):
print ' '
set_fname('p_%dsmp23'%jj[j])#file f_name.aig is read in
print 'p_%dsmp23'%jj[j]
run_command('time')
result = dprove3(1)
print result
run_command('time')
run_command('time')
os.chdir('../../python')
#sys.stdout = saveout
#output.close()
def sublist(L,I):
z = []
for i in range(len(I)):
s = L[I[i]],
s = list(s)
z = z + s
return z
def s2l(s):
""" takes the string s divided by '\n' and makess a list of items"""
result = []
while len(s)>2:
j = s.find('\n')
result.append(s[:j])
s = s[j+1:]
return result
def select(lst, s):
result = []
print lst
for j in range(len(lst)):
if s in lst[j]:
s1 = lst[j]
k = s1.find(':')
s1 = s1[:k]
result.append(s1)
return result
def process_result(name):
f = open(name,'r')
s = f.read()
f.close()
lst = s2l(s)
result = select(lst,'Timeout')
return result
def main():
stackno = 0
if len(sys.argv) != 2:
print "usage: %s <aig filename>"%sys.argv[0]
sys.exit(1)
aig_filename = sys.argv[1]
x("source ../../abc.rc")
read(aig_filename)
dprove3(1)
# a test to whether the script is being called from the command line
if __name__=="__main__":
main()
scripts/new_abc_commands.py
# You can use 'from pyabc import *' and then not need the pyabc. prefix everywhere
import os
import pyabc
import abc_common
import par
import tempfile
import shutil
import redirect
# A new command is just a function that accepts a list of string arguments
# The first argument is always the name of the command
# It MUST return an integer. -1: user quits, -2: error. Return 0 for success.
# a command that calls prove(1) and returns success
def prove_cmd(args):
result = abc_common.prove(1)
print result
return 0
# registers the command:
# The first argument is the function
# The second argument is the category (mainly for the ABC help command)
# The third argument is the new command name
# Keep the fourth argument 0, or consult with Alan
pyabc.add_abc_command(prove_cmd, "ZPython", "/prove", 0)
import optparse
def read_cmd(args):
if len(args)==2:
abc_common.read_file_quiet(args[1])
par.read_file_quiet(args[1])
else:
abc_common.read_file()
par.read_file()
return 0
pyabc.add_abc_command(read_cmd, "ZPython", "/rf", 0)
......@@ -109,75 +89,61 @@ def print_aiger_result(args):
pyabc.add_abc_command(print_aiger_result, "ZPython", "/print_aiger_result", 0)
def super_prove_aiger_cmd(args):
noisy = len(args)==2 and args[1]=='-n'
def proof_command_wrapper(prooffunc, category_name, command_name, change):
if not noisy:
pyabc.run_command('/pushredirect')
pyabc.run_command('/pushdtemp')
def wrapper(argv):
usage = "usage: %prog [options] <aig_file>"
try:
result = abc_common.super_prove()
except:
result = None
parser = optparse.OptionParser(usage, prog=command_name)
if not noisy:
pyabc.run_command('/popdtemp')
pyabc.run_command('/popredirect')
if result=="SAT":
print 1
elif result=="UNSAT":
print 0
else:
print 2
parser.add_option("-n", "--no_redirect", dest="noisy", action="store_true", default=False, help="don't redirect output")
parser.add_option("-d", "--current_dir", dest="current_dir", action="store_true", default=False, help="stay in current directory")
return 0
pyabc.add_abc_command(super_prove_aiger_cmd, "ZPython", "/super_prove_aiger", 0)
def prove_one_by_one_cmd(args):
noisy = len(args)==2 and args[1]=='-n'
# switch to a temporary directory
pyabc.run_command('/pushdtemp')
# write a copy of the original file in the temporary directory
pyabc.run_command('w original_aig_file.aig')
# iterate through the ouptus
for po in range(0, pyabc.n_pos()):
options, args = parser.parse_args(argv)
if not noisy:
pyabc.run_command('/pushredirect')
# replace the nework with the cone of the current PO
pyabc.run_command( 'cone -O %d -s'%po )
if len(args) != 2:
print args
parser.print_usage()
return 0
aig_filename = os.path.abspath(args[1])
# run super_prove
if not options.noisy:
pyabc.run_command('/pushredirect')
if not options.current_dir:
pyabc.run_command('/pushdtemp')
try:
result = abc_common.super_prove()
except:
result = 'UNKNOWN'
basename = os.path.basename( aig_filename )
shutil.copyfile(aig_filename, basename)
aig_filename = basename
if not noisy:
pyabc.run_command('/popredirect')
par.read_file_quiet(aig_filename)
result = prooffunc()
par.cex_list = []
except:
result = None
print 'PO %d is %s'%(po, result)
# stop if the result is not UNSAT
if result != "UNSAT":
break
if not options.current_dir:
pyabc.run_command('/popdtemp')
# read the original file for the next iteration
pyabc.run_command('r original_aig_file.aig')
# go back to the original directory
pyabc.run_command('/popdtemp')
if not options.noisy:
pyabc.run_command('/popredirect')
if result=="SAT":
print 1
elif result=="UNSAT":
print 0
else:
print 2
return 0
return 0
pyabc.add_abc_command(prove_one_by_one_cmd, "ZPython", "/prove_one_by_one", 0)
pyabc.add_abc_command(wrapper, category_name, command_name, change)
proof_command_wrapper(par.super_prove, 'HWMCC11', '/super_prove_aiger', 0)
proof_command_wrapper(par.simple_prove, 'HWMCC11', '/simple_prove_aiger', 0)
proof_command_wrapper(par.simple_bip, 'HWMCC11', '/simple_bip_aiger', 0)
scripts/par.py 0 → 100644
This source diff could not be displayed because it is too large. You can view the blob instead.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment