New tools for profiling verification miters.

src/aig/gia/gia.h

@@ -198,6 +198,7 @@ struct Gps_Par_t_
     int            fNpn;
     int            fLutProf;
     int            fMuxXor;
+    int            fMiter;
     char *         pDumpFile;
 };
 
@@ -1154,6 +1155,7 @@ extern double              Gia_ManMemory( Gia_Man_t * p );
 extern void                Gia_ManPrintStats( Gia_Man_t * p, Gps_Par_t * pPars ); 
 extern void                Gia_ManPrintStatsShort( Gia_Man_t * p ); 
 extern void                Gia_ManPrintMiterStatus( Gia_Man_t * p ); 
+extern void                Gia_ManPrintStatsMiter( Gia_Man_t * p, int fVerbose );
 extern void                Gia_ManSetRegNum( Gia_Man_t * p, int nRegs );
 extern void                Gia_ManReportImprovement( Gia_Man_t * p, Gia_Man_t * pNew );
 extern void                Gia_ManPrintNpnClasses( Gia_Man_t * p );
@@ -1244,6 +1246,7 @@ extern int                 Gia_SweeperRun( Gia_Man_t * p, Vec_Int_t * vProbeIds,
 extern float               Gia_ManEvaluateSwitching( Gia_Man_t * p );
 extern float               Gia_ManComputeSwitching( Gia_Man_t * p, int nFrames, int nPref, int fProbOne );
 extern Vec_Int_t *         Gia_ManComputeSwitchProbs( Gia_Man_t * pGia, int nFrames, int nPref, int fProbOne );
+extern Vec_Flt_t *         Gia_ManPrintOutputProb( Gia_Man_t * p );
 /*=== giaTim.c ===========================================================*/
 extern Gia_Man_t *         Gia_ManDupNormalize( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManDupUnnormalize( Gia_Man_t * p );

src/aig/gia/giaDup.c

@@ -2760,15 +2760,15 @@ Gia_Man_t * Gia_ManDupSliced( Gia_Man_t * p, int nSuppMax )
   SeeAlso     []
 
 ***********************************************************************/
-void Gia_ManDupWithConstrCollectAnd_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSuper )
+void Gia_ManDupWithConstrCollectAnd_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSuper, int fFirst )
 {
-    if ( Gia_IsComplement(pObj) || !Gia_ObjIsAnd(pObj) )
+    if ( (Gia_IsComplement(pObj) || !Gia_ObjIsAnd(pObj)) && !fFirst )
     {
         Vec_IntPushUnique( vSuper, Gia_ObjToLit(p, pObj) );
         return;
     }
-    Gia_ManDupWithConstrCollectAnd_rec( p, Gia_ObjChild0(pObj), vSuper );
+    Gia_ManDupWithConstrCollectAnd_rec( p, Gia_ObjChild0(pObj), vSuper, 0 );
-    Gia_ManDupWithConstrCollectAnd_rec( p, Gia_ObjChild1(pObj), vSuper );
+    Gia_ManDupWithConstrCollectAnd_rec( p, Gia_ObjChild1(pObj), vSuper, 0 );
 }
 Gia_Man_t * Gia_ManDupWithConstr( Gia_Man_t * p )
 {
@@ -2785,7 +2785,7 @@ Gia_Man_t * Gia_ManDupWithConstr( Gia_Man_t * p )
         return NULL;
     }
     vSuper = Vec_IntAlloc( 100 );
-    Gia_ManDupWithConstrCollectAnd_rec( p, Gia_ObjChild0(pObj), vSuper );
+    Gia_ManDupWithConstrCollectAnd_rec( p, Gia_ObjChild0(pObj), vSuper, 1 );
     assert( Vec_IntSize(vSuper) > 1 );
     // find the highest level
     Gia_ManLevelNum( p );
