summaryrefslogtreecommitdiffstats
path: root/src/aig/cec/cecSeq.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/cec/cecSeq.c')
-rw-r--r--src/aig/cec/cecSeq.c148
1 files changed, 128 insertions, 20 deletions
diff --git a/src/aig/cec/cecSeq.c b/src/aig/cec/cecSeq.c
index b19950b3..49f2a018 100644
--- a/src/aig/cec/cecSeq.c
+++ b/src/aig/cec/cecSeq.c
@@ -125,9 +125,9 @@ void Cec_ManSeqDeriveInfoInitRandom( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Gia_Ce
int Cec_ManSeqResimulate( Cec_ManSim_t * p, Vec_Ptr_t * vInfo )
{
unsigned * pInfo0, * pInfo1;
- int f, i, k, w, RetValue = 0;
+ int f, i, k, w;
// assert( Gia_ManRegNum(p->pAig) > 0 );
- assert( Vec_PtrSize(vInfo) == Gia_ManRegNum(p->pAig) + Gia_ManPiNum(p->pAig) * p->pPars->nRounds );
+ assert( Vec_PtrSize(vInfo) == Gia_ManRegNum(p->pAig) + Gia_ManPiNum(p->pAig) * p->pPars->nFrames );
for ( k = 0; k < Gia_ManRegNum(p->pAig); k++ )
{
pInfo0 = Vec_PtrEntry( vInfo, k );
@@ -135,7 +135,7 @@ int Cec_ManSeqResimulate( Cec_ManSim_t * p, Vec_Ptr_t * vInfo )
for ( w = 0; w < p->nWords; w++ )
pInfo1[w] = pInfo0[w];
}
- for ( f = 0; f < p->pPars->nRounds; f++ )
+ for ( f = 0; f < p->pPars->nFrames; f++ )
{
for ( i = 0; i < Gia_ManPiNum(p->pAig); i++ )
{
@@ -152,13 +152,10 @@ int Cec_ManSeqResimulate( Cec_ManSim_t * p, Vec_Ptr_t * vInfo )
pInfo1[w] = pInfo0[w];
}
if ( Cec_ManSimSimulateRound( p, p->vCiSimInfo, p->vCoSimInfo ) )
- {
- printf( "One of the outputs of the miter is asserted.\n" );
- RetValue = 1;
- }
+ return 1;
}
assert( k == Vec_PtrSize(vInfo) );
- return RetValue;
+ return 0;
}
/**Function*************************************************************
@@ -172,15 +169,16 @@ int Cec_ManSeqResimulate( Cec_ManSim_t * p, Vec_Ptr_t * vInfo )
SeeAlso []
***********************************************************************/
-int Cec_ManSeqResimulateInfo( Gia_Man_t * pAig, Vec_Ptr_t * vSimInfo, Gia_Cex_t * pBestState )
+int Cec_ManSeqResimulateInfo( Gia_Man_t * pAig, Vec_Ptr_t * vSimInfo, Gia_Cex_t * pBestState, int fCheckMiter )
{
Cec_ParSim_t ParsSim, * pParsSim = &ParsSim;
Cec_ManSim_t * pSim;
int RetValue, clkTotal = clock();
assert( (Vec_PtrSize(vSimInfo) - Gia_ManRegNum(pAig)) % Gia_ManPiNum(pAig) == 0 );
Cec_ManSimSetDefaultParams( pParsSim );
- pParsSim->nRounds = (Vec_PtrSize(vSimInfo) - Gia_ManRegNum(pAig)) / Gia_ManPiNum(pAig);
+ pParsSim->nFrames = (Vec_PtrSize(vSimInfo) - Gia_ManRegNum(pAig)) / Gia_ManPiNum(pAig);
pParsSim->nWords = Vec_PtrReadWordsSimInfo( vSimInfo );
+ pParsSim->fCheckMiter = fCheckMiter;
Gia_ManSetRefs( pAig );
pSim = Cec_ManSimStart( pAig, pParsSim );
if ( pBestState )
@@ -228,25 +226,83 @@ int Cec_ManSeqResimulateCounter( Gia_Man_t * pAig, Cec_ParSim_t * pPars, Gia_Cex
return -1;
}
if ( pPars->fVerbose )
- printf( "Resimulating %d timeframes.\n", pPars->nRounds + pCex->iFrame + 1 );
+ printf( "Resimulating %d timeframes.\n", pPars->nFrames + pCex->iFrame + 1 );
Gia_ManRandom( 1 );
vSimInfo = Vec_PtrAllocSimInfo( Gia_ManRegNum(pAig) +
- Gia_ManPiNum(pAig) * (pPars->nRounds + pCex->iFrame + 1), 1 );
+ Gia_ManPiNum(pAig) * (pPars->nFrames + pCex->iFrame + 1), 1 );
Cec_ManSeqDeriveInfoFromCex( vSimInfo, pAig, pCex );
if ( pPars->fVerbose )
Gia_ManEquivPrintClasses( pAig, 0, 0 );
- RetValue = Cec_ManSeqResimulateInfo( pAig, vSimInfo, NULL );
+ RetValue = Cec_ManSeqResimulateInfo( pAig, vSimInfo, NULL, pPars->fCheckMiter );
if ( pPars->fVerbose )
Gia_ManEquivPrintClasses( pAig, 0, 0 );
Vec_PtrFree( vSimInfo );
if ( pPars->fVerbose )
ABC_PRT( "Time", clock() - clkTotal );
+ if ( RetValue )
+ printf( "Cec_ManSeqResimulateCounter(): An output of the miter is asserted!\n" );
return RetValue;
}
/**Function*************************************************************
+ Synopsis [Returns the number of POs that are not const0 cands.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Cec_ManCountNonConstOutputs( Gia_Man_t * pAig )
+{
+ Gia_Obj_t * pObj;
+ int i, Counter = 0;
+ if ( pAig->pReprs == NULL )
+ return -1;
+ Gia_ManForEachPo( pAig, pObj, i )
+ if ( !Gia_ObjIsConst( pAig, Gia_ObjFaninId0p(pAig, pObj) ) )
+ Counter++;
+ return Counter;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns the number of POs that are not const0 cands.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Cec_ManCheckNonTrivialCands( Gia_Man_t * pAig )
+{
+ Gia_Obj_t * pObj;
+ int i, RetValue = 0;
+ if ( pAig->pReprs == NULL )
+ return 0;
+ // label internal nodes driving POs
+ Gia_ManForEachPo( pAig, pObj, i )
+ Gia_ObjFanin0(pObj)->fMark0 = 1;
+ // check if there are non-labled equivs
+ Gia_ManForEachObj( pAig, pObj, i )
+ if ( Gia_ObjIsCand(pObj) && !pObj->fMark0 && Gia_ObjRepr(pAig, i) != GIA_VOID )
+ {
+ RetValue = 1;
+ break;
+ }
+ // clean internal nodes driving POs
+ Gia_ManForEachPo( pAig, pObj, i )
+ Gia_ObjFanin0(pObj)->fMark0 = 0;
+ return RetValue;
+}
+
+/**Function*************************************************************
+
Synopsis [Performs semiformal refinement of equivalence classes.]
Description []
@@ -258,13 +314,15 @@ int Cec_ManSeqResimulateCounter( Gia_Man_t * pAig, Cec_ParSim_t * pPars, Gia_Cex
***********************************************************************/
int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars )
{
- int nAddFrames = 10; // additional timeframes to simulate
+ int nAddFrames = 16; // additional timeframes to simulate
+ int nCountNoRef = 0;
+ int nFramesReal;
Cec_ParSat_t ParsSat, * pParsSat = &ParsSat;
Vec_Ptr_t * vSimInfo;
Vec_Str_t * vStatus;
Gia_Cex_t * pState;
- Gia_Man_t * pSrm;
- int r, nPats, RetValue = -1;
+ Gia_Man_t * pSrm, * pReduce, * pAux;
+ int r, nPats, RetValue = 0;
if ( pAig->pReprs == NULL )
{
printf( "Cec_ManSeqSemiformal(): Equivalence classes are not available.\n" );
@@ -290,22 +348,36 @@ int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars )
Gia_ManEquivPrintClasses( pAig, 0, 0 );
}
// perform the given number of BMC rounds
+ Gia_ManCleanMark0( pAig );
for ( r = 0; r < pPars->nRounds; r++ )
{
+ if ( !Cec_ManCheckNonTrivialCands(pAig) )
+ {
+ printf( "Cec_ManSeqSemiformal: There are only trivial equiv candidates left (PO drivers). Quitting.\n" );
+ break;
+ }
// Gia_ManPrintCounterExample( pState );
// derive speculatively reduced model
- pSrm = Gia_ManSpecReduceInit( pAig, pState, pPars->nFrames, pPars->fDualOut );
- assert( Gia_ManRegNum(pSrm) == 0 && Gia_ManPiNum(pSrm) == (Gia_ManPiNum(pAig) * pPars->nFrames) );
+// pSrm = Gia_ManSpecReduceInit( pAig, pState, pPars->nFrames, pPars->fDualOut );
+ pSrm = Gia_ManSpecReduceInitFrames( pAig, pState, pPars->nFrames, &nFramesReal, pPars->fDualOut, pPars->nMinOutputs );
+ if ( pSrm == NULL )
+ {
+ printf( "Quitting refinement because miter could not be unrolled.\n" );
+ break;
+ }
+ assert( Gia_ManRegNum(pSrm) == 0 && Gia_ManPiNum(pSrm) == (Gia_ManPiNum(pAig) * nFramesReal) );
+ if ( pPars->fVerbose )
+ printf( "Unrolled for %d frames.\n", nFramesReal );
// allocate room for simulation info
vSimInfo = Vec_PtrAllocSimInfo( Gia_ManRegNum(pAig) +
- Gia_ManPiNum(pAig) * (pPars->nFrames + nAddFrames), pPars->nWords );
+ Gia_ManPiNum(pAig) * (nFramesReal + nAddFrames), pPars->nWords );
Cec_ManSeqDeriveInfoInitRandom( vSimInfo, pAig, pState );
// fill in simulation info with counter-examples
vStatus = Cec_ManSatSolveSeq( vSimInfo, pSrm, pParsSat, Gia_ManRegNum(pAig), &nPats );
Vec_StrFree( vStatus );
Gia_ManStop( pSrm );
// resimulate and refine the classes
- RetValue = Cec_ManSeqResimulateInfo( pAig, vSimInfo, pState );
+ RetValue = Cec_ManSeqResimulateInfo( pAig, vSimInfo, pState, pPars->fCheckMiter );
Vec_PtrFree( vSimInfo );
assert( pState->iPo >= 0 ); // hit counter
pState->iPo = -1;
@@ -314,11 +386,47 @@ int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars )
printf( "BMC = %3d ", nPats );
Gia_ManEquivPrintClasses( pAig, 0, 0 );
}
+
+ // write equivalence classes
+ Gia_WriteAiger( pAig, "gore.aig", 0, 0 );
+ // reduce the model
+ pReduce = Gia_ManSpecReduce( pAig, 0, 0 );
+ if ( pReduce )
+ {
+ pReduce = Gia_ManSeqStructSweep( pAux = pReduce, 1, 1, 0 );
+ Gia_ManStop( pAux );
+ Gia_WriteAiger( pReduce, "gsrm.aig", 0, 0 );
+// printf( "Speculatively reduced model was written into file \"%s\".\n", "gsrm.aig" );
+// Gia_ManPrintStatsShort( pReduce );
+ Gia_ManStop( pReduce );
+ }
+
+ if ( RetValue )
+ {
+ printf( "Cec_ManSeqSemiformal(): An output of the miter is asserted. Refinement stopped.\n" );
+ break;
+ }
+ // decide when to stop
+ if ( nPats > 0 )
+ nCountNoRef = 0;
+ else if ( ++nCountNoRef == pPars->nNonRefines )
+ break;
}
ABC_FREE( pState );
+ if ( pPars->fCheckMiter )
+ {
+ int nNonConsts = Cec_ManCountNonConstOutputs( pAig );
+ if ( nNonConsts )
+ printf( "The number of POs that are not const-0 candidates = %d.\n", nNonConsts );
+ }
return RetValue;
}
+//&r s13207.aig; &ps; &equiv; &ps; &semi -R 2 -vm
+//&r bug/50/temp.aig; &ps; &equiv -smv; &semi -v
+//r mentor/1_05c.blif; st; &get; &ps; &equiv -smv; &semi -mv
+//&r bug/50/hdl1.aig; &ps; &equiv -smv; &semi -mv; &srm; &r gsrm.aig; &ps
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-17 08:38:45 +0000