1 /**CFile****************************************************************
2
3 FileName [giaAig.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Scalable AIG package.]
8
9 Synopsis [Transformation between AIG 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: giaAig.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "giaAig.h"
22 #include "proof/fra/fra.h"
23 #include "proof/dch/dch.h"
24 #include "opt/dar/dar.h"
25 #include "opt/dau/dau.h"
26
27 ABC_NAMESPACE_IMPL_START
28
29
30 ////////////////////////////////////////////////////////////////////////
31 /// DECLARATIONS ///
32 ////////////////////////////////////////////////////////////////////////
33
Gia_ObjChild0Copy(Aig_Obj_t * pObj)34 static inline int Gia_ObjChild0Copy( Aig_Obj_t * pObj ) { return Abc_LitNotCond( Aig_ObjFanin0(pObj)->iData, Aig_ObjFaninC0(pObj) ); }
Gia_ObjChild1Copy(Aig_Obj_t * pObj)35 static inline int Gia_ObjChild1Copy( Aig_Obj_t * pObj ) { return Abc_LitNotCond( Aig_ObjFanin1(pObj)->iData, Aig_ObjFaninC1(pObj) ); }
36
Gia_ObjChild0Copy2(Aig_Obj_t ** ppNodes,Gia_Obj_t * pObj,int Id)37 static inline Aig_Obj_t * Gia_ObjChild0Copy2( Aig_Obj_t ** ppNodes, Gia_Obj_t * pObj, int Id ) { return Aig_NotCond( ppNodes[Gia_ObjFaninId0(pObj, Id)], Gia_ObjFaninC0(pObj) ); }
Gia_ObjChild1Copy2(Aig_Obj_t ** ppNodes,Gia_Obj_t * pObj,int Id)38 static inline Aig_Obj_t * Gia_ObjChild1Copy2( Aig_Obj_t ** ppNodes, Gia_Obj_t * pObj, int Id ) { return Aig_NotCond( ppNodes[Gia_ObjFaninId1(pObj, Id)], Gia_ObjFaninC1(pObj) ); }
39
40 ////////////////////////////////////////////////////////////////////////
41 /// FUNCTION DEFINITIONS ///
42 ////////////////////////////////////////////////////////////////////////
43
44 /**Function*************************************************************
45
46 Synopsis [Duplicates AIG in the DFS order.]
47
48 Description []
49
50 SideEffects []
51
52 SeeAlso []
53
54 ***********************************************************************/
Gia_ManFromAig_rec(Gia_Man_t * pNew,Aig_Man_t * p,Aig_Obj_t * pObj)55 void Gia_ManFromAig_rec( Gia_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
56 {
57 Aig_Obj_t * pNext;
58 if ( pObj->iData )
59 return;
60 assert( Aig_ObjIsNode(pObj) );
61 Gia_ManFromAig_rec( pNew, p, Aig_ObjFanin0(pObj) );
62 Gia_ManFromAig_rec( pNew, p, Aig_ObjFanin1(pObj) );
63 pObj->iData = Gia_ManAppendAnd( pNew, Gia_ObjChild0Copy(pObj), Gia_ObjChild1Copy(pObj) );
64 if ( p->pEquivs && (pNext = Aig_ObjEquiv(p, pObj)) )
65 {
66 int iObjNew, iNextNew;
67 Gia_ManFromAig_rec( pNew, p, pNext );
68 iObjNew = Abc_Lit2Var(pObj->iData);
69 iNextNew = Abc_Lit2Var(pNext->iData);
70 if ( pNew->pNexts )
71 pNew->pNexts[iObjNew] = iNextNew;
72 }
73 }
Gia_ManFromAig(Aig_Man_t * p)74 Gia_Man_t * Gia_ManFromAig( Aig_Man_t * p )
75 {
76 Gia_Man_t * pNew;
77 Aig_Obj_t * pObj;
78 int i;
79 // create the new manager
80 pNew = Gia_ManStart( Aig_ManObjNum(p) );
81 pNew->pName = Abc_UtilStrsav( p->pName );
82 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
83 pNew->nConstrs = p->nConstrs;
84 // create room to store equivalences
85 if ( p->pEquivs )
86 pNew->pNexts = ABC_CALLOC( int, Aig_ManObjNum(p) );
87 // create the PIs
88 Aig_ManCleanData( p );
89 Aig_ManConst1(p)->iData = 1;
90 Aig_ManForEachCi( p, pObj, i )
91 pObj->iData = Gia_ManAppendCi( pNew );
92 // add logic for the POs
93 Aig_ManForEachCo( p, pObj, i )
94 Gia_ManFromAig_rec( pNew, p, Aig_ObjFanin0(pObj) );
95 Aig_ManForEachCo( p, pObj, i )
96 Gia_ManAppendCo( pNew, Gia_ObjChild0Copy(pObj) );
97 Gia_ManSetRegNum( pNew, Aig_ManRegNum(p) );
98 if ( pNew->pNexts )
99 Gia_ManDeriveReprs( pNew );
100 return pNew;
101 }
102
103 /**Function*************************************************************
104
105 Synopsis [Duplicates AIG in the DFS order.]
106
107 Description []
108
109 SideEffects []
110
111 SeeAlso []
112
113 ***********************************************************************/
Gia_ManFromAigChoices_rec(Gia_Man_t * pNew,Aig_Man_t * p,Aig_Obj_t * pObj)114 void Gia_ManFromAigChoices_rec( Gia_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
115 {
116 if ( pObj == NULL || pObj->iData )
117 return;
118 assert( Aig_ObjIsNode(pObj) );
119 Gia_ManFromAigChoices_rec( pNew, p, Aig_ObjFanin0(pObj) );
120 Gia_ManFromAigChoices_rec( pNew, p, Aig_ObjFanin1(pObj) );
121 Gia_ManFromAigChoices_rec( pNew, p, Aig_ObjEquiv(p, pObj) );
122 pObj->iData = Gia_ManAppendAnd( pNew, Gia_ObjChild0Copy(pObj), Gia_ObjChild1Copy(pObj) );
123 if ( Aig_ObjEquiv(p, pObj) )
124 {
125 int iObjNew, iNextNew;
126 iObjNew = Abc_Lit2Var(pObj->iData);
127 iNextNew = Abc_Lit2Var(Aig_ObjEquiv(p, pObj)->iData);
128 assert( iObjNew > iNextNew );
129 assert( Gia_ObjIsAnd(Gia_ManObj(pNew, iNextNew)) );
130 pNew->pSibls[iObjNew] = iNextNew;
131 }
132 }
Gia_ManFromAigChoices(Aig_Man_t * p)133 Gia_Man_t * Gia_ManFromAigChoices( Aig_Man_t * p )
134 {
135 Gia_Man_t * pNew;
136 Aig_Obj_t * pObj;
137 int i;
138 assert( p->pEquivs != NULL );
139 // create the new manager
140 pNew = Gia_ManStart( Aig_ManObjNum(p) );
141 pNew->pName = Abc_UtilStrsav( p->pName );
142 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
143 pNew->nConstrs = p->nConstrs;
144 // create room to store equivalences
145 pNew->pSibls = ABC_CALLOC( int, Aig_ManObjNum(p) );
146 // create the PIs
147 Aig_ManCleanData( p );
148 Aig_ManConst1(p)->iData = 1;
149 Aig_ManForEachCi( p, pObj, i )
150 pObj->iData = Gia_ManAppendCi( pNew );
151 // add logic for the POs
152 Aig_ManForEachCo( p, pObj, i )
153 Gia_ManFromAigChoices_rec( pNew, p, Aig_ObjFanin0(pObj) );
154 Aig_ManForEachCo( p, pObj, i )
155 Gia_ManAppendCo( pNew, Gia_ObjChild0Copy(pObj) );
156 Gia_ManSetRegNum( pNew, Aig_ManRegNum(p) );
157 //assert( Gia_ManObjNum(pNew) == Aig_ManObjNum(p) );
158 return pNew;
159 }
160
161 /**Function*************************************************************
162
163 Synopsis [Duplicates AIG in the DFS order.]
164
165 Description []
166
167 SideEffects []
168
169 SeeAlso []
170
171 ***********************************************************************/
Gia_ManFromAigSimple(Aig_Man_t * p)172 Gia_Man_t * Gia_ManFromAigSimple( Aig_Man_t * p )
173 {
174 Gia_Man_t * pNew;
175 Aig_Obj_t * pObj;
176 int i;
177 // create the new manager
178 pNew = Gia_ManStart( Aig_ManObjNum(p) );
179 pNew->pName = Abc_UtilStrsav( p->pName );
180 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
181 pNew->nConstrs = p->nConstrs;
182 // create the PIs
183 Aig_ManCleanData( p );
184 Aig_ManForEachObj( p, pObj, i )
185 {
186 if ( Aig_ObjIsAnd(pObj) )
187 pObj->iData = Gia_ManAppendAnd( pNew, Gia_ObjChild0Copy(pObj), Gia_ObjChild1Copy(pObj) );
188 else if ( Aig_ObjIsCi(pObj) )
189 pObj->iData = Gia_ManAppendCi( pNew );
190 else if ( Aig_ObjIsCo(pObj) )
191 pObj->iData = Gia_ManAppendCo( pNew, Gia_ObjChild0Copy(pObj) );
192 else if ( Aig_ObjIsConst1(pObj) )
193 pObj->iData = 1;
194 else
195 assert( 0 );
196 }
197 Gia_ManSetRegNum( pNew, Aig_ManRegNum(p) );
198 return pNew;
199 }
200
201 /**Function*************************************************************
202
203 Synopsis [Handles choices as additional combinational outputs.]
204
205 Description []
206
207 SideEffects []
208
209 SeeAlso []
210
211 ***********************************************************************/
Gia_ManFromAigSwitch(Aig_Man_t * p)212 Gia_Man_t * Gia_ManFromAigSwitch( Aig_Man_t * p )
213 {
214 Gia_Man_t * pNew;
215 Aig_Obj_t * pObj;
216 int i;
217 // create the new manager
218 pNew = Gia_ManStart( Aig_ManObjNum(p) );
219 pNew->pName = Abc_UtilStrsav( p->pName );
220 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
221 pNew->nConstrs = p->nConstrs;
222 // create the PIs
223 Aig_ManCleanData( p );
224 Aig_ManConst1(p)->iData = 1;
225 Aig_ManForEachCi( p, pObj, i )
226 pObj->iData = Gia_ManAppendCi( pNew );
227 // add POs corresponding to the nodes with choices
228 Aig_ManForEachNode( p, pObj, i )
229 if ( Aig_ObjRefs(pObj) == 0 )
230 {
231 Gia_ManFromAig_rec( pNew, p, pObj );
232 Gia_ManAppendCo( pNew, pObj->iData );
233 }
234 // add logic for the POs
235 Aig_ManForEachCo( p, pObj, i )
236 Gia_ManFromAig_rec( pNew, p, Aig_ObjFanin0(pObj) );
237 Aig_ManForEachCo( p, pObj, i )
238 pObj->iData = Gia_ManAppendCo( pNew, Gia_ObjChild0Copy(pObj) );
239 Gia_ManSetRegNum( pNew, Aig_ManRegNum(p) );
240 return pNew;
241 }
242
243 /**Function*************************************************************
244
245 Synopsis [Duplicates AIG in the DFS order.]
246
247 Description []
248
249 SideEffects []
250
251 SeeAlso []
252
253 ***********************************************************************/
Gia_ManToAig_rec(Aig_Man_t * pNew,Aig_Obj_t ** ppNodes,Gia_Man_t * p,Gia_Obj_t * pObj)254 void Gia_ManToAig_rec( Aig_Man_t * pNew, Aig_Obj_t ** ppNodes, Gia_Man_t * p, Gia_Obj_t * pObj )
255 {
256 Gia_Obj_t * pNext;
257 if ( ppNodes[Gia_ObjId(p, pObj)] )
258 return;
259 if ( Gia_ObjIsCi(pObj) )
260 ppNodes[Gia_ObjId(p, pObj)] = Aig_ObjCreateCi( pNew );
261 else
262 {
263 assert( Gia_ObjIsAnd(pObj) );
264 Gia_ManToAig_rec( pNew, ppNodes, p, Gia_ObjFanin0(pObj) );
265 Gia_ManToAig_rec( pNew, ppNodes, p, Gia_ObjFanin1(pObj) );
266 ppNodes[Gia_ObjId(p, pObj)] = Aig_And( pNew, Gia_ObjChild0Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)), Gia_ObjChild1Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)) );
267 }
268 if ( pNew->pEquivs && (pNext = Gia_ObjNextObj(p, Gia_ObjId(p, pObj))) )
269 {
270 Aig_Obj_t * pObjNew, * pNextNew;
271 Gia_ManToAig_rec( pNew, ppNodes, p, pNext );
272 pObjNew = ppNodes[Gia_ObjId(p, pObj)];
273 pNextNew = ppNodes[Gia_ObjId(p, pNext)];
274 if ( pNew->pEquivs )
275 pNew->pEquivs[Aig_Regular(pObjNew)->Id] = Aig_Regular(pNextNew);
276 }
277 }
Gia_ManToAig(Gia_Man_t * p,int fChoices)278 Aig_Man_t * Gia_ManToAig( Gia_Man_t * p, int fChoices )
279 {
280 Aig_Man_t * pNew;
281 Aig_Obj_t ** ppNodes;
282 Gia_Obj_t * pObj;
283 int i;
284 assert( !fChoices || (p->pNexts && p->pReprs) );
285 // create the new manager
286 pNew = Aig_ManStart( Gia_ManAndNum(p) );
287 pNew->pName = Abc_UtilStrsav( p->pName );
288 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
289 pNew->nConstrs = p->nConstrs;
290 // pNew->pSpec = Abc_UtilStrsav( p->pName );
291 // duplicate representation of choice nodes
292 if ( fChoices )
293 pNew->pEquivs = ABC_CALLOC( Aig_Obj_t *, Gia_ManObjNum(p) );
294 // create the PIs
295 ppNodes = ABC_CALLOC( Aig_Obj_t *, Gia_ManObjNum(p) );
296 ppNodes[0] = Aig_ManConst0(pNew);
297 Gia_ManForEachCi( p, pObj, i )
298 ppNodes[Gia_ObjId(p, pObj)] = Aig_ObjCreateCi( pNew );
299 // transfer level
300 if ( p->vLevels )
301 Gia_ManForEachCi( p, pObj, i )
302 Aig_ObjSetLevel( ppNodes[Gia_ObjId(p, pObj)], Gia_ObjLevel(p, pObj) );
303 // add logic for the POs
304 Gia_ManForEachCo( p, pObj, i )
305 {
306 Gia_ManToAig_rec( pNew, ppNodes, p, Gia_ObjFanin0(pObj) );
307 ppNodes[Gia_ObjId(p, pObj)] = Aig_ObjCreateCo( pNew, Gia_ObjChild0Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)) );
308 }
309 Aig_ManSetRegNum( pNew, Gia_ManRegNum(p) );
310 ABC_FREE( ppNodes );
311 return pNew;
312 }
313
314 /**Function*************************************************************
315
316 Synopsis [Duplicates AIG in the DFS order.]
317
318 Description []
319
320 SideEffects []
321
322 SeeAlso []
323
324 ***********************************************************************/
Gia_ManToAigSkip(Gia_Man_t * p,int nOutDelta)325 Aig_Man_t * Gia_ManToAigSkip( Gia_Man_t * p, int nOutDelta )
326 {
327 Aig_Man_t * pNew;
328 Aig_Obj_t ** ppNodes;
329 Gia_Obj_t * pObj;
330 int i;
331 assert( p->pNexts == NULL && p->pReprs == NULL );
332 assert( nOutDelta > 0 && Gia_ManCoNum(p) % nOutDelta == 0 );
333 // create the new manager
334 pNew = Aig_ManStart( Gia_ManAndNum(p) );
335 pNew->pName = Abc_UtilStrsav( p->pName );
336 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
337 pNew->nConstrs = p->nConstrs;
338 // pNew->pSpec = Abc_UtilStrsav( p->pName );
339 // create the PIs
340 ppNodes = ABC_CALLOC( Aig_Obj_t *, Gia_ManObjNum(p) );
341 ppNodes[0] = Aig_ManConst0(pNew);
342 Gia_ManForEachCi( p, pObj, i )
343 ppNodes[Gia_ObjId(p, pObj)] = Aig_ObjCreateCi( pNew );
344 // add logic for the POs
345 Gia_ManForEachCo( p, pObj, i )
346 {
347 Gia_ManToAig_rec( pNew, ppNodes, p, Gia_ObjFanin0(pObj) );
348 if ( i % nOutDelta != 0 )
349 continue;
350 ppNodes[Gia_ObjId(p, pObj)] = Aig_ObjCreateCo( pNew, Gia_ObjChild0Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)) );
351 }
352 Aig_ManSetRegNum( pNew, Gia_ManRegNum(p) );
353 ABC_FREE( ppNodes );
354 return pNew;
355 }
356
357 /**Function*************************************************************
358
359 Synopsis [Duplicates AIG in the DFS order.]
360
361 Description []
362
363 SideEffects []
364
365 SeeAlso []
366
367 ***********************************************************************/
Gia_ManToAigSimple(Gia_Man_t * p)368 Aig_Man_t * Gia_ManToAigSimple( Gia_Man_t * p )
369 {
370 Aig_Man_t * pNew;
371 Aig_Obj_t ** ppNodes;
372 Gia_Obj_t * pObj;
373 int i;
374 ppNodes = ABC_FALLOC( Aig_Obj_t *, Gia_ManObjNum(p) );
375 // create the new manager
376 pNew = Aig_ManStart( Gia_ManObjNum(p) );
377 pNew->pName = Abc_UtilStrsav( p->pName );
378 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
379 pNew->nConstrs = p->nConstrs;
380 // create the PIs
381 Gia_ManForEachObj( p, pObj, i )
382 {
383 if ( Gia_ObjIsAnd(pObj) )
384 ppNodes[i] = Aig_And( pNew, Gia_ObjChild0Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)), Gia_ObjChild1Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)) );
385 else if ( Gia_ObjIsCi(pObj) )
386 ppNodes[i] = Aig_ObjCreateCi( pNew );
387 else if ( Gia_ObjIsCo(pObj) )
388 ppNodes[i] = Aig_ObjCreateCo( pNew, Gia_ObjChild0Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)) );
389 else if ( Gia_ObjIsConst0(pObj) )
390 ppNodes[i] = Aig_ManConst0(pNew);
391 else
392 assert( 0 );
393 pObj->Value = Abc_Var2Lit( Aig_ObjId(Aig_Regular(ppNodes[i])), Aig_IsComplement(ppNodes[i]) );
394 assert( i == 0 || Aig_ObjId(ppNodes[i]) == i );
395 }
396 Aig_ManSetRegNum( pNew, Gia_ManRegNum(p) );
397 ABC_FREE( ppNodes );
398 return pNew;
399 }
400
401 /**Function*************************************************************
402
403 Synopsis [Duplicates AIG in the DFS order.]
404
405 Description []
406
407 SideEffects []
408
409 SeeAlso []
410
411 ***********************************************************************/
Gia_ManCofactorAig(Aig_Man_t * p,int nFrames,int nCofFanLit)412 Aig_Man_t * Gia_ManCofactorAig( Aig_Man_t * p, int nFrames, int nCofFanLit )
413 {
414 Aig_Man_t * pMan;
415 Gia_Man_t * pGia, * pTemp;
416 pGia = Gia_ManFromAig( p );
417 pGia = Gia_ManUnrollAndCofactor( pTemp = pGia, nFrames, nCofFanLit, 1 );
418 Gia_ManStop( pTemp );
419 pMan = Gia_ManToAig( pGia, 0 );
420 Gia_ManStop( pGia );
421 return pMan;
422 }
423
424
425 /**Function*************************************************************
426
427 Synopsis [Transfers representatives from pGia to pAig.]
428
429 Description [Assumes that pGia was created from pAig.]
430
431 SideEffects []
432
433 SeeAlso []
434
435 ***********************************************************************/
Gia_ManReprToAigRepr(Aig_Man_t * pAig,Gia_Man_t * pGia)436 void Gia_ManReprToAigRepr( Aig_Man_t * pAig, Gia_Man_t * pGia )
437 {
438 Aig_Obj_t * pObj;
439 Gia_Obj_t * pGiaObj, * pGiaRepr;
440 int i;
441 assert( pAig->pReprs == NULL );
442 assert( pGia->pReprs != NULL );
443 // move pointers from AIG to GIA
444 Aig_ManForEachObj( pAig, pObj, i )
445 {
446 assert( i == 0 || !Abc_LitIsCompl(pObj->iData) );
447 pGiaObj = Gia_ManObj( pGia, Abc_Lit2Var(pObj->iData) );
448 pGiaObj->Value = i;
449 }
450 // set the pointers to the nodes in AIG
451 Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) );
452 Gia_ManForEachObj( pGia, pGiaObj, i )
453 {
454 pGiaRepr = Gia_ObjReprObj( pGia, i );
455 if ( pGiaRepr == NULL )
456 continue;
457 Aig_ObjCreateRepr( pAig, Aig_ManObj(pAig, pGiaRepr->Value), Aig_ManObj(pAig, pGiaObj->Value) );
458 }
459 }
Gia_ManReprToAigRepr2(Aig_Man_t * pAig,Gia_Man_t * pGia)460 void Gia_ManReprToAigRepr2( Aig_Man_t * pAig, Gia_Man_t * pGia )
461 {
462 Gia_Obj_t * pGiaObj, * pGiaRepr;
463 int i;
464 assert( pAig->pReprs == NULL );
465 assert( pGia->pReprs != NULL );
466 // set the pointers to the nodes in AIG
467 Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) );
468 Gia_ManForEachObj( pGia, pGiaObj, i )
469 {
470 pGiaRepr = Gia_ObjReprObj( pGia, i );
471 if ( pGiaRepr == NULL )
472 continue;
473 Aig_ObjCreateRepr( pAig, Aig_ManObj(pAig, Abc_Lit2Var(pGiaRepr->Value)), Aig_ManObj(pAig, Abc_Lit2Var(pGiaObj->Value)) );
474 }
475 }
476
477 /**Function*************************************************************
478
479 Synopsis [Transfers representatives from pAig to pGia.]
480
481 Description []
482
483 SideEffects []
484
485 SeeAlso []
486
487 ***********************************************************************/
Gia_ManReprFromAigRepr(Aig_Man_t * pAig,Gia_Man_t * pGia)488 void Gia_ManReprFromAigRepr( Aig_Man_t * pAig, Gia_Man_t * pGia )
489 {
490 Gia_Obj_t * pObjGia;
491 Aig_Obj_t * pObjAig, * pReprAig;
492 int i;
493 assert( pAig->pReprs != NULL );
494 assert( pGia->pReprs == NULL );
495 assert( Gia_ManObjNum(pGia) - Gia_ManCoNum(pGia) == Aig_ManObjNum(pAig) - Aig_ManCoNum(pAig) );
496 pGia->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(pGia) );
497 for ( i = 0; i < Gia_ManObjNum(pGia); i++ )
498 Gia_ObjSetRepr( pGia, i, GIA_VOID );
499 // move pointers from GIA to AIG
500 Gia_ManForEachObj( pGia, pObjGia, i )
501 {
502 if ( Gia_ObjIsCo(pObjGia) )
503 continue;
504 assert( i == 0 || !Abc_LitIsCompl(Gia_ObjValue(pObjGia)) );
505 pObjAig = Aig_ManObj( pAig, Abc_Lit2Var(Gia_ObjValue(pObjGia)) );
506 pObjAig->iData = i;
507 }
508 Aig_ManForEachObj( pAig, pObjAig, i )
509 {
510 if ( Aig_ObjIsCo(pObjAig) )
511 continue;
512 if ( pAig->pReprs[i] == NULL )
513 continue;
514 pReprAig = pAig->pReprs[i];
515 Gia_ObjSetRepr( pGia, pObjAig->iData, pReprAig->iData );
516 }
517 pGia->pNexts = Gia_ManDeriveNexts( pGia );
518 }
Gia_ManReprFromAigRepr2(Aig_Man_t * pAig,Gia_Man_t * pGia)519 void Gia_ManReprFromAigRepr2( Aig_Man_t * pAig, Gia_Man_t * pGia )
520 {
521 Aig_Obj_t * pObjAig, * pReprAig;
522 int i;
523 assert( pAig->pReprs != NULL );
524 assert( pGia->pReprs == NULL );
525 assert( Gia_ManObjNum(pGia) - Gia_ManCoNum(pGia) == Aig_ManObjNum(pAig) - Aig_ManCoNum(pAig) );
526 pGia->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(pGia) );
527 for ( i = 0; i < Gia_ManObjNum(pGia); i++ )
528 Gia_ObjSetRepr( pGia, i, GIA_VOID );
529 Aig_ManForEachObj( pAig, pObjAig, i )
530 {
531 if ( Aig_ObjIsCo(pObjAig) )
532 continue;
533 if ( pAig->pReprs[i] == NULL )
534 continue;
535 pReprAig = pAig->pReprs[i];
536 Gia_ObjSetRepr( pGia, Abc_Lit2Var(pObjAig->iData), Abc_Lit2Var(pReprAig->iData) );
537 }
538 pGia->pNexts = Gia_ManDeriveNexts( pGia );
539 }
540
541 /**Function*************************************************************
542
543 Synopsis [Applies DC2 to the GIA manager.]
544
545 Description []
546
547 SideEffects []
548
549 SeeAlso []
550
551 ***********************************************************************/
Gia_ManCompress2(Gia_Man_t * p,int fUpdateLevel,int fVerbose)552 Gia_Man_t * Gia_ManCompress2( Gia_Man_t * p, int fUpdateLevel, int fVerbose )
553 {
554 Gia_Man_t * pGia;
555 Aig_Man_t * pNew, * pTemp;
556 if ( p->pManTime && p->vLevels == NULL )
557 Gia_ManLevelWithBoxes( p );
558 pNew = Gia_ManToAig( p, 0 );
559 pNew = Dar_ManCompress2( pTemp = pNew, 1, fUpdateLevel, 1, 0, fVerbose );
560 Aig_ManStop( pTemp );
561 pGia = Gia_ManFromAig( pNew );
562 Aig_ManStop( pNew );
563 Gia_ManTransferTiming( pGia, p );
564 return pGia;
565 }
566
567 /**Function*************************************************************
568
569 Synopsis []
570
571 Description []
572
573 SideEffects []
574
575 SeeAlso []
576
577 ***********************************************************************/
Gia_ManPerformDch(Gia_Man_t * p,void * pPars)578 Gia_Man_t * Gia_ManPerformDch( Gia_Man_t * p, void * pPars )
579 {
580 int fUseMapping = 0;
581 Gia_Man_t * pGia, * pGia1;
582 Aig_Man_t * pNew;
583 if ( p->pManTime && p->vLevels == NULL )
584 Gia_ManLevelWithBoxes( p );
585 if ( fUseMapping && Gia_ManHasMapping(p) )
586 pGia1 = (Gia_Man_t *)Dsm_ManDeriveGia( p, 0 );
587 else
588 pGia1 = Gia_ManDup( p );
589 pNew = Gia_ManToAig( pGia1, 0 );
590 Gia_ManStop( pGia1 );
591 pNew = Dar_ManChoiceNew( pNew, (Dch_Pars_t *)pPars );
592 // pGia = Gia_ManFromAig( pNew );
593 pGia = Gia_ManFromAigChoices( pNew );
594 Aig_ManStop( pNew );
595 Gia_ManTransferTiming( pGia, p );
596 return pGia;
597 }
598
599 /**Function*************************************************************
600
601 Synopsis [Computes equivalences after structural sequential cleanup.]
602
603 Description []
604
605 SideEffects []
606
607 SeeAlso []
608
609 ***********************************************************************/
Gia_ManSeqCleanupClasses(Gia_Man_t * p,int fConst,int fEquiv,int fVerbose)610 void Gia_ManSeqCleanupClasses( Gia_Man_t * p, int fConst, int fEquiv, int fVerbose )
611 {
612 Aig_Man_t * pNew, * pTemp;
613 pNew = Gia_ManToAigSimple( p );
614 pTemp = Aig_ManScl( pNew, fConst, fEquiv, 0, -1, -1, fVerbose, 0 );
615 Gia_ManReprFromAigRepr( pNew, p );
616 Aig_ManStop( pTemp );
617 Aig_ManStop( pNew );
618 }
619
620 /**Function*************************************************************
621
622 Synopsis [Solves SAT problem.]
623
624 Description []
625
626 SideEffects []
627
628 SeeAlso []
629
630 ***********************************************************************/
Gia_ManSolveSat(Gia_Man_t * p)631 int Gia_ManSolveSat( Gia_Man_t * p )
632 {
633 // extern int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fFlipBits, int fAndOuts, int fNewSolver, int fVerbose );
634 Aig_Man_t * pNew;
635 int RetValue;//, clk = Abc_Clock();
636 pNew = Gia_ManToAig( p, 0 );
637 RetValue = Fra_FraigSat( pNew, 10000000, 0, 0, 0, 0, 1, 1, 0, 0 );
638 if ( RetValue == 0 )
639 {
640 Gia_Obj_t * pObj;
641 int i, * pInit = (int *)pNew->pData;
642 Gia_ManConst0(p)->fMark0 = 0;
643 Gia_ManForEachPi( p, pObj, i )
644 pObj->fMark0 = pInit[i];
645 Gia_ManForEachAnd( p, pObj, i )
646 pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) &
647 (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
648 Gia_ManForEachPo( p, pObj, i )
649 pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj));
650 Gia_ManForEachPo( p, pObj, i )
651 if ( pObj->fMark0 != 1 )
652 break;
653 if ( i != Gia_ManPoNum(p) )
654 Abc_Print( 1, "Counter-example verification has failed. " );
655 // else
656 // Abc_Print( 1, "Counter-example verification succeeded. " );
657 }
658 /*
659 else if ( RetValue == 1 )
660 Abc_Print( 1, "The SAT problem is unsatisfiable. " );
661 else if ( RetValue == -1 )
662 Abc_Print( 1, "The SAT problem is undecided. " );
663 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
664 */
665 Aig_ManStop( pNew );
666 return RetValue;
667 }
668
669
670 ////////////////////////////////////////////////////////////////////////
671 /// END OF FILE ///
672 ////////////////////////////////////////////////////////////////////////
673
674
675 ABC_NAMESPACE_IMPL_END
676
677