diff options
Diffstat (limited to 'src/aig')
-rw-r--r-- | src/aig/cec/cec.h | 23 | ||||
-rw-r--r-- | src/aig/cec/cecCec.c | 4 | ||||
-rw-r--r-- | src/aig/cec/cecClass.c | 124 | ||||
-rw-r--r-- | src/aig/cec/cecCore.c | 53 | ||||
-rw-r--r-- | src/aig/cec/cecInt.h | 7 | ||||
-rw-r--r-- | src/aig/cec/cecMan.c | 2 | ||||
-rw-r--r-- | src/aig/cec/cecSeq.c | 314 | ||||
-rw-r--r-- | src/aig/cec/cecSolve.c | 79 | ||||
-rw-r--r-- | src/aig/cec/cecSweep.c | 2 | ||||
-rw-r--r-- | src/aig/cec/module.make | 1 | ||||
-rw-r--r-- | src/aig/cec2/cec.h | 104 | ||||
-rw-r--r-- | src/aig/cec2/cecAig.c | 168 | ||||
-rw-r--r-- | src/aig/cec2/cecClass.c | 571 | ||||
-rw-r--r-- | src/aig/cec2/cecCnf.c | 328 | ||||
-rw-r--r-- | src/aig/cec2/cecCore.c | 245 | ||||
-rw-r--r-- | src/aig/cec2/cecInt.h | 208 | ||||
-rw-r--r-- | src/aig/cec2/cecMan.c | 59 | ||||
-rw-r--r-- | src/aig/cec2/cecSat.c | 250 | ||||
-rw-r--r-- | src/aig/cec2/cecSat2.c | 284 | ||||
-rw-r--r-- | src/aig/cec2/cecSim.c | 447 | ||||
-rw-r--r-- | src/aig/cec2/cecStatus.c | 187 | ||||
-rw-r--r-- | src/aig/cec2/cecSweep.c | 582 | ||||
-rw-r--r-- | src/aig/cec2/module.make | 9 | ||||
-rw-r--r-- | src/aig/gia/gia.h | 13 | ||||
-rw-r--r-- | src/aig/gia/giaDup.c | 90 | ||||
-rw-r--r-- | src/aig/gia/giaEquiv.c | 225 | ||||
-rw-r--r-- | src/aig/gia/giaUtil.c | 57 |
27 files changed, 881 insertions, 3555 deletions
diff --git a/src/aig/cec/cec.h b/src/aig/cec/cec.h index 16748233..a97bd958 100644 --- a/src/aig/cec/cec.h +++ b/src/aig/cec/cec.h @@ -57,7 +57,7 @@ struct Cec_ParSim_t_ int nWords; // the number of simulation words int nRounds; // the number of simulation rounds int TimeLimit; // the runtime limit in seconds - int fDoubleOuts; // miter with separate outputs + int fDualOut; // miter with separate outputs int fCheckMiter; // the circuit is the miter int fFirstStop; // stop on the first sat output int fSeqSimulate; // performs sequential simulation @@ -65,6 +65,21 @@ struct Cec_ParSim_t_ int fVerbose; // verbose stats }; +// semiformal parameters +typedef struct Cec_ParSmf_t_ Cec_ParSmf_t; +struct Cec_ParSmf_t_ +{ + int nWords; // the number of simulation words + int nRounds; // the number of simulation rounds + int nFrames; // the number of time frames + int nBTLimit; // conflict limit at a node + int TimeLimit; // the runtime limit in seconds + int fDualOut; // miter with separate outputs + int fCheckMiter; // the circuit is the miter + int fFirstStop; // stop on the first sat output + int fVerbose; // verbose stats +}; + // combinational SAT sweeping parameters typedef struct Cec_ParFra_t_ Cec_ParFra_t; struct Cec_ParFra_t_ @@ -79,7 +94,7 @@ struct Cec_ParFra_t_ int fRewriting; // enables AIG rewriting int fCheckMiter; // the circuit is the miter int fFirstStop; // stop on the first sat output - int fDoubleOuts; // miter with separate outputs + int fDualOut; // miter with separate outputs int fColorDiff; // miter with separate outputs int fVeryVerbose; // verbose stats int fVerbose; // verbose stats @@ -112,11 +127,15 @@ extern int Cec_ManVerifyTwo( Gia_Man_t * p0, Gia_Man_t * p1, int fVerb /*=== cecCore.c ==========================================================*/ extern void Cec_ManSatSetDefaultParams( Cec_ParSat_t * p ); extern void Cec_ManSimSetDefaultParams( Cec_ParSim_t * p ); +extern void Cec_ManSmfSetDefaultParams( Cec_ParSmf_t * p ); extern void Cec_ManFraSetDefaultParams( Cec_ParFra_t * p ); extern void Cec_ManCecSetDefaultParams( Cec_ParCec_t * p ); 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_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars ); #ifdef __cplusplus } diff --git a/src/aig/cec/cecCec.c b/src/aig/cec/cecCec.c index ea730693..96bddbcb 100644 --- a/src/aig/cec/cecCec.c +++ b/src/aig/cec/cecCec.c @@ -134,7 +134,7 @@ int Cec_ManVerify( Gia_Man_t * p, Cec_ParCec_t * pPars ) pParsFra->fVerbose = pPars->fVerbose; pParsFra->fCheckMiter = 1; pParsFra->fFirstStop = 1; - pParsFra->fDoubleOuts = 1; + pParsFra->fDualOut = 1; pNew = Cec_ManSatSweeping( p, pParsFra ); if ( pNew == NULL ) { @@ -192,7 +192,7 @@ int Cec_ManVerifyTwo( Gia_Man_t * p0, Gia_Man_t * p1, int fVerbose ) int RetValue; Cec_ManCecSetDefaultParams( pPars ); pPars->fVerbose = fVerbose; - pMiter = Gia_ManMiter( p0, p1, 0, 1, pPars->fVerbose ); + pMiter = Gia_ManMiter( p0, p1, 1, 0, pPars->fVerbose ); if ( pMiter == NULL ) return -1; RetValue = Cec_ManVerify( pMiter, pPars ); diff --git a/src/aig/cec/cecClass.c b/src/aig/cec/cecClass.c index aaa85ffa..0cac88af 100644 --- a/src/aig/cec/cecClass.c +++ b/src/aig/cec/cecClass.c @@ -155,6 +155,70 @@ int Cec_ManSimCompareEqualFirstBit( unsigned * p0, unsigned * p1, int nWords ) /**Function************************************************************* + Synopsis [Returns the number of the first non-equal bit.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cec_ManSimCompareConstScore( unsigned * p, int nWords, int * pScores ) +{ + int w, b; + if ( p[0] & 1 ) + { + for ( w = 0; w < nWords; w++ ) + if ( p[w] != ~0 ) + for ( b = 0; b < 32; b++ ) + if ( ((~p[w]) >> b ) & 1 ) + pScores[32*w + b]++; + } + else + { + for ( w = 0; w < nWords; w++ ) + if ( p[w] != 0 ) + for ( b = 0; b < 32; b++ ) + if ( ((p[w]) >> b ) & 1 ) + pScores[32*w + b]++; + } +} + +/**Function************************************************************* + + Synopsis [Compares simulation info of two nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cec_ManSimCompareEqualScore( unsigned * p0, unsigned * p1, int nWords, int * pScores ) +{ + int w, b; + if ( (p0[0] & 1) == (p1[0] & 1) ) + { + for ( w = 0; w < nWords; w++ ) + if ( p0[w] != p1[w] ) + for ( b = 0; b < 32; b++ ) + if ( ((p0[w] ^ p1[w]) >> b ) & 1 ) + pScores[32*w + b]++; + } + else + { + for ( w = 0; w < nWords; w++ ) + if ( p0[w] != ~p1[w] ) + for ( b = 0; b < 32; b++ ) + if ( ((p0[w] ^ ~p1[w]) >> b ) & 1 ) + pScores[32*w + b]++; + } +} + +/**Function************************************************************* + Synopsis [Creates equivalence class.] Description [] @@ -211,7 +275,11 @@ int Cec_ManSimClassRefineOne( Cec_ManSim_t * p, int i ) if ( Cec_ManSimCompareEqual( pSim0, pSim1, p->nWords ) ) Vec_IntPush( p->vClassOld, Ent ); else + { Vec_IntPush( p->vClassNew, Ent ); + if ( p->pBestState ) + Cec_ManSimCompareEqualScore( pSim0, pSim1, p->nWords, p->pScores ); + } } if ( Vec_IntSize( p->vClassNew ) == 0 ) return 0; @@ -422,6 +490,42 @@ void Cec_ManSimSavePattern( Cec_ManSim_t * p, int iPat ) /**Function************************************************************* + Synopsis [Find the best pattern using the scores.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cec_ManSimFindBestPattern( Cec_ManSim_t * p ) +{ + unsigned * pInfo; + int i, ScoreBest = 0, iPatBest = 1; + // find the best pattern + for ( i = 0; i < 32 * p->nWords; i++ ) + if ( ScoreBest < p->pScores[i] ) + { + ScoreBest = p->pScores[i]; + iPatBest = i; + } + // compare this with the available patterns - and save + if ( p->pBestState->iPo <= ScoreBest ) + { + 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 ); + if ( Aig_InfoHasBit(p->pBestState->pData, i) != Aig_InfoHasBit(pInfo, iPatBest) ) + Aig_InfoXorBit( p->pBestState->pData, i ); + } + p->pBestState->iPo = ScoreBest; + } +} + +/**Function************************************************************* + Synopsis [Returns 1 if computation should stop.] Description [] @@ -435,10 +539,11 @@ int Cec_ManSimAnalyzeOutputs( Cec_ManSim_t * p ) { unsigned * pInfo, * pInfo2; int i; - if ( p->vCoSimInfo == NULL ) + if ( !p->pPars->fCheckMiter ) return 0; + assert( p->vCoSimInfo != NULL ); // compare outputs with 0 - if ( p->pPars->fDoubleOuts ) + if ( p->pPars->fDualOut ) { assert( (Gia_ManCoNum(p->pAig) & 1) == 0 ); for ( i = 0; i < Gia_ManCoNum(p->pAig); i++ ) @@ -507,6 +612,10 @@ int Cec_ManSimSimulateRound( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t * if ( p->nWordsOld != p->nWords ) Cec_ManSimMemRelink( p ); p->nMemsMax = 0; + // allocate score counters + ABC_FREE( p->pScores ); + if ( p->pBestState ) + p->pScores = ABC_CALLOC( int, 32 * p->nWords ); // simulate nodes Vec_IntClear( p->vRefinedC ); if ( Gia_ObjValue(Gia_ManConst0(p->pAig)) ) @@ -583,6 +692,8 @@ references: { pRes[0]++; Vec_IntPush( p->vRefinedC, i ); + if ( p->pBestState ) + Cec_ManSimCompareConstScore( pRes + 1, p->nWords, p->pScores ); } // if the node belongs to a class, save it if ( Gia_ObjIsClass(p->pAig, i) ) @@ -607,6 +718,8 @@ references: printf( "Cec_ManSimSimulateRound(): Memory management error!\n" ); if ( p->pPars->fVeryVerbose ) Gia_ManEquivPrintClasses( p->pAig, 0, Cec_MemUsage(p) ); + if ( p->pBestState ) + Cec_ManSimFindBestPattern( p ); /* if ( p->nMems > 1 ) { for ( i = 1; i < p->nObjs; i++ ) @@ -682,8 +795,13 @@ int Cec_ManSimClassesPrepare( Cec_ManSim_t * p ) // allocate representation p->pAig->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p->pAig) ); p->pAig->pNexts = ABC_CALLOC( int, Gia_ManObjNum(p->pAig) ); + // set starting representative of internal nodes to be constant 0 Gia_ManForEachObj( p->pAig, pObj, i ) - Gia_ObjSetRepr( p->pAig, i, (Gia_ObjIsAnd(pObj) || Gia_ObjIsCi(pObj)) ? 0 : GIA_VOID ); + Gia_ObjSetRepr( p->pAig, i, Gia_ObjIsAnd(pObj) ? 0 : GIA_VOID ); + // if sequential simulation, set starting representative of ROs to be constant 0 + if ( p->pPars->fSeqSimulate ) + Gia_ManForEachRo( p->pAig, pObj, i ) + Gia_ObjSetRepr( p->pAig, Gia_ObjId(p->pAig, pObj), 0 ); // perform simulation Gia_ManSetRefs( p->pAig ); p->nWords = 1; diff --git a/src/aig/cec/cecCore.c b/src/aig/cec/cecCore.c index e25ddc90..061c3a7d 100644 --- a/src/aig/cec/cecCore.c +++ b/src/aig/cec/cecCore.c @@ -70,12 +70,37 @@ void Cec_ManSimSetDefaultParams( Cec_ParSim_t * p ) p->TimeLimit = 0; // the runtime limit in seconds p->fCheckMiter = 0; // the circuit is the miter p->fFirstStop = 0; // stop on the first sat output - p->fDoubleOuts = 0; // miter with separate outputs + p->fDualOut = 0; // miter with separate outputs p->fSeqSimulate = 0; // performs sequential simulation p->fVeryVerbose = 0; // verbose stats p->fVerbose = 0; // verbose stats } - + +/**Function************ ************************************************* + + Synopsis [This procedure sets default parameters.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cec_ManSmfSetDefaultParams( Cec_ParSmf_t * p ) +{ + memset( p, 0, sizeof(Cec_ParSmf_t) ); + p->nWords = 15; // the number of simulation words + p->nRounds = 15; // the number of simulation rounds + p->nFrames = 2; // the number of time frames + p->nBTLimit = 1000; // conflict limit at a node + p->TimeLimit = 0; // the runtime limit in seconds + p->fDualOut = 0; // miter with separate outputs + p->fCheckMiter = 0; // the circuit is the miter + p->fFirstStop = 0; // stop on the first sat output + p->fVerbose = 0; // verbose stats +} + /**Function************ ************************************************* Synopsis [This procedure sets default parameters.] @@ -100,7 +125,7 @@ void Cec_ManFraSetDefaultParams( Cec_ParFra_t * p ) p->fRewriting = 0; // enables AIG rewriting p->fCheckMiter = 0; // the circuit is the miter p->fFirstStop = 0; // stop on the first sat output - p->fDoubleOuts = 0; // miter with separate outputs + p->fDualOut = 0; // miter with separate outputs p->fColorDiff = 0; // miter with separate outputs p->fVeryVerbose = 0; // verbose stats p->fVerbose = 0; // verbose stats @@ -177,7 +202,8 @@ void Cec_ManSimulation( Gia_Man_t * pAig, Cec_ParSim_t * pPars ) if ( pPars->fCheckMiter ) printf( "The number of failed outputs of the miter = %6d. (Words = %4d. Rounds = %4d.)\n", pSim->iOut, pSim->nOuts, pPars->nWords, pPars->nRounds ); - ABC_PRT( "Time", clock() - clkTotal ); + if ( pPars->fVerbose ) + ABC_PRT( "Time", clock() - clkTotal ); Cec_ManSimStop( pSim ); } @@ -213,7 +239,7 @@ Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars ) // prepare the managers // SAT sweeping p = Cec_ManFraStart( pIni, pPars ); - if ( pPars->fDoubleOuts ) + if ( pPars->fDualOut ) pPars->fColorDiff = 1; // simulation Cec_ManSimSetDefaultParams( pParsSim ); @@ -221,10 +247,9 @@ Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars ) pParsSim->nRounds = pPars->nRounds; pParsSim->fCheckMiter = pPars->fCheckMiter; pParsSim->fFirstStop = pPars->fFirstStop; - pParsSim->fDoubleOuts = pPars->fDoubleOuts; + pParsSim->fDualOut = pPars->fDualOut; pParsSim->fVerbose = pPars->fVerbose; pSim = Cec_ManSimStart( p->pAig, pParsSim ); - pSim->nWords = p->pPars->nWords; // SAT solving Cec_ManSatSetDefaultParams( pParsSat ); pParsSat->nBTLimit = pPars->nBTLimit; @@ -250,7 +275,7 @@ p->timeSim += clock() - clk; { clk2 = clock(); nMatches = 0; - if ( pPars->fDoubleOuts ) + if ( pPars->fDualOut ) { nMatches = Gia_ManEquivSetColors( p->pAig, pPars->fVeryVerbose ); // p->pAig->pIso = Cec_ManDetectIsomorphism( p->pAig ); @@ -264,7 +289,7 @@ p->timeSim += clock() - clk; Gia_ManStop( pSrm ); if ( p->pPars->fVerbose ) printf( "Considered all available candidate equivalences.\n" ); - if ( pPars->fDoubleOuts && Gia_ManAndNum(p->pAig) > 0 ) + if ( pPars->fDualOut && Gia_ManAndNum(p->pAig) > 0 ) { if ( pPars->fColorDiff ) { @@ -276,7 +301,7 @@ p->timeSim += clock() - clk; { if ( p->pPars->fVerbose ) printf( "Switching into normal mode.\n" ); - pPars->fDoubleOuts = 0; + pPars->fDualOut = 0; } continue; } @@ -295,7 +320,7 @@ p->timeSat += clock() - clk; Gia_ManStop( pSrm ); // update the manager - pSim->pAig = p->pAig = Gia_ManEquivReduceAndRemap( pTemp = p->pAig, 0, pParsSim->fDoubleOuts ); + pSim->pAig = p->pAig = Gia_ManEquivReduceAndRemap( pTemp = p->pAig, 0, pParsSim->fDualOut ); Gia_ManStop( pTemp ); if ( p->pPars->fVerbose ) { @@ -332,18 +357,18 @@ p->timeSat += clock() - clk; } } } - if ( pPars->fDoubleOuts && pPars->fColorDiff && Gia_ManAndNum(p->pAig) < 100000 ) + if ( pPars->fDualOut && pPars->fColorDiff && Gia_ManAndNum(p->pAig) < 100000 ) { if ( p->pPars->fVerbose ) printf( "Switching into reduced mode.\n" ); pPars->fColorDiff = 0; } - if ( pPars->fDoubleOuts && Gia_ManAndNum(p->pAig) < 20000 ) + if ( pPars->fDualOut && Gia_ManAndNum(p->pAig) < 20000 ) { if ( p->pPars->fVerbose ) printf( "Switching into normal mode.\n" ); pPars->fColorDiff = 0; - pPars->fDoubleOuts = 0; + pPars->fDualOut = 0; } } finalize: diff --git a/src/aig/cec/cecInt.h b/src/aig/cec/cecInt.h index 1898b07c..ae4c6ff4 100644 --- a/src/aig/cec/cecInt.h +++ b/src/aig/cec/cecInt.h @@ -117,13 +117,17 @@ struct Cec_ManSim_t_ int nMemsMax; // the max number of used entries int MemFree; // next free entry int nWordsOld; // the number of simulation words after previous relink - // bug catcher + // internal simulation info Vec_Ptr_t * vCiSimInfo; // CI simulation info Vec_Ptr_t * vCoSimInfo; // CO simulation info + // counter examples 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 + // scoring simulation patterns + int * pScores; // counters of refinement for each pattern // temporaries Vec_Int_t * vClassOld; // old class numbers Vec_Int_t * vClassNew; // new class numbers @@ -182,6 +186,7 @@ extern Vec_Ptr_t * Cec_ManPatCollectPatterns( Cec_ManPat_t * pMan, int /*=== cecSolve.c ============================================================*/ extern int Cec_ObjSatVarValue( Cec_ManSat_t * p, Gia_Obj_t * pObj ); extern void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars ); +extern void Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat_t * pPars, int nRegs, int * pnPats ); /*=== ceFraeep.c ============================================================*/ 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 ); diff --git a/src/aig/cec/cecMan.c b/src/aig/cec/cecMan.c index 1a94409f..14f2493e 100644 --- a/src/aig/cec/cecMan.c +++ b/src/aig/cec/cecMan.c @@ -193,6 +193,7 @@ Cec_ManSim_t * Cec_ManSimStart( Gia_Man_t * pAig, Cec_ParSim_t * pPars ) memset( p, 0, sizeof(Cec_ManSim_t) ); p->pAig = pAig; p->pPars = pPars; + p->nWords = pPars->nWords; p->pSimInfo = ABC_CALLOC( int, Gia_ManObjNum(pAig) ); p->vClassOld = Vec_IntAlloc( 1000 ); p->vClassNew = Vec_IntAlloc( 1000 ); @@ -229,6 +230,7 @@ void Cec_ManSimStop( Cec_ManSim_t * p ) Vec_PtrFree( p->vCiSimInfo ); if ( p->vCoSimInfo ) Vec_PtrFree( p->vCoSimInfo ); + ABC_FREE( p->pScores ); ABC_FREE( p->pCexComb ); ABC_FREE( p->pCexes ); ABC_FREE( p->pMems ); diff --git a/src/aig/cec/cecSeq.c b/src/aig/cec/cecSeq.c new file mode 100644 index 00000000..6cb229ae --- /dev/null +++ b/src/aig/cec/cecSeq.c @@ -0,0 +1,314 @@ +/**CFile**************************************************************** + + FileName [cecSeq.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Combinatinoal equivalence checking.] + + Synopsis [Refinement of sequential equivalence classes.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: cecSeq.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "cecInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Sets register values from the counter-example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cec_ManSeqDeriveInfoFromCex( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Gia_Cex_t * pCex ) +{ + unsigned * pInfo; + int k, w, nWords; + assert( pCex->nBits == pCex->nRegs + pCex->nPis * (pCex->iFrame + 1) ); + assert( pCex->nBits <= Vec_PtrSize(vInfo) ); + nWords = Vec_PtrReadWordsSimInfo( vInfo ); + for ( k = 0; k < pCex->nRegs; k++ ) + { + pInfo = Vec_PtrEntry( vInfo, k ); + for ( w = 0; w < nWords; w++ ) + pInfo[w] = Aig_InfoHasBit( pCex->pData, k )? ~0 : 0; + } + for ( ; k < pCex->nBits; k++ ) + { + pInfo = Vec_PtrEntry( vInfo, k ); + for ( w = 0; w < nWords; w++ ) + pInfo[w] = Aig_ManRandom(0); + // set simulation pattern and make sure it is second (first will be erased during simulation) + pInfo[0] = (pInfo[0] << 1) | Aig_InfoHasBit( pCex->pData, k ); + pInfo[0] <<= 1; + } + for ( ; k < Vec_PtrSize(vInfo); k++ ) + { + pInfo = Vec_PtrEntry( vInfo, k ); + for ( w = 0; w < nWords; w++ ) + pInfo[w] = Aig_ManRandom(0); + } +} + +/**Function************************************************************* + + Synopsis [Sets register values from the counter-example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cec_ManSeqDeriveInfoInitRandom( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Gia_Cex_t * pCex ) +{ + unsigned * pInfo; + int k, w, nWords; + nWords = Vec_PtrReadWordsSimInfo( vInfo ); + assert( Gia_ManRegNum(pAig) == pCex->nRegs ); + assert( Gia_ManRegNum(pAig) <= Vec_PtrSize(vInfo) ); + for ( k = 0; k < Gia_ManRegNum(pAig); k++ ) + { + pInfo = Vec_PtrEntry( vInfo, k ); + for ( w = 0; w < nWords; w++ ) + pInfo[w] = Aig_InfoHasBit( pCex->pData, k )? ~0 : 0; + } + + for ( ; k < Vec_PtrSize(vInfo); k++ ) + { + pInfo = Vec_PtrEntry( vInfo, k ); + for ( w = 0; w < nWords; w++ ) + pInfo[w] = Aig_ManRandom( 0 ); + } +} + +/**Function************************************************************* + + Synopsis [Resimulates the classes using sequential simulation info.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cec_ManSeqResimulate( Cec_ManSim_t * p, Vec_Ptr_t * vInfo ) +{ + unsigned * pInfo0, * pInfo1; + int f, i, k, w, RetValue = 0; + assert( Gia_ManRegNum(p->pAig) > 0 ); + assert( Vec_PtrSize(vInfo) == Gia_ManRegNum(p->pAig) + Gia_ManPiNum(p->pAig) * p->pPars->nRounds ); + for ( k = 0; k < Gia_ManRegNum(p->pAig); k++ ) + { + pInfo0 = Vec_PtrEntry( vInfo, k ); + pInfo1 = Vec_PtrEntry( p->vCoSimInfo, Gia_ManPoNum(p->pAig) + k ); + for ( w = 0; w < p->nWords; w++ ) + pInfo1[w] = pInfo0[w]; + } + for ( f = 0; f < p->pPars->nRounds; f++ ) + { + for ( i = 0; i < Gia_ManPiNum(p->pAig); i++ ) + { + pInfo0 = Vec_PtrEntry( vInfo, k++ ); + pInfo1 = 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 ); + for ( w = 0; w < p->nWords; w++ ) + pInfo1[w] = pInfo0[w]; + } + if ( Cec_ManSimSimulateRound( p, p->vCiSimInfo, p->vCoSimInfo ) ) + { + printf( "One of the outputs of the miter is asserted.\n" ); + RetValue = 1; + } + } + assert( k == Vec_PtrSize(vInfo) ); + return RetValue; +} + +/**Function************************************************************* + + Synopsis [Resimulates information to refine equivalence classes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cec_ManSeqResimulateInfo( Gia_Man_t * pAig, Vec_Ptr_t * vSimInfo, Gia_Cex_t * pBestState ) +{ + Cec_ParSim_t ParsSim, * pParsSim = &ParsSim; + Cec_ManSim_t * pSim; + int RetValue, clkTotal = clock(); + assert( (Vec_PtrSize(vSimInfo) - Gia_ManRegNum(pAig)) % Gia_ManPiNum(pAig) == 0 ); + Cec_ManSimSetDefaultParams( pParsSim ); + pParsSim->nRounds = (Vec_PtrSize(vSimInfo) - Gia_ManRegNum(pAig)) / Gia_ManPiNum(pAig); + pParsSim->nWords = Vec_PtrReadWordsSimInfo( vSimInfo ); + Gia_ManSetRefs( pAig ); + pSim = Cec_ManSimStart( pAig, pParsSim ); + if ( pBestState ) + pSim->pBestState = pBestState; + RetValue = Cec_ManSeqResimulate( pSim, vSimInfo ); + pSim->pBestState = NULL; + Cec_ManSimStop( pSim ); + return RetValue; +} + +/**Function************************************************************* + + Synopsis [Resimuates one counter-example to refine equivalence classes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cec_ManSeqResimulateCounter( Gia_Man_t * pAig, Cec_ParSim_t * pPars, Gia_Cex_t * pCex ) +{ + Vec_Ptr_t * vSimInfo; + int RetValue, clkTotal = clock(); + if ( pCex == NULL ) + { + printf( "Cec_ManSeqResimulateCounter(): Counter-example is not available.\n" ); + return -1; + } + if ( pAig->pReprs == NULL ) + { + printf( "Cec_ManSeqResimulateCounter(): Equivalence classes are not available.\n" ); + return -1; + } + if ( Gia_ManRegNum(pAig) == 0 ) + { + printf( "Cec_ManSeqResimulateCounter(): Not a sequential AIG.\n" ); + return -1; + } + if ( Gia_ManRegNum(pAig) != pCex->nRegs || Gia_ManPiNum(pAig) != pCex->nPis ) + { + printf( "Cec_ManSeqResimulateCounter(): Parameters of the ccounter-example differ.\n" ); + return -1; + } + if ( pPars->fVerbose ) + printf( "Resimulating %d timeframes.\n", pPars->nRounds + pCex->iFrame + 1 ); + Aig_ManRandom( 1 ); + vSimInfo = Vec_PtrAllocSimInfo( Gia_ManRegNum(pAig) + + Gia_ManPiNum(pAig) * (pPars->nRounds + pCex->iFrame + 1), 1 ); + Cec_ManSeqDeriveInfoFromCex( vSimInfo, pAig, pCex ); + if ( pPars->fVerbose ) + Gia_ManEquivPrintClasses( pAig, 0, 0 ); + RetValue = Cec_ManSeqResimulateInfo( pAig, vSimInfo, NULL ); + if ( pPars->fVerbose ) + Gia_ManEquivPrintClasses( pAig, 0, 0 ); + Vec_PtrFree( vSimInfo ); + if ( pPars->fVerbose ) + ABC_PRT( "Time", clock() - clkTotal ); + return RetValue; +} + + +/**Function************************************************************* + + Synopsis [Performs semiformal refinement of equivalence classes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars ) +{ + int nAddFrames = 10; // additional timeframes to simulate + Cec_ParSat_t ParsSat, * pParsSat = &ParsSat; + Vec_Ptr_t * vSimInfo; + Gia_Cex_t * pState; + Gia_Man_t * pSrm; + int r, nPats, RetValue = -1; + if ( pAig->pReprs == NULL ) + { + printf( "Cec_ManSeqSemiformal(): Equivalence classes are not available.\n" ); + return -1; + } + if ( Gia_ManRegNum(pAig) == 0 ) + { + printf( "Cec_ManSeqSemiformal(): Not a sequential AIG.\n" ); + return -1; + } + Aig_ManRandom( 1 ); + // prepare starting pattern + pState = Gia_ManAllocCounterExample( Gia_ManRegNum(pAig), 0, 0 ); + pState->iFrame = -1; + pState->iPo = -1; + // prepare SAT solving + Cec_ManSatSetDefaultParams( pParsSat ); + pParsSat->nBTLimit = pPars->nBTLimit; + pParsSat->fVerbose = pPars->fVerbose; + if ( pParsSat->fVerbose ) + { + printf( "Starting: " ); + Gia_ManEquivPrintClasses( pAig, 0, 0 ); + } + // perform the given number of BMC rounds + for ( r = 0; r < pPars->nRounds; r++ ) + { +// Gia_ManPrintCounterExample( pState ); + // derive speculatively reduced model + pSrm = Gia_ManSpecReduceInit( pAig, pState, pPars->nFrames, pPars->fDualOut ); + assert( Gia_ManRegNum(pSrm) == 0 && Gia_ManPiNum(pSrm) == Gia_ManPiNum(pAig) * pPars->nFrames ); + // allocate room for simulation info + vSimInfo = Vec_PtrAllocSimInfo( Gia_ManRegNum(pAig) + + Gia_ManPiNum(pAig) * (pPars->nFrames + nAddFrames), pPars->nWords ); + Cec_ManSeqDeriveInfoInitRandom( vSimInfo, pAig, pState ); + // fill in simulation info with counter-examples + Cec_ManSatSolveSeq( vSimInfo, pSrm, pParsSat, Gia_ManRegNum(pAig), &nPats ); + Gia_ManStop( pSrm ); + // resimulate and refine the classes + RetValue = Cec_ManSeqResimulateInfo( pAig, vSimInfo, pState ); + Vec_PtrFree( vSimInfo ); + assert( pState->iPo >= 0 ); // hit counter + pState->iPo = -1; + if ( pPars->fVerbose ) + { + printf( "BMC = %3d ", nPats ); + Gia_ManEquivPrintClasses( pAig, 0, 0 ); + } + } + ABC_FREE( pState ); + return RetValue; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/cec/cecSolve.c b/src/aig/cec/cecSolve.c index ba4b0477..2b6997e1 100644 --- a/src/aig/cec/cecSolve.c +++ b/src/aig/cec/cecSolve.c @@ -630,6 +630,85 @@ ABC_PRT( "time", clock() - clk2 ); Cec_ManSatStop( p ); } + + +/**Function************************************************************* + + Synopsis [Save values in the cone of influence.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +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_ObjIsTravIdCurrent(p, pObj) ) + return; + Gia_ObjSetTravIdCurrent(p, pObj); + if ( Gia_ObjIsCi(pObj) ) + { + unsigned * pInfo = Vec_PtrEntry( vInfo, nRegs + Gia_ObjCioId(pObj) ); + if ( Cec_ObjSatVarValue( pSat, pObj ) != Aig_InfoHasBit( pInfo, iPat ) ) + Aig_InfoXorBit( pInfo, iPat ); + return; + } + assert( Gia_ObjIsAnd(pObj) ); + Cec_ManSatSolveSeq_rec( pSat, p, Gia_ObjFanin0(pObj), vInfo, iPat, nRegs ); + Cec_ManSatSolveSeq_rec( pSat, p, Gia_ObjFanin1(pObj), vInfo, iPat, nRegs ); +} + +/**Function************************************************************* + + Synopsis [Performs one round of solving for the POs of the AIG.] + + Description [Labels the nodes that have been proved (pObj->fMark1) + and returns the set of satisfying assignments.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat_t * pPars, int nRegs, int * pnPats ) +{ + Bar_Progress_t * pProgress = NULL; + Cec_ManSat_t * p; + Gia_Obj_t * pObj; + int iPat = 1, nPats = 32 * Vec_PtrReadWordsSimInfo(vPatts); + int i, status, clk = clock(); + Gia_ManSetPhase( pAig ); + Gia_ManLevelNum( pAig ); + Gia_ManResetTravId( pAig ); + p = Cec_ManSatCreate( pAig, pPars ); + pProgress = Bar_ProgressStart( stdout, Gia_ManPoNum(pAig) ); + Gia_ManForEachCo( pAig, pObj, i ) + { + if ( Gia_ObjIsConst0(Gia_ObjFanin0(pObj)) ) + continue; + Bar_ProgressUpdate( pProgress, i, "BMC..." ); + status = Cec_ManSatCheckNode( p, pObj ); + if ( status != 0 ) + continue; + // save the pattern + Gia_ManIncrementTravId( pAig ); + Cec_ManSatSolveSeq_rec( p, pAig, Gia_ObjFanin0(pObj), vPatts, iPat++, nRegs ); + if ( iPat == nPats ) + break; + // quit if one of them is solved + if ( pPars->fFirstStop ) + break; + } + p->timeTotal = clock() - clk; + Bar_ProgressStop( pProgress ); +// Cec_ManSatPrintStats( p ); + Cec_ManSatStop( p ); + if ( pnPats ) + *pnPats = iPat-1; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/cec/cecSweep.c b/src/aig/cec/cecSweep.c index 20a668bd..3024ac24 100644 --- a/src/aig/cec/cecSweep.c +++ b/src/aig/cec/cecSweep.c @@ -83,7 +83,7 @@ Gia_Man_t * Cec_ManFraSpecReduction( Cec_ManFra_t * p ) (Gia_ObjLevel(p->pAig, pObj) > p->pPars->nLevelMax || Gia_ObjLevel(p->pAig, pRepr) > p->pPars->nLevelMax) ) continue; - if ( p->pPars->fDoubleOuts ) + if ( p->pPars->fDualOut ) { // if ( i % 1000 == 0 && Gia_ObjRepr(p->pAig, i) ) // Gia_ManEquivPrintOne( p->pAig, Gia_ObjRepr(p->pAig, i), 0 ); diff --git a/src/aig/cec/module.make b/src/aig/cec/module.make index 4618c424..1fc9861c 100644 --- a/src/aig/cec/module.make +++ b/src/aig/cec/module.make @@ -4,6 +4,7 @@ SRC += src/aig/cec/cecCec.c \ src/aig/cec/cecIso.c \ src/aig/cec/cecMan.c \ src/aig/cec/cecPat.c \ + src/aig/cec/cecSeq.c \ src/aig/cec/cecSim.c \ src/aig/cec/cecSolve.c \ src/aig/cec/cecSweep.c diff --git a/src/aig/cec2/cec.h b/src/aig/cec2/cec.h deleted file mode 100644 index 3586b535..00000000 --- a/src/aig/cec2/cec.h +++ /dev/null @@ -1,104 +0,0 @@ -/**CFile**************************************************************** - - FileName [cec.h] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Combinatinoal equivalence checking.] - - Synopsis [External declarations.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: cec.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#ifndef __CEC_H__ -#define __CEC_H__ - -//////////////////////////////////////////////////////////////////////// -/// INCLUDES /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// PARAMETERS /// -//////////////////////////////////////////////////////////////////////// - -#ifdef __cplusplus -extern "C" { -#endif - -//////////////////////////////////////////////////////////////////////// -/// BASIC TYPES /// -//////////////////////////////////////////////////////////////////////// - -// dynamic SAT parameters -typedef struct Cec_ParSat_t_ Cec_ParSat_t; -struct Cec_ParSat_t_ -{ - int nBTLimit; // conflict limit at a node - int nSatVarMax; // the max number of SAT variables - int nCallsRecycle; // calls to perform before recycling SAT solver - int fFirstStop; // stop on the first sat output - int fPolarFlip; // uses polarity adjustment - int fVerbose; // verbose stats -}; - -// combinational SAT sweeping parameters -typedef struct Cec_ParCsw_t_ Cec_ParCsw_t; -struct Cec_ParCsw_t_ -{ - int nWords; // the number of simulation words - int nRounds; // the number of simulation rounds - int nBTLimit; // conflict limit at a node - int nSatVarMax; // the max number of SAT variables - int nCallsRecycle; // calls to perform before recycling SAT solver - int nLevelMax; // restriction on the level nodes to be swept - int fRewriting; // enables AIG rewriting - int fFirstStop; // stop on the first sat output - int fVerbose; // verbose stats -}; - -// combinational equivalence checking parameters -typedef struct Cec_ParCec_t_ Cec_ParCec_t; -struct Cec_ParCec_t_ -{ - int nIters; // iterations of SAT solving/sweeping - int nBTLimitBeg; // starting backtrack limit - int nBTlimitMulti; // multiple of backtrack limit - int fUseSmartCnf; // use smart CNF computation - int fRewriting; // enables AIG rewriting - int fSatSweeping; // enables SAT sweeping - int fFirstStop; // stop on the first sat output - int fVerbose; // verbose stats -}; - -//////////////////////////////////////////////////////////////////////// -/// MACRO DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -/*=== cecCore.c ==========================================================*/ -extern void Cec_ManSatSetDefaultParams( Cec_ParSat_t * p ); -extern void Cec_ManCswSetDefaultParams( Cec_ParCsw_t * p ); -extern void Cec_ManCecSetDefaultParams( Cec_ParCec_t * p ); -extern int Cec_Solve( Aig_Man_t * pAig0, Aig_Man_t * pAig1, Cec_ParCec_t * p ); - -#ifdef __cplusplus -} -#endif - -#endif - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - diff --git a/src/aig/cec2/cecAig.c b/src/aig/cec2/cecAig.c deleted file mode 100644 index c322ead8..00000000 --- a/src/aig/cec2/cecAig.c +++ /dev/null @@ -1,168 +0,0 @@ -/**CFile**************************************************************** - - FileName [cecAig.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Combinatinoal equivalence checking.] - - Synopsis [AIG manipulation.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: cecAig.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "cecInt.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Derives combinational miter of the two AIGs.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Aig_Obj_t * Cec_DeriveMiter_rec( Aig_Man_t * pNew, Aig_Obj_t * pObj ) -{ - if ( pObj->pData ) - return pObj->pData; - if ( Aig_ObjIsPi(pObj) ) - { - pObj->pData = Aig_ObjCreatePi( pNew ); - if ( pObj->pHaig ) - { - assert( pObj->pHaig->pData == NULL ); - pObj->pHaig->pData = pObj->pData; - } - return pObj->pData; - } - assert( Aig_ObjIsNode(pObj) ); - Cec_DeriveMiter_rec( pNew, Aig_ObjFanin0(pObj) ); - Cec_DeriveMiter_rec( pNew, Aig_ObjFanin1(pObj) ); - pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); - return pObj->pData; -} - -/**Function************************************************************* - - Synopsis [Derives combinational miter of the two AIGs.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Aig_Man_t * Cec_DeriveMiter( Aig_Man_t * p0, Aig_Man_t * p1 ) -{ - Bar_Progress_t * pProgress = NULL; - Aig_Man_t * pNew; - Aig_Obj_t * pObj0, * pObj1, * pObjNew; - int i; - assert( Aig_ManPiNum(p0) == Aig_ManPiNum(p1) ); - assert( Aig_ManPoNum(p0) == Aig_ManPoNum(p1) ); - // create the new manager - pNew = Aig_ManStart( Aig_ManNodeNum(p0) + Aig_ManNodeNum(p1) ); - pNew->pName = Aig_UtilStrsav( p0->pName ); - // create the PIs - Aig_ManCleanData( p0 ); - Aig_ManCleanData( p1 ); - Aig_ManConst1(p0)->pData = Aig_ManConst1(pNew); - Aig_ManConst1(p1)->pData = Aig_ManConst1(pNew); - Aig_ManForEachPi( p0, pObj0, i ) - { - pObj1 = Aig_ManPi( p1, i ); - pObj0->pHaig = pObj1; - pObj1->pHaig = pObj0; - if ( Aig_ObjRefs(pObj0) || Aig_ObjRefs(pObj1) ) - continue; - pObjNew = Aig_ObjCreatePi( pNew ); - pObj0->pData = pObjNew; - pObj1->pData = pObjNew; - } - // add logic for the POs - pProgress = Bar_ProgressStart( stdout, Aig_ManPoNum(p0) ); - Aig_ManForEachPo( p0, pObj0, i ) - { - Bar_ProgressUpdate( pProgress, i, "Miter..." ); - pObj1 = Aig_ManPo( p1, i ); - Cec_DeriveMiter_rec( pNew, Aig_ObjFanin0(pObj0) ); - Cec_DeriveMiter_rec( pNew, Aig_ObjFanin0(pObj1) ); - pObjNew = Aig_Exor( pNew, Aig_ObjChild0Copy(pObj0), Aig_ObjChild0Copy(pObj1) ); - Aig_ObjCreatePo( pNew, pObjNew ); - } - Bar_ProgressStop( pProgress ); - Aig_ManSetRegNum( pNew, 0 ); - assert( Aig_ManHasNoGaps(pNew) ); - return pNew; -} - -/**Function************************************************************* - - Synopsis [Duplicates AIG in the DFS order.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Aig_Man_t * Cec_Duplicate( Aig_Man_t * p ) -{ - Bar_Progress_t * pProgress = NULL; - Aig_Man_t * pNew; - Aig_Obj_t * pObj; - int i; - // make sure the AIG does not have choices and dangling nodes - Aig_ManForEachNode( p, pObj, i ) - assert( Aig_ObjRefs(pObj) > 0 ); - // create the new manager - pNew = Aig_ManStart( Aig_ManNodeNum(p) ); - pNew->pName = Aig_UtilStrsav( p->pName ); - // create the PIs - Aig_ManCleanData( p ); - Aig_ManConst1(p)->pData = Aig_ManConst1(pNew); - Aig_ManForEachPi( p, pObj, i ) - { - pObj->pHaig = NULL; - if ( Aig_ObjRefs(pObj) == 0 ) - pObj->pData = Aig_ObjCreatePi( pNew ); - } - // add logic for the POs - pProgress = Bar_ProgressStart( stdout, Aig_ManPoNum(p) ); - Aig_ManForEachPo( p, pObj, i ) - { - Bar_ProgressUpdate( pProgress, i, "Miter..." ); - Cec_DeriveMiter_rec( pNew, Aig_ObjFanin0(pObj) ); - Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); - } - Bar_ProgressStop( pProgress ); - Aig_ManSetRegNum( pNew, 0 ); - assert( Aig_ManHasNoGaps(pNew) ); - return pNew; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/aig/cec2/cecClass.c b/src/aig/cec2/cecClass.c deleted file mode 100644 index 24e40281..00000000 --- a/src/aig/cec2/cecClass.c +++ /dev/null @@ -1,571 +0,0 @@ -/**CFile**************************************************************** - - FileName [cecClass.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Combinatinoal equivalence checking.] - - Synopsis [Equivalence class representation.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: cecClass.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "cecInt.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Aig_Man_t * Caig_ManSpecReduce( Caig_Man_t * p, int nLevels ) -{ - Aig_Man_t * pAig; - Aig_Obj_t ** pCopy; - Aig_Obj_t * pRes0, * pRes1, * pRepr, * pNode; - Aig_Obj_t * pMiter; - int i; - pAig = Aig_ManStart( p->nNodes ); - pCopy = ABC_ALLOC( Aig_Obj_t *, p->nObjs ); - pCopy[0] = Aig_ManConst1(pAig); - for ( i = 1; i < p->nObjs; i++ ) - { - if ( p->pFans0[i] == -1 ) // pi always has zero first fanin - { - pCopy[i] = Aig_ObjCreatePi( pAig ); - continue; - } - if ( p->pFans1[i] == -1 ) // po always has non-zero 1st fanin and zero 2nd fanin - continue; - pRes0 = Aig_NotCond( pCopy[Cec_Lit2Var(p->pFans0[i])], Cec_LitIsCompl(p->pFans0[i]) ); - pRes1 = Aig_NotCond( pCopy[Cec_Lit2Var(p->pFans1[i])], Cec_LitIsCompl(p->pFans1[i]) ); - pNode = pCopy[i] = Aig_And( pAig, pRes0, pRes1 ); - if ( p->pReprs[i] < 0 ) - continue; - assert( p->pReprs[i] < i ); - pRepr = pCopy[p->pReprs[i]]; - if ( Aig_Regular(pNode) == Aig_Regular(pRepr) ) - continue; - pCopy[i] = Aig_NotCond( pRepr, Aig_ObjPhaseReal(pRepr) ^ Aig_ObjPhaseReal(pNode) ); - if ( nLevels && ((int)Aig_Regular(pRepr)->Level > nLevels || (int)Aig_Regular(pNode)->Level > nLevels) ) - continue; - pMiter = Aig_Exor( pAig, pNode, pRepr ); - Aig_ObjCreatePo( pAig, Aig_NotCond(pMiter, Aig_ObjPhaseReal(pMiter)) ); -// Aig_ObjCreatePo( pAig, Aig_Regular(pRepr) ); -// Aig_ObjCreatePo( pAig, Aig_Regular(pCopy[i]) ); - } - ABC_FREE( pCopy ); - Aig_ManSetRegNum( pAig, 0 ); - Aig_ManCleanup( pAig ); - return pAig; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Caig_ManCountOne( Caig_Man_t * p, int i ) -{ - int Ent, nLits = 0; - assert( p->pReprs[i] < 0 && p->pNexts[i] > 0 ); - for ( Ent = p->pNexts[i]; Ent; Ent = p->pNexts[Ent] ) - { - assert( p->pReprs[Ent] == i ); - nLits++; - } - return 1 + nLits; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Caig_ManCountLiterals( Caig_Man_t * p ) -{ - int i, nLits = 0; - for ( i = 1; i < p->nObjs; i++ ) - if ( p->pReprs[i] < 0 && p->pNexts[i] > 0 ) - nLits += Caig_ManCountOne(p, i) - 1; - return nLits; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Caig_ManPrintOne( Caig_Man_t * p, int i, int Counter ) -{ - int Ent; - printf( "Class %4d : Num = %2d {", Counter, Caig_ManCountOne(p, i) ); - for ( Ent = i; Ent; Ent = p->pNexts[Ent] ) - printf(" %d", Ent ); - printf( " }\n" ); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Caig_ManPrintClasses( Caig_Man_t * p, int fVerbose ) -{ - int i, Counter = 0, Counter1 = 0, CounterX = 0, nLits; - for ( i = 1; i < p->nObjs; i++ ) - { - if ( p->pReprs[i] < 0 && p->pNexts[i] > 0 ) - Counter++; - if ( p->pReprs[i] == 0 ) - Counter1++; - if ( p->pReprs[i] < 0 && p->pNexts[i] == 0 ) - CounterX++; - } - nLits = Caig_ManCountLiterals( p ); - printf( "Class = %6d. Const = %6d. Unsed = %6d. Lits = %7d. All = %7d. Mem = %5.2f Mb\n", - Counter, Counter1, CounterX, nLits, nLits+Counter1, 1.0*p->nMemsMax/(1<<20) ); - if ( fVerbose ) - for ( i = 1; i < p->nObjs; i++ ) - if ( p->pReprs[i] < 0 && p->pNexts[i] > 0 ) - Caig_ManPrintOne( p, i, ++Counter ); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Caig_ManCollectSimsSimple( Caig_Man_t * p, int i ) -{ - int Ent; - Vec_PtrClear( p->vSims ); - for ( Ent = i; Ent; Ent = p->pNexts[Ent] ) - Vec_PtrPush( p->vSims, p->pSims + Ent ); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Caig_ManCollectSimsNormal( Caig_Man_t * p, int i ) -{ - unsigned * pSim; - int Ent; - Vec_PtrClear( p->vSims ); - for ( Ent = i; Ent; Ent = p->pNexts[Ent] ) - { - pSim = Caig_ManSimDeref( p, Ent ); - Vec_PtrPush( p->vSims, pSim + 1 ); - } -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Caig_ManCompareEqual( unsigned * p0, unsigned * p1, int nWords ) -{ - int w; - if ( (p0[0] & 1) == (p1[0] & 1) ) - { - for ( w = 0; w < nWords; w++ ) - if ( p0[w] != p1[w] ) - return 0; - return 1; - } - else - { - for ( w = 0; w < nWords; w++ ) - if ( p0[w] != ~p1[w] ) - return 0; - return 1; - } -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Caig_ManCompareConst( unsigned * p, int nWords ) -{ - int w; - if ( p[0] & 1 ) - { - for ( w = 0; w < nWords; w++ ) - if ( p[w] != ~0 ) - return 0; - return 1; - } - else - { - for ( w = 0; w < nWords; w++ ) - if ( p[w] != 0 ) - return 0; - return 1; - } -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Caig_ManClassCreate( Caig_Man_t * p, Vec_Int_t * vClass ) -{ - int * pNext, Repr, Ent, i; - assert( Vec_IntSize(vClass) > 0 ); - Vec_IntForEachEntry( vClass, Ent, i ) - { - if ( i == 0 ) - { - Repr = Ent; - p->pReprs[Ent] = -1; - pNext = p->pNexts + Ent; - } - else - { - p->pReprs[Ent] = Repr; - *pNext = Ent; - pNext = p->pNexts + Ent; - } - } - *pNext = 0; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Caig_ManClassRefineOne( Caig_Man_t * p, int i, Vec_Ptr_t * vSims ) -{ - unsigned * pSim0, * pSim1; - int Ent, c = 0, d = 0; - Vec_IntClear( p->vClassOld ); - Vec_IntClear( p->vClassNew ); - pSim0 = Vec_PtrEntry( vSims, c++ ); - Vec_IntPush( p->vClassOld, i ); - for ( Ent = p->pNexts[i]; Ent; Ent = p->pNexts[Ent] ) - { - pSim1 = Vec_PtrEntry( vSims, c++ ); - if ( Caig_ManCompareEqual( pSim0, pSim1, p->nWords ) ) - Vec_IntPush( p->vClassOld, Ent ); - else - { - Vec_IntPush( p->vClassNew, Ent ); - Vec_PtrWriteEntry( vSims, d++, pSim1 ); - } - } -//if ( Vec_PtrSize(vSims) > 100 ) -//printf( "%d -> %d %d \n", Vec_PtrSize(vSims), Vec_IntSize(p->vClassOld), Vec_IntSize(p->vClassNew) ); - Vec_PtrShrink( vSims, d ); - if ( Vec_IntSize(p->vClassNew) == 0 ) - return 0; - Caig_ManClassCreate( p, p->vClassOld ); - Caig_ManClassCreate( p, p->vClassNew ); - if ( Vec_IntSize(p->vClassNew) > 1 ) - return 1 + Caig_ManClassRefineOne( p, Vec_IntEntry(p->vClassNew,0), vSims ); - return 1; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Caig_ManHashKey( unsigned * pSim, int nWords, int nTableSize ) -{ - static int s_Primes[16] = { - 1291, 1699, 1999, 2357, 2953, 3313, 3907, 4177, - 4831, 5147, 5647, 6343, 6899, 7103, 7873, 8147 }; - unsigned uHash = 0; - int i; - if ( pSim[0] & 1 ) - for ( i = 0; i < nWords; i++ ) - uHash ^= ~pSim[i] * s_Primes[i & 0xf]; - else - for ( i = 0; i < nWords; i++ ) - uHash ^= pSim[i] * s_Primes[i & 0xf]; - return (int)(uHash % nTableSize); - -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Caig_ManClassesCreate( Caig_Man_t * p ) -{ - int * pTable, nTableSize, i, Key; - nTableSize = Aig_PrimeCudd( 100 + p->nObjs / 10 ); - pTable = ABC_CALLOC( int, nTableSize ); - p->pReprs = ABC_ALLOC( int, p->nObjs ); - p->pNexts = ABC_CALLOC( int, p->nObjs ); - for ( i = 1; i < p->nObjs; i++ ) - { - if ( p->pFans0[i] > 0 && p->pFans1[i] == -1 ) // po always has non-zero 1st fanin and zero 2nd fanin - continue; - if ( Caig_ManCompareConst( p->pSims + i, 1 ) ) - { - p->pReprs[i] = 0; - continue; - } - Key = Caig_ManHashKey( p->pSims + i, 1, nTableSize ); - if ( pTable[Key] == 0 ) - p->pReprs[i] = -1; - else - { - p->pNexts[ pTable[Key] ] = i; - p->pReprs[i] = p->pReprs[ pTable[Key] ]; - if ( p->pReprs[i] == -1 ) - p->pReprs[i] = pTable[Key]; - } - pTable[Key] = i; - } - ABC_FREE( pTable ); -Caig_ManPrintClasses( p, 0 ); - // refine classes - for ( i = 1; i < p->nObjs; i++ ) - if ( p->pReprs[i] < 0 && p->pNexts[i] > 0 ) - { - Caig_ManCollectSimsSimple( p, i ); - Caig_ManClassRefineOne( p, i, p->vSims ); - } - // clean memory - memset( p->pSims, 0, sizeof(unsigned) * p->nObjs ); -Caig_ManPrintClasses( p, 0 ); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Caig_ManSimulateSimple( Caig_Man_t * p ) -{ - unsigned Res0, Res1; - int i; - for ( i = 1; i < p->nObjs; i++ ) - { - if ( p->pFans0[i] == -1 ) // pi - { - p->pSims[i] = Aig_ManRandom( 0 ); - continue; - } - if ( p->pFans1[i] == -1 ) // po always has non-zero 1st fanin and zero 2nd fanin - continue; - Res0 = p->pSims[Cec_Lit2Var(p->pFans0[i])]; - Res1 = p->pSims[Cec_Lit2Var(p->pFans1[i])]; - p->pSims[i] = (Cec_LitIsCompl(p->pFans0[i]) ? ~Res0: Res0) & - (Cec_LitIsCompl(p->pFans1[i]) ? ~Res1: Res1); - } -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Caig_ManProcessRefined( Caig_Man_t * p, Vec_Int_t * vRefined ) -{ - Vec_Int_t * vClasses; - int * pTable, nTableSize, i, Key, iNode; - unsigned * pSim; - if ( Vec_IntSize(vRefined) == 0 ) - return; - nTableSize = Aig_PrimeCudd( 100 + Vec_IntSize(vRefined) / 5 ); - pTable = ABC_CALLOC( int, nTableSize ); - vClasses = Vec_IntAlloc( 100 ); - Vec_IntForEachEntry( vRefined, iNode, i ) - { - pSim = Caig_ManSimRead( p, iNode ); - assert( !Caig_ManCompareConst( pSim + 1, p->nWords ) ); - Key = Caig_ManHashKey( pSim + 1, p->nWords, nTableSize ); - if ( pTable[Key] == 0 ) - { - assert( p->pReprs[iNode] == 0 ); - assert( p->pNexts[iNode] == 0 ); - p->pReprs[iNode] = -1; - Vec_IntPush( vClasses, iNode ); - } - else - { - p->pNexts[ pTable[Key] ] = iNode; - p->pReprs[iNode] = p->pReprs[ pTable[Key] ]; - if ( p->pReprs[iNode] == -1 ) - p->pReprs[iNode] = pTable[Key]; - assert( p->pReprs[iNode] > 0 ); - } - pTable[Key] = iNode; - } - ABC_FREE( pTable ); - // refine classes - Vec_IntForEachEntry( vClasses, iNode, i ) - { - if ( p->pNexts[iNode] == 0 ) - { - Caig_ManSimDeref( p, iNode ); - continue; - } - Caig_ManCollectSimsNormal( p, iNode ); - Caig_ManClassRefineOne( p, iNode, p->vSims ); - } - Vec_IntFree( vClasses ); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Caig_Man_t * Caig_ManClassesPrepare( Aig_Man_t * pAig, int nWords, int nIters ) -{ - Vec_Ptr_t * vInfo; - Caig_Man_t * p; - int i; - Aig_ManRandom( 1 ); - p = Caig_ManCreate( pAig ); - p->nWords = 1; - Caig_ManSimulateSimple( p ); - Caig_ManClassesCreate( p ); - p->nWords = nWords; - for ( i = 0; i < nIters; i++ ) - { - p->nWords = i + 1; - Caig_ManSimMemRelink( p ); - p->nMemsMax = 0; - - vInfo = Vec_PtrAllocSimInfo( p->nPis, p->nWords ); - Aig_ManRandomInfo( vInfo, 0, p->nWords ); - Caig_ManSimulateRound( p, vInfo, NULL ); - Vec_PtrFree( vInfo ); -Caig_ManPrintClasses( p, 0 ); - } - - p->nWords = nWords; - Caig_ManSimMemRelink( p ); - p->nMemsMax = 0; - return p; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/aig/cec2/cecCnf.c b/src/aig/cec2/cecCnf.c deleted file mode 100644 index 706b15e0..00000000 --- a/src/aig/cec2/cecCnf.c +++ /dev/null @@ -1,328 +0,0 @@ -/**CFile**************************************************************** - - FileName [cecCnf.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Combinatinoal equivalence checking.] - - Synopsis [CNF computation.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: cecCnf.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "cecInt.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Addes clauses to the solver.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Cec_AddClausesMux( Cec_ManSat_t * p, Aig_Obj_t * pNode ) -{ - Aig_Obj_t * pNodeI, * pNodeT, * pNodeE; - int pLits[4], RetValue, VarF, VarI, VarT, VarE, fCompT, fCompE; - - assert( !Aig_IsComplement( pNode ) ); - assert( Aig_ObjIsMuxType( pNode ) ); - // get nodes (I = if, T = then, E = else) - pNodeI = Aig_ObjRecognizeMux( pNode, &pNodeT, &pNodeE ); - // get the variable numbers - VarF = Cec_ObjSatNum(p,pNode); - VarI = Cec_ObjSatNum(p,pNodeI); - VarT = Cec_ObjSatNum(p,Aig_Regular(pNodeT)); - VarE = Cec_ObjSatNum(p,Aig_Regular(pNodeE)); - // get the complementation flags - fCompT = Aig_IsComplement(pNodeT); - fCompE = Aig_IsComplement(pNodeE); - - // f = ITE(i, t, e) - - // i' + t' + f - // i' + t + f' - // i + e' + f - // i + e + f' - - // create four clauses - pLits[0] = toLitCond(VarI, 1); - pLits[1] = toLitCond(VarT, 1^fCompT); - pLits[2] = toLitCond(VarF, 0); - if ( p->pPars->fPolarFlip ) - { - if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] ); - if ( Aig_Regular(pNodeT)->fPhase ) pLits[1] = lit_neg( pLits[1] ); - if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] ); - } - RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 ); - assert( RetValue ); - pLits[0] = toLitCond(VarI, 1); - pLits[1] = toLitCond(VarT, 0^fCompT); - pLits[2] = toLitCond(VarF, 1); - if ( p->pPars->fPolarFlip ) - { - if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] ); - if ( Aig_Regular(pNodeT)->fPhase ) pLits[1] = lit_neg( pLits[1] ); - if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] ); - } - RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 ); - assert( RetValue ); - pLits[0] = toLitCond(VarI, 0); - pLits[1] = toLitCond(VarE, 1^fCompE); - pLits[2] = toLitCond(VarF, 0); - if ( p->pPars->fPolarFlip ) - { - if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] ); - if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] ); - if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] ); - } - RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 ); - assert( RetValue ); - pLits[0] = toLitCond(VarI, 0); - pLits[1] = toLitCond(VarE, 0^fCompE); - pLits[2] = toLitCond(VarF, 1); - if ( p->pPars->fPolarFlip ) - { - if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] ); - if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] ); - if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] ); - } - RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 ); - assert( RetValue ); - - // two additional clauses - // t' & e' -> f' - // t & e -> f - - // t + e + f' - // t' + e' + f - - if ( VarT == VarE ) - { -// assert( fCompT == !fCompE ); - return; - } - - pLits[0] = toLitCond(VarT, 0^fCompT); - pLits[1] = toLitCond(VarE, 0^fCompE); - pLits[2] = toLitCond(VarF, 1); - if ( p->pPars->fPolarFlip ) - { - if ( Aig_Regular(pNodeT)->fPhase ) pLits[0] = lit_neg( pLits[0] ); - if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] ); - if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] ); - } - RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 ); - assert( RetValue ); - pLits[0] = toLitCond(VarT, 1^fCompT); - pLits[1] = toLitCond(VarE, 1^fCompE); - pLits[2] = toLitCond(VarF, 0); - if ( p->pPars->fPolarFlip ) - { - if ( Aig_Regular(pNodeT)->fPhase ) pLits[0] = lit_neg( pLits[0] ); - if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] ); - if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] ); - } - RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 ); - assert( RetValue ); -} - -/**Function************************************************************* - - Synopsis [Addes clauses to the solver.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Cec_AddClausesSuper( Cec_ManSat_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper ) -{ - Aig_Obj_t * pFanin; - int * pLits, nLits, RetValue, i; - assert( !Aig_IsComplement(pNode) ); - assert( Aig_ObjIsNode( pNode ) ); - // create storage for literals - nLits = Vec_PtrSize(vSuper) + 1; - pLits = ABC_ALLOC( int, nLits ); - // suppose AND-gate is A & B = C - // add !A => !C or A + !C - Vec_PtrForEachEntry( vSuper, pFanin, i ) - { - pLits[0] = toLitCond(Cec_ObjSatNum(p,Aig_Regular(pFanin)), Aig_IsComplement(pFanin)); - pLits[1] = toLitCond(Cec_ObjSatNum(p,pNode), 1); - if ( p->pPars->fPolarFlip ) - { - if ( Aig_Regular(pFanin)->fPhase ) pLits[0] = lit_neg( pLits[0] ); - if ( pNode->fPhase ) pLits[1] = lit_neg( pLits[1] ); - } - RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 ); - assert( RetValue ); - } - // add A & B => C or !A + !B + C - Vec_PtrForEachEntry( vSuper, pFanin, i ) - { - pLits[i] = toLitCond(Cec_ObjSatNum(p,Aig_Regular(pFanin)), !Aig_IsComplement(pFanin)); - if ( p->pPars->fPolarFlip ) - { - if ( Aig_Regular(pFanin)->fPhase ) pLits[i] = lit_neg( pLits[i] ); - } - } - pLits[nLits-1] = toLitCond(Cec_ObjSatNum(p,pNode), 0); - if ( p->pPars->fPolarFlip ) - { - if ( pNode->fPhase ) pLits[nLits-1] = lit_neg( pLits[nLits-1] ); - } - RetValue = sat_solver_addclause( p->pSat, pLits, pLits + nLits ); - assert( RetValue ); - ABC_FREE( pLits ); -} - -/**Function************************************************************* - - Synopsis [Collects the supergate.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Cec_CollectSuper_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int fUseMuxes ) -{ - // if the new node is complemented or a PI, another gate begins - if ( Aig_IsComplement(pObj) || Aig_ObjIsPi(pObj) || - (!fFirst && Aig_ObjRefs(pObj) > 1) || - (fUseMuxes && Aig_ObjIsMuxType(pObj)) ) - { - Vec_PtrPushUnique( vSuper, pObj ); - return; - } - // go through the branches - Cec_CollectSuper_rec( Aig_ObjChild0(pObj), vSuper, 0, fUseMuxes ); - Cec_CollectSuper_rec( Aig_ObjChild1(pObj), vSuper, 0, fUseMuxes ); -} - -/**Function************************************************************* - - Synopsis [Collects the supergate.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Cec_CollectSuper( Aig_Obj_t * pObj, int fUseMuxes, Vec_Ptr_t * vSuper ) -{ - assert( !Aig_IsComplement(pObj) ); - assert( !Aig_ObjIsPi(pObj) ); - Vec_PtrClear( vSuper ); - Cec_CollectSuper_rec( pObj, vSuper, 1, fUseMuxes ); -} - -/**Function************************************************************* - - Synopsis [Updates the solver clause database.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Cec_ObjAddToFrontier( Cec_ManSat_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vFrontier ) -{ - assert( !Aig_IsComplement(pObj) ); - if ( Cec_ObjSatNum(p,pObj) ) - return; - assert( Cec_ObjSatNum(p,pObj) == 0 ); - if ( Aig_ObjIsConst1(pObj) ) - return; - Vec_PtrPush( p->vUsedNodes, pObj ); - Cec_ObjSetSatNum( p, pObj, p->nSatVars++ ); - if ( Aig_ObjIsNode(pObj) ) - Vec_PtrPush( vFrontier, pObj ); -} - -/**Function************************************************************* - - Synopsis [Updates the solver clause database.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Cec_CnfNodeAddToSolver( Cec_ManSat_t * p, Aig_Obj_t * pObj ) -{ - Vec_Ptr_t * vFrontier; - Aig_Obj_t * pNode, * pFanin; - int i, k, fUseMuxes = 1; - // quit if CNF is ready - if ( Cec_ObjSatNum(p,pObj) ) - return; - // start the frontier - vFrontier = Vec_PtrAlloc( 100 ); - Cec_ObjAddToFrontier( p, pObj, vFrontier ); - // explore nodes in the frontier - Vec_PtrForEachEntry( vFrontier, pNode, i ) - { - // create the supergate - assert( Cec_ObjSatNum(p,pNode) ); - if ( fUseMuxes && Aig_ObjIsMuxType(pNode) ) - { - Vec_PtrClear( p->vFanins ); - Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin0( Aig_ObjFanin0(pNode) ) ); - Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin0( Aig_ObjFanin1(pNode) ) ); - Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin1( Aig_ObjFanin0(pNode) ) ); - Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin1( Aig_ObjFanin1(pNode) ) ); - Vec_PtrForEachEntry( p->vFanins, pFanin, k ) - Cec_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier ); - Cec_AddClausesMux( p, pNode ); - } - else - { - Cec_CollectSuper( pNode, fUseMuxes, p->vFanins ); - Vec_PtrForEachEntry( p->vFanins, pFanin, k ) - Cec_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier ); - Cec_AddClausesSuper( p, pNode, p->vFanins ); - } - assert( Vec_PtrSize(p->vFanins) > 1 ); - } - Vec_PtrFree( vFrontier ); -} - - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/aig/cec2/cecCore.c b/src/aig/cec2/cecCore.c deleted file mode 100644 index 540a3951..00000000 --- a/src/aig/cec2/cecCore.c +++ /dev/null @@ -1,245 +0,0 @@ -/**CFile**************************************************************** - - FileName [cecCore.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Combinatinoal equivalence checking.] - - Synopsis [Core procedures.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: cecCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "cecInt.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [This procedure sets default parameters.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Cec_ManSatSetDefaultParams( Cec_ParSat_t * p ) -{ - memset( p, 0, sizeof(Cec_ParSat_t) ); - p->nBTLimit = 10; // conflict limit at a node - p->nSatVarMax = 2000; // the max number of SAT variables - p->nCallsRecycle = 100; // calls to perform before recycling SAT solver - p->fFirstStop = 0; // stop on the first sat output - p->fPolarFlip = 0; // uses polarity adjustment - p->fVerbose = 0; // verbose stats -} - -/**Function************************************************************* - - Synopsis [This procedure sets default parameters.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Cec_ManCswSetDefaultParams( Cec_ParCsw_t * p ) -{ - memset( p, 0, sizeof(Cec_ParCsw_t) ); - p->nWords = 10; // the number of simulation words - p->nRounds = 10; // the number of simulation rounds - p->nBTLimit = 10; // conflict limit at a node - p->nSatVarMax = 2000; // the max number of SAT variables - p->nCallsRecycle = 100; // calls to perform before recycling SAT solver - p->nLevelMax = 50; // restriction on the level of nodes to be swept - p->fRewriting = 0; // enables AIG rewriting - p->fFirstStop = 0; // stop on the first sat output - p->fVerbose = 1; // verbose stats -} - -/**Function************************************************************* - - Synopsis [This procedure sets default parameters.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Cec_ManCecSetDefaultParams( Cec_ParCec_t * p ) -{ - memset( p, 0, sizeof(Cec_ParCec_t) ); - p->nIters = 1; // iterations of SAT solving/sweeping - p->nBTLimitBeg = 2; // starting backtrack limit - p->nBTlimitMulti = 8; // multiple of backtrack limiter - p->fUseSmartCnf = 0; // use smart CNF computation - p->fRewriting = 0; // enables AIG rewriting - p->fSatSweeping = 0; // enables SAT sweeping - p->fFirstStop = 0; // stop on the first sat output - p->fVerbose = 1; // verbose stats -} - - -/**Function************************************************************* - - Synopsis [Performs equivalence checking.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Cec_Sweep( Aig_Man_t * pAig, int nBTLimit ) -{ - extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact ); -// Cec_MtrStatus_t Status; - Cec_ParCsw_t ParsCsw, * pParsCsw = &ParsCsw; - Cec_ParSat_t ParsSat, * pParsSat = &ParsSat; - Caig_Man_t * pCaig; - Aig_Man_t * pSRAig; -// int clk; - - Cec_ManCswSetDefaultParams( pParsCsw ); - pParsCsw->nBTLimit = nBTLimit; - pCaig = Caig_ManClassesPrepare( pAig, pParsCsw->nWords, pParsCsw->nRounds ); - - pSRAig = Caig_ManSpecReduce( pCaig, 20 ); - Aig_ManPrintStats( pSRAig ); - Ioa_WriteAiger( pSRAig, "temp_srm.aig", 0, 1 ); - -/* - Cec_ManSatSetDefaultParams( pParsSat ); - pParsSat->fFirstStop = 0; - pParsSat->nBTLimit = pParsCsw->nBTlimit; -clk = clock(); - Status = Cec_SatSolveOutputs( pSRAig, pParsSat ); - Cec_MiterStatusPrint( Status, "SRM ", clock() - clk ); -*/ - - Aig_ManStop( pSRAig ); - - Caig_ManDelete( pCaig ); - - return 1; -} - -/**Function************************************************************* - - Synopsis [Performs equivalence checking.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Cec_Solve( Aig_Man_t * pAig0, Aig_Man_t * pAig1, Cec_ParCec_t * pPars ) -{ - Cec_ParSat_t ParsSat, * pParsSat = &ParsSat; - Cec_ParCsw_t ParsCsw, * pParsCsw = &ParsCsw; - Cec_MtrStatus_t Status; - Caig_Man_t * pCaig; - Aig_Man_t * pMiter; - int i, clk = clock(); - if ( pPars->fVerbose ) - { - Status = Cec_MiterStatusTrivial( pAig0 ); - Status.nNodes += pAig1? Aig_ManNodeNum( pAig1 ) : 0; - Cec_MiterStatusPrint( Status, "Init ", 0 ); - } - // create combinational miter - if ( pAig1 == NULL ) - { - Status = Cec_MiterStatus( pAig0 ); - if ( Status.nSat > 0 && pPars->fFirstStop ) - { - if ( pPars->fVerbose ) - printf( "Output %d is trivially SAT.\n", Status.iOut ); - return 0; - } - if ( Status.nUndec == 0 ) - { - if ( pPars->fVerbose ) - printf( "The miter has no undecided outputs.\n" ); - return 1; - } - pMiter = Cec_Duplicate( pAig0 ); - } - else - { - pMiter = Cec_DeriveMiter( pAig0, pAig1 ); - Status = Cec_MiterStatus( pMiter ); - if ( Status.nSat > 0 && pPars->fFirstStop ) - { - if ( pPars->fVerbose ) - printf( "Output %d is trivially SAT.\n", Status.iOut ); - Aig_ManStop( pMiter ); - return 0; - } - if ( Status.nUndec == 0 ) - { - if ( pPars->fVerbose ) - printf( "The problem is solved by structrual hashing.\n" ); - Aig_ManStop( pMiter ); - return 1; - } - } - if ( pPars->fVerbose ) - Cec_MiterStatusPrint( Status, "Strash", clock() - clk ); - // start parameter structures -// Cec_ManSatSetDefaultParams( pParsSat ); -// pParsSat->fFirstStop = pPars->fFirstStop; -// pParsSat->nBTLimit = pPars->nBTLimitBeg; -/* - // try SAT solving - clk = clock(); - pParsSat->nBTLimit *= pPars->nBTlimitMulti; - Status = Cec_SatSolveOutputs( pMiter, pParsSat ); - if ( pPars->fVerbose ) - Cec_MiterStatusPrint( Status, "SAT ", clock() - clk ); - if ( Status.nSat && pParsSat->fFirstStop ) - break; - if ( Status.nUndec == 0 ) - break; -*/ - - Cec_ManCswSetDefaultParams( pParsCsw ); - pCaig = Caig_ManClassesPrepare( pMiter, pParsCsw->nWords, pParsCsw->nRounds ); - for ( i = 0; i < pPars->nIters; i++ ) - { - Cec_ManSatSweepInt( pCaig, pParsCsw ); - i = i; - } - Caig_ManDelete( pCaig ); - Aig_ManStop( pMiter ); - return 1; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/aig/cec2/cecInt.h b/src/aig/cec2/cecInt.h deleted file mode 100644 index ef43e44c..00000000 --- a/src/aig/cec2/cecInt.h +++ /dev/null @@ -1,208 +0,0 @@ -/**CFile**************************************************************** - - FileName [cecInt.h] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Combinatinoal equivalence checking.] - - Synopsis [External declarations.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: cecInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#ifndef __CEC_INT_H__ -#define __CEC_INT_H__ - -//////////////////////////////////////////////////////////////////////// -/// INCLUDES /// -//////////////////////////////////////////////////////////////////////// - -#include "aig.h" -#include "satSolver.h" -#include "bar.h" -#include "cec.h" - -//////////////////////////////////////////////////////////////////////// -/// PARAMETERS /// -//////////////////////////////////////////////////////////////////////// - -#ifdef __cplusplus -extern "C" { -#endif - -//////////////////////////////////////////////////////////////////////// -/// BASIC TYPES /// -//////////////////////////////////////////////////////////////////////// - -typedef struct Cec_ManSat_t_ Cec_ManSat_t; -struct Cec_ManSat_t_ -{ - // parameters - Cec_ParSat_t * pPars; - // AIGs used in the package - Aig_Man_t * pAig; // the AIG whose outputs are considered - Vec_Int_t * vStatus; // status for each output - // SAT solving - sat_solver * pSat; // recyclable SAT solver - int nSatVars; // the counter of SAT variables - int * pSatVars; // mapping of each node into its SAT var - Vec_Ptr_t * vUsedNodes; // nodes whose SAT vars are assigned - int nRecycles; // the number of times SAT solver was recycled - int nCallsSince; // the number of calls since the last recycle - Vec_Ptr_t * vFanins; // fanins of the CNF node - // SAT calls statistics - int nSatUnsat; // the number of proofs - int nSatSat; // the number of failure - int nSatUndec; // the number of timeouts - // runtime stats - int timeSatUnsat; // unsat - int timeSatSat; // sat - int timeSatUndec; // undecided - int timeTotal; // total runtime -}; - -typedef struct Cec_ManCec_t_ Cec_ManCec_t; -struct Cec_ManCec_t_ -{ - // parameters - Cec_ParCec_t * pPars; - // AIGs used in the package - Aig_Man_t * pAig; // the miter for equivalence checking - // mapping of PI/PO nodes - - // counter-example - int * pCex; // counter-example - int iOutput; // the output for this counter-example - - // statistics - -}; - -typedef struct Cec_MtrStatus_t_ Cec_MtrStatus_t; -struct Cec_MtrStatus_t_ -{ - int nInputs; // the total number of inputs - int nNodes; // the total number of nodes - int nOutputs; // the total number of outputs - int nUnsat; // the number of UNSAT outputs - int nSat; // the number of SAT outputs - int nUndec; // the number of undecided outputs - int iOut; // the satisfied output -}; - -// combinational simulation manager -typedef struct Caig_Man_t_ Caig_Man_t; -struct Caig_Man_t_ -{ - // parameters - Aig_Man_t * pAig; // the AIG to be used for simulation - int nWords; // the number of simulation words - // AIG representation - int nPis; // the number of primary inputs - int nPos; // the number of primary outputs - int nNodes; // the number of internal nodes - int nObjs; // nPis + nNodes + nPos + 1 - int * pFans0; // fanin0 for all objects - int * pFans1; // fanin1 for all objects - // simulation info - int * pRefs; // reference counter for each node - unsigned * pSims; // simlulation information for each node - // recycable memory - unsigned * pMems; // allocated simulaton memory - int nWordsAlloc; // the number of allocated entries - int nMems; // the number of used entries - int nMemsMax; // the max number of used entries - int MemFree; // next ABC_FREE entry - // equivalence class representation - int * pReprs; // representatives of each node - int * pNexts; // nexts for each node - // temporaries - Vec_Ptr_t * vSims; // pointers to sim info - Vec_Int_t * vClassOld; // old class numbers - Vec_Int_t * vClassNew; // new class numbers - Vec_Int_t * vRefinedC; // refined const reprs -}; - -//////////////////////////////////////////////////////////////////////// -/// MACRO DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -static inline int Cec_Var2Lit( int Var, int fCompl ) { return Var + Var + fCompl; } -static inline int Cec_Lit2Var( int Lit ) { return Lit >> 1; } -static inline int Cec_LitIsCompl( int Lit ) { return Lit & 1; } -static inline int Cec_LitNot( int Lit ) { return Lit ^ 1; } -static inline int Cec_LitNotCond( int Lit, int c ) { return Lit ^ (int)(c > 0); } -static inline int Cec_LitRegular( int Lit ) { return Lit & ~01; } - -static inline int Cec_ObjSatNum( Cec_ManSat_t * p, Aig_Obj_t * pObj ) { return p->pSatVars[pObj->Id]; } -static inline void Cec_ObjSetSatNum( Cec_ManSat_t * p, Aig_Obj_t * pObj, int Num ) { p->pSatVars[pObj->Id] = Num; } - -static inline Aig_Obj_t * Cec_ObjFraig( Aig_Obj_t * pObj ) { return pObj->pData; } -static inline void Cec_ObjSetFraig( Aig_Obj_t * pObj, Aig_Obj_t * pNode ) { pObj->pData = pNode; } - -static inline int Cec_ObjIsConst1Cand( Aig_Man_t * pAig, Aig_Obj_t * pObj ) -{ - return Aig_ObjRepr(pAig, pObj) == Aig_ManConst1(pAig); -} -static inline void Cec_ObjSetConst1Cand( Aig_Man_t * pAig, Aig_Obj_t * pObj ) -{ - assert( !Cec_ObjIsConst1Cand( pAig, pObj ) ); - Aig_ObjSetRepr( pAig, pObj, Aig_ManConst1(pAig) ); -} - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -/*=== cecAig.c ==========================================================*/ -extern Aig_Man_t * Cec_Duplicate( Aig_Man_t * p ); -extern Aig_Man_t * Cec_DeriveMiter( Aig_Man_t * p0, Aig_Man_t * p1 ); -/*=== cecClass.c ==========================================================*/ -extern Aig_Man_t * Caig_ManSpecReduce( Caig_Man_t * p, int nLevels ); -extern int Caig_ManCompareEqual( unsigned * p0, unsigned * p1, int nWords ); -extern int Caig_ManCompareConst( unsigned * p, int nWords ); -extern void Caig_ManCollectSimsNormal( Caig_Man_t * p, int i ); -extern int Caig_ManClassRefineOne( Caig_Man_t * p, int i, Vec_Ptr_t * vSims ); -extern void Caig_ManProcessRefined( Caig_Man_t * p, Vec_Int_t * vRefined ); -extern void Caig_ManPrintClasses( Caig_Man_t * p, int fVerbose ); -extern Caig_Man_t * Caig_ManClassesPrepare( Aig_Man_t * pAig, int nWords, int nIters ); -/*=== cecCnf.c ==========================================================*/ -extern void Cec_CnfNodeAddToSolver( Cec_ManSat_t * p, Aig_Obj_t * pObj ); -/*=== cecSat.c ==========================================================*/ -extern Cec_MtrStatus_t Cec_SatSolveOutputs( Aig_Man_t * pAig, Cec_ParSat_t * pPars ); -/*=== cecSim.c ==========================================================*/ -extern Caig_Man_t * Caig_ManCreate( Aig_Man_t * pAig ); -extern void Caig_ManDelete( Caig_Man_t * p ); -extern void Caig_ManSimMemRelink( Caig_Man_t * p ); -extern unsigned * Caig_ManSimRead( Caig_Man_t * p, int i ); -extern unsigned * Caig_ManSimRef( Caig_Man_t * p, int i ); -extern unsigned * Caig_ManSimDeref( Caig_Man_t * p, int i ); -extern void Caig_ManSimulateRound( Caig_Man_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t * vInfoCos ); -extern int Cec_ManSimulate( Aig_Man_t * pAig, int nWords, int nIters, int TimeLimit, int fMiter, int fVerbose ); -/*=== cecStatus.c ==========================================================*/ -extern int Cec_OutputStatus( Aig_Man_t * p, Aig_Obj_t * pObj ); -extern Cec_MtrStatus_t Cec_MiterStatus( Aig_Man_t * p ); -extern Cec_MtrStatus_t Cec_MiterStatusTrivial( Aig_Man_t * p ); -extern void Cec_MiterStatusPrint( Cec_MtrStatus_t S, char * pString, int Time ); -/*=== cecSweep.c ==========================================================*/ -extern void Cec_ManSatSweepInt( Caig_Man_t * pMan, Cec_ParCsw_t * pPars ); -extern Aig_Man_t * Cec_ManSatSweep( Aig_Man_t * pAig, Cec_ParCsw_t * pPars ); - -#ifdef __cplusplus -} -#endif - -#endif - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - diff --git a/src/aig/cec2/cecMan.c b/src/aig/cec2/cecMan.c deleted file mode 100644 index 86415c53..00000000 --- a/src/aig/cec2/cecMan.c +++ /dev/null @@ -1,59 +0,0 @@ -/**CFile**************************************************************** - - FileName [cecMan.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Combinatinoal equivalence checking.] - - Synopsis [Manager pcocures.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: cecMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "cecInt.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/aig/cec2/cecSat.c b/src/aig/cec2/cecSat.c deleted file mode 100644 index a999dd97..00000000 --- a/src/aig/cec2/cecSat.c +++ /dev/null @@ -1,250 +0,0 @@ -/**CFile**************************************************************** - - FileName [cecSat.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Combinatinoal equivalence checking.] - - Synopsis [SAT solver calls.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: cecSat.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "cecInt.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Creates the manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Cec_ManSat_t * Cec_ManCreate( Aig_Man_t * pAig, Cec_ParSat_t * pPars ) -{ - Cec_ManSat_t * p; - // create interpolation manager - p = ABC_ALLOC( Cec_ManSat_t, 1 ); - memset( p, 0, sizeof(Cec_ManSat_t) ); - p->pPars = pPars; - p->pAig = pAig; - // SAT solving - p->nSatVars = 1; - p->pSatVars = ABC_CALLOC( int, Aig_ManObjNumMax(pAig) ); - p->vUsedNodes = Vec_PtrAlloc( 1000 ); - p->vFanins = Vec_PtrAlloc( 100 ); - return p; -} - -/**Function************************************************************* - - Synopsis [Frees the manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Cec_ManStop( Cec_ManSat_t * p ) -{ - if ( p->pSat ) - sat_solver_delete( p->pSat ); - Vec_PtrFree( p->vUsedNodes ); - Vec_PtrFree( p->vFanins ); - ABC_FREE( p->pSatVars ); - ABC_FREE( p ); -} - -/**Function************************************************************* - - Synopsis [Recycles the SAT solver.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Cec_ManSatSolverRecycle( Cec_ManSat_t * p ) -{ - int Lit; - if ( p->pSat ) - { - Aig_Obj_t * pObj; - int i; - Vec_PtrForEachEntry( p->vUsedNodes, pObj, i ) - Cec_ObjSetSatNum( p, pObj, 0 ); - Vec_PtrClear( p->vUsedNodes ); -// memset( p->pSatVars, 0, sizeof(int) * Aig_ManObjNumMax(p->pAigTotal) ); - sat_solver_delete( p->pSat ); - } - p->pSat = sat_solver_new(); - sat_solver_setnvars( p->pSat, 1000 ); - // var 0 is not used - // var 1 is reserved for const1 node - add the clause - p->nSatVars = 1; -// p->nSatVars = 0; - Lit = toLit( p->nSatVars ); - if ( p->pPars->fPolarFlip ) - Lit = lit_neg( Lit ); - sat_solver_addclause( p->pSat, &Lit, &Lit + 1 ); - Cec_ObjSetSatNum( p, Aig_ManConst1(p->pAig), p->nSatVars++ ); - - p->nRecycles++; - p->nCallsSince = 0; -} - -/**Function************************************************************* - - Synopsis [Runs equivalence test for the two nodes.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Cec_ManSatCheckNode( Cec_ManSat_t * p, Aig_Obj_t * pNode ) -{ - int nBTLimit = p->pPars->nBTLimit; - int Lit, RetValue, status, clk; - - // sanity checks - assert( !Aig_IsComplement(pNode) ); - - p->nCallsSince++; // experiment with this!!! - - // check if SAT solver needs recycling - if ( p->pSat == NULL || - (p->pPars->nSatVarMax && - p->nSatVars > p->pPars->nSatVarMax && - p->nCallsSince > p->pPars->nCallsRecycle) ) - Cec_ManSatSolverRecycle( p ); - - // if the nodes do not have SAT variables, allocate them - Cec_CnfNodeAddToSolver( p, pNode ); - - // propage unit clauses - if ( p->pSat->qtail != p->pSat->qhead ) - { - status = sat_solver_simplify(p->pSat); - assert( status != 0 ); - assert( p->pSat->qtail == p->pSat->qhead ); - } - - // solve under assumptions - // A = 1; B = 0 OR A = 1; B = 1 - Lit = toLitCond( Cec_ObjSatNum(p,pNode), pNode->fPhase ); - if ( p->pPars->fPolarFlip ) - { - if ( pNode->fPhase ) Lit = lit_neg( Lit ); - } -//Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 ); -clk = clock(); - RetValue = sat_solver_solve( p->pSat, &Lit, &Lit + 1, - (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); - if ( RetValue == l_False ) - { -p->timeSatUnsat += clock() - clk; - Lit = lit_neg( Lit ); - RetValue = sat_solver_addclause( p->pSat, &Lit, &Lit + 1 ); - assert( RetValue ); - p->timeSatUnsat++; - return 1; - } - else if ( RetValue == l_True ) - { -p->timeSatSat += clock() - clk; - p->timeSatSat++; - return 0; - } - else // if ( RetValue == l_Undef ) - { -p->timeSatUndec += clock() - clk; - p->timeSatUndec++; - return -1; - } -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Cec_MtrStatus_t Cec_SatSolveOutputs( Aig_Man_t * pAig, Cec_ParSat_t * pPars ) -{ - Bar_Progress_t * pProgress = NULL; - Cec_MtrStatus_t Status; - Cec_ManSat_t * p; - Aig_Obj_t * pObj; - int i, status; - Status = Cec_MiterStatus( pAig ); - p = Cec_ManCreate( pAig, pPars ); - pProgress = Bar_ProgressStart( stdout, Aig_ManPoNum(pAig) ); - Aig_ManForEachPo( pAig, pObj, i ) - { - Bar_ProgressUpdate( pProgress, i, "SAT..." ); - if ( Cec_OutputStatus(pAig, pObj) ) - continue; - status = Cec_ManSatCheckNode( p, Aig_ObjFanin0(pObj) ); - if ( status == 1 ) - { - Status.nUndec--, Status.nUnsat++; - Aig_ObjPatchFanin0( pAig, pObj, Aig_ManConst0(pAig) ); - } - if ( status == 0 ) - { - Status.nUndec--, Status.nSat++; - Aig_ObjPatchFanin0( pAig, pObj, Aig_ManConst1(pAig) ); - } - if ( status == -1 ) - continue; - // save the pattern (if it is first) - if ( Status.iOut == -1 ) - { - } - // quit if at least one of them is solved - if ( status == 0 && pPars->fFirstStop ) - break; - } - Aig_ManCleanup( pAig ); - Bar_ProgressStop( pProgress ); - printf( " Confs = %8d. Recycles = %6d.\n", p->pPars->nBTLimit, p->nRecycles ); - Cec_ManStop( p ); - return Status; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/aig/cec2/cecSat2.c b/src/aig/cec2/cecSat2.c deleted file mode 100644 index 4f009b25..00000000 --- a/src/aig/cec2/cecSat2.c +++ /dev/null @@ -1,284 +0,0 @@ -/**CFile**************************************************************** - - FileName [cecSat.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Combinational equivalence checking.] - - Synopsis [Backend calling the SAT solver.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 30, 2007.] - - Revision [$Id: cecSat.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "aig.h" -#include "cnf.h" -#include "../../sat/lsat/solver.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Writes CNF into a file.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -solver * Cnf_WriteIntoSolverNew( Cnf_Dat_t * p ) -{ - solver * pSat; - int i, status; - pSat = solver_new(); - for ( i = 0; i < p->nVars; i++ ) - solver_newVar( pSat ); - for ( i = 0; i < p->nClauses; i++ ) - { - if ( !solver_addClause( pSat, p->pClauses[i+1]-p->pClauses[i], p->pClauses[i] ) ) - { - solver_delete( pSat ); - return NULL; - } - } - status = solver_simplify(pSat); - if ( status == 0 ) - { - solver_delete( pSat ); - return NULL; - } - return pSat; -} - -/**Function************************************************************* - - Synopsis [Adds the OR-clause.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Cnf_DataWriteAndClausesNew( void * p, Cnf_Dat_t * pCnf ) -{ -/* - sat_solver * pSat = p; - Aig_Obj_t * pObj; - int i, Lit; - Aig_ManForEachPo( pCnf->pMan, pObj, i ) - { - Lit = toLitCond( pCnf->pVarNums[pObj->Id], 0 ); - if ( !sat_solver_addclause( pSat, &Lit, &Lit+1 ) ) - return 0; - } -*/ - return 1; -} - -/**Function************************************************************* - - Synopsis [Adds the OR-clause.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Cnf_DataWriteOrClauseNew( solver * pSat, Cnf_Dat_t * pCnf ) -{ - Aig_Obj_t * pObj; - int i, * pLits; - pLits = ALLOC( int, Aig_ManPoNum(pCnf->pMan) ); - Aig_ManForEachPo( pCnf->pMan, pObj, i ) - pLits[i] = solver_mkLit_args( pCnf->pVarNums[pObj->Id], 0 ); - if ( !solver_addClause( pSat, Aig_ManPoNum(pCnf->pMan), pLits ) ) - { - free( pLits ); - return 0; - } - free( pLits ); - return 1; -} - -/**Function************************************************************* - - Synopsis [Writes the given clause in a file in DIMACS format.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Sat_SolverPrintStatsNew( FILE * pFile, solver * pSat ) -{ -// printf( "starts : %8d\n", solver_num_assigns(pSat) ); - printf( "vars : %8d\n", solver_num_vars(pSat) ); - printf( "clauses : %8d\n", solver_num_clauses(pSat) ); - printf( "conflicts : %8d\n", solver_num_learnts(pSat) ); -} - -/**Function************************************************************* - - Synopsis [Returns a counter-example.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int * Sat_SolverGetModelNew( solver * pSat, int * pVars, int nVars ) -{ - int * pModel; - int i; - pModel = ALLOC( int, nVars+1 ); - for ( i = 0; i < nVars; i++ ) - { - assert( pVars[i] >= 0 && pVars[i] < solver_num_vars(pSat) ); - pModel[i] = (int)(solver_modelValue_Var( pSat, pVars[i] ) == solver_l_True); - } - return pModel; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Cec_RunSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fFlipBits, int fAndOuts, int fVerbose ) -{ - solver * pSat; - Cnf_Dat_t * pCnf; - int status, RetValue, clk = clock(); - Vec_Int_t * vCiIds; - - assert( Aig_ManRegNum(pMan) == 0 ); - pMan->pData = NULL; - - // derive CNF - pCnf = Cnf_Derive( pMan, Aig_ManPoNum(pMan) ); -// pCnf = Cnf_DeriveSimple( pMan, Aig_ManPoNum(pMan) ); - - // convert into SAT solver - pSat = Cnf_WriteIntoSolverNew( pCnf ); - if ( pSat == NULL ) - { - Cnf_DataFree( pCnf ); - return 1; - } - - - if ( fAndOuts ) - { - assert( 0 ); - // assert each output independently - if ( !Cnf_DataWriteAndClausesNew( pSat, pCnf ) ) - { - solver_delete( pSat ); - Cnf_DataFree( pCnf ); - return 1; - } - } - else - { - // add the OR clause for the outputs - if ( !Cnf_DataWriteOrClauseNew( pSat, pCnf ) ) - { - solver_delete( pSat ); - Cnf_DataFree( pCnf ); - return 1; - } - } - vCiIds = Cnf_DataCollectPiSatNums( pCnf, pMan ); - Cnf_DataFree( pCnf ); - - -// printf( "Created SAT problem with %d variable and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) ); -// PRT( "Time", clock() - clk ); - - // simplify the problem - clk = clock(); - status = solver_simplify(pSat); -// printf( "Simplified the problem to %d variables and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) ); -// PRT( "Time", clock() - clk ); - if ( status == 0 ) - { - Vec_IntFree( vCiIds ); - solver_delete( pSat ); -// printf( "The problem is UNSATISFIABLE after simplification.\n" ); - return 1; - } - - // solve the miter - clk = clock(); - if ( fVerbose ) - solver_set_verbosity( pSat, 1 ); - status = solver_solve( pSat, 0, NULL ); - if ( status == solver_l_Undef ) - { -// printf( "The problem timed out.\n" ); - RetValue = -1; - } - else if ( status == solver_l_True ) - { -// printf( "The problem is SATISFIABLE.\n" ); - RetValue = 0; - } - else if ( status == solver_l_False ) - { -// printf( "The problem is UNSATISFIABLE.\n" ); - RetValue = 1; - } - else - assert( 0 ); -// PRT( "SAT sat_solver time", clock() - clk ); -// printf( "The number of conflicts = %d.\n", (int)pSat->sat_solver_stats.conflicts ); - - // if the problem is SAT, get the counterexample - if ( status == solver_l_True ) - { - pMan->pData = Sat_SolverGetModelNew( pSat, vCiIds->pArray, vCiIds->nSize ); - } - // free the sat_solver - if ( fVerbose ) - Sat_SolverPrintStatsNew( stdout, pSat ); -//sat_solver_store_write( pSat, "trace.cnf" ); -//sat_solver_store_free( pSat ); - solver_delete( pSat ); - Vec_IntFree( vCiIds ); - return RetValue; -} - - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - diff --git a/src/aig/cec2/cecSim.c b/src/aig/cec2/cecSim.c deleted file mode 100644 index 4fedbddc..00000000 --- a/src/aig/cec2/cecSim.c +++ /dev/null @@ -1,447 +0,0 @@ -/**CFile**************************************************************** - - FileName [cecSim.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Combinatinoal equivalence checking.] - - Synopsis [AIG simulation.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: cecSim.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "cecInt.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Creates fast simulation manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Caig_Man_t * Caig_ManCreate( Aig_Man_t * pAig ) -{ - Caig_Man_t * p; - Aig_Obj_t * pObj; - int i; - assert( Aig_ManHasNoGaps(pAig) ); - Aig_ManCleanData( pAig ); - p = (Caig_Man_t *)ABC_ALLOC( Caig_Man_t, 1 ); - memset( p, 0, sizeof(Caig_Man_t) ); - p->pAig = pAig; - p->nPis = Aig_ManPiNum(pAig); - p->nPos = Aig_ManPoNum(pAig); - p->nNodes = Aig_ManNodeNum(pAig); - p->nObjs = p->nPis + p->nPos + p->nNodes + 1; - p->pFans0 = ABC_ALLOC( int, p->nObjs ); - p->pFans1 = ABC_ALLOC( int, p->nObjs ); - p->pRefs = ABC_ALLOC( int, p->nObjs ); - p->pSims = ABC_CALLOC( unsigned, p->nObjs ); - // add objects - Aig_ManForEachObj( pAig, pObj, i ) - { - p->pRefs[i] = Aig_ObjRefs(pObj); - if ( Aig_ObjIsNode(pObj) ) - { - p->pFans0[i] = (Aig_ObjFaninId0(pObj) << 1) | Aig_ObjFaninC0(pObj); - p->pFans1[i] = (Aig_ObjFaninId1(pObj) << 1) | Aig_ObjFaninC1(pObj); - } - else if ( Aig_ObjIsPo(pObj) ) - { - p->pFans0[i] = (Aig_ObjFaninId0(pObj) << 1) | Aig_ObjFaninC0(pObj); - p->pFans1[i] = -1; - } - else - { - assert( Aig_ObjIsPi(pObj) || Aig_ObjIsConst1(pObj) ); - p->pFans0[i] = -1; - p->pFans1[i] = -1; - } - } - // temporaries - p->vClassOld = Vec_IntAlloc( 1000 ); - p->vClassNew = Vec_IntAlloc( 1000 ); - p->vRefinedC = Vec_IntAlloc( 10000 ); - p->vSims = Vec_PtrAlloc( 1000 ); - return p; -} - -/**Function************************************************************* - - Synopsis [Creates fast simulation manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Caig_ManDelete( Caig_Man_t * p ) -{ - Vec_IntFree( p->vClassOld ); - Vec_IntFree( p->vClassNew ); - Vec_IntFree( p->vRefinedC ); - Vec_PtrFree( p->vSims ); - ABC_FREE( p->pFans0 ); - ABC_FREE( p->pFans1 ); - ABC_FREE( p->pRefs ); - ABC_FREE( p->pSims ); - ABC_FREE( p->pMems ); - ABC_FREE( p->pReprs ); - ABC_FREE( p->pNexts ); - ABC_FREE( p ); -} - -/**Function************************************************************* - - Synopsis [References simulation info.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Caig_ManSimMemRelink( Caig_Man_t * p ) -{ - int * pPlace, Ent; - pPlace = &p->MemFree; - for ( Ent = p->nMems * (p->nWords + 1); - Ent + p->nWords + 1 < p->nWordsAlloc; - Ent += p->nWords + 1 ) - { - *pPlace = Ent; - pPlace = p->pMems + Ent; - } - *pPlace = 0; -} - -/**Function************************************************************* - - Synopsis [References simulation info.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -unsigned * Caig_ManSimRead( Caig_Man_t * p, int i ) -{ - assert( i && p->pSims[i] > 0 ); - return p->pMems + p->pSims[i]; -} - -/**Function************************************************************* - - Synopsis [References simulation info.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -unsigned * Caig_ManSimRef( Caig_Man_t * p, int i ) -{ - unsigned * pSim; - assert( p->pSims[i] == 0 ); - if ( p->MemFree == 0 ) - { - if ( p->nWordsAlloc == 0 ) - { - assert( p->pMems == NULL ); - p->nWordsAlloc = (1<<17); // -> 1Mb - p->nMems = 1; - } - p->nWordsAlloc *= 2; - p->pMems = ABC_REALLOC( unsigned, p->pMems, p->nWordsAlloc ); - Caig_ManSimMemRelink( p ); - } - p->pSims[i] = p->MemFree; - pSim = p->pMems + p->MemFree; - p->MemFree = pSim[0]; - pSim[0] = p->pRefs[i]; - p->nMems++; - if ( p->nMemsMax < p->nMems ) - p->nMemsMax = p->nMems; - return pSim; -} - -/**Function************************************************************* - - Synopsis [Dereference simulaton info.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -unsigned * Caig_ManSimDeref( Caig_Man_t * p, int i ) -{ - unsigned * pSim; - assert( p->pSims[i] > 0 ); - pSim = p->pMems + p->pSims[i]; - if ( --pSim[0] == 0 ) - { - pSim[0] = p->MemFree; - p->MemFree = p->pSims[i]; - p->pSims[i] = 0; - p->nMems--; - } - return pSim; -} - -/**Function************************************************************* - - Synopsis [Simulates one round.] - - Description [Returns the number of PO entry if failed; 0 otherwise.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Caig_ManSimulateRound( Caig_Man_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t * vInfoCos ) -{ - unsigned * pRes0, * pRes1, * pRes; - int i, w, iCiId = 0, iCoId = 0; - int nWords = Vec_PtrReadWordsSimInfo( vInfoCis ); - assert( vInfoCos == NULL || nWords == Vec_PtrReadWordsSimInfo(vInfoCos) ); - Vec_IntClear( p->vRefinedC ); - if ( p->pRefs[0] ) - { - pRes = Caig_ManSimRef( p, 0 ); - for ( w = 1; w <= nWords; w++ ) - pRes[w] = ~0; - } - for ( i = 1; i < p->nObjs; i++ ) - { - if ( p->pFans0[i] == -1 ) // ci always has zero first fanin - { - if ( p->pRefs[i] == 0 ) - { - iCiId++; - continue; - } - pRes = Caig_ManSimRef( p, i ); - pRes0 = Vec_PtrEntry( vInfoCis, iCiId++ ); - for ( w = 1; w <= nWords; w++ ) - pRes[w] = pRes0[w-1]; - goto references; - } - if ( p->pFans1[i] == -1 ) // co always has non-zero 1st fanin and zero 2nd fanin - { - pRes0 = Caig_ManSimDeref( p, Cec_Lit2Var(p->pFans0[i]) ); - if ( vInfoCos ) - { - pRes = Vec_PtrEntry( vInfoCos, iCoId++ ); - if ( Cec_LitIsCompl(p->pFans0[i]) ) - for ( w = 1; w <= nWords; w++ ) - pRes[w-1] = ~pRes0[w]; - else - for ( w = 1; w <= nWords; w++ ) - pRes[w-1] = pRes0[w]; - } - continue; - } - assert( p->pRefs[i] ); - pRes = Caig_ManSimRef( p, i ); - pRes0 = Caig_ManSimDeref( p, Cec_Lit2Var(p->pFans0[i]) ); - pRes1 = Caig_ManSimDeref( p, Cec_Lit2Var(p->pFans1[i]) ); - if ( Cec_LitIsCompl(p->pFans0[i]) ) - { - if ( Cec_LitIsCompl(p->pFans1[i]) ) - for ( w = 1; w <= nWords; w++ ) - pRes[w] = ~(pRes0[w] | pRes1[w]); - else - for ( w = 1; w <= nWords; w++ ) - pRes[w] = ~pRes0[w] & pRes1[w]; - } - else - { - if ( Cec_LitIsCompl(p->pFans1[i]) ) - for ( w = 1; w <= nWords; w++ ) - pRes[w] = pRes0[w] & ~pRes1[w]; - else - for ( w = 1; w <= nWords; w++ ) - pRes[w] = pRes0[w] & pRes1[w]; - } -references: - if ( p->pReprs == NULL ) - continue; - // if this node is candidate constant, collect it - if ( p->pReprs[i] == 0 && !Caig_ManCompareConst(pRes + 1, nWords) ) - { - pRes[0]++; - Vec_IntPush( p->vRefinedC, i ); - } - // if the node belongs to a class, save it - if ( p->pReprs[i] > 0 || p->pNexts[i] > 0 ) - pRes[0]++; - // if this is the last node of the class, process it - if ( p->pReprs[i] > 0 && p->pNexts[i] == 0 ) - { - Caig_ManCollectSimsNormal( p, p->pReprs[i] ); - Caig_ManClassRefineOne( p, p->pReprs[i], p->vSims ); - } - } - if ( Vec_IntSize(p->vRefinedC) > 0 ) - Caig_ManProcessRefined( p, p->vRefinedC ); - assert( iCiId == p->nPis ); - assert( vInfoCos == NULL || iCoId == p->nPos ); - assert( p->nMems == 1 ); -/* - if ( p->nMems > 1 ) - { - for ( i = 1; i < p->nObjs; i++ ) - if ( p->pSims[i] ) - { - int x = 0; - } - } -*/ -} - -/**Function************************************************************* - - Synopsis [Returns the number of PO that failed.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Cec_ManFindPo( Vec_Ptr_t * vInfo, int nWords ) -{ - unsigned * pInfo; - int i, w; - Vec_PtrForEachEntry( vInfo, pInfo, i ) - for ( w = 0; w < nWords; w++ ) - if ( pInfo[w] != 0 ) - return i; - return -1; -} - -/**Function************************************************************* - - Synopsis [Returns 1 if the bug is detected, 0 otherwise.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Cec_ManSimulate( Aig_Man_t * pAig, int nWords, int nIters, int TimeLimit, int fMiter, int fVerbose ) -{ - Caig_Man_t * p; - Cec_MtrStatus_t Status; - Vec_Ptr_t * vInfoCis, * vInfoCos = NULL; - int i, RetValue = 0, clk, clkTotal = clock(); -/* - p = Caig_ManClassesPrepare( pAig, nWords, nIters ); -// if ( fVerbose ) - printf( "Maxcut = %6d. AIG mem = %8.3f Mb. Sim mem = %8.3f Mb.\n", - p->nMemsMax, - 1.0*(p->nObjs * 14)/(1<<20), - 1.0*(p->nMemsMax * (nWords+1))/(1<<20) ); - Caig_ManDelete( p ); - return 0; -*/ - if ( fMiter ) - { - Status = Cec_MiterStatus( pAig ); - if ( Status.nSat > 0 ) - { - printf( "Miter is trivially satisfiable (output %d).\n", Status.iOut ); - return 1; - } - if ( Status.nUndec == 0 ) - { - printf( "Miter is trivially unsatisfiable.\n" ); - return 0; - } - } - Aig_ManRandom( 1 ); - p = Caig_ManCreate( pAig ); - p->nWords = nWords; - if ( fMiter ) - vInfoCos = Vec_PtrAllocSimInfo( Aig_ManPiNum(pAig), nWords ); - for ( i = 0; i < nIters; i++ ) - { - clk = clock(); - vInfoCis = Vec_PtrAllocSimInfo( Aig_ManPiNum(pAig), nWords ); - Aig_ManRandomInfo( vInfoCis, 0, nWords ); - Caig_ManSimulateRound( p, vInfoCis, vInfoCos ); - Vec_PtrFree( vInfoCis ); - if ( fVerbose ) - { - printf( "Iter %3d out of %3d and timeout %3d sec. ", i+1, nIters, TimeLimit ); - printf("Time = %7.2f sec\r", (1.0*clock()-clkTotal)/CLOCKS_PER_SEC); - } - if ( fMiter ) - { - int iOut = Cec_ManFindPo( vInfoCos, nWords ); - if ( iOut >= 0 ) - { - if ( fVerbose ) - printf( "Miter is satisfiable after simulation (output %d).\n", iOut ); - RetValue = 1; - break; - } - } - if ( (clock() - clk)/CLOCKS_PER_SEC >= TimeLimit ) - { - printf( "No bug detected after %d rounds with time limit %d seconds.\n", i+1, TimeLimit ); - break; - } - } - if ( fVerbose ) - printf( "Maxcut = %6d. AIG mem = %8.3f Mb. Sim mem = %8.3f Mb.\n", - p->nMemsMax, - 1.0*(p->nObjs * 14)/(1<<20), - 1.0*(p->nMemsMax * 4 * (nWords+1))/(1<<20) ); - Caig_ManDelete( p ); - if ( vInfoCos ) - Vec_PtrFree( vInfoCos ); - return RetValue > 0; -} - - - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/aig/cec2/cecStatus.c b/src/aig/cec2/cecStatus.c deleted file mode 100644 index 79d6ec66..00000000 --- a/src/aig/cec2/cecStatus.c +++ /dev/null @@ -1,187 +0,0 @@ -/**CFile**************************************************************** - - FileName [cecStatus.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Combinatinoal equivalence checking.] - - Synopsis [Miter status.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: cecStatus.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "cecInt.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Returns 1 if the output is known.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Cec_OutputStatus( Aig_Man_t * p, Aig_Obj_t * pObj ) -{ - Aig_Obj_t * pChild; - assert( Aig_ObjIsPo(pObj) ); - pChild = Aig_ObjChild0(pObj); - // check if the output is constant 0 - if ( pChild == Aig_ManConst0(p) ) - return 1; - // check if the output is constant 1 - if ( pChild == Aig_ManConst1(p) ) - return 1; - // check if the output is a primary input - if ( Aig_ObjIsPi(Aig_Regular(pChild)) ) - return 1; - // check if the output is 1 for the 0000 pattern - if ( Aig_Regular(pChild)->fPhase != (unsigned)Aig_IsComplement(pChild) ) - return 1; - return 0; -} - -/**Function************************************************************* - - Synopsis [Returns number of used inputs.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Cec_CountInputs( Aig_Man_t * p ) -{ - Aig_Obj_t * pObj; - int i, Counter = 0; - Aig_ManForEachPi( p, pObj, i ) - Counter += (int)(pObj->nRefs > 0); - return Counter; -} - -/**Function************************************************************* - - Synopsis [Checks the status of the miter.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Cec_MtrStatus_t Cec_MiterStatus( Aig_Man_t * p ) -{ - Cec_MtrStatus_t Status; - Aig_Obj_t * pObj, * pChild; - int i; - assert( p->nRegs == 0 ); - memset( &Status, 0, sizeof(Cec_MtrStatus_t) ); - Status.iOut = -1; - Status.nInputs = Cec_CountInputs( p ); - Status.nNodes = Aig_ManNodeNum( p ); - Status.nOutputs = Aig_ManPoNum(p); - Aig_ManForEachPo( p, pObj, i ) - { - pChild = Aig_ObjChild0(pObj); - // check if the output is constant 0 - if ( pChild == Aig_ManConst0(p) ) - Status.nUnsat++; - // check if the output is constant 1 - else if ( pChild == Aig_ManConst1(p) ) - { - Status.nSat++; - if ( Status.iOut == -1 ) - Status.iOut = i; - } - // check if the output is a primary input - else if ( Aig_ObjIsPi(Aig_Regular(pChild)) ) - { - Status.nSat++; - if ( Status.iOut == -1 ) - Status.iOut = i; - } - // check if the output is 1 for the 0000 pattern - else if ( Aig_Regular(pChild)->fPhase != (unsigned)Aig_IsComplement(pChild) ) - { - Status.nSat++; - if ( Status.iOut == -1 ) - Status.iOut = i; - } - else - Status.nUndec++; - } - return Status; -} - -/**Function************************************************************* - - Synopsis [Checks the status of the miter.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Cec_MtrStatus_t Cec_MiterStatusTrivial( Aig_Man_t * p ) -{ - Cec_MtrStatus_t Status; - memset( &Status, 0, sizeof(Cec_MtrStatus_t) ); - Status.iOut = -1; - Status.nInputs = Aig_ManPiNum(p); - Status.nNodes = Aig_ManNodeNum( p ); - Status.nOutputs = Aig_ManPoNum(p); - Status.nUndec = Aig_ManPoNum(p); - return Status; -} - -/**Function************************************************************* - - Synopsis [Prints the status of the miter.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Cec_MiterStatusPrint( Cec_MtrStatus_t S, char * pString, int Time ) -{ - printf( "%s:", pString ); - printf( " I =%6d", S.nInputs ); - printf( " N =%7d", S.nNodes ); - printf( " " ); - printf( " ? =%6d", S.nUndec ); - printf( " U =%6d", S.nUnsat ); - printf( " S =%6d", S.nSat ); - printf(" %7.2f sec\n", (float)(Time)/(float)(CLOCKS_PER_SEC)); -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/aig/cec2/cecSweep.c b/src/aig/cec2/cecSweep.c deleted file mode 100644 index d7d85b02..00000000 --- a/src/aig/cec2/cecSweep.c +++ /dev/null @@ -1,582 +0,0 @@ -/**CFile**************************************************************** - - FileName [cecSweep.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Combinatinoal equivalence checking.] - - Synopsis [Pattern accumulation.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: cecSweep.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "cecInt.h" -#include "satSolver.h" -#include "cnf.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -typedef struct Cec_ManCsw_t_ Cec_ManCsw_t; -struct Cec_ManCsw_t_ -{ - // parameters - Cec_ParCsw_t * pPars; // parameters - Caig_Man_t * p; // AIG and simulation manager - // mapping into copy - Aig_Obj_t ** pCopy; // the copy of nodes - Vec_Int_t * vCopies; // the nodes copied in the last round - char * pProved; // tells if the given node is proved - char * pProvedNow; // tells if the given node is proved - int * pLevel; // level of the nodes - // collected patterns - Vec_Ptr_t * vInfo; // simulation info accumulated - Vec_Ptr_t * vPres; // simulation presence accumulated - Vec_Ptr_t * vInfoAll; // vector of vectors of simulation info - // temporaries - Vec_Int_t * vPiNums; // primary input numbers - Vec_Int_t * vPoNums; // primary output numbers - Vec_Int_t * vPat; // one counter-example - Vec_Ptr_t * vSupp; // support of one node -}; - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Adds pattern to storage.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Cec_ManSavePattern( Cec_ManCsw_t * p, Vec_Int_t * vPat ) -{ - unsigned * pInfo, * pPres; - int nPatsAlloc, iLit, i, c; - assert( p->p->nWords == Vec_PtrReadWordsSimInfo(p->vInfo) ); - // find next empty place - nPatsAlloc = 32 * p->p->nWords; - for ( c = 0; c < nPatsAlloc; c++ ) - { - Vec_IntForEachEntry( vPat, iLit, i ) - { - pPres = Vec_PtrEntry( p->vPres, Cec_Lit2Var(iLit) ); - if ( Aig_InfoHasBit( pPres, c ) ) - break; - } - if ( i == Vec_IntSize(vPat) ) - break; - } - // increase the size if needed - if ( c == nPatsAlloc ) - { - p->vInfo = Vec_PtrAllocSimInfo( p->p->nPis, p->p->nWords ); - Vec_PtrCleanSimInfo( p->vInfo, 0, p->p->nWords ); - Vec_PtrCleanSimInfo( p->vPres, 0, p->p->nWords ); - Vec_PtrPush( p->vInfoAll, p->vInfo ); - c = 0; - } - // save the pattern - Vec_IntForEachEntry( vPat, iLit, i ) - { - pPres = Vec_PtrEntry( p->vPres, Cec_Lit2Var(iLit) ); - pInfo = Vec_PtrEntry( p->vInfo, Cec_Lit2Var(iLit) ); - Aig_InfoSetBit( pPres, c ); - if ( !Cec_LitIsCompl(iLit) ) - Aig_InfoSetBit( pInfo, c ); - } -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Aig_Obj_t * Cec_ManCswCreatePartition_rec( Aig_Man_t * pAig, Cec_ManCsw_t * p, int i ) -{ - Aig_Obj_t * pRes0, * pRes1; - if ( p->pCopy[i] ) - return p->pCopy[i]; - Vec_IntPush( p->vCopies, i ); - if ( p->p->pFans0[i] == -1 ) // pi - { - Vec_IntPush( p->vPiNums, Aig_ObjPioNum( Aig_ManObj(p->p->pAig, i) ) ); - return p->pCopy[i] = Aig_ObjCreatePi( pAig ); - } - assert( p->p->pFans0[i] && p->p->pFans1[i] ); - pRes0 = Cec_ManCswCreatePartition_rec( pAig, p, Cec_Lit2Var(p->p->pFans0[i]) ); - pRes0 = Aig_NotCond( pRes0, Cec_LitIsCompl(p->p->pFans0[i]) ); - pRes1 = Cec_ManCswCreatePartition_rec( pAig, p, Cec_Lit2Var(p->p->pFans1[i]) ); - pRes1 = Aig_NotCond( pRes1, Cec_LitIsCompl(p->p->pFans1[i]) ); - return p->pCopy[i] = Aig_And( pAig, pRes0, pRes1 ); -} - -/**Function************************************************************* - - Synopsis [Creates dynamic partition.] - - Description [PIs point to node IDs. POs point to node IDs.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Aig_Man_t * Cec_ManCswCreatePartition( Cec_ManCsw_t * p, int * piStart, int nMitersMin, int nNodesMin, int nLevelMax ) -{ - Caig_Man_t * pMan = p->p; - Aig_Man_t * pAig; - Aig_Obj_t * pRepr, * pNode, * pMiter, * pTerm; - int i, iNode, Counter = 0; - assert( p->pCopy && p->vCopies ); - // clear previous marks - Vec_IntForEachEntry( p->vCopies, iNode, i ) - p->pCopy[iNode] = NULL; - Vec_IntClear( p->vCopies ); - // iterate through nodes starting from the given one - pAig = Aig_ManStart( nNodesMin ); - p->pCopy[0] = Aig_ManConst1(pAig); - Vec_IntPush( p->vCopies, 0 ); - for ( i = *piStart; i < pMan->nObjs; i++ ) - { - if ( pMan->pFans0[i] == -1 ) // pi always has zero first fanin - continue; - if ( pMan->pFans1[i] == -1 ) // po always has non-zero 1st fanin and zero 2nd fanin - continue; - if ( pMan->pReprs[i] < 0 ) - continue; - if ( p->pPars->nLevelMax && (p->pLevel[i] > p->pPars->nLevelMax || p->pLevel[pMan->pReprs[i]] > p->pPars->nLevelMax) ) - continue; - // create cones - pRepr = Cec_ManCswCreatePartition_rec( pAig, p, pMan->pReprs[i] ); - pNode = Cec_ManCswCreatePartition_rec( pAig, p, i ); - // skip if they are the same - if ( Aig_Regular(pRepr) == Aig_Regular(pNode) ) - { - p->pProvedNow[i] = 1; - continue; - } - // perform speculative reduction - assert( p->pCopy[i] == pNode ); - p->pCopy[i] = Aig_NotCond( pRepr, Aig_ObjPhaseReal(pRepr) ^ Aig_ObjPhaseReal(pNode) ); - if ( p->pProved[i] ) - { - p->pProvedNow[i] = 1; - continue; - } - pMiter = Aig_Exor( pAig, pRepr, pNode ); - pTerm = Aig_ObjCreatePo( pAig, Aig_NotCond(pMiter, Aig_ObjPhaseReal(pMiter)) ); - Vec_IntPush( p->vPoNums, i ); - if ( ++Counter > nMitersMin && Aig_ManObjNum(pAig) > nNodesMin ) - break; - } - *piStart = i + 1; - Aig_ManSetRegNum( pAig, 0 ); - Aig_ManCleanup( pAig ); - return pAig; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Cec_ManSatDerivePattern( Cec_ManCsw_t * p, Aig_Man_t * pAig, Aig_Obj_t * pRoot, Cnf_Dat_t * pCnf, sat_solver * pSat ) -{ - Aig_Obj_t * pObj; - int i, Value, iVar; - assert( Aig_ObjIsPo(pRoot) ); - Aig_SupportNodes( pAig, &pRoot, 1, p->vSupp ); - Vec_IntClear( p->vPat ); - Vec_PtrForEachEntry( p->vSupp, pObj, i ) - { - assert( Aig_ObjIsPi(pObj) ); - Value = sat_solver_var_value( pSat, pCnf->pVarNums[pObj->Id] ); - iVar = Vec_IntEntry( p->vPiNums, Aig_ObjPioNum(pObj) ); - assert( iVar >= 0 && iVar < p->p->nPis ); - Vec_IntPush( p->vPat, Cec_Var2Lit( iVar, !Value ) ); - } -} - -/**Function************************************************************* - - Synopsis [Creates level.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Cec_ManCreateLevel( Cec_ManCsw_t * p ) -{ - Aig_Obj_t * pObj; - int i; - assert( p->pLevel == NULL ); - p->pLevel = ABC_ALLOC( int, p->p->nObjs ); - Aig_ManForEachObj( p->p->pAig, pObj, i ) - p->pLevel[i] = Aig_ObjLevel(pObj); -} - -/**Function************************************************************* - - Synopsis [Creates the manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Cec_ManCsw_t * Cec_ManCswCreate( Caig_Man_t * pMan, Cec_ParCsw_t * pPars ) -{ - Cec_ManCsw_t * p; - // create interpolation manager - p = ABC_ALLOC( Cec_ManCsw_t, 1 ); - memset( p, 0, sizeof(Cec_ManCsw_t) ); - p->pPars = pPars; - p->p = pMan; - // internal storage - p->vCopies = Vec_IntAlloc( 10000 ); - p->pCopy = ABC_CALLOC( Aig_Obj_t *, pMan->nObjs ); - p->pProved = ABC_CALLOC( char, pMan->nObjs ); - p->pProvedNow = ABC_CALLOC( char, pMan->nObjs ); - // temporaries - p->vPat = Vec_IntAlloc( 1000 ); - p->vSupp = Vec_PtrAlloc( 1000 ); - p->vPiNums = Vec_IntAlloc( 1000 ); - p->vPoNums = Vec_IntAlloc( 1000 ); - if ( pPars->nLevelMax ) - Cec_ManCreateLevel( p ); - return p; -} - -/**Function************************************************************* - - Synopsis [Frees the manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Cec_ManCswStop( Cec_ManCsw_t * p ) -{ - Vec_IntFree( p->vPiNums ); - Vec_IntFree( p->vPoNums ); - Vec_PtrFree( p->vSupp ); - Vec_IntFree( p->vPat ); - Vec_IntFree( p->vCopies ); - Vec_PtrFree( p->vPres ); - Vec_VecFree( (Vec_Vec_t *)p->vInfoAll ); - ABC_FREE( p->pLevel ); - ABC_FREE( p->pCopy ); - ABC_FREE( p->pProved ); - ABC_FREE( p->pProvedNow ); - ABC_FREE( p ); -} - - -/**Function************************************************************* - - Synopsis [Cleans the manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Cec_ManCleanSimInfo( Cec_ManCsw_t * p ) -{ - if ( p->vInfoAll ) - Vec_VecFree( (Vec_Vec_t *)p->vInfoAll ); - if ( p->vPres ) - Vec_PtrFree( p->vPres ); - p->vInfoAll = Vec_PtrAlloc( 100 ); - p->vInfo = Vec_PtrAllocSimInfo( p->p->nPis, p->pPars->nWords ); - p->vPres = Vec_PtrAllocSimInfo( p->p->nPis, p->pPars->nWords ); - Vec_PtrCleanSimInfo( p->vInfo, 0, p->p->nWords ); - Vec_PtrCleanSimInfo( p->vPres, 0, p->p->nWords ); - Vec_PtrPush( p->vInfoAll, p->vInfo ); -} - -/**Function************************************************************* - - Synopsis [Update information about proved nodes.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Cec_ManCountProved( char * pArray, int nSize ) -{ - int i, Counter = 0; - for ( i = 0; i < nSize; i++ ) - Counter += (pArray[i] == 1); - return Counter; -} - -/**Function************************************************************* - - Synopsis [Update information about proved nodes.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Cec_ManCountDisproved( char * pArray, int nSize ) -{ - int i, Counter = 0; - for ( i = 0; i < nSize; i++ ) - Counter += (pArray[i] == -1); - return Counter; -} - -/**Function************************************************************* - - Synopsis [Update information about proved nodes.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Cec_ManCountTimedout( char * pArray, int nSize ) -{ - int i, Counter = 0; - for ( i = 0; i < nSize; i++ ) - Counter += (pArray[i] == -2); - return Counter; -} - -/**Function************************************************************* - - Synopsis [Update information about proved nodes.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Cec_ManUpdateProved( Cec_ManCsw_t * p ) -{ - Caig_Man_t * pMan = p->p; - int i; - for ( i = 1; i < pMan->nObjs; i++ ) - { - if ( pMan->pFans0[i] == -1 ) // pi always has zero first fanin - continue; - if ( pMan->pFans1[i] == -1 ) // po always has non-zero 1st fanin and zero 2nd fanin - continue; - if ( p->pProvedNow[Cec_Lit2Var(pMan->pFans0[i])] < 0 || - p->pProvedNow[Cec_Lit2Var(pMan->pFans1[i])] < 0 ) - p->pProvedNow[i] = -1; - if ( pMan->pReprs[i] < 0 ) - { - assert( p->pProvedNow[i] <= 0 ); - continue; - } - if ( p->pProved[i] ) - { - assert( p->pProvedNow[i] == 1 ); - continue; - } - if ( p->pProvedNow[i] == 1 ) - p->pProved[i] = 1; - } -} - -/**Function************************************************************* - - Synopsis [Creates dynamic partition.] - - Description [PIs point to node IDs. POs point to node IDs.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Cec_ManSatSweepRound( Cec_ManCsw_t * p ) -{ - Bar_Progress_t * pProgress = NULL; - Vec_Ptr_t * vInfo; - Aig_Man_t * pAig, * pTemp; - Aig_Obj_t * pObj; - Cnf_Dat_t * pCnf; - sat_solver * pSat; - int i, Lit, iNode, iStart, status; - int nProved, nDisproved, nTimedout, nBefore, nAfter, nRecycles = 0; - int clk = clock(); - Cec_ManCleanSimInfo( p ); - memset( p->pProvedNow, 0, sizeof(char) * p->p->nObjs ); - pProgress = Bar_ProgressStart( stdout, p->p->nObjs ); - for ( iStart = 1; iStart < p->p->nObjs; ) - { - Bar_ProgressUpdate( pProgress, iStart, "Sweep..." ); - Vec_IntClear( p->vPiNums ); - Vec_IntClear( p->vPoNums ); - // generate AIG, synthesize, convert to CNF, and solve - pAig = Cec_ManCswCreatePartition( p, &iStart, p->pPars->nCallsRecycle, p->pPars->nSatVarMax, p->pPars->nLevelMax ); - Aig_ManPrintStats( pAig ); - - if ( p->pPars->fRewriting ) - { - pAig = Dar_ManRwsat( pTemp = pAig, 1, 0 ); - Aig_ManStop( pTemp ); - } - pCnf = Cnf_Derive( pAig, Aig_ManPoNum(pAig) ); - pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); - Aig_ManForEachPo( pAig, pObj, i ) - { - iNode = Vec_IntEntry( p->vPoNums, i ); - Lit = toLitCond( pCnf->pVarNums[pObj->Id], 0 ); - status = sat_solver_solve( pSat, &Lit, &Lit + 1, (ABC_INT64_T)p->pPars->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); - if ( status == l_False ) - p->pProvedNow[iNode] = 1; - else if ( status == l_Undef ) - p->pProvedNow[iNode] = -2; - else if ( status == l_True ) - { - p->pProvedNow[iNode] = -1; - Cec_ManSatDerivePattern( p, pAig, pObj, pCnf, pSat ); - Cec_ManSavePattern( p, p->vPat ); - } - } - // clean up - Aig_ManStop( pAig ); - Cnf_DataFree( pCnf ); - sat_solver_delete( pSat ); - nRecycles++; - } - Bar_ProgressStop( pProgress ); - // collect statistics - nProved = Cec_ManCountProved( p->pProvedNow, p->p->nObjs ); - nDisproved = Cec_ManCountDisproved( p->pProvedNow, p->p->nObjs ); - nTimedout = Cec_ManCountTimedout( p->pProvedNow, p->p->nObjs ); - nBefore = Cec_ManCountProved( p->pProved, p->p->nObjs ); - Cec_ManUpdateProved( p ); - nAfter = Cec_ManCountProved( p->pProved, p->p->nObjs ); - printf( "Pr =%6d. Cex =%6d. Fail =%6d. Bef =%6d. Aft =%6d. Rcl =%4d.", - nProved, nDisproved, nTimedout, nBefore, nAfter, nRecycles ); - ABC_PRT( "Time", clock() - clk ); - // resimulate with the collected information - Vec_PtrForEachEntry( p->vInfoAll, vInfo, i ) - Caig_ManSimulateRound( p->p, vInfo, NULL ); -Caig_ManPrintClasses( p->p, 0 ); -} - -/**Function************************************************************* - - Synopsis [Performs one round of sweeping.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Cec_ManSatSweepInt( Caig_Man_t * pMan, Cec_ParCsw_t * pPars ) -{ - Cec_ManCsw_t * p; - p = Cec_ManCswCreate( pMan, pPars ); - Cec_ManSatSweepRound( p ); - Cec_ManCswStop( p ); -} - - -/**Function************************************************************* - - Synopsis [Performs equivalence checking.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Aig_Man_t * Cec_ManTrasferReprs( Aig_Man_t * pAig, Caig_Man_t * pCaig ) -{ - return NULL; -} - -/**Function************************************************************* - - Synopsis [Performs equivalence checking.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Aig_Man_t * Cec_ManSatSweep( Aig_Man_t * pAig, Cec_ParCsw_t * pPars ) -{ -/* - Aig_Man_t * pAigNew, * pAigDfs; - Caig_Man_t * pCaig; - Cec_ManCsw_t * p; - pAigDfs = Cec_Duplicate( pAig ); - pCaig = Caig_ManClassesPrepare( pAigDfs, pPars->nWords, pPars->nRounds ); - p = Cec_ManCswCreate( pCaig, pPars ); - Cec_ManSatSweep( p, pPars ); - Cec_ManCswStop( p ); -// pAigNew = - Caig_ManDelete( pCaig ); - Aig_ManStop( pAigDfs ); - return pAigNew; -*/ - return NULL; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/aig/cec2/module.make b/src/aig/cec2/module.make deleted file mode 100644 index 537397e3..00000000 --- a/src/aig/cec2/module.make +++ /dev/null @@ -1,9 +0,0 @@ -SRC += src/aig/cec/cecAig.c \ - src/aig/cec/cecClass.c \ - src/aig/cec/cecCnf.c \ - src/aig/cec/cecCore.c \ - src/aig/cec/cecMan.c \ - src/aig/cec/cecSat.c \ - src/aig/cec/cecSim.c \ - src/aig/cec/cecStatus.c \ - src/aig/cec/cecSweep.c diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 91507947..c5d55565 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -80,6 +80,7 @@ struct Gia_Cex_t_ unsigned pData[0]; // the cex bit data (the number of bits: nRegs + (iFrame+1) * nPis) }; +// new AIG manager typedef struct Gia_Man_t_ Gia_Man_t; struct Gia_Man_t_ { @@ -109,6 +110,7 @@ struct Gia_Man_t_ int nFansAlloc; // the size of fanout representation int * pMapping; // mapping for each node Gia_Cex_t * pCexComb; // combinational counter-example + int * pCopies; // intermediate copies }; @@ -446,7 +448,7 @@ extern Gia_Man_t * Gia_ManDupCofactored( Gia_Man_t * p, int iVar, int nL extern Gia_Man_t * Gia_ManDupDfsCiMap( Gia_Man_t * p, int * pCi2Lit, Vec_Int_t * vLits ); extern Gia_Man_t * Gia_ManDupDfsClasses( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupTopAnd( Gia_Man_t * p, int fVerbose ); -extern Gia_Man_t * Gia_ManMiter( Gia_Man_t * pAig0, Gia_Man_t * pAig1, int fXorOuts, int fComb, int fVerbose ); +extern Gia_Man_t * Gia_ManMiter( Gia_Man_t * pAig0, Gia_Man_t * pAig1, int fDualOut, int fSeq, int fVerbose ); extern Gia_Man_t * Gia_ManTransformMiter( Gia_Man_t * p ); /*=== giaEnable.c ==========================================================*/ extern void Gia_ManDetectSeqSignals( Gia_Man_t * p, int fSetReset ); @@ -454,9 +456,11 @@ extern void Gia_ManDetectSeqSignals( Gia_Man_t * p, int fSetReset extern int * Gia_ManDeriveNexts( Gia_Man_t * p ); extern void Gia_ManEquivPrintOne( Gia_Man_t * p, int i, int Counter ); extern void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem ); +extern Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll ); extern Gia_Man_t * Gia_ManEquivReduceAndRemap( Gia_Man_t * p, int fSeq, int fMiterPairs ); extern int Gia_ManEquivSetColors( Gia_Man_t * p, int fVerbose ); -extern Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p ); +extern Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut ); +extern Gia_Man_t * Gia_ManSpecReduceInit( Gia_Man_t * p, Gia_Cex_t * pInit, int nFrames, int fDualOut ); extern void Gia_ManEquivTransform( Gia_Man_t * p, int fVerbose ); /*=== giaFanout.c =========================================================*/ extern void Gia_ObjAddFanout( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pFanout ); @@ -526,7 +530,10 @@ extern Vec_Int_t * Gia_ManCollectPoIds( Gia_Man_t * p ); extern int Gia_ObjIsMuxType( Gia_Obj_t * pNode ); extern int Gia_ObjRecognizeExor( Gia_Obj_t * pObj, Gia_Obj_t ** ppFan0, Gia_Obj_t ** ppFan1 ); extern Gia_Obj_t * Gia_ObjRecognizeMux( Gia_Obj_t * pNode, Gia_Obj_t ** ppNodeT, Gia_Obj_t ** ppNodeE ); -extern int Gia_ManVerifyCounterExample( Gia_Man_t * pAig, Gia_Cex_t * p, int fDoubleOuts ); +extern Gia_Cex_t * Gia_ManAllocCounterExample( int nRegs, int nRealPis, int nFrames ); +extern int Gia_ManVerifyCounterExample( Gia_Man_t * pAig, Gia_Cex_t * p, int fDualOut ); +extern void Gia_ManPrintCounterExample( Gia_Cex_t * p ); + #ifdef __cplusplus } diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index 4821dba9..1d940b78 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -756,25 +756,12 @@ int Gia_ManMiter_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj ) SeeAlso [] ***********************************************************************/ -Gia_Man_t * Gia_ManMiter( Gia_Man_t * p0, Gia_Man_t * p1, int fXorOuts, int fComb, int fVerbose ) +Gia_Man_t * Gia_ManMiter( Gia_Man_t * p0, Gia_Man_t * p1, int fDualOut, int fSeq, int fVerbose ) { Gia_Man_t * pNew, * pTemp; Gia_Obj_t * pObj; int i, iLit; - if ( fComb ) - { - if ( Gia_ManCiNum(p0) != Gia_ManCiNum(p1) ) - { - printf( "Gia_ManMiter(): Designs have different number of CIs.\n" ); - return NULL; - } - if ( Gia_ManCoNum(p0) != Gia_ManCoNum(p1) ) - { - printf( "Gia_ManMiter(): Designs have different number of COs.\n" ); - return NULL; - } - } - else + if ( fSeq ) { if ( Gia_ManPiNum(p0) != Gia_ManPiNum(p1) ) { @@ -792,6 +779,19 @@ Gia_Man_t * Gia_ManMiter( Gia_Man_t * p0, Gia_Man_t * p1, int fXorOuts, int fCom return NULL; } } + else + { + if ( Gia_ManCiNum(p0) != Gia_ManCiNum(p1) ) + { + printf( "Gia_ManMiter(): Designs have different number of CIs.\n" ); + return NULL; + } + if ( Gia_ManCoNum(p0) != Gia_ManCoNum(p1) ) + { + printf( "Gia_ManMiter(): Designs have different number of COs.\n" ); + return NULL; + } + } // start the manager pNew = Gia_ManStart( Gia_ManObjNum(p0) + Gia_ManObjNum(p1) ); pNew->pName = Aig_UtilStrsav( "miter" ); @@ -802,31 +802,7 @@ Gia_Man_t * Gia_ManMiter( Gia_Man_t * p0, Gia_Man_t * p1, int fXorOuts, int fCom Gia_ManConst0(p1)->Value = 0; // map internal nodes and outputs Gia_ManHashAlloc( pNew ); - if ( fComb ) - { - // create combinational inputs - Gia_ManForEachCi( p0, pObj, i ) - pObj->Value = Gia_ManAppendCi( pNew ); - Gia_ManForEachCi( p1, pObj, i ) - pObj->Value = Gia_ObjToLit( pNew, Gia_ManCi(pNew, i) ); - // create combinational outputs - Gia_ManForEachCo( p0, pObj, i ) - { - Gia_ManMiter_rec( pNew, p0, Gia_ObjFanin0(pObj) ); - Gia_ManMiter_rec( pNew, p1, Gia_ObjFanin0(Gia_ManCo(p1,i)) ); - if ( fXorOuts ) - { - iLit = Gia_ManHashXor( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin0Copy(Gia_ManCo(p1,i)) ); - Gia_ManAppendCo( pNew, iLit ); - } - else - { - Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); - Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(Gia_ManCo(p1,i)) ); - } - } - } - else + if ( fSeq ) { // create primary inputs Gia_ManForEachPi( p0, pObj, i ) @@ -843,15 +819,15 @@ Gia_Man_t * Gia_ManMiter( Gia_Man_t * p0, Gia_Man_t * p1, int fXorOuts, int fCom { Gia_ManMiter_rec( pNew, p0, Gia_ObjFanin0(pObj) ); Gia_ManMiter_rec( pNew, p1, Gia_ObjFanin0(Gia_ManPo(p1,i)) ); - if ( fXorOuts ) + if ( fDualOut ) { - iLit = Gia_ManHashXor( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin0Copy(Gia_ManPo(p1,i)) ); - Gia_ManAppendCo( pNew, iLit ); + Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(Gia_ManPo(p1,i)) ); } else { - Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); - Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(Gia_ManPo(p1,i)) ); + iLit = Gia_ManHashXor( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin0Copy(Gia_ManPo(p1,i)) ); + Gia_ManAppendCo( pNew, iLit ); } } // create register inputs @@ -867,6 +843,30 @@ Gia_Man_t * Gia_ManMiter( Gia_Man_t * p0, Gia_Man_t * p1, int fXorOuts, int fCom } Gia_ManSetRegNum( pNew, Gia_ManRegNum(p0) + Gia_ManRegNum(p1) ); } + else + { + // create combinational inputs + Gia_ManForEachCi( p0, pObj, i ) + pObj->Value = Gia_ManAppendCi( pNew ); + Gia_ManForEachCi( p1, pObj, i ) + pObj->Value = Gia_ObjToLit( pNew, Gia_ManCi(pNew, i) ); + // create combinational outputs + Gia_ManForEachCo( p0, pObj, i ) + { + Gia_ManMiter_rec( pNew, p0, Gia_ObjFanin0(pObj) ); + Gia_ManMiter_rec( pNew, p1, Gia_ObjFanin0(Gia_ManCo(p1,i)) ); + if ( fDualOut ) + { + Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(Gia_ManCo(p1,i)) ); + } + else + { + iLit = Gia_ManHashXor( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin0Copy(Gia_ManCo(p1,i)) ); + Gia_ManAppendCo( pNew, iLit ); + } + } + } Gia_ManHashStop( pNew ); pNew = Gia_ManCleanup( pTemp = pNew ); Gia_ManStop( pTemp ); diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c index 9e190da3..acdd3c13 100644 --- a/src/aig/gia/giaEquiv.c +++ b/src/aig/gia/giaEquiv.c @@ -156,13 +156,13 @@ int Gia_ManEquivCheckLits( Gia_Man_t * p, int nLits ) ***********************************************************************/ void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem ) { - int i, Counter = 0, Counter1 = 0, CounterX = 0, Proved = 0, nLits; + int i, Counter = 0, Counter0 = 0, CounterX = 0, Proved = 0, nLits; for ( i = 1; i < Gia_ManObjNum(p); i++ ) { if ( Gia_ObjIsHead(p, i) ) Counter++; else if ( Gia_ObjIsConst(p, i) ) - Counter1++; + Counter0++; else if ( Gia_ObjIsNone(p, i) ) CounterX++; if ( Gia_ObjProved(p, i) ) @@ -170,8 +170,8 @@ void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem ) } CounterX -= Gia_ManCoNum(p); nLits = Gia_ManCiNum(p) + Gia_ManAndNum(p) - Counter - CounterX; - printf( "cls =%7d cst =%8d lit =%8d unused =%8d proof =%6d mem =%5.2f Mb\n", - Counter, Counter1, nLits, CounterX, Proved, (Mem == 0.0) ? 8.0*Gia_ManObjNum(p)/(1<<20) : Mem ); + printf( "cst =%8d cls =%7d lit =%8d unused =%8d proof =%6d mem =%5.2f Mb\n", + Counter0, Counter, nLits, CounterX, Proved, (Mem == 0.0) ? 8.0*Gia_ManObjNum(p)/(1<<20) : Mem ); assert( Gia_ManEquivCheckLits( p, nLits ) ); if ( fVerbose ) { @@ -192,10 +192,18 @@ void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem ) SeeAlso [] ***********************************************************************/ -static inline Gia_Obj_t * Gia_ManEquivRepr( Gia_Man_t * p, Gia_Obj_t * pObj ) +static inline Gia_Obj_t * Gia_ManEquivRepr( Gia_Man_t * p, Gia_Obj_t * pObj, int fUseAll ) { - if ( !Gia_ObjProved(p, Gia_ObjId(p,pObj)) ) - return NULL; + if ( fUseAll ) + { + if ( Gia_ObjRepr(p, Gia_ObjId(p,pObj)) == GIA_VOID ) + return NULL; + } + else + { + if ( !Gia_ObjProved(p, Gia_ObjId(p,pObj)) ) + return NULL; + } return Gia_ManObj( p, Gia_ObjRepr(p, Gia_ObjId(p,pObj)) ); } @@ -210,20 +218,20 @@ static inline Gia_Obj_t * Gia_ManEquivRepr( Gia_Man_t * p, Gia_Obj_t * pObj ) SeeAlso [] ***********************************************************************/ -void Gia_ManEquivReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj ) +void Gia_ManEquivReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int fUseAll ) { Gia_Obj_t * pRepr; if ( ~pObj->Value ) return; assert( Gia_ObjIsAnd(pObj) ); - if ( (pRepr = Gia_ManEquivRepr(p, pObj)) ) + if ( (pRepr = Gia_ManEquivRepr(p, pObj, fUseAll)) ) { - Gia_ManEquivReduce_rec( pNew, p, pRepr ); + Gia_ManEquivReduce_rec( pNew, p, pRepr, fUseAll ); pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ); return; } - Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin0(pObj) ); - Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin1(pObj) ); + Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin0(pObj), fUseAll ); + Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin1(pObj), fUseAll ); pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); } @@ -238,7 +246,7 @@ void Gia_ManEquivReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj ) SeeAlso [] ***********************************************************************/ -Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p ) +Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll ) { Gia_Man_t * pNew; Gia_Obj_t * pObj, * pRepr; @@ -251,12 +259,12 @@ Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p ) Gia_ManForEachCi( p, pObj, i ) { pObj->Value = Gia_ManAppendCi(pNew); - if ( (pRepr = Gia_ManEquivRepr(p, pObj)) ) + if ( (pRepr = Gia_ManEquivRepr(p, pObj, fUseAll)) ) pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ); } Gia_ManHashAlloc( pNew ); Gia_ManForEachCo( p, pObj, i ) - Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin0(pObj) ); + Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin0(pObj), fUseAll ); Gia_ManForEachCo( p, pObj, i ) Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); Gia_ManHashStop( pNew ); @@ -390,7 +398,7 @@ void Gia_ManEquivDeriveReprs( Gia_Man_t * p, Gia_Man_t * pNew, Gia_Man_t * pFina Gia_Man_t * Gia_ManEquivReduceAndRemap( Gia_Man_t * p, int fSeq, int fMiterPairs ) { Gia_Man_t * pNew, * pFinal; - pNew = Gia_ManEquivReduce( p ); + pNew = Gia_ManEquivReduce( p, 0 ); if ( fMiterPairs ) Gia_ManEquivFixOutputPairs( pNew ); if ( fSeq ) @@ -474,27 +482,43 @@ int Gia_ManEquivSetColors( Gia_Man_t * p, int fVerbose ) SeeAlso [] ***********************************************************************/ -void Gia_ManSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits ) +static inline void Gia_ManSpecBuild( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits ) { Gia_Obj_t * pRepr; - int iLitNew; - if ( ~pObj->Value ) - return; - assert( Gia_ObjIsAnd(pObj) ); - Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits ); - Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj), vXorLits ); - pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + unsigned iLitNew; pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) ); if ( pRepr == NULL ) return; iLitNew = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ); - if ( pObj->Value != (unsigned)iLitNew && !Gia_ObjProved(p, Gia_ObjId(p,pObj)) ) + if ( pObj->Value != iLitNew && !Gia_ObjProved(p, Gia_ObjId(p,pObj)) ) Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, pObj->Value, iLitNew) ); pObj->Value = iLitNew; } /**Function************************************************************* + Synopsis [Duplicates the AIG in the DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits ) +{ + if ( ~pObj->Value ) + return; + assert( Gia_ObjIsAnd(pObj) ); + Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits ); + Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj), vXorLits ); + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Gia_ManSpecBuild( pNew, p, pObj, vXorLits ); +} + +/**Function************************************************************* + Synopsis [Reduces AIG using equivalence classes.] Description [] @@ -504,33 +528,28 @@ void Gia_ManSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, V SeeAlso [] ***********************************************************************/ -Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p ) +Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut ) { Gia_Man_t * pNew, * pTemp; - Gia_Obj_t * pObj, * pRepr; + Gia_Obj_t * pObj; Vec_Int_t * vXorLits; int i, iLitNew; if ( !p->pReprs ) + { + printf( "Gia_ManSpecReduce(): Equivalence classes are not available.\n" ); return NULL; + } vXorLits = Vec_IntAlloc( 1000 ); Gia_ManSetPhase( p ); + Gia_ManFillValue( p ); pNew = Gia_ManStart( Gia_ManObjNum(p) ); pNew->pName = Aig_UtilStrsav( p->pName ); - Gia_ManFillValue( p ); + Gia_ManHashAlloc( pNew ); Gia_ManConst0(p)->Value = 0; Gia_ManForEachCi( p, pObj, i ) pObj->Value = Gia_ManAppendCi(pNew); - Gia_ManHashAlloc( pNew ); - Gia_ManForEachCi( p, pObj, i ) - { - pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) ); - if ( pRepr == NULL ) - continue; - iLitNew = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ); - if ( pObj->Value != (unsigned)iLitNew && !Gia_ObjProved(p, Gia_ObjId(p,pObj)) ) - Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, pObj->Value, iLitNew) ); - pObj->Value = iLitNew; - } + Gia_ManForEachRo( p, pObj, i ) + Gia_ManSpecBuild( pNew, p, pObj, vXorLits ); Gia_ManForEachCo( p, pObj, i ) Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits ); Vec_IntForEachEntry( vXorLits, iLitNew, i ) @@ -542,14 +561,140 @@ Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p ) } Gia_ManForEachRi( p, pObj, i ) Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); - Vec_IntFree( vXorLits ); Gia_ManHashStop( pNew ); + Vec_IntFree( vXorLits ); Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); pNew = Gia_ManCleanup( pTemp = pNew ); Gia_ManStop( pTemp ); return pNew; } + +static inline int Gia_ObjSpec( Gia_Man_t * p, int f, Gia_Obj_t * pObj ) { return p->pCopies[Gia_ManObjNum(p) * f + Gia_ObjId(p,pObj)]; } +static inline void Gia_ObjSetSpec( Gia_Man_t * p, int f, Gia_Obj_t * pObj, int iLit ) { p->pCopies[Gia_ManObjNum(p) * f + Gia_ObjId(p,pObj)] = iLit; } + +static inline int Gia_ObjChild0Spec( Gia_Man_t * p, int f, Gia_Obj_t * pObj ) { return Gia_LitNotCond(Gia_ObjSpec(p, f, Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj)); } +static inline int Gia_ObjChild1Spec( Gia_Man_t * p, int f, Gia_Obj_t * pObj ) { return Gia_LitNotCond(Gia_ObjSpec(p, f, Gia_ObjFanin1(pObj)), Gia_ObjFaninC1(pObj)); } + +/**Function************************************************************* + + Synopsis [Duplicates the AIG in the DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManSpecBuildInit( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits, int f ) +{ + Gia_Obj_t * pRepr; + int iLitNew; + pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) ); + if ( pRepr == NULL ) + return; + iLitNew = Gia_LitNotCond( Gia_ObjSpec(p, f, pRepr), Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ); + if ( Gia_ObjSpec(p, f, pObj) != iLitNew && !Gia_ObjProved(p, Gia_ObjId(p,pObj)) ) + Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, Gia_ObjSpec(p, f, pObj), iLitNew) ); + Gia_ObjSetSpec( p, f, pObj, iLitNew ); +} + +/**Function************************************************************* + + Synopsis [Duplicates the AIG in the DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManSpecReduceInit_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits, int f ) +{ + if ( ~Gia_ObjSpec(p, f, pObj) ) + return; + assert( Gia_ObjIsAnd(pObj) ); + Gia_ManSpecReduceInit_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, f ); + Gia_ManSpecReduceInit_rec( pNew, p, Gia_ObjFanin1(pObj), vXorLits, f ); + Gia_ObjSetSpec( p, f, pObj, Gia_ManHashAnd(pNew, Gia_ObjChild0Spec(p, f, pObj), Gia_ObjChild1Spec(p, f, pObj)) ); + Gia_ManSpecBuildInit( pNew, p, pObj, vXorLits, f ); +} + +/**Function************************************************************* + + Synopsis [Creates initialized SRM with the given number of frames.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManSpecReduceInit( Gia_Man_t * p, Gia_Cex_t * pInit, int nFrames, int fDualOut ) +{ + Gia_Man_t * pNew, * pTemp; + Gia_Obj_t * pObj, * pObjRi, * pObjRo; + Vec_Int_t * vXorLits; + int f, i, iLitNew; + if ( !p->pReprs ) + { + printf( "Gia_ManSpecReduceInit(): Equivalence classes are not available.\n" ); + return NULL; + } + if ( Gia_ManRegNum(p) == 0 ) + { + printf( "Gia_ManSpecReduceInit(): Circuit is not sequential.\n" ); + return NULL; + } + if ( Gia_ManRegNum(p) != pInit->nRegs ) + { + printf( "Gia_ManSpecReduceInit(): Mismatch in the number of registers.\n" ); + return NULL; + } + assert( pInit->nRegs == Gia_ManRegNum(p) && pInit->nPis == 0 ); + p->pCopies = ABC_FALLOC( int, nFrames * Gia_ManObjNum(p) ); + vXorLits = Vec_IntAlloc( 1000 ); + Gia_ManSetPhase( p ); + pNew = Gia_ManStart( nFrames * Gia_ManObjNum(p) ); + pNew->pName = Aig_UtilStrsav( p->pName ); + Gia_ManHashAlloc( pNew ); + Gia_ManForEachRo( p, pObj, i ) + Gia_ObjSetSpec( p, 0, pObj, Aig_InfoHasBit(pInit->pData, i) ); + for ( f = 0; f < nFrames; f++ ) + { + Gia_ObjSetSpec( p, f, Gia_ManConst0(p), 0 ); + Gia_ManForEachPi( p, pObj, i ) + Gia_ObjSetSpec( p, f, pObj, Gia_ManAppendCi(pNew) ); + Gia_ManForEachRo( p, pObj, i ) + Gia_ManSpecBuildInit( pNew, p, pObj, vXorLits, f ); + Gia_ManForEachCo( p, pObj, i ) + { + Gia_ManSpecReduceInit_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, f ); + Gia_ObjSetSpec( p, f, pObj, Gia_ObjChild0Spec(p, f, pObj) ); + } + if ( f == nFrames - 1 ) + break; + Gia_ManForEachRiRo( p, pObjRi, pObjRo, i ) + Gia_ObjSetSpec( p, f+1, pObjRo, Gia_ObjSpec(p, f, pObjRi) ); + } + Vec_IntForEachEntry( vXorLits, iLitNew, i ) + Gia_ManAppendCo( pNew, iLitNew ); + if ( Vec_IntSize(vXorLits) == 0 ) + { + printf( "Speculatively reduced model has no primary outputs.\n" ); + Gia_ManAppendCo( pNew, 0 ); + } + ABC_FREE( p->pCopies ); + Vec_IntFree( vXorLits ); + Gia_ManHashStop( pNew ); + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + return pNew; +} + /**Function************************************************************* Synopsis [Transforms equiv classes by removing the AB nodes.] diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c index cc1a3861..822f1e64 100644 --- a/src/aig/gia/giaUtil.c +++ b/src/aig/gia/giaUtil.c @@ -580,6 +580,29 @@ Gia_Obj_t * Gia_ObjRecognizeMux( Gia_Obj_t * pNode, Gia_Obj_t ** ppNodeT, Gia_Ob /**Function************************************************************* + Synopsis [Allocates a counter-example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Cex_t * Gia_ManAllocCounterExample( int nRegs, int nRealPis, int nFrames ) +{ + Gia_Cex_t * pCex; + int nWords = Aig_BitWordNum( nRegs + nRealPis * nFrames ); + pCex = (Gia_Cex_t *)ABC_ALLOC( char, sizeof(Gia_Cex_t) + sizeof(unsigned) * nWords ); + memset( pCex, 0, sizeof(Gia_Cex_t) + sizeof(unsigned) * nWords ); + pCex->nRegs = nRegs; + pCex->nPis = nRealPis; + pCex->nBits = nRegs + nRealPis * nFrames; + return pCex; +} + +/**Function************************************************************* + Synopsis [Resimulates the counter-example.] Description [] @@ -589,7 +612,7 @@ Gia_Obj_t * Gia_ObjRecognizeMux( Gia_Obj_t * pNode, Gia_Obj_t ** ppNodeT, Gia_Ob SeeAlso [] ***********************************************************************/ -int Gia_ManVerifyCounterExample( Gia_Man_t * pAig, Gia_Cex_t * p, int fDoubleOuts ) +int Gia_ManVerifyCounterExample( Gia_Man_t * pAig, Gia_Cex_t * p, int fDualOut ) { Gia_Obj_t * pObj, * pObjRi, * pObjRo; int RetValue, i, k, iBit = 0; @@ -608,7 +631,7 @@ int Gia_ManVerifyCounterExample( Gia_Man_t * pAig, Gia_Cex_t * p, int fDoubleOut pObjRo->fMark0 = pObjRi->fMark0; } assert( iBit == p->nBits ); - if ( fDoubleOuts ) + if ( fDualOut ) RetValue = Gia_ManPo(pAig, 2*p->iPo)->fMark0 ^ Gia_ManPo(pAig, 2*p->iPo+1)->fMark0; else RetValue = Gia_ManPo(pAig, p->iPo)->fMark0; @@ -616,6 +639,36 @@ int Gia_ManVerifyCounterExample( Gia_Man_t * pAig, Gia_Cex_t * p, int fDoubleOut return RetValue; } +/**Function************************************************************* + + Synopsis [Prints out the counter-example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManPrintCounterExample( Gia_Cex_t * p ) +{ + int i, f, k; + printf( "Counter-example: iPo = %d iFrame = %d nRegs = %d nPis = %d nBits = %d\n", + p->iPo, p->iFrame, p->nRegs, p->nPis, p->nBits ); + printf( "State : " ); + for ( k = 0; k < p->nRegs; k++ ) + printf( "%d", Aig_InfoHasBit(p->pData, k) ); + printf( "\n" ); + for ( f = 0; f <= p->iFrame; f++ ) + { + printf( "Frame %2d : ", f ); + for ( i = 0; i < p->nPis; i++ ) + printf( "%d", Aig_InfoHasBit(p->pData, k++) ); + printf( "\n" ); + } + assert( k == p->nBits ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// |