Version abc90528

committer: Baruch Sterin <baruchs@gmail.com>

6 files changed, 145 insertions, 18 deletions

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;