diff options
Diffstat (limited to 'src/aig')
| -rw-r--r-- | src/aig/cec/cec.h | 1 | ||||
| -rw-r--r-- | src/aig/cec/cecCorr.c | 41 | ||||
| -rw-r--r-- | src/aig/gia/gia.h | 2 | ||||
| -rw-r--r-- | src/aig/gia/giaMan.c | 2 |
4 files changed, 46 insertions, 0 deletions
diff --git a/src/aig/cec/cec.h b/src/aig/cec/cec.h index 7f445970..199d6939 100644 --- a/src/aig/cec/cec.h +++ b/src/aig/cec/cec.h @@ -135,6 +135,7 @@ struct Cec_ParCor_t_ int fUseCSat; // use circuit-based solver // int fFirstStop; // stop on the first sat output int fUseSmartCnf; // use smart CNF computation + int fVerboseFlops; // verbose stats int fVeryVerbose; // verbose stats int fVerbose; // verbose stats }; diff --git a/src/aig/cec/cecCorr.c b/src/aig/cec/cecCorr.c index 96c45907..27a7dd36 100644 --- a/src/aig/cec/cecCorr.c +++ b/src/aig/cec/cecCorr.c @@ -990,6 +990,39 @@ unsigned * Cec_ManComputeInitState( Gia_Man_t * pAig, int nFrames ) /**Function************************************************************* + Synopsis [Prints flop equivalences.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cec_ManPrintFlopEquivs( Gia_Man_t * p ) +{ + Gia_Obj_t * pObj, * pRepr; + int i; + assert( p->vNamesIn != NULL ); + Gia_ManForEachRo( p, pObj, i ) + { + if ( Gia_ObjIsConst(p, Gia_ObjId(p, pObj)) ) + printf( "Flop \"%s\" is equivalent to constant 0.\n", Vec_PtrEntry(p->vNamesIn, Gia_ObjCioId(pObj)) ); + else if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) ) + { + if ( Gia_ObjIsCi(pRepr) ) + printf( "Flop \"%s\" is equivalent to flop \"%s\".\n", + Vec_PtrEntry( p->vNamesIn, Gia_ObjCioId(pObj) ), + Vec_PtrEntry( p->vNamesIn, Gia_ObjCioId(pRepr) ) ); + else + printf( "Flop \"%s\" is equivalent to internal node %d.\n", + Vec_PtrEntry( p->vNamesIn, Gia_ObjCioId(pObj) ), Gia_ObjId(p, pRepr) ); + } + } +} + +/**Function************************************************************* + Synopsis [Top-level procedure for register correspondence.] Description [] @@ -1060,6 +1093,14 @@ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) } if ( pPars->nPrefix && (Gia_ManAndNum(pNew) < Gia_ManAndNum(pAig) || Gia_ManRegNum(pNew) < Gia_ManRegNum(pAig)) ) printf( "The reduced AIG was produced using %d-th invariants and will not verify.\n", pPars->nPrefix ); + // print verbose info about equivalences + if ( pPars->fVerboseFlops ) + { + if ( pAig->vNamesIn == NULL ) + printf( "Flop output names are not available. Use command \"&get -n\".\n" ); + else + Cec_ManPrintFlopEquivs( pAig ); + } return pNew; } diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 9dad2742..f8c1fe91 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -136,6 +136,8 @@ struct Gia_Man_t_ unsigned char* pSwitching; // switching activity for each object Gia_Plc_t * pPlacement; // placement of the objects int * pTravIds; // separate traversal ID representation + Vec_Ptr_t * vNamesIn; // the input names + Vec_Ptr_t * vNamesOut; // the output names }; diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c index 37afde13..4547e61c 100644 --- a/src/aig/gia/giaMan.c +++ b/src/aig/gia/giaMan.c @@ -66,6 +66,8 @@ Gia_Man_t * Gia_ManStart( int nObjsMax ) ***********************************************************************/ void Gia_ManStop( Gia_Man_t * p ) { + Vec_PtrFreeFree( p->vNamesIn ); + Vec_PtrFreeFree( p->vNamesOut ); if ( p->vFlopClasses ) Vec_IntFree( p->vFlopClasses ); Vec_IntFree( p->vCis ); |