Other changes to enable new features in the mapper (bug fix).

src/base/abc/abc.h

@@ -183,6 +183,9 @@ struct Abc_Ntk_t_
     int               nObjs;         // the number of live objs
     int               nConstrs;      // the number of constraints
     int               nRealPos;      // the number of real POs
+    float             nRealDelay;    // temporary mapping data
+    float             nRealLuts;     // temporary mapping data
+    float             nRealArea;     // temporary mapping data
     // the backup network and the step number
     Abc_Ntk_t *       pNetBackup;    // the pointer to the previous backup network
     int               iStep;         // the generation number for the given network
@@ -852,7 +855,9 @@ extern ABC_DLL Abc_Ntk_t *        Abc_NtkTopmost( Abc_Ntk_t * pNtk, int nLevels
 /*=== abcSweep.c ==========================================================*/
 extern ABC_DLL int                Abc_NtkSweep( Abc_Ntk_t * pNtk, int fVerbose );
 extern ABC_DLL int                Abc_NtkCleanup( Abc_Ntk_t * pNtk, int fVerbose );
+extern ABC_DLL int                Abc_NtkCleanupNodes( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, int fVerbose );
 extern ABC_DLL int                Abc_NtkCleanupSeq( Abc_Ntk_t * pNtk, int fLatchSweep, int fAutoSweep, int fVerbose );
+extern ABC_DLL int                Abc_NtkSweepBufsInvs( Abc_Ntk_t * pNtk, int fVerbose );
 /*=== abcTiming.c ==========================================================*/
 extern ABC_DLL Abc_Time_t *       Abc_NodeReadArrival( Abc_Obj_t * pNode );
 extern ABC_DLL Abc_Time_t *       Abc_NodeReadRequired( Abc_Obj_t * pNode );

src/base/abc/abcNetlist.c

@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "abc.h"
+#include "main.h"
 //#include "seq.h"
 
 ABC_NAMESPACE_IMPL_START
@@ -152,7 +153,8 @@ Abc_Ntk_t * Abc_NtkLogicToNetlist( Abc_Ntk_t * pNtk )
     assert( Abc_NtkIsLogic(pNtk) );
 
     // remove dangling nodes
-    Abc_NtkCleanup( pNtk, 0 );
+    if ( pNtk->vRealNodes == NULL )
+        Abc_NtkCleanup( pNtk, 0 );
 
     // make sure the CO names are unique
     Abc_NtkCheckUniqueCiNames( pNtk );
@@ -162,7 +164,8 @@ Abc_Ntk_t * Abc_NtkLogicToNetlist( Abc_Ntk_t * pNtk )
 //    assert( Abc_NtkLogicHasSimpleCos(pNtk) );
     if ( !Abc_NtkLogicHasSimpleCos(pNtk) )
     {
-        printf( "Abc_NtkLogicToNetlist() warning: The network is converted to have simple COs.\n" );
+        if ( !Abc_FrameReadFlag("silentmode") )
+            printf( "Abc_NtkLogicToNetlist() warning: The network is converted to have simple COs.\n" );
         Abc_NtkLogicMakeSimpleCos( pNtk, 0 );
     }
 
@@ -226,6 +229,7 @@ Abc_Ntk_t * Abc_NtkLogicToNetlist( Abc_Ntk_t * pNtk )
         pNtkNew->vRealNodes = Vec_IntAlloc( Vec_IntSize(pNtk->vRealNodes) );
         Abc_NtkForEachObjVec( pNtk->vRealNodes, pNtk, pObj, i )
             Vec_IntPush( pNtkNew->vRealNodes, Abc_ObjId(pObj->pCopy) );
+        assert( Vec_IntSize(pNtk->vRealNodes) == Vec_IntSize(pNtkNew->vRealNodes) );
     }
 
     // duplicate EXDC 

src/base/abc/abcNtk.c

@@ -109,9 +109,12 @@ Abc_Ntk_t * Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_
     fCopyNames = ( Type != ABC_NTK_NETLIST );
     // start the network
     pNtkNew = Abc_NtkAlloc( Type, Func, 1 );
