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

Unified the use of counter-examples in three packages.

This commit is contained in:
Alan Mishchenko 2011-02-13 17:46:48 -08:00
parent 686d38d667
commit 71cbf17e7f
42 changed files with 270 additions and 818 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
abclib.dsp
View File

@ -2359,6 +2359,14 @@ SOURCE=.\src\misc\util\util_hack.h
# End Source File
# Begin Source File
SOURCE=.\src\misc\util\utilCex.c
# End Source File
# Begin Source File
SOURCE=.\src\misc\util\utilCex.h
# End Source File
# Begin Source File
SOURCE=.\src\misc\util\utilFile.c
# End Source File
# Begin Source File
@ -4118,10 +4126,6 @@ SOURCE=.\src\aig\llb\llb3Nonlin.c
SOURCE=.\src\aig\llb\llbInt.h
# End Source File
# End Group
# Begin Group "bll"
# PROP Default_Filter ""
# End Group
# End Group
# End Group
# Begin Group "Header Files"

1
src/aig/aig/aig.h
View File

@ -33,6 +33,7 @@
#include <time.h>
#include "vec.h"
#include "utilCex.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///

5
src/aig/bbr/bbrCex.c
View File

@ -19,7 +19,6 @@
***********************************************************************/
#include "bbr.h"
#include "ssw.h"
ABC_NAMESPACE_IMPL_START
@ -60,7 +59,7 @@ Abc_Cex_t * Aig_ManVerifyUsingBddsCountExample( Aig_Man_t * p, DdManager * dd,
//printf( "\nDeriving counter-example.\n" );
// allocate room for the counter-example
pCex = Ssw_SmlAllocCounterExample( Saig_ManRegNum(p), Saig_ManPiNum(p), Vec_PtrSize(vOnionRings)+1 );
pCex = Abc_CexAlloc( Saig_ManRegNum(p), Saig_ManPiNum(p), Vec_PtrSize(vOnionRings)+1 );
pCex->iFrame = Vec_PtrSize(vOnionRings);
pCex->iPo = iOutput;
nPiOffset = Saig_ManRegNum(p) + Saig_ManPiNum(p) * Vec_PtrSize(vOnionRings);
@ -153,7 +152,7 @@ Abc_Cex_t * Aig_ManVerifyUsingBddsCountExample( Aig_Man_t * p, DdManager * dd,
// verify the counter example
if ( Vec_PtrSize(vOnionRings) < 1000 )
{
RetValue = Ssw_SmlRunCounterExample( p, pCex );
RetValue = Saig_ManVerifyCex( p, pCex );
if ( RetValue == 0 && !fSilent )
printf( "Aig_ManVerifyUsingBdds(): Counter-example verification has FAILED.\n" );
}

3
src/aig/bbr/bbrReach.c
View File

@ -19,7 +19,6 @@
***********************************************************************/
#include "bbr.h"
#include "ssw.h"
ABC_NAMESPACE_IMPL_START
@ -568,7 +567,7 @@ int Aig_ManVerifyUsingBdds( Aig_Man_t * pInit, Saig_ParBbr_t * pPars )
else
Vec_IntPush( vInputMap, -1 );
// create new pattern
pCexNew = Ssw_SmlAllocCounterExample( Saig_ManRegNum(pInit), Saig_ManPiNum(pInit), pCexOld->iFrame+1 );
pCexNew = Abc_CexAlloc( Saig_ManRegNum(pInit), Saig_ManPiNum(pInit), pCexOld->iFrame+1 );
pCexNew->iFrame = pCexOld->iFrame;
pCexNew->iPo = pCexOld->iPo;
// copy the bit-data

4
src/aig/cec/cecCec.c
View File

@ -164,7 +164,7 @@ int Cec_ManVerify( Gia_Man_t * pInit, Cec_ParCec_t * pPars )
{
if ( p->pCexComb != NULL )
{
if ( p->pCexComb && !Gia_ManVerifyCounterExample( p, p->pCexComb, 1 ) )
if ( p->pCexComb && !Gia_ManVerifyCex( p, p->pCexComb, 1 ) )
Abc_Print( 1, "Counter-example simulation has failed.\n" );
Abc_Print( 1, "Networks are NOT EQUIVALENT. " );
Abc_PrintTime( 1, "Time", clock() - clk );
@ -220,7 +220,7 @@ int Cec_ManVerify( Gia_Man_t * pInit, Cec_ParCec_t * pPars )
fflush( stdout );
RetValue = Cec_ManVerifyOld( pNew, pPars->fVerbose, &pPars->iOutFail );
p->pCexComb = pNew->pCexComb; pNew->pCexComb = NULL;
if ( p->pCexComb && !Gia_ManVerifyCounterExample( p, p->pCexComb, 1 ) )
if ( p->pCexComb && !Gia_ManVerifyCex( p, p->pCexComb, 1 ) )
Abc_Print( 1, "Counter-example simulation has failed.\n" );
Gia_ManStop( pNew );
return RetValue;

4
src/aig/cec/cecSeq.c
View File

@ -338,7 +338,7 @@ int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars )
}
Gia_ManRandom( 1 );
// prepare starting pattern
pState = Gia_ManAllocCounterExample( Gia_ManRegNum(pAig), 0, 0 );
pState = Abc_CexAlloc( Gia_ManRegNum(pAig), 0, 0 );
pState->iFrame = -1;
pState->iPo = -1;
// prepare SAT solving
@ -359,7 +359,7 @@ int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars )
Abc_Print( 1, "Cec_ManSeqSemiformal: There are only trivial equiv candidates left (PO drivers). Quitting.\n" );
break;
}
// Gia_ManPrintCounterExample( pState );
// Abc_CexPrint( pState );
// derive speculatively reduced model
// pSrm = Gia_ManSpecReduceInit( pAig, pState, pPars->nFrames, pPars->fDualOut );
pSrm = Gia_ManSpecReduceInitFrames( pAig, pState, pPars->nFrames, &nFramesReal, pPars->fDualOut, pPars->nMinOutputs );

6
src/aig/fra/fra.h
View File

@ -376,12 +376,6 @@ extern Fra_Sml_t * Fra_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int
extern Fra_Sml_t * Fra_SmlSimulateComb( Aig_Man_t * pAig, int nWords );
extern Abc_Cex_t * Fra_SmlGetCounterExample( Fra_Sml_t * p );
extern Abc_Cex_t * Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, int * pModel );
extern void Fra_SmlFreeCounterExample( Abc_Cex_t * p );
extern Abc_Cex_t * Fra_SmlTrivCounterExample( Aig_Man_t * pAig, int iFrameOut );
extern int Fra_SmlRunCounterExample( Aig_Man_t * pAig, Abc_Cex_t * p );
extern int Fra_SmlWriteCounterExample( FILE * pFile, Aig_Man_t * pAig, Abc_Cex_t * p );
extern Abc_Cex_t * Fra_SmlSimpleCounterExample( Aig_Man_t * pAig, int * pModel, int iFrame, int iPo );
ABC_NAMESPACE_HEADER_END

4
src/aig/fra/fraBmc.c
View File

@ -417,7 +417,7 @@ void Fra_BmcPerformSimple( Aig_Man_t * pAig, int nFrames, int nBTLimit, int fRew
clk = clock();
iOutput = Fra_FraigMiterAssertedOutput( pBmc->pAigFrames );
if ( iOutput >= 0 )
pAig->pSeqModel = Fra_SmlTrivCounterExample( pAig, iOutput );
pAig->pSeqModel = Abc_CexMakeTriv( Aig_ManRegNum(pAig), Aig_ManPiNum(pAig)-Aig_ManRegNum(pAig), Aig_ManPoNum(pAig)-Aig_ManRegNum(pAig), iOutput );
else
{
pBmc->pAigFraig = Fra_FraigEquivence( pBmc->pAigFrames, nBTLimit, 1 );
@ -428,7 +428,7 @@ void Fra_BmcPerformSimple( Aig_Man_t * pAig, int nFrames, int nBTLimit, int fRew
ABC_FREE( pBmc->pAigFraig->pData );
}
else if ( iOutput >= 0 )
pAig->pSeqModel = Fra_SmlTrivCounterExample( pAig, iOutput );
pAig->pSeqModel = Abc_CexMakeTriv( Aig_ManRegNum(pAig), Aig_ManPiNum(pAig)-Aig_ManRegNum(pAig), Aig_ManPoNum(pAig)-Aig_ManRegNum(pAig), iOutput );
}
if ( fVerbose )
{

14
src/aig/fra/fraSec.c
View File

@ -203,14 +203,14 @@ clk = clock();
if ( pTemp->pSeqModel )
{
if ( !Ssw_SmlRunCounterExample( pTemp, pTemp->pSeqModel ) )
if ( !Saig_ManVerifyCex( pTemp, pTemp->pSeqModel ) )
printf( "Fra_FraigSec(): Counter-example verification has FAILED.\n" );
if ( Saig_ManPiNum(p) != Saig_ManPiNum(pTemp) )
printf( "The counter-example is invalid because of phase abstraction.\n" );
else
{
ABC_FREE( p->pSeqModel );
p->pSeqModel = Ssw_SmlDupCounterExample( pTemp->pSeqModel, Aig_ManRegNum(p) );
p->pSeqModel = Abc_CexDup( pTemp->pSeqModel, Aig_ManRegNum(p) );
ABC_FREE( pTemp->pSeqModel );
}
}
@ -443,7 +443,7 @@ ABC_PRT( "Time", clock() - clk );
else
{
ABC_FREE( p->pSeqModel );
p->pSeqModel = Ssw_SmlDupCounterExample( pNew->pSeqModel, Aig_ManRegNum(p) );
p->pSeqModel = Abc_CexDup( pNew->pSeqModel, Aig_ManRegNum(p) );
ABC_FREE( pNew->pSeqModel );
}
@ -505,7 +505,7 @@ clk = clock();
RetValue = Inter_ManPerformInterpolation( pTemp, pPars, &Depth );
if ( pTemp->pSeqModel )
{
pCex = p->pSeqModel = Ssw_SmlDupCounterExample( pTemp->pSeqModel, Aig_ManRegNum(p) );
pCex = p->pSeqModel = Abc_CexDup( pTemp->pSeqModel, Aig_ManRegNum(p) );
pCex->iPo = i;
Aig_ManStop( pTemp );
break;
@ -548,7 +548,7 @@ clk = clock();
{
Abc_Cex_t * pCex;
pCex = pNew->pSeqModel = pNewOrpos->pSeqModel; pNewOrpos->pSeqModel = NULL;
pCex->iPo = Ssw_SmlFindOutputCounterExample( pNew, pNew->pSeqModel );
pCex->iPo = Saig_ManFindFailedPoCex( pNew, pNew->pSeqModel );
}
Aig_ManStop( pNewOrpos );
}
@ -598,7 +598,7 @@ ABC_PRT( "Time", clock() - clk );
printf( "Running property directed reachability...\n" );
RetValue = Pdr_ManSolve( pNewOrpos, pPars, &pCex );
if ( pCex )
pCex->iPo = Ssw_SmlFindOutputCounterExample( pNew, pCex );
pCex->iPo = Saig_ManFindFailedPoCex( pNew, pCex );
Aig_ManStop( pNewOrpos );
pNew->pSeqModel = pCex;
}
@ -665,7 +665,7 @@ ABC_PRT( "Time", clock() - clkTotal );
else
{
ABC_FREE( p->pSeqModel );
p->pSeqModel = Ssw_SmlDupCounterExample( pNew->pSeqModel, Aig_ManRegNum(p) );
p->pSeqModel = Abc_CexDup( pNew->pSeqModel, Aig_ManRegNum(p) );
ABC_FREE( pNew->pSeqModel );
}
}

