1 /**CFile****************************************************************
2
3 FileName [llb2Bad.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [BDD based reachability.]
8
9 Synopsis [Computing bad states.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: llb2Bad.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "llbInt.h"
22
23 ABC_NAMESPACE_IMPL_START
24
25
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29
30 ////////////////////////////////////////////////////////////////////////
31 /// FUNCTION DEFINITIONS ///
32 ////////////////////////////////////////////////////////////////////////
33
34 /**Function*************************************************************
35
36 Synopsis [Computes bad in working manager.]
37
38 Description []
39
40 SideEffects []
41
42 SeeAlso []
43
44 ***********************************************************************/
Llb_BddComputeBad(Aig_Man_t * pInit,DdManager * dd,abctime TimeOut)45 DdNode * Llb_BddComputeBad( Aig_Man_t * pInit, DdManager * dd, abctime TimeOut )
46 {
47 Vec_Ptr_t * vNodes;
48 DdNode * bBdd0, * bBdd1, * bTemp, * bResult;
49 Aig_Obj_t * pObj;
50 int i, k;
51 assert( Cudd_ReadSize(dd) == Aig_ManCiNum(pInit) );
52 // initialize elementary variables
53 Aig_ManConst1(pInit)->pData = Cudd_ReadOne( dd );
54 Saig_ManForEachLo( pInit, pObj, i )
55 pObj->pData = Cudd_bddIthVar( dd, i );
56 Saig_ManForEachPi( pInit, pObj, i )
57 pObj->pData = Cudd_bddIthVar( dd, Aig_ManRegNum(pInit) + i );
58 // compute internal nodes
59 vNodes = Aig_ManDfsNodes( pInit, (Aig_Obj_t **)Vec_PtrArray(pInit->vCos), Saig_ManPoNum(pInit) );
60 Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
61 {
62 if ( !Aig_ObjIsNode(pObj) )
63 continue;
64 bBdd0 = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
65 bBdd1 = Cudd_NotCond( (DdNode *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) );
66 // pObj->pData = Extra_bddAndTime( dd, bBdd0, bBdd1, TimeOut );
67 pObj->pData = Cudd_bddAnd( dd, bBdd0, bBdd1 );
68 if ( pObj->pData == NULL )
69 {
70 Vec_PtrForEachEntryStop( Aig_Obj_t *, vNodes, pObj, k, i )
71 if ( pObj->pData )
72 Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData );
73 Vec_PtrFree( vNodes );
74 return NULL;
75 }
76 Cudd_Ref( (DdNode *)pObj->pData );
77 }
78 // quantify PIs of each PO
79 bResult = Cudd_ReadLogicZero( dd ); Cudd_Ref( bResult );
80 Saig_ManForEachPo( pInit, pObj, i )
81 {
82 bBdd0 = Cudd_NotCond( Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
83 bResult = Cudd_bddOr( dd, bTemp = bResult, bBdd0 ); Cudd_Ref( bResult );
84 Cudd_RecursiveDeref( dd, bTemp );
85 }
86 // deref
87 Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
88 {
89 if ( !Aig_ObjIsNode(pObj) )
90 continue;
91 Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData );
92 }
93 Vec_PtrFree( vNodes );
94 Cudd_Deref( bResult );
95 return bResult;
96 }
97
98 /**Function*************************************************************
99
100 Synopsis []
101
102 Description []
103
104 SideEffects []
105
106 SeeAlso []
107
108 ***********************************************************************/
Llb_BddQuantifyPis(Aig_Man_t * pInit,DdManager * dd,DdNode * bFunc)109 DdNode * Llb_BddQuantifyPis( Aig_Man_t * pInit, DdManager * dd, DdNode * bFunc )
110 {
111 DdNode * bVar, * bCube, * bTemp;
112 Aig_Obj_t * pObj;
113 int i;
114 abctime TimeStop;
115 assert( Cudd_ReadSize(dd) == Aig_ManCiNum(pInit) );
116 TimeStop = dd->TimeStop; dd->TimeStop = 0;
117 // create PI cube
118 bCube = Cudd_ReadOne( dd ); Cudd_Ref( bCube );
119 Saig_ManForEachPi( pInit, pObj, i ) {
120 bVar = Cudd_bddIthVar( dd, Aig_ManRegNum(pInit) + i );
121 bCube = Cudd_bddAnd( dd, bTemp = bCube, bVar ); Cudd_Ref( bCube );
122 Cudd_RecursiveDeref( dd, bTemp );
123 }
124 // quantify PI cube
125 bFunc = Cudd_bddExistAbstract( dd, bFunc, bCube ); Cudd_Ref( bFunc );
126 Cudd_RecursiveDeref( dd, bCube );
127 Cudd_Deref( bFunc );
128 dd->TimeStop = TimeStop;
129 return bFunc;
130 }
131
132 ////////////////////////////////////////////////////////////////////////
133 /// END OF FILE ///
134 ////////////////////////////////////////////////////////////////////////
135
136
137 ABC_NAMESPACE_IMPL_END
138
139