Version abc80413

abc.dsp

@@ -2894,6 +2894,10 @@ SOURCE=.\src\aig\kit\kitIsop.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\kit\kitPla.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\kit\kitSop.c
 # End Source File
 # Begin Source File

src/aig/aig/aigDup.c

@@ -638,7 +638,10 @@ Aig_Man_t * Aig_ManDupRepres( Aig_Man_t * p )
         if ( Aig_ObjIsNode(pObj) )
             pObj->pData = Aig_And( pNew, Aig_ObjChild0Repres(p, pObj), Aig_ObjChild1Repres(p, pObj) );
         else if ( Aig_ObjIsPi(pObj) )
+        {
             pObj->pData = Aig_ObjCreatePi(pNew);
+            pObj->pData = Aig_ObjGetRepres( p, pObj );
+        }
         else if ( Aig_ObjIsPo(pObj) )
             pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Repres(p, pObj) );
         else if ( Aig_ObjIsConst1(pObj) )

src/aig/fra/fraSec.c

@@ -44,7 +44,7 @@ int Fra_FraigSec( Aig_Man_t * p, int nFramesMax, int fRetimeFirst, int fFraiging
 {
     Fra_Ssw_t Pars, * pPars = &Pars;
     Fra_Sml_t * pSml;
-    Aig_Man_t * pNew, * pTemp;
+    Aig_Man_t * pNew = NULL, * pTemp;
     int nFrames, RetValue, nIter, clk, clkTotal = clock();
     int fLatchCorr = 0;
 
@@ -235,7 +235,8 @@ PRT( "Time", clock() - clkTotal );
         Ioa_WriteAiger( pNew, pFileName, 0, 0 );
         printf( "The unsolved reduced miter is written into file \"%s\".\n", pFileName );
     }
-    Aig_ManStop( pNew );
+    if ( pNew )
+        Aig_ManStop( pNew );
     return RetValue;
 }
 

src/aig/kit/kit.h

@@ -160,6 +160,11 @@ static inline unsigned        Kit_DsdLitSupport( Kit_DsdNtk_t * pNtk, int Lit )
 #define Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )                              \
     for ( i = 0; (i < (pObj)->nFans) && ((iLit) = (pObj)->pFans[i], 1); i++ )
 
+#define Kit_PlaForEachCube( pSop, nFanins, pCube )                \
+    for ( pCube = (pSop); *pCube; pCube += (nFanins) + 3 )
+#define Kit_PlaCubeForEachVar( pCube, Value, i )                     \
+    for ( i = 0; (pCube[i] != ' ') && (Value = pCube[i]); i++ )           
+
 ////////////////////////////////////////////////////////////////////////
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
@@ -540,6 +545,17 @@ extern int             Kit_GraphLeafDepth_rec( Kit_Graph_t * pGraph, Kit_Node_t
 //extern Hop_Obj_t *     Kit_CoverToHop( Hop_Man_t * pMan, Vec_Int_t * vCover, int nVars, Vec_Int_t * vMemory );
 /*=== kitIsop.c ==========================================================*/
 extern int             Kit_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vMemory, int fTryBoth );
+/*=== kitPla.c ==========================================================*/
+extern int             Kit_PlaIsConst0( char * pSop );
+extern int             Kit_PlaGetVarNum( char * pSop );
+extern int             Kit_PlaGetCubeNum( char * pSop );
+extern int             Kit_PlaIsComplement( char * pSop );
+extern void            Kit_PlaComplement( char * pSop );
+extern char *          Kit_PlaStart( void * p, int nCubes, int nVars );
+extern char *          Kit_PlaCreateFromIsop( void * p, int nVars, Vec_Int_t * vCover );
+extern void            Kit_PlaToIsop( char * pSop, Vec_Int_t * vCover );
+extern char *          Kit_PlaStoreSop( void * p, char * pSop );
+extern char *          Kit_PlaFromTruth( void * p, unsigned * pTruth, int nVars, Vec_Int_t * vCover );
 /*=== kitSop.c ==========================================================*/
 extern void            Kit_SopCreate( Kit_Sop_t * cResult, Vec_Int_t * vInput, int nVars, Vec_Int_t * vMemory );
 extern void            Kit_SopCreateInverse( Kit_Sop_t * cResult, Vec_Int_t * vInput, int nVars, Vec_Int_t * vMemory );

src/aig/kit/kitPla.c

+/**CFile****************************************************************
+
+  FileName    [kitPla.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Computation kit.]
+
+  Synopsis    [Manipulating SOP in the form of a C-string.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - Dec 6, 2006.]
+
+  Revision    [$Id: kitPla.c,v 1.00 2006/12/06 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "kit.h"
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Checks if the cover is constant 0.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Kit_PlaIsConst0( char * pSop )
+{
+    return pSop[0] == ' ' && pSop[1] == '0';
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reads the number of variables in the cover.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Kit_PlaGetVarNum( char * pSop )
+{
+    char * pCur;
+    for ( pCur = pSop; *pCur != '\n'; pCur++ );
+    return pCur - pSop - 2;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reads the number of cubes in the cover.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Kit_PlaGetCubeNum( char * pSop )
+{
+    char * pCur;
+    int nCubes = 0;
+    if ( pSop == NULL )
+        return 0;
+    for ( pCur = pSop; *pCur; pCur++ )
+        nCubes += (*pCur == '\n');
+    return nCubes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Kit_PlaIsComplement( char * pSop )
+{
+    char * pCur;
+    for ( pCur = pSop; *pCur; pCur++ )
+        if ( *pCur == '\n' )
+            return (int)(*(pCur - 1) == '0' || *(pCur - 1) == 'n');
+    assert( 0 );
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Kit_PlaComplement( char * pSop )
+{
+    char * pCur;
+    for ( pCur = pSop; *pCur; pCur++ )
+        if ( *pCur == '\n' )
+        {
+            if ( *(pCur - 1) == '0' )
+                *(pCur - 1) = '1';
+            else if ( *(pCur - 1) == '1' )
+                *(pCur - 1) = '0';
+            else if ( *(pCur - 1) == 'x' )
+                *(pCur - 1) = 'n';
+            else if ( *(pCur - 1) == 'n' )
+                *(pCur - 1) = 'x';
+            else
+                assert( 0 );
+        }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the constant 1 cover with the given number of variables and cubes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Kit_PlaStart( void * p, int nCubes, int nVars )
+{
+    Aig_MmFlex_t * pMan = p;
+    char * pSopCover, * pCube;
+    int i, Length;
+
+    Length = nCubes * (nVars + 3);
+    pSopCover = Aig_MmFlexEntryFetch( pMan, Length + 1 );
+    memset( pSopCover, '-', Length );
+    pSopCover[Length] = 0;
+
+    for ( i = 0; i < nCubes; i++ )
+    {
+        pCube = pSopCover + i * (nVars + 3);
+        pCube[nVars + 0] = ' ';
+        pCube[nVars + 1] = '1';
+        pCube[nVars + 2] = '\n';
+    }
+    return pSopCover;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the cover from the ISOP computed from TT.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Kit_PlaCreateFromIsop( void * p, int nVars, Vec_Int_t * vCover )
+{
+    Aig_MmFlex_t * pMan = p;
+    char * pSop, * pCube;
+    int i, k, Entry, Literal;
+    assert( Vec_IntSize(vCover) > 0 );
+    if ( Vec_IntSize(vCover) == 0 )
+        return NULL;
+    // start the cover
+    pSop = Kit_PlaStart( pMan, Vec_IntSize(vCover), nVars );
+    // create cubes
+    Vec_IntForEachEntry( vCover, Entry, i )
+    {
+        pCube = pSop + i * (nVars + 3);
+        for ( k = 0; k < nVars; k++ )
+        {
+            Literal = 3 & (Entry >> (k << 1));
+            if ( Literal == 1 )
+                pCube[k] = '0';
+            else if ( Literal == 2 )
+                pCube[k] = '1';
+            else if ( Literal != 0 )
+                assert( 0 );
+        }
+    }
+    return pSop;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the cover from the ISOP computed from TT.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Kit_PlaToIsop( char * pSop, Vec_Int_t * vCover )
+{
+    char * pCube;
+    int k, nVars, Entry;
+    nVars = Kit_PlaGetVarNum( pSop );
+    assert( nVars > 0 );
+    // create cubes
+    Vec_IntClear( vCover );
+    for ( pCube = pSop; *pCube; pCube += nVars + 3 )
+    {
+        Entry = 0;
+        for ( k = nVars - 1; k >= 0; k-- )
+            if ( pCube[k] == '0' )
+                Entry = (Entry << 2) | 1;
+            else if ( pCube[k] == '1' )
+                Entry = (Entry << 2) | 2;
+            else if ( pCube[k] == '-' )
+                Entry = (Entry << 2);
+            else 
+                assert( 0 );
+        Vec_IntPush( vCover, Entry );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates memory and copies the SOP into it.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Kit_PlaStoreSop( void * p, char * pSop )
+{
+    Aig_MmFlex_t * pMan = p;
+    char * pStore;
+    pStore = Aig_MmFlexEntryFetch( pMan, strlen(pSop) + 1 );
+    strcpy( pStore, pSop );
+    return pStore;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Transforms truth table into the SOP.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Kit_PlaFromTruth( void * p, unsigned * pTruth, int nVars, Vec_Int_t * vCover )
+{
+    Aig_MmFlex_t * pMan = p;
+    char * pSop;
+    int RetValue;
+    if ( Kit_TruthIsConst0(pTruth, nVars) )
+        return Kit_PlaStoreSop( pMan, " 0\n" );
+    if ( Kit_TruthIsConst1(pTruth, nVars) )
+        return Kit_PlaStoreSop( pMan, " 1\n" );
+    RetValue = Kit_TruthIsop( pTruth, nVars, vCover, 0 ); // 1 );
+    assert( RetValue == 0 || RetValue == 1 );
+    pSop = Kit_PlaCreateFromIsop( pMan, nVars, vCover );
+    if ( RetValue )
+        Kit_PlaComplement( pSop );
+    return pSop;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/aig/kit/module.make

@@ -6,5 +6,6 @@ SRC +=  src/aig/kit/kitAig.c \
     src/aig/kit/kitGraph.c \
     src/aig/kit/kitHop.c \
     src/aig/kit/kitIsop.c \
+    src/aig/kit/kitPla.c \
     src/aig/kit/kitSop.c \
     src/aig/kit/kitTruth.c

src/aig/ntl/ntl.h

@@ -123,7 +123,6 @@ struct Ntl_Net_t_
     Ntl_Obj_t *        pDriver;        // driver of the net
     char               nVisits;        // the number of times the net is visited
     char               fMark;          // temporary mark
-    char               fCompl;         // complemented attribute
     char               pName[0];       // the name of this net
 };
 
@@ -235,10 +234,9 @@ extern void            Ntl_ManPrepareCec( char * pFileName1, char * pFileName2,
 extern Aig_Man_t *     Ntl_ManPrepareSec( char * pFileName1, char * pFileName2 );
 /*=== ntlExtract.c ==========================================================*/
 extern Aig_Man_t *     Ntl_ManExtract( Ntl_Man_t * p );
-extern Aig_Man_t *     Ntl_ManCollapse( Ntl_Man_t * p, int fSeq );
+extern Aig_Man_t *     Ntl_ManCollapse( Ntl_Man_t * p );
 extern Aig_Man_t *     Ntl_ManCollapseForCec( Ntl_Man_t * p );
 extern Aig_Man_t *     Ntl_ManCollapseForSec( Ntl_Man_t * p1, Ntl_Man_t * p2 );
-extern char *          Ntl_SopFromTruth( Ntl_Man_t * p, unsigned * pTruth, int nVars, Vec_Int_t * vCover );
 /*=== ntlInsert.c ==========================================================*/
 extern Ntl_Man_t *     Ntl_ManInsertMapping( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t * pAig );
 extern Ntl_Man_t *     Ntl_ManInsertAig( Ntl_Man_t * p, Aig_Man_t * pAig );
@@ -275,15 +273,16 @@ extern Ntl_Obj_t *     Ntl_ModelCreateBox( Ntl_Mod_t * pModel, int nFanins, int
 extern Ntl_Obj_t *     Ntl_ModelDupObj( Ntl_Mod_t * pModel, Ntl_Obj_t * pOld );
 extern Ntl_Obj_t *     Ntl_ModelCreatePiWithName( Ntl_Mod_t * pModel, char * pName );
 extern char *          Ntl_ManStoreName( Ntl_Man_t * p, char * pName );
-extern char *          Ntl_ManStoreSop( Ntl_Man_t * p, char * pSop );
+extern char *          Ntl_ManStoreSop( Aig_MmFlex_t * pMan, char * pSop );
 extern char *          Ntl_ManStoreFileName( Ntl_Man_t * p, char * pFileName );
 /*=== ntlSweep.c ==========================================================*/
-extern Ntl_Man_t *     Ntl_ManSweep( Ntl_Man_t * p, Aig_Man_t * pAig, int fVerbose );
+extern int             Ntl_ManSweep( Ntl_Man_t * p, int fVerbose );
 /*=== ntlTable.c ==========================================================*/
 extern Ntl_Net_t *     Ntl_ModelFindNet( Ntl_Mod_t * p, char * pName );
 extern Ntl_Net_t *     Ntl_ModelFindOrCreateNet( Ntl_Mod_t * p, char * pName );
 extern int             Ntl_ModelFindPioNumber( Ntl_Mod_t * p, char * pName, int * pNumber );
 extern int             Ntl_ModelSetNetDriver( Ntl_Obj_t * pObj, Ntl_Net_t * pNet );
+extern int             Ntl_ModelClearNetDriver( Ntl_Obj_t * pObj, Ntl_Net_t * pNet );
 extern void            Ntl_ModelDeleteNet( Ntl_Mod_t * p, Ntl_Net_t * pNet );
 extern int             Ntl_ModelCountNets( Ntl_Mod_t * p );
 /*=== ntlTime.c ==========================================================*/
@@ -295,13 +294,13 @@ extern void            Ioa_WriteBlif( Ntl_Man_t * p, char * pFileName );
 /*=== ntlUtil.c ==========================================================*/
 extern int             Ntl_ModelCountLut1( Ntl_Mod_t * pRoot );
 extern int             Ntl_ManCountSimpleCoDrivers( Ntl_Man_t * p );
-extern int             Ntl_ManTransformCoDrivers( Ntl_Man_t * p );
-extern int             Ntl_ManReconnectCoDrivers( Ntl_Man_t * p );
 extern Vec_Ptr_t *     Ntl_ManCollectCiNames( Ntl_Man_t * p );
 extern Vec_Ptr_t *     Ntl_ManCollectCoNames( Ntl_Man_t * p );
 extern void            Ntl_ManMarkCiCoNets( Ntl_Man_t * p );
 extern void            Ntl_ManUnmarkCiCoNets( Ntl_Man_t * p );
 extern int             Ntl_ManCheckNetsAreNotMarked( Ntl_Mod_t * pModel );
+extern void            Ntl_ManSetZeroInitValues( Ntl_Man_t * p );
+extern void            Ntl_ManTransformInitValues( Ntl_Man_t * p );
 
 #ifdef __cplusplus
 }

src/aig/ntl/ntlCheck.c

@@ -158,7 +158,7 @@ void Ntl_ModelFixNonDrivenNets( Ntl_Mod_t * pModel )
             continue;
         // add the constant 0 driver
         pNode = Ntl_ModelCreateNode( pModel, 0 );
-        pNode->pSop = Ntl_ManStoreSop( pModel->pMan, " 0\n" );
+        pNode->pSop = Ntl_ManStoreSop( pModel->pMan->pMemSops, " 0\n" );
         Ntl_ModelSetNetDriver( pNode, pNet );
         // add the net to those for which the warning will be printed
         Vec_PtrPush( vNets, pNet );

src/aig/ntl/ntlExtract.c

@@ -26,257 +26,12 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-#define Ntl_SopForEachCube( pSop, nFanins, pCube )                \
-    for ( pCube = (pSop); *pCube; pCube += (nFanins) + 3 )
-#define Ntl_CubeForEachVar( pCube, Value, i )                     \
-    for ( i = 0; (pCube[i] != ' ') && (Value = pCube[i]); i++ )           
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
-  Synopsis    [Checks if the cover is constant 0.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Ntl_SopIsConst0( char * pSop )
-{
-    return pSop[0] == ' ' && pSop[1] == '0';
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Reads the number of variables in the cover.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Ntl_SopGetVarNum( char * pSop )
-{
-    char * pCur;
-    for ( pCur = pSop; *pCur != '\n'; pCur++ );
-    return pCur - pSop - 2;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Reads the number of cubes in the cover.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Ntl_SopGetCubeNum( char * pSop )
-{
-    char * pCur;
-    int nCubes = 0;
-    if ( pSop == NULL )
-        return 0;
-    for ( pCur = pSop; *pCur; pCur++ )
-        nCubes += (*pCur == '\n');
-    return nCubes;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Ntl_SopIsComplement( char * pSop )
-{
-    char * pCur;
-    for ( pCur = pSop; *pCur; pCur++ )
-        if ( *pCur == '\n' )
-            return (int)(*(pCur - 1) == '0' || *(pCur - 1) == 'n');
-    assert( 0 );
-    return 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Ntl_SopComplement( char * pSop )
-{
-    char * pCur;
-    for ( pCur = pSop; *pCur; pCur++ )
-        if ( *pCur == '\n' )
-        {
-            if ( *(pCur - 1) == '0' )
-                *(pCur - 1) = '1';
-            else if ( *(pCur - 1) == '1' )
-                *(pCur - 1) = '0';
-            else if ( *(pCur - 1) == 'x' )
-                *(pCur - 1) = 'n';
-            else if ( *(pCur - 1) == 'n' )
-                *(pCur - 1) = 'x';
-            else
-                assert( 0 );
-        }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Creates the constant 1 cover with the given number of variables and cubes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-char * Ntl_SopStart( Aig_MmFlex_t * pMan, int nCubes, int nVars )
-{
-    char * pSopCover, * pCube;
-    int i, Length;
-
-    Length = nCubes * (nVars + 3);
-    pSopCover = Aig_MmFlexEntryFetch( pMan, Length + 1 );
-    memset( pSopCover, '-', Length );
-    pSopCover[Length] = 0;
-
-    for ( i = 0; i < nCubes; i++ )
-    {
-        pCube = pSopCover + i * (nVars + 3);
-        pCube[nVars + 0] = ' ';
-        pCube[nVars + 1] = '1';
-        pCube[nVars + 2] = '\n';
-    }
-    return pSopCover;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Creates the cover from the ISOP computed from TT.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-char * Ntl_SopCreateFromIsop( Aig_MmFlex_t * pMan, int nVars, Vec_Int_t * vCover )
-{
-    char * pSop, * pCube;
-    int i, k, Entry, Literal;
-    assert( Vec_IntSize(vCover) > 0 );
-    if ( Vec_IntSize(vCover) == 0 )
-        return NULL;
-    // start the cover
-    pSop = Ntl_SopStart( pMan, Vec_IntSize(vCover), nVars );
-    // create cubes
-    Vec_IntForEachEntry( vCover, Entry, i )
-    {
-        pCube = pSop + i * (nVars + 3);
-        for ( k = 0; k < nVars; k++ )
-        {
-            Literal = 3 & (Entry >> (k << 1));
-            if ( Literal == 1 )
-                pCube[k] = '0';
-            else if ( Literal == 2 )
-                pCube[k] = '1';
-            else if ( Literal != 0 )
-                assert( 0 );
-        }
-    }
-    return pSop;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Creates the cover from the ISOP computed from TT.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Ntl_SopToIsop( char * pSop, Vec_Int_t * vCover )
-{
-    char * pCube;
-    int k, nVars, Entry;
-    nVars = Ntl_SopGetVarNum( pSop );
-    assert( nVars > 0 );
-    // create cubes
-    Vec_IntClear( vCover );
-    for ( pCube = pSop; *pCube; pCube += nVars + 3 )
-    {
-        Entry = 0;
-        for ( k = nVars - 1; k >= 0; k-- )
-            if ( pCube[k] == '0' )
-                Entry = (Entry << 2) | 1;
-            else if ( pCube[k] == '1' )
-                Entry = (Entry << 2) | 2;
-            else if ( pCube[k] == '-' )
-                Entry = (Entry << 2);
-            else 
-                assert( 0 );
-        Vec_IntPush( vCover, Entry );
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Transforms truth table into the SOP.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-char * Ntl_SopFromTruth( Ntl_Man_t * p, unsigned * pTruth, int nVars, Vec_Int_t * vCover )
-{
-    char * pSop;
-    int RetValue;
-    if ( Kit_TruthIsConst0(pTruth, nVars) )
-        return Ntl_ManStoreSop( p, " 0\n" );
-    if ( Kit_TruthIsConst1(pTruth, nVars) )
-        return Ntl_ManStoreSop( p, " 1\n" );
-    RetValue = Kit_TruthIsop( pTruth, nVars, vCover, 0 ); // 1 );
-    assert( RetValue == 0 || RetValue == 1 );
-    pSop = Ntl_SopCreateFromIsop( p->pMemSops, nVars, vCover );
-    if ( RetValue )
-        Ntl_SopComplement( pSop );
-    return pSop;
-}
-
-
-
-/**Function*************************************************************
-
   Synopsis    [Strashes one logic node using its SOP.]
 
   Description []
@@ -293,14 +48,14 @@ Aig_Obj_t * Ntl_ConvertSopToAigInternal( Aig_Man_t * pMan, Ntl_Obj_t * pNode, ch
     int i, Value, nFanins;
     char * pCube;
     // get the number of variables
-    nFanins = Ntl_SopGetVarNum(pSop);
+    nFanins = Kit_PlaGetVarNum(pSop);
     // go through the cubes of the node's SOP
     pSum = Aig_ManConst0(pMan);
-    Ntl_SopForEachCube( pSop, nFanins, pCube )
+    Kit_PlaForEachCube( pSop, nFanins, pCube )
     {
         // create the AND of literals
         pAnd = Aig_ManConst1(pMan);
-        Ntl_CubeForEachVar( pCube, Value, i )
+        Kit_PlaCubeForEachVar( pCube, Value, i )
         {
             pNet = Ntl_ObjFanin( pNode, i );
             if ( Value == '1' )
@@ -312,7 +67,7 @@ Aig_Obj_t * Ntl_ConvertSopToAigInternal( Aig_Man_t * pMan, Ntl_Obj_t * pNode, ch
         pSum = Aig_Or( pMan, pSum, pAnd );
     }
     // decide whether to complement the result
-    if ( Ntl_SopIsComplement(pSop) )
+    if ( Kit_PlaIsComplement(pSop) )
         pSum = Aig_Not(pSum);
     return pSum;
 }
@@ -366,10 +121,10 @@ Aig_Obj_t * Ntl_ManBuildNodeAig( Ntl_Obj_t * pNode )
     Aig_Man_t * pMan = pNode->pModel->pMan->pAig;
     int fUseFactor = 1;
     // consider the constant node
-    if ( Ntl_SopGetVarNum(pNode->pSop) == 0 )
-        return Aig_NotCond( Aig_ManConst1(pMan), Ntl_SopIsConst0(pNode->pSop) );
+    if ( Kit_PlaGetVarNum(pNode->pSop) == 0 )
+        return Aig_NotCond( Aig_ManConst1(pMan), Kit_PlaIsConst0(pNode->pSop) );
     // decide when to use factoring
-    if ( fUseFactor && Ntl_SopGetVarNum(pNode->pSop) > 2 && Ntl_SopGetCubeNum(pNode->pSop) > 1 )
+    if ( fUseFactor && Kit_PlaGetVarNum(pNode->pSop) > 2 && Kit_PlaGetCubeNum(pNode->pSop) > 1 )
     {
         Dec_Graph_t * pFForm;
         Dec_Node_t * pFFNode;
@@ -437,13 +192,10 @@ int Ntl_ManExtract_rec( Ntl_Man_t * p, Ntl_Net_t * pNet )
             pNetFanin->pCopy = Aig_ObjCreatePi( p->pAig );
             Aig_ObjSetLevel( pNetFanin->pCopy, LevelMax + 1 );
         }
-//printf( "Creating fake PO with ID = %d.\n", Aig_ManPo(p->pAig, Vec_IntEntryLast(p->vBox1Cos))->Id );
     }
     Vec_PtrPush( p->vNodes, pObj );
     if ( Ntl_ObjIsNode(pObj) )
         pNet->pCopy = Ntl_ManBuildNodeAig( pObj );
-    if ( pNet->fCompl )
-        pNet->pCopy = Aig_Not(pNet->pCopy);
     pNet->nVisits = 2;
     return 1;
 }
@@ -517,9 +269,6 @@ Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p )
         if ( !Ntl_ManExtract_rec( p, pNet ) )
         {
             printf( "Ntl_ManExtract(): Error: Combinational loop is detected.\n" );
-            Vec_PtrClear( p->vCis );
-            Vec_PtrClear( p->vCos );
-            Vec_PtrClear( p->vNodes );
             return 0;
         }
         Vec_PtrPush( p->vCos, pNet );
@@ -532,9 +281,6 @@ Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p )
         if ( !Ntl_ManExtract_rec( p, pNet ) )
         {
             printf( "Ntl_ManExtract(): Error: Combinational loop is detected.\n" );
-            Vec_PtrClear( p->vCis );
-            Vec_PtrClear( p->vCos );
-            Vec_PtrClear( p->vNodes );
             return 0;
         }
         Vec_PtrPush( p->vCos, pNet );
@@ -555,8 +301,6 @@ Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p )
     return pAig;    
 }
 
-
-
 /**Function*************************************************************
 
   Synopsis    [Collects the nodes in a topological order.]
@@ -641,8 +385,6 @@ int Ntl_ManCollapse_rec( Ntl_Man_t * p, Ntl_Net_t * pNet )
     }
     if ( Ntl_ObjIsNode(pObj) )
         pNet->pCopy = Ntl_ManBuildNodeAig( pObj );
-    if ( pNet->fCompl )
-        pNet->pCopy = Aig_Not(pNet->pCopy);
     pNet->nVisits = 2;
     return 1;
 }
@@ -659,7 +401,7 @@ int Ntl_ManCollapse_rec( Ntl_Man_t * p, Ntl_Net_t * pNet )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p, int fSeq )
+Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p )
 {
     Aig_Man_t * pAig;
     Ntl_Mod_t * pRoot;
@@ -695,8 +437,6 @@ Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p, int fSeq )
         assert( Ntl_ObjFanoutNum(pObj) == 1 );
         pNet = Ntl_ObjFanout0(pObj);
         pNet->pCopy = Aig_ObjCreatePi( p->pAig );
-        if ( fSeq && (pObj->LatchId & 3) == 1 )
-            pNet->pCopy = Aig_Not(pNet->pCopy);
         if ( pNet->nVisits )
         {
             printf( "Ntl_ManCollapse(): Latch output is duplicated or defined as a primary input.\n" );
@@ -724,10 +464,7 @@ Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p, int fSeq )
             printf( "Ntl_ManCollapse(): Error: Combinational loop is detected.\n" );
             return 0;
         }
-        if ( fSeq && (pObj->LatchId & 3) == 1 )
-            Aig_ObjCreatePo( p->pAig, Aig_Not(pNet->pCopy) );
-        else
-            Aig_ObjCreatePo( p->pAig, pNet->pCopy );
+        Aig_ObjCreatePo( p->pAig, pNet->pCopy );
     }
     // cleanup the AIG
     Aig_ManCleanup( p->pAig );
@@ -788,10 +525,9 @@ Aig_Man_t * Ntl_ManCollapseForCec( Ntl_Man_t * p )
 
 /**Function*************************************************************
 
-  Synopsis    [Performs DFS.]
+  Synopsis    [Derives AIG for SEC.]
 
-  Description [Checks for combinational loops. Collects PI/PO nets.
-  Collects nodes in the topological order.]
+  Description [Uses CIs/COs collected in the internal arrays.]
                
   SideEffects []
 
@@ -988,18 +724,20 @@ Nwk_Obj_t * Ntl_ManExtractNwk_rec( Ntl_Man_t * p, Ntl_Net_t * pNet, Nwk_Man_t *
         Nwk_ObjAddFanin( pNode, pFaninNet->pCopy );
     }
     if ( Ntl_ObjFaninNum(pNet->pDriver) == 0 )
-        pNode->pFunc = Hop_NotCond( Hop_ManConst1(pNtk->pManHop), Ntl_SopIsConst0(pNet->pDriver->pSop) );
+        pNode->pFunc = Hop_NotCond( Hop_ManConst1(pNtk->pManHop), Kit_PlaIsConst0(pNet->pDriver->pSop) );
     else
     {
-        Ntl_SopToIsop( pNet->pDriver->pSop, vCover );
+        Kit_PlaToIsop( pNet->pDriver->pSop, vCover );
         pNode->pFunc = Kit_CoverToHop( pNtk->pManHop, vCover, Ntl_ObjFaninNum(pNet->pDriver), vMemory );
+        if ( Kit_PlaIsComplement(pNet->pDriver->pSop) )
+            pNode->pFunc = Hop_Not(pNode->pFunc);
     }
     return pNet->pCopy = pNode;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Extracts logic newtork out of the netlist.]
+  Synopsis    [Extracts logic network out of the netlist.]
 
   Description []
                
@@ -1054,7 +792,6 @@ Nwk_Man_t * Ntl_ManExtractNwk( Ntl_Man_t * p, Aig_Man_t * pAig )
             pNet = Ntl_ObjFanin0(pObj);
             pNet->pCopy = Ntl_ManExtractNwk_rec( p, pNet, pNtk, vCover, vMemory ); 
             pNode = Nwk_ManCreateCo( pNtk );
-            pNode->fCompl = pNet->fCompl;
             Nwk_ObjAddFanin( pNode, pNet->pCopy );
         }
     }
@@ -1112,7 +849,6 @@ Nwk_Man_t * Ntl_ManReadNwk( char * pFileName, Aig_Man_t * pAig, Tim_Man_t * pMan
     return pNtk;
 }
 
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

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;
 }
 
 

src/aig/ntl/ntlInsert.c

@@ -68,7 +68,7 @@ Ntl_Man_t * Ntl_ManInsertMapping( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t
     Vec_PtrForEachEntry( vMapping, pLut, i )
     {
         pNode = Ntl_ModelCreateNode( pRoot, pLut->nFanins );
-        pNode->pSop = Ntl_SopFromTruth( p, pLut->pTruth, pLut->nFanins, vCover );
+        pNode->pSop = Kit_PlaFromTruth( p->pMemSops, pLut->pTruth, pLut->nFanins, vCover );
         if ( !Kit_TruthIsConst0(pLut->pTruth, pLut->nFanins) && !Kit_TruthIsConst1(pLut->pTruth, pLut->nFanins) )
         {
             for ( k = 0; k < pLut->nFanins; k++ )
@@ -108,7 +108,7 @@ Ntl_Man_t * Ntl_ManInsertMapping( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t
         pNetCo->fMark = 1;
         pNet = Vec_PtrEntry( vCopies, Aig_Regular(pNetCo->pCopy)->Id );
         pNode = Ntl_ModelCreateNode( pRoot, 1 );
-        pNode->pSop = Aig_IsComplement(pNetCo->pCopy)? Ntl_ManStoreSop( p, "0 1\n" ) : Ntl_ManStoreSop( p, "1 1\n" );
+        pNode->pSop = Aig_IsComplement(pNetCo->pCopy)? Ntl_ManStoreSop( p->pMemSops, "0 1\n" ) : Ntl_ManStoreSop( p->pMemSops, "1 1\n" );
         Ntl_ObjSetFanin( pNode, pNet, 0 );
         // update the CO driver net
         assert( pNetCo->pDriver == NULL );
@@ -158,7 +158,7 @@ Ntl_Man_t * Ntl_ManInsertAig( Ntl_Man_t * p, Aig_Man_t * pAig )
     if ( Aig_ManConst1(pAig)->nRefs > 0 )
     {
         pNode = Ntl_ModelCreateNode( pRoot, 0 );
-        pNode->pSop = Ntl_ManStoreSop( p, " 1\n" );
+        pNode->pSop = Ntl_ManStoreSop( p->pMemSops, " 1\n" );
         if ( (pNet = Ntl_ModelFindNet( pRoot, "Const1" )) )
         {
             printf( "Ntl_ManInsertAig(): Internal error: Intermediate net name is not unique.\n" );
@@ -188,13 +188,13 @@ Ntl_Man_t * Ntl_ManInsertAig( Ntl_Man_t * p, Aig_Man_t * pAig )
         Ntl_ObjSetFanin( pNode, Aig_ObjFanin0(pObj)->pData, 0 );
         Ntl_ObjSetFanin( pNode, Aig_ObjFanin1(pObj)->pData, 1 );
         if ( Aig_ObjFaninC0(pObj) && Aig_ObjFaninC1(pObj) )
-            pNode->pSop = Ntl_ManStoreSop( p, "00 1\n" );
+            pNode->pSop = Ntl_ManStoreSop( p->pMemSops, "00 1\n" );
         else if ( Aig_ObjFaninC0(pObj) && !Aig_ObjFaninC1(pObj) )
-            pNode->pSop = Ntl_ManStoreSop( p, "01 1\n" );
+            pNode->pSop = Ntl_ManStoreSop( p->pMemSops, "01 1\n" );
         else if ( !Aig_ObjFaninC0(pObj) && Aig_ObjFaninC1(pObj) )
-            pNode->pSop = Ntl_ManStoreSop( p, "10 1\n" );
+            pNode->pSop = Ntl_ManStoreSop( p->pMemSops, "10 1\n" );
         else // if ( Aig_ObjFaninC0(pObj) && Aig_ObjFaninC1(pObj) )
-            pNode->pSop = Ntl_ManStoreSop( p, "11 1\n" );
+            pNode->pSop = Ntl_ManStoreSop( p->pMemSops, "11 1\n" );
         sprintf( Buffer, "and%0*d", nDigits, Counter++ );
         if ( (pNet = Ntl_ModelFindNet( pRoot, Buffer )) )
         {
@@ -224,7 +224,7 @@ Ntl_Man_t * Ntl_ManInsertAig( Ntl_Man_t * p, Aig_Man_t * pAig )
         // get the net driving the driver
         pNet = pFanin->pData; 
         pNode = Ntl_ModelCreateNode( pRoot, 1 );
-        pNode->pSop = Aig_ObjFaninC0(pObj)? Ntl_ManStoreSop( p, "0 1\n" ) : Ntl_ManStoreSop( p, "1 1\n" );
+        pNode->pSop = Aig_ObjFaninC0(pObj)? Ntl_ManStoreSop( p->pMemSops, "0 1\n" ) : Ntl_ManStoreSop( p->pMemSops, "1 1\n" );
         Ntl_ObjSetFanin( pNode, pNet, 0 );
         // update the CO driver net
         assert( pNetCo->pDriver == NULL );
@@ -288,7 +288,7 @@ Ntl_Man_t * Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk )
         pTruth = Hop_ManConvertAigToTruth( pNtk->pManHop, Hop_Regular(pObj->pFunc), Nwk_ObjFaninNum(pObj), vTruth, 0 );
         if ( Hop_IsComplement(pObj->pFunc) )
             Kit_TruthNot( pTruth, pTruth, Nwk_ObjFaninNum(pObj) );
-        pNode->pSop = Ntl_SopFromTruth( p, pTruth, Nwk_ObjFaninNum(pObj), vCover );
+        pNode->pSop = Kit_PlaFromTruth( p->pMemSops, pTruth, Nwk_ObjFaninNum(pObj), vCover );
         if ( !Kit_TruthIsConst0(pTruth, Nwk_ObjFaninNum(pObj)) && !Kit_TruthIsConst1(pTruth, Nwk_ObjFaninNum(pObj)) )
         {
             Nwk_ObjForEachFanin( pObj, pFanin, k )
@@ -332,9 +332,9 @@ Ntl_Man_t * Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk )
         pObj = Nwk_ManCo( pNtk, i );
         pFanin = Nwk_ObjFanin0( pObj );
         // get the net driving the driver
-        pNet = pFanin->pCopy; //Vec_PtrEntry( vCopies, Aig_Regular(pNetCo->pCopy)->Id );
+        pNet = pFanin->pCopy;
         pNode = Ntl_ModelCreateNode( pRoot, 1 );
-        pNode->pSop = pObj->fCompl /*Aig_IsComplement(pNetCo->pCopy)*/? Ntl_ManStoreSop( p, "0 1\n" ) : Ntl_ManStoreSop( p, "1 1\n" );
+        pNode->pSop = pObj->fInvert? Ntl_ManStoreSop( p->pMemSops, "0 1\n" ) : Ntl_ManStoreSop( p->pMemSops, "1 1\n" );
         Ntl_ObjSetFanin( pNode, pNet, 0 );
         // update the CO driver net
         assert( pNetCo->pDriver == NULL );

src/aig/ntl/ntlMan.c

@@ -326,16 +326,27 @@ Ntl_Mod_t * Ntl_ModelStartFrom( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld )
     Ntl_Obj_t * pObj;
     int i, k;
     pModelNew = Ntl_ModelAlloc( pManNew, pModelOld->pName );
+    Ntl_ModelForEachObj( pModelOld, pObj, i )
+    {
+        if ( Ntl_ObjIsNode(pObj) )
+            pObj->pCopy = NULL;
+        else
+            pObj->pCopy = Ntl_ModelDupObj( pModelNew, pObj );
+    }
     Ntl_ModelForEachNet( pModelOld, pNet, i )
+    {
         if ( pNet->fMark )
+        {
             pNet->pCopy = Ntl_ModelFindOrCreateNet( pModelNew, pNet->pName );
+            ((Ntl_Net_t *)pNet->pCopy)->pDriver = pNet->pDriver->pCopy;
+        }
         else
             pNet->pCopy = NULL;
+    }
     Ntl_ModelForEachObj( pModelOld, pObj, i )
     {
         if ( Ntl_ObjIsNode(pObj) )
             continue;
-        pObj->pCopy = Ntl_ModelDupObj( pModelNew, pObj );
         Ntl_ObjForEachFanin( pObj, pNet, k )
             if ( pNet->pCopy != NULL )
                 Ntl_ObjSetFanin( pObj->pCopy, pNet->pCopy, k );
@@ -369,11 +380,16 @@ Ntl_Mod_t * Ntl_ModelDup( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld )
     Ntl_Obj_t * pObj;
     int i, k;
     pModelNew = Ntl_ModelAlloc( pManNew, pModelOld->pName );
+    Ntl_ModelForEachObj( pModelOld, pObj, i )
+        pObj->pCopy = Ntl_ModelDupObj( pModelNew, pObj );
     Ntl_ModelForEachNet( pModelOld, pNet, i )
+    {
         pNet->pCopy = Ntl_ModelFindOrCreateNet( pModelNew, pNet->pName );
+        ((Ntl_Net_t *)pNet->pCopy)->pDriver = pNet->pDriver->pCopy;
+        assert( pNet->pDriver->pCopy != NULL );
+    }
     Ntl_ModelForEachObj( pModelOld, pObj, i )
     {
-        pObj->pCopy = Ntl_ModelDupObj( pModelNew, pObj );
         Ntl_ObjForEachFanin( pObj, pNet, k )
             Ntl_ObjSetFanin( pObj->pCopy, pNet->pCopy, k );
         Ntl_ObjForEachFanout( pObj, pNet, k )
@@ -381,7 +397,7 @@ Ntl_Mod_t * Ntl_ModelDup( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld )
         if ( Ntl_ObjIsLatch(pObj) )
             ((Ntl_Obj_t *)pObj->pCopy)->LatchId = pObj->LatchId;
         if ( Ntl_ObjIsNode(pObj) )
-            ((Ntl_Obj_t *)pObj->pCopy)->pSop = Ntl_ManStoreSop( pManNew, pObj->pSop );
+            ((Ntl_Obj_t *)pObj->pCopy)->pSop = Ntl_ManStoreSop( pManNew->pMemSops, pObj->pSop );
     }
     pModelNew->vDelays = pModelOld->vDelays? Vec_IntDup( pModelOld->vDelays ) : NULL;
     pModelNew->vArrivals = pModelOld->vArrivals? Vec_IntDup( pModelOld->vArrivals ) : NULL;

src/aig/ntl/ntlObj.c

@@ -245,10 +245,10 @@ char * Ntl_ManStoreName( Ntl_Man_t * p, char * pName )
   SeeAlso     []
 
 ***********************************************************************/
-char * Ntl_ManStoreSop( Ntl_Man_t * p, char * pSop )
+char * Ntl_ManStoreSop( Aig_MmFlex_t * pMan, char * pSop )
 {
     char * pStore;
-    pStore = Aig_MmFlexEntryFetch( p->pMemSops, strlen(pSop) + 1 );
+    pStore = Aig_MmFlexEntryFetch( pMan, strlen(pSop) + 1 );
     strcpy( pStore, pSop );
     return pStore;
 }

src/aig/ntl/ntlReadBlif.c

@@ -1048,7 +1048,7 @@ static char * Ioa_ReadParseTableBlif( Ioa_ReadMod_t * p, char * pTable, int nFan
     // get the tokens
     Ioa_ReadSplitIntoTokens( vTokens, pTable, '.' );
     if ( Vec_PtrSize(vTokens) == 0 )
-        return Ntl_ManStoreSop( p->pMan->pDesign, " 0\n" );
+        return Ntl_ManStoreSop( p->pMan->pDesign->pMemSops, " 0\n" );
     if ( Vec_PtrSize(vTokens) == 1 )
     {
         pOutput = Vec_PtrEntry( vTokens, 0 );
@@ -1057,7 +1057,7 @@ static char * Ioa_ReadParseTableBlif( Ioa_ReadMod_t * p, char * pTable, int nFan
             sprintf( p->pMan->sError, "Line %d: Constant table has wrong output value \"%s\".", Ioa_ReadGetLine(p->pMan, pOutput), pOutput );
             return NULL;
         }
-        return Ntl_ManStoreSop( p->pMan->pDesign, (pOutput[0] == '0') ? " 0\n" : " 1\n" );
+        return Ntl_ManStoreSop( p->pMan->pDesign->pMemSops, (pOutput[0] == '0') ? " 0\n" : " 1\n" );
     }
     pProduct = Vec_PtrEntry( vTokens, 0 );
     if ( Vec_PtrSize(vTokens) % 2 == 1 )
@@ -1123,12 +1123,6 @@ static int Ioa_ReadParseLineNamesBlif( Ioa_ReadMod_t * p, char * pLine )
     // parse the regular name line
     assert( !strcmp(Vec_PtrEntry(vTokens,0), "names") );
     pNameOut = Vec_PtrEntryLast( vTokens );
-/*
-    if ( strcmp( pNameOut, "18434" ) == 0 )
-    {
-        int x = 0;
-    }
-*/
     pNetOut = Ntl_ModelFindOrCreateNet( p->pNtk, pNameOut );
     // create fanins
     pNode = Ntl_ModelCreateNode( p->pNtk, Vec_PtrSize(vTokens) - 2 );
@@ -1147,7 +1141,7 @@ static int Ioa_ReadParseLineNamesBlif( Ioa_ReadMod_t * p, char * pLine )
     pNode->pSop = Ioa_ReadParseTableBlif( p, pNameOut + strlen(pNameOut), pNode->nFanins );
     if ( pNode->pSop == NULL )
         return 0;
-    pNode->pSop = Ntl_ManStoreSop( p->pNtk->pMan, pNode->pSop );
+    pNode->pSop = Ntl_ManStoreSop( p->pNtk->pMan->pMemSops, pNode->pSop );
     return 1;
 }
 

src/aig/ntl/ntlSweep.c

@@ -90,31 +90,23 @@ void Ntl_ManSweepMark( Ntl_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Ntl_Man_t * Ntl_ManSweep( Ntl_Man_t * p, Aig_Man_t * pAig, int fVerbose )
+int Ntl_ManSweep( Ntl_Man_t * p, int fVerbose )
 {
     int nObjsOld[NTL_OBJ_VOID];
-    Ntl_Man_t * pNew;
     Ntl_Mod_t * pRoot;
     Ntl_Net_t * pNet;
     Ntl_Obj_t * pObj;
     int i, k, nNetsOld;
-
-    // insert the AIG into the netlist
-    pNew = Ntl_ManInsertAig( p, pAig );
-    if ( pNew == NULL )
-    {
-        printf( "Ntl_ManSweep(): Inserting AIG has failed.\n" );
-        return NULL;
-    }
+    int Counter = 0;
 
     // remember the number of objects
-    pRoot = Ntl_ManRootModel( pNew );
+    pRoot = Ntl_ManRootModel( p );
     for ( i = 0; i < NTL_OBJ_VOID; i++ )
         nObjsOld[i] = pRoot->nObjs[i];
     nNetsOld = Ntl_ModelCountNets(pRoot);
 
     // mark the nets that do not fanout into POs
-    Ntl_ManSweepMark( pNew );
+    Ntl_ManSweepMark( p );
 
     // remove the useless objects and their nets
     Ntl_ModelForEachObj( pRoot, pObj, i )
@@ -126,20 +118,22 @@ Ntl_Man_t * Ntl_ManSweep( Ntl_Man_t * p, Aig_Man_t * pAig, int fVerbose )
         }
         // remove the fanout nets
         Ntl_ObjForEachFanout( pObj, pNet, k )
-            Ntl_ModelDeleteNet( pRoot, Ntl_ObjFanout0(pObj) );
+            if ( pNet != NULL )
+                Ntl_ModelDeleteNet( pRoot, pNet );
         // remove the object
         if ( Ntl_ObjIsNode(pObj) && Ntl_ObjFaninNum(pObj) == 1 )
             pRoot->nObjs[NTL_OBJ_LUT1]--;
-        else
+        else 
             pRoot->nObjs[pObj->Type]--;
         Vec_PtrWriteEntry( pRoot->vObjs, pObj->Id, NULL );
-        pObj->Id = NTL_OBJ_NONE;
+        pObj->Type = NTL_OBJ_NONE;
+        Counter++;
     }
 
     // print detailed statistics of sweeping
     if ( fVerbose )
     {
-        printf( "Sweep:" );
+        printf( "Swept away:" );
         printf( "  Node = %d (%4.1f %%)", 
             nObjsOld[NTL_OBJ_NODE] - pRoot->nObjs[NTL_OBJ_NODE],
             !nObjsOld[NTL_OBJ_NODE]? 0.0: 100.0 * (nObjsOld[NTL_OBJ_NODE] - pRoot->nObjs[NTL_OBJ_NODE]) / nObjsOld[NTL_OBJ_NODE] );
@@ -153,9 +147,10 @@ Ntl_Man_t * Ntl_ManSweep( Ntl_Man_t * p, Aig_Man_t * pAig, int fVerbose )
             nObjsOld[NTL_OBJ_BOX] - pRoot->nObjs[NTL_OBJ_BOX],
             !nObjsOld[NTL_OBJ_BOX]? 0.0: 100.0 * (nObjsOld[NTL_OBJ_BOX] - pRoot->nObjs[NTL_OBJ_BOX]) / nObjsOld[NTL_OBJ_BOX] );
         printf( "\n" );
-//        printf( "Also, sweep reduced %d nets.\n", nNetsOld - Ntl_ModelCountNets(pRoot) );
     }
-    return pNew;
+    if ( !Ntl_ManCheck( p ) )
+        printf( "Ntl_ManSweep: The check has failed for design %s.\n", p->pName );
+    return Counter;
 }
 
 ////////////////////////////////////////////////////////////////////////

src/aig/ntl/ntlTable.c

@@ -219,7 +219,7 @@ int Ntl_ModelFindPioNumber( Ntl_Mod_t * p, char * pName, int * pNumber )
 
 /**Function*************************************************************
 
-  Synopsis    [Finds or creates the net.]
+  Synopsis    [Sets the driver of the net.]
 
   Description []
                
@@ -241,7 +241,29 @@ int Ntl_ModelSetNetDriver( Ntl_Obj_t * pObj, Ntl_Net_t * pNet )
 
 /**Function*************************************************************
 
-  Synopsis    [Finds or creates the net.]
+  Synopsis    [Clears the driver of the net.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntl_ModelClearNetDriver( Ntl_Obj_t * pObj, Ntl_Net_t * pNet )
+{
+    if ( pObj->pFanio[pObj->nFanins] == NULL )
+        return 0;
+    if ( pNet->pDriver == NULL )
+        return 0;
+    pObj->pFanio[pObj->nFanins] = NULL;
+    pNet->pDriver = NULL;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of nets.]
 
   Description []
                

src/aig/ntl/ntlUtil.c

@@ -107,157 +107,6 @@ int Ntl_ManCountSimpleCoDrivers( Ntl_Man_t * p )
 
 /**Function*************************************************************
 
-  Synopsis    [Removes the CO drivers that are bufs/invs.]
-
-  Description [Should be called immediately after reading from file.]
-               
-  SideEffects [This procedure does not work because the internal net
-  (pNetFanin) may have other drivers.]
-
-  SeeAlso     []
-
-***********************************************************************/
-int Ntl_ManTransformCoDrivers( Ntl_Man_t * p )
-{
-    Vec_Ptr_t * vCoNets;
-    Ntl_Net_t * pNetCo, * pNetFanin;
-    Ntl_Obj_t * pObj;
-    Ntl_Mod_t * pRoot;
-    int i, k, Counter;
-    pRoot = Ntl_ManRootModel( p );
-    // collect the nets of the root model
-    vCoNets = Vec_PtrAlloc( 1000 );
-    Ntl_ModelForEachPo( pRoot, pObj, i )
-        if ( !Ntl_ObjFanin0(pObj)->fMark )
-        {
-            Ntl_ObjFanin0(pObj)->fMark = 1;
-            Vec_PtrPush( vCoNets, Ntl_ObjFanin0(pObj) );
-        }
-    Ntl_ModelForEachLatch( pRoot, pObj, i )
-        if ( !Ntl_ObjFanin0(pObj)->fMark )
-        {
-            Ntl_ObjFanin0(pObj)->fMark = 1;
-            Vec_PtrPush( vCoNets, Ntl_ObjFanin0(pObj) );
-        }
-    Ntl_ModelForEachBox( pRoot, pObj, k )
-    Ntl_ObjForEachFanin( pObj, pNetCo, i )
-        if ( !pNetCo->fMark )
-        {
-            pNetCo->fMark = 1;
-            Vec_PtrPush( vCoNets, pNetCo );
-        }
-    // check the nets
-    Vec_PtrForEachEntry( vCoNets, pNetCo, i )
-    {
-        if ( !Ntl_ObjIsNode(pNetCo->pDriver) )
-            continue;
-        if ( Ntl_ObjFaninNum(pNetCo->pDriver) != 1 )
-            break;
-        pNetFanin = Ntl_ObjFanin0(pNetCo->pDriver);
-        if ( !Ntl_ObjIsNode(pNetFanin->pDriver) )
-            break;
-    }
-    if ( i < Vec_PtrSize(vCoNets) )
-    {
-        Vec_PtrFree( vCoNets );
-        return 0;
-    }
-
-
-    // remove the buffers/inverters
-    Counter = 0;
-    Vec_PtrForEachEntry( vCoNets, pNetCo, i )
-    {
-        pNetCo->fMark = 0;
-        if ( !Ntl_ObjIsNode(pNetCo->pDriver) )
-            continue;
-        // if this net is driven by an interver
-        // set the complemented attribute of the CO
-        assert( Ntl_ObjFaninNum(pNetCo->pDriver) == 1 );
-        pNetCo->fCompl = (int)(pNetCo->pDriver->pSop[0] == '0');
-        // remove the driver
-        Vec_PtrWriteEntry( pRoot->vObjs, pNetCo->pDriver->Id, NULL );
-        // remove the net
-        pNetFanin = Ntl_ObjFanin0(pNetCo->pDriver);
-        Ntl_ModelDeleteNet( pRoot, pNetFanin );
-        // make the CO net point to the new driver
-        assert( Ntl_ObjIsNode(pNetFanin->pDriver) );
-        pNetCo->pDriver = NULL;
-        pNetFanin->pDriver->pFanio[pNetFanin->pDriver->nFanins] = NULL;
-        Ntl_ModelSetNetDriver( pNetFanin->pDriver, pNetCo );
-        Counter++;
-    }
-    Vec_PtrFree( vCoNets );
-    pRoot->nObjs[NTL_OBJ_LUT1] -= Counter;
-    return Counter;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Connects COs to the internal nodes other than inv/bufs.]
-
-  Description [Should be called immediately after reading from file.]
-               
-  SideEffects [This procedure does not work because the internal net
-  (pNetFanin) may have other drivers.]
-
-  SeeAlso     []
-
-***********************************************************************/
-int Ntl_ManReconnectCoDriverOne( Ntl_Net_t * pNetCo )
-{
-    Ntl_Net_t * pNetFanin;
-    // skip the case when the net is not driven by a node
-    if ( !Ntl_ObjIsNode(pNetCo->pDriver) )
-        return 0;
-    // skip the case when the node is not an inv/buf
-    if ( Ntl_ObjFaninNum(pNetCo->pDriver) != 1 )
-        return 0;
-    // skip the case when the second-generation driver is not a node
-    pNetFanin = Ntl_ObjFanin0(pNetCo->pDriver);
-    if ( !Ntl_ObjIsNode(pNetFanin->pDriver) )
-        return 0;
-    // set the complemented attribute of the net
-    pNetCo->fCompl = (int)(pNetCo->pDriver->pSop[0] == '0');
-    // drive the CO net with the second-generation driver
-    pNetCo->pDriver = NULL;
-    pNetFanin->pDriver->pFanio[pNetFanin->pDriver->nFanins] = NULL;
-    if ( !Ntl_ModelSetNetDriver( pNetFanin->pDriver, pNetCo ) )
-        printf( "Ntl_ManReconnectCoDriverOne(): Cannot connect the net.\n" );
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Connects COs to the internal nodes other than inv/bufs.]
-
-  Description [Should be called immediately after reading from file.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Ntl_ManReconnectCoDrivers( Ntl_Man_t * p )
-{
-    Ntl_Net_t * pNetCo;
-    Ntl_Obj_t * pObj;
-    Ntl_Mod_t * pRoot;
-    int i, k, Counter;
-    Counter = 0;
-    pRoot = Ntl_ManRootModel( p );
-    Ntl_ModelForEachPo( pRoot, pObj, i )
-        Counter += Ntl_ManReconnectCoDriverOne( Ntl_ObjFanin0(pObj) );
-    Ntl_ModelForEachLatch( pRoot, pObj, i )
-        Counter += Ntl_ManReconnectCoDriverOne( Ntl_ObjFanin0(pObj) );
-    Ntl_ModelForEachBox( pRoot, pObj, i )
-        Ntl_ObjForEachFanin( pObj, pNetCo, k )
-            Counter += Ntl_ManReconnectCoDriverOne( pNetCo );
-    return Counter;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Derives the array of CI names.]
 
   Description []
@@ -362,6 +211,119 @@ int Ntl_ManCheckNetsAreNotMarked( Ntl_Mod_t * pModel )
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Convert initial values of registers to be zero.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntl_ManSetZeroInitValues( Ntl_Man_t * p )
+{
+    Ntl_Mod_t * pRoot;
+    Ntl_Obj_t * pObj;
+    int i;
+    pRoot = Ntl_ManRootModel(p);
+    Ntl_ModelForEachLatch( pRoot, pObj, i )
+        pObj->LatchId &= ~3;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Transforms the netlist to have latches with const-0 init-values.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntl_ManAddInverters( Ntl_Obj_t * pObj )
+{
+    char * pStore;
+    Ntl_Mod_t * pRoot = pObj->pModel;
+    Ntl_Man_t * pMan = pRoot->pMan;
+    Ntl_Net_t * pNetLo, * pNetLi, * pNetLoInv, * pNetLiInv;
+    Ntl_Obj_t * pNode;
+    int nLength, RetValue;
+    assert( (pObj->LatchId & 3) == 1 );
+    // get the nets
+    pNetLi = Ntl_ObjFanin0(pObj);
+    pNetLo = Ntl_ObjFanout0(pObj);
+    // get storage for net names
+    nLength = strlen(pNetLi->pName) + strlen(pNetLo->pName) + 10; 
+    pStore = Aig_MmFlexEntryFetch( pMan->pMemSops, nLength );
+    // create input interter
+    pNode = Ntl_ModelCreateNode( pRoot, 1 );
+    pNode->pSop = Ntl_ManStoreSop( pMan->pMemSops, "0 1\n" );
+    Ntl_ObjSetFanin( pNode, pNetLi, 0 );
+    // create input net
+    strcpy( pStore, pNetLi->pName );
+    strcat( pStore, "_inv" );
+    if ( Ntl_ModelFindNet( pRoot, pStore ) )
+    {
+        printf( "Ntl_ManTransformInitValues(): Internal error! Cannot create net with LI-name + _inv\n" );
+        return;
+    }
+    pNetLiInv = Ntl_ModelFindOrCreateNet( pRoot, pStore );
+    RetValue = Ntl_ModelSetNetDriver( pNode, pNetLiInv );
+    assert( RetValue );
+    // connect latch to the input net
+    Ntl_ObjSetFanin( pObj, pNetLiInv, 0 );
+    // disconnect latch from the output net
+    RetValue = Ntl_ModelClearNetDriver( pObj, pNetLo );
+    assert( RetValue );
+    // create the output net
+    strcpy( pStore, pNetLo->pName );
+    strcat( pStore, "_inv" );
+    if ( Ntl_ModelFindNet( pRoot, pStore ) )
+    {
+        printf( "Ntl_ManTransformInitValues(): Internal error! Cannot create net with LO-name + _inv\n" );
+        return;
+    }
+    pNetLoInv = Ntl_ModelFindOrCreateNet( pRoot, pStore );
+    RetValue = Ntl_ModelSetNetDriver( pObj, pNetLoInv );
+    assert( RetValue );
+    // create output interter
+    pNode = Ntl_ModelCreateNode( pRoot, 1 );
+    pNode->pSop = Ntl_ManStoreSop( pMan->pMemSops, "0 1\n" );
+    Ntl_ObjSetFanin( pNode, pNetLoInv, 0 );
+    // redirect the old output net
+    RetValue = Ntl_ModelSetNetDriver( pNode, pNetLo );
+    assert( RetValue );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Transforms the netlist to have latches with const-0 init-values.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntl_ManTransformInitValues( Ntl_Man_t * p )
+{
+    Ntl_Mod_t * pRoot;
+    Ntl_Obj_t * pObj;
+    int i;
+    pRoot = Ntl_ManRootModel(p);
+    Ntl_ModelForEachLatch( pRoot, pObj, i )
+    {
+        if ( (pObj->LatchId & 3) == 1 )
+            Ntl_ManAddInverters( pObj );
+        pObj->LatchId &= ~3;
+    }
+
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/aig/ntl/ntlWriteBlif.c

@@ -120,7 +120,7 @@ void Ioa_WriteBlifModel( FILE * pFile, Ntl_Mod_t * pModel )
             if ( Ntl_ObjFanin(pObj, 1) != NULL )
                 fprintf( pFile, " %s", Ntl_ObjFanin(pObj, 1)->pName );
             else if ( pObj->LatchId >> 2 )
-                fprintf( pFile, " clock" ), fClockAdded = 1;
+                fprintf( pFile, " clock99" ), fClockAdded = 1;
             fprintf( pFile, " %d", pObj->LatchId & 3 );
             fprintf( pFile, "\n" );
         }
@@ -135,7 +135,7 @@ void Ioa_WriteBlifModel( FILE * pFile, Ntl_Mod_t * pModel )
         }
     }
     if ( fClockAdded )
-        fprintf( pFile, ".names clock\n 0\n" );
+        fprintf( pFile, ".names clock99\n 0\n" );
     fprintf( pFile, ".end\n\n" );
 }
 

src/aig/nwk/nwk.h

@@ -85,7 +85,7 @@ struct Nwk_Obj_t_
     void *             pNext;          // temporary pointer
     // node information
     unsigned           Type     :  3;  // object type
-    unsigned           fCompl   :  1;  // complemented attribute
+    unsigned           fInvert  :  1;  // complemented attribute
     unsigned           MarkA    :  1;  // temporary mark  
     unsigned           MarkB    :  1;  // temporary mark
     unsigned           PioId    : 26;  // number of this node in the PI/PO list
@@ -123,6 +123,8 @@ static inline Nwk_Obj_t * Nwk_ManCi( Nwk_Man_t * p, int i )       { return Vec_P
 static inline Nwk_Obj_t * Nwk_ManCo( Nwk_Man_t * p, int i )       { return Vec_PtrEntry( p->vCos, i );          } 
 static inline Nwk_Obj_t * Nwk_ManObj( Nwk_Man_t * p, int i )      { return Vec_PtrEntry( p->vObjs, i );         } 
 
+static inline int         Nwk_ObjId( Nwk_Obj_t * p )              { return p->Id;                               } 
+static inline int         Nwk_ObjPioNum( Nwk_Obj_t * p )          { return p->PioId;                            } 
 static inline int         Nwk_ObjFaninNum( Nwk_Obj_t * p )        { return p->nFanins;                          } 
 static inline int         Nwk_ObjFanoutNum( Nwk_Obj_t * p )       { return p->nFanouts;                         } 
 

src/aig/nwk/nwkMap.c

@@ -292,7 +292,7 @@ Nwk_Man_t * Nwk_ManFromIf( If_Man_t * pIfMan, Aig_Man_t * p, Vec_Ptr_t * vAigToI
         else if ( Aig_ObjIsPo(pObj) )
         {
             pObjNew = Nwk_ManCreateCo( pNtk );
-            pObjNew->fCompl = Aig_ObjFaninC0(pObj);
+            pObjNew->fInvert = Aig_ObjFaninC0(pObj);
             Nwk_ObjAddFanin( pObjNew, Aig_ObjFanin0(pObj)->pData );
         }
         else if ( Aig_ObjIsConst1(pObj) )

src/aig/nwk/nwkStrash.c

@@ -119,7 +119,7 @@ Aig_Man_t * Nwk_ManStrash( Nwk_Man_t * pNtk )
         }
         else if ( Nwk_ObjIsCo(pObj) )
         {
-            pObjNew = Aig_ObjCreatePo( pMan, Aig_NotCond(Nwk_ObjFanin0(pObj)->pCopy, pObj->fCompl) );
+            pObjNew = Aig_ObjCreatePo( pMan, Aig_NotCond(Nwk_ObjFanin0(pObj)->pCopy, pObj->fInvert) );
             Level = Aig_ObjLevel( pObjNew );
             Tim_ManSetCoArrival( pMan->pManTime, pObj->PioId, (float)Level );
         }

src/aig/nwk/nwkUtil.c

@@ -19,7 +19,8 @@
 ***********************************************************************/
 
 #include "nwk.h"
-#include "math.h"
+#include "kit.h"
+#include <math.h>
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -250,9 +251,93 @@ void Nwk_ObjPrint( Nwk_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-void Nwk_ManDumpBlif( Nwk_Man_t * pNtk, char * pFileName, Vec_Ptr_t * vCiNames, Vec_Ptr_t * vCoNames )
+void Nwk_ManDumpBlif( Nwk_Man_t * pNtk, char * pFileName, Vec_Ptr_t * vPiNames, Vec_Ptr_t * vPoNames )
 {
-    printf( "Dumping logic network is currently not supported.\n" );
+    FILE * pFile;
+    Vec_Ptr_t * vNodes;
+    Vec_Int_t * vTruth;
+    Vec_Int_t * vCover;
+    Nwk_Obj_t * pObj, * pFanin;
+    Aig_MmFlex_t * pMem;
+    char * pSop = NULL;
+    unsigned * pTruth;
+    int i, k, nDigits, Counter = 0;
+    if ( Nwk_ManPoNum(pNtk) == 0 )
+    {
+        printf( "Nwk_ManDumpBlif(): Network does not have POs.\n" );
+        return;
+    }
+    // collect nodes in the DFS order
+    nDigits = Aig_Base10Log( Nwk_ManObjNumMax(pNtk) );
+    // write the file 
+    pFile = fopen( pFileName, "w" );
+    fprintf( pFile, "# BLIF file written by procedure Nwk_ManDumpBlif()\n" );
+//    fprintf( pFile, "# http://www.eecs.berkeley.edu/~alanmi/abc/\n" );
+    fprintf( pFile, ".model %s\n", pNtk->pName );
+    // write PIs
+    fprintf( pFile, ".inputs" );
+    Nwk_ManForEachCi( pNtk, pObj, i )
+        if ( vPiNames )
+            fprintf( pFile, " %s", Vec_PtrEntry(vPiNames, i) );
+        else
+            fprintf( pFile, " n%0*d", nDigits, pObj->Id );
+    fprintf( pFile, "\n" );
+    // write POs
+    fprintf( pFile, ".outputs" );
+    Nwk_ManForEachCo( pNtk, pObj, i )
+        if ( vPoNames )
+            fprintf( pFile, " %s", Vec_PtrEntry(vPoNames, i) );
+        else
+            fprintf( pFile, " n%0*d", nDigits, pObj->Id );
+    fprintf( pFile, "\n" );
+    // write nodes
+    pMem = Aig_MmFlexStart();
+    vTruth = Vec_IntAlloc( 1 << 16 );
+    vCover = Vec_IntAlloc( 1 << 16 );
+    vNodes = Nwk_ManDfs( pNtk );
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+    {
+        if ( !Nwk_ObjIsNode(pObj) )
+            continue;
+        // derive SOP for the AIG
+        pTruth = Hop_ManConvertAigToTruth( pNtk->pManHop, Hop_Regular(pObj->pFunc), Nwk_ObjFaninNum(pObj), vTruth, 0 );
+        if ( Hop_IsComplement(pObj->pFunc) )
+            Kit_TruthNot( pTruth, pTruth, Nwk_ObjFaninNum(pObj) );
+        pSop = Kit_PlaFromTruth( pMem, pTruth, Nwk_ObjFaninNum(pObj), vCover );
+        // write the node
+        fprintf( pFile, ".names" );
+        if ( !Kit_TruthIsConst0(pTruth, Nwk_ObjFaninNum(pObj)) && !Kit_TruthIsConst1(pTruth, Nwk_ObjFaninNum(pObj)) )
+        {
+            Nwk_ObjForEachFanin( pObj, pFanin, k )
+                if ( vPiNames && Nwk_ObjIsPi(pFanin) )
+                    fprintf( pFile, " %s", Vec_PtrEntry(vPiNames, Nwk_ObjPioNum(pFanin)) );
+                else
+                    fprintf( pFile, " n%0*d", nDigits, pFanin->Id );
+        }
+        fprintf( pFile, " n%0*d\n", nDigits, pObj->Id );
+        // write the function
+        fprintf( pFile, "%s", pSop );
+    }
+    Vec_IntFree( vCover );
+    Vec_IntFree( vTruth );
+    Vec_PtrFree( vNodes );
+    Aig_MmFlexStop( pMem, 0 );
+    // write POs
+    Nwk_ManForEachCo( pNtk, pObj, i )
+    {
+        fprintf( pFile, ".names" );
+        if ( vPiNames && Nwk_ObjIsPi(Nwk_ObjFanin0(pObj)) )
+            fprintf( pFile, " %s", Vec_PtrEntry(vPiNames, Nwk_ObjPioNum(Nwk_ObjFanin0(pObj))) );
+        else
+            fprintf( pFile, " n%0*d", nDigits, Nwk_ObjFanin0(pObj)->Id );
+        if ( vPoNames )
+            fprintf( pFile, " %s\n", Vec_PtrEntry(vPoNames, Nwk_ObjPioNum(pObj)) );
+        else
+            fprintf( pFile, " n%0*d\n", nDigits, pObj->Id );
+        fprintf( pFile, "%d 1\n", !pObj->fInvert );
+    }
+    fprintf( pFile, ".end\n\n" );
+    fclose( pFile );
 }
 
 /**Function*************************************************************

src/base/abci/abc.c

@@ -226,6 +226,7 @@ static int Abc_CommandAbc8Scl        ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandAbc8Lcorr      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc8Ssw        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc8Sweep      ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc8Zero       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandAbc8Cec        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc8DSec       ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -470,6 +471,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC8",         "*lcorr",        Abc_CommandAbc8Lcorr,        0 );
     Cmd_CommandAdd( pAbc, "ABC8",         "*ssw",          Abc_CommandAbc8Ssw,          0 );
     Cmd_CommandAdd( pAbc, "ABC8",         "*sw",           Abc_CommandAbc8Sweep,        0 );
+    Cmd_CommandAdd( pAbc, "ABC8",         "*zero",         Abc_CommandAbc8Zero,         0 );
 
     Cmd_CommandAdd( pAbc, "ABC8",         "*cec",          Abc_CommandAbc8Cec,          0 );
     Cmd_CommandAdd( pAbc, "ABC8",         "*dsec",         Abc_CommandAbc8DSec,         0 );
@@ -14780,6 +14782,7 @@ int Abc_CommandAbc8Read( Abc_Frame_t * pAbc, int argc, char ** argv )
         printf( "Abc_CommandAbc8Read(): AIG extraction has failed.\n" );
         return 1;
     }
+
     return 0;
 
 usage:
@@ -14943,7 +14946,7 @@ int Abc_CommandAbc8Write( Abc_Frame_t * pAbc, int argc, char ** argv )
         else
         {
             pTemp = pAbc->pAbc8Ntl;
-            printf( "Writing the original design.\n" );
+            printf( "Writing the unmapped netlist.\n" );
             Ioa_WriteBlif( pTemp, pFileName );
         }
     }
@@ -14979,7 +14982,7 @@ int Abc_CommandAbc8WriteLogic( Abc_Frame_t * pAbc, int argc, char ** argv )
     extern void Nwk_ManDumpBlif( void * p, char * pFileName, Vec_Ptr_t * vCiNames, Vec_Ptr_t * vCoNames );
 
     // set defaults
-    fAig = 1;
+    fAig = 0;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "ah" ) ) != EOF )
     {
@@ -15003,6 +15006,7 @@ int Abc_CommandAbc8WriteLogic( Abc_Frame_t * pAbc, int argc, char ** argv )
     pFileName = argv[globalUtilOptind];
 //    vCiNames = Ntl_ManCollectCiNames( pAbc->pAbc8Ntl );
 //    vCoNames = Ntl_ManCollectCoNames( pAbc->pAbc8Ntl );
+    // the problem is duplicated CO names...
     if ( fAig )
     {
         if ( pAbc->pAbc8Aig != NULL )
@@ -16169,12 +16173,14 @@ usage:
 ***********************************************************************/
 int Abc_CommandAbc8Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    Aig_Man_t * pAigNew;
+    void * pNtlNew;
     int c, fVerbose;
     int nPartSize;
     int nConfLimit;
     int nLevelMax;
-    extern Aig_Man_t * Ntl_ManFraig( void * p, Aig_Man_t * pAig, int nPartSize, int nConfLimit, int nLevelMax, int fVerbose );
+    extern Aig_Man_t * Ntl_ManExtract( void * p );
+    extern void * Ntl_ManFraig( void * p, int nPartSize, int nConfLimit, int nLevelMax, int fVerbose );
+    extern void Ntl_ManFree( void * p );
 
     // set defaults
     nPartSize    = 0;
@@ -16234,29 +16240,33 @@ int Abc_CommandAbc8Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
         printf( "Abc_CommandAbc8Fraig(): There is no design to SAT sweep.\n" );
         return 1;
     }
-    if ( pAbc->pAbc8Aig == NULL )
-    {
-        printf( "Abc_CommandAbc8Fraig(): There is no AIG to SAT sweep.\n" );
-        return 1;
-    }
 
     // get the input file name
-    pAigNew = Ntl_ManFraig( pAbc->pAbc8Ntl, pAbc->pAbc8Aig, nPartSize, nConfLimit, nLevelMax, fVerbose );
-    if ( pAigNew == NULL )
+    pNtlNew = Ntl_ManFraig( pAbc->pAbc8Ntl, nPartSize, nConfLimit, nLevelMax, fVerbose );
+    if ( pNtlNew == NULL )
     {
         printf( "Abc_CommandAbc8Fraig(): Tranformation of the AIG has failed.\n" );
         return 1;
     }
-    if ( pAbc->pAbc8Aig )
-        Aig_ManStop( pAbc->pAbc8Aig );
-    pAbc->pAbc8Aig = pAigNew;
 
-    Abc_CommandAbc8Sweep( pAbc, 0, NULL );
+    Abc_FrameClearDesign(); 
+    pAbc->pAbc8Ntl = pNtlNew;
+    if ( pAbc->pAbc8Ntl == NULL )
+    {
+        printf( "Abc_CommandAbc8Fraig(): Reading BLIF has failed.\n" );
+        return 1;
+    }
+    pAbc->pAbc8Aig = Ntl_ManExtract( pAbc->pAbc8Ntl );
+    if ( pAbc->pAbc8Aig == NULL )
+    {
+        printf( "Abc_CommandAbc8Fraig(): AIG extraction has failed.\n" );
+        return 1;
+    }
     return 0;
 
 usage:
     fprintf( stdout, "usage: *fraig [-P num] [-C num] [-L num] [-vh]\n" );
-    fprintf( stdout, "\t         performs SAT sweeping with white-boxes\n" );
+    fprintf( stdout, "\t         applies SAT sweeping to netlist with white-boxes\n" );
     fprintf( stdout, "\t-P num : partition size (0 = partitioning is not used) [default = %d]\n", nPartSize );
     fprintf( stdout, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfLimit );
     fprintf( stdout, "\t-L num : limit on node level to fraig (0 = fraig all nodes) [default = %d]\n", nLevelMax );
@@ -16278,12 +16288,13 @@ usage:
 ***********************************************************************/
 int Abc_CommandAbc8Scl( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    Aig_Man_t * pAigNew;
+    void * pNtlNew;
     int c;
     int fLatchConst;
     int fLatchEqual;
     int fVerbose;
-    extern Aig_Man_t * Ntl_ManScl( void * p, Aig_Man_t * pAig, int fLatchConst, int fLatchEqual, int fVerbose );
+    extern Aig_Man_t * Ntl_ManExtract( void * p );
+    extern void * Ntl_ManScl( void * p, int fLatchConst, int fLatchEqual, int fVerbose );
     extern int Ntl_ManIsComb( void * p );
 
     // set defaults
@@ -16316,35 +16327,39 @@ int Abc_CommandAbc8Scl( Abc_Frame_t * pAbc, int argc, char ** argv )
         printf( "Abc_CommandAbc8Scl(): There is no design to SAT sweep.\n" );
         return 1;
     }
-    if ( pAbc->pAbc8Aig == NULL )
-    {
-        printf( "Abc_CommandAbc8Scl(): There is no AIG to SAT sweep.\n" );
-        return 1;
-    }
 
     if ( Ntl_ManIsComb(pAbc->pAbc8Ntl) )
     {
-        fprintf( stdout, "The network is combinational (run \"*fraig\").\n" );
+        fprintf( stdout, "Abc_CommandAbc8Scl(): The network is combinational (run \"*fraig\").\n" );
         return 0;
     }
 
     // get the input file name
-    pAigNew = Ntl_ManScl( pAbc->pAbc8Ntl, pAbc->pAbc8Aig, fLatchConst, fLatchEqual, fVerbose );
-    if ( pAigNew == NULL )
+    pNtlNew = Ntl_ManScl( pAbc->pAbc8Ntl, fLatchConst, fLatchEqual, fVerbose );
+    if ( pNtlNew == NULL )
     {
         printf( "Abc_CommandAbc8Scl(): Tranformation of the AIG has failed.\n" );
         return 1;
     }
-    if ( pAbc->pAbc8Aig )
-        Aig_ManStop( pAbc->pAbc8Aig );
-    pAbc->pAbc8Aig = pAigNew;
 
-    Abc_CommandAbc8Sweep( pAbc, 0, NULL );
+    Abc_FrameClearDesign(); 
+    pAbc->pAbc8Ntl = pNtlNew;
+    if ( pAbc->pAbc8Ntl == NULL )
+    {
+        printf( "Abc_CommandAbc8Scl(): Reading BLIF has failed.\n" );
+        return 1;
+    }
+    pAbc->pAbc8Aig = Ntl_ManExtract( pAbc->pAbc8Ntl );
+    if ( pAbc->pAbc8Aig == NULL )
+    {
+        printf( "Abc_CommandAbc8Scl(): AIG extraction has failed.\n" );
+        return 1;
+    }
     return 0;
 
 usage:
     fprintf( stdout, "usage: *scl [-cevh]\n" );
-    fprintf( stdout, "\t         performs sequential cleanup of the current network\n" );
+    fprintf( stdout, "\t         performs sequential cleanup of the netlist\n" );
     fprintf( stdout, "\t         by removing nodes and latches that do not feed into POs\n" );
     fprintf( stdout, "\t-c     : sweep stuck-at latches detected by ternary simulation [default = %s]\n", fLatchConst? "yes": "no" );
     fprintf( stdout, "\t-e     : merge equal latches (same data inputs and init states) [default = %s]\n", fLatchEqual? "yes": "no" );
@@ -16366,12 +16381,13 @@ usage:
 ***********************************************************************/
 int Abc_CommandAbc8Lcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    Aig_Man_t * pAigNew;
+    void * pNtlNew;
     int c;
     int nFramesP;
     int nConfMax;
     int fVerbose;
-    extern Aig_Man_t * Ntl_ManLcorr( void * p, Aig_Man_t * pAig, int nConfMax, int fVerbose );
+    extern Aig_Man_t * Ntl_ManExtract( void * p );
+    extern void * Ntl_ManLcorr( void * p, int nConfMax, int fVerbose );
     extern int Ntl_ManIsComb( void * p );
 
     // set defaults
@@ -16417,38 +16433,42 @@ int Abc_CommandAbc8Lcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     if ( pAbc->pAbc8Ntl == NULL )
     {
-        printf( "Abc_CommandAbc8Ssw(): There is no design to SAT sweep.\n" );
-        return 1;
-    }
-    if ( pAbc->pAbc8Aig == NULL )
-    {
-        printf( "Abc_CommandAbc8Ssw(): There is no AIG to SAT sweep.\n" );
+        printf( "Abc_CommandAbc8Lcorr(): There is no design to SAT sweep.\n" );
         return 1;
     }
 
     if ( Ntl_ManIsComb(pAbc->pAbc8Ntl) )
     {
-        fprintf( stdout, "The network is combinational (run \"*fraig\").\n" );
+        fprintf( stdout, "Abc_CommandAbc8Lcorr(): The network is combinational (run \"*fraig\").\n" );
         return 0;
     }
 
     // get the input file name
-    pAigNew = Ntl_ManLcorr( pAbc->pAbc8Ntl, pAbc->pAbc8Aig, nConfMax, fVerbose );
-    if ( pAigNew == NULL )
+    pNtlNew = Ntl_ManLcorr( pAbc->pAbc8Ntl, nConfMax, fVerbose );
+    if ( pNtlNew == NULL )
     {
-        printf( "Abc_CommandAbc8Ssw(): Tranformation of the AIG has failed.\n" );
+        printf( "Abc_CommandAbc8Lcorr(): Tranformation of the AIG has failed.\n" );
         return 1;
     }
-    if ( pAbc->pAbc8Aig )
-        Aig_ManStop( pAbc->pAbc8Aig );
-    pAbc->pAbc8Aig = pAigNew;
 
-    Abc_CommandAbc8Sweep( pAbc, 0, NULL );
+    Abc_FrameClearDesign(); 
+    pAbc->pAbc8Ntl = pNtlNew;
+    if ( pAbc->pAbc8Ntl == NULL )
+    {
+        printf( "Abc_CommandAbc8Lcorr(): Reading BLIF has failed.\n" );
+        return 1;
+    }
+    pAbc->pAbc8Aig = Ntl_ManExtract( pAbc->pAbc8Ntl );
+    if ( pAbc->pAbc8Aig == NULL )
+    {
+        printf( "Abc_CommandAbc8Lcorr(): AIG extraction has failed.\n" );
+        return 1;
+    }
     return 0;
 
 usage:
     fprintf( stdout, "usage: *lcorr [-C num] [-vh]\n" );
-    fprintf( stdout, "\t         computes latch correspondence using 1-step induction\n" );
+    fprintf( stdout, "\t         computes latch correspondence for the netlist\n" );
 //    fprintf( stdout, "\t-P num : number of time frames to use as the prefix [default = %d]\n", nFramesP );
     fprintf( stdout, "\t-C num : max conflict number when proving latch equivalence [default = %d]\n", nConfMax );
     fprintf( stdout, "\t-v     : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
@@ -16469,10 +16489,11 @@ usage:
 ***********************************************************************/
 int Abc_CommandAbc8Ssw( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    Aig_Man_t * pAigNew;
+    void * pNtlNew;
     Fra_Ssw_t Pars, * pPars = &Pars;
     int c;
-    extern Aig_Man_t * Ntl_ManSsw( void * p, Aig_Man_t * pAig, Fra_Ssw_t * pPars );
+    extern Aig_Man_t * Ntl_ManExtract( void * p );
+    extern void * Ntl_ManSsw( void * p, Fra_Ssw_t * pPars );
     extern int Ntl_ManIsComb( void * p );
 
     // set defaults
@@ -16593,11 +16614,6 @@ int Abc_CommandAbc8Ssw( Abc_Frame_t * pAbc, int argc, char ** argv )
         printf( "Abc_CommandAbc8Ssw(): There is no design to SAT sweep.\n" );
         return 1;
     }
-    if ( pAbc->pAbc8Aig == NULL )
-    {
-        printf( "Abc_CommandAbc8Ssw(): There is no AIG to SAT sweep.\n" );
-        return 1;
-    }
 
     if ( Ntl_ManIsComb(pAbc->pAbc8Ntl) )
     {
@@ -16618,22 +16634,31 @@ int Abc_CommandAbc8Ssw( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // get the input file name
-    pAigNew = Ntl_ManSsw( pAbc->pAbc8Ntl, pAbc->pAbc8Aig, pPars );
-    if ( pAigNew == NULL )
+    pNtlNew = Ntl_ManSsw( pAbc->pAbc8Ntl, pPars );
+    if ( pNtlNew == NULL )
     {
         printf( "Abc_CommandAbc8Ssw(): Tranformation of the AIG has failed.\n" );
         return 1;
     }
-    if ( pAbc->pAbc8Aig )
-        Aig_ManStop( pAbc->pAbc8Aig );
-    pAbc->pAbc8Aig = pAigNew;
 
-    Abc_CommandAbc8Sweep( pAbc, 0, NULL );
+    Abc_FrameClearDesign(); 
+    pAbc->pAbc8Ntl = pNtlNew;
+    if ( pAbc->pAbc8Ntl == NULL )
+    {
+        printf( "Abc_CommandAbc8Ssw(): Reading BLIF has failed.\n" );
+        return 1;
+    }
+    pAbc->pAbc8Aig = Ntl_ManExtract( pAbc->pAbc8Ntl );
+    if ( pAbc->pAbc8Aig == NULL )
+    {
+        printf( "Abc_CommandAbc8Ssw(): AIG extraction has failed.\n" );
+        return 1;
+    }
     return 0;
 
 usage:
     fprintf( stdout, "usage: *ssw [-PQNFL num] [-lrfetvh]\n" );
-    fprintf( stdout, "\t         performs sequential sweep using K-step induction\n" );
+    fprintf( stdout, "\t         performs sequential sweep using K-step induction on the netlist \n" );
     fprintf( stdout, "\t-P num : max partition size (0 = no partitioning) [default = %d]\n", pPars->nPartSize );
     fprintf( stdout, "\t-Q num : partition overlap (0 = no overlap) [default = %d]\n", pPars->nOverSize );
     fprintf( stdout, "\t-N num : number of time frames to use as the prefix [default = %d]\n", pPars->nFramesP );
@@ -16664,11 +16689,10 @@ usage:
 ***********************************************************************/
 int Abc_CommandAbc8Sweep( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    void * pNtlNew;
+    int Counter;
     int fVerbose;
     int c;
-    extern void * Ntl_ManSweep( void * p, Aig_Man_t * pAig, int fVerbose );
-    extern Aig_Man_t * Ntl_ManExtract( void * p );
+    extern int Ntl_ManSweep( void * p, int fVerbose );
 
     // set defaults
     fVerbose = 0;
@@ -16691,34 +16715,75 @@ int Abc_CommandAbc8Sweep( Abc_Frame_t * pAbc, int argc, char ** argv )
         printf( "Abc_CommandAbc8Sweep(): There is no design to sweep.\n" );
         return 1;
     }
-    if ( pAbc->pAbc8Aig == NULL )
-    {
-        printf( "Abc_CommandAbc8Sweep(): There is no AIG to use.\n" );
-        return 1;
-    }
 
     // sweep the current design
-    pNtlNew = Ntl_ManSweep( pAbc->pAbc8Ntl, pAbc->pAbc8Aig, fVerbose );
-    if ( pNtlNew == NULL )
+    Counter = Ntl_ManSweep( pAbc->pAbc8Ntl, fVerbose );
+    if ( Counter == 0 )
+        printf( "The netlist is unchanged by sweep.\n" );
+    return 0;
+
+usage:
+    fprintf( stdout, "usage: *sw [-h]\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-v    : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( stdout, "\t-h    : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc8Zero( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    void * pNtlNew;
+    int fVerbose;
+    int c;
+    extern void Ntl_ManTransformInitValues( void * p );
+
+    // set defaults
+    fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
     {
-        printf( "Abc_CommandAbc8Sweep(): Sweeping has failed.\n" );
-        return 1;
+        switch ( c )
+        {
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
     }
-    // replace
-    Abc_FrameClearDesign(); 
-    pAbc->pAbc8Ntl = pNtlNew;
-    pAbc->pAbc8Aig = Ntl_ManExtract( pAbc->pAbc8Ntl );
-    if ( pAbc->pAbc8Aig == NULL )
+    if ( pAbc->pAbc8Ntl == NULL )
     {
-        printf( "Abc_CommandAbc8Sweep(): AIG extraction has failed.\n" );
+        printf( "Abc_CommandAbc8Zero(): There is no design to convert.\n" );
         return 1;
     }
+
+    // transform the registers
+    pNtlNew = pAbc->pAbc8Ntl;
+    pAbc->pAbc8Ntl = NULL;
+    Ntl_ManTransformInitValues( pNtlNew );
+
+    // replace the design
+    Abc_FrameClearDesign(); 
+    pAbc->pAbc8Ntl = pNtlNew;
     return 0;
 
 usage:
-    fprintf( stdout, "usage: *sw [-h]\n" );
-    fprintf( stdout, "\t        performs structural sweep of the design\n" );
-    fprintf( stdout, "\t        removes dangling nodes, registers, and white-boxes\n" );
+    fprintf( stdout, "usage: *zero [-h]\n" );
+    fprintf( stdout, "\t        converts registers to have constant-0 initial value\n" );
     fprintf( stdout, "\t-v    : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( stdout, "\t-h    : print the command usage\n");
     return 1;
@@ -16746,7 +16811,7 @@ int Abc_CommandAbc8Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
     int nConfLimit;
     int fSmart;
     int nPartSize;
-    extern Aig_Man_t * Ntl_ManCollapse( void * p, int fSeq );
+    extern Aig_Man_t * Ntl_ManCollapse( void * p );
     extern void * Ntl_ManDup( void * pOld );
     extern void Ntl_ManFree( void * p );
     extern void * Ntl_ManInsertNtk( void * p, void * pNtk );
@@ -16827,14 +16892,14 @@ int Abc_CommandAbc8Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // derive AIGs
-    pAig1 = Ntl_ManCollapse( pAbc->pAbc8Ntl, 0 );
+    pAig1 = Ntl_ManCollapse( pAbc->pAbc8Ntl );
     pTemp = Ntl_ManInsertNtk( pAbc->pAbc8Ntl, pAbc->pAbc8Nwk );
     if ( pTemp == NULL )
     {
         printf( "Abc_CommandAbc8Cec(): Inserting the design has failed.\n" );
         return 1;
     }
-    pAig2 = Ntl_ManCollapse( pTemp, 0 );
+    pAig2 = Ntl_ManCollapse( pTemp );
     Ntl_ManFree( pTemp );
 
     // perform verification
@@ -16886,7 +16951,7 @@ int Abc_CommandAbc8DSec( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // set defaults
     nFrames      = 16;
-    fRetimeFirst =  1;
+    fRetimeFirst =  0;
     fFraiging    =  1;
     fVerbose     =  0;
     fVeryVerbose =  0;

src/base/abci/abcAbc8.c

@@ -129,7 +129,7 @@ Abc_Ntk_t * Abc_NtkFromNtkNew( Abc_Ntk_t * pNtkOld, Nwk_Man_t * pNtk )
     Nwk_ManForEachCo( pNtk, pObj, i )
     {
         pObjNew = Abc_NtkCreatePo( pNtkNew );
-        if ( pObj->fCompl )
+        if ( pObj->fInvert )
             pFaninNew = Abc_NtkCreateNodeInv( pNtkNew, Nwk_ObjFanin0(pObj)->pCopy );
         else
             pFaninNew = Nwk_ObjFanin0(pObj)->pCopy;