ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Functions
llb4Sweep.c File Reference
#include "llbInt.h"
Include dependency graph for llb4Sweep.c:

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START void Llb_Nonlin4SweepOrder_rec (Aig_Man_t *pAig, Aig_Obj_t *pObj, Vec_Int_t *vOrder, int *pCounter, int fSaveAll)
 DECLARATIONS ///.
 
Vec_Int_t * Llb_Nonlin4SweepOrder (Aig_Man_t *pAig, int *pCounter, int fSaveAll)
 
int Llb4_Nonlin4SweepCutpoints (Aig_Man_t *pAig, Vec_Int_t *vOrder, int nBddLimit, int fVerbose)
 
DdNode * Llb_Nonlin4SweepPartitions_rec (DdManager *dd, Aig_Obj_t *pObj, Vec_Int_t *vOrder, Vec_Ptr_t *vRoots)
 
Vec_Ptr_t * Llb_Nonlin4SweepPartitions (DdManager *dd, Aig_Man_t *pAig, Vec_Int_t *vOrder, int fTransition)
 
DdNode * Llb4_Nonlin4SweepBadMonitor (Aig_Man_t *pAig, Vec_Int_t *vOrder, DdManager *dd)
 
Vec_Int_t * Llb_Nonlin4SweepVars2Q (Aig_Man_t *pAig, Vec_Int_t *vOrder, int fAddLis)
 
void Llb_Nonlin4SweepDeref (DdManager *dd, Vec_Ptr_t *vParts)
 
void Llb_Nonlin4SweepPrint (Vec_Ptr_t *vFuncs)
 
DdManager * Llb4_Nonlin4SweepBadStates (Aig_Man_t *pAig, Vec_Int_t *vOrder, int nVars)
 
DdManager * Llb4_Nonlin4SweepGroups (Aig_Man_t *pAig, Vec_Int_t *vOrder, int nVars, Vec_Ptr_t **pvGroups, int nBddLimitClp, int fVerbose)
 
void Llb_Nonlin4SweepPrintSuppProfile (DdManager *dd, Aig_Man_t *pAig, Vec_Int_t *vOrder, Vec_Ptr_t *vGroups, int fVerbose)
 
void Llb4_Nonlin4Sweep (Aig_Man_t *pAig, int nSweepMax, int nClusterMax, DdManager **pdd, Vec_Int_t **pvOrder, Vec_Ptr_t **pvGroups, int fVerbose)
 
void Llb4_Nonlin4SweepExperiment (Aig_Man_t *pAig)
 

Function Documentation

◆ Llb4_Nonlin4Sweep()

void Llb4_Nonlin4Sweep ( Aig_Man_t * pAig,
int nSweepMax,
int nClusterMax,
DdManager ** pdd,
Vec_Int_t ** pvOrder,
Vec_Ptr_t ** pvGroups,
int fVerbose )

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

Synopsis [Performs BDD sweep on the netlist.]

Description [Returns BDD manager, ordering, clusters, and bad states inside dd->bFunc.]

SideEffects []

SeeAlso []

Definition at line 520 of file llb4Sweep.c.

