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.c71
1 files changed, 38 insertions, 33 deletions
diff --git a/src/aig/cec/cecSeq.c b/src/aig/cec/cecSeq.c
index 49f2a018..b91e8523 100644
--- a/src/aig/cec/cecSeq.c
+++ b/src/aig/cec/cecSeq.c
@@ -20,6 +20,9 @@
#include "cecInt.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -39,7 +42,7 @@
SeeAlso []
***********************************************************************/
-void Cec_ManSeqDeriveInfoFromCex( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Gia_Cex_t * pCex )
+void Cec_ManSeqDeriveInfoFromCex( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Abc_Cex_t * pCex )
{
unsigned * pInfo;
int k, i, w, nWords;
@@ -56,14 +59,14 @@ void Cec_ManSeqDeriveInfoFromCex( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Gia_Cex_t
*/
for ( k = 0; k < Gia_ManRegNum(pAig); k++ )
{
- pInfo = Vec_PtrEntry( vInfo, k );
+ pInfo = (unsigned *)Vec_PtrEntry( vInfo, k );
for ( w = 0; w < nWords; w++ )
pInfo[w] = 0;
}
for ( i = pCex->nRegs; i < pCex->nBits; i++ )
{
- pInfo = Vec_PtrEntry( vInfo, k++ );
+ pInfo = (unsigned *)Vec_PtrEntry( vInfo, k++ );
for ( w = 0; w < nWords; w++ )
pInfo[w] = Gia_ManRandom(0);
// set simulation pattern and make sure it is second (first will be erased during simulation)
@@ -72,7 +75,7 @@ void Cec_ManSeqDeriveInfoFromCex( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Gia_Cex_t
}
for ( ; k < Vec_PtrSize(vInfo); k++ )
{
- pInfo = Vec_PtrEntry( vInfo, k );
+ pInfo = (unsigned *)Vec_PtrEntry( vInfo, k );
for ( w = 0; w < nWords; w++ )
pInfo[w] = Gia_ManRandom(0);
}
@@ -89,7 +92,7 @@ void Cec_ManSeqDeriveInfoFromCex( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Gia_Cex_t
SeeAlso []
***********************************************************************/
-void Cec_ManSeqDeriveInfoInitRandom( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Gia_Cex_t * pCex )
+void Cec_ManSeqDeriveInfoInitRandom( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Abc_Cex_t * pCex )
{
unsigned * pInfo;
int k, w, nWords;
@@ -98,14 +101,14 @@ void Cec_ManSeqDeriveInfoInitRandom( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Gia_Ce
assert( Gia_ManRegNum(pAig) <= Vec_PtrSize(vInfo) );
for ( k = 0; k < Gia_ManRegNum(pAig); k++ )
{
- pInfo = Vec_PtrEntry( vInfo, k );
+ pInfo = (unsigned *)Vec_PtrEntry( vInfo, k );
for ( w = 0; w < nWords; w++ )
pInfo[w] = (pCex && Gia_InfoHasBit(pCex->pData, k))? ~0 : 0;
}
for ( ; k < Vec_PtrSize(vInfo); k++ )
{
- pInfo = Vec_PtrEntry( vInfo, k );
+ pInfo = (unsigned *)Vec_PtrEntry( vInfo, k );
for ( w = 0; w < nWords; w++ )
pInfo[w] = Gia_ManRandom( 0 );
}
@@ -130,8 +133,8 @@ int Cec_ManSeqResimulate( Cec_ManSim_t * p, Vec_Ptr_t * vInfo )
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 );
- pInfo1 = Vec_PtrEntry( p->vCoSimInfo, Gia_ManPoNum(p->pAig) + k );
+ pInfo0 = (unsigned *)Vec_PtrEntry( vInfo, k );
+ pInfo1 = (unsigned *)Vec_PtrEntry( p->vCoSimInfo, Gia_ManPoNum(p->pAig) + k );
for ( w = 0; w < p->nWords; w++ )
pInfo1[w] = pInfo0[w];
}
@@ -139,15 +142,15 @@ int Cec_ManSeqResimulate( Cec_ManSim_t * p, Vec_Ptr_t * vInfo )
{
for ( i = 0; i < Gia_ManPiNum(p->pAig); i++ )
{
- pInfo0 = Vec_PtrEntry( vInfo, k++ );
- pInfo1 = Vec_PtrEntry( p->vCiSimInfo, i );
+ pInfo0 = (unsigned *)Vec_PtrEntry( vInfo, k++ );
+ pInfo1 = (unsigned *)Vec_PtrEntry( p->vCiSimInfo, i );
for ( w = 0; w < p->nWords; w++ )
pInfo1[w] = pInfo0[w];
}
for ( i = 0; i < Gia_ManRegNum(p->pAig); i++ )
{
- pInfo0 = Vec_PtrEntry( p->vCoSimInfo, Gia_ManPoNum(p->pAig) + i );
- pInfo1 = Vec_PtrEntry( p->vCiSimInfo, Gia_ManPiNum(p->pAig) + i );
+ pInfo0 = (unsigned *)Vec_PtrEntry( p->vCoSimInfo, Gia_ManPoNum(p->pAig) + i );
+ pInfo1 = (unsigned *)Vec_PtrEntry( p->vCiSimInfo, Gia_ManPiNum(p->pAig) + i );
for ( w = 0; w < p->nWords; w++ )
pInfo1[w] = pInfo0[w];
}
@@ -169,7 +172,7 @@ 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 fCheckMiter )
+int Cec_ManSeqResimulateInfo( Gia_Man_t * pAig, Vec_Ptr_t * vSimInfo, Abc_Cex_t * pBestState, int fCheckMiter )
{
Cec_ParSim_t ParsSim, * pParsSim = &ParsSim;
Cec_ManSim_t * pSim;
@@ -200,33 +203,33 @@ int Cec_ManSeqResimulateInfo( Gia_Man_t * pAig, Vec_Ptr_t * vSimInfo, Gia_Cex_t
SeeAlso []
***********************************************************************/
-int Cec_ManSeqResimulateCounter( Gia_Man_t * pAig, Cec_ParSim_t * pPars, Gia_Cex_t * pCex )
+int Cec_ManSeqResimulateCounter( Gia_Man_t * pAig, Cec_ParSim_t * pPars, Abc_Cex_t * pCex )
{
Vec_Ptr_t * vSimInfo;
int RetValue, clkTotal = clock();
if ( pCex == NULL )
{
- printf( "Cec_ManSeqResimulateCounter(): Counter-example is not available.\n" );
+ Abc_Print( 1, "Cec_ManSeqResimulateCounter(): Counter-example is not available.\n" );
return -1;
}
if ( pAig->pReprs == NULL )
{
- printf( "Cec_ManSeqResimulateCounter(): Equivalence classes are not available.\n" );
+ Abc_Print( 1, "Cec_ManSeqResimulateCounter(): Equivalence classes are not available.\n" );
return -1;
}
if ( Gia_ManRegNum(pAig) == 0 )
{
- printf( "Cec_ManSeqResimulateCounter(): Not a sequential AIG.\n" );
+ Abc_Print( 1, "Cec_ManSeqResimulateCounter(): Not a sequential AIG.\n" );
return -1;
}
// if ( Gia_ManRegNum(pAig) != pCex->nRegs || Gia_ManPiNum(pAig) != pCex->nPis )
if ( Gia_ManPiNum(pAig) != pCex->nPis )
{
- printf( "Cec_ManSeqResimulateCounter(): The number of PIs in the AIG and the counter-example differ.\n" );
+ Abc_Print( 1, "Cec_ManSeqResimulateCounter(): The number of PIs in the AIG and the counter-example differ.\n" );
return -1;
}
if ( pPars->fVerbose )
- printf( "Resimulating %d timeframes.\n", pPars->nFrames + pCex->iFrame + 1 );
+ Abc_Print( 1, "Resimulating %d timeframes.\n", pPars->nFrames + pCex->iFrame + 1 );
Gia_ManRandom( 1 );
vSimInfo = Vec_PtrAllocSimInfo( Gia_ManRegNum(pAig) +
Gia_ManPiNum(pAig) * (pPars->nFrames + pCex->iFrame + 1), 1 );
@@ -240,7 +243,7 @@ int Cec_ManSeqResimulateCounter( Gia_Man_t * pAig, Cec_ParSim_t * pPars, Gia_Cex
if ( pPars->fVerbose )
ABC_PRT( "Time", clock() - clkTotal );
if ( RetValue )
- printf( "Cec_ManSeqResimulateCounter(): An output of the miter is asserted!\n" );
+ Abc_Print( 1, "Cec_ManSeqResimulateCounter(): An output of the miter is asserted!\n" );
return RetValue;
}
@@ -320,17 +323,17 @@ int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars )
Cec_ParSat_t ParsSat, * pParsSat = &ParsSat;
Vec_Ptr_t * vSimInfo;
Vec_Str_t * vStatus;
- Gia_Cex_t * pState;
+ Abc_Cex_t * pState;
Gia_Man_t * pSrm, * pReduce, * pAux;
int r, nPats, RetValue = 0;
if ( pAig->pReprs == NULL )
{
- printf( "Cec_ManSeqSemiformal(): Equivalence classes are not available.\n" );
+ Abc_Print( 1, "Cec_ManSeqSemiformal(): Equivalence classes are not available.\n" );
return -1;
}
if ( Gia_ManRegNum(pAig) == 0 )
{
- printf( "Cec_ManSeqSemiformal(): Not a sequential AIG.\n" );
+ Abc_Print( 1, "Cec_ManSeqSemiformal(): Not a sequential AIG.\n" );
return -1;
}
Gia_ManRandom( 1 );
@@ -344,7 +347,7 @@ int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars )
pParsSat->fVerbose = pPars->fVerbose;
if ( pParsSat->fVerbose )
{
- printf( "Starting: " );
+ Abc_Print( 1, "Starting: " );
Gia_ManEquivPrintClasses( pAig, 0, 0 );
}
// perform the given number of BMC rounds
@@ -353,7 +356,7 @@ int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars )
{
if ( !Cec_ManCheckNonTrivialCands(pAig) )
{
- printf( "Cec_ManSeqSemiformal: There are only trivial equiv candidates left (PO drivers). Quitting.\n" );
+ Abc_Print( 1, "Cec_ManSeqSemiformal: There are only trivial equiv candidates left (PO drivers). Quitting.\n" );
break;
}
// Gia_ManPrintCounterExample( pState );
@@ -362,12 +365,12 @@ int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars )
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" );
+ Abc_Print( 1, "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 );
+ Abc_Print( 1, "Unrolled for %d frames.\n", nFramesReal );
// allocate room for simulation info
vSimInfo = Vec_PtrAllocSimInfo( Gia_ManRegNum(pAig) +
Gia_ManPiNum(pAig) * (nFramesReal + nAddFrames), pPars->nWords );
@@ -383,27 +386,27 @@ int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars )
pState->iPo = -1;
if ( pPars->fVerbose )
{
- printf( "BMC = %3d ", nPats );
+ Abc_Print( 1, "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 );
+ pReduce = Gia_ManSpecReduce( pAig, 0, 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" );
+// Abc_Print( 1, "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" );
+ Abc_Print( 1, "Cec_ManSeqSemiformal(): An output of the miter is asserted. Refinement stopped.\n" );
break;
}
// decide when to stop
@@ -417,7 +420,7 @@ int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars )
{
int nNonConsts = Cec_ManCountNonConstOutputs( pAig );
if ( nNonConsts )
- printf( "The number of POs that are not const-0 candidates = %d.\n", nNonConsts );
+ Abc_Print( 1, "The number of POs that are not const-0 candidates = %d.\n", nNonConsts );
}
return RetValue;
}
@@ -432,3 +435,5 @@ int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars )
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-24 17:45:19 +0000