ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
acec.h File Reference
This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes

struct  Acec_ParCec_t_
 

Typedefs

typedef typedefABC_NAMESPACE_HEADER_START struct Acec_ParCec_t_ Acec_ParCec_t
 INCLUDES ///.
 

Functions

Gia_Man_tAcec_ManDecla (Gia_Man_t *pGia, int fBooth, int fVerbose)
 MACRO DEFINITIONS ///.
 
void Acec_ManCecSetDefaultParams (Acec_ParCec_t *p)
 FUNCTION DEFINITIONS ///.
 
int Acec_Solve (Gia_Man_t *pGia0, Gia_Man_t *pGia1, Acec_ParCec_t *pPars)
 
Vec_Int_tGia_ManDetectFullAdders (Gia_Man_t *p, int fVerbose, Vec_Int_t **vCutsXor2)
 
Vec_Int_tGia_ManDetectHalfAdders (Gia_Man_t *p, int fVerbose)
 FUNCTION DEFINITIONS ///.
 
Vec_Int_tGia_PolynReorder (Gia_Man_t *pGia, int fVerbose, int fVeryVerbose)
 
Vec_Int_tGia_PolynFindOrder (Gia_Man_t *pGia, Vec_Int_t *vFadds, Vec_Int_t *vHadds, int fVerbose, int fVeryVerbose)
 DECLARATIONS ///.
 
void Gia_PolynBuild (Gia_Man_t *pGia, Vec_Int_t *vOrder, int fSigned, int fVerbose, int fVeryVerbose)
 
Vec_Int_tRee_ManComputeCuts (Gia_Man_t *p, Vec_Int_t **pvXors, int fVerbose)
 
int Ree_ManCountFadds (Vec_Int_t *vAdds)
 
void Ree_ManPrintAdders (Vec_Int_t *vAdds, int fVerbose)
 
Gia_Man_tAcec_Normalize (Gia_Man_t *pGia, int fBooth, int fVerbose)
 

Typedef Documentation

◆ Acec_ParCec_t

typedef typedefABC_NAMESPACE_HEADER_START struct Acec_ParCec_t_ Acec_ParCec_t

INCLUDES ///.

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

FileName [acec.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [CEC for arithmetic circuits.]

Synopsis [External declarations.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id
acec.h,v 1.00 2005/06/20 00:00:00 alanmi Exp

] PARAMETERS /// BASIC TYPES ///

Definition at line 42 of file acec.h.

Function Documentation

◆ Acec_ManCecSetDefaultParams()

void Acec_ManCecSetDefaultParams ( Acec_ParCec_t * p)
extern

FUNCTION DEFINITIONS ///.

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

Synopsis [This procedure sets default parameters.]

Description []

SideEffects []

SeeAlso []

Definition at line 50 of file acecCore.c.

51{
52 memset( p, 0, sizeof(Acec_ParCec_t) );
53 p->nBTLimit = 1000; // conflict limit at a node
54 p->TimeLimit = 0; // the runtime limit in seconds
55 p->fMiter = 0; // input circuit is a miter
56 p->fDualOutput = 0; // dual-output miter
57 p->fTwoOutput = 0; // two-output miter
58 p->fSilent = 0; // print no messages
59 p->fVeryVerbose = 0; // verbose stats
60 p->fVerbose = 0; // verbose stats
61 p->iOutFail = -1; // the number of failed output
62}
typedefABC_NAMESPACE_HEADER_START struct Acec_ParCec_t_ Acec_ParCec_t
INCLUDES ///.
Definition acec.h:42
Cube * p
Definition exorList.c:222
char * memset()
Here is the call graph for this function:

◆ Acec_ManDecla()

Gia_Man_t * Acec_ManDecla ( Gia_Man_t * pGia,
int fBooth,
int fVerbose )
extern

MACRO DEFINITIONS ///.

ITERATORS /// FUNCTION DECLARATIONS ///

Definition at line 418 of file acecCl.c.

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}
ABC_INT64_T abctime
Definition abc_global.h:332
Gia_Man_t * Acec_RewriteReplace(Gia_Man_t *p, Vec_Int_t *vRes)
Definition acecCl.c:386
Vec_Int_t * Acec_RewriteTop(Gia_Man_t *p, Acec_Box_t *pBox)
Definition acecCl.c:349
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
Gia_Man_t * Gia_ManDup(Gia_Man_t *p)
Definition giaDup.c:720
struct Gia_Man_t_ Gia_Man_t
Definition gia.h:96
typedefABC_NAMESPACE_HEADER_START struct Vec_Bit_t_ Vec_Bit_t
INCLUDES ///.
Definition vecBit.h:42
Here is the call graph for this function:

◆ Acec_Normalize()

Gia_Man_t * Acec_Normalize ( Gia_Man_t * pGia,
int fBooth,
int fVerbose )
extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 210 of file acecNorm.c.

211{
212 Vec_Bit_t * vIgnore = fBooth ? Acec_BoothFindPPG( pGia ) : NULL;
213 Acec_Box_t * pBox = Acec_DeriveBox( pGia, vIgnore, 0, 0, fVerbose );
214 Gia_Man_t * pNew = Acec_InsertBox( pBox, 1 );
215 Acec_BoxFreeP( &pBox );
216 Vec_BitFreeP( &vIgnore );
217 return pNew;
218}
Gia_Man_t * Acec_InsertBox(Acec_Box_t *pBox, int fAll)
Definition acecNorm.c:156
Here is the call graph for this function:

