From 7ec48bc20de6209f311715f4b1479cb2e0a4d906 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 20 Apr 2008 20:01:00 -0700 Subject: Version abc80420_2 --- src/aig/ntl/ntl.h | 6 +- src/aig/ntl/ntlEc.c | 2 +- src/aig/ntl/ntlExtract.c | 9 +- src/aig/ntl/ntlFraig.c | 114 ++++++++++++++++--- src/aig/ntl/ntlMan.c | 29 ++++- src/aig/ntl/ntlReadBlif.c | 2 + src/aig/ntl/ntlWriteBlif.c | 21 +++- src/aig/nwk/nwk.h | 2 +- src/aig/nwk/nwkFanio.c | 53 --------- src/aig/nwk/nwkFlow.c | 2 +- src/aig/nwk/nwkMan.c | 131 +++++++++++++++++++--- src/aig/nwk/nwkMap.c | 3 + src/aig/nwk/nwkTiming.c | 2 +- src/aig/saig/saigRetMin.c | 269 +++++++++++++++++++++++++++++++++++++++++---- 14 files changed, 519 insertions(+), 126 deletions(-) (limited to 'src/aig') diff --git a/src/aig/ntl/ntl.h b/src/aig/ntl/ntl.h index fc9d21bc..0ba62bea 100644 --- a/src/aig/ntl/ntl.h +++ b/src/aig/ntl/ntl.h @@ -235,7 +235,7 @@ extern void Ntl_ManPrepareCec( char * pFileName1, char * pFileName2, extern Aig_Man_t * Ntl_ManPrepareSec( char * pFileName1, char * pFileName2 ); /*=== ntlExtract.c ==========================================================*/ extern Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p ); -extern Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p ); +extern Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p, int fSeq ); extern Aig_Man_t * Ntl_ManCollapseForCec( Ntl_Man_t * p ); extern Aig_Man_t * Ntl_ManCollapseForSec( Ntl_Man_t * p1, Ntl_Man_t * p2 ); /*=== ntlInsert.c ==========================================================*/ @@ -247,12 +247,13 @@ extern int Ntl_ManCheck( Ntl_Man_t * pMan ); extern int Ntl_ModelCheck( Ntl_Mod_t * pModel ); extern void Ntl_ModelFixNonDrivenNets( Ntl_Mod_t * pModel ); /*=== ntlMan.c ============================================================*/ -extern Ntl_Man_t * Ntl_ManAlloc( char * pFileName ); +extern Ntl_Man_t * Ntl_ManAlloc(); extern void Ntl_ManCleanup( Ntl_Man_t * p ); extern Ntl_Man_t * Ntl_ManStartFrom( Ntl_Man_t * p ); extern Ntl_Man_t * Ntl_ManDup( Ntl_Man_t * p ); extern void Ntl_ManFree( Ntl_Man_t * p ); extern int Ntl_ManIsComb( Ntl_Man_t * p ); +extern int Ntl_ManLatchNum( Ntl_Man_t * p ); extern Ntl_Mod_t * Ntl_ManFindModel( Ntl_Man_t * p, char * pName ); extern void Ntl_ManPrintStats( Ntl_Man_t * p ); extern Tim_Man_t * Ntl_ManReadTimeMan( Ntl_Man_t * p ); @@ -292,6 +293,7 @@ extern Tim_Man_t * Ntl_ManCreateTiming( Ntl_Man_t * p ); extern Ntl_Man_t * Ioa_ReadBlif( char * pFileName, int fCheck ); /*=== ntlWriteBlif.c ==========================================================*/ extern void Ioa_WriteBlif( Ntl_Man_t * p, char * pFileName ); +extern void Ioa_WriteBlifLogic( Nwk_Man_t * pNtk, Ntl_Man_t * p, char * pFileName ); /*=== ntlUtil.c ==========================================================*/ extern int Ntl_ModelCountLut1( Ntl_Mod_t * pRoot ); extern int Ntl_ManCountSimpleCoDrivers( Ntl_Man_t * p ); diff --git a/src/aig/ntl/ntlEc.c b/src/aig/ntl/ntlEc.c index 7cb6d6f5..0cd75cbc 100644 --- a/src/aig/ntl/ntlEc.c +++ b/src/aig/ntl/ntlEc.c @@ -238,7 +238,7 @@ void Ntl_ManPrepareCec( char * pFileName1, char * pFileName2, Aig_Man_t ** ppMan // derive AIGs *ppMan1 = Ntl_ManCollapseForCec( pMan1 ); *ppMan2 = Ntl_ManCollapseForCec( pMan2 ); - // cleanup + // cleanup Ntl_ManFree( pMan1 ); Ntl_ManFree( pMan2 ); } diff --git a/src/aig/ntl/ntlExtract.c b/src/aig/ntl/ntlExtract.c index 5a681a7e..f278cba8 100644 --- a/src/aig/ntl/ntlExtract.c +++ b/src/aig/ntl/ntlExtract.c @@ -404,7 +404,7 @@ int Ntl_ManCollapse_rec( Ntl_Man_t * p, Ntl_Net_t * pNet ) SeeAlso [] ***********************************************************************/ -Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p ) +Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p, int fSeq ) { Aig_Man_t * pAig; Ntl_Mod_t * pRoot; @@ -443,6 +443,8 @@ Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p ) assert( Ntl_ObjFanoutNum(pObj) == 1 ); pNet = Ntl_ObjFanout0(pObj); pNet->pCopy = Aig_ObjCreatePi( p->pAig ); + if ( fSeq && (pObj->LatchId & 3) == 1 ) + pNet->pCopy = Aig_Not(pNet->pCopy); if ( pNet->nVisits ) { printf( "Ntl_ManCollapse(): Latch output is duplicated or defined as a primary input.\n" ); @@ -470,7 +472,10 @@ Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p ) printf( "Ntl_ManCollapse(): Error: Combinational loop is detected.\n" ); return 0; } - Aig_ObjCreatePo( p->pAig, pNet->pCopy ); + if ( fSeq && (pObj->LatchId & 3) == 1 ) + Aig_ObjCreatePo( p->pAig, Aig_Not(pNet->pCopy) ); + else + Aig_ObjCreatePo( p->pAig, pNet->pCopy ); } // cleanup the AIG Aig_ManCleanup( p->pAig ); diff --git a/src/aig/ntl/ntlFraig.c b/src/aig/ntl/ntlFraig.c index 86d92b3c..767ea6e4 100644 --- a/src/aig/ntl/ntlFraig.c +++ b/src/aig/ntl/ntlFraig.c @@ -179,6 +179,35 @@ void Ntl_ManReduce( Ntl_Man_t * p, Aig_Man_t * pAig ) } } +/**Function************************************************************* + + Synopsis [Resets complemented attributes of the collapsed AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ntl_ManResetComplemented( Ntl_Man_t * p, Aig_Man_t * pAigCol ) +{ + Ntl_Mod_t * pRoot; + Ntl_Obj_t * pObj; + Aig_Obj_t * pObjCol; + int i; + pRoot = Ntl_ManRootModel(p); + Ntl_ModelForEachLatch( pRoot, pObj, i ) + { + if ( (pObj->LatchId & 3) == 1 ) + { + pObjCol = Ntl_ObjFanout0(pObj)->pCopy; + assert( pObjCol->fPhase == 0 ); + pObjCol->fPhase = 1; + } + } +} + /**Function************************************************************* Synopsis [Finalizes the transformation.] @@ -242,14 +271,14 @@ Ntl_Man_t * Ntl_ManFraig( Ntl_Man_t * p, int nPartSize, int nConfLimit, int nLev // collapse the AIG pAig = Ntl_ManExtract( p ); pNew = Ntl_ManInsertAig( p, pAig ); - pAigCol = Ntl_ManCollapse( pNew ); + pAigCol = Ntl_ManCollapse( pNew, 0 ); // perform fraiging for the given design nPartSize = nPartSize? nPartSize : Aig_ManPoNum(pAigCol); pTemp = Aig_ManFraigPartitioned( pAigCol, nPartSize, nConfLimit, nLevelMax, fVerbose ); Aig_ManStop( pTemp ); - // finalize the transformatoin + // finalize the transformation pNew = Ntl_ManFinalize( pAux = pNew, pAig, pAigCol, fVerbose ); Ntl_ManFree( pAux ); Aig_ManStop( pAig ); @@ -273,20 +302,17 @@ Ntl_Man_t * Ntl_ManScl( Ntl_Man_t * p, int fLatchConst, int fLatchEqual, int fVe Ntl_Man_t * pNew, * pAux; Aig_Man_t * pAig, * pAigCol, * pTemp; - // transform the design - Ntl_ManTransformInitValues( p ); - // collapse the AIG pAig = Ntl_ManExtract( p ); pNew = Ntl_ManInsertAig( p, pAig ); - pAigCol = Ntl_ManCollapse( pNew ); + pAigCol = Ntl_ManCollapse( pNew, 1 ); // perform SCL for the given design pAigCol->nRegs = Ntl_ModelLatchNum(Ntl_ManRootModel(p)); pTemp = Aig_ManScl( pAigCol, fLatchConst, fLatchEqual, fVerbose ); Aig_ManStop( pTemp ); - // finalize the transformatoin + // finalize the transformation pNew = Ntl_ManFinalize( pAux = pNew, pAig, pAigCol, fVerbose ); Ntl_ManFree( pAux ); Aig_ManStop( pAig ); @@ -310,20 +336,17 @@ Ntl_Man_t * Ntl_ManLcorr( Ntl_Man_t * p, int nConfMax, int fVerbose ) Ntl_Man_t * pNew, * pAux; Aig_Man_t * pAig, * pAigCol, * pTemp; - // transform the design - Ntl_ManTransformInitValues( p ); - // collapse the AIG pAig = Ntl_ManExtract( p ); pNew = Ntl_ManInsertAig( p, pAig ); - pAigCol = Ntl_ManCollapse( pNew ); + pAigCol = Ntl_ManCollapse( pNew, 1 ); // perform SCL for the given design pAigCol->nRegs = Ntl_ModelLatchNum(Ntl_ManRootModel(p)); pTemp = Fra_FraigLatchCorrespondence( pAigCol, 0, nConfMax, 0, fVerbose, NULL ); Aig_ManStop( pTemp ); - // finalize the transformatoin + // finalize the transformation pNew = Ntl_ManFinalize( pAux = pNew, pAig, pAigCol, fVerbose ); Ntl_ManFree( pAux ); Aig_ManStop( pAig ); @@ -347,20 +370,17 @@ Ntl_Man_t * Ntl_ManSsw( Ntl_Man_t * p, Fra_Ssw_t * pPars ) Ntl_Man_t * pNew, * pAux; Aig_Man_t * pAig, * pAigCol, * pTemp; - // transform the design - Ntl_ManTransformInitValues( p ); - // collapse the AIG pAig = Ntl_ManExtract( p ); pNew = Ntl_ManInsertAig( p, pAig ); - pAigCol = Ntl_ManCollapse( pNew ); + pAigCol = Ntl_ManCollapse( pNew, 1 ); // perform SCL for the given design pAigCol->nRegs = Ntl_ModelLatchNum(Ntl_ManRootModel(p)); pTemp = Fra_FraigInduction( pAigCol, pPars ); Aig_ManStop( pTemp ); - // finalize the transformatoin + // finalize the transformation pNew = Ntl_ManFinalize( pAux = pNew, pAig, pAigCol, pPars->fVerbose ); Ntl_ManFree( pAux ); Aig_ManStop( pAig ); @@ -457,6 +477,63 @@ void Ntl_ManAttachWhiteBoxes( Ntl_Man_t * p, Aig_Man_t * pAigCol, Aig_Man_t * pA printf( "Attached %d boxed (out of %d).\n", Counter, Ntl_ModelBoxNum(pRoot) ); } +/**Function************************************************************* + + Synopsis [Flip complemented edges.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ntl_ManFlipEdges( Ntl_Man_t * p, Aig_Man_t * pAigCol ) +{ + Ntl_Mod_t * pRoot; + Ntl_Obj_t * pObj; + Aig_Obj_t * pObjCol, * pFanin; + int i, iLatch; + pRoot = Ntl_ManRootModel(p); + iLatch = 0; + Ntl_ModelForEachLatch( pRoot, pObj, i ) + { + if ( (pObj->LatchId & 3) == 1 ) + { + pObjCol = Aig_ManPi( pAigCol, Ntl_ModelPiNum(pRoot) + iLatch ); + assert( pObjCol->fMarkA == 0 ); + pObjCol->fMarkA = 1; + } + iLatch++; + } + // flip pointers to the complemented edges + Aig_ManForEachObj( pAigCol, pObjCol, i ) + { + pFanin = Aig_ObjFanin0(pObjCol); + if ( pFanin && pFanin->fMarkA ) + pObjCol->pFanin0 = Aig_Not(pObjCol->pFanin0); + pFanin = Aig_ObjFanin1(pObjCol); + if ( pFanin && pFanin->fMarkA ) + pObjCol->pFanin1 = Aig_Not(pObjCol->pFanin1); + } + // flip complemented latch derivers and undo the marks + iLatch = 0; + Ntl_ModelForEachLatch( pRoot, pObj, i ) + { + if ( (pObj->LatchId & 3) == 1 ) + { + // flip the latch input + pObjCol = Aig_ManPo( pAigCol, Ntl_ModelPoNum(pRoot) + iLatch ); + pObjCol->pFanin0 = Aig_Not(pObjCol->pFanin0); + // unmark the latch output + pObjCol = Aig_ManPi( pAigCol, Ntl_ModelPiNum(pRoot) + iLatch ); + assert( pObjCol->fMarkA == 1 ); + pObjCol->fMarkA = 0; + } + iLatch++; + } +} + /**Function************************************************************* Synopsis [Returns AIG with WB after sequential SAT sweeping.] @@ -473,13 +550,14 @@ Ntl_Man_t * Ntl_ManSsw2( Ntl_Man_t * p, Fra_Ssw_t * pPars ) Ntl_Man_t * pNew; Aig_Man_t * pAigRed, * pAigCol; // collapse the AIG - pAigCol = Ntl_ManCollapse( p ); + pAigCol = Ntl_ManCollapse( p, 1 ); pAigCol->nRegs = Ntl_ModelLatchNum(Ntl_ManRootModel(p)); // transform the collapsed AIG pAigRed = Fra_FraigInduction( pAigCol, pPars ); Aig_ManStop( pAigRed ); pAigRed = Aig_ManDupReprBasic( pAigCol ); // insert the result back + Ntl_ManFlipEdges( p, pAigRed ); Ntl_ManTransferCopy( p ); pNew = Ntl_ManInsertAig( p, pAigRed ); // attach the white-boxes diff --git a/src/aig/ntl/ntlMan.c b/src/aig/ntl/ntlMan.c index b4b63905..e80e02c6 100644 --- a/src/aig/ntl/ntlMan.c +++ b/src/aig/ntl/ntlMan.c @@ -39,7 +39,7 @@ SeeAlso [] ***********************************************************************/ -Ntl_Man_t * Ntl_ManAlloc( char * pFileName ) +Ntl_Man_t * Ntl_ManAlloc() { Ntl_Man_t * p; // start the manager @@ -53,9 +53,6 @@ Ntl_Man_t * Ntl_ManAlloc( char * pFileName ) // start the manager p->pMemObjs = Aig_MmFlexStart(); p->pMemSops = Aig_MmFlexStart(); - // same the names - p->pName = Ntl_ManStoreFileName( p, pFileName ); - p->pSpec = Ntl_ManStoreName( p, pFileName ); return p; } @@ -106,7 +103,9 @@ Ntl_Man_t * Ntl_ManStartFrom( Ntl_Man_t * pOld ) Ntl_Obj_t * pBox; Ntl_Net_t * pNet; int i, k; - pNew = Ntl_ManAlloc( pOld->pSpec ); + pNew = Ntl_ManAlloc(); + pNew->pName = Ntl_ManStoreFileName( pNew, pOld->pName ); + pNew->pSpec = Ntl_ManStoreName( pNew, pOld->pName ); Vec_PtrForEachEntry( pOld->vModels, pModel, i ) if ( i == 0 ) { @@ -146,7 +145,9 @@ Ntl_Man_t * Ntl_ManDup( Ntl_Man_t * pOld ) Ntl_Obj_t * pBox; Ntl_Net_t * pNet; int i, k; - pNew = Ntl_ManAlloc( pOld->pSpec ); + pNew = Ntl_ManAlloc(); + pNew->pName = Ntl_ManStoreFileName( pNew, pOld->pName ); + pNew->pSpec = Ntl_ManStoreName( pNew, pOld->pName ); Vec_PtrForEachEntry( pOld->vModels, pModel, i ) pModel->pCopy = Ntl_ModelDup( pNew, pModel ); Vec_PtrForEachEntry( pOld->vModels, pModel, i ) @@ -211,6 +212,22 @@ int Ntl_ManIsComb( Ntl_Man_t * p ) return Ntl_ModelLatchNum(Ntl_ManRootModel(p)) == 0; } +/**Function************************************************************* + + Synopsis [Returns the number of registers.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ntl_ManLatchNum( Ntl_Man_t * p ) +{ + return Ntl_ModelLatchNum(Ntl_ManRootModel(p)); +} + /**Function************************************************************* Synopsis [Find the model with the given name.] diff --git a/src/aig/ntl/ntlReadBlif.c b/src/aig/ntl/ntlReadBlif.c index 23bb6d76..13050047 100644 --- a/src/aig/ntl/ntlReadBlif.c +++ b/src/aig/ntl/ntlReadBlif.c @@ -131,6 +131,8 @@ Ntl_Man_t * Ioa_ReadBlif( char * pFileName, int fCheck ) } // set the design name p->pDesign = Ntl_ManAlloc( pFileName ); + p->pDesign->pName = Ntl_ManStoreFileName( p->pDesign, pFileName ); + p->pDesign->pSpec = Ntl_ManStoreName( p->pDesign, pFileName ); // prepare the file for parsing Ioa_ReadReadPreparse( p ); // parse interfaces of each network diff --git a/src/aig/ntl/ntlWriteBlif.c b/src/aig/ntl/ntlWriteBlif.c index 24fa1370..ed45fcaf 100644 --- a/src/aig/ntl/ntlWriteBlif.c +++ b/src/aig/ntl/ntlWriteBlif.c @@ -141,7 +141,7 @@ void Ioa_WriteBlifModel( FILE * pFile, Ntl_Mod_t * pModel ) /**Function************************************************************* - Synopsis [Writes the network into the BLIF file.] + Synopsis [Writes the netlist into the BLIF file.] Description [] @@ -170,6 +170,25 @@ void Ioa_WriteBlif( Ntl_Man_t * p, char * pFileName ) fclose( pFile ); } +/**Function************************************************************* + + Synopsis [Writes the logic network into the BLIF file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ioa_WriteBlifLogic( Nwk_Man_t * pNtk, Ntl_Man_t * p, char * pFileName ) +{ + Ntl_Man_t * pNew; + pNew = Ntl_ManInsertNtk( p, pNtk ); + Ioa_WriteBlif( pNew, pFileName ); + Ntl_ManFree( pNew ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/nwk/nwk.h b/src/aig/nwk/nwk.h index d0a871cf..c36f3498 100644 --- a/src/aig/nwk/nwk.h +++ b/src/aig/nwk/nwk.h @@ -250,7 +250,7 @@ extern Vec_Ptr_t * Nwk_ManRetimeCutBackward( Nwk_Man_t * pMan, int nLatches, /*=== nwkMan.c ============================================================*/ extern Nwk_Man_t * Nwk_ManAlloc(); extern void Nwk_ManFree( Nwk_Man_t * p ); -extern void Nwk_ManPrintStats( Nwk_Man_t * p, If_Lib_t * pLutLib ); +extern void Nwk_ManPrintStats( Nwk_Man_t * p, If_Lib_t * pLutLib, int fSaveBest, int fDumpResult, void * pNtl ); /*=== nwkMap.c ============================================================*/ extern Nwk_Man_t * Nwk_MappingIf( Aig_Man_t * p, Tim_Man_t * pManTime, If_Par_t * pPars ); /*=== nwkObj.c ============================================================*/ diff --git a/src/aig/nwk/nwkFanio.c b/src/aig/nwk/nwkFanio.c index 1b701e9e..89bf60ee 100644 --- a/src/aig/nwk/nwkFanio.c +++ b/src/aig/nwk/nwkFanio.c @@ -125,58 +125,6 @@ static inline int Nwk_ObjReallocIsNeeded( Nwk_Obj_t * pObj ) { return pObj->nFanins + pObj->nFanouts == pObj->nFanioAlloc; } - -/**Function************************************************************* - - Synopsis [Reallocates the object.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static Nwk_Obj_t * Nwk_ManReallocNode_old( Nwk_Obj_t * pObj ) -{ - Nwk_Obj_t * pObjNew, * pTemp; - int i, iNum; - assert( Nwk_ObjReallocIsNeeded(pObj) ); - pObjNew = (Nwk_Obj_t *)Aig_MmFlexEntryFetch( pObj->pMan->pMemObjs, sizeof(Nwk_Obj_t) + 2 * pObj->nFanioAlloc * sizeof(Nwk_Obj_t *) ); - memmove( pObjNew, pObj, sizeof(Nwk_Obj_t) + pObj->nFanioAlloc * sizeof(Nwk_Obj_t *) ); - pObjNew->nFanioAlloc = 2 * pObj->nFanioAlloc; - // update the fanouts' fanins - Nwk_ObjForEachFanout( pObj, pTemp, i ) - { - iNum = Nwk_ObjFindFanin( pTemp, pObj ); - if ( iNum == -1 ) - printf( "Nwk_ManReallocNode(): Error! Fanin cannot be found.\n" ); - pTemp->pFanio[iNum] = pObjNew; - } - // update the fanins' fanouts - Nwk_ObjForEachFanin( pObj, pTemp, i ) - { - iNum = Nwk_ObjFindFanout( pTemp, pObj ); - if ( iNum == -1 ) - printf( "Nwk_ManReallocNode(): Error! Fanout cannot be found.\n" ); - pTemp->pFanio[pTemp->nFanins+iNum] = pObjNew; - } - memset( pObj, 0, sizeof(Nwk_Obj_t) + pObj->nFanioAlloc * sizeof(Nwk_Obj_t *) ); - assert( Nwk_ManObj(pObjNew->pMan, pObjNew->Id) == pObj ); - Vec_PtrWriteEntry( pObjNew->pMan->vObjs, pObjNew->Id, pObjNew ); - if ( Nwk_ObjIsCi(pObjNew) ) - { - assert( Nwk_ManCi(pObjNew->pMan, pObjNew->PioId) == pObj ); - Vec_PtrWriteEntry( pObjNew->pMan->vCis, pObjNew->PioId, pObjNew ); - } - if ( Nwk_ObjIsCo(pObjNew) ) - { - assert( Nwk_ManCo(pObjNew->pMan, pObjNew->PioId) == pObj ); - Vec_PtrWriteEntry( pObjNew->pMan->vCos, pObjNew->PioId, pObjNew ); - } - pObjNew->pMan->nRealloced++; - return pObjNew; -} /**Function************************************************************* @@ -200,7 +148,6 @@ static Nwk_Obj_t * Nwk_ManReallocNode( Nwk_Obj_t * pObj ) return NULL; } - /**Function************************************************************* Synopsis [Creates fanout/fanin relationship between the nodes.] diff --git a/src/aig/nwk/nwkFlow.c b/src/aig/nwk/nwkFlow.c index b245628a..3a7e6df6 100644 --- a/src/aig/nwk/nwkFlow.c +++ b/src/aig/nwk/nwkFlow.c @@ -524,7 +524,7 @@ Vec_Ptr_t * Nwk_ManRetimeCutBackward( Nwk_Man_t * pMan, int nLatches, int fVerbo pObj->MarkA = 1; Nwk_ManForEachPoSeq( pMan, pObj, i ) Nwk_ManMarkTfiCone_rec( pObj ); - Nwk_ManForEachObj( pMan, pObj, i ) + Nwk_ManForEachNode( pMan, pObj, i ) if ( Nwk_ObjFaninNum(pObj) == 0 ) pObj->MarkA = 1; // start flow computation from each LI driver diff --git a/src/aig/nwk/nwkMan.c b/src/aig/nwk/nwkMan.c index a1f20a8e..aeebac3f 100644 --- a/src/aig/nwk/nwkMan.c +++ b/src/aig/nwk/nwkMan.c @@ -102,6 +102,92 @@ void Nwk_ManPrintLutSizes( Nwk_Man_t * p, If_Lib_t * pLutLib ) printf( "%d:%d ", i, Counters[i] ); } +/**Function************************************************************* + + Synopsis [If the network is best, saves it in "best.blif" and returns 1.] + + Description [If the networks are incomparable, saves the new network, + returns its parameters in the internal parameter structure, and returns 1. + If the new network is not a logic network, quits without saving and returns 0.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Nwk_ManCompareAndSaveBest( Nwk_Man_t * pNtk, void * pNtl ) +{ + extern void Ioa_WriteBlifLogic( Nwk_Man_t * pNtk, void * pNtl, char * pFileName ); + static struct ParStruct { + char * pName; // name of the best saved network + int Depth; // depth of the best saved network + int Flops; // flops in the best saved network + int Nodes; // nodes in the best saved network + int nPis; // the number of primary inputs + int nPos; // the number of primary outputs + } ParsNew, ParsBest = { 0 }; + // free storage for the name + if ( pNtk == NULL ) + { + FREE( ParsBest.pName ); + return 0; + } + // get the parameters + ParsNew.Depth = Nwk_ManLevel( pNtk ); + ParsNew.Flops = Nwk_ManLatchNum( pNtk ); + ParsNew.Nodes = Nwk_ManNodeNum( pNtk ); + ParsNew.nPis = Nwk_ManPiNum( pNtk ); + ParsNew.nPos = Nwk_ManPoNum( pNtk ); + // reset the parameters if the network has the same name + if ( ParsBest.pName == NULL || + strcmp(ParsBest.pName, pNtk->pName) || + ParsBest.Depth > ParsNew.Depth || + ParsBest.Depth == ParsNew.Depth && ParsBest.Flops > ParsNew.Flops || + ParsBest.Depth == ParsNew.Depth && ParsBest.Flops == ParsNew.Flops && ParsBest.Nodes > ParsNew.Nodes ) + { + FREE( ParsBest.pName ); + ParsBest.pName = Aig_UtilStrsav( pNtk->pName ); + ParsBest.Depth = ParsNew.Depth; + ParsBest.Flops = ParsNew.Flops; + ParsBest.Nodes = ParsNew.Nodes; + ParsBest.nPis = ParsNew.nPis; + ParsBest.nPos = ParsNew.nPos; + // writ the network + Ioa_WriteBlifLogic( pNtk, pNtl, "best.blif" ); + return 1; + } + return 0; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +char * Nwk_FileNameGeneric( char * FileName ) +{ + char * pDot; + char * pUnd; + char * pRes; + // find the generic name of the file + pRes = Aig_UtilStrsav( FileName ); + // find the pointer to the "." symbol in the file name +// pUnd = strstr( FileName, "_" ); + pUnd = NULL; + pDot = strstr( FileName, "." ); + if ( pUnd ) + pRes[pUnd - FileName] = 0; + else if ( pDot ) + pRes[pDot - FileName] = 0; + return pRes; +} + /**Function************************************************************* Synopsis [Prints stats of the manager.] @@ -113,24 +199,37 @@ void Nwk_ManPrintLutSizes( Nwk_Man_t * p, If_Lib_t * pLutLib ) SeeAlso [] ***********************************************************************/ -void Nwk_ManPrintStats( Nwk_Man_t * p, If_Lib_t * pLutLib ) +void Nwk_ManPrintStats( Nwk_Man_t * pNtk, If_Lib_t * pLutLib, int fSaveBest, int fDumpResult, void * pNtl ) { - p->pLutLib = pLutLib; - printf( "%-15s : ", p->pName ); - printf( "pi = %5d ", Nwk_ManPiNum(p) ); - printf( "po = %5d ", Nwk_ManPoNum(p) ); - printf( "ci = %5d ", Nwk_ManCiNum(p) ); - printf( "co = %5d ", Nwk_ManCoNum(p) ); - printf( "lat = %5d ", Nwk_ManLatchNum(p) ); - printf( "node = %5d ", Nwk_ManNodeNum(p) ); - printf( "edge = %5d ", Nwk_ManGetTotalFanins(p) ); - printf( "aig = %6d ", Nwk_ManGetAigNodeNum(p) ); - printf( "lev = %3d ", Nwk_ManLevel(p) ); -// printf( "lev2 = %3d ", Nwk_ManLevelBackup(p) ); - printf( "delay = %5.2f ", Nwk_ManDelayTraceLut(p) ); - Nwk_ManPrintLutSizes( p, pLutLib ); + extern int Ntl_ManLatchNum( void * p ); + extern void Ioa_WriteBlifLogic( Nwk_Man_t * pNtk, void * pNtl, char * pFileName ); + if ( fSaveBest ) + Nwk_ManCompareAndSaveBest( pNtk, pNtl ); + if ( fDumpResult ) + { + char Buffer[1000] = {0}; + char * pNameGen = pNtk->pSpec? Nwk_FileNameGeneric( pNtk->pSpec ) : "nameless_"; + sprintf( Buffer, "%s_dump.blif", pNameGen ); + Ioa_WriteBlifLogic( pNtk, pNtl, Buffer ); + if ( pNtk->pSpec ) free( pNameGen ); + } + + pNtk->pLutLib = pLutLib; + printf( "%-15s : ", pNtk->pName ); + printf( "pi = %5d ", Nwk_ManPiNum(pNtk) ); + printf( "po = %5d ", Nwk_ManPoNum(pNtk) ); + printf( "ci = %5d ", Nwk_ManCiNum(pNtk) ); + printf( "co = %5d ", Nwk_ManCoNum(pNtk) ); + printf( "lat = %5d ", Ntl_ManLatchNum(pNtl) ); + printf( "node = %5d ", Nwk_ManNodeNum(pNtk) ); + printf( "edge = %5d ", Nwk_ManGetTotalFanins(pNtk) ); + printf( "aig = %6d ", Nwk_ManGetAigNodeNum(pNtk) ); + printf( "lev = %3d ", Nwk_ManLevel(pNtk) ); +// printf( "lev2 = %3d ", Nwk_ManLevelBackup(pNtk) ); + printf( "delay = %5.2f ", Nwk_ManDelayTraceLut(pNtk) ); + Nwk_ManPrintLutSizes( pNtk, pLutLib ); printf( "\n" ); -// Nwk_ManDelayTracePrint( p, pLutLib ); +// Nwk_ManDelayTracePrint( pNtk, pLutLib ); fflush( stdout ); } diff --git a/src/aig/nwk/nwkMap.c b/src/aig/nwk/nwkMap.c index effffcf7..45d56eb5 100644 --- a/src/aig/nwk/nwkMap.c +++ b/src/aig/nwk/nwkMap.c @@ -267,6 +267,9 @@ Nwk_Man_t * Nwk_ManFromIf( If_Man_t * pIfMan, Aig_Man_t * p, Vec_Ptr_t * vAigToI pNtk = Nwk_ManAlloc(); pNtk->pName = Aig_UtilStrsav( p->pName ); pNtk->pSpec = Aig_UtilStrsav( p->pSpec ); +// pNtk->nLatches = Aig_ManRegNum(p); +// pNtk->nTruePis = Nwk_ManCiNum(pNtk) - pNtk->nLatches; +// pNtk->nTruePos = Nwk_ManCoNum(pNtk) - pNtk->nLatches; Aig_ManForEachObj( p, pObj, i ) { pIfObj = Vec_PtrEntry( vAigToIf, i ); diff --git a/src/aig/nwk/nwkTiming.c b/src/aig/nwk/nwkTiming.c index 9ab24467..e8123dae 100644 --- a/src/aig/nwk/nwkTiming.c +++ b/src/aig/nwk/nwkTiming.c @@ -427,7 +427,7 @@ int Nwk_ManVerifyTiming( Nwk_Man_t * pNtk ) int i; Nwk_ManForEachObj( pNtk, pObj, i ) { - if ( Nwk_ObjIsPi(pObj) && Nwk_ObjFanoutNum(pObj) == 0 ) + if ( Nwk_ObjIsCi(pObj) && Nwk_ObjFanoutNum(pObj) == 0 ) continue; tArrival = Nwk_NodeComputeArrival( pObj, 1 ); tRequired = Nwk_NodeComputeRequired( pObj, 1 ); diff --git a/src/aig/saig/saigRetMin.c b/src/aig/saig/saigRetMin.c index 92d39ab6..3adb76c6 100644 --- a/src/aig/saig/saigRetMin.c +++ b/src/aig/saig/saigRetMin.c @@ -19,6 +19,8 @@ ***********************************************************************/ #include "saig.h" +#include "satSolver.h" +#include "cnf.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -54,7 +56,7 @@ void Saig_ManMarkCone_rec( Aig_Man_t * p, Aig_Obj_t * pObj ) /**Function************************************************************* - Synopsis [Marks the TFI cones with the current traversal ID.] + Synopsis [Counts the number of nodes to get registers after retiming.] Description [] @@ -63,18 +65,44 @@ void Saig_ManMarkCone_rec( Aig_Man_t * p, Aig_Obj_t * pObj ) SeeAlso [] ***********************************************************************/ -void Saig_ManMarkCones( Aig_Man_t * p, Vec_Ptr_t * vNodes ) +int Saig_ManRetimeCountCut( Aig_Man_t * p, Vec_Ptr_t * vCut ) { - Aig_Obj_t * pObj; - int i; + Vec_Ptr_t * vNodes; + Aig_Obj_t * pObj, * pFanin; + int i, RetValue; + // mark the cones Aig_ManIncrementTravId( p ); - Vec_PtrForEachEntry( vNodes, pObj, i ) + Vec_PtrForEachEntry( vCut, pObj, i ) Saig_ManMarkCone_rec( p, pObj ); + // collect the new cut + vNodes = Vec_PtrAlloc( 1000 ); + Aig_ManForEachObj( p, pObj, i ) + { + if ( Aig_ObjIsTravIdCurrent(p, pObj) ) + continue; + pFanin = Aig_ObjFanin0( pObj ); + if ( pFanin && !pFanin->fMarkA && Aig_ObjIsTravIdCurrent(p, pFanin) ) + { + Vec_PtrPush( vNodes, pFanin ); + pFanin->fMarkA = 1; + } + pFanin = Aig_ObjFanin1( pObj ); + if ( pFanin && !pFanin->fMarkA && Aig_ObjIsTravIdCurrent(p, pFanin) ) + { + Vec_PtrPush( vNodes, pFanin ); + pFanin->fMarkA = 1; + } + } + Vec_PtrForEachEntry( vNodes, pObj, i ) + pObj->fMarkA = 0; + RetValue = Vec_PtrSize( vNodes ); + Vec_PtrFree( vNodes ); + return RetValue; } /**Function************************************************************* - Synopsis [Counts the number of nodes to get registers after retiming.] + Synopsis [Computes the new cut after excluding the nodes in the set.] Description [] @@ -83,12 +111,18 @@ void Saig_ManMarkCones( Aig_Man_t * p, Vec_Ptr_t * vNodes ) SeeAlso [] ***********************************************************************/ -int Saig_ManRetimeCountCut( Aig_Man_t * p, Vec_Ptr_t * vCut ) +Vec_Ptr_t * Saig_ManRetimeExtendCut( Aig_Man_t * p, Vec_Ptr_t * vCut, Vec_Ptr_t * vToExclude ) { Vec_Ptr_t * vNodes; Aig_Obj_t * pObj, * pFanin; - int i, RetValue; - Saig_ManMarkCones( p, vCut ); + int i; + // mark the cones + Aig_ManIncrementTravId( p ); + Vec_PtrForEachEntry( vCut, pObj, i ) + Saig_ManMarkCone_rec( p, pObj ); + Vec_PtrForEachEntry( vToExclude, pObj, i ) + Saig_ManMarkCone_rec( p, pObj ); + // collect the new cut vNodes = Vec_PtrAlloc( 1000 ); Aig_ManForEachObj( p, pObj, i ) { @@ -107,16 +141,14 @@ int Saig_ManRetimeCountCut( Aig_Man_t * p, Vec_Ptr_t * vCut ) pFanin->fMarkA = 1; } } - RetValue = Vec_PtrSize( vNodes ); Vec_PtrForEachEntry( vNodes, pObj, i ) pObj->fMarkA = 0; - Vec_PtrFree( vNodes ); - return RetValue; + return vNodes; } /**Function************************************************************* - Synopsis [Duplicates the AIG while retiming the registers to the cut.] + Synopsis [Duplicates the AIG recursively.] Description [] @@ -125,13 +157,13 @@ int Saig_ManRetimeCountCut( Aig_Man_t * p, Vec_Ptr_t * vCut ) SeeAlso [] ***********************************************************************/ -void Saig_ManRetimeDupForward_rec( Aig_Man_t * pNew, Aig_Obj_t * pObj ) +void Saig_ManRetimeDup_rec( Aig_Man_t * pNew, Aig_Obj_t * pObj ) { if ( pObj->pData ) return; assert( Aig_ObjIsNode(pObj) ); - Saig_ManRetimeDupForward_rec( pNew, Aig_ObjFanin0(pObj) ); - Saig_ManRetimeDupForward_rec( pNew, Aig_ObjFanin1(pObj) ); + Saig_ManRetimeDup_rec( pNew, Aig_ObjFanin0(pObj) ); + Saig_ManRetimeDup_rec( pNew, Aig_ObjFanin1(pObj) ); pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); } @@ -168,9 +200,9 @@ Aig_Man_t * Saig_ManRetimeDupForward( Aig_Man_t * p, Vec_Ptr_t * vCut ) // create the registers Vec_PtrForEachEntry( vCut, pObj, i ) pObj->pData = Aig_NotCond( Aig_ObjCreatePi(pNew), pObj->fPhase ); - // duplicate the logic above the cut + // duplicate logic above the cut Aig_ManForEachPo( p, pObj, i ) - Saig_ManRetimeDupForward_rec( pNew, Aig_ObjFanin0(pObj) ); + Saig_ManRetimeDup_rec( pNew, Aig_ObjFanin0(pObj) ); // create the true POs Saig_ManForEachPo( p, pObj, i ) Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); @@ -182,12 +214,12 @@ Aig_Man_t * Saig_ManRetimeDupForward( Aig_Man_t * p, Vec_Ptr_t * vCut ) pObjLo->pData = pObjLi->pData; // erase the data values on the internal nodes of the cut Vec_PtrForEachEntry( vCut, pObj, i ) - if ( !Aig_ObjIsPi(pObj) ) + if ( Aig_ObjIsNode(pObj) ) pObj->pData = NULL; - // duplicate the logic below the cut + // duplicate logic below the cut Vec_PtrForEachEntry( vCut, pObj, i ) { - Saig_ManRetimeDupForward_rec( pNew, pObj ); + Saig_ManRetimeDup_rec( pNew, pObj ); Aig_ObjCreatePo( pNew, Aig_NotCond(pObj->pData, pObj->fPhase) ); } return pNew; @@ -195,7 +227,7 @@ Aig_Man_t * Saig_ManRetimeDupForward( Aig_Man_t * p, Vec_Ptr_t * vCut ) /**Function************************************************************* - Synopsis [Duplicates the AIG while retiming the registers to the cut.] + Synopsis [Derives AIG for the initial state computation.] Description [] @@ -204,10 +236,199 @@ Aig_Man_t * Saig_ManRetimeDupForward( Aig_Man_t * p, Vec_Ptr_t * vCut ) SeeAlso [] ***********************************************************************/ -Aig_Man_t * Saig_ManRetimeDupBackward( Aig_Man_t * p, Vec_Ptr_t * vCut ) +Aig_Man_t * Saig_ManRetimeDupInitState( Aig_Man_t * p, Vec_Ptr_t * vCut ) { Aig_Man_t * pNew; - pNew = Aig_ManDup( p ); + Aig_Obj_t * pObj; + int i; + // mark the cones under the cut +// assert( Vec_PtrSize(vCut) == Saig_ManRetimeCountCut(p, vCut) ); + // create the new manager + pNew = Aig_ManStart( Aig_ManObjNumMax(p) ); + // create the true PIs + Aig_ManCleanData( p ); + Aig_ManConst1(p)->pData = Aig_ManConst1(pNew); + // create the registers + Vec_PtrForEachEntry( vCut, pObj, i ) + pObj->pData = Aig_ObjCreatePi(pNew); + // duplicate logic above the cut and create POs + Saig_ManForEachLi( p, pObj, i ) + { + Saig_ManRetimeDup_rec( pNew, Aig_ObjFanin0(pObj) ); + Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); + } + return pNew; +} + +/**Function************************************************************* + + Synopsis [Derives the initial state after backward retiming.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Saig_ManRetimeFindInitState( Aig_Man_t * p ) +{ + int nConfLimit = 1000000; + Vec_Int_t * vCiIds, * vInit = NULL; + Cnf_Dat_t * pCnf; + sat_solver * pSat; + Aig_Obj_t * pObj; + int i, RetValue, * pAssumps, * pModel; + // solve the SAT problem + pCnf = Cnf_DeriveSimple( p, Aig_ManPoNum(p) ); + pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); + pAssumps = ALLOC( int, Aig_ManPoNum(p) ); + Aig_ManForEachPo( p, pObj, i ) + pAssumps[i] = toLitCond( pCnf->pVarNums[pObj->Id], 1 ); + RetValue = sat_solver_solve( pSat, pAssumps, pAssumps+Aig_ManPoNum(p), (sint64)nConfLimit, (sint64)0, (sint64)0, (sint64)0 ); + free( pAssumps ); + if ( RetValue == l_True ) + { + // accumulate SAT variables of the CIs + vCiIds = Vec_IntAlloc( Aig_ManPiNum(p) ); + Aig_ManForEachPi( p, pObj, i ) + Vec_IntPush( vCiIds, pCnf->pVarNums[pObj->Id] ); + // create the model + pModel = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize ); + vInit = Vec_IntAllocArray( pModel, Aig_ManPiNum(p) ); + Vec_IntFree( vCiIds ); + } + sat_solver_delete( pSat ); + Cnf_DataFree( pCnf ); + return vInit; +} + +/**Function************************************************************* + + Synopsis [Returns the array of bad registers.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Saig_ManGetRegistersToExclude( Aig_Man_t * p ) +{ + Vec_Ptr_t * vNodes = NULL; + Aig_Obj_t * pObj, * pFanin; + int i, Diffs; + assert( Saig_ManRegNum(p) > 0 ); + Saig_ManForEachLi( p, pObj, i ) + { + pFanin = Aig_ObjFanin0(pObj); + if ( !Aig_ObjFaninC0(pObj) ) + pFanin->fMarkA = 1; + else + pFanin->fMarkB = 1; + } + Diffs = 0; + Saig_ManForEachLi( p, pObj, i ) + { + pFanin = Aig_ObjFanin0(pObj); + Diffs += pFanin->fMarkA && pFanin->fMarkB; + } + if ( Diffs > 0 ) + vNodes = Vec_PtrAlloc( Diffs ); + Saig_ManForEachLi( p, pObj, i ) + { + pFanin = Aig_ObjFanin0(pObj); + if ( vNodes && pFanin->fMarkA && pFanin->fMarkB ) + Vec_PtrPush( vNodes, pFanin ); + pFanin->fMarkA = pFanin->fMarkB = 0; + } + return vNodes; +} + +/**Function************************************************************* + + Synopsis [Duplicates the AIG while retiming the registers to the cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Saig_ManRetimeDupBackward( Aig_Man_t * p, Vec_Ptr_t * vCutInit ) +{ + Vec_Ptr_t * vToExclude, * vCut; + Vec_Int_t * vInit = NULL; + Aig_Man_t * pNew, * pInit; + Aig_Obj_t * pObj, * pObjLi, * pObjLo; + int i; + // check if there are bad registers + vToExclude = Saig_ManGetRegistersToExclude( p ); + if ( vToExclude ) + { + vCut = Saig_ManRetimeExtendCut( p, vCutInit, vToExclude ); + printf( "Bad registers = %d. Extended cut from %d to %d nodes.\n", + Vec_PtrSize(vToExclude), Vec_PtrSize(vCutInit), Vec_PtrSize(vCut) ); + Vec_PtrFree( vToExclude ); + } + else + vCut = Vec_PtrDup( vCutInit ); + // mark the cones under the cut +// assert( Vec_PtrSize(vCut) == Saig_ManRetimeCountCut(p, vCut) ); + // count if there are registers to disable + // derive the initial state + pInit = Saig_ManRetimeDupInitState( p, vCut ); + vInit = Saig_ManRetimeFindInitState( pInit ); + if ( vInit == NULL ) + printf( "Initial state computation has failed.\n" ); + Aig_ManStop( pInit ); + // create the new manager + pNew = Aig_ManStart( Aig_ManObjNumMax(p) ); + pNew->pName = Aig_UtilStrsav( p->pName ); + pNew->pSpec = Aig_UtilStrsav( p->pSpec ); + pNew->nRegs = Vec_PtrSize(vCut); + pNew->nTruePis = p->nTruePis; + pNew->nTruePos = p->nTruePos; + // create the true PIs + Aig_ManCleanData( p ); + Aig_ManConst1(p)->pData = Aig_ManConst1(pNew); + Saig_ManForEachPi( p, pObj, i ) + pObj->pData = Aig_ObjCreatePi( pNew ); + // create the registers + Vec_PtrForEachEntry( vCut, pObj, i ) + pObj->pData = Aig_NotCond( Aig_ObjCreatePi(pNew), vInit?Vec_IntEntry(vInit,i):0 ); + // duplicate logic above the cut and remember values + Saig_ManForEachLi( p, pObj, i ) + { + Saig_ManRetimeDup_rec( pNew, Aig_ObjFanin0(pObj) ); + pObj->pData = Aig_ObjChild0Copy(pObj); + } + // transfer values from the LIs to the LOs + Saig_ManForEachLiLo( p, pObjLi, pObjLo, i ) + pObjLo->pData = pObjLi->pData; + // erase the data values on the internal nodes of the cut + Vec_PtrForEachEntry( vCut, pObj, i ) + if ( Aig_ObjIsNode(pObj) ) + pObj->pData = NULL; + // replicate the data on the primary inputs + Saig_ManForEachPi( p, pObj, i ) + pObj->pData = Aig_ManPi( pNew, i ); + // duplicate logic below the cut + Saig_ManForEachPo( p, pObj, i ) + { + Saig_ManRetimeDup_rec( pNew, Aig_ObjFanin0(pObj) ); + Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); + } + Vec_PtrForEachEntry( vCut, pObj, i ) + { + Saig_ManRetimeDup_rec( pNew, pObj ); + Aig_ObjCreatePo( pNew, Aig_NotCond(pObj->pData, vInit?Vec_IntEntry(vInit,i):0) ); + } + if ( vInit ) + Vec_IntFree( vInit ); + Vec_PtrFree( vCut ); return pNew; } -- cgit v1.2.3