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

Version abc90804 

committer: Baruch Sterin <baruchs@gmail.com>
This commit is contained in:
Alan Mishchenko 2015-06-22 23:04:59 -07:00
parent 270f6db246
commit da65e88e3b
38 changed files with 1187 additions and 470 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
Makefile
View File

@ -26,7 +26,7 @@ MODULES := \
src/aig/bdc src/aig/bar src/aig/ntl src/aig/nwk \
src/aig/mfx src/aig/tim src/aig/saig src/aig/bbr \
src/aig/int src/aig/dch src/aig/ssw src/aig/cgt \
src/aig/cec src/aig/gia src/aig/bbl
src/aig/cec src/aig/gia src/aig/bbl src/aig/live
default: $(PROG)

16
abclib.dsp
View File

@ -1671,6 +1671,10 @@ SOURCE=.\src\opt\mfs\mfsDiv.c
# End Source File
# Begin Source File
SOURCE=.\src\opt\mfs\mfsGia.c
# End Source File
# Begin Source File
SOURCE=.\src\opt\mfs\mfsInt.h
# End Source File
# Begin Source File
@ -3834,6 +3838,18 @@ SOURCE=.\src\aig\bbl\bblif.c
SOURCE=.\src\aig\bbl\bblif.h
# End Source File
# End Group
# Begin Group "live"
# PROP Default_Filter ""
# Begin Source File
SOURCE=.\src\aig\live\liveness.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\live\liveness_sim.c
# End Source File
# End Group
# End Group
# End Group
# Begin Group "Header Files"

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

