4 files changed, 62 insertions, 5 deletions

diff --git a/src/aig/ntl/ntl.h b/src/aig/ntl/ntl.h
index e1d3edd1..b0f3b1fb 100644
--- a/src/aig/ntl/ntl.h
+++ b/src/aig/ntl/ntl.h
@@ -377,6 +377,7 @@ extern ABC_DLL void            Ntl_ManUnmarkCiCoNets( Ntl_Man_t * p );
 extern ABC_DLL void            Ntl_ManSetZeroInitValues( Ntl_Man_t * p );
 extern ABC_DLL void            Ntl_ManTransformInitValues( Ntl_Man_t * p );
 extern ABC_DLL Vec_Vec_t *     Ntl_ManTransformRegClasses( Ntl_Man_t * pMan, int nSizeMax, int fVerbose );
+extern ABC_DLL void            Ntl_ManFilterRegisterClasses( Aig_Man_t * pAig, Vec_Int_t * vRegClasses, int fVerbose );
 extern ABC_DLL int             Ntl_ManLatchNum( Ntl_Man_t * p );
 extern ABC_DLL int             Ntl_ManIsComb( Ntl_Man_t * p );
 extern ABC_DLL int             Ntl_ModelCombLeafNum( Ntl_Mod_t * p );
diff --git a/src/aig/ntl/ntlExtract.c b/src/aig/ntl/ntlExtract.c
index f6f1ebb2..f4d33cf1 100644
--- a/src/aig/ntl/ntlExtract.c
+++ b/src/aig/ntl/ntlExtract.c
@@ -649,9 +649,9 @@ Aig_Man_t * Ntl_ManCollapseSeq( Ntl_Man_t * p, int nMinDomSize )
     if ( pAig->vClockDoms )
     {
         if ( Vec_VecSize(pAig->vClockDoms) == 0 )
-            printf( "Clock domains are small. Seq synthesis is not performed.\n" );
+            printf( "Register classes are small. Seq synthesis is not performed.\n" );
         else
-            printf( "Performing seq synthesis for %d clock domains.\n", Vec_VecSize(pAig->vClockDoms) );
+            printf( "Performing seq synthesis for %d register classes.\n", Vec_VecSize(pAig->vClockDoms) );
         printf( "\n" );
     }
     return pAig;
diff --git a/src/aig/ntl/ntlFraig.c b/src/aig/ntl/ntlFraig.c
index 6449cc33..bd39956e 100644
--- a/src/aig/ntl/ntlFraig.c
+++ b/src/aig/ntl/ntlFraig.c
@@ -320,6 +320,8 @@ Ntl_Man_t * Ntl_ManScl( Ntl_Man_t * p, int fLatchConst, int fLatchEqual, int fVe
     // perform SCL for the given design
     pTemp = Aig_ManScl( pAigCol, fLatchConst, fLatchEqual, fVerbose );
     Aig_ManStop( pTemp );
+    if ( pNew->vRegClasses && Vec_IntSize(pNew->vRegClasses) && pAigCol->pReprs )
+        Ntl_ManFilterRegisterClasses( pAigCol, pNew->vRegClasses, fVerbose );
 
     // finalize the transformation
     pNew = Ntl_ManFinalize( pAux = pNew, pAig, pAigCol, fVerbose );
@@ -353,6 +355,8 @@ Ntl_Man_t * Ntl_ManLcorr( Ntl_Man_t * p, int nConfMax, int fVerbose )
     // perform SCL for the given design
     pTemp = Fra_FraigLatchCorrespondence( pAigCol, 0, nConfMax, 0, fVerbose, NULL, 0 );
     Aig_ManStop( pTemp );
+    if ( p->vRegClasses && Vec_IntSize(p->vRegClasses) && pAigCol->pReprs )
+        Ntl_ManFilterRegisterClasses( pAigCol, p->vRegClasses, fVerbose );
 
     // finalize the transformation
     pNew = Ntl_ManFinalize( pAux = pNew, pAig, pAigCol, fVerbose );
diff --git a/src/aig/ntl/ntlUtil.c b/src/aig/ntl/ntlUtil.c
index 4fd1762c..51f3b818 100644
--- a/src/aig/ntl/ntlUtil.c
+++ b/src/aig/ntl/ntlUtil.c
@@ -403,7 +403,7 @@ Vec_Vec_t * Ntl_ManTransformRegClasses( Ntl_Man_t * pMan, int nSizeMax, int fVer
         printf( "The number of register clases = %d.\n", nClasses );
         for ( i = 0; i <= ClassMax; i++ )
             if ( pClassNums[i] )
-                printf( "%d:%d  ", i, pClassNums[i] );
+                printf( "(%d, %d)  ", i, pClassNums[i] );
         printf( "\n" );
     }
     // skip if there is only one class
@@ -416,7 +416,7 @@ Vec_Vec_t * Ntl_ManTransformRegClasses( Ntl_Man_t * pMan, int nSizeMax, int fVer
             vPart = Vec_IntStartNatural( Vec_IntSize(pMan->vRegClasses) );
             Vec_PtrPush( vParts, vPart );
         }
-        printf( "There is only one clock domain with %d registers.\n", Vec_IntSize(pMan->vRegClasses) );
+        printf( "There is only one class with %d registers.\n", Vec_IntSize(pMan->vRegClasses) );
         free( pClassNums );
         return (Vec_Vec_t *)vParts;
     }
