From 9bb5333f6210a49d7e0895139ef30386585b2594 Mon Sep 17 00:00:00 2001 From: Allen Ho Date: Thu, 7 Dec 2023 19:07:52 +0800 Subject: [PATCH] extend bo --- abc.rc | 148 ---------------------------------- src/aig/gia/giaDup.c | 19 +++++ src/base/abci/abc.c | 14 +++- src/proof/cec/cec.h | 1 + src/proof/cec/cecSatG2.c | 168 +++++++++++++++++++++++++++++---------- 5 files changed, 157 insertions(+), 193 deletions(-) delete mode 100644 abc.rc diff --git a/abc.rc b/abc.rc deleted file mode 100644 index a3efc0b09..000000000 --- a/abc.rc +++ /dev/null @@ -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" - - diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index 9d9b56a1c..ffd776cc4 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -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 ++; + } } diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index dab809c25..755aeaea0 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -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 ) { diff --git a/src/proof/cec/cec.h b/src/proof/cec/cec.h index ca4ac9aba..c9aa96658 100644 --- a/src/proof/cec/cec.h +++ b/src/proof/cec/cec.h @@ -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 diff --git a/src/proof/cec/cecSatG2.c b/src/proof/cec/cecSatG2.c index 4a39e95d3..a01cc7445 100644 --- a/src/proof/cec/cecSatG2.c +++ b/src/proof/cec/cecSatG2.c @@ -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();