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

Merge pull request #279 from allen1236/master 

Sat-sweeping-based ECO (&str_eco)
This commit is contained in:
alanminko 2024-03-02 15:38:08 -08:00 committed by GitHub
parent 1fd79c8430 23654254e1
commit 390a0e8ef3
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
12 changed files with 1470 additions and 169 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
.gitignore vendored
View File

@ -8,6 +8,12 @@ ReleaseExt/
_/
_TEST/
_sandwich/
_scripts/
*.aig
*.vcproj
*.sh
*.v
lib/abc*
lib/m114*
lib/bip*

3
Makefile
View File

@ -33,7 +33,8 @@ MODULES := \
src/proof/pdr src/proof/abs src/proof/live src/proof/ssc src/proof/int \
src/proof/cec src/proof/acec 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/aig/miniaig \
src/sat/bsat2
all: $(PROG)
default: $(PROG)

148
abc.rc
View File

@ -1,148 +0,0 @@
# 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"
# standard aliases
alias hi history
alias b balance
alias cg clockgate
alias cl cleanup
alias clp collapse
alias cs care_set
alias el eliminate
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; sop; 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"
alias &sw_ "&put; sweep; st; &get"
alias &fx_ "&put; sweep; sop; fx; st; &get"
alias &dc3 "&b; &jf -K 6; &b; &jf -K 4; &b"
alias &dc4 "&b; &jf -K 7; &fx; &b; &jf -K 5; &fx; &b"
# 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 r2rs "b; rs -K 6; rw; rs -K 6 -N 2; rf; rs -K 8; b; rs -K 8 -N 2; rw; rs -K 10; rwz; rs -K 10 -N 2; b; rs -K 12; rfz; rs -K 12 -N 2; rwz; b"
alias compress2rs "b -l; rs -K 6 -l; rw -l; rs -K 6 -N 2 -l; rf -l; rs -K 8 -l; b -l; rs -K 8 -N 2 -l; rw -l; rs -K 10 -l; rwz -l; rs -K 10 -N 2 -l; b -l; rs -K 12 -l; rfz -l; rs -K 12 -N 2 -l; rwz -l; b -l"
alias c2rs "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"

23
src/aig/gia/gia.h
View File

@ -1790,6 +1790,29 @@ extern void Tas_ManSatPrintStats( Tas_Man_t * p );
extern int Tas_ManSolve( Tas_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 );
extern int Tas_ManSolveArray( Tas_Man_t * p, Vec_Ptr_t * vObjs );
/*=== giaBound.c ===========================================================*/
typedef struct Bnd_Man_t_ Bnd_Man_t;
extern Bnd_Man_t* Bnd_ManStart( Gia_Man_t *pSpec, Gia_Man_t *pImpl );
extern void Bnd_ManStop();
//for fraig
extern void Bnd_ManMap( int iLit, int id, int spec );
extern void Bnd_ManMerge( int id1, int id2, int phaseDiff );
extern void Bnd_ManFinalizeMappings();
extern void Bnd_ManPrintMappings();
// for eco
extern int Bnd_ManCheckBound( Gia_Man_t *p );
extern void Bnd_ManFindBound( Gia_Man_t *p );
extern Gia_Man_t* Bnd_ManGenSpecOut( Gia_Man_t *p );
extern Gia_Man_t* Bnd_ManGenImplOut( Gia_Man_t *p );
extern Gia_Man_t* Bnd_ManGenPatched( Gia_Man_t *pOut, Gia_Man_t *pSpec, Gia_Man_t *pPatch );
extern void Bnd_ManSetEqOut( int eq );
extern void Bnd_ManSetEqRes( int eq );
extern void Bnd_ManPrintStats();
// util
extern Gia_Man_t* Bnd_ManCutBoundary( Gia_Man_t *p, Vec_Int_t* vEI, Vec_Int_t* vEO, Vec_Bit_t* vEI_phase, Vec_Bit_t* vEO_phase );
ABC_NAMESPACE_HEADER_END

1048
src/aig/gia/giaBound.c Normal file
View File

File diff suppressed because it is too large Load Diff

130
src/aig/gia/giaDup.c
View File

@ -30,6 +30,9 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
extern Bnd_Man_t* pBnd;
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@ -5674,7 +5677,7 @@ Gia_Man_t * Gia_ManDupAddFlop( Gia_Man_t * p )
***********************************************************************/
Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose )
{
Vec_Int_t * vLits;
// Vec_Int_t * vLits;
Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj;
int i, iLit;
@ -5692,7 +5695,7 @@ Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose )
assert( Gia_ManRegNum(p2) == 0 );
assert( Gia_ManCiNum(p1) == Gia_ManCiNum(p2) );
assert( Gia_ManCoNum(p1) == Gia_ManCoNum(p2) );
vLits = Vec_IntAlloc( Gia_ManBufNum(p1) );
// vLits = Vec_IntAlloc( Gia_ManBufNum(p1) );
if ( fVerbose )
printf( "Creating a boundary miter with %d inputs, %d outputs, and %d buffers.\n",
Gia_ManCiNum(p1), Gia_ManCoNum(p1), Gia_ManBufNum(p1) );
@ -5702,28 +5705,123 @@ Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose )
Gia_ManHashStart( pNew );
Gia_ManConst0(p1)->Value = 0;
Gia_ManConst0(p2)->Value = 0;
Gia_ManForEachCi( p1, pObj, i )
pObj->Value = Gia_ManCi(p2, i)->Value = Gia_ManAppendCi( pNew );
Gia_ManForEachAnd( p2, pObj, i )
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
Gia_ManForEachAnd( p1, pObj, i ) {
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
if ( Gia_ObjIsBuf(pObj) )
Vec_IntPush( vLits, pObj->Value );
for( int i = 0; i < Gia_ManCiNum(p1); i++ )
{
int iLit = Gia_ManCi(p1, i)->Value = Gia_ManCi(p2, i) -> Value = Gia_ManAppendCi(pNew);
pObj = Gia_ManCi(p1, i);
Bnd_ManMap( iLit, Gia_ObjId( p1, pObj ), 1 );
pObj = Gia_ManCi(p2, i);
Bnd_ManMap( iLit, Gia_ObjId( p2, pObj) , 0 );
}
// record the corresponding impl node of each lit
Gia_ManForEachAnd( p2, pObj, i )
{
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
Bnd_ManMap( pObj -> Value, Gia_ObjId(p2, pObj), 0 );
}
// record hashed equivalent nodes
Gia_ManForEachAnd( p1, pObj, i )
{
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
Bnd_ManMap( pObj -> Value, Gia_ObjId(p1, pObj), 1 );
}
Gia_ManForEachCo( p2, pObj, i )
Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
//Gia_ManForEachCo( p1, pObj, i )
// Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
Vec_IntForEachEntry( vLits, iLit, i )
Gia_ManAppendCo( pNew, iLit );
Vec_IntFree( vLits );
{
iLit = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
}
Gia_ManForEachCo( p1, pObj, i )
{
iLit = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
}
// Vec_IntForEachEntry( vLits, iLit, i )
// Gia_ManAppendCo( pNew, iLit );
// Vec_IntFree( vLits );
Gia_ManHashStop( pNew );
pNew = Gia_ManCleanup( pTemp = pNew );
Gia_ManStop( pTemp );
return pNew;
}
/**Function*************************************************************
Synopsis [Duplicates AIG while putting objects in the DFS order.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManImplFromBMiter( Gia_Man_t * p, int nPo, int nBInput )
{
Gia_Man_t * pNew, *pTemp;
Gia_Obj_t * pObj, *pObj2;
int i;
int nBoundI = 0, nBoundO = 0;
int nExtra;
Gia_ManFillValue( p );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
// pNew->pName = Abc_UtilStrsav( p->pName );
// pNew->pSpec = Abc_UtilStrsav( p->pSpec );
Gia_ManConst0(p)->Value = 0;
// add po of impl
Gia_ManForEachCo( p, pObj, i )
{
if ( i < nPo )
{
Gia_ManDupOrderDfs_rec( pNew, p, pObj );
}
}
nExtra = Gia_ManAndNum( pNew );
// add boundary as buf
Gia_ManForEachCo( p, pObj, i )
{
if ( i >= 2 * nPo )
{
pObj2 = Gia_ObjFanin0(pObj);
if (~pObj2->Value) // visited boundary
{
if ( i >= 2 * nPo + nBInput )
{
nBoundO ++;
}
else nBoundI ++;
}
Gia_ManDupOrderDfs_rec( pNew, p, pObj2 );
Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) );
}
}
nExtra = Gia_ManAndNum( pNew ) - nExtra - Gia_ManBufNum( pNew );
Gia_ManForEachCi( p, pObj, i )
if ( !~pObj->Value )
pObj->Value = Gia_ManAppendCi(pNew);
assert( Gia_ManCiNum(pNew) == Gia_ManCiNum(p) );
Gia_ManDupRemapCis( pNew, p );
pNew = Gia_ManCleanup( pTemp = pNew );
Gia_ManStop( pTemp );
printf( "synthesized implementation:\n" );
printf( "\t%d / %d input boundary recovered.\n", nBoundI, nBInput );
printf( "\t%d / %d output boundary recovered.\n", nBoundO, Gia_ManCoNum(p)-2*nPo-nBInput );
printf( "\t%d / %d unused nodes in the box.\n", nExtra, Gia_ManAndNum(pNew) - Gia_ManBufNum( pNew ) );
return pNew;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

3
src/aig/gia/module.make
View File

@ -109,4 +109,5 @@ SRC += src/aig/gia/giaAig.c \
src/aig/gia/giaTsim.c \
src/aig/gia/giaTtopt.cpp \
src/aig/gia/giaUnate.c \
src/aig/gia/giaUtil.c
src/aig/gia/giaUtil.c \
src/aig/gia/giaBound.c

224
src/base/abci/abc.c
View File

@ -599,6 +599,7 @@ static int Abc_CommandAbc9ProdAdd ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandAbc9AddFlop ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9BMiter ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9GenHie ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9StrEco ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Test ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -1380,6 +1381,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&addflop", Abc_CommandAbc9AddFlop, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&bmiter", Abc_CommandAbc9BMiter, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&gen_hie", Abc_CommandAbc9GenHie, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&str_eco", Abc_CommandAbc9StrEco, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&test", Abc_CommandAbc9Test, 0 );
{
@ -38065,7 +38067,7 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
int fCbs = 1, approxLim = 600, subBatchSz = 1, adaRecycle = 500, nMaxNodes = 0;
Cec4_ManSetParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "JWRILDCNPMrmdckngxysopwvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "JWRILDCNPMrmdckngxysopwqvh" ) ) != EOF )
{
switch ( c )
{
@ -38218,6 +38220,9 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'w':
pPars->fVeryVerbose ^= 1;
break;
case 'q':
pPars->fBMiterInfo ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
break;
@ -38282,6 +38287,7 @@ usage:
Abc_Print( -2, "\t-o : toggle using the old SAT sweeper [default = %s]\n", fUseIvy? "yes": "no" );
Abc_Print( -2, "\t-p : toggle trying to prove when running the old SAT sweeper [default = %s]\n", fUseProve? "yes": "no" );
Abc_Print( -2, "\t-w : toggle printing even more verbose information [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
Abc_Print( -2, "\t-q : toggle printing additional information for boundary miters [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
@ -51945,11 +51951,21 @@ int Abc_CommandAbc9BMiter( Abc_Frame_t * pAbc, int argc, char ** argv )
char * FileName = NULL;
FILE * pFile = NULL;
int c, fVerbose = 0;
int bi = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
// TODO: use a flag to block Bnd_Man
while ( ( c = Extra_UtilGetopt( argc, argv, "Ivh" ) ) != EOF )
{
switch ( c )
{
case 'I':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" );
goto usage;
}
bi = atoi(argv[globalUtilOptind++]);
break;
case 'v':
fVerbose ^= 1;
break;
@ -51994,8 +52010,9 @@ int Abc_CommandAbc9BMiter( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: &bmiter [-vh] <file>\n" );
Abc_Print( -2, "usage: &bmiter -I <biNum> [-vh] <file>\n" );
Abc_Print( -2, "\t creates the boundary miter\n" );
Abc_Print( -2, "\t-I <biNum>: number of boundary inputs\n" );
Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
Abc_Print( -2, "\t<file> : the implementation file\n");
@ -52062,6 +52079,207 @@ usage:
Abc_Print( -2, "\t (the PO count of <file[i]> should not be less than the PI count of <file[i+1]>)\n");
return 1;}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
extern Bnd_Man_t* pBnd;
int Abc_CommandAbc9StrEco( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars );
extern void Cec4_ManSetParams( Cec_ParFra_t * pPars );
extern Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose );
Gia_Man_t *pImpl, *pImpl_out = 0, *pSpec_out = 0, *pMiter, *pPatch, *pPatched, *pTemp, *pBmiter;;
char * FileName = NULL;
FILE * pFile = NULL;
int c, fVerbose = 0, success = 1;
// params
Gps_Par_t Pars, * pPars = &Pars;
memset( pPars, 0, sizeof(Gps_Par_t) );
Cec_ParCec_t ParsCec, *pParsCec = &ParsCec;
Cec_ManCecSetDefaultParams( pParsCec );
Cec_ParFra_t ParsFra, *pParsFra = &ParsFra;
Cec4_ManSetParams( pParsFra );
pParsFra -> fBMiterInfo = 1;
// TODO: save return value and return at the end of the function
// parse options
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
{
switch ( c )
{
case 'v':
fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9StrEco(): There is no AIG.\n" );
return 0;
}
if ( argc != globalUtilOptind + 2 )
{
printf("%d\n", argc-globalUtilOptind);
Abc_Print( -1, "Abc_CommandAbc9StrEco(): AIG should be given on the command line.\n" );
return 0;
}
// read impl
FileName = argv[globalUtilOptind];
if ( (pFile = fopen( FileName, "r" )) == NULL )
{
Abc_Print( -1, "Cannot open input file \"%s\". ", FileName );
if ( (FileName = Extra_FileGetSimilarName( FileName, ".aig", ".blif", ".pla", ".eqn", ".bench" )) )
Abc_Print( 1, "Did you mean \"%s\"?", FileName );
Abc_Print( 1, "\n" );
return 1;
}
fclose( pFile );
pImpl = Gia_AigerRead( FileName, 0, 0, 0 );
if ( pImpl == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9StrEco(): Cannot read the file name on the command line.\n" );
return 0;
}
// read patch
FileName = argv[globalUtilOptind+1];
if ( (pFile = fopen( FileName, "r" )) == NULL )
{
Abc_Print( -1, "Cannot open input file \"%s\". ", FileName );
if ( (FileName = Extra_FileGetSimilarName( FileName, ".aig", ".blif", ".pla", ".eqn", ".bench" )) )
Abc_Print( 1, "Did you mean \"%s\"?", FileName );
Abc_Print( 1, "\n" );
return 1;
}
fclose( pFile );
pPatch = Gia_AigerRead( FileName, 0, 1, 0 );
if ( pPatch == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9StrEco(): Cannot read the file name on the command line.\n" );
return 0;
}
// start boundary manager
pBnd = Bnd_ManStart( pAbc->pGia, pImpl );
// verify if spec eq impl
pMiter = Gia_ManMiter( pAbc->pGia, pImpl, 0, 1, 0, 0, 0 );
if ( !Cec_ManVerify( pMiter, pParsCec ) )
{
Abc_Print( -1, "Abc_CommandAbc9StrEco(): The given impl is not equivalent to spec.\n" );
success = 0;
}
Gia_ManStop(pMiter);
// check boundary
if ( success )
{
if ( 0 == Bnd_ManCheckBound( pPatch ) || 0 == Bnd_ManCheckBound( pAbc -> pGia ) )
{
Abc_Print( -1, "Abc_CommandAbc9StrEco(): The given boundary is invalid.\n" );
success = 0;
}
}
if ( success )
{
// create bmiter, run fraig
pBmiter = Gia_ManBoundaryMiter( pAbc -> pGia, pImpl, 0 );
pTemp = Cec4_ManSimulateTest( pBmiter, pParsFra );
Gia_ManStop(pBmiter);
Gia_ManStop(pTemp);
// find
Bnd_ManFindBound( pAbc -> pGia );
// create spec_out and
pSpec_out = Bnd_ManGenSpecOut( pAbc -> pGia );
if ( !pSpec_out ) success = 0;
pImpl_out = Bnd_ManGenImplOut( pImpl );
if ( !pImpl_out ) success = 0;
// Gia_AigerWrite( pSpec_out, "spec_out.aig", 0, 0, 0 );
// Gia_AigerWrite( pImpl_out, "impl_out.aig", 0, 0, 0 );
// Gia_ManPrintStats( pSpec_out, pPars );
// Gia_ManPrintStats( pImpl_out, pPars );
}
if ( success )
{
// check if spec_out and imnpl_out are equivalent
printf("Checking the equivalence of spec_out and impl_out\n");
pMiter = Gia_ManMiter( pSpec_out, pImpl_out, 0, 1, 0, 0, 0 );
Bnd_ManSetEqOut( Cec_ManVerify( pMiter, pParsCec ) );
Gia_ManStop( pMiter );
// generate patched impl
printf("Generating patched impl\n");
pPatched = Bnd_ManGenPatched( pImpl_out, pAbc->pGia, pPatch );
// generate patched spec just for debugging
printf("Generating patched spec\n");
pTemp = Bnd_ManGenPatched( pSpec_out, pAbc->pGia, pPatch );
printf("Checking the equivalence of patched spec and patched impl\n");
pMiter = Gia_ManMiter( pTemp, pPatched, 0, 1, 0, 0, 0 );
Cec_ManVerify( pMiter, pParsCec );
Gia_ManStop( pMiter );
printf("Checking the equivalence of patched spec and patch\n");
pMiter = Gia_ManMiter( pTemp, pPatch, 0, 1, 0, 0, 0 );
Cec_ManVerify( pMiter, pParsCec );
Gia_ManStop( pMiter );
Gia_ManStop( pTemp );
// check if patched is equiv to patch
printf("Checking the equivalence of patched impl and patch\n");
pMiter = Gia_ManMiter( pPatch, pPatched, 0, 1, 0, 0, 0 );
Bnd_ManSetEqRes( Cec_ManVerify( pMiter, pParsCec ) );
Gia_ManStop( pMiter );
}
Bnd_ManPrintStats();
Gia_ManStop( pImpl );
Gia_ManStop( pPatch );
if ( pSpec_out ) Gia_ManStop( pSpec_out );
if ( pImpl_out ) Gia_ManStop( pImpl_out );
if ( success )
{
Abc_FrameUpdateGia( pAbc, pPatched );
}
Bnd_ManStop();
return 0;
usage:
Abc_Print( -2, "usage: &str_eco -I <biNum> [-vh] <impl> <patch>\n" );
Abc_Print( -2, "\t SAT-sweeping-based ECO\n" );
Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
Abc_Print( -2, "\t<impl> : the implementation aig. (should be equivalent to spec)\n");
Abc_Print( -2, "\t<patch> : the modified spec. (should be a hierarchical AIG)\n");
return 1;
}
/**Function*************************************************************

1
src/base/abci/abcMiter.c
View File

@ -789,6 +789,7 @@ Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial, int fVer
pNtkFrames->pName = Extra_UtilStrsav(Buffer);
// map the constant nodes
Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(pNtkFrames);
// create new latches (or their initial values) and remember them in the new latches
if ( !fInitial )
{

21
src/misc/vec/vecBit.h
View File

@ -626,6 +626,27 @@ static inline void Vec_BitReset( Vec_Bit_t * p )
p->pArray[i] = 0;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_BitPrint( Vec_Bit_t * p )
{
int i, Entry;
printf( "Vector has %d entries: {", Vec_BitSize(p) );
Vec_BitForEachEntry( p, Entry, i )
printf( " %d", Entry );
printf( " }\n" );
}
ABC_NAMESPACE_HEADER_END
#endif

2
src/proof/cec/cec.h
View File

@ -120,6 +120,8 @@ struct Cec_ParFra_t_
int fVeryVerbose; // verbose stats
int fVerbose; // verbose stats
int iOutFail; // the failed output
int fBMiterInfo; // printing BMiter information
int nPO; // number of po in original design given a bmiter
};
// combinational equivalence checking parameters

30
src/proof/cec/cecSatG2.c
View File

@ -219,6 +219,7 @@ void Cec4_ManSetParams( Cec_ParFra_t * pPars )
pPars->nSatVarMax = 1000; // the max number of SAT variables before recycling SAT solver
pPars->nCallsRecycle = 500; // calls to perform before recycling SAT solver
pPars->nGenIters = 100; // pattern generation iterations
pPars->fBMiterInfo = 0; // printing BMiter information
}
/**Function*************************************************************
@ -1781,8 +1782,10 @@ void Gia_ManRemoveWrongChoices( Gia_Man_t * p )
}
//Abc_Print( 1, "Removed %d wrong choices.\n", Counter );
}
int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** ppNew, int fSimOnly )
{
Cec4_Man_t * pMan = Cec4_ManCreate( p, pPars );
Gia_Obj_t * pObj, * pRepr;
int i, fSimulate = 1;
@ -1878,8 +1881,16 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p
if ( pRepr == NULL )
continue;
}
int id_obj = Gia_ObjId( p, pObj );
int id_repr = Gia_ObjId( p, pRepr );
if ( Abc_Lit2Var(pObj->Value) == Abc_Lit2Var(pRepr->Value) )
{
if ( pPars->fBMiterInfo )
{
Bnd_ManMerge( id_repr, id_obj, pObj->fPhase ^ pRepr->fPhase );
}
assert( (pObj->Value ^ pRepr->Value) == (pObj->fPhase ^ pRepr->fPhase) );
Gia_ObjSetProved( p, i );
if ( Gia_ObjId(p, pRepr) == 0 )
@ -1887,8 +1898,26 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p
continue;
}
if ( Cec4_ManSweepNode(pMan, i, Gia_ObjId(p, pRepr)) && Gia_ObjProved(p, i) )
{
if (pPars->fBMiterInfo){
Bnd_ManMerge( id_repr, id_obj, pObj->fPhase ^ pRepr->fPhase );
// printf( "proven %d merged into %d (phase : %d)\n", Gia_ObjId(p, pObj), Gia_ObjId(p,pRepr), pObj->fPhase ^ pRepr -> fPhase );
}
pObj->Value = Abc_LitNotCond( pRepr->Value, pObj->fPhase ^ pRepr->fPhase );
}
}
if ( pPars->fBMiterInfo )
{
// print
Bnd_ManFinalizeMappings();
// Bnd_ManPrintMappings();
}
if ( p->iPatsPi > 0 )
{
abctime clk2 = Abc_Clock();
@ -1937,6 +1966,7 @@ Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars )
{
Gia_Man_t * pNew = NULL;
Cec4_ManPerformSweeping( p, pPars, &pNew, 0 );
return pNew;
}
void Cec4_ManSimulateTest2( Gia_Man_t * p, int nConfs, int fVerbose )