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(-) 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(-) 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 + src/proof/pdr/pdrIncr.c | 26 ++++++++++++++++++++++++++ 5 files changed, 42 insertions(+), 2 deletions(-) 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 } diff --git a/src/proof/pdr/pdrIncr.c b/src/proof/pdr/pdrIncr.c index 3fcd3d31..7bca217f 100644 --- a/src/proof/pdr/pdrIncr.c +++ b/src/proof/pdr/pdrIncr.c @@ -190,6 +190,21 @@ sat_solver * IPdr_ManSetSolver( Pdr_Man_t * p, int k, int nTotal ) SeeAlso [] ***********************************************************************/ + +int IPdr_ManRestoreAbsFlops( Pdr_Man_t * p ) +{ + Pdr_Set_t * pSet; int i, j, k; + + Vec_VecForEachEntry( Pdr_Set_t *, p->vClauses, pSet, i, j ) + { + for ( k = 0; k < pSet->nLits; k++ ) + { + Vec_IntWriteEntry( p->vAbsFlops, Abc_Lit2Var(pSet->Lits[k]), 1 ); + } + } + return 0; +} + int IPdr_ManRestore( Pdr_Man_t * p, Vec_Vec_t * vClauses, Vec_Int_t * vMap ) { int i; @@ -288,6 +303,17 @@ int IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPushClauses ) return 1; } } + + if ( p->pPars->fUseAbs && p->vAbsFlops == NULL && iFrame >= 1 ) + { + assert( p->vAbsFlops == NULL ); + p->vAbsFlops = Vec_IntStart( Saig_ManRegNum(p->pAig) ); + p->vMapFf2Ppi = Vec_IntStartFull( Saig_ManRegNum(p->pAig) ); + p->vMapPpi2Ff = Vec_IntAlloc( 100 ); + + IPdr_ManRestoreAbsFlops( p ); + } + } while ( 1 ) { -- cgit v1.2.3 From ca0bdde9b35a004303a843953e37c3bbe3bcc3f1 Mon Sep 17 00:00:00 2001 From: Yen-Sheng Ho Date: Thu, 23 Feb 2017 10:54:53 -0800 Subject: changed how pdr -t cleans up abs flops --- src/proof/pdr/pdrIncr.c | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/src/proof/pdr/pdrIncr.c b/src/proof/pdr/pdrIncr.c index 7bca217f..8ca8e29e 100644 --- a/src/proof/pdr/pdrIncr.c +++ b/src/proof/pdr/pdrIncr.c @@ -468,6 +468,9 @@ int IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPushClauses ) break; // keep solving } p->pAig->pSeqModel = pCex; + + if ( p->pPars->fVerbose && p->pPars->fUseAbs ) + Pdr_ManPrintProgress( p, !p->pPars->fSolveAll, Abc_Clock() - clkStart ); return 0; // SAT } p->pPars->nFailOuts++; @@ -517,6 +520,7 @@ int IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPushClauses ) p->timeToStopOne = 0; } } + /* if ( p->pPars->fUseAbs && p->vAbsFlops && !fRefined ) { int i, Used; @@ -524,6 +528,17 @@ int IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPushClauses ) if ( Used && (Vec_IntEntry(p->vPrio, i) >> p->nPrioShift) == 0 ) Vec_IntWriteEntry( p->vAbsFlops, i, 0 ); } + */ + if ( p->pPars->fUseAbs && p->vAbsFlops && !fRefined ) + { + Pdr_Set_t * pSet; + int i, j, k; + Vec_IntFill( p->vAbsFlops, Vec_IntSize( p->vAbsFlops ), 0 ); + Vec_VecForEachEntry( Pdr_Set_t *, p->vClauses, pSet, i, j ) + for ( k = 0; k < pSet->nLits; k++ ) + Vec_IntWriteEntry( p->vAbsFlops, Abc_Lit2Var(pSet->Lits[k]), 1 ); + } + if ( p->pPars->fVerbose ) Pdr_ManPrintProgress( p, !fRefined, Abc_Clock() - clkStart ); if ( fRefined ) -- 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(-) 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(+) 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 80773b95221237134719e08948ed1b74ac049536 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 25 Feb 2017 09:49:31 -0800 Subject: Adding dump of trivial abstraction map at the beginning in &gla -m. --- src/opt/sbd/sbd.c | 63 ++++++++++++++++++++++++++++++++++++++++++++++++++ src/proof/abs/absGla.c | 20 +++++++++++++++- 2 files changed, 82 insertions(+), 1 deletion(-) diff --git a/src/opt/sbd/sbd.c b/src/opt/sbd/sbd.c index 4d86d2ee..5c5b1f2b 100644 --- a/src/opt/sbd/sbd.c +++ b/src/opt/sbd/sbd.c @@ -19,6 +19,7 @@ ***********************************************************************/ #include "sbdInt.h" +#include "misc/vec/vecHsh.h" ABC_NAMESPACE_IMPL_START @@ -42,6 +43,68 @@ ABC_NAMESPACE_IMPL_START SeeAlso [] ***********************************************************************/ +int Sbd_CountConfigVars( Vec_Int_t * vSet, int nVars ) +{ + int i, k, Entry = 0, Entry2, Count = 0, Below; + int Prev = Vec_IntEntry( vSet, 0 ); + Vec_IntForEachEntryStart( vSet, Entry, i, 1 ) + { + assert( 2*Prev >= Entry ); + if ( 2*Prev == Entry ) + { + Prev = Entry; + continue; + } + Below = nVars; + Vec_IntForEachEntryStart( vSet, Entry2, k, i ) + Below += Entry2; + Count += Below * (2*Prev - 1); + Prev = Entry; + } + Count += nVars * 2*Prev; + return Vec_IntSum(vSet) < nVars - 1 ? 0 : Count; +} +void Sbd_CountTopos() +{ + Hsh_VecMan_t * p = Hsh_VecManStart( 100000 ); // hash table for arrays + Vec_Int_t * vSet = Vec_IntAlloc( 100 ); + int i, k, e, Start, Stop; + Start = Hsh_VecManAdd( p, vSet ); + for ( i = 1; i < 9; i++ ) + { + Stop = Hsh_VecSize( p ); + for ( e = Start; e < Stop; e++ ) + { + Vec_Int_t * vTemp = Hsh_VecReadEntry( p, e ); + Vec_IntClear( vSet ); + Vec_IntAppend( vSet, vTemp ); + for ( k = 0; k < Vec_IntSize(vSet); k++ ) + { + // skip if the number of entries on this level is equal to the number of fanins on the previous level + if ( k ? (Vec_IntEntry(vSet, k) == 2*Vec_IntEntry(vSet, k-1)) : (Vec_IntEntry(vSet, 0) > 0) ) + continue; + Vec_IntAddToEntry( vSet, k, 1 ); + Hsh_VecManAdd( p, vSet ); + Vec_IntAddToEntry( vSet, k, -1 ); + } + Vec_IntPush( vSet, 1 ); + Hsh_VecManAdd( p, vSet ); + } + printf( "%2d : This = %8d All = %8d\n", i, Hsh_VecSize(p) - Stop, Hsh_VecSize(p) ); + if ( 0 ) + { + for ( e = Stop; e < Hsh_VecSize(p); e++ ) + { + Vec_Int_t * vTemp = Hsh_VecReadEntry( p, e ); + printf( "Params = %3d. ", Sbd_CountConfigVars(vTemp, 5) ); + Vec_IntPrint( vTemp ); + } + } + Start = Stop; + } + Vec_IntFree( vSet ); + Hsh_VecManStop( p ); +} //////////////////////////////////////////////////////////////////////// diff --git a/src/proof/abs/absGla.c b/src/proof/abs/absGla.c index 97a8b644..420adfc3 100644 --- a/src/proof/abs/absGla.c +++ b/src/proof/abs/absGla.c @@ -1539,9 +1539,27 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars ) Abc_Print( 1, "LrnStart = %d LrnDelta = %d LrnRatio = %d %% Skip = %d SimpleCNF = %d Dump = %d\n", pPars->nLearnedStart, pPars->nLearnedDelta, pPars->nLearnedPerce, pPars->fUseSkip, pPars->fUseSimple, pPars->fDumpVabs|pPars->fDumpMabs ); if ( pPars->fDumpVabs || pPars->fDumpMabs ) - Abc_Print( 1, "%s will be dumped into file \"%s\".\n", + Abc_Print( 1, "%s will be continously dumped into file \"%s\".\n", pPars->fDumpVabs ? "Abstracted model" : "Miter with abstraction map", Ga2_GlaGetFileName(p, pPars->fDumpVabs) ); + if ( pPars->fDumpMabs ) + { + // create trivial abstraction map + Gia_Obj_t * pObj; + char * pFileName = Ga2_GlaGetFileName(p, 0); + Vec_Int_t * vMap = pAig->vGateClasses; pAig->vGateClasses = NULL; + pAig->vGateClasses = Vec_IntStart( Gia_ManObjNum(pAig) ); + Vec_IntWriteEntry( pAig->vGateClasses, 0, 1 ); + Gia_ManForEachAnd( pAig, pObj, i ) + Vec_IntWriteEntry( pAig->vGateClasses, i, 1 ); + Gia_ManForEachRo( pAig, pObj, i ) + Vec_IntWriteEntry( pAig->vGateClasses, Gia_ObjId(pAig, pObj), 1 ); + Gia_AigerWrite( pAig, pFileName, 0, 0 ); + Vec_IntFree( pAig->vGateClasses ); + pAig->vGateClasses = vMap; + if ( p->pPars->fVerbose ) + Abc_Print( 1, "Dumping miter with abstraction map into file \"%s\"...\n", pFileName ); + } Abc_Print( 1, " Frame %% Abs PPI FF LUT Confl Cex Vars Clas Lrns Time Mem\n" ); } // iterate unrolling -- cgit v1.2.3 From 7d5b1c572bfb5385dc79f795d4c9d3294adbdae6 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 25 Feb 2017 13:34:54 -0800 Subject: Restoring constraint manager to read old constraint file by default (use 'read_constr -n' to read new format). --- src/map/scl/scl.c | 34 +++++++++++++++++++++------------- src/map/scl/sclUtil.c | 10 +++++----- 2 files changed, 26 insertions(+), 18 deletions(-) diff --git a/src/map/scl/scl.c b/src/map/scl/scl.c index 9d4653a7..27342458 100644 --- a/src/map/scl/scl.c +++ b/src/map/scl/scl.c @@ -1823,13 +1823,17 @@ int Scl_CommandReadConstr( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc); FILE * pFile; char * pFileName; + int fUseNewFormat = 0; int c, fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "nvh" ) ) != EOF ) { switch ( c ) { + case 'n': + fVerbose ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -1850,25 +1854,29 @@ int Scl_CommandReadConstr( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } fclose( pFile ); -// Abc_SclReadTimingConstr( pAbc, pFileName, fVerbose ); - if ( pNtk == NULL ) - { - fprintf( pAbc->Err, "There is no current network.\n" ); - return 1; - } - - // input constraint manager - if ( pNtk ) + if ( !fUseNewFormat ) + Abc_SclReadTimingConstr( pAbc, pFileName, fVerbose ); + else { - Scl_Con_t * pCon = Scl_ConRead( pFileName, Abc_NtkNameMan(pNtk, 0), Abc_NtkNameMan(pNtk, 1) ); - if ( pCon ) Scl_ConUpdateMan( pAbc, pCon ); + if ( pNtk == NULL ) + { + fprintf( pAbc->Err, "There is no current network.\n" ); + return 1; + } + // input constraint manager + if ( pNtk ) + { + Scl_Con_t * pCon = Scl_ConRead( pFileName, Abc_NtkNameMan(pNtk, 0), Abc_NtkNameMan(pNtk, 1) ); + if ( pCon ) Scl_ConUpdateMan( pAbc, pCon ); + } } return 0; usage: - fprintf( pAbc->Err, "usage: read_constr [-vh] \n" ); + fprintf( pAbc->Err, "usage: read_constr [-nvh] \n" ); fprintf( pAbc->Err, "\t read file with timing constraints for standard-cell designs\n" ); + fprintf( pAbc->Err, "\t-n : toggle using new constraint file format [default = %s]\n", fUseNewFormat? "yes": "no" ); fprintf( pAbc->Err, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pAbc->Err, "\t-h : prints the command summary\n" ); fprintf( pAbc->Err, "\t : the name of a file to read\n" ); diff --git a/src/map/scl/sclUtil.c b/src/map/scl/sclUtil.c index 70140044..07e0deb6 100644 --- a/src/map/scl/sclUtil.c +++ b/src/map/scl/sclUtil.c @@ -254,21 +254,21 @@ void Abc_SclReadTimingConstr( Abc_Frame_t * pAbc, char * pFileName, int fVerbose pToken = strtok( Buffer, " \t\r\n" ); if ( pToken == NULL ) continue; -// if ( !strcmp(pToken, "set_driving_cell") ) - if ( !strcmp(pToken, "default_input_cell") ) + if ( !strcmp(pToken, "set_driving_cell") ) +// if ( !strcmp(pToken, "default_input_cell") ) { Abc_FrameSetDrivingCell( Abc_UtilStrsav(strtok(NULL, " \t\r\n")) ); if ( fVerbose ) printf( "Setting driving cell to be \"%s\".\n", Abc_FrameReadDrivingCell() ); } -// else if ( !strcmp(pToken, "set_load") ) - else if ( !strcmp(pToken, "default_output_load") ) + else if ( !strcmp(pToken, "set_load") ) +// else if ( !strcmp(pToken, "default_output_load") ) { Abc_FrameSetMaxLoad( atof(strtok(NULL, " \t\r\n")) ); if ( fVerbose ) printf( "Setting driving cell to be %f.\n", Abc_FrameReadMaxLoad() ); } -// else printf( "Unrecognized token \"%s\".\n", pToken ); + else printf( "Unrecognized token \"%s\".\n", pToken ); } fclose( pFile ); } -- 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(+) 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(+) 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 4ec5ee410d4523ca1396ff4c7247e3a7ceaf027a Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 25 Feb 2017 16:22:31 -0800 Subject: Adding dump of trivial abstraction map at the beginning in &gla -m. --- src/proof/abs/absGla.c | 40 +++++++++++++++++++++++++--------------- 1 file changed, 25 insertions(+), 15 deletions(-) diff --git a/src/proof/abs/absGla.c b/src/proof/abs/absGla.c index 420adfc3..5f8503a5 100644 --- a/src/proof/abs/absGla.c +++ b/src/proof/abs/absGla.c @@ -1544,21 +1544,31 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars ) Ga2_GlaGetFileName(p, pPars->fDumpVabs) ); if ( pPars->fDumpMabs ) { - // create trivial abstraction map - Gia_Obj_t * pObj; - char * pFileName = Ga2_GlaGetFileName(p, 0); - Vec_Int_t * vMap = pAig->vGateClasses; pAig->vGateClasses = NULL; - pAig->vGateClasses = Vec_IntStart( Gia_ManObjNum(pAig) ); - Vec_IntWriteEntry( pAig->vGateClasses, 0, 1 ); - Gia_ManForEachAnd( pAig, pObj, i ) - Vec_IntWriteEntry( pAig->vGateClasses, i, 1 ); - Gia_ManForEachRo( pAig, pObj, i ) - Vec_IntWriteEntry( pAig->vGateClasses, Gia_ObjId(pAig, pObj), 1 ); - Gia_AigerWrite( pAig, pFileName, 0, 0 ); - Vec_IntFree( pAig->vGateClasses ); - pAig->vGateClasses = vMap; - if ( p->pPars->fVerbose ) - Abc_Print( 1, "Dumping miter with abstraction map into file \"%s\"...\n", pFileName ); + { + char Command[1000]; + Abc_FrameSetStatus( -1 ); + Abc_FrameSetCex( NULL ); + Abc_FrameSetNFrames( -1 ); + sprintf( Command, "write_status %s", Extra_FileNameGenericAppend((char *)(p->pPars->pFileVabs ? p->pPars->pFileVabs : "glabs.aig"), ".status")); + Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), Command ); + } + { + // create trivial abstraction map + Gia_Obj_t * pObj; + char * pFileName = Ga2_GlaGetFileName(p, 0); + Vec_Int_t * vMap = pAig->vGateClasses; pAig->vGateClasses = NULL; + pAig->vGateClasses = Vec_IntStart( Gia_ManObjNum(pAig) ); + Vec_IntWriteEntry( pAig->vGateClasses, 0, 1 ); + Gia_ManForEachAnd( pAig, pObj, i ) + Vec_IntWriteEntry( pAig->vGateClasses, i, 1 ); + Gia_ManForEachRo( pAig, pObj, i ) + Vec_IntWriteEntry( pAig->vGateClasses, Gia_ObjId(pAig, pObj), 1 ); + Gia_AigerWrite( pAig, pFileName, 0, 0 ); + Vec_IntFree( pAig->vGateClasses ); + pAig->vGateClasses = vMap; + if ( p->pPars->fVerbose ) + Abc_Print( 1, "Dumping miter with abstraction map into file \"%s\"...\n", pFileName ); + } } Abc_Print( 1, " Frame %% Abs PPI FF LUT Confl Cex Vars Clas Lrns Time Mem\n" ); } -- 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(-) 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(-) 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(-) 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(-) 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(-) 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(-) 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(-) 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(-) 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(+) 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(-) 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(-) 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 9957736777844cdb531fe0a2477bcf4e330cc10d Mon Sep 17 00:00:00 2001 From: Bruno Schmitt Date: Tue, 28 Feb 2017 18:58:14 -0300 Subject: Adding an procedure to write DIMACS. Fixing small bugs. --- src/sat/satoko/clause.h | 14 +++++++++++++ src/sat/satoko/cnf_reader.c | 2 +- src/sat/satoko/satoko.h | 11 +++++++++++ src/sat/satoko/solver.c | 2 +- src/sat/satoko/solver_api.c | 48 ++++++++++++++++++++++++++++++++++++++++++++- 5 files changed, 74 insertions(+), 3 deletions(-) diff --git a/src/sat/satoko/clause.h b/src/sat/satoko/clause.h index 2be18cd6..9b05868b 100644 --- a/src/sat/satoko/clause.h +++ b/src/sat/satoko/clause.h @@ -59,5 +59,19 @@ static inline void clause_print(struct clause *clause) printf("}\n"); } +static inline void clause_dump(FILE *file, struct clause *clause, int no_zero_var) +{ + unsigned i; + for (i = 0; i < clause->size; i++) { + int var = (clause->data[i].lit >> 1); + char pol = (clause->data[i].lit & 1); + fprintf(file, "%d ", pol ? -(var + no_zero_var) : (var + no_zero_var)); + } + if (no_zero_var) + fprintf(file, "0\n"); + else + fprintf(file, "\n"); +} + ABC_NAMESPACE_HEADER_END #endif /* satoko__clause_h */ diff --git a/src/sat/satoko/cnf_reader.c b/src/sat/satoko/cnf_reader.c index adb9a47b..8223affd 100644 --- a/src/sat/satoko/cnf_reader.c +++ b/src/sat/satoko/cnf_reader.c @@ -150,7 +150,7 @@ int satoko_parse_dimacs(char *fname, satoko_t **solver) vec_uint_free(lits); satoko_free(buffer); *solver = p; - return satoko_simplify(p); + return SATOKO_OK; } ABC_NAMESPACE_IMPL_END diff --git a/src/sat/satoko/satoko.h b/src/sat/satoko/satoko.h index a0c4d216..6634e68e 100644 --- a/src/sat/satoko/satoko.h +++ b/src/sat/satoko/satoko.h @@ -60,6 +60,7 @@ struct satoko_opts { unsigned clause_min_lbd_bin_resol; float garbage_max_ratio; char verbose; + char no_simplify; }; typedef struct satoko_stats satoko_stats_t; @@ -108,6 +109,16 @@ extern void satoko_unbookmark(satoko_t *); */ extern int satoko_final_conflict(satoko_t *, unsigned *); +/* Procedure to dump a DIMACS file. + * - It receives as input the solver, a file name string and two integers. + * - If the file name string is NULL the solver will dump in stdout. + * - The first argument can be either 0 or 1 and is an option to dump learnt + * clauses. (value 1 will dump them). + * - The seccond argument can be either 0 or 1 and is an option to use 0 as a + * variable ID or not. Keep in mind that if 0 is used as an ID the generated + * file will not be a DIMACS. (value 1 will use 0 as ID). + */ +extern void satoko_write_dimacs(satoko_t *, char *, int, int); extern satoko_stats_t satoko_stats(satoko_t *); ABC_NAMESPACE_HEADER_END diff --git a/src/sat/satoko/solver.c b/src/sat/satoko/solver.c index af3dcffb..42bc6448 100644 --- a/src/sat/satoko/solver.c +++ b/src/sat/satoko/solver.c @@ -644,7 +644,7 @@ char solver_search(solver_t *s) solver_cancel_until(s, 0); return SATOKO_UNDEC; } - if (solver_dlevel(s) == 0) + if (!s->opts.no_simplify && solver_dlevel(s) == 0) satoko_simplify(s); /* Reduce the set of learnt clauses */ diff --git a/src/sat/satoko/solver_api.c b/src/sat/satoko/solver_api.c index 3cb9f3d3..dada33cc 100644 --- a/src/sat/satoko/solver_api.c +++ b/src/sat/satoko/solver_api.c @@ -152,6 +152,7 @@ void satoko_default_opts(satoko_opts_t *opts) { memset(opts, 0, sizeof(satoko_opts_t)); opts->verbose = 0; + opts->no_simplify = 0; /* Limits */ opts->conf_limit = 0; opts->prop_limit = 0; @@ -290,6 +291,10 @@ int satoko_solve(solver_t *s) //if (s->opts.verbose) // print_opts(s); + if (!s->opts.no_simplify) + if (satoko_simplify(s) != SATOKO_OK) + return SATOKO_UNDEC; + while (status == SATOKO_UNDEC) { status = solver_search(s); if (solver_check_limits(s) == 0) @@ -297,6 +302,7 @@ int satoko_solve(solver_t *s) } if (s->opts.verbose) print_stats(s); + solver_cancel_until(s, vec_uint_size(s->assumptions)); return status; } @@ -309,7 +315,6 @@ int satoko_final_conflict(solver_t *s, unsigned *out) memcpy(out, vec_uint_data(s->final_conflict), sizeof(unsigned) * vec_uint_size(s->final_conflict)); return vec_uint_size(s->final_conflict); - } satoko_stats_t satoko_stats(satoko_t *s) @@ -324,6 +329,7 @@ void satoko_bookmark(satoko_t *s) s->book_cl_lrnt = vec_uint_size(s->learnts); s->book_vars = vec_char_size(s->assigns); s->book_trail = vec_uint_size(s->trail); + s->opts.no_simplify = 1; } void satoko_unbookmark(satoko_t *s) @@ -333,6 +339,7 @@ void satoko_unbookmark(satoko_t *s) s->book_cdb = 0; s->book_vars = 0; s->book_trail = 0; + s->opts.no_simplify = 0; } void satoko_reset(satoko_t *s) @@ -442,4 +449,43 @@ void satoko_unmark_cone(satoko_t *s, int *pvars, int n_vars) var_clean_mark(s, pvars[i]); } +void satoko_write_dimacs(satoko_t *s, char *fname, int wrt_lrnt, int zero_var) +{ + FILE *file; + unsigned i; + unsigned n_vars = vec_act_size(s->activity); + unsigned n_orig = vec_uint_size(s->originals) + vec_uint_size(s->assumptions); + unsigned n_lrnts = vec_uint_size(s->learnts); + unsigned *array; + + assert(wrt_lrnt == 0 || wrt_lrnt == 1); + assert(zero_var == 0 || zero_var == 1); + if (fname != NULL) + file = fopen(fname, "w"); + else + file = stdout; + + if (file == NULL) { + printf( "Error: Cannot open output file.\n"); + return; + } + fprintf(file, "p cnf %d %d\n", n_vars, wrt_lrnt ? n_orig + n_lrnts : n_orig); + array = vec_uint_data(s->assumptions); + for (i = 0; i < vec_uint_size(s->assumptions); i++) + fprintf(file, "%d\n", array[i] & 1 ? -(array[i] + !zero_var) : array[i] + !zero_var); + + array = vec_uint_data(s->originals); + for (i = 0; i < vec_uint_size(s->originals); i++) + clause_dump(file, clause_read(s, array[i]), !zero_var); + + if (wrt_lrnt) { + printf(" Lertns %u", n_lrnts); + array = vec_uint_data(s->learnts); + for (i = 0; i < n_lrnts; i++) + clause_dump(file, clause_read(s, array[i]), !zero_var); + } + +} + + ABC_NAMESPACE_IMPL_END -- 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(-) 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(-) 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(-) 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 bd9b7d64e1131f45699a5a4b20b4bf44795da857 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 1 Mar 2017 13:59:23 -0800 Subject: Adding efficient procedure to minimize the set of assumptions. --- src/sat/bmc/bmcClp.c | 26 ++++++++++++++++++++++++ src/sat/bsat/satSolver.c | 52 ++++++++++++++++++++++++++++++++++++++++++++++++ src/sat/bsat/satSolver.h | 1 + 3 files changed, 79 insertions(+) diff --git a/src/sat/bmc/bmcClp.c b/src/sat/bmc/bmcClp.c index cfc608b1..2ac94da5 100644 --- a/src/sat/bmc/bmcClp.c +++ b/src/sat/bmc/bmcClp.c @@ -353,11 +353,37 @@ int Bmc_CollapseIrredundantFull( Vec_Str_t * vSop, int nCubes, int nVars ) SeeAlso [] ***********************************************************************/ +int Bmc_CollapseExpandRound2( sat_solver * pSat, Vec_Int_t * vLits, Vec_Int_t * vTemp, int nBTLimit, int fOnOffSetLit ) +{ + // put into new array + int i, iLit, nLits; + Vec_IntClear( vTemp ); + Vec_IntForEachEntry( vLits, iLit, i ) + if ( iLit != -1 ) + Vec_IntPush( vTemp, iLit ); + assert( Vec_IntSize(vTemp) > 0 ); + // assume condition literal + if ( fOnOffSetLit >= 0 ) + sat_solver_push( pSat, fOnOffSetLit ); + // minimize + nLits = sat_solver_minimize_assumptions( pSat, Vec_IntArray(vTemp), Vec_IntSize(vTemp), nBTLimit ); + Vec_IntShrink( vTemp, nLits ); + // assume conditional literal + if ( fOnOffSetLit >= 0 ) + sat_solver_pop( pSat ); + // modify output literas + Vec_IntForEachEntry( vLits, iLit, i ) + if ( iLit != -1 && Vec_IntFind(vTemp, iLit) == -1 ) + Vec_IntWriteEntry( vLits, i, -1 ); + return 0; +} + int Bmc_CollapseExpandRound( sat_solver * pSat, sat_solver * pSatOn, Vec_Int_t * vLits, Vec_Int_t * vNums, Vec_Int_t * vTemp, int nBTLimit, int fCanon, int fOnOffSetLit ) { int fProfile = 0; int k, n, iLit, status; abctime clk; + //return Bmc_CollapseExpandRound2( pSat, vLits, vTemp, nBTLimit, fOnOffSetLit ); // try removing one literal at a time for ( k = Vec_IntSize(vLits) - 1; k >= 0; k-- ) { diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index df9ada8e..3d24161e 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -2168,6 +2168,58 @@ int sat_solver_solve_lexsat( sat_solver* s, int * pLits, int nLits ) return status; } +// This procedure is called on a set of assumptions to minimize their number. +// The procedure relies on the fact that the current set of assumptions is UNSAT. +// It receives and returns SAT solver without assumptions. It returns the number +// of assumptions after minimization. The set of assumptions is returned in pLits. +int sat_solver_minimize_assumptions( sat_solver* s, int * pLits, int nLits, int nConfLimit ) +{ + int i, k, nLitsL, nLitsR, nResL, nResR; + if ( nLits == 1 ) + { + // since the problem is UNSAT, we will try to solve it without assuming the last literal + // the result is UNSAT, the last literal can be dropped; otherwise, it is needed + int status = l_False; + int Temp = s->nConfLimit; + s->nConfLimit = nConfLimit; + status = sat_solver_solve_internal( s ); + s->nConfLimit = Temp; + return (int)(status != l_False); // return 1 if the problem is not UNSAT + } + assert( nLits >= 2 ); + nLitsR = nLits / 2; + nLitsL = nLits - nLitsR; + // assume the left lits + for ( i = 0; i < nLitsL; i++ ) + if ( !sat_solver_push(s, pLits[i]) ) + { + for ( k = i; k >= 0; k-- ) + sat_solver_pop(s); + return sat_solver_minimize_assumptions( s, pLits, i+1, nConfLimit ); + } + // solve for the right lits + nResL = sat_solver_minimize_assumptions( s, pLits + nLitsL, nLitsR, nConfLimit ); + for ( i = 0; i < nLitsL; i++ ) + sat_solver_pop(s); + // swap literals + assert( nResL <= nLitsL ); + for ( i = 0; i < nResL; i++ ) + ABC_SWAP( int, pLits[i], pLits[nLitsL+i] ); + // assume the right lits + for ( i = 0; i < nResL; i++ ) + if ( !sat_solver_push(s, pLits[i]) ) + { + for ( k = i; k >= 0; k-- ) + sat_solver_pop(s); + return sat_solver_minimize_assumptions( s, pLits, i+1, nConfLimit ); + } + // solve for the left lits + nResR = sat_solver_minimize_assumptions( s, pLits + nResL, nLitsL, nConfLimit ); + for ( i = 0; i < nResL; i++ ) + sat_solver_pop(s); + return nResL + nResR; +} + int sat_solver_nvars(sat_solver* s) { diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h index 5a8483c1..ac0b6e8d 100644 --- a/src/sat/bsat/satSolver.h +++ b/src/sat/bsat/satSolver.h @@ -50,6 +50,7 @@ extern int sat_solver_simplify(sat_solver* s); extern int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal); extern int sat_solver_solve_internal(sat_solver* s); extern int sat_solver_solve_lexsat(sat_solver* s, int * pLits, int nLits); +extern int sat_solver_minimize_assumptions( sat_solver* s, int * pLits, int nLits, int nConfLimit ); extern int sat_solver_push(sat_solver* s, int p); extern void sat_solver_pop(sat_solver* s); extern void sat_solver_set_resource_limits(sat_solver* s, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal); -- cgit v1.2.3 From 7747d89c905a85c8ab6c03e987ad9747032d919d Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 1 Mar 2017 20:29:09 -0800 Subject: Adding alternative generalization procedure. --- src/proof/pdr/pdrCore.c | 164 +++++++++++++++++++++++++++++++++++++++++++++-- src/sat/bsat/satSolver.c | 2 +- 2 files changed, 159 insertions(+), 7 deletions(-) diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c index 501f9be6..0394040f 100644 --- a/src/proof/pdr/pdrCore.c +++ b/src/proof/pdr/pdrCore.c @@ -497,7 +497,7 @@ int ZPdr_ManDown( Pdr_Man_t * p, int k, Pdr_Set_t ** ppCube, Pdr_Set_t * pPred, SeeAlso [] ***********************************************************************/ -static inline void Vec_IntSelectSortCostReverseLit( int * pArray, int nSize, Vec_Int_t * vCosts ) +static inline int Vec_IntSelectSortCostReverseLit( int * pArray, int nSize, Vec_Int_t * vCosts ) { int i, j, best_i; for ( i = 0; i < nSize-1; i++ ) @@ -508,6 +508,137 @@ static inline void Vec_IntSelectSortCostReverseLit( int * pArray, int nSize, Vec best_i = j; ABC_SWAP( int, pArray[i], pArray[best_i] ); } + return 1; +} + +/**Function************************************************************* + + Synopsis [Performs generalization using a different idea.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Pdr_ManGeneralize2( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppCubeMin ) +{ + int fUseMinAss = 0; + sat_solver * pSat = Pdr_ManFetchSolver( p, k ); + int Order = Vec_IntSelectSortCostReverseLit( pCube->Lits, pCube->nLits, p->vPrio ); + Vec_Int_t * vLits1 = Pdr_ManCubeToLits( p, k, pCube, 1, 0 ); + int RetValue, Count = 0, iLit, Lits[2], nLits = Vec_IntSize( vLits1 ); + // create free variables + int i, iUseVar, iAndVar; + iAndVar = Pdr_ManFreeVar(p, k); + for ( i = 1; i < nLits; i++ ) + Pdr_ManFreeVar(p, k); + iUseVar = Pdr_ManFreeVar(p, k); + for ( i = 1; i < nLits; i++ ) + Pdr_ManFreeVar(p, k); + assert( iUseVar == iAndVar + nLits ); + // if there is only one positive literal, put it in front and always assume + if ( fUseMinAss ) + { + for ( i = 0; i < pCube->nLits; i++ ) + Count += !Abc_LitIsCompl(pCube->Lits[i]); + if ( Count == 1 ) + { + for ( i = 0; i < pCube->nLits; i++ ) + if ( !Abc_LitIsCompl(pCube->Lits[i]) ) + break; + assert( i < pCube->nLits ); + ABC_SWAP( int, pCube->Lits[0], pCube->Lits[i] ); + } + } + // add clauses for the additional AND-gates + Vec_IntForEachEntry( vLits1, iLit, i ) + { + sat_solver_add_buffer_enable( pSat, iAndVar + i, Abc_Lit2Var(iLit), iUseVar + i, Abc_LitIsCompl(iLit) ); + Vec_IntWriteEntry( vLits1, i, Abc_Var2Lit(iAndVar + i, 0) ); + } + // add clauses for the additional OR-gate + RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits1), Vec_IntLimit(vLits1) ); + assert( RetValue == 1 ); + // add implications + vLits1 = Pdr_ManCubeToLits( p, k, pCube, 0, 1 ); + assert( Vec_IntSize(vLits1) == nLits ); + Vec_IntForEachEntry( vLits1, iLit, i ) + { + Lits[0] = Abc_Var2Lit(iUseVar + i, 1); + Lits[1] = iLit; + RetValue = sat_solver_addclause( pSat, Lits, Lits+2 ); + assert( RetValue == 1 ); + Vec_IntWriteEntry( vLits1, i, Abc_Var2Lit(iUseVar + i, 0) ); + } + sat_solver_compress( pSat ); + // perform minimization + if ( fUseMinAss ) + { + if ( Count == 1 ) + { + if ( !sat_solver_push(pSat, Vec_IntEntry(vLits1, 0)) ) // UNSAT after assuming the first (mandatory) literal + nLits = 1; + else + nLits = 1 + sat_solver_minimize_assumptions( pSat, Vec_IntArray(vLits1)+1, nLits-1, p->pPars->nConfLimit ); + sat_solver_pop(pSat); // unassume the first literal + } + else + nLits = sat_solver_minimize_assumptions( pSat, Vec_IntArray(vLits1), nLits, p->pPars->nConfLimit ); + Vec_IntShrink( vLits1, nLits ); + } + else + { + int k, Entry; + // try removing one literal at a time in the old-fashioned way + Vec_Int_t * vTemp = Vec_IntAlloc( nLits ); + for ( i = 0; i < nLits; i++ ) + { + // check init state + if ( Pdr_SetIsInit(pCube, i) ) + continue; + // load remaining literals + Vec_IntClear( vTemp ); + Vec_IntForEachEntry( vLits1, Entry, k ) + if ( Entry != -1 && k != i ) + Vec_IntPush( vTemp, Entry ); + // solve with assumptions + RetValue = sat_solver_solve( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp), p->pPars->nConfLimit, 0, 0, 0 ); + if ( RetValue == l_False ) + Vec_IntWriteEntry( vLits1, i, -1 ); + } + Vec_IntFree( vTemp ); + // compact + k = 0; + Vec_IntForEachEntry( vLits1, Entry, i ) + if ( Entry != -1 ) + Vec_IntWriteEntry( vLits1, k++, Entry ); + Vec_IntShrink( vLits1, k ); + } + // remap auxiliary literals into original literals + Vec_IntForEachEntry( vLits1, iLit, i ) + Vec_IntWriteEntry( vLits1, i, pCube->Lits[Abc_Lit2Var(iLit)-iUseVar] ); + // make sure the cube has at least one positive literal + if ( fUseMinAss ) + { + Vec_IntForEachEntry( vLits1, iLit, i ) + if ( !Abc_LitIsCompl(iLit) ) + break; + if ( i == Vec_IntSize(vLits1) ) + { + // find positive lit in the cube + for ( i = 0; i < pCube->nLits; i++ ) + if ( !Abc_LitIsCompl(pCube->Lits[i]) ) + break; + assert( i < pCube->nLits ); + Vec_IntPush( vLits1, pCube->Lits[i] ); + } + } + // create a subset cube + *ppCubeMin = Pdr_SetCreateSubset( pCube, Vec_IntArray(vLits1), Vec_IntSize(vLits1) ); + assert( !Pdr_SetIsInit(*ppCubeMin, -1) ); + return 0; } /**Function************************************************************* @@ -543,8 +674,6 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP p->tGeneral += clock() - clk; return 0; } - - keep = p->pPars->fSkipDown ? NULL : Hash_IntAlloc( 1 ); // reduce clause using assumptions // pCubeMin = Pdr_SetDup( pCube ); @@ -552,6 +681,31 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP if ( pCubeMin == NULL ) pCubeMin = Pdr_SetDup( pCube ); + // perform simplified generalization + if ( p->pPars->fSimpleGeneral ) + { + assert( pCubeMin->nLits > 0 ); + if ( pCubeMin->nLits > 1 ) + { + RetValue = Pdr_ManGeneralize2( p, k, pCubeMin, ppCubeMin ); + Pdr_SetDeref( pCubeMin ); + assert( ppCubeMin != NULL ); + pCubeMin = *ppCubeMin; + } + *ppCubeMin = pCubeMin; + if ( p->pPars->fVeryVerbose ) + { + printf("Cube:\n"); + for ( i = 0; i < pCubeMin->nLits; i++) + printf ("%d ", pCubeMin->Lits[i]); + printf("\n"); + } + p->tGeneral += Abc_Clock() - clk; + return 1; + } + + keep = p->pPars->fSkipDown ? NULL : Hash_IntAlloc( 1 ); + // perform generalization if ( !p->pPars->fSkipGeneral ) { @@ -691,9 +845,7 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP { printf("Cube:\n"); for ( i = 0; i < pCubeMin->nLits; i++) - { - printf ("%d ", pCubeMin->Lits[i]); - } + printf ("%d ", pCubeMin->Lits[i]); printf("\n"); } *ppCubeMin = pCubeMin; diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index 3d24161e..47fba5e3 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -2178,7 +2178,7 @@ int sat_solver_minimize_assumptions( sat_solver* s, int * pLits, int nLits, int if ( nLits == 1 ) { // since the problem is UNSAT, we will try to solve it without assuming the last literal - // the result is UNSAT, the last literal can be dropped; otherwise, it is needed + // if the result is UNSAT, the last literal can be dropped; otherwise, it is needed int status = l_False; int Temp = s->nConfLimit; s->nConfLimit = nConfLimit; -- cgit v1.2.3 From f419f2e81298df40f90a6ce7d7cdd2e3eaed4918 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 1 Mar 2017 20:30:19 -0800 Subject: Adding alternative generalization procedure. --- src/proof/pdr/pdrCore.c | 1 + 1 file changed, 1 insertion(+) diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c index 0394040f..9d42417b 100644 --- a/src/proof/pdr/pdrCore.c +++ b/src/proof/pdr/pdrCore.c @@ -638,6 +638,7 @@ int Pdr_ManGeneralize2( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** pp // create a subset cube *ppCubeMin = Pdr_SetCreateSubset( pCube, Vec_IntArray(vLits1), Vec_IntSize(vLits1) ); assert( !Pdr_SetIsInit(*ppCubeMin, -1) ); + Order = 0; return 0; } -- cgit v1.2.3 From 160d1311c9ca687cffe0d9ee6752afdc3f43864c Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 2 Mar 2017 11:10:16 -0800 Subject: Adding efficient procedure to minimize the set of assumptions (improved literal reordering). --- src/sat/bsat/satSolver.c | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index 47fba5e3..aad0df51 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -2203,8 +2203,15 @@ int sat_solver_minimize_assumptions( sat_solver* s, int * pLits, int nLits, int sat_solver_pop(s); // swap literals assert( nResL <= nLitsL ); +// for ( i = 0; i < nResL; i++ ) +// ABC_SWAP( int, pLits[i], pLits[nLitsL+i] ); + veci_resize( &s->temp_clause, 0 ); + for ( i = 0; i < nLitsL; i++ ) + veci_push( &s->temp_clause, pLits[i] ); for ( i = 0; i < nResL; i++ ) - ABC_SWAP( int, pLits[i], pLits[nLitsL+i] ); + pLits[i] = pLits[nLitsL+i]; + for ( i = 0; i < nLitsL; i++ ) + pLits[nResL+i] = veci_begin(&s->temp_clause)[i]; // assume the right lits for ( i = 0; i < nResL; i++ ) if ( !sat_solver_push(s, pLits[i]) ) -- cgit v1.2.3 From ff88edd6645bebeb2cbe63b02e5db62b3e140d53 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 2 Mar 2017 13:01:32 -0800 Subject: Adding alternative generalization procedure. --- src/proof/pdr/pdrCore.c | 58 ++++++++++++++++++++---------- src/sat/bsat/satSolver.c | 94 ++++++++++++++++++++++++++++++++++++++++++++++-- src/sat/bsat/satSolver.h | 1 + 3 files changed, 132 insertions(+), 21 deletions(-) diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c index 9d42417b..60454752 100644 --- a/src/proof/pdr/pdrCore.c +++ b/src/proof/pdr/pdrCore.c @@ -288,7 +288,7 @@ int * Pdr_ManSortByPriority( Pdr_Man_t * p, Pdr_Set_t * pCube ) best_i = i; for ( j = i+1; j < nSize; j++ ) // if ( pArray[j] < pArray[best_i] ) - if ( pPrios[pCube->Lits[pArray[j]]>>1] < pPrios[pCube->Lits[pArray[best_i]]>>1] ) + if ( pPrios[pCube->Lits[pArray[j]]>>1] < pPrios[pCube->Lits[pArray[best_i]]>>1] ) // list lower priority first (these will be removed first) best_i = j; temp = pArray[i]; pArray[i] = pArray[best_i]; @@ -488,7 +488,7 @@ int ZPdr_ManDown( Pdr_Man_t * p, int k, Pdr_Set_t ** ppCube, Pdr_Set_t * pPred, /**Function************************************************************* - Synopsis [Specialized sorting of flops based on cost.] + Synopsis [Specialized sorting of flops based on priority.] Description [] @@ -497,14 +497,14 @@ int ZPdr_ManDown( Pdr_Man_t * p, int k, Pdr_Set_t ** ppCube, Pdr_Set_t * pPred, SeeAlso [] ***********************************************************************/ -static inline int Vec_IntSelectSortCostReverseLit( int * pArray, int nSize, Vec_Int_t * vCosts ) +static inline int Vec_IntSelectSortPrioReverseLit( int * pArray, int nSize, Vec_Int_t * vPrios ) { int i, j, best_i; for ( i = 0; i < nSize-1; i++ ) { best_i = i; for ( j = i+1; j < nSize; j++ ) - if ( Vec_IntEntry(vCosts, Abc_Lit2Var(pArray[j])) > Vec_IntEntry(vCosts, Abc_Lit2Var(pArray[best_i])) ) + if ( Vec_IntEntry(vPrios, Abc_Lit2Var(pArray[j])) > Vec_IntEntry(vPrios, Abc_Lit2Var(pArray[best_i])) ) // prefer higher priority best_i = j; ABC_SWAP( int, pArray[i], pArray[best_i] ); } @@ -526,7 +526,7 @@ int Pdr_ManGeneralize2( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** pp { int fUseMinAss = 0; sat_solver * pSat = Pdr_ManFetchSolver( p, k ); - int Order = Vec_IntSelectSortCostReverseLit( pCube->Lits, pCube->nLits, p->vPrio ); + int Order = Vec_IntSelectSortPrioReverseLit( pCube->Lits, pCube->nLits, p->vPrio ); Vec_Int_t * vLits1 = Pdr_ManCubeToLits( p, k, pCube, 1, 0 ); int RetValue, Count = 0, iLit, Lits[2], nLits = Vec_IntSize( vLits1 ); // create free variables @@ -541,7 +541,7 @@ int Pdr_ManGeneralize2( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** pp // if there is only one positive literal, put it in front and always assume if ( fUseMinAss ) { - for ( i = 0; i < pCube->nLits; i++ ) + for ( i = 0; i < pCube->nLits && Count < 2; i++ ) Count += !Abc_LitIsCompl(pCube->Lits[i]); if ( Count == 1 ) { @@ -549,7 +549,10 @@ int Pdr_ManGeneralize2( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** pp if ( !Abc_LitIsCompl(pCube->Lits[i]) ) break; assert( i < pCube->nLits ); - ABC_SWAP( int, pCube->Lits[0], pCube->Lits[i] ); + iLit = pCube->Lits[i]; + for ( ; i > 0; i-- ) + pCube->Lits[i] = pCube->Lits[i-1]; + pCube->Lits[0] = iLit; } } // add clauses for the additional AND-gates @@ -576,35 +579,51 @@ int Pdr_ManGeneralize2( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** pp // perform minimization if ( fUseMinAss ) { - if ( Count == 1 ) + if ( Count == 1 ) // always assume the only positive literal { - if ( !sat_solver_push(pSat, Vec_IntEntry(vLits1, 0)) ) // UNSAT after assuming the first (mandatory) literal + if ( !sat_solver_push(pSat, Vec_IntEntry(vLits1, 0)) ) // UNSAT with the first (mandatory) literal nLits = 1; else - nLits = 1 + sat_solver_minimize_assumptions( pSat, Vec_IntArray(vLits1)+1, nLits-1, p->pPars->nConfLimit ); + nLits = 1 + sat_solver_minimize_assumptions2( pSat, Vec_IntArray(vLits1)+1, nLits-1, p->pPars->nConfLimit ); sat_solver_pop(pSat); // unassume the first literal } else - nLits = sat_solver_minimize_assumptions( pSat, Vec_IntArray(vLits1), nLits, p->pPars->nConfLimit ); + nLits = sat_solver_minimize_assumptions2( pSat, Vec_IntArray(vLits1), nLits, p->pPars->nConfLimit ); Vec_IntShrink( vLits1, nLits ); } else { - int k, Entry; // try removing one literal at a time in the old-fashioned way + int k, Entry; Vec_Int_t * vTemp = Vec_IntAlloc( nLits ); - for ( i = 0; i < nLits; i++ ) + for ( i = nLits - 1; i >= 0; i-- ) { - // check init state - if ( Pdr_SetIsInit(pCube, i) ) - continue; + // if we are about to remove a positive lit, make sure at least one positive lit remains + if ( !Abc_LitIsCompl(Vec_IntEntry(vLits1, i)) ) + { + Vec_IntForEachEntry( vLits1, iLit, k ) + if ( iLit != -1 && k != i && !Abc_LitIsCompl(iLit) ) + break; + if ( k == Vec_IntSize(vLits1) ) // no other positive literals, except the i-th one + continue; + } // load remaining literals Vec_IntClear( vTemp ); Vec_IntForEachEntry( vLits1, Entry, k ) if ( Entry != -1 && k != i ) Vec_IntPush( vTemp, Entry ); + else if ( Entry != -1 ) // assume opposite literal + Vec_IntPush( vTemp, Abc_LitNot(Entry) ); // solve with assumptions RetValue = sat_solver_solve( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp), p->pPars->nConfLimit, 0, 0, 0 ); + // commit the literal + if ( RetValue == l_False ) + { + int LitNot = Abc_LitNot(Vec_IntEntry(vLits1, i)); + int RetValue = sat_solver_addclause( pSat, &LitNot, &LitNot+1 ); + assert( RetValue ); + } + // update the clause if ( RetValue == l_False ) Vec_IntWriteEntry( vLits1, i, -1 ); } @@ -625,7 +644,7 @@ int Pdr_ManGeneralize2( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** pp Vec_IntForEachEntry( vLits1, iLit, i ) if ( !Abc_LitIsCompl(iLit) ) break; - if ( i == Vec_IntSize(vLits1) ) + if ( i == Vec_IntSize(vLits1) ) // has no positive literals { // find positive lit in the cube for ( i = 0; i < pCube->nLits; i++ ) @@ -633,7 +652,10 @@ int Pdr_ManGeneralize2( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** pp break; assert( i < pCube->nLits ); Vec_IntPush( vLits1, pCube->Lits[i] ); +// printf( "-" ); } +// else +// printf( "+" ); } // create a subset cube *ppCubeMin = Pdr_SetCreateSubset( pCube, Vec_IntArray(vLits1), Vec_IntSize(vLits1) ); @@ -664,7 +686,7 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP // if there is no induction, return *ppCubeMin = NULL; if ( p->pPars->fFlopOrder ) - Vec_IntSelectSortCostReverseLit( pCube->Lits, pCube->nLits, p->vPrio ); + Vec_IntSelectSortPrioReverseLit( pCube->Lits, pCube->nLits, p->vPrio ); RetValue = Pdr_ManCheckCube( p, k, pCube, ppPred, p->pPars->nConfLimit, 0, 1 ); if ( p->pPars->fFlopOrder ) Vec_IntSelectSort( pCube->Lits, pCube->nLits ); diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index aad0df51..fe7e65fe 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -2187,8 +2187,8 @@ int sat_solver_minimize_assumptions( sat_solver* s, int * pLits, int nLits, int return (int)(status != l_False); // return 1 if the problem is not UNSAT } assert( nLits >= 2 ); - nLitsR = nLits / 2; - nLitsL = nLits - nLitsR; + nLitsL = nLits / 2; + nLitsR = nLits - nLitsL; // assume the left lits for ( i = 0; i < nLitsL; i++ ) if ( !sat_solver_push(s, pLits[i]) ) @@ -2202,7 +2202,7 @@ int sat_solver_minimize_assumptions( sat_solver* s, int * pLits, int nLits, int for ( i = 0; i < nLitsL; i++ ) sat_solver_pop(s); // swap literals - assert( nResL <= nLitsL ); +// assert( nResL <= nLitsL ); // for ( i = 0; i < nResL; i++ ) // ABC_SWAP( int, pLits[i], pLits[nLitsL+i] ); veci_resize( &s->temp_clause, 0 ); @@ -2227,6 +2227,94 @@ int sat_solver_minimize_assumptions( sat_solver* s, int * pLits, int nLits, int return nResL + nResR; } +// This is a specialized version of the above procedure with several custom changes: +// - makes sure that at least one of the marked literals is preserved in the clause +// - sets literals to zero when they do not have to be used +// - sets literals to zero for disproved variables +int sat_solver_minimize_assumptions2( sat_solver* s, int * pLits, int nLits, int nConfLimit ) +{ + int i, k, nLitsL, nLitsR, nResL, nResR; + if ( nLits == 1 ) + { + // since the problem is UNSAT, we will try to solve it without assuming the last literal + // if the result is UNSAT, the last literal can be dropped; otherwise, it is needed + int RetValue = 1, LitNot = Abc_LitNot(pLits[0]); + int status = l_False; + int Temp = s->nConfLimit; + s->nConfLimit = nConfLimit; + + RetValue = sat_solver_push( s, LitNot ); assert( RetValue ); + status = sat_solver_solve_internal( s ); + sat_solver_pop( s ); + + // if the problem is UNSAT, add clause + if ( status == l_False ) + { + RetValue = sat_solver_addclause( s, &LitNot, &LitNot+1 ); + assert( RetValue ); + } + + s->nConfLimit = Temp; + return (int)(status != l_False); // return 1 if the problem is not UNSAT + } + assert( nLits >= 2 ); + nLitsL = nLits / 2; + nLitsR = nLits - nLitsL; + // assume the left lits + for ( i = 0; i < nLitsL; i++ ) + if ( !sat_solver_push(s, pLits[i]) ) + { + for ( k = i; k >= 0; k-- ) + sat_solver_pop(s); + + // add clauses for these literal + for ( k = i+1; k > nLitsL; k++ ) + { + int LitNot = Abc_LitNot(pLits[i]); + int RetValue = sat_solver_addclause( s, &LitNot, &LitNot+1 ); + assert( RetValue ); + } + + return sat_solver_minimize_assumptions2( s, pLits, i+1, nConfLimit ); + } + // solve for the right lits + nResL = sat_solver_minimize_assumptions2( s, pLits + nLitsL, nLitsR, nConfLimit ); + for ( i = 0; i < nLitsL; i++ ) + sat_solver_pop(s); + // swap literals +// assert( nResL <= nLitsL ); + veci_resize( &s->temp_clause, 0 ); + for ( i = 0; i < nLitsL; i++ ) + veci_push( &s->temp_clause, pLits[i] ); + for ( i = 0; i < nResL; i++ ) + pLits[i] = pLits[nLitsL+i]; + for ( i = 0; i < nLitsL; i++ ) + pLits[nResL+i] = veci_begin(&s->temp_clause)[i]; + // assume the right lits + for ( i = 0; i < nResL; i++ ) + if ( !sat_solver_push(s, pLits[i]) ) + { + for ( k = i; k >= 0; k-- ) + sat_solver_pop(s); + + // add clauses for these literal + for ( k = i+1; k > nResL; k++ ) + { + int LitNot = Abc_LitNot(pLits[i]); + int RetValue = sat_solver_addclause( s, &LitNot, &LitNot+1 ); + assert( RetValue ); + } + + return sat_solver_minimize_assumptions2( s, pLits, i+1, nConfLimit ); + } + // solve for the left lits + nResR = sat_solver_minimize_assumptions2( s, pLits + nResL, nLitsL, nConfLimit ); + for ( i = 0; i < nResL; i++ ) + sat_solver_pop(s); + return nResL + nResR; +} + + int sat_solver_nvars(sat_solver* s) { diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h index ac0b6e8d..5191b2cd 100644 --- a/src/sat/bsat/satSolver.h +++ b/src/sat/bsat/satSolver.h @@ -51,6 +51,7 @@ extern int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT extern int sat_solver_solve_internal(sat_solver* s); extern int sat_solver_solve_lexsat(sat_solver* s, int * pLits, int nLits); extern int sat_solver_minimize_assumptions( sat_solver* s, int * pLits, int nLits, int nConfLimit ); +extern int sat_solver_minimize_assumptions2( sat_solver* s, int * pLits, int nLits, int nConfLimit ); extern int sat_solver_push(sat_solver* s, int p); extern void sat_solver_pop(sat_solver* s); extern void sat_solver_set_resource_limits(sat_solver* s, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal); -- cgit v1.2.3 From fc904409c3ff011ed1eb8ff391651f2c44e0f46b Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 2 Mar 2017 13:02:07 -0800 Subject: Network interface exploration. --- src/aig/miniaig/ndr.h | 614 ++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 614 insertions(+) create mode 100644 src/aig/miniaig/ndr.h diff --git a/src/aig/miniaig/ndr.h b/src/aig/miniaig/ndr.h new file mode 100644 index 00000000..d7f425e8 --- /dev/null +++ b/src/aig/miniaig/ndr.h @@ -0,0 +1,614 @@ +/**CFile**************************************************************** + + FileName [ndr.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Format for word-level design representation.] + + Synopsis [External declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - August 22, 2014.] + + Revision [$Id: ndr.h,v 1.00 2014/09/12 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef ABC__base__ndr__ndr_h +#define ABC__base__ndr__ndr_h + + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +#include +#include +#include +#include + +//ABC_NAMESPACE_HEADER_START + +#ifdef _WIN32 +#define inline __inline +#endif + +/* + For the lack of a better name, this format is called New Data Representation (NDR). + + NDR is based on the following principles: + - complex data is composed of individual records + - a record has one of several known types (module, name, range, fanins, etc) + - a record can be atomic, for example, a name or an operator type + - a record can be composed of other records (for example, a module is composed of objects, etc) + - the stored data should be easy to write into and read from a file, or pass around as a memory buffer + - the format should be simple, easy to use, low-memory, and extensible + - new record types can be added by the user as needed + + The implementation is based on the following ideas: + - a record is composed of two parts (the header followed by the body) + - the header contains two items (the record type and the body size, measured in terms of 4-byte integers) + - the body contains as many entries as stated in the record size + - if a record is composed of other records, its body contains these records + + As an example, consider a name. It can be a module name, an object name, or a net name. + A record storing one name has a header {NDR_NAME, 1} containing record type (NDR_NAME) and size (1), + The body of the record is composed of one unsigned integer representing the name (say, 357). + So the complete record looks as follows: {
, } = { {NDR_NAME, 1}, {357} }. + + As another example, consider a two-input AND-gate. In this case, the recent is composed + of a header {NDR_OBJECT, 4} containing record type (NDR_OBJECT) and the body size (4), followed + by an array of records creating the AND-gate: (a) name, (b) operation type, (c) fanins. + The complete record looks as follows: { {NDR_OBJECT, 5}, {{{NDR_NAME, 1}, 357}, {{NDR_OPERTYPE, 1}, WLC_OBJ_LOGIC_AND}, + {{NDR_INPUT, 2}, {, }}} }. Please note that only body entries are counted towards size. + In the case of one name, there is only one body entry. In the case of the AND-gate, there are 4 body entries + (name ID, gate type, first fanin, second fanin). + + Headers and bodies of all objects are stored differently. Headers are stored in an array of unsigned chars, + while bodies are stored in the array of 4-byte unsigned integers. This is important for memory efficiency. + However, the user does not see these details. + + To estimate memory usage, we can assume that each header takes 1 byte and each body entry contains 4 bytes. + A name takes 5 bytes, and an AND-gate takes 1 * NumHeaders + 4 * NumBodyEntries = 1 * 4 + 4 * 4 = 20 bytes. + Not bad. The same as memory usage in a well-designed AIG package with structural hashing. + + Comments: + - it is assumed that all port names, net names, and instance names are hashed into 1-based integer numbers called name IDs + - nets are not explicitly represented but their name ID are used to establish connectivity between the objects + - primary input and primary output objects have to be explicitly created (as shown in the example below) + - object inputs are name IDs of the driving nets; object outputs are name IDs of the driven nets + - objects can be added to a module in any order + - if the ordering of inputs/outputs/flops of a module is not provided as a separate record, + their ordering is determined by the order of their appearance of their records in the body of the module + - if range limits and signedness are all 0, it is assumed that it is a Boolean object + - if left limit and right limit of a range are equal, it is assumed that the range contains one bit + - instances of known operators can have types defined by Wlc_ObjType_t below + - instances of user modules have type equal to the name ID of the module plus 1000 + - initial states of the flops are given as char-strings containing 0, 1, and 'x' + (for example, "4'b10XX" is an init state of a 4-bit flop with bit-level init states const1, const0, unknown, unknown) + - word-level constants are represented as char-strings given in the same way as they would appear in a Verilog file + (for example, the 16-bit constant 10 is represented as a string "4'b1010". This string contains 8 bytes, + including the char '\0' to denote the end of the string. It will take 2 unsigned ints, therefore + its record will look as follows { {NDR_FUNCTION, 2}, {"4'b1010"} }, but the user does not see these details. + The user only gives "4'b1010" as an argument (char * pFunction) to the above procedure Ndr_ModuleAddObject(). +*/ + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +// record types +typedef enum { + NDR_NONE = 0, // 0: unused + NDR_DESIGN, // 1: design (or library of modules) + NDR_MODULE, // 2: one module + NDR_OBJECT, // 3: object + NDR_INPUT, // 4: input + NDR_OUTPUT, // 5: output + NDR_OPERTYPE, // 6: operator type (buffer, shifter, adder, etc) + NDR_NAME, // 7: name + NDR_RANGE, // 8: bit range + NDR_FUNCTION, // 9: specified for some operators (PLAs, etc) + NDR_UNKNOWN // 10: unknown +} Ndr_RecordType_t; + +// operator types +typedef enum { + WLC_OBJ_NONE = 0, // 00: unknown + WLC_OBJ_PI, // 01: primary input + WLC_OBJ_PO, // 02: primary output + WLC_OBJ_FO, // 03: flop output (unused) + WLC_OBJ_FI, // 04: flop input (unused) + WLC_OBJ_FF, // 05: flop + WLC_OBJ_CONST, // 06: constant + WLC_OBJ_BUF, // 07: buffer + WLC_OBJ_MUX, // 08: multiplexer + WLC_OBJ_SHIFT_R, // 09: shift right + WLC_OBJ_SHIFT_RA, // 10: shift right (arithmetic) + WLC_OBJ_SHIFT_L, // 11: shift left + WLC_OBJ_SHIFT_LA, // 12: shift left (arithmetic) + WLC_OBJ_ROTATE_R, // 13: rotate right + WLC_OBJ_ROTATE_L, // 14: rotate left + WLC_OBJ_BIT_NOT, // 15: bitwise NOT + WLC_OBJ_BIT_AND, // 16: bitwise AND + WLC_OBJ_BIT_OR, // 17: bitwise OR + WLC_OBJ_BIT_XOR, // 18: bitwise XOR + WLC_OBJ_BIT_NAND, // 19: bitwise AND + WLC_OBJ_BIT_NOR, // 20: bitwise OR + WLC_OBJ_BIT_NXOR, // 21: bitwise NXOR + WLC_OBJ_BIT_SELECT, // 22: bit selection + WLC_OBJ_BIT_CONCAT, // 23: bit concatenation + WLC_OBJ_BIT_ZEROPAD, // 24: zero padding + WLC_OBJ_BIT_SIGNEXT, // 25: sign extension + WLC_OBJ_LOGIC_NOT, // 26: logic NOT + WLC_OBJ_LOGIC_IMPL, // 27: logic implication + WLC_OBJ_LOGIC_AND, // 28: logic AND + WLC_OBJ_LOGIC_OR, // 29: logic OR + WLC_OBJ_LOGIC_XOR, // 30: logic XOR + WLC_OBJ_COMP_EQU, // 31: compare equal + WLC_OBJ_COMP_NOTEQU, // 32: compare not equal + WLC_OBJ_COMP_LESS, // 33: compare less + WLC_OBJ_COMP_MORE, // 34: compare more + WLC_OBJ_COMP_LESSEQU, // 35: compare less or equal + WLC_OBJ_COMP_MOREEQU, // 36: compare more or equal + WLC_OBJ_REDUCT_AND, // 37: reduction AND + WLC_OBJ_REDUCT_OR, // 38: reduction OR + WLC_OBJ_REDUCT_XOR, // 39: reduction XOR + WLC_OBJ_REDUCT_NAND, // 40: reduction NAND + WLC_OBJ_REDUCT_NOR, // 41: reduction NOR + WLC_OBJ_REDUCT_NXOR, // 42: reduction NXOR + WLC_OBJ_ARI_ADD, // 43: arithmetic addition + WLC_OBJ_ARI_SUB, // 44: arithmetic subtraction + WLC_OBJ_ARI_MULTI, // 45: arithmetic multiplier + WLC_OBJ_ARI_DIVIDE, // 46: arithmetic division + WLC_OBJ_ARI_REM, // 47: arithmetic remainder + WLC_OBJ_ARI_MODULUS, // 48: arithmetic modulus + WLC_OBJ_ARI_POWER, // 49: arithmetic power + WLC_OBJ_ARI_MINUS, // 50: arithmetic minus + WLC_OBJ_ARI_SQRT, // 51: integer square root + WLC_OBJ_ARI_SQUARE, // 52: integer square + WLC_OBJ_TABLE, // 53: bit table + WLC_OBJ_NUMBER // 54: unused +} Wlc_ObjType_t; + +// printing operator types +static inline char * Ndr_OperName( int Type ) +{ + if ( Type == WLC_OBJ_NONE ) return NULL; + if ( Type == WLC_OBJ_PI ) return "pi"; // 01: primary input + if ( Type == WLC_OBJ_PO ) return "po"; // 02: primary output (unused) + if ( Type == WLC_OBJ_FO ) return "ff"; // 03: flop output + if ( Type == WLC_OBJ_FI ) return "bi"; // 04: flop input (unused) + if ( Type == WLC_OBJ_FF ) return "ff"; // 05: flop (unused) + if ( Type == WLC_OBJ_CONST ) return "const"; // 06: constant + if ( Type == WLC_OBJ_BUF ) return "buf"; // 07: buffer + if ( Type == WLC_OBJ_MUX ) return "mux"; // 08: multiplexer + if ( Type == WLC_OBJ_SHIFT_R ) return ">>"; // 09: shift right + if ( Type == WLC_OBJ_SHIFT_RA ) return ">>>"; // 10: shift right (arithmetic) + if ( Type == WLC_OBJ_SHIFT_L ) return "<<"; // 11: shift left + if ( Type == WLC_OBJ_SHIFT_LA ) return "<<<"; // 12: shift left (arithmetic) + if ( Type == WLC_OBJ_ROTATE_R ) return "rotR"; // 13: rotate right + if ( Type == WLC_OBJ_ROTATE_L ) return "rotL"; // 14: rotate left + if ( Type == WLC_OBJ_BIT_NOT ) return "~"; // 15: bitwise NOT + if ( Type == WLC_OBJ_BIT_AND ) return "&"; // 16: bitwise AND + if ( Type == WLC_OBJ_BIT_OR ) return "|"; // 17: bitwise OR + if ( Type == WLC_OBJ_BIT_XOR ) return "^"; // 18: bitwise XOR + if ( Type == WLC_OBJ_BIT_NAND ) return "~&"; // 19: bitwise NAND + if ( Type == WLC_OBJ_BIT_NOR ) return "~|"; // 20: bitwise NOR + if ( Type == WLC_OBJ_BIT_NXOR ) return "~^"; // 21: bitwise NXOR + if ( Type == WLC_OBJ_BIT_SELECT ) return "[:]"; // 22: bit selection + if ( Type == WLC_OBJ_BIT_CONCAT ) return "{}"; // 23: bit concatenation + if ( Type == WLC_OBJ_BIT_ZEROPAD ) return "zPad"; // 24: zero padding + if ( Type == WLC_OBJ_BIT_SIGNEXT ) return "sExt"; // 25: sign extension + if ( Type == WLC_OBJ_LOGIC_NOT ) return "!"; // 26: logic NOT + if ( Type == WLC_OBJ_LOGIC_IMPL ) return "=>"; // 27: logic implication + if ( Type == WLC_OBJ_LOGIC_AND ) return "&&"; // 28: logic AND + if ( Type == WLC_OBJ_LOGIC_OR ) return "||"; // 29: logic OR + if ( Type == WLC_OBJ_LOGIC_XOR ) return "^^"; // 30: logic XOR + if ( Type == WLC_OBJ_COMP_EQU ) return "=="; // 31: compare equal + if ( Type == WLC_OBJ_COMP_NOTEQU ) return "!="; // 32: compare not equal + if ( Type == WLC_OBJ_COMP_LESS ) return "<"; // 33: compare less + if ( Type == WLC_OBJ_COMP_MORE ) return ">"; // 34: compare more + if ( Type == WLC_OBJ_COMP_LESSEQU ) return "<="; // 35: compare less or equal + if ( Type == WLC_OBJ_COMP_MOREEQU ) return ">="; // 36: compare more or equal + if ( Type == WLC_OBJ_REDUCT_AND ) return "&"; // 37: reduction AND + if ( Type == WLC_OBJ_REDUCT_OR ) return "|"; // 38: reduction OR + if ( Type == WLC_OBJ_REDUCT_XOR ) return "^"; // 39: reduction XOR + if ( Type == WLC_OBJ_REDUCT_NAND ) return "~&"; // 40: reduction NAND + if ( Type == WLC_OBJ_REDUCT_NOR ) return "~|"; // 41: reduction NOR + if ( Type == WLC_OBJ_REDUCT_NXOR ) return "~^"; // 42: reduction NXOR + if ( Type == WLC_OBJ_ARI_ADD ) return "+"; // 43: arithmetic addition + if ( Type == WLC_OBJ_ARI_SUB ) return "-"; // 44: arithmetic subtraction + if ( Type == WLC_OBJ_ARI_MULTI ) return "*"; // 45: arithmetic multiplier + if ( Type == WLC_OBJ_ARI_DIVIDE ) return "/"; // 46: arithmetic division + if ( Type == WLC_OBJ_ARI_REM ) return "%"; // 47: arithmetic reminder + if ( Type == WLC_OBJ_ARI_MODULUS ) return "mod"; // 48: arithmetic modulus + if ( Type == WLC_OBJ_ARI_POWER ) return "**"; // 49: arithmetic power + if ( Type == WLC_OBJ_ARI_MINUS ) return "-"; // 50: arithmetic minus + if ( Type == WLC_OBJ_ARI_SQRT ) return "sqrt"; // 51: integer square root + if ( Type == WLC_OBJ_ARI_SQUARE ) return "squar"; // 52: integer square + if ( Type == WLC_OBJ_TABLE ) return "table"; // 53: bit table + if ( Type == WLC_OBJ_NUMBER ) return NULL; // 54: unused + return NULL; +} + + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +// this is an internal procedure, which is not seen by the user +typedef struct Ndr_Data_t_ Ndr_Data_t; +struct Ndr_Data_t_ +{ + int nSize; + int nCap; + unsigned char * pHead; + unsigned int * pBody; +}; + +static inline int Ndr_DataType( Ndr_Data_t * p, int i ) { assert( p->pHead[i] ); return (int)p->pHead[i]; } +static inline int Ndr_DataSize( Ndr_Data_t * p, int i ) { return Ndr_DataType(p, i) > NDR_OBJECT ? 1 : p->pBody[i]; } +static inline int Ndr_DataEntry( Ndr_Data_t * p, int i ) { return (int)p->pBody[i]; } +static inline int * Ndr_DataEntryP( Ndr_Data_t * p, int i ) { return (int *)p->pBody + i; } +static inline int Ndr_DataEnd( Ndr_Data_t * p, int i ) { return i + p->pBody[i]; } +static inline void Ndr_DataAddTo( Ndr_Data_t * p, int i, int Add ) { assert(Ndr_DataType(p, i) <= NDR_OBJECT); p->pBody[i] += Add; } +static inline void Ndr_DataPush( Ndr_Data_t * p, int Type, int Entry ) { p->pHead[p->nSize] = Type; p->pBody[p->nSize++] = Entry; } + +//////////////////////////////////////////////////////////////////////// +/// ITERATORS /// +//////////////////////////////////////////////////////////////////////// + +// iterates over modules in the design +#define Ndr_DesForEachMod( p, Mod ) \ + for ( Mod = 1; Mod < Ndr_DataEntry(p, 0); Mod += Ndr_DataSize(p, Mod) ) if (Ndr_DataType(p, Mod) != NDR_MODULE) {} else + +// iterates over objects in a module +#define Ndr_ModForEachObj( p, Mod, Obj ) \ + for ( Obj = Mod + 1; Obj < Ndr_DataEnd(p, Mod); Obj += Ndr_DataSize(p, Obj) ) if (Ndr_DataType(p, Obj) != NDR_OBJECT) {} else + +// iterates over records in an object +#define Ndr_ObjForEachEntry( p, Obj, Ent ) \ + for ( Ent = Obj + 1; Ent < Ndr_DataEnd(p, Obj); Ent += Ndr_DataSize(p, Ent) ) + +// iterates over primary inputs of a module +#define Ndr_ModForEachPi( p, Mod, Obj ) \ + Ndr_ModForEachObj( p, 0, Obj ) if ( !Ndr_ObjIsType(p, Obj, WLC_OBJ_PI) ) {} else + +// iteraots over primary outputs of a module +#define Ndr_ModForEachPo( p, Mod, Obj ) \ + Ndr_ModForEachObj( p, 0, Obj ) if ( !Ndr_ObjIsType(p, Obj, WLC_OBJ_PO) ) {} else + +// iterates over internal nodes of a module +#define Ndr_ModForEachNode( p, Mod, Obj ) \ + Ndr_ModForEachObj( p, 0, Obj ) if ( Ndr_ObjIsType(p, Obj, WLC_OBJ_PI) || Ndr_ObjIsType(p, Obj, WLC_OBJ_PO) ) {} else + + +//////////////////////////////////////////////////////////////////////// +/// INTERNAL PROCEDURES /// +//////////////////////////////////////////////////////////////////////// + + +static inline void Ndr_DataResize( Ndr_Data_t * p, int Add ) +{ + if ( p->nSize + Add <= p->nCap ) + return; + p->nCap *= 2; + p->pHead = (unsigned char*)realloc( p->pHead, p->nCap ); + p->pBody = (unsigned int *)realloc( p->pBody, 4*p->nCap ); +} +static inline void Ndr_DataPushRange( Ndr_Data_t * p, int RangeLeft, int RangeRight, int fSignedness ) +{ + if ( fSignedness ) + { + Ndr_DataPush( p, NDR_RANGE, RangeLeft ); + Ndr_DataPush( p, NDR_RANGE, RangeRight ); + Ndr_DataPush( p, NDR_RANGE, fSignedness ); + return; + } + if ( !RangeLeft && !RangeRight ) + return; + if ( RangeLeft == RangeRight ) + Ndr_DataPush( p, NDR_RANGE, RangeLeft ); + else + { + Ndr_DataPush( p, NDR_RANGE, RangeLeft ); + Ndr_DataPush( p, NDR_RANGE, RangeRight ); + } +} +static inline void Ndr_DataPushArray( Ndr_Data_t * p, int Type, int nArray, int * pArray ) +{ + if ( !nArray ) + return; + assert( nArray > 0 ); + Ndr_DataResize( p, nArray ); + memset( p->pHead + p->nSize, Type, nArray ); + memcpy( p->pBody + p->nSize, pArray, 4*nArray ); + p->nSize += nArray; +} +static inline void Ndr_DataPushString( Ndr_Data_t * p, int Type, char * pFunc ) +{ + if ( !pFunc ) + return; + Ndr_DataPushArray( p, Type, (strlen(pFunc) + 4) / 4, (int *)pFunc ); +} + + +//////////////////////////////////////////////////////////////////////// +/// VERILOG WRITING /// +//////////////////////////////////////////////////////////////////////// + +static inline int Ndr_ObjReadEntry( Ndr_Data_t * p, int Obj, int Type ) +{ + int Ent; + Ndr_ObjForEachEntry( p, Obj, Ent ) + if ( Ndr_DataType(p, Ent) == Type ) + return Ndr_DataEntry(p, Ent); + return -1; +} +static inline int Ndr_ObjReadArray( Ndr_Data_t * p, int Obj, int Type, int ** ppStart ) +{ + int Ent, Counter = 0; *ppStart = NULL; + Ndr_ObjForEachEntry( p, Obj, Ent ) + if ( Ndr_DataType(p, Ent) == Type ) + { + Counter++; + if ( *ppStart == NULL ) + *ppStart = (int *)p->pBody + Ent; + } + else if ( *ppStart ) + return Counter; + return Counter; +} +static inline int Ndr_ObjIsType( Ndr_Data_t * p, int Obj, int Type ) +{ + int Ent; + Ndr_ObjForEachEntry( p, Obj, Ent ) + if ( Ndr_DataType(p, Ent) == NDR_OPERTYPE ) + return (int)(Ndr_DataEntry(p, Ent) == Type); + return -1; +} +static inline int Ndr_ObjReadBody( Ndr_Data_t * p, int Obj, int Type ) +{ + int Ent; + Ndr_ObjForEachEntry( p, Obj, Ent ) + if ( Ndr_DataType(p, Ent) == Type ) + return Ndr_DataEntry(p, Ent); + return -1; +} +static inline int * Ndr_ObjReadBodyP( Ndr_Data_t * p, int Obj, int Type ) +{ + int Ent; + Ndr_ObjForEachEntry( p, Obj, Ent ) + if ( Ndr_DataType(p, Ent) == Type ) + return Ndr_DataEntryP(p, Ent); + return NULL; +} +static inline void Ndr_ObjWriteRange( Ndr_Data_t * p, int Obj, FILE * pFile ) +{ + int * pArray, nArray = Ndr_ObjReadArray( p, Obj, NDR_RANGE, &pArray ); + if ( nArray == 0 ) + return; + if ( nArray == 3 ) + fprintf( pFile, "signed " ); + if ( nArray == 1 ) + fprintf( pFile, "[%d] ", pArray[0] ); + else + fprintf( pFile, "[%d:%d] ", pArray[0], pArray[1] ); +} +static inline char * Ndr_ObjReadOutName( Ndr_Data_t * p, int Obj, char ** pNames ) +{ + return pNames[Ndr_ObjReadBody(p, Obj, NDR_OUTPUT)]; +} +static inline char * Ndr_ObjReadInName( Ndr_Data_t * p, int Obj, char ** pNames ) +{ + return pNames[Ndr_ObjReadBody(p, Obj, NDR_INPUT)]; +} + +// to write signal names, this procedure takes a mapping of name IDs into actual char-strings (pNames) +static inline void Ndr_ModuleWriteVerilog( char * pFileName, void * pModule, char ** pNames ) +{ + Ndr_Data_t * p = (Ndr_Data_t *)pModule; + int Mod = 0, Obj, nArray, * pArray, fFirst = 1; + + FILE * pFile = pFileName ? fopen( pFileName, "wb" ) : stdout; + if ( pFile == NULL ) { printf( "Cannot open file \"%s\" for writing.\n", pFileName ); return; } + + fprintf( pFile, "\nmodule %s (\n ", pNames[Ndr_ObjReadEntry(p, 0, NDR_NAME)] ); + + Ndr_ModForEachPi( p, Mod, Obj ) + fprintf( pFile, "%s, ", Ndr_ObjReadOutName(p, Obj, pNames) ); + + fprintf( pFile, "\n " ); + + Ndr_ModForEachPo( p, Mod, Obj ) + fprintf( pFile, "%s%s", fFirst ? "":", ", Ndr_ObjReadInName(p, Obj, pNames) ), fFirst = 0; + + fprintf( pFile, "\n);\n\n" ); + + Ndr_ModForEachPi( p, Mod, Obj ) + { + fprintf( pFile, " input " ); + Ndr_ObjWriteRange( p, Obj, pFile ); + fprintf( pFile, "%s;\n", Ndr_ObjReadOutName(p, Obj, pNames) ); + } + + Ndr_ModForEachPo( p, Mod, Obj ) + { + fprintf( pFile, " output " ); + Ndr_ObjWriteRange( p, Obj, pFile ); + fprintf( pFile, "%s;\n", Ndr_ObjReadInName(p, Obj, pNames) ); + } + + Ndr_ModForEachNode( p, Mod, Obj ) + { + fprintf( pFile, " wire " ); + Ndr_ObjWriteRange( p, Obj, pFile ); + fprintf( pFile, "%s;\n", Ndr_ObjReadOutName(p, Obj, pNames) ); + } + + fprintf( pFile, "\n" ); + + Ndr_ModForEachNode( p, Mod, Obj ) + { + fprintf( pFile, " assign %s = ", Ndr_ObjReadOutName(p, Obj, pNames) ); + nArray = Ndr_ObjReadArray( p, Obj, NDR_INPUT, &pArray ); + if ( nArray == 0 ) + fprintf( pFile, "%s;\n", (char *)Ndr_ObjReadBodyP(p, Obj, NDR_FUNCTION) ); + else if ( nArray == 1 && Ndr_ObjReadBody(p, Obj, NDR_OPERTYPE) == WLC_OBJ_BUF ) + fprintf( pFile, "%s;\n", pNames[pArray[0]] ); + else if ( nArray == 1 ) + fprintf( pFile, "%s %s;\n", Ndr_OperName(Ndr_ObjReadBody(p, Obj, NDR_OPERTYPE)), pNames[pArray[0]] ); + else if ( nArray == 2 ) + fprintf( pFile, "%s %s %s;\n", pNames[pArray[0]], Ndr_OperName(Ndr_ObjReadBody(p, Obj, NDR_OPERTYPE)), pNames[pArray[1]] ); + else if ( Ndr_ObjReadBody(p, Obj, NDR_OPERTYPE) == WLC_OBJ_MUX ) + fprintf( pFile, "%s ? %s : %s;\n", pNames[pArray[0]], pNames[pArray[1]], pNames[pArray[2]] ); + else + fprintf( pFile, ";\n", Ndr_OperName(Ndr_ObjReadBody(p, Obj, NDR_OPERTYPE)) ); + } + + fprintf( pFile, "\nendmodule\n\n" ); + fclose( pFile ); +} + + +//////////////////////////////////////////////////////////////////////// +/// EXTERNAL PROCEDURES /// +//////////////////////////////////////////////////////////////////////// + +// creating a new module (returns pointer to the memory buffer storing the module info) +static inline void * Ndr_ModuleCreate( int Name ) +{ + Ndr_Data_t * p = malloc( sizeof(Ndr_Data_t) ); + p->nSize = 0; + p->nCap = 16; + p->pHead = malloc( p->nCap ); + p->pBody = malloc( p->nCap * 4 ); + Ndr_DataPush( p, NDR_MODULE, 0 ); + Ndr_DataPush( p, NDR_NAME, Name ); + Ndr_DataAddTo( p, 0, p->nSize ); + assert( p->nSize == 2 ); + assert( Name ); + return p; +} + +// adding a new object (input/output/flop/intenal node) to an already module module +static inline void Ndr_ModuleAddObject( void * pModule, int Type, int InstName, + int RangeLeft, int RangeRight, int fSignedness, + int nInputs, int * pInputs, + int nOutputs, int * pOutputs, + char * pFunction ) +{ + Ndr_Data_t * p = (Ndr_Data_t *)pModule; + int Obj = p->nSize; assert( Type != 0 ); + Ndr_DataResize( p, 6 ); + Ndr_DataPush( p, NDR_OBJECT, 0 ); + Ndr_DataPush( p, NDR_OPERTYPE, Type ); + Ndr_DataPushRange( p, RangeLeft, RangeRight, fSignedness ); + if ( InstName ) + Ndr_DataPush( p, NDR_NAME, InstName ); + Ndr_DataPushArray( p, NDR_INPUT, nInputs, pInputs ); + Ndr_DataPushArray( p, NDR_OUTPUT, nOutputs, pOutputs ); + Ndr_DataPushString( p, NDR_FUNCTION, pFunction ); + Ndr_DataAddTo( p, Obj, p->nSize - Obj ); + Ndr_DataAddTo( p, 0, p->nSize - Obj ); + assert( (int)p->pBody[0] == p->nSize ); +} + +// deallocate the memory buffer +static inline void Ndr_ModuleDelete( void * pModule ) +{ + Ndr_Data_t * p = (Ndr_Data_t *)pModule; + if ( !p ) return; + free( p->pHead ); + free( p->pBody ); + free( p ); +} + + +//////////////////////////////////////////////////////////////////////// +/// FILE READING AND WRITING /// +//////////////////////////////////////////////////////////////////////// + +// file reading/writing +static inline void * Ndr_ModuleRead( char * pFileName ) +{ + Ndr_Data_t * p; int nFileSize, RetValue; + FILE * pFile = fopen( pFileName, "rb" ); + if ( pFile == NULL ) { printf( "Cannot open file \"%s\" for reading.\n", pFileName ); return NULL; } + // check file size + fseek( pFile, 0, SEEK_END ); + nFileSize = ftell( pFile ); + assert( nFileSize % 5 == 0 ); + rewind( pFile ); + // create structure + p = malloc( sizeof(Ndr_Data_t) ); + p->nSize = p->nCap = nFileSize / 5; + p->pHead = malloc( p->nCap ); + p->pBody = malloc( p->nCap * 4 ); + RetValue = fread( p->pBody, 4, p->nCap, pFile ); + RetValue = fread( p->pHead, 1, p->nCap, pFile ); + assert( p->nSize == (int)p->pBody[0] ); + fclose( pFile ); + return p; +} +static inline void Ndr_ModuleWrite( char * pFileName, void * pModule ) +{ + Ndr_Data_t * p = (Ndr_Data_t *)pModule; int RetValue; + FILE * pFile = fopen( pFileName, "wb" ); + if ( pFile == NULL ) { printf( "Cannot open file \"%s\" for writing.\n", pFileName ); return; } + RetValue = fwrite( p->pBody, 4, p->pBody[0], pFile ); + RetValue = fwrite( p->pHead, 1, p->pBody[0], pFile ); + fclose( pFile ); +} + + +//////////////////////////////////////////////////////////////////////// +/// TESTING PROCEDURE /// +//////////////////////////////////////////////////////////////////////// + +// This testing procedure creates and writes into a Verilog file the following module + +// module add10 ( input [3:0] a, output [3:0] s ); +// wire [3:0] const10 = 4'b1010; +// assign s = a + const10; +// endmodule + +static inline void Ndr_ModuleTest() +{ + // name IDs + int NameIdA = 2; + int NameIdS = 3; + int NameIdC = 4; + // array of fanins of node s + int Fanins[2] = { NameIdA, NameIdC }; + // map name IDs into char strings + char * ppNames[5] = { NULL, "add10", "a", "s", "const10" }; + + // create a new module + void * pModule = Ndr_ModuleCreate( 1 ); + + // add objects to the modele + Ndr_ModuleAddObject( pModule, WLC_OBJ_PI, 0, 3, 0, 0, 0, NULL, 1, &NameIdA, NULL ); // no fanins + Ndr_ModuleAddObject( pModule, WLC_OBJ_CONST, 0, 3, 0, 0, 0, NULL, 1, &NameIdC, "4'b1010" ); // no fanins + Ndr_ModuleAddObject( pModule, WLC_OBJ_ARI_ADD, 0, 3, 0, 0, 2, Fanins, 1, &NameIdS, NULL ); // fanins are a and const10 + Ndr_ModuleAddObject( pModule, WLC_OBJ_PO, 0, 3, 0, 0, 1, &NameIdS, 0, NULL, NULL ); // fanin is a + + // write Verilog for verification + Ndr_ModuleWriteVerilog( NULL, pModule, ppNames ); + Ndr_ModuleDelete( pModule ); +} + + +//ABC_NAMESPACE_HEADER_END + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + -- 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/aig/gia/giaGlitch.c | 19 ++++++----- src/base/abc/abc.h | 1 + src/base/abci/abc.c | 84 ++++++++++++++++++++++++++++++++++++++++++++++++ src/base/abci/abcPrint.c | 79 ++++++++++++++++++++++++++++++++++++++++++--- 4 files changed, 168 insertions(+), 15 deletions(-) diff --git a/src/aig/gia/giaGlitch.c b/src/aig/gia/giaGlitch.c index cc69f6b3..8c0cc161 100644 --- a/src/aig/gia/giaGlitch.c +++ b/src/aig/gia/giaGlitch.c @@ -37,7 +37,7 @@ struct Gli_Obj_t_ unsigned nFanins : 3; // the number of fanins unsigned nFanouts : 25; // total number of fanouts unsigned Handle; // ID of the node - unsigned uTruth[2]; // truth table of the node + word * pTruth; // truth table of the node unsigned uSimInfo; // simulation info of the node union { @@ -333,7 +333,7 @@ static inline int Gli_NodeComputeValue( Gli_Obj_t * pNode ) int i, Phase = 0; for ( i = 0; i < (int)pNode->nFanins; i++ ) Phase |= (Gli_ObjFanin(pNode, i)->fPhase << i); - return Abc_InfoHasBit( pNode->uTruth, Phase ); + return Abc_InfoHasBit( (unsigned *)pNode->pTruth, Phase ); } /**Function************************************************************* @@ -352,7 +352,7 @@ static inline int Gli_NodeComputeValue2( Gli_Obj_t * pNode ) int i, Phase = 0; for ( i = 0; i < (int)pNode->nFanins; i++ ) Phase |= (Gli_ObjFanin(pNode, i)->fPhase2 << i); - return Abc_InfoHasBit( pNode->uTruth, Phase ); + return Abc_InfoHasBit( (unsigned *)pNode->pTruth, Phase ); } /**Function************************************************************* @@ -366,16 +366,15 @@ static inline int Gli_NodeComputeValue2( Gli_Obj_t * pNode ) SeeAlso [] ***********************************************************************/ -int Gli_ManCreateNode( Gli_Man_t * p, Vec_Int_t * vFanins, int nFanouts, unsigned * puTruth ) +int Gli_ManCreateNode( Gli_Man_t * p, Vec_Int_t * vFanins, int nFanouts, word * pGateTruth ) { Gli_Obj_t * pObj, * pFanin; int i; - assert( Vec_IntSize(vFanins) <= 6 ); + assert( Vec_IntSize(vFanins) <= 16 ); pObj = Gli_ObjAlloc( p, Vec_IntSize(vFanins), nFanouts ); Gli_ManForEachEntry( vFanins, p, pFanin, i ) Gli_ObjAddFanin( pObj, pFanin ); - pObj->uTruth[0] = puTruth[0]; - pObj->uTruth[1] = puTruth[Vec_IntSize(vFanins) == 6]; + pObj->pTruth = pGateTruth; pObj->fPhase = pObj->fPhase2 = Gli_NodeComputeValue( pObj ); return pObj->Handle; } @@ -584,7 +583,7 @@ unsigned Gli_ManSimulateSeqNode( Gli_Man_t * p, Gli_Obj_t * pNode ) int nFanins = Gli_ObjFaninNum(pNode); int i, k, Phase; Gli_Obj_t * pFanin; - assert( nFanins <= 6 ); + assert( nFanins <= 16 ); Gli_ObjForEachFanin( pNode, pFanin, i ) pSimInfos[i] = pFanin->uSimInfo; for ( i = 0; i < 32; i++ ) @@ -593,7 +592,7 @@ unsigned Gli_ManSimulateSeqNode( Gli_Man_t * p, Gli_Obj_t * pNode ) for ( k = 0; k < nFanins; k++ ) if ( (pSimInfos[k] >> i) & 1 ) Phase |= (1 << k); - if ( Abc_InfoHasBit( pNode->uTruth, Phase ) ) + if ( Abc_InfoHasBit( (unsigned *)pNode->pTruth, Phase ) ) Result |= (1 << i); } return Result; @@ -772,7 +771,7 @@ void Gli_ManSwitchesAndGlitches( Gli_Man_t * p, int nPatterns, float PiTransProb } if ( fVerbose ) { - printf( "\nSimulated %d patterns. ", nPatterns ); + printf( "Simulated %d patterns. Input transition probability %.2f. ", nPatterns, PiTransProb ); ABC_PRMn( "Memory", 4*p->nObjData ); ABC_PRT( "Time", Abc_Clock() - clk ); } 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. --- abclib.dsp | 4 ++++ src/base/abci/abc.c | 46 +++++++++++++++++++++++++++++++++++++ src/base/abci/abcEco.c | 58 +++++++++++++++++++++++++++++++++++++++++++++++ src/base/abci/module.make | 1 + 4 files changed, 109 insertions(+) create mode 100644 src/base/abci/abcEco.c diff --git a/abclib.dsp b/abclib.dsp index b852551d..6df9c79d 100644 --- a/abclib.dsp +++ b/abclib.dsp @@ -271,6 +271,10 @@ SOURCE=.\src\base\abci\abcDsd.c # End Source File # Begin Source File +SOURCE=.\src\base\abci\abcEco.c +# End Source File +# Begin Source File + SOURCE=.\src\base\abci\abcExact.c # End Source File # Begin Source File 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(-) 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/aig/miniaig/abcapis.h | 84 ------------------------------------ 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 +- 7 files changed, 199 insertions(+), 99 deletions(-) delete mode 100644 src/aig/miniaig/abcapis.h create mode 100644 src/base/main/abcapis.h create mode 100644 src/base/main/abcapis_old.h diff --git a/src/aig/miniaig/abcapis.h b/src/aig/miniaig/abcapis.h deleted file mode 100644 index eb8586fe..00000000 --- a/src/aig/miniaig/abcapis.h +++ /dev/null @@ -1,84 +0,0 @@ -/**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 /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// 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/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 From b1907e909d92d1147937b26b5e97fb344647f719 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 2 Mar 2017 20:56:16 -0800 Subject: Moving global declarations into 'abcapi.h' and moving it into 'main' package. --- abclib.dsp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/abclib.dsp b/abclib.dsp index 6df9c79d..407c3c66 100644 --- a/abclib.dsp +++ b/abclib.dsp @@ -699,6 +699,10 @@ SOURCE=.\src\base\io\ioWriteVerilog.c # PROP Default_Filter "" # Begin Source File +SOURCE=.\src\base\main\abcapis.h +# End Source File +# Begin Source File + SOURCE=.\src\base\main\libSupport.c # End Source File # Begin Source File -- cgit v1.2.3