From b3d81b5f76aa3673bb4c6e5c79056cfb4950082e Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 21 Jan 2019 14:57:05 -0800 Subject: Exploring other ways of CEX writing. --- src/aig/gia/gia.h | 2 +- src/aig/gia/giaAiger.c | 2 +- src/aig/gia/giaDup.c | 7 ++++-- src/aig/gia/giaRex.c | 2 +- src/aig/gia/giaTim.c | 2 +- src/base/abci/abc.c | 2 +- src/base/cba/cbaBlast.c | 2 +- src/base/io/io.c | 56 ++++++++++++++++++++++++++++++++++++++++++----- src/base/wlc/wlc.h | 1 + src/base/wlc/wlcBlast.c | 26 ++++++++++++++++++++-- src/base/wlc/wlcCom.c | 8 +++++-- src/base/wlc/wlcReadVer.c | 4 +++- 12 files changed, 96 insertions(+), 18 deletions(-) (limited to 'src') diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index e7e64302..2e888130 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -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 ); diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c index 03929aff..47986faa 100644 --- a/src/aig/gia/giaAiger.c +++ b/src/aig/gia/giaAiger.c @@ -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 ); diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index e868e3ae..ae38a95a 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -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++ ) diff --git a/src/aig/gia/giaRex.c b/src/aig/gia/giaRex.c index ebfc9401..7f8d365e 100644 --- a/src/aig/gia/giaRex.c +++ b/src/aig/gia/giaRex.c @@ -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 ); /* diff --git a/src/aig/gia/giaTim.c b/src/aig/gia/giaTim.c index e136f68f..3f65d65f 100644 --- a/src/aig/gia/giaTim.c +++ b/src/aig/gia/giaTim.c @@ -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 ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index bcd876a3..974cf0f4 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -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 ); } diff --git a/src/base/cba/cbaBlast.c b/src/base/cba/cbaBlast.c index 490a36eb..937b9b69 100644 --- a/src/base/cba/cbaBlast.c +++ b/src/base/cba/cbaBlast.c @@ -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 ); diff --git a/src/base/io/io.c b/src/base/io/io.c index a85d64ef..ea46ac66 100644 --- a/src/base/io/io.c +++ b/src/base/io/io.c @@ -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] \n" ); + fprintf( pAbc->Err, "usage: write_cex [-snmueocfzvh] \n" ); fprintf( pAbc->Err, "\t saves counter-example (CEX) derived by \"sat\", \"iprove\", \"dprove\", etc\n" ); fprintf( pAbc->Err, "\t the output 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 : the name of the file to write\n" ); return 1; diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h index 6547da13..a04e19e8 100644 --- a/src/base/wlc/wlc.h +++ b/src/base/wlc/wlc.h @@ -214,6 +214,7 @@ struct Wlc_BstPar_t_ int fNoCleanup; int fCreateMiter; int fDecMuxes; + int fSaveFfNames; int fVerbose; Vec_Int_t * vBoxIds; }; diff --git a/src/base/wlc/wlcBlast.c b/src/base/wlc/wlcBlast.c index 01b6e64c..9b55c008 100644 --- a/src/base/wlc/wlcBlast.c +++ b/src/base/wlc/wlcBlast.c @@ -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 ) diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c index 5e69000f..3031f331 100644 --- a/src/base/wlc/wlcCom.c +++ b/src/base/wlc/wlcCom.c @@ -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; diff --git a/src/base/wlc/wlcReadVer.c b/src/base/wlc/wlcReadVer.c index db2cf3b2..9c40e71e 100644 --- a/src/base/wlc/wlcReadVer.c +++ b/src/base/wlc/wlcReadVer.c @@ -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 ) -- cgit v1.2.3