-    pNtkNew->nConstrs = pNtk->nConstrs;
-    pNtkNew->nRealPos = pNtk->nRealPos;
-    pNtkNew->vRealPos = pNtk->vRealPos ? Vec_VecDup( pNtk->vRealPos ) : NULL;
+    pNtkNew->nConstrs   = pNtk->nConstrs;
+    pNtkNew->nRealPos   = pNtk->nRealPos;
+    pNtkNew->nRealDelay = pNtk->nRealDelay;
+    pNtkNew->nRealLuts  = pNtk->nRealLuts;
+    pNtkNew->nRealArea  = pNtk->nRealArea;
+    pNtkNew->vRealPos   = pNtk->vRealPos ? Vec_VecDup( pNtk->vRealPos ) : NULL;
     // duplicate the name and the spec
     pNtkNew->pName = Extra_UtilStrsav(pNtk->pName);
     pNtkNew->pSpec = Extra_UtilStrsav(pNtk->pSpec);
@@ -164,9 +167,12 @@ Abc_Ntk_t * Abc_NtkStartFromNoLatches( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc
     assert( Type != ABC_NTK_NETLIST );
     // start the network
     pNtkNew = Abc_NtkAlloc( Type, Func, 1 );
-    pNtkNew->nConstrs = pNtk->nConstrs;
-    pNtkNew->nRealPos = pNtk->nRealPos;
-    pNtkNew->vRealPos = pNtk->vRealPos ? Vec_VecDup( pNtk->vRealPos ) : NULL;
+    pNtkNew->nConstrs   = pNtk->nConstrs;
+    pNtkNew->nRealPos   = pNtk->nRealPos;
+    pNtkNew->nRealDelay = pNtk->nRealDelay;
+    pNtkNew->nRealLuts  = pNtk->nRealLuts;
+    pNtkNew->nRealArea  = pNtk->nRealArea;
+    pNtkNew->vRealPos   = pNtk->vRealPos ? Vec_VecDup( pNtk->vRealPos ) : NULL;
     // duplicate the name and the spec
     pNtkNew->pName = Extra_UtilStrsav(pNtk->pName);
     pNtkNew->pSpec = Extra_UtilStrsav(pNtk->pSpec);
@@ -357,6 +363,15 @@ Abc_Ntk_t * Abc_NtkDup( Abc_Ntk_t * pNtk )
                 Abc_ObjForEachFanin( pObj, pFanin, k )
                     Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy );
     }
+    // remap the real nodess
+    if ( pNtk->vRealNodes )
+    {
+        assert( pNtkNew->vRealNodes == NULL );
+        pNtkNew->vRealNodes = Vec_IntAlloc( Vec_IntSize(pNtk->vRealNodes) );
+        Abc_NtkForEachObjVec( pNtk->vRealNodes, pNtk, pObj, i )
+            Vec_IntPush( pNtkNew->vRealNodes, Abc_ObjId(pObj->pCopy) );
+        assert( Vec_IntSize(pNtk->vRealNodes) == Vec_IntSize(pNtkNew->vRealNodes) );
+    }
     // duplicate the EXDC Ntk
     if ( pNtk->pExdc )
         pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc );

src/base/abci/abc.c

@@ -3342,13 +3342,21 @@ int Abc_CommandSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
     int c;
+    int fSingle = 0;
+    int fVerbose = 0;
 
     // set defaults
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "svh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 's':
+            fSingle ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -3367,12 +3375,17 @@ int Abc_CommandSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
     // modify the current network
-    Abc_NtkSweep( pNtk, 0 );
+    if ( fSingle )
+        Abc_NtkSweepBufsInvs( pNtk, fVerbose );
+    else
+        Abc_NtkSweep( pNtk, fVerbose );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: sweep [-h]\n" );
+    Abc_Print( -2, "usage: sweep [-svh]\n" );
     Abc_Print( -2, "\t        removes dangling nodes; propagates constant, buffers, inverters\n" );