521{
522 DdManager * ddBad, * ddWork;
523 Vec_Ptr_t * vGroups;
524 Vec_Int_t * vOrder;
525 int Counter, nCutPoints;
526
527 // get the original ordering
528 Aig_ManCleanMarkA( pAig );
529 vOrder = Llb_Nonlin4SweepOrder( pAig, &Counter, 1 );
530 assert( Counter == Aig_ManNodeNum(pAig) );
531 // mark the nodes
532 nCutPoints = Llb4_Nonlin4SweepCutpoints( pAig, vOrder, nSweepMax, fVerbose );
533 Vec_IntFree( vOrder );
534 // get better ordering
535 vOrder = Llb_Nonlin4SweepOrder( pAig, &Counter, 0 );
536 assert( Counter == nCutPoints );
537 Aig_ManCleanMarkA( pAig );
538 // compute the BAD states
539 ddBad = Llb4_Nonlin4SweepBadStates( pAig, vOrder, nCutPoints + Aig_ManCiNum(pAig) + Aig_ManCoNum(pAig) );
540 // compute the clusters
541 ddWork = Llb4_Nonlin4SweepGroups( pAig, vOrder, nCutPoints + Aig_ManCiNum(pAig) + Aig_ManCoNum(pAig), &vGroups, nClusterMax, fVerbose );
542 // transfer the result from the Bad manager
543//printf( "Bad before = %d.\n", Cudd_DagSize(ddBad->bFunc) );
544 ddWork->bFunc = Cudd_bddTransfer( ddBad, ddWork, ddBad->bFunc ); Cudd_Ref( ddWork->bFunc );
545 Cudd_RecursiveDeref( ddBad, ddBad->bFunc ); ddBad->bFunc = NULL;
546 Extra_StopManager( ddBad );
547 // update ordering to exclude quantified variables
548//printf( "Bad after = %d.\n", Cudd_DagSize(ddWork->bFunc) );
549
550 Llb_Nonlin4SweepPrintSuppProfile( ddWork, pAig, vOrder, vGroups, fVerbose );
551
552 // return the result
553 *pdd = ddWork;
554 *pvOrder = vOrder;
555 *pvGroups = vGroups;
556}
Aig_ManCleanMarkA
void Aig_ManCleanMarkA(Aig_Man_t *p)
Definition aigUtil.c:148
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
Extra_StopManager
void Extra_StopManager(DdManager *dd)
Definition extraBddMisc.c:223
Llb4_Nonlin4SweepGroups
DdManager * Llb4_Nonlin4SweepGroups(Aig_Man_t *pAig, Vec_Int_t *vOrder, int nVars, Vec_Ptr_t **pvGroups, int nBddLimitClp, int fVerbose)
Definition llb4Sweep.c:420
Llb_Nonlin4SweepPrintSuppProfile
void Llb_Nonlin4SweepPrintSuppProfile(DdManager *dd, Aig_Man_t *pAig, Vec_Int_t *vOrder, Vec_Ptr_t *vGroups, int fVerbose)
Definition llb4Sweep.c:461
Llb4_Nonlin4SweepBadStates
DdManager * Llb4_Nonlin4SweepBadStates(Aig_Man_t *pAig, Vec_Int_t *vOrder, int nVars)
Definition llb4Sweep.c:384
Llb4_Nonlin4SweepCutpoints
int Llb4_Nonlin4SweepCutpoints(Aig_Man_t *pAig, Vec_Int_t *vOrder, int nBddLimit, int fVerbose)
Definition llb4Sweep.c:121
Llb_Nonlin4SweepOrder
Vec_Int_t * Llb_Nonlin4SweepOrder(Aig_Man_t *pAig, int *pCounter, int fSaveAll)
Definition llb4Sweep.c:86
assert
#define assert(ex)
Definition util_old.h:213
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Llb4_Nonlin4SweepBadMonitor()

DdNode * Llb4_Nonlin4SweepBadMonitor ( Aig_Man_t * pAig,
Vec_Int_t * vOrder,
DdManager * dd )

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

Synopsis [Get bad state monitor.]

Description []

SideEffects []

SeeAlso []

Definition at line 285 of file llb4Sweep.c.

286{
287 Aig_Obj_t * pObj;
288 DdNode * bRes, * bVar, * bTemp;
289 int i;
290 abctime TimeStop;
291 TimeStop = dd->TimeStop; dd->TimeStop = 0;
292 bRes = Cudd_ReadOne( dd ); Cudd_Ref( bRes );
293 Saig_ManForEachPo( pAig, pObj, i )
294 {
295 bVar = Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) );
296 bRes = Cudd_bddAnd( dd, bTemp = bRes, Cudd_Not(bVar) ); Cudd_Ref( bRes );
297 Cudd_RecursiveDeref( dd, bTemp );
298 }
299 Cudd_Deref( bRes );
300 dd->TimeStop = TimeStop;
301 return Cudd_Not(bRes);
302}
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
Aig_Obj_t
struct Aig_Obj_t_ Aig_Obj_t
Definition aig.h:51
Saig_ManForEachPo
#define Saig_ManForEachPo(p, pObj, i)
Definition saig.h:93
Here is the caller graph for this function:

