luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Merged alanmi/abc into default

This commit is contained in:
Mathias Soeken 2016-08-15 10:33:54 +02:00
parent 24af634508 9dc2f48858
commit 68f29c527e
7 changed files with 115 additions and 17 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

19
src/aig/gia/giaSatLE.c
View File

@ -867,25 +867,31 @@ int Sle_ManAddEdgeConstraints( Sle_Man_t * p, int nEdges )
***********************************************************************/
void Sle_ManDeriveResult( Sle_Man_t * p, Vec_Int_t * vEdge2, Vec_Int_t * vMapping )
{
Vec_Int_t * vMapTemp;
int iObj;
// create mapping
Vec_IntFill( vMapping, Gia_ManObjNum(p->pGia), 0 );
Gia_ManForEachAndId( p->pGia, iObj )
{
int i, iCut, iCutVar0 = Vec_IntEntry( p->vCutFirst, iObj );
int * pCut, * pList = Sle_ManList( p, iObj );
int * pCut, * pCutThis = NULL, * pList = Sle_ManList( p, iObj );
if ( !sat_solver_var_value(p->pSat, iObj) )
continue;
Sle_ForEachCut( pList, pCut, iCut )
if ( sat_solver_var_value(p->pSat, iCutVar0 + iCut) )
break;
assert( iCut < Sle_ListCutNum(pList) );
{
assert( pCutThis == NULL );
pCutThis = pCut;
}
assert( pCutThis != NULL );
Vec_IntWriteEntry( vMapping, iObj, Vec_IntSize(vMapping) );
Vec_IntPush( vMapping, Sle_CutSize(pCut) );
for ( i = 0; i < Sle_CutSize(pCut); i++ )
Vec_IntPush( vMapping, Sle_CutLeaves(pCut)[i] );
Vec_IntPush( vMapping, Sle_CutSize(pCutThis) );
for ( i = 0; i < Sle_CutSize(pCutThis); i++ )
Vec_IntPush( vMapping, Sle_CutLeaves(pCutThis)[i] );
Vec_IntPush( vMapping, iObj );
}
vMapTemp = p->pGia->vMapping;
p->pGia->vMapping = vMapping;
// collect edges
Vec_IntClear( vEdge2 );
Gia_ManForEachAndId( p->pGia, iObj )
@ -918,6 +924,7 @@ void Sle_ManDeriveResult( Sle_Man_t * p, Vec_Int_t * vEdge2, Vec_Int_t * vMappin
Vec_IntPushTwo( vEdge2, iFanin, iObj );
}
}
p->pGia->vMapping = vMapTemp;
}
/**Function*************************************************************

12
src/base/abci/abc.c
View File

@ -40439,13 +40439,13 @@ usage:
***********************************************************************/
int Abc_CommandAbc9Exorcism( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern int Abc_ExorcismMain( Vec_Wec_t * vEsop, int nIns, int nOuts, char * pFileNameOut, int Quality, int Verbosity );
extern int Abc_ExorcismMain( Vec_Wec_t * vEsop, int nIns, int nOuts, char * pFileNameOut, int Quality, int Verbosity, int fUseQCost );
extern Gia_Man_t * Eso_ManCompute( Gia_Man_t * pGia, int fVerbose, Vec_Wec_t ** pvRes );
Vec_Wec_t * vEsop = NULL;
char * pFileNameOut = NULL;
int c, Quality = 2, Verbosity = 0, fVerbose = 0;
int c, Quality = 2, Verbosity = 0, fUseQCost = 0, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "QVvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "QVqvh" ) ) != EOF )
{
switch ( c )
{
@ -40471,6 +40471,9 @@ int Abc_CommandAbc9Exorcism( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( Verbosity < 0 )
goto usage;
break;
case 'q':
fUseQCost ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
@ -40490,7 +40493,7 @@ int Abc_CommandAbc9Exorcism( Abc_Frame_t * pAbc, int argc, char ** argv )
pFileNameOut = argv[globalUtilOptind];
// generate starting cover and run minimization
Eso_ManCompute( pAbc->pGia, fVerbose, &vEsop );
Abc_ExorcismMain( vEsop, Gia_ManCiNum(pAbc->pGia), Gia_ManCoNum(pAbc->pGia), pFileNameOut, Quality, Verbosity );
Abc_ExorcismMain( vEsop, Gia_ManCiNum(pAbc->pGia), Gia_ManCoNum(pAbc->pGia), pFileNameOut, Quality, Verbosity, fUseQCost );
Vec_WecFree( vEsop );
return 0;
@ -40501,6 +40504,7 @@ usage:
Abc_Print( -2, " increasing this number improves quality and adds to runtime\n");
Abc_Print( -2, " -V N : verbosity level [default = %d]\n", Verbosity);
Abc_Print( -2, " 0 = no output; 1 = outline; 2 = verbose\n");
// Abc_Print( -2, " -q : toggle using quantum cost [default = %s]\n", fUseQCost? "yes": "no" );
Abc_Print( -2, " <file>: the output file name in ESOP-PLA format\n");
Abc_Print( -2, "\n" );
return 1;

57
src/base/exor/exor.c
View File

@ -66,6 +66,57 @@ extern int s_fDecreaseLiterals;
/// FUNCTION main() ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Number of negative literals.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static int QCost[16][16] =
{
{ 1}, // 0
{ 1, 2}, // 1
{ 5, 5, 6}, // 2
{ 14, 14, 16, 18}, // 3
{ 20, 20, 20, 22, 24}, // 4
{ 32, 32, 32, 34, 36, 38}, // 5
{ 44, 44, 44, 44, 46, 48, 50}, // 6
{ 56, 56, 56, 56, 58, 60, 62, 64}, // 7
{ 0 }
};
int CountNegLits( Vec_Int_t * vCube )
{
int i, Entry, nLits = 0;
Vec_IntForEachEntry( vCube, Entry, i )
nLits += Abc_LitIsCompl(Entry);
return nLits;
}
int ComputeQCost( Vec_Int_t * vCube )
{
return QCost[Abc_MinInt(Vec_IntSize(vCube), 7)][Abc_MinInt(CountNegLits(vCube), 7)];
}
int ComputeQCostBits( Cube * p )
{
extern varvalue GetVar( Cube* pC, int Var );
int v, nLits = 0, nLitsN = 0;
for ( v = 0; v < g_CoverInfo.nVarsIn; v++ )
{
int Value = GetVar( p, v );
if ( Value == VAR_NEG )
nLitsN++;
else if ( Value == VAR_POS )
nLits++;
}
nLits += nLitsN;
return QCost[Abc_MinInt(nLits, 7)][Abc_MinInt(nLitsN, 7)];
}
/**Function*************************************************************
Synopsis []
@ -591,6 +642,7 @@ void AddCubesToStartingCover( Vec_Wec_t * vEsop )
s_Level2Var[i] = i;
g_CoverInfo.nLiteralsBefore = 0;
g_CoverInfo.QCostBefore = 0;
Vec_WecForEachLevel( vEsop, vCube, c )
{
// get the output of this cube
@ -622,6 +674,7 @@ void AddCubesToStartingCover( Vec_Wec_t * vEsop )
// set literal counts
pNew->a = Vec_IntSize(vCube);
pNew->z = 1;
pNew->q = ComputeQCost(vCube);
// set the ID
pNew->ID = g_CoverInfo.cIDs++;
// skip through zero-ID
@ -632,6 +685,7 @@ void AddCubesToStartingCover( Vec_Wec_t * vEsop )
CheckForCloseCubes( pNew, 1 );
g_CoverInfo.nLiteralsBefore += Vec_IntSize(vCube);
g_CoverInfo.QCostBefore += ComputeQCost(vCube);
}
ABC_FREE( s_Level2Var );
ABC_FREE( s_LevelValues );
@ -798,11 +852,12 @@ int Exorcism( Vec_Wec_t * vEsop, int nIns, int nOuts, char * pFileNameOut )
SeeAlso []
***********************************************************************/
int Abc_ExorcismMain( Vec_Wec_t * vEsop, int nIns, int nOuts, char * pFileNameOut, int Quality, int Verbosity )
int Abc_ExorcismMain( Vec_Wec_t * vEsop, int nIns, int nOuts, char * pFileNameOut, int Quality, int Verbosity, int fUseQCost )
{
memset( &g_CoverInfo, 0, sizeof(cinfo) );
g_CoverInfo.Quality = Quality;
g_CoverInfo.Verbosity = Verbosity;
g_CoverInfo.fUseQCost = fUseQCost;
if ( g_CoverInfo.Verbosity )
{
printf( "\nEXORCISM, Ver.4.7: Exclusive Sum-of-Product Minimizer\n" );

6
src/base/exor/exor.h
View File

@ -105,11 +105,14 @@ typedef struct cinfo_tag
int nCubesInUse; // number of cubes after simplification
int nCubesFree; // number of free cubes
int nLiteralsBefore;// number of literals before
int nLiteralsAfter; // number of literals before
int nLiteralsAfter; // number of literals after
int QCostBefore; // q-cost before
int QCostAfter; // q-cost after
int cIDs; // the counter of cube IDs
int Verbosity; // verbosity level
int Quality; // quality
int fUseQCost; // use q-cost instead of literal count
abctime TimeRead; // reading time
abctime TimeStart; // starting cover computation time
@ -125,6 +128,7 @@ typedef struct cube
byte ID; // (almost) unique ID of the cube
short a; // the number of literals
short z; // the number of 1's in the output part
short q; // user cost
drow* pCubeDataIn; // a pointer to the bit string representing literals
drow* pCubeDataOut; // a pointer to the bit string representing literals
struct cube* Prev; // pointers to the previous/next cubes in the list/ring

1
src/base/exor/exorLink.c
View File

@ -335,6 +335,7 @@ static int DiffVarBits[5];
static drow MaskLiterals;
// the base for counting literals
static int StartingLiterals;
static int StartingQCost;
// the number of literals in each cube
static int CubeLiterals[32];
static int BitShift;

15
src/base/exor/exorList.c
View File

@ -222,6 +222,8 @@ static struct
Cube* p; // the pointer to the modified cube
int PrevQa;
int PrevPa;
int PrevQq;
int PrevPq;
int PrevPz;
int Var; // the number of variable that was changed
int Value; // the value what was there
@ -345,7 +347,9 @@ int IterativelyApplyExorLink2( char fDistEnable )
// decide whether to accept the second group, depending on literals
if ( s_fDecreaseLiterals )
{
if ( s_CubeGroup[0]->a + s_CubeGroup[1]->a >= s_pC1->a + s_pC2->a )
if ( g_CoverInfo.fUseQCost ?
s_CubeGroup[0]->q + s_CubeGroup[1]->q >= s_pC1->q + s_pC2->q :
s_CubeGroup[0]->a + s_CubeGroup[1]->a >= s_pC1->a + s_pC2->a )
// the group increases literals
{ // do not take the last group
@ -441,8 +445,10 @@ int IterativelyApplyExorLink3( char fDistEnable )
// decide whether to accept this group based on literal count
if ( s_fDecreaseLiterals && s_Gain == 1 )
if ( s_CubeGroup[0]->a + s_CubeGroup[1]->a + s_CubeGroup[2]->a >
s_pC1->a + s_pC2->a + s_ChangeStore.PrevQa ) // the group increases literals
if ( g_CoverInfo.fUseQCost ?
s_CubeGroup[0]->q + s_CubeGroup[1]->q + s_CubeGroup[2]->q > s_pC1->q + s_pC2->q + s_ChangeStore.PrevQq :
s_CubeGroup[0]->a + s_CubeGroup[1]->a + s_CubeGroup[2]->a > s_pC1->a + s_pC2->a + s_ChangeStore.PrevQa
) // the group increases literals
{ // do not take this group
// remember the group
s_GroupBest = s_GroupCounter;
@ -669,6 +675,8 @@ int CheckForCloseCubes( Cube* p, int fAddCube )
s_ChangeStore.p = p;
s_ChangeStore.PrevQa = s_q->a;
s_ChangeStore.PrevPa = p->a;
s_ChangeStore.PrevQq = s_q->q;
s_ChangeStore.PrevPq = p->q;
s_ChangeStore.PrevPz = p->z;
s_ChangeStore.Var = s_DiffVarNum;
s_ChangeStore.Value = s_DiffVarValueQ;
@ -750,6 +758,7 @@ void UndoRecentChanges()
{
ExorVar( p, s_ChangeStore.Var, (varvalue)s_ChangeStore.Value );
p->a = s_ChangeStore.PrevPa;
p->q = s_ChangeStore.PrevPq;
// p->z did not change
}
else // if ( s_ChangeStore.fInput ) // the output has changed

22
src/base/exor/exorUtil.c
View File

@ -108,6 +108,23 @@ int CountLiterals()
return LitCounter;
}
int CountQCost()
// nCubesAlloc is the number of allocated cubes
{
extern int ComputeQCostBits( Cube * p );
Cube* p;
int QCost = 0;
int QCostControl = 0;
for ( p = IterCubeSetStart( ); p; p = IterCubeSetNext() )
{
QCostControl += p->q;
QCost += ComputeQCostBits( p );
}
// if ( QCostControl != QCost )
// printf( "Warning! The recorded number of literals (%d) differs from the actual number (%d)\n", QCostControl, QCost );
return QCost;
}
void WriteTableIntoFile( FILE * pFile )
// nCubesAlloc is the number of allocated cubes
@ -175,13 +192,14 @@ int WriteResultIntoFile( char * pFileName )
TimeStr = asctime( localtime( &ltime ) );
// get the number of literals
g_CoverInfo.nLiteralsAfter = CountLiterals();
g_CoverInfo.QCostAfter = CountQCost();
fprintf( pFile, "# EXORCISM-4 output for command line arguments: " );
fprintf( pFile, "\"-Q %d -V %d\"\n", g_CoverInfo.Quality, g_CoverInfo.Verbosity );
fprintf( pFile, "# Minimization performed %s", TimeStr );
fprintf( pFile, "# Initial statistics: " );
fprintf( pFile, "Cubes = %d Literals = %d\n", g_CoverInfo.nCubesBefore, g_CoverInfo.nLiteralsBefore );
fprintf( pFile, "Cubes = %d Literals = %d QCost = %d\n", g_CoverInfo.nCubesBefore, g_CoverInfo.nLiteralsBefore, g_CoverInfo.QCostBefore );
fprintf( pFile, "# Final statistics: " );
fprintf( pFile, "Cubes = %d Literals = %d\n", g_CoverInfo.nCubesInUse, g_CoverInfo.nLiteralsAfter );
fprintf( pFile, "Cubes = %d Literals = %d QCost = %d\n", g_CoverInfo.nCubesInUse, g_CoverInfo.nLiteralsAfter, g_CoverInfo.QCostAfter );
fprintf( pFile, "# File reading and reordering time = %.2f sec\n", TICKS_TO_SECONDS(g_CoverInfo.TimeRead) );
fprintf( pFile, "# Starting cover generation time = %.2f sec\n", TICKS_TO_SECONDS(g_CoverInfo.TimeStart) );
fprintf( pFile, "# Pure ESOP minimization time = %.2f sec\n", TICKS_TO_SECONDS(g_CoverInfo.TimeMin) );