+    Abc_Print( -2, "\t-s    : toggle sweeping buffers/inverters only [default = %s]\n", fSingle? "yes": "no" );  
+    Abc_Print( -2, "\t-v    : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); 
     Abc_Print( -2, "\t-h    : print the command usage\n");
     return 1;
 }
@@ -13150,7 +13163,8 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
     // enable truth table computation if choices are selected
     if ( (c = Abc_NtkGetChoiceNum( pNtk )) )
     {
-        Abc_Print( 0, "Performing LUT mapping with %d choices.\n", c );
+        if ( !Abc_FrameReadFlag("silentmode") )
+            Abc_Print( 0, "Performing LUT mapping with %d choices.\n", c );
         pPars->fExpRed = 0;
     }
 
@@ -13243,7 +13257,8 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
             Abc_Print( -1, "Balancing before FPGA mapping has failed.\n" );
             return 1;
         }
-        Abc_Print( 1, "The network was strashed and balanced before FPGA mapping.\n" );
+        if ( !Abc_FrameReadFlag("silentmode") )
+            Abc_Print( 1, "The network was strashed and balanced before FPGA mapping.\n" );
         // get the new network
         pNtkRes = Abc_NtkIf( pNtk, pPars );
         if ( pNtkRes == NULL )

src/base/abci/abcIf.c

@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "abc.h"
+#include "main.h"
 #include "if.h"
 #include "kit.h"
 #include "aig.h"
@@ -332,7 +333,7 @@ Abc_Ntk_t * Abc_NtkFromIf( If_Man_t * pIfMan, Abc_Ntk_t * pNtk )
         Abc_NtkBddReorder( pNtkNew, 0 );
     // decouple the PO driver nodes to reduce the number of levels
     nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, !pIfMan->pPars->fUseBuffs );