222
src/aig/fra/fraSim.c
View File

@ -19,6 +19,7 @@
***********************************************************************/
#include "fra.h"
#include "saig.h"
ABC_NAMESPACE_IMPL_START
@ -877,45 +878,6 @@ Fra_Sml_t * Fra_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nW
return p;
}
/**Function*************************************************************
Synopsis [Allocates a counter-example.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Cex_t * Fra_SmlAllocCounterExample( int nRegs, int nRealPis, int nFrames )
{
Abc_Cex_t * pCex;
int nWords = Aig_BitWordNum( nRegs + nRealPis * nFrames );
pCex = (Abc_Cex_t *)ABC_ALLOC( char, sizeof(Abc_Cex_t) + sizeof(unsigned) * nWords );
memset( pCex, 0, sizeof(Abc_Cex_t) + sizeof(unsigned) * nWords );
pCex->nRegs = nRegs;
pCex->nPis = nRealPis;
pCex->nBits = nRegs + nRealPis * nFrames;
return pCex;
}
/**Function*************************************************************
Synopsis [Frees the counter-example.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_SmlFreeCounterExample( Abc_Cex_t * pCex )
{
ABC_FREE( pCex );
}
/**Function*************************************************************
Synopsis [Creates sequential counter-example from the simulation info.]
@ -960,7 +922,7 @@ Abc_Cex_t * Fra_SmlGetCounterExample( Fra_Sml_t * p )
assert( iBit < 32 * p->nWordsFrame );
// allocate the counter example
pCex = Fra_SmlAllocCounterExample( Aig_ManRegNum(p->pAig), Aig_ManPiNum(p->pAig) - Aig_ManRegNum(p->pAig), iFrame + 1 );
pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig), Aig_ManPiNum(p->pAig) - Aig_ManRegNum(p->pAig), iFrame + 1 );
pCex->iPo = iPo;
pCex->iFrame = iFrame;
@ -981,10 +943,10 @@ Abc_Cex_t * Fra_SmlGetCounterExample( Fra_Sml_t * p )
}
}
// verify the counter example
if ( !Fra_SmlRunCounterExample( p->pAig, pCex ) )
if ( !Saig_ManVerifyCex( p->pAig, pCex ) )
{
printf( "Fra_SmlGetCounterExample(): Counter-example is invalid.\n" );
Fra_SmlFreeCounterExample( pCex );
Abc_CexFree( pCex );
pCex = NULL;
}
return pCex;
@ -1026,7 +988,7 @@ Abc_Cex_t * Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, in
}
assert( iPo >= 0 );
// allocate the counter example
pCex = Fra_SmlAllocCounterExample( Aig_ManRegNum(pAig), nTruePis, iFrame + 1 );
pCex = Abc_CexAlloc( Aig_ManRegNum(pAig), nTruePis, iFrame + 1 );
pCex->iPo = iPo;
pCex->iFrame = iFrame;
@ -1040,186 +1002,16 @@ Abc_Cex_t * Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, in
}
// verify the counter example
if ( !Fra_SmlRunCounterExample( pAig, pCex ) )
if ( !Saig_ManVerifyCex( pAig, pCex ) )
{
printf( "Fra_SmlGetCounterExample(): Counter-example is invalid.\n" );
Fra_SmlFreeCounterExample( pCex );
Abc_CexFree( pCex );
pCex = NULL;
}
return pCex;
}
/**Function*************************************************************
Synopsis [Make the trivial counter-example for the trivially asserted output.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Cex_t * Fra_SmlTrivCounterExample( Aig_Man_t * pAig, int iFrameOut )
{
Abc_Cex_t * pCex;
int nTruePis, nTruePos, iPo, iFrame;
assert( Aig_ManRegNum(pAig) > 0 );
nTruePis = Aig_ManPiNum(pAig)-Aig_ManRegNum(pAig);
nTruePos = Aig_ManPoNum(pAig)-Aig_ManRegNum(pAig);
iPo = iFrameOut % nTruePos;
iFrame = iFrameOut / nTruePos;
// allocate the counter example
pCex = Fra_SmlAllocCounterExample( Aig_ManRegNum(pAig), nTruePis, iFrame + 1 );
pCex->iPo = iPo;
pCex->iFrame = iFrame;
return pCex;
}
/**Function*************************************************************
Synopsis [Resimulates the counter-example.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_SmlRunCounterExample( Aig_Man_t * pAig, Abc_Cex_t * p )
{
Fra_Sml_t * pSml;
Aig_Obj_t * pObj;
int RetValue, i, k, iBit;
assert( Aig_ManRegNum(pAig) > 0 );
assert( Aig_ManRegNum(pAig) < Aig_ManPiNum(pAig) );
// start a new sequential simulator
pSml = Fra_SmlStart( pAig, 0, p->iFrame+1, 1 );
// assign simulation info for the registers
iBit = 0;
Aig_ManForEachLoSeq( pAig, pObj, i )
Fra_SmlAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), 0 );
// assign simulation info for the primary inputs
for ( i = 0; i <= p->iFrame; i++ )
Aig_ManForEachPiSeq( pAig, pObj, k )
Fra_SmlAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), i );
assert( iBit == p->nBits );
// run random simulation
Fra_SmlSimulateOne( pSml );
// check if the given output has failed
RetValue = !Fra_SmlNodeIsZero( pSml, Aig_ManPo(pAig, p->iPo) );
Fra_SmlStop( pSml );
return RetValue;
}
/**Function*************************************************************
Synopsis [Make the trivial counter-example for the trivially asserted output.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Cex_t * Fra_SmlSimpleCounterExample( Aig_Man_t * pAig, int * pModel, int iFrame, int iPo )
{
Abc_Cex_t * pCex;
int iBit;
pCex = Fra_SmlAllocCounterExample( Aig_ManRegNum(pAig), Aig_ManPiNum(pAig)-Aig_ManRegNum(pAig), iFrame + 1 );
pCex->iPo = iPo;
pCex->iFrame = iFrame;
for ( iBit = Aig_ManRegNum(pAig); iBit < pCex->nBits; iBit++ )
if ( pModel[iBit-Aig_ManRegNum(pAig)] )
Aig_InfoSetBit( pCex->pData, iBit );
/*
if ( !Fra_SmlRunCounterExample( pAig, pCex ) )
{
printf( "Fra_SmlSimpleCounterExample(): Counter-example is invalid.\n" );
// Fra_SmlFreeCounterExample( pCex );
// pCex = NULL;
}
*/
return pCex;
}
/**Function*************************************************************
Synopsis [Resimulates the counter-example.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_SmlWriteCounterExample( FILE * pFile, Aig_Man_t * pAig, Abc_Cex_t * p )
{
Fra_Sml_t * pSml;
Aig_Obj_t * pObj;
int RetValue, i, k, iBit;
unsigned * pSims;
assert( Aig_ManRegNum(pAig) > 0 );
assert( Aig_ManRegNum(pAig) < Aig_ManPiNum(pAig) );
// start a new sequential simulator
pSml = Fra_SmlStart( pAig, 0, p->iFrame+1, 1 );
// assign simulation info for the registers
iBit = 0;
Aig_ManForEachLoSeq( pAig, pObj, i )
// Fra_SmlAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), 0 );
Fra_SmlAssignConst( pSml, pObj, 0, 0 );
// assign simulation info for the primary inputs
iBit = p->nRegs;
for ( i = 0; i <= p->iFrame; i++ )
Aig_ManForEachPiSeq( pAig, pObj, k )
Fra_SmlAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), i );
assert( iBit == p->nBits );
// run random simulation
Fra_SmlSimulateOne( pSml );
// check if the given output has failed
RetValue = !Fra_SmlNodeIsZero( pSml, Aig_ManPo(pAig, p->iPo) );
// write the output file
for ( i = 0; i <= p->iFrame; i++ )
{
/*
Aig_ManForEachLoSeq( pAig, pObj, k )
{
pSims = Fra_ObjSim(pSml, pObj->Id);
fprintf( pFile, "%d", (int)(pSims[i] != 0) );
}
fprintf( pFile, " " );
*/
Aig_ManForEachPiSeq( pAig, pObj, k )
{
pSims = Fra_ObjSim(pSml, pObj->Id);
fprintf( pFile, "%d", (int)(pSims[i] != 0) );
}
/*
fprintf( pFile, " " );
Aig_ManForEachPoSeq( pAig, pObj, k )
{
pSims = Fra_ObjSim(pSml, pObj->Id);
fprintf( pFile, "%d", (int)(pSims[i] != 0) );
}
fprintf( pFile, " " );
Aig_ManForEachLiSeq( pAig, pObj, k )
{
pSims = Fra_ObjSim(pSml, pObj->Id);
fprintf( pFile, "%d", (int)(pSims[i] != 0) );
}
*/
fprintf( pFile, "\n" );
}
Fra_SmlStop( pSml );
return RetValue;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///

2
src/aig/fsim/fsimSim.c
View File

@ -434,7 +434,7 @@ Abc_Cex_t * Fsim_ManGenerateCounter( Aig_Man_t * pAig, int iFrame, int iOut, int
Abc_Cex_t * p;
unsigned * pData;
int f, i, w, iPioId, Counter;
p = Ssw_SmlAllocCounterExample( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), iFrame+1 );
p = Abc_CexAlloc( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), iFrame+1 );
p->iFrame = iFrame;
p->iPo = iOut;
// fill in the binary data

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

@ -33,6 +33,7 @@
#include <time.h>
#include "vec.h"
#include "utilCex.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
@ -788,17 +789,13 @@ extern Vec_Int_t * Gia_ManCollectPoIds( Gia_Man_t * p );
extern int Gia_ObjIsMuxType( Gia_Obj_t * pNode );
extern int Gia_ObjRecognizeExor( Gia_Obj_t * pObj, Gia_Obj_t ** ppFan0, Gia_Obj_t ** ppFan1 );
extern Gia_Obj_t * Gia_ObjRecognizeMux( Gia_Obj_t * pNode, Gia_Obj_t ** ppNodeT, Gia_Obj_t ** ppNodeE );
extern Abc_Cex_t * Gia_ManAllocCounterExample( int nRegs, int nRealPis, int nFrames );
extern Abc_Cex_t * Gia_ManDeriveCexFromArray( Gia_Man_t * pAig, Vec_Int_t * vValues, int nSkip, int iFrame );
extern Abc_Cex_t * Gia_ManCreateFromComb( int nRegs, int nRealPis, int iPo, int * pModel );
extern Abc_Cex_t * Gia_ManDupCounterExample( Abc_Cex_t * p, int nRegsNew );
extern int Gia_ManVerifyCounterExample( Gia_Man_t * pAig, Abc_Cex_t * p, int fDualOut );
extern void Gia_ManPrintCounterExample( Abc_Cex_t * p );
extern int Gia_NodeMffcSize( Gia_Man_t * p, Gia_Obj_t * pNode );
extern int Gia_ManHasChoices( Gia_Man_t * p );
extern int Gia_ManHasDangling( Gia_Man_t * p );
extern Vec_Int_t * Gia_ManGetDangling( Gia_Man_t * p );
extern void Gia_ObjPrint( Gia_Man_t * p, Gia_Obj_t * pObj );
extern int Gia_ManVerifyCex( Gia_Man_t * pAig, Abc_Cex_t * p, int fDualOut );
extern int Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p );
/*=== giaCTas.c ===========================================================*/
typedef struct Tas_Man_t_ Tas_Man_t;
extern Tas_Man_t * Tas_ManAlloc( Gia_Man_t * pAig, int nBTLimit );
@ -808,8 +805,6 @@ extern void Tas_ManSatPrintStats( Tas_Man_t * p );
extern int Tas_ManSolve( Tas_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 );
extern int Tas_ManSolveArray( Tas_Man_t * p, Vec_Ptr_t * vObjs );
ABC_NAMESPACE_HEADER_END

4
src/aig/gia/giaAbs.c
View File

@ -530,8 +530,8 @@ void Gia_ManCexAbstractionStartNew( Gia_Man_t * pGia, Gia_ParAbs_t * pPars )
{
printf( "Problem is satisfiable. Found counter-example in frame %d. ", nFrames-1 );
Abc_PrintTime( 1, "Time", clk );
pGia->pCexSeq = Gia_ManDeriveCexFromArray( pGia, vCex, 0, nFrames-1 );
if ( !Gia_ManVerifyCounterExample( pGia, pGia->pCexSeq, 0 ) )
pGia->pCexSeq = Abc_CexCreate( Gia_ManRegNum(pGia), Gia_ManPiNum(pGia), Vec_IntArray(vCex), nFrames-1, 0, 0 );
if ( !Gia_ManVerifyCex( pGia, pGia->pCexSeq, 0 ) )
Abc_Print( 1, "Generated counter-example is INVALID.\n" );
pPars->Status = 0;
}

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

@ -416,7 +416,7 @@ Gia_Man_t * Gia_ManDup( Gia_Man_t * p )
}
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
if ( p->pCexSeq )
pNew->pCexSeq = Gia_ManDupCounterExample( p->pCexSeq, Gia_ManRegNum(p) );
pNew->pCexSeq = Abc_CexDup( p->pCexSeq, Gia_ManRegNum(p) );
return pNew;
}
@ -764,7 +764,7 @@ Gia_Man_t * Gia_ManDupDfs( Gia_Man_t * p )
Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
if ( p->pCexSeq )
pNew->pCexSeq = Gia_ManDupCounterExample( p->pCexSeq, Gia_ManRegNum(p) );
pNew->pCexSeq = Abc_CexDup( p->pCexSeq, Gia_ManRegNum(p) );
return pNew;
}

4
src/aig/gia/giaEra2.c
View File

