Version abc61210

6 files changed, 59 insertions, 28 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 115e9bb8..0619b26a 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -7529,25 +7529,26 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
     memset( pPars, 0, sizeof(If_Par_t) );
     // user-controlable paramters
     pPars->nLutSize    =  4;
-    pPars->nCutsMax    = 10;
+    pPars->nCutsMax    =  8;
     pPars->DelayTarget = -1;
     pPars->fPreprocess =  1;
     pPars->fArea       =  0;
     pPars->fFancy      =  0;
     pPars->fExpRed     =  1;
     pPars->fLatchPaths =  0;
-    pPars->fSeq        =  0;
+    pPars->fSeqMap     =  0;
     pPars->fVerbose    =  0;
     // internal parameters
     pPars->fTruth      =  0;
     pPars->nLatches    =  pNtk? Abc_NtkLatchNum(pNtk) : 0;
+    pPars->fLiftLeaves =  0;
     pPars->pLutLib     =  NULL; // Abc_FrameReadLibLut();
     pPars->pTimesArr   =  NULL; 
     pPars->pTimesArr   =  NULL;   
     pPars->pFuncCost   =  NULL;   
 
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "KCDpaflrsvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "KCDpaflrstvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -7600,7 +7601,10 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
             pPars->fExpRed ^= 1;
             break;
         case 's':
-            pPars->fSeq ^= 1;
+            pPars->fSeqMap ^= 1;
+            break;
+        case 't':
+            pPars->fLiftLeaves ^= 1;
             break;
         case 'v':
             pPars->fVerbose ^= 1;
@@ -7616,12 +7620,18 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Empty network.\n" );
         return 1;
     }
-
+/*
     if ( pPars->fSeq )
     {
         fprintf( pErr, "Sequential mapping is currently being implemented.\n" );
         return 1;
     }
+*/
+    if ( pPars->fSeqMap && pPars->nLatches == 0 )
+    {
+        fprintf( pErr, "The network has no latches. Use combinational mapping instead of sequential.\n" );
+        return 1;
+    }
 
     if ( pPars->nLutSize < 3 || pPars->nLutSize > IF_MAX_LUTSIZE )
     {
@@ -7649,13 +7659,6 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    // set the latch paths
-    if ( pPars->fLatchPaths )
-    {
-        for ( c = 0; c < Abc_NtkPiNum(pNtk); c++ )
-            pPars->pTimesArr[c] = -ABC_INFINITY;
-    }
-
     if ( !Abc_NtkIsStrash(pNtk) )
     {
         // strash and balance the network
@@ -7679,7 +7682,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
         {
             Abc_NtkDelete( pNtk );
             fprintf( pErr, "FPGA mapping has failed.\n" );
-            return 1;
+            return 0;
         }
         Abc_NtkDelete( pNtk );
     }
@@ -7690,7 +7693,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
         if ( pNtkRes == NULL )
         {
             fprintf( pErr, "FPGA mapping has failed.\n" );
-            return 1;
+            return 0;
         }
     }
     // replace the current network
@@ -7706,17 +7709,18 @@ usage:
         sprintf( LutSize, "library" );
     else
         sprintf( LutSize, "%d", pPars->nLutSize );
-    fprintf( pErr, "usage: if [-K num] [-C num] [-D float] [-pafrsvh]\n" );
+    fprintf( pErr, "usage: if [-K num] [-C num] [-D float] [-pafrstvh]\n" );
     fprintf( pErr, "\t           performs FPGA technology mapping of the network\n" );
     fprintf( pErr, "\t-K num   : the number of LUT inputs (2 < num < %d) [default = %s]\n", IF_MAX_LUTSIZE+1, LutSize );
     fprintf( pErr, "\t-C num   : the max number of cuts to use (1 < num < 2^12) [default = %d]\n", pPars->nCutsMax );
     fprintf( pErr, "\t-D float : sets the delay constraint for the mapping [default = %s]\n", Buffer );  
     fprintf( pErr, "\t-p       : toggles preprocessing using several starting points [default = %s]\n", pPars->fPreprocess? "yes": "no" );
     fprintf( pErr, "\t-a       : toggles area-oriented mapping [default = %s]\n", pPars->fArea? "yes": "no" );
-    fprintf( pErr, "\t-f       : toggles one fancy feature [default = %s]\n", pPars->fFancy? "yes": "no" );
+//    fprintf( pErr, "\t-f       : toggles one fancy feature [default = %s]\n", pPars->fFancy? "yes": "no" );
     fprintf( pErr, "\t-r       : enables expansion/reduction of the best cuts [default = %s]\n", pPars->fExpRed? "yes": "no" );
     fprintf( pErr, "\t-l       : optimizes latch paths for delay, other paths for area [default = %s]\n", pPars->fLatchPaths? "yes": "no" );
