From ae4b51351c93983a1285ce1028e3bbd90a6d5721 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Thu, 13 Jan 2011 12:38:59 -0800
Subject: Cumulative changes in the last few weeks.
---
src/aig/cnf/cnf.h | 4 ++
src/aig/cnf/cnfCore.c | 53 ++++++++++++++
src/aig/cnf/cnfMan.c | 2 +
src/aig/cnf/cnfWrite.c | 171 +++++++++++++++++++++++++++++++++++++++++++++-
src/aig/fra/fra.h | 2 +
src/aig/fra/fraSec.c | 23 ++++++-
src/aig/gia/gia.h | 1 +
src/aig/gia/giaEquiv.c | 5 ++
src/aig/gia/giaSim.c | 29 +++++++-
src/aig/gia/giaUtil.c | 4 ++
src/aig/gia/module.make | 1 +
src/aig/live/liveness.c | 2 +-
src/aig/live/ltl_parser.c | 1 +
src/aig/llb/llbCore.c | 2 +-
src/aig/llb/llbReach.c | 2 +-
src/aig/mfx/mfxInt.h | 3 +-
src/aig/mfx/mfxInter.c | 18 ++---
src/aig/mfx/mfxMan.c | 6 +-
src/aig/mfx/mfxResub.c | 12 ++--
src/aig/mfx/mfxSat.c | 10 +--
src/aig/saig/module.make | 1 +
src/aig/saig/saig.h | 3 +-
src/aig/saig/saigBmc2.c | 9 ++-
src/aig/saig/saigDup.c | 52 +++++++++++++-
src/aig/saig/saigPhase.c | 68 +++++++++++++++---
src/aig/ssw/ssw.h | 1 +
src/aig/ssw/sswConstr.c | 4 +-
src/aig/ssw/sswCore.c | 2 +
src/aig/ssw/sswDyn.c | 4 +-
src/aig/ssw/sswInt.h | 2 +-
src/aig/ssw/sswSemi.c | 2 +-
src/aig/ssw/sswSim.c | 96 ++++++--------------------
src/aig/ssw/sswSweep.c | 52 ++++++++++++--
33 files changed, 514 insertions(+), 133 deletions(-)
(limited to 'src/aig')
diff --git a/src/aig/cnf/cnf.h b/src/aig/cnf/cnf.h
index 7c3bf06b..42dcd9a9 100644
--- a/src/aig/cnf/cnf.h
+++ b/src/aig/cnf/cnf.h
@@ -62,6 +62,8 @@ struct Cnf_Dat_t_
int nClauses; // the number of CNF clauses
int ** pClauses; // the CNF clauses
int * pVarNums; // the number of CNF variable for each node ID (-1 if unused)
+ int * pObj2Clause; // the mapping of objects into clauses
+ int * pObj2Count; // the mapping of objects into clause number
};
// the cut used to represent node in the AIG
@@ -125,6 +127,7 @@ static inline void Cnf_ObjSetBestCut( Aig_Obj_t * pObj, Cnf_Cut_t * pCut
/*=== cnfCore.c ========================================================*/
extern Vec_Int_t * Cnf_DeriveMappingArray( Aig_Man_t * pAig );
extern Cnf_Dat_t * Cnf_Derive( Aig_Man_t * pAig, int nOutputs );
+extern Cnf_Dat_t * Cnf_DeriveOther( Aig_Man_t * pAig );
extern Cnf_Man_t * Cnf_ManRead();
extern void Cnf_ClearMemory();
/*=== cnfCut.c ========================================================*/
@@ -167,6 +170,7 @@ extern Vec_Int_t * Cnf_DataCollectCoSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p
extern Vec_Int_t * Cnf_ManWriteCnfMapping( Cnf_Man_t * p, Vec_Ptr_t * vMapped );
extern void Cnf_SopConvertToVector( char * pSop, int nCubes, Vec_Int_t * vCover );
extern Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs );
+extern Cnf_Dat_t * Cnf_ManWriteCnfOther( Cnf_Man_t * p, Vec_Ptr_t * vMapped );
extern Cnf_Dat_t * Cnf_DeriveSimple( Aig_Man_t * p, int nOutputs );
extern Cnf_Dat_t * Cnf_DeriveSimpleForRetiming( Aig_Man_t * p );
diff --git a/src/aig/cnf/cnfCore.c b/src/aig/cnf/cnfCore.c
index 85c971c2..eb46e704 100644
--- a/src/aig/cnf/cnfCore.c
+++ b/src/aig/cnf/cnfCore.c
@@ -138,6 +138,59 @@ p->timeSave = clock() - clk;
//ABC_PRT( "Saving ", p->timeSave );
return pCnf;
}
+
+/**Function*************************************************************
+
+ Synopsis [Converts AIG into the SAT solver.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Cnf_Dat_t * Cnf_DeriveOther( Aig_Man_t * pAig )
+{
+ Cnf_Man_t * p;
+ Cnf_Dat_t * pCnf;
+ Vec_Ptr_t * vMapped;
+ Aig_MmFixed_t * pMemCuts;
+ int clk;
+ // allocate the CNF manager
+ if ( s_pManCnf == NULL )
+ s_pManCnf = Cnf_ManStart();
+ // connect the managers
+ p = s_pManCnf;
+ p->pManAig = pAig;
+
+ // generate cuts for all nodes, assign cost, and find best cuts
+clk = clock();
+ pMemCuts = Dar_ManComputeCuts( pAig, 10, 0 );
+p->timeCuts = clock() - clk;
+
+ // find the mapping
+clk = clock();
+ Cnf_DeriveMapping( p );
+p->timeMap = clock() - clk;
+// Aig_ManScanMapping( p, 1 );
+
+ // convert it into CNF
+clk = clock();
+ Cnf_ManTransferCuts( p );
+ vMapped = Cnf_ManScanMapping( p, 1, 1 );
+ pCnf = Cnf_ManWriteCnfOther( p, vMapped );
+ Vec_PtrFree( vMapped );
+ Aig_MmFixedStop( pMemCuts, 0 );
+p->timeSave = clock() - clk;
+
+ // reset reference counters
+ Aig_ManResetRefs( pAig );
+//ABC_PRT( "Cuts ", p->timeCuts );
+//ABC_PRT( "Map ", p->timeMap );
+//ABC_PRT( "Saving ", p->timeSave );
+ return pCnf;
+}
/**Function*************************************************************
diff --git a/src/aig/cnf/cnfMan.c b/src/aig/cnf/cnfMan.c
index 762673ad..837ca2c2 100644
--- a/src/aig/cnf/cnfMan.c
+++ b/src/aig/cnf/cnfMan.c
@@ -180,6 +180,8 @@ void Cnf_DataFree( Cnf_Dat_t * p )
{
if ( p == NULL )
return;
+ ABC_FREE( p->pObj2Clause );
+ ABC_FREE( p->pObj2Count );
ABC_FREE( p->pClauses[0] );
ABC_FREE( p->pClauses );
ABC_FREE( p->pVarNums );
diff --git a/src/aig/cnf/cnfWrite.c b/src/aig/cnf/cnfWrite.c
index 4f737305..7a9443f2 100644
--- a/src/aig/cnf/cnfWrite.c
+++ b/src/aig/cnf/cnfWrite.c
@@ -245,8 +245,7 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs )
//printf( "\n" );
// allocate CNF
- pCnf = ABC_ALLOC( Cnf_Dat_t, 1 );
- memset( pCnf, 0, sizeof(Cnf_Dat_t) );
+ pCnf = ABC_CALLOC( Cnf_Dat_t, 1 );
pCnf->pMan = p->pManAig;
pCnf->nLiterals = nLiterals;
pCnf->nClauses = nClauses;
@@ -367,6 +366,174 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs )
// verify that the correct number of literals and clauses was written
assert( pLits - pCnf->pClauses[0] == nLiterals );
assert( pClas - pCnf->pClauses == nClauses );
+//Cnf_DataPrint( pCnf, 1 );
+ return pCnf;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Derives CNF for the mapping.]
+
+ Description [Derives CNF with obj IDs as SAT vars and mapping of
+ objects into clauses (pObj2Clause and pObj2Count).]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Cnf_Dat_t * Cnf_ManWriteCnfOther( Cnf_Man_t * p, Vec_Ptr_t * vMapped )
+{
+ Aig_Obj_t * pObj;
+ Cnf_Dat_t * pCnf;
+ Cnf_Cut_t * pCut;
+ Vec_Int_t * vCover, * vSopTemp;
+ int OutVar, PoVar, pVars[32], * pLits, ** pClas;
+ unsigned uTruth;
+ int i, k, nLiterals, nClauses, Cube;
+
+ // count the number of literals and clauses
+ nLiterals = 1 + 4 * Aig_ManPoNum( p->pManAig );
+ nClauses = 1 + 2 * Aig_ManPoNum( p->pManAig );
+ Vec_PtrForEachEntry( Aig_Obj_t *, vMapped, pObj, i )
+ {
+ assert( Aig_ObjIsNode(pObj) );
+ pCut = Cnf_ObjBestCut( pObj );
+ // positive polarity of the cut
+ if ( pCut->nFanins < 5 )
+ {
+ uTruth = 0xFFFF & *Cnf_CutTruth(pCut);
+ nLiterals += Cnf_SopCountLiterals( p->pSops[uTruth], p->pSopSizes[uTruth] ) + p->pSopSizes[uTruth];
+ assert( p->pSopSizes[uTruth] >= 0 );
+ nClauses += p->pSopSizes[uTruth];
+ }
+ else
+ {
+ nLiterals += Cnf_IsopCountLiterals( pCut->vIsop[1], pCut->nFanins ) + Vec_IntSize(pCut->vIsop[1]);
+ nClauses += Vec_IntSize(pCut->vIsop[1]);
+ }
+ // negative polarity of the cut
+ if ( pCut->nFanins < 5 )
+ {
+ uTruth = 0xFFFF & ~*Cnf_CutTruth(pCut);
+ nLiterals += Cnf_SopCountLiterals( p->pSops[uTruth], p->pSopSizes[uTruth] ) + p->pSopSizes[uTruth];
+ assert( p->pSopSizes[uTruth] >= 0 );
+ nClauses += p->pSopSizes[uTruth];
+ }
+ else
+ {
+ nLiterals += Cnf_IsopCountLiterals( pCut->vIsop[0], pCut->nFanins ) + Vec_IntSize(pCut->vIsop[0]);
+ nClauses += Vec_IntSize(pCut->vIsop[0]);
+ }
+ }
+
+ // allocate CNF
+ pCnf = ABC_CALLOC( Cnf_Dat_t, 1 );
+ pCnf->pMan = p->pManAig;
+ pCnf->nLiterals = nLiterals;
+ pCnf->nClauses = nClauses;
+ pCnf->pClauses = ABC_ALLOC( int *, nClauses + 1 );
+ pCnf->pClauses[0] = ABC_ALLOC( int, nLiterals );
+ pCnf->pClauses[nClauses] = pCnf->pClauses[0] + nLiterals;
+ // create room for variable numbers
+ pCnf->pObj2Clause = ABC_ALLOC( int, Aig_ManObjNumMax(p->pManAig) );
+ pCnf->pObj2Count = ABC_ALLOC( int, Aig_ManObjNumMax(p->pManAig) );
+ for ( i = 0; i < Aig_ManObjNumMax(p->pManAig); i++ )
+ pCnf->pObj2Clause[i] = pCnf->pObj2Count[i] = -1;
+ pCnf->nVars = Aig_ManObjNumMax(p->pManAig);
+
+ // clear the PI counters
+ Aig_ManForEachPi( p->pManAig, pObj, i )
+ pCnf->pObj2Count[pObj->Id] = 0;
+
+ // assign the clauses
+ vSopTemp = Vec_IntAlloc( 1 << 16 );
+ pLits = pCnf->pClauses[0];
+ pClas = pCnf->pClauses;
+ Vec_PtrForEachEntry( Aig_Obj_t *, vMapped, pObj, i )
+ {
+ // remember the starting clause
+ pCnf->pObj2Clause[pObj->Id] = pClas - pCnf->pClauses;
+ pCnf->pObj2Count[pObj->Id] = 0;
+
+ // get the best cut
+ pCut = Cnf_ObjBestCut( pObj );
+ // save variables of this cut
+ OutVar = pObj->Id;
+ for ( k = 0; k < (int)pCut->nFanins; k++ )
+ {
+ pVars[k] = pCut->pFanins[k];
+ assert( pVars[k] <= Aig_ManObjNumMax(p->pManAig) );
+ }
+
+ // positive polarity of the cut
+ if ( pCut->nFanins < 5 )
+ {
+ uTruth = 0xFFFF & *Cnf_CutTruth(pCut);
+ Cnf_SopConvertToVector( p->pSops[uTruth], p->pSopSizes[uTruth], vSopTemp );
+ vCover = vSopTemp;
+ }
+ else
+ vCover = pCut->vIsop[1];
+ Vec_IntForEachEntry( vCover, Cube, k )
+ {
+ *pClas++ = pLits;
+ *pLits++ = 2 * OutVar;
+ pLits += Cnf_IsopWriteCube( Cube, pCut->nFanins, pVars, pLits );
+ }
+ pCnf->pObj2Count[pObj->Id] += Vec_IntSize(vCover);
+
+ // negative polarity of the cut
+ if ( pCut->nFanins < 5 )
+ {
+ uTruth = 0xFFFF & ~*Cnf_CutTruth(pCut);
+ Cnf_SopConvertToVector( p->pSops[uTruth], p->pSopSizes[uTruth], vSopTemp );
+ vCover = vSopTemp;
+ }
+ else
+ vCover = pCut->vIsop[0];
+ Vec_IntForEachEntry( vCover, Cube, k )
+ {
+ *pClas++ = pLits;
+ *pLits++ = 2 * OutVar + 1;
+ pLits += Cnf_IsopWriteCube( Cube, pCut->nFanins, pVars, pLits );
+ }
+ pCnf->pObj2Count[pObj->Id] += Vec_IntSize(vCover);
+ }
+ Vec_IntFree( vSopTemp );
+
+ // write the output literals
+ Aig_ManForEachPo( p->pManAig, pObj, i )
+ {
+ // remember the starting clause
+ pCnf->pObj2Clause[pObj->Id] = pClas - pCnf->pClauses;
+ pCnf->pObj2Count[pObj->Id] = 2;
+ // get variables
+ OutVar = Aig_ObjFanin0(pObj)->Id;
+ PoVar = pObj->Id;
+ // first clause
+ *pClas++ = pLits;
+ *pLits++ = 2 * PoVar;
+ *pLits++ = 2 * OutVar + !Aig_ObjFaninC0(pObj);
+ // second clause
+ *pClas++ = pLits;
+ *pLits++ = 2 * PoVar + 1;
+ *pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj);
+ }
+
+ // remember the starting clause
+ pCnf->pObj2Clause[Aig_ManConst1(p->pManAig)->Id] = pClas - pCnf->pClauses;
+ pCnf->pObj2Count[Aig_ManConst1(p->pManAig)->Id] = 1;
+ // write the constant literal
+ OutVar = Aig_ManConst1(p->pManAig)->Id;
+ *pClas++ = pLits;
+ *pLits++ = 2 * OutVar;
+
+ // verify that the correct number of literals and clauses was written
+ assert( pLits - pCnf->pClauses[0] == nLiterals );
+ assert( pClas - pCnf->pClauses == nClauses );
+//Cnf_DataPrint( pCnf, 1 );
return pCnf;
}
diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index b046cc47..aee38d08 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -123,6 +123,7 @@ struct Fra_Sec_t_
int nBddVarsMax; // the state space limit for BDD reachability
int nBddMax; // the max number of BDD nodes
int nBddIterMax; // the limit on the number of BDD iterations
+ int nPdrTimeout; // the timeout for PDR in the end
int fPhaseAbstract; // enables phase abstraction
int fRetimeFirst; // enables most-forward retiming at the beginning
int fRetimeRegs; // enables min-register retiming at the beginning
@@ -134,6 +135,7 @@ struct Fra_Sec_t_
int fReorderImage; // enables BDD reordering during image computation
int fStopOnFirstFail; // enables stopping after first output of a miter has failed to prove
int fUseNewProver; // the new prover
+ int fUsePdr; // the PDR
int fSilent; // disables all output
int fVerbose; // enables verbose reporting of statistics
int fVeryVerbose; // enables very verbose reporting
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index 1576a70a..7608791f 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -24,6 +24,7 @@
#include "ssw.h"
#include "saig.h"
#include "bbr.h"
+#include "pdr.h"
ABC_NAMESPACE_IMPL_START
@@ -70,6 +71,8 @@ void Fra_SecSetDefaultParams( Fra_Sec_t * p )
p->fReorderImage = 1; // enables variable reordering during image computation
p->fStopOnFirstFail = 1; // enables stopping after first output of a miter has failed to prove
p->fUseNewProver = 0; // enables new prover
+ p->fUsePdr = 1; // enables PDR
+ p->nPdrTimeout = 60; // enabled PDR timeout
p->fSilent = 0; // disables all output
p->fVerbose = 0; // enables verbose reporting of statistics
p->fVeryVerbose = 0; // enables very verbose reporting
@@ -539,7 +542,7 @@ clk = clock();
}
else
{
- Aig_Man_t * pNewOrpos = Said_ManDupOrpos( pNew );
+ Aig_Man_t * pNewOrpos = Saig_ManDupOrpos( pNew );
RetValue = Inter_ManPerformInterpolation( pNewOrpos, pPars, &Depth );
if ( pNewOrpos->pSeqModel )
{
@@ -582,6 +585,24 @@ ABC_PRT( "Time", clock() - clk );
RetValue = Aig_ManVerifyUsingBdds( pNew, pPars );
}
+ // try PDR
+ if ( pParSec->fUsePdr && RetValue == -1 && Aig_ManRegNum(pNew) > 0 )
+ {
+ Abc_Cex_t * pCex = NULL;
+ Aig_Man_t * pNewOrpos = Saig_ManDupOrpos( pNew );
+ Pdr_Par_t Pars, * pPars = &Pars;
+ Pdr_ManSetDefaultParams( pPars );
+ pPars->nTimeOut = pParSec->nPdrTimeout;
+ pPars->fVerbose = pParSec->fVerbose;
+ if ( pParSec->fVerbose )
+ printf( "Running property directed reachability...\n" );
+ RetValue = Pdr_ManSolve( pNewOrpos, pPars, &pCex );
+ if ( pCex )
+ pCex->iPo = Ssw_SmlFindOutputCounterExample( pNew, pCex );
+ Aig_ManStop( pNewOrpos );
+ pNew->pSeqModel = pCex;
+ }
+
finish:
// report the miter
if ( RetValue == 1 )
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 3358ca76..e3546686 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -179,6 +179,7 @@ struct Gia_ParSim_t_
// user-controlled parameters
int nWords; // the number of machine words
int nIters; // the number of timeframes
+ int RandSeed; // seed to generate random numbers
int TimeLimit; // time limit in seconds
int fCheckMiter; // check if miter outputs are non-zero
int fVerbose; // enables verbose output
diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c
index 4c19b4f5..581383ea 100644
--- a/src/aig/gia/giaEquiv.c
+++ b/src/aig/gia/giaEquiv.c
@@ -1049,6 +1049,11 @@ Gia_Man_t * Gia_ManSpecReduceInitFrames( Gia_Man_t * p, Abc_Cex_t * pInit, int n
break;
if ( f == nFramesMax )
break;
+ if ( Gia_ManAndNum(pFrames) > 500000 )
+ {
+ Gia_ManStop( pFrames );
+ return NULL;
+ }
Gia_ManStop( pFrames );
pFrames = NULL;
}
diff --git a/src/aig/gia/giaSim.c b/src/aig/gia/giaSim.c
index 68b50fb6..1de1a2d4 100644
--- a/src/aig/gia/giaSim.c
+++ b/src/aig/gia/giaSim.c
@@ -65,6 +65,7 @@ void Gia_ManSimSetDefaultParams( Gia_ParSim_t * p )
// user-controlled parameters
p->nWords = 8; // the number of machine words
p->nIters = 32; // the number of timeframes
+ p->RandSeed = 0; // the seed to generate random numbers
p->TimeLimit = 60; // time limit in seconds
p->fCheckMiter = 0; // check if miter outputs are non-zero
p->fVerbose = 0; // enables verbose output
@@ -437,9 +438,8 @@ Abc_Cex_t * Gia_ManGenerateCounter( Gia_Man_t * pAig, int iFrame, int iOut, int
int f, i, w, iPioId, Counter;
p = Gia_ManAllocCounterExample( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), iFrame+1 );
p->iFrame = iFrame;
- p->iPo = iOut;
+ p->iPo = iOut;
// fill in the binary data
- Gia_ManRandom( 1 );
Counter = p->nRegs;
pData = ABC_ALLOC( unsigned, nWords );
for ( f = 0; f <= iFrame; f++, Counter += p->nPis )
@@ -457,6 +457,25 @@ Abc_Cex_t * Gia_ManGenerateCounter( Gia_Man_t * pAig, int iFrame, int iOut, int
return p;
}
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Gia_ManResetRandom( Gia_ParSim_t * pPars )
+{
+ int i;
+ Gia_ManRandom( 1 );
+ for ( i = 0; i < pPars->RandSeed; i++ )
+ Gia_ManRandom( 0 );
+}
+
/**Function*************************************************************
Synopsis []
@@ -470,12 +489,15 @@ Abc_Cex_t * Gia_ManGenerateCounter( Gia_Man_t * pAig, int iFrame, int iOut, int
***********************************************************************/
int Gia_ManSimSimulate( Gia_Man_t * pAig, Gia_ParSim_t * pPars )
{
+ extern int Gia_ManSimSimulateEquiv( Gia_Man_t * pAig, Gia_ParSim_t * pPars );
Gia_ManSim_t * p;
int i, clkTotal = clock();
int iOut, iPat, RetValue = 0;
+ if ( pAig->pReprs && pAig->pNexts )
+ return Gia_ManSimSimulateEquiv( pAig, pPars );
ABC_FREE( pAig->pCexSeq );
p = Gia_ManSimCreate( pAig, pPars );
- Gia_ManRandom( 1 );
+ Gia_ManResetRandom( pPars );
Gia_ManSimInfoInit( p );
for ( i = 0; i < pPars->nIters; i++ )
{
@@ -487,6 +509,7 @@ int Gia_ManSimSimulate( Gia_Man_t * pAig, Gia_ParSim_t * pPars )
}
if ( pPars->fCheckMiter && Gia_ManCheckPos( p, &iOut, &iPat ) )
{
+ Gia_ManResetRandom( pPars );
pPars->iOutFail = iOut;
pAig->pCexSeq = Gia_ManGenerateCounter( pAig, i, iOut, p->nWords, iPat, p->vCis2Ids );
Abc_Print( 1, "Networks are NOT EQUIVALENT. Output %d was asserted in frame %d. ", iOut, i );
diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c
index 002e766d..82bdb367 100644
--- a/src/aig/gia/giaUtil.c
+++ b/src/aig/gia/giaUtil.c
@@ -952,8 +952,12 @@ int Gia_ManVerifyCounterExample( Gia_Man_t * pAig, Abc_Cex_t * p, int fDualOut )
(Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
Gia_ManForEachCo( pAig, pObj, k )
pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
+ if ( i == p->iFrame )
+ break;
Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, k )
+ {
pObjRo->fMark0 = pObjRi->fMark0;
+ }
}
assert( iBit == p->nBits );
if ( fDualOut )
diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make
index fc1c5c73..fd0e0a5e 100644
--- a/src/aig/gia/module.make
+++ b/src/aig/gia/module.make
@@ -29,6 +29,7 @@ SRC += src/aig/gia/gia.c \
src/aig/gia/giaScl.c \
src/aig/gia/giaShrink.c \
src/aig/gia/giaSim.c \
+ src/aig/gia/giaSim2.c \
src/aig/gia/giaSort.c \
src/aig/gia/giaSpeedup.c \
src/aig/gia/giaSupMin.c \
diff --git a/src/aig/live/liveness.c b/src/aig/live/liveness.c
index e0511556..324865a9 100644
--- a/src/aig/live/liveness.c
+++ b/src/aig/live/liveness.c
@@ -2230,7 +2230,7 @@ Aig_Man_t * LivenessToSafetyTransformationWithLTL( int mode, Abc_Ntk_t * pNtk, A
#ifdef ALLOW_SAFETY_PROPERTIES
printf("liveness output is conjoined with safety assertions\n");
pObjSafetyAndLiveToSafety = Aig_Or( pNew, pObjSafetyGate, pNegatedSafetyConjunction );
- pObjSafetyPropertyOutput = Vec_PtrEntry( vPoForLtlProps, iii );
+ pObjSafetyPropertyOutput = (Aig_Obj_t *)Vec_PtrEntry( vPoForLtlProps, iii );
Aig_ObjPatchFanin0( pNew, pObjSafetyPropertyOutput, pObjSafetyAndLiveToSafety );
#else
pObjSafetyPropertyOutput = Vec_PtrEntry( vPoForLtlProps, iii );
diff --git a/src/aig/live/ltl_parser.c b/src/aig/live/ltl_parser.c
index 66d7f72d..58125818 100644
--- a/src/aig/live/ltl_parser.c
+++ b/src/aig/live/ltl_parser.c
@@ -78,6 +78,7 @@ void Abc_FrameCopyLTLDataBase( Abc_Frame_t *pAbc, Abc_Ntk_t * pNtk )
if( pAbc->vLTLProperties_global != NULL )
{
// printf("Deleting exisitng LTL database from the frame\n");
+ Vec_PtrFree( pAbc->vLTLProperties_global );
pAbc->vLTLProperties_global = NULL;
}
pAbc->vLTLProperties_global = Vec_PtrAlloc(Vec_PtrSize(pNtk->vLtlProperties));
diff --git a/src/aig/llb/llbCore.c b/src/aig/llb/llbCore.c
index 562a9800..cbd527e2 100644
--- a/src/aig/llb/llbCore.c
+++ b/src/aig/llb/llbCore.c
@@ -48,7 +48,7 @@ void Llb_ManSetDefaultParams( Gia_ParLlb_t * p )
{
memset( p, 0, sizeof(Gia_ParLlb_t) );
p->nBddMax = 1000000;
- p->nIterMax = 1000;
+ p->nIterMax = 10000000;
p->nClusterMax = 20;
p->nHintDepth = 0;
p->HintFirst = 0;
diff --git a/src/aig/llb/llbReach.c b/src/aig/llb/llbReach.c
index 7c12a88c..76ee7147 100644
--- a/src/aig/llb/llbReach.c
+++ b/src/aig/llb/llbReach.c
@@ -575,7 +575,7 @@ int Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, DdManager ** pddGlo
Cudd_RecursiveDeref( p->dd, bConstrNs ); bConstrNs = NULL;
if ( bReached == NULL )
return 0; // reachable
- assert( bCurrent == NULL );
+// assert( bCurrent == NULL );
if ( bCurrent )
Cudd_RecursiveDeref( p->dd, bCurrent );
// report the stats
diff --git a/src/aig/mfx/mfxInt.h b/src/aig/mfx/mfxInt.h
index 1fcf4e91..320e7a8e 100644
--- a/src/aig/mfx/mfxInt.h
+++ b/src/aig/mfx/mfxInt.h
@@ -60,7 +60,8 @@ struct Mfx_Man_t_
Vec_Ptr_t * vNodes; // the internal nodes of the window
Vec_Ptr_t * vDivs; // the divisors of the node
Vec_Int_t * vDivLits; // the SAT literals of divisor nodes
- Vec_Int_t * vProjVars; // the projection variables
+ Vec_Int_t * vProjVarsCnf; // the projection variables
+ Vec_Int_t * vProjVarsSat; // the projection variables
// intermediate simulation data
Vec_Ptr_t * vDivCexes; // the counter-example for dividors
int nDivWords; // the number of words
diff --git a/src/aig/mfx/mfxInter.c b/src/aig/mfx/mfxInter.c
index 2263398d..db2e5e7e 100644
--- a/src/aig/mfx/mfxInter.c
+++ b/src/aig/mfx/mfxInter.c
@@ -96,13 +96,13 @@ sat_solver * Mfx_CreateSolverResub( Mfx_Man_t * p, int * pCands, int nCands, int
Lits[0] = toLitCond( p->pCnf->pVarNums[pObjPo->Id], fInvert );
// collect the outputs of the divisors
- Vec_IntClear( p->vProjVars );
+ Vec_IntClear( p->vProjVarsCnf );
Vec_PtrForEachEntryStart( Aig_Obj_t *, p->pAigWin->vPos, pObjPo, i, Aig_ManPoNum(p->pAigWin) - Vec_PtrSize(p->vDivs) )
{
assert( p->pCnf->pVarNums[pObjPo->Id] >= 0 );
- Vec_IntPush( p->vProjVars, p->pCnf->pVarNums[pObjPo->Id] );
+ Vec_IntPush( p->vProjVarsCnf, p->pCnf->pVarNums[pObjPo->Id] );
}
- assert( Vec_IntSize(p->vProjVars) == Vec_PtrSize(p->vDivs) );
+ assert( Vec_IntSize(p->vProjVarsCnf) == Vec_PtrSize(p->vDivs) );
// start the solver
pSat = sat_solver_new();
@@ -161,7 +161,7 @@ sat_solver * Mfx_CreateSolverResub( Mfx_Man_t * p, int * pCands, int nCands, int
// get the variable number of this divisor
i = lit_var( pCands[c] ) - 2 * p->pCnf->nVars;
// get the corresponding SAT variable
- iVar = Vec_IntEntry( p->vProjVars, i );
+ iVar = Vec_IntEntry( p->vProjVarsCnf, i );
// add the corresponding EXOR gate
if ( !Mfx_SatAddXor( pSat, iVar, iVar + p->pCnf->nVars, 2 * p->pCnf->nVars + i ) )
{
@@ -181,15 +181,17 @@ sat_solver * Mfx_CreateSolverResub( Mfx_Man_t * p, int * pCands, int nCands, int
else
{
// add the clauses for the EXOR gates - and remember their outputs
- Vec_IntForEachEntry( p->vProjVars, iVar, i )
+ Vec_IntClear( p->vProjVarsSat );
+ Vec_IntForEachEntry( p->vProjVarsCnf, iVar, i )
{
if ( !Mfx_SatAddXor( pSat, iVar, iVar + p->pCnf->nVars, 2 * p->pCnf->nVars + i ) )
{
sat_solver_delete( pSat );
return NULL;
}
- Vec_IntWriteEntry( p->vProjVars, i, 2 * p->pCnf->nVars + i );
+ Vec_IntPush( p->vProjVarsSat, 2 * p->pCnf->nVars + i );
}
+ assert( Vec_IntSize(p->vProjVarsCnf) == Vec_IntSize(p->vProjVarsSat) );
// simplify the solver
status = sat_solver_simplify(pSat);
if ( status == 0 )
@@ -242,7 +244,7 @@ unsigned * Mfx_InterplateTruth( Mfx_Man_t * p, int * pCands, int nCands, int fIn
// get the variable number of this divisor
i = lit_var( pCands[c] ) - 2 * p->pCnf->nVars;
// get the corresponding SAT variable
- pGloVars[c] = Vec_IntEntry( p->vProjVars, i );
+ pGloVars[c] = Vec_IntEntry( p->vProjVarsCnf, i );
}
// derive the interpolant
@@ -342,7 +344,7 @@ Hop_Obj_t * Mfx_Interplate( Mfx_Man_t * p, int * pCands, int nCands )
// get the variable number of this divisor
i = lit_var( pCands[c] ) - 2 * p->pCnf->nVars;
// get the corresponding SAT variable
- pGloVars[c] = Vec_IntEntry( p->vProjVars, i );
+ pGloVars[c] = Vec_IntEntry( p->vProjVarsCnf, i );
}
// derive the interpolant
diff --git a/src/aig/mfx/mfxMan.c b/src/aig/mfx/mfxMan.c
index 9d9994bf..ff8b02fd 100644
--- a/src/aig/mfx/mfxMan.c
+++ b/src/aig/mfx/mfxMan.c
@@ -49,7 +49,8 @@ Mfx_Man_t * Mfx_ManAlloc( Mfx_Par_t * pPars )
p = ABC_ALLOC( Mfx_Man_t, 1 );
memset( p, 0, sizeof(Mfx_Man_t) );
p->pPars = pPars;
- p->vProjVars = Vec_IntAlloc( 100 );
+ p->vProjVarsCnf = Vec_IntAlloc( 100 );
+ p->vProjVarsSat = Vec_IntAlloc( 100 );
p->vDivLits = Vec_IntAlloc( 100 );
p->nDivWords = Aig_BitWordNum(p->pPars->nDivMax + MFX_FANIN_MAX);
p->vDivCexes = Vec_PtrAllocSimInfo( p->pPars->nDivMax+MFX_FANIN_MAX+1, p->nDivWords );
@@ -178,7 +179,8 @@ void Mfx_ManStop( Mfx_Man_t * p )
Vec_IntFree( p->vMem );
Vec_VecFree( p->vLevels );
Vec_PtrFree( p->vFanins );
- Vec_IntFree( p->vProjVars );
+ Vec_IntFree( p->vProjVarsCnf );
+ Vec_IntFree( p->vProjVarsSat );
Vec_IntFree( p->vDivLits );
Vec_PtrFree( p->vDivCexes );
ABC_FREE( p );
diff --git a/src/aig/mfx/mfxResub.c b/src/aig/mfx/mfxResub.c
index 83673661..5a4786d6 100644
--- a/src/aig/mfx/mfxResub.c
+++ b/src/aig/mfx/mfxResub.c
@@ -111,7 +111,7 @@ int Mfx_TryResubOnce( Mfx_Man_t * p, int * pCands, int nCands )
}
p->nSatCexes++;
// store the counter-example
- Vec_IntForEachEntry( p->vProjVars, iVar, i )
+ Vec_IntForEachEntry( p->vProjVarsSat, iVar, i )
{
pData = (unsigned *)Vec_PtrEntry( p->vDivCexes, i );
if ( !sat_solver_var_value( p->pSat, iVar ) ) // remove 0s!!!
@@ -166,7 +166,7 @@ int Mfx_SolveSatResub( Mfx_Man_t * p, Nwk_Obj_t * pNode, int iFanin, int fOnlyRe
continue;
Vec_PtrPush( p->vFanins, pFanin );
iVar = Vec_PtrSize(p->vDivs) - Nwk_ObjFaninNum(pNode) + i;
- pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVars, iVar ), 1 );
+ pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVarsSat, iVar ), 1 );
}
RetValue = Mfx_TryResubOnce( p, pCands, nCands );
if ( RetValue == -1 )
@@ -244,7 +244,7 @@ p->timeInt += clock() - clk;
if ( iVar == Vec_PtrSize(p->vDivs)-Nwk_ObjFaninNum(pNode) )
return 0;
- pCands[nCands] = toLitCond( Vec_IntEntry(p->vProjVars, iVar), 1 );
+ pCands[nCands] = toLitCond( Vec_IntEntry(p->vProjVarsSat, iVar), 1 );
RetValue = Mfx_TryResubOnce( p, pCands, nCands+1 );
if ( RetValue == -1 )
return 0;
@@ -316,7 +316,7 @@ int Mfx_SolveSatResub2( Mfx_Man_t * p, Nwk_Obj_t * pNode, int iFanin, int iFanin
continue;
Vec_PtrPush( p->vFanins, pFanin );
iVar = Vec_PtrSize(p->vDivs) - Nwk_ObjFaninNum(pNode) + i;
- pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVars, iVar ), 1 );
+ pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVarsSat, iVar ), 1 );
}
RetValue = Mfx_TryResubOnce( p, pCands, nCands );
if ( RetValue == -1 )
@@ -390,8 +390,8 @@ p->timeInt += clock() - clk;
if ( iVar == Vec_PtrSize(p->vDivs)-Nwk_ObjFaninNum(pNode) )
return 0;
- pCands[nCands] = toLitCond( Vec_IntEntry(p->vProjVars, iVar2), 1 );
- pCands[nCands+1] = toLitCond( Vec_IntEntry(p->vProjVars, iVar), 1 );
+ pCands[nCands] = toLitCond( Vec_IntEntry(p->vProjVarsSat, iVar2), 1 );
+ pCands[nCands+1] = toLitCond( Vec_IntEntry(p->vProjVarsSat, iVar), 1 );
RetValue = Mfx_TryResubOnce( p, pCands, nCands+2 );
if ( RetValue == -1 )
return 0;
diff --git a/src/aig/mfx/mfxSat.c b/src/aig/mfx/mfxSat.c
index dc4cd862..974563ab 100644
--- a/src/aig/mfx/mfxSat.c
+++ b/src/aig/mfx/mfxSat.c
@@ -58,7 +58,7 @@ int Mfx_SolveSat_iter( Mfx_Man_t * p )
p->nCares++;
// add SAT assignment to the solver
Mint = 0;
- Vec_IntForEachEntry( p->vProjVars, iVar, b )
+ Vec_IntForEachEntry( p->vProjVarsSat, iVar, b )
{
Lits[b] = toLit( iVar );
if ( sat_solver_var_value( p->pSat, iVar ) )
@@ -70,7 +70,7 @@ int Mfx_SolveSat_iter( Mfx_Man_t * p )
assert( !Aig_InfoHasBit(p->uCare, Mint) );
Aig_InfoSetBit( p->uCare, Mint );
// add the blocking clause
- RetValue = sat_solver_addclause( p->pSat, Lits, Lits + Vec_IntSize(p->vProjVars) );
+ RetValue = sat_solver_addclause( p->pSat, Lits, Lits + Vec_IntSize(p->vProjVarsSat) );
if ( RetValue == 0 )
return 0;
return 1;
@@ -92,15 +92,15 @@ int Mfx_SolveSat( Mfx_Man_t * p, Nwk_Obj_t * pNode )
Aig_Obj_t * pObjPo;
int RetValue, i;
// collect projection variables
- Vec_IntClear( p->vProjVars );
+ Vec_IntClear( p->vProjVarsSat );
Vec_PtrForEachEntryStart( Aig_Obj_t *, p->pAigWin->vPos, pObjPo, i, Aig_ManPoNum(p->pAigWin) - Nwk_ObjFaninNum(pNode) )
{
assert( p->pCnf->pVarNums[pObjPo->Id] >= 0 );
- Vec_IntPush( p->vProjVars, p->pCnf->pVarNums[pObjPo->Id] );
+ Vec_IntPush( p->vProjVarsSat, p->pCnf->pVarNums[pObjPo->Id] );
}
// prepare the truth table of care set
- p->nFanins = Vec_IntSize( p->vProjVars );
+ p->nFanins = Vec_IntSize( p->vProjVarsSat );
p->nWords = Aig_TruthWordNum( p->nFanins );
memset( p->uCare, 0, sizeof(unsigned) * p->nWords );
diff --git a/src/aig/saig/module.make b/src/aig/saig/module.make
index 88935121..a1f0e976 100644
--- a/src/aig/saig/module.make
+++ b/src/aig/saig/module.make
@@ -24,5 +24,6 @@ SRC += src/aig/saig/saigAbs.c \
src/aig/saig/saigStrSim.c \
src/aig/saig/saigSwitch.c \
src/aig/saig/saigSynch.c \
+ src/aig/saig/saigTempor.c \
src/aig/saig/saigTrans.c \
src/aig/saig/saigWnd.c
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index fc85d52a..b1017bdb 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -146,7 +146,8 @@ extern void Saig_ManDetectConstrFuncTest( Aig_Man_t * p, int nFrame
extern Aig_Man_t * Saig_ManDupFoldConstrsFunc( Aig_Man_t * pAig, int fCompl, int fVerbose );
extern Aig_Man_t * Saig_ManDupUnfoldConstrsFunc( Aig_Man_t * pAig, int nFrames, int nConfs, int nProps, int fOldAlgo, int fVerbose );
/*=== saigDup.c ==========================================================*/
-extern Aig_Man_t * Said_ManDupOrpos( Aig_Man_t * p );
+extern Aig_Man_t * Saig_ManDupOrpos( Aig_Man_t * p );
+extern Aig_Man_t * Saig_ManCreateEquivMiter( Aig_Man_t * pAig, Vec_Int_t * vPairs );
extern Aig_Man_t * Saig_ManDeriveAbstraction( Aig_Man_t * pAig, Vec_Int_t * vFlops );
/*=== saigHaig.c ==========================================================*/
extern Aig_Man_t * Saig_ManHaigRecord( Aig_Man_t * p, int nIters, int nSteps, int fRetimingOnly, int fAddBugs, int fUseCnf, int fVerbose );
diff --git a/src/aig/saig/saigBmc2.c b/src/aig/saig/saigBmc2.c
index c7129c67..3d57ae6e 100644
--- a/src/aig/saig/saigBmc2.c
+++ b/src/aig/saig/saigBmc2.c
@@ -820,7 +820,12 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax
{
printf( "No output was asserted in %d frames. ", p->iFramePrev-1 );
if ( piFrames )
- *piFrames = p->iFramePrev-1;
+ {
+ if ( p->iOutputLast > 0 )
+ *piFrames = p->iFramePrev - 1;
+ else
+ *piFrames = p->iFramePrev;
+ }
}
if ( fVerbOverwrite )
{
@@ -834,7 +839,7 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax
{
if ( p->iFrameLast >= p->nFramesMax )
printf( "Reached limit on the number of timeframes (%d).\n", p->nFramesMax );
- else if ( p->pSat->stats.conflicts > p->nConfMaxAll )
+ else if ( p->nConfMaxAll && p->pSat->stats.conflicts > p->nConfMaxAll )
printf( "Reached global conflict limit (%d).\n", p->nConfMaxAll );
else
printf( "Reached local conflict limit (%d).\n", p->nConfMaxOne );
diff --git a/src/aig/saig/saigDup.c b/src/aig/saig/saigDup.c
index 268540da..4d34224e 100644
--- a/src/aig/saig/saigDup.c
+++ b/src/aig/saig/saigDup.c
@@ -42,7 +42,7 @@ ABC_NAMESPACE_IMPL_START
SeeAlso []
***********************************************************************/
-Aig_Man_t * Said_ManDupOrpos( Aig_Man_t * pAig )
+Aig_Man_t * Saig_ManDupOrpos( Aig_Man_t * pAig )
{
Aig_Man_t * pAigNew;
Aig_Obj_t * pObj, * pMiter;
@@ -77,6 +77,56 @@ Aig_Man_t * Said_ManDupOrpos( Aig_Man_t * pAig )
return pAigNew;
}
+/**Function*************************************************************
+
+ Synopsis [Duplicates while ORing the POs of sequential circuit.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManCreateEquivMiter( Aig_Man_t * pAig, Vec_Int_t * vPairs )
+{
+ Aig_Man_t * pAigNew;
+ Aig_Obj_t * pObj, * pObj2, * pMiter;
+ int i;
+ if ( pAig->nConstrs > 0 )
+ {
+ printf( "The AIG manager should have no constraints.\n" );
+ return NULL;
+ }
+ // start the new manager
+ pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
+ pAigNew->pName = Aig_UtilStrsav( pAig->pName );
+ pAigNew->nConstrs = pAig->nConstrs;
+ // map the constant node
+ Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
+ // create variables for PIs
+ Aig_ManForEachPi( pAig, pObj, i )
+ pObj->pData = Aig_ObjCreatePi( pAigNew );
+ // add internal nodes of this frame
+ Aig_ManForEachNode( pAig, pObj, i )
+ pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+ // create POs
+ assert( Vec_IntSize(vPairs) % 2 == 0 );
+ Aig_ManForEachNodeVec( pAig, vPairs, pObj, i )
+ {
+ pObj2 = Aig_ManObj( pAig, Vec_IntEntry(vPairs, ++i) );
+ pMiter = Aig_Exor( pAigNew, pObj->pData, pObj2->pData );
+ pMiter = Aig_NotCond( pMiter, pObj->fPhase ^ pObj2->fPhase );
+ Aig_ObjCreatePo( pAigNew, pMiter );
+ }
+ // transfer to register outputs
+ Saig_ManForEachLi( pAig, pObj, i )
+ Aig_ObjCreatePo( pAigNew, Aig_ObjChild0Copy(pObj) );
+ Aig_ManCleanup( pAigNew );
+ Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig) );
+ return pAigNew;
+}
+
/**Function*************************************************************
Synopsis [Duplicates the AIG manager recursively.]
diff --git a/src/aig/saig/saigPhase.c b/src/aig/saig/saigPhase.c
index 340910d0..4a23ecf3 100644
--- a/src/aig/saig/saigPhase.c
+++ b/src/aig/saig/saigPhase.c
@@ -255,15 +255,22 @@ int Saig_TsiCountNonXValuedRegisters( Saig_Tsim_t * p, int nWords, int nPref )
SeeAlso []
***********************************************************************/
-void Saig_TsiPrintTraces( Saig_Tsim_t * p, int nWords, int nPrefix )
+void Saig_TsiPrintTraces( Saig_Tsim_t * p, int nWords, int nPrefix, int nLoop )
{
unsigned * pState;
int nRegs = p->pAig->nRegs;
int Value, i, k, Counter = 0;
- if ( Vec_PtrSize(p->vStates) > 80 )
- return;
+ printf( "Ternary traces for each flop:\n" );
+ printf( " : " );
+ for ( i = 0; i < Vec_PtrSize(p->vStates) - nLoop - 1; i++ )
+ printf( "%d", i%10 );
+ printf( " " );
+ for ( i = 0; i < nLoop; i++ )
+ printf( "%d", i%10 );
+ printf( "\n" );
for ( i = 0; i < nRegs; i++ )
{
+/*
Vec_PtrForEachEntry( unsigned *, p->vStates, pState, k )
{
Value = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i );
@@ -274,8 +281,11 @@ void Saig_TsiPrintTraces( Saig_Tsim_t * p, int nWords, int nPrefix )
Counter++;
else
continue;
+*/
+
// print trace
- printf( "%5d : %5d %5d ", Counter, i, Saig_ManLo(p->pAig, i)->Id );
+// printf( "%5d : %5d %5d ", Counter, i, Saig_ManLo(p->pAig, i)->Id );
+ printf( "%5d : ", Counter++ );
Vec_PtrForEachEntryStop( unsigned *, p->vStates, pState, k, Vec_PtrSize(p->vStates)-1 )
{
Value = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i );
@@ -488,7 +498,7 @@ Saig_Tsim_t * Saig_ManReachableTernary( Aig_Man_t * p, Vec_Int_t * vInits, int f
Saig_ManForEachLo( p, pObj, i )
Saig_ObjSetXsim( pObj, Saig_XsimConvertValue(Vec_IntEntry(vInits, i)) );
}
- else
+ else
{
Saig_ManForEachLo( p, pObj, i )
Saig_ObjSetXsim( pObj, SAIG_XVS0 );
@@ -800,6 +810,42 @@ int Saig_ManPhaseFrameNum( Aig_Man_t * p, Vec_Int_t * vInits )
return nFrames;
}
+/**Function*************************************************************
+
+ Synopsis [Performs automated phase abstraction.]
+
+ Description [Takes the AIG manager and the array of initial states.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Saig_ManPhasePrefixLength( Aig_Man_t * p, int fVerbose, int fVeryVerbose )
+{
+ Saig_Tsim_t * pTsi;
+ int nFrames, nPrefix, nNonXRegs;
+ assert( Saig_ManRegNum(p) );
+ assert( Saig_ManPiNum(p) );
+ assert( Saig_ManPoNum(p) );
+ // perform terminary simulation
+ pTsi = Saig_ManReachableTernary( p, NULL, 0 );
+ if ( pTsi == NULL )
+ return 0;
+ // derive information
+ nPrefix = Saig_TsiComputePrefix( pTsi, (unsigned *)Vec_PtrEntryLast(pTsi->vStates), pTsi->nWords );
+ nFrames = Vec_PtrSize(pTsi->vStates) - 1 - nPrefix;
+ nNonXRegs = Saig_TsiCountNonXValuedRegisters( pTsi, pTsi->nWords, nPrefix );
+ // print statistics
+ if ( fVerbose )
+ printf( "Lead = %5d. Loop = %5d. Total flops = %5d. Binary flops = %5d.\n", nPrefix, nFrames, p->nRegs, nNonXRegs );
+ if ( fVeryVerbose )
+ Saig_TsiPrintTraces( pTsi, pTsi->nWords, nPrefix, nFrames );
+ Saig_TsiStop( pTsi );
+ // potentially, may need to reduce nFrames if nPrefix is less than nFrames
+ return nPrefix;
+}
+
/**Function*************************************************************
Synopsis [Performs automated phase abstraction.]
@@ -829,10 +875,10 @@ Aig_Man_t * Saig_ManPhaseAbstract( Aig_Man_t * p, Vec_Int_t * vInits, int nFrame
// print statistics
if ( fVerbose )
{
- printf( "Prefix = %5d. Cycle = %5d. Total = %5d. Non-ternary = %5d.\n",
+ printf( "Lead = %5d. Loop = %5d. Total flops = %5d. Binary flops = %5d.\n",
pTsi->nPrefix, pTsi->nCycle, p->nRegs, pTsi->nNonXRegs );
- if ( pTsi->nNonXRegs < 100 )
- Saig_TsiPrintTraces( pTsi, pTsi->nWords, pTsi->nPrefix );
+ if ( pTsi->nNonXRegs < 100 && Vec_PtrSize(pTsi->vStates) < 80 )
+ Saig_TsiPrintTraces( pTsi, pTsi->nWords, pTsi->nPrefix, pTsi->nCycle );
}
if ( fPrint )
printf( "Print-out finished. Phase assignment is not performed.\n" );
@@ -885,10 +931,10 @@ Aig_Man_t * Saig_ManPhaseAbstractAuto( Aig_Man_t * p, int fVerbose )
// print statistics
if ( fVerbose )
{
- printf( "Prefix = %5d. Cycle = %5d. Total = %5d. Non-ternary = %5d.\n",
+ printf( "Lead = %5d. Loop = %5d. Total flops = %5d. Binary flops = %5d.\n",
pTsi->nPrefix, pTsi->nCycle, p->nRegs, pTsi->nNonXRegs );
- if ( pTsi->nNonXRegs < 100 )
- Saig_TsiPrintTraces( pTsi, pTsi->nWords, pTsi->nPrefix );
+ if ( pTsi->nNonXRegs < 100 && Vec_PtrSize(pTsi->vStates) < 80 )
+ Saig_TsiPrintTraces( pTsi, pTsi->nWords, pTsi->nPrefix, pTsi->nCycle );
}
nFrames = pTsi->nCycle;
if ( fPrint )
diff --git a/src/aig/ssw/ssw.h b/src/aig/ssw/ssw.h
index 207ebea9..bf8c918e 100644
--- a/src/aig/ssw/ssw.h
+++ b/src/aig/ssw/ssw.h
@@ -68,6 +68,7 @@ struct Ssw_Pars_t_
int fUseCSat; // new SAT solver using when fScorrGia is selected
int fVerbose; // verbose stats
int fFlopVerbose; // verbose printout of redundant flops
+ int fEquivDump; // enables dumping equivalences
// optimized latch correspondence
int fLatchCorrOpt; // perform register correspondence (optimized)
int nSatVarMax; // max number of SAT vars before recycling SAT solver (optimized latch corr only)
diff --git a/src/aig/ssw/sswConstr.c b/src/aig/ssw/sswConstr.c
index e233f133..6afdd270 100644
--- a/src/aig/ssw/sswConstr.c
+++ b/src/aig/ssw/sswConstr.c
@@ -83,8 +83,8 @@ Aig_Man_t * Ssw_FramesWithConstraints( Aig_Man_t * p, int nFrames )
}
// remove dangling nodes
Aig_ManCleanup( pFrames );
- return pFrames;
-}
+ return pFrames;
+}
/**Function*************************************************************
diff --git a/src/aig/ssw/sswCore.c b/src/aig/ssw/sswCore.c
index c277d76e..1419b889 100644
--- a/src/aig/ssw/sswCore.c
+++ b/src/aig/ssw/sswCore.c
@@ -64,6 +64,8 @@ void Ssw_ManSetDefaultParams( Ssw_Pars_t * p )
p->fDynamic = 0; // dynamic partitioning
p->fLocalSim = 0; // local simulation
p->fVerbose = 0; // verbose stats
+ p->fEquivDump = 0; // enables dumping equivalences
+
// latch correspondence
p->fLatchCorrOpt = 0; // performs optimized register correspondence
p->nSatVarMax = 1000; // the max number of SAT variables
diff --git a/src/aig/ssw/sswDyn.c b/src/aig/ssw/sswDyn.c
index 7e8edc66..7bdb2652 100644
--- a/src/aig/ssw/sswDyn.c
+++ b/src/aig/ssw/sswDyn.c
@@ -409,12 +409,12 @@ p->timeReduce += clock() - clk;
if ( p->pPars->fVerbose )
Bar_ProgressUpdate( pProgress, i, NULL );
if ( Saig_ObjIsLo(p->pAig, pObj) )
- p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0 );
+ p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0, NULL );
else if ( Aig_ObjIsNode(pObj) )
{
pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
Ssw_ObjSetFrame( p, pObj, f, pObjNew );
- p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0 );
+ p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0, NULL );
}
// check if it is time to recycle the solver
if ( p->pMSat->pSat == NULL ||
diff --git a/src/aig/ssw/sswInt.h b/src/aig/ssw/sswInt.h
index e3a9a341..ad868c6e 100644
--- a/src/aig/ssw/sswInt.h
+++ b/src/aig/ssw/sswInt.h
@@ -277,7 +277,7 @@ extern void Ssw_ManResimulateWord( Ssw_Man_t * p, Aig_Obj_t * pCand, Ai
/*=== sswSweep.c ===================================================*/
extern int Ssw_ManGetSatVarValue( Ssw_Man_t * p, Aig_Obj_t * pObj, int f );
extern void Ssw_SmlSavePatternAig( Ssw_Man_t * p, int f );
-extern int Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc );
+extern int Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc, Vec_Int_t * vPairs );
extern int Ssw_ManSweepBmc( Ssw_Man_t * p );
extern int Ssw_ManSweep( Ssw_Man_t * p );
/*=== sswUnique.c ===================================================*/
diff --git a/src/aig/ssw/sswSemi.c b/src/aig/ssw/sswSemi.c
index dfb2fb0f..2a28a29b 100644
--- a/src/aig/ssw/sswSemi.c
+++ b/src/aig/ssw/sswSemi.c
@@ -204,7 +204,7 @@ clk = clock();
{
pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
Ssw_ObjSetFrame( p, pObj, f, pObjNew );
- if ( Ssw_ManSweepNode( p, pObj, f, 1 ) )
+ if ( Ssw_ManSweepNode( p, pObj, f, 1, NULL ) )
{
Ssw_ManFilterBmcSavePattern( pBmc );
if ( fFirst == 0 )
diff --git a/src/aig/ssw/sswSim.c b/src/aig/ssw/sswSim.c
index 37bf5717..404302f2 100644
--- a/src/aig/ssw/sswSim.c
+++ b/src/aig/ssw/sswSim.c
@@ -302,6 +302,23 @@ int Ssw_SmlNodeIsZero( Ssw_Sml_t * p, Aig_Obj_t * pObj )
return 1;
}
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if simulation info is composed of all zeros.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ssw_SmlNodeIsZeroFrame( Ssw_Sml_t * p, Aig_Obj_t * pObj, int f )
+{
+ unsigned * pSims = Ssw_ObjSim(p, pObj->Id);
+ return pSims[f] == 0;
+}
+
/**Function*************************************************************
Synopsis [Counts the number of one's in the patten the object.]
@@ -1308,7 +1325,7 @@ int Ssw_SmlRunCounterExample( Aig_Man_t * pAig, Abc_Cex_t * p )
// run random simulation
Ssw_SmlSimulateOne( pSml );
// check if the given output has failed
- RetValue = !Ssw_SmlNodeIsZero( pSml, Aig_ManPo(pAig, p->iPo) );
+ RetValue = !Ssw_SmlNodeIsZeroFrame( pSml, Aig_ManPo(pAig, p->iPo), p->iFrame );
Ssw_SmlStop( pSml );
return RetValue;
}
@@ -1347,7 +1364,7 @@ int Ssw_SmlFindOutputCounterExample( Aig_Man_t * pAig, Abc_Cex_t * p )
// check if the given output has failed
iOut = -1;
Saig_ManForEachPo( pAig, pObj, k )
- if ( !Ssw_SmlNodeIsZero( pSml, Aig_ManPo(pAig, k) ) )
+ if ( !Ssw_SmlNodeIsZeroFrame( pSml, Aig_ManPo(pAig, k), p->iFrame ) )
{
iOut = k;
break;
@@ -1541,81 +1558,6 @@ Abc_Cex_t * Ssw_SmlDupCounterExample( Abc_Cex_t * p, int nRegsNew )
return pCex;
}
-/**Function*************************************************************
-
- Synopsis [Resimulates the counter-example.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Ssw_SmlWriteCounterExample( FILE * pFile, Aig_Man_t * pAig, Abc_Cex_t * p )
-{
- Ssw_Sml_t * pSml;
- Aig_Obj_t * pObj;
- int RetValue, i, k, iBit;
- unsigned * pSims;
- assert( Aig_ManRegNum(pAig) > 0 );
- assert( Aig_ManRegNum(pAig) < Aig_ManPiNum(pAig) );
- // start a new sequential simulator
- pSml = Ssw_SmlStart( pAig, 0, p->iFrame+1, 1 );
- // assign simulation info for the registers
- iBit = 0;
- Saig_ManForEachLo( pAig, pObj, i )
-// Ssw_SmlObjAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), 0 );
- Ssw_SmlObjAssignConst( pSml, pObj, 0, 0 );
- // assign simulation info for the primary inputs
- iBit = p->nRegs;
- for ( i = 0; i <= p->iFrame; i++ )
- Saig_ManForEachPi( pAig, pObj, k )
- Ssw_SmlObjAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), i );
- assert( iBit == p->nBits );
- // run random simulation
- Ssw_SmlSimulateOne( pSml );
- // check if the given output has failed
- RetValue = !Ssw_SmlNodeIsZero( pSml, Aig_ManPo(pAig, p->iPo) );
-
- // write the output file
- for ( i = 0; i <= p->iFrame; i++ )
- {
-/*
- Saig_ManForEachLo( pAig, pObj, k )
- {
- pSims = Ssw_ObjSim(pSml, pObj->Id);
- fprintf( pFile, "%d", (int)(pSims[i] != 0) );
- }
- fprintf( pFile, " " );
-*/
- Saig_ManForEachPi( pAig, pObj, k )
- {
- pSims = Ssw_ObjSim(pSml, pObj->Id);
- fprintf( pFile, "%d", (int)(pSims[i] != 0) );
- }
-/*
- fprintf( pFile, " " );
- Saig_ManForEachPo( pAig, pObj, k )
- {
- pSims = Ssw_ObjSim(pSml, pObj->Id);
- fprintf( pFile, "%d", (int)(pSims[i] != 0) );
- }
- fprintf( pFile, " " );
- Saig_ManForEachLi( pAig, pObj, k )
- {
- pSims = Ssw_ObjSim(pSml, pObj->Id);
- fprintf( pFile, "%d", (int)(pSims[i] != 0) );
- }
-*/
- fprintf( pFile, "\n" );
- }
-
- Ssw_SmlStop( pSml );
- return RetValue;
-}
-
-
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
diff --git a/src/aig/ssw/sswSweep.c b/src/aig/ssw/sswSweep.c
index 39fcd48e..40121e42 100644
--- a/src/aig/ssw/sswSweep.c
+++ b/src/aig/ssw/sswSweep.c
@@ -184,7 +184,7 @@ void Ssw_SmlAddPatternDyn( Ssw_Man_t * p )
SeeAlso []
***********************************************************************/
-int Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc )
+int Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc, Vec_Int_t * vPairs )
{
Aig_Obj_t * pObjRepr, * pObjFraig, * pObjFraig2, * pObjReprFraig;
int RetValue, clk;
@@ -221,6 +221,11 @@ p->timeMarkCones += clock() - clk;
Ssw_ObjSetFrame( p, pObj, f, pObjFraig2 );
return 0;
}
+ if ( vPairs )
+ {
+ Vec_IntPush( vPairs, pObjRepr->Id );
+ Vec_IntPush( vPairs, pObj->Id );
+ }
if ( RetValue == -1 ) // timed out
{
Ssw_ClassesRemoveNode( p->ppClasses, pObj );
@@ -287,7 +292,7 @@ clk = clock();
Bar_ProgressUpdate( pProgress, Aig_ManObjNumMax(p->pAig) * f + i, NULL );
pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
Ssw_ObjSetFrame( p, pObj, f, pObjNew );
- p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 1 );
+ p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 1, NULL );
}
// quit if this is the last timeframe
if ( f == p->pPars->nFramesK - 1 )
@@ -312,6 +317,39 @@ p->timeBmc += clock() - clk;
return p->fRefined;
}
+
+/**Function*************************************************************
+
+ Synopsis [Generates AIG with the following nodes put into seq miters.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ssw_ManDumpEquivMiter( Aig_Man_t * p, Vec_Int_t * vPairs, int Num )
+{
+ extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact );
+ FILE * pFile;
+ char pBuffer[16];
+ Aig_Man_t * pNew;
+ sprintf( pBuffer, "equiv%03d.aig", Num );
+ pFile = fopen( pBuffer, "w" );
+ if ( pFile == NULL )
+ {
+ printf( "Cannot open file %s for writing.\n", pBuffer );
+ return;
+ }
+ fclose( pFile );
+ pNew = Saig_ManCreateEquivMiter( p, vPairs );
+ Ioa_WriteAiger( pNew, pBuffer, 0, 0 );
+ Aig_ManStop( pNew );
+ printf( "AIG with %4d disproved equivs is dumped into file \"%s\".\n", Vec_IntSize(vPairs)/2, pBuffer );
+}
+
+
/**Function*************************************************************
Synopsis [Performs fraiging for the internal nodes.]
@@ -325,9 +363,11 @@ p->timeBmc += clock() - clk;
***********************************************************************/
int Ssw_ManSweep( Ssw_Man_t * p )
{
+ static int Counter;
Bar_Progress_t * pProgress = NULL;
Aig_Obj_t * pObj, * pObj2, * pObjNew;
int nConstrPairs, clk, i, f;
+ Vec_Int_t * vDisproved;
// perform speculative reduction
clk = clock();
@@ -362,17 +402,18 @@ p->timeReduce += clock() - clk;
Ssw_ClassesClearRefined( p->ppClasses );
if ( p->pPars->fVerbose )
pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) );
+ vDisproved = p->pPars->fEquivDump? Vec_IntAlloc(1000) : NULL;
Aig_ManForEachObj( p->pAig, pObj, i )
{
if ( p->pPars->fVerbose )
Bar_ProgressUpdate( pProgress, i, NULL );
if ( Saig_ObjIsLo(p->pAig, pObj) )
- p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0 );
+ p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0, vDisproved );
else if ( Aig_ObjIsNode(pObj) )
{
pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
Ssw_ObjSetFrame( p, pObj, f, pObjNew );
- p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0 );
+ p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0, vDisproved );
}
}
if ( p->pPars->fVerbose )
@@ -380,6 +421,9 @@ p->timeReduce += clock() - clk;
// cleanup
// Ssw_ClassesCheck( p->ppClasses );
+ if ( p->pPars->fEquivDump )
+ Ssw_ManDumpEquivMiter( p->pAig, vDisproved, Counter++ );
+ Vec_IntFreeP( &vDisproved );
return p->fRefined;
}
--
cgit v1.2.3