1 /**CFile****************************************************************
2
3 FileName [giaDup.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Scalable AIG package.]
8
9 Synopsis [Duplication procedures.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: giaDup.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "gia.h"
22 #include "misc/tim/tim.h"
23 #include "misc/vec/vecWec.h"
24 #include "proof/cec/cec.h"
25
26 ABC_NAMESPACE_IMPL_START
27
28
29 ////////////////////////////////////////////////////////////////////////
30 /// DECLARATIONS ///
31 ////////////////////////////////////////////////////////////////////////
32
33 ////////////////////////////////////////////////////////////////////////
34 /// FUNCTION DEFINITIONS ///
35 ////////////////////////////////////////////////////////////////////////
36
37 /**Function*************************************************************
38
39 Synopsis [Removes pointers to the unmarked nodes..]
40
41 Description [Array vLits contains literals of p. At the same time,
42 each object pObj of p points to a literal of pNew. This procedure
43 remaps literals in array vLits into literals of pNew.]
44
45 SideEffects []
46
47 SeeAlso []
48
49 ***********************************************************************/
Gia_ManDupRemapLiterals(Vec_Int_t * vLits,Gia_Man_t * p)50 void Gia_ManDupRemapLiterals( Vec_Int_t * vLits, Gia_Man_t * p )
51 {
52 Gia_Obj_t * pObj;
53 int i, iLit, iLitNew;
54 Vec_IntForEachEntry( vLits, iLit, i )
55 {
56 if ( iLit < 0 )
57 continue;
58 pObj = Gia_ManObj( p, Abc_Lit2Var(iLit) );
59 if ( ~pObj->Value == 0 )
60 iLitNew = -1;
61 else
62 iLitNew = Abc_LitNotCond( pObj->Value, Abc_LitIsCompl(iLit) );
63 Vec_IntWriteEntry( vLits, i, iLitNew );
64 }
65 }
66
67 /**Function*************************************************************
68
69 Synopsis [Removes pointers to the unmarked nodes..]
70
71 Description []
72
73 SideEffects []
74
75 SeeAlso []
76
77 ***********************************************************************/
Gia_ManDupRemapEquiv(Gia_Man_t * pNew,Gia_Man_t * p)78 void Gia_ManDupRemapEquiv( Gia_Man_t * pNew, Gia_Man_t * p )
79 {
80 Vec_Int_t * vClass;
81 int i, k, iNode, iRepr, iPrev;
82 if ( p->pReprs == NULL )
83 return;
84 assert( pNew->pReprs == NULL && pNew->pNexts == NULL );
85 // start representatives
86 pNew->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(pNew) );
87 for ( i = 0; i < Gia_ManObjNum(pNew); i++ )
88 Gia_ObjSetRepr( pNew, i, GIA_VOID );
89 // iterate over constant candidates
90 Gia_ManForEachConst( p, i )
91 Gia_ObjSetRepr( pNew, Abc_Lit2Var(Gia_ManObj(p, i)->Value), 0 );
92 // iterate over class candidates
93 vClass = Vec_IntAlloc( 100 );
94 Gia_ManForEachClass( p, i )
95 {
96 Vec_IntClear( vClass );
97 Gia_ClassForEachObj( p, i, k )
98 Vec_IntPushUnique( vClass, Abc_Lit2Var(Gia_ManObj(p, k)->Value) );
99 assert( Vec_IntSize( vClass ) > 1 );
100 Vec_IntSort( vClass, 0 );
101 iRepr = iPrev = Vec_IntEntry( vClass, 0 );
102 Vec_IntForEachEntryStart( vClass, iNode, k, 1 )
103 {
104 Gia_ObjSetRepr( pNew, iNode, iRepr );
105 assert( iPrev < iNode );
106 iPrev = iNode;
107 }
108 }
109 Vec_IntFree( vClass );
110 pNew->pNexts = Gia_ManDeriveNexts( pNew );
111 }
112
113 /**Function*************************************************************
114
115 Synopsis [Remaps combinational inputs when objects are DFS ordered.]
116
117 Description []
118
119 SideEffects []
120
121 SeeAlso []
122
123 ***********************************************************************/
Gia_ManDupRemapCis(Gia_Man_t * pNew,Gia_Man_t * p)124 void Gia_ManDupRemapCis( Gia_Man_t * pNew, Gia_Man_t * p )
125 {
126 Gia_Obj_t * pObj, * pObjNew;
127 int i;
128 assert( Vec_IntSize(p->vCis) == Vec_IntSize(pNew->vCis) );
129 Gia_ManForEachCi( p, pObj, i )
130 {
131 assert( Gia_ObjCioId(pObj) == i );
132 pObjNew = Gia_ObjFromLit( pNew, pObj->Value );
133 assert( !Gia_IsComplement(pObjNew) );
134 Vec_IntWriteEntry( pNew->vCis, i, Gia_ObjId(pNew, pObjNew) );
135 Gia_ObjSetCioId( pObjNew, i );
136 }
137 }
138
139 /**Function*************************************************************
140
141 Synopsis [Remaps combinational outputs when objects are DFS ordered.]
142
143 Description []
144
145 SideEffects []
146
147 SeeAlso []
148
149 ***********************************************************************/
Gia_ManDupRemapCos(Gia_Man_t * pNew,Gia_Man_t * p)150 void Gia_ManDupRemapCos( Gia_Man_t * pNew, Gia_Man_t * p )
151 {
152 Gia_Obj_t * pObj, * pObjNew;
153 int i;
154 assert( Vec_IntSize(p->vCos) == Vec_IntSize(pNew->vCos) );
155 Gia_ManForEachCo( p, pObj, i )
156 {
157 assert( Gia_ObjCioId(pObj) == i );
158 pObjNew = Gia_ObjFromLit( pNew, pObj->Value );
159 assert( !Gia_IsComplement(pObjNew) );
160 Vec_IntWriteEntry( pNew->vCos, i, Gia_ObjId(pNew, pObjNew) );
161 Gia_ObjSetCioId( pObjNew, i );
162 }
163 }
164
165 /**Function*************************************************************
166
167 Synopsis [Duplicates the AIG in the DFS order.]
168
169 Description []
170
171 SideEffects []
172
173 SeeAlso []
174
175 ***********************************************************************/
Gia_ManDupOrderDfs_rec(Gia_Man_t * pNew,Gia_Man_t * p,Gia_Obj_t * pObj)176 int Gia_ManDupOrderDfs_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
177 {
178 if ( ~pObj->Value )
179 return pObj->Value;
180 if ( Gia_ObjIsCi(pObj) )
181 return pObj->Value = Gia_ManAppendCi(pNew);
182 // if ( p->pNexts && Gia_ObjNext(p, Gia_ObjId(p, pObj)) )
183 // Gia_ManDupOrderDfs_rec( pNew, p, Gia_ObjNextObj(p, Gia_ObjId(p, pObj)) );
184 Gia_ManDupOrderDfs_rec( pNew, p, Gia_ObjFanin0(pObj) );
185 if ( Gia_ObjIsCo(pObj) )
186 return pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
187 Gia_ManDupOrderDfs_rec( pNew, p, Gia_ObjFanin1(pObj) );
188 return pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
189 }
190
191 /**Function*************************************************************
192
193 Synopsis [Duplicates AIG while putting objects in the DFS order.]
194
195 Description []
196
197 SideEffects []
198
199 SeeAlso []
200
201 ***********************************************************************/
Gia_ManDupOrderDfs(Gia_Man_t * p)202 Gia_Man_t * Gia_ManDupOrderDfs( Gia_Man_t * p )
203 {
204 Gia_Man_t * pNew;
205 Gia_Obj_t * pObj;
206 int i;
207 Gia_ManFillValue( p );
208 pNew = Gia_ManStart( Gia_ManObjNum(p) );
209 pNew->pName = Abc_UtilStrsav( p->pName );
210 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
211 Gia_ManConst0(p)->Value = 0;
212 Gia_ManForEachCo( p, pObj, i )
213 Gia_ManDupOrderDfs_rec( pNew, p, pObj );
214 Gia_ManForEachCi( p, pObj, i )
215 if ( !~pObj->Value )
216 pObj->Value = Gia_ManAppendCi(pNew);
217 assert( Gia_ManCiNum(pNew) == Gia_ManCiNum(p) );
218 Gia_ManDupRemapCis( pNew, p );
219 Gia_ManDupRemapEquiv( pNew, p );
220 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
221 return pNew;
222 }
223
224 /**Function*************************************************************
225
226 Synopsis [Duplicates AIG while putting objects in the DFS order.]
227
228 Description []
229
230 SideEffects []
231
232 SeeAlso []
233
234 ***********************************************************************/
Gia_ManDupAbs(Gia_Man_t * p,Vec_Int_t * vMapPpi2Ff,Vec_Int_t * vMapFf2Ppi)235 Gia_Man_t * Gia_ManDupAbs( Gia_Man_t * p, Vec_Int_t * vMapPpi2Ff, Vec_Int_t * vMapFf2Ppi )
236 {
237 Gia_Man_t * pNew;
238 Gia_Obj_t * pObj;
239 int k, Flop, Used;
240 assert( Vec_IntSize(vMapFf2Ppi) == Vec_IntSize(vMapPpi2Ff) + Vec_IntCountEntry(vMapFf2Ppi, -1) );
241 Gia_ManFillValue( p );
242 pNew = Gia_ManStart( Gia_ManObjNum(p) );
243 pNew->pName = Abc_UtilStrsav( p->pName );
244 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
245 Gia_ManConst0(p)->Value = 0;
246 // create inputs
247 Gia_ManForEachPi( p, pObj, k )
248 pObj->Value = Gia_ManAppendCi(pNew);
249 Vec_IntForEachEntry( vMapPpi2Ff, Flop, k )
250 {
251 pObj = Gia_ManCi( p, Gia_ManPiNum(p) + Flop );
252 pObj->Value = Gia_ManAppendCi(pNew);
253 }
254 Vec_IntForEachEntry( vMapFf2Ppi, Used, Flop )
255 {
256 pObj = Gia_ManCi( p, Gia_ManPiNum(p) + Flop );
257 if ( Used >= 0 )
258 {
259 assert( pObj->Value != ~0 );
260 continue;
261 }
262 assert( pObj->Value == ~0 );
263 pObj->Value = Gia_ManAppendCi(pNew);
264 }
265 Gia_ManForEachCi( p, pObj, k )
266 assert( pObj->Value != ~0 );
267 // create nodes
268 Gia_ManForEachPo( p, pObj, k )
269 Gia_ManDupOrderDfs_rec( pNew, p, Gia_ObjFanin0(pObj) );
270 Vec_IntForEachEntry( vMapFf2Ppi, Used, Flop )
271 {
272 if ( Used >= 0 )
273 continue;
274 pObj = Gia_ManCi( p, Gia_ManPiNum(p) + Flop );
275 pObj = Gia_ObjRoToRi( p, pObj );
276 Gia_ManDupOrderDfs_rec( pNew, p, Gia_ObjFanin0(pObj) );
277 }
278 // create outputs
279 Gia_ManForEachPo( p, pObj, k )
280 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
281 Vec_IntForEachEntry( vMapFf2Ppi, Used, Flop )
282 {
283 if ( Used >= 0 )
284 continue;
285 pObj = Gia_ManCi( p, Gia_ManPiNum(p) + Flop );
286 pObj = Gia_ObjRoToRi( p, pObj );
287 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
288 }
289 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) - Vec_IntSize(vMapPpi2Ff) );
290 assert( Gia_ManPiNum(pNew) == Gia_ManPiNum(p) + Vec_IntSize(vMapPpi2Ff) );
291 assert( Gia_ManCiNum(pNew) == Gia_ManCiNum(p) );
292 assert( Gia_ManPoNum(pNew) == Gia_ManPoNum(p) );
293 assert( Gia_ManCoNum(pNew) == Gia_ManCoNum(p) - Vec_IntSize(vMapPpi2Ff) );
294 return pNew;
295 }
296
297
298 /**Function*************************************************************
299
300 Synopsis [Duplicates AIG while putting objects in the DFS order.]
301
302 Description []
303
304 SideEffects []
305
306 SeeAlso []
307
308 ***********************************************************************/
Gia_ManDupOutputGroup(Gia_Man_t * p,int iOutStart,int iOutStop)309 Gia_Man_t * Gia_ManDupOutputGroup( Gia_Man_t * p, int iOutStart, int iOutStop )
310 {
311 Gia_Man_t * pNew;
312 Gia_Obj_t * pObj;
313 int i;
314 Gia_ManFillValue( p );
315 pNew = Gia_ManStart( Gia_ManObjNum(p) );
316 pNew->pName = Abc_UtilStrsav( p->pName );
317 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
318 Gia_ManConst0(p)->Value = 0;
319 for ( i = iOutStart; i < iOutStop; i++ )
320 {
321 pObj = Gia_ManCo( p, i );
322 Gia_ManDupOrderDfs_rec( pNew, p, pObj );
323 }
324 return pNew;
325 }
326
327 /**Function*************************************************************
328
329 Synopsis [Duplicates AIG while putting objects in the DFS order.]
330
331 Description []
332
333 SideEffects []
334
335 SeeAlso []
336
337 ***********************************************************************/
Gia_ManDupOutputVec(Gia_Man_t * p,Vec_Int_t * vOutPres)338 Gia_Man_t * Gia_ManDupOutputVec( Gia_Man_t * p, Vec_Int_t * vOutPres )
339 {
340 Gia_Man_t * pNew;
341 Gia_Obj_t * pObj;
342 int i;
343 assert( Gia_ManRegNum(p) == 0 );
344 assert( Gia_ManPoNum(p) == Vec_IntSize(vOutPres) );
345 Gia_ManFillValue( p );
346 pNew = Gia_ManStart( Gia_ManObjNum(p) );
347 pNew->pName = Abc_UtilStrsav( p->pName );
348 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
349 Gia_ManConst0(p)->Value = 0;
350 Gia_ManForEachPi( p, pObj, i )
351 pObj->Value = Gia_ManAppendCi(pNew);
352 Gia_ManForEachPo( p, pObj, i )
353 if ( Vec_IntEntry(vOutPres, i) )
354 Gia_ManDupOrderDfs_rec( pNew, p, Gia_ObjFanin0(pObj) );
355 Gia_ManForEachPo( p, pObj, i )
356 if ( Vec_IntEntry(vOutPres, i) )
357 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
358 return pNew;
359 }
360
361 /**Function*************************************************************
362
363 Synopsis [Duplicates AIG while putting objects in the DFS order.]
364
365 Description []
366
367 SideEffects []
368
369 SeeAlso []
370
371 ***********************************************************************/
Gia_ManDupSelectedOutputs(Gia_Man_t * p,Vec_Int_t * vOutsLeft)372 Gia_Man_t * Gia_ManDupSelectedOutputs( Gia_Man_t * p, Vec_Int_t * vOutsLeft )
373 {
374 Gia_Man_t * pNew;
375 Gia_Obj_t * pObj;
376 int i, iOut;
377 assert( Gia_ManRegNum(p) == 0 );
378 assert( Gia_ManPoNum(p) >= Vec_IntSize(vOutsLeft) );
379 Gia_ManFillValue( p );
380 pNew = Gia_ManStart( Gia_ManObjNum(p) );
381 pNew->pName = Abc_UtilStrsav( p->pName );
382 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
383 Gia_ManConst0(p)->Value = 0;
384 Gia_ManForEachPi( p, pObj, i )
385 pObj->Value = Gia_ManAppendCi(pNew);
386 Vec_IntForEachEntry( vOutsLeft, iOut, i )
387 Gia_ManDupOrderDfs_rec( pNew, p, Gia_ObjFanin0(Gia_ManPo(p, iOut)) );
388 Vec_IntForEachEntry( vOutsLeft, iOut, i )
389 Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(Gia_ManPo(p, iOut)) );
390 return pNew;
391 }
392
393 /**Function*************************************************************
394
395 Synopsis [Duplicates the AIG in the DFS order.]
396
397 Description []
398
399 SideEffects []
400
401 SeeAlso []
402
403 ***********************************************************************/
Gia_ManDupOrderDfsChoices_rec(Gia_Man_t * pNew,Gia_Man_t * p,Gia_Obj_t * pObj)404 void Gia_ManDupOrderDfsChoices_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
405 {
406 Gia_Obj_t * pNext;
407 if ( ~pObj->Value )
408 return;
409 assert( Gia_ObjIsAnd(pObj) );
410 pNext = Gia_ObjNextObj( p, Gia_ObjId(p, pObj) );
411 if ( pNext )
412 Gia_ManDupOrderDfsChoices_rec( pNew, p, pNext );
413 Gia_ManDupOrderDfsChoices_rec( pNew, p, Gia_ObjFanin0(pObj) );
414 Gia_ManDupOrderDfsChoices_rec( pNew, p, Gia_ObjFanin1(pObj) );
415 pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
416 if ( pNext )
417 {
418 pNew->pNexts[Abc_Lit2Var(pObj->Value)] = Abc_Lit2Var( Abc_Lit2Var(pNext->Value) );
419 assert( Abc_Lit2Var(pObj->Value) > Abc_Lit2Var(pNext->Value) );
420 }
421 }
422
423 /**Function*************************************************************
424
425 Synopsis [Duplicates AIG while putting objects in the DFS order.]
426
427 Description []
428
429 SideEffects []
430
431 SeeAlso []
432
433 ***********************************************************************/
Gia_ManDupOrderDfsChoices(Gia_Man_t * p)434 Gia_Man_t * Gia_ManDupOrderDfsChoices( Gia_Man_t * p )
435 {
436 Gia_Man_t * pNew;
437 Gia_Obj_t * pObj;
438 int i;
439 assert( p->pReprs && p->pNexts );
440 Gia_ManFillValue( p );
441 pNew = Gia_ManStart( Gia_ManObjNum(p) );
442 pNew->pName = Abc_UtilStrsav( p->pName );
443 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
444 pNew->pNexts = ABC_CALLOC( int, Gia_ManObjNum(p) );
445 Gia_ManConst0(p)->Value = 0;
446 Gia_ManForEachCi( p, pObj, i )
447 pObj->Value = Gia_ManAppendCi(pNew);
448 Gia_ManForEachCo( p, pObj, i )
449 {
450 Gia_ManDupOrderDfsChoices_rec( pNew, p, Gia_ObjFanin0(pObj) );
451 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
452 }
453 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
454 // Gia_ManDeriveReprs( pNew );
455 return pNew;
456 }
457
458 /**Function*************************************************************
459
460 Synopsis [Duplicates AIG while putting objects in the DFS order.]
461
462 Description []
463
464 SideEffects []
465
466 SeeAlso []
467
468 ***********************************************************************/
Gia_ManDupOrderDfsReverse(Gia_Man_t * p)469 Gia_Man_t * Gia_ManDupOrderDfsReverse( Gia_Man_t * p )
470 {
471 Gia_Man_t * pNew;
472 Gia_Obj_t * pObj;
473 int i;
474 Gia_ManFillValue( p );
475 pNew = Gia_ManStart( Gia_ManObjNum(p) );
476 pNew->pName = Abc_UtilStrsav( p->pName );
477 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
478 Gia_ManConst0(p)->Value = 0;
479 Gia_ManForEachCoReverse( p, pObj, i )
480 Gia_ManDupOrderDfs_rec( pNew, p, pObj );
481 Gia_ManForEachCi( p, pObj, i )
482 if ( !~pObj->Value )
483 pObj->Value = Gia_ManAppendCi(pNew);
484 assert( Gia_ManCiNum(pNew) == Gia_ManCiNum(p) );
485 Gia_ManDupRemapCis( pNew, p );
486 Gia_ManDupRemapCos( pNew, p );
487 Gia_ManDupRemapEquiv( pNew, p );
488 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
489 return pNew;
490 }
491
492 /**Function*************************************************************
493
494 Synopsis [Duplicates AIG while putting first PIs, then nodes, then POs.]
495
496 Description []
497
498 SideEffects []
499
500 SeeAlso []
501
502 ***********************************************************************/
Gia_ManDupOrderAiger(Gia_Man_t * p)503 Gia_Man_t * Gia_ManDupOrderAiger( Gia_Man_t * p )
504 {
505 Gia_Man_t * pNew;
506 Gia_Obj_t * pObj;
507 int i;
508 pNew = Gia_ManStart( Gia_ManObjNum(p) );
509 pNew->pName = Abc_UtilStrsav( p->pName );
510 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
511 Gia_ManConst0(p)->Value = 0;
512 Gia_ManForEachCi( p, pObj, i )
513 pObj->Value = Gia_ManAppendCi(pNew);
514 Gia_ManForEachAnd( p, pObj, i )
515 pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
516 Gia_ManForEachCo( p, pObj, i )
517 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
518 Gia_ManDupRemapEquiv( pNew, p );
519 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
520 assert( Gia_ManIsNormalized(pNew) );
521 return pNew;
522 }
523
524 /**Function*************************************************************
525
526 Synopsis [Duplicates AIG while putting first PIs, then nodes, then POs.]
527
528 Description []
529
530 SideEffects []
531
532 SeeAlso []
533
534 ***********************************************************************/
Gia_ManDupOnsetOffset(Gia_Man_t * p)535 Gia_Man_t * Gia_ManDupOnsetOffset( Gia_Man_t * p )
536 {
537 Gia_Man_t * pNew;
538 Gia_Obj_t * pObj;
539 int i;
540 pNew = Gia_ManStart( Gia_ManObjNum(p) );
541 pNew->pName = Abc_UtilStrsav( p->pName );
542 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
543 Gia_ManConst0(p)->Value = 0;
544 Gia_ManForEachCi( p, pObj, i )
545 pObj->Value = Gia_ManAppendCi(pNew);
546 Gia_ManForEachAnd( p, pObj, i )
547 pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
548 Gia_ManForEachCo( p, pObj, i )
549 {
550 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
551 pObj->Value = Gia_ManAppendCo( pNew, Abc_LitNot(Gia_ObjFanin0Copy(pObj)) );
552 }
553 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
554 return pNew;
555 }
556
557 /**Function*************************************************************
558
559 Synopsis [Duplicates AIG while putting first PIs, then nodes, then POs.]
560
561 Description []
562
563 SideEffects []
564
565 SeeAlso []
566
567 ***********************************************************************/
Gia_ManDupLastPis(Gia_Man_t * p,int nLastPis)568 Gia_Man_t * Gia_ManDupLastPis( Gia_Man_t * p, int nLastPis )
569 {
570 Gia_Man_t * pNew;
571 Gia_Obj_t * pObj;
572 int i;
573 assert( Gia_ManRegNum(p) == 0 );
574 pNew = Gia_ManStart( Gia_ManObjNum(p) );
575 pNew->pName = Abc_UtilStrsav( p->pName );
576 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
577 Gia_ManConst0(p)->Value = 0;
578 Gia_ManForEachCi( p, pObj, i )
579 pObj->Value = (i < Gia_ManCiNum(p) - nLastPis) ? ~0 : Gia_ManAppendCi(pNew);
580 Gia_ManForEachAnd( p, pObj, i )
581 pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
582 Gia_ManForEachCo( p, pObj, i )
583 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
584 return pNew;
585 }
586
587 /**Function*************************************************************
588
589 Synopsis [Duplicates AIG while complementing the flops.]
590
591 Description [The array of initial state contains the init state
592 for each state bit of the flops in the design.]
593
594 SideEffects []
595
596 SeeAlso []
597
598 ***********************************************************************/
Gia_ManDupFlip(Gia_Man_t * p,int * pInitState)599 Gia_Man_t * Gia_ManDupFlip( Gia_Man_t * p, int * pInitState )
600 {
601 Gia_Man_t * pNew;
602 Gia_Obj_t * pObj;
603 int i;
604 pNew = Gia_ManStart( Gia_ManObjNum(p) );
605 pNew->pName = Abc_UtilStrsav( p->pName );
606 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
607 Gia_ManConst0(p)->Value = 0;
608 Gia_ManForEachObj1( p, pObj, i )
609 {
610 if ( Gia_ObjIsAnd(pObj) )
611 pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
612 else if ( Gia_ObjIsCi(pObj) )
613 {
614 pObj->Value = Gia_ManAppendCi( pNew );
615 if ( Gia_ObjCioId(pObj) >= Gia_ManPiNum(p) )
616 pObj->Value = Abc_LitNotCond( pObj->Value, Abc_InfoHasBit((unsigned *)pInitState, Gia_ObjCioId(pObj) - Gia_ManPiNum(p)) );
617 }
618 else if ( Gia_ObjIsCo(pObj) )
619 {
620 pObj->Value = Gia_ObjFanin0Copy(pObj);
621 if ( Gia_ObjCioId(pObj) >= Gia_ManPoNum(p) )
622 pObj->Value = Abc_LitNotCond( pObj->Value, Abc_InfoHasBit((unsigned *)pInitState, Gia_ObjCioId(pObj) - Gia_ManPoNum(p)) );
623 pObj->Value = Gia_ManAppendCo( pNew, pObj->Value );
624 }
625 }
626 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
627 return pNew;
628 }
629
630
631 /**Function*************************************************************
632
633 Synopsis [Cycles AIG using random input.]
634
635 Description []
636
637 SideEffects []
638
639 SeeAlso []
640
641 ***********************************************************************/
Gia_ManCycle(Gia_Man_t * p,Abc_Cex_t * pCex,int nFrames)642 void Gia_ManCycle( Gia_Man_t * p, Abc_Cex_t * pCex, int nFrames )
643 {
644 Gia_Obj_t * pObj, * pObjRi, * pObjRo;
645 int i, k;
646 Gia_ManRandom( 1 );
647 assert( pCex == NULL || nFrames <= pCex->iFrame );
648 // iterate for the given number of frames
649 for ( i = 0; i < nFrames; i++ )
650 {
651 Gia_ManForEachPi( p, pObj, k )
652 pObj->fMark0 = pCex ? Abc_InfoHasBit(pCex->pData, pCex->nRegs+i*pCex->nPis+k) : (1 & Gia_ManRandom(0));
653 Gia_ManForEachAnd( p, pObj, k )
654 pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) &
655 (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
656 Gia_ManForEachCo( p, pObj, k )
657 pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
658 Gia_ManForEachRiRo( p, pObjRi, pObjRo, k )
659 pObjRo->fMark0 = pObjRi->fMark0;
660 }
661 }
Gia_ManDupCycled(Gia_Man_t * p,Abc_Cex_t * pCex,int nFrames)662 Gia_Man_t * Gia_ManDupCycled( Gia_Man_t * p, Abc_Cex_t * pCex, int nFrames )
663 {
664 Gia_Man_t * pNew;
665 Vec_Bit_t * vInits;
666 Gia_Obj_t * pObj;
667 int i;
668 Gia_ManCleanMark0(p);
669 Gia_ManCycle( p, pCex, nFrames );
670 vInits = Vec_BitAlloc( Gia_ManRegNum(p) );
671 Gia_ManForEachRo( p, pObj, i )
672 Vec_BitPush( vInits, pObj->fMark0 );
673 pNew = Gia_ManDupFlip( p, Vec_BitArray(vInits) );
674 Vec_BitFree( vInits );
675 Gia_ManCleanMark0(p);
676 return pNew;
677 }
678
679
680 /**Function*************************************************************
681
682 Synopsis [Duplicates AIG without any changes.]
683
684 Description []
685
686 SideEffects []
687
688 SeeAlso []
689
690 ***********************************************************************/
Gia_ManDup(Gia_Man_t * p)691 Gia_Man_t * Gia_ManDup( Gia_Man_t * p )
692 {
693 Gia_Man_t * pNew;
694 Gia_Obj_t * pObj;
695 int i;
696 pNew = Gia_ManStart( Gia_ManObjNum(p) );
697 pNew->pName = Abc_UtilStrsav( p->pName );
698 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
699 if ( Gia_ManHasChoices(p) )
700 pNew->pSibls = ABC_CALLOC( int, Gia_ManObjNum(p) );
701 Gia_ManConst0(p)->Value = 0;
702 Gia_ManForEachObj1( p, pObj, i )
703 {
704 if ( Gia_ObjIsBuf(pObj) )
705 pObj->Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) );
706 else if ( Gia_ObjIsAnd(pObj) )
707 {
708 pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
709 if ( Gia_ObjSibl(p, Gia_ObjId(p, pObj)) )
710 pNew->pSibls[Abc_Lit2Var(pObj->Value)] = Abc_Lit2Var(Gia_ObjSiblObj(p, Gia_ObjId(p, pObj))->Value);
711 }
712 else if ( Gia_ObjIsCi(pObj) )
713 pObj->Value = Gia_ManAppendCi( pNew );
714 else if ( Gia_ObjIsCo(pObj) )
715 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
716 }
717 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
718 if ( p->pCexSeq )
719 pNew->pCexSeq = Abc_CexDup( p->pCexSeq, Gia_ManRegNum(p) );
720 return pNew;
721 }
Gia_ManDup2(Gia_Man_t * p1,Gia_Man_t * p2)722 Gia_Man_t * Gia_ManDup2( Gia_Man_t * p1, Gia_Man_t * p2 )
723 {
724 Gia_Man_t * pNew;
725 Gia_Obj_t * pObj;
726 int i;
727 assert( Gia_ManCiNum(p1) == Gia_ManCiNum(p2) );
728 assert( Gia_ManCoNum(p1) == Gia_ManCoNum(p2) );
729 pNew = Gia_ManStart( Gia_ManObjNum(p1) + Gia_ManObjNum(p2) );
730 Gia_ManHashStart( pNew );
731 Gia_ManConst0(p1)->Value = 0;
732 Gia_ManConst0(p2)->Value = 0;
733 Gia_ManForEachCi( p1, pObj, i )
734 pObj->Value = Gia_ManCi(p2, i)->Value = Gia_ManAppendCi( pNew );
735 Gia_ManForEachAnd( p1, pObj, i )
736 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
737 Gia_ManForEachAnd( p2, pObj, i )
738 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
739 Gia_ManForEachCo( p1, pObj, i )
740 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
741 Gia_ManForEachCo( p2, pObj, i )
742 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
743 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p1) );
744 Gia_ManHashStop( pNew );
745 return pNew;
746 }
Gia_ManDupWithAttributes(Gia_Man_t * p)747 Gia_Man_t * Gia_ManDupWithAttributes( Gia_Man_t * p )
748 {
749 Gia_Man_t * pNew = Gia_ManDup(p);
750 Gia_ManTransferMapping( pNew, p );
751 Gia_ManTransferPacking( pNew, p );
752 if ( p->pManTime )
753 pNew->pManTime = Tim_ManDup( (Tim_Man_t *)p->pManTime, 0 );
754 if ( p->pAigExtra )
755 pNew->pAigExtra = Gia_ManDup( p->pAigExtra );
756 if ( p->nAnd2Delay )
757 pNew->nAnd2Delay = p->nAnd2Delay;
758 if ( p->vRegClasses )
759 pNew->vRegClasses = Vec_IntDup( p->vRegClasses );
760 if ( p->vRegInits )
761 pNew->vRegInits = Vec_IntDup( p->vRegInits );
762 if ( p->vConfigs )
763 pNew->vConfigs = Vec_IntDup( p->vConfigs );
764 if ( p->pCellStr )
765 pNew->pCellStr = Abc_UtilStrsav( p->pCellStr );
766 return pNew;
767 }
Gia_ManDupRemovePis(Gia_Man_t * p,int nRemPis)768 Gia_Man_t * Gia_ManDupRemovePis( Gia_Man_t * p, int nRemPis )
769 {
770 Gia_Man_t * pNew;
771 Gia_Obj_t * pObj;
772 int i;
773 pNew = Gia_ManStart( Gia_ManObjNum(p) );
774 pNew->pName = Abc_UtilStrsav( p->pName );
775 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
776 Gia_ManConst0(p)->Value = 0;
777 Gia_ManForEachObj1( p, pObj, i )
778 {
779 if ( Gia_ObjIsAnd(pObj) )
780 pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
781 else if ( Gia_ObjIsCi(pObj) && Gia_ObjCioId(pObj) < Gia_ManCiNum(p)-nRemPis )
782 pObj->Value = Gia_ManAppendCi( pNew );
783 else if ( Gia_ObjIsCo(pObj) )
784 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
785 }
786 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
787 return pNew;
788 }
789
790 /**Function*************************************************************
791
792 Synopsis [Duplicates AIG without any changes.]
793
794 Description []
795
796 SideEffects []
797
798 SeeAlso []
799
800 ***********************************************************************/
Gia_ManDupZero(Gia_Man_t * p)801 Gia_Man_t * Gia_ManDupZero( Gia_Man_t * p )
802 {
803 Gia_Man_t * pNew; int i;
804 pNew = Gia_ManStart( 1 + Gia_ManCiNum(p) + Gia_ManCoNum(p) );
805 pNew->pName = Abc_UtilStrsav( p->pName );
806 for ( i = 0; i < Gia_ManCiNum(p); i++ )
807 Gia_ManAppendCi( pNew );
808 for ( i = 0; i < Gia_ManCoNum(p); i++ )
809 Gia_ManAppendCo( pNew, 0 );
810 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
811 return pNew;
812 }
813
814 /**Function*************************************************************
815
816 Synopsis [Duplicates AIG without any changes.]
817
818 Description []
819
820 SideEffects []
821
822 SeeAlso []
823
824 ***********************************************************************/
Gia_ManDupPerm(Gia_Man_t * p,Vec_Int_t * vPiPerm)825 Gia_Man_t * Gia_ManDupPerm( Gia_Man_t * p, Vec_Int_t * vPiPerm )
826 {
827 // Vec_Int_t * vPiPermInv;
828 Gia_Man_t * pNew;
829 Gia_Obj_t * pObj;
830 int i;
831 assert( Vec_IntSize(vPiPerm) == Gia_ManPiNum(p) );
832 pNew = Gia_ManStart( Gia_ManObjNum(p) );
833 pNew->pName = Abc_UtilStrsav( p->pName );
834 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
835 Gia_ManConst0(p)->Value = 0;
836 // vPiPermInv = Vec_IntInvert( vPiPerm, -1 );
837 Gia_ManForEachPi( p, pObj, i )
838 // Gia_ManPi(p, Vec_IntEntry(vPiPermInv,i))->Value = Gia_ManAppendCi( pNew );
839 Gia_ManPi(p, Vec_IntEntry(vPiPerm,i))->Value = Gia_ManAppendCi( pNew );
840 // Vec_IntFree( vPiPermInv );
841 Gia_ManForEachObj1( p, pObj, i )
842 {
843 if ( Gia_ObjIsAnd(pObj) )
844 pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
845 else if ( Gia_ObjIsCi(pObj) )
846 {
847 if ( Gia_ObjIsRo(p, pObj) )
848 pObj->Value = Gia_ManAppendCi( pNew );
849 }
850 else if ( Gia_ObjIsCo(pObj) )
851 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
852 }
853 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
854 return pNew;
855 }
Gia_ManDupPermFlop(Gia_Man_t * p,Vec_Int_t * vFfPerm)856 Gia_Man_t * Gia_ManDupPermFlop( Gia_Man_t * p, Vec_Int_t * vFfPerm )
857 {
858 Vec_Int_t * vPermInv;
859 Gia_Man_t * pNew;
860 Gia_Obj_t * pObj;
861 int i;
862 assert( Vec_IntSize(vFfPerm) == Gia_ManRegNum(p) );
863 vPermInv = Vec_IntInvert( vFfPerm, -1 );
864 pNew = Gia_ManStart( Gia_ManObjNum(p) );
865 pNew->pName = Abc_UtilStrsav( p->pName );
866 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
867 Gia_ManConst0(p)->Value = 0;
868 Gia_ManForEachPi( p, pObj, i )
869 pObj->Value = Gia_ManAppendCi(pNew);
870 Gia_ManForEachRo( p, pObj, i )
871 Gia_ManRo(p, Vec_IntEntry(vPermInv, i))->Value = Gia_ManAppendCi(pNew);
872 Gia_ManForEachAnd( p, pObj, i )
873 pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
874 Gia_ManForEachPo( p, pObj, i )
875 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
876 Gia_ManForEachRi( p, pObj, i )
877 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy( Gia_ManRi(p, Vec_IntEntry(vPermInv, i)) ) );
878 Vec_IntFree( vPermInv );
879 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
880 return pNew;
881 }
Gia_ManDupSpreadFlop(Gia_Man_t * p,Vec_Int_t * vFfMask)882 Gia_Man_t * Gia_ManDupSpreadFlop( Gia_Man_t * p, Vec_Int_t * vFfMask )
883 {
884 Gia_Man_t * pNew;
885 Gia_Obj_t * pObj;
886 int i, k, Entry;
887 assert( Vec_IntSize(vFfMask) >= Gia_ManRegNum(p) );
888 pNew = Gia_ManStart( Gia_ManObjNum(p) );
889 pNew->pName = Abc_UtilStrsav( p->pName );
890 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
891 Gia_ManConst0(p)->Value = 0;
892 Gia_ManForEachPi( p, pObj, i )
893 pObj->Value = Gia_ManAppendCi(pNew);
894 k = 0;
895 Vec_IntForEachEntry( vFfMask, Entry, i )
896 if ( Entry == -1 )
897 Gia_ManAppendCi(pNew);
898 else
899 Gia_ManRo(p, k++)->Value = Gia_ManAppendCi(pNew);
900 assert( k == Gia_ManRegNum(p) );
901 Gia_ManForEachAnd( p, pObj, i )
902 pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
903 Gia_ManForEachPo( p, pObj, i )
904 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
905 k = 0;
906 Vec_IntForEachEntry( vFfMask, Entry, i )
907 if ( Entry == -1 )
908 Gia_ManAppendCo( pNew, 0 );
909 else
910 {
911 pObj = Gia_ManRi( p, k++ );
912 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
913 }
914 assert( k == Gia_ManRegNum(p) );
915 Gia_ManSetRegNum( pNew, Vec_IntSize(vFfMask) );
916 return pNew;
917 }
Gia_ManDupPermFlopGap(Gia_Man_t * p,Vec_Int_t * vFfMask)918 Gia_Man_t * Gia_ManDupPermFlopGap( Gia_Man_t * p, Vec_Int_t * vFfMask )
919 {
920 Vec_Int_t * vPerm = Vec_IntCondense( vFfMask, -1 );
921 Gia_Man_t * pPerm = Gia_ManDupPermFlop( p, vPerm );
922 Gia_Man_t * pSpread = Gia_ManDupSpreadFlop( pPerm, vFfMask );
923 Vec_IntFree( vPerm );
924 Gia_ManStop( pPerm );
925 return pSpread;
926 }
927
928 /**Function*************************************************************
929
930 Synopsis [Appends second AIG without any changes.]
931
932 Description []
933
934 SideEffects []
935
936 SeeAlso []
937
938 ***********************************************************************/
Gia_ManDupPiPerm(Gia_Man_t * p)939 Gia_Man_t * Gia_ManDupPiPerm( Gia_Man_t * p )
940 {
941 Gia_Man_t * pNew, * pOne;
942 Gia_Obj_t * pObj;
943 int i;
944 Gia_ManRandom(1);
945 pNew = Gia_ManStart( Gia_ManObjNum(p) );
946 pNew->pName = Abc_UtilStrsav( p->pName );
947 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
948 Gia_ManHashAlloc( pNew );
949 Gia_ManConst0(p)->Value = 0;
950 Gia_ManForEachCi( p, pObj, i )
951 pObj->Value = Gia_ManAppendCi( pNew );
952 Gia_ManForEachAnd( p, pObj, i )
953 {
954 int iLit0 = Gia_ObjFanin0Copy(pObj);
955 int iLit1 = Gia_ObjFanin1Copy(pObj);
956 int iPlace0 = Gia_ManRandom(0) % Gia_ManCiNum(p);
957 int iPlace1 = Gia_ManRandom(0) % Gia_ManCiNum(p);
958 if ( Abc_Lit2Var(iLit0) <= Gia_ManCiNum(p) )
959 iLit0 = Abc_Var2Lit( iPlace0+1, Abc_LitIsCompl(iLit0) );
960 if ( Abc_Lit2Var(iLit1) <= Gia_ManCiNum(p) )
961 iLit1 = Abc_Var2Lit( iPlace1+1, Abc_LitIsCompl(iLit1) );
962 pObj->Value = Gia_ManHashAnd( pNew, iLit0, iLit1 );
963 }
964 Gia_ManForEachCo( p, pObj, i )
965 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
966 Gia_ManHashStop( pNew );
967 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
968 pNew = Gia_ManCleanup( pOne = pNew );
969 Gia_ManStop( pOne );
970 return pNew;
971 }
972
973 /**Function*************************************************************
974
975 Synopsis [Appends second AIG without any changes.]
976
977 Description []
978
979 SideEffects []
980
981 SeeAlso []
982
983 ***********************************************************************/
Gia_ManDupAppend(Gia_Man_t * pNew,Gia_Man_t * pTwo)984 void Gia_ManDupAppend( Gia_Man_t * pNew, Gia_Man_t * pTwo )
985 {
986 Gia_Obj_t * pObj;
987 int i;
988 if ( pNew->nRegs > 0 )
989 pNew->nRegs = 0;
990 if ( Vec_IntSize(&pNew->vHTable) == 0 )
991 Gia_ManHashStart( pNew );
992 Gia_ManConst0(pTwo)->Value = 0;
993 Gia_ManForEachObj1( pTwo, pObj, i )
994 {
995 if ( Gia_ObjIsAnd(pObj) )
996 pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
997 else if ( Gia_ObjIsCi(pObj) )
998 pObj->Value = Gia_ManAppendCi( pNew );
999 else if ( Gia_ObjIsCo(pObj) )
1000 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
1001 }
1002 }
Gia_ManDupAppendShare(Gia_Man_t * pNew,Gia_Man_t * pTwo)1003 void Gia_ManDupAppendShare( Gia_Man_t * pNew, Gia_Man_t * pTwo )
1004 {
1005 Gia_Obj_t * pObj;
1006 int i;
1007 assert( Gia_ManCiNum(pNew) == Gia_ManCiNum(pTwo) );
1008 if ( Vec_IntSize(&pNew->vHTable) == 0 )
1009 Gia_ManHashStart( pNew );
1010 Gia_ManConst0(pTwo)->Value = 0;
1011 Gia_ManForEachObj1( pTwo, pObj, i )
1012 {
1013 if ( Gia_ObjIsAnd(pObj) )
1014 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
1015 else if ( Gia_ObjIsCi(pObj) )
1016 pObj->Value = Gia_Obj2Lit( pNew, Gia_ManCi( pNew, Gia_ObjCioId(pObj) ) );
1017 else if ( Gia_ObjIsCo(pObj) )
1018 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
1019 }
1020 }
Gia_ManDupAppendNew(Gia_Man_t * pOne,Gia_Man_t * pTwo)1021 Gia_Man_t * Gia_ManDupAppendNew( Gia_Man_t * pOne, Gia_Man_t * pTwo )
1022 {
1023 Gia_Man_t * pNew;
1024 Gia_Obj_t * pObj;
1025 int i;
1026 pNew = Gia_ManStart( Gia_ManObjNum(pOne) + Gia_ManObjNum(pTwo) );
1027 pNew->pName = Abc_UtilStrsav( pOne->pName );
1028 pNew->pSpec = Abc_UtilStrsav( pOne->pSpec );
1029 Gia_ManHashAlloc( pNew );
1030 Gia_ManConst0(pOne)->Value = 0;
1031 Gia_ManForEachObj1( pOne, pObj, i )
1032 {
1033 if ( Gia_ObjIsAnd(pObj) )
1034 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
1035 else if ( Gia_ObjIsCi(pObj) )
1036 pObj->Value = Gia_ManAppendCi( pNew );
1037 }
1038 Gia_ManConst0(pTwo)->Value = 0;
1039 Gia_ManForEachObj1( pTwo, pObj, i )
1040 {
1041 if ( Gia_ObjIsAnd(pObj) )
1042 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
1043 else if ( Gia_ObjIsPi(pTwo, pObj) )
1044 pObj->Value = Gia_ManPi(pOne, Gia_ObjCioId(pObj))->Value;
1045 else if ( Gia_ObjIsCi(pObj) )
1046 pObj->Value = Gia_ManAppendCi( pNew );
1047 }
1048 Gia_ManHashStop( pNew );
1049 // primary outputs
1050 Gia_ManForEachPo( pOne, pObj, i )
1051 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
1052 Gia_ManForEachPo( pTwo, pObj, i )
1053 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
1054 // flop inputs
1055 Gia_ManForEachRi( pOne, pObj, i )
1056 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
1057 Gia_ManForEachRi( pTwo, pObj, i )
1058 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
1059 Gia_ManSetRegNum( pNew, Gia_ManRegNum(pOne) + Gia_ManRegNum(pTwo) );
1060 return pNew;
1061 }
1062
1063 /**Function*************************************************************
1064
1065 Synopsis [Creates a miter for inductive checking of the invariant.]
1066
1067 Description [The first GIA (p) is a sequential AIG whose transition
1068 relation is used. The second GIA (pInv) is a combinational AIG representing
1069 the invariant over the register outputs. If the resulting combination miter
1070 is UNSAT, the invariant holds by simple induction.]
1071
1072 SideEffects []
1073
1074 SeeAlso []
1075
1076 ***********************************************************************/
Gia_ManDupInvMiter(Gia_Man_t * p,Gia_Man_t * pInv)1077 Gia_Man_t * Gia_ManDupInvMiter( Gia_Man_t * p, Gia_Man_t * pInv )
1078 {
1079 Gia_Man_t * pNew, * pTemp;
1080 Gia_Obj_t * pObj;
1081 int i, Node1, Node2, Node;
1082 assert( Gia_ManRegNum(p) > 0 );
1083 assert( Gia_ManRegNum(pInv) == 0 );
1084 assert( Gia_ManCoNum(pInv) == 1 );
1085 assert( Gia_ManRegNum(p) == Gia_ManCiNum(pInv) );
1086 Gia_ManFillValue(p);
1087 pNew = Gia_ManStart( Gia_ManObjNum(p) + 2*Gia_ManObjNum(pInv) );
1088 pNew->pName = Abc_UtilStrsav( p->pName );
1089 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
1090 Gia_ManHashAlloc( pNew );
1091 Gia_ManConst0(p)->Value = 0;
1092 Gia_ManForEachObj1( p, pObj, i )
1093 {
1094 if ( Gia_ObjIsAnd(pObj) )
1095 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
1096 else if ( Gia_ObjIsCi(pObj) )
1097 pObj->Value = Gia_ManAppendCi( pNew );
1098 else if ( Gia_ObjIsCo(pObj) )
1099 pObj->Value = Gia_ObjFanin0Copy(pObj);
1100 }
1101 // build invariant on top of register outputs in the first frame
1102 Gia_ManForEachRo( p, pObj, i )
1103 Gia_ManCi(pInv, i)->Value = pObj->Value;
1104 Gia_ManForEachAnd( pInv, pObj, i )
1105 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
1106 pObj = Gia_ManCo( pInv, 0 );
1107 Node1 = Gia_ObjFanin0Copy(pObj);
1108 // build invariant on top of register outputs in the second frame
1109 Gia_ManForEachRi( p, pObj, i )
1110 Gia_ManCi(pInv, i)->Value = pObj->Value;
1111 Gia_ManForEachAnd( pInv, pObj, i )
1112 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
1113 pObj = Gia_ManCo( pInv, 0 );
1114 Node2 = Gia_ObjFanin0Copy(pObj);
1115 // create miter output
1116 Node = Gia_ManHashAnd( pNew, Node1, Abc_LitNot(Node2) );
1117 Gia_ManAppendCo( pNew, Node );
1118 // cleanup
1119 pNew = Gia_ManCleanup( pTemp = pNew );
1120 Gia_ManStop( pTemp );
1121 return pNew;
1122 }
1123
1124 /**Function*************************************************************
1125
1126 Synopsis [Appends logic cones as additional property outputs.]
1127
1128 Description []
1129
1130 SideEffects []
1131
1132 SeeAlso []
1133
1134 ***********************************************************************/
Gia_ManDupAppendCones(Gia_Man_t * p,Gia_Man_t ** ppCones,int nCones,int fOnlyRegs)1135 Gia_Man_t * Gia_ManDupAppendCones( Gia_Man_t * p, Gia_Man_t ** ppCones, int nCones, int fOnlyRegs )
1136 {
1137 Gia_Man_t * pNew, * pOne;
1138 Gia_Obj_t * pObj;
1139 int i, k;
1140 pNew = Gia_ManStart( Gia_ManObjNum(p) );
1141 pNew->pName = Abc_UtilStrsav( p->pName );
1142 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
1143 Gia_ManHashAlloc( pNew );
1144 Gia_ManConst0(p)->Value = 0;
1145 Gia_ManForEachCi( p, pObj, i )
1146 pObj->Value = Gia_ManAppendCi( pNew );
1147 Gia_ManForEachAnd( p, pObj, i )
1148 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
1149 Gia_ManForEachPo( p, pObj, i )
1150 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
1151 for ( k = 0; k < nCones; k++ )
1152 {
1153 pOne = ppCones[k];
1154 assert( Gia_ManPoNum(pOne) == 1 );
1155 assert( Gia_ManRegNum(pOne) == 0 );
1156 if ( fOnlyRegs )
1157 assert( Gia_ManPiNum(pOne) == Gia_ManRegNum(p) );
1158 else
1159 assert( Gia_ManPiNum(pOne) == Gia_ManCiNum(p) );
1160 Gia_ManConst0(pOne)->Value = 0;
1161 Gia_ManForEachPi( pOne, pObj, i )
1162 pObj->Value = Gia_ManCiLit( pNew, fOnlyRegs ? Gia_ManPiNum(p) + i : i );
1163 Gia_ManForEachAnd( pOne, pObj, i )
1164 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
1165 Gia_ManForEachPo( pOne, pObj, i )
1166 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
1167 }
1168 Gia_ManForEachRi( p, pObj, i )
1169 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
1170 Gia_ManHashStop( pNew );
1171 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
1172 pNew = Gia_ManCleanup( pOne = pNew );
1173 Gia_ManStop( pOne );
1174 return pNew;
1175 }
1176
1177
1178 /**Function*************************************************************
1179
1180 Synopsis [Duplicates while adding self-loops to the registers.]
1181
1182 Description []
1183
1184 SideEffects []
1185
1186 SeeAlso []
1187
1188 ***********************************************************************/
Gia_ManDupSelf(Gia_Man_t * p)1189 Gia_Man_t * Gia_ManDupSelf( Gia_Man_t * p )
1190 {
1191 Gia_Man_t * pNew, * pTemp;
1192 Gia_Obj_t * pObj;
1193 int i, iCtrl;
1194 pNew = Gia_ManStart( Gia_ManObjNum(p) );
1195 pNew->pName = Abc_UtilStrsav( p->pName );
1196 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
1197 Gia_ManHashAlloc( pNew );
1198 Gia_ManFillValue( p );
1199 Gia_ManConst0(p)->Value = 0;
1200 iCtrl = Gia_ManAppendCi( pNew );
1201 Gia_ManForEachCi( p, pObj, i )
1202 pObj->Value = Gia_ManAppendCi( pNew );
1203 Gia_ManForEachAnd( p, pObj, i )
1204 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
1205 Gia_ManForEachPo( p, pObj, i )
1206 pObj->Value = Gia_ObjFanin0Copy(pObj);
1207 Gia_ManForEachRi( p, pObj, i )
1208 pObj->Value = Gia_ManHashMux( pNew, iCtrl, Gia_ObjFanin0Copy(pObj), Gia_ObjRiToRo(p, pObj)->Value );
1209 Gia_ManForEachCo( p, pObj, i )
1210 Gia_ManAppendCo( pNew, pObj->Value );
1211 Gia_ManHashStop( pNew );
1212 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
1213 pNew = Gia_ManCleanup( pTemp = pNew );
1214 Gia_ManStop( pTemp );
1215 return pNew;
1216 }
1217
1218 /**Function*************************************************************
1219
1220 Synopsis [Duplicates while adding self-loops to the registers.]
1221
1222 Description []
1223
1224 SideEffects []
1225
1226 SeeAlso []
1227
1228 ***********************************************************************/
Gia_ManDupFlopClass(Gia_Man_t * p,int iClass)1229 Gia_Man_t * Gia_ManDupFlopClass( Gia_Man_t * p, int iClass )
1230 {
1231 Gia_Man_t * pNew;
1232 Gia_Obj_t * pObj;
1233 int i, Counter1 = 0, Counter2 = 0;
1234 assert( p->vFlopClasses != NULL );
1235 pNew = Gia_ManStart( Gia_ManObjNum(p) );
1236 pNew->pName = Abc_UtilStrsav( p->pName );
1237 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
1238 Gia_ManFillValue( p );
1239 Gia_ManConst0(p)->Value = 0;
1240 Gia_ManForEachPi( p, pObj, i )
1241 pObj->Value = Gia_ManAppendCi( pNew );
1242 Gia_ManForEachRo( p, pObj, i )
1243 if ( Vec_IntEntry(p->vFlopClasses, i) != iClass )
1244 pObj->Value = Gia_ManAppendCi( pNew );
1245 Gia_ManForEachRo( p, pObj, i )
1246 if ( Vec_IntEntry(p->vFlopClasses, i) == iClass )
1247 pObj->Value = Gia_ManAppendCi( pNew ), Counter1++;
1248 Gia_ManForEachAnd( p, pObj, i )
1249 pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
1250 Gia_ManForEachPo( p, pObj, i )
1251 Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
1252 Gia_ManForEachRi( p, pObj, i )
1253 if ( Vec_IntEntry(p->vFlopClasses, i) != iClass )
1254 Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
1255 Gia_ManForEachRi( p, pObj, i )
1256 if ( Vec_IntEntry(p->vFlopClasses, i) == iClass )
1257 Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ), Counter2++;
1258 assert( Counter1 == Counter2 );
1259 Gia_ManSetRegNum( pNew, Counter1 );
1260 return pNew;
1261 }
1262
1263 /**Function*************************************************************
1264
1265 Synopsis [Duplicates AIG without any changes.]
1266
1267 Description []
1268
1269 SideEffects []
1270
1271 SeeAlso []
1272
1273 ***********************************************************************/
Gia_ManDupMarked(Gia_Man_t * p)1274 Gia_Man_t * Gia_ManDupMarked( Gia_Man_t * p )
1275 {
1276 Gia_Man_t * pNew;
1277 Gia_Obj_t * pObj;
1278 int i, nRos = 0, nRis = 0;
1279 int CountMarked = 0;
1280 Gia_ManForEachObj( p, pObj, i )
1281 CountMarked += pObj->fMark0;
1282 Gia_ManFillValue( p );
1283 pNew = Gia_ManStart( Gia_ManObjNum(p) - CountMarked );
1284 if ( p->pMuxes )
1285 pNew->pMuxes = ABC_CALLOC( unsigned, pNew->nObjsAlloc );
1286 pNew->nConstrs = p->nConstrs;
1287 pNew->pName = Abc_UtilStrsav( p->pName );
1288 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
1289 Gia_ManConst0(p)->Value = 0;
1290 Gia_ManForEachObj1( p, pObj, i )
1291 {
1292 if ( pObj->fMark0 )
1293 {
1294 assert( !Gia_ObjIsBuf(pObj) );
1295 pObj->fMark0 = 0;
1296 continue;
1297 }
1298 if ( Gia_ObjIsBuf(pObj) )
1299 pObj->Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) );
1300 else if ( Gia_ObjIsAnd(pObj) )
1301 {
1302 if ( Gia_ObjIsXor(pObj) )
1303 pObj->Value = Gia_ManAppendXorReal( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
1304 else if ( Gia_ObjIsMux(p, pObj) )
1305 pObj->Value = Gia_ManAppendMuxReal( pNew, Gia_ObjFanin2Copy(p, pObj), Gia_ObjFanin1Copy(pObj), Gia_ObjFanin0Copy(pObj) );
1306 else
1307 pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
1308 }
1309 else if ( Gia_ObjIsCi(pObj) )
1310 {
1311 pObj->Value = Gia_ManAppendCi( pNew );
1312 nRos += Gia_ObjIsRo(p, pObj);
1313 }
1314 else if ( Gia_ObjIsCo(pObj) )
1315 {
1316 // Gia_Obj_t * pFanin = Gia_ObjFanin0(pObj);
1317 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
1318 nRis += Gia_ObjIsRi(p, pObj);
1319 }
1320 }
1321 assert( pNew->nObjsAlloc == pNew->nObjs );
1322 assert( nRos == nRis );
1323 Gia_ManSetRegNum( pNew, nRos );
1324 if ( p->pReprs && p->pNexts )
1325 {
1326 Gia_Obj_t * pRepr;
1327 pNew->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(pNew) );
1328 for ( i = 0; i < Gia_ManObjNum(p); i++ )
1329 Gia_ObjSetRepr( pNew, i, GIA_VOID );
1330 Gia_ManForEachObj1( p, pObj, i )
1331 {
1332 if ( !~pObj->Value )
1333 continue;
1334 pRepr = Gia_ObjReprObj( p, i );
1335 if ( pRepr == NULL )
1336 continue;
1337 if ( !~pRepr->Value )
1338 continue;
1339 assert( !Gia_ObjIsBuf(pObj) );
1340 if ( Abc_Lit2Var(pObj->Value) != Abc_Lit2Var(pRepr->Value) )
1341 Gia_ObjSetRepr( pNew, Abc_Lit2Var(pObj->Value), Abc_Lit2Var(pRepr->Value) );
1342 }
1343 pNew->pNexts = Gia_ManDeriveNexts( pNew );
1344 }
1345 if ( Gia_ManHasChoices(p) )
1346 {
1347 Gia_Obj_t * pSibl;
1348 pNew->pSibls = ABC_CALLOC( int, Gia_ManObjNum(pNew) );
1349 Gia_ManForEachObj1( p, pObj, i )
1350 {
1351 if ( !~pObj->Value )
1352 continue;
1353 pSibl = Gia_ObjSiblObj( p, i );
1354 if ( pSibl == NULL )
1355 continue;
1356 if ( !~pSibl->Value )
1357 continue;
1358 assert( !Gia_ObjIsBuf(pObj) );
1359 assert( Abc_Lit2Var(pObj->Value) > Abc_Lit2Var(pSibl->Value) );
1360 pNew->pSibls[Abc_Lit2Var(pObj->Value)] = Abc_Lit2Var(pSibl->Value);
1361 }
1362 }
1363 return pNew;
1364 }
1365
1366 /**Function*************************************************************
1367
1368 Synopsis [Duplicates AIG while creating "parallel" copies.]
1369
1370 Description []
1371
1372 SideEffects []
1373
1374 SeeAlso []
1375
1376 ***********************************************************************/
Gia_ManDupTimes(Gia_Man_t * p,int nTimes)1377 Gia_Man_t * Gia_ManDupTimes( Gia_Man_t * p, int nTimes )
1378 {
1379 Gia_Man_t * pNew;
1380 Gia_Obj_t * pObj;
1381 Vec_Int_t * vPis, * vPos, * vRis, * vRos;
1382 int i, t, Entry;
1383 assert( nTimes > 0 );
1384 pNew = Gia_ManStart( Gia_ManObjNum(p) );
1385 pNew->pName = Abc_UtilStrsav( p->pName );
1386 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
1387 Gia_ManConst0(p)->Value = 0;
1388 vPis = Vec_IntAlloc( Gia_ManPiNum(p) * nTimes );
1389 vPos = Vec_IntAlloc( Gia_ManPoNum(p) * nTimes );
1390 vRis = Vec_IntAlloc( Gia_ManRegNum(p) * nTimes );
1391 vRos = Vec_IntAlloc( Gia_ManRegNum(p) * nTimes );
1392 for ( t = 0; t < nTimes; t++ )
1393 {
1394 Gia_ManForEachObj1( p, pObj, i )
1395 {
1396 if ( Gia_ObjIsAnd(pObj) )
1397 pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
1398 else if ( Gia_ObjIsCi(pObj) )
1399 {
1400 pObj->Value = Gia_ManAppendCi( pNew );
1401 if ( Gia_ObjIsPi(p, pObj) )
1402 Vec_IntPush( vPis, Abc_Lit2Var(pObj->Value) );
1403 else
1404 Vec_IntPush( vRos, Abc_Lit2Var(pObj->Value) );
1405 }
1406 else if ( Gia_ObjIsCo(pObj) )
1407 {
1408 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
1409 if ( Gia_ObjIsPo(p, pObj) )
1410 Vec_IntPush( vPos, Abc_Lit2Var(pObj->Value) );
1411 else
1412 Vec_IntPush( vRis, Abc_Lit2Var(pObj->Value) );
1413 }
1414 }
1415 }
1416 Vec_IntClear( pNew->vCis );
1417 Vec_IntForEachEntry( vPis, Entry, i )
1418 {
1419 Gia_ObjSetCioId( Gia_ManObj(pNew, Entry), Vec_IntSize(pNew->vCis) );
1420 Vec_IntPush( pNew->vCis, Entry );
1421 }
1422 Vec_IntForEachEntry( vRos, Entry, i )
1423 {
1424 Gia_ObjSetCioId( Gia_ManObj(pNew, Entry), Vec_IntSize(pNew->vCis) );
1425 Vec_IntPush( pNew->vCis, Entry );
1426 }
1427 Vec_IntClear( pNew->vCos );
1428 Vec_IntForEachEntry( vPos, Entry, i )
1429 {
1430 Gia_ObjSetCioId( Gia_ManObj(pNew, Entry), Vec_IntSize(pNew->vCos) );
1431 Vec_IntPush( pNew->vCos, Entry );
1432 }
1433 Vec_IntForEachEntry( vRis, Entry, i )
1434 {
1435 Gia_ObjSetCioId( Gia_ManObj(pNew, Entry), Vec_IntSize(pNew->vCos) );
1436 Vec_IntPush( pNew->vCos, Entry );
1437 }
1438 Vec_IntFree( vPis );
1439 Vec_IntFree( vPos );
1440 Vec_IntFree( vRis );
1441 Vec_IntFree( vRos );
1442 Gia_ManSetRegNum( pNew, nTimes * Gia_ManRegNum(p) );
1443 return pNew;
1444 }
1445
1446 /**Function*************************************************************
1447
1448 Synopsis [Duplicates the AIG in the DFS order.]
1449
1450 Description []
1451
1452 SideEffects []
1453
1454 SeeAlso []
1455
1456 ***********************************************************************/
Gia_ManDupDfs2_rec(Gia_Man_t * pNew,Gia_Man_t * p,Gia_Obj_t * pObj)1457 int Gia_ManDupDfs2_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
1458 {
1459 if ( ~pObj->Value )
1460 return pObj->Value;
1461 if ( p->pReprsOld && ~p->pReprsOld[Gia_ObjId(p, pObj)] )
1462 {
1463 Gia_Obj_t * pRepr = Gia_ManObj( p, p->pReprsOld[Gia_ObjId(p, pObj)] );
1464 pRepr->Value = Gia_ManDupDfs2_rec( pNew, p, pRepr );
1465 return pObj->Value = Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
1466 }
1467 if ( Gia_ObjIsCi(pObj) )
1468 return pObj->Value = Gia_ManAppendCi(pNew);
1469 Gia_ManDupDfs2_rec( pNew, p, Gia_ObjFanin0(pObj) );
1470 if ( Gia_ObjIsCo(pObj) )
1471 return pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
1472 Gia_ManDupDfs2_rec( pNew, p, Gia_ObjFanin1(pObj) );
1473 if ( Vec_IntSize(&pNew->vHTable) )
1474 return pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
1475 return pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
1476 }
1477
1478 /**Function*************************************************************
1479
1480 Synopsis [Duplicates AIG in the DFS order.]
1481
1482 Description []
1483
1484 SideEffects []
1485
1486 SeeAlso []
1487
1488 ***********************************************************************/
Gia_ManDupDfs2(Gia_Man_t * p)1489 Gia_Man_t * Gia_ManDupDfs2( Gia_Man_t * p )
1490 {
1491 Gia_Man_t * pNew;
1492 Gia_Obj_t * pObj, * pObjNew;
1493 int i;
1494 Gia_ManFillValue( p );
1495 pNew = Gia_ManStart( Gia_ManObjNum(p) );
1496 pNew->pName = Abc_UtilStrsav( p->pName );
1497 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
1498 Gia_ManConst0(p)->Value = 0;
1499 Gia_ManForEachCo( p, pObj, i )
1500 Gia_ManDupDfs2_rec( pNew, p, pObj );
1501 Gia_ManForEachCi( p, pObj, i )
1502 if ( ~pObj->Value == 0 )
1503 pObj->Value = Gia_ManAppendCi(pNew);
1504 assert( Gia_ManCiNum(pNew) == Gia_ManCiNum(p) );
1505 // remap combinational inputs
1506 Gia_ManForEachCi( p, pObj, i )
1507 {
1508 pObjNew = Gia_ObjFromLit( pNew, pObj->Value );
1509 assert( !Gia_IsComplement(pObjNew) );
1510 Vec_IntWriteEntry( pNew->vCis, Gia_ObjCioId(pObj), Gia_ObjId(pNew, pObjNew) );
1511 Gia_ObjSetCioId( pObjNew, Gia_ObjCioId(pObj) );
1512 }
1513 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
1514 return pNew;
1515 }
1516
1517 /**Function*************************************************************
1518
1519 Synopsis [Duplicates the AIG in the DFS order.]
1520
1521 Description []
1522
1523 SideEffects []
1524
1525 SeeAlso []
1526
1527 ***********************************************************************/
Gia_ManDupDfs_rec(Gia_Man_t * pNew,Gia_Man_t * p,Gia_Obj_t * pObj)1528 void Gia_ManDupDfs_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
1529 {
1530 if ( ~pObj->Value )
1531 return;
1532 assert( Gia_ObjIsAnd(pObj) );
1533 Gia_ManDupDfs_rec( pNew, p, Gia_ObjFanin0(pObj) );
1534 Gia_ManDupDfs_rec( pNew, p, Gia_ObjFanin1(pObj) );
1535 pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
1536 }
Gia_ManDupDfs(Gia_Man_t * p)1537 Gia_Man_t * Gia_ManDupDfs( Gia_Man_t * p )
1538 {
1539 Gia_Man_t * pNew;
1540 Gia_Obj_t * pObj;
1541 int i;
1542 pNew = Gia_ManStart( Gia_ManObjNum(p) );
1543 pNew->pName = Abc_UtilStrsav( p->pName );
1544 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
1545 Gia_ManFillValue( p );
1546 Gia_ManConst0(p)->Value = 0;
1547 Gia_ManForEachCi( p, pObj, i )
1548 pObj->Value = Gia_ManAppendCi(pNew);
1549 Gia_ManForEachCo( p, pObj, i )
1550 Gia_ManDupDfs_rec( pNew, p, Gia_ObjFanin0(pObj) );
1551 Gia_ManForEachCo( p, pObj, i )
1552 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
1553 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
1554 pNew->nConstrs = p->nConstrs;
1555 if ( p->pCexSeq )
1556 pNew->pCexSeq = Abc_CexDup( p->pCexSeq, Gia_ManRegNum(p) );
1557 return pNew;
1558 }
Gia_ManDupDfsOnePo(Gia_Man_t * p,int iPo)1559 Gia_Man_t * Gia_ManDupDfsOnePo( Gia_Man_t * p, int iPo )
1560 {
1561 Gia_Man_t * pNew, * pTemp;
1562 Gia_Obj_t * pObj;
1563 int i;
1564 assert( iPo >= 0 && iPo < Gia_ManPoNum(p) );
1565 pNew = Gia_ManStart( Gia_ManObjNum(p) );
1566 pNew->pName = Abc_UtilStrsav( p->pName );
1567 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
1568 Gia_ManFillValue( p );
1569 Gia_ManConst0(p)->Value = 0;
1570 Gia_ManForEachCi( p, pObj, i )
1571 pObj->Value = Gia_ManAppendCi(pNew);
1572 Gia_ManForEachCo( p, pObj, i )
1573 if ( !Gia_ObjIsPo(p, pObj) || i == iPo )
1574 Gia_ManDupDfs_rec( pNew, p, Gia_ObjFanin0(pObj) );
1575 Gia_ManForEachCo( p, pObj, i )
1576 if ( !Gia_ObjIsPo(p, pObj) || i == iPo )
1577 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
1578 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
1579 pNew = Gia_ManCleanup( pTemp = pNew );
1580 Gia_ManStop( pTemp );
1581 return pNew;
1582 }
1583
1584 /**Function*************************************************************
1585
1586 Synopsis [Cofactors w.r.t. a primary input variable.]
1587
1588 Description []
1589
1590 SideEffects []
1591
1592 SeeAlso []
1593
1594 ***********************************************************************/
Gia_ManDupCofactorVar_rec(Gia_Man_t * pNew,Gia_Man_t * p,Gia_Obj_t * pObj)1595 void Gia_ManDupCofactorVar_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
1596 {
1597 if ( ~pObj->Value )
1598 return;
1599 assert( Gia_ObjIsAnd(pObj) );
1600 Gia_ManDupCofactorVar_rec( pNew, p, Gia_ObjFanin0(pObj) );
1601 Gia_ManDupCofactorVar_rec( pNew, p, Gia_ObjFanin1(pObj) );
1602 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
1603 }
Gia_ManDupCofactorVar(Gia_Man_t * p,int iVar,int Value)1604 Gia_Man_t * Gia_ManDupCofactorVar( Gia_Man_t * p, int iVar, int Value )
1605 {
1606 Gia_Man_t * pNew, * pTemp;
1607 Gia_Obj_t * pObj;
1608 int i;
1609 assert( iVar >= 0 && iVar < Gia_ManPiNum(p) );
1610 assert( Value == 0 || Value == 1 );
1611 pNew = Gia_ManStart( Gia_ManObjNum(p) );
1612 pNew->pName = Abc_UtilStrsav( p->pName );
1613 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
1614 Gia_ManFillValue( p );
1615 Gia_ManConst0(p)->Value = 0;
1616 Gia_ManForEachCi( p, pObj, i )
1617 pObj->Value = Gia_ManAppendCi(pNew);
1618 Gia_ManPi( p, iVar )->Value = Value; // modification!
1619 Gia_ManHashAlloc( pNew );
1620 Gia_ManForEachCo( p, pObj, i )
1621 Gia_ManDupCofactorVar_rec( pNew, p, Gia_ObjFanin0(pObj) );
1622 Gia_ManForEachCo( p, pObj, i )
1623 Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
1624 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
1625 pNew->nConstrs = p->nConstrs;
1626 pNew = Gia_ManCleanup( pTemp = pNew );
1627 Gia_ManStop( pTemp );
1628 return pNew;
1629 }
Gia_ManDupMux(int iVar,Gia_Man_t * pCof1,Gia_Man_t * pCof0)1630 Gia_Man_t * Gia_ManDupMux( int iVar, Gia_Man_t * pCof1, Gia_Man_t * pCof0 )
1631 {
1632 Gia_Man_t * pGia[2] = {pCof0, pCof1};
1633 Gia_Man_t * pNew, * pTemp;
1634 Gia_Obj_t * pObj;
1635 int i, n;
1636 assert( Gia_ManRegNum(pCof0) == 0 );
1637 assert( Gia_ManRegNum(pCof1) == 0 );
1638 assert( Gia_ManCoNum(pCof0) == 1 );
1639 assert( Gia_ManCoNum(pCof1) == 1 );
1640 assert( Gia_ManCiNum(pCof1) == Gia_ManCiNum(pCof0) );
1641 assert( iVar >= 0 && iVar < Gia_ManCiNum(pCof1) );
1642 pNew = Gia_ManStart( Gia_ManObjNum(pCof1) + Gia_ManObjNum(pCof0) );
1643 pNew->pName = Abc_UtilStrsav( pCof1->pName );
1644 pNew->pSpec = Abc_UtilStrsav( pCof1->pSpec );
1645 Gia_ManHashAlloc( pNew );
1646 for ( n = 0; n < 2; n++ )
1647 {
1648 Gia_ManFillValue( pGia[n] );
1649 Gia_ManConst0(pGia[n])->Value = 0;
1650 Gia_ManForEachCi( pGia[n], pObj, i )
1651 pObj->Value = n ? Gia_ManCi(pGia[0], i)->Value : Gia_ManAppendCi(pNew);
1652 Gia_ManForEachCo( pGia[n], pObj, i )
1653 Gia_ManDupCofactorVar_rec( pNew, pGia[n], Gia_ObjFanin0(pObj) );
1654 }
1655 Gia_ManForEachCo( pGia[0], pObj, i )
1656 {
1657 int Ctrl = Gia_ManCi(pGia[0], iVar)->Value;
1658 int Lit1 = Gia_ObjFanin0Copy(Gia_ManCo(pGia[1], i));
1659 int Lit0 = Gia_ObjFanin0Copy(pObj);
1660 Gia_ManAppendCo( pNew, Gia_ManHashMux( pNew, Ctrl, Lit1, Lit0 ) );
1661 }
1662 pNew = Gia_ManCleanup( pTemp = pNew );
1663 Gia_ManStop( pTemp );
1664 return pNew;
1665 }
1666
1667 /**Function*************************************************************
1668
1669 Synopsis [Cofactors w.r.t. an internal node.]
1670
1671 Description []
1672
1673 SideEffects []
1674
1675 SeeAlso []
1676
1677 ***********************************************************************/
Gia_ManDupCofactorObj(Gia_Man_t * p,int iObj,int Value)1678 Gia_Man_t * Gia_ManDupCofactorObj( Gia_Man_t * p, int iObj, int Value )
1679 {
1680 Gia_Man_t * pNew, * pTemp;
1681 Gia_Obj_t * pObj;
1682 int i, iObjValue = -1;
1683 assert( Gia_ManRegNum(p) == 0 );
1684 assert( iObj > 0 && iObj < Gia_ManObjNum(p) );
1685 assert( Gia_ObjIsCand(Gia_ManObj(p, iObj)) );
1686 assert( Value == 0 || Value == 1 );
1687 pNew = Gia_ManStart( Gia_ManObjNum(p) );
1688 pNew->pName = Abc_UtilStrsav( p->pName );
1689 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
1690 Gia_ManConst0(p)->Value = 0;
1691 Gia_ManHashAlloc( pNew );
1692 Gia_ManForEachObj1( p, pObj, i )
1693 {
1694 if ( Gia_ObjIsCi(pObj) )
1695 pObj->Value = Gia_ManAppendCi( pNew );
1696 else if ( Gia_ObjIsAnd(pObj) )
1697 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
1698 else if ( Gia_ObjIsCo(pObj) )
1699 pObj->Value = Gia_ManAppendCo( pNew, Gia_ManHashAnd(pNew, Gia_ObjFanin0Copy(pObj), iObjValue) );
1700 if ( i == iObj )
1701 iObjValue = Abc_LitNotCond(pObj->Value, !Value), pObj->Value = Value;
1702 }
1703 pNew = Gia_ManCleanup( pTemp = pNew );
1704 Gia_ManStop( pTemp );
1705 return pNew;
1706 }
1707
1708 /**Function*************************************************************
1709
1710 Synopsis [Reduce bit-width of GIA assuming it is Boolean.]
1711
1712 Description []
1713
1714 SideEffects []
1715
1716 SeeAlso []
1717
1718 ***********************************************************************/
Gia_ManDupBlock(Gia_Man_t * p,int nBlock)1719 Gia_Man_t * Gia_ManDupBlock( Gia_Man_t * p, int nBlock )
1720 {
1721 Gia_Man_t * pNew, * pTemp;
1722 Gia_Obj_t * pObj; int i;
1723 assert( Gia_ManCiNum(p) % nBlock == 0 );
1724 assert( Gia_ManCoNum(p) % nBlock == 0 );
1725 pNew = Gia_ManStart( Gia_ManObjNum(p) );
1726 pNew->pName = Abc_UtilStrsav( p->pName );
1727 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
1728 Gia_ManFillValue( p );
1729 Gia_ManConst0(p)->Value = 0;
1730 Gia_ManForEachCi( p, pObj, i )
1731 pObj->Value = (i % nBlock == 0) ? Gia_ManAppendCi(pNew) : 0;
1732 Gia_ManHashAlloc( pNew );
1733 Gia_ManForEachAnd( p, pObj, i )
1734 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
1735 Gia_ManForEachCo( p, pObj, i )
1736 if ( i % nBlock == 0 )
1737 Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
1738 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p)/nBlock );
1739 pNew = Gia_ManCleanup( pTemp = pNew );
1740 Gia_ManStop( pTemp );
1741 return pNew;
1742 }
1743
1744 /**Function*************************************************************
1745
1746 Synopsis [Existentially quantified given variable.]
1747
1748 Description []
1749
1750 SideEffects []
1751
1752 SeeAlso []
1753
1754 ***********************************************************************/
Gia_ManDupExist(Gia_Man_t * p,int iVar)1755 Gia_Man_t * Gia_ManDupExist( Gia_Man_t * p, int iVar )
1756 {
1757 Gia_Man_t * pNew, * pTemp;
1758 Gia_Obj_t * pObj;
1759 int i;
1760 assert( iVar >= 0 && iVar < Gia_ManPiNum(p) );
1761 assert( Gia_ManPoNum(p) == 1 );
1762 assert( Gia_ManRegNum(p) == 0 );
1763 Gia_ManFillValue( p );
1764 // find the cofactoring variable
1765 pNew = Gia_ManStart( Gia_ManObjNum(p) );
1766 pNew->pName = Abc_UtilStrsav( p->pName );
1767 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
1768 Gia_ManHashAlloc( pNew );
1769 // compute negative cofactor
1770 Gia_ManConst0(p)->Value = 0;
1771 Gia_ManForEachCi( p, pObj, i )
1772 pObj->Value = Gia_ManAppendCi(pNew);
1773 Gia_ManPi( p, iVar )->Value = Abc_Var2Lit( 0, 0 );
1774 Gia_ManForEachAnd( p, pObj, i )
1775 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
1776 Gia_ManForEachPo( p, pObj, i )
1777 pObj->Value = Gia_ObjFanin0Copy(pObj);
1778 // compute the positive cofactor
1779 Gia_ManPi( p, iVar )->Value = Abc_Var2Lit( 0, 1 );
1780 Gia_ManForEachAnd( p, pObj, i )
1781 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
1782 // create OR gate
1783 Gia_ManForEachPo( p, pObj, i )
1784 pObj->Value = Gia_ManAppendCo( pNew, Gia_ManHashOr(pNew, Gia_ObjFanin0Copy(pObj), pObj->Value) );
1785 Gia_ManHashStop( pNew );
1786 pNew = Gia_ManCleanup( pTemp = pNew );
1787 Gia_ManStop( pTemp );
1788 return pNew;
1789 }
1790
1791 /**Function*************************************************************
1792
1793 Synopsis [Existentially quantified given variable.]
1794
1795 Description []
1796
1797 SideEffects []
1798
1799 SeeAlso []
1800
1801 ***********************************************************************/
Gia_ManDupUniv(Gia_Man_t * p,int iVar)1802 Gia_Man_t * Gia_ManDupUniv( Gia_Man_t * p, int iVar )
1803 {
1804 Gia_Man_t * pNew, * pTemp;
1805 Gia_Obj_t * pObj;
1806 int i;
1807 assert( iVar >= 0 && iVar < Gia_ManPiNum(p) );
1808 assert( Gia_ManRegNum(p) == 0 );
1809 Gia_ManFillValue( p );
1810 // find the cofactoring variable
1811 pNew = Gia_ManStart( Gia_ManObjNum(p) );
1812 pNew->pName = Abc_UtilStrsav( p->pName );
1813 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
1814 Gia_ManHashAlloc( pNew );
1815 // compute negative cofactor
1816 Gia_ManConst0(p)->Value = 0;
1817 Gia_ManForEachCi( p, pObj, i )
1818 pObj->Value = Gia_ManAppendCi(pNew);
1819 Gia_ManPi( p, iVar )->Value = Abc_Var2Lit( 0, 0 );
1820 Gia_ManForEachAnd( p, pObj, i )
1821 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
1822 Gia_ManForEachPo( p, pObj, i )
1823 pObj->Value = Gia_ObjFanin0Copy(pObj);
1824 // compute the positive cofactor
1825 Gia_ManPi( p, iVar )->Value = Abc_Var2Lit( 0, 1 );
1826 Gia_ManForEachAnd( p, pObj, i )
1827 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
1828 // create OR gate
1829 Gia_ManForEachPo( p, pObj, i )
1830 {
1831 if ( i == 0 )
1832 pObj->Value = Gia_ManAppendCo( pNew, Gia_ManHashAnd(pNew, Gia_ObjFanin0Copy(pObj), pObj->Value) );
1833 else
1834 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
1835 }
1836 Gia_ManHashStop( pNew );
1837 pNew = Gia_ManCleanup( pTemp = pNew );
1838 Gia_ManStop( pTemp );
1839 return pNew;
1840 }
1841
1842 /**Function*************************************************************
1843
1844 Synopsis [Existentially quantifies the given variable.]
1845
1846 Description []
1847
1848 SideEffects []
1849
1850 SeeAlso []
1851
1852 ***********************************************************************/
Gia_ManDupExist2(Gia_Man_t * p,int iVar)1853 Gia_Man_t * Gia_ManDupExist2( Gia_Man_t * p, int iVar )
1854 {
1855 Gia_Man_t * pNew, * pTemp;
1856 Gia_Obj_t * pObj;
1857 int i;
1858 assert( iVar >= 0 && iVar < Gia_ManPiNum(p) );
1859 pNew = Gia_ManStart( Gia_ManObjNum(p) );
1860 pNew->pName = Abc_UtilStrsav( p->pName );
1861 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
1862 Gia_ManFillValue( p );
1863 Gia_ManHashAlloc( pNew );
1864 Gia_ManConst0(p)->Value = 0;
1865 Gia_ManForEachCi( p, pObj, i )
1866 pObj->Value = Gia_ManAppendCi(pNew);
1867 // first part
1868 Gia_ManPi( p, iVar )->Value = 0; // modification!
1869 Gia_ManForEachCo( p, pObj, i )
1870 Gia_ManDupCofactorVar_rec( pNew, p, Gia_ObjFanin0(pObj) );
1871 Gia_ManForEachCo( p, pObj, i )
1872 pObj->Value = Gia_ObjFanin0Copy(pObj);
1873 // second part
1874 Gia_ManPi( p, iVar )->Value = 1; // modification!
1875 Gia_ManForEachAnd( p, pObj, i )
1876 pObj->Value = ~0;
1877 Gia_ManForEachCo( p, pObj, i )
1878 Gia_ManDupCofactorVar_rec( pNew, p, Gia_ObjFanin0(pObj) );
1879 // combination
1880 Gia_ManForEachCo( p, pObj, i )
1881 Gia_ManAppendCo( pNew, Gia_ManHashOr(pNew, Gia_ObjFanin0Copy(pObj), pObj->Value) );
1882 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
1883 pNew->nConstrs = p->nConstrs;
1884 pNew = Gia_ManCleanup( pTemp = pNew );
1885 Gia_ManStop( pTemp );
1886 return pNew;
1887 }
1888
1889
1890 /**Function*************************************************************
1891
1892 Synopsis [Duplicates AIG in the DFS order while putting CIs first.]
1893
1894 Description []
1895
1896 SideEffects []
1897
1898 SeeAlso []
1899
1900 ***********************************************************************/
Gia_ManDupDfsSkip(Gia_Man_t * p)1901 Gia_Man_t * Gia_ManDupDfsSkip( Gia_Man_t * p )
1902 {
1903 Gia_Man_t * pNew;
1904 Gia_Obj_t * pObj;
1905 int i;
1906 Gia_ManFillValue( p );
1907 pNew = Gia_ManStart( Gia_ManObjNum(p) );
1908 pNew->pName = Abc_UtilStrsav( p->pName );
1909 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
1910 Gia_ManConst0(p)->Value = 0;
1911 Gia_ManForEachCi( p, pObj, i )
1912 pObj->Value = Gia_ManAppendCi(pNew);
1913 Gia_ManForEachCo( p, pObj, i )
1914 if ( pObj->fMark1 == 0 )
1915 Gia_ManDupDfs_rec( pNew, p, pObj );
1916 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
1917 return pNew;
1918 }
1919
1920 /**Function*************************************************************
1921
1922 Synopsis [Duplicates AIG in the DFS order while putting CIs first.]
1923
1924 Description []
1925
1926 SideEffects []
1927
1928 SeeAlso []
1929
1930 ***********************************************************************/
Gia_ManDupDfsCone(Gia_Man_t * p,Gia_Obj_t * pRoot)1931 Gia_Man_t * Gia_ManDupDfsCone( Gia_Man_t * p, Gia_Obj_t * pRoot )
1932 {
1933 Gia_Man_t * pNew;
1934 Gia_Obj_t * pObj;
1935 int i;
1936 assert( Gia_ObjIsCo(pRoot) );
1937 Gia_ManFillValue( p );
1938 pNew = Gia_ManStart( Gia_ManObjNum(p) );
1939 pNew->pName = Abc_UtilStrsav( p->pName );
1940 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
1941 Gia_ManConst0(p)->Value = 0;
1942 Gia_ManForEachCi( p, pObj, i )
1943 pObj->Value = Gia_ManAppendCi(pNew);
1944 Gia_ManDupDfs_rec( pNew, p, Gia_ObjFanin0(pRoot) );
1945 Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pRoot) );
1946 Gia_ManSetRegNum( pNew, 0 );
1947 return pNew;
1948 }
1949
1950 /**Function*************************************************************
1951
1952 Synopsis [Duplicates logic cone of the literal and inserts it back.]
1953
1954 Description []
1955
1956 SideEffects []
1957
1958 SeeAlso []
1959
1960 ***********************************************************************/
Gia_ManDupConeSupp_rec(Gia_Man_t * pNew,Gia_Man_t * p,Gia_Obj_t * pObj,Vec_Int_t * vObjs)1961 void Gia_ManDupConeSupp_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vObjs )
1962 {
1963 int iLit0, iLit1, iObj = Gia_ObjId( p, pObj );
1964 int iLit = Gia_ObjCopyArray( p, iObj );
1965 if ( iLit >= 0 )
1966 return;
1967 assert( Gia_ObjIsAnd(pObj) );
1968 Gia_ManDupConeSupp_rec( pNew, p, Gia_ObjFanin0(pObj), vObjs );
1969 Gia_ManDupConeSupp_rec( pNew, p, Gia_ObjFanin1(pObj), vObjs );
1970 iLit0 = Gia_ObjCopyArray( p, Gia_ObjFaninId0(pObj, iObj) );
1971 iLit1 = Gia_ObjCopyArray( p, Gia_ObjFaninId1(pObj, iObj) );
1972 iLit0 = Abc_LitNotCond( iLit0, Gia_ObjFaninC0(pObj) );
1973 iLit1 = Abc_LitNotCond( iLit1, Gia_ObjFaninC1(pObj) );
1974 iLit = Gia_ManAppendAnd( pNew, iLit0, iLit1 );
1975 Gia_ObjSetCopyArray( p, iObj, iLit );
1976 Vec_IntPush( vObjs, iObj );
1977 }
Gia_ManDupConeSupp(Gia_Man_t * p,int iLit,Vec_Int_t * vCiIds)1978 Gia_Man_t * Gia_ManDupConeSupp( Gia_Man_t * p, int iLit, Vec_Int_t * vCiIds )
1979 {
1980 Gia_Man_t * pNew; int i, iLit0;
1981 Gia_Obj_t * pObj, * pRoot = Gia_ManObj( p, Abc_Lit2Var(iLit) );
1982 Vec_Int_t * vObjs = Vec_IntAlloc( 1000 );
1983 //assert( Gia_ObjIsAnd(pRoot) );
1984 if ( Vec_IntSize(&p->vCopies) < Gia_ManObjNum(p) )
1985 Vec_IntFillExtra( &p->vCopies, Gia_ManObjNum(p), -1 );
1986 pNew = Gia_ManStart( Gia_ManObjNum(p) );
1987 pNew->pName = Abc_UtilStrsav( p->pName );
1988 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
1989 Gia_ManForEachCiVec( vCiIds, p, pObj, i )
1990 Gia_ObjSetCopyArray( p, Gia_ObjId(p, pObj), Gia_ManAppendCi(pNew) );
1991 Gia_ManDupConeSupp_rec( pNew, p, pRoot, vObjs );
1992 iLit0 = Gia_ObjCopyArray( p, Abc_Lit2Var(iLit) );
1993 iLit0 = Abc_LitNotCond( iLit0, Abc_LitIsCompl(iLit) );
1994 Gia_ManAppendCo( pNew, iLit0 );
1995 Gia_ManForEachCiVec( vCiIds, p, pObj, i )
1996 Gia_ObjSetCopyArray( p, Gia_ObjId(p, pObj), -1 );
1997 Gia_ManForEachObjVec( vObjs, p, pObj, i )
1998 Gia_ObjSetCopyArray( p, Gia_ObjId(p, pObj), -1 );
1999 Vec_IntFree( vObjs );
2000 //assert( Vec_IntCountLarger(&p->vCopies, -1) == 0 );
2001 return pNew;
2002 }
Gia_ManDupConeBack_rec(Gia_Man_t * pNew,Gia_Man_t * p,Gia_Obj_t * pObj)2003 void Gia_ManDupConeBack_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
2004 {
2005 if ( ~pObj->Value )
2006 return;
2007 assert( Gia_ObjIsAnd(pObj) );
2008 Gia_ManDupConeBack_rec( pNew, p, Gia_ObjFanin0(pObj) );
2009 Gia_ManDupConeBack_rec( pNew, p, Gia_ObjFanin1(pObj) );
2010 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
2011 // pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
2012 }
Gia_ManDupConeBack(Gia_Man_t * p,Gia_Man_t * pNew,Vec_Int_t * vCiIds)2013 int Gia_ManDupConeBack( Gia_Man_t * p, Gia_Man_t * pNew, Vec_Int_t * vCiIds )
2014 {
2015 Gia_Obj_t * pObj, * pRoot; int i;
2016 assert( Gia_ManCiNum(pNew) == Vec_IntSize(vCiIds) );
2017 Gia_ManFillValue(pNew);
2018 Gia_ManConst0(pNew)->Value = 0;
2019 Gia_ManForEachCi( pNew, pObj, i )
2020 pObj->Value = Gia_Obj2Lit( p, Gia_ManCi(p, Vec_IntEntry(vCiIds, i)) );
2021 pRoot = Gia_ManCo(pNew, 0);
2022 Gia_ManDupConeBack_rec( p, pNew, Gia_ObjFanin0(pRoot) );
2023 return Gia_ObjFanin0Copy(pRoot);
2024 }
Gia_ManDupConeBackObjs(Gia_Man_t * p,Gia_Man_t * pNew,Vec_Int_t * vObjs)2025 int Gia_ManDupConeBackObjs( Gia_Man_t * p, Gia_Man_t * pNew, Vec_Int_t * vObjs )
2026 {
2027 Gia_Obj_t * pObj, * pRoot; int i;
2028 assert( Gia_ManCiNum(pNew) == Vec_IntSize(vObjs) );
2029 Gia_ManFillValue(pNew);
2030 Gia_ManConst0(pNew)->Value = 0;
2031 Gia_ManForEachCi( pNew, pObj, i )
2032 pObj->Value = Abc_Var2Lit( Vec_IntEntry(vObjs, i), 0 );
2033 pRoot = Gia_ManCo(pNew, 0);
2034 Gia_ManDupConeBack_rec( p, pNew, Gia_ObjFanin0(pRoot) );
2035 return Gia_ObjFanin0Copy(pRoot);
2036 }
2037
2038
2039 /**Function*************************************************************
2040
2041 Synopsis [Duplicates AIG in the DFS order while putting CIs first.]
2042
2043 Description []
2044
2045 SideEffects []
2046
2047 SeeAlso []
2048
2049 ***********************************************************************/
Gia_ManDupDfs3_rec(Gia_Man_t * pNew,Gia_Man_t * p,Gia_Obj_t * pObj)2050 void Gia_ManDupDfs3_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
2051 {
2052 if ( ~pObj->Value )
2053 return;
2054 if ( Gia_ObjIsCi(pObj) )
2055 {
2056 pObj->Value = Gia_ManAppendCi(pNew);
2057 return;
2058 }
2059 assert( Gia_ObjIsAnd(pObj) );
2060 Gia_ManDupDfs3_rec( pNew, p, Gia_ObjFanin0(pObj) );
2061 Gia_ManDupDfs3_rec( pNew, p, Gia_ObjFanin1(pObj) );
2062 pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
2063 }
Gia_ManDupDfsNode(Gia_Man_t * p,Gia_Obj_t * pRoot)2064 Gia_Man_t * Gia_ManDupDfsNode( Gia_Man_t * p, Gia_Obj_t * pRoot )
2065 {
2066 Gia_Man_t * pNew;
2067 assert( Gia_ObjIsAnd(pRoot) );
2068 Gia_ManFillValue( p );
2069 pNew = Gia_ManStart( Gia_ManObjNum(p) );
2070 pNew->pName = Abc_UtilStrsav( p->pName );
2071 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
2072 Gia_ManConst0(p)->Value = 0;
2073 Gia_ManDupDfs3_rec( pNew, p, pRoot );
2074 Gia_ManAppendCo( pNew, pRoot->Value );
2075 return pNew;
2076 }
2077
2078 /**Function*************************************************************
2079
2080 Synopsis [Duplicates AIG in the DFS order while putting CIs first.]
2081
2082 Description []
2083
2084 SideEffects []
2085
2086 SeeAlso []
2087
2088 ***********************************************************************/
Gia_ManDupDfsLitArray(Gia_Man_t * p,Vec_Int_t * vLits)2089 Gia_Man_t * Gia_ManDupDfsLitArray( Gia_Man_t * p, Vec_Int_t * vLits )
2090 {
2091 Gia_Man_t * pNew;
2092 Gia_Obj_t * pObj;
2093 int i, iLit, iLitRes;
2094 Gia_ManFillValue( p );
2095 pNew = Gia_ManStart( Gia_ManObjNum(p) );
2096 pNew->pName = Abc_UtilStrsav( p->pName );
2097 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
2098 Gia_ManConst0(p)->Value = 0;
2099 Gia_ManForEachCi( p, pObj, i )
2100 pObj->Value = Gia_ManAppendCi(pNew);
2101 Vec_IntForEachEntry( vLits, iLit, i )
2102 {
2103 iLitRes = Gia_ManDupDfs2_rec( pNew, p, Gia_ManObj(p, Abc_Lit2Var(iLit)) );
2104 Gia_ManAppendCo( pNew, Abc_LitNotCond( iLitRes, Abc_LitIsCompl(iLit)) );
2105 }
2106 Gia_ManSetRegNum( pNew, 0 );
2107 return pNew;
2108 }
2109
2110 /**Function*************************************************************
2111
2112 Synopsis [Returns the array of non-const-0 POs of the dual-output miter.]
2113
2114 Description []
2115
2116 SideEffects []
2117
2118 SeeAlso []
2119
2120 ***********************************************************************/
Gia_ManDupTrimmedNonZero(Gia_Man_t * p)2121 Vec_Int_t * Gia_ManDupTrimmedNonZero( Gia_Man_t * p )
2122 {
2123 Vec_Int_t * vNonZero;
2124 Gia_Man_t * pTemp, * pNonDual;
2125 Gia_Obj_t * pObj;
2126 int i;
2127 assert( (Gia_ManPoNum(p) & 1) == 0 );
2128 pNonDual = Gia_ManTransformMiter( p );
2129 pNonDual = Gia_ManSeqStructSweep( pTemp = pNonDual, 1, 1, 0 );
2130 Gia_ManStop( pTemp );
2131 assert( Gia_ManPiNum(pNonDual) > 0 );
2132 assert( 2 * Gia_ManPoNum(pNonDual) == Gia_ManPoNum(p) );
2133 // skip PO pairs corresponding to const0 POs of the non-dual miter
2134 vNonZero = Vec_IntAlloc( 100 );
2135 Gia_ManForEachPo( pNonDual, pObj, i )
2136 if ( !Gia_ObjIsConst0(Gia_ObjFanin0(pObj)) )
2137 Vec_IntPush( vNonZero, i );
2138 Gia_ManStop( pNonDual );
2139 return vNonZero;
2140 }
2141
2142
2143 /**Function*************************************************************
2144
2145 Synopsis [Returns 1 if PO can be removed.]
2146
2147 Description []
2148
2149 SideEffects []
2150
2151 SeeAlso []
2152
2153 ***********************************************************************/
Gia_ManPoIsToRemove(Gia_Man_t * p,Gia_Obj_t * pObj,int Value)2154 int Gia_ManPoIsToRemove( Gia_Man_t * p, Gia_Obj_t * pObj, int Value )
2155 {
2156 assert( Gia_ObjIsCo(pObj) );
2157 if ( Value == -1 )
2158 return Gia_ObjIsConst0(Gia_ObjFanin0(pObj));
2159 assert( Value == 0 || Value == 1 );
2160 return Gia_ObjIsConst0(Gia_ObjFanin0(pObj)) && Value == Gia_ObjFaninC0(pObj);
2161 }
2162
2163 /**Function*************************************************************
2164
2165 Synopsis [Duplicates AIG in the DFS order while putting CIs first.]
2166
2167 Description []
2168
2169 SideEffects []
2170
2171 SeeAlso []
2172
2173 ***********************************************************************/
Gia_ManDupTrimmed(Gia_Man_t * p,int fTrimCis,int fTrimCos,int fDualOut,int OutValue)2174 Gia_Man_t * Gia_ManDupTrimmed( Gia_Man_t * p, int fTrimCis, int fTrimCos, int fDualOut, int OutValue )
2175 {
2176 Vec_Int_t * vNonZero = NULL;
2177 Gia_Man_t * pNew, * pTemp;
2178 Gia_Obj_t * pObj;
2179 int i, Entry;
2180 // collect non-zero
2181 if ( fDualOut && fTrimCos )
2182 vNonZero = Gia_ManDupTrimmedNonZero( p );
2183 // start new manager
2184 pNew = Gia_ManStart( Gia_ManObjNum(p) );
2185 pNew->pName = Abc_UtilStrsav( p->pName );
2186 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
2187 // check if there are PIs to be added
2188 Gia_ManCreateRefs( p );
2189 Gia_ManForEachPi( p, pObj, i )
2190 if ( !fTrimCis || Gia_ObjRefNum(p, pObj) )
2191 break;
2192 if ( i == Gia_ManPiNum(p) ) // there is no PIs - add dummy PI
2193 Gia_ManAppendCi(pNew);
2194 // add the ROs
2195 Gia_ManFillValue( p );
2196 Gia_ManConst0(p)->Value = 0;
2197 Gia_ManForEachCi( p, pObj, i )
2198 if ( !fTrimCis || Gia_ObjRefNum(p, pObj) || Gia_ObjIsRo(p, pObj) )
2199 pObj->Value = Gia_ManAppendCi(pNew);
2200 Gia_ManForEachAnd( p, pObj, i )
2201 pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
2202 if ( fDualOut && fTrimCos )
2203 {
2204 Vec_IntForEachEntry( vNonZero, Entry, i )
2205 {
2206 Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(Gia_ManPo(p, 2*Entry+0)) );
2207 Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(Gia_ManPo(p, 2*Entry+1)) );
2208 }
2209 if ( Gia_ManPoNum(pNew) == 0 ) // nothing - add dummy PO
2210 {
2211 // Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(Gia_ManPo(p, 0)) );
2212 // Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(Gia_ManPo(p, 1)) );
2213 Gia_ManAppendCo( pNew, 0 );
2214 Gia_ManAppendCo( pNew, 0 );
2215 }
2216 Gia_ManForEachRi( p, pObj, i )
2217 Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
2218 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
2219 // cleanup
2220 pNew = Gia_ManSeqStructSweep( pTemp = pNew, 1, 1, 0 );
2221 Gia_ManStop( pTemp );
2222 // trim the PIs
2223 // pNew = Gia_ManDupTrimmed( pTemp = pNew, 1, 0, 0 );
2224 // Gia_ManStop( pTemp );
2225 }
2226 else
2227 {
2228 // check if there are POs to be added
2229 Gia_ManForEachPo( p, pObj, i )
2230 if ( !fTrimCos || !Gia_ManPoIsToRemove(p, pObj, OutValue) )
2231 break;
2232 if ( i == Gia_ManPoNum(p) ) // there is no POs - add dummy PO
2233 Gia_ManAppendCo( pNew, 0 );
2234 Gia_ManForEachCo( p, pObj, i )
2235 if ( !fTrimCos || !Gia_ManPoIsToRemove(p, pObj, OutValue) || Gia_ObjIsRi(p, pObj) )
2236 Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
2237 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
2238 }
2239 Vec_IntFreeP( &vNonZero );
2240 assert( !Gia_ManHasDangling( pNew ) );
2241 return pNew;
2242 }
2243
2244 /**Function*************************************************************
2245
2246 Synopsis [Removes POs driven by PIs and PIs without fanout.]
2247
2248 Description []
2249
2250 SideEffects []
2251
2252 SeeAlso []
2253
2254 ***********************************************************************/
Gia_ManDupTrimmed2(Gia_Man_t * p)2255 Gia_Man_t * Gia_ManDupTrimmed2( Gia_Man_t * p )
2256 {
2257 Gia_Man_t * pNew;
2258 Gia_Obj_t * pObj;
2259 int i;
2260 // start new manager
2261 pNew = Gia_ManStart( Gia_ManObjNum(p) );
2262 pNew->pName = Abc_UtilStrsav( p->pName );
2263 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
2264 // check if there are PIs to be added
2265 Gia_ManCreateRefs( p );
2266 // discount references of POs
2267 Gia_ManForEachPo( p, pObj, i )
2268 Gia_ObjRefFanin0Dec( p, pObj );
2269 // check if PIs are left
2270 Gia_ManForEachPi( p, pObj, i )
2271 if ( Gia_ObjRefNum(p, pObj) )
2272 break;
2273 if ( i == Gia_ManPiNum(p) ) // there is no PIs - add dummy PI
2274 Gia_ManAppendCi(pNew);
2275 // add the ROs
2276 Gia_ManFillValue( p );
2277 Gia_ManConst0(p)->Value = 0;
2278 Gia_ManForEachCi( p, pObj, i )
2279 if ( Gia_ObjRefNum(p, pObj) || Gia_ObjIsRo(p, pObj) )
2280 pObj->Value = Gia_ManAppendCi(pNew);
2281 Gia_ManForEachAnd( p, pObj, i )
2282 pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
2283 // check if there are POs to be added
2284 Gia_ManForEachPo( p, pObj, i )
2285 if ( !Gia_ObjIsConst0(Gia_ObjFanin0(pObj)) && !Gia_ObjIsPi(p, Gia_ObjFanin0(pObj)) )
2286 break;
2287 if ( i == Gia_ManPoNum(p) ) // there is no POs - add dummy PO
2288 Gia_ManAppendCo( pNew, 0 );
2289 Gia_ManForEachCo( p, pObj, i )
2290 if ( (!Gia_ObjIsConst0(Gia_ObjFanin0(pObj)) && !Gia_ObjIsPi(p, Gia_ObjFanin0(pObj))) || Gia_ObjIsRi(p, pObj) )
2291 Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
2292 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
2293 assert( !Gia_ManHasDangling( pNew ) );
2294 return pNew;
2295 }
2296
2297 /**Function*************************************************************
2298
2299 Synopsis [Duplicates AIG in the DFS order while putting CIs first.]
2300
2301 Description []
2302
2303 SideEffects []
2304
2305 SeeAlso []
2306
2307 ***********************************************************************/
Gia_ManDupOntop(Gia_Man_t * p,Gia_Man_t * p2)2308 Gia_Man_t * Gia_ManDupOntop( Gia_Man_t * p, Gia_Man_t * p2 )
2309 {
2310 Gia_Man_t * pTemp, * pNew;
2311 Gia_Obj_t * pObj;
2312 int i;
2313 assert( Gia_ManPoNum(p) == Gia_ManPiNum(p2) );
2314 assert( Gia_ManRegNum(p) == 0 );
2315 assert( Gia_ManRegNum(p2) == 0 );
2316 pNew = Gia_ManStart( Gia_ManObjNum(p)+Gia_ManObjNum(p2) );
2317 pNew->pName = Abc_UtilStrsav( p->pName );
2318 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
2319 Gia_ManHashAlloc( pNew );
2320 // dup first AIG
2321 Gia_ManConst0(p)->Value = 0;
2322 Gia_ManForEachCi( p, pObj, i )
2323 pObj->Value = Gia_ManAppendCi(pNew);
2324 Gia_ManForEachAnd( p, pObj, i )
2325 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
2326 // dup second AIG
2327 Gia_ManConst0(p2)->Value = 0;
2328 Gia_ManForEachCo( p, pObj, i )
2329 Gia_ManPi(p2, i)->Value = Gia_ObjFanin0Copy(pObj);
2330 Gia_ManForEachAnd( p2, pObj, i )
2331 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
2332 Gia_ManForEachCo( p2, pObj, i )
2333 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
2334 Gia_ManHashStop( pNew );
2335 // Gia_ManPrintStats( pGiaNew, 0 );
2336 pNew = Gia_ManCleanup( pTemp = pNew );
2337 Gia_ManStop( pTemp );
2338 return pNew;
2339 }
2340
2341 /**Function*************************************************************
2342
2343 Synopsis [Duplicates transition relation from p1 and property from p2.]
2344
2345 Description []
2346
2347 SideEffects []
2348
2349 SeeAlso []
2350
2351 ***********************************************************************/
Gia_ManDupWithNewPo(Gia_Man_t * p1,Gia_Man_t * p2)2352 Gia_Man_t * Gia_ManDupWithNewPo( Gia_Man_t * p1, Gia_Man_t * p2 )
2353 {
2354 Gia_Man_t * pTemp, * pNew;
2355 Gia_Obj_t * pObj;
2356 int i;
2357 // there is no flops in p2
2358 assert( Gia_ManRegNum(p2) == 0 );
2359 // there is only one PO in p2
2360 // assert( Gia_ManPoNum(p2) == 1 );
2361 // input count of p2 is equal to flop count of p1
2362 assert( Gia_ManPiNum(p2) == Gia_ManRegNum(p1) );
2363
2364 // start new AIG
2365 pNew = Gia_ManStart( Gia_ManObjNum(p1)+Gia_ManObjNum(p2) );
2366 pNew->pName = Abc_UtilStrsav( p1->pName );
2367 pNew->pSpec = Abc_UtilStrsav( p1->pSpec );
2368 Gia_ManHashAlloc( pNew );
2369 // dup first AIG
2370 Gia_ManConst0(p1)->Value = 0;
2371 Gia_ManForEachCi( p1, pObj, i )
2372 pObj->Value = Gia_ManAppendCi(pNew);
2373 Gia_ManForEachAnd( p1, pObj, i )
2374 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
2375 // dup second AIG
2376 Gia_ManConst0(p2)->Value = 0;
2377 Gia_ManForEachPi( p2, pObj, i )
2378 pObj->Value = Gia_ManRo(p1, i)->Value;
2379 Gia_ManForEachAnd( p2, pObj, i )
2380 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
2381 // add property output
2382 Gia_ManForEachPo( p2, pObj, i )
2383 Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
2384 // add flop inputs
2385 Gia_ManForEachRi( p1, pObj, i )
2386 Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
2387 Gia_ManHashStop( pNew );
2388 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p1) );
2389 pNew = Gia_ManCleanup( pTemp = pNew );
2390 Gia_ManStop( pTemp );
2391 return pNew;
2392 }
2393
2394 /**Function*************************************************************
2395
2396 Synopsis [Print representatives.]
2397
2398 Description []
2399
2400 SideEffects []
2401
2402 SeeAlso []
2403
2404 ***********************************************************************/
Gia_ManPrintRepr(Gia_Man_t * p)2405 void Gia_ManPrintRepr( Gia_Man_t * p )
2406 {
2407 Gia_Obj_t * pObj;
2408 int i;
2409 Gia_ManForEachObj( p, pObj, i )
2410 if ( ~p->pReprsOld[i] )
2411 printf( "%d->%d ", i, p->pReprs[i].iRepr );
2412 printf( "\n" );
2413 }
2414
2415 /**Function*************************************************************
2416
2417 Synopsis [Duplicates AIG in the DFS order.]
2418
2419 Description []
2420
2421 SideEffects []
2422
2423 SeeAlso []
2424
2425 ***********************************************************************/
Gia_ManDupDfsCiMap(Gia_Man_t * p,int * pCi2Lit,Vec_Int_t * vLits)2426 Gia_Man_t * Gia_ManDupDfsCiMap( Gia_Man_t * p, int * pCi2Lit, Vec_Int_t * vLits )
2427 {
2428 Gia_Man_t * pNew;
2429 Gia_Obj_t * pObj;
2430 int i;
2431 Gia_ManFillValue( p );
2432 pNew = Gia_ManStart( Gia_ManObjNum(p) );
2433 pNew->pName = Abc_UtilStrsav( p->pName );
2434 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
2435 Gia_ManConst0(p)->Value = 0;
2436 Gia_ManForEachCi( p, pObj, i )
2437 {
2438 pObj->Value = Gia_ManAppendCi(pNew);
2439 if ( ~pCi2Lit[i] )
2440 pObj->Value = Abc_LitNotCond( Gia_ManObj(p, Abc_Lit2Var(pCi2Lit[i]))->Value, Abc_LitIsCompl(pCi2Lit[i]) );
2441 }
2442 Gia_ManHashAlloc( pNew );
2443 if ( vLits )
2444 {
2445 int iLit, iLitRes;
2446 Vec_IntForEachEntry( vLits, iLit, i )
2447 {
2448 iLitRes = Gia_ManDupDfs2_rec( pNew, p, Gia_ManObj(p, Abc_Lit2Var(iLit)) );
2449 Gia_ManAppendCo( pNew, Abc_LitNotCond( iLitRes, Abc_LitIsCompl(iLit)) );
2450 }
2451 }
2452 else
2453 {
2454 Gia_ManForEachCo( p, pObj, i )
2455 {
2456 Gia_ManDupDfs2_rec( pNew, p, Gia_ObjFanin0(pObj) );
2457 Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
2458 }
2459 }
2460 Gia_ManHashStop( pNew );
2461 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
2462 return pNew;
2463 }
2464
2465 /**Function*************************************************************
2466
2467 Synopsis [Permute inputs.]
2468
2469 Description []
2470
2471 SideEffects []
2472
2473 SeeAlso []
2474
2475 ***********************************************************************/
Gia_ManPermuteInputs(Gia_Man_t * p,int nPpis,int nExtra)2476 Gia_Man_t * Gia_ManPermuteInputs( Gia_Man_t * p, int nPpis, int nExtra )
2477 {
2478 Gia_Man_t * pNew;
2479 Gia_Obj_t * pObj;
2480 int i;
2481 pNew = Gia_ManStart( Gia_ManObjNum(p) );
2482 pNew->pName = Abc_UtilStrsav( p->pName );
2483 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
2484 Gia_ManConst0(p)->Value = 0;
2485 for ( i = 0; i < Gia_ManPiNum(p) - nPpis - nExtra; i++ ) // regular PIs
2486 Gia_ManCi(p, i)->Value = Gia_ManAppendCi( pNew );
2487 for ( i = Gia_ManPiNum(p) - nExtra; i < Gia_ManPiNum(p); i++ ) // extra PIs due to DC values
2488 Gia_ManCi(p, i)->Value = Gia_ManAppendCi( pNew );
2489 for ( i = Gia_ManPiNum(p) - nPpis - nExtra; i < Gia_ManPiNum(p) - nExtra; i++ ) // pseudo-PIs
2490 Gia_ManCi(p, i)->Value = Gia_ManAppendCi( pNew );
2491 for ( i = Gia_ManPiNum(p); i < Gia_ManCiNum(p); i++ ) // flop outputs
2492 Gia_ManCi(p, i)->Value = Gia_ManAppendCi( pNew );
2493 assert( Gia_ManCiNum(pNew) == Gia_ManCiNum(p) );
2494 Gia_ManForEachAnd( p, pObj, i )
2495 pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
2496 Gia_ManForEachCo( p, pObj, i )
2497 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
2498 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
2499 return pNew;
2500 }
2501
2502 /**Function*************************************************************
2503
2504 Synopsis [Duplicates AIG in the DFS order.]
2505
2506 Description []
2507
2508 SideEffects []
2509
2510 SeeAlso []
2511
2512 ***********************************************************************/
Gia_ManDupDfsClasses(Gia_Man_t * p)2513 Gia_Man_t * Gia_ManDupDfsClasses( Gia_Man_t * p )
2514 {
2515 Gia_Man_t * pNew, * pTemp;
2516 Gia_Obj_t * pObj;
2517 int i;
2518 assert( p->pReprsOld != NULL );
2519 Gia_ManFillValue( p );
2520 pNew = Gia_ManStart( Gia_ManObjNum(p) );
2521 pNew->pName = Abc_UtilStrsav( p->pName );
2522 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
2523 Gia_ManConst0(p)->Value = 0;
2524 Gia_ManForEachCi( p, pObj, i )
2525 pObj->Value = Gia_ManAppendCi(pNew);
2526 Gia_ManHashAlloc( pNew );
2527 Gia_ManForEachCo( p, pObj, i )
2528 Gia_ManDupDfs_rec( pNew, p, pObj );
2529 Gia_ManHashStop( pNew );
2530 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
2531 pNew = Gia_ManCleanup( pTemp = pNew );
2532 Gia_ManStop( pTemp );
2533 return pNew;
2534 }
2535
2536 /**Function*************************************************************
2537
2538 Synopsis [Detect topmost gate.]
2539
2540 Description []
2541
2542 SideEffects []
2543
2544 SeeAlso []
2545
2546 ***********************************************************************/
Gia_ManDupTopAnd_iter(Gia_Man_t * p,int fVerbose)2547 Gia_Man_t * Gia_ManDupTopAnd_iter( Gia_Man_t * p, int fVerbose )
2548 {
2549 Gia_Man_t * pNew;
2550 Gia_Obj_t * pObj;
2551 Vec_Int_t * vFront, * vLeaves;
2552 int i, iLit, iObjId, nCiLits, * pCi2Lit;
2553 char * pVar2Val;
2554 // collect the frontier
2555 vFront = Vec_IntAlloc( 1000 );
2556 vLeaves = Vec_IntAlloc( 1000 );
2557 Gia_ManForEachCo( p, pObj, i )
2558 {
2559 if ( Gia_ObjIsConst0( Gia_ObjFanin0(pObj) ) )
2560 continue;
2561 if ( Gia_ObjFaninC0(pObj) )
2562 Vec_IntPush( vLeaves, Gia_ObjFaninLit0p(p, pObj) );
2563 else
2564 Vec_IntPush( vFront, Gia_ObjFaninId0p(p, pObj) );
2565 }
2566 if ( Vec_IntSize(vFront) == 0 )
2567 {
2568 if ( fVerbose )
2569 printf( "The AIG cannot be decomposed using AND-decomposition.\n" );
2570 Vec_IntFree( vFront );
2571 Vec_IntFree( vLeaves );
2572 return Gia_ManDupNormalize( p, 0 );
2573 }
2574 // expand the frontier
2575 Gia_ManForEachObjVec( vFront, p, pObj, i )
2576 {
2577 if ( Gia_ObjIsCi(pObj) )
2578 {
2579 Vec_IntPush( vLeaves, Abc_Var2Lit( Gia_ObjId(p, pObj), 0 ) );
2580 continue;
2581 }
2582 assert( Gia_ObjIsAnd(pObj) );
2583 if ( Gia_ObjFaninC0(pObj) )
2584 Vec_IntPush( vLeaves, Gia_ObjFaninLit0p(p, pObj) );
2585 else
2586 Vec_IntPush( vFront, Gia_ObjFaninId0p(p, pObj) );
2587 if ( Gia_ObjFaninC1(pObj) )
2588 Vec_IntPush( vLeaves, Gia_ObjFaninLit1p(p, pObj) );
2589 else
2590 Vec_IntPush( vFront, Gia_ObjFaninId1p(p, pObj) );
2591 }
2592 Vec_IntFree( vFront );
2593 // sort the literals
2594 nCiLits = 0;
2595 pCi2Lit = ABC_FALLOC( int, Gia_ManObjNum(p) );
2596 pVar2Val = ABC_FALLOC( char, Gia_ManObjNum(p) );
2597 Vec_IntForEachEntry( vLeaves, iLit, i )
2598 {
2599 iObjId = Abc_Lit2Var(iLit);
2600 pObj = Gia_ManObj(p, iObjId);
2601 if ( Gia_ObjIsCi(pObj) )
2602 {
2603 pCi2Lit[Gia_ObjCioId(pObj)] = !Abc_LitIsCompl(iLit);
2604 nCiLits++;
2605 }
2606 if ( pVar2Val[iObjId] != 0 && pVar2Val[iObjId] != 1 )
2607 pVar2Val[iObjId] = Abc_LitIsCompl(iLit);
2608 else if ( pVar2Val[iObjId] != Abc_LitIsCompl(iLit) )
2609 break;
2610 }
2611 if ( i < Vec_IntSize(vLeaves) )
2612 {
2613 printf( "Problem is trivially UNSAT.\n" );
2614 ABC_FREE( pCi2Lit );
2615 ABC_FREE( pVar2Val );
2616 Vec_IntFree( vLeaves );
2617 return Gia_ManDupNormalize( p, 0 );
2618 }
2619 // create array of input literals
2620 Vec_IntClear( vLeaves );
2621 Gia_ManForEachObj( p, pObj, i )
2622 if ( !Gia_ObjIsCi(pObj) && (pVar2Val[i] == 0 || pVar2Val[i] == 1) )
2623 Vec_IntPush( vLeaves, Abc_Var2Lit(i, pVar2Val[i]) );
2624 if ( fVerbose )
2625 printf( "Detected %6d AND leaves and %6d CI leaves.\n", Vec_IntSize(vLeaves), nCiLits );
2626 // create the input map
2627 if ( nCiLits == 0 )
2628 pNew = Gia_ManDupDfsLitArray( p, vLeaves );
2629 else
2630 pNew = Gia_ManDupDfsCiMap( p, pCi2Lit, vLeaves );
2631 ABC_FREE( pCi2Lit );
2632 ABC_FREE( pVar2Val );
2633 Vec_IntFree( vLeaves );
2634 return pNew;
2635 }
2636
2637 /**Function*************************************************************
2638
2639 Synopsis [Detect topmost gate.]
2640
2641 Description []
2642
2643 SideEffects []
2644
2645 SeeAlso []
2646
2647 ***********************************************************************/
Gia_ManDupTopAnd(Gia_Man_t * p,int fVerbose)2648 Gia_Man_t * Gia_ManDupTopAnd( Gia_Man_t * p, int fVerbose )
2649 {
2650 Gia_Man_t * pNew, * pTemp;
2651 int fContinue, iIter = 0;
2652 pNew = Gia_ManDupNormalize( p, 0 );
2653 for ( fContinue = 1; fContinue; )
2654 {
2655 pNew = Gia_ManDupTopAnd_iter( pTemp = pNew, fVerbose );
2656 if ( Gia_ManCoNum(pNew) == Gia_ManCoNum(pTemp) && Gia_ManAndNum(pNew) == Gia_ManAndNum(pTemp) )
2657 fContinue = 0;
2658 Gia_ManStop( pTemp );
2659 if ( fVerbose )
2660 {
2661 printf( "Iter %2d : ", ++iIter );
2662 Gia_ManPrintStatsShort( pNew );
2663 }
2664 }
2665 return pNew;
2666 }
2667
2668
2669 /**Function*************************************************************
2670
2671 Synopsis [Duplicates the AIG in the DFS order.]
2672
2673 Description []
2674
2675 SideEffects []
2676
2677 SeeAlso []
2678
2679 ***********************************************************************/
Gia_ManMiter_rec(Gia_Man_t * pNew,Gia_Man_t * p,Gia_Obj_t * pObj)2680 int Gia_ManMiter_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
2681 {
2682 if ( ~pObj->Value )
2683 return pObj->Value;
2684 assert( Gia_ObjIsAnd(pObj) );
2685 Gia_ManMiter_rec( pNew, p, Gia_ObjFanin0(pObj) );
2686 Gia_ManMiter_rec( pNew, p, Gia_ObjFanin1(pObj) );
2687 return pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
2688 }
2689
2690 /**Function*************************************************************
2691
2692 Synopsis [Creates miter of two designs.]
2693
2694 Description []
2695
2696 SideEffects []
2697
2698 SeeAlso []
2699
2700 ***********************************************************************/
Gia_ManMiter(Gia_Man_t * p0,Gia_Man_t * p1,int nInsDup,int fDualOut,int fSeq,int fImplic,int fVerbose)2701 Gia_Man_t * Gia_ManMiter( Gia_Man_t * p0, Gia_Man_t * p1, int nInsDup, int fDualOut, int fSeq, int fImplic, int fVerbose )
2702 {
2703 Gia_Man_t * pNew, * pTemp;
2704 Gia_Obj_t * pObj;
2705 int i, iLit;
2706 if ( fSeq )
2707 {
2708 if ( Gia_ManPiNum(p0) != Gia_ManPiNum(p1) )
2709 {
2710 printf( "Gia_ManMiter(): Designs have different number of PIs.\n" );
2711 return NULL;
2712 }
2713 if ( Gia_ManPoNum(p0) != Gia_ManPoNum(p1) )
2714 {
2715 printf( "Gia_ManMiter(): Designs have different number of POs.\n" );
2716 return NULL;
2717 }
2718 if ( Gia_ManRegNum(p0) == 0 || Gia_ManRegNum(p1) == 0 )
2719 {
2720 printf( "Gia_ManMiter(): At least one of the designs has no registers.\n" );
2721 return NULL;
2722 }
2723 }
2724 else
2725 {
2726 if ( Gia_ManCiNum(p0) != Gia_ManCiNum(p1) )
2727 {
2728 printf( "Gia_ManMiter(): Designs have different number of CIs.\n" );
2729 return NULL;
2730 }
2731 if ( Gia_ManCoNum(p0) != Gia_ManCoNum(p1) )
2732 {
2733 printf( "Gia_ManMiter(): Designs have different number of COs.\n" );
2734 return NULL;
2735 }
2736 }
2737 // start the manager
2738 pNew = Gia_ManStart( Gia_ManObjNum(p0) + Gia_ManObjNum(p1) );
2739 pNew->pName = Abc_UtilStrsav( "miter" );
2740 // map combinational inputs
2741 Gia_ManFillValue( p0 );
2742 Gia_ManFillValue( p1 );
2743 Gia_ManConst0(p0)->Value = 0;
2744 Gia_ManConst0(p1)->Value = 0;
2745 // map internal nodes and outputs
2746 Gia_ManHashAlloc( pNew );
2747 if ( fSeq )
2748 {
2749 // create primary inputs
2750 Gia_ManForEachPi( p0, pObj, i )
2751 pObj->Value = Gia_ManAppendCi( pNew );
2752 Gia_ManForEachPi( p1, pObj, i )
2753 if ( i < Gia_ManPiNum(p1) - nInsDup )
2754 pObj->Value = Gia_ObjToLit( pNew, Gia_ManPi(pNew, i) );
2755 else
2756 pObj->Value = Gia_ManAppendCi( pNew );
2757 // create latch outputs
2758 Gia_ManForEachRo( p0, pObj, i )
2759 pObj->Value = Gia_ManAppendCi( pNew );
2760 Gia_ManForEachRo( p1, pObj, i )
2761 pObj->Value = Gia_ManAppendCi( pNew );
2762 // create primary outputs
2763 Gia_ManForEachPo( p0, pObj, i )
2764 {
2765 Gia_ManMiter_rec( pNew, p0, Gia_ObjFanin0(pObj) );
2766 Gia_ManMiter_rec( pNew, p1, Gia_ObjFanin0(Gia_ManPo(p1,i)) );
2767 if ( fDualOut )
2768 {
2769 Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
2770 Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(Gia_ManPo(p1,i)) );
2771 }
2772 else if ( fImplic )
2773 {
2774 iLit = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Abc_LitNot(Gia_ObjFanin0Copy(Gia_ManPo(p1,i))) );
2775 Gia_ManAppendCo( pNew, iLit );
2776 }
2777 else
2778 {
2779 iLit = Gia_ManHashXor( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin0Copy(Gia_ManPo(p1,i)) );
2780 Gia_ManAppendCo( pNew, iLit );
2781 }
2782 }
2783 // create register inputs
2784 Gia_ManForEachRi( p0, pObj, i )
2785 {
2786 Gia_ManMiter_rec( pNew, p0, Gia_ObjFanin0(pObj) );
2787 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
2788 }
2789 Gia_ManForEachRi( p1, pObj, i )
2790 {
2791 Gia_ManMiter_rec( pNew, p1, Gia_ObjFanin0(pObj) );
2792 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
2793 }
2794 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p0) + Gia_ManRegNum(p1) );
2795 }
2796 else
2797 {
2798 // create combinational inputs
2799 Gia_ManForEachCi( p0, pObj, i )
2800 pObj->Value = Gia_ManAppendCi( pNew );
2801 Gia_ManForEachCi( p1, pObj, i )
2802 if ( i < Gia_ManCiNum(p1) - nInsDup )
2803 pObj->Value = Gia_ObjToLit( pNew, Gia_ManCi(pNew, i) );
2804 else
2805 pObj->Value = Gia_ManAppendCi( pNew );
2806 // create combinational outputs
2807 Gia_ManForEachCo( p0, pObj, i )
2808 {
2809 Gia_ManMiter_rec( pNew, p0, Gia_ObjFanin0(pObj) );
2810 Gia_ManMiter_rec( pNew, p1, Gia_ObjFanin0(Gia_ManCo(p1,i)) );
2811 if ( fDualOut )
2812 {
2813 Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
2814 Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(Gia_ManCo(p1,i)) );
2815 }
2816 else if ( fImplic )
2817 {
2818 iLit = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Abc_LitNot(Gia_ObjFanin0Copy(Gia_ManPo(p1,i))) );
2819 Gia_ManAppendCo( pNew, iLit );
2820 }
2821 else
2822 {
2823 iLit = Gia_ManHashXor( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin0Copy(Gia_ManCo(p1,i)) );
2824 Gia_ManAppendCo( pNew, iLit );
2825 }
2826 }
2827 }
2828 Gia_ManHashStop( pNew );
2829 pNew = Gia_ManCleanup( pTemp = pNew );
2830 Gia_ManStop( pTemp );
2831
2832 pNew = Gia_ManDupNormalize( pTemp = pNew, 0 );
2833 Gia_ManStop( pTemp );
2834 return pNew;
2835 }
2836
2837 /**Function*************************************************************
2838
2839 Synopsis [Computes the AND of all POs.]
2840
2841 Description []
2842
2843 SideEffects []
2844
2845 SeeAlso []
2846
2847 ***********************************************************************/
Gia_ManDupAndOr(Gia_Man_t * p,int nOuts,int fUseOr,int fCompl)2848 Gia_Man_t * Gia_ManDupAndOr( Gia_Man_t * p, int nOuts, int fUseOr, int fCompl )
2849 {
2850 Gia_Man_t * pNew, * pTemp;
2851 Gia_Obj_t * pObj;
2852 int i, iResult;
2853 assert( Gia_ManRegNum(p) == 0 );
2854 pNew = Gia_ManStart( Gia_ManObjNum(p) );
2855 pNew->pName = Abc_UtilStrsav( p->pName );
2856 Gia_ManConst0(p)->Value = 0;
2857 Gia_ManHashAlloc( pNew );
2858 Gia_ManForEachPi( p, pObj, i )
2859 pObj->Value = Gia_ManAppendCi( pNew );
2860 Gia_ManForEachAnd( p, pObj, i )
2861 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
2862 if ( fUseOr ) // construct OR of all POs
2863 {
2864 iResult = 0;
2865 Gia_ManForEachPo( p, pObj, i )
2866 iResult = Gia_ManHashOr( pNew, iResult, Gia_ObjFanin0Copy(pObj) );
2867 }
2868 else // construct AND of all POs
2869 {
2870 iResult = 1;
2871 Gia_ManForEachPo( p, pObj, i )
2872 iResult = Gia_ManHashAnd( pNew, iResult, Gia_ObjFanin0Copy(pObj) );
2873 }
2874 iResult = Abc_LitNotCond( iResult, (int)(fCompl > 0) );
2875 // Gia_ManForEachPo( p, pObj, i )
2876 // pObj->Value = Gia_ManAppendCo( pNew, iResult );
2877 for ( i = 0; i < nOuts; i++ )
2878 Gia_ManAppendCo( pNew, iResult );
2879 Gia_ManHashStop( pNew );
2880 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
2881 pNew = Gia_ManCleanup( pTemp = pNew );
2882 Gia_ManStop( pTemp );
2883 return pNew;
2884 }
2885
2886 /**Function*************************************************************
2887
2888 Synopsis [Transforms output names.]
2889
2890 Description []
2891
2892 SideEffects []
2893
2894 SeeAlso []
2895
2896 ***********************************************************************/
Gia_ManMiterNames(Vec_Ptr_t * p,int nOuts)2897 Vec_Ptr_t * Gia_ManMiterNames( Vec_Ptr_t * p, int nOuts )
2898 {
2899 char * pName1, * pName2, pBuffer[1000]; int i;
2900 Vec_Ptr_t * pNew = Vec_PtrAlloc( Vec_PtrSize(p) - nOuts/2 );
2901 assert( nOuts % 2 == 0 );
2902 assert( nOuts <= Vec_PtrSize(p) );
2903 Vec_PtrForEachEntryDouble( char *, char *, p, pName1, pName2, i )
2904 {
2905 if ( i == nOuts )
2906 break;
2907 sprintf( pBuffer, "%s_xor_%s", pName1, pName2 );
2908 Vec_PtrPush( pNew, Abc_UtilStrsav(pBuffer) );
2909 }
2910 Vec_PtrForEachEntryStart( char *, p, pName1, i, i )
2911 Vec_PtrPush( pNew, Abc_UtilStrsav(pName1) );
2912 return pNew;
2913 }
2914
2915 /**Function*************************************************************
2916
2917 Synopsis [Transforms the circuit into a regular miter.]
2918
2919 Description []
2920
2921 SideEffects []
2922
2923 SeeAlso []
2924
2925 ***********************************************************************/
Gia_ManTransformMiter(Gia_Man_t * p)2926 Gia_Man_t * Gia_ManTransformMiter( Gia_Man_t * p )
2927 {
2928 Gia_Man_t * pNew, * pTemp;
2929 Gia_Obj_t * pObj, * pObj2;
2930 int i, iLit;
2931 assert( (Gia_ManPoNum(p) & 1) == 0 );
2932 pNew = Gia_ManStart( Gia_ManObjNum(p) );
2933 pNew->pName = Abc_UtilStrsav( p->pName );
2934 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
2935 Gia_ManConst0(p)->Value = 0;
2936 Gia_ManHashAlloc( pNew );
2937 Gia_ManForEachCi( p, pObj, i )
2938 pObj->Value = Gia_ManAppendCi( pNew );
2939 Gia_ManForEachAnd( p, pObj, i )
2940 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
2941 Gia_ManForEachPo( p, pObj, i )
2942 {
2943 pObj2 = Gia_ManPo( p, ++i );
2944 iLit = Gia_ManHashXor( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin0Copy(pObj2) );
2945 Gia_ManAppendCo( pNew, iLit );
2946 }
2947 Gia_ManForEachRi( p, pObj, i )
2948 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
2949 Gia_ManHashStop( pNew );
2950 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
2951 pNew = Gia_ManCleanup( pTemp = pNew );
2952 Gia_ManStop( pTemp );
2953 if ( p->vNamesIn )
2954 pNew->vNamesIn = Vec_PtrDupStr(p->vNamesIn);
2955 if ( p->vNamesOut )
2956 pNew->vNamesOut = Gia_ManMiterNames(p->vNamesOut, Gia_ManPoNum(p));
2957 return pNew;
2958 }
Gia_ManTransformMiter2(Gia_Man_t * p)2959 Gia_Man_t * Gia_ManTransformMiter2( Gia_Man_t * p )
2960 {
2961 Gia_Man_t * pNew, * pTemp;
2962 Gia_Obj_t * pObj, * pObj2;
2963 int i, iLit, nPart = Gia_ManPoNum(p)/2;
2964 assert( (Gia_ManPoNum(p) & 1) == 0 );
2965 pNew = Gia_ManStart( Gia_ManObjNum(p) );
2966 pNew->pName = Abc_UtilStrsav( p->pName );
2967 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
2968 Gia_ManConst0(p)->Value = 0;
2969 Gia_ManHashAlloc( pNew );
2970 Gia_ManForEachCi( p, pObj, i )
2971 pObj->Value = Gia_ManAppendCi( pNew );
2972 Gia_ManForEachAnd( p, pObj, i )
2973 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
2974 Gia_ManForEachPo( p, pObj, i )
2975 {
2976 if ( i == nPart )
2977 break;
2978 pObj2 = Gia_ManPo( p, nPart + i );
2979 iLit = Gia_ManHashXor( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin0Copy(pObj2) );
2980 Gia_ManAppendCo( pNew, iLit );
2981 }
2982 Gia_ManForEachRi( p, pObj, i )
2983 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
2984 Gia_ManHashStop( pNew );
2985 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
2986 pNew = Gia_ManCleanup( pTemp = pNew );
2987 Gia_ManStop( pTemp );
2988 return pNew;
2989 }
Gia_ManTransformToDual(Gia_Man_t * p)2990 Gia_Man_t * Gia_ManTransformToDual( Gia_Man_t * p )
2991 {
2992 Gia_Man_t * pNew;
2993 Gia_Obj_t * pObj;
2994 int i;
2995 pNew = Gia_ManStart( Gia_ManObjNum(p) );
2996 pNew->pName = Abc_UtilStrsav( p->pName );
2997 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
2998 Gia_ManConst0(p)->Value = 0;
2999 Gia_ManHashAlloc( pNew );
3000 Gia_ManForEachCi( p, pObj, i )
3001 pObj->Value = Gia_ManAppendCi( pNew );
3002 Gia_ManForEachAnd( p, pObj, i )
3003 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
3004 Gia_ManForEachPo( p, pObj, i )
3005 {
3006 Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
3007 Gia_ManAppendCo( pNew, 0 );
3008 }
3009 Gia_ManForEachRi( p, pObj, i )
3010 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
3011 Gia_ManHashStop( pNew );
3012 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
3013 return pNew;
3014 }
Gia_ManTransformTwoWord2DualOutput(Gia_Man_t * p)3015 Gia_Man_t * Gia_ManTransformTwoWord2DualOutput( Gia_Man_t * p )
3016 {
3017 Gia_Man_t * pNew, * pTemp;
3018 Gia_Obj_t * pObj, * pObj2;
3019 int i, nPart = Gia_ManPoNum(p)/2;
3020 assert( (Gia_ManPoNum(p) & 1) == 0 );
3021 pNew = Gia_ManStart( Gia_ManObjNum(p) );
3022 pNew->pName = Abc_UtilStrsav( p->pName );
3023 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
3024 Gia_ManConst0(p)->Value = 0;
3025 Gia_ManHashAlloc( pNew );
3026 Gia_ManForEachCi( p, pObj, i )
3027 pObj->Value = Gia_ManAppendCi( pNew );
3028 Gia_ManForEachAnd( p, pObj, i )
3029 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
3030 Gia_ManForEachPo( p, pObj, i )
3031 {
3032 if ( i == nPart )
3033 break;
3034 pObj2 = Gia_ManPo( p, nPart + i );
3035 Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
3036 Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj2) );
3037 }
3038 Gia_ManForEachRi( p, pObj, i )
3039 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
3040 Gia_ManHashStop( pNew );
3041 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
3042 pNew = Gia_ManCleanup( pTemp = pNew );
3043 Gia_ManStop( pTemp );
3044 return pNew;
3045 }
3046
Gia_ManCollectOneSide_rec(Gia_Man_t * p,Gia_Obj_t * pObj,Vec_Int_t * vNodes)3047 void Gia_ManCollectOneSide_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vNodes )
3048 {
3049 if ( Gia_ObjIsTravIdCurrent(p, pObj) )
3050 return;
3051 Gia_ObjSetTravIdCurrent(p, pObj);
3052 if ( !Gia_ObjIsAnd(pObj) )
3053 return;
3054 Gia_ManCollectOneSide_rec( p, Gia_ObjFanin0(pObj), vNodes );
3055 Gia_ManCollectOneSide_rec( p, Gia_ObjFanin1(pObj), vNodes );
3056 Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
3057 }
Gia_ManCollectOneSide(Gia_Man_t * p,int iSide)3058 Vec_Int_t * Gia_ManCollectOneSide( Gia_Man_t * p, int iSide )
3059 {
3060 Gia_Obj_t * pObj; int i;
3061 Vec_Int_t * vNodes = Vec_IntAlloc( Gia_ManAndNum(p) );
3062 Gia_ManIncrementTravId( p );
3063 Gia_ManForEachPo( p, pObj, i )
3064 if ( (i & 1) == iSide )
3065 Gia_ManCollectOneSide_rec( p, Gia_ObjFanin0(pObj), vNodes );
3066 return vNodes;
3067 }
Gia_ManTransformDualOutput(Gia_Man_t * p)3068 Gia_Man_t * Gia_ManTransformDualOutput( Gia_Man_t * p )
3069 {
3070 Vec_Int_t * vNodes0 = Gia_ManCollectOneSide( p, 0 );
3071 Vec_Int_t * vNodes1 = Gia_ManCollectOneSide( p, 1 );
3072 Gia_Man_t * pNew, * pTemp;
3073 Gia_Obj_t * pObj, * pObj2;
3074 int i, fSwap = 0;
3075 assert( Gia_ManRegNum(p) == 0 );
3076 assert( (Gia_ManPoNum(p) & 1) == 0 );
3077 if ( Vec_IntSize(vNodes0) > Vec_IntSize(vNodes1) )
3078 {
3079 ABC_SWAP( Vec_Int_t *, vNodes0, vNodes1 );
3080 fSwap = 1;
3081 }
3082 assert( Vec_IntSize(vNodes0) <= Vec_IntSize(vNodes1) );
3083 pNew = Gia_ManStart( Gia_ManObjNum(p) );
3084 pNew->pName = Abc_UtilStrsav( p->pName );
3085 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
3086 Gia_ManConst0(p)->Value = 0;
3087 Gia_ManHashAlloc( pNew );
3088 Gia_ManForEachCi( p, pObj, i )
3089 pObj->Value = Gia_ManAppendCi( pNew );
3090 Gia_ManForEachObjVec( vNodes0, p, pObj, i )
3091 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
3092 Gia_ManForEachObjVec( vNodes1, p, pObj, i )
3093 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
3094 Vec_IntFree( vNodes0 );
3095 Vec_IntFree( vNodes1 );
3096 Gia_ManForEachPo( p, pObj, i )
3097 {
3098 pObj2 = Gia_ManPo( p, i^fSwap );
3099 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj2) );
3100 }
3101 Gia_ManHashStop( pNew );
3102 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
3103 pNew = Gia_ManCleanup( pTemp = pNew );
3104 Gia_ManStop( pTemp );
3105 return pNew;
3106 }
3107
3108 /**Function*************************************************************
3109
3110 Synopsis [Performs 'zero' and 'undc' operation.]
3111
3112 Description [The init string specifies 0/1/X for each flop.]
3113
3114 SideEffects []
3115
3116 SeeAlso []
3117
3118 ***********************************************************************/
Gia_ManDupZeroUndc(Gia_Man_t * p,char * pInit,int nNewPis,int fGiaSimple,int fVerbose)3119 Gia_Man_t * Gia_ManDupZeroUndc( Gia_Man_t * p, char * pInit, int nNewPis, int fGiaSimple, int fVerbose )
3120 {
3121 Gia_Man_t * pNew;
3122 Gia_Obj_t * pObj;
3123 int CountPis = Gia_ManPiNum(p), * pPiLits;
3124 int i, iResetFlop = -1, Count1 = 0;
3125 //printf( "Using %s\n", pInit );
3126 // map X-valued flops into new PIs
3127 assert( (int)strlen(pInit) == Gia_ManRegNum(p) );
3128 pPiLits = ABC_FALLOC( int, Gia_ManRegNum(p) );
3129 for ( i = 0; i < Gia_ManRegNum(p); i++ )
3130 if ( pInit[i] == 'x' || pInit[i] == 'X' )
3131 pPiLits[i] = CountPis++;
3132 // create new manager
3133 pNew = Gia_ManStart( Gia_ManObjNum(p) );
3134 pNew->pName = Abc_UtilStrsav( p->pName );
3135 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
3136 pNew->fGiaSimple = fGiaSimple;
3137 Gia_ManConst0(p)->Value = 0;
3138 // create primary inputs
3139 Gia_ManForEachPi( p, pObj, i )
3140 pObj->Value = Gia_ManAppendCi( pNew );
3141 // create additional primary inputs
3142 for ( i = Gia_ManPiNum(p); i < CountPis; i++ )
3143 Gia_ManAppendCi( pNew );
3144 // create additional primary inputs
3145 for ( i = 0; i < nNewPis; i++ )
3146 Gia_ManAppendCi( pNew );
3147 // create flop outputs
3148 Gia_ManForEachRo( p, pObj, i )
3149 pObj->Value = Gia_ManAppendCi( pNew );
3150 // create reset flop output
3151 if ( CountPis > Gia_ManPiNum(p) )
3152 iResetFlop = Gia_ManAppendCi( pNew );
3153 // update flop outputs
3154 Gia_ManMarkFanoutDrivers( p );
3155 Gia_ManForEachRo( p, pObj, i )
3156 {
3157 if ( pInit[i] == '1' )
3158 pObj->Value = Abc_LitNot(pObj->Value), Count1++;
3159 else if ( pInit[i] == 'x' || pInit[i] == 'X' )
3160 {
3161 if ( pObj->fMark0 ) // only add MUX if the flop has fanout
3162 pObj->Value = Gia_ManAppendMux( pNew, iResetFlop, pObj->Value, Gia_Obj2Lit(pNew, Gia_ManPi(pNew, pPiLits[i])) );
3163 }
3164 else if ( pInit[i] != '0' )
3165 assert( 0 );
3166 }
3167 Gia_ManCleanMark0( p );
3168 ABC_FREE( pPiLits );
3169 // build internal nodes
3170 Gia_ManForEachAnd( p, pObj, i )
3171 pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
3172 // create POs
3173 Gia_ManForEachPo( p, pObj, i )
3174 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
3175 // create flop inputs
3176 Gia_ManForEachRi( p, pObj, i )
3177 if ( pInit[i] == '1' )
3178 pObj->Value = Gia_ManAppendCo( pNew, Abc_LitNot(Gia_ObjFanin0Copy(pObj)) );
3179 else
3180 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
3181 // create reset flop input
3182 if ( CountPis > Gia_ManPiNum(p) )
3183 Gia_ManAppendCo( pNew, 1 );
3184 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) + (int)(CountPis > Gia_ManPiNum(p)) );
3185 if ( fVerbose )
3186 printf( "Converted %d 1-valued FFs and %d DC-valued FFs.\n", Count1, CountPis-Gia_ManPiNum(p) );
3187 return pNew;
3188 }
3189
3190 /**Function*************************************************************
3191
3192 Synopsis [Creates miter of two designs.]
3193
3194 Description []
3195
3196 SideEffects []
3197
3198 SeeAlso []
3199
3200 ***********************************************************************/
Gia_ManMiter2(Gia_Man_t * pStart,char * pInit,int fVerbose)3201 Gia_Man_t * Gia_ManMiter2( Gia_Man_t * pStart, char * pInit, int fVerbose )
3202 {
3203 Vec_Int_t * vCiValues, * vCoValues0, * vCoValues1;
3204 Gia_Man_t * pNew, * pUndc, * pTemp;
3205 Gia_Obj_t * pObj;
3206 char * pInitNew;
3207 int i, k;
3208 // check PI values
3209 for ( i = 0; i < Gia_ManPiNum(pStart); i++ )
3210 assert( pInit[i] == 'x' || pInit[i] == 'X' );
3211 // normalize the manager
3212 pUndc = Gia_ManDupZeroUndc( pStart, pInit + Gia_ManPiNum(pStart), 0, 0, fVerbose );
3213 // create new init string
3214 pInitNew = ABC_ALLOC( char, Gia_ManPiNum(pUndc)+1 );
3215 for ( i = 0; i < Gia_ManPiNum(pStart); i++ )
3216 pInitNew[i] = pInit[i];
3217 for ( i = k = Gia_ManPiNum(pStart); i < Gia_ManCiNum(pStart); i++ )
3218 if ( pInit[i] == 'x' || pInit[i] == 'X' )
3219 pInitNew[k++] = pInit[i];
3220 pInitNew[k] = 0;
3221 assert( k == Gia_ManPiNum(pUndc) );
3222 // derive miter
3223 pNew = Gia_ManStart( Gia_ManObjNum(pUndc) );
3224 pNew->pName = Abc_UtilStrsav( pUndc->pName );
3225 pNew->pSpec = Abc_UtilStrsav( pUndc->pSpec );
3226 Gia_ManConst0(pUndc)->Value = 0;
3227 Gia_ManHashAlloc( pNew );
3228 // add PIs of the first side
3229 Gia_ManForEachPi( pUndc, pObj, i )
3230 pObj->Value = Gia_ManAppendCi( pNew );
3231 // add PIs of the second side
3232 vCiValues = Vec_IntAlloc( Gia_ManPiNum(pUndc) );
3233 Gia_ManForEachPi( pUndc, pObj, i )
3234 if ( pInitNew[i] == 'x' )
3235 Vec_IntPush( vCiValues, Gia_Obj2Lit( pNew, Gia_ManPi(pNew, i) ) );
3236 else if ( pInitNew[i] == 'X' )
3237 Vec_IntPush( vCiValues, Gia_ManAppendCi( pNew ) );
3238 else assert( 0 );
3239 // build flops and internal nodes
3240 Gia_ManForEachRo( pUndc, pObj, i )
3241 pObj->Value = Gia_ManAppendCi( pNew );
3242 Gia_ManForEachAnd( pUndc, pObj, i )
3243 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
3244 // collect CO values
3245 vCoValues0 = Vec_IntAlloc( Gia_ManPoNum(pUndc) );
3246 Gia_ManForEachCo( pUndc, pObj, i )
3247 Vec_IntPush( vCoValues0, Gia_ObjFanin0Copy(pObj) );
3248 // build the other side
3249 Gia_ManForEachPi( pUndc, pObj, i )
3250 pObj->Value = Vec_IntEntry( vCiValues, i );
3251 Gia_ManForEachRo( pUndc, pObj, i )
3252 pObj->Value = Gia_ManAppendCi( pNew );
3253 Gia_ManForEachAnd( pUndc, pObj, i )
3254 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
3255 // collect CO values
3256 vCoValues1 = Vec_IntAlloc( Gia_ManPoNum(pUndc) );
3257 Gia_ManForEachCo( pUndc, pObj, i )
3258 Vec_IntPush( vCoValues1, Gia_ObjFanin0Copy(pObj) );
3259 // create POs
3260 Gia_ManForEachPo( pUndc, pObj, i )
3261 pObj->Value = Gia_ManAppendCo( pNew, Gia_ManHashXor( pNew, Vec_IntEntry(vCoValues0, i), Vec_IntEntry(vCoValues1, i) ) );
3262 // create flop inputs
3263 Gia_ManForEachRi( pUndc, pObj, i )
3264 pObj->Value = Gia_ManAppendCo( pNew, Vec_IntEntry(vCoValues0, Gia_ManPoNum(pUndc)+i) );
3265 Gia_ManForEachRi( pUndc, pObj, i )
3266 pObj->Value = Gia_ManAppendCo( pNew, Vec_IntEntry(vCoValues1, Gia_ManPoNum(pUndc)+i) );
3267 Vec_IntFree( vCoValues0 );
3268 Vec_IntFree( vCoValues1 );
3269 Vec_IntFree( vCiValues );
3270 ABC_FREE( pInitNew );
3271 // cleanup
3272 Gia_ManHashStop( pNew );
3273 Gia_ManSetRegNum( pNew, 2*Gia_ManRegNum(pUndc) );
3274 Gia_ManStop( pUndc );
3275 pNew = Gia_ManCleanup( pTemp = pNew );
3276 Gia_ManStop( pTemp );
3277 return pNew;
3278 }
3279
3280 /**Function*************************************************************
3281
3282 Synopsis [Duplicates the AIG in the DFS order.]
3283
3284 Description []
3285
3286 SideEffects []
3287
3288 SeeAlso []
3289
3290 ***********************************************************************/
Gia_ManChoiceMiter_rec(Gia_Man_t * pNew,Gia_Man_t * p,Gia_Obj_t * pObj)3291 int Gia_ManChoiceMiter_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
3292 {
3293 if ( ~pObj->Value )
3294 return pObj->Value;
3295 Gia_ManChoiceMiter_rec( pNew, p, Gia_ObjFanin0(pObj) );
3296 if ( Gia_ObjIsCo(pObj) )
3297 return pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
3298 Gia_ManChoiceMiter_rec( pNew, p, Gia_ObjFanin1(pObj) );
3299 return pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
3300 }
3301
3302 /**Function*************************************************************
3303
3304 Synopsis [Derives the miter of several AIGs for choice computation.]
3305
3306 Description []
3307
3308 SideEffects []
3309
3310 SeeAlso []
3311
3312 ***********************************************************************/
Gia_ManChoiceMiter(Vec_Ptr_t * vGias)3313 Gia_Man_t * Gia_ManChoiceMiter( Vec_Ptr_t * vGias )
3314 {
3315 Gia_Man_t * pNew, * pGia, * pGia0;
3316 int i, k, iNode, nNodes;
3317 // make sure they have equal parameters
3318 assert( Vec_PtrSize(vGias) > 0 );
3319 pGia0 = (Gia_Man_t *)Vec_PtrEntry( vGias, 0 );
3320 Vec_PtrForEachEntry( Gia_Man_t *, vGias, pGia, i )
3321 {
3322 assert( Gia_ManCiNum(pGia) == Gia_ManCiNum(pGia0) );
3323 assert( Gia_ManCoNum(pGia) == Gia_ManCoNum(pGia0) );
3324 assert( Gia_ManRegNum(pGia) == Gia_ManRegNum(pGia0) );
3325 Gia_ManFillValue( pGia );
3326 Gia_ManConst0(pGia)->Value = 0;
3327 }
3328 // start the new manager
3329 pNew = Gia_ManStart( Vec_PtrSize(vGias) * Gia_ManObjNum(pGia0) );
3330 pNew->pName = Abc_UtilStrsav( pGia0->pName );
3331 pNew->pSpec = Abc_UtilStrsav( pGia0->pSpec );
3332 // create new CIs and assign them to the old manager CIs
3333 for ( k = 0; k < Gia_ManCiNum(pGia0); k++ )
3334 {
3335 iNode = Gia_ManAppendCi(pNew);
3336 Vec_PtrForEachEntry( Gia_Man_t *, vGias, pGia, i )
3337 Gia_ManCi( pGia, k )->Value = iNode;
3338 }
3339 // create internal nodes
3340 Gia_ManHashAlloc( pNew );
3341 for ( k = 0; k < Gia_ManCoNum(pGia0); k++ )
3342 {
3343 Vec_PtrForEachEntry( Gia_Man_t *, vGias, pGia, i )
3344 Gia_ManChoiceMiter_rec( pNew, pGia, Gia_ManCo( pGia, k ) );
3345 }
3346 Gia_ManHashStop( pNew );
3347 // check the presence of dangling nodes
3348 nNodes = Gia_ManHasDangling( pNew );
3349 //assert( nNodes == 0 );
3350 // finalize
3351 Gia_ManSetRegNum( pNew, Gia_ManRegNum(pGia0) );
3352 return pNew;
3353 }
3354
3355 /**Function*************************************************************
3356
3357 Synopsis [Duplicates AIG while putting first PIs, then nodes, then POs.]
3358
3359 Description []
3360
3361 SideEffects []
3362
3363 SeeAlso []
3364
3365 ***********************************************************************/
Gia_ManDupWithConstraints(Gia_Man_t * p,Vec_Int_t * vPoTypes)3366 Gia_Man_t * Gia_ManDupWithConstraints( Gia_Man_t * p, Vec_Int_t * vPoTypes )
3367 {
3368 Gia_Man_t * pNew;
3369 Gia_Obj_t * pObj;
3370 int i, nConstr = 0;
3371 pNew = Gia_ManStart( Gia_ManObjNum(p) );
3372 pNew->pName = Abc_UtilStrsav( p->pName );
3373 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
3374 Gia_ManConst0(p)->Value = 0;
3375 Gia_ManForEachCi( p, pObj, i )
3376 pObj->Value = Gia_ManAppendCi(pNew);
3377 Gia_ManForEachAnd( p, pObj, i )
3378 pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
3379 Gia_ManForEachPo( p, pObj, i )
3380 if ( Vec_IntEntry(vPoTypes, i) == 0 ) // regular PO
3381 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
3382 Gia_ManForEachPo( p, pObj, i )
3383 if ( Vec_IntEntry(vPoTypes, i) == 1 ) // constraint (should be complemented!)
3384 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ^ 1 ), nConstr++;
3385 Gia_ManForEachRi( p, pObj, i )
3386 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
3387 // Gia_ManDupRemapEquiv( pNew, p );
3388 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
3389 pNew->nConstrs = nConstr;
3390 assert( Gia_ManIsNormalized(pNew) );
3391 return pNew;
3392 }
3393
3394 /**Function*************************************************************
3395
3396 Synopsis [Copy an AIG structure related to the selected POs.]
3397
3398 Description []
3399
3400 SideEffects []
3401
3402 SeeAlso []
3403
3404 ***********************************************************************/
Gia_ObjCompareByCioId(Gia_Obj_t ** pp1,Gia_Obj_t ** pp2)3405 int Gia_ObjCompareByCioId( Gia_Obj_t ** pp1, Gia_Obj_t ** pp2 )
3406 {
3407 Gia_Obj_t * pObj1 = *pp1;
3408 Gia_Obj_t * pObj2 = *pp2;
3409 return Gia_ObjCioId(pObj1) - Gia_ObjCioId(pObj2);
3410 }
Gia_ManDupCones_rec(Gia_Man_t * p,Gia_Obj_t * pObj,Vec_Ptr_t * vLeaves,Vec_Ptr_t * vNodes,Vec_Ptr_t * vRoots)3411 void Gia_ManDupCones_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes, Vec_Ptr_t * vRoots )
3412 {
3413 if ( Gia_ObjIsTravIdCurrent(p, pObj) )
3414 return;
3415 Gia_ObjSetTravIdCurrent(p, pObj);
3416 if ( Gia_ObjIsAnd(pObj) )
3417 {
3418 Gia_ManDupCones_rec( p, Gia_ObjFanin0(pObj), vLeaves, vNodes, vRoots );
3419 Gia_ManDupCones_rec( p, Gia_ObjFanin1(pObj), vLeaves, vNodes, vRoots );
3420 Vec_PtrPush( vNodes, pObj );
3421 }
3422 else if ( Gia_ObjIsCo(pObj) )
3423 Gia_ManDupCones_rec( p, Gia_ObjFanin0(pObj), vLeaves, vNodes, vRoots );
3424 else if ( Gia_ObjIsRo(p, pObj) )
3425 Vec_PtrPush( vRoots, Gia_ObjRoToRi(p, pObj) );
3426 else if ( Gia_ObjIsPi(p, pObj) )
3427 Vec_PtrPush( vLeaves, pObj );
3428 else assert( 0 );
3429 }
Gia_ManDupCones(Gia_Man_t * p,int * pPos,int nPos,int fTrimPis)3430 Gia_Man_t * Gia_ManDupCones( Gia_Man_t * p, int * pPos, int nPos, int fTrimPis )
3431 {
3432 Gia_Man_t * pNew;
3433 Vec_Ptr_t * vLeaves, * vNodes, * vRoots;
3434 Gia_Obj_t * pObj;
3435 int i;
3436
3437 // collect initial POs
3438 vLeaves = Vec_PtrAlloc( 100 );
3439 vNodes = Vec_PtrAlloc( 100 );
3440 vRoots = Vec_PtrAlloc( 100 );
3441 for ( i = 0; i < nPos; i++ )
3442 Vec_PtrPush( vRoots, Gia_ManPo(p, pPos[i]) );
3443
3444 // mark internal nodes
3445 Gia_ManIncrementTravId( p );
3446 Gia_ObjSetTravIdCurrent( p, Gia_ManConst0(p) );
3447 Vec_PtrForEachEntry( Gia_Obj_t *, vRoots, pObj, i )
3448 Gia_ManDupCones_rec( p, pObj, vLeaves, vNodes, vRoots );
3449 Vec_PtrSort( vLeaves, (int (*)(void))Gia_ObjCompareByCioId );
3450
3451 // start the new manager
3452 // Gia_ManFillValue( p );
3453 pNew = Gia_ManStart( (fTrimPis ? Vec_PtrSize(vLeaves) : Gia_ManCiNum(p)) + Vec_PtrSize(vNodes) + Vec_PtrSize(vRoots) + 1 );
3454 pNew->pName = Abc_UtilStrsav( p->pName );
3455 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
3456 // map the constant node
3457 Gia_ManConst0(p)->Value = 0;
3458 // create PIs
3459 if ( fTrimPis )
3460 {
3461 Vec_PtrForEachEntry( Gia_Obj_t *, vLeaves, pObj, i )
3462 pObj->Value = Gia_ManAppendCi( pNew );
3463 }
3464 else
3465 {
3466 Gia_ManForEachPi( p, pObj, i )
3467 pObj->Value = Gia_ManAppendCi( pNew );
3468 }
3469 // create LOs
3470 Vec_PtrForEachEntryStart( Gia_Obj_t *, vRoots, pObj, i, nPos )
3471 Gia_ObjRiToRo(p, pObj)->Value = Gia_ManAppendCi( pNew );
3472 // create internal nodes
3473 Vec_PtrForEachEntry( Gia_Obj_t *, vNodes, pObj, i )
3474 if ( Gia_ObjIsXor(pObj) )
3475 pObj->Value = Gia_ManAppendXor( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
3476 else
3477 pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
3478 // create COs
3479 Vec_PtrForEachEntry( Gia_Obj_t *, vRoots, pObj, i )
3480 Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
3481 // finalize
3482 Gia_ManSetRegNum( pNew, Vec_PtrSize(vRoots)-nPos );
3483 Vec_PtrFree( vLeaves );
3484 Vec_PtrFree( vNodes );
3485 Vec_PtrFree( vRoots );
3486 return pNew;
3487
3488 }
Gia_ManDupAndCones(Gia_Man_t * p,int * pAnds,int nAnds,int fTrimPis)3489 Gia_Man_t * Gia_ManDupAndCones( Gia_Man_t * p, int * pAnds, int nAnds, int fTrimPis )
3490 {
3491 Gia_Man_t * pNew;
3492 Vec_Ptr_t * vLeaves, * vNodes, * vRoots;
3493 Gia_Obj_t * pObj;
3494 int i;
3495
3496 // collect initial POs
3497 vLeaves = Vec_PtrAlloc( 100 );
3498 vNodes = Vec_PtrAlloc( 100 );
3499 vRoots = Vec_PtrAlloc( 100 );
3500 for ( i = 0; i < nAnds; i++ )
3501 // Vec_PtrPush( vRoots, Gia_ManPo(p, pPos[i]) );
3502 Vec_PtrPush( vRoots, Gia_ManObj(p, pAnds[i]) );
3503
3504 // mark internal nodes
3505 Gia_ManIncrementTravId( p );
3506 Gia_ObjSetTravIdCurrent( p, Gia_ManConst0(p) );
3507 Vec_PtrForEachEntry( Gia_Obj_t *, vRoots, pObj, i )
3508 Gia_ManDupCones_rec( p, pObj, vLeaves, vNodes, vRoots );
3509 Vec_PtrSort( vLeaves, (int (*)(void))Gia_ObjCompareByCioId );
3510
3511 // start the new manager
3512 // Gia_ManFillValue( p );
3513 pNew = Gia_ManStart( Vec_PtrSize(vLeaves) + Vec_PtrSize(vNodes) + Vec_PtrSize(vRoots) + 1);
3514 pNew->pName = Abc_UtilStrsav( p->pName );
3515 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
3516 // map the constant node
3517 Gia_ManConst0(p)->Value = 0;
3518 // create PIs
3519 if ( fTrimPis )
3520 {
3521 Vec_PtrForEachEntry( Gia_Obj_t *, vLeaves, pObj, i )
3522 pObj->Value = Gia_ManAppendCi( pNew );
3523 }
3524 else
3525 {
3526 Gia_ManForEachPi( p, pObj, i )
3527 pObj->Value = Gia_ManAppendCi( pNew );
3528 }
3529 // create LOs
3530 // Vec_PtrForEachEntryStart( Gia_Obj_t *, vRoots, pObj, i, nPos )
3531 // Gia_ObjRiToRo(p, pObj)->Value = Gia_ManAppendCi( pNew );
3532 // create internal nodes
3533 Vec_PtrForEachEntry( Gia_Obj_t *, vNodes, pObj, i )
3534 if ( Gia_ObjIsMux(p, pObj) )
3535 pObj->Value = Gia_ManAppendMux( pNew, Gia_ObjFanin2Copy(p, pObj), Gia_ObjFanin1Copy(pObj), Gia_ObjFanin0Copy(pObj) );
3536 else if ( Gia_ObjIsXor(pObj) )
3537 pObj->Value = Gia_ManAppendXor( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
3538 else
3539 pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
3540 // create COs
3541 Vec_PtrForEachEntry( Gia_Obj_t *, vRoots, pObj, i )
3542 // Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
3543 Gia_ManAppendCo( pNew, pObj->Value );
3544 // finalize
3545 // Gia_ManSetRegNum( pNew, Vec_PtrSize(vRoots)-nPos );
3546 Gia_ManSetRegNum( pNew, 0 );
3547 Vec_PtrFree( vLeaves );
3548 Vec_PtrFree( vNodes );
3549 Vec_PtrFree( vRoots );
3550 return pNew;
3551
3552 }
Gia_ManDupAndConesLimit_rec(Gia_Man_t * pNew,Gia_Man_t * p,int iObj,int Level)3553 void Gia_ManDupAndConesLimit_rec( Gia_Man_t * pNew, Gia_Man_t * p, int iObj, int Level )
3554 {
3555 Gia_Obj_t * pObj = Gia_ManObj(p, iObj);
3556 if ( ~pObj->Value )
3557 return;
3558 if ( !Gia_ObjIsAnd(pObj) || Gia_ObjLevel(p, pObj) < Level )
3559 {
3560 pObj->Value = Gia_ManAppendCi( pNew );
3561 //printf( "PI %d for %d.\n", Abc_Lit2Var(pObj->Value), iObj );
3562 return;
3563 }
3564 Gia_ManDupAndConesLimit_rec( pNew, p, Gia_ObjFaninId0(pObj, iObj), Level );
3565 Gia_ManDupAndConesLimit_rec( pNew, p, Gia_ObjFaninId1(pObj, iObj), Level );
3566 pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
3567 //printf( "Obj %d for %d.\n", Abc_Lit2Var(pObj->Value), iObj );
3568 }
Gia_ManDupAndConesLimit(Gia_Man_t * p,int * pAnds,int nAnds,int Level)3569 Gia_Man_t * Gia_ManDupAndConesLimit( Gia_Man_t * p, int * pAnds, int nAnds, int Level )
3570 {
3571 Gia_Man_t * pNew;
3572 int i;
3573 pNew = Gia_ManStart( 1000 );
3574 pNew->pName = Abc_UtilStrsav( p->pName );
3575 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
3576 Gia_ManLevelNum( p );
3577 Gia_ManFillValue( p );
3578 Gia_ManConst0(p)->Value = 0;
3579 for ( i = 0; i < nAnds; i++ )
3580 Gia_ManDupAndConesLimit_rec( pNew, p, pAnds[i], Level );
3581 for ( i = 0; i < nAnds; i++ )
3582 Gia_ManAppendCo( pNew, Gia_ManObj(p, pAnds[i])->Value );
3583 return pNew;
3584 }
3585
Gia_ManDupAndConesLimit2_rec(Gia_Man_t * pNew,Gia_Man_t * p,int iObj,int Level)3586 void Gia_ManDupAndConesLimit2_rec( Gia_Man_t * pNew, Gia_Man_t * p, int iObj, int Level )
3587 {
3588 Gia_Obj_t * pObj = Gia_ManObj(p, iObj);
3589 if ( ~pObj->Value )
3590 return;
3591 if ( !Gia_ObjIsAnd(pObj) || Level <= 0 )
3592 {
3593 pObj->Value = Gia_ManAppendCi( pNew );
3594 //printf( "PI %d for %d.\n", Abc_Lit2Var(pObj->Value), iObj );
3595 return;
3596 }
3597 Gia_ManDupAndConesLimit2_rec( pNew, p, Gia_ObjFaninId0(pObj, iObj), Level-1 );
3598 Gia_ManDupAndConesLimit2_rec( pNew, p, Gia_ObjFaninId1(pObj, iObj), Level-1 );
3599 pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
3600 //printf( "Obj %d for %d.\n", Abc_Lit2Var(pObj->Value), iObj );
3601 }
Gia_ManDupAndConesLimit2(Gia_Man_t * p,int * pAnds,int nAnds,int Level)3602 Gia_Man_t * Gia_ManDupAndConesLimit2( Gia_Man_t * p, int * pAnds, int nAnds, int Level )
3603 {
3604 Gia_Man_t * pNew;
3605 int i;
3606 pNew = Gia_ManStart( 1000 );
3607 pNew->pName = Abc_UtilStrsav( p->pName );
3608 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
3609 Gia_ManFillValue( p );
3610 Gia_ManConst0(p)->Value = 0;
3611 for ( i = 0; i < nAnds; i++ )
3612 Gia_ManDupAndConesLimit2_rec( pNew, p, pAnds[i], Level );
3613 for ( i = 0; i < nAnds; i++ )
3614 Gia_ManAppendCo( pNew, Gia_ManObj(p, pAnds[i])->Value );
3615 return pNew;
3616
3617 }
3618
3619 /**Function*************************************************************
3620
3621 Synopsis [Generates AIG representing 1-hot condition for N inputs.]
3622
3623 Description [The condition is true of all POs are 0.]
3624
3625 SideEffects []
3626
3627 SeeAlso []
3628
3629 ***********************************************************************/
Gia_ManOneHot(int nSkips,int nVars)3630 Gia_Man_t * Gia_ManOneHot( int nSkips, int nVars )
3631 {
3632 Gia_Man_t * p;
3633 int i, b, Shift, iGiaLit, nLogVars = Abc_Base2Log( nVars );
3634 int * pTemp = ABC_CALLOC( int, (1 << nLogVars) );
3635 p = Gia_ManStart( nSkips + 4 * nVars + 1 );
3636 p->pName = Abc_UtilStrsav( "onehot" );
3637 for ( i = 0; i < nSkips; i++ )
3638 Gia_ManAppendCi( p );
3639 for ( i = 0; i < nVars; i++ )
3640 pTemp[i] = Gia_ManAppendCi( p );
3641 Gia_ManHashStart( p );
3642 for ( b = 0; b < nLogVars; b++ )
3643 for ( i = 0, Shift = (1<<b); i < (1 << nLogVars); i += 2*Shift )
3644 {
3645 iGiaLit = Gia_ManHashAnd( p, pTemp[i], pTemp[i + Shift] );
3646 if ( iGiaLit )
3647 Gia_ManAppendCo( p, iGiaLit );
3648 pTemp[i] = Gia_ManHashOr( p, pTemp[i], pTemp[i + Shift] );
3649 }
3650 Gia_ManHashStop( p );
3651 Gia_ManAppendCo( p, Abc_LitNot(pTemp[0]) );
3652 ABC_FREE( pTemp );
3653 assert( Gia_ManObjNum(p) <= nSkips + 4 * nVars + 1 );
3654 return p;
3655 }
Gia_ManDupOneHot(Gia_Man_t * p)3656 Gia_Man_t * Gia_ManDupOneHot( Gia_Man_t * p )
3657 {
3658 Gia_Man_t * pOneHot, * pNew = Gia_ManDup( p );
3659 if ( Gia_ManRegNum(pNew) == 0 )
3660 {
3661 Abc_Print( 0, "Appending 1-hotness constraints to the PIs.\n" );
3662 pOneHot = Gia_ManOneHot( 0, Gia_ManCiNum(pNew) );
3663 }
3664 else
3665 pOneHot = Gia_ManOneHot( Gia_ManPiNum(pNew), Gia_ManRegNum(pNew) );
3666 Gia_ManDupAppendShare( pNew, pOneHot );
3667 pNew->nConstrs += Gia_ManPoNum(pOneHot);
3668 Gia_ManStop( pOneHot );
3669 return pNew;
3670 }
3671
3672 /**Function*************************************************************
3673
3674 Synopsis [Duplicates the AIG with nodes ordered by level.]
3675
3676 Description []
3677
3678 SideEffects []
3679
3680 SeeAlso []
3681
3682 ***********************************************************************/
Gia_ManDupLevelized(Gia_Man_t * p)3683 Gia_Man_t * Gia_ManDupLevelized( Gia_Man_t * p )
3684 {
3685 Gia_Man_t * pNew;
3686 Gia_Obj_t * pObj;
3687 int i, nLevels = Gia_ManLevelNum( p );
3688 int * pCounts = ABC_CALLOC( int, nLevels + 1 );
3689 int * pNodes = ABC_ALLOC( int, Gia_ManAndNum(p) );
3690 Gia_ManForEachAnd( p, pObj, i )
3691 pCounts[Gia_ObjLevel(p, pObj)]++;
3692 for ( i = 1; i <= nLevels; i++ )
3693 pCounts[i] += pCounts[i-1];
3694 Gia_ManForEachAnd( p, pObj, i )
3695 pNodes[pCounts[Gia_ObjLevel(p, pObj)-1]++] = i;
3696 // duplicate
3697 pNew = Gia_ManStart( Gia_ManObjNum(p) );
3698 pNew->pName = Abc_UtilStrsav( p->pName );
3699 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
3700 Gia_ManConst0(p)->Value = 0;
3701 Gia_ManForEachCi( p, pObj, i )
3702 pObj->Value = Gia_ManAppendCi( pNew );
3703 for ( i = 0; i < Gia_ManAndNum(p) && (pObj = Gia_ManObj(p, pNodes[i])); i++ )
3704 pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
3705 Gia_ManForEachCo( p, pObj, i )
3706 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
3707 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
3708 ABC_FREE( pCounts );
3709 ABC_FREE( pNodes );
3710 return pNew;
3711 }
3712
3713 /**Function*************************************************************
3714
3715 Synopsis []
3716
3717 Description []
3718
3719 SideEffects []
3720
3721 SeeAlso []
3722
3723 ***********************************************************************/
Gia_ManDupFromVecs(Gia_Man_t * p,Vec_Int_t * vCis,Vec_Int_t * vAnds,Vec_Int_t * vCos,int nRegs)3724 Gia_Man_t * Gia_ManDupFromVecs( Gia_Man_t * p, Vec_Int_t * vCis, Vec_Int_t * vAnds, Vec_Int_t * vCos, int nRegs )
3725 {
3726 Gia_Man_t * pNew;
3727 Gia_Obj_t * pObj;
3728 int i;
3729 // start the new manager
3730 pNew = Gia_ManStart( 5000 );
3731 pNew->pName = Abc_UtilStrsav( p->pName );
3732 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
3733 // create constant
3734 Gia_ManConst0(p)->Value = 0;
3735 // create PIs
3736 Gia_ManForEachObjVec( vCis, p, pObj, i )
3737 pObj->Value = Gia_ManAppendCi( pNew );
3738 // create internal nodes
3739 Gia_ManForEachObjVec( vAnds, p, pObj, i )
3740 pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
3741 // create ROs
3742 Gia_ManForEachObjVec( vCos, p, pObj, i )
3743 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
3744 Gia_ManSetRegNum( pNew, nRegs );
3745 return pNew;
3746 }
3747
3748 /**Function*************************************************************
3749
3750 Synopsis []
3751
3752 Description []
3753
3754 SideEffects []
3755
3756 SeeAlso []
3757
3758 ***********************************************************************/
Gia_ManDupSliced(Gia_Man_t * p,int nSuppMax)3759 Gia_Man_t * Gia_ManDupSliced( Gia_Man_t * p, int nSuppMax )
3760 {
3761 Gia_Man_t * pNew;
3762 Gia_Obj_t * pObj;
3763 int i;
3764 // start the new manager
3765 pNew = Gia_ManStart( 5000 );
3766 pNew->pName = Abc_UtilStrsav( p->pName );
3767 // create constant and PIs
3768 Gia_ManConst0(p)->Value = 0;
3769 Gia_ManForEachCi( p, pObj, i )
3770 pObj->Value = Gia_ManAppendCi( pNew );
3771 // create internal nodes
3772 Gia_ManCleanMark01(p);
3773 Gia_ManForEachAnd( p, pObj, i )
3774 if ( Gia_ManSuppSize(p, &i, 1) <= nSuppMax )
3775 {
3776 pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
3777 pObj->fMark0 = 1;
3778 }
3779 else
3780 {
3781 Gia_ObjFanin0(pObj)->fMark1 = 1;
3782 Gia_ObjFanin1(pObj)->fMark1 = 1;
3783 }
3784 Gia_ManForEachCo( p, pObj, i )
3785 Gia_ObjFanin0(pObj)->fMark1 = 1;
3786 // add POs for the nodes pointed to
3787 Gia_ManForEachAnd( p, pObj, i )
3788 if ( pObj->fMark0 && pObj->fMark1 )
3789 Gia_ManAppendCo( pNew, pObj->Value );
3790 // cleanup and leave
3791 Gia_ManCleanMark01(p);
3792 return pNew;
3793 }
3794
3795
3796 /**Function*************************************************************
3797
3798 Synopsis [Extract constraints.]
3799
3800 Description []
3801
3802 SideEffects []
3803
3804 SeeAlso []
3805
3806 ***********************************************************************/
Gia_ManDupWithConstrCollectAnd_rec(Gia_Man_t * p,Gia_Obj_t * pObj,Vec_Int_t * vSuper,int fFirst)3807 void Gia_ManDupWithConstrCollectAnd_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSuper, int fFirst )
3808 {
3809 if ( (Gia_IsComplement(pObj) || !Gia_ObjIsAnd(pObj)) && !fFirst )
3810 {
3811 Vec_IntPushUnique( vSuper, Gia_ObjToLit(p, pObj) );
3812 return;
3813 }
3814 Gia_ManDupWithConstrCollectAnd_rec( p, Gia_ObjChild0(pObj), vSuper, 0 );
3815 Gia_ManDupWithConstrCollectAnd_rec( p, Gia_ObjChild1(pObj), vSuper, 0 );
3816 }
Gia_ManDupWithConstr(Gia_Man_t * p)3817 Gia_Man_t * Gia_ManDupWithConstr( Gia_Man_t * p )
3818 {
3819 Vec_Int_t * vSuper;
3820 Gia_Man_t * pNew, * pTemp;
3821 Gia_Obj_t * pObj;
3822 int i, iDriver, iLit, iLitBest = -1, LevelBest = -1;
3823 assert( Gia_ManPoNum(p) == 1 );
3824 assert( Gia_ManRegNum(p) == 0 );
3825 pObj = Gia_ManPo( p, 0 );
3826 if ( Gia_ObjFaninC0(pObj) )
3827 {
3828 printf( "The miter's output is not AND-decomposable.\n" );
3829 return NULL;
3830 }
3831 if ( Gia_ObjFaninId0p(p, pObj) == 0 )
3832 {
3833 printf( "The miter's output is a constant.\n" );
3834 return NULL;
3835 }
3836 vSuper = Vec_IntAlloc( 100 );
3837 Gia_ManDupWithConstrCollectAnd_rec( p, Gia_ObjChild0(pObj), vSuper, 1 );
3838 assert( Vec_IntSize(vSuper) > 1 );
3839 // find the highest level
3840 Gia_ManLevelNum( p );
3841 Vec_IntForEachEntry( vSuper, iLit, i )
3842 if ( LevelBest < Gia_ObjLevelId(p, Abc_Lit2Var(iLit)) )
3843 LevelBest = Gia_ObjLevelId(p, Abc_Lit2Var(iLit)), iLitBest = iLit;
3844 assert( iLitBest != -1 );
3845 // create new manager
3846 pNew = Gia_ManStart( Gia_ManObjNum(p) );
3847 pNew->pName = Abc_UtilStrsav( p->pName );
3848 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
3849 Gia_ManConst0(p)->Value = 0;
3850 Gia_ManHashAlloc( pNew );
3851 Gia_ManForEachObj1( p, pObj, i )
3852 {
3853 if ( Gia_ObjIsAnd(pObj) )
3854 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
3855 else if ( Gia_ObjIsCi(pObj) )
3856 pObj->Value = Gia_ManAppendCi( pNew );
3857 }
3858 // create AND of nodes
3859 iDriver = -1;
3860 Vec_IntForEachEntry( vSuper, iLit, i )
3861 {
3862 if ( iLit == iLitBest )
3863 continue;
3864 if ( iDriver == -1 )
3865 iDriver = Gia_ObjLitCopy(p, iLit);
3866 else
3867 iDriver = Gia_ManHashAnd( pNew, iDriver, Gia_ObjLitCopy(p, iLit) );
3868 }
3869 // create the main PO
3870 Gia_ManAppendCo( pNew, Gia_ObjLitCopy(p, iLitBest) );
3871 // create the constraint PO
3872 Gia_ManAppendCo( pNew, Abc_LitNot(iDriver) );
3873 pNew->nConstrs = 1;
3874 // rehash
3875 pNew = Gia_ManCleanup( pTemp = pNew );
3876 Gia_ManStop( pTemp );
3877 Vec_IntFree( vSuper );
3878 return pNew;
3879
3880 }
3881
3882 /**Function*************************************************************
3883
3884 Synopsis [Compares two objects by their distance.]
3885
3886 Description []
3887
3888 SideEffects []
3889
3890 SeeAlso []
3891
3892 ***********************************************************************/
Gia_ManSortByValue(Gia_Obj_t ** pp1,Gia_Obj_t ** pp2)3893 int Gia_ManSortByValue( Gia_Obj_t ** pp1, Gia_Obj_t ** pp2 )
3894 {
3895 int Diff = Gia_Regular(*pp1)->Value - Gia_Regular(*pp2)->Value;
3896 if ( Diff < 0 )
3897 return -1;
3898 if ( Diff > 0 )
3899 return 1;
3900 return 0;
3901 }
3902
3903 /**Function*************************************************************
3904
3905 Synopsis [Decomposes the miter outputs.]
3906
3907 Description []
3908
3909 SideEffects []
3910
3911 SeeAlso []
3912
3913 ***********************************************************************/
Gia_ManDupOuts(Gia_Man_t * p)3914 Gia_Man_t * Gia_ManDupOuts( Gia_Man_t * p )
3915 {
3916 Gia_Man_t * pNew;
3917 Gia_Obj_t * pObj;
3918 int i;
3919 pNew = Gia_ManStart( Gia_ManObjNum(p) );
3920 pNew->pName = Abc_UtilStrsav( p->pName );
3921 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
3922 Gia_ManConst0(p)->Value = 0;
3923 Gia_ManForEachCi( p, pObj, i )
3924 pObj->Value = Gia_ManAppendCi(pNew);
3925 Gia_ManForEachAnd( p, pObj, i )
3926 pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
3927 Gia_ManForEachPo( p, pObj, i )
3928 Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
3929 Gia_ManForEachAnd( p, pObj, i )
3930 Gia_ManAppendCo( pNew, pObj->Value );
3931 Gia_ManForEachRi( p, pObj, i )
3932 Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
3933 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
3934 assert( Gia_ManIsNormalized(pNew) );
3935 return pNew;
3936 }
3937
3938 /**Function*************************************************************
3939
3940 Synopsis [Computes supports for each node.]
3941
3942 Description []
3943
3944 SideEffects []
3945
3946 SeeAlso []
3947
3948 ***********************************************************************/
Gia_ManCreateNodeSupps(Gia_Man_t * p,Vec_Int_t * vNodes,int fVerbose)3949 Vec_Wec_t * Gia_ManCreateNodeSupps( Gia_Man_t * p, Vec_Int_t * vNodes, int fVerbose )
3950 {
3951 abctime clk = Abc_Clock();
3952 Gia_Obj_t * pObj; int i, Id;
3953 Vec_Wec_t * vSuppsNo = Vec_WecStart( Vec_IntSize(vNodes) );
3954 Vec_Wec_t * vSupps = Vec_WecStart( Gia_ManObjNum(p) );
3955 Gia_ManForEachCiId( p, Id, i )
3956 Vec_IntPush( Vec_WecEntry(vSupps, Id), i );
3957 Gia_ManForEachAnd( p, pObj, Id )
3958 Vec_IntTwoMerge2( Vec_WecEntry(vSupps, Gia_ObjFaninId0(pObj, Id)),
3959 Vec_WecEntry(vSupps, Gia_ObjFaninId1(pObj, Id)),
3960 Vec_WecEntry(vSupps, Id) );
3961 Gia_ManForEachObjVec( vNodes, p, pObj, i )
3962 Vec_IntAppend( Vec_WecEntry(vSuppsNo, i), Vec_WecEntry(vSupps, Gia_ObjId(p, pObj)) );
3963 Vec_WecFree( vSupps );
3964 if ( fVerbose )
3965 Abc_PrintTime( 1, "Support computation", Abc_Clock() - clk );
3966 return vSuppsNo;
3967 }
3968
Gia_ManCreateCoSupps(Gia_Man_t * p,int fVerbose)3969 Vec_Wec_t * Gia_ManCreateCoSupps( Gia_Man_t * p, int fVerbose )
3970 {
3971 abctime clk = Abc_Clock();
3972 Gia_Obj_t * pObj; int i, Id;
3973 Vec_Wec_t * vSuppsCo = Vec_WecStart( Gia_ManCoNum(p) );
3974 Vec_Wec_t * vSupps = Vec_WecStart( Gia_ManObjNum(p) );
3975 Gia_ManForEachCiId( p, Id, i )
3976 Vec_IntPush( Vec_WecEntry(vSupps, Id), i );
3977 Gia_ManForEachAnd( p, pObj, Id )
3978 Vec_IntTwoMerge2( Vec_WecEntry(vSupps, Gia_ObjFaninId0(pObj, Id)),
3979 Vec_WecEntry(vSupps, Gia_ObjFaninId1(pObj, Id)),
3980 Vec_WecEntry(vSupps, Id) );
3981 Gia_ManForEachCo( p, pObj, i )
3982 Vec_IntAppend( Vec_WecEntry(vSuppsCo, i), Vec_WecEntry(vSupps, Gia_ObjFaninId0p(p, pObj)) );
3983 Vec_WecFree( vSupps );
3984 if ( fVerbose )
3985 Abc_PrintTime( 1, "Support computation", Abc_Clock() - clk );
3986 return vSuppsCo;
3987 }
Gia_ManCoSuppSizeMax(Gia_Man_t * p,Vec_Wec_t * vSupps)3988 int Gia_ManCoSuppSizeMax( Gia_Man_t * p, Vec_Wec_t * vSupps )
3989 {
3990 Gia_Obj_t * pObj;
3991 Vec_Int_t * vSuppOne;
3992 int i, nSuppMax = 1;
3993 Gia_ManForEachCo( p, pObj, i )
3994 {
3995 vSuppOne = Vec_WecEntry( vSupps, i );
3996 nSuppMax = Abc_MaxInt( nSuppMax, Vec_IntSize(vSuppOne) );
3997 }
3998 return nSuppMax;
3999 }
Gia_ManCoLargestSupp(Gia_Man_t * p,Vec_Wec_t * vSupps)4000 int Gia_ManCoLargestSupp( Gia_Man_t * p, Vec_Wec_t * vSupps )
4001 {
4002 Gia_Obj_t * pObj;
4003 Vec_Int_t * vSuppOne;
4004 int i, iCoMax = -1, nSuppMax = -1;
4005 Gia_ManForEachCo( p, pObj, i )
4006 {
4007 vSuppOne = Vec_WecEntry( vSupps, i );
4008 if ( nSuppMax < Vec_IntSize(vSuppOne) )
4009 {
4010 nSuppMax = Vec_IntSize(vSuppOne);
4011 iCoMax = i;
4012 }
4013 }
4014 return iCoMax;
4015 }
Gia_ManSortCoBySuppSize(Gia_Man_t * p,Vec_Wec_t * vSupps)4016 Vec_Int_t * Gia_ManSortCoBySuppSize( Gia_Man_t * p, Vec_Wec_t * vSupps )
4017 {
4018 Vec_Int_t * vOrder = Vec_IntAlloc( Gia_ManCoNum(p) );
4019 Vec_Wrd_t * vSortData = Vec_WrdAlloc( Gia_ManCoNum(p) );
4020 Vec_Int_t * vSuppOne; word Entry; int i;
4021 Vec_WecForEachLevel( vSupps, vSuppOne, i )
4022 Vec_WrdPush( vSortData, ((word)i << 32) | Vec_IntSize(vSuppOne) );
4023 Abc_QuickSort3( Vec_WrdArray(vSortData), Vec_WrdSize(vSortData), 1 );
4024 Vec_WrdForEachEntry( vSortData, Entry, i )
4025 Vec_IntPush( vOrder, (int)(Entry >> 32) );
4026 Vec_WrdFree( vSortData );
4027 return vOrder;
4028 }
4029
4030 /**Function*************************************************************
4031
4032 Synopsis [Remaps each CO cone to depend on the first CI variables.]
4033
4034 Description []
4035
4036 SideEffects []
4037
4038 SeeAlso []
4039
4040 ***********************************************************************/
Gia_ManDupHashDfs_rec(Gia_Man_t * pNew,Gia_Man_t * p,Gia_Obj_t * pObj)4041 int Gia_ManDupHashDfs_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
4042 {
4043 if ( ~pObj->Value )
4044 return pObj->Value;
4045 assert( Gia_ObjIsAnd(pObj) );
4046 Gia_ManDupHashDfs_rec( pNew, p, Gia_ObjFanin0(pObj) );
4047 Gia_ManDupHashDfs_rec( pNew, p, Gia_ObjFanin1(pObj) );
4048 return pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
4049 }
Gia_ManDupCleanDfs_rec(Gia_Obj_t * pObj)4050 void Gia_ManDupCleanDfs_rec( Gia_Obj_t * pObj )
4051 {
4052 if ( !~pObj->Value )
4053 return;
4054 pObj->Value = ~0;
4055 if ( Gia_ObjIsCi(pObj) )
4056 return;
4057 assert( Gia_ObjIsAnd(pObj) );
4058 Gia_ManDupCleanDfs_rec( Gia_ObjFanin0(pObj) );
4059 Gia_ManDupCleanDfs_rec( Gia_ObjFanin1(pObj) );
4060 }
Gia_ManDupStrashReduce(Gia_Man_t * p,Vec_Wec_t * vSupps,Vec_Int_t ** pvCoMap)4061 Gia_Man_t * Gia_ManDupStrashReduce( Gia_Man_t * p, Vec_Wec_t * vSupps, Vec_Int_t ** pvCoMap )
4062 {
4063 Gia_Obj_t * pObj;
4064 Gia_Man_t * pNew, * pTemp;
4065 Vec_Int_t * vSuppOne, * vCoMapLit;
4066 int i, k, iCi, iLit, nSuppMax;
4067 assert( Gia_ManRegNum(p) == 0 );
4068 Gia_ManFillValue( p );
4069 vCoMapLit = Vec_IntAlloc( Gia_ManCoNum(p) );
4070 pNew = Gia_ManStart( Gia_ManObjNum(p) );
4071 pNew->pName = Abc_UtilStrsav( p->pName );
4072 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
4073 Gia_ManConst0(p)->Value = 0;
4074 nSuppMax = Gia_ManCoSuppSizeMax( p, vSupps );
4075 for ( i = 0; i < nSuppMax; i++ )
4076 Gia_ManAppendCi(pNew);
4077 Gia_ManHashAlloc( pNew );
4078 Gia_ManForEachCo( p, pObj, i )
4079 {
4080 vSuppOne = Vec_WecEntry( vSupps, i );
4081 if ( Vec_IntSize(vSuppOne) == 0 )
4082 Vec_IntPush( vCoMapLit, Abc_Var2Lit(0, Gia_ObjFaninC0(pObj)) );
4083 else if ( Vec_IntSize(vSuppOne) == 1 )
4084 Vec_IntPush( vCoMapLit, Abc_Var2Lit(1, Gia_ObjFaninC0(pObj)) );
4085 else
4086 {
4087 Vec_IntForEachEntry( vSuppOne, iCi, k )
4088 Gia_ManCi(p, iCi)->Value = Gia_Obj2Lit(pNew, Gia_ManCi(pNew, k) );
4089 Gia_ManDupHashDfs_rec( pNew, p, Gia_ObjFanin0(pObj) );
4090 assert( Gia_ObjFanin0Copy(pObj) < 2 * Gia_ManObjNum(pNew) );
4091 Vec_IntPush( vCoMapLit, Gia_ObjFanin0Copy(pObj) );
4092 Gia_ManDupCleanDfs_rec( Gia_ObjFanin0(pObj) );
4093 }
4094 }
4095 Gia_ManHashStop( pNew );
4096 assert( Vec_IntSize(vCoMapLit) == Gia_ManCoNum(p) );
4097 if ( pvCoMap == NULL ) // do not remap
4098 {
4099 Vec_IntForEachEntry( vCoMapLit, iLit, i )
4100 Gia_ManAppendCo( pNew, iLit );
4101 }
4102 else // remap
4103 {
4104 Vec_Int_t * vCoMapRes = Vec_IntAlloc( Gia_ManCoNum(p) ); // map old CO into new CO
4105 Vec_Int_t * vMap = Vec_IntStartFull( 2*Gia_ManObjNum(pNew) ); // map new lit into new CO
4106 Vec_IntForEachEntry( vCoMapLit, iLit, i )
4107 {
4108 if ( Vec_IntEntry(vMap, iLit) == -1 )
4109 {
4110 Vec_IntWriteEntry( vMap, iLit, Gia_ManCoNum(pNew) );
4111 Gia_ManAppendCo( pNew, iLit );
4112 }
4113 Vec_IntPush( vCoMapRes, Vec_IntEntry(vMap, iLit) );
4114 }
4115 Vec_IntFree( vMap );
4116 *pvCoMap = vCoMapRes;
4117 }
4118 Vec_IntFree( vCoMapLit );
4119 pNew = Gia_ManCleanup( pTemp = pNew );
4120 Gia_ManStop( pTemp );
4121 return pNew;
4122 }
Gia_ManIsoStrashReduce2(Gia_Man_t * p,Vec_Ptr_t ** pvPosEquivs,int fVerbose)4123 Gia_Man_t * Gia_ManIsoStrashReduce2( Gia_Man_t * p, Vec_Ptr_t ** pvPosEquivs, int fVerbose )
4124 {
4125 Vec_Int_t * vCoMap;
4126 Vec_Wec_t * vSupps = Gia_ManCreateCoSupps( p, fVerbose );
4127 Gia_Man_t * pNew = Gia_ManDupStrashReduce( p, vSupps, &vCoMap );
4128 Vec_IntFree( vCoMap );
4129 Vec_WecFree( vSupps );
4130 *pvPosEquivs = NULL;
4131 return pNew;
4132 }
4133
Gia_ManIsoStrashReduceOne(Gia_Man_t * pNew,Gia_Man_t * p,Gia_Obj_t * pObj,Vec_Int_t * vSupp)4134 int Gia_ManIsoStrashReduceOne( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSupp )
4135 {
4136 int k, iCi, iLit;
4137 assert( Gia_ObjIsCo(pObj) );
4138 if ( Vec_IntSize(vSupp) == 0 )
4139 return Abc_Var2Lit(0, Gia_ObjFaninC0(pObj));
4140 if ( Vec_IntSize(vSupp) == 1 )
4141 return Abc_Var2Lit(1, Gia_ObjFaninC0(pObj));
4142 Vec_IntForEachEntry( vSupp, iCi, k )
4143 Gia_ManCi(p, iCi)->Value = Gia_Obj2Lit(pNew, Gia_ManCi(pNew, k) );
4144 Gia_ManDupHashDfs_rec( pNew, p, Gia_ObjFanin0(pObj) );
4145 iLit = Gia_ObjFanin0Copy(pObj);
4146 Gia_ManDupCleanDfs_rec( Gia_ObjFanin0(pObj) );
4147 return iLit;
4148 }
Gia_ManIsoStrashReduceInt(Gia_Man_t * p,Vec_Wec_t * vSupps,int fVerbose)4149 Vec_Wec_t * Gia_ManIsoStrashReduceInt( Gia_Man_t * p, Vec_Wec_t * vSupps, int fVerbose )
4150 {
4151 Gia_Man_t * pNew;
4152 Gia_Obj_t * pObj;
4153 Vec_Wec_t * vPosEquivs = Vec_WecAlloc( 100 );
4154 Vec_Int_t * vSuppOne, * vMap = Vec_IntAlloc( 10000 );
4155 int i, iLit, nSuppMax = Gia_ManCoSuppSizeMax( p, vSupps );
4156 // count how many times each support size appears
4157 Vec_Int_t * vSizeCount = Vec_IntStart( nSuppMax + 1 );
4158 Vec_WecForEachLevel( vSupps, vSuppOne, i )
4159 Vec_IntAddToEntry( vSizeCount, Vec_IntSize(vSuppOne), 1 );
4160 // create array of unique outputs
4161 Gia_ManFillValue( p );
4162 pNew = Gia_ManStart( Gia_ManObjNum(p) );
4163 Gia_ManConst0(p)->Value = 0;
4164 for ( i = 0; i < nSuppMax; i++ )
4165 Gia_ManAppendCi(pNew);
4166 Gia_ManHashAlloc( pNew );
4167 Gia_ManForEachCo( p, pObj, i )
4168 {
4169 vSuppOne = Vec_WecEntry( vSupps, i );
4170 if ( Vec_IntEntry(vSizeCount, Vec_IntSize(vSuppOne)) == 1 )
4171 {
4172 Vec_IntPush( Vec_WecPushLevel(vPosEquivs), i );
4173 continue;
4174 }
4175 iLit = Gia_ManIsoStrashReduceOne( pNew, p, pObj, vSuppOne );
4176 Vec_IntFillExtra( vMap, iLit + 1, -1 );
4177 if ( Vec_IntEntry(vMap, iLit) == -1 )
4178 {
4179 Vec_IntWriteEntry( vMap, iLit, Vec_WecSize(vPosEquivs) );
4180 Vec_IntPush( Vec_WecPushLevel(vPosEquivs), i );
4181 continue;
4182 }
4183 Vec_IntPush( Vec_WecEntry(vPosEquivs, Vec_IntEntry(vMap, iLit)), i );
4184 }
4185 Gia_ManHashStop( pNew );
4186 Gia_ManStop( pNew );
4187 Vec_IntFree( vSizeCount );
4188 Vec_IntFree( vMap );
4189 return vPosEquivs;
4190 }
Gia_ManIsoStrashReduce(Gia_Man_t * p,Vec_Ptr_t ** pvPosEquivs,int fVerbose)4191 Gia_Man_t * Gia_ManIsoStrashReduce( Gia_Man_t * p, Vec_Ptr_t ** pvPosEquivs, int fVerbose )
4192 {
4193 Vec_Wec_t * vSupps = Gia_ManCreateCoSupps( p, fVerbose );
4194 Vec_Wec_t * vPosEquivs = Gia_ManIsoStrashReduceInt( p, vSupps, fVerbose );
4195 // find the first outputs and derive GIA
4196 Vec_Int_t * vFirsts = Vec_WecCollectFirsts( vPosEquivs );
4197 Gia_Man_t * pNew = Gia_ManDupCones( p, Vec_IntArray(vFirsts), Vec_IntSize(vFirsts), 0 );
4198 Vec_IntFree( vFirsts );
4199 Vec_WecFree( vSupps );
4200 // report and return
4201 if ( fVerbose )
4202 {
4203 printf( "Nontrivial classes:\n" );
4204 Vec_WecPrint( vPosEquivs, 1 );
4205 }
4206 if ( pvPosEquivs )
4207 *pvPosEquivs = Vec_WecConvertToVecPtr( vPosEquivs );
4208 Vec_WecFree( vPosEquivs );
4209 return pNew;
4210 }
4211
4212 /**Function*************************************************************
4213
4214 Synopsis [Decomposes the miter outputs.]
4215
4216 Description []
4217
4218 SideEffects []
4219
4220 SeeAlso []
4221
4222 ***********************************************************************/
Gia_ManDupDemiter(Gia_Man_t * p,int fVerbose)4223 Gia_Man_t * Gia_ManDupDemiter( Gia_Man_t * p, int fVerbose )
4224 {
4225 Vec_Int_t * vSuper;
4226 Vec_Ptr_t * vSuperPtr;
4227 Gia_Man_t * pNew, * pTemp;
4228 Gia_Obj_t * pObj, * pObjPo;
4229 int i, iLit;
4230 assert( Gia_ManPoNum(p) == 1 );
4231 // decompose
4232 pObjPo = Gia_ManPo( p, 0 );
4233 vSuper = Vec_IntAlloc( 100 );
4234 Gia_ManDupWithConstrCollectAnd_rec( p, Gia_ObjFanin0(pObjPo), vSuper, 1 );
4235 assert( Vec_IntSize(vSuper) > 1 );
4236 // report the result
4237 printf( "The miter is %s-decomposable into %d parts.\n", Gia_ObjFaninC0(pObjPo) ? "OR":"AND", Vec_IntSize(vSuper) );
4238 // create levels
4239 Gia_ManLevelNum( p );
4240 Vec_IntForEachEntry( vSuper, iLit, i )
4241 Gia_ManObj(p, Abc_Lit2Var(iLit))->Value = Gia_ObjLevelId(p, Abc_Lit2Var(iLit));
4242 // create pointer array
4243 vSuperPtr = Vec_PtrAlloc( Vec_IntSize(vSuper) );
4244 Vec_IntForEachEntry( vSuper, iLit, i )
4245 Vec_PtrPush( vSuperPtr, Gia_Lit2Obj(p, iLit) );
4246 Vec_PtrSort( vSuperPtr, (int (*)(void))Gia_ManSortByValue );
4247 // create new manager
4248 pNew = Gia_ManStart( Gia_ManObjNum(p) );
4249 pNew->pName = Abc_UtilStrsav( p->pName );
4250 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
4251 Gia_ManConst0(p)->Value = 0;
4252 Gia_ManHashAlloc( pNew );
4253 Gia_ManForEachCi( p, pObj, i )
4254 pObj->Value = Gia_ManAppendCi( pNew );
4255 Gia_ManForEachAnd( p, pObj, i )
4256 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
4257 // create the outputs
4258 Vec_PtrForEachEntry( Gia_Obj_t *, vSuperPtr, pObj, i )
4259 Gia_ManAppendCo( pNew, Gia_ObjLitCopy(p, Gia_Obj2Lit(p, pObj)) ^ Gia_ObjFaninC0(pObjPo) );
4260 Gia_ManForEachRi( p, pObj, i )
4261 Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
4262 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
4263 // rehash
4264 pNew = Gia_ManCleanup( pTemp = pNew );
4265 Gia_ManStop( pTemp );
4266 Vec_IntFree( vSuper );
4267 Vec_PtrFree( vSuperPtr );
4268 return pNew;
4269 }
4270
4271 /**Function*************************************************************
4272
4273 Synopsis []
4274
4275 Description []
4276
4277 SideEffects []
4278
4279 SeeAlso []
4280
4281 ***********************************************************************/
Gia_ManDupDemiterOrderXors2(Gia_Man_t * p,Vec_Int_t * vXors)4282 void Gia_ManDupDemiterOrderXors2( Gia_Man_t * p, Vec_Int_t * vXors )
4283 {
4284 int i, iObj, * pPerm;
4285 Vec_Int_t * vSizes = Vec_IntAlloc( 100 );
4286 Vec_IntForEachEntry( vXors, iObj, i )
4287 Vec_IntPush( vSizes, Gia_ManSuppSize(p, &iObj, 1) );
4288 pPerm = Abc_MergeSortCost( Vec_IntArray(vSizes), Vec_IntSize(vSizes) );
4289 Vec_IntClear( vSizes );
4290 for ( i = 0; i < Vec_IntSize(vXors); i++ )
4291 Vec_IntPush( vSizes, Vec_IntEntry(vXors, pPerm[i]) );
4292 ABC_FREE( pPerm );
4293 Vec_IntClear( vXors );
4294 Vec_IntAppend( vXors, vSizes );
4295 Vec_IntFree( vSizes );
4296 }
Gia_ManDupDemiterFindMin(Vec_Wec_t * vSupps,Vec_Int_t * vTakenIns,Vec_Int_t * vTakenOuts)4297 int Gia_ManDupDemiterFindMin( Vec_Wec_t * vSupps, Vec_Int_t * vTakenIns, Vec_Int_t * vTakenOuts )
4298 {
4299 Vec_Int_t * vLevel;
4300 int i, k, iObj, iObjBest = -1;
4301 int Count, CountBest = ABC_INFINITY;
4302 Vec_WecForEachLevel( vSupps, vLevel, i )
4303 {
4304 if ( Vec_IntEntry(vTakenOuts, i) )
4305 continue;
4306 Count = 0;
4307 Vec_IntForEachEntry( vLevel, iObj, k )
4308 Count += !Vec_IntEntry(vTakenIns, iObj);
4309 if ( CountBest > Count )
4310 {
4311 CountBest = Count;
4312 iObjBest = i;
4313 }
4314 }
4315 return iObjBest;
4316 }
Gia_ManDupDemiterOrderXors(Gia_Man_t * p,Vec_Int_t * vXors)4317 void Gia_ManDupDemiterOrderXors( Gia_Man_t * p, Vec_Int_t * vXors )
4318 {
4319 extern Vec_Wec_t * Gia_ManCreateNodeSupps( Gia_Man_t * p, Vec_Int_t * vNodes, int fVerbose );
4320 Vec_Wec_t * vSupps = Gia_ManCreateNodeSupps( p, vXors, 0 );
4321 Vec_Int_t * vTakenIns = Vec_IntStart( Gia_ManCiNum(p) );
4322 Vec_Int_t * vTakenOuts = Vec_IntStart( Vec_IntSize(vXors) );
4323 Vec_Int_t * vOrder = Vec_IntAlloc( Vec_IntSize(vXors) );
4324 int i, k, iObj;
4325 // add outputs in the order of increasing supports
4326 for ( i = 0; i < Vec_IntSize(vXors); i++ )
4327 {
4328 int Index = Gia_ManDupDemiterFindMin( vSupps, vTakenIns, vTakenOuts );
4329 assert( Index >= 0 && Index < Vec_IntSize(vXors) );
4330 Vec_IntPush( vOrder, Vec_IntEntry(vXors, Index) );
4331 assert( !Vec_IntEntry( vTakenOuts, Index ) );
4332 Vec_IntWriteEntry( vTakenOuts, Index, 1 );
4333 Vec_IntForEachEntry( Vec_WecEntry(vSupps, Index), iObj, k )
4334 Vec_IntWriteEntry( vTakenIns, iObj, 1 );
4335 }
4336 Vec_WecFree( vSupps );
4337 Vec_IntFree( vTakenIns );
4338 Vec_IntFree( vTakenOuts );
4339 // reload
4340 Vec_IntClear( vXors );
4341 Vec_IntAppend( vXors, vOrder );
4342 Vec_IntFree( vOrder );
4343 }
4344
4345
4346 /**Function*************************************************************
4347
4348 Synopsis []
4349
4350 Description []
4351
4352 SideEffects []
4353
4354 SeeAlso []
4355
4356 ***********************************************************************/
Gia_ManSetMark0Dfs_rec(Gia_Man_t * p,int iObj)4357 void Gia_ManSetMark0Dfs_rec( Gia_Man_t * p, int iObj )
4358 {
4359 Gia_Obj_t * pObj;
4360 pObj = Gia_ManObj( p, iObj );
4361 if ( pObj->fMark0 )
4362 return;
4363 pObj->fMark0 = 1;
4364 if ( !Gia_ObjIsAnd(pObj) )
4365 return;
4366 Gia_ManSetMark0Dfs_rec( p, Gia_ObjFaninId0(pObj, iObj) );
4367 Gia_ManSetMark0Dfs_rec( p, Gia_ObjFaninId1(pObj, iObj) );
4368 }
Gia_ManSetMark1Dfs_rec(Gia_Man_t * p,int iObj)4369 void Gia_ManSetMark1Dfs_rec( Gia_Man_t * p, int iObj )
4370 {
4371 Gia_Obj_t * pObj;
4372 pObj = Gia_ManObj( p, iObj );
4373 if ( pObj->fMark1 )
4374 return;
4375 pObj->fMark1 = 1;
4376 if ( !Gia_ObjIsAnd(pObj) )
4377 return;
4378 Gia_ManSetMark1Dfs_rec( p, Gia_ObjFaninId0(pObj, iObj) );
4379 Gia_ManSetMark1Dfs_rec( p, Gia_ObjFaninId1(pObj, iObj) );
4380 }
4381
Gia_ManCountMark0Dfs_rec(Gia_Man_t * p,int iObj)4382 int Gia_ManCountMark0Dfs_rec( Gia_Man_t * p, int iObj )
4383 {
4384 Gia_Obj_t * pObj;
4385 if ( Gia_ObjIsTravIdCurrentId(p, iObj) )
4386 return 0;
4387 Gia_ObjSetTravIdCurrentId(p, iObj);
4388 pObj = Gia_ManObj( p, iObj );
4389 if ( !Gia_ObjIsAnd(pObj) )
4390 return pObj->fMark0;
4391 return Gia_ManCountMark0Dfs_rec( p, Gia_ObjFaninId0(pObj, iObj) ) +
4392 Gia_ManCountMark0Dfs_rec( p, Gia_ObjFaninId1(pObj, iObj) ) + pObj->fMark0;
4393 }
Gia_ManCountMark0Dfs(Gia_Man_t * p,int iObj)4394 int Gia_ManCountMark0Dfs( Gia_Man_t * p, int iObj )
4395 {
4396 Gia_ManIncrementTravId( p );
4397 return Gia_ManCountMark0Dfs_rec( p, iObj );
4398 }
Gia_ManCountMark1Dfs_rec(Gia_Man_t * p,int iObj)4399 int Gia_ManCountMark1Dfs_rec( Gia_Man_t * p, int iObj )
4400 {
4401 Gia_Obj_t * pObj;
4402 if ( Gia_ObjIsTravIdCurrentId(p, iObj) )
4403 return 0;
4404 Gia_ObjSetTravIdCurrentId(p, iObj);
4405 pObj = Gia_ManObj( p, iObj );
4406 if ( !Gia_ObjIsAnd(pObj) )
4407 return pObj->fMark1;
4408 return Gia_ManCountMark1Dfs_rec( p, Gia_ObjFaninId0(pObj, iObj) ) +
4409 Gia_ManCountMark1Dfs_rec( p, Gia_ObjFaninId1(pObj, iObj) ) + pObj->fMark1;
4410 }
Gia_ManCountMark1Dfs(Gia_Man_t * p,int iObj)4411 int Gia_ManCountMark1Dfs( Gia_Man_t * p, int iObj )
4412 {
4413 Gia_ManIncrementTravId( p );
4414 return Gia_ManCountMark1Dfs_rec( p, iObj );
4415 }
4416
Gia_ManDecideWhereToAdd(Gia_Man_t * p,Vec_Int_t * vPart[2],Gia_Obj_t * pFan[2])4417 int Gia_ManDecideWhereToAdd( Gia_Man_t * p, Vec_Int_t * vPart[2], Gia_Obj_t * pFan[2] )
4418 {
4419 int Count0 = 1, Count1 = 0;
4420 assert( Vec_IntSize(vPart[0]) == Vec_IntSize(vPart[1]) );
4421 if ( Vec_IntSize(vPart[0]) > 0 )
4422 {
4423 Count0 = Gia_ManCountMark0Dfs(p, Gia_ObjId(p, pFan[0])) + Gia_ManCountMark1Dfs(p, Gia_ObjId(p, pFan[1]));
4424 Count1 = Gia_ManCountMark0Dfs(p, Gia_ObjId(p, pFan[1])) + Gia_ManCountMark1Dfs(p, Gia_ObjId(p, pFan[0]));
4425 }
4426 return Count0 < Count1;
4427 }
Gia_ManCollectTopXors_rec(Gia_Man_t * p,Gia_Obj_t * pObj,Vec_Int_t * vXors)4428 void Gia_ManCollectTopXors_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXors )
4429 {
4430 Gia_Obj_t * pFan0, * pFan1;
4431 int iObj = Gia_ObjId( p, pObj );
4432 if ( Gia_ObjRecognizeExor(pObj, &pFan0, &pFan1) || !Gia_ObjIsAnd(pObj) )
4433 {
4434 Vec_IntPushUnique( vXors, Gia_ObjId(p, pObj) );
4435 return;
4436 }
4437 if ( Gia_ObjFaninC0(pObj) )
4438 Vec_IntPushUnique( vXors, Gia_ObjFaninId0(pObj, iObj) );
4439 else
4440 Gia_ManCollectTopXors_rec( p, Gia_ObjFanin0(pObj), vXors );
4441 if ( Gia_ObjFaninC1(pObj) )
4442 Vec_IntPushUnique( vXors, Gia_ObjFaninId1(pObj, iObj) );
4443 else
4444 Gia_ManCollectTopXors_rec( p, Gia_ObjFanin1(pObj), vXors );
4445 }
Gia_ManCollectTopXors(Gia_Man_t * p)4446 Vec_Int_t * Gia_ManCollectTopXors( Gia_Man_t * p )
4447 {
4448 int i, iObj, iObj2, fFlip, Count1 = 0;
4449 Vec_Int_t * vXors, * vPart[2], * vOrder;
4450 Gia_Obj_t * pFan[2], * pObj = Gia_ManCo(p, 0);
4451 vXors = Vec_IntAlloc( 100 );
4452 if ( Gia_ManCoNum(p) == 1 )
4453 {
4454 if ( Gia_ObjFaninC0(pObj) )
4455 Gia_ManCollectTopXors_rec( p, Gia_ObjFanin0(pObj), vXors );
4456 else
4457 Vec_IntPush( vXors, Gia_ObjId(p, Gia_ObjFanin0(pObj)) );
4458 }
4459 else
4460 {
4461 Gia_ManForEachCo( p, pObj, i )
4462 if ( Gia_ObjFaninId0p(p, pObj) > 0 )
4463 Vec_IntPush( vXors, Gia_ObjFaninId0p(p, pObj) );
4464 }
4465 // order by support size
4466 Gia_ManDupDemiterOrderXors( p, vXors );
4467 //Vec_IntPrint( vXors );
4468 Vec_IntReverseOrder( vXors ); // from MSB to LSB
4469 // divide into groups
4470 Gia_ManCleanMark01(p);
4471 vPart[0] = Vec_IntAlloc( 100 );
4472 vPart[1] = Vec_IntAlloc( 100 );
4473 Gia_ManForEachObjVec( vXors, p, pObj, i )
4474 {
4475 int fCompl = 0;
4476 if ( !Gia_ObjRecognizeExor(pObj, &pFan[0], &pFan[1]) )
4477 pFan[0] = pObj, pFan[1] = Gia_ManConst0(p), Count1++;
4478 else
4479 {
4480 fCompl ^= Gia_IsComplement(pFan[0]);
4481 fCompl ^= Gia_IsComplement(pFan[1]);
4482 pFan[0] = Gia_Regular(pFan[0]);
4483 pFan[1] = Gia_Regular(pFan[1]);
4484 }
4485 fFlip = Gia_ManDecideWhereToAdd( p, vPart, pFan );
4486 Vec_IntPush( vPart[0], Gia_ObjId(p, pFan[fFlip]) );
4487 Vec_IntPush( vPart[1], Gia_ObjId(p, pFan[!fFlip]) );
4488 Gia_ManSetMark0Dfs_rec( p, Gia_ObjId(p, pFan[fFlip]) );
4489 Gia_ManSetMark1Dfs_rec( p, Gia_ObjId(p, pFan[!fFlip]) );
4490 }
4491 //printf( "Detected %d single-output XOR miters and %d other miters.\n", Vec_IntSize(vXors) - Count1, Count1 );
4492 Vec_IntFree( vXors );
4493 Gia_ManCleanMark01(p);
4494 // create new order
4495 vOrder = Vec_IntAlloc( 100 );
4496 Vec_IntForEachEntryTwo( vPart[0], vPart[1], iObj, iObj2, i )
4497 Vec_IntPushTwo( vOrder, iObj, iObj2 );
4498 Vec_IntFree( vPart[0] );
4499 Vec_IntFree( vPart[1] );
4500 Vec_IntReverseOrder( vOrder ); // from LSB to MSB
4501 //Vec_IntPrint( vOrder );
4502 return vOrder;
4503 }
Gia_ManDemiterToDual(Gia_Man_t * p)4504 Gia_Man_t * Gia_ManDemiterToDual( Gia_Man_t * p )
4505 {
4506 Gia_Man_t * pNew; Gia_Obj_t * pObj; int i;
4507 Vec_Int_t * vNodes;
4508 Vec_Int_t * vOrder = Gia_ManCollectTopXors( p );
4509 if ( vOrder == NULL )
4510 {
4511 printf( "Cannot demiter because the top-most gate is an AND-gate.\n" );
4512 return NULL;
4513 }
4514 assert( Vec_IntSize(vOrder) % 2 == 0 );
4515 vNodes = Vec_IntAlloc( Gia_ManObjNum(p) );
4516 Gia_ManIncrementTravId( p );
4517 Gia_ManCollectAnds( p, Vec_IntArray(vOrder), Vec_IntSize(vOrder), vNodes, NULL );
4518 pNew = Gia_ManStart( 1 + Gia_ManCiNum(p) + Vec_IntSize(vNodes) + Vec_IntSize(vOrder) );
4519 pNew->pName = Abc_UtilStrsav( p->pName );
4520 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
4521 Gia_ManConst0(p)->Value = 0;
4522 Gia_ManForEachCi( p, pObj, i )
4523 pObj->Value = Gia_ManAppendCi( pNew );
4524 Gia_ManForEachObjVec( vNodes, p, pObj, i )
4525 pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
4526 pObj = Gia_ManCo(p, 0);
4527 if ( Gia_ObjFanin0(pObj) == Gia_ManConst0(p) )
4528 {
4529 Gia_ManAppendCo( pNew, 0 );
4530 Gia_ManAppendCo( pNew, Gia_ObjFaninC0(pObj) );
4531 }
4532 else
4533 {
4534 Gia_ManSetPhase( p );
4535 Gia_ManForEachObjVec( vOrder, p, pObj, i )
4536 Gia_ManAppendCo( pNew, Abc_LitNotCond(pObj->Value, pObj->fPhase) );
4537 }
4538 Vec_IntFree( vNodes );
4539 Vec_IntFree( vOrder );
4540 return pNew;
4541 }
4542
4543 /**Function*************************************************************
4544
4545 Synopsis [Collect nodes reachable from odd/even outputs.]
4546
4547 Description []
4548
4549 SideEffects []
4550
4551 SeeAlso []
4552
4553 ***********************************************************************/
Gia_ManCollectDfs_rec(Gia_Man_t * p,int iObj,Vec_Int_t * vNodes)4554 void Gia_ManCollectDfs_rec( Gia_Man_t * p, int iObj, Vec_Int_t * vNodes )
4555 {
4556 Gia_Obj_t * pObj;
4557 if ( Gia_ObjIsTravIdCurrentId(p, iObj) )
4558 return;
4559 Gia_ObjSetTravIdCurrentId(p, iObj);
4560 pObj = Gia_ManObj( p, iObj );
4561 if ( !Gia_ObjIsAnd(pObj) )
4562 return;
4563 Gia_ManCollectDfs_rec( p, Gia_ObjFaninId0(pObj, iObj), vNodes );
4564 Gia_ManCollectDfs_rec( p, Gia_ObjFaninId1(pObj, iObj), vNodes );
4565 Vec_IntPush( vNodes, iObj );
4566 }
Gia_ManCollectReach(Gia_Man_t * p,int fOdd)4567 Vec_Int_t * Gia_ManCollectReach( Gia_Man_t * p, int fOdd )
4568 {
4569 int i, iDriver;
4570 Vec_Int_t * vNodes = Vec_IntAlloc( Gia_ManObjNum(p) );
4571 Gia_ManIncrementTravId( p );
4572 Gia_ObjSetTravIdCurrent( p, Gia_ManConst0(p) );
4573 Gia_ManForEachCoDriverId( p, iDriver, i )
4574 if ( (i & 1) == fOdd )
4575 Gia_ManCollectDfs_rec( p, iDriver, vNodes );
4576 return vNodes;
4577 }
Gia_ManDemiterDual(Gia_Man_t * p,Gia_Man_t ** pp0,Gia_Man_t ** pp1)4578 int Gia_ManDemiterDual( Gia_Man_t * p, Gia_Man_t ** pp0, Gia_Man_t ** pp1 )
4579 {
4580 Gia_Obj_t * pObj;
4581 int i, fOdd;
4582 assert( Gia_ManRegNum(p) == 0 );
4583 assert( Gia_ManCoNum(p) % 2 == 0 );
4584 *pp0 = *pp1 = NULL;
4585 for ( fOdd = 0; fOdd < 2; fOdd++ )
4586 {
4587 Vec_Int_t * vNodes = Gia_ManCollectReach( p, fOdd );
4588 Gia_Man_t * pNew = Gia_ManStart( 1 + Gia_ManCiNum(p) + Vec_IntSize(vNodes) + Gia_ManCoNum(p)/2 );
4589 pNew->pName = Abc_UtilStrsav( p->pName );
4590 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
4591 Gia_ManConst0(p)->Value = 0;
4592 Gia_ManForEachPi( p, pObj, i )
4593 pObj->Value = Gia_ManAppendCi( pNew );
4594 Gia_ManForEachObjVec( vNodes, p, pObj, i )
4595 pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
4596 Gia_ManForEachCo( p, pObj, i )
4597 if ( (i & 1) == fOdd )
4598 Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
4599 Vec_IntFree( vNodes );
4600 if ( fOdd )
4601 *pp1 = pNew;
4602 else
4603 *pp0 = pNew;
4604 }
4605 return 1;
4606 }
4607
4608 /**Function*************************************************************
4609
4610 Synopsis [Collect nodes reachable from first/second half of outputs.]
4611
4612 Description []
4613
4614 SideEffects []
4615
4616 SeeAlso []
4617
4618 ***********************************************************************/
Gia_ManCollectReach2(Gia_Man_t * p,int fSecond)4619 Vec_Int_t * Gia_ManCollectReach2( Gia_Man_t * p, int fSecond )
4620 {
4621 int i, iDriver;
4622 Vec_Int_t * vNodes = Vec_IntAlloc( Gia_ManObjNum(p) );
4623 Gia_ManIncrementTravId( p );
4624 Gia_ObjSetTravIdCurrent( p, Gia_ManConst0(p) );
4625 Gia_ManForEachCoDriverId( p, iDriver, i )
4626 if ( (i < Gia_ManCoNum(p)/2) ^ fSecond )
4627 Gia_ManCollectDfs_rec( p, iDriver, vNodes );
4628 return vNodes;
4629 }
Gia_ManDemiterTwoWords(Gia_Man_t * p,Gia_Man_t ** pp0,Gia_Man_t ** pp1)4630 int Gia_ManDemiterTwoWords( Gia_Man_t * p, Gia_Man_t ** pp0, Gia_Man_t ** pp1 )
4631 {
4632 Gia_Obj_t * pObj;
4633 int i, fSecond;
4634 assert( Gia_ManRegNum(p) == 0 );
4635 assert( Gia_ManCoNum(p) % 2 == 0 );
4636 *pp0 = *pp1 = NULL;
4637 for ( fSecond = 0; fSecond < 2; fSecond++ )
4638 {
4639 Vec_Int_t * vNodes = Gia_ManCollectReach2( p, fSecond );
4640 Gia_Man_t * pNew = Gia_ManStart( 1 + Gia_ManCiNum(p) + Vec_IntSize(vNodes) + Gia_ManCoNum(p)/2 );
4641 pNew->pName = Abc_UtilStrsav( p->pName );
4642 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
4643 Gia_ManConst0(p)->Value = 0;
4644 Gia_ManForEachPi( p, pObj, i )
4645 pObj->Value = Gia_ManAppendCi( pNew );
4646 Gia_ManForEachObjVec( vNodes, p, pObj, i )
4647 pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
4648 Gia_ManForEachCo( p, pObj, i )
4649 if ( (i < Gia_ManCoNum(p)/2) ^ fSecond )
4650 Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
4651 Vec_IntFree( vNodes );
4652 if ( fSecond )
4653 *pp1 = pNew;
4654 else
4655 *pp0 = pNew;
4656 }
4657 return 1;
4658 }
4659
4660
4661
4662 /**Function*************************************************************
4663
4664 Synopsis [Extracts "half" of the sequential AIG.]
4665
4666 Description []
4667
4668 SideEffects []
4669
4670 SeeAlso []
4671
4672 ***********************************************************************/
Gia_ManDupHalfSeq(Gia_Man_t * p,int fSecond)4673 Gia_Man_t * Gia_ManDupHalfSeq( Gia_Man_t * p, int fSecond )
4674 {
4675 int i; Gia_Obj_t * pObj;
4676 Gia_Man_t * pNew = Gia_ManStart( Gia_ManObjNum(p) );
4677 pNew->pName = Abc_UtilStrsav( p->pName );
4678 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
4679 Gia_ManFillValue(p);
4680 Gia_ManConst0(p)->Value = 0;
4681 if ( fSecond )
4682 {
4683 Gia_ManForEachCi( p, pObj, i )
4684 pObj->Value = Gia_ManAppendCi( pNew );
4685 Gia_ManForEachPo( p, pObj, i )
4686 Gia_ManDupOrderDfs_rec( pNew, p, pObj );
4687 Gia_ManForEachRi( p, pObj, i )
4688 if ( i >= Gia_ManRegNum(p)/2 )
4689 Gia_ManDupOrderDfs_rec( pNew, p, pObj );
4690 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p)- Gia_ManRegNum(p)/2 );
4691 }
4692 else
4693 {
4694 Gia_ManForEachPi( p, pObj, i )
4695 pObj->Value = Gia_ManAppendCi( pNew );
4696 Gia_ManForEachRo( p, pObj, i )
4697 if ( i >= Gia_ManRegNum(p)/2 )
4698 pObj->Value = Gia_ManAppendCi( pNew );
4699 Gia_ManForEachRo( p, pObj, i )
4700 if ( i < Gia_ManRegNum(p)/2 )
4701 pObj->Value = Gia_ManAppendCi( pNew );
4702 Gia_ManForEachPo( p, pObj, i )
4703 Gia_ManDupOrderDfs_rec( pNew, p, pObj );
4704 Gia_ManForEachRi( p, pObj, i )
4705 if ( i < Gia_ManRegNum(p)/2 )
4706 Gia_ManDupOrderDfs_rec( pNew, p, pObj );
4707 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p)/2 );
4708 }
4709 return pNew;
4710 }
4711
4712 /**Function*************************************************************
4713
4714 Synopsis [Merge two sets of sequential equivalences.]
4715
4716 Description []
4717
4718 SideEffects []
4719
4720 SeeAlso []
4721
4722 ***********************************************************************/
Gia_ManSeqEquivMerge(Gia_Man_t * p,Gia_Man_t * pPart[2])4723 void Gia_ManSeqEquivMerge( Gia_Man_t * p, Gia_Man_t * pPart[2] )
4724 {
4725 int i, iObj, * pClasses = ABC_FALLOC( int, Gia_ManObjNum(p) );
4726 int n, Repr, * pClass2Repr = ABC_FALLOC( int, Gia_ManObjNum(p) );
4727 // initialize equiv class representation in the big AIG
4728 assert( p->pReprs == NULL && p->pNexts == NULL );
4729 p->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) );
4730 for ( i = 0; i < Gia_ManObjNum(p); i++ )
4731 Gia_ObjSetRepr( p, i, GIA_VOID );
4732 // map equivalences of p into classes
4733 pClasses[0] = 0;
4734 for ( n = 0; n < 2; n++ )
4735 {
4736 assert( pPart[n]->pReprs != NULL && pPart[n]->pNexts != NULL );
4737 for ( i = 0; i < Gia_ManObjNum(pPart[n]); i++ )
4738 if ( Gia_ObjRepr(pPart[n], i) == 0 )
4739 pClasses[Gia_ManObj(pPart[n], i)->Value] = 0;
4740 Gia_ManForEachClass( pPart[n], i )
4741 {
4742 Repr = Gia_ManObj(pPart[n], i)->Value;
4743 if ( n == 1 )
4744 {
4745 Gia_ClassForEachObj( pPart[n], i, iObj )
4746 if ( pClasses[Gia_ManObj(pPart[n], iObj)->Value] != -1 )
4747 Repr = pClasses[Gia_ManObj(pPart[n], iObj)->Value];
4748 }
4749 Gia_ClassForEachObj( pPart[n], i, iObj )
4750 pClasses[Gia_ManObj(pPart[n], iObj)->Value] = Repr;
4751 }
4752 }
4753 // map representatives of each class
4754 for ( i = 0; i < Gia_ManObjNum(p); i++ )
4755 if ( pClasses[i] != -1 && pClass2Repr[pClasses[i]] == -1 )
4756 {
4757 pClass2Repr[pClasses[i]] = i;
4758 pClasses[i] = -1;
4759 }
4760 // remap the remaining classes
4761 for ( i = 0; i < Gia_ManObjNum(p); i++ )
4762 if ( pClasses[i] != -1 )
4763 p->pReprs[i].iRepr = pClass2Repr[pClasses[i]];
4764 ABC_FREE(pClasses);
4765 ABC_FREE(pClass2Repr);
4766 // create next pointers
4767 p->pNexts = Gia_ManDeriveNexts( p );
4768 }
4769
4770 /**Function*************************************************************
4771
4772 Synopsis [Print equivalences.]
4773
4774 Description []
4775
4776 SideEffects []
4777
4778 SeeAlso []
4779
4780 ***********************************************************************/
Gia_ManPrintEquivs(Gia_Man_t * p)4781 void Gia_ManPrintEquivs( Gia_Man_t * p )
4782 {
4783 Gia_Obj_t * pObj; int i, iObj;
4784 printf( "Const0:" );
4785 Gia_ManForEachAnd( p, pObj, i )
4786 if ( Gia_ObjRepr(p, i) == 0 )
4787 printf( " %d", i );
4788 printf( "\n" );
4789 Gia_ManForEachClass( p, i )
4790 {
4791 printf( "%d:", i );
4792 Gia_ClassForEachObj1( p, i, iObj )
4793 printf( " %d", iObj );
4794 printf( "\n" );
4795 }
4796 }
4797
4798 /**Function*************************************************************
4799
4800 Synopsis [Computing seq equivs by dividing AIG into two parts.]
4801
4802 Description []
4803
4804 SideEffects []
4805
4806 SeeAlso []
4807
4808 ***********************************************************************/
Gia_ManSeqEquivDivide(Gia_Man_t * p,Cec_ParCor_t * pPars)4809 void Gia_ManSeqEquivDivide( Gia_Man_t * p, Cec_ParCor_t * pPars )
4810 {
4811 Gia_Man_t * pParts[2];
4812 Gia_Obj_t * pObj;
4813 int n, i;
4814 for ( n = 0; n < 2; n++ )
4815 {
4816 // derive n-th part of the AIG
4817 pParts[n] = Gia_ManDupHalfSeq( p, n );
4818 //Gia_ManPrintStats( pParts[n], NULL );
4819 // compute equivalences (recorded internally using pReprs and pNexts)
4820 Cec_ManLSCorrespondenceClasses( pParts[n], pPars );
4821 // make the nodes of the part AIG point to their prototypes in the AIG
4822 Gia_ManForEachObj( p, pObj, i )
4823 if ( ~pObj->Value )
4824 Gia_ManObj( pParts[n], Abc_Lit2Var(pObj->Value) )->Value = i;
4825 }
4826 Gia_ManSeqEquivMerge( p, pParts );
4827 Gia_ManStop( pParts[0] );
4828 Gia_ManStop( pParts[1] );
4829 }
Gia_ManScorrDivideTest(Gia_Man_t * p,Cec_ParCor_t * pPars)4830 Gia_Man_t * Gia_ManScorrDivideTest( Gia_Man_t * p, Cec_ParCor_t * pPars )
4831 {
4832 extern Gia_Man_t * Gia_ManCorrReduce( Gia_Man_t * p );
4833 Gia_Man_t * pNew, * pTemp;
4834 ABC_FREE( p->pReprs ); p->pReprs = NULL;
4835 ABC_FREE( p->pNexts ); p->pNexts = NULL;
4836 Gia_ManSeqEquivDivide( p, pPars );
4837 //Gia_ManPrintEquivs( p );
4838 pNew = Gia_ManCorrReduce( p );
4839 pNew = Gia_ManSeqCleanup( pTemp = pNew );
4840 Gia_ManStop( pTemp );
4841 return pNew;
4842 }
4843
4844 /**Function*************************************************************
4845
4846 Synopsis [Duplicate AIG by creating a cut between logic fed by PIs]
4847
4848 Description []
4849
4850 SideEffects []
4851
4852 SeeAlso []
4853
4854 ***********************************************************************/
Gia_ManHighLightFlopLogic(Gia_Man_t * p)4855 void Gia_ManHighLightFlopLogic( Gia_Man_t * p )
4856 {
4857 Gia_Obj_t * pObj; int i;
4858 Gia_ManForEachPi( p, pObj, i )
4859 pObj->fMark0 = 0;
4860 Gia_ManForEachRo( p, pObj, i )
4861 pObj->fMark0 = 1;
4862 Gia_ManForEachAnd( p, pObj, i )
4863 pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 | Gia_ObjFanin1(pObj)->fMark0;
4864 Gia_ManForEachCo( p, pObj, i )
4865 pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0;
4866 }
Gia_ManDupReplaceCut(Gia_Man_t * p)4867 Gia_Man_t * Gia_ManDupReplaceCut( Gia_Man_t * p )
4868 {
4869 Gia_Man_t * pNew; int i;
4870 Gia_Obj_t * pObj, * pFanin;
4871 Gia_ManHighLightFlopLogic( p );
4872 pNew = Gia_ManStart( Gia_ManObjNum(p) );
4873 pNew->pName = Abc_UtilStrsav( p->pName );
4874 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
4875 // create PIs for nodes pointed to from above the cut
4876 Gia_ManFillValue( p );
4877 Gia_ManConst0(p)->Value = 0;
4878 Gia_ManForEachAnd( p, pObj, i )
4879 {
4880 if ( !pObj->fMark0 )
4881 continue;
4882 pFanin = Gia_ObjFanin0(pObj);
4883 if ( !pFanin->fMark0 && !~pFanin->Value )
4884 pFanin->Value = Gia_ManAppendCi(pNew);
4885 pFanin = Gia_ObjFanin1(pObj);
4886 if ( !pFanin->fMark0 && !~pFanin->Value )
4887 pFanin->Value = Gia_ManAppendCi(pNew);
4888 }
4889 // create flop outputs
4890 Gia_ManForEachRo( p, pObj, i )
4891 pObj->Value = Gia_ManAppendCi(pNew);
4892 // create internal nodes
4893 Gia_ManForEachCo( p, pObj, i )
4894 Gia_ManDupOrderDfs_rec( pNew, p, pObj );
4895 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
4896 Gia_ManCleanMark0( p );
4897 return pNew;
4898 }
4899
4900 ////////////////////////////////////////////////////////////////////////
4901 /// END OF FILE ///
4902 ////////////////////////////////////////////////////////////////////////
4903
4904
4905 ABC_NAMESPACE_IMPL_END
4906
4907