| /**CFile**************************************************************** |
| |
| FileName [fraImp.c] |
| |
| SystemName [ABC: Logic synthesis and verification system.] |
| |
| PackageName [New FRAIG package.] |
| |
| Synopsis [Detecting and proving implications.] |
| |
| Author [Alan Mishchenko] |
| |
| Affiliation [UC Berkeley] |
| |
| Date [Ver. 1.0. Started - June 30, 2007.] |
| |
| Revision [$Id: fraImp.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $] |
| |
| ***********************************************************************/ |
| |
| #include "fra.h" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// DECLARATIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// FUNCTION DEFINITIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| /**Function************************************************************* |
| |
| Synopsis [Counts the number of 1s in each siminfo of each node.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| static inline int Fra_SmlCountOnesOne( Fra_Sml_t * p, int Node ) |
| { |
| unsigned * pSim; |
| int k, Counter = 0; |
| pSim = Fra_ObjSim( p, Node ); |
| for ( k = p->nWordsPref; k < p->nWordsTotal; k++ ) |
| Counter += Aig_WordCountOnes( pSim[k] ); |
| return Counter; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Counts the number of 1s in each siminfo of each node.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| static inline int * Fra_SmlCountOnes( Fra_Sml_t * p ) |
| { |
| Aig_Obj_t * pObj; |
| int i, * pnBits; |
| pnBits = ABC_ALLOC( int, Aig_ManObjNumMax(p->pAig) ); |
| memset( pnBits, 0, sizeof(int) * Aig_ManObjNumMax(p->pAig) ); |
| Aig_ManForEachObj( p->pAig, pObj, i ) |
| pnBits[i] = Fra_SmlCountOnesOne( p, i ); |
| return pnBits; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Returns 1 if implications holds.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| static inline int Sml_NodeCheckImp( Fra_Sml_t * p, int Left, int Right ) |
| { |
| unsigned * pSimL, * pSimR; |
| int k; |
| pSimL = Fra_ObjSim( p, Left ); |
| pSimR = Fra_ObjSim( p, Right ); |
| for ( k = p->nWordsPref; k < p->nWordsTotal; k++ ) |
| if ( pSimL[k] & ~pSimR[k] ) |
| return 0; |
| return 1; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Counts the number of 1s in the complement of the implication.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| static inline int Sml_NodeNotImpWeight( Fra_Sml_t * p, int Left, int Right ) |
| { |
| unsigned * pSimL, * pSimR; |
| int k, Counter = 0; |
| pSimL = Fra_ObjSim( p, Left ); |
| pSimR = Fra_ObjSim( p, Right ); |
| for ( k = p->nWordsPref; k < p->nWordsTotal; k++ ) |
| Counter += Aig_WordCountOnes( pSimL[k] & ~pSimR[k] ); |
| return Counter; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Computes the complement of the implication.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| static inline void Sml_NodeSaveNotImpPatterns( Fra_Sml_t * p, int Left, int Right, unsigned * pResult ) |
| { |
| unsigned * pSimL, * pSimR; |
| int k; |
| pSimL = Fra_ObjSim( p, Left ); |
| pSimR = Fra_ObjSim( p, Right ); |
| for ( k = p->nWordsPref; k < p->nWordsTotal; k++ ) |
| pResult[k] |= pSimL[k] & ~pSimR[k]; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Returns the array of nodes sorted by the number of 1s.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Vec_Ptr_t * Fra_SmlSortUsingOnes( Fra_Sml_t * p, int fLatchCorr ) |
| { |
| Aig_Obj_t * pObj; |
| Vec_Ptr_t * vNodes; |
| int i, nNodes, nTotal, nBits, * pnNodes, * pnBits, * pMemory; |
| assert( p->nWordsTotal > 0 ); |
| // count 1s in each node's siminfo |
| pnBits = Fra_SmlCountOnes( p ); |
| // count number of nodes having that many 1s |
| nNodes = 0; |
| nBits = p->nWordsTotal * 32; |
| pnNodes = ABC_ALLOC( int, nBits + 1 ); |
| memset( pnNodes, 0, sizeof(int) * (nBits + 1) ); |
| Aig_ManForEachObj( p->pAig, pObj, i ) |
| { |
| if ( i == 0 ) continue; |
| // skip non-PI and non-internal nodes |
| if ( fLatchCorr ) |
| { |
| if ( !Aig_ObjIsCi(pObj) ) |
| continue; |
| } |
| else |
| { |
| if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) ) |
| continue; |
| } |
| // skip nodes participating in the classes |
| // if ( Fra_ClassObjRepr(pObj) ) |
| // continue; |
| assert( pnBits[i] <= nBits ); // "<" because of normalized info |
| pnNodes[pnBits[i]]++; |
| nNodes++; |
| } |
| // allocate memory for all the nodes |
| pMemory = ABC_ALLOC( int, nNodes + nBits + 1 ); |
| // markup the memory for each node |
| vNodes = Vec_PtrAlloc( nBits + 1 ); |
| Vec_PtrPush( vNodes, pMemory ); |
| for ( i = 1; i <= nBits; i++ ) |
| { |
| pMemory += pnNodes[i-1] + 1; |
| Vec_PtrPush( vNodes, pMemory ); |
| } |
| // add the nodes |
| memset( pnNodes, 0, sizeof(int) * (nBits + 1) ); |
| Aig_ManForEachObj( p->pAig, pObj, i ) |
| { |
| if ( i == 0 ) continue; |
| // skip non-PI and non-internal nodes |
| if ( fLatchCorr ) |
| { |
| if ( !Aig_ObjIsCi(pObj) ) |
| continue; |
| } |
| else |
| { |
| if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) ) |
| continue; |
| } |
| // skip nodes participating in the classes |
| // if ( Fra_ClassObjRepr(pObj) ) |
| // continue; |
| pMemory = (int *)Vec_PtrEntry( vNodes, pnBits[i] ); |
| pMemory[ pnNodes[pnBits[i]]++ ] = i; |
| } |
| // add 0s in the end |
| nTotal = 0; |
| Vec_PtrForEachEntry( int *, vNodes, pMemory, i ) |
| { |
| pMemory[ pnNodes[i]++ ] = 0; |
| nTotal += pnNodes[i]; |
| } |
| assert( nTotal == nNodes + nBits + 1 ); |
| ABC_FREE( pnNodes ); |
| ABC_FREE( pnBits ); |
| return vNodes; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Returns the array of implications with the highest cost.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Vec_Int_t * Fra_SmlSelectMaxCost( Vec_Int_t * vImps, int * pCosts, int nCostMax, int nImpLimit, int * pCostRange ) |
| { |
| Vec_Int_t * vImpsNew; |
| int * pCostCount, nImpCount, Imp, i, c; |
| assert( Vec_IntSize(vImps) >= nImpLimit ); |
| // count how many implications have each cost |
| pCostCount = ABC_ALLOC( int, nCostMax + 1 ); |
| memset( pCostCount, 0, sizeof(int) * (nCostMax + 1) ); |
| for ( i = 0; i < Vec_IntSize(vImps); i++ ) |
| { |
| assert( pCosts[i] <= nCostMax ); |
| pCostCount[ pCosts[i] ]++; |
| } |
| assert( pCostCount[0] == 0 ); |
| // select the bound on the cost (above this bound, implication will be included) |
| nImpCount = 0; |
| for ( c = nCostMax; c > 0; c-- ) |
| { |
| nImpCount += pCostCount[c]; |
| if ( nImpCount >= nImpLimit ) |
| break; |
| } |
| // printf( "Cost range >= %d.\n", c ); |
| // collect implications with the given costs |
| vImpsNew = Vec_IntAlloc( nImpLimit ); |
| Vec_IntForEachEntry( vImps, Imp, i ) |
| { |
| if ( pCosts[i] < c ) |
| continue; |
| Vec_IntPush( vImpsNew, Imp ); |
| if ( Vec_IntSize( vImpsNew ) == nImpLimit ) |
| break; |
| } |
| ABC_FREE( pCostCount ); |
| if ( pCostRange ) |
| *pCostRange = c; |
| return vImpsNew; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Compares two implications using their largest ID.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Sml_CompareMaxId( unsigned short * pImp1, unsigned short * pImp2 ) |
| { |
| int Max1 = Abc_MaxInt( pImp1[0], pImp1[1] ); |
| int Max2 = Abc_MaxInt( pImp2[0], pImp2[1] ); |
| if ( Max1 < Max2 ) |
| return -1; |
| if ( Max1 > Max2 ) |
| return 1; |
| return 0; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Derives implication candidates.] |
| |
| Description [Implication candidates have the property that |
| (1) they hold using sequential simulation information |
| (2) they do not hold using combinational simulation information |
| (3) they have as high expressive power as possible (heuristically) |
| that is, they are easy to disprove combinationally |
| meaning they cover relatively larger sequential subspace.] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, int fLatchCorr ) |
| { |
| int nSimWords = 64; |
| Fra_Sml_t * pSeq, * pComb; |
| Vec_Int_t * vImps, * vTemp; |
| Vec_Ptr_t * vNodes; |
| int * pImpCosts, * pNodesI, * pNodesK; |
| int nImpsTotal = 0, nImpsTried = 0, nImpsNonSeq = 0, nImpsComb = 0, nImpsCollected = 0; |
| int CostMin = ABC_INFINITY, CostMax = 0; |
| int i, k, Imp, CostRange; |
| abctime clk = Abc_Clock(); |
| assert( Aig_ManObjNumMax(p->pManAig) < (1 << 15) ); |
| assert( nImpMaxLimit > 0 && nImpUseLimit > 0 && nImpUseLimit <= nImpMaxLimit ); |
| // normalize both managers |
| pComb = Fra_SmlSimulateComb( p->pManAig, nSimWords, 0 ); |
| pSeq = Fra_SmlSimulateSeq( p->pManAig, p->pPars->nFramesP, nSimWords, 1, 1 ); |
| // get the nodes sorted by the number of 1s |
| vNodes = Fra_SmlSortUsingOnes( pSeq, fLatchCorr ); |
| // count the total number of implications |
| for ( k = nSimWords * 32; k > 0; k-- ) |
| for ( i = k - 1; i > 0; i-- ) |
| for ( pNodesI = (int *)Vec_PtrEntry( vNodes, i ); *pNodesI; pNodesI++ ) |
| for ( pNodesK = (int *)Vec_PtrEntry( vNodes, k ); *pNodesK; pNodesK++ ) |
| nImpsTotal++; |
| |
| // compute implications and their costs |
| pImpCosts = ABC_ALLOC( int, nImpMaxLimit ); |
| vImps = Vec_IntAlloc( nImpMaxLimit ); |
| for ( k = pSeq->nWordsTotal * 32; k > 0; k-- ) |
| for ( i = k - 1; i > 0; i-- ) |
| { |
| // HERE WE ARE MISSING SOME POTENTIAL IMPLICATIONS (with complement!) |
| |
| for ( pNodesI = (int *)Vec_PtrEntry( vNodes, i ); *pNodesI; pNodesI++ ) |
| for ( pNodesK = (int *)Vec_PtrEntry( vNodes, k ); *pNodesK; pNodesK++ ) |
| { |
| nImpsTried++; |
| if ( !Sml_NodeCheckImp(pSeq, *pNodesI, *pNodesK) ) |
| { |
| nImpsNonSeq++; |
| continue; |
| } |
| if ( Sml_NodeCheckImp(pComb, *pNodesI, *pNodesK) ) |
| { |
| nImpsComb++; |
| continue; |
| } |
| nImpsCollected++; |
| Imp = Fra_ImpCreate( *pNodesI, *pNodesK ); |
| pImpCosts[ Vec_IntSize(vImps) ] = Sml_NodeNotImpWeight(pComb, *pNodesI, *pNodesK); |
| CostMin = Abc_MinInt( CostMin, pImpCosts[ Vec_IntSize(vImps) ] ); |
| CostMax = Abc_MaxInt( CostMax, pImpCosts[ Vec_IntSize(vImps) ] ); |
| Vec_IntPush( vImps, Imp ); |
| if ( Vec_IntSize(vImps) == nImpMaxLimit ) |
| goto finish; |
| } |
| } |
| finish: |
| Fra_SmlStop( pComb ); |
| Fra_SmlStop( pSeq ); |
| |
| // select implications with the highest cost |
| CostRange = CostMin; |
| if ( Vec_IntSize(vImps) > nImpUseLimit ) |
| { |
| vImps = Fra_SmlSelectMaxCost( vTemp = vImps, pImpCosts, nSimWords * 32, nImpUseLimit, &CostRange ); |
| Vec_IntFree( vTemp ); |
| } |
| |
| // dealloc |
| ABC_FREE( pImpCosts ); |
| { |
| void * pTemp = Vec_PtrEntry(vNodes, 0); |
| ABC_FREE( pTemp ); |
| } |
| Vec_PtrFree( vNodes ); |
| // reorder implications topologically |
| qsort( (void *)Vec_IntArray(vImps), Vec_IntSize(vImps), sizeof(int), |
| (int (*)(const void *, const void *)) Sml_CompareMaxId ); |
| if ( p->pPars->fVerbose ) |
| { |
| printf( "Implications: All = %d. Try = %d. NonSeq = %d. Comb = %d. Res = %d.\n", |
| nImpsTotal, nImpsTried, nImpsNonSeq, nImpsComb, nImpsCollected ); |
| printf( "Implication weight: Min = %d. Pivot = %d. Max = %d. ", |
| CostMin, CostRange, CostMax ); |
| ABC_PRT( "Time", Abc_Clock() - clk ); |
| } |
| return vImps; |
| } |
| |
| |
| // the following three procedures are called to |
| // - add implications to the SAT solver |
| // - check implications using the SAT solver |
| // - refine implications using after a cex is generated |
| |
| /**Function************************************************************* |
| |
| Synopsis [Add implication clauses to the SAT solver.] |
| |
| Description [Note that implications should be checked in the first frame!] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Fra_ImpAddToSolver( Fra_Man_t * p, Vec_Int_t * vImps, int * pSatVarNums ) |
| { |
| sat_solver * pSat = p->pSat; |
| Aig_Obj_t * pLeft, * pRight; |
| Aig_Obj_t * pLeftF, * pRightF; |
| int pLits[2], Imp, Left, Right, i, f, status; |
| int fComplL, fComplR; |
| Vec_IntForEachEntry( vImps, Imp, i ) |
| { |
| // get the corresponding nodes |
| pLeft = Aig_ManObj( p->pManAig, Fra_ImpLeft(Imp) ); |
| pRight = Aig_ManObj( p->pManAig, Fra_ImpRight(Imp) ); |
| // check if all the nodes are present |
| for ( f = 0; f < p->pPars->nFramesK; f++ ) |
| { |
| // map these info fraig |
| pLeftF = Fra_ObjFraig( pLeft, f ); |
| pRightF = Fra_ObjFraig( pRight, f ); |
| if ( Aig_ObjIsNone(Aig_Regular(pLeftF)) || Aig_ObjIsNone(Aig_Regular(pRightF)) ) |
| { |
| Vec_IntWriteEntry( vImps, i, 0 ); |
| break; |
| } |
| } |
| if ( f < p->pPars->nFramesK ) |
| continue; |
| // add constraints in each timeframe |
| for ( f = 0; f < p->pPars->nFramesK; f++ ) |
| { |
| // map these info fraig |
| pLeftF = Fra_ObjFraig( pLeft, f ); |
| pRightF = Fra_ObjFraig( pRight, f ); |
| // get the corresponding SAT numbers |
| Left = pSatVarNums[ Aig_Regular(pLeftF)->Id ]; |
| Right = pSatVarNums[ Aig_Regular(pRightF)->Id ]; |
| assert( Left > 0 && Left < p->nSatVars ); |
| assert( Right > 0 && Right < p->nSatVars ); |
| // get the complemented attributes |
| fComplL = pLeft->fPhase ^ Aig_IsComplement(pLeftF); |
| fComplR = pRight->fPhase ^ Aig_IsComplement(pRightF); |
| // get the constraint |
| // L => R L' v R (complement = L & R') |
| pLits[0] = 2 * Left + !fComplL; |
| pLits[1] = 2 * Right + fComplR; |
| // add constraint to solver |
| if ( !sat_solver_addclause( pSat, pLits, pLits + 2 ) ) |
| { |
| sat_solver_delete( pSat ); |
| p->pSat = NULL; |
| return; |
| } |
| } |
| } |
| status = sat_solver_simplify(pSat); |
| if ( status == 0 ) |
| { |
| sat_solver_delete( pSat ); |
| p->pSat = NULL; |
| } |
| // printf( "Total imps = %d. ", Vec_IntSize(vImps) ); |
| Fra_ImpCompactArray( vImps ); |
| // printf( "Valid imps = %d. \n", Vec_IntSize(vImps) ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Check implications for the node (if they are present).] |
| |
| Description [Returns the new position in the array.] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Fra_ImpCheckForNode( Fra_Man_t * p, Vec_Int_t * vImps, Aig_Obj_t * pNode, int Pos ) |
| { |
| Aig_Obj_t * pLeft, * pRight; |
| Aig_Obj_t * pLeftF, * pRightF; |
| int i, Imp, Left, Right, Max, RetValue; |
| int fComplL, fComplR; |
| Vec_IntForEachEntryStart( vImps, Imp, i, Pos ) |
| { |
| if ( Imp == 0 ) |
| continue; |
| Left = Fra_ImpLeft(Imp); |
| Right = Fra_ImpRight(Imp); |
| Max = Abc_MaxInt( Left, Right ); |
| assert( Max >= pNode->Id ); |
| if ( Max > pNode->Id ) |
| return i; |
| // get the corresponding nodes |
| pLeft = Aig_ManObj( p->pManAig, Left ); |
| pRight = Aig_ManObj( p->pManAig, Right ); |
| // get the corresponding FRAIG nodes |
| pLeftF = Fra_ObjFraig( pLeft, p->pPars->nFramesK ); |
| pRightF = Fra_ObjFraig( pRight, p->pPars->nFramesK ); |
| // get the complemented attributes |
| fComplL = pLeft->fPhase ^ Aig_IsComplement(pLeftF); |
| fComplR = pRight->fPhase ^ Aig_IsComplement(pRightF); |
| // check equality |
| if ( Aig_Regular(pLeftF) == Aig_Regular(pRightF) ) |
| { |
| if ( fComplL == fComplR ) // x => x - always true |
| continue; |
| assert( fComplL != fComplR ); |
| // consider 4 possibilities: |
| // NOT(1) => 1 or 0 => 1 - always true |
| // 1 => NOT(1) or 1 => 0 - never true |
| // NOT(x) => x or x - not always true |
| // x => NOT(x) or NOT(x) - not always true |
| if ( Aig_ObjIsConst1(Aig_Regular(pLeftF)) && fComplL ) // proved implication |
| continue; |
| // disproved implication |
| p->pCla->fRefinement = 1; |
| Vec_IntWriteEntry( vImps, i, 0 ); |
| continue; |
| } |
| // check the implication |
| // - if true, a clause is added |
| // - if false, a cex is simulated |
| // make sure the implication is refined |
| RetValue = Fra_NodesAreImp( p, Aig_Regular(pLeftF), Aig_Regular(pRightF), fComplL, fComplR ); |
| if ( RetValue != 1 ) |
| { |
| p->pCla->fRefinement = 1; |
| if ( RetValue == 0 ) |
| Fra_SmlResimulate( p ); |
| if ( Vec_IntEntry(vImps, i) != 0 ) |
| printf( "Fra_ImpCheckForNode(): Implication is not refined!\n" ); |
| assert( Vec_IntEntry(vImps, i) == 0 ); |
| } |
| } |
| return i; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Removes those implications that no longer hold.] |
| |
| Description [Returns 1 if refinement has happened.] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Fra_ImpRefineUsingCex( Fra_Man_t * p, Vec_Int_t * vImps ) |
| { |
| Aig_Obj_t * pLeft, * pRight; |
| int Imp, i, RetValue = 0; |
| Vec_IntForEachEntry( vImps, Imp, i ) |
| { |
| if ( Imp == 0 ) |
| continue; |
| // get the corresponding nodes |
| pLeft = Aig_ManObj( p->pManAig, Fra_ImpLeft(Imp) ); |
| pRight = Aig_ManObj( p->pManAig, Fra_ImpRight(Imp) ); |
| // check if implication holds using this simulation info |
| if ( !Sml_NodeCheckImp(p->pSml, pLeft->Id, pRight->Id) ) |
| { |
| Vec_IntWriteEntry( vImps, i, 0 ); |
| RetValue = 1; |
| } |
| } |
| return RetValue; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Removes empty implications.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Fra_ImpCompactArray( Vec_Int_t * vImps ) |
| { |
| int i, k, Imp; |
| k = 0; |
| Vec_IntForEachEntry( vImps, Imp, i ) |
| if ( Imp ) |
| Vec_IntWriteEntry( vImps, k++, Imp ); |
| Vec_IntShrink( vImps, k ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Determines the ratio of the state space by computed implications.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| double Fra_ImpComputeStateSpaceRatio( Fra_Man_t * p ) |
| { |
| int nSimWords = 64; |
| Fra_Sml_t * pComb; |
| unsigned * pResult; |
| double Ratio = 0.0; |
| int Left, Right, Imp, i; |
| if ( p->pCla->vImps == NULL || Vec_IntSize(p->pCla->vImps) == 0 ) |
| return Ratio; |
| // simulate the AIG manager with combinational patterns |
| pComb = Fra_SmlSimulateComb( p->pManAig, nSimWords, 0 ); |
| // go through the implications and collect where they do not hold |
| pResult = Fra_ObjSim( pComb, 0 ); |
| assert( pResult[0] == 0 ); |
| Vec_IntForEachEntry( p->pCla->vImps, Imp, i ) |
| { |
| Left = Fra_ImpLeft(Imp); |
| Right = Fra_ImpRight(Imp); |
| Sml_NodeSaveNotImpPatterns( pComb, Left, Right, pResult ); |
| } |
| // count the number of ones in this area |
| Ratio = 100.0 * Fra_SmlCountOnesOne( pComb, 0 ) / (32*(pComb->nWordsTotal-pComb->nWordsPref)); |
| Fra_SmlStop( pComb ); |
| return Ratio; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Returns the number of failed implications.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Fra_ImpVerifyUsingSimulation( Fra_Man_t * p ) |
| { |
| int nFrames = 2000; |
| int nSimWords = 8; |
| Fra_Sml_t * pSeq; |
| char * pfFails; |
| int Left, Right, Imp, i, Counter; |
| if ( p->pCla->vImps == NULL || Vec_IntSize(p->pCla->vImps) == 0 ) |
| return 0; |
| // simulate the AIG manager with combinational patterns |
| pSeq = Fra_SmlSimulateSeq( p->pManAig, p->pPars->nFramesP, nFrames, nSimWords, 1 ); |
| // go through the implications and check how many of them do not hold |
| pfFails = ABC_ALLOC( char, Vec_IntSize(p->pCla->vImps) ); |
| memset( pfFails, 0, sizeof(char) * Vec_IntSize(p->pCla->vImps) ); |
| Vec_IntForEachEntry( p->pCla->vImps, Imp, i ) |
| { |
| Left = Fra_ImpLeft(Imp); |
| Right = Fra_ImpRight(Imp); |
| pfFails[i] = !Sml_NodeCheckImp( pSeq, Left, Right ); |
| } |
| // count how many has failed |
| Counter = 0; |
| for ( i = 0; i < Vec_IntSize(p->pCla->vImps); i++ ) |
| Counter += pfFails[i]; |
| ABC_FREE( pfFails ); |
| Fra_SmlStop( pSeq ); |
| return Counter; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Record proven implications in the AIG manager.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Fra_ImpRecordInManager( Fra_Man_t * p, Aig_Man_t * pNew ) |
| { |
| Aig_Obj_t * pLeft, * pRight, * pMiter; |
| int nPosOld, Imp, i; |
| if ( p->pCla->vImps == NULL || Vec_IntSize(p->pCla->vImps) == 0 ) |
| return; |
| // go through the implication |
| nPosOld = Aig_ManCoNum(pNew); |
| Vec_IntForEachEntry( p->pCla->vImps, Imp, i ) |
| { |
| pLeft = Aig_ManObj( p->pManAig, Fra_ImpLeft(Imp) ); |
| pRight = Aig_ManObj( p->pManAig, Fra_ImpRight(Imp) ); |
| // record the implication: L' + R |
| pMiter = Aig_Or( pNew, |
| Aig_NotCond((Aig_Obj_t *)pLeft->pData, !pLeft->fPhase), |
| Aig_NotCond((Aig_Obj_t *)pRight->pData, pRight->fPhase) ); |
| Aig_ObjCreateCo( pNew, pMiter ); |
| } |
| pNew->nAsserts = Aig_ManCoNum(pNew) - nPosOld; |
| } |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
