Adding integrity check for boxes and flops.

5 files changed, 115 insertions, 23 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 1e9bf6ef..e29689fc 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -1319,6 +1319,7 @@ extern Gia_Man_t *         Gia_ManStgRead( char * pFileName, int kHot, int fVerb
 /*=== giaSweep.c ============================================================*/
 extern Gia_Man_t *         Gia_ManFraigSweepSimple( Gia_Man_t * p, void * pPars );
 extern Gia_Man_t *         Gia_ManSweepWithBoxes( Gia_Man_t * p, void * pParsC, void * pParsS, int fConst, int fEquiv, int fVerbose );
+extern void                Gia_ManCheckIntegrityWithBoxes( Gia_Man_t * p );
 /*=== giaSweeper.c ============================================================*/
 extern Gia_Man_t *         Gia_SweeperStart( Gia_Man_t * p );
 extern void                Gia_SweeperStop( Gia_Man_t * p );
@@ -1351,6 +1352,9 @@ extern Vec_Flt_t *         Gia_ManPrintOutputProb( Gia_Man_t * p );
 /*=== giaTim.c ===========================================================*/
 extern int                 Gia_ManBoxNum( Gia_Man_t * p );
 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_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 533b6cad..69eda95e 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -403,13 +403,15 @@ void Gia_ManPrintStats( Gia_Man_t * p, Gps_Par_t * pPars )
     if ( p->pName )
         Abc_Print( 1, "%s%-8s%s : ", "\033[1;37m", p->pName, "\033[0m" );  // bright
 #endif
-    Abc_Print( 1, "i/o =%7d/%7d", Gia_ManPiNum(p), Gia_ManPoNum(p) );
+    Abc_Print( 1, "i/o =%7d/%7d", 
+        Gia_ManPiNum(p) - Gia_ManBoxCiNum(p) - Gia_ManRegBoxNum(p), 
+        Gia_ManPoNum(p) - Gia_ManBoxCoNum(p) - Gia_ManRegBoxNum(p) );
     if ( Gia_ManConstrNum(p) )
         Abc_Print( 1, "(c=%d)", Gia_ManConstrNum(p) );
     if ( Gia_ManRegNum(p) )
         Abc_Print( 1, "  ff =%7d", Gia_ManRegNum(p) );
-    if ( p->vRegClasses )
-        Abc_Print( 1, "  boxff =%d(%d)", Vec_IntSize(p->vRegClasses), Vec_IntFindMax(p->vRegClasses) );
+    if ( Gia_ManRegBoxNum(p) )
+        Abc_Print( 1, "  boxff =%d(%d)", Gia_ManRegBoxNum(p), Vec_IntFindMax(p->vRegClasses) );
 
 #ifdef WIN32
     {
@@ -433,7 +435,7 @@ void Gia_ManPrintStats( Gia_Man_t * p, Gps_Par_t * pPars )
     if ( Gia_ManHasChoices(p) )
         Abc_Print( 1, "  ch =%5d", Gia_ManChoiceNum(p) );
     if ( p->pManTime )
-        Abc_Print( 1, "  box = %d", Gia_ManBoxNum(p) - Gia_ManRegBoxNum(p) );
+        Abc_Print( 1, "  box = %d", Gia_ManNonRegBoxNum(p) );
     if ( pPars && pPars->fMuxXor )
         printf( "\nXOR/MUX " ), Gia_ManPrintMuxStats( p );
     if ( pPars && pPars->fSwitch )
@@ -475,6 +477,17 @@ void Gia_ManPrintStats( Gia_Man_t * p, Gps_Par_t * pPars )
 //    }
     if ( p->vInitClasses )
         Gia_ManPrintInitClasses( p->vInitClasses );
+    // check integrity of boxes
+    Gia_ManCheckIntegrityWithBoxes( p );
+/*
+    if ( Gia_ManRegBoxNum(p) )
+    {
+        int i, Limit = Vec_IntFindMax(p->vRegClasses);
+        for ( i = 1; i <= Limit; i++ )
+            printf( "%d ", Vec_IntCountEntry(p->vRegClasses, i) );
+        printf( "\n" );
+    }
+*/
     if ( pPars && pPars->fTents )
     {
 /*
diff --git a/src/aig/gia/giaMfs.c b/src/aig/gia/giaMfs.c
index 32322ab2..039b6654 100644
--- a/src/aig/gia/giaMfs.c
+++ b/src/aig/gia/giaMfs.c
@@ -404,6 +404,8 @@ Gia_Man_t * Gia_ManPerformMfs( Gia_Man_t * p, Sfm_Par_t * pPars )
         pNew = Gia_ManInsertMfs( p, pNtk );
         if( pPars->fVerbose )
             Abc_Print( 1, "The network has %d nodes changed by \"&mfs\".\n", nNodes );
+        // check integrity
+        //Gia_ManCheckIntegrityWithBoxes( pNew );
     }
     Sfm_NtkFree( pNtk );
     return pNew;
diff --git a/src/aig/gia/giaSweep.c b/src/aig/gia/giaSweep.c
index 76176d80..682e39c9 100644
--- a/src/aig/gia/giaSweep.c
+++ b/src/aig/gia/giaSweep.c
@@ -361,6 +361,75 @@ Gia_Man_t * Gia_ManFraigReduceGia( Gia_Man_t * p, int * pReprs )
 
 /**Function*************************************************************
 
+  Synopsis    [Compute the set of CIs representing carry-outs of boxes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Gia_ManComputeCarryOuts( Gia_Man_t * p )
+{
+    Gia_Obj_t * pObj;
+    Tim_Man_t * pManTime = (Tim_Man_t *)p->pManTime;
+    int i, iLast, iBox, nBoxes =  Tim_ManBoxNum( pManTime );
+    Vec_Int_t * vCarryOuts = Vec_IntAlloc( nBoxes );
+    for ( i = 0; i < nBoxes; i++ )
+    {
+        iLast = Tim_ManBoxInputLast( pManTime, i );
+        pObj = Gia_ObjFanin0( Gia_ManCo(p, iLast) );
+        if ( !Gia_ObjIsCi(pObj) )
+            continue;
+        iBox = Tim_ManBoxForCi( pManTime, Gia_ObjCioId(pObj) );
+        if ( iBox == -1 ) 
+            continue;
+        assert( Gia_ObjIsCi(pObj) );
+        if ( Gia_ObjCioId(pObj) == Tim_ManBoxOutputLast(pManTime, iBox) )
+            Vec_IntPush( vCarryOuts, Gia_ObjId(p, pObj) );
+    }
+    return vCarryOuts;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks integriting of complex flops and carry-chains.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManCheckIntegrityWithBoxes( Gia_Man_t * p )
+{
+    Gia_Obj_t * pObj;
+    Vec_Int_t * vCarryOuts;
+    int i, nCountReg = 0, nCountCarry = 0;
+    if ( p->pManTime == NULL )
+        return;
+    Gia_ManCreateRefs( p );
+    for ( i = Gia_ManPoNum(p) - Gia_ManRegBoxNum(p); i < Gia_ManPoNum(p); i++ )
+    {
+        pObj = Gia_ObjFanin0( Gia_ManPo(p, i) );
+        assert( Gia_ObjIsCi(pObj) );
+        if ( Gia_ObjRefNum(p, pObj) > 1 )
+            nCountReg++;
+    }
+    vCarryOuts = Gia_ManComputeCarryOuts( p );
+    Gia_ManForEachObjVec( vCarryOuts, p, pObj, i )
+        if ( Gia_ObjRefNum(p, pObj) > 1 )
+            nCountCarry++;
+    Vec_IntFree( vCarryOuts );
+    if ( nCountReg || nCountCarry )
+        printf( "Warning: AIG with boxes has internal fanout in %d complex flops and %d carries.\n", nCountReg, nCountCarry );
+    ABC_FREE( p->pRefs );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Computes representatives in terms of the original objects.]
 
   Description []
@@ -373,11 +442,12 @@ Gia_Man_t * Gia_ManFraigReduceGia( Gia_Man_t * p, int * pReprs )
 int * Gia_ManFraigSelectReprs( Gia_Man_t * p, Gia_Man_t * pClp, int fVerbose )
 {
     Gia_Obj_t * pObj;
+    Vec_Int_t * vCarryOuts;
     Tim_Man_t * pManTime = (Tim_Man_t *)p->pManTime;
     int * pReprs   = ABC_FALLOC( int, Gia_ManObjNum(p) );
     int * pClp2Gia = ABC_FALLOC( int, Gia_ManObjNum(pClp) );
-    int i, nBoxes, iLast, iBox, iLitClp, iLitClp2, iReprClp, fCompl;
-    int nConsts = 0, nReprs = 0, Count1 = 0, Count2 = 0;
+    int i, iLitClp, iLitClp2, iReprClp, fCompl;
+    int nConsts = 0, nReprs = 0;
     assert( pManTime != NULL );
     // count the number of equivalent objects
     Gia_ManForEachObj1( pClp, pObj, i )
@@ -402,26 +472,15 @@ int * Gia_ManFraigSelectReprs( Gia_Man_t * p, Gia_Man_t * pClp, int fVerbose )
         pObj = Gia_ObjFanin0( Gia_ManPo(p, i) );
         assert( Gia_ObjIsCi(pObj) );
         pObj->fMark0 = 1;
-        Count1++;
     }
     // mark connects between last box inputs and first box outputs
-    nBoxes =  Tim_ManBoxNum( pManTime );
-    for ( i = 0; i < nBoxes; i++ )
-    {
-        iLast = Tim_ManBoxInputLast( pManTime, i );
-        pObj = Gia_ObjFanin0( Gia_ManCo(p, iLast) );
-        if ( !Gia_ObjIsCi(pObj) )
-            continue;
-        iBox = Tim_ManBoxForCi( pManTime, Gia_ObjCioId(pObj) );
-        if ( iBox == -1 ) 
-            continue;
-        assert( Gia_ObjIsCi(pObj) );
-        if ( Gia_ObjCioId(pObj) == Tim_ManBoxOutputLast(pManTime, iBox) )
-            pObj->fMark0 = 1, Count2++;
-    }
+    vCarryOuts = Gia_ManComputeCarryOuts( p );
+    Gia_ManForEachObjVec( vCarryOuts, p, pObj, i )
+        pObj->fMark0 = 1;
     if ( fVerbose )
-        printf( "Fixed %d flop inputs and %d box/box connections (out of %d boxes).\n", 
-            Count1, Count2, nBoxes - Gia_ManRegBoxNum(p) );
+        printf( "Fixed %d flop inputs and %d box/box connections (out of %d non-flop boxes).\n", 
+            Gia_ManRegBoxNum(p), Vec_IntSize(vCarryOuts), Gia_ManNonRegBoxNum(p) );
+    Vec_IntFree( vCarryOuts );
 
     // compute representatives
     pClp2Gia[0] = 0;
@@ -553,6 +612,8 @@ Gia_Man_t * Gia_ManSweepWithBoxes( Gia_Man_t * p, void * pParsC, void * pParsS,
     pNew = Gia_ManDupNormalize( pTemp = pNew );
     Gia_ManTransferTiming( pNew, pTemp );
     Gia_ManStop( pTemp );
+    // check integrity
+    //Gia_ManCheckIntegrityWithBoxes( pNew );
     return pNew;
 }
 
diff --git a/src/aig/gia/giaTim.c b/src/aig/gia/giaTim.c
index e1054fa9..ed232e82 100644
--- a/src/aig/gia/giaTim.c
+++ b/src/aig/gia/giaTim.c
@@ -54,6 +54,18 @@ int Gia_ManRegBoxNum( Gia_Man_t * p )
 {
     return p->vRegClasses ? Vec_IntSize(p->vRegClasses) : 0;
 }
+int Gia_ManNonRegBoxNum( Gia_Man_t * p )
+{
+    return Gia_ManBoxNum(p) - Gia_ManRegBoxNum(p);
+}
+int Gia_ManBoxCiNum( Gia_Man_t * p )
+{
+    return p->pManTime ? Gia_ManCiNum(p) - Tim_ManPiNum((Tim_Man_t *)p->pManTime) : 0;
+}
+int Gia_ManBoxCoNum( Gia_Man_t * p )
+{
+    return p->pManTime ? Gia_ManCoNum(p) - Tim_ManPoNum((Tim_Man_t *)p->pManTime) : 0;
+}
 
 /**Function*************************************************************