summaryrefslogtreecommitdiffstats
path: root/src/aig/cec
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/cec')
-rw-r--r--src/aig/cec/cec.c5
-rw-r--r--src/aig/cec/cec.h50
-rw-r--r--src/aig/cec/cecCec.c124
-rw-r--r--src/aig/cec/cecChoice.c106
-rw-r--r--src/aig/cec/cecClass.c48
-rw-r--r--src/aig/cec/cecCore.c73
-rw-r--r--src/aig/cec/cecCorr.c114
-rw-r--r--src/aig/cec/cecCorr_updated.c7
-rw-r--r--src/aig/cec/cecInt.h26
-rw-r--r--src/aig/cec/cecIso.c11
-rw-r--r--src/aig/cec/cecMan.c45
-rw-r--r--src/aig/cec/cecPat.c19
-rw-r--r--src/aig/cec/cecSeq.c71
-rw-r--r--src/aig/cec/cecSim.c5
-rw-r--r--src/aig/cec/cecSolve.c75
-rw-r--r--src/aig/cec/cecSweep.c11
-rw-r--r--src/aig/cec/cecSynth.c380
-rw-r--r--src/aig/cec/module.make1
18 files changed, 838 insertions, 333 deletions
diff --git a/src/aig/cec/cec.c b/src/aig/cec/cec.c
index 17b27ec5..6968a599 100644
--- a/src/aig/cec/cec.c
+++ b/src/aig/cec/cec.c
@@ -20,6 +20,9 @@
#include "cecInt.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -46,3 +49,5 @@
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/cec/cec.h b/src/aig/cec/cec.h
index 199d6939..e4547f5e 100644
--- a/src/aig/cec/cec.h
+++ b/src/aig/cec/cec.h
@@ -21,6 +21,7 @@
#ifndef __CEC_H__
#define __CEC_H__
+
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
@@ -29,9 +30,10 @@
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
-#ifdef __cplusplus
-extern "C" {
-#endif
+
+
+ABC_NAMESPACE_HEADER_START
+
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
@@ -103,8 +105,10 @@ struct Cec_ParFra_t_
// int fFirstStop; // stop on the first sat output
int fDualOut; // miter with separate outputs
int fColorDiff; // miter with separate outputs
+ int fSatSweeping; // enable SAT sweeping
int fVeryVerbose; // verbose stats
int fVerbose; // verbose stats
+ int iOutFail; // the failed output
};
// combinational equivalence checking parameters
@@ -118,6 +122,7 @@ struct Cec_ParCec_t_
int fRewriting; // enables AIG rewriting
int fVeryVerbose; // verbose stats
int fVerbose; // verbose stats
+ int iOutFail; // the number of failed output
};
// sequential register correspodence parameters
@@ -129,6 +134,8 @@ struct Cec_ParCor_t_
int nFrames; // the number of time frames
int nPrefix; // the number of time frames in the prefix
int nBTLimit; // conflict limit at a node
+ int nLevelMax; // (scorr only) the max number of levels
+ int nStepsMax; // (scorr only) the max number of induction steps
int fLatchCorr; // consider only latch outputs
int fUseRings; // use rings
int fMakeChoices; // use equilvaences as choices
@@ -138,6 +145,9 @@ struct Cec_ParCor_t_
int fVerboseFlops; // verbose stats
int fVeryVerbose; // verbose stats
int fVerbose; // verbose stats
+ // callback
+ void * pData;
+ void * pFunc;
};
// sequential register correspodence parameters
@@ -153,6 +163,23 @@ struct Cec_ParChc_t_
int fVerbose; // verbose stats
};
+// sequential synthesis parameters
+typedef struct Cec_ParSeq_t_ Cec_ParSeq_t;
+struct Cec_ParSeq_t_
+{
+ int fUseLcorr; // enables latch correspondence
+ int fUseScorr; // enables signal correspondence
+ int nBTLimit; // (scorr/lcorr) conflict limit at a node
+ int nFrames; // (scorr/lcorr) the number of timeframes
+ int nLevelMax; // (scorr only) the max number of levels
+ int fConsts; // (scl only) merging constants
+ int fEquivs; // (scl only) merging equivalences
+ int fUseMiniSat; // enables MiniSat in lcorr/scorr
+ int nMinDomSize; // the size of minimum clock domain
+ int fVeryVerbose; // verbose stats
+ int fVerbose; // verbose stats
+};
+
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@@ -167,6 +194,7 @@ extern int Cec_ManVerifyTwo( Gia_Man_t * p0, Gia_Man_t * p1, int fVerb
/*=== cecChoice.c ==========================================================*/
extern Gia_Man_t * Cec_ManChoiceComputation( Gia_Man_t * pAig, Cec_ParChc_t * pPars );
/*=== cecCorr.c ==========================================================*/
+extern int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars );
extern Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars );
/*=== cecCore.c ==========================================================*/
extern void Cec_ManSatSetDefaultParams( Cec_ParSat_t * p );
@@ -180,12 +208,20 @@ extern Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars
extern Gia_Man_t * Cec_ManSatSolving( Gia_Man_t * pAig, Cec_ParSat_t * pPars );
extern void Cec_ManSimulation( Gia_Man_t * pAig, Cec_ParSim_t * pPars );
/*=== cecSeq.c ==========================================================*/
-extern int Cec_ManSeqResimulateCounter( Gia_Man_t * pAig, Cec_ParSim_t * pPars, Gia_Cex_t * pCex );
+extern int Cec_ManSeqResimulateCounter( Gia_Man_t * pAig, Cec_ParSim_t * pPars, Abc_Cex_t * pCex );
extern int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars );
+extern int Cec_ManCheckNonTrivialCands( Gia_Man_t * pAig );
+/*=== cecSynth.c ==========================================================*/
+extern int Cec_SeqReadMinDomSize( Cec_ParSeq_t * p );
+extern int Cec_SeqReadVerbose( Cec_ParSeq_t * p );
+extern void Cec_SeqSynthesisSetDefaultParams( Cec_ParSeq_t * pPars );
+extern int Cec_SequentialSynthesisPart( Gia_Man_t * p, Cec_ParSeq_t * pPars );
+
+
+
+ABC_NAMESPACE_HEADER_END
+
-#ifdef __cplusplus
-}
-#endif
#endif
diff --git a/src/aig/cec/cecCec.c b/src/aig/cec/cecCec.c
index 1efa9235..0859a9ad 100644
--- a/src/aig/cec/cecCec.c
+++ b/src/aig/cec/cecCec.c
@@ -19,8 +19,12 @@
***********************************************************************/
#include "cecInt.h"
+#include "fra.h"
#include "giaAig.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -44,8 +48,8 @@ void Cec_ManTransformPattern( Gia_Man_t * p, int iOut, int * pValues )
{
int i;
assert( p->pCexComb == NULL );
- p->pCexComb = (Gia_Cex_t *)ABC_CALLOC( char,
- sizeof(Gia_Cex_t) + sizeof(unsigned) * Gia_BitWordNum(Gia_ManCiNum(p)) );
+ p->pCexComb = (Abc_Cex_t *)ABC_CALLOC( char,
+ sizeof(Abc_Cex_t) + sizeof(unsigned) * Gia_BitWordNum(Gia_ManCiNum(p)) );
p->pCexComb->iPo = iOut;
p->pCexComb->nPis = Gia_ManCiNum(p);
p->pCexComb->nBits = Gia_ManCiNum(p);
@@ -65,45 +69,53 @@ void Cec_ManTransformPattern( Gia_Man_t * p, int iOut, int * pValues )
SeeAlso []
***********************************************************************/
-int Cec_ManVerifyOld( Gia_Man_t * pMiter, int fVerbose )
+int Cec_ManVerifyOld( Gia_Man_t * pMiter, int fVerbose, int * piOutFail )
{
- extern int Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose );
+// extern int Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose );
extern int Ssw_SecCexResimulate( Aig_Man_t * p, int * pModel, int * pnOutputs );
Gia_Man_t * pTemp = Gia_ManTransformMiter( pMiter );
Aig_Man_t * pMiterCec = Gia_ManToAig( pTemp, 0 );
int RetValue, iOut, nOuts, clkTotal = clock();
+ if ( piOutFail )
+ *piOutFail = -1;
Gia_ManStop( pTemp );
// run CEC on this miter
- RetValue = Fra_FraigCec( &pMiterCec, 100000, fVerbose );
+ RetValue = Fra_FraigCec( &pMiterCec, 10000000, fVerbose );
// report the miter
if ( RetValue == 1 )
{
- printf( "Networks are equivalent. " );
-ABC_PRT( "Time", clock() - clkTotal );
+ Abc_Print( 1, "Networks are equivalent. " );
+Abc_PrintTime( 1, "Time", clock() - clkTotal );
}
else if ( RetValue == 0 )
{
- printf( "Networks are NOT EQUIVALENT. " );
-ABC_PRT( "Time", clock() - clkTotal );
+ Abc_Print( 1, "Networks are NOT EQUIVALENT. " );
+Abc_PrintTime( 1, "Time", clock() - clkTotal );
if ( pMiterCec->pData == NULL )
- printf( "Counter-example is not available.\n" );
+ Abc_Print( 1, "Counter-example is not available.\n" );
else
{
- iOut = Ssw_SecCexResimulate( pMiterCec, pMiterCec->pData, &nOuts );
+ iOut = Ssw_SecCexResimulate( pMiterCec, (int *)pMiterCec->pData, &nOuts );
if ( iOut == -1 )
- printf( "Counter-example verification has failed.\n" );
+ Abc_Print( 1, "Counter-example verification has failed.\n" );
else
{
- printf( "Primary output %d has failed in frame %d.\n", iOut );
- printf( "The counter-example detected %d incorrect outputs.\n", nOuts );
+// Aig_Obj_t * pObj = Aig_ManPo(pMiterCec, iOut);
+// Aig_Obj_t * pFan = Aig_ObjFanin0(pObj);
+ Abc_Print( 1, "Primary output %d has failed", iOut );
+ if ( nOuts-1 >= 0 )
+ Abc_Print( 1, ", along with other %d incorrect outputs", nOuts-1 );
+ Abc_Print( 1, ".\n" );
+ if ( piOutFail )
+ *piOutFail = iOut;
}
- Cec_ManTransformPattern( pMiter, iOut, pMiterCec->pData );
+ Cec_ManTransformPattern( pMiter, iOut, (int *)pMiterCec->pData );
}
}
else
{
- printf( "Networks are UNDECIDED. " );
-ABC_PRT( "Time", clock() - clkTotal );
+ Abc_Print( 1, "Networks are UNDECIDED. " );
+Abc_PrintTime( 1, "Time", clock() - clkTotal );
}
fflush( stdout );
Aig_ManStop( pMiterCec );
@@ -121,13 +133,18 @@ ABC_PRT( "Time", clock() - clkTotal );
SeeAlso []
***********************************************************************/
-int Cec_ManVerify( Gia_Man_t * p, Cec_ParCec_t * pPars )
+int Cec_ManVerify( Gia_Man_t * pInit, Cec_ParCec_t * pPars )
{
- int fDumpUndecided = 1;
+ int fDumpUndecided = 0;
Cec_ParFra_t ParsFra, * pParsFra = &ParsFra;
- Gia_Man_t * pNew;
+ Gia_Man_t * p, * pNew;
int RetValue, clk = clock();
double clkTotal = clock();
+ // preprocess
+ p = Gia_ManDup( pInit );
+ Gia_ManEquivFixOutputPairs( p );
+ p = Gia_ManCleanup( pNew = p );
+ Gia_ManStop( pNew );
// sweep for equivalences
Cec_ManFraSetDefaultParams( pParsFra );
pParsFra->nItersMax = 1000;
@@ -137,27 +154,60 @@ int Cec_ManVerify( Gia_Man_t * p, Cec_ParCec_t * pPars )
pParsFra->fCheckMiter = 1;
pParsFra->fDualOut = 1;
pNew = Cec_ManSatSweeping( p, pParsFra );
+ pPars->iOutFail = pParsFra->iOutFail;
+ // update
+ pInit->pCexComb = p->pCexComb; p->pCexComb = NULL;
+ Gia_ManStop( p );
+ p = pInit;
+ // continue
if ( pNew == NULL )
{
- if ( !Gia_ManVerifyCounterExample( p, p->pCexComb, 1 ) )
- printf( "Counter-example simulation has failed.\n" );
- printf( "Networks are NOT EQUIVALENT. " );
- ABC_PRT( "Time", clock() - clk );
- return 0;
+ if ( p->pCexComb != NULL )
+ {
+ if ( p->pCexComb && !Gia_ManVerifyCounterExample( p, p->pCexComb, 1 ) )
+ Abc_Print( 1, "Counter-example simulation has failed.\n" );
+ Abc_Print( 1, "Networks are NOT EQUIVALENT. " );
+ Abc_PrintTime( 1, "Time", clock() - clk );
+ return 0;
+ }
+ p = Gia_ManDup( pInit );
+ Gia_ManEquivFixOutputPairs( p );
+ p = Gia_ManCleanup( pNew = p );
+ Gia_ManStop( pNew );
+ pNew = p;
}
if ( Gia_ManAndNum(pNew) == 0 )
{
- printf( "Networks are equivalent. " );
- ABC_PRT( "Time", clock() - clk );
+ Gia_Obj_t * pObj1, * pObj2;
+ int i;
+ Gia_ManForEachPo( pNew, pObj1, i )
+ {
+ pObj2 = Gia_ManPo( pNew, ++i );
+ if ( Gia_ObjChild0(pObj1) != Gia_ObjChild0(pObj2) )
+ {
+ Abc_Print( 1, "Networks are NOT EQUIVALENT. Outputs %d trivially differ. ", i/2 );
+ Abc_PrintTime( 1, "Time", clock() - clk );
+ Gia_ManStop( pNew );
+ pPars->iOutFail = i/2;
+ return 0;
+ }
+ }
+ Abc_Print( 1, "Networks are equivalent. " );
+ Abc_PrintTime( 1, "Time", clock() - clk );
Gia_ManStop( pNew );
return 1;
}
- printf( "Networks are UNDECIDED after the new CEC engine. " );
- ABC_PRT( "Time", clock() - clk );
+ if ( pPars->fVerbose )
+ {
+ Abc_Print( 1, "Networks are UNDECIDED after the new CEC engine. " );
+ Abc_PrintTime( 1, "Time", clock() - clk );
+ }
if ( fDumpUndecided )
{
+ ABC_FREE( pNew->pReprs );
+ ABC_FREE( pNew->pNexts );
Gia_WriteAiger( pNew, "gia_cec_undecided.aig", 0, 0 );
- printf( "The result is written into file \"%s\".\n", "gia_cec_undecided.aig" );
+ Abc_Print( 1, "The result is written into file \"%s\".\n", "gia_cec_undecided.aig" );
}
if ( pPars->TimeLimit && ((double)clock() - clkTotal)/CLOCKS_PER_SEC >= pPars->TimeLimit )
{
@@ -165,12 +215,13 @@ int Cec_ManVerify( Gia_Man_t * p, Cec_ParCec_t * pPars )
return -1;
}
// call other solver
- printf( "Calling the old CEC engine.\n" );
+ if ( pPars->fVerbose )
+ Abc_Print( 1, "Calling the old CEC engine.\n" );
fflush( stdout );
- RetValue = Cec_ManVerifyOld( pNew, pPars->fVerbose );
+ RetValue = Cec_ManVerifyOld( pNew, pPars->fVerbose, &pPars->iOutFail );
p->pCexComb = pNew->pCexComb; pNew->pCexComb = NULL;
if ( p->pCexComb && !Gia_ManVerifyCounterExample( p, p->pCexComb, 1 ) )
- printf( "Counter-example simulation has failed.\n" );
+ Abc_Print( 1, "Counter-example simulation has failed.\n" );
Gia_ManStop( pNew );
return RetValue;
}
@@ -208,7 +259,7 @@ int Cec_ManVerifyTwo( Gia_Man_t * p0, Gia_Man_t * p1, int fVerbose )
Description [Returns 1 if equivalent, 0 if counter-example, -1 if undecided.
Counter-example is returned in the first manager as pAig0->pSeqModel.
- The format is given in Gia_Cex_t (file "abc\src\aig\gia\gia.h").]
+ The format is given in Abc_Cex_t (file "abc\src\aig\gia\gia.h").]
SideEffects []
@@ -248,7 +299,6 @@ int Cec_ManVerifyTwoAigs( Aig_Man_t * pAig0, Aig_Man_t * pAig1, int fVerbose )
***********************************************************************/
Aig_Man_t * Cec_LatchCorrespondence( Aig_Man_t * pAig, int nConfs, int fUseCSat )
{
- extern int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars );
Gia_Man_t * pGia;
Cec_ParCor_t CorPars, * pCorPars = &CorPars;
Cec_ManCorSetDefaultParams( pCorPars );
@@ -275,7 +325,6 @@ Aig_Man_t * Cec_LatchCorrespondence( Aig_Man_t * pAig, int nConfs, int fUseCSat
***********************************************************************/
Aig_Man_t * Cec_SignalCorrespondence( Aig_Man_t * pAig, int nConfs, int fUseCSat )
{
- extern int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars );
Gia_Man_t * pGia;
Cec_ParCor_t CorPars, * pCorPars = &CorPars;
Cec_ManCorSetDefaultParams( pCorPars );
@@ -304,6 +353,7 @@ Aig_Man_t * Cec_FraigCombinational( Aig_Man_t * pAig, int nConfs, int fVerbose )
Gia_Man_t * pGia;
Cec_ParFra_t FraPars, * pFraPars = &FraPars;
Cec_ManFraSetDefaultParams( pFraPars );
+ pFraPars->fSatSweeping = 1;
pFraPars->nBTLimit = nConfs;
pFraPars->nItersMax = 20;
pFraPars->fVerbose = fVerbose;
@@ -319,3 +369,5 @@ Aig_Man_t * Cec_FraigCombinational( Aig_Man_t * pAig, int nConfs, int fVerbose )
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/cec/cecChoice.c b/src/aig/cec/cecChoice.c
index fc316f46..076b34a2 100644
--- a/src/aig/cec/cecChoice.c
+++ b/src/aig/cec/cecChoice.c
@@ -22,6 +22,9 @@
#include "giaAig.h"
#include "dch.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -175,9 +178,9 @@ Gia_Man_t * Cec_ManCombSpecReduce( Gia_Man_t * p, Vec_Int_t ** pvOutputs, int fR
Gia_ManAppendCo( pNew, iObjNew );
Vec_IntFree( vXorLits );
Gia_ManHashStop( pNew );
-//printf( "Before sweeping = %d\n", Gia_ManAndNum(pNew) );
+//Abc_Print( 1, "Before sweeping = %d\n", Gia_ManAndNum(pNew) );
pNew = Gia_ManCleanup( pTemp = pNew );
-//printf( "After sweeping = %d\n", Gia_ManAndNum(pNew) );
+//Abc_Print( 1, "After sweeping = %d\n", Gia_ManAndNum(pNew) );
Gia_ManStop( pTemp );
return pNew;
}
@@ -219,7 +222,7 @@ int Cec_ManChoiceComputation_int( Gia_Man_t * pAig, Cec_ParChc_t * pPars )
pParsSim->fSeqSimulate = 0;
// create equivalence classes of registers
pSim = Cec_ManSimStart( pAig, pParsSim );
- Cec_ManSimClassesPrepare( pSim );
+ Cec_ManSimClassesPrepare( pSim, -1 );
Cec_ManSimClassesRefine( pSim );
// prepare SAT solving
Cec_ManSatSetDefaultParams( pParsSat );
@@ -227,7 +230,7 @@ int Cec_ManChoiceComputation_int( Gia_Man_t * pAig, Cec_ParChc_t * pPars )
pParsSat->fVerbose = pPars->fVerbose;
if ( pPars->fVerbose )
{
- printf( "Obj = %7d. And = %7d. Conf = %5d. Ring = %d. CSat = %d.\n",
+ Abc_Print( 1, "Obj = %7d. And = %7d. Conf = %5d. Ring = %d. CSat = %d.\n",
Gia_ManObjNum(pAig), Gia_ManAndNum(pAig), pPars->nBTLimit, pPars->fUseRings, pPars->fUseCSat );
Cec_ManRefinedClassPrintStats( pAig, NULL, 0, clock() - clk );
}
@@ -280,97 +283,23 @@ int Cec_ManChoiceComputation_int( Gia_Man_t * pAig, Cec_ParChc_t * pPars )
}
// check the overflow
if ( r == nItersMax )
- printf( "The refinement was not finished. The result may be incorrect.\n" );
+ Abc_Print( 1, "The refinement was not finished. The result may be incorrect.\n" );
Cec_ManSimStop( pSim );
clkTotal = clock() - clkTotal;
// report the results
if ( pPars->fVerbose )
{
- ABC_PRTP( "Srm ", clkSrm, clkTotal );
- ABC_PRTP( "Sat ", clkSat, clkTotal );
- ABC_PRTP( "Sim ", clkSim, clkTotal );
- ABC_PRTP( "Other", clkTotal-clkSat-clkSrm-clkSim, clkTotal );
- ABC_PRT( "TOTAL", clkTotal );
+ Abc_PrintTimeP( 1, "Srm ", clkSrm, clkTotal );
+ Abc_PrintTimeP( 1, "Sat ", clkSat, clkTotal );
+ Abc_PrintTimeP( 1, "Sim ", clkSim, clkTotal );
+ Abc_PrintTimeP( 1, "Other", clkTotal-clkSat-clkSrm-clkSim, clkTotal );
+ Abc_PrintTime( 1, "TOTAL", clkTotal );
}
return 0;
}
/**Function*************************************************************
- Synopsis [Duplicates the AIG in the DFS order.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Gia_ManChoiceMiter_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
-{
- if ( ~pObj->Value )
- return pObj->Value;
- Gia_ManChoiceMiter_rec( pNew, p, Gia_ObjFanin0(pObj) );
- if ( Gia_ObjIsCo(pObj) )
- return pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
- Gia_ManChoiceMiter_rec( pNew, p, Gia_ObjFanin1(pObj) );
- return pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
-}
-
-/**Function*************************************************************
-
- Synopsis [Derives the miter of several AIGs for choice computation.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Gia_Man_t * Gia_ManChoiceMiter( Vec_Ptr_t * vGias )
-{
- Gia_Man_t * pNew, * pGia, * pGia0;
- int i, k, iNode, nNodes;
- // make sure they have equal parameters
- assert( Vec_PtrSize(vGias) > 0 );
- pGia0 = Vec_PtrEntry( vGias, 0 );
- Vec_PtrForEachEntry( vGias, pGia, i )
- {
- assert( Gia_ManCiNum(pGia) == Gia_ManCiNum(pGia0) );
- assert( Gia_ManCoNum(pGia) == Gia_ManCoNum(pGia0) );
- assert( Gia_ManRegNum(pGia) == Gia_ManRegNum(pGia0) );
- Gia_ManFillValue( pGia );
- Gia_ManConst0(pGia)->Value = 0;
- }
- // start the new manager
- pNew = Gia_ManStart( Vec_PtrSize(vGias) * Gia_ManObjNum(pGia0) );
- pNew->pName = Gia_UtilStrsav( pGia0->pName );
- // create new CIs and assign them to the old manager CIs
- for ( k = 0; k < Gia_ManCiNum(pGia0); k++ )
- {
- iNode = Gia_ManAppendCi(pNew);
- Vec_PtrForEachEntry( vGias, pGia, i )
- Gia_ManCi( pGia, k )->Value = iNode;
- }
- // create internal nodes
- Gia_ManHashAlloc( pNew );
- for ( k = 0; k < Gia_ManCoNum(pGia0); k++ )
- {
- Vec_PtrForEachEntry( vGias, pGia, i )
- Gia_ManChoiceMiter_rec( pNew, pGia, Gia_ManCo( pGia, k ) );
- }
- Gia_ManHashStop( pNew );
- // check the presence of dangling nodes
- nNodes = Gia_ManHasDandling( pNew );
- assert( nNodes == 0 );
- // finalize
-// Gia_ManSetRegNum( pNew, Gia_ManRegNum(pGia0) );
- return pNew;
-}
-
-/**Function*************************************************************
-
Synopsis [Computes choices for the vector of AIGs.]
Description []
@@ -386,6 +315,7 @@ Gia_Man_t * Cec_ManChoiceComputationVec( Gia_Man_t * pGia, int nGias, Cec_ParChc
int RetValue;
// compute equivalences of the miter
// pMiter = Gia_ManChoiceMiter( vGias );
+// Gia_ManSetRegNum( pMiter, 0 );
RetValue = Cec_ManChoiceComputation_int( pGia, pPars );
// derive AIG with choices
pNew = Gia_ManEquivToChoices( pGia, nGias );
@@ -394,7 +324,7 @@ Gia_Man_t * Cec_ManChoiceComputationVec( Gia_Man_t * pGia, int nGias, Cec_ParChc
// report the results
if ( pPars->fVerbose )
{
-// printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n",
+// Abc_Print( 1, "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n",
// Gia_ManAndNum(pAig), Gia_ManAndNum(pNew),
// 100.0*(Gia_ManAndNum(pAig)-Gia_ManAndNum(pNew))/(Gia_ManAndNum(pAig)?Gia_ManAndNum(pAig):1),
// Gia_ManRegNum(pAig), Gia_ManRegNum(pNew),
@@ -416,7 +346,7 @@ Gia_Man_t * Cec_ManChoiceComputationVec( Gia_Man_t * pGia, int nGias, Cec_ParChc
***********************************************************************/
Gia_Man_t * Cec_ManChoiceComputation( Gia_Man_t * pAig, Cec_ParChc_t * pParsChc )
{
- extern Aig_Man_t * Dar_ManChoiceNew( Aig_Man_t * pAig, Dch_Pars_t * pPars );
+// extern Aig_Man_t * Dar_ManChoiceNew( Aig_Man_t * pAig, Dch_Pars_t * pPars );
Dch_Pars_t Pars, * pPars = &Pars;
Aig_Man_t * pMan, * pManNew;
Gia_Man_t * pGia;
@@ -456,7 +386,7 @@ Aig_Man_t * Cec_ComputeChoices( Gia_Man_t * pGia, Dch_Pars_t * pPars )
Cec_ParChc_t ParsChc, * pParsChc = &ParsChc;
Aig_Man_t * pAig;
if ( pPars->fVerbose )
- ABC_PRT( "Synthesis time", pPars->timeSynth );
+ Abc_PrintTime( 1, "Synthesis time", pPars->timeSynth );
Cec_ManChcSetDefaultParams( pParsChc );
pParsChc->nBTLimit = pPars->nBTLimit;
pParsChc->fUseCSat = pPars->fUseCSat;
@@ -475,3 +405,5 @@ Aig_Man_t * Cec_ComputeChoices( Gia_Man_t * pGia, Dch_Pars_t * pPars )
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/cec/cecClass.c b/src/aig/cec/cecClass.c
index 749f7f71..95414851 100644
--- a/src/aig/cec/cecClass.c
+++ b/src/aig/cec/cecClass.c
@@ -20,6 +20,9 @@
#include "cecInt.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -375,7 +378,7 @@ int Cec_ManSimHashKey( unsigned * pSim, int nWords, int nTableSize )
void Cec_ManSimMemRelink( Cec_ManSim_t * p )
{
unsigned * pPlace, Ent;
- pPlace = &p->MemFree;
+ pPlace = (unsigned *)&p->MemFree;
for ( Ent = p->nMems * (p->nWords + 1);
Ent + p->nWords + 1 < (unsigned)p->nWordsAlloc;
Ent += p->nWords + 1 )
@@ -518,14 +521,14 @@ void Cec_ManSimSavePattern( Cec_ManSim_t * p, int iPat )
int i;
assert( p->pCexComb == NULL );
assert( iPat >= 0 && iPat < 32 * p->nWords );
- p->pCexComb = (Gia_Cex_t *)ABC_CALLOC( char,
- sizeof(Gia_Cex_t) + sizeof(unsigned) * Gia_BitWordNum(Gia_ManCiNum(p->pAig)) );
+ p->pCexComb = (Abc_Cex_t *)ABC_CALLOC( char,
+ sizeof(Abc_Cex_t) + sizeof(unsigned) * Gia_BitWordNum(Gia_ManCiNum(p->pAig)) );
p->pCexComb->iPo = p->iOut;
p->pCexComb->nPis = Gia_ManCiNum(p->pAig);
p->pCexComb->nBits = Gia_ManCiNum(p->pAig);
for ( i = 0; i < Gia_ManCiNum(p->pAig); i++ )
{
- pInfo = Vec_PtrEntry( p->vCiSimInfo, i );
+ pInfo = (unsigned *)Vec_PtrEntry( p->vCiSimInfo, i );
if ( Gia_InfoHasBit( pInfo, iPat ) )
Gia_InfoSetBit( p->pCexComb->pData, i );
}
@@ -559,7 +562,7 @@ void Cec_ManSimFindBestPattern( Cec_ManSim_t * p )
assert( p->pBestState->nRegs == Gia_ManRegNum(p->pAig) );
for ( i = 0; i < Gia_ManRegNum(p->pAig); i++ )
{
- pInfo = Vec_PtrEntry( p->vCiSimInfo, Gia_ManPiNum(p->pAig) + i );
+ pInfo = (unsigned *)Vec_PtrEntry( p->vCiSimInfo, Gia_ManPiNum(p->pAig) + i );
if ( Gia_InfoHasBit(p->pBestState->pData, i) != Gia_InfoHasBit(pInfo, iPatBest) )
Gia_InfoXorBit( p->pBestState->pData, i );
}
@@ -591,8 +594,8 @@ int Cec_ManSimAnalyzeOutputs( Cec_ManSim_t * p )
assert( (Gia_ManPoNum(p->pAig) & 1) == 0 );
for ( i = 0; i < Gia_ManPoNum(p->pAig); i++ )
{
- pInfo = Vec_PtrEntry( p->vCoSimInfo, i );
- pInfo2 = Vec_PtrEntry( p->vCoSimInfo, ++i );
+ pInfo = (unsigned *)Vec_PtrEntry( p->vCoSimInfo, i );
+ pInfo2 = (unsigned *)Vec_PtrEntry( p->vCoSimInfo, ++i );
if ( !Cec_ManSimCompareEqual( pInfo, pInfo2, p->nWords ) )
{
if ( p->iOut == -1 )
@@ -614,7 +617,7 @@ int Cec_ManSimAnalyzeOutputs( Cec_ManSim_t * p )
{
for ( i = 0; i < Gia_ManPoNum(p->pAig); i++ )
{
- pInfo = Vec_PtrEntry( p->vCoSimInfo, i );
+ pInfo = (unsigned *)Vec_PtrEntry( p->vCoSimInfo, i );
if ( !Cec_ManSimCompareConst( pInfo, p->nWords ) )
{
if ( p->iOut == -1 )
@@ -679,7 +682,7 @@ int Cec_ManSimSimulateRound( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t *
pRes = Cec_ManSimSimRef( p, i );
if ( vInfoCis )
{
- pRes0 = Vec_PtrEntry( vInfoCis, iCiId++ );
+ pRes0 = (unsigned *)Vec_PtrEntry( vInfoCis, iCiId++ );
for ( w = 1; w <= p->nWords; w++ )
pRes[w] = pRes0[w-1];
}
@@ -697,7 +700,7 @@ int Cec_ManSimSimulateRound( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t *
pRes0 = Cec_ManSimSimDeref( p, Gia_ObjFaninId0(pObj,i) );
if ( vInfoCos )
{
- pRes = Vec_PtrEntry( vInfoCos, iCoId++ );
+ pRes = (unsigned *)Vec_PtrEntry( vInfoCos, iCoId++ );
if ( Gia_ObjFaninC0(pObj) )
for ( w = 1; w <= p->nWords; w++ )
pRes[w-1] = ~pRes0[w];
@@ -712,7 +715,7 @@ int Cec_ManSimSimulateRound( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t *
pRes0 = Cec_ManSimSimDeref( p, Gia_ObjFaninId0(pObj,i) );
pRes1 = Cec_ManSimSimDeref( p, Gia_ObjFaninId1(pObj,i) );
-// printf( "%d,%d ", Gia_ObjValue( Gia_ObjFanin0(pObj) ), Gia_ObjValue( Gia_ObjFanin1(pObj) ) );
+// Abc_Print( 1, "%d,%d ", Gia_ObjValue( Gia_ObjFanin0(pObj) ), Gia_ObjValue( Gia_ObjFanin1(pObj) ) );
if ( Gia_ObjFaninC0(pObj) )
{
@@ -762,7 +765,7 @@ references:
assert( vInfoCos == NULL || iCoId == Gia_ManCoNum(p->pAig) );
assert( p->nMems == 1 );
if ( p->nMems != 1 )
- printf( "Cec_ManSimSimulateRound(): Memory management error!\n" );
+ Abc_Print( 1, "Cec_ManSimSimulateRound(): Memory management error!\n" );
if ( p->pPars->fVeryVerbose )
Gia_ManEquivPrintClasses( p->pAig, 0, Cec_MemUsage(p) );
if ( p->pBestState )
@@ -800,14 +803,14 @@ void Cec_ManSimCreateInfo( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t * v
assert( vInfoCis && vInfoCos );
for ( i = 0; i < Gia_ManPiNum(p->pAig); i++ )
{
- pRes0 = Vec_PtrEntry( vInfoCis, i );
+ pRes0 = (unsigned *)Vec_PtrEntry( vInfoCis, i );
for ( w = 0; w < p->nWords; w++ )
pRes0[w] = Gia_ManRandom( 0 );
}
for ( i = 0; i < Gia_ManRegNum(p->pAig); i++ )
{
- pRes0 = Vec_PtrEntry( vInfoCis, Gia_ManPiNum(p->pAig) + i );
- pRes1 = Vec_PtrEntry( vInfoCos, Gia_ManPoNum(p->pAig) + i );
+ pRes0 = (unsigned *)Vec_PtrEntry( vInfoCis, Gia_ManPiNum(p->pAig) + i );
+ pRes1 = (unsigned *)Vec_PtrEntry( vInfoCos, Gia_ManPoNum(p->pAig) + i );
for ( w = 0; w < p->nWords; w++ )
pRes0[w] = pRes1[w];
}
@@ -816,7 +819,7 @@ void Cec_ManSimCreateInfo( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t * v
{
for ( i = 0; i < Gia_ManCiNum(p->pAig); i++ )
{
- pRes0 = Vec_PtrEntry( vInfoCis, i );
+ pRes0 = (unsigned *)Vec_PtrEntry( vInfoCis, i );
for ( w = 0; w < p->nWords; w++ )
pRes0[w] = Gia_ManRandom( 0 );
}
@@ -834,7 +837,7 @@ void Cec_ManSimCreateInfo( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t * v
SeeAlso []
***********************************************************************/
-int Cec_ManSimClassesPrepare( Cec_ManSim_t * p )
+int Cec_ManSimClassesPrepare( Cec_ManSim_t * p, int LevelMax )
{
Gia_Obj_t * pObj;
int i;
@@ -848,9 +851,16 @@ int Cec_ManSimClassesPrepare( Cec_ManSim_t * p )
if ( p->pPars->fLatchCorr )
Gia_ManForEachObj( p->pAig, pObj, i )
Gia_ObjSetRepr( p->pAig, i, GIA_VOID );
- else
+ else if ( LevelMax == -1 )
Gia_ManForEachObj( p->pAig, pObj, i )
Gia_ObjSetRepr( p->pAig, i, Gia_ObjIsAnd(pObj) ? 0 : GIA_VOID );
+ else
+ {
+ Gia_ManLevelNum( p->pAig );
+ Gia_ManForEachObj( p->pAig, pObj, i )
+ Gia_ObjSetRepr( p->pAig, i, (Gia_ObjIsAnd(pObj) && Gia_ObjLevel(p->pAig,pObj) <= LevelMax) ? 0 : GIA_VOID );
+ Vec_IntFreeP( &p->pAig->vLevels );
+ }
// if sequential simulation, set starting representative of ROs to be constant 0
if ( p->pPars->fSeqSimulate )
Gia_ManForEachRo( p->pAig, pObj, i )
@@ -906,3 +916,5 @@ int Cec_ManSimClassesRefine( Cec_ManSim_t * p )
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/cec/cecCore.c b/src/aig/cec/cecCore.c
index 10c145ec..5e71dbff 100644
--- a/src/aig/cec/cecCore.c
+++ b/src/aig/cec/cecCore.c
@@ -20,6 +20,9 @@
#include "cecInt.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -133,8 +136,10 @@ void Cec_ManFraSetDefaultParams( Cec_ParFra_t * p )
// p->fFirstStop = 0; // stop on the first sat output
p->fDualOut = 0; // miter with separate outputs
p->fColorDiff = 0; // miter with separate outputs
+ p->fSatSweeping = 0; // enable SAT sweeping
p->fVeryVerbose = 0; // verbose stats
p->fVerbose = 0; // verbose stats
+ p->iOutFail = -1; // the failed output
}
/**Function*************************************************************
@@ -158,6 +163,7 @@ void Cec_ManCecSetDefaultParams( Cec_ParCec_t * p )
p->fRewriting = 0; // enables AIG rewriting
p->fVeryVerbose = 0; // verbose stats
p->fVerbose = 0; // verbose stats
+ p->iOutFail = -1; // the number of failed output
}
/**Function*************************************************************
@@ -178,6 +184,8 @@ void Cec_ManCorSetDefaultParams( Cec_ParCor_t * p )
p->nRounds = 15; // the number of simulation rounds
p->nFrames = 1; // the number of time frames
p->nBTLimit = 100; // conflict limit at a node
+ p->nLevelMax = -1; // (scorr only) the max number of levels
+ p->nStepsMax = -1; // (scorr only) the max number of induction steps
p->fLatchCorr = 0; // consider only latch outputs
p->fUseRings = 1; // combine classes into rings
p->fUseCSat = 1; // use circuit-based solver
@@ -249,12 +257,12 @@ int Cec_ManSimulationOne( Gia_Man_t * pAig, Cec_ParSim_t * pPars )
Cec_ManSim_t * pSim;
int RetValue = 0, clkTotal = clock();
pSim = Cec_ManSimStart( pAig, pPars );
- if ( (pAig->pReprs == NULL && (RetValue = Cec_ManSimClassesPrepare( pSim ))) ||
+ if ( (pAig->pReprs == NULL && (RetValue = Cec_ManSimClassesPrepare( pSim, -1 ))) ||
(RetValue == 0 && (RetValue = Cec_ManSimClassesRefine( pSim ))) )
- printf( "The number of failed outputs of the miter = %6d. (Words = %4d. Frames = %4d.)\n",
+ Abc_Print( 1, "The number of failed outputs of the miter = %6d. (Words = %4d. Frames = %4d.)\n",
pSim->nOuts, pPars->nWords, pPars->nFrames );
if ( pPars->fVerbose )
- ABC_PRT( "Time", clock() - clkTotal );
+ Abc_PrintTime( 1, "Time", clock() - clkTotal );
Cec_ManSimStop( pSim );
return RetValue;
}
@@ -275,7 +283,7 @@ void Cec_ManSimulation( Gia_Man_t * pAig, Cec_ParSim_t * pPars )
int r, nLitsOld, nLitsNew, nCountNoRef = 0, fStop = 0;
Gia_ManRandom( 1 );
if ( pPars->fSeqSimulate )
- printf( "Performing rounds of random simulation of %d frames with %d words.\n",
+ Abc_Print( 1, "Performing rounds of random simulation of %d frames with %d words.\n",
pPars->nRounds, pPars->nFrames, pPars->nWords );
nLitsOld = Gia_ManEquivCountLits( pAig );
for ( r = 0; r < pPars->nRounds; r++ )
@@ -301,14 +309,14 @@ void Cec_ManSimulation( Gia_Man_t * pAig, Cec_ParSim_t * pPars )
}
// if ( pPars->fVerbose )
if ( r == pPars->nRounds || fStop )
- printf( "Random simulation is stopped after %d rounds.\n", r );
+ Abc_Print( 1, "Random simulation is stopped after %d rounds.\n", r );
else
- printf( "Random simulation saturated after %d rounds.\n", r );
+ Abc_Print( 1, "Random simulation saturated after %d rounds.\n", r );
if ( pPars->fCheckMiter )
{
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 );
}
}
@@ -366,7 +374,7 @@ Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars )
clk = clock();
if ( p->pAig->pReprs == NULL )
{
- if ( Cec_ManSimClassesPrepare(pSim) || Cec_ManSimClassesRefine(pSim) )
+ if ( Cec_ManSimClassesPrepare(pSim, -1) || Cec_ManSimClassesRefine(pSim) )
{
Gia_ManStop( p->pAig );
p->pAig = NULL;
@@ -395,19 +403,19 @@ p->timeSim += clock() - clk;
{
Gia_ManStop( pSrm );
if ( p->pPars->fVerbose )
- printf( "Considered all available candidate equivalences.\n" );
+ Abc_Print( 1, "Considered all available candidate equivalences.\n" );
if ( pPars->fDualOut && Gia_ManAndNum(p->pAig) > 0 )
{
if ( pPars->fColorDiff )
{
if ( p->pPars->fVerbose )
- printf( "Switching into reduced mode.\n" );
+ Abc_Print( 1, "Switching into reduced mode.\n" );
pPars->fColorDiff = 0;
}
else
{
if ( p->pPars->fVerbose )
- printf( "Switching into normal mode.\n" );
+ Abc_Print( 1, "Switching into normal mode.\n" );
pPars->fDualOut = 0;
}
continue;
@@ -433,14 +441,14 @@ p->timeSat += clock() - clk;
break;
if ( p->pPars->fVerbose )
{
- printf( "%3d : P =%7d. D =%7d. F =%6d. M = %7d. And =%8d. ",
+ Abc_Print( 1, "%3d : P =%7d. D =%7d. F =%6d. M = %7d. And =%8d. ",
i, p->nAllProved, p->nAllDisproved, p->nAllFailed, nMatches, Gia_ManAndNum(p->pAig) );
- ABC_PRT( "Time", clock() - clk2 );
+ Abc_PrintTime( 1, "Time", clock() - clk2 );
}
if ( Gia_ManAndNum(p->pAig) == 0 )
{
if ( p->pPars->fVerbose )
- printf( "Network after reduction is empty.\n" );
+ Abc_Print( 1, "Network after reduction is empty.\n" );
break;
}
// check resource limits
@@ -454,54 +462,63 @@ p->timeSat += clock() - clk;
{
if ( pParsSat->nBTLimit >= 10001 )
break;
+ if ( pPars->fSatSweeping )
+ {
+ if ( p->pPars->fVerbose )
+ Abc_Print( 1, "Exceeded the limit on the number of conflicts (%d).\n", pParsSat->nBTLimit );
+ break;
+ }
pParsSat->nBTLimit *= 10;
if ( p->pPars->fVerbose )
{
if ( p->pPars->fVerbose )
- printf( "Increasing conflict limit to %d.\n", pParsSat->nBTLimit );
+ Abc_Print( 1, "Increasing conflict limit to %d.\n", pParsSat->nBTLimit );
if ( fOutputResult )
{
Gia_WriteAiger( p->pAig, "gia_cec_temp.aig", 0, 0 );
- printf("The result is written into file \"%s\".\n", "gia_cec_temp.aig" );
+ Abc_Print( 1,"The result is written into file \"%s\".\n", "gia_cec_temp.aig" );
}
}
}
if ( pPars->fDualOut && pPars->fColorDiff && (Gia_ManAndNum(p->pAig) < 100000 || p->nAllProved + p->nAllDisproved < 10) )
{
if ( p->pPars->fVerbose )
- printf( "Switching into reduced mode.\n" );
+ Abc_Print( 1, "Switching into reduced mode.\n" );
pPars->fColorDiff = 0;
}
// if ( pPars->fDualOut && Gia_ManAndNum(p->pAig) < 20000 )
else if ( pPars->fDualOut && (Gia_ManAndNum(p->pAig) < 20000 || p->nAllProved + p->nAllDisproved < 10) )
{
if ( p->pPars->fVerbose )
- printf( "Switching into normal mode.\n" );
+ Abc_Print( 1, "Switching into normal mode.\n" );
pPars->fColorDiff = 0;
pPars->fDualOut = 0;
}
}
finalize:
- if ( p->pPars->fVerbose )
+ if ( p->pPars->fVerbose && p->pAig )
{
- printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n",
+ Abc_Print( 1, "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n",
Gia_ManAndNum(pAig), Gia_ManAndNum(p->pAig),
100.0*(Gia_ManAndNum(pAig)-Gia_ManAndNum(p->pAig))/(Gia_ManAndNum(pAig)?Gia_ManAndNum(pAig):1),
Gia_ManRegNum(pAig), Gia_ManRegNum(p->pAig),
100.0*(Gia_ManRegNum(pAig)-Gia_ManRegNum(p->pAig))/(Gia_ManRegNum(pAig)?Gia_ManRegNum(pAig):1) );
- ABC_PRTP( "Sim ", p->timeSim, clock() - (int)clkTotal );
- ABC_PRTP( "Sat ", p->timeSat-pPat->timeTotalSave, clock() - (int)clkTotal );
- ABC_PRTP( "Pat ", p->timePat+pPat->timeTotalSave, clock() - (int)clkTotal );
- ABC_PRT( "Time", clock() - clkTotal );
+ Abc_PrintTimeP( 1, "Sim ", p->timeSim, clock() - (int)clkTotal );
+ Abc_PrintTimeP( 1, "Sat ", p->timeSat-pPat->timeTotalSave, clock() - (int)clkTotal );
+ Abc_PrintTimeP( 1, "Pat ", p->timePat+pPat->timeTotalSave, clock() - (int)clkTotal );
+ Abc_PrintTime( 1, "Time", (int)(clock() - clkTotal) );
}
pTemp = p->pAig; p->pAig = NULL;
if ( pTemp == NULL && pSim->iOut >= 0 )
- printf( "Disproved at least one output of the miter (zero-based number %d).\n", pSim->iOut );
+ {
+ Abc_Print( 1, "Disproved at least one output of the miter (zero-based number %d).\n", pSim->iOut );
+ pPars->iOutFail = pSim->iOut;
+ }
else if ( pSim->pCexes )
- printf( "Disproved %d outputs of the miter.\n", pSim->nOuts );
+ Abc_Print( 1, "Disproved %d outputs of the miter.\n", pSim->nOuts );
if ( fTimeOut )
- printf( "Timed out after %d seconds.\n", (int)((double)clock() - clkTotal)/CLOCKS_PER_SEC );
+ Abc_Print( 1, "Timed out after %d seconds.\n", (int)((double)clock() - clkTotal)/CLOCKS_PER_SEC );
pAig->pCexComb = pSim->pCexComb; pSim->pCexComb = NULL;
Cec_ManSimStop( pSim );
@@ -516,3 +533,5 @@ finalize:
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/cec/cecCorr.c b/src/aig/cec/cecCorr.c
index 52d2b80e..565ca47e 100644
--- a/src/aig/cec/cecCorr.c
+++ b/src/aig/cec/cecCorr.c
@@ -20,6 +20,9 @@
#include "cecInt.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -197,9 +200,9 @@ Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_I
Vec_IntFree( vXorLits );
Gia_ManHashStop( pNew );
ABC_FREE( p->pCopies );
-//printf( "Before sweeping = %d\n", Gia_ManAndNum(pNew) );
+//Abc_Print( 1, "Before sweeping = %d\n", Gia_ManAndNum(pNew) );
pNew = Gia_ManCleanup( pTemp = pNew );
-//printf( "After sweeping = %d\n", Gia_ManAndNum(pNew) );
+//Abc_Print( 1, "After sweeping = %d\n", Gia_ManAndNum(pNew) );
Gia_ManStop( pTemp );
return pNew;
}
@@ -266,9 +269,9 @@ Gia_Man_t * Gia_ManCorrSpecReduceInit( Gia_Man_t * p, int nFrames, int nPrefix,
Vec_IntFree( vXorLits );
Gia_ManHashStop( pNew );
ABC_FREE( p->pCopies );
-//printf( "Before sweeping = %d\n", Gia_ManAndNum(pNew) );
+//Abc_Print( 1, "Before sweeping = %d\n", Gia_ManAndNum(pNew) );
pNew = Gia_ManCleanup( pTemp = pNew );
-//printf( "After sweeping = %d\n", Gia_ManAndNum(pNew) );
+//Abc_Print( 1, "After sweeping = %d\n", Gia_ManAndNum(pNew) );
Gia_ManStop( pTemp );
return pNew;
}
@@ -292,13 +295,13 @@ void Cec_ManStartSimInfo( Vec_Ptr_t * vInfo, int nFlops )
assert( nFlops <= Vec_PtrSize(vInfo) );
for ( k = 0; k < nFlops; k++ )
{
- pInfo = Vec_PtrEntry( vInfo, k );
+ pInfo = (unsigned *)Vec_PtrEntry( vInfo, k );
for ( w = 0; w < nWords; w++ )
pInfo[w] = 0;
}
for ( k = nFlops; 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 );
}
@@ -327,20 +330,20 @@ void Gia_ManCorrRemapSimInfo( Gia_Man_t * p, Vec_Ptr_t * vInfo )
pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
if ( pRepr == NULL || Gia_ObjFailed(p, Gia_ObjId(p,pObj)) )
continue;
- pInfoObj = Vec_PtrEntry( vInfo, i );
+ pInfoObj = (unsigned *)Vec_PtrEntry( vInfo, i );
for ( w = 0; w < nWords; w++ )
assert( pInfoObj[w] == 0 );
// skip ROs with constant representatives
if ( Gia_ObjIsConst0(pRepr) )
continue;
assert( Gia_ObjIsRo(p, pRepr) );
-// printf( "%d -> %d ", i, Gia_ObjId(p, pRepr) );
+// Abc_Print( 1, "%d -> %d ", i, Gia_ObjId(p, pRepr) );
// transfer info from the representative
- pInfoRepr = Vec_PtrEntry( vInfo, Gia_ObjCioId(pRepr) - Gia_ManPiNum(p) );
+ pInfoRepr = (unsigned *)Vec_PtrEntry( vInfo, Gia_ObjCioId(pRepr) - Gia_ManPiNum(p) );
for ( w = 0; w < nWords; w++ )
pInfoObj[w] = pInfoRepr[w];
}
-// printf( "\n" );
+// Abc_Print( 1, "\n" );
}
/**Function*************************************************************
@@ -368,7 +371,7 @@ Vec_Int_t * Gia_ManCorrCreateRemapping( Gia_Man_t * p )
// if ( pRepr == NULL || Gia_ObjIsConst0(pRepr) || Gia_ObjIsFailedPair(p, Gia_ObjId(p, pRepr), Gia_ObjId(p, pObj)) )
continue;
assert( Gia_ObjIsRo(p, pRepr) );
-// printf( "%d -> %d ", Gia_ObjId(p,pObj), Gia_ObjId(p, pRepr) );
+// Abc_Print( 1, "%d -> %d ", Gia_ObjId(p,pObj), Gia_ObjId(p, pRepr) );
// remember the pair
Vec_IntPush( vPairs, Gia_ObjCioId(pRepr) - Gia_ManPiNum(p) );
Vec_IntPush( vPairs, i );
@@ -395,8 +398,8 @@ void Gia_ManCorrPerformRemapping( Vec_Int_t * vPairs, Vec_Ptr_t * vInfo )
Vec_IntForEachEntry( vPairs, iRepr, i )
{
iObj = Vec_IntEntry( vPairs, ++i );
- pInfoObj = Vec_PtrEntry( vInfo, iObj );
- pInfoRepr = Vec_PtrEntry( vInfo, iRepr );
+ pInfoObj = (unsigned *)Vec_PtrEntry( vInfo, iObj );
+ pInfoRepr = (unsigned *)Vec_PtrEntry( vInfo, iRepr );
for ( w = 0; w < nWords; w++ )
{
assert( pInfoObj[w] == 0 );
@@ -422,16 +425,16 @@ int Cec_ManLoadCounterExamplesTry( Vec_Ptr_t * vInfo, Vec_Ptr_t * vPres, int iBi
int i;
for ( i = 0; i < nLits; i++ )
{
- pInfo = Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i]));
- pPres = Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i]));
+ pInfo = (unsigned *)Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i]));
+ pPres = (unsigned *)Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i]));
if ( Gia_InfoHasBit( pPres, iBit ) &&
Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) )
return 0;
}
for ( i = 0; i < nLits; i++ )
{
- pInfo = Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i]));
- pPres = Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i]));
+ pInfo = (unsigned *)Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i]));
+ pPres = (unsigned *)Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i]));
Gia_InfoSetBit( pPres, iBit );
if ( Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) )
Gia_InfoXorBit( pInfo, iBit );
@@ -506,7 +509,7 @@ int Cec_ManLoadCounterExamples2( Vec_Ptr_t * vInfo, Vec_Int_t * vCexStore, int i
// skip the output number
// iStart++;
Out = Vec_IntEntry( vCexStore, iStart++ );
-// printf( "iBit = %d. Out = %d.\n", iBit, Out );
+// Abc_Print( 1, "iBit = %d. Out = %d.\n", iBit, Out );
// get the number of items
nLits = Vec_IntEntry( vCexStore, iStart++ );
if ( nLits <= 0 )
@@ -515,14 +518,14 @@ int Cec_ManLoadCounterExamples2( Vec_Ptr_t * vInfo, Vec_Int_t * vCexStore, int i
for ( k = 0; k < nLits; k++ )
{
iLit = Vec_IntEntry( vCexStore, iStart++ );
- pInfo = Vec_PtrEntry( vInfo, Gia_Lit2Var(iLit) );
+ pInfo = (unsigned *)Vec_PtrEntry( vInfo, Gia_Lit2Var(iLit) );
if ( Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(iLit) )
Gia_InfoXorBit( pInfo, iBit );
}
if ( ++iBit == nBits )
break;
}
-// printf( "added %d bits\n", iBit-1 );
+// Abc_Print( 1, "added %d bits\n", iBit-1 );
return iStart;
}
@@ -620,7 +623,7 @@ int Gia_ManCheckRefinements( Gia_Man_t * p, Vec_Str_t * vStatus, Vec_Int_t * vOu
if ( Gia_ObjHasSameRepr(p, iRepr, iObj) )
Counter++;
// if ( Gia_ObjHasSameRepr(p, iRepr, iObj) )
-// printf( "Gia_ManCheckRefinements(): Disproved equivalence (%d,%d) is not refined!\n", iRepr, iObj );
+// Abc_Print( 1, "Gia_ManCheckRefinements(): Disproved equivalence (%d,%d) is not refined!\n", iRepr, iObj );
// if ( Gia_ObjHasSameRepr(p, iRepr, iObj) )
// Cec_ManSimClassRemoveOne( pSim, iObj );
continue;
@@ -628,7 +631,7 @@ int Gia_ManCheckRefinements( Gia_Man_t * p, Vec_Str_t * vStatus, Vec_Int_t * vOu
if ( status == -1 )
{
// if ( !Gia_ObjFailed( p, iObj ) )
-// printf( "Gia_ManCheckRefinements(): Failed equivalence is not marked as failed!\n" );
+// Abc_Print( 1, "Gia_ManCheckRefinements(): Failed equivalence is not marked as failed!\n" );
// Gia_ObjSetFailed( p, iRepr );
// Gia_ObjSetFailed( p, iObj );
// if ( fRings )
@@ -638,7 +641,7 @@ int Gia_ManCheckRefinements( Gia_Man_t * p, Vec_Str_t * vStatus, Vec_Int_t * vOu
}
}
// if ( Counter )
-// printf( "Gia_ManCheckRefinements(): Could not refine %d nodes.\n", Counter );
+// Abc_Print( 1, "Gia_ManCheckRefinements(): Could not refine %d nodes.\n", Counter );
return 1;
}
@@ -732,10 +735,10 @@ void Cec_ManRefinedClassPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIte
CounterX -= Gia_ManCoNum(p);
nLits = Gia_ManCiNum(p) + Gia_ManAndNum(p) - Counter - CounterX;
if ( iIter == -1 )
- printf( "BMC : " );
+ Abc_Print( 1, "BMC : " );
else
- printf( "%3d : ", iIter );
- printf( "c =%8d cl =%7d lit =%8d ", Counter0, Counter, nLits );
+ Abc_Print( 1, "%3d : ", iIter );
+ Abc_Print( 1, "c =%8d cl =%7d lit =%8d ", Counter0, Counter, nLits );
if ( vStatus )
Vec_StrForEachEntry( vStatus, Entry, i )
{
@@ -746,8 +749,8 @@ void Cec_ManRefinedClassPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIte
else if ( Entry == -1 )
nFail++;
}
- printf( "p =%6d d =%6d f =%6d ", nProve, nDispr, nFail );
- ABC_PRT( "T", Time );
+ Abc_Print( 1, "p =%6d d =%6d f =%6d ", nProve, nDispr, nFail );
+ Abc_PrintTime( 1, "T", Time );
}
/**Function*************************************************************
@@ -833,7 +836,7 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
{
int nIterMax = 100000;
int nAddFrames = 1; // additional timeframes to simulate
- int fRunBmcFirst = 0;
+ int fRunBmcFirst = 1;
Vec_Str_t * vStatus;
Vec_Int_t * vOutputs;
Vec_Int_t * vCexStore;
@@ -846,7 +849,7 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
int clk2, clk = clock();
if ( Gia_ManRegNum(pAig) == 0 )
{
- printf( "Cec_ManLatchCorrespondence(): Not a sequential AIG.\n" );
+ Abc_Print( 1, "Cec_ManLatchCorrespondence(): Not a sequential AIG.\n" );
return 0;
}
Gia_ManRandom( 1 );
@@ -861,7 +864,7 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
pSim = Cec_ManSimStart( pAig, pParsSim );
if ( pAig->pReprs == NULL )
{
- Cec_ManSimClassesPrepare( pSim );
+ Cec_ManSimClassesPrepare( pSim, pPars->nLevelMax );
Cec_ManSimClassesRefine( pSim );
}
// prepare SAT solving
@@ -870,7 +873,7 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
pParsSat->fVerbose = pPars->fVerbose;
if ( pPars->fVerbose )
{
- printf( "Obj = %7d. And = %7d. Conf = %5d. Fr = %d. Lcorr = %d. Ring = %d. CSat = %d.\n",
+ Abc_Print( 1, "Obj = %7d. And = %7d. Conf = %5d. Fr = %d. Lcorr = %d. Ring = %d. CSat = %d.\n",
Gia_ManObjNum(pAig), Gia_ManAndNum(pAig),
pPars->nBTLimit, pPars->nFrames, pPars->fLatchCorr, pPars->fUseRings, pPars->fUseCSat );
Cec_ManRefinedClassPrintStats( pAig, NULL, 0, clock() - clk );
@@ -878,9 +881,26 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
// check the base case
if ( fRunBmcFirst && (!pPars->fLatchCorr || pPars->nFrames > 1) )
Cec_ManLSCorrespondenceBmc( pAig, pPars, 0 );
+ if ( pPars->pFunc )
+ {
+ ((int (*)(void *))pPars->pFunc)( pPars->pData );
+ ((int (*)(void *))pPars->pFunc)( pPars->pData );
+ }
+ if ( pPars->nStepsMax == 0 )
+ {
+ Abc_Print( 1, "Stopped signal correspondence after BMC.\n" );
+ Cec_ManSimStop( pSim );
+ return 1;
+ }
// perform refinement of equivalence classes
for ( r = 0; r < nIterMax; r++ )
{
+ if ( pPars->nStepsMax == r )
+ {
+ Cec_ManSimStop( pSim );
+ Abc_Print( 1, "Stopped signal correspondence after %d refiment iterations.\n", r );
+ return 1;
+ }
clk = clock();
// perform speculative reduction
clk2 = clock();
@@ -920,12 +940,14 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
Vec_StrFree( vStatus );
Vec_IntFree( vOutputs );
//Gia_ManEquivPrintClasses( pAig, 1, 0 );
+ if ( pPars->pFunc )
+ ((int (*)(void *))pPars->pFunc)( pPars->pData );
}
if ( pPars->fVerbose )
Cec_ManRefinedClassPrintStats( pAig, NULL, r+1, clock() - clk );
// check the overflow
if ( r == nIterMax )
- printf( "The refinement was not finished. The result may be incorrect.\n" );
+ Abc_Print( 1, "The refinement was not finished. The result may be incorrect.\n" );
Cec_ManSimStop( pSim );
// check the base case
if ( !fRunBmcFirst && (!pPars->fLatchCorr || pPars->nFrames > 1) )
@@ -938,9 +960,9 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
ABC_PRTP( "Sat ", clkSat, clkTotal );
ABC_PRTP( "Sim ", clkSim, clkTotal );
ABC_PRTP( "Other", clkTotal-clkSat-clkSrm-clkSim, clkTotal );
- ABC_PRT( "TOTAL", clkTotal );
+ Abc_PrintTime( 1, "TOTAL", clkTotal );
}
- return 0;
+ return 1;
}
/**Function*************************************************************
@@ -960,7 +982,7 @@ unsigned * Cec_ManComputeInitState( Gia_Man_t * pAig, int nFrames )
unsigned * pInitState;
int i, f;
Gia_ManRandom( 1 );
-// printf( "Simulating %d timeframes.\n", nFrames );
+// Abc_Print( 1, "Simulating %d timeframes.\n", nFrames );
Gia_ManForEachRo( pAig, pObj, i )
pObj->fMark1 = 0;
for ( f = 0; f < nFrames; f++ )
@@ -981,9 +1003,9 @@ unsigned * Cec_ManComputeInitState( Gia_Man_t * pAig, int nFrames )
{
if ( pObj->fMark1 )
Gia_InfoSetBit( pInitState, i );
-// printf( "%d", pObj->fMark1 );
+// Abc_Print( 1, "%d", pObj->fMark1 );
}
-// printf( "\n" );
+// Abc_Print( 1, "\n" );
Gia_ManCleanMark1( pAig );
return pInitState;
}
@@ -1007,15 +1029,15 @@ void Cec_ManPrintFlopEquivs( Gia_Man_t * p )
Gia_ManForEachRo( p, pObj, i )
{
if ( Gia_ObjIsConst(p, Gia_ObjId(p, pObj)) )
- printf( "Original flop %s is proved equivalent to constant.\n", Vec_PtrEntry(p->vNamesIn, Gia_ObjCioId(pObj)) );
+ Abc_Print( 1, "Original flop %s is proved equivalent to constant.\n", Vec_PtrEntry(p->vNamesIn, Gia_ObjCioId(pObj)) );
else if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
{
if ( Gia_ObjIsCi(pRepr) )
- printf( "Original flop %s is proved equivalent to flop %s.\n",
+ Abc_Print( 1, "Original flop %s is proved equivalent to flop %s.\n",
Vec_PtrEntry( p->vNamesIn, Gia_ObjCioId(pObj) ),
Vec_PtrEntry( p->vNamesIn, Gia_ObjCioId(pRepr) ) );
else
- printf( "Original flop %s is proved equivalent to internal node %d.\n",
+ Abc_Print( 1, "Original flop %s is proved equivalent to internal node %d.\n",
Vec_PtrEntry( p->vNamesIn, Gia_ObjCioId(pObj) ), Gia_ObjId(p, pRepr) );
}
}
@@ -1046,7 +1068,7 @@ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
{
// compute the cycles AIG
pInitState = Cec_ManComputeInitState( pAig, pPars->nPrefix );
- pTemp = Gia_ManDupFlip( pAig, pInitState );
+ pTemp = Gia_ManDupFlip( pAig, (int *)pInitState );
ABC_FREE( pInitState );
// compute classes of this AIG
RetValue = Cec_ManLSCorrespondenceClasses( pTemp, pPars );
@@ -1086,19 +1108,19 @@ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
// report the results
if ( pPars->fVerbose )
{
- printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n",
+ Abc_Print( 1, "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n",
Gia_ManAndNum(pAig), Gia_ManAndNum(pNew),
100.0*(Gia_ManAndNum(pAig)-Gia_ManAndNum(pNew))/(Gia_ManAndNum(pAig)?Gia_ManAndNum(pAig):1),
Gia_ManRegNum(pAig), Gia_ManRegNum(pNew),
100.0*(Gia_ManRegNum(pAig)-Gia_ManRegNum(pNew))/(Gia_ManRegNum(pAig)?Gia_ManRegNum(pAig):1) );
}
if ( pPars->nPrefix && (Gia_ManAndNum(pNew) < Gia_ManAndNum(pAig) || Gia_ManRegNum(pNew) < Gia_ManRegNum(pAig)) )
- printf( "The reduced AIG was produced using %d-th invariants and will not verify.\n", pPars->nPrefix );
+ Abc_Print( 1, "The reduced AIG was produced using %d-th invariants and will not verify.\n", pPars->nPrefix );
// print verbose info about equivalences
if ( pPars->fVerboseFlops )
{
if ( pAig->vNamesIn == NULL )
- printf( "Flop output names are not available. Use command \"&get -n\".\n" );
+ Abc_Print( 1, "Flop output names are not available. Use command \"&get -n\".\n" );
else
Cec_ManPrintFlopEquivs( pAig );
}
@@ -1110,3 +1132,5 @@ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/cec/cecCorr_updated.c b/src/aig/cec/cecCorr_updated.c
index dbe81d81..8ce1bd74 100644
--- a/src/aig/cec/cecCorr_updated.c
+++ b/src/aig/cec/cecCorr_updated.c
@@ -20,6 +20,9 @@
#include "cecInt.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -970,7 +973,7 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
ABC_PRTP( "Other", clkTotal-clkSat-clkSrm-clkSim, clkTotal );
ABC_PRT( "TOTAL", clkTotal );
}
- return 0;
+ return 1;
}
/**Function*************************************************************
@@ -1020,3 +1023,5 @@ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/cec/cecInt.h b/src/aig/cec/cecInt.h
index 73f108ba..6216eae2 100644
--- a/src/aig/cec/cecInt.h
+++ b/src/aig/cec/cecInt.h
@@ -21,6 +21,7 @@
#ifndef __CEC_INT_H__
#define __CEC_INT_H__
+
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
@@ -34,9 +35,10 @@
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
-#ifdef __cplusplus
-extern "C" {
-#endif
+
+
+ABC_NAMESPACE_HEADER_START
+
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
@@ -128,8 +130,8 @@ struct Cec_ManSim_t_
void ** pCexes; // counter-examples for each output
int iOut; // first failed output
int nOuts; // the number of failed outputs
- Gia_Cex_t * pCexComb; // counter-example for the first failed output
- Gia_Cex_t * pBestState; // the state that led to most of the refinements
+ Abc_Cex_t * pCexComb; // counter-example for the first failed output
+ Abc_Cex_t * pBestState; // the state that led to most of the refinements
// scoring simulation patterns
int * pScores; // counters of refinement for each pattern
// temporaries
@@ -170,7 +172,7 @@ struct Cec_ManFra_t_
extern void Cec_ManRefinedClassPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIter, int Time );
/*=== cecClass.c ============================================================*/
extern int Cec_ManSimClassRemoveOne( Cec_ManSim_t * p, int i );
-extern int Cec_ManSimClassesPrepare( Cec_ManSim_t * p );
+extern int Cec_ManSimClassesPrepare( Cec_ManSim_t * p, int LevelMax );
extern int Cec_ManSimClassesRefine( Cec_ManSim_t * p );
extern int Cec_ManSimSimulateRound( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t * vInfoCos );
/*=== cecIso.c ============================================================*/
@@ -192,8 +194,8 @@ extern Vec_Ptr_t * Cec_ManPatCollectPatterns( Cec_ManPat_t * pMan, int
extern Vec_Ptr_t * Cec_ManPatPackPatterns( Vec_Int_t * vCexStore, int nInputs, int nRegs, int nWordsInit );
/*=== cecSeq.c ============================================================*/
extern int Cec_ManSeqResimulate( Cec_ManSim_t * p, Vec_Ptr_t * vInfo );
-extern int Cec_ManSeqResimulateInfo( Gia_Man_t * pAig, Vec_Ptr_t * vSimInfo, Gia_Cex_t * pBestState, int fCheckMiter );
-extern void Cec_ManSeqDeriveInfoInitRandom( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Gia_Cex_t * pCex );
+extern int Cec_ManSeqResimulateInfo( Gia_Man_t * pAig, Vec_Ptr_t * vSimInfo, Abc_Cex_t * pBestState, int fCheckMiter );
+extern void Cec_ManSeqDeriveInfoInitRandom( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Abc_Cex_t * pCex );
extern int Cec_ManCountNonConstOutputs( Gia_Man_t * pAig );
extern int Cec_ManCheckNonTrivialCands( Gia_Man_t * pAig );
/*=== cecSolve.c ============================================================*/
@@ -209,9 +211,11 @@ extern Vec_Int_t * Cec_ManSatReadCex( Cec_ManSat_t * p );
extern Gia_Man_t * Cec_ManFraSpecReduction( Cec_ManFra_t * p );
extern int Cec_ManFraClassesUpdate( Cec_ManFra_t * p, Cec_ManSim_t * pSim, Cec_ManPat_t * pPat, Gia_Man_t * pNew );
-#ifdef __cplusplus
-}
-#endif
+
+
+ABC_NAMESPACE_HEADER_END
+
+
#endif
diff --git a/src/aig/cec/cecIso.c b/src/aig/cec/cecIso.c
index d9aa5240..ec237fe5 100644
--- a/src/aig/cec/cecIso.c
+++ b/src/aig/cec/cecIso.c
@@ -20,6 +20,9 @@
#include "cecInt.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -348,13 +351,13 @@ int * Cec_ManDetectIsomorphism( Gia_Man_t * p )
{
if ( (Gia_ObjIsHead(p,pIso[i]) && Gia_ObjRepr(p,i)==pIso[i]) ||
(Gia_ObjIsClass(p,pIso[i]) && Gia_ObjRepr(p,i)==Gia_ObjRepr(p,pIso[i])) )
- printf( "1" );
+ Abc_Print( 1, "1" );
else
- printf( "0" );
+ Abc_Print( 1, "0" );
}
*/
}
- printf( "Computed %d pairs of structurally equivalent nodes.\n", Counter );
+ Abc_Print( 1, "Computed %d pairs of structurally equivalent nodes.\n", Counter );
// p->pIso = pIso;
// Cec_ManTransformClasses( p );
@@ -368,3 +371,5 @@ int * Cec_ManDetectIsomorphism( Gia_Man_t * p )
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/cec/cecMan.c b/src/aig/cec/cecMan.c
index 70396cca..f03ec701 100644
--- a/src/aig/cec/cecMan.c
+++ b/src/aig/cec/cecMan.c
@@ -20,6 +20,9 @@
#include "cecInt.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -70,21 +73,21 @@ Cec_ManSat_t * Cec_ManSatCreate( Gia_Man_t * pAig, Cec_ParSat_t * pPars )
***********************************************************************/
void Cec_ManSatPrintStats( Cec_ManSat_t * p )
{
- printf( "CO = %8d ", Gia_ManCoNum(p->pAig) );
- printf( "AND = %8d ", Gia_ManAndNum(p->pAig) );
- printf( "Conf = %5d ", p->pPars->nBTLimit );
- printf( "MinVar = %5d ", p->pPars->nSatVarMax );
- printf( "MinCalls = %5d\n", p->pPars->nCallsRecycle );
- printf( "Unsat calls %6d (%6.2f %%) Ave conf = %8.1f ",
+ Abc_Print( 1, "CO = %8d ", Gia_ManCoNum(p->pAig) );
+ Abc_Print( 1, "AND = %8d ", Gia_ManAndNum(p->pAig) );
+ Abc_Print( 1, "Conf = %5d ", p->pPars->nBTLimit );
+ Abc_Print( 1, "MinVar = %5d ", p->pPars->nSatVarMax );
+ Abc_Print( 1, "MinCalls = %5d\n", p->pPars->nCallsRecycle );
+ Abc_Print( 1, "Unsat calls %6d (%6.2f %%) Ave conf = %8.1f ",
p->nSatUnsat, p->nSatTotal? 100.0*p->nSatUnsat/p->nSatTotal : 0.0, p->nSatUnsat? 1.0*p->nConfUnsat/p->nSatUnsat :0.0 );
- ABC_PRTP( "Time", p->timeSatUnsat, p->timeTotal );
- printf( "Sat calls %6d (%6.2f %%) Ave conf = %8.1f ",
+ Abc_PrintTimeP( 1, "Time", p->timeSatUnsat, p->timeTotal );
+ Abc_Print( 1, "Sat calls %6d (%6.2f %%) Ave conf = %8.1f ",
p->nSatSat, p->nSatTotal? 100.0*p->nSatSat/p->nSatTotal : 0.0, p->nSatSat? 1.0*p->nConfSat/p->nSatSat : 0.0 );
- ABC_PRTP( "Time", p->timeSatSat, p->timeTotal );
- printf( "Undef calls %6d (%6.2f %%) Ave conf = %8.1f ",
+ Abc_PrintTimeP( 1, "Time", p->timeSatSat, p->timeTotal );
+ Abc_Print( 1, "Undef calls %6d (%6.2f %%) Ave conf = %8.1f ",
p->nSatUndec, p->nSatTotal? 100.0*p->nSatUndec/p->nSatTotal : 0.0, p->nSatUndec? 1.0*p->nConfUndec/p->nSatUndec : 0.0 );
- ABC_PRTP( "Time", p->timeSatUndec, p->timeTotal );
- ABC_PRT( "Total time", p->timeTotal );
+ Abc_PrintTimeP( 1, "Time", p->timeSatUndec, p->timeTotal );
+ Abc_PrintTime( 1, "Total time", p->timeTotal );
}
/**Function*************************************************************
@@ -146,18 +149,18 @@ Cec_ManPat_t * Cec_ManPatStart()
***********************************************************************/
void Cec_ManPatPrintStats( Cec_ManPat_t * p )
{
- printf( "Latest: P = %8d. L = %10d. Lm = %10d. Ave = %6.1f. MEM =%6.2f Mb\n",
+ Abc_Print( 1, "Latest: P = %8d. L = %10d. Lm = %10d. Ave = %6.1f. MEM =%6.2f Mb\n",
p->nPats, p->nPatLits, p->nPatLitsMin, 1.0 * p->nPatLitsMin/p->nPats,
1.0*(Vec_StrSize(p->vStorage)-p->iStart)/(1<<20) );
- printf( "Total: P = %8d. L = %10d. Lm = %10d. Ave = %6.1f. MEM =%6.2f Mb\n",
+ Abc_Print( 1, "Total: P = %8d. L = %10d. Lm = %10d. Ave = %6.1f. MEM =%6.2f Mb\n",
p->nPatsAll, p->nPatLitsAll, p->nPatLitsMinAll, 1.0 * p->nPatLitsMinAll/p->nPatsAll,
1.0*Vec_StrSize(p->vStorage)/(1<<20) );
- ABC_PRTP( "Finding ", p->timeFind, p->timeTotal );
- ABC_PRTP( "Shrinking", p->timeShrink, p->timeTotal );
- ABC_PRTP( "Verifying", p->timeVerify, p->timeTotal );
- ABC_PRTP( "Sorting ", p->timeSort, p->timeTotal );
- ABC_PRTP( "Packing ", p->timePack, p->timeTotal );
- ABC_PRT( "TOTAL ", p->timeTotal );
+ Abc_PrintTimeP( 1, "Finding ", p->timeFind, p->timeTotal );
+ Abc_PrintTimeP( 1, "Shrinking", p->timeShrink, p->timeTotal );
+ Abc_PrintTimeP( 1, "Verifying", p->timeVerify, p->timeTotal );
+ Abc_PrintTimeP( 1, "Sorting ", p->timeSort, p->timeTotal );
+ Abc_PrintTimeP( 1, "Packing ", p->timePack, p->timeTotal );
+ Abc_PrintTime( 1, "TOTAL ", p->timeTotal );
}
/**Function*************************************************************
@@ -290,3 +293,5 @@ void Cec_ManFraStop( Cec_ManFra_t * p )
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/cec/cecPat.c b/src/aig/cec/cecPat.c
index 8537fe4a..82c12ea9 100644
--- a/src/aig/cec/cecPat.c
+++ b/src/aig/cec/cecPat.c
@@ -20,6 +20,9 @@
#include "cecInt.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -296,7 +299,7 @@ void Cec_ManPatVerifyPattern( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vPat
Value = Cec_ManPatComputePattern3_rec( p, Gia_ObjFanin0(pObj) );
Value = Gia_XsimNotCond( Value, Gia_ObjFaninC0(pObj) );
if ( Value != GIA_ONE )
- printf( "Cec_ManPatVerifyPattern(): Verification failed.\n" );
+ Abc_Print( 1, "Cec_ManPatVerifyPattern(): Verification failed.\n" );
assert( Value == GIA_ONE );
}
@@ -412,16 +415,16 @@ int Cec_ManPatCollectTry( Vec_Ptr_t * vInfo, Vec_Ptr_t * vPres, int iBit, int *
int i;
for ( i = 0; i < nLits; i++ )
{
- pInfo = Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i]));
- pPres = Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i]));
+ pInfo = (unsigned *)Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i]));
+ pPres = (unsigned *)Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i]));
if ( Gia_InfoHasBit( pPres, iBit ) &&
Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) )
return 0;
}
for ( i = 0; i < nLits; i++ )
{
- pInfo = Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i]));
- pPres = Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i]));
+ pInfo = (unsigned *)Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i]));
+ pPres = (unsigned *)Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i]));
Gia_InfoSetBit( pPres, iBit );
if ( Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) )
Gia_InfoXorBit( pInfo, iBit );
@@ -478,7 +481,7 @@ Vec_Ptr_t * Cec_ManPatCollectPatterns( Cec_ManPat_t * pMan, int nInputs, int nW
pMan->iStart = iStartOld;
if ( pMan->fVerbose )
{
- printf( "Total = %5d. Max used = %5d. Full = %5d. Series = %d. ",
+ Abc_Print( 1, "Total = %5d. Max used = %5d. Full = %5d. Series = %d. ",
nPatterns, kMax, nWordsInit*32, pMan->nSeries );
ABC_PRT( "Time", clock() - clk );
Cec_ManPatPrintStats( pMan );
@@ -551,7 +554,7 @@ Vec_Ptr_t * Cec_ManPatPackPatterns( Vec_Int_t * vCexStore, int nInputs, int nReg
nBits *= 2;
}
}
-// printf( "packed %d patterns into %d vectors (out of %d)\n", nPatterns, kMax, nBits );
+// Abc_Print( 1, "packed %d patterns into %d vectors (out of %d)\n", nPatterns, kMax, nBits );
Vec_PtrFree( vPres );
Vec_IntFree( vPat );
return vInfo;
@@ -562,3 +565,5 @@ Vec_Ptr_t * Cec_ManPatPackPatterns( Vec_Int_t * vCexStore, int nInputs, int nReg
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
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
+
diff --git a/src/aig/cec/cecSim.c b/src/aig/cec/cecSim.c
index 61610a46..92f8fc2e 100644
--- a/src/aig/cec/cecSim.c
+++ b/src/aig/cec/cecSim.c
@@ -20,6 +20,9 @@
#include "cecInt.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -46,3 +49,5 @@
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/cec/cecSolve.c b/src/aig/cec/cecSolve.c
index fa10d222..dc1b88eb 100644
--- a/src/aig/cec/cecSolve.c
+++ b/src/aig/cec/cecSolve.c
@@ -20,6 +20,9 @@
#include "cecInt.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -188,7 +191,7 @@ void Cec_AddClausesSuper( Cec_ManSat_t * p, Gia_Obj_t * pNode, Vec_Ptr_t * vSupe
pLits = ABC_ALLOC( int, nLits );
// suppose AND-gate is A & B = C
// add !A => !C or A + !C
- Vec_PtrForEachEntry( vSuper, pFanin, i )
+ Vec_PtrForEachEntry( Gia_Obj_t *, vSuper, pFanin, i )
{
pLits[0] = toLitCond(Cec_ObjSatNum(p,Gia_Regular(pFanin)), Gia_IsComplement(pFanin));
pLits[1] = toLitCond(Cec_ObjSatNum(p,pNode), 1);
@@ -201,7 +204,7 @@ void Cec_AddClausesSuper( Cec_ManSat_t * p, Gia_Obj_t * pNode, Vec_Ptr_t * vSupe
assert( RetValue );
}
// add A & B => C or !A + !B + C
- Vec_PtrForEachEntry( vSuper, pFanin, i )
+ Vec_PtrForEachEntry( Gia_Obj_t *, vSuper, pFanin, i )
{
pLits[i] = toLitCond(Cec_ObjSatNum(p,Gia_Regular(pFanin)), !Gia_IsComplement(pFanin));
if ( p->pPars->fPolarFlip )
@@ -320,7 +323,7 @@ void Cec_CnfNodeAddToSolver( Cec_ManSat_t * p, Gia_Obj_t * pObj )
vFrontier = Vec_PtrAlloc( 100 );
Cec_ObjAddToFrontier( p, pObj, vFrontier );
// explore nodes in the frontier
- Vec_PtrForEachEntry( vFrontier, pNode, i )
+ Vec_PtrForEachEntry( Gia_Obj_t *, vFrontier, pNode, i )
{
// create the supergate
assert( Cec_ObjSatNum(p,pNode) );
@@ -331,14 +334,14 @@ void Cec_CnfNodeAddToSolver( Cec_ManSat_t * p, Gia_Obj_t * pObj )
Vec_PtrPushUnique( p->vFanins, Gia_ObjFanin0( Gia_ObjFanin1(pNode) ) );
Vec_PtrPushUnique( p->vFanins, Gia_ObjFanin1( Gia_ObjFanin0(pNode) ) );
Vec_PtrPushUnique( p->vFanins, Gia_ObjFanin1( Gia_ObjFanin1(pNode) ) );
- Vec_PtrForEachEntry( p->vFanins, pFanin, k )
+ Vec_PtrForEachEntry( Gia_Obj_t *, p->vFanins, pFanin, k )
Cec_ObjAddToFrontier( p, Gia_Regular(pFanin), vFrontier );
Cec_AddClausesMux( p, pNode );
}
else
{
Cec_CollectSuper( pNode, fUseMuxes, p->vFanins );
- Vec_PtrForEachEntry( p->vFanins, pFanin, k )
+ Vec_PtrForEachEntry( Gia_Obj_t *, p->vFanins, pFanin, k )
Cec_ObjAddToFrontier( p, Gia_Regular(pFanin), vFrontier );
Cec_AddClausesSuper( p, pNode, p->vFanins );
}
@@ -366,7 +369,7 @@ void Cec_ManSatSolverRecycle( Cec_ManSat_t * p )
{
Gia_Obj_t * pObj;
int i;
- Vec_PtrForEachEntry( p->vUsedNodes, pObj, i )
+ Vec_PtrForEachEntry( Gia_Obj_t *, p->vUsedNodes, pObj, i )
Cec_ObjSetSatNum( p, pObj, 0 );
Vec_PtrClear( p->vUsedNodes );
// memset( p->pSatVars, 0, sizeof(int) * Gia_ManObjNumMax(p->pAigTotal) );
@@ -404,9 +407,9 @@ void Cec_SetActivityFactors_rec( Cec_ManSat_t * p, Gia_Obj_t * pObj, int LevelMi
float dActConeBumpMax = 20.0;
int iVar;
// skip visited variables
- if ( Gia_ObjIsTravIdCurrentArray(p->pAig, pObj) )
+ if ( Gia_ObjIsTravIdCurrent(p->pAig, pObj) )
return;
- Gia_ObjSetTravIdCurrentArray(p->pAig, pObj);
+ Gia_ObjSetTravIdCurrent(p->pAig, pObj);
// add the PI to the list
if ( Gia_ObjLevel(p->pAig, pObj) <= LevelMin || Gia_ObjIsCi(pObj) )
return;
@@ -440,7 +443,7 @@ int Cec_SetActivityFactors( Cec_ManSat_t * p, Gia_Obj_t * pObj )
// reset the active variables
veci_resize(&p->pSat->act_vars, 0);
// prepare for traversal
- Gia_ManIncrementTravIdArray( p->pAig );
+ Gia_ManIncrementTravId( p->pAig );
// determine the min and max level to visit
assert( dActConeRatio > 0 && dActConeRatio < 1 );
LevelMax = Gia_ObjLevel(p->pAig,pObj);
@@ -491,7 +494,7 @@ int Cec_ManSatCheckNode( Cec_ManSat_t * p, Gia_Obj_t * pObj )
clk2 = clock();
Cec_CnfNodeAddToSolver( p, pObjR );
//ABC_PRT( "cnf", clock() - clk2 );
-//printf( "%d \n", p->pSat->size );
+//Abc_Print( 1, "%d \n", p->pSat->size );
clk2 = clock();
// Cec_SetActivityFactors( p, pObjR );
@@ -529,7 +532,7 @@ p->timeSatUnsat += clock() - clk;
assert( RetValue );
p->nSatUnsat++;
p->nConfUnsat += p->pSat->stats.conflicts - nConflicts;
-//printf( "UNSAT after %d conflicts\n", p->pSat->stats.conflicts - nConflicts );
+//Abc_Print( 1, "UNSAT after %d conflicts\n", p->pSat->stats.conflicts - nConflicts );
return 1;
}
else if ( RetValue == l_True )
@@ -537,7 +540,7 @@ p->timeSatUnsat += clock() - clk;
p->timeSatSat += clock() - clk;
p->nSatSat++;
p->nConfSat += p->pSat->stats.conflicts - nConflicts;
-//printf( "SAT after %d conflicts\n", p->pSat->stats.conflicts - nConflicts );
+//Abc_Print( 1, "SAT after %d conflicts\n", p->pSat->stats.conflicts - nConflicts );
return 0;
}
else // if ( RetValue == l_Undef )
@@ -545,7 +548,7 @@ p->timeSatSat += clock() - clk;
p->timeSatUndec += clock() - clk;
p->nSatUndec++;
p->nConfUndec += p->pSat->stats.conflicts - nConflicts;
-//printf( "UNDEC after %d conflicts\n", p->pSat->stats.conflicts - nConflicts );
+//Abc_Print( 1, "UNDEC after %d conflicts\n", p->pSat->stats.conflicts - nConflicts );
return -1;
}
}
@@ -591,7 +594,7 @@ clk2 = clock();
Cec_CnfNodeAddToSolver( p, pObjR1 );
Cec_CnfNodeAddToSolver( p, pObjR2 );
//ABC_PRT( "cnf", clock() - clk2 );
-//printf( "%d \n", p->pSat->size );
+//Abc_Print( 1, "%d \n", p->pSat->size );
clk2 = clock();
// Cec_SetActivityFactors( p, pObjR1 );
@@ -633,7 +636,7 @@ p->timeSatUnsat += clock() - clk;
assert( RetValue );
p->nSatUnsat++;
p->nConfUnsat += p->pSat->stats.conflicts - nConflicts;
-//printf( "UNSAT after %d conflicts\n", p->pSat->stats.conflicts - nConflicts );
+//Abc_Print( 1, "UNSAT after %d conflicts\n", p->pSat->stats.conflicts - nConflicts );
return 1;
}
else if ( RetValue == l_True )
@@ -641,7 +644,7 @@ p->timeSatUnsat += clock() - clk;
p->timeSatSat += clock() - clk;
p->nSatSat++;
p->nConfSat += p->pSat->stats.conflicts - nConflicts;
-//printf( "SAT after %d conflicts\n", p->pSat->stats.conflicts - nConflicts );
+//Abc_Print( 1, "SAT after %d conflicts\n", p->pSat->stats.conflicts - nConflicts );
return 0;
}
else // if ( RetValue == l_Undef )
@@ -649,7 +652,7 @@ p->timeSatSat += clock() - clk;
p->timeSatUndec += clock() - clk;
p->nSatUndec++;
p->nConfUndec += p->pSat->stats.conflicts - nConflicts;
-//printf( "UNDEC after %d conflicts\n", p->pSat->stats.conflicts - nConflicts );
+//Abc_Print( 1, "UNDEC after %d conflicts\n", p->pSat->stats.conflicts - nConflicts );
return -1;
}
}
@@ -683,7 +686,7 @@ void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPar
}
Gia_ManSetPhase( pAig );
Gia_ManLevelNum( pAig );
- Gia_ManResetTravIdArray( pAig );
+ Gia_ManIncrementTravId( pAig );
p = Cec_ManSatCreate( pAig, pPars );
pProgress = Bar_ProgressStart( stdout, Gia_ManPoNum(pAig) );
Gia_ManForEachCo( pAig, pObj, i )
@@ -705,7 +708,7 @@ clk2 = clock();
Gia_Man_t * pTemp = Gia_ManDupDfsCone( pAig, pObj );
Gia_WriteAiger( pTemp, "gia_hard.aig", 0, 0 );
Gia_ManStop( pTemp );
- printf( "Dumping hard cone into file \"%s\".\n", "gia_hard.aig" );
+ Abc_Print( 1, "Dumping hard cone into file \"%s\".\n", "gia_hard.aig" );
}
*/
if ( status != 0 )
@@ -759,12 +762,12 @@ Vec_Int_t * Cec_ManSatReadCex( Cec_ManSat_t * pSat )
***********************************************************************/
void Cec_ManSatSolveSeq_rec( Cec_ManSat_t * pSat, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Ptr_t * vInfo, int iPat, int nRegs )
{
- if ( Gia_ObjIsTravIdCurrentArray(p, pObj) )
+ if ( Gia_ObjIsTravIdCurrent(p, pObj) )
return;
- Gia_ObjSetTravIdCurrentArray(p, pObj);
+ Gia_ObjSetTravIdCurrent(p, pObj);
if ( Gia_ObjIsCi(pObj) )
{
- unsigned * pInfo = Vec_PtrEntry( vInfo, nRegs + Gia_ObjCioId(pObj) );
+ unsigned * pInfo = (unsigned *)Vec_PtrEntry( vInfo, nRegs + Gia_ObjCioId(pObj) );
if ( Cec_ObjSatVarValue( pSat, pObj ) != Gia_InfoHasBit( pInfo, iPat ) )
Gia_InfoXorBit( pInfo, iPat );
pSat->nCexLits++;
@@ -799,7 +802,7 @@ Vec_Str_t * Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat
nPatsInit = nPats = 32 * Vec_PtrReadWordsSimInfo(vPatts);
Gia_ManSetPhase( pAig );
Gia_ManLevelNum( pAig );
- Gia_ManResetTravIdArray( pAig );
+ Gia_ManIncrementTravId( pAig );
p = Cec_ManSatCreate( pAig, pPars );
vStatus = Vec_StrAlloc( Gia_ManPoNum(pAig) );
pProgress = Bar_ProgressStart( stdout, Gia_ManPoNum(pAig) );
@@ -810,18 +813,18 @@ Vec_Str_t * Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat
{
if ( Gia_ObjFaninC0(pObj) )
{
-// printf( "Constant 1 output of SRM!!!\n" );
+// Abc_Print( 1, "Constant 1 output of SRM!!!\n" );
Vec_StrPush( vStatus, 0 );
}
else
{
-// printf( "Constant 0 output of SRM!!!\n" );
+// Abc_Print( 1, "Constant 0 output of SRM!!!\n" );
Vec_StrPush( vStatus, 1 );
}
continue;
}
status = Cec_ManSatCheckNode( p, Gia_ObjChild0(pObj) );
-//printf( "output %d status = %d\n", i, status );
+//Abc_Print( 1, "output %d status = %d\n", i, status );
Vec_StrPush( vStatus, (char)status );
if ( status != 0 )
continue;
@@ -836,7 +839,7 @@ Vec_Str_t * Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat
if ( iPat % nPatsInit == 0 )
iPat++;
// save the pattern
- Gia_ManIncrementTravIdArray( pAig );
+ Gia_ManIncrementTravId( pAig );
// Vec_IntClear( p->vCex );
Cec_ManSatSolveSeq_rec( p, pAig, Gia_ObjFanin0(pObj), vPatts, iPat++, nRegs );
// Gia_SatVerifyPattern( pAig, pObj, p->vCex, p->vVisits );
@@ -853,7 +856,7 @@ Vec_Str_t * Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat
Bar_ProgressStop( pProgress );
if ( pPars->fVerbose )
Cec_ManSatPrintStats( p );
-// printf( "Total number of cex literals = %d. (Ave = %d)\n", p->nCexLits, p->nCexLits/p->nSatSat );
+// Abc_Print( 1, "Total number of cex literals = %d. (Ave = %d)\n", p->nCexLits, p->nCexLits/p->nSatSat );
Cec_ManSatStop( p );
if ( pnPats )
*pnPats = iPat-1;
@@ -900,9 +903,9 @@ void Cec_ManSatAddToStore( Vec_Int_t * vCexStore, Vec_Int_t * vCex, int Out )
***********************************************************************/
void Cec_ManSatSolveMiter_rec( Cec_ManSat_t * pSat, Gia_Man_t * p, Gia_Obj_t * pObj )
{
- if ( Gia_ObjIsTravIdCurrentArray(p, pObj) )
+ if ( Gia_ObjIsTravIdCurrent(p, pObj) )
return;
- Gia_ObjSetTravIdCurrentArray(p, pObj);
+ Gia_ObjSetTravIdCurrent(p, pObj);
if ( Gia_ObjIsCi(pObj) )
{
pSat->nCexLits++;
@@ -928,7 +931,7 @@ void Cec_ManSatSolveMiter_rec( Cec_ManSat_t * pSat, Gia_Man_t * p, Gia_Obj_t * p
void Cec_ManSavePattern( Cec_ManSat_t * p, Gia_Obj_t * pObj1, Gia_Obj_t * pObj2 )
{
Vec_IntClear( p->vCex );
- Gia_ManIncrementTravIdArray( p->pAig );
+ Gia_ManIncrementTravId( p->pAig );
Cec_ManSatSolveMiter_rec( p, p->pAig, Gia_Regular(pObj1) );
if ( pObj2 )
Cec_ManSatSolveMiter_rec( p, p->pAig, Gia_Regular(pObj2) );
@@ -957,7 +960,7 @@ Vec_Int_t * Cec_ManSatSolveMiter( Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_St
// prepare AIG
Gia_ManSetPhase( pAig );
Gia_ManLevelNum( pAig );
- Gia_ManResetTravIdArray( pAig );
+ Gia_ManIncrementTravId( pAig );
// create resulting data-structures
vStatus = Vec_StrAlloc( Gia_ManPoNum(pAig) );
vCexStore = Vec_IntAlloc( 10000 );
@@ -972,13 +975,13 @@ Vec_Int_t * Cec_ManSatSolveMiter( Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_St
{
if ( Gia_ObjFaninC0(pObj) )
{
-// printf( "Constant 1 output of SRM!!!\n" );
+// Abc_Print( 1, "Constant 1 output of SRM!!!\n" );
Cec_ManSatAddToStore( vCexStore, p->vCex, i ); // trivial counter-example
Vec_StrPush( vStatus, 0 );
}
else
{
-// printf( "Constant 0 output of SRM!!!\n" );
+// Abc_Print( 1, "Constant 0 output of SRM!!!\n" );
Vec_StrPush( vStatus, 1 );
}
continue;
@@ -994,7 +997,7 @@ Vec_Int_t * Cec_ManSatSolveMiter( Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_St
continue;
assert( status == 0 );
// save the pattern
-// Gia_ManIncrementTravIdArray( pAig );
+// Gia_ManIncrementTravId( pAig );
// Cec_ManSatSolveMiter_rec( p, pAig, Gia_ObjFanin0(pObj) );
Cec_ManSavePattern( p, Gia_ObjFanin0(pObj), NULL );
// Gia_SatVerifyPattern( pAig, pObj, p->vCex, p->vVisits );
@@ -1015,3 +1018,5 @@ Vec_Int_t * Cec_ManSatSolveMiter( Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_St
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/cec/cecSweep.c b/src/aig/cec/cecSweep.c
index 1b68efe0..97f5e36a 100644
--- a/src/aig/cec/cecSweep.c
+++ b/src/aig/cec/cecSweep.c
@@ -20,6 +20,9 @@
#include "cecInt.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -162,8 +165,8 @@ void Cec_ManFraCreateInfo( Cec_ManSim_t * p, Vec_Ptr_t * vCiInfo, Vec_Ptr_t * vI
int i, w;
for ( i = 0; i < Gia_ManCiNum(p->pAig); i++ )
{
- pRes0 = Vec_PtrEntry( vCiInfo, i );
- pRes1 = Vec_PtrEntry( vInfo, i );
+ pRes0 = (unsigned *)Vec_PtrEntry( vCiInfo, i );
+ pRes1 = (unsigned *)Vec_PtrEntry( vInfo, i );
pRes1 += p->nWords * nSeries;
for ( w = 0; w < p->nWords; w++ )
pRes0[w] = pRes1[w];
@@ -270,7 +273,7 @@ p->timeSim += clock() - clk;
// if ( pObjOld->fMark0 == 0 )
{
if ( iRepr == Gia_ObjRepr(p->pAig, iNode) )
- printf( "Cec_ManFraClassesUpdate(): Error! Node is not refined!\n" );
+ Abc_Print( 1, "Cec_ManFraClassesUpdate(): Error! Node is not refined!\n" );
p->nAllDisproved++;
}
}
@@ -292,3 +295,5 @@ p->timeSim += clock() - clk;
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/cec/cecSynth.c b/src/aig/cec/cecSynth.c
new file mode 100644
index 00000000..52b50a43
--- /dev/null
+++ b/src/aig/cec/cecSynth.c
@@ -0,0 +1,380 @@
+/**CFile****************************************************************
+
+ FileName [cecSynth.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Combinational equivalence checking.]
+
+ Synopsis [Partitioned sequential synthesis.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: cecSynth.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cecInt.h"
+#include "giaAig.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Populate sequential synthesis parameters.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cec_SeqSynthesisSetDefaultParams( Cec_ParSeq_t * p )
+{
+ memset( p, 0, sizeof(Cec_ParSeq_t) );
+ p->fUseLcorr = 0; // enables latch correspondence
+ p->fUseScorr = 0; // enables signal correspondence
+ p->nBTLimit = 1000; // (scorr/lcorr) conflict limit at a node
+ p->nFrames = 1; // (scorr only) the number of timeframes
+ p->nLevelMax = -1; // (scorr only) the max number of levels
+ p->fConsts = 1; // (scl only) merging constants
+ p->fEquivs = 1; // (scl only) merging equivalences
+ p->fUseMiniSat = 0; // enables MiniSat in lcorr/scorr
+ p->nMinDomSize = 100; // the size of minimum clock domain
+ p->fVeryVerbose = 0; // verbose stats
+ p->fVerbose = 0; // verbose stats
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Cec_SeqReadMinDomSize( Cec_ParSeq_t * p )
+{
+ return p->nMinDomSize;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Cec_SeqReadVerbose( Cec_ParSeq_t * p )
+{
+ return p->fVerbose;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes partitioning of registers.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManRegCreatePart( Gia_Man_t * p, Vec_Int_t * vPart, int * pnCountPis, int * pnCountRegs, int ** ppMapBack )
+{
+ Gia_Man_t * pNew;
+ Gia_Obj_t * pObj;
+ Vec_Int_t * vNodes, * vRoots;
+ int i, iOut, nCountPis, nCountRegs;
+ int * pMapBack;
+ // collect/mark nodes/PIs in the DFS order from the roots
+ Gia_ManIncrementTravId( p );
+ vRoots = Vec_IntAlloc( Vec_IntSize(vPart) );
+ Vec_IntForEachEntry( vPart, iOut, i )
+ Vec_IntPush( vRoots, Gia_ObjId(p, Gia_ManCo(p, Gia_ManPoNum(p)+iOut)) );
+ vNodes = Gia_ManCollectNodesCis( p, Vec_IntArray(vRoots), Vec_IntSize(vRoots) );
+ Vec_IntFree( vRoots );
+ // unmark register outputs
+ Vec_IntForEachEntry( vPart, iOut, i )
+ Gia_ObjSetTravIdPrevious( p, Gia_ManCi(p, Gia_ManPiNum(p)+iOut) );
+ // count pure PIs
+ nCountPis = nCountRegs = 0;
+ Gia_ManForEachPi( p, pObj, i )
+ nCountPis += Gia_ObjIsTravIdCurrent(p, pObj);
+ // count outputs of other registers
+ Gia_ManForEachRo( p, pObj, i )
+ nCountRegs += Gia_ObjIsTravIdCurrent(p, pObj); // should be !Gia_... ???
+ if ( pnCountPis )
+ *pnCountPis = nCountPis;
+ if ( pnCountRegs )
+ *pnCountRegs = nCountRegs;
+ // clean old manager
+ Gia_ManFillValue(p);
+ Gia_ManConst0(p)->Value = 0;
+ // create the new manager
+ pNew = Gia_ManStart( Vec_IntSize(vNodes) );
+ // create the PIs
+ Gia_ManForEachCi( p, pObj, i )
+ if ( Gia_ObjIsTravIdCurrent(p, pObj) )
+ pObj->Value = Gia_ManAppendCi(pNew);
+ // add variables for the register outputs
+ // create fake POs to hold the register outputs
+ Vec_IntForEachEntry( vPart, iOut, i )
+ {
+ pObj = Gia_ManCi(p, Gia_ManPiNum(p)+iOut);
+ pObj->Value = Gia_ManAppendCi(pNew);
+ Gia_ManAppendCo( pNew, pObj->Value );
+ Gia_ObjSetTravIdCurrent( p, pObj ); // added
+ }
+ // create the nodes
+ Gia_ManForEachObjVec( vNodes, p, pObj, i )
+ if ( Gia_ObjIsAnd(pObj) )
+ pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+ // add real POs for the registers
+ Vec_IntForEachEntry( vPart, iOut, i )
+ {
+ pObj = Gia_ManCo( p, Gia_ManPoNum(p)+iOut );
+ Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+ }
+ Gia_ManSetRegNum( pNew, Vec_IntSize(vPart) );
+ // create map
+ if ( ppMapBack )
+ {
+ pMapBack = ABC_FALLOC( int, Gia_ManObjNum(pNew) );
+ // map constant nodes
+ pMapBack[0] = 0;
+ // logic cones of register outputs
+ Gia_ManForEachObjVec( vNodes, p, pObj, i )
+ {
+// pObjNew = Aig_Regular(pObj->pData);
+// pMapBack[pObjNew->Id] = pObj->Id;
+ assert( Gia_Lit2Var(Gia_ObjValue(pObj)) >= 0 );
+ assert( Gia_Lit2Var(Gia_ObjValue(pObj)) < Gia_ManObjNum(pNew) );
+ pMapBack[ Gia_Lit2Var(Gia_ObjValue(pObj)) ] = Gia_ObjId(p, pObj);
+ }
+ // map register outputs
+ Vec_IntForEachEntry( vPart, iOut, i )
+ {
+ pObj = Gia_ManCi(p, Gia_ManPiNum(p)+iOut);
+// pObjNew = pObj->pData;
+// pMapBack[pObjNew->Id] = pObj->Id;
+ assert( Gia_Lit2Var(Gia_ObjValue(pObj)) >= 0 );
+ assert( Gia_Lit2Var(Gia_ObjValue(pObj)) < Gia_ManObjNum(pNew) );
+ pMapBack[ Gia_Lit2Var(Gia_ObjValue(pObj)) ] = Gia_ObjId(p, pObj);
+ }
+ *ppMapBack = pMapBack;
+ }
+ Vec_IntFree( vNodes );
+ return pNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Transfers the classes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Gia_TransferMappedClasses( Gia_Man_t * pPart, int * pMapBack, int * pReprs )
+{
+ Gia_Obj_t * pObj;
+ int i, Id1, Id2, nClasses;
+ if ( pPart->pReprs == NULL )
+ return 0;
+ nClasses = 0;
+ Gia_ManForEachObj( pPart, pObj, i )
+ {
+ if ( Gia_ObjRepr(pPart, i) == GIA_VOID )
+ continue;
+ assert( i < Gia_ManObjNum(pPart) );
+ assert( Gia_ObjRepr(pPart, i) < Gia_ManObjNum(pPart) );
+ Id1 = pMapBack[ i ];
+ Id2 = pMapBack[ Gia_ObjRepr(pPart, i) ];
+ if ( Id1 == Id2 )
+ continue;
+ if ( Id1 < Id2 )
+ pReprs[Id2] = Id1;
+ else
+ pReprs[Id1] = Id2;
+ nClasses++;
+ }
+ return nClasses;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Gia_ManFindRepr_rec( int * pReprs, int Id )
+{
+ if ( pReprs[Id] == 0 )
+ return 0;
+ if ( pReprs[Id] == ~0 )
+ return Id;
+ return Gia_ManFindRepr_rec( pReprs, pReprs[Id] );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Normalizes equivalences.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Gia_ManNormalizeEquivalences( Gia_Man_t * p, int * pReprs )
+{
+ int i, iRepr;
+ assert( p->pReprs == NULL );
+ assert( p->pNexts == NULL );
+ p->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) );
+ for ( i = 0; i < Gia_ManObjNum(p); i++ )
+ Gia_ObjSetRepr( p, i, GIA_VOID );
+ for ( i = 0; i < Gia_ManObjNum(p); i++ )
+ {
+ if ( pReprs[i] == ~0 )
+ continue;
+ iRepr = Gia_ManFindRepr_rec( pReprs, i );
+ Gia_ObjSetRepr( p, i, iRepr );
+ }
+ p->pNexts = Gia_ManDeriveNexts( p );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Partitioned sequential synthesis.]
+
+ Description [Returns AIG annotated with equivalence classes.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Cec_SequentialSynthesisPart( Gia_Man_t * p, Cec_ParSeq_t * pPars )
+{
+ int fPrintParts = 0;
+ char Buffer[100];
+ Gia_Man_t * pTemp;
+ Vec_Ptr_t * vParts = (Vec_Ptr_t *)p->vClockDoms;
+ Vec_Int_t * vPart;
+ int * pMapBack, * pReprs;
+ int i, nCountPis, nCountRegs;
+ int nClasses, clk = clock();
+
+ // save parameters
+ if ( fPrintParts )
+ {
+ // print partitions
+ Abc_Print( 1, "The following clock domains are used:\n" );
+ Vec_PtrForEachEntry( Vec_Int_t *, vParts, vPart, i )
+ {
+ pTemp = Gia_ManRegCreatePart( p, vPart, &nCountPis, &nCountRegs, NULL );
+ sprintf( Buffer, "part%03d.aig", i );
+ Gia_WriteAiger( pTemp, Buffer, 0, 0 );
+ Abc_Print( 1, "part%03d.aig : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d.\n",
+ i, Vec_IntSize(vPart), Gia_ManCiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Gia_ManAndNum(pTemp) );
+ Gia_ManStop( pTemp );
+ }
+ }
+
+ // perform sequential synthesis for clock domains
+ pReprs = ABC_FALLOC( int, Gia_ManObjNum(p) );
+ Vec_PtrForEachEntry( Vec_Int_t *, vParts, vPart, i )
+ {
+ pTemp = Gia_ManRegCreatePart( p, vPart, &nCountPis, &nCountRegs, &pMapBack );
+ if ( nCountPis > 0 )
+ {
+ if ( pPars->fUseScorr )
+ {
+ Cec_ParCor_t CorPars, * pCorPars = &CorPars;
+ Cec_ManCorSetDefaultParams( pCorPars );
+ pCorPars->nBTLimit = pPars->nBTLimit;
+ pCorPars->nLevelMax = pPars->nLevelMax;
+ pCorPars->fVerbose = pPars->fVeryVerbose;
+ pCorPars->fUseCSat = 1;
+ Cec_ManLSCorrespondenceClasses( pTemp, pCorPars );
+ }
+ else if ( pPars->fUseLcorr )
+ {
+ Cec_ParCor_t CorPars, * pCorPars = &CorPars;
+ Cec_ManCorSetDefaultParams( pCorPars );
+ pCorPars->fLatchCorr = 1;
+ pCorPars->nBTLimit = pPars->nBTLimit;
+ pCorPars->fVerbose = pPars->fVeryVerbose;
+ pCorPars->fUseCSat = 1;
+ Cec_ManLSCorrespondenceClasses( pTemp, pCorPars );
+ }
+ else
+ {
+// pNew = Gia_ManSeqStructSweep( pTemp, pPars->fConsts, pPars->fEquivs, pPars->fVerbose );
+// Gia_ManStop( pNew );
+ Gia_ManSeqCleanupClasses( pTemp, pPars->fConsts, pPars->fEquivs, pPars->fVerbose );
+ }
+//Abc_Print( 1, "Part equivalences = %d.\n", Gia_ManEquivCountLitsAll(pTemp) );
+ nClasses = Gia_TransferMappedClasses( pTemp, pMapBack, pReprs );
+ if ( pPars->fVerbose )
+ {
+ Abc_Print( 1, "%3d : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d. Cl = %5d.\n",
+ i, Vec_IntSize(vPart), Gia_ManCiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Gia_ManAndNum(pTemp), nClasses );
+ }
+ }
+ Gia_ManStop( pTemp );
+ ABC_FREE( pMapBack );
+ }
+
+ // generate resulting equivalences
+ Gia_ManNormalizeEquivalences( p, pReprs );
+//Abc_Print( 1, "Total equivalences = %d.\n", Gia_ManEquivCountLitsAll(p) );
+ ABC_FREE( pReprs );
+ if ( pPars->fVerbose )
+ {
+ Abc_PrintTime( 1, "Total time", clock() - clk );
+ }
+ return 1;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/cec/module.make b/src/aig/cec/module.make
index 35a18cae..42e0cd1b 100644
--- a/src/aig/cec/module.make
+++ b/src/aig/cec/module.make
@@ -9,4 +9,5 @@ SRC += src/aig/cec/cecCec.c \
src/aig/cec/cecSeq.c \
src/aig/cec/cecSim.c \
src/aig/cec/cecSolve.c \
+ src/aig/cec/cecSynth.c \
src/aig/cec/cecSweep.c
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-02 16:50:56 +0000