ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
nwkFlow_depth.c
Go to the documentation of this file.
1
20
21#include "nwk.h"
22
24
25
26/*
27 This code is based on the papers:
28 A. Hurst, A. Mishchenko, and R. Brayton, "Fast minimum-register retiming
29 via binary maximum-flow", Proc. FMCAD '07, pp. 181-187.
30 A. Hurst, A. Mishchenko, and R. Brayton, "Scalable min-area retiming
31 under simultaneous delay and initial state constraints". Proc. DAC'08.
32*/
33
35
39
40// predecessors
41static inline Nwk_Obj_t * Nwk_ObjPred( Nwk_Obj_t * pObj ) { return pObj->pCopy; }
42static inline int Nwk_ObjSetPred( Nwk_Obj_t * pObj, Nwk_Obj_t * p ) { pObj->pCopy = p; return 1; }
43// sink
44static inline int Nwk_ObjIsSink( Nwk_Obj_t * pObj ) { return pObj->MarkA; }
45static inline void Nwk_ObjSetSink( Nwk_Obj_t * pObj ) { pObj->MarkA = 1; }
46// flow
47static inline int Nwk_ObjHasFlow( Nwk_Obj_t * pObj ) { return pObj->MarkB; }
48static inline void Nwk_ObjSetFlow( Nwk_Obj_t * pObj ) { pObj->MarkB = 1; }
49static inline void Nwk_ObjClearFlow( Nwk_Obj_t * pObj ) { pObj->MarkB = 0; }
50
51// representation of visited nodes
52// pObj->TravId < pNtk->nTravIds-2 --- not visited
53// pObj->TravId == pNtk->nTravIds-2 --- visited bot only
54// pObj->TravId == pNtk->nTravIds-1 --- visited top only
55// pObj->TravId == pNtk->nTravIds --- visited bot and top
56static inline int Nwk_ObjVisitedBotOnly( Nwk_Obj_t * pObj )
57{
58 return pObj->TravId == pObj->pMan->nTravIds - 2;
59}
60static inline int Nwk_ObjVisitedBot( Nwk_Obj_t * pObj )
61{
62 return pObj->TravId == pObj->pMan->nTravIds - 2 || pObj->TravId == pObj->pMan->nTravIds;
63}
64static inline int Nwk_ObjVisitedTop( Nwk_Obj_t * pObj )
65{
66 return pObj->TravId == pObj->pMan->nTravIds - 1 || pObj->TravId == pObj->pMan->nTravIds;
67}
68static inline void Nwk_ObjSetVisitedBot( Nwk_Obj_t * pObj )
69{
70 if ( pObj->TravId < pObj->pMan->nTravIds - 2 )
71 pObj->TravId = pObj->pMan->nTravIds - 2;
72 else if ( pObj->TravId == pObj->pMan->nTravIds - 1 )
73 pObj->TravId = pObj->pMan->nTravIds;
74 else
75 assert( 0 );
76}
77static inline void Nwk_ObjSetVisitedTop( Nwk_Obj_t * pObj )
78{
79 if ( pObj->TravId < pObj->pMan->nTravIds - 2 )
80 pObj->TravId = pObj->pMan->nTravIds - 1;
81 else if ( pObj->TravId == pObj->pMan->nTravIds - 2 )
82 pObj->TravId = pObj->pMan->nTravIds;
83 else
84 assert( 0 );
85}
86static inline Nwk_ManIncrementTravIdFlow( Nwk_Man_t * pMan )
87{
91}
92
93static int Nwk_ManPushForwardTop_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred );
94static int Nwk_ManPushForwardBot_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred );
95
96static int Nwk_ManPushBackwardTop_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred );
97static int Nwk_ManPushBackwardBot_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred );
98
102
115{
116 Nwk_Obj_t * pNext;
117 int i;
118 if ( pObj->MarkA )
119 return;
120 pObj->MarkA = 1;
121 Nwk_ObjForEachFanin( pObj, pNext, i )
122 Nwk_ManMarkTfiCone_rec( pNext );
123}
124
137{
138 Nwk_Obj_t * pNext;
139 int i;
140 if ( pObj->MarkA )
141 return;
142 pObj->MarkA = 1;
143 Nwk_ObjForEachFanout( pObj, pNext, i )
144 Nwk_ManMarkTfoCone_rec( pNext );
145}
146
159{
160 Nwk_Obj_t * pNext;
161 int i;
162 if ( Nwk_ObjIsTravIdCurrent( pObj ) )
163 return 0;
164 Nwk_ObjSetTravIdCurrent( pObj );
165 if ( Nwk_ObjHasFlow(pObj) )
166 return 0;
167 if ( Nwk_ObjIsSink(pObj) )
168 {
169 Nwk_ObjSetFlow(pObj);
170 return Nwk_ObjSetPred( pObj, pPred );
171 }
172 Nwk_ObjForEachFanout( pObj, pNext, i )
173 if ( Nwk_ManPushForwardFast_rec( pNext, pObj ) )
174 {
175 Nwk_ObjSetFlow(pObj);
176 return Nwk_ObjSetPred( pObj, pPred );
177 }
178 return 0;
179}
180
193{
194 Nwk_Obj_t * pNext;
195 int i;
196 if ( Nwk_ObjIsTravIdCurrent( pObj ) )
197 return 0;
198 Nwk_ObjSetTravIdCurrent( pObj );
199 if ( Nwk_ObjHasFlow(pObj) )
200 return 0;
201 if ( Nwk_ObjIsSink(pObj) )
202 {
203 Nwk_ObjSetFlow(pObj);
204 return Nwk_ObjSetPred( pObj, pPred );
205 }
206 Nwk_ObjForEachFanin( pObj, pNext, i )
207 if ( Nwk_ManPushBackwardFast_rec( pNext, pObj ) )
208 {
209 Nwk_ObjSetFlow(pObj);
210 return Nwk_ObjSetPred( pObj, pPred );
211 }
212 return 0;
213}
214
226int Nwk_ManPushForwardBot_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred )
227{
228 Nwk_Obj_t * pNext;
229 int i;
230 if ( Nwk_ObjVisitedBot(pObj) )
231 return 0;
232 Nwk_ObjSetVisitedBot(pObj);
233 DepthFwd++;
234 if ( DepthFwdMax < DepthFwd )
236 // propagate through the internal edge
237 if ( Nwk_ObjHasFlow(pObj) )
238 {
239 if ( Nwk_ObjPred(pObj) )
240 if ( Nwk_ManPushForwardTop_rec( Nwk_ObjPred(pObj), Nwk_ObjPred(pObj) ) )
241 {
242 DepthFwd--;
243 return Nwk_ObjSetPred( pObj, pPred );
244 }
245 }
246 else if ( Nwk_ManPushForwardTop_rec(pObj, pObj) )
247 {
248 DepthFwd--;
249 Nwk_ObjSetFlow( pObj );
250 return Nwk_ObjSetPred( pObj, pPred );
251 }
252 // try to push through the fanins
253 Nwk_ObjForEachFanin( pObj, pNext, i )
254 if ( Nwk_ManPushForwardBot_rec( pNext, pPred ) )
255 {
256 DepthFwd--;
257 return 1;
258 }
259 DepthFwd--;
260 return 0;
261}
262
274int Nwk_ManPushForwardTop_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred )
275{
276 Nwk_Obj_t * pNext;
277 int i;
278 if ( Nwk_ObjVisitedTop(pObj) )
279 return 0;
280 Nwk_ObjSetVisitedTop(pObj);
281 // check if this is the sink
282 if ( Nwk_ObjIsSink(pObj) )
283 return 1;
284 DepthFwd++;
285 if ( DepthFwdMax < DepthFwd )
287 // try to push through the fanouts
288 Nwk_ObjForEachFanout( pObj, pNext, i )
289 if ( Nwk_ManPushForwardBot_rec( pNext, pPred ) )
290 {
291 DepthFwd--;
292 return 1;
293 }
294 // redirect the flow
295 if ( Nwk_ObjHasFlow(pObj) && !Nwk_ObjIsCi(pObj) )
296 if ( Nwk_ManPushForwardBot_rec( pObj, Nwk_ObjPred(pObj) ) )
297 {
298 DepthFwd--;
299 Nwk_ObjClearFlow( pObj );
300 return Nwk_ObjSetPred( pObj, NULL );
301 }
302 DepthFwd--;
303 return 0;
304}
305
317int Nwk_ManPushBackwardBot_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred )
318{
319 if ( Nwk_ObjVisitedBot(pObj) )
320 return 0;
321 Nwk_ObjSetVisitedBot(pObj);
322 // propagate through the internal edge
323 if ( Nwk_ObjHasFlow(pObj) )
324 {
325 if ( Nwk_ObjPred(pObj) )
326 if ( Nwk_ManPushBackwardTop_rec( Nwk_ObjPred(pObj), Nwk_ObjPred(pObj) ) )
327 return Nwk_ObjSetPred( pObj, pPred );
328 }
329 else if ( Nwk_ManPushBackwardTop_rec(pObj, pObj) )
330 {
331 Nwk_ObjSetFlow( pObj );
332 return Nwk_ObjSetPred( pObj, pPred );
333 }
334 return 0;
335}
336
348int Nwk_ManPushBackwardTop_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred )
349{
350 Nwk_Obj_t * pNext;
351 int i;
352 if ( Nwk_ObjVisitedTop(pObj) )
353 return 0;
354 Nwk_ObjSetVisitedTop(pObj);
355 // check if this is the sink
356 if ( Nwk_ObjIsSink(pObj) )
357 return 1;
358 // try to push through the fanins
359 Nwk_ObjForEachFanin( pObj, pNext, i )
360 if ( Nwk_ManPushBackwardBot_rec( pNext, pPred ) )
361 return 1;
362 // try to push through the fanouts
363 Nwk_ObjForEachFanout( pObj, pNext, i )
364 if ( !Nwk_ObjIsCo(pObj) && Nwk_ManPushBackwardTop_rec( pNext, pPred ) )
365 return 1;
366 // redirect the flow
367 if ( Nwk_ObjHasFlow(pObj) )
368 if ( Nwk_ObjPred(pObj) && Nwk_ManPushBackwardBot_rec( pObj, Nwk_ObjPred(pObj) ) )
369 {
370 Nwk_ObjClearFlow( pObj );
371 return Nwk_ObjSetPred( pObj, NULL );
372 }
373 return 0;
374}
375
388{
389 Nwk_Obj_t * pNext;
390 int i;
391 if ( pObj->MarkA )
392 return 1;
393 if ( Nwk_ObjIsLo(pObj) )
394 return 0;
395 if ( Nwk_ObjIsTravIdCurrent( pObj ) )
396 return 1;
397 Nwk_ObjSetTravIdCurrent( pObj );
398 Nwk_ObjForEachFanin( pObj, pNext, i )
399 if ( !Nwk_ManVerifyCut_rec( pNext ) )
400 return 0;
401 return 1;
402}
403
416{
417 Nwk_Obj_t * pObj;
418 int i;
419 // mark the nodes
420 Vec_PtrForEachEntry( Nwk_Obj_t *, vNodes, pObj, i )
421 {
422 assert( pObj->MarkA == 0 );
423 pObj->MarkA = 1;
424 }
425 // traverse from the COs
427 Nwk_ManForEachCo( pMan, pObj, i )
428 if ( !Nwk_ManVerifyCut_rec( pObj ) )
429 printf( "Nwk_ManRetimeVerifyCutForward(): Internal cut verification failed.\n" );
430 // unmark the nodes
431 Vec_PtrForEachEntry( Nwk_Obj_t *, vNodes, pObj, i )
432 pObj->MarkA = 0;
433 return 1;
434}
435
448{
449 return 1;
450}
451
463Vec_Ptr_t * Nwk_ManRetimeCutForward( Nwk_Man_t * pMan, int nLatches, int fVerbose )
464{
465 Vec_Ptr_t * vNodes;
466 Nwk_Obj_t * pObj;
467 int i, RetValue, Counter = 0, Counter2 = 0;
468 clock_t clk = clock();
469 // set the sequential parameters
470 pMan->nLatches = nLatches;
471 pMan->nTruePis = Nwk_ManCiNum(pMan) - nLatches;
472 pMan->nTruePos = Nwk_ManCoNum(pMan) - nLatches;
473 // mark the COs and the TFO of PIs
474 Nwk_ManForEachCo( pMan, pObj, i )
475 pObj->MarkA = 1;
476 Nwk_ManForEachPiSeq( pMan, pObj, i )
478 // start flow computation from each LO
479 Nwk_ManIncrementTravIdFlow( pMan );
480 Nwk_ManForEachLoSeq( pMan, pObj, i )
481 {
482 if ( !Nwk_ManPushForwardFast_rec( pObj, NULL ) )
483 continue;
484 Nwk_ManIncrementTravIdFlow( pMan );
485 Counter++;
486 }
487 if ( fVerbose )
488 printf( "Forward: Max-flow = %4d -> ", Counter );
489 // continue flow computation from each LO
490 DepthFwdMax = DepthFwd = 0;
491 Nwk_ManIncrementTravIdFlow( pMan );
492 Nwk_ManForEachLoSeq( pMan, pObj, i )
493 {
494 printf( "%d ", DepthFwdMax );
495 if ( !Nwk_ManPushForwardBot_rec( pObj, NULL ) )
496 continue;
497 assert( DepthFwd == 0 );
498 Nwk_ManIncrementTravIdFlow( pMan );
499 Counter2++;
500 }
501 printf( "DepthMax = %d.\n", DepthFwdMax );
502 if ( fVerbose )
503 printf( "%4d. ", Counter+Counter2 );
504 // repeat flow computation from each LO
505 if ( Counter2 > 0 )
506 {
507 Nwk_ManIncrementTravIdFlow( pMan );
508 Nwk_ManForEachLoSeq( pMan, pObj, i )
509 {
510 RetValue = Nwk_ManPushForwardBot_rec( pObj, NULL );
511 assert( !RetValue );
512 }
513 }
514 // cut is a set of nodes whose bottom is visited but top is not visited
515 vNodes = Vec_PtrAlloc( Counter+Counter2 );
516 Counter = 0;
517 Nwk_ManForEachObj( pMan, pObj, i )
518 {
519 if ( Nwk_ObjVisitedBotOnly(pObj) )
520 {
521 assert( Nwk_ObjHasFlow(pObj) );
522 assert( !Nwk_ObjIsCo(pObj) );
523 Vec_PtrPush( vNodes, pObj );
524 Counter += Nwk_ObjIsCi(pObj);
525 }
526 }
527 Nwk_ManCleanMarks( pMan );
528 assert( Nwk_ManRetimeVerifyCutForward(pMan, vNodes) );
529 if ( fVerbose )
530 {
531 printf( "Min-cut = %4d. Unmoved = %4d. ", Vec_PtrSize(vNodes), Counter );
532 PRT( "Time", clock() - clk );
533 }
534 return vNodes;
535}
536
548Vec_Ptr_t * Nwk_ManRetimeCutBackward( Nwk_Man_t * pMan, int nLatches, int fVerbose )
549{
550 Vec_Ptr_t * vNodes;
551 Nwk_Obj_t * pObj;
552 int i, RetValue, Counter = 0, Counter2 = 0;
553 clock_t clk = clock();
554 // set the sequential parameters
555 pMan->nLatches = nLatches;
556 pMan->nTruePis = Nwk_ManCiNum(pMan) - nLatches;
557 pMan->nTruePos = Nwk_ManCoNum(pMan) - nLatches;
558 // mark the CIs, the TFI of POs, and the constant nodes
559 Nwk_ManForEachCi( pMan, pObj, i )
560 pObj->MarkA = 1;
561 Nwk_ManForEachPoSeq( pMan, pObj, i )
563 Nwk_ManForEachNode( pMan, pObj, i )
564 if ( Nwk_ObjFaninNum(pObj) == 0 )
565 pObj->MarkA = 1;
566 // start flow computation from each LI driver
567 Nwk_ManIncrementTravIdFlow( pMan );
568 Nwk_ManForEachLiSeq( pMan, pObj, i )
569 {
570 if ( !Nwk_ManPushBackwardFast_rec( Nwk_ObjFanin0(pObj), NULL ) )
571 continue;
572 Nwk_ManIncrementTravIdFlow( pMan );
573 Counter++;
574 }
575 if ( fVerbose )
576 printf( "Backward: Max-flow = %4d -> ", Counter );
577 // continue flow computation from each LI driver
578 Nwk_ManIncrementTravIdFlow( pMan );
579 Nwk_ManForEachLiSeq( pMan, pObj, i )
580 {
581 if ( !Nwk_ManPushBackwardBot_rec( Nwk_ObjFanin0(pObj), NULL ) )
582 continue;
583 Nwk_ManIncrementTravIdFlow( pMan );
584 Counter2++;
585 }
586 if ( fVerbose )
587 printf( "%4d. ", Counter+Counter2 );
588 // repeat flow computation from each LI driver
589 if ( Counter2 > 0 )
590 {
591 Nwk_ManIncrementTravIdFlow( pMan );
592 Nwk_ManForEachLiSeq( pMan, pObj, i )
593 {
594 RetValue = Nwk_ManPushBackwardBot_rec( Nwk_ObjFanin0(pObj), NULL );
595 assert( !RetValue );
596 }
597 }
598 // cut is a set of nodes whose bottom is visited but top is not visited
599 vNodes = Vec_PtrAlloc( Counter+Counter2 );
600 Nwk_ManForEachObj( pMan, pObj, i )
601 {
602 if ( Nwk_ObjVisitedBotOnly(pObj) )
603 {
604 assert( Nwk_ObjHasFlow(pObj) );
605 assert( !Nwk_ObjIsCo(pObj) );
606 Vec_PtrPush( vNodes, pObj );
607 }
608 }
609 // count CO drivers
610 Counter = 0;
611 Nwk_ManForEachLiSeq( pMan, pObj, i )
612 if ( Nwk_ObjVisitedBotOnly( Nwk_ObjFanin0(pObj) ) )
613 Counter++;
614 Nwk_ManCleanMarks( pMan );
615 assert( Nwk_ManRetimeVerifyCutBackward(pMan, vNodes) );
616 if ( fVerbose )
617 {
618 printf( "Min-cut = %4d. Unmoved = %4d. ", Vec_PtrSize(vNodes), Counter );
619 PRT( "Time", clock() - clk );
620 }
621 return vNodes;
622}
623
624
628
629
631
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
#define PRT(FMT,...)
Cube * p
Definition exorList.c:222
struct Nwk_Man_t_ Nwk_Man_t
Definition ntlnwk.h:41
ABC_NAMESPACE_IMPL_START int DepthFwdMax
ABC_NAMESPACE_IMPL_START int DepthBwd
int Nwk_ManPushBackwardFast_rec(Nwk_Obj_t *pObj, Nwk_Obj_t *pPred)
int Nwk_ManRetimeVerifyCutForward(Nwk_Man_t *pMan, Vec_Ptr_t *vNodes)
Vec_Ptr_t * Nwk_ManRetimeCutBackward(Nwk_Man_t *pMan, int nLatches, int fVerbose)
Vec_Ptr_t * Nwk_ManRetimeCutForward(Nwk_Man_t *pMan, int nLatches, int fVerbose)
void Nwk_ManMarkTfiCone_rec(Nwk_Obj_t *pObj)
FUNCTION DEFINITIONS ///.
int Nwk_ManVerifyCut_rec(Nwk_Obj_t *pObj)
int Nwk_ManPushForwardFast_rec(Nwk_Obj_t *pObj, Nwk_Obj_t *pPred)
int Nwk_ManRetimeVerifyCutBackward(Nwk_Man_t *pMan, Vec_Ptr_t *vNodes)
ABC_NAMESPACE_IMPL_START int DepthBwdMax
void Nwk_ManMarkTfoCone_rec(Nwk_Obj_t *pObj)
ABC_NAMESPACE_IMPL_START int DepthFwd
ABC_DLL void Nwk_ManIncrementTravId(Nwk_Man_t *pNtk)
DECLARATIONS ///.
Definition nwkUtil.c:47
#define Nwk_ManForEachNode(p, pObj, i)
Definition nwk.h:192
#define Nwk_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition nwk.h:179
#define Nwk_ManForEachLoSeq(p, pObj, i)
Definition nwk.h:209
typedefABC_NAMESPACE_HEADER_START struct Nwk_Obj_t_ Nwk_Obj_t
INCLUDES ///.
Definition nwk.h:49
#define Nwk_ManForEachPoSeq(p, pObj, i)
Definition nwk.h:207
#define Nwk_ManForEachObj(p, pObj, i)
Definition nwk.h:189
#define Nwk_ObjForEachFanout(pObj, pFanout, i)
Definition nwk.h:201
#define Nwk_ManForEachCo(p, pObj, i)
Definition nwk.h:181
#define Nwk_ObjForEachFanin(pObj, pFanin, i)
Definition nwk.h:199
ABC_DLL void Nwk_ManCleanMarks(Nwk_Man_t *pNtk)
Definition nwkUtil.c:464
#define Nwk_ManForEachLiSeq(p, pObj, i)
Definition nwk.h:211
#define Nwk_ManForEachPiSeq(p, pObj, i)
Definition nwk.h:205
int nLatches
Definition nwk.h:81
int nTruePis
Definition nwk.h:82
int nTruePos
Definition nwk.h:83
#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