Version abc90528

committer: Baruch Sterin <baruchs@gmail.com>

10 files changed, 208 insertions, 32 deletions

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