Version abc80228

9 files changed, 518 insertions, 137 deletions

diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index ccc34caf..744a044e 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -521,9 +521,14 @@ extern Vec_Ptr_t *     Aig_ManSupports( Aig_Man_t * p );
 extern Vec_Ptr_t *     Aig_ManSupportsInverse( Aig_Man_t * p );
 extern Vec_Ptr_t *     Aig_ManSupportsRegisters( Aig_Man_t * p );
 extern Vec_Ptr_t *     Aig_ManPartitionSmart( Aig_Man_t * p, int nPartSizeLimit, int fVerbose, Vec_Ptr_t ** pvPartSupps );
+extern Vec_Ptr_t *     Aig_ManPartitionSmartRegisters( Aig_Man_t * pAig, int nSuppSizeLimit, int fVerbose );
 extern Vec_Ptr_t *     Aig_ManPartitionNaive( Aig_Man_t * p, int nPartSize );
 extern Vec_Ptr_t *     Aig_ManMiterPartitioned( Aig_Man_t * p1, Aig_Man_t * p2, int nPartSize );
 extern Aig_Man_t *     Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize, int nConfMax, int nLevelMax, int fVerbose );
+/*=== aigPartReg.c =========================================================*/
+extern Vec_Ptr_t *     Aig_ManRegPartitionSimple( Aig_Man_t * pAig, int nPartSize, int nOverSize );
+extern Vec_Ptr_t *     Aig_ManRegPartitionSmart( Aig_Man_t * pAig, int nPartSize );
+extern Aig_Man_t *     Aig_ManRegCreatePart( Aig_Man_t * pAig, Vec_Int_t * vPart, int * pnCountPis, int * pnCountRegs, int ** ppMapBack );
 /*=== aigRepr.c =========================================================*/
 extern void            Aig_ManReprStart( Aig_Man_t * p, int nIdMax );
 extern void            Aig_ManReprStop( Aig_Man_t * p );
@@ -532,6 +537,7 @@ extern void            Aig_ManTransferRepr( Aig_Man_t * pNew, Aig_Man_t * p );
 extern Aig_Man_t *     Aig_ManDupRepr( Aig_Man_t * p, int fOrdered );
 extern Aig_Man_t *     Aig_ManRehash( Aig_Man_t * p );
 extern void            Aig_ManMarkValidChoices( Aig_Man_t * p );
+extern int             Aig_TransferMappedClasses( Aig_Man_t * pAig, Aig_Man_t * pPart, int * pMapBack );
 /*=== aigRet.c ========================================================*/
 extern Aig_Man_t *     Rtm_ManRetime( Aig_Man_t * p, int fForward, int nStepsMax, int fVerbose );
 /*=== aigRetF.c ========================================================*/
diff --git a/src/aig/aig/aigPart.c b/src/aig/aig/aigPart.c
index 7e765f60..df5792b2 100644
--- a/src/aig/aig/aigPart.c
+++ b/src/aig/aig/aigPart.c
@@ -772,6 +772,135 @@ if ( fVerbose )
 
 /**Function*************************************************************
 
+  Synopsis    [Perform the smart partitioning.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Aig_ManPartitionSmartRegisters( Aig_Man_t * pAig, int nSuppSizeLimit, int fVerbose )
+{
+    Vec_Ptr_t * vPartSuppsBit;
+    Vec_Ptr_t * vSupports, * vPartsAll, * vPartsAll2, * vPartSuppsAll;
+    Vec_Int_t * vOne, * vPart, * vPartSupp, * vTemp;
+    int i, iPart, iOut, clk;
+
+    // add output number to each
+clk = clock();
+    vSupports = Aig_ManSupportsRegisters( pAig );
+    assert( Vec_PtrSize(vSupports) == Aig_ManRegNum(pAig) );
+    Vec_PtrForEachEntry( vSupports, vOne, i )
+        Vec_IntPush( vOne, i );
+if ( fVerbose )
+{
+PRT( "Supps", clock() - clk );
+}
+
+    // start char-based support representation
+    vPartSuppsBit = Vec_PtrAlloc( 1000 );
+
+    // create partitions
+clk = clock();
+    vPartsAll = Vec_PtrAlloc( 256 );
+    vPartSuppsAll = Vec_PtrAlloc( 256 );
+    Vec_PtrForEachEntry( vSupports, vOne, i )
+    {
+        // get the output number
+        iOut = Vec_IntPop(vOne);
+        // find closely matching part
+        iPart = Aig_ManPartitionSmartFindPart( vPartSuppsAll, vPartsAll, vPartSuppsBit, nSuppSizeLimit, vOne );
+        if ( iPart == -1 )
+        {
+            // create new partition
+            vPart = Vec_IntAlloc( 32 );
+            Vec_IntPush( vPart, iOut );
+            // create new partition support
+            vPartSupp = Vec_IntDup( vOne );
+            // add this partition and its support
+            Vec_PtrPush( vPartsAll, vPart );
+            Vec_PtrPush( vPartSuppsAll, vPartSupp );
+
+            Vec_PtrPush( vPartSuppsBit, Aig_ManSuppCharStart(vOne, Vec_PtrSize(vSupports)) );
+        }
+        else
+        {
+            // add output to this partition
+            vPart = Vec_PtrEntry( vPartsAll, iPart );
+            Vec_IntPush( vPart, iOut );
+            // merge supports
+            vPartSupp = Vec_PtrEntry( vPartSuppsAll, iPart );
+            vPartSupp = Vec_IntTwoMerge( vTemp = vPartSupp, vOne );
+            Vec_IntFree( vTemp );
+            // reinsert new support
+            Vec_PtrWriteEntry( vPartSuppsAll, iPart, vPartSupp );
+
+            Aig_ManSuppCharAdd( Vec_PtrEntry(vPartSuppsBit, iPart), vOne, Vec_PtrSize(vSupports) );
+        }
+    }
+
+    // stop char-based support representation
+    Vec_PtrForEachEntry( vPartSuppsBit, vTemp, i )
+        free( vTemp );
+    Vec_PtrFree( vPartSuppsBit );
+
+//printf( "\n" );
+if ( fVerbose )
+{
+PRT( "Parts", clock() - clk );
+}
+
+clk = clock();
+    // reorder partitions in the decreasing order of support sizes
+    // remember partition number in each partition support
+    Vec_PtrForEachEntry( vPartSuppsAll, vOne, i )
+        Vec_IntPush( vOne, i );
+    // sort the supports in the decreasing order
+    Vec_VecSort( (Vec_Vec_t *)vPartSuppsAll, 1 );
+    // reproduce partitions
+    vPartsAll2 = Vec_PtrAlloc( 256 );
+    Vec_PtrForEachEntry( vPartSuppsAll, vOne, i )
+        Vec_PtrPush( vPartsAll2, Vec_PtrEntry(vPartsAll, Vec_IntPop(vOne)) );
+    Vec_PtrFree( vPartsAll );
+    vPartsAll = vPartsAll2;
+
+    // compact small partitions
+//    Aig_ManPartitionPrint( p, vPartsAll, vPartSuppsAll );
+    Aig_ManPartitionCompact( vPartsAll, vPartSuppsAll, nSuppSizeLimit );
+    if ( fVerbose )
+//    Aig_ManPartitionPrint( p, vPartsAll, vPartSuppsAll );
+    printf( "Created %d partitions.\n", Vec_PtrSize(vPartsAll) );
+
+if ( fVerbose )
+{
+//PRT( "Comps", clock() - clk );
+}
+
+    // cleanup
+    Vec_VecFree( (Vec_Vec_t *)vSupports );
+//    if ( pvPartSupps == NULL )
+        Vec_VecFree( (Vec_Vec_t *)vPartSuppsAll );
+//    else
+//        *pvPartSupps = vPartSuppsAll;
+
+/*
+    // converts from intergers to nodes
+    Vec_PtrForEachEntry( vPartsAll, vPart, iPart )
+    {
+        vPartPtr = Vec_PtrAlloc( Vec_IntSize(vPart) );
+        Vec_IntForEachEntry( vPart, iOut, i )
+            Vec_PtrPush( vPartPtr, Aig_ManPo(p, iOut) );
+        Vec_IntFree( vPart );
+        Vec_PtrWriteEntry( vPartsAll, iPart, vPartPtr );
+    }
+*/
+    return vPartsAll;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Perform the naive partitioning.]
 
   Description []
