diff options
Diffstat (limited to 'src/base/io/io.c')
-rw-r--r-- | src/base/io/io.c | 400 |
1 files changed, 366 insertions, 34 deletions
diff --git a/src/base/io/io.c b/src/base/io/io.c index 9b3d288a..b8d1d7db 100644 --- a/src/base/io/io.c +++ b/src/base/io/io.c @@ -44,6 +44,7 @@ static int IoCommandReadBblif ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandReadBlif ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandReadBlifMv ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandReadBench ( Abc_Frame_t * pAbc, int argc, char **argv ); +static int IoCommandReadCex ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandReadDsd ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandReadEdif ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandReadEqn ( Abc_Frame_t * pAbc, int argc, char **argv ); @@ -114,6 +115,7 @@ void Io_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "I/O", "read_blif", IoCommandReadBlif, 1 ); Cmd_CommandAdd( pAbc, "I/O", "read_blif_mv", IoCommandReadBlifMv, 1 ); Cmd_CommandAdd( pAbc, "I/O", "read_bench", IoCommandReadBench, 1 ); + Cmd_CommandAdd( pAbc, "I/O", "read_cex", IoCommandReadCex, 1 ); Cmd_CommandAdd( pAbc, "I/O", "read_dsd", IoCommandReadDsd, 1 ); Cmd_CommandAdd( pAbc, "I/O", "read_formula", IoCommandReadDsd, 1 ); // Cmd_CommandAdd( pAbc, "I/O", "read_edif", IoCommandReadEdif, 1 ); @@ -681,6 +683,291 @@ usage: SeeAlso [] ***********************************************************************/ +int Abc_NtkReadCexFile( char * pFileName, Abc_Ntk_t * pNtk, Abc_Cex_t ** ppCex, int * pnFrames, int * fOldFormat ) +{ + FILE * pFile; + Abc_Cex_t * pCex; + Vec_Int_t * vNums; + int c, nRegs = -1, nFrames = -1; + pFile = fopen( pFileName, "r" ); + if ( pFile == NULL ) + { + printf( "Cannot open log file for reading \"%s\".\n" , pFileName ); + return -1; + } + + vNums = Vec_IntAlloc( 100 ); + int usedX = 0; + *fOldFormat = 0; + + int MaxLine = 1000000; + char *Buffer; + int state = 0; + int iPo = 0; + nFrames = -1; + int status = 0; + int i; + int nRegsNtk = 0; + Abc_Obj_t * pObj; + Abc_NtkForEachLatch( pNtk, pObj, i ) nRegsNtk++; + + Buffer = ABC_ALLOC( char, MaxLine ); + while ( fgets( Buffer, MaxLine, pFile ) != NULL ) + { + if ( Buffer[0] == '#' || Buffer[0] == 'c' || Buffer[0] == 'f' || Buffer[0] == 'u' ) + continue; + Buffer[strlen(Buffer) - 1] = '\0'; + if (state==0 && strlen(Buffer)>1) { + // old format detected + *fOldFormat = 1; + state = 2; + iPo = 0; + status = 1; + } + if (state==1 && Buffer[0]!='b' && Buffer[0]!='j') { + // old format detected, first line was actually register + *fOldFormat = 1; + state = 3; + Vec_IntPush( vNums, status ); + status = 1; + } + if (Buffer[0] == '.' ) + break; + switch(state) { + case 0 : + { + char c = Buffer[0]; + if ( c == '0' || c == '1' || c == '2' ) { + status = c - '0' ; + state = 1; + } else if ( c == 'x' ) { + // old format with one x state latch + usedX = 1; + // set to 2 so we can Abc_LatchSetInitNone + // acts like 0 when setting bits + Vec_IntPush( vNums, 2 ); + nRegs = Vec_IntSize(vNums); + state = 3; + } else { + printf( "ERROR: Bad aiger status line.\n" ); + return -1; + } + } + break; + case 1 : + iPo = atoi(Buffer+1); + state = 2; + break; + case 2 : + for (i=0; i<strlen(Buffer);i++) { + char c = Buffer[i]; + if ( c == '0' || c == '1' ) + Vec_IntPush( vNums, c - '0' ); + else if ( c == 'x') { + usedX = 1; + // set to 2 so we can Abc_LatchSetInitNone + // acts like 0 when setting bits + Vec_IntPush( vNums, 2 ); + } + } + nRegs = Vec_IntSize(vNums); + if ( nRegs < nRegsNtk ) + { + printf( "WARNING: Register number is smaller then in Ntk. Appending.\n" ); + for (i=0; i<nRegsNtk-nRegs;i++) { + Vec_IntPush( vNums, 0 ); + } + nRegs = Vec_IntSize(vNums); + } + else if ( nRegs > nRegsNtk ) + { + printf( "WARNING: Register number is larger then in Ntk. Truncating.\n" ); + Vec_IntShrink( vNums, nRegsNtk ); + nRegs = nRegsNtk; + } + state = 3; + break; + default: + for (i=0; i<strlen(Buffer);i++) { + char c = Buffer[i]; + if ( c == '0' || c == '1' ) + Vec_IntPush( vNums, c - '0' ); + else if ( c == 'x') { + usedX = 1; + Vec_IntPush( vNums, 0 ); + } + } + nFrames++; + break; + } + } + fclose( pFile ); + + if (usedX) + printf( "Warning: Using 0 instead of x in latches or primary inputs\n" ); + int iFrameCex = nFrames; + int nPiNtk = 0; + int nPoNtk = 0; + Abc_NtkForEachPi(pNtk, pObj, i ) nPiNtk++; + Abc_NtkForEachPo(pNtk, pObj, i ) nPoNtk++; + if ( nRegs < 0 ) + { + if (status == 0 || *fOldFormat == 0) + printf( "Counter-example is not available.\n" ); + else + printf( "ERROR: Cannot read register number.\n" ); + Vec_IntFree( vNums ); + return -1; + } + if ( nRegs != nRegsNtk ) + { + printf( "ERROR: Register number not coresponding to Ntk.\n" ); + Vec_IntFree( vNums ); + return -1; + } + if ( Vec_IntSize(vNums)-nRegs == 0 ) + { + printf( "ERROR: Cannot read counter example.\n" ); + Vec_IntFree( vNums ); + return -1; + } + if ( (Vec_IntSize(vNums)-nRegs) % (iFrameCex + 1) != 0 ) + { + printf( "ERROR: Incorrect number of bits.\n" ); + Vec_IntFree( vNums ); + return -1; + } + int nPi = (Vec_IntSize(vNums)-nRegs)/(iFrameCex + 1); + if ( nPi != nPiNtk ) + { + printf( "ERROR: Number of primary inputs not coresponding to Ntk.\n" ); + Vec_IntFree( vNums ); + return -1; + } + if ( iPo >= nPoNtk ) + { + printf( "ERROR: PO that failed verification not coresponding to Ntk.\n" ); + Vec_IntFree( vNums ); + return -1; + } + Abc_NtkForEachLatch( pNtk, pObj, i ) { + if ( Vec_IntEntry(vNums, i) ==0) + Abc_LatchSetInit0(pObj); + else if ( Vec_IntEntry(vNums, i) ==2) + Abc_LatchSetInitNone(pObj); + else + Abc_LatchSetInit1(pObj); + } + + pCex = 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; + // the zero-based number of the time-frame, for which verificaiton failed + pCex->iFrame = iFrameCex; + assert( Vec_IntSize(vNums) == pCex->nBits ); + for ( c = 0; c < pCex->nBits; c++ ) + if ( Vec_IntEntry(vNums, c) == 1) + Abc_InfoSetBit( pCex->pData, c ); + Vec_IntFree( vNums ); + if ( ppCex ) + *ppCex = pCex; + else + ABC_FREE( pCex ); + + if ( pnFrames ) + *pnFrames = nFrames; + return status; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ + + +int IoCommandReadCex( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + Abc_Ntk_t * pNtk; + char * pFileName; + FILE * pFile; + int fCheck; + int c; + int fOldFormat = 0; + + fCheck = 1; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF ) + { + switch ( c ) + { + case 'c': + fCheck ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( argc != globalUtilOptind + 1 ) + goto usage; + + // get the input file name + pFileName = argv[globalUtilOptind]; + if ( (pFile = fopen( pFileName, "r" )) == NULL ) + { + fprintf( pAbc->Err, "Cannot open input file \"%s\". \n", pFileName ); + return 1; + } + fclose( pFile ); + + pNtk = pAbc->pNtkCur; + if ( pNtk == NULL ) + { + fprintf( pAbc->Out, "Empty network.\n" ); + return 0; + } + Abc_FrameClearVerifStatus( pAbc ); + pAbc->Status = Abc_NtkReadCexFile( pFileName, pNtk, &pAbc->pCex, &pAbc->nFrames, &fOldFormat ); + + 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; + } + return 0; + +usage: + fprintf( pAbc->Err, "usage: read_cex [-ch] <file>\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-h : prints the command summary\n" ); + fprintf( pAbc->Err, "\tfile : the name of a file to read\n" ); + return 1; +} +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int IoCommandReadDsd( Abc_Frame_t * pAbc, int argc, char ** argv ) { Abc_Ntk_t * pNtk; @@ -2451,10 +2738,15 @@ void Abc_NtkDumpOneCexSpecial( FILE * pFile, Abc_Ntk_t * pNtk, Abc_Cex_t * pCex } +extern Abc_Cex_t * Bmc_CexInnerStates( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t ** ppCexImpl, int fVerbose ); +extern Abc_Cex_t * Bmc_CexEssentialBits( Gia_Man_t * p, Abc_Cex_t * pCexState, Abc_Cex_t * pCexCare, int fVerbose ); +extern Abc_Cex_t * Bmc_CexCareBits( Gia_Man_t * p, Abc_Cex_t * pCexState, Abc_Cex_t * pCexImpl, Abc_Cex_t * pCexEss, int fFindAll, int fVerbose ); + void Abc_NtkDumpOneCex( FILE * pFile, Abc_Ntk_t * pNtk, Abc_Cex_t * pCex, - int fPrintFull, int fNames, int fUseFfNames, int fMinimize, int fUseOldMin, - int fCheckCex, int fUseSatBased, int fHighEffort, int fAiger, int fVerbose ) + int fPrintFull, int fNames, int fUseFfNames, int fMinimize, int fUseOldMin, int fCexInfo, + int fCheckCex, int fUseSatBased, int fHighEffort, int fAiger, int fVerbose, int fExtended ) { + Abc_Cex_t * pCare = NULL; Abc_Obj_t * pObj; int i, f; if ( fPrintFull ) @@ -2470,15 +2762,17 @@ void Abc_NtkDumpOneCex( FILE * pFile, Abc_Ntk_t * pNtk, Abc_Cex_t * pCex, fprintf( pFile, "%s@%d=%c ", Abc_ObjName(pObj), f, '0'+Abc_InfoHasBit(pCexFull->pData, Abc_NtkCiNum(pNtk)*f + i) ); Abc_CexFreeP( &pCexFull ); } - else if ( fNames ) + else { - Abc_Cex_t * pCare = NULL; + if ( fNames ) + { + fprintf( pFile, "# FALSIFYING OUTPUTS:"); + fprintf( pFile, " %s", Abc_ObjName(Abc_NtkCo(pNtk, pCex->iPo)) ); + } if ( fMinimize ) { extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters ); Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 ); - fprintf( pFile, "# FALSIFYING OUTPUTS:"); - fprintf( pFile, " %s", Abc_ObjName(Abc_NtkCo(pNtk, pCex->iPo)) ); if ( fUseOldMin ) { pCare = Saig_ManCbaFindCexCareBits( pAig, pCex, 0, fVerbose ); @@ -2487,20 +2781,41 @@ void Abc_NtkDumpOneCex( FILE * pFile, Abc_Ntk_t * pNtk, Abc_Cex_t * pCex, } else if ( fUseSatBased ) pCare = Bmc_CexCareSatBasedMinimize( pAig, Saig_ManPiNum(pAig), pCex, fHighEffort, fCheckCex, fVerbose ); + else if ( fCexInfo ) + { + Gia_Man_t * p = Gia_ManFromAigSimple( pAig ); + Abc_Cex_t * pCexImpl = NULL; + Abc_Cex_t * pCexStates = Bmc_CexInnerStates( p, pCex, &pCexImpl, fVerbose ); + Abc_Cex_t * pCexCare = Bmc_CexCareBits( p, pCexStates, pCexImpl, NULL, 1, fVerbose ); + Abc_Cex_t * pCexEss; + + if ( fCheckCex && !Bmc_CexVerify( p, pCex, pCexCare ) ) + printf( "Counter-example care-set verification has failed.\n" ); + + pCexEss = Bmc_CexEssentialBits( p, pCexStates, pCexCare, fVerbose ); + + // pCare is pCexMin from Bmc_CexTest + pCare = Bmc_CexCareBits( p, pCexStates, pCexImpl, pCexEss, 0, fVerbose ); + + if ( fCheckCex && !Bmc_CexVerify( p, pCex, pCare ) ) + printf( "Counter-example min-set verification has failed.\n" ); + Abc_CexFreeP( &pCexStates ); + Abc_CexFreeP( &pCexImpl ); + Abc_CexFreeP( &pCexCare ); + Abc_CexFreeP( &pCexEss ); + } else pCare = Bmc_CexCareMinimize( pAig, Saig_ManPiNum(pAig), pCex, 4, fCheckCex, fVerbose ); Aig_ManStop( pAig ); - if(pCare == NULL) + if(pCare == NULL) printf( "Counter-example minimization has failed.\n" ); } - else + if (fNames) { - fprintf( pFile, "# FALSIFYING OUTPUTS:"); - fprintf( pFile, " %s", Abc_ObjName(Abc_NtkCo(pNtk, pCex->iPo)) ); + fprintf( pFile, "\n"); + fprintf( pFile, "# COUNTEREXAMPLE LENGTH: %u\n", pCex->iFrame+1); } - fprintf( pFile, "\n"); - fprintf( pFile, "# COUNTEREXAMPLE LENGTH: %u\n", pCex->iFrame+1); - if ( fUseFfNames && Abc_NtkCheckSpecialPi(pNtk) ) + if ( fNames && fUseFfNames && Abc_NtkCheckSpecialPi(pNtk) ) { int * pValues; int nXValues = 0, iFlop = 0, iPivotPi = -1; @@ -2540,29 +2855,36 @@ void Abc_NtkDumpOneCex( FILE * pFile, Abc_Ntk_t * pNtk, Abc_Cex_t * pCex, } else { + if (fExtended && fAiger && !fNames) { + fprintf( pFile, "1\n"); + fprintf( pFile, "b%d\n", pCex->iPo); + } // 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) ); + if ( fNames ) + fprintf( pFile, "%s@0=%c\n", Abc_ObjName(Abc_ObjFanout0(pObj)), '0'+!Abc_LatchIsInit0(pObj) ); + else + fprintf( pFile, "%c", '0'+!Abc_LatchIsInit0(pObj) ); + if ( !fNames && fAiger) + fprintf( pFile, "\n"); // output PI values (while skipping the minimized ones) - for ( f = 0; f <= pCex->iFrame; f++ ) + for ( f = 0; f <= pCex->iFrame; f++ ) { 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) ); + if ( fNames ) + fprintf( pFile, "%s@%d=%c\n", Abc_ObjName(pObj), f, '0'+Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i) ); + else + fprintf( pFile, "%c", '0'+Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i) ); + else if ( !fNames ) + fprintf( pFile, "x"); + if ( !fNames && fAiger) + fprintf( pFile, "\n"); + } + if (fExtended && fAiger && !fNames) + fprintf( pFile, ".\n"); } Abc_CexFreeP( &pCare ); } - else - { - Abc_NtkForEachLatch( pNtk, pObj, i ) - fprintf( pFile, "%c", '0'+!Abc_LatchIsInit0(pObj) ); - - for ( i = pCex->nRegs; i < pCex->nBits; i++ ) - { - if ( fAiger && (i-pCex->nRegs)%pCex->nPis == 0) - fprintf( pFile, "\n"); - fprintf( pFile, "%c", '0'+Abc_InfoHasBit(pCex->pData, i) ); - } - } } /**Function************************************************************* @@ -2591,9 +2913,11 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv ) int fPrintFull = 0; int fUseFfNames = 0; int fVerbose = 0; + int fCexInfo = 0; + int fExtended = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "snmueocafzvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "snmueocafzvhxt" ) ) != EOF ) { switch ( c ) { @@ -2630,6 +2954,12 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv ) case 'v': fVerbose ^= 1; break; + case 'x': + fCexInfo ^= 1; + break; + case 't': + fExtended ^= 1; + break; case 'h': goto usage; default: @@ -2678,8 +3008,8 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv ) if ( pAbc->pCex ) { Abc_NtkDumpOneCex( pFile, pNtk, pCex, - fPrintFull, fNames, fUseFfNames, fMinimize, fUseOldMin, - fCheckCex, fUseSatBased, fHighEffort, fAiger, fVerbose ); + fPrintFull, fNames, fUseFfNames, fMinimize, fUseOldMin, fCexInfo, + fCheckCex, fUseSatBased, fHighEffort, fAiger, fVerbose, fExtended ); } else if ( pAbc->vCexVec ) { @@ -2687,10 +3017,10 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv ) { if ( pCex == NULL ) continue; - fprintf( pFile, "#\n#\n# CEX for output %d\n#\n", i ); + fprintf( pFile, "#\n#\n# CEX for output %d\n#\n", i ); Abc_NtkDumpOneCex( pFile, pNtk, pCex, - fPrintFull, fNames, fUseFfNames, fMinimize, fUseOldMin, - fCheckCex, fUseSatBased, fHighEffort, fAiger, fVerbose ); + fPrintFull, fNames, fUseFfNames, fMinimize, fUseOldMin, fCexInfo, + fCheckCex, fUseSatBased, fHighEffort, fAiger, fVerbose, fExtended ); } } fprintf( pFile, "# DONE\n" ); @@ -2734,8 +3064,10 @@ usage: fprintf( pAbc->Err, "\t-u : use fast SAT-based CEX minimization [default = %s]\n", fUseSatBased? "yes": "no" ); 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-x : minimize using algorithm from cexinfo command [default = %s]\n", fCexInfo? "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-t : extended header info when 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" ); |