1 /**CFile****************************************************************
2
3 FileName [llb1Man.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [BDD based reachability.]
8
9 Synopsis [Reachability manager.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: llb1Man.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 []
37
38 Description []
39
40 SideEffects []
41
42 SeeAlso []
43
44 ***********************************************************************/
Llb_ManPrepareVarMap(Llb_Man_t * p)45 void Llb_ManPrepareVarMap( Llb_Man_t * p )
46 {
47 Aig_Obj_t * pObjLi, * pObjLo;
48 int i, iVarLi, iVarLo;
49 assert( p->vNs2Glo == NULL );
50 assert( p->vCs2Glo == NULL );
51 assert( p->vGlo2Cs == NULL );
52 assert( p->vGlo2Ns == NULL );
53 p->vNs2Glo = Vec_IntStartFull( Vec_IntSize(p->vVar2Obj) );
54 p->vCs2Glo = Vec_IntStartFull( Vec_IntSize(p->vVar2Obj) );
55 p->vGlo2Cs = Vec_IntStartFull( Aig_ManRegNum(p->pAig) );
56 p->vGlo2Ns = Vec_IntStartFull( Aig_ManRegNum(p->pAig) );
57 Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
58 {
59 iVarLi = Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObjLi));
60 iVarLo = Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObjLo));
61 assert( iVarLi >= 0 && iVarLi < Vec_IntSize(p->vVar2Obj) );
62 assert( iVarLo >= 0 && iVarLo < Vec_IntSize(p->vVar2Obj) );
63 Vec_IntWriteEntry( p->vNs2Glo, iVarLi, i );
64 Vec_IntWriteEntry( p->vCs2Glo, iVarLo, i );
65 Vec_IntWriteEntry( p->vGlo2Cs, i, iVarLo );
66 Vec_IntWriteEntry( p->vGlo2Ns, i, iVarLi );
67 }
68 // add mapping of the PIs
69 Saig_ManForEachPi( p->pAig, pObjLo, i )
70 {
71 iVarLo = Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObjLo));
72 Vec_IntWriteEntry( p->vCs2Glo, iVarLo, Aig_ManRegNum(p->pAig)+i );
73 Vec_IntWriteEntry( p->vNs2Glo, iVarLo, Aig_ManRegNum(p->pAig)+i );
74 }
75 }
76
77 /**Function*************************************************************
78
79 Synopsis []
80
81 Description []
82
83 SideEffects []
84
85 SeeAlso []
86
87 ***********************************************************************/
Llb_ManPrepareVarLimits(Llb_Man_t * p)88 void Llb_ManPrepareVarLimits( Llb_Man_t * p )
89 {
90 Llb_Grp_t * pGroup;
91 Aig_Obj_t * pVar;
92 int i, k;
93 assert( p->vVarBegs == NULL );
94 assert( p->vVarEnds == NULL );
95 p->vVarEnds = Vec_IntStart( Aig_ManObjNumMax(p->pAig) );
96 p->vVarBegs = Vec_IntStart( Aig_ManObjNumMax(p->pAig) );
97 Vec_IntFill( p->vVarBegs, Aig_ManObjNumMax(p->pAig), p->pMatrix->nCols );
98
99 for ( i = 0; i < p->pMatrix->nCols; i++ )
100 {
101 pGroup = p->pMatrix->pColGrps[i];
102
103 Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pVar, k )
104 if ( Vec_IntEntry(p->vVarBegs, pVar->Id) > i )
105 Vec_IntWriteEntry( p->vVarBegs, pVar->Id, i );
106 Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pVar, k )
107 if ( Vec_IntEntry(p->vVarBegs, pVar->Id) > i )
108 Vec_IntWriteEntry( p->vVarBegs, pVar->Id, i );
109
110 Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pVar, k )
111 if ( Vec_IntEntry(p->vVarEnds, pVar->Id) < i )
112 Vec_IntWriteEntry( p->vVarEnds, pVar->Id, i );
113 Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pVar, k )
114 if ( Vec_IntEntry(p->vVarEnds, pVar->Id) < i )
115 Vec_IntWriteEntry( p->vVarEnds, pVar->Id, i );
116 }
117 }
118
119 /**Function*************************************************************
120
121 Synopsis []
122
123 Description []
124
125 SideEffects []
126
127 SeeAlso []
128
129 ***********************************************************************/
Llb_ManStop(Llb_Man_t * p)130 void Llb_ManStop( Llb_Man_t * p )
131 {
132 Llb_Grp_t * pGrp;
133 DdNode * bTemp;
134 int i;
135
136 // Vec_IntFreeP( &p->vMem );
137 // Vec_PtrFreeP( &p->vTops );
138 // Vec_PtrFreeP( &p->vBots );
139 // Vec_VecFreeP( (Vec_Vec_t **)&p->vCuts );
140
141 if ( p->pMatrix )
142 Llb_MtrFree( p->pMatrix );
143 Vec_PtrForEachEntry( Llb_Grp_t *, p->vGroups, pGrp, i )
144 Llb_ManGroupStop( pGrp );
145 if ( p->dd )
146 {
147 // printf( "Manager dd\n" );
148 Extra_StopManager( p->dd );
149 }
150 if ( p->ddG )
151 {
152 // printf( "Manager ddG\n" );
153 if ( p->ddG->bFunc )
154 Cudd_RecursiveDeref( p->ddG, p->ddG->bFunc );
155 Extra_StopManager( p->ddG );
156 }
157 if ( p->ddR )
158 {
159 // printf( "Manager ddR\n" );
160 if ( p->ddR->bFunc )
161 Cudd_RecursiveDeref( p->ddR, p->ddR->bFunc );
162 Vec_PtrForEachEntry( DdNode *, p->vRings, bTemp, i )
163 Cudd_RecursiveDeref( p->ddR, bTemp );
164 Extra_StopManager( p->ddR );
165 }
166 Aig_ManStop( p->pAig );
167 Vec_PtrFreeP( &p->vGroups );
168 Vec_IntFreeP( &p->vVar2Obj );
169 Vec_IntFreeP( &p->vObj2Var );
170 Vec_IntFreeP( &p->vVarBegs );
171 Vec_IntFreeP( &p->vVarEnds );
172 Vec_PtrFreeP( &p->vRings );
173 Vec_IntFreeP( &p->vNs2Glo );
174 Vec_IntFreeP( &p->vCs2Glo );
175 Vec_IntFreeP( &p->vGlo2Cs );
176 Vec_IntFreeP( &p->vGlo2Ns );
177 // Vec_IntFreeP( &p->vHints );
178 ABC_FREE( p );
179 }
180
181
182 /**Function*************************************************************
183
184 Synopsis []
185
186 Description []
187
188 SideEffects []
189
190 SeeAlso []
191
192 ***********************************************************************/
Llb_ManStart(Aig_Man_t * pAigGlo,Aig_Man_t * pAig,Gia_ParLlb_t * pPars)193 Llb_Man_t * Llb_ManStart( Aig_Man_t * pAigGlo, Aig_Man_t * pAig, Gia_ParLlb_t * pPars )
194 {
195 Llb_Man_t * p;
196 Aig_ManCleanMarkA( pAig );
197 p = ABC_CALLOC( Llb_Man_t, 1 );
198 p->pAigGlo = pAigGlo;
199 p->pPars = pPars;
200 p->pAig = pAig;
201 p->vVar2Obj = Llb_ManMarkPivotNodes( p->pAig, pPars->fUsePivots );
202 p->vObj2Var = Vec_IntInvert( p->vVar2Obj, -1 );
203 p->vRings = Vec_PtrAlloc( 100 );
204 Llb_ManPrepareVarMap( p );
205 Llb_ManPrepareGroups( p );
206 Aig_ManCleanMarkA( pAig );
207 p->pMatrix = Llb_MtrCreate( p );
208 p->pMatrix->pMan = p;
209 return p;
210 }
211
212 ////////////////////////////////////////////////////////////////////////
213 /// END OF FILE ///
214 ////////////////////////////////////////////////////////////////////////
215
216
217 ABC_NAMESPACE_IMPL_END
218
219