@@ -968,16 +1097,21 @@ Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize, int nCon
     Vec_Ptr_t * vParts;
     Aig_Obj_t * pObj;
     void ** ppData;
-    int i, k, m;
+    int i, k, m, nIdMax;
+    assert( Vec_PtrSize(vAigs) > 1 );
+
+    // compute the total number of IDs
+    nIdMax = 0;
+    Vec_PtrForEachEntry( vAigs, pAig, i )
+        nIdMax += Aig_ManObjNumMax(pAig);
 
     // partition the first AIG in the array
-    assert( Vec_PtrSize(vAigs) > 1 );
     pAig = Vec_PtrEntry( vAigs, 0 );
     vParts = Aig_ManPartitionSmart( pAig, nPartSize, 0, NULL );
 
     // start the total fraiged AIG
     pAigTotal = Aig_ManStartFrom( pAig );
-    Aig_ManReprStart( pAigTotal, Vec_PtrSize(vAigs) * Aig_ManObjNumMax(pAig) + 10000 );
+    Aig_ManReprStart( pAigTotal, nIdMax );
     vOutsTotal = Vec_PtrStart( Aig_ManPoNum(pAig) );
 
     // set the PI numbers
diff --git a/src/aig/aig/aigPartReg.c b/src/aig/aig/aigPartReg.c
index 1f218bd8..88ae66ee 100644
--- a/src/aig/aig/aigPartReg.c
+++ b/src/aig/aig/aigPartReg.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "aig.h"
+#include "fra.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -59,14 +60,14 @@ struct Aig_ManPre_t_
   SeeAlso     []
 
 ***********************************************************************/
-Aig_ManPre_t * Aig_ManRegManStart( Aig_Man_t * pAig )
+Aig_ManPre_t * Aig_ManRegManStart( Aig_Man_t * pAig, int nPartSize )
 {
     Aig_ManPre_t * p;
     p = ALLOC( Aig_ManPre_t, 1 );
     memset( p, 0, sizeof(Aig_ManPre_t) );
     p->pAig      = pAig;
     p->vMatrix   = Aig_ManSupportsRegisters( pAig );
-    p->nRegsMax  = 500;
+    p->nRegsMax  = nPartSize;
     p->vParts    = Vec_PtrAlloc(256);
     p->vRegs     = Vec_IntAlloc(256);
     p->vUniques  = Vec_IntAlloc(256);
@@ -105,9 +106,10 @@ void Aig_ManRegManStop( Aig_ManPre_t * p )
 
 /**Function*************************************************************
 
-  Synopsis    [Computes the max-support register that is not taken yet.]
+  Synopsis    [Determines what register to use as the seed.]
 
-  Description []
+  Description [The register is selected as the one having the largest
+  number of non-taken registers in its support.]
                
   SideEffects []
 
@@ -116,12 +118,16 @@ void Aig_ManRegManStop( Aig_ManPre_t * p )
 ***********************************************************************/
 int Aig_ManRegFindSeed( Aig_ManPre_t * p )
 {
-    int i, iMax, nRegsCur, nRegsMax = -1;
+    Vec_Int_t * vRegs;
+    int i, k, iReg, iMax, nRegsCur, nRegsMax = -1;
     for ( i = 0; i < Aig_ManRegNum(p->pAig); i++ )
     {
         if ( p->pfUsedRegs[i] )
             continue;
-        nRegsCur = Vec_IntSize( Vec_PtrEntry(p->vMatrix,i) );
+        nRegsCur = 0;
+        vRegs = Vec_PtrEntry( p->vMatrix, i );
+        Vec_IntForEachEntry( vRegs, iReg, k )
+            nRegsCur += !p->pfUsedRegs[iReg];
         if ( nRegsMax < nRegsCur )
         {
             nRegsMax = nRegsCur;
@@ -157,7 +163,11 @@ int Aig_ManRegFindBestVar( Aig_ManPre_t * p )
         // count the number of new vars
         nNewVars = 0;
         Vec_IntForEachEntry( vSupp, iVarSupp, k )
-            nNewVars += !p->pfPartVars[iVarSupp];
+        {
+            if ( p->pfPartVars[iVarSupp] )
+                continue;
+            nNewVars += 1 + 3 * p->pfUsedRegs[iVarSupp];
+        }
         // quit if there is no new variables
         if ( nNewVars == 0 )
             return iVarFree;
@@ -229,14 +239,15 @@ void Aig_ManRegPartitionAdd( Aig_ManPre_t * p, int iReg )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Aig_ManRegCreatePart( Aig_Man_t * pAig, Vec_Int_t * vPart, int * pnCountPis, int * pnCountRegs )
+Aig_Man_t * Aig_ManRegCreatePart( Aig_Man_t * pAig, Vec_Int_t * vPart, int * pnCountPis, int * pnCountRegs, int ** ppMapBack )
 {
     Aig_Man_t * pNew;
-    Aig_Obj_t * pObj;
+    Aig_Obj_t * pObj, * pObjNew;
     Vec_Ptr_t * vNodes;
     Vec_Ptr_t * vRoots;
     int nOffset, iOut, i;
     int nCountPis, nCountRegs;
+    int * pMapBack;
     // collect roots
     vRoots = Vec_PtrAlloc( Vec_IntSize(vPart) );
     nOffset = Aig_ManPoNum(pAig)-Aig_ManRegNum(pAig);
@@ -275,6 +286,7 @@ Aig_Man_t * Aig_ManRegCreatePart( Aig_Man_t * pAig, Vec_Int_t * vPart, int * pnC
             pObj->pData = Aig_ObjCreatePi(pNew);
     // add variables for the register outputs
     // create fake POs to hold the register outputs
+    nOffset = Aig_ManPiNum(pAig)-Aig_ManRegNum(pAig);
     Vec_IntForEachEntry( vPart, iOut, i )
     {
         pObj = Aig_ManPi(pAig, nOffset+iOut);
@@ -285,7 +297,6 @@ Aig_Man_t * Aig_ManRegCreatePart( Aig_Man_t * pAig, Vec_Int_t * vPart, int * pnC
     Vec_PtrForEachEntry( vNodes, pObj, i )
         if ( Aig_ObjIsNode(pObj) )
             pObj->pData = Aig_And(pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
-    Vec_PtrFree( vNodes );
     // add real POs for the registers
     nOffset = Aig_ManPoNum(pAig)-Aig_ManRegNum(pAig);
     Vec_IntForEachEntry( vPart, iOut, i )
@@ -294,6 +305,30 @@ Aig_Man_t * Aig_ManRegCreatePart( Aig_Man_t * pAig, Vec_Int_t * vPart, int * pnC
         Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
     }
     pNew->nRegs = Vec_IntSize(vPart);
+    // create map
+    if ( ppMapBack )
+    {
+        pMapBack = ALLOC( int, Aig_ManObjNumMax(pNew) );
+        memset( pMapBack, 0xff, sizeof(int) * Aig_ManObjNumMax(pNew) );
+        // map constant nodes
+        pMapBack[0] = 0;
+        // logic cones of register outputs
+        Vec_PtrForEachEntry( vNodes, pObj, i )
+        {
+            pObjNew = Aig_Regular(pObj->pData);
+            pMapBack[pObjNew->Id] = pObj->Id;
+        }
+        // map register outputs
+        nOffset = Aig_ManPiNum(pAig)-Aig_ManRegNum(pAig);
+        Vec_IntForEachEntry( vPart, iOut, i )
+        {
+            pObj = Aig_ManPi(pAig, nOffset+iOut);
+            pObjNew = pObj->pData;
+            pMapBack[pObjNew->Id] = pObj->Id;
+        }
+        *ppMapBack = pMapBack;
+    }
+    Vec_PtrFree( vNodes );
     return pNew;
 }
 
@@ -308,7 +343,7 @@ Aig_Man_t * Aig_ManRegCreatePart( Aig_Man_t * pAig, Vec_Int_t * vPart, int * pnC
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Ptr_t * Aig_ManRegPartitionSmart( Aig_Man_t * pAig )
+Vec_Ptr_t * Aig_ManRegPartitionSmart( Aig_Man_t * pAig, int nPartSize )
 {
     extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact );
 
@@ -316,11 +351,11 @@ Vec_Ptr_t * Aig_ManRegPartitionSmart( Aig_Man_t * pAig )
     Vec_Ptr_t * vResult;
     int iSeed, iNext, i, k;
     // create the manager
-    p = Aig_ManRegManStart( pAig );
+    p = Aig_ManRegManStart( pAig, nPartSize );
     // add partitions as long as registers remain
     for ( i = 0; (iSeed = Aig_ManRegFindSeed(p)) >= 0; i++ )
     {
-printf( "Seed variable = %d.\n", iSeed );
+//printf( "Seed variable = %d.\n", iSeed );
         // clean the current partition information
         Vec_IntClear( p->vRegs );
         Vec_IntClear( p->vUniques );
@@ -339,9 +374,9 @@ printf( "Seed variable = %d.\n", iSeed );
             // add the register to the support of the partition
             Aig_ManRegPartitionAdd( p, iNext );
             // report the result
-printf( "Part %3d  Reg %3d : Free = %4d. Total = %4d. Ratio = %6.2f. Unique = %4d.\n", i, k, 
-                Vec_IntSize(p->vFreeVars), Vec_IntSize(p->vRegs), 
-                1.0*Vec_IntSize(p->vFreeVars)/Vec_IntSize(p->vRegs), Vec_IntSize(p->vUniques) );
+//printf( "Part %3d  Reg %3d : Free = %4d. Total = %4d. Ratio = %6.2f. Unique = %4d.\n", i, k, 
+//                Vec_IntSize(p->vFreeVars), Vec_IntSize(p->vRegs), 
+//                1.0*Vec_IntSize(p->vFreeVars)/Vec_IntSize(p->vRegs), Vec_IntSize(p->vUniques) );
             // quit if there are not free variables
             if ( Vec_IntSize(p->vFreeVars) == 0 )
                 break;
@@ -351,7 +386,7 @@ printf( "Part %3d  Reg %3d : Free = %4d. Total = %4d. Ratio = %6.2f. Unique = %4
 printf( "Part %3d  SUMMARY:  Free = %4d. Total = %4d. Ratio = %6.2f. Unique = %4d.\n", i,
                 Vec_IntSize(p->vFreeVars), Vec_IntSize(p->vRegs), 
                 1.0*Vec_IntSize(p->vFreeVars)/Vec_IntSize(p->vRegs), Vec_IntSize(p->vUniques) );
-printf( "\n" ); 
+//printf( "\n" ); 
     }
     vResult = p->vParts; p->vParts = NULL;
     Aig_ManRegManStop( p );
@@ -369,24 +404,34 @@ printf( "\n" );
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Ptr_t * Aig_ManRegPartitionSimple( Aig_Man_t * pAig, int nPartSize )
+Vec_Ptr_t * Aig_ManRegPartitionSimple( Aig_Man_t * pAig, int nPartSize, int nOverSize )
 {
     Vec_Ptr_t * vResult;
     Vec_Int_t * vPart;
-    int i, k, nParts;
-    nParts = (Aig_ManRegNum(pAig) / nPartSize) + (int)(Aig_ManRegNum(pAig) % nPartSize > 0);
-    vResult = Vec_PtrAlloc( nParts );
-    for ( i = 0; i < nParts; i++ )
+    int i, Counter;
+    if ( nOverSize >= nPartSize )
+    {
+        printf( "Overlap size (%d) if more or equal to the partition size (%d).\n", nOverSize, nPartSize );
+        printf( "Adjusting it to be equal to half of the partition size.\n" );
+        nOverSize = nPartSize/2;
+    }
+    assert( nOverSize < nPartSize );
+    vResult = Vec_PtrAlloc( 100 );
+    for ( Counter = 0; Counter < Aig_ManRegNum(pAig); Counter -= nOverSize )
     {
         vPart = Vec_IntAlloc( nPartSize );
-        for ( k = 0; k < nPartSize; k++ )
-            if ( i * nPartSize + k < Aig_ManRegNum(pAig) )
-                Vec_IntPush( vPart, i * nPartSize + k );
-        Vec_PtrPush( vResult, vPart );
+        for ( i = 0; i < nPartSize; i++ )
+            if ( ++Counter < Aig_ManRegNum(pAig) )
+                Vec_IntPush( vPart, Counter );
+        if ( Vec_IntSize(vPart) <= nOverSize )
+            Vec_IntFree(vPart);
+        else
+            Vec_PtrPush( vResult, vPart );
     }
     return vResult;
 }
 
+
 /**Function*************************************************************
 
   Synopsis    [Computes partitioning of registers.]
@@ -398,26 +443,77 @@ Vec_Ptr_t * Aig_ManRegPartitionSimple( Aig_Man_t * pAig, int nPartSize )
   SeeAlso     []
 
 ***********************************************************************/
-void Aig_ManRegPartitionRun( Aig_Man_t * pAig )
+void Aig_ManRegPartitionTraverse_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vLos )
 {
-    int nPartSize = 1000;
-    char Buffer[100];
-    Aig_Man_t * pTemp;
-    Vec_Ptr_t * vResult;
-    Vec_Int_t * vPart;
-    int i, nCountPis, nCountRegs;
-    vResult = Aig_ManRegPartitionSimple( pAig, nPartSize );
-    printf( "Simple partitioning: %d partitions are saved:\n", Vec_PtrSize(vResult) );
-    Vec_PtrForEachEntry( vResult, vPart, i )
+    if ( Aig_ObjIsTravIdCurrent(p, pObj) )
+        return;
+    Aig_ObjSetTravIdCurrent( p, pObj );
+    if ( Aig_ObjIsPi(pObj) )
     {
-        sprintf( Buffer, "part%03d.aig", i );
-        pTemp = Aig_ManRegCreatePart( pAig, vPart, &nCountPis, &nCountRegs );
-        Ioa_WriteAiger( pTemp, Buffer, 0, 0 );
-        printf( "part%03d.aig : Regs = %4d. PIs = %4d. (True PIs = %4d. Other regs = %4d.)\n", 
-            i, Vec_IntSize(vPart), Aig_ManPiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs );
-        Aig_ManStop( pTemp );
+        if ( pObj->iData >= Aig_ManPiNum(p) - Aig_ManRegNum(p) )
+        {
+            Vec_PtrPush( vLos, pObj );
+            printf( "%d ", pObj->iData - (Aig_ManPiNum(p) - Aig_ManRegNum(p)) );
+        }
+        return;
     }
-    Vec_VecFree( (Vec_Vec_t *)vResult );
+    Aig_ManRegPartitionTraverse_rec( p, Aig_ObjFanin0(pObj), vLos );
+    Aig_ManRegPartitionTraverse_rec( p, Aig_ObjFanin1(pObj), vLos );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes partitioning of registers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Aig_ManRegPartitionTraverse( Aig_Man_t * p )
+{
+    Vec_Ptr_t * vLos;
+    Aig_Obj_t * pObj;
+    int i, nPrev, Counter;
+    // mark the registers
+    Aig_ManForEachPi( p, pObj, i )
+       pObj->iData = i; 
+    // collect registers
+    vLos = Vec_PtrAlloc( Aig_ManRegNum(p) );
+    nPrev = 0;
+    Counter = 0;
+    Aig_ManIncrementTravId( p );
+    Aig_ManForEachLiSeq( p, pObj, i )
+    {
+        ++Counter;
+        printf( "Latch %d: ", Counter );
+        Aig_ManRegPartitionTraverse_rec( p, Aig_ObjFanin0(pObj), vLos );
+printf( "%d=%d \n", Counter, Vec_PtrSize(vLos)-nPrev );
+        nPrev = Vec_PtrSize(vLos);
+    }
+    printf( "Total collected = %d. Total regs = %d.\n", Vec_PtrSize(vLos), Aig_ManRegNum(p) );
+    return vLos;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes partitioning of registers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Aig_ManRegPartitionLinear( Aig_Man_t * pAig, int nPartSize )
+{
+    Vec_Ptr_t * vLos;
+    vLos = Aig_ManRegPartitionTraverse( pAig );
+    Vec_PtrFree( vLos );
+    return NULL;
 }
 
 
diff --git a/src/aig/aig/aigRepr.c b/src/aig/aig/aigRepr.c
index 3a7e382c..eb4325f4 100644
--- a/src/aig/aig/aigRepr.c
+++ b/src/aig/aig/aigRepr.c
@@ -443,6 +443,11 @@ void Aig_ManMarkValidChoices( Aig_Man_t * p )
         }
 //printf( "Node %d is represented by node %d.\n", pObj->Id, pRepr->Id );
         // add choice to the choice node
+        if ( pObj->nRefs > 0 )
+        {
+            Aig_ObjClearRepr( p, pObj );
+            continue;
+        }
         assert( pObj->nRefs == 0 );
         p->pEquivs[pObj->Id] = p->pEquivs[pRepr->Id];
         p->pEquivs[pRepr->Id] = pObj;
@@ -450,6 +455,36 @@ void Aig_ManMarkValidChoices( Aig_Man_t * p )
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    [Transfers the classes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_TransferMappedClasses( Aig_Man_t * pAig, Aig_Man_t * pPart, int * pMapBack )
+{
+    Aig_Obj_t * pObj;
+    int nClasses, k;
+    nClasses = 0;
+    if ( pPart->pReprs )
+    Aig_ManForEachObj( pPart, pObj, k )
+    {
+        if ( pPart->pReprs[pObj->Id] == NULL )
+            continue;
+        nClasses++;
+        Aig_ObjSetRepr( pAig, 
+            Aig_ManObj(pAig, pMapBack[pObj->Id]), 
+            Aig_ManObj(pAig, pMapBack[pPart->pReprs[pObj->Id]->Id]) );
+    }
+    return nClasses;
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/aig/aigScl.c b/src/aig/aig/aigScl.c
index 70586c68..d8ffda9a 100644
--- a/src/aig/aig/aigScl.c
+++ b/src/aig/aig/aigScl.c
@@ -376,10 +376,14 @@ Aig_Man_t * Aig_ManReduceLaches( Aig_Man_t * p, int fVerbose )
         printf( "RBeg = %5d. NBeg = %6d.   ", Aig_ManRegNum(p), Aig_ManNodeNum(p) );
         }
         vMap = Aig_ManReduceLachesOnce( p );
+//Aig_ManPrintStats( p );
         p = Aig_ManRemap( pTemp = p, vMap );
+//Aig_ManPrintStats( p );
         Aig_ManStop( pTemp );
         Vec_PtrFree( vMap );
         Aig_ManSeqCleanup( p );
+//Aig_ManPrintStats( p );
+//printf( "\n" );
         if ( fVerbose )
         {
         printf( "REnd = %5d. NEnd = %6d.   ", Aig_ManRegNum(p), Aig_ManNodeNum(p) );
diff --git a/src/aig/aig/aigTsim.c b/src/aig/aig/aigTsim.c
index a8a3dda8..1d974778 100644
--- a/src/aig/aig/aigTsim.c
+++ b/src/aig/aig/aigTsim.c
@@ -25,6 +25,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 #define TSI_MAX_ROUNDS    1000
+#define TSI_ONE_SERIES     300
 
 #define AIG_XVS0   1
 #define AIG_XVS1   2
@@ -282,6 +283,51 @@ void Aig_TsiStatePrint( Aig_Tsi_t * p, unsigned * pState )
     printf( " (0=%5d, 1=%5d, x=%5d)\n", nZeros, nOnes, nDcs );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Count constant values in the state.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_TsiStateCount( Aig_Tsi_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 == 1 || Value == 2);
+    }
+    return nCounter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Count constant values in the state.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_TsiStateOrAll( Aig_Tsi_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*************************************************************
 
@@ -300,8 +346,8 @@ Vec_Ptr_t * Aig_ManTernarySimulate( Aig_Man_t * p, int fVerbose )
     Aig_Tsi_t * pTsi;
     Vec_Ptr_t * vMap;
     Aig_Obj_t * pObj, * pObjLi, * pObjLo;
-    unsigned * pState, * pPrev;
-    int i, k, f, fConstants, Value, nCounter;
+    unsigned * pState;//, * pPrev;
+    int i, f, fConstants, Value, nCounter;
     // allocate the simulation manager
     pTsi = Aig_TsiStart( p );
     // initialize the values
@@ -323,10 +369,16 @@ Vec_Ptr_t * Aig_ManTernarySimulate( Aig_Man_t * p, int fVerbose )
             if ( Value & 2 )
                 Aig_InfoSetBit( pState, 2 * i + 1 );
         }
+
+//        printf( "%d ", Aig_TsiStateCount(pTsi, pState) );
 //        Aig_TsiStatePrint( pTsi, pState );
         // check if this state exists
         if ( Aig_TsiStateLookup( pTsi, pState, pTsi->nWords ) )
             break;
+//        nCounter = 0;
+//        Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
+//            nCounter += (Aig_ObjGetXsim(pObjLo) == AIG_XVS0);
+//printf( "%d -> ", nCounter );
         // insert this state
         Aig_TsiStateInsert( pTsi, pState, pTsi->nWords );
         // simulate internal nodes
@@ -335,9 +387,23 @@ Vec_Ptr_t * Aig_ManTernarySimulate( Aig_Man_t * p, int fVerbose )
         // transfer the latch values
         Aig_ManForEachLiSeq( p, pObj, i )
             Aig_ObjSetXsim( pObj, Aig_ObjGetXsimFanin0(pObj) );
+        nCounter = 0;
         Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
-            Aig_ObjSetXsim( pObjLo, Aig_ObjGetXsim(pObjLi) );
+        {
+            if ( f < TSI_ONE_SERIES )
+                Aig_ObjSetXsim( pObjLo, Aig_ObjGetXsim(pObjLi) );
+            else
+            {
+                if ( Aig_ObjGetXsim(pObjLi) != Aig_ObjGetXsim(pObjLo) )
+                    Aig_ObjSetXsim( pObjLo, AIG_XVSX );
+            }
+            nCounter += (Aig_ObjGetXsim(pObjLo) == AIG_XVS0);
+        }
+//        if ( f && (f % 1000 == 0) )
+//            printf( "%d \n", f );
+//printf( "%d  ", nCounter );
     }
+//printf( "\n" );
     if ( f == TSI_MAX_ROUNDS )
     {
         printf( "Aig_ManTernarySimulate(): Did not reach a fixed point after %d iterations (not a bug).\n", TSI_MAX_ROUNDS );
@@ -346,11 +412,7 @@ Vec_Ptr_t * Aig_ManTernarySimulate( Aig_Man_t * p, int fVerbose )
     }
     // OR all the states
     pState = Vec_PtrEntry( pTsi->vStates, 0 );
-    Vec_PtrForEachEntry( pTsi->vStates, pPrev, i )
-    {
-        for ( k = 0; k < pTsi->nWords; k++ )
-            pState[k] |= pPrev[k];
-    }
+    Aig_TsiStateOrAll( pTsi, pState );
     // check if there are constants
     fConstants = 0;
     if ( 2*Aig_ManRegNum(p) == 32*pTsi->nWords )
diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index 2ee84f39..cc64b024 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -50,6 +50,7 @@ extern "C" {
 ////////////////////////////////////////////////////////////////////////
 
 typedef struct Fra_Par_t_   Fra_Par_t;
+typedef struct Fra_Ssw_t_   Fra_Ssw_t;
 typedef struct Fra_Man_t_   Fra_Man_t;
 typedef struct Fra_Cla_t_   Fra_Cla_t;
 typedef struct Fra_Sml_t_   Fra_Sml_t;
@@ -86,6 +87,25 @@ struct Fra_Par_t_
     int              fDontShowBar;      // does not show progressbar during fraiging
 };
 
+// seq SAT sweeping parametesr
+struct Fra_Ssw_t_
+{
+    int              nPartSize;         // size of the partition
+    int              nOverSize;         // size of the overlap between partitions
+    int              nFramesP;          // number of frames in the prefix
+    int              nFramesK;          // number of frames for induction (1=simple) 
+    int              nMaxImps;          // max implications to consider
+    int              nMaxLevs;          // max levels to consider
+    int              fUseImps;          // use implications  
+    int              fRewrite;          // enable rewriting of the specualatively reduced model
+    int              fFraiging;         // enable comb SAT sweeping as preprocessing 
+    int              fLatchCorr;        // perform register correspondence
+    int              fWriteImps;        // write implications into a file
+    int              fUse1Hot;          // use one-hotness constraints
+    int              fVerbose;          // enable verbose output 
+    int              nIters;            // the number of iterations performed
+};
+
 // FRAIG equivalence classes
 struct Fra_Cla_t_
 {
@@ -287,7 +307,7 @@ extern double              Fra_ImpComputeStateSpaceRatio( Fra_Man_t * p );
 extern int                 Fra_ImpVerifyUsingSimulation( Fra_Man_t * p );
 extern void                Fra_ImpRecordInManager( Fra_Man_t * p, Aig_Man_t * pNew );
 /*=== fraInd.c ========================================================*/
-extern Aig_Man_t *         Fra_FraigInduction( Aig_Man_t * p, int nFramesP, int nFramesK, int nMaxImps, int nMaxLevs, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fUse1Hot, int fVerbose, int * pnIter );
+extern Aig_Man_t *         Fra_FraigInduction( Aig_Man_t * p, Fra_Ssw_t * pPars );
 /*=== fraIndVer.c =====================================================*/
 extern int                 Fra_InvariantVerify( Aig_Man_t * p, int nFrames, Vec_Int_t * vClauses, Vec_Int_t * vLits );
 /*=== fraLcr.c ========================================================*/
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index ea17706c..0715524e 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -234,7 +234,7 @@ void Fra_FramesAddMore( Aig_Man_t * p, int nFrames )
 
 /**Function*************************************************************
 
-  Synopsis    [Performs choicing of the AIG.]
+  Synopsis    [Performs partitioned sequential SAT sweepingG.]
 
   Description []
                
@@ -243,7 +243,77 @@ void Fra_FramesAddMore( Aig_Man_t * p, int nFrames )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK, int nMaxImps, int nMaxLevs, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fUse1Hot, int fVerbose, int * pnIter )
+Aig_Man_t * Fra_FraigInductionPart( Aig_Man_t * pAig, Fra_Ssw_t * pPars )
+{
+    int fPrintParts = 0;
+    char Buffer[100];
+    Aig_Man_t * pTemp, * pNew;
+    Vec_Ptr_t * vResult;
+    Vec_Int_t * vPart;
+    int * pMapBack;
+    int i, nCountPis, nCountRegs;
+    int nClasses, nPartSize, fVerbose;
+
+    // save parameters
+    nPartSize = pPars->nPartSize; pPars->nPartSize = 0;
+    fVerbose  = pPars->fVerbose;  pPars->fVerbose = 0;
+    // generate partitions
+    vResult = Aig_ManRegPartitionSimple( pAig, nPartSize, pPars->nOverSize );
+//    vResult = Aig_ManPartitionSmartRegisters( pAig, nPartSize, 0 ); 
+//    vResult = Aig_ManRegPartitionSmart( pAig, nPartSize );
+    if ( fPrintParts )
+    {
+        // print partitions
+        printf( "Simple partitioning. %d partitions are saved:\n", Vec_PtrSize(vResult) );
+        Vec_PtrForEachEntry( vResult, vPart, i )
+        {
+            sprintf( Buffer, "part%03d.aig", i );
+            pTemp = Aig_ManRegCreatePart( pAig, vPart, &nCountPis, &nCountRegs, NULL );
+            Ioa_WriteAiger( pTemp, Buffer, 0, 0 );
+            printf( "part%03d.aig : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d.\n", 
+                i, Vec_IntSize(vPart), Aig_ManPiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp) );
+            Aig_ManStop( pTemp );
+        }
+    }
+
+    // perform SSW with partitions
+    Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) );
+    Vec_PtrForEachEntry( vResult, vPart, i )
+    {
+        pTemp = Aig_ManRegCreatePart( pAig, vPart, &nCountPis, &nCountRegs, &pMapBack );
+        // run SSW
+        pNew = Fra_FraigInduction( pTemp, pPars );
+        nClasses = Aig_TransferMappedClasses( pAig, pTemp, pMapBack );
+        if ( fVerbose )
+            printf( "%3d : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d. It = %3d. Cl = %5d.\n", 
+                i, Vec_IntSize(vPart), Aig_ManPiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp), pPars->nIters, nClasses );
+        Aig_ManStop( pNew );
+        Aig_ManStop( pTemp );
+        free( pMapBack );
+    }
+    // remap the AIG
+    pNew = Aig_ManDupRepr( pAig, 0 );
+    Aig_ManSeqCleanup( pNew );
+//    Aig_ManPrintStats( pAig );
+//    Aig_ManPrintStats( pNew );
+    Vec_VecFree( (Vec_Vec_t *)vResult );
+    pPars->nPartSize = nPartSize;
+    pPars->fVerbose = fVerbose;
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs sequential SAT sweeping.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, Fra_Ssw_t * pParams )
 {
     int fUseSimpleCnf = 0;
     int fUseOldSimulation = 0;
@@ -263,13 +333,22 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK,
 
     if ( Aig_ManNodeNum(pManAig) == 0 )
     {
-        if ( pnIter ) *pnIter = 0;
+        pParams->nIters = 0;
         return Aig_ManDup(pManAig, 1);
     }
     assert( Aig_ManLatchNum(pManAig) == 0 );
     assert( Aig_ManRegNum(pManAig) > 0 );
-    assert( nFramesK > 0 );
+    assert( pParams->nFramesK > 0 );
 //Aig_ManShow( pManAig, 0, NULL );
+
+    if ( pParams->fWriteImps && pParams->nPartSize > 0 )
+    {
+        pParams->nPartSize = 0;
+        printf( "Partitioning was disabled to allow implication writing.\n" );
+    }
+    // perform partitioning
+    if ( pParams->nPartSize > 0 && pParams->nPartSize < Aig_ManRegNum(pManAig) )
+        return Fra_FraigInductionPart( pManAig, pParams );
  
     nNodesBeg = Aig_ManNodeNum(pManAig);
     nRegsBeg  = Aig_ManRegNum(pManAig);
@@ -279,16 +358,16 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK,
 
     // get parameters
     Fra_ParamsDefaultSeq( pPars );
-    pPars->nFramesP   = nFramesP;
-    pPars->nFramesK   = nFramesK;
-    pPars->nMaxImps   = nMaxImps;
-    pPars->nMaxLevs   = nMaxLevs;
-    pPars->fVerbose   = fVerbose;
-    pPars->fRewrite   = fRewrite;
-    pPars->fLatchCorr = fLatchCorr;
-    pPars->fUseImps   = fUseImps;
-    pPars->fWriteImps = fWriteImps;
-    pPars->fUse1Hot   = fUse1Hot;
+    pPars->nFramesP   = pParams->nFramesP;
+    pPars->nFramesK   = pParams->nFramesK;
+    pPars->nMaxImps   = pParams->nMaxImps;
+    pPars->nMaxLevs   = pParams->nMaxLevs;
+    pPars->fVerbose   = pParams->fVerbose;
+    pPars->fRewrite   = pParams->fRewrite;
+    pPars->fLatchCorr = pParams->fLatchCorr;
+    pPars->fUseImps   = pParams->fUseImps;
+    pPars->fWriteImps = pParams->fWriteImps;
+    pPars->fUse1Hot   = pParams->fUse1Hot;
 
     assert( !(pPars->nFramesP > 0 && pPars->fUse1Hot) );
     assert( !(pPars->nFramesK > 1 && pPars->fUse1Hot) );
@@ -311,10 +390,10 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK,
         // bug:  r iscas/blif/s5378.blif    ; st; ssw -v
         // bug:  r iscas/blif/s1238.blif    ; st; ssw -v
         // refine the classes with more simulation rounds
-if ( fVerbose )
+if ( pPars->fVerbose )
 printf( "Simulating %d AIG nodes for %d cycles ... ", Aig_ManNodeNum(pManAig), pPars->nFramesP + 32 );
         p->pSml = Fra_SmlSimulateSeq( pManAig, pPars->nFramesP, 32, 1 ); //pPars->nFramesK + 1, 1 );  
-if ( fVerbose ) 
+if ( pPars->fVerbose ) 
 {
 PRT( "Time", clock() - clk );
 }
@@ -408,7 +487,7 @@ p->timeTrav += clock() - clk2;
             Fra_OneHotAssume( p, p->vOneHots );
 
         // report the intermediate results
-        if ( fVerbose )
+        if ( pPars->fVerbose )
         {
             printf( "%3d : Const = %6d. Class = %6d.  L = %6d. LR = %6d.  ", 
                 nIter, Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), 
@@ -428,7 +507,7 @@ clk2 = clock();
         if ( p->pPars->fUse1Hot )
             Fra_OneHotCheck( p, p->vOneHots );
         Fra_FraigSweep( p );
-        if ( fVerbose )
+        if ( pPars->fVerbose )
         {
 //            PRT( "t", clock() - clk2 ); 
         } 
@@ -508,7 +587,7 @@ p->timeTotal = clock() - clk;
 //    if ( Aig_ManPoNum(pManAigNew) - Aig_ManRegNum(pManAigNew) == 1 )
 //        if ( Aig_ObjChild0( Aig_ManPo(pManAigNew,0) ) == Aig_ManConst0(pManAigNew) )
 //            printf( "Proved output constant 0.\n" );
-    if ( pnIter ) *pnIter = nIter;
+    pParams->nIters = nIter;
     return pManAigNew;
 }
 
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index a43d83b1..75d297cf 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -40,73 +40,17 @@
   SeeAlso     []
 
 ***********************************************************************/
-int Fra_FraigSec2( Aig_Man_t * p, int nFramesFix, int fVerbose, int fVeryVerbose )
-{
-    Aig_Man_t * pNew;
-    int nFrames, RetValue, nIter, clk, clkTotal = clock();
-    int fLatchCorr = 0;
-    if ( nFramesFix )
-    {
-        nFrames = nFramesFix;
-        // perform seq sweeping for one frame number
-        pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, 0, fLatchCorr, 0, 0, fVeryVerbose, &nIter );
-    }
-    else
-    {
-        // perform seq sweeping while increasing the number of frames
-        for ( nFrames = 1; ; nFrames++ )
-        {
-clk = clock();
-            pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, 0, fLatchCorr, 0, 0, fVeryVerbose, &nIter );
-            RetValue = Fra_FraigMiterStatus( pNew );
-            if ( fVerbose )
-            {
-                printf( "FRAMES %3d : Iters = %3d. ", nFrames, nIter );
-                if ( RetValue == 1 )
-                    printf( "UNSAT     " );
-                else
-                    printf( "UNDECIDED " );
-PRT( "Time", clock() - clk );
-            }
-            if ( RetValue != -1 )
-                break;
-            Aig_ManStop( pNew );
-        }
-    }
-
-    // get the miter status
-    RetValue = Fra_FraigMiterStatus( pNew );
-    Aig_ManStop( pNew );
-
-    // report the miter
-    if ( RetValue == 1 )
-        printf( "Networks are equivalent after seq sweeping with K=%d frames (%d iters). ", nFrames, nIter );
-    else if ( RetValue == 0 )
-        printf( "Networks are NOT EQUIVALENT. " );
-    else
-        printf( "Networks are UNDECIDED after seq sweeping with K=%d frames (%d iters). ", nFrames, nIter );
-PRT( "Time", clock() - clkTotal );
-    return RetValue;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
 int Fra_FraigSec( Aig_Man_t * p, int nFramesMax, int fRetimeFirst, int fVerbose, int fVeryVerbose )
 {
+    Fra_Ssw_t Pars, * pPars = &Pars;
     Fra_Sml_t * pSml;
     Aig_Man_t * pNew, * pTemp;
     int nFrames, RetValue, nIter, clk, clkTotal = clock();
     int fLatchCorr = 0;
+    // prepare parameters
+    memset( pPars, 0, sizeof(Fra_Ssw_t) );
+    pPars->fLatchCorr  = fLatchCorr;
+    pPars->fVerbose = fVeryVerbose;
 
     pNew = Aig_ManDup( p, 1 );
     if ( fVerbose )
@@ -185,13 +129,14 @@ PRT( "Time", clock() - clk );
     for ( nFrames = 1; nFrames <= nFramesMax; nFrames *= 2 )
     {
 clk = clock();
-        pNew = Fra_FraigInduction( pTemp = pNew, 0, nFrames, 0, 0, 0, 0, fLatchCorr, 0, 0, fVeryVerbose, &nIter );
+        pPars->nFramesK = nFrames;
+        pNew = Fra_FraigInduction( pTemp = pNew, pPars );
         Aig_ManStop( pTemp );
         RetValue = Fra_FraigMiterStatus( pNew );
         if ( fVerbose )
         { 
             printf( "K-step (K=%2d,I=%3d):  Latches = %5d. Nodes = %6d. ", 
-                nFrames, nIter, Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
+                nFrames, pPars->nIters, Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
 PRT( "Time", clock() - clk );
         }
         if ( RetValue != -1 )