mirror of https://github.com/YosysHQ/abc.git
Code for structural unateness checking.
This commit is contained in:
Alan Mishchenko
parent
1e5d826c4c
commit
eff11d95d2
|
|
@ -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
|
||||
|
||||
Loading…
Reference in New Issue