-    if ( nDupGates && pIfMan->pPars->fVerbose )
+    if ( nDupGates && pIfMan->pPars->fVerbose && !Abc_FrameReadFlag("silentmode") )
     {
         if ( pIfMan->pPars->fUseBuffs )
             printf( "Added %d buffers/inverters to decouple the CO drivers.\n", nDupGates );
@@ -812,16 +813,19 @@ void Abc_NtkCollectPoDrivers( If_Man_t * p, Abc_Ntk_t * pNtk )
     int i, g, nGroups;
     if ( pNtk->nRealPos == 0 )
     {
-        printf( "PO drivers are not defined.\n" );
+        if ( !Abc_FrameReadFlag("silentmode") )
+            printf( "PO drivers are not defined.\n" );
         return;
     }
     if ( (Abc_NtkPoNum(pNtk) - pNtk->nRealPos) % 5 != 0 )
     {
-        printf( "PO drivers are not divisible by 5.\n" );
+        if ( !Abc_FrameReadFlag("silentmode") )
+            printf( "PO drivers are not divisible by 5.\n" );
         return;
     }
     nGroups = (Abc_NtkPoNum(pNtk) - pNtk->nRealPos) / 5;
-    printf( "Processing %d groups of PO drivers.\n", nGroups );
+    if ( !Abc_FrameReadFlag("silentmode") )
+        printf( "Processing %d groups of PO drivers.\n", nGroups );
     // mark the drivers (0 a   1 b   2 c   3 s   4 c)
     assert( p->pDriverCuts == NULL );
     p->pDriverCuts = ABC_CALLOC( Vec_Int_t *, If_ManObjNum(p) );
@@ -987,7 +991,9 @@ void Abc_NtkFreePoDrivers( If_Man_t * p, Abc_Ntk_t * pNtk )
     int i;
     if ( p->pDriverCuts == NULL )
         return;
-    printf( "Actual delay after mapping = %.2f\n", p->RequiredGlo );
+    pNtk->nRealDelay = p->RequiredGlo;
+    if ( !Abc_FrameReadFlag("silentmode") )
+        printf( "Actual delay after mapping = %.2f\n", p->RequiredGlo );
     assert( Abc_NtkPoNum(pNtk) == If_ManCoNum(p) - Abc_NtkLatchNum(pNtk) );
     // print the cut sizes of the drivers
     for ( i = pNtk->nRealPos; i <  Abc_NtkPoNum(pNtk); i += 5 )
@@ -1080,7 +1086,8 @@ void Abc_NtkRecreatePoDrivers( If_Man_t * p, Abc_Ntk_t * pNtkNew )
     float RealLutArea;
     if ( pNtkNew->vRealPos == NULL )
     {
-        printf( "Missing key information.\n" );
+        if ( !Abc_FrameReadFlag("silentmode") )
+            printf( "Missing key information.\n" );
         return;
     }
 
@@ -1088,7 +1095,7 @@ void Abc_NtkRecreatePoDrivers( If_Man_t * p, Abc_Ntk_t * pNtkNew )
     // create drivers
     vDrivers = Vec_PtrStart( pNtkNew->nRealPos );
     vDriverInvs = Vec_IntStart( pNtkNew->nRealPos );
-    pNtkNew->vRealNodes = Vec_IntAlloc( pNtkNew->nRealPos );
+    pNtkNew->vRealNodes = Vec_IntAlloc( Abc_NtkPoNum(pNtkNew) - pNtkNew->nRealPos );
     for ( i = pNtkNew->nRealPos; i < Abc_NtkPoNum(pNtkNew); i++ )
     {
         pObj = Abc_NtkPo( pNtkNew, i );
@@ -1130,12 +1137,16 @@ void Abc_NtkRecreatePoDrivers( If_Man_t * p, Abc_Ntk_t * pNtkNew )
             Vec_PtrPush( vFanins, pExor );
             Vec_PtrPush( vFanins, (Abc_Obj_t *)Vec_PtrEntry(vDrivers, numPo+2) ); 
             pNode = Abc_NtkCreateNodeExor( pNtkNew, vFanins );
+            // update pointers
             Vec_PtrWriteEntry( vDriversNew, numPo+3, pNode );
+            Vec_IntWriteEntry( pNtkNew->vRealNodes, numPo+3 - pNtkNew->nRealPos, Abc_ObjId(pNode) );
             // create MUX
             pNode = Abc_NtkCreateNodeMux( pNtkNew, pExor, 
                 (Abc_Obj_t *)Vec_PtrEntry(vDrivers, numPo+2), 
                 (Abc_Obj_t *)Vec_PtrEntry(vDrivers, numPo+(fCompl ? 0 : 1)) );
+            // update pointers
             Vec_PtrWriteEntry( vDriversNew, numPo+4, pNode );
+            Vec_IntWriteEntry( pNtkNew->vRealNodes, numPo+4 - pNtkNew->nRealPos, Abc_ObjId(pNode) );
         }
     }
     Vec_PtrFree( vFanins );
@@ -1147,15 +1158,31 @@ void Abc_NtkRecreatePoDrivers( If_Man_t * p, Abc_Ntk_t * pNtkNew )
     {
         pObj = Abc_NtkPo( pNtkNew, numPo+3 );
         Vec_IntWriteEntry( vNodeMap, Abc_ObjId( Abc_ObjFanin0(pObj) ), numPo+3 );
+
+        // update the PO pointer
+//        if ( Abc_ObjFaninC0(pObj) )
+//            Abc_ObjXorFaninC( pObj, 0 );
+//       Abc_ObjPatchFanin( pObj, Abc_ObjFanin0(pObj), Vec_PtrEntry(vDriversNew, numPo+3) );
+
         pObj = Abc_NtkPo( pNtkNew, numPo+4 );
         Vec_IntWriteEntry( vNodeMap, Abc_ObjId( Abc_ObjFanin0(pObj) ), numPo+4 );
+
+        // update the PO pointer
+//        if ( Abc_ObjFaninC0(pObj) )
+//            Abc_ObjXorFaninC( pObj, 0 );
+//        Abc_ObjPatchFanin( pObj, Abc_ObjFanin0(pObj), Vec_PtrEntry(vDriversNew, numPo+4) );
+
     }
 
     // replace logic
     Abc_NtkForEachObj( pNtkNew, pObj, i )
     {
+//        if ( Abc_ObjIsPo(pObj) )
+//            continue;
         Abc_ObjForEachFanin( pObj, pFanin, k )
         {
+            if ( !Abc_ObjIsNode(pFanin) || Abc_ObjFaninNum(pFanin) == 0 )
+                continue;
             numPo = Vec_IntEntry( vNodeMap, Abc_ObjId(pFanin) );
             if ( numPo == ~0 )
                 continue;
@@ -1171,14 +1198,24 @@ void Abc_NtkRecreatePoDrivers( If_Man_t * p, Abc_Ntk_t * pNtkNew )
                 Abc_ObjPatchFanin( pObj, pFanin, pFaninNew );
         }
     }    
