Version abc80502

src/aig/aig/aigDfs.c

@@ -448,6 +448,13 @@ int Aig_ManChoiceLevel( Aig_Man_t * p )
         if ( LevelMax < Aig_ObjLevel(pObj) )
             LevelMax = Aig_ObjLevel(pObj);
     }
+    // account for dangling boxes
+    Aig_ManForEachPi( p, pObj, i )
+    {
+        Aig_ManChoiceLevel_rec( p, pObj );
+        if ( LevelMax < Aig_ObjLevel(pObj) )
+            LevelMax = Aig_ObjLevel(pObj);
+    }
     Aig_ManCleanPioNumbers( p );
 //    Aig_ManForEachNode( p, pObj, i )
 //        assert( Aig_ObjLevel(pObj) > 0 );

src/aig/ntl/ntl.h

@@ -86,6 +86,7 @@ struct Ntl_Mod_t_
     Vec_Ptr_t *        vPis;           // the array of PI objects
     Vec_Ptr_t *        vPos;           // the array of PO objects
     int                nObjs[NTL_OBJ_VOID]; // counter of objects of each type
+    int                fKeep;          // indicates persistant model
     // hashing names into nets
     Ntl_Net_t **       pTable;         // the hash table of names into nets
     int                nTableSize;     // the allocated table size
@@ -219,9 +220,9 @@ static inline void        Ntl_ObjSetFanout( Ntl_Obj_t * p, Ntl_Net_t * pNet, int
         for ( pNet = pNwk->pTable[i]; pNet; pNet = pNet->pNext ) 
 
 #define Ntl_ObjForEachFanin( pObj, pFanin, i )                                  \
-    for ( i = 0; (i < (pObj)->nFanins) && ((pFanin) = (pObj)->pFanio[i]); i++ )
+    for ( i = 0; (i < (pObj)->nFanins) && (((pFanin) = (pObj)->pFanio[i]), 1); i++ )
 #define Ntl_ObjForEachFanout( pObj, pFanout, i )                                \
-    for ( i = 0; (i < (pObj)->nFanouts) && ((pFanout) = (pObj)->pFanio[(pObj)->nFanins+i]); i++ )
+    for ( i = 0; (i < (pObj)->nFanouts) && (((pFanout) = (pObj)->pFanio[(pObj)->nFanins+i]), 1); i++ )
 
 ////////////////////////////////////////////////////////////////////////
 ///                    FUNCTION DECLARATIONS                         ///

src/aig/ntl/ntlEc.c

@@ -226,6 +226,13 @@ void Ntl_ManPrepareCec( char * pFileName1, char * pFileName2, Aig_Man_t ** ppMan
     }
     // normalize inputs/outputs
     Ntl_ManCreateMissingInputs( pModel1, pModel2, 0 );
+    if ( Ntl_ModelCiNum(pModel1) != Ntl_ModelCiNum(pModel2) )
+    {
+        if ( pMan1 )  Ntl_ManFree( pMan1 );
+        if ( pMan2 )  Ntl_ManFree( pMan2 );
+        printf( "Ntl_ManPrepareCec(): Cannot verify designs with too many different CIs.\n" );
+        return;
+    }
     Ntl_ManDeriveCommonCis( pMan1, pMan2, 0 );
     Ntl_ManDeriveCommonCos( pMan1, pMan2, 0 );
     if ( Vec_PtrSize(pMan1->vCos) == 0 )

src/aig/ntl/ntlExtract.c

@@ -289,6 +289,16 @@ Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p )
         Vec_PtrPush( p->vCos, pNet );
         Aig_ObjCreatePo( p->pAig, pNet->pCopy );
     }
+    // visit dangling boxes
+    Ntl_ModelForEachBox( pRoot, pObj, i )
+    {
+        pNet = Ntl_ObjFanout0(pObj);
+        if ( !Ntl_ManExtract_rec( p, pNet ) )
+        {
+            printf( "Ntl_ManExtract(): Error: Combinational loop is detected.\n" );
+            return 0;
+        }
+    }
     // report the number of dangling objects
     nUselessObjects = Ntl_ModelNodeNum(pRoot) + Ntl_ModelLut1Num(pRoot) + Ntl_ModelBoxNum(pRoot) - Vec_PtrSize(p->vNodes);
 //    if ( nUselessObjects )

src/aig/ntl/ntlReadBlif.c

