diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2009-02-15 08:01:00 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2009-02-15 08:01:00 -0800 |
commit | 0871bffae307e0553e0c5186336189e8b55cf6a6 (patch) | |
tree | 4571d1563fe33a53a57fea1c35fb668b9d33265f /src/aig/cec2/cecStatus.c | |
parent | f936cc0680c98ffe51b3a1716c996072d5dbf76c (diff) | |
download | abc-0871bffae307e0553e0c5186336189e8b55cf6a6.tar.gz abc-0871bffae307e0553e0c5186336189e8b55cf6a6.tar.bz2 abc-0871bffae307e0553e0c5186336189e8b55cf6a6.zip |
Version abc90215
Diffstat (limited to 'src/aig/cec2/cecStatus.c')
-rw-r--r-- | src/aig/cec2/cecStatus.c | 187 |
1 files changed, 187 insertions, 0 deletions
diff --git a/src/aig/cec2/cecStatus.c b/src/aig/cec2/cecStatus.c new file mode 100644 index 00000000..79d6ec66 --- /dev/null +++ b/src/aig/cec2/cecStatus.c @@ -0,0 +1,187 @@ +/**CFile**************************************************************** + + FileName [cecStatus.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Combinatinoal equivalence checking.] + + Synopsis [Miter status.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: cecStatus.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "cecInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Returns 1 if the output is known.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cec_OutputStatus( Aig_Man_t * p, Aig_Obj_t * pObj ) +{ + Aig_Obj_t * pChild; + assert( Aig_ObjIsPo(pObj) ); + pChild = Aig_ObjChild0(pObj); + // check if the output is constant 0 + if ( pChild == Aig_ManConst0(p) ) + return 1; + // check if the output is constant 1 + if ( pChild == Aig_ManConst1(p) ) + return 1; + // check if the output is a primary input + if ( Aig_ObjIsPi(Aig_Regular(pChild)) ) + return 1; + // check if the output is 1 for the 0000 pattern + if ( Aig_Regular(pChild)->fPhase != (unsigned)Aig_IsComplement(pChild) ) + return 1; + return 0; +} + +/**Function************************************************************* + + Synopsis [Returns number of used inputs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cec_CountInputs( Aig_Man_t * p ) +{ + Aig_Obj_t * pObj; + int i, Counter = 0; + Aig_ManForEachPi( p, pObj, i ) + Counter += (int)(pObj->nRefs > 0); + return Counter; +} + +/**Function************************************************************* + + Synopsis [Checks the status of the miter.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Cec_MtrStatus_t Cec_MiterStatus( Aig_Man_t * p ) +{ + Cec_MtrStatus_t Status; + Aig_Obj_t * pObj, * pChild; + int i; + assert( p->nRegs == 0 ); + memset( &Status, 0, sizeof(Cec_MtrStatus_t) ); + Status.iOut = -1; + Status.nInputs = Cec_CountInputs( p ); + Status.nNodes = Aig_ManNodeNum( p ); + Status.nOutputs = Aig_ManPoNum(p); + Aig_ManForEachPo( p, pObj, i ) + { + pChild = Aig_ObjChild0(pObj); + // check if the output is constant 0 + if ( pChild == Aig_ManConst0(p) ) + Status.nUnsat++; + // check if the output is constant 1 + else if ( pChild == Aig_ManConst1(p) ) + { + Status.nSat++; + if ( Status.iOut == -1 ) + Status.iOut = i; + } + // check if the output is a primary input + else if ( Aig_ObjIsPi(Aig_Regular(pChild)) ) + { + Status.nSat++; + if ( Status.iOut == -1 ) + Status.iOut = i; + } + // check if the output is 1 for the 0000 pattern + else if ( Aig_Regular(pChild)->fPhase != (unsigned)Aig_IsComplement(pChild) ) + { + Status.nSat++; + if ( Status.iOut == -1 ) + Status.iOut = i; + } + else + Status.nUndec++; + } + return Status; +} + +/**Function************************************************************* + + Synopsis [Checks the status of the miter.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Cec_MtrStatus_t Cec_MiterStatusTrivial( Aig_Man_t * p ) +{ + Cec_MtrStatus_t Status; + memset( &Status, 0, sizeof(Cec_MtrStatus_t) ); + Status.iOut = -1; + Status.nInputs = Aig_ManPiNum(p); + Status.nNodes = Aig_ManNodeNum( p ); + Status.nOutputs = Aig_ManPoNum(p); + Status.nUndec = Aig_ManPoNum(p); + return Status; +} + +/**Function************************************************************* + + Synopsis [Prints the status of the miter.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cec_MiterStatusPrint( Cec_MtrStatus_t S, char * pString, int Time ) +{ + printf( "%s:", pString ); + printf( " I =%6d", S.nInputs ); + printf( " N =%7d", S.nNodes ); + printf( " " ); + printf( " ? =%6d", S.nUndec ); + printf( " U =%6d", S.nUnsat ); + printf( " S =%6d", S.nSat ); + printf(" %7.2f sec\n", (float)(Time)/(float)(CLOCKS_PER_SEC)); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + |