diff options
Diffstat (limited to 'src/aig/ssw')
-rw-r--r-- | src/aig/ssw/ssw.h | 2 | ||||
-rw-r--r-- | src/aig/ssw/sswClass.c | 174 | ||||
-rw-r--r-- | src/aig/ssw/sswCore.c | 8 | ||||
-rw-r--r-- | src/aig/ssw/sswMan.c | 2 | ||||
-rw-r--r-- | src/aig/ssw/sswSim.c | 64 |
5 files changed, 175 insertions, 75 deletions
diff --git a/src/aig/ssw/ssw.h b/src/aig/ssw/ssw.h index 4bb2356a..5d70812d 100644 --- a/src/aig/ssw/ssw.h +++ b/src/aig/ssw/ssw.h @@ -90,8 +90,6 @@ struct Ssw_Cex_t_ /// FUNCTION DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -/*=== sswAbs.c ==========================================================*/ -extern Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fVerbose ); /*=== sswBmc.c ==========================================================*/ extern int Ssw_BmcDynamic( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int fVerbose, int * piFrame ); /*=== sswCore.c ==========================================================*/ diff --git a/src/aig/ssw/sswClass.c b/src/aig/ssw/sswClass.c index 3dfee28b..771fd530 100644 --- a/src/aig/ssw/sswClass.c +++ b/src/aig/ssw/sswClass.c @@ -482,75 +482,34 @@ void Ssw_ClassesRemoveNode( Ssw_Cla_t * p, Aig_Obj_t * pObj ) /**Function************************************************************* - Synopsis [Creates initial simulation classes.] + Synopsis [Takes the set of const1 cands and rehashes them using sim info.] - Description [Assumes that simulation info is assigned.] + Description [] SideEffects [] SeeAlso [] ***********************************************************************/ -Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs, int fVerbose ) +int Ssw_ClassesPrepareRehash( Ssw_Cla_t * p, Vec_Ptr_t * vCands ) { -// int nFrames = 4; -// int nWords = 1; -// int nIters = 16; - -// int nFrames = 32; -// int nWords = 4; -// int nIters = 0; - - int nFrames = 4; - int nWords = 2; - int nIters = 16; - Ssw_Cla_t * p; - Ssw_Sml_t * pSml; + Aig_Man_t * pAig = p->pAig; Aig_Obj_t ** ppTable, ** ppNexts, ** ppClassNew; Aig_Obj_t * pObj, * pTemp, * pRepr; - int i, k, nTableSize, nNodes, iEntry, nEntries, nEntries2, RetValue; - int clk; - - // start the classes - p = Ssw_ClassesStart( pAig ); - - // perform sequential simulation -clk = clock(); - pSml = Ssw_SmlSimulateSeq( pAig, 0, nFrames, nWords ); -if ( fVerbose ) -{ - printf( "Allocated %.2f Mb for simulation information.\n", - 1.0*(sizeof(unsigned) * Aig_ManObjNumMax(pAig) * nFrames * nWords)/(1<<20) ); - printf( "Initial simulation of %d frames with %d words. ", nFrames, nWords ); - PRT( "Time", clock() - clk ); -} - - // set comparison procedures -clk = clock(); - Ssw_ClassesSetData( p, pSml, Ssw_SmlObjHashWord, Ssw_SmlObjIsConstWord, Ssw_SmlObjsAreEqualWord ); + int i, k, nTableSize, nNodes, iEntry, nEntries, nEntries2; // allocate the hash table hashing simulation info into nodes - nTableSize = Aig_PrimeCudd( Aig_ManObjNumMax(p->pAig)/4 ); + nTableSize = Aig_PrimeCudd( Vec_PtrSize(vCands)/2 ); ppTable = CALLOC( Aig_Obj_t *, nTableSize ); ppNexts = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) ); - // add all the nodes to the hash table + // sort through the candidates nEntries = 0; - Aig_ManForEachObj( p->pAig, pObj, i ) + p->nCands1 = 0; + Vec_PtrForEachEntry( vCands, pObj, i ) { - if ( fLatchCorr ) - { - if ( !Saig_ObjIsLo(p->pAig, pObj) ) - continue; - } - else - { - if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) ) - continue; - // skip the node with more that the given number of levels - if ( nMaxLevs && (int)pObj->Level > nMaxLevs ) - continue; - } + assert( p->pClassSizes[pObj->Id] == 0 ); + Aig_ObjSetRepr( p->pAig, pObj, NULL ); // check if the node belongs to the class of constant 1 if ( p->pFuncNodeIsConst( p->pManData, pObj ) ) { @@ -562,7 +521,9 @@ clk = clock(); iEntry = p->pFuncNodeHash( p->pManData, pObj ) % nTableSize; // add the node to the class if ( ppTable[iEntry] == NULL ) + { ppTable[iEntry] = pObj; + } else { // set the representative of this node @@ -581,24 +542,18 @@ clk = clock(); nEntries++; } } - - // allocate room for classes - p->pMemClasses = ALLOC( Aig_Obj_t *, nEntries + p->nCands1 ); - p->pMemClassesFree = p->pMemClasses + nEntries; // copy the entries into storage in the topological order nEntries2 = 0; - Aig_ManForEachObj( p->pAig, pObj, i ) + Vec_PtrForEachEntry( vCands, pObj, i ) { - if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) ) - continue; nNodes = p->pClassSizes[pObj->Id]; // skip the nodes that are not representatives of non-trivial classes if ( nNodes == 0 ) continue; assert( nNodes > 1 ); // add the nodes to the class in the topological order - ppClassNew = p->pMemClasses + nEntries2; + ppClassNew = p->pMemClassesFree + nEntries2; ppClassNew[0] = pObj; for ( pTemp = Ssw_ObjNext(ppNexts, pObj), k = 1; pTemp; pTemp = Ssw_ObjNext(ppNexts, pTemp), k++ ) @@ -611,12 +566,88 @@ clk = clock(); // increment the number of entries nEntries2 += nNodes; } + p->pMemClassesFree += nEntries2; assert( nEntries == nEntries2 ); free( ppTable ); free( ppNexts ); + // now it is time to refine the classes + return Ssw_ClassesRefine( p, 1 ); +} + +/**Function************************************************************* + + Synopsis [Creates initial simulation classes.] + + Description [Assumes that simulation info is assigned.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs, int fVerbose ) +{ +// int nFrames = 4; +// int nWords = 1; +// int nIters = 16; + +// int nFrames = 32; +// int nWords = 4; +// int nIters = 0; + + int nFrames = 4; + int nWords = 2; + int nIters = 16; + Ssw_Cla_t * p; + Ssw_Sml_t * pSml; + Vec_Ptr_t * vCands; + Aig_Obj_t * pObj; + int i, k, RetValue, clk; + + // start the classes + p = Ssw_ClassesStart( pAig ); + + // perform sequential simulation +clk = clock(); + pSml = Ssw_SmlSimulateSeq( pAig, 0, nFrames, nWords ); +if ( fVerbose ) +{ + printf( "Allocated %.2f Mb to store simulation information.\n", + 1.0*(sizeof(unsigned) * Aig_ManObjNumMax(pAig) * nFrames * nWords)/(1<<20) ); + printf( "Initial simulation of %d frames with %d words. ", nFrames, nWords ); + PRT( "Time", clock() - clk ); +} + + // set comparison procedures +clk = clock(); + Ssw_ClassesSetData( p, pSml, Ssw_SmlObjHashWord, Ssw_SmlObjIsConstWord, Ssw_SmlObjsAreEqualWord ); + + // collect nodes to be considered as candidates + vCands = Vec_PtrAlloc( 1000 ); + Aig_ManForEachObj( p->pAig, pObj, i ) + { + if ( fLatchCorr ) + { + if ( !Saig_ObjIsLo(p->pAig, pObj) ) + continue; + } + else + { + if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) ) + continue; + // skip the node with more that the given number of levels + if ( nMaxLevs && (int)pObj->Level > nMaxLevs ) + continue; + } + Vec_PtrPush( vCands, pObj ); + } + + // allocate room for classes + p->pMemClasses = ALLOC( Aig_Obj_t *, Vec_PtrSize(vCands) ); + p->pMemClassesFree = p->pMemClasses; // now it is time to refine the classes - Ssw_ClassesRefine( p, 1 ); + Ssw_ClassesPrepareRehash( p, vCands ); if ( fVerbose ) { printf( "Collecting candidate equivalence classes. " ); @@ -625,27 +656,30 @@ PRT( "Time", clock() - clk ); clk = clock(); // perform iterative refinement using simulation - k = 0; for ( i = 1; i < nIters; i++ ) { + // collect const1 candidates + Vec_PtrClear( vCands ); + Aig_ManForEachObj( p->pAig, pObj, k ) + if ( Ssw_ObjIsConst1Cand( p->pAig, pObj ) ) + Vec_PtrPush( vCands, pObj ); + assert( Vec_PtrSize(vCands) == p->nCands1 ); + // perform new round of simulation Ssw_SmlResimulateSeq( pSml ); - // simulate internal nodes - Ssw_SmlSimulateOne( pSml ); // check equivalence classes - RetValue = Ssw_ClassesRefineConst1( p, 1 ); - RetValue += Ssw_ClassesRefine( p, 1 ); - k++; + RetValue = Ssw_ClassesPrepareRehash( p, vCands ); if ( RetValue == 0 ) break; } - Ssw_ClassesCheck( p ); Ssw_SmlStop( pSml ); + Vec_PtrFree( vCands ); if ( fVerbose ) { printf( "Simulation of %d frames with %d words (%2d rounds). ", - nFrames, nWords, k ); + nFrames, nWords, i-1 ); PRT( "Time", clock() - clk ); } + Ssw_ClassesCheck( p ); // Ssw_ClassesPrint( p, 0 ); return p; } @@ -848,7 +882,7 @@ int Ssw_ClassesRefineOneClass( Ssw_Cla_t * p, Aig_Obj_t * pReprOld, int fRecursi { Aig_Obj_t ** pClassOld, ** pClassNew; Aig_Obj_t * pObj, * pReprNew; - int i; + int i; // split the class Vec_PtrClear( p->vClassOld ); diff --git a/src/aig/ssw/sswCore.c b/src/aig/ssw/sswCore.c index 6db8cc3a..68c00a0e 100644 --- a/src/aig/ssw/sswCore.c +++ b/src/aig/ssw/sswCore.c @@ -150,7 +150,7 @@ clk = clock(); RetValue = Ssw_ManSweepLatch( p ); if ( p->pPars->fVerbose ) { - printf( "%3d : C =%7d. Cl =%7d. Pr =%6d. Cex =%5d. Rcl = %3d. F = %3d. ", + printf( "%3d : C =%7d. Cl =%7d. Pr =%6d. Cex =%5d. R =%4d. F =%4d. ", nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses), p->nSatProof-nSatProof, p->nSatCallsSat-nSatCallsSat, p->nRecycles-nRecycles, p->nSatFailsReal-nSatFailsReal ); @@ -174,11 +174,13 @@ clk = clock(); else if ( p->pPars->fDynamic ) { printf( "Cex =%5d. ", p->nSatCallsSat-nSatCallsSat ); - printf( "R =%3d. ", p->nRecycles-nRecycles ); + printf( "R =%4d. ", p->nRecycles-nRecycles ); } - printf( "F =%3d. ", p->nSatFailsReal-nSatFailsReal ); + printf( "F =%5d. ", p->nSatFailsReal-nSatFailsReal ); PRT( "T", clock() - clk ); } +// if ( p->pPars->fDynamic && p->nSatCallsSat-nSatCallsSat < 100 ) +// p->pPars->nBTLimit = 10000; } nSatProof = p->nSatProof; nSatCallsSat = p->nSatCallsSat; diff --git a/src/aig/ssw/sswMan.c b/src/aig/ssw/sswMan.c index 91f6e713..913f7518 100644 --- a/src/aig/ssw/sswMan.c +++ b/src/aig/ssw/sswMan.c @@ -61,6 +61,8 @@ Ssw_Man_t * Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) // other p->vNewLos = Vec_PtrAlloc( 100 ); p->vNewPos = Vec_IntAlloc( 100 ); + +// p->pPars->fVerbose = 1; return p; } diff --git a/src/aig/ssw/sswSim.c b/src/aig/ssw/sswSim.c index ce6ca38c..836b75e3 100644 --- a/src/aig/ssw/sswSim.c +++ b/src/aig/ssw/sswSim.c @@ -187,6 +187,70 @@ int Ssw_SmlNodeNotEquWeight( Ssw_Sml_t * p, int Left, int Right ) /**Function************************************************************* + Synopsis [Checks implication.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_SmlCheckXorImplication( Ssw_Sml_t * p, Aig_Obj_t * pObjLi, Aig_Obj_t * pObjLo, Aig_Obj_t * pCand ) +{ + unsigned * pSimLi, * pSimLo, * pSimCand; + int k; + pSimCand = Ssw_ObjSim( p, Aig_Regular(pCand)->Id ); + pSimLi = Ssw_ObjSim( p, pObjLi->Id ); + pSimLo = Ssw_ObjSim( p, pObjLo->Id ); + if ( !Aig_IsComplement(pCand) ) + { + for ( k = p->nWordsPref; k < p->nWordsTotal; k++ ) + if ( pSimCand[k] & (pSimLi[k] ^ pSimLo[k]) ) + return 0; + } + else + { + for ( k = p->nWordsPref; k < p->nWordsTotal; k++ ) + if ( ~pSimCand[k] & (pSimLi[k] ^ pSimLo[k]) ) + return 0; + } + return 1; +} + +/**Function************************************************************* + + Synopsis [Counts the number of 1s in the implication.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_SmlCountXorImplication( Ssw_Sml_t * p, Aig_Obj_t * pObjLi, Aig_Obj_t * pObjLo, Aig_Obj_t * pCand ) +{ + unsigned * pSimLi, * pSimLo, * pSimCand; + int k, Counter = 0; + pSimCand = Ssw_ObjSim( p, Aig_Regular(pCand)->Id ); + pSimLi = Ssw_ObjSim( p, pObjLi->Id ); + pSimLo = Ssw_ObjSim( p, pObjLo->Id ); + if ( !Aig_IsComplement(pCand) ) + { + for ( k = p->nWordsPref; k < p->nWordsTotal; k++ ) + Counter += Aig_WordCountOnes(pSimCand[k] & ~(pSimLi[k] ^ pSimLo[k])); + } + else + { + for ( k = p->nWordsPref; k < p->nWordsTotal; k++ ) + Counter += Aig_WordCountOnes(~pSimCand[k] & ~(pSimLi[k] ^ pSimLo[k])); + } + return Counter; +} + +/**Function************************************************************* + Synopsis [Returns 1 if simulation info is composed of all zeros.] Description [] |