◆ Llb4_Nonlin4SweepBadStates()

DdManager * Llb4_Nonlin4SweepBadStates ( Aig_Man_t * pAig,
Vec_Int_t * vOrder,
int nVars )

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

Synopsis [Computes bad states.]

Description []

SideEffects []

SeeAlso []

Definition at line 384 of file llb4Sweep.c.

385{
386 DdManager * dd;
387 Vec_Ptr_t * vParts;
388 Vec_Int_t * vVars2Q;
389 DdNode * bMonitor, * bImage;
390 // get quantifiable variables
391 vVars2Q = Llb_Nonlin4SweepVars2Q( pAig, vOrder, 0 );
392 // start BDD manager and create partitions
393 dd = Cudd_Init( nVars, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
394 vParts = Llb_Nonlin4SweepPartitions( dd, pAig, vOrder, 0 );
395//printf( "Outputs: " );
396//Llb_Nonlin4SweepPrint( vParts );
397 // compute image of the partitions
398 bMonitor = Llb4_Nonlin4SweepBadMonitor( pAig, vOrder, dd ); Cudd_Ref( bMonitor );
399 Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
400 bImage = Llb_Nonlin4Image( dd, vParts, bMonitor, vVars2Q ); Cudd_Ref( bImage );
401 Cudd_RecursiveDeref( dd, bMonitor );
402 Llb_Nonlin4SweepDeref( dd, vParts );
403 Vec_IntFree( vVars2Q );
404 // save image and return
405 dd->bFunc = bImage;
406 return dd;
407}
Llb_Nonlin4Image
DdNode * Llb_Nonlin4Image(DdManager *dd, Vec_Ptr_t *vParts, DdNode *bCurrent, Vec_Int_t *vVars2Q)
Definition llb4Image.c:752
Llb4_Nonlin4SweepBadMonitor
DdNode * Llb4_Nonlin4SweepBadMonitor(Aig_Man_t *pAig, Vec_Int_t *vOrder, DdManager *dd)
Definition llb4Sweep.c:285
Llb_Nonlin4SweepVars2Q
Vec_Int_t * Llb_Nonlin4SweepVars2Q(Aig_Man_t *pAig, Vec_Int_t *vOrder, int fAddLis)
Definition llb4Sweep.c:315
Llb_Nonlin4SweepPartitions
Vec_Ptr_t * Llb_Nonlin4SweepPartitions(DdManager *dd, Aig_Man_t *pAig, Vec_Int_t *vOrder, int fTransition)
Definition llb4Sweep.c:251
Llb_Nonlin4SweepDeref
void Llb_Nonlin4SweepDeref(DdManager *dd, Vec_Ptr_t *vParts)
Definition llb4Sweep.c:343
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Llb4_Nonlin4SweepCutpoints()

int Llb4_Nonlin4SweepCutpoints ( Aig_Man_t * pAig,
Vec_Int_t * vOrder,
int nBddLimit,
int fVerbose )

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

Synopsis [Performs BDD sweep on the netlist.]

Description [Returns AIG with internal cut points labeled with fMarkA.]

SideEffects []

SeeAlso []

Definition at line 121 of file llb4Sweep.c.

122{
123 DdManager * dd;
124 DdNode * bFunc0, * bFunc1, * bFunc;
125 Aig_Obj_t * pObj;
126 int i, Counter = 0, Counter1 = 0;
127 dd = Cudd_Init( Aig_ManObjNumMax(pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
128 // assign elementary variables
129 Aig_ManCleanData( pAig );
130 Aig_ManForEachCi( pAig, pObj, i )
131 pObj->pData = Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) );
132 // sweep internal nodes
133 Aig_ManForEachNode( pAig, pObj, i )
134 {
135/*
136 if ( pObj->nRefs >= 4 )
137 {
138 bFunc = Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) ); Cudd_Ref( bFunc );
139 pObj->pData = bFunc;
140 Counter1++;
141 continue;
142 }
143*/
144 bFunc0 = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
145 bFunc1 = Cudd_NotCond( (DdNode *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) );
146 bFunc = Cudd_bddAnd( dd, bFunc0, bFunc1 ); Cudd_Ref( bFunc );
147 if ( Cudd_DagSize(bFunc) > nBddLimit )
148 {
149// if ( fVerbose )
150// printf( "Node %5d : Beg =%5d. ", i, Cudd_DagSize(bFunc) );
151
152 // add cutpoint at a larger one
153 Cudd_RecursiveDeref( dd, bFunc );
154 if ( Cudd_DagSize(bFunc0) >= Cudd_DagSize(bFunc1) )
155 {
156 Cudd_RecursiveDeref( dd, (DdNode *)Aig_ObjFanin0(pObj)->pData );
157 bFunc = Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, Aig_ObjFanin0(pObj)) );
158 Aig_ObjFanin0(pObj)->pData = bFunc; Cudd_Ref( bFunc );
159 Aig_ObjFanin0(pObj)->fMarkA = 1;
160
161// if ( fVerbose )
162// printf( "Ref =%3d ", Aig_ObjFanin0(pObj)->nRefs );
163 }
164 else
165 {
166 Cudd_RecursiveDeref( dd, (DdNode *)Aig_ObjFanin1(pObj)->pData );
167 bFunc = Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, Aig_ObjFanin1(pObj)) );
168 Aig_ObjFanin1(pObj)->pData = bFunc; Cudd_Ref( bFunc );
169 Aig_ObjFanin1(pObj)->fMarkA = 1;
170
171// if ( fVerbose )
172// printf( "Ref =%3d ", Aig_ObjFanin1(pObj)->nRefs );
173 }
174 // perform new operation
175 bFunc0 = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
176 bFunc1 = Cudd_NotCond( (DdNode *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) );
177 bFunc = Cudd_bddAnd( dd, bFunc0, bFunc1 ); Cudd_Ref( bFunc );
178// assert( Cudd_DagSize(bFunc) <= nBddLimit );
179
180// if ( fVerbose )
181// printf( "End =%5d.\n", Cudd_DagSize(bFunc) );
182 Counter++;
183 }
184 pObj->pData = bFunc;
185//printf( "%d ", Cudd_DagSize(bFunc) );
186 }
187//printf( "\n" );
188 // clean up
189 Aig_ManForEachNode( pAig, pObj, i )
190 Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData );
191 Extra_StopManager( dd );
192// Aig_ManCleanMarkA( pAig );
193 if ( fVerbose )
194 printf( "Added %d cut points. Used %d high fanout points.\n", Counter, Counter1 );
195 return Counter + Counter1;
196}
Aig_ManForEachCi
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition aig.h:393
Aig_ManForEachNode
#define Aig_ManForEachNode(p, pObj, i)
Definition aig.h:413
Aig_ManCleanData
void Aig_ManCleanData(Aig_Man_t *p)
Definition aigUtil.c:205
Aig_Obj_t_::pData
void * pData
Definition aig.h:87
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Llb4_Nonlin4SweepExperiment()

void Llb4_Nonlin4SweepExperiment ( Aig_Man_t * pAig)

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

Synopsis [Performs BDD sweep on the netlist.]

Description []

SideEffects []

SeeAlso []

Definition at line 569 of file llb4Sweep.c.

570{
571 DdManager * dd;
572 Vec_Int_t * vOrder;
573 Vec_Ptr_t * vGroups;
574 Llb4_Nonlin4Sweep( pAig, 100, 500, &dd, &vOrder, &vGroups, 1 );
575
576 Llb_Nonlin4SweepDeref( dd, vGroups );
577
578 Cudd_RecursiveDeref( dd, dd->bFunc );
579 Extra_StopManager( dd );
580 Vec_IntFree( vOrder );
581}
Llb4_Nonlin4Sweep
void Llb4_Nonlin4Sweep(Aig_Man_t *pAig, int nSweepMax, int nClusterMax, DdManager **pdd, Vec_Int_t **pvOrder, Vec_Ptr_t **pvGroups, int fVerbose)
Definition llb4Sweep.c:520
Here is the call graph for this function:

◆ Llb4_Nonlin4SweepGroups()

DdManager * Llb4_Nonlin4SweepGroups ( Aig_Man_t * pAig,
Vec_Int_t * vOrder,
int nVars,
Vec_Ptr_t ** pvGroups,
int nBddLimitClp,
int fVerbose )

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