@ -47,21 +47,23 @@ struct Cec_ParSat_t_
int fNonChrono; // use non-chronological backtracling (for circuit SAT only)
int fPolarFlip; // flops polarity of variables
int fCheckMiter; // the circuit is the miter
int fFirstStop; // stop on the first sat output
// int fFirstStop; // stop on the first sat output
int fLearnCls; // perform clause learning
int fVerbose; // verbose stats
};
// simulation parameters
typedef struct Cec_ParSim_t_ Cec_ParSim_t;
struct Cec_ParSim_t_
struct Cec_ParSim_t_
{
int nWords; // the number of simulation words
int nFrames; // the number of simulation frames
int nRounds; // the number of simulation rounds
int nNonRefines; // the max number of rounds without refinement
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 fFirstStop; // stop on the first sat output
int fSeqSimulate; // performs sequential simulation
int fLatchCorr; // consider only latch outputs
int fVeryVerbose; // verbose stats
@ -74,12 +76,14 @@ 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 nFrames; // the max number of time frames
int nNonRefines; // the max number of rounds without refinement
int nMinOutputs; // the min outputs to accumulate
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 fFirstStop; // stop on the first sat output
int fVerbose; // verbose stats
};
@ -96,7 +100,7 @@ struct Cec_ParFra_t_
int nDepthMax; // the depth in terms of steps of speculative reduction
int fRewriting; // enables AIG rewriting
int fCheckMiter; // the circuit is the miter
int fFirstStop; // stop on the first sat output
// int fFirstStop; // stop on the first sat output
int fDualOut; // miter with separate outputs
int fColorDiff; // miter with separate outputs
int fVeryVerbose; // verbose stats
@ -109,7 +113,7 @@ struct Cec_ParCec_t_
{
int nBTLimit; // conflict limit at a node
int TimeLimit; // the runtime limit in seconds
int fFirstStop; // stop on the first sat output
// int fFirstStop; // stop on the first sat output
int fUseSmartCnf; // use smart CNF computation
int fRewriting; // enables AIG rewriting
int fVeryVerbose; // verbose stats
@ -129,7 +133,7 @@ struct Cec_ParCor_t_
int fUseRings; // use rings
int fMakeChoices; // use equilvaences as choices
int fUseCSat; // use circuit-based solver
int fFirstStop; // stop on the first sat output
// int fFirstStop; // stop on the first sat output
int fUseSmartCnf; // use smart CNF computation
int fVeryVerbose; // verbose stats
int fVerbose; // verbose stats

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

@ -135,7 +135,6 @@ int Cec_ManVerify( Gia_Man_t * p, Cec_ParCec_t * pPars )
pParsFra->TimeLimit = pPars->TimeLimit;
pParsFra->fVerbose = pPars->fVerbose;
pParsFra->fCheckMiter = 1;
pParsFra->fFirstStop = 1;
pParsFra->fDualOut = 1;
pNew = Cec_ManSatSweeping( p, pParsFra );
if ( pNew == NULL )

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

@ -213,7 +213,7 @@ int Cec_ManChoiceComputation_int( Gia_Man_t * pAig, Cec_ParChc_t * pPars )
// prepare simulation manager
Cec_ManSimSetDefaultParams( pParsSim );
pParsSim->nWords = pPars->nWords;
pParsSim->nRounds = pPars->nRounds;
pParsSim->nFrames = pPars->nRounds;
pParsSim->fVerbose = pPars->fVerbose;
pParsSim->fLatchCorr = 0;
pParsSim->fSeqSimulate = 0;

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

@ -545,7 +545,7 @@ void Cec_ManSimSavePattern( Cec_ManSim_t * p, int iPat )
void Cec_ManSimFindBestPattern( Cec_ManSim_t * p )
{
unsigned * pInfo;
int i, ScoreBest = 0, iPatBest = 1;
int i, ScoreBest = 0, iPatBest = 1; // set the first pattern
// find the best pattern
for ( i = 0; i < 32 * p->nWords; i++ )
if ( ScoreBest < p->pScores[i] )
@ -588,8 +588,8 @@ int Cec_ManSimAnalyzeOutputs( Cec_ManSim_t * p )
// compare outputs with 0
if ( p->pPars->fDualOut )
{
assert( (Gia_ManCoNum(p->pAig) & 1) == 0 );
for ( i = 0; i < Gia_ManCoNum(p->pAig); i++ )
assert( (Gia_ManPoNum(p->pAig) & 1) == 0 );
for ( i = 0; i < Gia_ManPoNum(p->pAig); i++ )
{
pInfo = Vec_PtrEntry( p->vCoSimInfo, i );
pInfo2 = Vec_PtrEntry( p->vCoSimInfo, ++i );
@ -601,7 +601,7 @@ int Cec_ManSimAnalyzeOutputs( Cec_ManSim_t * p )
Cec_ManSimSavePattern( p, Cec_ManSimCompareEqualFirstBit(pInfo, pInfo2, p->nWords) );
}
if ( p->pCexes == NULL )
p->pCexes = ABC_CALLOC( void *, Gia_ManCoNum(p->pAig)/2 );
p->pCexes = ABC_CALLOC( void *, Gia_ManPoNum(p->pAig)/2 );
if ( p->pCexes[i/2] == NULL )
{
p->nOuts++;
@ -612,7 +612,7 @@ int Cec_ManSimAnalyzeOutputs( Cec_ManSim_t * p )
}
else
{
for ( i = 0; i < Gia_ManCoNum(p->pAig); i++ )
for ( i = 0; i < Gia_ManPoNum(p->pAig); i++ )
{
pInfo = Vec_PtrEntry( p->vCoSimInfo, i );
if ( !Cec_ManSimCompareConst( pInfo, p->nWords ) )
@ -623,7 +623,7 @@ int Cec_ManSimAnalyzeOutputs( Cec_ManSim_t * p )
Cec_ManSimSavePattern( p, Cec_ManSimCompareConstFirstBit(pInfo, p->nWords) );
}
if ( p->pCexes == NULL )
p->pCexes = ABC_CALLOC( void *, Gia_ManCoNum(p->pAig) );
p->pCexes = ABC_CALLOC( void *, Gia_ManPoNum(p->pAig) );
if ( p->pCexes[i] == NULL )
{
p->nOuts++;
@ -632,7 +632,7 @@ int Cec_ManSimAnalyzeOutputs( Cec_ManSim_t * p )
}
}
}
return p->pCexes != NULL && p->pPars->fFirstStop;
return p->pCexes != NULL;
}
/**Function*************************************************************

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

@ -48,7 +48,7 @@ void Cec_ManSatSetDefaultParams( Cec_ParSat_t * p )
p->fNonChrono = 0; // use non-chronological backtracling (for circuit SAT only)
p->fPolarFlip = 1; // flops polarity of variables
p->fCheckMiter = 0; // the circuit is the miter
p->fFirstStop = 0; // stop on the first sat output
// p->fFirstStop = 0; // stop on the first sat output
p->fLearnCls = 0; // perform clause learning
p->fVerbose = 0; // verbose stats
}
@ -67,11 +67,13 @@ void Cec_ManSatSetDefaultParams( Cec_ParSat_t * p )
void Cec_ManSimSetDefaultParams( Cec_ParSim_t * p )
{
memset( p, 0, sizeof(Cec_ParSim_t) );
p->nWords = 15; // the number of simulation words
p->nRounds = 15; // the number of simulation rounds
p->nWords = 31; // the number of simulation words
p->nFrames = 100; // the number of simulation frames
p->nRounds = 20; // the max number of simulation rounds
p->nNonRefines = 3; // the max number of rounds without refinement
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->fFirstStop = 0; // stop on the first sat output
p->fDualOut = 0; // miter with separate outputs
p->fSeqSimulate = 0; // performs sequential simulation
p->fVeryVerbose = 0; // verbose stats
@ -93,13 +95,15 @@ void Cec_ManSmfSetDefaultParams( Cec_ParSmf_t * p )
{
memset( p, 0, sizeof(Cec_ParSmf_t) );
p->nWords = 31; // the number of simulation words
p->nRounds = 1; // the number of simulation rounds
p->nFrames = 2; // the number of time frames
p->nRounds = 200; // the number of simulation rounds
p->nFrames = 200; // the max number of time frames
p->nNonRefines = 3; // the max number of rounds without refinement
p->nMinOutputs = 0; // the min outputs to accumulate
p->nBTLimit = 100; // 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->fFirstStop = 0; // stop on the first sat output
p->fVerbose = 0; // verbose stats
}
@ -126,7 +130,7 @@ void Cec_ManFraSetDefaultParams( Cec_ParFra_t * p )
p->nDepthMax = 1; // the depth in terms of steps of speculative reduction
p->fRewriting = 0; // enables AIG rewriting
p->fCheckMiter = 0; // the circuit is the miter
p->fFirstStop = 0; // stop on the first sat output
// p->fFirstStop = 0; // stop on the first sat output
p->fDualOut = 0; // miter with separate outputs
p->fColorDiff = 0; // miter with separate outputs
p->fVeryVerbose = 0; // verbose stats
@ -149,7 +153,7 @@ void Cec_ManCecSetDefaultParams( Cec_ParCec_t * p )
memset( p, 0, sizeof(Cec_ParCec_t) );
p->nBTLimit = 1000; // conflict limit at a node
p->TimeLimit = 0; // the runtime limit in seconds
p->fFirstStop = 0; // stop on the first sat output
// p->fFirstStop = 0; // stop on the first sat output
p->fUseSmartCnf = 0; // use smart CNF computation
p->fRewriting = 0; // enables AIG rewriting
p->fVeryVerbose = 0; // verbose stats
@ -177,7 +181,7 @@ void Cec_ManCorSetDefaultParams( Cec_ParCor_t * p )
p->fLatchCorr = 0; // consider only latch outputs
p->fUseRings = 1; // combine classes into rings
p->fUseCSat = 1; // use circuit-based solver
p->fFirstStop = 0; // stop on the first sat output
// p->fFirstStop = 0; // stop on the first sat output
p->fUseSmartCnf = 0; // use smart CNF computation
p->fVeryVerbose = 0; // verbose stats
p->fVerbose = 0; // verbose stats
@ -229,6 +233,32 @@ Gia_Man_t * Cec_ManSatSolving( Gia_Man_t * pAig, Cec_ParSat_t * pPars )
return pNew;
}
/**Function*************************************************************
Synopsis [Core procedure for simulation.]
Description [Returns 1 if refinement has happened.]
SideEffects []
SeeAlso []
***********************************************************************/
int Cec_ManSimulationOne( Gia_Man_t * pAig, Cec_ParSim_t * pPars )
{
Cec_ManSim_t * pSim;
int RetValue = 0, clkTotal = clock();
pSim = Cec_ManSimStart( pAig, pPars );
if ( (pAig->pReprs == NULL && (RetValue = Cec_ManSimClassesPrepare( pSim ))) ||
(RetValue == 0 && (RetValue = Cec_ManSimClassesRefine( pSim ))) )
printf( "The number of failed outputs of the miter = %6d. (Words = %4d. Frames = %4d.)\n",
pSim->nOuts, pPars->nWords, pPars->nFrames );
if ( pPars->fVerbose )
ABC_PRT( "Time", clock() - clkTotal );
Cec_ManSimStop( pSim );
return RetValue;
}
/**Function*************************************************************
Synopsis [Core procedure for simulation.]
@ -242,22 +272,44 @@ Gia_Man_t * Cec_ManSatSolving( Gia_Man_t * pAig, Cec_ParSat_t * pPars )
***********************************************************************/
void Cec_ManSimulation( Gia_Man_t * pAig, Cec_ParSim_t * pPars )
{
Cec_ManSim_t * pSim;
int RetValue, clkTotal = clock();
if ( pPars->fSeqSimulate )
printf( "Performing sequential simulation of %d frames with %d words.\n",
pPars->nRounds, pPars->nWords );
int r, nLitsOld, nLitsNew, nCountNoRef = 0, fStop = 0;
Gia_ManRandom( 1 );
pSim = Cec_ManSimStart( pAig, pPars );
if ( pAig->pReprs == NULL )
RetValue = Cec_ManSimClassesPrepare( pSim );
Cec_ManSimClassesRefine( pSim );
if ( pPars->fSeqSimulate )
printf( "Performing rounds of random simulation of %d frames with %d words.\n",
pPars->nRounds, pPars->nFrames, pPars->nWords );
nLitsOld = Gia_ManEquivCountLits( pAig );
for ( r = 0; r < pPars->nRounds; r++ )
{
if ( Cec_ManSimulationOne( pAig, pPars ) )
{
fStop = 1;
break;
}
// decide when to stop
nLitsNew = Gia_ManEquivCountLits( pAig );
if ( nLitsOld == 0 || nLitsOld > nLitsNew )
{
nLitsOld = nLitsNew;
nCountNoRef = 0;
}
else if ( ++nCountNoRef == pPars->nNonRefines )
{
r++;
break;
}
assert( nLitsOld == nLitsNew );
}
// if ( pPars->fVerbose )
if ( r == pPars->nRounds || fStop )
printf( "Random simulation is stopped after %d rounds.\n", r );
else
printf( "Random simulation saturated after %d rounds.\n", r );
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 );
if ( pPars->fVerbose )
ABC_PRT( "Time", clock() - clkTotal );
Cec_ManSimStop( pSim );
{
int nNonConsts = Cec_ManCountNonConstOutputs( pAig );
if ( nNonConsts )
printf( "The number of POs that are not const-0 candidates = %d.\n", nNonConsts );
}
}
/**Function*************************************************************
@ -297,9 +349,8 @@ Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars )
// simulation
Cec_ManSimSetDefaultParams( pParsSim );
pParsSim->nWords = pPars->nWords;
pParsSim->nRounds = pPars->nRounds;
pParsSim->nFrames = pPars->nRounds;
pParsSim->fCheckMiter = pPars->fCheckMiter;
pParsSim->fFirstStop = pPars->fFirstStop;
pParsSim->fDualOut = pPars->fDualOut;
pParsSim->fVerbose = pPars->fVerbose;
pSim = Cec_ManSimStart( p->pAig, pParsSim );

8
src/aig/cec/cecCorr.c
View File

@ -545,7 +545,7 @@ int Cec_ManResimulateCounterExamples( Cec_ManSim_t * pSim, Vec_Int_t * vCexStore
vPairs = Gia_ManCorrCreateRemapping( pSim->pAig );
Gia_ManSetRefs( pSim->pAig );
// pSim->pPars->nWords = 63;
pSim->pPars->nRounds = nFrames;
pSim->pPars->nFrames = nFrames;
vSimInfo = Vec_PtrAllocSimInfo( Gia_ManRegNum(pSim->pAig) + Gia_ManPiNum(pSim->pAig) * nFrames, pSim->pPars->nWords );
while ( iStart < Vec_IntSize(vCexStore) )
{
@ -580,7 +580,7 @@ int Cec_ManResimulateCounterExamplesComb( Cec_ManSim_t * pSim, Vec_Int_t * vCexS
Vec_Ptr_t * vSimInfo;
int RetValue = 0, iStart = 0;
Gia_ManSetRefs( pSim->pAig );
pSim->pPars->nRounds = 1;
pSim->pPars->nFrames = 1;
vSimInfo = Vec_PtrAllocSimInfo( Gia_ManCiNum(pSim->pAig), pSim->pPars->nWords );
while ( iStart < Vec_IntSize(vCexStore) )
{
@ -774,7 +774,7 @@ void Cec_ManLSCorrespondenceBmc( Gia_Man_t * pAig, Cec_ParCor_t * pPars, int nPr
// prepare simulation manager
Cec_ManSimSetDefaultParams( pParsSim );
pParsSim->nWords = pPars->nWords;
pParsSim->nRounds = pPars->nRounds;
pParsSim->nFrames = pPars->nRounds;
pParsSim->fVerbose = pPars->fVerbose;
pParsSim->fLatchCorr = pPars->fLatchCorr;
pParsSim->fSeqSimulate = 1;
@ -853,7 +853,7 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
// prepare simulation manager
Cec_ManSimSetDefaultParams( pParsSim );
pParsSim->nWords = pPars->nWords;
pParsSim->nRounds = pPars->nRounds;
pParsSim->nFrames = pPars->nFrames;
pParsSim->fVerbose = pPars->fVerbose;
pParsSim->fLatchCorr = pPars->fLatchCorr;
pParsSim->fSeqSimulate = 1;

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

@ -192,8 +192,10 @@ extern Vec_Ptr_t * Cec_ManPatCollectPatterns( Cec_ManPat_t * pMan, int
extern Vec_Ptr_t * Cec_ManPatPackPatterns( Vec_Int_t * vCexStore, int nInputs, int nRegs, int nWordsInit );
/*=== cecSeq.c ============================================================*/
extern int Cec_ManSeqResimulate( Cec_ManSim_t * p, Vec_Ptr_t * vInfo );
extern int Cec_ManSeqResimulateInfo( Gia_Man_t * pAig, Vec_Ptr_t * vSimInfo, Gia_Cex_t * pBestState );
extern int Cec_ManSeqResimulateInfo( Gia_Man_t * pAig, Vec_Ptr_t * vSimInfo, Gia_Cex_t * pBestState, int fCheckMiter );
extern void Cec_ManSeqDeriveInfoInitRandom( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Gia_Cex_t * pCex );
extern int Cec_ManCountNonConstOutputs( Gia_Man_t * pAig );
extern int Cec_ManCheckNonTrivialCands( Gia_Man_t * pAig );
/*=== 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 );

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

@ -76,13 +76,13 @@ void Cec_ManSatPrintStats( Cec_ManSat_t * p )
printf( "MinVar = %5d ", p->pPars->nSatVarMax );
printf( "MinCalls = %5d\n", p->pPars->nCallsRecycle );
printf( "Unsat calls %6d (%6.2f %%) Ave conf = %8.1f ",
p->nSatUnsat, 100.0*p->nSatUnsat/p->nSatTotal, p->nSatUnsat? 1.0*p->nConfUnsat/p->nSatUnsat :0.0 );
p->nSatUnsat, p->nSatTotal? 100.0*p->nSatUnsat/p->nSatTotal : 0.0, p->nSatUnsat? 1.0*p->nConfUnsat/p->nSatUnsat :0.0 );
ABC_PRTP( "Time", p->timeSatUnsat, p->timeTotal );
printf( "Sat calls %6d (%6.2f %%) Ave conf = %8.1f ",
p->nSatSat, 100.0*p->nSatSat/p->nSatTotal, p->nSatSat? 1.0*p->nConfSat/p->nSatSat : 0.0 );
p->nSatSat, p->nSatTotal? 100.0*p->nSatSat/p->nSatTotal : 0.0, p->nSatSat? 1.0*p->nConfSat/p->nSatSat : 0.0 );
ABC_PRTP( "Time", p->timeSatSat, p->timeTotal );
printf( "Undef calls %6d (%6.2f %%) Ave conf = %8.1f ",
p->nSatUndec, 100.0*p->nSatUndec/p->nSatTotal, p->nSatUndec? 1.0*p->nConfUndec/p->nSatUndec : 0.0 );
p->nSatUndec, p->nSatTotal? 100.0*p->nSatUndec/p->nSatTotal : 0.0, p->nSatUndec? 1.0*p->nConfUndec/p->nSatUndec : 0.0 );
ABC_PRTP( "Time", p->timeSatUndec, p->timeTotal );
ABC_PRT( "Total time", p->timeTotal );
}

148
src/aig/cec/cecSeq.c
View File

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

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

@ -718,7 +718,7 @@ clk2 = clock();
pPat->timeTotalSave += clock() - clk3;
}
// quit if one of them is solved
if ( pPars->fFirstStop )
if ( pPars->fCheckMiter )
break;
}
p->timeTotal = clock() - clk;
@ -810,12 +810,12 @@ Vec_Str_t * Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat
{
if ( Gia_ObjFaninC0(pObj) )
{
printf( "Constant 1 output of SRM!!!\n" );
// printf( "Constant 1 output of SRM!!!\n" );
Vec_StrPush( vStatus, 0 );
}
else
{
printf( "Constant 0 output of SRM!!!\n" );
// printf( "Constant 0 output of SRM!!!\n" );
Vec_StrPush( vStatus, 1 );
}
continue;

2
src/aig/dch/dch.h
View File

@ -68,7 +68,7 @@ struct Dch_Pars_t_
/*=== dchCore.c ==========================================================*/
extern void Dch_ManSetDefaultParams( Dch_Pars_t * p );
extern Aig_Man_t * Dch_ComputeChoices( Aig_Man_t * pAig, Dch_Pars_t * pPars );
extern void Dch_ComputeEquivalences( Aig_Man_t * pAig, Dch_Pars_t * pPars );
#ifdef __cplusplus
}