@@ -31,6 +31,7 @@ struct Ioa_ReadMod_t_
 {
     // file lines
     char *               pFirst;       // .model line
+    char *               pAttrib;      // .attrib line
     Vec_Ptr_t *          vInputs;      // .inputs lines
     Vec_Ptr_t *          vOutputs;     // .outputs lines
     Vec_Ptr_t *          vLatches;     // .latch lines
@@ -78,6 +79,7 @@ static void              Ioa_ReadReadPreparse( Ioa_ReadMan_t * p );
 static int               Ioa_ReadReadInterfaces( Ioa_ReadMan_t * p );
 static Ntl_Man_t *       Ioa_ReadParse( Ioa_ReadMan_t * p );
 static int               Ioa_ReadParseLineModel( Ioa_ReadMod_t * p, char * pLine );
+static int               Ioa_ReadParseLineAttrib( Ioa_ReadMod_t * p, char * pLine );
 static int               Ioa_ReadParseLineInputs( Ioa_ReadMod_t * p, char * pLine );
 static int               Ioa_ReadParseLineOutputs( Ioa_ReadMod_t * p, char * pLine );
 static int               Ioa_ReadParseLineLatch( Ioa_ReadMod_t * p, char * pLine );
@@ -519,6 +521,8 @@ static void Ioa_ReadReadPreparse( Ioa_ReadMan_t * p )
             p->pLatest->pFirst = pCur;
             p->pLatest->pMan = p;
         }
