abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
Functions
cecIso.c File Reference
#include "cecInt.h"

Go to the source code of this file.

Functions

static
ABC_NAMESPACE_IMPL_START
unsigned * 		Cec_ManIsoInfo (unsigned *pStore, int nWords, int Id)
 DECLARATIONS ///. More...
 
static void Gia_ManIsoSimulate (Gia_Obj_t *pObj, int Id, unsigned *pStore, int nWords)
 FUNCTION DEFINITIONS ///. More...
 
static void Gia_ManIsoCopy (int IdDest, int IdSour, unsigned *pStore, int nWords)
 
static int Gia_ManIsoEqual (int Id0, int Id1, unsigned *pStore, int nWords)
 
static void Gia_ManIsoRandom (int Id, unsigned *pStore, int nWords)
 
static int Gia_ManIsoHashKey (int Id, unsigned *pStore, int nWords, int nTableSize)
 
static void Gia_ManIsoTableAdd (Gia_Man_t *p, int Id, unsigned *pStore, int nWords, int *pTable, int nTableSize)
 
static int Gia_ManIsoExtractClasses (Gia_Man_t *p, int Bin, unsigned *pStore, int nWords, Vec_Int_t *vNodesA, Vec_Int_t *vNodesB)
 
static void Gia_ManIsoMatchNodes (int *pIso, unsigned *pStore, int nWords, Vec_Int_t *vNodesA, Vec_Int_t *vNodesB)
 
void Cec_ManTransformClasses (Gia_Man_t *p)
 
int * Cec_ManDetectIsomorphism (Gia_Man_t *p)
 

Function Documentation

int* Cec_ManDetectIsomorphism ( Gia_Man_t *  p)

Function*************************************************************

Synopsis [Finds node correspondences in the miter.]

Description [Assumes that the colors are assigned.]

SideEffects []

SeeAlso []

Definition at line 297 of file cecIso.c.

298 {
299  int nWords = 2;
300  Gia_Obj_t * pObj;
301  Vec_Int_t * vNodesA, * vNodesB;
302  unsigned * pStore, Counter;
303  int i, * pIso, * pTable, nTableSize;
304  // start equivalence classes
305  pIso = ABC_CALLOC( int, Gia_ManObjNum(p) );
306  Gia_ManForEachObj( p, pObj, i )
307  {
308  if ( Gia_ObjIsCo(pObj) )
309  {
310  assert( Gia_ObjColors(p, i) == 0 );
311  continue;
312  }
313  assert( Gia_ObjColors(p, i) );
314  if ( Gia_ObjColors(p, i) == 3 )
315  pIso[i] = i;
316  }
317  // start simulation info
318  pStore = ABC_ALLOC( unsigned, Gia_ManObjNum(p) * nWords );
319  // simulate and create table
320  nTableSize = Abc_PrimeCudd( 100 + Gia_ManObjNum(p)/2 );
321  pTable = ABC_CALLOC( int, nTableSize );
322  Gia_ManCleanValue( p );
323  Gia_ManForEachObj1( p, pObj, i )
324  {
325  if ( Gia_ObjIsCo(pObj) )
326  continue;
327  if ( pIso[i] == 0 ) // simulate
328  Gia_ManIsoSimulate( pObj, i, pStore, nWords );
329  else if ( pIso[i] < i ) // copy
330  Gia_ManIsoCopy( i, pIso[i], pStore, nWords );
331  else // generate
332  Gia_ManIsoRandom( i, pStore, nWords );
333  if ( pIso[i] == 0 )
334  Gia_ManIsoTableAdd( p, i, pStore, nWords, pTable, nTableSize );
335  }
336  // create equivalence classes
337  vNodesA = Vec_IntAlloc( 100 );
338  vNodesB = Vec_IntAlloc( 100 );
339  for ( i = 0; i < nTableSize; i++ )
340  if ( Gia_ManIsoExtractClasses( p, pTable[i], pStore, nWords, vNodesA, vNodesB ) )
341  Gia_ManIsoMatchNodes( pIso, pStore, nWords, vNodesA, vNodesB );
342  Vec_IntFree( vNodesA );
343  Vec_IntFree( vNodesB );
344  // collect info
345  Counter = 0;
346  Gia_ManForEachObj1( p, pObj, i )
347  {
348  Counter += (pIso[i] && pIso[i] < i);
349 /*
350  if ( pIso[i] && pIso[i] < i )
351  {
352  if ( (Gia_ObjIsHead(p,pIso[i]) && Gia_ObjRepr(p,i)==pIso[i]) ||
353  (Gia_ObjIsClass(p,pIso[i]) && Gia_ObjRepr(p,i)==Gia_ObjRepr(p,pIso[i])) )
354  Abc_Print( 1, "1" );
355  else
356  Abc_Print( 1, "0" );
357  }
358 */
359  }
360  Abc_Print( 1, "Computed %d pairs of structurally equivalent nodes.\n", Counter );
361 // p->pIso = pIso;
362 // Cec_ManTransformClasses( p );
363 
364  ABC_FREE( pTable );
365  ABC_FREE( pStore );
366  return pIso;
367 }
Abc_PrimeCudd
static int Abc_PrimeCudd(unsigned int p)
Definition: abc_global.h:383
Gia_ManIsoMatchNodes
static void Gia_ManIsoMatchNodes(int *pIso, unsigned *pStore, int nWords, Vec_Int_t *vNodesA, Vec_Int_t *vNodesB)
Definition: cecIso.c:239
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Gia_ManCleanValue
void Gia_ManCleanValue(Gia_Man_t *p)
Definition: giaUtil.c:310
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
nWords
int nWords
Definition: abcNpn.c:127
Gia_Obj_t_
Definition: gia.h:75
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Gia_ManIsoCopy
static void Gia_ManIsoCopy(int IdDest, int IdSour, unsigned *pStore, int nWords)
Definition: cecIso.c:84
Gia_ManIsoSimulate
static void Gia_ManIsoSimulate(Gia_Obj_t *pObj, int Id, unsigned *pStore, int nWords)
FUNCTION DEFINITIONS ///.
Definition: cecIso.c:47
Counter
static int Counter
Definition: extraBddMisc.c:1877
Abc_Print
static void Abc_Print(int level, const char *format,...)
Definition: abc_global.h:313
Gia_ObjColors
static int Gia_ObjColors(Gia_Man_t *p, int Id)
Definition: gia.h:904
Gia_ObjIsCo
static int Gia_ObjIsCo(Gia_Obj_t *pObj)
Definition: gia.h:421
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Gia_ManForEachObj
#define Gia_ManForEachObj(p, pObj, i)
MACRO DEFINITIONS ///.
Definition: gia.h:984
Gia_ManIsoExtractClasses
static int Gia_ManIsoExtractClasses(Gia_Man_t *p, int Bin, unsigned *pStore, int nWords, Vec_Int_t *vNodesA, Vec_Int_t *vNodesB)
Definition: cecIso.c:206
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
assert
#define assert(ex)
Definition: util_old.h:213
Gia_ManForEachObj1
#define Gia_ManForEachObj1(p, pObj, i)
Definition: gia.h:986
Gia_ManIsoRandom
static void Gia_ManIsoRandom(int Id, unsigned *pStore, int nWords)
Definition: cecIso.c:126
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
Gia_ManObjNum
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
Gia_ManIsoTableAdd
static void Gia_ManIsoTableAdd(Gia_Man_t *p, int Id, unsigned *pStore, int nWords, int *pTable, int nTableSize)
Definition: cecIso.c:170
static ABC_NAMESPACE_IMPL_START unsigned* Cec_ManIsoInfo ( unsigned *  pStore,
int  nWords,
int  Id 
)
inlinestatic

DECLARATIONS ///.

CFile****************************************************************

FileName [cecIso.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Combinational equivalence checking.]

Synopsis [Detection of structural isomorphism.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id:
cecIso.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

]

Definition at line 30 of file cecIso.c.

30 { return pStore + nWords * Id; }
nWords
int nWords
Definition: abcNpn.c:127
void Cec_ManTransformClasses ( Gia_Man_t *  p)

Function*************************************************************

Synopsis [Transforms iso into equivalence classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 268 of file cecIso.c.

269 {
270  Gia_Obj_t * pObj;
271  int i;
272  assert( p->pReprs && p->pNexts && p->pIso );
273  memset( p->pReprs, 0, sizeof(int) * Gia_ManObjNum(p) );
274  memset( p->pNexts, 0, sizeof(int) * Gia_ManObjNum(p) );
275  Gia_ManForEachObj( p, pObj, i )
276  {
277  p->pReprs[i].iRepr = GIA_VOID;
278  if ( p->pIso[i] && p->pIso[i] < i )
279  {
280  p->pReprs[i].iRepr = p->pIso[i];
281  p->pNexts[p->pIso[i]] = i;
282  }
283  }
284 }
memset
char * memset()
Gia_Man_t_::pNexts
int * pNexts
Definition: gia.h:122
Gia_Man_t_::pIso
int * pIso
Definition: gia.h:124
Gia_Rpr_t_::iRepr
unsigned iRepr
Definition: gia.h:58
Gia_Obj_t_
Definition: gia.h:75
GIA_VOID
#define GIA_VOID
Definition: gia.h:45
Gia_ManForEachObj
#define Gia_ManForEachObj(p, pObj, i)
MACRO DEFINITIONS ///.
Definition: gia.h:984
Gia_Man_t_::pReprs
Gia_Rpr_t * pReprs
Definition: gia.h:121
assert
#define assert(ex)
Definition: util_old.h:213
Gia_ManObjNum
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
static void Gia_ManIsoCopy ( int  IdDest,
int  IdSour,
unsigned *  pStore,
int  nWords 
)
inlinestatic

Function*************************************************************

Synopsis [Copies simulation info.]

Description []

SideEffects []

SeeAlso []

Definition at line 84 of file cecIso.c.

85 {
86  unsigned * pInfo0 = Cec_ManIsoInfo( pStore, nWords, IdDest );
87  unsigned * pInfo1 = Cec_ManIsoInfo( pStore, nWords, IdSour );
88  int w;
89  for ( w = 0; w < nWords; w++ )
90  pInfo0[w] = pInfo1[w];
91 }
Cec_ManIsoInfo
static ABC_NAMESPACE_IMPL_START unsigned * Cec_ManIsoInfo(unsigned *pStore, int nWords, int Id)
DECLARATIONS ///.
Definition: cecIso.c:30
nWords
int nWords
Definition: abcNpn.c:127
static int Gia_ManIsoEqual ( int  Id0,
int  Id1,
unsigned *  pStore,
int  nWords 
)
inlinestatic

Function*************************************************************

Synopsis [Compares simulation info of two nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 104 of file cecIso.c.

105 {
106  unsigned * pInfo0 = Cec_ManIsoInfo( pStore, nWords, Id0 );
107  unsigned * pInfo1 = Cec_ManIsoInfo( pStore, nWords, Id1 );
108  int w;
109  for ( w = 0; w < nWords; w++ )
110  if ( pInfo0[w] != pInfo1[w] )
111  return 0;
112  return 1;
113 }
Cec_ManIsoInfo
static ABC_NAMESPACE_IMPL_START unsigned * Cec_ManIsoInfo(unsigned *pStore, int nWords, int Id)
DECLARATIONS ///.
Definition: cecIso.c:30
nWords
int nWords
Definition: abcNpn.c:127
static int Gia_ManIsoExtractClasses ( Gia_Man_t *  p,
int  Bin,
unsigned *  pStore,
int  nWords,
Vec_Int_t *  vNodesA,
Vec_Int_t *  vNodesB 
)
inlinestatic

Function*************************************************************

Synopsis [Extracts equivalence class candidates from one bin.]

Description []

SideEffects []

SeeAlso []

Definition at line 206 of file cecIso.c.

207 {
208  Gia_Obj_t * pTemp;
209  int Ent;
210  Vec_IntClear( vNodesA );
211  Vec_IntClear( vNodesB );
212  for ( Ent = Bin, pTemp = (Ent ? Gia_ManObj(p, Ent) : NULL); pTemp;
213  Ent = pTemp->Value, pTemp = (Ent ? Gia_ManObj(p, Ent) : NULL) )
214  {
215  if ( pTemp->fMark0 )
216  {
217  pTemp->fMark0 = 0;
218  continue;
219  }
220  if ( Gia_ObjColors( p, Ent ) == 1 )
221  Vec_IntPush( vNodesA, Ent );
222  else
223  Vec_IntPush( vNodesB, Ent );
224  }
225  return Vec_IntSize(vNodesA) > 0 && Vec_IntSize(vNodesB) > 0;
226 }
Gia_ManObj
static Gia_Obj_t * Gia_ManObj(Gia_Man_t *p, int v)
Definition: gia.h:402
Gia_Obj_t_
Definition: gia.h:75
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Gia_ObjColors
static int Gia_ObjColors(Gia_Man_t *p, int Id)
Definition: gia.h:904
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Gia_Obj_t_::fMark0
unsigned fMark0
Definition: gia.h:79
Gia_Obj_t_::Value
unsigned Value
Definition: gia.h:87
Vec_IntClear
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
static int Gia_ManIsoHashKey ( int  Id,
unsigned *  pStore,
int  nWords,
int  nTableSize 
)
inlinestatic

Function*************************************************************

Synopsis [Computes hash key of the simuation info.]

Description []

SideEffects []

SeeAlso []

Definition at line 145 of file cecIso.c.

146 {
147  static int s_Primes[16] = {
148  1291, 1699, 1999, 2357, 2953, 3313, 3907, 4177,
149  4831, 5147, 5647, 6343, 6899, 7103, 7873, 8147 };
150  unsigned * pInfo0 = Cec_ManIsoInfo( pStore, nWords, Id );
151  unsigned uHash = 0;
152  int i;
153  for ( i = 0; i < nWords; i++ )
154  uHash ^= pInfo0[i] * s_Primes[i & 0xf];
155  return (int)(uHash % nTableSize);
156 
157 }
Cec_ManIsoInfo
static ABC_NAMESPACE_IMPL_START unsigned * Cec_ManIsoInfo(unsigned *pStore, int nWords, int Id)
DECLARATIONS ///.
Definition: cecIso.c:30
nWords
int nWords
Definition: abcNpn.c:127
s_Primes
static int s_Primes[MAX_PRIMES]
Definition: fxuPair.c:30
static void Gia_ManIsoMatchNodes ( int *  pIso,
unsigned *  pStore,
int  nWords,
Vec_Int_t *  vNodesA,
Vec_Int_t *  vNodesB 
)
inlinestatic

Function*************************************************************

Synopsis [Matches nodes in the extacted classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 239 of file cecIso.c.

240 {
241  int k0, k1, IdA, IdB;
242  Vec_IntForEachEntry( vNodesA, IdA, k0 )
243  Vec_IntForEachEntry( vNodesB, IdB, k1 )
244  {
245  if ( Gia_ManIsoEqual( IdA, IdB, pStore, nWords ) )
246  {
247  assert( pIso[IdA] == 0 );
248  assert( pIso[IdB] == 0 );
249  assert( IdA != IdB );
250  pIso[IdA] = IdB;
251  pIso[IdB] = IdA;
252  continue;
253  }
254  }
255 }
nWords
int nWords
Definition: abcNpn.c:127
Gia_ManIsoEqual
static int Gia_ManIsoEqual(int Id0, int Id1, unsigned *pStore, int nWords)
Definition: cecIso.c:104
assert
#define assert(ex)
Definition: util_old.h:213
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
static void Gia_ManIsoRandom ( int  Id,
unsigned *  pStore,
int  nWords 
)
inlinestatic

Function*************************************************************

Synopsis [Generates random simulation info.]

Description []

SideEffects []

SeeAlso []

Definition at line 126 of file cecIso.c.

127 {
128  unsigned * pInfo0 = Cec_ManIsoInfo( pStore, nWords, Id );
129  int w;
130  for ( w = 0; w < nWords; w++ )
131  pInfo0[w] = Gia_ManRandom( 0 );
132 }
Cec_ManIsoInfo
static ABC_NAMESPACE_IMPL_START unsigned * Cec_ManIsoInfo(unsigned *pStore, int nWords, int Id)
DECLARATIONS ///.
Definition: cecIso.c:30
nWords
int nWords
Definition: abcNpn.c:127
Gia_ManRandom
unsigned Gia_ManRandom(int fReset)
FUNCTION DEFINITIONS ///.
Definition: giaUtil.c:49
static void Gia_ManIsoSimulate ( Gia_Obj_t *  pObj,
int  Id,
unsigned *  pStore,
int  nWords 
)
inlinestatic

FUNCTION DEFINITIONS ///.

Function*************************************************************

Synopsis [Computes simulation info for one node.]

Description []

SideEffects []

SeeAlso []

Definition at line 47 of file cecIso.c.

48 {
49  unsigned * pInfo = Cec_ManIsoInfo( pStore, nWords, Id );
50  unsigned * pInfo0 = Cec_ManIsoInfo( pStore, nWords, Gia_ObjFaninId0(pObj, Id) );
51  unsigned * pInfo1 = Cec_ManIsoInfo( pStore, nWords, Gia_ObjFaninId1(pObj, Id) );
52  int w;
53  if ( Gia_ObjFaninC0(pObj) )
54  {
55  if ( Gia_ObjFaninC1(pObj) )
56  for ( w = 0; w < nWords; w++ )
57  pInfo[w] = ~(pInfo0[w] | pInfo1[w]);
58  else
59  for ( w = 0; w < nWords; w++ )
60  pInfo[w] = ~pInfo0[w] & pInfo1[w];
61  }
62  else
63  {
64  if ( Gia_ObjFaninC1(pObj) )
65  for ( w = 0; w < nWords; w++ )
66  pInfo[w] = pInfo0[w] & ~pInfo1[w];
67  else
68  for ( w = 0; w < nWords; w++ )
69  pInfo[w] = pInfo0[w] & pInfo1[w];
70  }
71 }
Gia_ObjFaninC1
static int Gia_ObjFaninC1(Gia_Obj_t *pObj)
Definition: gia.h:452
Cec_ManIsoInfo
static ABC_NAMESPACE_IMPL_START unsigned * Cec_ManIsoInfo(unsigned *pStore, int nWords, int Id)
DECLARATIONS ///.
Definition: cecIso.c:30
nWords
int nWords
Definition: abcNpn.c:127
Gia_ObjFaninC0
static int Gia_ObjFaninC0(Gia_Obj_t *pObj)
Definition: gia.h:451
Gia_ObjFaninId1
static int Gia_ObjFaninId1(Gia_Obj_t *pObj, int ObjId)
Definition: gia.h:461
Gia_ObjFaninId0
static int Gia_ObjFaninId0(Gia_Obj_t *pObj, int ObjId)
Definition: gia.h:460
static void Gia_ManIsoTableAdd ( Gia_Man_t *  p,
int  Id,
unsigned *  pStore,
int  nWords,
int *  pTable,
int  nTableSize 
)
inlinestatic

Function*************************************************************

Synopsis [Adds node to the hash table.]

Description []

SideEffects []

SeeAlso []

Definition at line 170 of file cecIso.c.

171 {
172  Gia_Obj_t * pTemp;
173  int Key, Ent, Color = Gia_ObjColors( p, Id );
174  assert( Color == 1 || Color == 2 );
175  Key = Gia_ManIsoHashKey( Id, pStore, nWords, nTableSize );
176  for ( Ent = pTable[Key], pTemp = (Ent ? Gia_ManObj(p, Ent) : NULL); pTemp;
177  Ent = pTemp->Value, pTemp = (Ent ? Gia_ManObj(p, Ent) : NULL) )
178  {
179  if ( Gia_ObjColors( p, Ent ) != Color )
180  continue;
181  if ( !Gia_ManIsoEqual( Id, Ent, pStore, nWords ) )
182  continue;
183  // found node with the same color and signature - mark it and do not add new node
184  pTemp->fMark0 = 1;
185  return;
186  }
187  // did not find the node with the same color and signature - add new node
188  pTemp = Gia_ManObj( p, Id );
189  assert( pTemp->Value == 0 );
190  assert( pTemp->fMark0 == 0 );
191  pTemp->Value = pTable[Key];
192  pTable[Key] = Id;
193 }
Gia_ManIsoHashKey
static int Gia_ManIsoHashKey(int Id, unsigned *pStore, int nWords, int nTableSize)
Definition: cecIso.c:145
nWords
int nWords
Definition: abcNpn.c:127
Gia_ManObj
static Gia_Obj_t * Gia_ManObj(Gia_Man_t *p, int v)
Definition: gia.h:402
Gia_Obj_t_
Definition: gia.h:75
Gia_ObjColors
static int Gia_ObjColors(Gia_Man_t *p, int Id)
Definition: gia.h:904
Gia_Obj_t_::fMark0
unsigned fMark0
Definition: gia.h:79
Gia_ManIsoEqual
static int Gia_ManIsoEqual(int Id0, int Id1, unsigned *pStore, int nWords)
Definition: cecIso.c:104
assert
#define assert(ex)
Definition: util_old.h:213
Gia_Obj_t_::Value
unsigned Value
Definition: gia.h:87