diff options
-rw-r--r-- | abclib.dsp | 44 | ||||
-rw-r--r-- | src/aig/cec/cecCec.c | 52 | ||||
-rw-r--r-- | src/aig/gia/module.make | 1 | ||||
-rw-r--r-- | src/aig/ntl/ntl.h | 3 | ||||
-rw-r--r-- | src/aig/ntl/ntlExtract.c | 11 | ||||
-rw-r--r-- | src/aig/ntl/ntlFraig.c | 41 | ||||
-rw-r--r-- | src/aig/ntl/ntlMan.c | 82 | ||||
-rw-r--r-- | src/aig/ntl/ntlTable.c | 24 | ||||
-rw-r--r-- | src/aig/ntl/ntlWriteBlif.c | 2 | ||||
-rw-r--r-- | src/aig/nwk/nwkUtil.c | 12 | ||||
-rw-r--r-- | src/aig/ssw/sswCore.c | 12 | ||||
-rw-r--r-- | src/base/abc/abcLib.c | 2 | ||||
-rw-r--r-- | src/base/abci/abc.c | 121 | ||||
-rw-r--r-- | src/base/abci/abcXsim.c | 14 | ||||
-rw-r--r-- | src/base/io/io.c | 11 | ||||
-rw-r--r-- | src/base/io/ioReadBlif.c | 75 | ||||
-rw-r--r-- | src/base/io/ioReadBlifMv.c | 8 | ||||
-rw-r--r-- | src/base/main/main.c | 124 |
18 files changed, 586 insertions, 53 deletions
@@ -3669,6 +3669,46 @@ SOURCE=.\src\aig\cgt\cgtSat.c # Begin Group "nal" # PROP Default_Filter "" +# Begin Source File + +SOURCE=.\src\aig\nal090422\nal.h +# End Source File +# Begin Source File + +SOURCE=.\src\aig\nal090422\nalCore.c +# End Source File +# Begin Source File + +SOURCE=.\src\aig\nal090422\nalFlop.c +# End Source File +# Begin Source File + +SOURCE=.\src\aig\nal090422\nalFunc.c +# End Source File +# Begin Source File + +SOURCE=.\src\aig\nal090422\nalInt.h +# End Source File +# Begin Source File + +SOURCE=.\src\aig\nal090422\nalMan.c +# End Source File +# Begin Source File + +SOURCE=.\src\aig\nal090422\nalModels.c +# End Source File +# Begin Source File + +SOURCE=.\src\aig\nal090422\nalRead.c +# End Source File +# Begin Source File + +SOURCE=.\src\aig\nal090422\nalUtil.c +# End Source File +# Begin Source File + +SOURCE=.\src\aig\nal090422\nalWrite.c +# End Source File # End Group # Begin Group "gia" @@ -3727,6 +3767,10 @@ SOURCE=.\src\aig\gia\giaEquiv.c # End Source File # Begin Source File +SOURCE=.\src\aig\gia\giaEra.c +# End Source File +# Begin Source File + SOURCE=.\src\aig\gia\giaFanout.c # End Source File # Begin Source File diff --git a/src/aig/cec/cecCec.c b/src/aig/cec/cecCec.c index 111cc8a8..a385be3e 100644 --- a/src/aig/cec/cecCec.c +++ b/src/aig/cec/cecCec.c @@ -247,6 +247,33 @@ int Cec_ManVerifyTwoAigs( Aig_Man_t * pAig0, Aig_Man_t * pAig1, int fVerbose ) SeeAlso [] ***********************************************************************/ +Aig_Man_t * Cec_LatchCorrespondence( Aig_Man_t * pAig, int nConfs, int fUseCSat ) +{ + extern int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars ); + Gia_Man_t * pGia; + Cec_ParCor_t CorPars, * pCorPars = &CorPars; + Cec_ManCorSetDefaultParams( pCorPars ); + pCorPars->fLatchCorr = 1; + pCorPars->fUseCSat = fUseCSat; + pCorPars->nBTLimit = nConfs; + pGia = Gia_ManFromAigSimple( pAig ); + Cec_ManLSCorrespondenceClasses( pGia, pCorPars ); + Gia_ManReprToAigRepr( pAig, pGia ); + Gia_ManStop( pGia ); + return Aig_ManDupSimple( pAig ); +} + +/**Function************************************************************* + + Synopsis [Implementation of new signal correspodence.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ Aig_Man_t * Cec_SignalCorrespondence( Aig_Man_t * pAig, int nConfs, int fUseCSat ) { extern int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars ); @@ -262,6 +289,31 @@ Aig_Man_t * Cec_SignalCorrespondence( Aig_Man_t * pAig, int nConfs, int fUseCSat return Aig_ManDupSimple( pAig ); } +/**Function************************************************************* + + Synopsis [Implementation of fraiging.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Cec_FraigCombinational( Aig_Man_t * pAig, int nConfs, int fVerbose ) +{ + Gia_Man_t * pGia; + Cec_ParFra_t FraPars, * pFraPars = &FraPars; + Cec_ManFraSetDefaultParams( pFraPars ); + pFraPars->nBTLimit = nConfs; + pFraPars->nItersMax = 20; + pFraPars->fVerbose = fVerbose; + pGia = Gia_ManFromAigSimple( pAig ); + Cec_ManSatSweeping( pGia, pFraPars ); + Gia_ManReprToAigRepr( pAig, pGia ); + Gia_ManStop( pGia ); + return Aig_ManDupSimple( pAig ); +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make index 916414fc..6f70f7d3 100644 --- a/src/aig/gia/module.make +++ b/src/aig/gia/module.make @@ -9,6 +9,7 @@ SRC += src/aig/gia/gia.c \ src/aig/gia/giaEmbed.c \ src/aig/gia/giaEnable.c \ src/aig/gia/giaEquiv.c \ + src/aig/gia/giaEra.c \ src/aig/gia/giaFanout.c \ src/aig/gia/giaForce.c \ src/aig/gia/giaFrames.c \ diff --git a/src/aig/ntl/ntl.h b/src/aig/ntl/ntl.h index c8d38331..a82b4d6c 100644 --- a/src/aig/ntl/ntl.h +++ b/src/aig/ntl/ntl.h @@ -309,7 +309,7 @@ extern ABC_DLL Aig_Man_t * Ntl_ManPrepareSec( char * pFileName1, char * pFil extern ABC_DLL Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p ); extern ABC_DLL Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p, int fSeq ); extern ABC_DLL Aig_Man_t * Ntl_ManCollapseComb( Ntl_Man_t * p ); -extern ABC_DLL Aig_Man_t * Ntl_ManCollapseSeq( Ntl_Man_t * p, int nMinDomSize ); +extern ABC_DLL Aig_Man_t * Ntl_ManCollapseSeq( Ntl_Man_t * p, int nMinDomSize, int fVerbose ); extern ABC_DLL Nwk_Man_t * Ntl_ManExtractNwk( Ntl_Man_t * p, Aig_Man_t * pAig, Tim_Man_t * pManTime ); /*=== ntlInsert.c ==========================================================*/ extern ABC_DLL Ntl_Man_t * Ntl_ManInsertMapping( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t * pAig ); @@ -354,6 +354,7 @@ extern ABC_DLL char * Ntl_ManStoreFileName( Ntl_Man_t * p, char * pFile extern ABC_DLL int Ntl_ManSweep( Ntl_Man_t * p, int fVerbose ); /*=== ntlTable.c ==========================================================*/ extern ABC_DLL Ntl_Net_t * Ntl_ModelFindNet( Ntl_Mod_t * p, const char * pName ); +extern ABC_DLL char * Ntl_ModelCreateNetName( Ntl_Mod_t * p, const char * pName, int Num ); extern ABC_DLL Ntl_Net_t * Ntl_ModelFindOrCreateNet( Ntl_Mod_t * p, const char * pName ); extern ABC_DLL Ntl_Net_t * Ntl_ModelDontFindCreateNet( Ntl_Mod_t * p, const char * pName ); extern ABC_DLL void Ntl_ModelSetPioNumbers( Ntl_Mod_t * p ); diff --git a/src/aig/ntl/ntlExtract.c b/src/aig/ntl/ntlExtract.c index b4abe3bf..6afeba26 100644 --- a/src/aig/ntl/ntlExtract.c +++ b/src/aig/ntl/ntlExtract.c @@ -623,7 +623,7 @@ Aig_Man_t * Ntl_ManCollapseComb( Ntl_Man_t * p ) SeeAlso [] ***********************************************************************/ -Aig_Man_t * Ntl_ManCollapseSeq( Ntl_Man_t * p, int nMinDomSize ) +Aig_Man_t * Ntl_ManCollapseSeq( Ntl_Man_t * p, int nMinDomSize, int fVerbose ) { Aig_Man_t * pAig; Ntl_Mod_t * pRoot; @@ -645,7 +645,7 @@ Aig_Man_t * Ntl_ManCollapseSeq( Ntl_Man_t * p, int nMinDomSize ) // perform the traversal pAig = Ntl_ManCollapse( p, 1 ); // check if there are register classes - pAig->vClockDoms = Ntl_ManTransformRegClasses( p, nMinDomSize, 1 ); + pAig->vClockDoms = Ntl_ManTransformRegClasses( p, nMinDomSize, fVerbose ); if ( pAig->vClockDoms ) { if ( Vec_VecSize(pAig->vClockDoms) == 0 ) @@ -654,9 +654,10 @@ Aig_Man_t * Ntl_ManCollapseSeq( Ntl_Man_t * p, int nMinDomSize ) Aig_ManStop( pAig ); pAig = NULL; } - else + else if ( fVerbose ) printf( "Performing seq synthesis for %d register classes.\n", Vec_VecSize(pAig->vClockDoms) ); - printf( "\n" ); + if ( fVerbose ) + printf( "\n" ); } return pAig; } @@ -706,7 +707,7 @@ Nwk_Obj_t * Ntl_ManExtractNwk_rec( Ntl_Man_t * p, Ntl_Net_t * pNet, Nwk_Man_t * Ntl_ManExtractNwk_rec( p, pFaninNet, pNtk, vCover, vMemory ); Nwk_ObjAddFanin( pNode, pFaninNet->pCopy2 ); } - if ( Ntl_ObjFaninNum(pNet->pDriver) == 0 ) + if ( Ntl_ObjFaninNum(pNet->pDriver) == 0 || Kit_PlaGetVarNum(pNet->pDriver->pSop) == 0 ) pNode->pFunc = Hop_NotCond( Hop_ManConst1(pNtk->pManHop), Kit_PlaIsConst0(pNet->pDriver->pSop) ); else { diff --git a/src/aig/ntl/ntlFraig.c b/src/aig/ntl/ntlFraig.c index 70f97d89..e98a3b46 100644 --- a/src/aig/ntl/ntlFraig.c +++ b/src/aig/ntl/ntlFraig.c @@ -219,6 +219,8 @@ void Ntl_ManReduce( Ntl_Man_t * p, Aig_Man_t * pAig ) Ntl_Mod_t * pRoot; Ntl_Obj_t * pNode, * pNodeOld; int i, fCompl, Counter = 0; + char * pNameNew; +// int Lenght; assert( pAig->pReprs ); pRoot = Ntl_ManRootModel( p ); Aig_ManForEachObj( pAig, pObj, i ) @@ -276,13 +278,17 @@ void Ntl_ManReduce( Ntl_Man_t * p, Aig_Man_t * pAig ) printf( "Ntl_ManReduce(): Internal error! Net already has no driver.\n" ); if ( !Ntl_ModelSetNetDriver( pNode, pNet ) ) printf( "Ntl_ManReduce(): Internal error! Net already has a driver.\n" ); - +/* // remove this net from the hash table (but do not remove from the array) Ntl_ModelDeleteNet( pRoot, pNet ); // create new net with the same name pNetNew = Ntl_ModelFindOrCreateNet( pRoot, pNet->pName ); // clean the name pNet->pName[0] = 0; +*/ + // create new net with a new name + pNameNew = Ntl_ModelCreateNetName( pRoot, "noname", (int)(ABC_PTRINT_T)pNet ); + pNetNew = Ntl_ModelFindOrCreateNet( pRoot, pNameNew ); // make the old node drive the new net without fanouts if ( !Ntl_ModelSetNetDriver( pNodeOld, pNetNew ) ) @@ -290,6 +296,7 @@ void Ntl_ManReduce( Ntl_Man_t * p, Aig_Man_t * pAig ) Counter++; } +// printf( "Nets without names = %d.\n", Counter ); } /**Function************************************************************* @@ -373,7 +380,7 @@ if ( fVerbose ) SeeAlso [] ***********************************************************************/ -Ntl_Man_t * Ntl_ManFraig( Ntl_Man_t * p, int nPartSize, int nConfLimit, int nLevelMax, int fVerbose ) +Ntl_Man_t * Ntl_ManFraig( Ntl_Man_t * p, int nPartSize, int nConfLimit, int nLevelMax, int fUseCSat, int fVerbose ) { Ntl_Man_t * pNew, * pAux; Aig_Man_t * pAig, * pAigCol, * pTemp; @@ -392,9 +399,19 @@ Ntl_Man_t * Ntl_ManFraig( Ntl_Man_t * p, int nPartSize, int nConfLimit, int nLev } // perform fraiging for the given design - nPartSize = nPartSize? nPartSize : Aig_ManPoNum(pAigCol); - pTemp = Aig_ManFraigPartitioned( pAigCol, nPartSize, nConfLimit, nLevelMax, fVerbose ); - Aig_ManStop( pTemp ); +// if ( fUseCSat ) + if ( 0 ) + { + extern Aig_Man_t * Cec_FraigCombinational( Aig_Man_t * pAig, int nConfs, int fVerbose ); + pTemp = Cec_FraigCombinational( pAigCol, nConfLimit, fVerbose ); + Aig_ManStop( pTemp ); + } + else + { + nPartSize = nPartSize? nPartSize : Aig_ManPoNum(pAigCol); + pTemp = Aig_ManFraigPartitioned( pAigCol, nPartSize, nConfLimit, nLevelMax, fVerbose ); + Aig_ManStop( pTemp ); + } // finalize the transformation pNew = Ntl_ManFinalize( pAux = pNew, pAig, pAigCol, fVerbose ); @@ -425,7 +442,7 @@ Ntl_Man_t * Ntl_ManScl( Ntl_Man_t * p, int fLatchConst, int fLatchEqual, int fVe //Ntl_ManPrintStats( p ); //Aig_ManPrintStats( pAig ); pNew = Ntl_ManInsertAig( p, pAig ); - pAigCol = Ntl_ManCollapseSeq( pNew, 0 ); + pAigCol = Ntl_ManCollapseSeq( pNew, 0, fVerbose ); if ( pAigCol == NULL ) { Aig_ManStop( pAig ); @@ -457,7 +474,7 @@ Ntl_Man_t * Ntl_ManScl( Ntl_Man_t * p, int fLatchConst, int fLatchEqual, int fVe SeeAlso [] ***********************************************************************/ -Ntl_Man_t * Ntl_ManLcorr( Ntl_Man_t * p, int nConfMax, int fVerbose ) +Ntl_Man_t * Ntl_ManLcorr( Ntl_Man_t * p, int nConfMax, int fScorrGia, int fUseCSat, int fVerbose ) { Ntl_Man_t * pNew, * pAux; Aig_Man_t * pAig, * pAigCol, * pTemp; @@ -469,7 +486,7 @@ Ntl_Man_t * Ntl_ManLcorr( Ntl_Man_t * p, int nConfMax, int fVerbose ) // collapse the AIG pAig = Ntl_ManExtract( p ); pNew = Ntl_ManInsertAig( p, pAig ); - pAigCol = Ntl_ManCollapseSeq( pNew, pPars->nMinDomSize ); + pAigCol = Ntl_ManCollapseSeq( pNew, pPars->nMinDomSize, pPars->fVerbose ); if ( pAigCol == NULL ) { Aig_ManStop( pAig ); @@ -477,6 +494,8 @@ Ntl_Man_t * Ntl_ManLcorr( Ntl_Man_t * p, int nConfMax, int fVerbose ) } // perform LCORR for the given design + pPars->fScorrGia = fScorrGia; + pPars->fUseCSat = fUseCSat; pTemp = Ssw_LatchCorrespondence( pAigCol, pPars ); Aig_ManStop( pTemp ); @@ -507,7 +526,7 @@ Ntl_Man_t * Ntl_ManSsw( Ntl_Man_t * p, Fra_Ssw_t * pPars ) // collapse the AIG pAig = Ntl_ManExtract( p ); pNew = Ntl_ManInsertAig( p, pAig ); - pAigCol = Ntl_ManCollapseSeq( pNew, pPars->nMinDomSize ); + pAigCol = Ntl_ManCollapseSeq( pNew, pPars->nMinDomSize, pPars->fVerbose ); if ( pAigCol == NULL ) { Aig_ManStop( pAig ); @@ -545,7 +564,7 @@ Ntl_Man_t * Ntl_ManScorr( Ntl_Man_t * p, Ssw_Pars_t * pPars ) // collapse the AIG pAig = Ntl_ManExtract( p ); pNew = Ntl_ManInsertAig( p, pAig ); - pAigCol = Ntl_ManCollapseSeq( pNew, pPars->nMinDomSize ); + pAigCol = Ntl_ManCollapseSeq( pNew, pPars->nMinDomSize, pPars->fVerbose ); if ( pAigCol == NULL ) { Aig_ManStop( pAig ); @@ -724,7 +743,7 @@ 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_ManCollapseSeq( p, pPars->nMinDomSize ); + pAigCol = Ntl_ManCollapseSeq( p, pPars->nMinDomSize, pPars->fVerbose ); // transform the collapsed AIG pAigRed = Fra_FraigInduction( pAigCol, pPars ); Aig_ManStop( pAigRed ); diff --git a/src/aig/ntl/ntlMan.c b/src/aig/ntl/ntlMan.c index 4c9bb311..da7e2317 100644 --- a/src/aig/ntl/ntlMan.c +++ b/src/aig/ntl/ntlMan.c @@ -285,6 +285,88 @@ void Nwk_ManPrintStatsShort( Ntl_Man_t * p, Aig_Man_t * pAig, Nwk_Man_t * pNtk ) /**Function************************************************************* + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Nwk_ManStatsRegs( Ntl_Man_t * p ) +{ + Ntl_Mod_t * pRoot; + Ntl_Obj_t * pObj; + int i, Counter = 0; + pRoot = Ntl_ManRootModel( p ); + Ntl_ModelForEachBox( pRoot, pObj, i ) + if ( strcmp(pObj->pImplem->pName, "dff") == 0 ) + Counter++; + return Counter; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Nwk_ManStatsLuts( Nwk_Man_t * pNtk ) +{ + return pNtk ? Nwk_ManNodeNum(pNtk) : -1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Nwk_ManStatsLevs( Nwk_Man_t * pNtk ) +{ + return pNtk ? Nwk_ManLevel(pNtk) : -1; +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Nwk_ManPrintStatsUpdate( Ntl_Man_t * p, Aig_Man_t * pAig, Nwk_Man_t * pNtk, + int nRegInit, int nLutInit, int nLevInit, int Time ) +{ + printf( "FF =%7d (%4.1f%%) ", Nwk_ManStatsRegs(p), 100.0*(nRegInit-Nwk_ManStatsRegs(p))/nRegInit ); + if ( pNtk == NULL ) + printf( "Mapping is not available. " ); + else + { + printf( "Lut =%7d (%4.1f%%) ", Nwk_ManStatsLuts(pNtk), 100.0*(nLutInit-Nwk_ManStatsLuts(pNtk))/nLutInit ); + printf( "Lev =%4d (%4.1f%%) ", Nwk_ManStatsLevs(pNtk), 100.0*(nLevInit-Nwk_ManStatsLevs(pNtk))/nLevInit ); + } + ABC_PRT( "Time", clock() - Time ); +} + + +/**Function************************************************************* + Synopsis [Deallocates the netlist manager.] Description [] diff --git a/src/aig/ntl/ntlTable.c b/src/aig/ntl/ntlTable.c index d227b1b9..0b87c8be 100644 --- a/src/aig/ntl/ntlTable.c +++ b/src/aig/ntl/ntlTable.c @@ -65,6 +65,30 @@ Ntl_Net_t * Ntl_ModelCreateNet( Ntl_Mod_t * p, const char * pName ) /**Function************************************************************* + Synopsis [Allocates memory for the net.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +char * Ntl_ModelCreateNetName( Ntl_Mod_t * p, const char * pName, int Num ) +{ + char * pResult; + char Buffer[1000]; + assert( strlen(pName) < 900 ); + do { + sprintf( Buffer, "%s%d", pName, Num++ ); + } while ( Ntl_ModelFindNet( p, Buffer ) != NULL ); + pResult = (char *)Aig_MmFlexEntryFetch( p->pMan->pMemObjs, strlen(Buffer) + 1 ); + strcpy( pResult, Buffer ); + return pResult; +} + +/**Function************************************************************* + Synopsis [Resizes the table.] Description [] diff --git a/src/aig/ntl/ntlWriteBlif.c b/src/aig/ntl/ntlWriteBlif.c index 4099d738..e6e4cbdd 100644 --- a/src/aig/ntl/ntlWriteBlif.c +++ b/src/aig/ntl/ntlWriteBlif.c @@ -631,7 +631,7 @@ void Ioa_WriteBlif( Ntl_Man_t * p, char * pFileName ) Ntl_Mod_t * pModel; int i, bzError; bz2file b; - if ( p->pNal ) + if ( p->pNal && strncmp(pFileName+strlen(pFileName)-5,".blif",5) ) { p->pNalW( p, pFileName ); return; diff --git a/src/aig/nwk/nwkUtil.c b/src/aig/nwk/nwkUtil.c index 12a72e2f..10b7b462 100644 --- a/src/aig/nwk/nwkUtil.c +++ b/src/aig/nwk/nwkUtil.c @@ -518,21 +518,9 @@ void Nwk_ManMinimumBase( Nwk_Man_t * pNtk, int fVerbose ) Vec_Int_t * vTruth; Nwk_Obj_t * pObj; int i, Counter = 0; - Nwk_Obj_t * pNodeThis = pNtk->vObjs->pArray[72688]; - vTruth = Vec_IntAlloc( 1 << 16 ); Nwk_ManForEachNode( pNtk, pObj, i ) - { - if ( i == 641386 ) - { - int x = 0; - } Counter += Nwk_ManMinimumBaseNode( pObj, vTruth, fVerbose ); - if ( pNodeThis->nFanouts != 15 ) - { - int s = 0; - } - } if ( fVerbose && Counter ) printf( "Support minimization reduced support of %d nodes.\n", Counter ); Vec_IntFree( vTruth ); diff --git a/src/aig/ssw/sswCore.c b/src/aig/ssw/sswCore.c index 41123ca4..6cb84800 100644 --- a/src/aig/ssw/sswCore.c +++ b/src/aig/ssw/sswCore.c @@ -280,8 +280,16 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) if ( pPars->fScorrGia ) { - extern Aig_Man_t * Cec_SignalCorrespondence( Aig_Man_t * pAig, int nConfs, int fUseCSat ); - return Cec_SignalCorrespondence( pAig, pPars->nBTLimit, pPars->fUseCSat ); + if ( pPars->fLatchCorrOpt ) + { + extern Aig_Man_t * Cec_LatchCorrespondence( Aig_Man_t * pAig, int nConfs, int fUseCSat ); + return Cec_LatchCorrespondence( pAig, pPars->nBTLimit, pPars->fUseCSat ); + } + else + { + extern Aig_Man_t * Cec_SignalCorrespondence( Aig_Man_t * pAig, int nConfs, int fUseCSat ); + return Cec_SignalCorrespondence( pAig, pPars->nBTLimit, pPars->fUseCSat ); + } } // start the induction manager diff --git a/src/base/abc/abcLib.c b/src/base/abc/abcLib.c index 138dc9a1..4540462d 100644 --- a/src/base/abc/abcLib.c +++ b/src/base/abc/abcLib.c @@ -82,7 +82,7 @@ void Abc_LibFree( Abc_Lib_t * pLib, Abc_Ntk_t * pNtkSave ) continue; // pNtk->pManFunc = NULL; pNtk->pDesign = NULL; - if ( pNtk->pManFunc == pNtkSave->pManFunc ) + if ( pNtkSave && pNtk->pManFunc == pNtkSave->pManFunc ) pNtk->pManFunc = NULL; Abc_NtkDelete( pNtk ); } diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 946b7210..660bf3e1 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -310,6 +310,7 @@ static int Abc_CommandAbc9Cec ( Abc_Frame_t * pAbc, int argc, char ** arg static int Abc_CommandAbc9Force ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Embed ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9If ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Era ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Test ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbcTestNew ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -629,6 +630,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "AIG", "&force", Abc_CommandAbc9Force, 0 ); Cmd_CommandAdd( pAbc, "AIG", "&embed", Abc_CommandAbc9Embed, 0 ); Cmd_CommandAdd( pAbc, "AIG", "&if", Abc_CommandAbc9If, 0 ); + Cmd_CommandAdd( pAbc, "AIG", "&era", Abc_CommandAbc9Era, 0 ); Cmd_CommandAdd( pAbc, "AIG", "&test", Abc_CommandAbc9Test, 0 ); Cmd_CommandAdd( pAbc, "Various", "testnew", Abc_CommandAbcTestNew, 0 ); @@ -18973,8 +18975,8 @@ int Abc_CommandAbc8Read( Abc_Frame_t * pAbc, int argc, char ** argv ) } else { -// extern void * Nal_ManRead( char * pFileName ); pAbc->pAbc8Ntl = NULL; +// extern void * Nal_ManRead( char * pFileName ); // pAbc->pAbc8Ntl = Nal_ManRead( pFileName ); // Ioa_WriteBlif( pAbc->pAbc8Ntl, "test_boxes.blif" ); if ( pAbc->pAbc8Ntl == NULL ) @@ -19104,7 +19106,7 @@ int Abc_CommandAbc8Write( Abc_Frame_t * pAbc, int argc, char ** argv ) extern void * Ntl_ManInsertAig( void * p, Aig_Man_t * pAig ); extern void * Ntl_ManDup( void * pOld ); extern void Ntl_ManFree( void * p ); - extern Aig_Man_t * Ntl_ManCollapseSeq( void * p, int nMinDomSize ); + extern Aig_Man_t * Ntl_ManCollapseSeq( void * p, int nMinDomSize, int fVerbose ); // set defaults fAig = 0; @@ -19142,7 +19144,7 @@ int Abc_CommandAbc8Write( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( fCollapsed ) { extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact ); - pTemp = Ntl_ManCollapseSeq( pAbc->pAbc8Ntl, 0 ); + pTemp = Ntl_ManCollapseSeq( pAbc->pAbc8Ntl, 0, 0 ); if ( fBlif ) Saig_ManDumpBlif( pTemp, pFileName ); else @@ -19632,7 +19634,7 @@ int Abc_CommandAbc8If( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pAbc->pAbc8Lib == NULL ) { - printf( "LUT library is not given. Using default LUT library.\n" ); +// printf( "LUT library is not given. Using default LUT library.\n" ); pAbc->pAbc8Lib = If_SetSimpleLutLib( 6 ); } @@ -19774,7 +19776,7 @@ int Abc_CommandAbc8If( Abc_Frame_t * pAbc, int argc, char ** argv ) // enable truth table computation if choices are selected if ( (c = Aig_ManChoiceNum( pAbc->pAbc8Aig )) ) { - printf( "Performing LUT mapping with %d choices.\n", c ); +// printf( "Performing LUT mapping with %d choices.\n", c ); pPars->fExpRed = 0; } // enable truth table computation if cut minimization is selected @@ -20813,17 +20815,19 @@ int Abc_CommandAbc8Fraig( Abc_Frame_t * pAbc, int argc, char ** argv ) int nPartSize; int nConfLimit; int nLevelMax; + int fUseCSat; extern Aig_Man_t * Ntl_ManExtract( void * p ); - extern void * Ntl_ManFraig( void * p, int nPartSize, int nConfLimit, int nLevelMax, int fVerbose ); + extern void * Ntl_ManFraig( void * p, int nPartSize, int nConfLimit, int nLevelMax, int fUseCSat, int fVerbose ); extern void Ntl_ManFree( void * p ); // set defaults nPartSize = 0; nConfLimit = 100; nLevelMax = 0; + fUseCSat = 0; fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "PCLvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "PCLcvh" ) ) != EOF ) { switch ( c ) { @@ -20860,6 +20864,9 @@ int Abc_CommandAbc8Fraig( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nLevelMax < 0 ) goto usage; break; + case 'c': + fUseCSat ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -20877,7 +20884,7 @@ int Abc_CommandAbc8Fraig( Abc_Frame_t * pAbc, int argc, char ** argv ) } // get the input file name - pNtlNew = Ntl_ManFraig( pAbc->pAbc8Ntl, nPartSize, nConfLimit, nLevelMax, fVerbose ); + pNtlNew = Ntl_ManFraig( pAbc->pAbc8Ntl, nPartSize, nConfLimit, nLevelMax, fUseCSat, fVerbose ); if ( pNtlNew == NULL ) { printf( "Abc_CommandAbc8Fraig(): Tranformation of the AIG has failed.\n" ); @@ -20905,6 +20912,7 @@ usage: fprintf( stdout, "\t-P num : partition size (0 = partitioning is not used) [default = %d]\n", nPartSize ); fprintf( stdout, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfLimit ); fprintf( stdout, "\t-L num : limit on node level to fraig (0 = fraig all nodes) [default = %d]\n", nLevelMax ); +// fprintf( stdout, "\t-c : toggle using new AIG package and SAT solver [default = %s]\n", fUseCSat? "yes": "no" ); fprintf( stdout, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" ); fprintf( stdout, "\t-h : print the command usage\n"); return 1; @@ -21018,19 +21026,23 @@ int Abc_CommandAbc8Lcorr( Abc_Frame_t * pAbc, int argc, char ** argv ) { void * pNtlNew; int c; + int fScorrGia; + int fUseCSat; int nFramesP; int nConfMax; int fVerbose; extern Aig_Man_t * Ntl_ManExtract( void * p ); - extern void * Ntl_ManLcorr( void * p, int nConfMax, int fVerbose ); + extern void * Ntl_ManLcorr( void * p, int nConfMax, int fScorrGia, int fUseCSat, int fVerbose ); extern int Ntl_ManIsComb( void * p ); // set defaults + fScorrGia = 0; + fUseCSat = 0; nFramesP = 0; nConfMax = 10000; fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "PCvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "PCncvh" ) ) != EOF ) { switch ( c ) { @@ -21056,6 +21068,12 @@ int Abc_CommandAbc8Lcorr( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nConfMax < 0 ) goto usage; break; + case 'n': + fScorrGia ^= 1; + break; + case 'c': + fUseCSat ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -21079,7 +21097,7 @@ int Abc_CommandAbc8Lcorr( Abc_Frame_t * pAbc, int argc, char ** argv ) } // get the input file name - pNtlNew = Ntl_ManLcorr( pAbc->pAbc8Ntl, nConfMax, fVerbose ); + pNtlNew = Ntl_ManLcorr( pAbc->pAbc8Ntl, nConfMax, fScorrGia, fUseCSat, fVerbose ); if ( pNtlNew == NULL ) { printf( "Abc_CommandAbc8Lcorr(): Tranformation of the AIG has failed.\n" ); @@ -21102,10 +21120,12 @@ int Abc_CommandAbc8Lcorr( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( stdout, "usage: *lcorr [-C num] [-vh]\n" ); + fprintf( stdout, "usage: *lcorr [-C num] [-ncvh]\n" ); fprintf( stdout, "\t computes latch correspondence for the netlist\n" ); // fprintf( stdout, "\t-P num : number of time frames to use as the prefix [default = %d]\n", nFramesP ); fprintf( stdout, "\t-C num : max conflict number when proving latch equivalence [default = %d]\n", nConfMax ); + fprintf( stdout, "\t-n : toggle using new AIG package [default = %s]\n", fScorrGia? "yes": "no" ); + fprintf( stdout, "\t-c : toggle using new AIG package and SAT solver [default = %s]\n", fUseCSat? "yes": "no" ); fprintf( stdout, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" ); fprintf( stdout, "\t-h : print the command usage\n"); return 1; @@ -21625,7 +21645,7 @@ int Abc_CommandAbc8Sweep( Abc_Frame_t * pAbc, int argc, char ** argv ) // sweep the current design Counter = Ntl_ManSweep( pAbc->pAbc8Ntl, fVerbose ); - if ( Counter == 0 ) + if ( Counter == 0 && fVerbose ) printf( "The netlist is unchanged by sweep.\n" ); // if mapped, create new AIG and new mapped network @@ -24508,6 +24528,7 @@ usage: fprintf( stdout, "\t-h : print the command usage\n"); return 1; } + /**Function************************************************************* Synopsis [] @@ -24739,6 +24760,80 @@ usage: SeeAlso [] ***********************************************************************/ +int Abc_CommandAbc9Era( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + Gia_Man_t * pTemp = NULL; + int c, fVerbose = 0; + int fMiter = 0; + int nStatesMax = 1000000; + extern void Gia_ManCollectReachable( Gia_Man_t * pAig, int nStatesMax, int fMiter, int fVerbose ); + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "Smvh" ) ) != EOF ) + { + switch ( c ) + { + case 'S': + if ( globalUtilOptind >= argc ) + { + fprintf( stdout, "Command line switch \"-S\" should be followed by a positive integer.\n" ); + goto usage; + } + nStatesMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nStatesMax < 0 ) + goto usage; + break; + case 'm': + fMiter ^= 1; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pAbc->pAig == NULL ) + { + printf( "Abc_CommandAbc9Era(): There is no AIG.\n" ); + return 1; + } + if ( Gia_ManPiNum(pAbc->pAig) > 12 ) + { + printf( "Abc_CommandAbc9Era(): The number of PIs (%d) should be no more than 12.\n", Gia_ManPiNum(pAbc->pAig) ); + return 1; + } + if ( Gia_ManRegNum(pAbc->pAig) == 0 ) + { + printf( "Abc_CommandAbc9Era(): The network is combinational.\n" ); + return 1; + } + Gia_ManCollectReachable( pAbc->pAig, nStatesMax, fMiter, fVerbose ); + return 0; + +usage: + fprintf( stdout, "usage: &era [-S num] [-mvh]\n" ); + fprintf( stdout, "\t explicit reachability analysis for small sequential AIGs\n" ); + fprintf( stdout, "\t-S num : the max number of states to traverse (num > 0) [default = %d]\n", nStatesMax ); + fprintf( stdout, "\t-m : stop when the miter output is 1 [default = %s]\n", fMiter? "yes": "no" ); + fprintf( stdout, "\t-v : print verbose information [default = %s]\n", fVerbose? "yes": "no" ); + fprintf( stdout, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv ) { Gia_Man_t * pTemp = NULL; diff --git a/src/base/abci/abcXsim.c b/src/base/abci/abcXsim.c index 5e9093e7..b77f9d77 100644 --- a/src/base/abci/abcXsim.c +++ b/src/base/abci/abcXsim.c @@ -20,6 +20,8 @@ #include "abc.h" +extern unsigned Gia_ManRandom( int fReset ); + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -50,13 +52,15 @@ static inline int Abc_XsimAnd( int Value0, int Value1 ) } static inline int Abc_XsimRand2() { - return (rand() & 1) ? XVS1 : XVS0; +// return (rand() & 1) ? XVS1 : XVS0; + return (Gia_ManRandom(0) & 1) ? XVS1 : XVS0; } static inline int Abc_XsimRand3() { int RetValue; do { - RetValue = rand() & 3; +// RetValue = rand() & 3; + RetValue = Gia_ManRandom(0) & 3; } while ( RetValue == 0 ); return RetValue; } @@ -108,7 +112,8 @@ void Abc_NtkXValueSimulate( Abc_Ntk_t * pNtk, int nFrames, int fXInputs, int fXS Abc_Obj_t * pObj; int i, f; assert( Abc_NtkIsStrash(pNtk) ); - srand( 0x12341234 ); +// srand( 0x12341234 ); + Gia_ManRandom( 1 ); // start simulation Abc_ObjSetXsim( Abc_AigConst1(pNtk), XVS1 ); if ( fXInputs ) @@ -194,7 +199,8 @@ void Abc_NtkCycleInitState( Abc_Ntk_t * pNtk, int nFrames, int fUseXval, int fVe Abc_Obj_t * pObj; int i, f; assert( Abc_NtkIsStrash(pNtk) ); - srand( 0x12341234 ); +// srand( 0x12341234 ); + Gia_ManRandom( 1 ); // initialize the values Abc_ObjSetXsim( Abc_AigConst1(pNtk), XVS1 ); Abc_NtkForEachLatch( pNtk, pObj, i ) diff --git a/src/base/io/io.c b/src/base/io/io.c index e29a3009..ecc6302f 100644 --- a/src/base/io/io.c +++ b/src/base/io/io.c @@ -2343,13 +2343,17 @@ int IoCommandWriteTruth( Abc_Frame_t * pAbc, int argc, char **argv ) char * pFileName; FILE * pFile; unsigned * pTruth; + int fReverse = 0; int c; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "rh" ) ) != EOF ) { switch ( c ) { + case 'r': + fReverse ^= 1; + break; case 'h': goto usage; default: @@ -2394,7 +2398,7 @@ int IoCommandWriteTruth( Abc_Frame_t * pAbc, int argc, char **argv ) // convert to logic Abc_NtkToAig( pNtk ); vTruth = Vec_IntAlloc( 0 ); - pTruth = Hop_ManConvertAigToTruth( pNtk->pManFunc, pNode->pData, Abc_ObjFaninNum(pNode), vTruth, 0 ); + pTruth = Hop_ManConvertAigToTruth( pNtk->pManFunc, pNode->pData, Abc_ObjFaninNum(pNode), vTruth, fReverse ); pFile = fopen( pFileName, "w" ); if ( pFile == NULL ) { @@ -2408,8 +2412,9 @@ int IoCommandWriteTruth( Abc_Frame_t * pAbc, int argc, char **argv ) return 0; usage: - fprintf( pAbc->Err, "usage: write_truth [-h] <file>\n" ); + fprintf( pAbc->Err, "usage: write_truth [-rh] <file>\n" ); fprintf( pAbc->Err, "\t writes truth table into a file\n" ); + fprintf( pAbc->Err, "\t-r : toggle reversing bits in the truth table [default = %s]\n", fReverse? "yes":"no" ); fprintf( pAbc->Err, "\t-h : print the help massage\n" ); fprintf( pAbc->Err, "\tfile : the name of the file to write\n" ); return 1; diff --git a/src/base/io/ioReadBlif.c b/src/base/io/ioReadBlif.c index b6eb29e3..f2c3e8c2 100644 --- a/src/base/io/ioReadBlif.c +++ b/src/base/io/ioReadBlif.c @@ -535,6 +535,71 @@ int Io_ReadBlifNetworkNames( Io_ReadBlif_t * p, Vec_Ptr_t ** pvTokens ) SeeAlso [] ***********************************************************************/ +int Io_ReadBlifReorderFormalNames( Vec_Ptr_t * vTokens, Mio_Gate_t * pGate ) +{ + Mio_Pin_t * pGatePin; + char * pName, * pNamePin; + int i, k, nSize, Length; + nSize = Vec_PtrSize(vTokens); + if ( nSize - 3 != Mio_GateReadInputs(pGate) ) + return 0; + // check if the names are in order + for ( pGatePin = Mio_GateReadPins(pGate), i = 0; pGatePin; pGatePin = Mio_PinReadNext(pGatePin), i++ ) + { + pNamePin = Mio_PinReadName(pGatePin); + Length = strlen(pNamePin); + pName = Vec_PtrEntry(vTokens, i+2); + if ( !strncmp( pNamePin, pName, Length ) && pName[Length] == '=' ) + continue; + break; + } + if ( i == nSize - 3 ) + return 1; + // reorder the pins + for ( pGatePin = Mio_GateReadPins(pGate), i = 0; pGatePin; pGatePin = Mio_PinReadNext(pGatePin), i++ ) + { + pNamePin = Mio_PinReadName(pGatePin); + Length = strlen(pNamePin); + for ( k = 2; k < nSize; k++ ) + { + pName = Vec_PtrEntry(vTokens, k); + if ( !strncmp( pNamePin, pName, Length ) && pName[Length] == '=' ) + { + Vec_PtrPush( vTokens, pName ); + break; + } + } + } + pNamePin = Mio_GateReadOutName(pGate); + Length = strlen(pNamePin); + for ( k = 2; k < nSize; k++ ) + { + pName = Vec_PtrEntry(vTokens, k); + if ( !strncmp( pNamePin, pName, Length ) && pName[Length] == '=' ) + { + Vec_PtrPush( vTokens, pName ); + break; + } + } + if ( Vec_PtrSize(vTokens) - nSize != nSize - 2 ) + return 0; + Vec_PtrForEachEntryStart( vTokens, pName, k, nSize ) + Vec_PtrWriteEntry( vTokens, k - nSize + 2, pName ); + Vec_PtrShrink( vTokens, nSize ); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int Io_ReadBlifNetworkGate( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens ) { Mio_Library_t * pGenlib; @@ -581,6 +646,16 @@ int Io_ReadBlifNetworkGate( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens ) p->pNtkCur->pManFunc = pGenlib; } + // reorder the formal inputs to be in the same order as in the gate + if ( !Io_ReadBlifReorderFormalNames( vTokens, pGate ) ) + { + p->LineCur = Extra_FileReaderGetLineNumber(p->pReader, 0); + sprintf( p->sError, "Mismatch in the fanins of gate \"%s\".", (char*)vTokens->pArray[1] ); + Io_ReadBlifPrintErrorMessage( p ); + return 1; + } + + // remove the formal parameter names for ( i = 2; i < vTokens->nSize; i++ ) { diff --git a/src/base/io/ioReadBlifMv.c b/src/base/io/ioReadBlifMv.c index 95e7cd1d..2e2388d3 100644 --- a/src/base/io/ioReadBlifMv.c +++ b/src/base/io/ioReadBlifMv.c @@ -1828,6 +1828,7 @@ static char * Io_ReadBlifCleanName( char * pName ) ***********************************************************************/ static int Io_MvParseLineGateBlif( Io_MvMod_t * p, Vec_Ptr_t * vTokens ) { + extern int Io_ReadBlifReorderFormalNames( Vec_Ptr_t * vTokens, Mio_Gate_t * pGate ); Mio_Library_t * pGenlib; Mio_Gate_t * pGate; Abc_Obj_t * pNode; @@ -1868,6 +1869,13 @@ static int Io_MvParseLineGateBlif( Io_MvMod_t * p, Vec_Ptr_t * vTokens ) p->pNtk->pManFunc = pGenlib; } + // reorder the formal inputs to be in the same order as in the gate + if ( !Io_ReadBlifReorderFormalNames( vTokens, pGate ) ) + { + sprintf( p->pMan->sError, "Line %d: Mismatch in the fanins of gate \"%s\".", Io_MvGetLine(p->pMan, pName), (char*)vTokens->pArray[1] ); + return 0; + } + // remove the formal parameter names for ( i = 2; i < vTokens->nSize; i++ ) { diff --git a/src/base/main/main.c b/src/base/main/main.c index 3aee2e44..738f217c 100644 --- a/src/base/main/main.c +++ b/src/base/main/main.c @@ -310,6 +310,130 @@ static int TypeCheck( Abc_Frame_t * pAbc, char * s ) } } + + + +/**Function************************************************************* + + Synopsis [Find the file name.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +char * Abc_MainFileName( char * pFileName ) +{ + static char Buffer[200]; + char * pExtension; + assert( strlen(pFileName) < 190 ); + pExtension = Extra_FileNameExtension( pFileName ); + if ( pExtension == NULL ) + sprintf( Buffer, "%s.opt", pFileName ); + else + { + strncpy( Buffer, pFileName, pExtension-pFileName-1 ); + sprintf( Buffer+(pExtension-pFileName-1), ".opt.%s", pExtension ); + } + return Buffer; +} + +/**Function************************************************************* + + Synopsis [The main() procedure.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int main_( int argc, char * argv[] ) +{ + extern void Nwk_ManPrintStatsUpdate( void * p, void * pAig, void * pNtk, + int nRegInit, int nLutInit, int nLevInit, int Time ); + char * pComs[20] = + { +/*00*/ "*r -am ", +/*01*/ "*w -abc 1.aig", +/*02*/ "*lcorr -nc",//; *ps", +/*03*/ "*scorr -nc",//; *ps", +/*04*/ "*dch; *if -K 4 -C 16 -F 3 -A 2; *sw -m",//; *ps", +/*05*/ "*dch; *if -K 4 -C 16 -F 3 -A 2; *sw -m",//; *ps", +/*06*/ "*w ", +/*07*/ "*w -abc 2.aig", +/*08*/ "miter -mc 1.aig 2.aig; sim -F 4 -W 4 -mv" + }; + char Command[1000]; + int i, nComs; + Abc_Frame_t * pAbc; + FILE * pFile; + int nRegInit, nLutInit, nLevInit; + int clkStart = clock(); + + // added to detect memory leaks: +#if defined(_DEBUG) && defined(_MSC_VER) + _CrtSetDbgFlag( _CRTDBG_ALLOC_MEM_DF | _CRTDBG_LEAK_CHECK_DF ); +#endif + + // check that the file is present + if ( argc != 2 ) + { + printf( "Expecting one command argument (file name).\n" ); + return 0; + } + pFile = fopen( argv[1], "r" ); + if ( pFile == NULL ) + { + printf( "Cannot open file \"%s\".\n", argv[1] ); + return 0; + } + fclose( pFile ); + + // count the number of commands + for ( nComs = 0; nComs < 20; nComs++ ) + if ( pComs[nComs] == NULL ) + break; + // perform the commands + printf( "Reading design \"%s\"...\n", argv[1] ); + pAbc = Abc_FrameGetGlobalFrame(); + for ( i = 0; i < nComs; i++ ) + { + + if ( i == 0 ) + sprintf( Command, "%s%s", pComs[i], argv[1] ); + else if ( i == 6 ) + sprintf( Command, "%s%s", pComs[i], Abc_MainFileName(argv[1]) ); + else + sprintf( Command, "%s", pComs[i] ); + if ( Cmd_CommandExecute( pAbc, Command ) ) + { + printf( "Internal command %d failed.\n", i ); + return 0; + } + if ( i == 0 ) + { + extern int Nwk_ManStatsRegs( void * p ); + extern int Nwk_ManStatsLuts( void * pNtk ); + extern int Nwk_ManStatsLevs( void * pNtk ); + nRegInit = Nwk_ManStatsRegs( pAbc->pAbc8Ntl ); + nLutInit = Nwk_ManStatsLuts( pAbc->pAbc8Nwk ); + nLevInit = Nwk_ManStatsLevs( pAbc->pAbc8Nwk ); + } + if ( i >= 1 && i <= 5 ) + Nwk_ManPrintStatsUpdate( pAbc->pAbc8Ntl, pAbc->pAbc8Aig, pAbc->pAbc8Nwk, + nRegInit, nLutInit, nLevInit, clkStart ); + } + Abc_Stop(); + printf( "Writing optimized design \"%s\"...\n", Abc_MainFileName(argv[1]) ); + ABC_PRT( "Total time", clock() - clkStart ); + printf( "\n" ); + return 0; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// |