Synopsis [Computes clusters.]

Description []

SideEffects []

SeeAlso []

Definition at line 420 of file llb4Sweep.c.

421{
422 DdManager * dd;
423 Vec_Ptr_t * vParts;
424 Vec_Int_t * vVars2Q;
425 // get quantifiable variables
426 vVars2Q = Llb_Nonlin4SweepVars2Q( pAig, vOrder, 1 );
427 // start BDD manager and create partitions
428 dd = Cudd_Init( nVars, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
429 vParts = Llb_Nonlin4SweepPartitions( dd, pAig, vOrder, 1 );
430//printf( "Transitions: " );
431//Llb_Nonlin4SweepPrint( vParts );
432 // compute image of the partitions
433
434 Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
435 *pvGroups = Llb_Nonlin4Group( dd, vParts, vVars2Q, nBddLimitClp );
436 Llb_Nonlin4SweepDeref( dd, vParts );
437// *pvGroups = vParts;
438
439if ( fVerbose )
440{
441printf( "Groups: " );
442Llb_Nonlin4SweepPrint( *pvGroups );
443}
444
445 Vec_IntFree( vVars2Q );
446 return dd;
447}
Llb_Nonlin4Group
Vec_Ptr_t * Llb_Nonlin4Group(DdManager *dd, Vec_Ptr_t *vParts, Vec_Int_t *vVars2Q, int nSizeMax)
Definition llb4Image.c:806
Llb_Nonlin4SweepPrint
void Llb_Nonlin4SweepPrint(Vec_Ptr_t *vFuncs)
Definition llb4Sweep.c:363
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Llb_Nonlin4SweepDeref()

void Llb_Nonlin4SweepDeref ( DdManager * dd,
Vec_Ptr_t * vParts )

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

Synopsis [Multiply every partition by the cube.]

Description []

SideEffects []

SeeAlso []

Definition at line 343 of file llb4Sweep.c.

344{
345 DdNode * bFunc;
346 int i;
347 Vec_PtrForEachEntry( DdNode *, vParts, bFunc, i )
348 Cudd_RecursiveDeref( dd, bFunc );
349 Vec_PtrFree( vParts );
350}
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition vecPtr.h:55
Here is the caller graph for this function:

◆ Llb_Nonlin4SweepOrder()

Vec_Int_t * Llb_Nonlin4SweepOrder ( Aig_Man_t * pAig,
int * pCounter,
int fSaveAll )

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

Synopsis [Find good static variable ordering.]

Description []

SideEffects []

SeeAlso []

Definition at line 86 of file llb4Sweep.c.

87{
88 Vec_Int_t * vOrder;
89 Aig_Obj_t * pObj;
90 int i, Counter = 0;
91 // collect nodes in the order
92 vOrder = Vec_IntStartFull( Aig_ManObjNumMax(pAig) );
93 Aig_ManIncrementTravId( pAig );
94 Aig_ObjSetTravIdCurrent( pAig, Aig_ManConst1(pAig) );
95 Aig_ManForEachCo( pAig, pObj, i )
96 {
97 Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ );
98 Llb_Nonlin4SweepOrder_rec( pAig, Aig_ObjFanin0(pObj), vOrder, &Counter, fSaveAll );
99 }
100 Aig_ManForEachCi( pAig, pObj, i )
101 if ( Llb_ObjBddVar(vOrder, pObj) < 0 )
102 Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ );
103// assert( Counter == Aig_ManObjNum(pAig) - 1 ); // no dangling nodes
104 if ( pCounter )
105 *pCounter = Counter - Aig_ManCiNum(pAig) - Aig_ManCoNum(pAig);
106 return vOrder;
107}
Aig_ManIncrementTravId
void Aig_ManIncrementTravId(Aig_Man_t *p)
DECLARATIONS ///.
Definition aigUtil.c:44
Aig_ManForEachCo
#define Aig_ManForEachCo(p, pObj, i)
Definition aig.h:398
Llb_Nonlin4SweepOrder_rec
ABC_NAMESPACE_IMPL_START void Llb_Nonlin4SweepOrder_rec(Aig_Man_t *pAig, Aig_Obj_t *pObj, Vec_Int_t *vOrder, int *pCounter, int fSaveAll)
DECLARATIONS ///.
Definition llb4Sweep.c:45
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Llb_Nonlin4SweepOrder_rec()

ABC_NAMESPACE_IMPL_START void Llb_Nonlin4SweepOrder_rec ( Aig_Man_t * pAig,
Aig_Obj_t * pObj,
Vec_Int_t * vOrder,
int * pCounter,
int fSaveAll )

DECLARATIONS ///.

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

FileName [llb2Sweep.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [BDD based reachability.]

Synopsis [Non-linear quantification scheduling.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

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

] FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [Find good static variable ordering.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file llb4Sweep.c.

46{
47 Aig_Obj_t * pFanin0, * pFanin1;
48 if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
49 return;
50 Aig_ObjSetTravIdCurrent( pAig, pObj );
51 assert( Llb_ObjBddVar(vOrder, pObj) < 0 );
52 if ( Aig_ObjIsCi(pObj) )
53 {
54 Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), (*pCounter)++ );
55 return;
56 }
57 // try fanins with higher level first
58 pFanin0 = Aig_ObjFanin0(pObj);
59 pFanin1 = Aig_ObjFanin1(pObj);
60// if ( pFanin0->Level > pFanin1->Level || (pFanin0->Level == pFanin1->Level && pFanin0->Id < pFanin1->Id) )
61 if ( pFanin0->Level > pFanin1->Level )
62 {
63 Llb_Nonlin4SweepOrder_rec( pAig, pFanin0, vOrder, pCounter, fSaveAll );
64 Llb_Nonlin4SweepOrder_rec( pAig, pFanin1, vOrder, pCounter, fSaveAll );
65 }
66 else
67 {
68 Llb_Nonlin4SweepOrder_rec( pAig, pFanin1, vOrder, pCounter, fSaveAll );
69 Llb_Nonlin4SweepOrder_rec( pAig, pFanin0, vOrder, pCounter, fSaveAll );
70 }
71 if ( fSaveAll || pObj->fMarkA )
72 Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), (*pCounter)++ );
73}
Aig_Obj_t_::fMarkA
unsigned int fMarkA
Definition aig.h:79
Aig_Obj_t_::Level
unsigned Level
Definition aig.h:82
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Llb_Nonlin4SweepPartitions()

Vec_Ptr_t * Llb_Nonlin4SweepPartitions ( DdManager * dd,
Aig_Man_t * pAig,
Vec_Int_t * vOrder,
int fTransition )

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

Synopsis [Derives BDDs for the partitions.]

Description []

SideEffects []

SeeAlso []

Definition at line 251 of file llb4Sweep.c.

