Version abc80416

12 files changed, 1182 insertions, 22 deletions

diff --git a/abc.dsp b/abc.dsp
index 5f676b48..cffc06f5 100644
--- a/abc.dsp
+++ b/abc.dsp
@@ -42,7 +42,7 @@ RSC=rc.exe
 # PROP Ignore_Export_Lib 0
 # PROP Target_Dir ""
 # ADD BASE CPP /nologo /W3 /GX /O2 /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /c
-# ADD CPP /nologo /W3 /GX /O2 /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /c
+# ADD CPP /nologo /W3 /GX /O2 /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /I "src/aig/saig" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /c
 # ADD BASE RSC /l 0x409 /d "NDEBUG"
 # ADD RSC /l 0x409 /d "NDEBUG"
 BSC32=bscmake.exe
@@ -66,7 +66,7 @@ LINK32=link.exe
 # PROP Ignore_Export_Lib 0
 # PROP Target_Dir ""
 # ADD BASE CPP /nologo /W3 /Gm /GX /ZI /Od /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /GZ /c
-# ADD CPP /nologo /W3 /Gm /GX /ZI /Od /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /GZ /c
+# ADD CPP /nologo /W3 /Gm /GX /ZI /Od /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /I "src/aig/saig" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /GZ /c
 # SUBTRACT CPP /X
 # ADD BASE RSC /l 0x409 /d "_DEBUG"
 # ADD RSC /l 0x409 /d "_DEBUG"
@@ -3229,6 +3229,18 @@ SOURCE=.\src\aig\mfx\mfxStrash.c
 SOURCE=.\src\aig\mfx\mfxWin.c
 # End Source File
 # End Group
+# Begin Group "saig"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\aig\saig\saig.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\saig\saigPhase.c
+# End Source File
+# End Group
 # End Group
 # End Group
 # Begin Group "Header Files"
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 9d6bde98..8593fd76 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -99,6 +99,8 @@ struct Aig_Man_t_
     Aig_Obj_t *      pConst1;        // the constant 1 node
     Aig_Obj_t        Ghost;          // the ghost node
     int              nRegs;          // the number of registers (registers are last POs)
+    int              nTruePis;       // the number of registers (registers are last POs)
+    int              nTruePos;       // the number of registers (registers are last POs)
     int              nAsserts;       // the number of asserts among POs (asserts are first POs)
     // AIG node counters
     int              nObjs[AIG_OBJ_VOID];// the number of objects by type
@@ -486,6 +488,7 @@ extern Aig_Man_t *     Aig_ManStartFrom( Aig_Man_t * p );
 extern Aig_Man_t *     Aig_ManExtractMiter( Aig_Man_t * p, Aig_Obj_t * pNode1, Aig_Obj_t * pNode2 );
 extern void            Aig_ManStop( Aig_Man_t * p );
 extern int             Aig_ManCleanup( Aig_Man_t * p );
+extern int             Aig_ManPiCleanup( Aig_Man_t * p );
 extern void            Aig_ManPrintStats( Aig_Man_t * p );
 /*=== aigMem.c ==========================================================*/
 extern void            Aig_ManStartMemory( Aig_Man_t * p );
diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c
index 4c4b7aad..ee782423 100644
--- a/src/aig/aig/aigMan.c
+++ b/src/aig/aig/aigMan.c
@@ -222,9 +222,9 @@ void Aig_ManStop( Aig_Man_t * p )
 
 /**Function*************************************************************
 
-  Synopsis    [Returns the number of dangling nodes removed.]
+  Synopsis    [Removes combinational logic that does not feed into POs.]
 
-  Description []
+  Description [Returns the number of dangling nodes removed.]
                
   SideEffects []
 
@@ -251,6 +251,37 @@ int Aig_ManCleanup( Aig_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Removes PIs without fanouts.]
+
+  Description [Returns the number of PIs removed.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ManPiCleanup( Aig_Man_t * p )
+{
+    Aig_Obj_t * pObj;
+    int i, k = 0, nPisOld = Aig_ManPiNum(p);
+    Vec_PtrForEachEntry( p->vPis, pObj, i )
+    {
+        if ( i >= Aig_ManPiNum(p) - Aig_ManRegNum(p) )
+            Vec_PtrWriteEntry( p->vPis, k++, pObj );
+        else if ( Aig_ObjRefs(pObj) > 0 )
+            Vec_PtrWriteEntry( p->vPis, k++, pObj );
+        else
+            Vec_PtrWriteEntry( p->vObjs, pObj->Id, NULL );
+    }
+    Vec_PtrShrink( p->vPis, k );
+    p->nObjs[AIG_OBJ_PI] = Vec_PtrSize( p->vPis );
+    if ( Aig_ManRegNum(p) )
+        p->nTruePis = Aig_ManPiNum(p) - Aig_ManRegNum(p);
+    return nPisOld - Aig_ManPiNum(p);
+}
+
+/**Function*************************************************************
+
   Synopsis    [Performs one iteration of AIG rewriting.]
 
   Description []
diff --git a/src/aig/aig/aigScl.c b/src/aig/aig/aigScl.c
index c32f2f4f..34b3482d 100644
--- a/src/aig/aig/aigScl.c
+++ b/src/aig/aig/aigScl.c
@@ -230,6 +230,8 @@ int Aig_ManSeqCleanup( Aig_Man_t * p )
                 
     }
     Vec_PtrFree( vNodes );
+    p->nTruePis = Aig_ManPiNum(p) - Aig_ManRegNum(p); 
+    p->nTruePos = Aig_ManPoNum(p) - Aig_ManRegNum(p); 
     // remove dangling nodes
     return Aig_ManCleanup( p );
 }
diff --git a/src/aig/ntl/ntlExtract.c b/src/aig/ntl/ntlExtract.c
index d474b4dd..18ca1a53 100644
--- a/src/aig/ntl/ntlExtract.c
+++ b/src/aig/ntl/ntlExtract.c
@@ -288,8 +288,8 @@ Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p )
     }
     // report the number of dangling objects
     nUselessObjects = Ntl_ModelNodeNum(pRoot) + Ntl_ModelLut1Num(pRoot) + Ntl_ModelBoxNum(pRoot) - Vec_PtrSize(p->vNodes);
-    if ( nUselessObjects )
-        printf( "The number of nodes that do not feed into POs = %d.\n", nUselessObjects );
+//    if ( nUselessObjects )
+//        printf( "The number of nodes that do not feed into POs = %d.\n", nUselessObjects );
     // cleanup the AIG
     Aig_ManCleanup( p->pAig );
     // extract the timing manager
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
new file mode 100644
index 00000000..ce09fd32
--- /dev/null
+++ b/src/aig/saig/saig.h
@@ -0,0 +1,82 @@
+/**CFile****************************************************************
+
+  FileName    [saig.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Sequential AIG package.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: saig.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef __SAIG_H__
+#define __SAIG_H__
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+static inline int          Saig_ManPiNum( Aig_Man_t * p )          { return p->nTruePis;                     }
+static inline int          Saig_ManPoNum( Aig_Man_t * p )          { return p->nTruePos;                     }
+static inline int          Saig_ManRegNum( Aig_Man_t * p )         { return p->nRegs;                        }
+static inline Aig_Obj_t *  Saig_ManLo( Aig_Man_t * p, int i )      { return (Aig_Obj_t *)Vec_PtrEntry(p->vPis, Saig_ManPiNum(p)+i);   }
+static inline Aig_Obj_t *  Saig_ManLi( Aig_Man_t * p, int i )      { return (Aig_Obj_t *)Vec_PtrEntry(p->vPos, Saig_ManPoNum(p)+i);   }
+
+// iterator over the primary inputs/outputs
+#define Saig_ManForEachPi( p, pObj, i )                                           \
+    Vec_PtrForEachEntryStop( p->vPis, pObj, i, Saig_ManPiNum(p) )
+#define Saig_ManForEachPo( p, pObj, i )                                           \
+    Vec_PtrForEachEntryStop( p->vPos, pObj, i, Saig_ManPoNum(p) )
+// iterator over the latch inputs/outputs
+#define Saig_ManForEachLo( p, pObj, i )                                           \
+    for ( i = 0; (i < Saig_ManRegNum(p)) && (((pObj) = Vec_PtrEntry(p->vPis, i+Saig_ManPiNum(p))), 1); i++ )
+#define Saig_ManForEachLi( p, pObj, i )                                           \
+    for ( i = 0; (i < Saig_ManRegNum(p)) && (((pObj) = Vec_PtrEntry(p->vPos, i+Saig_ManPoNum(p))), 1); i++ )
+// iterator over the latch input and outputs
+#define Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )                               \
+    for ( i = 0; (i < Saig_ManRegNum(p)) && (((pObjLi) = Saig_ManLi(p, i)), 1)    \
+        && (((pObjLo)=Saig_ManLo(p, i)), 1); i++ )
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== saigPhase.c ==========================================================*/
+ 
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/aig/saig/saigPhase.c b/src/aig/saig/saigPhase.c
new file mode 100644
index 00000000..f83666c4
--- /dev/null
+++ b/src/aig/saig/saigPhase.c
@@ -0,0 +1,763 @@
+/**CFile****************************************************************
+
+  FileName    [saigPhase.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Sequential AIG package.]
+
+  Synopsis    [Automated phase abstraction.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: saigPhase.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "saig.h"
+
+/*
+    The algorithm is described in the paper: Per Bjesse and Jim Kukula,
+    "Automatic Phase Abstraction for Formal Verification", ICCAD 2005
+    http://www.iccad.com/data2/iccad/iccad_05acceptedpapers.nsf/9cfb1ebaaf59043587256a6a00031f78/1701ecf34b149e958725702f00708828?OpenDocument
+*/
+
+// the maximum number of cycles of termiry simulation
+#define TSIM_MAX_ROUNDS    10000
+#define TSIM_ONE_SERIES     3000
+
+#define SAIG_XVS0   1
+#define SAIG_XVS1   2
+#define SAIG_XVSX   3
+
+static inline int  Saig_XsimConvertValue( int v )  { return v == 0? SAIG_XVS0 : (v == 1? SAIG_XVS1 : (v == 2? SAIG_XVSX : -1));  }
+
+static inline void Saig_ObjSetXsim( Aig_Obj_t * pObj, int Value )  { pObj->nCuts = Value;  }
+static inline int  Saig_ObjGetXsim( Aig_Obj_t * pObj )             { return pObj->nCuts;   }
+static inline int  Saig_XsimInv( int Value )   
+{ 
+    if ( Value == SAIG_XVS0 )
+        return SAIG_XVS1;
+    if ( Value == SAIG_XVS1 )
+        return SAIG_XVS0;
+    assert( Value == SAIG_XVSX );       
+    return SAIG_XVSX;
+}
+static inline int  Saig_XsimAnd( int Value0, int Value1 )   
+{ 
+    if ( Value0 == SAIG_XVS0 || Value1 == SAIG_XVS0 )
+        return SAIG_XVS0;
+    if ( Value0 == SAIG_XVSX || Value1 == SAIG_XVSX )
+        return SAIG_XVSX;
+    assert( Value0 == SAIG_XVS1 && Value1 == SAIG_XVS1 );
+    return SAIG_XVS1;
+}
+static inline int  Saig_XsimRand2()   
+{
+    return (rand() & 1) ? SAIG_XVS1 : SAIG_XVS0;
+}
+static inline int  Saig_XsimRand3()   
+{
+    int RetValue;
+    do { 
+        RetValue = rand() & 3; 
+    } while ( RetValue == 0 );
+    return RetValue;
+}
+static inline int  Saig_ObjGetXsimFanin0( Aig_Obj_t * pObj )       
+{ 
+    int RetValue;
+    RetValue = Saig_ObjGetXsim(Aig_ObjFanin0(pObj));
+    return Aig_ObjFaninC0(pObj)? Saig_XsimInv(RetValue) : RetValue;
+}
+static inline int  Saig_ObjGetXsimFanin1( Aig_Obj_t * pObj )       
+{ 
+    int RetValue;
+    RetValue = Saig_ObjGetXsim(Aig_ObjFanin1(pObj));
+    return Aig_ObjFaninC1(pObj)? Saig_XsimInv(RetValue) : RetValue;
+}
+static inline void Saig_XsimPrint( FILE * pFile, int Value )   
+{ 
+    if ( Value == SAIG_XVS0 )
+    {
+        fprintf( pFile, "0" );
+        return;
+    }
+    if ( Value == SAIG_XVS1 )
+    {
+        fprintf( pFile, "1" );
+        return;
+    }
+    assert( Value == SAIG_XVSX );       
+    fprintf( pFile, "x" );
+}
+
+// simulation manager
+typedef struct Saig_Tsim_t_ Saig_Tsim_t;
+struct Saig_Tsim_t_
+{
+    Aig_Man_t *      pAig;              // the original AIG manager
+    int              nWords;            // the number of words in the states
+    // ternary state representation
+    Vec_Ptr_t *      vStates;           // the collection of ternary states
+    Aig_MmFixed_t *  pMem;              // memory for ternary states
+    int              nPrefix;           // prefix of the ternary state space
+    int              nCycle;            // cycle of the ternary state space
+    int              nNonXRegs;         // the number of candidate registers
+    Vec_Int_t *      vNonXRegs;         // the candidate registers
+    // hash table for terminary states
+    unsigned **      pBins;
+    int              nBins;
+};
+
+static inline unsigned * Saig_TsiNext( unsigned * pState, int nWords )                      { return *((unsigned **)(pState + nWords));  }
+static inline void       Saig_TsiSetNext( unsigned * pState, int nWords, unsigned * pNext ) { *((unsigned **)(pState + nWords)) = pNext; }
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates simulation manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Saig_Tsim_t * Saig_TsiStart( Aig_Man_t * pAig )
+{
+    Saig_Tsim_t * p;
+    p = (Saig_Tsim_t *)malloc( sizeof(Saig_Tsim_t) );
+    memset( p, 0, sizeof(Saig_Tsim_t) );
+    p->pAig    = pAig;
+    p->nWords  = Aig_BitWordNum( 2*Aig_ManRegNum(pAig) );
+    p->vStates = Vec_PtrAlloc( 1000 );
+    p->pMem    = Aig_MmFixedStart( sizeof(unsigned) * p->nWords + sizeof(unsigned *), 10000 );
+    p->nBins   = Aig_PrimeCudd(TSIM_MAX_ROUNDS/2);
+    p->pBins   = ALLOC( unsigned *, p->nBins );
+    memset( p->pBins, 0, sizeof(unsigned *) * p->nBins );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deallocates simulation manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Saig_TsiStop( Saig_Tsim_t * p )
+{
+    if ( p->vNonXRegs )
+        Vec_IntFree( p->vNonXRegs );
+    Aig_MmFixedStop( p->pMem, 0 );
+    Vec_PtrFree( p->vStates );
+    free( p->pBins );
+    free( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes hash value of the node using its simulation info.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Saig_TsiStateHash( unsigned * pState, int nWords, int nTableSize )
+{
+    static int s_FPrimes[128] = { 
+        1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459, 
+        1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997, 
+        2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543, 
+        2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089, 
+        3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671, 
+        3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243, 
+        4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871, 
+        4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471, 
+        5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073, 
+        6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689, 
+        6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309, 
+        7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933, 
+        8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147
+    };
+    unsigned uHash;
+    int i;
+    uHash = 0;
+    for ( i = 0; i < nWords; i++ )
+        uHash ^= pState[i] * s_FPrimes[i & 0x7F];
+    return uHash % nTableSize;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Count non-X-valued registers in the simulation data.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Saig_TsiCountNonXValuedRegisters( Saig_Tsim_t * p, int nWords )
+{
+    unsigned * pState;
+    int nRegs = p->pAig->nRegs;
+    int Value, i, k;
+    assert( p->vNonXRegs == NULL );
+    p->vNonXRegs = Vec_IntAlloc( 10 );
+    for ( i = 0; i < nRegs; i++ )
+    {
+        Vec_PtrForEachEntry( p->vStates, pState, k )
+        {
+            Value = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i );
+            assert( Value != 0 );
+            if ( Value == SAIG_XVSX )
+                break;
+        }
+        if ( k == Vec_PtrSize(p->vStates) )
+            Vec_IntPush( p->vNonXRegs, i );
+    }
+    return Vec_IntSize(p->vNonXRegs);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Count non-X-valued registers in the simulation data.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Saig_TsiPrintTraces( Saig_Tsim_t * p, int nWords, int nPrefix )
+{
+    unsigned * pState;
+    int nRegs = p->pAig->nRegs;
+    int Value, i, k, Counter = 0;
+    if ( Vec_PtrSize(p->vStates) > 80 )
+        return;
+    for ( i = 0; i < nRegs; i++ )
+    {
+        Vec_PtrForEachEntry( p->vStates, pState, k )
+        {
+            Value = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i );
+            if ( Value == SAIG_XVSX )
+                break;
+        }
+        if ( k == Vec_PtrSize(p->vStates) )
+            Counter++;
+        else
+            continue;
+        // print trace
+        printf( "%5d : %5d  ", Counter, i );
+        Vec_PtrForEachEntryStop( p->vStates, pState, k, Vec_PtrSize(p->vStates)-1 )
+        {
+            Value = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i );
+            if ( Value == SAIG_XVS0 )
+                printf( "0" );
+            else if ( Value == SAIG_XVS1 )
+                printf( "1" );
+            else if ( Value == SAIG_XVSX )
+                printf( "x" );
+            else
+                assert( 0 );
+            if ( k == nPrefix - 1 )
+                printf( "  " );
+        }
+        printf( "\n" );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the number of the state.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Saig_TsiComputePrefix( Saig_Tsim_t * p, unsigned * pState, int nWords )
+{
+    unsigned * pEntry, * pPrev;
+    int Hash, i;
+    Hash = Saig_TsiStateHash( pState, nWords, p->nBins );
+    for ( pEntry = p->pBins[Hash]; pEntry; pEntry = Saig_TsiNext(pEntry, nWords) )
+        if ( !memcmp( pEntry, pState, sizeof(unsigned) * nWords ) )
+        {
+            Vec_PtrForEachEntry( p->vStates, pPrev, i )
+            {
+                if ( pPrev == pEntry )
+                    return i;
+            }
+            assert( 0 );
+            return -1;
+        }
+    return -1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks if the value exists in the table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Saig_TsiStateLookup( Saig_Tsim_t * p, unsigned * pState, int nWords )
+{
+    unsigned * pEntry;
+    int Hash;
+    Hash = Saig_TsiStateHash( pState, nWords, p->nBins );
+    for ( pEntry = p->pBins[Hash]; pEntry; pEntry = Saig_TsiNext(pEntry, nWords) )
+        if ( !memcmp( pEntry, pState, sizeof(unsigned) * nWords ) )
+            return 1;
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Inserts value into the table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Saig_TsiStateInsert( Saig_Tsim_t * p, unsigned * pState, int nWords )
+{
+    int Hash = Saig_TsiStateHash( pState, nWords, p->nBins );
+    assert( !Saig_TsiStateLookup( p, pState, nWords ) );
+    Saig_TsiSetNext( pState, nWords, p->pBins[Hash] );
+    p->pBins[Hash] = pState;    
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Inserts value into the table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned * Saig_TsiStateNew( Saig_Tsim_t * p )
+{
+    unsigned * pState;
+    pState = (unsigned *)Aig_MmFixedEntryFetch( p->pMem );
+    memset( pState, 0, sizeof(unsigned) * p->nWords );
+    Vec_PtrPush( p->vStates, pState );
+    return pState;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Inserts value into the table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Saig_TsiStatePrint( Saig_Tsim_t * p, unsigned * pState )
+{
+    int i, Value, nZeros = 0, nOnes = 0, nDcs = 0;
+    for ( i = 0; i < Aig_ManRegNum(p->pAig); i++ )
+    {
+        Value = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i );
+        if ( Value == SAIG_XVS0 )
+            printf( "0" ), nZeros++;
+        else if ( Value == SAIG_XVS1 )
+            printf( "1" ), nOnes++;
+        else if ( Value == SAIG_XVSX )
+            printf( "x" ), nDcs++;
+        else
+            assert( 0 );
+    }
+    printf( " (0=%5d, 1=%5d, x=%5d)\n", nZeros, nOnes, nDcs );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Count constant values in the state.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Saig_TsiStateCount( Saig_Tsim_t * p, unsigned * pState )
+{
+    Aig_Obj_t * pObjLi, * pObjLo;
+    int i, Value, nCounter = 0;
+    Aig_ManForEachLiLoSeq( p->pAig, pObjLi, pObjLo, i )
+    {
+        Value = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i );
+        nCounter += (Value == SAIG_XVS0 || Value == SAIG_XVS1);
+    }
+    return nCounter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Count constant values in the state.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Saig_TsiStateOrAll( Saig_Tsim_t * pTsi, unsigned * pState )
+{
+    unsigned * pPrev;
+    int i, k;
+    Vec_PtrForEachEntry( pTsi->vStates, pPrev, i )
+    {
+        for ( k = 0; k < pTsi->nWords; k++ )
+            pState[k] |= pPrev[k];
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Cycles the circuit to create a new initial state.]
+
+  Description [Simulates the circuit with random input for the given 
+  number of timeframes to get a better initial state.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Saig_Tsim_t * Saig_ManReachableTernary( Aig_Man_t * p, Vec_Int_t * vInits )
+{
+    Saig_Tsim_t * pTsi;
+    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
+    unsigned * pState;
+    int i, f, Value, nCounter;
+    // allocate the simulation manager
+    pTsi = Saig_TsiStart( p );
+    // initialize the values
+    Saig_ObjSetXsim( Aig_ManConst1(p), SAIG_XVS1 );
+    Saig_ManForEachPi( p, pObj, i )
+        Saig_ObjSetXsim( pObj, SAIG_XVSX );
+    if ( vInits )
+    {
+        Saig_ManForEachLo( p, pObj, i )
+            Saig_ObjSetXsim( pObj, Saig_XsimConvertValue(Vec_IntEntry(vInits, i)) );
+    }
+    else
+    {
+        Saig_ManForEachLo( p, pObj, i )
+            Saig_ObjSetXsim( pObj, SAIG_XVS0 );
+    }
+    // simulate for the given number of timeframes
+    for ( f = 0; f < TSIM_MAX_ROUNDS; f++ )
+    {
+        // collect this state
+        pState = Saig_TsiStateNew( pTsi );
+        Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
+        {
+            Value = Saig_ObjGetXsim(pObjLo);
+            if ( Value & 1 )
+                Aig_InfoSetBit( pState, 2 * i );
+            if ( Value & 2 )
+                Aig_InfoSetBit( pState, 2 * i + 1 );
+        }
+//        printf( "%d ", Saig_TsiStateCount(pTsi, pState) );
+//        Saig_TsiStatePrint( pTsi, pState );
+        // check if this state exists
+        if ( Saig_TsiStateLookup( pTsi, pState, pTsi->nWords ) )
+            return pTsi;
+        // insert this state
+        Saig_TsiStateInsert( pTsi, pState, pTsi->nWords );
+        // simulate internal nodes
+        Aig_ManForEachNode( p, pObj, i )
+            Saig_ObjSetXsim( pObj, Saig_XsimAnd(Saig_ObjGetXsimFanin0(pObj), Saig_ObjGetXsimFanin1(pObj)) );
+        // transfer the latch values
+        Saig_ManForEachLi( p, pObj, i )
+            Saig_ObjSetXsim( pObj, Saig_ObjGetXsimFanin0(pObj) );
+        nCounter = 0;
+        Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
+        {
+            if ( f < TSIM_ONE_SERIES )
+                Saig_ObjSetXsim( pObjLo, Saig_ObjGetXsim(pObjLi) );
+            else
+            {
+                if ( Saig_ObjGetXsim(pObjLi) != Saig_ObjGetXsim(pObjLo) )
+                    Saig_ObjSetXsim( pObjLo, SAIG_XVSX );
+            }
+            nCounter += (Saig_ObjGetXsim(pObjLo) == SAIG_XVS0);
+        }
+    }
+    printf( "Saig_ManReachableTernary(): Did not reach a fixed point after %d iterations (not a bug).\n", TSIM_MAX_ROUNDS );
+    Saig_TsiStop( pTsi );
+    return NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Finds the registers to phase-abstract.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Saig_ManFindRegisters( Saig_Tsim_t * pTsi, int nFrames, int fIgnore, int fVerbose )
+{
+    int Values[256];
+    unsigned * pState;
+    int r, i, k, Reg, Value;
+    int nTests = pTsi->nPrefix + 2 * pTsi->nCycle;
+    assert( nFrames < 256 );
+    r = 0;
+    Vec_IntForEachEntry( pTsi->vNonXRegs, Reg, i )
+    {
+        for ( k = 0; k < nTests; k++ )
+        {
+            if ( k < pTsi->nPrefix + pTsi->nCycle )
+                pState = Vec_PtrEntry( pTsi->vStates, k );
+            else
+                pState = Vec_PtrEntry( pTsi->vStates, k - pTsi->nCycle );
+            Value = (Aig_InfoHasBit( pState, 2 * Reg + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * Reg );
+            assert( Value == SAIG_XVS0 || Value == SAIG_XVS1 );
+            if ( k < nFrames || (fIgnore && k == nFrames) )
+                Values[k % nFrames] = Value;
+            else if ( Values[k % nFrames] != Value )
+                break;
+        }
+        if ( k < nTests )
+            continue;
+        // skip stuck at
+        if ( fIgnore )
+        {
+            for ( k = 1; k < nFrames; k++ )
+                if ( Values[k] != Values[0] )
+                    break;
+            if ( k == nFrames )
+                continue;
+        }
+        // report useful register
+        Vec_IntWriteEntry( pTsi->vNonXRegs, r++, Reg );
+        if ( fVerbose )
+        {
+            printf( "Register %5d has generator: [", Reg );
+            for ( k = 0; k < nFrames; k++ )
+                Saig_XsimPrint( stdout, Values[k] );
+            printf( "]\n" );
+        }
+    }
+    Vec_IntShrink( pTsi->vNonXRegs, r );
+    if ( fVerbose )
+        printf( "Found %3d useful registers.\n", Vec_IntSize(pTsi->vNonXRegs) );
+    return Vec_IntSize(pTsi->vNonXRegs);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Mapping of AIG nodes into frames nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Aig_Obj_t * Saig_ObjFrames( Aig_Obj_t ** pObjMap, int nFs, Aig_Obj_t * pObj, int i )                       { return pObjMap[nFs*pObj->Id + i];  }
+static inline void        Saig_ObjSetFrames( Aig_Obj_t ** pObjMap, int nFs, Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { pObjMap[nFs*pObj->Id + i] = pNode; }
+
+static inline Aig_Obj_t * Saig_ObjChild0Frames( Aig_Obj_t ** pObjMap, int nFs, Aig_Obj_t * pObj, int i ) { return Aig_ObjFanin0(pObj)? Aig_NotCond(Saig_ObjFrames(pObjMap,nFs,Aig_ObjFanin0(pObj),i), Aig_ObjFaninC0(pObj)) : NULL;  }
+static inline Aig_Obj_t * Saig_ObjChild1Frames( Aig_Obj_t ** pObjMap, int nFs, Aig_Obj_t * pObj, int i ) { return Aig_ObjFanin1(pObj)? Aig_NotCond(Saig_ObjFrames(pObjMap,nFs,Aig_ObjFanin1(pObj),i), Aig_ObjFaninC1(pObj)) : NULL;  }
+
+/**Function*************************************************************
+
+  Synopsis    [Performs phase abstraction by unrolling the circuit.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManPerformAbstraction( Saig_Tsim_t * pTsi, int nFrames, int fVerbose )
+{
+    Aig_Man_t * pFrames, * pAig = pTsi->pAig;
+    Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjNew;
+    Aig_Obj_t ** pObjMap;
+    unsigned * pState;
+    int i, f, Reg, Value;
+
+    assert( Vec_IntSize(pTsi->vNonXRegs) > 0 );
+
+    // create mapping for the frames nodes
+    pObjMap = ALLOC( Aig_Obj_t *, nFrames * Aig_ManObjNumMax(pAig) );
+    memset( pObjMap, 0, sizeof(Aig_Obj_t *) * nFrames * Aig_ManObjNumMax(pAig) );
+
+    // start the fraig package
+    pFrames = Aig_ManStart( Aig_ManObjNumMax(pAig) * nFrames );
+    pFrames->pName = Aig_UtilStrsav( pAig->pName );
+    pFrames->pSpec = Aig_UtilStrsav( pAig->pSpec );
+    // map constant nodes
+    for ( f = 0; f < nFrames; f++ )
+        Saig_ObjSetFrames( pObjMap, nFrames, Aig_ManConst1(pAig), f, Aig_ManConst1(pFrames) );
+    // create PI nodes for the frames
+    for ( f = 0; f < nFrames; f++ )
+        Aig_ManForEachPiSeq( pAig, pObj, i )
+            Saig_ObjSetFrames( pObjMap, nFrames, pObj, f, Aig_ObjCreatePi(pFrames) );
+    // create the latches
+    Aig_ManForEachLoSeq( pAig, pObj, i )
+        Saig_ObjSetFrames( pObjMap, nFrames, pObj, 0, Aig_ObjCreatePi(pFrames) );
+
+    // add timeframes
+    for ( f = 0; f < nFrames; f++ )
+    {
+        // replace abstracted registers by constants
+        Vec_IntForEachEntry( pTsi->vNonXRegs, Reg, i )
+        {
+            pObj = Saig_ManLo( pAig, Reg );
+            pState = Vec_PtrEntry( pTsi->vStates, f );
+            Value = (Aig_InfoHasBit( pState, 2 * Reg + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * Reg );
+            assert( Value == SAIG_XVS0 || Value == SAIG_XVS1 );
+            pObjNew = Value? Aig_ManConst1(pFrames) : Aig_ManConst0(pFrames);
+            Saig_ObjSetFrames( pObjMap, nFrames, pObj, f, pObjNew );
+        }
+        // add internal nodes of this frame
+        Aig_ManForEachNode( pAig, pObj, i ) 
+        {
+            pObjNew = Aig_And( pFrames, Saig_ObjChild0Frames(pObjMap,nFrames,pObj,f), Saig_ObjChild1Frames(pObjMap,nFrames,pObj,f) );
+            Saig_ObjSetFrames( pObjMap, nFrames, pObj, f, pObjNew );
+        }
+        // set the latch inputs and copy them into the latch outputs of the next frame
+        Aig_ManForEachLiLoSeq( pAig, pObjLi, pObjLo, i )
+        {
+            pObjNew = Saig_ObjChild0Frames(pObjMap,nFrames,pObjLi,f);
+            if ( f < nFrames - 1 )
+                Saig_ObjSetFrames( pObjMap, nFrames, pObjLo, f+1, pObjNew );
+        }
+    }
+    for ( f = 0; f < nFrames; f++ )
+    {
+        Aig_ManForEachPoSeq( pAig, pObj, i )
+        {
+            pObjNew = Aig_ObjCreatePo( pFrames, Saig_ObjChild0Frames(pObjMap,nFrames,pObj,f) );
+            Saig_ObjSetFrames( pObjMap, nFrames, pObj, f, pObjNew );
+        }
+    }
+    pFrames->nRegs = pAig->nRegs;
+    pFrames->nTruePis = Aig_ManPiNum(pFrames) - Aig_ManRegNum(pFrames); 
+    pFrames->nTruePos = Aig_ManPoNum(pFrames) - Aig_ManRegNum(pFrames); 
+    Aig_ManForEachLiSeq( pAig, pObj, i )
+    {
+        pObjNew = Aig_ObjCreatePo( pFrames, Saig_ObjChild0Frames(pObjMap,nFrames,pObj,nFrames-1) );
+        Saig_ObjSetFrames( pObjMap, nFrames, pObj, nFrames-1, pObjNew );
+    }
+//Aig_ManPrintStats( pFrames );
+    Aig_ManSeqCleanup( pFrames );
+//Aig_ManPrintStats( pFrames );
+    Aig_ManPiCleanup( pFrames );
+//Aig_ManPrintStats( pFrames );
+    free( pObjMap );
+    return pFrames;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs automated phase abstraction.]
+
+  Description [Takes the AIG manager and the array of initial states.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManPhaseAbstract( Aig_Man_t * p, Vec_Int_t * vInits, int nFrames, int fIgnore, int fPrint, int fVerbose )
+{
+    Aig_Man_t * pNew = NULL;
+    Saig_Tsim_t * pTsi;
+    assert( Saig_ManRegNum(p) );
+    assert( Saig_ManPiNum(p) );
+    assert( Saig_ManPoNum(p) );
+    // perform terminary simulation
+    pTsi = Saig_ManReachableTernary( p, vInits );
+    if ( pTsi == NULL )
+        return NULL;
+    // derive information
+    pTsi->nPrefix = Saig_TsiComputePrefix( pTsi, Vec_PtrEntryLast(pTsi->vStates), pTsi->nWords );
+    pTsi->nCycle = Vec_PtrSize(pTsi->vStates) - 1 - pTsi->nPrefix;
+    pTsi->nNonXRegs = Saig_TsiCountNonXValuedRegisters(pTsi, pTsi->nWords);
+    // print statistics
+    if ( fVerbose )
+    {
+        printf( "Prefix = %5d. Cycle = %5d.  Total = %5d. Non-ternary = %5d.\n", 
+            pTsi->nPrefix, pTsi->nCycle, p->nRegs, pTsi->nNonXRegs );
+        if ( pTsi->nNonXRegs < 100 )
+            Saig_TsiPrintTraces( pTsi, pTsi->nWords, pTsi->nPrefix );
+    }
+    if ( fPrint )
+        printf( "Print-out finished. Phase assignment is not performed.\n" );
+    else if ( nFrames < 2 )
+        printf( "The number of frames is less than 2. Phase assignment is not performed.\n" );
+    else if ( pTsi->nCycle == 0 )
+        printf( "The cycle of ternary states is trivial. Phase abstraction cannot be done.\n" );
+    else if ( pTsi->nCycle % nFrames != 0 )
+        printf( "The cycle (%d) is not modulo the number of frames (%d). Phase abstraction cannot be done.\n", pTsi->nCycle, nFrames );
+    else if ( pTsi->nNonXRegs == 0 )
+        printf( "All registers have X-valued states. Phase abstraction cannot be done.\n" );
+    else if ( !Saig_ManFindRegisters( pTsi, nFrames, fIgnore, fVerbose ) )
+        printf( "There is no registers to abstract with %d frames.\n", nFrames );
+    else
+        pNew = Saig_ManPerformAbstraction( pTsi, nFrames, fVerbose );
+    Saig_TsiStop( pTsi );
+    return pNew;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/saig/saig_.c b/src/aig/saig/saig_.c
new file mode 100644
index 00000000..255639e6
--- /dev/null
+++ b/src/aig/saig/saig_.c
@@ -0,0 +1,47 @@
+/**CFile****************************************************************
+
+  FileName    [saig_.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Sequential AIG package.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: saig_.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "saig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 9cc2fd53..6340f358 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -184,6 +184,7 @@ static int Abc_CommandSeqCleanup     ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandCycle          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandXsim           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSim            ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandDarPhase       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandCec            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandDCec           ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -431,6 +432,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Sequential",   "cycle",         Abc_CommandCycle,            1 );
     Cmd_CommandAdd( pAbc, "Sequential",   "xsim",          Abc_CommandXsim,             0 );
     Cmd_CommandAdd( pAbc, "Sequential",   "sim",           Abc_CommandSim,              0 );
+    Cmd_CommandAdd( pAbc, "Sequential",   "phase",         Abc_CommandDarPhase,         1 );
 
     Cmd_CommandAdd( pAbc, "Verification", "cec",           Abc_CommandCec,              0 );
     Cmd_CommandAdd( pAbc, "Verification", "dcec",          Abc_CommandDCec,             0 );
@@ -4944,7 +4946,7 @@ int Abc_CommandAppend( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( Abc_NtkLatchNum(pNtk2) )
     {
         fprintf( pErr, "The second network has latches. Appending does not work for such networks.\n" );
-        return 1;
+        return 0;
     }
 
     // get the new network
@@ -12683,7 +12685,7 @@ int Abc_CommandLcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( Abc_NtkIsComb(pNtk) )
     {
         fprintf( pErr, "The network is combinational (run \"fraig\" or \"fraig_sweep\").\n" );
-        return 1;
+        return 0;
     }
 
     if ( !Abc_NtkIsStrash(pNtk) )
@@ -12774,8 +12776,8 @@ int Abc_CommandSeqCleanup( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( !Abc_NtkLatchNum(pNtk) )
     {
-        fprintf( pErr, "Only works for sequential networks.\n" );
-        return 1;
+        fprintf( pErr, "The network is combinational.\n" );
+        return 0;
     }
     // modify the current network
     pNtkRes = Abc_NtkDarLatchSweep( pNtk, fLatchConst, fLatchEqual, fVerbose );
@@ -12865,8 +12867,8 @@ int Abc_CommandCycle( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( !Abc_NtkLatchNum(pNtk) )
     {
-        fprintf( pErr, "Only works for sequential networks.\n" );
-        return 1;
+        fprintf( pErr, "The network is combinational.\n" );
+        return 0;
     }
 
     if ( Abc_NtkIsStrash(pNtk) )
@@ -12960,8 +12962,8 @@ int Abc_CommandXsim( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( !Abc_NtkLatchNum(pNtk) )
     {
-        fprintf( pErr, "Only works for sequential networks.\n" );
-        return 1;
+        fprintf( pErr, "The network is combinational.\n" );
+        return 0;
     }
     Abc_NtkXValueSimulate( pNtk, nFrames, fXInputs, fXState, fVerbose );
     return 0;
@@ -13056,8 +13058,8 @@ int Abc_CommandSim( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( !Abc_NtkLatchNum(pNtk) )
     {
-        fprintf( pErr, "Only works for sequential networks.\n" );
-        return 1;
+        fprintf( pErr, "The network is combinational.\n" );
+        return 0;
     }
 
     FREE( pNtk->pSeqModel );
@@ -13074,6 +13076,111 @@ usage:
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandDarPhase( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtkRes;
+    int c;
+    int nFrames;
+    int fIgnore;
+    int fPrint;
+    int fVerbose;
+    extern Abc_Ntk_t * Abc_NtkPhaseAbstract( Abc_Ntk_t * pNtk, int nFrames, int fIgnore, int fPrint, int fVerbose );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    nFrames     = 0;
+    fIgnore     = 0;
+    fPrint      = 0;
+    fVerbose    = 1;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Fipvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nFrames = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nFrames < 0 ) 
+                goto usage;
+            break;
+        case 'i':
+            fIgnore ^= 1;
+            break;
+        case 'p':
+            fPrint ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( pErr, "Only works for structrally hashed networks.\n" );
+        return 1;
+    }
+    if ( !Abc_NtkLatchNum(pNtk) )
+    {
+        fprintf( pErr, "The network is combinational.\n" );
+        return 0;
+    }
+    if ( fPrint )
+    {
+        Abc_NtkPhaseAbstract( pNtk, 0, fIgnore, 1, fVerbose );
+        return 0;
+    }
+    // modify the current network
+    pNtkRes = Abc_NtkPhaseAbstract( pNtk, nFrames, fIgnore, 0, fVerbose );
+    if ( pNtkRes == NULL )
+    {
+//        fprintf( pErr, "Phase abstraction has failed.\n" );
+        return 0;
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: phase [-F <num>] [-ipvh]\n" );
+    fprintf( pErr, "\t         performs sequential cleanup of the current network\n" );
+    fprintf( pErr, "\t         by removing nodes and latches that do not feed into POs\n" );
+    fprintf( pErr, "\t-F num : the number of frames to abstract [default = %d]\n", nFrames );
+    fprintf( pErr, "\t-i     : toggle ignoring the initial state [default = %s]\n", fIgnore? "yes": "no" );
+    fprintf( pErr, "\t-p     : toggle printing statistics about generators [default = %s]\n", fPrint? "yes": "no" );
+    fprintf( pErr, "\t-v     : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
 
 
 /**Function*************************************************************
@@ -14474,8 +14581,8 @@ int Abc_CommandIndcut( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( Abc_NtkIsComb(pNtk) )
     {
-        fprintf( pErr, "Only works for sequential networks.\n" );
-        return 1;
+        fprintf( pErr, "The network is combinational.\n" );
+        return 0;
     }
     if ( !Abc_NtkIsStrash(pNtk) )
     {
@@ -14568,8 +14675,8 @@ int Abc_CommandEnlarge( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( Abc_NtkIsComb(pNtk) )
     {
-        fprintf( pErr, "Only works for sequential networks.\n" );
-        return 1;
+        fprintf( pErr, "The network is combinational.\n" );
+        return 0;
     }
     if ( !Abc_NtkIsStrash(pNtk) )
     {
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 26c64099..d7263bbc 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -326,6 +326,77 @@ Abc_Ntk_t * Abc_NtkFromDarSeqSweep( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
 
   Synopsis    [Converts the network from the AIG manager into ABC.]
 
+  Description [This procedure should be called after seq sweeping, 
+  which changes the number of registers.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan )
+{
+    Vec_Ptr_t * vNodes; 
+    Abc_Ntk_t * pNtkNew;
+    Abc_Obj_t * pObjNew;
+    Aig_Obj_t * pObj, * pObjLo, * pObjLi;
+    int i; 
+    assert( pMan->nAsserts == 0 );
+    // perform strashing
+    pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
+    Aig_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew);
+    // create PIs
+    Aig_ManForEachPiSeq( pMan, pObj, i )
+    {
+        pObjNew = Abc_NtkCreatePi( pNtkNew );
+        Abc_ObjAssignName( pObjNew, Abc_ObjName(pObjNew), NULL );
+        pObj->pData = pObjNew;
+    }
+    // create POs
+    Aig_ManForEachPoSeq( pMan, pObj, i )
+    {
+        pObjNew = Abc_NtkCreatePo( pNtkNew );
+        Abc_ObjAssignName( pObjNew, Abc_ObjName(pObjNew), NULL );
+        pObj->pData = pObjNew;
+    }
+    assert( Abc_NtkCiNum(pNtkNew) == Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan) );
+    assert( Abc_NtkCoNum(pNtkNew) == Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan) );
+    // create as many latches as there are registers in the manager
+    Aig_ManForEachLiLoSeq( pMan, pObjLi, pObjLo, i )
+    {
+        pObjNew = Abc_NtkCreateLatch( pNtkNew );
+        pObjLi->pData = Abc_NtkCreateBi( pNtkNew );
+        pObjLo->pData = Abc_NtkCreateBo( pNtkNew );
+        Abc_ObjAddFanin( pObjNew, pObjLi->pData );
+        Abc_ObjAddFanin( pObjLo->pData, pObjNew );
+        Abc_LatchSetInit0( pObjNew );
+        Abc_ObjAssignName( pObjLi->pData, Abc_ObjName(pObjLi->pData), NULL );
+        Abc_ObjAssignName( pObjLo->pData, Abc_ObjName(pObjLo->pData), NULL );
+    }
+    // rebuild the AIG
+    vNodes = Aig_ManDfs( pMan, 1 );
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+        if ( Aig_ObjIsBuf(pObj) )
+            pObj->pData = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj);
+        else
+            pObj->pData = Abc_AigAnd( pNtkNew->pManFunc, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj), (Abc_Obj_t *)Aig_ObjChild1Copy(pObj) );
+    Vec_PtrFree( vNodes );
+    // connect the PO nodes
+    Aig_ManForEachPo( pMan, pObj, i )
+    {
+        pObjNew = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj);
+        Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), pObjNew );
+    }
+    // check the resulting AIG
+    if ( !Abc_NtkCheck( pNtkNew ) )
+        fprintf( stdout, "Abc_NtkFromAigPhase(): Network check has failed.\n" );
+    return pNtkNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Converts the network from the AIG manager into ABC.]
+
   Description []
                
   SideEffects []
@@ -463,8 +534,14 @@ Vec_Int_t * Abc_NtkGetLatchValues( Abc_Ntk_t * pNtk )
     vInits = Vec_IntAlloc( Abc_NtkLatchNum(pNtk) );
     Abc_NtkForEachLatch( pNtk, pLatch, i )
     {
-        assert( Abc_LatchIsInit1(pLatch) == 0 );
-        Vec_IntPush( vInits, Abc_LatchIsInit1(pLatch) );
+        if ( Abc_LatchIsInit0(pLatch) )
+            Vec_IntPush( vInits, 0 );
+        else if ( Abc_LatchIsInit1(pLatch) )
+            Vec_IntPush( vInits, 1 );
+        else if ( Abc_LatchIsInitDc(pLatch) )
+            Vec_IntPush( vInits, 2 );
+        else
+            assert( 0 );
     }
     return vInits;
 }
@@ -1721,6 +1798,42 @@ Abc_Ntk_t * Abc_NtkBalanceExor( Abc_Ntk_t * pNtk, int fUpdateLevel, int fVerbose
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    [Performs phase abstraction.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkPhaseAbstract( Abc_Ntk_t * pNtk, int nFrames, int fIgnore, int fPrint, int fVerbose )
+{
+    extern Aig_Man_t * Saig_ManPhaseAbstract( Aig_Man_t * p, Vec_Int_t * vInits, int nFrames, int fIgnore, int fPrint, int fVerbose );
+    Vec_Int_t * vInits;
+    Abc_Ntk_t * pNtkAig;
+    Aig_Man_t * pMan, * pTemp;
+    pMan = Abc_NtkToDar( pNtk, 0, 0 );
+    pMan->nRegs = Abc_NtkLatchNum(pNtk);
+    pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan); 
+    pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan); 
+    if ( pMan == NULL )
+        return NULL;
+    vInits = Abc_NtkGetLatchValues(pNtk);
+    pMan = Saig_ManPhaseAbstract( pTemp = pMan, vInits, nFrames, fIgnore, fPrint, fVerbose );
+    Vec_IntFree( vInits );
+    Aig_ManStop( pTemp );
+    if ( pMan == NULL )
+        return NULL;
+    pNtkAig = Abc_NtkFromAigPhase( pMan );
+    pNtkAig->pName = Extra_UtilStrsav(pNtk->pName);
+    pNtkAig->pSpec = Extra_UtilStrsav(pNtk->pSpec);
+    Aig_ManStop( pMan );
+    return pNtkAig;
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/map/pcm/module.make b/src/map/pcm/module.make
new file mode 100644
index 00000000..e69de29b
--- /dev/null
+++ b/src/map/pcm/module.make
diff --git a/src/map/ply/module.make b/src/map/ply/module.make
new file mode 100644
index 00000000..e69de29b
--- /dev/null
+++ b/src/map/ply/module.make