| /**CFile**************************************************************** |
| |
| FileName [fraClaus.c] |
| |
| SystemName [ABC: Logic synthesis and verification system.] |
| |
| PackageName [New FRAIG package.] |
| |
| Synopsis [Induction with clause strengthening.] |
| |
| Author [Alan Mishchenko] |
| |
| Affiliation [UC Berkeley] |
| |
| Date [Ver. 1.0. Started - June 30, 2007.] |
| |
| Revision [$Id: fraClau.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $] |
| |
| ***********************************************************************/ |
| |
| #include "fra.h" |
| #include "sat/cnf/cnf.h" |
| #include "sat/bsat/satSolver.h" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// DECLARATIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| typedef struct Clu_Man_t_ Clu_Man_t; |
| struct Clu_Man_t_ |
| { |
| // parameters |
| int nFrames; // the K of the K-step induction |
| int nPref; // the number of timeframes to skip |
| int nClausesMax; // the max number of 4-clauses to consider |
| int nLutSize; // the max cut size |
| int nLevels; // the number of levels for cut computation |
| int nCutsMax; // the maximum number of cuts to compute at a node |
| int nBatches; // the number of clause batches to use |
| int fStepUp; // increase cut size for each batch |
| int fTarget; // tries to prove the property |
| int fVerbose; |
| int fVeryVerbose; |
| // internal parameters |
| int nSimWords; // the number of simulation words |
| int nSimWordsPref; // the number of simulation words in the prefix |
| int nSimFrames; // the number of frames to simulate |
| int nBTLimit; // the largest number of backtracks (0 = infinite) |
| // the network |
| Aig_Man_t * pAig; |
| // SAT solvers |
| sat_solver * pSatMain; |
| sat_solver * pSatBmc; |
| // CNF for the test solver |
| Cnf_Dat_t * pCnf; |
| int fFail; |
| int fFiltering; |
| int fNothingNew; |
| // clauses |
| Vec_Int_t * vLits; |
| Vec_Int_t * vClauses; |
| Vec_Int_t * vCosts; |
| int nClauses; |
| int nCuts; |
| int nOneHots; |
| int nOneHotsProven; |
| // clauses proven |
| Vec_Int_t * vLitsProven; |
| Vec_Int_t * vClausesProven; |
| // counter-examples |
| Vec_Ptr_t * vCexes; |
| int nCexes; |
| int nCexesAlloc; |
| }; |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// FUNCTION DEFINITIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| /**Function************************************************************* |
| |
| Synopsis [Runs the SAT solver on the problem.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Fra_ClausRunBmc( Clu_Man_t * p ) |
| { |
| Aig_Obj_t * pObj; |
| int Lits[2], nLitsTot, RetValue, i; |
| // set the output literals |
| nLitsTot = 2 * p->pCnf->nVars; |
| pObj = Aig_ManCo(p->pAig, 0); |
| for ( i = 0; i < p->nPref + p->nFrames; i++ ) |
| { |
| Lits[0] = i * nLitsTot + toLitCond( p->pCnf->pVarNums[pObj->Id], 0 ); |
| RetValue = sat_solver_solve( p->pSatBmc, Lits, Lits + 1, (ABC_INT64_T)p->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); |
| if ( RetValue != l_False ) |
| return 0; |
| } |
| return 1; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Runs the SAT solver on the problem.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Fra_ClausRunSat( Clu_Man_t * p ) |
| { |
| Aig_Obj_t * pObj; |
| int * pLits; |
| int i, RetValue; |
| pLits = ABC_ALLOC( int, p->nFrames + 1 ); |
| // set the output literals |
| pObj = Aig_ManCo(p->pAig, 0); |
| for ( i = 0; i <= p->nFrames; i++ ) |
| pLits[i] = i * 2 * p->pCnf->nVars + toLitCond( p->pCnf->pVarNums[pObj->Id], i != p->nFrames ); |
| // try to solve the problem |
| RetValue = sat_solver_solve( p->pSatMain, pLits, pLits + p->nFrames + 1, (ABC_INT64_T)p->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); |
| ABC_FREE( pLits ); |
| if ( RetValue == l_False ) |
| return 1; |
| // get the counter-example |
| assert( RetValue == l_True ); |
| return 0; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Runs the SAT solver on the problem.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Fra_ClausRunSat0( Clu_Man_t * p ) |
| { |
| Aig_Obj_t * pObj; |
| int Lits[2], RetValue; |
| pObj = Aig_ManCo(p->pAig, 0); |
| Lits[0] = toLitCond( p->pCnf->pVarNums[pObj->Id], 0 ); |
| RetValue = sat_solver_solve( p->pSatMain, Lits, Lits + 1, (ABC_INT64_T)p->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); |
| if ( RetValue == l_False ) |
| return 1; |
| return 0; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Return combinations appearing in the cut.] |
| |
| Description [This procedure is taken from "Hacker's Delight" by H.S.Warren.] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void transpose32a( unsigned a[32] ) |
| { |
| int j, k; |
| unsigned long m, t; |
| for ( j = 16, m = 0x0000FFFF; j; j >>= 1, m ^= m << j ) |
| { |
| for ( k = 0; k < 32; k = ((k | j) + 1) & ~j ) |
| { |
| t = (a[k] ^ (a[k|j] >> j)) & m; |
| a[k] ^= t; |
| a[k|j] ^= (t << j); |
| } |
| } |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Return combinations appearing in the cut.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Fra_ClausProcessClausesCut( Clu_Man_t * p, Fra_Sml_t * pSimMan, Dar_Cut_t * pCut, int * pScores ) |
| { |
| unsigned Matrix[32]; |
| unsigned * pSims[16], uWord; |
| int nSeries, i, k, j; |
| int nWordsForSim = pSimMan->nWordsTotal - p->nSimWordsPref; |
| // compute parameters |
| assert( pCut->nLeaves > 1 && pCut->nLeaves < 5 ); |
| assert( nWordsForSim % 8 == 0 ); |
| // get parameters |
| for ( i = 0; i < (int)pCut->nLeaves; i++ ) |
| pSims[i] = Fra_ObjSim( pSimMan, pCut->pLeaves[i] ) + p->nSimWordsPref; |
| // add combinational patterns |
| memset( pScores, 0, sizeof(int) * 16 ); |
| nSeries = nWordsForSim / 8; |
| for ( i = 0; i < nSeries; i++ ) |
| { |
| memset( Matrix, 0, sizeof(unsigned) * 32 ); |
| for ( k = 0; k < 8; k++ ) |
| for ( j = 0; j < (int)pCut->nLeaves; j++ ) |
| Matrix[31-(k*4+j)] = pSims[j][i*8+k]; |
| transpose32a( Matrix ); |
| for ( k = 0; k < 32; k++ ) |
| for ( j = 0, uWord = Matrix[k]; j < 8; j++, uWord >>= 4 ) |
| pScores[uWord & 0xF]++; |
| } |
| // collect patterns |
| uWord = 0; |
| for ( i = 0; i < 16; i++ ) |
| if ( pScores[i] ) |
| uWord |= (1 << i); |
| // Extra_PrintBinary( stdout, &uWord, 16 ); printf( "\n" ); |
| return (int)uWord; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Return combinations appearing in the cut.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Fra_ClausProcessClausesCut2( Clu_Man_t * p, Fra_Sml_t * pSimMan, Dar_Cut_t * pCut, int * pScores ) |
| { |
| unsigned * pSims[16], uWord; |
| int iMint, i, k, b; |
| int nWordsForSim = pSimMan->nWordsTotal - p->nSimWordsPref; |
| // compute parameters |
| assert( pCut->nLeaves > 1 && pCut->nLeaves < 5 ); |
| assert( nWordsForSim % 8 == 0 ); |
| // get parameters |
| for ( i = 0; i < (int)pCut->nLeaves; i++ ) |
| pSims[i] = Fra_ObjSim( pSimMan, pCut->pLeaves[i] ) + p->nSimWordsPref; |
| // add combinational patterns |
| memset( pScores, 0, sizeof(int) * 16 ); |
| for ( i = 0; i < nWordsForSim; i++ ) |
| for ( k = 0; k < 32; k++ ) |
| { |
| iMint = 0; |
| for ( b = 0; b < (int)pCut->nLeaves; b++ ) |
| if ( pSims[b][i] & (1 << k) ) |
| iMint |= (1 << b); |
| pScores[iMint]++; |
| } |
| // collect patterns |
| uWord = 0; |
| for ( i = 0; i < 16; i++ ) |
| if ( pScores[i] ) |
| uWord |= (1 << i); |
| // Extra_PrintBinary( stdout, &uWord, 16 ); printf( "\n" ); |
| return (int)uWord; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Return the number of combinations appearing in the cut.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Fra_ClausProcessClausesCut3( Clu_Man_t * p, Fra_Sml_t * pSimMan, Aig_Cut_t * pCut, int * pScores ) |
| { |
| unsigned Matrix[32]; |
| unsigned * pSims[16], uWord; |
| int iMint, i, j, k, b, nMints, nSeries; |
| int nWordsForSim = pSimMan->nWordsTotal - p->nSimWordsPref; |
| |
| // compute parameters |
| assert( pCut->nFanins > 1 && pCut->nFanins < 17 ); |
| assert( nWordsForSim % 8 == 0 ); |
| // get parameters |
| for ( i = 0; i < (int)pCut->nFanins; i++ ) |
| pSims[i] = Fra_ObjSim( pSimMan, pCut->pFanins[i] ) + p->nSimWordsPref; |
| // add combinational patterns |
| nMints = (1 << pCut->nFanins); |
| memset( pScores, 0, sizeof(int) * nMints ); |
| |
| if ( pCut->nLeafMax == 4 ) |
| { |
| // convert the simulation patterns |
| nSeries = nWordsForSim / 8; |
| for ( i = 0; i < nSeries; i++ ) |
| { |
| memset( Matrix, 0, sizeof(unsigned) * 32 ); |
| for ( k = 0; k < 8; k++ ) |
| for ( j = 0; j < (int)pCut->nFanins; j++ ) |
| Matrix[31-(k*4+j)] = pSims[j][i*8+k]; |
| transpose32a( Matrix ); |
| for ( k = 0; k < 32; k++ ) |
| for ( j = 0, uWord = Matrix[k]; j < 8; j++, uWord >>= 4 ) |
| pScores[uWord & 0xF]++; |
| } |
| } |
| else |
| { |
| // go through the simulation patterns |
| for ( i = 0; i < nWordsForSim; i++ ) |
| for ( k = 0; k < 32; k++ ) |
| { |
| iMint = 0; |
| for ( b = 0; b < (int)pCut->nFanins; b++ ) |
| if ( pSims[b][i] & (1 << k) ) |
| iMint |= (1 << b); |
| pScores[iMint]++; |
| } |
| } |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Returns the cut-off cost.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Fra_ClausSelectClauses( Clu_Man_t * p ) |
| { |
| int * pCostCount, nClauCount, Cost, CostMax, i, c; |
| assert( Vec_IntSize(p->vClauses) > p->nClausesMax ); |
| // count how many implications have each cost |
| CostMax = p->nSimWords * 32 + 1; |
| pCostCount = ABC_ALLOC( int, CostMax ); |
| memset( pCostCount, 0, sizeof(int) * CostMax ); |
| Vec_IntForEachEntry( p->vCosts, Cost, i ) |
| { |
| if ( Cost == -1 ) |
| continue; |
| assert( Cost < CostMax ); |
| pCostCount[ Cost ]++; |
| } |
| assert( pCostCount[0] == 0 ); |
| // select the bound on the cost (above this bound, implication will be included) |
| nClauCount = 0; |
| for ( c = CostMax - 1; c > 0; c-- ) |
| { |
| assert( pCostCount[c] >= 0 ); |
| nClauCount += pCostCount[c]; |
| if ( nClauCount >= p->nClausesMax ) |
| break; |
| } |
| // collect implications with the given costs |
| nClauCount = 0; |
| Vec_IntForEachEntry( p->vCosts, Cost, i ) |
| { |
| if ( Cost >= c && nClauCount < p->nClausesMax ) |
| { |
| nClauCount++; |
| continue; |
| } |
| Vec_IntWriteEntry( p->vCosts, i, -1 ); |
| } |
| ABC_FREE( pCostCount ); |
| p->nClauses = nClauCount; |
| if ( p->fVerbose ) |
| printf( "Selected %d clauses. Cost range: [%d < %d < %d]\n", nClauCount, 1, c, CostMax ); |
| return c; |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Processes the clauses.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Fra_ClausRecordClause( Clu_Man_t * p, Dar_Cut_t * pCut, int iMint, int Cost ) |
| { |
| int i; |
| for ( i = 0; i < (int)pCut->nLeaves; i++ ) |
| Vec_IntPush( p->vLits, toLitCond( p->pCnf->pVarNums[pCut->pLeaves[i]], (iMint&(1<<i)) ) ); |
| Vec_IntPush( p->vClauses, Vec_IntSize(p->vLits) ); |
| Vec_IntPush( p->vCosts, Cost ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Processes the clauses.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Fra_ClausRecordClause2( Clu_Man_t * p, Aig_Cut_t * pCut, int iMint, int Cost ) |
| { |
| int i; |
| for ( i = 0; i < (int)pCut->nFanins; i++ ) |
| Vec_IntPush( p->vLits, toLitCond( p->pCnf->pVarNums[pCut->pFanins[i]], (iMint&(1<<i)) ) ); |
| Vec_IntPush( p->vClauses, Vec_IntSize(p->vLits) ); |
| Vec_IntPush( p->vCosts, Cost ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Returns 1 if simulation info is composed of all zeros.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Fra_ClausSmlNodeIsConst( Fra_Sml_t * pSeq, Aig_Obj_t * pObj ) |
| { |
| unsigned * pSims; |
| int i; |
| pSims = Fra_ObjSim(pSeq, pObj->Id); |
| for ( i = pSeq->nWordsPref; i < pSeq->nWordsTotal; i++ ) |
| if ( pSims[i] ) |
| return 0; |
| return 1; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Returns 1 if implications holds.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Fra_ClausSmlNodesAreImp( Fra_Sml_t * pSeq, Aig_Obj_t * pObj1, Aig_Obj_t * pObj2 ) |
| { |
| unsigned * pSimL, * pSimR; |
| int k; |
| pSimL = Fra_ObjSim(pSeq, pObj1->Id); |
| pSimR = Fra_ObjSim(pSeq, pObj2->Id); |
| for ( k = pSeq->nWordsPref; k < pSeq->nWordsTotal; k++ ) |
| if ( pSimL[k] & ~pSimR[k] ) // !(Obj1 -> Obj2) |
| return 0; |
| return 1; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Returns 1 if implications holds.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Fra_ClausSmlNodesAreImpC( Fra_Sml_t * pSeq, Aig_Obj_t * pObj1, Aig_Obj_t * pObj2 ) |
| { |
| unsigned * pSimL, * pSimR; |
| int k; |
| pSimL = Fra_ObjSim(pSeq, pObj1->Id); |
| pSimR = Fra_ObjSim(pSeq, pObj2->Id); |
| for ( k = pSeq->nWordsPref; k < pSeq->nWordsTotal; k++ ) |
| if ( pSimL[k] & pSimR[k] ) |
| return 0; |
| return 1; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Processes the clauses.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Fra_ClausCollectLatchClauses( Clu_Man_t * p, Fra_Sml_t * pSeq ) |
| { |
| Aig_Obj_t * pObj1, * pObj2; |
| unsigned * pSims1, * pSims2; |
| int CostMax, i, k, nCountConst, nCountImps; |
| |
| nCountConst = nCountImps = 0; |
| CostMax = p->nSimWords * 32; |
| /* |
| // add the property |
| { |
| Aig_Obj_t * pObj; |
| int Lits[1]; |
| pObj = Aig_ManCo( p->pAig, 0 ); |
| Lits[0] = toLitCond( p->pCnf->pVarNums[pObj->Id], 1 ); |
| Vec_IntPush( p->vLits, Lits[0] ); |
| Vec_IntPush( p->vClauses, Vec_IntSize(p->vLits) ); |
| Vec_IntPush( p->vCosts, CostMax ); |
| nCountConst++; |
| // printf( "Added the target property to the set of clauses to be inductively checked.\n" ); |
| } |
| */ |
| |
| pSeq->nWordsPref = p->nSimWordsPref; |
| Aig_ManForEachLoSeq( p->pAig, pObj1, i ) |
| { |
| pSims1 = Fra_ObjSim( pSeq, pObj1->Id ); |
| if ( Fra_ClausSmlNodeIsConst( pSeq, pObj1 ) ) |
| { |
| Vec_IntPush( p->vLits, toLitCond( p->pCnf->pVarNums[pObj1->Id], 1 ) ); |
| Vec_IntPush( p->vClauses, Vec_IntSize(p->vLits) ); |
| Vec_IntPush( p->vCosts, CostMax ); |
| nCountConst++; |
| continue; |
| } |
| Aig_ManForEachLoSeq( p->pAig, pObj2, k ) |
| { |
| pSims2 = Fra_ObjSim( pSeq, pObj2->Id ); |
| if ( Fra_ClausSmlNodesAreImp( pSeq, pObj1, pObj2 ) ) |
| { |
| Vec_IntPush( p->vLits, toLitCond( p->pCnf->pVarNums[pObj1->Id], 1 ) ); |
| Vec_IntPush( p->vLits, toLitCond( p->pCnf->pVarNums[pObj2->Id], 0 ) ); |
| Vec_IntPush( p->vClauses, Vec_IntSize(p->vLits) ); |
| Vec_IntPush( p->vCosts, CostMax ); |
| nCountImps++; |
| continue; |
| } |
| if ( Fra_ClausSmlNodesAreImp( pSeq, pObj2, pObj1 ) ) |
| { |
| Vec_IntPush( p->vLits, toLitCond( p->pCnf->pVarNums[pObj2->Id], 1 ) ); |
| Vec_IntPush( p->vLits, toLitCond( p->pCnf->pVarNums[pObj1->Id], 0 ) ); |
| Vec_IntPush( p->vClauses, Vec_IntSize(p->vLits) ); |
| Vec_IntPush( p->vCosts, CostMax ); |
| nCountImps++; |
| continue; |
| } |
| if ( Fra_ClausSmlNodesAreImpC( pSeq, pObj1, pObj2 ) ) |
| { |
| Vec_IntPush( p->vLits, toLitCond( p->pCnf->pVarNums[pObj1->Id], 1 ) ); |
| Vec_IntPush( p->vLits, toLitCond( p->pCnf->pVarNums[pObj2->Id], 1 ) ); |
| Vec_IntPush( p->vClauses, Vec_IntSize(p->vLits) ); |
| Vec_IntPush( p->vCosts, CostMax ); |
| nCountImps++; |
| continue; |
| } |
| } |
| if ( nCountConst + nCountImps > p->nClausesMax / 2 ) |
| break; |
| } |
| pSeq->nWordsPref = 0; |
| if ( p->fVerbose ) |
| printf( "Collected %d register constants and %d one-hotness implications.\n", nCountConst, nCountImps ); |
| p->nOneHots = nCountConst + nCountImps; |
| p->nOneHotsProven = 0; |
| return 0; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Processes the clauses.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Fra_ClausProcessClauses( Clu_Man_t * p, int fRefs ) |
| { |
| Aig_MmFixed_t * pMemCuts; |
| // Aig_ManCut_t * pManCut; |
| Fra_Sml_t * pComb, * pSeq; |
| Aig_Obj_t * pObj; |
| Dar_Cut_t * pCut; |
| int Scores[16], uScores, i, k, j, nCuts = 0; |
| abctime clk; |
| |
| // simulate the AIG |
| clk = Abc_Clock(); |
| // srand( 0xAABBAABB ); |
| Aig_ManRandom(1); |
| pSeq = Fra_SmlSimulateSeq( p->pAig, 0, p->nPref + p->nSimFrames, p->nSimWords/p->nSimFrames, 1 ); |
| if ( p->fTarget && pSeq->fNonConstOut ) |
| { |
| printf( "Property failed after sequential simulation!\n" ); |
| Fra_SmlStop( pSeq ); |
| return 0; |
| } |
| if ( p->fVerbose ) |
| { |
| ABC_PRT( "Sim-seq", Abc_Clock() - clk ); |
| } |
| |
| |
| clk = Abc_Clock(); |
| if ( fRefs ) |
| { |
| Fra_ClausCollectLatchClauses( p, pSeq ); |
| if ( p->fVerbose ) |
| { |
| ABC_PRT( "Lat-cla", Abc_Clock() - clk ); |
| } |
| } |
| |
| |
| // generate cuts for all nodes, assign cost, and find best cuts |
| clk = Abc_Clock(); |
| pMemCuts = Dar_ManComputeCuts( p->pAig, 10, 0, 1 ); |
| // pManCut = Aig_ComputeCuts( p->pAig, 10, 4, 0, 1 ); |
| if ( p->fVerbose ) |
| { |
| ABC_PRT( "Cuts ", Abc_Clock() - clk ); |
| } |
| |
| // collect sequential info for each cut |
| clk = Abc_Clock(); |
| Aig_ManForEachNode( p->pAig, pObj, i ) |
| Dar_ObjForEachCut( pObj, pCut, k ) |
| if ( pCut->nLeaves > 1 ) |
| { |
| pCut->uTruth = Fra_ClausProcessClausesCut( p, pSeq, pCut, Scores ); |
| // uScores = Fra_ClausProcessClausesCut2( p, pSeq, pCut, Scores ); |
| // if ( uScores != pCut->uTruth ) |
| // { |
| // int x = 0; |
| // } |
| } |
| if ( p->fVerbose ) |
| { |
| ABC_PRT( "Infoseq", Abc_Clock() - clk ); |
| } |
| Fra_SmlStop( pSeq ); |
| |
| // perform combinational simulation |
| clk = Abc_Clock(); |
| // srand( 0xAABBAABB ); |
| Aig_ManRandom(1); |
| pComb = Fra_SmlSimulateComb( p->pAig, p->nSimWords + p->nSimWordsPref, 0 ); |
| if ( p->fVerbose ) |
| { |
| ABC_PRT( "Sim-cmb", Abc_Clock() - clk ); |
| } |
| |
| // collect combinational info for each cut |
| clk = Abc_Clock(); |
| Aig_ManForEachNode( p->pAig, pObj, i ) |
| Dar_ObjForEachCut( pObj, pCut, k ) |
| if ( pCut->nLeaves > 1 ) |
| { |
| nCuts++; |
| uScores = Fra_ClausProcessClausesCut( p, pComb, pCut, Scores ); |
| uScores &= ~pCut->uTruth; pCut->uTruth = 0; |
| if ( uScores == 0 ) |
| continue; |
| // write the clauses |
| for ( j = 0; j < (1<<pCut->nLeaves); j++ ) |
| if ( uScores & (1 << j) ) |
| Fra_ClausRecordClause( p, pCut, j, Scores[j] ); |
| |
| } |
| Fra_SmlStop( pComb ); |
| Aig_MmFixedStop( pMemCuts, 0 ); |
| // Aig_ManCutStop( pManCut ); |
| if ( p->fVerbose ) |
| { |
| ABC_PRT( "Infocmb", Abc_Clock() - clk ); |
| } |
| |
| if ( p->fVerbose ) |
| printf( "Node = %5d. Non-triv cuts = %7d. Clauses = %6d. Clause per cut = %6.2f.\n", |
| Aig_ManNodeNum(p->pAig), nCuts, Vec_IntSize(p->vClauses), 1.0*Vec_IntSize(p->vClauses)/nCuts ); |
| |
| if ( Vec_IntSize(p->vClauses) > p->nClausesMax ) |
| Fra_ClausSelectClauses( p ); |
| else |
| p->nClauses = Vec_IntSize( p->vClauses ); |
| return 1; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Processes the clauses.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Fra_ClausProcessClauses2( Clu_Man_t * p, int fRefs ) |
| { |
| // Aig_MmFixed_t * pMemCuts; |
| Aig_ManCut_t * pManCut; |
| Fra_Sml_t * pComb, * pSeq; |
| Aig_Obj_t * pObj; |
| Aig_Cut_t * pCut; |
| int i, k, j, nCuts = 0; |
| abctime clk; |
| int ScoresSeq[1<<12], ScoresComb[1<<12]; |
| assert( p->nLutSize < 13 ); |
| |
| // simulate the AIG |
| clk = Abc_Clock(); |
| // srand( 0xAABBAABB ); |
| Aig_ManRandom(1); |
| pSeq = Fra_SmlSimulateSeq( p->pAig, 0, p->nPref + p->nSimFrames, p->nSimWords/p->nSimFrames, 1 ); |
| if ( p->fTarget && pSeq->fNonConstOut ) |
| { |
| printf( "Property failed after sequential simulation!\n" ); |
| Fra_SmlStop( pSeq ); |
| return 0; |
| } |
| if ( p->fVerbose ) |
| { |
| //ABC_PRT( "Sim-seq", Abc_Clock() - clk ); |
| } |
| |
| // perform combinational simulation |
| clk = Abc_Clock(); |
| // srand( 0xAABBAABB ); |
| Aig_ManRandom(1); |
| pComb = Fra_SmlSimulateComb( p->pAig, p->nSimWords + p->nSimWordsPref, 0 ); |
| if ( p->fVerbose ) |
| { |
| //ABC_PRT( "Sim-cmb", Abc_Clock() - clk ); |
| } |
| |
| |
| clk = Abc_Clock(); |
| if ( fRefs ) |
| { |
| Fra_ClausCollectLatchClauses( p, pSeq ); |
| if ( p->fVerbose ) |
| { |
| //ABC_PRT( "Lat-cla", Abc_Clock() - clk ); |
| } |
| } |
| |
| |
| // generate cuts for all nodes, assign cost, and find best cuts |
| clk = Abc_Clock(); |
| // pMemCuts = Dar_ManComputeCuts( p->pAig, 10, 0, 1 ); |
| pManCut = Aig_ComputeCuts( p->pAig, p->nCutsMax, p->nLutSize, 0, p->fVerbose ); |
| if ( p->fVerbose ) |
| { |
| //ABC_PRT( "Cuts ", Abc_Clock() - clk ); |
| } |
| |
| // collect combinational info for each cut |
| clk = Abc_Clock(); |
| Aig_ManForEachNode( p->pAig, pObj, i ) |
| { |
| if ( pObj->Level > (unsigned)p->nLevels ) |
| continue; |
| Aig_ObjForEachCut( pManCut, pObj, pCut, k ) |
| if ( pCut->nFanins > 1 ) |
| { |
| nCuts++; |
| Fra_ClausProcessClausesCut3( p, pSeq, pCut, ScoresSeq ); |
| Fra_ClausProcessClausesCut3( p, pComb, pCut, ScoresComb ); |
| // write the clauses |
| for ( j = 0; j < (1<<pCut->nFanins); j++ ) |
| if ( ScoresComb[j] != 0 && ScoresSeq[j] == 0 ) |
| Fra_ClausRecordClause2( p, pCut, j, ScoresComb[j] ); |
| |
| } |
| } |
| Fra_SmlStop( pSeq ); |
| Fra_SmlStop( pComb ); |
| p->nCuts = nCuts; |
| // Aig_MmFixedStop( pMemCuts, 0 ); |
| Aig_ManCutStop( pManCut ); |
| p->pAig->pManCuts = NULL; |
| |
| if ( p->fVerbose ) |
| { |
| printf( "Node = %5d. Cuts = %7d. Clauses = %6d. Clause/cut = %6.2f.\n", |
| Aig_ManNodeNum(p->pAig), nCuts, Vec_IntSize(p->vClauses), 1.0*Vec_IntSize(p->vClauses)/nCuts ); |
| ABC_PRT( "Processing sim-info to find candidate clauses (unoptimized)", Abc_Clock() - clk ); |
| } |
| |
| // filter out clauses that are contained in the already proven clauses |
| assert( p->nClauses == 0 ); |
| p->nClauses = Vec_IntSize( p->vClauses ); |
| if ( Vec_IntSize( p->vClausesProven ) > 0 ) |
| { |
| int RetValue, k, Beg; |
| int End = -1; // Suppress "might be used uninitialized" |
| int * pStart; |
| // reset the solver |
| if ( p->pSatMain ) sat_solver_delete( p->pSatMain ); |
| p->pSatMain = (sat_solver *)Cnf_DataWriteIntoSolver( p->pCnf, 1, 0 ); |
| if ( p->pSatMain == NULL ) |
| { |
| printf( "Error: Main solver is unsat.\n" ); |
| return -1; |
| } |
| |
| // add the proven clauses |
| Beg = 0; |
| pStart = Vec_IntArray(p->vLitsProven); |
| Vec_IntForEachEntry( p->vClausesProven, End, i ) |
| { |
| assert( End - Beg <= p->nLutSize ); |
| // add the clause to all timeframes |
| RetValue = sat_solver_addclause( p->pSatMain, pStart + Beg, pStart + End ); |
| if ( RetValue == 0 ) |
| { |
| printf( "Error: Solver is UNSAT after adding assumption clauses.\n" ); |
| return -1; |
| } |
| Beg = End; |
| } |
| assert( End == Vec_IntSize(p->vLitsProven) ); |
| |
| // check the clauses |
| Beg = 0; |
| pStart = Vec_IntArray(p->vLits); |
| Vec_IntForEachEntry( p->vClauses, End, i ) |
| { |
| assert( Vec_IntEntry( p->vCosts, i ) >= 0 ); |
| assert( End - Beg <= p->nLutSize ); |
| // check the clause |
| for ( k = Beg; k < End; k++ ) |
| pStart[k] = lit_neg( pStart[k] ); |
| RetValue = sat_solver_solve( p->pSatMain, pStart + Beg, pStart + End, (ABC_INT64_T)p->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); |
| for ( k = Beg; k < End; k++ ) |
| pStart[k] = lit_neg( pStart[k] ); |
| // the clause holds |
| if ( RetValue == l_False ) |
| { |
| Vec_IntWriteEntry( p->vCosts, i, -1 ); |
| p->nClauses--; |
| } |
| Beg = End; |
| } |
| assert( End == Vec_IntSize(p->vLits) ); |
| if ( p->fVerbose ) |
| printf( "Already proved clauses filtered out %d candidate clauses (out of %d).\n", |
| Vec_IntSize(p->vClauses) - p->nClauses, Vec_IntSize(p->vClauses) ); |
| } |
| |
| p->fFiltering = 0; |
| if ( p->nClauses > p->nClausesMax ) |
| { |
| Fra_ClausSelectClauses( p ); |
| p->fFiltering = 1; |
| } |
| return 1; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Converts AIG into the SAT solver.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Fra_ClausBmcClauses( Clu_Man_t * p ) |
| { |
| int * pStart, nLitsTot, RetValue, Beg, End, Counter, i, k, f; |
| /* |
| for ( i = 0; i < Vec_IntSize(p->vLits); i++ ) |
| printf( "%d ", p->vLits->pArray[i] ); |
| printf( "\n" ); |
| */ |
| // add the clauses |
| Counter = 0; |
| // skip through the prefix variables |
| if ( p->nPref ) |
| { |
| nLitsTot = p->nPref * 2 * p->pCnf->nVars; |
| for ( i = 0; i < Vec_IntSize(p->vLits); i++ ) |
| p->vLits->pArray[i] += nLitsTot; |
| } |
| // go through the timeframes |
| nLitsTot = 2 * p->pCnf->nVars; |
| pStart = Vec_IntArray(p->vLits); |
| for ( f = 0; f < p->nFrames; f++ ) |
| { |
| Beg = 0; |
| Vec_IntForEachEntry( p->vClauses, End, i ) |
| { |
| if ( Vec_IntEntry( p->vCosts, i ) == -1 ) |
| { |
| Beg = End; |
| continue; |
| } |
| assert( Vec_IntEntry( p->vCosts, i ) > 0 ); |
| assert( End - Beg <= p->nLutSize ); |
| |
| for ( k = Beg; k < End; k++ ) |
| pStart[k] = lit_neg( pStart[k] ); |
| RetValue = sat_solver_solve( p->pSatBmc, pStart + Beg, pStart + End, (ABC_INT64_T)p->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); |
| for ( k = Beg; k < End; k++ ) |
| pStart[k] = lit_neg( pStart[k] ); |
| |
| if ( RetValue != l_False ) |
| { |
| Beg = End; |
| Vec_IntWriteEntry( p->vCosts, i, -1 ); |
| Counter++; |
| continue; |
| } |
| /* |
| // add the clause |
| RetValue = sat_solver_addclause( p->pSatBmc, pStart + Beg, pStart + End ); |
| // assert( RetValue == 1 ); |
| if ( RetValue == 0 ) |
| { |
| printf( "Error: Solver is UNSAT after adding BMC clauses.\n" ); |
| return -1; |
| } |
| */ |
| Beg = End; |
| |
| // simplify the solver |
| if ( p->pSatBmc->qtail != p->pSatBmc->qhead ) |
| { |
| RetValue = sat_solver_simplify(p->pSatBmc); |
| assert( RetValue != 0 ); |
| assert( p->pSatBmc->qtail == p->pSatBmc->qhead ); |
| } |
| } |
| // increment literals |
| for ( i = 0; i < Vec_IntSize(p->vLits); i++ ) |
| p->vLits->pArray[i] += nLitsTot; |
| } |
| |
| // return clauses back to normal |
| nLitsTot = (p->nPref + p->nFrames) * nLitsTot; |
| for ( i = 0; i < Vec_IntSize(p->vLits); i++ ) |
| p->vLits->pArray[i] -= nLitsTot; |
| /* |
| for ( i = 0; i < Vec_IntSize(p->vLits); i++ ) |
| printf( "%d ", p->vLits->pArray[i] ); |
| printf( "\n" ); |
| */ |
| return Counter; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Cleans simulation info.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Fra_ClausSimInfoClean( Clu_Man_t * p ) |
| { |
| assert( p->pCnf->nVars <= Vec_PtrSize(p->vCexes) ); |
| Vec_PtrCleanSimInfo( p->vCexes, 0, p->nCexesAlloc/32 ); |
| p->nCexes = 0; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Reallocs simulation info.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Fra_ClausSimInfoRealloc( Clu_Man_t * p ) |
| { |
| assert( p->nCexes == p->nCexesAlloc ); |
| Vec_PtrReallocSimInfo( p->vCexes ); |
| Vec_PtrCleanSimInfo( p->vCexes, p->nCexesAlloc/32, 2 * p->nCexesAlloc/32 ); |
| p->nCexesAlloc *= 2; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Records simulation info.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Fra_ClausSimInfoRecord( Clu_Man_t * p, int * pModel ) |
| { |
| int i; |
| if ( p->nCexes == p->nCexesAlloc ) |
| Fra_ClausSimInfoRealloc( p ); |
| assert( p->nCexes < p->nCexesAlloc ); |
| for ( i = 0; i < p->pCnf->nVars; i++ ) |
| { |
| if ( pModel[i] == l_True ) |
| { |
| assert( Abc_InfoHasBit( (unsigned *)Vec_PtrEntry(p->vCexes, i), p->nCexes ) == 0 ); |
| Abc_InfoSetBit( (unsigned *)Vec_PtrEntry(p->vCexes, i), p->nCexes ); |
| } |
| } |
| p->nCexes++; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Uses the simulation info.] |
| |
| Description [Returns 1 if the simulation info disproved the clause.] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Fra_ClausSimInfoCheck( Clu_Man_t * p, int * pLits, int nLits ) |
| { |
| unsigned * pSims[16], uWord; |
| int nWords, iVar, i, w; |
| for ( i = 0; i < nLits; i++ ) |
| { |
| iVar = lit_var(pLits[i]) - p->nFrames * p->pCnf->nVars; |
| assert( iVar > 0 && iVar < p->pCnf->nVars ); |
| pSims[i] = (unsigned *)Vec_PtrEntry( p->vCexes, iVar ); |
| } |
| nWords = p->nCexes / 32; |
| for ( w = 0; w < nWords; w++ ) |
| { |
| uWord = ~(unsigned)0; |
| for ( i = 0; i < nLits; i++ ) |
| uWord &= (lit_sign(pLits[i])? pSims[i][w] : ~pSims[i][w]); |
| if ( uWord ) |
| return 1; |
| } |
| if ( p->nCexes % 32 ) |
| { |
| uWord = ~(unsigned)0; |
| for ( i = 0; i < nLits; i++ ) |
| uWord &= (lit_sign(pLits[i])? pSims[i][w] : ~pSims[i][w]); |
| if ( uWord & Abc_InfoMask( p->nCexes % 32 ) ) |
| return 1; |
| } |
| return 0; |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Converts AIG into the SAT solver.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Fra_ClausInductiveClauses( Clu_Man_t * p ) |
| { |
| // Aig_Obj_t * pObjLi, * pObjLo; |
| int * pStart, nLitsTot, RetValue, Beg, End, Counter, i, k, f, fFlag;//, Lits[2]; |
| p->fFail = 0; |
| |
| // reset the solver |
| if ( p->pSatMain ) sat_solver_delete( p->pSatMain ); |
| p->pSatMain = (sat_solver *)Cnf_DataWriteIntoSolver( p->pCnf, p->nFrames+1, 0 ); |
| if ( p->pSatMain == NULL ) |
| { |
| printf( "Error: Main solver is unsat.\n" ); |
| return -1; |
| } |
| Fra_ClausSimInfoClean( p ); |
| |
| /* |
| // check if the property holds |
| if ( Fra_ClausRunSat0( p ) ) |
| printf( "Property holds without strengthening.\n" ); |
| else |
| printf( "Property does not hold without strengthening.\n" ); |
| */ |
| /* |
| // add constant registers |
| Aig_ManForEachLiLoSeq( p->pAig, pObjLi, pObjLo, i ) |
| if ( Aig_ObjFanin0(pObjLi) == Aig_ManConst1(p->pAig) ) |
| { |
| for ( k = 0; k < p->nFrames; k++ ) |
| { |
| Lits[0] = k * 2 * p->pCnf->nVars + toLitCond( p->pCnf->pVarNums[pObjLo->Id], Aig_ObjFaninC0(pObjLi) ); |
| RetValue = sat_solver_addclause( p->pSatMain, Lits, Lits + 1 ); |
| if ( RetValue == 0 ) |
| { |
| printf( "Error: Solver is UNSAT after adding constant-register clauses.\n" ); |
| return -1; |
| } |
| } |
| } |
| */ |
| |
| |
| // add the proven clauses |
| nLitsTot = 2 * p->pCnf->nVars; |
| pStart = Vec_IntArray(p->vLitsProven); |
| for ( f = 0; f < p->nFrames; f++ ) |
| { |
| Beg = 0; |
| Vec_IntForEachEntry( p->vClausesProven, End, i ) |
| { |
| assert( End - Beg <= p->nLutSize ); |
| // add the clause to all timeframes |
| RetValue = sat_solver_addclause( p->pSatMain, pStart + Beg, pStart + End ); |
| if ( RetValue == 0 ) |
| { |
| printf( "Error: Solver is UNSAT after adding assumption clauses.\n" ); |
| return -1; |
| } |
| Beg = End; |
| } |
| // increment literals |
| for ( i = 0; i < Vec_IntSize(p->vLitsProven); i++ ) |
| p->vLitsProven->pArray[i] += nLitsTot; |
| } |
| // return clauses back to normal |
| nLitsTot = (p->nFrames) * nLitsTot; |
| for ( i = 0; i < Vec_IntSize(p->vLitsProven); i++ ) |
| p->vLitsProven->pArray[i] -= nLitsTot; |
| |
| /* |
| // add the proven clauses |
| nLitsTot = 2 * p->pCnf->nVars; |
| pStart = Vec_IntArray(p->vLitsProven); |
| Beg = 0; |
| Vec_IntForEachEntry( p->vClausesProven, End, i ) |
| { |
| assert( End - Beg <= p->nLutSize ); |
| // add the clause to all timeframes |
| RetValue = sat_solver_addclause( p->pSatMain, pStart + Beg, pStart + End ); |
| if ( RetValue == 0 ) |
| { |
| printf( "Error: Solver is UNSAT after adding assumption clauses.\n" ); |
| return -1; |
| } |
| Beg = End; |
| } |
| */ |
| |
| // add the clauses |
| nLitsTot = 2 * p->pCnf->nVars; |
| pStart = Vec_IntArray(p->vLits); |
| for ( f = 0; f < p->nFrames; f++ ) |
| { |
| Beg = 0; |
| Vec_IntForEachEntry( p->vClauses, End, i ) |
| { |
| if ( Vec_IntEntry( p->vCosts, i ) == -1 ) |
| { |
| Beg = End; |
| continue; |
| } |
| assert( Vec_IntEntry( p->vCosts, i ) > 0 ); |
| assert( End - Beg <= p->nLutSize ); |
| // add the clause to all timeframes |
| RetValue = sat_solver_addclause( p->pSatMain, pStart + Beg, pStart + End ); |
| if ( RetValue == 0 ) |
| { |
| printf( "Error: Solver is UNSAT after adding assumption clauses.\n" ); |
| return -1; |
| } |
| Beg = End; |
| } |
| // increment literals |
| for ( i = 0; i < Vec_IntSize(p->vLits); i++ ) |
| p->vLits->pArray[i] += nLitsTot; |
| } |
| |
| // simplify the solver |
| if ( p->pSatMain->qtail != p->pSatMain->qhead ) |
| { |
| RetValue = sat_solver_simplify(p->pSatMain); |
| assert( RetValue != 0 ); |
| assert( p->pSatMain->qtail == p->pSatMain->qhead ); |
| } |
| |
| // check if the property holds |
| if ( p->fTarget ) |
| { |
| if ( Fra_ClausRunSat0( p ) ) |
| { |
| if ( p->fVerbose ) |
| printf( " Property holds. " ); |
| } |
| else |
| { |
| if ( p->fVerbose ) |
| printf( " Property fails. " ); |
| // return -2; |
| p->fFail = 1; |
| } |
| } |
| |
| /* |
| // add the property for the first K frames |
| for ( i = 0; i < p->nFrames; i++ ) |
| { |
| Aig_Obj_t * pObj; |
| int Lits[2]; |
| // set the output literals |
| pObj = Aig_ManCo(p->pAig, 0); |
| Lits[0] = i * nLitsTot + toLitCond( p->pCnf->pVarNums[pObj->Id], 1 ); |
| // add the clause |
| RetValue = sat_solver_addclause( p->pSatMain, Lits, Lits + 1 ); |
| // assert( RetValue == 1 ); |
| if ( RetValue == 0 ) |
| { |
| printf( "Error: Solver is UNSAT after adding property for the first K frames.\n" ); |
| return -1; |
| } |
| } |
| */ |
| |
| // simplify the solver |
| if ( p->pSatMain->qtail != p->pSatMain->qhead ) |
| { |
| RetValue = sat_solver_simplify(p->pSatMain); |
| assert( RetValue != 0 ); |
| assert( p->pSatMain->qtail == p->pSatMain->qhead ); |
| } |
| |
| |
| // check the clause in the last timeframe |
| Beg = 0; |
| Counter = 0; |
| Vec_IntForEachEntry( p->vClauses, End, i ) |
| { |
| if ( Vec_IntEntry( p->vCosts, i ) == -1 ) |
| { |
| Beg = End; |
| continue; |
| } |
| assert( Vec_IntEntry( p->vCosts, i ) > 0 ); |
| assert( End - Beg <= p->nLutSize ); |
| |
| if ( Fra_ClausSimInfoCheck(p, pStart + Beg, End - Beg) ) |
| { |
| fFlag = 1; |
| // printf( "s-" ); |
| |
| Beg = End; |
| Vec_IntWriteEntry( p->vCosts, i, -1 ); |
| Counter++; |
| continue; |
| } |
| else |
| { |
| fFlag = 0; |
| // printf( "s?" ); |
| } |
| |
| for ( k = Beg; k < End; k++ ) |
| pStart[k] = lit_neg( pStart[k] ); |
| RetValue = sat_solver_solve( p->pSatMain, pStart + Beg, pStart + End, (ABC_INT64_T)p->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); |
| for ( k = Beg; k < End; k++ ) |
| pStart[k] = lit_neg( pStart[k] ); |
| |
| // the problem is not solved |
| if ( RetValue != l_False ) |
| { |
| // printf( "S- " ); |
| // Fra_ClausSimInfoRecord( p, (int*)p->pSatMain->model.ptr + p->nFrames * p->pCnf->nVars ); |
| Fra_ClausSimInfoRecord( p, (int*)p->pSatMain->model + p->nFrames * p->pCnf->nVars ); |
| // RetValue = Fra_ClausSimInfoCheck(p, pStart + Beg, End - Beg); |
| // assert( RetValue ); |
| |
| Beg = End; |
| Vec_IntWriteEntry( p->vCosts, i, -1 ); |
| Counter++; |
| continue; |
| } |
| // printf( "S+ " ); |
| // assert( !fFlag ); |
| |
| /* |
| // add the clause |
| RetValue = sat_solver_addclause( p->pSatMain, pStart + Beg, pStart + End ); |
| // assert( RetValue == 1 ); |
| if ( RetValue == 0 ) |
| { |
| printf( "Error: Solver is UNSAT after adding proved clauses.\n" ); |
| return -1; |
| } |
| */ |
| Beg = End; |
| |
| // simplify the solver |
| if ( p->pSatMain->qtail != p->pSatMain->qhead ) |
| { |
| RetValue = sat_solver_simplify(p->pSatMain); |
| assert( RetValue != 0 ); |
| assert( p->pSatMain->qtail == p->pSatMain->qhead ); |
| } |
| } |
| |
| // return clauses back to normal |
| nLitsTot = p->nFrames * nLitsTot; |
| for ( i = 0; i < Vec_IntSize(p->vLits); i++ ) |
| p->vLits->pArray[i] -= nLitsTot; |
| |
| // if ( fFail ) |
| // return -2; |
| return Counter; |
| } |
| |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Converts AIG into the SAT solver.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Clu_Man_t * Fra_ClausAlloc( Aig_Man_t * pAig, int nFrames, int nPref, int nClausesMax, int nLutSize, int nLevels, int nCutsMax, int nBatches, int fStepUp, int fTarget, int fVerbose, int fVeryVerbose ) |
| { |
| Clu_Man_t * p; |
| p = ABC_ALLOC( Clu_Man_t, 1 ); |
| memset( p, 0, sizeof(Clu_Man_t) ); |
| p->pAig = pAig; |
| p->nFrames = nFrames; |
| p->nPref = nPref; |
| p->nClausesMax = nClausesMax; |
| p->nLutSize = nLutSize; |
| p->nLevels = nLevels; |
| p->nCutsMax = nCutsMax; |
| p->nBatches = nBatches; |
| p->fStepUp = fStepUp; |
| p->fTarget = fTarget; |
| p->fVerbose = fVerbose; |
| p->fVeryVerbose = fVeryVerbose; |
| p->nSimWords = 512;//1024;//64; |
| p->nSimFrames = 32;//8;//32; |
| p->nSimWordsPref = p->nPref*p->nSimWords/p->nSimFrames; |
| |
| p->vLits = Vec_IntAlloc( 1<<14 ); |
| p->vClauses = Vec_IntAlloc( 1<<12 ); |
| p->vCosts = Vec_IntAlloc( 1<<12 ); |
| |
| p->vLitsProven = Vec_IntAlloc( 1<<14 ); |
| p->vClausesProven= Vec_IntAlloc( 1<<12 ); |
| |
| p->nCexesAlloc = 1024; |
| p->vCexes = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(p->pAig)+1, p->nCexesAlloc/32 ); |
| Vec_PtrCleanSimInfo( p->vCexes, 0, p->nCexesAlloc/32 ); |
| return p; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Converts AIG into the SAT solver.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Fra_ClausFree( Clu_Man_t * p ) |
| { |
| if ( p->vCexes ) Vec_PtrFree( p->vCexes ); |
| if ( p->vLits ) Vec_IntFree( p->vLits ); |
| if ( p->vClauses ) Vec_IntFree( p->vClauses ); |
| if ( p->vLitsProven ) Vec_IntFree( p->vLitsProven ); |
| if ( p->vClausesProven ) Vec_IntFree( p->vClausesProven ); |
| if ( p->vCosts ) Vec_IntFree( p->vCosts ); |
| if ( p->pCnf ) Cnf_DataFree( p->pCnf ); |
| if ( p->pSatMain ) sat_solver_delete( p->pSatMain ); |
| if ( p->pSatBmc ) sat_solver_delete( p->pSatBmc ); |
| ABC_FREE( p ); |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Converts AIG into the SAT solver.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Fra_ClausAddToStorage( Clu_Man_t * p ) |
| { |
| int * pStart; |
| int Beg, End, Counter, i, k; |
| Beg = 0; |
| Counter = 0; |
| pStart = Vec_IntArray( p->vLits ); |
| Vec_IntForEachEntry( p->vClauses, End, i ) |
| { |
| if ( Vec_IntEntry( p->vCosts, i ) == -1 ) |
| { |
| Beg = End; |
| continue; |
| } |
| assert( Vec_IntEntry( p->vCosts, i ) > 0 ); |
| assert( End - Beg <= p->nLutSize ); |
| for ( k = Beg; k < End; k++ ) |
| Vec_IntPush( p->vLitsProven, pStart[k] ); |
| Vec_IntPush( p->vClausesProven, Vec_IntSize(p->vLitsProven) ); |
| Beg = End; |
| Counter++; |
| |
| if ( i < p->nOneHots ) |
| p->nOneHotsProven++; |
| } |
| if ( p->fVerbose ) |
| printf( "Added to storage %d proved clauses (including %d one-hot clauses)\n", Counter, p->nOneHotsProven ); |
| |
| Vec_IntClear( p->vClauses ); |
| Vec_IntClear( p->vLits ); |
| Vec_IntClear( p->vCosts ); |
| p->nClauses = 0; |
| |
| p->fNothingNew = (int)(Counter == 0); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Converts AIG into the SAT solver.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Fra_ClausPrintIndClauses( Clu_Man_t * p ) |
| { |
| int Counters[9] = {0}; |
| int * pStart; |
| int Beg, End, i; |
| Beg = 0; |
| pStart = Vec_IntArray( p->vLitsProven ); |
| Vec_IntForEachEntry( p->vClausesProven, End, i ) |
| { |
| if ( End - Beg >= 8 ) |
| Counters[8]++; |
| else |
| Counters[End - Beg]++; |
| //printf( "%d ", End-Beg ); |
| Beg = End; |
| } |
| printf( "SUMMARY: Total proved clauses = %d. ", Vec_IntSize(p->vClausesProven) ); |
| printf( "Clause per lit: " ); |
| for ( i = 0; i < 8; i++ ) |
| if ( Counters[i] ) |
| printf( "%d=%d ", i, Counters[i] ); |
| if ( Counters[8] ) |
| printf( ">7=%d ", Counters[8] ); |
| printf( "\n" ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Writes the clauses into an AIGER file.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Aig_Obj_t * Fra_ClausGetLiteral( Clu_Man_t * p, int * pVar2Id, int Lit ) |
| { |
| Aig_Obj_t * pLiteral; |
| int NodeId = pVar2Id[ lit_var(Lit) ]; |
| assert( NodeId >= 0 ); |
| pLiteral = (Aig_Obj_t *)Aig_ManObj( p->pAig, NodeId )->pData; |
| return Aig_NotCond( pLiteral, lit_sign(Lit) ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Writes the clauses into an AIGER file.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Fra_ClausWriteIndClauses( Clu_Man_t * p ) |
| { |
| extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact ); |
| Aig_Man_t * pNew; |
| Aig_Obj_t * pClause, * pLiteral; |
| char * pName; |
| int * pStart, * pVar2Id; |
| int Beg, End, i, k; |
| // create mapping from SAT vars to node IDs |
| pVar2Id = ABC_ALLOC( int, p->pCnf->nVars ); |
| memset( pVar2Id, 0xFF, sizeof(int) * p->pCnf->nVars ); |
| for ( i = 0; i < Aig_ManObjNumMax(p->pAig); i++ ) |
| if ( p->pCnf->pVarNums[i] >= 0 ) |
| { |
| assert( p->pCnf->pVarNums[i] < p->pCnf->nVars ); |
| pVar2Id[ p->pCnf->pVarNums[i] ] = i; |
| } |
| // start the manager |
| pNew = Aig_ManDupWithoutPos( p->pAig ); |
| // add the clauses |
| Beg = 0; |
| pStart = Vec_IntArray( p->vLitsProven ); |
| Vec_IntForEachEntry( p->vClausesProven, End, i ) |
| { |
| pClause = Fra_ClausGetLiteral( p, pVar2Id, pStart[Beg] ); |
| for ( k = Beg + 1; k < End; k++ ) |
| { |
| pLiteral = Fra_ClausGetLiteral( p, pVar2Id, pStart[k] ); |
| pClause = Aig_Or( pNew, pClause, pLiteral ); |
| } |
| Aig_ObjCreateCo( pNew, pClause ); |
| Beg = End; |
| } |
| ABC_FREE( pVar2Id ); |
| Aig_ManCleanup( pNew ); |
| pName = Ioa_FileNameGenericAppend( p->pAig->pName, "_care.aig" ); |
| printf( "Care one-hotness clauses will be written into file \"%s\".\n", pName ); |
| Ioa_WriteAiger( pNew, pName, 0, 1 ); |
| Aig_ManStop( pNew ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Checks if the clause holds using the given simulation info.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Fra_ClausEstimateCoverageOne( Fra_Sml_t * pSim, int * pLits, int nLits, int * pVar2Id, unsigned * pResult ) |
| { |
| unsigned * pSims[16]; |
| int iVar, i, w; |
| for ( i = 0; i < nLits; i++ ) |
| { |
| iVar = lit_var(pLits[i]); |
| pSims[i] = Fra_ObjSim( pSim, pVar2Id[iVar] ); |
| } |
| for ( w = 0; w < pSim->nWordsTotal; w++ ) |
| { |
| pResult[w] = ~(unsigned)0; |
| for ( i = 0; i < nLits; i++ ) |
| pResult[w] &= (lit_sign(pLits[i])? pSims[i][w] : ~pSims[i][w]); |
| } |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Estimates the coverage of state space by clauses.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Fra_ClausEstimateCoverage( Clu_Man_t * p ) |
| { |
| int nCombSimWords = (1<<11); |
| Fra_Sml_t * pComb; |
| unsigned * pResultTot, * pResultOne; |
| int nCovered, Beg, End, i, w; |
| int * pStart, * pVar2Id; |
| abctime clk = Abc_Clock(); |
| // simulate the circuit with nCombSimWords * 32 = 64K patterns |
| // srand( 0xAABBAABB ); |
| Aig_ManRandom(1); |
| pComb = Fra_SmlSimulateComb( p->pAig, nCombSimWords, 0 ); |
| // create mapping from SAT vars to node IDs |
| pVar2Id = ABC_ALLOC( int, p->pCnf->nVars ); |
| memset( pVar2Id, 0, sizeof(int) * p->pCnf->nVars ); |
| for ( i = 0; i < Aig_ManObjNumMax(p->pAig); i++ ) |
| if ( p->pCnf->pVarNums[i] >= 0 ) |
| { |
| assert( p->pCnf->pVarNums[i] < p->pCnf->nVars ); |
| pVar2Id[ p->pCnf->pVarNums[i] ] = i; |
| } |
| // get storage for one assignment and all assignments |
| assert( Aig_ManCoNum(p->pAig) > 2 ); |
| pResultOne = Fra_ObjSim( pComb, Aig_ManCo(p->pAig, 0)->Id ); |
| pResultTot = Fra_ObjSim( pComb, Aig_ManCo(p->pAig, 1)->Id ); |
| // start the OR of don't-cares |
| for ( w = 0; w < nCombSimWords; w++ ) |
| pResultTot[w] = 0; |
| // check clauses |
| Beg = 0; |
| pStart = Vec_IntArray( p->vLitsProven ); |
| Vec_IntForEachEntry( p->vClausesProven, End, i ) |
| { |
| Fra_ClausEstimateCoverageOne( pComb, pStart + Beg, End-Beg, pVar2Id, pResultOne ); |
| Beg = End; |
| for ( w = 0; w < nCombSimWords; w++ ) |
| pResultTot[w] |= pResultOne[w]; |
| } |
| // count the total number of patterns contained in the don't-care |
| nCovered = 0; |
| for ( w = 0; w < nCombSimWords; w++ ) |
| nCovered += Aig_WordCountOnes( pResultTot[w] ); |
| Fra_SmlStop( pComb ); |
| ABC_FREE( pVar2Id ); |
| // print the result |
| printf( "Care states ratio = %f. ", 1.0 * (nCombSimWords * 32 - nCovered) / (nCombSimWords * 32) ); |
| printf( "(%d out of %d patterns) ", nCombSimWords * 32 - nCovered, nCombSimWords * 32 ); |
| ABC_PRT( "Time", Abc_Clock() - clk ); |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Converts AIG into the SAT solver.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Fra_Claus( Aig_Man_t * pAig, int nFrames, int nPref, int nClausesMax, int nLutSize, int nLevels, int nCutsMax, int nBatches, int fStepUp, int fBmc, int fRefs, int fTarget, int fVerbose, int fVeryVerbose ) |
| { |
| Clu_Man_t * p; |
| abctime clk, clkTotal = Abc_Clock(), clkInd; |
| int b, Iter, Counter, nPrefOld; |
| int nClausesBeg = 0; |
| |
| // create the manager |
| p = Fra_ClausAlloc( pAig, nFrames, nPref, nClausesMax, nLutSize, nLevels, nCutsMax, nBatches, fStepUp, fTarget, fVerbose, fVeryVerbose ); |
| if ( p->fVerbose ) |
| { |
| printf( "PARAMETERS: Frames = %d. Pref = %d. Clauses max = %d. Cut size = %d.\n", nFrames, nPref, nClausesMax, nLutSize ); |
| printf( "Level max = %d. Cuts max = %d. Batches = %d. Increment cut size = %s.\n", nLevels, nCutsMax, nBatches, fStepUp? "yes":"no" ); |
| //ABC_PRT( "Sim-seq", Abc_Clock() - clk ); |
| } |
| |
| assert( !p->fTarget || Aig_ManCoNum(pAig) - Aig_ManRegNum(pAig) == 1 ); |
| |
| clk = Abc_Clock(); |
| // derive CNF |
| // if ( p->fTarget ) |
| // p->pAig->nRegs++; |
| p->pCnf = Cnf_DeriveSimple( p->pAig, Aig_ManCoNum(p->pAig) ); |
| // if ( p->fTarget ) |
| // p->pAig->nRegs--; |
| if ( fVerbose ) |
| { |
| //ABC_PRT( "CNF ", Abc_Clock() - clk ); |
| } |
| |
| // check BMC |
| clk = Abc_Clock(); |
| p->pSatBmc = (sat_solver *)Cnf_DataWriteIntoSolver( p->pCnf, p->nPref + p->nFrames, 1 ); |
| if ( p->pSatBmc == NULL ) |
| { |
| printf( "Error: BMC solver is unsat.\n" ); |
| Fra_ClausFree( p ); |
| return 1; |
| } |
| if ( p->fTarget && !Fra_ClausRunBmc( p ) ) |
| { |
| printf( "Problem fails the base case after %d frame expansion.\n", p->nPref + p->nFrames ); |
| Fra_ClausFree( p ); |
| return 1; |
| } |
| if ( fVerbose ) |
| { |
| //ABC_PRT( "SAT-bmc", Abc_Clock() - clk ); |
| } |
| |
| // start the SAT solver |
| clk = Abc_Clock(); |
| p->pSatMain = (sat_solver *)Cnf_DataWriteIntoSolver( p->pCnf, p->nFrames+1, 0 ); |
| if ( p->pSatMain == NULL ) |
| { |
| printf( "Error: Main solver is unsat.\n" ); |
| Fra_ClausFree( p ); |
| return 1; |
| } |
| |
| |
| for ( b = 0; b < p->nBatches; b++ ) |
| { |
| // if ( fVerbose ) |
| printf( "*** BATCH %d: ", b+1 ); |
| if ( b && p->nLutSize < 12 && (!p->fFiltering || p->fNothingNew || p->fStepUp) ) |
| p->nLutSize++; |
| printf( "Using %d-cuts.\n", p->nLutSize ); |
| |
| // try solving without additional clauses |
| if ( p->fTarget && Fra_ClausRunSat( p ) ) |
| { |
| printf( "Problem is inductive without strengthening.\n" ); |
| Fra_ClausFree( p ); |
| return 1; |
| } |
| if ( fVerbose ) |
| { |
| // ABC_PRT( "SAT-ind", Abc_Clock() - clk ); |
| } |
| |
| // collect the candidate inductive clauses using 4-cuts |
| clk = Abc_Clock(); |
| nPrefOld = p->nPref; p->nPref = 0; p->nSimWordsPref = 0; |
| // Fra_ClausProcessClauses( p, fRefs ); |
| Fra_ClausProcessClauses2( p, fRefs ); |
| p->nPref = nPrefOld; |
| p->nSimWordsPref = p->nPref*p->nSimWords/p->nSimFrames; |
| nClausesBeg = p->nClauses; |
| |
| //ABC_PRT( "Clauses", Abc_Clock() - clk ); |
| |
| |
| // check clauses using BMC |
| if ( fBmc ) |
| { |
| clk = Abc_Clock(); |
| Counter = Fra_ClausBmcClauses( p ); |
| p->nClauses -= Counter; |
| if ( fVerbose ) |
| { |
| printf( "BMC disproved %d clauses. ", Counter ); |
| ABC_PRT( "Time", Abc_Clock() - clk ); |
| } |
| } |
| |
| |
| // prove clauses inductively |
| clkInd = clk = Abc_Clock(); |
| Counter = 1; |
| for ( Iter = 0; Counter > 0; Iter++ ) |
| { |
| if ( fVerbose ) |
| printf( "Iter %3d : Begin = %5d. ", Iter, p->nClauses ); |
| Counter = Fra_ClausInductiveClauses( p ); |
| if ( Counter > 0 ) |
| p->nClauses -= Counter; |
| if ( fVerbose ) |
| { |
| printf( "End = %5d. Exs = %5d. ", p->nClauses, p->nCexes ); |
| // printf( "\n" ); |
| ABC_PRT( "Time", Abc_Clock() - clk ); |
| } |
| clk = Abc_Clock(); |
| } |
| // add proved clauses to storage |
| Fra_ClausAddToStorage( p ); |
| // report the results |
| if ( p->fTarget ) |
| { |
| if ( Counter == -1 ) |
| printf( "Fra_Claus(): Internal error. " ); |
| else if ( p->fFail ) |
| printf( "Property FAILS during refinement. " ); |
| else |
| printf( "Property HOLDS inductively after strengthening. " ); |
| ABC_PRT( "Time ", Abc_Clock() - clkTotal ); |
| if ( !p->fFail ) |
| break; |
| } |
| else |
| { |
| printf( "Finished proving inductive clauses. " ); |
| ABC_PRT( "Time ", Abc_Clock() - clkTotal ); |
| } |
| } |
| |
| // verify the computed interpolant |
| Fra_InvariantVerify( pAig, nFrames, p->vClausesProven, p->vLitsProven ); |
| // printf( "THIS COMMAND IS KNOWN TO HAVE A BUG!\n" ); |
| |
| // if ( !p->fTarget && p->fVerbose ) |
| if ( p->fVerbose ) |
| { |
| Fra_ClausPrintIndClauses( p ); |
| Fra_ClausEstimateCoverage( p ); |
| } |
| |
| if ( !p->fTarget ) |
| { |
| Fra_ClausWriteIndClauses( p ); |
| } |
| /* |
| // print the statistic into a file |
| { |
| FILE * pTable; |
| assert( p->nBatches == 1 ); |
| pTable = fopen( "stats.txt", "a+" ); |
| fprintf( pTable, "%s ", pAig->pName ); |
| fprintf( pTable, "%d ", Aig_ManCiNum(pAig)-Aig_ManRegNum(pAig) ); |
| fprintf( pTable, "%d ", Aig_ManCoNum(pAig)-Aig_ManRegNum(pAig) ); |
| fprintf( pTable, "%d ", Aig_ManRegNum(pAig) ); |
| fprintf( pTable, "%d ", Aig_ManNodeNum(pAig) ); |
| fprintf( pTable, "%d ", p->nCuts ); |
| fprintf( pTable, "%d ", nClausesBeg ); |
| fprintf( pTable, "%d ", p->nClauses ); |
| fprintf( pTable, "%d ", Iter ); |
| fprintf( pTable, "%.2f ", (float)(clkInd-clkTotal)/(float)(CLOCKS_PER_SEC) ); |
| fprintf( pTable, "%.2f ", (float)(Abc_Clock()-clkInd)/(float)(CLOCKS_PER_SEC) ); |
| fprintf( pTable, "%.2f ", (float)(Abc_Clock()-clkTotal)/(float)(CLOCKS_PER_SEC) ); |
| fprintf( pTable, "\n" ); |
| fclose( pTable ); |
| } |
| */ |
| // clean the manager |
| Fra_ClausFree( p ); |
| return 1; |
| } |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
