diff options
Diffstat (limited to 'src/aig')
-rw-r--r-- | src/aig/aig/aig.h | 6 | ||||
-rw-r--r-- | src/aig/aig/aigPart.c | 140 | ||||
-rw-r--r-- | src/aig/aig/aigPartReg.c | 182 | ||||
-rw-r--r-- | src/aig/aig/aigRepr.c | 35 | ||||
-rw-r--r-- | src/aig/aig/aigScl.c | 4 | ||||
-rw-r--r-- | src/aig/aig/aigTsim.c | 78 | ||||
-rw-r--r-- | src/aig/fra/fra.h | 22 | ||||
-rw-r--r-- | src/aig/fra/fraInd.c | 117 | ||||
-rw-r--r-- | src/aig/fra/fraSec.c | 71 |
9 files changed, 518 insertions, 137 deletions
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 @@ -772,6 +772,135 @@ if ( fVerbose ) /**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.] Description [] @@ -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 @@ -40,73 +40,17 @@ 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 [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ 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 ) |