Version abc80327

5 files changed, 132 insertions, 58 deletions

diff --git a/src/aig/ntl/ntl.h b/src/aig/ntl/ntl.h
index caaa86f8..72a5674b 100644
--- a/src/aig/ntl/ntl.h
+++ b/src/aig/ntl/ntl.h
@@ -31,6 +31,7 @@ extern "C" {
 
 #include "aig.h"
 #include "tim.h"
+#include "ntk.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                         PARAMETERS                               ///
@@ -227,6 +228,7 @@ extern Aig_Man_t *     Ntl_ManExtract( Ntl_Man_t * p );
 extern char *          Ntl_SopFromTruth( Ntl_Man_t * p, unsigned * pTruth, int nVars, Vec_Int_t * vCover );
 /*=== ntlInsert.c ==========================================================*/
 extern int             Ntl_ManInsert( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t * pAig );
+extern int             Ntl_ManInsertNtk( Ntl_Man_t * p, Ntk_Man_t * pNtk );
 /*=== ntlCheck.c ==========================================================*/
 extern int             Ntl_ManCheck( Ntl_Man_t * pMan );
 extern int             Ntl_ModelCheck( Ntl_Mod_t * pModel );
@@ -236,6 +238,7 @@ extern Ntl_Man_t *     Ntl_ManAlloc( char * pFileName );
 extern void            Ntl_ManFree( Ntl_Man_t * p );
 extern Ntl_Mod_t *     Ntl_ManFindModel( Ntl_Man_t * p, char * pName );
 extern void            Ntl_ManPrintStats( Ntl_Man_t * p );
+extern Tim_Man_t *     Ntl_ManReadTimeMan( Ntl_Man_t * p );
 extern Ntl_Mod_t *     Ntl_ModelAlloc( Ntl_Man_t * pMan, char * pName );
 extern void            Ntl_ModelFree( Ntl_Mod_t * p );
 /*=== ntlMap.c ============================================================*/
diff --git a/src/aig/ntl/ntlExtract.c b/src/aig/ntl/ntlExtract.c
index 72a8bc40..a54618e5 100644
--- a/src/aig/ntl/ntlExtract.c
+++ b/src/aig/ntl/ntlExtract.c
@@ -438,6 +438,8 @@ Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p )
     // start the AIG manager
     assert( p->pAig == NULL );
     p->pAig = Aig_ManStart( 10000 );
+    p->pAig->pName = Aig_UtilStrsav( p->pName );
+    p->pAig->pSpec = Aig_UtilStrsav( p->pSpec );
     // get the root model
     pRoot = Vec_PtrEntry( p->vModels, 0 );
     // collect primary inputs