-    fprintf( pErr, "\t-s       : toggles sequential mapping [default = %s]\n", pPars->fSeq? "yes": "no" );
+    fprintf( pErr, "\t-s       : toggles sequential mapping [default = %s]\n", pPars->fSeqMap? "yes": "no" );
+    fprintf( pErr, "\t-t       : toggles the use of true sequential cuts [default = %s]\n", pPars->fLiftLeaves? "yes": "no" );
     fprintf( pErr, "\t-v       : toggles verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h       : prints the command usage\n");
     return 1;
diff --git a/src/base/abci/abcFraig.c b/src/base/abci/abcFraig.c
index a4c44883..daf30331 100644
--- a/src/base/abci/abcFraig.c
+++ b/src/base/abci/abcFraig.c
@@ -117,7 +117,7 @@ void * Abc_NtkToFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes, int fExd
     // create PIs and remember them in the old nodes
     Abc_NtkForEachCi( pNtk, pNode, i )
         pNode->pCopy = (Abc_Obj_t *)Fraig_ManReadIthVar(pMan, i);
-
+ 
     // perform strashing
     vNodes = Abc_AigDfs( pNtk, fAllNodes, 0 );
     if ( !fInternal )
diff --git a/src/base/abci/abcIf.c b/src/base/abci/abcIf.c
index d2129e82..871bf148 100644
--- a/src/base/abci/abcIf.c
+++ b/src/base/abci/abcIf.c
@@ -58,6 +58,14 @@ Abc_Ntk_t * Abc_NtkIf( Abc_Ntk_t * pNtk, If_Par_t * pPars )
     pPars->pTimesArr = Abc_NtkGetCiArrivalFloats(pNtk);
     pPars->pTimesReq = NULL;
 
+    // set the latch paths
+    if ( pPars->fLatchPaths && pPars->pTimesArr )
+    {
+        int c;
+        for ( c = 0; c < Abc_NtkPiNum(pNtk); c++ )
+            pPars->pTimesArr[c] = -ABC_INFINITY;
+    }
+
     // perform FPGA mapping
     pIfMan = Abc_NtkToIf( pNtk, pPars );    
     if ( pIfMan == NULL )
@@ -117,7 +125,10 @@ If_Man_t * Abc_NtkToIf( Abc_Ntk_t * pNtk, If_Par_t * pPars )
     // create PIs and remember them in the old nodes
     Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)If_ManConst1( pIfMan );
     Abc_NtkForEachCi( pNtk, pNode, i )
-        pNode->pCopy = (Abc_Obj_t *)If_ManCreatePi( pIfMan );
+    {
+        pNode->pCopy = (Abc_Obj_t *)If_ManCreateCi( pIfMan );
+//printf( "AIG CI %2d -> IF CI %2d\n", pNode->Id, ((If_Obj_t *)pNode->pCopy)->Id );
+    }
 
     // load the AIG into the mapper
     pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pNtk) );
@@ -136,13 +147,14 @@ If_Man_t * Abc_NtkToIf( Abc_Ntk_t * pNtk, If_Par_t * pPars )
                 If_ObjSetChoice( (If_Obj_t *)pPrev->pCopy, (If_Obj_t *)pFanin->pCopy );
             If_ManCreateChoice( pIfMan, (If_Obj_t *)pNode->pCopy );
         }
+//printf( "AIG node %2d -> IF node %2d\n", pNode->Id, ((If_Obj_t *)pNode->pCopy)->Id );
     }
     Extra_ProgressBarStop( pProgress );
     Vec_PtrFree( vNodes );
 
     // set the primary outputs without copying the phase
     Abc_NtkForEachCo( pNtk, pNode, i )
-        If_ManCreatePo( pIfMan, (If_Obj_t *)Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) );
+        If_ManCreateCo( pIfMan, (If_Obj_t *)Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) );
     return pIfMan;
 }
 
@@ -177,15 +189,15 @@ Abc_Ntk_t * Abc_NtkFromIf( If_Man_t * pIfMan, Abc_Ntk_t * pNtk )
     // make the mapper point to the new network
     If_ObjSetCopy( If_ManConst1(pIfMan), Abc_NtkCreateNodeConst1(pNtkNew) );
     Abc_NtkForEachCi( pNtk, pNode, i )
