From eff11d95d20a3fcce5469ae104a0f5a424d2c1d6 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 18 Mar 2017 13:38:54 -0700 Subject: Code for structural unateness checking. --- src/aig/gia/giaUnate.c | 255 +++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 255 insertions(+) create mode 100644 src/aig/gia/giaUnate.c (limited to 'src/aig/gia') 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 + -- cgit v1.2.3