+        else if ( !strncmp(pCur, "attrib", 6) ) 
+            p->pLatest->pAttrib = pCur;
         else if ( !strncmp(pCur, "end", 3) )
         {
             if ( p->pLatest )
@@ -562,6 +566,9 @@ static int Ioa_ReadReadInterfaces( Ioa_ReadMan_t * p )
         // parse the model
         if ( !Ioa_ReadParseLineModel( pMod, pMod->pFirst ) )
             return 0;
+        // parse the model attributes
+        if ( pMod->pAttrib && !Ioa_ReadParseLineAttrib( pMod, pMod->pAttrib ) )
+            return 0;
         // parse the inputs
         Vec_PtrForEachEntry( pMod->vInputs, pLine, k )
             if ( !Ioa_ReadParseLineInputs( pMod, pLine ) )
@@ -651,7 +658,7 @@ static int Ioa_ReadParseLineModel( Ioa_ReadMod_t * p, char * pLine )
     assert( !strcmp(pToken, "model") );
     if ( Vec_PtrSize(vTokens) != 2 )
     {
-        sprintf( p->pMan->sError, "Line %d: The number of entries in .model line (%d) is different from two.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrSize(vTokens) );
+        sprintf( p->pMan->sError, "Line %d: The number of entries (%d) in .model line is different from two.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrSize(vTokens) );
         return 0;
     }
     p->pNtk = Ntl_ModelAlloc( p->pMan->pDesign, Vec_PtrEntry(vTokens, 1) );
@@ -660,6 +667,39 @@ static int Ioa_ReadParseLineModel( Ioa_ReadMod_t * p, char * pLine )
 
 /**Function*************************************************************
 
+  Synopsis    [Parses the model line.]
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static int Ioa_ReadParseLineAttrib( Ioa_ReadMod_t * p, char * pLine )
+{
+    Vec_Ptr_t * vTokens = p->pMan->vTokens;
+    char * pToken;
+    Ioa_ReadSplitIntoTokens( vTokens, pLine, '\0' );
+    pToken = Vec_PtrEntry( vTokens, 0 );
+    assert( !strcmp(pToken, "attrib") );
+    if ( Vec_PtrSize(vTokens) != 2 )
+    {
+        sprintf( p->pMan->sError, "Line %d: The number of entries (%d) in .attrib line is different from two.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrSize(vTokens) );
+        return 0;
+    }
+    if ( strcmp( Vec_PtrEntry(vTokens, 1), "keep" ) == 0 )
+        p->pNtk->fKeep = 1;
+    else
+    {
+        sprintf( p->pMan->sError, "Line %d: Unknown attribute (%s) in the .attrib line of model %s.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens, 1), p->pNtk->pName );
+        return 0;
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Parses the inputs line.]
 
   Description []

src/aig/ntl/ntlSweep.c

@@ -77,11 +77,15 @@ void Ntl_ManSweepMark( Ntl_Man_t * p )
     // start from the primary outputs
     Ntl_ModelForEachPo( pRoot, pObj, i )
         Ntl_ManSweepMark_rec( p, pObj );
+    // start from the persistant boxes
+    Ntl_ModelForEachBox( pRoot, pObj, i )
+        if ( pObj->pImplem->fKeep )
+            Ntl_ManSweepMark_rec( p, pObj );
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Derives new netlist by sweeping current netlist with the current AIG.]
+  Synopsis    [Removes logic that does not fanout into POs.]
 
   Description []
                

src/aig/ntl/ntlWriteBlif.c

@@ -47,6 +47,8 @@ void Ioa_WriteBlifModel( FILE * pFile, Ntl_Mod_t * pModel )
     float Delay;
     int i, k, fClockAdded = 0;
     fprintf( pFile, ".model %s\n", pModel->pName );
+    if ( pModel->fKeep )
+        fprintf( pFile, ".attrib keep\n" );
     fprintf( pFile, ".inputs" );
     Ntl_ModelForEachPi( pModel, pObj, i )
         fprintf( pFile, " %s", Ntl_ObjFanout0(pObj)->pName );

src/aig/nwk/nwkDfs.c

@@ -222,6 +222,12 @@ int Nwk_ManLevel( Nwk_Man_t * pNtk )
         if ( LevelMax < Nwk_ObjLevel(pObj) )
             LevelMax = Nwk_ObjLevel(pObj);
     }
+    Nwk_ManForEachCi( pNtk, pObj, i )
+    {
+        Nwk_ManLevel_rec( pObj );
+        if ( LevelMax < Nwk_ObjLevel(pObj) )
+            LevelMax = Nwk_ObjLevel(pObj);
+    }
     return LevelMax;
 }
 
@@ -448,6 +454,10 @@ Vec_Ptr_t * Nwk_ManDfsReverse( Nwk_Man_t * pNtk )
     vNodes = Vec_PtrAlloc( 100 );
     Nwk_ManForEachPi( pNtk, pObj, i )
         Nwk_ManDfsReverse_rec( pObj, vNodes );
+    // add nodes without fanins
+    Nwk_ManForEachNode( pNtk, pObj, i )
+        if ( Nwk_ObjFaninNum(pObj) == 0 && !Nwk_ObjIsTravIdCurrent(pObj) )
+            Vec_PtrPush( vNodes, pObj );
     return vNodes;
 }
 

src/base/abci/abc.c

@@ -252,8 +252,8 @@ static int Abc_CommandAbc8DSec       ( Abc_Frame_t * pAbc, int argc, char ** arg
 void Abc_FrameClearDesign()
 {
     extern Abc_Frame_t * Abc_FrameGetGlobalFrame();
-    extern void Ntl_ManFree( void * );
-    extern void Nwk_ManFree( void * );
+    extern void Ntl_ManFree( void * p );
+    extern void Nwk_ManFree( void * p );
     Abc_Frame_t * pAbc;
 
     pAbc = Abc_FrameGetGlobalFrame();
@@ -15083,7 +15083,7 @@ int Abc_CommandAbc8ReadLogic( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     extern void * Ntl_ManReadNwk( char * pFileName, Aig_Man_t * pAig, Tim_Man_t * pManTime );
     extern Tim_Man_t * Ntl_ManReadTimeMan( void * p );
-    extern void Nwk_ManFree( void * );
+    extern void Nwk_ManFree( void * p );
 
     // set defaults
     Extra_UtilGetoptReset();
@@ -15432,7 +15432,7 @@ int Abc_CommandAbc8PrintLut( Abc_Frame_t * pAbc, int argc, char **argv )
 
     // set the new network
     if ( pAbc->pAbc8Lib == NULL )
-        printf( "LUT library is not specified.\n" );
+        printf( "Abc_CommandAbc8PrintLut(): LUT library is not specified.\n" );
     else
         If_LutLibPrint( pAbc->pAbc8Lib );
     return 0;
@@ -15486,7 +15486,7 @@ int Abc_CommandAbc8Ps( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( pAbc->pAbc8Ntl == NULL )
     {
-        printf( "Abc_CommandAbc8Write(): There is no design to show.\n" );
+        printf( "Abc_CommandAbc8Ps(): There is no design to show.\n" );
         return 1;
     }
 
@@ -15587,7 +15587,7 @@ int Abc_CommandAbc8If( Abc_Frame_t * pAbc, int argc, char ** argv )
     extern Tim_Man_t * Ntl_ManReadTimeMan( void * p );
     extern If_Lib_t * If_SetSimpleLutLib( int nLutSize );
     extern void Nwk_ManSetIfParsDefault( If_Par_t * pPars );
-    extern void Nwk_ManFree( void * );
+    extern void Nwk_ManFree( void * p );
 
     if ( pAbc->pAbc8Lib == NULL )
     {
@@ -15710,7 +15710,7 @@ int Abc_CommandAbc8If( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( pAbc->pAbc8Aig == NULL )
     {
-        printf( "Abc_CommandAbc8Write(): There is no AIG to map.\n" );
+        printf( "Abc_CommandAbc8If(): There is no AIG to map.\n" );
         return 1;
     }
 
@@ -15937,7 +15937,7 @@ int Abc_CommandAbc8DC2( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( pAbc->pAbc8Aig == NULL )
     {
-        printf( "Abc_CommandAbc8DChoice(): There is no AIG to synthesize.\n" );
+        printf( "Abc_CommandAbc8DC2(): There is no AIG to synthesize.\n" );
         return 1;
     }
 
@@ -15945,7 +15945,7 @@ int Abc_CommandAbc8DC2( Abc_Frame_t * pAbc, int argc, char ** argv )
     pAigNew = Dar_ManCompress2( pAbc->pAbc8Aig, fBalance, fUpdateLevel, 1, fVerbose );
     if ( pAigNew == NULL )
     {
-        printf( "Abc_CommandAbc8DChoice(): Tranformation of the AIG has failed.\n" );
+        printf( "Abc_CommandAbc8DC2(): Tranformation of the AIG has failed.\n" );
         return 1;
     }
     Aig_ManStop( pAbc->pAbc8Aig );
@@ -15993,7 +15993,7 @@ int Abc_CommandAbc8Bidec( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( pAbc->pAbc8Nwk == NULL )
     {
-        printf( "Abc_CommandAbc8DChoice(): There is no mapped network to strash.\n" );
+        printf( "Abc_CommandAbc8Bidec(): There is no mapped network to strash.\n" );
         return 1;
     }
     Nwk_ManBidecResyn( pAbc->pAbc8Nwk, 0 );
@@ -16037,7 +16037,7 @@ int Abc_CommandAbc8Strash( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( pAbc->pAbc8Nwk == NULL )
     {
-        printf( "Abc_CommandAbc8DChoice(): There is no mapped network to strash.\n" );
+        printf( "Abc_CommandAbc8Strash(): There is no mapped network to strash.\n" );
         return 1;
     }
 
@@ -16250,7 +16250,7 @@ int Abc_CommandAbc8Lutpack( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( pAbc->pAbc8Nwk == NULL )
     {
-        printf( "Abc_CommandAbc8DChoice(): There is no mapped network to strash.\n" );
+        printf( "Abc_CommandAbc8Lutpack(): There is no mapped network to strash.\n" );
         return 1;
     }
 
@@ -16325,7 +16325,7 @@ int Abc_CommandAbc8Balance( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( pAbc->pAbc8Aig == NULL )
     {
-        printf( "Abc_CommandAbc8DChoice(): There is no AIG to synthesize.\n" );
+        printf( "Abc_CommandAbc8Balance(): There is no AIG to synthesize.\n" );
         return 1;
     }
 
@@ -16422,7 +16422,7 @@ int Abc_CommandAbc8Speedup( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( pAbc->pAbc8Nwk == NULL )
     {
-        printf( "Abc_CommandAbc8DChoice(): There is no mapped network to strash.\n" );
+        printf( "Abc_CommandAbc8Speedup(): There is no mapped network to strash.\n" );
         return 1;
     }
        
@@ -16978,18 +16978,24 @@ usage:
 ***********************************************************************/
 int Abc_CommandAbc8Sweep( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
+    void * pNtlTemp;
     int Counter;
+    int fMapped;
     int fVerbose;
     int c;
     extern int Ntl_ManSweep( void * p, int fVerbose );
 
     // set defaults
+    fMapped  = 0;
     fVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "mvh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'm':
+            fMapped ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -17005,16 +17011,65 @@ int Abc_CommandAbc8Sweep( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
+    // if mapped, insert the network
+    if ( fMapped )
+    {
+        if ( pAbc->pAbc8Nwk == NULL )
+        {
+            printf( "Abc_CommandAbc8Sweep(): There is no mapped network to sweep.\n" );
+            return 1;
+        }
+        pNtlTemp = Ntl_ManInsertNtk( pAbc->pAbc8Ntl, pAbc->pAbc8Nwk );
+        if ( pNtlTemp == NULL )
+        {
+            printf( "Abc_CommandAbc8Sweep():  Inserting mapped network has failed.\n" );
+            return 1;
+        }
+        Abc_FrameClearDesign(); 
+        pAbc->pAbc8Ntl = pNtlTemp;
+    }
+
     // sweep the current design
     Counter = Ntl_ManSweep( pAbc->pAbc8Ntl, fVerbose );
     if ( Counter == 0 )
         printf( "The netlist is unchanged by sweep.\n" );
+
+    // if mapped, create new AIG and new mapped network
+    if ( fMapped )
+    {
+        pAbc->pAbc8Aig = Ntl_ManExtract( pAbc->pAbc8Ntl );
+        if ( pAbc->pAbc8Aig == NULL )
+        {
+            printf( "Abc_CommandAbc8Sweep(): AIG extraction has failed.\n" );
+            return 1;
+        }
+        pAbc->pAbc8Nwk = Ntl_ManExtractNwk( pAbc->pAbc8Ntl, pAbc->pAbc8Aig, NULL );
+        if ( pAbc->pAbc8Nwk == NULL )
+        {
+            printf( "Abc_CommandAbc8Sweep(): Failed to extract the mapped network.\n" );
+            return 1;
+        }
+    }
+    else // remove old AIG/mapped and create new AIG
+    {
+        pNtlTemp = pAbc->pAbc8Ntl; pAbc->pAbc8Ntl = NULL;
+        Abc_FrameClearDesign(); 
+        pAbc->pAbc8Ntl = pNtlTemp;
+        // extract new AIG
+        pAbc->pAbc8Aig = Ntl_ManExtract( pAbc->pAbc8Ntl );
+        if ( pAbc->pAbc8Aig == NULL )
+        {
+            printf( "Abc_CommandAbc8Sweep(): AIG extraction has failed.\n" );
+            return 1;
+        }
+    }
     return 0;
 
 usage:
-    fprintf( stdout, "usage: *sw [-h]\n" );
+    fprintf( stdout, "usage: *sw [-mvh]\n" );
     fprintf( stdout, "\t        performs structural sweep of the netlist\n" );
     fprintf( stdout, "\t        removes dangling nodes, registers, and white-boxes\n" );
+    fprintf( stdout, "\t-m    : inserts mapped network into netlist and sweeps it [default = %s]\n", fMapped? "yes": "no" );
     fprintf( stdout, "\t-v    : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( stdout, "\t-h    : print the command usage\n");
     return 1;

src/base/abci/abcNtbdd.c

@@ -294,6 +294,15 @@ DdManager * Abc_NtkBuildGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fDrop
             printf( "Constructing global BDDs is aborted.\n" );
             Abc_NtkFreeGlobalBdds( pNtk, 0 );
             Cudd_Quit( dd ); 
+
+            // reset references
+            Abc_NtkForEachObj( pNtk, pObj, i )
+                if ( !Abc_ObjIsBox(pObj) && !Abc_ObjIsBi(pObj) )
+                    pObj->vFanouts.nSize = 0;
+            Abc_NtkForEachObj( pNtk, pObj, i )
+                if ( !Abc_ObjIsBox(pObj) && !Abc_ObjIsBo(pObj) )
+                    Abc_ObjForEachFanin( pObj, pFanin, k )
+                        pFanin->vFanouts.nSize++;
             return NULL;
         }
         bFunc = Cudd_NotCond( bFunc, Abc_ObjFaninC0(pObj) );  Cudd_Ref( bFunc ); 
@@ -322,6 +331,9 @@ DdManager * Abc_NtkBuildGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fDrop
 */
     // reset references
     Abc_NtkForEachObj( pNtk, pObj, i )
+        if ( !Abc_ObjIsBox(pObj) && !Abc_ObjIsBi(pObj) )
+            pObj->vFanouts.nSize = 0;
+    Abc_NtkForEachObj( pNtk, pObj, i )
         if ( !Abc_ObjIsBox(pObj) && !Abc_ObjIsBo(pObj) )
             Abc_ObjForEachFanin( pObj, pFanin, k )
                 pFanin->vFanouts.nSize++;

src/opt/fret/fretMain.c

@@ -523,7 +523,7 @@ Abc_FlowRetime_PushFlows( Abc_Ntk_t * pNtk, bool fVerbose ) {
   
   if (fVerbose) vprintf("max-flow2 = %d\n", flow);
 
-  PRT( "time", clock() - clk );
+//  PRT( "time", clock() - clk );
   return flow;
 }