summaryrefslogtreecommitdiffstats
path: root/src/aig/fra
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/fra')
-rw-r--r--src/aig/fra/fra.h22
-rw-r--r--src/aig/fra/fraBmc.c78
-rw-r--r--src/aig/fra/fraCore.c45
-rw-r--r--src/aig/fra/fraLcr.c6
-rw-r--r--src/aig/fra/fraSec.c4
-rw-r--r--src/aig/fra/fraSim.c255
6 files changed, 383 insertions, 27 deletions
diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index 0de803ed..8cd677d1 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -53,6 +53,7 @@ typedef struct Fra_Par_t_ Fra_Par_t;
typedef struct Fra_Man_t_ Fra_Man_t;
typedef struct Fra_Cla_t_ Fra_Cla_t;
typedef struct Fra_Sml_t_ Fra_Sml_t;
+typedef struct Fra_Cex_t_ Fra_Cex_t;
typedef struct Fra_Bmc_t_ Fra_Bmc_t;
// FRAIG parameters
@@ -118,6 +119,17 @@ struct Fra_Sml_t_
unsigned pData[0]; // simulation data for the nodes
};
+// simulation manager
+struct Fra_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)
+};
+
// FRAIG manager
struct Fra_Man_t_
{
@@ -227,6 +239,7 @@ extern int Fra_BmcNodeIsConst( Aig_Obj_t * pObj );
extern int Fra_BmcNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
extern void Fra_BmcStop( Fra_Bmc_t * p );
extern void Fra_BmcPerform( Fra_Man_t * p, int nPref, int nDepth );
+extern void Fra_BmcPerformSimple( Aig_Man_t * pAig, int nFrames, int nBTLimit, int fRewrite, int fVerbose );
/*=== fraClass.c ========================================================*/
extern Fra_Cla_t * Fra_ClassesStart( Aig_Man_t * pAig );
extern void Fra_ClassesStop( Fra_Cla_t * p );
@@ -247,9 +260,10 @@ extern void Fra_CnfNodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pO
/*=== fraCore.c ========================================================*/
extern void Fra_FraigSweep( Fra_Man_t * pManAig );
extern int Fra_FraigMiterStatus( Aig_Man_t * p );
+extern int Fra_FraigMiterAssertedOutput( Aig_Man_t * p );
extern Aig_Man_t * Fra_FraigPerform( Aig_Man_t * pManAig, Fra_Par_t * pPars );
extern Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax );
-extern Aig_Man_t * Fra_FraigEquivence( Aig_Man_t * pManAig, int nConfMax );
+extern Aig_Man_t * Fra_FraigEquivence( Aig_Man_t * pManAig, int nConfMax, int fProve );
/*=== fraImp.c ========================================================*/
extern Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, int fLatchCorr );
extern void Fra_ImpAddToSolver( Fra_Man_t * p, Vec_Int_t * vImps, int * pSatVarNums );
@@ -291,7 +305,11 @@ extern Fra_Sml_t * Fra_SmlStart( Aig_Man_t * pAig, int nPref, int nFrame
extern void Fra_SmlStop( Fra_Sml_t * p );
extern Fra_Sml_t * Fra_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nWords );
extern Fra_Sml_t * Fra_SmlSimulateComb( Aig_Man_t * pAig, int nWords );
-
+extern Fra_Cex_t * Fra_SmlGetCounterExample( Fra_Sml_t * p );
+extern Fra_Cex_t * Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, int * pModel );
+extern void Fra_SmlFreeCounterExample( Fra_Cex_t * p );
+extern int Fra_SmlRunCounterExample( Aig_Man_t * pAig, Fra_Cex_t * p );
+extern Fra_Cex_t * Fra_SmlTrivCounterExample( Aig_Man_t * pAig, int iFrameOut );
#ifdef __cplusplus
}
diff --git a/src/aig/fra/fraBmc.c b/src/aig/fra/fraBmc.c
index eebafaf6..cf026fac 100644
--- a/src/aig/fra/fraBmc.c
+++ b/src/aig/fra/fraBmc.c
@@ -213,7 +213,8 @@ Fra_Bmc_t * Fra_BmcStart( Aig_Man_t * pAig, int nPref, int nDepth )
void Fra_BmcStop( Fra_Bmc_t * p )
{
Aig_ManStop( p->pAigFrames );
- Aig_ManStop( p->pAigFraig );
+ if ( p->pAigFraig )
+ Aig_ManStop( p->pAigFraig );
free( p->pObjToFrames );
free( p->pObjToFraig );
free( p );
@@ -230,7 +231,7 @@ void Fra_BmcStop( Fra_Bmc_t * p )
SeeAlso []
***********************************************************************/
-Aig_Man_t * Fra_BmcFrames( Fra_Bmc_t * p )
+Aig_Man_t * Fra_BmcFrames( Fra_Bmc_t * p, int fKeepPos )
{
Aig_Man_t * pAigFrames;
Aig_Obj_t * pObj, * pObjNew;
@@ -274,11 +275,20 @@ Aig_Man_t * Fra_BmcFrames( Fra_Bmc_t * p )
assert( k == Aig_ManRegNum(p->pAig) );
}
free( pLatches );
- // add POs to all the dangling nodes
- Aig_ManForEachObj( pAigFrames, pObjNew, i )
- if ( Aig_ObjIsNode(pObjNew) && pObjNew->nRefs == 0 )
- Aig_ObjCreatePo( pAigFrames, pObjNew );
-
+ if ( fKeepPos )
+ {
+ for ( f = 0; f < p->nFramesAll; f++ )
+ Aig_ManForEachPoSeq( p->pAig, pObj, i )
+ Aig_ObjCreatePo( pAigFrames, Bmc_ObjChild0Frames(pObj,f) );
+ Aig_ManCleanup( pAigFrames );
+ }
+ else
+ {
+ // add POs to all the dangling nodes
+ Aig_ManForEachObj( pAigFrames, pObjNew, i )
+ if ( Aig_ObjIsNode(pObjNew) && pObjNew->nRefs == 0 )
+ Aig_ObjCreatePo( pAigFrames, pObjNew );
+ }
// return the new manager
return pAigFrames;
}
@@ -301,7 +311,7 @@ void Fra_BmcPerform( Fra_Man_t * p, int nPref, int nDepth )
assert( p->pBmc == NULL );
// derive and fraig the frames
p->pBmc = Fra_BmcStart( p->pManAig, nPref, nDepth );
- p->pBmc->pAigFrames = Fra_BmcFrames( p->pBmc );
+ p->pBmc->pAigFrames = Fra_BmcFrames( p->pBmc, 0 );
// if implications are present, configure the AIG manager to check them
if ( p->pCla->vImps )
{
@@ -310,7 +320,7 @@ void Fra_BmcPerform( Fra_Man_t * p, int nPref, int nDepth )
p->pBmc->vImps = p->pCla->vImps;
nImpsOld = Vec_IntSize(p->pCla->vImps);
}
- p->pBmc->pAigFraig = Fra_FraigEquivence( p->pBmc->pAigFrames, 1000000 );
+ p->pBmc->pAigFraig = Fra_FraigEquivence( p->pBmc->pAigFrames, 1000000, 0 );
p->pBmc->pObjToFraig = p->pBmc->pAigFrames->pObjCopies;
p->pBmc->pAigFrames->pObjCopies = NULL;
// annotate frames nodes with pointers to the manager
@@ -354,6 +364,56 @@ void Fra_BmcPerform( Fra_Man_t * p, int nPref, int nDepth )
p->pBmc = NULL;
}
+/**Function*************************************************************
+
+ Synopsis [Performs BMC for the given AIG.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Fra_BmcPerformSimple( Aig_Man_t * pAig, int nFrames, int nBTLimit, int fRewrite, int fVerbose )
+{
+ extern Fra_Man_t * Fra_LcrAigPrepare( Aig_Man_t * pAig );
+ Fra_Man_t * pTemp;
+ Fra_Bmc_t * pBmc;
+ Aig_Man_t * pAigTemp;
+ int iOutput;
+ // derive and fraig the frames
+ pBmc = Fra_BmcStart( pAig, 0, nFrames );
+ pTemp = Fra_LcrAigPrepare( pAig );
+ pTemp->pBmc = pBmc;
+ pBmc->pAigFrames = Fra_BmcFrames( pBmc, 1 );
+ if ( fRewrite )
+ {
+ pBmc->pAigFrames = Dar_ManRwsat( pAigTemp = pBmc->pAigFrames, 1, 0 );
+ Aig_ManStop( pAigTemp );
+ }
+ iOutput = Fra_FraigMiterAssertedOutput( pBmc->pAigFrames );
+ if ( iOutput >= 0 )
+ pAig->pSeqModel = Fra_SmlTrivCounterExample( pAig, iOutput );
+ else
+ {
+ pBmc->pAigFraig = Fra_FraigEquivence( pBmc->pAigFrames, nBTLimit, 1 );
+ iOutput = Fra_FraigMiterAssertedOutput( pBmc->pAigFraig );
+ if ( pBmc->pAigFraig->pData )
+ {
+ pAig->pSeqModel = Fra_SmlCopyCounterExample( pAig, pBmc->pAigFrames, pBmc->pAigFraig->pData );
+ FREE( pBmc->pAigFraig->pData );
+ }
+ else if ( iOutput >= 0 )
+ pAig->pSeqModel = Fra_SmlTrivCounterExample( pAig, iOutput );
+ }
+ if ( fVerbose )
+ printf( "nFrames = %3d. Aig = %6d. Init frames = %6d. Fraiged init frames = %6d.\n",
+ nFrames, Aig_ManNodeNum(pAig), Aig_ManNodeNum(pBmc->pAigFrames), pBmc->pAigFraig? Aig_ManNodeNum(pBmc->pAigFraig) : -1 );
+ Fra_BmcStop( pBmc );
+ free( pTemp );
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
diff --git a/src/aig/fra/fraCore.c b/src/aig/fra/fraCore.c
index ad73501f..7400b3f9 100644
--- a/src/aig/fra/fraCore.c
+++ b/src/aig/fra/fraCore.c
@@ -58,27 +58,27 @@
***********************************************************************/
int Fra_FraigMiterStatus( Aig_Man_t * p )
{
- Aig_Obj_t * pObj, * pObjNew;
+ Aig_Obj_t * pObj, * pChild;
int i, CountConst0 = 0, CountNonConst0 = 0, CountUndecided = 0;
if ( p->pData )
return 0;
Aig_ManForEachPoSeq( p, pObj, i )
{
- pObjNew = Aig_ObjChild0(pObj);
+ pChild = Aig_ObjChild0(pObj);
// check if the output is constant 0
- if ( pObjNew == Aig_ManConst0(p) )
+ if ( pChild == Aig_ManConst0(p) )
{
CountConst0++;
continue;
}
// check if the output is constant 1
- if ( pObjNew == Aig_ManConst1(p) )
+ if ( pChild == Aig_ManConst1(p) )
{
CountNonConst0++;
continue;
}
// check if the output can be not constant 0
- if ( Aig_Regular(pObjNew)->fPhase != (unsigned)Aig_IsComplement(pObjNew) )
+ if ( Aig_Regular(pChild)->fPhase != (unsigned)Aig_IsComplement(pChild) )
{
CountNonConst0++;
continue;
@@ -104,6 +104,37 @@ int Fra_FraigMiterStatus( Aig_Man_t * p )
/**Function*************************************************************
+ Synopsis [Reports the status of the miter.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Fra_FraigMiterAssertedOutput( Aig_Man_t * p )
+{
+ Aig_Obj_t * pObj, * pChild;
+ int i;
+ Aig_ManForEachPoSeq( p, pObj, i )
+ {
+ pChild = Aig_ObjChild0(pObj);
+ // check if the output is constant 0
+ if ( pChild == Aig_ManConst0(p) )
+ continue;
+ // check if the output is constant 1
+ if ( pChild == Aig_ManConst1(p) )
+ return i;
+ // check if the output can be not constant 0
+ if ( Aig_Regular(pChild)->fPhase != (unsigned)Aig_IsComplement(pChild) )
+ return i;
+ }
+ return -1;
+}
+
+/**Function*************************************************************
+
Synopsis [Write speculative miter for one node.]
Description []
@@ -410,7 +441,7 @@ Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax )
SeeAlso []
***********************************************************************/
-Aig_Man_t * Fra_FraigEquivence( Aig_Man_t * pManAig, int nConfMax )
+Aig_Man_t * Fra_FraigEquivence( Aig_Man_t * pManAig, int nConfMax, int fProve )
{
Aig_Man_t * pFraig;
Fra_Par_t Pars, * pPars = &Pars;
@@ -419,7 +450,7 @@ Aig_Man_t * Fra_FraigEquivence( Aig_Man_t * pManAig, int nConfMax )
pPars->fChoicing = 0;
pPars->fDoSparse = 1;
pPars->fSpeculate = 0;
- pPars->fProve = 0;
+ pPars->fProve = fProve;
pPars->fVerbose = 0;
pPars->fDontShowBar = 1;
pFraig = Fra_FraigPerform( pManAig, pPars );
diff --git a/src/aig/fra/fraLcr.c b/src/aig/fra/fraLcr.c
index 597dda71..daa789a8 100644
--- a/src/aig/fra/fraLcr.c
+++ b/src/aig/fra/fraLcr.c
@@ -159,7 +159,8 @@ Fra_Man_t * Fra_LcrAigPrepare( Aig_Man_t * pAig )
int i;
p = ALLOC( Fra_Man_t, 1 );
memset( p, 0, sizeof(Fra_Man_t) );
- Aig_ManForEachPi( pAig, pObj, i )
+// Aig_ManForEachPi( pAig, pObj, i )
+ Aig_ManForEachObj( pAig, pObj, i )
pObj->pData = p;
return p;
}
@@ -532,6 +533,7 @@ timeSim = clock() - clk2;
// check if simulation discovered non-constant-0 POs
if ( fProve && pSml->fNonConstOut )
{
+ pAig->pSeqModel = Fra_SmlGetCounterExample( pSml );
Fra_SmlStop( pSml );
return NULL;
}
@@ -587,7 +589,7 @@ clk2 = clock();
pAigPart = Fra_LcrCreatePart( p, vPart );
p->timeTrav += clock() - clk2;
clk2 = clock();
- pAigNew = Fra_FraigEquivence( pAigPart, nConfMax );
+ pAigNew = Fra_FraigEquivence( pAigPart, nConfMax, 0 );
p->timeFraig += clock() - clk2;
Vec_PtrPush( p->vFraigs, pAigNew );
Aig_ManStop( pAigPart );
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index 15206a4d..573d3570 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -150,6 +150,7 @@ clk = clock();
pNew = Aig_ManDup( pTemp = pNew, 1 );
Aig_ManStop( pTemp );
pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 100000, 1, fVeryVerbose, &nIter );
+ p->pSeqModel = pTemp->pSeqModel; pTemp->pSeqModel = NULL;
Aig_ManStop( pTemp );
if ( pNew == NULL )
{
@@ -169,7 +170,7 @@ PRT( "Time", clock() - clk );
// perform fraiging
clk = clock();
- pNew = Fra_FraigEquivence( pTemp = pNew, 100 );
+ pNew = Fra_FraigEquivence( pTemp = pNew, 100, 0 );
Aig_ManStop( pTemp );
if ( fVerbose )
{
@@ -240,6 +241,7 @@ PRT( "Time", clock() - clk );
}
if ( pSml->fNonConstOut )
{
+ p->pSeqModel = Fra_SmlGetCounterExample( pSml );
Fra_SmlStop( pSml );
Aig_ManStop( pNew );
RetValue = 0;
diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c
index b77c775a..3e8f2da1 100644
--- a/src/aig/fra/fraSim.c
+++ b/src/aig/fra/fraSim.c
@@ -252,12 +252,14 @@ void Fra_SmlSavePattern( Fra_Man_t * p )
SeeAlso []
***********************************************************************/
-void Fra_SmlCheckOutputSavePattern( Fra_Man_t * p, Aig_Obj_t * pObj )
+void Fra_SmlCheckOutputSavePattern( Fra_Man_t * p, Aig_Obj_t * pObjPo )
{
+ Aig_Obj_t * pFanin, * pObjPi;
unsigned * pSims;
int i, k, BestPat, * pModel;
// find the word of the pattern
- pSims = Fra_ObjSim(p->pSml, pObj->Id);
+ pFanin = Aig_ObjFanin0(pObjPo);
+ pSims = Fra_ObjSim(p->pSml, pFanin->Id);
for ( i = 0; i < p->pSml->nWordsTotal; i++ )
if ( pSims[i] )
break;
@@ -270,12 +272,13 @@ void Fra_SmlCheckOutputSavePattern( Fra_Man_t * p, Aig_Obj_t * pObj )
// determine the best pattern
BestPat = i * 32 + k;
// fill in the counter-example data
- pModel = ALLOC( int, Aig_ManPiNum(p->pManFraig) );
- Aig_ManForEachPi( p->pManAig, pObj, i )
+ pModel = ALLOC( int, Aig_ManPiNum(p->pManFraig)+1 );
+ Aig_ManForEachPi( p->pManAig, pObjPi, i )
{
- pModel[i] = Aig_InfoHasBit(Fra_ObjSim(p->pSml, pObj->Id), BestPat);
+ pModel[i] = Aig_InfoHasBit(Fra_ObjSim(p->pSml, pObjPi->Id), BestPat);
// printf( "%d", pModel[i] );
}
+ pModel[Aig_ManPiNum(p->pManAig)] = pObjPo->Id;
// printf( "\n" );
// set the model
assert( p->pManFraig->pData == NULL );
@@ -306,7 +309,7 @@ int Fra_SmlCheckOutput( Fra_Man_t * p )
if ( !Fra_SmlNodeIsConst( Aig_ObjFanin0(pObj) ) )
{
// create the counter-example from this pattern
- Fra_SmlCheckOutputSavePattern( p, Aig_ObjFanin0(pObj) );
+ Fra_SmlCheckOutputSavePattern( p, pObj );
return 1;
}
}
@@ -680,6 +683,8 @@ void Fra_SmlSimulate( Fra_Man_t * p, int fInit )
// start the classes
Fra_SmlInitialize( p->pSml, fInit );
Fra_SmlSimulateOne( p->pSml );
+ if ( p->pPars->fProve && Fra_SmlCheckOutput(p) )
+ return;
Fra_ClassesPrepare( p->pCla, p->pPars->fLatchCorr );
// Fra_ClassesPrint( p->pCla, 0 );
if ( fVerbose )
@@ -816,6 +821,244 @@ Fra_Sml_t * Fra_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nW
return p;
}
+/**Function*************************************************************
+
+ Synopsis [Resimulates the counter-example.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Fra_SmlRunCounterExample( Aig_Man_t * pAig, Fra_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 [Allocates a counter-example.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Fra_Cex_t * Fra_SmlAllocCounterExample( int nRegs, int nRealPis, int nFrames )
+{
+ Fra_Cex_t * pCex;
+ int nWords = Aig_BitWordNum( nRegs + nRealPis * nFrames );
+ pCex = (Fra_Cex_t *)malloc( sizeof(Fra_Cex_t) + sizeof(unsigned) * nWords );
+ memset( pCex, 0, sizeof(Fra_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( Fra_Cex_t * pCex )
+{
+ free( pCex );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Creates sequential counter-example from the simulation info.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Fra_Cex_t * Fra_SmlGetCounterExample( Fra_Sml_t * p )
+{
+ Fra_Cex_t * pCex;
+ Aig_Obj_t * pObj;
+ unsigned * pSims;
+ int iPo, iFrame, iBit, i, k;
+
+ // make sure the simulation manager has it
+ assert( p->fNonConstOut );
+
+ // find the first output that failed
+ iPo = -1;
+ iBit = -1;
+ iFrame = -1;
+ Aig_ManForEachPoSeq( p->pAig, pObj, iPo )
+ {
+ if ( Fra_SmlNodeIsZero(p, pObj) )
+ continue;
+ pSims = Fra_ObjSim( p, pObj->Id );
+ for ( i = p->nWordsPref; i < p->nWordsTotal; i++ )
+ if ( pSims[i] )
+ {
+ iFrame = i / p->nWordsFrame;
+ iBit = 32 * (i % p->nWordsFrame) + Aig_WordFindFirstBit( pSims[i] );
+ break;
+ }
+ break;
+ }
+ assert( iPo < Aig_ManPoNum(p->pAig)-Aig_ManRegNum(p->pAig) );
+ assert( iFrame < p->nFrames );
+ 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->iPo = iPo;
+ pCex->iFrame = iFrame;
+
+ // copy the bit data
+ Aig_ManForEachLoSeq( p->pAig, pObj, k )
+ {
+ pSims = Fra_ObjSim( p, pObj->Id );
+ if ( Aig_InfoHasBit( pSims, iBit ) )
+ Aig_InfoSetBit( pCex->pData, k );
+ }
+ for ( i = 0; i <= iFrame; i++ )
+ {
+ Aig_ManForEachPiSeq( p->pAig, pObj, k )
+ {
+ pSims = Fra_ObjSim( p, pObj->Id );
+ if ( Aig_InfoHasBit( pSims, 32 * p->nWordsFrame * i + iBit ) )
+ Aig_InfoSetBit( pCex->pData, pCex->nRegs + pCex->nPis * i + k );
+ }
+ }
+ // verify the counter example
+ if ( !Fra_SmlRunCounterExample( p->pAig, pCex ) )
+ {
+ printf( "Fra_SmlGetCounterExample(): Counter-example is invalid.\n" );
+ Fra_SmlFreeCounterExample( pCex );
+ pCex = NULL;
+ }
+ return pCex;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Generates seq counter-example from the combinational one.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Fra_Cex_t * Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, int * pModel )
+{
+ Fra_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 = Fra_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 ( !Fra_SmlRunCounterExample( pAig, pCex ) )
+ {
+ printf( "Fra_SmlGetCounterExample(): Counter-example is invalid.\n" );
+ Fra_SmlFreeCounterExample( pCex );
+ pCex = NULL;
+ }
+ return pCex;
+
+}
+
+/**Function*************************************************************
+
+ Synopsis [Make the trivial counter-example for the trivially asserted output.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Fra_Cex_t * Fra_SmlTrivCounterExample( Aig_Man_t * pAig, int iFrameOut )
+{
+ Fra_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;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
generated by cgit v1.2.3 (git 2.25.1) at 2025-01-19 01:55:12 +0000