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

extend bo

This commit is contained in:
Allen Ho 2023-12-07 19:07:52 +08:00
parent a316847341
commit 9bb5333f62
5 changed files with 157 additions and 193 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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"

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

@ -31,6 +31,8 @@ ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
Vec_Int_t* vLitBmiter;
Vec_Int_t* vIdBI;
Vec_Int_t* vIdBO;
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
@ -5728,6 +5730,11 @@ Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose,
int c1 = 0;
int c2 = 0;
int count;
int val;
vIdBI = Vec_IntAlloc(16);
vIdBO = Vec_IntAlloc(16);
Gia_ManForEachBuf( p1, pObj, i )
{
if ( count < n )
@ -5782,6 +5789,7 @@ Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose,
// TODO: record hashed equivalent nodes
count = 0;
Gia_ManForEachAnd( p1, pObj, i ) {
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
if ( Vec_IntEntry( vTypeSpec, Gia_ObjId( p1, pObj) ) > 0 )
@ -5796,7 +5804,18 @@ Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose,
}
}
if ( Gia_ObjIsBuf(pObj) )
{
Vec_IntPush( vLits, pObj->Value );
if ( count < n )
{
Vec_IntPush( vIdBI, (pObj->Value) >> 1 );
}
else
{
Vec_IntPush( vIdBO, (pObj->Value) >> 1 );
}
count ++;
}
}

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

@ -37921,7 +37921,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, "JWRILDCNPMrmdckngxysopwqvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "OJWRILDCNPMrmdckngxysopwqvh" ) ) != EOF )
{
switch ( c )
{
@ -37969,6 +37969,18 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nItersMax < 0 )
goto usage;
break;
case 'O':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-O\" should be followed by an integer.\n" );
goto usage;
}
pPars->nPO = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nPO < 1 )
goto usage;
break;
case 'L':
if ( globalUtilOptind >= argc )
{

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

@ -121,6 +121,7 @@ struct Cec_ParFra_t_
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

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

@ -145,6 +145,9 @@ static inline void Cec4_ObjCleanSatId( Gia_Man_t * p, Gia_Obj_t * pObj )
extern Vec_Int_t* vLitBmiter;
extern Vec_Int_t* vIdBI;
extern Vec_Int_t* vIdBO;
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
@ -1887,51 +1890,9 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p
if ( Abc_Lit2Var(pObj->Value) == Abc_Lit2Var(pRepr->Value) )
{
// printf( "*node %d (%d) merged into node %d (%d)\n", lit_obj >> 1, Vec_IntEntry( vLitBmiter, lit_obj ), lit_repr >> 1, Vec_IntEntry( vLitBmiter, lit_repr) );
if ( Vec_IntEntry( vLitBmiter, lit_repr ) == 3 )
printf( "*node %d (%d) merged into node %d (%d)\n", lit_obj >> 1, Vec_IntEntry( vLitBmiter, lit_obj ), lit_repr >> 1, Vec_IntEntry( vLitBmiter, lit_repr) );
if ( pPars->fBMiterInfo )
{
switch ( Vec_IntEntry( vLitBmiter, lit_obj ) )
{
case 1:
case 4:
Vec_IntUpdateEntry( vLitBmiter, lit_repr, 4 );
break;
case 2:
case 5:
Vec_IntUpdateEntry( vLitBmiter, lit_repr, 5 );
break;
default:
break;
}
}
else
{
if ( Vec_IntEntry(vLitBmiter, lit_obj ) == 3 )
switch ( Vec_IntEntry( vLitBmiter, lit_repr ) )
{
case 1:
case 4:
Vec_IntUpdateEntry( vLitBmiter, lit_obj, 4 );
break;
case 2:
case 5:
Vec_IntUpdateEntry( vLitBmiter, lit_obj, 5 );
break;
default:
break;
}
}
assert( (pObj->Value ^ pRepr->Value) == (pObj->fPhase ^ pRepr->fPhase) );
Gia_ObjSetProved( p, i );
if ( Gia_ObjId(p, pRepr) == 0 )
pMan->iLastConst = i;
continue;
}
if ( Cec4_ManSweepNode(pMan, i, Gia_ObjId(p, pRepr)) && Gia_ObjProved(p, i) )
{
if (pPars->fBMiterInfo){
// printf( "node %d (%d) merged into node %d (%d)\n", lit_obj, Vec_IntEntry( vLitBmiter, lit_obj ), lit_repr, Vec_IntEntry( vLitBmiter, lit_repr ) );
if ( Vec_IntEntry( vLitBmiter, lit_repr ) == 3 )
{
switch ( Vec_IntEntry( vLitBmiter, lit_obj ) )
@ -1966,10 +1927,129 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p
}
}
// TODO
Vec_IntSetEntry( vLitBmiter, lit_obj, Vec_IntEntry( vLitBmiter, lit_repr) );
}
assert( (pObj->Value ^ pRepr->Value) == (pObj->fPhase ^ pRepr->fPhase) );
Gia_ObjSetProved( p, i );
if ( Gia_ObjId(p, pRepr) == 0 )
pMan->iLastConst = i;
continue;
}
if ( Cec4_ManSweepNode(pMan, i, Gia_ObjId(p, pRepr)) && Gia_ObjProved(p, i) )
{
if (pPars->fBMiterInfo){
printf( "node %d (%d) merged into node %d (%d)\n", lit_obj >> 1, Vec_IntEntry( vLitBmiter, lit_obj ), lit_repr >> 1, Vec_IntEntry( vLitBmiter, lit_repr ) );
if ( Vec_IntEntry( vLitBmiter, lit_repr ) == 3 )
{
switch ( Vec_IntEntry( vLitBmiter, lit_obj ) )
{
case 1:
case 4:
Vec_IntUpdateEntry( vLitBmiter, lit_repr, 4 );
break;
case 2:
case 5:
Vec_IntUpdateEntry( vLitBmiter, lit_repr, 5 );
break;
default:
break;
}
}
else
{
if ( Vec_IntEntry(vLitBmiter, lit_obj ) == 3 )
switch ( Vec_IntEntry( vLitBmiter, lit_repr ) )
{
case 1:
case 4:
Vec_IntUpdateEntry( vLitBmiter, lit_obj, 4 );
break;
case 2:
case 5:
Vec_IntUpdateEntry( vLitBmiter, lit_obj, 5 );
break;
default:
break;
}
}
// TODO
Vec_IntSetEntry( vLitBmiter, lit_obj, Vec_IntEntry( vLitBmiter, lit_repr) );
}
pObj->Value = Abc_LitNotCond( pRepr->Value, pObj->fPhase ^ pRepr->fPhase );
}
}
if ( pPars->fBMiterInfo )
{
// check bi, bo
Vec_Ptr_t* vBO = Vec_PtrAlloc( 16 );
Vec_Ptr_t * vQ = Vec_PtrAlloc(16);
int val;
printf("BI:");
Vec_IntForEachEntry( vIdBI, val, i )
{
printf( " %d (%d)", val, Vec_IntEntry( vLitBmiter, val << 1) );
}
printf("\nBO:");
Vec_IntForEachEntry( vIdBO, val, i )
{
printf( " %d (%d)", val, Vec_IntEntry( vLitBmiter, val << 1) );
if ( Vec_IntEntry( vLitBmiter, val << 1) != 5 )
{
Vec_PtrPush(vQ, &((p->pObjs)[val]) );
}
}
printf("\n");
// find bound
Gia_ManStaticFanoutStart( p );
Vec_Int_t* vFlag = Vec_IntAlloc( p->nObjs );
Vec_IntFill( vFlag, p->nObjs, 0 );
Gia_Obj_t * pObj2;
int cnt_node = 0;
int cnt_newBo = 0;
while ( Vec_PtrSize(vQ) != 0 )
{
pObj2 = Vec_PtrPop(vQ);
if ( Vec_IntEntry( vFlag, Gia_ObjId(p, pObj2) ) != 0 ) continue;
cnt_node ++;
Vec_IntSetEntry( vFlag, Gia_ObjId(p, pObj2), 1 );
val = Vec_IntEntry(vLitBmiter, Gia_ObjId(p, pObj2) << 1);
if ( val == 5 || Gia_ObjIsCo( pObj2 ) ) // boundary found
{
cnt_newBo ++;
Vec_PtrPush( vBO, pObj2 );
continue;
}
for( int j = 0; j < Gia_ObjFanoutNum(p, pObj2); j++ )
{
Vec_PtrPush( vQ, Gia_ObjFanout(p, pObj2, j) );
printf( "add fanout\n");
}
}
Gia_ManStaticFanoutStop(p);
printf("extended BO with %d extra nodes:", cnt_node);
Vec_PtrForEachEntry( Gia_Obj_t*, vBO, pObj, i )
{
printf( " %d", Gia_ObjId(p, pObj) );
}
printf("\n");
}
if ( p->iPatsPi > 0 )
{
abctime clk2 = Abc_Clock();