summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/aig/gia/giaDup.c6
-rw-r--r--src/base/abci/abc.c218
-rw-r--r--src/misc/util/utilCex.c23
-rw-r--r--src/sat/bmc/bmc.h1
-rw-r--r--src/sat/bmc/bmcCexCut.c67
5 files changed, 275 insertions, 40 deletions
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index b0c5ca21..eddbd320 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -1234,8 +1234,8 @@ Gia_Man_t * Gia_ManDupWithNewPo( Gia_Man_t * p1, Gia_Man_t * p2 )
assert( Gia_ManRegNum(p2) == 0 );
// there is only one PO in p2
assert( Gia_ManPoNum(p2) == 1 );
- // flop count of p1 is equal to input count of p2
- assert( Gia_ManRegNum(p1) == Gia_ManPiNum(p2) );
+ // input count of p2 is equal to flop count of p1
+ assert( Gia_ManPiNum(p2) == Gia_ManRegNum(p1) );
// start new AIG
pNew = Gia_ManStart( Gia_ManObjNum(p1)+Gia_ManObjNum(p2) );
@@ -1261,7 +1261,7 @@ Gia_Man_t * Gia_ManDupWithNewPo( Gia_Man_t * p1, Gia_Man_t * p2 )
Gia_ManForEachRi( p1, pObj, i )
Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
Gia_ManHashStop( pNew );
-// Gia_ManPrintStats( pGiaNew, 0 );
+ Gia_ManSetRegNum( pNew, Gia_ManRegNum(p1) );
pNew = Gia_ManCleanup( pTemp = pNew );
Gia_ManStop( pTemp );
return pNew;
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 7618c164..678589e2 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -296,6 +296,8 @@ static int Abc_CommandPdr ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandReconcile ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandCexSave ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandCexLoad ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandCexCut ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandCexMerge ( Abc_Frame_t * pAbc, int argc, char ** argv );
//static int Abc_CommandCexMin ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDualRail ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandBlockPo ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -364,8 +366,8 @@ static int Abc_CommandAbc9ReachN ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandAbc9ReachY ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Undo ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Iso ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandAbc9CexCut ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandAbc9CexMerge ( Abc_Frame_t * pAbc, int argc, char ** argv );
+//static int Abc_CommandAbc9CexCut ( Abc_Frame_t * pAbc, int argc, char ** argv );
+//static int Abc_CommandAbc9CexMerge ( Abc_Frame_t * pAbc, int argc, char ** argv );
//static int Abc_CommandAbc9CexMin ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9AbsDerive ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -755,6 +757,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Verification", "reconcile", Abc_CommandReconcile, 1 );
Cmd_CommandAdd( pAbc, "Verification", "cexsave", Abc_CommandCexSave, 0 );
Cmd_CommandAdd( pAbc, "Verification", "cexload", Abc_CommandCexLoad, 0 );
+ Cmd_CommandAdd( pAbc, "Verification", "cexcut", Abc_CommandCexCut, 0 );
+ Cmd_CommandAdd( pAbc, "Verification", "cexmerge", Abc_CommandCexMerge, 0 );
// Cmd_CommandAdd( pAbc, "Verification", "cexmin", Abc_CommandCexMin, 0 );
Cmd_CommandAdd( pAbc, "Verification", "dualrail", Abc_CommandDualRail, 1 );
Cmd_CommandAdd( pAbc, "Verification", "blockpo", Abc_CommandBlockPo, 1 );
@@ -820,8 +824,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&reachy", Abc_CommandAbc9ReachY, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&undo", Abc_CommandAbc9Undo, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&iso", Abc_CommandAbc9Iso, 0 );
- Cmd_CommandAdd( pAbc, "ABC9", "&cexcut", Abc_CommandAbc9CexCut, 0 );
- Cmd_CommandAdd( pAbc, "ABC9", "&cexmerge", Abc_CommandAbc9CexMerge, 0 );
+// Cmd_CommandAdd( pAbc, "ABC9", "&cexcut", Abc_CommandAbc9CexCut, 0 );
+// Cmd_CommandAdd( pAbc, "ABC9", "&cexmerge", Abc_CommandAbc9CexMerge, 0 );
// Cmd_CommandAdd( pAbc, "ABC9", "&cexmin", Abc_CommandAbc9CexMin, 0 );
Cmd_CommandAdd( pAbc, "Abstraction", "&abs_derive", Abc_CommandAbc9AbsDerive, 0 );
@@ -22516,7 +22520,7 @@ int Abc_CommandCexSave( Abc_Frame_t * pAbc, int argc, char ** argv )
}
if ( pAbc->pCex == NULL )
{
- Abc_Print( -1, "Empty network.\n" );
+ Abc_Print( -1, "Current CEX is not available..\n" );
return 1;
}
ABC_FREE( pAbc->pCex2 );
@@ -22555,9 +22559,9 @@ int Abc_CommandCexLoad( Abc_Frame_t * pAbc, int argc, char ** argv )
goto usage;
}
}
- if ( pAbc->pCex == NULL )
+ if ( pAbc->pCex2 == NULL )
{
- Abc_Print( -1, "Empty network.\n" );
+ Abc_Print( -1, "Saved CEX is not available.\n" );
return 1;
}
ABC_FREE( pAbc->pCex );
@@ -22583,6 +22587,200 @@ usage:
SeeAlso []
***********************************************************************/
+int Abc_CommandCexCut( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ int c;
+ int iFrStart = 0;
+ int iFrStop = ABC_INFINITY;
+ int fVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "FGvh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'F':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ iFrStart = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( iFrStart < 0 )
+ goto usage;
+ break;
+ case 'G':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-G\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ iFrStop = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( iFrStop < 0 )
+ goto usage;
+ break;
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ Abc_Print( -2, "Unknown switch.\n");
+ goto usage;
+ }
+ }
+
+ if ( pAbc->pCex == NULL )
+ {
+ Abc_Print( 1, "There is no current cex.\n");
+ return 0;
+ }
+ if ( pAbc->pNtkCur == NULL )
+ {
+ Abc_Print( 1, "There is no AIG in the &-space.\n");
+ return 0;
+ }
+ if ( !Abc_NtkIsStrash(pAbc->pNtkCur) )
+ {
+ Abc_Print( 1, "Current network is not an AIG.\n");
+ return 0;
+ }
+ if ( iFrStop == ABC_INFINITY )
+ iFrStop = pAbc->pCex->iFrame;
+
+ {
+ Abc_Ntk_t * pNtkNew;
+ Aig_Man_t * pAig = Abc_NtkToDar( pAbc->pNtkCur, 0, 1 );
+ Aig_Man_t * pAigNew = Bmc_AigTargetStates( pAig, pAbc->pCex, iFrStart, iFrStop, fVerbose );
+ Aig_ManStop( pAig );
+ if ( pAigNew == NULL )
+ {
+ Abc_Print( 1, "Command has failed.\n");
+ return 0;
+ }
+ pNtkNew = Abc_NtkFromAigPhase( pAigNew );
+ pNtkNew->pName = Extra_UtilStrsav( pAbc->pNtkCur->pName );
+ Aig_ManStop( pAigNew );
+ // update the network
+ Abc_FrameReplaceCurrentNetwork( pAbc, pNtkNew );
+ }
+ return 0;
+
+usage:
+ Abc_Print( -2, "usage: cexcut [-FG num] [-vh]\n" );
+ Abc_Print( -2, "\t creates logic for bad states using the current CEX\n" );
+ Abc_Print( -2, "\t-F num : 0-based number of the starting frame [default = %d]\n", iFrStart );
+ Abc_Print( -2, "\t-G num : 0-based number of the ending frame [default = %d]\n", iFrStop );
+ Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-h : print the command usage\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_CommandCexMerge( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ Abc_Cex_t * pCexNew;
+ int c;
+ int iFrStart = 0;
+ int iFrStop = ABC_INFINITY;
+ int fVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "FGvh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'F':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ iFrStart = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( iFrStart < 0 )
+ goto usage;
+ break;
+ case 'G':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-G\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ iFrStop = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( iFrStop < 0 )
+ goto usage;
+ break;
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ Abc_Print( -2, "Unknown switch.\n");
+ goto usage;
+ }
+ }
+
+ if ( pAbc->pCex == NULL )
+ {
+ Abc_Print( 1, "There is no current cex.\n");
+ return 0;
+ }
+ if ( pAbc->pCex2 == NULL )
+ {
+ Abc_Print( 1, "There is no saved cex.\n");
+ return 0;
+ }
+ if ( iFrStop - iFrStart < pAbc->pCex->iFrame )
+ {
+ Abc_Print( 1, "Current CEX does not allow to shorten the saved CEX.\n");
+ return 0;
+ }
+ pCexNew = Abc_CexMerge( pAbc->pCex2, pAbc->pCex, iFrStart, iFrStop );
+ if ( pCexNew == NULL )
+ {
+ Abc_Print( 1, "Merging CEXes has failed.\n");
+ return 0;
+ }
+ // replace the saved CEX
+ ABC_FREE( pAbc->pCex2 );
+ pAbc->pCex2 = pCexNew;
+ return 0;
+
+usage:
+ Abc_Print( -2, "usage: cexmerge [-FG num] [-vh]\n" );
+ Abc_Print( -2, "\t merges the current CEX into the saved one\n" );
+ Abc_Print( -2, "\t and sets the resulting CEX as the saved one\n" );
+ Abc_Print( -2, "\t-F num : 0-based number of the starting frame [default = %d]\n", iFrStart );
+ Abc_Print( -2, "\t-G num : 0-based number of the ending frame [default = %d]\n", iFrStop );
+ Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-h : print the command usage\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Abc_CommandCexMin( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pNtk;
@@ -28680,10 +28878,10 @@ int Abc_CommandAbc9CexCut( Abc_Frame_t * pAbc, int argc, char ** argv )
usage:
Abc_Print( -2, "usage: &cexcut [-FG num] [-vh]\n" );
- Abc_Print( -2, "\t extract logic representation of bad states\n" );
+ Abc_Print( -2, "\t creates logic for bad states using the current CEX\n" );
Abc_Print( -2, "\t-F num : 0-based number of the starting frame [default = %d]\n", iFrStart );
Abc_Print( -2, "\t-G num : 0-based number of the ending frame [default = %d]\n", iFrStop );
- Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
@@ -28754,7 +28952,7 @@ int Abc_CommandAbc9CexMerge( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( 1, "There is no saved cex.\n");
return 0;
}
- if ( iFrStop - iFrStart > pAbc->pCex->iFrame )
+ if ( iFrStop - iFrStart < pAbc->pCex->iFrame )
{
Abc_Print( 1, "Current CEX does not allow to shorten the saved CEX.\n");
return 0;
diff --git a/src/misc/util/utilCex.c b/src/misc/util/utilCex.c
index 16dbb076..edb246b9 100644
--- a/src/misc/util/utilCex.c
+++ b/src/misc/util/utilCex.c
@@ -195,14 +195,14 @@ Abc_Cex_t * Abc_CexMerge( Abc_Cex_t * pCex, Abc_Cex_t * pPart, int iFrBeg, int i
{ printf( "Starting frame is more than the last frame of CEX (%d).\n", pCex->iFrame ); return NULL; }
if ( iFrEnd > pCex->iFrame )
{ printf( "Stopping frame is more than the last frame of CEX (%d).\n", pCex->iFrame ); return NULL; }
- if ( iFrBeg >= iFrEnd )
+ if ( iFrBeg > iFrEnd )
{ printf( "Starting frame (%d) should be less than stopping frame (%d).\n", iFrBeg, iFrEnd ); return NULL; }
assert( iFrBeg >= 0 && iFrBeg <= pCex->iFrame );
assert( iFrEnd >= 0 && iFrEnd <= pCex->iFrame );
- assert( iFrBeg < iFrEnd );
+ assert( iFrBeg <= iFrEnd );
assert( pCex->nPis == pPart->nPis );
- assert( iFrEnd - iFrBeg > pPart->iFrame );
+ assert( iFrEnd - iFrBeg >= pPart->iFrame );
nFramesGain = (iFrEnd - iFrBeg) - pPart->iFrame;
pNew = Abc_CexAlloc( pCex->nRegs, pCex->nPis, pCex->iFrame + 1 - nFramesGain );
@@ -211,20 +211,21 @@ Abc_Cex_t * Abc_CexMerge( Abc_Cex_t * pCex, Abc_Cex_t * pPart, int iFrBeg, int i
for ( iBit = 0; iBit < pCex->nRegs; iBit++ )
if ( Abc_InfoHasBit(pCex->pData, iBit) )
- Abc_InfoSetBit( pNew->pData, iBit++ );
+ Abc_InfoSetBit( pNew->pData, iBit );
for ( f = 0; f < iFrBeg; f++ )
- for ( i = 0; i < pCex->nPis; i++ )
+ for ( i = 0; i < pCex->nPis; i++, iBit++ )
if ( Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i) )
- Abc_InfoSetBit( pNew->pData, iBit++ );
+ Abc_InfoSetBit( pNew->pData, iBit );
for ( f = 0; f < pPart->iFrame; f++ )
- for ( i = 0; i < pCex->nPis; i++ )
+ for ( i = 0; i < pCex->nPis; i++, iBit++ )
if ( Abc_InfoHasBit(pPart->pData, pPart->nRegs + pCex->nPis * f + i) )
- Abc_InfoSetBit( pNew->pData, iBit++ );
+ Abc_InfoSetBit( pNew->pData, iBit );
for ( f = iFrEnd; f <= pCex->iFrame; f++ )
- for ( i = 0; i < pCex->nPis; i++ )
- if ( Abc_InfoHasBit(pPart->pData, pPart->nRegs + pCex->nPis * f + i) )
- Abc_InfoSetBit( pNew->pData, iBit++ );
+ for ( i = 0; i < pCex->nPis; i++, iBit++ )
+ if ( Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i) )
+ Abc_InfoSetBit( pNew->pData, iBit );
assert( iBit == pNew->nBits );
+
return pNew;
}
diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h
index e1841bbc..5d789dcb 100644
--- a/src/sat/bmc/bmc.h
+++ b/src/sat/bmc/bmc.h
@@ -76,6 +76,7 @@ extern void Saig_ParBmcSetDefaultParams( Saig_ParBmc_t * p );
extern int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars );
/*=== bmcCexCut.c ==========================================================*/
extern Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fVerbose );
+extern Aig_Man_t * Bmc_AigTargetStates( Aig_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fVerbose );
/*=== bmcCexMin.c ==========================================================*/
extern Abc_Cex_t * Saig_ManCexMinPerform( Aig_Man_t * pAig, Abc_Cex_t * pCex );
diff --git a/src/sat/bmc/bmcCexCut.c b/src/sat/bmc/bmcCexCut.c
index 96d46fb3..bbb1bc73 100644
--- a/src/sat/bmc/bmcCexCut.c
+++ b/src/sat/bmc/bmcCexCut.c
@@ -6,7 +6,7 @@
PackageName [SAT-based bounded model checking.]
- Synopsis []
+ Synopsis [Derives characterization of bad states.]
Author [Alan Mishchenko]
@@ -19,6 +19,7 @@
***********************************************************************/
#include "bmc.h"
+#include "aig/gia/giaAig.h"
ABC_NAMESPACE_IMPL_START
@@ -47,7 +48,7 @@ Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, in
Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj, * pObjRo, * pObjRi;
Vec_Bit_t * vInitNew;
- int i, k, iBit = 0;
+ int i, k, iBit = 0, fCompl0, fCompl1;
if ( iFrBeg < 0 )
{ printf( "Starting frame is less than 0.\n" ); return NULL; }
@@ -57,7 +58,7 @@ Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, in
{ printf( "Starting frame is more than the last frame of CEX (%d).\n", pCex->iFrame ); return NULL; }
if ( iFrEnd > pCex->iFrame )
{ printf( "Stopping frame is more than the last frame of CEX (%d).\n", pCex->iFrame ); return NULL; }
- if ( iFrBeg >= iFrEnd )
+ if ( iFrBeg > iFrEnd )
{ printf( "Starting frame (%d) should be less than stopping frame (%d).\n", iFrBeg, iFrEnd ); return NULL; }
assert( iFrBeg >= 0 && iFrBeg <= pCex->iFrame );
assert( iFrEnd >= 0 && iFrEnd <= pCex->iFrame );
@@ -65,7 +66,7 @@ Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, in
// skip trough the first iFrEnd frames
Gia_ManCleanMark0(p);
- Gia_ManForEachRo( p, pObj, i )
+ Gia_ManForEachRo( p, pObj, k )
pObj->fMark0 = Abc_InfoHasBit(pCex->pData, iBit++);
vInitNew = Vec_BitStart( Gia_ManRegNum(p) );
for ( i = 0; i < iFrEnd; i++ )
@@ -90,35 +91,39 @@ Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, in
// create new AIG manager
pNew = Gia_ManStart( 10000 );
+ pNew->pName = Abc_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 1;
Gia_ManForEachPi( p, pObj, k )
pObj->Value = 1;
- Gia_ManForEachRo( p, pObjRo, i )
- pObj->Value = Abc_LitNotCond( Gia_ManAppendCi(pNew), !pObjRo->fMark0 );
- Gia_ManHashStart( p );
+ Gia_ManForEachRo( p, pObjRo, k )
+ pObjRo->Value = Abc_LitNotCond( Gia_ManAppendCi(pNew), !pObjRo->fMark0 );
+ Gia_ManHashStart( pNew );
for ( i = iFrEnd; i <= pCex->iFrame; i++ )
{
Gia_ManForEachPi( p, pObj, k )
pObj->fMark0 = Abc_InfoHasBit(pCex->pData, iBit++);
Gia_ManForEachAnd( p, pObj, k )
{
- pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) &
- (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
+ fCompl0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
+ fCompl1 = Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj);
+ pObj->fMark0 = fCompl0 & fCompl1;
if ( pObj->fMark0 )
- pObj->Value = Gia_ManHashAnd( p, Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value );
- else if ( !Gia_ObjFanin0(pObj)->fMark0 && !Gia_ObjFanin1(pObj)->fMark0 )
- pObj->Value = Gia_ManHashOr( p, Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value );
- else if ( !Gia_ObjFanin0(pObj)->fMark0 )
+ pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value );
+ else if ( !fCompl0 && !fCompl1 )
+ pObj->Value = Gia_ManHashOr( pNew, Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value );
+ else if ( !fCompl0 )
pObj->Value = Gia_ObjFanin0(pObj)->Value;
- else if ( !Gia_ObjFanin1(pObj)->fMark0 )
+ else if ( !fCompl1 )
pObj->Value = Gia_ObjFanin1(pObj)->Value;
else assert( 0 );
+ assert( pObj->Value > 0 );
}
Gia_ManForEachCo( p, pObj, k )
{
pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
pObj->Value = Gia_ObjFanin0(pObj)->Value;
- }
+ assert( pObj->Value > 0 );
+ }
if ( i == pCex->iFrame )
break;
Gia_ManForEachRiRo( p, pObjRi, pObjRo, k )
@@ -127,7 +132,7 @@ Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, in
pObjRo->Value = pObjRi->Value;
}
}
- Gia_ManHashStop( p );
+ Gia_ManHashStop( pNew );
assert( iBit == pCex->nBits );
// create PO
@@ -143,10 +148,40 @@ Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, in
// create new initial state
pNew = Gia_ManDupFlip( pTemp = pNew, Vec_BitArray(vInitNew) );
Gia_ManStop( pTemp );
+
Vec_BitFree( vInitNew );
return pNew;
}
+/**Function*************************************************************
+
+ Synopsis [Generate AIG for target bad states.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Bmc_AigTargetStates( Aig_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fVerbose )
+{
+ Aig_Man_t * pAig;
+ Gia_Man_t * pGia, * pRes;
+ pGia = Gia_ManFromAigSimple( p );
+ if ( !Gia_ManVerifyCex( pGia, pCex, 0 ) )
+ {
+ Abc_Print( 1, "Current CEX does not fail AIG \"%s\".\n", p->pName );
+ Gia_ManStop( pGia );
+ return NULL;
+ }
+ pRes = Bmc_GiaTargetStates( pGia, pCex, iFrBeg, iFrEnd, fVerbose );
+ pAig = Gia_ManToAigSimple( pRes );
+ Gia_ManStop( pGia );
+ Gia_ManStop( pRes );
+ return pAig;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
generated by cgit v1.2.3 (git 2.25.1) at 2025-01-27 08:35:44 +0000