Skip to content

A
abc
Commit c610c036 by Baruch Sterin
Options

pyabc: remove python integration from abc, it is moved to a separate extension

parent aa62165a
Showing with 1 additions and 5660 deletions
Makefile
......@@ -29,8 +29,7 @@ MODULES := \
src/proof/pdr src/proof/abs src/proof/live src/proof/ssc src/proof/int \
src/proof/cec src/proof/dch src/proof/fraig src/proof/fra src/proof/ssw \
src/aig/aig src/aig/saig src/aig/gia src/aig/ioa src/aig/ivy src/aig/hop \
src/aig/miniaig \
src/python
src/aig/miniaig
all: $(PROG)
default: $(PROG)
......
scripts/abc.rc deleted 100644 → 0
# reachx
python new_abc_commands.py
python -c "import reachx_cmd"
# global parameters
set check # checks intermediate networks
#set checkfio # prints warnings when fanins/fanouts are duplicated
#unset checkread # does not check 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
set dotunix dot
set gsviewwin gsview32.exe
set gsviewunix gv
set siswin sis.exe
set sisunix sis
set mvsiswin mvsis.exe
set mvsisunix mvsis
set capowin MetaPl-Capo10.1-Win32.exe
set capounix MetaPl-Capo10.1
set gnuplotwin wgnuplot.exe
set gnuplotunix gnuplot
# Niklas Een's commands
#load_plugin C:\_projects\abc\lib\bip_win.exe "BIP"
#load_plugin /hd/common/pyabc/bip "BIP"
# standard aliases
alias hi history
alias b balance
alias cg clockgate
alias cl cleanup
alias clp collapse
alias cs care_set
alias esd ext_seq_dcs
alias f fraig
alias fs fraig_sweep
alias fsto fraig_store
alias fres fraig_restore
alias fr fretime
alias ft fraig_trust
alias ic indcut
alias lp lutpack
alias pcon print_cone
alias pd print_dsd
alias pex print_exdc -d
alias pf print_factor
alias pfan print_fanio
alias pg print_gates
alias pl print_level
alias plat print_latch
alias pio print_io
alias pk print_kmap
alias pm print_miter
alias ps print_stats
alias psb print_stats -b
alias psu print_supp
alias psy print_symm
alias pun print_unate
alias q quit
alias r read
alias ra read_aiger
alias r3 retime -M 3
alias r3f retime -M 3 -f
alias r3b retime -M 3 -b
alias ren renode
alias rh read_hie
alias ri read_init
alias rl read_blif
alias rb read_bench
alias ret retime
alias dret dretime
alias rp read_pla
alias rt read_truth
alias rv read_verilog
alias rvl read_verlib
alias rsup read_super mcnc5_old.super
alias rlib read_library
alias rlibc read_library cadence.genlib
alias rty read_liberty
alias rlut read_lut
alias rw rewrite
alias rwz rewrite -z
alias rf refactor
alias rfz refactor -z
alias re restructure
alias rez restructure -z
alias rs resub
alias rsz resub -z
alias sa set autoexec ps
alias scl scleanup
alias sif if -s
alias so source -x
alias st strash
alias sw sweep
alias ssw ssweep
alias tr0 trace_start
alias tr1 trace_check
alias trt "r c.blif; st; tr0; b; tr1"
alias u undo
alias w write
alias wa write_aiger
alias wb write_bench
alias wc write_cnf
alias wh write_hie
alias wl write_blif
alias wp write_pla
alias wv write_verilog
# standard scripts
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 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 compress2 "b -l; rw -l; rf -l; b -l; rw -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 drwsat2 "st; drw; b -l; drw; drf; ifraig -C 20; drw; b -l; drw; drf"
alias share "st; multi -m; fx; resyn2"
alias addinit "read_init; undc; strash; zero"
alias blif2aig "undc; strash; zero"
alias v2p "&vta_gla; &ps; &gla_derive; &put; w 1.aig; pdr -v"
alias g2p "&ps; &gla_derive; &put; w 2.aig; pdr -v"
# resubstitution scripts for the IWLS paper
alias src_rw "st; rw -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"
# use this script to convert 1-valued and DC-valued flops for an AIG
alias fix_aig "logic; undc; strash; zero"
# use this script to convert 1-valued and DC-valued flops for a logic network coming from BLIF
alias fix_blif "undc; strash; zero"
# lazy man's synthesis
alias recadd3 "st; rec_add3; b; rec_add3; dc2; rec_add3; if -K 8; bidec; st; rec_add3; dc2; rec_add3; if -g -K 6; st; rec_add3"
scripts/abc_common.py deleted 100644 → 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
scripts/main.py deleted 100644 → 0
import os
import time
from datetime import *
##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')
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 help(s):
run_command('%s -h'%s)
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 fn_def(f,n):
filename = f.__code__.co_filename
firstline = f.__code__.co_firstlineno
lines = open(filename, "r").readlines()
print "".join(lines[firstline : n+firstline])
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()
result = []
for j in range(len(dir)):
name = dir[j][:-4]
if not s_in_s(s,name):
continue
print '%s '%name,
abc('r %s.aig'%name)
ps()
result = result + [name]
return result
def list_original():
list_dir = os.listdir('.')
list_dir.sort()
out = []
for i in range(len(list_dir)):
name = '%s/original.aig'%list_dir[i]
if os.access('%s'%name,os.R_OK):
abc('r %s;&ps'%name)
if n_latches() > 0 and n_pos() > 1:
size = str(sizeof())
print list_dir[i],
ps()
out = out + ['%s: %s'%(list_dir[i],size)]
return out
def list_size(s=''):
""" prnts out the sizes of aig files. Leaves .aig as part of name"""
#os.chdir('../ibm-web')
list_all = os.listdir('.')
dir = lst(list_all,'.aig')
dir.sort()
result = []
for j in range(len(dir)):
## name = dir[j][:-4]
name = dir[j] #leaves .aig as part of name
if not s_in_s(s,name):
continue
print '%s '%name,
## abc('r %s.aig'%name)
abc('r %s'%name)
ps()
result = result + [name[:-4]] #takes .aig off of name
return result
def rename(l=[]):
for j in range(len(l)):
name = l[j]
name1 = name +'.aig'
name2 = name[:-4]+'simp.aig' #take off _smp and put on simp
os.rename(name1,name2)
def list_blif(s=''):
""" prnts out the sizes of aig files"""
#os.chdir('../ibm-web')
list_all = os.listdir('.')
dir = lst(list_all,'.blif')
dir.sort()
result = []
for j in range(len(dir)):
name = dir[j][:-5]
if not s_in_s(s,name):
continue
print '%s: '%name,
abc('read_blif %s.blif'%name)
run_command('ps')
abc('st;zero;w %s.aig'%name)
result = result + [name]
return result
def s_in_s(s1,s2):
ls1 = len(s1)
l = 1+len(s2)- ls1
if l< 0:
return False
else:
for j in range(l):
if s1 == s2[j:j+ls1]:
return True
else:
continue
return False
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 ((s_in_s('_smp',name)) or (s_in_s('_save', name)) or (s_in_s('_backup', name)) or (s_in_s('_osave', name))
or (s_in_s('_best', name)) or (s_in_s('_gsrm', name)) or (s_in_s('gore', name)) or
(s_in_s('_bip', name)) or (s_in_s('sm0', name)) or (s_in_s('gabs', name))
or (s_in_s('temp', name)) or (s_in_s('__', name)) or (s_in_s('greg', name)) or (s_in_s('tf2', name))
or (s_in_s('gsrm', name)) or (s_in_s('_rpm', name )) or (s_in_s('gsyn', name)) or (s_in_s('beforerpm', name))
or (s_in_s('afterrpm', name)) or (s_in_s('initabs', name)) or (s_in_s('_init', name))
or (s_in_s('_osave', name)) or (s_in_s('tt_', name)) or (s_in_s('_before', name)) or (s_in_s('_after', name))
or (s_in_s('_and', name)) or (s_in_s('_spec', name)) or (s_in_s('temp.a', name))
or (s_in_s('_sync', name)) or (s_in_s('_old', name)) or (s_in_s('_cone_', name)) or (s_in_s('_abs', name))
or (s_in_s('_vabs', name)) or (s_in_s('_gla', name)) or (s_in_s('vabs', name)) or (s_in_s('_mp2', name))
or (s_in_s('_sc1', name)) or (s_in_s('_sc2', name)) or (s_in_s('_after', name))
or (s_in_s('_before', name)) or (s_in_s('_aigs_', name)) or (s_in_s('_cex.', name))
or (s_in_s('_bmc1', name)) or (s_in_s('_p0_', name)) or (s_in_s('_p1_', name))
or (s_in_s('_unsolv', name)) or (s_in_s('_iso1', 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 time_stamp():
d=datetime.today()
s = d.strftime('%m.%d.%y-%X')
return s
def apply_sp(list):
global m_trace
s = time_stamp()
out_name = "%s-traces.txt"%s
print out_name
if os.access(out_name,os.R_OK):
os.remove(out_name)
f = open(out_name,'w')
print f
for j in range(len(list)):
name = list[j]
print '\n\n**** %s ****\n'%name
f.write('\n\n****%s ****'%name)
read_file_quiet(name)
result = super_prove()
trace = result[1]
s = str(trace)
f.write('\n\n')
f.write(s)
f.flush()
f.close()
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/multi_prove.sh deleted 100644 → 0
#!/bin/sh
abc_root()
{
cwd="$(pwd)"
cd $(dirname "$1")
echo $(dirname "$(pwd)")
cd "${cwd}"
}
abc_dir=$(abc_root "$0")
bin_dir="${abc_dir}"/bin
exec ${bin_dir}/abc -q "/multi_prove_aiger $*"
scripts/new_abc_commands.py deleted 100644 → 0
import sys
import os
import pyabc
import par
import tempfile
import shutil
import redirect
import optparse
from contextlib import contextmanager
def read_cmd(args):
if len(args)==2:
par.read_file_quiet(args[1])
else:
par.read_file()
return 0
pyabc.add_abc_command(read_cmd, "ZPython", "/rf", 0)
def chdir_cmd(args):
os.chdir( args[1] )
return 0
pyabc.add_abc_command(chdir_cmd, "ZPython", "/cd", 0)
def pwd_cmd(args):
print os.getcwd()
return 0
pyabc.add_abc_command(pwd_cmd, "ZPython", "/pwd", 0)
def ls_cmd(args):
os.system("ls " + " ".join(args[1:]))
return 0
pyabc.add_abc_command(ls_cmd, "ZPython", "/ls", 0)
pushd_temp_stack = []
def pushdtemp_cmd(args):
tmpdir = tempfile.mkdtemp()
pushd_temp_stack.append( (os.getcwd(), tmpdir) )
os.chdir(tmpdir)
return 0
pyabc.add_abc_command(pushdtemp_cmd, "ZPython", "/pushdtemp", 0)
def popdtemp_cmd(args):
prev, temp = pushd_temp_stack.pop()
os.chdir(prev)
shutil.rmtree(temp, ignore_errors=True)
return 0
pyabc.add_abc_command(popdtemp_cmd, "ZPython", "/popdtemp", 0)
pushredirect_stack = []
def push_redirect_cmd(args):
fdout = redirect.start_redirect( redirect.null_file, sys.stdout)
pushredirect_stack.append( (sys.stdout, fdout) )
fderr = redirect.start_redirect( redirect.null_file, sys.stderr)
pushredirect_stack.append( (sys.stderr, fderr) )
return 0
pyabc.add_abc_command(push_redirect_cmd, "ZPython", "/pushredirect", 0)
def pop_redirect_cmd(args):
err, fderr = pushredirect_stack.pop()
redirect.end_redirect(err, fderr)
out, fdout = pushredirect_stack.pop()
redirect.end_redirect(out, fdout)
return 0
pyabc.add_abc_command(pop_redirect_cmd, "ZPython", "/popredirect", 0)
def print_aiger_result(args):
status = pyabc.prob_status()
if status==1:
print 0
elif status==0:
print 1
else:
print 2
return 0
pyabc.add_abc_command(print_aiger_result, "ZPython", "/print_aiger_result", 0)
@contextmanager
def replace_report_result(multi):
def report_result(po, result):
print "REPORT RESULT: ", po, result
print >> stdout, "%d"%result
print >> stdout, "b%d"%po
print >> stdout, "."
def report_liveness_result(po, result):
print "REPORT RESULT: ", po, result
print >> stdout, "%d"%result
print >> stdout, "j%d"%po
print >> stdout, "."
def report_bmc_depth(depth):
if not multi:
print "REPORT BMC DEPTH:", depth
print >> stdout, "u%d"%depth
with redirect.save_stdout() as stdout:
old_report_result = par.report_result
par.report_result = report_result
#old_report_liveness_result = par.report_liveness_result
par.report_liveness_result = report_liveness_result
old_report_bmc_depth = par.report_bmc_depth
par.report_bmc_depth = report_bmc_depth
try:
yield
finally:
par.report_result = old_report_result
#~ par.report_liveness_result = report_liveness_result
par.report_bmc_depth = old_report_bmc_depth
def proof_command_wrapper_internal(prooffunc, category_name, command_name, change, multi=False):
def wrapper(argv):
usage = "usage: %prog [options] <aig_file>"
parser = optparse.OptionParser(usage, prog=command_name)
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")
options, args = parser.parse_args(argv)
if len(args) != 2:
parser.print_usage()
return 0
aig_filename = os.path.abspath(args[1])
with replace_report_result(multi):
if not options.noisy:
pyabc.run_command('/pushredirect')
if not options.current_dir:
pyabc.run_command('/pushdtemp')
try:
for d in os.environ['PATH'].split(':'):
bip = os.path.join(d, 'bip')
if os.path.exists(bip):
pyabc.run_command("load_plugin %s Bip"%bip)
break
basename = os.path.basename( aig_filename )
shutil.copyfile(aig_filename, basename)
aig_filename = basename
result = prooffunc(aig_filename)
par.cex_list = []
except:
result = None
if not multi:
if result=="SAT":
par.report_result(0,1)
elif result=="UNSAT":
par.report_result(0,0)
elif type(result)==list and len(result)>0 and result[0] == "SAT":
par.report_result(0,1)
elif type(result)==list and len(result)>0 and result[0] == "UNSAT":
par.report_result(0,0)
else:
par.report_result(0,2)
if not options.current_dir:
pyabc.run_command('/popdtemp')
if not options.noisy:
pyabc.run_command('/popredirect')
return 0
pyabc.add_abc_command(wrapper, category_name, command_name, change)
def proof_command_wrapper(prooffunc, category_name, command_name, change, multi=False):
def pf(aig_filename):
par.read_file_quiet(aig_filename)
return prooffunc()
return proof_command_wrapper_internal(pf, category_name, command_name, change, multi)
proof_command_wrapper(par.sp, 'HWMCC13', '/super_prove_aiger', 0)
proof_command_wrapper(par.simple, 'HWMCC13', '/simple_aiger', 0)
proof_command_wrapper(par.simple_bip, 'HWMCC13', '/simple_bip_aiger', 0)
proof_command_wrapper(par.simple_sat, 'HWMCC13', '/simple_sat_aiger', 0)
proof_command_wrapper(par.mp, 'HWMCC13', '/multi_prove_aiger', 0, multi=True)
def simple_liveness_prooffunc(aig_filename):
import niklas
from pyaig import utils
def simplify(aiger_in, aiger_out):
with niklas.temp_file_names(2, suffix='.aig') as tmp:
saved = utils.save_po_info(aiger_in, tmp[0])
par.read_file_quiet(tmp[0])
par.pre_simp()
pyabc.run_command( 'write_aiger %s'%tmp[1] )
utils.restore_po_info( saved, tmp[1], aiger_out )
return True
def report_result(id, res):
if res and 'result' in res:
result = res['result']
if result=='proved':
par.report_liveness_result(id, 0)
return True
elif result=='failed':
par.report_liveness_result(id, 1)
return True
return False
try:
niklas.run_niklas_multi(aig_filename, simplify=simplify, report_result=report_result)
except:
import traceback
traceback.print_exc()
proof_command_wrapper_internal( simple_liveness_prooffunc, "HWMCC13", "/simple_liveness_aiger", 0, multi=True)
scripts/niklas.py deleted 100644 → 0
import os
import sys
import time
import tempfile
import subprocess
from contextlib import contextmanager
import pyabc
import pyabc_split
@contextmanager
def temp_file_names(N, suffix=""):
files = []
try:
for i in xrange(N):
files.append( tempfile.NamedTemporaryFile(suffix=suffix) )
yield [ f.name for f in files ]
finally:
for f in files:
f.close()
def parse_bip_status(status):
res = {}
for line in open(status, 'r'):
line = line.strip()
colon = line.find(':')
if colon < 0:
continue
field = line[:colon]
data = line[colon+2:]
res[field] = data
return res
def run_bip(args, aiger):
import redirect
with redirect.redirect():
with temp_file_names(1) as tmpnames:
args = [
'bip',
'-abc',
'-input=%s'%aiger,
'-output=%s'%tmpnames[0],
] + args;
rc = subprocess.call(args, preexec_fn=pyabc._set_death_signal)
if rc!=0:
return None
return parse_bip_status(tmpnames[0])
from pyaig import AIG, read_aiger, write_aiger, utils
def run_niklas_single(aiger, simplify, report_result, timeout=None):
orig_args = [
[ ',live', '-k=l2s', '-eng=treb-abs' ],
[ ',live', '-k=inc' ],
[ ',live', '-k=l2s', '-eng=bmc' ],
]
simplified_args = [
[ ',live', '-k=inc' ],
[ ',live', '-k=l2s', '-eng=bmc' ],
[ ',live', '-k=l2s', '-eng=treb' ],
]
with temp_file_names(1, suffix='.aig') as simple_aiger:
orig_funcs = [ pyabc_split.defer(run_bip)(a, aiger) for a in orig_args ]
simplified_funcs = [ pyabc_split.defer(run_bip)(a, simple_aiger[0]) for a in simplified_args ]
with pyabc_split.make_splitter() as splitter:
sleep_id = splitter.fork_one( lambda : time.sleep(timeout ) ) if timeout else None
ids = splitter.fork_all( orig_funcs )
kill_if_simplified = ids[1:]
simplifier_id = splitter.fork_one( pyabc_split.defer(simplify)(aiger, simple_aiger[0]) )
for id, res in splitter:
print 'NIKLAS: process %d finished with'%id, res
if id == sleep_id:
print 'NIKLAS: timeout'
return False
elif id == simplifier_id:
print 'NIKLAS: simplify ended'
if not res:
continue
print 'NIKLAS: killing'
splitter.kill(kill_if_simplified)
splitter.fork_all( simplified_funcs )
continue
elif report_result(res):
print 'NIKLAS: RESULT'
return True
return False
def run_niklas_multi(aiger, simplify, report_result):
with open(aiger, 'r') as fin:
aig = read_aiger( fin )
n_j_pos = aig.n_justice()
assert n_j_pos > 0
if n_j_pos==1:
return run_niklas_single( aiger, simplify, report_result=lambda res: report_result(0, res) )
with temp_file_names(n_j_pos, suffix='.aig') as single_aiger:
def extract(j_po):
with open(single_aiger[j_po], 'w') as fout:
write_aiger(utils.extract_justice_po(aig, j_po), fout)
for _ in pyabc_split.split_all_full( [pyabc_split.defer(extract)(i) for i in xrange(n_j_pos) ] ):
pass
unsolved = set( xrange(n_j_pos) )
timeout = 1
while unsolved:
for j_po in sorted(unsolved):
if run_niklas_single( single_aiger[j_po], simplify, report_result=lambda res: report_result(j_po, res), timeout=timeout ):
unsolved.remove(j_po)
timeout *= 2
return not unsolved
if __name__ == "__main__":
def simplify(aiger_in, aiger_out):
with temp_file_names(2, suffix='.aig') as tmp:
saved = utils.save_po_info(aiger_in, tmp[0])
pyabc.run_command( 'read_aiger %s'%tmp[0] )
pyabc.run_command( 'dc2 ; dc2 ; dc2 ; dc2' )
pyabc.run_command( 'write_aiger %s'%tmp[1] )
utils.restore_po_info( saved, tmp[1], aiger_out )
return True
def report_result(id, res):
if res and 'result' in res:
result = res['result']
if result=='proved':
print "PROVED: ", id
return True
elif result=='failed':
print "FAILED:", id
return True
return False
aiger = "test.aig"
while True:
try:
run_niklas_multi(aiger, simplify=simplify, report_result=report_result)
except:
import traceback
traceback.print_exc()
scripts/par.py deleted 100644 → 0
This source diff could not be displayed because it is too large. You can view the blob instead.
scripts/simple.sh deleted 100644 → 0
#!/bin/sh
abc_root()
{
cwd="$(pwd)"
cd $(dirname "$1")
echo $(dirname "$(pwd)")
cd "${cwd}"
}
abc_dir=$(abc_root "$0")
bin_dir="${abc_dir}"/bin
exec ${bin_dir}/abc -q "/simple_aiger $*"
scripts/simple_bip.sh deleted 100644 → 0
#!/bin/sh
abc_root()
{
cwd="$(pwd)"
cd $(dirname "$1")
echo $(dirname "$(pwd)")
cd "${cwd}"
}
abc_dir=$(abc_root "$0")
bin_dir="${abc_dir}"/bin
exec ${bin_dir}/abc -q "/simple_bip_aiger $*"
scripts/simple_liveness.sh deleted 100644 → 0
#!/bin/sh
abc_root()
{
cwd="$(pwd)"
cd $(dirname "$1")
echo $(dirname "$(pwd)")
cd "${cwd}"
}
abc_dir=$(abc_root "$0")
bin_dir="${abc_dir}"/bin
exec ${bin_dir}/abc -q "/simple_liveness_aiger $*"
scripts/simple_sat.sh deleted 100644 → 0
#!/bin/sh
abc_root()
{
cwd="$(pwd)"
cd $(dirname "$1")
echo $(dirname "$(pwd)")
cd "${cwd}"
}
abc_dir=$(abc_root "$0")
bin_dir="${abc_dir}"/bin
exec ${bin_dir}/abc -q "/simple_sat_aiger $*"
scripts/super_prove.sh deleted 100644 → 0
#!/bin/sh
abc_root()
{
cwd="$(pwd)"
cd $(dirname "$1")
echo $(dirname "$(pwd)")
cd "${cwd}"
}
abc_dir=$(abc_root "$0")
bin_dir="${abc_dir}"/bin
exec ${bin_dir}/abc -q "/super_prove_aiger $*"
src/base/main/mainReal.c
......@@ -45,10 +45,6 @@ SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.
***********************************************************************/
#ifdef ABC_PYTHON_EMBED
#include <Python.h>
#endif /* ABC_PYTHON_EMBED */
#include "base/abc/abc.h"
#include "mainInt.h"
#include "base/wlc/wlc.h"
......@@ -108,29 +104,6 @@ int Abc_RealMain( int argc, char * argv[] )
pAbc = Abc_FrameGetGlobalFrame();
pAbc->sBinary = argv[0];
#ifdef ABC_PYTHON_EMBED
{
PyObject* pModule;
void init_pyabc(void);
Py_SetProgramName(argv[0]);
Py_NoSiteFlag = 1;
Py_Initialize();
init_pyabc();
pModule = PyImport_ImportModule("pyabc");
if (pModule)
{
Py_DECREF(pModule);
}
else
{
fprintf( pAbc->Err, "error: pyabc.py not found. PYTHONPATH may not be set properly.\n");
}
}
#endif /* ABC_PYTHON_EMBED */
// default options
fBatch = INTERACTIVE;
fInitSource = 1;
......@@ -354,12 +327,6 @@ int Abc_RealMain( int argc, char * argv[] )
}
}
#ifdef ABC_PYTHON_EMBED
{
Py_Finalize();
}
#endif /* ABC_PYTHON_EMBED */
// if the memory should be freed, quit packages
// if ( fStatus < 0 )
{
......
src/base/main/mainUtils.c
......@@ -190,23 +190,6 @@ void Abc_UtilsSource( Abc_Frame_t * pAbc )
}
#endif
#ifdef ABC_PYTHON_EMBED
if ( getenv("ABC_PYTHON_ABC_RC") )
{
/* read script file from $ABC_PYTHON_ABC_RC */
char * sPath = getenv("ABC_PYTHON_ABC_RC");
if (sPath){
char * sCmd = ABC_ALLOC(char, strlen(sPath) + 50);
(void) sprintf(sCmd, "source -s %s", sPath);
(void) Cmd_CommandExecute(pAbc, sCmd);
ABC_FREE(sCmd);
}
}
else
#endif /* #ifdef ABC_PYTHON_EMBED */
{
char * sPath1, * sPath2;
char * home;
......
src/misc/util/utilSignal.c
......@@ -41,8 +41,6 @@ ABC_NAMESPACE_IMPL_START
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
#ifndef ABC_PYTHON_EMBED
int Util_SignalSystem(const char* cmd)
{
return system(cmd);
......@@ -63,8 +61,6 @@ void Util_SignalTmpFileRemove(const char* fname, int fLeave)
}
}
#endif /* ABC_PYTHON_EMBED */
ABC_NAMESPACE_IMPL_END
////////////////////////////////////////////////////////////////////////
......
src/python/abc.sh deleted 100644 → 0
#!/bin/sh
#
# Setup the ABC/Py environment and run the ABC/Py executable
# (ABC/Py stands for ABC with embedded Python)
#
# ABC/Py expects the following directory structure
#
# abc_root/
# bin/
# abc - this script
# abc_exe - the ABC executable
# ... - Other scripts
# lib/
# pyabc.py - support file for pyabc extension
# python_library.zip - The Python standard library. Only if not using the system Python interpreter.
# *.so - Python extensions, Only if not using the system Python interpreter.
# scripts/
# *.py - default directory for python scripts
#
# usage: abspath <dir>
# get the absolute path of <dir>
abspath()
{
cwd="$(pwd)"
cd "$1"
echo "$(pwd)"
cd "${cwd}"
}
self=$0
self_dir=$(dirname "${self}")
self_dir=$(abspath "${self_dir}")
abc_root=$(dirname "${self_dir}")
abc_exe="${abc_root}/bin/abc_exe"
PYTHONPATH="${abc_root}/lib":"${PYTHONPATH}"
export PYTHONPATH
if [ -d "${abc_root}/scripts" ] ; then
ABC_PYTHON_SCRIPTS="${abc_root}/scripts"
export ABC_PYTHON_SCRIPTS
PYTHONPATH="${ABC_PYTHON_SCRIPTS}":"${PYTHONPATH}"
export PYTHONPATH
fi
if [ -f "${abc_root}/scripts/abc.rc" ] ; then
ABC_PYTHON_ABC_RC="${abc_root}/scripts/abc.rc"
export ABC_PYTHON_ABC_RC
fi
if [ -f "${abc_root}/lib/python_library.zip" ] ; then
PYTHONHOME="${abc_root}"
export PYTHONHOME
PYTHONPATH="${abc_root}/lib/python_library.zip":"${PYTHONPATH}"
export PYTHONPATH
fi
PATH="${abc_root}/bin:$PATH"
export PATH
if [ "$1" = "--debug" ]; then
shift
abc_debugger="$1"
shift
echo export PYTHONHOME=$PYTHONHOME
echo export PYTHONPATH=$PYTHONPATH
echo export ABC_PYTHON_SCRIPTS=$ABC_PYTHON_SCRIPTS
echo export ABC_PYTHON_ABC_RC=$ABC_PYTHON_ABC_RC
fi
exec ${abc_debugger} "${abc_exe}" "$@"
src/python/abcpy_test.py deleted 100644 → 0
# You can use 'from pyabc import *' and then not need the pyabc. prefix everywhere
import pyabc
# 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 simple command that just prints its arguments and returns success
def pytest1_cmd(args):
print args
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
# Keet the fourth argument 0, or consult with Alan
pyabc.add_abc_command(pytest1_cmd, "Python-Test", "pytest1", 0)
# a simple command that just prints its arguments and runs the command 'scorr -h'
def pytest2_cmd(args):
print args
pyabc.run_command('scorr -h')
return 0
pyabc.add_abc_command(pytest2_cmd, "Python-Test", "pytest2", 0)
# Now a more complicated command with argument parsing
# This command gets two command line arguments -c and -v. -c cmd runs the command 'cmd -h' and -v prints the python version
# for more details see the optparse module: http://docs.python.org/library/optparse.html
import optparse
def pytest3_cmd(args):
usage = "usage: %prog [options]"
parser = optparse.OptionParser(usage, prog="pytest3")
parser.add_option("-c", "--cmd", dest="cmd", help="command to ask help for")
parser.add_option("-v", "--version", action="store_true", dest="version", help="display Python Version")
options, args = parser.parse_args(args)
if options.version:
print sys.version
return 0
if options.cmd:
pyabc.run_command("%s -h"%options.cmd)
return 0
return 0
pyabc.add_abc_command(pytest3_cmd, "Python-Test", "pytest3", 0)
src/python/build.txt deleted 100644 → 0
On Windows:
python setup.py build
python setup.py bdist_wininst
On Linux (from the main abc directory)
To build the extensions (make sure -fPIC is added to OPTFLAG in the main ABC Makefile first)
make ABC_PYTHON=/usr/bin/python pyabc_extension_install
To build the ABC with embedded python
make pyabc.tgz
Updating the latest version on mima:
alanmi@mima:~/abc_60$ cp ./src/python/build/lib.linux-x86_64-2.6/_pyabc.so /hd/common/pyabc/builds/101030/_pyabc.so
alanmi@mima:~/abc_60$ cp ./src/python/build/lib.linux-x86_64-2.6/pyabc.py /hd/common/pyabc/builds/101030/pyabc.py
alanmi@mima:/hd/common/pyabc$ rm current
alanmi@mima:/hd/common/pyabc$ ln -s builds/101030 current
alanmi@mima:/hd/common/pyabc$ ls -l
total 4
lrwxrwxrwx 1 alanmi common 13 2010-10-30 14:55 current -> builds/101030
Latest documentation:
http://goo.gl/jNV2
\ No newline at end of file
src/python/getch.py deleted 100644 → 0
class _Getch:
"""Gets a single character from standard input. Does not echo to the screen."""
def __init__(self):
try:
self.impl = _GetchWindows()
except ImportError:
self.impl = _GetchUnix()
def __call__(self): return self.impl()
class _GetchUnix:
def __init__(self):
import tty, sys
def __call__(self):
import sys, tty, termios
fd = sys.stdin.fileno()
old_settings = termios.tcgetattr(fd)
try:
tty.setraw(sys.stdin.fileno())
ch = sys.stdin.read(1)
finally:
termios.tcsetattr(fd, termios.TCSADRAIN, old_settings)
return ch
class _GetchWindows:
def __init__(self):
import msvcrt
def __call__(self):
import msvcrt
return msvcrt.getch()
getch = _Getch()
src/python/module.make deleted 100644 → 0
# To compile with the embedded python interpreter set
# the variable ABC_PYTHON to point to the python executable
#
# Examples:
# make ABC_PYTHON=/usr/bin/python
# make ABC_PYTHON=/usr/bin/python2.5
#
# To build the Python extension build the target pyabc
# To create a package of ABC with embedded Python use the target pyabc.tgz
ifdef ABC_PYTHON
# get the directory containing this file
ABC_PYTHON_FILES_PREFIX := $(CURDIR)/src/python
ABC_SWIG := swig
ABC_PYTHON_CONFIG := $(ABC_PYTHON)-config
ABC_PYTHON_CFLAGS := $(shell $(ABC_PYTHON_CONFIG) --includes) -DABC_PYTHON_EMBED=1
ABC_PYTHON_LDFLAGS := $(shell $(ABC_PYTHON_CONFIG) --ldflags)
CFLAGS += $(ABC_PYTHON_CFLAGS)
CXXFLAGS += $(ABC_PYTHON_CFLAGS)
LIBS += $(ABC_PYTHON_LDFLAGS)
ABC_PYTHON_SRC := $(ABC_PYTHON_FILES_PREFIX)/pyabc_wrap.c
SRC += $(ABC_PYTHON_SRC)
GARBAGE += \
$(ABC_PYTHON_SRC) \
$(ABC_PYTHON_SRC:_wrap.c=.py) \
$(ABC_PYTHON_SRC:_wrap.c=.pyc) \
$(ABC_PYTHON_FILES_PREFIX)/build \
$(ABC_PYTHON_FILES_PREFIX)/dist \
pyabc.tgz
ABC_PYABC_DIR ?= pyabc
ABC_PYABC_TGZ ?= pyabc.tgz
ABC_PYABC_EXTRA_BIN ?=
ABC_PYABC_EXTRA_LIB ?=
%_wrap.c %.py : %.i
$(ABC_SWIG) -python -outdir $(<D) $<
.PHONY: pyabc_extension_build
pyabc_extension_build : lib$(PROG).a $(ABC_PYTHON_SRC) $(ABC_PYTHON_SRC:_wrap.c=.py)
( cd $(ABC_PYTHON_FILES_PREFIX) && rm -rf build/ )
( cd $(ABC_PYTHON_FILES_PREFIX) && $(ABC_PYTHON) setup.py build )
.PHONY: pyabc_extension_install
pyabc_extension_install : pyabc_extension_build
( cd $(ABC_PYTHON_FILES_PREFIX) && $(ABC_PYTHON) setup.py install --user )
.PHONY: pyabc_extension_bdist
pyabc_extension_bdist : pyabc_extension_build
( cd $(ABC_PYTHON_FILES_PREFIX) && python setup.py bdist )
.PHONY: pyabc_tgz
pyabc_tgz : $(ABC_PYABC_TGZ)
$(ABC_PYABC_TGZ) : $(PROG) $(ABC_PYTHON_SRC:_wrap.c=.py) $(ABC_PYTHON_FILES_PREFIX)/abc.sh $(ABC_PYTHON_FILES_PREFIX)/package.py
$(ABC_PYTHON) $(ABC_PYTHON_FILES_PREFIX)/package.py \
--pyabc_dir=$(ABC_PYABC_DIR) \
--abc=$(PROG) \
--abc_sh=$(ABC_PYTHON_FILES_PREFIX)/abc.sh \
--pyabc=$(ABC_PYTHON_FILES_PREFIX) \
--extra_bin="$(ABC_PYABC_EXTRA_BIN)" \
--extra_lib="$(ABC_PYABC_EXTRA_LIB)" \
--out=$@ \
$(ABC_PYTHON_OPTIONS)
PYABC_INSTALL_TARGET ?= $(shell date +%Y-%m-%d_%H-%M.%N_${USER})
PYABC_INSTALL_TARGET := $(PYABC_INSTALL_TARGET)
PYABC_INSTALL_DIR ?= /hd/common/pyabc/builds/pyabc_builds/
pyabc_install_target: pyabc_extension_bdist
mkdir -p "$(PYABC_INSTALL_DIR)/$(PYABC_INSTALL_TARGET)"
tar \
--directory="$(PYABC_INSTALL_DIR)/$(PYABC_INSTALL_TARGET)" \
--show-transformed-names \
--transform='s#^.*/##g' \
-xvzf "$(ABC_PYTHON_FILES_PREFIX)/dist/pyabc-1.0.linux-x86_64.tar.gz"
find "$(PYABC_INSTALL_DIR)/$(PYABC_INSTALL_TARGET)/"* -type d | xargs rmdir
echo "Installed at $(PYABC_INSTALL_DIR)/$(PYABC_INSTALL_TARGET)"
endif
src/python/package.py deleted 100644 → 0
import os
import sys
import optparse
import zipfile
import tarfile
import tempfile
import time
import py_compile
def zip_library(f, extra_files = []):
lib = "%s/lib/python%s/"%(sys.prefix,sys.version[:3])
zf = zipfile.ZipFile(f, "w", zipfile.ZIP_DEFLATED)
for root, _, files in os.walk(lib):
arcroot = os.path.relpath(root, lib)
for f in files:
_, ext = os.path.splitext(f)
if ext in ['.py']:
zf.write(os.path.join(root,f), os.path.join(arcroot, f))
for s, r in extra_files:
zf.write( s, r )
zf.close()
def add_python_lib(tf, lib_dir, lib, mtime):
_, prefix = os.path.split(lib)
for root, _, files in os.walk(lib):
relpath = os.path.relpath(root, lib)
if '.hg' in relpath.split('/'):
continue
if relpath=='.':
arcroot = lib_dir
else:
arcroot = os.path.join( lib_dir, os.path.relpath(root, lib) )
arcroot = os.path.join(arcroot, prefix)
add_dir(tf, arcroot, mtime)
for f in files:
_, ext = os.path.splitext(f)
if ext in ['.py', '.so']:
add_file( tf, os.path.join(root,f), os.path.join(arcroot, f), 0666, mtime)
def add_dir(tf, dir, mtime):
ti = tarfile.TarInfo(dir)
ti.mode = 0777
ti.mtime = mtime
ti.type = tarfile.DIRTYPE
tf.addfile(ti)
def add_fileobj(tf, f, arcname, mode, mtime):
ti = tarfile.TarInfo(arcname)
ti.mode = mode
ti.mtime = mtime
f.seek(0, os.SEEK_END)
ti.size = f.tell()
f.seek(0, os.SEEK_SET)
tf.addfile(ti, f)
def add_file(tf, fname, arcname, mode, mtime):
print "\t adding %s as %s"%(fname, arcname)
with open(fname, "rb") as f:
add_fileobj(tf, f, arcname, mode, mtime)
def package(pyabc_dir, extra_bin, extra_lib, extra_files, abc_exe, abc_sh, pyabc, ofname, scripts_dir, use_sys):
mtime = time.time()
tf = tarfile.open(ofname, "w:gz")
add_dir(tf, "%s"%pyabc_dir, mtime)
add_dir(tf, "%s/bin"%pyabc_dir, mtime)
add_file(tf, abc_exe, "%s/bin/abc_exe"%pyabc_dir, 0777, mtime)
add_file(tf, abc_sh, "%s/bin/abc"%pyabc_dir, 0777, mtime)
if scripts_dir:
for fn in os.listdir(scripts_dir):
if fn.startswith('.'):
continue
fullname = os.path.join(scripts_dir, fn)
if os.path.isfile(fullname):
fnroot, fnext = os.path.splitext(fn)
if fnext==".sh":
add_file( tf, fullname, os.path.join("%s/bin"%pyabc_dir, fnroot), 0777, mtime)
elif fnext not in ( '.pyc', '.pyo'):
add_file( tf, fullname, os.path.join("%s/scripts"%pyabc_dir, fn), 0666, mtime)
for bin in extra_bin:
add_file( tf, bin, os.path.join("%s/bin"%pyabc_dir, os.path.basename(bin)), 0777, mtime)
lib_dir = "%s/lib"%pyabc_dir
add_dir(tf, lib_dir, mtime)
for lib in extra_lib:
add_python_lib( tf, lib_dir, lib, mtime)
for file, dest in extra_files:
add_file(tf, file, '%s/%s'%(pyabc_dir, dest), 0666, mtime)
for entry in os.listdir(pyabc):
if entry.endswith('.py'):
add_file( tf, os.path.join(pyabc, entry), os.path.join("%s/lib"%pyabc_dir, entry), 0666, mtime)
if not use_sys:
# ZIP standard library
zf = tempfile.NamedTemporaryFile("w+b")
#zip_library(zf, [(pyabc, "pyabc.py")])
zip_library(zf, [])
zf.flush()
add_fileobj(tf, zf, "%s/lib/python_library.zip"%pyabc_dir, 0666, mtime)
zf.close()
# add all extensions
lib_dynload = os.path.join(sys.exec_prefix,"lib", "python%s"%sys.version[:3], "lib-dynload")
for fn in os.listdir(lib_dynload):
fullname = os.path.join(lib_dynload, fn)
if os.path.isfile(fullname):
add_file( tf, fullname, os.path.join("%s/lib"%pyabc_dir, fn), 0666, mtime)
tf.close()
def main(args):
usage = "usage: %prog [options]"
parser = optparse.OptionParser(usage)
parser.add_option("-d", "--pyabc_dir", dest="pyabc_dir", help="name of generated directory" )
parser.add_option("-b", "--extra_bin", dest="extra_bin", help="extra binaries to pack" )
parser.add_option("-l", "--extra_lib", dest="extra_lib", help="extra directories in lib to pack" )
parser.add_option("-f", "--extra_files", dest="extra_files", help="additional files (comma separated pairs of file:dest" )
parser.add_option("-a", "--abc", dest="abc", help="location of the ABC exeutable")
parser.add_option("-s", "--abc_sh", dest="abc_sh", help="location of the ABC setup script")
parser.add_option("-p", "--pyabc", dest="pyabc", help="location of pyabc.py")
parser.add_option("-o", "--out", dest="out", help="location of output tar gzipped file")
parser.add_option("-x", "--scripts", dest="scripts", default="scripts", help="location of scripts")
parser.add_option("-S", "--system", action="store_false", dest="sys", default=True, help="use default python installation")
options, args = parser.parse_args(args)
if len(args) > 1:
parser.print_help()
return 1
if not options.pyabc_dir or not options.abc or not options.abc_sh or not options.pyabc or not options.out:
parser.print_help()
return 1
extra_bin = options.extra_bin.split(',') if options.extra_bin else []
extra_lib = options.extra_lib.split(',') if options.extra_lib else []
extra_files = [ s.split(':') for s in options.extra_files.split(',')] if options.extra_files else []
return package(options.pyabc_dir, extra_bin, extra_lib, extra_files, options.abc, options.abc_sh, options.pyabc, options.out, options.scripts, options.sys)
if __name__=="__main__":
main(sys.argv)
src/python/pyabc.i deleted 100644 → 0
%module pyabc
// -------------------------------------------------------------------
// SWIG typemap allowing us to grab a Python callable object
// -------------------------------------------------------------------
#ifdef SWIG<Python>
%typemap(in) PyObject *PyFunc
{
if ( !PyCallable_Check($source) )
{
PyErr_SetString(PyExc_TypeError, "Need a callable object!");
return NULL;
}
$target = $source;
}
#endif /* #ifdef SWIG<Python> */
%{
#include <base/main/main.h>
#include <misc/util/utilCex.h>
#include <stdlib.h>
#include <signal.h>
#include <sys/prctl.h>
#include <sys/types.h>
#include <sys/time.h>
#include <sys/resource.h>
#include <sys/wait.h>
#include <sys/stat.h>
#include <fcntl.h>
int n_ands()
{
Abc_Frame_t* pAbc = Abc_FrameGetGlobalFrame();
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
if ( pNtk && Abc_NtkIsStrash(pNtk) )
{
return Abc_NtkNodeNum(pNtk);
}
return -1;
}
int n_nodes()
{
Abc_Frame_t* pAbc = Abc_FrameGetGlobalFrame();
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
if ( pNtk )
{
return Abc_NtkNodeNum(pNtk);
}
return -1;
}
int n_pis()
{
Abc_Frame_t* pAbc = Abc_FrameGetGlobalFrame();
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
if ( pNtk )
{
return Abc_NtkPiNum(pNtk);
}
return -1;
}
int n_pos()
{
Abc_Frame_t* pAbc = Abc_FrameGetGlobalFrame();
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
if ( pNtk )
{
return Abc_NtkPoNum(pNtk);
}
return -1;
}
int n_latches()
{
Abc_Frame_t* pAbc = Abc_FrameGetGlobalFrame();
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
if ( pNtk )
{
return Abc_NtkLatchNum(pNtk);
}
return -1;
}
int n_levels()
{
Abc_Frame_t* pAbc = Abc_FrameGetGlobalFrame();
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
if ( pNtk )
{
return Abc_NtkLevel(pNtk);
}
return -1;
}
double n_area()
{
Abc_Frame_t* pAbc = Abc_FrameGetGlobalFrame();
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
if ( pNtk && Abc_NtkHasMapping(pNtk) )
{
return Abc_NtkGetMappedArea(pNtk);
}
return -1;
}
int has_comb_model()
{
Abc_Frame_t* pAbc = Abc_FrameGetGlobalFrame();
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
return pNtk && pNtk->pModel;
}
int has_seq_model()
{
Abc_Frame_t* pAbc = Abc_FrameGetGlobalFrame();
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
return pNtk && pNtk->pSeqModel;
}
int n_bmc_frames()
{
Abc_Frame_t* pAbc = Abc_FrameGetGlobalFrame();
return Abc_FrameReadBmcFrames(pAbc);
}
int prob_status()
{
Abc_Frame_t* pAbc = Abc_FrameGetGlobalFrame();
return Abc_FrameReadProbStatus(pAbc);
}
int is_valid_cex()
{
Abc_Frame_t* pAbc = Abc_FrameGetGlobalFrame();
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
return pNtk && Abc_FrameReadCex(pAbc) && Abc_NtkIsValidCex( pNtk, Abc_FrameReadCex(pAbc) );
}
int is_true_cex()
{
Abc_Frame_t* pAbc = Abc_FrameGetGlobalFrame();
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
return pNtk && Abc_FrameReadCex(pAbc) && Abc_NtkIsTrueCex( pNtk, Abc_FrameReadCex(pAbc) );
}
int n_cex_pis()
{
Abc_Frame_t* pAbc = Abc_FrameGetGlobalFrame();
return Abc_FrameReadCex(pAbc) ? Abc_FrameReadCexPiNum( pAbc ) : -1;
}
int n_cex_regs()
{
Abc_Frame_t* pAbc = Abc_FrameGetGlobalFrame();
return Abc_FrameReadCex(pAbc) ? Abc_FrameReadCexRegNum( pAbc ) : -1;
}
int cex_po()
{
Abc_Frame_t* pAbc = Abc_FrameGetGlobalFrame();
return Abc_FrameReadCex(pAbc) ? Abc_FrameReadCexPo( pAbc ) : -1;
}
int cex_frame()
{
Abc_Frame_t* pAbc = Abc_FrameGetGlobalFrame();
return Abc_FrameReadCex(pAbc) ? Abc_FrameReadCexFrame( pAbc ) : -1;
}
int n_phases()
{
Abc_Frame_t* pAbc = Abc_FrameGetGlobalFrame();
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
return pNtk ? Abc_NtkPhaseFrameNum(pNtk) : 1;
}
int is_const_po( int iPoNum )
{
Abc_Frame_t* pAbc = Abc_FrameGetGlobalFrame();
return Abc_FrameCheckPoConst( pAbc, iPoNum );
}
Abc_Cex_t* _cex_get()
{
Abc_Frame_t* pAbc = Abc_FrameGetGlobalFrame();
Abc_Cex_t* pCex = Abc_FrameReadCex(pAbc);
if ( ! pCex )
{
return NULL;
}
return Abc_CexDup( pCex, -1 );
}
int _cex_get_vec_len()
{
Abc_Frame_t* pAbc = Abc_FrameGetGlobalFrame();
Vec_Ptr_t* vCexVec = Abc_FrameReadCexVec(pAbc);
if( ! vCexVec )
{
return 0;
}
return Vec_PtrSize(vCexVec);
}
Abc_Cex_t* _cex_get_vec(int i)
{
Abc_Frame_t* pAbc = Abc_FrameGetGlobalFrame();
Vec_Ptr_t* vCexVec = Abc_FrameReadCexVec(pAbc);
if( ! vCexVec )
{
return NULL;
}
Abc_Cex_t* pCex = (Abc_Cex_t*)Vec_PtrEntry( vCexVec, i );
if ( ! pCex )
{
return NULL;
}
return Abc_CexDup( pCex, -1 );
}
int _status_get_vec_len()
{
Abc_Frame_t* pAbc = Abc_FrameGetGlobalFrame();
Vec_Int_t* vStatusVec = Abc_FrameReadStatusVec(pAbc);
if( ! vStatusVec )
{
return 0;
}
return Vec_IntSize(vStatusVec);
}
int _status_get_vec(int i)
{
Abc_Frame_t* pAbc = Abc_FrameGetGlobalFrame();
Vec_Int_t* vStatusVec = Abc_FrameReadStatusVec(pAbc);
if( ! vStatusVec )
{
return -1;
}
return Vec_IntEntry( vStatusVec, i );
}
void _cex_put(Abc_Cex_t* pCex)
{
if ( pCex )
{
pCex = Abc_CexDup(pCex, -1);
}
Abc_FrameSetCex( pCex );
}
void _cex_free(Abc_Cex_t* pCex)
{
Abc_CexFree(pCex);
}
int _cex_n_regs(Abc_Cex_t* pCex)
{
return pCex->nRegs;
}
int _cex_n_pis(Abc_Cex_t* pCex)
{
return pCex->nPis;
}
int _cex_get_po(Abc_Cex_t* pCex)
{
return pCex->iPo;
}
int _cex_get_frame(Abc_Cex_t* pCex)
{
return pCex->iFrame;
}
static PyObject* VecInt_To_PyList(Vec_Int_t* v)
{
PyObject* pylist = PyList_New( Vec_IntSize(v) );
int elem, i;
Vec_IntForEachEntry( v, elem, i)
{
PyList_SetItem( pylist, i, PyInt_FromLong(elem) );
}
return pylist;
}
PyObject* eq_classes()
{
Abc_Frame_t* pAbc = Abc_FrameGetGlobalFrame();
Vec_Ptr_t *vPoEquivs = Abc_FrameReadPoEquivs(pAbc);
PyObject* eq_classes;
Vec_Int_t* pEntry;
int i;
if( ! vPoEquivs )
{
Py_RETURN_NONE;
}
eq_classes = PyList_New( Vec_PtrSize(vPoEquivs) );
Vec_PtrForEachEntry( Vec_Int_t*, vPoEquivs, pEntry, i )
{
PyList_SetItem( eq_classes, i, VecInt_To_PyList(pEntry) );
}
return eq_classes;
}
PyObject* co_supp( int iCo )
{
PyObject* co_supp;
Vec_Int_t * vSupp;
Abc_Frame_t* pAbc = Abc_FrameGetGlobalFrame();
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
if ( !pNtk )
{
Py_RETURN_NONE;
}
vSupp = Abc_NtkNodeSupportInt( pNtk, iCo );
if( !vSupp )
{
Py_RETURN_NONE;
}
co_supp = VecInt_To_PyList( vSupp );
Vec_IntFree( vSupp );
return co_supp;
}
int is_func_iso( int iCo1, int iCo2 )
{
Abc_Frame_t* pAbc = Abc_FrameGetGlobalFrame();
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
if ( !pNtk )
{
return 0;
}
return Abc_NtkFunctionalIso( pNtk, iCo1, iCo2, 0 );
}
int is_func_iso2( int iCo1, int iCo2 )
{
Abc_Frame_t* pAbc = Abc_FrameGetGlobalFrame();
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
if ( !pNtk )
{
return 0;
}
return Abc_NtkFunctionalIso( pNtk, iCo1, iCo2, 1 );
}
void _pyabc_array_clear()
{
Abc_Frame_t* pAbc = Abc_FrameGetGlobalFrame();
Vec_Int_t *vObjIds = Abc_FrameReadObjIds(pAbc);
Vec_IntClear( vObjIds );
}
void _pyabc_array_push(int i)
{
Abc_Frame_t* pAbc = Abc_FrameGetGlobalFrame();
Vec_Int_t *vObjIds = Abc_FrameReadObjIds(pAbc);
Vec_IntPush( vObjIds, i );
}
int pyabc_array_read_entry(int i)
{
Abc_Frame_t* pAbc = Abc_FrameGetGlobalFrame();
Vec_Int_t *vObjIds = Abc_FrameReadObjIds(pAbc);
if( !vObjIds )
return -1;
return Vec_IntEntry( vObjIds, i );
}
static PyObject* pyabc_internal_python_command_callback = 0;
void pyabc_internal_set_command_callback( PyObject* callback )
{
Py_XINCREF(callback);
Py_XDECREF(pyabc_internal_python_command_callback);
pyabc_internal_python_command_callback = callback;
}
static int pyabc_internal_abc_command_callback(Abc_Frame_t * pAbc, int argc, char ** argv)
{
int i;
PyObject* args;
PyObject* arglist;
PyObject* res;
PyGILState_STATE gstate;
long lres;
if ( !pyabc_internal_python_command_callback )
return 0;
gstate = PyGILState_Ensure();
args = PyList_New(argc);
for( i=0 ; i<argc ; i++ )
PyList_SetItem(args, i, PyString_FromString(argv[i]) );
arglist = Py_BuildValue("(O)", args);
Py_INCREF(arglist);
res = PyEval_CallObject( pyabc_internal_python_command_callback, arglist );
Py_DECREF(arglist);
if ( !res )
{
PyGILState_Release(gstate);
return -1;
}
lres = PyInt_AsLong(res);
Py_DECREF(res);
PyGILState_Release(gstate);
return lres;
}
int run_command(char* cmd)
{
Abc_Frame_t* pAbc = Abc_FrameGetGlobalFrame();
int rc;
Py_BEGIN_ALLOW_THREADS
rc = Cmd_CommandExecute(pAbc, cmd);
Py_END_ALLOW_THREADS
return rc;
}
void pyabc_internal_register_command( char * sGroup, char * sName, int fChanges )
{
Abc_Frame_t* pAbc = Abc_FrameGetGlobalFrame();
Cmd_CommandAdd( pAbc, sGroup, sName, (Cmd_CommandFuncType)pyabc_internal_abc_command_callback, fChanges);
}
static int sigchld_pipe_fd = -1;
static void sigchld_handler(int signum)
{
while( write(sigchld_pipe_fd, "", 1) == -1 && errno==EINTR )
;
}
static void install_sigchld_handler(int sigchld_fd)
{
sigchld_pipe_fd = sigchld_fd;
signal(SIGCHLD, sigchld_handler);
}
static int sigint_pipe_fd = -1;
static void sigint_handler(int signum)
{
unsigned char tmp = (unsigned char)signum;
while( write(sigint_pipe_fd, &tmp, 1) == -1 && errno==EINTR )
;
}
static void install_sigint_handler(int sigint_fd)
{
sigint_pipe_fd = sigint_fd;
signal(SIGINT, sigint_handler);
// try to catch other signals that ask the process to terminate
signal(SIGABRT, sigint_handler);
signal(SIGQUIT, sigint_handler);
signal(SIGTERM, sigint_handler);
// try to ensure cleanup on exceptional conditions
signal(SIGBUS, sigint_handler);
signal(SIGILL, sigint_handler);
signal(SIGSEGV, sigint_handler);
// try to ensure cleanup before being killed due to resource limit
signal(SIGXCPU, sigint_handler);
signal(SIGXFSZ, sigint_handler);
}
sigset_t old_procmask;
static int nblocks = 0;
void block_sigint()
{
sigset_t procmask;
assert(nblocks==0);
nblocks ++ ;
sigemptyset(&procmask);
sigaddset(&procmask, SIGINT);
sigprocmask(SIG_BLOCK, &procmask, &old_procmask);
}
void unblock_sigint()
{
assert( nblocks==1);
nblocks--;
sigprocmask(SIG_SETMASK, &old_procmask, NULL);
}
static PyObject* pyabc_internal_system_callback = 0;
static PyObject* pyabc_internal_tmpfile_callback = 0;
static PyObject* pyabc_internal_tmpfile_remove_callback = 0;
int Util_SignalSystem(const char* cmd)
{
PyObject* arglist;
PyObject* res;
PyGILState_STATE gstate;
long lres;
if ( !pyabc_internal_system_callback )
return -1;
gstate = PyGILState_Ensure();
arglist = Py_BuildValue("(O)", PyString_FromString(cmd));
Py_INCREF(arglist);
res = PyEval_CallObject( pyabc_internal_system_callback, arglist );
Py_DECREF(arglist);
if ( !res )
{
PyGILState_Release(gstate);
return -1;
}
lres = PyInt_AsLong(res);
Py_DECREF(res);
PyGILState_Release(gstate);
return lres;
}
int Util_SignalTmpFile(const char* prefix, const char* suffix, char** out_name)
{
char* str;
Py_ssize_t size;
PyObject* arglist;
PyObject* res;
PyGILState_STATE gstate;
*out_name = NULL;
if ( !pyabc_internal_tmpfile_callback )
return 0;
gstate = PyGILState_Ensure();
arglist = Py_BuildValue("(ss)", prefix, suffix);
Py_INCREF(arglist);
res = PyEval_CallObject( pyabc_internal_tmpfile_callback, arglist );
Py_DECREF(arglist);
if ( !res )
{
PyGILState_Release(gstate);
return -1;
}
PyString_AsStringAndSize(res, &str, &size);
*out_name = ABC_ALLOC(char, size+1);
strcpy(*out_name, str);
Py_DECREF(res);
PyGILState_Release(gstate);
return open(*out_name, O_WRONLY);
}
void Util_SignalTmpFileRemove(const char* fname, int fLeave)
{
PyObject* arglist;
PyObject* res;
PyGILState_STATE gstate;
if ( !pyabc_internal_tmpfile_remove_callback )
return;
gstate = PyGILState_Ensure();
arglist = Py_BuildValue("(si)", fname, fLeave);
Py_INCREF(arglist);
res = PyEval_CallObject( pyabc_internal_tmpfile_remove_callback, arglist );
Py_DECREF(arglist);
Py_XDECREF(res);
PyGILState_Release(gstate);
}
void pyabc_internal_set_util_callbacks( PyObject* system_callback, PyObject* tmpfile_callback, PyObject* tmpfile_remove_callback )
{
Py_XINCREF(system_callback);
Py_XDECREF(pyabc_internal_system_callback);
pyabc_internal_system_callback = system_callback;
Py_XINCREF(tmpfile_callback);
Py_XDECREF(pyabc_internal_tmpfile_callback);
pyabc_internal_tmpfile_callback = tmpfile_callback;
Py_XINCREF(tmpfile_remove_callback);
Py_XDECREF(pyabc_internal_tmpfile_remove_callback);
pyabc_internal_tmpfile_remove_callback = tmpfile_remove_callback;
}
PyObject* _wait_no_hang()
{
int status;
int pid;
pid = wait3(&status, WNOHANG, NULL);
return Py_BuildValue("(iii)", pid, status, errno);
}
int _posix_kill(int pid, int signum)
{
return kill(pid, signum);
}
void _set_death_signal()
{
// send SIGINT if parent process is dead
prctl(PR_SET_PDEATHSIG, SIGINT);
// if parent process is already dead (and adopted by init)
if ( getppid() == 1)
{
raise(SIGINT);
}
}
%}
%init
%{
Abc_Start();
%}
int n_ands();
int n_nodes();
int n_pis();
int n_pos();
int n_latches();
int n_levels();
double n_area();
int run_command(char* cmd);
int has_comb_model();
int has_seq_model();
int n_bmc_frames();
int prob_status();
int is_valid_cex();
int is_true_cex();
int n_cex_pis();
int n_cex_regs();
int cex_po();
int cex_frame();
int n_phases();
int is_const_po( int iPoNum );
Abc_Cex_t* _cex_get();
int _cex_get_vec_len();
Abc_Cex_t* _cex_get_vec(int i);
int _status_get_vec_len();
int _status_get_vec(int i);
void _cex_put(Abc_Cex_t* pCex);
void _cex_free(Abc_Cex_t* pCex);
int _cex_n_regs(Abc_Cex_t* pCex);
int _cex_n_pis(Abc_Cex_t* pCex);
int _cex_get_po(Abc_Cex_t* pCex);
int _cex_get_frame(Abc_Cex_t* pCex);
PyObject* eq_classes();
PyObject* co_supp(int iCo);
int is_func_iso(int iCo1, int iCo2);
int is_func_iso2(int iCo1, int iCo2);
void _pyabc_array_clear();
void _pyabc_array_push(int i);
int pyabc_array_read_entry(int i);
void pyabc_internal_set_command_callback( PyObject* callback );
void pyabc_internal_register_command( char * sGroup, char * sName, int fChanges );
void install_sigchld_handler(int sigint_fd);
void install_sigint_handler(int sigint_fd);
void block_sigint();
void unblock_sigint();
void pyabc_internal_set_util_callbacks( PyObject* system_callback, PyObject* tmpfile_callback, PyObject* tmpfile_remove_callback );
PyObject* _wait_no_hang();
void _set_death_signal();
int _posix_kill(int pid, int signum);
void _set_death_signal();
%pythoncode
%{
class _Cex(object):
def __new__(cls, pCex):
if not pCex:
return None
if int(pCex)==1:
return True
return object.__new__(cls)
def __init__(self, pCex):
self.pCex = pCex
def __del__(self):
if _cex_free:
_cex_free(self.pCex)
def n_regs(self):
return _cex_n_regs(self.pCex)
def n_pis(self):
return _cex_n_pis(self.pCex)
def get_po(self):
return _cex_get_po(self.pCex)
def get_frame(self):
return _cex_get_frame(self.pCex)
def cex_get_vector():
return [ _Cex(_cex_get_vec(i)) for i in xrange(_cex_get_vec_len()) ]
def status_get_vector():
return [ _status_get_vec(i) for i in xrange(_status_get_vec_len()) ]
def cex_get():
return _Cex( _cex_get() )
def cex_put(cex):
assert cex is not None
assert cex.pCex is not None
return _cex_put(cex.pCex)
def create_abc_array(List):
_pyabc_array_clear()
for ObjId in List:
_pyabc_array_push(ObjId)
import threading
import select
import signal
import tempfile
import os
import errno
import sys, traceback
import subprocess
_active_lock = threading.Lock()
_die_flag = False
_active_pids = set()
_active_temp_files = set()
_terminated_pids_cond = threading.Condition(_active_lock)
_terminated_pids = {}
def add_temp_file(fname):
with _active_lock:
_active_temp_files.add(fname)
def remove_temp_file(fname):
with _active_lock:
_active_temp_files.remove(fname)
_old_os_wait3 = os.wait3
_select_select = select.select
def _retry_select(fd):
while True:
try:
rrdy,_,_ = _select_select([fd],[],[])
if fd in rrdy:
return
except select.error as e:
if e[0] == errno.EINTR:
continue
raise
def _retry_read(fd):
while True:
try:
return fd.read(1)
except OSError as e:
if e.errno == errno.EINTR:
continue
raise
def _retry_os_read(fd):
while True:
try:
return os.read(fd, 1)
except OSError as e:
if e.errno == errno.EINTR:
continue
raise
def _retry_wait():
while True:
pid, status, e = _wait_no_hang()
if pid>0:
return pid, status
elif pid==0:
return 0,0
elif pid == -1 and e == errno.ECHILD:
return 0,0
elif pid==-1 and e != errno.EINTR:
raise OSError(e, 'unknown error in wait3()')
def _sigint_wait_thread_func(fd):
global _die_flag
while True:
_retry_select(fd)
_retry_read(fd)
with _active_lock:
if _die_flag:
os._exit(-1)
_die_flag = True
for pid in _active_pids:
rc = _posix_kill(pid, signal.SIGINT)
for fname in _active_temp_files:
os.remove(fname)
os._exit(-1)
def _child_wait_thread_func(fd):
while True:
_retry_select(fd)
rc = _retry_read(fd)
with _active_lock:
while True:
pid, status = _retry_wait()
if pid==0:
break
if pid in _active_pids:
_active_pids.remove(pid)
_terminated_pids[pid] = status
os.write(_wait_fd_write, "1")
_terminated_pids_cond.notifyAll()
_sigint_pipe_read_fd = -1
_sigint_pipe_write_fd = -1
_sigchld_pipe_read_fd = -1
_sigchld_pipe_write_fd = -1
wait_fd = -1
_wait_fd_write = -1
def _start_threads():
global wait_fd, _wait_fd_write
wait_fd, _wait_fd_write = os.pipe()
global _sigint_pipe_read_fd, _sigint_pipe_write_fd
_sigint_pipe_read_fd, _sigint_pipe_write_fd = os.pipe()
sigint_read = os.fdopen(_sigint_pipe_read_fd, "r", 0 )
sigint_wait_thread = threading.Thread(target=_sigint_wait_thread_func, name="SIGINT wait thread", args=(sigint_read,))
sigint_wait_thread.setDaemon(True)
sigint_wait_thread.start()
install_sigint_handler(_sigint_pipe_write_fd)
global _sigchld_pipe_read_fd, _sigchld_pipe_write_fd
_sigchld_pipe_read_fd, _sigchld_pipe_write_fd = os.pipe()
sigchld_read = os.fdopen(_sigchld_pipe_read_fd, "r", 0 )
child_wait_thread = threading.Thread(target=_child_wait_thread_func, name="child process wait thread", args=(sigchld_read,))
child_wait_thread.setDaemon(True)
child_wait_thread.start()
install_sigchld_handler(_sigchld_pipe_write_fd)
_close_on_fork = []
def close_on_fork(fd):
_close_on_fork.append(fd)
def after_fork():
_set_death_signal()
global _close_on_fork
for fd in _close_on_fork:
os.close(fd)
_close_on_fork = []
os.close(wait_fd)
os.close(_wait_fd_write)
os.close(_sigint_pipe_read_fd)
os.close(_sigint_pipe_write_fd)
os.close(_sigchld_pipe_read_fd)
os.close(_sigchld_pipe_write_fd)
global _active_lock
_active_lock = threading.Lock()
global _terminated_pids_cond
_terminated_pids_cond = threading.Condition(_active_lock)
global _terminated_pids
_terminated_pids = {}
global _active_pids
_active_pids = set()
global _active_temp_files
_active_temp_files = set()
_start_threads()
class _sigint_block_section(object):
def __init__(self):
self.blocked = False
def __enter__(self):
block_sigint()
self.blocked = True
def __exit__(self, type, value, traceback):
self.release()
def release(self):
if self.blocked:
self.blocked = False
unblock_sigint()
_old_os_fork = os.fork
def _fork():
ppid = os.getpid()
with _sigint_block_section() as cs:
with _active_lock:
if _die_flag:
os._exit(-1)
pid = _old_os_fork()
if pid == 0:
after_fork()
if pid > 0:
_active_pids.add(pid)
return pid
def _waitpid(pid, options=0):
while True:
with _active_lock:
if pid in _terminated_pids:
_retry_os_read(wait_fd)
status = _terminated_pids[pid]
del _terminated_pids[pid]
return pid, status
if options==os.WNOHANG:
return 0, 0
_terminated_pids_cond.wait()
def _wait(options=0):
while True:
with _active_lock:
for pid, status in _terminated_pids.iteritems():
_retry_os_read(wait_fd)
del _terminated_pids[pid]
return pid, status
if options==os.WNOHANG:
return 0, 0
_terminated_pids_cond.wait()
_old_os_kill = os.kill
def _kill(pid, sig):
with _active_lock:
if pid in _terminated_pids:
return None
return _old_os_kill(pid,sig)
os.kill = _kill
os.fork = _fork
os.wait = _wait
os.waitpid = _waitpid
def _split_command_line(cmd):
args = []
i=0
while i<len(cmd):
while i<len(cmd) and cmd[i] in [' ','\t','\f']:
i += 1
if i >= len(cmd):
break
arg = []
in_quotes = None
while i<len(cmd):
if not in_quotes and cmd[i] in ['\'','\"','\'']:
in_quotes = cmd[i]
elif in_quotes and cmd[i]==in_quotes:
in_quotes = None
elif cmd[i] == '\\' and i<(len(cmd)+1):
i += 1
if cmd[i]=='\\':
arg.append('\\')
elif cmd[i]=='\'':
arg.append('\'')
elif cmd[i]=='\"':
arg.append('\'')
elif cmd[i]=='\"':
arg.append('\"')
elif cmd[i]=='a':
arg.append('\a')
elif cmd[i]=='b':
arg.append('\b')
elif cmd[i]=='n':
arg.append('\n')
elif cmd[i]=='f':
arg.append('\f')
elif cmd[i]=='r':
arg.append('\r')
elif cmd[i]=='t':
arg.append('\t')
elif cmd[i]=='v':
arg.append('\v')
else:
arg.append(cmd[i])
elif not in_quotes and cmd[i] in [' ','\t','\f']:
break
else:
arg.append(cmd[i])
i += 1
args.append( "".join(arg) )
return args
def system(cmd):
args = _split_command_line(cmd)
if args[-2] == '>':
with open(args[-1],'w') as fout:
p = subprocess.Popen(args[:-2], stdout=fout)
rc = p.wait()
return rc
else:
p = subprocess.Popen(args)
return p.wait()
def tmpfile(prefix, suffix):
with _active_lock:
with tempfile.NamedTemporaryFile(delete=False, prefix=prefix, suffix=suffix) as file:
_active_temp_files.add(file.name)
return file.name
def tmpfile_remove(fname, leave):
with _active_lock:
os.remove(fname)
_active_temp_files.remove(fname)
pyabc_internal_set_util_callbacks( system, tmpfile,tmpfile_remove )
_start_threads()
_registered_commands = {}
def _cmd_callback(args):
try:
assert len(args) > 0
cmd = args[0]
assert cmd in _registered_commands
res = _registered_commands[cmd](args)
assert type(res) == int, "User-defined Python command must return an integer."
return res
except Exception, e:
import traceback
traceback.print_exc()
except SystemExit, se:
pass
return 0
pyabc_internal_set_command_callback( _cmd_callback )
def add_abc_command(fcmd, group, cmd, change):
_registered_commands[ cmd ] = fcmd
pyabc_internal_register_command( group, cmd, change)
import optparse
xxx = {}
def cmd_python(cmd_args):
usage = "usage: %prog [options] <Python files>"
parser = optparse.OptionParser(usage, prog="python")
parser.add_option("-c", "--cmd", dest="cmd", help="Execute Python command directly")
parser.add_option("-v", "--version", action="store_true", dest="version", help="Display Python Version")
options, args = parser.parse_args(cmd_args)
if options.version:
print sys.version
return 0
if options.cmd:
exec options.cmd in xxx
return 0
scripts_dir = os.getenv('ABC_PYTHON_SCRIPTS', ".")
scripts_dirs = scripts_dir.split(':')
for fname in args[1:]:
if os.path.isabs(fname):
execfile(fname, xxx)
else:
for d in scripts_dirs:
fname = os.path.join(scripts_dir, fname)
if os.path.exists(fname):
execfile(fname, xxx)
break
return 0
add_abc_command(cmd_python, "Python", "python", 0)
%}
src/python/pyabc_split.py deleted 100644 → 0
"""
module pyabc_split
Executes python functions and their arguements as separate processes and returns their return values through pickling. This modules offers a single function:
Function: split_all(funcs)
The function returns a generator objects that allowes iteration over the results,
Arguments:
funcs: a list of tuples (f, args) where f is a python function and args is a collection of arguments for f.
Caveats:
1. Global variables in the parent process are not affected by the child processes.
2. The functions can only return simple types, see the pickle module for details
Usage:
Assume you would like to run the function f_1(1), f_2(1,2), f_3(1,2,3) in different processes.
def f_1(i):
return i+1
def f_2(i,j):
return i*10+j+1
def f_3(i,j,k):
return i*100+j*10+k+1
Construct a tuple of the function and arguments for each function
t_1 = (f_1, [1])
t_2 = (f_2, [1,2])
t_3 = (f_3, [1,2,3])
Create a list containing these tuples:
funcs = [t_1, t_2, t_3]
Use the function split_all() to run these functions in separate processes:
for res in split_all(funcs):
print res
The output will be:
2
13
124
(The order may be different, except that in this case the processes are so fast that they terminate before the next one is created)
Alternatively, you may quite in the middle, say after the first process returns:
for res in split_all(funcs):
print res
break
This will kill all processes not yet finished.
To run ABC operations, that required saving the child process state and restoring it at the parent, use abc_split_all().
import pyabc
def abc_f(truth):
import os
print "pid=%d, abc_f(%s)"%(os.getpid(), truth)
pyabc.run_command('read_truth %s'%truth)
pyabc.run_command('strash')
funcs = [
defer(abc_f)("1000"),
defer(abc_f)("0001")
]
for _ in abc_split_all(funcs):
pyabc.run_command('write_verilog /dev/stdout')
Author: Baruch Sterin <sterin@berkeley.edu>
"""
import os
import select
import fcntl
import errno
import sys
import cPickle as pickle
import signal
import cStringIO
import traceback
from contextlib import contextmanager
import pyabc
def _retry_select(rlist):
while True:
try:
rrdy,_,_ = select.select(rlist,[],[])
if rrdy:
return rrdy
except select.error as e:
if e[0] == errno.EINTR:
continue
raise
class _splitter(object):
def __init__(self):
self.pids = []
self.fds = {}
self.buffers = {}
self.results = {}
def is_done(self):
return len(self.fds) == 0
def _kill(self, pids):
# close pipes and kill child processes
for pid in pids:
if pid == -1:
continue
i, fd = self.fds[pid]
del self.buffers[fd]
del self.fds[pid]
self.pids[i] = -1
self.results[pid] = None
os.close(fd)
try:
os.kill( pid, signal.SIGINT)
except Exception as e:
print >>sys.stderr, 'exception while trying to kill pid=%d: '%pid, e
raise
# wait for termination and update result
for pid in pids:
os.waitpid( pid, 0 )
def kill(self, ids):
self._kill( [ self.pids[i] for i in ids ] )
def cleanup(self):
self._kill( self.fds.keys() )
def child( self, fdw, f):
# call function
try:
res = f()
except:
traceback.print_exc()
raise
# write return value into pipe
with os.fdopen( fdw, "w" ) as fout:
pickle.dump(res, fout)
return 0
def _fork_one(self, f):
# create a pipe to communicate with the child process
pr,pw = os.pipe()
# set pr to be non-blocking
fcntl.fcntl(pr, fcntl.F_SETFL, os.O_NONBLOCK)
parentpid = os.getpid()
rc = 1
try:
# create child process
pid = os.fork()
if pid == 0:
# child process:
os.close(pr)
pyabc.close_on_fork(pw)
rc = self.child( pw, f)
os._exit(rc)
else:
# parent process:
os.close(pw)
return (pid, pr)
finally:
if os.getpid() != parentpid:
os._exit(rc)
def fork_one(self, func):
pid, fd = self._fork_one(func)
i = len(self.pids)
self.pids.append(pid)
self.fds[pid] = (i, fd)
self.buffers[fd] = cStringIO.StringIO()
return i
def fork_all(self, funcs):
return [ self.fork_one(f) for f in funcs ]
def communicate(self):
rlist = [ fd for _, (_,fd) in self.fds.iteritems() ]
rlist.append(pyabc.wait_fd)
stop = False
while not stop:
rrdy = _retry_select( rlist )
for fd in rrdy:
if fd == pyabc.wait_fd:
stop = True
continue
self.buffers[fd].write( os.read(fd, 16384) )
def get_next_result(self):
# read from the pipes as needed, while waiting for the next child process to terminate
self.communicate()
# wait for the next child process to terminate
pid, rc = os.wait()
assert pid in self.fds
# retrieve the pipe file descriptor
i, fd = self.fds[pid]
del self.fds[pid]
# remove the pid
self.pids[i] = -1
# retrieve the buffer
buffer = self.buffers[fd]
del self.buffers[fd]
# fill the buffer
while True:
s = os.read(fd, 16384)
if not s:
break
buffer.write(s)
os.close(fd)
try:
return (i, pickle.loads(buffer.getvalue()))
except EOFError, pickle.UnpicklingError:
return (i, None)
def __iter__(self):
def iterator():
while not self.is_done():
yield self.get_next_result()
return iterator()
@contextmanager
def make_splitter():
# ensure cleanup of child processes
s = _splitter()
try:
yield s
finally:
s.cleanup()
def split_all_full(funcs):
# provide an iterator for child process result
with make_splitter() as s:
s.fork_all(funcs)
for res in s:
yield res
def defer(f):
return lambda *args, **kwargs: lambda : f(*args,**kwargs)
def split_all(funcs):
for _, res in split_all_full( ( defer(f)(*args) for f,args in funcs ) ):
yield res
import tempfile
@contextmanager
def temp_file_names(suffixes):
names = []
try:
for suffix in suffixes:
with tempfile.NamedTemporaryFile(delete=False, suffix=suffix) as file:
names.append( file.name )
yield names
finally:
for name in names:
os.unlink(name)
class abc_state(object):
def __init__(self):
with tempfile.NamedTemporaryFile(delete=False, suffix='.aig') as file:
self.aig = file.name
with tempfile.NamedTemporaryFile(delete=False, suffix='.log') as file:
self.log = file.name
pyabc.run_command(r'write_status %s'%self.log)
pyabc.run_command(r'write_aiger %s'%self.aig)
def __del__(self):
os.unlink( self.aig )
os.unlink( self.log )
def restore(self):
pyabc.run_command(r'read_aiger %s'%self.aig)
pyabc.run_command(r'read_status %s'%self.log)
def abc_split_all(funcs):
import pyabc
def child(f, aig, log):
res = f()
pyabc.run_command(r'write_status %s'%log)
pyabc.run_command(r'write_aiger %s'%aig)
return res
def parent(res, aig, log):
pyabc.run_command(r'read_aiger %s'%aig)
pyabc.run_command(r'read_status %s'%log)
return res
with temp_file_names( ['.aig','.log']*len(funcs) ) as tmp:
funcs = [ defer(child)(f, tmp[2*i],tmp[2*i+1]) for i,f in enumerate(funcs) ]
for i, res in split_all_full(funcs):
yield i, parent(res, tmp[2*i],tmp[2*i+1])
if __name__ == "__main__":
# define some functions to run
def f_1(i):
return i+1
def f_2(i,j):
return i*10+j+1
def f_3(i,j,k):
return i*100+j*10+k+1
# Construct a tuple of the function and arguments for each function
t_1 = (f_1, [1])
t_2 = (f_2, [1,2])
t_3 = (f_3, [1,2,3])
# Create a list containing these tuples:
funcs = [t_1, t_2, t_3]
# Use the function split_all() to run these functions in separate processes:
for res in split_all(funcs):
print res
# Alternatively, quit after the first process returns:
for res in split_all(funcs):
print res
break
# For operations with ABC that save and restore status
import pyabc
def abc_f(truth):
import os
print "pid=%d, abc_f(%s)"%(os.getpid(), truth)
pyabc.run_command('read_truth %s'%truth)
pyabc.run_command('strash')
return 100
funcs = [
defer(abc_f)("1000"),
defer(abc_f)("0001")
]
best = None
for i, res in abc_split_all(funcs):
print i, res
if best is None:\
# save state
best = abc_state()
pyabc.run_command('write_verilog /dev/stdout')
# if there is a saved state, restore it
if best is not None:
best.restore()
pyabc.run_command('write_verilog /dev/stdout')
src/python/reachx_cmd.py deleted 100644 → 0
# You can use 'from pyabc import *' and then not need the pyabc. prefix everywhere
import sys
import optparse
import subprocess
import tempfile
import threading
import os
import os.path
from contextlib import contextmanager, nested
import pyabc
def popen_and_wait_with_timeout(timeout,cmd, *args, **kwargs):
""" Wait for a subprocess.Popen object to terminate, or until timeout (in seconds) expires. """
p = None
t = None
try:
p = subprocess.Popen(cmd, *args, **kwargs)
if timeout <= 0:
timeout = None
t = threading.Thread(target=lambda: p.communicate())
t.start()
t.join(timeout)
finally:
if p is not None and p.poll() is None:
p.kill()
if t is not None and t.is_alive():
t.join()
if p is not None:
return p.returncode
return -1
@contextmanager
def temp_file_name(suffix=""):
file = tempfile.NamedTemporaryFile(delete=False, suffix=suffix)
name = file.name
file.close()
try:
yield name
finally:
os.unlink(name)
def cygpath(path):
if sys.platform == "win32":
if os.path.isabs(path):
drive, tail = os.path.splitdrive(path)
drive = drive.lower()
tail = tail.split(os.path.sep)
return '/cygdrive/%s'%drive[0] + '/'.join(tail)
else:
path = path.split(os.path.sep)
return "/".join(path)
return path
def run_reachx_cmd(effort, timeout):
with nested(temp_file_name(suffix=".aig"), temp_file_name()) as (tmpaig_name, tmplog_name):
pyabc.run_command("write %s"%tmpaig_name)
cmdline = [
'read %s'%cygpath(tmpaig_name),
'qua_ffix -effort %d -L %s'%(effort, cygpath(tmplog_name)),
'quit'
]
cmd = ["jabc", "-c", " ; ".join(cmdline)]
rc = popen_and_wait_with_timeout(timeout, cmd, shell=False, stdout=sys.stdout, stderr=sys.stderr)
if rc != 0:
# jabc failed or stopped. Write a status file to update the status to unknown
with open(tmplog_name, "w") as f:
f.write('snl_UNK -1 unknown\n')
f.write('NULL\n')
f.write('NULL\n')
pyabc.run_command("read_status %s"%tmplog_name)
return rc
def reachx_cmd(argv):
usage = "usage: %prog [options]"
parser = optparse.OptionParser(usage, prog="reachx")
parser.add_option("-e", "--effort", dest="effort", type=int, default=0, help="effort level. [default=0, means unlimited]")
parser.add_option("-t", "--timeout", dest="timeout", type=int, default=0, help="timeout in seconds [default=0, unlimited]")
options, args = parser.parse_args(argv)
rc = run_reachx_cmd(options.effort, options.timeout)
print "%s command: jabc returned: %d"%(argv[0], rc)
return 0
pyabc.add_abc_command(reachx_cmd, "Verification", "reachx", 0)
src/python/redirect.py deleted 100644 → 0
"""
A simple context manager for redirecting streams in Python.
The streams are redirected at the the C runtime level so that the output of C extensions
that use stdio will also be redirected.
null_file : a stream representing the null device (e.g. /dev/null on Unix)
redirect: a context manager for redirecting streams
Author: Baruch Sterin (sterin@berkeley.edu)
"""
import os
import sys
from contextlib import contextmanager
null_file = open( os.devnull, "w" )
@contextmanager
def _dup( f ):
fd = os.dup( f.fileno() )
yield fd
os.close(fd)
@contextmanager
def save_stdout( src = sys.stdout ):
"""
Redirect
"""
fd = os.dup( src.fileno() )
own = True
try:
with os.fdopen( fd, "w", 0) as f:
own = False
yield f
except:
if own:
os.close(fd)
raise
@contextmanager
def redirect(dst = null_file, src = sys.stdout):
"""
Redirect the src stream into dst.
Example:
with redirect( open("somefile.txt", sys.stdout ) ):
do some stuff ...
"""
if src.fileno() == dst.fileno():
yield
return
with _dup( src ) as fd_dup_src:
dst.flush()
src.flush()
os.close( src.fileno() )
os.dup2( dst.fileno(), src.fileno() )
yield
src.flush()
os.close( src.fileno() )
os.dup2( fd_dup_src, src.fileno() )
def start_redirect(dst = null_file, src = sys.stdout):
"""
Start redirection of src stream into dst. Return the duplicated file handle of the source.
Example:
fd = start_redirect( open("somefile.txt"), sys.stdout )
... do some stuff ...
end_redirect(sys.stdout, fd)
"""
if src.fileno() == dst.fileno():
return None
fd_dup_src = os.dup( src.fileno() )
dst.flush()
src.flush()
os.close( src.fileno() )
os.dup2( dst.fileno(), src.fileno() )
return fd_dup_src
def end_redirect(src, fd_dup_src):
"""
End redirection of stream src.Redirect the src stream into dst. src is the source stream and fd_dup_src is the value returned by
start_redirect()
"""
if fd_dup_src is None:
return
src.flush()
os.close( src.fileno() )
os.dup2( fd_dup_src, src.fileno() )
os.close(fd_dup_src)
src/python/setup.py deleted 100644 → 0
import sys
from distutils.core import setup, Extension
from distutils.sysconfig import get_config_vars
from distutils import util
from distutils.command.build_ext import build_ext
from distutils import sysconfig
define_macros = []
libraries = []
library_dirs = []
if sys.platform == "win32":
src_file = [ 'pyabc.i' ]
define_macros.append( ('WIN32', 1) )
define_macros.append( ('ABC_DLL', 'ABC_DLLEXPORT') )
libraries.append('abcr')
library_dirs.append('./../../lib')
else:
src_file = [ 'pyabc_wrap.c' ]
if get_config_vars()['SIZEOF_VOID_P'] > 4:
define_macros.append( ('LIN64', 1) )
else:
define_macros.append( ('LIN', 1) )
libraries.append( 'abc' )
libraries.append( 'rt' )
libraries.append( 'readline' )
library_dirs.append('./../../')
# ugly hack to silence strict-prototype warnings
class build_ext_subclass( build_ext ):
def build_extensions(self):
CC = sysconfig.get_config_var("CC")
if self.compiler.compiler_type == 'unix' and ( 'gcc' in CC or 'g++' in CC):
for e in self.extensions:
e.extra_compile_args.append( '-Wno-strict-prototypes' )
build_ext.build_extensions(self)
ext = Extension(
'_pyabc',
src_file,
define_macros=define_macros,
include_dirs = ["../../src"],
library_dirs=library_dirs,
libraries=libraries
)
setup(
name='pyabc',
version='1.0',
ext_modules=[ext],
py_modules=['pyabc','getch','pyabc_split','redirect', 'reachx_cmd'],
cmdclass = {'build_ext': build_ext_subclass }
)
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