ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
simSymStr.c
Go to the documentation of this file.
1
20
21#include "base/abc/abc.h"
22#include "sim.h"
23
25
26
30
31#define SIM_READ_SYMMS(pNode) ((Vec_Int_t *)pNode->pCopy)
32#define SIM_SET_SYMMS(pNode,vVect) (pNode->pCopy = (Abc_Obj_t *)(vVect))
33
34static void Sim_SymmsStructComputeOne( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, int * pMap );
35static void Sim_SymmsBalanceCollect_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes );
36static void Sim_SymmsPartitionNodes( Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesPis0, Vec_Ptr_t * vNodesPis1, Vec_Ptr_t * vNodesOther );
37static void Sim_SymmsAppendFromGroup( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodesPi, Vec_Ptr_t * vNodesOther, Vec_Int_t * vSymms, int * pMap );
38static void Sim_SymmsAppendFromNode( Abc_Ntk_t * pNtk, Vec_Int_t * vSymms0, Vec_Ptr_t * vNodesOther, Vec_Ptr_t * vNodesPi0, Vec_Ptr_t * vNodesPi1, Vec_Int_t * vSymms, int * pMap );
39static int Sim_SymmsIsCompatibleWithNodes( Abc_Ntk_t * pNtk, unsigned uSymm, Vec_Ptr_t * vNodesOther, int * pMap );
40static int Sim_SymmsIsCompatibleWithGroup( unsigned uSymm, Vec_Ptr_t * vNodesPi, int * pMap );
41static void Sim_SymmsPrint( Vec_Int_t * vSymms );
42static void Sim_SymmsTrans( Vec_Int_t * vSymms );
43static void Sim_SymmsTransferToMatrix( Extra_BitMat_t * pMatSymm, Vec_Int_t * vSymms, unsigned * pSupport );
44static int * Sim_SymmsCreateMap( Abc_Ntk_t * pNtk );
45
49
61void Sim_SymmsStructCompute( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMatrs, Vec_Ptr_t * vSuppFun )
62{
63 Vec_Ptr_t * vNodes;
64 Abc_Obj_t * pTemp;
65 int * pMap, i;
66
67 assert( Abc_NtkCiNum(pNtk) + 10 < (1<<16) );
68
69 // get the structural support
70 pNtk->vSupps = Sim_ComputeStrSupp( pNtk );
71 // set elementary info for the CIs
72 Abc_NtkForEachCi( pNtk, pTemp, i )
73 SIM_SET_SYMMS( pTemp, Vec_IntAlloc(0) );
74 // create the map of CI ids into their numbers
75 pMap = Sim_SymmsCreateMap( pNtk );
76 // collect the nodes in the TFI cone of this output
77 vNodes = Abc_NtkDfs( pNtk, 0 );
78 Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pTemp, i )
79 {
80// if ( Abc_NodeIsConst(pTemp) )
81// continue;
82 Sim_SymmsStructComputeOne( pNtk, pTemp, pMap );
83 }
84 // collect the results for the COs;
85 Abc_NtkForEachCo( pNtk, pTemp, i )
86 {
87//printf( "Output %d:\n", i );
88 pTemp = Abc_ObjFanin0(pTemp);
89 if ( Abc_ObjIsCi(pTemp) || Abc_AigNodeIsConst(pTemp) )
90 continue;
91 Sim_SymmsTransferToMatrix( (Extra_BitMat_t *)Vec_PtrEntry(vMatrs, i), SIM_READ_SYMMS(pTemp), (unsigned *)Vec_PtrEntry(vSuppFun, i) );
92 }
93 // clean the intermediate results
94 Sim_UtilInfoFree( pNtk->vSupps );
95 pNtk->vSupps = NULL;
96 Abc_NtkForEachCi( pNtk, pTemp, i )
97 Vec_IntFree( SIM_READ_SYMMS(pTemp) );
98 Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pTemp, i )
99// if ( !Abc_NodeIsConst(pTemp) )
100 Vec_IntFree( SIM_READ_SYMMS(pTemp) );
101 Vec_PtrFree( vNodes );
102 ABC_FREE( pMap );
103}
104
116void Sim_SymmsStructComputeOne( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, int * pMap )
117{
118 Vec_Ptr_t * vNodes, * vNodesPi0, * vNodesPi1, * vNodesOther;
119 Vec_Int_t * vSymms;
120 Abc_Obj_t * pTemp;
121 int i;
122
123 // allocate the temporary arrays
124 vNodes = Vec_PtrAlloc( 10 );
125 vNodesPi0 = Vec_PtrAlloc( 10 );
126 vNodesPi1 = Vec_PtrAlloc( 10 );
127 vNodesOther = Vec_PtrAlloc( 10 );
128
129 // collect the fanins of the implication supergate
130 Sim_SymmsBalanceCollect_rec( pNode, vNodes );
131
132 // sort the nodes in the implication supergate
133 Sim_SymmsPartitionNodes( vNodes, vNodesPi0, vNodesPi1, vNodesOther );
134
135 // start the resulting set
136 vSymms = Vec_IntAlloc( 10 );
137 // generate symmetries from the groups
138 Sim_SymmsAppendFromGroup( pNtk, vNodesPi0, vNodesOther, vSymms, pMap );
139 Sim_SymmsAppendFromGroup( pNtk, vNodesPi1, vNodesOther, vSymms, pMap );
140 // add symmetries from other inputs
141 for ( i = 0; i < vNodesOther->nSize; i++ )
142 {
143 pTemp = Abc_ObjRegular((Abc_Obj_t *)vNodesOther->pArray[i]);
144 Sim_SymmsAppendFromNode( pNtk, SIM_READ_SYMMS(pTemp), vNodesOther, vNodesPi0, vNodesPi1, vSymms, pMap );
145 }
146 Vec_PtrFree( vNodes );
147 Vec_PtrFree( vNodesPi0 );
148 Vec_PtrFree( vNodesPi1 );
149 Vec_PtrFree( vNodesOther );
150
151 // set the symmetry at the node
152 SIM_SET_SYMMS( pNode, vSymms );
153}
154
155
167void Sim_SymmsBalanceCollect_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
168{
169 // if the new node is complemented, another gate begins
170 if ( Abc_ObjIsComplement(pNode) )
171 {
172 Vec_PtrPushUnique( vNodes, pNode );
173 return;
174 }
175 // if pNew is the PI node, return
176 if ( Abc_ObjIsCi(pNode) )
177 {
178 Vec_PtrPushUnique( vNodes, pNode );
179 return;
180 }
181 // go through the branches
182 Sim_SymmsBalanceCollect_rec( Abc_ObjChild0(pNode), vNodes );
183 Sim_SymmsBalanceCollect_rec( Abc_ObjChild1(pNode), vNodes );
184}
185
197void Sim_SymmsPartitionNodes( Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesPis0,
198 Vec_Ptr_t * vNodesPis1, Vec_Ptr_t * vNodesOther )
199{
200 Abc_Obj_t * pNode;
201 int i;
202 Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
203 {
204 if ( !Abc_ObjIsCi(Abc_ObjRegular(pNode)) )
205 Vec_PtrPush( vNodesOther, pNode );
206 else if ( Abc_ObjIsComplement(pNode) )
207 Vec_PtrPush( vNodesPis0, pNode );
208 else
209 Vec_PtrPush( vNodesPis1, pNode );
210 }
211}
212
224void Sim_SymmsAppendFromGroup( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodesPi, Vec_Ptr_t * vNodesOther, Vec_Int_t * vSymms, int * pMap )
225{
226 Abc_Obj_t * pNode1, * pNode2;
227 unsigned uSymm;
228 int i, k;
229
230 if ( vNodesPi->nSize == 0 )
231 return;
232
233 // go through the pairs
234 for ( i = 0; i < vNodesPi->nSize; i++ )
235 for ( k = i+1; k < vNodesPi->nSize; k++ )
236 {
237 // get the two PI nodes
238 pNode1 = Abc_ObjRegular((Abc_Obj_t *)vNodesPi->pArray[i]);
239 pNode2 = Abc_ObjRegular((Abc_Obj_t *)vNodesPi->pArray[k]);
240 assert( pMap[pNode1->Id] != pMap[pNode2->Id] );
241 assert( pMap[pNode1->Id] >= 0 );
242 assert( pMap[pNode2->Id] >= 0 );
243 // generate symmetry
244 if ( pMap[pNode1->Id] < pMap[pNode2->Id] )
245 uSymm = ((pMap[pNode1->Id] << 16) | pMap[pNode2->Id]);
246 else
247 uSymm = ((pMap[pNode2->Id] << 16) | pMap[pNode1->Id]);
248 // check if symmetry belongs
249 if ( Sim_SymmsIsCompatibleWithNodes( pNtk, uSymm, vNodesOther, pMap ) )
250 Vec_IntPushUnique( vSymms, (int)uSymm );
251 }
252}
253
265void Sim_SymmsAppendFromNode( Abc_Ntk_t * pNtk, Vec_Int_t * vSymms0, Vec_Ptr_t * vNodesOther,
266 Vec_Ptr_t * vNodesPi0, Vec_Ptr_t * vNodesPi1, Vec_Int_t * vSymms, int * pMap )
267{
268 unsigned uSymm;
269 int i;
270
271 if ( vSymms0->nSize == 0 )
272 return;
273
274 // go through the pairs
275 for ( i = 0; i < vSymms0->nSize; i++ )
276 {
277 uSymm = (unsigned)vSymms0->pArray[i];
278 // check if symmetry belongs
279 if ( Sim_SymmsIsCompatibleWithNodes( pNtk, uSymm, vNodesOther, pMap ) &&
280 Sim_SymmsIsCompatibleWithGroup( uSymm, vNodesPi0, pMap ) &&
281 Sim_SymmsIsCompatibleWithGroup( uSymm, vNodesPi1, pMap ) )
282 Vec_IntPushUnique( vSymms, (int)uSymm );
283 }
284}
285
297int Sim_SymmsIsCompatibleWithNodes( Abc_Ntk_t * pNtk, unsigned uSymm, Vec_Ptr_t * vNodesOther, int * pMap )
298{
299 Vec_Int_t * vSymmsNode;
300 Abc_Obj_t * pNode;
301 int i, s, Ind1, Ind2, fIsVar1, fIsVar2;
302
303 if ( vNodesOther->nSize == 0 )
304 return 1;
305
306 // get the indices of the PI variables
307 Ind1 = (uSymm & 0xffff);
308 Ind2 = (uSymm >> 16);
309
310 // go through the nodes
311 // if they do not belong to a support, it is okay
312 // if one belongs, the other does not belong, quit
313 // if they belong, but are not part of symmetry, quit
314 for ( i = 0; i < vNodesOther->nSize; i++ )
315 {
316 pNode = Abc_ObjRegular((Abc_Obj_t *)vNodesOther->pArray[i]);
317 fIsVar1 = Sim_SuppStrHasVar( pNtk->vSupps, pNode, Ind1 );
318 fIsVar2 = Sim_SuppStrHasVar( pNtk->vSupps, pNode, Ind2 );
319
320 if ( !fIsVar1 && !fIsVar2 )
321 continue;
322 if ( fIsVar1 ^ fIsVar2 )
323 return 0;
324 // both belong
325 // check if there is a symmetry
326 vSymmsNode = SIM_READ_SYMMS( pNode );
327 for ( s = 0; s < vSymmsNode->nSize; s++ )
328 if ( uSymm == (unsigned)vSymmsNode->pArray[s] )
329 break;
330 if ( s == vSymmsNode->nSize )
331 return 0;
332 }
333 return 1;
334}
335
347int Sim_SymmsIsCompatibleWithGroup( unsigned uSymm, Vec_Ptr_t * vNodesPi, int * pMap )
348{
349 Abc_Obj_t * pNode;
350 int i, Ind1, Ind2, fHasVar1, fHasVar2;
351
352 if ( vNodesPi->nSize == 0 )
353 return 1;
354
355 // get the indices of the PI variables
356 Ind1 = (uSymm & 0xffff);
357 Ind2 = (uSymm >> 16);
358
359 // go through the PI nodes
360 fHasVar1 = fHasVar2 = 0;
361 for ( i = 0; i < vNodesPi->nSize; i++ )
362 {
363 pNode = Abc_ObjRegular((Abc_Obj_t *)vNodesPi->pArray[i]);
364 if ( pMap[pNode->Id] == Ind1 )
365 fHasVar1 = 1;
366 else if ( pMap[pNode->Id] == Ind2 )
367 fHasVar2 = 1;
368 }
369 return fHasVar1 == fHasVar2;
370}
371
372
373
385void Sim_SymmsTrans( Vec_Int_t * vSymms )
386{
387 unsigned uSymm, uSymma, uSymmr;
388 int i, Ind1, Ind2;
389 int k, Ind1a, Ind2a;
390 int j;
391 int nTrans = 0;
392
393 for ( i = 0; i < vSymms->nSize; i++ )
394 {
395 uSymm = (unsigned)vSymms->pArray[i];
396 Ind1 = (uSymm & 0xffff);
397 Ind2 = (uSymm >> 16);
398 // find other symmetries that have Ind1
399 for ( k = i+1; k < vSymms->nSize; k++ )
400 {
401 uSymma = (unsigned)vSymms->pArray[k];
402 if ( uSymma == uSymm )
403 continue;
404 Ind1a = (uSymma & 0xffff);
405 Ind2a = (uSymma >> 16);
406 if ( Ind1a == Ind1 )
407 {
408 // find the symmetry (Ind2,Ind2a)
409 if ( Ind2 < Ind2a )
410 uSymmr = ((Ind2 << 16) | Ind2a);
411 else
412 uSymmr = ((Ind2a << 16) | Ind2);
413 for ( j = 0; j < vSymms->nSize; j++ )
414 if ( uSymmr == (unsigned)vSymms->pArray[j] )
415 break;
416 if ( j == vSymms->nSize )
417 nTrans++;
418 }
419 }
420
421 }
422 printf( "Trans = %d.\n", nTrans );
423}
424
425
437void Sim_SymmsTransferToMatrix( Extra_BitMat_t * pMatSymm, Vec_Int_t * vSymms, unsigned * pSupport )
438{
439 int i, Ind1, Ind2, nInputs;
440 unsigned uSymm;
441 // add diagonal elements
442 nInputs = Extra_BitMatrixReadSize( pMatSymm );
443 for ( i = 0; i < nInputs; i++ )
444 Extra_BitMatrixInsert1( pMatSymm, i, i );
445 // add non-diagonal elements
446 for ( i = 0; i < vSymms->nSize; i++ )
447 {
448 uSymm = (unsigned)vSymms->pArray[i];
449 Ind1 = (uSymm & 0xffff);
450 Ind2 = (uSymm >> 16);
451//printf( "%d,%d ", Ind1, Ind2 );
452 // skip variables that are not in the true support
453 assert( Sim_HasBit(pSupport, Ind1) == Sim_HasBit(pSupport, Ind2) );
454 if ( !Sim_HasBit(pSupport, Ind1) || !Sim_HasBit(pSupport, Ind2) )
455 continue;
456 Extra_BitMatrixInsert1( pMatSymm, Ind1, Ind2 );
457 Extra_BitMatrixInsert2( pMatSymm, Ind1, Ind2 );
458 }
459}
460
472int * Sim_SymmsCreateMap( Abc_Ntk_t * pNtk )
473{
474 int * pMap;
475 Abc_Obj_t * pNode;
476 int i;
477 pMap = ABC_ALLOC( int, Abc_NtkObjNumMax(pNtk) );
478 for ( i = 0; i < Abc_NtkObjNumMax(pNtk); i++ )
479 pMap[i] = -1;
480 Abc_NtkForEachCi( pNtk, pNode, i )
481 pMap[pNode->Id] = i;
482 return pMap;
483}
484
485
486
490
491
493
struct Abc_Obj_t_ Abc_Obj_t
Definition abc.h:116
#define Abc_NtkForEachCo(pNtk, pCo, i)
Definition abc.h:522
ABC_DLL Vec_Ptr_t * Abc_NtkDfs(Abc_Ntk_t *pNtk, int fCollectAll)
Definition abcDfs.c:82
struct Abc_Ntk_t_ Abc_Ntk_t
Definition abc.h:115
#define Abc_NtkForEachCi(pNtk, pCi, i)
Definition abc.h:518
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
#define ABC_FREE(obj)
Definition abc_global.h:267
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
struct Extra_BitMat_t_ Extra_BitMat_t
Definition extra.h:81
int Extra_BitMatrixReadSize(Extra_BitMat_t *p)
void Extra_BitMatrixInsert1(Extra_BitMat_t *p, int i, int k)
void Extra_BitMatrixInsert2(Extra_BitMat_t *p, int i, int k)
void Sim_SymmsStructCompute(Abc_Ntk_t *pNtk, Vec_Ptr_t *vMatrs, Vec_Ptr_t *vSuppFun)
FUNCTION DEFINITIONS ///.
Definition simSymStr.c:61
#define SIM_SET_SYMMS(pNode, vVect)
Definition simSymStr.c:32
#define SIM_READ_SYMMS(pNode)
DECLARATIONS ///.
Definition simSymStr.c:31
void Sim_UtilInfoFree(Vec_Ptr_t *p)
Definition simUtils.c:84
#define Sim_HasBit(p, i)
Definition sim.h:163
Vec_Ptr_t * Sim_ComputeStrSupp(Abc_Ntk_t *pNtk)
FUNCTION DEFINITIONS ///.
Definition simSupp.c:57
#define Sim_SuppStrHasVar(vSupps, pNode, v)
Definition sim.h:167
Vec_Ptr_t * vSupps
Definition abc.h:197
int Id
Definition abc.h:132
#define assert(ex)
Definition util_old.h:213
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition vecPtr.h:55