34
src/aig/dch/dchCore.c
View File

@ -90,7 +90,7 @@ p->timeTotal = clock() - clkTotal;
ABC_FREE( pAig->pTable );
pResult = Dch_DeriveChoiceAig( pAig );
// count the number of representatives
if ( pPars->fVerbose )
if ( pPars->fVerbose )
printf( "STATS: Reprs = %6d. Equivs = %6d. Choices = %6d.\n",
Dch_DeriveChoiceCountReprs( pAig ),
Dch_DeriveChoiceCountEquivs( pResult ),
@ -98,6 +98,38 @@ p->timeTotal = clock() - clkTotal;
return pResult;
}
/**Function*************************************************************
Synopsis [Performs computation of AIGs with choices.]
Description [Takes several AIGs and performs choicing.]
SideEffects []
SeeAlso []
***********************************************************************/
void Dch_ComputeEquivalences( Aig_Man_t * pAig, Dch_Pars_t * pPars )
{
Dch_Man_t * p;
int clk, clkTotal = clock();
// reset random numbers
Aig_ManRandom(1);
// start the choicing manager
p = Dch_ManCreate( pAig, pPars );
// compute candidate equivalence classes
clk = clock();
p->ppClasses = Dch_CreateCandEquivClasses( pAig, pPars->nWords, pPars->fVerbose );
p->timeSimInit = clock() - clk;
// Dch_ClassesPrint( p->ppClasses, 0 );
p->nLits = Dch_ClassesLitNum( p->ppClasses );
// perform SAT sweeping
Dch_ManSweep( p );
// free memory ahead of time
p->timeTotal = clock() - clkTotal;
Dch_ManStop( p );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

6
src/aig/fra/fraSec.c
View File

@ -480,6 +480,7 @@ clk = clock();
}
else if ( pParSec->fInterSeparate )
{
Ssw_Cex_t * pCex = NULL;
Aig_Man_t * pTemp, * pAux;
Aig_Obj_t * pObjPo;
int i, Counter = 0;
@ -495,8 +496,7 @@ clk = clock();
RetValue = Inter_ManPerformInterpolation( pTemp, pPars, &Depth );
if ( pTemp->pSeqModel )
{
Ssw_Cex_t * pCex;
pCex = pNew->pSeqModel = pTemp->pSeqModel; pTemp->pSeqModel = NULL;
pCex = p->pSeqModel = Ssw_SmlDupCounterExample( pTemp->pSeqModel, Aig_ManRegNum(p) );
pCex->iPo = i;
Aig_ManStop( pTemp );
break;
@ -520,7 +520,7 @@ clk = clock();
printf( "Solving output %3d (out of %3d) using interpolation.\r", i, Saig_ManPoNum(pNew) );
}
Aig_ManCleanup( pNew );
if ( pNew->pSeqModel == NULL )
if ( pCex == NULL )
{
printf( "Interpolation left %d (out of %d) outputs unsolved \n", Counter, Saig_ManPoNum(pNew) );
if ( Counter )

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

@ -557,6 +557,7 @@ extern Gia_Man_t * Gia_ManRemoveEnables( Gia_Man_t * p );
extern int Gia_ManCheckTopoOrder( Gia_Man_t * p );
extern int * Gia_ManDeriveNexts( Gia_Man_t * p );
extern void Gia_ManDeriveReprs( Gia_Man_t * p );
extern int Gia_ManEquivCountLits( Gia_Man_t * p );
extern int Gia_ManEquivCountClasses( 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 );
@ -565,6 +566,7 @@ extern Gia_Man_t * Gia_ManEquivReduceAndRemap( Gia_Man_t * p, int fSeq,
extern int Gia_ManEquivSetColors( Gia_Man_t * p, int fVerbose );
extern Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fVerbose );
extern Gia_Man_t * Gia_ManSpecReduceInit( Gia_Man_t * p, Gia_Cex_t * pInit, int nFrames, int fDualOut );
extern Gia_Man_t * Gia_ManSpecReduceInitFrames( Gia_Man_t * p, Gia_Cex_t * pInit, int nFramesMax, int * pnFrames, int fDualOut, int nMinOutputs );
extern void Gia_ManEquivTransform( Gia_Man_t * p, int fVerbose );
extern void Gia_ManEquivImprove( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManEquivToChoices( Gia_Man_t * p, int nSnapshots );
@ -663,6 +665,7 @@ extern void Tas_ManStop( Tas_Man_t * p );
extern Vec_Int_t * Tas_ReadModel( Tas_Man_t * p );
extern void Tas_ManSatPrintStats( Tas_Man_t * p );
extern int Tas_ManSolve( Tas_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 );
extern int Tas_ManSolveArray( Tas_Man_t * p, Vec_Ptr_t * vObjs );
#ifdef __cplusplus

2
src/aig/gia/giaAiger.c
View File

@ -841,7 +841,7 @@ void Gia_WriteAiger( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int
// create normalized AIG
if ( !Gia_ManIsNormalized(pInit) )
{
printf( "Gia_WriteAiger(): Normalizing AIG for writing.\n" );
// printf( "Gia_WriteAiger(): Normalizing AIG for writing.\n" );
p = Gia_ManDupNormalized( pInit );
}
else

6
src/aig/gia/giaCSat.c
View File

@ -969,13 +969,13 @@ void Cbs_ManSatPrintStats( Cbs_Man_t * p )
printf( "JustMax = %5d ", p->Pars.nJustLimit );
printf( "\n" );
printf( "Unsat calls %6d (%6.2f %%) Ave conf = %8.1f ",
p->nSatUnsat, 100.0*p->nSatUnsat/p->nSatTotal, p->nSatUnsat? 1.0*p->nConfUnsat/p->nSatUnsat :0.0 );
p->nSatUnsat, p->nSatTotal? 100.0*p->nSatUnsat/p->nSatTotal :0.0, p->nSatUnsat? 1.0*p->nConfUnsat/p->nSatUnsat :0.0 );
ABC_PRTP( "Time", p->timeSatUnsat, p->timeTotal );
printf( "Sat calls %6d (%6.2f %%) Ave conf = %8.1f ",
p->nSatSat, 100.0*p->nSatSat/p->nSatTotal, p->nSatSat? 1.0*p->nConfSat/p->nSatSat : 0.0 );
p->nSatSat, p->nSatTotal? 100.0*p->nSatSat/p->nSatTotal :0.0, p->nSatSat? 1.0*p->nConfSat/p->nSatSat : 0.0 );
ABC_PRTP( "Time", p->timeSatSat, p->timeTotal );
printf( "Undef calls %6d (%6.2f %%) Ave conf = %8.1f ",
p->nSatUndec, 100.0*p->nSatUndec/p->nSatTotal, p->nSatUndec? 1.0*p->nConfUndec/p->nSatUndec : 0.0 );
p->nSatUndec, p->nSatTotal? 100.0*p->nSatUndec/p->nSatTotal :0.0, p->nSatUndec? 1.0*p->nConfUndec/p->nSatUndec : 0.0 );
ABC_PRTP( "Time", p->timeSatUndec, p->timeTotal );
ABC_PRT( "Total time", p->timeTotal );
}

6
src/aig/gia/giaCSatOld.c
View File

@ -680,13 +680,13 @@ void Cbs0_ManSatPrintStats( Cbs0_Man_t * p )
printf( "JustMax = %5d ", p->Pars.nJustLimit );
printf( "\n" );
printf( "Unsat calls %6d (%6.2f %%) Ave conf = %8.1f ",
p->nSatUnsat, 100.0*p->nSatUnsat/p->nSatTotal, p->nSatUnsat? 1.0*p->nConfUnsat/p->nSatUnsat :0.0 );
p->nSatUnsat, p->nSatTotal? 100.0*p->nSatUnsat/p->nSatTotal :0.0, p->nSatUnsat? 1.0*p->nConfUnsat/p->nSatUnsat :0.0 );
ABC_PRTP( "Time", p->timeSatUnsat, p->timeTotal );
printf( "Sat calls %6d (%6.2f %%) Ave conf = %8.1f ",
p->nSatSat, 100.0*p->nSatSat/p->nSatTotal, p->nSatSat? 1.0*p->nConfSat/p->nSatSat : 0.0 );
p->nSatSat, p->nSatTotal? 100.0*p->nSatSat/p->nSatTotal :0.0, p->nSatSat? 1.0*p->nConfSat/p->nSatSat : 0.0 );
ABC_PRTP( "Time", p->timeSatSat, p->timeTotal );
printf( "Undef calls %6d (%6.2f %%) Ave conf = %8.1f ",
p->nSatUndec, 100.0*p->nSatUndec/p->nSatTotal, p->nSatUndec? 1.0*p->nConfUndec/p->nSatUndec : 0.0 );
p->nSatUndec, p->nSatTotal? 100.0*p->nSatUndec/p->nSatTotal :0.0, p->nSatUndec? 1.0*p->nConfUndec/p->nSatUndec : 0.0 );
ABC_PRTP( "Time", p->timeSatUndec, p->timeTotal );
ABC_PRT( "Total time", p->timeTotal );
}

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

@ -245,6 +245,69 @@ int Gia_ManEquivCheckLits( Gia_Man_t * p, int nLits )
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManPrintStatsClasses( Gia_Man_t * p )
{
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) )
Counter0++;
else if ( Gia_ObjIsNone(p, i) )
CounterX++;
if ( Gia_ObjProved(p, i) )
Proved++;
}
CounterX -= Gia_ManCoNum(p);
nLits = Gia_ManCiNum(p) + Gia_ManAndNum(p) - Counter - CounterX;
// printf( "i/o/ff =%5d/%5d/%5d ", Gia_ManPiNum(p), Gia_ManPoNum(p), Gia_ManRegNum(p) );
// printf( "and =%5d ", Gia_ManAndNum(p) );
// printf( "lev =%3d ", Gia_ManLevelNum(p) );
printf( "cst =%3d cls =%6d lit =%8d\n", Counter0, Counter, nLits );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ManEquivCountLits( Gia_Man_t * p )
{
int i, Counter = 0, Counter0 = 0, CounterX = 0;
if ( p->pReprs == NULL || p->pNexts == NULL )
return 0;
for ( i = 1; i < Gia_ManObjNum(p); i++ )
{
if ( Gia_ObjIsHead(p, i) )
Counter++;
else if ( Gia_ObjIsConst(p, i) )
Counter0++;
else if ( Gia_ObjIsNone(p, i) )
CounterX++;
}
CounterX -= Gia_ManCoNum(p);
return Gia_ManCiNum(p) + Gia_ManAndNum(p) - Counter - CounterX;
}
/**Function*************************************************************
Synopsis []
@ -274,6 +337,8 @@ void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem )
nLits = Gia_ManCiNum(p) + Gia_ManAndNum(p) - Counter - CounterX;
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 );
// printf( "cst =%8d cls =%7d lit =%8d\n",
// Counter0, Counter, nLits );
assert( Gia_ManEquivCheckLits( p, nLits ) );
if ( fVerbose )
{
@ -694,6 +759,29 @@ static inline void Gia_ManSpecBuild( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t
pObj->Value = iLitNew;
}
/**Function*************************************************************
Synopsis [Returns 1 if AIG has dangling nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ManHasNoEquivs( Gia_Man_t * p )
{
Gia_Obj_t * pObj;
int i;
if ( p->pReprs == NULL )
return 1;
Gia_ManForEachObj( p, pObj, i )
if ( Gia_ObjReprObj(p, i) != NULL )
break;
return i == Gia_ManObjNum(p);
}
/**Function*************************************************************
Synopsis [Duplicates the AIG in the DFS order.]
@ -743,16 +831,11 @@ Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fVerbose )
printf( "Gia_ManSpecReduce(): Dual-output miter should have even number of POs.\n" );
return NULL;
}
// check if there are any equivalences defined
Gia_ManForEachObj( p, pObj, i )
if ( Gia_ObjReprObj(p, i) != NULL )
break;
if ( i == Gia_ManObjNum(p) )
if ( Gia_ManHasNoEquivs(p) )
{
printf( "Gia_ManSpecReduce(): There are no equivalences to reduce.\n" );
return NULL;
}
/*
if ( !Gia_ManCheckTopoOrder( p ) )
{
@ -792,7 +875,6 @@ Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fVerbose )
return pNew;
}
/**Function*************************************************************
Synopsis [Duplicates the AIG in the DFS order.]
@ -879,6 +961,7 @@ Gia_Man_t * Gia_ManSpecReduceInit( Gia_Man_t * p, Gia_Cex_t * pInit, int nFrames
printf( "Gia_ManSpecReduceInit(): Dual-output miter should have even number of POs.\n" );
return NULL;
}
/*
if ( !Gia_ManCheckTopoOrder( p ) )
{
@ -918,7 +1001,7 @@ Gia_Man_t * Gia_ManSpecReduceInit( Gia_Man_t * p, Gia_Cex_t * pInit, int nFrames
Gia_ManAppendCo( pNew, iLitNew );
if ( Vec_IntSize(vXorLits) == 0 )
{
printf( "Speculatively reduced model has no primary outputs.\n" );
// printf( "Speculatively reduced model has no primary outputs.\n" );
Gia_ManAppendCo( pNew, 0 );
}
ABC_FREE( p->pCopies );
@ -929,6 +1012,41 @@ Gia_Man_t * Gia_ManSpecReduceInit( Gia_Man_t * p, Gia_Cex_t * pInit, int nFrames
return pNew;
}
/**Function*************************************************************
Synopsis [Creates initialized SRM with the given number of frames.]
Description [Uses as many frames as needed to create the number of
output not less than the number of equivalence literals.]
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManSpecReduceInitFrames( Gia_Man_t * p, Gia_Cex_t * pInit, int nFramesMax, int * pnFrames, int fDualOut, int nMinOutputs )
{
Gia_Man_t * pFrames;
int f, nLits;
nLits = Gia_ManEquivCountLits( p );
for ( f = 1; ; f++ )
{
pFrames = Gia_ManSpecReduceInit( p, pInit, f, fDualOut );
if ( (nMinOutputs == 0 && Gia_ManPoNum(pFrames) >= nLits/2+1) ||
(nMinOutputs != 0 && Gia_ManPoNum(pFrames) >= nMinOutputs) )
break;
if ( f == nFramesMax )
break;
Gia_ManStop( pFrames );
pFrames = NULL;
}
if ( f == nFramesMax )
printf( "Stopped unrolling after %d frames.\n", nFramesMax );
if ( pnFrames )
*pnFrames = f;
return pFrames;
}
/**Function*************************************************************
Synopsis [Transforms equiv classes by removing the AB nodes.]
@ -1292,6 +1410,107 @@ Gia_Man_t * Gia_ManEquivToChoices( Gia_Man_t * p, int nSnapshots )
return pNew;
}
#include "aig.h"
#include "saig.h"
#include "cec.h"
#include "giaAig.h"
/**Function*************************************************************
Synopsis [Implements iteration during speculation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_CommandSpecI( Gia_Man_t * pGia, int nFramesInit, int nBTLimitInit, int fStart, int fCheckMiter, int fVerbose )
{
extern int Cec_ManCheckNonTrivialCands( Gia_Man_t * pAig );
Aig_Man_t * pTemp;
Gia_Man_t * pSrm, * pReduce, * pAux;
int nIter, nStart = 0;
if ( pGia->pReprs == NULL || pGia->pNexts == NULL )
{
printf( "Gia_CommandSpecI(): Equivalence classes are not defined.\n" );
return 0;
}
// (spech)* where spech = &srm; restore save3; bmc2 -F 100 -C 25000; &resim
Gia_ManCleanMark0( pGia );
Gia_ManPrintStats( pGia, 0 );
for ( nIter = 0; ; nIter++ )
{
if ( Gia_ManHasNoEquivs(pGia) )
{
printf( "Gia_CommandSpecI: No equivalences left.\n" );
break;
}
printf( "ITER %3d : ", nIter );
// if ( fVerbose )
// printf( "Starting BMC from frame %d.\n", nStart );
// if ( fVerbose )
// Gia_ManPrintStats( pGia, 0 );
Gia_ManPrintStatsClasses( pGia );
// perform speculative reduction
// if ( Gia_ManPoNum(pSrm) <= Gia_ManPoNum(pGia) )
if ( !Cec_ManCheckNonTrivialCands(pGia) )
{
printf( "Gia_CommandSpecI: There are only trivial equiv candidates left (PO drivers). Quitting.\n" );
break;
}
pSrm = Gia_ManSpecReduce( pGia, 0, 0 );
// bmc2 -F 100 -C 25000
{
Gia_Cex_t * pCex;
int nFrames = nFramesInit; // different from default
int nNodeDelta = 2000;
int nBTLimit = nBTLimitInit; // different from default
int nBTLimitAll = 2000000;
pTemp = Gia_ManToAig( pSrm, 0 );
// Aig_ManPrintStats( pTemp );
Gia_ManStop( pSrm );
Saig_BmcPerform( pTemp, nStart, nFrames, nNodeDelta, 20, nBTLimit, nBTLimitAll, fVerbose, 0 );
pCex = pTemp->pSeqModel; pTemp->pSeqModel = NULL;
Aig_ManStop( pTemp );
if ( pCex == NULL )
{
printf( "Gia_CommandSpecI(): Internal BMC could not find a counter-example.\n" );
break;
}
if ( fStart )
nStart = pCex->iFrame;
// perform simulation
{
Cec_ParSim_t Pars, * pPars = &Pars;
Cec_ManSimSetDefaultParams( pPars );
pPars->fCheckMiter = fCheckMiter;
if ( Cec_ManSeqResimulateCounter( pGia, pPars, pCex ) )
{
ABC_FREE( pCex );
break;
}
ABC_FREE( pCex );
}
}
// write equivalence classes
Gia_WriteAiger( pGia, "gore.aig", 0, 0 );
// reduce the model
pReduce = Gia_ManSpecReduce( pGia, 0, 0 );
if ( pReduce )
{
pReduce = Gia_ManSeqStructSweep( pAux = pReduce, 1, 1, 0 );
Gia_ManStop( pAux );
Gia_WriteAiger( pReduce, "gsrm.aig", 0, 0 );
// printf( "Speculatively reduced model was written into file \"%s\".\n", "gsrm.aig" );
// Gia_ManPrintStatsShort( pReduce );
Gia_ManStop( pReduce );
}
}
return 1;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

2
src/aig/int/intCore.c
View File

@ -193,7 +193,7 @@ p->timeCnf += clock() - clk;
}
// likely spurious counter-example
p->nFrames += i;
Inter_ManClean( p );
Inter_ManClean( p );
break;
}
else if ( RetValue == -1 ) // timed out

63
src/aig/ioa/ioaReadAig.c
View File

@ -88,34 +88,27 @@ Vec_Int_t * Ioa_WriteDecodeLiterals( char ** ppPos, int nEntries )
/**Function*************************************************************
Synopsis [Reads the AIG in the binary AIGER format.]
Synopsis [Reads the AIG in from the memory buffer.]
Description []
Description [The buffer constains the AIG in AIGER format. The size gives
the number of types in the buffer. The buffer is allocated by the user
and not deallocated by this procedure.]
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Ioa_ReadAiger( char * pFileName, int fCheck )
Aig_Man_t * Ioa_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck )
{
// Bar_Progress_t * pProgress;
FILE * pFile;
Vec_Int_t * vLits = NULL;
Vec_Ptr_t * vNodes, * vDrivers;//, * vTerms;
Aig_Obj_t * pObj, * pNode0, * pNode1;
Aig_Man_t * pNew;
int nTotal, nInputs, nOutputs, nLatches, nAnds, nFileSize, i;//, iTerm, nDigits;
char * pContents, * pDrivers, * pSymbols, * pCur, * pName;//, * pType;
int nTotal, nInputs, nOutputs, nLatches, nAnds, i;//, iTerm, nDigits;
char * pDrivers, * pSymbols, * pCur;//, * pType;
unsigned uLit0, uLit1, uLit;
// read the file into the buffer
nFileSize = Ioa_FileSize( pFileName );
pFile = fopen( pFileName, "rb" );
pContents = ABC_ALLOC( char, nFileSize );
fread( pContents, nFileSize, 1, pFile );
fclose( pFile );
// check if the input file format is correct
if ( strncmp(pContents, "aig", 3) != 0 || (pContents[3] != ' ' && pContents[3] != '2') )
{
@ -145,10 +138,6 @@ Aig_Man_t * Ioa_ReadAiger( char * pFileName, int fCheck )
// allocate the empty AIG
pNew = Aig_ManStart( nAnds );
pName = Ioa_FileNameGeneric( pFileName );
pNew->pName = Aig_UtilStrsav( pName );
// pNew->pSpec = Ioa_UtilStrsav( pFileName );
ABC_FREE( pName );
// prepare the array of nodes
vNodes = Vec_PtrAlloc( 1 + nInputs + nLatches + nAnds );
@ -355,7 +344,6 @@ Aig_Man_t * Ioa_ReadAiger( char * pFileName, int fCheck )
}
// skipping the comments
ABC_FREE( pContents );
Vec_PtrFree( vNodes );
// remove the extra nodes
@ -372,6 +360,43 @@ Aig_Man_t * Ioa_ReadAiger( char * pFileName, int fCheck )
return pNew;
}
/**Function*************************************************************
Synopsis [Reads the AIG in the binary AIGER format.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Ioa_ReadAiger( char * pFileName, int fCheck )
{
FILE * pFile;
Aig_Man_t * pNew;
char * pName, * pContents;
int nFileSize;
// read the file into the buffer
nFileSize = Ioa_FileSize( pFileName );
pFile = fopen( pFileName, "rb" );
pContents = ABC_ALLOC( char, nFileSize );
fread( pContents, nFileSize, 1, pFile );
fclose( pFile );
pNew = Ioa_ReadAigerFromMemory( pContents, nFileSize, fCheck );
ABC_FREE( pContents );
if ( pNew )
{
pName = Ioa_FileNameGeneric( pFileName );
pNew->pName = Aig_UtilStrsav( pName );
// pNew->pSpec = Ioa_UtilStrsav( pFileName );
ABC_FREE( pName );
}
return pNew;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///

16
src/aig/ntl/ntlFraig.c
View File

@ -21,6 +21,7 @@
#include "ntl.h"
#include "fra.h"
#include "ssw.h"
#include "dch.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@ -400,12 +401,17 @@ Ntl_Man_t * Ntl_ManFraig( Ntl_Man_t * p, int nPartSize, int nConfLimit, int nLev
}
// perform fraiging for the given design
// if ( fUseCSat )
if ( 0 )
if ( fUseCSat )
{
extern Aig_Man_t * Cec_FraigCombinational( Aig_Man_t * pAig, int nConfs, int fVerbose );
pTemp = Cec_FraigCombinational( pAigCol, nConfLimit, fVerbose );
Aig_ManStop( pTemp );
// extern Aig_Man_t * Cec_FraigCombinational( Aig_Man_t * pAig, int nConfs, int fVerbose );
// pTemp = Cec_FraigCombinational( pAigCol, nConfLimit, fVerbose );
// Aig_ManStop( pTemp );
extern void Dch_ComputeEquivalences( Aig_Man_t * pAig, Dch_Pars_t * pPars );
Dch_Pars_t Pars, * pPars = &Pars;
Dch_ManSetDefaultParams( pPars );
pPars->nBTLimit = nConfLimit;
pPars->fVerbose = fVerbose;
Dch_ComputeEquivalences( pAigCol, pPars );
}
else
{

4
src/aig/saig/saig.h
View File

@ -90,10 +90,10 @@ static inline Aig_Obj_t * Saig_ObjLiToLo( Aig_Man_t * p, Aig_Obj_t * pObj ) {
////////////////////////////////////////////////////////////////////////
/*=== sswAbs.c ==========================================================*/
extern Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int nRatio, int fVerbose );
extern Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int nRatio, int fUseBdds, int fUseDprove, int fUseStart, int fVerbose );
/*=== saigBmc.c ==========================================================*/
extern int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fVerbose, int * piFrame, int nCofFanLit );
extern void Saig_BmcPerform( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, int nConfMaxOne, int nConfMaxAll, int fVerbose );
extern void Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite );
/*=== saigCone.c ==========================================================*/
extern void Saig_ManPrintCones( Aig_Man_t * p );
/*=== saigDup.c ==========================================================*/

