From f65983c2c0810cfb933f696952325a81d2378987 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 28 Feb 2008 08:01:00 -0800 Subject: Version abc80228 --- abc.dsp | 4 + src/aig/aig/aig.h | 6 + src/aig/aig/aigPart.c | 140 ++++++++- src/aig/aig/aigPartReg.c | 182 ++++++++--- src/aig/aig/aigRepr.c | 35 +++ src/aig/aig/aigScl.c | 4 + src/aig/aig/aigTsim.c | 78 ++++- src/aig/fra/fra.h | 22 +- src/aig/fra/fraInd.c | 117 +++++-- src/aig/fra/fraSec.c | 71 +---- src/base/abc/abc.h | 4 +- src/base/abci/abc.c | 247 +++++++++------ src/base/abci/abcDar.c | 75 ++--- src/base/abci/abcDelay.c | 73 ++++- src/base/abci/abcIf.c | 2 + src/base/abci/abcPrint.c | 13 +- src/map/if/if.h | 4 +- src/map/if/ifTime.c | 24 ++ src/map/if/ifTruth.c | 36 +++ src/opt/fret/fretFlow.c | 1 + src/opt/fret/fretInit.c | 793 ++++++++++++++++++++++++++++++++++++++++------- src/opt/fret/fretMain.c | 431 ++++++++++++++++++++++---- src/opt/fret/fretime.h | 82 +++-- 23 files changed, 1962 insertions(+), 482 deletions(-) diff --git a/abc.dsp b/abc.dsp index 32cfed71..a8d6a3c6 100644 --- a/abc.dsp +++ b/abc.dsp @@ -2378,6 +2378,10 @@ SOURCE=.\src\misc\espresso\verify.c # PROP Default_Filter "" # Begin Source File +SOURCE=.\src\misc\util\port_type.h +# End Source File +# Begin Source File + SOURCE=.\src\misc\util\util_hack.h # End Source File # End Group diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h index ccc34caf..744a044e 100644 --- a/src/aig/aig/aig.h +++ b/src/aig/aig/aig.h @@ -521,9 +521,14 @@ extern Vec_Ptr_t * Aig_ManSupports( Aig_Man_t * p ); extern Vec_Ptr_t * Aig_ManSupportsInverse( Aig_Man_t * p ); extern Vec_Ptr_t * Aig_ManSupportsRegisters( Aig_Man_t * p ); extern Vec_Ptr_t * Aig_ManPartitionSmart( Aig_Man_t * p, int nPartSizeLimit, int fVerbose, Vec_Ptr_t ** pvPartSupps ); +extern Vec_Ptr_t * Aig_ManPartitionSmartRegisters( Aig_Man_t * pAig, int nSuppSizeLimit, int fVerbose ); extern Vec_Ptr_t * Aig_ManPartitionNaive( Aig_Man_t * p, int nPartSize ); extern Vec_Ptr_t * Aig_ManMiterPartitioned( Aig_Man_t * p1, Aig_Man_t * p2, int nPartSize ); extern Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize, int nConfMax, int nLevelMax, int fVerbose ); +/*=== aigPartReg.c =========================================================*/ +extern Vec_Ptr_t * Aig_ManRegPartitionSimple( Aig_Man_t * pAig, int nPartSize, int nOverSize ); +extern Vec_Ptr_t * Aig_ManRegPartitionSmart( Aig_Man_t * pAig, int nPartSize ); +extern Aig_Man_t * Aig_ManRegCreatePart( Aig_Man_t * pAig, Vec_Int_t * vPart, int * pnCountPis, int * pnCountRegs, int ** ppMapBack ); /*=== aigRepr.c =========================================================*/ extern void Aig_ManReprStart( Aig_Man_t * p, int nIdMax ); extern void Aig_ManReprStop( Aig_Man_t * p ); @@ -532,6 +537,7 @@ extern void Aig_ManTransferRepr( Aig_Man_t * pNew, Aig_Man_t * p ); extern Aig_Man_t * Aig_ManDupRepr( Aig_Man_t * p, int fOrdered ); extern Aig_Man_t * Aig_ManRehash( Aig_Man_t * p ); extern void Aig_ManMarkValidChoices( Aig_Man_t * p ); +extern int Aig_TransferMappedClasses( Aig_Man_t * pAig, Aig_Man_t * pPart, int * pMapBack ); /*=== aigRet.c ========================================================*/ extern Aig_Man_t * Rtm_ManRetime( Aig_Man_t * p, int fForward, int nStepsMax, int fVerbose ); /*=== aigRetF.c ========================================================*/ diff --git a/src/aig/aig/aigPart.c b/src/aig/aig/aigPart.c index 7e765f60..df5792b2 100644 --- a/src/aig/aig/aigPart.c +++ b/src/aig/aig/aigPart.c @@ -770,6 +770,135 @@ if ( fVerbose ) return vPartsAll; } +/**Function************************************************************* + + Synopsis [Perform the smart partitioning.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Aig_ManPartitionSmartRegisters( Aig_Man_t * pAig, int nSuppSizeLimit, int fVerbose ) +{ + Vec_Ptr_t * vPartSuppsBit; + Vec_Ptr_t * vSupports, * vPartsAll, * vPartsAll2, * vPartSuppsAll; + Vec_Int_t * vOne, * vPart, * vPartSupp, * vTemp; + int i, iPart, iOut, clk; + + // add output number to each +clk = clock(); + vSupports = Aig_ManSupportsRegisters( pAig ); + assert( Vec_PtrSize(vSupports) == Aig_ManRegNum(pAig) ); + Vec_PtrForEachEntry( vSupports, vOne, i ) + Vec_IntPush( vOne, i ); +if ( fVerbose ) +{ +PRT( "Supps", clock() - clk ); +} + + // start char-based support representation + vPartSuppsBit = Vec_PtrAlloc( 1000 ); + + // create partitions +clk = clock(); + vPartsAll = Vec_PtrAlloc( 256 ); + vPartSuppsAll = Vec_PtrAlloc( 256 ); + Vec_PtrForEachEntry( vSupports, vOne, i ) + { + // get the output number + iOut = Vec_IntPop(vOne); + // find closely matching part + iPart = Aig_ManPartitionSmartFindPart( vPartSuppsAll, vPartsAll, vPartSuppsBit, nSuppSizeLimit, vOne ); + if ( iPart == -1 ) + { + // create new partition + vPart = Vec_IntAlloc( 32 ); + Vec_IntPush( vPart, iOut ); + // create new partition support + vPartSupp = Vec_IntDup( vOne ); + // add this partition and its support + Vec_PtrPush( vPartsAll, vPart ); + Vec_PtrPush( vPartSuppsAll, vPartSupp ); + + Vec_PtrPush( vPartSuppsBit, Aig_ManSuppCharStart(vOne, Vec_PtrSize(vSupports)) ); + } + else + { + // add output to this partition + vPart = Vec_PtrEntry( vPartsAll, iPart ); + Vec_IntPush( vPart, iOut ); + // merge supports + vPartSupp = Vec_PtrEntry( vPartSuppsAll, iPart ); + vPartSupp = Vec_IntTwoMerge( vTemp = vPartSupp, vOne ); + Vec_IntFree( vTemp ); + // reinsert new support + Vec_PtrWriteEntry( vPartSuppsAll, iPart, vPartSupp ); + + Aig_ManSuppCharAdd( Vec_PtrEntry(vPartSuppsBit, iPart), vOne, Vec_PtrSize(vSupports) ); + } + } + + // stop char-based support representation + Vec_PtrForEachEntry( vPartSuppsBit, vTemp, i ) + free( vTemp ); + Vec_PtrFree( vPartSuppsBit ); + +//printf( "\n" ); +if ( fVerbose ) +{ +PRT( "Parts", clock() - clk ); +} + +clk = clock(); + // reorder partitions in the decreasing order of support sizes + // remember partition number in each partition support + Vec_PtrForEachEntry( vPartSuppsAll, vOne, i ) + Vec_IntPush( vOne, i ); + // sort the supports in the decreasing order + Vec_VecSort( (Vec_Vec_t *)vPartSuppsAll, 1 ); + // reproduce partitions + vPartsAll2 = Vec_PtrAlloc( 256 ); + Vec_PtrForEachEntry( vPartSuppsAll, vOne, i ) + Vec_PtrPush( vPartsAll2, Vec_PtrEntry(vPartsAll, Vec_IntPop(vOne)) ); + Vec_PtrFree( vPartsAll ); + vPartsAll = vPartsAll2; + + // compact small partitions +// Aig_ManPartitionPrint( p, vPartsAll, vPartSuppsAll ); + Aig_ManPartitionCompact( vPartsAll, vPartSuppsAll, nSuppSizeLimit ); + if ( fVerbose ) +// Aig_ManPartitionPrint( p, vPartsAll, vPartSuppsAll ); + printf( "Created %d partitions.\n", Vec_PtrSize(vPartsAll) ); + +if ( fVerbose ) +{ +//PRT( "Comps", clock() - clk ); +} + + // cleanup + Vec_VecFree( (Vec_Vec_t *)vSupports ); +// if ( pvPartSupps == NULL ) + Vec_VecFree( (Vec_Vec_t *)vPartSuppsAll ); +// else +// *pvPartSupps = vPartSuppsAll; + +/* + // converts from intergers to nodes + Vec_PtrForEachEntry( vPartsAll, vPart, iPart ) + { + vPartPtr = Vec_PtrAlloc( Vec_IntSize(vPart) ); + Vec_IntForEachEntry( vPart, iOut, i ) + Vec_PtrPush( vPartPtr, Aig_ManPo(p, iOut) ); + Vec_IntFree( vPart ); + Vec_PtrWriteEntry( vPartsAll, iPart, vPartPtr ); + } +*/ + return vPartsAll; +} + /**Function************************************************************* Synopsis [Perform the naive partitioning.] @@ -968,16 +1097,21 @@ Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize, int nCon Vec_Ptr_t * vParts; Aig_Obj_t * pObj; void ** ppData; - int i, k, m; + int i, k, m, nIdMax; + assert( Vec_PtrSize(vAigs) > 1 ); + + // compute the total number of IDs + nIdMax = 0; + Vec_PtrForEachEntry( vAigs, pAig, i ) + nIdMax += Aig_ManObjNumMax(pAig); // partition the first AIG in the array - assert( Vec_PtrSize(vAigs) > 1 ); pAig = Vec_PtrEntry( vAigs, 0 ); vParts = Aig_ManPartitionSmart( pAig, nPartSize, 0, NULL ); // start the total fraiged AIG pAigTotal = Aig_ManStartFrom( pAig ); - Aig_ManReprStart( pAigTotal, Vec_PtrSize(vAigs) * Aig_ManObjNumMax(pAig) + 10000 ); + Aig_ManReprStart( pAigTotal, nIdMax ); vOutsTotal = Vec_PtrStart( Aig_ManPoNum(pAig) ); // set the PI numbers diff --git a/src/aig/aig/aigPartReg.c b/src/aig/aig/aigPartReg.c index 1f218bd8..88ae66ee 100644 --- a/src/aig/aig/aigPartReg.c +++ b/src/aig/aig/aigPartReg.c @@ -19,6 +19,7 @@ ***********************************************************************/ #include "aig.h" +#include "fra.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -59,14 +60,14 @@ struct Aig_ManPre_t_ SeeAlso [] ***********************************************************************/ -Aig_ManPre_t * Aig_ManRegManStart( Aig_Man_t * pAig ) +Aig_ManPre_t * Aig_ManRegManStart( Aig_Man_t * pAig, int nPartSize ) { Aig_ManPre_t * p; p = ALLOC( Aig_ManPre_t, 1 ); memset( p, 0, sizeof(Aig_ManPre_t) ); p->pAig = pAig; p->vMatrix = Aig_ManSupportsRegisters( pAig ); - p->nRegsMax = 500; + p->nRegsMax = nPartSize; p->vParts = Vec_PtrAlloc(256); p->vRegs = Vec_IntAlloc(256); p->vUniques = Vec_IntAlloc(256); @@ -105,9 +106,10 @@ void Aig_ManRegManStop( Aig_ManPre_t * p ) /**Function************************************************************* - Synopsis [Computes the max-support register that is not taken yet.] + Synopsis [Determines what register to use as the seed.] - Description [] + Description [The register is selected as the one having the largest + number of non-taken registers in its support.] SideEffects [] @@ -116,12 +118,16 @@ void Aig_ManRegManStop( Aig_ManPre_t * p ) ***********************************************************************/ int Aig_ManRegFindSeed( Aig_ManPre_t * p ) { - int i, iMax, nRegsCur, nRegsMax = -1; + Vec_Int_t * vRegs; + int i, k, iReg, iMax, nRegsCur, nRegsMax = -1; for ( i = 0; i < Aig_ManRegNum(p->pAig); i++ ) { if ( p->pfUsedRegs[i] ) continue; - nRegsCur = Vec_IntSize( Vec_PtrEntry(p->vMatrix,i) ); + nRegsCur = 0; + vRegs = Vec_PtrEntry( p->vMatrix, i ); + Vec_IntForEachEntry( vRegs, iReg, k ) + nRegsCur += !p->pfUsedRegs[iReg]; if ( nRegsMax < nRegsCur ) { nRegsMax = nRegsCur; @@ -157,7 +163,11 @@ int Aig_ManRegFindBestVar( Aig_ManPre_t * p ) // count the number of new vars nNewVars = 0; Vec_IntForEachEntry( vSupp, iVarSupp, k ) - nNewVars += !p->pfPartVars[iVarSupp]; + { + if ( p->pfPartVars[iVarSupp] ) + continue; + nNewVars += 1 + 3 * p->pfUsedRegs[iVarSupp]; + } // quit if there is no new variables if ( nNewVars == 0 ) return iVarFree; @@ -229,14 +239,15 @@ void Aig_ManRegPartitionAdd( Aig_ManPre_t * p, int iReg ) SeeAlso [] ***********************************************************************/ -Aig_Man_t * Aig_ManRegCreatePart( Aig_Man_t * pAig, Vec_Int_t * vPart, int * pnCountPis, int * pnCountRegs ) +Aig_Man_t * Aig_ManRegCreatePart( Aig_Man_t * pAig, Vec_Int_t * vPart, int * pnCountPis, int * pnCountRegs, int ** ppMapBack ) { Aig_Man_t * pNew; - Aig_Obj_t * pObj; + Aig_Obj_t * pObj, * pObjNew; Vec_Ptr_t * vNodes; Vec_Ptr_t * vRoots; int nOffset, iOut, i; int nCountPis, nCountRegs; + int * pMapBack; // collect roots vRoots = Vec_PtrAlloc( Vec_IntSize(vPart) ); nOffset = Aig_ManPoNum(pAig)-Aig_ManRegNum(pAig); @@ -275,6 +286,7 @@ Aig_Man_t * Aig_ManRegCreatePart( Aig_Man_t * pAig, Vec_Int_t * vPart, int * pnC pObj->pData = Aig_ObjCreatePi(pNew); // add variables for the register outputs // create fake POs to hold the register outputs + nOffset = Aig_ManPiNum(pAig)-Aig_ManRegNum(pAig); Vec_IntForEachEntry( vPart, iOut, i ) { pObj = Aig_ManPi(pAig, nOffset+iOut); @@ -285,7 +297,6 @@ Aig_Man_t * Aig_ManRegCreatePart( Aig_Man_t * pAig, Vec_Int_t * vPart, int * pnC Vec_PtrForEachEntry( vNodes, pObj, i ) if ( Aig_ObjIsNode(pObj) ) pObj->pData = Aig_And(pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); - Vec_PtrFree( vNodes ); // add real POs for the registers nOffset = Aig_ManPoNum(pAig)-Aig_ManRegNum(pAig); Vec_IntForEachEntry( vPart, iOut, i ) @@ -294,6 +305,30 @@ Aig_Man_t * Aig_ManRegCreatePart( Aig_Man_t * pAig, Vec_Int_t * vPart, int * pnC Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); } pNew->nRegs = Vec_IntSize(vPart); + // create map + if ( ppMapBack ) + { + pMapBack = ALLOC( int, Aig_ManObjNumMax(pNew) ); + memset( pMapBack, 0xff, sizeof(int) * Aig_ManObjNumMax(pNew) ); + // map constant nodes + pMapBack[0] = 0; + // logic cones of register outputs + Vec_PtrForEachEntry( vNodes, pObj, i ) + { + pObjNew = Aig_Regular(pObj->pData); + pMapBack[pObjNew->Id] = pObj->Id; + } + // map register outputs + nOffset = Aig_ManPiNum(pAig)-Aig_ManRegNum(pAig); + Vec_IntForEachEntry( vPart, iOut, i ) + { + pObj = Aig_ManPi(pAig, nOffset+iOut); + pObjNew = pObj->pData; + pMapBack[pObjNew->Id] = pObj->Id; + } + *ppMapBack = pMapBack; + } + Vec_PtrFree( vNodes ); return pNew; } @@ -308,7 +343,7 @@ Aig_Man_t * Aig_ManRegCreatePart( Aig_Man_t * pAig, Vec_Int_t * vPart, int * pnC SeeAlso [] ***********************************************************************/ -Vec_Ptr_t * Aig_ManRegPartitionSmart( Aig_Man_t * pAig ) +Vec_Ptr_t * Aig_ManRegPartitionSmart( Aig_Man_t * pAig, int nPartSize ) { extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact ); @@ -316,11 +351,11 @@ Vec_Ptr_t * Aig_ManRegPartitionSmart( Aig_Man_t * pAig ) Vec_Ptr_t * vResult; int iSeed, iNext, i, k; // create the manager - p = Aig_ManRegManStart( pAig ); + p = Aig_ManRegManStart( pAig, nPartSize ); // add partitions as long as registers remain for ( i = 0; (iSeed = Aig_ManRegFindSeed(p)) >= 0; i++ ) { -printf( "Seed variable = %d.\n", iSeed ); +//printf( "Seed variable = %d.\n", iSeed ); // clean the current partition information Vec_IntClear( p->vRegs ); Vec_IntClear( p->vUniques ); @@ -339,9 +374,9 @@ printf( "Seed variable = %d.\n", iSeed ); // add the register to the support of the partition Aig_ManRegPartitionAdd( p, iNext ); // report the result -printf( "Part %3d Reg %3d : Free = %4d. Total = %4d. Ratio = %6.2f. Unique = %4d.\n", i, k, - Vec_IntSize(p->vFreeVars), Vec_IntSize(p->vRegs), - 1.0*Vec_IntSize(p->vFreeVars)/Vec_IntSize(p->vRegs), Vec_IntSize(p->vUniques) ); +//printf( "Part %3d Reg %3d : Free = %4d. Total = %4d. Ratio = %6.2f. Unique = %4d.\n", i, k, +// Vec_IntSize(p->vFreeVars), Vec_IntSize(p->vRegs), +// 1.0*Vec_IntSize(p->vFreeVars)/Vec_IntSize(p->vRegs), Vec_IntSize(p->vUniques) ); // quit if there are not free variables if ( Vec_IntSize(p->vFreeVars) == 0 ) break; @@ -351,7 +386,7 @@ printf( "Part %3d Reg %3d : Free = %4d. Total = %4d. Ratio = %6.2f. Unique = %4 printf( "Part %3d SUMMARY: Free = %4d. Total = %4d. Ratio = %6.2f. Unique = %4d.\n", i, Vec_IntSize(p->vFreeVars), Vec_IntSize(p->vRegs), 1.0*Vec_IntSize(p->vFreeVars)/Vec_IntSize(p->vRegs), Vec_IntSize(p->vUniques) ); -printf( "\n" ); +//printf( "\n" ); } vResult = p->vParts; p->vParts = NULL; Aig_ManRegManStop( p ); @@ -369,24 +404,34 @@ printf( "\n" ); SeeAlso [] ***********************************************************************/ -Vec_Ptr_t * Aig_ManRegPartitionSimple( Aig_Man_t * pAig, int nPartSize ) +Vec_Ptr_t * Aig_ManRegPartitionSimple( Aig_Man_t * pAig, int nPartSize, int nOverSize ) { Vec_Ptr_t * vResult; Vec_Int_t * vPart; - int i, k, nParts; - nParts = (Aig_ManRegNum(pAig) / nPartSize) + (int)(Aig_ManRegNum(pAig) % nPartSize > 0); - vResult = Vec_PtrAlloc( nParts ); - for ( i = 0; i < nParts; i++ ) + int i, Counter; + if ( nOverSize >= nPartSize ) + { + printf( "Overlap size (%d) if more or equal to the partition size (%d).\n", nOverSize, nPartSize ); + printf( "Adjusting it to be equal to half of the partition size.\n" ); + nOverSize = nPartSize/2; + } + assert( nOverSize < nPartSize ); + vResult = Vec_PtrAlloc( 100 ); + for ( Counter = 0; Counter < Aig_ManRegNum(pAig); Counter -= nOverSize ) { vPart = Vec_IntAlloc( nPartSize ); - for ( k = 0; k < nPartSize; k++ ) - if ( i * nPartSize + k < Aig_ManRegNum(pAig) ) - Vec_IntPush( vPart, i * nPartSize + k ); - Vec_PtrPush( vResult, vPart ); + for ( i = 0; i < nPartSize; i++ ) + if ( ++Counter < Aig_ManRegNum(pAig) ) + Vec_IntPush( vPart, Counter ); + if ( Vec_IntSize(vPart) <= nOverSize ) + Vec_IntFree(vPart); + else + Vec_PtrPush( vResult, vPart ); } return vResult; } + /**Function************************************************************* Synopsis [Computes partitioning of registers.] @@ -398,26 +443,77 @@ Vec_Ptr_t * Aig_ManRegPartitionSimple( Aig_Man_t * pAig, int nPartSize ) SeeAlso [] ***********************************************************************/ -void Aig_ManRegPartitionRun( Aig_Man_t * pAig ) +void Aig_ManRegPartitionTraverse_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vLos ) { - int nPartSize = 1000; - char Buffer[100]; - Aig_Man_t * pTemp; - Vec_Ptr_t * vResult; - Vec_Int_t * vPart; - int i, nCountPis, nCountRegs; - vResult = Aig_ManRegPartitionSimple( pAig, nPartSize ); - printf( "Simple partitioning: %d partitions are saved:\n", Vec_PtrSize(vResult) ); - Vec_PtrForEachEntry( vResult, vPart, i ) + if ( Aig_ObjIsTravIdCurrent(p, pObj) ) + return; + Aig_ObjSetTravIdCurrent( p, pObj ); + if ( Aig_ObjIsPi(pObj) ) { - sprintf( Buffer, "part%03d.aig", i ); - pTemp = Aig_ManRegCreatePart( pAig, vPart, &nCountPis, &nCountRegs ); - Ioa_WriteAiger( pTemp, Buffer, 0, 0 ); - printf( "part%03d.aig : Regs = %4d. PIs = %4d. (True PIs = %4d. Other regs = %4d.)\n", - i, Vec_IntSize(vPart), Aig_ManPiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs ); - Aig_ManStop( pTemp ); + if ( pObj->iData >= Aig_ManPiNum(p) - Aig_ManRegNum(p) ) + { + Vec_PtrPush( vLos, pObj ); + printf( "%d ", pObj->iData - (Aig_ManPiNum(p) - Aig_ManRegNum(p)) ); + } + return; } - Vec_VecFree( (Vec_Vec_t *)vResult ); + Aig_ManRegPartitionTraverse_rec( p, Aig_ObjFanin0(pObj), vLos ); + Aig_ManRegPartitionTraverse_rec( p, Aig_ObjFanin1(pObj), vLos ); +} + +/**Function************************************************************* + + Synopsis [Computes partitioning of registers.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Aig_ManRegPartitionTraverse( Aig_Man_t * p ) +{ + Vec_Ptr_t * vLos; + Aig_Obj_t * pObj; + int i, nPrev, Counter; + // mark the registers + Aig_ManForEachPi( p, pObj, i ) + pObj->iData = i; + // collect registers + vLos = Vec_PtrAlloc( Aig_ManRegNum(p) ); + nPrev = 0; + Counter = 0; + Aig_ManIncrementTravId( p ); + Aig_ManForEachLiSeq( p, pObj, i ) + { + ++Counter; + printf( "Latch %d: ", Counter ); + Aig_ManRegPartitionTraverse_rec( p, Aig_ObjFanin0(pObj), vLos ); +printf( "%d=%d \n", Counter, Vec_PtrSize(vLos)-nPrev ); + nPrev = Vec_PtrSize(vLos); + } + printf( "Total collected = %d. Total regs = %d.\n", Vec_PtrSize(vLos), Aig_ManRegNum(p) ); + return vLos; +} + +/**Function************************************************************* + + Synopsis [Computes partitioning of registers.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Aig_ManRegPartitionLinear( Aig_Man_t * pAig, int nPartSize ) +{ + Vec_Ptr_t * vLos; + vLos = Aig_ManRegPartitionTraverse( pAig ); + Vec_PtrFree( vLos ); + return NULL; } diff --git a/src/aig/aig/aigRepr.c b/src/aig/aig/aigRepr.c index 3a7e382c..eb4325f4 100644 --- a/src/aig/aig/aigRepr.c +++ b/src/aig/aig/aigRepr.c @@ -443,6 +443,11 @@ void Aig_ManMarkValidChoices( Aig_Man_t * p ) } //printf( "Node %d is represented by node %d.\n", pObj->Id, pRepr->Id ); // add choice to the choice node + if ( pObj->nRefs > 0 ) + { + Aig_ObjClearRepr( p, pObj ); + continue; + } assert( pObj->nRefs == 0 ); p->pEquivs[pObj->Id] = p->pEquivs[pRepr->Id]; p->pEquivs[pRepr->Id] = pObj; @@ -450,6 +455,36 @@ void Aig_ManMarkValidChoices( Aig_Man_t * p ) } +/**Function************************************************************* + + Synopsis [Transfers the classes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_TransferMappedClasses( Aig_Man_t * pAig, Aig_Man_t * pPart, int * pMapBack ) +{ + Aig_Obj_t * pObj; + int nClasses, k; + nClasses = 0; + if ( pPart->pReprs ) + Aig_ManForEachObj( pPart, pObj, k ) + { + if ( pPart->pReprs[pObj->Id] == NULL ) + continue; + nClasses++; + Aig_ObjSetRepr( pAig, + Aig_ManObj(pAig, pMapBack[pObj->Id]), + Aig_ManObj(pAig, pMapBack[pPart->pReprs[pObj->Id]->Id]) ); + } + return nClasses; +} + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/aig/aigScl.c b/src/aig/aig/aigScl.c index 70586c68..d8ffda9a 100644 --- a/src/aig/aig/aigScl.c +++ b/src/aig/aig/aigScl.c @@ -376,10 +376,14 @@ Aig_Man_t * Aig_ManReduceLaches( Aig_Man_t * p, int fVerbose ) printf( "RBeg = %5d. NBeg = %6d. ", Aig_ManRegNum(p), Aig_ManNodeNum(p) ); } vMap = Aig_ManReduceLachesOnce( p ); +//Aig_ManPrintStats( p ); p = Aig_ManRemap( pTemp = p, vMap ); +//Aig_ManPrintStats( p ); Aig_ManStop( pTemp ); Vec_PtrFree( vMap ); Aig_ManSeqCleanup( p ); +//Aig_ManPrintStats( p ); +//printf( "\n" ); if ( fVerbose ) { printf( "REnd = %5d. NEnd = %6d. ", Aig_ManRegNum(p), Aig_ManNodeNum(p) ); diff --git a/src/aig/aig/aigTsim.c b/src/aig/aig/aigTsim.c index a8a3dda8..1d974778 100644 --- a/src/aig/aig/aigTsim.c +++ b/src/aig/aig/aigTsim.c @@ -25,6 +25,7 @@ //////////////////////////////////////////////////////////////////////// #define TSI_MAX_ROUNDS 1000 +#define TSI_ONE_SERIES 300 #define AIG_XVS0 1 #define AIG_XVS1 2 @@ -282,6 +283,51 @@ void Aig_TsiStatePrint( Aig_Tsi_t * p, unsigned * pState ) printf( " (0=%5d, 1=%5d, x=%5d)\n", nZeros, nOnes, nDcs ); } +/**Function************************************************************* + + Synopsis [Count constant values in the state.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_TsiStateCount( Aig_Tsi_t * p, unsigned * pState ) +{ + Aig_Obj_t * pObjLi, * pObjLo; + int i, Value, nCounter = 0; + Aig_ManForEachLiLoSeq( p->pAig, pObjLi, pObjLo, i ) + { + Value = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i ); + nCounter += (Value == 1 || Value == 2); + } + return nCounter; +} + +/**Function************************************************************* + + Synopsis [Count constant values in the state.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_TsiStateOrAll( Aig_Tsi_t * pTsi, unsigned * pState ) +{ + unsigned * pPrev; + int i, k; + Vec_PtrForEachEntry( pTsi->vStates, pPrev, i ) + { + for ( k = 0; k < pTsi->nWords; k++ ) + pState[k] |= pPrev[k]; + } +} + /**Function************************************************************* @@ -300,8 +346,8 @@ Vec_Ptr_t * Aig_ManTernarySimulate( Aig_Man_t * p, int fVerbose ) Aig_Tsi_t * pTsi; Vec_Ptr_t * vMap; Aig_Obj_t * pObj, * pObjLi, * pObjLo; - unsigned * pState, * pPrev; - int i, k, f, fConstants, Value, nCounter; + unsigned * pState;//, * pPrev; + int i, f, fConstants, Value, nCounter; // allocate the simulation manager pTsi = Aig_TsiStart( p ); // initialize the values @@ -323,10 +369,16 @@ Vec_Ptr_t * Aig_ManTernarySimulate( Aig_Man_t * p, int fVerbose ) if ( Value & 2 ) Aig_InfoSetBit( pState, 2 * i + 1 ); } + +// printf( "%d ", Aig_TsiStateCount(pTsi, pState) ); // Aig_TsiStatePrint( pTsi, pState ); // check if this state exists if ( Aig_TsiStateLookup( pTsi, pState, pTsi->nWords ) ) break; +// nCounter = 0; +// Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i ) +// nCounter += (Aig_ObjGetXsim(pObjLo) == AIG_XVS0); +//printf( "%d -> ", nCounter ); // insert this state Aig_TsiStateInsert( pTsi, pState, pTsi->nWords ); // simulate internal nodes @@ -335,9 +387,23 @@ Vec_Ptr_t * Aig_ManTernarySimulate( Aig_Man_t * p, int fVerbose ) // transfer the latch values Aig_ManForEachLiSeq( p, pObj, i ) Aig_ObjSetXsim( pObj, Aig_ObjGetXsimFanin0(pObj) ); + nCounter = 0; Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i ) - Aig_ObjSetXsim( pObjLo, Aig_ObjGetXsim(pObjLi) ); + { + if ( f < TSI_ONE_SERIES ) + Aig_ObjSetXsim( pObjLo, Aig_ObjGetXsim(pObjLi) ); + else + { + if ( Aig_ObjGetXsim(pObjLi) != Aig_ObjGetXsim(pObjLo) ) + Aig_ObjSetXsim( pObjLo, AIG_XVSX ); + } + nCounter += (Aig_ObjGetXsim(pObjLo) == AIG_XVS0); + } +// if ( f && (f % 1000 == 0) ) +// printf( "%d \n", f ); +//printf( "%d ", nCounter ); } +//printf( "\n" ); if ( f == TSI_MAX_ROUNDS ) { printf( "Aig_ManTernarySimulate(): Did not reach a fixed point after %d iterations (not a bug).\n", TSI_MAX_ROUNDS ); @@ -346,11 +412,7 @@ Vec_Ptr_t * Aig_ManTernarySimulate( Aig_Man_t * p, int fVerbose ) } // OR all the states pState = Vec_PtrEntry( pTsi->vStates, 0 ); - Vec_PtrForEachEntry( pTsi->vStates, pPrev, i ) - { - for ( k = 0; k < pTsi->nWords; k++ ) - pState[k] |= pPrev[k]; - } + Aig_TsiStateOrAll( pTsi, pState ); // check if there are constants fConstants = 0; if ( 2*Aig_ManRegNum(p) == 32*pTsi->nWords ) diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h index 2ee84f39..cc64b024 100644 --- a/src/aig/fra/fra.h +++ b/src/aig/fra/fra.h @@ -50,6 +50,7 @@ extern "C" { //////////////////////////////////////////////////////////////////////// typedef struct Fra_Par_t_ Fra_Par_t; +typedef struct Fra_Ssw_t_ Fra_Ssw_t; typedef struct Fra_Man_t_ Fra_Man_t; typedef struct Fra_Cla_t_ Fra_Cla_t; typedef struct Fra_Sml_t_ Fra_Sml_t; @@ -86,6 +87,25 @@ struct Fra_Par_t_ int fDontShowBar; // does not show progressbar during fraiging }; +// seq SAT sweeping parametesr +struct Fra_Ssw_t_ +{ + int nPartSize; // size of the partition + int nOverSize; // size of the overlap between partitions + int nFramesP; // number of frames in the prefix + int nFramesK; // number of frames for induction (1=simple) + int nMaxImps; // max implications to consider + int nMaxLevs; // max levels to consider + int fUseImps; // use implications + int fRewrite; // enable rewriting of the specualatively reduced model + int fFraiging; // enable comb SAT sweeping as preprocessing + int fLatchCorr; // perform register correspondence + int fWriteImps; // write implications into a file + int fUse1Hot; // use one-hotness constraints + int fVerbose; // enable verbose output + int nIters; // the number of iterations performed +}; + // FRAIG equivalence classes struct Fra_Cla_t_ { @@ -287,7 +307,7 @@ extern double Fra_ImpComputeStateSpaceRatio( Fra_Man_t * p ); extern int Fra_ImpVerifyUsingSimulation( Fra_Man_t * p ); extern void Fra_ImpRecordInManager( Fra_Man_t * p, Aig_Man_t * pNew ); /*=== fraInd.c ========================================================*/ -extern Aig_Man_t * Fra_FraigInduction( Aig_Man_t * p, int nFramesP, int nFramesK, int nMaxImps, int nMaxLevs, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fUse1Hot, int fVerbose, int * pnIter ); +extern Aig_Man_t * Fra_FraigInduction( Aig_Man_t * p, Fra_Ssw_t * pPars ); /*=== fraIndVer.c =====================================================*/ extern int Fra_InvariantVerify( Aig_Man_t * p, int nFrames, Vec_Int_t * vClauses, Vec_Int_t * vLits ); /*=== fraLcr.c ========================================================*/ diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c index ea17706c..0715524e 100644 --- a/src/aig/fra/fraInd.c +++ b/src/aig/fra/fraInd.c @@ -234,7 +234,7 @@ void Fra_FramesAddMore( Aig_Man_t * p, int nFrames ) /**Function************************************************************* - Synopsis [Performs choicing of the AIG.] + Synopsis [Performs partitioned sequential SAT sweepingG.] Description [] @@ -243,7 +243,77 @@ void Fra_FramesAddMore( Aig_Man_t * p, int nFrames ) SeeAlso [] ***********************************************************************/ -Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK, int nMaxImps, int nMaxLevs, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fUse1Hot, int fVerbose, int * pnIter ) +Aig_Man_t * Fra_FraigInductionPart( Aig_Man_t * pAig, Fra_Ssw_t * pPars ) +{ + int fPrintParts = 0; + char Buffer[100]; + Aig_Man_t * pTemp, * pNew; + Vec_Ptr_t * vResult; + Vec_Int_t * vPart; + int * pMapBack; + int i, nCountPis, nCountRegs; + int nClasses, nPartSize, fVerbose; + + // save parameters + nPartSize = pPars->nPartSize; pPars->nPartSize = 0; + fVerbose = pPars->fVerbose; pPars->fVerbose = 0; + // generate partitions + vResult = Aig_ManRegPartitionSimple( pAig, nPartSize, pPars->nOverSize ); +// vResult = Aig_ManPartitionSmartRegisters( pAig, nPartSize, 0 ); +// vResult = Aig_ManRegPartitionSmart( pAig, nPartSize ); + if ( fPrintParts ) + { + // print partitions + printf( "Simple partitioning. %d partitions are saved:\n", Vec_PtrSize(vResult) ); + Vec_PtrForEachEntry( vResult, vPart, i ) + { + sprintf( Buffer, "part%03d.aig", i ); + pTemp = Aig_ManRegCreatePart( pAig, vPart, &nCountPis, &nCountRegs, NULL ); + Ioa_WriteAiger( pTemp, Buffer, 0, 0 ); + printf( "part%03d.aig : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d.\n", + i, Vec_IntSize(vPart), Aig_ManPiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp) ); + Aig_ManStop( pTemp ); + } + } + + // perform SSW with partitions + Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) ); + Vec_PtrForEachEntry( vResult, vPart, i ) + { + pTemp = Aig_ManRegCreatePart( pAig, vPart, &nCountPis, &nCountRegs, &pMapBack ); + // run SSW + pNew = Fra_FraigInduction( pTemp, pPars ); + nClasses = Aig_TransferMappedClasses( pAig, pTemp, pMapBack ); + if ( fVerbose ) + printf( "%3d : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d. It = %3d. Cl = %5d.\n", + i, Vec_IntSize(vPart), Aig_ManPiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp), pPars->nIters, nClasses ); + Aig_ManStop( pNew ); + Aig_ManStop( pTemp ); + free( pMapBack ); + } + // remap the AIG + pNew = Aig_ManDupRepr( pAig, 0 ); + Aig_ManSeqCleanup( pNew ); +// Aig_ManPrintStats( pAig ); +// Aig_ManPrintStats( pNew ); + Vec_VecFree( (Vec_Vec_t *)vResult ); + pPars->nPartSize = nPartSize; + pPars->fVerbose = fVerbose; + return pNew; +} + +/**Function************************************************************* + + Synopsis [Performs sequential SAT sweeping.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, Fra_Ssw_t * pParams ) { int fUseSimpleCnf = 0; int fUseOldSimulation = 0; @@ -263,13 +333,22 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK, if ( Aig_ManNodeNum(pManAig) == 0 ) { - if ( pnIter ) *pnIter = 0; + pParams->nIters = 0; return Aig_ManDup(pManAig, 1); } assert( Aig_ManLatchNum(pManAig) == 0 ); assert( Aig_ManRegNum(pManAig) > 0 ); - assert( nFramesK > 0 ); + assert( pParams->nFramesK > 0 ); //Aig_ManShow( pManAig, 0, NULL ); + + if ( pParams->fWriteImps && pParams->nPartSize > 0 ) + { + pParams->nPartSize = 0; + printf( "Partitioning was disabled to allow implication writing.\n" ); + } + // perform partitioning + if ( pParams->nPartSize > 0 && pParams->nPartSize < Aig_ManRegNum(pManAig) ) + return Fra_FraigInductionPart( pManAig, pParams ); nNodesBeg = Aig_ManNodeNum(pManAig); nRegsBeg = Aig_ManRegNum(pManAig); @@ -279,16 +358,16 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK, // get parameters Fra_ParamsDefaultSeq( pPars ); - pPars->nFramesP = nFramesP; - pPars->nFramesK = nFramesK; - pPars->nMaxImps = nMaxImps; - pPars->nMaxLevs = nMaxLevs; - pPars->fVerbose = fVerbose; - pPars->fRewrite = fRewrite; - pPars->fLatchCorr = fLatchCorr; - pPars->fUseImps = fUseImps; - pPars->fWriteImps = fWriteImps; - pPars->fUse1Hot = fUse1Hot; + pPars->nFramesP = pParams->nFramesP; + pPars->nFramesK = pParams->nFramesK; + pPars->nMaxImps = pParams->nMaxImps; + pPars->nMaxLevs = pParams->nMaxLevs; + pPars->fVerbose = pParams->fVerbose; + pPars->fRewrite = pParams->fRewrite; + pPars->fLatchCorr = pParams->fLatchCorr; + pPars->fUseImps = pParams->fUseImps; + pPars->fWriteImps = pParams->fWriteImps; + pPars->fUse1Hot = pParams->fUse1Hot; assert( !(pPars->nFramesP > 0 && pPars->fUse1Hot) ); assert( !(pPars->nFramesK > 1 && pPars->fUse1Hot) ); @@ -311,10 +390,10 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK, // bug: r iscas/blif/s5378.blif ; st; ssw -v // bug: r iscas/blif/s1238.blif ; st; ssw -v // refine the classes with more simulation rounds -if ( fVerbose ) +if ( pPars->fVerbose ) printf( "Simulating %d AIG nodes for %d cycles ... ", Aig_ManNodeNum(pManAig), pPars->nFramesP + 32 ); p->pSml = Fra_SmlSimulateSeq( pManAig, pPars->nFramesP, 32, 1 ); //pPars->nFramesK + 1, 1 ); -if ( fVerbose ) +if ( pPars->fVerbose ) { PRT( "Time", clock() - clk ); } @@ -408,7 +487,7 @@ p->timeTrav += clock() - clk2; Fra_OneHotAssume( p, p->vOneHots ); // report the intermediate results - if ( fVerbose ) + if ( pPars->fVerbose ) { printf( "%3d : Const = %6d. Class = %6d. L = %6d. LR = %6d. ", nIter, Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), @@ -428,7 +507,7 @@ clk2 = clock(); if ( p->pPars->fUse1Hot ) Fra_OneHotCheck( p, p->vOneHots ); Fra_FraigSweep( p ); - if ( fVerbose ) + if ( pPars->fVerbose ) { // PRT( "t", clock() - clk2 ); } @@ -508,7 +587,7 @@ p->timeTotal = clock() - clk; // if ( Aig_ManPoNum(pManAigNew) - Aig_ManRegNum(pManAigNew) == 1 ) // if ( Aig_ObjChild0( Aig_ManPo(pManAigNew,0) ) == Aig_ManConst0(pManAigNew) ) // printf( "Proved output constant 0.\n" ); - if ( pnIter ) *pnIter = nIter; + pParams->nIters = nIter; return pManAigNew; } diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c index a43d83b1..75d297cf 100644 --- a/src/aig/fra/fraSec.c +++ b/src/aig/fra/fraSec.c @@ -29,67 +29,6 @@ /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Fra_FraigSec2( Aig_Man_t * p, int nFramesFix, int fVerbose, int fVeryVerbose ) -{ - Aig_Man_t * pNew; - int nFrames, RetValue, nIter, clk, clkTotal = clock(); - int fLatchCorr = 0; - if ( nFramesFix ) - { - nFrames = nFramesFix; - // perform seq sweeping for one frame number - pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, 0, fLatchCorr, 0, 0, fVeryVerbose, &nIter ); - } - else - { - // perform seq sweeping while increasing the number of frames - for ( nFrames = 1; ; nFrames++ ) - { -clk = clock(); - pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, 0, fLatchCorr, 0, 0, fVeryVerbose, &nIter ); - RetValue = Fra_FraigMiterStatus( pNew ); - if ( fVerbose ) - { - printf( "FRAMES %3d : Iters = %3d. ", nFrames, nIter ); - if ( RetValue == 1 ) - printf( "UNSAT " ); - else - printf( "UNDECIDED " ); -PRT( "Time", clock() - clk ); - } - if ( RetValue != -1 ) - break; - Aig_ManStop( pNew ); - } - } - - // get the miter status - RetValue = Fra_FraigMiterStatus( pNew ); - Aig_ManStop( pNew ); - - // report the miter - if ( RetValue == 1 ) - printf( "Networks are equivalent after seq sweeping with K=%d frames (%d iters). ", nFrames, nIter ); - else if ( RetValue == 0 ) - printf( "Networks are NOT EQUIVALENT. " ); - else - printf( "Networks are UNDECIDED after seq sweeping with K=%d frames (%d iters). ", nFrames, nIter ); -PRT( "Time", clock() - clkTotal ); - return RetValue; -} - - /**Function************************************************************* Synopsis [] @@ -103,10 +42,15 @@ PRT( "Time", clock() - clkTotal ); ***********************************************************************/ int Fra_FraigSec( Aig_Man_t * p, int nFramesMax, int fRetimeFirst, int fVerbose, int fVeryVerbose ) { + Fra_Ssw_t Pars, * pPars = &Pars; Fra_Sml_t * pSml; Aig_Man_t * pNew, * pTemp; int nFrames, RetValue, nIter, clk, clkTotal = clock(); int fLatchCorr = 0; + // prepare parameters + memset( pPars, 0, sizeof(Fra_Ssw_t) ); + pPars->fLatchCorr = fLatchCorr; + pPars->fVerbose = fVeryVerbose; pNew = Aig_ManDup( p, 1 ); if ( fVerbose ) @@ -185,13 +129,14 @@ PRT( "Time", clock() - clk ); for ( nFrames = 1; nFrames <= nFramesMax; nFrames *= 2 ) { clk = clock(); - pNew = Fra_FraigInduction( pTemp = pNew, 0, nFrames, 0, 0, 0, 0, fLatchCorr, 0, 0, fVeryVerbose, &nIter ); + pPars->nFramesK = nFrames; + pNew = Fra_FraigInduction( pTemp = pNew, pPars ); Aig_ManStop( pTemp ); RetValue = Fra_FraigMiterStatus( pNew ); if ( fVerbose ) { printf( "K-step (K=%2d,I=%3d): Latches = %5d. Nodes = %6d. ", - nFrames, nIter, Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) ); + nFrames, pPars->nIters, Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) ); PRT( "Time", clock() - clk ); } if ( RetValue != -1 ) diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index fdff8b39..86cc7e62 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -567,6 +567,8 @@ extern void * Abc_NodeGetCuts( void * p, Abc_Obj_t * pObj, int fDag, extern void Abc_NodeGetCutsSeq( void * p, Abc_Obj_t * pObj, int fFirst ); extern void * Abc_NodeReadCuts( void * p, Abc_Obj_t * pObj ); extern void Abc_NodeFreeCuts( void * p, Abc_Obj_t * pObj ); +/*=== abcDelay.c ==========================================================*/ +extern float Abc_NtkDelayTraceLut( Abc_Ntk_t * pNtk, int fUseLutLib ); /*=== abcDfs.c ==========================================================*/ extern Vec_Ptr_t * Abc_NtkDfs( Abc_Ntk_t * pNtk, int fCollectAll ); extern Vec_Ptr_t * Abc_NtkDfsNodes( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes ); @@ -733,7 +735,7 @@ extern bool Abc_NodeIsBuf( Abc_Obj_t * pNode ); extern bool Abc_NodeIsInv( Abc_Obj_t * pNode ); extern void Abc_NodeComplement( Abc_Obj_t * pNode ); /*=== abcPrint.c ==========================================================*/ -extern void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSaveBest ); +extern void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSaveBest, int fDumpResult, int fUseLutLib ); extern void Abc_NtkPrintIo( FILE * pFile, Abc_Ntk_t * pNtk ); extern void Abc_NtkPrintLatch( FILE * pFile, Abc_Ntk_t * pNtk ); extern void Abc_NtkPrintFanio( FILE * pFile, Abc_Ntk_t * pNtk ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 492d1910..99da9201 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -30,6 +30,7 @@ #include "aig.h" #include "dar.h" #include "mfs.h" +#include "fra.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -442,6 +443,8 @@ int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Ntk_t * pNtk; int fFactor; int fSaveBest; + int fDumpResult; + int fUseLutLib; int c; pNtk = Abc_FrameReadNtk(pAbc); @@ -451,8 +454,10 @@ int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv ) // set the defaults fFactor = 0; fSaveBest = 0; + fDumpResult = 0; + fUseLutLib = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "fbh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "fbdlh" ) ) != EOF ) { switch ( c ) { @@ -462,6 +467,12 @@ int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'b': fSaveBest ^= 1; break; + case 'd': + fDumpResult ^= 1; + break; + case 'l': + fUseLutLib ^= 1; + break; case 'h': goto usage; default: @@ -474,14 +485,16 @@ int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( Abc_FrameReadErr(pAbc), "Empty network.\n" ); return 1; } - Abc_NtkPrintStats( pOut, pNtk, fFactor, fSaveBest ); + Abc_NtkPrintStats( pOut, pNtk, fFactor, fSaveBest, fDumpResult, fUseLutLib ); return 0; usage: - fprintf( pErr, "usage: print_stats [-fbh]\n" ); + fprintf( pErr, "usage: print_stats [-fbdlh]\n" ); fprintf( pErr, "\t prints the network statistics\n" ); fprintf( pErr, "\t-f : toggles printing the literal count in the factored forms [default = %s]\n", fFactor? "yes": "no" ); fprintf( pErr, "\t-b : toggles saving the best logic network in \"best.blif\" [default = %s]\n", fSaveBest? "yes": "no" ); + fprintf( pErr, "\t-d : toggles dumping network into file \"_dump.blif\" [default = %s]\n", fDumpResult? "yes": "no" ); + fprintf( pErr, "\t-l : toggles printing delay of LUT mapping using LUT library [default = %s]\n", fSaveBest? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; } @@ -567,7 +580,7 @@ int Abc_CommandPrintExdc( Abc_Frame_t * pAbc, int argc, char ** argv ) } else printf( "EXDC network statistics: \n" ); - Abc_NtkPrintStats( pOut, pNtk->pExdc, 0, 0 ); + Abc_NtkPrintStats( pOut, pNtk->pExdc, 0, 0, 0, 0 ); return 0; usage: @@ -672,7 +685,7 @@ int Abc_CommandPrintLatch( Abc_Frame_t * pAbc, int argc, char ** argv ) pErr = Abc_FrameReadErr(pAbc); // set defaults - fPrintSccs = 0; + fPrintSccs = 1; Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "sh" ) ) != EOF ) { @@ -6829,7 +6842,8 @@ usage: int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; - Abc_Ntk_t * pNtk;//, * pNtkRes; + Abc_Ntk_t * pNtk; +// Abc_Ntk_t * pNtkRes; int c; int fBmc; int nFrames; @@ -6849,14 +6863,14 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) // extern Abc_Ntk_t * Abc_NtkPcmTest( Abc_Ntk_t * pNtk, int fVerbose ); extern Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk ); // extern void Abc_NtkDarTestBlif( char * pFileName ); - extern void Abc_NtkDarPartition( Abc_Ntk_t * pNtk ); +// extern Abc_Ntk_t * Abc_NtkDarPartition( Abc_Ntk_t * pNtk ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); -// printf( "This command is temporarily disabled.\n" ); -// return 0; + printf( "This command is temporarily disabled.\n" ); + return 0; // set defaults fVeryVerbose = 0; @@ -7032,8 +7046,17 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_NtkDarTestBlif( argv[globalUtilOptind] ); */ - Abc_NtkDarPartition( pNtk ); - +// Abc_NtkDarPartition( pNtk ); +/* + pNtkRes = Abc_NtkDarPartition( pNtk ); + if ( pNtkRes == NULL ) + { + fprintf( pErr, "Command has failed.\n" ); + return 1; + } + // replace the current network + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); +*/ return 0; usage: fprintf( pErr, "usage: test [-vwh]\n" ); @@ -10825,6 +10848,9 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv ) } // get LUT size from the library pPars->nLutSize = pPars->pLutLib->LutMax; + // if variable pin delay, force truth table computation + if ( pPars->pLutLib->fVarPinDelays ) + pPars->fTruth = 1; } if ( pPars->nLutSize < 3 || pPars->nLutSize > IF_MAX_LUTSIZE ) @@ -11646,6 +11672,7 @@ usage: fprintf( pErr, "\t-h : print the command usage\n"); return 1; } + /**Function************************************************************* Synopsis [] @@ -11665,12 +11692,14 @@ int Abc_CommandFlowRetime( Abc_Frame_t * pAbc, int argc, char ** argv ) int fForward; int fBackward; int fVerbose; - int fComputeInit; + int fComputeInit, fGuaranteeInit, fBlockConst; + int fFastButConservative; int maxDelay; - extern Abc_Ntk_t* Abc_FlowRetime_MinReg( Abc_Ntk_t * pNtk, int fVerbose, int fComputeInit, + extern Abc_Ntk_t* Abc_FlowRetime_MinReg( Abc_Ntk_t * pNtk, int fVerbose, + int fComputeInit, int fGuaranteeInit, int fBlockConst, int fForward, int fBackward, int nMaxIters, - int maxDelay); + int maxDelay, int fFastButConservative); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -11678,13 +11707,16 @@ int Abc_CommandFlowRetime( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults fForward = 0; + fFastButConservative = 0; fBackward = 0; fComputeInit = 1; + fGuaranteeInit = 0; fVerbose = 0; + fBlockConst = 0; nMaxIters = 999; maxDelay = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "MDfbivh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "MDfcgbkivh" ) ) != EOF ) { switch ( c ) { @@ -11709,16 +11741,25 @@ int Abc_CommandFlowRetime( Abc_Frame_t * pAbc, int argc, char ** argv ) globalUtilOptind++; if ( maxDelay < 0 ) goto usage; - break; + break; case 'f': fForward ^= 1; break; + case 'c': + fFastButConservative ^= 1; + break; case 'i': fComputeInit ^= 1; break; case 'b': fBackward ^= 1; break; + case 'g': + fGuaranteeInit ^= 1; + break; + case 'k': + fBlockConst ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -11741,6 +11782,12 @@ int Abc_CommandFlowRetime( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } + if ( fGuaranteeInit && !fComputeInit ) + { + fprintf( pErr, "Initial state guarantee (-g) requires initial state computation (-i).\n" ); + return 1; + } + if ( !Abc_NtkLatchNum(pNtk) ) { fprintf( pErr, "The network has no latches. Retiming is not performed.\n" ); @@ -11754,7 +11801,10 @@ int Abc_CommandFlowRetime( Abc_Frame_t * pAbc, int argc, char ** argv ) } // perform the retiming - pNtkRes = Abc_FlowRetime_MinReg( pNtk, fVerbose, fComputeInit, fForward, fBackward, nMaxIters, maxDelay ); + pNtkRes = Abc_FlowRetime_MinReg( pNtk, fVerbose, fComputeInit, + fGuaranteeInit, fBlockConst, + fForward, fBackward, + nMaxIters, maxDelay, fFastButConservative ); if (pNtkRes != pNtk) Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); @@ -11767,6 +11817,9 @@ usage: fprintf( pErr, "\t-M num : the maximum number of iterations [default = %d]\n", nMaxIters ); fprintf( pErr, "\t-D num : the maximum delay [default = none]\n" ); fprintf( pErr, "\t-i : enables init state computation [default = %s]\n", fComputeInit? "yes": "no" ); + fprintf( pErr, "\t-k : blocks retiming over const nodes [default = %s]\n", fBlockConst? "yes": "no" ); + fprintf( pErr, "\t-g : guarantees init state computation [default = %s]\n", fGuaranteeInit? "yes": "no" ); + fprintf( pErr, "\t-c : very fast (but conserv.) delay constraints [default = %s]\n", fFastButConservative? "yes": "no" ); fprintf( pErr, "\t-f : enables forward-only retiming [default = %s]\n", fForward? "yes": "no" ); fprintf( pErr, "\t-b : enables backward-only retiming [default = %s]\n", fBackward? "yes": "no" ); fprintf( pErr, "\t-v : enables verbose output [default = %s]\n", fVerbose? "yes": "no" ); @@ -12044,38 +12097,30 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; Abc_Ntk_t * pNtk, * pNtkRes; + Fra_Ssw_t Pars, * pPars = &Pars; int c; - int nFramesP; - int nFramesK; - int nMaxImps; - int nMaxLevs; - int fUseImps; - int fRewrite; - int fFraiging; - int fLatchCorr; - int fWriteImps; - int fUse1Hot; - int fVerbose; - extern Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFrames, int nMaxImps, int nMaxLevs, int fRewrite, int fFraiging, int fUseImps, int fLatchCorr, int fWriteImps, int fUse1Hot, int fVerbose ); + extern Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, Fra_Ssw_t * pPars ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); // set defaults - nFramesP = 0; - nFramesK = 1; - nMaxImps = 5000; - nMaxLevs = 0; - fUseImps = 0; - fRewrite = 0; - fFraiging = 0; - fLatchCorr = 0; - fWriteImps = 0; - fUse1Hot = 0; - fVerbose = 0; + pPars->nPartSize = 0; + pPars->nOverSize = 0; + pPars->nFramesP = 0; + pPars->nFramesK = 1; + pPars->nMaxImps = 5000; + pPars->nMaxLevs = 0; + pPars->fUseImps = 0; + pPars->fRewrite = 0; + pPars->fFraiging = 0; + pPars->fLatchCorr = 0; + pPars->fWriteImps = 0; + pPars->fUse1Hot = 0; + pPars->fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "PFILirfletvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "PQNFILirfletvh" ) ) != EOF ) { switch ( c ) { @@ -12085,9 +12130,31 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Command line switch \"-P\" should be followed by an integer.\n" ); goto usage; } - nFramesP = atoi(argv[globalUtilOptind]); + pPars->nPartSize = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( nFramesP < 0 ) + if ( pPars->nPartSize < 2 ) + goto usage; + break; + case 'Q': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-Q\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nOverSize = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nOverSize < 0 ) + goto usage; + break; + case 'N': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nFramesP = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nFramesP < 0 ) goto usage; break; case 'F': @@ -12096,9 +12163,9 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" ); goto usage; } - nFramesK = atoi(argv[globalUtilOptind]); + pPars->nFramesK = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( nFramesK <= 0 ) + if ( pPars->nFramesK <= 0 ) goto usage; break; case 'I': @@ -12107,9 +12174,9 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Command line switch \"-I\" should be followed by an integer.\n" ); goto usage; } - nMaxImps = atoi(argv[globalUtilOptind]); + pPars->nMaxImps = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( nMaxImps <= 0 ) + if ( pPars->nMaxImps <= 0 ) goto usage; break; case 'L': @@ -12118,31 +12185,31 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Command line switch \"-L\" should be followed by an integer.\n" ); goto usage; } - nMaxLevs = atoi(argv[globalUtilOptind]); + pPars->nMaxLevs = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( nMaxLevs <= 0 ) + if ( pPars->nMaxLevs <= 0 ) goto usage; break; case 'i': - fUseImps ^= 1; + pPars->fUseImps ^= 1; break; case 'r': - fRewrite ^= 1; + pPars->fRewrite ^= 1; break; case 'f': - fFraiging ^= 1; + pPars->fFraiging ^= 1; break; case 'l': - fLatchCorr ^= 1; + pPars->fLatchCorr ^= 1; break; case 'e': - fWriteImps ^= 1; + pPars->fWriteImps ^= 1; break; case 't': - fUse1Hot ^= 1; + pPars->fUse1Hot ^= 1; break; case 'v': - fVerbose ^= 1; + pPars->fVerbose ^= 1; break; case 'h': goto usage; @@ -12169,20 +12236,20 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; } - if ( nFramesK > 1 && fUse1Hot ) + if ( pPars->nFramesK > 1 && pPars->fUse1Hot ) { printf( "Currrently can only use one-hotness for simple induction (K=1).\n" ); return 0; } - if ( nFramesP && fUse1Hot ) + if ( pPars->nFramesP && pPars->fUse1Hot ) { printf( "Currrently can only use one-hotness without prefix.\n" ); return 0; } // get the new network - pNtkRes = Abc_NtkDarSeqSweep( pNtk, nFramesP, nFramesK, nMaxImps, nMaxLevs, fRewrite, fFraiging, fUseImps, fLatchCorr, fWriteImps, fUse1Hot, fVerbose ); + pNtkRes = Abc_NtkDarSeqSweep( pNtk, pPars ); if ( pNtkRes == NULL ) { fprintf( pErr, "Sequential sweeping has failed.\n" ); @@ -12193,19 +12260,21 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: ssweep [-P num] [-F num] [-I num] [-ilrfetvh]\n" ); + fprintf( pErr, "usage: ssweep [-PQNFL num] [-lrfetvh]\n" ); fprintf( pErr, "\t performs sequential sweep using K-step induction\n" ); - fprintf( pErr, "\t-P num : number of time frames to use as the prefix [default = %d]\n", nFramesP ); - fprintf( pErr, "\t-F num : number of time frames for induction (1=simple) [default = %d]\n", nFramesK ); - fprintf( pErr, "\t-I num : max number of implications to consider [default = %d]\n", nMaxImps ); - fprintf( pErr, "\t-L num : max number of levels to consider (0=all) [default = %d]\n", nMaxLevs ); - fprintf( pErr, "\t-i : toggle using implications [default = %s]\n", fUseImps? "yes": "no" ); - fprintf( pErr, "\t-l : toggle latch correspondence only [default = %s]\n", fLatchCorr? "yes": "no" ); - fprintf( pErr, "\t-r : toggle AIG rewriting [default = %s]\n", fRewrite? "yes": "no" ); - fprintf( pErr, "\t-f : toggle fraiging (combinational SAT sweeping) [default = %s]\n", fFraiging? "yes": "no" ); - fprintf( pErr, "\t-e : toggle writing implications as assertions [default = %s]\n", fWriteImps? "yes": "no" ); - fprintf( pErr, "\t-t : toggle using one-hotness conditions [default = %s]\n", fUse1Hot? "yes": "no" ); - fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" ); + fprintf( pErr, "\t-P num : max partition size (0 = no partitioning) [default = %d]\n", pPars->nPartSize ); + fprintf( pErr, "\t-Q num : partition overlap (0 = no overlap) [default = %d]\n", pPars->nOverSize ); + fprintf( pErr, "\t-N num : number of time frames to use as the prefix [default = %d]\n", pPars->nFramesP ); + fprintf( pErr, "\t-F num : number of time frames for induction (1=simple) [default = %d]\n", pPars->nFramesK ); + fprintf( pErr, "\t-L num : max number of levels to consider (0=all) [default = %d]\n", pPars->nMaxLevs ); +// fprintf( pErr, "\t-I num : max number of implications to consider [default = %d]\n", pPars->nMaxImps ); +// fprintf( pErr, "\t-i : toggle using implications [default = %s]\n", pPars->fUseImps? "yes": "no" ); + fprintf( pErr, "\t-l : toggle latch correspondence only [default = %s]\n", pPars->fLatchCorr? "yes": "no" ); + fprintf( pErr, "\t-r : toggle AIG rewriting [default = %s]\n", pPars->fRewrite? "yes": "no" ); + fprintf( pErr, "\t-f : toggle fraiging (combinational SAT sweeping) [default = %s]\n", pPars->fFraiging? "yes": "no" ); + fprintf( pErr, "\t-e : toggle writing implications as assertions [default = %s]\n", pPars->fWriteImps? "yes": "no" ); + fprintf( pErr, "\t-t : toggle using one-hotness conditions [default = %s]\n", pPars->fUse1Hot? "yes": "no" ); + fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; } @@ -12331,29 +12400,29 @@ int Abc_CommandSeqCleanup( Abc_Frame_t * pAbc, int argc, char ** argv ) FILE * pOut, * pErr; Abc_Ntk_t * pNtk, * pNtkRes; int c; - int fLatchSweep; - int fAutoSweep; + int fLatchConst; + int fLatchEqual; int fVerbose; - extern Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fLatchSweep, int fVerbose ); + extern Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fLatchConst, int fLatchEqual, int fVerbose ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); // set defaults - fLatchSweep = 0; - fAutoSweep = 0; + fLatchConst = 1; + fLatchEqual = 1; fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "lavh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "cevh" ) ) != EOF ) { switch ( c ) { - case 'l': - fLatchSweep ^= 1; + case 'c': + fLatchConst ^= 1; break; - case 'a': - fAutoSweep ^= 1; + case 'e': + fLatchEqual ^= 1; break; case 'v': fVerbose ^= 1; @@ -12380,7 +12449,7 @@ int Abc_CommandSeqCleanup( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } // modify the current network - pNtkRes = Abc_NtkDarLatchSweep( pNtk, fLatchSweep, fVerbose ); + pNtkRes = Abc_NtkDarLatchSweep( pNtk, fLatchConst, fLatchEqual, fVerbose ); if ( pNtkRes == NULL ) { fprintf( pErr, "Sequential cleanup has failed.\n" ); @@ -12391,13 +12460,11 @@ int Abc_CommandSeqCleanup( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: scleanup [-lvh]\n" ); - fprintf( pErr, "\t performs sequential cleanup\n" ); - fprintf( pErr, "\t - removes nodes/latches that do not feed into POs\n" ); - fprintf( pErr, "\t - removes stuck-at and identical latches (latch sweep)\n" ); -// fprintf( pErr, "\t - replaces autonomous logic by free PI variables\n" ); - fprintf( pErr, "\t-l : toggle sweeping latches [default = %s]\n", fLatchSweep? "yes": "no" ); -// fprintf( pErr, "\t-a : toggle removing autonomous logic [default = %s]\n", fAutoSweep? "yes": "no" ); + fprintf( pErr, "usage: scleanup [-cevh]\n" ); + fprintf( pErr, "\t performs sequential cleanup of the current network\n" ); + fprintf( pErr, "\t by removing nodes and latches that do not feed into POs\n" ); + fprintf( pErr, "\t-c : sweep stuck-at latches detected by ternary simulation [default = %s]\n", fLatchConst? "yes": "no" ); + fprintf( pErr, "\t-e : merge equal latches (same data inputs and init states) [default = %s]\n", fLatchEqual? "yes": "no" ); fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; @@ -13901,7 +13968,7 @@ usage: fprintf( pErr, "\t perform bounded model checking\n" ); fprintf( pErr, "\t-F num : the number of time frames [default = %d]\n", nFrames ); fprintf( pErr, "\t-C num : the max number of conflicts at a node [default = %d]\n", nBTLimit ); - fprintf( pErr, "\t-r : toggle initialization of the first frame [default = %s]\n", fRewrite? "yes": "no" ); + fprintf( pErr, "\t-r : toggle the use of rewriting [default = %s]\n", fRewrite? "yes": "no" ); fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 119a2a97..6f5138c8 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -263,6 +263,25 @@ Abc_Ntk_t * Abc_NtkFromDarSeqSweep( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan ) Abc_NtkAddDummyBoxNames( pNtkNew ); else { + { + int i, k, iFlop, Counter = 0; + FILE * pFile; + pFile = fopen( "out.txt", "w" ); + fprintf( pFile, "The total of %d registers were removed (out of %d):\n", + Abc_NtkLatchNum(pNtkOld)-Vec_IntSize(pMan->vFlopNums), Abc_NtkLatchNum(pNtkOld) ); + for ( i = 0; i < Abc_NtkLatchNum(pNtkOld); i++ ) + { + Vec_IntForEachEntry( pMan->vFlopNums, iFlop, k ) + { + if ( i == iFlop ) + break; + } + if ( k == Vec_IntSize(pMan->vFlopNums) ) + fprintf( pFile, "%6d (%6d) : %s\n", ++Counter, i, Abc_ObjName( Abc_ObjFanout0(Abc_NtkBox(pNtkOld, i)) ) ); + } + fclose( pFile ); + //printf( "\n" ); + } assert( Abc_NtkBoxNum(pNtkOld) == Abc_NtkLatchNum(pNtkOld) ); nDigits = Extra_Base10Log( Abc_NtkLatchNum(pNtkNew) ); Abc_NtkForEachLatch( pNtkNew, pObjNew, i ) @@ -1034,7 +1053,7 @@ PRT( "Time", clock() - clkTotal ); SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFramesK, int nMaxImps, int nMaxLevs, int fRewrite, int fFraiging, int fUseImps, int fLatchCorr, int fWriteImps, int fUse1Hot, int fVerbose ) +Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, Fra_Ssw_t * pPars ) { Fraig_Params_t Params; Abc_Ntk_t * pNtkAig, * pNtkFraig; @@ -1046,21 +1065,23 @@ Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFramesK, in // so fraiging does not reduce the number of functions represented by nodes Fraig_ParamsSetDefault( &Params ); Params.nBTLimit = 100000; - if ( fFraiging ) + if ( pPars->fFraiging && pPars->nPartSize == 0 ) + { pNtkFraig = Abc_NtkFraig( pNtk, &Params, 0, 0 ); - else - pNtkFraig = Abc_NtkDup( pNtk ); -if ( fVerbose ) +if ( pPars->fVerbose ) { PRT( "Initial fraiging time", clock() - clk ); } + } + else + pNtkFraig = Abc_NtkDup( pNtk ); pMan = Abc_NtkToDar( pNtkFraig, 1 ); Abc_NtkDelete( pNtkFraig ); if ( pMan == NULL ) return NULL; - pMan = Fra_FraigInduction( pTemp = pMan, nFramesP, nFramesK, nMaxImps, nMaxLevs, fRewrite, fUseImps, fLatchCorr, fWriteImps, fUse1Hot, fVerbose, NULL ); + pMan = Fra_FraigInduction( pTemp = pMan, pPars ); Aig_ManStop( pTemp ); if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) ) @@ -1283,7 +1304,7 @@ int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fRetim SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fLatchSweep, int fVerbose ) +Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fLatchConst, int fLatchEqual, int fVerbose ) { Abc_Ntk_t * pNtkAig; Aig_Man_t * pMan; @@ -1291,13 +1312,10 @@ Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fLatchSweep, int fVerbos if ( pMan == NULL ) return NULL; Aig_ManSeqCleanup( pMan ); - if ( fLatchSweep ) - { - if ( pMan->nRegs ) - pMan = Aig_ManReduceLaches( pMan, fVerbose ); - if ( pMan->nRegs ) - pMan = Aig_ManConstReduce( pMan, fVerbose ); - } + if ( fLatchConst && pMan->nRegs ) + pMan = Aig_ManConstReduce( pMan, fVerbose ); + if ( fLatchEqual && pMan->nRegs ) + pMan = Aig_ManReduceLaches( pMan, fVerbose ); pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan ); Aig_ManStop( pMan ); return pNtkAig; @@ -1557,41 +1575,16 @@ Abc_Ntk_t * Abc_NtkInter( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fVerbose ***********************************************************************/ void Abc_NtkPrintSccs( Abc_Ntk_t * pNtk, int fVerbose ) { +// extern Vec_Ptr_t * Aig_ManRegPartitionLinear( Aig_Man_t * pAig, int nPartSize ); Aig_Man_t * pMan; pMan = Abc_NtkToDar( pNtk, 1 ); if ( pMan == NULL ) return; Aig_ManComputeSccs( pMan ); +// Aig_ManRegPartitionLinear( pMan, 1000 ); Aig_ManStop( pMan ); } -/**Function************************************************************* - - Synopsis [Performs partitioning.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NtkDarPartition( Abc_Ntk_t * pNtk ) -{ - extern void Aig_ManRegPartitionRun( Aig_Man_t * pAig ); - Aig_Man_t * pMan; - - // convert to the AIG manager - assert( Abc_NtkIsStrash(pNtk) ); - pMan = Abc_NtkToDar( pNtk, 1 ); - if ( pMan == NULL ) - return; - - Aig_ManRegPartitionRun( pMan ); - Aig_ManStop( pMan ); -} - - #include "ntl.h" diff --git a/src/base/abci/abcDelay.c b/src/base/abci/abcDelay.c index 7317b41b..bb654b73 100644 --- a/src/base/abci/abcDelay.c +++ b/src/base/abci/abcDelay.c @@ -74,7 +74,7 @@ void Abc_NtkDelayTraceSortPins( Abc_Obj_t * pNode, int * pPinPerm, float * pPinD pPinPerm[best_i] = temp; } // verify - assert( pPinPerm[0] < Abc_ObjFaninNum(pNode) ); + assert( Abc_ObjFaninNum(pNode) == 0 || pPinPerm[0] < Abc_ObjFaninNum(pNode) ); for ( i = 1; i < Abc_ObjFaninNum(pNode); i++ ) { assert( pPinPerm[i] < Abc_ObjFaninNum(pNode) ); @@ -96,6 +96,7 @@ void Abc_NtkDelayTraceSortPins( Abc_Obj_t * pNode, int * pPinPerm, float * pPinD float Abc_NtkDelayTraceLut( Abc_Ntk_t * pNtk, int fUseLutLib ) { extern void * Abc_FrameReadLibLut(); + int fUseSorting = 0; int pPinPerm[32]; float pPinDelays[32]; If_Lib_t * pLutLib; @@ -144,10 +145,19 @@ float Abc_NtkDelayTraceLut( Abc_Ntk_t * pNtk, int fUseLutLib ) else { pDelays = pLutLib->pLutDelays[Abc_ObjFaninNum(pNode)]; - Abc_NtkDelayTraceSortPins( pNode, pPinPerm, pPinDelays ); - Abc_ObjForEachFanin( pNode, pFanin, k ) - if ( tArrival < Abc_ObjArrival(Abc_ObjFanin(pNode,pPinPerm[k])) + pDelays[k] ) - tArrival = Abc_ObjArrival(Abc_ObjFanin(pNode,pPinPerm[k])) + pDelays[k]; + if ( fUseSorting ) + { + Abc_NtkDelayTraceSortPins( pNode, pPinPerm, pPinDelays ); + Abc_ObjForEachFanin( pNode, pFanin, k ) + if ( tArrival < Abc_ObjArrival(Abc_ObjFanin(pNode,pPinPerm[k])) + pDelays[k] ) + tArrival = Abc_ObjArrival(Abc_ObjFanin(pNode,pPinPerm[k])) + pDelays[k]; + } + else + { + Abc_ObjForEachFanin( pNode, pFanin, k ) + if ( tArrival < Abc_ObjArrival(pFanin) + pDelays[k] ) + tArrival = Abc_ObjArrival(pFanin) + pDelays[k]; + } } if ( Abc_ObjFaninNum(pNode) == 0 ) tArrival = 0.0; @@ -188,12 +198,24 @@ float Abc_NtkDelayTraceLut( Abc_Ntk_t * pNtk, int fUseLutLib ) else { pDelays = pLutLib->pLutDelays[Abc_ObjFaninNum(pNode)]; - Abc_NtkDelayTraceSortPins( pNode, pPinPerm, pPinDelays ); - Abc_ObjForEachFanin( pNode, pFanin, k ) + if ( fUseSorting ) { - tRequired = Abc_ObjRequired(pNode) - pDelays[k]; - if ( Abc_ObjRequired(Abc_ObjFanin(pNode,pPinPerm[k])) > tRequired ) - Abc_ObjSetRequired( Abc_ObjFanin(pNode,pPinPerm[k]), tRequired ); + Abc_NtkDelayTraceSortPins( pNode, pPinPerm, pPinDelays ); + Abc_ObjForEachFanin( pNode, pFanin, k ) + { + tRequired = Abc_ObjRequired(pNode) - pDelays[k]; + if ( Abc_ObjRequired(Abc_ObjFanin(pNode,pPinPerm[k])) > tRequired ) + Abc_ObjSetRequired( Abc_ObjFanin(pNode,pPinPerm[k]), tRequired ); + } + } + else + { + Abc_ObjForEachFanin( pNode, pFanin, k ) + { + tRequired = Abc_ObjRequired(pNode) - pDelays[k]; + if ( Abc_ObjRequired(pFanin) > tRequired ) + Abc_ObjSetRequired( pFanin, tRequired ); + } } } // set slack for this object @@ -265,8 +287,17 @@ unsigned Abc_NtkDelayTraceTCEdges( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, float tD void Abc_NtkDelayTracePrint( Abc_Ntk_t * pNtk, int fUseLutLib, int fVerbose ) { Abc_Obj_t * pNode; + If_Lib_t * pLutLib; int i, Nodes, * pCounters; float tArrival, tDelta, nSteps, Num; + // get the library + pLutLib = fUseLutLib? Abc_FrameReadLibLut() : NULL; + if ( pLutLib && pLutLib->LutMax < Abc_NtkGetFaninMax(pNtk) ) + { + printf( "The max LUT size (%d) is less than the max fanin count (%d).\n", + pLutLib->LutMax, Abc_NtkGetFaninMax(pNtk) ); + return; + } // decide how many steps nSteps = fUseLutLib ? 20 : Abc_NtkLevel(pNtk); pCounters = ALLOC( int, nSteps + 1 ); @@ -277,6 +308,8 @@ void Abc_NtkDelayTracePrint( Abc_Ntk_t * pNtk, int fUseLutLib, int fVerbose ) // count how many nodes have slack in the corresponding intervals Abc_NtkForEachNode( pNtk, pNode, i ) { + if ( Abc_ObjFaninNum(pNode) == 0 ) + continue; Num = Abc_ObjSlack(pNode) / tDelta; assert( Num >=0 && Num <= nSteps ); pCounters[(int)Num]++; @@ -356,15 +389,20 @@ int Abc_AigCheckTfi( Abc_Obj_t * pNew, Abc_Obj_t * pOld ) SeeAlso [] ***********************************************************************/ -void Abc_NtkSpeedupNode_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes ) +int Abc_NtkSpeedupNode_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes ) { if ( Abc_NodeIsTravIdCurrent(pNode) ) - return; + return 1; + if ( Abc_ObjIsCi(pNode) ) + return 0; assert( Abc_ObjIsNode(pNode) ); Abc_NodeSetTravIdCurrent( pNode ); - Abc_NtkSpeedupNode_rec( Abc_ObjFanin0(pNode), vNodes ); - Abc_NtkSpeedupNode_rec( Abc_ObjFanin1(pNode), vNodes ); + if ( !Abc_NtkSpeedupNode_rec( Abc_ObjFanin0(pNode), vNodes ) ) + return 0; + if ( !Abc_NtkSpeedupNode_rec( Abc_ObjFanin1(pNode), vNodes ) ) + return 0; Vec_PtrPush( vNodes, pNode ); + return 1; } /**Function************************************************************* @@ -405,7 +443,12 @@ void Abc_NtkSpeedupNode( Abc_Ntk_t * pNtk, Abc_Ntk_t * pAig, Abc_Obj_t * pNode, } // traverse from the root node pAnd = pNode->pCopy; - Abc_NtkSpeedupNode_rec( Abc_ObjRegular(pAnd), vNodes ); + if ( !Abc_NtkSpeedupNode_rec( Abc_ObjRegular(pAnd), vNodes ) ) + { +// printf( "Bad node!!!\n" ); + Vec_PtrFree( vNodes ); + return; + } // derive cofactors nCofs = (1 << Vec_PtrSize(vTimes)); diff --git a/src/base/abci/abcIf.c b/src/base/abci/abcIf.c index 5d24398b..742a3a02 100644 --- a/src/base/abci/abcIf.c +++ b/src/base/abci/abcIf.c @@ -252,6 +252,8 @@ Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t // create a new node pNodeNew = Abc_NtkCreateNode( pNtkNew ); pCutBest = If_ObjCutBest( pIfObj ); + if ( pIfMan->pPars->pLutLib && pIfMan->pPars->pLutLib->fVarPinDelays ) + If_CutRotatePins( pIfMan, pCutBest ); if ( pIfMan->pPars->fUseCnfs || pIfMan->pPars->fUseMv ) { If_CutForEachLeafReverse( pIfMan, pCutBest, pIfLeaf, i ) diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c index 5d35f329..239b155c 100644 --- a/src/base/abci/abcPrint.c +++ b/src/base/abci/abcPrint.c @@ -111,12 +111,20 @@ int Abc_NtkCompareAndSaveBest( Abc_Ntk_t * pNtk ) SeeAlso [] ***********************************************************************/ -void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSaveBest ) +void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSaveBest, int fDumpResult, int fUseLutLib ) { int Num; if ( fSaveBest ) Abc_NtkCompareAndSaveBest( pNtk ); + if ( fDumpResult ) + { + char Buffer[1000] = {0}; + char * pNameGen = pNtk->pSpec? Extra_FileNameGeneric( pNtk->pSpec ) : "nameless_"; + sprintf( Buffer, "%s_dump.blif", pNameGen ); + Io_Write( pNtk, Buffer, IO_FILE_BLIF ); + if ( pNtk->pSpec ) free( pNameGen ); + } // if ( Abc_NtkIsStrash(pNtk) ) // Abc_AigCountNext( pNtk->pManFunc ); @@ -181,7 +189,8 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSave fprintf( pFile, " lev = %3d", Abc_AigLevel(pNtk) ); else fprintf( pFile, " lev = %3d", Abc_NtkLevel(pNtk) ); - + if ( fUseLutLib && Abc_FrameReadLibLut() ) + fprintf( pFile, " delay = %5.2f", Abc_NtkDelayTraceLut(pNtk, 1) ); fprintf( pFile, "\n" ); // Abc_NtkCrossCut( pNtk ); diff --git a/src/map/if/if.h b/src/map/if/if.h index b3d2d745..19222f3b 100644 --- a/src/map/if/if.h +++ b/src/map/if/if.h @@ -170,10 +170,10 @@ struct If_Man_t_ // priority cut struct If_Cut_t_ { - float Delay; // delay of the cut float Area; // area (or area-flow) of the cut float AveRefs; // the average number of leaf references float Edge; // the edge flow + float Delay; // delay of the cut unsigned uSign; // cut signature unsigned Cost : 14; // the user's cost of the cut unsigned fCompl : 1; // the complemented attribute @@ -379,8 +379,10 @@ extern int If_ManPerformMappingSeq( If_Man_t * p ); /*=== ifTime.c ============================================================*/ extern float If_CutDelay( If_Man_t * p, If_Cut_t * pCut ); extern void If_CutPropagateRequired( If_Man_t * p, If_Cut_t * pCut, float Required ); +extern void If_CutRotatePins( If_Man_t * p, If_Cut_t * pCut ); /*=== ifTruth.c ===========================================================*/ extern void If_CutComputeTruth( If_Man_t * p, If_Cut_t * pCut, If_Cut_t * pCut0, If_Cut_t * pCut1, int fCompl0, int fCompl1 ); +extern void If_CutTruthPermute( unsigned * pOut, unsigned * pIn, int nVars, float * pDelays, int * pVars ); /*=== ifUtil.c ============================================================*/ extern void If_ManCleanNodeCopy( If_Man_t * p ); extern void If_ManCleanCutData( If_Man_t * p ); diff --git a/src/map/if/ifTime.c b/src/map/if/ifTime.c index 3d1dab1b..33bbdf74 100644 --- a/src/map/if/ifTime.c +++ b/src/map/if/ifTime.c @@ -221,6 +221,30 @@ void If_CutSortInputPins( If_Man_t * p, If_Cut_t * pCut, int * pPinPerm, float * } } +/**Function************************************************************* + + Synopsis [Sorts the pins in the decreasing order of delays.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void If_CutRotatePins( If_Man_t * p, If_Cut_t * pCut ) +{ + If_Obj_t * pLeaf; + float PinDelays[32]; +// int PinPerm[32]; + int i; + assert( p->pPars->pLutLib && p->pPars->pLutLib->fVarPinDelays && p->pPars->fTruth ); + If_CutForEachLeaf( p, pCut, pLeaf, i ) + PinDelays[i] = If_ObjCutBest(pLeaf)->Delay; + If_CutTruthPermute( p->puTemp[0], If_CutTruth(pCut), If_CutLeaveNum(pCut), PinDelays, If_CutLeaves(pCut) ); +// If_CutSortInputPins( p, pCut, PinPerm, PinDelays ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/map/if/ifTruth.c b/src/map/if/ifTruth.c index f18d8308..a3a7e1ee 100644 --- a/src/map/if/ifTruth.c +++ b/src/map/if/ifTruth.c @@ -124,6 +124,42 @@ void If_TruthSwapAdjacentVars( unsigned * pOut, unsigned * pIn, int nVars, int i } } +/**Function************************************************************* + + Synopsis [Implements given permutation of variables.] + + Description [Permutes truth table in-place (returns it in pIn).] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void If_CutTruthPermute( unsigned * pOut, unsigned * pIn, int nVars, float * pDelays, int * pVars ) +{ + unsigned * pTemp; + float tTemp; + int i, Temp, Counter = 0, fChange = 1; + while ( fChange ) + { + fChange = 0; + for ( i = 0; i < nVars - 1; i++ ) + { + if ( pDelays[i] >= pDelays[i+1] ) + continue; + tTemp = pDelays[i]; pDelays[i] = pDelays[i+1]; pDelays[i+1] = tTemp; + Temp = pVars[i]; pVars[i] = pVars[i+1]; pVars[i+1] = Temp; + If_TruthSwapAdjacentVars( pOut, pIn, nVars, i ); + pTemp = pOut; pOut = pIn; pIn = pTemp; + fChange = 1; + Counter++; + } + } + if ( Counter & 1 ) + If_TruthCopy( pOut, pIn, nVars ); +} + + /**Function************************************************************* Synopsis [Expands the truth table according to the phase.] diff --git a/src/opt/fret/fretFlow.c b/src/opt/fret/fretFlow.c index a9cef327..4b2bd936 100644 --- a/src/opt/fret/fretFlow.c +++ b/src/opt/fret/fretFlow.c @@ -73,6 +73,7 @@ void dfsfast_preorder( Abc_Ntk_t *pNtk ) { #endif // clear histogram + assert(pManMR->vSinkDistHist); memset(Vec_IntArray(pManMR->vSinkDistHist), 0, sizeof(int)*Vec_IntSize(pManMR->vSinkDistHist)); // seed queue : latches, PIOs, and blocks diff --git a/src/opt/fret/fretInit.c b/src/opt/fret/fretInit.c index 53df7386..47d338cb 100644 --- a/src/opt/fret/fretInit.c +++ b/src/opt/fret/fretInit.c @@ -23,6 +23,10 @@ #include "io.h" #include "fretime.h" #include "mio.h" +#include "hop.h" + +#undef DEBUG_PRINT_INIT_NTK + //////////////////////////////////////////////////////////////////////// /// FUNCTION PROTOTYPES /// @@ -31,20 +35,24 @@ static void Abc_FlowRetime_UpdateForwardInit_rec( Abc_Obj_t * pObj ); static void Abc_FlowRetime_VerifyBackwardInit( Abc_Ntk_t * pNtk ); static void Abc_FlowRetime_VerifyBackwardInit_rec( Abc_Obj_t * pObj ); -static Abc_Obj_t* Abc_FlowRetime_UpdateBackwardInit_rec( Abc_Obj_t *pOrigObj, - Abc_Obj_t *pUseThisPi, Vec_Ptr_t *vOtherPis, - int recurse); +static Abc_Obj_t* Abc_FlowRetime_UpdateBackwardInit_rec( Abc_Obj_t *pOrigObj ); + static void Abc_FlowRetime_SimulateNode( Abc_Obj_t * pObj ); static void Abc_FlowRetime_SimulateSop( Abc_Obj_t * pObj, char *pSop ); -extern void * Abc_FrameReadLibGen(); -extern Abc_Ntk_t * Abc_NtkRestrash( Abc_Ntk_t * pNtk, bool fCleanup ); +static void Abc_FlowRetime_SetInitToOrig( Abc_Obj_t *pInit, Abc_Obj_t *pOrig ); +static void Abc_FlowRetime_GetInitToOrig( Abc_Obj_t *pInit, Abc_Obj_t **pOrig, int *lag ); +static void Abc_FlowRetime_ClearInitToOrig( Abc_Obj_t *pInit ); +extern void * Abc_FrameReadLibGen(); + +extern void Abc_NtkMarkCone_rec( Abc_Obj_t * pObj, int fForward ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// + /**Function************************************************************* Synopsis [Updates initial state information.] @@ -69,6 +77,40 @@ Abc_FlowRetime_InitState( Abc_Ntk_t * pNtk ) { } } +/**Function************************************************************* + + Synopsis [Prints initial state information.] + + Description [Prints distribution of 0,1,and X initial states.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +inline int +Abc_FlowRetime_ObjFirstNonLatchBox( Abc_Obj_t * pOrigObj, Abc_Obj_t ** pResult ) { + int lag = 0; + Abc_Ntk_t *pNtk; + *pResult = pOrigObj; + pNtk = Abc_ObjNtk( pOrigObj ); + + Abc_NtkIncrementTravId( pNtk ); + + while( Abc_ObjIsBo(*pResult) || Abc_ObjIsLatch(*pResult) || Abc_ObjIsBi(*pResult) ) { + assert(Abc_ObjFaninNum(*pResult)); + *pResult = Abc_ObjFanin0(*pResult); + + if (Abc_NodeIsTravIdCurrent(*pResult)) + return -1; + Abc_NodeSetTravIdCurrent(*pResult); + + if (Abc_ObjIsLatch(*pResult)) ++lag; + } + + return lag; +} + /**Function************************************************************* @@ -152,6 +194,58 @@ void Abc_FlowRetime_UpdateForwardInit_rec( Abc_Obj_t * pObj ) { Abc_FlowRetime_SimulateNode( pObj ); } +/**Function************************************************************* + + Synopsis [Recursively evaluates HOP netlist.] + + Description [Exponential. There aren't enough flags on a HOP node.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static void Abc_FlowRetime_EvalHop_rec( Hop_Man_t *pHop, Hop_Obj_t *pObj, int *f, int *dc ) { + int f1, dc1, f2, dc2; + Hop_Obj_t *pReg = Hop_Regular(pObj); + + // const 0 + if (Hop_ObjIsConst1(pReg)) { + *f = 1; + *f ^= (pReg == pObj ? 1 : 0); + *dc = 0; + return; + } + + // PI + if (Hop_ObjIsPi(pReg)) { + *f = pReg->fMarkA; + *f ^= (pReg == pObj ? 1 : 0); + *dc = pReg->fMarkB; + return; + } + + // PO + if (Hop_ObjIsPo(pReg)) { + assert( pReg == pObj ); + Abc_FlowRetime_EvalHop_rec(pHop, Hop_ObjChild0(pReg), f, dc); + return; + } + + // AND + if (Hop_ObjIsAnd(pReg)) { + Abc_FlowRetime_EvalHop_rec(pHop, Hop_ObjChild0(pReg), &f1, &dc1); + Abc_FlowRetime_EvalHop_rec(pHop, Hop_ObjChild1(pReg), &f2, &dc2); + + *dc = (dc1 & f2) | (dc2 & f1) | (dc1 & dc2); + *f = f1 & f2; + *f ^= (pReg == pObj ? 1 : 0); + return; + } + + assert(0); +} + /**Function************************************************************* @@ -196,11 +290,13 @@ void Abc_FlowRetime_SimulateNode( Abc_Obj_t * pObj ) { int i, rAnd, rVar, dcAnd, dcVar; DdManager * dd = pNtk->pManFunc; DdNode *pBdd = pObj->pData, *pVar; + Hop_Man_t *pHop = pNtk->pManFunc; assert(!Abc_ObjIsLatch(pObj)); + assert(Abc_ObjRegular(pObj)); // (i) constant nodes - if (Abc_NtkHasAig(pNtk) && Abc_AigNodeIsConst(pObj)) { + if (Abc_NtkIsStrash(pNtk) && Abc_AigNodeIsConst(pObj)) { Abc_FlowRetime_SetInitValue(pObj, 1, 0); return; } @@ -258,10 +354,37 @@ void Abc_FlowRetime_SimulateNode( Abc_Obj_t * pObj ) { return; } - // ------ AIG network - else if ( Abc_NtkHasAig( pNtk )) { - assert(Abc_AigNodeIsAnd(pObj)); + // ------ AIG logic network + else if ( Abc_NtkHasAig( pNtk ) && !Abc_NtkIsStrash( pNtk )) { + + assert(Abc_ObjIsNode(pObj)); + assert(pObj->pData); + assert(Abc_ObjFaninNum(pObj) <= Hop_ManPiNum(pHop) ); + + // set vals at inputs + Abc_ObjForEachFanin(pObj, pFanin, i) { + Hop_ManPi(pHop, i)->fMarkA = FTEST(pFanin, INIT_1)?1:0; + Hop_ManPi(pHop, i)->fMarkB = FTEST(pFanin, INIT_CARE)?1:0; + } + + Abc_FlowRetime_EvalHop_rec( pHop, pObj->pData, &rVar, &dcVar ); + + Abc_FlowRetime_SetInitValue(pObj, rVar, dcVar); + + // clear flags + Abc_ObjForEachFanin(pObj, pFanin, i) { + Hop_ManPi(pHop, i)->fMarkA = 0; + Hop_ManPi(pHop, i)->fMarkB = 0; + } + + return; + } + + // ------ strashed network + else if ( Abc_NtkIsStrash( pNtk )) { + + assert(Abc_ObjType(pObj) == ABC_OBJ_NODE); dcAnd = 0, rAnd = 1; pFanin = Abc_ObjFanin0(pObj); @@ -361,7 +484,9 @@ void Abc_FlowRetime_SetupBackwardInit( Abc_Ntk_t * pNtk ) { Vec_Ptr_t *vObj = Vec_PtrAlloc(100); // create the network used for the initial state computation - if (Abc_NtkHasMapping(pNtk)) + if (Abc_NtkIsStrash(pNtk)) { + pManMR->pInitNtk = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP, 1 ); + } else if (Abc_NtkHasMapping(pNtk)) pManMR->pInitNtk = Abc_NtkAlloc( pNtk->ntkType, ABC_FUNC_SOP, 1 ); else pManMR->pInitNtk = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc, 1 ); @@ -371,14 +496,12 @@ void Abc_FlowRetime_SetupBackwardInit( Abc_Ntk_t * pNtk ) { // map latch to initial state network pPi = Abc_NtkCreatePi( pManMR->pInitNtk ); + // DEBUG + // printf("setup : mapping latch %d to PI %d\n", pLatch->Id, pPi->Id); + // has initial state requirement? if (Abc_LatchIsInit0(pLatch)) { - - if (Abc_NtkHasAig(pNtk)) - pObj = Abc_ObjNot( pPi ); - else - pObj = Abc_NtkCreateNodeInv( pManMR->pInitNtk, pPi ); - + pObj = Abc_NtkCreateNodeInv( pManMR->pInitNtk, pPi ); Vec_PtrPush(vObj, pObj); } else if (Abc_LatchIsInit1(pLatch)) { @@ -397,14 +520,9 @@ void Abc_FlowRetime_SetupBackwardInit( Abc_Ntk_t * pNtk ) { pManMR->fSolutionIsDc = 0; // mitre output - if (Abc_NtkHasAig(pNtk)) { - // create AND-by-AND - pObj = Vec_PtrPop( vObj ); - while( Vec_PtrSize(vObj) ) - pObj = Abc_AigAnd( pManMR->pInitNtk->pManFunc, pObj, Vec_PtrPop( vObj ) ); - } else - // create n-input AND gate - pObj = Abc_NtkCreateNodeAnd( pManMR->pInitNtk, vObj ); + + // create n-input AND gate + pObj = Abc_NtkCreateNodeAnd( pManMR->pInitNtk, vObj ); Abc_ObjAddFanin( Abc_NtkCreatePo( pManMR->pInitNtk ), pObj ); @@ -418,7 +536,7 @@ void Abc_FlowRetime_SetupBackwardInit( Abc_Ntk_t * pNtk ) { Description [] - SideEffects [] + SideEffects [Sets object copies in init ntk.] SeeAlso [] @@ -427,13 +545,13 @@ int Abc_FlowRetime_SolveBackwardInit( Abc_Ntk_t * pNtk ) { int i; Abc_Obj_t *pObj, *pInitObj; Vec_Ptr_t *vDelete = Vec_PtrAlloc(0); + Abc_Ntk_t *pSatNtk; int result; assert(pManMR->pInitNtk); // is the solution entirely DC's? if (pManMR->fSolutionIsDc) { - Abc_NtkDelete(pManMR->pInitNtk); Vec_PtrFree(vDelete); Abc_NtkForEachLatch( pNtk, pObj, i ) Abc_LatchSetInitDc( pObj ); vprintf("\tno init state computation: all-don't-care solution\n"); @@ -441,15 +559,10 @@ int Abc_FlowRetime_SolveBackwardInit( Abc_Ntk_t * pNtk ) { } // check that network is combinational - // mark superfluous BI nodes for deletion Abc_NtkForEachObj( pManMR->pInitNtk, pObj, i ) { assert(!Abc_ObjIsLatch(pObj)); assert(!Abc_ObjIsBo(pObj)); - - if (Abc_ObjIsBi(pObj)) { - Abc_ObjBetterTransferFanout( pObj, Abc_ObjFanin0(pObj), Abc_ObjFaninC0(pObj) ); - Vec_PtrPush( vDelete, pObj ); - } + assert(!Abc_ObjIsBi(pObj)); } // delete superfluous nodes @@ -464,9 +577,13 @@ int Abc_FlowRetime_SolveBackwardInit( Abc_Ntk_t * pNtk ) { Abc_NtkAddDummyPiNames(pManMR->pInitNtk); if (Abc_NtkIsLogic(pManMR->pInitNtk)) Abc_NtkCleanup(pManMR->pInitNtk, 0); - else if (Abc_NtkIsStrash(pManMR->pInitNtk)) { - Abc_NtkReassignIds(pManMR->pInitNtk); - } + +#if defined(DEBUG_PRINT_INIT_NTK) + Abc_NtkLevelReverse( pManMR->pInitNtk ); + Abc_NtkForEachObj( pManMR->pInitNtk, pObj, i ) + if (Abc_ObjLevel( pObj ) < 2) + Abc_ObjPrint(stdout, pObj); +#endif vprintf("\tsolving for init state (%d nodes)... ", Abc_NtkObjNum(pManMR->pInitNtk)); fflush(stdout); @@ -474,17 +591,19 @@ int Abc_FlowRetime_SolveBackwardInit( Abc_Ntk_t * pNtk ) { // convert SOPs to BDD if (Abc_NtkHasSop(pManMR->pInitNtk)) Abc_NtkSopToBdd( pManMR->pInitNtk ); + // convert AIGs to BDD + if (Abc_NtkHasAig(pManMR->pInitNtk)) + Abc_NtkAigToBdd( pManMR->pInitNtk ); + + pSatNtk = pManMR->pInitNtk; // solve - result = Abc_NtkMiterSat( pManMR->pInitNtk, (sint64)500000, (sint64)50000000, 0, NULL, NULL ); + result = Abc_NtkMiterSat( pSatNtk, (sint64)500000, (sint64)50000000, 0, NULL, NULL ); if (!result) { vprintf("SUCCESS\n"); } else { vprintf("FAILURE\n"); - printf("WARNING: no equivalent init state. setting all initial states to don't-cares\n"); - Abc_NtkForEachLatch( pNtk, pObj, i ) Abc_LatchSetInitDc( pObj ); - Abc_NtkDelete(pManMR->pInitNtk); return 0; } @@ -495,6 +614,9 @@ int Abc_FlowRetime_SolveBackwardInit( Abc_Ntk_t * pNtk ) { assert( Abc_ObjIsPi( pInitObj )); Abc_ObjSetCopy( pInitObj, pObj ); Abc_LatchSetInitNone( pObj ); + + // DEBUG + // printf("solve : getting latch %d from PI %d\n", pObj->Id, pInitObj->Id); } // copy solution from PIs to latches @@ -513,9 +635,6 @@ int Abc_FlowRetime_SolveBackwardInit( Abc_Ntk_t * pNtk ) { Abc_NtkForEachLatch( pNtk, pObj, i ) assert( !Abc_LatchIsInitNone( pObj ) ); #endif - // deallocate - Abc_NtkDelete( pManMR->pInitNtk ); - return 1; } @@ -534,7 +653,9 @@ int Abc_FlowRetime_SolveBackwardInit( Abc_Ntk_t * pNtk ) { void Abc_FlowRetime_UpdateBackwardInit( Abc_Ntk_t * pNtk ) { Abc_Obj_t *pOrigObj, *pInitObj; Vec_Ptr_t *vBo = Vec_PtrAlloc(100); - Vec_Ptr_t *vOldPis = Vec_PtrAlloc(100); + Vec_Ptr_t *vPi = Vec_PtrAlloc(100); + Abc_Ntk_t *pInitNtk = pManMR-> pInitNtk; + Abc_Obj_t *pBuf; int i; // remove PIs from network (from BOs) @@ -542,18 +663,43 @@ void Abc_FlowRetime_UpdateBackwardInit( Abc_Ntk_t * pNtk ) { if (Abc_ObjIsBo(pOrigObj)) { pInitObj = FDATA(pOrigObj)->pInitObj; assert(Abc_ObjIsPi(pInitObj)); - Vec_PtrPush(vBo, pOrigObj); - Abc_FlowRetime_UpdateBackwardInit_rec( Abc_ObjFanin0( pOrigObj ), pInitObj, vOldPis, 0 ); - } + // DEBUG + // printf("update : freeing PI %d\n", pInitObj->Id); + + // create a buffer instead + pBuf = Abc_NtkCreateNodeBuf( pInitNtk, NULL ); + Abc_FlowRetime_ClearInitToOrig( pBuf ); - // add PIs to network (at latches) - Abc_NtkForEachLatch( pNtk, pOrigObj, i ) - Abc_FlowRetime_UpdateBackwardInit_rec( pOrigObj, NULL, vOldPis, 0 ); + Abc_ObjBetterTransferFanout( pInitObj, pBuf, 0 ); + FDATA(pOrigObj)->pInitObj = pBuf; + pOrigObj->fMarkA = 1; + + Vec_PtrPush(vBo, pOrigObj); + Vec_PtrPush(vPi, pInitObj); + } - // connect nodes in init state network + // check that PIs are all free + Abc_NtkForEachPi( pInitNtk, pInitObj, i) { + assert( Abc_ObjFanoutNum( pInitObj ) == 0); + } + + // add PIs to to latches + Abc_NtkForEachLatch( pNtk, pOrigObj, i ) { + assert(Vec_PtrSize(vPi) > 0); + pInitObj = Vec_PtrPop(vPi); + + // DEBUG + // printf("update : mapping latch %d to PI %d\n", pOrigObj->Id, pInitObj->Id); + + pOrigObj->fMarkA = pOrigObj->fMarkB = 1; + FDATA(pOrigObj)->pInitObj = pInitObj; + Abc_ObjSetData(pOrigObj, pInitObj); + } + + // recursively build init network Vec_PtrForEachEntry( vBo, pOrigObj, i ) - Abc_FlowRetime_UpdateBackwardInit_rec( Abc_ObjFanin0( pOrigObj ), NULL, NULL, 1 ); + Abc_FlowRetime_UpdateBackwardInit_rec( pOrigObj ); // clear flags Abc_NtkForEachObj( pNtk, pOrigObj, i ) @@ -561,10 +707,93 @@ void Abc_FlowRetime_UpdateBackwardInit( Abc_Ntk_t * pNtk ) { // deallocate Vec_PtrFree( vBo ); - Vec_PtrFree( vOldPis ); + Vec_PtrFree( vPi ); } +/**Function************************************************************* + + Synopsis [Creates a corresponding node in the init state network] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Obj_t *Abc_FlowRetime_CopyNodeToInitNtk( Abc_Obj_t *pOrigObj ) { + Abc_Ntk_t *pNtk = pManMR->pNtk; + Abc_Ntk_t *pInitNtk = pManMR->pInitNtk; + Abc_Obj_t *pInitObj; + void *pData; + int fCompl[2]; + + assert(pOrigObj); + + // what we do depends on the ntk types of original / init networks... + + // (0) convert BI/BO nodes to buffers + if (Abc_ObjIsBi( pOrigObj ) || Abc_ObjIsBo( pOrigObj ) ) { + pInitObj = Abc_NtkCreateNodeBuf( pInitNtk, NULL ); + Abc_FlowRetime_ClearInitToOrig( pInitObj ); + return pInitObj; + } + + // (i) strash node -> SOP node + if (Abc_NtkIsStrash( pNtk )) { + + if (Abc_AigNodeIsConst( pOrigObj )) { + return Abc_NtkCreateNodeConst1( pInitNtk ); + } + if (!Abc_ObjIsNode( pOrigObj )) { + assert(Abc_ObjFaninNum(pOrigObj) == 1); + pInitObj = Abc_NtkCreateNodeBuf( pInitNtk, NULL ); + Abc_FlowRetime_ClearInitToOrig( pInitObj ); + return pInitObj; + } + + assert( Abc_ObjIsNode(pOrigObj) ); + pInitObj = Abc_NtkCreateObj( pInitNtk, ABC_OBJ_NODE ); + + fCompl[0] = pOrigObj->fCompl0 ? 1 : 0; + fCompl[1] = pOrigObj->fCompl1 ? 1 : 0; + + pData = Abc_SopCreateAnd( pInitNtk->pManFunc, 2, fCompl ); + assert(pData); + pInitObj->pData = Abc_SopRegister( pInitNtk->pManFunc, pData ); + } + + // (ii) mapped node -> SOP node + else if (Abc_NtkHasMapping( pNtk )) { + if (!pOrigObj->pData) { + // assume terminal... + assert(Abc_ObjFaninNum(pOrigObj) == 1); + + pInitObj = Abc_NtkCreateNodeBuf( pInitNtk, NULL ); + Abc_FlowRetime_ClearInitToOrig( pInitObj ); + return pInitObj; + } + + pInitObj = Abc_NtkCreateObj( pInitNtk, Abc_ObjType(pOrigObj) ); + pData = Mio_GateReadSop(pOrigObj->pData); + assert( Abc_SopGetVarNum(pData) == Abc_ObjFaninNum(pOrigObj) ); + + pInitObj->pData = Abc_SopRegister( pInitNtk->pManFunc, pData ); + } + + // (iii) otherwise, duplicate obj + else { + pInitObj = Abc_NtkDupObj( pInitNtk, pOrigObj, 0 ); + + // copy phase + pInitObj->fPhase = pOrigObj->fPhase; + } + + assert(pInitObj); + return pInitObj; +} + /**Function************************************************************* Synopsis [Updates backward initial state computation problem.] @@ -587,87 +816,43 @@ void Abc_FlowRetime_UpdateBackwardInit( Abc_Ntk_t * pNtk ) { SeeAlso [] ***********************************************************************/ -Abc_Obj_t* Abc_FlowRetime_UpdateBackwardInit_rec( Abc_Obj_t *pOrigObj, - Abc_Obj_t *pUseThisPi, Vec_Ptr_t *vOtherPis, - int fRecurse) { - Abc_Obj_t *pInitObj, *pOrigFanin, *pInitFanin; - void *pData; +Abc_Obj_t* Abc_FlowRetime_UpdateBackwardInit_rec( Abc_Obj_t *pOrigObj) { + Abc_Obj_t *pOrigFanin, *pInitFanin, *pInitObj; int i; - Abc_Ntk_t *pNtk = Abc_ObjNtk( pOrigObj ); + + assert(pOrigObj); // should never reach primary IOs assert(!Abc_ObjIsPi(pOrigObj)); assert(!Abc_ObjIsPo(pOrigObj)); - // if fanin is latch, it becomes a primary input - if (Abc_ObjIsLatch( pOrigObj )) { - if (pOrigObj->fMarkA) return FDATA(pOrigObj)->pInitObj; - - assert(vOtherPis); - - if (pUseThisPi) { - // reuse curent PI - pInitObj = pUseThisPi; } - else { - // reuse previous PI - pInitObj = (Abc_Obj_t*)Vec_PtrPop(vOtherPis); - } - - // remember link from original node to init ntk - Abc_ObjSetData( pOrigObj, pInitObj ); - - pOrigObj->fMarkA = 1; - return (FDATA(pOrigObj)->pInitObj = pInitObj); - } + // skip bias nodes + if (FTEST(pOrigObj, BIAS_NODE)) + return NULL; // does an init node already exist? if(!pOrigObj->fMarkA) { - if (Abc_NtkHasMapping( pNtk )) { - if (!pOrigObj->pData) { - // assume terminal... - assert(Abc_ObjFaninNum(pOrigObj) == 1); - pInitObj = Abc_NtkCreateNodeBuf( pManMR->pInitNtk, NULL ); - } else { - pInitObj = Abc_NtkCreateObj( pManMR->pInitNtk, Abc_ObjType(pOrigObj) ); - pData = Mio_GateReadSop(pOrigObj->pData); - assert( Abc_SopGetVarNum(pData) == Abc_ObjFaninNum(pOrigObj) ); - - pInitObj->pData = Abc_SopRegister( pManMR->pInitNtk->pManFunc, pData ); - } - } else { - pData = Abc_ObjCopy( pOrigObj ); // save ptr to flow data - if (Abc_NtkIsStrash( pNtk ) && Abc_AigNodeIsConst( pOrigObj )) - pInitObj = Abc_AigConst1( pManMR->pInitNtk ); - else - pInitObj = Abc_NtkDupObj( pManMR->pInitNtk, pOrigObj, 0 ); - Abc_ObjSetCopy( pOrigObj, pData ); // restore ptr to flow data - - // copy complementation - pInitObj->fCompl0 = pOrigObj->fCompl0; - pInitObj->fCompl1 = pOrigObj->fCompl1; - pInitObj->fPhase = pOrigObj->fPhase; - } + pInitObj = Abc_FlowRetime_CopyNodeToInitNtk( pOrigObj ); - // if we didn't use given PI, immediately transfer fanouts - // and add to list for later reuse - if (pUseThisPi) { - Abc_ObjBetterTransferFanout( pUseThisPi, pInitObj, 0 ); - Vec_PtrPush( vOtherPis, pUseThisPi ); - } + Abc_FlowRetime_SetInitToOrig( pInitObj, pOrigObj ); + FDATA(pOrigObj)->pInitObj = pInitObj; pOrigObj->fMarkA = 1; - FDATA(pOrigObj)->pInitObj = pInitObj; } else { pInitObj = FDATA(pOrigObj)->pInitObj; } + assert(pInitObj); // have we already connected this object? - if (fRecurse && !pOrigObj->fMarkB) { + if (!pOrigObj->fMarkB) { // create and/or connect fanins Abc_ObjForEachFanin( pOrigObj, pOrigFanin, i ) { - pInitFanin = Abc_FlowRetime_UpdateBackwardInit_rec( pOrigFanin, NULL, NULL, fRecurse ); + // should not reach BOs (i.e. the start of the next frame) + // the new latch bounday should lie before it + assert(!Abc_ObjIsBo( pOrigFanin )); + pInitFanin = Abc_FlowRetime_UpdateBackwardInit_rec( pOrigFanin ); Abc_ObjAddFanin( pInitObj, pInitFanin ); } @@ -745,6 +930,72 @@ void Abc_FlowRetime_VerifyBackwardInit_rec( Abc_Obj_t * pObj ) { Abc_FlowRetime_SimulateNode( pObj ); } +/**Function************************************************************* + + Synopsis [Constrains backward retiming for initializability.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +bool Abc_FlowRetime_PartialSat(Vec_Ptr_t *vNodes, int cut) { + Abc_Ntk_t *pPartNtk, *pInitNtk = pManMR->pInitNtk; + Abc_Obj_t *pObj, *pNext, *pPartObj, *pPartNext, *pPo; + int i, j, result; + + assert( Abc_NtkPoNum( pInitNtk ) == 1 ); + + pPartNtk = Abc_NtkAlloc( pInitNtk->ntkType, pInitNtk->ntkFunc, 0 ); + + // copy network + Vec_PtrForEachEntry( vNodes, pObj, i ) { + pObj->Level = i; + assert(!Abc_ObjIsPo( pObj )); + + if (i < cut && !pObj->fMarkA) { + pPartObj = Abc_NtkCreatePi( pPartNtk ); + Abc_ObjSetCopy( pObj, pPartObj ); + } else { + // copy node + pPartObj = Abc_NtkDupObj( pPartNtk, pObj, 0 ); + // copy complementation + pPartObj->fPhase = pObj->fPhase; + + // connect fanins + Abc_ObjForEachFanin( pObj, pNext, j ) { + pPartNext = Abc_ObjCopy( pNext ); + assert(pPartNext); + Abc_ObjAddFanin( pPartObj, pPartNext ); + } + } + + assert(pObj->pCopy == pPartObj); + } + + // create PO + pPo = Abc_NtkCreatePo( pPartNtk ); + pNext = Abc_ObjFanin0( Abc_NtkPo( pInitNtk, 0 ) ); + pPartNext = Abc_ObjCopy( pNext ); + assert( pPartNext ); + Abc_ObjAddFanin( pPo, pPartNext ); + + // check network +#if defined(DEBUG_CHECK) + Abc_NtkAddDummyPoNames(pPartNtk); + Abc_NtkAddDummyPiNames(pPartNtk); + Abc_NtkCheck( pPartNtk ); +#endif + + result = Abc_NtkMiterSat( pPartNtk, (sint64)500000, (sint64)50000000, 0, NULL, NULL ); + + Abc_NtkDelete( pPartNtk ); + + return !result; +} + /**Function************************************************************* @@ -758,5 +1009,321 @@ void Abc_FlowRetime_VerifyBackwardInit_rec( Abc_Obj_t * pObj ) { ***********************************************************************/ void Abc_FlowRetime_ConstrainInit( ) { - // unimplemented + Vec_Ptr_t *vNodes; + int low, high, mid; + int i, n, lag; + Abc_Obj_t *pObj = NULL, *pOrigObj; + InitConstraint_t *pConstraint = ALLOC( InitConstraint_t, 1 ); + + memset( pConstraint, 0, sizeof(InitConstraint_t) ); + + assert(pManMR->pInitNtk); + + vprintf("\tsearch for initial state conflict...\n"); + + vNodes = Abc_NtkDfs(pManMR->pInitNtk, 0); + n = Vec_PtrSize(vNodes); + // also add PIs to vNodes + Abc_NtkForEachPi(pManMR->pInitNtk, pObj, i) + Vec_PtrPush(vNodes, pObj); + Vec_PtrReorder(vNodes, n); + +#if defined(DEBUG_CHECK) + assert(!Abc_FlowRetime_PartialSat( vNodes, 0 )); +#endif + + // grow initialization constraint + do { + vprintf("\t\t"); + + // find element to add to set... + low = 0, high = Vec_PtrSize(vNodes); + while (low != high-1) { + mid = (low + high) >> 1; + + if (!Abc_FlowRetime_PartialSat( vNodes, mid )) { + low = mid; + vprintf("-"); + } else { + high = mid; + vprintf("*"); + } + fflush(stdout); + } + +#if defined(DEBUG_CHECK) + assert(Abc_FlowRetime_PartialSat( vNodes, high )); + assert(!Abc_FlowRetime_PartialSat( vNodes, low )); +#endif + + // mark its TFO + pObj = Vec_PtrEntry( vNodes, low ); + Abc_NtkMarkCone_rec( pObj, 1 ); + vprintf(" conflict term = %d ", low); + +#if 0 + printf("init ------\n"); + Abc_ObjPrint(stdout, pObj); + printf("\n"); + Abc_ObjPrintNeighborhood( pObj, 1 ); + printf("------\n"); +#endif + + // add node to constraint + Abc_FlowRetime_GetInitToOrig( pObj, &pOrigObj, &lag ); + assert(pOrigObj); + vprintf(" <=> %d/%d\n", Abc_ObjId(pOrigObj), lag); + +#if 0 + printf("orig ------\n"); + Abc_ObjPrint(stdout, pOrigObj); + printf("\n"); + Abc_ObjPrintNeighborhood( pOrigObj, 1 ); + printf("------\n"); +#endif + Vec_IntPush( &pConstraint->vNodes, Abc_ObjId(pOrigObj) ); + Vec_IntPush( &pConstraint->vLags, lag ); + + } while (Abc_FlowRetime_PartialSat( vNodes, Vec_PtrSize(vNodes) )); + + pConstraint->pBiasNode = NULL; + + // add constraint + Vec_PtrPush( pManMR->vInitConstraints, pConstraint ); + + // clear marks + Abc_NtkForEachObj( pManMR->pInitNtk, pObj, i) + pObj->fMarkA = 0; + + // free + Vec_PtrFree( vNodes ); +} + + +/**Function************************************************************* + + Synopsis [Removes nodes to bias against uninitializable cuts.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_FlowRetime_RemoveInitBias( ) { + // Abc_Ntk_t *pNtk = pManMR->pNtk; + Abc_Obj_t *pBiasNode; + InitConstraint_t *pConstraint; + int i; + + Vec_PtrForEachEntry( pManMR->vInitConstraints, pConstraint, i ) { + pBiasNode = pConstraint->pBiasNode; + pConstraint->pBiasNode = NULL; + + if (pBiasNode) + Abc_NtkDeleteObj(pBiasNode); + } +} + + +/**Function************************************************************* + + Synopsis [Connects the bias node to one of the constraint vertices.] + + Description [ACK! + Currently this is dumb dumb hack. + What should we do with biases that belong on BOs? These + move through the circuit. + Currently, the bias gets marked on the fan-in of BO + and the bias gets implemented on every BO fan-out of a + node.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static void Abc_FlowRetime_ConnectBiasNode(Abc_Obj_t *pBiasNode, Abc_Obj_t *pObj, int biasLag) { + Abc_Obj_t *pCur, *pNext; + int i; + int lag; + Vec_Ptr_t *vNodes = Vec_PtrAlloc(1); + Vec_Int_t *vLags = Vec_IntAlloc(1); + Abc_Ntk_t *pNtk = Abc_ObjNtk( pObj ); + + Vec_PtrPush( vNodes, pObj ); + Vec_IntPush( vLags, 0 ); + + Abc_NtkIncrementTravId( pNtk ); + + while (Vec_PtrSize( vNodes )) { + pCur = Vec_PtrPop( vNodes ); + lag = Vec_IntPop( vLags ); + + if (Abc_NodeIsTravIdCurrent( pCur )) continue; + Abc_NodeSetTravIdCurrent( pCur ); + + if (!Abc_ObjIsLatch(pCur) && + !Abc_ObjIsBo(pCur) && + Abc_FlowRetime_GetLag(pObj)+lag == biasLag ) { + + // printf("biasing : "); + // Abc_ObjPrint(stdout, pCur ); +#if 1 + FSET( pCur, BLOCK ); +#else + Abc_ObjAddFanin( pCur, pBiasNode ); +#endif + } + + Abc_ObjForEachFanout( pCur, pNext, i ) { + if (Abc_ObjIsBi(pNext) || + Abc_ObjIsLatch(pNext) || + Abc_ObjIsBo(pNext) || + Abc_ObjIsBo(pCur)) { + Vec_PtrPush( vNodes, pNext ); + Vec_IntPush( vLags, lag - Abc_ObjIsLatch(pNext) ? 1 : 0 ); + } + } + } + + Vec_PtrFree( vNodes ); + Vec_IntFree( vLags ); +} + +/**Function************************************************************* + + Synopsis [Adds nodes to bias against uninitializable cuts.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_FlowRetime_AddInitBias( ) { + Abc_Ntk_t *pNtk = pManMR->pNtk; + Abc_Obj_t *pBiasNode, *pObj, *pNext, *pNext2; + InitConstraint_t *pConstraint; + int i, j, k, l, id; + const int nConstraints = Vec_PtrSize( pManMR->vInitConstraints ); + + pManMR->pDataArray = REALLOC( Flow_Data_t, pManMR->pDataArray, pManMR->nNodes + (nConstraints*(pManMR->iteration+1)) ); + memset(pManMR->pDataArray + pManMR->nNodes, 0, sizeof(Flow_Data_t)*(nConstraints*(pManMR->iteration+1))); + + vprintf("\t\tcreating %d bias structures\n", nConstraints); + + Vec_PtrForEachEntry( pManMR->vInitConstraints, pConstraint, i ) { + if (pConstraint->pBiasNode) continue; + + // printf("\t\t\tbias %d...\n", i); + pBiasNode = Abc_NtkCreateBlackbox( pNtk ); + + Vec_IntForEachEntry( &pConstraint->vNodes, id, j ) { + pObj = Abc_NtkObj(pNtk, id); + Abc_FlowRetime_ConnectBiasNode(pBiasNode, pObj, Vec_IntEntry(&pConstraint->vLags, j)); + } + + // pConstraint->pBiasNode = pBiasNode; + } +} + + +/**Function************************************************************* + + Synopsis [Clears mapping from init node to original node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_FlowRetime_ClearInitToOrig( Abc_Obj_t *pInit ) +{ + int id = Abc_ObjId( pInit ); + + // grow data structure if necessary + if (id >= pManMR->sizeInitToOrig) { + int oldSize = pManMR->sizeInitToOrig; + pManMR->sizeInitToOrig = 1.5*id + 10; + pManMR->pInitToOrig = realloc(pManMR->pInitToOrig, sizeof(NodeLag_t)*pManMR->sizeInitToOrig); + memset( &(pManMR->pInitToOrig[oldSize]), 0, sizeof(NodeLag_t)*(pManMR->sizeInitToOrig-oldSize) ); + } + assert( pManMR->pInitToOrig ); + + pManMR->pInitToOrig[id].id = -1; +} + + +/**Function************************************************************* + + Synopsis [Sets mapping from init node to original node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_FlowRetime_SetInitToOrig( Abc_Obj_t *pInit, Abc_Obj_t *pOrig) +{ + int lag; + int id = Abc_ObjId( pInit ); + + // grow data structure if necessary + if (id >= pManMR->sizeInitToOrig) { + int oldSize = pManMR->sizeInitToOrig; + pManMR->sizeInitToOrig = 1.5*id + 10; + pManMR->pInitToOrig = realloc(pManMR->pInitToOrig, sizeof(NodeLag_t)*pManMR->sizeInitToOrig); + memset( &(pManMR->pInitToOrig[oldSize]), 0, sizeof(NodeLag_t)*(pManMR->sizeInitToOrig-oldSize) ); + } + assert( pManMR->pInitToOrig ); + + // ignore BI, BO, and latch nodes + if (Abc_ObjIsBo(pOrig) || Abc_ObjIsBi(pOrig) || Abc_ObjIsLatch(pOrig)) { + Abc_FlowRetime_ClearInitToOrig(pInit); + return; + } + + // move out of latch boxes + lag = Abc_FlowRetime_ObjFirstNonLatchBox(pOrig, &pOrig); + + pManMR->pInitToOrig[id].id = Abc_ObjId(pOrig); + pManMR->pInitToOrig[id].lag = Abc_FlowRetime_GetLag(pOrig) + lag; +} + + +/**Function************************************************************* + + Synopsis [Gets mapping from init node to original node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_FlowRetime_GetInitToOrig( Abc_Obj_t *pInit, Abc_Obj_t **pOrig, int *lag ) { + + int id = Abc_ObjId( pInit ); + int origId; + + assert(id < pManMR->sizeInitToOrig); + + origId = pManMR->pInitToOrig[id].id; + + if (origId < 0) { + assert(Abc_ObjFaninNum(pInit)); + Abc_FlowRetime_GetInitToOrig( Abc_ObjFanin0(pInit), pOrig, lag); + return; + } + + *pOrig = Abc_NtkObj(pManMR->pNtk, origId); + *lag = pManMR->pInitToOrig[id].lag; } diff --git a/src/opt/fret/fretMain.c b/src/opt/fret/fretMain.c index 780c1f6f..a9ba8c4b 100644 --- a/src/opt/fret/fretMain.c +++ b/src/opt/fret/fretMain.c @@ -28,18 +28,22 @@ static void Abc_FlowRetime_AddDummyFanin( Abc_Obj_t * pObj ); -static void Abc_FlowRetime_MainLoop( ); +static Abc_Ntk_t* Abc_FlowRetime_MainLoop( ); static void Abc_FlowRetime_MarkBlocks( Abc_Ntk_t * pNtk ); static void Abc_FlowRetime_MarkReachable_rec( Abc_Obj_t * pObj, char end ); static int Abc_FlowRetime_ImplementCut( Abc_Ntk_t * pNtk ); static void Abc_FlowRetime_RemoveLatchBubbles( Abc_Obj_t * pLatch ); +static Abc_Ntk_t* Abc_FlowRetime_NtkDup( Abc_Ntk_t * pNtk ); + static void Abc_FlowRetime_VerifyPathLatencies( Abc_Ntk_t * pNtk ); static int Abc_FlowRetime_VerifyPathLatencies_rec( Abc_Obj_t * pObj, int markD ); +static void Abc_FlowRetime_UpdateLags_forw_rec( Abc_Obj_t *pObj ); +static void Abc_FlowRetime_UpdateLags_back_rec( Abc_Obj_t *pObj ); + extern void Abc_NtkMarkCone_rec( Abc_Obj_t * pObj, int fForward ); -extern Abc_Ntk_t * Abc_NtkRestrash( Abc_Ntk_t * pNtk, bool fCleanup ); void print_node3(Abc_Obj_t *pObj); @@ -64,12 +68,14 @@ int fPathError = 0; ***********************************************************************/ Abc_Ntk_t * -Abc_FlowRetime_MinReg( Abc_Ntk_t * pNtk, int fVerbose, int fComputeInitState, +Abc_FlowRetime_MinReg( Abc_Ntk_t * pNtk, int fVerbose, + int fComputeInitState, int fGuaranteeInitState, int fBlockConst, int fForwardOnly, int fBackwardOnly, int nMaxIters, int maxDelay, int fFastButConservative ) { int i; Abc_Obj_t *pObj, *pNext; + InitConstraint_t *pData; // create manager pManMR = ALLOC( MinRegMan_t, 1 ); @@ -77,7 +83,8 @@ Abc_FlowRetime_MinReg( Abc_Ntk_t * pNtk, int fVerbose, int fComputeInitState, pManMR->pNtk = pNtk; pManMR->fVerbose = fVerbose; pManMR->fComputeInitState = fComputeInitState; - pManMR->fGuaranteeInitState = 0; + pManMR->fGuaranteeInitState = fGuaranteeInitState; + pManMR->fBlockConst = fBlockConst; pManMR->fForwardOnly = fForwardOnly; pManMR->fBackwardOnly = fBackwardOnly; pManMR->nMaxIters = nMaxIters; @@ -85,6 +92,10 @@ Abc_FlowRetime_MinReg( Abc_Ntk_t * pNtk, int fVerbose, int fComputeInitState, pManMR->fComputeInitState = fComputeInitState; pManMR->fConservTimingOnly = fFastButConservative; pManMR->vNodes = Vec_PtrAlloc(100); + pManMR->vInitConstraints = Vec_PtrAlloc(2); + pManMR->pInitNtk = NULL; + pManMR->pInitToOrig = NULL; + pManMR->sizeInitToOrig = 0; vprintf("Flow-based minimum-register retiming...\n"); @@ -96,7 +107,7 @@ Abc_FlowRetime_MinReg( Abc_Ntk_t * pNtk, int fVerbose, int fComputeInitState, if (maxDelay) { vprintf("\tmax delay constraint = %d\n", maxDelay); if (maxDelay < (i = Abc_NtkLevel(pNtk))) { - printf("ERROR: max delay constraint must be > current max delay (%d)\n", i); + printf("ERROR: max delay constraint (%d) must be > current max delay (%d)\n", maxDelay, i); return pNtk; } } @@ -151,19 +162,18 @@ Abc_FlowRetime_MinReg( Abc_Ntk_t * pNtk, int fVerbose, int fComputeInitState, if (maxDelay) Abc_FlowRetime_InitTiming( pNtk ); - // create Flow_Data structure + // create lag and Flow_Data structure + pManMR->vLags = Vec_IntStart(pManMR->nNodes); + memset(pManMR->vLags->pArray, 0, sizeof(int)*pManMR->nNodes); + pManMR->pDataArray = ALLOC( Flow_Data_t, pManMR->nNodes ); Abc_FlowRetime_ClearFlows( 1 ); - Abc_NtkForEachObj( pNtk, pObj, i ) - Abc_ObjSetCopy( pObj, (void *)(&pManMR->pDataArray[i]) ); // main loop! - Abc_FlowRetime_MainLoop(); + pNtk = Abc_FlowRetime_MainLoop(); - // clear pCopy field + // cleanup node fields Abc_NtkForEachObj( pNtk, pObj, i ) { - Abc_ObjSetCopy( pObj, NULL ); - // if not computing init state, set all latches to DC if (!fComputeInitState && Abc_ObjIsLatch(pObj)) Abc_LatchSetInitDc(pObj); @@ -171,14 +181,24 @@ Abc_FlowRetime_MinReg( Abc_Ntk_t * pNtk, int fVerbose, int fComputeInitState, // deallocate space FREE( pManMR->pDataArray ); + if (pManMR->pInitToOrig) FREE( pManMR->pInitToOrig ); if (pManMR->vNodes) Vec_PtrFree(pManMR->vNodes); + if (pManMR->vLags) Vec_IntFree(pManMR->vLags); if (pManMR->vSinkDistHist) Vec_IntFree(pManMR->vSinkDistHist); if (pManMR->maxDelay) Abc_FlowRetime_FreeTiming( pNtk ); + while( Vec_PtrSize( pManMR->vInitConstraints )) { + pData = Vec_PtrPop( pManMR->vInitConstraints ); + //assert( pData->pBiasNode ); + //Abc_NtkDeleteObj( pData->pBiasNode ); + FREE( pData->vNodes.pArray ); + FREE( pData ); + } + FREE( pManMR->vInitConstraints ); // restrash if necessary if (Abc_NtkIsStrash(pNtk)) { Abc_NtkReassignIds( pNtk ); - pNtk = Abc_NtkRestrash( pNtk, 1 ); + pNtk = Abc_FlowRetime_NtkSilentRestrash( pNtk, 1 ); } vprintf("\tfinal reg count = %d\n", Abc_NtkLatchNum(pNtk)); @@ -205,10 +225,10 @@ Abc_FlowRetime_MinReg( Abc_Ntk_t * pNtk, int fVerbose, int fComputeInitState, SeeAlso [] ***********************************************************************/ -void +Abc_Ntk_t * Abc_FlowRetime_MainLoop( ) { - Abc_Ntk_t *pNtk = pManMR->pNtk; - // Abc_Obj_t *pObj; int i; + Abc_Ntk_t *pNtk = pManMR->pNtk, *pNtkCopy = pNtk; + Abc_Obj_t *pObj; int i; int last, flow = 0, cut; // (i) forward retiming loop @@ -237,30 +257,20 @@ Abc_FlowRetime_MainLoop( ) { cut = Abc_FlowRetime_ImplementCut( pNtk ); +#if defined (DEBUG_PRINT_LEVELS) vprintf("\t\tlevels = %d\n", Abc_NtkLevel(pNtk)); - -#if 0 - Abc_NtkForEachObj( pNtk, pObj, i ) pObj->Level = 0; - - Abc_NtkLevel(pNtk); - Abc_NtkForEachObj( pNtk, pObj, i ) - if (pObj->Level > pManMR->maxDelay) { - print_node( pObj ); - Vec_PtrForEachEntry( FTIMEEDGES(pObj), p2,j ) { - printf(":%d ", p2->Id); - } - } - Abc_NtkLevelReverse(pNtk); - Abc_NtkForEachObj( pNtk, pObj, i ) - if (pObj->Level > pManMR->maxDelay) { - print_node( pObj ); - } #endif Abc_FlowRetime_ClearFlows( 1 ); pManMR->iteration++; } while( cut != last ); + + // intermediate cleanup (for strashed networks) + if (Abc_NtkIsStrash(pNtk)) { + Abc_NtkReassignIds( pNtk ); + pNtk = pManMR->pNtk = Abc_FlowRetime_NtkSilentRestrash( pNtk, 1 ); + } // print info about initial states if (pManMR->fComputeInitState && pManMR->fVerbose) @@ -268,10 +278,18 @@ Abc_FlowRetime_MainLoop( ) { // (ii) backward retiming loop pManMR->fIsForward = 0; - pManMR->iteration = 0; if (!pManMR->fForwardOnly) do { // initializability loop + pManMR->iteration = 0; + + // copy/restore network + if (pManMR->fGuaranteeInitState) { + if ( pNtk != pNtkCopy ) + Abc_NtkDelete( pNtk ); + pNtk = pManMR->pNtk = Abc_FlowRetime_NtkDup( pNtkCopy ); + vprintf("\trestoring network. regs = %d\n", Abc_NtkLatchNum( pNtk )); + } if (pManMR->fComputeInitState) { Abc_FlowRetime_SetupBackwardInit( pNtk ); @@ -284,8 +302,9 @@ Abc_FlowRetime_MainLoop( ) { vprintf("\tbackward iteration %d\n", pManMR->iteration); last = Abc_NtkLatchNum( pNtk ); + Abc_FlowRetime_AddInitBias( ); Abc_FlowRetime_MarkBlocks( pNtk ); - + if (pManMR->maxDelay) { // timing-constrained loop Abc_FlowRetime_ConstrainConserv( pNtk ); @@ -296,25 +315,13 @@ Abc_FlowRetime_MainLoop( ) { } else { flow = Abc_FlowRetime_PushFlows( pNtk, 1 ); } - + + Abc_FlowRetime_RemoveInitBias( ); cut = Abc_FlowRetime_ImplementCut( pNtk ); +#if defined(DEBUG_PRINT_LEVELS) vprintf("\t\tlevels = %d\n", Abc_NtkLevelReverse(pNtk)); - -#if 0 - Abc_NtkForEachObj( pNtk, pObj, i ) pObj->Level = 0; - - Abc_NtkLevel(pNtk); - Abc_NtkForEachObj( pNtk, pObj, i ) - if (pObj->Level > pManMR->maxDelay) { - print_node( pObj ); - } - Abc_NtkLevelReverse(pNtk); - Abc_NtkForEachObj( pNtk, pObj, i ) - if (pObj->Level > pManMR->maxDelay) { - print_node( pObj ); - } -#endif +#endif Abc_FlowRetime_ClearFlows( 1 ); @@ -328,10 +335,23 @@ Abc_FlowRetime_MainLoop( ) { if (pManMR->fVerbose) Abc_FlowRetime_PrintInitStateInfo( pNtk ); break; } else { - if (!pManMR->fGuaranteeInitState) break; + if (!pManMR->fGuaranteeInitState) { + printf("WARNING: no equivalent init state. setting all initial states to don't-cares\n"); + Abc_NtkForEachLatch( pNtk, pObj, i ) Abc_LatchSetInitDc( pObj ); + break; + } Abc_FlowRetime_ConstrainInit( ); } + + Abc_NtkDelete(pManMR->pInitNtk); + pManMR->pInitNtk = NULL; } while(1); + + assert(!pManMR->fComputeInitState || pManMR->pInitNtk); + if (pManMR->fComputeInitState) Abc_NtkDelete(pManMR->pInitNtk); + if (pManMR->fGuaranteeInitState) ; /* Abc_NtkDelete(pNtkCopy); note: original ntk deleted later */ + + return pNtk; } @@ -369,7 +389,7 @@ Abc_FlowRetime_RemoveLatchBubbles( Abc_Obj_t * pLatch ) { pBi->fCompl0 ^= bubble ^ Abc_ObjFaninC0(pLatch); // convert bubble to INV if not AIG - if (!Abc_NtkHasAig( pNtk ) && Abc_ObjFaninC0(pBi)) { + if (!Abc_NtkIsStrash( pNtk ) && Abc_ObjFaninC0(pBi)) { pBi->fCompl0 = 0; pInv = Abc_NtkCreateNodeInv( pNtk, Abc_ObjFanin0(pBi) ); Abc_ObjPatchFanin( pBi, Abc_ObjFanin0(pBi), pInv ); @@ -397,6 +417,8 @@ Abc_FlowRetime_MarkBlocks( Abc_Ntk_t * pNtk ) { Abc_Obj_t *pObj; if (pManMR->fIsForward){ + // --- forward retiming : block TFO of inputs + // mark the frontier Abc_NtkForEachPo( pNtk, pObj, i ) pObj->fMarkA = 1; @@ -408,6 +430,8 @@ Abc_FlowRetime_MarkBlocks( Abc_Ntk_t * pNtk ) { Abc_NtkForEachPi( pNtk, pObj, i ) Abc_NtkMarkCone_rec( pObj, pManMR->fIsForward ); } else { + // --- backward retiming : block TFI of outputs + // mark the frontier Abc_NtkForEachPi( pNtk, pObj, i ) pObj->fMarkA = 1; @@ -418,6 +442,14 @@ Abc_FlowRetime_MarkBlocks( Abc_Ntk_t * pNtk ) { // mark the nodes reachable from the POs Abc_NtkForEachPo( pNtk, pObj, i ) Abc_NtkMarkCone_rec( pObj, pManMR->fIsForward ); + // block constant nodes (if enabled) + if (pManMR->fBlockConst) { + Abc_NtkForEachObj( pNtk, pObj, i ) + if ((Abc_NtkIsStrash(pNtk) && Abc_AigNodeIsConst(pObj)) || + (!Abc_NtkIsStrash(pNtk) && Abc_NodeIsConst(pObj))) { + FSET(pObj, BLOCK); + } + } } // copy marks @@ -518,7 +550,7 @@ Abc_FlowRetime_FixLatchBoxes( Abc_Ntk_t *pNtk, Vec_Ptr_t *vBoxIns ) { pBi = (Abc_Obj_t *)Vec_PtrPop( vBoxIns ); assert(Abc_ObjIsBi(pBi)); assert(Abc_ObjFanoutNum(pBi) == 1); - assert(Abc_ObjFaninNum(pBi) == 1); + // APH: broken by bias nodes assert(Abc_ObjFaninNum(pBi) == 1); pBo = Abc_ObjFanout0(pBi); assert(!Abc_ObjFaninC0(pBo)); @@ -546,7 +578,12 @@ Abc_FlowRetime_FixLatchBoxes( Abc_Ntk_t *pNtk, Vec_Ptr_t *vBoxIns ) { assert(Abc_ObjFanoutNum(pBi) == 0); assert(Abc_ObjFaninNum(pBo) == 0); assert(Abc_ObjFanoutNum(pBo) == 0); - } else assert(Abc_ObjIsLatch(pBo)); + } else if (Abc_ObjIsLatch(pBo)) { + } else { + Abc_ObjPrint(stdout, pBi); + Abc_ObjPrint(stdout, pBo); + assert(0); + } } // 2. add bi/bos as necessary for latches @@ -803,6 +840,7 @@ Abc_FlowRetime_ImplementCut( Abc_Ntk_t * pNtk ) { // insert latches into netlist Abc_NtkForEachObj( pNtk, pObj, i ) { if (Abc_ObjIsLatch( pObj )) continue; + if (FTEST(pObj, BIAS_NODE)) continue; // a latch is required on every node that lies across the min-cit assert(!pManMR->fIsForward || !FTEST(pObj, VISITED_E) || FTEST(pObj, VISITED_R)); @@ -837,7 +875,7 @@ Abc_FlowRetime_ImplementCut( Abc_Ntk_t * pNtk ) { if (Abc_ObjIsBi(pNext)) assert(Abc_ObjFaninNum(pNext) == 1); } - if (Abc_ObjIsBi(pObj)) assert(Abc_ObjFaninNum(pObj) == 1); + // APH: broken by bias nodes if (Abc_ObjIsBi(pObj)) assert(Abc_ObjFaninNum(pObj) == 1); } } @@ -852,6 +890,7 @@ Abc_FlowRetime_ImplementCut( Abc_Ntk_t * pNtk ) { } // update initial states + Abc_FlowRetime_UpdateLags( ); Abc_FlowRetime_InitState( pNtk ); // restore latch boxes @@ -881,7 +920,7 @@ void Abc_FlowRetime_AddDummyFanin( Abc_Obj_t * pObj ) { Abc_Ntk_t *pNtk = Abc_ObjNtk( pObj ); - if (Abc_NtkHasAig(pNtk)) + if (Abc_NtkIsStrash(pNtk)) Abc_ObjAddFanin(pObj, Abc_AigConst1( pNtk )); else Abc_ObjAddFanin(pObj, Abc_NtkCreateNodeConst0( pNtk )); @@ -1057,3 +1096,281 @@ void Abc_FlowRetime_ClearFlows( bool fClearAll ) { } } } + + +/**Function************************************************************* + + Synopsis [Duplicates network.] + + Description [Duplicates any type of network. Preserves copy data.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static Abc_Ntk_t* Abc_FlowRetime_NtkDup( Abc_Ntk_t * pNtk ) { + Abc_Ntk_t *pNtkCopy; + Abc_Obj_t *pObj, *pObjCopy, *pNext, *pNextCopy; + int i, j; + + pNtkCopy = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc, 1 ); + + // copy each object + Abc_NtkForEachObj( pNtk, pObj, i) { + + if (Abc_NtkIsStrash( pNtk ) && Abc_AigNodeIsConst( pObj )) + pObjCopy = Abc_AigConst1( pNtkCopy ); + else + pObjCopy = Abc_NtkDupObj( pNtkCopy, pObj, 0 ); + + FDATA( pObj )->pCopy = pObjCopy; + FDATA( pObj )->mark = 0; + + // assert( pManMR->fIsForward || pObj->Id == pObjCopy->Id ); + + // copy complementation + pObjCopy->fCompl0 = pObj->fCompl0; + pObjCopy->fCompl1 = pObj->fCompl1; + pObjCopy->fPhase = pObj->fPhase; + } + + // connect fanin + Abc_NtkForEachObj( pNtk, pObj, i) { + pObjCopy = FDATA(pObj)->pCopy; + assert(pObjCopy); + Abc_ObjForEachFanin( pObj, pNext, j ) { + pNextCopy = FDATA(pNext)->pCopy; + assert(pNextCopy); + assert(pNext->Type == pNextCopy->Type); + + Abc_ObjAddFanin(pObjCopy, pNextCopy); + } + } + +#if defined(DEBUG_CHECK) || 1 + Abc_NtkForEachObj( pNtk, pObj, i) { + pObjCopy = FDATA(pObj)->pCopy; + assert( Abc_ObjFanoutNum( pObj ) == Abc_ObjFanoutNum( pObjCopy ) ); + assert( Abc_ObjFaninNum( pObj ) == Abc_ObjFaninNum( pObjCopy ) ); + } +#endif + + assert(Abc_NtkObjNum( pNtk ) == Abc_NtkObjNum( pNtkCopy ) ); + assert(Abc_NtkLatchNum( pNtk ) == Abc_NtkLatchNum( pNtkCopy ) ); + assert(Abc_NtkPoNum( pNtk ) == Abc_NtkPoNum( pNtkCopy ) ); + assert(Abc_NtkPiNum( pNtk ) == Abc_NtkPiNum( pNtkCopy ) ); + + return pNtkCopy; +} + + +/**Function************************************************************* + + Synopsis [Silent restrash.] + + Description [Same functionality as Abc_NtkRestrash but w/o warnings.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_FlowRetime_NtkSilentRestrash( Abc_Ntk_t * pNtk, bool fCleanup ) +{ + Abc_Ntk_t * pNtkAig; + Abc_Obj_t * pObj; + int i, nNodes;//, RetValue; + assert( Abc_NtkIsStrash(pNtk) ); + // start the new network (constants and CIs of the old network will point to the their counterparts in the new network) + pNtkAig = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG ); + // restrash the nodes (assuming a topological order of the old network) + Abc_NtkForEachNode( pNtk, pObj, i ) + pObj->pCopy = Abc_AigAnd( pNtkAig->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) ); + // finalize the network + Abc_NtkFinalize( pNtk, pNtkAig ); + // perform cleanup if requested + if ( fCleanup ) + nNodes = Abc_AigCleanup(pNtkAig->pManFunc); + // duplicate EXDC + if ( pNtk->pExdc ) + pNtkAig->pExdc = Abc_NtkDup( pNtk->pExdc ); + // make sure everything is okay + if ( !Abc_NtkCheck( pNtkAig ) ) + { + printf( "Abc_NtkStrash: The network check has failed.\n" ); + Abc_NtkDelete( pNtkAig ); + return NULL; + } + return pNtkAig; +} + + + +/**Function************************************************************* + + Synopsis [Updates lag values.] + + Description [Recursive. Forward retiming.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void +Abc_FlowRetime_UpdateLags_forw_rec( Abc_Obj_t *pObj ) { + Abc_Obj_t *pNext; + int i; + + assert(!Abc_ObjIsPi(pObj)); + assert(!Abc_ObjIsLatch(pObj)); + + if (Abc_ObjIsBo(pObj)) return; + if (Abc_NodeIsTravIdCurrent(pObj)) return; + + Abc_NodeSetTravIdCurrent(pObj); + + if (Abc_ObjIsNode(pObj)) { + Abc_FlowRetime_SetLag( pObj, -1+Abc_FlowRetime_GetLag(pObj) ); + } + + Abc_ObjForEachFanin( pObj, pNext, i ) { + Abc_FlowRetime_UpdateLags_forw_rec( pNext ); + } +} + + +/**Function************************************************************* + + Synopsis [Updates lag values.] + + Description [Recursive. Backward retiming.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void +Abc_FlowRetime_UpdateLags_back_rec( Abc_Obj_t *pObj ) { + Abc_Obj_t *pNext; + int i; + + assert(!Abc_ObjIsPo(pObj)); + assert(!Abc_ObjIsLatch(pObj)); + + if (Abc_ObjIsBo(pObj)) return; + if (Abc_NodeIsTravIdCurrent(pObj)) return; + + Abc_NodeSetTravIdCurrent(pObj); + + if (Abc_ObjIsNode(pObj)) { + Abc_FlowRetime_SetLag( pObj, 1+Abc_FlowRetime_GetLag(pObj) ); + } + + Abc_ObjForEachFanout( pObj, pNext, i ) { + Abc_FlowRetime_UpdateLags_back_rec( pNext ); + } +} + +/**Function************************************************************* + + Synopsis [Updates lag values.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void +Abc_FlowRetime_UpdateLags( ) { + Abc_Obj_t *pObj, *pNext; + int i, j; + + Abc_NtkIncrementTravId( pManMR->pNtk ); + + Abc_NtkForEachLatch( pManMR->pNtk, pObj, i ) + if (pManMR->fIsForward) { + Abc_ObjForEachFanin( pObj, pNext, j ) + Abc_FlowRetime_UpdateLags_forw_rec( pNext ); + } else { + Abc_ObjForEachFanout( pObj, pNext, j ) + Abc_FlowRetime_UpdateLags_back_rec( pNext ); + } +} + + +/**Function************************************************************* + + Synopsis [Gets lag value of a node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int +Abc_FlowRetime_GetLag( Abc_Obj_t *pObj ) { + assert( !Abc_ObjIsLatch(pObj) ); + assert( Abc_ObjId(pObj) < Vec_IntSize(pManMR->vLags) ); + + return Vec_IntEntry(pManMR->vLags, Abc_ObjId(pObj)); +} + +/**Function************************************************************* + + Synopsis [Sets lag value of a node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void +Abc_FlowRetime_SetLag( Abc_Obj_t *pObj, int lag ) { + assert( Abc_ObjIsNode(pObj) ); + assert( Abc_ObjId(pObj) < Vec_IntSize(pManMR->vLags) ); + + Vec_IntWriteEntry(pManMR->vLags, Abc_ObjId(pObj), lag); +} + + +static void Abc_ObjPrintNeighborhood_rec( Abc_Obj_t *pObj, Vec_Ptr_t *vNodes, int depth ) { + Abc_Obj_t *pObj2; + int i; + + if (pObj->fMarkC || depth < 0) return; + + pObj->fMarkC = 1; + Vec_PtrPush( vNodes, pObj ); + + Abc_ObjPrint( stdout, pObj ); + + Abc_ObjForEachFanout(pObj, pObj2, i) { + Abc_ObjPrintNeighborhood_rec( pObj2, vNodes, depth-1 ); + } + Abc_ObjForEachFanin(pObj, pObj2, i) { + Abc_ObjPrintNeighborhood_rec( pObj2, vNodes, depth-1 ); + } +} + +void Abc_ObjPrintNeighborhood( Abc_Obj_t *pObj, int depth ) { + Vec_Ptr_t *vNodes = Vec_PtrAlloc(100); + Abc_Obj_t *pObj2; + + Abc_ObjPrintNeighborhood_rec( pObj, vNodes, depth ); + + while(Vec_PtrSize(vNodes)) { + pObj2 = Vec_PtrPop(vNodes); + pObj2->fMarkC = 0; + } + + Vec_PtrFree(vNodes); +} diff --git a/src/opt/fret/fretime.h b/src/opt/fret/fretime.h index 167543ce..bbb79d26 100644 --- a/src/opt/fret/fretime.h +++ b/src/opt/fret/fretime.h @@ -27,7 +27,8 @@ // #define DEBUG_PRINT_FLOWS // #define DEBUG_VISITED // #define DEBUG_PREORDER -// #define DEBUG_CHECK +#define DEBUG_CHECK +// #define DEBUG_PRINT_LEVELS //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -36,17 +37,18 @@ #define MAX_DIST 30000 // flags in Flow_Data structure... -#define VISITED_E 0x01 -#define VISITED_R 0x02 +#define VISITED_E 0x001 +#define VISITED_R 0x002 #define VISITED (VISITED_E | VISITED_R) -#define FLOW 0x04 -#define CROSS_BOUNDARY 0x08 -#define BLOCK 0x10 -#define INIT_0 0x20 -#define INIT_1 0x40 +#define FLOW 0x004 +#define CROSS_BOUNDARY 0x008 +#define BLOCK 0x010 +#define INIT_0 0x020 +#define INIT_1 0x040 #define INIT_CARE (INIT_0 | INIT_1) -#define CONSERVATIVE 0x80 +#define CONSERVATIVE 0x080 #define BLOCK_OR_CONS (BLOCK | CONSERVATIVE) +#define BIAS_NODE 0x100 typedef struct Flow_Data_t_ { unsigned int mark : 16; @@ -55,6 +57,7 @@ typedef struct Flow_Data_t_ { Abc_Obj_t *pred; /* unsigned int var; */ Abc_Obj_t *pInitObj; + Abc_Obj_t *pCopy; Vec_Ptr_t *vNodes; }; @@ -63,26 +66,30 @@ typedef struct Flow_Data_t_ { } Flow_Data_t; // useful macros for manipulating Flow_Data structure... -#define FDATA( x ) ((Flow_Data_t *)Abc_ObjCopy(x)) -#define FSET( x, y ) ((Flow_Data_t *)Abc_ObjCopy(x))->mark |= y -#define FUNSET( x, y ) ((Flow_Data_t *)Abc_ObjCopy(x))->mark &= ~y -#define FTEST( x, y ) (((Flow_Data_t *)Abc_ObjCopy(x))->mark & y) +#define FDATA( x ) (pManMR->pDataArray+Abc_ObjId(x)) +#define FSET( x, y ) FDATA(x)->mark |= y +#define FUNSET( x, y ) FDATA(x)->mark &= ~y +#define FTEST( x, y ) (FDATA(x)->mark & y) #define FTIMEEDGES( x ) &(pManMR->vTimeEdges[Abc_ObjId( x )]) -static inline void FSETPRED(Abc_Obj_t *pObj, Abc_Obj_t *pPred) { - assert(!Abc_ObjIsLatch(pObj)); // must preserve field to maintain init state linkage - FDATA(pObj)->pred = pPred; -} -static inline Abc_Obj_t * FGETPRED(Abc_Obj_t *pObj) { - return FDATA(pObj)->pred; -} +typedef struct NodeLag_T_ { + int id; + int lag; +} NodeLag_t; +typedef struct InitConstraint_t_ { + Abc_Obj_t *pBiasNode; + + Vec_Int_t vNodes; + Vec_Int_t vLags; + +} InitConstraint_t; typedef struct MinRegMan_t_ { // problem description: int maxDelay; - bool fComputeInitState, fGuaranteeInitState; + bool fComputeInitState, fGuaranteeInitState, fBlockConst; int nNodes, nLatches; bool fForwardOnly, fBackwardOnly; bool fConservTimingOnly; @@ -99,24 +106,38 @@ typedef struct MinRegMan_t_ { int fSolutionIsDc; int constraintMask; int iteration, subIteration; + Vec_Int_t *vLags; // problem data Vec_Int_t *vSinkDistHist; Flow_Data_t *pDataArray; Vec_Ptr_t *vTimeEdges; Vec_Ptr_t *vExactNodes; + Vec_Ptr_t *vInitConstraints; Abc_Ntk_t *pInitNtk; Vec_Ptr_t *vNodes; // re-useable struct - + + NodeLag_t *pInitToOrig; + int sizeInitToOrig; + } MinRegMan_t ; +extern MinRegMan_t *pManMR; + #define vprintf if (pManMR->fVerbose) printf +static inline void FSETPRED(Abc_Obj_t *pObj, Abc_Obj_t *pPred) { + assert(!Abc_ObjIsLatch(pObj)); // must preserve field to maintain init state linkage + FDATA(pObj)->pred = pPred; +} +static inline Abc_Obj_t * FGETPRED(Abc_Obj_t *pObj) { + return FDATA(pObj)->pred; +} + /*=== fretMain.c ==========================================================*/ - -extern MinRegMan_t *pManMR; -Abc_Ntk_t * Abc_FlowRetime_MinReg( Abc_Ntk_t * pNtk, int fVerbose, int fComputeInitState, +Abc_Ntk_t * Abc_FlowRetime_MinReg( Abc_Ntk_t * pNtk, int fVerbose, + int fComputeInitState, int fGuaranteeInitState, int fBlockConst, int fForward, int fBackward, int nMaxIters, int maxDelay, int fFastButConservative); @@ -128,6 +149,15 @@ int Abc_FlowRetime_PushFlows( Abc_Ntk_t * pNtk, bool fVerbose ); bool Abc_FlowRetime_IsAcrossCut( Abc_Obj_t *pCur, Abc_Obj_t *pNext ); void Abc_FlowRetime_ClearFlows( bool fClearAll ); +int Abc_FlowRetime_GetLag( Abc_Obj_t *pObj ); +void Abc_FlowRetime_SetLag( Abc_Obj_t *pObj, int lag ); + +void Abc_FlowRetime_UpdateLags( ); + +void Abc_ObjPrintNeighborhood( Abc_Obj_t *pObj, int depth ); + +Abc_Ntk_t * Abc_FlowRetime_NtkSilentRestrash( Abc_Ntk_t * pNtk, bool fCleanup ); + /*=== fretFlow.c ==========================================================*/ int dfsplain_e( Abc_Obj_t *pObj, Abc_Obj_t *pPred ); @@ -150,6 +180,8 @@ void Abc_FlowRetime_SetupBackwardInit( Abc_Ntk_t * pNtk ); int Abc_FlowRetime_SolveBackwardInit( Abc_Ntk_t * pNtk ); void Abc_FlowRetime_ConstrainInit( ); +void Abc_FlowRetime_AddInitBias( ); +void Abc_FlowRetime_RemoveInitBias( ); /*=== fretTime.c ==========================================================*/ -- cgit v1.2.3