◆ Acec_Solve()

int Acec_Solve ( Gia_Man_t * pGia0,
Gia_Man_t * pGia1,
Acec_ParCec_t * pPars )
extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 488 of file acecCore.c.

489{
490 int status = -1;
491 abctime clk = Abc_Clock();
492 Gia_Man_t * pMiter;
493 Gia_Man_t * pGia0n = pGia0, * pGia1n = pGia1;
494 Cec_ParCec_t ParsCec, * pCecPars = &ParsCec;
495// Vec_Bit_t * vIgnore0 = pPars->fBooth ? Acec_BoothFindPPG(pGia0) : NULL;
496// Vec_Bit_t * vIgnore1 = pPars->fBooth ? Acec_BoothFindPPG(pGia1) : NULL;
497// Acec_Box_t * pBox0 = Acec_DeriveBox( pGia0, vIgnore0, 0, 0, pPars->fVerbose );
498// Acec_Box_t * pBox1 = Acec_DeriveBox( pGia1, vIgnore1, 0, 0, pPars->fVerbose );
499// Vec_BitFreeP( &vIgnore0 );
500// Vec_BitFreeP( &vIgnore1 );
501 Acec_Box_t * pBox0 = Acec_ProduceBox( pGia0, pPars->fVerbose );
502 Acec_Box_t * pBox1 = Acec_ProduceBox( pGia1, pPars->fVerbose );
503 if ( pBox0 == NULL || pBox1 == NULL ) // cannot match
504 printf( "Cannot find arithmetic boxes in both LHS and RHS. Trying regular CEC.\n" );
505 else if ( !Acec_MatchBoxes( pBox0, pBox1 ) ) // cannot find matching
506 printf( "Cannot match arithmetic boxes in LHS and RHS. Trying regular CEC.\n" );
507 else
508 {
509 pGia0n = Acec_InsertBox( pBox0, 0 );
510 pGia1n = Acec_InsertBox( pBox1, 0 );
511 printf( "Matching of adder trees in LHS and RHS succeeded. " );
512 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
513 // remove the last output
514 Gia_ManPatchCoDriver( pGia0n, Gia_ManCoNum(pGia0n)-1, 0 );
515 Gia_ManPatchCoDriver( pGia1n, Gia_ManCoNum(pGia1n)-1, 0 );
516
517 Gia_ManPatchCoDriver( pGia0n, Gia_ManCoNum(pGia0n)-2, 0 );
518 Gia_ManPatchCoDriver( pGia1n, Gia_ManCoNum(pGia1n)-2, 0 );
519 }
520 // solve regular CEC problem
521 Cec_ManCecSetDefaultParams( pCecPars );
522 pCecPars->nBTLimit = pPars->nBTLimit;
523 pMiter = Gia_ManMiter( pGia0n, pGia1n, 0, 1, 0, 0, pPars->fVerbose );
524 if ( pMiter )
525 {
526 int fDumpMiter = 0;
527 if ( fDumpMiter )
528 {
529 Abc_Print( 0, "The verification miter is written into file \"%s\".\n", "acec_miter.aig" );
530 Gia_AigerWrite( pMiter, "acec_miter.aig", 0, 0, 0 );
531 }
532 status = Cec_ManVerify( pMiter, pCecPars );
533 ABC_SWAP( Abc_Cex_t *, pGia0->pCexComb, pMiter->pCexComb );
534 Gia_ManStop( pMiter );
535 }
536 else
537 printf( "Miter computation has failed.\n" );
538 if ( pGia0n != pGia0 )
539 Gia_ManStop( pGia0n );
540 if ( pGia1n != pGia1 )
541 Gia_ManStop( pGia1n );
542 Acec_BoxFreeP( &pBox0 );
543 Acec_BoxFreeP( &pBox1 );
544 return status;
545}
#define ABC_SWAP(Type, a, b)
Definition abc_global.h:253
int Acec_MatchBoxes(Acec_Box_t *pBox0, Acec_Box_t *pBox1)
Definition acecCore.c:394
Gia_Man_t * Acec_InsertBox(Acec_Box_t *pBox, int fAll)
Definition acecNorm.c:156
Acec_Box_t * Acec_ProduceBox(Gia_Man_t *p, int fVerbose)
Definition acecXor.c:375
void Cec_ManCecSetDefaultParams(Cec_ParCec_t *p)
Definition cecCore.c:159
struct Cec_ParCec_t_ Cec_ParCec_t
Definition cec.h:129
int Cec_ManVerify(Gia_Man_t *p, Cec_ParCec_t *pPars)
MACRO DEFINITIONS ///.
Definition cecCec.c:326
void Gia_ManStop(Gia_Man_t *p)
Definition giaMan.c:82
Gia_Man_t * Gia_ManMiter(Gia_Man_t *pAig0, Gia_Man_t *pAig1, int nInsDup, int fDualOut, int fSeq, int fImplic, int fVerbose)
Definition giaDup.c:2983
void Gia_AigerWrite(Gia_Man_t *p, char *pFileName, int fWriteSymbols, int fCompact, int fWriteNewLine)
Definition giaAiger.c:1595
int nBTLimit
Definition cec.h:132
Abc_Cex_t * pCexComb
Definition gia.h:149
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition utilCex.h:39
Here is the call graph for this function:

◆ Gia_ManDetectFullAdders()

Vec_Int_t * Gia_ManDetectFullAdders ( Gia_Man_t * p,
int fVerbose,
Vec_Int_t ** vCutsXor2 )
extern

