| /**CFile**************************************************************** |
| |
| FileName [fraInd.c] |
| |
| SystemName [ABC: Logic synthesis and verification system.] |
| |
| PackageName [New FRAIG package.] |
| |
| Synopsis [Inductive prover.] |
| |
| Author [Alan Mishchenko] |
| |
| Affiliation [UC Berkeley] |
| |
| Date [Ver. 1.0. Started - June 30, 2007.] |
| |
| Revision [$Id: fraInd.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $] |
| |
| ***********************************************************************/ |
| |
| #include "fra.h" |
| #include "sat/cnf/cnf.h" |
| #include "opt/dar/dar.h" |
| #include "aig/saig/saig.h" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// DECLARATIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// FUNCTION DEFINITIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| /**Function************************************************************* |
| |
| Synopsis [Performs AIG rewriting on the constraint manager.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Fra_FraigInductionRewrite( Fra_Man_t * p ) |
| { |
| Aig_Man_t * pTemp; |
| Aig_Obj_t * pObj, * pObjPo; |
| int nTruePis, k, i; |
| abctime clk = Abc_Clock(); |
| // perform AIG rewriting on the speculated frames |
| // pTemp = Dar_ManRwsat( pTemp, 1, 0 ); |
| pTemp = Dar_ManRewriteDefault( p->pManFraig ); |
| // printf( "Before = %6d. After = %6d.\n", Aig_ManNodeNum(p->pManFraig), Aig_ManNodeNum(pTemp) ); |
| //Aig_ManDumpBlif( p->pManFraig, "1.blif", NULL, NULL ); |
| //Aig_ManDumpBlif( pTemp, "2.blif", NULL, NULL ); |
| // Fra_FramesWriteCone( pTemp ); |
| // Aig_ManStop( pTemp ); |
| // transfer PI/register pointers |
| assert( p->pManFraig->nRegs == pTemp->nRegs ); |
| assert( p->pManFraig->nAsserts == pTemp->nAsserts ); |
| nTruePis = Aig_ManCiNum(p->pManAig) - Aig_ManRegNum(p->pManAig); |
| memset( p->pMemFraig, 0, sizeof(Aig_Obj_t *) * p->nSizeAlloc * p->nFramesAll ); |
| Fra_ObjSetFraig( Aig_ManConst1(p->pManAig), p->pPars->nFramesK, Aig_ManConst1(pTemp) ); |
| Aig_ManForEachPiSeq( p->pManAig, pObj, i ) |
| Fra_ObjSetFraig( pObj, p->pPars->nFramesK, Aig_ManCi(pTemp,nTruePis*p->pPars->nFramesK+i) ); |
| k = 0; |
| assert( Aig_ManRegNum(p->pManAig) == Aig_ManCoNum(pTemp) - pTemp->nAsserts ); |
| Aig_ManForEachLoSeq( p->pManAig, pObj, i ) |
| { |
| pObjPo = Aig_ManCo(pTemp, pTemp->nAsserts + k++); |
| Fra_ObjSetFraig( pObj, p->pPars->nFramesK, Aig_ObjChild0(pObjPo) ); |
| } |
| // exchange |
| Aig_ManStop( p->pManFraig ); |
| p->pManFraig = pTemp; |
| p->timeRwr += Abc_Clock() - clk; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Performs speculative reduction for one node.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| static inline void Fra_FramesConstrainNode( Aig_Man_t * pManFraig, Aig_Obj_t * pObj, int iFrame ) |
| { |
| Aig_Obj_t * pObjNew, * pObjNew2, * pObjRepr, * pObjReprNew, * pMiter; |
| // skip nodes without representative |
| if ( (pObjRepr = Fra_ClassObjRepr(pObj)) == NULL ) |
| return; |
| assert( pObjRepr->Id < pObj->Id ); |
| // get the new node |
| pObjNew = Fra_ObjFraig( pObj, iFrame ); |
| // get the new node of the representative |
| pObjReprNew = Fra_ObjFraig( pObjRepr, iFrame ); |
| // if this is the same node, no need to add constraints |
| if ( Aig_Regular(pObjNew) == Aig_Regular(pObjReprNew) ) |
| return; |
| // these are different nodes - perform speculative reduction |
| pObjNew2 = Aig_NotCond( pObjReprNew, pObj->fPhase ^ pObjRepr->fPhase ); |
| // set the new node |
| Fra_ObjSetFraig( pObj, iFrame, pObjNew2 ); |
| // add the constraint |
| pMiter = Aig_Exor( pManFraig, pObjNew, pObjReprNew ); |
| pMiter = Aig_NotCond( pMiter, !Aig_ObjPhaseReal(pMiter) ); |
| assert( Aig_ObjPhaseReal(pMiter) == 1 ); |
| Aig_ObjCreateCo( pManFraig, pMiter ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Prepares the inductive case with speculative reduction.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p ) |
| { |
| Aig_Man_t * pManFraig; |
| Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjNew; |
| int i, k, f; |
| assert( p->pManFraig == NULL ); |
| assert( Aig_ManRegNum(p->pManAig) > 0 ); |
| assert( Aig_ManRegNum(p->pManAig) < Aig_ManCiNum(p->pManAig) ); |
| |
| // start the fraig package |
| pManFraig = Aig_ManStart( Aig_ManObjNumMax(p->pManAig) * p->nFramesAll ); |
| pManFraig->pName = Abc_UtilStrsav( p->pManAig->pName ); |
| pManFraig->pSpec = Abc_UtilStrsav( p->pManAig->pSpec ); |
| pManFraig->nRegs = p->pManAig->nRegs; |
| // create PI nodes for the frames |
| for ( f = 0; f < p->nFramesAll; f++ ) |
| Fra_ObjSetFraig( Aig_ManConst1(p->pManAig), f, Aig_ManConst1(pManFraig) ); |
| for ( f = 0; f < p->nFramesAll; f++ ) |
| Aig_ManForEachPiSeq( p->pManAig, pObj, i ) |
| Fra_ObjSetFraig( pObj, f, Aig_ObjCreateCi(pManFraig) ); |
| // create latches for the first frame |
| Aig_ManForEachLoSeq( p->pManAig, pObj, i ) |
| Fra_ObjSetFraig( pObj, 0, Aig_ObjCreateCi(pManFraig) ); |
| |
| // add timeframes |
| // pManFraig->fAddStrash = 1; |
| for ( f = 0; f < p->nFramesAll - 1; f++ ) |
| { |
| // set the constraints on the latch outputs |
| Aig_ManForEachLoSeq( p->pManAig, pObj, i ) |
| Fra_FramesConstrainNode( pManFraig, pObj, f ); |
| // add internal nodes of this frame |
| Aig_ManForEachNode( p->pManAig, pObj, i ) |
| { |
| pObjNew = Aig_And( pManFraig, Fra_ObjChild0Fra(pObj,f), Fra_ObjChild1Fra(pObj,f) ); |
| Fra_ObjSetFraig( pObj, f, pObjNew ); |
| Fra_FramesConstrainNode( pManFraig, pObj, f ); |
| } |
| // transfer latch input to the latch outputs |
| Aig_ManForEachLiLoSeq( p->pManAig, pObjLi, pObjLo, k ) |
| Fra_ObjSetFraig( pObjLo, f+1, Fra_ObjChild0Fra(pObjLi,f) ); |
| } |
| // pManFraig->fAddStrash = 0; |
| // mark the asserts |
| pManFraig->nAsserts = Aig_ManCoNum(pManFraig); |
| // add the POs for the latch outputs of the last frame |
| Aig_ManForEachLoSeq( p->pManAig, pObj, i ) |
| Aig_ObjCreateCo( pManFraig, Fra_ObjFraig(pObj,p->nFramesAll-1) ); |
| |
| // remove dangling nodes |
| Aig_ManCleanup( pManFraig ); |
| // make sure the satisfying assignment is node assigned |
| assert( pManFraig->pData == NULL ); |
| return pManFraig; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Prepares the inductive case with speculative reduction.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Fra_FramesAddMore( Aig_Man_t * p, int nFrames ) |
| { |
| Aig_Obj_t * pObj, ** pLatches; |
| int i, k, f, nNodesOld; |
| // set copy pointer of each object to point to itself |
| Aig_ManForEachObj( p, pObj, i ) |
| pObj->pData = pObj; |
| // iterate and add objects |
| nNodesOld = Aig_ManObjNumMax(p); |
| pLatches = ABC_ALLOC( Aig_Obj_t *, Aig_ManRegNum(p) ); |
| for ( f = 0; f < nFrames; f++ ) |
| { |
| // clean latch inputs and outputs |
| Aig_ManForEachLiSeq( p, pObj, i ) |
| pObj->pData = NULL; |
| Aig_ManForEachLoSeq( p, pObj, i ) |
| pObj->pData = NULL; |
| // save the latch input values |
| k = 0; |
| Aig_ManForEachLiSeq( p, pObj, i ) |
| { |
| if ( Aig_ObjFanin0(pObj)->pData ) |
| pLatches[k++] = Aig_ObjChild0Copy(pObj); |
| else |
| pLatches[k++] = NULL; |
| } |
| // insert them as the latch output values |
| k = 0; |
| Aig_ManForEachLoSeq( p, pObj, i ) |
| pObj->pData = pLatches[k++]; |
| // create the next time frame of nodes |
| Aig_ManForEachNode( p, pObj, i ) |
| { |
| if ( i > nNodesOld ) |
| break; |
| if ( Aig_ObjFanin0(pObj)->pData && Aig_ObjFanin1(pObj)->pData ) |
| pObj->pData = Aig_And( p, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); |
| else |
| pObj->pData = NULL; |
| } |
| } |
| ABC_FREE( pLatches ); |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Performs partitioned sequential SAT sweepingG.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Aig_Man_t * Fra_FraigInductionPart( Aig_Man_t * pAig, Fra_Ssw_t * pPars ) |
| { |
| int fPrintParts = 0; |
| char Buffer[100]; |
| Aig_Man_t * pTemp, * pNew; |
| Vec_Ptr_t * vResult; |
| Vec_Int_t * vPart; |
| int * pMapBack; |
| int i, nCountPis, nCountRegs; |
| int nClasses, nPartSize, fVerbose; |
| abctime clk = Abc_Clock(); |
| |
| // save parameters |
| nPartSize = pPars->nPartSize; pPars->nPartSize = 0; |
| fVerbose = pPars->fVerbose; pPars->fVerbose = 0; |
| // generate partitions |
| if ( pAig->vClockDoms ) |
| { |
| // divide large clock domains into separate partitions |
| vResult = Vec_PtrAlloc( 100 ); |
| Vec_PtrForEachEntry( Vec_Int_t *, (Vec_Ptr_t *)pAig->vClockDoms, vPart, i ) |
| { |
| if ( nPartSize && Vec_IntSize(vPart) > nPartSize ) |
| Aig_ManPartDivide( vResult, vPart, nPartSize, pPars->nOverSize ); |
| else |
| Vec_PtrPush( vResult, Vec_IntDup(vPart) ); |
| } |
| } |
| else |
| vResult = Aig_ManRegPartitionSimple( pAig, nPartSize, pPars->nOverSize ); |
| // vResult = Aig_ManPartitionSmartRegisters( pAig, nPartSize, 0 ); |
| // vResult = Aig_ManRegPartitionSmart( pAig, nPartSize ); |
| if ( fPrintParts ) |
| { |
| // print partitions |
| printf( "Simple partitioning. %d partitions are saved:\n", Vec_PtrSize(vResult) ); |
| Vec_PtrForEachEntry( Vec_Int_t *, vResult, vPart, i ) |
| { |
| sprintf( Buffer, "part%03d.aig", i ); |
| pTemp = Aig_ManRegCreatePart( pAig, vPart, &nCountPis, &nCountRegs, NULL ); |
| Ioa_WriteAiger( pTemp, Buffer, 0, 0 ); |
| printf( "part%03d.aig : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d.\n", |
| i, Vec_IntSize(vPart), Aig_ManCiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp) ); |
| Aig_ManStop( pTemp ); |
| } |
| } |
| |
| // perform SSW with partitions |
| Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) ); |
| Vec_PtrForEachEntry( Vec_Int_t *, vResult, vPart, i ) |
| { |
| pTemp = Aig_ManRegCreatePart( pAig, vPart, &nCountPis, &nCountRegs, &pMapBack ); |
| // create the projection of 1-hot registers |
| if ( pAig->vOnehots ) |
| pTemp->vOnehots = Aig_ManRegProjectOnehots( pAig, pTemp, pAig->vOnehots, fVerbose ); |
| // run SSW |
| pNew = Fra_FraigInduction( pTemp, pPars ); |
| nClasses = Aig_TransferMappedClasses( pAig, pTemp, pMapBack ); |
| if ( fVerbose ) |
| printf( "%3d : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d. It = %3d. Cl = %5d.\n", |
| i, Vec_IntSize(vPart), Aig_ManCiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp), pPars->nIters, nClasses ); |
| Aig_ManStop( pNew ); |
| Aig_ManStop( pTemp ); |
| ABC_FREE( pMapBack ); |
| } |
| // remap the AIG |
| pNew = Aig_ManDupRepr( pAig, 0 ); |
| Aig_ManSeqCleanup( pNew ); |
| // Aig_ManPrintStats( pAig ); |
| // Aig_ManPrintStats( pNew ); |
| Vec_VecFree( (Vec_Vec_t *)vResult ); |
| pPars->nPartSize = nPartSize; |
| pPars->fVerbose = fVerbose; |
| if ( fVerbose ) |
| { |
| ABC_PRT( "Total time", Abc_Clock() - clk ); |
| } |
| return pNew; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Performs sequential SAT sweeping.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, Fra_Ssw_t * pParams ) |
| { |
| int fUseSimpleCnf = 0; |
| int fUseOldSimulation = 0; |
| // other paramaters affecting performance |
| // - presence of FRAIGing in Abc_NtkDarSeqSweep() |
| // - using distance-1 patterns in Fra_SmlAssignDist1() |
| // - the number of simulation patterns |
| // - the number of BMC frames |
| |
| Fra_Man_t * p; |
| Fra_Par_t Pars, * pPars = &Pars; |
| Aig_Obj_t * pObj; |
| Cnf_Dat_t * pCnf; |
| Aig_Man_t * pManAigNew = NULL; |
| int nNodesBeg, nRegsBeg; |
| int nIter = -1; // Suppress "might be used uninitialized" |
| int i; |
| abctime clk = Abc_Clock(), clk2; |
| abctime TimeToStop = pParams->TimeLimit ? pParams->TimeLimit * CLOCKS_PER_SEC + Abc_Clock() : 0; |
| |
| if ( Aig_ManNodeNum(pManAig) == 0 ) |
| { |
| pParams->nIters = 0; |
| // Ntl_ManFinalize() needs the following to satisfy an assertion |
| Aig_ManReprStart(pManAig,Aig_ManObjNumMax(pManAig)); |
| return Aig_ManDupOrdered(pManAig); |
| } |
| assert( Aig_ManRegNum(pManAig) > 0 ); |
| assert( pParams->nFramesK > 0 ); |
| //Aig_ManShow( pManAig, 0, NULL ); |
| |
| if ( pParams->fWriteImps && pParams->nPartSize > 0 ) |
| { |
| pParams->nPartSize = 0; |
| printf( "Partitioning was disabled to allow implication writing.\n" ); |
| } |
| // perform partitioning |
| if ( (pParams->nPartSize > 0 && pParams->nPartSize < Aig_ManRegNum(pManAig)) |
| || (pManAig->vClockDoms && Vec_VecSize(pManAig->vClockDoms) > 0) ) |
| return Fra_FraigInductionPart( pManAig, pParams ); |
| |
| nNodesBeg = Aig_ManNodeNum(pManAig); |
| nRegsBeg = Aig_ManRegNum(pManAig); |
| |
| // enhance the AIG by adding timeframes |
| // Fra_FramesAddMore( pManAig, 3 ); |
| |
| // get parameters |
| Fra_ParamsDefaultSeq( pPars ); |
| pPars->nFramesP = pParams->nFramesP; |
| pPars->nFramesK = pParams->nFramesK; |
| pPars->nMaxImps = pParams->nMaxImps; |
| pPars->nMaxLevs = pParams->nMaxLevs; |
| pPars->fVerbose = pParams->fVerbose; |
| pPars->fRewrite = pParams->fRewrite; |
| pPars->fLatchCorr = pParams->fLatchCorr; |
| pPars->fUseImps = pParams->fUseImps; |
| pPars->fWriteImps = pParams->fWriteImps; |
| pPars->fUse1Hot = pParams->fUse1Hot; |
| |
| assert( !(pPars->nFramesP > 0 && pPars->fUse1Hot) ); |
| assert( !(pPars->nFramesK > 1 && pPars->fUse1Hot) ); |
| |
| // start the fraig manager for this run |
| p = Fra_ManStart( pManAig, pPars ); |
| p->pPars->nBTLimitNode = 0; |
| // derive and refine e-classes using K initialized frames |
| if ( fUseOldSimulation ) |
| { |
| if ( pPars->nFramesP > 0 ) |
| { |
| pPars->nFramesP = 0; |
| printf( "Fra_FraigInduction(): Prefix cannot be used.\n" ); |
| } |
| p->pSml = Fra_SmlStart( pManAig, 0, pPars->nFramesK + 1, pPars->nSimWords ); |
| Fra_SmlSimulate( p, 1 ); |
| } |
| else |
| { |
| // bug: r iscas/blif/s5378.blif ; st; ssw -v |
| // bug: r iscas/blif/s1238.blif ; st; ssw -v |
| // refine the classes with more simulation rounds |
| if ( pPars->fVerbose ) |
| printf( "Simulating %d AIG nodes for %d cycles ... ", Aig_ManNodeNum(pManAig), pPars->nFramesP + 32 ); |
| p->pSml = Fra_SmlSimulateSeq( pManAig, pPars->nFramesP, 32, 1, 1 ); //pPars->nFramesK + 1, 1 ); |
| if ( pPars->fVerbose ) |
| { |
| ABC_PRT( "Time", Abc_Clock() - clk ); |
| } |
| Fra_ClassesPrepare( p->pCla, p->pPars->fLatchCorr, p->pPars->nMaxLevs ); |
| // Fra_ClassesPostprocess( p->pCla ); |
| // compute one-hotness conditions |
| if ( p->pPars->fUse1Hot ) |
| p->vOneHots = Fra_OneHotCompute( p, p->pSml ); |
| // allocate new simulation manager for simulating counter-examples |
| Fra_SmlStop( p->pSml ); |
| p->pSml = Fra_SmlStart( pManAig, 0, pPars->nFramesK + 1, pPars->nSimWords ); |
| } |
| |
| // select the most expressive implications |
| if ( pPars->fUseImps ) |
| p->pCla->vImps = Fra_ImpDerive( p, 5000000, pPars->nMaxImps, pPars->fLatchCorr ); |
| |
| if ( pParams->TimeLimit != 0.0 && Abc_Clock() > TimeToStop ) |
| { |
| if ( !pParams->fSilent ) |
| printf( "Fra_FraigInduction(): Runtime limit exceeded.\n" ); |
| goto finish; |
| } |
| |
| // perform BMC (for the min number of frames) |
| Fra_BmcPerform( p, pPars->nFramesP, pPars->nFramesK+1 ); // +1 is needed to prevent non-refinement |
| //Fra_ClassesPrint( p->pCla, 1 ); |
| // if ( p->vCex == NULL ) |
| // p->vCex = Vec_IntAlloc( 1000 ); |
| |
| p->nLitsBeg = Fra_ClassesCountLits( p->pCla ); |
| p->nNodesBeg = nNodesBeg; // Aig_ManNodeNum(pManAig); |
| p->nRegsBeg = nRegsBeg; // Aig_ManRegNum(pManAig); |
| |
| // dump AIG of the timeframes |
| // pManAigNew = Fra_ClassesDeriveAig( p->pCla, pPars->nFramesK ); |
| // Aig_ManDumpBlif( pManAigNew, "frame_aig.blif", NULL, NULL ); |
| // Fra_ManPartitionTest2( pManAigNew ); |
| // Aig_ManStop( pManAigNew ); |
| |
| // iterate the inductive case |
| p->pCla->fRefinement = 1; |
| for ( nIter = 0; p->pCla->fRefinement; nIter++ ) |
| { |
| int nLitsOld = Fra_ClassesCountLits(p->pCla); |
| int nImpsOld = p->pCla->vImps? Vec_IntSize(p->pCla->vImps) : 0; |
| int nHotsOld = p->vOneHots? Fra_OneHotCount(p, p->vOneHots) : 0; |
| abctime clk3 = Abc_Clock(); |
| |
| if ( pParams->TimeLimit != 0.0 && Abc_Clock() > TimeToStop ) |
| { |
| if ( !pParams->fSilent ) |
| printf( "Fra_FraigInduction(): Runtime limit exceeded.\n" ); |
| goto finish; |
| } |
| |
| // mark the classes as non-refined |
| p->pCla->fRefinement = 0; |
| // derive non-init K-timeframes while implementing e-classes |
| clk2 = Abc_Clock(); |
| p->pManFraig = Fra_FramesWithClasses( p ); |
| p->timeTrav += Abc_Clock() - clk2; |
| //Aig_ManDumpBlif( p->pManFraig, "testaig.blif", NULL, NULL ); |
| |
| // perform AIG rewriting |
| if ( p->pPars->fRewrite ) |
| Fra_FraigInductionRewrite( p ); |
| |
| // convert the manager to SAT solver (the last nLatches outputs are inputs) |
| if ( fUseSimpleCnf || pPars->fUseImps ) |
| pCnf = Cnf_DeriveSimple( p->pManFraig, Aig_ManRegNum(p->pManFraig) ); |
| else |
| pCnf = Cnf_Derive( p->pManFraig, Aig_ManRegNum(p->pManFraig) ); |
| // Cnf_DataTranformPolarity( pCnf, 0 ); |
| //Cnf_DataWriteIntoFile( pCnf, "temp.cnf", 1 ); |
| |
| p->pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); |
| p->nSatVars = pCnf->nVars; |
| assert( p->pSat != NULL ); |
| if ( p->pSat == NULL ) |
| printf( "Fra_FraigInduction(): Computed CNF is not valid.\n" ); |
| if ( pPars->fUseImps ) |
| { |
| Fra_ImpAddToSolver( p, p->pCla->vImps, pCnf->pVarNums ); |
| if ( p->pSat == NULL ) |
| printf( "Fra_FraigInduction(): Adding implicationsn to CNF led to a conflict.\n" ); |
| } |
| |
| // set the pointers to the manager |
| Aig_ManForEachObj( p->pManFraig, pObj, i ) |
| pObj->pData = p; |
| |
| // prepare solver for fraiging the last timeframe |
| Fra_ManClean( p, Aig_ManObjNumMax(p->pManFraig) + Aig_ManNodeNum(p->pManAig) ); |
| |
| // transfer PI/LO variable numbers |
| Aig_ManForEachObj( p->pManFraig, pObj, i ) |
| { |
| if ( pCnf->pVarNums[pObj->Id] == -1 ) |
| continue; |
| Fra_ObjSetSatNum( pObj, pCnf->pVarNums[pObj->Id] ); |
| Fra_ObjSetFaninVec( pObj, (Vec_Ptr_t *)1 ); |
| } |
| Cnf_DataFree( pCnf ); |
| |
| // add one-hotness clauses |
| if ( p->pPars->fUse1Hot ) |
| Fra_OneHotAssume( p, p->vOneHots ); |
| // if ( p->pManAig->vOnehots ) |
| // Fra_OneHotAddKnownConstraint( p, p->pManAig->vOnehots ); |
| |
| // report the intermediate results |
| if ( pPars->fVerbose ) |
| { |
| printf( "%3d : C = %6d. Cl = %6d. L = %6d. LR = %6d. ", |
| nIter, Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), |
| Fra_ClassesCountLits(p->pCla), p->pManFraig->nAsserts ); |
| if ( p->pCla->vImps ) |
| printf( "I = %6d. ", Vec_IntSize(p->pCla->vImps) ); |
| if ( p->pPars->fUse1Hot ) |
| printf( "1h = %6d. ", Fra_OneHotCount(p, p->vOneHots) ); |
| printf( "NR = %6d. ", Aig_ManNodeNum(p->pManFraig) ); |
| // printf( "\n" ); |
| } |
| |
| // perform sweeping |
| p->nSatCallsRecent = 0; |
| p->nSatCallsSkipped = 0; |
| clk2 = Abc_Clock(); |
| if ( p->pPars->fUse1Hot ) |
| Fra_OneHotCheck( p, p->vOneHots ); |
| Fra_FraigSweep( p ); |
| if ( pPars->fVerbose ) |
| { |
| ABC_PRT( "T", Abc_Clock() - clk3 ); |
| } |
| |
| // Sat_SolverPrintStats( stdout, p->pSat ); |
| // remove FRAIG and SAT solver |
| Aig_ManStop( p->pManFraig ); p->pManFraig = NULL; |
| // printf( "Vars = %d. Clauses = %d. Learnts = %d.\n", p->pSat->size, p->pSat->clauses.size, p->pSat->learnts.size ); |
| sat_solver_delete( p->pSat ); p->pSat = NULL; |
| memset( p->pMemFraig, 0, sizeof(Aig_Obj_t *) * p->nSizeAlloc * p->nFramesAll ); |
| // printf( "Recent SAT called = %d. Skipped = %d.\n", p->nSatCallsRecent, p->nSatCallsSkipped ); |
| assert( p->vTimeouts == NULL ); |
| if ( p->vTimeouts ) |
| printf( "Fra_FraigInduction(): SAT solver timed out!\n" ); |
| // check if refinement has happened |
| // p->pCla->fRefinement = (int)(nLitsOld != Fra_ClassesCountLits(p->pCla)); |
| if ( p->pCla->fRefinement && |
| nLitsOld == Fra_ClassesCountLits(p->pCla) && |
| nImpsOld == (p->pCla->vImps? Vec_IntSize(p->pCla->vImps) : 0) && |
| nHotsOld == (p->vOneHots? Fra_OneHotCount(p, p->vOneHots) : 0) ) |
| { |
| printf( "Fra_FraigInduction(): Internal error. The result may not verify.\n" ); |
| break; |
| } |
| } |
| /* |
| // verify implications using simulation |
| if ( p->pCla->vImps && Vec_IntSize(p->pCla->vImps) ) |
| { |
| int Temp; |
| abctime clk = Abc_Clock(); |
| if ( Temp = Fra_ImpVerifyUsingSimulation( p ) ) |
| printf( "Implications failing the simulation test = %d (out of %d). ", Temp, Vec_IntSize(p->pCla->vImps) ); |
| else |
| printf( "All %d implications have passed the simulation test. ", Vec_IntSize(p->pCla->vImps) ); |
| ABC_PRT( "Time", Abc_Clock() - clk ); |
| } |
| */ |
| |
| // move the classes into representatives and reduce AIG |
| clk2 = Abc_Clock(); |
| if ( p->pPars->fWriteImps && p->vOneHots && Fra_OneHotCount(p, p->vOneHots) ) |
| { |
| extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact ); |
| Aig_Man_t * pNew; |
| char * pFileName = Ioa_FileNameGenericAppend( p->pManAig->pName, "_care.aig" ); |
| printf( "Care one-hotness clauses will be written into file \"%s\".\n", pFileName ); |
| pManAigNew = Aig_ManDupOrdered( pManAig ); |
| pNew = Fra_OneHotCreateExdc( p, p->vOneHots ); |
| Ioa_WriteAiger( pNew, pFileName, 0, 1 ); |
| Aig_ManStop( pNew ); |
| } |
| else |
| { |
| // Fra_ClassesPrint( p->pCla, 1 ); |
| Fra_ClassesSelectRepr( p->pCla ); |
| Fra_ClassesCopyReprs( p->pCla, p->vTimeouts ); |
| pManAigNew = Aig_ManDupRepr( pManAig, 0 ); |
| } |
| // add implications to the manager |
| // if ( fWriteImps && p->pCla->vImps && Vec_IntSize(p->pCla->vImps) ) |
| // Fra_ImpRecordInManager( p, pManAigNew ); |
| // cleanup the new manager |
| Aig_ManSeqCleanup( pManAigNew ); |
| // remove pointers to the dead nodes |
| // Aig_ManForEachObj( pManAig, pObj, i ) |
| // if ( pObj->pData && Aig_ObjIsNone(pObj->pData) ) |
| // pObj->pData = NULL; |
| // Aig_ManCountMergeRegs( pManAigNew ); |
| p->timeTrav += Abc_Clock() - clk2; |
| p->timeTotal = Abc_Clock() - clk; |
| // get the final stats |
| p->nLitsEnd = Fra_ClassesCountLits( p->pCla ); |
| p->nNodesEnd = Aig_ManNodeNum(pManAigNew); |
| p->nRegsEnd = Aig_ManRegNum(pManAigNew); |
| // free the manager |
| finish: |
| Fra_ManStop( p ); |
| // check the output |
| // if ( Aig_ManCoNum(pManAigNew) - Aig_ManRegNum(pManAigNew) == 1 ) |
| // if ( Aig_ObjChild0( Aig_ManCo(pManAigNew,0) ) == Aig_ManConst0(pManAigNew) ) |
| // printf( "Proved output constant 0.\n" ); |
| pParams->nIters = nIter; |
| return pManAigNew; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Outputs a set of pairs of equivalent nodes.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Fra_FraigInductionTest( char * pFileName, Fra_Ssw_t * pParams ) |
| { |
| FILE * pFile; |
| char * pFilePairs; |
| Aig_Man_t * pMan, * pNew; |
| Aig_Obj_t * pObj, * pRepr; |
| int * pNum2Id; |
| int i, Counter = 0; |
| pMan = Saig_ManReadBlif( pFileName ); |
| if ( pMan == NULL ) |
| return 0; |
| // perform seq SAT sweeping |
| pNew = Fra_FraigInduction( pMan, pParams ); |
| if ( pNew == NULL ) |
| { |
| Aig_ManStop( pMan ); |
| return 0; |
| } |
| if ( pParams->fVerbose ) |
| { |
| printf( "Original AIG: " ); |
| Aig_ManPrintStats( pMan ); |
| printf( "Reduced AIG: " ); |
| Aig_ManPrintStats( pNew ); |
| } |
| Aig_ManStop( pNew ); |
| pNum2Id = (int *)pMan->pData; |
| // write the output file |
| pFilePairs = Aig_FileNameGenericAppend( pFileName, ".pairs" ); |
| pFile = fopen( pFilePairs, "w" ); |
| Aig_ManForEachObj( pMan, pObj, i ) |
| if ( (pRepr = pMan->pReprs[pObj->Id]) ) |
| { |
| fprintf( pFile, "%d %d %c\n", pNum2Id[pObj->Id], pNum2Id[pRepr->Id], (Aig_ObjPhase(pObj) ^ Aig_ObjPhase(pRepr))? '-' : '+' ); |
| Counter++; |
| } |
| fclose( pFile ); |
| if ( pParams->fVerbose ) |
| { |
| printf( "Result: %d pairs of seq equiv nodes are written into file \"%s\".\n", Counter, pFilePairs ); |
| } |
| Aig_ManStop( pMan ); |
| return 1; |
| } |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
