Improving simulation patterns by local search.

This commit is contained in:
Alan Mishchenko 2020-04-17 18:56:12 -07:00
parent 5f163c0152
commit d0e316df5b
3 changed files with 528 additions and 38 deletions

View File

@ -1653,9 +1653,12 @@ Vec_Int_t * Cbs2_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvS
p->timeTotal = Abc_Clock() - clkTotal;
if ( fVerbose )
Cbs2_ManSatPrintStats( p );
if ( fVerbose )
{
// printf( "RecCalls = %8d. RecClause = %8d. RecNonChro = %8d.\n", p->nRecCall, p->nRecClause, p->nRecNonChro );
printf( "Prop1 = %d. Prop2 = %d. Prop3 = %d. ClaConf = %d. FailJ = %d. FailC = %d. ", p->nPropCalls[0], p->nPropCalls[1], p->nPropCalls[2], p->nClauseConf, p->nFails[0], p->nFails[1] );
Abc_PrintTime( 1, "JFront", p->timeJFront );
}
Cbs2_ManStop( p );
*pvStatus = vStatus;

View File

@ -239,11 +239,10 @@ Vec_Wrd_t * Gia_ManSimBitPacking( Gia_Man_t * p, Vec_Int_t * vCexStore, int nCex
assert( iPat <= nCexes + nUnDecs );
Out = 0;
}
printf( "Compressed %d CEXes into %d test patterns.\n", nCexes, iPat );
assert( iCur == Vec_IntSize(vCexStore) );
vSimsRes = Gia_ManSimCombine( Gia_ManCiNum(p), p->vSimsPi, vSimsIn, Abc_Bit6WordNum(iPat+1) );
printf( "Combined %d words of the original info with %d words of additional info.\n",
Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p), Abc_Bit6WordNum(iPat+1) );
printf( "Compressed %d CEXes into %d patterns and added %d words to available %d words.\n",
nCexes, iPat, Abc_Bit6WordNum(iPat+1), Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p) );
Vec_WrdFree( vSimsIn );
Vec_WrdFree( vSimsCare );
return vSimsRes;
@ -344,7 +343,7 @@ void Gia_ManSimPatWrite( char * pFileName, Vec_Wrd_t * vSimsIn, int nWords )
for ( i = 0; i < nNodes; i++ )
Gia_ManSimPatWriteOne( pFile, Vec_WrdEntryP(vSimsIn, i*nWords), nWords );
fclose( pFile );
printf( "Written %d words of simulation data.\n", nWords );
printf( "Written %d words of simulation data into file \"%s\".\n", nWords, pFileName );
}
int Gia_ManSimPatReadOne( char c )
{
@ -405,11 +404,11 @@ void Gia_ManSimProfile( Gia_Man_t * pGia )
Vec_Wrd_t * vSims = Gia_ManSimPatSim( pGia );
int nWords = Vec_WrdSize(vSims) / Gia_ManObjNum(pGia);
int nC0s = 0, nC1s = 0, nUnique = Gia_ManSimPatHashPatterns( pGia, nWords, vSims, &nC0s, &nC1s );
printf( "Simulating %d words leads to %d unique objects (%.2f %% out of %d), Const0 = %d. Const1 = %d.\n",
nWords, nUnique, 100.0*nUnique/Gia_ManCandNum(pGia), Gia_ManCandNum(pGia), nC0s, nC1s );
printf( "Simulating %d patterns leads to %d unique objects (%.2f %% out of %d), Const0 = %d. Const1 = %d.\n",
64*nWords, nUnique, 100.0*nUnique/Gia_ManCandNum(pGia), Gia_ManCandNum(pGia), nC0s, nC1s );
Vec_WrdFree( vSims );
}
void Gia_ManSimPat( Gia_Man_t * p, int nWords0, int fVerbose )
void Gia_ManPatSatImprove( Gia_Man_t * p, int nWords0, int fVerbose )
{
extern Vec_Int_t * Cbs2_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStatus, int fVerbose );
int i, Status, Counts[3] = {0};
@ -418,7 +417,7 @@ void Gia_ManSimPat( Gia_Man_t * p, int nWords0, int fVerbose )
Vec_Str_t * vStatus = NULL;
Vec_Int_t * vCexStore = NULL;
Vec_Wrd_t * vSims = Gia_ManSimPatSim( p );
Gia_ManSimProfile( p );
//Gia_ManSimProfile( p );
pGia = Gia_ManSimPatGenMiter( p, vSims );
vCexStore = Cbs2_ManSolveMiterNc( pGia, 1000, &vStatus, 0 );
Gia_ManStop( pGia );
@ -427,7 +426,8 @@ void Gia_ManSimPat( Gia_Man_t * p, int nWords0, int fVerbose )
assert( Status >= -1 && Status <= 1 );
Counts[Status+1]++;
}
printf( "Total = %d : SAT = %d. UNSAT = %d. UNDEC = %d.\n", Counts[1]+Counts[2]+Counts[0], Counts[1], Counts[2], Counts[0] );
if ( fVerbose )
printf( "Total = %d : SAT = %d. UNSAT = %d. UNDEC = %d.\n", Counts[1]+Counts[2]+Counts[0], Counts[1], Counts[2], Counts[0] );
if ( Counts[1] == 0 )
printf( "There are no counter-examples. No need for more simulation.\n" );
else
@ -435,7 +435,7 @@ void Gia_ManSimPat( Gia_Man_t * p, int nWords0, int fVerbose )
vSimsIn = Gia_ManSimBitPacking( p, vCexStore, Counts[1], Counts[0] );
Vec_WrdFreeP( &p->vSimsPi );
p->vSimsPi = vSimsIn;
Gia_ManSimProfile( p );
//Gia_ManSimProfile( p );
}
Vec_StrFree( vStatus );
Vec_IntFree( vCexStore );
@ -1643,6 +1643,392 @@ Vec_Int_t * Gia_RsbSetFind( word * pOffSet, word * pOnSet, Vec_Wrd_t * vSims, in
return vObjs;
}
/**Function*************************************************************
Synopsis [Improving quality of simulation patterns.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Gia_SimQualityOne( Gia_Man_t * p, Vec_Int_t * vPat, int fPoOnly )
{
int i, Id, Value, nWords = Abc_Bit6WordNum( 1+Gia_ManCiNum(p) );
Vec_Wrd_t * vTemp, * vSims, * vSimsPi = Vec_WrdStart( Gia_ManCiNum(p) * nWords );
Vec_Int_t * vRes;
assert( Vec_IntSize(vPat) == Gia_ManCiNum(p) );
Vec_IntForEachEntry( vPat, Value, i )
{
word * pSim = Vec_WrdEntryP( vSimsPi, i*nWords );
if ( Value )
Abc_TtFill( pSim, nWords );
Abc_TtXorBit( pSim, i+1 );
}
vTemp = p->vSimsPi;
p->vSimsPi = vSimsPi;
vSims = Gia_ManSimPatSim( p );
p->vSimsPi = vTemp;
if ( fPoOnly )
{
vRes = Vec_IntStart( Gia_ManCoNum(p) );
Gia_ManForEachCoId( p, Id, i )
{
word * pSim = Vec_WrdEntryP( vSims, Id*nWords );
if ( pSim[0] & 1 )
Abc_TtNot( pSim, nWords );
Vec_IntWriteEntry( vRes, i, Abc_TtCountOnesVec(pSim, nWords) );
}
assert( Vec_IntSize(vRes) == Gia_ManCoNum(p) );
}
else
{
vRes = Vec_IntStart( Gia_ManObjNum(p) );
Gia_ManForEachAndId( p, Id )
{
word * pSim = Vec_WrdEntryP( vSims, Id*nWords );
if ( pSim[0] & 1 )
Abc_TtNot( pSim, nWords );
Vec_IntWriteEntry( vRes, Id, Abc_TtCountOnesVec(pSim, nWords) );
}
assert( Vec_IntSize(vRes) == Gia_ManObjNum(p) );
}
Vec_WrdFree( vSims );
Vec_WrdFree( vSimsPi );
return vRes;
}
void Gia_SimQualityTest( Gia_Man_t * p )
{
Vec_Int_t * vPat, * vRes;
int k, m, nMints = (1 << Gia_ManCiNum(p));
assert( Gia_ManCiNum(p) <= 10 );
for ( m = 0; m < nMints; m++ )
{
printf( "%d : ", m );
Extra_PrintBinary( stdout, (unsigned*)&m, Gia_ManCiNum(p) );
printf( " " );
vPat = Vec_IntAlloc( Gia_ManCiNum(p) );
for ( k = 0; k < Gia_ManCiNum(p); k++ )
Vec_IntPush( vPat, (m >> k) & 1 );
vRes = Gia_SimQualityOne( p, vPat, 1 );
printf( "%d ", Vec_IntSum(vRes) );
Vec_IntFree( vRes );
Vec_IntFree( vPat );
printf( "\n" );
}
}
Vec_Int_t * Gia_SimGenerateStats( Gia_Man_t * p )
{
Vec_Int_t * vTotal = Vec_IntStart( Gia_ManObjNum(p) );
Vec_Int_t * vRes, * vPat;
int i, k, Value;
Abc_Random(1);
for ( i = 0; i < 1000; i++ )
{
vPat = Vec_IntAlloc( Gia_ManCiNum(p) );
for ( k = 0; k < Gia_ManCiNum(p); k++ )
Vec_IntPush( vPat, Abc_Random(0) & 1 );
vRes = Gia_SimQualityOne( p, vPat, 0 );
assert( Vec_IntSize(vRes) == Gia_ManObjNum(p) );
Vec_IntForEachEntry( vRes, Value, k )
Vec_IntAddToEntry( vTotal, k, Value );
Vec_IntFree( vRes );
Vec_IntFree( vPat );
}
//Vec_IntPrint( vTotal );
return vTotal;
}
double Gia_SimComputeScore( Gia_Man_t * p, Vec_Int_t * vTotal, Vec_Int_t * vThis )
{
double TotalScore = 0;
int i, Total, This;
assert( Vec_IntSize(vTotal) == Vec_IntSize(vThis) );
Vec_IntForEachEntryTwo( vTotal, vThis, Total, This, i )
{
if ( Total == 0 )
Total = 1;
TotalScore += 1000.0*This/Total;
}
return TotalScore == 0 ? 1.0 : TotalScore/Gia_ManAndNum(p);
}
int Gia_SimQualityPatternsMax( Gia_Man_t * p, Vec_Int_t * vPat, int Iter, int fVerbose, Vec_Int_t * vStats )
{
int k, MaxIn = -1;
Vec_Int_t * vTries = Vec_IntAlloc( 100 );
Vec_Int_t * vRes = Gia_SimQualityOne( p, vPat, 0 );
double Value, InitValue, MaxValue = InitValue = Gia_SimComputeScore( p, vStats, vRes );
Vec_IntFree( vRes );
if ( fVerbose )
printf( "Iter %5d : Init = %6.3f ", Iter, InitValue );
for ( k = 0; k < Gia_ManCiNum(p); k++ )
{
Vec_IntArray(vPat)[k] ^= 1;
//Vec_IntPrint( vPat );
vRes = Gia_SimQualityOne( p, vPat, 0 );
Value = Gia_SimComputeScore( p, vStats, vRes );
if ( MaxValue <= Value )
{
if ( MaxValue < Value )
Vec_IntClear( vTries );
Vec_IntPush( vTries, k );
MaxValue = Value;
MaxIn = k;
}
Vec_IntFree( vRes );
Vec_IntArray(vPat)[k] ^= 1;
}
MaxIn = Vec_IntSize(vTries) ? Vec_IntEntry( vTries, rand()%Vec_IntSize(vTries) ) : -1;
if ( fVerbose )
{
printf( "Final = %6.3f Ratio = %4.2f Tries = %5d ", MaxValue, MaxValue/InitValue, Vec_IntSize(vTries) );
printf( "Choosing %5d\r", MaxIn );
}
Vec_IntFree( vTries );
return MaxIn;
}
Vec_Int_t * Gia_ManPatCollectOne( Gia_Man_t * p, Vec_Wrd_t * vPatterns, int n, int nWords )
{
Vec_Int_t * vPat = Vec_IntAlloc( Gia_ManCiNum(p) ); int k;
for ( k = 0; k < Gia_ManCiNum(p); k++ )
Vec_IntPush( vPat, Abc_TtGetBit( Vec_WrdEntryP(vPatterns, k*nWords), n ) );
return vPat;
}
void Gia_ManPatUpdateOne( Gia_Man_t * p, Vec_Wrd_t * vPatterns, int n, int nWords, Vec_Int_t * vPat )
{
int k, Value;
Vec_IntForEachEntry( vPat, Value, k )
{
word * pSim = Vec_WrdEntryP( vPatterns, k*nWords );
if ( Abc_TtGetBit(pSim, n) != Value )
Abc_TtXorBit( pSim, n );
}
}
void Gia_ManPatDistImprove( Gia_Man_t * p, int fVerbose )
{
int n, k, nWords = Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p);
double InitValue, InitTotal = 0, FinalValue, FinalTotal = 0;
Vec_Int_t * vPat, * vRes, * vStats = Gia_SimGenerateStats( p );
Vec_Wrd_t * vPatterns = p->vSimsPi; p->vSimsPi = NULL;
Abc_Random(1);
for ( n = 0; n < 64*nWords; n++ )
{
abctime clk = Abc_Clock();
// if ( n == 32 )
// break;
vPat = Gia_ManPatCollectOne( p, vPatterns, n, nWords );
vRes = Gia_SimQualityOne( p, vPat, 0 );
InitValue = Gia_SimComputeScore(p, vStats, vRes);
InitTotal += InitValue;
Vec_IntFree( vRes );
for ( k = 0; k < 100; k++ )
{
int MaxIn = Gia_SimQualityPatternsMax( p, vPat, k, fVerbose, vStats );
if ( MaxIn == -1 )
break;
assert( MaxIn >= 0 && MaxIn < Gia_ManCiNum(p) );
Vec_IntArray(vPat)[MaxIn] ^= 1;
}
//Vec_IntPrint( vPat );
vRes = Gia_SimQualityOne( p, vPat, 0 );
FinalValue = Gia_SimComputeScore(p, vStats, vRes);
FinalTotal += FinalValue;
Vec_IntFree( vRes );
if ( fVerbose )
{
printf( "Pat %5d : Tries = %5d InitValue = %6.3f FinalValue = %6.3f Ratio = %4.2f ",
n, k, InitValue, FinalValue, FinalValue/InitValue );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
Gia_ManPatUpdateOne( p, vPatterns, n, nWords, vPat );
Vec_IntFree( vPat );
}
Vec_IntFree( vStats );
if ( fVerbose )
printf( "\n" );
printf( "Improved %d patterns with average init value %.2f and average final value %.2f.\n",
64*nWords, 1.0*InitTotal/(64*nWords), 1.0*FinalTotal/(64*nWords) );
p->vSimsPi = vPatterns;
}
/**Function*************************************************************
Synopsis [Improving quality of simulation patterns.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Gia_SimCollectRare( Gia_Man_t * p, Vec_Wrd_t * vPatterns, int RareLimit )
{
Vec_Int_t * vRareCounts = Vec_IntAlloc( 100 ); // (node, rare_count) pairs
int Id, nWords = Vec_WrdSize(vPatterns) / Gia_ManCiNum(p), TotalBits = 64*nWords;
Vec_Wrd_t * vSims, * vTemp = p->vSimsPi;
assert( Vec_WrdSize(vPatterns) % Gia_ManCiNum(p) == 0 );
p->vSimsPi = vPatterns;
vSims = Gia_ManSimPatSim( p );
p->vSimsPi = vTemp;
Gia_ManForEachAndId( p, Id )
{
word * pSim = Vec_WrdEntryP( vSims, Id*nWords );
int Count = Abc_TtCountOnesVec( pSim, nWords );
int fRareOne = Count < TotalBits/2; // fRareOne is 1 if rare value is 1
int CountRare = fRareOne ? Count : TotalBits - Count;
assert( CountRare <= TotalBits/2 );
if ( CountRare <= RareLimit )
Vec_IntPushTwo( vRareCounts, Abc_Var2Lit(Id, fRareOne), CountRare );
}
Vec_WrdFree( vSims );
return vRareCounts;
}
Vec_Flt_t * Gia_SimQualityImpact( Gia_Man_t * p, Vec_Int_t * vPat, Vec_Int_t * vRareCounts )
{
Vec_Flt_t * vQuoIncs = Vec_FltStart( Gia_ManCiNum(p) );
int nWordsNew = Abc_Bit6WordNum( 1+Gia_ManCiNum(p) );
Vec_Wrd_t * vSimsPiNew = Vec_WrdStart( Gia_ManCiNum(p) * nWordsNew );
Vec_Wrd_t * vTemp, * vSims;
int i, k, Value, RareLit, RareCount;
assert( Vec_IntSize(vPat) == Gia_ManCiNum(p) );
Vec_IntForEachEntry( vPat, Value, i )
{
word * pSim = Vec_WrdEntryP( vSimsPiNew, i*nWordsNew );
if ( Value )
Abc_TtFill( pSim, nWordsNew );
Abc_TtXorBit( pSim, i+1 );
}
vTemp = p->vSimsPi;
p->vSimsPi = vSimsPiNew;
vSims = Gia_ManSimPatSim( p );
p->vSimsPi = vTemp;
Vec_IntForEachEntryDouble( vRareCounts, RareLit, RareCount, i )
{
float Incrm = (float)1.0/(RareCount+1);
int RareObj = Abc_Lit2Var(RareLit);
int RareVal = Abc_LitIsCompl(RareLit);
word * pSim = Vec_WrdEntryP( vSims, RareObj*nWordsNew );
int OrigVal = pSim[0] & 1;
if ( OrigVal )
Abc_TtNot( pSim, nWordsNew );
for ( k = 0; k < Gia_ManCiNum(p); k++ )
if ( Abc_TtGetBit(pSim, k+1) ) // value changed
Vec_FltAddToEntry( vQuoIncs, k, OrigVal != RareVal ? Incrm : -Incrm );
}
Vec_WrdFree( vSims );
Vec_WrdFree( vSimsPiNew );
return vQuoIncs;
}
Vec_Int_t * Gia_SimCollectBest( Vec_Flt_t * vQuo )
{
Vec_Int_t * vRes; int i;
float Value, ValueMax = Vec_FltFindMax( vQuo );
if ( ValueMax <= 0 )
return NULL;
vRes = Vec_IntAlloc( 100 ); // variables with max quo
Vec_FltForEachEntry( vQuo, Value, i )
if ( Value == ValueMax )
Vec_IntPush( vRes, i );
return vRes;
}
float Gia_ManPatGetQuo( Gia_Man_t * p, Vec_Int_t * vRareCounts, Vec_Wrd_t * vSims, int n, int nWords )
{
float Quality = 0;
int RareLit, RareCount, i;
assert( Vec_WrdSize(vSims) == Gia_ManObjNum(p) );
Vec_IntForEachEntryDouble( vRareCounts, RareLit, RareCount, i )
{
float Incrm = (float)1.0/(RareCount+1);
int RareObj = Abc_Lit2Var(RareLit);
int RareVal = Abc_LitIsCompl(RareLit);
word * pSim = Vec_WrdEntryP( vSims, RareObj*nWords );
if ( Abc_TtGetBit(pSim, n) == RareVal )
Quality += Incrm;
}
return Quality;
}
float Gia_ManPatGetTotalQuo( Gia_Man_t * p, int RareLimit, Vec_Wrd_t * vPatterns, int nWords )
{
float Total = 0; int n;
Vec_Int_t * vRareCounts = Gia_SimCollectRare( p, vPatterns, RareLimit );
Vec_Wrd_t * vSims, * vTemp = p->vSimsPi;
p->vSimsPi = vPatterns;
vSims = Gia_ManSimPatSim( p );
p->vSimsPi = vTemp;
for ( n = 0; n < 64*nWords; n++ )
Total += Gia_ManPatGetQuo( p, vRareCounts, vSims, n, nWords );
Vec_IntFree( vRareCounts );
Vec_WrdFree( vSims );
return Total;
}
float Gia_ManPatGetOneQuo( Gia_Man_t * p, int RareLimit, Vec_Wrd_t * vPatterns, int nWords, int n )
{
float Total = 0;
Vec_Int_t * vRareCounts = Gia_SimCollectRare( p, vPatterns, RareLimit );
Vec_Wrd_t * vSims, * vTemp = p->vSimsPi;
p->vSimsPi = vPatterns;
vSims = Gia_ManSimPatSim( p );
p->vSimsPi = vTemp;
Total += Gia_ManPatGetQuo( p, vRareCounts, vSims, n, nWords );
Vec_IntFree( vRareCounts );
Vec_WrdFree( vSims );
return Total;
}
void Gia_ManPatRareImprove( Gia_Man_t * p, int RareLimit, int fVerbose )
{
abctime clk = Abc_Clock();
float FinalTotal, InitTotal;
int n, nRares = 0, nChanges = 0, nWords = Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p);
Vec_Wrd_t * vPatterns = p->vSimsPi; p->vSimsPi = NULL;
InitTotal = Gia_ManPatGetTotalQuo( p, RareLimit, vPatterns, nWords );
for ( n = 0; n < 64*nWords; n++ )
{
abctime clk = Abc_Clock();
Vec_Int_t * vRareCounts = Gia_SimCollectRare( p, vPatterns, RareLimit );
Vec_Int_t * vPat = Gia_ManPatCollectOne( p, vPatterns, n, nWords );
Vec_Flt_t * vQuoIncs = Gia_SimQualityImpact( p, vPat, vRareCounts );
Vec_Int_t * vBest = Gia_SimCollectBest( vQuoIncs );
if ( fVerbose )
{
float PatQuo = Gia_ManPatGetOneQuo( p, RareLimit, vPatterns, nWords, n );
printf( "Pat %5d : Rare = %4d Cands = %3d Value = %8.3f Change = %8.3f ",
n, Vec_IntSize(vRareCounts)/2, vBest ? Vec_IntSize(vBest) : 0,
PatQuo, vBest ? Vec_FltEntry(vQuoIncs, Vec_IntEntry(vBest,0)) : 0 );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
if ( vBest != NULL )
{
int VarBest = Vec_IntEntry( vBest, rand()%Vec_IntSize(vBest) );
Abc_TtXorBit( Vec_WrdEntryP(vPatterns, VarBest*nWords), n );
nChanges++;
}
nRares = Vec_IntSize(vRareCounts)/2;
Vec_IntFree( vRareCounts );
Vec_IntFree( vPat );
Vec_FltFree( vQuoIncs );
Vec_IntFreeP( &vBest );
}
if ( fVerbose )
printf( "\n" );
FinalTotal = Gia_ManPatGetTotalQuo( p, RareLimit, vPatterns, nWords );
p->vSimsPi = vPatterns;
printf( "Improved %d out of %d patterns using %d rare nodes: %.2f -> %.2f. ",
nChanges, 64*nWords, nRares, InitTotal, FinalTotal );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

View File

@ -416,7 +416,8 @@ static int Abc_CommandAbc9MLGen ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandAbc9MLTest ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9ReadSim ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9WriteSim ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9SimPat ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9PrintSim ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9GenSim ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9SimRsb ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Resim ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9SpecI ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -1131,9 +1132,10 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&sim3", Abc_CommandAbc9Sim3, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&mlgen", Abc_CommandAbc9MLGen, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&mltest", Abc_CommandAbc9MLTest, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&read_sim", Abc_CommandAbc9ReadSim, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&write_sim", Abc_CommandAbc9WriteSim, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&simpat", Abc_CommandAbc9SimPat, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&sim_read", Abc_CommandAbc9ReadSim, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&sim_write", Abc_CommandAbc9WriteSim, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&sim_print", Abc_CommandAbc9PrintSim, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&sim_gen", Abc_CommandAbc9GenSim, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&simrsb", Abc_CommandAbc9SimRsb, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&resim", Abc_CommandAbc9Resim, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&speci", Abc_CommandAbc9SpecI, 0 );
@ -32832,13 +32834,6 @@ int Abc_CommandAbc9ReadSim( Abc_Frame_t * pAbc, int argc, char ** argv )
}
pArgvNew = argv + globalUtilOptind;
nArgcNew = argc - globalUtilOptind;
if ( nArgcNew == 0 )
{
Gia_ManRandom( 1 );
pAbc->pGia->vSimsPi = Vec_WrdStartRandom( Gia_ManCiNum(pAbc->pGia) * nWords );
printf( "Generated %d random patterns (%d 64-bit words) for each input of the AIG.\n", 64*nWords, nWords );
return 0;
}
if ( nArgcNew != 1 )
{
Abc_Print( -1, "File name is not given on the command line.\n" );
@ -32875,7 +32870,7 @@ int Abc_CommandAbc9ReadSim( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: &read_sim [-W num] [-ovh] <file>\n" );
Abc_Print( -2, "usage: &sim_read [-W num] [-ovh] <file>\n" );
Abc_Print( -2, "\t reads simulation patterns from file\n" );
Abc_Print( -2, "\t-W num : the number of words to simulate [default = %d]\n", nWords );
Abc_Print( -2, "\t-o : toggle reading output information [default = %s]\n", fOutputs? "yes": "no" );
@ -32954,7 +32949,7 @@ int Abc_CommandAbc9WriteSim( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: &write_sim [-vh] <file>\n" );
Abc_Print( -2, "usage: &sim_write [-vh] <file>\n" );
Abc_Print( -2, "\t writes simulation patterns into a file\n" );
Abc_Print( -2, "\t-o : toggle writing output information [default = %s]\n", fOutputs? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
@ -32974,12 +32969,69 @@ usage:
SeeAlso []
***********************************************************************/
int Abc_CommandAbc9SimPat( Abc_Frame_t * pAbc, int argc, char ** argv )
int Abc_CommandAbc9PrintSim( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern void Gia_ManSimPat( Gia_Man_t * pGia, int nWords, int fVerbose );
int c, nWords = 4, fVerbose = 0;
extern void Gia_ManSimProfile( Gia_Man_t * pGia );
int c, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Wvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
{
switch ( c )
{
case 'v':
fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9PrintSim(): There is no AIG.\n" );
return 1;
}
if ( Gia_ManRegNum(pAbc->pGia) > 0 )
{
Abc_Print( -1, "Abc_CommandAbc9PrintSim(): This command works only for combinational AIGs.\n" );
return 0;
}
if ( pAbc->pGia->vSimsPi == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9PrintSim(): Simulation patterns are not defined.\n" );
return 0;
}
Gia_ManSimProfile( pAbc->pGia );
return 0;
usage:
Abc_Print( -2, "usage: &sim_print [-vh]\n" );
Abc_Print( -2, "\t writes simulation patterns into a file\n" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandAbc9GenSim( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern void Gia_ManPatSatImprove( Gia_Man_t * pGia, int nWords, int fVerbose );
extern void Gia_ManPatDistImprove( Gia_Man_t * p, int fVerbose );
extern void Gia_ManPatRareImprove( Gia_Man_t * p, int RareLimit, int fVerbose );
int c, nWords = 4, nRare = -1, fDist = 0, fSatBased = 0, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "WRsdvh" ) ) != EOF )
{
switch ( c )
{
@ -32994,6 +33046,23 @@ int Abc_CommandAbc9SimPat( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nWords < 0 )
goto usage;
break;
case 'R':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" );
goto usage;
}
nRare = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nRare < 0 )
goto usage;
break;
case 's':
fSatBased ^= 1;
break;
case 'd':
fDist ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
@ -33005,27 +33074,59 @@ int Abc_CommandAbc9SimPat( Abc_Frame_t * pAbc, int argc, char ** argv )
}
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9SimPat(): There is no AIG.\n" );
Abc_Print( -1, "Abc_CommandAbc9GenSim(): There is no AIG.\n" );
return 1;
}
if ( Gia_ManRegNum(pAbc->pGia) > 0 )
{
Abc_Print( -1, "Abc_CommandAbc9SimPat(): This command works only for combinational AIGs.\n" );
Abc_Print( -1, "Abc_CommandAbc9GenSim(): This command works only for combinational AIGs.\n" );
return 0;
}
if ( pAbc->pGia->vSimsPi == NULL )
if ( fSatBased )
{
Abc_Print( -1, "Abc_CommandAbc9SimPat(): Does not have simulation information available.\n" );
return 0;
if ( pAbc->pGia->vSimsPi == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9GenSim(): Does not have simulation information available.\n" );
return 0;
}
Gia_ManPatSatImprove( pAbc->pGia, nWords, fVerbose );
}
Gia_ManSimPat( pAbc->pGia, nWords, fVerbose );
else if ( fDist )
{
if ( pAbc->pGia->vSimsPi == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9GenSim(): Does not have simulation information available.\n" );
return 0;
}
Gia_ManPatDistImprove( pAbc->pGia, fVerbose );
}
else if ( nRare >= 0 )
{
if ( pAbc->pGia->vSimsPi == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9GenSim(): Does not have simulation information available.\n" );
return 0;
}
Gia_ManPatRareImprove( pAbc->pGia, nRare, fVerbose );
}
else
{
Abc_Random(1);
Vec_WrdFreeP( &pAbc->pGia->vSimsPi );
pAbc->pGia->vSimsPi = Vec_WrdStartRandom( Gia_ManCiNum(pAbc->pGia) * nWords );
printf( "Generated %d random patterns (%d 64-bit data words) for each input of the AIG.\n", 64*nWords, nWords );
}
Gia_ManSimProfile( pAbc->pGia );
return 0;
usage:
Abc_Print( -2, "usage: &simpat [-W num] [-vh]\n" );
Abc_Print( -2, "\t performs simulation of the AIG\n" );
Abc_Print( -2, "\t-W num : the number of frames to simulate [default = %d]\n", nWords );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "usage: &sim_gen [-WR num] [-sdvh]\n" );
Abc_Print( -2, "\t generates random simulation patterns\n" );
Abc_Print( -2, "\t-W num : the number of 64-bit words of simulation info [default = %d]\n", nWords );
Abc_Print( -2, "\t-R num : the rarity parameter used to define scope [default = %d]\n", nRare );
Abc_Print( -2, "\t-s : toggle using SAT-based improvement of available patterns [default = %s]\n", fSatBased? "yes": "no" );
Abc_Print( -2, "\t-d : toggle using one improvement of available patterns [default = %s]\n", fDist? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
@ -47689,7 +47790,7 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
// return 1;
// }
// Abc_FrameUpdateGia( pAbc, Abc_Procedure(pAbc->pGia) );
//Gia_ManStructExperiment( pAbc->pGia );
// Gia_SimQualityTest( pAbc->pGia );
return 0;
usage:
Abc_Print( -2, "usage: &test [-FW num] [-svh]\n" );