ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
acecCl.c
Go to the documentation of this file.
1
20
21#include "acecInt.h"
22#include "misc/vec/vecWec.h"
23#include "misc/extra/extra.h"
24
26
30
31
32
36
48void Acec_ManDerive_rec( Gia_Man_t * pNew, Gia_Man_t * p, int Node, Vec_Int_t * vMirrors )
49{
50 Gia_Obj_t * pObj;
51 int Obj = Node;
52 if ( Vec_IntEntry(vMirrors, Node) >= 0 )
53 Obj = Abc_Lit2Var( Vec_IntEntry(vMirrors, Node) );
54 pObj = Gia_ManObj( p, Obj );
55 if ( !~pObj->Value )
56 {
57 assert( Gia_ObjIsAnd(pObj) );
58 Acec_ManDerive_rec( pNew, p, Gia_ObjFaninId0(pObj, Obj), vMirrors );
59 Acec_ManDerive_rec( pNew, p, Gia_ObjFaninId1(pObj, Obj), vMirrors );
60 if ( Gia_ObjIsXor(pObj) )
61 pObj->Value = Gia_ManAppendXorReal( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
62 else
63 pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
64 }
65 // set the original node as well
66 if ( Obj != Node )
67 Gia_ManObj(p, Node)->Value = Abc_LitNotCond( pObj->Value, Abc_LitIsCompl(Vec_IntEntry(vMirrors, Node)) );
68}
70{
71 Gia_Man_t * pNew;
72 Gia_Obj_t * pObj;
73 int i;
74 assert( p->pMuxes == NULL );
76 pNew = Gia_ManStart( Gia_ManObjNum(p) );
77 pNew->pName = Abc_UtilStrsav( p->pName );
78 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
79 Gia_ManConst0(p)->Value = 0;
80 Gia_ManHashAlloc( pNew );
81 Gia_ManForEachCi( p, pObj, i )
82 pObj->Value = Gia_ManAppendCi(pNew);
83 Gia_ManForEachCo( p, pObj, i )
84 Acec_ManDerive_rec( pNew, p, Gia_ObjFaninId0p(p, pObj), vMirrors );
85 Gia_ManForEachCo( p, pObj, i )
86 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
87 Gia_ManHashStop( pNew );
88 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
89 return pNew;
90}
91
104{
105 Vec_Int_t * vRootXorSet = Vec_IntAlloc( Gia_ManCoNum(p) );
106 Gia_Obj_t * pObj, * pFan0, * pFan1, * pFan00, * pFan01, * pFan10, * pFan11;
107 int i, fXor0, fXor1, fFirstXor = 0;
108 Gia_ManForEachCoDriver( p, pObj, i )
109 {
110 if ( !Gia_ObjRecognizeExor(pObj, &pFan0, &pFan1) )
111 {
112 if ( fFirstXor )
113 {
114 printf( "XORs do not form a continuous sequence\n" );
115 Vec_IntFreeP( &vRootXorSet );
116 break;
117 }
118 continue;
119 }
120 fFirstXor = 1;
121 fXor0 = Gia_ObjRecognizeExor(Gia_Regular(pFan0), &pFan00, &pFan01);
122 fXor1 = Gia_ObjRecognizeExor(Gia_Regular(pFan1), &pFan10, &pFan11);
123 if ( fXor0 == fXor1 )
124 {
125 printf( "Both inputs of top level XOR have XOR/non-XOR\n" );
126 Vec_IntFreeP( &vRootXorSet );
127 break;
128 }
129 Vec_IntPush( vRootXorSet, Gia_ObjId(p, pObj) );
130 Vec_IntPush( vRootXorSet, fXor1 ? Gia_ObjId(p, Gia_Regular(pFan0)) : Gia_ObjId(p, Gia_Regular(pFan1)) );
131 Vec_IntPush( vRootXorSet, fXor1 ? Gia_ObjId(p, Gia_Regular(pFan10)) : Gia_ObjId(p, Gia_Regular(pFan00)) );
132 Vec_IntPush( vRootXorSet, fXor1 ? Gia_ObjId(p, Gia_Regular(pFan11)) : Gia_ObjId(p, Gia_Regular(pFan01)) );
133 }
134 for ( i = 0; 4*i < Vec_IntSize(vRootXorSet); i++ )
135 {
136 printf( "%2d : ", i );
137 printf( "%4d <- ", Vec_IntEntry(vRootXorSet, 4*i) );
138 printf( "%4d ", Vec_IntEntry(vRootXorSet, 4*i+1) );
139 printf( "%4d ", Vec_IntEntry(vRootXorSet, 4*i+2) );
140 printf( "%4d ", Vec_IntEntry(vRootXorSet, 4*i+3) );
141 printf( "\n" );
142 }
143 return vRootXorSet;
144}
145
157int Acec_DetectLitPolarity( Gia_Man_t * p, int Node, int Leaf )
158{
159 Gia_Obj_t * pNode;
160 int Lit0, Lit1;
161 if ( Node < Leaf )
162 return -1;
163 if ( Node == Leaf )
164 return Abc_Var2Lit(Node, 0);
165 pNode = Gia_ManObj( p, Node );
166 Lit0 = Acec_DetectLitPolarity( p, Gia_ObjFaninId0(pNode, Node), Leaf );
167 Lit1 = Acec_DetectLitPolarity( p, Gia_ObjFaninId1(pNode, Node), Leaf );
168 Lit0 = Lit0 == -1 ? Lit0 : Abc_LitNotCond( Lit0, Gia_ObjFaninC0(pNode) );
169 Lit1 = Lit1 == -1 ? Lit1 : Abc_LitNotCond( Lit1, Gia_ObjFaninC1(pNode) );
170 if ( Lit0 == -1 && Lit1 == -1 )
171 return -1;
172 assert( Lit0 != -1 || Lit1 != -1 );
173 if ( Lit0 != -1 && Lit1 != -1 )
174 {
175 assert( Lit0 == Lit1 );
176 printf( "Problem for leaf %d\n", Leaf );
177 return Lit0;
178 }
179 return Lit0 != -1 ? Lit0 : Lit1;
180}
181
194{
195 if ( Gia_ObjIsTravIdCurrent(p, pObj) )
196 return;
197 Gia_ObjSetTravIdCurrent(p, pObj);
198 if ( pObj->fMark0 )
199 {
200 Vec_IntPush( vSupp, Gia_ObjId(p, pObj) );
201 return;
202 }
203 assert( Gia_ObjIsAnd(pObj) );
204 Acec_DetectComputeSuppOne_rec( p, Gia_ObjFanin0(pObj), vSupp, vNods );
205 Acec_DetectComputeSuppOne_rec( p, Gia_ObjFanin1(pObj), vSupp, vNods );
206 Vec_IntPush( vNods, Gia_ObjId(p, pObj) );
207}
209{
210 Vec_Int_t * vNods = Vec_IntAlloc( 100 );
211 Vec_Int_t * vPols = Vec_IntAlloc( 100 );
212 Vec_Int_t * vSupp = Vec_IntAlloc( 100 ); int i, k, Node, Pol;
213 for ( i = 0; 4*i < Vec_IntSize(vRootXorSet); i++ )
214 {
215 Gia_ManObj( p, Vec_IntEntry(vRootXorSet, 4*i+1) )->fMark0 = 1;
216 Gia_ManObj( p, Vec_IntEntry(vRootXorSet, 4*i+2) )->fMark0 = 1;
217 Gia_ManObj( p, Vec_IntEntry(vRootXorSet, 4*i+3) )->fMark0 = 1;
218 }
219 for ( i = 1; 4*i < Vec_IntSize(vRootXorSet); i++ )
220 {
221 Vec_IntClear( vSupp );
223
224 Gia_ManObj( p, Vec_IntEntry(vRootXorSet, 4*i+1) )->fMark0 = 0;
225 Acec_DetectComputeSuppOne_rec( p, Gia_ManObj( p, Vec_IntEntry(vRootXorSet, 4*i+1) ), vSupp, vNods );
226 Gia_ManObj( p, Vec_IntEntry(vRootXorSet, 4*i+1) )->fMark0 = 1;
227
228 Vec_IntSort( vSupp, 0 );
229
230 printf( "Out %4d : %4d \n", i, Vec_IntEntry(vRootXorSet, 4*i+1) );
231 Vec_IntPrint( vSupp );
232
233 printf( "Cone:\n" );
234 Vec_IntForEachEntry( vNods, Node, k )
235 Gia_ObjPrint( p, Gia_ManObj(p, Node) );
236
237
238 Vec_IntClear( vPols );
239 Vec_IntForEachEntry( vSupp, Node, k )
240 Vec_IntPush( vPols, Acec_DetectLitPolarity(p, Vec_IntEntry(vRootXorSet, 4*i+1), Node) );
241
242 Vec_IntForEachEntryTwo( vSupp, vPols, Node, Pol, k )
243 printf( "%d(%d) ", Node, Abc_LitIsCompl(Pol) );
244
245 printf( "\n" );
246
247 Vec_IntPrint( vSupp );
248 }
249 for ( i = 0; 4*i < Vec_IntSize(vRootXorSet); i++ )
250 {
251 Gia_ManObj( p, Vec_IntEntry(vRootXorSet, 4*i+1) )->fMark0 = 0;
252 Gia_ManObj( p, Vec_IntEntry(vRootXorSet, 4*i+2) )->fMark0 = 0;
253 Gia_ManObj( p, Vec_IntEntry(vRootXorSet, 4*i+3) )->fMark0 = 0;
254 }
255 Vec_IntFree( vSupp );
256 Vec_IntFree( vPols );
257 Vec_IntFree( vNods );
258}
259
272{
273 Gia_Man_t * pNew;
274 int i, k, iOr1, iAnd1, iAnd2, pLits[3]; // carry, in1, in2
275 Vec_Int_t * vMirrors = Vec_IntStart( Gia_ManObjNum(p) );
276 for ( i = 0; 4*i < Vec_IntSize(vRootXorSet); i++ )
277 {
278 pLits[0] = Acec_DetectLitPolarity( p, Vec_IntEntry(vRootXorSet, 4*i), Vec_IntEntry(vRootXorSet, 4*i+1) );
279 // get polarity of two new ones
280 for ( k = 1; k < 3; k++ )
281 pLits[k] = Acec_DetectLitPolarity( p, Vec_IntEntry(vRootXorSet, 4*i), Vec_IntEntry(vRootXorSet, 4*i+k+1) );
282 // create the gate
283 iOr1 = Gia_ManAppendOr( p, pLits[1], pLits[2] );
284 iAnd1 = Gia_ManAppendAnd( p, pLits[0], iOr1 );
285 iAnd2 = Gia_ManAppendAnd( p, pLits[1], pLits[2] );
286 pLits[0] = Gia_ManAppendOr( p, iAnd1, iAnd2 );
287 Vec_IntWriteEntry( vMirrors, Vec_IntEntry(vRootXorSet, 4*i+1), pLits[0] );
288 }
289 // remap the AIG using map
290 pNew = Acec_ManDerive( p, vMirrors );
291 Vec_IntFree( vMirrors );
292 return pNew;
293}
294
295
308{
309 abctime clk = Abc_Clock();
310 Gia_Man_t * pNew;
311 Vec_Int_t * vRootXorSet;
312// Vec_Int_t * vXors, * vAdds = Ree_ManComputeCuts( p, &vXors, 0 );
313
314 //Ree_ManPrintAdders( vAdds, 1 );
315// printf( "Detected %d full-adders and %d half-adders. Found %d XOR-cuts. ", Ree_ManCountFadds(vAdds), Vec_IntSize(vAdds)/6-Ree_ManCountFadds(vAdds), Vec_IntSize(vXors)/4 );
316// Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
317
318 clk = Abc_Clock();
319 vRootXorSet = Acec_CollectXorTops( p );
320 if ( vRootXorSet )
321 {
322 Acec_DetectComputeSupports( p, vRootXorSet );
323
324 pNew = Acec_DetectXorBuildNew( p, vRootXorSet );
325 Vec_IntFree( vRootXorSet );
326 }
327 else
328 pNew = Gia_ManDup( p );
329
330 printf( "Detected %d top XORs. ", Vec_IntSize(vRootXorSet)/4 );
331 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
332
333// Vec_IntFree( vXors );
334// Vec_IntFree( vAdds );
335 return pNew;
336}
337
350{
351 Vec_Int_t * vRes = Vec_IntAlloc( Gia_ManCoNum(p) + 1 );
352 Vec_Int_t * vLevel;
353 int i, k, iStart, iLit, Driver, Count = 0;
354 // determine how much to shift
355 Driver = Gia_ObjFaninId0p( p, Gia_ManCo(p, 0) );
356 Vec_WecForEachLevel( pBox->vRootLits, vLevel, iStart )
357 if ( Abc_Lit2Var(Vec_IntEntry(vLevel,0)) == Driver )
358 break;
359 assert( iStart < Gia_ManCoNum(p) );
360 //Vec_WecPrintLits( pBox->vRootLits );
361 Vec_WecForEachLevelStart( pBox->vRootLits, vLevel, i, iStart )
362 {
363 int In[3] = {0}, Out[2];
364 assert( Vec_IntSize(vLevel) > 0 );
365 assert( Vec_IntSize(vLevel) <= 3 );
366 if ( Vec_IntSize(vLevel) == 1 )
367 {
368 Vec_IntPush( vRes, Vec_IntEntry(vLevel, 0) );
369 continue;
370 }
371 Vec_IntForEachEntry( vLevel, iLit, k )
372 In[k] = iLit;
373 Acec_InsertFadd( p, In, Out );
374 Vec_IntPush( vRes, Out[0] );
375 if ( i+1 < Vec_WecSize(pBox->vRootLits) )
376 Vec_IntPush( Vec_WecEntry(pBox->vRootLits, i+1), Out[1] );
377 else
378 Vec_IntPush( Vec_WecPushLevel(pBox->vRootLits), Out[1] );
379 Count++;
380 }
381 assert( Vec_IntSize(vRes) >= Gia_ManCoNum(p) );
382 Vec_IntShrink( vRes, Gia_ManCoNum(p) );
383 printf( "Added %d adders for replace CLAs. ", Count );
384 return vRes;
385}
387{
388 Gia_Man_t * pNew, * pTemp;
389 Gia_Obj_t * pObj; int i;
390 assert( Gia_ManCoNum(p) == Vec_IntSize(vRes) );
391 // create new manager
392 pNew = Gia_ManStart( Gia_ManObjNum(p) );
393 pNew->pName = Abc_UtilStrsav( p->pName );
394 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
396 Gia_ManConst0(p)->Value = 0;
397 Gia_ManForEachCi( p, pObj, i )
398 pObj->Value = Gia_ManAppendCi(pNew);
399 Gia_ManForEachAnd( p, pObj, i )
400 pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
401 Gia_ManForEachCo( p, pObj, i )
402 {
403 int iLit = Vec_IntEntry( vRes, i );
404 Gia_Obj_t * pRepr = Gia_ManObj( p, Abc_Lit2Var(iLit) );
405 pObj->Value = Gia_ManAppendCo( pNew, pRepr->Value );
406 }
407 // set correct phase
409 Gia_ManSetPhase( pNew );
410 Gia_ManForEachCo( pNew, pObj, i )
411 if ( Gia_ObjPhase(pObj) != Gia_ObjPhase(Gia_ManCo(p, i)) )
412 Gia_ObjFlipFaninC0( pObj );
413 // remove dangling nodes
414 pNew = Gia_ManCleanup( pTemp = pNew );
415 Gia_ManStop( pTemp );
416 return pNew;
417}
418Gia_Man_t * Acec_ManDecla( Gia_Man_t * pGia, int fBooth, int fVerbose )
419{
420 abctime clk = Abc_Clock();
421 Gia_Man_t * pNew = NULL;
422 Vec_Bit_t * vIgnore = fBooth ? Acec_BoothFindPPG(pGia) : NULL;
423 Acec_Box_t * pBox = Acec_DeriveBox( pGia, vIgnore, 0, 0, fVerbose );
424 Vec_Int_t * vResult;
425 Vec_BitFreeP( &vIgnore );
426 if ( pBox == NULL ) // cannot match
427 {
428 printf( "Cannot find arithmetic boxes.\n" );
429 return Gia_ManDup( pGia );
430 }
431 vResult = Acec_RewriteTop( pGia, pBox );
432 Acec_BoxFreeP( &pBox );
433 pNew = Acec_RewriteReplace( pGia, vResult );
434 Vec_IntFree( vResult );
435 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
436 return pNew;
437}
438
442
443
445
ABC_INT64_T abctime
Definition abc_global.h:332
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
Gia_Man_t * Acec_ManDerive(Gia_Man_t *p, Vec_Int_t *vMirrors)
Definition acecCl.c:69
void Acec_DetectComputeSuppOne_rec(Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vSupp, Vec_Int_t *vNods)
Definition acecCl.c:193
Gia_Man_t * Acec_DetectAdditional(Gia_Man_t *p, int fVerbose)
Definition acecCl.c:307
int Acec_DetectLitPolarity(Gia_Man_t *p, int Node, int Leaf)
Definition acecCl.c:157
Gia_Man_t * Acec_DetectXorBuildNew(Gia_Man_t *p, Vec_Int_t *vRootXorSet)
Definition acecCl.c:271
ABC_NAMESPACE_IMPL_START void Acec_ManDerive_rec(Gia_Man_t *pNew, Gia_Man_t *p, int Node, Vec_Int_t *vMirrors)
DECLARATIONS ///.
Definition acecCl.c:48
Gia_Man_t * Acec_RewriteReplace(Gia_Man_t *p, Vec_Int_t *vRes)
Definition acecCl.c:386
void Acec_DetectComputeSupports(Gia_Man_t *p, Vec_Int_t *vRootXorSet)
Definition acecCl.c:208
Vec_Int_t * Acec_CollectXorTops(Gia_Man_t *p)
Definition acecCl.c:103
Vec_Int_t * Acec_RewriteTop(Gia_Man_t *p, Acec_Box_t *pBox)
Definition acecCl.c:349
Gia_Man_t * Acec_ManDecla(Gia_Man_t *pGia, int fBooth, int fVerbose)
MACRO DEFINITIONS ///.
Definition acecCl.c:418
void Acec_InsertFadd(Gia_Man_t *pNew, int In[3], int Out[2])
Definition acecNorm.c:53
Acec_Box_t * Acec_DeriveBox(Gia_Man_t *p, Vec_Bit_t *vIgnore, int fFilterIn, int fFilterOut, int fVerbose)
Definition acecTree.c:754
Vec_Bit_t * Acec_BoothFindPPG(Gia_Man_t *p)
Definition acecMult.c:656
typedefABC_NAMESPACE_HEADER_START struct Acec_Box_t_ Acec_Box_t
INCLUDES ///.
Definition acecInt.h:40
void Acec_BoxFreeP(Acec_Box_t **ppBox)
Definition acecTree.c:54
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
Cube * p
Definition exorList.c:222
void Gia_ManStop(Gia_Man_t *p)
Definition giaMan.c:82
Gia_Man_t * Gia_ManDup(Gia_Man_t *p)
Definition giaDup.c:720
#define Gia_ManForEachAnd(p, pObj, i)
Definition gia.h:1214
void Gia_ManSetRegNum(Gia_Man_t *p, int nRegs)
Definition giaMan.c:764
void Gia_ManHashAlloc(Gia_Man_t *p)
Definition giaHash.c:105
Gia_Man_t * Gia_ManStart(int nObjsMax)
FUNCTION DEFINITIONS ///.
Definition giaMan.c:57
struct Gia_Obj_t_ Gia_Obj_t
Definition gia.h:76
void Gia_ObjPrint(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition giaUtil.c:1456
void Gia_ManFillValue(Gia_Man_t *p)
Definition giaUtil.c:369
struct Gia_Man_t_ Gia_Man_t
Definition gia.h:96
Gia_Man_t * Gia_ManCleanup(Gia_Man_t *p)
Definition giaScl.c:84
int Gia_ObjRecognizeExor(Gia_Obj_t *pObj, Gia_Obj_t **ppFan0, Gia_Obj_t **ppFan1)
Definition giaUtil.c:1018
void Gia_ManIncrementTravId(Gia_Man_t *p)
Definition giaUtil.c:190
#define Gia_ManForEachCo(p, pObj, i)
Definition gia.h:1236
#define Gia_ManForEachCi(p, pObj, i)
Definition gia.h:1228
void Gia_ManSetPhase(Gia_Man_t *p)
Definition giaUtil.c:420
void Gia_ManHashStop(Gia_Man_t *p)
Definition giaHash.c:149
#define Gia_ManForEachCoDriver(p, pObj, i)
Definition gia.h:1244
char * pSpec
Definition gia.h:100
char * pName
Definition gia.h:99
unsigned Value
Definition gia.h:89
unsigned fMark0
Definition gia.h:81
#define assert(ex)
Definition util_old.h:213
typedefABC_NAMESPACE_HEADER_START struct Vec_Bit_t_ Vec_Bit_t
INCLUDES ///.
Definition vecBit.h:42
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
#define Vec_IntForEachEntryTwo(vVec1, vVec2, Entry1, Entry2, i)
Definition vecInt.h:66
#define Vec_WecForEachLevel(vGlob, vVec, i)
MACRO DEFINITIONS ///.
Definition vecWec.h:55
#define Vec_WecForEachLevelStart(vGlob, vVec, i, LevelStart)
Definition vecWec.h:59