luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Version abc90311

This commit is contained in:
Alan Mishchenko 2009-03-11 08:01:00 -07:00
parent 32314347ba
commit 243cb29e56
30 changed files with 1183 additions and 3582 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
abclib.dsp
View File

@ -3571,6 +3571,10 @@ SOURCE=.\src\aig\cec\cecPat.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\cec\cecSeq.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\cec\cecSim.c
# End Source File
# Begin Source File

23
src/aig/cec/cec.h
View File

@ -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
}

4
src/aig/cec/cecCec.c
View File

@ -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 );

124
src/aig/cec/cecClass.c
View File

@ -153,6 +153,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.]
@ -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;
@ -420,6 +488,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.]
@ -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;

53
src/aig/cec/cecCore.c
View File

@ -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:

7
src/aig/cec/cecInt.h
View File

@ -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 );

2
src/aig/cec/cecMan.c
View File

@ -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 );

314
src/aig/cec/cecSeq.c Normal file
View File

@ -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 ///
////////////////////////////////////////////////////////////////////////

79
src/aig/cec/cecSolve.c
View File

@ -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 ///
////////////////////////////////////////////////////////////////////////

2
src/aig/cec/cecSweep.c
View File

@ -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 );

1
src/aig/cec/module.make
View File

@ -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

104
src/aig/cec2/cec.h
View File

@ -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 ///
////////////////////////////////////////////////////////////////////////

168
src/aig/cec2/cecAig.c
View File

@ -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 ///
////////////////////////////////////////////////////////////////////////

571
src/aig/cec2/cecClass.c
View File

@ -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 ///
////////////////////////////////////////////////////////////////////////

328
src/aig/cec2/cecCnf.c
View File

@ -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 ///
////////////////////////////////////////////////////////////////////////

245
src/aig/cec2/cecCore.c
View File

@ -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 ///
////////////////////////////////////////////////////////////////////////

208
src/aig/cec2/cecInt.h
View File

@ -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 ///
////////////////////////////////////////////////////////////////////////

59
src/aig/cec2/cecMan.c
View File

@ -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 ///
////////////////////////////////////////////////////////////////////////

250
src/aig/cec2/cecSat.c
View File

@ -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 ///
////////////////////////////////////////////////////////////////////////

284
src/aig/cec2/cecSat2.c
View File

@ -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 ///
////////////////////////////////////////////////////////////////////////

447
src/aig/cec2/cecSim.c
View File

@ -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 ///
////////////////////////////////////////////////////////////////////////

187
src/aig/cec2/cecStatus.c
View File

@ -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 ///
////////////////////////////////////////////////////////////////////////

582
src/aig/cec2/cecSweep.c
View File

@ -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 ///
////////////////////////////////////////////////////////////////////////

9
src/aig/cec2/module.make
View File

@ -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

13
src/aig/gia/gia.h
View File

@ -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
}

92
src/aig/gia/giaDup.c
View File

@ -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,16 +819,16 @@ 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 )
{
iLit = Gia_ManHashXor( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin0Copy(Gia_ManPo(p1,i)) );
Gia_ManAppendCo( pNew, iLit );
}
else
if ( fDualOut )
{
Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(Gia_ManPo(p1,i)) );
}
else
{
iLit = Gia_ManHashXor( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin0Copy(Gia_ManPo(p1,i)) );
Gia_ManAppendCo( pNew, iLit );
}
}
// create register inputs
Gia_ManForEachRi( p0, pObj, i )
@ -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 );

225
src/aig/gia/giaEquiv.c
View File

@ -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,23 +482,39 @@ 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;
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 != 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) );
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)) )
Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, pObj->Value, iLitNew) );
pObj->Value = iLitNew;
Gia_ManSpecBuild( pNew, p, pObj, vXorLits );
}
/**Function*************************************************************
@ -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,9 +561,135 @@ Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p )
}
Gia_ManForEachRi( p, pObj, i )
Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
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 );
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
pNew = Gia_ManCleanup( pTemp = pNew );
Gia_ManStop( pTemp );
return pNew;

57
src/aig/gia/giaUtil.c
View File

@ -578,6 +578,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.]
@ -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 ///
////////////////////////////////////////////////////////////////////////

322
src/base/abci/abc.c
View File

@ -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:
@ -22445,6 +22471,69 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
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 []
@ -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,12 +22626,131 @@ 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;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
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 []
@ -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 );

1
src/base/main/mainInt.h
View File

@ -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