From feedbc744955df2b142d6a0b9dc62814567f5fc2 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Fri, 5 Aug 2022 14:28:13 +0200 Subject: read_cex: Faster parsing and care bits for verification --- src/base/io/io.c | 106 +++++++++++++++++++++++++++++++--------------- src/sat/bmc/bmc.h | 4 +- src/sat/bmc/bmcCexCare.c | 38 ++++++++++++++++- src/sat/bmc/bmcCexTools.c | 47 ++++++++++++++++++++ 4 files changed, 159 insertions(+), 36 deletions(-) diff --git a/src/base/io/io.c b/src/base/io/io.c index b8d1d7db..a8a5b618 100644 --- a/src/base/io/io.c +++ b/src/base/io/io.c @@ -683,10 +683,11 @@ usage: SeeAlso [] ***********************************************************************/ -int Abc_NtkReadCexFile( char * pFileName, Abc_Ntk_t * pNtk, Abc_Cex_t ** ppCex, int * pnFrames, int * fOldFormat ) +int Abc_NtkReadCexFile( char * pFileName, Abc_Ntk_t * pNtk, Abc_Cex_t ** ppCex, Abc_Cex_t ** ppCexCare, int * pnFrames, int * fOldFormat, int xMode ) { FILE * pFile; Abc_Cex_t * pCex; + Abc_Cex_t * pCexCare; Vec_Int_t * vNums; int c, nRegs = -1, nFrames = -1; pFile = fopen( pFileName, "r" ); @@ -702,6 +703,7 @@ int Abc_NtkReadCexFile( char * pFileName, Abc_Ntk_t * pNtk, Abc_Cex_t ** ppCex, int MaxLine = 1000000; char *Buffer; + int BufferLen = 0; int state = 0; int iPo = 0; nFrames = -1; @@ -716,8 +718,9 @@ int Abc_NtkReadCexFile( char * pFileName, Abc_Ntk_t * pNtk, Abc_Cex_t ** ppCex, { if ( Buffer[0] == '#' || Buffer[0] == 'c' || Buffer[0] == 'f' || Buffer[0] == 'u' ) continue; - Buffer[strlen(Buffer) - 1] = '\0'; - if (state==0 && strlen(Buffer)>1) { + BufferLen = strlen(Buffer) - 1; + Buffer[BufferLen] = '\0'; + if (state==0 && BufferLen>1) { // old format detected *fOldFormat = 1; state = 2; @@ -759,7 +762,7 @@ int Abc_NtkReadCexFile( char * pFileName, Abc_Ntk_t * pNtk, Abc_Cex_t ** ppCex, state = 2; break; case 2 : - for (i=0; i nRegsNtk ) { - printf( "WARNING: Register number is larger then in Ntk. Truncating.\n" ); + printf( "WARNING: Register number is larger than in Ntk. Truncating.\n" ); Vec_IntShrink( vNums, nRegsNtk ); nRegs = nRegsNtk; } state = 3; break; default: - for (i=0; i= nPoNtk ) + if ( iPo >= Abc_NtkPoNum(pNtk) ) { - printf( "ERROR: PO that failed verification not coresponding to Ntk.\n" ); - Vec_IntFree( vNums ); - return -1; + printf( "WARNING: PO that failed verification not coresponding to Ntk, using first PO instead.\n" ); + iPo = 0; } Abc_NtkForEachLatch( pNtk, pObj, i ) { - if ( Vec_IntEntry(vNums, i) ==0) - Abc_LatchSetInit0(pObj); - else if ( Vec_IntEntry(vNums, i) ==2) + if ( Vec_IntEntry(vNums, i) == 1 ) + Abc_LatchSetInit1(pObj); + else if ( Vec_IntEntry(vNums, i) == 2 && xMode ) Abc_LatchSetInitNone(pObj); else - Abc_LatchSetInit1(pObj); + Abc_LatchSetInit0(pObj); } pCex = Abc_CexAlloc( nRegs, nPi, iFrameCex + 1 ); + pCexCare = Abc_CexAlloc( nRegs, nPi, iFrameCex + 1); // the zero-based number of PO, for which verification failed // fails in Bmc_CexVerify if not less than actual number of PO pCex->iPo = iPo; + pCexCare->iPo = iPo; // the zero-based number of the time-frame, for which verificaiton failed pCex->iFrame = iFrameCex; + pCexCare->iFrame = iFrameCex; assert( Vec_IntSize(vNums) == pCex->nBits ); - for ( c = 0; c < pCex->nBits; c++ ) + for ( c = 0; c < pCex->nBits; c++ ) { if ( Vec_IntEntry(vNums, c) == 1) + { Abc_InfoSetBit( pCex->pData, c ); + Abc_InfoSetBit( pCexCare->pData, c ); + } + else if ( Vec_IntEntry(vNums, c) == 2 && xMode ) + { + // nothing to set + } + else + Abc_InfoSetBit( pCexCare->pData, c ); + } + Vec_IntFree( vNums ); + Abc_CexFreeP( ppCex ); if ( ppCex ) *ppCex = pCex; else - ABC_FREE( pCex ); + Abc_CexFree( pCex ); + Abc_CexFreeP( ppCexCare ); + if ( ppCexCare ) + *ppCexCare = pCexCare; + else + Abc_CexFree( pCexCare ); if ( pnFrames ) *pnFrames = nFrames; @@ -896,21 +914,27 @@ int Abc_NtkReadCexFile( char * pFileName, Abc_Ntk_t * pNtk, Abc_Cex_t ** ppCex, int IoCommandReadCex( Abc_Frame_t * pAbc, int argc, char ** argv ) { Abc_Ntk_t * pNtk; + Abc_Cex_t * pCex = NULL; + Abc_Cex_t * pCexCare = NULL; char * pFileName; FILE * pFile; - int fCheck; + int fCheck = 1; + int fXMode = 0; int c; int fOldFormat = 0; + int verified; - fCheck = 1; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "cxh" ) ) != EOF ) { switch ( c ) { case 'c': fCheck ^= 1; break; + case 'x': + fXMode ^= 1; + break; case 'h': goto usage; default: @@ -936,16 +960,31 @@ int IoCommandReadCex( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; } Abc_FrameClearVerifStatus( pAbc ); - pAbc->Status = Abc_NtkReadCexFile( pFileName, pNtk, &pAbc->pCex, &pAbc->nFrames, &fOldFormat ); + pAbc->Status = Abc_NtkReadCexFile( pFileName, pNtk, &pCex, &pCexCare, &pAbc->nFrames, &fOldFormat, fXMode); + if ( fOldFormat && !fCheck ) + printf( "WARNING: Old witness format detected and checking is disabled. Reading might have failed.\n" ); if ( fCheck && pAbc->Status==1) { extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters ); Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 ); - Bmc_CexCareVerify( pAig, pAbc->pCex, pAbc->pCex, false ); - Aig_ManStop( pAig ); - } else if (fOldFormat) { - fprintf( pAbc->Err, "Using old aiger format with no checks enabled.\n" ); - return -1; + + verified = Bmc_CexCareVerify( pAig, pCex, pCexCare, false ); + if (!verified) + { + printf( "Checking CEX for any PO.\n" ); + int verified = Bmc_CexCareVerifyAnyPo( pAig, pCex, pCexCare, false ); + Aig_ManStop( pAig ); + if (verified < 0) + { + Abc_CexFreeP(&pCex); + Abc_CexFreeP(&pCexCare); + return 1; + } + pAbc->pCex->iPo = verified; + } + + Abc_CexFreeP(&pCexCare); + Abc_FrameReplaceCex( pAbc, &pCex ); } return 0; @@ -953,6 +992,7 @@ usage: fprintf( pAbc->Err, "usage: read_cex [-ch] \n" ); fprintf( pAbc->Err, "\t reads the witness cex\n" ); fprintf( pAbc->Err, "\t-c : toggle check after reading [default = %s]\n", fCheck? "yes":"no" ); + fprintf( pAbc->Err, "\t-x : read x bits for verification [default = %s]\n", fXMode? "yes":"no" ); fprintf( pAbc->Err, "\t-h : prints the command summary\n" ); fprintf( pAbc->Err, "\tfile : the name of a file to read\n" ); return 1; diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h index 12439faa..2c843392 100644 --- a/src/sat/bmc/bmc.h +++ b/src/sat/bmc/bmc.h @@ -219,7 +219,8 @@ extern int Gia_ManBmcPerform( Gia_Man_t * p, Bmc_AndPar_t * pPars extern Abc_Cex_t * Bmc_CexCareExtendToObjects( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare ); extern Abc_Cex_t * Bmc_CexCareMinimize( Aig_Man_t * p, int nRealPis, Abc_Cex_t * pCex, int nTryCexes, int fCheck, int fVerbose ); extern Abc_Cex_t * Bmc_CexCareMinimizeAig( Gia_Man_t * p, int nRealPis, Abc_Cex_t * pCex, int nTryCexes, int fCheck, int fVerbose ); -extern void Bmc_CexCareVerify( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, int fVerbose ); +extern int Bmc_CexCareVerify( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, int fVerbose ); +extern int Bmc_CexCareVerifyAnyPo( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, int fVerbose ); extern Abc_Cex_t * Bmc_CexCareSatBasedMinimize( Aig_Man_t * p, int nRealPis, Abc_Cex_t * pCex, int fHighEffort, int fCheck, int fVerbose ); extern Abc_Cex_t * Bmc_CexCareSatBasedMinimizeAig( Gia_Man_t * p, Abc_Cex_t * pCex, int fHighEffort, int fVerbose ); /*=== bmcCexCut.c ==========================================================*/ @@ -230,6 +231,7 @@ extern Abc_Cex_t * Saig_ManCexMinPerform( Aig_Man_t * pAig, Abc_Cex_t * pC /*=== bmcCexTool.c ==========================================================*/ extern void Bmc_CexPrint( Abc_Cex_t * pCex, int nRealPis, int fVerbose ); extern int Bmc_CexVerify( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare ); +extern int Bmc_CexVerifyAnyPo( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare ); /*=== bmcICheck.c ==========================================================*/ extern void Bmc_PerformICheck( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fEmpty, int fVerbose ); extern Vec_Int_t * Bmc_PerformISearch( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fReverse, int fBackTopo, int fDump, int fVerbose ); diff --git a/src/sat/bmc/bmcCexCare.c b/src/sat/bmc/bmcCexCare.c index c274b04c..d9a677c3 100644 --- a/src/sat/bmc/bmcCexCare.c +++ b/src/sat/bmc/bmcCexCare.c @@ -455,8 +455,9 @@ Abc_Cex_t * Bmc_CexCareSatBasedMinimize( Aig_Man_t * p, int nRealPis, Abc_Cex_t SeeAlso [] ***********************************************************************/ -void Bmc_CexCareVerify( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, int fVerbose ) +int Bmc_CexCareVerify( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, int fVerbose ) { + int result; Gia_Man_t * pGia = Gia_ManFromAigSimple( p ); if ( fVerbose ) { @@ -465,11 +466,13 @@ void Bmc_CexCareVerify( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, in printf( "Minimized: " ); Bmc_CexPrint( pCexMin, Gia_ManPiNum(pGia), 0 ); } - if ( !Bmc_CexVerify( pGia, pCex, pCexMin ) ) + result = Bmc_CexVerify( pGia, pCex, pCexMin ); + if ( !result ) printf( "Counter-example verification has failed.\n" ); else printf( "Counter-example verification succeeded.\n" ); Gia_ManStop( pGia ); + return result; } /* { @@ -480,6 +483,37 @@ void Bmc_CexCareVerify( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, in } */ +/**Function************************************************************* + + Synopsis [Verifies the care set of the counter-example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Bmc_CexCareVerifyAnyPo( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, int fVerbose ) +{ + int iPo; + Gia_Man_t * pGia = Gia_ManFromAigSimple( p ); + if ( fVerbose ) + { + printf( "Original : " ); + Bmc_CexPrint( pCex, Gia_ManPiNum(pGia), 0 ); + printf( "Minimized: " ); + Bmc_CexPrint( pCexMin, Gia_ManPiNum(pGia), 0 ); + } + iPo = Bmc_CexVerifyAnyPo( pGia, pCex, pCexMin ); + if ( iPo < 0 ) + printf( "Counter-example verification has failed.\n" ); + else + printf( "Counter-example verification succeeded.\n" ); + Gia_ManStop( pGia ); + return iPo; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/sat/bmc/bmcCexTools.c b/src/sat/bmc/bmcCexTools.c index 6cc29857..6bea6fc5 100644 --- a/src/sat/bmc/bmcCexTools.c +++ b/src/sat/bmc/bmcCexTools.c @@ -374,6 +374,53 @@ int Bmc_CexVerify( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare ) return Gia_ObjTerSimGet1(pObj); } +/**Function************************************************************* + + Synopsis [Verifies the care set of the counter-example for an arbitrary PO.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Bmc_CexVerifyAnyPo( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare ) +{ + Gia_Obj_t * pObj; + int i, k; +// assert( pCex->nRegs > 0 ); +// assert( pCexCare->nRegs == 0 ); + Gia_ObjTerSimSet0( Gia_ManConst0(p) ); + Gia_ManForEachRi( p, pObj, k ) + Gia_ObjTerSimSet0( pObj ); + for ( i = 0; i <= pCex->iFrame; i++ ) + { + Gia_ManForEachPi( p, pObj, k ) + { + if ( !Abc_InfoHasBit( pCexCare->pData, pCexCare->nRegs + i * pCexCare->nPis + k ) ) + Gia_ObjTerSimSetX( pObj ); + else if ( Abc_InfoHasBit( pCex->pData, pCex->nRegs + i * pCex->nPis + k ) ) + Gia_ObjTerSimSet1( pObj ); + else + Gia_ObjTerSimSet0( pObj ); + } + Gia_ManForEachRo( p, pObj, k ) + Gia_ObjTerSimRo( p, pObj ); + Gia_ManForEachAnd( p, pObj, k ) + Gia_ObjTerSimAnd( pObj ); + Gia_ManForEachCo( p, pObj, k ) + Gia_ObjTerSimCo( pObj ); + } + for (i = 0; i < Gia_ManPoNum(p) - Gia_ManConstrNum(p); i++) + { + pObj = Gia_ManPo( p, i ); + if (Gia_ObjTerSimGet1(pObj)) + return i; + } + return -1; +} + /**Function************************************************************* Synopsis [Computes internal states of the CEX.] -- cgit v1.2.3