From 1e76ebdf3beee8bfd47d433f203c1aa7e998b179 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 20 Jun 2014 17:51:35 -0700 Subject: New tools for profiling verification miters. --- src/aig/gia/gia.h | 3 ++ src/aig/gia/giaDup.c | 90 ++++++++++++++++++++++++++++++++++++++++++++++--- src/aig/gia/giaMan.c | 39 +++++++++++++++++++++ src/aig/gia/giaSwitch.c | 21 ++++++++++++ src/base/abci/abc.c | 64 +++++++++++++++++++++++++++++++++-- 5 files changed, 210 insertions(+), 7 deletions(-) (limited to 'src') diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 8872ef83..f7e27a08 100644 --- a/src/aig/gia/gia.h +++ b/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 ); diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index 747e68b1..86d8039f 100644 --- a/src/aig/gia/giaDup.c +++ b/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_ObjChild1(pObj), vSuper ); + Gia_ManDupWithConstrCollectAnd_rec( p, Gia_ObjChild0(pObj), vSuper, 0 ); + 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 /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c index f1470287..a0880837 100644 --- a/src/aig/gia/giaMan.c +++ b/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.] diff --git a/src/aig/gia/giaSwitch.c b/src/aig/gia/giaSwitch.c index a7b63864..e5b1eb22 100644 --- a/src/aig/gia/giaSwitch.c +++ b/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 /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 118136bd..3c2d0c4f 100644 --- a/src/base/abci/abc.c +++ b/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 [] -- cgit v1.2.3