summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/aig/cec/cec.h23
-rw-r--r--src/aig/cec/cecCec.c4
-rw-r--r--src/aig/cec/cecClass.c124
-rw-r--r--src/aig/cec/cecCore.c53
-rw-r--r--src/aig/cec/cecInt.h7
-rw-r--r--src/aig/cec/cecMan.c2
-rw-r--r--src/aig/cec/cecSeq.c314
-rw-r--r--src/aig/cec/cecSolve.c79
-rw-r--r--src/aig/cec/cecSweep.c2
-rw-r--r--src/aig/cec/module.make1
-rw-r--r--src/aig/cec2/cec.h104
-rw-r--r--src/aig/cec2/cecAig.c168
-rw-r--r--src/aig/cec2/cecClass.c571
-rw-r--r--src/aig/cec2/cecCnf.c328
-rw-r--r--src/aig/cec2/cecCore.c245
-rw-r--r--src/aig/cec2/cecInt.h208
-rw-r--r--src/aig/cec2/cecMan.c59
-rw-r--r--src/aig/cec2/cecSat.c250
-rw-r--r--src/aig/cec2/cecSat2.c284
-rw-r--r--src/aig/cec2/cecSim.c447
-rw-r--r--src/aig/cec2/cecStatus.c187
-rw-r--r--src/aig/cec2/cecSweep.c582
-rw-r--r--src/aig/cec2/module.make9
-rw-r--r--src/aig/gia/gia.h13
-rw-r--r--src/aig/gia/giaDup.c90
-rw-r--r--src/aig/gia/giaEquiv.c225
-rw-r--r--src/aig/gia/giaUtil.c57
-rw-r--r--src/base/abci/abc.c322
-rw-r--r--src/base/main/mainInt.h1
29 files changed, 1178 insertions, 3581 deletions
diff --git a/src/aig/cec/cec.h b/src/aig/cec/cec.h
index 16748233..a97bd958 100644
--- a/src/aig/cec/cec.h
+++ b/src/aig/cec/cec.h
@@ -57,7 +57,7 @@ struct Cec_ParSim_t_
int nWords; // the number of simulation words
int nRounds; // the number of simulation rounds
int TimeLimit; // the runtime limit in seconds
- int fDoubleOuts; // miter with separate outputs
+ int fDualOut; // miter with separate outputs
int fCheckMiter; // the circuit is the miter
int fFirstStop; // stop on the first sat output
int fSeqSimulate; // performs sequential simulation
@@ -65,6 +65,21 @@ struct Cec_ParSim_t_
int fVerbose; // verbose stats
};
+// semiformal parameters
+typedef struct Cec_ParSmf_t_ Cec_ParSmf_t;
+struct Cec_ParSmf_t_
+{
+ int nWords; // the number of simulation words
+ int nRounds; // the number of simulation rounds
+ int nFrames; // the number of time frames
+ int nBTLimit; // conflict limit at a node
+ int TimeLimit; // the runtime limit in seconds
+ int fDualOut; // miter with separate outputs
+ int fCheckMiter; // the circuit is the miter
+ int fFirstStop; // stop on the first sat output
+ int fVerbose; // verbose stats
+};
+
// combinational SAT sweeping parameters
typedef struct Cec_ParFra_t_ Cec_ParFra_t;
struct Cec_ParFra_t_
@@ -79,7 +94,7 @@ struct Cec_ParFra_t_
int fRewriting; // enables AIG rewriting
int fCheckMiter; // the circuit is the miter
int fFirstStop; // stop on the first sat output
- int fDoubleOuts; // miter with separate outputs
+ int fDualOut; // miter with separate outputs
int fColorDiff; // miter with separate outputs
int fVeryVerbose; // verbose stats
int fVerbose; // verbose stats
@@ -112,11 +127,15 @@ extern int Cec_ManVerifyTwo( Gia_Man_t * p0, Gia_Man_t * p1, int fVerb
/*=== cecCore.c ==========================================================*/
extern void Cec_ManSatSetDefaultParams( Cec_ParSat_t * p );
extern void Cec_ManSimSetDefaultParams( Cec_ParSim_t * p );
+extern void Cec_ManSmfSetDefaultParams( Cec_ParSmf_t * p );
extern void Cec_ManFraSetDefaultParams( Cec_ParFra_t * p );
extern void Cec_ManCecSetDefaultParams( Cec_ParCec_t * p );
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_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars );
#ifdef __cplusplus
}
diff --git a/src/aig/cec/cecCec.c b/src/aig/cec/cecCec.c
index ea730693..96bddbcb 100644
--- a/src/aig/cec/cecCec.c
+++ b/src/aig/cec/cecCec.c
@@ -134,7 +134,7 @@ int Cec_ManVerify( Gia_Man_t * p, Cec_ParCec_t * pPars )
pParsFra->fVerbose = pPars->fVerbose;
pParsFra->fCheckMiter = 1;
pParsFra->fFirstStop = 1;
- pParsFra->fDoubleOuts = 1;
+ pParsFra->fDualOut = 1;
pNew = Cec_ManSatSweeping( p, pParsFra );
if ( pNew == NULL )
{
@@ -192,7 +192,7 @@ int Cec_ManVerifyTwo( Gia_Man_t * p0, Gia_Man_t * p1, int fVerbose )
int RetValue;
Cec_ManCecSetDefaultParams( pPars );
pPars->fVerbose = fVerbose;
- pMiter = Gia_ManMiter( p0, p1, 0, 1, pPars->fVerbose );
+ pMiter = Gia_ManMiter( p0, p1, 1, 0, pPars->fVerbose );
if ( pMiter == NULL )
return -1;
RetValue = Cec_ManVerify( pMiter, pPars );
diff --git a/src/aig/cec/cecClass.c b/src/aig/cec/cecClass.c
index aaa85ffa..0cac88af 100644
--- a/src/aig/cec/cecClass.c
+++ b/src/aig/cec/cecClass.c
@@ -155,6 +155,70 @@ int Cec_ManSimCompareEqualFirstBit( unsigned * p0, unsigned * p1, int nWords )
/**Function*************************************************************
+ Synopsis [Returns the number of the first non-equal bit.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cec_ManSimCompareConstScore( unsigned * p, int nWords, int * pScores )
+{
+ int w, b;
+ if ( p[0] & 1 )
+ {
+ for ( w = 0; w < nWords; w++ )
+ if ( p[w] != ~0 )
+ for ( b = 0; b < 32; b++ )
+ if ( ((~p[w]) >> b ) & 1 )
+ pScores[32*w + b]++;
+ }
+ else
+ {
+ for ( w = 0; w < nWords; w++ )
+ if ( p[w] != 0 )
+ for ( b = 0; b < 32; b++ )
+ if ( ((p[w]) >> b ) & 1 )
+ pScores[32*w + b]++;
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Compares simulation info of two nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cec_ManSimCompareEqualScore( unsigned * p0, unsigned * p1, int nWords, int * pScores )
+{
+ int w, b;
+ if ( (p0[0] & 1) == (p1[0] & 1) )
+ {
+ for ( w = 0; w < nWords; w++ )
+ if ( p0[w] != p1[w] )
+ for ( b = 0; b < 32; b++ )
+ if ( ((p0[w] ^ p1[w]) >> b ) & 1 )
+ pScores[32*w + b]++;
+ }
+ else
+ {
+ for ( w = 0; w < nWords; w++ )
+ if ( p0[w] != ~p1[w] )
+ for ( b = 0; b < 32; b++ )
+ if ( ((p0[w] ^ ~p1[w]) >> b ) & 1 )
+ pScores[32*w + b]++;
+ }
+}
+
+/**Function*************************************************************
+
Synopsis [Creates equivalence class.]
Description []
@@ -211,7 +275,11 @@ int Cec_ManSimClassRefineOne( Cec_ManSim_t * p, int i )
if ( Cec_ManSimCompareEqual( pSim0, pSim1, p->nWords ) )
Vec_IntPush( p->vClassOld, Ent );
else
+ {
Vec_IntPush( p->vClassNew, Ent );
+ if ( p->pBestState )
+ Cec_ManSimCompareEqualScore( pSim0, pSim1, p->nWords, p->pScores );
+ }
}
if ( Vec_IntSize( p->vClassNew ) == 0 )
return 0;
@@ -422,6 +490,42 @@ void Cec_ManSimSavePattern( Cec_ManSim_t * p, int iPat )
/**Function*************************************************************
+ Synopsis [Find the best pattern using the scores.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cec_ManSimFindBestPattern( Cec_ManSim_t * p )
+{
+ unsigned * pInfo;
+ int i, ScoreBest = 0, iPatBest = 1;
+ // find the best pattern
+ for ( i = 0; i < 32 * p->nWords; i++ )
+ if ( ScoreBest < p->pScores[i] )
+ {
+ ScoreBest = p->pScores[i];
+ iPatBest = i;
+ }
+ // compare this with the available patterns - and save
+ if ( p->pBestState->iPo <= ScoreBest )
+ {
+ 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 );
+ if ( Aig_InfoHasBit(p->pBestState->pData, i) != Aig_InfoHasBit(pInfo, iPatBest) )
+ Aig_InfoXorBit( p->pBestState->pData, i );
+ }
+ p->pBestState->iPo = ScoreBest;
+ }
+}
+
+/**Function*************************************************************
+
Synopsis [Returns 1 if computation should stop.]
Description []
@@ -435,10 +539,11 @@ int Cec_ManSimAnalyzeOutputs( Cec_ManSim_t * p )
{
unsigned * pInfo, * pInfo2;
int i;
- if ( p->vCoSimInfo == NULL )
+ if ( !p->pPars->fCheckMiter )
return 0;
+ assert( p->vCoSimInfo != NULL );
// compare outputs with 0
- if ( p->pPars->fDoubleOuts )
+ if ( p->pPars->fDualOut )
{
assert( (Gia_ManCoNum(p->pAig) & 1) == 0 );
for ( i = 0; i < Gia_ManCoNum(p->pAig); i++ )
@@ -507,6 +612,10 @@ int Cec_ManSimSimulateRound( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t *
if ( p->nWordsOld != p->nWords )
Cec_ManSimMemRelink( p );
p->nMemsMax = 0;
+ // allocate score counters
+ ABC_FREE( p->pScores );
+ if ( p->pBestState )
+ p->pScores = ABC_CALLOC( int, 32 * p->nWords );
// simulate nodes
Vec_IntClear( p->vRefinedC );
if ( Gia_ObjValue(Gia_ManConst0(p->pAig)) )
@@ -583,6 +692,8 @@ references:
{
pRes[0]++;
Vec_IntPush( p->vRefinedC, i );
+ if ( p->pBestState )
+ Cec_ManSimCompareConstScore( pRes + 1, p->nWords, p->pScores );
}
// if the node belongs to a class, save it
if ( Gia_ObjIsClass(p->pAig, i) )
@@ -607,6 +718,8 @@ references:
printf( "Cec_ManSimSimulateRound(): Memory management error!\n" );
if ( p->pPars->fVeryVerbose )
Gia_ManEquivPrintClasses( p->pAig, 0, Cec_MemUsage(p) );
+ if ( p->pBestState )
+ Cec_ManSimFindBestPattern( p );
/*
if ( p->nMems > 1 ) {
for ( i = 1; i < p->nObjs; i++ )
@@ -682,8 +795,13 @@ int Cec_ManSimClassesPrepare( Cec_ManSim_t * p )
// allocate representation
p->pAig->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p->pAig) );
p->pAig->pNexts = ABC_CALLOC( int, Gia_ManObjNum(p->pAig) );
+ // set starting representative of internal nodes to be constant 0
Gia_ManForEachObj( p->pAig, pObj, i )
- Gia_ObjSetRepr( p->pAig, i, (Gia_ObjIsAnd(pObj) || Gia_ObjIsCi(pObj)) ? 0 : GIA_VOID );
+ Gia_ObjSetRepr( p->pAig, i, Gia_ObjIsAnd(pObj) ? 0 : GIA_VOID );
+ // if sequential simulation, set starting representative of ROs to be constant 0
+ if ( p->pPars->fSeqSimulate )
+ Gia_ManForEachRo( p->pAig, pObj, i )
+ Gia_ObjSetRepr( p->pAig, Gia_ObjId(p->pAig, pObj), 0 );
// perform simulation
Gia_ManSetRefs( p->pAig );
p->nWords = 1;
diff --git a/src/aig/cec/cecCore.c b/src/aig/cec/cecCore.c
index e25ddc90..061c3a7d 100644
--- a/src/aig/cec/cecCore.c
+++ b/src/aig/cec/cecCore.c
@@ -70,12 +70,37 @@ void Cec_ManSimSetDefaultParams( Cec_ParSim_t * p )
p->TimeLimit = 0; // the runtime limit in seconds
p->fCheckMiter = 0; // the circuit is the miter
p->fFirstStop = 0; // stop on the first sat output
- p->fDoubleOuts = 0; // miter with separate outputs
+ p->fDualOut = 0; // miter with separate outputs
p->fSeqSimulate = 0; // performs sequential simulation
p->fVeryVerbose = 0; // verbose stats
p->fVerbose = 0; // verbose stats
}
-
+
+/**Function************ *************************************************
+
+ Synopsis [This procedure sets default parameters.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cec_ManSmfSetDefaultParams( Cec_ParSmf_t * p )
+{
+ memset( p, 0, sizeof(Cec_ParSmf_t) );
+ p->nWords = 15; // the number of simulation words
+ p->nRounds = 15; // the number of simulation rounds
+ p->nFrames = 2; // the number of time frames
+ p->nBTLimit = 1000; // conflict limit at a node
+ p->TimeLimit = 0; // the runtime limit in seconds
+ p->fDualOut = 0; // miter with separate outputs
+ p->fCheckMiter = 0; // the circuit is the miter
+ p->fFirstStop = 0; // stop on the first sat output
+ p->fVerbose = 0; // verbose stats
+}
+
/**Function************ *************************************************
Synopsis [This procedure sets default parameters.]
@@ -100,7 +125,7 @@ void Cec_ManFraSetDefaultParams( Cec_ParFra_t * p )
p->fRewriting = 0; // enables AIG rewriting
p->fCheckMiter = 0; // the circuit is the miter
p->fFirstStop = 0; // stop on the first sat output
- p->fDoubleOuts = 0; // miter with separate outputs
+ p->fDualOut = 0; // miter with separate outputs
p->fColorDiff = 0; // miter with separate outputs
p->fVeryVerbose = 0; // verbose stats
p->fVerbose = 0; // verbose stats
@@ -177,7 +202,8 @@ void Cec_ManSimulation( Gia_Man_t * pAig, Cec_ParSim_t * pPars )
if ( pPars->fCheckMiter )
printf( "The number of failed outputs of the miter = %6d. (Words = %4d. Rounds = %4d.)\n",
pSim->iOut, pSim->nOuts, pPars->nWords, pPars->nRounds );
- ABC_PRT( "Time", clock() - clkTotal );
+ if ( pPars->fVerbose )
+ ABC_PRT( "Time", clock() - clkTotal );
Cec_ManSimStop( pSim );
}
@@ -213,7 +239,7 @@ Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars )
// prepare the managers
// SAT sweeping
p = Cec_ManFraStart( pIni, pPars );
- if ( pPars->fDoubleOuts )
+ if ( pPars->fDualOut )
pPars->fColorDiff = 1;
// simulation
Cec_ManSimSetDefaultParams( pParsSim );
@@ -221,10 +247,9 @@ Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars )
pParsSim->nRounds = pPars->nRounds;
pParsSim->fCheckMiter = pPars->fCheckMiter;
pParsSim->fFirstStop = pPars->fFirstStop;
- pParsSim->fDoubleOuts = pPars->fDoubleOuts;
+ pParsSim->fDualOut = pPars->fDualOut;
pParsSim->fVerbose = pPars->fVerbose;
pSim = Cec_ManSimStart( p->pAig, pParsSim );
- pSim->nWords = p->pPars->nWords;
// SAT solving
Cec_ManSatSetDefaultParams( pParsSat );
pParsSat->nBTLimit = pPars->nBTLimit;
@@ -250,7 +275,7 @@ p->timeSim += clock() - clk;
{
clk2 = clock();
nMatches = 0;
- if ( pPars->fDoubleOuts )
+ if ( pPars->fDualOut )
{
nMatches = Gia_ManEquivSetColors( p->pAig, pPars->fVeryVerbose );
// p->pAig->pIso = Cec_ManDetectIsomorphism( p->pAig );
@@ -264,7 +289,7 @@ p->timeSim += clock() - clk;
Gia_ManStop( pSrm );
if ( p->pPars->fVerbose )
printf( "Considered all available candidate equivalences.\n" );
- if ( pPars->fDoubleOuts && Gia_ManAndNum(p->pAig) > 0 )
+ if ( pPars->fDualOut && Gia_ManAndNum(p->pAig) > 0 )
{
if ( pPars->fColorDiff )
{
@@ -276,7 +301,7 @@ p->timeSim += clock() - clk;
{
if ( p->pPars->fVerbose )
printf( "Switching into normal mode.\n" );
- pPars->fDoubleOuts = 0;
+ pPars->fDualOut = 0;
}
continue;
}
@@ -295,7 +320,7 @@ p->timeSat += clock() - clk;
Gia_ManStop( pSrm );
// update the manager
- pSim->pAig = p->pAig = Gia_ManEquivReduceAndRemap( pTemp = p->pAig, 0, pParsSim->fDoubleOuts );
+ pSim->pAig = p->pAig = Gia_ManEquivReduceAndRemap( pTemp = p->pAig, 0, pParsSim->fDualOut );
Gia_ManStop( pTemp );
if ( p->pPars->fVerbose )
{
@@ -332,18 +357,18 @@ p->timeSat += clock() - clk;
}
}
}
- if ( pPars->fDoubleOuts && pPars->fColorDiff && Gia_ManAndNum(p->pAig) < 100000 )
+ if ( pPars->fDualOut && pPars->fColorDiff && Gia_ManAndNum(p->pAig) < 100000 )
{
if ( p->pPars->fVerbose )
printf( "Switching into reduced mode.\n" );
pPars->fColorDiff = 0;
}
- if ( pPars->fDoubleOuts && Gia_ManAndNum(p->pAig) < 20000 )
+ if ( pPars->fDualOut && Gia_ManAndNum(p->pAig) < 20000 )
{
if ( p->pPars->fVerbose )
printf( "Switching into normal mode.\n" );
pPars->fColorDiff = 0;
- pPars->fDoubleOuts = 0;
+ pPars->fDualOut = 0;
}
}
finalize:
diff --git a/src/aig/cec/cecInt.h b/src/aig/cec/cecInt.h
index 1898b07c..ae4c6ff4 100644
--- a/src/aig/cec/cecInt.h
+++ b/src/aig/cec/cecInt.h
@@ -117,13 +117,17 @@ struct Cec_ManSim_t_
int nMemsMax; // the max number of used entries
int MemFree; // next free entry
int nWordsOld; // the number of simulation words after previous relink
- // bug catcher
+ // internal simulation info
Vec_Ptr_t * vCiSimInfo; // CI simulation info
Vec_Ptr_t * vCoSimInfo; // CO simulation info
+ // counter examples
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
+ // scoring simulation patterns
+ int * pScores; // counters of refinement for each pattern
// temporaries
Vec_Int_t * vClassOld; // old class numbers
Vec_Int_t * vClassNew; // new class numbers
@@ -182,6 +186,7 @@ extern Vec_Ptr_t * Cec_ManPatCollectPatterns( Cec_ManPat_t * pMan, int
/*=== cecSolve.c ============================================================*/
extern int Cec_ObjSatVarValue( Cec_ManSat_t * p, Gia_Obj_t * pObj );
extern void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars );
+extern void Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat_t * pPars, int nRegs, int * pnPats );
/*=== ceFraeep.c ============================================================*/
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 );
diff --git a/src/aig/cec/cecMan.c b/src/aig/cec/cecMan.c
index 1a94409f..14f2493e 100644
--- a/src/aig/cec/cecMan.c
+++ b/src/aig/cec/cecMan.c
@@ -193,6 +193,7 @@ Cec_ManSim_t * Cec_ManSimStart( Gia_Man_t * pAig, Cec_ParSim_t * pPars )
memset( p, 0, sizeof(Cec_ManSim_t) );
p->pAig = pAig;
p->pPars = pPars;
+ p->nWords = pPars->nWords;
p->pSimInfo = ABC_CALLOC( int, Gia_ManObjNum(pAig) );
p->vClassOld = Vec_IntAlloc( 1000 );
p->vClassNew = Vec_IntAlloc( 1000 );
@@ -229,6 +230,7 @@ void Cec_ManSimStop( Cec_ManSim_t * p )
Vec_PtrFree( p->vCiSimInfo );
if ( p->vCoSimInfo )
Vec_PtrFree( p->vCoSimInfo );
+ ABC_FREE( p->pScores );
ABC_FREE( p->pCexComb );
ABC_FREE( p->pCexes );
ABC_FREE( p->pMems );
diff --git a/src/aig/cec/cecSeq.c b/src/aig/cec/cecSeq.c
new file mode 100644
index 00000000..6cb229ae
--- /dev/null
+++ b/src/aig/cec/cecSeq.c
@@ -0,0 +1,314 @@
+/**CFile****************************************************************
+
+ FileName [cecSeq.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Combinatinoal equivalence checking.]
+
+ Synopsis [Refinement of sequential equivalence classes.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: cecSeq.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cecInt.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Sets register values from the counter-example.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cec_ManSeqDeriveInfoFromCex( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Gia_Cex_t * pCex )
+{
+ unsigned * pInfo;
+ int k, w, nWords;
+ assert( pCex->nBits == pCex->nRegs + pCex->nPis * (pCex->iFrame + 1) );
+ assert( pCex->nBits <= Vec_PtrSize(vInfo) );
+ nWords = Vec_PtrReadWordsSimInfo( vInfo );
+ for ( k = 0; k < pCex->nRegs; k++ )
+ {
+ pInfo = Vec_PtrEntry( vInfo, k );
+ for ( w = 0; w < nWords; w++ )
+ pInfo[w] = Aig_InfoHasBit( pCex->pData, k )? ~0 : 0;
+ }
+ for ( ; k < pCex->nBits; k++ )
+ {
+ pInfo = Vec_PtrEntry( vInfo, k );
+ for ( w = 0; w < nWords; w++ )
+ pInfo[w] = Aig_ManRandom(0);
+ // set simulation pattern and make sure it is second (first will be erased during simulation)
+ pInfo[0] = (pInfo[0] << 1) | Aig_InfoHasBit( pCex->pData, k );
+ pInfo[0] <<= 1;
+ }
+ for ( ; k < Vec_PtrSize(vInfo); k++ )
+ {
+ pInfo = Vec_PtrEntry( vInfo, k );
+ for ( w = 0; w < nWords; w++ )
+ pInfo[w] = Aig_ManRandom(0);
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Sets register values from the counter-example.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cec_ManSeqDeriveInfoInitRandom( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Gia_Cex_t * pCex )
+{
+ unsigned * pInfo;
+ int k, w, nWords;
+ nWords = Vec_PtrReadWordsSimInfo( vInfo );
+ assert( Gia_ManRegNum(pAig) == pCex->nRegs );
+ assert( Gia_ManRegNum(pAig) <= Vec_PtrSize(vInfo) );
+ for ( k = 0; k < Gia_ManRegNum(pAig); k++ )
+ {
+ pInfo = Vec_PtrEntry( vInfo, k );
+ for ( w = 0; w < nWords; w++ )
+ pInfo[w] = Aig_InfoHasBit( pCex->pData, k )? ~0 : 0;
+ }
+
+ for ( ; k < Vec_PtrSize(vInfo); k++ )
+ {
+ pInfo = Vec_PtrEntry( vInfo, k );
+ for ( w = 0; w < nWords; w++ )
+ pInfo[w] = Aig_ManRandom( 0 );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Resimulates the classes using sequential simulation info.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Cec_ManSeqResimulate( Cec_ManSim_t * p, Vec_Ptr_t * vInfo )
+{
+ unsigned * pInfo0, * pInfo1;
+ int f, i, k, w, RetValue = 0;
+ assert( Gia_ManRegNum(p->pAig) > 0 );
+ assert( Vec_PtrSize(vInfo) == Gia_ManRegNum(p->pAig) + Gia_ManPiNum(p->pAig) * p->pPars->nRounds );
+ for ( k = 0; k < Gia_ManRegNum(p->pAig); k++ )
+ {
+ pInfo0 = Vec_PtrEntry( vInfo, k );
+ pInfo1 = Vec_PtrEntry( p->vCoSimInfo, Gia_ManPoNum(p->pAig) + k );
+ for ( w = 0; w < p->nWords; w++ )
+ pInfo1[w] = pInfo0[w];
+ }
+ for ( f = 0; f < p->pPars->nRounds; f++ )
+ {
+ for ( i = 0; i < Gia_ManPiNum(p->pAig); i++ )
+ {
+ pInfo0 = Vec_PtrEntry( vInfo, k++ );
+ pInfo1 = 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 );
+ for ( w = 0; w < p->nWords; w++ )
+ pInfo1[w] = pInfo0[w];
+ }
+ if ( Cec_ManSimSimulateRound( p, p->vCiSimInfo, p->vCoSimInfo ) )
+ {
+ printf( "One of the outputs of the miter is asserted.\n" );
+ RetValue = 1;
+ }
+ }
+ assert( k == Vec_PtrSize(vInfo) );
+ return RetValue;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Resimulates information to refine equivalence classes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Cec_ManSeqResimulateInfo( Gia_Man_t * pAig, Vec_Ptr_t * vSimInfo, Gia_Cex_t * pBestState )
+{
+ Cec_ParSim_t ParsSim, * pParsSim = &ParsSim;
+ Cec_ManSim_t * pSim;
+ int RetValue, clkTotal = clock();
+ assert( (Vec_PtrSize(vSimInfo) - Gia_ManRegNum(pAig)) % Gia_ManPiNum(pAig) == 0 );
+ Cec_ManSimSetDefaultParams( pParsSim );
+ pParsSim->nRounds = (Vec_PtrSize(vSimInfo) - Gia_ManRegNum(pAig)) / Gia_ManPiNum(pAig);
+ pParsSim->nWords = Vec_PtrReadWordsSimInfo( vSimInfo );
+ Gia_ManSetRefs( pAig );
+ pSim = Cec_ManSimStart( pAig, pParsSim );
+ if ( pBestState )
+ pSim->pBestState = pBestState;
+ RetValue = Cec_ManSeqResimulate( pSim, vSimInfo );
+ pSim->pBestState = NULL;
+ Cec_ManSimStop( pSim );
+ return RetValue;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Resimuates one counter-example to refine equivalence classes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Cec_ManSeqResimulateCounter( Gia_Man_t * pAig, Cec_ParSim_t * pPars, Gia_Cex_t * pCex )
+{
+ Vec_Ptr_t * vSimInfo;
+ int RetValue, clkTotal = clock();
+ if ( pCex == NULL )
+ {
+ printf( "Cec_ManSeqResimulateCounter(): Counter-example is not available.\n" );
+ return -1;
+ }
+ if ( pAig->pReprs == NULL )
+ {
+ printf( "Cec_ManSeqResimulateCounter(): Equivalence classes are not available.\n" );
+ return -1;
+ }
+ if ( Gia_ManRegNum(pAig) == 0 )
+ {
+ printf( "Cec_ManSeqResimulateCounter(): Not a sequential AIG.\n" );
+ return -1;
+ }
+ if ( Gia_ManRegNum(pAig) != pCex->nRegs || Gia_ManPiNum(pAig) != pCex->nPis )
+ {
+ printf( "Cec_ManSeqResimulateCounter(): Parameters of the ccounter-example differ.\n" );
+ return -1;
+ }
+ if ( pPars->fVerbose )
+ printf( "Resimulating %d timeframes.\n", pPars->nRounds + pCex->iFrame + 1 );
+ Aig_ManRandom( 1 );
+ vSimInfo = Vec_PtrAllocSimInfo( Gia_ManRegNum(pAig) +
+ Gia_ManPiNum(pAig) * (pPars->nRounds + pCex->iFrame + 1), 1 );
+ Cec_ManSeqDeriveInfoFromCex( vSimInfo, pAig, pCex );
+ if ( pPars->fVerbose )
+ Gia_ManEquivPrintClasses( pAig, 0, 0 );
+ RetValue = Cec_ManSeqResimulateInfo( pAig, vSimInfo, NULL );
+ if ( pPars->fVerbose )
+ Gia_ManEquivPrintClasses( pAig, 0, 0 );
+ Vec_PtrFree( vSimInfo );
+ if ( pPars->fVerbose )
+ ABC_PRT( "Time", clock() - clkTotal );
+ return RetValue;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Performs semiformal refinement of equivalence classes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars )
+{
+ int nAddFrames = 10; // additional timeframes to simulate
+ Cec_ParSat_t ParsSat, * pParsSat = &ParsSat;
+ Vec_Ptr_t * vSimInfo;
+ Gia_Cex_t * pState;
+ Gia_Man_t * pSrm;
+ int r, nPats, RetValue = -1;
+ if ( pAig->pReprs == NULL )
+ {
+ printf( "Cec_ManSeqSemiformal(): Equivalence classes are not available.\n" );
+ return -1;
+ }
+ if ( Gia_ManRegNum(pAig) == 0 )
+ {
+ printf( "Cec_ManSeqSemiformal(): Not a sequential AIG.\n" );
+ return -1;
+ }
+ Aig_ManRandom( 1 );
+ // prepare starting pattern
+ pState = Gia_ManAllocCounterExample( Gia_ManRegNum(pAig), 0, 0 );
+ pState->iFrame = -1;
+ pState->iPo = -1;
+ // prepare SAT solving
+ Cec_ManSatSetDefaultParams( pParsSat );
+ pParsSat->nBTLimit = pPars->nBTLimit;
+ pParsSat->fVerbose = pPars->fVerbose;
+ if ( pParsSat->fVerbose )
+ {
+ printf( "Starting: " );
+ Gia_ManEquivPrintClasses( pAig, 0, 0 );
+ }
+ // perform the given number of BMC rounds
+ for ( r = 0; r < pPars->nRounds; r++ )
+ {
+// Gia_ManPrintCounterExample( pState );
+ // derive speculatively reduced model
+ pSrm = Gia_ManSpecReduceInit( pAig, pState, pPars->nFrames, pPars->fDualOut );
+ assert( Gia_ManRegNum(pSrm) == 0 && Gia_ManPiNum(pSrm) == Gia_ManPiNum(pAig) * pPars->nFrames );
+ // allocate room for simulation info
+ vSimInfo = Vec_PtrAllocSimInfo( Gia_ManRegNum(pAig) +
+ Gia_ManPiNum(pAig) * (pPars->nFrames + nAddFrames), pPars->nWords );
+ Cec_ManSeqDeriveInfoInitRandom( vSimInfo, pAig, pState );
+ // fill in simulation info with counter-examples
+ Cec_ManSatSolveSeq( vSimInfo, pSrm, pParsSat, Gia_ManRegNum(pAig), &nPats );
+ Gia_ManStop( pSrm );
+ // resimulate and refine the classes
+ RetValue = Cec_ManSeqResimulateInfo( pAig, vSimInfo, pState );
+ Vec_PtrFree( vSimInfo );
+ assert( pState->iPo >= 0 ); // hit counter
+ pState->iPo = -1;
+ if ( pPars->fVerbose )
+ {
+ printf( "BMC = %3d ", nPats );
+ Gia_ManEquivPrintClasses( pAig, 0, 0 );
+ }
+ }
+ ABC_FREE( pState );
+ return RetValue;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/cec/cecSolve.c b/src/aig/cec/cecSolve.c
index ba4b0477..2b6997e1 100644
--- a/src/aig/cec/cecSolve.c
+++ b/src/aig/cec/cecSolve.c
@@ -630,6 +630,85 @@ ABC_PRT( "time", clock() - clk2 );
Cec_ManSatStop( p );
}
+
+
+/**Function*************************************************************
+
+ Synopsis [Save values in the cone of influence.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+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_ObjIsTravIdCurrent(p, pObj) )
+ return;
+ Gia_ObjSetTravIdCurrent(p, pObj);
+ if ( Gia_ObjIsCi(pObj) )
+ {
+ unsigned * pInfo = Vec_PtrEntry( vInfo, nRegs + Gia_ObjCioId(pObj) );
+ if ( Cec_ObjSatVarValue( pSat, pObj ) != Aig_InfoHasBit( pInfo, iPat ) )
+ Aig_InfoXorBit( pInfo, iPat );
+ return;
+ }
+ assert( Gia_ObjIsAnd(pObj) );
+ Cec_ManSatSolveSeq_rec( pSat, p, Gia_ObjFanin0(pObj), vInfo, iPat, nRegs );
+ Cec_ManSatSolveSeq_rec( pSat, p, Gia_ObjFanin1(pObj), vInfo, iPat, nRegs );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs one round of solving for the POs of the AIG.]
+
+ Description [Labels the nodes that have been proved (pObj->fMark1)
+ and returns the set of satisfying assignments.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat_t * pPars, int nRegs, int * pnPats )
+{
+ Bar_Progress_t * pProgress = NULL;
+ Cec_ManSat_t * p;
+ Gia_Obj_t * pObj;
+ int iPat = 1, nPats = 32 * Vec_PtrReadWordsSimInfo(vPatts);
+ int i, status, clk = clock();
+ Gia_ManSetPhase( pAig );
+ Gia_ManLevelNum( pAig );
+ Gia_ManResetTravId( pAig );
+ p = Cec_ManSatCreate( pAig, pPars );
+ pProgress = Bar_ProgressStart( stdout, Gia_ManPoNum(pAig) );
+ Gia_ManForEachCo( pAig, pObj, i )
+ {
+ if ( Gia_ObjIsConst0(Gia_ObjFanin0(pObj)) )
+ continue;
+ Bar_ProgressUpdate( pProgress, i, "BMC..." );
+ status = Cec_ManSatCheckNode( p, pObj );
+ if ( status != 0 )
+ continue;
+ // save the pattern
+ Gia_ManIncrementTravId( pAig );
+ Cec_ManSatSolveSeq_rec( p, pAig, Gia_ObjFanin0(pObj), vPatts, iPat++, nRegs );
+ if ( iPat == nPats )
+ break;
+ // quit if one of them is solved
+ if ( pPars->fFirstStop )
+ break;
+ }
+ p->timeTotal = clock() - clk;
+ Bar_ProgressStop( pProgress );
+// Cec_ManSatPrintStats( p );
+ Cec_ManSatStop( p );
+ if ( pnPats )
+ *pnPats = iPat-1;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/cec/cecSweep.c b/src/aig/cec/cecSweep.c
index 20a668bd..3024ac24 100644
--- a/src/aig/cec/cecSweep.c
+++ b/src/aig/cec/cecSweep.c
@@ -83,7 +83,7 @@ Gia_Man_t * Cec_ManFraSpecReduction( Cec_ManFra_t * p )
(Gia_ObjLevel(p->pAig, pObj) > p->pPars->nLevelMax ||
Gia_ObjLevel(p->pAig, pRepr) > p->pPars->nLevelMax) )
continue;
- if ( p->pPars->fDoubleOuts )
+ if ( p->pPars->fDualOut )
{
// if ( i % 1000 == 0 && Gia_ObjRepr(p->pAig, i) )
// Gia_ManEquivPrintOne( p->pAig, Gia_ObjRepr(p->pAig, i), 0 );
diff --git a/src/aig/cec/module.make b/src/aig/cec/module.make
index 4618c424..1fc9861c 100644
--- a/src/aig/cec/module.make
+++ b/src/aig/cec/module.make
@@ -4,6 +4,7 @@ SRC += src/aig/cec/cecCec.c \
src/aig/cec/cecIso.c \
src/aig/cec/cecMan.c \
src/aig/cec/cecPat.c \
+ src/aig/cec/cecSeq.c \
src/aig/cec/cecSim.c \
src/aig/cec/cecSolve.c \
src/aig/cec/cecSweep.c
diff --git a/src/aig/cec2/cec.h b/src/aig/cec2/cec.h
deleted file mode 100644
index 3586b535..00000000
--- a/src/aig/cec2/cec.h
+++ /dev/null
@@ -1,104 +0,0 @@
-/**CFile****************************************************************
-
- FileName [cec.h]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [Combinatinoal equivalence checking.]
-
- Synopsis [External declarations.]
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - June 20, 2005.]
-
- Revision [$Id: cec.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#ifndef __CEC_H__
-#define __CEC_H__
-
-////////////////////////////////////////////////////////////////////////
-/// INCLUDES ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// PARAMETERS ///
-////////////////////////////////////////////////////////////////////////
-
-#ifdef __cplusplus
-extern "C" {
-#endif
-
-////////////////////////////////////////////////////////////////////////
-/// BASIC TYPES ///
-////////////////////////////////////////////////////////////////////////
-
-// dynamic SAT parameters
-typedef struct Cec_ParSat_t_ Cec_ParSat_t;
-struct Cec_ParSat_t_
-{
- int nBTLimit; // conflict limit at a node
- int nSatVarMax; // the max number of SAT variables
- int nCallsRecycle; // calls to perform before recycling SAT solver
- int fFirstStop; // stop on the first sat output
- int fPolarFlip; // uses polarity adjustment
- int fVerbose; // verbose stats
-};
-
-// combinational SAT sweeping parameters
-typedef struct Cec_ParCsw_t_ Cec_ParCsw_t;
-struct Cec_ParCsw_t_
-{
- int nWords; // the number of simulation words
- int nRounds; // the number of simulation rounds
- int nBTLimit; // conflict limit at a node
- int nSatVarMax; // the max number of SAT variables
- int nCallsRecycle; // calls to perform before recycling SAT solver
- int nLevelMax; // restriction on the level nodes to be swept
- int fRewriting; // enables AIG rewriting
- int fFirstStop; // stop on the first sat output
- int fVerbose; // verbose stats
-};
-
-// combinational equivalence checking parameters
-typedef struct Cec_ParCec_t_ Cec_ParCec_t;
-struct Cec_ParCec_t_
-{
- int nIters; // iterations of SAT solving/sweeping
- int nBTLimitBeg; // starting backtrack limit
- int nBTlimitMulti; // multiple of backtrack limit
- int fUseSmartCnf; // use smart CNF computation
- int fRewriting; // enables AIG rewriting
- int fSatSweeping; // enables SAT sweeping
- int fFirstStop; // stop on the first sat output
- int fVerbose; // verbose stats
-};
-
-////////////////////////////////////////////////////////////////////////
-/// MACRO DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/*=== cecCore.c ==========================================================*/
-extern void Cec_ManSatSetDefaultParams( Cec_ParSat_t * p );
-extern void Cec_ManCswSetDefaultParams( Cec_ParCsw_t * p );
-extern void Cec_ManCecSetDefaultParams( Cec_ParCec_t * p );
-extern int Cec_Solve( Aig_Man_t * pAig0, Aig_Man_t * pAig1, Cec_ParCec_t * p );
-
-#ifdef __cplusplus
-}
-#endif
-
-#endif
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
diff --git a/src/aig/cec2/cecAig.c b/src/aig/cec2/cecAig.c
deleted file mode 100644
index c322ead8..00000000
--- a/src/aig/cec2/cecAig.c
+++ /dev/null
@@ -1,168 +0,0 @@
-/**CFile****************************************************************
-
- FileName [cecAig.c]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [Combinatinoal equivalence checking.]
-
- Synopsis [AIG manipulation.]
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - June 20, 2005.]
-
- Revision [$Id: cecAig.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "cecInt.h"
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis [Derives combinational miter of the two AIGs.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Aig_Obj_t * Cec_DeriveMiter_rec( Aig_Man_t * pNew, Aig_Obj_t * pObj )
-{
- if ( pObj->pData )
- return pObj->pData;
- if ( Aig_ObjIsPi(pObj) )
- {
- pObj->pData = Aig_ObjCreatePi( pNew );
- if ( pObj->pHaig )
- {
- assert( pObj->pHaig->pData == NULL );
- pObj->pHaig->pData = pObj->pData;
- }
- return pObj->pData;
- }
- assert( Aig_ObjIsNode(pObj) );
- Cec_DeriveMiter_rec( pNew, Aig_ObjFanin0(pObj) );
- Cec_DeriveMiter_rec( pNew, Aig_ObjFanin1(pObj) );
- pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
- return pObj->pData;
-}
-
-/**Function*************************************************************
-
- Synopsis [Derives combinational miter of the two AIGs.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Aig_Man_t * Cec_DeriveMiter( Aig_Man_t * p0, Aig_Man_t * p1 )
-{
- Bar_Progress_t * pProgress = NULL;
- Aig_Man_t * pNew;
- Aig_Obj_t * pObj0, * pObj1, * pObjNew;
- int i;
- assert( Aig_ManPiNum(p0) == Aig_ManPiNum(p1) );
- assert( Aig_ManPoNum(p0) == Aig_ManPoNum(p1) );
- // create the new manager
- pNew = Aig_ManStart( Aig_ManNodeNum(p0) + Aig_ManNodeNum(p1) );
- pNew->pName = Aig_UtilStrsav( p0->pName );
- // create the PIs
- Aig_ManCleanData( p0 );
- Aig_ManCleanData( p1 );
- Aig_ManConst1(p0)->pData = Aig_ManConst1(pNew);
- Aig_ManConst1(p1)->pData = Aig_ManConst1(pNew);
- Aig_ManForEachPi( p0, pObj0, i )
- {
- pObj1 = Aig_ManPi( p1, i );
- pObj0->pHaig = pObj1;
- pObj1->pHaig = pObj0;
- if ( Aig_ObjRefs(pObj0) || Aig_ObjRefs(pObj1) )
- continue;
- pObjNew = Aig_ObjCreatePi( pNew );
- pObj0->pData = pObjNew;
- pObj1->pData = pObjNew;
- }
- // add logic for the POs
- pProgress = Bar_ProgressStart( stdout, Aig_ManPoNum(p0) );
- Aig_ManForEachPo( p0, pObj0, i )
- {
- Bar_ProgressUpdate( pProgress, i, "Miter..." );
- pObj1 = Aig_ManPo( p1, i );
- Cec_DeriveMiter_rec( pNew, Aig_ObjFanin0(pObj0) );
- Cec_DeriveMiter_rec( pNew, Aig_ObjFanin0(pObj1) );
- pObjNew = Aig_Exor( pNew, Aig_ObjChild0Copy(pObj0), Aig_ObjChild0Copy(pObj1) );
- Aig_ObjCreatePo( pNew, pObjNew );
- }
- Bar_ProgressStop( pProgress );
- Aig_ManSetRegNum( pNew, 0 );
- assert( Aig_ManHasNoGaps(pNew) );
- return pNew;
-}
-
-/**Function*************************************************************
-
- Synopsis [Duplicates AIG in the DFS order.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Aig_Man_t * Cec_Duplicate( Aig_Man_t * p )
-{
- Bar_Progress_t * pProgress = NULL;
- Aig_Man_t * pNew;
- Aig_Obj_t * pObj;
- int i;
- // make sure the AIG does not have choices and dangling nodes
- Aig_ManForEachNode( p, pObj, i )
- assert( Aig_ObjRefs(pObj) > 0 );
- // create the new manager
- pNew = Aig_ManStart( Aig_ManNodeNum(p) );
- pNew->pName = Aig_UtilStrsav( p->pName );
- // create the PIs
- Aig_ManCleanData( p );
- Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
- Aig_ManForEachPi( p, pObj, i )
- {
- pObj->pHaig = NULL;
- if ( Aig_ObjRefs(pObj) == 0 )
- pObj->pData = Aig_ObjCreatePi( pNew );
- }
- // add logic for the POs
- pProgress = Bar_ProgressStart( stdout, Aig_ManPoNum(p) );
- Aig_ManForEachPo( p, pObj, i )
- {
- Bar_ProgressUpdate( pProgress, i, "Miter..." );
- Cec_DeriveMiter_rec( pNew, Aig_ObjFanin0(pObj) );
- Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
- }
- Bar_ProgressStop( pProgress );
- Aig_ManSetRegNum( pNew, 0 );
- assert( Aig_ManHasNoGaps(pNew) );
- return pNew;
-}
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/aig/cec2/cecClass.c b/src/aig/cec2/cecClass.c
deleted file mode 100644
index 24e40281..00000000
--- a/src/aig/cec2/cecClass.c
+++ /dev/null
@@ -1,571 +0,0 @@
-/**CFile****************************************************************
-
- FileName [cecClass.c]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [Combinatinoal equivalence checking.]
-
- Synopsis [Equivalence class representation.]
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - June 20, 2005.]
-
- Revision [$Id: cecClass.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "cecInt.h"
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Aig_Man_t * Caig_ManSpecReduce( Caig_Man_t * p, int nLevels )
-{
- Aig_Man_t * pAig;
- Aig_Obj_t ** pCopy;
- Aig_Obj_t * pRes0, * pRes1, * pRepr, * pNode;
- Aig_Obj_t * pMiter;
- int i;
- pAig = Aig_ManStart( p->nNodes );
- pCopy = ABC_ALLOC( Aig_Obj_t *, p->nObjs );
- pCopy[0] = Aig_ManConst1(pAig);
- for ( i = 1; i < p->nObjs; i++ )
- {
- if ( p->pFans0[i] == -1 ) // pi always has zero first fanin
- {
- pCopy[i] = Aig_ObjCreatePi( pAig );
- continue;
- }
- if ( p->pFans1[i] == -1 ) // po always has non-zero 1st fanin and zero 2nd fanin
- continue;
- pRes0 = Aig_NotCond( pCopy[Cec_Lit2Var(p->pFans0[i])], Cec_LitIsCompl(p->pFans0[i]) );
- pRes1 = Aig_NotCond( pCopy[Cec_Lit2Var(p->pFans1[i])], Cec_LitIsCompl(p->pFans1[i]) );
- pNode = pCopy[i] = Aig_And( pAig, pRes0, pRes1 );
- if ( p->pReprs[i] < 0 )
- continue;
- assert( p->pReprs[i] < i );
- pRepr = pCopy[p->pReprs[i]];
- if ( Aig_Regular(pNode) == Aig_Regular(pRepr) )
- continue;
- pCopy[i] = Aig_NotCond( pRepr, Aig_ObjPhaseReal(pRepr) ^ Aig_ObjPhaseReal(pNode) );
- if ( nLevels && ((int)Aig_Regular(pRepr)->Level > nLevels || (int)Aig_Regular(pNode)->Level > nLevels) )
- continue;
- pMiter = Aig_Exor( pAig, pNode, pRepr );
- Aig_ObjCreatePo( pAig, Aig_NotCond(pMiter, Aig_ObjPhaseReal(pMiter)) );
-// Aig_ObjCreatePo( pAig, Aig_Regular(pRepr) );
-// Aig_ObjCreatePo( pAig, Aig_Regular(pCopy[i]) );
- }
- ABC_FREE( pCopy );
- Aig_ManSetRegNum( pAig, 0 );
- Aig_ManCleanup( pAig );
- return pAig;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Caig_ManCountOne( Caig_Man_t * p, int i )
-{
- int Ent, nLits = 0;
- assert( p->pReprs[i] < 0 && p->pNexts[i] > 0 );
- for ( Ent = p->pNexts[i]; Ent; Ent = p->pNexts[Ent] )
- {
- assert( p->pReprs[Ent] == i );
- nLits++;
- }
- return 1 + nLits;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Caig_ManCountLiterals( Caig_Man_t * p )
-{
- int i, nLits = 0;
- for ( i = 1; i < p->nObjs; i++ )
- if ( p->pReprs[i] < 0 && p->pNexts[i] > 0 )
- nLits += Caig_ManCountOne(p, i) - 1;
- return nLits;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Caig_ManPrintOne( Caig_Man_t * p, int i, int Counter )
-{
- int Ent;
- printf( "Class %4d : Num = %2d {", Counter, Caig_ManCountOne(p, i) );
- for ( Ent = i; Ent; Ent = p->pNexts[Ent] )
- printf(" %d", Ent );
- printf( " }\n" );
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Caig_ManPrintClasses( Caig_Man_t * p, int fVerbose )
-{
- int i, Counter = 0, Counter1 = 0, CounterX = 0, nLits;
- for ( i = 1; i < p->nObjs; i++ )
- {
- if ( p->pReprs[i] < 0 && p->pNexts[i] > 0 )
- Counter++;
- if ( p->pReprs[i] == 0 )
- Counter1++;
- if ( p->pReprs[i] < 0 && p->pNexts[i] == 0 )
- CounterX++;
- }
- nLits = Caig_ManCountLiterals( p );
- printf( "Class = %6d. Const = %6d. Unsed = %6d. Lits = %7d. All = %7d. Mem = %5.2f Mb\n",
- Counter, Counter1, CounterX, nLits, nLits+Counter1, 1.0*p->nMemsMax/(1<<20) );
- if ( fVerbose )
- for ( i = 1; i < p->nObjs; i++ )
- if ( p->pReprs[i] < 0 && p->pNexts[i] > 0 )
- Caig_ManPrintOne( p, i, ++Counter );
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Caig_ManCollectSimsSimple( Caig_Man_t * p, int i )
-{
- int Ent;
- Vec_PtrClear( p->vSims );
- for ( Ent = i; Ent; Ent = p->pNexts[Ent] )
- Vec_PtrPush( p->vSims, p->pSims + Ent );
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Caig_ManCollectSimsNormal( Caig_Man_t * p, int i )
-{
- unsigned * pSim;
- int Ent;
- Vec_PtrClear( p->vSims );
- for ( Ent = i; Ent; Ent = p->pNexts[Ent] )
- {
- pSim = Caig_ManSimDeref( p, Ent );
- Vec_PtrPush( p->vSims, pSim + 1 );
- }
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Caig_ManCompareEqual( unsigned * p0, unsigned * p1, int nWords )
-{
- int w;
- if ( (p0[0] & 1) == (p1[0] & 1) )
- {
- for ( w = 0; w < nWords; w++ )
- if ( p0[w] != p1[w] )
- return 0;
- return 1;
- }
- else
- {
- for ( w = 0; w < nWords; w++ )
- if ( p0[w] != ~p1[w] )
- return 0;
- return 1;
- }
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Caig_ManCompareConst( unsigned * p, int nWords )
-{
- int w;
- if ( p[0] & 1 )
- {
- for ( w = 0; w < nWords; w++ )
- if ( p[w] != ~0 )
- return 0;
- return 1;
- }
- else
- {
- for ( w = 0; w < nWords; w++ )
- if ( p[w] != 0 )
- return 0;
- return 1;
- }
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Caig_ManClassCreate( Caig_Man_t * p, Vec_Int_t * vClass )
-{
- int * pNext, Repr, Ent, i;
- assert( Vec_IntSize(vClass) > 0 );
- Vec_IntForEachEntry( vClass, Ent, i )
- {
- if ( i == 0 )
- {
- Repr = Ent;
- p->pReprs[Ent] = -1;
- pNext = p->pNexts + Ent;
- }
- else
- {
- p->pReprs[Ent] = Repr;
- *pNext = Ent;
- pNext = p->pNexts + Ent;
- }
- }
- *pNext = 0;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Caig_ManClassRefineOne( Caig_Man_t * p, int i, Vec_Ptr_t * vSims )
-{
- unsigned * pSim0, * pSim1;
- int Ent, c = 0, d = 0;
- Vec_IntClear( p->vClassOld );
- Vec_IntClear( p->vClassNew );
- pSim0 = Vec_PtrEntry( vSims, c++ );
- Vec_IntPush( p->vClassOld, i );
- for ( Ent = p->pNexts[i]; Ent; Ent = p->pNexts[Ent] )
- {
- pSim1 = Vec_PtrEntry( vSims, c++ );
- if ( Caig_ManCompareEqual( pSim0, pSim1, p->nWords ) )
- Vec_IntPush( p->vClassOld, Ent );
- else
- {
- Vec_IntPush( p->vClassNew, Ent );
- Vec_PtrWriteEntry( vSims, d++, pSim1 );
- }
- }
-//if ( Vec_PtrSize(vSims) > 100 )
-//printf( "%d -> %d %d \n", Vec_PtrSize(vSims), Vec_IntSize(p->vClassOld), Vec_IntSize(p->vClassNew) );
- Vec_PtrShrink( vSims, d );
- if ( Vec_IntSize(p->vClassNew) == 0 )
- return 0;
- Caig_ManClassCreate( p, p->vClassOld );
- Caig_ManClassCreate( p, p->vClassNew );
- if ( Vec_IntSize(p->vClassNew) > 1 )
- return 1 + Caig_ManClassRefineOne( p, Vec_IntEntry(p->vClassNew,0), vSims );
- return 1;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Caig_ManHashKey( unsigned * pSim, int nWords, int nTableSize )
-{
- static int s_Primes[16] = {
- 1291, 1699, 1999, 2357, 2953, 3313, 3907, 4177,
- 4831, 5147, 5647, 6343, 6899, 7103, 7873, 8147 };
- unsigned uHash = 0;
- int i;
- if ( pSim[0] & 1 )
- for ( i = 0; i < nWords; i++ )
- uHash ^= ~pSim[i] * s_Primes[i & 0xf];
- else
- for ( i = 0; i < nWords; i++ )
- uHash ^= pSim[i] * s_Primes[i & 0xf];
- return (int)(uHash % nTableSize);
-
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Caig_ManClassesCreate( Caig_Man_t * p )
-{
- int * pTable, nTableSize, i, Key;
- nTableSize = Aig_PrimeCudd( 100 + p->nObjs / 10 );
- pTable = ABC_CALLOC( int, nTableSize );
- p->pReprs = ABC_ALLOC( int, p->nObjs );
- p->pNexts = ABC_CALLOC( int, p->nObjs );
- for ( i = 1; i < p->nObjs; i++ )
- {
- if ( p->pFans0[i] > 0 && p->pFans1[i] == -1 ) // po always has non-zero 1st fanin and zero 2nd fanin
- continue;
- if ( Caig_ManCompareConst( p->pSims + i, 1 ) )
- {
- p->pReprs[i] = 0;
- continue;
- }
- Key = Caig_ManHashKey( p->pSims + i, 1, nTableSize );
- if ( pTable[Key] == 0 )
- p->pReprs[i] = -1;
- else
- {
- p->pNexts[ pTable[Key] ] = i;
- p->pReprs[i] = p->pReprs[ pTable[Key] ];
- if ( p->pReprs[i] == -1 )
- p->pReprs[i] = pTable[Key];
- }
- pTable[Key] = i;
- }
- ABC_FREE( pTable );
-Caig_ManPrintClasses( p, 0 );
- // refine classes
- for ( i = 1; i < p->nObjs; i++ )
- if ( p->pReprs[i] < 0 && p->pNexts[i] > 0 )
- {
- Caig_ManCollectSimsSimple( p, i );
- Caig_ManClassRefineOne( p, i, p->vSims );
- }
- // clean memory
- memset( p->pSims, 0, sizeof(unsigned) * p->nObjs );
-Caig_ManPrintClasses( p, 0 );
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Caig_ManSimulateSimple( Caig_Man_t * p )
-{
- unsigned Res0, Res1;
- int i;
- for ( i = 1; i < p->nObjs; i++ )
- {
- if ( p->pFans0[i] == -1 ) // pi
- {
- p->pSims[i] = Aig_ManRandom( 0 );
- continue;
- }
- if ( p->pFans1[i] == -1 ) // po always has non-zero 1st fanin and zero 2nd fanin
- continue;
- Res0 = p->pSims[Cec_Lit2Var(p->pFans0[i])];
- Res1 = p->pSims[Cec_Lit2Var(p->pFans1[i])];
- p->pSims[i] = (Cec_LitIsCompl(p->pFans0[i]) ? ~Res0: Res0) &
- (Cec_LitIsCompl(p->pFans1[i]) ? ~Res1: Res1);
- }
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Caig_ManProcessRefined( Caig_Man_t * p, Vec_Int_t * vRefined )
-{
- Vec_Int_t * vClasses;
- int * pTable, nTableSize, i, Key, iNode;
- unsigned * pSim;
- if ( Vec_IntSize(vRefined) == 0 )
- return;
- nTableSize = Aig_PrimeCudd( 100 + Vec_IntSize(vRefined) / 5 );
- pTable = ABC_CALLOC( int, nTableSize );
- vClasses = Vec_IntAlloc( 100 );
- Vec_IntForEachEntry( vRefined, iNode, i )
- {
- pSim = Caig_ManSimRead( p, iNode );
- assert( !Caig_ManCompareConst( pSim + 1, p->nWords ) );
- Key = Caig_ManHashKey( pSim + 1, p->nWords, nTableSize );
- if ( pTable[Key] == 0 )
- {
- assert( p->pReprs[iNode] == 0 );
- assert( p->pNexts[iNode] == 0 );
- p->pReprs[iNode] = -1;
- Vec_IntPush( vClasses, iNode );
- }
- else
- {
- p->pNexts[ pTable[Key] ] = iNode;
- p->pReprs[iNode] = p->pReprs[ pTable[Key] ];
- if ( p->pReprs[iNode] == -1 )
- p->pReprs[iNode] = pTable[Key];
- assert( p->pReprs[iNode] > 0 );
- }
- pTable[Key] = iNode;
- }
- ABC_FREE( pTable );
- // refine classes
- Vec_IntForEachEntry( vClasses, iNode, i )
- {
- if ( p->pNexts[iNode] == 0 )
- {
- Caig_ManSimDeref( p, iNode );
- continue;
- }
- Caig_ManCollectSimsNormal( p, iNode );
- Caig_ManClassRefineOne( p, iNode, p->vSims );
- }
- Vec_IntFree( vClasses );
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Caig_Man_t * Caig_ManClassesPrepare( Aig_Man_t * pAig, int nWords, int nIters )
-{
- Vec_Ptr_t * vInfo;
- Caig_Man_t * p;
- int i;
- Aig_ManRandom( 1 );
- p = Caig_ManCreate( pAig );
- p->nWords = 1;
- Caig_ManSimulateSimple( p );
- Caig_ManClassesCreate( p );
- p->nWords = nWords;
- for ( i = 0; i < nIters; i++ )
- {
- p->nWords = i + 1;
- Caig_ManSimMemRelink( p );
- p->nMemsMax = 0;
-
- vInfo = Vec_PtrAllocSimInfo( p->nPis, p->nWords );
- Aig_ManRandomInfo( vInfo, 0, p->nWords );
- Caig_ManSimulateRound( p, vInfo, NULL );
- Vec_PtrFree( vInfo );
-Caig_ManPrintClasses( p, 0 );
- }
-
- p->nWords = nWords;
- Caig_ManSimMemRelink( p );
- p->nMemsMax = 0;
- return p;
-}
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/aig/cec2/cecCnf.c b/src/aig/cec2/cecCnf.c
deleted file mode 100644
index 706b15e0..00000000
--- a/src/aig/cec2/cecCnf.c
+++ /dev/null
@@ -1,328 +0,0 @@
-/**CFile****************************************************************
-
- FileName [cecCnf.c]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [Combinatinoal equivalence checking.]
-
- Synopsis [CNF computation.]
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - June 20, 2005.]
-
- Revision [$Id: cecCnf.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "cecInt.h"
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis [Addes clauses to the solver.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Cec_AddClausesMux( Cec_ManSat_t * p, Aig_Obj_t * pNode )
-{
- Aig_Obj_t * pNodeI, * pNodeT, * pNodeE;
- int pLits[4], RetValue, VarF, VarI, VarT, VarE, fCompT, fCompE;
-
- assert( !Aig_IsComplement( pNode ) );
- assert( Aig_ObjIsMuxType( pNode ) );
- // get nodes (I = if, T = then, E = else)
- pNodeI = Aig_ObjRecognizeMux( pNode, &pNodeT, &pNodeE );
- // get the variable numbers
- VarF = Cec_ObjSatNum(p,pNode);
- VarI = Cec_ObjSatNum(p,pNodeI);
- VarT = Cec_ObjSatNum(p,Aig_Regular(pNodeT));
- VarE = Cec_ObjSatNum(p,Aig_Regular(pNodeE));
- // get the complementation flags
- fCompT = Aig_IsComplement(pNodeT);
- fCompE = Aig_IsComplement(pNodeE);
-
- // f = ITE(i, t, e)
-
- // i' + t' + f
- // i' + t + f'
- // i + e' + f
- // i + e + f'
-
- // create four clauses
- pLits[0] = toLitCond(VarI, 1);
- pLits[1] = toLitCond(VarT, 1^fCompT);
- pLits[2] = toLitCond(VarF, 0);
- if ( p->pPars->fPolarFlip )
- {
- if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] );
- if ( Aig_Regular(pNodeT)->fPhase ) pLits[1] = lit_neg( pLits[1] );
- if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] );
- }
- RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
- assert( RetValue );
- pLits[0] = toLitCond(VarI, 1);
- pLits[1] = toLitCond(VarT, 0^fCompT);
- pLits[2] = toLitCond(VarF, 1);
- if ( p->pPars->fPolarFlip )
- {
- if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] );
- if ( Aig_Regular(pNodeT)->fPhase ) pLits[1] = lit_neg( pLits[1] );
- if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] );
- }
- RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
- assert( RetValue );
- pLits[0] = toLitCond(VarI, 0);
- pLits[1] = toLitCond(VarE, 1^fCompE);
- pLits[2] = toLitCond(VarF, 0);
- if ( p->pPars->fPolarFlip )
- {
- if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] );
- if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] );
- if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] );
- }
- RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
- assert( RetValue );
- pLits[0] = toLitCond(VarI, 0);
- pLits[1] = toLitCond(VarE, 0^fCompE);
- pLits[2] = toLitCond(VarF, 1);
- if ( p->pPars->fPolarFlip )
- {
- if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] );
- if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] );
- if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] );
- }
- RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
- assert( RetValue );
-
- // two additional clauses
- // t' & e' -> f'
- // t & e -> f
-
- // t + e + f'
- // t' + e' + f
-
- if ( VarT == VarE )
- {
-// assert( fCompT == !fCompE );
- return;
- }
-
- pLits[0] = toLitCond(VarT, 0^fCompT);
- pLits[1] = toLitCond(VarE, 0^fCompE);
- pLits[2] = toLitCond(VarF, 1);
- if ( p->pPars->fPolarFlip )
- {
- if ( Aig_Regular(pNodeT)->fPhase ) pLits[0] = lit_neg( pLits[0] );
- if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] );
- if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] );
- }
- RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
- assert( RetValue );
- pLits[0] = toLitCond(VarT, 1^fCompT);
- pLits[1] = toLitCond(VarE, 1^fCompE);
- pLits[2] = toLitCond(VarF, 0);
- if ( p->pPars->fPolarFlip )
- {
- if ( Aig_Regular(pNodeT)->fPhase ) pLits[0] = lit_neg( pLits[0] );
- if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] );
- if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] );
- }
- RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
- assert( RetValue );
-}
-
-/**Function*************************************************************
-
- Synopsis [Addes clauses to the solver.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Cec_AddClausesSuper( Cec_ManSat_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper )
-{
- Aig_Obj_t * pFanin;
- int * pLits, nLits, RetValue, i;
- assert( !Aig_IsComplement(pNode) );
- assert( Aig_ObjIsNode( pNode ) );
- // create storage for literals
- nLits = Vec_PtrSize(vSuper) + 1;
- pLits = ABC_ALLOC( int, nLits );
- // suppose AND-gate is A & B = C
- // add !A => !C or A + !C
- Vec_PtrForEachEntry( vSuper, pFanin, i )
- {
- pLits[0] = toLitCond(Cec_ObjSatNum(p,Aig_Regular(pFanin)), Aig_IsComplement(pFanin));
- pLits[1] = toLitCond(Cec_ObjSatNum(p,pNode), 1);
- if ( p->pPars->fPolarFlip )
- {
- if ( Aig_Regular(pFanin)->fPhase ) pLits[0] = lit_neg( pLits[0] );
- if ( pNode->fPhase ) pLits[1] = lit_neg( pLits[1] );
- }
- RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
- assert( RetValue );
- }
- // add A & B => C or !A + !B + C
- Vec_PtrForEachEntry( vSuper, pFanin, i )
- {
- pLits[i] = toLitCond(Cec_ObjSatNum(p,Aig_Regular(pFanin)), !Aig_IsComplement(pFanin));
- if ( p->pPars->fPolarFlip )
- {
- if ( Aig_Regular(pFanin)->fPhase ) pLits[i] = lit_neg( pLits[i] );
- }
- }
- pLits[nLits-1] = toLitCond(Cec_ObjSatNum(p,pNode), 0);
- if ( p->pPars->fPolarFlip )
- {
- if ( pNode->fPhase ) pLits[nLits-1] = lit_neg( pLits[nLits-1] );
- }
- RetValue = sat_solver_addclause( p->pSat, pLits, pLits + nLits );
- assert( RetValue );
- ABC_FREE( pLits );
-}
-
-/**Function*************************************************************
-
- Synopsis [Collects the supergate.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Cec_CollectSuper_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int fUseMuxes )
-{
- // if the new node is complemented or a PI, another gate begins
- if ( Aig_IsComplement(pObj) || Aig_ObjIsPi(pObj) ||
- (!fFirst && Aig_ObjRefs(pObj) > 1) ||
- (fUseMuxes && Aig_ObjIsMuxType(pObj)) )
- {
- Vec_PtrPushUnique( vSuper, pObj );
- return;
- }
- // go through the branches
- Cec_CollectSuper_rec( Aig_ObjChild0(pObj), vSuper, 0, fUseMuxes );
- Cec_CollectSuper_rec( Aig_ObjChild1(pObj), vSuper, 0, fUseMuxes );
-}
-
-/**Function*************************************************************
-
- Synopsis [Collects the supergate.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Cec_CollectSuper( Aig_Obj_t * pObj, int fUseMuxes, Vec_Ptr_t * vSuper )
-{
- assert( !Aig_IsComplement(pObj) );
- assert( !Aig_ObjIsPi(pObj) );
- Vec_PtrClear( vSuper );
- Cec_CollectSuper_rec( pObj, vSuper, 1, fUseMuxes );
-}
-
-/**Function*************************************************************
-
- Synopsis [Updates the solver clause database.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Cec_ObjAddToFrontier( Cec_ManSat_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vFrontier )
-{
- assert( !Aig_IsComplement(pObj) );
- if ( Cec_ObjSatNum(p,pObj) )
- return;
- assert( Cec_ObjSatNum(p,pObj) == 0 );
- if ( Aig_ObjIsConst1(pObj) )
- return;
- Vec_PtrPush( p->vUsedNodes, pObj );
- Cec_ObjSetSatNum( p, pObj, p->nSatVars++ );
- if ( Aig_ObjIsNode(pObj) )
- Vec_PtrPush( vFrontier, pObj );
-}
-
-/**Function*************************************************************
-
- Synopsis [Updates the solver clause database.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Cec_CnfNodeAddToSolver( Cec_ManSat_t * p, Aig_Obj_t * pObj )
-{
- Vec_Ptr_t * vFrontier;
- Aig_Obj_t * pNode, * pFanin;
- int i, k, fUseMuxes = 1;
- // quit if CNF is ready
- if ( Cec_ObjSatNum(p,pObj) )
- return;
- // start the frontier
- vFrontier = Vec_PtrAlloc( 100 );
- Cec_ObjAddToFrontier( p, pObj, vFrontier );
- // explore nodes in the frontier
- Vec_PtrForEachEntry( vFrontier, pNode, i )
- {
- // create the supergate
- assert( Cec_ObjSatNum(p,pNode) );
- if ( fUseMuxes && Aig_ObjIsMuxType(pNode) )
- {
- Vec_PtrClear( p->vFanins );
- Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin0( Aig_ObjFanin0(pNode) ) );
- Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin0( Aig_ObjFanin1(pNode) ) );
- Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin1( Aig_ObjFanin0(pNode) ) );
- Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin1( Aig_ObjFanin1(pNode) ) );
- Vec_PtrForEachEntry( p->vFanins, pFanin, k )
- Cec_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier );
- Cec_AddClausesMux( p, pNode );
- }
- else
- {
- Cec_CollectSuper( pNode, fUseMuxes, p->vFanins );
- Vec_PtrForEachEntry( p->vFanins, pFanin, k )
- Cec_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier );
- Cec_AddClausesSuper( p, pNode, p->vFanins );
- }
- assert( Vec_PtrSize(p->vFanins) > 1 );
- }
- Vec_PtrFree( vFrontier );
-}
-
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/aig/cec2/cecCore.c b/src/aig/cec2/cecCore.c
deleted file mode 100644
index 540a3951..00000000
--- a/src/aig/cec2/cecCore.c
+++ /dev/null
@@ -1,245 +0,0 @@
-/**CFile****************************************************************
-
- FileName [cecCore.c]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [Combinatinoal equivalence checking.]
-
- Synopsis [Core procedures.]
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - June 20, 2005.]
-
- Revision [$Id: cecCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "cecInt.h"
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis [This procedure sets default parameters.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Cec_ManSatSetDefaultParams( Cec_ParSat_t * p )
-{
- memset( p, 0, sizeof(Cec_ParSat_t) );
- p->nBTLimit = 10; // conflict limit at a node
- p->nSatVarMax = 2000; // the max number of SAT variables
- p->nCallsRecycle = 100; // calls to perform before recycling SAT solver
- p->fFirstStop = 0; // stop on the first sat output
- p->fPolarFlip = 0; // uses polarity adjustment
- p->fVerbose = 0; // verbose stats
-}
-
-/**Function*************************************************************
-
- Synopsis [This procedure sets default parameters.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Cec_ManCswSetDefaultParams( Cec_ParCsw_t * p )
-{
- memset( p, 0, sizeof(Cec_ParCsw_t) );
- p->nWords = 10; // the number of simulation words
- p->nRounds = 10; // the number of simulation rounds
- p->nBTLimit = 10; // conflict limit at a node
- p->nSatVarMax = 2000; // the max number of SAT variables
- p->nCallsRecycle = 100; // calls to perform before recycling SAT solver
- p->nLevelMax = 50; // restriction on the level of nodes to be swept
- p->fRewriting = 0; // enables AIG rewriting
- p->fFirstStop = 0; // stop on the first sat output
- p->fVerbose = 1; // verbose stats
-}
-
-/**Function*************************************************************
-
- Synopsis [This procedure sets default parameters.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Cec_ManCecSetDefaultParams( Cec_ParCec_t * p )
-{
- memset( p, 0, sizeof(Cec_ParCec_t) );
- p->nIters = 1; // iterations of SAT solving/sweeping
- p->nBTLimitBeg = 2; // starting backtrack limit
- p->nBTlimitMulti = 8; // multiple of backtrack limiter
- p->fUseSmartCnf = 0; // use smart CNF computation
- p->fRewriting = 0; // enables AIG rewriting
- p->fSatSweeping = 0; // enables SAT sweeping
- p->fFirstStop = 0; // stop on the first sat output
- p->fVerbose = 1; // verbose stats
-}
-
-
-/**Function*************************************************************
-
- Synopsis [Performs equivalence checking.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Cec_Sweep( Aig_Man_t * pAig, int nBTLimit )
-{
- extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact );
-// Cec_MtrStatus_t Status;
- Cec_ParCsw_t ParsCsw, * pParsCsw = &ParsCsw;
- Cec_ParSat_t ParsSat, * pParsSat = &ParsSat;
- Caig_Man_t * pCaig;
- Aig_Man_t * pSRAig;
-// int clk;
-
- Cec_ManCswSetDefaultParams( pParsCsw );
- pParsCsw->nBTLimit = nBTLimit;
- pCaig = Caig_ManClassesPrepare( pAig, pParsCsw->nWords, pParsCsw->nRounds );
-
- pSRAig = Caig_ManSpecReduce( pCaig, 20 );
- Aig_ManPrintStats( pSRAig );
- Ioa_WriteAiger( pSRAig, "temp_srm.aig", 0, 1 );
-
-/*
- Cec_ManSatSetDefaultParams( pParsSat );
- pParsSat->fFirstStop = 0;
- pParsSat->nBTLimit = pParsCsw->nBTlimit;
-clk = clock();
- Status = Cec_SatSolveOutputs( pSRAig, pParsSat );
- Cec_MiterStatusPrint( Status, "SRM ", clock() - clk );
-*/
-
- Aig_ManStop( pSRAig );
-
- Caig_ManDelete( pCaig );
-
- return 1;
-}
-
-/**Function*************************************************************
-
- Synopsis [Performs equivalence checking.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Cec_Solve( Aig_Man_t * pAig0, Aig_Man_t * pAig1, Cec_ParCec_t * pPars )
-{
- Cec_ParSat_t ParsSat, * pParsSat = &ParsSat;
- Cec_ParCsw_t ParsCsw, * pParsCsw = &ParsCsw;
- Cec_MtrStatus_t Status;
- Caig_Man_t * pCaig;
- Aig_Man_t * pMiter;
- int i, clk = clock();
- if ( pPars->fVerbose )
- {
- Status = Cec_MiterStatusTrivial( pAig0 );
- Status.nNodes += pAig1? Aig_ManNodeNum( pAig1 ) : 0;
- Cec_MiterStatusPrint( Status, "Init ", 0 );
- }
- // create combinational miter
- if ( pAig1 == NULL )
- {
- Status = Cec_MiterStatus( pAig0 );
- if ( Status.nSat > 0 && pPars->fFirstStop )
- {
- if ( pPars->fVerbose )
- printf( "Output %d is trivially SAT.\n", Status.iOut );
- return 0;
- }
- if ( Status.nUndec == 0 )
- {
- if ( pPars->fVerbose )
- printf( "The miter has no undecided outputs.\n" );
- return 1;
- }
- pMiter = Cec_Duplicate( pAig0 );
- }
- else
- {
- pMiter = Cec_DeriveMiter( pAig0, pAig1 );
- Status = Cec_MiterStatus( pMiter );
- if ( Status.nSat > 0 && pPars->fFirstStop )
- {
- if ( pPars->fVerbose )
- printf( "Output %d is trivially SAT.\n", Status.iOut );
- Aig_ManStop( pMiter );
- return 0;
- }
- if ( Status.nUndec == 0 )
- {
- if ( pPars->fVerbose )
- printf( "The problem is solved by structrual hashing.\n" );
- Aig_ManStop( pMiter );
- return 1;
- }
- }
- if ( pPars->fVerbose )
- Cec_MiterStatusPrint( Status, "Strash", clock() - clk );
- // start parameter structures
-// Cec_ManSatSetDefaultParams( pParsSat );
-// pParsSat->fFirstStop = pPars->fFirstStop;
-// pParsSat->nBTLimit = pPars->nBTLimitBeg;
-/*
- // try SAT solving
- clk = clock();
- pParsSat->nBTLimit *= pPars->nBTlimitMulti;
- Status = Cec_SatSolveOutputs( pMiter, pParsSat );
- if ( pPars->fVerbose )
- Cec_MiterStatusPrint( Status, "SAT ", clock() - clk );
- if ( Status.nSat && pParsSat->fFirstStop )
- break;
- if ( Status.nUndec == 0 )
- break;
-*/
-
- Cec_ManCswSetDefaultParams( pParsCsw );
- pCaig = Caig_ManClassesPrepare( pMiter, pParsCsw->nWords, pParsCsw->nRounds );
- for ( i = 0; i < pPars->nIters; i++ )
- {
- Cec_ManSatSweepInt( pCaig, pParsCsw );
- i = i;
- }
- Caig_ManDelete( pCaig );
- Aig_ManStop( pMiter );
- return 1;
-}
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/aig/cec2/cecInt.h b/src/aig/cec2/cecInt.h
deleted file mode 100644
index ef43e44c..00000000
--- a/src/aig/cec2/cecInt.h
+++ /dev/null
@@ -1,208 +0,0 @@
-/**CFile****************************************************************
-
- FileName [cecInt.h]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [Combinatinoal equivalence checking.]
-
- Synopsis [External declarations.]
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - June 20, 2005.]
-
- Revision [$Id: cecInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#ifndef __CEC_INT_H__
-#define __CEC_INT_H__
-
-////////////////////////////////////////////////////////////////////////
-/// INCLUDES ///
-////////////////////////////////////////////////////////////////////////
-
-#include "aig.h"
-#include "satSolver.h"
-#include "bar.h"
-#include "cec.h"
-
-////////////////////////////////////////////////////////////////////////
-/// PARAMETERS ///
-////////////////////////////////////////////////////////////////////////
-
-#ifdef __cplusplus
-extern "C" {
-#endif
-
-////////////////////////////////////////////////////////////////////////
-/// BASIC TYPES ///
-////////////////////////////////////////////////////////////////////////
-
-typedef struct Cec_ManSat_t_ Cec_ManSat_t;
-struct Cec_ManSat_t_
-{
- // parameters
- Cec_ParSat_t * pPars;
- // AIGs used in the package
- Aig_Man_t * pAig; // the AIG whose outputs are considered
- Vec_Int_t * vStatus; // status for each output
- // SAT solving
- sat_solver * pSat; // recyclable SAT solver
- int nSatVars; // the counter of SAT variables
- int * pSatVars; // mapping of each node into its SAT var
- Vec_Ptr_t * vUsedNodes; // nodes whose SAT vars are assigned
- int nRecycles; // the number of times SAT solver was recycled
- int nCallsSince; // the number of calls since the last recycle
- Vec_Ptr_t * vFanins; // fanins of the CNF node
- // SAT calls statistics
- int nSatUnsat; // the number of proofs
- int nSatSat; // the number of failure
- int nSatUndec; // the number of timeouts
- // runtime stats
- int timeSatUnsat; // unsat
- int timeSatSat; // sat
- int timeSatUndec; // undecided
- int timeTotal; // total runtime
-};
-
-typedef struct Cec_ManCec_t_ Cec_ManCec_t;
-struct Cec_ManCec_t_
-{
- // parameters
- Cec_ParCec_t * pPars;
- // AIGs used in the package
- Aig_Man_t * pAig; // the miter for equivalence checking
- // mapping of PI/PO nodes
-
- // counter-example
- int * pCex; // counter-example
- int iOutput; // the output for this counter-example
-
- // statistics
-
-};
-
-typedef struct Cec_MtrStatus_t_ Cec_MtrStatus_t;
-struct Cec_MtrStatus_t_
-{
- int nInputs; // the total number of inputs
- int nNodes; // the total number of nodes
- int nOutputs; // the total number of outputs
- int nUnsat; // the number of UNSAT outputs
- int nSat; // the number of SAT outputs
- int nUndec; // the number of undecided outputs
- int iOut; // the satisfied output
-};
-
-// combinational simulation manager
-typedef struct Caig_Man_t_ Caig_Man_t;
-struct Caig_Man_t_
-{
- // parameters
- Aig_Man_t * pAig; // the AIG to be used for simulation
- int nWords; // the number of simulation words
- // AIG representation
- int nPis; // the number of primary inputs
- int nPos; // the number of primary outputs
- int nNodes; // the number of internal nodes
- int nObjs; // nPis + nNodes + nPos + 1
- int * pFans0; // fanin0 for all objects
- int * pFans1; // fanin1 for all objects
- // simulation info
- int * pRefs; // reference counter for each node
- unsigned * pSims; // simlulation information for each node
- // recycable memory
- unsigned * pMems; // allocated simulaton memory
- int nWordsAlloc; // the number of allocated entries
- int nMems; // the number of used entries
- int nMemsMax; // the max number of used entries
- int MemFree; // next ABC_FREE entry
- // equivalence class representation
- int * pReprs; // representatives of each node
- int * pNexts; // nexts for each node
- // temporaries
- Vec_Ptr_t * vSims; // pointers to sim info
- Vec_Int_t * vClassOld; // old class numbers
- Vec_Int_t * vClassNew; // new class numbers
- Vec_Int_t * vRefinedC; // refined const reprs
-};
-
-////////////////////////////////////////////////////////////////////////
-/// MACRO DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-static inline int Cec_Var2Lit( int Var, int fCompl ) { return Var + Var + fCompl; }
-static inline int Cec_Lit2Var( int Lit ) { return Lit >> 1; }
-static inline int Cec_LitIsCompl( int Lit ) { return Lit & 1; }
-static inline int Cec_LitNot( int Lit ) { return Lit ^ 1; }
-static inline int Cec_LitNotCond( int Lit, int c ) { return Lit ^ (int)(c > 0); }
-static inline int Cec_LitRegular( int Lit ) { return Lit & ~01; }
-
-static inline int Cec_ObjSatNum( Cec_ManSat_t * p, Aig_Obj_t * pObj ) { return p->pSatVars[pObj->Id]; }
-static inline void Cec_ObjSetSatNum( Cec_ManSat_t * p, Aig_Obj_t * pObj, int Num ) { p->pSatVars[pObj->Id] = Num; }
-
-static inline Aig_Obj_t * Cec_ObjFraig( Aig_Obj_t * pObj ) { return pObj->pData; }
-static inline void Cec_ObjSetFraig( Aig_Obj_t * pObj, Aig_Obj_t * pNode ) { pObj->pData = pNode; }
-
-static inline int Cec_ObjIsConst1Cand( Aig_Man_t * pAig, Aig_Obj_t * pObj )
-{
- return Aig_ObjRepr(pAig, pObj) == Aig_ManConst1(pAig);
-}
-static inline void Cec_ObjSetConst1Cand( Aig_Man_t * pAig, Aig_Obj_t * pObj )
-{
- assert( !Cec_ObjIsConst1Cand( pAig, pObj ) );
- Aig_ObjSetRepr( pAig, pObj, Aig_ManConst1(pAig) );
-}
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/*=== cecAig.c ==========================================================*/
-extern Aig_Man_t * Cec_Duplicate( Aig_Man_t * p );
-extern Aig_Man_t * Cec_DeriveMiter( Aig_Man_t * p0, Aig_Man_t * p1 );
-/*=== cecClass.c ==========================================================*/
-extern Aig_Man_t * Caig_ManSpecReduce( Caig_Man_t * p, int nLevels );
-extern int Caig_ManCompareEqual( unsigned * p0, unsigned * p1, int nWords );
-extern int Caig_ManCompareConst( unsigned * p, int nWords );
-extern void Caig_ManCollectSimsNormal( Caig_Man_t * p, int i );
-extern int Caig_ManClassRefineOne( Caig_Man_t * p, int i, Vec_Ptr_t * vSims );
-extern void Caig_ManProcessRefined( Caig_Man_t * p, Vec_Int_t * vRefined );
-extern void Caig_ManPrintClasses( Caig_Man_t * p, int fVerbose );
-extern Caig_Man_t * Caig_ManClassesPrepare( Aig_Man_t * pAig, int nWords, int nIters );
-/*=== cecCnf.c ==========================================================*/
-extern void Cec_CnfNodeAddToSolver( Cec_ManSat_t * p, Aig_Obj_t * pObj );
-/*=== cecSat.c ==========================================================*/
-extern Cec_MtrStatus_t Cec_SatSolveOutputs( Aig_Man_t * pAig, Cec_ParSat_t * pPars );
-/*=== cecSim.c ==========================================================*/
-extern Caig_Man_t * Caig_ManCreate( Aig_Man_t * pAig );
-extern void Caig_ManDelete( Caig_Man_t * p );
-extern void Caig_ManSimMemRelink( Caig_Man_t * p );
-extern unsigned * Caig_ManSimRead( Caig_Man_t * p, int i );
-extern unsigned * Caig_ManSimRef( Caig_Man_t * p, int i );
-extern unsigned * Caig_ManSimDeref( Caig_Man_t * p, int i );
-extern void Caig_ManSimulateRound( Caig_Man_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t * vInfoCos );
-extern int Cec_ManSimulate( Aig_Man_t * pAig, int nWords, int nIters, int TimeLimit, int fMiter, int fVerbose );
-/*=== cecStatus.c ==========================================================*/
-extern int Cec_OutputStatus( Aig_Man_t * p, Aig_Obj_t * pObj );
-extern Cec_MtrStatus_t Cec_MiterStatus( Aig_Man_t * p );
-extern Cec_MtrStatus_t Cec_MiterStatusTrivial( Aig_Man_t * p );
-extern void Cec_MiterStatusPrint( Cec_MtrStatus_t S, char * pString, int Time );
-/*=== cecSweep.c ==========================================================*/
-extern void Cec_ManSatSweepInt( Caig_Man_t * pMan, Cec_ParCsw_t * pPars );
-extern Aig_Man_t * Cec_ManSatSweep( Aig_Man_t * pAig, Cec_ParCsw_t * pPars );
-
-#ifdef __cplusplus
-}
-#endif
-
-#endif
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
diff --git a/src/aig/cec2/cecMan.c b/src/aig/cec2/cecMan.c
deleted file mode 100644
index 86415c53..00000000
--- a/src/aig/cec2/cecMan.c
+++ /dev/null
@@ -1,59 +0,0 @@
-/**CFile****************************************************************
-
- FileName [cecMan.c]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [Combinatinoal equivalence checking.]
-
- Synopsis [Manager pcocures.]
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - June 20, 2005.]
-
- Revision [$Id: cecMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "cecInt.h"
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/aig/cec2/cecSat.c b/src/aig/cec2/cecSat.c
deleted file mode 100644
index a999dd97..00000000
--- a/src/aig/cec2/cecSat.c
+++ /dev/null
@@ -1,250 +0,0 @@
-/**CFile****************************************************************
-
- FileName [cecSat.c]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [Combinatinoal equivalence checking.]
-
- Synopsis [SAT solver calls.]
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - June 20, 2005.]
-
- Revision [$Id: cecSat.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "cecInt.h"
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis [Creates the manager.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Cec_ManSat_t * Cec_ManCreate( Aig_Man_t * pAig, Cec_ParSat_t * pPars )
-{
- Cec_ManSat_t * p;
- // create interpolation manager
- p = ABC_ALLOC( Cec_ManSat_t, 1 );
- memset( p, 0, sizeof(Cec_ManSat_t) );
- p->pPars = pPars;
- p->pAig = pAig;
- // SAT solving
- p->nSatVars = 1;
- p->pSatVars = ABC_CALLOC( int, Aig_ManObjNumMax(pAig) );
- p->vUsedNodes = Vec_PtrAlloc( 1000 );
- p->vFanins = Vec_PtrAlloc( 100 );
- return p;
-}
-
-/**Function*************************************************************
-
- Synopsis [Frees the manager.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Cec_ManStop( Cec_ManSat_t * p )
-{
- if ( p->pSat )
- sat_solver_delete( p->pSat );
- Vec_PtrFree( p->vUsedNodes );
- Vec_PtrFree( p->vFanins );
- ABC_FREE( p->pSatVars );
- ABC_FREE( p );
-}
-
-/**Function*************************************************************
-
- Synopsis [Recycles the SAT solver.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Cec_ManSatSolverRecycle( Cec_ManSat_t * p )
-{
- int Lit;
- if ( p->pSat )
- {
- Aig_Obj_t * pObj;
- int i;
- Vec_PtrForEachEntry( p->vUsedNodes, pObj, i )
- Cec_ObjSetSatNum( p, pObj, 0 );
- Vec_PtrClear( p->vUsedNodes );
-// memset( p->pSatVars, 0, sizeof(int) * Aig_ManObjNumMax(p->pAigTotal) );
- sat_solver_delete( p->pSat );
- }
- p->pSat = sat_solver_new();
- sat_solver_setnvars( p->pSat, 1000 );
- // var 0 is not used
- // var 1 is reserved for const1 node - add the clause
- p->nSatVars = 1;
-// p->nSatVars = 0;
- Lit = toLit( p->nSatVars );
- if ( p->pPars->fPolarFlip )
- Lit = lit_neg( Lit );
- sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
- Cec_ObjSetSatNum( p, Aig_ManConst1(p->pAig), p->nSatVars++ );
-
- p->nRecycles++;
- p->nCallsSince = 0;
-}
-
-/**Function*************************************************************
-
- Synopsis [Runs equivalence test for the two nodes.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Cec_ManSatCheckNode( Cec_ManSat_t * p, Aig_Obj_t * pNode )
-{
- int nBTLimit = p->pPars->nBTLimit;
- int Lit, RetValue, status, clk;
-
- // sanity checks
- assert( !Aig_IsComplement(pNode) );
-
- p->nCallsSince++; // experiment with this!!!
-
- // check if SAT solver needs recycling
- if ( p->pSat == NULL ||
- (p->pPars->nSatVarMax &&
- p->nSatVars > p->pPars->nSatVarMax &&
- p->nCallsSince > p->pPars->nCallsRecycle) )
- Cec_ManSatSolverRecycle( p );
-
- // if the nodes do not have SAT variables, allocate them
- Cec_CnfNodeAddToSolver( p, pNode );
-
- // propage unit clauses
- if ( p->pSat->qtail != p->pSat->qhead )
- {
- status = sat_solver_simplify(p->pSat);
- assert( status != 0 );
- assert( p->pSat->qtail == p->pSat->qhead );
- }
-
- // solve under assumptions
- // A = 1; B = 0 OR A = 1; B = 1
- Lit = toLitCond( Cec_ObjSatNum(p,pNode), pNode->fPhase );
- if ( p->pPars->fPolarFlip )
- {
- if ( pNode->fPhase ) Lit = lit_neg( Lit );
- }
-//Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
-clk = clock();
- RetValue = sat_solver_solve( p->pSat, &Lit, &Lit + 1,
- (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
- if ( RetValue == l_False )
- {
-p->timeSatUnsat += clock() - clk;
- Lit = lit_neg( Lit );
- RetValue = sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
- assert( RetValue );
- p->timeSatUnsat++;
- return 1;
- }
- else if ( RetValue == l_True )
- {
-p->timeSatSat += clock() - clk;
- p->timeSatSat++;
- return 0;
- }
- else // if ( RetValue == l_Undef )
- {
-p->timeSatUndec += clock() - clk;
- p->timeSatUndec++;
- return -1;
- }
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Cec_MtrStatus_t Cec_SatSolveOutputs( Aig_Man_t * pAig, Cec_ParSat_t * pPars )
-{
- Bar_Progress_t * pProgress = NULL;
- Cec_MtrStatus_t Status;
- Cec_ManSat_t * p;
- Aig_Obj_t * pObj;
- int i, status;
- Status = Cec_MiterStatus( pAig );
- p = Cec_ManCreate( pAig, pPars );
- pProgress = Bar_ProgressStart( stdout, Aig_ManPoNum(pAig) );
- Aig_ManForEachPo( pAig, pObj, i )
- {
- Bar_ProgressUpdate( pProgress, i, "SAT..." );
- if ( Cec_OutputStatus(pAig, pObj) )
- continue;
- status = Cec_ManSatCheckNode( p, Aig_ObjFanin0(pObj) );
- if ( status == 1 )
- {
- Status.nUndec--, Status.nUnsat++;
- Aig_ObjPatchFanin0( pAig, pObj, Aig_ManConst0(pAig) );
- }
- if ( status == 0 )
- {
- Status.nUndec--, Status.nSat++;
- Aig_ObjPatchFanin0( pAig, pObj, Aig_ManConst1(pAig) );
- }
- if ( status == -1 )
- continue;
- // save the pattern (if it is first)
- if ( Status.iOut == -1 )
- {
- }
- // quit if at least one of them is solved
- if ( status == 0 && pPars->fFirstStop )
- break;
- }
- Aig_ManCleanup( pAig );
- Bar_ProgressStop( pProgress );
- printf( " Confs = %8d. Recycles = %6d.\n", p->pPars->nBTLimit, p->nRecycles );
- Cec_ManStop( p );
- return Status;
-}
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/aig/cec2/cecSat2.c b/src/aig/cec2/cecSat2.c
deleted file mode 100644
index 4f009b25..00000000
--- a/src/aig/cec2/cecSat2.c
+++ /dev/null
@@ -1,284 +0,0 @@
-/**CFile****************************************************************
-
- FileName [cecSat.c]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [Combinational equivalence checking.]
-
- Synopsis [Backend calling the SAT solver.]
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - June 30, 2007.]
-
- Revision [$Id: cecSat.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "aig.h"
-#include "cnf.h"
-#include "../../sat/lsat/solver.h"
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis [Writes CNF into a file.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-solver * Cnf_WriteIntoSolverNew( Cnf_Dat_t * p )
-{
- solver * pSat;
- int i, status;
- pSat = solver_new();
- for ( i = 0; i < p->nVars; i++ )
- solver_newVar( pSat );
- for ( i = 0; i < p->nClauses; i++ )
- {
- if ( !solver_addClause( pSat, p->pClauses[i+1]-p->pClauses[i], p->pClauses[i] ) )
- {
- solver_delete( pSat );
- return NULL;
- }
- }
- status = solver_simplify(pSat);
- if ( status == 0 )
- {
- solver_delete( pSat );
- return NULL;
- }
- return pSat;
-}
-
-/**Function*************************************************************
-
- Synopsis [Adds the OR-clause.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Cnf_DataWriteAndClausesNew( void * p, Cnf_Dat_t * pCnf )
-{
-/*
- sat_solver * pSat = p;
- Aig_Obj_t * pObj;
- int i, Lit;
- Aig_ManForEachPo( pCnf->pMan, pObj, i )
- {
- Lit = toLitCond( pCnf->pVarNums[pObj->Id], 0 );
- if ( !sat_solver_addclause( pSat, &Lit, &Lit+1 ) )
- return 0;
- }
-*/
- return 1;
-}
-
-/**Function*************************************************************
-
- Synopsis [Adds the OR-clause.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Cnf_DataWriteOrClauseNew( solver * pSat, Cnf_Dat_t * pCnf )
-{
- Aig_Obj_t * pObj;
- int i, * pLits;
- pLits = ALLOC( int, Aig_ManPoNum(pCnf->pMan) );
- Aig_ManForEachPo( pCnf->pMan, pObj, i )
- pLits[i] = solver_mkLit_args( pCnf->pVarNums[pObj->Id], 0 );
- if ( !solver_addClause( pSat, Aig_ManPoNum(pCnf->pMan), pLits ) )
- {
- free( pLits );
- return 0;
- }
- free( pLits );
- return 1;
-}
-
-/**Function*************************************************************
-
- Synopsis [Writes the given clause in a file in DIMACS format.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Sat_SolverPrintStatsNew( FILE * pFile, solver * pSat )
-{
-// printf( "starts : %8d\n", solver_num_assigns(pSat) );
- printf( "vars : %8d\n", solver_num_vars(pSat) );
- printf( "clauses : %8d\n", solver_num_clauses(pSat) );
- printf( "conflicts : %8d\n", solver_num_learnts(pSat) );
-}
-
-/**Function*************************************************************
-
- Synopsis [Returns a counter-example.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int * Sat_SolverGetModelNew( solver * pSat, int * pVars, int nVars )
-{
- int * pModel;
- int i;
- pModel = ALLOC( int, nVars+1 );
- for ( i = 0; i < nVars; i++ )
- {
- assert( pVars[i] >= 0 && pVars[i] < solver_num_vars(pSat) );
- pModel[i] = (int)(solver_modelValue_Var( pSat, pVars[i] ) == solver_l_True);
- }
- return pModel;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Cec_RunSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fFlipBits, int fAndOuts, int fVerbose )
-{
- solver * pSat;
- Cnf_Dat_t * pCnf;
- int status, RetValue, clk = clock();
- Vec_Int_t * vCiIds;
-
- assert( Aig_ManRegNum(pMan) == 0 );
- pMan->pData = NULL;
-
- // derive CNF
- pCnf = Cnf_Derive( pMan, Aig_ManPoNum(pMan) );
-// pCnf = Cnf_DeriveSimple( pMan, Aig_ManPoNum(pMan) );
-
- // convert into SAT solver
- pSat = Cnf_WriteIntoSolverNew( pCnf );
- if ( pSat == NULL )
- {
- Cnf_DataFree( pCnf );
- return 1;
- }
-
-
- if ( fAndOuts )
- {
- assert( 0 );
- // assert each output independently
- if ( !Cnf_DataWriteAndClausesNew( pSat, pCnf ) )
- {
- solver_delete( pSat );
- Cnf_DataFree( pCnf );
- return 1;
- }
- }
- else
- {
- // add the OR clause for the outputs
- if ( !Cnf_DataWriteOrClauseNew( pSat, pCnf ) )
- {
- solver_delete( pSat );
- Cnf_DataFree( pCnf );
- return 1;
- }
- }
- vCiIds = Cnf_DataCollectPiSatNums( pCnf, pMan );
- Cnf_DataFree( pCnf );
-
-
-// printf( "Created SAT problem with %d variable and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) );
-// PRT( "Time", clock() - clk );
-
- // simplify the problem
- clk = clock();
- status = solver_simplify(pSat);
-// printf( "Simplified the problem to %d variables and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) );
-// PRT( "Time", clock() - clk );
- if ( status == 0 )
- {
- Vec_IntFree( vCiIds );
- solver_delete( pSat );
-// printf( "The problem is UNSATISFIABLE after simplification.\n" );
- return 1;
- }
-
- // solve the miter
- clk = clock();
- if ( fVerbose )
- solver_set_verbosity( pSat, 1 );
- status = solver_solve( pSat, 0, NULL );
- if ( status == solver_l_Undef )
- {
-// printf( "The problem timed out.\n" );
- RetValue = -1;
- }
- else if ( status == solver_l_True )
- {
-// printf( "The problem is SATISFIABLE.\n" );
- RetValue = 0;
- }
- else if ( status == solver_l_False )
- {
-// printf( "The problem is UNSATISFIABLE.\n" );
- RetValue = 1;
- }
- else
- assert( 0 );
-// PRT( "SAT sat_solver time", clock() - clk );
-// printf( "The number of conflicts = %d.\n", (int)pSat->sat_solver_stats.conflicts );
-
- // if the problem is SAT, get the counterexample
- if ( status == solver_l_True )
- {
- pMan->pData = Sat_SolverGetModelNew( pSat, vCiIds->pArray, vCiIds->nSize );
- }
- // free the sat_solver
- if ( fVerbose )
- Sat_SolverPrintStatsNew( stdout, pSat );
-//sat_solver_store_write( pSat, "trace.cnf" );
-//sat_solver_store_free( pSat );
- solver_delete( pSat );
- Vec_IntFree( vCiIds );
- return RetValue;
-}
-
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
diff --git a/src/aig/cec2/cecSim.c b/src/aig/cec2/cecSim.c
deleted file mode 100644
index 4fedbddc..00000000
--- a/src/aig/cec2/cecSim.c
+++ /dev/null
@@ -1,447 +0,0 @@
-/**CFile****************************************************************
-
- FileName [cecSim.c]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [Combinatinoal equivalence checking.]
-
- Synopsis [AIG simulation.]
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - June 20, 2005.]
-
- Revision [$Id: cecSim.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "cecInt.h"
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis [Creates fast simulation manager.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Caig_Man_t * Caig_ManCreate( Aig_Man_t * pAig )
-{
- Caig_Man_t * p;
- Aig_Obj_t * pObj;
- int i;
- assert( Aig_ManHasNoGaps(pAig) );
- Aig_ManCleanData( pAig );
- p = (Caig_Man_t *)ABC_ALLOC( Caig_Man_t, 1 );
- memset( p, 0, sizeof(Caig_Man_t) );
- p->pAig = pAig;
- p->nPis = Aig_ManPiNum(pAig);
- p->nPos = Aig_ManPoNum(pAig);
- p->nNodes = Aig_ManNodeNum(pAig);
- p->nObjs = p->nPis + p->nPos + p->nNodes + 1;
- p->pFans0 = ABC_ALLOC( int, p->nObjs );
- p->pFans1 = ABC_ALLOC( int, p->nObjs );
- p->pRefs = ABC_ALLOC( int, p->nObjs );
- p->pSims = ABC_CALLOC( unsigned, p->nObjs );
- // add objects
- Aig_ManForEachObj( pAig, pObj, i )
- {
- p->pRefs[i] = Aig_ObjRefs(pObj);
- if ( Aig_ObjIsNode(pObj) )
- {
- p->pFans0[i] = (Aig_ObjFaninId0(pObj) << 1) | Aig_ObjFaninC0(pObj);
- p->pFans1[i] = (Aig_ObjFaninId1(pObj) << 1) | Aig_ObjFaninC1(pObj);
- }
- else if ( Aig_ObjIsPo(pObj) )
- {
- p->pFans0[i] = (Aig_ObjFaninId0(pObj) << 1) | Aig_ObjFaninC0(pObj);
- p->pFans1[i] = -1;
- }
- else
- {
- assert( Aig_ObjIsPi(pObj) || Aig_ObjIsConst1(pObj) );
- p->pFans0[i] = -1;
- p->pFans1[i] = -1;
- }
- }
- // temporaries
- p->vClassOld = Vec_IntAlloc( 1000 );
- p->vClassNew = Vec_IntAlloc( 1000 );
- p->vRefinedC = Vec_IntAlloc( 10000 );
- p->vSims = Vec_PtrAlloc( 1000 );
- return p;
-}
-
-/**Function*************************************************************
-
- Synopsis [Creates fast simulation manager.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Caig_ManDelete( Caig_Man_t * p )
-{
- Vec_IntFree( p->vClassOld );
- Vec_IntFree( p->vClassNew );
- Vec_IntFree( p->vRefinedC );
- Vec_PtrFree( p->vSims );
- ABC_FREE( p->pFans0 );
- ABC_FREE( p->pFans1 );
- ABC_FREE( p->pRefs );
- ABC_FREE( p->pSims );
- ABC_FREE( p->pMems );
- ABC_FREE( p->pReprs );
- ABC_FREE( p->pNexts );
- ABC_FREE( p );
-}
-
-/**Function*************************************************************
-
- Synopsis [References simulation info.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Caig_ManSimMemRelink( Caig_Man_t * p )
-{
- int * pPlace, Ent;
- pPlace = &p->MemFree;
- for ( Ent = p->nMems * (p->nWords + 1);
- Ent + p->nWords + 1 < p->nWordsAlloc;
- Ent += p->nWords + 1 )
- {
- *pPlace = Ent;
- pPlace = p->pMems + Ent;
- }
- *pPlace = 0;
-}
-
-/**Function*************************************************************
-
- Synopsis [References simulation info.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-unsigned * Caig_ManSimRead( Caig_Man_t * p, int i )
-{
- assert( i && p->pSims[i] > 0 );
- return p->pMems + p->pSims[i];
-}
-
-/**Function*************************************************************
-
- Synopsis [References simulation info.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-unsigned * Caig_ManSimRef( Caig_Man_t * p, int i )
-{
- unsigned * pSim;
- assert( p->pSims[i] == 0 );
- if ( p->MemFree == 0 )
- {
- if ( p->nWordsAlloc == 0 )
- {
- assert( p->pMems == NULL );
- p->nWordsAlloc = (1<<17); // -> 1Mb
- p->nMems = 1;
- }
- p->nWordsAlloc *= 2;
- p->pMems = ABC_REALLOC( unsigned, p->pMems, p->nWordsAlloc );
- Caig_ManSimMemRelink( p );
- }
- p->pSims[i] = p->MemFree;
- pSim = p->pMems + p->MemFree;
- p->MemFree = pSim[0];
- pSim[0] = p->pRefs[i];
- p->nMems++;
- if ( p->nMemsMax < p->nMems )
- p->nMemsMax = p->nMems;
- return pSim;
-}
-
-/**Function*************************************************************
-
- Synopsis [Dereference simulaton info.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-unsigned * Caig_ManSimDeref( Caig_Man_t * p, int i )
-{
- unsigned * pSim;
- assert( p->pSims[i] > 0 );
- pSim = p->pMems + p->pSims[i];
- if ( --pSim[0] == 0 )
- {
- pSim[0] = p->MemFree;
- p->MemFree = p->pSims[i];
- p->pSims[i] = 0;
- p->nMems--;
- }
- return pSim;
-}
-
-/**Function*************************************************************
-
- Synopsis [Simulates one round.]
-
- Description [Returns the number of PO entry if failed; 0 otherwise.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Caig_ManSimulateRound( Caig_Man_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t * vInfoCos )
-{
- unsigned * pRes0, * pRes1, * pRes;
- int i, w, iCiId = 0, iCoId = 0;
- int nWords = Vec_PtrReadWordsSimInfo( vInfoCis );
- assert( vInfoCos == NULL || nWords == Vec_PtrReadWordsSimInfo(vInfoCos) );
- Vec_IntClear( p->vRefinedC );
- if ( p->pRefs[0] )
- {
- pRes = Caig_ManSimRef( p, 0 );
- for ( w = 1; w <= nWords; w++ )
- pRes[w] = ~0;
- }
- for ( i = 1; i < p->nObjs; i++ )
- {
- if ( p->pFans0[i] == -1 ) // ci always has zero first fanin
- {
- if ( p->pRefs[i] == 0 )
- {
- iCiId++;
- continue;
- }
- pRes = Caig_ManSimRef( p, i );
- pRes0 = Vec_PtrEntry( vInfoCis, iCiId++ );
- for ( w = 1; w <= nWords; w++ )
- pRes[w] = pRes0[w-1];
- goto references;
- }
- if ( p->pFans1[i] == -1 ) // co always has non-zero 1st fanin and zero 2nd fanin
- {
- pRes0 = Caig_ManSimDeref( p, Cec_Lit2Var(p->pFans0[i]) );
- if ( vInfoCos )
- {
- pRes = Vec_PtrEntry( vInfoCos, iCoId++ );
- if ( Cec_LitIsCompl(p->pFans0[i]) )
- for ( w = 1; w <= nWords; w++ )
- pRes[w-1] = ~pRes0[w];
- else
- for ( w = 1; w <= nWords; w++ )
- pRes[w-1] = pRes0[w];
- }
- continue;
- }
- assert( p->pRefs[i] );
- pRes = Caig_ManSimRef( p, i );
- pRes0 = Caig_ManSimDeref( p, Cec_Lit2Var(p->pFans0[i]) );
- pRes1 = Caig_ManSimDeref( p, Cec_Lit2Var(p->pFans1[i]) );
- if ( Cec_LitIsCompl(p->pFans0[i]) )
- {
- if ( Cec_LitIsCompl(p->pFans1[i]) )
- for ( w = 1; w <= nWords; w++ )
- pRes[w] = ~(pRes0[w] | pRes1[w]);
- else
- for ( w = 1; w <= nWords; w++ )
- pRes[w] = ~pRes0[w] & pRes1[w];
- }
- else
- {
- if ( Cec_LitIsCompl(p->pFans1[i]) )
- for ( w = 1; w <= nWords; w++ )
- pRes[w] = pRes0[w] & ~pRes1[w];
- else
- for ( w = 1; w <= nWords; w++ )
- pRes[w] = pRes0[w] & pRes1[w];
- }
-references:
- if ( p->pReprs == NULL )
- continue;
- // if this node is candidate constant, collect it
- if ( p->pReprs[i] == 0 && !Caig_ManCompareConst(pRes + 1, nWords) )
- {
- pRes[0]++;
- Vec_IntPush( p->vRefinedC, i );
- }
- // if the node belongs to a class, save it
- if ( p->pReprs[i] > 0 || p->pNexts[i] > 0 )
- pRes[0]++;
- // if this is the last node of the class, process it
- if ( p->pReprs[i] > 0 && p->pNexts[i] == 0 )
- {
- Caig_ManCollectSimsNormal( p, p->pReprs[i] );
- Caig_ManClassRefineOne( p, p->pReprs[i], p->vSims );
- }
- }
- if ( Vec_IntSize(p->vRefinedC) > 0 )
- Caig_ManProcessRefined( p, p->vRefinedC );
- assert( iCiId == p->nPis );
- assert( vInfoCos == NULL || iCoId == p->nPos );
- assert( p->nMems == 1 );
-/*
- if ( p->nMems > 1 )
- {
- for ( i = 1; i < p->nObjs; i++ )
- if ( p->pSims[i] )
- {
- int x = 0;
- }
- }
-*/
-}
-
-/**Function*************************************************************
-
- Synopsis [Returns the number of PO that failed.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Cec_ManFindPo( Vec_Ptr_t * vInfo, int nWords )
-{
- unsigned * pInfo;
- int i, w;
- Vec_PtrForEachEntry( vInfo, pInfo, i )
- for ( w = 0; w < nWords; w++ )
- if ( pInfo[w] != 0 )
- return i;
- return -1;
-}
-
-/**Function*************************************************************
-
- Synopsis [Returns 1 if the bug is detected, 0 otherwise.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Cec_ManSimulate( Aig_Man_t * pAig, int nWords, int nIters, int TimeLimit, int fMiter, int fVerbose )
-{
- Caig_Man_t * p;
- Cec_MtrStatus_t Status;
- Vec_Ptr_t * vInfoCis, * vInfoCos = NULL;
- int i, RetValue = 0, clk, clkTotal = clock();
-/*
- p = Caig_ManClassesPrepare( pAig, nWords, nIters );
-// if ( fVerbose )
- printf( "Maxcut = %6d. AIG mem = %8.3f Mb. Sim mem = %8.3f Mb.\n",
- p->nMemsMax,
- 1.0*(p->nObjs * 14)/(1<<20),
- 1.0*(p->nMemsMax * (nWords+1))/(1<<20) );
- Caig_ManDelete( p );
- return 0;
-*/
- if ( fMiter )
- {
- Status = Cec_MiterStatus( pAig );
- if ( Status.nSat > 0 )
- {
- printf( "Miter is trivially satisfiable (output %d).\n", Status.iOut );
- return 1;
- }
- if ( Status.nUndec == 0 )
- {
- printf( "Miter is trivially unsatisfiable.\n" );
- return 0;
- }
- }
- Aig_ManRandom( 1 );
- p = Caig_ManCreate( pAig );
- p->nWords = nWords;
- if ( fMiter )
- vInfoCos = Vec_PtrAllocSimInfo( Aig_ManPiNum(pAig), nWords );
- for ( i = 0; i < nIters; i++ )
- {
- clk = clock();
- vInfoCis = Vec_PtrAllocSimInfo( Aig_ManPiNum(pAig), nWords );
- Aig_ManRandomInfo( vInfoCis, 0, nWords );
- Caig_ManSimulateRound( p, vInfoCis, vInfoCos );
- Vec_PtrFree( vInfoCis );
- if ( fVerbose )
- {
- printf( "Iter %3d out of %3d and timeout %3d sec. ", i+1, nIters, TimeLimit );
- printf("Time = %7.2f sec\r", (1.0*clock()-clkTotal)/CLOCKS_PER_SEC);
- }
- if ( fMiter )
- {
- int iOut = Cec_ManFindPo( vInfoCos, nWords );
- if ( iOut >= 0 )
- {
- if ( fVerbose )
- printf( "Miter is satisfiable after simulation (output %d).\n", iOut );
- RetValue = 1;
- break;
- }
- }
- if ( (clock() - clk)/CLOCKS_PER_SEC >= TimeLimit )
- {
- printf( "No bug detected after %d rounds with time limit %d seconds.\n", i+1, TimeLimit );
- break;
- }
- }
- if ( fVerbose )
- printf( "Maxcut = %6d. AIG mem = %8.3f Mb. Sim mem = %8.3f Mb.\n",
- p->nMemsMax,
- 1.0*(p->nObjs * 14)/(1<<20),
- 1.0*(p->nMemsMax * 4 * (nWords+1))/(1<<20) );
- Caig_ManDelete( p );
- if ( vInfoCos )
- Vec_PtrFree( vInfoCos );
- return RetValue > 0;
-}
-
-
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/aig/cec2/cecStatus.c b/src/aig/cec2/cecStatus.c
deleted file mode 100644
index 79d6ec66..00000000
--- a/src/aig/cec2/cecStatus.c
+++ /dev/null
@@ -1,187 +0,0 @@
-/**CFile****************************************************************
-
- FileName [cecStatus.c]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [Combinatinoal equivalence checking.]
-
- Synopsis [Miter status.]
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - June 20, 2005.]
-
- Revision [$Id: cecStatus.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "cecInt.h"
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis [Returns 1 if the output is known.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Cec_OutputStatus( Aig_Man_t * p, Aig_Obj_t * pObj )
-{
- Aig_Obj_t * pChild;
- assert( Aig_ObjIsPo(pObj) );
- pChild = Aig_ObjChild0(pObj);
- // check if the output is constant 0
- if ( pChild == Aig_ManConst0(p) )
- return 1;
- // check if the output is constant 1
- if ( pChild == Aig_ManConst1(p) )
- return 1;
- // check if the output is a primary input
- if ( Aig_ObjIsPi(Aig_Regular(pChild)) )
- return 1;
- // check if the output is 1 for the 0000 pattern
- if ( Aig_Regular(pChild)->fPhase != (unsigned)Aig_IsComplement(pChild) )
- return 1;
- return 0;
-}
-
-/**Function*************************************************************
-
- Synopsis [Returns number of used inputs.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Cec_CountInputs( Aig_Man_t * p )
-{
- Aig_Obj_t * pObj;
- int i, Counter = 0;
- Aig_ManForEachPi( p, pObj, i )
- Counter += (int)(pObj->nRefs > 0);
- return Counter;
-}
-
-/**Function*************************************************************
-
- Synopsis [Checks the status of the miter.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Cec_MtrStatus_t Cec_MiterStatus( Aig_Man_t * p )
-{
- Cec_MtrStatus_t Status;
- Aig_Obj_t * pObj, * pChild;
- int i;
- assert( p->nRegs == 0 );
- memset( &Status, 0, sizeof(Cec_MtrStatus_t) );
- Status.iOut = -1;
- Status.nInputs = Cec_CountInputs( p );
- Status.nNodes = Aig_ManNodeNum( p );
- Status.nOutputs = Aig_ManPoNum(p);
- Aig_ManForEachPo( p, pObj, i )
- {
- pChild = Aig_ObjChild0(pObj);
- // check if the output is constant 0
- if ( pChild == Aig_ManConst0(p) )
- Status.nUnsat++;
- // check if the output is constant 1
- else if ( pChild == Aig_ManConst1(p) )
- {
- Status.nSat++;
- if ( Status.iOut == -1 )
- Status.iOut = i;
- }
- // check if the output is a primary input
- else if ( Aig_ObjIsPi(Aig_Regular(pChild)) )
- {
- Status.nSat++;
- if ( Status.iOut == -1 )
- Status.iOut = i;
- }
- // check if the output is 1 for the 0000 pattern
- else if ( Aig_Regular(pChild)->fPhase != (unsigned)Aig_IsComplement(pChild) )
- {
- Status.nSat++;
- if ( Status.iOut == -1 )
- Status.iOut = i;
- }
- else
- Status.nUndec++;
- }
- return Status;
-}
-
-/**Function*************************************************************
-
- Synopsis [Checks the status of the miter.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Cec_MtrStatus_t Cec_MiterStatusTrivial( Aig_Man_t * p )
-{
- Cec_MtrStatus_t Status;
- memset( &Status, 0, sizeof(Cec_MtrStatus_t) );
- Status.iOut = -1;
- Status.nInputs = Aig_ManPiNum(p);
- Status.nNodes = Aig_ManNodeNum( p );
- Status.nOutputs = Aig_ManPoNum(p);
- Status.nUndec = Aig_ManPoNum(p);
- return Status;
-}
-
-/**Function*************************************************************
-
- Synopsis [Prints the status of the miter.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Cec_MiterStatusPrint( Cec_MtrStatus_t S, char * pString, int Time )
-{
- printf( "%s:", pString );
- printf( " I =%6d", S.nInputs );
- printf( " N =%7d", S.nNodes );
- printf( " " );
- printf( " ? =%6d", S.nUndec );
- printf( " U =%6d", S.nUnsat );
- printf( " S =%6d", S.nSat );
- printf(" %7.2f sec\n", (float)(Time)/(float)(CLOCKS_PER_SEC));
-}
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/aig/cec2/cecSweep.c b/src/aig/cec2/cecSweep.c
deleted file mode 100644
index d7d85b02..00000000
--- a/src/aig/cec2/cecSweep.c
+++ /dev/null
@@ -1,582 +0,0 @@
-/**CFile****************************************************************
-
- FileName [cecSweep.c]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [Combinatinoal equivalence checking.]
-
- Synopsis [Pattern accumulation.]
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - June 20, 2005.]
-
- Revision [$Id: cecSweep.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "cecInt.h"
-#include "satSolver.h"
-#include "cnf.h"
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-typedef struct Cec_ManCsw_t_ Cec_ManCsw_t;
-struct Cec_ManCsw_t_
-{
- // parameters
- Cec_ParCsw_t * pPars; // parameters
- Caig_Man_t * p; // AIG and simulation manager
- // mapping into copy
- Aig_Obj_t ** pCopy; // the copy of nodes
- Vec_Int_t * vCopies; // the nodes copied in the last round
- char * pProved; // tells if the given node is proved
- char * pProvedNow; // tells if the given node is proved
- int * pLevel; // level of the nodes
- // collected patterns
- Vec_Ptr_t * vInfo; // simulation info accumulated
- Vec_Ptr_t * vPres; // simulation presence accumulated
- Vec_Ptr_t * vInfoAll; // vector of vectors of simulation info
- // temporaries
- Vec_Int_t * vPiNums; // primary input numbers
- Vec_Int_t * vPoNums; // primary output numbers
- Vec_Int_t * vPat; // one counter-example
- Vec_Ptr_t * vSupp; // support of one node
-};
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis [Adds pattern to storage.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Cec_ManSavePattern( Cec_ManCsw_t * p, Vec_Int_t * vPat )
-{
- unsigned * pInfo, * pPres;
- int nPatsAlloc, iLit, i, c;
- assert( p->p->nWords == Vec_PtrReadWordsSimInfo(p->vInfo) );
- // find next empty place
- nPatsAlloc = 32 * p->p->nWords;
- for ( c = 0; c < nPatsAlloc; c++ )
- {
- Vec_IntForEachEntry( vPat, iLit, i )
- {
- pPres = Vec_PtrEntry( p->vPres, Cec_Lit2Var(iLit) );
- if ( Aig_InfoHasBit( pPres, c ) )
- break;
- }
- if ( i == Vec_IntSize(vPat) )
- break;
- }
- // increase the size if needed
- if ( c == nPatsAlloc )
- {
- p->vInfo = Vec_PtrAllocSimInfo( p->p->nPis, p->p->nWords );
- Vec_PtrCleanSimInfo( p->vInfo, 0, p->p->nWords );
- Vec_PtrCleanSimInfo( p->vPres, 0, p->p->nWords );
- Vec_PtrPush( p->vInfoAll, p->vInfo );
- c = 0;
- }
- // save the pattern
- Vec_IntForEachEntry( vPat, iLit, i )
- {
- pPres = Vec_PtrEntry( p->vPres, Cec_Lit2Var(iLit) );
- pInfo = Vec_PtrEntry( p->vInfo, Cec_Lit2Var(iLit) );
- Aig_InfoSetBit( pPres, c );
- if ( !Cec_LitIsCompl(iLit) )
- Aig_InfoSetBit( pInfo, c );
- }
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Aig_Obj_t * Cec_ManCswCreatePartition_rec( Aig_Man_t * pAig, Cec_ManCsw_t * p, int i )
-{
- Aig_Obj_t * pRes0, * pRes1;
- if ( p->pCopy[i] )
- return p->pCopy[i];
- Vec_IntPush( p->vCopies, i );
- if ( p->p->pFans0[i] == -1 ) // pi
- {
- Vec_IntPush( p->vPiNums, Aig_ObjPioNum( Aig_ManObj(p->p->pAig, i) ) );
- return p->pCopy[i] = Aig_ObjCreatePi( pAig );
- }
- assert( p->p->pFans0[i] && p->p->pFans1[i] );
- pRes0 = Cec_ManCswCreatePartition_rec( pAig, p, Cec_Lit2Var(p->p->pFans0[i]) );
- pRes0 = Aig_NotCond( pRes0, Cec_LitIsCompl(p->p->pFans0[i]) );
- pRes1 = Cec_ManCswCreatePartition_rec( pAig, p, Cec_Lit2Var(p->p->pFans1[i]) );
- pRes1 = Aig_NotCond( pRes1, Cec_LitIsCompl(p->p->pFans1[i]) );
- return p->pCopy[i] = Aig_And( pAig, pRes0, pRes1 );
-}
-
-/**Function*************************************************************
-
- Synopsis [Creates dynamic partition.]
-
- Description [PIs point to node IDs. POs point to node IDs.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Aig_Man_t * Cec_ManCswCreatePartition( Cec_ManCsw_t * p, int * piStart, int nMitersMin, int nNodesMin, int nLevelMax )
-{
- Caig_Man_t * pMan = p->p;
- Aig_Man_t * pAig;
- Aig_Obj_t * pRepr, * pNode, * pMiter, * pTerm;
- int i, iNode, Counter = 0;
- assert( p->pCopy && p->vCopies );
- // clear previous marks
- Vec_IntForEachEntry( p->vCopies, iNode, i )
- p->pCopy[iNode] = NULL;
- Vec_IntClear( p->vCopies );
- // iterate through nodes starting from the given one
- pAig = Aig_ManStart( nNodesMin );
- p->pCopy[0] = Aig_ManConst1(pAig);
- Vec_IntPush( p->vCopies, 0 );
- for ( i = *piStart; i < pMan->nObjs; i++ )
- {
- if ( pMan->pFans0[i] == -1 ) // pi always has zero first fanin
- continue;
- if ( pMan->pFans1[i] == -1 ) // po always has non-zero 1st fanin and zero 2nd fanin
- continue;
- if ( pMan->pReprs[i] < 0 )
- continue;
- if ( p->pPars->nLevelMax && (p->pLevel[i] > p->pPars->nLevelMax || p->pLevel[pMan->pReprs[i]] > p->pPars->nLevelMax) )
- continue;
- // create cones
- pRepr = Cec_ManCswCreatePartition_rec( pAig, p, pMan->pReprs[i] );
- pNode = Cec_ManCswCreatePartition_rec( pAig, p, i );
- // skip if they are the same
- if ( Aig_Regular(pRepr) == Aig_Regular(pNode) )
- {
- p->pProvedNow[i] = 1;
- continue;
- }
- // perform speculative reduction
- assert( p->pCopy[i] == pNode );
- p->pCopy[i] = Aig_NotCond( pRepr, Aig_ObjPhaseReal(pRepr) ^ Aig_ObjPhaseReal(pNode) );
- if ( p->pProved[i] )
- {
- p->pProvedNow[i] = 1;
- continue;
- }
- pMiter = Aig_Exor( pAig, pRepr, pNode );
- pTerm = Aig_ObjCreatePo( pAig, Aig_NotCond(pMiter, Aig_ObjPhaseReal(pMiter)) );
- Vec_IntPush( p->vPoNums, i );
- if ( ++Counter > nMitersMin && Aig_ManObjNum(pAig) > nNodesMin )
- break;
- }
- *piStart = i + 1;
- Aig_ManSetRegNum( pAig, 0 );
- Aig_ManCleanup( pAig );
- return pAig;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Cec_ManSatDerivePattern( Cec_ManCsw_t * p, Aig_Man_t * pAig, Aig_Obj_t * pRoot, Cnf_Dat_t * pCnf, sat_solver * pSat )
-{
- Aig_Obj_t * pObj;
- int i, Value, iVar;
- assert( Aig_ObjIsPo(pRoot) );
- Aig_SupportNodes( pAig, &pRoot, 1, p->vSupp );
- Vec_IntClear( p->vPat );
- Vec_PtrForEachEntry( p->vSupp, pObj, i )
- {
- assert( Aig_ObjIsPi(pObj) );
- Value = sat_solver_var_value( pSat, pCnf->pVarNums[pObj->Id] );
- iVar = Vec_IntEntry( p->vPiNums, Aig_ObjPioNum(pObj) );
- assert( iVar >= 0 && iVar < p->p->nPis );
- Vec_IntPush( p->vPat, Cec_Var2Lit( iVar, !Value ) );
- }
-}
-
-/**Function*************************************************************
-
- Synopsis [Creates level.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Cec_ManCreateLevel( Cec_ManCsw_t * p )
-{
- Aig_Obj_t * pObj;
- int i;
- assert( p->pLevel == NULL );
- p->pLevel = ABC_ALLOC( int, p->p->nObjs );
- Aig_ManForEachObj( p->p->pAig, pObj, i )
- p->pLevel[i] = Aig_ObjLevel(pObj);
-}
-
-/**Function*************************************************************
-
- Synopsis [Creates the manager.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Cec_ManCsw_t * Cec_ManCswCreate( Caig_Man_t * pMan, Cec_ParCsw_t * pPars )
-{
- Cec_ManCsw_t * p;
- // create interpolation manager
- p = ABC_ALLOC( Cec_ManCsw_t, 1 );
- memset( p, 0, sizeof(Cec_ManCsw_t) );
- p->pPars = pPars;
- p->p = pMan;
- // internal storage
- p->vCopies = Vec_IntAlloc( 10000 );
- p->pCopy = ABC_CALLOC( Aig_Obj_t *, pMan->nObjs );
- p->pProved = ABC_CALLOC( char, pMan->nObjs );
- p->pProvedNow = ABC_CALLOC( char, pMan->nObjs );
- // temporaries
- p->vPat = Vec_IntAlloc( 1000 );
- p->vSupp = Vec_PtrAlloc( 1000 );
- p->vPiNums = Vec_IntAlloc( 1000 );
- p->vPoNums = Vec_IntAlloc( 1000 );
- if ( pPars->nLevelMax )
- Cec_ManCreateLevel( p );
- return p;
-}
-
-/**Function*************************************************************
-
- Synopsis [Frees the manager.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Cec_ManCswStop( Cec_ManCsw_t * p )
-{
- Vec_IntFree( p->vPiNums );
- Vec_IntFree( p->vPoNums );
- Vec_PtrFree( p->vSupp );
- Vec_IntFree( p->vPat );
- Vec_IntFree( p->vCopies );
- Vec_PtrFree( p->vPres );
- Vec_VecFree( (Vec_Vec_t *)p->vInfoAll );
- ABC_FREE( p->pLevel );
- ABC_FREE( p->pCopy );
- ABC_FREE( p->pProved );
- ABC_FREE( p->pProvedNow );
- ABC_FREE( p );
-}
-
-
-/**Function*************************************************************
-
- Synopsis [Cleans the manager.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Cec_ManCleanSimInfo( Cec_ManCsw_t * p )
-{
- if ( p->vInfoAll )
- Vec_VecFree( (Vec_Vec_t *)p->vInfoAll );
- if ( p->vPres )
- Vec_PtrFree( p->vPres );
- p->vInfoAll = Vec_PtrAlloc( 100 );
- p->vInfo = Vec_PtrAllocSimInfo( p->p->nPis, p->pPars->nWords );
- p->vPres = Vec_PtrAllocSimInfo( p->p->nPis, p->pPars->nWords );
- Vec_PtrCleanSimInfo( p->vInfo, 0, p->p->nWords );
- Vec_PtrCleanSimInfo( p->vPres, 0, p->p->nWords );
- Vec_PtrPush( p->vInfoAll, p->vInfo );
-}
-
-/**Function*************************************************************
-
- Synopsis [Update information about proved nodes.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Cec_ManCountProved( char * pArray, int nSize )
-{
- int i, Counter = 0;
- for ( i = 0; i < nSize; i++ )
- Counter += (pArray[i] == 1);
- return Counter;
-}
-
-/**Function*************************************************************
-
- Synopsis [Update information about proved nodes.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Cec_ManCountDisproved( char * pArray, int nSize )
-{
- int i, Counter = 0;
- for ( i = 0; i < nSize; i++ )
- Counter += (pArray[i] == -1);
- return Counter;
-}
-
-/**Function*************************************************************
-
- Synopsis [Update information about proved nodes.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Cec_ManCountTimedout( char * pArray, int nSize )
-{
- int i, Counter = 0;
- for ( i = 0; i < nSize; i++ )
- Counter += (pArray[i] == -2);
- return Counter;
-}
-
-/**Function*************************************************************
-
- Synopsis [Update information about proved nodes.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Cec_ManUpdateProved( Cec_ManCsw_t * p )
-{
- Caig_Man_t * pMan = p->p;
- int i;
- for ( i = 1; i < pMan->nObjs; i++ )
- {
- if ( pMan->pFans0[i] == -1 ) // pi always has zero first fanin
- continue;
- if ( pMan->pFans1[i] == -1 ) // po always has non-zero 1st fanin and zero 2nd fanin
- continue;
- if ( p->pProvedNow[Cec_Lit2Var(pMan->pFans0[i])] < 0 ||
- p->pProvedNow[Cec_Lit2Var(pMan->pFans1[i])] < 0 )
- p->pProvedNow[i] = -1;
- if ( pMan->pReprs[i] < 0 )
- {
- assert( p->pProvedNow[i] <= 0 );
- continue;
- }
- if ( p->pProved[i] )
- {
- assert( p->pProvedNow[i] == 1 );
- continue;
- }
- if ( p->pProvedNow[i] == 1 )
- p->pProved[i] = 1;
- }
-}
-
-/**Function*************************************************************
-
- Synopsis [Creates dynamic partition.]
-
- Description [PIs point to node IDs. POs point to node IDs.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Cec_ManSatSweepRound( Cec_ManCsw_t * p )
-{
- Bar_Progress_t * pProgress = NULL;
- Vec_Ptr_t * vInfo;
- Aig_Man_t * pAig, * pTemp;
- Aig_Obj_t * pObj;
- Cnf_Dat_t * pCnf;
- sat_solver * pSat;
- int i, Lit, iNode, iStart, status;
- int nProved, nDisproved, nTimedout, nBefore, nAfter, nRecycles = 0;
- int clk = clock();
- Cec_ManCleanSimInfo( p );
- memset( p->pProvedNow, 0, sizeof(char) * p->p->nObjs );
- pProgress = Bar_ProgressStart( stdout, p->p->nObjs );
- for ( iStart = 1; iStart < p->p->nObjs; )
- {
- Bar_ProgressUpdate( pProgress, iStart, "Sweep..." );
- Vec_IntClear( p->vPiNums );
- Vec_IntClear( p->vPoNums );
- // generate AIG, synthesize, convert to CNF, and solve
- pAig = Cec_ManCswCreatePartition( p, &iStart, p->pPars->nCallsRecycle, p->pPars->nSatVarMax, p->pPars->nLevelMax );
- Aig_ManPrintStats( pAig );
-
- if ( p->pPars->fRewriting )
- {
- pAig = Dar_ManRwsat( pTemp = pAig, 1, 0 );
- Aig_ManStop( pTemp );
- }
- pCnf = Cnf_Derive( pAig, Aig_ManPoNum(pAig) );
- pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
- Aig_ManForEachPo( pAig, pObj, i )
- {
- iNode = Vec_IntEntry( p->vPoNums, i );
- Lit = toLitCond( pCnf->pVarNums[pObj->Id], 0 );
- status = sat_solver_solve( pSat, &Lit, &Lit + 1, (ABC_INT64_T)p->pPars->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
- if ( status == l_False )
- p->pProvedNow[iNode] = 1;
- else if ( status == l_Undef )
- p->pProvedNow[iNode] = -2;
- else if ( status == l_True )
- {
- p->pProvedNow[iNode] = -1;
- Cec_ManSatDerivePattern( p, pAig, pObj, pCnf, pSat );
- Cec_ManSavePattern( p, p->vPat );
- }
- }
- // clean up
- Aig_ManStop( pAig );
- Cnf_DataFree( pCnf );
- sat_solver_delete( pSat );
- nRecycles++;
- }
- Bar_ProgressStop( pProgress );
- // collect statistics
- nProved = Cec_ManCountProved( p->pProvedNow, p->p->nObjs );
- nDisproved = Cec_ManCountDisproved( p->pProvedNow, p->p->nObjs );
- nTimedout = Cec_ManCountTimedout( p->pProvedNow, p->p->nObjs );
- nBefore = Cec_ManCountProved( p->pProved, p->p->nObjs );
- Cec_ManUpdateProved( p );
- nAfter = Cec_ManCountProved( p->pProved, p->p->nObjs );
- printf( "Pr =%6d. Cex =%6d. Fail =%6d. Bef =%6d. Aft =%6d. Rcl =%4d.",
- nProved, nDisproved, nTimedout, nBefore, nAfter, nRecycles );
- ABC_PRT( "Time", clock() - clk );
- // resimulate with the collected information
- Vec_PtrForEachEntry( p->vInfoAll, vInfo, i )
- Caig_ManSimulateRound( p->p, vInfo, NULL );
-Caig_ManPrintClasses( p->p, 0 );
-}
-
-/**Function*************************************************************
-
- Synopsis [Performs one round of sweeping.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Cec_ManSatSweepInt( Caig_Man_t * pMan, Cec_ParCsw_t * pPars )
-{
- Cec_ManCsw_t * p;
- p = Cec_ManCswCreate( pMan, pPars );
- Cec_ManSatSweepRound( p );
- Cec_ManCswStop( p );
-}
-
-
-/**Function*************************************************************
-
- Synopsis [Performs equivalence checking.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Aig_Man_t * Cec_ManTrasferReprs( Aig_Man_t * pAig, Caig_Man_t * pCaig )
-{
- return NULL;
-}
-
-/**Function*************************************************************
-
- Synopsis [Performs equivalence checking.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Aig_Man_t * Cec_ManSatSweep( Aig_Man_t * pAig, Cec_ParCsw_t * pPars )
-{
-/*
- Aig_Man_t * pAigNew, * pAigDfs;
- Caig_Man_t * pCaig;
- Cec_ManCsw_t * p;
- pAigDfs = Cec_Duplicate( pAig );
- pCaig = Caig_ManClassesPrepare( pAigDfs, pPars->nWords, pPars->nRounds );
- p = Cec_ManCswCreate( pCaig, pPars );
- Cec_ManSatSweep( p, pPars );
- Cec_ManCswStop( p );
-// pAigNew =
- Caig_ManDelete( pCaig );
- Aig_ManStop( pAigDfs );
- return pAigNew;
-*/
- return NULL;
-}
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/aig/cec2/module.make b/src/aig/cec2/module.make
deleted file mode 100644
index 537397e3..00000000
--- a/src/aig/cec2/module.make
+++ /dev/null
@@ -1,9 +0,0 @@
-SRC += src/aig/cec/cecAig.c \
- src/aig/cec/cecClass.c \
- src/aig/cec/cecCnf.c \
- src/aig/cec/cecCore.c \
- src/aig/cec/cecMan.c \
- src/aig/cec/cecSat.c \
- src/aig/cec/cecSim.c \
- src/aig/cec/cecStatus.c \
- src/aig/cec/cecSweep.c
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 91507947..c5d55565 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -80,6 +80,7 @@ struct Gia_Cex_t_
unsigned pData[0]; // the cex bit data (the number of bits: nRegs + (iFrame+1) * nPis)
};
+// new AIG manager
typedef struct Gia_Man_t_ Gia_Man_t;
struct Gia_Man_t_
{
@@ -109,6 +110,7 @@ struct Gia_Man_t_
int nFansAlloc; // the size of fanout representation
int * pMapping; // mapping for each node
Gia_Cex_t * pCexComb; // combinational counter-example
+ int * pCopies; // intermediate copies
};
@@ -446,7 +448,7 @@ extern Gia_Man_t * Gia_ManDupCofactored( Gia_Man_t * p, int iVar, int nL
extern Gia_Man_t * Gia_ManDupDfsCiMap( Gia_Man_t * p, int * pCi2Lit, Vec_Int_t * vLits );
extern Gia_Man_t * Gia_ManDupDfsClasses( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManDupTopAnd( Gia_Man_t * p, int fVerbose );
-extern Gia_Man_t * Gia_ManMiter( Gia_Man_t * pAig0, Gia_Man_t * pAig1, int fXorOuts, int fComb, int fVerbose );
+extern Gia_Man_t * Gia_ManMiter( Gia_Man_t * pAig0, Gia_Man_t * pAig1, int fDualOut, int fSeq, int fVerbose );
extern Gia_Man_t * Gia_ManTransformMiter( Gia_Man_t * p );
/*=== giaEnable.c ==========================================================*/
extern void Gia_ManDetectSeqSignals( Gia_Man_t * p, int fSetReset );
@@ -454,9 +456,11 @@ extern void Gia_ManDetectSeqSignals( Gia_Man_t * p, int fSetReset
extern int * Gia_ManDeriveNexts( Gia_Man_t * p );
extern void Gia_ManEquivPrintOne( Gia_Man_t * p, int i, int Counter );
extern void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem );
+extern Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll );
extern Gia_Man_t * Gia_ManEquivReduceAndRemap( Gia_Man_t * p, int fSeq, int fMiterPairs );
extern int Gia_ManEquivSetColors( Gia_Man_t * p, int fVerbose );
-extern Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p );
+extern Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut );
+extern Gia_Man_t * Gia_ManSpecReduceInit( Gia_Man_t * p, Gia_Cex_t * pInit, int nFrames, int fDualOut );
extern void Gia_ManEquivTransform( Gia_Man_t * p, int fVerbose );
/*=== giaFanout.c =========================================================*/
extern void Gia_ObjAddFanout( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pFanout );
@@ -526,7 +530,10 @@ extern Vec_Int_t * Gia_ManCollectPoIds( Gia_Man_t * p );
extern int Gia_ObjIsMuxType( Gia_Obj_t * pNode );
extern int Gia_ObjRecognizeExor( Gia_Obj_t * pObj, Gia_Obj_t ** ppFan0, Gia_Obj_t ** ppFan1 );
extern Gia_Obj_t * Gia_ObjRecognizeMux( Gia_Obj_t * pNode, Gia_Obj_t ** ppNodeT, Gia_Obj_t ** ppNodeE );
-extern int Gia_ManVerifyCounterExample( Gia_Man_t * pAig, Gia_Cex_t * p, int fDoubleOuts );
+extern Gia_Cex_t * Gia_ManAllocCounterExample( int nRegs, int nRealPis, int nFrames );
+extern int Gia_ManVerifyCounterExample( Gia_Man_t * pAig, Gia_Cex_t * p, int fDualOut );
+extern void Gia_ManPrintCounterExample( Gia_Cex_t * p );
+
#ifdef __cplusplus
}
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index 4821dba9..1d940b78 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -756,25 +756,12 @@ int Gia_ManMiter_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
SeeAlso []
***********************************************************************/
-Gia_Man_t * Gia_ManMiter( Gia_Man_t * p0, Gia_Man_t * p1, int fXorOuts, int fComb, int fVerbose )
+Gia_Man_t * Gia_ManMiter( Gia_Man_t * p0, Gia_Man_t * p1, int fDualOut, int fSeq, int fVerbose )
{
Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj;
int i, iLit;
- if ( fComb )
- {
- if ( Gia_ManCiNum(p0) != Gia_ManCiNum(p1) )
- {
- printf( "Gia_ManMiter(): Designs have different number of CIs.\n" );
- return NULL;
- }
- if ( Gia_ManCoNum(p0) != Gia_ManCoNum(p1) )
- {
- printf( "Gia_ManMiter(): Designs have different number of COs.\n" );
- return NULL;
- }
- }
- else
+ if ( fSeq )
{
if ( Gia_ManPiNum(p0) != Gia_ManPiNum(p1) )
{
@@ -792,6 +779,19 @@ Gia_Man_t * Gia_ManMiter( Gia_Man_t * p0, Gia_Man_t * p1, int fXorOuts, int fCom
return NULL;
}
}
+ else
+ {
+ if ( Gia_ManCiNum(p0) != Gia_ManCiNum(p1) )
+ {
+ printf( "Gia_ManMiter(): Designs have different number of CIs.\n" );
+ return NULL;
+ }
+ if ( Gia_ManCoNum(p0) != Gia_ManCoNum(p1) )
+ {
+ printf( "Gia_ManMiter(): Designs have different number of COs.\n" );
+ return NULL;
+ }
+ }
// start the manager
pNew = Gia_ManStart( Gia_ManObjNum(p0) + Gia_ManObjNum(p1) );
pNew->pName = Aig_UtilStrsav( "miter" );
@@ -802,31 +802,7 @@ Gia_Man_t * Gia_ManMiter( Gia_Man_t * p0, Gia_Man_t * p1, int fXorOuts, int fCom
Gia_ManConst0(p1)->Value = 0;
// map internal nodes and outputs
Gia_ManHashAlloc( pNew );
- if ( fComb )
- {
- // create combinational inputs
- Gia_ManForEachCi( p0, pObj, i )
- pObj->Value = Gia_ManAppendCi( pNew );
- Gia_ManForEachCi( p1, pObj, i )
- pObj->Value = Gia_ObjToLit( pNew, Gia_ManCi(pNew, i) );
- // create combinational outputs
- Gia_ManForEachCo( p0, pObj, i )
- {
- Gia_ManMiter_rec( pNew, p0, Gia_ObjFanin0(pObj) );
- Gia_ManMiter_rec( pNew, p1, Gia_ObjFanin0(Gia_ManCo(p1,i)) );
- if ( fXorOuts )
- {
- iLit = Gia_ManHashXor( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin0Copy(Gia_ManCo(p1,i)) );
- Gia_ManAppendCo( pNew, iLit );
- }
- else
- {
- Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
- Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(Gia_ManCo(p1,i)) );
- }
- }
- }
- else
+ if ( fSeq )
{
// create primary inputs
Gia_ManForEachPi( p0, pObj, i )
@@ -843,15 +819,15 @@ Gia_Man_t * Gia_ManMiter( Gia_Man_t * p0, Gia_Man_t * p1, int fXorOuts, int fCom
{
Gia_ManMiter_rec( pNew, p0, Gia_ObjFanin0(pObj) );
Gia_ManMiter_rec( pNew, p1, Gia_ObjFanin0(Gia_ManPo(p1,i)) );
- if ( fXorOuts )
+ if ( fDualOut )
{
- iLit = Gia_ManHashXor( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin0Copy(Gia_ManPo(p1,i)) );
- Gia_ManAppendCo( pNew, iLit );
+ Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+ Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(Gia_ManPo(p1,i)) );
}
else
{
- Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
- Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(Gia_ManPo(p1,i)) );
+ iLit = Gia_ManHashXor( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin0Copy(Gia_ManPo(p1,i)) );
+ Gia_ManAppendCo( pNew, iLit );
}
}
// create register inputs
@@ -867,6 +843,30 @@ Gia_Man_t * Gia_ManMiter( Gia_Man_t * p0, Gia_Man_t * p1, int fXorOuts, int fCom
}
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p0) + Gia_ManRegNum(p1) );
}
+ else
+ {
+ // create combinational inputs
+ Gia_ManForEachCi( p0, pObj, i )
+ pObj->Value = Gia_ManAppendCi( pNew );
+ Gia_ManForEachCi( p1, pObj, i )
+ pObj->Value = Gia_ObjToLit( pNew, Gia_ManCi(pNew, i) );
+ // create combinational outputs
+ Gia_ManForEachCo( p0, pObj, i )
+ {
+ Gia_ManMiter_rec( pNew, p0, Gia_ObjFanin0(pObj) );
+ Gia_ManMiter_rec( pNew, p1, Gia_ObjFanin0(Gia_ManCo(p1,i)) );
+ if ( fDualOut )
+ {
+ Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+ Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(Gia_ManCo(p1,i)) );
+ }
+ else
+ {
+ iLit = Gia_ManHashXor( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin0Copy(Gia_ManCo(p1,i)) );
+ Gia_ManAppendCo( pNew, iLit );
+ }
+ }
+ }
Gia_ManHashStop( pNew );
pNew = Gia_ManCleanup( pTemp = pNew );
Gia_ManStop( pTemp );
diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c
index 9e190da3..acdd3c13 100644
--- a/src/aig/gia/giaEquiv.c
+++ b/src/aig/gia/giaEquiv.c
@@ -156,13 +156,13 @@ int Gia_ManEquivCheckLits( Gia_Man_t * p, int nLits )
***********************************************************************/
void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem )
{
- int i, Counter = 0, Counter1 = 0, CounterX = 0, Proved = 0, nLits;
+ int i, Counter = 0, Counter0 = 0, CounterX = 0, Proved = 0, nLits;
for ( i = 1; i < Gia_ManObjNum(p); i++ )
{
if ( Gia_ObjIsHead(p, i) )
Counter++;
else if ( Gia_ObjIsConst(p, i) )
- Counter1++;
+ Counter0++;
else if ( Gia_ObjIsNone(p, i) )
CounterX++;
if ( Gia_ObjProved(p, i) )
@@ -170,8 +170,8 @@ void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem )
}
CounterX -= Gia_ManCoNum(p);
nLits = Gia_ManCiNum(p) + Gia_ManAndNum(p) - Counter - CounterX;
- printf( "cls =%7d cst =%8d lit =%8d unused =%8d proof =%6d mem =%5.2f Mb\n",
- Counter, Counter1, nLits, CounterX, Proved, (Mem == 0.0) ? 8.0*Gia_ManObjNum(p)/(1<<20) : Mem );
+ printf( "cst =%8d cls =%7d lit =%8d unused =%8d proof =%6d mem =%5.2f Mb\n",
+ Counter0, Counter, nLits, CounterX, Proved, (Mem == 0.0) ? 8.0*Gia_ManObjNum(p)/(1<<20) : Mem );
assert( Gia_ManEquivCheckLits( p, nLits ) );
if ( fVerbose )
{
@@ -192,10 +192,18 @@ void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem )
SeeAlso []
***********************************************************************/
-static inline Gia_Obj_t * Gia_ManEquivRepr( Gia_Man_t * p, Gia_Obj_t * pObj )
+static inline Gia_Obj_t * Gia_ManEquivRepr( Gia_Man_t * p, Gia_Obj_t * pObj, int fUseAll )
{
- if ( !Gia_ObjProved(p, Gia_ObjId(p,pObj)) )
- return NULL;
+ if ( fUseAll )
+ {
+ if ( Gia_ObjRepr(p, Gia_ObjId(p,pObj)) == GIA_VOID )
+ return NULL;
+ }
+ else
+ {
+ if ( !Gia_ObjProved(p, Gia_ObjId(p,pObj)) )
+ return NULL;
+ }
return Gia_ManObj( p, Gia_ObjRepr(p, Gia_ObjId(p,pObj)) );
}
@@ -210,20 +218,20 @@ static inline Gia_Obj_t * Gia_ManEquivRepr( Gia_Man_t * p, Gia_Obj_t * pObj )
SeeAlso []
***********************************************************************/
-void Gia_ManEquivReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
+void Gia_ManEquivReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int fUseAll )
{
Gia_Obj_t * pRepr;
if ( ~pObj->Value )
return;
assert( Gia_ObjIsAnd(pObj) );
- if ( (pRepr = Gia_ManEquivRepr(p, pObj)) )
+ if ( (pRepr = Gia_ManEquivRepr(p, pObj, fUseAll)) )
{
- Gia_ManEquivReduce_rec( pNew, p, pRepr );
+ Gia_ManEquivReduce_rec( pNew, p, pRepr, fUseAll );
pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
return;
}
- Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin0(pObj) );
- Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin1(pObj) );
+ Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin0(pObj), fUseAll );
+ Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin1(pObj), fUseAll );
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
}
@@ -238,7 +246,7 @@ void Gia_ManEquivReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
SeeAlso []
***********************************************************************/
-Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p )
+Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll )
{
Gia_Man_t * pNew;
Gia_Obj_t * pObj, * pRepr;
@@ -251,12 +259,12 @@ Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p )
Gia_ManForEachCi( p, pObj, i )
{
pObj->Value = Gia_ManAppendCi(pNew);
- if ( (pRepr = Gia_ManEquivRepr(p, pObj)) )
+ if ( (pRepr = Gia_ManEquivRepr(p, pObj, fUseAll)) )
pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
}
Gia_ManHashAlloc( pNew );
Gia_ManForEachCo( p, pObj, i )
- Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin0(pObj) );
+ Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin0(pObj), fUseAll );
Gia_ManForEachCo( p, pObj, i )
Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
Gia_ManHashStop( pNew );
@@ -390,7 +398,7 @@ void Gia_ManEquivDeriveReprs( Gia_Man_t * p, Gia_Man_t * pNew, Gia_Man_t * pFina
Gia_Man_t * Gia_ManEquivReduceAndRemap( Gia_Man_t * p, int fSeq, int fMiterPairs )
{
Gia_Man_t * pNew, * pFinal;
- pNew = Gia_ManEquivReduce( p );
+ pNew = Gia_ManEquivReduce( p, 0 );
if ( fMiterPairs )
Gia_ManEquivFixOutputPairs( pNew );
if ( fSeq )
@@ -474,27 +482,43 @@ int Gia_ManEquivSetColors( Gia_Man_t * p, int fVerbose )
SeeAlso []
***********************************************************************/
-void Gia_ManSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits )
+static inline void Gia_ManSpecBuild( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits )
{
Gia_Obj_t * pRepr;
- int iLitNew;
- if ( ~pObj->Value )
- return;
- assert( Gia_ObjIsAnd(pObj) );
- Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits );
- Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj), vXorLits );
- pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+ unsigned iLitNew;
pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
if ( pRepr == NULL )
return;
iLitNew = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
- if ( pObj->Value != (unsigned)iLitNew && !Gia_ObjProved(p, Gia_ObjId(p,pObj)) )
+ if ( pObj->Value != iLitNew && !Gia_ObjProved(p, Gia_ObjId(p,pObj)) )
Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, pObj->Value, iLitNew) );
pObj->Value = iLitNew;
}
/**Function*************************************************************
+ Synopsis [Duplicates the AIG in the DFS order.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Gia_ManSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits )
+{
+ if ( ~pObj->Value )
+ return;
+ assert( Gia_ObjIsAnd(pObj) );
+ Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits );
+ Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj), vXorLits );
+ pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+ Gia_ManSpecBuild( pNew, p, pObj, vXorLits );
+}
+
+/**Function*************************************************************
+
Synopsis [Reduces AIG using equivalence classes.]
Description []
@@ -504,33 +528,28 @@ void Gia_ManSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, V
SeeAlso []
***********************************************************************/
-Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p )
+Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut )
{
Gia_Man_t * pNew, * pTemp;
- Gia_Obj_t * pObj, * pRepr;
+ Gia_Obj_t * pObj;
Vec_Int_t * vXorLits;
int i, iLitNew;
if ( !p->pReprs )
+ {
+ printf( "Gia_ManSpecReduce(): Equivalence classes are not available.\n" );
return NULL;
+ }
vXorLits = Vec_IntAlloc( 1000 );
Gia_ManSetPhase( p );
+ Gia_ManFillValue( p );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
- Gia_ManFillValue( p );
+ Gia_ManHashAlloc( pNew );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
- Gia_ManHashAlloc( pNew );
- Gia_ManForEachCi( p, pObj, i )
- {
- pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
- if ( pRepr == NULL )
- continue;
- iLitNew = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
- if ( pObj->Value != (unsigned)iLitNew && !Gia_ObjProved(p, Gia_ObjId(p,pObj)) )
- Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, pObj->Value, iLitNew) );
- pObj->Value = iLitNew;
- }
+ Gia_ManForEachRo( p, pObj, i )
+ Gia_ManSpecBuild( pNew, p, pObj, vXorLits );
Gia_ManForEachCo( p, pObj, i )
Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits );
Vec_IntForEachEntry( vXorLits, iLitNew, i )
@@ -542,14 +561,140 @@ Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p )
}
Gia_ManForEachRi( p, pObj, i )
Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
- Vec_IntFree( vXorLits );
Gia_ManHashStop( pNew );
+ Vec_IntFree( vXorLits );
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
pNew = Gia_ManCleanup( pTemp = pNew );
Gia_ManStop( pTemp );
return pNew;
}
+
+static inline int Gia_ObjSpec( Gia_Man_t * p, int f, Gia_Obj_t * pObj ) { return p->pCopies[Gia_ManObjNum(p) * f + Gia_ObjId(p,pObj)]; }
+static inline void Gia_ObjSetSpec( Gia_Man_t * p, int f, Gia_Obj_t * pObj, int iLit ) { p->pCopies[Gia_ManObjNum(p) * f + Gia_ObjId(p,pObj)] = iLit; }
+
+static inline int Gia_ObjChild0Spec( Gia_Man_t * p, int f, Gia_Obj_t * pObj ) { return Gia_LitNotCond(Gia_ObjSpec(p, f, Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj)); }
+static inline int Gia_ObjChild1Spec( Gia_Man_t * p, int f, Gia_Obj_t * pObj ) { return Gia_LitNotCond(Gia_ObjSpec(p, f, Gia_ObjFanin1(pObj)), Gia_ObjFaninC1(pObj)); }
+
+/**Function*************************************************************
+
+ Synopsis [Duplicates the AIG in the DFS order.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Gia_ManSpecBuildInit( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits, int f )
+{
+ Gia_Obj_t * pRepr;
+ int iLitNew;
+ pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
+ if ( pRepr == NULL )
+ return;
+ iLitNew = Gia_LitNotCond( Gia_ObjSpec(p, f, pRepr), Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
+ if ( Gia_ObjSpec(p, f, pObj) != iLitNew && !Gia_ObjProved(p, Gia_ObjId(p,pObj)) )
+ Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, Gia_ObjSpec(p, f, pObj), iLitNew) );
+ Gia_ObjSetSpec( p, f, pObj, iLitNew );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Duplicates the AIG in the DFS order.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Gia_ManSpecReduceInit_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits, int f )
+{
+ if ( ~Gia_ObjSpec(p, f, pObj) )
+ return;
+ assert( Gia_ObjIsAnd(pObj) );
+ Gia_ManSpecReduceInit_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, f );
+ Gia_ManSpecReduceInit_rec( pNew, p, Gia_ObjFanin1(pObj), vXorLits, f );
+ Gia_ObjSetSpec( p, f, pObj, Gia_ManHashAnd(pNew, Gia_ObjChild0Spec(p, f, pObj), Gia_ObjChild1Spec(p, f, pObj)) );
+ Gia_ManSpecBuildInit( pNew, p, pObj, vXorLits, f );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Creates initialized SRM with the given number of frames.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManSpecReduceInit( Gia_Man_t * p, Gia_Cex_t * pInit, int nFrames, int fDualOut )
+{
+ Gia_Man_t * pNew, * pTemp;
+ Gia_Obj_t * pObj, * pObjRi, * pObjRo;
+ Vec_Int_t * vXorLits;
+ int f, i, iLitNew;
+ if ( !p->pReprs )
+ {
+ printf( "Gia_ManSpecReduceInit(): Equivalence classes are not available.\n" );
+ return NULL;
+ }
+ if ( Gia_ManRegNum(p) == 0 )
+ {
+ printf( "Gia_ManSpecReduceInit(): Circuit is not sequential.\n" );
+ return NULL;
+ }
+ if ( Gia_ManRegNum(p) != pInit->nRegs )
+ {
+ printf( "Gia_ManSpecReduceInit(): Mismatch in the number of registers.\n" );
+ return NULL;
+ }
+ assert( pInit->nRegs == Gia_ManRegNum(p) && pInit->nPis == 0 );
+ p->pCopies = ABC_FALLOC( int, nFrames * Gia_ManObjNum(p) );
+ vXorLits = Vec_IntAlloc( 1000 );
+ Gia_ManSetPhase( p );
+ pNew = Gia_ManStart( nFrames * Gia_ManObjNum(p) );
+ pNew->pName = Aig_UtilStrsav( p->pName );
+ Gia_ManHashAlloc( pNew );
+ Gia_ManForEachRo( p, pObj, i )
+ Gia_ObjSetSpec( p, 0, pObj, Aig_InfoHasBit(pInit->pData, i) );
+ for ( f = 0; f < nFrames; f++ )
+ {
+ Gia_ObjSetSpec( p, f, Gia_ManConst0(p), 0 );
+ Gia_ManForEachPi( p, pObj, i )
+ Gia_ObjSetSpec( p, f, pObj, Gia_ManAppendCi(pNew) );
+ Gia_ManForEachRo( p, pObj, i )
+ Gia_ManSpecBuildInit( pNew, p, pObj, vXorLits, f );
+ Gia_ManForEachCo( p, pObj, i )
+ {
+ Gia_ManSpecReduceInit_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, f );
+ Gia_ObjSetSpec( p, f, pObj, Gia_ObjChild0Spec(p, f, pObj) );
+ }
+ if ( f == nFrames - 1 )
+ break;
+ Gia_ManForEachRiRo( p, pObjRi, pObjRo, i )
+ Gia_ObjSetSpec( p, f+1, pObjRo, Gia_ObjSpec(p, f, pObjRi) );
+ }
+ Vec_IntForEachEntry( vXorLits, iLitNew, i )
+ Gia_ManAppendCo( pNew, iLitNew );
+ if ( Vec_IntSize(vXorLits) == 0 )
+ {
+ printf( "Speculatively reduced model has no primary outputs.\n" );
+ Gia_ManAppendCo( pNew, 0 );
+ }
+ ABC_FREE( p->pCopies );
+ Vec_IntFree( vXorLits );
+ Gia_ManHashStop( pNew );
+ pNew = Gia_ManCleanup( pTemp = pNew );
+ Gia_ManStop( pTemp );
+ return pNew;
+}
+
/**Function*************************************************************
Synopsis [Transforms equiv classes by removing the AB nodes.]
diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c
index cc1a3861..822f1e64 100644
--- a/src/aig/gia/giaUtil.c
+++ b/src/aig/gia/giaUtil.c
@@ -580,6 +580,29 @@ Gia_Obj_t * Gia_ObjRecognizeMux( Gia_Obj_t * pNode, Gia_Obj_t ** ppNodeT, Gia_Ob
/**Function*************************************************************
+ Synopsis [Allocates a counter-example.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Gia_Cex_t * Gia_ManAllocCounterExample( int nRegs, int nRealPis, int nFrames )
+{
+ Gia_Cex_t * pCex;
+ int nWords = Aig_BitWordNum( nRegs + nRealPis * nFrames );
+ pCex = (Gia_Cex_t *)ABC_ALLOC( char, sizeof(Gia_Cex_t) + sizeof(unsigned) * nWords );
+ memset( pCex, 0, sizeof(Gia_Cex_t) + sizeof(unsigned) * nWords );
+ pCex->nRegs = nRegs;
+ pCex->nPis = nRealPis;
+ pCex->nBits = nRegs + nRealPis * nFrames;
+ return pCex;
+}
+
+/**Function*************************************************************
+
Synopsis [Resimulates the counter-example.]
Description []
@@ -589,7 +612,7 @@ Gia_Obj_t * Gia_ObjRecognizeMux( Gia_Obj_t * pNode, Gia_Obj_t ** ppNodeT, Gia_Ob
SeeAlso []
***********************************************************************/
-int Gia_ManVerifyCounterExample( Gia_Man_t * pAig, Gia_Cex_t * p, int fDoubleOuts )
+int Gia_ManVerifyCounterExample( Gia_Man_t * pAig, Gia_Cex_t * p, int fDualOut )
{
Gia_Obj_t * pObj, * pObjRi, * pObjRo;
int RetValue, i, k, iBit = 0;
@@ -608,7 +631,7 @@ int Gia_ManVerifyCounterExample( Gia_Man_t * pAig, Gia_Cex_t * p, int fDoubleOut
pObjRo->fMark0 = pObjRi->fMark0;
}
assert( iBit == p->nBits );
- if ( fDoubleOuts )
+ if ( fDualOut )
RetValue = Gia_ManPo(pAig, 2*p->iPo)->fMark0 ^ Gia_ManPo(pAig, 2*p->iPo+1)->fMark0;
else
RetValue = Gia_ManPo(pAig, p->iPo)->fMark0;
@@ -616,6 +639,36 @@ int Gia_ManVerifyCounterExample( Gia_Man_t * pAig, Gia_Cex_t * p, int fDoubleOut
return RetValue;
}
+/**Function*************************************************************
+
+ Synopsis [Prints out the counter-example.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Gia_ManPrintCounterExample( Gia_Cex_t * p )
+{
+ int i, f, k;
+ printf( "Counter-example: iPo = %d iFrame = %d nRegs = %d nPis = %d nBits = %d\n",
+ p->iPo, p->iFrame, p->nRegs, p->nPis, p->nBits );
+ printf( "State : " );
+ for ( k = 0; k < p->nRegs; k++ )
+ printf( "%d", Aig_InfoHasBit(p->pData, k) );
+ printf( "\n" );
+ for ( f = 0; f <= p->iFrame; f++ )
+ {
+ printf( "Frame %2d : ", f );
+ for ( i = 0; i < p->nPis; i++ )
+ printf( "%d", Aig_InfoHasBit(p->pData, k++) );
+ printf( "\n" );
+ }
+ assert( k == p->nBits );
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 1164c3da..3045eb93 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -288,7 +288,9 @@ static int Abc_CommandAbc9Cof ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandAbc9Trim ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Dfs ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Sim ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Resim ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Equiv ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Semi ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Times ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Frames ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Miter ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -296,6 +298,7 @@ static int Abc_CommandAbc9Scl ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandAbc9Sat ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Fraig ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Srm ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Reduce ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Cec ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Force ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Embed ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -596,7 +599,9 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "AIG", "&trim", Abc_CommandAbc9Trim, 0 );
Cmd_CommandAdd( pAbc, "AIG", "&dfs", Abc_CommandAbc9Dfs, 0 );
Cmd_CommandAdd( pAbc, "AIG", "&sim", Abc_CommandAbc9Sim, 0 );
+ Cmd_CommandAdd( pAbc, "AIG", "&resim", Abc_CommandAbc9Resim, 0 );
Cmd_CommandAdd( pAbc, "AIG", "&equiv", Abc_CommandAbc9Equiv, 0 );
+ Cmd_CommandAdd( pAbc, "AIG", "&semi", Abc_CommandAbc9Semi, 0 );
Cmd_CommandAdd( pAbc, "AIG", "&times", Abc_CommandAbc9Times, 0 );
Cmd_CommandAdd( pAbc, "AIG", "&frames", Abc_CommandAbc9Frames, 0 );
Cmd_CommandAdd( pAbc, "AIG", "&miter", Abc_CommandAbc9Miter, 0 );
@@ -604,6 +609,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "AIG", "&sat", Abc_CommandAbc9Sat, 0 );
Cmd_CommandAdd( pAbc, "AIG", "&fraig", Abc_CommandAbc9Fraig, 0 );
Cmd_CommandAdd( pAbc, "AIG", "&srm", Abc_CommandAbc9Srm, 0 );
+ Cmd_CommandAdd( pAbc, "AIG", "&reduce", Abc_CommandAbc9Reduce, 0 );
Cmd_CommandAdd( pAbc, "AIG", "&cec", Abc_CommandAbc9Cec, 0 );
Cmd_CommandAdd( pAbc, "AIG", "&force", Abc_CommandAbc9Force, 0 );
Cmd_CommandAdd( pAbc, "AIG", "&embed", Abc_CommandAbc9Embed, 0 );
@@ -15904,8 +15910,8 @@ usage:
fprintf( pErr, "\t-P num : partition size for multi-output networks [default = %s]\n", Buffer );
fprintf( pErr, "\t-p : toggle automatic partitioning [default = %s]\n", fPartition? "yes": "no" );
fprintf( pErr, "\t-s : toggle \"SAT only\" and \"FRAIG + SAT\" [default = %s]\n", fSat? "SAT only": "FRAIG + SAT" );
- fprintf( pErr, "\t-n : toggle using names to match CIs/COs [default = %s]\n", fIgnoreNames? "yes": "no" );
- fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
+ fprintf( pErr, "\t-n : toggle ignoring names when matching CIs/COs [default = %s]\n", fIgnoreNames? "yes": "no" );
+ fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
fprintf( pErr, "\tfile1 : (optional) the file with the first network\n");
fprintf( pErr, "\tfile2 : (optional) the file with the second network\n");
@@ -16236,6 +16242,7 @@ int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv )
char ** pArgvNew;
int nArgcNew;
int c;
+ int fIgnoreNames;
extern void Fra_SecSetDefaultParams( Fra_Sec_t * p );
extern int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Fra_Sec_t * p );
@@ -16247,8 +16254,9 @@ int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
Fra_SecSetDefaultParams( pSecPar );
pSecPar->TimeLimit = 0;
+ fIgnoreNames = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "FTarmfwvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "FTarmfnwvh" ) ) != EOF )
{
switch ( c )
{
@@ -16286,6 +16294,9 @@ int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'f':
pSecPar->fFraiging ^= 1;
break;
+ case 'n':
+ fIgnoreNames ^= 1;
+ break;
case 'w':
pSecPar->fVeryVerbose ^= 1;
break;
@@ -16308,6 +16319,12 @@ int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv )
printf( "The network has no latches. Used combinational command \"cec\".\n" );
return 0;
}
+
+ if ( fIgnoreNames )
+ {
+ Abc_NtkShortNames( pNtk1 );
+ Abc_NtkShortNames( pNtk2 );
+ }
// perform verification
Abc_NtkDarSec( pNtk1, pNtk2, pSecPar );
@@ -16317,7 +16334,7 @@ int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- fprintf( pErr, "usage: dsec [-F num] [-T num] [-armfwvh] <file1> <file2>\n" );
+ fprintf( pErr, "usage: dsec [-F num] [-T num] [-armfnwvh] <file1> <file2>\n" );
fprintf( pErr, "\t performs inductive sequential equivalence checking\n" );
fprintf( pErr, "\t-F num : the limit on the depth of induction [default = %d]\n", pSecPar->nFramesMax );
fprintf( pErr, "\t-T num : the approximate runtime limit (in seconds) [default = %d]\n", pSecPar->TimeLimit );
@@ -16325,6 +16342,7 @@ usage:
fprintf( pErr, "\t-r : toggles forward retiming at the beginning [default = %s]\n", pSecPar->fRetimeFirst? "yes": "no" );
fprintf( pErr, "\t-m : toggles min-register retiming [default = %s]\n", pSecPar->fRetimeRegs? "yes": "no" );
fprintf( pErr, "\t-f : toggles the internal use of fraiging [default = %s]\n", pSecPar->fFraiging? "yes": "no" );
+ fprintf( pErr, "\t-n : toggle ignoring names when matching PIs/POs [default = %s]\n", fIgnoreNames? "yes": "no" );
fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", pSecPar->fVerbose? "yes": "no" );
fprintf( pErr, "\t-w : toggles additional verbose output [default = %s]\n", pSecPar->fVeryVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
@@ -16479,6 +16497,11 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv )
goto usage;
}
}
+ if ( pNtk == NULL )
+ {
+ fprintf( pErr, "Empty network.\n" );
+ return 1;
+ }
if ( !Abc_NtkIsStrash(pNtk) )
{
@@ -16488,6 +16511,7 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv )
// perform verification
Abc_NtkDarProve( pNtk, pSecPar );
+ pAbc->pCex = pNtk->pSeqModel; // temporary ???
// Fra_SmlWriteCounterExample( stdout, Aig_Man_t * pAig, Fra_Cex_t * p )
@@ -17664,6 +17688,7 @@ int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
}
Abc_NtkDarBmc( pNtk, nFrames, nSizeMax, nNodeDelta, nBTLimit, nBTLimitAll, fRewrite, fNewAlgo, fVerbose );
+ pAbc->pCex = pNtk->pSeqModel; // temporary ???
return 0;
usage:
@@ -17813,6 +17838,7 @@ int Abc_CommandBmc2( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
}
Abc_NtkDarBmc( pNtk, nFrames, nSizeMax, nNodeDelta, nBTLimit, nBTLimitAll, fRewrite, fNewAlgo, fVerbose );
+ pAbc->pCex = pNtk->pSeqModel; // temporary ???
return 0;
usage:
@@ -22456,6 +22482,69 @@ usage:
SeeAlso []
***********************************************************************/
+int Abc_CommandAbc9Resim( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ Cec_ParSim_t Pars, * pPars = &Pars;
+ int c;
+ Cec_ManSimSetDefaultParams( pPars );
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Fmvh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'F':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( stdout, "Command line switch \"-F\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nRounds = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nRounds < 0 )
+ goto usage;
+ break;
+ case 'm':
+ pPars->fCheckMiter ^= 1;
+ break;
+ case 'v':
+ pPars->fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( pAbc->pAig == NULL )
+ {
+ printf( "Abc_CommandAbc9Resim(): There is no AIG.\n" );
+ return 1;
+ }
+ Cec_ManSeqResimulateCounter( pAbc->pAig, pPars, pAbc->pCex );
+ return 0;
+
+usage:
+ fprintf( stdout, "usage: &resim [-F <num>] [-mvh]\n" );
+ fprintf( stdout, "\t resimulates equivalence classes using counter-example\n" );
+ fprintf( stdout, "\t-F num : the number of additinal frames to simulate [default = %d]\n", pPars->nRounds );
+ fprintf( stdout, "\t-m : toggle miter vs. any circuit [default = %s]\n", pPars->fCheckMiter? "miter": "not miter" );
+ fprintf( stdout, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
+ fprintf( stdout, "\t-h : print the command usage\n");
+ return 1;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Abc_CommandAbc9Equiv( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Cec_ParSim_t Pars, * pPars = &Pars;
@@ -22509,7 +22598,7 @@ int Abc_CommandAbc9Equiv( Abc_Frame_t * pAbc, int argc, char ** argv )
pPars->fFirstStop ^= 1;
break;
case 'd':
- pPars->fDoubleOuts ^= 1;
+ pPars->fDualOut ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
@@ -22537,7 +22626,7 @@ usage:
fprintf( stdout, "\t-s : toggle seq vs. comb simulation [default = %s]\n", pPars->fSeqSimulate? "yes": "no" );
fprintf( stdout, "\t-m : toggle miter vs. any circuit [default = %s]\n", pPars->fCheckMiter? "yes": "no" );
fprintf( stdout, "\t-f : toggle quitting when one PO is asserted [default = %s]\n", pPars->fFirstStop? "yes": "no" );
- fprintf( stdout, "\t-d : toggle using two POs intead of XOR [default = %s]\n", pPars->fDoubleOuts? "yes": "no" );
+ fprintf( stdout, "\t-d : toggle using two POs intead of XOR [default = %s]\n", pPars->fDualOut? "yes": "no" );
fprintf( stdout, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
fprintf( stdout, "\t-h : print the command usage\n");
return 1;
@@ -22554,6 +22643,125 @@ usage:
SeeAlso []
***********************************************************************/
+int Abc_CommandAbc9Semi( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ Cec_ParSmf_t Pars, * pPars = &Pars;
+ int c;
+ Cec_ManSmfSetDefaultParams( pPars );
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "WRFCTmfdvh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'W':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( stdout, "Command line switch \"-W\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nWords = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nWords < 0 )
+ goto usage;
+ break;
+ case 'R':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( stdout, "Command line switch \"-R\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nRounds = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nRounds < 0 )
+ goto usage;
+ break;
+ case 'F':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( stdout, "Command line switch \"-F\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nFrames = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nFrames < 0 )
+ goto usage;
+ break;
+ case 'C':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( stdout, "Command line switch \"-C\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nBTLimit = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nBTLimit < 0 )
+ goto usage;
+ break;
+ case 'T':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( stdout, "Command line switch \"-T\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->TimeLimit = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->TimeLimit < 0 )
+ goto usage;
+ break;
+ case 'm':
+ pPars->fCheckMiter ^= 1;
+ break;
+ case 'f':
+ pPars->fFirstStop ^= 1;
+ break;
+ case 'd':
+ pPars->fDualOut ^= 1;
+ break;
+ case 'v':
+ pPars->fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( pAbc->pAig == NULL )
+ {
+ printf( "Abc_CommandAbc9Resim(): There is no AIG.\n" );
+ return 1;
+ }
+ Cec_ManSeqSemiformal( pAbc->pAig, pPars );
+ return 0;
+
+usage:
+ fprintf( stdout, "usage: &semi [-WRFCT <num>] [-mfdvh]\n" );
+ fprintf( stdout, "\t performs semiformal refinement of equivalence classes\n" );
+ fprintf( stdout, "\t-W num : the number of words to simulate [default = %d]\n", pPars->nWords );
+ fprintf( stdout, "\t-R num : the number of rounds to simulate [default = %d]\n", pPars->nRounds );
+ fprintf( stdout, "\t-F num : the number of frames to simulate [default = %d]\n", pPars->nFrames );
+ fprintf( stdout, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
+ fprintf( stdout, "\t-T num : approximate runtime limit in seconds [default = %d]\n", pPars->TimeLimit );
+ fprintf( stdout, "\t-m : toggle miter vs. any circuit [default = %s]\n", pPars->fCheckMiter? "yes": "no" );
+ fprintf( stdout, "\t-f : toggle quitting when one PO is asserted [default = %s]\n", pPars->fFirstStop? "yes": "no" );
+ fprintf( stdout, "\t-d : toggle using two POs intead of XOR [default = %s]\n", pPars->fDualOut? "yes": "no" );
+ fprintf( stdout, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
+ fprintf( stdout, "\t-h : print the command usage\n");
+ return 1;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Abc_CommandAbc9Times( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Gia_Man_t * pTemp;
@@ -22685,20 +22893,20 @@ int Abc_CommandAbc9Miter( Abc_Frame_t * pAbc, int argc, char ** argv )
char ** pArgvNew;
int nArgcNew;
int c;
- int fXorOuts = 1;
- int fComb = 1;
+ int fDualOut = 0;
+ int fSeq = 0;
int fTrans = 0;
int fVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "xctvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "dstvh" ) ) != EOF )
{
switch ( c )
{
- case 'x':
- fXorOuts ^= 1;
+ case 'd':
+ fDualOut ^= 1;
break;
- case 'c':
- fComb ^= 1;
+ case 's':
+ fSeq ^= 1;
break;
case 't':
fTrans ^= 1;
@@ -22755,7 +22963,7 @@ int Abc_CommandAbc9Miter( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
}
// compute the miter
- pAbc->pAig = Gia_ManMiter( pAux = pAbc->pAig, pSecond, fXorOuts, fComb, fVerbose );
+ pAbc->pAig = Gia_ManMiter( pAux = pAbc->pAig, pSecond, fDualOut, fSeq, fVerbose );
Gia_ManStop( pSecond );
if ( pAbc->pAig == NULL )
{
@@ -22767,10 +22975,10 @@ int Abc_CommandAbc9Miter( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- fprintf( stdout, "usage: &miter [-xctvh] <file>\n" );
+ fprintf( stdout, "usage: &miter [-dstvh] <file>\n" );
fprintf( stdout, "\t creates miter of two designs (current AIG vs. <file>)\n" );
- fprintf( stdout, "\t-x : toggle creating XOR of output pairs [default = %s]\n", fXorOuts? "yes": "no" );
- fprintf( stdout, "\t-c : toggle creating combinational miter [default = %s]\n", fComb? "yes": "no" );
+ fprintf( stdout, "\t-d : toggle creating dual output miter [default = %s]\n", fDualOut? "yes": "no" );
+ fprintf( stdout, "\t-s : toggle creating sequential miter [default = %s]\n", fSeq? "yes": "no" );
fprintf( stdout, "\t-t : toggle XORing pair-wise POs of the miter [default = %s]\n", fTrans? "yes": "no" );
fprintf( stdout, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
fprintf( stdout, "\t-h : print the command usage\n");
@@ -23021,7 +23229,7 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
pPars->fFirstStop ^= 1;
break;
case 'd':
- pPars->fDoubleOuts ^= 1;
+ pPars->fDualOut ^= 1;
break;
case 'w':
pPars->fVeryVerbose ^= 1;
@@ -23058,7 +23266,7 @@ usage:
fprintf( stdout, "\t-r : toggle the use of AIG rewriting [default = %s]\n", pPars->fRewriting? "yes": "no" );
fprintf( stdout, "\t-m : toggle miter vs. any circuit [default = %s]\n", pPars->fCheckMiter? "yes": "no" );
fprintf( stdout, "\t-f : toggle quitting when one PO is asserted [default = %s]\n", pPars->fFirstStop? "yes": "no" );
- fprintf( stdout, "\t-d : toggle using double output miters [default = %s]\n", pPars->fDoubleOuts? "yes": "no" );
+ fprintf( stdout, "\t-d : toggle using double output miters [default = %s]\n", pPars->fDualOut? "yes": "no" );
fprintf( stdout, "\t-w : toggle printing even more verbose information [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
fprintf( stdout, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
fprintf( stdout, "\t-h : print the command usage\n");
@@ -23078,13 +23286,18 @@ usage:
***********************************************************************/
int Abc_CommandAbc9Srm( Abc_Frame_t * pAbc, int argc, char ** argv )
{
+ char * pFileName = "gia_srm.aig";
Gia_Man_t * pTemp;
int c, fVerbose = 0;
+ int fDualOut = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "dvh" ) ) != EOF )
{
switch ( c )
{
+ case 'd':
+ fDualOut ^= 1;
+ break;
case 'v':
fVerbose ^= 1;
break;
@@ -23099,15 +23312,72 @@ int Abc_CommandAbc9Srm( Abc_Frame_t * pAbc, int argc, char ** argv )
printf( "Abc_CommandAbc9Srm(): There is no AIG.\n" );
return 1;
}
- pAbc->pAig = Gia_ManSpecReduce( pTemp = pAbc->pAig );
+// pAbc->pAig = Gia_ManSpecReduce( pTemp = pAbc->pAig, fDualOut );
+// Gia_ManStop( pTemp );
+ pTemp = Gia_ManSpecReduce( pAbc->pAig, fDualOut );
+ Gia_WriteAiger( pTemp, "gia_srm.aig", 0, 0 );
+ printf( "Speculatively reduced model was written into file \"%s\".\n", pFileName );
+ Gia_ManPrintStatsShort( pTemp );
Gia_ManStop( pTemp );
return 0;
usage:
- fprintf( stdout, "usage: &srm [-vh]\n" );
- fprintf( stdout, "\t testing various procedures\n" );
- fprintf( stdout, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
- fprintf( stdout, "\t-h : print the command usage\n");
+ fprintf( stdout, "usage: &srm [-dvh]\n" );
+ fprintf( stdout, "\t writes speculatively reduced model into file \"%s\"\n", pFileName );
+ fprintf( stdout, "\t-d : toggle creating dual output miter [default = %s]\n", fDualOut? "yes": "no" );
+ fprintf( stdout, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+ fprintf( stdout, "\t-h : print the command usage\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_CommandAbc9Reduce( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ Gia_Man_t * pTemp;
+ int c, fVerbose = 0;
+ int fUseAll = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "avh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'a':
+ fUseAll ^= 1;
+ break;
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( pAbc->pAig == NULL )
+ {
+ printf( "Abc_CommandAbc9Reduce(): There is no AIG.\n" );
+ return 1;
+ }
+ pAbc->pAig = Gia_ManEquivReduce( pTemp = pAbc->pAig, fUseAll );
+ Gia_ManStop( pTemp );
+ return 0;
+
+usage:
+ fprintf( stdout, "usage: &reduce [-avh]\n" );
+ fprintf( stdout, "\t reduces the circuit using equivalence classes\n" );
+ fprintf( stdout, "\t-a : toggle creating dual output miter [default = %s]\n", fUseAll? "yes": "no" );
+ fprintf( stdout, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+ fprintf( stdout, "\t-h : print the command usage\n");
return 1;
}
@@ -23207,7 +23477,7 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
}
// compute the miter
- pMiter = Gia_ManMiter( pAbc->pAig, pSecond, 0, 1, pPars->fVerbose );
+ pMiter = Gia_ManMiter( pAbc->pAig, pSecond, 1, 0, pPars->fVerbose );
if ( pMiter )
{
Cec_ManVerify( pMiter, pPars );
diff --git a/src/base/main/mainInt.h b/src/base/main/mainInt.h
index e234d674..ca8717be 100644
--- a/src/base/main/mainInt.h
+++ b/src/base/main/mainInt.h
@@ -80,6 +80,7 @@ struct Abc_Frame_t_
void * pAbc8Aig; // the current AIG
void * pAbc8Lib; // the current LUT library
void * pAig;
+ void * pCex;
// the addition to keep the best Ntl that can be used to restore
void * pAbc8NtlBestDelay; // the best delay, Ntl
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-07 21:59:18 +0000