Version abc80413

1 files changed, 175 insertions, 114 deletions

diff --git a/src/aig/ntl/ntlFraig.c b/src/aig/ntl/ntlFraig.c
index 98f14d3d..117f3275 100644
--- a/src/aig/ntl/ntlFraig.c
+++ b/src/aig/ntl/ntlFraig.c
@@ -48,8 +48,13 @@ Aig_Obj_t ** Ntl_ManFraigDeriveClasses( Aig_Man_t * pAig, Ntl_Man_t * pNew, Aig_
     Aig_Obj_t * pObj, * pObjCol, * pObjColRepr, * pCorresp;
     int i;
 
+    // remember pointers to the nets of pNew
+    Aig_ManForEachObj( pAig, pObj, i )
+        pObj->pNext = pObj->pData;
+
     // map the AIG managers
     Aig_ManForEachObj( pAig, pObj, i )
+    {
         if ( Aig_ObjIsConst1(pObj) )
             pObj->pData = Aig_ManConst1(pAigCol);
         else if ( !Aig_ObjIsPo(pObj) )
@@ -58,6 +63,7 @@ Aig_Obj_t ** Ntl_ManFraigDeriveClasses( Aig_Man_t * pAig, Ntl_Man_t * pNew, Aig_
             pObjCol = Aig_Regular(pNet->pCopy);
             pObj->pData = pObjCol;
         }
+    }
 
     // create mapping from the collapsed manager into the original manager
     // (each node in the collapsed manager may have more than one equivalent node 
@@ -98,12 +104,84 @@ Aig_Obj_t ** Ntl_ManFraigDeriveClasses( Aig_Man_t * pAig, Ntl_Man_t * pNew, Aig_
             pReprs[pCorresp->Id] = pObj;
     }
     free( pMapBack );
+
+    // recall pointers to the nets of pNew
+    Aig_ManForEachObj( pAig, pObj, i )
+        pObj->pData = pObj->pNext, pObj->pNext = NULL;
     return pReprs;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Returns AIG with WB after fraiging.]