+
+    // sweep
+    Abc_NtkCleanupNodes( pNtkNew, vDriversNew, 0 );
+
+    // make sure that all vDriversNew are still present
+    {
+        Abc_Obj_t * pObj;
+        int i;
+        Vec_PtrForEachEntry( Abc_Obj_t *, vDriversNew, pObj, i )
+            if ( pObj && Abc_ObjIsNone(pObj) )
+                assert( 0 );
+    }
+
     Vec_PtrFree( vDrivers );
     Vec_PtrFree( vDriversNew );
     Vec_IntFree( vNodeMap );
     Vec_IntFree( vDriverInvs );
 
-    // sweep
-    Abc_NtkCleanup( pNtkNew, 0 );
-
     // count non-trivial LUTs nodes
     nRealLuts   = -2 * Vec_VecSizeSize(pNtkNew->vRealPos);
     RealLutArea = -(p->pPars->pLutLib ? p->pPars->pLutLib->pLutAreas[2] + p->pPars->pLutLib->pLutAreas[3] : 2.0) * Vec_VecSizeSize(pNtkNew->vRealPos);
@@ -1188,7 +1225,10 @@ void Abc_NtkRecreatePoDrivers( If_Man_t * p, Abc_Ntk_t * pNtkNew )
             nRealLuts++;
             RealLutArea += p->pPars->pLutLib->pLutAreas[Abc_ObjFaninNum(pNode)];
         }
-    printf( "The number of real LUTs = %d.  Real LUT area = %.2f.\n", nRealLuts, RealLutArea );
+    if ( !Abc_FrameReadFlag("silentmode") )
+        printf( "The number of real LUTs = %d.  Real LUT area = %.2f.\n", nRealLuts, RealLutArea );
+    pNtkNew->nRealLuts = nRealLuts;
+    pNtkNew->nRealArea = RealLutArea;
 }
 
 ////////////////////////////////////////////////////////////////////////

src/base/abci/abcSweep.c

