1 /**CFile****************************************************************
2
3 FileName [giaFront.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Scalable AIG package.]
8
9 Synopsis [Frontier representation.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: giaFront.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "gia.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 [Find the next place on the frontier.]
37
38 Description []
39
40 SideEffects []
41
42 SeeAlso []
43
44 ***********************************************************************/
Gia_ManFrontFindNext(char * pFront,int nFront,int iFront)45 static inline int Gia_ManFrontFindNext( char * pFront, int nFront, int iFront )
46 {
47 assert( iFront < nFront );
48 for ( ; pFront[iFront]; iFront = (iFront + 1) % nFront );
49 assert( pFront[iFront] == 0 );
50 pFront[iFront] = 1;
51 return iFront;
52 }
53
54 /**Function*************************************************************
55
56 Synopsis [Transforms the frontier manager to its initial state.]
57
58 Description []
59
60 SideEffects []
61
62 SeeAlso []
63
64 ***********************************************************************/
Gia_ManFrontTransform(Gia_Man_t * p)65 void Gia_ManFrontTransform( Gia_Man_t * p )
66 {
67 Gia_Obj_t * pObj;
68 int i, * pFrontToId; // mapping of nodes into frontier variables
69 assert( p->nFront > 0 );
70 pFrontToId = ABC_FALLOC( int, p->nFront );
71 Gia_ManForEachObj( p, pObj, i )
72 {
73 if ( Gia_ObjIsCo(pObj) )
74 {
75 assert( pObj->Value == GIA_NONE );
76 pObj->iDiff0 = i - pFrontToId[Gia_ObjDiff0(pObj)];
77 }
78 else if ( Gia_ObjIsAnd(pObj) )
79 {
80 assert( (int)pObj->Value < p->nFront );
81 pObj->iDiff0 = i - pFrontToId[Gia_ObjDiff0(pObj)];
82 pObj->iDiff1 = i - pFrontToId[Gia_ObjDiff1(pObj)];
83 pFrontToId[pObj->Value] = i;
84 }
85 else
86 {
87 assert( (int)pObj->Value < p->nFront );
88 pFrontToId[pObj->Value] = i;
89 }
90 pObj->Value = 0;
91 }
92 ABC_FREE( pFrontToId );
93 }
94
95 /**Function*************************************************************
96
97 Synopsis [Determine the frontier.]
98
99 Description []
100
101 SideEffects []
102
103 SeeAlso []
104
105 ***********************************************************************/
Gia_ManCrossCutSimple(Gia_Man_t * p)106 int Gia_ManCrossCutSimple( Gia_Man_t * p )
107 {
108 Gia_Obj_t * pObj;
109 int i, nCutCur = 0, nCutMax = 0;
110 Gia_ManCreateValueRefs( p );
111 Gia_ManForEachObj( p, pObj, i )
112 {
113 if ( pObj->Value )
114 nCutCur++;
115 if ( nCutMax < nCutCur )
116 nCutMax = nCutCur;
117 if ( Gia_ObjIsAnd(pObj) )
118 {
119 if ( --Gia_ObjFanin0(pObj)->Value == 0 )
120 nCutCur--;
121 if ( --Gia_ObjFanin1(pObj)->Value == 0 )
122 nCutCur--;
123 }
124 else if ( Gia_ObjIsCo(pObj) )
125 {
126 if ( --Gia_ObjFanin0(pObj)->Value == 0 )
127 nCutCur--;
128 }
129 }
130 // Gia_ManForEachObj( p, pObj, i )
131 // assert( pObj->Value == 0 );
132 return nCutMax;
133 }
134
135
136 /**Function*************************************************************
137
138 Synopsis [Determine the frontier.]
139
140 Description []
141
142 SideEffects []
143
144 SeeAlso []
145
146 ***********************************************************************/
Gia_ManFront(Gia_Man_t * p)147 Gia_Man_t * Gia_ManFront( Gia_Man_t * p )
148 {
149 Gia_Man_t * pNew;
150 Gia_Obj_t * pObj, * pFanin0New, * pFanin1New, * pObjNew;
151 char * pFront; // places used for the frontier
152 int i, iLit, nCrossCut = 0, nCrossCutMax = 0;
153 int nCrossCutMaxInit = Gia_ManCrossCutSimple( p );
154 int iFront = 0;//, clk = Abc_Clock();
155 // set references for all objects
156 Gia_ManCreateValueRefs( p );
157 // start the new manager
158 pNew = Gia_ManStart( Gia_ManObjNum(p) );
159 pNew->pName = Abc_UtilStrsav( p->pName );
160 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
161 pNew->nFront = 1 + (int)((float)1.1 * nCrossCutMaxInit);
162 // start the frontier
163 pFront = ABC_CALLOC( char, pNew->nFront );
164 // add constant node
165 Gia_ManConst0(pNew)->Value = iFront = Gia_ManFrontFindNext( pFront, pNew->nFront, iFront );
166 if ( Gia_ObjValue(Gia_ManConst0(p)) == 0 )
167 pFront[iFront] = 0;
168 else
169 nCrossCut = 1;
170 // iterate through the objects
171 Gia_ManForEachObj1( p, pObj, i )
172 {
173 if ( Gia_ObjIsCi(pObj) )
174 {
175 if ( Gia_ObjValue(pObj) && nCrossCutMax < ++nCrossCut )
176 nCrossCutMax = nCrossCut;
177 // create new node
178 iLit = Gia_ManAppendCi( pNew );
179 pObjNew = Gia_ManObj( pNew, Abc_Lit2Var(iLit) );
180 assert( Gia_ObjId(pNew, pObjNew) == Gia_ObjId(p, pObj) );
181 pObjNew->Value = iFront = Gia_ManFrontFindNext( pFront, pNew->nFront, iFront );
182 // handle CIs without fanout
183 if ( Gia_ObjValue(pObj) == 0 )
184 pFront[iFront] = 0;
185 continue;
186 }
187 if ( Gia_ObjIsCo(pObj) )
188 {
189 assert( Gia_ObjValue(pObj) == 0 );
190 // create new node
191 iLit = Gia_ManAppendCo( pNew, 0 );
192 pObjNew = Gia_ManObj( pNew, Abc_Lit2Var(iLit) );
193 assert( Gia_ObjId(pNew, pObjNew) == Gia_ObjId(p, pObj) );
194 // get the fanin
195 pFanin0New = Gia_ManObj( pNew, Gia_ObjFaninId0(pObj, i) );
196 assert( pFanin0New->Value != GIA_NONE );
197 pObjNew->Value = GIA_NONE;
198 pObjNew->iDiff0 = pFanin0New->Value;
199 pObjNew->fCompl0 = Gia_ObjFaninC0(pObj);
200 // deref the fanin
201 if ( --Gia_ObjFanin0(pObj)->Value == 0 )
202 {
203 pFront[pFanin0New->Value] = 0;
204 nCrossCut--;
205 }
206 continue;
207 }
208 if ( Gia_ObjValue(pObj) && nCrossCutMax < ++nCrossCut )
209 nCrossCutMax = nCrossCut;
210 // create new node
211 pObjNew = Gia_ManAppendObj( pNew );
212 assert( Gia_ObjId(pNew, pObjNew) == Gia_ObjId(p, pObj) );
213 // assign the first fanin
214 pFanin0New = Gia_ManObj( pNew, Gia_ObjFaninId0(pObj, i) );
215 assert( pFanin0New->Value != GIA_NONE );
216 pObjNew->iDiff0 = pFanin0New->Value;
217 pObjNew->fCompl0 = Gia_ObjFaninC0(pObj);
218 // assign the second fanin
219 pFanin1New = Gia_ManObj( pNew, Gia_ObjFaninId1(pObj, i) );
220 assert( pFanin1New->Value != GIA_NONE );
221 pObjNew->iDiff1 = pFanin1New->Value;
222 pObjNew->fCompl1 = Gia_ObjFaninC1(pObj);
223 // assign the frontier number
224 pObjNew->Value = iFront = Gia_ManFrontFindNext( pFront, pNew->nFront, iFront );
225 // deref the fanins
226 if ( --Gia_ObjFanin0(pObj)->Value == 0 )
227 {
228 pFront[pFanin0New->Value] = 0;
229 nCrossCut--;
230 }
231 if ( --Gia_ObjFanin1(pObj)->Value == 0 )
232 {
233 pFront[pFanin1New->Value] = 0;
234 nCrossCut--;
235 }
236 // handle nodes without fanout (choice nodes)
237 if ( Gia_ObjValue(pObj) == 0 )
238 pFront[iFront] = 0;
239 }
240 assert( pNew->nObjs == p->nObjs );
241 assert( nCrossCut == 0 || nCrossCutMax == nCrossCutMaxInit );
242 for ( i = 0; i < pNew->nFront; i++ )
243 assert( pFront[i] == 0 );
244 ABC_FREE( pFront );
245 //printf( "Crosscut = %6d. Frontier = %6d. ", nCrossCutMaxInit, pNew->nFront );
246 //ABC_PRT( "Time", Abc_Clock() - clk );
247 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
248 return pNew;
249 }
250
251 /**Function*************************************************************
252
253 Synopsis []
254
255 Description []
256
257 SideEffects []
258
259 SeeAlso []
260
261 ***********************************************************************/
Gia_ManFrontTest(Gia_Man_t * p)262 void Gia_ManFrontTest( Gia_Man_t * p )
263 {
264 Gia_Man_t * pNew;
265 pNew = Gia_ManFront( p );
266 Gia_ManFrontTransform( pNew );
267 // Gia_ManCleanValue( p );
268 // Gia_ManCleanValue( pNew );
269 if ( memcmp( pNew->pObjs, p->pObjs, sizeof(Gia_Obj_t) * p->nObjs ) )
270 {
271 /*
272 Gia_Obj_t * pObj, * pObjNew;
273 int i;
274 Gia_ManForEachObj( p, pObj, i )
275 {
276 pObjNew = Gia_ManObj( pNew, i );
277 printf( "%5d %5d %5d %5d\n",
278 pObj->iDiff0, pObjNew->iDiff0,
279 pObj->iDiff1, pObjNew->iDiff1 );
280 }
281 */
282 printf( "Verification failed.\n" );
283 }
284 else
285 printf( "Verification successful.\n" );
286 Gia_ManStop( pNew );
287 }
288
289 ////////////////////////////////////////////////////////////////////////
290 /// END OF FILE ///
291 ////////////////////////////////////////////////////////////////////////
292
293
294 ABC_NAMESPACE_IMPL_END
295
296