Version abc51127

src/base/abc/abcCheck.c

@@ -20,6 +20,7 @@
 
 #include "abc.h"
 #include "main.h"
+#include "seq.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -151,6 +152,8 @@ bool Abc_NtkDoCheck( Abc_Ntk_t * pNtk )
     {
         if ( Abc_NtkIsStrash(pNtk) ) 
             Abc_AigCheck( pNtk->pManFunc );
+        else
+            Abc_NtkSeqCheck( pNtk );
     }
     else
     {

src/base/abc/abcDfs.c

@@ -464,6 +464,9 @@ int Abc_NtkGetLevelNum( Abc_Ntk_t * pNtk )
     int i, LevelsMax;
     // set the traversal ID for this traversal
     Abc_NtkIncrementTravId( pNtk );
+    // set the CI levels to zero
+    Abc_NtkForEachCi( pNtk, pNode, i )
+        pNode->Level = 0;
     // perform the traversal
     LevelsMax = 0;
     Abc_NtkForEachNode( pNtk, pNode, i )
@@ -508,7 +511,8 @@ int Abc_NtkGetLevelNum_rec( Abc_Obj_t * pNode )
         if ( pNode->Level < (unsigned)Level )
             pNode->Level = Level;
     }
-    pNode->Level++;
+    if ( Abc_ObjFaninNum(pNode) > 0 )
+        pNode->Level++;
     return pNode->Level;
 }
 

src/base/abc/abcNtk.c

@@ -330,6 +330,9 @@ Abc_Ntk_t * Abc_NtkDup( Abc_Ntk_t * pNtk )
         Abc_AigForEachAnd( pNtk, pObj, i )
             if ( pObj->pData )
                 pObj->pCopy->pData = ((Abc_Obj_t *)pObj->pData)->pCopy;
