Version abc80410

1 files changed, 157 insertions, 7 deletions

diff --git a/src/aig/ntl/ntlFraig.c b/src/aig/ntl/ntlFraig.c
index 7153f081..8a172e6c 100644
--- a/src/aig/ntl/ntlFraig.c
+++ b/src/aig/ntl/ntlFraig.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "ntl.h"
+#include "fra.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -30,10 +31,10 @@
 
 /**Function*************************************************************
 
-  Synopsis    [Returns AIG with WB after fraiging.]
+  Synopsis    [Transfers equivalence class info from pAigCol to pAig.]
 
-  Description [pAig points to the nodes of pNew derived using it.
-  pNew points to the nodes of pAigCol derived using it.]
+  Description [pAig points to the nodes of netlist (pNew) derived using it.
+  pNew points to the nodes of the collapsed AIG (pAigCol) derived using it.]
                
   SideEffects []
 
@@ -59,6 +60,9 @@ Aig_Obj_t ** Ntl_ManFraigDeriveClasses( Aig_Man_t * pAig, Ntl_Man_t * pNew, Aig_
         }
 
     // create mapping from the collapsed manager into the original manager
+    // (each node in the collapsed manager may have more than one equivalent node 
+    // in the original manager; this procedure finds the first node in the original 
+    // manager that is equivalent to the given node in the collapsed manager) 
     pMapBack = ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAigCol) );
     memset( pMapBack, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(pAigCol) );
     Aig_ManForEachObj( pAig, pObj, i )
@@ -115,16 +119,15 @@ Aig_Man_t * Ntl_ManFraig( Ntl_Man_t * p, Aig_Man_t * pAig, int nPartSize, int nC
     assert( pAig->pReprs == NULL );
 
     // create a new netlist whose nodes are in 1-to-1 relationship with AIG
-    pNew = Ntl_ManDup( p );
-    if ( !Ntl_ManInsertAig( pNew, pAig ) )
+    pNew = Ntl_ManInsertAig( p, pAig );
+    if ( pNew == NULL )
     {
-        Ntl_ManFree( pNew );
         printf( "Ntk_ManFraig(): Inserting AIG has failed.\n" );
         return NULL;
     }
 
     // collapse the AIG
-    pAigCol = Ntl_ManCollapse( pNew );
+    pAigCol = Ntl_ManCollapse( pNew, 0 );
     // perform fraiging for the given design
     if ( nPartSize == 0 )
         nPartSize = Aig_ManPoNum(pAigCol);
@@ -148,6 +151,153 @@ Aig_Man_t * Ntl_ManFraig( Ntl_Man_t * p, Aig_Man_t * pAig, int nPartSize, int nC
     return pTemp;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Performs sequential cleanup.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Ntl_ManScl( Ntl_Man_t * p, Aig_Man_t * pAig, int fLatchConst, int fLatchEqual, int fVerbose )
+{
+    Ntl_Man_t * pNew;
+    Aig_Man_t * pAigCol, * pTemp;
+    assert( pAig->pReprs == NULL );
+
+    // 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
+    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
+    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;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns AIG with WB after fraiging.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Ntl_ManLcorr( Ntl_Man_t * p, Aig_Man_t * pAig, int nConfMax, int fVerbose )
+{
+    Ntl_Man_t * pNew;
+    Aig_Man_t * pAigCol, * pTemp;
+    assert( pAig->pReprs == NULL );
+
+    // 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
+    pAigCol->nRegs = Ntl_ModelLatchNum(Ntl_ManRootModel(p));
+    pTemp = Fra_FraigLatchCorrespondence( pAigCol, 0, nConfMax, 0, fVerbose, NULL );
+    Aig_ManStop( pTemp );
+
+    // transfer equivalence classes to the original AIG
+    pAig->pReprs = Ntl_ManFraigDeriveClasses( pAig, pNew, pAigCol );
+    pAig->nReprsAlloc = Aig_ManObjNumMax(pAig);
+    // cleanup
+    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;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns AIG with WB after fraiging.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Ntl_ManSsw( Ntl_Man_t * p, Aig_Man_t * pAig, Fra_Ssw_t * pPars )
+{
+    Ntl_Man_t * pNew;
+    Aig_Man_t * pAigCol, * pTemp;
+    assert( pAig->pReprs == NULL );
+
+    // 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
+    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
+    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;
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///