+  Synopsis    [Uses equivalences in the AID to reduce the design.]
+
+  Description [The AIG (pAig) was extracted from the netlist and still 
+  points to it (pObj->pData is the pointer to the nets in the netlist).
+  Equivalences have been computed for the collapsed AIG and transfered
+  to this AIG (pAig). This procedure reduces the corresponding nets.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntl_ManReduce( Ntl_Man_t * p, Aig_Man_t * pAig )
+{
+    Aig_Obj_t * pObj, * pObjRepr;
+    Ntl_Net_t * pNet, * pNetRepr;
+    Ntl_Mod_t * pRoot;
+    Ntl_Obj_t * pNode;
+    int i, fCompl, Counter = 0;
+    assert( pAig->pReprs );
+    pRoot = Ntl_ManRootModel( p );
+
+    Aig_ManForEachObj( pAig, pObj, i )
+    {
+        pObjRepr = Aig_ObjRepr( pAig, pObj );
+        if ( pObjRepr == NULL )
+            continue;
+        assert( pObj != pObjRepr );
+        pNet = pObj->pData;
+        pNetRepr = pObjRepr->pData;
+        if ( pNetRepr == NULL )
+        {
+            // this is the constant node
+            assert( Aig_ObjIsConst1(pObjRepr) );
+            pNode = Ntl_ModelCreateNode( pRoot, 0 );
+            pNode->pSop = Ntl_ManStoreSop( p->pMemSops, " 1\n" );
+            if ( (pNetRepr = Ntl_ModelFindNet( pRoot, "Const1" )) )
+            {
+                printf( "Ntl_ManReduce(): Internal error: Intermediate net name is not unique.\n" );
+                return;
+            }
+            pNetRepr = Ntl_ModelFindOrCreateNet( pRoot, "Const1" );
+            if ( !Ntl_ModelSetNetDriver( pNode, pNetRepr ) )
+            {
+                printf( "Ntl_ManReduce(): Internal error: Net has more than one fanin.\n" );
+                return;
+            }
+            pObjRepr->pData = pNetRepr;
+            pNetRepr->pCopy = Aig_ManConst1(pAig);
+        }
+        // get the complemented attributes of the nets
+        fCompl = Aig_IsComplement(pNet->pCopy) ^ Aig_Regular(pNet->pCopy)->fPhase ^
+                 Aig_IsComplement(pNetRepr->pCopy) ^ Aig_Regular(pNetRepr->pCopy)->fPhase;
+        // create interter/buffer driven by the representative net
+        pNode = Ntl_ModelCreateNode( pRoot, 1 );
+        pNode->pSop = fCompl? Ntl_ManStoreSop( p->pMemSops, "0 1\n" ) : Ntl_ManStoreSop( p->pMemSops, "1 1\n" );
+        Ntl_ObjSetFanin( pNode, pNetRepr, 0 );
+        // make the new node drive the equivalent net (pNet)
+        if ( !Ntl_ModelClearNetDriver( pNet->pDriver, pNet ) )
+            printf( "Ntl_ManReduce(): Internal error! Net already has no driver.\n" );
+        if ( !Ntl_ModelSetNetDriver( pNode, pNet ) )
+            printf( "Ntl_ManReduce(): Internal error! Net already has a driver.\n" );
+        Counter++;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Finalizes the transformation.]
 
   Description []
                
@@ -112,43 +190,68 @@ Aig_Obj_t ** Ntl_ManFraigDeriveClasses( Aig_Man_t * pAig, Ntl_Man_t * pNew, Aig_
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Ntl_ManFraig( Ntl_Man_t * p, Aig_Man_t * pAig, int nPartSize, int nConfLimit, int nLevelMax, int fVerbose )
+Ntl_Man_t * Ntl_ManFinalize( Ntl_Man_t * pNew, Aig_Man_t * pAig, Aig_Man_t * pAigCol, int fVerbose )
 {
-    Ntl_Man_t * pNew;
-    Aig_Man_t * pAigCol, * pTemp;
+    int fUseExtraSweep = 1;
+    Ntl_Man_t * pSwept;
+    Aig_Man_t * pTemp;
     assert( pAig->pReprs == NULL );
+    assert( pAigCol->pReprs != NULL );
 
-    // create a new netlist whose nodes are in 1-to-1 relationship with AIG
-    pNew = Ntl_ManInsertAig( p, pAig );
-    if ( pNew == NULL )
+    // transfer equivalence classes to the original AIG
+    pAig->pReprs = Ntl_ManFraigDeriveClasses( pAig, pNew, pAigCol );
+    pAig->nReprsAlloc = Aig_ManObjNumMax(pAig);
+if ( fVerbose )
+    printf( "Equivalences:  Collapsed = %5d.  Extracted = %5d.\n", Aig_ManCountReprs(pAigCol), Aig_ManCountReprs(pAig) );
+
+    // implement equivalence classes and remove dangling nodes
+    Ntl_ManReduce( pNew, pAig );
+    Ntl_ManSweep( pNew, fVerbose );
+
+    // perform one more sweep
+    if ( fUseExtraSweep )
     {
-        printf( "Ntk_ManFraig(): Inserting AIG has failed.\n" );
-        return NULL;
+        pTemp = Ntl_ManExtract( pNew );
+        pSwept = Ntl_ManInsertAig( pNew, pTemp );
+        Aig_ManStop( pTemp );
+        Ntl_ManSweep( pSwept, fVerbose );
+        return pSwept;
     }
+    return Ntl_ManDup(pNew);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns AIG with WB after fraiging.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ntl_Man_t * Ntl_ManFraig( Ntl_Man_t * p, int nPartSize, int nConfLimit, int nLevelMax, int fVerbose )
+{
+    Ntl_Man_t * pNew, * pAux;
+    Aig_Man_t * pAig, * pAigCol, * pTemp;
 
     // collapse the AIG
-    pAigCol = Ntl_ManCollapse( pNew, 0 );
+    pAig = Ntl_ManExtract( p );
+    pNew = Ntl_ManInsertAig( p, pAig );
+    pAigCol = Ntl_ManCollapse( pNew );
+
     // perform fraiging for the given design
-    if ( nPartSize == 0 )
-        nPartSize = Aig_ManPoNum(pAigCol);
+    nPartSize = nPartSize? nPartSize : Aig_ManPoNum(pAigCol);
     pTemp = Aig_ManFraigPartitioned( pAigCol, nPartSize, nConfLimit, nLevelMax, fVerbose );
     Aig_ManStop( pTemp );
 
-    // transfer equivalence classes to the original AIG
-    pAig->pReprs = Ntl_ManFraigDeriveClasses( pAig, pNew, pAigCol );
-    pAig->nReprsAlloc = Aig_ManObjNumMax(pAig);
-    // cleanup
+    // finalize the transformatoin
+    pNew = Ntl_ManFinalize( pAux = pNew, pAig, pAigCol, fVerbose );
+    Ntl_ManFree( pAux );
+    Aig_ManStop( pAig );
     Aig_ManStop( pAigCol );
-    Ntl_ManFree( pNew );
-
-    // derive the new AIG
-    pTemp = Aig_ManDupRepresDfs( pAig );
-    // duplicate the timing manager
-    if ( pAig->pManTime )
-        pTemp->pManTime = Tim_ManDup( pAig->pManTime, 0 );
-    // reset levels
-    Aig_ManChoiceLevel( pTemp );
-    return pTemp;
+    return pNew;
 }
 
 /**Function*************************************************************
@@ -162,44 +265,30 @@ Aig_Man_t * Ntl_ManFraig( Ntl_Man_t * p, Aig_Man_t * pAig, int nPartSize, int nC
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Ntl_ManScl( Ntl_Man_t * p, Aig_Man_t * pAig, int fLatchConst, int fLatchEqual, int fVerbose )
+Ntl_Man_t * Ntl_ManScl( Ntl_Man_t * p, int fLatchConst, int fLatchEqual, int fVerbose )
 {
-    Ntl_Man_t * pNew;
-    Aig_Man_t * pAigCol, * pTemp;
-    assert( pAig->pReprs == NULL );
+    Ntl_Man_t * pNew, * pAux;
+    Aig_Man_t * pAig, * pAigCol, * pTemp;
+
+    // transform the design
+    Ntl_ManTransformInitValues( p );
 
-    // create a new netlist whose nodes are in 1-to-1 relationship with AIG
-    pNew = Ntl_ManInsertAig( p, pAig );
-    if ( pNew == NULL )
-    {
-        printf( "Ntk_ManFraig(): Inserting AIG has failed.\n" );
-        return NULL;
-    }
- 
     // collapse the AIG
-    pAigCol = Ntl_ManCollapse( pNew, 1 );
-    // perform fraiging for the given design
+    pAig = Ntl_ManExtract( p );
+    pNew = Ntl_ManInsertAig( p, pAig );
+    pAigCol = Ntl_ManCollapse( pNew );
+
+    // perform SCL for the given design
     pAigCol->nRegs = Ntl_ModelLatchNum(Ntl_ManRootModel(p));
     pTemp = Aig_ManScl( pAigCol, fLatchConst, fLatchEqual, fVerbose );
     Aig_ManStop( pTemp );
 
-    // transfer equivalence classes to the original AIG
-    pAig->pReprs = Ntl_ManFraigDeriveClasses( pAig, pNew, pAigCol );
-    pAig->nReprsAlloc = Aig_ManObjNumMax(pAig);
-    // cleanup
+    // finalize the transformatoin
+    pNew = Ntl_ManFinalize( pAux = pNew, pAig, pAigCol, fVerbose );
+    Ntl_ManFree( pAux );
+    Aig_ManStop( pAig );
     Aig_ManStop( pAigCol );
-    Ntl_ManFree( pNew );
-
-    // derive the new AIG
-    pTemp = Aig_ManDupRepresDfs( pAig );
-printf( "Intermediate:\n" );
-Aig_ManPrintStats( pTemp );
-    // duplicate the timing manager
-    if ( pAig->pManTime )
-        pTemp->pManTime = Tim_ManDup( pAig->pManTime, 0 );
-    // reset levels
-    Aig_ManChoiceLevel( pTemp );
-    return pTemp;
+    return pNew;
 }
 
 /**Function*************************************************************
@@ -213,46 +302,30 @@ Aig_ManPrintStats( pTemp );
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Ntl_ManLcorr( Ntl_Man_t * p, Aig_Man_t * pAig, int nConfMax, int fVerbose )
+Ntl_Man_t * Ntl_ManLcorr( Ntl_Man_t * p, int nConfMax, int fVerbose )
 {
-    Ntl_Man_t * pNew;
-    Aig_Man_t * pAigCol, * pTemp;
-    assert( pAig->pReprs == NULL );
+    Ntl_Man_t * pNew, * pAux;
+    Aig_Man_t * pAig, * pAigCol, * pTemp;
 
-    // create a new netlist whose nodes are in 1-to-1 relationship with AIG
-    pNew = Ntl_ManInsertAig( p, pAig );
-    if ( pNew == NULL )
-    {
-        printf( "Ntk_ManFraig(): Inserting AIG has failed.\n" );
-        return NULL;
-    }
+    // transform the design
+    Ntl_ManTransformInitValues( p );
 
     // collapse the AIG
-    pAigCol = Ntl_ManCollapse( pNew, 1 );
-    // perform fraiging for the given design
+    pAig = Ntl_ManExtract( p );
+    pNew = Ntl_ManInsertAig( p, pAig );
+    pAigCol = Ntl_ManCollapse( pNew );
+
+    // perform SCL for the given design
     pAigCol->nRegs = Ntl_ModelLatchNum(Ntl_ManRootModel(p));
     pTemp = Fra_FraigLatchCorrespondence( pAigCol, 0, nConfMax, 0, fVerbose, NULL );
-//printf( "Reprs = %d.\n", Aig_ManCountReprs(pAigCol) );
     Aig_ManStop( pTemp );
 
-    // transfer equivalence classes to the original AIG
-    pAig->pReprs = Ntl_ManFraigDeriveClasses( pAig, pNew, pAigCol );
-    pAig->nReprsAlloc = Aig_ManObjNumMax(pAig);
-//printf( "Reprs = %d.\n", Aig_ManCountReprs(pAig) );
-    // cleanup
+    // finalize the transformatoin
+    pNew = Ntl_ManFinalize( pAux = pNew, pAig, pAigCol, fVerbose );
+    Ntl_ManFree( pAux );
+    Aig_ManStop( pAig );
     Aig_ManStop( pAigCol );
-    Ntl_ManFree( pNew );
-
-    // derive the new AIG
-    pTemp = Aig_ManDupRepresDfs( pAig );
-//printf( "Intermediate LCORR:\n" );
-//Aig_ManPrintStats( pTemp );
-    // duplicate the timing manager
-    if ( pAig->pManTime )
-        pTemp->pManTime = Tim_ManDup( pAig->pManTime, 0 );
-    // reset levels
-    Aig_ManChoiceLevel( pTemp );
-    return pTemp;
+    return pNew;
 }
 
 /**Function*************************************************************
@@ -266,42 +339,30 @@ Aig_Man_t * Ntl_ManLcorr( Ntl_Man_t * p, Aig_Man_t * pAig, int nConfMax, int fVe
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Ntl_ManSsw( Ntl_Man_t * p, Aig_Man_t * pAig, Fra_Ssw_t * pPars )
+Ntl_Man_t * Ntl_ManSsw( Ntl_Man_t * p, Fra_Ssw_t * pPars )
 {
-    Ntl_Man_t * pNew;
-    Aig_Man_t * pAigCol, * pTemp;
-    assert( pAig->pReprs == NULL );
+    Ntl_Man_t * pNew, * pAux;
+    Aig_Man_t * pAig, * pAigCol, * pTemp;
 
-    // create a new netlist whose nodes are in 1-to-1 relationship with AIG
-    pNew = Ntl_ManInsertAig( p, pAig );
-    if ( pNew == NULL )
-    {
-        printf( "Ntk_ManFraig(): Inserting AIG has failed.\n" );
-        return NULL;
-    }
+    // transform the design
+    Ntl_ManTransformInitValues( p );
 
     // collapse the AIG
-    pAigCol = Ntl_ManCollapse( pNew, 1 );
-    // perform fraiging for the given design
+    pAig = Ntl_ManExtract( p );
+    pNew = Ntl_ManInsertAig( p, pAig );
+    pAigCol = Ntl_ManCollapse( pNew );
+
+    // perform SCL for the given design
     pAigCol->nRegs = Ntl_ModelLatchNum(Ntl_ManRootModel(p));
     pTemp = Fra_FraigInduction( pAigCol, pPars );
     Aig_ManStop( pTemp );
 
-    // transfer equivalence classes to the original AIG
-    pAig->pReprs = Ntl_ManFraigDeriveClasses( pAig, pNew, pAigCol );
-    pAig->nReprsAlloc = Aig_ManObjNumMax(pAig);
-    // cleanup
+    // finalize the transformatoin
+    pNew = Ntl_ManFinalize( pAux = pNew, pAig, pAigCol, pPars->fVerbose );
+    Ntl_ManFree( pAux );
+    Aig_ManStop( pAig );
     Aig_ManStop( pAigCol );
-    Ntl_ManFree( pNew );
-
-    // derive the new AIG
-    pTemp = Aig_ManDupRepresDfs( pAig );
-    // duplicate the timing manager
-    if ( pAig->pManTime )
-        pTemp->pManTime = Tim_ManDup( pAig->pManTime, 0 );
-    // reset levels
-    Aig_ManChoiceLevel( pTemp );
-    return pTemp;
+    return pNew;
 }