Improvements to handling boxes and flops.

4 files changed, 123 insertions, 4 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index e29689fc..7b8020ad 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -1355,6 +1355,7 @@ extern int                 Gia_ManRegBoxNum( Gia_Man_t * p );
 extern int                 Gia_ManNonRegBoxNum( Gia_Man_t * p );
 extern int                 Gia_ManBoxCiNum( Gia_Man_t * p );
 extern int                 Gia_ManBoxCoNum( Gia_Man_t * p );
+extern int                 Gia_ManClockDomainNum( Gia_Man_t * p );
 extern int                 Gia_ManIsSeqWithBoxes( Gia_Man_t * p );
 extern int                 Gia_ManIsNormalized( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManDupNormalize( Gia_Man_t * p );
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index 69eda95e..44dff1a2 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -411,7 +411,7 @@ void Gia_ManPrintStats( Gia_Man_t * p, Gps_Par_t * pPars )
     if ( Gia_ManRegNum(p) )
         Abc_Print( 1, "  ff =%7d", Gia_ManRegNum(p) );
     if ( Gia_ManRegBoxNum(p) )
-        Abc_Print( 1, "  boxff =%d(%d)", Gia_ManRegBoxNum(p), Vec_IntFindMax(p->vRegClasses) );
+        Abc_Print( 1, "  boxff =%d(%d)", Gia_ManRegBoxNum(p), Gia_ManClockDomainNum(p) );
 
 #ifdef WIN32
     {
diff --git a/src/aig/gia/giaSweep.c b/src/aig/gia/giaSweep.c
index 682e39c9..7d383dc7 100644
--- a/src/aig/gia/giaSweep.c
+++ b/src/aig/gia/giaSweep.c
@@ -567,6 +567,109 @@ Gia_Man_t * Gia_ManFraigSweepSimple( Gia_Man_t * p, void * pPars )
 
 /**Function*************************************************************
 
+  Synopsis    [Computes equivalences for one clock domain.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManSweepComputeOneDomainEquivs( Gia_Man_t * p, Vec_Int_t * vRegClasses, int iDom, void * pParsS, int fConst, int fEquiv, int fVerbose )
+{
+    Gia_Man_t * pNew;
+    Gia_Obj_t * pObj;
+    Vec_Int_t * vPerm;
+    int i, Class, nFlops;
+    int nDoms = Vec_IntFindMax(vRegClasses);
+    assert( iDom >= 1 && iDom <= nDoms );
+    assert( p->pManTime == NULL );
+    assert( Gia_ManRegNum(p) > 0 );
+    // create required flop permutation
+    vPerm = Vec_IntAlloc( Gia_ManRegNum(p) );
+    Vec_IntForEachEntry( vRegClasses, Class, i )
+        if ( Class != iDom )
+            Vec_IntPush( vPerm, i );
+    nFlops = Vec_IntSize( vPerm );
+    Vec_IntForEachEntry( vRegClasses, Class, i )
+        if ( Class == iDom )
+            Vec_IntPush( vPerm, i );
+    nFlops = Vec_IntSize(vPerm) - nFlops;
+    assert( Vec_IntSize(vPerm) == Gia_ManRegNum(p) );
+    // derive new AIG
+    pNew = Gia_ManDupPermFlop( p, vPerm );
+    assert( Gia_ManObjNum(pNew) == Gia_ManObjNum(p) );
+    Vec_IntFree( vPerm );
+    // perform computation of equivalences 
+    pNew->nRegs = nFlops;
+    if ( pParsS )
+        Cec_ManLSCorrespondenceClasses( pNew, (Cec_ParCor_t *)pParsS );
+    else 
+        Gia_ManSeqCleanupClasses( pNew, fConst, fEquiv, fVerbose );
+    pNew->nRegs = Gia_ManRegNum(p);
+    // make new point to old
+    Gia_ManForEachObj( p, pObj, i )
+    {
+        assert( !Abc_LitIsCompl(pObj->Value) );
+        Gia_ManObj(pNew, Abc_Lit2Var(pObj->Value))->Value = Abc_Var2Lit(i, 0);
+    }
+    // transfer
+    Gia_ManDupRemapEquiv( p, pNew );
+    Gia_ManStop( pNew );
+}
+Gia_Man_t * Gia_ManSweepWithBoxesAndDomains( Gia_Man_t * p, void * pParsS, int fConst, int fEquiv, int fVerbose )
+{ 
+    Gia_Man_t * pClp, * pNew, * pTemp;
+    int nDoms = Vec_IntFindMax(p->vRegClasses);
+    int * pReprs, iDom;
+    assert( Gia_ManRegNum(p) == 0 );
+    assert( p->pAigExtra != NULL );
+    assert( nDoms > 1 );
+    // order AIG objects
+    pNew = Gia_ManDupUnnormalize( p );
+    if ( pNew == NULL )
+        return NULL;
+    Gia_ManTransferTiming( pNew, p );
+    // iterate over domains
+    for ( iDom = 1; iDom <= nDoms; iDom++ )
+    {
+        if ( Vec_IntCountEntry(pNew->vRegClasses, iDom) < 2 )
+            continue;
+        // find global equivalences
+        pClp = Gia_ManDupCollapse( pNew, pNew->pAigExtra, NULL, 1 );
+        // compute equivalences
+        Gia_ManSweepComputeOneDomainEquivs( pClp, pNew->vRegClasses, iDom, pParsS, fConst, fEquiv, fVerbose );
+        // transfer equivalences
+        pReprs = Gia_ManFraigSelectReprs( pNew, pClp, fVerbose );
+        Gia_ManStop( pClp );
+        // reduce AIG
+        Gia_ManTransferTiming( p, pNew );
+        pNew = Gia_ManFraigReduceGia( pTemp = pNew, pReprs );
+        Gia_ManTransferTiming( pNew, p );
+        Gia_ManStop( pTemp );
+        ABC_FREE( pReprs );
+        // derive new AIG
+        pNew = Gia_ManDupWithBoxes( pTemp = pNew, 1 );
+        Gia_ManStop( pTemp );
+        // report
+        //if ( fVerbose )
+        {
+        printf( "Domain %2d with %5d flops:  ", iDom, Vec_IntCountEntry(pNew->vRegClasses, iDom) );
+        Gia_ManPrintStats( pNew, NULL );
+        }
+    }
+    // normalize the result
+    pNew = Gia_ManDupNormalize( pTemp = pNew );
+    Gia_ManTransferTiming( pNew, pTemp );
+    Gia_ManStop( pTemp );
+    // check integrity
+    //Gia_ManCheckIntegrityWithBoxes( pNew );
+    return pNew;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Reduces root model with scorr.]
 
   Description []
@@ -582,12 +685,15 @@ Gia_Man_t * Gia_ManSweepWithBoxes( Gia_Man_t * p, void * pParsC, void * pParsS,
     int * pReprs;
     assert( Gia_ManRegNum(p) == 0 );
     assert( p->pAigExtra != NULL );
+    // consider seq synthesis with multiple clock domains
+//    if ( pParsC == NULL && Gia_ManClockDomainNum(p) > 1 )
+//        return Gia_ManSweepWithBoxesAndDomains( p, pParsS, fConst, fEquiv, fVerbose );
     // order AIG objects
     pNew = Gia_ManDupUnnormalize( p );
     if ( pNew == NULL )
         return NULL;
-    // find global equivalences
     Gia_ManTransferTiming( pNew, p );
+    // find global equivalences
     pClp = Gia_ManDupCollapse( pNew, pNew->pAigExtra, NULL, pParsC ? 0 : 1 );
     // compute equivalences
     if ( pParsC )
diff --git a/src/aig/gia/giaTim.c b/src/aig/gia/giaTim.c
index ed232e82..1017308a 100644
--- a/src/aig/gia/giaTim.c
+++ b/src/aig/gia/giaTim.c
@@ -66,6 +66,18 @@ int Gia_ManBoxCoNum( Gia_Man_t * p )
 {
     return p->pManTime ? Gia_ManCoNum(p) - Tim_ManPoNum((Tim_Man_t *)p->pManTime) : 0;
 }
+int Gia_ManClockDomainNum( Gia_Man_t * p )
+{
+    int i, nDoms, Count = 0;
+    if ( p->vRegClasses == NULL )
+        return 0;
+    nDoms = Vec_IntFindMax(p->vRegClasses);
+    assert( Vec_IntCountEntry(p->vRegClasses, 0) == 0 );
+    for ( i = 1; i <= nDoms; i++ )
+        if ( Vec_IntCountEntry(p->vRegClasses, i) > 0 )
+            Count++;
+    return Count;    
+}
 
 /**Function*************************************************************
 
@@ -80,7 +92,7 @@ int Gia_ManBoxCoNum( Gia_Man_t * p )
 ***********************************************************************/
 int Gia_ManIsSeqWithBoxes( Gia_Man_t * p )
 {
-    return (Gia_ManRegNum(p) > 0) && (p->pManTime != NULL) && (Tim_ManBoxNum((Tim_Man_t *)p->pManTime) > 0);
+    return (Gia_ManRegNum(p) > 0 && Gia_ManBoxNum(p) > 0);
 }
 
 /**Function*************************************************************
@@ -152,7 +164,7 @@ Gia_Man_t * Gia_ManDupNormalize( Gia_Man_t * p )
         // copy flops last
         for ( i = nCIs - Gia_ManRegNum(p); i < nCIs; i++ )
             Gia_ManCi(p, i)->Value = Gia_ManAppendCi(pNew);
-        printf( "Warning: Suffled CI order to be correct sequential AIG.\n" );
+        printf( "Warning: Shuffled CI order to be correct sequential AIG.\n" );
     }
     Gia_ManForEachAnd( p, pObj, i )
         pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );