| |
| int Saig_ManFilterUsingIndOne2( Aig_Man_t * p, Aig_Man_t * pFrame, sat_solver * pSat, Cnf_Dat_t * pCnf, int nConfs, int nProps, int Counter |
| , int type_ /* jlong -- */ |
| ) |
| { |
| Aig_Obj_t * pObj; |
| int Lit, status; |
| pObj = Aig_ManCo( pFrame, Counter*3+type_ ); /* which co */ |
| 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 ) /* unsat */ |
| return status; |
| if ( status == l_Undef ) |
| { |
| printf( "Solver returned undecided.\n" ); |
| return status; |
| } |
| assert( status == l_True ); |
| return status; |
| } |
| |
| Aig_Man_t * Saig_ManCreateIndMiter2( Aig_Man_t * pAig, Vec_Vec_t * vCands ) |
| { |
| int nFrames = 3; |
| 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 ); |
| |
| /* need to check p & Xp is satisfiable */ |
| /* jlong -- begin */ |
| { |
| Aig_Obj_t * pMiter2 = Aig_And( pFrames, pFan0, Aig_Not(pFan1)); |
| Aig_ObjCreateCo( pFrames, pMiter2 ); |
| } |
| /* jlong -- end */ |
| } |
| |
| { /* jlong -- begin */ |
| Aig_Obj_t * pNode2 = pObjMap[nFrames*Aig_ObjId(pObjR)+2]; |
| Aig_Obj_t * pFan0 = Aig_NotCond( pNode0, Aig_IsComplement(pObj) ); |
| Aig_Obj_t * pFan1 = Aig_NotCond( pNode1, Aig_IsComplement(pObj) ); |
| Aig_Obj_t * pFan2 = Aig_NotCond( pNode2, !Aig_IsComplement(pObj) ); |
| Aig_Obj_t * pMiter = Aig_And( pFrames, Aig_And(pFrames, pFan0, pFan1 ), pFan2); |
| Aig_ObjCreateCo( pFrames, pMiter ); /* jlong -- end */ |
| } |
| |
| } |
| } |
| Aig_ManCleanup( pFrames ); |
| ABC_FREE( pObjMap ); |
| |
| //Aig_ManShow( pAig, 0, NULL ); |
| //Aig_ManShow( pFrames, 0, NULL ); |
| return pFrames; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Detects constraints functionally.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Saig_ManFilterUsingInd2( 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_ManCreateIndMiter2( p, vCands ); |
| assert( Aig_ManCoNum(pFrames) == Vec_VecSizeSize(vCands)*3 ); |
| // 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: \n" ); |
| Counter = 0; |
| Vec_VecForEachLevel( vCands, vNodes, i ) |
| { |
| assert(i==0); /* only one item */ |
| k2 = 0; |
| Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, k ) |
| { |
| if ( Saig_ManFilterUsingIndOne2( p, pFrames, pSat, pCnf, nConfs, nProps, Counter++ , 0) == l_False) |
| // if ( Saig_ManFilterUsingIndOne_old( p, pSat, pCnf, nConfs, pObj ) ) |
| { |
| Vec_PtrWriteEntry( vNodes, k2++, pObj ); |
| if ( fVerbose ) |
| printf( "%d:%s%d \n", i, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) ); |
| printf( " type I : %d:%s%d \n", i, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) ); |
| Vec_PtrPush(p->unfold2_type_I, pObj); |
| } |
| /* jlong -- begin */ |
| else if ( Saig_ManFilterUsingIndOne2( p, pFrames, pSat, pCnf, nConfs, nProps, Counter-1 , 1) == l_True ) /* can be self-conflicting */ |
| { |
| if ( Saig_ManFilterUsingIndOne2( p, pFrames, pSat, pCnf, nConfs, nProps, Counter-1 , 2) == l_False ){ |
| //Vec_PtrWriteEntry( vNodes, k2++, pObj ); |
| if ( fVerbose ) |
| printf( "%d:%s%d \n", i, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) ); |
| printf( " type II: %d:%s%d \n", i, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) ); |
| Vec_PtrWriteEntry( vNodes, k2++, pObj ); /* add type II constraints */ |
| Vec_PtrPush(p->unfold2_type_II, pObj); |
| } |
| } |
| /* jlong -- end */ |
| } |
| Vec_PtrShrink( vNodes, k2 ); |
| } |
| |
| // clean up |
| Cnf_DataFree( pCnf ); |
| sat_solver_delete( pSat ); |
| if ( fVerbose ) |
| Aig_ManPrintStats( pFrames ); |
| Aig_ManStop( pFrames ); |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Returns the number of variables implied by the output.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Vec_Vec_t * Ssw_ManFindDirectImplications2( 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; |
| assert(nFrames == 1); |
| vCands = Vec_VecAlloc( nFrames ); |
| assert(nFrames == 1); |
| // 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; |
| //--jlong : also use internal nodes as well |
| /* if ( !Aig_ObjIsCi(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 ); |
| /* -- jlong -- this does the SAT proof of the constraints */ |
| Saig_ManFilterUsingInd2( 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 [Duplicates the AIG while unfolding constraints.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Aig_Man_t * Saig_ManDupUnfoldConstrsFunc2( Aig_Man_t * pAig, int nFrames, int nConfs, int nProps, int fOldAlgo, int fVerbose , int * typeII_cnt){ |
| Aig_Man_t * pNew; |
| Vec_Vec_t * vCands; |
| Vec_Ptr_t * vNewFlops; |
| Aig_Obj_t * pObj; |
| int i, k, nNewFlops; |
| const int fCompl = 0 ; |
| if ( fOldAlgo ) |
| vCands = Saig_ManDetectConstrFunc( pAig, nFrames, nConfs, nProps, fVerbose ); |
| else |
| vCands = Ssw_ManFindDirectImplications2( 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 ); /* good */ |
| pNew->nConstrs = pAig->nConstrs + Vec_VecSizeSize(vCands); |
| pNew->nConstrs = pAig->nConstrs + Vec_PtrSize(pAig->unfold2_type_II) |
| + Vec_PtrSize(pAig->unfold2_type_I); |
| // pNew->nConstrsTypeII = Vec_PtrSize(pAig->unfold2_type_II); |
| *typeII_cnt = Vec_PtrSize(pAig->unfold2_type_II); |
| |
| /* new set of registers */ |
| |
| // add normal POs |
| Saig_ManForEachPo( pAig, pObj, i ) |
| Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) ); |
| // create constraint outputs |
| vNewFlops = Vec_PtrAlloc( 100 ); |
| |
| |
| Vec_PtrForEachEntry(Aig_Obj_t * , pAig->unfold2_type_I, pObj, k){ |
| Aig_Obj_t * x = Aig_ObjRealCopy(pObj); |
| Aig_ObjCreateCo(pNew, x); |
| } |
| |
| Vec_PtrForEachEntry(Aig_Obj_t * , pAig->unfold2_type_II, pObj, k){ |
| Aig_Obj_t * type_II_latch |
| = Aig_ObjCreateCi(pNew); /* will get connected later; */ |
| Aig_Obj_t * x = Aig_ObjRealCopy(pObj); |
| |
| Aig_Obj_t * n = Aig_And(pNew, |
| Aig_NotCond(type_II_latch, fCompl), |
| Aig_NotCond(x, fCompl)); |
| Aig_ObjCreateCo(pNew, n);//Aig_Not(n)); |
| } |
| |
| // add latch outputs |
| Saig_ManForEachLi( pAig, pObj, i ) |
| Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) ); |
| |
| Vec_PtrForEachEntry(Aig_Obj_t * , pAig->unfold2_type_II, pObj, k){ |
| Aig_Obj_t * x = Aig_ObjRealCopy(pObj); |
| Aig_ObjCreateCo(pNew, x); |
| } |
| |
| // add new latch outputs |
| nNewFlops = Vec_PtrSize(pAig->unfold2_type_II); |
| //assert( nNewFlops == Vec_PtrSize(vNewFlops) ); |
| Aig_ManSetRegNum( pNew, Aig_ManRegNum(pAig) + nNewFlops ); |
| printf("#reg after unfold2: %d\n", 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_ManDupFoldConstrsFunc2( Aig_Man_t * pAig, int fCompl, int fVerbose , |
| int typeII_cnt) |
| { |
| Aig_Man_t * pAigNew; |
| Aig_Obj_t * pMiter, * pFlopOut, * pFlopIn, * pObj; |
| int i, typeII_cc, type_II; |
| 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 ); |
| typeII_cc = 0;//typeII_cnt; |
| typeII_cnt = 0; |
| type_II = 0; |
| |
| Saig_ManForEachPo( pAig, pObj, i ) |
| { |
| |
| if ( i < Saig_ManPoNum(pAig)-Aig_ManConstrNum(pAig) ) |
| continue; |
| if (i + typeII_cnt >= Saig_ManPoNum(pAig) ) { |
| type_II = 1; |
| } |
| /* now we got the constraint */ |
| if (type_II) { |
| |
| Aig_Obj_t * type_II_latch |
| = Aig_ObjCreateCi(pAigNew); /* will get connected later; */ |
| pMiter = Aig_Or(pAigNew, pMiter, |
| Aig_And(pAigNew, |
| Aig_NotCond(type_II_latch, fCompl), |
| Aig_NotCond( Aig_ObjChild0Copy(pObj), fCompl ) ) |
| ); |
| printf( "modeling typeII : %d:%s%d \n", i, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) ); |
| } else |
| 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 |
| { |
| /* the same for type I and type II */ |
| Aig_Obj_t * pObjLi, *pObjLo; |
| |
| Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i ) { |
| if( i + typeII_cc < Aig_ManRegNum(pAig)) { |
| Aig_Obj_t *c = Aig_Mux(pAigNew, Aig_Not(pFlopIn), |
| Aig_ObjChild0Copy(pObjLi) , |
| (Aig_Obj_t*)pObjLo->pData); |
| Aig_ObjCreateCo( pAigNew, c); |
| } else { |
| printf ( "skipping: reg%d\n", i); |
| Aig_ObjCreateCo( pAigNew,Aig_ObjChild0Copy(pObjLi)); |
| } |
| } |
| |
| } |
| if(0)Saig_ManForEachLi( pAig, pObj, i ) { |
| Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) ); |
| } |
| Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig) ); |
| |
| type_II = 0; |
| Saig_ManForEachPo( pAig, pObj, i ) |
| { |
| |
| if ( i < Saig_ManPoNum(pAig)-Aig_ManConstrNum(pAig) ) |
| continue; |
| if (i + typeII_cnt >= Saig_ManPoNum(pAig) ) { |
| type_II = 1; |
| } |
| /* now we got the constraint */ |
| if (type_II) { |
| Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj)); |
| Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAigNew)+1 ); |
| printf( "Latch for typeII : %d:%s%d \n", i, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) ); |
| } |
| } |
| |
| |
| // create additional flop |
| |
| if ( Saig_ManRegNum(pAig) > 0 ) |
| { |
| Aig_ObjCreateCo( pAigNew, pFlopIn ); |
| Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAigNew)+1 ); |
| } |
| printf("#reg after fold2: %d\n", Aig_ManRegNum(pAigNew)); |
| // perform cleanup |
| Aig_ManCleanup( pAigNew ); |
| Aig_ManSeqCleanup( pAigNew ); |
| return pAigNew; |
| } |
