ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
acbPush.c
Go to the documentation of this file.
1
20
21#include "acb.h"
22#include "misc/util/utilTruth.h"
23
25
29
33
45void Acb_ObjPushToFanout( Acb_Ntk_t * p, int iObj, int iFaninIndex, int iFanout )
46{
47 word c0, uTruthObjNew = 0, uTruthObj = Acb_ObjTruth( p, iObj ), Gate;
48 word c1, uTruthFanNew = 0, uTruthFan = Acb_ObjTruth( p, iFanout );
49 int DecType = Abc_Tt6CheckOutDec( uTruthObj, iFaninIndex, &uTruthObjNew );
50 int iFanin = Acb_ObjFanin( p, iObj, iFaninIndex );
51 int iFanoutObjIndex = Acb_ObjWhatFanin( p, iFanout, iObj );
52 int iFanoutFaninIndex = Acb_ObjWhatFanin( p, iFanout, iFanin );
53 if ( iFanoutFaninIndex == -1 )
54 iFanoutFaninIndex = Acb_ObjFaninNum(p, iFanout);
55 assert( !Acb_ObjIsCio(p, iObj) );
56 assert( !Acb_ObjIsCio(p, iFanout) );
57 assert( iFanoutFaninIndex >= 0 );
58 assert( iFaninIndex < Acb_ObjFaninNum(p, iObj) );
59 assert( Acb_ObjFanoutNum(p, iObj) == 1 );
60 // compute new function of the fanout
61 c0 = Abc_Tt6Cofactor0( uTruthFan, iFanoutObjIndex );
62 c1 = Abc_Tt6Cofactor1( uTruthFan, iFanoutObjIndex );
63 if ( DecType == 0 ) // F = i * G
64 Gate = s_Truths6[iFanoutFaninIndex] & s_Truths6[iFanoutObjIndex];
65 else if ( DecType == 1 ) // F = ~i * G
66 Gate = ~s_Truths6[iFanoutFaninIndex] & s_Truths6[iFanoutObjIndex];
67 else if ( DecType == 2 ) // F = ~i + G
68 Gate = ~s_Truths6[iFanoutFaninIndex] | s_Truths6[iFanoutObjIndex];
69 else if ( DecType == 3 ) // F = i + G
70 Gate = s_Truths6[iFanoutFaninIndex] | s_Truths6[iFanoutObjIndex];
71 else if ( DecType == 4 ) // F = i # G
72 Gate = s_Truths6[iFanoutFaninIndex] ^ s_Truths6[iFanoutObjIndex];
73 else assert( 0 );
74 uTruthFanNew = (~Gate & c0) | (Gate & c1);
75 // update functions
76 Vec_WrdWriteEntry( &p->vObjTruth, iObj, Abc_Tt6RemoveVar(uTruthObjNew, iFaninIndex) );
77 Vec_WrdWriteEntry( &p->vObjTruth, iFanout, uTruthFanNew );
78 // update fanins
79 Acb_ObjRemoveFaninFanoutOne( p, iObj, iFanin );
80 if ( iFanoutFaninIndex == Acb_ObjFaninNum(p, iFanout) ) // adding new
81 Acb_ObjAddFaninFanoutOne( p, iFanout, iFanin );
82}
83
95void Acb_ObjPushToFanin( Acb_Ntk_t * p, int iObj, int iFaninIndex2, int iFanin )
96{
97 word uTruthObjNew = 0, uTruthObj = Acb_ObjTruth( p, iObj );
98 word uTruthFanNew = 0, uTruthFan = Acb_ObjTruth( p, iFanin );
99 int iFaninIndex = Acb_ObjWhatFanin( p, iObj, iFanin );
100 int DecType = Abc_TtCheckDsdAnd( uTruthObj, iFaninIndex, iFaninIndex2, &uTruthObjNew );
101 int iFanin2 = Acb_ObjFanin( p, iObj, iFaninIndex2 );
102 int iFaninFaninIndex = Acb_ObjWhatFanin( p, iFanin, iFanin2 );
103 if ( iFaninFaninIndex == -1 )
104 iFaninFaninIndex = Acb_ObjFaninNum(p, iFanin);
105 assert( !Acb_ObjIsCio(p, iObj) );
106 assert( !Acb_ObjIsCio(p, iFanin) );
107 assert( iFaninIndex < Acb_ObjFaninNum(p, iObj) );
108 assert( iFaninIndex2 < Acb_ObjFaninNum(p, iObj) );
109 assert( iFaninIndex != iFaninIndex2 );
110 assert( Acb_ObjFanoutNum(p, iFanin) == 1 );
111 // compute new function of the fanout
112 if ( DecType == 0 ) // i * j
113 uTruthFanNew = uTruthFan & s_Truths6[iFaninFaninIndex];
114 else if ( DecType == 1 ) // i * !j
115 uTruthFanNew = ~uTruthFan & s_Truths6[iFaninFaninIndex];
116 else if ( DecType == 2 ) // !i * j
117 uTruthFanNew = uTruthFan & ~s_Truths6[iFaninFaninIndex];
118 else if ( DecType == 3 ) // !i * !j
119 uTruthFanNew = ~uTruthFan & ~s_Truths6[iFaninFaninIndex];
120 else if ( DecType == 4 ) // i # j
121 uTruthFanNew = uTruthFan ^ s_Truths6[iFaninFaninIndex];
122 else assert( 0 );
123 // update functions
124 Vec_WrdWriteEntry( &p->vObjTruth, iObj, Abc_Tt6RemoveVar(uTruthObjNew, iFaninIndex2) );
125 Vec_WrdWriteEntry( &p->vObjTruth, iFanin, uTruthFanNew );
126 // update fanins
127 Acb_ObjRemoveFaninFanoutOne( p, iObj, iFanin2 );
128 if ( iFaninFaninIndex == Acb_ObjFaninNum(p, iFanin) ) // adding new
129 Acb_ObjAddFaninFanoutOne( p, iFanin, iFanin2 );
130}
131
143static inline int Acb_ObjFindNodeFanout( Acb_Ntk_t * p, int iObj )
144{
145 int i, iFanout;
146 Acb_ObjForEachFanout( p, iObj, iFanout, i )
147 if ( !Acb_ObjIsCio(p, iFanout) )
148 return iFanout;
149 return -1;
150}
152{
153 int k, iFanin, * pFanins;
154 word uTruth = Acb_ObjTruth( p, iObj );
155 Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, k )
156 {
157 if ( Abc_Tt6HasVar(uTruth, k) )
158 continue;
159 Acb_ObjDeleteFaninIndex( p, iObj, k );
160 Vec_IntRemove( Vec_WecEntry(&p->vFanouts, iFanin), iObj );
161 Vec_WrdWriteEntry( &p->vObjTruth, iObj, Abc_Tt6RemoveVar(uTruth, k) );
162 return 1;
163 }
164 return 0;
165}
166void Acb_ObjSuppMin( Acb_Ntk_t * p, int iObj )
167{
168 while ( Acb_ObjSuppMin_int(p, iObj) );
169}
170void Acb_ObjRemoveDup( Acb_Ntk_t * p, int iObj, int i, int j )
171{
172 word c00, c11, uTruthNew, uTruth = Acb_ObjTruth( p, iObj );
173 assert( !Acb_ObjIsCio(p, iObj) );
174 assert( Acb_ObjFanin(p, iObj, i) == Acb_ObjFanin(p, iObj, j) );
175 c00 = Abc_Tt6Cofactor0( Abc_Tt6Cofactor0(uTruth, i), j );
176 c11 = Abc_Tt6Cofactor1( Abc_Tt6Cofactor1(uTruth, i), j );
177 uTruthNew = (~s_Truths6[i] & c00) | (s_Truths6[i] & c11);
178 Vec_WrdWriteEntry( &p->vObjTruth, iObj, Abc_Tt6RemoveVar(uTruthNew, j) );
179 Acb_ObjDeleteFaninIndex( p, iObj, j );
180 Vec_IntRemove( Vec_WecEntry(&p->vFanouts, iObj), Acb_ObjFanin(p, iObj, j) );
181 Acb_ObjSuppMin( p, iObj );
182}
184{
185 int i, k, * pFanins = Acb_ObjFanins( p, iObj );
186 for ( i = 0; i < pFanins[0]; i++ )
187 for ( k = i+1; k < pFanins[0]; k++ )
188 {
189 if ( pFanins[1+i] != pFanins[1+k] )
190 continue;
191 Acb_ObjRemoveDup( p, iObj, i, k );
192 return 1;
193 }
194 return 0;
195}
197{
198 assert( !Acb_ObjIsCio(p, iObj) );
199 while ( Acb_ObjRemoveDupFanins_int(p, iObj) );
200}
201void Acb_ObjRemoveConst( Acb_Ntk_t * p, int iObj )
202{
203 int iFanout;
204 word uTruth = Acb_ObjTruth( p, iObj );
205 assert( !Acb_ObjIsCio(p, iObj) );
206 assert( Acb_ObjFaninNum(p, iObj) == 0 );
207 assert( uTruth == 0 || ~uTruth == 0 );
208 while ( (iFanout = Acb_ObjFindNodeFanout(p, iObj)) >= 0 )
209 {
210 int iObjIndex = Acb_ObjWhatFanin( p, iFanout, iObj );
211 word uTruthF = Acb_ObjTruth( p, iFanout );
212 Acb_ObjRemoveFaninFanoutOne( p, iFanout, iObj );
213 uTruthF = (uTruth & 1) ? Abc_Tt6Cofactor1(uTruthF, iObjIndex) : Abc_Tt6Cofactor0(uTruthF, iObjIndex);
214 Vec_WrdWriteEntry( &p->vObjTruth, iFanout, Abc_Tt6RemoveVar(uTruthF, iObjIndex) );
215 Acb_ObjSuppMin( p, iFanout );
216 }
217 if ( Acb_ObjFanoutNum(p, iObj) == 0 )
218 Acb_ObjCleanType( p, iObj );
219}
220void Acb_ObjRemoveBufInv( Acb_Ntk_t * p, int iObj )
221{
222 int iFanout;
223 word uTruth = Acb_ObjTruth( p, iObj );
224 assert( !Acb_ObjIsCio(p, iObj) );
225 assert( Acb_ObjFaninNum(p, iObj) == 1 );
226 assert( uTruth == s_Truths6[0] || ~uTruth == s_Truths6[0] );
227 while ( (iFanout = Acb_ObjFindNodeFanout(p, iObj)) >= 0 )
228 {
229 int iFanin = Acb_ObjFanin( p, iObj, 0 );
230 int iObjIndex = Acb_ObjWhatFanin( p, iFanout, iObj );
231 Acb_ObjPatchFanin( p, iFanout, iObj, iFanin );
232 if ( uTruth & 1 ) // inv
233 {
234 word uTruthF = Acb_ObjTruth( p, iFanout );
235 Vec_WrdWriteEntry( &p->vObjTruth, iFanout, Abc_Tt6Flip(uTruthF, iObjIndex) );
236 }
237 Acb_ObjRemoveDupFanins( p, iFanout );
238 }
239 while ( (uTruth & 1) == 0 && Acb_ObjFanoutNum(p, iObj) > 0 )
240 {
241 int iFanin = Acb_ObjFanin( p, iObj, 0 );
242 int iFanout = Acb_ObjFanout( p, iObj, 0 );
243 assert( Acb_ObjIsCo(p, iFanout) );
244 Acb_ObjPatchFanin( p, iFanout, iObj, iFanin );
245 }
246 if ( Acb_ObjFanoutNum(p, iObj) == 0 )
247 {
248 Acb_ObjRemoveFaninFanout( p, iObj );
249 Acb_ObjRemoveFanins( p, iObj );
250 Acb_ObjCleanType( p, iObj );
251 }
252}
253
265static inline int Acb_ObjFindFaninPushableIndex( Acb_Ntk_t * p, int iObj, int iFanIndex )
266{
267 int k, iFanin, * pFanins;
268 Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, k )
269 if ( k != iFanIndex && Abc_TtCheckDsdAnd(Acb_ObjTruth(p, iObj), k, iFanIndex, NULL) >= 0 )
270 return k;
271 return -1;
272}
273static inline int Acb_ObjFindFanoutPushableIndex( Acb_Ntk_t * p, int iObj )
274{
275 int k, iFanin, * pFanins;
276 Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, k )
277 if ( Abc_Tt6CheckOutDec(Acb_ObjTruth(p, iObj), k, NULL) >= 0 )
278 return k;
279 return -1;
280}
281int Acb_ObjPushToFanins( Acb_Ntk_t * p, int iObj, int nLutSize )
282{
283 int k, k2, iFanin, * pFanins;
284 if ( Acb_ObjFaninNum(p, iObj) < 2 )
285 return 0;
286 Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, k )
287 {
288 if ( Acb_ObjIsCi(p, iFanin) )
289 continue;
290 if ( Acb_ObjFanoutNum(p, iFanin) > 1 )
291 continue;
292 if ( Acb_ObjFaninNum(p, iFanin) == nLutSize )
293 continue;
294 if ( (k2 = Acb_ObjFindFaninPushableIndex(p, iObj, k)) == -1 )
295 continue;
296 //printf( "Object %4d : Pushing fanin %d (%d) into fanin %d.\n", iObj, Acb_ObjFanin(p, iObj, k2), k2, iFanin );
297 Acb_ObjPushToFanin( p, iObj, k2, iFanin );
298 return 1;
299 }
300 if ( Acb_ObjFaninNum(p, iObj) == 2 && Acb_ObjFanoutNum(p, iObj) == 1 )
301 {
302 int iFanout = Acb_ObjFanout( p, iObj, 0 );
303 if ( !Acb_ObjIsCo(p, iFanout) && Acb_ObjFaninNum(p, iFanout) < nLutSize )
304 {
305 k2 = Acb_ObjFindFanoutPushableIndex( p, iObj );
306 //printf( "Object %4d : Pushing fanin %d (%d) into fanout %d.\n", iObj, Acb_ObjFanin(p, iObj, k2), k2, iFanout );
307 Acb_ObjPushToFanout( p, iObj, k2, iFanout );
308 return 1;
309 }
310 }
311 return 0;
312}
313
325void Acb_NtkPushLogic( Acb_Ntk_t * p, int nLutSize, int fVerbose )
326{
327 int n = 0, iObj, nNodes = Acb_NtkNodeNum(p), nPushes = 0;
328 Acb_NtkCreateFanout( p ); // fanout data structure
329 Acb_NtkForEachNodeSupp( p, iObj, 0 )
330 Acb_ObjRemoveConst( p, iObj );
331 Acb_NtkForEachNodeSupp( p, iObj, 1 )
332 Acb_ObjRemoveBufInv( p, iObj );
333 for ( n = 2; n <= nLutSize; n++ )
334 Acb_NtkForEachNodeSupp( p, iObj, n )
335 {
336 while ( Acb_ObjPushToFanins(p, iObj, nLutSize) )
337 nPushes++;
338 if ( Acb_ObjFaninNum(p, iObj) == 1 )
339 Acb_ObjRemoveBufInv( p, iObj );
340 }
341 printf( "Saved %d nodes after %d pushes.\n", nNodes - Acb_NtkNodeNum(p), nPushes );
342}
343
355void Acb_NtkPushLogic2( Acb_Ntk_t * p, int nLutSize, int fVerbose )
356{
357 int iObj;
358 Acb_NtkCreateFanout( p ); // fanout data structure
359 Acb_NtkForEachObj( p, iObj )
360 if ( !Acb_ObjIsCio(p, iObj) )
361 break;
362 Acb_ObjPushToFanout( p, iObj, Acb_ObjFaninNum(p, iObj)-1, Acb_ObjFanout(p, iObj, 0) );
363// Acb_ObjPushToFanin( p, Acb_ObjFanout(p, iObj, 0), Acb_ObjFaninNum(p, iObj)-1, iObj );
364}
365
369
370
372
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
void Acb_ObjRemoveDup(Acb_Ntk_t *p, int iObj, int i, int j)
Definition acbPush.c:170
void Acb_NtkPushLogic2(Acb_Ntk_t *p, int nLutSize, int fVerbose)
Definition acbPush.c:355
ABC_NAMESPACE_IMPL_START void Acb_ObjPushToFanout(Acb_Ntk_t *p, int iObj, int iFaninIndex, int iFanout)
DECLARATIONS ///.
Definition acbPush.c:45
void Acb_ObjRemoveDupFanins(Acb_Ntk_t *p, int iObj)
Definition acbPush.c:196
int Acb_ObjRemoveDupFanins_int(Acb_Ntk_t *p, int iObj)
Definition acbPush.c:183
int Acb_ObjPushToFanins(Acb_Ntk_t *p, int iObj, int nLutSize)
Definition acbPush.c:281
void Acb_ObjRemoveConst(Acb_Ntk_t *p, int iObj)
Definition acbPush.c:201
void Acb_ObjPushToFanin(Acb_Ntk_t *p, int iObj, int iFaninIndex2, int iFanin)
Definition acbPush.c:95
void Acb_ObjRemoveBufInv(Acb_Ntk_t *p, int iObj)
Definition acbPush.c:220
int Acb_ObjSuppMin_int(Acb_Ntk_t *p, int iObj)
Definition acbPush.c:151
void Acb_ObjSuppMin(Acb_Ntk_t *p, int iObj)
Definition acbPush.c:166
void Acb_NtkPushLogic(Acb_Ntk_t *p, int nLutSize, int fVerbose)
Definition acbPush.c:325
struct Acb_Ntk_t_ Acb_Ntk_t
Definition acb.h:47
#define Acb_ObjForEachFanout(p, iObj, iFanout, k)
Definition acb.h:378
#define Acb_NtkForEachNodeSupp(p, i, nSuppSize)
Definition acb.h:364
#define Acb_NtkForEachObj(p, i)
Definition acb.h:358
#define Acb_ObjForEachFaninFast(p, iObj, pFanins, iFanin, k)
Definition acb.h:375
Cube * p
Definition exorList.c:222
unsigned __int64 word
DECLARATIONS ///.
Definition kitPerm.c:36
#define assert(ex)
Definition util_old.h:213