Definition at line 442 of file acecFadds.c.

443{
444 Vec_Int_t * vCutsXor, * vCutsMaj, * vFadds;
445 Dtc_ManComputeCuts( p, pvCutsXor2, &vCutsXor, &vCutsMaj, fVerbose );
446 qsort( Vec_IntArray(vCutsXor), (size_t)(Vec_IntSize(vCutsXor)/4), 16, (int (*)(const void *, const void *))Dtc_ManCompare );
447 qsort( Vec_IntArray(vCutsMaj), (size_t)(Vec_IntSize(vCutsMaj)/4), 16, (int (*)(const void *, const void *))Dtc_ManCompare );
448 vFadds = Dtc_ManFindCommonCuts( p, vCutsXor, vCutsMaj );
449 qsort( Vec_IntArray(vFadds), (size_t)(Vec_IntSize(vFadds)/5), 20, (int (*)(const void *, const void *))Dtc_ManCompare2 );
450 if ( fVerbose )
451 printf( "XOR3 cuts = %d. MAJ cuts = %d. Full-adders = %d.\n", Vec_IntSize(vCutsXor)/4, Vec_IntSize(vCutsMaj)/4, Vec_IntSize(vFadds)/5 );
452 if ( fVerbose )
453 Dtc_ManPrintFadds( vFadds );
454 Vec_IntFree( vCutsXor );
455 Vec_IntFree( vCutsMaj );
456 return vFadds;
457}
void Dtc_ManComputeCuts(Gia_Man_t *p, Vec_Int_t **pvCutsXor2, Vec_Int_t **pvCutsXor, Vec_Int_t **pvCutsMaj, int fVerbose)
Definition acecFadds.c:335
int Dtc_ManCompare(int *pCut0, int *pCut1)
Definition acecFadds.c:425
Vec_Int_t * Dtc_ManFindCommonCuts(Gia_Man_t *p, Vec_Int_t *vCutsXor, Vec_Int_t *vCutsMaj)
Definition acecFadds.c:374
void Dtc_ManPrintFadds(Vec_Int_t *vFadds)
Definition acecFadds.c:404
int Dtc_ManCompare2(int *pCut0, int *pCut1)
Definition acecFadds.c:435
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Gia_ManDetectHalfAdders()

Vec_Int_t * Gia_ManDetectHalfAdders ( Gia_Man_t * p,
int fVerbose )
extern

FUNCTION DEFINITIONS ///.

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

Synopsis [Detecting HADDs in the AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 50 of file acecFadds.c.

51{
52 Vec_Int_t * vHadds = Vec_IntAlloc( 1000 );
53 Gia_Obj_t * pObj, * pFan0, * pFan1;
54 int i, iLit, iFan0, iFan1, fComplDiff, Count, Counts[5] = {0};
56 if ( p->nXors )
57 {
58 Gia_ManForEachAnd( p, pObj, i )
59 {
60 if ( !Gia_ObjIsXor(pObj) )
61 continue;
62 Count = 0;
63 iFan0 = Gia_ObjFaninId0(pObj, i);
64 iFan1 = Gia_ObjFaninId1(pObj, i);
65 if ( (iLit = Gia_ManHashLookupInt(p, Abc_Var2Lit(iFan0, 0), Abc_Var2Lit(iFan1, 0))) )
66 Vec_IntPushTwo( vHadds, i, Abc_Lit2Var(iLit) ), Count++;
67 if ( (iLit = Gia_ManHashLookupInt(p, Abc_Var2Lit(iFan0, 1), Abc_Var2Lit(iFan1, 1))) )
68 Vec_IntPushTwo( vHadds, i, Abc_Lit2Var(iLit) ), Count++;
69 if ( (iLit = Gia_ManHashLookupInt(p, Abc_Var2Lit(iFan0, 0), Abc_Var2Lit(iFan1, 1))) )
70 Vec_IntPushTwo( vHadds, i, Abc_Lit2Var(iLit) ), Count++;
71 if ( (iLit = Gia_ManHashLookupInt(p, Abc_Var2Lit(iFan0, 1), Abc_Var2Lit(iFan1, 0))) )
72 Vec_IntPushTwo( vHadds, i, Abc_Lit2Var(iLit) ), Count++;
73 Counts[Count]++;
74 }
75 }
76 else
77 {
78 ABC_FREE( p->pRefs );
80 Gia_ManForEachAnd( p, pObj, i )
81 {
82 if ( !Gia_ObjRecognizeExor(pObj, &pFan0, &pFan1) )
83 continue;
84 Count = 0;
85 if ( Gia_ObjRefNumId(p, Gia_ObjFaninId0(pObj, i)) > 1 )
86 Vec_IntPushTwo( vHadds, i, Gia_ObjFaninId0(pObj, i) ), Count++;
87 if ( Gia_ObjRefNumId(p, Gia_ObjFaninId1(pObj, i)) > 1 )
88 Vec_IntPushTwo( vHadds, i, Gia_ObjFaninId1(pObj, i) ), Count++;
89 iFan0 = Gia_ObjId( p, pFan0 );
90 iFan1 = Gia_ObjId( p, pFan1 );
91 fComplDiff = (Gia_ObjFaninC0(Gia_ObjFanin0(pObj)) ^ Gia_ObjFaninC1(Gia_ObjFanin0(pObj)));
92 assert( fComplDiff == (Gia_ObjFaninC0(Gia_ObjFanin1(pObj)) ^ Gia_ObjFaninC1(Gia_ObjFanin1(pObj))) );
93 if ( fComplDiff )
94 {
95 if ( (iLit = Gia_ManHashLookupInt(p, Abc_Var2Lit(iFan0, 0), Abc_Var2Lit(iFan1, 0))) )
96 Vec_IntPushTwo( vHadds, i, Abc_Lit2Var(iLit) ), Count++;
97 if ( (iLit = Gia_ManHashLookupInt(p, Abc_Var2Lit(iFan0, 1), Abc_Var2Lit(iFan1, 1))) )
98 Vec_IntPushTwo( vHadds, i, Abc_Lit2Var(iLit) ), Count++;
99 }
100 else
101 {
102 if ( (iLit = Gia_ManHashLookupInt(p, Abc_Var2Lit(iFan0, 0), Abc_Var2Lit(iFan1, 1))) )
103 Vec_IntPushTwo( vHadds, i, Abc_Lit2Var(iLit) ), Count++;
104 if ( (iLit = Gia_ManHashLookupInt(p, Abc_Var2Lit(iFan0, 1), Abc_Var2Lit(iFan1, 0))) )
105 Vec_IntPushTwo( vHadds, i, Abc_Lit2Var(iLit) ), Count++;
106 }
107 Counts[Count]++;
108 }
109 ABC_FREE( p->pRefs );
110 }
112 if ( fVerbose )
113 {
114 int iXor, iAnd;
115 printf( "Found %d half-adders with XOR gates: ", Vec_IntSize(vHadds)/2 );
116 for ( i = 0; i <= 4; i++ )
117 printf( "%d=%d ", i, Counts[i] );
118 printf( "\n" );
119
120 Vec_IntForEachEntryDouble( vHadds, iXor, iAnd, i )
121 {
122 pObj = Gia_ManObj( p, iXor );
123 printf( "%3d : %5d %5d -> %5d %5d\n", i, Gia_ObjFaninId0(pObj, iXor), Gia_ObjFaninId1(pObj, iXor), iXor, iAnd );
124 }
125 }
126 return vHadds;
127}
#define ABC_FREE(obj)
Definition abc_global.h:267
void Gia_ManHashStart(Gia_Man_t *p)
Definition giaHash.c:125
#define Gia_ManForEachAnd(p, pObj, i)
Definition gia.h:1214
struct Gia_Obj_t_ Gia_Obj_t
Definition gia.h:76
int Gia_ObjRecognizeExor(Gia_Obj_t *pObj, Gia_Obj_t **ppFan0, Gia_Obj_t **ppFan1)
Definition giaUtil.c:1018
void Gia_ManCreateRefs(Gia_Man_t *p)
Definition giaUtil.c:779
int Gia_ManHashLookupInt(Gia_Man_t *p, int iLit0, int iLit1)
Definition giaHash.c:81
void Gia_ManHashStop(Gia_Man_t *p)
Definition giaHash.c:149
#define assert(ex)
Definition util_old.h:213
#define Vec_IntForEachEntryDouble(vVec, Entry1, Entry2, i)
Definition vecInt.h:72
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Gia_PolynBuild()

void Gia_PolynBuild ( Gia_Man_t * pGia,
Vec_Int_t * vOrder,
int fSigned,
int fVerbose,
int fVeryVerbose )
extern

Definition at line 340 of file acecPolyn.c.

341{
342 abctime clk = Abc_Clock();//, clk2 = 0;
343 Gia_Obj_t * pObj;
344 Vec_Bit_t * vPres = Vec_BitStart( Gia_ManObjNum(pGia) );
345 int i, iMono, iDriver, LevPrev, LevCur, Iter, Line = 0;
346 Pln_Man_t * p = Pln_ManAlloc( pGia, vOrder );
347 Gia_ManForEachCoReverse( pGia, pObj, i )
348 {
349 Vec_IntFill( p->vTempC[0], 1, i+1 ); // 2^i
350 Vec_IntFill( p->vTempC[1], 1, -i-1 ); // -2^i
351
352 iDriver = Gia_ObjFaninId0p( pGia, pObj );
353 Vec_IntFill( p->vTempM[0], 1, iDriver ); // Driver
354
355 if ( fSigned && i == Gia_ManCoNum(pGia)-1 )
356 {
357 if ( Gia_ObjFaninC0(pObj) )
358 {
359 Gia_PolynBuildAdd( p, p->vTempC[1], NULL ); // -C
360 Gia_PolynBuildAdd( p, p->vTempC[0], p->vTempM[0] ); // C * Driver
361 }
362 else
363 Gia_PolynBuildAdd( p, p->vTempC[1], p->vTempM[0] ); // -C * Driver
364 }
365 else
366 {
367 if ( Gia_ObjFaninC0(pObj) )
368 {
369 Gia_PolynBuildAdd( p, p->vTempC[0], NULL ); // C
370 Gia_PolynBuildAdd( p, p->vTempC[1], p->vTempM[0] ); // -C * Driver
371 }
372 else
373 Gia_PolynBuildAdd( p, p->vTempC[0], p->vTempM[0] ); // C * Driver
374 }
375 }
376 LevPrev = -1;
377 for ( Iter = 0; ; Iter++ )
378 {
379 Vec_Int_t * vTempM;
380 //abctime temp = Abc_Clock();
381 if ( Vec_QueSize(p->vQue) == 0 )
382 break;
383 iMono = Vec_QuePop(p->vQue);
384
385 // report
386 vTempM = Hsh_VecReadEntry( p->pHashM, iMono );
387 //printf( "Removing var %d\n", Vec_IntEntryLast(vTempM) );
388 LevCur = Vec_IntEntryLast(vTempM);
389 if ( !Gia_ObjIsAnd(Gia_ManObj(pGia, LevCur)) )
390 continue;
391
392 if ( LevPrev != LevCur )
393 {
394 if ( Vec_BitEntry( vPres, LevCur ) && fVerbose )
395 printf( "Repeating entry %d\n", LevCur );
396 else
397 Vec_BitSetEntry( vPres, LevCur, 1 );
398
399 if ( fVeryVerbose )
400 printf( "Line%5d Iter%10d : Obj =%6d. Order =%6d. HashC =%6d. HashM =%10d. Total =%10d. Used =%10d.\n",
401 Line++, Iter, LevCur, Vec_IntEntry(p->vOrder, LevCur), Hsh_VecSize(p->pHashC), Hsh_VecSize(p->pHashM), p->nBuilds, p->nUsed );
402 }
403 LevPrev = LevCur;
404
405 Gia_PolynBuildOne( p, iMono );
406 //clk2 += Abc_Clock() - temp;
407 }
408 //Abc_PrintTime( 1, "Time2", clk2 );
409 Pln_ManPrintFinal( p, fVerbose, fVeryVerbose );
410 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
411 Pln_ManStop( p );
412 Vec_BitFree( vPres );
413}
void Pln_ManStop(Pln_Man_t *p)
Definition acecPolyn.c:101
void Pln_ManPrintFinal(Pln_Man_t *p, int fVerbose, int fVeryVerbose)
Definition acecPolyn.c:125
void Gia_PolynBuildOne(Pln_Man_t *p, int iMono)
Definition acecPolyn.c:258
typedefABC_NAMESPACE_IMPL_START struct Pln_Man_t_ Pln_Man_t
DECLARATIONS ///.
Definition acecPolyn.c:45
Pln_Man_t * Pln_ManAlloc(Gia_Man_t *pGia, Vec_Int_t *vOrder)
FUNCTION DEFINITIONS ///.
Definition acecPolyn.c:76
#define Gia_ManForEachCoReverse(p, pObj, i)
Definition gia.h:1242
Here is the call graph for this function:

◆ Gia_PolynFindOrder()

Vec_Int_t * Gia_PolynFindOrder ( Gia_Man_t * pGia,
Vec_Int_t * vFadds,
Vec_Int_t * vHadds,
int fVerbose,
int fVeryVerbose )
extern

DECLARATIONS ///.

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

FileName [acecOrder.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [CEC for arithmetic circuits.]

Synopsis [Node ordering.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

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

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file acecOrder.c.

46{
47 int fDumpLeftOver = 0;
48 int i, iXor, iMaj, iAnd, Entry, Iter, fFound, fFoundAll = 1;
49 Vec_Int_t * vRecord = Vec_IntAlloc( 100 ), * vLeft, * vRecord2;
50 Vec_Int_t * vMap = Vec_IntStart( Gia_ManObjNum(pGia) );
51 Gia_ManForEachCoDriverId( pGia, iAnd, i )
52 Vec_IntWriteEntry( vMap, iAnd, 1 );
53
54 // collect the last XOR
55 Vec_IntFreeP( &pGia->vXors );
56 pGia->vXors = Gia_PolynCollectLastXor( pGia, fVerbose );
57 printf( "Collected %d topmost XORs\n", Vec_IntSize(pGia->vXors) );
58 //Vec_IntPrint( p->vXors );
59 Vec_IntForEachEntry( pGia->vXors, iAnd, i )
60 {
61 Gia_Obj_t * pAnd = Gia_ManObj( pGia, iAnd );
62 assert( Vec_IntEntry(vMap, iAnd) );
63 Vec_IntWriteEntry( vMap, iAnd, 0 );
64 Vec_IntWriteEntry( vMap, Gia_ObjFaninId0(pAnd, iAnd), 1 );
65 Vec_IntWriteEntry( vMap, Gia_ObjFaninId1(pAnd, iAnd), 1 );
66 Vec_IntPush( vRecord, Abc_Var2Lit2(iAnd, 3) );
67 if ( fVeryVerbose )
68 printf( "Recognizing %d => XXXOR(%d %d)\n", iAnd, Gia_ObjFaninId0(pAnd, iAnd), Gia_ObjFaninId1(pAnd, iAnd) );
69 }
70
71 // detect FAs and HAs
72 for ( Iter = 0; fFoundAll; Iter++ )
73 {
74 if ( fVeryVerbose )
75 printf( "Iteration %d\n", Iter );
76
77 // check if we can extract FADDs
78 fFoundAll = 0;
79 do {
80 fFound = 0;
81 for ( i = Vec_IntSize(vFadds)/5 - 1; i >= 0; i-- )
82 {
83 iXor = Vec_IntEntry(vFadds, 5*i+3);
84 iMaj = Vec_IntEntry(vFadds, 5*i+4);
85 if ( Vec_IntEntry(vMap, iXor) && Vec_IntEntry(vMap, iMaj) )
86 {
87 Vec_IntWriteEntry( vMap, iXor, 0 );
88 Vec_IntWriteEntry( vMap, iMaj, 0 );
89 Vec_IntWriteEntry( vMap, Vec_IntEntry(vFadds, 5*i+0), 1 );
90 Vec_IntWriteEntry( vMap, Vec_IntEntry(vFadds, 5*i+1), 1 );
91 Vec_IntWriteEntry( vMap, Vec_IntEntry(vFadds, 5*i+2), 1 );
92 Vec_IntPush( vRecord, Abc_Var2Lit2(i, 2) );
93 fFound = 1;
94 fFoundAll = 1;
95 if ( fVeryVerbose )
96 printf( "Recognizing (%d %d) => FA(%d %d %d)\n", iXor, iMaj, Vec_IntEntry(vFadds, 5*i+0), Vec_IntEntry(vFadds, 5*i+1), Vec_IntEntry(vFadds, 5*i+2) );
97 }
98 }
99 } while ( fFound );
100 // check if we can extract HADDs
101 do {
102 fFound = 0;
103 for ( i = Vec_IntSize(vHadds)/2 - 1; i >= 0; i-- )
104 {
105 iXor = Vec_IntEntry(vHadds, 2*i+0);
106 iMaj = Vec_IntEntry(vHadds, 2*i+1);
107 if ( Vec_IntEntry(vMap, iXor) && Vec_IntEntry(vMap, iMaj) )
108 {
109 Gia_Obj_t * pAnd = Gia_ManObj( pGia, iMaj );
110 Vec_IntWriteEntry( vMap, iXor, 0 );
111 Vec_IntWriteEntry( vMap, iMaj, 0 );
112 Vec_IntWriteEntry( vMap, Gia_ObjFaninId0(pAnd, iMaj), 1 );
113 Vec_IntWriteEntry( vMap, Gia_ObjFaninId1(pAnd, iMaj), 1 );
114 Vec_IntPush( vRecord, Abc_Var2Lit2(i, 1) );
115 fFound = 1;
116 fFoundAll = 1;
117 if ( fVeryVerbose )
118 printf( "Recognizing (%d %d) => HA(%d %d)\n", iXor, iMaj, Gia_ObjFaninId0(pAnd, iMaj), Gia_ObjFaninId1(pAnd, iMaj) );
119 }
120 }
121 break; // only one iter!
122 } while ( fFound );
123 if ( fFoundAll )
124 continue;
125/*
126 // find the last one
127 Vec_IntForEachEntryReverse( vMap, Entry, iAnd )
128 if ( Entry && Gia_ObjIsAnd(Gia_ManObj(pGia, iAnd)) )//&& Vec_IntFind(vFadds, iAnd) == -1 )//&& Vec_IntFind(vHadds, iAnd) == -1 )
129 {
130 Gia_Obj_t * pFan0, * pFan1, * pAnd = Gia_ManObj( pGia, iAnd );
131 if ( !Gia_ObjRecognizeExor(pAnd, &pFan0, &pFan1) )
132 {
133 Vec_IntWriteEntry( vMap, iAnd, 0 );
134 Vec_IntWriteEntry( vMap, Gia_ObjFaninId0(pAnd, iAnd), 1 );
135 Vec_IntWriteEntry( vMap, Gia_ObjFaninId1(pAnd, iAnd), 1 );
136 Vec_IntPush( vRecord, Abc_Var2Lit2(iAnd, 0) );
137 }
138 else
139 {
140 Vec_IntWriteEntry( vMap, iAnd, 0 );
141 Vec_IntWriteEntry( vMap, Gia_ObjId(pGia, pFan0), 1 );
142 Vec_IntWriteEntry( vMap, Gia_ObjId(pGia, pFan1), 1 );
143 Vec_IntPush( vRecord, Abc_Var2Lit2(iAnd, 0) );
144 Vec_IntPush( vRecord, Abc_Var2Lit2(Gia_ObjFaninId0(pAnd, iAnd), 0) );
145 Vec_IntPush( vRecord, Abc_Var2Lit2(Gia_ObjFaninId1(pAnd, iAnd), 0) );
146 printf( "Recognizing %d => XOR(%d %d)\n", iAnd, Gia_ObjId(pGia, pFan0), Gia_ObjId(pGia, pFan1) );
147 }
148 fFoundAll = 1;
149 if ( fVeryVerbose )
150 printf( "Recognizing %d => AND(%d %d)\n", iAnd, Gia_ObjFaninId0(pAnd, iAnd), Gia_ObjFaninId1(pAnd, iAnd) );
151 break;
152 }
153*/
154 }
155 //Vec_IntPrint( vMap );
156
157 // collect remaining ones
158 vLeft = Vec_IntAlloc( 100 );
159 Vec_IntForEachEntry( vMap, Entry, i )
160 if ( Entry && Gia_ObjIsAnd(Gia_ManObj(pGia, i)) )
161 Vec_IntPush( vLeft, i );
162 Vec_IntFree( vMap );
163
164 // collect them in the topo order
165 vRecord2 = Vec_IntAlloc( 100 );
167 Gia_ManCollectAnds( pGia, Vec_IntArray(vLeft), Vec_IntSize(vLeft), vRecord2, NULL );
168 Vec_IntForEachEntry( vRecord2, iAnd, i )
169 Vec_IntWriteEntry( vRecord2, i, Abc_Var2Lit2(iAnd, 0) );
170
171 // dump remaining nodes as an AIG
172 if ( fDumpLeftOver )
173 {
174 Gia_Man_t * pNew;
175 pNew = Gia_ManDupAndCones( pGia, Vec_IntArray(vLeft), Vec_IntSize(vLeft), 0 );
176 Gia_AigerWrite( pNew, "leftover.aig", 0, 0, 0 );
177 printf( "Leftover AIG with %d nodes is dumped into file \"%s\".\n", Gia_ManAndNum(pNew), "leftover.aig" );
178 Gia_ManStop( pNew );
179 }
180 Vec_IntFree( vLeft );
181
182 Vec_IntReverseOrder( vRecord );
183 Vec_IntAppend( vRecord2, vRecord );
184 Vec_IntFree( vRecord );
185 return vRecord2;
186}
Vec_Int_t * Gia_PolynCollectLastXor(Gia_Man_t *pGia, int fVerbose)
Definition acecUtil.c:57
#define Gia_ManForEachCoDriverId(p, DriverId, i)
Definition gia.h:1246
void Gia_ManIncrementTravId(Gia_Man_t *p)
Definition giaUtil.c:190
Gia_Man_t * Gia_ManDupAndCones(Gia_Man_t *p, int *pAnds, int nAnds, int fTrimPis)
Definition giaDup.c:3941
void Gia_ManCollectAnds(Gia_Man_t *p, int *pNodes, int nNodes, Vec_Int_t *vNodes, Vec_Int_t *vLeaves)
Definition giaDfs.c:125
Vec_Int_t * vXors
Definition gia.h:164
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Gia_PolynReorder()

Vec_Int_t * Gia_PolynReorder ( Gia_Man_t * pGia,
int fVerbose,
int fVeryVerbose )
extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 199 of file acecOrder.c.

200{
201 Vec_Int_t * vFadds = Gia_ManDetectFullAdders( pGia, fVeryVerbose, NULL );
202 Vec_Int_t * vHadds = Gia_ManDetectHalfAdders( pGia, fVeryVerbose );
203 Vec_Int_t * vRecord = Gia_PolynFindOrder( pGia, vFadds, vHadds, fVerbose, fVeryVerbose );
204 Vec_Int_t * vOrder = Vec_IntAlloc( Gia_ManAndNum(pGia) );
205 Vec_Int_t * vOrder2 = Vec_IntStart( Gia_ManObjNum(pGia) );
206 int i, k, Entry;
207
208 // collect nodes
210 Vec_IntForEachEntry( vRecord, Entry, i )
211 {
212 int Node = Abc_Lit2Var2(Entry);
213 int Attr = Abc_Lit2Att2(Entry);
214 if ( Attr == 2 )
215 {
216 int * pFanins = Vec_IntEntryP( vFadds, 5*Node );
217 for ( k = 3; k < 5; k++ )
218 Gia_ManCollectAnds_rec( pGia, pFanins[k], vOrder );
219 }
220 else if ( Attr == 1 )
221 {
222 int * pFanins = Vec_IntEntryP( vHadds, 2*Node );
223 for ( k = 0; k < 2; k++ )
224 Gia_ManCollectAnds_rec( pGia, pFanins[k], vOrder );
225 }
226 else
227 Gia_ManCollectAnds_rec( pGia, Node, vOrder );
228 //printf( "Order = %d. Node = %d. Size = %d ", i, Node, Vec_IntSize(vOrder) );
229 }
230 //printf( "\n" );
231 //assert( Vec_IntSize(vOrder) == Gia_ManAndNum(pGia) );
232
233 // remap order
234 Gia_ManForEachCiId( pGia, Entry, i )
235 Vec_IntWriteEntry( vOrder2, Entry, 1+i );
236 Vec_IntForEachEntry( vOrder, Entry, i )
237 Vec_IntWriteEntry( vOrder2, Entry, 1+Gia_ManCiNum(pGia)+i );
238 //Vec_IntPrint( vOrder );
239
240 Vec_IntFree( vRecord );
241 Vec_IntFree( vFadds );
242 Vec_IntFree( vHadds );
243 Vec_IntFree( vOrder );
244 return vOrder2;
245}
ABC_NAMESPACE_IMPL_START Vec_Int_t * Gia_PolynFindOrder(Gia_Man_t *pGia, Vec_Int_t *vFadds, Vec_Int_t *vHadds, int fVerbose, int fVeryVerbose)
DECLARATIONS ///.
Definition acecOrder.c:45
Vec_Int_t * Gia_ManDetectHalfAdders(Gia_Man_t *p, int fVerbose)
FUNCTION DEFINITIONS ///.
Definition acecFadds.c:50
Vec_Int_t * Gia_ManDetectFullAdders(Gia_Man_t *p, int fVerbose, Vec_Int_t **vCutsXor2)
Definition acecFadds.c:442
void Gia_ManCollectAnds_rec(Gia_Man_t *p, int iObj, Vec_Int_t *vNodes)
Definition giaDfs.c:99
#define Gia_ManForEachCiId(p, Id, i)
Definition gia.h:1230
Here is the call graph for this function:

◆ Ree_ManComputeCuts()

Vec_Int_t * Ree_ManComputeCuts ( Gia_Man_t * p,
Vec_Int_t ** pvXors,
int fVerbose )
extern

Definition at line 408 of file acecRe.c.

409{
410 extern void Ree_ManRemoveTrivial( Gia_Man_t * p, Vec_Int_t * vAdds );
411 extern void Ree_ManRemoveContained( Gia_Man_t * p, Vec_Int_t * vAdds );
412 Gia_Obj_t * pObj;
413 int * pList0, * pList1, i, nCuts = 0;
414 Hash_IntMan_t * pHash = Hash_IntManStart( 1000 );
415 Vec_Int_t * vAdds;
416 Vec_Int_t * vTemp = Vec_IntAlloc( 1000 );
417 Vec_Int_t * vData = Vec_IntAlloc( 1000 );
418 Vec_Int_t * vCuts = Vec_IntAlloc( 30 * Gia_ManAndNum(p) );
419 Vec_IntFill( vCuts, Gia_ManObjNum(p), 0 );
421 Gia_ManForEachCi( p, pObj, i )
422 {
423 Vec_IntWriteEntry( vCuts, Gia_ObjId(p, pObj), Vec_IntSize(vCuts) );
424 Vec_IntPush( vCuts, 1 );
425 Vec_IntPush( vCuts, 1 );
426 Vec_IntPush( vCuts, Gia_ObjId(p, pObj) );
427 Vec_IntPush( vCuts, 0xAA );
428 }
429 if ( pvXors ) *pvXors = Vec_IntAlloc( 1000 );
430 Gia_ManForEachAnd( p, pObj, i )
431 {
432 pList0 = Vec_IntEntryP( vCuts, Vec_IntEntry(vCuts, Gia_ObjFaninId0(pObj, i)) );
433 pList1 = Vec_IntEntryP( vCuts, Vec_IntEntry(vCuts, Gia_ObjFaninId1(pObj, i)) );
434 Ree_ManCutMerge( p, i, pList0, pList1, vTemp, pHash, vData, pvXors ? *pvXors : NULL );
435 Vec_IntWriteEntry( vCuts, i, Vec_IntSize(vCuts) );
436 Vec_IntAppend( vCuts, vTemp );
437 nCuts += Vec_IntEntry( vTemp, 0 );
438 }
439 if ( fVerbose )
440 printf( "AIG nodes = %d. Cuts = %d. Cuts/Node = %.2f. Ints/Node = %.2f.\n",
441 Gia_ManAndNum(p), nCuts, 1.0*nCuts/Gia_ManAndNum(p), 1.0*Vec_IntSize(vCuts)/Gia_ManAndNum(p) );
442 Vec_IntFree( vTemp );
443 Vec_IntFree( vCuts );
444 vAdds = Ree_ManDeriveAdds( pHash, vData, fVerbose );
445 qsort( Vec_IntArray(vAdds), (size_t)(Vec_IntSize(vAdds)/6), 24, (int (*)(const void *, const void *))Ree_ManCompare );
446 if ( fVerbose )
447 printf( "Adders = %d. Total cuts = %d. Hashed cuts = %d. Hashed/Adders = %.2f.\n",
448 Vec_IntSize(vAdds)/6, Vec_IntSize(vData)/3, Hash_IntManEntryNum(pHash), 6.0*Hash_IntManEntryNum(pHash)/Vec_IntSize(vAdds) );
449 Vec_IntFree( vData );
450 Hash_IntManStop( pHash );
451 Ree_ManRemoveTrivial( p, vAdds );
452 Ree_ManRemoveContained( p, vAdds );
453 //Ree_ManPrintAdders( vAdds, 1 );
454 return vAdds;
455}
int Ree_ManCompare(int *pCut0, int *pCut1)
Definition acecRe.c:400
void Ree_ManRemoveContained(Gia_Man_t *p, Vec_Int_t *vAdds)
Definition acecRe.c:540
void Ree_ManRemoveTrivial(Gia_Man_t *p, Vec_Int_t *vAdds)
Definition acecRe.c:515
Vec_Int_t * Ree_ManDeriveAdds(Hash_IntMan_t *p, Vec_Int_t *vData, int fVerbose)
Definition acecRe.c:328
void Ree_ManCutMerge(Gia_Man_t *p, int iObj, int *pList0, int *pList1, Vec_Int_t *vCuts, Hash_IntMan_t *pHash, Vec_Int_t *vData, Vec_Int_t *vXors)
Definition acecRe.c:258
void Gia_ManCleanValue(Gia_Man_t *p)
Definition giaUtil.c:351
#define Gia_ManForEachCi(p, pObj, i)
Definition gia.h:1228
struct Hash_IntMan_t_ Hash_IntMan_t
Definition vecHash.h:51
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Ree_ManCountFadds()

int Ree_ManCountFadds ( Vec_Int_t * vAdds)
extern

Definition at line 556 of file acecRe.c.

557{
558 int i, Count = 0;
559 for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ )
560 if ( Vec_IntEntry(vAdds, 6*i+2) != 0 )
561 Count++;
562 return Count;
563}
Here is the caller graph for this function:

◆ Ree_ManPrintAdders()

void Ree_ManPrintAdders ( Vec_Int_t * vAdds,
int fVerbose )
extern

Definition at line 564 of file acecRe.c.

565{
566 int i;
567 for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ )
568 {
569 //if ( Vec_IntEntry(vAdds, 6*i+2) == 0 )
570 // continue;
571 if ( !fVerbose )
572 continue;
573 printf( "%6d : ", i );
574 printf( "%6d ", Vec_IntEntry(vAdds, 6*i+0) );
575 printf( "%6d ", Vec_IntEntry(vAdds, 6*i+1) );
576 printf( "%6d ", Vec_IntEntry(vAdds, 6*i+2) );
577 printf( " -> " );
578 printf( "%6d ", Vec_IntEntry(vAdds, 6*i+3) );
579 printf( "%6d ", Vec_IntEntry(vAdds, 6*i+4) );
580 printf( " (%d)", Vec_IntEntry(vAdds, 6*i+5) );
581 printf( "\n" );
582 }
583}
Here is the caller graph for this function: