diff options
Diffstat (limited to 'src/aig/saig/saigConstr2.c')
-rw-r--r-- | src/aig/saig/saigConstr2.c | 1001 |
1 files changed, 1001 insertions, 0 deletions
diff --git a/src/aig/saig/saigConstr2.c b/src/aig/saig/saigConstr2.c new file mode 100644 index 00000000..a5a575fd --- /dev/null +++ b/src/aig/saig/saigConstr2.c @@ -0,0 +1,1001 @@ +/**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 "cnf.h" +#include "satSolver.h" +#include "kit.h" +#include "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, clk = 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_ManForEachPo( 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", clock() - clk ); + // print the state + if ( fVerbose ) + { + Saig_ManForEachPo( p, pObj, i ) + { + if ( i < Saig_ManPoNum(p) - Saig_ManConstrNum(p) ) + printf( "Primary output : ", i ); + 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 = Aig_UtilStrsav( pAig->pName ); + pFrames->pSpec = Aig_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_ObjCreatePi(pFrames) ); + // set initial state for the latches + Aig_ManForEachLoSeq( pAig, pObj, i ) + Aig_ObjSetFrames( pObjMap, nFrames, pObj, 0, Aig_ObjCreatePi(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_ObjCreatePo( 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_ManPo( 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_ManPoNum(pFrames) == Vec_VecSizeSize(vCands) ); + // start the SAT solver + pCnf = Cnf_DeriveSimple( pFrames, Aig_ManPoNum(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 = Aig_UtilStrsav( pAig->pName ); + pFrames->pSpec = Aig_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_ObjCreatePi(pFrames) ); + // set initial state for the latches + Aig_ManForEachLoSeq( pAig, pObj, i ) + Aig_ObjSetFrames( pObjMap, nFrames, pObj, 0, Aig_ObjCreatePi(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_ObjCreatePo( 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_ObjIsPi(pObj) ) + continue; + assert( pCnf->pVarNums[i] > 0 ); + pInfo = (unsigned *)Vec_PtrEntry( vInfo, i ); + if ( Aig_InfoHasBit(pInfo, *piPat) != sat_solver_var_value(pSat, pCnf->pVarNums[i]) ) + Aig_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_ManPo( 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_ManPoNum(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)] ]; + 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_ManPoNum(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_ManPoNum(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_ManPo(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_ObjIsPi(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_ObjIsPi(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_Ptr_t *)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_Ptr_t *)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_ObjCreatePo( 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_ObjCreatePi(pNew) ); + Aig_ObjCreatePo( pNew, (Aig_Obj_t *)Vec_PtrPop(vNewFlops) ); + } + } + // add latch outputs + Saig_ManForEachLi( pAig, pObj, i ) + Aig_ObjCreatePo( 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_ObjCreatePo( 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; + assert( Saig_ManRegNum(pAig) > 0 ); + 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 = Aig_UtilStrsav( pAig->pName ); + pAigNew->pSpec = Aig_UtilStrsav( pAig->pSpec ); + // map the constant node + Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew ); + // create variables for PIs + Aig_ManForEachPi( pAig, pObj, i ) + pObj->pData = Aig_ObjCreatePi( 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 + pFlopOut = Aig_ObjCreatePi( pAigNew ); + pFlopIn = Aig_Or( pAigNew, pMiter, pFlopOut ); + + // 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_ObjCreatePo( pAigNew, pMiter ); + } + + // transfer to register outputs + Saig_ManForEachLi( pAig, pObj, i ) + Aig_ObjCreatePo( pAigNew, Aig_ObjChild0Copy(pObj) ); + // create additional flop + Aig_ObjCreatePo( pAigNew, pFlopIn ); + + Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig)+1 ); + Aig_ManCleanup( pAigNew ); + Aig_ManSeqCleanup( pAigNew ); + return pAigNew; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + |