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

Better CEX minimization and renaming of write_counter into write_cex.

This commit is contained in:
Alan Mishchenko 2014-04-04 13:14:16 -07:00
parent 11bab8caf9
commit f6ae0e41f3
8 changed files with 366 additions and 14 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
abclib.dsp
View File

@ -1423,6 +1423,10 @@ SOURCE=.\src\sat\bmc\bmcBmci.c
# End Source File
# Begin Source File
SOURCE=.\src\sat\bmc\bmcCexCare.c
# End Source File
# Begin Source File
SOURCE=.\src\sat\bmc\bmcCexCut.c
# End Source File
# Begin Source File

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

@ -22,6 +22,7 @@
#include "base/main/mainInt.h"
#include "aig/saig/saig.h"
#include "proof/abs/abs.h"
#include "sat/bmc/bmc.h"
ABC_NAMESPACE_IMPL_START
@ -60,7 +61,7 @@ static int IoCommandWriteBook ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteCellNet( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteCnf ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteCnf2 ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteCex ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteDot ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteEqn ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteGml ( Abc_Frame_t * pAbc, int argc, char **argv );
@ -124,7 +125,7 @@ void Io_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "I/O", "write_bench", IoCommandWriteBench, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write_book", IoCommandWriteBook, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write_cellnet", IoCommandWriteCellNet, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write_counter", IoCommandWriteCounter, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write_cex", IoCommandWriteCex, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write_cnf", IoCommandWriteCnf, 0 );
Cmd_CommandAdd( pAbc, "I/O", "&write_cnf", IoCommandWriteCnf2, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write_dot", IoCommandWriteDot, 0 );
@ -2171,18 +2172,20 @@ ABC_NAMESPACE_IMPL_START
SeeAlso []
***********************************************************************/
int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv )
int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv )
{
Abc_Ntk_t * pNtk;
char * pFileName;
int c, fNames = 0;
int fMinimize = 0;
int fUseOldMin = 0;
int fCheckCex = 0;
int forceSeq = 0;
int fPrintFull = 0;
int fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "snmfvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "snmocfvh" ) ) != EOF )
{
switch ( c )
{
@ -2195,6 +2198,12 @@ int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv )
case 'm':
fMinimize ^= 1;
break;
case 'o':
fUseOldMin ^= 1;
break;
case 'c':
fCheckCex ^= 1;
break;
case 'f':
fPrintFull ^= 1;
break;
@ -2236,7 +2245,7 @@ int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv )
Abc_NtkForEachLatch( pNtk, pObj, i )
if ( !Abc_LatchIsInit0(pObj) )
{
fprintf( stdout, "IoCommandWriteCounter(): The init-state should be all-0 for counter-example to work.\n" );
fprintf( stdout, "IoCommandWriteCex(): The init-state should be all-0 for counter-example to work.\n" );
fprintf( stdout, "Run commands \"undc\" and \"zero\" and then rerun the equivalence check.\n" );
return 1;
}
@ -2244,7 +2253,7 @@ int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv )
pFile = fopen( pFileName, "w" );
if ( pFile == NULL )
{
fprintf( stdout, "IoCommandWriteCounter(): Cannot open the output file \"%s\".\n", pFileName );
fprintf( stdout, "IoCommandWriteCex(): Cannot open the output file \"%s\".\n", pFileName );
return 1;
}
if ( fPrintFull )
@ -2267,9 +2276,14 @@ int IoCommandWriteCounter( 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 );
pCare = Saig_ManCbaFindCexCareBits( pAig, pCex, 0, fVerbose );
if ( pCare == NULL )
printf( "Counter-example minimization has failed.\n" );
if ( fUseOldMin )
{
pCare = Saig_ManCbaFindCexCareBits( pAig, pCex, 0, fVerbose );
if ( fCheckCex )
Bmc_CexCareVerify( pAig, pCex, pCare, fVerbose );
}
else
pCare = Bmc_CexCareMinimize( pAig, pCex, fCheckCex, fVerbose );
Aig_ManStop( pAig );
}
// output flop values (unaffected by the minimization)
@ -2299,7 +2313,7 @@ int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv )
int i;
if ( pFile == NULL )
{
fprintf( stdout, "IoCommandWriteCounter(): Cannot open the output file \"%s\".\n", pFileName );
fprintf( stdout, "IoCommandWriteCex(): Cannot open the output file \"%s\".\n", pFileName );
return 1;
}
if ( fNames )
@ -2321,12 +2335,14 @@ int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv )
return 0;
usage:
fprintf( pAbc->Err, "usage: write_counter [-snmfvh] <file>\n" );
fprintf( pAbc->Err, "usage: write_cex [-snmocfvh] <file>\n" );
fprintf( pAbc->Err, "\t saves counter-example derived by \"sat\", \"iprove\", or \"dprove\"\n" );
fprintf( pAbc->Err, "\t the file contains values for each PI in the natural order\n" );
fprintf( pAbc->Err, "\t-s : always report a sequential ctrex (cycle 0 for comb) [default = %s]\n", forceSeq? "yes": "no" );
fprintf( pAbc->Err, "\t-n : write input names into the file [default = %s]\n", fNames? "yes": "no" );
fprintf( pAbc->Err, "\t-m : minimize counter-example by dropping don't-care values [default = %s]\n", fMinimize? "yes": "no" );
fprintf( pAbc->Err, "\t-o : use old counter-example minimization algorithm [default = %s]\n", fUseOldMin? "yes": "no" );
fprintf( pAbc->Err, "\t-c : check generated counter-example using ternary simulation [default = %s]\n", fCheckCex? "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-h : print the help massage\n" );
@ -2334,7 +2350,6 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []

27
src/misc/util/utilCex.c
View File

@ -488,6 +488,33 @@ Abc_Cex_t * Abc_CexPermuteTwo( Abc_Cex_t * p, Vec_Int_t * vPermOld, Vec_Int_t *
return pCex;
}
/**Function*************************************************************
Synopsis [Count the number of 1s in the CEX.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Abc_CexOnes32( unsigned i )
{
i = i - ((i >> 1) & 0x55555555);
i = (i & 0x33333333) + ((i >> 2) & 0x33333333);
i = ((i + (i >> 4)) & 0x0F0F0F0F);
return (i*(0x01010101))>>24;
}
int Abc_CexCountOnes( Abc_Cex_t * p )
{
int nWords = Abc_BitWordNum( p->nBits );
int i, Count = 0;
for ( i = 0; i < nWords; i++ )
Count += Abc_CexOnes32( p->pData[i] );
return Count;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

1
src/misc/util/utilCex.h
View File

@ -72,6 +72,7 @@ extern Abc_Cex_t * Abc_CexTransformPhase( Abc_Cex_t * p, int nPisOld, int nPos
extern Abc_Cex_t * Abc_CexTransformTempor( Abc_Cex_t * p, int nPisOld, int nPosOld, int nRegsOld );
extern Abc_Cex_t * Abc_CexPermute( Abc_Cex_t * p, Vec_Int_t * vMapOld2New );
extern Abc_Cex_t * Abc_CexPermuteTwo( Abc_Cex_t * p, Vec_Int_t * vPermOld, Vec_Int_t * vPermNew );
extern int Abc_CexCountOnes( Abc_Cex_t * p );
ABC_NAMESPACE_HEADER_END

6
src/sat/bmc/bmc.h
View File

@ -126,11 +126,17 @@ extern void Saig_ParBmcSetDefaultParams( Saig_ParBmc_t * p );
extern int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars );
/*=== bmcBmcAnd.c ==========================================================*/
extern int Gia_ManBmcPerform( Gia_Man_t * p, Bmc_AndPar_t * pPars );
/*=== bmcCexCare.c ==========================================================*/
extern Abc_Cex_t * Bmc_CexCareMinimize( Aig_Man_t * p, Abc_Cex_t * pCex, int fCheck, int fVerbose );
extern void Bmc_CexCareVerify( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, int fVerbose );
/*=== bmcCexCut.c ==========================================================*/
extern Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fGenAll, int fAllFrames, int fVerbose );
extern Aig_Man_t * Bmc_AigTargetStates( Aig_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fGenAll, int fAllFrames, int fVerbose );
/*=== bmcCexMin.c ==========================================================*/
extern Abc_Cex_t * Saig_ManCexMinPerform( Aig_Man_t * pAig, Abc_Cex_t * pCex );
/*=== bmcCexTool.c ==========================================================*/
extern void Bmc_CexPrint( Abc_Cex_t * pCex, int nInputs, int fVerbose );
extern int Bmc_CexVerify( 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 fDump, int fVerbose );

298
src/sat/bmc/bmcCexCare.c Normal file
View File

@ -0,0 +1,298 @@
/**CFile****************************************************************
FileName [bmcCexCare.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [SAT-based bounded model checking.]
Synopsis [Computing care set of the counter-example.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: bmcCexCare.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "bmc.h"
#include "aig/gia/giaAig.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Backward propagation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Bmc_CexCarePropagateFwdOne( Gia_Man_t * p, Abc_Cex_t * pCex, int f, int fGrow )
{
Gia_Obj_t * pObj;
int Prio, Prio0, Prio1;
int i, Phase0, Phase1;
if ( (fGrow & 2) )
{
Gia_ManForEachPi( p, pObj, i )
pObj->Value = Abc_Var2Lit( f * pCex->nPis + (pCex->nPis-1-i) + 1, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i) );
}
else
{
Gia_ManForEachPi( p, pObj, i )
pObj->Value = Abc_Var2Lit( f * pCex->nPis + i + 1, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i) );
}
Gia_ManForEachAnd( p, pObj, i )
{
Prio0 = Abc_Lit2Var(Gia_ObjFanin0(pObj)->Value);
Prio1 = Abc_Lit2Var(Gia_ObjFanin1(pObj)->Value);
Phase0 = Abc_LitIsCompl(Gia_ObjFanin0(pObj)->Value) ^ Gia_ObjFaninC0(pObj);
Phase1 = Abc_LitIsCompl(Gia_ObjFanin1(pObj)->Value) ^ Gia_ObjFaninC1(pObj);
if ( Phase0 && Phase1 )
Prio = (fGrow & 1) ? Abc_MinInt(Prio0, Prio1) : Abc_MaxInt(Prio0, Prio1);
else if ( Phase0 && !Phase1 )
Prio = Prio1;
else if ( !Phase0 && Phase1 )
Prio = Prio0;
else // if ( !Phase0 && !Phase1 )
Prio = (fGrow & 1) ? Abc_MaxInt(Prio0, Prio1) : Abc_MinInt(Prio0, Prio1);
pObj->Value = Abc_Var2Lit( Prio, Phase0 & Phase1 );
}
Gia_ManForEachCo( p, pObj, i )
pObj->Value = Abc_LitNotCond( Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj) );
}
void Bmc_CexCarePropagateFwd( Gia_Man_t * p, Abc_Cex_t * pCex, int fGrow, Vec_Int_t * vPrios )
{
Gia_Obj_t * pObj, * pObjRo, * pObjRi;
int f, i;
Gia_ManConst0( p )->Value = 0;
Gia_ManForEachRi( p, pObj, i )
pObj->Value = 0;
Vec_IntClear( vPrios );
for ( f = 0; f <= pCex->iFrame; f++ )
{
Gia_ManForEachRiRo( p, pObjRi, pObjRo, i )
Vec_IntPush( vPrios, (pObjRo->Value = pObjRi->Value) );
Bmc_CexCarePropagateFwdOne( p, pCex, f, fGrow );
}
}
/**Function*************************************************************
Synopsis [Forward propagation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Bmc_CexCarePropagateBwdOne( Gia_Man_t * p, Abc_Cex_t * pCex, int f, Abc_Cex_t * pCexMin )
{
Gia_Obj_t * pObj;
int i, Phase0, Phase1;
Gia_ManForEachCand( p, pObj, i )
pObj->fPhase = 0;
Gia_ManForEachCo( p, pObj, i )
if ( pObj->fPhase )
Gia_ObjFanin0(pObj)->fPhase = 1;
Gia_ManForEachAndReverse( p, pObj, i )
{
if ( !pObj->fPhase )
continue;
Phase0 = Abc_LitIsCompl(Gia_ObjFanin0(pObj)->Value) ^ Gia_ObjFaninC0(pObj);
Phase1 = Abc_LitIsCompl(Gia_ObjFanin1(pObj)->Value) ^ Gia_ObjFaninC1(pObj);
if ( Phase0 && Phase1 )
{
Gia_ObjFanin0(pObj)->fPhase = 1;
Gia_ObjFanin1(pObj)->fPhase = 1;
}
else if ( Phase0 && !Phase1 )
Gia_ObjFanin1(pObj)->fPhase = 1;
else if ( !Phase0 && Phase1 )
Gia_ObjFanin0(pObj)->fPhase = 1;
else // if ( !Phase0 && !Phase1 )
{
if ( Abc_Lit2Var(Gia_ObjFanin0(pObj)->Value) <= Abc_Lit2Var(Gia_ObjFanin1(pObj)->Value) )
Gia_ObjFanin0(pObj)->fPhase = 1;
else
Gia_ObjFanin1(pObj)->fPhase = 1;
}
}
Gia_ManForEachPi( p, pObj, i )
if ( pObj->fPhase )
Abc_InfoSetBit( pCexMin->pData, pCexMin->nRegs + pCexMin->nPis * f + i );
}
Abc_Cex_t * Bmc_CexCarePropagateBwd( Gia_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vPrios, int fGrow )
{
Abc_Cex_t * pCexMin;
Gia_Obj_t * pObj, * pObjRo, * pObjRi;
int f, i;
pCexMin = Abc_CexAlloc( pCex->nRegs, pCex->nPis, pCex->iFrame + 1 );
pCexMin->iPo = pCex->iPo;
pCexMin->iFrame = pCex->iFrame;
Gia_ManForEachCo( p, pObj, i )
pObj->fPhase = 0;
for ( f = pCex->iFrame; f >= 0; f-- )
{
Gia_ManPo(p, pCex->iPo)->fPhase = (int)(f == pCex->iFrame);
Gia_ManForEachRo( p, pObj, i )
pObj->Value = Vec_IntEntry( vPrios, f * pCex->nRegs + i );
Bmc_CexCarePropagateFwdOne( p, pCex, f, fGrow );
Bmc_CexCarePropagateBwdOne( p, pCex, f, pCexMin );
Gia_ManForEachRiRo( p, pObjRi, pObjRo, i )
pObjRi->fPhase = pObjRo->fPhase;
}
return pCexMin;
}
/**Function*************************************************************
Synopsis [Computes the care set of the counter-example.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Cex_t * Bmc_CexCareMinimizeAig( Gia_Man_t * p, Abc_Cex_t * pCex, int fCheck, int fVerbose )
{
int nTryCexes = 4; // belongs to range [1;4]
Abc_Cex_t * pCexBest, * pCexMin[4] = {NULL};
int k, nOnesBest, nOnesCur;
Vec_Int_t * vPrios;
if ( pCex->nPis != Gia_ManPiNum(p) )
{
printf( "Given CEX does to have same number of inputs as the AIG.\n" );
return NULL;
}
if ( pCex->nRegs != Gia_ManRegNum(p) )
{
printf( "Given CEX does to have same number of flops as the AIG.\n" );
return NULL;
}
if ( !(pCex->iPo >= 0 && pCex->iPo < Gia_ManPoNum(p)) )
{
printf( "Given CEX has PO whose index is out of range for the AIG.\n" );
return NULL;
}
assert( pCex->nPis == Gia_ManPiNum(p) );
assert( pCex->nRegs == Gia_ManRegNum(p) );
assert( pCex->iPo >= 0 && pCex->iPo < Gia_ManPoNum(p) );
if ( fVerbose )
{
printf( "Original : " );
Bmc_CexPrint( pCex, Gia_ManPiNum(p), 0 );
}
vPrios = Vec_IntAlloc( pCex->nRegs * (pCex->iFrame + 1) );
for ( k = 0; k < nTryCexes; k++ )
{
Bmc_CexCarePropagateFwd(p, pCex, k, vPrios );
assert( Vec_IntSize(vPrios) == pCex->nRegs * (pCex->iFrame + 1) );
if ( !Abc_LitIsCompl(Gia_ManPo(p, pCex->iPo)->Value) )
{
printf( "Counter-example is invalid.\n" );
Vec_IntFree( vPrios );
return NULL;
}
pCexMin[k] = Bmc_CexCarePropagateBwd( p, pCex, vPrios, k );
if ( fVerbose )
{
if ( (k & 1) )
printf( "Decrease : " );
else
printf( "Increase : " );
Bmc_CexPrint( pCexMin[k], Gia_ManPiNum(p), 0 );
}
}
Vec_IntFree( vPrios );
// select the best one
pCexBest = pCexMin[0];
nOnesBest = Abc_CexCountOnes(pCexMin[0]);
for ( k = 1; k < nTryCexes; k++ )
{
nOnesCur = Abc_CexCountOnes(pCexMin[k]);
if ( nOnesBest > nOnesCur )
{
nOnesBest = nOnesCur;
pCexBest = pCexMin[k];
}
}
for ( k = 0; k < nTryCexes; k++ )
if ( pCexBest != pCexMin[k] )
Abc_CexFreeP( &pCexMin[k] );
// verify and return
if ( fVerbose )
{
printf( "Final : " );
Bmc_CexPrint( pCexBest, Gia_ManPiNum(p), 0 );
}
if ( !Bmc_CexVerify( p, pCex, pCexBest ) )
printf( "Counter-example verification has failed.\n" );
else if ( fCheck )
printf( "Counter-example verification succeeded.\n" );
return pCexBest;
}
Abc_Cex_t * Bmc_CexCareMinimize( Aig_Man_t * p, Abc_Cex_t * pCex, int fCheck, int fVerbose )
{
Gia_Man_t * pGia = Gia_ManFromAigSimple( p );
Abc_Cex_t * pCexMin = Bmc_CexCareMinimizeAig( pGia, pCex, fCheck, fVerbose );
Gia_ManStop( pGia );
return pCexMin;
}
/**Function*************************************************************
Synopsis [Verifies the care set of the counter-example.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Bmc_CexCareVerify( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, int fVerbose )
{
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 );
}
if ( !Bmc_CexVerify( pGia, pCex, pCexMin ) )
printf( "Counter-example verification has failed.\n" );
else
printf( "Counter-example verification succeeded.\n" );
Gia_ManStop( pGia );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END

4
src/sat/bmc/bmcCexTools.c
View File

@ -348,7 +348,7 @@ int Bmc_CexVerify( 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 );
// assert( pCexCare->nRegs == 0 );
Gia_ObjTerSimSet0( Gia_ManConst0(p) );
Gia_ManForEachRi( p, pObj, k )
Gia_ObjTerSimSet0( pObj );
@ -356,7 +356,7 @@ int Bmc_CexVerify( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare )
{
Gia_ManForEachPi( p, pObj, k )
{
if ( !Abc_InfoHasBit( pCexCare->pData, i * pCexCare->nPis + 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 );

1
src/sat/bmc/module.make
View File

@ -3,6 +3,7 @@ SRC += src/sat/bmc/bmcBmc.c \
src/sat/bmc/bmcBmc3.c \
src/sat/bmc/bmcBmcAnd.c \
src/sat/bmc/bmcBmci.c \
src/sat/bmc/bmcCexCare.c \
src/sat/bmc/bmcCexCut.c \
src/sat/bmc/bmcCexDepth.c \
src/sat/bmc/bmcCexMin1.c \