diff options
Diffstat (limited to 'src/proof/llb/llb1Hint.c')
| -rw-r--r-- | src/proof/llb/llb1Hint.c | 226 |
1 files changed, 226 insertions, 0 deletions
diff --git a/src/proof/llb/llb1Hint.c b/src/proof/llb/llb1Hint.c new file mode 100644 index 00000000..f68030ff --- /dev/null +++ b/src/proof/llb/llb1Hint.c @@ -0,0 +1,226 @@ +/**CFile**************************************************************** + + FileName [llb1Hint.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [BDD based reachability.] + + Synopsis [Cofactors the circuit w.r.t. the high-fanout variables.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: llb1Hint.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "llbInt.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Returns CI index with the largest number of fanouts.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Llb_ManMaxFanoutCi( Aig_Man_t * pAig ) +{ + Aig_Obj_t * pObj; + int i, WeightMax = -ABC_INFINITY, iInput = -1; + Aig_ManForEachPi( pAig, pObj, i ) + if ( WeightMax < Aig_ObjRefs(pObj) ) + { + WeightMax = Aig_ObjRefs(pObj); + iInput = i; + } + assert( iInput >= 0 ); + return iInput; +} + +/**Function************************************************************* + + Synopsis [Derives AIG whose PI is substituted by a constant.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Llb_ManPerformHints( Aig_Man_t * pAig, int nHintDepth ) +{ + Aig_Man_t * pNew, * pTemp; + int i, iInput; + pNew = Aig_ManDupDfs( pAig ); + for ( i = 0; i < nHintDepth; i++ ) + { + iInput = Llb_ManMaxFanoutCi( pNew ); + Abc_Print( 1, "%d %3d\n", i, iInput ); + pNew = Aig_ManDupCof( pTemp = pNew, iInput, 1 ); + Aig_ManStop( pTemp ); + } + return pNew; +} + +/**Function************************************************************* + + Synopsis [Returns CI index with the largest number of fanouts.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Llb_ManCollectHighFanoutObjects( Aig_Man_t * pAig, int nCandMax, int fCisOnly ) +{ + Vec_Int_t * vFanouts, * vResult; + Aig_Obj_t * pObj; + int i, fChanges, PivotValue; +// int Entry; + // collect fanout counts + vFanouts = Vec_IntAlloc( 100 ); + Aig_ManForEachObj( pAig, pObj, i ) + { +// if ( !Aig_ObjIsPi(pObj) && (fCisOnly || !Aig_ObjIsNode(pObj)) ) + if ( !Saig_ObjIsLo(pAig,pObj) && (fCisOnly || !Aig_ObjIsNode(pObj)) ) + continue; + Vec_IntPush( vFanouts, Aig_ObjRefs(pObj) ); + } + Vec_IntSort( vFanouts, 1 ); + // pick the separator + nCandMax = Abc_MinInt( nCandMax, Vec_IntSize(vFanouts) - 1 ); + PivotValue = Vec_IntEntry( vFanouts, nCandMax ); + Vec_IntFree( vFanouts ); + // collect obj satisfying the constraints + vResult = Vec_IntAlloc( 100 ); + Aig_ManForEachObj( pAig, pObj, i ) + { +// if ( !Aig_ObjIsPi(pObj) && (fCisOnly || !Aig_ObjIsNode(pObj)) ) + if ( !Saig_ObjIsLo(pAig,pObj) && (fCisOnly || !Aig_ObjIsNode(pObj)) ) + continue; + if ( Aig_ObjRefs(pObj) < PivotValue ) + continue; + Vec_IntPush( vResult, Aig_ObjId(pObj) ); + } + assert( Vec_IntSize(vResult) >= nCandMax ); + // order in the decreasing order of fanouts + do + { + fChanges = 0; + for ( i = 0; i < Vec_IntSize(vResult) - 1; i++ ) + if ( Aig_ObjRefs(Aig_ManObj(pAig, Vec_IntEntry(vResult, i))) < + Aig_ObjRefs(Aig_ManObj(pAig, Vec_IntEntry(vResult, i+1))) ) + { + int Temp = Vec_IntEntry( vResult, i ); + Vec_IntWriteEntry( vResult, i, Vec_IntEntry(vResult, i+1) ); + Vec_IntWriteEntry( vResult, i+1, Temp ); + fChanges = 1; + } + } + while ( fChanges ); +/* + Vec_IntForEachEntry( vResult, Entry, i ) + printf( "%d ", Aig_ObjRefs(Aig_ManObj(pAig, Entry)) ); +printf( "\n" ); +*/ + return vResult; +} + +/**Function************************************************************* + + Synopsis [Derives AIG whose PI is substituted by a constant.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Llb_ManModelCheckAigWithHints( Aig_Man_t * pAigGlo, Gia_ParLlb_t * pPars ) +{ + DdManager * ddGlo = NULL; + Vec_Int_t * vHints; + Vec_Int_t * vHFCands; + int i, Entry, RetValue = -1; + int clk = clock(); + assert( pPars->nHintDepth > 0 ); +/* + // perform reachability without hints + RetValue = Llb_ManModelCheckAig( pAigGlo, pPars, NULL, NULL ); + if ( RetValue >= 0 ) + return RetValue; +*/ + // create hints representation + vHFCands = Llb_ManCollectHighFanoutObjects( pAigGlo, pPars->nHintDepth+pPars->HintFirst, 1 ); + vHints = Vec_IntStartFull( Aig_ManObjNumMax(pAigGlo) ); + // add one hint at a time till the problem is solved + Vec_IntForEachEntryStart( vHFCands, Entry, i, pPars->HintFirst ) + { + Vec_IntWriteEntry( vHints, Entry, 1 ); // change to 1 to start from zero cof!!! + // solve under hints + RetValue = Llb_ManModelCheckAig( pAigGlo, pPars, vHints, &ddGlo ); + if ( RetValue == 0 ) + goto Finish; + if ( RetValue == 1 ) + break; + } + if ( RetValue == -1 ) + goto Finish; + // undo the hints one at a time + for ( ; i >= pPars->HintFirst; i-- ) + { + Entry = Vec_IntEntry( vHFCands, i ); + Vec_IntWriteEntry( vHints, Entry, -1 ); + // solve under relaxed hints + RetValue = Llb_ManModelCheckAig( pAigGlo, pPars, vHints, &ddGlo ); + if ( RetValue == 0 ) + goto Finish; + if ( RetValue == 1 ) + continue; + break; + } +Finish: + if ( ddGlo ) + { + if ( ddGlo->bFunc ) + Cudd_RecursiveDeref( ddGlo, ddGlo->bFunc ); + Extra_StopManager( ddGlo ); + } + Vec_IntFreeP( &vHFCands ); + Vec_IntFreeP( &vHints ); + if ( pPars->fVerbose ) + Abc_PrintTime( 1, "Total runtime", clock() - clk ); + return RetValue; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + |