From 2f90e5e15d8308a9cbebdc15976f5b5b8d3d8032 Mon Sep 17 00:00:00 2001 From: Yen-Sheng Ho Date: Wed, 22 Feb 2017 15:37:49 -0800 Subject: added an option -m for %pdra --- src/base/wlc/wlc.h | 1 + src/base/wlc/wlcCom.c | 10 +++++++--- src/base/wlc/wlcNtk.c | 1 + 3 files changed, 9 insertions(+), 3 deletions(-) (limited to 'src/base') diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h index 686d9f00..abb75f5e 100644 --- a/src/base/wlc/wlc.h +++ b/src/base/wlc/wlc.h @@ -172,6 +172,7 @@ struct Wlc_Par_t_ int fXorOutput; // XOR outputs of word-level miter int fCheckClauses; // Check clauses in the reloaded trace int fPushClauses; // Push clauses in the reloaded trace + int fMFFC; // Refine the entire MFFC of a PPI int fVerbose; // verbose output int fPdrVerbose; // verbose output }; diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c index df736e70..1c86bc23 100644 --- a/src/base/wlc/wlcCom.c +++ b/src/base/wlc/wlcCom.c @@ -462,7 +462,7 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; Wlc_ManSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFIcpxvwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFIcpmxvwh" ) ) != EOF ) { switch ( c ) { @@ -530,6 +530,9 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'p': pPars->fPushClauses ^= 1; break; + case 'm': + pPars->fMFFC ^= 1; + break; case 'v': pPars->fVerbose ^= 1; break; @@ -550,7 +553,7 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv ) Wlc_NtkPdrAbs( pNtk, pPars ); return 0; usage: - Abc_Print( -2, "usage: %%pdra [-AMXFI num] [-cpxvwh]\n" ); + Abc_Print( -2, "usage: %%pdra [-AMXFI num] [-cpmxvwh]\n" ); Abc_Print( -2, "\t abstraction for word-level networks\n" ); Abc_Print( -2, "\t-A num : minimum bit-width of an adder/subtractor to abstract [default = %d]\n", pPars->nBitsAdd ); Abc_Print( -2, "\t-M num : minimum bit-width of a multiplier to abstract [default = %d]\n", pPars->nBitsMul ); @@ -559,7 +562,8 @@ usage: Abc_Print( -2, "\t-I num : maximum number of CEGAR iterations [default = %d]\n", pPars->nIterMax ); Abc_Print( -2, "\t-x : toggle XORing outputs of word-level miter [default = %s]\n", pPars->fXorOutput? "yes": "no" ); Abc_Print( -2, "\t-c : toggle checking clauses in the reloaded trace [default = %s]\n", pPars->fCheckClauses? "yes": "no" ); - Abc_Print( -2, "\t-p : toggle pushing clauses in the reloaded trace [default = %s]\n", pPars->fPushClauses? "yes": "no" ); + Abc_Print( -2, "\t-p : toggle pushing clauses in the reloaded trace [default = %s]\n", pPars->fPushClauses? "yes": "no" ); + Abc_Print( -2, "\t-m : toggle refining the whole MFFC of a PPI [default = %s]\n", pPars->fMFFC? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); Abc_Print( -2, "\t-w : toggle printing verbose PDR output [default = %s]\n", pPars->fPdrVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); diff --git a/src/base/wlc/wlcNtk.c b/src/base/wlc/wlcNtk.c index c8fc15a7..e27ba77b 100644 --- a/src/base/wlc/wlcNtk.c +++ b/src/base/wlc/wlcNtk.c @@ -116,6 +116,7 @@ void Wlc_ManSetDefaultParams( Wlc_Par_t * pPars ) pPars->fXorOutput = 1; // XOR outputs of word-level miter pPars->fCheckClauses = 1; // Check clauses in the reloaded trace pPars->fPushClauses = 0; // Push clauses in the reloaded trace + pPars->fMFFC = 1; // Refine the entire MFFC of a PPI pPars->fVerbose = 0; // verbose output` pPars->fPdrVerbose = 0; // show verbose PDR output } -- cgit v1.2.3 From f01c63f712a31726af27340b6255fc1ffbee87b7 Mon Sep 17 00:00:00 2001 From: Yen-Sheng Ho Date: Wed, 22 Feb 2017 17:57:19 -0800 Subject: working on %pdra -m --- src/base/wlc/wlcAbs.c | 27 ++++++++++++++++++++++++--- 1 file changed, 24 insertions(+), 3 deletions(-) (limited to 'src/base') diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c index e33424f7..b22f9128 100644 --- a/src/base/wlc/wlcAbs.c +++ b/src/base/wlc/wlcAbs.c @@ -302,6 +302,17 @@ static int Wlc_NtkRemoveFromAbstraction( Wlc_Ntk_t * p, Vec_Int_t * vRefine, Vec return nNodes; } +static int Wlc_NtkUnmarkRefinement( Wlc_Ntk_t * p, Vec_Int_t * vRefine, Vec_Bit_t * vUnmark ) +{ + Wlc_Obj_t * pObj; int i, nNodes = 0; + Wlc_NtkForEachObjVec( vRefine, p, pObj, i ) + { + Vec_BitWriteEntry( vUnmark, Wlc_ObjId(p, pObj), 1 ); + ++nNodes; + } + return nNodes; +} + /**Function************************************************************* Synopsis [Computes the map for remapping flop IDs used in the clauses.] @@ -480,9 +491,19 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) Pdr_ManStop( pPdr ); // update the set of objects to be un-abstracted - nNodes = Wlc_NtkRemoveFromAbstraction( p, vRefine, vUnmark ); - if ( pPars->fVerbose ) - printf( "Refinement of CEX in frame %d came up with %d un-abstacted PPIs, whose MFFCs include %d objects.\n", pCex->iFrame, Vec_IntSize(vRefine), nNodes ); + if ( pPars->fMFFC ) + { + nNodes = Wlc_NtkRemoveFromAbstraction( p, vRefine, vUnmark ); + if ( pPars->fVerbose ) + printf( "Refinement of CEX in frame %d came up with %d un-abstacted PPIs, whose MFFCs include %d objects.\n", pCex->iFrame, Vec_IntSize(vRefine), nNodes ); + } + else + { + nNodes = Wlc_NtkUnmarkRefinement( p, vRefine, vUnmark ); + if ( pPars->fVerbose ) + printf( "Refinement of CEX in frame %d came up with %d un-abstacted PPIs.\n", pCex->iFrame, Vec_IntSize(vRefine) ); + + } Vec_IntFree( vRefine ); Abc_CexFree( pCex ); Aig_ManStop( pAig ); -- cgit v1.2.3 From d5bbf9188c4ea4ded22afe67b18290b148bf1d88 Mon Sep 17 00:00:00 2001 From: Yen-Sheng Ho Date: Thu, 23 Feb 2017 08:48:53 -0800 Subject: added %pdra -a: run with pdr -nct --- src/base/wlc/wlc.h | 1 + src/base/wlc/wlcAbs.c | 8 ++++++++ src/base/wlc/wlcCom.c | 8 ++++++-- src/base/wlc/wlcNtk.c | 1 + 4 files changed, 16 insertions(+), 2 deletions(-) (limited to 'src/base') diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h index abb75f5e..cb84a70d 100644 --- a/src/base/wlc/wlc.h +++ b/src/base/wlc/wlc.h @@ -173,6 +173,7 @@ struct Wlc_Par_t_ int fCheckClauses; // Check clauses in the reloaded trace int fPushClauses; // Push clauses in the reloaded trace int fMFFC; // Refine the entire MFFC of a PPI + int fPdra; // Use pdr -nct int fVerbose; // verbose output int fPdrVerbose; // verbose output }; diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c index b22f9128..c1bb7f94 100644 --- a/src/base/wlc/wlcAbs.c +++ b/src/base/wlc/wlcAbs.c @@ -390,6 +390,14 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) pPdrPars->fVerbose = pPars->fPdrVerbose; pPdrPars->fVeryVerbose = 0; + if ( pPars->fPdra ) + { + pPdrPars->fUseAbs = 1; // use 'pdr -t' (on-the-fly abstraction) + pPdrPars->fCtgs = 1; // use 'pdr -nc' (improved generalization) + pPdrPars->fSkipDown = 0; // use 'pdr -nc' (improved generalization) + pPdrPars->nRestLimit = 500; // reset queue or proof-obligations when it gets larger than this + } + // perform refinement iterations for ( nIters = 1; nIters < pPars->nIterMax; nIters++ ) { diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c index 1c86bc23..32b26b68 100644 --- a/src/base/wlc/wlcCom.c +++ b/src/base/wlc/wlcCom.c @@ -462,7 +462,7 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; Wlc_ManSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFIcpmxvwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFIacpmxvwh" ) ) != EOF ) { switch ( c ) { @@ -521,6 +521,9 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->nIterMax < 0 ) goto usage; break; + case 'a': + pPars->fPdra ^= 1; + break; case 'x': pPars->fXorOutput ^= 1; break; @@ -553,7 +556,7 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv ) Wlc_NtkPdrAbs( pNtk, pPars ); return 0; usage: - Abc_Print( -2, "usage: %%pdra [-AMXFI num] [-cpmxvwh]\n" ); + Abc_Print( -2, "usage: %%pdra [-AMXFI num] [-acpmxvwh]\n" ); Abc_Print( -2, "\t abstraction for word-level networks\n" ); Abc_Print( -2, "\t-A num : minimum bit-width of an adder/subtractor to abstract [default = %d]\n", pPars->nBitsAdd ); Abc_Print( -2, "\t-M num : minimum bit-width of a multiplier to abstract [default = %d]\n", pPars->nBitsMul ); @@ -561,6 +564,7 @@ usage: Abc_Print( -2, "\t-F num : minimum bit-width of a flip-flop to abstract [default = %d]\n", pPars->nBitsFlop ); Abc_Print( -2, "\t-I num : maximum number of CEGAR iterations [default = %d]\n", pPars->nIterMax ); Abc_Print( -2, "\t-x : toggle XORing outputs of word-level miter [default = %s]\n", pPars->fXorOutput? "yes": "no" ); + Abc_Print( -2, "\t-a : toggle running pdr with -nct [default = %s]\n", pPars->fPdra? "yes": "no" ); Abc_Print( -2, "\t-c : toggle checking clauses in the reloaded trace [default = %s]\n", pPars->fCheckClauses? "yes": "no" ); Abc_Print( -2, "\t-p : toggle pushing clauses in the reloaded trace [default = %s]\n", pPars->fPushClauses? "yes": "no" ); Abc_Print( -2, "\t-m : toggle refining the whole MFFC of a PPI [default = %s]\n", pPars->fMFFC? "yes": "no" ); diff --git a/src/base/wlc/wlcNtk.c b/src/base/wlc/wlcNtk.c index e27ba77b..4d7604b2 100644 --- a/src/base/wlc/wlcNtk.c +++ b/src/base/wlc/wlcNtk.c @@ -117,6 +117,7 @@ void Wlc_ManSetDefaultParams( Wlc_Par_t * pPars ) pPars->fCheckClauses = 1; // Check clauses in the reloaded trace pPars->fPushClauses = 0; // Push clauses in the reloaded trace pPars->fMFFC = 1; // Refine the entire MFFC of a PPI + pPars->fPdra = 0; // Use pdr -nct pPars->fVerbose = 0; // verbose output` pPars->fPdrVerbose = 0; // show verbose PDR output } -- cgit v1.2.3 From db36c65bce6bce54fc22349be651c784e710d3da Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 23 Feb 2017 14:12:56 -0800 Subject: Small changes in the usage message for &gla. --- src/base/abci/abc.c | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'src/base') diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 466af66a..003842f0 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -1000,12 +1000,14 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&save", Abc_CommandAbc9Save, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&load", Abc_CommandAbc9Load, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&r", Abc_CommandAbc9Read, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&read", Abc_CommandAbc9Read, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&read_blif", Abc_CommandAbc9ReadBlif, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&read_cblif", Abc_CommandAbc9ReadCBlif, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&read_stg", Abc_CommandAbc9ReadStg, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&read_ver", Abc_CommandAbc9ReadVer, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&write_ver", Abc_CommandAbc9WriteVer, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&w", Abc_CommandAbc9Write, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&write", Abc_CommandAbc9Write, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&wlut", Abc_CommandAbc9WriteLut, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&ps", Abc_CommandAbc9Ps, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&pfan", Abc_CommandAbc9PFan, 0 ); @@ -42428,7 +42430,7 @@ usage: Abc_Print( -2, "\t-Q num : stop when abstraction size exceeds num %% during refinement (0<=num<=100) [default = %d]\n", pPars->nRatioMin2 ); Abc_Print( -2, "\t-P num : maximum percentage of added objects before a restart (0<=num<=100) [default = %d]\n", pPars->nRatioMax ); Abc_Print( -2, "\t-B num : the number of stable frames to call prover or dump abstraction [default = %d]\n", pPars->nFramesNoChangeLim ); - Abc_Print( -2, "\t-A file : file name for dumping abstrated model [default = \"glabs.aig\"]\n" ); + Abc_Print( -2, "\t-A file : file name for dumping abstrated model (&gla -d) or abstraction map (&gla -m)\n" ); Abc_Print( -2, "\t-f : toggle propagating fanout implications [default = %s]\n", pPars->fPropFanout? "yes": "no" ); Abc_Print( -2, "\t-a : toggle refinement by adding one layers of gates [default = %s]\n", pPars->fAddLayer? "yes": "no" ); Abc_Print( -2, "\t-r : toggle using improved refinement heuristics [default = %s]\n", pPars->fNewRefine? "yes": "no" ); -- cgit v1.2.3 From 14cf117968a796b176ab7df2ee8a09d94eaf55f6 Mon Sep 17 00:00:00 2001 From: Yen-Sheng Ho Date: Sat, 25 Feb 2017 09:37:59 -0800 Subject: imported proof-based codes from ufar --- src/base/wlc/wlcAbs.c | 88 +++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 88 insertions(+) (limited to 'src/base') diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c index c1bb7f94..d28e95c3 100644 --- a/src/base/wlc/wlcAbs.c +++ b/src/base/wlc/wlcAbs.c @@ -38,6 +38,94 @@ extern int IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPu /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +Wlc_Ntk_t * Wlc_NtkIntroduceChoices( Wlc_Ntk_t * pNtk, Vec_Int_t * vNodes ) +{ + if ( vNodes == NULL ) return NULL; + + Wlc_Ntk_t * pNew; + Wlc_Obj_t * pObj; + int i, k, iObj, iFanin; + Vec_Int_t * vFanins = Vec_IntAlloc( 3 ); + Vec_Int_t * vMapNode2Pi = Vec_IntStart( Wlc_NtkObjNum(pNtk) ); + int nOrigObjNum = Wlc_NtkObjNumMax( pNtk ); + Wlc_Ntk_t * p = Wlc_NtkDupDfs( pNtk, 0, 1 ); + + Wlc_NtkForEachObjVec( vNodes, pNtk, pObj, i ) + { + // TODO : fix FOs here + Vec_IntWriteEntry(vNodes, i, Wlc_ObjCopy(pNtk, Wlc_ObjId(pNtk, pObj))); + } + + // Vec_IntPrint(vNodes); + Wlc_NtkCleanCopy( p ); + + // mark nodes + Wlc_NtkForEachObjVec( vNodes, p, pObj, i ) + { + iObj = Wlc_ObjId(p, pObj); + pObj->Mark = 1; + // add fresh PI with the same number of bits + Vec_IntWriteEntry( vMapNode2Pi, iObj, Wlc_ObjAlloc( p, WLC_OBJ_PI, Wlc_ObjIsSigned(pObj), Wlc_ObjRange(pObj) - 1, 0 ) ); + } + + // iterate through the nodes in the DFS order + Wlc_NtkForEachObj( p, pObj, i ) + { + int isSigned, range, iSelID; + if ( i == nOrigObjNum ) + { + // cout << "break at " << i << endl; + break; + } + if ( pObj->Mark ) + { + // clean + pObj->Mark = 0; + + isSigned = Wlc_ObjIsSigned(pObj); + range = Wlc_ObjRange(pObj); + iSelID = Wlc_ObjAlloc( p, WLC_OBJ_PI, 0, 0, 0); + Vec_IntClear(vFanins); + Vec_IntPush(vFanins, iSelID); + Vec_IntPush(vFanins, Vec_IntEntry( vMapNode2Pi, i ) ); + Vec_IntPush(vFanins, i); + iObj = Wlc_ObjCreate(p, WLC_OBJ_MUX, isSigned, range - 1, 0, vFanins); + } + else + { + // update fanins + Wlc_ObjForEachFanin( pObj, iFanin, k ) + Wlc_ObjFanins(pObj)[k] = Wlc_ObjCopy(p, iFanin); + // node to remain + iObj = i; + } + Wlc_ObjSetCopy( p, i, iObj ); + } + + Wlc_NtkForEachCo( p, pObj, i ) + { + iObj = Wlc_ObjId(p, pObj); + if (iObj != Wlc_ObjCopy(p, iObj)) + { + if (pObj->fIsFi) + Wlc_NtkObj(p, Wlc_ObjCopy(p, iObj))->fIsFi = 1; + else + Wlc_NtkObj(p, Wlc_ObjCopy(p, iObj))->fIsPo = 1; + + Vec_IntWriteEntry(&p->vCos, i, Wlc_ObjCopy(p, iObj)); + } + } + + // DumpWlcNtk(p); + pNew = Wlc_NtkDupDfs( p, 0, 1 ); + + Vec_IntFree( vFanins ); + Vec_IntFree( vMapNode2Pi ); + Wlc_NtkFree( p ); + + return pNew; +} + /**Function************************************************************* Synopsis [Mark operators that meet the abstraction criteria.] -- cgit v1.2.3 From 7508a37a5188807bae90f16c99aa27ae6a79e44a Mon Sep 17 00:00:00 2001 From: Yen-Sheng Ho Date: Sat, 25 Feb 2017 14:58:01 -0800 Subject: imported proof-based codes from ufar --- src/base/wlc/wlcAbs.c | 72 +++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 72 insertions(+) (limited to 'src/base') diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c index d28e95c3..cc6e6a46 100644 --- a/src/base/wlc/wlcAbs.c +++ b/src/base/wlc/wlcAbs.c @@ -38,6 +38,78 @@ extern int IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPu /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +int Wlc_NtkNumPiBits( Wlc_Ntk_t * pNtk ) +{ + int num = 0; + int i; + Wlc_Obj_t * pObj; + Wlc_NtkForEachPi(pNtk, pObj, i) { + num += Wlc_ObjRange(pObj); + } + return num; +} + +static Gia_Man_t * Wlc_NtkUnrollWithCex(Wlc_Ntk_t * pChoice, Abc_Cex_t * pCex, int nbits_old_pis, int num_sel_pis, int * p_num_ppis, int sel_pi_first) +{ + Gia_Man_t * pGiaChoice = Wlc_NtkBitBlast( pChoice, NULL, -1, 0, 0, 0, 0 ); + int nbits_new_pis = Wlc_NtkNumPiBits( pChoice ); + int num_ppis = nbits_new_pis - nbits_old_pis - num_sel_pis; + *p_num_ppis = num_ppis; + int num_undc_pis = Gia_ManPiNum(pGiaChoice) - nbits_new_pis; + Gia_Man_t * pFrames = NULL; + Gia_Obj_t * pObj, * pObjRi; + int f, i; + int is_sel_pi; + Gia_Man_t * pGia; + + Abc_Print( 1, "#orig_pis = %d, #ppis = %d, #sel_pis = %d, #undc_pis = %d\n", nbits_old_pis, num_ppis, num_sel_pis, num_undc_pis ); + assert(Gia_ManPiNum(pGiaChoice)==nbits_old_pis+num_ppis+num_sel_pis+num_undc_pis); + assert(Gia_ManPiNum(pGiaChoice)==pCex->nPis+num_sel_pis); + + pFrames = Gia_ManStart( 10000 ); + pFrames->pName = Abc_UtilStrsav( pGiaChoice->pName ); + Gia_ManHashAlloc( pFrames ); + Gia_ManConst0(pGiaChoice)->Value = 0; + Gia_ManForEachRi( pGiaChoice, pObj, i ) + pObj->Value = 0; + + for ( f = 0; f <= pCex->iFrame; f++ ) + { + for( i = 0; i < Gia_ManPiNum(pGiaChoice); i++ ) + { + if ( i >= nbits_old_pis && i < nbits_old_pis + num_ppis + num_sel_pis ) + { + is_sel_pi = sel_pi_first ? (i < nbits_old_pis + num_sel_pis) : (i >= nbits_old_pis + num_ppis); + if(f == 0 || !is_sel_pi) + Gia_ManPi(pGiaChoice, i)->Value = Gia_ManAppendCi(pFrames); + } + else if (i < nbits_old_pis) + { + Gia_ManPi(pGiaChoice, i)->Value = Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i); + } + else if (i >= nbits_old_pis + num_ppis + num_sel_pis) + { + Gia_ManPi(pGiaChoice, i)->Value = Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i - num_sel_pis); + } + } + Gia_ManForEachRiRo( pGiaChoice, pObjRi, pObj, i ) + pObj->Value = pObjRi->Value; + Gia_ManForEachAnd( pGiaChoice, pObj, i ) + pObj->Value = Gia_ManHashAnd(pFrames, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj)); + Gia_ManForEachCo( pGiaChoice, pObj, i ) + pObj->Value = Gia_ObjFanin0Copy(pObj); + Gia_ManForEachPo( pGiaChoice, pObj, i ) + Gia_ManAppendCo(pFrames, pObj->Value); + } + Gia_ManHashStop (pFrames); + Gia_ManSetRegNum(pFrames, 0); + pFrames = Gia_ManCleanup(pGia = pFrames); + Gia_ManStop(pGia); + Gia_ManStop(pGiaChoice); + + return pFrames; +} + Wlc_Ntk_t * Wlc_NtkIntroduceChoices( Wlc_Ntk_t * pNtk, Vec_Int_t * vNodes ) { if ( vNodes == NULL ) return NULL; -- cgit v1.2.3 From a7bc919b6921fe0a2a0fc152929bc01f6e31b820 Mon Sep 17 00:00:00 2001 From: Yen-Sheng Ho Date: Sat, 25 Feb 2017 15:22:30 -0800 Subject: imported proof-based codes from ufar --- src/base/wlc/wlcAbs.c | 78 +++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 78 insertions(+) (limited to 'src/base') diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c index cc6e6a46..249fe1af 100644 --- a/src/base/wlc/wlcAbs.c +++ b/src/base/wlc/wlcAbs.c @@ -49,6 +49,84 @@ int Wlc_NtkNumPiBits( Wlc_Ntk_t * pNtk ) return num; } +static Vec_Int_t * Wlc_NtkGetCoreSels( Gia_Man_t * pFrames, int nFrames, int num_sel_pis, int num_other_pis, int sel_pi_first, int nConfLimit ) +{ + Vec_Int_t * vCores = NULL; + Aig_Man_t * pAigFrames = Gia_ManToAigSimple( pFrames ); + Cnf_Dat_t * pCnf = Cnf_Derive(pAigFrames, Aig_ManCoNum(pAigFrames)); + sat_solver * pSat = sat_solver_new(); + + sat_solver_setnvars(pSat, pCnf->nVars); + + for (int i = 0; i < pCnf->nClauses; i++) + { + if (!sat_solver_addclause(pSat, pCnf->pClauses[i], pCnf->pClauses[i + 1])) + assert(false); + } + // add PO clauses + { + Vec_Int_t* vLits = Vec_IntAlloc(100); + Aig_Obj_t* pObj; + int i, ret; + Aig_ManForEachCo( pAigFrames, pObj, i ) + { + assert(pCnf->pVarNums[pObj->Id] >= 0); + Vec_IntPush(vLits, toLitCond(pCnf->pVarNums[pObj->Id], 0)); + } + ret = sat_solver_addclause(pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits)); + if (!ret) + Abc_Print( 1, "UNSAT after adding PO clauses.\n" ); + + Vec_IntFree(vLits); + } + // main procedure + { + Vec_Int_t* vLits = Vec_IntAlloc(100); + Vec_Int_t* vMapVar2Sel = Vec_IntStart( pCnf->nVars ); + int first_sel_pi = sel_pi_first ? 0 : num_other_pis; + for ( int i = 0; i < num_sel_pis; ++i ) + { + int cur_pi = first_sel_pi + i; + int var = pCnf->pVarNums[Aig_ManCi(pAigFrames, cur_pi)->Id]; + assert(var >= 0); + Vec_IntWriteEntry( vMapVar2Sel, var, i ); + Vec_IntPush(vLits, toLitCond(var, 0)); + } + + { + int i, Entry; + Abc_Print( 1, "#vLits = %d; vLits = ", Vec_IntSize(vLits) ); + Vec_IntForEachEntry(vLits, Entry, i) + Abc_Print( 1, "%d ", Entry); + Abc_Print( 1, "\n", Entry); + } + int status = sat_solver_solve(pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), (ABC_INT64_T)(nConfLimit), (ABC_INT64_T)(0), (ABC_INT64_T)(0), (ABC_INT64_T)(0)); + if (status == l_False) { + Abc_Print( 1, "UNSAT.\n" ); + int nCoreLits, *pCoreLits; + nCoreLits = sat_solver_final(pSat, &pCoreLits); + + vCores = Vec_IntAlloc( nCoreLits ); + for (int i = 0; i < nCoreLits; i++) + { + Vec_IntPush( vCores, Vec_IntEntry( vMapVar2Sel, lit_var( pCoreLits[i] ) ) ); + } + } else if (status == l_True) { + Abc_Print( 1, "SAT.\n" ); + } else { + Abc_Print( 1, "UNKNOWN.\n" ); + } + + Vec_IntFree(vLits); + Vec_IntFree(vMapVar2Sel); + } + Cnf_ManFree(); + sat_solver_delete(pSat); + Aig_ManStop(pAigFrames); + + return vCores; +} + static Gia_Man_t * Wlc_NtkUnrollWithCex(Wlc_Ntk_t * pChoice, Abc_Cex_t * pCex, int nbits_old_pis, int num_sel_pis, int * p_num_ppis, int sel_pi_first) { Gia_Man_t * pGiaChoice = Wlc_NtkBitBlast( pChoice, NULL, -1, 0, 0, 0, 0 ); -- cgit v1.2.3 From a8f6e5c60a0ffb23ebb6c1ae2a1a6f27514dc0e2 Mon Sep 17 00:00:00 2001 From: Yen-Sheng Ho Date: Sat, 25 Feb 2017 18:32:43 -0800 Subject: added an option -b to %pdra --- src/base/wlc/wlc.h | 2 + src/base/wlc/wlcAbs.c | 205 +++++++++++++++++++++++++++++++++++++++++++++----- src/base/wlc/wlcCom.c | 10 ++- src/base/wlc/wlcNtk.c | 52 ++++++++++--- 4 files changed, 237 insertions(+), 32 deletions(-) (limited to 'src/base') diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h index cb84a70d..71273f98 100644 --- a/src/base/wlc/wlc.h +++ b/src/base/wlc/wlc.h @@ -174,6 +174,7 @@ struct Wlc_Par_t_ int fPushClauses; // Push clauses in the reloaded trace int fMFFC; // Refine the entire MFFC of a PPI int fPdra; // Use pdr -nct + int fProofRefine; // Use proof-based refinement int fVerbose; // verbose output int fPdrVerbose; // verbose output }; @@ -311,6 +312,7 @@ extern void Wlc_NtkTransferNames( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p ); extern char * Wlc_NtkNewName( Wlc_Ntk_t * p, int iCoId, int fSeq ); extern Wlc_Ntk_t * Wlc_NtkDupDfs( Wlc_Ntk_t * p, int fMarked, int fSeq ); extern Wlc_Ntk_t * Wlc_NtkDupDfsAbs( Wlc_Ntk_t * p, Vec_Int_t * vPisOld, Vec_Int_t * vPisNew, Vec_Int_t * vFlops ); +extern Wlc_Ntk_t * Wlc_NtkDupDfsSimple( Wlc_Ntk_t * p ); extern void Wlc_NtkCleanMarks( Wlc_Ntk_t * p ); extern void Wlc_NtkMarkCone( Wlc_Ntk_t * p, int iCoId, int Range, int fSeq, int fAllPis ); extern void Wlc_NtkProfileCones( Wlc_Ntk_t * p ); diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c index 249fe1af..bc6d6717 100644 --- a/src/base/wlc/wlcAbs.c +++ b/src/base/wlc/wlcAbs.c @@ -49,7 +49,7 @@ int Wlc_NtkNumPiBits( Wlc_Ntk_t * pNtk ) return num; } -static Vec_Int_t * Wlc_NtkGetCoreSels( Gia_Man_t * pFrames, int nFrames, int num_sel_pis, int num_other_pis, int sel_pi_first, int nConfLimit ) +static Vec_Int_t * Wlc_NtkGetCoreSels( Gia_Man_t * pFrames, int nFrames, int num_sel_pis, int num_other_pis, int sel_pi_first, int nConfLimit, Wlc_Par_t * pPars ) { Vec_Int_t * vCores = NULL; Aig_Man_t * pAigFrames = Gia_ManToAigSimple( pFrames ); @@ -93,13 +93,13 @@ static Vec_Int_t * Wlc_NtkGetCoreSels( Gia_Man_t * pFrames, int nFrames, int num Vec_IntPush(vLits, toLitCond(var, 0)); } - { + /* int i, Entry; Abc_Print( 1, "#vLits = %d; vLits = ", Vec_IntSize(vLits) ); Vec_IntForEachEntry(vLits, Entry, i) Abc_Print( 1, "%d ", Entry); - Abc_Print( 1, "\n", Entry); - } + Abc_Print( 1, "\n"); + */ int status = sat_solver_solve(pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), (ABC_INT64_T)(nConfLimit), (ABC_INT64_T)(0), (ABC_INT64_T)(0), (ABC_INT64_T)(0)); if (status == l_False) { Abc_Print( 1, "UNSAT.\n" ); @@ -167,7 +167,7 @@ static Gia_Man_t * Wlc_NtkUnrollWithCex(Wlc_Ntk_t * pChoice, Abc_Cex_t * pCex, i } else if (i >= nbits_old_pis + num_ppis + num_sel_pis) { - Gia_ManPi(pGiaChoice, i)->Value = Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i - num_sel_pis); + Gia_ManPi(pGiaChoice, i)->Value = Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i - num_sel_pis - num_ppis); } } Gia_ManForEachRiRo( pGiaChoice, pObjRi, pObj, i ) @@ -188,17 +188,19 @@ static Gia_Man_t * Wlc_NtkUnrollWithCex(Wlc_Ntk_t * pChoice, Abc_Cex_t * pCex, i return pFrames; } -Wlc_Ntk_t * Wlc_NtkIntroduceChoices( Wlc_Ntk_t * pNtk, Vec_Int_t * vNodes ) +Wlc_Ntk_t * Wlc_NtkIntroduceChoices( Wlc_Ntk_t * pNtk, Vec_Int_t * vBlacks ) { - if ( vNodes == NULL ) return NULL; + if ( vBlacks== NULL ) return NULL; + Vec_Int_t * vNodes = Vec_IntDup( vBlacks ); Wlc_Ntk_t * pNew; Wlc_Obj_t * pObj; int i, k, iObj, iFanin; Vec_Int_t * vFanins = Vec_IntAlloc( 3 ); - Vec_Int_t * vMapNode2Pi = Vec_IntStart( Wlc_NtkObjNum(pNtk) ); + Vec_Int_t * vMapNode2Pi = Vec_IntStart( Wlc_NtkObjNumMax(pNtk) ); + Vec_Int_t * vMapNode2Sel = Vec_IntStart( Wlc_NtkObjNumMax(pNtk) ); int nOrigObjNum = Wlc_NtkObjNumMax( pNtk ); - Wlc_Ntk_t * p = Wlc_NtkDupDfs( pNtk, 0, 1 ); + Wlc_Ntk_t * p = Wlc_NtkDupDfsSimple( pNtk ); Wlc_NtkForEachObjVec( vNodes, pNtk, pObj, i ) { @@ -218,10 +220,17 @@ Wlc_Ntk_t * Wlc_NtkIntroduceChoices( Wlc_Ntk_t * pNtk, Vec_Int_t * vNodes ) Vec_IntWriteEntry( vMapNode2Pi, iObj, Wlc_ObjAlloc( p, WLC_OBJ_PI, Wlc_ObjIsSigned(pObj), Wlc_ObjRange(pObj) - 1, 0 ) ); } + // add sel PI + Wlc_NtkForEachObjVec( vNodes, p, pObj, i ) + { + iObj = Wlc_ObjId( p, pObj ); + Vec_IntWriteEntry( vMapNode2Sel, iObj, Wlc_ObjAlloc( p, WLC_OBJ_PI, 0, 0, 0 ) ); + } + // iterate through the nodes in the DFS order Wlc_NtkForEachObj( p, pObj, i ) { - int isSigned, range, iSelID; + int isSigned, range; if ( i == nOrigObjNum ) { // cout << "break at " << i << endl; @@ -234,9 +243,8 @@ Wlc_Ntk_t * Wlc_NtkIntroduceChoices( Wlc_Ntk_t * pNtk, Vec_Int_t * vNodes ) isSigned = Wlc_ObjIsSigned(pObj); range = Wlc_ObjRange(pObj); - iSelID = Wlc_ObjAlloc( p, WLC_OBJ_PI, 0, 0, 0); Vec_IntClear(vFanins); - Vec_IntPush(vFanins, iSelID); + Vec_IntPush(vFanins, Vec_IntEntry( vMapNode2Sel, i) ); Vec_IntPush(vFanins, Vec_IntEntry( vMapNode2Pi, i ) ); Vec_IntPush(vFanins, i); iObj = Wlc_ObjCreate(p, WLC_OBJ_MUX, isSigned, range - 1, 0, vFanins); @@ -267,15 +275,127 @@ Wlc_Ntk_t * Wlc_NtkIntroduceChoices( Wlc_Ntk_t * pNtk, Vec_Int_t * vNodes ) } // DumpWlcNtk(p); - pNew = Wlc_NtkDupDfs( p, 0, 1 ); + pNew = Wlc_NtkDupDfsSimple( p ); Vec_IntFree( vFanins ); Vec_IntFree( vMapNode2Pi ); + Vec_IntFree( vMapNode2Sel ); + Vec_IntFree( vNodes ); Wlc_NtkFree( p ); return pNew; } +static Wlc_Ntk_t * Wlc_NtkAbs2( Wlc_Ntk_t * pNtk, Vec_Int_t * vBlacks, Vec_Int_t ** pvFlops ) +{ + Vec_Int_t * vFlops = Vec_IntAlloc( 100 ); + Vec_Int_t * vNodes = Vec_IntDup( vBlacks ); + Wlc_Ntk_t * pNew; + Wlc_Obj_t * pObj; + int i, k, iObj, iFanin; + Vec_Int_t * vMapNode2Pi = Vec_IntStart( Wlc_NtkObjNumMax(pNtk) ); + int nOrigObjNum = Wlc_NtkObjNumMax( pNtk ); + + if ( vNodes == NULL ) + return NULL; + + Wlc_Ntk_t * p = NULL; + p = Wlc_NtkDupDfsSimple( pNtk ); + + Wlc_NtkForEachCi( pNtk, pObj, i ) + { + if ( !Wlc_ObjIsPi( pObj ) ) + Vec_IntPush( vFlops, Wlc_ObjId( pNtk, pObj ) ); + } + + Wlc_NtkForEachObjVec( vNodes, pNtk, pObj, i ) + Vec_IntWriteEntry(vNodes, i, Wlc_ObjCopy(pNtk, Wlc_ObjId(pNtk, pObj))); + + // mark nodes + Wlc_NtkForEachObjVec( vNodes, p, pObj, i ) + { + iObj = Wlc_ObjId(p, pObj); + pObj->Mark = 1; + // add fresh PI with the same number of bits + Vec_IntWriteEntry( vMapNode2Pi, iObj, Wlc_ObjAlloc( p, WLC_OBJ_PI, Wlc_ObjIsSigned(pObj), Wlc_ObjRange(pObj) - 1, 0 ) ); + } + + Wlc_NtkCleanCopy( p ); + + Wlc_NtkForEachObj( p, pObj, i ) + { + if ( i == nOrigObjNum ) + break; + + if ( pObj->Mark ) { + // clean + pObj->Mark = 0; + iObj = Vec_IntEntry( vMapNode2Pi, i ); + } + else { + // update fanins + Wlc_ObjForEachFanin( pObj, iFanin, k ) + Wlc_ObjFanins(pObj)[k] = Wlc_ObjCopy(p, iFanin); + // node to remain + iObj = i; + } + Wlc_ObjSetCopy( p, i, iObj ); + } + + Wlc_NtkForEachCo( p, pObj, i ) + { + iObj = Wlc_ObjId(p, pObj); + if (iObj != Wlc_ObjCopy(p, iObj)) + { + if (pObj->fIsFi) + Wlc_NtkObj(p, Wlc_ObjCopy(p, iObj))->fIsFi = 1; + else + Wlc_NtkObj(p, Wlc_ObjCopy(p, iObj))->fIsPo = 1; + + + Vec_IntWriteEntry(&p->vCos, i, Wlc_ObjCopy(p, iObj)); + } + } + + pNew = Wlc_NtkDupDfsSimple( p ); + Vec_IntFree( vMapNode2Pi ); + Vec_IntFree( vNodes ); + Wlc_NtkFree( p ); + + if ( pvFlops ) + *pvFlops = vFlops; + else + Vec_IntFree( vFlops ); + + return pNew; +} + +static Vec_Int_t * Wlc_NtkProofRefine( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Gia_Man_t * pGia, Abc_Cex_t * pCex, Vec_Int_t * vBlacks ) +{ + Vec_Int_t * vRefine = Vec_IntAlloc( 100 ); + Wlc_Ntk_t * pNtkWithChoices = Wlc_NtkIntroduceChoices( p, vBlacks ); + Vec_Int_t * vCoreSels; + int num_ppis = -1; + int Entry, i; + Gia_Man_t * pGiaFrames = Wlc_NtkUnrollWithCex( pNtkWithChoices, pCex, Wlc_NtkNumPiBits( p ), Vec_IntSize( vBlacks ), &num_ppis, 0 ); + vCoreSels = Wlc_NtkGetCoreSels( pGiaFrames, pCex->iFrame+1, Vec_IntSize( vBlacks ), num_ppis, 0, 0, pPars ); + + Vec_IntForEachEntry( vCoreSels, Entry, i ) + Vec_IntPush( vRefine, Vec_IntEntry( vBlacks, Entry ) ); + + Wlc_NtkFree( pNtkWithChoices ); + Gia_ManStop( pGiaFrames ); + Vec_IntFree( vCoreSels ); + + if ( Vec_IntSize( vRefine ) == 0 ) + { + Vec_IntFree( vRefine ); + vRefine = NULL; + } + + return vRefine; +} + /**Function************************************************************* Synopsis [Mark operators that meet the abstraction criteria.] @@ -289,6 +409,45 @@ Wlc_Ntk_t * Wlc_NtkIntroduceChoices( Wlc_Ntk_t * pNtk, Vec_Int_t * vNodes ) SeeAlso [] ***********************************************************************/ +static Vec_Int_t * Wlc_NtkGetBlacks( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Bit_t * vUnmark ) +{ + Vec_Int_t * vBlacks = Vec_IntAlloc( 100 ) ; + Wlc_Obj_t * pObj; int i, Count[4] = {0}; + Wlc_NtkForEachObj( p, pObj, i ) + { + if ( vUnmark && Vec_BitEntry(vUnmark, i) ) // not allow this object to be abstracted away + continue; + + if ( pObj->Type == WLC_OBJ_ARI_ADD || pObj->Type == WLC_OBJ_ARI_SUB || pObj->Type == WLC_OBJ_ARI_MINUS ) + { + if ( Wlc_ObjRange(pObj) >= pPars->nBitsAdd ) + Vec_IntPush( vBlacks, Wlc_ObjId(p, pObj) ), Count[0]++; + continue; + } + if ( pObj->Type == WLC_OBJ_ARI_MULTI || pObj->Type == WLC_OBJ_ARI_DIVIDE || pObj->Type == WLC_OBJ_ARI_REM || pObj->Type == WLC_OBJ_ARI_MODULUS ) + { + if ( Wlc_ObjRange(pObj) >= pPars->nBitsMul ) + Vec_IntPush( vBlacks, Wlc_ObjId(p, pObj) ), Count[1]++; + continue; + } + if ( pObj->Type == WLC_OBJ_MUX ) + { + if ( Wlc_ObjRange(pObj) >= pPars->nBitsMux ) + Vec_IntPush( vBlacks, Wlc_ObjId(p, pObj) ), Count[2]++; + continue; + } + if ( Wlc_ObjIsCi(pObj) && !Wlc_ObjIsPi(pObj) ) + { + if ( Wlc_ObjRange(pObj) >= pPars->nBitsFlop ) + Vec_IntPush( vBlacks, Wlc_ObjId(p, pObj) ), Count[3]++; + continue; + } + } + if ( pPars->fVerbose ) + printf( "Abstraction engine marked %d adds/subs, %d muls/divs, %d muxes, and %d flops to be abstracted away.\n", Count[0], Count[1], Count[2], Count[3] ); + return vBlacks; +} + static Vec_Bit_t * Wlc_NtkAbsMarkOpers( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Bit_t * vUnmark, int fVerbose ) { Vec_Bit_t * vLeaves = Vec_BitStart( Wlc_NtkObjNumMax(p) ); @@ -641,7 +800,8 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) { Aig_Man_t * pAig; Abc_Cex_t * pCex; - Vec_Int_t * vPisNew, * vRefine; + Vec_Int_t * vPisNew = NULL; + Vec_Int_t * vRefine; Gia_Man_t * pGia, * pTemp; Wlc_Ntk_t * pAbs; @@ -649,7 +809,15 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) printf( "\nIteration %d:\n", nIters ); // get abstracted GIA and the set of pseudo-PIs (vPisNew) - pAbs = Wlc_NtkAbs( p, pPars, vUnmark, &vPisNew, &vFfNew, pPars->fVerbose ); + if ( pPars->fProofRefine ) + { + vPisNew = Wlc_NtkGetBlacks( p, pPars, vUnmark ); + pAbs = Wlc_NtkAbs2( p, vPisNew, &vFfNew ); + } + else + { + pAbs = Wlc_NtkAbs( p, pPars, vUnmark, &vPisNew, &vFfNew, pPars->fVerbose ); + } pGia = Wlc_NtkBitBlast( pAbs, NULL, -1, 0, 0, 0, 0 ); // map old flops into new flops @@ -720,7 +888,10 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) } // perform refinement - vRefine = Wlc_NtkAbsRefinement( p, pGia, pCex, vPisNew ); + if ( pPars->fProofRefine ) + vRefine = Wlc_NtkProofRefine( p, pPars, pGia, pCex, vPisNew ); + else + vRefine = Wlc_NtkAbsRefinement( p, pGia, pCex, vPisNew ); Gia_ManStop( pGia ); Vec_IntFree( vPisNew ); if ( vRefine == NULL ) // real CEX @@ -754,7 +925,7 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) Abc_CexFree( pCex ); Aig_ManStop( pAig ); } - + Vec_IntFreeP( &vFfOld ); Vec_BitFree( vUnmark ); // report the result diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c index 32b26b68..99105e39 100644 --- a/src/base/wlc/wlcCom.c +++ b/src/base/wlc/wlcCom.c @@ -462,7 +462,7 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; Wlc_ManSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFIacpmxvwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFIabcpmxvwh" ) ) != EOF ) { switch ( c ) { @@ -524,6 +524,9 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'a': pPars->fPdra ^= 1; break; + case 'b': + pPars->fProofRefine ^= 1; + break; case 'x': pPars->fXorOutput ^= 1; break; @@ -556,7 +559,7 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv ) Wlc_NtkPdrAbs( pNtk, pPars ); return 0; usage: - Abc_Print( -2, "usage: %%pdra [-AMXFI num] [-acpmxvwh]\n" ); + Abc_Print( -2, "usage: %%pdra [-AMXFI num] [-abcpmxvwh]\n" ); Abc_Print( -2, "\t abstraction for word-level networks\n" ); Abc_Print( -2, "\t-A num : minimum bit-width of an adder/subtractor to abstract [default = %d]\n", pPars->nBitsAdd ); Abc_Print( -2, "\t-M num : minimum bit-width of a multiplier to abstract [default = %d]\n", pPars->nBitsMul ); @@ -564,7 +567,8 @@ usage: Abc_Print( -2, "\t-F num : minimum bit-width of a flip-flop to abstract [default = %d]\n", pPars->nBitsFlop ); Abc_Print( -2, "\t-I num : maximum number of CEGAR iterations [default = %d]\n", pPars->nIterMax ); Abc_Print( -2, "\t-x : toggle XORing outputs of word-level miter [default = %s]\n", pPars->fXorOutput? "yes": "no" ); - Abc_Print( -2, "\t-a : toggle running pdr with -nct [default = %s]\n", pPars->fPdra? "yes": "no" ); + Abc_Print( -2, "\t-a : toggle running pdr with -nct [default = %s]\n", pPars->fPdra? "yes": "no" ); + Abc_Print( -2, "\t-b : toggle using proof-based refinement [default = %s]\n", pPars->fProofRefine? "yes": "no" ); Abc_Print( -2, "\t-c : toggle checking clauses in the reloaded trace [default = %s]\n", pPars->fCheckClauses? "yes": "no" ); Abc_Print( -2, "\t-p : toggle pushing clauses in the reloaded trace [default = %s]\n", pPars->fPushClauses? "yes": "no" ); Abc_Print( -2, "\t-m : toggle refining the whole MFFC of a PPI [default = %s]\n", pPars->fMFFC? "yes": "no" ); diff --git a/src/base/wlc/wlcNtk.c b/src/base/wlc/wlcNtk.c index 4d7604b2..1b5317e2 100644 --- a/src/base/wlc/wlcNtk.c +++ b/src/base/wlc/wlcNtk.c @@ -108,18 +108,19 @@ char * Wlc_ObjTypeName( Wlc_Obj_t * p ) { return Wlc_Names[p->Type]; } void Wlc_ManSetDefaultParams( Wlc_Par_t * pPars ) { memset( pPars, 0, sizeof(Wlc_Par_t) ); - pPars->nBitsAdd = ABC_INFINITY; // adder bit-width - pPars->nBitsMul = ABC_INFINITY; // multiplier bit-widht - pPars->nBitsMux = ABC_INFINITY; // MUX bit-width - pPars->nBitsFlop = ABC_INFINITY; // flop bit-width - pPars->nIterMax = 1000; // the max number of iterations - pPars->fXorOutput = 1; // XOR outputs of word-level miter - pPars->fCheckClauses = 1; // Check clauses in the reloaded trace - pPars->fPushClauses = 0; // Push clauses in the reloaded trace - pPars->fMFFC = 1; // Refine the entire MFFC of a PPI - pPars->fPdra = 0; // Use pdr -nct - pPars->fVerbose = 0; // verbose output` - pPars->fPdrVerbose = 0; // show verbose PDR output + pPars->nBitsAdd = ABC_INFINITY; // adder bit-width + pPars->nBitsMul = ABC_INFINITY; // multiplier bit-widht + pPars->nBitsMux = ABC_INFINITY; // MUX bit-width + pPars->nBitsFlop = ABC_INFINITY; // flop bit-width + pPars->nIterMax = 1000; // the max number of iterations + pPars->fXorOutput = 1; // XOR outputs of word-level miter + pPars->fCheckClauses = 1; // Check clauses in the reloaded trace + pPars->fPushClauses = 0; // Push clauses in the reloaded trace + pPars->fMFFC = 1; // Refine the entire MFFC of a PPI + pPars->fPdra = 0; // Use pdr -nct + pPars->fProofRefine = 0; // Use proof-based refinement + pPars->fVerbose = 0; // verbose output` + pPars->fPdrVerbose = 0; // show verbose PDR output } /**Function************************************************************* @@ -832,6 +833,33 @@ void Wlc_NtkDupDfs_rec( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p, int iObj, Vec_Int_t * v Wlc_NtkDupDfs_rec( pNew, p, iFanin, vFanins ); Wlc_ObjDup( pNew, p, iObj, vFanins ); } + +Wlc_Ntk_t * Wlc_NtkDupDfsSimple( Wlc_Ntk_t * p ) +{ + Wlc_Ntk_t * pNew; + Wlc_Obj_t * pObj; + Vec_Int_t * vFanins; + int i; + Wlc_NtkCleanCopy( p ); + vFanins = Vec_IntAlloc( 100 ); + pNew = Wlc_NtkAlloc( p->pName, p->nObjsAlloc ); + pNew->fSmtLib = p->fSmtLib; + Wlc_NtkForEachCi( p, pObj, i ) + Wlc_ObjDup( pNew, p, Wlc_ObjId(p, pObj), vFanins ); + Wlc_NtkForEachCo( p, pObj, i ) + Wlc_NtkDupDfs_rec( pNew, p, Wlc_ObjId(p, pObj), vFanins ); + Wlc_NtkForEachCo( p, pObj, i ) + Wlc_ObjSetCo( pNew, Wlc_ObjCopyObj(pNew, p, pObj), pObj->fIsFi ); + if ( p->vInits ) + pNew->vInits = Vec_IntDup( p->vInits ); + if ( p->pInits ) + pNew->pInits = Abc_UtilStrsav( p->pInits ); + Vec_IntFree( vFanins ); + if ( p->pSpec ) + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + return pNew; +} + Wlc_Ntk_t * Wlc_NtkDupDfs( Wlc_Ntk_t * p, int fMarked, int fSeq ) { Wlc_Ntk_t * pNew; -- cgit v1.2.3 From cba376cfff789b51a6267caf17f163a167c28b59 Mon Sep 17 00:00:00 2001 From: Yen-Sheng Ho Date: Sat, 25 Feb 2017 22:26:51 -0800 Subject: improved %pdra -b --- src/base/wlc/wlcAbs.c | 67 +++++++++++++++++++++++++++++++++------------------ 1 file changed, 43 insertions(+), 24 deletions(-) (limited to 'src/base') diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c index bc6d6717..a929f8c5 100644 --- a/src/base/wlc/wlcAbs.c +++ b/src/base/wlc/wlcAbs.c @@ -49,7 +49,7 @@ int Wlc_NtkNumPiBits( Wlc_Ntk_t * pNtk ) return num; } -static Vec_Int_t * Wlc_NtkGetCoreSels( Gia_Man_t * pFrames, int nFrames, int num_sel_pis, int num_other_pis, int sel_pi_first, int nConfLimit, Wlc_Par_t * pPars ) +static Vec_Int_t * Wlc_NtkGetCoreSels( Gia_Man_t * pFrames, int nFrames, int num_sel_pis, int num_other_pis, Vec_Bit_t * vMark, int sel_pi_first, int nConfLimit, Wlc_Par_t * pPars ) { Vec_Int_t * vCores = NULL; Aig_Man_t * pAigFrames = Gia_ManToAigSimple( pFrames ); @@ -88,11 +88,15 @@ static Vec_Int_t * Wlc_NtkGetCoreSels( Gia_Man_t * pFrames, int nFrames, int num { int cur_pi = first_sel_pi + i; int var = pCnf->pVarNums[Aig_ManCi(pAigFrames, cur_pi)->Id]; + int Lit; assert(var >= 0); Vec_IntWriteEntry( vMapVar2Sel, var, i ); - Vec_IntPush(vLits, toLitCond(var, 0)); + Lit = toLitCond( var, 0 ); + if ( Vec_BitEntry( vMark, i ) ) + Vec_IntPush(vLits, Lit); + else + sat_solver_addclause( pSat, &Lit, &Lit+1 ); } - /* int i, Entry; Abc_Print( 1, "#vLits = %d; vLits = ", Vec_IntSize(vLits) ); @@ -295,12 +299,7 @@ static Wlc_Ntk_t * Wlc_NtkAbs2( Wlc_Ntk_t * pNtk, Vec_Int_t * vBlacks, Vec_Int_t int i, k, iObj, iFanin; Vec_Int_t * vMapNode2Pi = Vec_IntStart( Wlc_NtkObjNumMax(pNtk) ); int nOrigObjNum = Wlc_NtkObjNumMax( pNtk ); - - if ( vNodes == NULL ) - return NULL; - - Wlc_Ntk_t * p = NULL; - p = Wlc_NtkDupDfsSimple( pNtk ); + Wlc_Ntk_t * p = Wlc_NtkDupDfsSimple( pNtk ); Wlc_NtkForEachCi( pNtk, pObj, i ) { @@ -370,30 +369,51 @@ static Wlc_Ntk_t * Wlc_NtkAbs2( Wlc_Ntk_t * pNtk, Vec_Int_t * vBlacks, Vec_Int_t return pNew; } -static Vec_Int_t * Wlc_NtkProofRefine( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Gia_Man_t * pGia, Abc_Cex_t * pCex, Vec_Int_t * vBlacks ) +static int Wlc_NtkProofRefine( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Abc_Cex_t * pCex, Vec_Int_t * vBlacks, Vec_Int_t ** pvRefine ) { - Vec_Int_t * vRefine = Vec_IntAlloc( 100 ); - Wlc_Ntk_t * pNtkWithChoices = Wlc_NtkIntroduceChoices( p, vBlacks ); + Vec_Int_t * vRefine = NULL; + Vec_Bit_t * vUnmark; + Vec_Bit_t * vChoiceMark; + Wlc_Ntk_t * pNtkWithChoices = NULL; Vec_Int_t * vCoreSels; int num_ppis = -1; int Entry, i; + + if ( *pvRefine == NULL ) + return 0; + + vUnmark = Vec_BitStart( Wlc_NtkObjNumMax( p ) ); + vChoiceMark = Vec_BitStart( Vec_IntSize( vBlacks ) ); + + Vec_IntForEachEntry( *pvRefine, Entry, i ) + Vec_BitWriteEntry( vUnmark, Entry, 1 ); + + Vec_IntForEachEntry( vBlacks, Entry, i ) + { + if ( Vec_BitEntry( vUnmark, Entry ) ) + Vec_BitWriteEntry( vChoiceMark, i, 1 ); + } + + pNtkWithChoices = Wlc_NtkIntroduceChoices( p, vBlacks ); Gia_Man_t * pGiaFrames = Wlc_NtkUnrollWithCex( pNtkWithChoices, pCex, Wlc_NtkNumPiBits( p ), Vec_IntSize( vBlacks ), &num_ppis, 0 ); - vCoreSels = Wlc_NtkGetCoreSels( pGiaFrames, pCex->iFrame+1, Vec_IntSize( vBlacks ), num_ppis, 0, 0, pPars ); + vCoreSels = Wlc_NtkGetCoreSels( pGiaFrames, pCex->iFrame+1, Vec_IntSize( vBlacks ), num_ppis, vChoiceMark, 0, 0, pPars ); + Wlc_NtkFree( pNtkWithChoices ); + Gia_ManStop( pGiaFrames ); + Vec_BitFree( vUnmark ); + Vec_BitFree( vChoiceMark ); + + assert( Vec_IntSize( vCoreSels ) ); + vRefine = Vec_IntAlloc( 100 ); Vec_IntForEachEntry( vCoreSels, Entry, i ) Vec_IntPush( vRefine, Vec_IntEntry( vBlacks, Entry ) ); - Wlc_NtkFree( pNtkWithChoices ); - Gia_ManStop( pGiaFrames ); Vec_IntFree( vCoreSels ); - if ( Vec_IntSize( vRefine ) == 0 ) - { - Vec_IntFree( vRefine ); - vRefine = NULL; - } + Vec_IntFree( *pvRefine ); + *pvRefine = vRefine; - return vRefine; + return 0; } /**Function************************************************************* @@ -888,10 +908,9 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) } // perform refinement + vRefine = Wlc_NtkAbsRefinement( p, pGia, pCex, vPisNew ); if ( pPars->fProofRefine ) - vRefine = Wlc_NtkProofRefine( p, pPars, pGia, pCex, vPisNew ); - else - vRefine = Wlc_NtkAbsRefinement( p, pGia, pCex, vPisNew ); + Wlc_NtkProofRefine( p, pPars, pCex, vPisNew, &vRefine ); Gia_ManStop( pGia ); Vec_IntFree( vPisNew ); if ( vRefine == NULL ) // real CEX -- cgit v1.2.3 From 27bdffd5a20d34acaffd08de87565922ba9cd5fc Mon Sep 17 00:00:00 2001 From: Yen-Sheng Ho Date: Sun, 26 Feb 2017 14:38:38 -0800 Subject: small tweaks --- src/base/wlc/wlcAbs.c | 69 +++++++++++++++++++++++++++++++++++++++++++-------- 1 file changed, 58 insertions(+), 11 deletions(-) (limited to 'src/base') diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c index a929f8c5..b02c3662 100644 --- a/src/base/wlc/wlcAbs.c +++ b/src/base/wlc/wlcAbs.c @@ -410,25 +410,51 @@ static int Wlc_NtkProofRefine( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Abc_Cex_t * pCe Vec_IntFree( vCoreSels ); + if ( pPars->fVerbose ) + Abc_Print( 1, "Proof-based refinement reduces %d (out of %d) white boxes\n", Vec_IntSize( *pvRefine ) - Vec_IntSize( vRefine ), Vec_IntSize( *pvRefine ) ); + Vec_IntFree( *pvRefine ); *pvRefine = vRefine; return 0; } -/**Function************************************************************* +static int Wlc_NtkUpdateBlacks( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Int_t ** pvBlacks, Vec_Bit_t * vUnmark ) +{ + int Entry, i; + Wlc_Obj_t * pObj; int Count[4] = {0}; + Vec_Int_t * vBlacks = Vec_IntAlloc( 100 ); - Synopsis [Mark operators that meet the abstraction criteria.] + assert( *pvBlacks ); - Description [This procedure returns the array of objects (vLeaves) that - should be abstracted because of their high bit-width. It uses input array (vUnmark) - to not abstract those objects that have been refined in the previous rounds.] - - SideEffects [] + Vec_IntForEachEntry( *pvBlacks, Entry, i ) + { + if ( Vec_BitEntry( vUnmark, Entry) ) + continue; + Vec_IntPush( vBlacks, Entry ); - SeeAlso [] + pObj = Wlc_NtkObj( p, Entry ); + if ( pObj->Type == WLC_OBJ_ARI_ADD || pObj->Type == WLC_OBJ_ARI_SUB || pObj->Type == WLC_OBJ_ARI_MINUS ) + Count[0]++; + else if ( pObj->Type == WLC_OBJ_ARI_MULTI || pObj->Type == WLC_OBJ_ARI_DIVIDE || pObj->Type == WLC_OBJ_ARI_REM || pObj->Type == WLC_OBJ_ARI_MODULUS ) + Count[1]++; + else if ( pObj->Type == WLC_OBJ_MUX ) + Count[2]++; + else if ( Wlc_ObjIsCi(pObj) && !Wlc_ObjIsPi(pObj) ) + Count[3]++; + } + + assert( Vec_IntSize( vBlacks ) ); + + Vec_IntFree( *pvBlacks ); + *pvBlacks = vBlacks; + + if ( pPars->fVerbose ) + printf( "Abstraction engine marked %d adds/subs, %d muls/divs, %d muxes, and %d flops to be abstracted away.\n", Count[0], Count[1], Count[2], Count[3] ); + + return 0; +} -***********************************************************************/ static Vec_Int_t * Wlc_NtkGetBlacks( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Bit_t * vUnmark ) { Vec_Int_t * vBlacks = Vec_IntAlloc( 100 ) ; @@ -468,6 +494,20 @@ static Vec_Int_t * Wlc_NtkGetBlacks( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Bit_t return vBlacks; } +/**Function************************************************************* + + Synopsis [Mark operators that meet the abstraction criteria.] + + Description [This procedure returns the array of objects (vLeaves) that + should be abstracted because of their high bit-width. It uses input array (vUnmark) + to not abstract those objects that have been refined in the previous rounds.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ + static Vec_Bit_t * Wlc_NtkAbsMarkOpers( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Bit_t * vUnmark, int fVerbose ) { Vec_Bit_t * vLeaves = Vec_BitStart( Wlc_NtkObjNumMax(p) ); @@ -797,6 +837,7 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) Pdr_Man_t * pPdr; Vec_Vec_t * vClauses = NULL; Vec_Int_t * vFfOld = NULL, * vFfNew = NULL, * vMap = NULL; + Vec_Int_t * vBlacks = NULL; int nIters, nNodes, nDcFlops, RetValue = -1, nGiaFfNumOld = -1; // start the bitmap to mark objects that cannot be abstracted because of refinement // currently, this bitmap is empty because abstraction begins without refinement @@ -831,8 +872,12 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) // get abstracted GIA and the set of pseudo-PIs (vPisNew) if ( pPars->fProofRefine ) { - vPisNew = Wlc_NtkGetBlacks( p, pPars, vUnmark ); - pAbs = Wlc_NtkAbs2( p, vPisNew, &vFfNew ); + if ( vBlacks == NULL ) + vBlacks = Wlc_NtkGetBlacks( p, pPars, vUnmark ); + else + Wlc_NtkUpdateBlacks( p, pPars, &vBlacks, vUnmark ); + pAbs = Wlc_NtkAbs2( p, vBlacks, &vFfNew ); + vPisNew = Vec_IntDup( vBlacks ); } else { @@ -945,6 +990,8 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) Aig_ManStop( pAig ); } + if ( vBlacks ) + Vec_IntFree( vBlacks ); Vec_IntFreeP( &vFfOld ); Vec_BitFree( vUnmark ); // report the result -- cgit v1.2.3 From 86b3cb3da999b1d5f3e59ff7dacfca00e9c321d6 Mon Sep 17 00:00:00 2001 From: Yen-Sheng Ho Date: Sun, 26 Feb 2017 15:39:48 -0800 Subject: added an option -L to %pdra for limiting the number of muxes --- src/base/wlc/wlc.h | 1 + src/base/wlc/wlcAbs.c | 70 ++++++++++++++++++++++++++++++++++++++++++++++++++- src/base/wlc/wlcCom.c | 16 ++++++++++-- src/base/wlc/wlcNtk.c | 1 + 4 files changed, 85 insertions(+), 3 deletions(-) (limited to 'src/base') diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h index 71273f98..49ad5bf0 100644 --- a/src/base/wlc/wlc.h +++ b/src/base/wlc/wlc.h @@ -169,6 +169,7 @@ struct Wlc_Par_t_ int nBitsMux; // MUX bit-width int nBitsFlop; // flop bit-width int nIterMax; // the max number of iterations + int nMuxLimit; // the max number of muxes int fXorOutput; // XOR outputs of word-level miter int fCheckClauses; // Check clauses in the reloaded trace int fPushClauses; // Push clauses in the reloaded trace diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c index b02c3662..bb3a6368 100644 --- a/src/base/wlc/wlcAbs.c +++ b/src/base/wlc/wlcAbs.c @@ -34,6 +34,18 @@ extern Vec_Vec_t * IPdr_ManSaveClauses( Pdr_Man_t * p, int fDropLast ); extern int IPdr_ManRestore( Pdr_Man_t * p, Vec_Vec_t * vClauses, Vec_Int_t * vMap ); extern int IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPushClauses ); +typedef struct Int_Pair_t_ Int_Pair_t; +struct Int_Pair_t_ +{ + int first; + int second; +}; + +int IntPairPtrCompare ( Int_Pair_t ** a, Int_Pair_t ** b ) +{ + return (*a)->second < (*b)->second; +} + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -455,10 +467,59 @@ static int Wlc_NtkUpdateBlacks( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Int_t ** p return 0; } +static Vec_Bit_t * Wlc_NtkMarkMuxes( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) +{ + Vec_Bit_t * vMuxMark = NULL; + Vec_Ptr_t * vMuxes = Vec_PtrAlloc( 1000 ); + Wlc_Obj_t * pObj; int i; + Int_Pair_t * pPair; + + if ( pPars->nMuxLimit == ABC_INFINITY ) + return NULL; + + vMuxMark = Vec_BitStart( Wlc_NtkObjNumMax( p ) ); + + Wlc_NtkForEachObj( p, pObj, i ) + { + if ( pObj->Type == WLC_OBJ_MUX ) { + if ( Wlc_ObjRange(pObj) >= pPars->nBitsMux ) + { + pPair = ABC_ALLOC( Int_Pair_t, 1 ); + pPair->first = i; + pPair->second = Wlc_ObjRange( pObj ); + Vec_PtrPush( vMuxes, pPair ); + } + } + } + + Vec_PtrSort( vMuxes, (int (*)(void))IntPairPtrCompare ) ; + + Vec_PtrForEachEntry( Int_Pair_t *, vMuxes, pPair, i ) + { + if ( i >= pPars->nMuxLimit ) + break; + + Vec_BitWriteEntry( vMuxMark, pPair->first, 1 ); + } + + if ( i && pPars->fVerbose ) + Abc_Print( 1, "%%PDRA: %d-th MUX has width = %d\n", i, pPair->second ); + + Vec_PtrForEachEntry( Int_Pair_t *, vMuxes, pPair, i ) + ABC_FREE( pPair ); + Vec_PtrFree( vMuxes ); + + return vMuxMark; +} + static Vec_Int_t * Wlc_NtkGetBlacks( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Bit_t * vUnmark ) { Vec_Int_t * vBlacks = Vec_IntAlloc( 100 ) ; Wlc_Obj_t * pObj; int i, Count[4] = {0}; + Vec_Bit_t * vMuxMark = NULL; + + vMuxMark = Wlc_NtkMarkMuxes( p, pPars ) ; + Wlc_NtkForEachObj( p, pObj, i ) { if ( vUnmark && Vec_BitEntry(vUnmark, i) ) // not allow this object to be abstracted away @@ -479,7 +540,12 @@ static Vec_Int_t * Wlc_NtkGetBlacks( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Bit_t if ( pObj->Type == WLC_OBJ_MUX ) { if ( Wlc_ObjRange(pObj) >= pPars->nBitsMux ) - Vec_IntPush( vBlacks, Wlc_ObjId(p, pObj) ), Count[2]++; + { + if ( vMuxMark == NULL ) + Vec_IntPush( vBlacks, Wlc_ObjId(p, pObj) ), Count[2]++; + else if ( Vec_BitEntry( vMuxMark, i ) ) + Vec_IntPush( vBlacks, Wlc_ObjId(p, pObj) ), Count[2]++; + } continue; } if ( Wlc_ObjIsCi(pObj) && !Wlc_ObjIsPi(pObj) ) @@ -489,6 +555,8 @@ static Vec_Int_t * Wlc_NtkGetBlacks( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Bit_t continue; } } + if ( vMuxMark ) + Vec_BitFree( vMuxMark ); if ( pPars->fVerbose ) printf( "Abstraction engine marked %d adds/subs, %d muls/divs, %d muxes, and %d flops to be abstracted away.\n", Count[0], Count[1], Count[2], Count[3] ); return vBlacks; diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c index 99105e39..0528b4c4 100644 --- a/src/base/wlc/wlcCom.c +++ b/src/base/wlc/wlcCom.c @@ -462,7 +462,7 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; Wlc_ManSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFIabcpmxvwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFILabcpmxvwh" ) ) != EOF ) { switch ( c ) { @@ -521,6 +521,17 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->nIterMax < 0 ) goto usage; break; + case 'L': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nMuxLimit = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nMuxLimit < 0 ) + goto usage; + break; case 'a': pPars->fPdra ^= 1; break; @@ -559,13 +570,14 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv ) Wlc_NtkPdrAbs( pNtk, pPars ); return 0; usage: - Abc_Print( -2, "usage: %%pdra [-AMXFI num] [-abcpmxvwh]\n" ); + Abc_Print( -2, "usage: %%pdra [-AMXFIL num] [-abcpmxvwh]\n" ); Abc_Print( -2, "\t abstraction for word-level networks\n" ); Abc_Print( -2, "\t-A num : minimum bit-width of an adder/subtractor to abstract [default = %d]\n", pPars->nBitsAdd ); Abc_Print( -2, "\t-M num : minimum bit-width of a multiplier to abstract [default = %d]\n", pPars->nBitsMul ); Abc_Print( -2, "\t-X num : minimum bit-width of a MUX operator to abstract [default = %d]\n", pPars->nBitsMux ); Abc_Print( -2, "\t-F num : minimum bit-width of a flip-flop to abstract [default = %d]\n", pPars->nBitsFlop ); Abc_Print( -2, "\t-I num : maximum number of CEGAR iterations [default = %d]\n", pPars->nIterMax ); + Abc_Print( -2, "\t-L num : maximum number of muxes [default = %d]\n", pPars->nMuxLimit ); Abc_Print( -2, "\t-x : toggle XORing outputs of word-level miter [default = %s]\n", pPars->fXorOutput? "yes": "no" ); Abc_Print( -2, "\t-a : toggle running pdr with -nct [default = %s]\n", pPars->fPdra? "yes": "no" ); Abc_Print( -2, "\t-b : toggle using proof-based refinement [default = %s]\n", pPars->fProofRefine? "yes": "no" ); diff --git a/src/base/wlc/wlcNtk.c b/src/base/wlc/wlcNtk.c index 1b5317e2..9605ce7a 100644 --- a/src/base/wlc/wlcNtk.c +++ b/src/base/wlc/wlcNtk.c @@ -113,6 +113,7 @@ void Wlc_ManSetDefaultParams( Wlc_Par_t * pPars ) pPars->nBitsMux = ABC_INFINITY; // MUX bit-width pPars->nBitsFlop = ABC_INFINITY; // flop bit-width pPars->nIterMax = 1000; // the max number of iterations + pPars->nMuxLimit = ABC_INFINITY; // the max number of muxes pPars->fXorOutput = 1; // XOR outputs of word-level miter pPars->fCheckClauses = 1; // Check clauses in the reloaded trace pPars->fPushClauses = 0; // Push clauses in the reloaded trace -- cgit v1.2.3 From ff745ca1a596b124a72b54fecd27b0fcdf4412ad Mon Sep 17 00:00:00 2001 From: Yen-Sheng Ho Date: Sun, 26 Feb 2017 15:45:35 -0800 Subject: fixed a bug --- src/base/wlc/wlcAbs.c | 2 -- 1 file changed, 2 deletions(-) (limited to 'src/base') diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c index bb3a6368..410d1d22 100644 --- a/src/base/wlc/wlcAbs.c +++ b/src/base/wlc/wlcAbs.c @@ -456,8 +456,6 @@ static int Wlc_NtkUpdateBlacks( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Int_t ** p Count[3]++; } - assert( Vec_IntSize( vBlacks ) ); - Vec_IntFree( *pvBlacks ); *pvBlacks = vBlacks; -- cgit v1.2.3 From ed31679759150284161c20920c9c3a4d61cb6ae8 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 27 Feb 2017 12:18:24 -0800 Subject: Enabling LUT pairing. --- src/base/abci/abc.c | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'src/base') diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 003842f0..2efa041c 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -61,6 +61,7 @@ #include "bool/rpo/rpo.h" #include "map/mpm/mpm.h" #include "opt/fret/fretime.h" +#include "opt/nwk/nwkMerge.h" #ifndef _WIN32 #include @@ -124,7 +125,7 @@ static int Abc_CommandTrace ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandSpeedup ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandPowerdown ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAddBuffs ( Abc_Frame_t * pAbc, int argc, char ** argv ); -//static int Abc_CommandMerge ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandMerge ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandTestDec ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandTestNpn ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandTestRPO ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -774,7 +775,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Synthesis", "speedup", Abc_CommandSpeedup, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "powerdown", Abc_CommandPowerdown, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "addbuffs", Abc_CommandAddBuffs, 1 ); -// Cmd_CommandAdd( pAbc, "Synthesis", "merge", Abc_CommandMerge, 1 ); + Cmd_CommandAdd( pAbc, "Synthesis", "merge", Abc_CommandMerge, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "testdec", Abc_CommandTestDec, 0 ); Cmd_CommandAdd( pAbc, "Synthesis", "testnpn", Abc_CommandTestNpn, 0 ); Cmd_CommandAdd( pAbc, "LogiCS", "testrpo", Abc_CommandTestRPO, 0 ); @@ -6011,7 +6012,7 @@ usage: return 1; } -#if 0 +//#if 0 /**Function************************************************************* Synopsis [] @@ -6144,7 +6145,7 @@ usage: Abc_Print( -2, "\t-h : print the command usage\n"); return 1; } -#endif +//#endif -- cgit v1.2.3 From bb3eacf480360a51ea2c131bb4b4feff213d3170 Mon Sep 17 00:00:00 2001 From: Yen-Sheng Ho Date: Mon, 27 Feb 2017 13:45:22 -0800 Subject: small tweaks --- src/base/wlc/wlcAbs.c | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'src/base') diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c index 410d1d22..333c3a48 100644 --- a/src/base/wlc/wlcAbs.c +++ b/src/base/wlc/wlcAbs.c @@ -460,7 +460,7 @@ static int Wlc_NtkUpdateBlacks( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Int_t ** p *pvBlacks = vBlacks; if ( pPars->fVerbose ) - printf( "Abstraction engine marked %d adds/subs, %d muls/divs, %d muxes, and %d flops to be abstracted away.\n", Count[0], Count[1], Count[2], Count[3] ); + printf( "Abstraction engine marked %d adds/subs, %d muls/divs, %d muxes, and %d flops to be abstracted away.\n", Count[0], Count[1], Count[2], Vec_IntSize( vBlacks ) - Count[0] - Count[1] - Count[2] ); return 0; } @@ -526,13 +526,13 @@ static Vec_Int_t * Wlc_NtkGetBlacks( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Bit_t if ( pObj->Type == WLC_OBJ_ARI_ADD || pObj->Type == WLC_OBJ_ARI_SUB || pObj->Type == WLC_OBJ_ARI_MINUS ) { if ( Wlc_ObjRange(pObj) >= pPars->nBitsAdd ) - Vec_IntPush( vBlacks, Wlc_ObjId(p, pObj) ), Count[0]++; + Vec_IntPushUniqueOrder( vBlacks, Wlc_ObjId(p, pObj) ), Count[0]++; continue; } if ( pObj->Type == WLC_OBJ_ARI_MULTI || pObj->Type == WLC_OBJ_ARI_DIVIDE || pObj->Type == WLC_OBJ_ARI_REM || pObj->Type == WLC_OBJ_ARI_MODULUS ) { if ( Wlc_ObjRange(pObj) >= pPars->nBitsMul ) - Vec_IntPush( vBlacks, Wlc_ObjId(p, pObj) ), Count[1]++; + Vec_IntPushUniqueOrder( vBlacks, Wlc_ObjId(p, pObj) ), Count[1]++; continue; } if ( pObj->Type == WLC_OBJ_MUX ) @@ -540,16 +540,16 @@ static Vec_Int_t * Wlc_NtkGetBlacks( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Bit_t if ( Wlc_ObjRange(pObj) >= pPars->nBitsMux ) { if ( vMuxMark == NULL ) - Vec_IntPush( vBlacks, Wlc_ObjId(p, pObj) ), Count[2]++; + Vec_IntPushUniqueOrder( vBlacks, Wlc_ObjId(p, pObj) ), Count[2]++; else if ( Vec_BitEntry( vMuxMark, i ) ) - Vec_IntPush( vBlacks, Wlc_ObjId(p, pObj) ), Count[2]++; + Vec_IntPushUniqueOrder( vBlacks, Wlc_ObjId(p, pObj) ), Count[2]++; } continue; } if ( Wlc_ObjIsCi(pObj) && !Wlc_ObjIsPi(pObj) ) { if ( Wlc_ObjRange(pObj) >= pPars->nBitsFlop ) - Vec_IntPush( vBlacks, Wlc_ObjId(p, pObj) ), Count[3]++; + Vec_IntPushUniqueOrder( vBlacks, Wlc_ObjId( p, Wlc_ObjFo2Fi( p, pObj ) ) ), Count[3]++; continue; } } -- cgit v1.2.3 From 9195192f65bed0c5f3ca2fd8f8b51b34b94f47b3 Mon Sep 17 00:00:00 2001 From: Yen-Sheng Ho Date: Mon, 27 Feb 2017 14:31:59 -0800 Subject: %pdra -L: now applies to all types --- src/base/wlc/wlc.h | 2 +- src/base/wlc/wlcAbs.c | 128 +++++++++++++++++++++++++++++++++++++++----------- src/base/wlc/wlcCom.c | 6 +-- src/base/wlc/wlcNtk.c | 2 +- 4 files changed, 105 insertions(+), 33 deletions(-) (limited to 'src/base') diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h index 49ad5bf0..1a2bc505 100644 --- a/src/base/wlc/wlc.h +++ b/src/base/wlc/wlc.h @@ -169,7 +169,7 @@ struct Wlc_Par_t_ int nBitsMux; // MUX bit-width int nBitsFlop; // flop bit-width int nIterMax; // the max number of iterations - int nMuxLimit; // the max number of muxes + int nLimit; // the max number of signals int fXorOutput; // XOR outputs of word-level miter int fCheckClauses; // Check clauses in the reloaded trace int fPushClauses; // Push clauses in the reloaded trace diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c index 333c3a48..c599b9a0 100644 --- a/src/base/wlc/wlcAbs.c +++ b/src/base/wlc/wlcAbs.c @@ -465,21 +465,45 @@ static int Wlc_NtkUpdateBlacks( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Int_t ** p return 0; } -static Vec_Bit_t * Wlc_NtkMarkMuxes( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) +static Vec_Bit_t * Wlc_NtkMarkLimit( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) { - Vec_Bit_t * vMuxMark = NULL; + Vec_Bit_t * vMarks = NULL; + Vec_Ptr_t * vAdds = Vec_PtrAlloc( 1000 ); Vec_Ptr_t * vMuxes = Vec_PtrAlloc( 1000 ); + Vec_Ptr_t * vMults = Vec_PtrAlloc( 1000 ); + Vec_Ptr_t * vFlops = Vec_PtrAlloc( 1000 ); Wlc_Obj_t * pObj; int i; Int_Pair_t * pPair; - if ( pPars->nMuxLimit == ABC_INFINITY ) + if ( pPars->nLimit == ABC_INFINITY ) return NULL; - vMuxMark = Vec_BitStart( Wlc_NtkObjNumMax( p ) ); + vMarks = Vec_BitStart( Wlc_NtkObjNumMax( p ) ); Wlc_NtkForEachObj( p, pObj, i ) { - if ( pObj->Type == WLC_OBJ_MUX ) { + if ( pObj->Type == WLC_OBJ_ARI_ADD || pObj->Type == WLC_OBJ_ARI_SUB || pObj->Type == WLC_OBJ_ARI_MINUS ) + { + if ( Wlc_ObjRange(pObj) >= pPars->nBitsAdd ) + { + pPair = ABC_ALLOC( Int_Pair_t, 1 ); + pPair->first = i; + pPair->second = Wlc_ObjRange( pObj ); + Vec_PtrPush( vAdds, pPair ); + } + } + else if ( pObj->Type == WLC_OBJ_ARI_MULTI || pObj->Type == WLC_OBJ_ARI_DIVIDE || pObj->Type == WLC_OBJ_ARI_REM || pObj->Type == WLC_OBJ_ARI_MODULUS ) + { + if ( Wlc_ObjRange(pObj) >= pPars->nBitsMul ) + { + pPair = ABC_ALLOC( Int_Pair_t, 1 ); + pPair->first = i; + pPair->second = Wlc_ObjRange( pObj ); + Vec_PtrPush( vMults, pPair ); + } + } + else if ( pObj->Type == WLC_OBJ_MUX ) + { if ( Wlc_ObjRange(pObj) >= pPars->nBitsMux ) { pPair = ABC_ALLOC( Int_Pair_t, 1 ); @@ -488,60 +512,103 @@ static Vec_Bit_t * Wlc_NtkMarkMuxes( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) Vec_PtrPush( vMuxes, pPair ); } } + else if ( Wlc_ObjIsCi(pObj) && !Wlc_ObjIsPi(pObj) ) + { + if ( Wlc_ObjRange(pObj) >= pPars->nBitsFlop ) + { + pPair = ABC_ALLOC( Int_Pair_t, 1 ); + pPair->first = i; + pPair->second = Wlc_ObjRange( pObj ); + Vec_PtrPush( vFlops, pPair ); + } + } } + Vec_PtrSort( vAdds, (int (*)(void))IntPairPtrCompare ) ; + Vec_PtrSort( vMults, (int (*)(void))IntPairPtrCompare ) ; Vec_PtrSort( vMuxes, (int (*)(void))IntPairPtrCompare ) ; + Vec_PtrSort( vFlops, (int (*)(void))IntPairPtrCompare ) ; - Vec_PtrForEachEntry( Int_Pair_t *, vMuxes, pPair, i ) + Vec_PtrForEachEntry( Int_Pair_t *, vAdds, pPair, i ) { - if ( i >= pPars->nMuxLimit ) - break; - - Vec_BitWriteEntry( vMuxMark, pPair->first, 1 ); + if ( i >= pPars->nLimit ) break; + Vec_BitWriteEntry( vMarks, pPair->first, 1 ); } + if ( i && pPars->fVerbose ) Abc_Print( 1, "%%PDRA: %d-th ADD has width = %d\n", i, pPair->second ); - if ( i && pPars->fVerbose ) - Abc_Print( 1, "%%PDRA: %d-th MUX has width = %d\n", i, pPair->second ); + Vec_PtrForEachEntry( Int_Pair_t *, vMults, pPair, i ) + { + if ( i >= pPars->nLimit ) break; + Vec_BitWriteEntry( vMarks, pPair->first, 1 ); + } + if ( i && pPars->fVerbose ) Abc_Print( 1, "%%PDRA: %d-th MUL has width = %d\n", i, pPair->second ); Vec_PtrForEachEntry( Int_Pair_t *, vMuxes, pPair, i ) - ABC_FREE( pPair ); + { + if ( i >= pPars->nLimit ) break; + Vec_BitWriteEntry( vMarks, pPair->first, 1 ); + } + if ( i && pPars->fVerbose ) Abc_Print( 1, "%%PDRA: %d-th MUX has width = %d\n", i, pPair->second ); + + Vec_PtrForEachEntry( Int_Pair_t *, vFlops, pPair, i ) + { + if ( i >= pPars->nLimit ) break; + Vec_BitWriteEntry( vMarks, pPair->first, 1 ); + } + if ( i && pPars->fVerbose ) Abc_Print( 1, "%%PDRA: %d-th FF has width = %d\n", i, pPair->second ); + + + Vec_PtrForEachEntry( Int_Pair_t *, vAdds, pPair, i ) ABC_FREE( pPair ); + Vec_PtrForEachEntry( Int_Pair_t *, vMults, pPair, i ) ABC_FREE( pPair ); + Vec_PtrForEachEntry( Int_Pair_t *, vMuxes, pPair, i ) ABC_FREE( pPair ); + Vec_PtrForEachEntry( Int_Pair_t *, vFlops, pPair, i ) ABC_FREE( pPair ); + Vec_PtrFree( vAdds ); + Vec_PtrFree( vMults ); Vec_PtrFree( vMuxes ); + Vec_PtrFree( vFlops ); - return vMuxMark; + return vMarks; } -static Vec_Int_t * Wlc_NtkGetBlacks( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Bit_t * vUnmark ) +static Vec_Int_t * Wlc_NtkGetBlacks( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) { Vec_Int_t * vBlacks = Vec_IntAlloc( 100 ) ; Wlc_Obj_t * pObj; int i, Count[4] = {0}; - Vec_Bit_t * vMuxMark = NULL; + Vec_Bit_t * vMarks = NULL; - vMuxMark = Wlc_NtkMarkMuxes( p, pPars ) ; + vMarks = Wlc_NtkMarkLimit( p, pPars ) ; Wlc_NtkForEachObj( p, pObj, i ) { - if ( vUnmark && Vec_BitEntry(vUnmark, i) ) // not allow this object to be abstracted away - continue; - if ( pObj->Type == WLC_OBJ_ARI_ADD || pObj->Type == WLC_OBJ_ARI_SUB || pObj->Type == WLC_OBJ_ARI_MINUS ) { if ( Wlc_ObjRange(pObj) >= pPars->nBitsAdd ) - Vec_IntPushUniqueOrder( vBlacks, Wlc_ObjId(p, pObj) ), Count[0]++; + { + if ( vMarks == NULL ) + Vec_IntPushUniqueOrder( vBlacks, Wlc_ObjId(p, pObj) ), Count[0]++; + else if ( Vec_BitEntry( vMarks, i ) ) + Vec_IntPushUniqueOrder( vBlacks, Wlc_ObjId(p, pObj) ), Count[0]++; + } continue; } if ( pObj->Type == WLC_OBJ_ARI_MULTI || pObj->Type == WLC_OBJ_ARI_DIVIDE || pObj->Type == WLC_OBJ_ARI_REM || pObj->Type == WLC_OBJ_ARI_MODULUS ) { if ( Wlc_ObjRange(pObj) >= pPars->nBitsMul ) - Vec_IntPushUniqueOrder( vBlacks, Wlc_ObjId(p, pObj) ), Count[1]++; + { + if ( vMarks == NULL ) + Vec_IntPushUniqueOrder( vBlacks, Wlc_ObjId(p, pObj) ), Count[1]++; + else if ( Vec_BitEntry( vMarks, i ) ) + Vec_IntPushUniqueOrder( vBlacks, Wlc_ObjId(p, pObj) ), Count[1]++; + } continue; } if ( pObj->Type == WLC_OBJ_MUX ) { if ( Wlc_ObjRange(pObj) >= pPars->nBitsMux ) { - if ( vMuxMark == NULL ) + if ( vMarks == NULL ) Vec_IntPushUniqueOrder( vBlacks, Wlc_ObjId(p, pObj) ), Count[2]++; - else if ( Vec_BitEntry( vMuxMark, i ) ) + else if ( Vec_BitEntry( vMarks, i ) ) Vec_IntPushUniqueOrder( vBlacks, Wlc_ObjId(p, pObj) ), Count[2]++; } continue; @@ -549,12 +616,17 @@ static Vec_Int_t * Wlc_NtkGetBlacks( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Bit_t if ( Wlc_ObjIsCi(pObj) && !Wlc_ObjIsPi(pObj) ) { if ( Wlc_ObjRange(pObj) >= pPars->nBitsFlop ) - Vec_IntPushUniqueOrder( vBlacks, Wlc_ObjId( p, Wlc_ObjFo2Fi( p, pObj ) ) ), Count[3]++; + { + if ( vMarks == NULL ) + Vec_IntPushUniqueOrder( vBlacks, Wlc_ObjId( p, Wlc_ObjFo2Fi( p, pObj ) ) ), Count[3]++; + else if ( Vec_BitEntry( vMarks, i ) ) + Vec_IntPushUniqueOrder( vBlacks, Wlc_ObjId( p, Wlc_ObjFo2Fi( p, pObj ) ) ), Count[3]++; + } continue; } } - if ( vMuxMark ) - Vec_BitFree( vMuxMark ); + if ( vMarks ) + Vec_BitFree( vMarks ); if ( pPars->fVerbose ) printf( "Abstraction engine marked %d adds/subs, %d muls/divs, %d muxes, and %d flops to be abstracted away.\n", Count[0], Count[1], Count[2], Count[3] ); return vBlacks; @@ -939,7 +1011,7 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) if ( pPars->fProofRefine ) { if ( vBlacks == NULL ) - vBlacks = Wlc_NtkGetBlacks( p, pPars, vUnmark ); + vBlacks = Wlc_NtkGetBlacks( p, pPars ); else Wlc_NtkUpdateBlacks( p, pPars, &vBlacks, vUnmark ); pAbs = Wlc_NtkAbs2( p, vBlacks, &vFfNew ); diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c index 0528b4c4..0bad60bf 100644 --- a/src/base/wlc/wlcCom.c +++ b/src/base/wlc/wlcCom.c @@ -527,9 +527,9 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" ); goto usage; } - pPars->nMuxLimit = atoi(argv[globalUtilOptind]); + pPars->nLimit = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( pPars->nMuxLimit < 0 ) + if ( pPars->nLimit < 0 ) goto usage; break; case 'a': @@ -577,7 +577,7 @@ usage: Abc_Print( -2, "\t-X num : minimum bit-width of a MUX operator to abstract [default = %d]\n", pPars->nBitsMux ); Abc_Print( -2, "\t-F num : minimum bit-width of a flip-flop to abstract [default = %d]\n", pPars->nBitsFlop ); Abc_Print( -2, "\t-I num : maximum number of CEGAR iterations [default = %d]\n", pPars->nIterMax ); - Abc_Print( -2, "\t-L num : maximum number of muxes [default = %d]\n", pPars->nMuxLimit ); + Abc_Print( -2, "\t-L num : maximum number of each type of signals [default = %d]\n", pPars->nLimit ); Abc_Print( -2, "\t-x : toggle XORing outputs of word-level miter [default = %s]\n", pPars->fXorOutput? "yes": "no" ); Abc_Print( -2, "\t-a : toggle running pdr with -nct [default = %s]\n", pPars->fPdra? "yes": "no" ); Abc_Print( -2, "\t-b : toggle using proof-based refinement [default = %s]\n", pPars->fProofRefine? "yes": "no" ); diff --git a/src/base/wlc/wlcNtk.c b/src/base/wlc/wlcNtk.c index 9605ce7a..02af1a16 100644 --- a/src/base/wlc/wlcNtk.c +++ b/src/base/wlc/wlcNtk.c @@ -113,7 +113,7 @@ void Wlc_ManSetDefaultParams( Wlc_Par_t * pPars ) pPars->nBitsMux = ABC_INFINITY; // MUX bit-width pPars->nBitsFlop = ABC_INFINITY; // flop bit-width pPars->nIterMax = 1000; // the max number of iterations - pPars->nMuxLimit = ABC_INFINITY; // the max number of muxes + pPars->nLimit = ABC_INFINITY; // the max number of signals pPars->fXorOutput = 1; // XOR outputs of word-level miter pPars->fCheckClauses = 1; // Check clauses in the reloaded trace pPars->fPushClauses = 0; // Push clauses in the reloaded trace -- cgit v1.2.3 From 46b6ac1539ec92587a3e95edd2ce76807d7afccc Mon Sep 17 00:00:00 2001 From: Yen-Sheng Ho Date: Mon, 27 Feb 2017 20:44:19 -0800 Subject: improved %pdra -L --- src/base/wlc/wlcAbs.c | 14 ++++++++++++++ 1 file changed, 14 insertions(+) (limited to 'src/base') diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c index c599b9a0..21ae4e4d 100644 --- a/src/base/wlc/wlcAbs.c +++ b/src/base/wlc/wlcAbs.c @@ -570,6 +570,17 @@ static Vec_Bit_t * Wlc_NtkMarkLimit( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) return vMarks; } +static void Wlc_NtkSetUnmark( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Bit_t * vUnmark ) +{ + int Entry, i; + Vec_Bit_t * vMarks = Wlc_NtkMarkLimit( p, pPars ); + + Vec_BitForEachEntry( vMarks, Entry, i ) + Vec_BitWriteEntry( vUnmark, i, Entry^1 ); + + Vec_BitFree( vMarks ); +} + static Vec_Int_t * Wlc_NtkGetBlacks( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) { Vec_Int_t * vBlacks = Vec_IntAlloc( 100 ) ; @@ -1019,6 +1030,9 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) } else { + if ( nIters == 1 && pPars->nLimit < ABC_INFINITY ) + Wlc_NtkSetUnmark( p, pPars, vUnmark ); + pAbs = Wlc_NtkAbs( p, pPars, vUnmark, &vPisNew, &vFfNew, pPars->fVerbose ); } pGia = Wlc_NtkBitBlast( pAbs, NULL, -1, 0, 0, 0, 0 ); -- cgit v1.2.3 From 43f34ddc023552559afa3bb66bee60a4d93f0a93 Mon Sep 17 00:00:00 2001 From: Yen-Sheng Ho Date: Tue, 28 Feb 2017 08:05:33 -0800 Subject: added -L to %abs --- src/base/wlc/wlcAbs.c | 2 ++ src/base/wlc/wlcCom.c | 16 ++++++++++++++-- 2 files changed, 16 insertions(+), 2 deletions(-) (limited to 'src/base') diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c index 21ae4e4d..af5f78dc 100644 --- a/src/base/wlc/wlcAbs.c +++ b/src/base/wlc/wlcAbs.c @@ -1206,6 +1206,8 @@ int Wlc_NtkAbsCore( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) printf( "\nIteration %d:\n", nIters ); // get abstracted GIA and the set of pseudo-PIs (vPisNew) + if ( nIters == 1 && pPars->nLimit < ABC_INFINITY ) + Wlc_NtkSetUnmark( p, pPars, vUnmark ); pAbs = Wlc_NtkAbs( p, pPars, vUnmark, &vPisNew, NULL, pPars->fVerbose ); pGia = Wlc_NtkBitBlast( pAbs, NULL, -1, 0, 0, 0, 0 ); diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c index 0bad60bf..781f4a9a 100644 --- a/src/base/wlc/wlcCom.c +++ b/src/base/wlc/wlcCom.c @@ -609,7 +609,7 @@ int Abc_CommandAbs( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; Wlc_ManSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFIxvwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFILxvwh" ) ) != EOF ) { switch ( c ) { @@ -668,6 +668,17 @@ int Abc_CommandAbs( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->nIterMax < 0 ) goto usage; break; + case 'L': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nLimit = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nLimit < 0 ) + goto usage; + break; case 'x': pPars->fXorOutput ^= 1; break; @@ -691,13 +702,14 @@ int Abc_CommandAbs( Abc_Frame_t * pAbc, int argc, char ** argv ) Wlc_NtkAbsCore( pNtk, pPars ); return 0; usage: - Abc_Print( -2, "usage: %%abs [-AMXFI num] [-xvwh]\n" ); + Abc_Print( -2, "usage: %%abs [-AMXFIL num] [-xvwh]\n" ); Abc_Print( -2, "\t abstraction for word-level networks\n" ); Abc_Print( -2, "\t-A num : minimum bit-width of an adder/subtractor to abstract [default = %d]\n", pPars->nBitsAdd ); Abc_Print( -2, "\t-M num : minimum bit-width of a multiplier to abstract [default = %d]\n", pPars->nBitsMul ); Abc_Print( -2, "\t-X num : minimum bit-width of a MUX operator to abstract [default = %d]\n", pPars->nBitsMux ); Abc_Print( -2, "\t-F num : minimum bit-width of a flip-flop to abstract [default = %d]\n", pPars->nBitsFlop ); Abc_Print( -2, "\t-I num : maximum number of CEGAR iterations [default = %d]\n", pPars->nIterMax ); + Abc_Print( -2, "\t-L num : maximum number of each type of signals [default = %d]\n", pPars->nLimit ); Abc_Print( -2, "\t-x : toggle XORing outputs of word-level miter [default = %s]\n", pPars->fXorOutput? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); Abc_Print( -2, "\t-w : toggle printing verbose PDR output [default = %s]\n", pPars->fPdrVerbose? "yes": "no" ); -- cgit v1.2.3 From d95d51c474fdd5d882b34c8bcbcd27173ba8431c Mon Sep 17 00:00:00 2001 From: Yen-Sheng Ho Date: Tue, 28 Feb 2017 11:30:13 -0800 Subject: improved profiling in %pdra --- src/base/wlc/wlcAbs.c | 30 ++++++++++++++++++++++++++---- 1 file changed, 26 insertions(+), 4 deletions(-) (limited to 'src/base') diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c index af5f78dc..69d1df77 100644 --- a/src/base/wlc/wlcAbs.c +++ b/src/base/wlc/wlcAbs.c @@ -982,7 +982,8 @@ Vec_Int_t * Wlc_NtkFlopsRemap( Wlc_Ntk_t * p, Vec_Int_t * vFfOld, Vec_Int_t * vF int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) { abctime clk = Abc_Clock(); - abctime pdrClk; + abctime clk2; + abctime tPdr = 0, tCbr = 0, tPbr = 0, tTotal = 0; Pdr_Man_t * pPdr; Vec_Vec_t * vClauses = NULL; Vec_Int_t * vFfOld = NULL, * vFfNew = NULL, * vMap = NULL; @@ -1080,7 +1081,7 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) pAig = Gia_ManToAigSimple( pGia ); pPdr = Pdr_ManStart( pAig, pPdrPars, NULL ); - pdrClk = Abc_Clock(); + clk2 = Abc_Clock(); if ( vClauses ) { assert( Vec_VecSize( vClauses) >= 2 ); @@ -1089,7 +1090,8 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) Vec_IntFreeP( &vMap ); RetValue = IPdr_ManSolveInt( pPdr, pPars->fCheckClauses, pPars->fPushClauses ); - pPdr->tTotal += Abc_Clock() - pdrClk; + pPdr->tTotal += Abc_Clock() - clk2; + tPdr += pPdr->tTotal; pCex = pAig->pSeqModel; pAig->pSeqModel = NULL; @@ -1105,9 +1107,15 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) } // perform refinement + clk2 = Abc_Clock(); vRefine = Wlc_NtkAbsRefinement( p, pGia, pCex, vPisNew ); + tCbr += Abc_Clock() - clk2; if ( pPars->fProofRefine ) + { + clk2 = Abc_Clock(); Wlc_NtkProofRefine( p, pPars, pCex, vPisNew, &vRefine ); + tPbr += Abc_Clock() - clk2; + } Gia_ManStop( pGia ); Vec_IntFree( vPisNew ); if ( vRefine == NULL ) // real CEX @@ -1124,6 +1132,7 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) Pdr_ManStop( pPdr ); // update the set of objects to be un-abstracted + clk2 = Abc_Clock(); if ( pPars->fMFFC ) { nNodes = Wlc_NtkRemoveFromAbstraction( p, vRefine, vUnmark ); @@ -1137,6 +1146,8 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) printf( "Refinement of CEX in frame %d came up with %d un-abstacted PPIs.\n", pCex->iFrame, Vec_IntSize(vRefine) ); } + tCbr += Abc_Clock() - clk2; + Vec_IntFree( vRefine ); Abc_CexFree( pCex ); Aig_ManStop( pAig ); @@ -1157,7 +1168,18 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) else printf( "timed out" ); printf( " after %d iterations. ", nIters ); - Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + tTotal = Abc_Clock() - clk; + Abc_PrintTime( 1, "Time", tTotal ); + + if ( pPars->fVerbose ) + { + ABC_PRTP( "PDR ", tPdr, tTotal ); + ABC_PRTP( "CEX Refine ", tCbr, tTotal ); + ABC_PRTP( "Proof Refine ", tPbr, tTotal ); + ABC_PRTP( "Misc. ", tTotal - tPdr - tCbr - tPbr, tTotal ); + ABC_PRTP( "Total ", tTotal, tTotal ); + } + return RetValue; } -- cgit v1.2.3 From 902a78eeb883cb97131e03cc31cf0892787e806e Mon Sep 17 00:00:00 2001 From: Yen-Sheng Ho Date: Tue, 28 Feb 2017 18:05:58 -0800 Subject: added an option -r to %pdra: proof-based refinement only --- src/base/wlc/wlc.h | 9 +++++---- src/base/wlc/wlcAbs.c | 13 ++++++++++--- src/base/wlc/wlcCom.c | 6 +++++- src/base/wlc/wlcNtk.c | 1 + 4 files changed, 21 insertions(+), 8 deletions(-) (limited to 'src/base') diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h index 1a2bc505..f5dbba42 100644 --- a/src/base/wlc/wlc.h +++ b/src/base/wlc/wlc.h @@ -171,11 +171,12 @@ struct Wlc_Par_t_ int nIterMax; // the max number of iterations int nLimit; // the max number of signals int fXorOutput; // XOR outputs of word-level miter - int fCheckClauses; // Check clauses in the reloaded trace - int fPushClauses; // Push clauses in the reloaded trace - int fMFFC; // Refine the entire MFFC of a PPI - int fPdra; // Use pdr -nct + int fCheckClauses; // Check clauses in the reloaded trace + int fPushClauses; // Push clauses in the reloaded trace + int fMFFC; // Refine the entire MFFC of a PPI + int fPdra; // Use pdr -nct int fProofRefine; // Use proof-based refinement + int fHybrid; // Use a hybrid of CBR and PBR int fVerbose; // verbose output int fPdrVerbose; // verbose output }; diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c index 69d1df77..1eb5a964 100644 --- a/src/base/wlc/wlcAbs.c +++ b/src/base/wlc/wlcAbs.c @@ -1107,9 +1107,16 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) } // perform refinement - clk2 = Abc_Clock(); - vRefine = Wlc_NtkAbsRefinement( p, pGia, pCex, vPisNew ); - tCbr += Abc_Clock() - clk2; + if ( pPars->fHybrid || !pPars->fProofRefine ) + { + clk2 = Abc_Clock(); + vRefine = Wlc_NtkAbsRefinement( p, pGia, pCex, vPisNew ); + tCbr += Abc_Clock() - clk2; + } + else // proof-based only + { + vRefine = Vec_IntDup( vPisNew ); + } if ( pPars->fProofRefine ) { clk2 = Abc_Clock(); diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c index 781f4a9a..0c9cdabb 100644 --- a/src/base/wlc/wlcCom.c +++ b/src/base/wlc/wlcCom.c @@ -462,7 +462,7 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; Wlc_ManSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFILabcpmxvwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFILabrcpmxvwh" ) ) != EOF ) { switch ( c ) { @@ -538,6 +538,9 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'b': pPars->fProofRefine ^= 1; break; + case 'r': + pPars->fHybrid ^= 1; + break; case 'x': pPars->fXorOutput ^= 1; break; @@ -581,6 +584,7 @@ usage: Abc_Print( -2, "\t-x : toggle XORing outputs of word-level miter [default = %s]\n", pPars->fXorOutput? "yes": "no" ); Abc_Print( -2, "\t-a : toggle running pdr with -nct [default = %s]\n", pPars->fPdra? "yes": "no" ); Abc_Print( -2, "\t-b : toggle using proof-based refinement [default = %s]\n", pPars->fProofRefine? "yes": "no" ); + Abc_Print( -2, "\t-r : toggle using both cex-based and proof-based refinement [default = %s]\n", pPars->fHybrid? "yes": "no" ); Abc_Print( -2, "\t-c : toggle checking clauses in the reloaded trace [default = %s]\n", pPars->fCheckClauses? "yes": "no" ); Abc_Print( -2, "\t-p : toggle pushing clauses in the reloaded trace [default = %s]\n", pPars->fPushClauses? "yes": "no" ); Abc_Print( -2, "\t-m : toggle refining the whole MFFC of a PPI [default = %s]\n", pPars->fMFFC? "yes": "no" ); diff --git a/src/base/wlc/wlcNtk.c b/src/base/wlc/wlcNtk.c index 02af1a16..89699949 100644 --- a/src/base/wlc/wlcNtk.c +++ b/src/base/wlc/wlcNtk.c @@ -120,6 +120,7 @@ void Wlc_ManSetDefaultParams( Wlc_Par_t * pPars ) pPars->fMFFC = 1; // Refine the entire MFFC of a PPI pPars->fPdra = 0; // Use pdr -nct pPars->fProofRefine = 0; // Use proof-based refinement + pPars->fHybrid = 1; // Use a hybrid of CBR and PBR pPars->fVerbose = 0; // verbose output` pPars->fPdrVerbose = 0; // show verbose PDR output } -- cgit v1.2.3 From 007195ddd85248e6e8f5762dc69b8810695e5ab1 Mon Sep 17 00:00:00 2001 From: Yen-Sheng Ho Date: Tue, 28 Feb 2017 19:25:11 -0800 Subject: small tweaks --- src/base/wlc/wlcCom.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/base') diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c index 0c9cdabb..38f919d4 100644 --- a/src/base/wlc/wlcCom.c +++ b/src/base/wlc/wlcCom.c @@ -573,7 +573,7 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv ) Wlc_NtkPdrAbs( pNtk, pPars ); return 0; usage: - Abc_Print( -2, "usage: %%pdra [-AMXFIL num] [-abcpmxvwh]\n" ); + Abc_Print( -2, "usage: %%pdra [-AMXFIL num] [-abrcpmxvwh]\n" ); Abc_Print( -2, "\t abstraction for word-level networks\n" ); Abc_Print( -2, "\t-A num : minimum bit-width of an adder/subtractor to abstract [default = %d]\n", pPars->nBitsAdd ); Abc_Print( -2, "\t-M num : minimum bit-width of a multiplier to abstract [default = %d]\n", pPars->nBitsMul ); -- cgit v1.2.3 From b71d2ab2ba4dd1da265845a94439c36a38e9d8d3 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 28 Feb 2017 20:15:33 -0800 Subject: Fixed a few compilcation issues with Windows compiler. --- src/base/wlc/wlcAbs.c | 23 ++++++++++++----------- 1 file changed, 12 insertions(+), 11 deletions(-) (limited to 'src/base') diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c index 1eb5a964..ad6c6642 100644 --- a/src/base/wlc/wlcAbs.c +++ b/src/base/wlc/wlcAbs.c @@ -67,10 +67,11 @@ static Vec_Int_t * Wlc_NtkGetCoreSels( Gia_Man_t * pFrames, int nFrames, int num Aig_Man_t * pAigFrames = Gia_ManToAigSimple( pFrames ); Cnf_Dat_t * pCnf = Cnf_Derive(pAigFrames, Aig_ManCoNum(pAigFrames)); sat_solver * pSat = sat_solver_new(); + int i; sat_solver_setnvars(pSat, pCnf->nVars); - for (int i = 0; i < pCnf->nClauses; i++) + for (i = 0; i < pCnf->nClauses; i++) { if (!sat_solver_addclause(pSat, pCnf->pClauses[i], pCnf->pClauses[i + 1])) assert(false); @@ -93,10 +94,11 @@ static Vec_Int_t * Wlc_NtkGetCoreSels( Gia_Man_t * pFrames, int nFrames, int num } // main procedure { + int status; Vec_Int_t* vLits = Vec_IntAlloc(100); Vec_Int_t* vMapVar2Sel = Vec_IntStart( pCnf->nVars ); int first_sel_pi = sel_pi_first ? 0 : num_other_pis; - for ( int i = 0; i < num_sel_pis; ++i ) + for ( i = 0; i < num_sel_pis; ++i ) { int cur_pi = first_sel_pi + i; int var = pCnf->pVarNums[Aig_ManCi(pAigFrames, cur_pi)->Id]; @@ -116,14 +118,13 @@ static Vec_Int_t * Wlc_NtkGetCoreSels( Gia_Man_t * pFrames, int nFrames, int num Abc_Print( 1, "%d ", Entry); Abc_Print( 1, "\n"); */ - int status = sat_solver_solve(pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), (ABC_INT64_T)(nConfLimit), (ABC_INT64_T)(0), (ABC_INT64_T)(0), (ABC_INT64_T)(0)); + status = sat_solver_solve(pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), (ABC_INT64_T)(nConfLimit), (ABC_INT64_T)(0), (ABC_INT64_T)(0), (ABC_INT64_T)(0)); if (status == l_False) { - Abc_Print( 1, "UNSAT.\n" ); int nCoreLits, *pCoreLits; + Abc_Print( 1, "UNSAT.\n" ); nCoreLits = sat_solver_final(pSat, &pCoreLits); - vCores = Vec_IntAlloc( nCoreLits ); - for (int i = 0; i < nCoreLits; i++) + for (i = 0; i < nCoreLits; i++) { Vec_IntPush( vCores, Vec_IntEntry( vMapVar2Sel, lit_var( pCoreLits[i] ) ) ); } @@ -148,13 +149,13 @@ static Gia_Man_t * Wlc_NtkUnrollWithCex(Wlc_Ntk_t * pChoice, Abc_Cex_t * pCex, i Gia_Man_t * pGiaChoice = Wlc_NtkBitBlast( pChoice, NULL, -1, 0, 0, 0, 0 ); int nbits_new_pis = Wlc_NtkNumPiBits( pChoice ); int num_ppis = nbits_new_pis - nbits_old_pis - num_sel_pis; - *p_num_ppis = num_ppis; int num_undc_pis = Gia_ManPiNum(pGiaChoice) - nbits_new_pis; Gia_Man_t * pFrames = NULL; Gia_Obj_t * pObj, * pObjRi; int f, i; int is_sel_pi; Gia_Man_t * pGia; + *p_num_ppis = num_ppis; Abc_Print( 1, "#orig_pis = %d, #ppis = %d, #sel_pis = %d, #undc_pis = %d\n", nbits_old_pis, num_ppis, num_sel_pis, num_undc_pis ); assert(Gia_ManPiNum(pGiaChoice)==nbits_old_pis+num_ppis+num_sel_pis+num_undc_pis); @@ -206,8 +207,7 @@ static Gia_Man_t * Wlc_NtkUnrollWithCex(Wlc_Ntk_t * pChoice, Abc_Cex_t * pCex, i Wlc_Ntk_t * Wlc_NtkIntroduceChoices( Wlc_Ntk_t * pNtk, Vec_Int_t * vBlacks ) { - if ( vBlacks== NULL ) return NULL; - + //if ( vBlacks== NULL ) return NULL; Vec_Int_t * vNodes = Vec_IntDup( vBlacks ); Wlc_Ntk_t * pNew; Wlc_Obj_t * pObj; @@ -383,6 +383,7 @@ static Wlc_Ntk_t * Wlc_NtkAbs2( Wlc_Ntk_t * pNtk, Vec_Int_t * vBlacks, Vec_Int_t static int Wlc_NtkProofRefine( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Abc_Cex_t * pCex, Vec_Int_t * vBlacks, Vec_Int_t ** pvRefine ) { + Gia_Man_t * pGiaFrames; Vec_Int_t * vRefine = NULL; Vec_Bit_t * vUnmark; Vec_Bit_t * vChoiceMark; @@ -406,8 +407,8 @@ static int Wlc_NtkProofRefine( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Abc_Cex_t * pCe Vec_BitWriteEntry( vChoiceMark, i, 1 ); } - pNtkWithChoices = Wlc_NtkIntroduceChoices( p, vBlacks ); - Gia_Man_t * pGiaFrames = Wlc_NtkUnrollWithCex( pNtkWithChoices, pCex, Wlc_NtkNumPiBits( p ), Vec_IntSize( vBlacks ), &num_ppis, 0 ); + pNtkWithChoices = vBlacks ? Wlc_NtkIntroduceChoices( p, vBlacks ) : NULL; + pGiaFrames = Wlc_NtkUnrollWithCex( pNtkWithChoices, pCex, Wlc_NtkNumPiBits( p ), Vec_IntSize( vBlacks ), &num_ppis, 0 ); vCoreSels = Wlc_NtkGetCoreSels( pGiaFrames, pCex->iFrame+1, Vec_IntSize( vBlacks ), num_ppis, vChoiceMark, 0, 0, pPars ); Wlc_NtkFree( pNtkWithChoices ); Gia_ManStop( pGiaFrames ); -- cgit v1.2.3 From d8505990202576e06db2c0c9a24a652fc66b2bd3 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 2 Mar 2017 14:26:04 -0800 Subject: Adding command 'glitch' for glitch simulation. --- src/base/abc/abc.h | 1 + src/base/abci/abc.c | 84 ++++++++++++++++++++++++++++++++++++++++++++++++ src/base/abci/abcPrint.c | 79 ++++++++++++++++++++++++++++++++++++++++++--- 3 files changed, 159 insertions(+), 5 deletions(-) (limited to 'src/base') diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index 6c0d96d1..fad0b804 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -825,6 +825,7 @@ extern ABC_DLL void Abc_NtkDontCareFree( Odc_Man_t * p ); extern ABC_DLL int Abc_NtkDontCareCompute( Odc_Man_t * p, Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, unsigned * puTruth ); /*=== abcPrint.c ==========================================================*/ extern ABC_DLL float Abc_NtkMfsTotalSwitching( Abc_Ntk_t * pNtk ); +extern ABC_DLL float Abc_NtkMfsTotalGlitching( Abc_Ntk_t * pNtk, int nPats, int Prob, int fVerbose ); extern ABC_DLL void Abc_NtkPrintStats( Abc_Ntk_t * pNtk, int fFactored, int fSaveBest, int fDumpResult, int fUseLutLib, int fPrintMuxes, int fPower, int fGlitch, int fSkipBuf, int fSkipSmall, int fPrintMem ); extern ABC_DLL void Abc_NtkPrintIo( FILE * pFile, Abc_Ntk_t * pNtk, int fPrintFlops ); extern ABC_DLL void Abc_NtkPrintLatch( FILE * pFile, Abc_Ntk_t * pNtk ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 2efa041c..8fa870a1 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -122,6 +122,7 @@ static int Abc_CommandMfs ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandMfs2 ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandMfs3 ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandTrace ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandGlitch ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandSpeedup ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandPowerdown ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAddBuffs ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -772,6 +773,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Synthesis", "mfs2", Abc_CommandMfs2, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "mfs3", Abc_CommandMfs3, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "trace", Abc_CommandTrace, 0 ); + Cmd_CommandAdd( pAbc, "Synthesis", "glitch", Abc_CommandGlitch, 0 ); Cmd_CommandAdd( pAbc, "Synthesis", "speedup", Abc_CommandSpeedup, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "powerdown", Abc_CommandPowerdown, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "addbuffs", Abc_CommandAddBuffs, 1 ); @@ -5707,6 +5709,88 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandGlitch( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc); + int nPats = 4000; + int Prob = 8; + int fVerbose = 1; + int c; + + // set defaults + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "NPvh" ) ) != EOF ) + { + switch ( c ) + { + case 'N': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" ); + goto usage; + } + nPats = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nPats < 1 ) + goto usage; + break; + case 'P': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-P\" should be followed by an integer.\n" ); + goto usage; + } + Prob = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( Prob < 1 ) + goto usage; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pNtk == NULL ) + { + Abc_Print( -1, "Empty network.\n" ); + return 1; + } + if ( !Abc_NtkIsLogic(pNtk) ) + { + Abc_Print( -1, "This command can only be applied to a mapped logic network.\n" ); + return 1; + } + if ( Abc_NtkIsMappedLogic(pNtk) || Abc_NtkGetFaninMax(pNtk) <= 6 ) + Abc_Print( 1, "Glitching adds %7.2f %% of signal transitions, compared to switching.\n", Abc_NtkMfsTotalGlitching(pNtk, nPats, Prob, fVerbose) ); + else + printf( "Currently computes glitching only for K-LUT networks with K <= 6.\n" ); + return 0; + +usage: + Abc_Print( -2, "usage: glitch [-NP ] [-vh]\n" ); + Abc_Print( -2, "\t comparing glitching activity to switching activity\n" ); + Abc_Print( -2, "\t-N : the number of random patterns to use (0 < num < 1000000) [default = %d]\n", nPats ); + Abc_Print( -2, "\t-P : once in how many cycles an input changes its value [default = %d]\n", Prob ); + Abc_Print( -2, "\t-v : toggle printing optimization summary [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + /**Function************************************************************* Synopsis [] diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c index 2129782f..ea91619c 100644 --- a/src/base/abci/abcPrint.c +++ b/src/base/abci/abcPrint.c @@ -351,9 +351,8 @@ void Abc_NtkPrintStats( Abc_Ntk_t * pNtk, int fFactored, int fSaveBest, int fDum Abc_Print( 1," power =%7.2f", Abc_NtkMfsTotalSwitching(pNtk) ); if ( fGlitch ) { - extern float Abc_NtkMfsTotalGlitching( Abc_Ntk_t * pNtk ); if ( Abc_NtkIsLogic(pNtk) && Abc_NtkGetFaninMax(pNtk) <= 6 ) - Abc_Print( 1," glitch =%7.2f %%", Abc_NtkMfsTotalGlitching(pNtk) ); + Abc_Print( 1," glitch =%7.2f %%", Abc_NtkMfsTotalGlitching(pNtk, 4000, 8, 0) ); else printf( "\nCurrently computes glitching only for K-LUT networks with K <= 6." ); } @@ -1744,7 +1743,7 @@ extern Gli_Man_t * Gli_ManAlloc( int nObjs, int nRegs, int nFanioPairs ); extern void Gli_ManStop( Gli_Man_t * p ); extern int Gli_ManCreateCi( Gli_Man_t * p, int nFanouts ); extern int Gli_ManCreateCo( Gli_Man_t * p, int iFanin ); -extern int Gli_ManCreateNode( Gli_Man_t * p, Vec_Int_t * vFanins, int nFanouts, unsigned * puTruth ); +extern int Gli_ManCreateNode( Gli_Man_t * p, Vec_Int_t * vFanins, int nFanouts, word * pGateTruth ); extern void Gli_ManSwitchesAndGlitches( Gli_Man_t * p, int nPatterns, float PiTransProb, int fVerbose ); extern int Gli_ObjNumSwitches( Gli_Man_t * p, int iNode ); @@ -1761,13 +1760,14 @@ extern int Gli_ObjNumGlitches( Gli_Man_t * p, int iNode ); SeeAlso [] ***********************************************************************/ -float Abc_NtkMfsTotalGlitching( Abc_Ntk_t * pNtk ) +float Abc_NtkMfsTotalGlitchingLut( Abc_Ntk_t * pNtk, int nPats, int Prob, int fVerbose ) { int nSwitches, nGlitches; Gli_Man_t * p; Vec_Ptr_t * vNodes; Vec_Int_t * vFanins, * vTruth; Abc_Obj_t * pObj, * pFanin; + Vec_Wrd_t * vTruths; word * pTruth; unsigned * puTruth; int i, k; assert( Abc_NtkIsLogic(pNtk) ); @@ -1781,6 +1781,7 @@ float Abc_NtkMfsTotalGlitching( Abc_Ntk_t * pNtk ) vNodes = Abc_NtkDfs( pNtk, 0 ); vFanins = Vec_IntAlloc( 6 ); vTruth = Vec_IntAlloc( 1 << 12 ); + vTruths = Vec_WrdStart( Abc_NtkObjNumMax(pNtk) ); // derive network for glitch computation p = Gli_ManAlloc( Vec_PtrSize(vNodes) + Abc_NtkCiNum(pNtk) + Abc_NtkCoNum(pNtk), @@ -1795,7 +1796,9 @@ float Abc_NtkMfsTotalGlitching( Abc_Ntk_t * pNtk ) Abc_ObjForEachFanin( pObj, pFanin, k ) Vec_IntPush( vFanins, pFanin->iTemp ); puTruth = Hop_ManConvertAigToTruth( (Hop_Man_t *)pNtk->pManFunc, (Hop_Obj_t *)pObj->pData, Abc_ObjFaninNum(pObj), vTruth, 0 ); - pObj->iTemp = Gli_ManCreateNode( p, vFanins, Abc_ObjFanoutNum(pObj), puTruth ); + pTruth = Vec_WrdEntryP( vTruths, Abc_ObjId(pObj) ); + *pTruth = ((word)puTruth[Abc_ObjFaninNum(pObj) == 6] << 32) | (word)puTruth[0]; + pObj->iTemp = Gli_ManCreateNode( p, vFanins, Abc_ObjFanoutNum(pObj), pTruth ); } Abc_NtkForEachCo( pNtk, pObj, i ) Gli_ManCreateCo( p, Abc_ObjFanin0(pObj)->iTemp ); @@ -1816,6 +1819,72 @@ float Abc_NtkMfsTotalGlitching( Abc_Ntk_t * pNtk ) Vec_PtrFree( vNodes ); Vec_IntFree( vTruth ); Vec_IntFree( vFanins ); + Vec_WrdFree( vTruths ); + return nSwitches ? 100.0*(nGlitches-nSwitches)/nSwitches : 0.0; +} + +/**Function************************************************************* + + Synopsis [Returns the percentable of increased power due to glitching.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +float Abc_NtkMfsTotalGlitching( Abc_Ntk_t * pNtk, int nPats, int Prob, int fVerbose ) +{ + int nSwitches, nGlitches; + Gli_Man_t * p; + Vec_Ptr_t * vNodes; + Vec_Int_t * vFanins; + Abc_Obj_t * pObj, * pFanin; + int i, k, nFaninMax = Abc_NtkGetFaninMax(pNtk); + if ( !Abc_NtkIsMappedLogic(pNtk) ) + return Abc_NtkMfsTotalGlitchingLut( pNtk, nPats, Prob, fVerbose ); + assert( Abc_NtkIsMappedLogic(pNtk) ); + if ( nFaninMax > 16 ) + { + printf( "Abc_NtkMfsTotalGlitching() This procedure works only for mapped networks with LUTs size up to 6 inputs.\n" ); + return -1.0; + } + vNodes = Abc_NtkDfs( pNtk, 0 ); + vFanins = Vec_IntAlloc( 6 ); + + // derive network for glitch computation + p = Gli_ManAlloc( Vec_PtrSize(vNodes) + Abc_NtkCiNum(pNtk) + Abc_NtkCoNum(pNtk), + Abc_NtkLatchNum(pNtk), Abc_NtkGetTotalFanins(pNtk) + Abc_NtkCoNum(pNtk) ); + Abc_NtkForEachObj( pNtk, pObj, i ) + pObj->iTemp = -1; + Abc_NtkForEachCi( pNtk, pObj, i ) + pObj->iTemp = Gli_ManCreateCi( p, Abc_ObjFanoutNum(pObj) ); + Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i ) + { + Vec_IntClear( vFanins ); + Abc_ObjForEachFanin( pObj, pFanin, k ) + Vec_IntPush( vFanins, pFanin->iTemp ); + pObj->iTemp = Gli_ManCreateNode( p, vFanins, Abc_ObjFanoutNum(pObj), Mio_GateReadTruthP((Mio_Gate_t *)pObj->pData) ); + } + Abc_NtkForEachCo( pNtk, pObj, i ) + Gli_ManCreateCo( p, Abc_ObjFanin0(pObj)->iTemp ); + + // compute glitching + Gli_ManSwitchesAndGlitches( p, nPats, 1.0/Prob, fVerbose ); + + // compute the ratio + nSwitches = nGlitches = 0; + Abc_NtkForEachObj( pNtk, pObj, i ) + if ( pObj->iTemp >= 0 ) + { + nSwitches += Abc_ObjFanoutNum(pObj) * Gli_ObjNumSwitches(p, pObj->iTemp); + nGlitches += Abc_ObjFanoutNum(pObj) * Gli_ObjNumGlitches(p, pObj->iTemp); + } + + Gli_ManStop( p ); + Vec_PtrFree( vNodes ); + Vec_IntFree( vFanins ); return nSwitches ? 100.0*(nGlitches-nSwitches)/nSwitches : 0.0; } -- cgit v1.2.3 From 96a399568d1c3e54e27d3a560cab3745f0d8ee06 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 2 Mar 2017 15:26:29 -0800 Subject: Adding experimental command. --- src/base/abci/abc.c | 46 +++++++++++++++++++++++++++++++++++++ src/base/abci/abcEco.c | 58 +++++++++++++++++++++++++++++++++++++++++++++++ src/base/abci/module.make | 1 + 3 files changed, 105 insertions(+) create mode 100644 src/base/abci/abcEco.c (limited to 'src/base') diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 8fa870a1..7fc45f48 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -317,6 +317,7 @@ static int Abc_CommandPSat ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandProve ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandIProve ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandDebug ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandEco ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandBmc ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandBmc2 ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandBmc3 ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -968,6 +969,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Verification", "prove", Abc_CommandProve, 1 ); Cmd_CommandAdd( pAbc, "Verification", "iprove", Abc_CommandIProve, 1 ); Cmd_CommandAdd( pAbc, "Verification", "debug", Abc_CommandDebug, 0 ); + Cmd_CommandAdd( pAbc, "Verification", "eco", Abc_CommandEco, 0 ); Cmd_CommandAdd( pAbc, "Verification", "bmc", Abc_CommandBmc, 0 ); Cmd_CommandAdd( pAbc, "Verification", "bmc2", Abc_CommandBmc2, 0 ); Cmd_CommandAdd( pAbc, "Verification", "bmc3", Abc_CommandBmc3, 1 ); @@ -23938,6 +23940,50 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandEco( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern void Abc_NtkEco( char * pFileNames[3] ); + char * pFileNames[3] = {NULL}; int c; + // set defaults + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) + { + switch ( c ) + { + case 'h': + goto usage; + default: + goto usage; + } + } + if ( globalUtilOptind + 3 != argc ) + { + Abc_Print( -1, "Expecting three file names on the command line.\n" ); + return 1; + } + for ( c = 0; c < 3; c++ ) + pFileNames[c] = argv[globalUtilOptind+c]; + Abc_NtkEco( pFileNames ); + return 0; + +usage: + Abc_Print( -2, "usage: eco [-h]\n" ); + Abc_Print( -2, "\t performs experimental ECO computation\n" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + /**Function************************************************************* Synopsis [] diff --git a/src/base/abci/abcEco.c b/src/base/abci/abcEco.c new file mode 100644 index 00000000..70a76729 --- /dev/null +++ b/src/base/abci/abcEco.c @@ -0,0 +1,58 @@ +/**CFile**************************************************************** + + FileName [abcEco.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network and node package.] + + Synopsis [Experimental procedures.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: abcEco.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "base/abc/abc.h" +#include "base/main/main.h" +#include "map/mio/mio.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkEco( char * pFileNames[3] ) +{ +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/base/abci/module.make b/src/base/abci/module.make index b97f526f..abf56716 100644 --- a/src/base/abci/module.make +++ b/src/base/abci/module.make @@ -17,6 +17,7 @@ SRC += src/base/abci/abc.c \ src/base/abci/abcDress2.c \ src/base/abci/abcDress3.c \ src/base/abci/abcDsd.c \ + src/base/abci/abcEco.c \ src/base/abci/abcExact.c \ src/base/abci/abcExtract.c \ src/base/abci/abcFraig.c \ -- cgit v1.2.3 From 64035e52ab2c245f3ef871983b1e9369b1fda2e4 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 2 Mar 2017 17:27:24 -0800 Subject: Macro to prevent writing history file. --- src/base/cmd/cmdHist.c | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) (limited to 'src/base') diff --git a/src/base/cmd/cmdHist.c b/src/base/cmd/cmdHist.c index d1ff0a9d..36e546a7 100644 --- a/src/base/cmd/cmdHist.c +++ b/src/base/cmd/cmdHist.c @@ -30,6 +30,8 @@ ABC_NAMESPACE_IMPL_START /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +#define ABC_USE_HISTORY 1 + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -99,7 +101,7 @@ void Cmd_HistoryAddCommand( Abc_Frame_t * p, const char * command ) ***********************************************************************/ void Cmd_HistoryRead( Abc_Frame_t * p ) { -#if defined(WIN32) +#if defined(WIN32) && defined(ABC_USE_HISTORY) char Buffer[ABC_MAX_STR]; FILE * pFile; assert( Vec_PtrSize(p->aHistory) == 0 ); @@ -130,7 +132,7 @@ void Cmd_HistoryRead( Abc_Frame_t * p ) ***********************************************************************/ void Cmd_HistoryWrite( Abc_Frame_t * p, int Limit ) { -#if defined(WIN32) +#if defined(WIN32) && defined(ABC_USE_HISTORY) FILE * pFile; char * pStr; int i; @@ -160,7 +162,7 @@ void Cmd_HistoryWrite( Abc_Frame_t * p, int Limit ) ***********************************************************************/ void Cmd_HistoryPrint( Abc_Frame_t * p, int Limit ) { -#if defined(WIN32) +#if defined(WIN32) && defined(ABC_USE_HISTORY) char * pStr; int i; Limit = Abc_MaxInt( 0, Vec_PtrSize(p->aHistory)-Limit ); -- cgit v1.2.3 From 2f69fa134e387698c05ea5c1c47f19684e99961f Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 2 Mar 2017 20:50:56 -0800 Subject: Moving global declarations into 'abcapi.h' and moving it into 'main' package. --- src/base/abci/abcMap.c | 16 +++---- src/base/main/abcapis.h | 102 ++++++++++++++++++++++++++++++++++++++++++++ src/base/main/abcapis_old.h | 84 ++++++++++++++++++++++++++++++++++++ src/base/main/main.h | 8 ++-- src/base/main/mainFrame.c | 2 +- src/base/wlc/wlcStdin.c | 2 +- 6 files changed, 199 insertions(+), 15 deletions(-) create mode 100644 src/base/main/abcapis.h create mode 100644 src/base/main/abcapis_old.h (limited to 'src/base') diff --git a/src/base/abci/abcMap.c b/src/base/abci/abcMap.c index 4e588e2d..f758d0f0 100644 --- a/src/base/abci/abcMap.c +++ b/src/base/abci/abcMap.c @@ -923,9 +923,9 @@ void Abc_NtkPrintMiniMapping( int * pArray ) SeeAlso [] ***********************************************************************/ -int * Abc_NtkOutputMiniMapping( void * pAbc0 ) +int * Abc_NtkOutputMiniMapping( Abc_Frame_t * pAbc ) { - Abc_Frame_t * pAbc = (Abc_Frame_t *)pAbc0; + //Abc_Frame_t * pAbc = (Abc_Frame_t *)pAbc0; Abc_Ntk_t * pNtk; Vec_Int_t * vMapping; int * pArray; @@ -977,9 +977,9 @@ void Abc_NtkTestMiniMapping( Abc_Ntk_t * p ) SeeAlso [] ***********************************************************************/ -void Abc_NtkSetCiArrivalTime( void * pAbc0, int iCi, float Rise, float Fall ) +void Abc_NtkSetCiArrivalTime( Abc_Frame_t * pAbc, int iCi, float Rise, float Fall ) { - Abc_Frame_t * pAbc = (Abc_Frame_t *)pAbc0; + //Abc_Frame_t * pAbc = (Abc_Frame_t *)pAbc0; Abc_Ntk_t * pNtk; Abc_Obj_t * pNode; if ( pAbc == NULL ) @@ -1001,9 +1001,9 @@ void Abc_NtkSetCiArrivalTime( void * pAbc0, int iCi, float Rise, float Fall ) pNode = Abc_NtkCi( pNtk, iCi ); Abc_NtkTimeSetArrival( pNtk, Abc_ObjId(pNode), Rise, Fall ); } -void Abc_NtkSetCoRequiredTime( void * pAbc0, int iCo, float Rise, float Fall ) +void Abc_NtkSetCoRequiredTime( Abc_Frame_t * pAbc, int iCo, float Rise, float Fall ) { - Abc_Frame_t * pAbc = (Abc_Frame_t *)pAbc0; + //Abc_Frame_t * pAbc = (Abc_Frame_t *)pAbc0; Abc_Ntk_t * pNtk; Abc_Obj_t * pNode; if ( pAbc == NULL )\ @@ -1037,9 +1037,9 @@ void Abc_NtkSetCoRequiredTime( void * pAbc0, int iCo, float Rise, float Fall ) SeeAlso [] ***********************************************************************/ -void Abc_NtkSetAndGateDelay( void * pAbc0, float Delay ) +void Abc_NtkSetAndGateDelay( Abc_Frame_t * pAbc, float Delay ) { - Abc_Frame_t * pAbc = (Abc_Frame_t *)pAbc0; + //Abc_Frame_t * pAbc = (Abc_Frame_t *)pAbc0; Abc_Ntk_t * pNtk; if ( pAbc == NULL ) { diff --git a/src/base/main/abcapis.h b/src/base/main/abcapis.h new file mode 100644 index 00000000..3445a00f --- /dev/null +++ b/src/base/main/abcapis.h @@ -0,0 +1,102 @@ +/**CFile**************************************************************** + + FileName [abcapis.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Include this file in the external code calling ABC.] + + Synopsis [External declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - September 29, 2012.] + + Revision [$Id: abcapis.h,v 1.00 2012/09/29 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef MINI_AIG__abc_apis_h +#define MINI_AIG__abc_apis_h + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Abc_Frame_t_ Abc_Frame_t; + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +#ifdef WIN32 + #ifdef WIN32_NO_DLL + #define ABC_DLLEXPORT + #define ABC_DLLIMPORT + #else + #define ABC_DLLEXPORT __declspec(dllexport) + #define ABC_DLLIMPORT __declspec(dllimport) + #endif +#else /* defined(WIN32) */ +#define ABC_DLLIMPORT +#endif /* defined(WIN32) */ + +#ifndef ABC_DLL +#define ABC_DLL ABC_DLLIMPORT +#endif + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +// procedures to start and stop the ABC framework +extern ABC_DLL void Abc_Start(); +extern ABC_DLL void Abc_Stop(); + +// procedures to get the ABC framework (pAbc) and execute commands in it +extern ABC_DLL Abc_Frame_t * Abc_FrameGetGlobalFrame(); +extern ABC_DLL int Cmd_CommandExecute( Abc_Frame_t * pAbc, const char * pCommandLine ); + +// procedures to input/output 'mini AIG' +extern ABC_DLL void Abc_NtkInputMiniAig( Abc_Frame_t * pAbc, void * pMiniAig ); +extern ABC_DLL void * Abc_NtkOutputMiniAig( Abc_Frame_t * pAbc ); +extern ABC_DLL void Abc_FrameGiaInputMiniAig( Abc_Frame_t * pAbc, void * p ); +extern ABC_DLL void * Abc_FrameGiaOutputMiniAig( Abc_Frame_t * pAbc ); +extern ABC_DLL void Abc_NtkSetFlopNum( Abc_Frame_t * pAbc, int nFlops ); + +// procedures to input/output 'mini LUT' +extern ABC_DLL void Abc_FrameGiaInputMiniLut( Abc_Frame_t * pAbc, void * pMiniLut ); +extern ABC_DLL void * Abc_FrameGiaOutputMiniLut( Abc_Frame_t * pAbc ); + +// procedures to set CI/CO arrival/required times +extern ABC_DLL void Abc_NtkSetCiArrivalTime( Abc_Frame_t * pAbc, int iCi, float Rise, float Fall ); +extern ABC_DLL void Abc_NtkSetCoRequiredTime( Abc_Frame_t * pAbc, int iCo, float Rise, float Fall ); + +// procedure to set AND-gate delay to tech-independent synthesis and mapping +extern ABC_DLL void Abc_NtkSetAndGateDelay( Abc_Frame_t * pAbc, float Delay ); + +// procedures to return the mapped network +extern ABC_DLL int * Abc_NtkOutputMiniMapping( Abc_Frame_t * pAbc ); +extern ABC_DLL void Abc_NtkPrintMiniMapping( int * pArray ); + +// procedures to access verifization status and a counter-example +extern ABC_DLL int Abc_FrameReadProbStatus( Abc_Frame_t * pAbc ); +extern ABC_DLL void * Abc_FrameReadCex( Abc_Frame_t * pAbc ); + + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/base/main/abcapis_old.h b/src/base/main/abcapis_old.h new file mode 100644 index 00000000..b2703bea --- /dev/null +++ b/src/base/main/abcapis_old.h @@ -0,0 +1,84 @@ +/**CFile**************************************************************** + + FileName [abcapis.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Include this file in the external code calling ABC.] + + Synopsis [External declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - September 29, 2012.] + + Revision [$Id: abcapis.h,v 1.00 2012/09/29 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef MINI_AIG__abc_apis_old_h +#define MINI_AIG__abc_apis_old_h + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +// procedures to start and stop the ABC framework +extern void Abc_Start(); +extern void Abc_Stop(); + +// procedures to get the ABC framework (pAbc) and execute commands in it +extern void * Abc_FrameGetGlobalFrame(); +extern int Cmd_CommandExecute( void * pAbc, char * pCommandLine ); + +// procedures to input/output 'mini AIG' +extern void Abc_NtkInputMiniAig( void * pAbc, void * pMiniAig ); +extern void * Abc_NtkOutputMiniAig( void * pAbc ); +extern void Abc_FrameGiaInputMiniAig( void * pAbc, void * p ); +extern void * Abc_FrameGiaOutputMiniAig( void * pAbc ); +extern void Abc_NtkSetFlopNum( void * pAbc, int nFlops ); + +// procedures to input/output 'mini LUT' +extern void Abc_FrameGiaInputMiniLut( void * pAbc, void * pMiniLut ); +extern void * Abc_FrameGiaOutputMiniLut( void * pAbc ); + +// procedures to set CI/CO arrival/required times +extern void Abc_NtkSetCiArrivalTime( void * pAbc, int iCi, float Rise, float Fall ); +extern void Abc_NtkSetCoRequiredTime( void * pAbc, int iCo, float Rise, float Fall ); + +// procedure to set AND-gate delay to tech-independent synthesis and mapping +extern void Abc_NtkSetAndGateDelay( void * pAbc, float Delay ); + +// procedures to return the mapped network +extern int * Abc_NtkOutputMiniMapping( void * pAbc ); +extern void Abc_NtkPrintMiniMapping( int * pArray ); + +// procedures to access verifization status and a counter-example +extern int Abc_FrameReadProbStatus( void * pAbc ); +extern void * Abc_FrameReadCex( void * pAbc ); + + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/base/main/main.h b/src/base/main/main.h index 89353fa6..a59a9a40 100644 --- a/src/base/main/main.h +++ b/src/base/main/main.h @@ -34,10 +34,8 @@ #include "misc/vec/vec.h" #include "misc/st/st.h" -ABC_NAMESPACE_HEADER_START -// the framework containing all data -typedef struct Abc_Frame_t_ Abc_Frame_t; -ABC_NAMESPACE_HEADER_END +// the framework containing all data is defined here +#include "abcapis.h" #include "base/cmd/cmd.h" #include "base/io/ioAbc.h" @@ -116,7 +114,7 @@ extern ABC_DLL void Abc_FrameSetBridgeMode(); extern ABC_DLL int Abc_FrameReadBmcFrames( Abc_Frame_t * p ); extern ABC_DLL int Abc_FrameReadProbStatus( Abc_Frame_t * p ); -extern ABC_DLL Abc_Cex_t * Abc_FrameReadCex( Abc_Frame_t * p ); +extern ABC_DLL void * Abc_FrameReadCex( Abc_Frame_t * p ); extern ABC_DLL Vec_Ptr_t * Abc_FrameReadCexVec( Abc_Frame_t * p ); extern ABC_DLL Vec_Int_t * Abc_FrameReadStatusVec( Abc_Frame_t * p ); extern ABC_DLL Vec_Ptr_t * Abc_FrameReadPoEquivs( Abc_Frame_t * p ); diff --git a/src/base/main/mainFrame.c b/src/base/main/mainFrame.c index 9647d020..cd4ff2c7 100644 --- a/src/base/main/mainFrame.c +++ b/src/base/main/mainFrame.c @@ -69,7 +69,7 @@ char * Abc_FrameReadFlag( char * pFlag ) { return Cmd_FlagRe int Abc_FrameReadBmcFrames( Abc_Frame_t * p ) { return s_GlobalFrame->nFrames; } int Abc_FrameReadProbStatus( Abc_Frame_t * p ) { return s_GlobalFrame->Status; } -Abc_Cex_t * Abc_FrameReadCex( Abc_Frame_t * p ) { return s_GlobalFrame->pCex; } +void * Abc_FrameReadCex( Abc_Frame_t * p ) { return s_GlobalFrame->pCex; } Vec_Ptr_t * Abc_FrameReadCexVec( Abc_Frame_t * p ) { return s_GlobalFrame->vCexVec; } Vec_Int_t * Abc_FrameReadStatusVec( Abc_Frame_t * p ) { return s_GlobalFrame->vStatuses; } Vec_Ptr_t * Abc_FrameReadPoEquivs( Abc_Frame_t * p ) { return s_GlobalFrame->vPoEquivs; } diff --git a/src/base/wlc/wlcStdin.c b/src/base/wlc/wlcStdin.c index 49c25ad0..3b747cc5 100644 --- a/src/base/wlc/wlcStdin.c +++ b/src/base/wlc/wlcStdin.c @@ -239,7 +239,7 @@ int Wlc_StdinProcessSmt( Abc_Frame_t * pAbc, char * pCmd ) return 0; } // report value of this variable - Wlc_NtkReport( (Wlc_Ntk_t *)pAbc->pAbcWlc, Abc_FrameReadCex(pAbc), pName, 16 ); + Wlc_NtkReport( (Wlc_Ntk_t *)pAbc->pAbcWlc, (Abc_Cex_t *)Abc_FrameReadCex(pAbc), pName, 16 ); Vec_StrFree( vInput ); fflush( stdout ); } -- cgit v1.2.3