/**CFile****************************************************************
FileName [sscClass.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [SAT sweeping under constraints.]
Synopsis [Equivalence classes.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 29, 2008.]
Revision [$Id: sscClass.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
***********************************************************************/
#include "sscInt.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Computes hash key of the simuation info.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Ssc_GiaSimHashKey( Gia_Man_t * p, int iObj, int nTableSize )
{
static int s_Primes[16] = {
1291, 1699, 1999, 2357, 2953, 3313, 3907, 4177,
4831, 5147, 5647, 6343, 6899, 7103, 7873, 8147 };
word * pSim = Gia_ObjSim( p, iObj );
unsigned uHash = 0;
int i, nWords = Gia_ObjSimWords(p);
if ( pSim[0] & 1 )
for ( i = 0; i < nWords; i++ )
uHash ^= ~pSim[i] * s_Primes[i & 0xf];
else
for ( i = 0; i < nWords; i++ )
uHash ^= pSim[i] * s_Primes[i & 0xf];
return (int)(uHash % nTableSize);
}
/**Function*************************************************************
Synopsis [Returns 1 if sim patterns are equal up to the complement.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Ssc_GiaSimIsConst0( Gia_Man_t * p, int iObj0 )
{
int w, nWords = Gia_ObjSimWords(p);
word * pSim = Gia_ObjSim( p, iObj0 );
if ( pSim[0] & 1 )
{
for ( w = 0; w < nWords; w++ )
if ( ~pSim[w] )
return 0;
}
else
{
for ( w = 0; w < nWords; w++ )
if ( pSim[w] )
return 0;
}
return 1;
}
static inline int Ssc_GiaSimAreEqual( Gia_Man_t * p, int iObj0, int iObj1 )
{
int w, nWords = Gia_ObjSimWords(p);
word * pSim0 = Gia_ObjSim( p, iObj0 );
word * pSim1 = Gia_ObjSim( p, iObj1 );
if ( (pSim0[0] & 1) != (pSim1[0] & 1) )
{
for ( w = 0; w < nWords; w++ )
if ( pSim0[w] != ~pSim1[w] )
return 0;
}
else
{
for ( w = 0; w < nWords; w++ )
if ( pSim0[w] != pSim1[w] )
return 0;
}
return 1;
}
static inline int Ssc_GiaSimAreEqualBit( Gia_Man_t * p, int iObj0, int iObj1 )
{
Gia_Obj_t * pObj0 = Gia_ManObj( p, iObj0 );
Gia_Obj_t * pObj1 = Gia_ManObj( p, iObj1 );
return (pObj0->fPhase ^ pObj0->fMark0) == (pObj1->fPhase ^ pObj1->fMark0);
}
/**Function*************************************************************
Synopsis [Refines one equivalence class.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ssc_GiaSimClassCreate( Gia_Man_t * p, Vec_Int_t * vClass )
{
int Repr = GIA_VOID, EntPrev = -1, Ent, i;
assert( Vec_IntSize(vClass) > 0 );
Vec_IntForEachEntry( vClass, Ent, i )
{
if ( i == 0 )
{
Repr = Ent;
Gia_ObjSetRepr( p, Ent, GIA_VOID );
EntPrev = Ent;
}
else
{
assert( Repr < Ent );
Gia_ObjSetRepr( p, Ent, Repr );
Gia_ObjSetNext( p, EntPrev, Ent );
EntPrev = Ent;
}
}
Gia_ObjSetNext( p, EntPrev, 0 );
}
/**Function*************************************************************
Synopsis [Refines one equivalence class using individual bit-pattern.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ssc_GiaSimClassRefineOneBit( Gia_Man_t * p, int i )
{
Gia_Obj_t * pObj;
int Ent;
assert( Gia_ObjIsHead( p, i ) );
Vec_IntClear( p->vClassOld );
Vec_IntClear( p->vClassNew );
Vec_IntPush( p->vClassOld, i );
pObj = Gia_ManObj(p, i);
Gia_ClassForEachObj1( p, i, Ent )
{
if ( Ssc_GiaSimAreEqualBit( p, i, Ent ) )
Vec_IntPush( p->vClassOld, Ent );
else
Vec_IntPush( p->vClassNew, Ent );
}
if ( Vec_IntSize( p->vClassNew ) == 0 )
return 0;
Ssc_GiaSimClassCreate( p, p->vClassOld );
Ssc_GiaSimClassCreate( p, p->vClassNew );
return 1;
}
/**Function*************************************************************
Synopsis [Refines one class using simulation patterns.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ssc_GiaSimClassRefineOne( Gia_Man_t * p, int i )
{
Gia_Obj_t * pObj;
int Ent;
assert( Gia_ObjIsHead( p, i ) );
Vec_IntClear( p->vClassOld );
Vec_IntClear( p->vClassNew );
Vec_IntPush( p->vClassOld, i );
pObj = Gia_ManObj(p, i);
Gia_ClassForEachObj1( p, i, Ent )
{
if ( Ssc_GiaSimAreEqual( p, i, Ent ) )
Vec_IntPush( p->vClassOld, Ent );
else
Vec_IntPush( p->vClassNew, Ent );
}
if ( Vec_IntSize( p->vClassNew ) == 0 )
return 0;
Ssc_GiaSimClassCreate( p, p->vClassOld );
Ssc_GiaSimClassCreate( p, p->vClassNew );
if ( Vec_IntSize(p->vClassNew) > 1 )
return 1 + Ssc_GiaSimClassRefineOne( p, Vec_IntEntry(p->vClassNew,0) );
return 1;
}
void Ssc_GiaSimProcessRefined( Gia_Man_t * p, Vec_Int_t * vRefined )
{
int * pTable, nTableSize, i, k, Key;
if ( Vec_IntSize(vRefined) == 0 )
return;
nTableSize = Abc_PrimeCudd( 100 + Vec_IntSize(vRefined) / 3 );
pTable = ABC_CALLOC( int, nTableSize );
Vec_IntForEachEntry( vRefined, i, k )
{
assert( !Ssc_GiaSimIsConst0( p, i ) );
Key = Ssc_GiaSimHashKey( p, i, nTableSize );
if ( pTable[Key] == 0 )
{
assert( Gia_ObjRepr(p, i) == 0 );
assert( Gia_ObjNext(p, i) == 0 );
Gia_ObjSetRepr( p, i, GIA_VOID );
}
else
{
Gia_ObjSetNext( p, pTable[Key], i );
Gia_ObjSetRepr( p, i, Gia_ObjRepr(p, pTable[Key]) );
if ( Gia_ObjRepr(p, i) == GIA_VOID )
Gia_ObjSetRepr( p, i, pTable[Key] );
assert( Gia_ObjRepr(p, i) > 0 );
}
pTable[Key] = i;
}
Vec_IntForEachEntry( vRefined, i, k )
if ( Gia_ObjIsHead( p, i ) )
Ssc_GiaSimClassRefineOne( p, i );
ABC_FREE( pTable );
}
/**Function*************************************************************
Synopsis [Refines equivalence classes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ssc_GiaClassesInit( Gia_Man_t * p )
{
Gia_Obj_t * pObj;
int i;
assert( p->pReprs == NULL );
p->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) );
p->pNexts = ABC_CALLOC( int, Gia_ManObjNum(p) );
Gia_ManForEachObj( p, pObj, i )
Gia_ObjSetRepr( p, i, Gia_ObjIsCand(pObj) ? 0 : GIA_VOID );
if ( p->vClassOld == NULL )
p->vClassOld = Vec_IntAlloc( 100 );
if ( p->vClassNew == NULL )
p->vClassNew = Vec_IntAlloc( 100 );
}
int Ssc_GiaClassesRefine( Gia_Man_t * p )
{
Vec_Int_t * vRefinedC;
Gia_Obj_t * pObj;
int i, Counter = 0;
assert( p->pReprs != NULL );
vRefinedC = Vec_IntAlloc( 100 );
Gia_ManForEachCand( p, pObj, i )
if ( Gia_ObjIsTail(p, i) )
Counter += Ssc_GiaSimClassRefineOne( p, Gia_ObjRepr(p, i) );
else if ( Gia_ObjIsConst(p, i) && !Ssc_GiaSimIsConst0(p, i) )
Vec_IntPush( vRefinedC, i );
Ssc_GiaSimProcessRefined( p, vRefinedC );
Counter += Vec_IntSize( vRefinedC );
Vec_IntFree( vRefinedC );
return Counter;
}
/**Function*************************************************************
Synopsis [Check if the pairs have been disproved.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ssc_GiaClassesCheckPairs( Gia_Man_t * p, Vec_Int_t * vDisPairs )
{
int i, iRepr, iObj, Result = 1;
Vec_IntForEachEntryDouble( vDisPairs, iRepr, iObj, i )
if ( iRepr == Gia_ObjRepr(p, iObj) )
printf( "Pair (%d, %d) are still equivalent.\n", iRepr, iObj ), Result = 0;
// if ( Result )
// printf( "Classes are refined correctly.\n" );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END