diff --git a/src/aig/ntl/ntlInsert.c b/src/aig/ntl/ntlInsert.c
index 971d1278..84a7af84 100644
--- a/src/aig/ntl/ntlInsert.c
+++ b/src/aig/ntl/ntlInsert.c
@@ -123,6 +123,105 @@ int Ntl_ManInsert( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t * pAig )
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Inserts the given mapping into the netlist.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntl_ManInsertNtk( Ntl_Man_t * p, Ntk_Man_t * pNtk )
+{
+    char Buffer[100];
+    Vec_Int_t * vTruth;
+    Vec_Int_t * vCover;
+    Ntl_Mod_t * pRoot;
+    Ntl_Obj_t * pNode;
+    Ntl_Net_t * pNet, * pNetCo;
+    Ntk_Obj_t * pObj, * pFanin;
+    int i, k, nDigits;
+    unsigned * pTruth;
+    assert( Vec_PtrSize(p->vCis) == Ntk_ManCiNum(pNtk) );
+    assert( Vec_PtrSize(p->vCos) == Ntk_ManCoNum(pNtk) );
+    // set the correspondence between the PI/PO nodes
+    Ntl_ManForEachCiNet( p, pNet, i )
+        Ntk_ManCi( pNtk, i )->pCopy = pNet;
+//    Ntl_ManForEachCoNet( p, pNet, i )
+//        Ntk_ManCo( pNtk, i )->pCopy = pNet;
+    // remove old nodes
+    pRoot = Vec_PtrEntry( p->vModels, 0 );
+    Ntl_ModelForEachNode( pRoot, pNode, i )
+        Vec_PtrWriteEntry( pRoot->vObjs, pNode->Id, NULL );
+    // create a new node for each LUT
+    vTruth = Vec_IntAlloc( 1 << 16 );
+    vCover = Vec_IntAlloc( 1 << 16 );
+    nDigits = Aig_Base10Log( Ntk_ManNodeNum(pNtk) );
+    Ntk_ManForEachNode( pNtk, pObj, i )
+    {
+        pNode = Ntl_ModelCreateNode( pRoot, Ntk_ObjFaninNum(pObj) );
+        pTruth = Hop_ManConvertAigToTruth( pNtk->pManHop, pObj->pFunc, Ntk_ObjFaninNum(pObj), vTruth, 0 );
+        pNode->pSop = Ntl_SopFromTruth( p, pTruth, Ntk_ObjFaninNum(pObj), vCover );
+        if ( !Kit_TruthIsConst0(pTruth, Ntk_ObjFaninNum(pObj)) && !Kit_TruthIsConst1(pTruth, Ntk_ObjFaninNum(pObj)) )
+        {
+            Ntk_ObjForEachFanin( pObj, pFanin, k )
+            {
+                pNet = pFanin->pCopy;
+                if ( pNet == NULL )
+                {
+                    printf( "Ntl_ManInsert(): Internal error: Net not found.\n" );
+                    return 0;
+                }
+                Ntl_ObjSetFanin( pNode, pNet, k );
+            }
+        }
+        sprintf( Buffer, "lut%0*d", nDigits, i );
+        if ( (pNet = Ntl_ModelFindNet( pRoot, Buffer )) )
+        {
+            printf( "Ntl_ManInsert(): Internal error: Intermediate net name is not unique.\n" );
+            return 0;
+        }
+        pNet = Ntl_ModelFindOrCreateNet( pRoot, Buffer );
+        if ( !Ntl_ModelSetNetDriver( pNode, pNet ) )
+        {
+            printf( "Ntl_ManInsert(): Internal error: Net has more than one fanin.\n" );
+            return 0;
+        }
+        pObj->pCopy = pNet;
+    }
+    Vec_IntFree( vCover );
+    Vec_IntFree( vTruth );
+    // mark CIs and outputs of the registers
+    Ntl_ManForEachCiNet( p, pNetCo, i )
+        pNetCo->nVisits = 101;
+    // update the CO pointers
+    Ntl_ManForEachCoNet( p, pNetCo, i )
+    {
+        if ( pNetCo->nVisits == 101 )
+            continue;
+        pNetCo->nVisits = 101;
+        // get the corresponding PO and its driver
+        pObj = Ntk_ManCo( pNtk, i );
+        pFanin = Ntk_ObjFanin0( pObj );
+        // get the net driving the driver
+        pNet = pFanin->pCopy; //Vec_PtrEntry( vCopies, Aig_Regular(pNetCo->pFunc)->Id );
+        pNode = Ntl_ModelCreateNode( pRoot, 1 );
+        pNode->pSop = pObj->fCompl /*Aig_IsComplement(pNetCo->pFunc)*/? Ntl_ManStoreSop( p, "0 1\n" ) : Ntl_ManStoreSop( p, "1 1\n" );
+        Ntl_ObjSetFanin( pNode, pNet, 0 );
+        // update the CO driver net
+        pNetCo->pDriver = NULL;
+        if ( !Ntl_ModelSetNetDriver( pNode, pNetCo ) )
+        {
+            printf( "Ntl_ManInsert(): Internal error: PO net has more than one fanin.\n" );
+            return 0;
+        }
+    }
+    return 1;
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/aig/ntl/ntlMan.c b/src/aig/ntl/ntlMan.c
index b5331ae2..9614a423 100644
--- a/src/aig/ntl/ntlMan.c
+++ b/src/aig/ntl/ntlMan.c
@@ -139,6 +139,22 @@ void Ntl_ManPrintStats( Ntl_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Deallocates the netlist manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Tim_Man_t * Ntl_ManReadTimeMan( Ntl_Man_t * p )
+{
+    return p->pManTime;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Allocates the model.]
 
   Description []
diff --git a/src/aig/ntl/ntlMap.c b/src/aig/ntl/ntlMap.c
index 3de74200..20bc79cf 100644
--- a/src/aig/ntl/ntlMap.c
+++ b/src/aig/ntl/ntlMap.c
@@ -117,7 +117,7 @@ Vec_Ptr_t * Ntl_MappingFromAig( Aig_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Ntk_ManSetIfParsDefault( If_Par_t * pPars )
+void Ntl_ManSetIfParsDefault( If_Par_t * pPars )
 {
 //    extern void * Abc_FrameReadLibLut();
     // set defaults
@@ -162,57 +162,6 @@ void Ntk_ManSetIfParsDefault( If_Par_t * pPars )
 */
 }
 
-/**Function*************************************************************
-
-  Synopsis    [Load the network into FPGA manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-If_Man_t * Ntk_ManToIf_old( Aig_Man_t * p, If_Par_t * pPars )
-{
-    If_Man_t * pIfMan;
-    Aig_Obj_t * pNode;//, * pFanin, * pPrev;
-    Vec_Ptr_t * vNodes;
-    int i;
-    // start the mapping manager and set its parameters
-    pIfMan = If_ManStart( pPars );
-    // print warning about excessive memory usage
-    if ( 1.0 * Aig_ManObjNum(p) * pIfMan->nObjBytes / (1<<30) > 1.0 )
-        printf( "Warning: The mapper will allocate %.1f Gb for to represent the subject graph with %d AIG nodes.\n", 
-            1.0 * Aig_ManObjNum(p) * pIfMan->nObjBytes / (1<<30), Aig_ManObjNum(p) );
-    // load the AIG into the mapper
-    vNodes = Aig_ManDfsPio( p );
-    Vec_PtrForEachEntry( vNodes, pNode, i )
-    {
-        if ( Aig_ObjIsAnd(pNode) )
-            pNode->pData = (Aig_Obj_t *)If_ManCreateAnd( pIfMan, 
-                If_NotCond( (If_Obj_t *)Aig_ObjFanin0(pNode)->pData, Aig_ObjFaninC0(pNode) ), 
-                If_NotCond( (If_Obj_t *)Aig_ObjFanin1(pNode)->pData, Aig_ObjFaninC1(pNode) ) );
-        else if ( Aig_ObjIsPi(pNode) )
-            pNode->pData = If_ManCreateCi( pIfMan );
-        else if ( Aig_ObjIsPo(pNode) )
-            If_ManCreateCo( pIfMan, If_NotCond( Aig_ObjFanin0(pNode)->pData, Aig_ObjFaninC0(pNode) ) );
-        else if ( Aig_ObjIsConst1(pNode) )
-            Aig_ManConst1(p)->pData = If_ManConst1( pIfMan );
-        else // add the node to the mapper
-            assert( 0 );
-        // set up the choice node
-//        if ( Aig_AigNodeIsChoice( pNode ) )
-//        {
-//            pIfMan->nChoices++;
-//            for ( pPrev = pNode, pFanin = pNode->pData; pFanin; pPrev = pFanin, pFanin = pFanin->pData )
-//                If_ObjSetChoice( (If_Obj_t *)pPrev->pData, (If_Obj_t *)pFanin->pData );
-//            If_ManCreateChoice( pIfMan, (If_Obj_t *)pNode->pData );
-//        }
-    }
-    Vec_PtrFree( vNodes );
-    return pIfMan;
-}
 
 /**Function*************************************************************
 
@@ -225,7 +174,7 @@ If_Man_t * Ntk_ManToIf_old( Aig_Man_t * p, If_Par_t * pPars )
   SeeAlso     []
 
 ***********************************************************************/
-If_Man_t * Ntk_ManToIf( Aig_Man_t * p, If_Par_t * pPars )
+If_Man_t * Ntl_ManToIf( Aig_Man_t * p, If_Par_t * pPars )
 {
     If_Man_t * pIfMan;
     Aig_Obj_t * pNode;//, * pFanin, * pPrev;
@@ -251,7 +200,7 @@ If_Man_t * Ntk_ManToIf( Aig_Man_t * p, If_Par_t * pPars )
                 pIfMan->nLevelMax = (int)pNode->Level;
         }
         else if ( Aig_ObjIsPo(pNode) )
-            If_ManCreateCo( pIfMan, If_NotCond( Aig_ObjFanin0(pNode)->pData, Aig_ObjFaninC0(pNode) ) );
+            pNode->pData = If_ManCreateCo( pIfMan, If_NotCond( Aig_ObjFanin0(pNode)->pData, Aig_ObjFaninC0(pNode) ) );
         else if ( Aig_ObjIsConst1(pNode) )
             Aig_ManConst1(p)->pData = If_ManConst1( pIfMan );
         else // add the node to the mapper
@@ -264,6 +213,11 @@ If_Man_t * Ntk_ManToIf( Aig_Man_t * p, If_Par_t * pPars )
 //                If_ObjSetChoice( (If_Obj_t *)pPrev->pData, (If_Obj_t *)pFanin->pData );
 //            If_ManCreateChoice( pIfMan, (If_Obj_t *)pNode->pData );
 //        }
+        {
+            If_Obj_t * pIfObj = pNode->pData;
+            assert( !If_IsComplement(pIfObj) );
+            assert( pIfObj->Id == pNode->Id );
+        }
     }
     return pIfMan;
 }
@@ -279,7 +233,7 @@ If_Man_t * Ntk_ManToIf( Aig_Man_t * p, If_Par_t * pPars )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Ptr_t * Ntk_ManFromIf( Aig_Man_t * p, If_Man_t * pMan )
+Vec_Ptr_t * Ntl_ManFromIf( Aig_Man_t * p, If_Man_t * pMan )
 {
     Vec_Ptr_t * vIfMap;
     If_Obj_t * pNode, * pLeaf; 
@@ -356,12 +310,12 @@ Vec_Ptr_t * Ntl_MappingIf( Ntl_Man_t * pMan, Aig_Man_t * p )
     If_Par_t Pars, * pPars = &Pars;
     If_Man_t * pIfMan;
     // perform FPGA mapping
-    Ntk_ManSetIfParsDefault( pPars );
+    Ntl_ManSetIfParsDefault( pPars );
     // set the arrival times
     pPars->pTimesArr = ALLOC( float, Aig_ManPiNum(p) );
     memset( pPars->pTimesArr, 0, sizeof(float) * Aig_ManPiNum(p) );
     // translate into the mapper
-    pIfMan = Ntk_ManToIf( p, pPars );    
+    pIfMan = Ntl_ManToIf( p, pPars );    
     if ( pIfMan == NULL )
         return NULL;
     pIfMan->pManTim = Tim_ManDup( pMan->pManTime, 0 );
@@ -371,7 +325,7 @@ Vec_Ptr_t * Ntl_MappingIf( Ntl_Man_t * pMan, Aig_Man_t * p )
         return NULL;
     }
     // transform the result of mapping into the new network
-    vMapping = Ntk_ManFromIf( p, pIfMan );
+    vMapping = Ntl_ManFromIf( p, pIfMan );
     If_ManStop( pIfMan );
     if ( vMapping == NULL )
         return NULL;