@ -1758,7 +1758,7 @@ int Gia_ManArePerform( Gia_Man_t * pAig, int nStatesMax, int fMiter, int fVerbos
// verify
if ( pAig->pCexSeq )
{
if ( !Gia_ManVerifyCounterExample( pAig, pAig->pCexSeq, 0 ) )
if ( !Gia_ManVerifyCex( pAig, pAig->pCexSeq, 0 ) )
printf( "Generated counter-example is INVALID. \n" );
else
printf( "Generated counter-example verified correctly. \n" );
@ -1922,7 +1922,7 @@ Abc_Cex_t * Gia_ManAreDeriveCex( Gia_ManAre_t * p, Gia_StaAre_t * pLast )
Vec_PtrPush( vStates, pSta );
assert( Vec_PtrSize(vStates) >= 1 );
// start the counter-example
pCex = Gia_ManAllocCounterExample( Gia_ManRegNum(p->pAig), Gia_ManPiNum(p->pAig), Vec_PtrSize(vStates) );
pCex = Abc_CexAlloc( Gia_ManRegNum(p->pAig), Gia_ManPiNum(p->pAig), Vec_PtrSize(vStates) );
pCex->iFrame = Vec_PtrSize(vStates)-1;
pCex->iPo = p->iOutFail;
// compute states

4
src/aig/gia/giaSim.c
View File

@ -436,7 +436,7 @@ Abc_Cex_t * Gia_ManGenerateCounter( Gia_Man_t * pAig, int iFrame, int iOut, int
Abc_Cex_t * p;
unsigned * pData;
int f, i, w, iPioId, Counter;
p = Gia_ManAllocCounterExample( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), iFrame+1 );
p = Abc_CexAlloc( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), iFrame+1 );
p->iFrame = iFrame;
p->iPo = iOut;
// fill in the binary data
@ -513,7 +513,7 @@ int Gia_ManSimSimulate( Gia_Man_t * pAig, Gia_ParSim_t * pPars )
pPars->iOutFail = iOut;
pAig->pCexSeq = Gia_ManGenerateCounter( pAig, i, iOut, p->nWords, iPat, p->vCis2Ids );
Abc_Print( 1, "Networks are NOT EQUIVALENT. Output %d was asserted in frame %d. ", iOut, i );
if ( !Gia_ManVerifyCounterExample( pAig, pAig->pCexSeq, 0 ) )
if ( !Gia_ManVerifyCex( pAig, pAig->pCexSeq, 0 ) )
{
// Abc_Print( 1, "\n" );
Abc_Print( 1, "\nGenerated counter-example is INVALID. " );

4
src/aig/gia/giaSim2.c
View File

@ -606,7 +606,7 @@ Abc_Cex_t * Gia_Sim2GenerateCounter( Gia_Man_t * pAig, int iFrame, int iOut, int
Abc_Cex_t * p;
unsigned * pData;
int f, i, w, Counter;
p = Gia_ManAllocCounterExample( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), iFrame+1 );
p = Abc_CexAlloc( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), iFrame+1 );
p->iFrame = iFrame;
p->iPo = iOut;
// fill in the binary data
@ -663,7 +663,7 @@ int Gia_ManSimSimulateEquiv( Gia_Man_t * pAig, Gia_ParSim_t * pPars )
pPars->iOutFail = iOut;
pAig->pCexSeq = Gia_Sim2GenerateCounter( pAig, i, iOut, p->nWords, iPat );
Abc_Print( 1, "Networks are NOT EQUIVALENT. Output %d was asserted in frame %d. ", iOut, i );
if ( !Gia_ManVerifyCounterExample( pAig, pAig->pCexSeq, 0 ) )
if ( !Gia_ManVerifyCex( pAig, pAig->pCexSeq, 0 ) )
{
// Abc_Print( 1, "\n" );
Abc_Print( 1, "\nGenerated counter-example is INVALID. " );

323
src/aig/gia/giaUtil.c
View File

@ -827,244 +827,6 @@ Gia_Obj_t * Gia_ObjRecognizeMux( Gia_Obj_t * pNode, Gia_Obj_t ** ppNodeT, Gia_Ob
}
/**Function*************************************************************
Synopsis [Allocates a counter-example.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Cex_t * Gia_ManAllocCounterExample( int nRegs, int nRealPis, int nFrames )
{
Abc_Cex_t * pCex;
int nWords = Gia_BitWordNum( nRegs + nRealPis * nFrames );
pCex = (Abc_Cex_t *)ABC_ALLOC( char, sizeof(Abc_Cex_t) + sizeof(unsigned) * nWords );
memset( pCex, 0, sizeof(Abc_Cex_t) + sizeof(unsigned) * nWords );
pCex->nRegs = nRegs;
pCex->nPis = nRealPis;
pCex->nBits = nRegs + nRealPis * nFrames;
return pCex;
}
/**Function*************************************************************
Synopsis [Prints the counter-example.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManPrintCex( Abc_Cex_t * p )
{
int i, f, k;
for ( k = 0; k < p->nRegs; k++ )
printf( "%d", Gia_InfoHasBit(p->pData, k) );
printf( "\n" );
for ( f = 0; f <= p->iFrame; f++ )
{
for ( i = 0; i < p->nPis; i++ )
printf( "%d", Gia_InfoHasBit(p->pData, k++) );
printf( "\n" );
}
}
/**Function*************************************************************
Synopsis [Derives the counter-example.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Cex_t * Gia_ManDeriveCexFromArray( Gia_Man_t * pAig, Vec_Int_t * vValues, int nSkip, int iFrame )
{
Abc_Cex_t * pCex;
int i;
pCex = Gia_ManAllocCounterExample( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), iFrame+1 );
assert( Vec_IntSize(vValues) == nSkip + pCex->nBits );
pCex->iPo = 0;
pCex->iFrame = iFrame;
for ( i = 0; i < pCex->nBits; i++ )
if ( Vec_IntEntry(vValues, nSkip + i) )
Gia_InfoSetBit( pCex->pData, i );
return pCex;
}
/**Function*************************************************************
Synopsis [Allocates a counter-example.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Cex_t * Gia_ManCreateFromComb( int nRegs, int nRealPis, int iPo, int * pModel )
{
Abc_Cex_t * pCex;
int i;
pCex = Gia_ManAllocCounterExample( nRegs, nRealPis, 1 );
pCex->iPo = iPo;
pCex->iFrame = 0;
for ( i = pCex->nRegs; i < pCex->nBits; i++ )
if ( pModel[i-pCex->nRegs] )
Gia_InfoSetBit( pCex->pData, i );
return pCex;
}
/**Function*************************************************************
Synopsis [Resimulates the counter-example.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ManVerifyCounterExample( Gia_Man_t * pAig, Abc_Cex_t * p, int fDualOut )
{
Gia_Obj_t * pObj, * pObjRi, * pObjRo;
int RetValue, i, k, iBit = 0;
Gia_ManCleanMark0(pAig);
Gia_ManForEachRo( pAig, pObj, i )
pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++);
for ( i = 0; i <= p->iFrame; i++ )
{
Gia_ManForEachPi( pAig, pObj, k )
pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++);
Gia_ManForEachAnd( pAig, pObj, k )
pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) &
(Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
Gia_ManForEachCo( pAig, pObj, k )
pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
if ( i == p->iFrame )
break;
Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, k )
{
pObjRo->fMark0 = pObjRi->fMark0;
}
}
assert( iBit == p->nBits );
if ( fDualOut )
RetValue = Gia_ManPo(pAig, 2*p->iPo)->fMark0 ^ Gia_ManPo(pAig, 2*p->iPo+1)->fMark0;
else
RetValue = Gia_ManPo(pAig, p->iPo)->fMark0;
Gia_ManCleanMark0(pAig);
return RetValue;
}
/**Function*************************************************************
Synopsis [Resimulates the counter-example.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ManVerifyCounterExampleAllOuts( Gia_Man_t * pAig, Abc_Cex_t * p )
{
Gia_Obj_t * pObj, * pObjRi, * pObjRo;
int RetValue, i, k, iBit = 0;
Gia_ManCleanMark0(pAig);
Gia_ManForEachRo( pAig, pObj, i )
pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++);
for ( i = 0; i <= p->iFrame; i++ )
{
Gia_ManForEachPi( pAig, pObj, k )
pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++);
Gia_ManForEachAnd( pAig, pObj, k )
pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) &
(Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
Gia_ManForEachCo( pAig, pObj, k )
pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, k )
pObjRo->fMark0 = pObjRi->fMark0;
}
assert( iBit == p->nBits );
// remember the number of failed output
RetValue = -1;
Gia_ManForEachPo( pAig, pObj, i )
if ( Gia_ManPo(pAig, i)->fMark0 )
{
RetValue = i;
break;
}
Gia_ManCleanMark0(pAig);
return RetValue;
}
/**Function*************************************************************
Synopsis [Make the trivial counter-example for the trivially asserted output.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Cex_t * Gia_ManDupCounterExample( Abc_Cex_t * p, int nRegsNew )
{
Abc_Cex_t * pCex;
int i;
pCex = Gia_ManAllocCounterExample( nRegsNew, p->nPis, p->iFrame+1 );
pCex->iPo = p->iPo;
pCex->iFrame = p->iFrame;
for ( i = p->nRegs; i < p->nBits; i++ )
if ( Gia_InfoHasBit(p->pData, i) )
Gia_InfoSetBit( pCex->pData, pCex->nRegs + i - p->nRegs );
return pCex;
}
/**Function*************************************************************
Synopsis [Prints out the counter-example.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManPrintCounterExample( Abc_Cex_t * p )
{
int i, f, k;
printf( "Counter-example: iPo = %d iFrame = %d nRegs = %d nPis = %d nBits = %d\n",
p->iPo, p->iFrame, p->nRegs, p->nPis, p->nBits );
printf( "State : " );
for ( k = 0; k < p->nRegs; k++ )
printf( "%d", Gia_InfoHasBit(p->pData, k) );
printf( "\n" );
for ( f = 0; f <= p->iFrame; f++ )
{
printf( "Frame %2d : ", f );
for ( i = 0; i < p->nPis; i++ )
printf( "%d", Gia_InfoHasBit(p->pData, k++) );
printf( "\n" );
}
assert( k == p->nBits );
}
/**Function*************************************************************
Synopsis [Dereferences the node's MFFC.]
@ -1371,6 +1133,91 @@ void Gia_ObjPrint( Gia_Man_t * p, Gia_Obj_t * pObj )
*/
}
/**Function*************************************************************
Synopsis [Resimulates the counter-example.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ManVerifyCex( Gia_Man_t * pAig, Abc_Cex_t * p, int fDualOut )
{
Gia_Obj_t * pObj, * pObjRi, * pObjRo;
int RetValue, i, k, iBit = 0;
Gia_ManCleanMark0(pAig);
Gia_ManForEachRo( pAig, pObj, i )
pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++);
for ( i = 0; i <= p->iFrame; i++ )
{
Gia_ManForEachPi( pAig, pObj, k )
pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++);
Gia_ManForEachAnd( pAig, pObj, k )
pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) &
(Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
Gia_ManForEachCo( pAig, pObj, k )
pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
if ( i == p->iFrame )
break;
Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, k )
{
pObjRo->fMark0 = pObjRi->fMark0;
}
}
assert( iBit == p->nBits );
if ( fDualOut )
RetValue = Gia_ManPo(pAig, 2*p->iPo)->fMark0 ^ Gia_ManPo(pAig, 2*p->iPo+1)->fMark0;
else
RetValue = Gia_ManPo(pAig, p->iPo)->fMark0;
Gia_ManCleanMark0(pAig);
return RetValue;
}
/**Function*************************************************************
Synopsis [Resimulates the counter-example.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p )
{
Gia_Obj_t * pObj, * pObjRi, * pObjRo;
int RetValue, i, k, iBit = 0;
Gia_ManCleanMark0(pAig);
Gia_ManForEachRo( pAig, pObj, i )
pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++);
for ( i = 0; i <= p->iFrame; i++ )
{
Gia_ManForEachPi( pAig, pObj, k )
pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++);
Gia_ManForEachAnd( pAig, pObj, k )
pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) &
(Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
Gia_ManForEachCo( pAig, pObj, k )
pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, k )
pObjRo->fMark0 = pObjRi->fMark0;
}
assert( iBit == p->nBits );
// remember the number of failed output
RetValue = -1;
Gia_ManForEachPo( pAig, pObj, i )
if ( Gia_ManPo(pAig, i)->fMark0 )
{
RetValue = i;
break;
}
Gia_ManCleanMark0(pAig);
return RetValue;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///

4
src/aig/int/intCtrex.c
View File

@ -133,7 +133,7 @@ void * Inter_ManGetCounterExample( Aig_Man_t * pAig, int nFrames, int fVerbose )
if ( status == l_True )
{
int i, * pModel = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize );
pCtrex = Ssw_SmlAllocCounterExample( Saig_ManRegNum(pAig), Saig_ManPiNum(pAig), nFrames );
pCtrex = Abc_CexAlloc( Saig_ManRegNum(pAig), Saig_ManPiNum(pAig), nFrames );
pCtrex->iFrame = nFrames - 1;
pCtrex->iPo = 0;
for ( i = 0; i < Vec_IntSize(vCiIds); i++ )
@ -145,7 +145,7 @@ void * Inter_ManGetCounterExample( Aig_Man_t * pAig, int nFrames, int fVerbose )
sat_solver_delete( pSat );
Vec_IntFree( vCiIds );
// verify counter-example
status = Ssw_SmlRunCounterExample( pAig, pCtrex );
status = Saig_ManVerifyCex( pAig, pCtrex );
if ( status == 0 )
printf( "Inter_ManGetCounterExample(): Counter-example verification has FAILED.\n" );
// report the results

5
src/aig/llb/llb2Core.c
View File

@ -94,7 +94,6 @@ DdNode * Llb_CoreComputeCube( DdManager * dd, Vec_Int_t * vVars, int fUseVarInde
***********************************************************************/
Abc_Cex_t * Llb_CoreDeriveCex( Llb_Img_t * p )
{
extern Abc_Cex_t * Ssw_SmlAllocCounterExample( int nRegs, int nRealPis, int nFrames );
Abc_Cex_t * pCex;
Aig_Obj_t * pObj;
Vec_Ptr_t * vSupps, * vQuant0, * vQuant1;
@ -112,7 +111,7 @@ Abc_Cex_t * Llb_CoreDeriveCex( Llb_Img_t * p )
// Llb_ImgQuantifyFirst( p->pAig, p->vDdMans, vQuant0 );
// allocate room for the counter-example
pCex = Ssw_SmlAllocCounterExample( Saig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Vec_PtrSize(p->vRings) );
pCex = Abc_CexAlloc( Saig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Vec_PtrSize(p->vRings) );
pCex->iFrame = Vec_PtrSize(p->vRings) - 1;
pCex->iPo = -1;
@ -178,7 +177,7 @@ Abc_Cex_t * Llb_CoreDeriveCex( Llb_Img_t * p )
}
assert( nPiOffset == Saig_ManRegNum(p->pAig) );
// update the output number
RetValue = Ssw_SmlFindOutputCounterExample( p->pInit, pCex );
RetValue = Saig_ManFindFailedPoCex( p->pInit, pCex );
assert( RetValue >= 0 && RetValue < Saig_ManPoNum(p->pInit) ); // invalid CEX!!!
pCex->iPo = RetValue;
// cleanup

6
src/aig/llb/llb3Nonlin.c
View File

@ -237,7 +237,6 @@ DdNode * Llb_NonlinComputeInitState( Aig_Man_t * pAig, DdManager * dd )
***********************************************************************/
Abc_Cex_t * Llb_NonlinDeriveCex( Llb_Mnn_t * p )
{
extern Abc_Cex_t * Ssw_SmlAllocCounterExample( int nRegs, int nRealPis, int nFrames );
Abc_Cex_t * pCex;
Aig_Obj_t * pObj;
Vec_Int_t * vVarsNs;
@ -263,7 +262,7 @@ Abc_Cex_t * Llb_NonlinDeriveCex( Llb_Mnn_t * p )
printf( "\n" );
*/
// allocate room for the counter-example
pCex = Ssw_SmlAllocCounterExample( Saig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Vec_PtrSize(p->vRings) );
pCex = Abc_CexAlloc( Saig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Vec_PtrSize(p->vRings) );
pCex->iFrame = Vec_PtrSize(p->vRings) - 1;
pCex->iPo = -1;
@ -330,7 +329,8 @@ Abc_Cex_t * Llb_NonlinDeriveCex( Llb_Mnn_t * p )
}
assert( nPiOffset == Saig_ManRegNum(p->pAig) );
// update the output number
RetValue = Ssw_SmlFindOutputCounterExample( p->pInit, pCex );
//Abc_CexPrint( pCex );
RetValue = Saig_ManFindFailedPoCex( p->pInit, pCex );
assert( RetValue >= 0 && RetValue < Saig_ManPoNum(p->pInit) ); // invalid CEX!!!
pCex->iPo = RetValue;
// cleanup

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

@ -149,6 +149,8 @@ extern Aig_Man_t * Saig_ManDupUnfoldConstrsFunc( Aig_Man_t * pAig, int nFr
extern Aig_Man_t * Saig_ManDupOrpos( Aig_Man_t * p );
extern Aig_Man_t * Saig_ManCreateEquivMiter( Aig_Man_t * pAig, Vec_Int_t * vPairs );
extern Aig_Man_t * Saig_ManDeriveAbstraction( Aig_Man_t * pAig, Vec_Int_t * vFlops );
extern int Saig_ManVerifyCex( Aig_Man_t * pAig, Abc_Cex_t * p );
extern int Saig_ManFindFailedPoCex( Aig_Man_t * pAig, Abc_Cex_t * p );
/*=== saigHaig.c ==========================================================*/
extern Aig_Man_t * Saig_ManHaigRecord( Aig_Man_t * p, int nIters, int nSteps, int fRetimingOnly, int fAddBugs, int fUseCnf, int fVerbose );
/*=== saigInd.c ==========================================================*/

10
src/aig/saig/saigAbs.c
View File

@ -101,12 +101,12 @@ Abc_Cex_t * Saig_ManCexRemap( Aig_Man_t * p, Aig_Man_t * pAbs, Abc_Cex_t * pCexA
Abc_Cex_t * pCex;
Aig_Obj_t * pObj;
int i, f;
if ( !Ssw_SmlRunCounterExample( pAbs, pCexAbs ) )
if ( !Saig_ManVerifyCex( pAbs, pCexAbs ) )
printf( "Saig_ManCexRemap(): The intial counter-example is invalid.\n" );
else
printf( "Saig_ManCexRemap(): The intial counter-example is correct.\n" );
// start the counter-example
pCex = Ssw_SmlAllocCounterExample( Aig_ManRegNum(p), Saig_ManPiNum(p), pCexAbs->iFrame+1 );
pCex = Abc_CexAlloc( Aig_ManRegNum(p), Saig_ManPiNum(p), pCexAbs->iFrame+1 );
pCex->iFrame = pCexAbs->iFrame;
pCex->iPo = pCexAbs->iPo;
// copy the bit data
@ -121,10 +121,10 @@ Abc_Cex_t * Saig_ManCexRemap( Aig_Man_t * p, Aig_Man_t * pAbs, Abc_Cex_t * pCexA
}
}
// verify the counter example
if ( !Ssw_SmlRunCounterExample( p, pCex ) )
if ( !Saig_ManVerifyCex( p, pCex ) )
{
printf( "Saig_ManCexRemap(): Counter-example is invalid.\n" );
Ssw_SmlFreeCounterExample( pCex );
Abc_CexFree( pCex );
pCex = NULL;
}
else
@ -194,7 +194,7 @@ Aig_Man_t * Saig_ManCexRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlo
printf( "Running property directed reachability...\n" );
RetValue = Pdr_ManSolve( pAbsOrpos, pPars, &pCex );
if ( pCex )
pCex->iPo = Ssw_SmlFindOutputCounterExample( pAbs, pCex );
pCex->iPo = Saig_ManFindFailedPoCex( pAbs, pCex );
Aig_ManStop( pAbsOrpos );
pAbs->pSeqModel = pCex;
if ( RetValue )

3
src/aig/saig/saigBmc.c
View File

@ -301,11 +301,10 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
}
else if ( status == l_True )
{
// extern void * Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, int * pModel );
Vec_Int_t * vCiIds = Cnf_DataCollectPiSatNums( pCnf, pFrames );
int * pModel = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize );
pModel[Aig_ManPiNum(pFrames)] = pObj->Id;
pAig->pSeqModel = (Abc_Cex_t *)Fra_SmlCopyCounterExample( pAig, pFrames, pModel );
pAig->pSeqModel = Fra_SmlCopyCounterExample( pAig, pFrames, pModel );
ABC_FREE( pModel );
Vec_IntFree( vCiIds );

6
src/aig/saig/saigBmc2.c
View File

@ -637,7 +637,7 @@ Abc_Cex_t * Saig_BmcGenerateCounterExample( Saig_Bmc_t * p )
Aig_Obj_t * pObj, * pObjFrm;
int i, f, iVarNum;
// start the counter-example
pCex = Ssw_SmlAllocCounterExample( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), p->iFrameFail+1 );
pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), p->iFrameFail+1 );
pCex->iFrame = p->iFrameFail;
pCex->iPo = p->iOutputFail;
// copy the bit data
@ -656,10 +656,10 @@ Abc_Cex_t * Saig_BmcGenerateCounterExample( Saig_Bmc_t * p )
}
}
// verify the counter example
if ( !Ssw_SmlRunCounterExample( p->pAig, pCex ) )
if ( !Saig_ManVerifyCex( p->pAig, pCex ) )
{
printf( "Saig_BmcGenerateCounterExample(): Counter-example is invalid.\n" );
Ssw_SmlFreeCounterExample( pCex );
Abc_CexFree( pCex );
pCex = NULL;
}
return pCex;

6
src/aig/saig/saigBmc3.c
View File

@ -1108,8 +1108,7 @@ clkOther += clock() - clk2;
continue;
if ( Lit == 1 )
{
extern Abc_Cex_t * Fra_SmlTrivCounterExample( Aig_Man_t * pAig, int iFrameOut );
Abc_Cex_t * pCex = Fra_SmlTrivCounterExample( pAig, f*Saig_ManPoNum(pAig)+i );
Abc_Cex_t * pCex = Abc_CexMakeTriv( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), f*Saig_ManPoNum(pAig)+i );
printf( "Output %d is trivially SAT in frame %d.\n", i, f );
if ( !pPars->fSolveAll )
{
@ -1137,9 +1136,8 @@ clkOther += clock() - clk2;
}
else if ( status == l_True )
{
// extern void * Fra_SmlSimpleCounterExample( Aig_Man_t * p, int * pModel, int iFrame, int iPo );
int * pModel = Sat_SolverGetModel( p->pSat, Vec_IntArray(p->vPiVars), Vec_IntSize(p->vPiVars) );
Abc_Cex_t * pCex = Fra_SmlSimpleCounterExample( pAig, pModel, f, i );
Abc_Cex_t * pCex = Abc_CexCreate( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), pModel, f, i, 1 );
ABC_FREE( pModel );
fFirst = 0;
if ( !pPars->fSolveAll )