@@ -2830,6 +2830,86 @@ Gia_Man_t * Gia_ManDupWithConstr( Gia_Man_t * p )
 
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Compares two objects by their distance.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManSortByValue( Gia_Obj_t ** pp1, Gia_Obj_t ** pp2 )
+{
+    int Diff = Gia_Regular(*pp1)->Value - Gia_Regular(*pp2)->Value;
+    if ( Diff < 0 )
+        return -1;
+    if ( Diff > 0 ) 
+        return 1;
+    return 0; 
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Decomposes the miter outputs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManDupDemiter( Gia_Man_t * p, int fVerbose )
+{
+    Vec_Int_t * vSuper;
+    Vec_Ptr_t * vSuperPtr;
+    Gia_Man_t * pNew, * pTemp;
+    Gia_Obj_t * pObj, * pObjPo;
+    int i, iLit;
+    assert( Gia_ManPoNum(p) == 1 );
+    // decompose
+    pObjPo = Gia_ManPo( p, 0 );
+    vSuper = Vec_IntAlloc( 100 );
+    Gia_ManDupWithConstrCollectAnd_rec( p, Gia_ObjFanin0(pObjPo), vSuper, 1 );
+    assert( Vec_IntSize(vSuper) > 1 );
+    // report the result
+    printf( "The miter is %s-decomposable into %d parts.\n", Gia_ObjFaninC0(pObjPo) ? "OR":"AND", Vec_IntSize(vSuper) );
+    // create levels
+    Gia_ManLevelNum( p );
+    Vec_IntForEachEntry( vSuper, iLit, i )
+        Gia_ManObj(p, Abc_Lit2Var(iLit))->Value = Gia_ObjLevelId(p, Abc_Lit2Var(iLit));
+    // create pointer array
+    vSuperPtr = Vec_PtrAlloc( Vec_IntSize(vSuper) );
+    Vec_IntForEachEntry( vSuper, iLit, i )
+        Vec_PtrPush( vSuperPtr, Gia_Lit2Obj(p, iLit) );
+    Vec_PtrSort( vSuperPtr, (int (*)(void))Gia_ManSortByValue );
+    // create new manager
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManHashAlloc( pNew );
+    Gia_ManForEachCi( p, pObj, i )
+        pObj->Value = Gia_ManAppendCi( pNew );
+    Gia_ManForEachAnd( p, pObj, i )
+        pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    // create the outputs
+    Vec_PtrForEachEntry( Gia_Obj_t *, vSuperPtr, pObj, i )
+        Gia_ManAppendCo( pNew, Gia_ObjLitCopy(p, Gia_Obj2Lit(p, pObj)) ^ Gia_ObjFaninC0(pObjPo) );
+    Gia_ManForEachRi( p, pObj, i )
+        Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+    // rehash
+    pNew = Gia_ManCleanup( pTemp = pNew );
+    Gia_ManStop( pTemp );
+    Vec_IntFree( vSuper );
+    Vec_PtrFree( vSuperPtr );
+    return pNew;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/aig/gia/giaMan.c

@@ -385,6 +385,11 @@ void Gia_ManPrintChoiceStats( Gia_Man_t * p )
 void Gia_ManPrintStats( Gia_Man_t * p, Gps_Par_t * pPars )
 {
     extern float Gia_ManLevelAve( Gia_Man_t * p );
+    if ( pPars->fMiter )
+    {
+        Gia_ManPrintStatsMiter( p, 0 );
+        return;
+    }
 #ifdef WIN32
     SetConsoleTextAttribute( GetStdHandle(STD_OUTPUT_HANDLE), 15 ); // bright
     if ( p->pName )
@@ -546,6 +551,40 @@ void Gia_ManPrintMiterStatus( Gia_Man_t * p )
         Gia_ManPoNum(p), nUnsat, nSat, nUndec );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Statistics of the miter.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManPrintStatsMiter( Gia_Man_t * p, int fVerbose )
+{
+    Gia_Obj_t * pObj;
+    Vec_Flt_t * vProb;
+    int i, iObjId;
+    Gia_ManLevelNum( p );
+    Gia_ManCreateRefs( p );
+    vProb = Gia_ManPrintOutputProb( p );
+    printf( "Statistics for each outputs of the miter:\n" );
+    Gia_ManForEachPo( p, pObj, i )
+    {
+        iObjId = Gia_ObjId(p, pObj);
+        printf( "%4d : ", i );
+        printf( "Level = %5d  ",  Gia_ObjLevelId(p, iObjId) );
+        printf( "Supp = %5d  ",   Gia_ManSuppSize(p, &iObjId, 1) );
+        printf( "Cone = %5d  ",   Gia_ManConeSize(p, &iObjId, 1) );
+        printf( "Mffc = %5d  ",   Gia_NodeMffcSize(p, Gia_ObjFanin0(pObj)) );
+        printf( "Prob = %8.4f  ", Vec_FltEntry(vProb, iObjId) );
+        printf( "\n" );
+    }
+    Vec_FltFree( vProb );
+}
+
 /**Function*************************************************************
 
   Synopsis    [Prints stats for the AIG.]

src/aig/gia/giaSwitch.c

@@ -777,6 +777,27 @@ float Gia_ManComputeSwitching( Gia_Man_t * p, int nFrames, int nPref, int fProbO
     return SwitchTotal;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Determine probability of being 1 at the outputs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Flt_t * Gia_ManPrintOutputProb( Gia_Man_t * p )
+{
+    Vec_Flt_t * vSimData;
+    Gia_Man_t * pDfs = Gia_ManDup( p );
+    assert( Gia_ManObjNum(pDfs) == Gia_ManObjNum(p) );
+    vSimData = (Vec_Flt_t *)Gia_ManComputeSwitchProbs( pDfs, (Gia_ManRegNum(p) ? 16 : 1), 0, 1 );
+    Gia_ManStop( pDfs );
+    return vSimData;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/base/abci/abc.c

@@ -413,6 +413,7 @@ static int Abc_CommandAbc9Inse               ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandAbc9Maxi               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Bmci               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9PoXsim             ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Demiter            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 //static int Abc_CommandAbc9PoPart2            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 //static int Abc_CommandAbc9CexCut             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 //static int Abc_CommandAbc9CexMerge           ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -990,6 +991,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC9",         "&maxi",         Abc_CommandAbc9Maxi,         0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&bmci",         Abc_CommandAbc9Bmci,         0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&poxsim",       Abc_CommandAbc9PoXsim,       0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&demiter",      Abc_CommandAbc9Demiter,      0 );
 //    Cmd_CommandAdd( pAbc, "ABC9",         "&popart2",      Abc_CommandAbc9PoPart2,      0 );
 //    Cmd_CommandAdd( pAbc, "ABC9",         "&cexcut",       Abc_CommandAbc9CexCut,       0 );
 //    Cmd_CommandAdd( pAbc, "ABC9",         "&cexmerge",     Abc_CommandAbc9CexMerge,     0 );
@@ -25410,7 +25412,7 @@ int Abc_CommandAbc9Ps( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     memset( pPars, 0, sizeof(Gps_Par_t) );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Dtpcnlmh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Dtpcnlmah" ) ) != EOF )
     {
         switch ( c )
         {
@@ -25432,6 +25434,9 @@ int Abc_CommandAbc9Ps( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'm':
             pPars->fMuxXor ^= 1;
             break;
+        case 'a':
+            pPars->fMiter ^= 1;
+            break;
         case 'D':
             if ( globalUtilOptind >= argc )
             {
@@ -25456,7 +25461,7 @@ int Abc_CommandAbc9Ps( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &ps [-tpcnlmh] [-D file]\n" );
+    Abc_Print( -2, "usage: &ps [-tpcnlmah] [-D file]\n" );
     Abc_Print( -2, "\t          prints stats of the current AIG\n" );
     Abc_Print( -2, "\t-t      : toggle printing BMC tents [default = %s]\n",                pPars->fTents? "yes": "no" );
     Abc_Print( -2, "\t-p      : toggle printing switching activity [default = %s]\n",       pPars->fSwitch? "yes": "no" );
@@ -25464,6 +25469,7 @@ usage:
     Abc_Print( -2, "\t-n      : toggle printing NPN classes of functions [default = %s]\n", pPars->fNpn? "yes": "no" );
     Abc_Print( -2, "\t-l      : toggle printing LUT size profile [default = %s]\n",         pPars->fLutProf? "yes": "no" );
     Abc_Print( -2, "\t-m      : toggle printing MUX/XOR statistics [default = %s]\n",       pPars->fMuxXor? "yes": "no" );
+    Abc_Print( -2, "\t-a      : toggle printing miter statistics [default = %s]\n",         pPars->fMiter? "yes": "no" );
     Abc_Print( -2, "\t-D file : file name to dump statistics [default = none]\n" );
     Abc_Print( -2, "\t-h      : print the command usage\n");
     return 1;
@@ -34408,6 +34414,60 @@ usage:
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc9Demiter( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern Gia_Man_t * Gia_ManDupDemiter( Gia_Man_t * p, int fVerbose );
+    Gia_Man_t * pTemp;
+    int c, fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9Demiter(): There is no AIG.\n" );
+        return 0;
+    }
+    if ( Gia_ManPoNum(pAbc->pGia) != 1 )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9Demiter(): Miter should have one output.\n" );
+        return 0;
+    }
+    pTemp = Gia_ManDupDemiter( pAbc->pGia, fVerbose );
+    Abc_FrameUpdateGia( pAbc, pTemp );
+    if ( fVerbose )
+        Gia_ManPrintStatsMiter( pTemp, 0 );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &demiter [-vh]\n" );
+    Abc_Print( -2, "\t         decomposes a single-output miter\n" );
+    Abc_Print( -2, "\t-v     : toggles printing verbose information [default = %s]\n",  fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    return 1;
+}
+
 /**Function*************************************************************
 
   Synopsis    []