@@ -434,12 +434,13 @@ Vec_Vec_t * Ntl_ManTransformRegClasses( Ntl_Man_t * pMan, int nSizeMax, int fVer
         Vec_PtrPush( vParts, vPart );
     }
     free( pClassNums );
+    Vec_VecSort( (Vec_Vec_t *)vParts, 1 );
     // report the selected classes
     if ( fVerbose )
     {
         printf( "The number of selected register clases = %d.\n", Vec_PtrSize(vParts) );
         Vec_PtrForEachEntry( vParts, vPart, i )
-            printf( "%d:%d  ", i, Vec_IntSize(vPart) );
+            printf( "(%d, %d)  ", i, Vec_IntSize(vPart) );
         printf( "\n" );
     }
     return (Vec_Vec_t *)vParts;
@@ -447,6 +448,57 @@ Vec_Vec_t * Ntl_ManTransformRegClasses( Ntl_Man_t * pMan, int nSizeMax, int fVer
 
 /**Function*************************************************************
 
+  Synopsis    [Filter register clases using clock-domain information.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntl_ManFilterRegisterClasses( Aig_Man_t * pAig, Vec_Int_t * vRegClasses, int fVerbose )
+{
+    Aig_Obj_t * pObj, * pRepr;
+    int i, k, nOmitted, nTotal;
+    if ( pAig->pReprs == NULL )
+        return;
+    assert( pAig->nRegs > 0 );
+    Aig_ManForEachPi( pAig, pObj, i )
+        pObj->PioNum = -1;
+    k = 0;
+    Aig_ManForEachLoSeq( pAig, pObj, i )
+        pObj->PioNum = k++;
+    // consider equivalences
+    nOmitted = nTotal = 0;
+    Aig_ManForEachObj( pAig, pObj, i )
+    {
+        pRepr = pAig->pReprs[pObj->Id];
+        if ( pRepr == NULL )
+            continue;
+        nTotal++;
+        assert( Aig_ObjIsPi(pObj) );
+        assert( Aig_ObjIsPi(pRepr) || Aig_ObjIsConst1(pRepr) );
+        if ( Aig_ObjIsConst1(pRepr) )
+            continue;
+        assert( pObj->PioNum >= 0 && pRepr->PioNum >= 0 );
+        // remove equivalence if they belong to different classes
+        if ( Vec_IntEntry( vRegClasses, pObj->PioNum ) == 
+             Vec_IntEntry( vRegClasses, pRepr->PioNum ) )
+             continue;
+         pAig->pReprs[pObj->Id] = NULL;
+         nOmitted++;
+    }
+    Aig_ManForEachPi( pAig, pObj, i )
+        pObj->PioNum = -1;
+    if ( fVerbose )
+        printf( "Omitted %d (out of %d) equivs due to register class mismatch.\n", 
+            nOmitted, nTotal );
+}
+
+
+/**Function*************************************************************
+
   Synopsis    [Counts the number of CIs in the model.]
 
   Description []