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

Corner-case bug fix in SAT-based sim info generation.

This commit is contained in:
Alan Mishchenko 2020-04-07 13:04:02 -07:00
parent 71fd9165e3
commit 2dfadb9607
1 changed files with 6 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
src/aig/gia/giaSimBase.c
View File

@ -221,20 +221,22 @@ int Gia_ManSimBitPackOne( int nWords, Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsCare
} }
return (int)(i == iPat); return (int)(i == iPat);
} }
Vec_Wrd_t * Gia_ManSimBitPacking( Gia_Man_t * p, Vec_Int_t * vCexStore, int nCexes ) Vec_Wrd_t * Gia_ManSimBitPacking( Gia_Man_t * p, Vec_Int_t * vCexStore, int nCexes, int nUnDecs )
{ {
int c, iCur = 0, iPat = 0; int c, iCur = 0, iPat = 0;
int nWordsMax = Abc_Bit6WordNum( nCexes ); int nWordsMax = Abc_Bit6WordNum( nCexes );
Vec_Wrd_t * vSimsIn = Vec_WrdStartRandom( Gia_ManCiNum(p) * nWordsMax ); Vec_Wrd_t * vSimsIn = Vec_WrdStartRandom( Gia_ManCiNum(p) * nWordsMax );
Vec_Wrd_t * vSimsCare = Vec_WrdStart( Gia_ManCiNum(p) * nWordsMax ); Vec_Wrd_t * vSimsCare = Vec_WrdStart( Gia_ManCiNum(p) * nWordsMax );
Vec_Wrd_t * vSimsRes = NULL; Vec_Wrd_t * vSimsRes = NULL;
for ( c = 0; c < nCexes; c++ ) for ( c = 0; c < nCexes + nUnDecs; c++ )
{ {
int Out = Vec_IntEntry( vCexStore, iCur++ ); int Out = Vec_IntEntry( vCexStore, iCur++ );
int Size = Vec_IntEntry( vCexStore, iCur++ ); int Size = Vec_IntEntry( vCexStore, iCur++ );
if ( Size == -1 )
continue;
iPat += Gia_ManSimBitPackOne( nWordsMax, vSimsIn, vSimsCare, iPat, Vec_IntEntryP(vCexStore, iCur), Size ); iPat += Gia_ManSimBitPackOne( nWordsMax, vSimsIn, vSimsCare, iPat, Vec_IntEntryP(vCexStore, iCur), Size );
iCur += Size; iCur += Size;
assert( iPat <= nCexes ); assert( iPat <= nCexes + nUnDecs );
Out = 0; Out = 0;
} }
printf( "Compressed %d CEXes into %d test patterns.\n", nCexes, iPat ); printf( "Compressed %d CEXes into %d test patterns.\n", nCexes, iPat );
@ -430,7 +432,7 @@ void Gia_ManSimPat( Gia_Man_t * p, int nWords0, int fVerbose )
printf( "There are no counter-examples. No need for more simulation.\n" ); printf( "There are no counter-examples. No need for more simulation.\n" );
else else
{ {
vSimsIn = Gia_ManSimBitPacking( p, vCexStore, Counts[1] ); vSimsIn = Gia_ManSimBitPacking( p, vCexStore, Counts[1], Counts[0] );
Vec_WrdFreeP( &p->vSimsPi ); Vec_WrdFreeP( &p->vSimsPi );
p->vSimsPi = vSimsIn; p->vSimsPi = vSimsIn;
Gia_ManSimProfile( p ); Gia_ManSimProfile( p );