252{
253 Vec_Ptr_t * vRoots;
254 Aig_Obj_t * pObj;
255 int i;
256 Aig_ManCleanData( pAig );
257 vRoots = Vec_PtrAlloc( 100 );
258 if ( fTransition )
259 {
260 Saig_ManForEachLi( pAig, pObj, i )
261 Llb_Nonlin4SweepPartitions_rec( dd, pObj, vOrder, vRoots );
262 }
263 else
264 {
265 Saig_ManForEachPo( pAig, pObj, i )
266 Llb_Nonlin4SweepPartitions_rec( dd, pObj, vOrder, vRoots );
267 }
268 Aig_ManForEachNode( pAig, pObj, i )
269 if ( pObj->pData )
270 Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData );
271 return vRoots;
272}
Llb_Nonlin4SweepPartitions_rec
DdNode * Llb_Nonlin4SweepPartitions_rec(DdManager *dd, Aig_Obj_t *pObj, Vec_Int_t *vOrder, Vec_Ptr_t *vRoots)
Definition llb4Sweep.c:209
Saig_ManForEachLi
#define Saig_ManForEachLi(p, pObj, i)
Definition saig.h:98
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Llb_Nonlin4SweepPartitions_rec()

DdNode * Llb_Nonlin4SweepPartitions_rec ( DdManager * dd,
Aig_Obj_t * pObj,
Vec_Int_t * vOrder,
Vec_Ptr_t * vRoots )

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

Synopsis [Derives BDDs for the partitions.]

Description []

SideEffects []

SeeAlso []

Definition at line 209 of file llb4Sweep.c.

210{
211 DdNode * bBdd, * bBdd0, * bBdd1, * bPart, * vVar;
212 if ( Aig_ObjIsConst1(pObj) )
213 return Cudd_ReadOne(dd);
214 if ( Aig_ObjIsCi(pObj) )
215 return Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) );
216 if ( pObj->pData )
217 return (DdNode *)pObj->pData;
218 if ( Aig_ObjIsCo(pObj) )
219 {
220 bBdd0 = Cudd_NotCond( Llb_Nonlin4SweepPartitions_rec(dd, Aig_ObjFanin0(pObj), vOrder, vRoots), Aig_ObjFaninC0(pObj) );
221 bPart = Cudd_bddXnor( dd, Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) ), bBdd0 ); Cudd_Ref( bPart );
222 Vec_PtrPush( vRoots, bPart );
223 return NULL;
224 }
225 bBdd0 = Cudd_NotCond( Llb_Nonlin4SweepPartitions_rec(dd, Aig_ObjFanin0(pObj), vOrder, vRoots), Aig_ObjFaninC0(pObj) );
226 bBdd1 = Cudd_NotCond( Llb_Nonlin4SweepPartitions_rec(dd, Aig_ObjFanin1(pObj), vOrder, vRoots), Aig_ObjFaninC1(pObj) );
227 bBdd = Cudd_bddAnd( dd, bBdd0, bBdd1 ); Cudd_Ref( bBdd );
228 if ( Llb_ObjBddVar(vOrder, pObj) >= 0 )
229 {
230 vVar = Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) );
231 bPart = Cudd_bddXnor( dd, vVar, bBdd ); Cudd_Ref( bPart );
232 Vec_PtrPush( vRoots, bPart );
233 Cudd_RecursiveDeref( dd, bBdd );
234 bBdd = vVar; Cudd_Ref( vVar );
235 }
236 pObj->pData = bBdd;
237 return bBdd;
238}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Llb_Nonlin4SweepPrint()

void Llb_Nonlin4SweepPrint ( Vec_Ptr_t * vFuncs)

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

Synopsis [Multiply every partition by the cube.]

Description []

SideEffects []

SeeAlso []

Definition at line 363 of file llb4Sweep.c.

364{
365 DdNode * bFunc;
366 int i;
367 printf( "(%d) ", Vec_PtrSize(vFuncs) );
368 Vec_PtrForEachEntry( DdNode *, vFuncs, bFunc, i )
369 printf( "%d ", Cudd_DagSize(bFunc) );
370 printf( "\n" );
371}
Here is the caller graph for this function:

◆ Llb_Nonlin4SweepPrintSuppProfile()

