Improvements to handling boxes and flops.

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

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
     {

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 )

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

src/base/abci/abc.c

@@ -26539,11 +26539,11 @@ int Abc_CommandAbc9Strash( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     else if ( fCollapse && pAbc->pGia->pAigExtra )
     {
-        if ( Gia_ManIsSeqWithBoxes(pAbc->pGia) )
+        if ( Gia_ManIsSeqWithBoxes(pAbc->pGia) || Gia_ManRegBoxNum(pAbc->pGia) )
         {
             Gia_Man_t * pUnshuffled = Gia_ManDupUnshuffleInputs( pAbc->pGia );
             Gia_ManTransferTiming( pUnshuffled, pAbc->pGia );
-            pTemp = Gia_ManDupCollapse( pUnshuffled, pUnshuffled->pAigExtra, NULL, 0 );
+            pTemp = Gia_ManDupCollapse( pUnshuffled, pUnshuffled->pAigExtra, NULL, Gia_ManRegBoxNum(pUnshuffled) > 0 );
             Gia_ManTransferTiming( pAbc->pGia, pUnshuffled );
             Gia_ManStop( pUnshuffled );
         }