Skip to content

A
abc
Commit 5ebe403a by Alan Mishchenko
Options

Print-out of sequential equivalences in &scorr.

parent d00cbdb5
Showing with 59 additions and 21 deletions
src/aig/gia/gia.h
......@@ -1330,7 +1330,7 @@ extern void Gia_ManStgPrint( FILE * pFile, Vec_Int_t * vLines, in
extern Gia_Man_t * Gia_ManStgRead( char * pFileName, int kHot, int fVerbose );
/*=== giaSweep.c ============================================================*/
extern Gia_Man_t * Gia_ManFraigSweepSimple( Gia_Man_t * p, void * pPars );
extern Gia_Man_t * Gia_ManSweepWithBoxes( Gia_Man_t * p, void * pParsC, void * pParsS, int fConst, int fEquiv, int fVerbose );
extern Gia_Man_t * Gia_ManSweepWithBoxes( Gia_Man_t * p, void * pParsC, void * pParsS, int fConst, int fEquiv, int fVerbose, int fVerbEquivs );
extern void Gia_ManCheckIntegrityWithBoxes( Gia_Man_t * p );
/*=== giaSweeper.c ============================================================*/
extern Gia_Man_t * Gia_SweeperStart( Gia_Man_t * p );
......
src/aig/gia/giaSweep.c
......@@ -439,7 +439,7 @@ void Gia_ManCheckIntegrityWithBoxes( Gia_Man_t * p )
SeeAlso []
***********************************************************************/
int * Gia_ManFraigSelectReprs( Gia_Man_t * p, Gia_Man_t * pClp, int fVerbose )
int * Gia_ManFraigSelectReprs( Gia_Man_t * p, Gia_Man_t * pClp, int fVerbose, int pFlopTypes[3] )
{
Gia_Obj_t * pObj;
Vec_Int_t * vCarryOuts;
......@@ -482,6 +482,20 @@ int * Gia_ManFraigSelectReprs( Gia_Man_t * p, Gia_Man_t * pClp, int fVerbose )
Gia_ManRegBoxNum(p), Vec_IntSize(vCarryOuts), Gia_ManNonRegBoxNum(p) );
Vec_IntFree( vCarryOuts );
// collect equivalent node info
pFlopTypes[0] = pFlopTypes[1] = pFlopTypes[2] = 0;
Gia_ManForEachRo( pClp, pObj, i )
{
Gia_Obj_t * pRepr = Gia_ObjReprObj(pClp, i);
if ( pRepr && pRepr != pObj )
{
if ( pRepr == Gia_ManConst0(pClp) )
pFlopTypes[0]++;
else if ( Gia_ObjIsRo(pClp, pRepr) )
pFlopTypes[1]++;
}
}
// compute representatives
pClp2Gia[0] = 0;
Gia_ManSetPhase( pClp );
......@@ -618,11 +632,11 @@ void Gia_ManSweepComputeOneDomainEquivs( Gia_Man_t * p, Vec_Int_t * vRegClasses,
Gia_ManDupRemapEquiv( p, pNew );
Gia_ManStop( pNew );
}
Gia_Man_t * Gia_ManSweepWithBoxesAndDomains( Gia_Man_t * p, void * pParsS, int fConst, int fEquiv, int fVerbose )
Gia_Man_t * Gia_ManSweepWithBoxesAndDomains( Gia_Man_t * p, void * pParsS, int fConst, int fEquiv, int fVerbose, int fVerbEquivs )
{
Gia_Man_t * pClp, * pNew, * pTemp;
int nDoms = Vec_IntFindMax(p->vRegClasses);
int * pReprs, iDom;
int * pReprs, iDom, pFlopTypes[3] = {0};
assert( Gia_ManRegNum(p) == 0 );
assert( p->pAigExtra != NULL );
assert( nDoms > 1 );
......@@ -634,7 +648,7 @@ Gia_Man_t * Gia_ManSweepWithBoxesAndDomains( Gia_Man_t * p, void * pParsS, int f
// iterate over domains
for ( iDom = 1; iDom <= nDoms; iDom++ )
{
int nFlops = Vec_IntCountEntry(pNew->vRegClasses, iDom);
int nFlopsNew, nFlops = Vec_IntCountEntry(pNew->vRegClasses, iDom);
if ( nFlops < 2 )
continue;
// find global equivalences
......@@ -642,7 +656,7 @@ Gia_Man_t * Gia_ManSweepWithBoxesAndDomains( Gia_Man_t * p, void * pParsS, int f
// compute equivalences
Gia_ManSweepComputeOneDomainEquivs( pClp, pNew->vRegClasses, iDom, pParsS, fConst, fEquiv, fVerbose );
// transfer equivalences
pReprs = Gia_ManFraigSelectReprs( pNew, pClp, fVerbose );
pReprs = Gia_ManFraigSelectReprs( pNew, pClp, fVerbose, pFlopTypes );
Gia_ManStop( pClp );
// reduce AIG
Gia_ManTransferTiming( p, pNew );
......@@ -654,10 +668,14 @@ Gia_Man_t * Gia_ManSweepWithBoxesAndDomains( Gia_Man_t * p, void * pParsS, int f
pNew = Gia_ManDupWithBoxes( pTemp = pNew, 1 );
Gia_ManStop( pTemp );
// report
if ( fVerbose )
nFlopsNew = Vec_IntCountEntry(pNew->vRegClasses, iDom);
pFlopTypes[2] = nFlops - nFlopsNew - (pFlopTypes[0] + pFlopTypes[1]);
if ( fVerbEquivs )
{
printf( "Domain %2d : %5d -> %5d : ", iDom, nFlops, Vec_IntCountEntry(pNew->vRegClasses, iDom) );
Gia_ManPrintStats( pNew, NULL );
printf( "Domain %2d : %5d -> %5d : ", iDom, nFlops, nFlopsNew );
printf( "EqConst =%4d. EqFlop =%4d. Dangling =%4d. Unused =%4d.\n",
pFlopTypes[0], pFlopTypes[1], Abc_MaxInt(0, pFlopTypes[2]), Abc_MaxInt(0, -pFlopTypes[2]) );
//Gia_ManPrintStats( pNew, NULL );
}
}
// normalize the result
......@@ -680,20 +698,22 @@ Gia_Man_t * Gia_ManSweepWithBoxesAndDomains( Gia_Man_t * p, void * pParsS, int f
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManSweepWithBoxes( Gia_Man_t * p, void * pParsC, void * pParsS, int fConst, int fEquiv, int fVerbose )
Gia_Man_t * Gia_ManSweepWithBoxes( Gia_Man_t * p, void * pParsC, void * pParsS, int fConst, int fEquiv, int fVerbose, int fVerbEquivs )
{
Gia_Man_t * pClp, * pNew, * pTemp;
int * pReprs;
int * pReprs, pFlopTypes[3] = {0};
int nFlopsNew, nFlops;
assert( Gia_ManRegNum(p) == 0 );
assert( p->pAigExtra != NULL );
// consider seq synthesis with multiple clock domains
if ( pParsC == NULL && Gia_ManClockDomainNum(p) > 1 )
return Gia_ManSweepWithBoxesAndDomains( p, pParsS, fConst, fEquiv, fVerbose );
return Gia_ManSweepWithBoxesAndDomains( p, pParsS, fConst, fEquiv, fVerbose, fVerbEquivs );
// order AIG objects
pNew = Gia_ManDupUnnormalize( p );
if ( pNew == NULL )
return NULL;
Gia_ManTransferTiming( pNew, p );
nFlops = Vec_IntCountEntry(pNew->vRegClasses, 1);
// find global equivalences
pClp = Gia_ManDupCollapse( pNew, pNew->pAigExtra, NULL, pParsC ? 0 : 1 );
// compute equivalences
......@@ -704,7 +724,7 @@ Gia_Man_t * Gia_ManSweepWithBoxes( Gia_Man_t * p, void * pParsC, void * pParsS,
else
Gia_ManSeqCleanupClasses( pClp, fConst, fEquiv, fVerbose );
// transfer equivalences
pReprs = Gia_ManFraigSelectReprs( pNew, pClp, fVerbose );
pReprs = Gia_ManFraigSelectReprs( pNew, pClp, fVerbose, pFlopTypes );
Gia_ManStop( pClp );
// reduce AIG
Gia_ManTransferTiming( p, pNew );
......@@ -715,6 +735,15 @@ Gia_Man_t * Gia_ManSweepWithBoxes( Gia_Man_t * p, void * pParsC, void * pParsS,
// derive new AIG
pNew = Gia_ManDupWithBoxes( pTemp = pNew, pParsC ? 0 : 1 );
Gia_ManStop( pTemp );
// report
nFlopsNew = Vec_IntCountEntry(pNew->vRegClasses, 1);
pFlopTypes[2] = nFlops - nFlopsNew - (pFlopTypes[0] + pFlopTypes[1]);
if ( fVerbEquivs )
{
printf( "Domain %2d : %5d -> %5d : ", 1, nFlops, nFlopsNew );
printf( "EqConst =%4d. EqFlop =%4d. Dangling =%4d. Unused =%4d.\n",
pFlopTypes[0], pFlopTypes[1], Abc_MaxInt(0, pFlopTypes[2]), Abc_MaxInt(0, -pFlopTypes[2]) );
}
// normalize the result
pNew = Gia_ManDupNormalize( pTemp = pNew );
Gia_ManTransferTiming( pNew, pTemp );
......
src/base/abci/abc.c
......@@ -29731,8 +29731,9 @@ int Abc_CommandAbc9Scl( Abc_Frame_t * pAbc, int argc, char ** argv )
int fConst = 1;
int fEquiv = 1;
int fVerbose = 0;
int fVerboseFlops = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "cevh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "cevwh" ) ) != EOF )
{
switch ( c )
{
......@@ -29745,6 +29746,9 @@ int Abc_CommandAbc9Scl( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'v':
fVerbose ^= 1;
break;
case 'w':
fVerboseFlops ^= 1;
break;
default:
goto usage;
}
......@@ -29761,7 +29765,7 @@ int Abc_CommandAbc9Scl( Abc_Frame_t * pAbc, int argc, char ** argv )
printf( "Timing manager is given but there is no GIA of boxes.\n" );
return 0;
}
pTemp = Gia_ManSweepWithBoxes( pAbc->pGia, NULL, NULL, fConst, fEquiv, fVerbose );
pTemp = Gia_ManSweepWithBoxes( pAbc->pGia, NULL, NULL, fConst, fEquiv, fVerbose, fVerboseFlops );
Abc_FrameUpdateGia( pAbc, pTemp );
return 0;
}
......@@ -29775,11 +29779,12 @@ int Abc_CommandAbc9Scl( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: &scl [-cevh]\n" );
Abc_Print( -2, "usage: &scl [-cevwh]\n" );
Abc_Print( -2, "\t performs structural sequential cleanup\n" );
Abc_Print( -2, "\t-c : toggle removing stuck-at constant registers [default = %s]\n", fConst? "yes": "no" );
Abc_Print( -2, "\t-e : toggle removing equivalent-driver registers [default = %s]\n", fEquiv? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-w : toggle printing verbose info about equivalent flops [default = %s]\n", fVerboseFlops? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
......@@ -29803,7 +29808,7 @@ int Abc_CommandAbc9Lcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
Cec_ManCorSetDefaultParams( pPars );
pPars->fLatchCorr = 1;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "FCPrcvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "FCPrcvwh" ) ) != EOF )
{
switch ( c )
{
......@@ -29849,6 +29854,9 @@ int Abc_CommandAbc9Lcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'v':
pPars->fVerbose ^= 1;
break;
case 'w':
pPars->fVerboseFlops ^= 1;
break;
default:
goto usage;
}
......@@ -29865,7 +29873,7 @@ int Abc_CommandAbc9Lcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
printf( "Timing manager is given but there is no GIA of boxes.\n" );
return 0;
}
pTemp = Gia_ManSweepWithBoxes( pAbc->pGia, NULL, pPars, 0, 0, pPars->fVerbose );
pTemp = Gia_ManSweepWithBoxes( pAbc->pGia, NULL, pPars, 0, 0, pPars->fVerbose, pPars->fVerboseFlops );
Abc_FrameUpdateGia( pAbc, pTemp );
return 0;
}
......@@ -29879,7 +29887,7 @@ int Abc_CommandAbc9Lcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: &lcorr [-FCP num] [-rcvh]\n" );
Abc_Print( -2, "usage: &lcorr [-FCP num] [-rcvwh]\n" );
Abc_Print( -2, "\t performs latch correpondence computation\n" );
Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
Abc_Print( -2, "\t-F num : the number of timeframes in inductive case [default = %d]\n", pPars->nFrames );
......@@ -29887,6 +29895,7 @@ usage:
Abc_Print( -2, "\t-r : toggle using implication rings during refinement [default = %s]\n", pPars->fUseRings? "yes": "no" );
Abc_Print( -2, "\t-c : toggle using circuit-based SAT solver [default = %s]\n", pPars->fUseCSat? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-w : toggle printing verbose info about equivalent flops [default = %s]\n", pPars->fVerboseFlops? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
......@@ -29983,7 +29992,7 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
printf( "Timing manager is given but there is no GIA of boxes.\n" );
return 0;
}
pTemp = Gia_ManSweepWithBoxes( pAbc->pGia, NULL, pPars, 0, 0, pPars->fVerbose );
pTemp = Gia_ManSweepWithBoxes( pAbc->pGia, NULL, pPars, 0, 0, pPars->fVerbose, pPars->fVerboseFlops );
Abc_FrameUpdateGia( pAbc, pTemp );
return 0;
}
......@@ -31249,7 +31258,7 @@ int Abc_CommandAbc9Sweep( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
}
if ( Gia_ManBoxNum(pAbc->pGia) )
pTemp = Gia_ManSweepWithBoxes( pAbc->pGia, pPars, NULL, 0, 0, pPars->fVerbose );
pTemp = Gia_ManSweepWithBoxes( pAbc->pGia, pPars, NULL, 0, 0, pPars->fVerbose, 0 );
else
pTemp = Gia_ManFraigSweepSimple( pAbc->pGia, pPars );
Abc_FrameUpdateGia( pAbc, pTemp );
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment