| /**CFile**************************************************************** |
| |
| FileName [saigConstr2.c] |
| |
| SystemName [ABC: Logic synthesis and verification system.] |
| |
| PackageName [Sequential AIG package.] |
| |
| Synopsis [Functional constraint detection.] |
| |
| Author [Alan Mishchenko] |
| |
| Affiliation [UC Berkeley] |
| |
| Date [Ver. 1.0. Started - June 20, 2005.] |
| |
| Revision [$Id: saigConstr2.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] |
| |
| ***********************************************************************/ |
| |
| #include "saig.h" |
| #include "sat/cnf/cnf.h" |
| #include "sat/bsat/satSolver.h" |
| #include "bool/kit/kit.h" |
| #include "misc/bar/bar.h" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// DECLARATIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| static inline Aig_Obj_t * Aig_ObjFrames( Aig_Obj_t ** pObjMap, int nFs, Aig_Obj_t * pObj, int i ) { return pObjMap[nFs*pObj->Id + i]; } |
| static inline void Aig_ObjSetFrames( Aig_Obj_t ** pObjMap, int nFs, Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { pObjMap[nFs*pObj->Id + i] = pNode; } |
| |
| static inline Aig_Obj_t * Aig_ObjChild0Frames( Aig_Obj_t ** pObjMap, int nFs, Aig_Obj_t * pObj, int i ) { return Aig_ObjFanin0(pObj)? Aig_NotCond(Aig_ObjFrames(pObjMap,nFs,Aig_ObjFanin0(pObj),i), Aig_ObjFaninC0(pObj)) : NULL; } |
| static inline Aig_Obj_t * Aig_ObjChild1Frames( Aig_Obj_t ** pObjMap, int nFs, Aig_Obj_t * pObj, int i ) { return Aig_ObjFanin1(pObj)? Aig_NotCond(Aig_ObjFrames(pObjMap,nFs,Aig_ObjFanin1(pObj),i), Aig_ObjFaninC1(pObj)) : NULL; } |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// FUNCTION DEFINITIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| /**Function************************************************************* |
| |
| Synopsis [Returns the probability of POs being 1 under rand seq sim.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Ssw_ManProfileConstraints( Aig_Man_t * p, int nWords, int nFrames, int fVerbose ) |
| { |
| Vec_Ptr_t * vInfo; |
| Vec_Int_t * vProbs, * vProbs2; |
| Aig_Obj_t * pObj, * pObjLi; |
| unsigned * pInfo, * pInfo0, * pInfo1, * pInfoMask, * pInfoMask2; |
| int i, w, f, RetValue = 1; |
| abctime clk = Abc_Clock(); |
| if ( fVerbose ) |
| printf( "Simulating %d nodes and %d flops for %d frames with %d words... ", |
| Aig_ManNodeNum(p), Aig_ManRegNum(p), nFrames, nWords ); |
| Aig_ManRandom( 1 ); |
| vInfo = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(p)+2, nWords ); |
| Vec_PtrCleanSimInfo( vInfo, 0, nWords ); |
| vProbs = Vec_IntStart( Saig_ManPoNum(p) ); |
| vProbs2 = Vec_IntStart( Saig_ManPoNum(p) ); |
| // start the constant |
| pInfo = (unsigned *)Vec_PtrEntry( vInfo, Aig_ObjId(Aig_ManConst1(p)) ); |
| for ( w = 0; w < nWords; w++ ) |
| pInfo[w] = ~0; |
| // start the flop inputs |
| Saig_ManForEachLi( p, pObj, i ) |
| { |
| pInfo = (unsigned *)Vec_PtrEntry( vInfo, Aig_ObjId(pObj) ); |
| for ( w = 0; w < nWords; w++ ) |
| pInfo[w] = 0; |
| } |
| // get the info mask |
| pInfoMask = (unsigned *)Vec_PtrEntry( vInfo, Aig_ManObjNumMax(p) ); // PO failed |
| pInfoMask2 = (unsigned *)Vec_PtrEntry( vInfo, Aig_ManObjNumMax(p)+1 ); // constr failed |
| for ( f = 0; f < nFrames; f++ ) |
| { |
| // assign primary inputs |
| Saig_ManForEachPi( p, pObj, i ) |
| { |
| pInfo = (unsigned *)Vec_PtrEntry( vInfo, Aig_ObjId(pObj) ); |
| for ( w = 0; w < nWords; w++ ) |
| pInfo[w] = Aig_ManRandom( 0 ); |
| } |
| // move the flop values |
| Saig_ManForEachLiLo( p, pObjLi, pObj, i ) |
| { |
| pInfo = (unsigned *)Vec_PtrEntry( vInfo, Aig_ObjId(pObj) ); |
| pInfo0 = (unsigned *)Vec_PtrEntry( vInfo, Aig_ObjId(pObjLi) ); |
| for ( w = 0; w < nWords; w++ ) |
| pInfo[w] = pInfo0[w]; |
| } |
| // simulate the nodes |
| Aig_ManForEachNode( p, pObj, i ) |
| { |
| pInfo = (unsigned *)Vec_PtrEntry( vInfo, Aig_ObjId(pObj) ); |
| pInfo0 = (unsigned *)Vec_PtrEntry( vInfo, Aig_ObjFaninId0(pObj) ); |
| pInfo1 = (unsigned *)Vec_PtrEntry( vInfo, Aig_ObjFaninId1(pObj) ); |
| if ( Aig_ObjFaninC0(pObj) ) |
| { |
| if ( Aig_ObjFaninC1(pObj) ) |
| for ( w = 0; w < nWords; w++ ) |
| pInfo[w] = ~(pInfo0[w] | pInfo1[w]); |
| else |
| for ( w = 0; w < nWords; w++ ) |
| pInfo[w] = ~pInfo0[w] & pInfo1[w]; |
| } |
| else |
| { |
| if ( Aig_ObjFaninC1(pObj) ) |
| for ( w = 0; w < nWords; w++ ) |
| pInfo[w] = pInfo0[w] & ~pInfo1[w]; |
| else |
| for ( w = 0; w < nWords; w++ ) |
| pInfo[w] = pInfo0[w] & pInfo1[w]; |
| } |
| } |
| // clean the mask |
| for ( w = 0; w < nWords; w++ ) |
| pInfoMask[w] = pInfoMask2[w] = 0; |
| // simulate the primary outputs |
| Aig_ManForEachCo( p, pObj, i ) |
| { |
| pInfo = (unsigned *)Vec_PtrEntry( vInfo, Aig_ObjId(pObj) ); |
| pInfo0 = (unsigned *)Vec_PtrEntry( vInfo, Aig_ObjFaninId0(pObj) ); |
| if ( i < Saig_ManPoNum(p)-Saig_ManConstrNum(p) || i >= Saig_ManPoNum(p) ) |
| { |
| if ( Aig_ObjFaninC0(pObj) ) |
| { |
| for ( w = 0; w < nWords; w++ ) |
| pInfo[w] = ~pInfo0[w]; |
| } |
| else |
| { |
| for ( w = 0; w < nWords; w++ ) |
| pInfo[w] = pInfo0[w]; |
| } |
| } |
| else |
| { |
| if ( Aig_ObjFaninC0(pObj) ) |
| { |
| for ( w = 0; w < nWords; w++ ) |
| pInfo[w] |= ~pInfo0[w]; |
| } |
| else |
| { |
| for ( w = 0; w < nWords; w++ ) |
| pInfo[w] |= pInfo0[w]; |
| } |
| } |
| // collect patterns when one of the outputs fails |
| if ( i < Saig_ManPoNum(p)-Saig_ManConstrNum(p) ) |
| { |
| for ( w = 0; w < nWords; w++ ) |
| pInfoMask[w] |= pInfo[w]; |
| } |
| else if ( i < Saig_ManPoNum(p) ) |
| { |
| for ( w = 0; w < nWords; w++ ) |
| pInfoMask2[w] |= pInfo[w]; |
| } |
| } |
| // compare the PO values (mask=1 => out=0) or UNSAT(mask=1 & out=1) |
| Saig_ManForEachPo( p, pObj, i ) |
| { |
| pInfo = (unsigned *)Vec_PtrEntry( vInfo, Aig_ObjId(pObj) ); |
| for ( w = 0; w < nWords; w++ ) |
| Vec_IntAddToEntry( vProbs, i, Aig_WordCountOnes(pInfo[w]) ); |
| if ( i < Saig_ManPoNum(p)-Saig_ManConstrNum(p) ) |
| { |
| // chek the output |
| for ( w = 0; w < nWords; w++ ) |
| if ( pInfo[w] & ~pInfoMask2[w] ) |
| break; |
| if ( w == nWords ) |
| continue; |
| printf( "Primary output %d fails on some input patterns.\n", i ); |
| } |
| else |
| { |
| // collect patterns that block the POs |
| for ( w = 0; w < nWords; w++ ) |
| Vec_IntAddToEntry( vProbs2, i, Aig_WordCountOnes(pInfo[w] & pInfoMask[w]) ); |
| } |
| } |
| } |
| if ( fVerbose ) |
| Abc_PrintTime( 1, "T", Abc_Clock() - clk ); |
| // print the state |
| if ( fVerbose ) |
| { |
| Saig_ManForEachPo( p, pObj, i ) |
| { |
| if ( i < Saig_ManPoNum(p) - Saig_ManConstrNum(p) ) |
| printf( "Primary output : " ); |
| else |
| printf( "Constraint %3d : ", i-(Saig_ManPoNum(p) - Saig_ManConstrNum(p)) ); |
| printf( "ProbOne = %f ", (float)Vec_IntEntry(vProbs, i)/(32*nWords*nFrames) ); |
| printf( "ProbOneC = %f ", (float)Vec_IntEntry(vProbs2, i)/(32*nWords*nFrames) ); |
| printf( "AllZeroValue = %d ", Aig_ObjPhase(pObj) ); |
| printf( "\n" ); |
| } |
| } |
| |
| // print the states |
| Vec_PtrFree( vInfo ); |
| Vec_IntFree( vProbs ); |
| Vec_IntFree( vProbs2 ); |
| return RetValue; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Creates COI of the property output.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Aig_Man_t * Saig_ManCreateIndMiter( Aig_Man_t * pAig, Vec_Vec_t * vCands ) |
| { |
| int nFrames = 2; |
| Vec_Ptr_t * vNodes; |
| Aig_Man_t * pFrames; |
| Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjNew; |
| Aig_Obj_t ** pObjMap; |
| int i, f, k; |
| |
| // create mapping for the frames nodes |
| pObjMap = ABC_CALLOC( Aig_Obj_t *, nFrames * Aig_ManObjNumMax(pAig) ); |
| |
| // start the fraig package |
| pFrames = Aig_ManStart( Aig_ManObjNumMax(pAig) * nFrames ); |
| pFrames->pName = Abc_UtilStrsav( pAig->pName ); |
| pFrames->pSpec = Abc_UtilStrsav( pAig->pSpec ); |
| // map constant nodes |
| for ( f = 0; f < nFrames; f++ ) |
| Aig_ObjSetFrames( pObjMap, nFrames, Aig_ManConst1(pAig), f, Aig_ManConst1(pFrames) ); |
| // create PI nodes for the frames |
| for ( f = 0; f < nFrames; f++ ) |
| Aig_ManForEachPiSeq( pAig, pObj, i ) |
| Aig_ObjSetFrames( pObjMap, nFrames, pObj, f, Aig_ObjCreateCi(pFrames) ); |
| // set initial state for the latches |
| Aig_ManForEachLoSeq( pAig, pObj, i ) |
| Aig_ObjSetFrames( pObjMap, nFrames, pObj, 0, Aig_ObjCreateCi(pFrames) ); |
| |
| // add timeframes |
| for ( f = 0; f < nFrames; f++ ) |
| { |
| // add internal nodes of this frame |
| Aig_ManForEachNode( pAig, pObj, i ) |
| { |
| pObjNew = Aig_And( pFrames, Aig_ObjChild0Frames(pObjMap,nFrames,pObj,f), Aig_ObjChild1Frames(pObjMap,nFrames,pObj,f) ); |
| Aig_ObjSetFrames( pObjMap, nFrames, pObj, f, pObjNew ); |
| } |
| // set the latch inputs and copy them into the latch outputs of the next frame |
| Aig_ManForEachLiLoSeq( pAig, pObjLi, pObjLo, i ) |
| { |
| pObjNew = Aig_ObjChild0Frames(pObjMap,nFrames,pObjLi,f); |
| if ( f < nFrames - 1 ) |
| Aig_ObjSetFrames( pObjMap, nFrames, pObjLo, f+1, pObjNew ); |
| } |
| } |
| |
| // go through the candidates |
| Vec_VecForEachLevel( vCands, vNodes, i ) |
| { |
| Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, k ) |
| { |
| Aig_Obj_t * pObjR = Aig_Regular(pObj); |
| Aig_Obj_t * pNode0 = pObjMap[nFrames*Aig_ObjId(pObjR)+0]; |
| Aig_Obj_t * pNode1 = pObjMap[nFrames*Aig_ObjId(pObjR)+1]; |
| Aig_Obj_t * pFan0 = Aig_NotCond( pNode0, Aig_IsComplement(pObj) ); |
| Aig_Obj_t * pFan1 = Aig_NotCond( pNode1, !Aig_IsComplement(pObj) ); |
| Aig_Obj_t * pMiter = Aig_And( pFrames, pFan0, pFan1 ); |
| Aig_ObjCreateCo( pFrames, pMiter ); |
| } |
| } |
| Aig_ManCleanup( pFrames ); |
| ABC_FREE( pObjMap ); |
| |
| //Aig_ManShow( pAig, 0, NULL ); |
| //Aig_ManShow( pFrames, 0, NULL ); |
| return pFrames; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Performs inductive check for one of the constraints.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Saig_ManFilterUsingIndOne_new( Aig_Man_t * p, Aig_Man_t * pFrame, sat_solver * pSat, Cnf_Dat_t * pCnf, int nConfs, int nProps, int Counter ) |
| { |
| Aig_Obj_t * pObj; |
| int Lit, status; |
| pObj = Aig_ManCo( pFrame, Counter ); |
| Lit = toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], 0 ); |
| status = sat_solver_solve( pSat, &Lit, &Lit + 1, (ABC_INT64_T)nConfs, 0, 0, 0 ); |
| if ( status == l_False ) |
| return 1; |
| if ( status == l_Undef ) |
| { |
| // printf( "Solver returned undecided.\n" ); |
| return 0; |
| } |
| assert( status == l_True ); |
| return 0; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Detects constraints functionally.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Saig_ManFilterUsingInd( Aig_Man_t * p, Vec_Vec_t * vCands, int nConfs, int nProps, int fVerbose ) |
| { |
| Vec_Ptr_t * vNodes; |
| Aig_Man_t * pFrames; |
| sat_solver * pSat; |
| Cnf_Dat_t * pCnf; |
| Aig_Obj_t * pObj; |
| int i, k, k2, Counter; |
| /* |
| Vec_VecForEachLevel( vCands, vNodes, i ) |
| Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, k ) |
| printf( "%d ", Aig_ObjId(Aig_Regular(pObj)) ); |
| printf( "\n" ); |
| */ |
| // create timeframes |
| // pFrames = Saig_ManUnrollInd( p ); |
| pFrames = Saig_ManCreateIndMiter( p, vCands ); |
| assert( Aig_ManCoNum(pFrames) == Vec_VecSizeSize(vCands) ); |
| // start the SAT solver |
| pCnf = Cnf_DeriveSimple( pFrames, Aig_ManCoNum(pFrames) ); |
| pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); |
| // check candidates |
| if ( fVerbose ) |
| printf( "Filtered cands: " ); |
| Counter = 0; |
| Vec_VecForEachLevel( vCands, vNodes, i ) |
| { |
| k2 = 0; |
| Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, k ) |
| { |
| if ( Saig_ManFilterUsingIndOne_new( p, pFrames, pSat, pCnf, nConfs, nProps, Counter++ ) ) |
| // if ( Saig_ManFilterUsingIndOne_old( p, pSat, pCnf, nConfs, pObj ) ) |
| { |
| Vec_PtrWriteEntry( vNodes, k2++, pObj ); |
| if ( fVerbose ) |
| printf( "%d:%s%d ", i, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) ); |
| } |
| } |
| Vec_PtrShrink( vNodes, k2 ); |
| } |
| if ( fVerbose ) |
| printf( "\n" ); |
| // clean up |
| Cnf_DataFree( pCnf ); |
| sat_solver_delete( pSat ); |
| if ( fVerbose ) |
| Aig_ManPrintStats( pFrames ); |
| Aig_ManStop( pFrames ); |
| } |
| |
| |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Creates COI of the property output.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Aig_Man_t * Saig_ManUnrollCOI_( Aig_Man_t * p, int nFrames ) |
| { |
| Aig_Man_t * pFrames; |
| Aig_Obj_t ** pObjMap; |
| int i; |
| //Aig_Man_t * Aig_ManFrames( Aig_Man_t * pAig, int nFrames, int fInit, int fOuts, int fRegs, int fEnlarge, Aig_Obj_t *** ppObjMap ) |
| pFrames = Aig_ManFrames( p, nFrames, 0, 1, 1, 0, &pObjMap ); |
| for ( i = 0; i < nFrames * Aig_ManObjNumMax(p); i++ ) |
| if ( pObjMap[i] && Aig_ObjIsNone( Aig_Regular(pObjMap[i]) ) ) |
| pObjMap[i] = NULL; |
| assert( p->pObjCopies == NULL ); |
| p->pObjCopies = pObjMap; |
| return pFrames; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Creates COI of the property output.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Aig_Man_t * Saig_ManUnrollCOI( Aig_Man_t * pAig, int nFrames ) |
| { |
| Aig_Man_t * pFrames; |
| Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjNew; |
| Aig_Obj_t ** pObjMap; |
| int i, f; |
| // create mapping for the frames nodes |
| pObjMap = ABC_CALLOC( Aig_Obj_t *, nFrames * Aig_ManObjNumMax(pAig) ); |
| // start the fraig package |
| pFrames = Aig_ManStart( Aig_ManObjNumMax(pAig) * nFrames ); |
| pFrames->pName = Abc_UtilStrsav( pAig->pName ); |
| pFrames->pSpec = Abc_UtilStrsav( pAig->pSpec ); |
| // map constant nodes |
| for ( f = 0; f < nFrames; f++ ) |
| Aig_ObjSetFrames( pObjMap, nFrames, Aig_ManConst1(pAig), f, Aig_ManConst1(pFrames) ); |
| // create PI nodes for the frames |
| for ( f = 0; f < nFrames; f++ ) |
| Aig_ManForEachPiSeq( pAig, pObj, i ) |
| Aig_ObjSetFrames( pObjMap, nFrames, pObj, f, Aig_ObjCreateCi(pFrames) ); |
| // set initial state for the latches |
| Aig_ManForEachLoSeq( pAig, pObj, i ) |
| Aig_ObjSetFrames( pObjMap, nFrames, pObj, 0, Aig_ObjCreateCi(pFrames) ); |
| // add timeframes |
| for ( f = 0; f < nFrames; f++ ) |
| { |
| Aig_ManForEachNode( pAig, pObj, i ) |
| { |
| pObjNew = Aig_And( pFrames, Aig_ObjChild0Frames(pObjMap,nFrames,pObj,f), Aig_ObjChild1Frames(pObjMap,nFrames,pObj,f) ); |
| Aig_ObjSetFrames( pObjMap, nFrames, pObj, f, pObjNew ); |
| } |
| // set the latch inputs and copy them into the latch outputs of the next frame |
| Aig_ManForEachLiLoSeq( pAig, pObjLi, pObjLo, i ) |
| { |
| pObjNew = Aig_ObjChild0Frames(pObjMap,nFrames,pObjLi,f); |
| if ( f < nFrames - 1 ) |
| Aig_ObjSetFrames( pObjMap, nFrames, pObjLo, f+1, pObjNew ); |
| } |
| } |
| // create the only output |
| for ( f = nFrames-1; f < nFrames; f++ ) |
| { |
| Aig_ManForEachPoSeq( pAig, pObj, i ) |
| { |
| pObjNew = Aig_ObjCreateCo( pFrames, Aig_ObjChild0Frames(pObjMap,nFrames,pObj,f) ); |
| Aig_ObjSetFrames( pObjMap, nFrames, pObj, f, pObjNew ); |
| } |
| } |
| // created lots of dangling nodes - no sweeping! |
| //Aig_ManCleanup( pFrames ); |
| assert( pAig->pObjCopies == NULL ); |
| pAig->pObjCopies = pObjMap; |
| return pFrames; |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Collects and saves values of the SAT variables.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Saig_CollectSatValues( sat_solver * pSat, Cnf_Dat_t * pCnf, Vec_Ptr_t * vInfo, int * piPat ) |
| { |
| Aig_Obj_t * pObj; |
| unsigned * pInfo; |
| int i; |
| Aig_ManForEachObj( pCnf->pMan, pObj, i ) |
| { |
| if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) ) |
| continue; |
| assert( pCnf->pVarNums[i] > 0 ); |
| pInfo = (unsigned *)Vec_PtrEntry( vInfo, i ); |
| if ( Abc_InfoHasBit(pInfo, *piPat) != sat_solver_var_value(pSat, pCnf->pVarNums[i]) ) |
| Abc_InfoXorBit(pInfo, *piPat); |
| } |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Runs the SAT test for the node in one polarity.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Saig_DetectTryPolarity( sat_solver * pSat, int nConfs, int nProps, Cnf_Dat_t * pCnf, Aig_Obj_t * pObj, int iPol, Vec_Ptr_t * vInfo, int * piPat, int fVerbose ) |
| { |
| Aig_Obj_t * pOut = Aig_ManCo( pCnf->pMan, 0 ); |
| int status, Lits[2]; |
| // ABC_INT64_T nOldConfs = pSat->stats.conflicts; |
| // ABC_INT64_T nOldImps = pSat->stats.propagations; |
| Lits[0] = toLitCond( pCnf->pVarNums[Aig_ObjId(pOut)], 0 ); |
| Lits[1] = toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], !iPol ); |
| status = sat_solver_solve( pSat, Lits, Lits + 2, (ABC_INT64_T)nConfs, (ABC_INT64_T)nProps, 0, 0 ); |
| if ( status == l_False ) |
| { |
| // printf( "u%d(%d) ", (int)(pSat->stats.conflicts-nOldConfs), (int)(pSat->stats.propagations-nOldImps) ); |
| return 1; |
| } |
| if ( status == l_Undef ) |
| { |
| // printf( "Solver returned undecided.\n" ); |
| return 0; |
| } |
| // printf( "s%d(%d) ", (int)(pSat->stats.conflicts-nOldConfs), (int)(pSat->stats.propagations-nOldImps) ); |
| assert( status == l_True ); |
| Saig_CollectSatValues( pSat, pCnf, vInfo, piPat ); |
| (*piPat)++; |
| if ( *piPat == Vec_PtrReadWordsSimInfo(vInfo) * 32 ) |
| { |
| if ( fVerbose ) |
| printf( "Warning: Reached the limit on the number of patterns.\n" ); |
| *piPat = 0; |
| } |
| return 0; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Returns the number of variables implied by the output.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Vec_Vec_t * Ssw_ManFindDirectImplications( Aig_Man_t * p, int nFrames, int nConfs, int nProps, int fVerbose ) |
| { |
| Vec_Vec_t * vCands = NULL; |
| Vec_Ptr_t * vNodes; |
| Cnf_Dat_t * pCnf; |
| sat_solver * pSat; |
| Aig_Man_t * pFrames; |
| Aig_Obj_t * pObj, * pRepr, * pReprR; |
| int i, f, k, value; |
| vCands = Vec_VecAlloc( nFrames ); |
| |
| // perform unrolling |
| pFrames = Saig_ManUnrollCOI( p, nFrames ); |
| assert( Aig_ManCoNum(pFrames) == 1 ); |
| // start the SAT solver |
| pCnf = Cnf_DeriveSimple( pFrames, 0 ); |
| pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); |
| if ( pSat != NULL ) |
| { |
| Aig_ManIncrementTravId( p ); |
| for ( f = 0; f < nFrames; f++ ) |
| { |
| Aig_ManForEachObj( p, pObj, i ) |
| { |
| if ( !Aig_ObjIsCand(pObj) ) |
| continue; |
| if ( Aig_ObjIsTravIdCurrent(p, pObj) ) |
| continue; |
| // get the node from timeframes |
| pRepr = p->pObjCopies[nFrames*i + nFrames-1-f]; |
| pReprR = Aig_Regular(pRepr); |
| if ( pCnf->pVarNums[Aig_ObjId(pReprR)] < 0 ) |
| continue; |
| // value = pSat->assigns[ pCnf->pVarNums[Aig_ObjId(pReprR)] ]; |
| value = sat_solver_get_var_value( pSat, pCnf->pVarNums[Aig_ObjId(pReprR)] ); |
| if ( value == l_Undef ) |
| continue; |
| // label this node as taken |
| Aig_ObjSetTravIdCurrent(p, pObj); |
| if ( Saig_ObjIsLo(p, pObj) ) |
| Aig_ObjSetTravIdCurrent( p, Aig_ObjFanin0(Saig_ObjLoToLi(p, pObj)) ); |
| // remember the node |
| Vec_VecPush( vCands, f, Aig_NotCond( pObj, (value == l_True) ^ Aig_IsComplement(pRepr) ) ); |
| // printf( "%s%d ", (value == l_False)? "":"!", i ); |
| } |
| } |
| // printf( "\n" ); |
| sat_solver_delete( pSat ); |
| } |
| Aig_ManStop( pFrames ); |
| Cnf_DataFree( pCnf ); |
| |
| if ( fVerbose ) |
| { |
| printf( "Found %3d candidates.\n", Vec_VecSizeSize(vCands) ); |
| Vec_VecForEachLevel( vCands, vNodes, k ) |
| { |
| printf( "Level %d. Cands =%d ", k, Vec_PtrSize(vNodes) ); |
| // Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i ) |
| // printf( "%d:%s%d ", k, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) ); |
| printf( "\n" ); |
| } |
| } |
| |
| ABC_FREE( p->pObjCopies ); |
| Saig_ManFilterUsingInd( p, vCands, nConfs, nProps, fVerbose ); |
| if ( Vec_VecSizeSize(vCands) ) |
| printf( "Found %3d constraints after filtering.\n", Vec_VecSizeSize(vCands) ); |
| if ( fVerbose ) |
| { |
| Vec_VecForEachLevel( vCands, vNodes, k ) |
| { |
| printf( "Level %d. Constr =%d ", k, Vec_PtrSize(vNodes) ); |
| // Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i ) |
| // printf( "%d:%s%d ", k, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) ); |
| printf( "\n" ); |
| } |
| } |
| |
| return vCands; |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Detects constraints functionally.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Vec_Vec_t * Saig_ManDetectConstrFunc( Aig_Man_t * p, int nFrames, int nConfs, int nProps, int fVerbose ) |
| { |
| int iPat = 0, nWordsAlloc = 16; |
| Bar_Progress_t * pProgress = NULL; |
| Vec_Vec_t * vCands = NULL; |
| Vec_Ptr_t * vInfo, * vNodes; |
| Aig_Obj_t * pObj, * pRepr, * pObjNew; |
| Aig_Man_t * pFrames; |
| sat_solver * pSat; |
| Cnf_Dat_t * pCnf; |
| unsigned * pInfo; |
| int i, j, k, Lit, status, nCands = 0; |
| assert( Saig_ManPoNum(p) == 1 ); |
| if ( Saig_ManPoNum(p) != 1 ) |
| { |
| printf( "The number of outputs is different from 1.\n" ); |
| return NULL; |
| } |
| //printf( "Implications = %d.\n", Ssw_ManCountImplications(p, nFrames) ); |
| |
| // perform unrolling |
| pFrames = Saig_ManUnrollCOI( p, nFrames ); |
| assert( Aig_ManCoNum(pFrames) == 1 ); |
| if ( fVerbose ) |
| { |
| printf( "Detecting constraints with %d frames, %d conflicts, and %d propagations.\n", nFrames, nConfs, nProps ); |
| printf( "Frames: " ); |
| Aig_ManPrintStats( pFrames ); |
| } |
| // Aig_ManShow( pFrames, 0, NULL ); |
| |
| // start the SAT solver |
| pCnf = Cnf_DeriveSimple( pFrames, Aig_ManCoNum(pFrames) ); |
| pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); |
| //printf( "Implications = %d.\n", pSat->qhead ); |
| |
| // solve the original problem |
| Lit = toLitCond( pCnf->pVarNums[Aig_ObjId(Aig_ManCo(pFrames,0))], 0 ); |
| status = sat_solver_solve( pSat, &Lit, &Lit + 1, (ABC_INT64_T)nConfs, 0, 0, 0 ); |
| if ( status == l_False ) |
| { |
| printf( "The problem is trivially UNSAT (inductive with k=%d).\n", nFrames-1 ); |
| Cnf_DataFree( pCnf ); |
| sat_solver_delete( pSat ); |
| Aig_ManStop( pFrames ); |
| return NULL; |
| } |
| if ( status == l_Undef ) |
| { |
| printf( "Solver could not solve the original problem.\n" ); |
| Cnf_DataFree( pCnf ); |
| sat_solver_delete( pSat ); |
| Aig_ManStop( pFrames ); |
| return NULL; |
| } |
| assert( status == l_True ); |
| |
| // create simulation info |
| vInfo = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(pFrames), nWordsAlloc ); |
| Vec_PtrCleanSimInfo( vInfo, 0, nWordsAlloc ); |
| Saig_CollectSatValues( pSat, pCnf, vInfo, &iPat ); |
| Aig_ManForEachObj( pFrames, pObj, i ) |
| { |
| pInfo = (unsigned *)Vec_PtrEntry( vInfo, i ); |
| if ( pInfo[0] & 1 ) |
| memset( (char*)pInfo, 0xff, 4*nWordsAlloc ); |
| } |
| // Aig_ManShow( pFrames, 0, NULL ); |
| // Aig_ManShow( p, 0, NULL ); |
| |
| // consider the nodes for ci=>!Out and label when it holds |
| pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(pFrames) ); |
| Aig_ManCleanMarkAB( pFrames ); |
| Aig_ManForEachObj( pFrames, pObj, i ) |
| { |
| if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) ) |
| continue; |
| Bar_ProgressUpdate( pProgress, i, NULL ); |
| // check if the node is available in both polarities |
| pInfo = (unsigned *)Vec_PtrEntry( vInfo, i ); |
| for ( k = 0; k < nWordsAlloc; k++ ) |
| if ( pInfo[k] != ~0 ) |
| break; |
| if ( k == nWordsAlloc ) |
| { |
| if ( Saig_DetectTryPolarity(pSat, nConfs, nProps, pCnf, pObj, 0, vInfo, &iPat, fVerbose) ) // !pObj is a constr |
| { |
| pObj->fMarkA = 1, nCands++; |
| // printf( "!%d ", Aig_ObjId(pObj) ); |
| } |
| continue; |
| } |
| for ( k = 0; k < nWordsAlloc; k++ ) |
| if ( pInfo[k] != 0 ) |
| break; |
| if ( k == nWordsAlloc ) |
| { |
| if ( Saig_DetectTryPolarity(pSat, nConfs, nProps, pCnf, pObj, 1, vInfo, &iPat, fVerbose) ) // pObj is a constr |
| { |
| pObj->fMarkB = 1, nCands++; |
| // printf( "%d ", Aig_ObjId(pObj) ); |
| } |
| continue; |
| } |
| } |
| Bar_ProgressStop( pProgress ); |
| if ( nCands ) |
| { |
| |
| // printf( "\n" ); |
| if ( fVerbose ) |
| printf( "Found %3d classes of candidates.\n", nCands ); |
| vCands = Vec_VecAlloc( nFrames ); |
| for ( k = 0; k < nFrames; k++ ) |
| { |
| Aig_ManForEachObj( p, pObj, i ) |
| { |
| if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) ) |
| continue; |
| pRepr = p->pObjCopies[nFrames*i + nFrames-1-k]; |
| // pRepr = p->pObjCopies[nFrames*i + k]; |
| if ( pRepr == NULL ) |
| continue; |
| if ( Aig_Regular(pRepr)->fMarkA ) // !pObj is a constr |
| { |
| pObjNew = Aig_NotCond(pObj, !Aig_IsComplement(pRepr)); |
| |
| for ( j = 0; j < k; j++ ) |
| if ( Vec_PtrFind( Vec_VecEntry(vCands, j), pObjNew ) >= 0 ) |
| break; |
| if ( j == k ) |
| Vec_VecPush( vCands, k, pObjNew ); |
| // printf( "%d->!%d ", Aig_ObjId(Aig_Regular(pRepr)), Aig_ObjId(pObj) ); |
| } |
| else if ( Aig_Regular(pRepr)->fMarkB ) // pObj is a constr |
| { |
| pObjNew = Aig_NotCond(pObj, Aig_IsComplement(pRepr)); |
| |
| for ( j = 0; j < k; j++ ) |
| if ( Vec_PtrFind( Vec_VecEntry(vCands, j), pObjNew ) >= 0 ) |
| break; |
| if ( j == k ) |
| Vec_VecPush( vCands, k, pObjNew ); |
| // printf( "%d->%d ", Aig_ObjId(Aig_Regular(pRepr)), Aig_ObjId(pObj) ); |
| } |
| } |
| } |
| |
| // printf( "\n" ); |
| if ( fVerbose ) |
| { |
| printf( "Found %3d candidates.\n", Vec_VecSizeSize(vCands) ); |
| Vec_VecForEachLevel( vCands, vNodes, k ) |
| { |
| printf( "Level %d. Cands =%d ", k, Vec_PtrSize(vNodes) ); |
| // Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i ) |
| // printf( "%d:%s%d ", k, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) ); |
| printf( "\n" ); |
| } |
| } |
| |
| ABC_FREE( p->pObjCopies ); |
| Saig_ManFilterUsingInd( p, vCands, nConfs, nProps, fVerbose ); |
| if ( Vec_VecSizeSize(vCands) ) |
| printf( "Found %3d constraints after filtering.\n", Vec_VecSizeSize(vCands) ); |
| if ( fVerbose ) |
| { |
| Vec_VecForEachLevel( vCands, vNodes, k ) |
| { |
| printf( "Level %d. Constr =%d ", k, Vec_PtrSize(vNodes) ); |
| // Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i ) |
| // printf( "%d:%s%d ", k, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) ); |
| printf( "\n" ); |
| } |
| } |
| } |
| Vec_PtrFree( vInfo ); |
| Cnf_DataFree( pCnf ); |
| sat_solver_delete( pSat ); |
| Aig_ManCleanMarkAB( pFrames ); |
| Aig_ManStop( pFrames ); |
| return vCands; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Experimental procedure.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Saig_ManDetectConstrFuncTest( Aig_Man_t * p, int nFrames, int nConfs, int nProps, int fOldAlgo, int fVerbose ) |
| { |
| Vec_Vec_t * vCands; |
| if ( fOldAlgo ) |
| vCands = Saig_ManDetectConstrFunc( p, nFrames, nConfs, nProps, fVerbose ); |
| else |
| vCands = Ssw_ManFindDirectImplications( p, nFrames, nConfs, nProps, fVerbose ); |
| Vec_VecFreeP( &vCands ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Duplicates the AIG while unfolding constraints.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Aig_Man_t * Saig_ManDupUnfoldConstrsFunc( Aig_Man_t * pAig, int nFrames, int nConfs, int nProps, int fOldAlgo, int fVerbose ) |
| { |
| Aig_Man_t * pNew; |
| Vec_Vec_t * vCands; |
| Vec_Ptr_t * vNodes, * vNewFlops; |
| Aig_Obj_t * pObj; |
| int i, j, k, nNewFlops; |
| if ( fOldAlgo ) |
| vCands = Saig_ManDetectConstrFunc( pAig, nFrames, nConfs, nProps, fVerbose ); |
| else |
| vCands = Ssw_ManFindDirectImplications( pAig, nFrames, nConfs, nProps, fVerbose ); |
| if ( vCands == NULL || Vec_VecSizeSize(vCands) == 0 ) |
| { |
| Vec_VecFreeP( &vCands ); |
| return Aig_ManDupDfs( pAig ); |
| } |
| // create new manager |
| pNew = Aig_ManDupWithoutPos( pAig ); |
| pNew->nConstrs = pAig->nConstrs + Vec_VecSizeSize(vCands); |
| // add normal POs |
| Saig_ManForEachPo( pAig, pObj, i ) |
| Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) ); |
| // create constraint outputs |
| vNewFlops = Vec_PtrAlloc( 100 ); |
| Vec_VecForEachLevel( vCands, vNodes, i ) |
| { |
| Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, k ) |
| { |
| Vec_PtrPush( vNewFlops, Aig_ObjRealCopy(pObj) ); |
| for ( j = 0; j < i; j++ ) |
| Vec_PtrPush( vNewFlops, Aig_ObjCreateCi(pNew) ); |
| Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Vec_PtrPop(vNewFlops) ); |
| } |
| } |
| // add latch outputs |
| Saig_ManForEachLi( pAig, pObj, i ) |
| Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) ); |
| // add new latch outputs |
| nNewFlops = 0; |
| Vec_VecForEachLevel( vCands, vNodes, i ) |
| { |
| Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, k ) |
| { |
| for ( j = 0; j < i; j++ ) |
| Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Vec_PtrEntry(vNewFlops, nNewFlops++) ); |
| } |
| } |
| assert( nNewFlops == Vec_PtrSize(vNewFlops) ); |
| Aig_ManSetRegNum( pNew, Aig_ManRegNum(pAig) + nNewFlops ); |
| Vec_VecFreeP( &vCands ); |
| Vec_PtrFree( vNewFlops ); |
| return pNew; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Duplicates the AIG while unfolding constraints.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Aig_Man_t * Saig_ManDupFoldConstrsFunc( Aig_Man_t * pAig, int fCompl, int fVerbose ) |
| { |
| Aig_Man_t * pAigNew; |
| Aig_Obj_t * pMiter, * pFlopOut, * pFlopIn, * pObj; |
| int i; |
| if ( Aig_ManConstrNum(pAig) == 0 ) |
| return Aig_ManDupDfs( pAig ); |
| assert( Aig_ManConstrNum(pAig) < Saig_ManPoNum(pAig) ); |
| // start the new manager |
| pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) ); |
| pAigNew->pName = Abc_UtilStrsav( pAig->pName ); |
| pAigNew->pSpec = Abc_UtilStrsav( pAig->pSpec ); |
| // map the constant node |
| Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew ); |
| // create variables for PIs |
| Aig_ManForEachCi( pAig, pObj, i ) |
| pObj->pData = Aig_ObjCreateCi( pAigNew ); |
| // add internal nodes of this frame |
| Aig_ManForEachNode( pAig, pObj, i ) |
| pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); |
| |
| // OR the constraint outputs |
| pMiter = Aig_ManConst0( pAigNew ); |
| Saig_ManForEachPo( pAig, pObj, i ) |
| { |
| if ( i < Saig_ManPoNum(pAig)-Aig_ManConstrNum(pAig) ) |
| continue; |
| pMiter = Aig_Or( pAigNew, pMiter, Aig_NotCond( Aig_ObjChild0Copy(pObj), fCompl ) ); |
| } |
| |
| // create additional flop |
| if ( Saig_ManRegNum(pAig) > 0 ) |
| { |
| pFlopOut = Aig_ObjCreateCi( pAigNew ); |
| pFlopIn = Aig_Or( pAigNew, pMiter, pFlopOut ); |
| } |
| else |
| pFlopIn = pMiter; |
| |
| // create primary output |
| Saig_ManForEachPo( pAig, pObj, i ) |
| { |
| if ( i >= Saig_ManPoNum(pAig)-Aig_ManConstrNum(pAig) ) |
| continue; |
| pMiter = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_Not(pFlopIn) ); |
| Aig_ObjCreateCo( pAigNew, pMiter ); |
| } |
| |
| // transfer to register outputs |
| Saig_ManForEachLi( pAig, pObj, i ) |
| Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) ); |
| |
| // create additional flop |
| if ( Saig_ManRegNum(pAig) > 0 ) |
| { |
| Aig_ObjCreateCo( pAigNew, pFlopIn ); |
| Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig)+1 ); |
| } |
| |
| // perform cleanup |
| Aig_ManCleanup( pAigNew ); |
| Aig_ManSeqCleanup( pAigNew ); |
| return pAigNew; |
| } |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| #include "saigUnfold2.c" |
| ABC_NAMESPACE_IMPL_END |
| |
