Version abc90118

1 files changed, 187 insertions, 0 deletions

diff --git a/src/aig/cec/cecStatus.c b/src/aig/cec/cecStatus.c
new file mode 100644
index 00000000..79d6ec66
--- /dev/null
+++ b/src/aig/cec/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                                ///
+////////////////////////////////////////////////////////////////////////
+
+