Code for structural unateness checking.

1 files changed, 255 insertions, 0 deletions

diff --git a/src/aig/gia/giaUnate.c b/src/aig/gia/giaUnate.c
new file mode 100644
index 00000000..b627641e
--- /dev/null
+++ b/src/aig/gia/giaUnate.c
@@ -0,0 +1,255 @@
+/**CFile****************************************************************
+
+  FileName    [giaUnate.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Scalable AIG package.]
+
+  Synopsis    [Computation of structural unateness.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: giaUnate.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "gia.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Flips the first bit in all entries of the vector.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Vec_Int_t * Vec_IntFlopBit( Vec_Int_t * p )
+{
+    int i;
+    for ( i = 0; i < p->nSize; i++ )
+    {
+        if ( i+1 < p->nSize && Abc_Lit2Var(p->pArray[i]) == Abc_Lit2Var(p->pArray[i+1]) ) 
+            i++; // skip variable appearing as both pos and neg literal
+        else
+            p->pArray[i] ^= 1;
+    }
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Compute unateness for all outputs in terms of inputs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Wec_t * Gia_ManCheckUnateVec( Gia_Man_t * p, Vec_Int_t * vCiIds, Vec_Int_t * vCoIds )
+{
+    Vec_Int_t * vCiVec = vCiIds ? Vec_IntDup(vCiIds) : Vec_IntStartNatural(Gia_ManCiNum(p));
+    Vec_Int_t * vCoVec = vCoIds ? Vec_IntDup(vCoIds) : Vec_IntStartNatural(Gia_ManCoNum(p));
+    Vec_Wec_t * vUnatesCo = Vec_WecStart( Vec_IntSize(vCoVec) );
+    Vec_Wec_t * vUnates   = Vec_WecStart( Gia_ManObjNum(p) );
+    Vec_Int_t * vUnate0, * vUnate1;
+    Gia_Obj_t * pObj; int i, CioId;
+    Vec_IntForEachEntry( vCiVec, CioId, i )
+    {
+        pObj = Gia_ManCi( p, CioId );
+        Vec_IntPush( Vec_WecEntry(vUnates, Gia_ObjId(p, pObj)), Abc_Var2Lit(CioId, 0) );
+    }
+    Gia_ManForEachAnd( p, pObj, i )
+    {
+        vUnate0 = Vec_WecEntry(vUnates, Gia_ObjFaninId0(pObj, i));
+        vUnate1 = Vec_WecEntry(vUnates, Gia_ObjFaninId1(pObj, i));
+        vUnate0 = Gia_ObjFaninC0(pObj) ? Vec_IntFlopBit(vUnate0) : vUnate0;
+        vUnate1 = Gia_ObjFaninC1(pObj) ? Vec_IntFlopBit(vUnate1) : vUnate1;
+        Vec_IntTwoMerge2( vUnate0, vUnate1, Vec_WecEntry(vUnates, i) ); 
+        vUnate0 = Gia_ObjFaninC0(pObj) ? Vec_IntFlopBit(vUnate0) : vUnate0;
+        vUnate1 = Gia_ObjFaninC1(pObj) ? Vec_IntFlopBit(vUnate1) : vUnate1;
+    }
+    Vec_IntForEachEntry( vCoVec, CioId, i )
+    {
+        pObj    = Gia_ManCo( p, CioId );
+        vUnate0 = Vec_WecEntry(vUnates, Gia_ObjFaninId0p(p, pObj));
+        vUnate0 = Gia_ObjFaninC0(pObj) ? Vec_IntFlopBit(vUnate0) : vUnate0;
+        Vec_IntAppend( Vec_WecEntry(vUnatesCo, i), vUnate0 );
+        vUnate0 = Gia_ObjFaninC0(pObj) ? Vec_IntFlopBit(vUnate0) : vUnate0;
+    }
+    Vec_WecFree( vUnates );
+    Vec_IntFree( vCiVec );
+    Vec_IntFree( vCoVec );
+    return vUnatesCo;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks unateness one function in one variable.]
+
+  Description [Returns 0 if Co is not unate in Ci.
+               Returns 1 if Co is neg-unate in Ci.
+               Returns 2 if Co is pos-unate in Ci.
+               Returns 3 if Co does not depend on Ci.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManCheckUnate_rec( Gia_Man_t * p, int iObj )
+{
+    Gia_Obj_t * pObj;
+    int Res0, Res1;
+    if ( p->nTravIds - p->pTravIds[iObj] <= 3 )
+        return p->nTravIds - p->pTravIds[iObj];
+    pObj = Gia_ManObj( p, iObj );
+    p->pTravIds[iObj] = p->nTravIds - 3;
+    if ( Gia_ObjIsCi(pObj) )
+        return 3;
+    Res0 = Gia_ManCheckUnate_rec( p, Gia_ObjFaninId0(pObj, iObj) );
+    Res1 = Gia_ManCheckUnate_rec( p, Gia_ObjFaninId1(pObj, iObj) );
+    Res0 = ((Res0 == 1 || Res0 == 2) && Gia_ObjFaninC0(pObj)) ? Res0 ^ 3 : Res0;
+    Res1 = ((Res1 == 1 || Res1 == 2) && Gia_ObjFaninC1(pObj)) ? Res1 ^ 3 : Res1;
+    p->pTravIds[iObj] = p->nTravIds - (Res0 & Res1);
+    assert( (Res0 & Res1) <= 3 );
+    return p->nTravIds - p->pTravIds[iObj];
+}
+int Gia_ManCheckUnate( Gia_Man_t * p, int iCiId, int iCoId )
+{
+    int Res;
+    int CiObjId = Gia_ObjId(p, Gia_ManCi(p, iCiId));
+    int CoObjId = Gia_ObjId(p, Gia_ManCo(p, iCoId));
+    Gia_Obj_t * pCoObj = Gia_ManCo(p, iCoId);
+    Gia_ManIncrementTravId( p ); // Co does not depend on Ci.
+    Gia_ManIncrementTravId( p ); // Co is pos-unate in Ci
+    Gia_ObjSetTravIdCurrentId( p, CiObjId );
+    Gia_ManIncrementTravId( p ); // Co is neg-unate in Ci
+    Gia_ManIncrementTravId( p ); // Co is not unate in Ci
+    Res = Gia_ManCheckUnate_rec( p, Gia_ObjFaninId0(pCoObj, CoObjId) );
+    return ((Res == 1 || Res == 2) && Gia_ObjFaninC0(pCoObj)) ? Res ^ 3 : Res;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Testing procedure for all pairs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManCheckUnateVecTest( Gia_Man_t * p, int fVerbose )
+{
+    abctime clk = Abc_Clock();
+    Vec_Wec_t * vUnates = Gia_ManCheckUnateVec( p, NULL, NULL );
+    int i, o, Var, nVars = Gia_ManCiNum(p);
+    int nUnate = 0, nNonUnate = 0;
+    char * pBuffer = ABC_CALLOC( char, nVars+1 );
+    if ( fVerbose )
+    {
+        printf( "Inputs  : " );
+        for ( i = 0; i < nVars; i++ )
+            printf( "%d", i % 10 );
+        printf( "\n" );
+    }
+    for ( o = 0; o < Gia_ManCoNum(p); o++ )
+    {
+        Vec_Int_t * vUnate = Vec_WecEntry( vUnates, o );
+        memset( pBuffer, ' ', nVars );
+        Vec_IntForEachEntry( vUnate, Var, i )
+            if ( i+1 < Vec_IntSize(vUnate) && Abc_Lit2Var(Var) == Abc_Lit2Var(Vec_IntEntry(vUnate, i+1)) ) // both lits are present
+                pBuffer[Abc_Lit2Var(Var)] = '.', i++, nNonUnate++; // does not depend on this var
+            else
+                pBuffer[Abc_Lit2Var(Var)] = Abc_LitIsCompl(Var) ? 'n' : 'p', nUnate++;
+        if ( fVerbose )
+            printf( "Out%4d : %s\n", o, pBuffer );
+    }
+    ABC_FREE( pBuffer );
+    // print stats
+    printf( "Ins/Outs = %4d/%4d.  Total supp = %5d.  Total unate = %5d.\n",
+        Gia_ManCiNum(p), Gia_ManCoNum(p), nUnate+nNonUnate, nUnate );
+    ABC_PRT( "Total time", Abc_Clock() - clk );
+    //Vec_WecPrint( vUnates, 0 );
+    Vec_WecFree( vUnates );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Testing procedure for one pair.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManCheckUnateTest( Gia_Man_t * p, int fComputeAll, int fVerbose )
+{
+    if ( fComputeAll )
+        Gia_ManCheckUnateVecTest( p, fVerbose );
+    else
+    {
+        abctime clk = Abc_Clock();
+        int i, o, nVars = Gia_ManCiNum(p);
+        int nUnate = 0, nNonUnate = 0;
+        char * pBuffer = ABC_CALLOC( char, nVars+1 );
+        if ( fVerbose )
+        {
+            printf( "Inputs  : " );
+            for ( i = 0; i < nVars; i++ )
+                printf( "%d", i % 10 );
+            printf( "\n" );
+        }
+        for ( o = 0; o < Gia_ManCoNum(p); o++ )
+        {
+            for ( i = 0; i < nVars; i++ )
+            {
+                int Res = Gia_ManCheckUnate( p, i, o );
+                if ( Res == 3 )       pBuffer[i] = ' ';
+                else if ( Res == 2 )  pBuffer[i] = 'p', nUnate++;
+                else if ( Res == 1 )  pBuffer[i] = 'n', nUnate++;
+                else if ( Res == 0 )  pBuffer[i] = '.', nNonUnate++;
+                else assert( 0 );
+            }
+            if ( fVerbose )
+                printf( "Out%4d : %s\n", o, pBuffer );
+        }
+        ABC_FREE( pBuffer );
+        // print stats
+        printf( "Ins/Outs = %4d/%4d.  Total supp = %5d.  Total unate = %5d.\n",
+            Gia_ManCiNum(p), Gia_ManCoNum(p), nUnate+nNonUnate, nUnate );
+        ABC_PRT( "Total time", Abc_Clock() - clk );
+    }
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+