@@ -490,6 +490,40 @@ int Abc_NtkCleanup( Abc_Ntk_t * pNtk, int fVerbose )
 
 /**Function*************************************************************
 
+  Synopsis    [Removes dangling nodes.]
+
+  Description [Returns the number of nodes removed.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkCleanupNodes( Abc_Ntk_t * pNtk, Vec_Ptr_t * vRoots, int fVerbose )
+{
+    Vec_Ptr_t * vNodes, * vStarts;
+    Abc_Obj_t * pObj;
+    int i, Counter;
+    assert( Abc_NtkIsLogic(pNtk) );
+    // collect starting nodes into one array
+    vStarts = Vec_PtrAlloc( 1000 );
+    Abc_NtkForEachCo( pNtk, pObj, i )
+        Vec_PtrPush( vStarts, pObj );
+    Vec_PtrForEachEntry( Abc_Obj_t *, vRoots, pObj, i )
+        if ( pObj )
+            Vec_PtrPush( vStarts, pObj );
+    // mark the nodes reachable from the POs
+    vNodes = Abc_NtkDfsNodes( pNtk, (Abc_Obj_t **)Vec_PtrArray(vStarts), Vec_PtrSize(vStarts) );
+    Vec_PtrFree( vStarts );
+    Counter = Abc_NtkReduceNodes( pNtk, vNodes );
+    if ( fVerbose )
+        printf( "Cleanup removed %d dangling nodes.\n", Counter );
+    Vec_PtrFree( vNodes );
+    return Counter;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Preserves the nodes collected in the array.]
 
   Description [Returns the number of nodes removed.]
@@ -945,6 +979,80 @@ int Abc_NtkCleanupSeq( Abc_Ntk_t * pNtk, int fLatchSweep, int fAutoSweep, int fV
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Sweep to remove buffers and inverters.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkSweepBufsInvs( Abc_Ntk_t * pNtk, int fVerbose )
+{
+    Hop_Man_t * pMan;
+    Abc_Obj_t * pObj, * pFanin;
+    int i, k, fChanges = 1, Counter = 0;
+    assert( Abc_NtkIsLogic(pNtk) ); 
+    // convert network to BDD representation
+    if ( !Abc_NtkToAig(pNtk) )
+    {
+        fprintf( stdout, "Converting to SOP has failed.\n" );
+        return 1;
+    }
+    // get AIG manager
+    pMan = (Hop_Man_t *)pNtk->pManFunc;
+    // label selected nodes
+    Abc_NtkIncrementTravId( pNtk );
+    if ( pNtk->vRealNodes )
+    {
+        Abc_Obj_t * pObj;
+        assert( Vec_IntSize(pNtk->vRealNodes) == Abc_NtkPoNum(pNtk) - pNtk->nRealPos );
+        Abc_NtkForEachObjVec( pNtk->vRealNodes, pNtk, pObj, i )
+            Abc_NodeSetTravIdCurrent( pObj );
+    }
+    // iterate till no improvement
+    while ( fChanges )
+    {
+        fChanges = 0;
+        Abc_NtkForEachObj( pNtk, pObj, i )
+        {
+            Abc_ObjForEachFanin( pObj, pFanin, k )
+            {
+                // do not eliminate marked fanins
+                if ( Abc_NodeIsTravIdCurrent(pFanin) )
+                    continue;
+                // do not eliminate constant nodes
+                if ( !Abc_ObjIsNode(pFanin) || Abc_ObjFaninNum(pFanin) != 1 )
+                    continue;
+                // do not eliminate inverters into COs
+                if ( Abc_ObjIsCo(pObj) && Abc_NodeIsInv(pFanin) )
+                    continue;
+                // do not eliminate buffers connecting PIs and POs 
+//                if ( Abc_ObjIsCo(pObj) && Abc_ObjIsCi(Abc_ObjFanin0(pFanin)) )
+//                    continue;
+                fChanges = 1;
+                Counter++;
+                // update function of the node
+                if ( Abc_NodeIsInv(pFanin) )
+                    pObj->pData = Hop_Compose( pMan, (Hop_Obj_t *)pObj->pData, Hop_Not(Hop_IthVar(pMan, k)), k );
+                // update the fanin
+                Abc_ObjPatchFanin( pObj, pFanin, Abc_ObjFanin0(pFanin) );
+                if ( Abc_ObjFanoutNum(pFanin) == 0 )
+                    Abc_NtkDeleteObj(pFanin);            
+            }
+        }
+    }
+    if ( fVerbose )
+        printf( "Removed %d single input nodes.\n", Counter );
+    return Counter;
+}
+
+
+
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///

src/base/io/ioWriteBlif.c

@@ -387,8 +387,10 @@ void Io_NtkWritePos( FILE * pFile, Abc_Ntk_t * pNtk, int fWriteLatches )
     if ( pNtk->vRealNodes )
     {
         Abc_Obj_t * pObj;
+        int Num1 = Vec_IntSize(pNtk->vRealNodes);
+        int Num2 = Abc_NtkPoNum(pNtk)-pNtk->nRealPos;
         fprintf( pFile, "\n\n" );
-        assert( pNtk->nRealPos >= 0 );
+        assert( Vec_IntSize(pNtk->vRealNodes) == Abc_NtkPoNum(pNtk)-pNtk->nRealPos );
         Abc_NtkForEachObjVec( pNtk->vRealNodes, pNtk, pObj, i )
             fprintf( pFile, "#INFO %s %s\n", 
                 Abc_ObjName(Abc_ObjFanin0(Abc_NtkPo(pNtk, pNtk->nRealPos+i))),