abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
aigMffc.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [aigMffc.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [AIG package.]
8 
9  Synopsis [Computation of MFFCs.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - April 28, 2007.]
16 
17  Revision [$Id: aigMffc.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "aig.h"
22 
23 ABC_NAMESPACE_IMPL_START
24 
25 
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29 
30 ////////////////////////////////////////////////////////////////////////
31 /// FUNCTION DEFINITIONS ///
32 ////////////////////////////////////////////////////////////////////////
33 
34 /**Function*************************************************************
35 
36  Synopsis [Dereferences the node's MFFC.]
37 
38  Description []
39 
40  SideEffects []
41 
42  SeeAlso []
43 
44 ***********************************************************************/
45 int Aig_NodeDeref_rec( Aig_Obj_t * pNode, unsigned LevelMin, float * pPower, float * pProbs )
46 {
47  float Power0 = 0.0, Power1 = 0.0;
48  Aig_Obj_t * pFanin;
49  int Counter = 0;
50  if ( pProbs )
51  *pPower = 0.0;
52  if ( Aig_ObjIsCi(pNode) )
53  return 0;
54  // consider the first fanin
55  pFanin = Aig_ObjFanin0(pNode);
56  assert( pFanin->nRefs > 0 );
57  if ( --pFanin->nRefs == 0 && (!LevelMin || pFanin->Level > LevelMin) )
58  Counter += Aig_NodeDeref_rec( pFanin, LevelMin, &Power0, pProbs );
59  if ( pProbs )
60  *pPower += Power0 + 2.0 * pProbs[pFanin->Id] * (1.0 - pProbs[pFanin->Id]);
61  // skip the buffer
62  if ( Aig_ObjIsBuf(pNode) )
63  return Counter;
64  assert( Aig_ObjIsNode(pNode) );
65  // consider the second fanin
66  pFanin = Aig_ObjFanin1(pNode);
67  assert( pFanin->nRefs > 0 );
68  if ( --pFanin->nRefs == 0 && (!LevelMin || pFanin->Level > LevelMin) )
69  Counter += Aig_NodeDeref_rec( pFanin, LevelMin, &Power1, pProbs );
70  if ( pProbs )
71  *pPower += Power1 + 2.0 * pProbs[pFanin->Id] * (1.0 - pProbs[pFanin->Id]);
72  return Counter + 1;
73 }
74 
75 /**Function*************************************************************
76 
77  Synopsis [References the node's MFFC.]
78 
79  Description []
80 
81  SideEffects []
82 
83  SeeAlso []
84 
85 ***********************************************************************/
86 int Aig_NodeRef_rec( Aig_Obj_t * pNode, unsigned LevelMin )
87 {
88  Aig_Obj_t * pFanin;
89  int Counter = 0;
90  if ( Aig_ObjIsCi(pNode) )
91  return 0;
92  // consider the first fanin
93  pFanin = Aig_ObjFanin0(pNode);
94  if ( pFanin->nRefs++ == 0 && (!LevelMin || pFanin->Level > LevelMin) )
95  Counter += Aig_NodeRef_rec( pFanin, LevelMin );
96  // skip the buffer
97  if ( Aig_ObjIsBuf(pNode) )
98  return Counter;
99  assert( Aig_ObjIsNode(pNode) );
100  // consider the second fanin
101  pFanin = Aig_ObjFanin1(pNode);
102  if ( pFanin->nRefs++ == 0 && (!LevelMin || pFanin->Level > LevelMin) )
103  Counter += Aig_NodeRef_rec( pFanin, LevelMin );
104  return Counter + 1;
105 }
106 
107 /**Function*************************************************************
108 
109  Synopsis [References the node's MFFC.]
110 
111  Description []
112 
113  SideEffects []
114 
115  SeeAlso []
116 
117 ***********************************************************************/
118 int Aig_NodeRefLabel_rec( Aig_Man_t * p, Aig_Obj_t * pNode, unsigned LevelMin )
119 {
120  Aig_Obj_t * pFanin;
121  int Counter = 0;
122  if ( Aig_ObjIsCi(pNode) )
123  return 0;
124  Aig_ObjSetTravIdCurrent( p, pNode );
125  // consider the first fanin
126  pFanin = Aig_ObjFanin0(pNode);
127  if ( pFanin->nRefs++ == 0 && (!LevelMin || pFanin->Level > LevelMin) )
128  Counter += Aig_NodeRefLabel_rec( p, pFanin, LevelMin );
129  if ( Aig_ObjIsBuf(pNode) )
130  return Counter;
131  assert( Aig_ObjIsNode(pNode) );
132  // consider the second fanin
133  pFanin = Aig_ObjFanin1(pNode);
134  if ( pFanin->nRefs++ == 0 && (!LevelMin || pFanin->Level > LevelMin) )
135  Counter += Aig_NodeRefLabel_rec( p, pFanin, LevelMin );
136  return Counter + 1;
137 }
138 
139 /**Function*************************************************************
140 
141  Synopsis [Collects the internal and boundary nodes in the derefed MFFC.]
142 
143  Description []
144 
145  SideEffects []
146 
147  SeeAlso []
148 
149 ***********************************************************************/
150 void Aig_NodeMffcSupp_rec( Aig_Man_t * p, Aig_Obj_t * pNode, unsigned LevelMin, Vec_Ptr_t * vSupp, int fTopmost, Aig_Obj_t * pObjSkip )
151 {
152  // skip visited nodes
153  if ( Aig_ObjIsTravIdCurrent(p, pNode) )
154  return;
155  Aig_ObjSetTravIdCurrent(p, pNode);
156  // add to the new support nodes
157  if ( !fTopmost && pNode != pObjSkip && (Aig_ObjIsCi(pNode) || pNode->nRefs > 0 || pNode->Level <= LevelMin) )
158  {
159  if ( vSupp ) Vec_PtrPush( vSupp, pNode );
160  return;
161  }
162  assert( Aig_ObjIsNode(pNode) );
163  // recur on the children
164  Aig_NodeMffcSupp_rec( p, Aig_ObjFanin0(pNode), LevelMin, vSupp, 0, pObjSkip );
165  Aig_NodeMffcSupp_rec( p, Aig_ObjFanin1(pNode), LevelMin, vSupp, 0, pObjSkip );
166 }
167 
168 /**Function*************************************************************
169 
170  Synopsis [Collects the support of depth-limited MFFC.]
171 
172  Description [Returns the number of internal nodes in the MFFC.]
173 
174  SideEffects []
175 
176  SeeAlso []
177 
178 ***********************************************************************/
179 int Aig_NodeMffcSupp( Aig_Man_t * p, Aig_Obj_t * pNode, int LevelMin, Vec_Ptr_t * vSupp )
180 {
181  int ConeSize1, ConeSize2;
182  if ( vSupp ) Vec_PtrClear( vSupp );
183  if ( !Aig_ObjIsNode(pNode) )
184  {
185  if ( Aig_ObjIsCi(pNode) && vSupp )
186  Vec_PtrPush( vSupp, pNode );
187  return 0;
188  }
189  assert( !Aig_IsComplement(pNode) );
190  assert( Aig_ObjIsNode(pNode) );
191  Aig_ManIncrementTravId( p );
192  ConeSize1 = Aig_NodeDeref_rec( pNode, LevelMin, NULL, NULL );
193  Aig_NodeMffcSupp_rec( p, pNode, LevelMin, vSupp, 1, NULL );
194  ConeSize2 = Aig_NodeRef_rec( pNode, LevelMin );
195  assert( ConeSize1 == ConeSize2 );
196  assert( ConeSize1 > 0 );
197  return ConeSize1;
198 }
199 
200 /**Function*************************************************************
201 
202  Synopsis [Labels the nodes in the MFFC.]
203 
204  Description [Returns the number of internal nodes in the MFFC.]
205 
206  SideEffects []
207 
208  SeeAlso []
209 
210 ***********************************************************************/
211 int Aig_NodeMffcLabel( Aig_Man_t * p, Aig_Obj_t * pNode, float * pPower )
212 {
213  int ConeSize1, ConeSize2;
214  assert( (pPower != NULL) == (p->vProbs != NULL) );
215  assert( !Aig_IsComplement(pNode) );
216  assert( Aig_ObjIsNode(pNode) );
217  Aig_ManIncrementTravId( p );
218  ConeSize1 = Aig_NodeDeref_rec( pNode, 0, pPower, p->vProbs? (float *)p->vProbs->pArray : NULL );
219  ConeSize2 = Aig_NodeRefLabel_rec( p, pNode, 0 );
220  assert( ConeSize1 == ConeSize2 );
221  assert( ConeSize1 > 0 );
222  return ConeSize1;
223 }
224 
225 /**Function*************************************************************
226 
227  Synopsis [Labels the nodes in the MFFC.]
228 
229  Description [Returns the number of internal nodes in the MFFC.]
230 
231  SideEffects []
232 
233  SeeAlso []
234 
235 ***********************************************************************/
236 int Aig_NodeMffcLabelCut( Aig_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vLeaves )
237 {
238  Aig_Obj_t * pObj;
239  int i, ConeSize1, ConeSize2;
240  assert( !Aig_IsComplement(pNode) );
241  assert( Aig_ObjIsNode(pNode) );
242  Aig_ManIncrementTravId( p );
243  Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pObj, i )
244  pObj->nRefs++;
245  ConeSize1 = Aig_NodeDeref_rec( pNode, 0, NULL, NULL );
246  ConeSize2 = Aig_NodeRefLabel_rec( p, pNode, 0 );
247  Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pObj, i )
248  pObj->nRefs--;
249  assert( ConeSize1 == ConeSize2 );
250  assert( ConeSize1 > 0 );
251  return ConeSize1;
252 }
253 
254 /**Function*************************************************************
255 
256  Synopsis [Expands the cut by adding the most closely related node.]
257 
258  Description [Returns 1 if the cut exists.]
259 
260  SideEffects []
261 
262  SeeAlso []
263 
264 ***********************************************************************/
265 int Aig_NodeMffcExtendCut( Aig_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vResult )
266 {
267  Aig_Obj_t * pObj, * pLeafBest;
268  int i, LevelMax, ConeSize1, ConeSize2, ConeCur1, ConeCur2, ConeBest;
269  // dereference the current cut
270  LevelMax = 0;
271  Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pObj, i )
272  LevelMax = Abc_MaxInt( LevelMax, (int)pObj->Level );
273  if ( LevelMax == 0 )
274  return 0;
275  // dereference the cut
276  ConeSize1 = Aig_NodeDeref_rec( pNode, 0, NULL, NULL );
277  // try expanding each node in the boundary
278  ConeBest = ABC_INFINITY;
279  pLeafBest = NULL;
280  Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pObj, i )
281  {
282  if ( (int)pObj->Level != LevelMax )
283  continue;
284  ConeCur1 = Aig_NodeDeref_rec( pObj, 0, NULL, NULL );
285  if ( ConeBest > ConeCur1 )
286  {
287  ConeBest = ConeCur1;
288  pLeafBest = pObj;
289  }
290  ConeCur2 = Aig_NodeRef_rec( pObj, 0 );
291  assert( ConeCur1 == ConeCur2 );
292  }
293  assert( pLeafBest != NULL );
294  assert( Aig_ObjIsNode(pLeafBest) );
295  // deref the best leaf
296  ConeCur1 = Aig_NodeDeref_rec( pLeafBest, 0, NULL, NULL );
297  // collect the cut nodes
298  Vec_PtrClear( vResult );
299  Aig_ManIncrementTravId( p );
300  Aig_NodeMffcSupp_rec( p, pNode, 0, vResult, 1, pLeafBest );
301  // ref the nodes
302  ConeCur2 = Aig_NodeRef_rec( pLeafBest, 0 );
303  assert( ConeCur1 == ConeCur2 );
304  // ref the original node
305  ConeSize2 = Aig_NodeRef_rec( pNode, 0 );
306  assert( ConeSize1 == ConeSize2 );
307  return 1;
308 }
309 
310 ////////////////////////////////////////////////////////////////////////
311 /// END OF FILE ///
312 ////////////////////////////////////////////////////////////////////////
313 
314 
315 ABC_NAMESPACE_IMPL_END
316 
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Aig_Obj_t_::Level
unsigned Level
Definition: aig.h:82
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Aig_ObjIsTravIdCurrent
static int Aig_ObjIsTravIdCurrent(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:295
Aig_NodeMffcExtendCut
int Aig_NodeMffcExtendCut(Aig_Man_t *p, Aig_Obj_t *pNode, Vec_Ptr_t *vLeaves, Vec_Ptr_t *vResult)
Definition: aigMffc.c:265
Aig_ObjFanin0
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
Aig_IsComplement
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
Aig_NodeRefLabel_rec
int Aig_NodeRefLabel_rec(Aig_Man_t *p, Aig_Obj_t *pNode, unsigned LevelMin)
Definition: aigMffc.c:118
Abc_MaxInt
static int Abc_MaxInt(int a, int b)
Definition: abc_global.h:238
Aig_ObjFanin1
static Aig_Obj_t * Aig_ObjFanin1(Aig_Obj_t *pObj)
Definition: aig.h:309
Aig_ObjSetTravIdCurrent
static void Aig_ObjSetTravIdCurrent(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:293
Aig_ManIncrementTravId
void Aig_ManIncrementTravId(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigUtil.c:44
Aig_ObjIsNode
static int Aig_ObjIsNode(Aig_Obj_t *pObj)
Definition: aig.h:280
Aig_ObjIsBuf
static int Aig_ObjIsBuf(Aig_Obj_t *pObj)
Definition: aig.h:277
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Aig_NodeRef_rec
int Aig_NodeRef_rec(Aig_Obj_t *pNode, unsigned LevelMin)
Definition: aigMffc.c:86
Aig_Obj_t_
Definition: aig.h:69
Counter
static int Counter
Definition: extraBddMisc.c:1877
Aig_NodeMffcSupp
int Aig_NodeMffcSupp(Aig_Man_t *p, Aig_Obj_t *pNode, int LevelMin, Vec_Ptr_t *vSupp)
Definition: aigMffc.c:179
Aig_NodeMffcSupp_rec
void Aig_NodeMffcSupp_rec(Aig_Man_t *p, Aig_Obj_t *pNode, unsigned LevelMin, Vec_Ptr_t *vSupp, int fTopmost, Aig_Obj_t *pObjSkip)
Definition: aigMffc.c:150
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Aig_NodeMffcLabel
int Aig_NodeMffcLabel(Aig_Man_t *p, Aig_Obj_t *pNode, float *pPower)
Definition: aigMffc.c:211
ABC_INFINITY
#define ABC_INFINITY
MACRO DEFINITIONS ///.
Definition: abc_global.h:216
assert
#define assert(ex)
Definition: util_old.h:213
Vec_PtrClear
static void Vec_PtrClear(Vec_Ptr_t *p)
Definition: vecPtr.h:545
Aig_NodeDeref_rec
ABC_NAMESPACE_IMPL_START int Aig_NodeDeref_rec(Aig_Obj_t *pNode, unsigned LevelMin, float *pPower, float *pProbs)
DECLARATIONS ///.
Definition: aigMffc.c:45
Aig_NodeMffcLabelCut
int Aig_NodeMffcLabelCut(Aig_Man_t *p, Aig_Obj_t *pNode, Vec_Ptr_t *vLeaves)
Definition: aigMffc.c:236
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
Aig_ObjIsCi
static int Aig_ObjIsCi(Aig_Obj_t *pObj)
Definition: aig.h:275
Aig_Obj_t_::Id
int Id
Definition: aig.h:85
Aig_Obj_t_::nRefs
unsigned int nRefs
Definition: aig.h:81