diff options
Diffstat (limited to 'src/aig/cec/cecStatus.c')
| -rw-r--r-- | src/aig/cec/cecStatus.c | 187 |
1 files changed, 0 insertions, 187 deletions
diff --git a/src/aig/cec/cecStatus.c b/src/aig/cec/cecStatus.c deleted file mode 100644 index 79d6ec66..00000000 --- a/src/aig/cec/cecStatus.c +++ /dev/null @@ -1,187 +0,0 @@ -/**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 /// -//////////////////////////////////////////////////////////////////////// - - |