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

Merge pull request #280 from allen1236/master 

added command &brecover and modified &str_eco
This commit is contained in:
alanminko 2024-03-03 20:29:46 -08:00 committed by GitHub
parent a747f46292 c607fc3101
commit 8bfd49880e
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
11 changed files with 621 additions and 150 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
.gitignore vendored
View File

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

3
Makefile
View File

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

148
abc.rc Normal file
View File

@ -0,0 +1,148 @@
# 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"

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

@ -1793,19 +1793,26 @@ extern int Tas_ManSolveArray( Tas_Man_t * p, Vec_Ptr_t * vObjs )
/*=== giaBound.c ===========================================================*/ /*=== giaBound.c ===========================================================*/
typedef struct Bnd_Man_t_ Bnd_Man_t; typedef struct Bnd_Man_t_ Bnd_Man_t;
extern Bnd_Man_t* Bnd_ManStart( Gia_Man_t *pSpec, Gia_Man_t *pImpl ); extern Bnd_Man_t* Bnd_ManStart( Gia_Man_t *pSpec, Gia_Man_t *pImpl, int fVerbose );
extern void Bnd_ManStop(); extern void Bnd_ManStop();
// getter
extern int Bnd_ManGetNInternal();
extern int Bnd_ManGetNExtra();
//for fraig //for fraig
extern void Bnd_ManMap( int iLit, int id, int spec ); extern void Bnd_ManMap( int iLit, int id, int spec );
extern void Bnd_ManMerge( int id1, int id2, int phaseDiff ); extern void Bnd_ManMerge( int id1, int id2, int phaseDiff );
extern void Bnd_ManFinalizeMappings(); extern void Bnd_ManFinalizeMappings();
extern void Bnd_ManPrintMappings(); extern void Bnd_ManPrintMappings();
// for eco // for eco
extern int Bnd_ManCheckBound( Gia_Man_t *p ); extern int Bnd_ManCheckBound( Gia_Man_t *p, int fVerbose );
extern void Bnd_ManFindBound( 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_ManGenSpecOut( Gia_Man_t *p );
extern Gia_Man_t* Bnd_ManGenImplOut( 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 Gia_Man_t* Bnd_ManGenPatched( Gia_Man_t *pOut, Gia_Man_t *pSpec, Gia_Man_t *pPatch );
extern Gia_Man_t* Bnd_ManGenPatched1( Gia_Man_t *pOut, Gia_Man_t *pSpec );
extern Gia_Man_t* Bnd_ManGenPatched2( Gia_Man_t *pImpl, Gia_Man_t *pPatch, int fSkiptStrash, int fVerbose );
extern void Bnd_ManSetEqOut( int eq ); extern void Bnd_ManSetEqOut( int eq );
extern void Bnd_ManSetEqRes( int eq ); extern void Bnd_ManSetEqRes( int eq );
extern void Bnd_ManPrintStats(); extern void Bnd_ManPrintStats();

281
src/aig/gia/giaBound.c
View File

@ -29,6 +29,7 @@ struct Bnd_Man_t_
int nNode_patched; int nNode_patched;
int status; // 0: init 1: boundary found 2: out generated 3: patched generated int status; // 0: init 1: boundary found 2: out generated 3: patched generated
int fVerbose;
int combLoop_spec; int combLoop_spec;
int combLoop_impl; int combLoop_impl;
@ -57,7 +58,7 @@ struct Bnd_Man_t_
}; };
Bnd_Man_t* pBnd; Bnd_Man_t* pBnd = 0;
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS /// /// FUNCTION DEFINITIONS ///
@ -78,7 +79,7 @@ void Bnd_ManSetEqRes( int eq ) { pBnd -> eq_res = eq;}
***********************************************************************/ ***********************************************************************/
Bnd_Man_t* Bnd_ManStart( Gia_Man_t *pSpec, Gia_Man_t *pImpl ) Bnd_Man_t* Bnd_ManStart( Gia_Man_t *pSpec, Gia_Man_t *pImpl, int fVerbose )
{ {
int i; int i;
Bnd_Man_t* p = ABC_CALLOC( Bnd_Man_t, 1 ); Bnd_Man_t* p = ABC_CALLOC( Bnd_Man_t, 1 );
@ -113,6 +114,8 @@ Bnd_Man_t* Bnd_ManStart( Gia_Man_t *pSpec, Gia_Man_t *pImpl )
p -> nNode_patched = 0; p -> nNode_patched = 0;
p -> status = 0; p -> status = 0;
p -> fVerbose = fVerbose;
p -> combLoop_spec = 0; p -> combLoop_spec = 0;
p -> combLoop_impl = 0; p -> combLoop_impl = 0;
p -> eq_out = 0; p -> eq_out = 0;
@ -166,6 +169,8 @@ void Bnd_ManStop()
ABC_FREE( pBnd ); ABC_FREE( pBnd );
} }
int Bnd_ManGetNInternal() { assert(pBnd); return pBnd -> nInternal; }
int Bnd_ManGetNExtra() { assert(pBnd); return pBnd -> nExtra; }
void Bnd_ManMap( int iLit, int id, int spec ) void Bnd_ManMap( int iLit, int id, int spec )
{ {
@ -370,23 +375,22 @@ void Bnd_ManPrintStats()
Description [check if the given boundary is valid. Return 0 if Description [check if the given boundary is valid. Return 0 if
the boundary is invalid. Return k if the boundary is valid and the boundary is invalid. Return k if the boundary is valid and
there're k boundary inputs. ] there're k boundary inputs.
Can be called even if Bnd_Man_t is not created]
SideEffects [] SideEffects []
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Bnd_ManCheckBound( Gia_Man_t * p ) int Bnd_ManCheckBound( Gia_Man_t * p, int fVerbose )
{ {
int i; int i;
Gia_Obj_t *pObj; Gia_Obj_t *pObj;
int valid = 1; int valid = 1;
pBnd -> nBI = 0; int nBI = 0, nBO = 0, nInternal = 0;
pBnd -> nBO = 0;
pBnd -> nInternal = 0;
printf( "Checking boundary... \n"); if ( fVerbose ) printf( "Checking boundary... \n");
Vec_Int_t *vPath; Vec_Int_t *vPath;
vPath = Vec_IntAlloc( Gia_ManObjNum(p) ); vPath = Vec_IntAlloc( Gia_ManObjNum(p) );
@ -417,7 +421,7 @@ int Bnd_ManCheckBound( Gia_Man_t * p )
if ( path == 1 ) // boundary input if ( path == 1 ) // boundary input
{ {
// TODO: record BIs here since they may not be in the first n buffers // TODO: record BIs here since they may not be in the first n buffers
pBnd -> nBO ++; nBO ++;
} }
} }
else if ( Gia_ObjFaninNum( p, pObj ) >= 1 ) else if ( Gia_ObjFaninNum( p, pObj ) >= 1 )
@ -431,7 +435,7 @@ int Bnd_ManCheckBound( Gia_Man_t * p )
if ( path == 2 ) // inside boundary if ( path == 2 ) // inside boundary
{ {
// TODO: record BIs here since they may not be in the first n buffers // TODO: record BIs here since they may not be in the first n buffers
pBnd -> nInternal ++; nInternal ++;
} }
} }
else // PI or const, check validity else // PI or const, check validity
@ -445,20 +449,33 @@ int Bnd_ManCheckBound( Gia_Man_t * p )
} }
} }
pBnd -> nBI = Gia_ManBufNum(p) - pBnd -> nBO; nBI = Gia_ManBufNum(p) - nBO;
if ( !valid ) if ( !valid )
{ {
printf("invalid boundary\n"); printf("invalid boundary\n");
return 0; return 0;
} }
else if ( nBI == 0 )
{
printf("no boundary\n");
return 0;
}
else else
{ {
printf("valid boundary ("); if ( fVerbose )
printf("#BI = %d\t#BO = %d\t", pBnd -> nBI, Gia_ManBufNum(p)- pBnd -> nBI); {
printf("#Internal = %d)\n", pBnd -> nInternal ); printf("valid boundary (");
assert( pBnd -> nBI > 0 ); printf("#BI = %d\t#BO = %d\t", nBI, Gia_ManBufNum(p)- nBI);
return pBnd -> nBI; printf("#Internal = %d)\n", nInternal );
}
if ( pBnd )
{
pBnd -> nBI = nBI;
pBnd -> nBO = nBO;
pBnd -> nInternal = nInternal;
}
return nBI;
} }
} }
@ -572,7 +589,7 @@ void Bnd_ManFindBound( Gia_Man_t * p )
{ {
if ( cnt < pBnd -> nBI ) if ( cnt < pBnd -> nBI )
{ {
Vec_IntPush( vBI, Gia_ObjId(p, pObj) ); Vec_IntPush( vBI, Gia_ObjId(p, Gia_ObjFanin0(pObj) ) );
} }
else else
{ {
@ -593,7 +610,7 @@ void Bnd_ManFindBound( Gia_Man_t * p )
Vec_IntPush(vEO_spec, id); Vec_IntPush(vEO_spec, id);
} }
} }
printf("%d BO doesn't match. ", Vec_PtrSize(vQ) ); if ( pBnd -> fVerbose ) printf("%d BO doesn't match. ", Vec_PtrSize(vQ) );
pBnd -> nBO_miss = Vec_PtrSize(vQ); pBnd -> nBO_miss = Vec_PtrSize(vQ);
int cnt_extra = - Vec_PtrSize(vQ); int cnt_extra = - Vec_PtrSize(vQ);
@ -622,7 +639,7 @@ void Bnd_ManFindBound( Gia_Man_t * p )
} }
} }
// printf("%d AO found with %d extra nodes\n", Vec_IntSize(vAO) , cnt_extra ); // printf("%d AO found with %d extra nodes\n", Vec_IntSize(vAO) , cnt_extra );
printf("%d AO found\n", Vec_IntSize(vAO) ); if ( pBnd -> fVerbose ) printf("%d AO found\n", Vec_IntSize(vAO) );
// mark TFOC of BO with flag 1 to prevent them from being selected into EI // mark TFOC of BO with flag 1 to prevent them from being selected into EI
@ -665,7 +682,7 @@ void Bnd_ManFindBound( Gia_Man_t * p )
Vec_IntPush(vEI_spec, id); Vec_IntPush(vEI_spec, id);
} }
} }
printf("%d BI doesn't match. ", Vec_PtrSize(vQ) ); if ( pBnd -> fVerbose ) printf("%d BI doesn't match. ", Vec_PtrSize(vQ) );
pBnd -> nBI_miss = Vec_PtrSize(vQ); pBnd -> nBI_miss = Vec_PtrSize(vQ);
cnt_extra -= Vec_PtrSize(vQ); cnt_extra -= Vec_PtrSize(vQ);
@ -708,7 +725,7 @@ void Bnd_ManFindBound( Gia_Man_t * p )
Vec_IntSetEntry( vFlag, id, 2 ); Vec_IntSetEntry( vFlag, id, 2 );
} }
printf("%d AI found with %d extra nodes in total\n", Vec_IntSize(vAI) , cnt_extra ); if ( pBnd -> fVerbose ) printf("%d AI found with %d extra nodes in total\n", Vec_IntSize(vAI) , cnt_extra );
pBnd -> nExtra = cnt_extra; pBnd -> nExtra = cnt_extra;
@ -738,8 +755,11 @@ void Bnd_ManFindBound( Gia_Man_t * p )
// print // print
pBnd -> status = 1; pBnd -> status = 1;
printf("#EI = %d\t#EO = %d\t#Extra Node = %d\n", Vec_IntSize(vEI_spec) , Vec_IntSize(vEO_spec), cnt_extra ); if ( pBnd -> fVerbose )
Bnd_ManPrintBound(); {
printf("#EI = %d\t#EO = %d\t#Extra Node = %d\n", Vec_IntSize(vEI_spec) , Vec_IntSize(vEO_spec), cnt_extra );
Bnd_ManPrintBound();
}
// check boundary has comb loop // check boundary has comb loop
if ( !Bnd_ManCheckExtBound( p, vEI_spec, vEO_spec ) ) if ( !Bnd_ManCheckExtBound( p, vEI_spec, vEO_spec ) )
@ -869,42 +889,47 @@ Gia_Man_t* Bnd_ManCutBoundary( Gia_Man_t *p, Vec_Int_t* vEI, Vec_Int_t* vEO, Vec
} }
Gia_Man_t* Bnd_ManGenSpecOut( Gia_Man_t* p ) Gia_Man_t* Bnd_ManGenSpecOut( Gia_Man_t* p )
{ {
printf("Generating spec_out with given boundary.\n"); if ( pBnd -> fVerbose ) printf("Generating spec_out with given boundary.\n");
Gia_Man_t *pNew = Bnd_ManCutBoundary( p, pBnd->vEI_spec, pBnd->vEO_spec, 0, 0 ); Gia_Man_t *pNew = Bnd_ManCutBoundary( p, pBnd->vEI_spec, pBnd->vEO_spec, 0, 0 );
return pNew; return pNew;
} }
Gia_Man_t* Bnd_ManGenImplOut( Gia_Man_t* p ) Gia_Man_t* Bnd_ManGenImplOut( Gia_Man_t* p)
{ {
printf("Generating impl_out with given boundary.\n"); if ( pBnd -> fVerbose ) printf("Generating impl_out with given boundary.\n");
Gia_Man_t *pNew = Bnd_ManCutBoundary( p, pBnd->vEI_impl, pBnd->vEO_impl, pBnd->vEI_phase, pBnd->vEO_phase ); Gia_Man_t *pNew = Bnd_ManCutBoundary( p, pBnd->vEI_impl, pBnd->vEO_impl, pBnd->vEI_phase, pBnd->vEO_phase );
if ( pNew ) pBnd -> status = 2; if ( pNew ) pBnd -> status = 2;
else pBnd -> combLoop_impl = 1; else pBnd -> combLoop_impl = 1;
return pNew; return pNew;
} }
void Bnd_AddNodeRec( Gia_Man_t *p, Gia_Man_t *pNew, Gia_Obj_t *pObj ) void Bnd_AddNodeRec( Gia_Man_t *p, Gia_Man_t *pNew, Gia_Obj_t *pObj, int fSkipStrash )
{ {
// TODO does this mean constant zero node? // TODO does this mean constant zero node?
if ( pObj -> Value != ~0 ) return; if ( pObj -> Value != ~0 ) return;
for( int i = 0; i < Gia_ObjFaninNum(p, pObj); i++ ) for( int i = 0; i < Gia_ObjFaninNum(p, pObj); i++ )
{ {
Bnd_AddNodeRec( p, pNew, Gia_ObjFanin(pObj, i) ); Bnd_AddNodeRec( p, pNew, Gia_ObjFanin(pObj, i), fSkipStrash );
} }
if ( Gia_ObjIsAnd(pObj) ) if ( Gia_ObjIsAnd(pObj) )
{ {
pObj -> Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); if ( fSkipStrash )
{
if ( Gia_ObjIsBuf(pObj) ) pObj -> Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) );
else pObj -> Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
}
else
{
pObj -> Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
}
} }
else else
{ {
if ( Gia_ObjIsCi(pObj) )
{
printf("Ci with value 0 encountered (id = %d)\n", Gia_ObjId(p, pObj) );
}
assert( Gia_ObjIsCo(pObj) ); assert( Gia_ObjIsCo(pObj) );
// if ( Gia_ObjIsCi(pObj) ) printf("Ci with value ~0 encountered (id = %d)\n", Gia_ObjId(p, pObj) );
pObj -> Value = Gia_ObjFanin0Copy(pObj); pObj -> Value = Gia_ObjFanin0Copy(pObj);
} }
} }
@ -963,7 +988,7 @@ Gia_Man_t* Bnd_ManGenPatched( Gia_Man_t *pOut, Gia_Man_t *pSpec, Gia_Man_t *pPat
for ( i = 0; i < Vec_IntSize( pBnd -> vEI_spec ); i++ ) for ( i = 0; i < Vec_IntSize( pBnd -> vEI_spec ); i++ )
{ {
pObj = Gia_ManCo(pOut, i + Gia_ManCoNum(pSpec) ); pObj = Gia_ManCo(pOut, i + Gia_ManCoNum(pSpec) );
Bnd_AddNodeRec( pOut, pNew, pObj ); Bnd_AddNodeRec( pOut, pNew, pObj, 0 );
// set Spec EI // set Spec EI
Gia_ManObj( pSpec, Vec_IntEntry(pBnd -> vEI_spec, i) ) -> Value = pObj -> Value; Gia_ManObj( pSpec, Vec_IntEntry(pBnd -> vEI_spec, i) ) -> Value = pObj -> Value;
@ -976,7 +1001,7 @@ Gia_Man_t* Bnd_ManGenPatched( Gia_Man_t *pOut, Gia_Man_t *pSpec, Gia_Man_t *pPat
Vec_IntForEachEntry( pBnd -> vBI, id, i ) Vec_IntForEachEntry( pBnd -> vBI, id, i )
{ {
pObj = Gia_ManObj( pSpec, id ); pObj = Gia_ManObj( pSpec, id );
Bnd_AddNodeRec( pSpec, pNew, pObj ); Bnd_AddNodeRec( pSpec, pNew, pObj, 0 );
// set patch bi // set patch bi
Gia_ManObj( pPatch, Vec_IntEntry( vBI_patch, i) ) -> Value = pObj -> Value; Gia_ManObj( pPatch, Vec_IntEntry( vBI_patch, i) ) -> Value = pObj -> Value;
@ -989,7 +1014,7 @@ Gia_Man_t* Bnd_ManGenPatched( Gia_Man_t *pOut, Gia_Man_t *pSpec, Gia_Man_t *pPat
Vec_IntForEachEntry( vBO_patch, id, i ) Vec_IntForEachEntry( vBO_patch, id, i )
{ {
pObj = Gia_ManObj( pPatch, id ); pObj = Gia_ManObj( pPatch, id );
Bnd_AddNodeRec( pPatch, pNew, pObj ); Bnd_AddNodeRec( pPatch, pNew, pObj, 0 );
// set spec bo // set spec bo
Gia_ManObj( pSpec, Vec_IntEntry( pBnd -> vBO, i) ) -> Value = pObj -> Value; Gia_ManObj( pSpec, Vec_IntEntry( pBnd -> vBO, i) ) -> Value = pObj -> Value;
@ -1002,7 +1027,7 @@ Gia_Man_t* Bnd_ManGenPatched( Gia_Man_t *pOut, Gia_Man_t *pSpec, Gia_Man_t *pPat
Vec_IntForEachEntry( pBnd -> vEO_spec, id, i ) Vec_IntForEachEntry( pBnd -> vEO_spec, id, i )
{ {
pObj = Gia_ManObj( pSpec, id ); pObj = Gia_ManObj( pSpec, id );
Bnd_AddNodeRec( pSpec, pNew, pObj ); Bnd_AddNodeRec( pSpec, pNew, pObj, 0 );
// set impl EO (PI) // set impl EO (PI)
Gia_ManCi( pOut, i + Gia_ManCiNum(pSpec) ) -> Value = pObj -> Value; Gia_ManCi( pOut, i + Gia_ManCiNum(pSpec) ) -> Value = pObj -> Value;
@ -1015,7 +1040,7 @@ Gia_Man_t* Bnd_ManGenPatched( Gia_Man_t *pOut, Gia_Man_t *pSpec, Gia_Man_t *pPat
for ( i = 0; i < Gia_ManCoNum(pSpec); i++ ) for ( i = 0; i < Gia_ManCoNum(pSpec); i++ )
{ {
pObj = Gia_ManCo( pOut, i ); pObj = Gia_ManCo( pOut, i );
Bnd_AddNodeRec( pOut, pNew, pObj ); Bnd_AddNodeRec( pOut, pNew, pObj, 0 );
Gia_ManAppendCo( pNew, pObj->Value ); Gia_ManAppendCo( pNew, pObj->Value );
// printf(" %d",pObj -> Value); // printf(" %d",pObj -> Value);
} }
@ -1036,8 +1061,186 @@ Gia_Man_t* Bnd_ManGenPatched( Gia_Man_t *pOut, Gia_Man_t *pSpec, Gia_Man_t *pPat
return pNew; return pNew;
} }
Gia_Man_t* Bnd_ManGenPatched1( Gia_Man_t *pOut, Gia_Man_t *pSpec )
{
Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj;
int i, id;
pNew = Gia_ManStart( Gia_ManObjNum(pOut) + Gia_ManObjNum( pSpec ) );
pNew -> pName = ABC_ALLOC( char, strlen(pOut->pName)+3);
sprintf( pNew -> pName, "%s_p", pOut -> pName );
Gia_ManFillValue(pOut);
Gia_ManFillValue(pSpec);
Gia_ManConst0(pOut)->Value = 0;
Gia_ManConst0(pSpec)->Value = 0;
// add Impl (real) PI
for ( i = 0; i < Gia_ManCiNum(pSpec); i++ )
{
pObj = Gia_ManCi(pOut, i);
pObj -> Value = Gia_ManAppendCi( pNew );
}
// add Impl EI to CI
// printf("adding EI to CI in Impl\n");
for ( i = 0; i < Vec_IntSize( pBnd -> vEI_spec ); i++ )
{
pObj = Gia_ManCo(pOut, i + Gia_ManCoNum(pSpec) );
Bnd_AddNodeRec( pOut, pNew, pObj, 1 );
// set Spec EI
Gia_ManObj( pSpec, Vec_IntEntry(pBnd -> vEI_spec, i) ) -> Value = pObj -> Value;
// printf(" %d",pObj -> Value);
}
// printf("\n");
// add Spec EO to EI
// add BI -> BO -> EO to maintain the order of bufs
// Vec_IntForEachEntry( pBnd -> vBI, id, i )
// {
// pObj = Gia_ManObj( pSpec, id );
// Bnd_AddNodeRec( pSpec, pNew, pObj, 1 );
// }
// Vec_IntForEachEntry( pBnd -> vBO, id, i )
// {
// pObj = Gia_ManObj( pSpec, id );
// Bnd_AddNodeRec( pSpec, pNew, pObj, 1 );
// }
Gia_ManForEachBuf( pSpec, pObj, i )
{
Bnd_AddNodeRec( pSpec, pNew, pObj, 1 );
}
Vec_IntForEachEntry( pBnd -> vEO_spec, id, i )
{
pObj = Gia_ManObj( pSpec, id );
Bnd_AddNodeRec( pSpec, pNew, pObj, 1 );
// set impl EO (PI)
Gia_ManCi( pOut, i + Gia_ManCiNum(pSpec) ) -> Value = pObj -> Value;
// printf(" %d",pObj -> Value);
}
// printf("\n");
// add Impl (real) PO to EO
// printf("adding CO to EO in Impl\n");
for ( i = 0; i < Gia_ManCoNum(pSpec); i++ )
{
pObj = Gia_ManCo( pOut, i );
Bnd_AddNodeRec( pOut, pNew, pObj, 1 );
Gia_ManAppendCo( pNew, pObj->Value );
// printf(" %d",pObj -> Value);
}
// printf("\n");
// clean up
pNew = Gia_ManCleanup( pTemp = pNew );
Gia_ManStop( pTemp );
pBnd -> nNode_patched = Gia_ManAndNum( pNew );
pBnd -> status = 3;
return pNew;
}
Gia_Man_t* Bnd_ManGenPatched2( Gia_Man_t *pImpl, Gia_Man_t *pPatch, int fSkipStrash, int fVerbose )
{
Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj;
int i, nBI, nBI_patch, cnt;
Vec_Int_t* vLit;
// check boundary first
nBI = Bnd_ManCheckBound( pImpl, fVerbose );
nBI_patch = Bnd_ManCheckBound( pPatch, fVerbose );
if ( 0 == nBI_patch || Gia_ManBufNum(pImpl) != Gia_ManBufNum(pPatch) || nBI != nBI_patch )
{
Abc_Print( -1, "Abc_CommandAbc9StrEco(): The given boundary is invalid.\n" );
return 0;
}
// prepare new network
pNew = Gia_ManStart( Gia_ManObjNum(pImpl) + Gia_ManObjNum( pPatch ) );
pNew -> pName = ABC_ALLOC( char, strlen(pImpl->pName)+3);
sprintf( pNew -> pName, "%s_p", pImpl -> pName );
if ( !fSkipStrash )
{
Gia_ManHashAlloc( pNew );
}
Gia_ManFillValue(pImpl);
Gia_ManFillValue(pPatch);
Gia_ManConst0(pImpl)->Value = 0;
Gia_ManConst0(pPatch)->Value = 0;
vLit = Vec_IntAlloc( Gia_ManBufNum(pImpl) );
// add Impl (real) CI
Gia_ManForEachCi( pImpl, pObj, i )
{
pObj -> Value = Gia_ManAppendCi( pNew );
}
// add Impl BI to CI
cnt = 0;
Gia_ManForEachBuf( pImpl, pObj, i )
{
Bnd_AddNodeRec( pImpl, pNew, pObj, fSkipStrash );
Vec_IntPush( vLit, pObj -> Value );
cnt ++;
if ( cnt >= nBI ) break;
}
// set BI in patch
// add patch BO to BI
cnt = 0;
Gia_ManForEachBuf( pPatch, pObj, i )
{
if ( cnt < nBI )
{
pObj -> Value = Vec_IntEntry( vLit, cnt );
}
else
{
Bnd_AddNodeRec( pPatch, pNew, pObj, fSkipStrash );
Vec_IntPush( vLit, pObj -> Value );
}
cnt ++;
if ( cnt == nBI ) Vec_IntClear( vLit );
}
// set BO in impl
cnt = 0;
Gia_ManForEachBuf( pImpl, pObj, i )
{
cnt ++;
if ( cnt <= nBI) continue;
pObj -> Value = Vec_IntEntry( vLit, cnt-nBI-1 );
}
// add impl CO to BO
Gia_ManForEachCo( pImpl, pObj, i )
{
Bnd_AddNodeRec( pImpl, pNew, pObj, fSkipStrash );
Gia_ManAppendCo( pNew, pObj -> Value );
}
// clean up
if ( !fSkipStrash )
{
Gia_ManHashStop( pNew );
}
Vec_IntFree( vLit );
pNew = Gia_ManCleanup( pTemp = pNew );
Gia_ManStop( pTemp );
return pNew;
}
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////

309
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_CommandAbc9AddFlop ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9BMiter ( 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_CommandAbc9GenHie ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9BRecover ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9StrEco ( 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 ); static int Abc_CommandAbc9Test ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -1381,6 +1382,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&addflop", Abc_CommandAbc9AddFlop, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&addflop", Abc_CommandAbc9AddFlop, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&bmiter", Abc_CommandAbc9BMiter, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&bmiter", Abc_CommandAbc9BMiter, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&gen_hie", Abc_CommandAbc9GenHie, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&gen_hie", Abc_CommandAbc9GenHie, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&brecover", Abc_CommandAbc9BRecover, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&str_eco", Abc_CommandAbc9StrEco, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&str_eco", Abc_CommandAbc9StrEco, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&test", Abc_CommandAbc9Test, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&test", Abc_CommandAbc9Test, 0 );
@ -52092,12 +52094,12 @@ usage:
***********************************************************************/ ***********************************************************************/
extern Bnd_Man_t* pBnd; extern Bnd_Man_t* pBnd;
int Abc_CommandAbc9StrEco( Abc_Frame_t * pAbc, int argc, char ** argv ) int Abc_CommandAbc9BRecover( Abc_Frame_t * pAbc, int argc, char ** argv )
{ {
extern Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars ); extern Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars );
extern void Cec4_ManSetParams( 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 ); 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;; Gia_Man_t *pSpec, *pImpl_out = 0, *pSpec_out = 0, *pMiter, *pPatched = 0, *pTemp, *pBmiter;
char * FileName = NULL; char * FileName = NULL;
FILE * pFile = NULL; FILE * pFile = NULL;
int c, fVerbose = 0, success = 1; int c, fVerbose = 0, success = 1;
@ -52111,8 +52113,6 @@ int Abc_CommandAbc9StrEco( Abc_Frame_t * pAbc, int argc, char ** argv )
Cec4_ManSetParams( pParsFra ); Cec4_ManSetParams( pParsFra );
pParsFra -> fBMiterInfo = 1; pParsFra -> fBMiterInfo = 1;
// TODO: save return value and return at the end of the function
// parse options // parse options
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
@ -52130,17 +52130,17 @@ int Abc_CommandAbc9StrEco( Abc_Frame_t * pAbc, int argc, char ** argv )
} }
if ( pAbc->pGia == NULL ) if ( pAbc->pGia == NULL )
{ {
Abc_Print( -1, "Abc_CommandAbc9StrEco(): There is no AIG.\n" ); Abc_Print( -1, "Abc_CommandAbc9BRecover(): There is no AIG.\n" );
return 0; return 0;
} }
if ( argc != globalUtilOptind + 2 ) if ( argc != globalUtilOptind + 1 )
{ {
printf("%d\n", argc-globalUtilOptind); printf("%d\n", argc-globalUtilOptind);
Abc_Print( -1, "Abc_CommandAbc9StrEco(): AIG should be given on the command line.\n" ); Abc_Print( -1, "Abc_CommandAbc9BRecover(): AIG should be given on the command line.\n" );
return 0; return 0;
} }
// read impl // read spec
FileName = argv[globalUtilOptind]; FileName = argv[globalUtilOptind];
if ( (pFile = fopen( FileName, "r" )) == NULL ) if ( (pFile = fopen( FileName, "r" )) == NULL )
{ {
@ -52151,15 +52151,198 @@ int Abc_CommandAbc9StrEco( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1; return 1;
} }
fclose( pFile ); fclose( pFile );
pImpl = Gia_AigerRead( FileName, 0, 0, 0 ); pSpec = Gia_AigerRead( FileName, 0, 1, 0 );
if ( pImpl == NULL ) if ( pSpec == NULL )
{ {
Abc_Print( -1, "Abc_CommandAbc9StrEco(): Cannot read the file name on the command line.\n" ); Abc_Print( -1, "Abc_CommandAbc9BRecover(): Cannot read the file name on the command line.\n" );
return 0;
}
if ( Gia_ManBufNum(pSpec) == 0 )
{
Abc_Print( -1, "Abc_CommandAbc9BRecover(): The given spec should be hierarchical.\n" );
Gia_ManStop(pSpec);
return 0;
}
// start boundary manager
pBnd = Bnd_ManStart( pSpec, pAbc->pGia, fVerbose );
// verify if spec eq impl
pMiter = Gia_ManMiter( pAbc->pGia, pSpec, 0, 1, 0, 0, 0 );
if ( !Cec_ManVerify( pMiter, pParsCec ) )
{
Abc_Print( -1, "Abc_CommandAbc9BRecover(): The given spec is not equivalent to current impl.\n" );
success = 0;
}
Gia_ManStop(pMiter);
// check boundary
if ( success )
{
if ( 0 == Bnd_ManCheckBound( pSpec, fVerbose ) )
{
Abc_Print( -1, "Abc_CommandAbc9BRecover(): The given spec has invalid boundary.\n" );
success = 0;
}
}
if ( success )
{
// create bmiter, run fraig, record mapping
pBmiter = Gia_ManBoundaryMiter( pSpec, pAbc->pGia, 0 );
pTemp = Cec4_ManSimulateTest( pBmiter, pParsFra );
Gia_ManStop(pBmiter);
Gia_ManStop(pTemp);
// find
Bnd_ManFindBound( pSpec );
// create spec_out and
pSpec_out = Bnd_ManGenSpecOut( pSpec );
if ( !pSpec_out ) success = 0;
pImpl_out = Bnd_ManGenImplOut( pAbc->pGia );
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 )
{
printf("Abc_CommandAbc9BRecover(): The generated boundary is invalid. The circuit is not changed.\n");
}
else
{
// check if spec_out and imnpl_out are equivalent
if ( fVerbose )
{
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
if ( fVerbose ) printf("Generating patched impl\n");
pPatched = Bnd_ManGenPatched1( pImpl_out, pSpec );
// // 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 spec
if ( fVerbose ) printf("Checking the equivalence of patched impl and spec\n");
pMiter = Gia_ManMiter( pSpec, pPatched, 0, 1, 0, 0, 0 );
success = Cec_ManVerify( pMiter, pParsCec );
Bnd_ManSetEqRes( success );
if ( !success )
{
printf("Failed. The generated AIG is not equivalent.\n");
}
Gia_ManStop( pMiter );
}
if ( fVerbose ) Bnd_ManPrintStats();
Gia_ManStop( pSpec );
if ( pSpec_out ) Gia_ManStop( pSpec_out );
if ( pImpl_out ) Gia_ManStop( pImpl_out );
if ( success )
{
printf("Success. The generated hierarchical impl is equivalent. (box size: %d -> %d)\n", Bnd_ManGetNInternal(), Bnd_ManGetNInternal() + Bnd_ManGetNExtra() );
}
if (pPatched) Abc_FrameUpdateGia( pAbc, pPatched );
Bnd_ManStop();
return 0;
usage:
Abc_Print( -2, "usage: &brecover -I <biNum> [-vh] <impl> <patch>\n" );
Abc_Print( -2, "\t recover boundary using SAT-Sweeping\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*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
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 );
Gia_Man_t *pMiter, *pPatch, *pPatched;
char * FileName = NULL;
FILE * pFile = NULL;
int c, success = 1;
int fVerbose = 0, fSkipStrash = 0;
// 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;
// parse options
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "vsh" ) ) != EOF )
{
switch ( c )
{
case 'v':
fVerbose ^= 1;
break;
case 's':
fSkipStrash ^= 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 + 1 )
{
printf("%d\n", argc-globalUtilOptind);
Abc_Print( -1, "Abc_CommandAbc9StrEco(): AIG should be given on the command line.\n" );
return 0; return 0;
} }
// read patch // read patch
FileName = argv[globalUtilOptind+1]; FileName = argv[globalUtilOptind];
if ( (pFile = fopen( FileName, "r" )) == NULL ) if ( (pFile = fopen( FileName, "r" )) == NULL )
{ {
Abc_Print( -1, "Cannot open input file \"%s\". ", FileName ); Abc_Print( -1, "Cannot open input file \"%s\". ", FileName );
@ -52176,98 +52359,29 @@ int Abc_CommandAbc9StrEco( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0; return 0;
} }
// start boundary manager // generate patched impl
pBnd = Bnd_ManStart( pAbc->pGia, pImpl ); if ( fVerbose ) printf("Generating patched impl\n");
pPatched = Bnd_ManGenPatched2( pAbc->pGia, pPatch, fSkipStrash, fVerbose );
// verify if spec eq impl if ( pPatched )
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 // check if patched is equiv to patch
printf("Checking the equivalence of patched impl and patch\n"); if ( fVerbose ) printf("Checking the equivalence of patched impl and patch\n");
pMiter = Gia_ManMiter( pPatch, pPatched, 0, 1, 0, 0, 0 ); pMiter = Gia_ManMiter( pPatch, pPatched, 0, 1, 0, 0, 0 );
Bnd_ManSetEqRes( Cec_ManVerify( pMiter, pParsCec ) ); success = Cec_ManVerify( pMiter, pParsCec );
if( !success )
{
printf("Failed. The patched circuit is not equivalent.\n");
}
Gia_ManStop( pMiter ); 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 ); Abc_FrameUpdateGia( pAbc, pPatched );
} }
Bnd_ManStop();
Gia_ManStop( pPatch );
if ( success )
{
printf("Success. The patched circuit is equivalent.\n");
}
return 0; return 0;
@ -52275,6 +52389,7 @@ usage:
Abc_Print( -2, "usage: &str_eco -I <biNum> [-vh] <impl> <patch>\n" ); 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 SAT-sweeping-based ECO\n" );
Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-s : toggles skipping structural hash [default = %s]\n", fSkipStrash? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n"); 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<impl> : the implementation aig. (should be equivalent to spec)\n");
Abc_Print( -2, "\t<patch> : the modified spec. (should be a hierarchical AIG)\n"); Abc_Print( -2, "\t<patch> : the modified spec. (should be a hierarchical AIG)\n");

2
src/sat/bsat2/Options.cpp
View File

@ -45,10 +45,12 @@ int Minisat::parseOptions(int& argc, char** argv, bool strict)
} }
if (!parsed_ok) if (!parsed_ok)
{
if (strict && match(argv[i], "-")) if (strict && match(argv[i], "-"))
{ fprintf(stderr, "ERROR! Unknown flag \"%s\". Use '--%shelp' for help.\n", argv[i], Option::getHelpPrefixString()); return 0; } // exit(0); { fprintf(stderr, "ERROR! Unknown flag \"%s\". Use '--%shelp' for help.\n", argv[i], Option::getHelpPrefixString()); return 0; } // exit(0);
else else
argv[j++] = argv[i]; argv[j++] = argv[i];
}
} }
} }

2
src/sat/bsat2/Options.h
View File

@ -62,7 +62,7 @@ class Option
struct OptionLt { struct OptionLt {
bool operator()(const Option* x, const Option* y) { bool operator()(const Option* x, const Option* y) {
int test1 = strcmp(x->category, y->category); int test1 = strcmp(x->category, y->category);
return test1 < 0 || test1 == 0 && strcmp(x->type_name, y->type_name) < 0; return test1 < 0 || ( test1 == 0 && strcmp(x->type_name, y->type_name) < 0 );
} }
}; };

4
src/sat/bsat2/SimpSolver.cpp
View File

@ -230,10 +230,12 @@ bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& ou
if (var(qs[i]) != v){ if (var(qs[i]) != v){
for (j = 0; j < ps.size(); j++) for (j = 0; j < ps.size(); j++)
if (var(ps[j]) == var(qs[i])) if (var(ps[j]) == var(qs[i]))
{
if (ps[j] == ~qs[i]) if (ps[j] == ~qs[i])
return false; return false;
else else
goto next; goto next;
}
out_clause.push(qs[i]); out_clause.push(qs[i]);
} }
next:; next:;
@ -264,10 +266,12 @@ bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, int& size)
if (var(__qs[i]) != v){ if (var(__qs[i]) != v){
for (int j = 0; j < ps.size(); j++) for (int j = 0; j < ps.size(); j++)
if (var(__ps[j]) == var(__qs[i])) if (var(__ps[j]) == var(__qs[i]))
{
if (__ps[j] == ~__qs[i]) if (__ps[j] == ~__qs[i])
return false; return false;
else else
goto next; goto next;
}
size++; size++;
} }
next:; next:;

4
src/sat/bsat2/Solver.cpp
View File

@ -211,7 +211,7 @@ void Solver::cancelUntil(int level) {
for (int c = trail.size()-1; c >= trail_lim[level]; c--){ for (int c = trail.size()-1; c >= trail_lim[level]; c--){
Var x = var(trail[c]); Var x = var(trail[c]);
assigns [x] = l_Undef; assigns [x] = l_Undef;
if (phase_saving > 1 || (phase_saving == 1) && c > trail_lim.last()) if (phase_saving > 1 || ((phase_saving == 1) && c > trail_lim.last()))
polarity[x] = sign(trail[c]); polarity[x] = sign(trail[c]);
insertVarOrder(x); } insertVarOrder(x); }
qhead = trail_lim[level]; qhead = trail_lim[level];
@ -659,7 +659,7 @@ lbool Solver::search(int nof_conflicts)
}else{ }else{
// NO CONFLICT // NO CONFLICT
if (nof_conflicts >= 0 && conflictC >= nof_conflicts || !withinBudget()){ if ( (nof_conflicts >= 0 && conflictC >= nof_conflicts) || !withinBudget()){
// Reached bound on number of conflicts: // Reached bound on number of conflicts:
progress_estimate = progressEstimate(); progress_estimate = progressEstimate();
cancelUntil(0); cancelUntil(0);

1
src/sat/bsat2/Vec.h
View File

@ -93,7 +93,6 @@ public:
void moveTo(vec<T>& dest) { dest.clear(true); dest.data = data; dest.sz = sz; dest.cap = cap; data = NULL; sz = 0; cap = 0; } void moveTo(vec<T>& dest) { dest.clear(true); dest.data = data; dest.sz = sz; dest.cap = cap; data = NULL; sz = 0; cap = 0; }
}; };
template<class T> template<class T>
void vec<T>::capacity(int min_cap) { void vec<T>::capacity(int min_cap) {
if (cap >= min_cap) return; if (cap >= min_cap) return;