ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
saigMiter.c
Go to the documentation of this file.
1
20
21#include "saig.h"
22#include "proof/fra/fra.h"
23
24ABC_NAMESPACE_IMPL_START
25
26
30
34
46Sec_MtrStatus_t Sec_MiterStatus( Aig_Man_t * p )
47{
48 Sec_MtrStatus_t Status;
49 Aig_Obj_t * pObj, * pChild;
50 int i;
51 memset( &Status, 0, sizeof(Sec_MtrStatus_t) );
52 Status.iOut = -1;
53 Status.nInputs = Saig_ManPiNum( p );
54 Status.nNodes = Aig_ManNodeNum( p );
55 Status.nOutputs = Saig_ManPoNum(p);
56 Saig_ManForEachPo( p, pObj, i )
57 {
58 pChild = Aig_ObjChild0(pObj);
59 // check if the output is constant 0
60 if ( pChild == Aig_ManConst0(p) )
61 Status.nUnsat++;
62 // check if the output is constant 1
63 else if ( pChild == Aig_ManConst1(p) )
64 {
65 Status.nSat++;
66 if ( Status.iOut == -1 )
67 Status.iOut = i;
68 }
69 // check if the output is a primary input
70 else if ( Saig_ObjIsPi(p, Aig_Regular(pChild)) )
71 {
72 Status.nSat++;
73 if ( Status.iOut == -1 )
74 Status.iOut = i;
75 }
76 // check if the output is 1 for the 0000 pattern
77 else if ( Aig_Regular(pChild)->fPhase != (unsigned)Aig_IsComplement(pChild) )
78 {
79 Status.nSat++;
80 if ( Status.iOut == -1 )
81 Status.iOut = i;
82 }
83 else
84 Status.nUndec++;
85 }
86 return Status;
87}
88
100Aig_Man_t * Saig_ManCreateMiter( Aig_Man_t * p0, Aig_Man_t * p1, int Oper )
101{
102 Aig_Man_t * pNew;
103 Aig_Obj_t * pObj;
104 int i;
105 assert( Saig_ManRegNum(p0) > 0 || Saig_ManRegNum(p1) > 0 );
106 assert( Saig_ManPiNum(p0) == Saig_ManPiNum(p1) );
107 assert( Saig_ManPoNum(p0) == Saig_ManPoNum(p1) );
108 pNew = Aig_ManStart( Aig_ManObjNumMax(p0) + Aig_ManObjNumMax(p1) );
109 pNew->pName = Abc_UtilStrsav( "miter" );
110 Aig_ManCleanData( p0 );
111 Aig_ManCleanData( p1 );
112 // map constant nodes
113 Aig_ManConst1(p0)->pData = Aig_ManConst1(pNew);
114 Aig_ManConst1(p1)->pData = Aig_ManConst1(pNew);
115 // map primary inputs
116 Saig_ManForEachPi( p0, pObj, i )
117 pObj->pData = Aig_ObjCreateCi( pNew );
118 Saig_ManForEachPi( p1, pObj, i )
119 pObj->pData = Aig_ManCi( pNew, i );
120 // map register outputs
121 Saig_ManForEachLo( p0, pObj, i )
122 pObj->pData = Aig_ObjCreateCi( pNew );
123 Saig_ManForEachLo( p1, pObj, i )
124 pObj->pData = Aig_ObjCreateCi( pNew );
125 // map internal nodes
126 Aig_ManForEachNode( p0, pObj, i )
127 pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
128 Aig_ManForEachNode( p1, pObj, i )
129 pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
130 // create primary outputs
131 Saig_ManForEachPo( p0, pObj, i )
132 {
133 if ( Oper == 0 ) // XOR
134 pObj = Aig_Exor( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild0Copy(Aig_ManCo(p1,i)) );
135 else if ( Oper == 1 ) // implication is PO(p0) -> PO(p1) ... complement is PO(p0) & !PO(p1)
136 pObj = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_Not(Aig_ObjChild0Copy(Aig_ManCo(p1,i))) );
137 else
138 assert( 0 );
139 Aig_ObjCreateCo( pNew, pObj );
140 }
141 // create register inputs
142 Saig_ManForEachLi( p0, pObj, i )
143 pObj->pData = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
144 Saig_ManForEachLi( p1, pObj, i )
145 pObj->pData = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
146 // cleanup
147 Aig_ManSetRegNum( pNew, Saig_ManRegNum(p0) + Saig_ManRegNum(p1) );
148// Aig_ManCleanup( pNew );
149 return pNew;
150}
151
163Aig_Man_t * Saig_ManCreateMiterComb( Aig_Man_t * p0, Aig_Man_t * p1, int Oper )
164{
165 Aig_Man_t * pNew;
166 Aig_Obj_t * pObj;
167 int i;
168 assert( Aig_ManCiNum(p0) == Aig_ManCiNum(p1) );
169 assert( Aig_ManCoNum(p0) == Aig_ManCoNum(p1) );
170 pNew = Aig_ManStart( Aig_ManObjNumMax(p0) + Aig_ManObjNumMax(p1) );
171 pNew->pName = Abc_UtilStrsav( "miter" );
172 // map constant nodes
173 Aig_ManConst1(p0)->pData = Aig_ManConst1(pNew);
174 Aig_ManConst1(p1)->pData = Aig_ManConst1(pNew);
175 // map primary inputs and register outputs
176 Aig_ManForEachCi( p0, pObj, i )
177 pObj->pData = Aig_ObjCreateCi( pNew );
178 Aig_ManForEachCi( p1, pObj, i )
179 pObj->pData = Aig_ManCi( pNew, i );
180 // map internal nodes
181 Aig_ManForEachNode( p0, pObj, i )
182 pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
183 Aig_ManForEachNode( p1, pObj, i )
184 pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
185 // create primary outputs
186 Aig_ManForEachCo( p0, pObj, i )
187 {
188 if ( Oper == 0 ) // XOR
189 pObj = Aig_Exor( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild0Copy(Aig_ManCo(p1,i)) );
190 else if ( Oper == 1 ) // implication is PO(p0) -> PO(p1) ... complement is PO(p0) & !PO(p1)
191 pObj = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_Not(Aig_ObjChild0Copy(Aig_ManCo(p1,i))) );
192 else
193 assert( 0 );
194 Aig_ObjCreateCo( pNew, pObj );
195 }
196 // cleanup
197 Aig_ManSetRegNum( pNew, 0 );
198 Aig_ManCleanup( pNew );
199 return pNew;
200}
201
213void Saig_AndDualRail( Aig_Man_t * pNew, Aig_Obj_t * pObj, Aig_Obj_t ** ppData, Aig_Obj_t ** ppNext )
214{
215 Aig_Obj_t * pFanin0 = Aig_ObjFanin0(pObj);
216 Aig_Obj_t * pFanin1 = Aig_ObjFanin1(pObj);
217 Aig_Obj_t * p0Data = Aig_ObjFaninC0(pObj)? pFanin0->pNext : (Aig_Obj_t *)pFanin0->pData;
218 Aig_Obj_t * p0Next = Aig_ObjFaninC0(pObj)? (Aig_Obj_t *)pFanin0->pData : pFanin0->pNext;
219 Aig_Obj_t * p1Data = Aig_ObjFaninC1(pObj)? pFanin1->pNext : (Aig_Obj_t *)pFanin1->pData;
220 Aig_Obj_t * p1Next = Aig_ObjFaninC1(pObj)? (Aig_Obj_t *)pFanin1->pData : pFanin1->pNext;
221 *ppData = Aig_Or( pNew,
222 Aig_And(pNew, p0Data, Aig_Not(p0Next)),
223 Aig_And(pNew, p1Data, Aig_Not(p1Next)) );
224 *ppNext = Aig_And( pNew,
225 Aig_And(pNew, Aig_Not(p0Data), p0Next),
226 Aig_And(pNew, Aig_Not(p1Data), p1Next) );
227}
228
240Aig_Man_t * Saig_ManDualRail( Aig_Man_t * p, int fMiter )
241{
242 Aig_Man_t * pNew;
243 Aig_Obj_t * pObj, * pMiter;
244 int i;
245 Aig_ManCleanData( p );
246 Aig_ManCleanNext( p );
247 // create the new manager
248 pNew = Aig_ManStart( 4*Aig_ManObjNumMax(p) );
249 pNew->pName = Abc_UtilStrsav( p->pName );
250 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
251 // create the PIs
252 Aig_ManConst1(p)->pData = Aig_ManConst0(pNew);
253 Aig_ManConst1(p)->pNext = Aig_ManConst1(pNew);
254 Aig_ManForEachCi( p, pObj, i )
255 {
256 pObj->pData = Aig_ObjCreateCi( pNew );
257 pObj->pNext = Aig_ObjCreateCi( pNew );
258 }
259 // duplicate internal nodes
260 Aig_ManForEachNode( p, pObj, i )
261 Saig_AndDualRail( pNew, pObj, (Aig_Obj_t **)&pObj->pData, &pObj->pNext );
262 // add the POs
263 if ( fMiter )
264 {
265 pMiter = Aig_ManConst1(pNew);
266 Saig_ManForEachLo( p, pObj, i )
267 {
268 pMiter = Aig_And( pNew, pMiter,
269 Aig_Or(pNew, (Aig_Obj_t *)pObj->pData, pObj->pNext) );
270 }
271 Aig_ObjCreateCo( pNew, pMiter );
272 Saig_ManForEachLi( p, pObj, i )
273 {
274 if ( !Aig_ObjFaninC0(pObj) )
275 {
276 Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData );
277 Aig_ObjCreateCo( pNew, Aig_ObjFanin0(pObj)->pNext );
278 }
279 else
280 {
281 Aig_ObjCreateCo( pNew, Aig_ObjFanin0(pObj)->pNext );
282 Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData );
283 }
284 }
285 }
286 else
287 {
288 Aig_ManForEachCo( p, pObj, i )
289 {
290 if ( !Aig_ObjFaninC0(pObj) )
291 {
292 Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData );
293 Aig_ObjCreateCo( pNew, Aig_ObjFanin0(pObj)->pNext );
294 }
295 else
296 {
297 Aig_ObjCreateCo( pNew, Aig_ObjFanin0(pObj)->pNext );
298 Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData );
299 }
300 }
301 }
302 Aig_ManSetRegNum( pNew, 2*Aig_ManRegNum(p) );
303 Aig_ManCleanData( p );
304 Aig_ManCleanNext( p );
305 Aig_ManCleanup( pNew );
306 // check the resulting network
307 if ( !Aig_ManCheck(pNew) )
308 printf( "Aig_ManDupSimple(): The check has failed.\n" );
309 return pNew;
310}
311
323Aig_Man_t * Saig_ManUnrollTwo( Aig_Man_t * pBot, Aig_Man_t * pTop, int nFrames )
324{
325 Aig_Man_t * p, * pAig;
326 Aig_Obj_t * pObj, * pObjLi, * pObjLo;
327 int i, f;
328// assert( nFrames > 1 );
329 assert( Saig_ManPiNum(pBot) == Saig_ManPiNum(pTop) );
330 assert( Saig_ManPoNum(pBot) == Saig_ManPoNum(pTop) );
331 assert( Saig_ManRegNum(pBot) == Saig_ManRegNum(pTop) );
332 assert( Saig_ManRegNum(pBot) > 0 || Saig_ManRegNum(pTop) > 0 );
333 // start timeframes
334 p = Aig_ManStart( nFrames * Abc_MaxInt(Aig_ManObjNumMax(pBot), Aig_ManObjNumMax(pTop)) );
335 p->pName = Abc_UtilStrsav( "frames" );
336 // create variables for register outputs
337 pAig = pBot;
338 Saig_ManForEachLo( pAig, pObj, i )
339 pObj->pData = Aig_ObjCreateCi( p );
340 // add timeframes
341 for ( f = 0; f < nFrames; f++ )
342 {
343 // create PI nodes for this frame
344 Aig_ManConst1(pAig)->pData = Aig_ManConst1( p );
345 Saig_ManForEachPi( pAig, pObj, i )
346 pObj->pData = Aig_ObjCreateCi( p );
347 // add internal nodes of this frame
348 Aig_ManForEachNode( pAig, pObj, i )
349 pObj->pData = Aig_And( p, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
350 if ( f == nFrames - 1 )
351 {
352 // create POs for this frame
353 Aig_ManForEachCo( pAig, pObj, i )
354 Aig_ObjCreateCo( p, Aig_ObjChild0Copy(pObj) );
355 break;
356 }
357 // create POs for this frame
358 Saig_ManForEachPo( pAig, pObj, i )
359 Aig_ObjCreateCo( p, Aig_ObjChild0Copy(pObj) );
360 // save register inputs
361 Saig_ManForEachLi( pAig, pObj, i )
362 pObj->pData = Aig_ObjChild0Copy(pObj);
363 // transfer to register outputs
364 Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
365 pObjLo->pData = pObjLi->pData;
366 if ( f == 0 )
367 {
368 // transfer from pOld to pNew
369 Saig_ManForEachLo( pAig, pObj, i )
370 Saig_ManLo(pTop, i)->pData = pObj->pData;
371 pAig = pTop;
372 }
373 }
374 Aig_ManCleanup( p );
375 return p;
376}
377
389Aig_Man_t * Aig_ManDupNodesAll( Aig_Man_t * p, Vec_Ptr_t * vSet )
390{
391 Aig_Man_t * pNew, * pCopy;
392 Aig_Obj_t * pObj;
393 int i;
394 pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
395 pNew->pName = Abc_UtilStrsav( p->pName );
396 Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
397 Aig_ManForEachCi( p, pObj, i )
398 pObj->pData = Aig_ObjCreateCi( pNew );
399 Aig_ManForEachNode( p, pObj, i )
400 pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
401// Saig_ManForEachPo( p, pObj, i )
402// pObj->pData = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
403 Vec_PtrForEachEntry( Aig_Obj_t *, vSet, pObj, i )
404 Aig_ObjCreateCo( pNew, Aig_NotCond((Aig_Obj_t *)Aig_Regular(pObj)->pData, Aig_IsComplement(pObj)) );
405 Saig_ManForEachLi( p, pObj, i )
406 pObj->pData = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
407 Aig_ManSetRegNum( pNew, Saig_ManRegNum(p) );
408 // cleanup and return a copy
409 Aig_ManSeqCleanup( pNew );
410 pCopy = Aig_ManDupSimpleDfs( pNew );
411 Aig_ManStop( pNew );
412 return pCopy;
413}
414
426Aig_Man_t * Aig_ManDupNodesHalf( Aig_Man_t * p, Vec_Ptr_t * vSet, int iPart )
427{
428 Aig_Man_t * pNew, * pCopy;
429 Aig_Obj_t * pObj;
430 int i;
431 Aig_ManCleanData( p );
432 pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
433 pNew->pName = Abc_UtilStrsav( p->pName );
434 Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
435 Saig_ManForEachPi( p, pObj, i )
436 pObj->pData = Aig_ObjCreateCi( pNew );
437 if ( iPart == 0 )
438 {
439 Saig_ManForEachLo( p, pObj, i )
440 if ( i < Saig_ManRegNum(p)/2 )
441 pObj->pData = Aig_ObjCreateCi( pNew );
442 }
443 else
444 {
445 Saig_ManForEachLo( p, pObj, i )
446 if ( i >= Saig_ManRegNum(p)/2 )
447 pObj->pData = Aig_ObjCreateCi( pNew );
448 }
449 Aig_ManForEachNode( p, pObj, i )
450 if ( Aig_ObjFanin0(pObj)->pData && Aig_ObjFanin1(pObj)->pData )
451 pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
452// Saig_ManForEachPo( p, pObj, i )
453// pObj->pData = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
454 Vec_PtrForEachEntry( Aig_Obj_t *, vSet, pObj, i )
455 {
456 assert( Aig_Regular(pObj)->pData != NULL );
457 Aig_ObjCreateCo( pNew, Aig_NotCond((Aig_Obj_t *)Aig_Regular(pObj)->pData, Aig_IsComplement(pObj)) );
458 }
459 if ( iPart == 0 )
460 {
461 Saig_ManForEachLi( p, pObj, i )
462 if ( i < Saig_ManRegNum(p)/2 )
463 pObj->pData = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
464 }
465 else
466 {
467 Saig_ManForEachLi( p, pObj, i )
468 if ( i >= Saig_ManRegNum(p)/2 )
469 pObj->pData = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
470 }
471 Aig_ManSetRegNum( pNew, Saig_ManRegNum(p)/2 );
472 // cleanup and return a copy
473// Aig_ManSeqCleanup( pNew );
474 Aig_ManCleanup( pNew );
475 pCopy = Aig_ManDupSimpleDfs( pNew );
476 Aig_ManStop( pNew );
477 return pCopy;
478}
479
491int Saig_ManDemiterSimple( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAig1 )
492{
493 Vec_Ptr_t * vSet0, * vSet1;
494 Aig_Obj_t * pObj, * pFanin, * pObj0, * pObj1;
495 int i, Counter = 0;
496 assert( Saig_ManRegNum(p) % 2 == 0 );
497 vSet0 = Vec_PtrAlloc( Saig_ManPoNum(p) );
498 vSet1 = Vec_PtrAlloc( Saig_ManPoNum(p) );
499 Saig_ManForEachPo( p, pObj, i )
500 {
501 pFanin = Aig_ObjFanin0(pObj);
502 if ( Aig_ObjIsConst1( pFanin ) )
503 {
504 if ( !Aig_ObjFaninC0(pObj) )
505 printf( "The output number %d of the miter is constant 1.\n", i );
506 Counter++;
507 continue;
508 }
509 if ( !Aig_ObjIsNode(pFanin) || !Aig_ObjRecognizeExor( pFanin, &pObj0, &pObj1 ) )
510 {
511 printf( "The miter cannot be demitered.\n" );
512 Vec_PtrFree( vSet0 );
513 Vec_PtrFree( vSet1 );
514 return 0;
515 }
516 if ( Aig_ObjFaninC0(pObj) )
517 pObj0 = Aig_Not(pObj0);
518
519// printf( "%d %d ", Aig_Regular(pObj0)->Id, Aig_Regular(pObj1)->Id );
520 if ( Aig_Regular(pObj0)->Id < Aig_Regular(pObj1)->Id )
521 {
522 Vec_PtrPush( vSet0, pObj0 );
523 Vec_PtrPush( vSet1, pObj1 );
524 }
525 else
526 {
527 Vec_PtrPush( vSet0, pObj1 );
528 Vec_PtrPush( vSet1, pObj0 );
529 }
530 }
531// printf( "Miter has %d constant outputs.\n", Counter );
532// printf( "\n" );
533 if ( ppAig0 )
534 {
535 *ppAig0 = Aig_ManDupNodesHalf( p, vSet0, 0 );
536 ABC_FREE( (*ppAig0)->pName );
537 (*ppAig0)->pName = Abc_UtilStrsav( "part0" );
538 }
539 if ( ppAig1 )
540 {
541 *ppAig1 = Aig_ManDupNodesHalf( p, vSet1, 1 );
542 ABC_FREE( (*ppAig1)->pName );
543 (*ppAig1)->pName = Abc_UtilStrsav( "part1" );
544 }
545 Vec_PtrFree( vSet0 );
546 Vec_PtrFree( vSet1 );
547 return 1;
548}
549
561void Saig_ManDemiterMarkPos( Aig_Man_t * p )
562{
563 Aig_Obj_t * pObj;
564 int i;
565 Aig_ManCleanMarkAB( p );
566 Saig_ManForEachLo( p, pObj, i )
567 if ( i < Saig_ManRegNum(p)/2 )
568 pObj->fMarkA = 1;
569 else
570 pObj->fMarkB = 1;
571 Aig_ManForEachNode( p, pObj, i )
572 {
573 pObj->fMarkA = Aig_ObjFanin0(pObj)->fMarkA | Aig_ObjFanin1(pObj)->fMarkA;
574 pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB | Aig_ObjFanin1(pObj)->fMarkB;
575 }
576}
577
589int Saig_ManDemiterCheckPo( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t ** ppPo0, Aig_Obj_t ** ppPo1 )
590{
591 Aig_Obj_t * pFanin, * pObj0, * pObj1, * pObjR0, * pObjR1;
592 assert( Saig_ObjIsPo(p, pObj) );
593 pFanin = Aig_ObjFanin0( pObj );
594 if ( Aig_ObjIsConst1(pFanin) )
595 {
596 if ( !Aig_ObjFaninC0(pObj) )
597 return 0;
598 *ppPo0 = Aig_ManConst0(p);
599 *ppPo1 = Aig_ManConst0(p);
600 return 1;
601 }
602 if ( !Aig_ObjIsNode(pFanin) )
603 return 0;
604 if ( !Aig_ObjRecognizeExor( pFanin, &pObj0, &pObj1 ) )
605 return 0;
606 if ( Aig_ObjFaninC0(pObj) )
607 pObj0 = Aig_Not(pObj0);
608 // make sure they can reach only one
609 pObjR0 = Aig_Regular(pObj0);
610 pObjR1 = Aig_Regular(pObj1);
611 if ( (pObjR0->fMarkA && pObjR0->fMarkB) || (pObjR1->fMarkA && pObjR1->fMarkB) ||
612 (pObjR0->fMarkA && pObjR1->fMarkA) || (pObjR0->fMarkB && pObjR1->fMarkB) )
613 return 0;
614
615 if ( pObjR1->fMarkA && !pObjR0->fMarkA )
616 {
617 *ppPo0 = pObj1;
618 *ppPo1 = pObj0;
619 }
620 else if ( pObjR0->fMarkA && !pObjR1->fMarkA )
621 {
622 *ppPo0 = pObj0;
623 *ppPo1 = pObj1;
624 }
625 else
626 {
627/*
628printf( "%d", pObjR0->fMarkA );
629printf( "%d", pObjR0->fMarkB );
630printf( ":" );
631printf( "%d", pObjR1->fMarkA );
632printf( "%d", pObjR1->fMarkB );
633printf( " " );
634*/
635 if ( Aig_Regular(pObj0)->Id < Aig_Regular(pObj1)->Id )
636 {
637 *ppPo0 = pObj0;
638 *ppPo1 = pObj1;
639 }
640 else
641 {
642 *ppPo0 = pObj1;
643 *ppPo1 = pObj0;
644 }
645 }
646 return 1;
647}
648
660int Saig_ManDemiterSimpleDiff( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAig1 )
661{
662 Vec_Ptr_t * vSet0, * vSet1;
663 Aig_Obj_t * pObj, * pObj0, * pObj1;
664 int i;
665 if ( Aig_ManRegNum(p) == 0 || (Aig_ManRegNum(p) & 1) )
666 return 0;
667 Saig_ManDemiterMarkPos( p );
668 vSet0 = Vec_PtrAlloc( Saig_ManPoNum(p) );
669 vSet1 = Vec_PtrAlloc( Saig_ManPoNum(p) );
670 Saig_ManForEachPo( p, pObj, i )
671 {
672 if ( !Saig_ManDemiterCheckPo( p, pObj, &pObj0, &pObj1 ) )
673 {
674 Vec_PtrFree( vSet0 );
675 Vec_PtrFree( vSet1 );
676 Aig_ManCleanMarkAB( p );
677 return 0;
678 }
679 Vec_PtrPush( vSet0, pObj0 );
680 Vec_PtrPush( vSet1, pObj1 );
681 }
682 // create new AIG
683 *ppAig0 = Aig_ManDupNodesHalf( p, vSet0, 0 );
684 ABC_FREE( (*ppAig0)->pName );
685 (*ppAig0)->pName = Abc_UtilStrsav( "part0" );
686 // create new AIGs
687 *ppAig1 = Aig_ManDupNodesHalf( p, vSet1, 1 );
688 ABC_FREE( (*ppAig1)->pName );
689 (*ppAig1)->pName = Abc_UtilStrsav( "part1" );
690 // cleanup
691 Vec_PtrFree( vSet0 );
692 Vec_PtrFree( vSet1 );
693 Aig_ManCleanMarkAB( p );
694 return 1;
695}
696
708int Saig_ManDemiterDual( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAig1 )
709{
710 Aig_Man_t * pTemp;
711 Aig_Obj_t * pObj;
712 int i, k;
713
714 if ( p->pFanData )
715 Aig_ManFanoutStop( p );
716
717 k = 0;
718 pTemp = Aig_ManDupSimple( p );
719 Saig_ManForEachPo( pTemp, pObj, i )
720 {
721 if ( i & 1 )
722 Aig_ObjDeletePo( pTemp, pObj );
723 else
724 Vec_PtrWriteEntry( pTemp->vCos, k++, pObj );
725 }
726 Saig_ManForEachLi( pTemp, pObj, i )
727 Vec_PtrWriteEntry( pTemp->vCos, k++, pObj );
728 Vec_PtrShrink( pTemp->vCos, k );
729 pTemp->nTruePos = k - Saig_ManRegNum(pTemp);
730 Aig_ManSeqCleanup( pTemp );
731 *ppAig0 = Aig_ManDupSimple( pTemp );
732 Aig_ManStop( pTemp );
733
734 k = 0;
735 pTemp = Aig_ManDupSimple( p );
736 Saig_ManForEachPo( pTemp, pObj, i )
737 {
738 if ( i & 1 )
739 Vec_PtrWriteEntry( pTemp->vCos, k++, pObj );
740 else
741 Aig_ObjDeletePo( pTemp, pObj );
742 }
743 Saig_ManForEachLi( pTemp, pObj, i )
744 Vec_PtrWriteEntry( pTemp->vCos, k++, pObj );
745 Vec_PtrShrink( pTemp->vCos, k );
746 pTemp->nTruePos = k - Saig_ManRegNum(pTemp);
747 Aig_ManSeqCleanup( pTemp );
748 *ppAig1 = Aig_ManDupSimple( pTemp );
749 Aig_ManStop( pTemp );
750
751 return 1;
752}
753
765int Saig_ManDemiterSimpleDiff_old( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAig1 )
766{
767 Vec_Ptr_t * vSet0, * vSet1;
768 Aig_Obj_t * pObj, * pFanin, * pObj0, * pObj1;
769 int i, Counter = 0;
770// assert( Saig_ManRegNum(p) % 2 == 0 );
771 vSet0 = Vec_PtrAlloc( Saig_ManPoNum(p) );
772 vSet1 = Vec_PtrAlloc( Saig_ManPoNum(p) );
773 Saig_ManForEachPo( p, pObj, i )
774 {
775 pFanin = Aig_ObjFanin0(pObj);
776 if ( Aig_ObjIsConst1( pFanin ) )
777 {
778 if ( !Aig_ObjFaninC0(pObj) )
779 printf( "The output number %d of the miter is constant 1.\n", i );
780 Counter++;
781 continue;
782 }
783 if ( !Aig_ObjIsNode(pFanin) || !Aig_ObjRecognizeExor( pFanin, &pObj0, &pObj1 ) )
784 {
785/*
786 printf( "The miter cannot be demitered.\n" );
787 Vec_PtrFree( vSet0 );
788 Vec_PtrFree( vSet1 );
789 return 0;
790*/
791 printf( "The output number %d cannot be demitered.\n", i );
792 continue;
793 }
794 if ( Aig_ObjFaninC0(pObj) )
795 pObj0 = Aig_Not(pObj0);
796
797// printf( "%d %d ", Aig_Regular(pObj0)->Id, Aig_Regular(pObj1)->Id );
798 if ( Aig_Regular(pObj0)->Id < Aig_Regular(pObj1)->Id )
799 {
800 Vec_PtrPush( vSet0, pObj0 );
801 Vec_PtrPush( vSet1, pObj1 );
802 }
803 else
804 {
805 Vec_PtrPush( vSet0, pObj1 );
806 Vec_PtrPush( vSet1, pObj0 );
807 }
808 }
809// printf( "Miter has %d constant outputs.\n", Counter );
810// printf( "\n" );
811 if ( ppAig0 )
812 {
813 *ppAig0 = Aig_ManDupNodesAll( p, vSet0 );
814 ABC_FREE( (*ppAig0)->pName );
815 (*ppAig0)->pName = Abc_UtilStrsav( "part0" );
816 }
817 if ( ppAig1 )
818 {
819 *ppAig1 = Aig_ManDupNodesAll( p, vSet1 );
820 ABC_FREE( (*ppAig1)->pName );
821 (*ppAig1)->pName = Abc_UtilStrsav( "part1" );
822 }
823 Vec_PtrFree( vSet0 );
824 Vec_PtrFree( vSet1 );
825 return 1;
826}
827
839void Saig_ManDemiterLabel_rec( Aig_Man_t * p, Aig_Obj_t * pObj, int Value )
840{
841 if ( Aig_ObjIsTravIdCurrent(p, pObj) )
842 return;
843 Aig_ObjSetTravIdCurrent(p, pObj);
844 if ( Value )
845 pObj->fMarkB = 1;
846 else
847 pObj->fMarkA = 1;
848 if ( Saig_ObjIsPi(p, pObj) )
849 return;
850 if ( Saig_ObjIsLo(p, pObj) )
851 {
852 Saig_ManDemiterLabel_rec( p, Aig_ObjFanin0( Saig_ObjLoToLi(p, pObj) ), Value );
853 return;
854 }
855 assert( Aig_ObjIsNode(pObj) );
856 Saig_ManDemiterLabel_rec( p, Aig_ObjFanin0(pObj), Value );
857 Saig_ManDemiterLabel_rec( p, Aig_ObjFanin1(pObj), Value );
858}
859
871Aig_Obj_t * Saig_ManGetLabeledRegister_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
872{
873 Aig_Obj_t * pResult;
874 if ( Aig_ObjIsTravIdCurrent(p, pObj) )
875 return NULL;
876 Aig_ObjSetTravIdCurrent(p, pObj);
877 if ( Saig_ObjIsPi(p, pObj) )
878 return NULL;
879 if ( Saig_ObjIsLo(p, pObj) )
880 {
881 if ( pObj->fMarkA || pObj->fMarkB )
882 return pObj;
883 return Saig_ManGetLabeledRegister_rec( p, Aig_ObjFanin0( Saig_ObjLoToLi(p, pObj) ) );
884 }
885 assert( Aig_ObjIsNode(pObj) );
886 pResult = Saig_ManGetLabeledRegister_rec( p, Aig_ObjFanin0(pObj) );
887 if ( pResult )
888 return pResult;
889 return Saig_ManGetLabeledRegister_rec( p, Aig_ObjFanin1(pObj) );
890}
891
903int Saig_ManDemiter( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAig1 )
904{
905 Vec_Ptr_t * vPairs, * vSet0, * vSet1;
906 Aig_Obj_t * pObj, * pObj0, * pObj1, * pFlop0, * pFlop1;
907 int i, Counter;
908 assert( Saig_ManRegNum(p) > 0 );
909 Aig_ManSetCioIds( p );
910 // check if demitering is possible
911 vPairs = Vec_PtrAlloc( 2 * Saig_ManPoNum(p) );
912 Saig_ManForEachPo( p, pObj, i )
913 {
914 if ( !Aig_ObjRecognizeExor( Aig_ObjFanin0(pObj), &pObj0, &pObj1 ) )
915 {
916 Vec_PtrFree( vPairs );
917 return 0;
918 }
919 Vec_PtrPush( vPairs, pObj0 );
920 Vec_PtrPush( vPairs, pObj1 );
921 }
922 // start array of outputs
923 vSet0 = Vec_PtrAlloc( Saig_ManPoNum(p) );
924 vSet1 = Vec_PtrAlloc( Saig_ManPoNum(p) );
925 // get the first pair of outputs
926 pObj0 = (Aig_Obj_t *)Vec_PtrEntry( vPairs, 0 );
927 pObj1 = (Aig_Obj_t *)Vec_PtrEntry( vPairs, 1 );
928 // label registers reachable from the outputs
929 Aig_ManIncrementTravId( p );
930 Saig_ManDemiterLabel_rec( p, Aig_Regular(pObj0), 0 );
931 Vec_PtrPush( vSet0, pObj0 );
932 Aig_ManIncrementTravId( p );
933 Saig_ManDemiterLabel_rec( p, Aig_Regular(pObj1), 1 );
934 Vec_PtrPush( vSet1, pObj1 );
935 // find where each output belongs
936 for ( i = 2; i < Vec_PtrSize(vPairs); i += 2 )
937 {
938 pObj0 = (Aig_Obj_t *)Vec_PtrEntry( vPairs, i );
939 pObj1 = (Aig_Obj_t *)Vec_PtrEntry( vPairs, i+1 );
940
941 Aig_ManIncrementTravId( p );
942 pFlop0 = Saig_ManGetLabeledRegister_rec( p, Aig_Regular(pObj0) );
943
944 Aig_ManIncrementTravId( p );
945 pFlop1 = Saig_ManGetLabeledRegister_rec( p, Aig_Regular(pObj1) );
946
947 if ( (pFlop0->fMarkA && pFlop0->fMarkB) || (pFlop1->fMarkA && pFlop1->fMarkB) ||
948 (pFlop0->fMarkA && pFlop1->fMarkA) || (pFlop0->fMarkB && pFlop1->fMarkB) )
949 printf( "Output pair %4d: Difficult case...\n", i/2 );
950
951 if ( pFlop0->fMarkB )
952 {
953 Saig_ManDemiterLabel_rec( p, pObj0, 1 );
954 Vec_PtrPush( vSet0, pObj0 );
955 }
956 else // if ( pFlop0->fMarkA ) or none
957 {
958 Saig_ManDemiterLabel_rec( p, pObj0, 0 );
959 Vec_PtrPush( vSet1, pObj0 );
960 }
961
962 if ( pFlop1->fMarkB )
963 {
964 Saig_ManDemiterLabel_rec( p, pObj1, 1 );
965 Vec_PtrPush( vSet0, pObj1 );
966 }
967 else // if ( pFlop1->fMarkA ) or none
968 {
969 Saig_ManDemiterLabel_rec( p, pObj1, 0 );
970 Vec_PtrPush( vSet1, pObj1 );
971 }
972 }
973 // check if there are any flops in common
974 Counter = 0;
975 Saig_ManForEachLo( p, pObj, i )
976 if ( pObj->fMarkA && pObj->fMarkB )
977 Counter++;
978 if ( Counter > 0 )
979 printf( "The miters contains %d flops reachable from both AIGs.\n", Counter );
980
981 // produce two miters
982 if ( ppAig0 )
983 {
984 assert( 0 );
985 *ppAig0 = Aig_ManDupNodesHalf( p, vSet0, 0 ); // not ready
986 ABC_FREE( (*ppAig0)->pName );
987 (*ppAig0)->pName = Abc_UtilStrsav( "part0" );
988 }
989 if ( ppAig1 )
990 {
991 assert( 0 );
992 *ppAig1 = Aig_ManDupNodesHalf( p, vSet1, 1 ); // not ready
993 ABC_FREE( (*ppAig1)->pName );
994 (*ppAig1)->pName = Abc_UtilStrsav( "part1" );
995 }
996 Vec_PtrFree( vSet0 );
997 Vec_PtrFree( vSet1 );
998 Vec_PtrFree( vPairs );
999 return 1;
1000}
1001
1002
1014Aig_Man_t * Saig_ManCreateMiterTwo( Aig_Man_t * pOld, Aig_Man_t * pNew, int nFrames )
1015{
1016 Aig_Man_t * pFrames0, * pFrames1, * pMiter;
1017// assert( Aig_ManNodeNum(pOld) <= Aig_ManNodeNum(pNew) );
1018 pFrames0 = Saig_ManUnrollTwo( pOld, pOld, nFrames );
1019 pFrames1 = Saig_ManUnrollTwo( pNew, pOld, nFrames );
1020 pMiter = Saig_ManCreateMiterComb( pFrames0, pFrames1, 0 );
1021 Aig_ManStop( pFrames0 );
1022 Aig_ManStop( pFrames1 );
1023 return pMiter;
1024}
1025
1026
1038int Ssw_SecCexResimulate( Aig_Man_t * p, int * pModel, int * pnOutputs )
1039{
1040 Aig_Obj_t * pObj;
1041 int i, RetValue = -1;
1042 *pnOutputs = 0;
1043 Aig_ManConst1(p)->fMarkA = 1;
1044 Aig_ManForEachCi( p, pObj, i )
1045 pObj->fMarkA = pModel[i];
1046 Aig_ManForEachNode( p, pObj, i )
1047 pObj->fMarkA = ( Aig_ObjFanin0(pObj)->fMarkA ^ Aig_ObjFaninC0(pObj) ) &
1048 ( Aig_ObjFanin1(pObj)->fMarkA ^ Aig_ObjFaninC1(pObj) );
1049 Aig_ManForEachCo( p, pObj, i )
1050 pObj->fMarkA = Aig_ObjFanin0(pObj)->fMarkA ^ Aig_ObjFaninC0(pObj);
1051 Aig_ManForEachCo( p, pObj, i )
1052 if ( pObj->fMarkA )
1053 {
1054 if ( RetValue == -1 )
1055 RetValue = i;
1056 (*pnOutputs)++;
1057 }
1058 Aig_ManCleanMarkA(p);
1059 return RetValue;
1060}
1061
1074int Ssw_SecSpecial( Aig_Man_t * pPart0, Aig_Man_t * pPart1, int nFrames, int fVerbose )
1075{
1076// extern int Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose );
1077 int iOut, nOuts;
1078 Aig_Man_t * pMiterCec;
1079 int RetValue;
1080 abctime clkTotal = Abc_Clock();
1081 if ( fVerbose )
1082 {
1083 Aig_ManPrintStats( pPart0 );
1084 Aig_ManPrintStats( pPart1 );
1085 }
1086// Aig_ManDumpBlif( pPart0, "file0.blif", NULL, NULL );
1087// Aig_ManDumpBlif( pPart1, "file1.blif", NULL, NULL );
1088// assert( Aig_ManNodeNum(pPart0) <= Aig_ManNodeNum(pPart1) );
1089/*
1090 if ( Aig_ManNodeNum(pPart0) >= Aig_ManNodeNum(pPart1) )
1091 {
1092 printf( "Warning: The design after synthesis is smaller!\n" );
1093 printf( "This warning may indicate that the order of designs is changed.\n" );
1094 printf( "The solver expects the original design as first argument and\n" );
1095 printf( "the modified design as the second argument in \"absec\".\n" );
1096 }
1097*/
1098 // create two-level miter
1099 pMiterCec = Saig_ManCreateMiterTwo( pPart0, pPart1, nFrames );
1100 if ( fVerbose )
1101 {
1102 Aig_ManPrintStats( pMiterCec );
1103// Aig_ManDumpBlif( pMiterCec, "miter01.blif", NULL, NULL );
1104// printf( "The new miter is written into file \"%s\".\n", "miter01.blif" );
1105 }
1106 // run CEC on this miter
1107 RetValue = Fra_FraigCec( &pMiterCec, 100000, fVerbose );
1108 // transfer model if given
1109// if ( pNtk2 == NULL )
1110// pNtk1->pModel = pMiterCec->pData, pMiterCec->pData = NULL;
1111 // report the miter
1112 if ( RetValue == 1 )
1113 {
1114 printf( "Networks are equivalent. " );
1115ABC_PRT( "Time", Abc_Clock() - clkTotal );
1116 }
1117 else if ( RetValue == 0 )
1118 {
1119 printf( "Networks are NOT EQUIVALENT. " );
1120ABC_PRT( "Time", Abc_Clock() - clkTotal );
1121 if ( pMiterCec->pData == NULL )
1122 printf( "Counter-example is not available.\n" );
1123 else
1124 {
1125 iOut = Ssw_SecCexResimulate( pMiterCec, (int *)pMiterCec->pData, &nOuts );
1126 if ( iOut == -1 )
1127 printf( "Counter-example verification has failed.\n" );
1128 else
1129 {
1130 if ( iOut < Saig_ManPoNum(pPart0) * nFrames )
1131 printf( "Primary output %d has failed in frame %d.\n",
1132 iOut%Saig_ManPoNum(pPart0), iOut/Saig_ManPoNum(pPart0) );
1133 else
1134 printf( "Flop input %d has failed in the last frame.\n",
1135 iOut - Saig_ManPoNum(pPart0) * nFrames );
1136 printf( "The counter-example detected %d incorrect POs or flop inputs.\n", nOuts );
1137 }
1138 }
1139 }
1140 else
1141 {
1142 printf( "Networks are UNDECIDED. " );
1143ABC_PRT( "Time", Abc_Clock() - clkTotal );
1144 }
1145 fflush( stdout );
1146 Aig_ManStop( pMiterCec );
1147 return RetValue;
1148}
1149
1161int Ssw_SecSpecialMiter( Aig_Man_t * p0, Aig_Man_t * p1, int nFrames, int fVerbose )
1162{
1163 Aig_Man_t * pPart0, * pPart1;
1164 int RetValue;
1165 if ( fVerbose )
1166 printf( "Performing sequential verification using combinational A/B miter.\n" );
1167 // consider the case when a miter is given
1168 if ( p1 == NULL )
1169 {
1170 if ( fVerbose )
1171 {
1172 Aig_ManPrintStats( p0 );
1173 }
1174 // demiter the miter
1175 if ( !Saig_ManDemiterSimpleDiff( p0, &pPart0, &pPart1 ) )
1176 {
1177 printf( "Demitering has failed.\n" );
1178 return -1;
1179 }
1180 if ( Aig_ManRegNum(pPart0) != Aig_ManRegNum(pPart1) )
1181 {
1182 Aig_ManStop( pPart0 );
1183 Aig_ManStop( pPart1 );
1184 printf( "After demitering AIGs have different number of flops. Quitting.\n" );
1185 return -1;
1186 }
1187 }
1188 else
1189 {
1190 pPart0 = Aig_ManDupSimple( p0 );
1191 pPart1 = Aig_ManDupSimple( p1 );
1192 }
1193 if ( fVerbose )
1194 {
1195// Aig_ManPrintStats( pPart0 );
1196// Aig_ManPrintStats( pPart1 );
1197 if ( p1 == NULL )
1198 {
1199// Aig_ManDumpBlif( pPart0, "part0.blif", NULL, NULL );
1200// Aig_ManDumpBlif( pPart1, "part1.blif", NULL, NULL );
1201// printf( "The result of demitering is written into files \"%s\" and \"%s\".\n", "part0.blif", "part1.blif" );
1202 }
1203 }
1204 assert( Aig_ManRegNum(pPart0) > 0 );
1205 assert( Aig_ManRegNum(pPart1) > 0 );
1206 assert( Saig_ManPiNum(pPart0) == Saig_ManPiNum(pPart1) );
1207 assert( Saig_ManPoNum(pPart0) == Saig_ManPoNum(pPart1) );
1208 assert( Aig_ManRegNum(pPart0) == Aig_ManRegNum(pPart1) );
1209 RetValue = Ssw_SecSpecial( pPart0, pPart1, nFrames, fVerbose );
1210 if ( RetValue != 1 && Aig_ManNodeNum(pPart0) >= Aig_ManNodeNum(pPart1) )
1211 RetValue = Ssw_SecSpecial( pPart1, pPart0, nFrames, fVerbose );
1212 Aig_ManStop( pPart0 );
1213 Aig_ManStop( pPart1 );
1214 return RetValue;
1215}
1216
1217
1218
1230int Saig_ManDemiterNew( Aig_Man_t * pMan )
1231{
1232 Vec_Ptr_t * vSuper, * vSupp0, * vSupp1;
1233 Aig_Obj_t * pObj, * pTemp, * pFan0, * pFan1;
1234 int i, k;
1235 vSuper = Vec_PtrAlloc( 100 );
1236 Saig_ManForEachPo( pMan, pObj, i )
1237 {
1238 if ( pMan->nConstrs && i >= Saig_ManPoNum(pMan) - pMan->nConstrs )
1239 break;
1240 printf( "Output %3d : ", i );
1241 if ( Aig_ObjIsConst1(Aig_ObjFanin0(pObj)) )
1242 {
1243 if ( !Aig_ObjFaninC0(pObj) )
1244 printf( "Const1\n" );
1245 else
1246 printf( "Const0\n" );
1247 continue;
1248 }
1249 if ( !Aig_ObjIsNode(Aig_ObjFanin0(pObj)) )
1250 {
1251 printf( "Terminal\n" );
1252 continue;
1253 }
1254 // check AND
1255 if ( !Aig_ObjFaninC0(pObj) )
1256 {
1257 printf( "AND " );
1258 if ( Aig_ObjRecognizeExor(Aig_ObjFanin0(pObj), &pFan0, &pFan1) )
1259 printf( " Yes" );
1260 else
1261 printf( " No" );
1262 printf( "\n" );
1263 continue;
1264 }
1265 // check OR
1266 Aig_ObjCollectSuper( Aig_ObjFanin0(pObj), vSuper );
1267 printf( "OR with %d inputs ", Vec_PtrSize(vSuper) );
1268 if ( Vec_PtrSize(vSuper) == 2 )
1269 {
1270 if ( Aig_ObjRecognizeExor(Aig_ObjFanin0(pObj), &pFan0, &pFan1) )
1271 {
1272 printf( " Yes" );
1273 printf( "\n" );
1274
1275 vSupp0 = Aig_Support( pMan, Aig_Regular(pFan0) );
1276 Vec_PtrForEachEntry( Aig_Obj_t *, vSupp0, pTemp, k )
1277 if ( Saig_ObjIsLo(pMan, pTemp) )
1278 printf( " %d", Aig_ObjCioId(pTemp) );
1279 printf( "\n" );
1280 Vec_PtrFree( vSupp0 );
1281
1282 vSupp1 = Aig_Support( pMan, Aig_Regular(pFan1) );
1283 Vec_PtrForEachEntry( Aig_Obj_t *, vSupp1, pTemp, k )
1284 if ( Saig_ObjIsLo(pMan, pTemp) )
1285 printf( " %d", Aig_ObjCioId(pTemp) );
1286 printf( "\n" );
1287 Vec_PtrFree( vSupp1 );
1288 }
1289 else
1290 printf( " No" );
1291 printf( "\n" );
1292 continue;
1293 }
1294/*
1295 Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pTemp, k )
1296 if ( Aig_ObjRecognizeExor(Aig_Regular(pTemp), &pFan0, &pFan1) )
1297 {
1298 printf( " Yes" );
1299 if ( Aig_IsComplement(pTemp) )
1300 pFan0 = Aig_Not(pFan0);
1301 }
1302 else
1303 printf( " No" );
1304*/
1305 printf( "\n" );
1306 }
1307 Vec_PtrFree( vSuper );
1308 return 1;
1309}
1310
1314
1315
1316ABC_NAMESPACE_IMPL_END
1317
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
ABC_PRT
#define ABC_PRT(a, t)
Definition abc_global.h:255
ABC_FREE
#define ABC_FREE(obj)
Definition abc_global.h:267
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition abc_namespaces.h:54
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition abc_namespaces.h:55
Aig_ManSeqCleanup
int Aig_ManSeqCleanup(Aig_Man_t *p)
Definition aigScl.c:158
Aig_ManSetRegNum
void Aig_ManSetRegNum(Aig_Man_t *p, int nRegs)
Definition aigMan.c:438
Aig_ManDupSimple
Aig_Man_t * Aig_ManDupSimple(Aig_Man_t *p)
DECLARATIONS ///.
Definition aigDup.c:46
Aig_ManSetCioIds
void Aig_ManSetCioIds(Aig_Man_t *p)
Definition aigUtil.c:978
Aig_ManDupSimpleDfs
Aig_Man_t * Aig_ManDupSimpleDfs(Aig_Man_t *p)
Definition aigDup.c:184
Aig_ManCleanMarkA
void Aig_ManCleanMarkA(Aig_Man_t *p)
Definition aigUtil.c:148
Aig_ObjRecognizeExor
int Aig_ObjRecognizeExor(Aig_Obj_t *pObj, Aig_Obj_t **ppFan0, Aig_Obj_t **ppFan1)
Definition aigUtil.c:343
Aig_ManFanoutStop
void Aig_ManFanoutStop(Aig_Man_t *p)
Definition aigFanout.c:89
Aig_ObjDeletePo
void Aig_ObjDeletePo(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition aigObj.c:261
Aig_ManStop
void Aig_ManStop(Aig_Man_t *p)
Definition aigMan.c:187
Aig_ManIncrementTravId
void Aig_ManIncrementTravId(Aig_Man_t *p)
DECLARATIONS ///.
Definition aigUtil.c:44
Aig_ManForEachCi
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition aig.h:393
Aig_And
Aig_Obj_t * Aig_And(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition aigOper.c:104
Aig_ObjCreateCo
Aig_Obj_t * Aig_ObjCreateCo(Aig_Man_t *p, Aig_Obj_t *pDriver)
Definition aigObj.c:66
Aig_ManCleanNext
void Aig_ManCleanNext(Aig_Man_t *p)
Definition aigUtil.c:224
Aig_ObjCollectSuper
int Aig_ObjCollectSuper(Aig_Obj_t *pObj, Vec_Ptr_t *vSuper)
Definition aigDfs.c:1111
Aig_Obj_t
struct Aig_Obj_t_ Aig_Obj_t
Definition aig.h:51
Aig_Exor
Aig_Obj_t * Aig_Exor(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition aigOper.c:220
Aig_ManStart
Aig_Man_t * Aig_ManStart(int nNodesMax)
DECLARATIONS ///.
Definition aigMan.c:47
Aig_ManPrintStats
void Aig_ManPrintStats(Aig_Man_t *p)
Definition aigMan.c:379
Aig_ManForEachNode
#define Aig_ManForEachNode(p, pObj, i)
Definition aig.h:413
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition aig.h:50
Aig_ManCleanup
int Aig_ManCleanup(Aig_Man_t *p)
Definition aigMan.c:265
Aig_ManCleanMarkAB
void Aig_ManCleanMarkAB(Aig_Man_t *p)
Definition aigUtil.c:186
Aig_ManForEachCo
#define Aig_ManForEachCo(p, pObj, i)
Definition aig.h:398
Aig_ObjCreateCi
Aig_Obj_t * Aig_ObjCreateCi(Aig_Man_t *p)
DECLARATIONS ///.
Definition aigObj.c:45
Aig_Support
Vec_Ptr_t * Aig_Support(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition aigDfs.c:846
Aig_ManCleanData
void Aig_ManCleanData(Aig_Man_t *p)
Definition aigUtil.c:205
Aig_Or
Aig_Obj_t * Aig_Or(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition aigOper.c:259
Aig_ManCheck
ABC_DLL int Aig_ManCheck(Aig_Man_t *p)
FUNCTION DECLARATIONS ///.
Definition aigCheck.c:45
p
Cube * p
Definition exorList.c:222
Fra_FraigCec
int Fra_FraigCec(Aig_Man_t **ppAig, int nConfLimit, int fVerbose)
Definition fraCec.c:320
Saig_ManDemiterDual
int Saig_ManDemiterDual(Aig_Man_t *p, Aig_Man_t **ppAig0, Aig_Man_t **ppAig1)
Definition saigMiter.c:708
Saig_AndDualRail
void Saig_AndDualRail(Aig_Man_t *pNew, Aig_Obj_t *pObj, Aig_Obj_t **ppData, Aig_Obj_t **ppNext)
Definition saigMiter.c:213
Saig_ManCreateMiterComb
Aig_Man_t * Saig_ManCreateMiterComb(Aig_Man_t *p0, Aig_Man_t *p1, int Oper)
Definition saigMiter.c:163
Ssw_SecSpecial
int Ssw_SecSpecial(Aig_Man_t *pPart0, Aig_Man_t *pPart1, int nFrames, int fVerbose)
Definition saigMiter.c:1074
Saig_ManDemiterNew
int Saig_ManDemiterNew(Aig_Man_t *pMan)
Definition saigMiter.c:1230
Saig_ManDemiter
int Saig_ManDemiter(Aig_Man_t *p, Aig_Man_t **ppAig0, Aig_Man_t **ppAig1)
Definition saigMiter.c:903
Saig_ManCreateMiter
Aig_Man_t * Saig_ManCreateMiter(Aig_Man_t *p0, Aig_Man_t *p1, int Oper)
Definition saigMiter.c:100
Saig_ManCreateMiterTwo
Aig_Man_t * Saig_ManCreateMiterTwo(Aig_Man_t *pOld, Aig_Man_t *pNew, int nFrames)
Definition saigMiter.c:1014
Aig_ManDupNodesHalf
Aig_Man_t * Aig_ManDupNodesHalf(Aig_Man_t *p, Vec_Ptr_t *vSet, int iPart)
Definition saigMiter.c:426
Saig_ManDemiterSimpleDiff_old
int Saig_ManDemiterSimpleDiff_old(Aig_Man_t *p, Aig_Man_t **ppAig0, Aig_Man_t **ppAig1)
Definition saigMiter.c:765
Aig_ManDupNodesAll
Aig_Man_t * Aig_ManDupNodesAll(Aig_Man_t *p, Vec_Ptr_t *vSet)
Definition saigMiter.c:389
Sec_MiterStatus
ABC_NAMESPACE_IMPL_START Sec_MtrStatus_t Sec_MiterStatus(Aig_Man_t *p)
DECLARATIONS ///.
Definition saigMiter.c:46
Saig_ManUnrollTwo
Aig_Man_t * Saig_ManUnrollTwo(Aig_Man_t *pBot, Aig_Man_t *pTop, int nFrames)
Definition saigMiter.c:323
Ssw_SecSpecialMiter
int Ssw_SecSpecialMiter(Aig_Man_t *p0, Aig_Man_t *p1, int nFrames, int fVerbose)
Definition saigMiter.c:1161
Saig_ManDemiterSimpleDiff
int Saig_ManDemiterSimpleDiff(Aig_Man_t *p, Aig_Man_t **ppAig0, Aig_Man_t **ppAig1)
Definition saigMiter.c:660
Saig_ManDemiterCheckPo
int Saig_ManDemiterCheckPo(Aig_Man_t *p, Aig_Obj_t *pObj, Aig_Obj_t **ppPo0, Aig_Obj_t **ppPo1)
Definition saigMiter.c:589
Saig_ManDemiterSimple
int Saig_ManDemiterSimple(Aig_Man_t *p, Aig_Man_t **ppAig0, Aig_Man_t **ppAig1)
Definition saigMiter.c:491
Saig_ManDualRail
Aig_Man_t * Saig_ManDualRail(Aig_Man_t *p, int fMiter)
Definition saigMiter.c:240
Ssw_SecCexResimulate
int Ssw_SecCexResimulate(Aig_Man_t *p, int *pModel, int *pnOutputs)
Definition saigMiter.c:1038
Saig_ManDemiterMarkPos
void Saig_ManDemiterMarkPos(Aig_Man_t *p)
Definition saigMiter.c:561
Saig_ManDemiterLabel_rec
void Saig_ManDemiterLabel_rec(Aig_Man_t *p, Aig_Obj_t *pObj, int Value)
Definition saigMiter.c:839
Saig_ManGetLabeledRegister_rec
Aig_Obj_t * Saig_ManGetLabeledRegister_rec(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition saigMiter.c:871
Saig_ManForEachLiLo
#define Saig_ManForEachLiLo(p, pObjLi, pObjLo, i)
Definition saig.h:101
Saig_ManForEachLi
#define Saig_ManForEachLi(p, pObj, i)
Definition saig.h:98
Saig_ManForEachPo
#define Saig_ManForEachPo(p, pObj, i)
Definition saig.h:93
Saig_ManForEachLo
#define Saig_ManForEachLo(p, pObj, i)
Definition saig.h:96
Saig_ManForEachPi
#define Saig_ManForEachPi(p, pObj, i)
Definition saig.h:91
Sec_MtrStatus_t
typedefABC_NAMESPACE_HEADER_START struct Sec_MtrStatus_t_ Sec_MtrStatus_t
INCLUDES ///.
Definition saig.h:41
Aig_Obj_t_::fMarkB
unsigned int fMarkB
Definition aig.h:80
Aig_Obj_t_::pNext
Aig_Obj_t * pNext
Definition aig.h:72
Aig_Obj_t_::fMarkA
unsigned int fMarkA
Definition aig.h:79
Aig_Obj_t_::pData
void * pData
Definition aig.h:87
assert
#define assert(ex)
Definition util_old.h:213
memset
char * memset()
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition vecPtr.h:55