ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
ivyRwrAlg.c
Go to the documentation of this file.
1
20
21#include "ivy.h"
22
24
25
29
30static int Ivy_ManFindAlgCut( Ivy_Obj_t * pRoot, Vec_Ptr_t * vFront, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone );
31static Ivy_Obj_t * Ivy_NodeRewriteAlg( Ivy_Obj_t * pObj, Vec_Ptr_t * vFront, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone, Vec_Ptr_t * vSols, int LevelR, int fUseZeroCost );
32static int Ivy_NodeCountMffc( Ivy_Obj_t * pNode );
33
37
49int Ivy_ManRewriteAlg( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost )
50{
51 Vec_Int_t * vRequired;
52 Vec_Ptr_t * vFront, * vLeaves, * vCone, * vSol;
53 Ivy_Obj_t * pObj, * pResult;
54 int i, RetValue, LevelR, nNodesOld;
55 int CountUsed, CountUndo;
56 vRequired = fUpdateLevel? Ivy_ManRequiredLevels( p ) : NULL;
57 vFront = Vec_PtrAlloc( 100 );
58 vLeaves = Vec_PtrAlloc( 100 );
59 vCone = Vec_PtrAlloc( 100 );
60 vSol = Vec_PtrAlloc( 100 );
61 // go through the nodes in the topological order
62 CountUsed = CountUndo = 0;
63 nNodesOld = Ivy_ManObjIdNext(p);
64 Ivy_ManForEachObj( p, pObj, i )
65 {
66 assert( !Ivy_ObjIsBuf(pObj) );
67 if ( i >= nNodesOld )
68 break;
69 // skip no-nodes and MUX roots
70 if ( !Ivy_ObjIsNode(pObj) || Ivy_ObjIsExor(pObj) || Ivy_ObjIsMuxType(pObj) )
71 continue;
72// if ( pObj->Id > 297 ) // 296 --- 297
73// break;
74 if ( pObj->Id == 297 )
75 {
76 int x = 0;
77 }
78 // get the largest algebraic cut
79 RetValue = Ivy_ManFindAlgCut( pObj, vFront, vLeaves, vCone );
80 // the case of a trivial tree cut
81 if ( RetValue == 1 )
82 continue;
83 // the case of constant 0 cone
84 if ( RetValue == -1 )
85 {
86 Ivy_ObjReplace( pObj, Ivy_ManConst0(p), 1, 0, 1 );
87 continue;
88 }
89 assert( Vec_PtrSize(vLeaves) > 2 );
90 // get the required level for this node
91 LevelR = vRequired? Vec_IntEntry(vRequired, pObj->Id) : 1000000;
92 // create a new cone
93 pResult = Ivy_NodeRewriteAlg( pObj, vFront, vLeaves, vCone, vSol, LevelR, fUseZeroCost );
94 if ( pResult == NULL || pResult == pObj )
95 continue;
96 assert( Vec_PtrSize(vSol) == 1 || !Ivy_IsComplement(pResult) );
97 if ( Ivy_ObjLevel(Ivy_Regular(pResult)) > LevelR && Ivy_ObjRefs(Ivy_Regular(pResult)) == 0 )
98 Ivy_ObjDelete_rec(Ivy_Regular(pResult), 1), CountUndo++;
99 else
100 Ivy_ObjReplace( pObj, pResult, 1, 0, 1 ), CountUsed++;
101 }
102 printf( "Used = %d. Undo = %d.\n", CountUsed, CountUndo );
103 Vec_PtrFree( vFront );
104 Vec_PtrFree( vCone );
105 Vec_PtrFree( vSol );
106 if ( vRequired ) Vec_IntFree( vRequired );
107 if ( i = Ivy_ManCleanup(p) )
108 printf( "Cleanup after rewriting removed %d dangling nodes.\n", i );
109 if ( !Ivy_ManCheck(p) )
110 printf( "Ivy_ManRewriteAlg(): The check has failed.\n" );
111 return 1;
112}
113
125Ivy_Obj_t * Ivy_NodeRewriteAlg( Ivy_Obj_t * pObj, Vec_Ptr_t * vFront, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone, Vec_Ptr_t * vSols, int LevelR, int fUseZeroCost )
126{
127 int fVerbose = 0;
128 Ivy_Obj_t * pTemp;
129 int k, Counter, nMffc, RetValue;
130
131 if ( fVerbose )
132 {
133 if ( Ivy_ObjIsExor(pObj) )
134 printf( "x " );
135 else
136 printf( " " );
137 }
138
139/*
140 printf( "%d ", Vec_PtrSize(vFront) );
141 printf( "( " );
142 Vec_PtrForEachEntry( Ivy_Obj_t *, vFront, pTemp, k )
143 printf( "%d ", Ivy_ObjRefs(Ivy_Regular(pTemp)) );
144 printf( ")\n" );
145*/
146 // collect nodes in the cone
147 if ( Ivy_ObjIsExor(pObj) )
148 Ivy_ManCollectCone( pObj, vFront, vCone );
149 else
150 Ivy_ManCollectCone( pObj, vLeaves, vCone );
151
152 // deref nodes in the cone
153 Vec_PtrForEachEntry( Ivy_Obj_t *, vCone, pTemp, k )
154 {
155 Ivy_ObjRefsDec( Ivy_ObjFanin0(pTemp) );
156 Ivy_ObjRefsDec( Ivy_ObjFanin1(pTemp) );
157 pTemp->fMarkB = 1;
158 }
159
160 // count the MFFC size
161 Vec_PtrForEachEntry( Ivy_Obj_t *, vFront, pTemp, k )
162 Ivy_Regular(pTemp)->fMarkA = 1;
163 nMffc = Ivy_NodeCountMffc( pObj );
164 Vec_PtrForEachEntry( Ivy_Obj_t *, vFront, pTemp, k )
165 Ivy_Regular(pTemp)->fMarkA = 0;
166
167 if ( fVerbose )
168 {
169 Counter = 0;
170 Vec_PtrForEachEntry( Ivy_Obj_t *, vCone, pTemp, k )
171 Counter += (Ivy_ObjRefs(pTemp) > 0);
172 printf( "%5d : Leaves = %2d. Cone = %2d. ConeRef = %2d. Mffc = %d. Lev = %d. LevR = %d.\n",
173 pObj->Id, Vec_PtrSize(vFront), Vec_PtrSize(vCone), Counter-1, nMffc, Ivy_ObjLevel(pObj), LevelR );
174 }
175/*
176 printf( "Leaves:" );
177 Vec_PtrForEachEntry( Ivy_Obj_t *, vLeaves, pTemp, k )
178 printf( " %d%s", Ivy_Regular(pTemp)->Id, Ivy_IsComplement(pTemp)? "\'" : "" );
179 printf( "\n" );
180 printf( "Cone:\n" );
181 Vec_PtrForEachEntry( Ivy_Obj_t *, vCone, pTemp, k )
182 printf( " %5d = %d%s %d%s\n", pTemp->Id,
183 Ivy_ObjFaninId0(pTemp), Ivy_ObjFaninC0(pTemp)? "\'" : "",
184 Ivy_ObjFaninId1(pTemp), Ivy_ObjFaninC1(pTemp)? "\'" : "" );
185*/
186
187 RetValue = Ivy_MultiPlus( vLeaves, vCone, Ivy_ObjType(pObj), nMffc + fUseZeroCost, vSols );
188
189 // ref nodes in the cone
190 Vec_PtrForEachEntry( Ivy_Obj_t *, vCone, pTemp, k )
191 {
192 Ivy_ObjRefsInc( Ivy_ObjFanin0(pTemp) );
193 Ivy_ObjRefsInc( Ivy_ObjFanin1(pTemp) );
194 pTemp->fMarkA = 0;
195 pTemp->fMarkB = 0;
196 }
197
198 if ( !RetValue )
199 return NULL;
200
201 if ( Vec_PtrSize( vSols ) == 1 )
202 return Vec_PtrEntry( vSols, 0 );
203 return Ivy_NodeBalanceBuildSuper( vSols, Ivy_ObjType(pObj), 1 );
204}
205
218{
219 if ( Ivy_ObjRefs(pNode) > 0 || Ivy_ObjIsCi(pNode) || pNode->fMarkA )
220 return 0;
221 assert( pNode->fMarkB );
222 pNode->fMarkA = 1;
223// printf( "%d ", pNode->Id );
224 if ( Ivy_ObjIsBuf(pNode) )
225 return Ivy_NodeCountMffc_rec( Ivy_ObjFanin0(pNode) );
226 return 1 + Ivy_NodeCountMffc_rec( Ivy_ObjFanin0(pNode) ) + Ivy_NodeCountMffc_rec( Ivy_ObjFanin1(pNode) );
227}
228
240int Ivy_NodeCountMffc( Ivy_Obj_t * pNode )
241{
242 assert( pNode->fMarkB );
243 return 1 + Ivy_NodeCountMffc_rec( Ivy_ObjFanin0(pNode) ) + Ivy_NodeCountMffc_rec( Ivy_ObjFanin1(pNode) );
244}
245
258{
259 if ( *pp1 < *pp2 )
260 return -1;
261 if ( *pp1 > *pp2 )
262 return 1;
263 return 0;
264}
265
279int Ivy_ManFindAlgCut_rec( Ivy_Obj_t * pObj, Ivy_Type_t Type, Vec_Ptr_t * vFront, Vec_Ptr_t * vCone )
280{
281 int RetValue0, RetValue1;
282 Ivy_Obj_t * pObjR = Ivy_Regular(pObj);
283 assert( !Ivy_ObjIsBuf(pObjR) );
284 assert( Type != IVY_EXOR || !Ivy_IsComplement(pObj) );
285
286 // make sure the node is not visited twice in different polarities
287 if ( Ivy_IsComplement(pObj) )
288 { // if complemented, mark B
289 if ( pObjR->fMarkA )
290 return -1;
291 pObjR->fMarkB = 1;
292 }
293 else
294 { // if non-complicated, mark A
295 if ( pObjR->fMarkB )
296 return -1;
297 pObjR->fMarkA = 1;
298 }
299 Vec_PtrPush( vCone, pObjR );
300
301 // if the node is the end of the tree, return
302 if ( Ivy_IsComplement(pObj) || Ivy_ObjType(pObj) != Type )
303 {
304 if ( Ivy_ObjRefs(pObjR) == 1 )
305 return 1;
306 assert( Ivy_ObjRefs(pObjR) > 1 );
307 Vec_PtrPush( vFront, pObj );
308 return 0;
309 }
310
311 // branch on the node
312 assert( !Ivy_IsComplement(pObj) );
313 assert( Ivy_ObjIsNode(pObj) );
314 // what if buffer has more than one fanout???
315 RetValue0 = Ivy_ManFindAlgCut_rec( Ivy_ObjReal( Ivy_ObjChild0(pObj) ), Type, vFront, vCone );
316 RetValue1 = Ivy_ManFindAlgCut_rec( Ivy_ObjReal( Ivy_ObjChild1(pObj) ), Type, vFront, vCone );
317 if ( RetValue0 == -1 || RetValue1 == -1 )
318 return -1;
319
320 // the case when both have no external references
321 if ( RetValue0 && RetValue1 )
322 {
323 if ( Ivy_ObjRefs(pObj) == 1 )
324 return 1;
325 assert( Ivy_ObjRefs(pObj) > 1 );
326 Vec_PtrPush( vFront, pObj );
327 return 0;
328 }
329 // the case when one of them has external references
330 if ( RetValue0 )
331 Vec_PtrPush( vFront, Ivy_ObjReal( Ivy_ObjChild0(pObj) ) );
332 if ( RetValue1 )
333 Vec_PtrPush( vFront, Ivy_ObjReal( Ivy_ObjChild1(pObj) ) );
334 return 0;
335}
336
350int Ivy_ManFindAlgCut( Ivy_Obj_t * pRoot, Vec_Ptr_t * vFront, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone )
351{
352 Ivy_Obj_t * pObj, * pPrev;
353 int RetValue, i;
354 assert( !Ivy_IsComplement(pRoot) );
355 assert( Ivy_ObjIsNode(pRoot) );
356 // clear the frontier and collect the nodes
357 Vec_PtrClear( vCone );
358 Vec_PtrClear( vFront );
359 Vec_PtrClear( vLeaves );
360 RetValue = Ivy_ManFindAlgCut_rec( pRoot, Ivy_ObjType(pRoot), vFront, vCone );
361 // clean the marks
362 Vec_PtrForEachEntry( Ivy_Obj_t *, vCone, pObj, i )
363 pObj->fMarkA = pObj->fMarkB = 0;
364 // quit if the same node is found in both polarities
365 if ( RetValue == -1 )
366 return -1;
367 // return if the node is the root of a tree
368 if ( RetValue == 1 )
369 return 1;
370 // return if the cut is composed of two nodes
371 if ( Vec_PtrSize(vFront) <= 2 )
372 return 1;
373 // sort the entries in increasing order
374 Vec_PtrSort( vFront, (int (*)(const void *, const void *))Ivy_ManFindAlgCutCompare );
375 // remove duplicates from vFront and save the nodes in vLeaves
376 pPrev = Vec_PtrEntry(vFront, 0);
377 Vec_PtrPush( vLeaves, pPrev );
378 Vec_PtrForEachEntryStart( Ivy_Obj_t *, vFront, pObj, i, 1 )
379 {
380 // compare current entry and the previous entry
381 if ( pObj == pPrev )
382 {
383 if ( Ivy_ObjIsExor(pRoot) ) // A <+> A = 0
384 {
385 // vLeaves are no longer structural support of pRoot!!!
386 Vec_PtrPop(vLeaves);
387 pPrev = Vec_PtrSize(vLeaves) == 0 ? NULL : Vec_PtrEntryLast(vLeaves);
388 }
389 continue;
390 }
391 if ( pObj == Ivy_Not(pPrev) )
392 {
393 assert( Ivy_ObjIsAnd(pRoot) );
394 return -1;
395 }
396 pPrev = pObj;
397 Vec_PtrPush( vLeaves, pObj );
398 }
399 if ( Vec_PtrSize(vLeaves) == 0 )
400 return -1;
401 if ( Vec_PtrSize(vLeaves) <= 2 )
402 return 1;
403 return 0;
404}
405
406
410
411
413
#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
Cube * p
Definition exorList.c:222
int Ivy_NodeCountMffc_rec(Ivy_Obj_t *pNode)
Definition ivyRwrAlg.c:217
int Ivy_ManFindAlgCutCompare(Ivy_Obj_t **pp1, Ivy_Obj_t **pp2)
Definition ivyRwrAlg.c:257
int Ivy_ManFindAlgCut_rec(Ivy_Obj_t *pObj, Ivy_Type_t Type, Vec_Ptr_t *vFront, Vec_Ptr_t *vCone)
Definition ivyRwrAlg.c:279
int Ivy_ManRewriteAlg(Ivy_Man_t *p, int fUpdateLevel, int fUseZeroCost)
FUNCTION DEFINITIONS ///.
Definition ivyRwrAlg.c:49
int Ivy_MultiPlus(Ivy_Man_t *p, Vec_Ptr_t *vLeaves, Vec_Ptr_t *vCone, Ivy_Type_t Type, int nLimit, Vec_Ptr_t *vSol)
FUNCTION DEFINITIONS ///.
Definition ivyMulti.c:58
int Ivy_ManCheck(Ivy_Man_t *p)
DECLARATIONS ///.
Definition ivyCheck.c:45
typedefABC_NAMESPACE_HEADER_START struct Ivy_Man_t_ Ivy_Man_t
INCLUDES ///.
Definition ivy.h:46
Ivy_Obj_t * Ivy_NodeBalanceBuildSuper(Ivy_Man_t *p, Vec_Ptr_t *vSuper, Ivy_Type_t Type, int fUpdateLevel)
Definition ivyBalance.c:175
Vec_Int_t * Ivy_ManRequiredLevels(Ivy_Man_t *p)
Definition ivyDfs.c:250
int Ivy_ManCleanup(Ivy_Man_t *p)
Definition ivyMan.c:265
#define Ivy_ManForEachObj(p, pObj, i)
Definition ivy.h:393
Ivy_Obj_t * Ivy_ObjReal(Ivy_Obj_t *pObj)
Definition ivyUtil.c:609
struct Ivy_Obj_t_ Ivy_Obj_t
Definition ivy.h:47
void Ivy_ObjReplace(Ivy_Man_t *p, Ivy_Obj_t *pObjOld, Ivy_Obj_t *pObjNew, int fDeleteOld, int fFreeTop, int fUpdateLevel)
Definition ivyObj.c:328
int Ivy_ObjIsMuxType(Ivy_Obj_t *pObj)
Definition ivyUtil.c:479
Ivy_Type_t
Definition ivy.h:52
@ IVY_EXOR
Definition ivy.h:59
void Ivy_ObjDelete_rec(Ivy_Man_t *p, Ivy_Obj_t *pObj, int fFreeTop)
Definition ivyObj.c:299
void Ivy_ManCollectCone(Ivy_Obj_t *pObj, Vec_Ptr_t *vFront, Vec_Ptr_t *vCone)
Definition ivyDfs.c:195
unsigned fMarkB
Definition ivy.h:79
int Id
Definition ivy.h:75
unsigned fMarkA
Definition ivy.h:78
#define assert(ex)
Definition util_old.h:213
#define Vec_PtrForEachEntryStart(Type, vVec, pEntry, i, Start)
Definition vecPtr.h:57
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