Version abc90813

committer: Baruch Sterin <baruchs@gmail.com>

4 files changed, 202 insertions, 2 deletions

diff --git a/src/aig/ntl/ntl.h b/src/aig/ntl/ntl.h
index 0df0f512..5407fcf8 100644
--- a/src/aig/ntl/ntl.h
+++ b/src/aig/ntl/ntl.h
@@ -218,6 +218,7 @@ static inline int         Ntl_ObjIsPo( Ntl_Obj_t * p )            { return p->Ty
 static inline int         Ntl_ObjIsNode( Ntl_Obj_t * p )          { return p->Type == NTL_OBJ_NODE;             } 
 static inline int         Ntl_ObjIsLatch( Ntl_Obj_t * p )         { return p->Type == NTL_OBJ_LATCH;            } 
 static inline int         Ntl_ObjIsBox( Ntl_Obj_t * p )           { return p->Type == NTL_OBJ_BOX;              } 
+static inline int         Ntl_ObjIsLutBox( Ntl_Obj_t * p )        { return Ntl_ObjIsBox(p) && strncmp("LUT", p->pImplem->pName, 3) == 0;  } 
 
 static inline Ntl_Net_t * Ntl_ObjFanin0( Ntl_Obj_t * p )          { return p->pFanio[0];                        } 
 static inline Ntl_Net_t * Ntl_ObjFanout0( Ntl_Obj_t * p )         { return p->pFanio[p->nFanins];               } 
@@ -332,6 +333,7 @@ extern ABC_DLL Ntl_Man_t *     Ntl_ManAlloc();
 extern ABC_DLL void            Ntl_ManCleanup( Ntl_Man_t * p );
 extern ABC_DLL Ntl_Man_t *     Ntl_ManStartFrom( Ntl_Man_t * p );
 extern ABC_DLL Ntl_Man_t *     Ntl_ManDup( Ntl_Man_t * p );
+extern ABC_DLL Ntl_Man_t *     Ntl_ManDupCollapseLuts( Ntl_Man_t * p );
 extern ABC_DLL void            Ntl_ManFree( Ntl_Man_t * p );
 extern ABC_DLL void            Ntl_ManPrintStats( Ntl_Man_t * p );
 extern ABC_DLL Tim_Man_t *     Ntl_ManReadTimeMan( Ntl_Man_t * p );
@@ -342,6 +344,7 @@ extern ABC_DLL void            Ntl_ManPrintResets( Ntl_Man_t * p );
 extern ABC_DLL Ntl_Mod_t *     Ntl_ModelAlloc( Ntl_Man_t * pMan, char * pName );
 extern ABC_DLL Ntl_Mod_t *     Ntl_ModelStartFrom( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld );
 extern ABC_DLL Ntl_Mod_t *     Ntl_ModelDup( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld );
+extern ABC_DLL Ntl_Mod_t *     Ntl_ModelDupCollapseLuts( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld );
 extern ABC_DLL void            Ntl_ModelFree( Ntl_Mod_t * p );
 extern ABC_DLL Ntl_Mod_t *     Ntl_ManCreateLatchModel( Ntl_Man_t * pMan, int Init );
 extern ABC_DLL int             Ntl_ModelCountLut0( Ntl_Mod_t * p );
diff --git a/src/aig/ntl/ntlMan.c b/src/aig/ntl/ntlMan.c
index ec3e34bb..b5ad7815 100644
--- a/src/aig/ntl/ntlMan.c
+++ b/src/aig/ntl/ntlMan.c
@@ -176,6 +176,44 @@ Ntl_Man_t * Ntl_ManDup( Ntl_Man_t * pOld )
 
 /**Function*************************************************************
 
+  Synopsis    [Duplicates the design.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ntl_Man_t * Ntl_ManDupCollapseLuts( Ntl_Man_t * pOld )
+{
+    Ntl_Man_t * pNew;
+    Ntl_Mod_t * pModel;
+    Ntl_Obj_t * pBox;
+//    Ntl_Net_t * pNet;
+    int i, k;
+    pNew = Ntl_ManAlloc();
+    pNew->pName = Ntl_ManStoreFileName( pNew, pOld->pName );
+    pNew->pSpec = Ntl_ManStoreName( pNew, pOld->pName );
+    Vec_PtrForEachEntry( pOld->vModels, pModel, i )
+        pModel->pCopy = Ntl_ModelDupCollapseLuts( pNew, pModel );
+    Vec_PtrForEachEntry( pOld->vModels, pModel, i )
+        Ntl_ModelForEachBox( pModel, pBox, k )
+            if ( pBox->pCopy )
+                ((Ntl_Obj_t *)pBox->pCopy)->pImplem = pBox->pImplem->pCopy;
+//    Ntl_ManForEachCiNet( pOld, pNet, i )
+//        Vec_PtrPush( pNew->vCis, pNet->pCopy );
+//    Ntl_ManForEachCoNet( pOld, pNet, i )
+//        Vec_PtrPush( pNew->vCos, pNet->pCopy );
+//    if ( pOld->pManTime )
+//        pNew->pManTime = Tim_ManDup( pOld->pManTime, 0 );
+    if ( !Ntl_ManCheck( pNew ) )
+        printf( "Ntl_ManDup: The check has failed for design %s.\n", pNew->pName );
+    return pNew;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Deallocates the netlist manager.]
 
   Description []
@@ -738,6 +776,119 @@ Ntl_Mod_t * Ntl_ModelDup( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld )
     return pModelNew;
 }
 
+
+// *r x\large\club_u2.blif.bz2;     *ps; *clplut; *ps
+// *r x\large\amazon_core.blif.bz2; *ps; *clplut; *ps
+
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates the model.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ntl_Mod_t * Ntl_ModelDupCollapseLuts( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld )
+{
+    Ntl_Mod_t * pModelNew, * pModelBox;
+    Ntl_Net_t * pNet;
+    Ntl_Obj_t * pObj, * pObjBox;
+    char * pNameBuf = ABC_ALLOC( char, 10000 );
+    int i, k, m, Counter = 0;
+    pModelNew = Ntl_ModelAlloc( pManNew, pModelOld->pName );
+    pModelNew->attrWhite   = pModelOld->attrWhite;
+    pModelNew->attrBox       = pModelOld->attrBox;
+    pModelNew->attrComb       = pModelOld->attrComb;
+    pModelNew->attrKeep       = pModelOld->attrKeep;
+    pModelNew->attrNoMerge = pModelOld->attrNoMerge;
+    Ntl_ModelForEachObj( pModelOld, pObj, i )
+        if ( Ntl_ObjIsLutBox(pObj) ) // skip collapsible LUT boxes
+            pObj->pCopy = NULL;
+        else
+            pObj->pCopy = Ntl_ModelDupObj( pModelNew, pObj );
+    Ntl_ModelForEachNet( pModelOld, pNet, i )
+    {
+        pNet->pCopy = Ntl_ModelFindOrCreateNet( pModelNew, pNet->pName );
+        ((Ntl_Net_t *)pNet->pCopy)->fFixed = pNet->fFixed;
+        if ( pNet->pDriver == NULL )
+        {
+            assert( !pModelOld->attrWhite );
+            continue;
+        }
+        if ( Ntl_ObjIsLutBox(pNet->pDriver) ) 
+            continue;
+        ((Ntl_Net_t *)pNet->pCopy)->pDriver = pNet->pDriver->pCopy;
+        assert( pNet->pDriver->pCopy != NULL );
+    }
+    Ntl_ModelForEachObj( pModelOld, pObj, i )
+    {
+        if ( Ntl_ObjIsLutBox(pObj) ) // collapse LUT boxes
+        {
+            pModelBox = pObj->pImplem;
+            assert( pModelBox->attrComb );
+            assert( Ntl_ObjFaninNum(pObj) == Ntl_ModelPiNum(pModelBox) );
+            assert( Ntl_ObjFanoutNum(pObj) == Ntl_ModelPoNum(pModelBox) );
+            Ntl_ModelClearNets( pModelBox );
+            // attach PI/PO nets
+            Ntl_ModelForEachPi( pModelBox, pObjBox, k )
+                Ntl_ObjFanout0(pObjBox)->pCopy = Ntl_ObjFanin(pObj, k)->pCopy;
+            Ntl_ModelForEachPo( pModelBox, pObjBox, k )
+                Ntl_ObjFanin0(pObjBox)->pCopy = Ntl_ObjFanout(pObj, k)->pCopy;
+            // duplicate internal nodes
+            Ntl_ModelForEachNode( pModelBox, pObjBox, k )
+                pObjBox->pCopy = Ntl_ModelDupObj( pModelNew, pObjBox );
+            // duplicate and connect nets
+            Ntl_ModelForEachNet( pModelBox, pNet, k )
+            {
+                if ( pNet->pCopy != NULL )
+                    continue;
+                sprintf( pNameBuf, "box%d_%s", i, pNet->pName );
+                pNet->pCopy = Ntl_ModelFindOrCreateNet( pModelNew, pNameBuf ); // change name!!!
+                ((Ntl_Net_t *)pNet->pCopy)->pDriver = pNet->pDriver->pCopy;
+            }
+            // connect nodes
+            Ntl_ModelForEachNode( pModelBox, pObjBox, k )
+            {
+                Ntl_ObjForEachFanin( pObjBox, pNet, m )
+                    Ntl_ObjSetFanin( pObjBox->pCopy, pNet->pCopy, m );
+                Ntl_ObjForEachFanout( pObjBox, pNet, m )
+                    Ntl_ObjSetFanout( pObjBox->pCopy, pNet->pCopy, m );
+                ((Ntl_Obj_t *)pObjBox->pCopy)->pSop = Ntl_ManStoreSop( pManNew->pMemSops, pObjBox->pSop );
+            }
+            // connect the PO nets
+            Ntl_ModelForEachPo( pModelBox, pObjBox, k )
+                ((Ntl_Net_t *)Ntl_ObjFanin0(pObjBox)->pCopy)->pDriver = Ntl_ObjFanin0(pObjBox)->pDriver->pCopy;
+            assert( pObj->pCopy == NULL );
+            Counter++;
+        }
+        else
+        {
+            Ntl_ObjForEachFanin( pObj, pNet, k )
+                Ntl_ObjSetFanin( pObj->pCopy, pNet->pCopy, k );
+            Ntl_ObjForEachFanout( pObj, pNet, k )
+                Ntl_ObjSetFanout( pObj->pCopy, pNet->pCopy, k );
+            if ( Ntl_ObjIsLatch(pObj) )
+            {
+                ((Ntl_Obj_t *)pObj->pCopy)->LatchId = pObj->LatchId;
+                ((Ntl_Obj_t *)pObj->pCopy)->pClock = pObj->pClock? pObj->pClock->pCopy : NULL;
+            }
+            if ( Ntl_ObjIsNode(pObj) )
+                ((Ntl_Obj_t *)pObj->pCopy)->pSop = Ntl_ManStoreSop( pManNew->pMemSops, pObj->pSop );
+        }
+    }
+    pModelNew->vDelays = pModelOld->vDelays? Vec_IntDup( pModelOld->vDelays ) : NULL;
+    pModelNew->vTimeInputs = pModelOld->vTimeInputs? Vec_IntDup( pModelOld->vTimeInputs ) : NULL;
+    pModelNew->vTimeOutputs = pModelOld->vTimeOutputs? Vec_IntDup( pModelOld->vTimeOutputs ) : NULL;
+    ABC_FREE( pNameBuf );
+    if ( Counter )
+    printf( "Collapsed %d LUT boxes.\n", Counter );
+    return pModelNew;
+}
+
 /**Function*************************************************************
 
   Synopsis    [Deallocates the model.]
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 50aa938c..789d2714 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -264,6 +264,7 @@ static int Abc_CommandAbc8Balance            ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandAbc8Speedup            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc8Merge              ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc8Insert             ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc8ClpLut             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandAbc8Fraig              ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc8Scl                ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -598,6 +599,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC8",         "*speedup",      Abc_CommandAbc8Speedup,      0 );
     Cmd_CommandAdd( pAbc, "ABC8",         "*merge",        Abc_CommandAbc8Merge,        0 );
     Cmd_CommandAdd( pAbc, "ABC8",         "*insert",       Abc_CommandAbc8Insert,       0 );
+    Cmd_CommandAdd( pAbc, "ABC8",         "*clplut",       Abc_CommandAbc8ClpLut,       0 );
 
     Cmd_CommandAdd( pAbc, "ABC8",         "*fraig",        Abc_CommandAbc8Fraig,        0 );
     Cmd_CommandAdd( pAbc, "ABC8",         "*scl",          Abc_CommandAbc8Scl,          0 );
@@ -21026,6 +21028,50 @@ usage:
                
   SideEffects []
 
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc8ClpLut( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern void * Ntl_ManDupCollapseLuts( void * p );
+    void * pNtlNew;
+    int c;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pAbc8Ntl == NULL )
+    {
+        printf( "Abc_CommandAbc8Insert(): There is no design.\n" );
+        return 1;
+    }
+    pNtlNew = Ntl_ManDupCollapseLuts( pAbc->pAbc8Ntl );
+    Abc_FrameClearDesign(); 
+    pAbc->pAbc8Ntl = pNtlNew;
+    pAbc->pAbc8Aig = Ntl_ManExtract( pAbc->pAbc8Ntl );
+    return 0;
+
+usage:
+    fprintf( stdout, "usage: *clplut [-h]\n" );
+    fprintf( stdout, "\t         collapses comb white boxes whose model name begins with \"LUT\"\n" );
+    fprintf( stdout, "\t-h     : print the command usage\n");
+    return 1;
+}
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
   SeeAlso     [] 
 
 ***********************************************************************/
diff --git a/src/opt/mfs/mfsResub.c b/src/opt/mfs/mfsResub.c
index 7d0fccc0..49ce6901 100644
--- a/src/opt/mfs/mfsResub.c
+++ b/src/opt/mfs/mfsResub.c
@@ -107,10 +107,10 @@ int Abc_NtkMfsTryResubOnce( Mfs_Man_t * p, int * pCands, int nCands )
 p->timeGia += clock() - clk;
         return RetValue2;
     }
-
+ 
     p->nSatCalls++;
     RetValue = sat_solver_solve( p->pSat, pCands, pCands + nCands, (ABC_INT64_T)p->pPars->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
-    assert( RetValue == l_False || RetValue == l_True );
+//    assert( RetValue == l_False || RetValue == l_True );
 
     if ( RetValue != l_Undef && RetValue2 != -1 )
     {