abc70930: src/aig/fra/fraImp.c Source File

00001 
00021 #include "fra.h"
00022 
00026 
00030 
00042 static inline int Fra_SmlCountOnesOne( Fra_Sml_t * p, int Node )
00043 {
00044     unsigned * pSim;
00045     int k, Counter = 0;
00046     pSim = Fra_ObjSim( p, Node );
00047     for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
00048         Counter += Aig_WordCountOnes( pSim[k] );
00049     return Counter;
00050 }
00051 
00063 static inline int * Fra_SmlCountOnes( Fra_Sml_t * p )
00064 {
00065     Aig_Obj_t * pObj;
00066     int i, * pnBits; 
00067     pnBits = ALLOC( int, Aig_ManObjNumMax(p->pAig) );  
00068     memset( pnBits, 0, sizeof(int) * Aig_ManObjNumMax(p->pAig) );
00069     Aig_ManForEachObj( p->pAig, pObj, i )
00070         pnBits[i] = Fra_SmlCountOnesOne( p, i );
00071     return pnBits;
00072 }
00073 
00085 static inline int Sml_NodeCheckImp( Fra_Sml_t * p, int Left, int Right )
00086 {
00087     unsigned * pSimL, * pSimR;
00088     int k;
00089     pSimL = Fra_ObjSim( p, Left );
00090     pSimR = Fra_ObjSim( p, Right );
00091     for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
00092         if ( pSimL[k] & ~pSimR[k] )
00093             return 0;
00094     return 1;
00095 }
00096 
00108 static inline int Sml_NodeNotImpWeight( Fra_Sml_t * p, int Left, int Right )
00109 {
00110     unsigned * pSimL, * pSimR;
00111     int k, Counter = 0;
00112     pSimL = Fra_ObjSim( p, Left );
00113     pSimR = Fra_ObjSim( p, Right );
00114     for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
00115         Counter += Aig_WordCountOnes( pSimL[k] & ~pSimR[k] );
00116     return Counter;
00117 }
00118 
00130 static inline void Sml_NodeSaveNotImpPatterns( Fra_Sml_t * p, int Left, int Right, unsigned * pResult )
00131 {
00132     unsigned * pSimL, * pSimR;
00133     int k;
00134     pSimL = Fra_ObjSim( p, Left );
00135     pSimR = Fra_ObjSim( p, Right );
00136     for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
00137         pResult[k] |= pSimL[k] & ~pSimR[k];
00138 }
00139 
00151 Vec_Ptr_t * Fra_SmlSortUsingOnes( Fra_Sml_t * p, int fLatchCorr )
00152 {
00153     Aig_Obj_t * pObj;
00154     Vec_Ptr_t * vNodes;
00155     int i, nNodes, nTotal, nBits, * pnNodes, * pnBits, * pMemory;
00156     assert( p->nWordsTotal > 0 );
00157     // count 1s in each node's siminfo
00158     pnBits = Fra_SmlCountOnes( p );
00159     // count number of nodes having that many 1s
00160     nNodes = 0;
00161     nBits = p->nWordsTotal * 32;
00162     pnNodes = ALLOC( int, nBits + 1 );
00163     memset( pnNodes, 0, sizeof(int) * (nBits + 1) );
00164     Aig_ManForEachObj( p->pAig, pObj, i )
00165     {
00166         if ( i == 0 ) continue;
00167         // skip non-PI and non-internal nodes
00168         if ( fLatchCorr )
00169         {
00170             if ( !Aig_ObjIsPi(pObj) )
00171                 continue;
00172         }
00173         else
00174         {
00175             if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
00176                 continue;
00177         }
00178         // skip nodes participating in the classes
00179 //        if ( Fra_ClassObjRepr(pObj) )
00180 //            continue;
00181         assert( pnBits[i] <= nBits ); // "<" because of normalized info
00182         pnNodes[pnBits[i]]++;
00183         nNodes++;
00184     }
00185     // allocate memory for all the nodes
00186     pMemory = ALLOC( int, nNodes + nBits + 1 );  
00187     // markup the memory for each node
00188     vNodes = Vec_PtrAlloc( nBits + 1 );
00189     Vec_PtrPush( vNodes, pMemory );
00190     for ( i = 1; i <= nBits; i++ )
00191     {
00192         pMemory += pnNodes[i-1] + 1;
00193         Vec_PtrPush( vNodes, pMemory );
00194     }
00195     // add the nodes
00196     memset( pnNodes, 0, sizeof(int) * (nBits + 1) );
00197     Aig_ManForEachObj( p->pAig, pObj, i )
00198     {
00199         if ( i == 0 ) continue;
00200         // skip non-PI and non-internal nodes
00201         if ( fLatchCorr )
00202         {
00203             if ( !Aig_ObjIsPi(pObj) )
00204                 continue;
00205         }
00206         else
00207         {
00208             if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
00209                 continue;
00210         }
00211         // skip nodes participating in the classes
00212 //        if ( Fra_ClassObjRepr(pObj) )
00213 //            continue;
00214         pMemory = Vec_PtrEntry( vNodes, pnBits[i] );
00215         pMemory[ pnNodes[pnBits[i]]++ ] = i;
00216     }
00217     // add 0s in the end
00218     nTotal = 0;
00219     Vec_PtrForEachEntry( vNodes, pMemory, i )
00220     {
00221         pMemory[ pnNodes[i]++ ] = 0;
00222         nTotal += pnNodes[i];
00223     }
00224     assert( nTotal == nNodes + nBits + 1 );
00225     free( pnNodes );
00226     free( pnBits );
00227     return vNodes;
00228 }
00229 
00241 Vec_Int_t * Fra_SmlSelectMaxCost( Vec_Int_t * vImps, int * pCosts, int nCostMax, int nImpLimit, int * pCostRange )
00242 {
00243     Vec_Int_t * vImpsNew;
00244     int * pCostCount, nImpCount, Imp, i, c;
00245     assert( Vec_IntSize(vImps) >= nImpLimit );
00246     // count how many implications have each cost
00247     pCostCount = ALLOC( int, nCostMax + 1 );
00248     memset( pCostCount, 0, sizeof(int) * (nCostMax + 1) );
00249     for ( i = 0; i < Vec_IntSize(vImps); i++ )
00250     {
00251         assert( pCosts[i] <= nCostMax );
00252         pCostCount[ pCosts[i] ]++;
00253     }
00254     assert( pCostCount[0] == 0 );
00255     // select the bound on the cost (above this bound, implication will be included)
00256     nImpCount = 0;
00257     for ( c = nCostMax; c > 0; c-- )
00258     {
00259         nImpCount += pCostCount[c];
00260         if ( nImpCount >= nImpLimit )
00261             break;
00262     }
00263 //    printf( "Cost range >= %d.\n", c );
00264     // collect implications with the given costs
00265     vImpsNew = Vec_IntAlloc( nImpLimit );
00266     Vec_IntForEachEntry( vImps, Imp, i )
00267     {
00268         if ( pCosts[i] < c )
00269             continue;
00270         Vec_IntPush( vImpsNew, Imp );
00271         if ( Vec_IntSize( vImpsNew ) == nImpLimit )
00272             break;
00273     }
00274     free( pCostCount );
00275     if ( pCostRange )
00276         *pCostRange = c;
00277     return vImpsNew;
00278 }
00279 
00291 int Sml_CompareMaxId( unsigned short * pImp1, unsigned short * pImp2 )
00292 {
00293     int Max1 = AIG_MAX( pImp1[0], pImp1[1] );
00294     int Max2 = AIG_MAX( pImp2[0], pImp2[1] );
00295     if ( Max1 < Max2 )
00296         return -1;
00297     if ( Max1 > Max2  )
00298         return 1;
00299     return 0; 
00300 }
00301 
00318 Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, int fLatchCorr )
00319 {
00320     int nSimWords = 64;
00321     Fra_Sml_t * pSeq, * pComb;
00322     Vec_Int_t * vImps, * vTemp;
00323     Vec_Ptr_t * vNodes;
00324     int * pImpCosts, * pNodesI, * pNodesK;
00325     int nImpsTotal = 0, nImpsTried = 0, nImpsNonSeq = 0, nImpsComb = 0, nImpsCollected = 0;
00326     int CostMin = AIG_INFINITY, CostMax = 0;
00327     int i, k, Imp, CostRange, clk = clock();
00328     assert( Aig_ManObjNumMax(p->pManAig) < (1 << 15) );
00329     assert( nImpMaxLimit > 0 && nImpUseLimit > 0 && nImpUseLimit <= nImpMaxLimit );
00330     // normalize both managers
00331     pComb = Fra_SmlSimulateComb( p->pManAig, nSimWords );
00332     pSeq = Fra_SmlSimulateSeq( p->pManAig, p->pPars->nFramesP, nSimWords, 1 );
00333     // get the nodes sorted by the number of 1s
00334     vNodes = Fra_SmlSortUsingOnes( pSeq, fLatchCorr );
00335     // count the total number of implications
00336     for ( k = nSimWords * 32; k > 0; k-- )
00337     for ( i = k - 1; i > 0; i-- )
00338     for ( pNodesI = Vec_PtrEntry( vNodes, i ); *pNodesI; pNodesI++ )
00339     for ( pNodesK = Vec_PtrEntry( vNodes, k ); *pNodesK; pNodesK++ )
00340         nImpsTotal++;
00341 
00342     // compute implications and their costs
00343     pImpCosts = ALLOC( int, nImpMaxLimit );
00344     vImps = Vec_IntAlloc( nImpMaxLimit );
00345     for ( k = pSeq->nWordsTotal * 32; k > 0; k-- )
00346         for ( i = k - 1; i > 0; i-- )
00347         {
00348             for ( pNodesI = Vec_PtrEntry( vNodes, i ); *pNodesI; pNodesI++ )
00349             for ( pNodesK = Vec_PtrEntry( vNodes, k ); *pNodesK; pNodesK++ )
00350             {
00351                 nImpsTried++;
00352                 if ( !Sml_NodeCheckImp(pSeq, *pNodesI, *pNodesK) )
00353                 {
00354                     nImpsNonSeq++;
00355                     continue;
00356                 }
00357                 if ( Sml_NodeCheckImp(pComb, *pNodesI, *pNodesK) )
00358                 {
00359                     nImpsComb++;
00360                     continue;
00361                 }
00362                 nImpsCollected++;
00363                 Imp = Fra_ImpCreate( *pNodesI, *pNodesK );
00364                 pImpCosts[ Vec_IntSize(vImps) ] = Sml_NodeNotImpWeight(pComb, *pNodesI, *pNodesK);
00365                 CostMin = AIG_MIN( CostMin, pImpCosts[ Vec_IntSize(vImps) ] );
00366                 CostMax = AIG_MAX( CostMax, pImpCosts[ Vec_IntSize(vImps) ] );
00367                 Vec_IntPush( vImps, Imp );
00368                 if ( Vec_IntSize(vImps) == nImpMaxLimit )
00369                     goto finish;
00370             } 
00371         }
00372 finish:
00373     Fra_SmlStop( pComb );
00374     Fra_SmlStop( pSeq );
00375 
00376     // select implications with the highest cost
00377     CostRange = CostMin;
00378     if ( Vec_IntSize(vImps) > nImpUseLimit )
00379     {
00380         vImps = Fra_SmlSelectMaxCost( vTemp = vImps, pImpCosts, nSimWords * 32, nImpUseLimit, &CostRange );
00381         Vec_IntFree( vTemp );  
00382     }
00383 
00384     // dealloc
00385     free( pImpCosts ); 
00386     free( Vec_PtrEntry(vNodes, 0) );
00387     Vec_PtrFree( vNodes );
00388     // reorder implications topologically
00389     qsort( (void *)Vec_IntArray(vImps), Vec_IntSize(vImps), sizeof(int), 
00390             (int (*)(const void *, const void *)) Sml_CompareMaxId );
00391 if ( p->pPars->fVerbose )
00392 {
00393 printf( "Implications: All = %d. Try = %d. NonSeq = %d. Comb = %d. Res = %d.\n", 
00394     nImpsTotal, nImpsTried, nImpsNonSeq, nImpsComb, nImpsCollected );
00395 printf( "Implication weight: Min = %d. Pivot = %d. Max = %d.   ", 
00396        CostMin, CostRange, CostMax );
00397 PRT( "Time", clock() - clk );
00398 }
00399     return vImps;
00400 }
00401 
00402 
00403 // the following three procedures are called to 
00404 // - add implications to the SAT solver
00405 // - check implications using the SAT solver
00406 // - refine implications using after a cex is generated
00407 
00419 void Fra_ImpAddToSolver( Fra_Man_t * p, Vec_Int_t * vImps, int * pSatVarNums )
00420 {
00421     sat_solver * pSat = p->pSat;
00422     Aig_Obj_t * pLeft, * pRight;
00423     Aig_Obj_t * pLeftF, * pRightF;
00424     int pLits[2], Imp, Left, Right, i, f, status;
00425     int fComplL, fComplR;
00426     Vec_IntForEachEntry( vImps, Imp, i )
00427     {
00428         // get the corresponding nodes
00429         pLeft = Aig_ManObj( p->pManAig, Fra_ImpLeft(Imp) );
00430         pRight = Aig_ManObj( p->pManAig, Fra_ImpRight(Imp) );
00431         // check if all the nodes are present
00432         for ( f = 0; f < p->pPars->nFramesK; f++ )
00433         {
00434             // map these info fraig
00435             pLeftF = Fra_ObjFraig( pLeft, f );
00436             pRightF = Fra_ObjFraig( pRight, f );
00437             if ( Aig_ObjIsNone(Aig_Regular(pLeftF)) || Aig_ObjIsNone(Aig_Regular(pRightF)) )
00438             {
00439                 Vec_IntWriteEntry( vImps, i, 0 );
00440                 break;
00441             }
00442         }
00443         if ( f < p->pPars->nFramesK )
00444             continue;
00445         // add constraints in each timeframe
00446         for ( f = 0; f < p->pPars->nFramesK; f++ )
00447         {
00448             // map these info fraig
00449             pLeftF = Fra_ObjFraig( pLeft, f );
00450             pRightF = Fra_ObjFraig( pRight, f );
00451             // get the corresponding SAT numbers
00452             Left = pSatVarNums[ Aig_Regular(pLeftF)->Id ];
00453             Right = pSatVarNums[ Aig_Regular(pRightF)->Id ];
00454             assert( Left > 0  && Left < p->nSatVars );
00455             assert( Right > 0 && Right < p->nSatVars );
00456             // get the complemented attributes
00457             fComplL = pLeft->fPhase ^ Aig_IsComplement(pLeftF);
00458             fComplR = pRight->fPhase ^ Aig_IsComplement(pRightF);
00459             // get the constraint
00460             // L => R      L' v R     (complement = L & R')
00461             pLits[0] = 2 * Left  + !fComplL;
00462             pLits[1] = 2 * Right +  fComplR;
00463             // add contraint to solver
00464             if ( !sat_solver_addclause( pSat, pLits, pLits + 2 ) )
00465             {
00466                 sat_solver_delete( pSat );
00467                 p->pSat = NULL;
00468                 return;
00469             }
00470         }
00471     }
00472     status = sat_solver_simplify(pSat);
00473     if ( status == 0 )
00474     {
00475         sat_solver_delete( pSat );
00476         p->pSat = NULL;
00477     }
00478 //    printf( "Total imps = %d. ", Vec_IntSize(vImps) );
00479     Fra_ImpCompactArray( vImps );
00480 //    printf( "Valid imps = %d. \n", Vec_IntSize(vImps) );
00481 }
00482 
00494 int Fra_ImpCheckForNode( Fra_Man_t * p, Vec_Int_t * vImps, Aig_Obj_t * pNode, int Pos )
00495 {
00496     Aig_Obj_t * pLeft, * pRight;
00497     Aig_Obj_t * pLeftF, * pRightF;
00498     int i, Imp, Left, Right, Max, RetValue;
00499     int fComplL, fComplR;
00500     Vec_IntForEachEntryStart( vImps, Imp, i, Pos )
00501     {
00502         if ( Imp == 0 )
00503             continue;
00504         Left = Fra_ImpLeft(Imp);
00505         Right = Fra_ImpRight(Imp);
00506         Max = AIG_MAX( Left, Right );
00507         assert( Max >= pNode->Id );
00508         if ( Max > pNode->Id )
00509             return i;
00510         // get the corresponding nodes
00511         pLeft  = Aig_ManObj( p->pManAig, Left );
00512         pRight = Aig_ManObj( p->pManAig, Right );
00513         // get the corresponding FRAIG nodes
00514         pLeftF  = Fra_ObjFraig( pLeft, p->pPars->nFramesK );
00515         pRightF = Fra_ObjFraig( pRight, p->pPars->nFramesK );
00516         // get the complemented attributes
00517         fComplL = pLeft->fPhase ^ Aig_IsComplement(pLeftF);
00518         fComplR = pRight->fPhase ^ Aig_IsComplement(pRightF);
00519         // check equality
00520         if ( Aig_Regular(pLeftF) == Aig_Regular(pRightF) )
00521         {
00522             if ( fComplL == fComplR ) // x => x  - always true
00523                 continue;
00524             assert( fComplL != fComplR );
00525             // consider 4 possibilities:
00526             // NOT(1) => 1    or   0 => 1  - always true
00527             // 1 => NOT(1)    or   1 => 0  - never true
00528             // NOT(x) => x    or   x       - not always true
00529             // x => NOT(x)    or   NOT(x)  - not always true
00530             if ( Aig_ObjIsConst1(Aig_Regular(pLeftF)) && fComplL ) // proved implication
00531                 continue;
00532             // disproved implication
00533             p->pCla->fRefinement = 1;
00534             Vec_IntWriteEntry( vImps, i, 0 );
00535             continue;
00536         }
00537         // check the implication 
00538         // - if true, a clause is added
00539         // - if false, a cex is simulated
00540         // make sure the implication is refined
00541         RetValue = Fra_NodesAreImp( p, Aig_Regular(pLeftF), Aig_Regular(pRightF), fComplL, fComplR );
00542         if ( RetValue != 1 )
00543         {
00544             p->pCla->fRefinement = 1;
00545             if ( RetValue == 0 )
00546                 Fra_SmlResimulate( p );
00547             if ( Vec_IntEntry(vImps, i) != 0 )
00548                 printf( "Fra_ImpCheckForNode(): Implication is not refined!\n" );
00549             assert( Vec_IntEntry(vImps, i) == 0 );
00550         }
00551     }
00552     return i;
00553 }
00554 
00566 int Fra_ImpRefineUsingCex( Fra_Man_t * p, Vec_Int_t * vImps )
00567 {
00568     Aig_Obj_t * pLeft, * pRight;
00569     int Imp, i, RetValue = 0;
00570     Vec_IntForEachEntry( vImps, Imp, i )
00571     {
00572         if ( Imp == 0 )
00573             continue;
00574         // get the corresponding nodes
00575         pLeft = Aig_ManObj( p->pManAig, Fra_ImpLeft(Imp) );
00576         pRight = Aig_ManObj( p->pManAig, Fra_ImpRight(Imp) );
00577         // check if implication holds using this simulation info
00578         if ( !Sml_NodeCheckImp(p->pSml, pLeft->Id, pRight->Id) )
00579         {
00580             Vec_IntWriteEntry( vImps, i, 0 );
00581             RetValue = 1;
00582         }
00583     }
00584     return RetValue;
00585 }
00586 
00598 void Fra_ImpCompactArray( Vec_Int_t * vImps )
00599 {
00600     int i, k, Imp;
00601     k = 0;
00602     Vec_IntForEachEntry( vImps, Imp, i )
00603         if ( Imp )
00604             Vec_IntWriteEntry( vImps, k++, Imp );
00605     Vec_IntShrink( vImps, k );
00606 }
00607 
00619 double Fra_ImpComputeStateSpaceRatio( Fra_Man_t * p )
00620 {
00621     int nSimWords = 64;
00622     Fra_Sml_t * pComb;
00623     unsigned * pResult;
00624     double Ratio = 0.0;
00625     int Left, Right, Imp, i;
00626     if ( p->pCla->vImps == NULL || Vec_IntSize(p->pCla->vImps) == 0 )
00627         return Ratio;
00628     // simulate the AIG manager with combinational patterns
00629     pComb = Fra_SmlSimulateComb( p->pManAig, nSimWords );
00630     // go through the implications and collect where they do not hold
00631     pResult = Fra_ObjSim( pComb, 0 );
00632     assert( pResult[0] == 0 );
00633     Vec_IntForEachEntry( p->pCla->vImps, Imp, i )
00634     {
00635         Left = Fra_ImpLeft(Imp);
00636         Right = Fra_ImpRight(Imp);
00637         Sml_NodeSaveNotImpPatterns( pComb, Left, Right, pResult );
00638     }
00639     // count the number of ones in this area
00640     Ratio = 100.0 * Fra_SmlCountOnesOne( pComb, 0 ) / (32*(pComb->nWordsTotal-pComb->nWordsPref));
00641     Fra_SmlStop( pComb );
00642     return Ratio;
00643 }
00644 
00656 int Fra_ImpVerifyUsingSimulation( Fra_Man_t * p )
00657 {
00658     int nFrames = 2000;
00659     int nSimWords = 8;
00660     Fra_Sml_t * pSeq;
00661     char * pfFails;
00662     int Left, Right, Imp, i, Counter;
00663     if ( p->pCla->vImps == NULL || Vec_IntSize(p->pCla->vImps) == 0 )
00664         return 0;
00665     // simulate the AIG manager with combinational patterns
00666     pSeq = Fra_SmlSimulateSeq( p->pManAig, p->pPars->nFramesP, nFrames, nSimWords );
00667     // go through the implications and check how many of them do not hold
00668     pfFails = ALLOC( char, Vec_IntSize(p->pCla->vImps) );
00669     memset( pfFails, 0, sizeof(char) * Vec_IntSize(p->pCla->vImps) );
00670     Vec_IntForEachEntry( p->pCla->vImps, Imp, i )
00671     {
00672         Left = Fra_ImpLeft(Imp);
00673         Right = Fra_ImpRight(Imp);
00674         pfFails[i] = !Sml_NodeCheckImp( pSeq, Left, Right );
00675     }
00676     // count how many has failed
00677     Counter = 0;
00678     for ( i = 0; i < Vec_IntSize(p->pCla->vImps); i++ )
00679         Counter += pfFails[i];
00680     free( pfFails );
00681     Fra_SmlStop( pSeq );
00682     return Counter;
00683 }
00684 
00696 void Fra_ImpRecordInManager( Fra_Man_t * p, Aig_Man_t * pNew )
00697 {
00698     Aig_Obj_t * pLeft, * pRight, * pMiter;
00699     int nPosOld, Imp, i;
00700     if ( p->pCla->vImps == NULL || Vec_IntSize(p->pCla->vImps) == 0 )
00701         return;
00702     // go through the implication
00703     nPosOld = Aig_ManPoNum(pNew);
00704     Vec_IntForEachEntry( p->pCla->vImps, Imp, i )
00705     {
00706         pLeft = Aig_ManObj( p->pManAig, Fra_ImpLeft(Imp) );
00707         pRight = Aig_ManObj( p->pManAig, Fra_ImpRight(Imp) );
00708         // record the implication: L' + R
00709         pMiter = Aig_Or( pNew, 
00710             Aig_NotCond(pLeft->pData, !pLeft->fPhase), 
00711             Aig_NotCond(pRight->pData, pRight->fPhase) ); 
00712         Aig_ObjCreatePo( pNew, pMiter );
00713     }
00714     pNew->nAsserts = Aig_ManPoNum(pNew) - nPosOld;
00715 }
00716 
00720 
00721