53
src/aig/saig/saigAbs.c
View File

@ -25,6 +25,7 @@
#include "satStore.h"
#include "ssw.h"
#include "ioa.h"
#include "fra.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@ -694,17 +695,38 @@ Ssw_Cex_t * Saig_ManCexShrink( Aig_Man_t * p, Aig_Man_t * pAbs, Ssw_Cex_t * pCex
SeeAlso []
***********************************************************************/
Aig_Man_t * Saig_ManProofRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlops, int nFrames, int nConfMaxOne, int fVerbose )
Aig_Man_t * Saig_ManProofRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlops, int nFrames, int nConfMaxOne, int fUseBdds, int fUseDprove, int * pnUseStart, int fVerbose )
{
extern void Saig_BmcPerform( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, int nConfMaxOne, int nConfMaxAll, int fVerbose );
extern void Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite );
extern Vec_Int_t * Saig_ManExtendCounterExampleTest( Aig_Man_t * p, int iFirstPi, void * pCex, int fVerbose );
extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fReorderImage, int fVerbose, int fSilent );
Vec_Int_t * vFlopsNew, * vPiToReg;
Aig_Obj_t * pObj;
int i, Entry, iFlop;
Saig_BmcPerform( pAbs, nFrames, 2000, nConfMaxOne, 1000000, fVerbose );
if ( fUseDprove && Aig_ManRegNum(pAbs) > 0 )
{
Fra_Sec_t SecPar, * pSecPar = &SecPar;
int RetValue;
Fra_SecSetDefaultParams( pSecPar );
pSecPar->fVerbose = fVerbose;
RetValue = Fra_FraigSec( pAbs, pSecPar, NULL );
}
else if ( fUseBdds && (Aig_ManRegNum(pAbs) > 0 && Aig_ManRegNum(pAbs) <= 80) )
{
int nBddMax = 1000000;
int nIterMax = nFrames;
int fPartition = 1;
int fReorder = 1;
int fReorderImage = 1;
Aig_ManVerifyUsingBdds( pAbs, nBddMax, nIterMax, fPartition, fReorder, fReorderImage, fVerbose, 0 );
}
else
Saig_BmcPerform( pAbs, pnUseStart? *pnUseStart: 0, nFrames, 2000, 20, nConfMaxOne, 1000000, fVerbose, 0 );
if ( pAbs->pSeqModel == NULL )
return NULL;
if ( pnUseStart )
*pnUseStart = ((Fra_Cex_t *)pAbs->pSeqModel)->iFrame;
// Saig_ManExtendCounterExampleTest( p->pAig, 0, p->pAig->pSeqModel );
vFlopsNew = Saig_ManExtendCounterExampleTest( pAbs, Saig_ManPiNum(p), pAbs->pSeqModel, fVerbose );
if ( Vec_IntSize(vFlopsNew) == 0 )
@ -766,7 +788,7 @@ Aig_Man_t * Saig_ManProofRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vF
SeeAlso []
***********************************************************************/
Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int nRatio, int fVerbose )
Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int nRatio, int fUseBdds, int fUseDprove, int fUseStart, int fVerbose )
{
Aig_Man_t * pResult, * pTemp;
Cnf_Dat_t * pCnf;
@ -845,13 +867,14 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax,
Saig_AbsExtendOneStep( p, vFlops );
if ( fVerbose )
printf( " %d flops.\n", Vec_IntSize(vFlops) );
}
}
*/
// create the resulting AIG
pResult = Saig_ManAbstraction( p, vFlops );
if ( fExtend )
{
int nUseStart = 0;
if ( !fVerbose )
{
printf( "Init : " );
@ -860,21 +883,19 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax,
printf( "Refining abstraction...\n" );
for ( Iter = 0; ; Iter++ )
{
char FileName[100];
pTemp = Saig_ManProofRefine( p, pResult, vFlops, nFramesBmc, nConfMaxBmc, fVerbose );
pTemp = Saig_ManProofRefine( p, pResult, vFlops, nFramesBmc, nConfMaxBmc, fUseBdds, fUseDprove, fUseStart?&nUseStart:NULL, fVerbose );
if ( pTemp == NULL )
break;
Aig_ManStop( pResult );
pResult = pTemp;
printf( "%4d : ", Iter );
printf( "ITER %4d : ", Iter );
if ( !fVerbose )
Aig_ManPrintStats( pResult );
else
printf( " -----------------------------------------------------\n" );
// else
// printf( " -----------------------------------------------------\n" );
// output the intermediate result of abstraction
sprintf( FileName, "gabs%02d.aig", Iter );
Ioa_WriteAiger( pResult, FileName, 0, 0 );
printf( "Intermediate abstracted model was written into file \"%s\".\n", FileName );
Ioa_WriteAiger( pResult, "gabs.aig", 0, 0 );
// printf( "Intermediate abstracted model was written into file \"%s\".\n", "gabs.aig" );
// check if the ratio is reached
if ( 100.0*(Aig_ManRegNum(p)-Aig_ManRegNum(pTemp))/Aig_ManRegNum(p) < 1.0*nRatio )
{
@ -886,6 +907,12 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax,
}
}
Vec_IntFree( vFlops );
// write the final result
if ( pResult )
{
Ioa_WriteAiger( pResult, "gabs.aig", 0, 0 );
printf( "Final abstracted model was written into file \"%s\".\n", "gabs.aig" );
}
return pResult;
}

21
src/aig/saig/saigBmc.c
View File

@ -508,7 +508,7 @@ Ssw_Cex_t * Saig_BmcGenerateCounterExample( Saig_Bmc_t * p )
SeeAlso []
***********************************************************************/
int Saig_BmcSolveTargets( Saig_Bmc_t * p )
int Saig_BmcSolveTargets( Saig_Bmc_t * p, int nStart, int * pnOutsSolved )
{
Aig_Obj_t * pObj;
int i, VarNum, Lit, RetValue;
@ -520,6 +520,8 @@ int Saig_BmcSolveTargets( Saig_Bmc_t * p )
}
Vec_PtrForEachEntry( p->vTargets, pObj, i )
{
if ( ((*pnOutsSolved)++ / Saig_ManPoNum(p->pAig)) < nStart )
continue;
if ( p->pSat->stats.conflicts > p->nConfMaxAll )
return l_Undef;
VarNum = Saig_BmcSatNum( p, Aig_Regular(pObj) );
@ -575,11 +577,12 @@ void Saig_BmcAddTargetsAsPos( Saig_Bmc_t * p )
SeeAlso []
***********************************************************************/
void Saig_BmcPerform( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, int nConfMaxOne, int nConfMaxAll, int fVerbose )
void Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite )
{
Saig_Bmc_t * p;
Aig_Man_t * pNew;
Cnf_Dat_t * pCnf;
int nOutsSolved = 0;
int Iter, RetValue, clk = clock(), clk2;
p = Saig_BmcManStart( pAig, nFramesMax, nNodesMax, nConfMaxOne, nConfMaxAll, fVerbose );
if ( fVerbose )
@ -609,7 +612,7 @@ void Saig_BmcPerform( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, int nConf
Cnf_DataFree( pCnf );
Aig_ManStop( pNew );
// solve the targets
RetValue = Saig_BmcSolveTargets( p );
RetValue = Saig_BmcSolveTargets( p, nStart, &nOutsSolved );
if ( fVerbose )
{
printf( "%3d : F = %3d. O =%4d. And = %7d. Var = %7d. Conf = %7d. ",
@ -620,11 +623,21 @@ void Saig_BmcPerform( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, int nConf
break;
}
if ( RetValue == l_True )
{
assert( p->iFrameFail * Saig_ManPoNum(p->pAig) + p->iOutputFail + 1 == nOutsSolved );
printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ",
p->iOutputFail, p->iFrameFail );
}
else // if ( RetValue == l_False || RetValue == l_Undef )
printf( "No output was asserted in %d frames. ", p->iFramePrev-1 );
ABC_PRT( "Time", clock() - clk );
if ( fVerbOverwrite )
{
ABC_PRTr( "Time", clock() - clk );
}
else
{
ABC_PRT( "Time", clock() - clk );
}
if ( RetValue != l_True )
{
if ( p->iFrameLast >= p->nFramesMax )

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

File diff suppressed because it is too large Load Diff

17
src/base/abci/abcDar.c
View File

@ -1550,7 +1550,7 @@ static void sigfunc( int signo )
SeeAlso []
***********************************************************************/
int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nNodeDelta, int nBTLimit, int nBTLimitAll, int fRewrite, int fNewAlgo, int nCofFanLit, int fVerbose )
int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nStart, int nFrames, int nSizeMax, int nNodeDelta, int nTimeOut, int nBTLimit, int nBTLimitAll, int fRewrite, int fNewAlgo, int nCofFanLit, int fVerbose )
{
Aig_Man_t * pMan;
int status, RetValue = -1, clk = clock();
@ -1632,7 +1632,7 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nNodeDelta,
printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", pCex->iPo, pCex->iFrame );
}
*/
Saig_BmcPerform( pMan, nFrames, nNodeDelta, nBTLimit, nBTLimitAll, fVerbose );
Saig_BmcPerform( pMan, nStart, nFrames, nNodeDelta, nTimeOut, nBTLimit, nBTLimitAll, fVerbose, 0 );
ABC_FREE( pNtk->pModel );
ABC_FREE( pNtk->pSeqModel );
pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
@ -1676,11 +1676,6 @@ int Abc_NtkDarBmcInter_int( Aig_Man_t * pMan, Inter_ManParams_t * pPars )
pTemp = Aig_ManDupOneOutput( pMan, i, 1 );
pTemp = Aig_ManScl( pAux = pTemp, 1, 1, 0 );
Aig_ManStop( pAux );
if ( Aig_ObjFanin0(pObjPo) == Aig_ManConst1(pMan) )
{
Aig_ManStop( pTemp );
continue;
}
RetValue = Inter_ManPerformInterpolation( pTemp, pPars, &iFrame );
if ( pTemp->pSeqModel )
{
@ -1864,7 +1859,7 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar )
}
if ( pSecPar->fTryBmc )
{
RetValue = Abc_NtkDarBmc( pNtk, 20, 100000, -1, 2000, -1, 0, 1, 0, 0 );
RetValue = Abc_NtkDarBmc( pNtk, 0, 20, 100000, -1, 0, 2000, -1, 0, 1, 0, 0 );
if ( RetValue == 0 )
{
printf( "Networks are not equivalent.\n" );
@ -2675,7 +2670,7 @@ ABC_PRT( "Time", clock() - clkTotal );
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int nRatio, int fVerbose )
Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int nRatio, int fUseBdds, int fUseDprove, int fUseStart, int fVerbose )
{
Abc_Ntk_t * pNtkAig;
Aig_Man_t * pMan, * pTemp;
@ -2685,7 +2680,7 @@ Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConf
return NULL;
Aig_ManSetRegNum( pMan, pMan->nRegs );
pMan = Saig_ManProofAbstraction( pTemp = pMan, nFramesMax, nConfMax, fDynamic, fExtend, fSkipProof, nFramesBmc, nConfMaxBmc, nRatio, fVerbose );
pMan = Saig_ManProofAbstraction( pTemp = pMan, nFramesMax, nConfMax, fDynamic, fExtend, fSkipProof, nFramesBmc, nConfMaxBmc, nRatio, fUseBdds, fUseDprove, fUseStart, fVerbose );
if ( pTemp->pSeqModel )
{
ABC_FREE( pNtk->pModel );
@ -3498,7 +3493,7 @@ Abc_Ntk_t * Abc_NtkDarTestNtk( Abc_Ntk_t * pNtk )
return NULL;
/*
Aig_ManSetRegNum( pMan, pMan->nRegs );
pMan = Saig_ManProofAbstraction( pTemp = pMan, 5, 10000, 0, 0, 0, -1, -1, 99, 1 );
pMan = Saig_ManProofAbstraction( pTemp = pMan, 5, 10000, 0, 0, 0, -1, -1, 99, fUseBdds, fUseDprove, 0, 1 );
Aig_ManStop( pTemp );
if ( pMan == NULL )
return NULL;

2
src/base/abci/abcIvy.c
View File

@ -504,7 +504,7 @@ int Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars )
pNtk = Abc_NtkStrash( pNtkTemp = pNtk, 0, 1, 0 );
Abc_NtkDelete( pNtkTemp );
}
// check the case when the 0000 simulation pattern detect the bug
pObj = Abc_NtkPo(pNtk,0);
pFanin = Abc_ObjFanin0(pObj);

5
src/map/amap/amapGraph.c
View File

@ -115,6 +115,7 @@ Amap_Obj_t * Amap_ManCreatePo( Amap_Man_t * p, Amap_Obj_t * pFan0 )
pObj->Level = Amap_Regular(pFan0)->Level;
if ( p->nLevelMax < (int)pObj->Level )
p->nLevelMax = (int)pObj->Level;
assert( p->nLevelMax < 4094 ); // 2^12-2
p->nObjs[AMAP_OBJ_PO]++;
return pObj;
}
@ -142,6 +143,7 @@ Amap_Obj_t * Amap_ManCreateAnd( Amap_Man_t * p, Amap_Obj_t * pFan0, Amap_Obj_t *
pObj->Level = 1 + ABC_MAX( Amap_Regular(pFan0)->Level, Amap_Regular(pFan1)->Level );
if ( p->nLevelMax < (int)pObj->Level )
p->nLevelMax = (int)pObj->Level;
assert( p->nLevelMax < 4094 ); // 2^12-2
p->nObjs[AMAP_OBJ_AND]++;
return pObj;
}
@ -168,6 +170,7 @@ Amap_Obj_t * Amap_ManCreateXor( Amap_Man_t * p, Amap_Obj_t * pFan0, Amap_Obj_t *
pObj->Level = 2 + ABC_MAX( Amap_Regular(pFan0)->Level, Amap_Regular(pFan1)->Level );
if ( p->nLevelMax < (int)pObj->Level )
p->nLevelMax = (int)pObj->Level;
assert( p->nLevelMax < 4094 ); // 2^12-2
p->nObjs[AMAP_OBJ_XOR]++;
return pObj;
}
@ -197,6 +200,7 @@ Amap_Obj_t * Amap_ManCreateMux( Amap_Man_t * p, Amap_Obj_t * pFan0, Amap_Obj_t *
pObj->Level = 2 + ABC_MAX( pObj->Level, Amap_Regular(pFanC)->Level );
if ( p->nLevelMax < (int)pObj->Level )
p->nLevelMax = (int)pObj->Level;
assert( p->nLevelMax < 4094 ); // 2^12-2
p->nObjs[AMAP_OBJ_MUX]++;
return pObj;
}
@ -227,6 +231,7 @@ void Amap_ManCreateChoice( Amap_Man_t * p, Amap_Obj_t * pObj )
// mark the largest level
if ( p->nLevelMax < (int)pObj->Level )
p->nLevelMax = (int)pObj->Level;
assert( p->nLevelMax < 4094 ); // 2^12-2
}
/**Function*************************************************************

4
src/map/amap/amapInt.h
View File

@ -200,8 +200,8 @@ struct Amap_Obj_t_
unsigned fPhase : 1;
unsigned fRepr : 1;
unsigned fPolar : 1; // pCutBest->fInv ^ pSetBest->fInv
unsigned Level : 20;
unsigned nCuts : 12;
unsigned Level : 12; // 20 (July 16, 2009)
unsigned nCuts : 20; // 12 (July 16, 2009)
int nRefs;
int Equiv;
int Fan[3];

26
src/map/amap/amapMerge.c
View File

@ -170,9 +170,10 @@ Amap_Cut_t * Amap_ManCutCreate3( Amap_Man_t * p,
***********************************************************************/
void Amap_ManCutSaveStored( Amap_Man_t * p, Amap_Obj_t * pNode )
{
int nMaxCuts = 500;
int * pBuffer;
Amap_Cut_t * pNext, * pCut;
int i, nWords, Entry, nCuts;
int i, nWords, Entry, nCuts, nCuts2;
assert( pNode->pData == NULL );
// count memory needed
nCuts = 1;
@ -182,7 +183,8 @@ void Amap_ManCutSaveStored( Amap_Man_t * p, Amap_Obj_t * pNode )
for ( pCut = p->ppCutsTemp[Entry]; pCut; pCut = *Amap_ManCutNextP(pCut) )
{
nCuts++;
nWords += pCut->nFans + 1;
if ( nCuts < nMaxCuts )
nWords += pCut->nFans + 1;
}
}
p->nBytesUsed += 4*nWords;
@ -194,17 +196,23 @@ void Amap_ManCutSaveStored( Amap_Man_t * p, Amap_Obj_t * pNode )
pNext->fInv = 0;
pNext->nFans = 1;
pNext->Fans[0] = Amap_Var2Lit(pNode->Id, 0);
pNext = (Amap_Cut_t *)(pBuffer + 2);
pNext = (Amap_Cut_t *)(pBuffer + 2);
// add other cuts
nCuts2 = 1;
Vec_IntForEachEntry( p->vTemp, Entry, i )
{
for ( pCut = p->ppCutsTemp[Entry]; pCut; pCut = *Amap_ManCutNextP(pCut) )
{
memcpy( pNext, pCut, sizeof(int) * (pCut->nFans + 1) );
pNext = (Amap_Cut_t *)((int *)pNext + pCut->nFans + 1);
nCuts2++;
if ( nCuts2 < nMaxCuts )
{
memcpy( pNext, pCut, sizeof(int) * (pCut->nFans + 1) );
pNext = (Amap_Cut_t *)((int *)pNext + pCut->nFans + 1);
}
}
p->ppCutsTemp[Entry] = NULL;
}
assert( nCuts == nCuts2 );
assert( (int *)pNext - pBuffer == nWords );
// restore the storage
Vec_IntClear( p->vTemp );
@ -213,7 +221,8 @@ void Amap_ManCutSaveStored( Amap_Man_t * p, Amap_Obj_t * pNode )
if ( p->ppCutsTemp[i] != NULL )
printf( "Amap_ManCutSaveStored(): Error!\n" );
pNode->pData = (Amap_Cut_t *)pBuffer;
pNode->nCuts = nCuts;
pNode->nCuts = ABC_MIN( nCuts, nMaxCuts-1 );
assert( nCuts < (1<<20) );
// printf("%d ", nCuts );
// verify cuts
pCut = NULL;
@ -221,6 +230,8 @@ void Amap_ManCutSaveStored( Amap_Man_t * p, Amap_Obj_t * pNode )
// for ( i = 0, pNext = (Amap_Cut_t *)pNode->pData; i < (int)pNode->nCuts;
// i++, pNext = Amap_ManCutNext(pNext) )
{
if ( i == nMaxCuts )
break;
assert( pCut == NULL || pCut->iMat <= pNext->iMat );
pCut = pNext;
}
@ -311,8 +322,11 @@ void Amap_ManMergeNodeChoice( Amap_Man_t * p, Amap_Obj_t * pNode )
for ( pTemp = pNode; pTemp; pTemp = Amap_ObjChoice(p, pTemp) )
{
Amap_NodeForEachCut( pTemp, pCut, c )
{
if (!pCut) break; // mikelee added; abort when pCut is NULL
if ( pCut->iMat )
Amap_ManCutStore( p, pCut, pNode->fPhase ^ pTemp->fPhase );
}
pTemp->pData = NULL;
}
Amap_ManCutSaveStored( p, pNode );

1
src/misc/util/abc_global.h
View File

@ -154,6 +154,7 @@ typedef unsigned __int64 ABC_UINT64_T;
#define ABC_INFINITY (100000000)
#define ABC_PRT(a,t) (printf("%s = ", (a)), printf("%7.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC)))
#define ABC_PRTr(a,t) (printf("%s = ", (a)), printf("%7.2f sec\r", (float)(t)/(float)(CLOCKS_PER_SEC)))
#define ABC_PRTn(a,t) (printf("%s = ", (a)), printf("%6.2f sec ", (float)(t)/(float)(CLOCKS_PER_SEC)))
#define ABC_PRTP(a,t,T) (printf("%s = ", (a)), printf("%7.2f sec (%6.2f %%)\n", (float)(t)/(float)(CLOCKS_PER_SEC), (T)? 100.0*(t)/(T) : 0.0))
#define ABC_PRM(a,f) (printf("%s = ", (a)), printf("%7.2f Mb ", 1.0*(f)/(1<<20)))

4
src/opt/mfs/mfsCore.c
View File

@ -265,6 +265,9 @@ clk = clock();
p->nNodesBad++;
return 1;
}
clk = clock();
Abc_NtkMfsConstructGia( p );
p->timeGia += clock() - clk;
// solve the SAT problem
if ( p->pPars->fPower )
Abc_NtkMfsEdgePower( p, pNode );
@ -277,6 +280,7 @@ clk = clock();
Abc_NtkMfsResubNode2( p, pNode );
}
p->timeSat += clock() - clk;
Abc_NtkMfsDeconstructGia( p );
return 1;
}

12
src/opt/mfs/mfsInt.h
View File

@ -32,6 +32,7 @@
#include "satSolver.h"
#include "satStore.h"
#include "bdc.h"
#include "gia.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
@ -65,6 +66,12 @@ struct Mfs_Man_t_
int nCexes; // the numbe rof current counter-examples
int nSatCalls;
int nSatCexes;
// intermediate AIG data
Gia_Man_t * pGia; // replica of the AIG in the new package
Gia_Obj_t ** pSat2Gia; // mapping of PO SAT var into internal GIA nodes
Tas_Man_t * pTas; // the SAT solver
Vec_Int_t * vCex; // the counter-example
Vec_Ptr_t * vGiaLits; // literals given as assumptions
// used for bidecomposition
Vec_Int_t * vTruth;
Bdc_Man_t * pManDec;
@ -110,6 +117,7 @@ struct Mfs_Man_t_
int timeWin;
int timeDiv;
int timeAig;
int timeGia;
int timeCnf;
int timeSat;
int timeInt;
@ -155,6 +163,10 @@ extern double Abc_NtkConstraintRatio( Mfs_Man_t * p, Abc_Obj_t * pNode
/*=== mfsWin.c ==========================================================*/
extern Vec_Ptr_t * Abc_MfsComputeRoots( Abc_Obj_t * pNode, int nWinTfoMax, int nFanoutLimit );
/*=== mfsGia.c ==========================================================*/
extern void Abc_NtkMfsConstructGia( Mfs_Man_t * p );
extern void Abc_NtkMfsDeconstructGia( Mfs_Man_t * p );
extern int Abc_NtkMfsTryResubOnceGia( Mfs_Man_t * p, int * pCands, int nCands );
#ifdef __cplusplus
}

5
src/opt/mfs/mfsMan.c
View File

@ -157,15 +157,16 @@ void Mfs_ManPrint( Mfs_Man_t * p )
printf( "Nodes resyn = %d. Ratio = %5.2f. Total AIG node gain = %d. Timeouts = %d.\n",
p->nNodesDec, 1.0 * p->nNodesDec / p->nNodesTried, p->nNodesGained, p->nTimeOuts );
}
/*
ABC_PRTP( "Win", p->timeWin , p->timeTotal );
ABC_PRTP( "Div", p->timeDiv , p->timeTotal );
ABC_PRTP( "Aig", p->timeAig , p->timeTotal );
ABC_PRTP( "Gia", p->timeGia , p->timeTotal );
ABC_PRTP( "Cnf", p->timeCnf , p->timeTotal );
ABC_PRTP( "Sat", p->timeSat-p->timeInt , p->timeTotal );
ABC_PRTP( "Int", p->timeInt , p->timeTotal );
ABC_PRTP( "ALL", p->timeTotal , p->timeTotal );
*/
}
/**Function*************************************************************

8
src/opt/mfs/mfsResub.c
View File

@ -99,9 +99,17 @@ int Abc_NtkMfsTryResubOnce( Mfs_Man_t * p, int * pCands, int nCands )
{
unsigned * pData;
int RetValue, iVar, i;
int clk = clock(), RetValue2 = Abc_NtkMfsTryResubOnceGia( p, pCands, nCands );
p->timeGia += clock() - clk;
p->nSatCalls++;
RetValue = sat_solver_solve( p->pSat, pCands, pCands + nCands, (ABC_INT64_T)p->pPars->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
// assert( RetValue == l_False || RetValue == l_True );
if ( RetValue != l_Undef && RetValue2 != -1 )
{
assert( (RetValue == l_False) == (RetValue2 == 1) );
}
if ( RetValue == l_False )
return 1;
if ( RetValue != l_True )

1
src/opt/mfs/module.make
View File

@ -1,5 +1,6 @@
SRC += src/opt/mfs/mfsCore.c \
src/opt/mfs/mfsDiv.c \
src/opt/mfs/mfsGia.c \
src/opt/mfs/mfsInter.c \
src/opt/mfs/mfsMan.c \
src/opt/mfs/mfsResub.c \