diff options
Diffstat (limited to 'src/aig')
33 files changed, 514 insertions, 133 deletions
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 ) @@ -468,14 +468,36 @@ Abc_Cex_t * Gia_ManGenerateCounter( Gia_Man_t * pAig, int iFrame, int iOut, int 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 [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ 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; @@ -79,6 +79,56 @@ Aig_Man_t * Said_ManDupOrpos( Aig_Man_t * pAig ) /**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.] Description [] 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 ); @@ -811,6 +821,42 @@ int Saig_ManPhaseFrameNum( Aig_Man_t * p, Vec_Int_t * vInits ) 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.] + + Description [Takes the AIG manager and the array of initial states.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ Aig_Man_t * Saig_ManPhaseAbstract( Aig_Man_t * p, Vec_Int_t * vInits, int nFrames, int nPref, int fIgnore, int fPrint, int fVerbose ) { Aig_Man_t * pNew = NULL; @@ -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 @@ -304,6 +304,23 @@ int Ssw_SmlNodeIsZero( Ssw_Sml_t * p, Aig_Obj_t * pObj ) /**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.] Description [] @@ -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; } |