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

Exploring other ways of CEX writing.

This commit is contained in:
Alan Mishchenko 2019-01-21 14:57:05 -08:00
parent d4ce4cc982
commit b3d81b5f76
12 changed files with 96 additions and 18 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/aig/gia/gia.h
View File

@ -1313,7 +1313,7 @@ extern Gia_Man_t * Gia_ManDupDfsClasses( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManDupTopAnd( Gia_Man_t * p, int fVerbose );
extern Gia_Man_t * Gia_ManMiter( Gia_Man_t * pAig0, Gia_Man_t * pAig1, int nInsDup, int fDualOut, int fSeq, int fImplic, int fVerbose );
extern Gia_Man_t * Gia_ManDupAndOr( Gia_Man_t * p, int nOuts, int fUseOr, int fCompl );
extern Gia_Man_t * Gia_ManDupZeroUndc( Gia_Man_t * p, char * pInit, int fGiaSimple, int fVerbose );
extern Gia_Man_t * Gia_ManDupZeroUndc( Gia_Man_t * p, char * pInit, int nNewPis, int fGiaSimple, int fVerbose );
extern Gia_Man_t * Gia_ManMiter2( Gia_Man_t * p, char * pInit, int fVerbose );
extern Gia_Man_t * Gia_ManTransformMiter( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManTransformMiter2( Gia_Man_t * p );

2
src/aig/gia/giaAiger.c
View File

@ -848,7 +848,7 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fGiaSi
}
}
pInit[i] = 0;
pNew = Gia_ManDupZeroUndc( pTemp = pNew, pInit, fGiaSimple, 1 );
pNew = Gia_ManDupZeroUndc( pTemp = pNew, pInit, 0, fGiaSimple, 1 );
pNew->nConstrs = pTemp->nConstrs; pTemp->nConstrs = 0;
Gia_ManStop( pTemp );
ABC_FREE( pInit );

7
src/aig/gia/giaDup.c
View File

@ -3047,7 +3047,7 @@ Gia_Man_t * Gia_ManTransformDualOutput( Gia_Man_t * p )
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManDupZeroUndc( Gia_Man_t * p, char * pInit, int fGiaSimple, int fVerbose )
Gia_Man_t * Gia_ManDupZeroUndc( Gia_Man_t * p, char * pInit, int nNewPis, int fGiaSimple, int fVerbose )
{
Gia_Man_t * pNew;
Gia_Obj_t * pObj;
@ -3072,6 +3072,9 @@ Gia_Man_t * Gia_ManDupZeroUndc( Gia_Man_t * p, char * pInit, int fGiaSimple, int
// create additional primary inputs
for ( i = Gia_ManPiNum(p); i < CountPis; i++ )
Gia_ManAppendCi( pNew );
// create additional primary inputs
for ( i = 0; i < nNewPis; i++ )
Gia_ManAppendCi( pNew );
// create flop outputs
Gia_ManForEachRo( p, pObj, i )
pObj->Value = Gia_ManAppendCi( pNew );
@ -3137,7 +3140,7 @@ Gia_Man_t * Gia_ManMiter2( Gia_Man_t * pStart, char * pInit, int fVerbose )
for ( i = 0; i < Gia_ManPiNum(pStart); i++ )
assert( pInit[i] == 'x' || pInit[i] == 'X' );
// normalize the manager
pUndc = Gia_ManDupZeroUndc( pStart, pInit + Gia_ManPiNum(pStart), 0, fVerbose );
pUndc = Gia_ManDupZeroUndc( pStart, pInit + Gia_ManPiNum(pStart), 0, 0, fVerbose );
// create new init string
pInitNew = ABC_ALLOC( char, Gia_ManPiNum(pUndc)+1 );
for ( i = 0; i < Gia_ManPiNum(pStart); i++ )

2
src/aig/gia/giaRex.c
View File

@ -309,7 +309,7 @@ Gia_Man_t * Gia_ManRex2Gia( char * pStrInit, int fOrder, int fVerbose )
Gia_ManStop( pTemp );
// add initial state
pNew = Gia_ManDupZeroUndc( pTemp = pNew, Vec_StrArray(vInit), 0, 0 );
pNew = Gia_ManDupZeroUndc( pTemp = pNew, Vec_StrArray(vInit), 0, 0, 0 );
Gia_ManStop( pTemp );
Vec_StrFree( vInit );
/*

2
src/aig/gia/giaTim.c
View File

@ -874,7 +874,7 @@ Gia_Man_t * Gia_ManDupCollapse( Gia_Man_t * p, Gia_Man_t * pBoxes, Vec_Int_t * v
pInit[i] = 'X';
}
pInit[i] = 0;
pNew = Gia_ManDupZeroUndc( pTemp = pNew, pInit, 0, 1 );
pNew = Gia_ManDupZeroUndc( pTemp = pNew, pInit, 0, 0, 1 );
pNew->nConstrs = pTemp->nConstrs; pTemp->nConstrs = 0;
Gia_ManStop( pTemp );
ABC_FREE( pInit );

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

@ -29478,7 +29478,7 @@ int Abc_CommandAbc9Get( Abc_Frame_t * pAbc, int argc, char ** argv )
Aig_ManStop( pAig );
// perform undc/zero
pInits = Abc_NtkCollectLatchValuesStr( pAbc->pNtkCur );
pGia = Gia_ManDupZeroUndc( pTemp = pGia, pInits, 0, fVerbose );
pGia = Gia_ManDupZeroUndc( pTemp = pGia, pInits, 0, 0, fVerbose );
Gia_ManStop( pTemp );
ABC_FREE( pInits );
}

2
src/base/cba/cbaBlast.c
View File

@ -1013,7 +1013,7 @@ Gia_Man_t * Cba_NtkBlast( Cba_Ntk_t * p, int fSeq )
{
Gia_ManSetRegNum( pNew, Vec_StrSize(vInit) );
Vec_StrPush( vInit, '\0' );
pNew = Gia_ManDupZeroUndc( pTemp = pNew, Vec_StrArray(vInit), 0, 1 );
pNew = Gia_ManDupZeroUndc( pTemp = pNew, Vec_StrArray(vInit), 0, 0, 1 );
Gia_ManDupRemapLiterals( vBits, pTemp );
Gia_ManStop( pTemp );
Vec_StrFreeP( &vInit );

56
src/base/io/io.c
View File

@ -2317,10 +2317,11 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv )
int forceSeq = 0;
int fAiger = 0;
int fPrintFull = 0;
int fUseFfNames = 0;
int fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "snmueocafvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "snmueocafzvh" ) ) != EOF )
{
switch ( c )
{
@ -2351,6 +2352,9 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv )
case 'f':
fPrintFull ^= 1;
break;
case 'z':
fUseFfNames ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
@ -2444,6 +2448,46 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv )
}
fprintf( pFile, "\n");
fprintf( pFile, "# COUNTEREXAMPLE LENGTH: %u\n", pCex->iFrame+1);
if ( fUseFfNames )
{
int * pValues;
int nXValues = 0, iFlop = 0, iPivotPi = -1;
Abc_NtkForEachPi( pNtk, pObj, iPivotPi )
if ( !strcmp(Abc_ObjName(pObj), "_abc_190121_abc_") )
break;
if ( iPivotPi == Abc_NtkPiNum(pNtk) )
{
fprintf( stdout, "IoCommandWriteCex(): Cannot find special PI required by switch \"-z\".\n" );
return 1;
}
// count X-valued flops
for ( i = iPivotPi+1; i < Abc_NtkPiNum(pNtk); i++ )
if ( Abc_ObjName(Abc_NtkPi(pNtk, i))[0] == 'x' )
nXValues++;
// map X-valued flops into auxiliary PIs
pValues = ABC_FALLOC( int, Abc_NtkPiNum(pNtk) );
for ( i = iPivotPi+1; i < Abc_NtkPiNum(pNtk); i++ )
if ( Abc_ObjName(Abc_NtkPi(pNtk, i))[0] == 'x' )
pValues[i] = iPivotPi - nXValues + iFlop++;
assert( iFlop == nXValues );
// write flop values
for ( i = iPivotPi+1; i < Abc_NtkPiNum(pNtk); i++ )
if ( pValues[i] == -1 )
fprintf( pFile, "%s@0=%c\n", Abc_ObjName(Abc_NtkPi(pNtk, i))+1, Abc_ObjName(Abc_NtkPi(pNtk, i))[0] );
else if ( Abc_InfoHasBit(pCare->pData, pCare->nRegs + pValues[i]) )
fprintf( pFile, "%s@0=%c\n", Abc_ObjName(Abc_NtkPi(pNtk, i))+1, '0'+Abc_InfoHasBit(pCex->pData, pCex->nRegs + pValues[i]) );
ABC_FREE( pValues );
// output PI values (while skipping the minimized ones)
for ( f = 0; f <= pCex->iFrame; f++ )
Abc_NtkForEachPi( pNtk, pObj, i )
{
if ( i == iPivotPi - nXValues ) break;
if ( !pCare || Abc_InfoHasBit(pCare->pData, pCare->nRegs+pCare->nPis*f + i) )
fprintf( pFile, "%s@%d=%c\n", Abc_ObjName(pObj), f, '0'+Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i) );
}
}
else
{
// output flop values (unaffected by the minimization)
Abc_NtkForEachLatch( pNtk, pObj, i )
fprintf( pFile, "%s@0=%c\n", Abc_ObjName(Abc_ObjFanout0(pObj)), '0'+!Abc_LatchIsInit0(pObj) );
@ -2452,6 +2496,7 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv )
Abc_NtkForEachPi( pNtk, pObj, i )
if ( !pCare || Abc_InfoHasBit(pCare->pData, pCare->nRegs+pCare->nPis*f + i) )
fprintf( pFile, "%s@%d=%c\n", Abc_ObjName(pObj), f, '0'+Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i) );
}
Abc_CexFreeP( &pCare );
}
else
@ -2498,7 +2543,7 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv )
return 0;
usage:
fprintf( pAbc->Err, "usage: write_cex [-snmueocfvh] <file>\n" );
fprintf( pAbc->Err, "usage: write_cex [-snmueocfzvh] <file>\n" );
fprintf( pAbc->Err, "\t saves counter-example (CEX) derived by \"sat\", \"iprove\", \"dprove\", etc\n" );
fprintf( pAbc->Err, "\t the output file <file> contains values for each PI in natural order\n" );
fprintf( pAbc->Err, "\t-s : always report a sequential CEX (cycle 0 for comb) [default = %s]\n", forceSeq? "yes": "no" );
@ -2508,9 +2553,10 @@ usage:
fprintf( pAbc->Err, "\t-e : use high-effort SAT-based CEX minimization [default = %s]\n", fHighEffort? "yes": "no" );
fprintf( pAbc->Err, "\t-o : use old CEX minimization algorithm [default = %s]\n", fUseOldMin? "yes": "no" );
fprintf( pAbc->Err, "\t-c : check generated CEX using ternary simulation [default = %s]\n", fCheckCex? "yes": "no" );
fprintf( pAbc->Err, "\t-a : print cex in AIGER 1.9 format [default = %s].\n", fAiger? "yes": "no" );
fprintf( pAbc->Err, "\t-f : enable printing flop values in each timeframe [default = %s].\n", fPrintFull? "yes": "no" );
fprintf( pAbc->Err, "\t-v : enable verbose output [default = %s].\n", fVerbose? "yes": "no" );
fprintf( pAbc->Err, "\t-a : print cex in AIGER 1.9 format [default = %s]\n", fAiger? "yes": "no" );
fprintf( pAbc->Err, "\t-f : enable printing flop values in each timeframe [default = %s]\n", fPrintFull? "yes": "no" );
fprintf( pAbc->Err, "\t-z : toggle using saved flop names [default = %s]\n", fUseFfNames? "yes": "no" );
fprintf( pAbc->Err, "\t-v : enable verbose output [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pAbc->Err, "\t-h : print the help massage\n" );
fprintf( pAbc->Err, "\t<file> : the name of the file to write\n" );
return 1;

1
src/base/wlc/wlc.h
View File

@ -214,6 +214,7 @@ struct Wlc_BstPar_t_
int fNoCleanup;
int fCreateMiter;
int fDecMuxes;
int fSaveFfNames;
int fVerbose;
Vec_Int_t * vBoxIds;
};

26
src/base/wlc/wlcBlast.c
View File

@ -2055,7 +2055,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pParIn )
}
else
{
pNew = Gia_ManDupZeroUndc( pTemp = pNew, p->pInits, pPar->fGiaSimple, 0 );
pNew = Gia_ManDupZeroUndc( pTemp = pNew, p->pInits, pPar->fSaveFfNames ? 1+Gia_ManRegNum(pNew) : 0, pPar->fGiaSimple, 0 );
Gia_ManDupRemapLiterals( vBits, pTemp );
Gia_ManStop( pTemp );
}
@ -2121,10 +2121,13 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pParIn )
if ( p->pInits[i] == 'x' || p->pInits[i] == 'X' )
{
char Buffer[100];
sprintf( Buffer, "%s%d", "init", i );
sprintf( Buffer, "_%s_abc_%d_", "init", i );
Vec_PtrPush( pNew->vNamesIn, Abc_UtilStrsav(Buffer) );
fAdded = 1;
}
if ( pPar->fSaveFfNames )
for ( i = 0; i < 1+Length; i++ )
Vec_PtrPush( pNew->vNamesIn, NULL );
}
Wlc_NtkForEachCi( p, pObj, i )
if ( !Wlc_ObjIsPi(pObj) )
@ -2173,6 +2176,25 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pParIn )
Vec_PtrPush( pNew->vNamesIn, Abc_UtilStrsav(Buffer) );
}
}
if ( p->pInits && pPar->fSaveFfNames )
{
char * pName;
int Length = (int)strlen(p->pInits);
int NameStart = Vec_PtrSize(pNew->vNamesIn)-Length;
int NullStart = Vec_PtrSize(pNew->vNamesIn)-2*Length;
int SepStart = Vec_PtrSize(pNew->vNamesIn)-2*Length-1;
assert( Vec_PtrEntry(pNew->vNamesIn, SepStart) == NULL );
Vec_PtrWriteEntry( pNew->vNamesIn, SepStart, Abc_UtilStrsav("_abc_190121_abc_") );
for ( i = 0; i < Length; i++ )
{
char Buffer[100];
sprintf( Buffer, "%c%s", p->pInits[i], Vec_PtrEntry(pNew->vNamesIn, NameStart+i) );
assert( Vec_PtrEntry(pNew->vNamesIn, NullStart+i) == NULL );
Vec_PtrWriteEntry( pNew->vNamesIn, NullStart+i, Abc_UtilStrsav(Buffer) );
}
Vec_PtrForEachEntry( char *, pNew->vNamesIn, pName, i )
assert( pName != NULL );
}
if ( p->pInits && fAdded )
Vec_PtrPush( pNew->vNamesIn, Abc_UtilStrsav("abc_reset_flop") );
if ( pPar->vBoxIds )

8
src/base/wlc/wlcCom.c
View File

@ -978,7 +978,7 @@ int Abc_CommandBlast( Abc_Frame_t * pAbc, int argc, char ** argv )
Wlc_BstParDefault( pPar );
pPar->nOutputRange = 2;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "ORAMcombadstnivh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "ORAMcombadstnizvh" ) ) != EOF )
{
switch ( c )
{
@ -1057,6 +1057,9 @@ int Abc_CommandBlast( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'i':
fPrintInputInfo ^= 1;
break;
case 'z':
pPar->fSaveFfNames ^= 1;
break;
case 'v':
pPar->fVerbose ^= 1;
break;
@ -1125,7 +1128,7 @@ int Abc_CommandBlast( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_FrameUpdateGia( pAbc, pNew );
return 0;
usage:
Abc_Print( -2, "usage: %%blast [-ORAM num] [-combadstnivh]\n" );
Abc_Print( -2, "usage: %%blast [-ORAM num] [-combadstnizvh]\n" );
Abc_Print( -2, "\t performs bit-blasting of the word-level design\n" );
Abc_Print( -2, "\t-O num : zero-based index of the first word-level PO to bit-blast [default = %d]\n", pPar->iOutput );
Abc_Print( -2, "\t-R num : the total number of word-level POs to bit-blast [default = %d]\n", pPar->nOutputRange );
@ -1141,6 +1144,7 @@ usage:
Abc_Print( -2, "\t-t : toggle creating regular multi-output miter [default = %s]\n", fMiter? "yes": "no" );
Abc_Print( -2, "\t-n : toggle dumping signal names into a text file [default = %s]\n", fDumpNames? "yes": "no" );
Abc_Print( -2, "\t-i : toggle to print input names after blasting [default = %s]\n", fPrintInputInfo ? "yes": "no" );
Abc_Print( -2, "\t-z : toggle saving flop names after blasting [default = %s]\n", pPar->fSaveFfNames ? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPar->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;

4
src/base/wlc/wlcReadVer.c
View File

@ -457,7 +457,7 @@ char * Wlc_PrsConvertInitValues( Wlc_Ntk_t * p )
pObj = Wlc_NtkObj( p, Wlc_ObjFaninId0(pObj) );
pInits = (pObj->Type == WLC_OBJ_CONST && !pObj->fXConst) ? Wlc_ObjConstValue(pObj) : NULL;
for ( k = 0; k < Abc_MinInt(Value, Wlc_ObjRange(pObj)); k++ )
Vec_StrPush( vStr, (char)(pInits ? '0' + Abc_InfoHasBit((unsigned *)pInits, k) : 'X') );
Vec_StrPush( vStr, (char)(pInits ? '0' + Abc_InfoHasBit((unsigned *)pInits, k) : 'x') );
// extend values with zero, in case the init value signal has different range compared to constant used
for ( ; k < Value; k++ )
Vec_StrPush( vStr, '0' );
@ -588,6 +588,8 @@ static inline char * Wlc_PrsReadConstant( Wlc_Prs_t * p, char * pStr, Vec_Int_t
if ( pStr[1] != 'h' )
return (char *)(ABC_PTRINT_T)Wlc_PrsWriteErrorMessage( p, pStr, "Expecting hexadecimal constant and not \"%c\".", pStr[1] );
*pXValue = (pStr[2] == 'x' || pStr[2] == 'X');
if ( *pXValue == 'X' )
*pXValue = 'x';
Vec_IntFill( vFanins, Abc_BitWordNum(nBits), 0 );
nDigits = Abc_TtReadHexNumber( (word *)Vec_IntArray(vFanins), pStr+2 );
if ( nDigits != (nBits + 3)/4 )