void Llb_Nonlin4SweepPrintSuppProfile ( DdManager * dd,
Aig_Man_t * pAig,
Vec_Int_t * vOrder,
Vec_Ptr_t * vGroups,
int fVerbose )

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

Synopsis [Creates quantifiable variables for both types of traversal.]

Description []

SideEffects []

SeeAlso []

Definition at line 461 of file llb4Sweep.c.

462{
463 Aig_Obj_t * pObj;
464 int i, * pSupp;
465 int nSuppAll = 0, nSuppPi = 0, nSuppPo = 0, nSuppLi = 0, nSuppLo = 0, nSuppAnd = 0;
466
467 pSupp = ABC_CALLOC( int, Cudd_ReadSize(dd) );
468 Extra_VectorSupportArray( dd, (DdNode **)Vec_PtrArray(vGroups), Vec_PtrSize(vGroups), pSupp );
469
470 Aig_ManForEachObj( pAig, pObj, i )
471 {
472 if ( Llb_ObjBddVar(vOrder, pObj) < 0 )
473 continue;
474 // remove variables that do not participate
475 if ( pSupp[Llb_ObjBddVar(vOrder, pObj)] == 0 )
476 {
477 if ( Aig_ObjIsNode(pObj) )
478 Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), -1 );
479 continue;
480 }
481 nSuppAll++;
482 if ( Saig_ObjIsPi(pAig, pObj) )
483 nSuppPi++;
484 else if ( Saig_ObjIsLo(pAig, pObj) )
485 nSuppLo++;
486 else if ( Saig_ObjIsPo(pAig, pObj) )
487 nSuppPo++;
488 else if ( Saig_ObjIsLi(pAig, pObj) )
489 nSuppLi++;
490 else
491 nSuppAnd++;
492 }
493 ABC_FREE( pSupp );
494
495 if ( fVerbose )
496 {
497 printf( "Groups =%3d ", Vec_PtrSize(vGroups) );
498 printf( "Variables: all =%4d ", nSuppAll );
499 printf( "pi =%4d ", nSuppPi );
500 printf( "po =%4d ", nSuppPo );
501 printf( "lo =%4d ", nSuppLo );
502 printf( "li =%4d ", nSuppLi );
503 printf( "and =%4d", nSuppAnd );
504 printf( "\n" );
505 }
506}
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition abc_global.h:265
ABC_FREE
#define ABC_FREE(obj)
Definition abc_global.h:267
Aig_ManForEachObj
#define Aig_ManForEachObj(p, pObj, i)
Definition aig.h:403
Extra_VectorSupportArray
int * Extra_VectorSupportArray(DdManager *dd, DdNode **F, int n, int *support)
Definition extraBddMisc.c:572
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Llb_Nonlin4SweepVars2Q()

Vec_Int_t * Llb_Nonlin4SweepVars2Q ( Aig_Man_t * pAig,
Vec_Int_t * vOrder,
int fAddLis )

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

Synopsis [Creates quantifiable variables for both types of traversal.]

Description []

SideEffects []

SeeAlso []

Definition at line 315 of file llb4Sweep.c.

316{
317 Vec_Int_t * vVars2Q;
318 Aig_Obj_t * pObj;
319 int i;
320 vVars2Q = Vec_IntAlloc( 0 );
321 Vec_IntFill( vVars2Q, Aig_ManObjNumMax(pAig), 1 );
322 // add flop outputs
323 Saig_ManForEachLo( pAig, pObj, i )
324 Vec_IntWriteEntry( vVars2Q, Llb_ObjBddVar(vOrder, pObj), 0 );
325 // add flop inputs
326 if ( fAddLis )
327 Saig_ManForEachLi( pAig, pObj, i )
328 Vec_IntWriteEntry( vVars2Q, Llb_ObjBddVar(vOrder, pObj), 0 );
329 return vVars2Q;
330}
Saig_ManForEachLo
#define Saig_ManForEachLo(p, pObj, i)
Definition saig.h:96
Here is the caller graph for this function: