diff options
Diffstat (limited to 'src/aig/cec')
-rw-r--r-- | src/aig/cec/cec.c | 5 | ||||
-rw-r--r-- | src/aig/cec/cec.h | 50 | ||||
-rw-r--r-- | src/aig/cec/cecCec.c | 124 | ||||
-rw-r--r-- | src/aig/cec/cecChoice.c | 106 | ||||
-rw-r--r-- | src/aig/cec/cecClass.c | 48 | ||||
-rw-r--r-- | src/aig/cec/cecCore.c | 73 | ||||
-rw-r--r-- | src/aig/cec/cecCorr.c | 114 | ||||
-rw-r--r-- | src/aig/cec/cecCorr_updated.c | 7 | ||||
-rw-r--r-- | src/aig/cec/cecInt.h | 26 | ||||
-rw-r--r-- | src/aig/cec/cecIso.c | 11 | ||||
-rw-r--r-- | src/aig/cec/cecMan.c | 45 | ||||
-rw-r--r-- | src/aig/cec/cecPat.c | 19 | ||||
-rw-r--r-- | src/aig/cec/cecSeq.c | 71 | ||||
-rw-r--r-- | src/aig/cec/cecSim.c | 5 | ||||
-rw-r--r-- | src/aig/cec/cecSolve.c | 75 | ||||
-rw-r--r-- | src/aig/cec/cecSweep.c | 11 | ||||
-rw-r--r-- | src/aig/cec/cecSynth.c | 380 | ||||
-rw-r--r-- | src/aig/cec/module.make | 1 |
18 files changed, 838 insertions, 333 deletions
diff --git a/src/aig/cec/cec.c b/src/aig/cec/cec.c index 17b27ec5..6968a599 100644 --- a/src/aig/cec/cec.c +++ b/src/aig/cec/cec.c @@ -20,6 +20,9 @@ #include "cecInt.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -46,3 +49,5 @@ //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/cec/cec.h b/src/aig/cec/cec.h index 199d6939..e4547f5e 100644 --- a/src/aig/cec/cec.h +++ b/src/aig/cec/cec.h @@ -21,6 +21,7 @@ #ifndef __CEC_H__ #define __CEC_H__ + //////////////////////////////////////////////////////////////////////// /// INCLUDES /// //////////////////////////////////////////////////////////////////////// @@ -29,9 +30,10 @@ /// PARAMETERS /// //////////////////////////////////////////////////////////////////////// -#ifdef __cplusplus -extern "C" { -#endif + + +ABC_NAMESPACE_HEADER_START + //////////////////////////////////////////////////////////////////////// /// BASIC TYPES /// @@ -103,8 +105,10 @@ struct Cec_ParFra_t_ // int fFirstStop; // stop on the first sat output int fDualOut; // miter with separate outputs int fColorDiff; // miter with separate outputs + int fSatSweeping; // enable SAT sweeping int fVeryVerbose; // verbose stats int fVerbose; // verbose stats + int iOutFail; // the failed output }; // combinational equivalence checking parameters @@ -118,6 +122,7 @@ struct Cec_ParCec_t_ int fRewriting; // enables AIG rewriting int fVeryVerbose; // verbose stats int fVerbose; // verbose stats + int iOutFail; // the number of failed output }; // sequential register correspodence parameters @@ -129,6 +134,8 @@ struct Cec_ParCor_t_ int nFrames; // the number of time frames int nPrefix; // the number of time frames in the prefix int nBTLimit; // conflict limit at a node + int nLevelMax; // (scorr only) the max number of levels + int nStepsMax; // (scorr only) the max number of induction steps int fLatchCorr; // consider only latch outputs int fUseRings; // use rings int fMakeChoices; // use equilvaences as choices @@ -138,6 +145,9 @@ struct Cec_ParCor_t_ int fVerboseFlops; // verbose stats int fVeryVerbose; // verbose stats int fVerbose; // verbose stats + // callback + void * pData; + void * pFunc; }; // sequential register correspodence parameters @@ -153,6 +163,23 @@ struct Cec_ParChc_t_ int fVerbose; // verbose stats }; +// sequential synthesis parameters +typedef struct Cec_ParSeq_t_ Cec_ParSeq_t; +struct Cec_ParSeq_t_ +{ + int fUseLcorr; // enables latch correspondence + int fUseScorr; // enables signal correspondence + int nBTLimit; // (scorr/lcorr) conflict limit at a node + int nFrames; // (scorr/lcorr) the number of timeframes + int nLevelMax; // (scorr only) the max number of levels + int fConsts; // (scl only) merging constants + int fEquivs; // (scl only) merging equivalences + int fUseMiniSat; // enables MiniSat in lcorr/scorr + int nMinDomSize; // the size of minimum clock domain + int fVeryVerbose; // verbose stats + int fVerbose; // verbose stats +}; + //////////////////////////////////////////////////////////////////////// /// MACRO DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -167,6 +194,7 @@ extern int Cec_ManVerifyTwo( Gia_Man_t * p0, Gia_Man_t * p1, int fVerb /*=== cecChoice.c ==========================================================*/ extern Gia_Man_t * Cec_ManChoiceComputation( Gia_Man_t * pAig, Cec_ParChc_t * pPars ); /*=== cecCorr.c ==========================================================*/ +extern int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars ); extern Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars ); /*=== cecCore.c ==========================================================*/ extern void Cec_ManSatSetDefaultParams( Cec_ParSat_t * p ); @@ -180,12 +208,20 @@ extern Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars extern Gia_Man_t * Cec_ManSatSolving( Gia_Man_t * pAig, Cec_ParSat_t * pPars ); extern void Cec_ManSimulation( Gia_Man_t * pAig, Cec_ParSim_t * pPars ); /*=== cecSeq.c ==========================================================*/ -extern int Cec_ManSeqResimulateCounter( Gia_Man_t * pAig, Cec_ParSim_t * pPars, Gia_Cex_t * pCex ); +extern int Cec_ManSeqResimulateCounter( Gia_Man_t * pAig, Cec_ParSim_t * pPars, Abc_Cex_t * pCex ); extern int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars ); +extern int Cec_ManCheckNonTrivialCands( Gia_Man_t * pAig ); +/*=== cecSynth.c ==========================================================*/ +extern int Cec_SeqReadMinDomSize( Cec_ParSeq_t * p ); +extern int Cec_SeqReadVerbose( Cec_ParSeq_t * p ); +extern void Cec_SeqSynthesisSetDefaultParams( Cec_ParSeq_t * pPars ); +extern int Cec_SequentialSynthesisPart( Gia_Man_t * p, Cec_ParSeq_t * pPars ); + + + +ABC_NAMESPACE_HEADER_END + -#ifdef __cplusplus -} -#endif #endif diff --git a/src/aig/cec/cecCec.c b/src/aig/cec/cecCec.c index 1efa9235..0859a9ad 100644 --- a/src/aig/cec/cecCec.c +++ b/src/aig/cec/cecCec.c @@ -19,8 +19,12 @@ ***********************************************************************/ #include "cecInt.h" +#include "fra.h" #include "giaAig.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -44,8 +48,8 @@ void Cec_ManTransformPattern( Gia_Man_t * p, int iOut, int * pValues ) { int i; assert( p->pCexComb == NULL ); - p->pCexComb = (Gia_Cex_t *)ABC_CALLOC( char, - sizeof(Gia_Cex_t) + sizeof(unsigned) * Gia_BitWordNum(Gia_ManCiNum(p)) ); + p->pCexComb = (Abc_Cex_t *)ABC_CALLOC( char, + sizeof(Abc_Cex_t) + sizeof(unsigned) * Gia_BitWordNum(Gia_ManCiNum(p)) ); p->pCexComb->iPo = iOut; p->pCexComb->nPis = Gia_ManCiNum(p); p->pCexComb->nBits = Gia_ManCiNum(p); @@ -65,45 +69,53 @@ void Cec_ManTransformPattern( Gia_Man_t * p, int iOut, int * pValues ) SeeAlso [] ***********************************************************************/ -int Cec_ManVerifyOld( Gia_Man_t * pMiter, int fVerbose ) +int Cec_ManVerifyOld( Gia_Man_t * pMiter, int fVerbose, int * piOutFail ) { - extern int Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose ); +// extern int Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose ); extern int Ssw_SecCexResimulate( Aig_Man_t * p, int * pModel, int * pnOutputs ); Gia_Man_t * pTemp = Gia_ManTransformMiter( pMiter ); Aig_Man_t * pMiterCec = Gia_ManToAig( pTemp, 0 ); int RetValue, iOut, nOuts, clkTotal = clock(); + if ( piOutFail ) + *piOutFail = -1; Gia_ManStop( pTemp ); // run CEC on this miter - RetValue = Fra_FraigCec( &pMiterCec, 100000, fVerbose ); + RetValue = Fra_FraigCec( &pMiterCec, 10000000, fVerbose ); // report the miter if ( RetValue == 1 ) { - printf( "Networks are equivalent. " ); -ABC_PRT( "Time", clock() - clkTotal ); + Abc_Print( 1, "Networks are equivalent. " ); +Abc_PrintTime( 1, "Time", clock() - clkTotal ); } else if ( RetValue == 0 ) { - printf( "Networks are NOT EQUIVALENT. " ); -ABC_PRT( "Time", clock() - clkTotal ); + Abc_Print( 1, "Networks are NOT EQUIVALENT. " ); +Abc_PrintTime( 1, "Time", clock() - clkTotal ); if ( pMiterCec->pData == NULL ) - printf( "Counter-example is not available.\n" ); + Abc_Print( 1, "Counter-example is not available.\n" ); else { - iOut = Ssw_SecCexResimulate( pMiterCec, pMiterCec->pData, &nOuts ); + iOut = Ssw_SecCexResimulate( pMiterCec, (int *)pMiterCec->pData, &nOuts ); if ( iOut == -1 ) - printf( "Counter-example verification has failed.\n" ); + Abc_Print( 1, "Counter-example verification has failed.\n" ); else { - printf( "Primary output %d has failed in frame %d.\n", iOut ); - printf( "The counter-example detected %d incorrect outputs.\n", nOuts ); +// Aig_Obj_t * pObj = Aig_ManPo(pMiterCec, iOut); +// Aig_Obj_t * pFan = Aig_ObjFanin0(pObj); + Abc_Print( 1, "Primary output %d has failed", iOut ); + if ( nOuts-1 >= 0 ) + Abc_Print( 1, ", along with other %d incorrect outputs", nOuts-1 ); + Abc_Print( 1, ".\n" ); + if ( piOutFail ) + *piOutFail = iOut; } - Cec_ManTransformPattern( pMiter, iOut, pMiterCec->pData ); + Cec_ManTransformPattern( pMiter, iOut, (int *)pMiterCec->pData ); } } else { - printf( "Networks are UNDECIDED. " ); -ABC_PRT( "Time", clock() - clkTotal ); + Abc_Print( 1, "Networks are UNDECIDED. " ); +Abc_PrintTime( 1, "Time", clock() - clkTotal ); } fflush( stdout ); Aig_ManStop( pMiterCec ); @@ -121,13 +133,18 @@ ABC_PRT( "Time", clock() - clkTotal ); SeeAlso [] ***********************************************************************/ -int Cec_ManVerify( Gia_Man_t * p, Cec_ParCec_t * pPars ) +int Cec_ManVerify( Gia_Man_t * pInit, Cec_ParCec_t * pPars ) { - int fDumpUndecided = 1; + int fDumpUndecided = 0; Cec_ParFra_t ParsFra, * pParsFra = &ParsFra; - Gia_Man_t * pNew; + Gia_Man_t * p, * pNew; int RetValue, clk = clock(); double clkTotal = clock(); + // preprocess + p = Gia_ManDup( pInit ); + Gia_ManEquivFixOutputPairs( p ); + p = Gia_ManCleanup( pNew = p ); + Gia_ManStop( pNew ); // sweep for equivalences Cec_ManFraSetDefaultParams( pParsFra ); pParsFra->nItersMax = 1000; @@ -137,27 +154,60 @@ int Cec_ManVerify( Gia_Man_t * p, Cec_ParCec_t * pPars ) pParsFra->fCheckMiter = 1; pParsFra->fDualOut = 1; pNew = Cec_ManSatSweeping( p, pParsFra ); + pPars->iOutFail = pParsFra->iOutFail; + // update + pInit->pCexComb = p->pCexComb; p->pCexComb = NULL; + Gia_ManStop( p ); + p = pInit; + // continue if ( pNew == NULL ) { - if ( !Gia_ManVerifyCounterExample( p, p->pCexComb, 1 ) ) - printf( "Counter-example simulation has failed.\n" ); - printf( "Networks are NOT EQUIVALENT. " ); - ABC_PRT( "Time", clock() - clk ); - return 0; + if ( p->pCexComb != NULL ) + { + if ( p->pCexComb && !Gia_ManVerifyCounterExample( p, p->pCexComb, 1 ) ) + Abc_Print( 1, "Counter-example simulation has failed.\n" ); + Abc_Print( 1, "Networks are NOT EQUIVALENT. " ); + Abc_PrintTime( 1, "Time", clock() - clk ); + return 0; + } + p = Gia_ManDup( pInit ); + Gia_ManEquivFixOutputPairs( p ); + p = Gia_ManCleanup( pNew = p ); + Gia_ManStop( pNew ); + pNew = p; } if ( Gia_ManAndNum(pNew) == 0 ) { - printf( "Networks are equivalent. " ); - ABC_PRT( "Time", clock() - clk ); + Gia_Obj_t * pObj1, * pObj2; + int i; + Gia_ManForEachPo( pNew, pObj1, i ) + { + pObj2 = Gia_ManPo( pNew, ++i ); + if ( Gia_ObjChild0(pObj1) != Gia_ObjChild0(pObj2) ) + { + Abc_Print( 1, "Networks are NOT EQUIVALENT. Outputs %d trivially differ. ", i/2 ); + Abc_PrintTime( 1, "Time", clock() - clk ); + Gia_ManStop( pNew ); + pPars->iOutFail = i/2; + return 0; + } + } + Abc_Print( 1, "Networks are equivalent. " ); + Abc_PrintTime( 1, "Time", clock() - clk ); Gia_ManStop( pNew ); return 1; } - printf( "Networks are UNDECIDED after the new CEC engine. " ); - ABC_PRT( "Time", clock() - clk ); + if ( pPars->fVerbose ) + { + Abc_Print( 1, "Networks are UNDECIDED after the new CEC engine. " ); + Abc_PrintTime( 1, "Time", clock() - clk ); + } if ( fDumpUndecided ) { + ABC_FREE( pNew->pReprs ); + ABC_FREE( pNew->pNexts ); Gia_WriteAiger( pNew, "gia_cec_undecided.aig", 0, 0 ); - printf( "The result is written into file \"%s\".\n", "gia_cec_undecided.aig" ); + Abc_Print( 1, "The result is written into file \"%s\".\n", "gia_cec_undecided.aig" ); } if ( pPars->TimeLimit && ((double)clock() - clkTotal)/CLOCKS_PER_SEC >= pPars->TimeLimit ) { @@ -165,12 +215,13 @@ int Cec_ManVerify( Gia_Man_t * p, Cec_ParCec_t * pPars ) return -1; } // call other solver - printf( "Calling the old CEC engine.\n" ); + if ( pPars->fVerbose ) + Abc_Print( 1, "Calling the old CEC engine.\n" ); fflush( stdout ); - RetValue = Cec_ManVerifyOld( pNew, pPars->fVerbose ); + RetValue = Cec_ManVerifyOld( pNew, pPars->fVerbose, &pPars->iOutFail ); p->pCexComb = pNew->pCexComb; pNew->pCexComb = NULL; if ( p->pCexComb && !Gia_ManVerifyCounterExample( p, p->pCexComb, 1 ) ) - printf( "Counter-example simulation has failed.\n" ); + Abc_Print( 1, "Counter-example simulation has failed.\n" ); Gia_ManStop( pNew ); return RetValue; } @@ -208,7 +259,7 @@ int Cec_ManVerifyTwo( Gia_Man_t * p0, Gia_Man_t * p1, int fVerbose ) Description [Returns 1 if equivalent, 0 if counter-example, -1 if undecided. Counter-example is returned in the first manager as pAig0->pSeqModel. - The format is given in Gia_Cex_t (file "abc\src\aig\gia\gia.h").] + The format is given in Abc_Cex_t (file "abc\src\aig\gia\gia.h").] SideEffects [] @@ -248,7 +299,6 @@ int Cec_ManVerifyTwoAigs( Aig_Man_t * pAig0, Aig_Man_t * pAig1, int fVerbose ) ***********************************************************************/ Aig_Man_t * Cec_LatchCorrespondence( Aig_Man_t * pAig, int nConfs, int fUseCSat ) { - extern int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars ); Gia_Man_t * pGia; Cec_ParCor_t CorPars, * pCorPars = &CorPars; Cec_ManCorSetDefaultParams( pCorPars ); @@ -275,7 +325,6 @@ Aig_Man_t * Cec_LatchCorrespondence( Aig_Man_t * pAig, int nConfs, int fUseCSat ***********************************************************************/ Aig_Man_t * Cec_SignalCorrespondence( Aig_Man_t * pAig, int nConfs, int fUseCSat ) { - extern int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars ); Gia_Man_t * pGia; Cec_ParCor_t CorPars, * pCorPars = &CorPars; Cec_ManCorSetDefaultParams( pCorPars ); @@ -304,6 +353,7 @@ Aig_Man_t * Cec_FraigCombinational( Aig_Man_t * pAig, int nConfs, int fVerbose ) Gia_Man_t * pGia; Cec_ParFra_t FraPars, * pFraPars = &FraPars; Cec_ManFraSetDefaultParams( pFraPars ); + pFraPars->fSatSweeping = 1; pFraPars->nBTLimit = nConfs; pFraPars->nItersMax = 20; pFraPars->fVerbose = fVerbose; @@ -319,3 +369,5 @@ Aig_Man_t * Cec_FraigCombinational( Aig_Man_t * pAig, int nConfs, int fVerbose ) //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/cec/cecChoice.c b/src/aig/cec/cecChoice.c index fc316f46..076b34a2 100644 --- a/src/aig/cec/cecChoice.c +++ b/src/aig/cec/cecChoice.c @@ -22,6 +22,9 @@ #include "giaAig.h" #include "dch.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -175,9 +178,9 @@ Gia_Man_t * Cec_ManCombSpecReduce( Gia_Man_t * p, Vec_Int_t ** pvOutputs, int fR Gia_ManAppendCo( pNew, iObjNew ); Vec_IntFree( vXorLits ); Gia_ManHashStop( pNew ); -//printf( "Before sweeping = %d\n", Gia_ManAndNum(pNew) ); +//Abc_Print( 1, "Before sweeping = %d\n", Gia_ManAndNum(pNew) ); pNew = Gia_ManCleanup( pTemp = pNew ); -//printf( "After sweeping = %d\n", Gia_ManAndNum(pNew) ); +//Abc_Print( 1, "After sweeping = %d\n", Gia_ManAndNum(pNew) ); Gia_ManStop( pTemp ); return pNew; } @@ -219,7 +222,7 @@ int Cec_ManChoiceComputation_int( Gia_Man_t * pAig, Cec_ParChc_t * pPars ) pParsSim->fSeqSimulate = 0; // create equivalence classes of registers pSim = Cec_ManSimStart( pAig, pParsSim ); - Cec_ManSimClassesPrepare( pSim ); + Cec_ManSimClassesPrepare( pSim, -1 ); Cec_ManSimClassesRefine( pSim ); // prepare SAT solving Cec_ManSatSetDefaultParams( pParsSat ); @@ -227,7 +230,7 @@ int Cec_ManChoiceComputation_int( Gia_Man_t * pAig, Cec_ParChc_t * pPars ) pParsSat->fVerbose = pPars->fVerbose; if ( pPars->fVerbose ) { - printf( "Obj = %7d. And = %7d. Conf = %5d. Ring = %d. CSat = %d.\n", + Abc_Print( 1, "Obj = %7d. And = %7d. Conf = %5d. Ring = %d. CSat = %d.\n", Gia_ManObjNum(pAig), Gia_ManAndNum(pAig), pPars->nBTLimit, pPars->fUseRings, pPars->fUseCSat ); Cec_ManRefinedClassPrintStats( pAig, NULL, 0, clock() - clk ); } @@ -280,97 +283,23 @@ int Cec_ManChoiceComputation_int( Gia_Man_t * pAig, Cec_ParChc_t * pPars ) } // check the overflow if ( r == nItersMax ) - printf( "The refinement was not finished. The result may be incorrect.\n" ); + Abc_Print( 1, "The refinement was not finished. The result may be incorrect.\n" ); Cec_ManSimStop( pSim ); clkTotal = clock() - clkTotal; // report the results if ( pPars->fVerbose ) { - ABC_PRTP( "Srm ", clkSrm, clkTotal ); - ABC_PRTP( "Sat ", clkSat, clkTotal ); - ABC_PRTP( "Sim ", clkSim, clkTotal ); - ABC_PRTP( "Other", clkTotal-clkSat-clkSrm-clkSim, clkTotal ); - ABC_PRT( "TOTAL", clkTotal ); + Abc_PrintTimeP( 1, "Srm ", clkSrm, clkTotal ); + Abc_PrintTimeP( 1, "Sat ", clkSat, clkTotal ); + Abc_PrintTimeP( 1, "Sim ", clkSim, clkTotal ); + Abc_PrintTimeP( 1, "Other", clkTotal-clkSat-clkSrm-clkSim, clkTotal ); + Abc_PrintTime( 1, "TOTAL", clkTotal ); } return 0; } /**Function************************************************************* - Synopsis [Duplicates the AIG in the DFS order.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Gia_ManChoiceMiter_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj ) -{ - if ( ~pObj->Value ) - return pObj->Value; - Gia_ManChoiceMiter_rec( pNew, p, Gia_ObjFanin0(pObj) ); - if ( Gia_ObjIsCo(pObj) ) - return pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); - Gia_ManChoiceMiter_rec( pNew, p, Gia_ObjFanin1(pObj) ); - return pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); -} - -/**Function************************************************************* - - Synopsis [Derives the miter of several AIGs for choice computation.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Gia_Man_t * Gia_ManChoiceMiter( Vec_Ptr_t * vGias ) -{ - Gia_Man_t * pNew, * pGia, * pGia0; - int i, k, iNode, nNodes; - // make sure they have equal parameters - assert( Vec_PtrSize(vGias) > 0 ); - pGia0 = Vec_PtrEntry( vGias, 0 ); - Vec_PtrForEachEntry( vGias, pGia, i ) - { - assert( Gia_ManCiNum(pGia) == Gia_ManCiNum(pGia0) ); - assert( Gia_ManCoNum(pGia) == Gia_ManCoNum(pGia0) ); - assert( Gia_ManRegNum(pGia) == Gia_ManRegNum(pGia0) ); - Gia_ManFillValue( pGia ); - Gia_ManConst0(pGia)->Value = 0; - } - // start the new manager - pNew = Gia_ManStart( Vec_PtrSize(vGias) * Gia_ManObjNum(pGia0) ); - pNew->pName = Gia_UtilStrsav( pGia0->pName ); - // create new CIs and assign them to the old manager CIs - for ( k = 0; k < Gia_ManCiNum(pGia0); k++ ) - { - iNode = Gia_ManAppendCi(pNew); - Vec_PtrForEachEntry( vGias, pGia, i ) - Gia_ManCi( pGia, k )->Value = iNode; - } - // create internal nodes - Gia_ManHashAlloc( pNew ); - for ( k = 0; k < Gia_ManCoNum(pGia0); k++ ) - { - Vec_PtrForEachEntry( vGias, pGia, i ) - Gia_ManChoiceMiter_rec( pNew, pGia, Gia_ManCo( pGia, k ) ); - } - Gia_ManHashStop( pNew ); - // check the presence of dangling nodes - nNodes = Gia_ManHasDandling( pNew ); - assert( nNodes == 0 ); - // finalize -// Gia_ManSetRegNum( pNew, Gia_ManRegNum(pGia0) ); - return pNew; -} - -/**Function************************************************************* - Synopsis [Computes choices for the vector of AIGs.] Description [] @@ -386,6 +315,7 @@ Gia_Man_t * Cec_ManChoiceComputationVec( Gia_Man_t * pGia, int nGias, Cec_ParChc int RetValue; // compute equivalences of the miter // pMiter = Gia_ManChoiceMiter( vGias ); +// Gia_ManSetRegNum( pMiter, 0 ); RetValue = Cec_ManChoiceComputation_int( pGia, pPars ); // derive AIG with choices pNew = Gia_ManEquivToChoices( pGia, nGias ); @@ -394,7 +324,7 @@ Gia_Man_t * Cec_ManChoiceComputationVec( Gia_Man_t * pGia, int nGias, Cec_ParChc // report the results if ( pPars->fVerbose ) { -// printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n", +// Abc_Print( 1, "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n", // Gia_ManAndNum(pAig), Gia_ManAndNum(pNew), // 100.0*(Gia_ManAndNum(pAig)-Gia_ManAndNum(pNew))/(Gia_ManAndNum(pAig)?Gia_ManAndNum(pAig):1), // Gia_ManRegNum(pAig), Gia_ManRegNum(pNew), @@ -416,7 +346,7 @@ Gia_Man_t * Cec_ManChoiceComputationVec( Gia_Man_t * pGia, int nGias, Cec_ParChc ***********************************************************************/ Gia_Man_t * Cec_ManChoiceComputation( Gia_Man_t * pAig, Cec_ParChc_t * pParsChc ) { - extern Aig_Man_t * Dar_ManChoiceNew( Aig_Man_t * pAig, Dch_Pars_t * pPars ); +// extern Aig_Man_t * Dar_ManChoiceNew( Aig_Man_t * pAig, Dch_Pars_t * pPars ); Dch_Pars_t Pars, * pPars = &Pars; Aig_Man_t * pMan, * pManNew; Gia_Man_t * pGia; @@ -456,7 +386,7 @@ Aig_Man_t * Cec_ComputeChoices( Gia_Man_t * pGia, Dch_Pars_t * pPars ) Cec_ParChc_t ParsChc, * pParsChc = &ParsChc; Aig_Man_t * pAig; if ( pPars->fVerbose ) - ABC_PRT( "Synthesis time", pPars->timeSynth ); + Abc_PrintTime( 1, "Synthesis time", pPars->timeSynth ); Cec_ManChcSetDefaultParams( pParsChc ); pParsChc->nBTLimit = pPars->nBTLimit; pParsChc->fUseCSat = pPars->fUseCSat; @@ -475,3 +405,5 @@ Aig_Man_t * Cec_ComputeChoices( Gia_Man_t * pGia, Dch_Pars_t * pPars ) //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/cec/cecClass.c b/src/aig/cec/cecClass.c index 749f7f71..95414851 100644 --- a/src/aig/cec/cecClass.c +++ b/src/aig/cec/cecClass.c @@ -20,6 +20,9 @@ #include "cecInt.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -375,7 +378,7 @@ int Cec_ManSimHashKey( unsigned * pSim, int nWords, int nTableSize ) void Cec_ManSimMemRelink( Cec_ManSim_t * p ) { unsigned * pPlace, Ent; - pPlace = &p->MemFree; + pPlace = (unsigned *)&p->MemFree; for ( Ent = p->nMems * (p->nWords + 1); Ent + p->nWords + 1 < (unsigned)p->nWordsAlloc; Ent += p->nWords + 1 ) @@ -518,14 +521,14 @@ void Cec_ManSimSavePattern( Cec_ManSim_t * p, int iPat ) int i; assert( p->pCexComb == NULL ); assert( iPat >= 0 && iPat < 32 * p->nWords ); - p->pCexComb = (Gia_Cex_t *)ABC_CALLOC( char, - sizeof(Gia_Cex_t) + sizeof(unsigned) * Gia_BitWordNum(Gia_ManCiNum(p->pAig)) ); + p->pCexComb = (Abc_Cex_t *)ABC_CALLOC( char, + sizeof(Abc_Cex_t) + sizeof(unsigned) * Gia_BitWordNum(Gia_ManCiNum(p->pAig)) ); p->pCexComb->iPo = p->iOut; p->pCexComb->nPis = Gia_ManCiNum(p->pAig); p->pCexComb->nBits = Gia_ManCiNum(p->pAig); for ( i = 0; i < Gia_ManCiNum(p->pAig); i++ ) { - pInfo = Vec_PtrEntry( p->vCiSimInfo, i ); + pInfo = (unsigned *)Vec_PtrEntry( p->vCiSimInfo, i ); if ( Gia_InfoHasBit( pInfo, iPat ) ) Gia_InfoSetBit( p->pCexComb->pData, i ); } @@ -559,7 +562,7 @@ void Cec_ManSimFindBestPattern( Cec_ManSim_t * p ) assert( p->pBestState->nRegs == Gia_ManRegNum(p->pAig) ); for ( i = 0; i < Gia_ManRegNum(p->pAig); i++ ) { - pInfo = Vec_PtrEntry( p->vCiSimInfo, Gia_ManPiNum(p->pAig) + i ); + pInfo = (unsigned *)Vec_PtrEntry( p->vCiSimInfo, Gia_ManPiNum(p->pAig) + i ); if ( Gia_InfoHasBit(p->pBestState->pData, i) != Gia_InfoHasBit(pInfo, iPatBest) ) Gia_InfoXorBit( p->pBestState->pData, i ); } @@ -591,8 +594,8 @@ int Cec_ManSimAnalyzeOutputs( Cec_ManSim_t * p ) assert( (Gia_ManPoNum(p->pAig) & 1) == 0 ); for ( i = 0; i < Gia_ManPoNum(p->pAig); i++ ) { - pInfo = Vec_PtrEntry( p->vCoSimInfo, i ); - pInfo2 = Vec_PtrEntry( p->vCoSimInfo, ++i ); + pInfo = (unsigned *)Vec_PtrEntry( p->vCoSimInfo, i ); + pInfo2 = (unsigned *)Vec_PtrEntry( p->vCoSimInfo, ++i ); if ( !Cec_ManSimCompareEqual( pInfo, pInfo2, p->nWords ) ) { if ( p->iOut == -1 ) @@ -614,7 +617,7 @@ int Cec_ManSimAnalyzeOutputs( Cec_ManSim_t * p ) { for ( i = 0; i < Gia_ManPoNum(p->pAig); i++ ) { - pInfo = Vec_PtrEntry( p->vCoSimInfo, i ); + pInfo = (unsigned *)Vec_PtrEntry( p->vCoSimInfo, i ); if ( !Cec_ManSimCompareConst( pInfo, p->nWords ) ) { if ( p->iOut == -1 ) @@ -679,7 +682,7 @@ int Cec_ManSimSimulateRound( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t * pRes = Cec_ManSimSimRef( p, i ); if ( vInfoCis ) { - pRes0 = Vec_PtrEntry( vInfoCis, iCiId++ ); + pRes0 = (unsigned *)Vec_PtrEntry( vInfoCis, iCiId++ ); for ( w = 1; w <= p->nWords; w++ ) pRes[w] = pRes0[w-1]; } @@ -697,7 +700,7 @@ int Cec_ManSimSimulateRound( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t * pRes0 = Cec_ManSimSimDeref( p, Gia_ObjFaninId0(pObj,i) ); if ( vInfoCos ) { - pRes = Vec_PtrEntry( vInfoCos, iCoId++ ); + pRes = (unsigned *)Vec_PtrEntry( vInfoCos, iCoId++ ); if ( Gia_ObjFaninC0(pObj) ) for ( w = 1; w <= p->nWords; w++ ) pRes[w-1] = ~pRes0[w]; @@ -712,7 +715,7 @@ int Cec_ManSimSimulateRound( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t * pRes0 = Cec_ManSimSimDeref( p, Gia_ObjFaninId0(pObj,i) ); pRes1 = Cec_ManSimSimDeref( p, Gia_ObjFaninId1(pObj,i) ); -// printf( "%d,%d ", Gia_ObjValue( Gia_ObjFanin0(pObj) ), Gia_ObjValue( Gia_ObjFanin1(pObj) ) ); +// Abc_Print( 1, "%d,%d ", Gia_ObjValue( Gia_ObjFanin0(pObj) ), Gia_ObjValue( Gia_ObjFanin1(pObj) ) ); if ( Gia_ObjFaninC0(pObj) ) { @@ -762,7 +765,7 @@ references: assert( vInfoCos == NULL || iCoId == Gia_ManCoNum(p->pAig) ); assert( p->nMems == 1 ); if ( p->nMems != 1 ) - printf( "Cec_ManSimSimulateRound(): Memory management error!\n" ); + Abc_Print( 1, "Cec_ManSimSimulateRound(): Memory management error!\n" ); if ( p->pPars->fVeryVerbose ) Gia_ManEquivPrintClasses( p->pAig, 0, Cec_MemUsage(p) ); if ( p->pBestState ) @@ -800,14 +803,14 @@ void Cec_ManSimCreateInfo( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t * v assert( vInfoCis && vInfoCos ); for ( i = 0; i < Gia_ManPiNum(p->pAig); i++ ) { - pRes0 = Vec_PtrEntry( vInfoCis, i ); + pRes0 = (unsigned *)Vec_PtrEntry( vInfoCis, i ); for ( w = 0; w < p->nWords; w++ ) pRes0[w] = Gia_ManRandom( 0 ); } for ( i = 0; i < Gia_ManRegNum(p->pAig); i++ ) { - pRes0 = Vec_PtrEntry( vInfoCis, Gia_ManPiNum(p->pAig) + i ); - pRes1 = Vec_PtrEntry( vInfoCos, Gia_ManPoNum(p->pAig) + i ); + pRes0 = (unsigned *)Vec_PtrEntry( vInfoCis, Gia_ManPiNum(p->pAig) + i ); + pRes1 = (unsigned *)Vec_PtrEntry( vInfoCos, Gia_ManPoNum(p->pAig) + i ); for ( w = 0; w < p->nWords; w++ ) pRes0[w] = pRes1[w]; } @@ -816,7 +819,7 @@ void Cec_ManSimCreateInfo( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t * v { for ( i = 0; i < Gia_ManCiNum(p->pAig); i++ ) { - pRes0 = Vec_PtrEntry( vInfoCis, i ); + pRes0 = (unsigned *)Vec_PtrEntry( vInfoCis, i ); for ( w = 0; w < p->nWords; w++ ) pRes0[w] = Gia_ManRandom( 0 ); } @@ -834,7 +837,7 @@ void Cec_ManSimCreateInfo( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t * v SeeAlso [] ***********************************************************************/ -int Cec_ManSimClassesPrepare( Cec_ManSim_t * p ) +int Cec_ManSimClassesPrepare( Cec_ManSim_t * p, int LevelMax ) { Gia_Obj_t * pObj; int i; @@ -848,9 +851,16 @@ int Cec_ManSimClassesPrepare( Cec_ManSim_t * p ) if ( p->pPars->fLatchCorr ) Gia_ManForEachObj( p->pAig, pObj, i ) Gia_ObjSetRepr( p->pAig, i, GIA_VOID ); - else + else if ( LevelMax == -1 ) Gia_ManForEachObj( p->pAig, pObj, i ) Gia_ObjSetRepr( p->pAig, i, Gia_ObjIsAnd(pObj) ? 0 : GIA_VOID ); + else + { + Gia_ManLevelNum( p->pAig ); + Gia_ManForEachObj( p->pAig, pObj, i ) + Gia_ObjSetRepr( p->pAig, i, (Gia_ObjIsAnd(pObj) && Gia_ObjLevel(p->pAig,pObj) <= LevelMax) ? 0 : GIA_VOID ); + Vec_IntFreeP( &p->pAig->vLevels ); + } // if sequential simulation, set starting representative of ROs to be constant 0 if ( p->pPars->fSeqSimulate ) Gia_ManForEachRo( p->pAig, pObj, i ) @@ -906,3 +916,5 @@ int Cec_ManSimClassesRefine( Cec_ManSim_t * p ) //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/cec/cecCore.c b/src/aig/cec/cecCore.c index 10c145ec..5e71dbff 100644 --- a/src/aig/cec/cecCore.c +++ b/src/aig/cec/cecCore.c @@ -20,6 +20,9 @@ #include "cecInt.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -133,8 +136,10 @@ void Cec_ManFraSetDefaultParams( Cec_ParFra_t * p ) // p->fFirstStop = 0; // stop on the first sat output p->fDualOut = 0; // miter with separate outputs p->fColorDiff = 0; // miter with separate outputs + p->fSatSweeping = 0; // enable SAT sweeping p->fVeryVerbose = 0; // verbose stats p->fVerbose = 0; // verbose stats + p->iOutFail = -1; // the failed output } /**Function************************************************************* @@ -158,6 +163,7 @@ void Cec_ManCecSetDefaultParams( Cec_ParCec_t * p ) p->fRewriting = 0; // enables AIG rewriting p->fVeryVerbose = 0; // verbose stats p->fVerbose = 0; // verbose stats + p->iOutFail = -1; // the number of failed output } /**Function************************************************************* @@ -178,6 +184,8 @@ void Cec_ManCorSetDefaultParams( Cec_ParCor_t * p ) p->nRounds = 15; // the number of simulation rounds p->nFrames = 1; // the number of time frames p->nBTLimit = 100; // conflict limit at a node + p->nLevelMax = -1; // (scorr only) the max number of levels + p->nStepsMax = -1; // (scorr only) the max number of induction steps p->fLatchCorr = 0; // consider only latch outputs p->fUseRings = 1; // combine classes into rings p->fUseCSat = 1; // use circuit-based solver @@ -249,12 +257,12 @@ int Cec_ManSimulationOne( Gia_Man_t * pAig, Cec_ParSim_t * pPars ) Cec_ManSim_t * pSim; int RetValue = 0, clkTotal = clock(); pSim = Cec_ManSimStart( pAig, pPars ); - if ( (pAig->pReprs == NULL && (RetValue = Cec_ManSimClassesPrepare( pSim ))) || + if ( (pAig->pReprs == NULL && (RetValue = Cec_ManSimClassesPrepare( pSim, -1 ))) || (RetValue == 0 && (RetValue = Cec_ManSimClassesRefine( pSim ))) ) - printf( "The number of failed outputs of the miter = %6d. (Words = %4d. Frames = %4d.)\n", + Abc_Print( 1, "The number of failed outputs of the miter = %6d. (Words = %4d. Frames = %4d.)\n", pSim->nOuts, pPars->nWords, pPars->nFrames ); if ( pPars->fVerbose ) - ABC_PRT( "Time", clock() - clkTotal ); + Abc_PrintTime( 1, "Time", clock() - clkTotal ); Cec_ManSimStop( pSim ); return RetValue; } @@ -275,7 +283,7 @@ void Cec_ManSimulation( Gia_Man_t * pAig, Cec_ParSim_t * pPars ) int r, nLitsOld, nLitsNew, nCountNoRef = 0, fStop = 0; Gia_ManRandom( 1 ); if ( pPars->fSeqSimulate ) - printf( "Performing rounds of random simulation of %d frames with %d words.\n", + Abc_Print( 1, "Performing rounds of random simulation of %d frames with %d words.\n", pPars->nRounds, pPars->nFrames, pPars->nWords ); nLitsOld = Gia_ManEquivCountLits( pAig ); for ( r = 0; r < pPars->nRounds; r++ ) @@ -301,14 +309,14 @@ void Cec_ManSimulation( Gia_Man_t * pAig, Cec_ParSim_t * pPars ) } // if ( pPars->fVerbose ) if ( r == pPars->nRounds || fStop ) - printf( "Random simulation is stopped after %d rounds.\n", r ); + Abc_Print( 1, "Random simulation is stopped after %d rounds.\n", r ); else - printf( "Random simulation saturated after %d rounds.\n", r ); + Abc_Print( 1, "Random simulation saturated after %d rounds.\n", r ); if ( pPars->fCheckMiter ) { int nNonConsts = Cec_ManCountNonConstOutputs( pAig ); if ( nNonConsts ) - printf( "The number of POs that are not const-0 candidates = %d.\n", nNonConsts ); + Abc_Print( 1, "The number of POs that are not const-0 candidates = %d.\n", nNonConsts ); } } @@ -366,7 +374,7 @@ Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars ) clk = clock(); if ( p->pAig->pReprs == NULL ) { - if ( Cec_ManSimClassesPrepare(pSim) || Cec_ManSimClassesRefine(pSim) ) + if ( Cec_ManSimClassesPrepare(pSim, -1) || Cec_ManSimClassesRefine(pSim) ) { Gia_ManStop( p->pAig ); p->pAig = NULL; @@ -395,19 +403,19 @@ p->timeSim += clock() - clk; { Gia_ManStop( pSrm ); if ( p->pPars->fVerbose ) - printf( "Considered all available candidate equivalences.\n" ); + Abc_Print( 1, "Considered all available candidate equivalences.\n" ); if ( pPars->fDualOut && Gia_ManAndNum(p->pAig) > 0 ) { if ( pPars->fColorDiff ) { if ( p->pPars->fVerbose ) - printf( "Switching into reduced mode.\n" ); + Abc_Print( 1, "Switching into reduced mode.\n" ); pPars->fColorDiff = 0; } else { if ( p->pPars->fVerbose ) - printf( "Switching into normal mode.\n" ); + Abc_Print( 1, "Switching into normal mode.\n" ); pPars->fDualOut = 0; } continue; @@ -433,14 +441,14 @@ p->timeSat += clock() - clk; break; if ( p->pPars->fVerbose ) { - printf( "%3d : P =%7d. D =%7d. F =%6d. M = %7d. And =%8d. ", + Abc_Print( 1, "%3d : P =%7d. D =%7d. F =%6d. M = %7d. And =%8d. ", i, p->nAllProved, p->nAllDisproved, p->nAllFailed, nMatches, Gia_ManAndNum(p->pAig) ); - ABC_PRT( "Time", clock() - clk2 ); + Abc_PrintTime( 1, "Time", clock() - clk2 ); } if ( Gia_ManAndNum(p->pAig) == 0 ) { if ( p->pPars->fVerbose ) - printf( "Network after reduction is empty.\n" ); + Abc_Print( 1, "Network after reduction is empty.\n" ); break; } // check resource limits @@ -454,54 +462,63 @@ p->timeSat += clock() - clk; { if ( pParsSat->nBTLimit >= 10001 ) break; + if ( pPars->fSatSweeping ) + { + if ( p->pPars->fVerbose ) + Abc_Print( 1, "Exceeded the limit on the number of conflicts (%d).\n", pParsSat->nBTLimit ); + break; + } pParsSat->nBTLimit *= 10; if ( p->pPars->fVerbose ) { if ( p->pPars->fVerbose ) - printf( "Increasing conflict limit to %d.\n", pParsSat->nBTLimit ); + Abc_Print( 1, "Increasing conflict limit to %d.\n", pParsSat->nBTLimit ); if ( fOutputResult ) { Gia_WriteAiger( p->pAig, "gia_cec_temp.aig", 0, 0 ); - printf("The result is written into file \"%s\".\n", "gia_cec_temp.aig" ); + Abc_Print( 1,"The result is written into file \"%s\".\n", "gia_cec_temp.aig" ); } } } if ( pPars->fDualOut && pPars->fColorDiff && (Gia_ManAndNum(p->pAig) < 100000 || p->nAllProved + p->nAllDisproved < 10) ) { if ( p->pPars->fVerbose ) - printf( "Switching into reduced mode.\n" ); + Abc_Print( 1, "Switching into reduced mode.\n" ); pPars->fColorDiff = 0; } // if ( pPars->fDualOut && Gia_ManAndNum(p->pAig) < 20000 ) else if ( pPars->fDualOut && (Gia_ManAndNum(p->pAig) < 20000 || p->nAllProved + p->nAllDisproved < 10) ) { if ( p->pPars->fVerbose ) - printf( "Switching into normal mode.\n" ); + Abc_Print( 1, "Switching into normal mode.\n" ); pPars->fColorDiff = 0; pPars->fDualOut = 0; } } finalize: - if ( p->pPars->fVerbose ) + if ( p->pPars->fVerbose && p->pAig ) { - printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n", + Abc_Print( 1, "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n", Gia_ManAndNum(pAig), Gia_ManAndNum(p->pAig), 100.0*(Gia_ManAndNum(pAig)-Gia_ManAndNum(p->pAig))/(Gia_ManAndNum(pAig)?Gia_ManAndNum(pAig):1), Gia_ManRegNum(pAig), Gia_ManRegNum(p->pAig), 100.0*(Gia_ManRegNum(pAig)-Gia_ManRegNum(p->pAig))/(Gia_ManRegNum(pAig)?Gia_ManRegNum(pAig):1) ); - ABC_PRTP( "Sim ", p->timeSim, clock() - (int)clkTotal ); - ABC_PRTP( "Sat ", p->timeSat-pPat->timeTotalSave, clock() - (int)clkTotal ); - ABC_PRTP( "Pat ", p->timePat+pPat->timeTotalSave, clock() - (int)clkTotal ); - ABC_PRT( "Time", clock() - clkTotal ); + Abc_PrintTimeP( 1, "Sim ", p->timeSim, clock() - (int)clkTotal ); + Abc_PrintTimeP( 1, "Sat ", p->timeSat-pPat->timeTotalSave, clock() - (int)clkTotal ); + Abc_PrintTimeP( 1, "Pat ", p->timePat+pPat->timeTotalSave, clock() - (int)clkTotal ); + Abc_PrintTime( 1, "Time", (int)(clock() - clkTotal) ); } pTemp = p->pAig; p->pAig = NULL; if ( pTemp == NULL && pSim->iOut >= 0 ) - printf( "Disproved at least one output of the miter (zero-based number %d).\n", pSim->iOut ); + { + Abc_Print( 1, "Disproved at least one output of the miter (zero-based number %d).\n", pSim->iOut ); + pPars->iOutFail = pSim->iOut; + } else if ( pSim->pCexes ) - printf( "Disproved %d outputs of the miter.\n", pSim->nOuts ); + Abc_Print( 1, "Disproved %d outputs of the miter.\n", pSim->nOuts ); if ( fTimeOut ) - printf( "Timed out after %d seconds.\n", (int)((double)clock() - clkTotal)/CLOCKS_PER_SEC ); + Abc_Print( 1, "Timed out after %d seconds.\n", (int)((double)clock() - clkTotal)/CLOCKS_PER_SEC ); pAig->pCexComb = pSim->pCexComb; pSim->pCexComb = NULL; Cec_ManSimStop( pSim ); @@ -516,3 +533,5 @@ finalize: //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/cec/cecCorr.c b/src/aig/cec/cecCorr.c index 52d2b80e..565ca47e 100644 --- a/src/aig/cec/cecCorr.c +++ b/src/aig/cec/cecCorr.c @@ -20,6 +20,9 @@ #include "cecInt.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -197,9 +200,9 @@ Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_I Vec_IntFree( vXorLits ); Gia_ManHashStop( pNew ); ABC_FREE( p->pCopies ); -//printf( "Before sweeping = %d\n", Gia_ManAndNum(pNew) ); +//Abc_Print( 1, "Before sweeping = %d\n", Gia_ManAndNum(pNew) ); pNew = Gia_ManCleanup( pTemp = pNew ); -//printf( "After sweeping = %d\n", Gia_ManAndNum(pNew) ); +//Abc_Print( 1, "After sweeping = %d\n", Gia_ManAndNum(pNew) ); Gia_ManStop( pTemp ); return pNew; } @@ -266,9 +269,9 @@ Gia_Man_t * Gia_ManCorrSpecReduceInit( Gia_Man_t * p, int nFrames, int nPrefix, Vec_IntFree( vXorLits ); Gia_ManHashStop( pNew ); ABC_FREE( p->pCopies ); -//printf( "Before sweeping = %d\n", Gia_ManAndNum(pNew) ); +//Abc_Print( 1, "Before sweeping = %d\n", Gia_ManAndNum(pNew) ); pNew = Gia_ManCleanup( pTemp = pNew ); -//printf( "After sweeping = %d\n", Gia_ManAndNum(pNew) ); +//Abc_Print( 1, "After sweeping = %d\n", Gia_ManAndNum(pNew) ); Gia_ManStop( pTemp ); return pNew; } @@ -292,13 +295,13 @@ void Cec_ManStartSimInfo( Vec_Ptr_t * vInfo, int nFlops ) assert( nFlops <= Vec_PtrSize(vInfo) ); for ( k = 0; k < nFlops; k++ ) { - pInfo = Vec_PtrEntry( vInfo, k ); + pInfo = (unsigned *)Vec_PtrEntry( vInfo, k ); for ( w = 0; w < nWords; w++ ) pInfo[w] = 0; } for ( k = nFlops; k < Vec_PtrSize(vInfo); k++ ) { - pInfo = Vec_PtrEntry( vInfo, k ); + pInfo = (unsigned *)Vec_PtrEntry( vInfo, k ); for ( w = 0; w < nWords; w++ ) pInfo[w] = Gia_ManRandom( 0 ); } @@ -327,20 +330,20 @@ void Gia_ManCorrRemapSimInfo( Gia_Man_t * p, Vec_Ptr_t * vInfo ) pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) ); if ( pRepr == NULL || Gia_ObjFailed(p, Gia_ObjId(p,pObj)) ) continue; - pInfoObj = Vec_PtrEntry( vInfo, i ); + pInfoObj = (unsigned *)Vec_PtrEntry( vInfo, i ); for ( w = 0; w < nWords; w++ ) assert( pInfoObj[w] == 0 ); // skip ROs with constant representatives if ( Gia_ObjIsConst0(pRepr) ) continue; assert( Gia_ObjIsRo(p, pRepr) ); -// printf( "%d -> %d ", i, Gia_ObjId(p, pRepr) ); +// Abc_Print( 1, "%d -> %d ", i, Gia_ObjId(p, pRepr) ); // transfer info from the representative - pInfoRepr = Vec_PtrEntry( vInfo, Gia_ObjCioId(pRepr) - Gia_ManPiNum(p) ); + pInfoRepr = (unsigned *)Vec_PtrEntry( vInfo, Gia_ObjCioId(pRepr) - Gia_ManPiNum(p) ); for ( w = 0; w < nWords; w++ ) pInfoObj[w] = pInfoRepr[w]; } -// printf( "\n" ); +// Abc_Print( 1, "\n" ); } /**Function************************************************************* @@ -368,7 +371,7 @@ Vec_Int_t * Gia_ManCorrCreateRemapping( Gia_Man_t * p ) // if ( pRepr == NULL || Gia_ObjIsConst0(pRepr) || Gia_ObjIsFailedPair(p, Gia_ObjId(p, pRepr), Gia_ObjId(p, pObj)) ) continue; assert( Gia_ObjIsRo(p, pRepr) ); -// printf( "%d -> %d ", Gia_ObjId(p,pObj), Gia_ObjId(p, pRepr) ); +// Abc_Print( 1, "%d -> %d ", Gia_ObjId(p,pObj), Gia_ObjId(p, pRepr) ); // remember the pair Vec_IntPush( vPairs, Gia_ObjCioId(pRepr) - Gia_ManPiNum(p) ); Vec_IntPush( vPairs, i ); @@ -395,8 +398,8 @@ void Gia_ManCorrPerformRemapping( Vec_Int_t * vPairs, Vec_Ptr_t * vInfo ) Vec_IntForEachEntry( vPairs, iRepr, i ) { iObj = Vec_IntEntry( vPairs, ++i ); - pInfoObj = Vec_PtrEntry( vInfo, iObj ); - pInfoRepr = Vec_PtrEntry( vInfo, iRepr ); + pInfoObj = (unsigned *)Vec_PtrEntry( vInfo, iObj ); + pInfoRepr = (unsigned *)Vec_PtrEntry( vInfo, iRepr ); for ( w = 0; w < nWords; w++ ) { assert( pInfoObj[w] == 0 ); @@ -422,16 +425,16 @@ int Cec_ManLoadCounterExamplesTry( Vec_Ptr_t * vInfo, Vec_Ptr_t * vPres, int iBi int i; for ( i = 0; i < nLits; i++ ) { - pInfo = Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i])); - pPres = Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i])); + pInfo = (unsigned *)Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i])); + pPres = (unsigned *)Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i])); if ( Gia_InfoHasBit( pPres, iBit ) && Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) ) return 0; } for ( i = 0; i < nLits; i++ ) { - pInfo = Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i])); - pPres = Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i])); + pInfo = (unsigned *)Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i])); + pPres = (unsigned *)Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i])); Gia_InfoSetBit( pPres, iBit ); if ( Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) ) Gia_InfoXorBit( pInfo, iBit ); @@ -506,7 +509,7 @@ int Cec_ManLoadCounterExamples2( Vec_Ptr_t * vInfo, Vec_Int_t * vCexStore, int i // skip the output number // iStart++; Out = Vec_IntEntry( vCexStore, iStart++ ); -// printf( "iBit = %d. Out = %d.\n", iBit, Out ); +// Abc_Print( 1, "iBit = %d. Out = %d.\n", iBit, Out ); // get the number of items nLits = Vec_IntEntry( vCexStore, iStart++ ); if ( nLits <= 0 ) @@ -515,14 +518,14 @@ int Cec_ManLoadCounterExamples2( Vec_Ptr_t * vInfo, Vec_Int_t * vCexStore, int i for ( k = 0; k < nLits; k++ ) { iLit = Vec_IntEntry( vCexStore, iStart++ ); - pInfo = Vec_PtrEntry( vInfo, Gia_Lit2Var(iLit) ); + pInfo = (unsigned *)Vec_PtrEntry( vInfo, Gia_Lit2Var(iLit) ); if ( Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(iLit) ) Gia_InfoXorBit( pInfo, iBit ); } if ( ++iBit == nBits ) break; } -// printf( "added %d bits\n", iBit-1 ); +// Abc_Print( 1, "added %d bits\n", iBit-1 ); return iStart; } @@ -620,7 +623,7 @@ int Gia_ManCheckRefinements( Gia_Man_t * p, Vec_Str_t * vStatus, Vec_Int_t * vOu if ( Gia_ObjHasSameRepr(p, iRepr, iObj) ) Counter++; // if ( Gia_ObjHasSameRepr(p, iRepr, iObj) ) -// printf( "Gia_ManCheckRefinements(): Disproved equivalence (%d,%d) is not refined!\n", iRepr, iObj ); +// Abc_Print( 1, "Gia_ManCheckRefinements(): Disproved equivalence (%d,%d) is not refined!\n", iRepr, iObj ); // if ( Gia_ObjHasSameRepr(p, iRepr, iObj) ) // Cec_ManSimClassRemoveOne( pSim, iObj ); continue; @@ -628,7 +631,7 @@ int Gia_ManCheckRefinements( Gia_Man_t * p, Vec_Str_t * vStatus, Vec_Int_t * vOu if ( status == -1 ) { // if ( !Gia_ObjFailed( p, iObj ) ) -// printf( "Gia_ManCheckRefinements(): Failed equivalence is not marked as failed!\n" ); +// Abc_Print( 1, "Gia_ManCheckRefinements(): Failed equivalence is not marked as failed!\n" ); // Gia_ObjSetFailed( p, iRepr ); // Gia_ObjSetFailed( p, iObj ); // if ( fRings ) @@ -638,7 +641,7 @@ int Gia_ManCheckRefinements( Gia_Man_t * p, Vec_Str_t * vStatus, Vec_Int_t * vOu } } // if ( Counter ) -// printf( "Gia_ManCheckRefinements(): Could not refine %d nodes.\n", Counter ); +// Abc_Print( 1, "Gia_ManCheckRefinements(): Could not refine %d nodes.\n", Counter ); return 1; } @@ -732,10 +735,10 @@ void Cec_ManRefinedClassPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIte CounterX -= Gia_ManCoNum(p); nLits = Gia_ManCiNum(p) + Gia_ManAndNum(p) - Counter - CounterX; if ( iIter == -1 ) - printf( "BMC : " ); + Abc_Print( 1, "BMC : " ); else - printf( "%3d : ", iIter ); - printf( "c =%8d cl =%7d lit =%8d ", Counter0, Counter, nLits ); + Abc_Print( 1, "%3d : ", iIter ); + Abc_Print( 1, "c =%8d cl =%7d lit =%8d ", Counter0, Counter, nLits ); if ( vStatus ) Vec_StrForEachEntry( vStatus, Entry, i ) { @@ -746,8 +749,8 @@ void Cec_ManRefinedClassPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIte else if ( Entry == -1 ) nFail++; } - printf( "p =%6d d =%6d f =%6d ", nProve, nDispr, nFail ); - ABC_PRT( "T", Time ); + Abc_Print( 1, "p =%6d d =%6d f =%6d ", nProve, nDispr, nFail ); + Abc_PrintTime( 1, "T", Time ); } /**Function************************************************************* @@ -833,7 +836,7 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) { int nIterMax = 100000; int nAddFrames = 1; // additional timeframes to simulate - int fRunBmcFirst = 0; + int fRunBmcFirst = 1; Vec_Str_t * vStatus; Vec_Int_t * vOutputs; Vec_Int_t * vCexStore; @@ -846,7 +849,7 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) int clk2, clk = clock(); if ( Gia_ManRegNum(pAig) == 0 ) { - printf( "Cec_ManLatchCorrespondence(): Not a sequential AIG.\n" ); + Abc_Print( 1, "Cec_ManLatchCorrespondence(): Not a sequential AIG.\n" ); return 0; } Gia_ManRandom( 1 ); @@ -861,7 +864,7 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) pSim = Cec_ManSimStart( pAig, pParsSim ); if ( pAig->pReprs == NULL ) { - Cec_ManSimClassesPrepare( pSim ); + Cec_ManSimClassesPrepare( pSim, pPars->nLevelMax ); Cec_ManSimClassesRefine( pSim ); } // prepare SAT solving @@ -870,7 +873,7 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) pParsSat->fVerbose = pPars->fVerbose; if ( pPars->fVerbose ) { - printf( "Obj = %7d. And = %7d. Conf = %5d. Fr = %d. Lcorr = %d. Ring = %d. CSat = %d.\n", + Abc_Print( 1, "Obj = %7d. And = %7d. Conf = %5d. Fr = %d. Lcorr = %d. Ring = %d. CSat = %d.\n", Gia_ManObjNum(pAig), Gia_ManAndNum(pAig), pPars->nBTLimit, pPars->nFrames, pPars->fLatchCorr, pPars->fUseRings, pPars->fUseCSat ); Cec_ManRefinedClassPrintStats( pAig, NULL, 0, clock() - clk ); @@ -878,9 +881,26 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) // check the base case if ( fRunBmcFirst && (!pPars->fLatchCorr || pPars->nFrames > 1) ) Cec_ManLSCorrespondenceBmc( pAig, pPars, 0 ); + if ( pPars->pFunc ) + { + ((int (*)(void *))pPars->pFunc)( pPars->pData ); + ((int (*)(void *))pPars->pFunc)( pPars->pData ); + } + if ( pPars->nStepsMax == 0 ) + { + Abc_Print( 1, "Stopped signal correspondence after BMC.\n" ); + Cec_ManSimStop( pSim ); + return 1; + } // perform refinement of equivalence classes for ( r = 0; r < nIterMax; r++ ) { + if ( pPars->nStepsMax == r ) + { + Cec_ManSimStop( pSim ); + Abc_Print( 1, "Stopped signal correspondence after %d refiment iterations.\n", r ); + return 1; + } clk = clock(); // perform speculative reduction clk2 = clock(); @@ -920,12 +940,14 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) Vec_StrFree( vStatus ); Vec_IntFree( vOutputs ); //Gia_ManEquivPrintClasses( pAig, 1, 0 ); + if ( pPars->pFunc ) + ((int (*)(void *))pPars->pFunc)( pPars->pData ); } if ( pPars->fVerbose ) Cec_ManRefinedClassPrintStats( pAig, NULL, r+1, clock() - clk ); // check the overflow if ( r == nIterMax ) - printf( "The refinement was not finished. The result may be incorrect.\n" ); + Abc_Print( 1, "The refinement was not finished. The result may be incorrect.\n" ); Cec_ManSimStop( pSim ); // check the base case if ( !fRunBmcFirst && (!pPars->fLatchCorr || pPars->nFrames > 1) ) @@ -938,9 +960,9 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) ABC_PRTP( "Sat ", clkSat, clkTotal ); ABC_PRTP( "Sim ", clkSim, clkTotal ); ABC_PRTP( "Other", clkTotal-clkSat-clkSrm-clkSim, clkTotal ); - ABC_PRT( "TOTAL", clkTotal ); + Abc_PrintTime( 1, "TOTAL", clkTotal ); } - return 0; + return 1; } /**Function************************************************************* @@ -960,7 +982,7 @@ unsigned * Cec_ManComputeInitState( Gia_Man_t * pAig, int nFrames ) unsigned * pInitState; int i, f; Gia_ManRandom( 1 ); -// printf( "Simulating %d timeframes.\n", nFrames ); +// Abc_Print( 1, "Simulating %d timeframes.\n", nFrames ); Gia_ManForEachRo( pAig, pObj, i ) pObj->fMark1 = 0; for ( f = 0; f < nFrames; f++ ) @@ -981,9 +1003,9 @@ unsigned * Cec_ManComputeInitState( Gia_Man_t * pAig, int nFrames ) { if ( pObj->fMark1 ) Gia_InfoSetBit( pInitState, i ); -// printf( "%d", pObj->fMark1 ); +// Abc_Print( 1, "%d", pObj->fMark1 ); } -// printf( "\n" ); +// Abc_Print( 1, "\n" ); Gia_ManCleanMark1( pAig ); return pInitState; } @@ -1007,15 +1029,15 @@ void Cec_ManPrintFlopEquivs( Gia_Man_t * p ) Gia_ManForEachRo( p, pObj, i ) { if ( Gia_ObjIsConst(p, Gia_ObjId(p, pObj)) ) - printf( "Original flop %s is proved equivalent to constant.\n", Vec_PtrEntry(p->vNamesIn, Gia_ObjCioId(pObj)) ); + Abc_Print( 1, "Original flop %s is proved equivalent to constant.\n", Vec_PtrEntry(p->vNamesIn, Gia_ObjCioId(pObj)) ); else if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) ) { if ( Gia_ObjIsCi(pRepr) ) - printf( "Original flop %s is proved equivalent to flop %s.\n", + Abc_Print( 1, "Original flop %s is proved equivalent to flop %s.\n", Vec_PtrEntry( p->vNamesIn, Gia_ObjCioId(pObj) ), Vec_PtrEntry( p->vNamesIn, Gia_ObjCioId(pRepr) ) ); else - printf( "Original flop %s is proved equivalent to internal node %d.\n", + Abc_Print( 1, "Original flop %s is proved equivalent to internal node %d.\n", Vec_PtrEntry( p->vNamesIn, Gia_ObjCioId(pObj) ), Gia_ObjId(p, pRepr) ); } } @@ -1046,7 +1068,7 @@ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) { // compute the cycles AIG pInitState = Cec_ManComputeInitState( pAig, pPars->nPrefix ); - pTemp = Gia_ManDupFlip( pAig, pInitState ); + pTemp = Gia_ManDupFlip( pAig, (int *)pInitState ); ABC_FREE( pInitState ); // compute classes of this AIG RetValue = Cec_ManLSCorrespondenceClasses( pTemp, pPars ); @@ -1086,19 +1108,19 @@ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) // report the results if ( pPars->fVerbose ) { - printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n", + Abc_Print( 1, "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n", Gia_ManAndNum(pAig), Gia_ManAndNum(pNew), 100.0*(Gia_ManAndNum(pAig)-Gia_ManAndNum(pNew))/(Gia_ManAndNum(pAig)?Gia_ManAndNum(pAig):1), Gia_ManRegNum(pAig), Gia_ManRegNum(pNew), 100.0*(Gia_ManRegNum(pAig)-Gia_ManRegNum(pNew))/(Gia_ManRegNum(pAig)?Gia_ManRegNum(pAig):1) ); } if ( pPars->nPrefix && (Gia_ManAndNum(pNew) < Gia_ManAndNum(pAig) || Gia_ManRegNum(pNew) < Gia_ManRegNum(pAig)) ) - printf( "The reduced AIG was produced using %d-th invariants and will not verify.\n", pPars->nPrefix ); + Abc_Print( 1, "The reduced AIG was produced using %d-th invariants and will not verify.\n", pPars->nPrefix ); // print verbose info about equivalences if ( pPars->fVerboseFlops ) { if ( pAig->vNamesIn == NULL ) - printf( "Flop output names are not available. Use command \"&get -n\".\n" ); + Abc_Print( 1, "Flop output names are not available. Use command \"&get -n\".\n" ); else Cec_ManPrintFlopEquivs( pAig ); } @@ -1110,3 +1132,5 @@ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/cec/cecCorr_updated.c b/src/aig/cec/cecCorr_updated.c index dbe81d81..8ce1bd74 100644 --- a/src/aig/cec/cecCorr_updated.c +++ b/src/aig/cec/cecCorr_updated.c @@ -20,6 +20,9 @@ #include "cecInt.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -970,7 +973,7 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) ABC_PRTP( "Other", clkTotal-clkSat-clkSrm-clkSim, clkTotal ); ABC_PRT( "TOTAL", clkTotal ); } - return 0; + return 1; } /**Function************************************************************* @@ -1020,3 +1023,5 @@ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/cec/cecInt.h b/src/aig/cec/cecInt.h index 73f108ba..6216eae2 100644 --- a/src/aig/cec/cecInt.h +++ b/src/aig/cec/cecInt.h @@ -21,6 +21,7 @@ #ifndef __CEC_INT_H__ #define __CEC_INT_H__ + //////////////////////////////////////////////////////////////////////// /// INCLUDES /// //////////////////////////////////////////////////////////////////////// @@ -34,9 +35,10 @@ /// PARAMETERS /// //////////////////////////////////////////////////////////////////////// -#ifdef __cplusplus -extern "C" { -#endif + + +ABC_NAMESPACE_HEADER_START + //////////////////////////////////////////////////////////////////////// /// BASIC TYPES /// @@ -128,8 +130,8 @@ struct Cec_ManSim_t_ void ** pCexes; // counter-examples for each output int iOut; // first failed output int nOuts; // the number of failed outputs - Gia_Cex_t * pCexComb; // counter-example for the first failed output - Gia_Cex_t * pBestState; // the state that led to most of the refinements + Abc_Cex_t * pCexComb; // counter-example for the first failed output + Abc_Cex_t * pBestState; // the state that led to most of the refinements // scoring simulation patterns int * pScores; // counters of refinement for each pattern // temporaries @@ -170,7 +172,7 @@ struct Cec_ManFra_t_ extern void Cec_ManRefinedClassPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIter, int Time ); /*=== cecClass.c ============================================================*/ extern int Cec_ManSimClassRemoveOne( Cec_ManSim_t * p, int i ); -extern int Cec_ManSimClassesPrepare( Cec_ManSim_t * p ); +extern int Cec_ManSimClassesPrepare( Cec_ManSim_t * p, int LevelMax ); extern int Cec_ManSimClassesRefine( Cec_ManSim_t * p ); extern int Cec_ManSimSimulateRound( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t * vInfoCos ); /*=== cecIso.c ============================================================*/ @@ -192,8 +194,8 @@ extern Vec_Ptr_t * Cec_ManPatCollectPatterns( Cec_ManPat_t * pMan, int extern Vec_Ptr_t * Cec_ManPatPackPatterns( Vec_Int_t * vCexStore, int nInputs, int nRegs, int nWordsInit ); /*=== cecSeq.c ============================================================*/ extern int Cec_ManSeqResimulate( Cec_ManSim_t * p, Vec_Ptr_t * vInfo ); -extern int Cec_ManSeqResimulateInfo( Gia_Man_t * pAig, Vec_Ptr_t * vSimInfo, Gia_Cex_t * pBestState, int fCheckMiter ); -extern void Cec_ManSeqDeriveInfoInitRandom( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Gia_Cex_t * pCex ); +extern int Cec_ManSeqResimulateInfo( Gia_Man_t * pAig, Vec_Ptr_t * vSimInfo, Abc_Cex_t * pBestState, int fCheckMiter ); +extern void Cec_ManSeqDeriveInfoInitRandom( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Abc_Cex_t * pCex ); extern int Cec_ManCountNonConstOutputs( Gia_Man_t * pAig ); extern int Cec_ManCheckNonTrivialCands( Gia_Man_t * pAig ); /*=== cecSolve.c ============================================================*/ @@ -209,9 +211,11 @@ extern Vec_Int_t * Cec_ManSatReadCex( Cec_ManSat_t * p ); extern Gia_Man_t * Cec_ManFraSpecReduction( Cec_ManFra_t * p ); extern int Cec_ManFraClassesUpdate( Cec_ManFra_t * p, Cec_ManSim_t * pSim, Cec_ManPat_t * pPat, Gia_Man_t * pNew ); -#ifdef __cplusplus -} -#endif + + +ABC_NAMESPACE_HEADER_END + + #endif diff --git a/src/aig/cec/cecIso.c b/src/aig/cec/cecIso.c index d9aa5240..ec237fe5 100644 --- a/src/aig/cec/cecIso.c +++ b/src/aig/cec/cecIso.c @@ -20,6 +20,9 @@ #include "cecInt.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -348,13 +351,13 @@ int * Cec_ManDetectIsomorphism( Gia_Man_t * p ) { if ( (Gia_ObjIsHead(p,pIso[i]) && Gia_ObjRepr(p,i)==pIso[i]) || (Gia_ObjIsClass(p,pIso[i]) && Gia_ObjRepr(p,i)==Gia_ObjRepr(p,pIso[i])) ) - printf( "1" ); + Abc_Print( 1, "1" ); else - printf( "0" ); + Abc_Print( 1, "0" ); } */ } - printf( "Computed %d pairs of structurally equivalent nodes.\n", Counter ); + Abc_Print( 1, "Computed %d pairs of structurally equivalent nodes.\n", Counter ); // p->pIso = pIso; // Cec_ManTransformClasses( p ); @@ -368,3 +371,5 @@ int * Cec_ManDetectIsomorphism( Gia_Man_t * p ) //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/cec/cecMan.c b/src/aig/cec/cecMan.c index 70396cca..f03ec701 100644 --- a/src/aig/cec/cecMan.c +++ b/src/aig/cec/cecMan.c @@ -20,6 +20,9 @@ #include "cecInt.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -70,21 +73,21 @@ Cec_ManSat_t * Cec_ManSatCreate( Gia_Man_t * pAig, Cec_ParSat_t * pPars ) ***********************************************************************/ void Cec_ManSatPrintStats( Cec_ManSat_t * p ) { - printf( "CO = %8d ", Gia_ManCoNum(p->pAig) ); - printf( "AND = %8d ", Gia_ManAndNum(p->pAig) ); - printf( "Conf = %5d ", p->pPars->nBTLimit ); - printf( "MinVar = %5d ", p->pPars->nSatVarMax ); - printf( "MinCalls = %5d\n", p->pPars->nCallsRecycle ); - printf( "Unsat calls %6d (%6.2f %%) Ave conf = %8.1f ", + Abc_Print( 1, "CO = %8d ", Gia_ManCoNum(p->pAig) ); + Abc_Print( 1, "AND = %8d ", Gia_ManAndNum(p->pAig) ); + Abc_Print( 1, "Conf = %5d ", p->pPars->nBTLimit ); + Abc_Print( 1, "MinVar = %5d ", p->pPars->nSatVarMax ); + Abc_Print( 1, "MinCalls = %5d\n", p->pPars->nCallsRecycle ); + Abc_Print( 1, "Unsat calls %6d (%6.2f %%) Ave conf = %8.1f ", p->nSatUnsat, p->nSatTotal? 100.0*p->nSatUnsat/p->nSatTotal : 0.0, p->nSatUnsat? 1.0*p->nConfUnsat/p->nSatUnsat :0.0 ); - ABC_PRTP( "Time", p->timeSatUnsat, p->timeTotal ); - printf( "Sat calls %6d (%6.2f %%) Ave conf = %8.1f ", + Abc_PrintTimeP( 1, "Time", p->timeSatUnsat, p->timeTotal ); + Abc_Print( 1, "Sat calls %6d (%6.2f %%) Ave conf = %8.1f ", p->nSatSat, p->nSatTotal? 100.0*p->nSatSat/p->nSatTotal : 0.0, p->nSatSat? 1.0*p->nConfSat/p->nSatSat : 0.0 ); - ABC_PRTP( "Time", p->timeSatSat, p->timeTotal ); - printf( "Undef calls %6d (%6.2f %%) Ave conf = %8.1f ", + Abc_PrintTimeP( 1, "Time", p->timeSatSat, p->timeTotal ); + Abc_Print( 1, "Undef calls %6d (%6.2f %%) Ave conf = %8.1f ", p->nSatUndec, p->nSatTotal? 100.0*p->nSatUndec/p->nSatTotal : 0.0, p->nSatUndec? 1.0*p->nConfUndec/p->nSatUndec : 0.0 ); - ABC_PRTP( "Time", p->timeSatUndec, p->timeTotal ); - ABC_PRT( "Total time", p->timeTotal ); + Abc_PrintTimeP( 1, "Time", p->timeSatUndec, p->timeTotal ); + Abc_PrintTime( 1, "Total time", p->timeTotal ); } /**Function************************************************************* @@ -146,18 +149,18 @@ Cec_ManPat_t * Cec_ManPatStart() ***********************************************************************/ void Cec_ManPatPrintStats( Cec_ManPat_t * p ) { - printf( "Latest: P = %8d. L = %10d. Lm = %10d. Ave = %6.1f. MEM =%6.2f Mb\n", + Abc_Print( 1, "Latest: P = %8d. L = %10d. Lm = %10d. Ave = %6.1f. MEM =%6.2f Mb\n", p->nPats, p->nPatLits, p->nPatLitsMin, 1.0 * p->nPatLitsMin/p->nPats, 1.0*(Vec_StrSize(p->vStorage)-p->iStart)/(1<<20) ); - printf( "Total: P = %8d. L = %10d. Lm = %10d. Ave = %6.1f. MEM =%6.2f Mb\n", + Abc_Print( 1, "Total: P = %8d. L = %10d. Lm = %10d. Ave = %6.1f. MEM =%6.2f Mb\n", p->nPatsAll, p->nPatLitsAll, p->nPatLitsMinAll, 1.0 * p->nPatLitsMinAll/p->nPatsAll, 1.0*Vec_StrSize(p->vStorage)/(1<<20) ); - ABC_PRTP( "Finding ", p->timeFind, p->timeTotal ); - ABC_PRTP( "Shrinking", p->timeShrink, p->timeTotal ); - ABC_PRTP( "Verifying", p->timeVerify, p->timeTotal ); - ABC_PRTP( "Sorting ", p->timeSort, p->timeTotal ); - ABC_PRTP( "Packing ", p->timePack, p->timeTotal ); - ABC_PRT( "TOTAL ", p->timeTotal ); + Abc_PrintTimeP( 1, "Finding ", p->timeFind, p->timeTotal ); + Abc_PrintTimeP( 1, "Shrinking", p->timeShrink, p->timeTotal ); + Abc_PrintTimeP( 1, "Verifying", p->timeVerify, p->timeTotal ); + Abc_PrintTimeP( 1, "Sorting ", p->timeSort, p->timeTotal ); + Abc_PrintTimeP( 1, "Packing ", p->timePack, p->timeTotal ); + Abc_PrintTime( 1, "TOTAL ", p->timeTotal ); } /**Function************************************************************* @@ -290,3 +293,5 @@ void Cec_ManFraStop( Cec_ManFra_t * p ) //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/cec/cecPat.c b/src/aig/cec/cecPat.c index 8537fe4a..82c12ea9 100644 --- a/src/aig/cec/cecPat.c +++ b/src/aig/cec/cecPat.c @@ -20,6 +20,9 @@ #include "cecInt.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -296,7 +299,7 @@ void Cec_ManPatVerifyPattern( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vPat Value = Cec_ManPatComputePattern3_rec( p, Gia_ObjFanin0(pObj) ); Value = Gia_XsimNotCond( Value, Gia_ObjFaninC0(pObj) ); if ( Value != GIA_ONE ) - printf( "Cec_ManPatVerifyPattern(): Verification failed.\n" ); + Abc_Print( 1, "Cec_ManPatVerifyPattern(): Verification failed.\n" ); assert( Value == GIA_ONE ); } @@ -412,16 +415,16 @@ int Cec_ManPatCollectTry( Vec_Ptr_t * vInfo, Vec_Ptr_t * vPres, int iBit, int * int i; for ( i = 0; i < nLits; i++ ) { - pInfo = Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i])); - pPres = Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i])); + pInfo = (unsigned *)Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i])); + pPres = (unsigned *)Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i])); if ( Gia_InfoHasBit( pPres, iBit ) && Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) ) return 0; } for ( i = 0; i < nLits; i++ ) { - pInfo = Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i])); - pPres = Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i])); + pInfo = (unsigned *)Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i])); + pPres = (unsigned *)Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i])); Gia_InfoSetBit( pPres, iBit ); if ( Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) ) Gia_InfoXorBit( pInfo, iBit ); @@ -478,7 +481,7 @@ Vec_Ptr_t * Cec_ManPatCollectPatterns( Cec_ManPat_t * pMan, int nInputs, int nW pMan->iStart = iStartOld; if ( pMan->fVerbose ) { - printf( "Total = %5d. Max used = %5d. Full = %5d. Series = %d. ", + Abc_Print( 1, "Total = %5d. Max used = %5d. Full = %5d. Series = %d. ", nPatterns, kMax, nWordsInit*32, pMan->nSeries ); ABC_PRT( "Time", clock() - clk ); Cec_ManPatPrintStats( pMan ); @@ -551,7 +554,7 @@ Vec_Ptr_t * Cec_ManPatPackPatterns( Vec_Int_t * vCexStore, int nInputs, int nReg nBits *= 2; } } -// printf( "packed %d patterns into %d vectors (out of %d)\n", nPatterns, kMax, nBits ); +// Abc_Print( 1, "packed %d patterns into %d vectors (out of %d)\n", nPatterns, kMax, nBits ); Vec_PtrFree( vPres ); Vec_IntFree( vPat ); return vInfo; @@ -562,3 +565,5 @@ Vec_Ptr_t * Cec_ManPatPackPatterns( Vec_Int_t * vCexStore, int nInputs, int nReg //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/cec/cecSeq.c b/src/aig/cec/cecSeq.c index 49f2a018..b91e8523 100644 --- a/src/aig/cec/cecSeq.c +++ b/src/aig/cec/cecSeq.c @@ -20,6 +20,9 @@ #include "cecInt.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -39,7 +42,7 @@ SeeAlso [] ***********************************************************************/ -void Cec_ManSeqDeriveInfoFromCex( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Gia_Cex_t * pCex ) +void Cec_ManSeqDeriveInfoFromCex( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Abc_Cex_t * pCex ) { unsigned * pInfo; int k, i, w, nWords; @@ -56,14 +59,14 @@ void Cec_ManSeqDeriveInfoFromCex( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Gia_Cex_t */ for ( k = 0; k < Gia_ManRegNum(pAig); k++ ) { - pInfo = Vec_PtrEntry( vInfo, k ); + pInfo = (unsigned *)Vec_PtrEntry( vInfo, k ); for ( w = 0; w < nWords; w++ ) pInfo[w] = 0; } for ( i = pCex->nRegs; i < pCex->nBits; i++ ) { - pInfo = Vec_PtrEntry( vInfo, k++ ); + pInfo = (unsigned *)Vec_PtrEntry( vInfo, k++ ); for ( w = 0; w < nWords; w++ ) pInfo[w] = Gia_ManRandom(0); // set simulation pattern and make sure it is second (first will be erased during simulation) @@ -72,7 +75,7 @@ void Cec_ManSeqDeriveInfoFromCex( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Gia_Cex_t } for ( ; k < Vec_PtrSize(vInfo); k++ ) { - pInfo = Vec_PtrEntry( vInfo, k ); + pInfo = (unsigned *)Vec_PtrEntry( vInfo, k ); for ( w = 0; w < nWords; w++ ) pInfo[w] = Gia_ManRandom(0); } @@ -89,7 +92,7 @@ void Cec_ManSeqDeriveInfoFromCex( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Gia_Cex_t SeeAlso [] ***********************************************************************/ -void Cec_ManSeqDeriveInfoInitRandom( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Gia_Cex_t * pCex ) +void Cec_ManSeqDeriveInfoInitRandom( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Abc_Cex_t * pCex ) { unsigned * pInfo; int k, w, nWords; @@ -98,14 +101,14 @@ void Cec_ManSeqDeriveInfoInitRandom( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Gia_Ce assert( Gia_ManRegNum(pAig) <= Vec_PtrSize(vInfo) ); for ( k = 0; k < Gia_ManRegNum(pAig); k++ ) { - pInfo = Vec_PtrEntry( vInfo, k ); + pInfo = (unsigned *)Vec_PtrEntry( vInfo, k ); for ( w = 0; w < nWords; w++ ) pInfo[w] = (pCex && Gia_InfoHasBit(pCex->pData, k))? ~0 : 0; } for ( ; k < Vec_PtrSize(vInfo); k++ ) { - pInfo = Vec_PtrEntry( vInfo, k ); + pInfo = (unsigned *)Vec_PtrEntry( vInfo, k ); for ( w = 0; w < nWords; w++ ) pInfo[w] = Gia_ManRandom( 0 ); } @@ -130,8 +133,8 @@ int Cec_ManSeqResimulate( Cec_ManSim_t * p, Vec_Ptr_t * vInfo ) assert( Vec_PtrSize(vInfo) == Gia_ManRegNum(p->pAig) + Gia_ManPiNum(p->pAig) * p->pPars->nFrames ); for ( k = 0; k < Gia_ManRegNum(p->pAig); k++ ) { - pInfo0 = Vec_PtrEntry( vInfo, k ); - pInfo1 = Vec_PtrEntry( p->vCoSimInfo, Gia_ManPoNum(p->pAig) + k ); + pInfo0 = (unsigned *)Vec_PtrEntry( vInfo, k ); + pInfo1 = (unsigned *)Vec_PtrEntry( p->vCoSimInfo, Gia_ManPoNum(p->pAig) + k ); for ( w = 0; w < p->nWords; w++ ) pInfo1[w] = pInfo0[w]; } @@ -139,15 +142,15 @@ int Cec_ManSeqResimulate( Cec_ManSim_t * p, Vec_Ptr_t * vInfo ) { for ( i = 0; i < Gia_ManPiNum(p->pAig); i++ ) { - pInfo0 = Vec_PtrEntry( vInfo, k++ ); - pInfo1 = Vec_PtrEntry( p->vCiSimInfo, i ); + pInfo0 = (unsigned *)Vec_PtrEntry( vInfo, k++ ); + pInfo1 = (unsigned *)Vec_PtrEntry( p->vCiSimInfo, i ); for ( w = 0; w < p->nWords; w++ ) pInfo1[w] = pInfo0[w]; } for ( i = 0; i < Gia_ManRegNum(p->pAig); i++ ) { - pInfo0 = Vec_PtrEntry( p->vCoSimInfo, Gia_ManPoNum(p->pAig) + i ); - pInfo1 = Vec_PtrEntry( p->vCiSimInfo, Gia_ManPiNum(p->pAig) + i ); + pInfo0 = (unsigned *)Vec_PtrEntry( p->vCoSimInfo, Gia_ManPoNum(p->pAig) + i ); + pInfo1 = (unsigned *)Vec_PtrEntry( p->vCiSimInfo, Gia_ManPiNum(p->pAig) + i ); for ( w = 0; w < p->nWords; w++ ) pInfo1[w] = pInfo0[w]; } @@ -169,7 +172,7 @@ int Cec_ManSeqResimulate( Cec_ManSim_t * p, Vec_Ptr_t * vInfo ) SeeAlso [] ***********************************************************************/ -int Cec_ManSeqResimulateInfo( Gia_Man_t * pAig, Vec_Ptr_t * vSimInfo, Gia_Cex_t * pBestState, int fCheckMiter ) +int Cec_ManSeqResimulateInfo( Gia_Man_t * pAig, Vec_Ptr_t * vSimInfo, Abc_Cex_t * pBestState, int fCheckMiter ) { Cec_ParSim_t ParsSim, * pParsSim = &ParsSim; Cec_ManSim_t * pSim; @@ -200,33 +203,33 @@ int Cec_ManSeqResimulateInfo( Gia_Man_t * pAig, Vec_Ptr_t * vSimInfo, Gia_Cex_t SeeAlso [] ***********************************************************************/ -int Cec_ManSeqResimulateCounter( Gia_Man_t * pAig, Cec_ParSim_t * pPars, Gia_Cex_t * pCex ) +int Cec_ManSeqResimulateCounter( Gia_Man_t * pAig, Cec_ParSim_t * pPars, Abc_Cex_t * pCex ) { Vec_Ptr_t * vSimInfo; int RetValue, clkTotal = clock(); if ( pCex == NULL ) { - printf( "Cec_ManSeqResimulateCounter(): Counter-example is not available.\n" ); + Abc_Print( 1, "Cec_ManSeqResimulateCounter(): Counter-example is not available.\n" ); return -1; } if ( pAig->pReprs == NULL ) { - printf( "Cec_ManSeqResimulateCounter(): Equivalence classes are not available.\n" ); + Abc_Print( 1, "Cec_ManSeqResimulateCounter(): Equivalence classes are not available.\n" ); return -1; } if ( Gia_ManRegNum(pAig) == 0 ) { - printf( "Cec_ManSeqResimulateCounter(): Not a sequential AIG.\n" ); + Abc_Print( 1, "Cec_ManSeqResimulateCounter(): Not a sequential AIG.\n" ); return -1; } // if ( Gia_ManRegNum(pAig) != pCex->nRegs || Gia_ManPiNum(pAig) != pCex->nPis ) if ( Gia_ManPiNum(pAig) != pCex->nPis ) { - printf( "Cec_ManSeqResimulateCounter(): The number of PIs in the AIG and the counter-example differ.\n" ); + Abc_Print( 1, "Cec_ManSeqResimulateCounter(): The number of PIs in the AIG and the counter-example differ.\n" ); return -1; } if ( pPars->fVerbose ) - printf( "Resimulating %d timeframes.\n", pPars->nFrames + pCex->iFrame + 1 ); + Abc_Print( 1, "Resimulating %d timeframes.\n", pPars->nFrames + pCex->iFrame + 1 ); Gia_ManRandom( 1 ); vSimInfo = Vec_PtrAllocSimInfo( Gia_ManRegNum(pAig) + Gia_ManPiNum(pAig) * (pPars->nFrames + pCex->iFrame + 1), 1 ); @@ -240,7 +243,7 @@ int Cec_ManSeqResimulateCounter( Gia_Man_t * pAig, Cec_ParSim_t * pPars, Gia_Cex if ( pPars->fVerbose ) ABC_PRT( "Time", clock() - clkTotal ); if ( RetValue ) - printf( "Cec_ManSeqResimulateCounter(): An output of the miter is asserted!\n" ); + Abc_Print( 1, "Cec_ManSeqResimulateCounter(): An output of the miter is asserted!\n" ); return RetValue; } @@ -320,17 +323,17 @@ int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars ) Cec_ParSat_t ParsSat, * pParsSat = &ParsSat; Vec_Ptr_t * vSimInfo; Vec_Str_t * vStatus; - Gia_Cex_t * pState; + Abc_Cex_t * pState; Gia_Man_t * pSrm, * pReduce, * pAux; int r, nPats, RetValue = 0; if ( pAig->pReprs == NULL ) { - printf( "Cec_ManSeqSemiformal(): Equivalence classes are not available.\n" ); + Abc_Print( 1, "Cec_ManSeqSemiformal(): Equivalence classes are not available.\n" ); return -1; } if ( Gia_ManRegNum(pAig) == 0 ) { - printf( "Cec_ManSeqSemiformal(): Not a sequential AIG.\n" ); + Abc_Print( 1, "Cec_ManSeqSemiformal(): Not a sequential AIG.\n" ); return -1; } Gia_ManRandom( 1 ); @@ -344,7 +347,7 @@ int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars ) pParsSat->fVerbose = pPars->fVerbose; if ( pParsSat->fVerbose ) { - printf( "Starting: " ); + Abc_Print( 1, "Starting: " ); Gia_ManEquivPrintClasses( pAig, 0, 0 ); } // perform the given number of BMC rounds @@ -353,7 +356,7 @@ int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars ) { if ( !Cec_ManCheckNonTrivialCands(pAig) ) { - printf( "Cec_ManSeqSemiformal: There are only trivial equiv candidates left (PO drivers). Quitting.\n" ); + Abc_Print( 1, "Cec_ManSeqSemiformal: There are only trivial equiv candidates left (PO drivers). Quitting.\n" ); break; } // Gia_ManPrintCounterExample( pState ); @@ -362,12 +365,12 @@ int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars ) pSrm = Gia_ManSpecReduceInitFrames( pAig, pState, pPars->nFrames, &nFramesReal, pPars->fDualOut, pPars->nMinOutputs ); if ( pSrm == NULL ) { - printf( "Quitting refinement because miter could not be unrolled.\n" ); + Abc_Print( 1, "Quitting refinement because miter could not be unrolled.\n" ); break; } assert( Gia_ManRegNum(pSrm) == 0 && Gia_ManPiNum(pSrm) == (Gia_ManPiNum(pAig) * nFramesReal) ); if ( pPars->fVerbose ) - printf( "Unrolled for %d frames.\n", nFramesReal ); + Abc_Print( 1, "Unrolled for %d frames.\n", nFramesReal ); // allocate room for simulation info vSimInfo = Vec_PtrAllocSimInfo( Gia_ManRegNum(pAig) + Gia_ManPiNum(pAig) * (nFramesReal + nAddFrames), pPars->nWords ); @@ -383,27 +386,27 @@ int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars ) pState->iPo = -1; if ( pPars->fVerbose ) { - printf( "BMC = %3d ", nPats ); + Abc_Print( 1, "BMC = %3d ", nPats ); Gia_ManEquivPrintClasses( pAig, 0, 0 ); } // write equivalence classes Gia_WriteAiger( pAig, "gore.aig", 0, 0 ); // reduce the model - pReduce = Gia_ManSpecReduce( pAig, 0, 0 ); + pReduce = Gia_ManSpecReduce( pAig, 0, 0, 0 ); if ( pReduce ) { pReduce = Gia_ManSeqStructSweep( pAux = pReduce, 1, 1, 0 ); Gia_ManStop( pAux ); Gia_WriteAiger( pReduce, "gsrm.aig", 0, 0 ); -// printf( "Speculatively reduced model was written into file \"%s\".\n", "gsrm.aig" ); +// Abc_Print( 1, "Speculatively reduced model was written into file \"%s\".\n", "gsrm.aig" ); // Gia_ManPrintStatsShort( pReduce ); Gia_ManStop( pReduce ); } if ( RetValue ) { - printf( "Cec_ManSeqSemiformal(): An output of the miter is asserted. Refinement stopped.\n" ); + Abc_Print( 1, "Cec_ManSeqSemiformal(): An output of the miter is asserted. Refinement stopped.\n" ); break; } // decide when to stop @@ -417,7 +420,7 @@ int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars ) { int nNonConsts = Cec_ManCountNonConstOutputs( pAig ); if ( nNonConsts ) - printf( "The number of POs that are not const-0 candidates = %d.\n", nNonConsts ); + Abc_Print( 1, "The number of POs that are not const-0 candidates = %d.\n", nNonConsts ); } return RetValue; } @@ -432,3 +435,5 @@ int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars ) //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/cec/cecSim.c b/src/aig/cec/cecSim.c index 61610a46..92f8fc2e 100644 --- a/src/aig/cec/cecSim.c +++ b/src/aig/cec/cecSim.c @@ -20,6 +20,9 @@ #include "cecInt.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -46,3 +49,5 @@ //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/cec/cecSolve.c b/src/aig/cec/cecSolve.c index fa10d222..dc1b88eb 100644 --- a/src/aig/cec/cecSolve.c +++ b/src/aig/cec/cecSolve.c @@ -20,6 +20,9 @@ #include "cecInt.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -188,7 +191,7 @@ void Cec_AddClausesSuper( Cec_ManSat_t * p, Gia_Obj_t * pNode, Vec_Ptr_t * vSupe pLits = ABC_ALLOC( int, nLits ); // suppose AND-gate is A & B = C // add !A => !C or A + !C - Vec_PtrForEachEntry( vSuper, pFanin, i ) + Vec_PtrForEachEntry( Gia_Obj_t *, vSuper, pFanin, i ) { pLits[0] = toLitCond(Cec_ObjSatNum(p,Gia_Regular(pFanin)), Gia_IsComplement(pFanin)); pLits[1] = toLitCond(Cec_ObjSatNum(p,pNode), 1); @@ -201,7 +204,7 @@ void Cec_AddClausesSuper( Cec_ManSat_t * p, Gia_Obj_t * pNode, Vec_Ptr_t * vSupe assert( RetValue ); } // add A & B => C or !A + !B + C - Vec_PtrForEachEntry( vSuper, pFanin, i ) + Vec_PtrForEachEntry( Gia_Obj_t *, vSuper, pFanin, i ) { pLits[i] = toLitCond(Cec_ObjSatNum(p,Gia_Regular(pFanin)), !Gia_IsComplement(pFanin)); if ( p->pPars->fPolarFlip ) @@ -320,7 +323,7 @@ void Cec_CnfNodeAddToSolver( Cec_ManSat_t * p, Gia_Obj_t * pObj ) vFrontier = Vec_PtrAlloc( 100 ); Cec_ObjAddToFrontier( p, pObj, vFrontier ); // explore nodes in the frontier - Vec_PtrForEachEntry( vFrontier, pNode, i ) + Vec_PtrForEachEntry( Gia_Obj_t *, vFrontier, pNode, i ) { // create the supergate assert( Cec_ObjSatNum(p,pNode) ); @@ -331,14 +334,14 @@ void Cec_CnfNodeAddToSolver( Cec_ManSat_t * p, Gia_Obj_t * pObj ) Vec_PtrPushUnique( p->vFanins, Gia_ObjFanin0( Gia_ObjFanin1(pNode) ) ); Vec_PtrPushUnique( p->vFanins, Gia_ObjFanin1( Gia_ObjFanin0(pNode) ) ); Vec_PtrPushUnique( p->vFanins, Gia_ObjFanin1( Gia_ObjFanin1(pNode) ) ); - Vec_PtrForEachEntry( p->vFanins, pFanin, k ) + Vec_PtrForEachEntry( Gia_Obj_t *, p->vFanins, pFanin, k ) Cec_ObjAddToFrontier( p, Gia_Regular(pFanin), vFrontier ); Cec_AddClausesMux( p, pNode ); } else { Cec_CollectSuper( pNode, fUseMuxes, p->vFanins ); - Vec_PtrForEachEntry( p->vFanins, pFanin, k ) + Vec_PtrForEachEntry( Gia_Obj_t *, p->vFanins, pFanin, k ) Cec_ObjAddToFrontier( p, Gia_Regular(pFanin), vFrontier ); Cec_AddClausesSuper( p, pNode, p->vFanins ); } @@ -366,7 +369,7 @@ void Cec_ManSatSolverRecycle( Cec_ManSat_t * p ) { Gia_Obj_t * pObj; int i; - Vec_PtrForEachEntry( p->vUsedNodes, pObj, i ) + Vec_PtrForEachEntry( Gia_Obj_t *, p->vUsedNodes, pObj, i ) Cec_ObjSetSatNum( p, pObj, 0 ); Vec_PtrClear( p->vUsedNodes ); // memset( p->pSatVars, 0, sizeof(int) * Gia_ManObjNumMax(p->pAigTotal) ); @@ -404,9 +407,9 @@ void Cec_SetActivityFactors_rec( Cec_ManSat_t * p, Gia_Obj_t * pObj, int LevelMi float dActConeBumpMax = 20.0; int iVar; // skip visited variables - if ( Gia_ObjIsTravIdCurrentArray(p->pAig, pObj) ) + if ( Gia_ObjIsTravIdCurrent(p->pAig, pObj) ) return; - Gia_ObjSetTravIdCurrentArray(p->pAig, pObj); + Gia_ObjSetTravIdCurrent(p->pAig, pObj); // add the PI to the list if ( Gia_ObjLevel(p->pAig, pObj) <= LevelMin || Gia_ObjIsCi(pObj) ) return; @@ -440,7 +443,7 @@ int Cec_SetActivityFactors( Cec_ManSat_t * p, Gia_Obj_t * pObj ) // reset the active variables veci_resize(&p->pSat->act_vars, 0); // prepare for traversal - Gia_ManIncrementTravIdArray( p->pAig ); + Gia_ManIncrementTravId( p->pAig ); // determine the min and max level to visit assert( dActConeRatio > 0 && dActConeRatio < 1 ); LevelMax = Gia_ObjLevel(p->pAig,pObj); @@ -491,7 +494,7 @@ int Cec_ManSatCheckNode( Cec_ManSat_t * p, Gia_Obj_t * pObj ) clk2 = clock(); Cec_CnfNodeAddToSolver( p, pObjR ); //ABC_PRT( "cnf", clock() - clk2 ); -//printf( "%d \n", p->pSat->size ); +//Abc_Print( 1, "%d \n", p->pSat->size ); clk2 = clock(); // Cec_SetActivityFactors( p, pObjR ); @@ -529,7 +532,7 @@ p->timeSatUnsat += clock() - clk; assert( RetValue ); p->nSatUnsat++; p->nConfUnsat += p->pSat->stats.conflicts - nConflicts; -//printf( "UNSAT after %d conflicts\n", p->pSat->stats.conflicts - nConflicts ); +//Abc_Print( 1, "UNSAT after %d conflicts\n", p->pSat->stats.conflicts - nConflicts ); return 1; } else if ( RetValue == l_True ) @@ -537,7 +540,7 @@ p->timeSatUnsat += clock() - clk; p->timeSatSat += clock() - clk; p->nSatSat++; p->nConfSat += p->pSat->stats.conflicts - nConflicts; -//printf( "SAT after %d conflicts\n", p->pSat->stats.conflicts - nConflicts ); +//Abc_Print( 1, "SAT after %d conflicts\n", p->pSat->stats.conflicts - nConflicts ); return 0; } else // if ( RetValue == l_Undef ) @@ -545,7 +548,7 @@ p->timeSatSat += clock() - clk; p->timeSatUndec += clock() - clk; p->nSatUndec++; p->nConfUndec += p->pSat->stats.conflicts - nConflicts; -//printf( "UNDEC after %d conflicts\n", p->pSat->stats.conflicts - nConflicts ); +//Abc_Print( 1, "UNDEC after %d conflicts\n", p->pSat->stats.conflicts - nConflicts ); return -1; } } @@ -591,7 +594,7 @@ clk2 = clock(); Cec_CnfNodeAddToSolver( p, pObjR1 ); Cec_CnfNodeAddToSolver( p, pObjR2 ); //ABC_PRT( "cnf", clock() - clk2 ); -//printf( "%d \n", p->pSat->size ); +//Abc_Print( 1, "%d \n", p->pSat->size ); clk2 = clock(); // Cec_SetActivityFactors( p, pObjR1 ); @@ -633,7 +636,7 @@ p->timeSatUnsat += clock() - clk; assert( RetValue ); p->nSatUnsat++; p->nConfUnsat += p->pSat->stats.conflicts - nConflicts; -//printf( "UNSAT after %d conflicts\n", p->pSat->stats.conflicts - nConflicts ); +//Abc_Print( 1, "UNSAT after %d conflicts\n", p->pSat->stats.conflicts - nConflicts ); return 1; } else if ( RetValue == l_True ) @@ -641,7 +644,7 @@ p->timeSatUnsat += clock() - clk; p->timeSatSat += clock() - clk; p->nSatSat++; p->nConfSat += p->pSat->stats.conflicts - nConflicts; -//printf( "SAT after %d conflicts\n", p->pSat->stats.conflicts - nConflicts ); +//Abc_Print( 1, "SAT after %d conflicts\n", p->pSat->stats.conflicts - nConflicts ); return 0; } else // if ( RetValue == l_Undef ) @@ -649,7 +652,7 @@ p->timeSatSat += clock() - clk; p->timeSatUndec += clock() - clk; p->nSatUndec++; p->nConfUndec += p->pSat->stats.conflicts - nConflicts; -//printf( "UNDEC after %d conflicts\n", p->pSat->stats.conflicts - nConflicts ); +//Abc_Print( 1, "UNDEC after %d conflicts\n", p->pSat->stats.conflicts - nConflicts ); return -1; } } @@ -683,7 +686,7 @@ void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPar } Gia_ManSetPhase( pAig ); Gia_ManLevelNum( pAig ); - Gia_ManResetTravIdArray( pAig ); + Gia_ManIncrementTravId( pAig ); p = Cec_ManSatCreate( pAig, pPars ); pProgress = Bar_ProgressStart( stdout, Gia_ManPoNum(pAig) ); Gia_ManForEachCo( pAig, pObj, i ) @@ -705,7 +708,7 @@ clk2 = clock(); Gia_Man_t * pTemp = Gia_ManDupDfsCone( pAig, pObj ); Gia_WriteAiger( pTemp, "gia_hard.aig", 0, 0 ); Gia_ManStop( pTemp ); - printf( "Dumping hard cone into file \"%s\".\n", "gia_hard.aig" ); + Abc_Print( 1, "Dumping hard cone into file \"%s\".\n", "gia_hard.aig" ); } */ if ( status != 0 ) @@ -759,12 +762,12 @@ Vec_Int_t * Cec_ManSatReadCex( Cec_ManSat_t * pSat ) ***********************************************************************/ void Cec_ManSatSolveSeq_rec( Cec_ManSat_t * pSat, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Ptr_t * vInfo, int iPat, int nRegs ) { - if ( Gia_ObjIsTravIdCurrentArray(p, pObj) ) + if ( Gia_ObjIsTravIdCurrent(p, pObj) ) return; - Gia_ObjSetTravIdCurrentArray(p, pObj); + Gia_ObjSetTravIdCurrent(p, pObj); if ( Gia_ObjIsCi(pObj) ) { - unsigned * pInfo = Vec_PtrEntry( vInfo, nRegs + Gia_ObjCioId(pObj) ); + unsigned * pInfo = (unsigned *)Vec_PtrEntry( vInfo, nRegs + Gia_ObjCioId(pObj) ); if ( Cec_ObjSatVarValue( pSat, pObj ) != Gia_InfoHasBit( pInfo, iPat ) ) Gia_InfoXorBit( pInfo, iPat ); pSat->nCexLits++; @@ -799,7 +802,7 @@ Vec_Str_t * Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat nPatsInit = nPats = 32 * Vec_PtrReadWordsSimInfo(vPatts); Gia_ManSetPhase( pAig ); Gia_ManLevelNum( pAig ); - Gia_ManResetTravIdArray( pAig ); + Gia_ManIncrementTravId( pAig ); p = Cec_ManSatCreate( pAig, pPars ); vStatus = Vec_StrAlloc( Gia_ManPoNum(pAig) ); pProgress = Bar_ProgressStart( stdout, Gia_ManPoNum(pAig) ); @@ -810,18 +813,18 @@ Vec_Str_t * Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat { if ( Gia_ObjFaninC0(pObj) ) { -// printf( "Constant 1 output of SRM!!!\n" ); +// Abc_Print( 1, "Constant 1 output of SRM!!!\n" ); Vec_StrPush( vStatus, 0 ); } else { -// printf( "Constant 0 output of SRM!!!\n" ); +// Abc_Print( 1, "Constant 0 output of SRM!!!\n" ); Vec_StrPush( vStatus, 1 ); } continue; } status = Cec_ManSatCheckNode( p, Gia_ObjChild0(pObj) ); -//printf( "output %d status = %d\n", i, status ); +//Abc_Print( 1, "output %d status = %d\n", i, status ); Vec_StrPush( vStatus, (char)status ); if ( status != 0 ) continue; @@ -836,7 +839,7 @@ Vec_Str_t * Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat if ( iPat % nPatsInit == 0 ) iPat++; // save the pattern - Gia_ManIncrementTravIdArray( pAig ); + Gia_ManIncrementTravId( pAig ); // Vec_IntClear( p->vCex ); Cec_ManSatSolveSeq_rec( p, pAig, Gia_ObjFanin0(pObj), vPatts, iPat++, nRegs ); // Gia_SatVerifyPattern( pAig, pObj, p->vCex, p->vVisits ); @@ -853,7 +856,7 @@ Vec_Str_t * Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat Bar_ProgressStop( pProgress ); if ( pPars->fVerbose ) Cec_ManSatPrintStats( p ); -// printf( "Total number of cex literals = %d. (Ave = %d)\n", p->nCexLits, p->nCexLits/p->nSatSat ); +// Abc_Print( 1, "Total number of cex literals = %d. (Ave = %d)\n", p->nCexLits, p->nCexLits/p->nSatSat ); Cec_ManSatStop( p ); if ( pnPats ) *pnPats = iPat-1; @@ -900,9 +903,9 @@ void Cec_ManSatAddToStore( Vec_Int_t * vCexStore, Vec_Int_t * vCex, int Out ) ***********************************************************************/ void Cec_ManSatSolveMiter_rec( Cec_ManSat_t * pSat, Gia_Man_t * p, Gia_Obj_t * pObj ) { - if ( Gia_ObjIsTravIdCurrentArray(p, pObj) ) + if ( Gia_ObjIsTravIdCurrent(p, pObj) ) return; - Gia_ObjSetTravIdCurrentArray(p, pObj); + Gia_ObjSetTravIdCurrent(p, pObj); if ( Gia_ObjIsCi(pObj) ) { pSat->nCexLits++; @@ -928,7 +931,7 @@ void Cec_ManSatSolveMiter_rec( Cec_ManSat_t * pSat, Gia_Man_t * p, Gia_Obj_t * p void Cec_ManSavePattern( Cec_ManSat_t * p, Gia_Obj_t * pObj1, Gia_Obj_t * pObj2 ) { Vec_IntClear( p->vCex ); - Gia_ManIncrementTravIdArray( p->pAig ); + Gia_ManIncrementTravId( p->pAig ); Cec_ManSatSolveMiter_rec( p, p->pAig, Gia_Regular(pObj1) ); if ( pObj2 ) Cec_ManSatSolveMiter_rec( p, p->pAig, Gia_Regular(pObj2) ); @@ -957,7 +960,7 @@ Vec_Int_t * Cec_ManSatSolveMiter( Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_St // prepare AIG Gia_ManSetPhase( pAig ); Gia_ManLevelNum( pAig ); - Gia_ManResetTravIdArray( pAig ); + Gia_ManIncrementTravId( pAig ); // create resulting data-structures vStatus = Vec_StrAlloc( Gia_ManPoNum(pAig) ); vCexStore = Vec_IntAlloc( 10000 ); @@ -972,13 +975,13 @@ Vec_Int_t * Cec_ManSatSolveMiter( Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_St { if ( Gia_ObjFaninC0(pObj) ) { -// printf( "Constant 1 output of SRM!!!\n" ); +// Abc_Print( 1, "Constant 1 output of SRM!!!\n" ); Cec_ManSatAddToStore( vCexStore, p->vCex, i ); // trivial counter-example Vec_StrPush( vStatus, 0 ); } else { -// printf( "Constant 0 output of SRM!!!\n" ); +// Abc_Print( 1, "Constant 0 output of SRM!!!\n" ); Vec_StrPush( vStatus, 1 ); } continue; @@ -994,7 +997,7 @@ Vec_Int_t * Cec_ManSatSolveMiter( Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_St continue; assert( status == 0 ); // save the pattern -// Gia_ManIncrementTravIdArray( pAig ); +// Gia_ManIncrementTravId( pAig ); // Cec_ManSatSolveMiter_rec( p, pAig, Gia_ObjFanin0(pObj) ); Cec_ManSavePattern( p, Gia_ObjFanin0(pObj), NULL ); // Gia_SatVerifyPattern( pAig, pObj, p->vCex, p->vVisits ); @@ -1015,3 +1018,5 @@ Vec_Int_t * Cec_ManSatSolveMiter( Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_St //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/cec/cecSweep.c b/src/aig/cec/cecSweep.c index 1b68efe0..97f5e36a 100644 --- a/src/aig/cec/cecSweep.c +++ b/src/aig/cec/cecSweep.c @@ -20,6 +20,9 @@ #include "cecInt.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -162,8 +165,8 @@ void Cec_ManFraCreateInfo( Cec_ManSim_t * p, Vec_Ptr_t * vCiInfo, Vec_Ptr_t * vI int i, w; for ( i = 0; i < Gia_ManCiNum(p->pAig); i++ ) { - pRes0 = Vec_PtrEntry( vCiInfo, i ); - pRes1 = Vec_PtrEntry( vInfo, i ); + pRes0 = (unsigned *)Vec_PtrEntry( vCiInfo, i ); + pRes1 = (unsigned *)Vec_PtrEntry( vInfo, i ); pRes1 += p->nWords * nSeries; for ( w = 0; w < p->nWords; w++ ) pRes0[w] = pRes1[w]; @@ -270,7 +273,7 @@ p->timeSim += clock() - clk; // if ( pObjOld->fMark0 == 0 ) { if ( iRepr == Gia_ObjRepr(p->pAig, iNode) ) - printf( "Cec_ManFraClassesUpdate(): Error! Node is not refined!\n" ); + Abc_Print( 1, "Cec_ManFraClassesUpdate(): Error! Node is not refined!\n" ); p->nAllDisproved++; } } @@ -292,3 +295,5 @@ p->timeSim += clock() - clk; //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/cec/cecSynth.c b/src/aig/cec/cecSynth.c new file mode 100644 index 00000000..52b50a43 --- /dev/null +++ b/src/aig/cec/cecSynth.c @@ -0,0 +1,380 @@ +/**CFile**************************************************************** + + FileName [cecSynth.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Combinational equivalence checking.] + + Synopsis [Partitioned sequential synthesis.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: cecSynth.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "cecInt.h" +#include "giaAig.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Populate sequential synthesis parameters.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cec_SeqSynthesisSetDefaultParams( Cec_ParSeq_t * p ) +{ + memset( p, 0, sizeof(Cec_ParSeq_t) ); + p->fUseLcorr = 0; // enables latch correspondence + p->fUseScorr = 0; // enables signal correspondence + p->nBTLimit = 1000; // (scorr/lcorr) conflict limit at a node + p->nFrames = 1; // (scorr only) the number of timeframes + p->nLevelMax = -1; // (scorr only) the max number of levels + p->fConsts = 1; // (scl only) merging constants + p->fEquivs = 1; // (scl only) merging equivalences + p->fUseMiniSat = 0; // enables MiniSat in lcorr/scorr + p->nMinDomSize = 100; // the size of minimum clock domain + p->fVeryVerbose = 0; // verbose stats + p->fVerbose = 0; // verbose stats +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cec_SeqReadMinDomSize( Cec_ParSeq_t * p ) +{ + return p->nMinDomSize; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cec_SeqReadVerbose( Cec_ParSeq_t * p ) +{ + return p->fVerbose; +} + +/**Function************************************************************* + + Synopsis [Computes partitioning of registers.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManRegCreatePart( Gia_Man_t * p, Vec_Int_t * vPart, int * pnCountPis, int * pnCountRegs, int ** ppMapBack ) +{ + Gia_Man_t * pNew; + Gia_Obj_t * pObj; + Vec_Int_t * vNodes, * vRoots; + int i, iOut, nCountPis, nCountRegs; + int * pMapBack; + // collect/mark nodes/PIs in the DFS order from the roots + Gia_ManIncrementTravId( p ); + vRoots = Vec_IntAlloc( Vec_IntSize(vPart) ); + Vec_IntForEachEntry( vPart, iOut, i ) + Vec_IntPush( vRoots, Gia_ObjId(p, Gia_ManCo(p, Gia_ManPoNum(p)+iOut)) ); + vNodes = Gia_ManCollectNodesCis( p, Vec_IntArray(vRoots), Vec_IntSize(vRoots) ); + Vec_IntFree( vRoots ); + // unmark register outputs + Vec_IntForEachEntry( vPart, iOut, i ) + Gia_ObjSetTravIdPrevious( p, Gia_ManCi(p, Gia_ManPiNum(p)+iOut) ); + // count pure PIs + nCountPis = nCountRegs = 0; + Gia_ManForEachPi( p, pObj, i ) + nCountPis += Gia_ObjIsTravIdCurrent(p, pObj); + // count outputs of other registers + Gia_ManForEachRo( p, pObj, i ) + nCountRegs += Gia_ObjIsTravIdCurrent(p, pObj); // should be !Gia_... ??? + if ( pnCountPis ) + *pnCountPis = nCountPis; + if ( pnCountRegs ) + *pnCountRegs = nCountRegs; + // clean old manager + Gia_ManFillValue(p); + Gia_ManConst0(p)->Value = 0; + // create the new manager + pNew = Gia_ManStart( Vec_IntSize(vNodes) ); + // create the PIs + Gia_ManForEachCi( p, pObj, i ) + if ( Gia_ObjIsTravIdCurrent(p, pObj) ) + pObj->Value = Gia_ManAppendCi(pNew); + // add variables for the register outputs + // create fake POs to hold the register outputs + Vec_IntForEachEntry( vPart, iOut, i ) + { + pObj = Gia_ManCi(p, Gia_ManPiNum(p)+iOut); + pObj->Value = Gia_ManAppendCi(pNew); + Gia_ManAppendCo( pNew, pObj->Value ); + Gia_ObjSetTravIdCurrent( p, pObj ); // added + } + // create the nodes + Gia_ManForEachObjVec( vNodes, p, pObj, i ) + if ( Gia_ObjIsAnd(pObj) ) + pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + // add real POs for the registers + Vec_IntForEachEntry( vPart, iOut, i ) + { + pObj = Gia_ManCo( p, Gia_ManPoNum(p)+iOut ); + Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + } + Gia_ManSetRegNum( pNew, Vec_IntSize(vPart) ); + // create map + if ( ppMapBack ) + { + pMapBack = ABC_FALLOC( int, Gia_ManObjNum(pNew) ); + // map constant nodes + pMapBack[0] = 0; + // logic cones of register outputs + Gia_ManForEachObjVec( vNodes, p, pObj, i ) + { +// pObjNew = Aig_Regular(pObj->pData); +// pMapBack[pObjNew->Id] = pObj->Id; + assert( Gia_Lit2Var(Gia_ObjValue(pObj)) >= 0 ); + assert( Gia_Lit2Var(Gia_ObjValue(pObj)) < Gia_ManObjNum(pNew) ); + pMapBack[ Gia_Lit2Var(Gia_ObjValue(pObj)) ] = Gia_ObjId(p, pObj); + } + // map register outputs + Vec_IntForEachEntry( vPart, iOut, i ) + { + pObj = Gia_ManCi(p, Gia_ManPiNum(p)+iOut); +// pObjNew = pObj->pData; +// pMapBack[pObjNew->Id] = pObj->Id; + assert( Gia_Lit2Var(Gia_ObjValue(pObj)) >= 0 ); + assert( Gia_Lit2Var(Gia_ObjValue(pObj)) < Gia_ManObjNum(pNew) ); + pMapBack[ Gia_Lit2Var(Gia_ObjValue(pObj)) ] = Gia_ObjId(p, pObj); + } + *ppMapBack = pMapBack; + } + Vec_IntFree( vNodes ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [Transfers the classes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_TransferMappedClasses( Gia_Man_t * pPart, int * pMapBack, int * pReprs ) +{ + Gia_Obj_t * pObj; + int i, Id1, Id2, nClasses; + if ( pPart->pReprs == NULL ) + return 0; + nClasses = 0; + Gia_ManForEachObj( pPart, pObj, i ) + { + if ( Gia_ObjRepr(pPart, i) == GIA_VOID ) + continue; + assert( i < Gia_ManObjNum(pPart) ); + assert( Gia_ObjRepr(pPart, i) < Gia_ManObjNum(pPart) ); + Id1 = pMapBack[ i ]; + Id2 = pMapBack[ Gia_ObjRepr(pPart, i) ]; + if ( Id1 == Id2 ) + continue; + if ( Id1 < Id2 ) + pReprs[Id2] = Id1; + else + pReprs[Id1] = Id2; + nClasses++; + } + return nClasses; +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManFindRepr_rec( int * pReprs, int Id ) +{ + if ( pReprs[Id] == 0 ) + return 0; + if ( pReprs[Id] == ~0 ) + return Id; + return Gia_ManFindRepr_rec( pReprs, pReprs[Id] ); +} + +/**Function************************************************************* + + Synopsis [Normalizes equivalences.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManNormalizeEquivalences( Gia_Man_t * p, int * pReprs ) +{ + int i, iRepr; + assert( p->pReprs == NULL ); + assert( p->pNexts == NULL ); + p->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) ); + for ( i = 0; i < Gia_ManObjNum(p); i++ ) + Gia_ObjSetRepr( p, i, GIA_VOID ); + for ( i = 0; i < Gia_ManObjNum(p); i++ ) + { + if ( pReprs[i] == ~0 ) + continue; + iRepr = Gia_ManFindRepr_rec( pReprs, i ); + Gia_ObjSetRepr( p, i, iRepr ); + } + p->pNexts = Gia_ManDeriveNexts( p ); +} + +/**Function************************************************************* + + Synopsis [Partitioned sequential synthesis.] + + Description [Returns AIG annotated with equivalence classes.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cec_SequentialSynthesisPart( Gia_Man_t * p, Cec_ParSeq_t * pPars ) +{ + int fPrintParts = 0; + char Buffer[100]; + Gia_Man_t * pTemp; + Vec_Ptr_t * vParts = (Vec_Ptr_t *)p->vClockDoms; + Vec_Int_t * vPart; + int * pMapBack, * pReprs; + int i, nCountPis, nCountRegs; + int nClasses, clk = clock(); + + // save parameters + if ( fPrintParts ) + { + // print partitions + Abc_Print( 1, "The following clock domains are used:\n" ); + Vec_PtrForEachEntry( Vec_Int_t *, vParts, vPart, i ) + { + pTemp = Gia_ManRegCreatePart( p, vPart, &nCountPis, &nCountRegs, NULL ); + sprintf( Buffer, "part%03d.aig", i ); + Gia_WriteAiger( pTemp, Buffer, 0, 0 ); + Abc_Print( 1, "part%03d.aig : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d.\n", + i, Vec_IntSize(vPart), Gia_ManCiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Gia_ManAndNum(pTemp) ); + Gia_ManStop( pTemp ); + } + } + + // perform sequential synthesis for clock domains + pReprs = ABC_FALLOC( int, Gia_ManObjNum(p) ); + Vec_PtrForEachEntry( Vec_Int_t *, vParts, vPart, i ) + { + pTemp = Gia_ManRegCreatePart( p, vPart, &nCountPis, &nCountRegs, &pMapBack ); + if ( nCountPis > 0 ) + { + if ( pPars->fUseScorr ) + { + Cec_ParCor_t CorPars, * pCorPars = &CorPars; + Cec_ManCorSetDefaultParams( pCorPars ); + pCorPars->nBTLimit = pPars->nBTLimit; + pCorPars->nLevelMax = pPars->nLevelMax; + pCorPars->fVerbose = pPars->fVeryVerbose; + pCorPars->fUseCSat = 1; + Cec_ManLSCorrespondenceClasses( pTemp, pCorPars ); + } + else if ( pPars->fUseLcorr ) + { + Cec_ParCor_t CorPars, * pCorPars = &CorPars; + Cec_ManCorSetDefaultParams( pCorPars ); + pCorPars->fLatchCorr = 1; + pCorPars->nBTLimit = pPars->nBTLimit; + pCorPars->fVerbose = pPars->fVeryVerbose; + pCorPars->fUseCSat = 1; + Cec_ManLSCorrespondenceClasses( pTemp, pCorPars ); + } + else + { +// pNew = Gia_ManSeqStructSweep( pTemp, pPars->fConsts, pPars->fEquivs, pPars->fVerbose ); +// Gia_ManStop( pNew ); + Gia_ManSeqCleanupClasses( pTemp, pPars->fConsts, pPars->fEquivs, pPars->fVerbose ); + } +//Abc_Print( 1, "Part equivalences = %d.\n", Gia_ManEquivCountLitsAll(pTemp) ); + nClasses = Gia_TransferMappedClasses( pTemp, pMapBack, pReprs ); + if ( pPars->fVerbose ) + { + Abc_Print( 1, "%3d : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d. Cl = %5d.\n", + i, Vec_IntSize(vPart), Gia_ManCiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Gia_ManAndNum(pTemp), nClasses ); + } + } + Gia_ManStop( pTemp ); + ABC_FREE( pMapBack ); + } + + // generate resulting equivalences + Gia_ManNormalizeEquivalences( p, pReprs ); +//Abc_Print( 1, "Total equivalences = %d.\n", Gia_ManEquivCountLitsAll(p) ); + ABC_FREE( pReprs ); + if ( pPars->fVerbose ) + { + Abc_PrintTime( 1, "Total time", clock() - clk ); + } + return 1; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/cec/module.make b/src/aig/cec/module.make index 35a18cae..42e0cd1b 100644 --- a/src/aig/cec/module.make +++ b/src/aig/cec/module.make @@ -9,4 +9,5 @@ SRC += src/aig/cec/cecCec.c \ src/aig/cec/cecSeq.c \ src/aig/cec/cecSim.c \ src/aig/cec/cecSolve.c \ + src/aig/cec/cecSynth.c \ src/aig/cec/cecSweep.c |