-        If_ObjSetCopy( If_ManPi(pIfMan, i), pNode->pCopy );
+        If_ObjSetCopy( If_ManCi(pIfMan, i), pNode->pCopy );
     // process the nodes in topological order
     vCover = Vec_IntAlloc( 1 << 16 );
     pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) );
     Abc_NtkForEachCo( pNtk, pNode, i )
     {
         Extra_ProgressBarUpdate( pProgress, i, "Final" );
-        pNodeNew = Abc_NodeFromIf_rec( pNtkNew, pIfMan, If_ObjFanin0(If_ManPo(pIfMan, i)), vCover );
-        pNodeNew = Abc_ObjNotCond( pNodeNew, If_ObjFaninC0(If_ManPo(pIfMan, i)) );
+        pNodeNew = Abc_NodeFromIf_rec( pNtkNew, pIfMan, If_ObjFanin0(If_ManCo(pIfMan, i)), vCover );
+        pNodeNew = Abc_ObjNotCond( pNodeNew, If_ObjFaninC0(If_ManCo(pIfMan, i)) );
         Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
     }
     Extra_ProgressBarStop( pProgress );
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index 002a885c..27235d0a 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -118,15 +118,19 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
         fprintf( pFile, "  lev = %3d", Abc_NtkLevel(pNtk) );
 
     fprintf( pFile, "\n" );
+
+
     // print the statistic into a file
 /*
     {
         FILE * pTable;
-        pTable = fopen( "stats.txt", "a+" );
+        pTable = fopen( "a/seqmap__stats.txt", "a+" );
         fprintf( pTable, "%s ",  pNtk->pName );
         fprintf( pTable, "%d ", Abc_NtkPiNum(pNtk) );
+        fprintf( pTable, "%d ", Abc_NtkPoNum(pNtk) );
+        fprintf( pTable, "%d ", Abc_NtkLatchNum(pNtk) );
         fprintf( pTable, "%d ", Abc_NtkNodeNum(pNtk) );
-        fprintf( pTable, "%d ", Abc_AigLevel(pNtk) );
+        fprintf( pTable, "%d ", Abc_NtkLevel(pNtk) );
         fprintf( pTable, "\n" );
         fclose( pTable );
     }
diff --git a/src/base/abci/abcRenode.c b/src/base/abci/abcRenode.c
index b8aa49a4..462d9da3 100644
--- a/src/base/abci/abcRenode.c
+++ b/src/base/abci/abcRenode.c
@@ -56,6 +56,9 @@ Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int nCubeMax, int fA
     If_Par_t Pars, * pPars = &Pars;
     Abc_Ntk_t * pNtkNew;
 
+    if ( Abc_NtkGetChoiceNum( pNtk ) )
+        printf( "Performing renoding with choices.\n" );
+
     // set defaults
     memset( pPars, 0, sizeof(If_Par_t) );
     // user-controlable paramters
@@ -67,11 +70,11 @@ Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int nCubeMax, int fA
     pPars->fFancy      =  0;
     pPars->fExpRed     =  0; //
     pPars->fLatchPaths =  0;
-    pPars->fSeq        =  0;
+    pPars->fSeqMap     =  0;
     pPars->fVerbose    =  fVerbose;
     // internal parameters
     pPars->fTruth      =  1;
-    pPars->fUsePerm    =  1; //!fUseSops;
+    pPars->fUsePerm    =  1; 
     pPars->nLatches    =  0;
     pPars->pLutLib     =  NULL; // Abc_FrameReadLibLut();
     pPars->pTimesArr   =  NULL; 
diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c
index a3719b10..2e1b3eb1 100644
--- a/src/base/abci/abcStrash.c
+++ b/src/base/abci/abcStrash.c
@@ -151,7 +151,8 @@ Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes, bool fCleanup )
 int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fAddPos )
 {
     Abc_Obj_t * pObj;
-    int i;
+    char * pName;
+    int i, nNewCis;
     // the first network should be an AIG
     assert( Abc_NtkIsStrash(pNtk1) );
     assert( Abc_NtkIsLogic(pNtk2) || Abc_NtkIsStrash(pNtk2) ); 
@@ -165,13 +166,20 @@ int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fAddPos )
     if ( !Abc_NtkCompareSignals( pNtk1, pNtk2, 1, 1 ) )
         printf( "Abc_NtkAppend(): The union of the network PIs is computed (warning).\n" );
     // perform strashing
+    nNewCis = 0;
     Abc_NtkCleanCopy( pNtk2 );
     Abc_NtkForEachCi( pNtk2, pObj, i )
     {
+        pName = Abc_ObjName(pObj);
         pObj->pCopy = Abc_NtkFindCi(pNtk1, Abc_ObjName(pObj));
         if ( pObj->pCopy == NULL )
+        {
             pObj->pCopy = Abc_NtkDupObj(pNtk1, pObj, 1);
+            nNewCis++;
+        }
     }
+    if ( nNewCis )
+        printf( "Warning: Procedure Abc_NtkAppend() added %d new CIs.\n", nNewCis );
     // add pNtk2 to pNtk1 while strashing
     if ( Abc_NtkIsLogic(pNtk2) )
         Abc_NtkStrashPerform( pNtk2, pNtk1, 1 );