diff options
-rw-r--r-- | abc.dsp | 4 | ||||
-rw-r--r-- | src/aig/aig/aig.h | 15 | ||||
-rw-r--r-- | src/aig/aig/aigMan.c | 5 | ||||
-rw-r--r-- | src/aig/aig/aigScl.c | 9 | ||||
-rw-r--r-- | src/aig/aig/aigTime.c | 299 | ||||
-rw-r--r-- | src/aig/fra/fra.h | 3 | ||||
-rw-r--r-- | src/aig/fra/fraBmc.c | 25 | ||||
-rw-r--r-- | src/aig/fra/fraImp.c | 33 | ||||
-rw-r--r-- | src/aig/fra/fraInd.c | 7 | ||||
-rw-r--r-- | src/aig/fra/fraLcr.c | 33 | ||||
-rw-r--r-- | src/aig/fra/fraSat.c | 9 | ||||
-rw-r--r-- | src/aig/fra/fraSec.c | 33 | ||||
-rw-r--r-- | src/aig/fra/fraSim.c | 50 | ||||
-rw-r--r-- | src/aig/ivy/ivyFraig.c | 6 | ||||
-rw-r--r-- | src/aig/kit/kitDsd.c | 2 | ||||
-rw-r--r-- | src/base/abci/abc.c | 2 | ||||
-rw-r--r-- | src/base/abci/abcDar.c | 23 | ||||
-rw-r--r-- | src/base/abci/abcStrash.c | 4 | ||||
-rw-r--r-- | src/base/seq/seqCreate.c | 2 | ||||
-rw-r--r-- | src/base/seq/seqRetCore.c | 2 |
20 files changed, 519 insertions, 47 deletions
@@ -2930,6 +2930,10 @@ SOURCE=.\src\aig\aig\aigTable.c # End Source File # Begin Source File +SOURCE=.\src\aig\aig\aigTime.c +# End Source File +# Begin Source File + SOURCE=.\src\aig\aig\aigTiming.c # End Source File # Begin Source File diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h index d5c2a4db..fe237142 100644 --- a/src/aig/aig/aig.h +++ b/src/aig/aig/aig.h @@ -50,6 +50,7 @@ typedef struct Aig_Obj_t_ Aig_Obj_t; typedef struct Aig_MmFixed_t_ Aig_MmFixed_t; typedef struct Aig_MmFlex_t_ Aig_MmFlex_t; typedef struct Aig_MmStep_t_ Aig_MmStep_t; +typedef struct Aig_TMan_t_ Aig_TMan_t; // object types typedef enum { @@ -131,6 +132,7 @@ struct Aig_Man_t_ Aig_Obj_t ** pObjCopies; // mapping of AIG nodes into FRAIG nodes void (*pImpFunc) (void*, void*); // implication checking precedure void * pImpData; // implication checking data + Aig_TMan_t * pManTime; // the timing manager // timing statistics int time1; int time2; @@ -520,6 +522,19 @@ extern char * Aig_MmStepEntryFetch( Aig_MmStep_t * p, int nBytes ); extern void Aig_MmStepEntryRecycle( Aig_MmStep_t * p, char * pEntry, int nBytes ); extern int Aig_MmStepReadMemUsage( Aig_MmStep_t * p ); +/*=== aigTime.c ===========================================================*/ +extern Aig_TMan_t * Aig_TManStart( int nPis, int nPos ); +extern void Aig_TManStop( Aig_TMan_t * p ); +extern void Aig_TManCreateBox( Aig_TMan_t * p, int * pPis, int nPis, int * pPos, int nPos, float * pPiTimes, float * pPoTimes ); +extern void Aig_TManSetPiDelay( Aig_TMan_t * p, int iPi, float Delay ); +extern void Aig_TManSetPoDelay( Aig_TMan_t * p, int iPo, float Delay ); +extern void Aig_TManSetPiArrival( Aig_TMan_t * p, int iPi, float Delay ); +extern void Aig_TManSetPoRequired( Aig_TMan_t * p, int iPo, float Delay ); +extern void Aig_TManIncrementTravId( Aig_TMan_t * p ); +extern float Aig_TManGetPiArrival( Aig_TMan_t * p, int iPi ); +extern float Aig_TManGetPoRequired( Aig_TMan_t * p, int iPo ); + + #ifdef __cplusplus } #endif diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c index 30a7991a..1e0ee278 100644 --- a/src/aig/aig/aigMan.c +++ b/src/aig/aig/aigMan.c @@ -229,6 +229,9 @@ void Aig_ManStop( Aig_Man_t * p ) // print time if ( p->time1 ) { PRT( "time1", p->time1 ); } if ( p->time2 ) { PRT( "time2", p->time2 ); } + // delete timing + if ( p->pManTime ) + Aig_TManStop( p->pManTime ); // delete fanout if ( p->pFanData ) Aig_ManFanoutStop( p ); @@ -304,6 +307,8 @@ void Aig_ManPrintStats( Aig_Man_t * p ) // printf( "Lev = %3d. ", Aig_ManCountLevels(p) ); printf( "Max = %7d. ", Aig_ManObjNumMax(p) ); printf( "Lev = %3d. ", Aig_ManLevels(p) ); + if ( Aig_ManRegNum(p) ) + printf( "Lat = %5d. ", Aig_ManRegNum(p) ); printf( "\n" ); } diff --git a/src/aig/aig/aigScl.c b/src/aig/aig/aigScl.c index 166377bf..2f00a7eb 100644 --- a/src/aig/aig/aigScl.c +++ b/src/aig/aig/aigScl.c @@ -157,12 +157,21 @@ int Aig_ManSeqCleanup( Aig_Man_t * p ) Aig_ManForEachPi( p, pObj, i ) if ( Aig_ObjIsTravIdCurrent(p, pObj) ) Vec_PtrPush( vCis, pObj ); + else + { + Vec_PtrWriteEntry( p->vObjs, pObj->Id, NULL ); +// Aig_ManRecycleMemory( p, pObj ); + } vCos = Vec_PtrAlloc( Aig_ManPoNum(p) ); Aig_ManForEachPo( p, pObj, i ) if ( Aig_ObjIsTravIdCurrent(p, pObj) ) Vec_PtrPush( vCos, pObj ); else + { Aig_ObjDisconnect( p, pObj ); + Vec_PtrWriteEntry( p->vObjs, pObj->Id, NULL ); +// Aig_ManRecycleMemory( p, pObj ); + } // remember the number of true PIs/POs nTruePis = Aig_ManPiNum(p) - Aig_ManRegNum(p); nTruePos = Aig_ManPoNum(p) - Aig_ManRegNum(p); diff --git a/src/aig/aig/aigTime.c b/src/aig/aig/aigTime.c new file mode 100644 index 00000000..42f5f575 --- /dev/null +++ b/src/aig/aig/aigTime.c @@ -0,0 +1,299 @@ +/**CFile**************************************************************** + + FileName [aigTime.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [AIG package.] + + Synopsis [Representation of timing information.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - April 28, 2007.] + + Revision [$Id: aigTime.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "aig.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Aig_TBox_t_ Aig_TBox_t; +typedef struct Aig_TObj_t_ Aig_TObj_t; + +// timing manager +struct Aig_TMan_t_ +{ + Vec_Ptr_t * vBoxes; // the timing boxes + Aig_MmFlex_t * pMemObj; // memory manager for boxes + int nTravIds; // traversal ID of the manager + int nPis; // the number of PIs + int nPos; // the number of POs + Aig_TObj_t * pPis; // timing info for the PIs + Aig_TObj_t * pPos; // timing info for the POs +}; + +// timing box +struct Aig_TBox_t_ +{ + int iBox; // the unique ID of this box + int TravId; // traversal ID of this box + int nInputs; // the number of box inputs + int nOutputs; // the number of box outputs + int Inouts[0]; // the int numbers of PIs and POs +}; + +// timing object +struct Aig_TObj_t_ +{ + int iObj2Box; // mapping of the object into its box + float timeOffset; // the static timing of the node + float timeActual; // the actual timing of the node +}; + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Starts the network manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_TMan_t * Aig_TManStart( int nPis, int nPos ) +{ + Aig_TMan_t * p; + int i; + p = ALLOC( Aig_TMan_t, 1 ); + memset( p, 0, sizeof(Aig_TMan_t) ); + p->pMemObj = Aig_MmFlexStart(); + p->vBoxes = Vec_PtrAlloc( 100 ); + Vec_PtrPush( p->vBoxes, NULL ); + p->nPis = nPis; + p->nPos = nPos; + p->pPis = ALLOC( Aig_TObj_t, nPis ); + memset( p->pPis, 0, sizeof(Aig_TObj_t) * nPis ); + p->pPos = ALLOC( Aig_TObj_t, nPos ); + memset( p->pPos, 0, sizeof(Aig_TObj_t) * nPos ); + for ( i = 0; i < nPis; i++ ) + p->pPis[i].iObj2Box = -1; + for ( i = 0; i < nPos; i++ ) + p->pPos[i].iObj2Box = -1; + return p; +} + +/**Function************************************************************* + + Synopsis [Stops the network manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_TManStop( Aig_TMan_t * p ) +{ + Vec_PtrFree( p->vBoxes ); + Aig_MmFlexStop( p->pMemObj, 0 ); + free( p->pPis ); + free( p->pPos ); + free( p ); +} + +/**Function************************************************************* + + Synopsis [Creates the new timing box.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_TManCreateBox( Aig_TMan_t * p, int * pPis, int nPis, int * pPos, int nPos, float * pPiTimes, float * pPoTimes ) +{ + Aig_TBox_t * pBox; + int i; + pBox = (Aig_TBox_t *)Aig_MmFlexEntryFetch( p->pMemObj, sizeof(Aig_TBox_t) + sizeof(int) * (nPis+nPos) ); + memset( pBox, 0, sizeof(Aig_TBox_t) ); + pBox->iBox = Vec_PtrSize( p->vBoxes ); + Vec_PtrPush( p->vBoxes, pBox ); + pBox->nInputs = nPis; + pBox->nOutputs = nPos; + for ( i = 0; i < nPis; i++ ) + { + assert( pPis[i] < p->nPis ); + pBox->Inouts[i] = pPis[i]; + Aig_TManSetPiArrival( p, pPis[i], pPiTimes[i] ); + p->pPis[pPis[i]].iObj2Box = pBox->iBox; + } + for ( i = 0; i < nPos; i++ ) + { + assert( pPos[i] < p->nPos ); + pBox->Inouts[nPis+i] = pPos[i]; + Aig_TManSetPoRequired( p, pPos[i], pPoTimes[i] ); + p->pPos[pPos[i]].iObj2Box = pBox->iBox; + } +} + +/**Function************************************************************* + + Synopsis [Creates the new timing box.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_TManSetPiDelay( Aig_TMan_t * p, int iPi, float Delay ) +{ + assert( iPi < p->nPis ); + p->pPis[iPi].timeActual = Delay; +} + +/**Function************************************************************* + + Synopsis [Creates the new timing box.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_TManSetPoDelay( Aig_TMan_t * p, int iPo, float Delay ) +{ + assert( iPo < p->nPos ); + p->pPos[iPo].timeActual = Delay; +} + +/**Function************************************************************* + + Synopsis [Creates the new timing box.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_TManSetPiArrival( Aig_TMan_t * p, int iPi, float Delay ) +{ + assert( iPi < p->nPis ); + p->pPis[iPi].timeOffset = Delay; +} + +/**Function************************************************************* + + Synopsis [Creates the new timing box.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_TManSetPoRequired( Aig_TMan_t * p, int iPo, float Delay ) +{ + assert( iPo < p->nPos ); + p->pPos[iPo].timeOffset = Delay; +} + +/**Function************************************************************* + + Synopsis [Increments the trav ID of the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_TManIncrementTravId( Aig_TMan_t * p ) +{ + p->nTravIds++; +} + +/**Function************************************************************* + + Synopsis [Returns PI arrival time.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +float Aig_TManGetPiArrival( Aig_TMan_t * p, int iPi ) +{ + Aig_TBox_t * pBox; + Aig_TObj_t * pObj; + float DelayMax; + int i; + assert( iPi < p->nPis ); + if ( p->pPis[iPi].iObj2Box < 0 ) + return p->pPis[iPi].timeOffset; + pBox = Vec_PtrEntry( p->vBoxes, p->pPis[iPi].iObj2Box ); + // check if box timing is updated + if ( pBox->TravId == p->nTravIds ) + return p->pPis[iPi].timeOffset; + pBox->TravId = p->nTravIds; + // update box timing + DelayMax = -1.0e+20F; + for ( i = 0; i < pBox->nOutputs; i++ ) + { + pObj = p->pPos + pBox->Inouts[pBox->nInputs+i]; + DelayMax = AIG_MAX( DelayMax, pObj->timeActual + pObj->timeOffset ); + } + for ( i = 0; i < pBox->nInputs; i++ ) + { + pObj = p->pPis + pBox->Inouts[i]; + pObj->timeActual = DelayMax + pObj->timeOffset; + } + return p->pPis[iPi].timeActual; +} + +/**Function************************************************************* + + Synopsis [Returns PO required time.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +float Aig_TManGetPoRequired( Aig_TMan_t * p, int iPo ) +{ + return 0.0; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h index cd6bdfd4..210af244 100644 --- a/src/aig/fra/fra.h +++ b/src/aig/fra/fra.h @@ -111,6 +111,7 @@ struct Fra_Sml_t_ int nWordsFrame; // the number of words in each time frame int nWordsTotal; // the total number of words at a node int nWordsPref; // the number of word in the prefix + int fNonConstOut; // have seen a non-const-0 output during simulation int nSimRounds; // statistics int timeSim; // statistics unsigned pData[0]; // simulation data for the nodes @@ -256,7 +257,7 @@ extern void Fra_ImpRecordInManager( Fra_Man_t * p, Aig_Man_t * pN /*=== fraInd.c ========================================================*/ extern Aig_Man_t * Fra_FraigInduction( Aig_Man_t * p, int nFramesP, int nFramesK, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fVerbose, int * pnIter ); /*=== fraLcr.c ========================================================*/ -extern Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nConfMax, int fVerbose, int * pnIter ); +extern Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nConfMax, int fProve, int fVerbose, int * pnIter ); /*=== fraMan.c ========================================================*/ extern void Fra_ParamsDefault( Fra_Par_t * pParams ); extern void Fra_ParamsDefaultSeq( Fra_Par_t * pParams ); diff --git a/src/aig/fra/fraBmc.c b/src/aig/fra/fraBmc.c index 1df25c0a..1140f3a4 100644 --- a/src/aig/fra/fraBmc.c +++ b/src/aig/fra/fraBmc.c @@ -128,7 +128,7 @@ void Fra_BmcFilterImplications( Fra_Man_t * p, Fra_Bmc_t * pBmc ) { if ( Imp == 0 ) continue; - Left = Fra_ImpLeft(Imp); + Left = Fra_ImpLeft(Imp); Right = Fra_ImpRight(Imp); // get the corresponding nodes pLeft = Aig_ManObj( pBmc->pAig, Left ); @@ -136,7 +136,7 @@ void Fra_BmcFilterImplications( Fra_Man_t * p, Fra_Bmc_t * pBmc ) // iterate through the timeframes for ( f = pBmc->nPref; f < pBmc->nFramesAll; f++ ) { - // get timeframes nodes + // get timeframe nodes pLeftT = Bmc_ObjFrames( pLeft, f ); pRightT = Bmc_ObjFrames( pRight, f ); // get the corresponding FRAIG nodes @@ -148,14 +148,21 @@ void Fra_BmcFilterImplications( Fra_Man_t * p, Fra_Bmc_t * pBmc ) // check equality if ( Aig_Regular(pLeftF) == Aig_Regular(pRightF) ) { - if ( fComplL != fComplR ) - Vec_IntWriteEntry( pBmc->vImps, i, 0 ); + if ( fComplL == fComplR ) // x => x - always true + continue; + assert( fComplL != fComplR ); + // consider 4 possibilities: + // NOT(1) => 1 or 0 => 1 - always true + // 1 => NOT(1) or 1 => 0 - never true + // NOT(x) => x or x - not always true + // x => NOT(x) or NOT(x) - not always true + if ( Aig_ObjIsConst1(Aig_Regular(pLeftF)) && fComplL ) // proved implication + continue; + // disproved implication + Vec_IntWriteEntry( pBmc->vImps, i, 0 ); break; } // check the implication - // - if true, a clause is added - // - if false, a cex is simulated - // make sure the implication is refined if ( Fra_NodesAreImp( p, Aig_Regular(pLeftF), Aig_Regular(pRightF), fComplL, fComplR ) != 1 ) { Vec_IntWriteEntry( pBmc->vImps, i, 0 ); @@ -320,7 +327,7 @@ void Fra_BmcPerform( Fra_Man_t * p, int nPref, int nDepth ) // Fra_ClassesPrint( p->pCla, 0 ); printf( "Const = %5d. Class = %5d. Lit = %5d. ", Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), Fra_ClassesCountLits(p->pCla) ); - if ( p->pCla->vImps && Vec_IntSize(p->pCla->vImps) > 0 ) + if ( p->pCla->vImps ) printf( "Imp = %5d. ", nImpsOld ); printf( "\n" ); } @@ -338,7 +345,7 @@ void Fra_BmcPerform( Fra_Man_t * p, int nPref, int nDepth ) // Fra_ClassesPrint( p->pCla, 0 ); printf( "Const = %5d. Class = %5d. Lit = %5d. ", Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), Fra_ClassesCountLits(p->pCla) ); - if ( p->pCla->vImps && Vec_IntSize(p->pCla->vImps) > 0 ) + if ( p->pCla->vImps ) printf( "Imp = %5d. ", Vec_IntSize(p->pCla->vImps) ); printf( "\n" ); } diff --git a/src/aig/fra/fraImp.c b/src/aig/fra/fraImp.c index d8bf4e48..a5fc7d58 100644 --- a/src/aig/fra/fraImp.c +++ b/src/aig/fra/fraImp.c @@ -96,7 +96,7 @@ static inline int Sml_NodeCheckImp( Fra_Sml_t * p, int Left, int Right ) /**Function************************************************************* - Synopsis [Counts the number of 1s in the reverse implication.] + Synopsis [Counts the number of 1s in the complement of the implication.] Description [] @@ -118,7 +118,7 @@ static inline int Sml_NodeNotImpWeight( Fra_Sml_t * p, int Left, int Right ) /**Function************************************************************* - Synopsis [Counts the number of 1s in the reverse implication.] + Synopsis [Computes the complement of the implication.] Description [] @@ -495,7 +495,7 @@ int Fra_ImpCheckForNode( Fra_Man_t * p, Vec_Int_t * vImps, Aig_Obj_t * pNode, in { Aig_Obj_t * pLeft, * pRight; Aig_Obj_t * pLeftF, * pRightF; - int i, Imp, Left, Right, Max; + int i, Imp, Left, Right, Max, RetValue; int fComplL, fComplR; Vec_IntForEachEntryStart( vImps, Imp, i, Pos ) { @@ -519,18 +519,31 @@ int Fra_ImpCheckForNode( Fra_Man_t * p, Vec_Int_t * vImps, Aig_Obj_t * pNode, in // check equality if ( Aig_Regular(pLeftF) == Aig_Regular(pRightF) ) { - if ( fComplL != fComplR ) - Vec_IntWriteEntry( vImps, i, 0 ); + if ( fComplL == fComplR ) // x => x - always true + continue; + assert( fComplL != fComplR ); + // consider 4 possibilities: + // NOT(1) => 1 or 0 => 1 - always true + // 1 => NOT(1) or 1 => 0 - never true + // NOT(x) => x or x - not always true + // x => NOT(x) or NOT(x) - not always true + if ( Aig_ObjIsConst1(Aig_Regular(pLeftF)) && fComplL ) // proved implication + continue; + // disproved implication + p->pCla->fRefinement = 1; + Vec_IntWriteEntry( vImps, i, 0 ); continue; } // check the implication // - if true, a clause is added // - if false, a cex is simulated // make sure the implication is refined - if ( Fra_NodesAreImp( p, Aig_Regular(pLeftF), Aig_Regular(pRightF), fComplL, fComplR ) == 0 ) + RetValue = Fra_NodesAreImp( p, Aig_Regular(pLeftF), Aig_Regular(pRightF), fComplL, fComplR ); + if ( RetValue != 1 ) { p->pCla->fRefinement = 1; - Fra_SmlResimulate( p ); + if ( RetValue == 0 ) + Fra_SmlResimulate( p ); if ( Vec_IntEntry(vImps, i) != 0 ) printf( "Fra_ImpCheckForNode(): Implication is not refined!\n" ); assert( Vec_IntEntry(vImps, i) == 0 ); @@ -642,14 +655,15 @@ double Fra_ImpComputeStateSpaceRatio( Fra_Man_t * p ) ***********************************************************************/ int Fra_ImpVerifyUsingSimulation( Fra_Man_t * p ) { - int nSimWords = 2000; + int nFrames = 2000; + int nSimWords = 8; Fra_Sml_t * pSeq; char * pfFails; int Left, Right, Imp, i, Counter; if ( p->pCla->vImps == NULL || Vec_IntSize(p->pCla->vImps) == 0 ) return 0; // simulate the AIG manager with combinational patterns - pSeq = Fra_SmlSimulateSeq( p->pManAig, p->pPars->nFramesP, nSimWords, 4 ); + pSeq = Fra_SmlSimulateSeq( p->pManAig, p->pPars->nFramesP, nFrames, nSimWords ); // go through the implications and check how many of them do not hold pfFails = ALLOC( char, Vec_IntSize(p->pCla->vImps) ); memset( pfFails, 0, sizeof(char) * Vec_IntSize(p->pCla->vImps) ); @@ -664,6 +678,7 @@ int Fra_ImpVerifyUsingSimulation( Fra_Man_t * p ) for ( i = 0; i < Vec_IntSize(p->pCla->vImps); i++ ) Counter += pfFails[i]; free( pfFails ); + Fra_SmlStop( pSeq ); return Counter; } diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c index 14fba9ba..98025280 100644 --- a/src/aig/fra/fraInd.c +++ b/src/aig/fra/fraInd.c @@ -257,7 +257,7 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK, Aig_Obj_t * pObj; Cnf_Dat_t * pCnf; Aig_Man_t * pManAigNew; - int nNodesBeg, nRegsBeg, Temp; + int nNodesBeg, nRegsBeg; int nIter, i, clk = clock(), clk2; if ( Aig_ManNodeNum(pManAig) == 0 ) @@ -424,17 +424,18 @@ PRT( "Time", clock() - clk ); break; } } +/* // check implications using simulation if ( p->pCla->vImps && Vec_IntSize(p->pCla->vImps) ) { - int clk = clock(); + int Temp, clk = clock(); if ( Temp = Fra_ImpVerifyUsingSimulation( p ) ) printf( "Implications failing the simulation test = %d (out of %d). ", Temp, Vec_IntSize(p->pCla->vImps) ); else printf( "All %d implications have passed the simulation test. ", Vec_IntSize(p->pCla->vImps) ); PRT( "Time", clock() - clk ); } - +*/ // move the classes into representatives and reduce AIG clk2 = clock(); diff --git a/src/aig/fra/fraLcr.c b/src/aig/fra/fraLcr.c index e73d610f..50fd6687 100644 --- a/src/aig/fra/fraLcr.c +++ b/src/aig/fra/fraLcr.c @@ -500,17 +500,18 @@ void Fra_ClassNodesUnmark( Fra_Lcr_t * p ) SeeAlso [] ***********************************************************************/ -Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nConfMax, int fVerbose, int * pnIter ) +Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nConfMax, int fProve, int fVerbose, int * pnIter ) { int nPartSize = 200; int fReprSelect = 0; Fra_Lcr_t * p; + Fra_Sml_t * pSml; Fra_Man_t * pTemp; Aig_Man_t * pAigPart, * pAigNew = NULL; Vec_Int_t * vPart; // Aig_Obj_t * pObj = Aig_ManObj(pAig, 2078); - int i, nIter, clk = clock(), clk2, clk3; + int i, nIter, timeSim, clk = clock(), clk2, clk3; if ( Aig_ManNodeNum(pAig) == 0 ) { if ( pnIter ) *pnIter = 0; @@ -519,23 +520,33 @@ Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nC assert( Aig_ManLatchNum(pAig) == 0 ); assert( Aig_ManRegNum(pAig) > 0 ); - // start the manager - p = Lcr_ManAlloc( pAig ); - p->nFramesP = nFramesP; - p->fVerbose = fVerbose; - // simulate the AIG clk2 = clock(); if ( fVerbose ) printf( "Simulating AIG with %d nodes for %d cycles ... ", Aig_ManNodeNum(pAig), nFramesP + 32 ); - pTemp = Fra_LcrAigPrepare( p->pAig ); - pTemp->pBmc = (Fra_Bmc_t *)p; - pTemp->pSml = Fra_SmlSimulateSeq( p->pAig, p->nFramesP, 32, 1 ); + pSml = Fra_SmlSimulateSeq( pAig, nFramesP, 32, 1 ); if ( fVerbose ) { PRT( "Time", clock() - clk2 ); -p->timeSim += clock() - clk2; +timeSim = clock() - clk2; } + // check if simulation discovered non-constant-0 POs + if ( fProve && pSml->fNonConstOut ) + { + Fra_SmlStop( pSml ); + return NULL; + } + + // start the manager + p = Lcr_ManAlloc( pAig ); + p->nFramesP = nFramesP; + p->fVerbose = fVerbose; + p->timeSim += timeSim; + + pTemp = Fra_LcrAigPrepare( pAig ); + pTemp->pBmc = (Fra_Bmc_t *)p; + pTemp->pSml = pSml; + // get preliminary info about equivalence classes pTemp->pCla = p->pCla = Fra_ClassesStart( p->pAig ); Fra_ClassesPrepare( p->pCla, 1 ); diff --git a/src/aig/fra/fraSat.c b/src/aig/fra/fraSat.c index e1cc4c32..11029b69 100644 --- a/src/aig/fra/fraSat.c +++ b/src/aig/fra/fraSat.c @@ -75,6 +75,9 @@ int Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) p->pSat = sat_solver_new(); p->nSatVars = 1; sat_solver_setnvars( p->pSat, 1000 ); + // var 0 is reserved for const1 node - add the clause + pLits[0] = toLit( 0 ); + sat_solver_addclause( p->pSat, pLits, pLits + 1 ); } // if the nodes do not have SAT variables, allocate them @@ -232,6 +235,9 @@ int Fra_NodesAreImp( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew, int fCom p->pSat = sat_solver_new(); p->nSatVars = 1; sat_solver_setnvars( p->pSat, 1000 ); + // var 0 is reserved for const1 node - add the clause + pLits[0] = toLit( 0 ); + sat_solver_addclause( p->pSat, pLits, pLits + 1 ); } // if the nodes do not have SAT variables, allocate them @@ -318,6 +324,9 @@ int Fra_NodeIsConst( Fra_Man_t * p, Aig_Obj_t * pNew ) p->pSat = sat_solver_new(); p->nSatVars = 1; sat_solver_setnvars( p->pSat, 1000 ); + // var 0 is reserved for const1 node - add the clause + pLits[0] = toLit( 0 ); + sat_solver_addclause( p->pSat, pLits, pLits + 1 ); } // if the nodes do not have SAT variables, allocate them diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c index 0146ac5a..0919e035 100644 --- a/src/aig/fra/fraSec.c +++ b/src/aig/fra/fraSec.c @@ -103,6 +103,7 @@ PRT( "Time", clock() - clkTotal ); ***********************************************************************/ int Fra_FraigSec( Aig_Man_t * p, int nFramesMax, int fRetimeFirst, int fVerbose, int fVeryVerbose ) { + Fra_Sml_t * pSml; Aig_Man_t * pNew, * pTemp; int nFrames, RetValue, nIter, clk, clkTotal = clock(); int fLatchCorr = 0; @@ -148,8 +149,16 @@ clk = clock(); { pNew = Aig_ManDup( pTemp = pNew, 1 ); Aig_ManStop( pTemp ); - pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 100000, fVeryVerbose, &nIter ); + pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 100000, 1, fVeryVerbose, &nIter ); Aig_ManStop( pTemp ); + if ( pNew == NULL ) + { + RetValue = 0; + printf( "Networks are NOT EQUIVALENT after simulation. " ); +PRT( "Time", clock() - clkTotal ); + return RetValue; + } + if ( fVerbose ) { printf( "Latch-corr (I=%3d): Latches = %5d. Nodes = %6d. ", @@ -196,7 +205,7 @@ clk = clock(); printf( "Rewriting: Latches = %5d. Nodes = %6d. ", Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) ); PRT( "Time", clock() - clk ); - } + } // perform retiming clk = clock(); pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 ); @@ -211,6 +220,26 @@ PRT( "Time", clock() - clk ); } if ( pNew->nRegs ) pNew = Aig_ManConstReduce( pNew, 0 ); + + // perform sequential simulation +clk = clock(); + pSml = Fra_SmlSimulateSeq( pNew, 0, 128 * nFrames, 1 + 16/(1+Aig_ManNodeNum(pNew)/1000) ); + if ( fVerbose ) + { + printf( "Seq simulation : Latches = %5d. Nodes = %6d. ", + Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) ); +PRT( "Time", clock() - clk ); + } + if ( pSml->fNonConstOut ) + { + Fra_SmlStop( pSml ); + Aig_ManStop( pNew ); + RetValue = 0; + printf( "Networks are NOT EQUIVALENT after simulation. " ); +PRT( "Time", clock() - clkTotal ); + return RetValue; + } + Fra_SmlStop( pSml ); } // get the miter status diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c index d6f6d74a..d379cf53 100644 --- a/src/aig/fra/fraSim.c +++ b/src/aig/fra/fraSim.c @@ -137,6 +137,28 @@ int Fra_SmlNodeNotEquWeight( Fra_Sml_t * p, int Left, int Right ) return Counter; } +/**Function************************************************************* + + Synopsis [Returns 1 if simulation info is composed of all zeros.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fra_SmlNodeIsZero( Fra_Sml_t * p, Aig_Obj_t * pObj ) +{ + unsigned * pSims; + int i; + pSims = Fra_ObjSim(p, pObj->Id); + for ( i = p->nWordsPref; i < p->nWordsTotal; i++ ) + if ( pSims[i] ) + return 0; + return 1; +} + /**Function************************************************************* @@ -550,6 +572,27 @@ void Fra_SmlNodeTransferNext( Fra_Sml_t * p, Aig_Obj_t * pOut, Aig_Obj_t * pIn, /**Function************************************************************* + Synopsis [Check if any of the POs becomes non-constant.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fra_SmlCheckNonConstOutputs( Fra_Sml_t * p ) +{ + Aig_Obj_t * pObj; + int i; + Aig_ManForEachPoSeq( p->pAig, pObj, i ) + if ( !Fra_SmlNodeIsZero(p, pObj) ) + return 1; + return 0; +} + +/**Function************************************************************* + Synopsis [Simulates AIG manager.] Description [Assumes that the PI simulation info is attached.] @@ -569,14 +612,16 @@ clk = clock(); // simulate the nodes Aig_ManForEachNode( p->pAig, pObj, i ) Fra_SmlNodeSimulate( p, pObj, f ); + // copy simulation info into outputs + Aig_ManForEachPoSeq( p->pAig, pObj, i ) + Fra_SmlNodeCopyFanin( p, pObj, f ); + // quit if this is the last timeframe if ( f == p->nFrames - 1 ) break; // copy simulation info into outputs Aig_ManForEachLiSeq( p->pAig, pObj, i ) Fra_SmlNodeCopyFanin( p, pObj, f ); // copy simulation info into the inputs -// for ( i = 0; i < Aig_ManRegNum(p->pAig); i++ ) -// Fra_SmlNodeTransferNext( p, Aig_ManLi(p->pAig, i), Aig_ManLo(p->pAig, i), f ); Aig_ManForEachLiLoSeq( p->pAig, pObjLi, pObjLo, i ) Fra_SmlNodeTransferNext( p, pObjLi, pObjLo, f ); } @@ -768,6 +813,7 @@ Fra_Sml_t * Fra_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nW p = Fra_SmlStart( pAig, nPref, nFrames, nWords ); Fra_SmlInitialize( p, 1 ); Fra_SmlSimulateOne( p ); + p->fNonConstOut = Fra_SmlCheckNonConstOutputs( p ); return p; } diff --git a/src/aig/ivy/ivyFraig.c b/src/aig/ivy/ivyFraig.c index a922674d..81ed895e 100644 --- a/src/aig/ivy/ivyFraig.c +++ b/src/aig/ivy/ivyFraig.c @@ -2100,6 +2100,9 @@ int Ivy_FraigNodesAreEquiv( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pN p->pSat = sat_solver_new(); p->nSatVars = 1; sat_solver_setnvars( p->pSat, 1000 ); + // var 0 is reserved for const1 node - add the clause + pLits[0] = toLit( 0 ); + sat_solver_addclause( p->pSat, pLits, pLits + 1 ); } // if the nodes do not have SAT variables, allocate them @@ -2231,6 +2234,9 @@ int Ivy_FraigNodeIsConst( Ivy_FraigMan_t * p, Ivy_Obj_t * pNew ) p->pSat = sat_solver_new(); p->nSatVars = 1; sat_solver_setnvars( p->pSat, 1000 ); + // var 0 is reserved for const1 node - add the clause + pLits[0] = toLit( 0 ); + sat_solver_addclause( p->pSat, pLits, pLits + 1 ); } // if the nodes do not have SAT variables, allocate them diff --git a/src/aig/kit/kitDsd.c b/src/aig/kit/kitDsd.c index ada4ef09..abd07e68 100644 --- a/src/aig/kit/kitDsd.c +++ b/src/aig/kit/kitDsd.c @@ -48,7 +48,7 @@ Kit_DsdMan_t * Kit_DsdManAlloc( int nVars, int nNodes ) p->nWords = Kit_TruthWordNum( p->nVars ); p->vTtElems = Vec_PtrAllocTruthTables( p->nVars ); p->vTtNodes = Vec_PtrAllocSimInfo( nNodes, p->nWords ); - p->dd = Cloud_Init( 16, 13 ); + p->dd = Cloud_Init( 16, 14 ); p->vTtBdds = Vec_PtrAllocSimInfo( (1<<12), p->nWords ); p->vNodes = Vec_IntAlloc( 512 ); return p; diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index a8888d81..bbaa80a4 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -3095,7 +3095,7 @@ usage: fprintf( pErr, "\t-N <num> : the max number of LUTs in the structure (2 <= num) [default = %d]\n", pPars->nLutsMax ); fprintf( pErr, "\t-Q <num> : the max number of LUTs not in MFFC (0 <= num) [default = %d]\n", pPars->nLutsOver ); fprintf( pErr, "\t-S <num> : the max number of LUT inputs shared (0 <= num <= 3) [default = %d]\n", pPars->nVarsShared ); - fprintf( pErr, "\t-L <num> : the largest increase in node level after resynthesis (0 <= num) [default = %d]\n", pPars->nGrowthLevel ); + fprintf( pErr, "\t-L <num> : max level increase after resynthesis (0 <= num) [default = %d]\n", pPars->nGrowthLevel ); fprintf( pErr, "\t-s : toggle iteration till saturation [default = %s]\n", pPars->fSatur? "yes": "no" ); fprintf( pErr, "\t-z : toggle zero-cost replacements [default = %s]\n", pPars->fZeroCost? "yes": "no" ); fprintf( pErr, "\t-f : toggle using only first node and first cut [default = %s]\n", pPars->fFirst? "yes": "no" ); diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 356a5565..06e425d5 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -49,10 +49,10 @@ Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fRegisters ) Aig_Man_t * pMan; Aig_Obj_t * pObjNew; Abc_Obj_t * pObj; - int i, nNodes; + int i, nNodes, nDontCares; // make sure the latches follow PIs/POs - if ( fRegisters ) - { + if ( fRegisters ) + { assert( Abc_NtkBoxNum(pNtk) == Abc_NtkLatchNum(pNtk) ); Abc_NtkForEachCi( pNtk, pObj, i ) if ( i < Abc_NtkPiNum(pNtk) ) @@ -64,6 +64,21 @@ Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fRegisters ) assert( Abc_ObjIsPo(pObj) ); else assert( Abc_ObjIsBi(pObj) ); + // print warning about initial values + nDontCares = 0; + Abc_NtkForEachLatch( pNtk, pObj, i ) + if ( Abc_LatchIsInitDc(pObj) ) + { + Abc_LatchSetInit0(pObj); + nDontCares++; + } + if ( nDontCares ) + { + printf( "Warning: %d registers in this network have don't-care init values.\n", nDontCares ); + printf( "The don't-care are assumed to be 0. The result may not verify.\n" ); + printf( "Use command \"print_latch\" to see the init values of registers.\n" ); + printf( "Use command \"init\" to change the values.\n" ); + } } // create the manager pMan = Aig_ManStart( Abc_NtkNodeNum(pNtk) + 100 ); @@ -985,7 +1000,7 @@ Abc_Ntk_t * Abc_NtkDarLcorr( Abc_Ntk_t * pNtk, int nFramesP, int nConfMax, int f pMan = Abc_NtkToDar( pNtk, 1 ); if ( pMan == NULL ) return NULL; - pMan = Fra_FraigLatchCorrespondence( pTemp = pMan, nFramesP, nConfMax, fVerbose, NULL ); + pMan = Fra_FraigLatchCorrespondence( pTemp = pMan, nFramesP, nConfMax, 0, fVerbose, NULL ); Aig_ManStop( pTemp ); if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) ) pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan ); diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c index 69373597..c77f8dea 100644 --- a/src/base/abci/abcStrash.c +++ b/src/base/abci/abcStrash.c @@ -80,7 +80,7 @@ Abc_Ntk_t * Abc_NtkRestrash( Abc_Ntk_t * pNtk, bool fCleanup ) } //timeRetime = clock() - timeRetime; // if ( RetValue = Abc_NtkRemoveSelfFeedLatches(pNtkAig) ) -// printf( "Modified %d self-feeding latches. The result will not verify.\n", RetValue ); +// printf( "Modified %d self-feeding latches. The result may not verify.\n", RetValue ); return pNtkAig; } @@ -145,7 +145,7 @@ Abc_Ntk_t * Abc_NtkRestrashZero( Abc_Ntk_t * pNtk, bool fCleanup ) } //timeRetime = clock() - timeRetime; // if ( RetValue = Abc_NtkRemoveSelfFeedLatches(pNtkAig) ) -// printf( "Modified %d self-feeding latches. The result will not verify.\n", RetValue ); +// printf( "Modified %d self-feeding latches. The result may not verify.\n", RetValue ); return pNtkAig; } diff --git a/src/base/seq/seqCreate.c b/src/base/seq/seqCreate.c index a4bcaefc..16c7cc92 100644 --- a/src/base/seq/seqCreate.c +++ b/src/base/seq/seqCreate.c @@ -82,7 +82,7 @@ Abc_Ntk_t * Abc_NtkAigToSeq( Abc_Ntk_t * pNtk ) assert( Abc_NtkIsDfsOrdered(pNtk) ); if ( RetValue = Abc_NtkRemoveSelfFeedLatches(pNtk) ) - printf( "Modified %d self-feeding latches. The result will not verify.\n", RetValue ); + printf( "Modified %d self-feeding latches. The result may not verify.\n", RetValue ); assert( Abc_NtkCountSelfFeedLatches(pNtk) == 0 ); // start the network diff --git a/src/base/seq/seqRetCore.c b/src/base/seq/seqRetCore.c index ba2c154c..27638644 100644 --- a/src/base/seq/seqRetCore.c +++ b/src/base/seq/seqRetCore.c @@ -99,7 +99,7 @@ Abc_Ntk_t * Seq_NtkRetimeDerive( Abc_Ntk_t * pNtk, int fVerbose ) // make sure it is an AIG without self-feeding latches assert( !Abc_NtkHasAig(pNtk) ); if ( RetValue = Abc_NtkRemoveSelfFeedLatches(pNtk) ) - printf( "Modified %d self-feeding latches. The result will not verify.\n", RetValue ); + printf( "Modified %d self-feeding latches. The result may not verify.\n", RetValue ); assert( Abc_NtkCountSelfFeedLatches(pNtk) == 0 ); // remove the dangling nodes |