+        // copy the cutset
+        Abc_SeqForEachCutsetNode( pNtk, pObj, i )
+            Vec_PtrPush( pNtkNew->vCutSet, pObj->pCopy );
     }
     else
     {

src/base/abc/abcShow.c

@@ -112,7 +112,7 @@ void Abc_NtkShowAig( Abc_Ntk_t * pNtk )
     Abc_NtkForEachObj( pNtk, pNode, i )
         Vec_PtrPush( vNodes, pNode );
     // write the DOT file
-    Io_WriteDot( pNtk, vNodes, NULL, FileNameDot, 0 );
+    Io_WriteDotAig( pNtk, vNodes, NULL, FileNameDot, 0 );
     Vec_PtrFree( vNodes );
 
     // visualize the file 
@@ -168,7 +168,7 @@ void Abc_NtkShowMulti( Abc_Ntk_t * pNtk )
         Vec_PtrPush( vNodes, pNode );
 
     // write the DOT file
-    Io_WriteDot( pNtk, vNodes, NULL, FileNameDot, 1 );
+    Io_WriteDotAig( pNtk, vNodes, NULL, FileNameDot, 1 );
     Vec_PtrFree( vNodes );
 
     // undo the supergates
@@ -232,7 +232,7 @@ void Abc_NodeShowCut( Abc_Obj_t * pNode, int nNodeSizeMax, int nConeSizeMax )
     // add the root node to the cone (for visualization)
     Vec_PtrPush( vCutSmall, pNode );
     // write the DOT file
-    Io_WriteDot( pNode->pNtk, vInside, vCutSmall, FileNameDot, 0 );
+    Io_WriteDotAig( pNode->pNtk, vInside, vCutSmall, FileNameDot, 0 );
     // stop the cut computation manager
     Abc_NtkManCutStop( p );
 
@@ -240,6 +240,48 @@ void Abc_NodeShowCut( Abc_Obj_t * pNode, int nNodeSizeMax, int nConeSizeMax )
     Abc_ShowFile( FileNameDot );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Visualizes AIG with choices.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkShow( Abc_Ntk_t * pNtk, int fGateNames )
+{
+    FILE * pFile;
+    Abc_Obj_t * pNode;
+    Vec_Ptr_t * vNodes;
+    char FileNameDot[200];
+    int i;
+
+    assert( !Abc_NtkHasAig(pNtk) );
+    // create the file name
+    Abc_ShowGetFileName( pNtk->pName, FileNameDot );
+    // check that the file can be opened
+    if ( (pFile = fopen( FileNameDot, "w" )) == NULL )
+    {
+        fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", FileNameDot );
+        return;
+    }
+    fclose( pFile );
+
+    // collect all nodes in the network
+    vNodes = Vec_PtrAlloc( 100 );
+    Abc_NtkForEachObj( pNtk, pNode, i )
+        Vec_PtrPush( vNodes, pNode );
+    // write the DOT file
+    Io_WriteDotNtk( pNtk, vNodes, NULL, FileNameDot, fGateNames );
+    Vec_PtrFree( vNodes );
+
+    // visualize the file 
+    Abc_ShowFile( FileNameDot );
+}
+
 
 /**Function*************************************************************
 

src/base/abci/abcPrint.c

@@ -20,6 +20,8 @@
 
 #include "abc.h"
 #include "dec.h"
+#include "main.h"
+#include "mio.h"
 #include "seq.h"
 
 ////////////////////////////////////////////////////////////////////////
@@ -524,6 +526,96 @@ void Abc_NodePrintKMap( Abc_Obj_t * pNode, int fUseRealNames )
 
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Prints statistics about gates used in the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkPrintGates( Abc_Ntk_t * pNtk, int fUseLibrary )
+{
+    Abc_Obj_t * pObj;
+    int fHasBdds, i;
+    int CountConst, CountBuf, CountInv, CountAnd, CountOr, CountOther, CounterTotal;
+    char * pSop;
+
+    if ( fUseLibrary && Abc_NtkHasMapping(pNtk) )
+    {
+        stmm_table * tTable;
+        stmm_generator * gen;
+        char * pName;
+        int * pCounter, Counter;
+        double Area, AreaTotal;
+
+        // count the gates by name
+        CounterTotal = 0;
+        tTable = stmm_init_table(strcmp, stmm_strhash);
+        Abc_NtkForEachNode( pNtk, pObj, i )
+        {
+            if ( i == 0 ) continue;
+            if ( !stmm_find_or_add( tTable, Mio_GateReadName(pObj->pData), (char ***)&pCounter ) )
+                *pCounter = 0;
+            (*pCounter)++;
+            CounterTotal++;
+        }
+        // print the gates
+        AreaTotal = Abc_NtkGetMappedArea(pNtk);
+        stmm_foreach_item( tTable, gen, (char **)&pName, (char **)&Counter )
+        {
+            Area = Counter * Mio_GateReadArea(Mio_LibraryReadGateByName(pNtk->pManFunc,pName));
+            printf( "%-12s = %8d   %10.2f    %6.2f %%\n", pName, Counter, Area, 100.0 * Area / AreaTotal );
+        }
+        printf( "%-12s = %8d   %10.2f    %6.2f %%\n", "TOTAL", CounterTotal, AreaTotal, 100.0 );
+        stmm_free_table( tTable );
+        return;
+    }
+
+    // transform logic functions from BDD to SOP
+    if ( fHasBdds = Abc_NtkIsBddLogic(pNtk) )
+        Abc_NtkBddToSop(pNtk);
+
+    // get hold of the SOP of the node
+    CountConst = CountBuf = CountInv = CountAnd = CountOr = CountOther = CounterTotal = 0;
+    Abc_NtkForEachNode( pNtk, pObj, i )
+    {
+        if ( i == 0 ) continue;
+        if ( Abc_NtkHasMapping(pNtk) )
+            pSop = Mio_GateReadSop(pObj->pData);
+        else
+            pSop = pObj->pData;
+        // collect the stats
+        if ( Abc_SopIsConst0(pSop) || Abc_SopIsConst1(pSop) )
+            CountConst++;
+        else if ( Abc_SopIsBuf(pSop) )
+            CountBuf++;
+        else if ( Abc_SopIsInv(pSop) )
+            CountInv++;
+        else if ( !Abc_SopIsComplement(pSop) && Abc_SopIsAndType(pSop) ||  Abc_SopIsComplement(pSop) && Abc_SopIsOrType(pSop) )
+            CountAnd++;
+        else if (  Abc_SopIsComplement(pSop) && Abc_SopIsAndType(pSop) || !Abc_SopIsComplement(pSop) && Abc_SopIsOrType(pSop) )
+            CountOr++;
+        else
+            CountOther++;
+        CounterTotal++;
+    }
+    printf( "Const        = %8d    %6.2f %%\n", CountConst  ,  100.0 * CountConst   / CounterTotal );
+    printf( "Buffer       = %8d    %6.2f %%\n", CountBuf    ,  100.0 * CountBuf     / CounterTotal );
+    printf( "Inverter     = %8d    %6.2f %%\n", CountInv    ,  100.0 * CountInv     / CounterTotal );
+    printf( "And          = %8d    %6.2f %%\n", CountAnd    ,  100.0 * CountAnd     / CounterTotal );
+    printf( "Or           = %8d    %6.2f %%\n", CountOr     ,  100.0 * CountOr      / CounterTotal );
+    printf( "Other        = %8d    %6.2f %%\n", CountOther  ,  100.0 * CountOther   / CounterTotal );
+    printf( "TOTAL        = %8d    %6.2f %%\n", CounterTotal,  100.0 * CounterTotal / CounterTotal );
+
+    // convert the network back into BDDs if this is how it was
+    if ( fHasBdds )
+        Abc_NtkSopToBdd(pNtk);
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/base/abci/abcSweep.c

@@ -449,6 +449,7 @@ int Abc_NtkCleanup( Abc_Ntk_t * pNtk, int fVerbose )
     Vec_Ptr_t * vNodes;
     Abc_Obj_t * pNode;
     int i, Counter;
+    assert( !Abc_NtkHasAig(pNtk) );
     // mark the nodes reachable from the POs
     vNodes = Abc_NtkDfs( pNtk, 0 );
     for ( i = 0; i < vNodes->nSize; i++ )
@@ -458,7 +459,7 @@ int Abc_NtkCleanup( Abc_Ntk_t * pNtk, int fVerbose )
     }
     Vec_PtrFree( vNodes );
     // if it is an AIG, also mark the constant 1 node
-    if ( Abc_NtkIsStrash(pNtk) )
+    if ( Abc_NtkConst1(pNtk) )
         Abc_NtkConst1(pNtk)->fMarkA = 1;
     // remove the non-marked nodes
     Counter = 0;
@@ -514,7 +515,7 @@ int Abc_NtkSweep( Abc_Ntk_t * pNtk, int fVerbose )
     {
         // sweep constants and single-input nodes
         Abc_NtkForEachNode( pNtk, pNode, i )
-            if ( Abc_ObjFaninNum(pNode) < 2 )
+            if ( i && Abc_ObjFaninNum(pNode) < 2 )
                 Abc_NodeSweep( pNode, fVerbose );
         // make the network minimum base
         Abc_NtkRemoveDupFanins(pNtk);

src/base/io/io.c

@@ -1101,7 +1101,7 @@ int IoCommandWriteDot( Abc_Frame_t * pAbc, int argc, char **argv )
     FileName = argv[util_optind];
     // write the file
     vNodes = Abc_NtkCollectObjects( pAbc->pNtkCur );
-    Io_WriteDot( pAbc->pNtkCur, vNodes, NULL, FileName, 0 );
+    Io_WriteDotAig( pAbc->pNtkCur, vNodes, NULL, FileName, 0 );
     Vec_PtrFree( vNodes );
     return 0;
 

src/base/io/io.h

@@ -80,7 +80,8 @@ extern int                Io_WriteBench( Abc_Ntk_t * pNtk, char * FileName );
 /*=== abcWriteCnf.c ==========================================================*/
 extern int                Io_WriteCnf( Abc_Ntk_t * pNtk, char * FileName );
 /*=== abcWriteDot.c ==========================================================*/
-extern void               Io_WriteDot( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow, char * pFileName, int fMulti );
+extern void               Io_WriteDotAig( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow, char * pFileName, int fMulti );
+extern void               Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow, char * pFileName, int fGateNames );
 /*=== abcWriteEqn.c ==========================================================*/
 extern void               Io_WriteEqn( Abc_Ntk_t * pNtk, char * pFileName );
 /*=== abcWriteGml.c ==========================================================*/

src/base/seq/seq.h

@@ -44,7 +44,7 @@ typedef struct Abc_Seq_t_  Abc_Seq_t;
 ////////////////////////////////////////////////////////////////////////
 
 /*=== seqAigCore.c ===========================================================*/
-extern void            Seq_NtkSeqRetimeDelay( Abc_Ntk_t * pNtk, int fInitial, int fVerbose );
+extern void            Seq_NtkSeqRetimeDelay( Abc_Ntk_t * pNtk, int nMaxIters, int fInitial, int fVerbose );
 extern void            Seq_NtkSeqRetimeForward( Abc_Ntk_t * pNtk, int fInitial, int fVerbose );
 extern void            Seq_NtkSeqRetimeBackward( Abc_Ntk_t * pNtk, int fInitial, int fVerbose );
 /*=== seqFpgaCore.c ===============================================================*/
@@ -52,7 +52,7 @@ extern Abc_Ntk_t *     Seq_NtkFpgaMapRetime( Abc_Ntk_t * pNtk, int nMaxIters, in
 /*=== seqMapCore.c ===============================================================*/
 extern Abc_Ntk_t *     Seq_MapRetime( Abc_Ntk_t * pNtk, int nMaxIters, int fVerbose );
 /*=== seqRetCore.c ===========================================================*/
-extern Abc_Ntk_t *     Seq_NtkRetime( Abc_Ntk_t * pNtk, int nMaxIters, int fVerbose );
+extern Abc_Ntk_t *     Seq_NtkRetime( Abc_Ntk_t * pNtk, int nMaxIters, int fInitial, int fVerbose );
 /*=== seqLatch.c ===============================================================*/
 extern void            Seq_NodeDupLats( Abc_Obj_t * pObjNew, Abc_Obj_t * pObj, int Edge );
 extern int             Seq_NodeCompareLats( Abc_Obj_t * pObj1, int Edge1, Abc_Obj_t * pObj2, int Edge2 );
@@ -63,10 +63,12 @@ extern void            Seq_Delete( Abc_Seq_t * p );
 /*=== abcSeq.c ===============================================================*/
 extern Abc_Ntk_t *     Abc_NtkAigToSeq( Abc_Ntk_t * pNtk );
 extern Abc_Ntk_t *     Abc_NtkSeqToLogicSop( Abc_Ntk_t * pNtk );
+extern bool            Abc_NtkSeqCheck( Abc_Ntk_t * pNtk ); 
 /*=== seqShare.c =============================================================*/
 extern void            Seq_NtkShareFanouts( Abc_Ntk_t * pNtk );
 extern void            Seq_NtkShareLatches( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk );
 extern void            Seq_NtkShareLatchesFpga( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, Vec_Ptr_t * vMapAnds );
+extern void            Seq_NtkShareLatchesClean( Abc_Ntk_t * pNtk );
 /*=== seqUtil.c ==============================================================*/
 extern char *          Seq_ObjFaninGetInitPrintable( Abc_Obj_t * pObj, int Edge );
 extern void            Seq_NtkLatchSetValues( Abc_Ntk_t * pNtk, Abc_InitType_t Init );

src/base/seq/seqAigCore.c

@@ -65,13 +65,14 @@ static void        Abc_ObjRetimeBackwardTry( Abc_Obj_t * pObj, int nLatches );
   SeeAlso     []
 
 ***********************************************************************/
-void Seq_NtkSeqRetimeDelay( Abc_Ntk_t * pNtk, int fInitial, int fVerbose )
+void Seq_NtkSeqRetimeDelay( Abc_Ntk_t * pNtk, int nMaxIters, int fInitial, int fVerbose )
 {
     Abc_Seq_t * p = pNtk->pManFunc;
     int RetValue;
     if ( !fInitial )
         Seq_NtkLatchSetValues( pNtk, ABC_INIT_DC );
     // get the retiming lags
+    p->nMaxIters = nMaxIters;
     Seq_AigRetimeDelayLags( pNtk, fVerbose );
     // implement this retiming
     RetValue = Seq_NtkImplementRetiming( pNtk, p->vLags, fVerbose );
@@ -490,31 +491,33 @@ int Abc_ObjRetimeBackward( Abc_Obj_t * pObj, Abc_Ntk_t * pNtkNew, stmm_table * t
         {
             Edge = 0;
             Value = Seq_NodeDeleteLast( pFanout, Edge );
-            if ( Value != ABC_INIT_NONE )
-                continue;
-            // value is unknown, remove it from the table
-            RetEdge.iNode  = pFanout->Id;
-            RetEdge.iEdge  = Edge;
-            RetEdge.iLatch = Seq_ObjFaninL( pFanout, Edge ); // after edge is removed
-            if ( !stmm_delete( tTable, (char **)&RetEdge, (char **)&pFanoutNew ) )
-                assert( 0 );
-            // create the fanout of the AND gate
-            Abc_ObjAddFanin( pFanoutNew, pNodeNew );
+            if ( Value == ABC_INIT_NONE )
+            {
+                // value is unknown, remove it from the table
+                RetEdge.iNode  = pFanout->Id;
+                RetEdge.iEdge  = Edge;
+                RetEdge.iLatch = Seq_ObjFaninL( pFanout, Edge ); // after edge is removed
+                if ( !stmm_delete( tTable, (char **)&RetEdge, (char **)&pFanoutNew ) )
+                    assert( 0 );
+                // create the fanout of the AND gate
+                Abc_ObjAddFanin( pFanoutNew, pNodeNew );
+            }
         }
         if ( Abc_ObjFaninId1(pFanout) == pObj->Id )
         {
             Edge = 1;
             Value = Seq_NodeDeleteLast( pFanout, Edge );
-            if ( Value != ABC_INIT_NONE )
-                continue;
-            // value is unknown, remove it from the table
-            RetEdge.iNode  = pFanout->Id;
-            RetEdge.iEdge  = Edge;
-            RetEdge.iLatch = Seq_ObjFaninL( pFanout, Edge ); // after edge is removed
-            if ( !stmm_delete( tTable, (char **)&RetEdge, (char **)&pFanoutNew ) )
-                assert( 0 );
-            // create the fanout of the AND gate
-            Abc_ObjAddFanin( pFanoutNew, pNodeNew );
+            if ( Value == ABC_INIT_NONE )
+            {
+                // value is unknown, remove it from the table
+                RetEdge.iNode  = pFanout->Id;
+                RetEdge.iEdge  = Edge;
+                RetEdge.iLatch = Seq_ObjFaninL( pFanout, Edge ); // after edge is removed
+                if ( !stmm_delete( tTable, (char **)&RetEdge, (char **)&pFanoutNew ) )
+                    assert( 0 );
+                // create the fanout of the AND gate
+                Abc_ObjAddFanin( pFanoutNew, pNodeNew );
+            }
         }
     }
     // clean the label

src/base/seq/seqCreate.c

@@ -164,7 +164,7 @@ Abc_Ntk_t * Abc_NtkAigToSeq( Abc_Ntk_t * pNtk )
     Seq_NtkLatchGetEqualFaninNum( pNtkNew );
 
     // copy EXDC and check correctness
-    if ( pNtkNew->pExdc )
+    if ( pNtk->pExdc )
         fprintf( stdout, "Warning: EXDC is not copied when converting to sequential AIG.\n" );
     if ( !Abc_NtkCheck( pNtkNew ) )
         fprintf( stdout, "Abc_NtkAigToSeq(): Network check has failed.\n" );
@@ -292,6 +292,8 @@ Abc_Ntk_t * Abc_NtkSeqToLogicSop( Abc_Ntk_t * pNtk )
         pFaninNew = Abc_ObjNotCond( pFaninNew, Abc_ObjFaninC0(pObj) );
         Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
     }
+    // clean the latch pointers
+    Seq_NtkShareLatchesClean( pNtk );
 
     // add the latches and their names
     Abc_NtkAddDummyLatchNames( pNtkNew );
@@ -408,6 +410,73 @@ Abc_Obj_t * Abc_NodeSeqToLogic( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pFanin, Seq_Lat
     return pLatch;    
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Makes sure that every node in the table is in the network and vice versa.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+bool Abc_NtkSeqCheck( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj;
+    int i, nFanins;
+    Abc_NtkForEachNode( pNtk, pObj, i )
+    {
+        nFanins = Abc_ObjFaninNum(pObj);
+        if ( nFanins == 0 )
+        {
+            if ( pObj != Abc_NtkConst1(pNtk) )
+            {
+                printf( "Abc_SeqCheck: The AIG has non-standard constant nodes.\n" );
+                return 0;
+            }
+            continue;
+        }
+        if ( nFanins == 1 )
+        {
+            printf( "Abc_SeqCheck: The AIG has single input nodes.\n" );
+            return 0;
+        }
+        if ( nFanins > 2 )
+        {
+            printf( "Abc_SeqCheck: The AIG has non-standard nodes.\n" );
+            return 0;
+        }
+    }
+    // check the correctness of the internal representation of the initial states
+    Abc_NtkForEachObj( pNtk, pObj, i )
+    {
+        nFanins = Abc_ObjFaninNum(pObj);
+        if ( nFanins == 0 )
+            continue;
+        if ( nFanins == 1 )
+        {
+            if ( Seq_NodeCountLats(pObj, 0) != Seq_ObjFaninL0(pObj) )
+            {
+                printf( "Abc_SeqCheck: Node %d has mismatch in the number of latches.\n", Abc_ObjName(pObj) );
+                return 0;
+            }
+        }
+        // look at both inputs
+        if ( Seq_NodeCountLats(pObj, 0) != Seq_ObjFaninL0(pObj) )
+        {
+            printf( "Abc_SeqCheck: The first fanin of node %d has mismatch in the number of latches.\n", Abc_ObjName(pObj) );
+            return 0;
+        }
+        if ( Seq_NodeCountLats(pObj, 1) != Seq_ObjFaninL1(pObj) )
+        {
+            printf( "Abc_SeqCheck: The second fanin of node %d has mismatch in the number of latches.\n", Abc_ObjName(pObj) );
+            return 0;
+        }
+    }
+    return 1;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/base/seq/seqInt.h

@@ -195,7 +195,8 @@ static inline void           Seq_NodeRecycleLat( Abc_Obj_t * pObj, Seq_Lat_t * p
 static inline Seq_Lat_t *    Seq_NodeGetLatFirst( Abc_Obj_t * pObj, int Edge )               { return Seq_NodeGetRing(pObj, Edge);                      }
 static inline Seq_Lat_t *    Seq_NodeGetLatLast( Abc_Obj_t * pObj, int Edge )                { return Seq_LatPrev( Seq_NodeGetRing(pObj, Edge) );       }
 static inline Seq_Lat_t *    Seq_NodeGetLat( Abc_Obj_t * pObj, int Edge, int iLat )          { int c; Seq_Lat_t * pLat = Seq_NodeGetRing(pObj, Edge); for ( c = 0; c != iLat; c++ ) pLat = pLat->pNext; return pLat; }
-static inline int            Seq_NodeCountLats( Abc_Obj_t * pObj, int Edge )                 { int c; Seq_Lat_t * pLat, * pRing = Seq_NodeGetRing(pObj, Edge); if ( pRing == NULL ) return 0; for ( c = 0, pLat = pRing; !c || pLat != pRing; c++ )      pLat = pLat->pNext; return c; }
+static inline int            Seq_NodeCountLats( Abc_Obj_t * pObj, int Edge )                 { int c; Seq_Lat_t * pLat, * pRing = Seq_NodeGetRing(pObj, Edge); if ( pRing == NULL ) return 0; for ( c = 0, pLat = pRing; !c || pLat != pRing; c++ )  pLat = pLat->pNext; return c; }
+static inline void           Seq_NodeCleanLats( Abc_Obj_t * pObj, int Edge )                 { int c; Seq_Lat_t * pLat, * pRing = Seq_NodeGetRing(pObj, Edge); if ( pRing == NULL ) return  ; for ( c = 0, pLat = pRing; !c || pLat != pRing; c++ )  pLat->pLatch = NULL, pLat = pLat->pNext; return;  }
 
 // getting/setting initial states of the latches
 static inline Abc_InitType_t Seq_NodeGetInitOne( Abc_Obj_t * pObj, int Edge, int iLat )      { return Seq_LatInit( Seq_NodeGetLat(pObj, Edge, iLat) );  }

src/base/seq/seqLatch.c

@@ -61,6 +61,7 @@ void Seq_NodeInsertFirst( Abc_Obj_t * pObj, int Edge, Abc_InitType_t Init )
     }
     Seq_LatSetInit( pLat, Init );
     Seq_ObjAddFaninL( pObj, Edge, 1 );
+    assert( pLat->pLatch == NULL );
 }
 
 /**Function*************************************************************

src/base/seq/seqMapIter.c

@@ -207,8 +207,8 @@ int Seq_MapRetimeForPeriod( Abc_Ntk_t * pNtk, float Fi, int fVerbose )
     char * pReason = "";
 
     // set l-values of all nodes to be minus infinity
-    Vec_IntFill( p->vLValues,  p->nSize, -ABC_INFINITY );
-    Vec_IntFill( p->vLValuesN, p->nSize, -ABC_INFINITY );
+    Vec_IntFill( p->vLValues,  p->nSize, Abc_Float2Int( (float)-ABC_INFINITY ) );
+    Vec_IntFill( p->vLValuesN, p->nSize, Abc_Float2Int( (float)-ABC_INFINITY ) );
     Vec_StrFill( p->vUses,     p->nSize, 0             );
 
     // set l-values of constants and PIs

src/base/seq/seqRetIter.c

@@ -76,7 +76,7 @@ void Seq_NtkRetimeDelayLags( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtk, int fVerbose
             }
         }
         // get the upper bound on the clock period
-        FiMax = Delta * (2 + Seq_NtkLevelMax(pNtk));
+        FiMax = Delta * 2 + Abc_NtkDelayTrace(pNtkOld);
         Delta /= 2;
     }
     else
@@ -95,14 +95,24 @@ void Seq_NtkRetimeDelayLags( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtk, int fVerbose
     RetValue = Seq_NtkMappingForPeriod( pNtk, FiBest, fVerbose );
     assert( RetValue );
 
-    // write the retiming lags for both phases of each node
+    // experiment by adding an epsilon to all LValues
+//    Vec_PtrForEachEntry( p->vMapAnds, pNode, i )
+//        Seq_NodeSetLValueP( pNode, Seq_NodeGetLValueP(pNode) - p->fEpsilon );
+
+    // save the retiming lags
+    // mark the nodes
+    Vec_PtrForEachEntry( p->vMapAnds, pNode, i )
+        pNode->fMarkA = 1;
+    // process the nodes
     Vec_StrFill( p->vLags,  p->nSize, 0 );
     Vec_PtrForEachEntry( p->vMapAnds, pNode, i )
     {
         NodeLag = Seq_NodeComputeLagFloat( Seq_NodeGetLValueP(pNode), FiBest );
-//        Seq_NodeSetLag( pNode, NodeLag );
         Seq_NodeRetimeSetLag_rec( pNode, NodeLag );
     }
+    // unmark the nodes
+    Vec_PtrForEachEntry( p->vMapAnds, pNode, i )
+        pNode->fMarkA = 0;
 
     // print the result
     if ( fVerbose )
@@ -153,7 +163,7 @@ int Seq_NtkMappingForPeriod( Abc_Ntk_t * pNtk, float Fi, int fVerbose )
     char * pReason = "";
 
     // set l-values of all nodes to be minus infinity
-    Vec_IntFill( p->vLValues,  p->nSize, -ABC_INFINITY );
+    Vec_IntFill( p->vLValues,  p->nSize, Abc_Float2Int( (float)-ABC_INFINITY ) );
 
     // set l-values of constants and PIs
     pObj = Abc_NtkObj( pNtk, 0 );
@@ -268,11 +278,18 @@ int Seq_NtkNodeUpdateLValue( Abc_Obj_t * pObj, float Fi, Vec_Ptr_t * vLeaves, Ve
 ***********************************************************************/
 void Seq_NodeRetimeSetLag_rec( Abc_Obj_t * pNode, char Lag )
 {
-    if ( pNode->pCopy )
+    Abc_Obj_t * pFanin;
+    if ( !Abc_NodeIsAigAnd(pNode) )
         return;
-    Seq_NodeRetimeSetLag_rec( Abc_ObjFanin0(pNode), Lag );
-    Seq_NodeRetimeSetLag_rec( Abc_ObjFanin1(pNode), Lag );
     Seq_NodeSetLag( pNode, Lag );
+    // consider the first fanin
+    pFanin = Abc_ObjFanin0(pNode);
+    if ( pFanin->fMarkA == 0 ) // internal node
+        Seq_NodeRetimeSetLag_rec( pFanin, Lag );
+    // consider the second fanin
+    pFanin = Abc_ObjFanin1(pNode);
+    if ( pFanin->fMarkA == 0 ) // internal node
+        Seq_NodeRetimeSetLag_rec( pFanin, Lag );
 }
 
 

src/base/seq/seqShare.c

@@ -342,6 +342,31 @@ void Seq_NtkShareLatchesFpga( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, Vec_Ptr_t *
     Vec_PtrShrink( vMapAnds, nOldNodes );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Clean the latches after sharing them.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Seq_NtkShareLatchesClean( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj;
+    int i;
+    assert( Abc_NtkIsSeq( pNtk ) );
+    Abc_AigForEachAnd( pNtk, pObj, i )
+    {
+        Seq_NodeCleanLats( pObj, 0 );
+        Seq_NodeCleanLats( pObj, 1 );
+    }
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        Seq_NodeCleanLats( pObj, 0 );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/map/fpga/fpgaCore.c

@@ -85,7 +85,7 @@ int Fpga_Mapping( Fpga_Man_t * p )
   It iterates the loop, in which the required times are computed and
   the mapping is updated. It is conceptually similar to the paper: 
   V. Manohararajah, S. D. Brown, Z. G. Vranesic, Heuristics for area 
-  minimization in LUT-based FGPA technology mapping. Proc. IWLS '04.]
+  minimization in LUT-based FPGA technology mapping. Proc. IWLS '04.]
                
   SideEffects []