85
src/aig/saig/saigDup.c
View File

@ -265,6 +265,91 @@ Aig_Man_t * Saig_ManDeriveAbstraction( Aig_Man_t * p, Vec_Int_t * vFlops )
return pNew;
}
/**Function*************************************************************
Synopsis [Resimulates the counter-example.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Saig_ManVerifyCex( Aig_Man_t * pAig, Abc_Cex_t * p )
{
Aig_Obj_t * pObj, * pObjRi, * pObjRo;
int RetValue, i, k, iBit = 0;
Aig_ManCleanMarkB(pAig);
Aig_ManConst1(pAig)->fMarkB = 1;
Saig_ManForEachLo( pAig, pObj, i )
pObj->fMarkB = Aig_InfoHasBit(p->pData, iBit++);
for ( i = 0; i <= p->iFrame; i++ )
{
Saig_ManForEachPi( pAig, pObj, k )
pObj->fMarkB = Aig_InfoHasBit(p->pData, iBit++);
Aig_ManForEachNode( pAig, pObj, k )
pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) &
(Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj));
Aig_ManForEachPo( pAig, pObj, k )
pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj);
if ( i == p->iFrame )
break;
Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, k )
pObjRo->fMarkB = pObjRi->fMarkB;
}
assert( iBit == p->nBits );
RetValue = Aig_ManPo(pAig, p->iPo)->fMarkB;
Aig_ManCleanMarkB(pAig);
return RetValue;
}
/**Function*************************************************************
Synopsis [Resimulates the counter-example.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Saig_ManFindFailedPoCex( Aig_Man_t * pAig, Abc_Cex_t * p )
{
Aig_Obj_t * pObj, * pObjRi, * pObjRo;
int RetValue, i, k, iBit = 0;
Aig_ManCleanMarkB(pAig);
Aig_ManConst1(pAig)->fMarkB = 1;
Saig_ManForEachLo( pAig, pObj, i )
pObj->fMarkB = Aig_InfoHasBit(p->pData, iBit++);
for ( i = 0; i <= p->iFrame; i++ )
{
Saig_ManForEachPi( pAig, pObj, k )
pObj->fMarkB = Aig_InfoHasBit(p->pData, iBit++);
Aig_ManForEachNode( pAig, pObj, k )
pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) &
(Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj));
Aig_ManForEachPo( pAig, pObj, k )
pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj);
if ( i == p->iFrame )
break;
Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, k )
pObjRo->fMarkB = pObjRi->fMarkB;
}
assert( iBit == p->nBits );
// remember the number of failed output
RetValue = -1;
Saig_ManForEachPo( pAig, pObj, i )
if ( pObj->fMarkB )
{
RetValue = i;
break;
}
Aig_ManCleanMarkB(pAig);
return RetValue;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

2
src/aig/saig/saigSimSeq.c
View File

@ -418,7 +418,7 @@ Abc_Cex_t * Raig_ManGenerateCounter( Aig_Man_t * pAig, int iFrame, int iOut, int
Abc_Cex_t * p;
unsigned * pData;
int f, i, w, iPioId, Counter;
p = Ssw_SmlAllocCounterExample( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), iFrame+1 );
p = Abc_CexAlloc( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), iFrame+1 );
p->iFrame = iFrame;
p->iPo = iOut;
// fill in the binary data

9
src/aig/ssw/ssw.h
View File

@ -123,18 +123,9 @@ extern int Ssw_SmlNumFrames( Ssw_Sml_t * p );
extern int Ssw_SmlNumWordsTotal( Ssw_Sml_t * p );
extern unsigned * Ssw_SmlSimInfo( Ssw_Sml_t * p, Aig_Obj_t * pObj );
extern int Ssw_SmlObjsAreEqualWord( Ssw_Sml_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
extern Abc_Cex_t * Ssw_SmlAllocCounterExample( int nRegs, int nRealPis, int nFrames );
extern void Ssw_SmlFreeCounterExample( Abc_Cex_t * pCex );
extern int Ssw_SmlRunCounterExample( Aig_Man_t * pAig, Abc_Cex_t * p );
extern int Ssw_SmlFindOutputCounterExample( Aig_Man_t * pAig, Abc_Cex_t * p );
extern Abc_Cex_t * Ssw_SmlDupCounterExample( Abc_Cex_t * p, int nRegsNew );
ABC_NAMESPACE_HEADER_END
#endif
////////////////////////////////////////////////////////////////////////

2
src/aig/ssw/sswBmc.c
View File

@ -94,7 +94,7 @@ Abc_Cex_t * Ssw_BmcGetCounterExample( Ssw_Frm_t * pFrm, Ssw_Sat_t * pSat, int iP
int f, i, nShift;
assert( Saig_ManRegNum(pFrm->pAig) > 0 );
// allocate the counter example
pCex = Ssw_SmlAllocCounterExample( Saig_ManRegNum(pFrm->pAig), Saig_ManPiNum(pFrm->pAig), iFrame + 1 );
pCex = Abc_CexAlloc( Saig_ManRegNum(pFrm->pAig), Saig_ManPiNum(pFrm->pAig), iFrame + 1 );
pCex->iPo = iPo;
pCex->iFrame = iFrame;
// create data-bits

243
src/aig/ssw/sswSim.c
View File

@ -1248,131 +1248,6 @@ unsigned * Ssw_SmlSimInfo( Ssw_Sml_t * p, Aig_Obj_t * pObj )
return Ssw_ObjSim( p, pObj->Id );
}
/**Function*************************************************************
Synopsis [Allocates a counter-example.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Cex_t * Ssw_SmlAllocCounterExample( int nRegs, int nRealPis, int nFrames )
{
Abc_Cex_t * pCex;
int nWords = Aig_BitWordNum( nRegs + nRealPis * nFrames );
pCex = (Abc_Cex_t *)ABC_ALLOC( char, sizeof(Abc_Cex_t) + sizeof(unsigned) * nWords );
memset( pCex, 0, sizeof(Abc_Cex_t) + sizeof(unsigned) * nWords );
pCex->nRegs = nRegs;
pCex->nPis = nRealPis;
pCex->nBits = nRegs + nRealPis * nFrames;
return pCex;
}
/**Function*************************************************************
Synopsis [Frees the counter-example.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ssw_SmlFreeCounterExample( Abc_Cex_t * pCex )
{
ABC_FREE( pCex );
}
/**Function*************************************************************
Synopsis [Resimulates the counter-example.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ssw_SmlRunCounterExample( Aig_Man_t * pAig, Abc_Cex_t * p )
{
Ssw_Sml_t * pSml;
Aig_Obj_t * pObj;
int RetValue, i, k, iBit;
if ( Saig_ManPiNum(pAig) != p->nPis )
return 0;
// if ( Saig_ManRegNum(pAig) != p->nRegs )
// return 0;
// assert( Aig_ManRegNum(pAig) > 0 );
// assert( Aig_ManRegNum(pAig) < Aig_ManPiNum(pAig) );
// start a new sequential simulator
pSml = Ssw_SmlStart( pAig, 0, p->iFrame+1, 1 );
// assign simulation info for the registers
iBit = 0;
Saig_ManForEachLo( pAig, pObj, i )
Ssw_SmlObjAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), 0 );
// assign simulation info for the primary inputs
iBit = Saig_ManRegNum(pAig);
for ( i = 0; i <= p->iFrame; i++ )
Saig_ManForEachPi( pAig, pObj, k )
Ssw_SmlObjAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), i );
// assert( iBit == p->nBits );
// run random simulation
Ssw_SmlSimulateOne( pSml );
// check if the given output has failed
RetValue = !Ssw_SmlNodeIsZeroFrame( pSml, Aig_ManPo(pAig, p->iPo), p->iFrame );
Ssw_SmlStop( pSml );
return RetValue;
}
/**Function*************************************************************
Synopsis [Resimulates the counter-example.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ssw_SmlFindOutputCounterExample( Aig_Man_t * pAig, Abc_Cex_t * p )
{
Ssw_Sml_t * pSml;
Aig_Obj_t * pObj;
int i, k, iBit, iOut;
assert( Aig_ManRegNum(pAig) > 0 );
assert( Aig_ManRegNum(pAig) < Aig_ManPiNum(pAig) );
// start a new sequential simulator
pSml = Ssw_SmlStart( pAig, 0, p->iFrame+1, 1 );
// assign simulation info for the registers
iBit = 0;
Saig_ManForEachLo( pAig, pObj, i )
Ssw_SmlObjAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), 0 );
// assign simulation info for the primary inputs
for ( i = 0; i <= p->iFrame; i++ )
Saig_ManForEachPi( pAig, pObj, k )
Ssw_SmlObjAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), i );
assert( iBit == p->nBits );
// run random simulation
Ssw_SmlSimulateOne( pSml );
// check if the given output has failed
iOut = -1;
Saig_ManForEachPo( pAig, pObj, k )
if ( !Ssw_SmlNodeIsZeroFrame( pSml, Aig_ManPo(pAig, k), p->iFrame ) )
{
iOut = k;
break;
}
Ssw_SmlStop( pSml );
return iOut;
}
/**Function*************************************************************
Synopsis [Creates sequential counter-example from the simulation info.]
@ -1417,7 +1292,7 @@ Abc_Cex_t * Ssw_SmlGetCounterExample( Ssw_Sml_t * p )
assert( iBit < 32 * p->nWordsFrame );
// allocate the counter example
pCex = Ssw_SmlAllocCounterExample( Aig_ManRegNum(p->pAig), Aig_ManPiNum(p->pAig) - Aig_ManRegNum(p->pAig), iFrame + 1 );
pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig), Aig_ManPiNum(p->pAig) - Aig_ManRegNum(p->pAig), iFrame + 1 );
pCex->iPo = iPo;
pCex->iFrame = iFrame;
@ -1438,126 +1313,14 @@ Abc_Cex_t * Ssw_SmlGetCounterExample( Ssw_Sml_t * p )
}
}
// verify the counter example
if ( !Ssw_SmlRunCounterExample( p->pAig, pCex ) )
if ( !Saig_ManVerifyCex( p->pAig, pCex ) )
{
printf( "Ssw_SmlGetCounterExample(): Counter-example is invalid.\n" );
Ssw_SmlFreeCounterExample( pCex );
Abc_CexFree( pCex );
pCex = NULL;
}
return pCex;
}
/**Function*************************************************************
Synopsis [Generates seq counter-example from the combinational one.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Cex_t * Ssw_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, int * pModel )
{
Abc_Cex_t * pCex;
Aig_Obj_t * pObj;
int i, nFrames, nTruePis, nTruePos, iPo, iFrame;
// get the number of frames
assert( Aig_ManRegNum(pAig) > 0 );
assert( Aig_ManRegNum(pFrames) == 0 );
nTruePis = Aig_ManPiNum(pAig)-Aig_ManRegNum(pAig);
nTruePos = Aig_ManPoNum(pAig)-Aig_ManRegNum(pAig);
nFrames = Aig_ManPiNum(pFrames) / nTruePis;
assert( nTruePis * nFrames == Aig_ManPiNum(pFrames) );
assert( nTruePos * nFrames == Aig_ManPoNum(pFrames) );
// find the PO that failed
iPo = -1;
iFrame = -1;
Aig_ManForEachPo( pFrames, pObj, i )
if ( pObj->Id == pModel[Aig_ManPiNum(pFrames)] )
{
iPo = i % nTruePos;
iFrame = i / nTruePos;
break;
}
assert( iPo >= 0 );
// allocate the counter example
pCex = Ssw_SmlAllocCounterExample( Aig_ManRegNum(pAig), nTruePis, iFrame + 1 );
pCex->iPo = iPo;
pCex->iFrame = iFrame;
// copy the bit data
for ( i = 0; i < Aig_ManPiNum(pFrames); i++ )
{
if ( pModel[i] )
Aig_InfoSetBit( pCex->pData, pCex->nRegs + i );
if ( pCex->nRegs + i == pCex->nBits - 1 )
break;
}
// verify the counter example
if ( !Ssw_SmlRunCounterExample( pAig, pCex ) )
{
printf( "Ssw_SmlGetCounterExample(): Counter-example is invalid.\n" );
Ssw_SmlFreeCounterExample( pCex );
pCex = NULL;
}
return pCex;
}
/**Function*************************************************************
Synopsis [Make the trivial counter-example for the trivially asserted output.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Cex_t * Ssw_SmlTrivCounterExample( Aig_Man_t * pAig, int iFrameOut )
{
Abc_Cex_t * pCex;
int nTruePis, nTruePos, iPo, iFrame;
assert( Aig_ManRegNum(pAig) > 0 );
nTruePis = Aig_ManPiNum(pAig)-Aig_ManRegNum(pAig);
nTruePos = Aig_ManPoNum(pAig)-Aig_ManRegNum(pAig);
iPo = iFrameOut % nTruePos;
iFrame = iFrameOut / nTruePos;
// allocate the counter example
pCex = Ssw_SmlAllocCounterExample( Aig_ManRegNum(pAig), nTruePis, iFrame + 1 );
pCex->iPo = iPo;
pCex->iFrame = iFrame;
return pCex;
}
/**Function*************************************************************
Synopsis [Make the trivial counter-example for the trivially asserted output.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Cex_t * Ssw_SmlDupCounterExample( Abc_Cex_t * p, int nRegsNew )
{
Abc_Cex_t * pCex;
int i;
pCex = Ssw_SmlAllocCounterExample( nRegsNew, p->nPis, p->iFrame+1 );
pCex->iPo = p->iPo;
pCex->iFrame = p->iFrame;
for ( i = p->nRegs; i < p->nBits; i++ )
if ( Aig_InfoHasBit(p->pData, i) )
Aig_InfoSetBit( pCex->pData, pCex->nRegs + i - p->nRegs );
return pCex;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///

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

@ -38,6 +38,7 @@
#include "extra.h"
#include "stmm.h"
#include "nm.h"
#include "utilCex.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///

4
src/base/abc/abcNtk.c
View File

@ -131,9 +131,7 @@ Abc_Ntk_t * Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_
if ( pNtk->vOnehots )
pNtkNew->vOnehots = (Vec_Ptr_t *)Vec_VecDupInt( (Vec_Vec_t *)pNtk->vOnehots );
if ( pNtk->pSeqModel )
{
pNtkNew->pSeqModel = Gia_ManDupCounterExample( pNtk->pSeqModel, Abc_NtkLatchNum(pNtk) );
}
pNtkNew->pSeqModel = Abc_CexDup( pNtk->pSeqModel, Abc_NtkLatchNum(pNtk) );
// check that the CI/CO/latches are copied correctly
assert( Abc_NtkCiNum(pNtk) == Abc_NtkCiNum(pNtkNew) );
assert( Abc_NtkCoNum(pNtk) == Abc_NtkCoNum(pNtkNew) );

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

@ -17580,7 +17580,7 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pSimInfo[0] != 1 )
Abc_Print( 1, "ERROR in Abc_NtkMiterSat(): Generated counter example is invalid.\n" );
ABC_FREE( pSimInfo );
pAbc->pCex = Gia_ManCreateFromComb( 0, Abc_NtkPiNum(pNtk), 0, pNtk->pModel );
pAbc->pCex = Abc_CexCreate( 0, Abc_NtkPiNum(pNtk), pNtk->pModel, 0, 0, 0 );
}
pAbc->Status = RetValue;
if ( RetValue == -1 )
@ -19840,8 +19840,7 @@ int Abc_CommandTestCex( Abc_Frame_t * pAbc, int argc, char ** argv )
extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 );
Gia_Man_t * pGia = Gia_ManFromAigSimple( pAig );
if ( !Gia_ManVerifyCounterExample( pGia, pAbc->pCex, 0 ) )
// if ( !Ssw_SmlRunCounterExample( pAig, pAbc->pCex ) )
if ( !Gia_ManVerifyCex( pGia, pAbc->pCex, 0 ) )
Abc_Print( 1, "Main AIG: The cex does not fail any outputs.\n" );
else
Abc_Print( 1, "Main AIG: The cex is correct.\n" );
@ -19860,7 +19859,7 @@ int Abc_CommandTestCex( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( 1, "And AIG: The number of POs (%d) is less than the PO index in cex (%d).\n", Gia_ManPoNum(pAbc->pGia), pAbc->pCex->iPo );
else
{
if ( !Gia_ManVerifyCounterExample( pAbc->pGia, pAbc->pCex, 0 ) )
if ( !Gia_ManVerifyCex( pAbc->pGia, pAbc->pCex, 0 ) )
Abc_Print( 1, "And AIG: The cex does not fail any outputs.\n" );
else
Abc_Print( 1, "And AIG: The cex is correct.\n" );

25
src/base/abci/abcDar.c
View File

@ -21,7 +21,6 @@
#include "abc.h"
#include "main.h"
#include "giaAig.h"
#include "saig.h"
#include "dar.h"
#include "cnf.h"
#include "fra.h"
@ -1790,7 +1789,7 @@ ABC_PRT( "Time", clock() - clk );
// verify counter-example
if ( pNtk->pSeqModel )
{
status = Ssw_SmlRunCounterExample( pMan, pNtk->pSeqModel );
status = Saig_ManVerifyCex( pMan, pNtk->pSeqModel );
if ( status == 0 )
printf( "Abc_NtkDarBmc(): Counter-example verification has FAILED.\n" );
}
@ -1857,7 +1856,7 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars )
ABC_PRT( "Time", clock() - clk );
if ( pNtk->pSeqModel )
{
status = Ssw_SmlRunCounterExample( pMan, pNtk->pSeqModel );
status = Saig_ManVerifyCex( pMan, pNtk->pSeqModel );
if ( status == 0 )
printf( "Abc_NtkDarBmc3(): Counter-example verification has FAILED.\n" );
}
@ -1902,7 +1901,7 @@ int Abc_NtkDarBmcInter_int( Aig_Man_t * pMan, Inter_ManParams_t * pPars, Aig_Man
pTemp->pSeqModel = NULL;
RetValue = Fra_FraigSat( pTemp, pPars->nBTLimit, 0, 0, 0, 0 );
if ( pTemp->pData )
pTemp->pSeqModel = Gia_ManCreateFromComb( Aig_ManRegNum(pMan), Saig_ManPiNum(pMan), i, (int *)pTemp->pData );
pTemp->pSeqModel = Abc_CexCreate( Aig_ManRegNum(pMan), Saig_ManPiNum(pMan), (int *)pTemp->pData, 0, i, 1 );
// pNtk->pModel = pTemp->pData, pTemp->pData = NULL;
}
else
@ -2150,7 +2149,7 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar )
{
Abc_Cex_t * pCex = pNtk->pSeqModel;
printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness).\n", pCex->iPo, pCex->iFrame );
if ( !Ssw_SmlRunCounterExample( pMan, pNtk->pSeqModel ) )
if ( !Saig_ManVerifyCex( pMan, pNtk->pSeqModel ) )
printf( "Abc_NtkDarProve(): Counter-example verification has FAILED.\n" );
}
}
@ -2274,7 +2273,7 @@ int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex )
Aig_Man_t * pTemp = Saig_ManDupOrpos( pMan );
RetValue = Pdr_ManSolve( pTemp, pPars, ppCex );
if ( RetValue == 0 )
(*ppCex)->iPo = Ssw_SmlFindOutputCounterExample( pMan, *ppCex );
(*ppCex)->iPo = Saig_ManFindFailedPoCex( pMan, *ppCex );
Aig_ManStop( pTemp );
}
else
@ -2290,7 +2289,7 @@ int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex )
assert( 0 );
ABC_PRT( "Time", clock() - clk );
if ( *ppCex && !Ssw_SmlRunCounterExample( pMan, *ppCex ) )
if ( *ppCex && !Saig_ManVerifyCex( pMan, *ppCex ) )
printf( "Abc_NtkDarPdr(): Counter-example verification has FAILED.\n" );
Aig_ManStop( pMan );
return RetValue;
@ -2710,7 +2709,7 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
{
printf( "Simulation iterated %d times with %d words asserted output %d in frame %d. ",
nFrames, nWords, pCex->iPo, pCex->iFrame );
status = Ssw_SmlRunCounterExample( pMan, pCex );
status = Saig_ManVerifyCex( pMan, pCex );
if ( status == 0 )
printf( "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" );
}
@ -2737,7 +2736,7 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
{
printf( "Simulation of %d frames with %d words asserted output %d in frame %d. ",
nFrames, nWords, pCex->iPo, pCex->iFrame );
status = Ssw_SmlRunCounterExample( pMan, pCex );
status = Saig_ManVerifyCex( pMan, pCex );
if ( status == 0 )
printf( "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" );
}
@ -2767,7 +2766,7 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
{
printf( "Simulation of %d frames with %d words asserted output %d in frame %d. ",
nFrames, nWords, pCex->iPo, pCex->iFrame );
status = Ssw_SmlRunCounterExample( pMan, pCex );
status = Saig_ManVerifyCex( pMan, pCex );
if ( status == 0 )
printf( "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" );
}
@ -2798,7 +2797,7 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
{
printf( "Simulation of %d frames with %d words asserted output %d in frame %d. ",
nFrames, nWords, pGia->pCexSeq->iPo, pGia->pCexSeq->iFrame );
status = Ssw_SmlRunCounterExample( pMan, pGia->pCexSeq );
status = Saig_ManVerifyCex( pMan, pGia->pCexSeq );
if ( status == 0 )
printf( "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" );
}
@ -2825,7 +2824,7 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
{
printf( "Simulation of %d frames with %d words asserted output %d in frame %d. ",
nFrames, nWords, pCex->iPo, pCex->iFrame );
status = Ssw_SmlRunCounterExample( pMan, pCex );
status = Saig_ManVerifyCex( pMan, pCex );
if ( status == 0 )
printf( "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" );
}
@ -2847,7 +2846,7 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
{
printf( "Simulation of %d frames with %d words asserted output %d in frame %d. ",
nFrames, nWords, pCex->iPo, pCex->iFrame );
status = Ssw_SmlRunCounterExample( pMan, pCex );
status = Saig_ManVerifyCex( pMan, pCex );
if ( status == 0 )
printf( "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" );
}

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

@ -384,7 +384,7 @@ finish:
// verify counter-example
if ( pNtk->pSeqModel )
{
int status = Ssw_SmlRunCounterExample( pMan, pNtk->pSeqModel );
int status = Saig_ManVerifyCex( pMan, pNtk->pSeqModel );
if ( status == 0 )
printf( "Abc_NtkDarBmc(): Counter-example verification has FAILED.\n" );
}

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

@ -197,7 +197,7 @@ int Abc_NtkReadLogFile( char * pFileName, Abc_Cex_t ** ppCex, int * pnFrames )
printf( "Incorrect number of bits.\n" );
return -1;
}
pCex = Gia_ManAllocCounterExample( nRegs, (Vec_IntSize(vNums)-nRegs)/nFrames, nFrames );
pCex = Abc_CexAlloc( nRegs, (Vec_IntSize(vNums)-nRegs)/nFrames, nFrames );
pCex->iPo = iPo;
pCex->iFrame = nFrames - 1;
assert( Vec_IntSize(vNums) == pCex->nBits );

4
src/base/abci/abcVerify.c
View File

@ -24,6 +24,7 @@
#include "fraig.h"
#include "sim.h"
#include "aig.h"
#include "saig.h"
#include "gia.h"
#include "ssw.h"
@ -1029,7 +1030,6 @@ void Abc_NtkSimulteBuggyMiter( Abc_Ntk_t * pNtk )
int Abc_NtkIsTrueCex( Abc_Ntk_t * pNtk, Abc_Cex_t * pCex )
{
extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
// extern int Ssw_SmlRunCounterExample( Aig_Man_t * pAig, Abc_Cex_t * p );
Aig_Man_t * pMan;
int status, fStrashed = 0;
if ( !Abc_NtkIsStrash(pNtk) )
@ -1040,7 +1040,7 @@ int Abc_NtkIsTrueCex( Abc_Ntk_t * pNtk, Abc_Cex_t * pCex )
pMan = Abc_NtkToDar( pNtk, 0, 1 );
if ( pMan )
{
status = Ssw_SmlRunCounterExample( pMan, pCex );
status = Saig_ManVerifyCex( pMan, pCex );
Aig_ManStop( pMan );
}
if ( fStrashed )

10
src/base/cmd/cmdPlugin.c
View File

@ -484,20 +484,18 @@ int Cmd_CommandAbcPlugIn( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( 1, "Counter example has a wrong length.\n" );
else
{
extern int Gia_ManVerifyCounterExampleAllOuts( Gia_Man_t * pAig, Abc_Cex_t * p );
Abc_Print( 1, "Problem is satisfiable. Found counter-example in frame %d. ", nFrames-1 );
Abc_PrintTime( 1, "Time", clk );
ABC_FREE( pAbc->pCex );
pAbc->pCex = Gia_ManDeriveCexFromArray( pAbc->pGia, vCex, 0, nFrames-1 );
pAbc->pCex = Abc_CexCreate( Gia_ManRegNum(pAbc->pGia), Gia_ManPiNum(pAbc->pGia), Vec_IntArray(vCex), nFrames-1, 0, 0 );
// Gia_ManPrintCex( pAbc->pCex );
// Abc_CexPrint( pAbc->pCex );
// if ( !Gia_ManVerifyCounterExample( pAbc->pGia, pAbc->pCex, 0 ) )
// if ( !Gia_ManVerifyCex( pAbc->pGia, pAbc->pCex, 0 ) )
// Abc_Print( 1, "Generated counter-example is INVALID.\n" );
// remporary work-around to detect the output number - October 18, 2010
pAbc->pCex->iPo = Gia_ManVerifyCounterExampleAllOuts( pAbc->pGia, pAbc->pCex );
pAbc->pCex->iPo = Gia_ManFindFailedPoCex( pAbc->pGia, pAbc->pCex );
if ( pAbc->pCex->iPo == -1 )
{
Abc_Print( 1, "Generated counter-example is INVALID.\n" );

12
src/misc/util/abc_global.h
View File

@ -288,18 +288,6 @@ static inline void Abc_PrintMemoryP( int level, const char * pStr, int time, int
}
// sequential counter-example
typedef struct Abc_Cex_t_ Abc_Cex_t;
struct Abc_Cex_t_
{
int iPo; // the zero-based number of PO, for which verification failed
int iFrame; // the zero-based number of the time-frame, for which verificaiton failed
int nRegs; // the number of registers in the miter
int nPis; // the number of primary inputs in the miter
int nBits; // the number of words of bit data used
unsigned pData[0]; // the cex bit data (the number of bits: nRegs + (iFrame+1) * nPis)
};
ABC_NAMESPACE_HEADER_END
#endif

4
src/misc/util/module.make
View File

@ -1 +1,3 @@
SRC += src/misc/util/utilFile.c src/misc/util/utilSignal.c
SRC += src/misc/util/utilCex.c \
src/misc/util/utilFile.c \
src/misc/util/utilSignal.c

3
src/sat/pdr/pdrMan.c
View File

@ -19,7 +19,6 @@
***********************************************************************/
#include "pdrInt.h"
#include "ssw.h"
ABC_NAMESPACE_IMPL_START
@ -165,7 +164,7 @@ Abc_Cex_t * Pdr_ManDeriveCex( Pdr_Man_t * p )
for ( pObl = p->pQueue; pObl; pObl = pObl->pNext )
nFrames++;
// create the counter-example
pCex = Ssw_SmlAllocCounterExample( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), nFrames );
pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), nFrames );
pCex->iPo = (p->pPars->iOutput==-1)? 0 : p->pPars->iOutput;
pCex->iFrame = nFrames-1;
for ( pObl = p->pQueue, f = 0; pObl; pObl = pObl->pNext, f++ )