| /**CFile**************************************************************** |
| |
| FileName [llb1Constr.c] |
| |
| SystemName [ABC: Logic synthesis and verification system.] |
| |
| PackageName [BDD based reachability.] |
| |
| Synopsis [Computing inductive constraints.] |
| |
| Author [Alan Mishchenko] |
| |
| Affiliation [UC Berkeley] |
| |
| Date [Ver. 1.0. Started - June 20, 2005.] |
| |
| Revision [$Id: llb1Constr.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 the array of constraint candidates.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Llb_ManCountEntries( Vec_Int_t * vCands ) |
| { |
| int i, Entry, Counter = 0; |
| Vec_IntForEachEntry( vCands, Entry, i ) |
| Counter += ((Entry == 0) || (Entry == 1)); |
| return Counter; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Returns the array of constraint candidates.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Llb_ManPrintEntries( Aig_Man_t * p, Vec_Int_t * vCands ) |
| { |
| int i, Entry; |
| if ( vCands == NULL ) |
| { |
| printf( "There is no hints.\n" ); |
| return; |
| } |
| Entry = Llb_ManCountEntries(vCands); |
| printf( "\n*** Using %d hint%s:\n", Entry, (Entry != 1 ? "s":"") ); |
| Vec_IntForEachEntry( vCands, Entry, i ) |
| { |
| if ( Entry != 0 && Entry != 1 ) |
| continue; |
| printf( "%c", Entry ? '+' : '-' ); |
| printf( "%-6d : ", i ); |
| Aig_ObjPrint( p, Aig_ManObj(p, i) ); |
| printf( "\n" ); |
| } |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Dereference BDD nodes.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Llb_ManDerefenceBdds( Aig_Man_t * p, DdManager * dd ) |
| { |
| Aig_Obj_t * pObj; |
| int i; |
| Aig_ManForEachObj( p, pObj, i ) |
| Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Returns the array of constraint candidates.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| DdNode * Llb_ManComputeIndCase_rec( Aig_Man_t * p, Aig_Obj_t * pObj, DdManager * dd, Vec_Ptr_t * vBdds ) |
| { |
| DdNode * bBdd0, * bBdd1; |
| DdNode * bFunc = (DdNode *)Vec_PtrEntry( vBdds, Aig_ObjId(pObj) ); |
| if ( bFunc != NULL ) |
| return bFunc; |
| assert( Aig_ObjIsNode(pObj) ); |
| bBdd0 = Llb_ManComputeIndCase_rec( p, Aig_ObjFanin0(pObj), dd, vBdds ); |
| bBdd1 = Llb_ManComputeIndCase_rec( p, Aig_ObjFanin1(pObj), dd, vBdds ); |
| bBdd0 = Cudd_NotCond( bBdd0, Aig_ObjFaninC0(pObj) ); |
| bBdd1 = Cudd_NotCond( bBdd1, Aig_ObjFaninC1(pObj) ); |
| bFunc = Cudd_bddAnd( dd, bBdd0, bBdd1 ); Cudd_Ref( bFunc ); |
| Vec_PtrWriteEntry( vBdds, Aig_ObjId(pObj), bFunc ); |
| return bFunc; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Returns the array of constraint candidates.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Llb_ManComputeIndCase( Aig_Man_t * p, DdManager * dd, Vec_Int_t * vNodes ) |
| { |
| Vec_Ptr_t * vBdds; |
| Aig_Obj_t * pObj; |
| DdNode * bFunc; |
| int i, Entry; |
| vBdds = Vec_PtrStart( Aig_ManObjNumMax(p) ); |
| bFunc = Cudd_ReadOne(dd); Cudd_Ref( bFunc ); |
| Vec_PtrWriteEntry( vBdds, Aig_ObjId(Aig_ManConst1(p)), bFunc ); |
| Saig_ManForEachPi( p, pObj, i ) |
| { |
| bFunc = Cudd_bddIthVar( dd, Aig_ManCiNum(p) + i ); Cudd_Ref( bFunc ); |
| Vec_PtrWriteEntry( vBdds, Aig_ObjId(pObj), bFunc ); |
| } |
| Saig_ManForEachLi( p, pObj, i ) |
| { |
| bFunc = (DdNode *)pObj->pData; Cudd_Ref( bFunc ); |
| Vec_PtrWriteEntry( vBdds, Aig_ObjId(Saig_ObjLiToLo(p, pObj)), bFunc ); |
| } |
| Vec_IntForEachEntry( vNodes, Entry, i ) |
| { |
| if ( Entry != 0 && Entry != 1 ) |
| continue; |
| pObj = Aig_ManObj( p, i ); |
| bFunc = Llb_ManComputeIndCase_rec( p, pObj, dd, vBdds ); |
| if ( Entry == 0 ) |
| { |
| // Extra_bddPrint( dd, Cudd_Not(pObj->pData) ); printf( "\n" ); |
| // Extra_bddPrint( dd, Cudd_Not(bFunc) ); printf( "\n" ); |
| if ( !Cudd_bddLeq( dd, Cudd_Not(pObj->pData), Cudd_Not(bFunc) ) ) |
| Vec_IntWriteEntry( vNodes, i, -1 ); |
| } |
| else if ( Entry == 1 ) |
| { |
| // Extra_bddPrint( dd, pObj->pData ); printf( "\n" ); |
| // Extra_bddPrint( dd, bFunc ); printf( "\n" ); |
| if ( !Cudd_bddLeq( dd, (DdNode *)pObj->pData, bFunc ) ) |
| Vec_IntWriteEntry( vNodes, i, -1 ); |
| } |
| } |
| Vec_PtrForEachEntry( DdNode *, vBdds, bFunc, i ) |
| if ( bFunc ) |
| Cudd_RecursiveDeref( dd, bFunc ); |
| Vec_PtrFree( vBdds ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Returns the array of constraint candidates.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Vec_Int_t * Llb_ManComputeBaseCase( Aig_Man_t * p, DdManager * dd ) |
| { |
| Vec_Int_t * vNodes; |
| Aig_Obj_t * pObj, * pRoot; |
| int i; |
| pRoot = Aig_ManCo( p, 0 ); |
| vNodes = Vec_IntStartFull( Aig_ManObjNumMax(p) ); |
| Aig_ManForEachObj( p, pObj, i ) |
| { |
| if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) ) |
| continue; |
| if ( Cudd_bddLeq( dd, (DdNode *)pObj->pData, Cudd_Not(pRoot->pData) ) ) |
| Vec_IntWriteEntry( vNodes, i, 1 ); |
| else if ( Cudd_bddLeq( dd, Cudd_Not((DdNode *)pObj->pData), Cudd_Not(pRoot->pData) ) ) |
| Vec_IntWriteEntry( vNodes, i, 0 ); |
| } |
| return vNodes; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Constructs global BDDs for each object in the AIG manager.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| DdManager * Llb_ManConstructGlobalBdds( Aig_Man_t * p ) |
| { |
| DdManager * dd; |
| DdNode * bBdd0, * bBdd1; |
| Aig_Obj_t * pObj; |
| int i; |
| dd = Cudd_Init( Aig_ManCiNum(p), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); |
| Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT ); |
| pObj = Aig_ManConst1(p); |
| pObj->pData = Cudd_ReadOne(dd); Cudd_Ref( (DdNode *)pObj->pData ); |
| Aig_ManForEachCi( p, pObj, i ) |
| { |
| pObj->pData = Cudd_bddIthVar(dd, i); Cudd_Ref( (DdNode *)pObj->pData ); |
| } |
| Aig_ManForEachNode( p, pObj, i ) |
| { |
| bBdd0 = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) ); |
| bBdd1 = Cudd_NotCond( (DdNode *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) ); |
| pObj->pData = Cudd_bddAnd( dd, bBdd0, bBdd1 ); Cudd_Ref( (DdNode *)pObj->pData ); |
| } |
| Aig_ManForEachCo( p, pObj, i ) |
| { |
| pObj->pData = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) ); Cudd_Ref( (DdNode *)pObj->pData ); |
| } |
| return dd; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Derives inductive constraints.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Vec_Int_t * Llb_ManDeriveConstraints( Aig_Man_t * p ) |
| { |
| DdManager * dd; |
| Vec_Int_t * vNodes; |
| if ( Saig_ManPoNum(p) != 1 ) |
| { |
| printf( "The AIG has %d property outputs.\n", Saig_ManPoNum(p) ); |
| return NULL; |
| } |
| assert( Saig_ManPoNum(p) == 1 ); |
| dd = Llb_ManConstructGlobalBdds( p ); |
| vNodes = Llb_ManComputeBaseCase( p, dd ); |
| if ( Llb_ManCountEntries(vNodes) > 0 ) |
| Llb_ManComputeIndCase( p, dd, vNodes ); |
| if ( Llb_ManCountEntries(vNodes) == 0 ) |
| Vec_IntFreeP( &vNodes ); |
| Llb_ManDerefenceBdds( p, dd ); |
| Extra_StopManager( dd ); |
| return vNodes; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Tests derived constraints.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Llb_ManConstrTest( Aig_Man_t * p ) |
| { |
| Vec_Int_t * vNodes; |
| vNodes = Llb_ManDeriveConstraints( p ); |
| Llb_ManPrintEntries( p, vNodes ); |
| Vec_IntFreeP( &vNodes ); |
| } |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
