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 ***********************************************************************/
Aig_NodeDeref_rec(Aig_Obj_t * pNode,unsigned LevelMin,float * pPower,float * pProbs)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 ***********************************************************************/
Aig_NodeRef_rec(Aig_Obj_t * pNode,unsigned LevelMin)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 ***********************************************************************/
Aig_NodeRefLabel_rec(Aig_Man_t * p,Aig_Obj_t * pNode,unsigned LevelMin)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 ***********************************************************************/
Aig_NodeMffcSupp_rec(Aig_Man_t * p,Aig_Obj_t * pNode,unsigned LevelMin,Vec_Ptr_t * vSupp,int fTopmost,Aig_Obj_t * pObjSkip)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 ***********************************************************************/
Aig_NodeMffcSupp(Aig_Man_t * p,Aig_Obj_t * pNode,int LevelMin,Vec_Ptr_t * vSupp)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 ***********************************************************************/
Aig_NodeMffcLabel(Aig_Man_t * p,Aig_Obj_t * pNode,float * pPower)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 ***********************************************************************/
Aig_NodeMffcLabelCut(Aig_Man_t * p,Aig_Obj_t * pNode,Vec_Ptr_t * vLeaves)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 ***********************************************************************/
Aig_NodeMffcExtendCut(Aig_Man_t * p,Aig_Obj_t * pNode,Vec_Ptr_t * vLeaves,Vec_Ptr_t * vResult)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
317