abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
abcDar.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [abcDar.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Network and node package.]
8 
9  Synopsis [DAG-aware rewriting.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: abcDar.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "base/abc/abc.h"
22 #include "base/main/main.h"
23 #include "aig/gia/giaAig.h"
24 #include "opt/dar/dar.h"
25 #include "sat/cnf/cnf.h"
26 #include "proof/fra/fra.h"
27 #include "proof/fraig/fraig.h"
28 #include "proof/int/int.h"
29 #include "proof/dch/dch.h"
30 #include "proof/ssw/ssw.h"
31 #include "opt/cgt/cgt.h"
32 #include "proof/bbr/bbr.h"
33 #include "aig/gia/gia.h"
34 #include "proof/cec/cec.h"
35 #include "opt/csw/csw.h"
36 #include "proof/pdr/pdr.h"
37 #include "sat/bmc/bmc.h"
38 #include "map/mio/mio.h"
39 
41 
42 ////////////////////////////////////////////////////////////////////////
43 /// DECLARATIONS ///
44 ////////////////////////////////////////////////////////////////////////
45 
46 ////////////////////////////////////////////////////////////////////////
47 /// FUNCTION DEFINITIONS ///
48 ////////////////////////////////////////////////////////////////////////
49 
50 /**Function*************************************************************
51 
52  Synopsis []
53 
54  Description []
55 
56  SideEffects []
57 
58  SeeAlso []
59 
60 ***********************************************************************/
61 int Abc_ObjCompareById( Abc_Obj_t ** pp1, Abc_Obj_t ** pp2 )
62 {
63  return Abc_ObjId(Abc_ObjRegular(*pp1)) - Abc_ObjId(Abc_ObjRegular(*pp2));
64 }
65 
66 /**Function*************************************************************
67 
68  Synopsis [Collects the supergate.]
69 
70  Description []
71 
72  SideEffects []
73 
74  SeeAlso []
75 
76 ***********************************************************************/
77 void Abc_CollectTopOr_rec( Abc_Obj_t * pObj, Vec_Ptr_t * vSuper )
78 {
79  if ( Abc_ObjIsComplement(pObj) || !Abc_ObjIsNode(pObj) )
80  {
81  Vec_PtrPush( vSuper, pObj );
82  return;
83  }
84  // go through the branches
85  Abc_CollectTopOr_rec( Abc_ObjChild0(pObj), vSuper );
86  Abc_CollectTopOr_rec( Abc_ObjChild1(pObj), vSuper );
87 }
88 void Abc_CollectTopOr( Abc_Obj_t * pObj, Vec_Ptr_t * vSuper )
89 {
90  Vec_PtrClear( vSuper );
91  if ( Abc_ObjIsComplement(pObj) )
92  {
93  Abc_CollectTopOr_rec( Abc_ObjNot(pObj), vSuper );
94  Vec_PtrUniqify( vSuper, (int (*)())Abc_ObjCompareById );
95  }
96  else
97  Vec_PtrPush( vSuper, Abc_ObjNot(pObj) );
98 }
99 
100 /**Function*************************************************************
101 
102  Synopsis [Converts the network from the AIG manager into ABC.]
103 
104  Description [The returned map maps new PO IDs into old ones.]
105 
106  SideEffects []
107 
108  SeeAlso []
109 
110 ***********************************************************************/
112 {
113  Aig_Man_t * pMan;
114  Abc_Obj_t * pObj, * pTemp;
115  Vec_Ptr_t * vDrivers;
116  Vec_Ptr_t * vSuper;
117  int i, k, nDontCares;
118 
119  // print warning about initial values
120  nDontCares = 0;
121  Abc_NtkForEachLatch( pNtk, pObj, i )
122  if ( Abc_LatchIsInitDc(pObj) )
123  {
124  Abc_LatchSetInit0(pObj);
125  nDontCares++;
126  }
127  if ( nDontCares )
128  {
129  Abc_Print( 1, "Warning: %d registers in this network have don't-care init values.\n", nDontCares );
130  Abc_Print( 1, "The don't-care are assumed to be 0. The result may not verify.\n" );
131  Abc_Print( 1, "Use command \"print_latch\" to see the init values of registers.\n" );
132  Abc_Print( 1, "Use command \"zero\" to convert or \"init\" to change the values.\n" );
133  }
134 
135  // collect the drivers
136  vSuper = Vec_PtrAlloc( 100 );
137  vDrivers = Vec_PtrAlloc( 100 );
138  if ( pvMap )
139  *pvMap = Vec_IntAlloc( 100 );
140  Abc_NtkForEachPo( pNtk, pObj, i )
141  {
142  if ( pNtk->nConstrs && i >= pNtk->nConstrs )
143  {
144  Vec_PtrPush( vDrivers, Abc_ObjNot(Abc_ObjChild0(pObj)) );
145  if ( pvMap )
146  Vec_IntPush( *pvMap, i );
147  continue;
148  }
149  Abc_CollectTopOr( Abc_ObjChild0(pObj), vSuper );
150  Vec_PtrForEachEntry( Abc_Obj_t *, vSuper, pTemp, k )
151  {
152  Vec_PtrPush( vDrivers, pTemp );
153  if ( pvMap )
154  Vec_IntPush( *pvMap, i );
155  }
156  }
157  Vec_PtrFree( vSuper );
158 
159  // create network
160  pMan = Aig_ManStart( Abc_NtkNodeNum(pNtk) + 100 );
161  pMan->nConstrs = pNtk->nConstrs;
162  pMan->nBarBufs = pNtk->nBarBufs;
163  pMan->pName = Extra_UtilStrsav( pNtk->pName );
164  pMan->pSpec = Extra_UtilStrsav( pNtk->pSpec );
165  // transfer the pointers to the basic nodes
166  Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)Aig_ManConst1(pMan);
167  Abc_NtkForEachCi( pNtk, pObj, i )
168  pObj->pCopy = (Abc_Obj_t *)Aig_ObjCreateCi(pMan);
169  // create flops
170  Abc_NtkForEachLatch( pNtk, pObj, i )
171  Abc_ObjFanout0(pObj)->pCopy = Abc_ObjNotCond( Abc_ObjFanout0(pObj)->pCopy, Abc_LatchIsInit1(pObj) );
172  // copy internal nodes
173  Abc_NtkForEachNode( pNtk, pObj, i )
174  pObj->pCopy = (Abc_Obj_t *)Aig_And( pMan, (Aig_Obj_t *)Abc_ObjChild0Copy(pObj), (Aig_Obj_t *)Abc_ObjChild1Copy(pObj) );
175  // create the POs
176  Vec_PtrForEachEntry( Abc_Obj_t *, vDrivers, pTemp, k )
177  Aig_ObjCreateCo( pMan, (Aig_Obj_t *)Abc_ObjNotCond(Abc_ObjRegular(pTemp)->pCopy, !Abc_ObjIsComplement(pTemp)) );
178  Vec_PtrFree( vDrivers );
179  // create flops
180  Abc_NtkForEachLatchInput( pNtk, pObj, i )
182 
183  // remove dangling nodes
184  Aig_ManSetRegNum( pMan, Abc_NtkLatchNum(pNtk) );
185  Aig_ManCleanup( pMan );
186  if ( !Aig_ManCheck( pMan ) )
187  {
188  Abc_Print( 1, "Abc_NtkToDarBmc: AIG check has failed.\n" );
189  Aig_ManStop( pMan );
190  return NULL;
191  }
192  return pMan;
193 }
194 
195 
196 /**Function*************************************************************
197 
198  Synopsis [Collects information about what flops have unknown values.]
199 
200  Description []
201 
202  SideEffects []
203 
204  SeeAlso []
205 
206 ***********************************************************************/
208 {
209  Vec_Int_t * vUnknown;
210  Abc_Obj_t * pObj;
211  int i;
212  vUnknown = Vec_IntStart( Abc_NtkLatchNum(pNtk) );
213  Abc_NtkForEachLatch( pNtk, pObj, i )
214  if ( Abc_LatchIsInitDc(pObj) )
215  {
216  Vec_IntWriteEntry( vUnknown, i, 1 );
217  Abc_LatchSetInit0(pObj);
218  }
219  return vUnknown;
220 }
221 
222 /**Function*************************************************************
223 
224  Synopsis [Converts the network from the AIG manager into ABC.]
225 
226  Description [Assumes that registers are ordered after PIs/POs.]
227 
228  SideEffects []
229 
230  SeeAlso []
231 
232 ***********************************************************************/
233 Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters )
234 {
235  Vec_Ptr_t * vNodes;
236  Aig_Man_t * pMan;
237  Aig_Obj_t * pObjNew;
238  Abc_Obj_t * pObj;
239  int i, nNodes, nDontCares;
240  // make sure the latches follow PIs/POs
241  if ( fRegisters )
242  {
243  assert( Abc_NtkBoxNum(pNtk) == Abc_NtkLatchNum(pNtk) );
244  Abc_NtkForEachCi( pNtk, pObj, i )
245  if ( i < Abc_NtkPiNum(pNtk) )
246  {
247  assert( Abc_ObjIsPi(pObj) );
248  if ( !Abc_ObjIsPi(pObj) )
249  Abc_Print( 1, "Abc_NtkToDar(): Temporary bug: The PI ordering is wrong!\n" );
250  }
251  else
252  assert( Abc_ObjIsBo(pObj) );
253  Abc_NtkForEachCo( pNtk, pObj, i )
254  if ( i < Abc_NtkPoNum(pNtk) )
255  {
256  assert( Abc_ObjIsPo(pObj) );
257  if ( !Abc_ObjIsPo(pObj) )
258  Abc_Print( 1, "Abc_NtkToDar(): Temporary bug: The PO ordering is wrong!\n" );
259  }
260  else
261  assert( Abc_ObjIsBi(pObj) );
262  // print warning about initial values
263  nDontCares = 0;
264  Abc_NtkForEachLatch( pNtk, pObj, i )
265  if ( Abc_LatchIsInitDc(pObj) )
266  {
267  Abc_LatchSetInit0(pObj);
268  nDontCares++;
269  }
270  if ( nDontCares )
271  {
272  Abc_Print( 1, "Warning: %d registers in this network have don't-care init values.\n", nDontCares );
273  Abc_Print( 1, "The don't-care are assumed to be 0. The result may not verify.\n" );
274  Abc_Print( 1, "Use command \"print_latch\" to see the init values of registers.\n" );
275  Abc_Print( 1, "Use command \"zero\" to convert or \"init\" to change the values.\n" );
276  }
277  }
278  // create the manager
279  pMan = Aig_ManStart( Abc_NtkNodeNum(pNtk) + 100 );
280  pMan->fCatchExor = fExors;
281  pMan->nConstrs = pNtk->nConstrs;
282  pMan->nBarBufs = pNtk->nBarBufs;
283  pMan->pName = Extra_UtilStrsav( pNtk->pName );
284  pMan->pSpec = Extra_UtilStrsav( pNtk->pSpec );
285  // transfer the pointers to the basic nodes
286  Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)Aig_ManConst1(pMan);
287  Abc_NtkForEachCi( pNtk, pObj, i )
288  {
289  pObj->pCopy = (Abc_Obj_t *)Aig_ObjCreateCi(pMan);
290  // initialize logic level of the CIs
291  ((Aig_Obj_t *)pObj->pCopy)->Level = pObj->Level;
292  }
293  // complement the 1-values registers
294  if ( fRegisters ) {
295  Abc_NtkForEachLatch( pNtk, pObj, i )
296  if ( Abc_LatchIsInit1(pObj) )
297  Abc_ObjFanout0(pObj)->pCopy = Abc_ObjNot(Abc_ObjFanout0(pObj)->pCopy);
298  }
299  // perform the conversion of the internal nodes (assumes DFS ordering)
300 // pMan->fAddStrash = 1;
301  vNodes = Abc_NtkDfs( pNtk, 0 );
302  Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
303 // Abc_NtkForEachNode( pNtk, pObj, i )
304  {
305  pObj->pCopy = (Abc_Obj_t *)Aig_And( pMan, (Aig_Obj_t *)Abc_ObjChild0Copy(pObj), (Aig_Obj_t *)Abc_ObjChild1Copy(pObj) );
306 // Abc_Print( 1, "%d->%d ", pObj->Id, ((Aig_Obj_t *)pObj->pCopy)->Id );
307  }
308  Vec_PtrFree( vNodes );
309  pMan->fAddStrash = 0;
310  // create the POs
311  Abc_NtkForEachCo( pNtk, pObj, i )
312  Aig_ObjCreateCo( pMan, (Aig_Obj_t *)Abc_ObjChild0Copy(pObj) );
313  // complement the 1-valued registers
314  Aig_ManSetRegNum( pMan, Abc_NtkLatchNum(pNtk) );
315  if ( fRegisters )
316  Aig_ManForEachLiSeq( pMan, pObjNew, i )
317  if ( Abc_LatchIsInit1(Abc_ObjFanout0(Abc_NtkCo(pNtk,i))) )
318  pObjNew->pFanin0 = Aig_Not(pObjNew->pFanin0);
319  // remove dangling nodes
320  nNodes = (Abc_NtkGetChoiceNum(pNtk) == 0)? Aig_ManCleanup( pMan ) : 0;
321  if ( !fExors && nNodes )
322  Abc_Print( 1, "Abc_NtkToDar(): Unexpected %d dangling nodes when converting to AIG!\n", nNodes );
323 //Aig_ManDumpVerilog( pMan, "test.v" );
324  // save the number of registers
325  if ( fRegisters )
326  {
327  Aig_ManSetRegNum( pMan, Abc_NtkLatchNum(pNtk) );
328  pMan->vFlopNums = Vec_IntStartNatural( pMan->nRegs );
329 // pMan->vFlopNums = NULL;
330 // pMan->vOnehots = Abc_NtkConverLatchNamesIntoNumbers( pNtk );
331  if ( pNtk->vOnehots )
332  pMan->vOnehots = (Vec_Ptr_t *)Vec_VecDupInt( (Vec_Vec_t *)pNtk->vOnehots );
333  }
334  if ( !Aig_ManCheck( pMan ) )
335  {
336  Abc_Print( 1, "Abc_NtkToDar: AIG check has failed.\n" );
337  Aig_ManStop( pMan );
338  return NULL;
339  }
340  return pMan;
341 }
342 
343 /**Function*************************************************************
344 
345  Synopsis [Converts the network from the AIG manager into ABC.]
346 
347  Description [Assumes that registers are ordered after PIs/POs.]
348 
349  SideEffects []
350 
351  SeeAlso []
352 
353 ***********************************************************************/
355 {
356  Aig_Man_t * pMan;
357  Abc_Obj_t * pObj, * pPrev, * pFanin;
358  Vec_Ptr_t * vNodes;
359  int i;
360  vNodes = Abc_AigDfs( pNtk, 0, 0 );
361  // create the manager
362  pMan = Aig_ManStart( Abc_NtkNodeNum(pNtk) + 100 );
363  pMan->nConstrs = pNtk->nConstrs;
364  pMan->nBarBufs = pNtk->nBarBufs;
365  pMan->pName = Extra_UtilStrsav( pNtk->pName );
366  pMan->pSpec = Extra_UtilStrsav( pNtk->pSpec );
367  if ( Abc_NtkGetChoiceNum(pNtk) )
368  {
369  pMan->pEquivs = ABC_ALLOC( Aig_Obj_t *, Abc_NtkObjNum(pNtk) );
370  memset( pMan->pEquivs, 0, sizeof(Aig_Obj_t *) * Abc_NtkObjNum(pNtk) );
371  }
372  // transfer the pointers to the basic nodes
373  Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)Aig_ManConst1(pMan);
374  Abc_NtkForEachCi( pNtk, pObj, i )
375  pObj->pCopy = (Abc_Obj_t *)Aig_ObjCreateCi(pMan);
376  // perform the conversion of the internal nodes (assumes DFS ordering)
377  Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
378  {
379  pObj->pCopy = (Abc_Obj_t *)Aig_And( pMan, (Aig_Obj_t *)Abc_ObjChild0Copy(pObj), (Aig_Obj_t *)Abc_ObjChild1Copy(pObj) );
380 // Abc_Print( 1, "%d->%d ", pObj->Id, ((Aig_Obj_t *)pObj->pCopy)->Id );
381  if ( Abc_AigNodeIsChoice( pObj ) )
382  {
383  for ( pPrev = pObj, pFanin = (Abc_Obj_t *)pObj->pData; pFanin; pPrev = pFanin, pFanin = (Abc_Obj_t *)pFanin->pData )
384  Aig_ObjSetEquiv( pMan, (Aig_Obj_t *)pPrev->pCopy, (Aig_Obj_t *)pFanin->pCopy );
385 // Aig_ManCreateChoice( pIfMan, (Aig_Obj_t *)pNode->pCopy );
386  }
387  }
388  Vec_PtrFree( vNodes );
389  // create the POs
390  Abc_NtkForEachCo( pNtk, pObj, i )
391  Aig_ObjCreateCo( pMan, (Aig_Obj_t *)Abc_ObjChild0Copy(pObj) );
392  // complement the 1-valued registers
393  Aig_ManSetRegNum( pMan, 0 );
394  if ( !Aig_ManCheck( pMan ) )
395  {
396  Abc_Print( 1, "Abc_NtkToDar: AIG check has failed.\n" );
397  Aig_ManStop( pMan );
398  return NULL;
399  }
400  return pMan;
401 }
402 
403 /**Function*************************************************************
404 
405  Synopsis [Converts the network from the AIG manager into ABC.]
406 
407  Description []
408 
409  SideEffects []
410 
411  SeeAlso []
412 
413 ***********************************************************************/
415 {
416  Vec_Ptr_t * vNodes;
417  Abc_Ntk_t * pNtkNew;
418  Aig_Obj_t * pObj;
419  int i;
420  assert( pMan->nAsserts == 0 );
421 // assert( Aig_ManRegNum(pMan) == Abc_NtkLatchNum(pNtkOld) );
422  // perform strashing
423  pNtkNew = Abc_NtkStartFrom( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
424  pNtkNew->nConstrs = pMan->nConstrs;
425  pNtkNew->nBarBufs = pNtkOld->nBarBufs;
426  // transfer the pointers to the basic nodes
427  Aig_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew);
428  Aig_ManForEachCi( pMan, pObj, i )
429  {
430  pObj->pData = Abc_NtkCi(pNtkNew, i);
431  // initialize logic level of the CIs
432  ((Abc_Obj_t *)pObj->pData)->Level = pObj->Level;
433  }
434  // rebuild the AIG
435  vNodes = Aig_ManDfs( pMan, 1 );
436  Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
437  if ( Aig_ObjIsBuf(pObj) )
438  pObj->pData = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj);
439  else
440  pObj->pData = Abc_AigAnd( (Abc_Aig_t *)pNtkNew->pManFunc, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj), (Abc_Obj_t *)Aig_ObjChild1Copy(pObj) );
441  Vec_PtrFree( vNodes );
442  // connect the PO nodes
443  Aig_ManForEachCo( pMan, pObj, i )
444  {
445  if ( pMan->nAsserts && i == Aig_ManCoNum(pMan) - pMan->nAsserts )
446  break;
447  Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), (Abc_Obj_t *)Aig_ObjChild0Copy(pObj) );
448  }
449  // if there are assertions, add them
450  if ( !Abc_NtkCheck( pNtkNew ) )
451  Abc_Print( 1, "Abc_NtkFromDar(): Network check has failed.\n" );
452 //Abc_NtkPrintCiLevels( pNtkNew );
453  return pNtkNew;
454 }
455 
456 /**Function*************************************************************
457 
458  Synopsis [Converts the network from the AIG manager into ABC.]
459 
460  Description [This procedure should be called after seq sweeping,
461  which changes the number of registers.]
462 
463  SideEffects []
464 
465  SeeAlso []
466 
467 ***********************************************************************/
469 {
470  Vec_Ptr_t * vNodes;
471  Abc_Ntk_t * pNtkNew;
472  Abc_Obj_t * pObjNew, * pLatch;
473  Aig_Obj_t * pObj, * pObjLo, * pObjLi;
474  int i, iNodeId, nDigits;
475  assert( pMan->nAsserts == 0 );
476  assert( pNtkOld->nBarBufs == 0 );
477 // assert( Aig_ManRegNum(pMan) != Abc_NtkLatchNum(pNtkOld) );
478  // perform strashing
480  pNtkNew->nConstrs = pMan->nConstrs;
481  pNtkNew->nBarBufs = pMan->nBarBufs;
482  // consider the case of target enlargement
483  if ( Abc_NtkCiNum(pNtkNew) < Aig_ManCiNum(pMan) - Aig_ManRegNum(pMan) )
484  {
485  for ( i = Aig_ManCiNum(pMan) - Aig_ManRegNum(pMan) - Abc_NtkCiNum(pNtkNew); i > 0; i-- )
486  {
487  pObjNew = Abc_NtkCreatePi( pNtkNew );
488  Abc_ObjAssignName( pObjNew, Abc_ObjName(pObjNew), NULL );
489  }
490  Abc_NtkOrderCisCos( pNtkNew );
491  }
492  assert( Abc_NtkCiNum(pNtkNew) == Aig_ManCiNum(pMan) - Aig_ManRegNum(pMan) );
493  assert( Abc_NtkCoNum(pNtkNew) == Aig_ManCoNum(pMan) - Aig_ManRegNum(pMan) );
494  // transfer the pointers to the basic nodes
495  Aig_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew);
496  Aig_ManForEachPiSeq( pMan, pObj, i )
497  pObj->pData = Abc_NtkCi(pNtkNew, i);
498  // create as many latches as there are registers in the manager
499  Aig_ManForEachLiLoSeq( pMan, pObjLi, pObjLo, i )
500  {
501  pObjNew = Abc_NtkCreateLatch( pNtkNew );
502  pObjLi->pData = Abc_NtkCreateBi( pNtkNew );
503  pObjLo->pData = Abc_NtkCreateBo( pNtkNew );
504  Abc_ObjAddFanin( pObjNew, (Abc_Obj_t *)pObjLi->pData );
505  Abc_ObjAddFanin( (Abc_Obj_t *)pObjLo->pData, pObjNew );
506  Abc_LatchSetInit0( pObjNew );
507  }
508  // rebuild the AIG
509  vNodes = Aig_ManDfs( pMan, 1 );
510  Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
511  if ( Aig_ObjIsBuf(pObj) )
512  pObj->pData = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj);
513  else
514  pObj->pData = Abc_AigAnd( (Abc_Aig_t *)pNtkNew->pManFunc, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj), (Abc_Obj_t *)Aig_ObjChild1Copy(pObj) );
515  Vec_PtrFree( vNodes );
516  // connect the PO nodes
517  Aig_ManForEachCo( pMan, pObj, i )
518  {
519 // if ( pMan->nAsserts && i == Aig_ManCoNum(pMan) - pMan->nAsserts )
520 // break;
521  iNodeId = Nm_ManFindIdByNameTwoTypes( pNtkNew->pManName, Abc_ObjName(Abc_NtkCo(pNtkNew, i)), ABC_OBJ_PI, ABC_OBJ_BO );
522  if ( iNodeId >= 0 )
523  pObjNew = Abc_NtkObj( pNtkNew, iNodeId );
524  else
525  pObjNew = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj);
526  Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), pObjNew );
527  }
528  if ( pMan->vFlopNums == NULL )
529  Abc_NtkAddDummyBoxNames( pNtkNew );
530  else
531  {
532 /*
533  {
534  int i, k, iFlop, Counter = 0;
535  FILE * pFile;
536  pFile = fopen( "out.txt", "w" );
537  fAbc_Print( 1, pFile, "The total of %d registers were removed (out of %d):\n",
538  Abc_NtkLatchNum(pNtkOld)-Vec_IntSize(pMan->vFlopNums), Abc_NtkLatchNum(pNtkOld) );
539  for ( i = 0; i < Abc_NtkLatchNum(pNtkOld); i++ )
540  {
541  Vec_IntForEachEntry( pMan->vFlopNums, iFlop, k )
542  {
543  if ( i == iFlop )
544  break;
545  }
546  if ( k == Vec_IntSize(pMan->vFlopNums) )
547  fAbc_Print( 1, pFile, "%6d (%6d) : %s\n", ++Counter, i, Abc_ObjName( Abc_ObjFanout0(Abc_NtkBox(pNtkOld, i)) ) );
548  }
549  fclose( pFile );
550  //Abc_Print( 1, "\n" );
551  }
552 */
553  assert( Abc_NtkBoxNum(pNtkOld) == Abc_NtkLatchNum(pNtkOld) );
554  nDigits = Abc_Base10Log( Abc_NtkLatchNum(pNtkNew) );
555  Abc_NtkForEachLatch( pNtkNew, pObjNew, i )
556  {
557  pLatch = Abc_NtkBox( pNtkOld, Vec_IntEntry( pMan->vFlopNums, i ) );
558  iNodeId = Nm_ManFindIdByName( pNtkNew->pManName, Abc_ObjName(Abc_ObjFanout0(pLatch)), ABC_OBJ_PO );
559  if ( iNodeId >= 0 )
560  {
561  Abc_ObjAssignName( pObjNew, Abc_ObjNameDummy("l", i, nDigits), NULL );
562  Abc_ObjAssignName( Abc_ObjFanin0(pObjNew), Abc_ObjNameDummy("li", i, nDigits), NULL );
563  Abc_ObjAssignName( Abc_ObjFanout0(pObjNew), Abc_ObjNameDummy("lo", i, nDigits), NULL );
564 //Abc_Print( 1, "happening %s -> %s\n", Abc_ObjName(Abc_ObjFanin0(pObjNew)), Abc_ObjName(Abc_ObjFanout0(pObjNew)) );
565  continue;
566  }
567  Abc_ObjAssignName( pObjNew, Abc_ObjName(pLatch), NULL );
568  Abc_ObjAssignName( Abc_ObjFanin0(pObjNew), Abc_ObjName(Abc_ObjFanin0(pLatch)), NULL );
569  Abc_ObjAssignName( Abc_ObjFanout0(pObjNew), Abc_ObjName(Abc_ObjFanout0(pLatch)), NULL );
570  }
571  }
572  // if there are assertions, add them
573  if ( !Abc_NtkCheck( pNtkNew ) )
574  Abc_Print( 1, "Abc_NtkFromDar(): Network check has failed.\n" );
575  return pNtkNew;
576 }
577 
578 /**Function*************************************************************
579 
580  Synopsis [Converts the network from the AIG manager into ABC.]
581 
582  Description [This procedure should be called after seq sweeping,
583  which changes the number of registers.]
584 
585  SideEffects []
586 
587  SeeAlso []
588 
589 ***********************************************************************/
591 {
592  Vec_Ptr_t * vNodes;
593  Abc_Ntk_t * pNtkNew;
594  Abc_Obj_t * pObjNew;
595  Aig_Obj_t * pObj, * pObjLo, * pObjLi;
596  int i;
597  assert( pMan->nAsserts == 0 );
598  // perform strashing
599  pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
600  pNtkNew->nConstrs = pMan->nConstrs;
601  pNtkNew->nBarBufs = pMan->nBarBufs;
602  // duplicate the name and the spec
603 // pNtkNew->pName = Extra_UtilStrsav(pMan->pName);
604 // pNtkNew->pSpec = Extra_UtilStrsav(pMan->pSpec);
605  Aig_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew);
606  // create PIs
607  Aig_ManForEachPiSeq( pMan, pObj, i )
608  {
609  pObjNew = Abc_NtkCreatePi( pNtkNew );
610 // Abc_ObjAssignName( pObjNew, Abc_ObjName(pObjNew), NULL );
611  pObj->pData = pObjNew;
612  }
613  // create POs
614  Aig_ManForEachPoSeq( pMan, pObj, i )
615  {
616  pObjNew = Abc_NtkCreatePo( pNtkNew );
617 // Abc_ObjAssignName( pObjNew, Abc_ObjName(pObjNew), NULL );
618  pObj->pData = pObjNew;
619  }
620  assert( Abc_NtkCiNum(pNtkNew) == Aig_ManCiNum(pMan) - Aig_ManRegNum(pMan) );
621  assert( Abc_NtkCoNum(pNtkNew) == Aig_ManCoNum(pMan) - Aig_ManRegNum(pMan) );
622  // create as many latches as there are registers in the manager
623  Aig_ManForEachLiLoSeq( pMan, pObjLi, pObjLo, i )
624  {
625  pObjNew = Abc_NtkCreateLatch( pNtkNew );
626  pObjLi->pData = Abc_NtkCreateBi( pNtkNew );
627  pObjLo->pData = Abc_NtkCreateBo( pNtkNew );
628  Abc_ObjAddFanin( pObjNew, (Abc_Obj_t *)pObjLi->pData );
629  Abc_ObjAddFanin( (Abc_Obj_t *)pObjLo->pData, pObjNew );
630  Abc_LatchSetInit0( pObjNew );
631 // Abc_ObjAssignName( (Abc_Obj_t *)pObjLi->pData, Abc_ObjName((Abc_Obj_t *)pObjLi->pData), NULL );
632 // Abc_ObjAssignName( (Abc_Obj_t *)pObjLo->pData, Abc_ObjName((Abc_Obj_t *)pObjLo->pData), NULL );
633  }
634  // rebuild the AIG
635  vNodes = Aig_ManDfs( pMan, 1 );
636  Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
637  if ( Aig_ObjIsBuf(pObj) )
638  pObj->pData = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj);
639  else
640  pObj->pData = Abc_AigAnd( (Abc_Aig_t *)pNtkNew->pManFunc, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj), (Abc_Obj_t *)Aig_ObjChild1Copy(pObj) );
641  Vec_PtrFree( vNodes );
642  // connect the PO nodes
643  Aig_ManForEachCo( pMan, pObj, i )
644  {
645  pObjNew = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj);
646  Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), pObjNew );
647  }
648 
649  Abc_NtkAddDummyPiNames( pNtkNew );
650  Abc_NtkAddDummyPoNames( pNtkNew );
651  Abc_NtkAddDummyBoxNames( pNtkNew );
652 
653  // check the resulting AIG
654  if ( !Abc_NtkCheck( pNtkNew ) )
655  Abc_Print( 1, "Abc_NtkFromAigPhase(): Network check has failed.\n" );
656  return pNtkNew;
657 }
658 
659 
660 
661 /**Function*************************************************************
662 
663  Synopsis [Creates local function of the node.]
664 
665  Description []
666 
667  SideEffects []
668 
669  SeeAlso []
670 
671 ***********************************************************************/
672 Hop_Obj_t * Abc_ObjHopFromGia_rec( Hop_Man_t * pHopMan, Gia_Man_t * p, int Id, Vec_Ptr_t * vCopies )
673 {
674  Gia_Obj_t * pObj;
675  Hop_Obj_t * gFunc, * gFunc0, * gFunc1;
676  if ( Gia_ObjIsTravIdCurrentId(p, Id) )
677  return (Hop_Obj_t *)Vec_PtrEntry( vCopies, Id );
679  pObj = Gia_ManObj(p, Id);
680  assert( Gia_ObjIsAnd(pObj) );
681  // compute the functions of the children
682  gFunc0 = Abc_ObjHopFromGia_rec( pHopMan, p, Gia_ObjFaninId0(pObj, Id), vCopies );
683  gFunc1 = Abc_ObjHopFromGia_rec( pHopMan, p, Gia_ObjFaninId1(pObj, Id), vCopies );
684  // get the function of the cut
685  gFunc = Hop_And( pHopMan, Hop_NotCond(gFunc0, Gia_ObjFaninC0(pObj)), Hop_NotCond(gFunc1, Gia_ObjFaninC1(pObj)) );
686  Vec_PtrWriteEntry( vCopies, Id, gFunc );
687  return gFunc;
688 }
689 Hop_Obj_t * Abc_ObjHopFromGia( Hop_Man_t * pHopMan, Gia_Man_t * p, int GiaId, Vec_Ptr_t * vCopies )
690 {
691  int k, iFan;
692  assert( Gia_ObjIsLut(p, GiaId) );
693  assert( Gia_ObjLutSize(p, GiaId) > 0 );
695  Gia_LutForEachFanin( p, GiaId, iFan, k )
696  {
697  Gia_ObjSetTravIdCurrentId(p, iFan);
698  Vec_PtrWriteEntry( vCopies, iFan, Hop_IthVar(pHopMan, k) );
699  }
700  return Abc_ObjHopFromGia_rec( pHopMan, p, GiaId, vCopies );
701 }
702 
703 /**Function*************************************************************
704 
705  Synopsis [Converts the network from the mapped GIA manager.]
706 
707  Description []
708 
709  SideEffects []
710 
711  SeeAlso []
712 
713 ***********************************************************************/
715 {
716  int fVerbose = 0;
717  int fDuplicate = 0;
718  Abc_Ntk_t * pNtkNew;
719  Abc_Obj_t * pObjNew, * pObjNewLi, * pObjNewLo, * pConst0 = NULL;
720  Gia_Obj_t * pObj, * pObjLi, * pObjLo;
721  Vec_Ptr_t * vReflect;
722  int i, k, iFan, nDupGates;
723  assert( Gia_ManHasMapping(p) || p->pMuxes );
725  // duplicate the name and the spec
726  pNtkNew->pName = Extra_UtilStrsav(p->pName);
727  pNtkNew->pSpec = Extra_UtilStrsav(p->pSpec);
728  Gia_ManFillValue( p );
729  // create constant
730  pConst0 = Abc_NtkCreateNodeConst0( pNtkNew );
731  Gia_ManConst0(p)->Value = Abc_ObjId(pConst0);
732  // create PIs
733  Gia_ManForEachPi( p, pObj, i )
734  pObj->Value = Abc_ObjId( Abc_NtkCreatePi( pNtkNew ) );
735  // create POs
736  Gia_ManForEachPo( p, pObj, i )
737  pObj->Value = Abc_ObjId( Abc_NtkCreatePo( pNtkNew ) );
738  // create as many latches as there are registers in the manager
739  Gia_ManForEachRiRo( p, pObjLi, pObjLo, i )
740  {
741  pObjNew = Abc_NtkCreateLatch( pNtkNew );
742  pObjNewLi = Abc_NtkCreateBi( pNtkNew );
743  pObjNewLo = Abc_NtkCreateBo( pNtkNew );
744  Abc_ObjAddFanin( pObjNew, pObjNewLi );
745  Abc_ObjAddFanin( pObjNewLo, pObjNew );
746  pObjLi->Value = Abc_ObjId( pObjNewLi );
747  pObjLo->Value = Abc_ObjId( pObjNewLo );
748  Abc_LatchSetInit0( pObjNew );
749  }
750  // rebuild the AIG
751  if ( p->pMuxes )
752  {
753  Gia_ManForEachAnd( p, pObj, i )
754  {
755  pObjNew = Abc_NtkCreateNode( pNtkNew );
756  if ( Gia_ObjIsMuxId(p, i) )
757  {
758  Abc_ObjAddFanin( pObjNew, Abc_NtkObj(pNtkNew, Gia_ObjValue(Gia_ObjFanin2(p, pObj))) );
759  Abc_ObjAddFanin( pObjNew, Abc_NtkObj(pNtkNew, Gia_ObjValue(Gia_ObjFanin1(pObj))) );
760  Abc_ObjAddFanin( pObjNew, Abc_NtkObj(pNtkNew, Gia_ObjValue(Gia_ObjFanin0(pObj))) );
761  pObjNew->pData = Abc_SopCreateMux( (Mem_Flex_t *)pNtkNew->pManFunc );
762  if ( Gia_ObjFaninC2(p, pObj) ) Abc_SopComplementVar( (char *)pObjNew->pData, 0 );
763  if ( Gia_ObjFaninC1(pObj) ) Abc_SopComplementVar( (char *)pObjNew->pData, 1 );
764  if ( Gia_ObjFaninC0(pObj) ) Abc_SopComplementVar( (char *)pObjNew->pData, 2 );
765  }
766  else if ( Gia_ObjIsXor(pObj) )
767  {
768  Abc_ObjAddFanin( pObjNew, Abc_NtkObj(pNtkNew, Gia_ObjValue(Gia_ObjFanin0(pObj))) );
769  Abc_ObjAddFanin( pObjNew, Abc_NtkObj(pNtkNew, Gia_ObjValue(Gia_ObjFanin1(pObj))) );
770  pObjNew->pData = Abc_SopCreateXor( (Mem_Flex_t *)pNtkNew->pManFunc, 2 );
771  if ( Gia_ObjFaninC0(pObj) ) Abc_SopComplementVar( (char *)pObjNew->pData, 0 );
772  if ( Gia_ObjFaninC1(pObj) ) Abc_SopComplementVar( (char *)pObjNew->pData, 1 );
773  }
774  else
775  {
776  Abc_ObjAddFanin( pObjNew, Abc_NtkObj(pNtkNew, Gia_ObjValue(Gia_ObjFanin0(pObj))) );
777  Abc_ObjAddFanin( pObjNew, Abc_NtkObj(pNtkNew, Gia_ObjValue(Gia_ObjFanin1(pObj))) );
778  pObjNew->pData = Abc_SopCreateAnd( (Mem_Flex_t *)pNtkNew->pManFunc, 2, NULL );
779  if ( Gia_ObjFaninC0(pObj) ) Abc_SopComplementVar( (char *)pObjNew->pData, 0 );
780  if ( Gia_ObjFaninC1(pObj) ) Abc_SopComplementVar( (char *)pObjNew->pData, 1 );
781  }
782  pObj->Value = Abc_ObjId( pObjNew );
783  }
784  }
785  else
786  {
787  vReflect = Vec_PtrStart( Gia_ManObjNum(p) );
788  Gia_ManForEachLut( p, i )
789  {
790  pObj = Gia_ManObj(p, i);
791  assert( pObj->Value == ~0 );
792  if ( Gia_ObjLutSize(p, i) == 0 )
793  {
794  pObj->Value = Abc_ObjId(pConst0);
795  continue;
796  }
797  pObjNew = Abc_NtkCreateNode( pNtkNew );
798  Gia_LutForEachFanin( p, i, iFan, k )
799  Abc_ObjAddFanin( pObjNew, Abc_NtkObj(pNtkNew, Gia_ObjValue(Gia_ManObj(p, iFan))) );
800  pObjNew->pData = Abc_ObjHopFromGia( (Hop_Man_t *)pNtkNew->pManFunc, p, i, vReflect );
801  pObj->Value = Abc_ObjId( pObjNew );
802  }
803  Vec_PtrFree( vReflect );
804  }
805  // connect the PO nodes
806  Gia_ManForEachCo( p, pObj, i )
807  {
808  pObjNew = Abc_NtkObj( pNtkNew, Gia_ObjValue(Gia_ObjFanin0(pObj)) );
809  Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), Abc_ObjNotCond( pObjNew, Gia_ObjFaninC0(pObj) ) );
810  }
811  // create names
812  Abc_NtkAddDummyPiNames( pNtkNew );
813  Abc_NtkAddDummyPoNames( pNtkNew );
814  Abc_NtkAddDummyBoxNames( pNtkNew );
815 
816  // decouple the PO driver nodes to reduce the number of levels
817  nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, fDuplicate );
818  if ( fVerbose && nDupGates && !Abc_FrameReadFlag("silentmode") )
819  {
820  if ( !fDuplicate )
821  printf( "Added %d buffers/inverters to decouple the CO drivers.\n", nDupGates );
822  else
823  printf( "Duplicated %d gates to decouple the CO drivers.\n", nDupGates );
824  }
825  // remove const node if it is not used
826  if ( !Abc_ObjIsNone(pConst0) && Abc_ObjFanoutNum(pConst0) == 0 )
827  Abc_NtkDeleteObj( pConst0 );
828 
829  assert( Gia_ManPiNum(p) == Abc_NtkPiNum(pNtkNew) );
830  assert( Gia_ManPoNum(p) == Abc_NtkPoNum(pNtkNew) );
831  assert( Gia_ManRegNum(p) == Abc_NtkLatchNum(pNtkNew) );
832 
833  // check the resulting AIG
834  if ( !Abc_NtkCheck( pNtkNew ) )
835  Abc_Print( 1, "Abc_NtkFromMappedGia(): Network check has failed.\n" );
836  return pNtkNew;
837 }
838 
839 /**Function*************************************************************
840 
841  Synopsis [Converts the network from the mapped GIA manager.]
842 
843  Description []
844 
845  SideEffects []
846 
847  SeeAlso []
848 
849 ***********************************************************************/
850 static inline void Abc_NtkFromCellWrite( Vec_Int_t * vCopyLits, int i, int c, int Id )
851 {
852  Vec_IntWriteEntry( vCopyLits, Abc_Var2Lit(i, c), Id );
853 }
854 static inline Abc_Obj_t * Abc_NtkFromCellRead( Abc_Ntk_t * p, Vec_Int_t * vCopyLits, int i, int c )
855 {
856  Abc_Obj_t * pObjNew;
857  int iObjNew = Vec_IntEntry( vCopyLits, Abc_Var2Lit(i, c) );
858  if ( iObjNew >= 0 )
859  return Abc_NtkObj(p, iObjNew);
860  // opposite phase should be already constructed
861  assert( 0 );
862  if ( i == 0 )
863  pObjNew = c ? Abc_NtkCreateNodeConst1(p) : Abc_NtkCreateNodeConst0(p);
864  else
865  {
866  iObjNew = Vec_IntEntry( vCopyLits, Abc_Var2Lit(i, !c) ); assert( iObjNew >= 0 );
867  pObjNew = Abc_NtkCreateNodeInv( p, Abc_NtkObj(p, iObjNew) );
868  }
869  Abc_NtkFromCellWrite( vCopyLits, i, c, Abc_ObjId(pObjNew) );
870  return pObjNew;
871 }
873 {
874  int fVerbose = 1;
875  int fDuplicate = 1;
876  Abc_Ntk_t * pNtkNew;
877  Vec_Int_t * vCopyLits;
878  Abc_Obj_t * pObjNew, * pObjNewLi, * pObjNewLo;
879  Gia_Obj_t * pObj, * pObjLi, * pObjLo;
880  int i, k, iLit, iFanLit, nDupGates, nCells, fNeedConst[2] = {0};
881  Mio_Cell_t * pCells = Mio_CollectRootsNewDefault( 6, &nCells, 0 );
883  // start network
884  pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_MAP, 1 );
885  pNtkNew->pName = Extra_UtilStrsav(p->pName);
886  pNtkNew->pSpec = Extra_UtilStrsav(p->pSpec);
887  assert( pNtkNew->pManFunc == Abc_FrameReadLibGen() );
888  vCopyLits = Vec_IntStartFull( 2*Gia_ManObjNum(p) );
889  // create PIs
890  Gia_ManForEachPi( p, pObj, i )
891  Abc_NtkFromCellWrite( vCopyLits, Gia_ObjId(p, pObj), 0, Abc_ObjId( Abc_NtkCreatePi( pNtkNew ) ) );
892  // create POs
893  Gia_ManForEachPo( p, pObj, i )
894  Abc_NtkFromCellWrite( vCopyLits, Gia_ObjId(p, pObj), 0, Abc_ObjId( Abc_NtkCreatePo( pNtkNew ) ) );
895  // create as many latches as there are registers in the manager
896  Gia_ManForEachRiRo( p, pObjLi, pObjLo, i )
897  {
898  pObjNew = Abc_NtkCreateLatch( pNtkNew );
899  pObjNewLi = Abc_NtkCreateBi( pNtkNew );
900  pObjNewLo = Abc_NtkCreateBo( pNtkNew );
901  Abc_ObjAddFanin( pObjNew, pObjNewLi );
902  Abc_ObjAddFanin( pObjNewLo, pObjNew );
903 // pObjLi->Value = Abc_ObjId( pObjNewLi );
904 // pObjLo->Value = Abc_ObjId( pObjNewLo );
905  Abc_NtkFromCellWrite( vCopyLits, Gia_ObjId(p, pObjLi), 0, Abc_ObjId( pObjNewLi ) );
906  Abc_NtkFromCellWrite( vCopyLits, Gia_ObjId(p, pObjLo), 0, Abc_ObjId( pObjNewLo ) );
907  Abc_LatchSetInit0( pObjNew );
908  }
909 
910  // create constants
911  Gia_ManForEachCo( p, pObj, i )
912  if ( Gia_ObjFaninId0p(p, pObj) == 0 )
913  fNeedConst[Gia_ObjFaninC0(pObj)] = 1;
914  Gia_ManForEachBuf( p, pObj, i )
915  if ( Gia_ObjFaninId0p(p, pObj) == 0 )
916  fNeedConst[Gia_ObjFaninC0(pObj)] = 1;
917  if ( fNeedConst[0] )
918  Abc_NtkFromCellWrite( vCopyLits, 0, 0, Abc_ObjId(Abc_NtkCreateNodeConst0(pNtkNew)) );
919  if ( fNeedConst[1] )
920  Abc_NtkFromCellWrite( vCopyLits, 0, 1, Abc_ObjId(Abc_NtkCreateNodeConst1(pNtkNew)) );
921 
922  // rebuild the AIG
923  Gia_ManForEachCell( p, iLit )
924  {
925  int fSkip = 0;
926  if ( Gia_ObjIsCellBuf(p, iLit) )
927  {
928  assert( !Abc_LitIsCompl(iLit) );
929  // build buffer
930  pObjNew = Abc_NtkCreateNode( pNtkNew );
931  iFanLit = Gia_ObjFaninLit0p( p, Gia_ManObj(p, Abc_Lit2Var(iLit)) );
932  Abc_ObjAddFanin( pObjNew, Abc_NtkFromCellRead(pNtkNew, vCopyLits, Abc_Lit2Var(iFanLit), Abc_LitIsCompl(iFanLit)) );
933  pObjNew->pData = NULL; // barrier buffer
934  assert( Abc_ObjIsBarBuf(pObjNew) );
935  pNtkNew->nBarBufs2++;
936  }
937  else if ( Gia_ObjIsCellInv(p, iLit) )
938  {
939  int iLitNot = Abc_LitNot(iLit);
940  if ( !Abc_LitIsCompl(iLit) ) // positive phase
941  {
942  // build negative phase
943  assert( Vec_IntEntry(vCopyLits, iLitNot) == -1 );
944  assert( Gia_ObjCellId(p, iLitNot) > 0 );
945  pObjNew = Abc_NtkCreateNode( pNtkNew );
946  Gia_CellForEachFanin( p, iLitNot, iFanLit, k )
947  Abc_ObjAddFanin( pObjNew, Abc_NtkFromCellRead(pNtkNew, vCopyLits, Abc_Lit2Var(iFanLit), Abc_LitIsCompl(iFanLit)) );
948  pObjNew->pData = Mio_LibraryReadGateByName( (Mio_Library_t *)pNtkNew->pManFunc, pCells[Gia_ObjCellId(p, iLitNot)].pName, NULL );
949  Abc_NtkFromCellWrite( vCopyLits, Abc_Lit2Var(iLitNot), Abc_LitIsCompl(iLitNot), Abc_ObjId(pObjNew) );
950  fSkip = 1;
951  }
952  else // negative phase
953  {
954  // positive phase is available
955  assert( Vec_IntEntry(vCopyLits, iLitNot) != -1 );
956  }
957  // build inverter
958  pObjNew = Abc_NtkCreateNode( pNtkNew );
959  Abc_ObjAddFanin( pObjNew, Abc_NtkFromCellRead(pNtkNew, vCopyLits, Abc_Lit2Var(iLit), Abc_LitIsCompl(iLitNot)) );
960  pObjNew->pData = Mio_LibraryReadGateByName( (Mio_Library_t *)pNtkNew->pManFunc, pCells[3].pName, NULL );
961  }
962  else
963  {
964  assert( Gia_ObjCellId(p, iLit) > 0 );
965  pObjNew = Abc_NtkCreateNode( pNtkNew );
966  Gia_CellForEachFanin( p, iLit, iFanLit, k )
967  Abc_ObjAddFanin( pObjNew, Abc_NtkFromCellRead(pNtkNew, vCopyLits, Abc_Lit2Var(iFanLit), Abc_LitIsCompl(iFanLit)) );
968  pObjNew->pData = Mio_LibraryReadGateByName( (Mio_Library_t *)pNtkNew->pManFunc, pCells[Gia_ObjCellId(p, iLit)].pName, NULL );
969  }
970  assert( Vec_IntEntry(vCopyLits, iLit) == -1 );
971  Abc_NtkFromCellWrite( vCopyLits, Abc_Lit2Var(iLit), Abc_LitIsCompl(iLit), Abc_ObjId(pObjNew) );
972  // skip next
973  iLit += fSkip;
974  }
975 
976  // connect the PO nodes
977  Gia_ManForEachCo( p, pObj, i )
978  {
979  pObjNew = Abc_NtkFromCellRead( pNtkNew, vCopyLits, Gia_ObjFaninId0p(p, pObj), Gia_ObjFaninC0(pObj) );
980  Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), pObjNew );
981  }
982  // create names
983  Abc_NtkAddDummyPiNames( pNtkNew );
984  Abc_NtkAddDummyPoNames( pNtkNew );
985  Abc_NtkAddDummyBoxNames( pNtkNew );
986 
987  // decouple the PO driver nodes to reduce the number of levels
988  nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, fDuplicate );
989  if ( fVerbose && nDupGates && !Abc_FrameReadFlag("silentmode") )
990  {
991  if ( !fDuplicate )
992  printf( "Added %d buffers/inverters to decouple the CO drivers.\n", nDupGates );
993  else
994  printf( "Duplicated %d gates to decouple the CO drivers.\n", nDupGates );
995  }
996  assert( Gia_ManPiNum(p) == Abc_NtkPiNum(pNtkNew) );
997  assert( Gia_ManPoNum(p) == Abc_NtkPoNum(pNtkNew) );
998  assert( Gia_ManRegNum(p) == Abc_NtkLatchNum(pNtkNew) );
999  Vec_IntFree( vCopyLits );
1000  ABC_FREE( pCells );
1001 
1002  // check the resulting AIG
1003  if ( !Abc_NtkCheck( pNtkNew ) )
1004  Abc_Print( 1, "Abc_NtkFromMappedGia(): Network check has failed.\n" );
1005  return pNtkNew;
1006 }
1007 
1008 
1009 /**Function*************************************************************
1010 
1011  Synopsis [Converts the network from the AIG manager into ABC.]
1012 
1013  Description [This procedure should be called after seq sweeping,
1014  which changes the number of registers.]
1015 
1016  SideEffects []
1017 
1018  SeeAlso []
1019 
1020 ***********************************************************************/
1022 {
1023  Vec_Ptr_t * vNodes;
1024  Abc_Ntk_t * pNtkNew;
1025  Abc_Obj_t * pObjNew, * pObjOld;
1026  Aig_Obj_t * pObj, * pObjLo, * pObjLi;
1027  int i;
1028  assert( pMan->nAsserts == 0 );
1029  assert( pNtkOld->nBarBufs == 0 );
1030  assert( Aig_ManRegNum(pMan) <= Abc_NtkLatchNum(pNtkOld) );
1031  assert( Saig_ManPiNum(pMan) <= Abc_NtkCiNum(pNtkOld) );
1032  assert( Saig_ManPoNum(pMan) == Abc_NtkPoNum(pNtkOld) );
1033  assert( pMan->vCiNumsOrig != NULL );
1034  // perform strashing
1035  pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
1036  pNtkNew->nConstrs = pMan->nConstrs;
1037  pNtkNew->nBarBufs = pMan->nBarBufs;
1038  // duplicate the name and the spec
1039 // pNtkNew->pName = Extra_UtilStrsav(pMan->pName);
1040 // pNtkNew->pSpec = Extra_UtilStrsav(pMan->pSpec);
1041  Aig_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew);
1042  // create PIs
1043  Aig_ManForEachPiSeq( pMan, pObj, i )
1044  {
1045  pObjNew = Abc_NtkCreatePi( pNtkNew );
1046  pObj->pData = pObjNew;
1047  // find the name
1048  pObjOld = Abc_NtkCi( pNtkOld, Vec_IntEntry(pMan->vCiNumsOrig, i) );
1049  Abc_ObjAssignName( pObjNew, Abc_ObjName(pObjOld), NULL );
1050  }
1051  // create POs
1052  Aig_ManForEachPoSeq( pMan, pObj, i )
1053  {
1054  pObjNew = Abc_NtkCreatePo( pNtkNew );
1055  pObj->pData = pObjNew;
1056  // find the name
1057  pObjOld = Abc_NtkCo( pNtkOld, i );
1058  Abc_ObjAssignName( pObjNew, Abc_ObjName(pObjOld), NULL );
1059  }
1060  assert( Abc_NtkCiNum(pNtkNew) == Aig_ManCiNum(pMan) - Aig_ManRegNum(pMan) );
1061  assert( Abc_NtkCoNum(pNtkNew) == Aig_ManCoNum(pMan) - Aig_ManRegNum(pMan) );
1062  // create as many latches as there are registers in the manager
1063  Aig_ManForEachLiLoSeq( pMan, pObjLi, pObjLo, i )
1064  {
1065  pObjNew = Abc_NtkCreateLatch( pNtkNew );
1066  pObjLi->pData = Abc_NtkCreateBi( pNtkNew );
1067  pObjLo->pData = Abc_NtkCreateBo( pNtkNew );
1068  Abc_ObjAddFanin( pObjNew, (Abc_Obj_t *)pObjLi->pData );
1069  Abc_ObjAddFanin( (Abc_Obj_t *)pObjLo->pData, pObjNew );
1070  Abc_LatchSetInit0( pObjNew );
1071  // find the name
1072  pObjOld = Abc_NtkCi( pNtkOld, Vec_IntEntry(pMan->vCiNumsOrig, Saig_ManPiNum(pMan)+i) );
1073  Abc_ObjAssignName( (Abc_Obj_t *)pObjLo->pData, Abc_ObjName(pObjOld), NULL );
1074  // find the name
1075  pObjOld = Abc_NtkCo( pNtkOld, Saig_ManPoNum(pMan)+i );
1076  Abc_ObjAssignName( (Abc_Obj_t *)pObjLi->pData, Abc_ObjName(pObjOld), NULL );
1077  }
1078  // rebuild the AIG
1079  vNodes = Aig_ManDfs( pMan, 1 );
1080  Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
1081  if ( Aig_ObjIsBuf(pObj) )
1082  pObj->pData = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj);
1083  else
1084  pObj->pData = Abc_AigAnd( (Abc_Aig_t *)pNtkNew->pManFunc, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj), (Abc_Obj_t *)Aig_ObjChild1Copy(pObj) );
1085  Vec_PtrFree( vNodes );
1086  // connect the PO nodes
1087  Aig_ManForEachCo( pMan, pObj, i )
1088  {
1089  pObjNew = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj);
1090  Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), pObjNew );
1091  }
1092  // check the resulting AIG
1093  if ( !Abc_NtkCheck( pNtkNew ) )
1094  Abc_Print( 1, "Abc_NtkAfterTrim(): Network check has failed.\n" );
1095  return pNtkNew;
1096 }
1097 
1098 /**Function*************************************************************
1099 
1100  Synopsis [Converts the network from the AIG manager into ABC.]
1101 
1102  Description []
1103 
1104  SideEffects []
1105 
1106  SeeAlso []
1107 
1108 ***********************************************************************/
1110 {
1111  Abc_Ntk_t * pNtkNew;
1112  Aig_Obj_t * pObj, * pTemp;
1113  int i;
1114  assert( pMan->pEquivs != NULL );
1115  assert( Aig_ManBufNum(pMan) == 0 );
1116  // perform strashing
1117  pNtkNew = Abc_NtkStartFrom( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
1118  pNtkNew->nConstrs = pMan->nConstrs;
1119  pNtkNew->nBarBufs = pNtkOld->nBarBufs;
1120  // transfer the pointers to the basic nodes
1121  Aig_ManCleanData( pMan );
1122  Aig_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew);
1123  Aig_ManForEachCi( pMan, pObj, i )
1124  pObj->pData = Abc_NtkCi(pNtkNew, i);
1125  // rebuild the AIG
1126  Aig_ManForEachNode( pMan, pObj, i )
1127  {
1128  pObj->pData = Abc_AigAnd( (Abc_Aig_t *)pNtkNew->pManFunc, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj), (Abc_Obj_t *)Aig_ObjChild1Copy(pObj) );
1129  if ( (pTemp = Aig_ObjEquiv(pMan, pObj)) )
1130  {
1131  assert( pTemp->pData != NULL );
1132  ((Abc_Obj_t *)pObj->pData)->pData = ((Abc_Obj_t *)pTemp->pData);
1133  }
1134  }
1135  // connect the PO nodes
1136  Aig_ManForEachCo( pMan, pObj, i )
1137  Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), (Abc_Obj_t *)Aig_ObjChild0Copy(pObj) );
1138  if ( !Abc_NtkCheck( pNtkNew ) )
1139  Abc_Print( 1, "Abc_NtkFromDar(): Network check has failed.\n" );
1140 
1141  // verify topological order
1142  if ( 0 )
1143  {
1144  Abc_Obj_t * pNode;
1145  Abc_NtkForEachNode( pNtkNew, pNode, i )
1146  if ( Abc_AigNodeIsChoice( pNode ) )
1147  {
1148  int Counter = 0;
1149  for ( pNode = Abc_ObjEquiv(pNode); pNode; pNode = Abc_ObjEquiv(pNode) )
1150  Counter++;
1151  printf( "%d ", Counter );
1152  }
1153  printf( "\n" );
1154  }
1155  return pNtkNew;
1156 }
1157 
1158 /**Function*************************************************************
1159 
1160  Synopsis [Converts the network from the AIG manager into ABC.]
1161 
1162  Description []
1163 
1164  SideEffects []
1165 
1166  SeeAlso []
1167 
1168 ***********************************************************************/
1170 {
1171  Vec_Ptr_t * vNodes;
1172  Abc_Ntk_t * pNtkNew;
1173  Abc_Obj_t * pObjNew, * pFaninNew, * pFaninNew0, * pFaninNew1;
1174  Aig_Obj_t * pObj;
1175  int i;
1176 // assert( Aig_ManLatchNum(pMan) > 0 );
1177  assert( pNtkOld->nBarBufs == 0 );
1178  // perform strashing
1179  pNtkNew = Abc_NtkStartFromNoLatches( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
1180  pNtkNew->nConstrs = pMan->nConstrs;
1181  pNtkNew->nBarBufs = pMan->nBarBufs;
1182  // transfer the pointers to the basic nodes
1183  Aig_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew);
1184  Aig_ManForEachCi( pMan, pObj, i )
1185  pObj->pData = Abc_NtkPi(pNtkNew, i);
1186  // create latches of the new network
1187  Aig_ManForEachObj( pMan, pObj, i )
1188  {
1189  pObjNew = Abc_NtkCreateLatch( pNtkNew );
1190  pFaninNew0 = Abc_NtkCreateBi( pNtkNew );
1191  pFaninNew1 = Abc_NtkCreateBo( pNtkNew );
1192  Abc_ObjAddFanin( pObjNew, pFaninNew0 );
1193  Abc_ObjAddFanin( pFaninNew1, pObjNew );
1194  Abc_LatchSetInit0( pObjNew );
1195  pObj->pData = Abc_ObjFanout0( pObjNew );
1196  }
1197  Abc_NtkAddDummyBoxNames( pNtkNew );
1198  // rebuild the AIG
1199  vNodes = Aig_ManDfs( pMan, 1 );
1200  Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
1201  {
1202  // add the first fanin
1203  pObj->pData = pFaninNew0 = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj);
1204  if ( Aig_ObjIsBuf(pObj) )
1205  continue;
1206  // add the second fanin
1207  pFaninNew1 = (Abc_Obj_t *)Aig_ObjChild1Copy(pObj);
1208  // create the new node
1209  if ( Aig_ObjIsExor(pObj) )
1210  pObj->pData = pObjNew = Abc_AigXor( (Abc_Aig_t *)pNtkNew->pManFunc, pFaninNew0, pFaninNew1 );
1211  else
1212  pObj->pData = pObjNew = Abc_AigAnd( (Abc_Aig_t *)pNtkNew->pManFunc, pFaninNew0, pFaninNew1 );
1213  }
1214  Vec_PtrFree( vNodes );
1215  // connect the PO nodes
1216  Aig_ManForEachCo( pMan, pObj, i )
1217  {
1218  pFaninNew = (Abc_Obj_t *)Aig_ObjChild0Copy( pObj );
1219  Abc_ObjAddFanin( Abc_NtkPo(pNtkNew, i), pFaninNew );
1220  }
1221  // connect the latches
1222  Aig_ManForEachObj( pMan, pObj, i )
1223  {
1224  pFaninNew = (Abc_Obj_t *)Aig_ObjChild0Copy( pObj );
1225  Abc_ObjAddFanin( Abc_ObjFanin0(Abc_ObjFanin0((Abc_Obj_t *)pObj->pData)), pFaninNew );
1226  }
1227  if ( !Abc_NtkCheck( pNtkNew ) )
1228  Abc_Print( 1, "Abc_NtkFromIvySeq(): Network check has failed.\n" );
1229  return pNtkNew;
1230 }
1231 
1232 /**Function*************************************************************
1233 
1234  Synopsis [Collects CI of the network.]
1235 
1236  Description []
1237 
1238  SideEffects []
1239 
1240  SeeAlso []
1241 
1242 ***********************************************************************/
1244 {
1245  Abc_Obj_t * pObj;
1246  int i;
1247  Vec_Ptr_t * vNames;
1248  vNames = Vec_PtrAlloc( 100 );
1249  Abc_NtkForEachCi( pNtk, pObj, i )
1250  Vec_PtrPush( vNames, Extra_UtilStrsav(Abc_ObjName(pObj)) );
1251  return vNames;
1252 }
1253 
1254 /**Function*************************************************************
1255 
1256  Synopsis [Collects CO of the network.]
1257 
1258  Description []
1259 
1260  SideEffects []
1261 
1262  SeeAlso []
1263 
1264 ***********************************************************************/
1266 {
1267  Abc_Obj_t * pObj;
1268  int i;
1269  Vec_Ptr_t * vNames;
1270  vNames = Vec_PtrAlloc( 100 );
1271  Abc_NtkForEachCo( pNtk, pObj, i )
1272  Vec_PtrPush( vNames, Extra_UtilStrsav(Abc_ObjName(pObj)) );
1273  return vNames;
1274 }
1275 
1276 /**Function*************************************************************
1277 
1278  Synopsis [Collect latch values.]
1279 
1280  Description []
1281 
1282  SideEffects []
1283 
1284  SeeAlso []
1285 
1286 ***********************************************************************/
1288 {
1289  Vec_Int_t * vInits;
1290  Abc_Obj_t * pLatch;
1291  int i;
1292  vInits = Vec_IntAlloc( Abc_NtkLatchNum(pNtk) );
1293  Abc_NtkForEachLatch( pNtk, pLatch, i )
1294  {
1295  if ( Abc_LatchIsInit0(pLatch) )
1296  Vec_IntPush( vInits, 0 );
1297  else if ( Abc_LatchIsInit1(pLatch) )
1298  Vec_IntPush( vInits, 1 );
1299  else if ( Abc_LatchIsInitDc(pLatch) )
1300  Vec_IntPush( vInits, 2 );
1301  else
1302  assert( 0 );
1303  }
1304  return vInits;
1305 }
1306 
1307 /**Function*************************************************************
1308 
1309  Synopsis [Gives the current ABC network to AIG manager for processing.]
1310 
1311  Description []
1312 
1313  SideEffects []
1314 
1315  SeeAlso []
1316 
1317 ***********************************************************************/
1319 {
1320  Abc_Ntk_t * pNtkAig = NULL;
1321  Aig_Man_t * pMan;
1322  extern void Fra_ManPartitionTest( Aig_Man_t * p, int nComLim );
1323 
1324  assert( Abc_NtkIsStrash(pNtk) );
1325  // convert to the AIG manager
1326  pMan = Abc_NtkToDar( pNtk, 0, 0 );
1327  if ( pMan == NULL )
1328  return NULL;
1329 
1330  // perform computation
1331 // Fra_ManPartitionTest( pMan, 4 );
1332  pNtkAig = Abc_NtkFromDar( pNtk, pMan );
1333  Aig_ManStop( pMan );
1334 
1335  // make sure everything is okay
1336  if ( pNtkAig && !Abc_NtkCheck( pNtkAig ) )
1337  {
1338  Abc_Print( 1, "Abc_NtkDar: The network check has failed.\n" );
1339  Abc_NtkDelete( pNtkAig );
1340  return NULL;
1341  }
1342  return pNtkAig;
1343 }
1344 
1345 
1346 /**Function*************************************************************
1347 
1348  Synopsis [Gives the current ABC network to AIG manager for processing.]
1349 
1350  Description []
1351 
1352  SideEffects []
1353 
1354  SeeAlso []
1355 
1356 ***********************************************************************/
1357 Abc_Ntk_t * Abc_NtkDarFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, int fProve, int fTransfer, int fSpeculate, int fChoicing, int fVerbose )
1358 {
1359  Fra_Par_t Pars, * pPars = &Pars;
1360  Abc_Ntk_t * pNtkAig;
1361  Aig_Man_t * pMan, * pTemp;
1362  pMan = Abc_NtkToDar( pNtk, 0, 0 );
1363  if ( pMan == NULL )
1364  return NULL;
1365  Fra_ParamsDefault( pPars );
1366  pPars->nBTLimitNode = nConfLimit;
1367  pPars->fChoicing = fChoicing;
1368  pPars->fDoSparse = fDoSparse;
1369  pPars->fSpeculate = fSpeculate;
1370  pPars->fProve = fProve;
1371  pPars->fVerbose = fVerbose;
1372  pMan = Fra_FraigPerform( pTemp = pMan, pPars );
1373  if ( fChoicing )
1374  pNtkAig = Abc_NtkFromDarChoices( pNtk, pMan );
1375  else
1376  pNtkAig = Abc_NtkFromDar( pNtk, pMan );
1377  Aig_ManStop( pTemp );
1378  Aig_ManStop( pMan );
1379  return pNtkAig;
1380 }
1381 
1382 /**Function*************************************************************
1383 
1384  Synopsis [Gives the current ABC network to AIG manager for processing.]
1385 
1386  Description []
1387 
1388  SideEffects []
1389 
1390  SeeAlso []
1391 
1392 ***********************************************************************/
1393 Abc_Ntk_t * Abc_NtkDarFraigPart( Abc_Ntk_t * pNtk, int nPartSize, int nConfLimit, int nLevelMax, int fVerbose )
1394 {
1395  Abc_Ntk_t * pNtkAig;
1396  Aig_Man_t * pMan, * pTemp;
1397  pMan = Abc_NtkToDar( pNtk, 0, 0 );
1398  if ( pMan == NULL )
1399  return NULL;
1400  pMan = Aig_ManFraigPartitioned( pTemp = pMan, nPartSize, nConfLimit, nLevelMax, fVerbose );
1401  Aig_ManStop( pTemp );
1402  pNtkAig = Abc_NtkFromDar( pNtk, pMan );
1403  Aig_ManStop( pMan );
1404  return pNtkAig;
1405 }
1406 
1407 /**Function*************************************************************
1408 
1409  Synopsis [Gives the current ABC network to AIG manager for processing.]
1410 
1411  Description []
1412 
1413  SideEffects []
1414 
1415  SeeAlso []
1416 
1417 ***********************************************************************/
1418 Abc_Ntk_t * Abc_NtkCSweep( Abc_Ntk_t * pNtk, int nCutsMax, int nLeafMax, int fVerbose )
1419 {
1420 // extern Aig_Man_t * Csw_Sweep( Aig_Man_t * pAig, int nCutsMax, int nLeafMax, int fVerbose );
1421  Abc_Ntk_t * pNtkAig;
1422  Aig_Man_t * pMan, * pTemp;
1423  pMan = Abc_NtkToDar( pNtk, 0, 0 );
1424  if ( pMan == NULL )
1425  return NULL;
1426  pMan = Csw_Sweep( pTemp = pMan, nCutsMax, nLeafMax, fVerbose );
1427  pNtkAig = Abc_NtkFromDar( pNtk, pMan );
1428  Aig_ManStop( pTemp );
1429  Aig_ManStop( pMan );
1430  return pNtkAig;
1431 }
1432 
1433 /**Function*************************************************************
1434 
1435  Synopsis [Gives the current ABC network to AIG manager for processing.]
1436 
1437  Description []
1438 
1439  SideEffects []
1440 
1441  SeeAlso []
1442 
1443 ***********************************************************************/
1445 {
1446  Aig_Man_t * pMan, * pTemp;
1447  Abc_Ntk_t * pNtkAig;
1448  abctime clk;
1449  assert( Abc_NtkIsStrash(pNtk) );
1450  pMan = Abc_NtkToDar( pNtk, 0, 0 );
1451  if ( pMan == NULL )
1452  return NULL;
1453 // Aig_ManPrintStats( pMan );
1454 /*
1455 // Aig_ManSupports( pMan );
1456  {
1457  Vec_Vec_t * vParts;
1458  vParts = Aig_ManPartitionSmart( pMan, 50, 1, NULL );
1459  Vec_VecFree( vParts );
1460  }
1461 */
1462  Dar_ManRewrite( pMan, pPars );
1463 // pMan = Dar_ManBalance( pTemp = pMan, pPars->fUpdateLevel );
1464 // Aig_ManStop( pTemp );
1465 
1466 clk = Abc_Clock();
1467  pMan = Aig_ManDupDfs( pTemp = pMan );
1468  Aig_ManStop( pTemp );
1469 //ABC_PRT( "time", Abc_Clock() - clk );
1470 
1471 // Aig_ManPrintStats( pMan );
1472  pNtkAig = Abc_NtkFromDar( pNtk, pMan );
1473  Aig_ManStop( pMan );
1474  return pNtkAig;
1475 }
1476 
1477 /**Function*************************************************************
1478 
1479  Synopsis [Gives the current ABC network to AIG manager for processing.]
1480 
1481  Description []
1482 
1483  SideEffects []
1484 
1485  SeeAlso []
1486 
1487 ***********************************************************************/
1489 {
1490  Aig_Man_t * pMan, * pTemp;
1491  Abc_Ntk_t * pNtkAig;
1492  abctime clk;
1493  assert( Abc_NtkIsStrash(pNtk) );
1494  pMan = Abc_NtkToDar( pNtk, 0, 0 );
1495  if ( pMan == NULL )
1496  return NULL;
1497 // Aig_ManPrintStats( pMan );
1498 
1499  Dar_ManRefactor( pMan, pPars );
1500 // pMan = Dar_ManBalance( pTemp = pMan, pPars->fUpdateLevel );
1501 // Aig_ManStop( pTemp );
1502 
1503 clk = Abc_Clock();
1504  pMan = Aig_ManDupDfs( pTemp = pMan );
1505  Aig_ManStop( pTemp );
1506 //ABC_PRT( "time", Abc_Clock() - clk );
1507 
1508 // Aig_ManPrintStats( pMan );
1509  pNtkAig = Abc_NtkFromDar( pNtk, pMan );
1510  Aig_ManStop( pMan );
1511  return pNtkAig;
1512 }
1513 
1514 /**Function*************************************************************
1515 
1516  Synopsis [Gives the current ABC network to AIG manager for processing.]
1517 
1518  Description []
1519 
1520  SideEffects []
1521 
1522  SeeAlso []
1523 
1524 ***********************************************************************/
1525 Abc_Ntk_t * Abc_NtkDC2( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int fFanout, int fPower, int fVerbose )
1526 {
1527  Aig_Man_t * pMan, * pTemp;
1528  Abc_Ntk_t * pNtkAig;
1529  abctime clk;
1530  assert( Abc_NtkIsStrash(pNtk) );
1531  pMan = Abc_NtkToDar( pNtk, 0, 0 );
1532  if ( pMan == NULL )
1533  return NULL;
1534 // Aig_ManPrintStats( pMan );
1535 
1536 clk = Abc_Clock();
1537  pMan = Dar_ManCompress2( pTemp = pMan, fBalance, fUpdateLevel, fFanout, fPower, fVerbose );
1538  Aig_ManStop( pTemp );
1539 //ABC_PRT( "time", Abc_Clock() - clk );
1540 
1541 // Aig_ManPrintStats( pMan );
1542  pNtkAig = Abc_NtkFromDar( pNtk, pMan );
1543  Aig_ManStop( pMan );
1544  return pNtkAig;
1545 }
1546 
1547 /**Function*************************************************************
1548 
1549  Synopsis [Gives the current ABC network to AIG manager for processing.]
1550 
1551  Description []
1552 
1553  SideEffects []
1554 
1555  SeeAlso []
1556 
1557 ***********************************************************************/
1558 Abc_Ntk_t * Abc_NtkDChoice( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int fConstruct, int nConfMax, int nLevelMax, int fVerbose )
1559 {
1560  Aig_Man_t * pMan, * pTemp;
1561  Abc_Ntk_t * pNtkAig;
1562  assert( Abc_NtkIsStrash(pNtk) );
1563  pMan = Abc_NtkToDar( pNtk, 0, 0 );
1564  if ( pMan == NULL )
1565  return NULL;
1566  pMan = Dar_ManChoice( pTemp = pMan, fBalance, fUpdateLevel, fConstruct, nConfMax, nLevelMax, fVerbose );
1567  Aig_ManStop( pTemp );
1568  pNtkAig = Abc_NtkFromDarChoices( pNtk, pMan );
1569  Aig_ManStop( pMan );
1570  return pNtkAig;
1571 }
1572 
1573 /**Function*************************************************************
1574 
1575  Synopsis [Gives the current ABC network to AIG manager for processing.]
1576 
1577  Description []
1578 
1579  SideEffects []
1580 
1581  SeeAlso []
1582 
1583 ***********************************************************************/
1585 {
1586  extern Gia_Man_t * Dar_NewChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fPower, int fLightSynth, int fVerbose );
1587  extern Aig_Man_t * Cec_ComputeChoices( Gia_Man_t * pGia, Dch_Pars_t * pPars );
1588 
1589  Aig_Man_t * pMan, * pTemp;
1590  Abc_Ntk_t * pNtkAig;
1591  Gia_Man_t * pGia;
1592  abctime clk;
1593  assert( Abc_NtkIsStrash(pNtk) );
1594  pMan = Abc_NtkToDar( pNtk, 0, 0 );
1595  if ( pMan == NULL )
1596  return NULL;
1597 clk = Abc_Clock();
1598  if ( pPars->fSynthesis )
1599  pGia = Dar_NewChoiceSynthesis( pMan, 1, 1, pPars->fPower, pPars->fLightSynth, pPars->fVerbose );
1600  else
1601  {
1602  pGia = Gia_ManFromAig( pMan );
1603  Aig_ManStop( pMan );
1604  }
1605 pPars->timeSynth = Abc_Clock() - clk;
1606  if ( pPars->fUseGia )
1607  pMan = Cec_ComputeChoices( pGia, pPars );
1608  else
1609  {
1610  pMan = Gia_ManToAigSkip( pGia, 3 );
1611  Gia_ManStop( pGia );
1612  pMan = Dch_ComputeChoices( pTemp = pMan, pPars );
1613  Aig_ManStop( pTemp );
1614  }
1615  pNtkAig = Abc_NtkFromDarChoices( pNtk, pMan );
1616  Aig_ManStop( pMan );
1617  return pNtkAig;
1618 }
1619 
1620 /**Function*************************************************************
1621 
1622  Synopsis [Gives the current ABC network to AIG manager for processing.]
1623 
1624  Description []
1625 
1626  SideEffects []
1627 
1628  SeeAlso []
1629 
1630 ***********************************************************************/
1631 Abc_Ntk_t * Abc_NtkDrwsat( Abc_Ntk_t * pNtk, int fBalance, int fVerbose )
1632 {
1633  Aig_Man_t * pMan, * pTemp;
1634  Abc_Ntk_t * pNtkAig;
1635  abctime clk;
1636  assert( Abc_NtkIsStrash(pNtk) );
1637  pMan = Abc_NtkToDar( pNtk, 0, 0 );
1638  if ( pMan == NULL )
1639  return NULL;
1640 // Aig_ManPrintStats( pMan );
1641 
1642 clk = Abc_Clock();
1643  pMan = Dar_ManRwsat( pTemp = pMan, fBalance, fVerbose );
1644  Aig_ManStop( pTemp );
1645 //ABC_PRT( "time", Abc_Clock() - clk );
1646 
1647 // Aig_ManPrintStats( pMan );
1648  pNtkAig = Abc_NtkFromDar( pNtk, pMan );
1649  Aig_ManStop( pMan );
1650  return pNtkAig;
1651 }
1652 
1653 /**Function*************************************************************
1654 
1655  Synopsis [Gives the current ABC network to AIG manager for processing.]
1656 
1657  Description []
1658 
1659  SideEffects []
1660 
1661  SeeAlso []
1662 
1663 ***********************************************************************/
1665 {
1666  Abc_Ntk_t * pNtkNew;
1667  Abc_Obj_t * pNode, * pNodeNew;
1668  Aig_Obj_t * pObj, * pLeaf;
1669  Cnf_Cut_t * pCut;
1670  Vec_Int_t * vCover;
1671  unsigned uTruth;
1672  int i, k, nDupGates;
1673  // create the new network
1674  pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP );
1675  // make the mapper point to the new network
1676  Aig_ManConst1(p->pManAig)->pData = Abc_NtkCreateNodeConst1(pNtkNew);
1677  Abc_NtkForEachCi( pNtk, pNode, i )
1678  Aig_ManCi(p->pManAig, i)->pData = pNode->pCopy;
1679  // process the nodes in topological order
1680  vCover = Vec_IntAlloc( 1 << 16 );
1681  Vec_PtrForEachEntry( Aig_Obj_t *, vMapped, pObj, i )
1682  {
1683  // create new node
1684  pNodeNew = Abc_NtkCreateNode( pNtkNew );
1685  // add fanins according to the cut
1686  pCut = (Cnf_Cut_t *)pObj->pData;
1687  Cnf_CutForEachLeaf( p->pManAig, pCut, pLeaf, k )
1688  Abc_ObjAddFanin( pNodeNew, (Abc_Obj_t *)pLeaf->pData );
1689  // add logic function
1690  if ( pCut->nFanins < 5 )
1691  {
1692  uTruth = 0xFFFF & *Cnf_CutTruth(pCut);
1693  Cnf_SopConvertToVector( p->pSops[uTruth], p->pSopSizes[uTruth], vCover );
1694  pNodeNew->pData = Abc_SopCreateFromIsop( (Mem_Flex_t *)pNtkNew->pManFunc, pCut->nFanins, vCover );
1695  }
1696  else
1697  pNodeNew->pData = Abc_SopCreateFromIsop( (Mem_Flex_t *)pNtkNew->pManFunc, pCut->nFanins, pCut->vIsop[1] );
1698  // save the node
1699  pObj->pData = pNodeNew;
1700  }
1701  Vec_IntFree( vCover );
1702  // add the CO drivers
1703  Abc_NtkForEachCo( pNtk, pNode, i )
1704  {
1705  pObj = Aig_ManCo(p->pManAig, i);
1706  pNodeNew = Abc_ObjNotCond( (Abc_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
1707  Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
1708  }
1709 
1710  // remove the constant node if not used
1711  pNodeNew = (Abc_Obj_t *)Aig_ManConst1(p->pManAig)->pData;
1712  if ( Abc_ObjFanoutNum(pNodeNew) == 0 )
1713  Abc_NtkDeleteObj( pNodeNew );
1714  // minimize the node
1715 // Abc_NtkSweep( pNtkNew, 0 );
1716  // decouple the PO driver nodes to reduce the number of levels
1717  nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 );
1718 // if ( nDupGates && If_ManReadVerbose(pIfMan) )
1719 // Abc_Print( 1, "Duplicated %d gates to decouple the CO drivers.\n", nDupGates );
1720  if ( !Abc_NtkCheck( pNtkNew ) )
1721  Abc_Print( 1, "Abc_NtkConstructFromCnf(): Network check has failed.\n" );
1722  return pNtkNew;
1723 }
1724 
1725 /**Function*************************************************************
1726 
1727  Synopsis [Gives the current ABC network to AIG manager for processing.]
1728 
1729  Description []
1730 
1731  SideEffects []
1732 
1733  SeeAlso []
1734 
1735 ***********************************************************************/
1736 Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName, int fFastAlgo, int fChangePol, int fVerbose )
1737 {
1738 // Vec_Ptr_t * vMapped = NULL;
1739  Aig_Man_t * pMan;
1740 // Cnf_Man_t * pManCnf = NULL;
1741  Cnf_Dat_t * pCnf;
1742  Abc_Ntk_t * pNtkNew = NULL;
1743  abctime clk = Abc_Clock();
1744  assert( Abc_NtkIsStrash(pNtk) );
1745 
1746  // convert to the AIG manager
1747  pMan = Abc_NtkToDar( pNtk, 0, 0 );
1748  if ( pMan == NULL )
1749  return NULL;
1750  if ( !Aig_ManCheck( pMan ) )
1751  {
1752  Abc_Print( 1, "Abc_NtkDarToCnf: AIG check has failed.\n" );
1753  Aig_ManStop( pMan );
1754  return NULL;
1755  }
1756  // perform balance
1757  if ( fVerbose )
1758  Aig_ManPrintStats( pMan );
1759 
1760  // derive CNF
1761  if ( fFastAlgo )
1762  pCnf = Cnf_DeriveFast( pMan, 0 );
1763  else
1764  pCnf = Cnf_Derive( pMan, 0 );
1765 
1766  // adjust polarity
1767  if ( fChangePol )
1768  Cnf_DataTranformPolarity( pCnf, 0 );
1769 
1770  // print stats
1771 // if ( fVerbose )
1772  {
1773  Abc_Print( 1, "CNF stats: Vars = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );
1774  Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
1775  }
1776 
1777 /*
1778  // write the network for verification
1779  pManCnf = Cnf_ManRead();
1780  vMapped = Cnf_ManScanMapping( pManCnf, 1, 0 );
1781  pNtkNew = Abc_NtkConstructFromCnf( pNtk, pManCnf, vMapped );
1782  Vec_PtrFree( vMapped );
1783 */
1784  // write CNF into a file
1785  Cnf_DataWriteIntoFile( pCnf, pFileName, 0, NULL, NULL );
1786  Cnf_DataFree( pCnf );
1787  Cnf_ManFree();
1788  Aig_ManStop( pMan );
1789  return pNtkNew;
1790 }
1791 
1792 
1793 /**Function*************************************************************
1794 
1795  Synopsis [Solves combinational miter using a SAT solver.]
1796 
1797  Description []
1798 
1799  SideEffects []
1800 
1801  SeeAlso []
1802 
1803 ***********************************************************************/
1804 int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fAlignPol, int fAndOuts, int fNewSolver, int fVerbose )
1805 {
1806  Aig_Man_t * pMan;
1807  int RetValue;//, clk = Abc_Clock();
1808  assert( Abc_NtkIsStrash(pNtk) );
1809  assert( Abc_NtkLatchNum(pNtk) == 0 );
1810 // assert( Abc_NtkPoNum(pNtk) == 1 );
1811  pMan = Abc_NtkToDar( pNtk, 0, 0 );
1812  RetValue = Fra_FraigSat( pMan, nConfLimit, nInsLimit, nLearnedStart, nLearnedDelta, nLearnedPerce, fAlignPol, fAndOuts, fNewSolver, fVerbose );
1813  pNtk->pModel = (int *)pMan->pData, pMan->pData = NULL;
1814  Aig_ManStop( pMan );
1815  return RetValue;
1816 }
1817 
1818 /**Function*************************************************************
1819 
1820  Synopsis [Solves combinational miter using a SAT solver.]
1821 
1822  Description []
1823 
1824  SideEffects []
1825 
1826  SeeAlso []
1827 
1828 ***********************************************************************/
1829 int Abc_NtkPartitionedSat( Abc_Ntk_t * pNtk, int nAlgo, int nPartSize, int nConfPart, int nConfTotal, int fAlignPol, int fSynthesize, int fVerbose )
1830 {
1831  extern int Aig_ManPartitionedSat( Aig_Man_t * pNtk, int nAlgo, int nPartSize, int nConfPart, int nConfTotal, int fAlignPol, int fSynthesize, int fVerbose );
1832  Aig_Man_t * pMan;
1833  int RetValue;//, clk = Abc_Clock();
1834  assert( Abc_NtkIsStrash(pNtk) );
1835  assert( Abc_NtkLatchNum(pNtk) == 0 );
1836  pMan = Abc_NtkToDar( pNtk, 0, 0 );
1837  RetValue = Aig_ManPartitionedSat( pMan, nAlgo, nPartSize, nConfPart, nConfTotal, fAlignPol, fSynthesize, fVerbose );
1838  pNtk->pModel = (int *)pMan->pData, pMan->pData = NULL;
1839  Aig_ManStop( pMan );
1840  return RetValue;
1841 }
1842 
1843 /**Function*************************************************************
1844 
1845  Synopsis [Gives the current ABC network to AIG manager for processing.]
1846 
1847  Description []
1848 
1849  SideEffects []
1850 
1851  SeeAlso []
1852 
1853 ***********************************************************************/
1854 int Abc_NtkDarCec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int fPartition, int fVerbose )
1855 {
1856  Aig_Man_t * pMan, * pMan1, * pMan2;
1857  Abc_Ntk_t * pMiter;
1858  int RetValue;
1859  abctime clkTotal = Abc_Clock();
1860 /*
1861  {
1862  extern void Cec_ManVerifyTwoAigs( Aig_Man_t * pAig0, Aig_Man_t * pAig1, int fVerbose );
1863  Aig_Man_t * pAig0 = Abc_NtkToDar( pNtk1, 0, 0 );
1864  Aig_Man_t * pAig1 = Abc_NtkToDar( pNtk2, 0, 0 );
1865  Cec_ManVerifyTwoAigs( pAig0, pAig1, 1 );
1866  Aig_ManStop( pAig0 );
1867  Aig_ManStop( pAig1 );
1868  return 1;
1869  }
1870 */
1871  // cannot partition if it is already a miter
1872  if ( pNtk2 == NULL && fPartition == 1 )
1873  {
1874  Abc_Print( 1, "Abc_NtkDarCec(): Switching to non-partitioned CEC for the miter.\n" );
1875  fPartition = 0;
1876  }
1877 
1878  // if partitioning is selected, call partitioned CEC
1879  if ( fPartition )
1880  {
1881  pMan1 = Abc_NtkToDar( pNtk1, 0, 0 );
1882  pMan2 = Abc_NtkToDar( pNtk2, 0, 0 );
1883  RetValue = Fra_FraigCecPartitioned( pMan1, pMan2, nConfLimit, 100, 1, fVerbose );
1884  Aig_ManStop( pMan1 );
1885  Aig_ManStop( pMan2 );
1886  goto finish;
1887  }
1888 
1889  if ( pNtk2 != NULL )
1890  {
1891  // get the miter of the two networks
1892  pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0, 0, 0, 0 );
1893  if ( pMiter == NULL )
1894  {
1895  Abc_Print( 1, "Miter computation has failed.\n" );
1896  return 0;
1897  }
1898  }
1899  else
1900  {
1901  pMiter = Abc_NtkDup( pNtk1 );
1902  }
1903  RetValue = Abc_NtkMiterIsConstant( pMiter );
1904  if ( RetValue == 0 )
1905  {
1906 // extern void Abc_NtkVerifyReportErrorSeq( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel, int nFrames );
1907  Abc_Print( 1, "Networks are NOT EQUIVALENT after structural hashing.\n" );
1908  // report the error
1909  if ( pNtk2 == NULL )
1910  pNtk1->pModel = Abc_NtkVerifyGetCleanModel( pNtk1, 1 );
1911 // pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, nFrames );
1912 // Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, pMiter->pModel, nFrames );
1913 // ABC_FREE( pMiter->pModel );
1914  Abc_NtkDelete( pMiter );
1915  return 0;
1916  }
1917  if ( RetValue == 1 )
1918  {
1919  Abc_NtkDelete( pMiter );
1920  Abc_Print( 1, "Networks are equivalent after structural hashing.\n" );
1921  return 1;
1922  }
1923 
1924  // derive the AIG manager
1925  pMan = Abc_NtkToDar( pMiter, 0, 0 );
1926  Abc_NtkDelete( pMiter );
1927  if ( pMan == NULL )
1928  {
1929  Abc_Print( 1, "Converting miter into AIG has failed.\n" );
1930  return -1;
1931  }
1932  // perform verification
1933  RetValue = Fra_FraigCec( &pMan, 100000, fVerbose );
1934  // transfer model if given
1935  if ( pNtk2 == NULL )
1936  pNtk1->pModel = (int *)pMan->pData, pMan->pData = NULL;
1937  Aig_ManStop( pMan );
1938 
1939 finish:
1940  // report the miter
1941  if ( RetValue == 1 )
1942  {
1943  Abc_Print( 1, "Networks are equivalent. " );
1944 ABC_PRT( "Time", Abc_Clock() - clkTotal );
1945  }
1946  else if ( RetValue == 0 )
1947  {
1948  Abc_Print( 1, "Networks are NOT EQUIVALENT. " );
1949 ABC_PRT( "Time", Abc_Clock() - clkTotal );
1950  }
1951  else
1952  {
1953  Abc_Print( 1, "Networks are UNDECIDED. " );
1954 ABC_PRT( "Time", Abc_Clock() - clkTotal );
1955  }
1956  fflush( stdout );
1957  return RetValue;
1958 }
1959 
1960 /**Function*************************************************************
1961 
1962  Synopsis [Gives the current ABC network to AIG manager for processing.]
1963 
1964  Description []
1965 
1966  SideEffects []
1967 
1968  SeeAlso []
1969 
1970 ***********************************************************************/
1972 {
1973  Fraig_Params_t Params;
1974  Abc_Ntk_t * pNtkAig = NULL, * pNtkFraig;
1975  Aig_Man_t * pMan, * pTemp;
1976  abctime clk = Abc_Clock();
1977 
1978  // preprocess the miter by fraiging it
1979  // (note that for each functional class, fraiging leaves one representative;
1980  // so fraiging does not reduce the number of functions represented by nodes
1981  Fraig_ParamsSetDefault( &Params );
1982  Params.nBTLimit = 100000;
1983  if ( pPars->fFraiging && pPars->nPartSize == 0 )
1984  {
1985  pNtkFraig = Abc_NtkFraig( pNtk, &Params, 0, 0 );
1986 if ( pPars->fVerbose )
1987 {
1988 ABC_PRT( "Initial fraiging time", Abc_Clock() - clk );
1989 }
1990  }
1991  else
1992  pNtkFraig = Abc_NtkDup( pNtk );
1993 
1994  pMan = Abc_NtkToDar( pNtkFraig, 0, 1 );
1995  Abc_NtkDelete( pNtkFraig );
1996  if ( pMan == NULL )
1997  return NULL;
1998 
1999 // pPars->TimeLimit = 5.0;
2000  pMan = Fra_FraigInduction( pTemp = pMan, pPars );
2001  Aig_ManStop( pTemp );
2002  if ( pMan )
2003  {
2004  if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) )
2005  pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
2006  else
2007  {
2008  Abc_Obj_t * pObj;
2009  int i;
2010  pNtkAig = Abc_NtkFromDar( pNtk, pMan );
2011  Abc_NtkForEachLatch( pNtkAig, pObj, i )
2012  Abc_LatchSetInit0( pObj );
2013  }
2014  Aig_ManStop( pMan );
2015  }
2016  return pNtkAig;
2017 }
2018 
2019 /**Function*************************************************************
2020 
2021  Synopsis [Print Latch Equivalence Classes.]
2022 
2023  Description []
2024 
2025  SideEffects []
2026 
2027  SeeAlso []
2028 
2029 ***********************************************************************/
2031 {
2032  int header_dumped = 0;
2033  int num_orig_latches = Abc_NtkLatchNum(pNtk);
2034  char **pNames = ABC_ALLOC( char *, num_orig_latches );
2035  int *p_irrelevant = ABC_ALLOC( int, num_orig_latches );
2036  char * pFlopName, * pReprName;
2037  Aig_Obj_t * pFlop, * pRepr;
2038  Abc_Obj_t * pNtkFlop;
2039  int repr_idx;
2040  int i;
2041 
2042  Abc_NtkForEachLatch( pNtk, pNtkFlop, i )
2043  {
2044  char *temp_name = Abc_ObjName( Abc_ObjFanout0(pNtkFlop) );
2045  pNames[i] = ABC_ALLOC( char , strlen(temp_name)+1);
2046  strcpy(pNames[i], temp_name);
2047  }
2048  i = 0;
2049 
2050  Aig_ManSetCioIds( pAig );
2051  Saig_ManForEachLo( pAig, pFlop, i )
2052  {
2053  p_irrelevant[i] = false;
2054 
2055  pFlopName = pNames[i];
2056 
2057  pRepr = Aig_ObjRepr(pAig, pFlop);
2058 
2059  if ( pRepr == NULL )
2060  {
2061  // Abc_Print( 1, "Nothing equivalent to flop %s\n", pFlopName);
2062 // p_irrelevant[i] = true;
2063  continue;
2064  }
2065 
2066  if (!header_dumped)
2067  {
2068  Abc_Print( 1, "Here are the flop equivalences:\n");
2069  header_dumped = true;
2070  }
2071 
2072  // pRepr is representative of the equivalence class, to which pFlop belongs
2073  if ( Aig_ObjIsConst1(pRepr) )
2074  {
2075  Abc_Print( 1, "Original flop %s is proved equivalent to constant.\n", pFlopName );
2076  // Abc_Print( 1, "Original flop # %d is proved equivalent to constant.\n", i );
2077  continue;
2078  }
2079 
2080  assert( Saig_ObjIsLo( pAig, pRepr ) );
2081  repr_idx = Aig_ObjCioId(pRepr) - Saig_ManPiNum(pAig);
2082  pReprName = pNames[repr_idx];
2083  Abc_Print( 1, "Original flop %s is proved equivalent to flop %s.\n", pFlopName, pReprName );
2084  // Abc_Print( 1, "Original flop # %d is proved equivalent to flop # %d.\n", i, repr_idx );
2085  }
2086 
2087  header_dumped = false;
2088  for (i=0; i<num_orig_latches; ++i)
2089  {
2090  if (p_irrelevant[i])
2091  {
2092  if (!header_dumped)
2093  {
2094  Abc_Print( 1, "The following flops have been deemed irrelevant:\n");
2095  header_dumped = true;
2096  }
2097  Abc_Print( 1, "%s ", pNames[i]);
2098  }
2099 
2100  ABC_FREE(pNames[i]);
2101  }
2102  if (header_dumped)
2103  Abc_Print( 1, "\n");
2104 
2105  ABC_FREE(pNames);
2106  ABC_FREE(p_irrelevant);
2107 }
2108 
2109 /**Function*************************************************************
2110 
2111  Synopsis [Gives the current ABC network to AIG manager for processing.]
2112 
2113  Description []
2114 
2115  SideEffects []
2116 
2117  SeeAlso []
2118 
2119 ***********************************************************************/
2121 {
2122  Abc_Ntk_t * pNtkAig;
2123  Aig_Man_t * pMan, * pTemp;
2124 
2125  pMan = Abc_NtkToDar( pNtk, 0, 1 );
2126  if ( pMan == NULL )
2127  return NULL;
2128 
2129  pMan = Ssw_SignalCorrespondence( pTemp = pMan, pPars );
2130 
2131  if ( pPars->fFlopVerbose )
2132  Abc_NtkPrintLatchEquivClasses(pNtk, pTemp);
2133 
2134  Aig_ManStop( pTemp );
2135  if ( pMan == NULL )
2136  return NULL;
2137 
2138  if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) )
2139  pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
2140  else
2141  {
2142  Abc_Obj_t * pObj;
2143  int i;
2144  pNtkAig = Abc_NtkFromDar( pNtk, pMan );
2145  Abc_NtkForEachLatch( pNtkAig, pObj, i )
2146  Abc_LatchSetInit0( pObj );
2147  }
2148  Aig_ManStop( pMan );
2149  return pNtkAig;
2150 }
2151 
2152 /**Function*************************************************************
2153 
2154  Synopsis [Computes latch correspondence.]
2155 
2156  Description []
2157 
2158  SideEffects []
2159 
2160  SeeAlso []
2161 
2162 ***********************************************************************/
2163 Abc_Ntk_t * Abc_NtkDarLcorr( Abc_Ntk_t * pNtk, int nFramesP, int nConfMax, int fVerbose )
2164 {
2165  Aig_Man_t * pMan, * pTemp;
2166  Abc_Ntk_t * pNtkAig = NULL;
2167  pMan = Abc_NtkToDar( pNtk, 0, 1 );
2168  if ( pMan == NULL )
2169  return NULL;
2170  pMan = Fra_FraigLatchCorrespondence( pTemp = pMan, nFramesP, nConfMax, 0, fVerbose, NULL, 0.0 );
2171  Aig_ManStop( pTemp );
2172  if ( pMan )
2173  {
2174  if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) )
2175  pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
2176  else
2177  {
2178  Abc_Obj_t * pObj;
2179  int i;
2180  pNtkAig = Abc_NtkFromDar( pNtk, pMan );
2181  Abc_NtkForEachLatch( pNtkAig, pObj, i )
2182  Abc_LatchSetInit0( pObj );
2183  }
2184  Aig_ManStop( pMan );
2185  }
2186  return pNtkAig;
2187 }
2188 
2189 /**Function*************************************************************
2190 
2191  Synopsis [Computes latch correspondence.]
2192 
2193  Description []
2194 
2195  SideEffects []
2196 
2197  SeeAlso []
2198 
2199 ***********************************************************************/
2200 Abc_Ntk_t * Abc_NtkDarLcorrNew( Abc_Ntk_t * pNtk, int nVarsMax, int nConfMax, int fVerbose )
2201 {
2202  Ssw_Pars_t Pars, * pPars = &Pars;
2203  Aig_Man_t * pMan, * pTemp;
2204  Abc_Ntk_t * pNtkAig = NULL;
2205  pMan = Abc_NtkToDar( pNtk, 0, 1 );
2206  if ( pMan == NULL )
2207  return NULL;
2208  Ssw_ManSetDefaultParams( pPars );
2209  pPars->fLatchCorrOpt = 1;
2210  pPars->nBTLimit = nConfMax;
2211  pPars->nSatVarMax = nVarsMax;
2212  pPars->fVerbose = fVerbose;
2213  pMan = Ssw_SignalCorrespondence( pTemp = pMan, pPars );
2214  Aig_ManStop( pTemp );
2215  if ( pMan )
2216  {
2217  if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) )
2218  pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
2219  else
2220  {
2221  Abc_Obj_t * pObj;
2222  int i;
2223  pNtkAig = Abc_NtkFromDar( pNtk, pMan );
2224  Abc_NtkForEachLatch( pNtkAig, pObj, i )
2225  Abc_LatchSetInit0( pObj );
2226  }
2227  Aig_ManStop( pMan );
2228  }
2229  return pNtkAig;
2230 }
2231 
2232 /*
2233 #include <signal.h>
2234 #include "misc/util/utilMem.h"
2235 static void sigfunc( int signo )
2236 {
2237  if (signo == SIGINT) {
2238  Abc_Print( 1, "SIGINT received!\n");
2239  s_fInterrupt = 1;
2240  }
2241 }
2242 */
2243 
2244 /**Function*************************************************************
2245 
2246  Synopsis [Gives the current ABC network to AIG manager for processing.]
2247 
2248  Description []
2249 
2250  SideEffects []
2251 
2252  SeeAlso []
2253 
2254 ***********************************************************************/
2255 int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nStart, int nFrames, int nSizeMax, int nNodeDelta, int nTimeOut, int nBTLimit, int nBTLimitAll, int fRewrite, int fNewAlgo, int fOrDecomp, int nCofFanLit, int fVerbose, int * piFrames )
2256 {
2257  Aig_Man_t * pMan;
2258  Vec_Int_t * vMap = NULL;
2259  int status, RetValue = -1;
2260  abctime clk = Abc_Clock();
2261  abctime nTimeLimit = nTimeOut ? nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0;
2262  // derive the AIG manager
2263  if ( fOrDecomp )
2264  pMan = Abc_NtkToDarBmc( pNtk, &vMap );
2265  else
2266  pMan = Abc_NtkToDar( pNtk, 0, 1 );
2267  if ( pMan == NULL )
2268  {
2269  Abc_Print( 1, "Converting miter into AIG has failed.\n" );
2270  return RetValue;
2271  }
2272  assert( pMan->nRegs > 0 );
2273  assert( vMap == NULL || Vec_IntSize(vMap) == Saig_ManPoNum(pMan) );
2274  if ( fVerbose && vMap && Abc_NtkPoNum(pNtk) != Saig_ManPoNum(pMan) )
2275  Abc_Print( 1, "Expanded %d outputs into %d outputs using OR decomposition.\n", Abc_NtkPoNum(pNtk), Saig_ManPoNum(pMan) );
2276 
2277  // perform verification
2278  if ( fNewAlgo ) // command 'bmc'
2279  {
2280  int iFrame;
2281  RetValue = Saig_ManBmcSimple( pMan, nFrames, nSizeMax, nBTLimit, fRewrite, fVerbose, &iFrame, nCofFanLit );
2282  if ( piFrames )
2283  *piFrames = iFrame;
2284  ABC_FREE( pNtk->pModel );
2285  ABC_FREE( pNtk->pSeqModel );
2286  pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
2287  if ( RetValue == 1 )
2288  Abc_Print( 1, "Incorrect return value. " );
2289  else if ( RetValue == -1 )
2290  {
2291  Abc_Print( 1, "No output asserted in %d frames. Resource limit reached ", Abc_MaxInt(iFrame+1,0) );
2292  if ( nTimeLimit && Abc_Clock() > nTimeLimit )
2293  Abc_Print( 1, "(timeout %d sec). ", nTimeLimit );
2294  else
2295  Abc_Print( 1, "(conf limit %d). ", nBTLimit );
2296  }
2297  else // if ( RetValue == 0 )
2298  {
2299  Abc_Cex_t * pCex = pNtk->pSeqModel;
2300  Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pCex->iPo, pNtk->pName, pCex->iFrame );
2301  }
2302 ABC_PRT( "Time", Abc_Clock() - clk );
2303  }
2304  else
2305  {
2306  RetValue = Saig_BmcPerform( pMan, nStart, nFrames, nNodeDelta, nTimeOut, nBTLimit, nBTLimitAll, fVerbose, 0, piFrames, 0 );
2307  ABC_FREE( pNtk->pModel );
2308  ABC_FREE( pNtk->pSeqModel );
2309  pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
2310  }
2311  // verify counter-example
2312  if ( pNtk->pSeqModel )
2313  {
2314  status = Saig_ManVerifyCex( pMan, pNtk->pSeqModel );
2315  if ( status == 0 )
2316  Abc_Print( 1, "Abc_NtkDarBmc(): Counter-example verification has FAILED.\n" );
2317  }
2318  Aig_ManStop( pMan );
2319  // update the counter-example
2320  if ( pNtk->pSeqModel && vMap )
2321  pNtk->pSeqModel->iPo = Vec_IntEntry( vMap, pNtk->pSeqModel->iPo );
2322  Vec_IntFreeP( &vMap );
2323  return RetValue;
2324 }
2325 
2326 /**Function*************************************************************
2327 
2328  Synopsis []
2329 
2330  Description []
2331 
2332  SideEffects []
2333 
2334  SeeAlso []
2335 
2336 ***********************************************************************/
2337 int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars, int fOrDecomp )
2338 {
2339  Aig_Man_t * pMan;
2340  Vec_Int_t * vMap = NULL;
2341  int status, RetValue = -1;
2342  abctime clk = Abc_Clock();
2343  abctime nTimeOut = pPars->nTimeOut ? pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0;
2344  if ( fOrDecomp && !pPars->fSolveAll )
2345  pMan = Abc_NtkToDarBmc( pNtk, &vMap );
2346  else
2347  pMan = Abc_NtkToDar( pNtk, 0, 1 );
2348  if ( pMan == NULL )
2349  {
2350  Abc_Print( 1, "Converting miter into AIG has failed.\n" );
2351  return RetValue;
2352  }
2353  assert( pMan->nRegs > 0 );
2354  if ( pPars->fVerbose && vMap && Abc_NtkPoNum(pNtk) != Saig_ManPoNum(pMan) )
2355  Abc_Print( 1, "Expanded %d outputs into %d outputs using OR decomposition.\n", Abc_NtkPoNum(pNtk), Saig_ManPoNum(pMan) );
2356 
2357  RetValue = Saig_ManBmcScalable( pMan, pPars );
2358  ABC_FREE( pNtk->pModel );
2359  ABC_FREE( pNtk->pSeqModel );
2360  pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
2361  if ( !pPars->fSilent )
2362  {
2363  if ( RetValue == 1 )
2364  {
2365  Abc_Print( 1, "Explored all reachable states after completing %d frames. ", 1<<Aig_ManRegNum(pMan) );
2366  }
2367  else if ( RetValue == -1 )
2368  {
2369  if ( pPars->nFailOuts == 0 )
2370  {
2371  Abc_Print( 1, "No output asserted in %d frames. Resource limit reached ", Abc_MaxInt(pPars->iFrame+1,0) );
2372  if ( nTimeOut && Abc_Clock() > nTimeOut )
2373  Abc_Print( 1, "(timeout %d sec). ", pPars->nTimeOut );
2374  else
2375  Abc_Print( 1, "(conf limit %d). ", pPars->nConfLimit );
2376  }
2377  else
2378  {
2379  Abc_Print( 1, "The total of %d outputs asserted in %d frames. Resource limit reached ", pPars->nFailOuts, pPars->iFrame );
2380  if ( Abc_Clock() > nTimeOut )
2381  Abc_Print( 1, "(timeout %d sec). ", pPars->nTimeOut );
2382  else
2383  Abc_Print( 1, "(conf limit %d). ", pPars->nConfLimit );
2384  }
2385  }
2386  else // if ( RetValue == 0 )
2387  {
2388  if ( !pPars->fSolveAll )
2389  {
2390  Abc_Cex_t * pCex = pNtk->pSeqModel;
2391  Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pCex->iPo, pNtk->pName, pCex->iFrame );
2392  }
2393  else
2394  {
2395  int nOutputs = Saig_ManPoNum(pMan) - Saig_ManConstrNum(pMan);
2396  if ( pMan->vSeqModelVec == NULL || Vec_PtrCountZero(pMan->vSeqModelVec) == nOutputs )
2397  Abc_Print( 1, "None of the %d outputs is found to be SAT", nOutputs );
2398  else if ( Vec_PtrCountZero(pMan->vSeqModelVec) == 0 )
2399  Abc_Print( 1, "All %d outputs are found to be SAT", nOutputs );
2400  else
2401  {
2402  Abc_Print( 1, "Some outputs are SAT (%d out of %d)", nOutputs - Vec_PtrCountZero(pMan->vSeqModelVec), nOutputs );
2403  if ( pPars->nDropOuts )
2404  Abc_Print( 1, " while others timed out (%d out of %d)", pPars->nDropOuts, nOutputs );
2405  }
2406  Abc_Print( 1, " after %d frames", pPars->iFrame+2 );
2407  Abc_Print( 1, ". " );
2408  }
2409  }
2410  ABC_PRT( "Time", Abc_Clock() - clk );
2411  }
2412  if ( RetValue == 0 && pPars->fSolveAll )
2413  {
2414  if ( pNtk->vSeqModelVec )
2415  Vec_PtrFreeFree( pNtk->vSeqModelVec );
2416  pNtk->vSeqModelVec = pMan->vSeqModelVec; pMan->vSeqModelVec = NULL;
2417  }
2418  if ( pNtk->pSeqModel )
2419  {
2420  status = Saig_ManVerifyCex( pMan, pNtk->pSeqModel );
2421  if ( status == 0 )
2422  Abc_Print( 1, "Abc_NtkDarBmc3(): Counter-example verification has FAILED.\n" );
2423  }
2424  Aig_ManStop( pMan );
2425  // update the counter-example
2426  if ( pNtk->pSeqModel && vMap )
2427  pNtk->pSeqModel->iPo = Vec_IntEntry( vMap, pNtk->pSeqModel->iPo );
2428  Vec_IntFreeP( &vMap );
2429  return RetValue;
2430 }
2431 
2432 /**Function*************************************************************
2433 
2434  Synopsis [Gives the current ABC network to AIG manager for processing.]
2435 
2436  Description []
2437 
2438  SideEffects []
2439 
2440  SeeAlso []
2441 
2442 ***********************************************************************/
2444 {
2445  int RetValue = -1, iFrame;
2446  abctime clk = Abc_Clock();
2447  int nTotalProvedSat = 0;
2448  assert( pMan->nRegs > 0 );
2449  if ( ppNtkRes )
2450  *ppNtkRes = NULL;
2451  if ( pPars->fUseSeparate )
2452  {
2453  Aig_Man_t * pTemp, * pAux;
2454  Aig_Obj_t * pObjPo;
2455  int i, Counter = 0;
2456  Saig_ManForEachPo( pMan, pObjPo, i )
2457  {
2458  if ( Aig_ObjFanin0(pObjPo) == Aig_ManConst1(pMan) )
2459  continue;
2460  if ( pPars->fVerbose )
2461  Abc_Print( 1, "Solving output %2d (out of %2d):\n", i, Saig_ManPoNum(pMan) );
2462  pTemp = Aig_ManDupOneOutput( pMan, i, 1 );
2463  pTemp = Aig_ManScl( pAux = pTemp, 1, 1, 0, -1, -1, 0, 0 );
2464  Aig_ManStop( pAux );
2465  if ( Aig_ManRegNum(pTemp) == 0 )
2466  {
2467  pTemp->pSeqModel = NULL;
2468  RetValue = Fra_FraigSat( pTemp, pPars->nBTLimit, 0, 0, 0, 0, 0, 0, 0, 0 );
2469  if ( pTemp->pData )
2470  pTemp->pSeqModel = Abc_CexCreate( Aig_ManRegNum(pMan), Saig_ManPiNum(pMan), (int *)pTemp->pData, 0, i, 1 );
2471 // pNtk->pModel = pTemp->pData, pTemp->pData = NULL;
2472  }
2473  else
2474  RetValue = Inter_ManPerformInterpolation( pTemp, pPars, &iFrame );
2475  if ( pTemp->pSeqModel )
2476  {
2477  if ( pPars->fDropSatOuts )
2478  {
2479  Abc_Print( 1, "Output %d proved SAT in frame %d (replacing by const 0 and continuing...)\n", i, pTemp->pSeqModel->iFrame );
2480  Aig_ObjPatchFanin0( pMan, pObjPo, Aig_ManConst0(pMan) );
2481  Aig_ManStop( pTemp );
2482  nTotalProvedSat++;
2483  continue;
2484  }
2485  else
2486  {
2487  Abc_Cex_t * pCex;
2488  pCex = pMan->pSeqModel = pTemp->pSeqModel; pTemp->pSeqModel = NULL;
2489  pCex->iPo = i;
2490  Aig_ManStop( pTemp );
2491  break;
2492  }
2493  }
2494  // if solved, remove the output
2495  if ( RetValue == 1 )
2496  {
2497  Aig_ObjPatchFanin0( pMan, pObjPo, Aig_ManConst0(pMan) );
2498 // Abc_Print( 1, "Output %3d : Solved ", i );
2499  }
2500  else
2501  {
2502  Counter++;
2503 // Abc_Print( 1, "Output %3d : Undec ", i );
2504  }
2505 // Aig_ManPrintStats( pTemp );
2506  Aig_ManStop( pTemp );
2507  Abc_Print( 1, "Solving output %3d (out of %3d) using interpolation.\r", i, Saig_ManPoNum(pMan) );
2508  }
2509  Aig_ManCleanup( pMan );
2510  if ( pMan->pSeqModel == NULL )
2511  {
2512  Abc_Print( 1, "Interpolation left %d (out of %d) outputs unsolved \n", Counter, Saig_ManPoNum(pMan) );
2513  if ( Counter )
2514  RetValue = -1;
2515  }
2516  if ( ppNtkRes )
2517  {
2518  pTemp = Aig_ManDupUnsolvedOutputs( pMan, 1 );
2519  *ppNtkRes = Aig_ManScl( pTemp, 1, 1, 0, -1, -1, 0, 0 );
2520  Aig_ManStop( pTemp );
2521  }
2522  }
2523  else
2524  {
2525  RetValue = Inter_ManPerformInterpolation( pMan, pPars, &iFrame );
2526  }
2527  if ( nTotalProvedSat )
2528  Abc_Print( 1, "The total of %d outputs proved SAT and replaced by const 0 in this run.\n", nTotalProvedSat );
2529  if ( RetValue == 1 )
2530  Abc_Print( 1, "Property proved. " );
2531  else if ( RetValue == 0 )
2532  Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pMan->pSeqModel ? pMan->pSeqModel->iPo : -1, pMan->pName, iFrame );
2533  else if ( RetValue == -1 )
2534  Abc_Print( 1, "Property UNDECIDED. " );
2535  else
2536  assert( 0 );
2537 ABC_PRT( "Time", Abc_Clock() - clk );
2538  return RetValue;
2539 }
2540 
2541 /**Function*************************************************************
2542 
2543  Synopsis [Gives the current ABC network to AIG manager for processing.]
2544 
2545  Description []
2546 
2547  SideEffects []
2548 
2549  SeeAlso []
2550 
2551 ***********************************************************************/
2552 int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, Inter_ManParams_t * pPars, Abc_Ntk_t ** ppNtkRes )
2553 {
2554  Aig_Man_t * pMan;
2555  int RetValue;
2556  if ( ppNtkRes )
2557  *ppNtkRes = NULL;
2558  pMan = Abc_NtkToDar( pNtk, 0, 1 );
2559  if ( pMan == NULL )
2560  {
2561  Abc_Print( 1, "Converting miter into AIG has failed.\n" );
2562  return -1;
2563  }
2564  if ( pPars->fUseSeparate && ppNtkRes )
2565  {
2566  Aig_Man_t * pManNew;
2567  RetValue = Abc_NtkDarBmcInter_int( pMan, pPars, &pManNew );
2568  *ppNtkRes = Abc_NtkFromAigPhase( pManNew );
2569  Aig_ManStop( pManNew );
2570  }
2571  else
2572  {
2573  RetValue = Abc_NtkDarBmcInter_int( pMan, pPars, NULL );
2574  }
2575  ABC_FREE( pNtk->pModel );
2576  ABC_FREE( pNtk->pSeqModel );
2577  pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
2578  Aig_ManStop( pMan );
2579  return RetValue;
2580 }
2581 
2582 /**Function*************************************************************
2583 
2584  Synopsis [Gives the current ABC network to AIG manager for processing.]
2585 
2586  Description []
2587 
2588  SideEffects []
2589 
2590  SeeAlso []
2591 
2592 ***********************************************************************/
2594 {
2595  char * pFileNameGeneric, pFileName0[1000], pFileName1[1000];
2596  Aig_Man_t * pMan, * pPart0, * pPart1;//, * pMiter;
2597  // derive the AIG manager
2598  pMan = Abc_NtkToDar( pNtk, 0, 1 );
2599  if ( pMan == NULL )
2600  {
2601  Abc_Print( 1, "Converting network into AIG has failed.\n" );
2602  return 0;
2603  }
2604 // if ( !Saig_ManDemiterSimple( pMan, &pPart0, &pPart1 ) )
2605  if ( !Saig_ManDemiterSimpleDiff( pMan, &pPart0, &pPart1 ) )
2606  {
2607  Aig_ManStop( pMan );
2608  Abc_Print( 1, "Demitering has failed.\n" );
2609  return 0;
2610  }
2611  // create file names
2612  pFileNameGeneric = Extra_FileNameGeneric( pNtk->pSpec ? pNtk->pSpec : pNtk->pName );
2613 // sprintf( pFileName0, "%s%s", pFileNameGeneric, "_part0.aig" );
2614 // sprintf( pFileName1, "%s%s", pFileNameGeneric, "_part1.aig" );
2615  sprintf( pFileName0, "%s", "part0.aig" );
2616  sprintf( pFileName1, "%s", "part1.aig" );
2617  ABC_FREE( pFileNameGeneric );
2618  // dump files
2619  Ioa_WriteAiger( pPart0, pFileName0, 0, 0 );
2620  Ioa_WriteAiger( pPart1, pFileName1, 0, 0 );
2621  Abc_Print( 1, "Demitering produced two files \"%s\" and \"%s\".\n", pFileName0, pFileName1 );
2622  // create two-level miter
2623 // pMiter = Saig_ManCreateMiterTwo( pPart0, pPart1, 2 );
2624 // Aig_ManDumpBlif( pMiter, "miter01.blif", NULL, NULL );
2625 // Aig_ManStop( pMiter );
2626 // Abc_Print( 1, "The new miter is written into file \"%s\".\n", "miter01.blif" );
2627  Aig_ManStop( pPart0 );
2628  Aig_ManStop( pPart1 );
2629  Aig_ManStop( pMan );
2630  return 1;
2631 }
2632 
2633 /**Function*************************************************************
2634 
2635  Synopsis [Gives the current ABC network to AIG manager for processing.]
2636 
2637  Description []
2638 
2639  SideEffects []
2640 
2641  SeeAlso []
2642 
2643 ***********************************************************************/
2645 {
2646  char * pFileNameGeneric, pFileName0[1000], pFileName1[1000];
2647  Aig_Man_t * pMan, * pPart0, * pPart1;//, * pMiter;
2648  // derive the AIG manager
2649  pMan = Abc_NtkToDar( pNtk, 0, 1 );
2650  if ( pMan == NULL )
2651  {
2652  Abc_Print( 1, "Converting network into AIG has failed.\n" );
2653  return 0;
2654  }
2655 
2656  Saig_ManDemiterNew( pMan );
2657  Aig_ManStop( pMan );
2658  return 1;
2659 
2660 // if ( !Saig_ManDemiterSimple( pMan, &pPart0, &pPart1 ) )
2661  if ( !Saig_ManDemiterSimpleDiff( pMan, &pPart0, &pPart1 ) )
2662  {
2663  Abc_Print( 1, "Demitering has failed.\n" );
2664  return 0;
2665  }
2666  // create file names
2667  pFileNameGeneric = Extra_FileNameGeneric( pNtk->pSpec );
2668  sprintf( pFileName0, "%s%s", pFileNameGeneric, "_part0.aig" );
2669  sprintf( pFileName1, "%s%s", pFileNameGeneric, "_part1.aig" );
2670  ABC_FREE( pFileNameGeneric );
2671  // dump files
2672  Ioa_WriteAiger( pPart0, pFileName0, 0, 0 );
2673  Ioa_WriteAiger( pPart1, pFileName1, 0, 0 );
2674  Abc_Print( 1, "Demitering produced two files \"%s\" and \"%s\".\n", pFileName0, pFileName1 );
2675  // create two-level miter
2676 // pMiter = Saig_ManCreateMiterTwo( pPart0, pPart1, 2 );
2677 // Aig_ManDumpBlif( pMiter, "miter01.blif", NULL, NULL );
2678 // Aig_ManStop( pMiter );
2679 // Abc_Print( 1, "The new miter is written into file \"%s\".\n", "miter01.blif" );
2680  Aig_ManStop( pPart0 );
2681  Aig_ManStop( pPart1 );
2682  Aig_ManStop( pMan );
2683  return 1;
2684 }
2685 
2686 /**Function*************************************************************
2687 
2688  Synopsis [Gives the current ABC network to AIG manager for processing.]
2689 
2690  Description []
2691 
2692  SideEffects []
2693 
2694  SeeAlso []
2695 
2696 ***********************************************************************/
2697 int Abc_NtkDarDemiterDual( Abc_Ntk_t * pNtk, int fVerbose )
2698 {
2699  char * pFileNameGeneric, pFileName0[1000], pFileName1[1000];
2700  Aig_Man_t * pMan, * pPart0, * pPart1;//, * pMiter;
2701  if ( (Abc_NtkPoNum(pNtk) & 1) )
2702  {
2703  Abc_Print( 1, "The number of POs should be even.\n" );
2704  return 0;
2705  }
2706  // derive the AIG manager
2707  pMan = Abc_NtkToDar( pNtk, 0, 1 );
2708  if ( pMan == NULL )
2709  {
2710  Abc_Print( 1, "Converting network into AIG has failed.\n" );
2711  return 0;
2712  }
2713 // if ( !Saig_ManDemiterSimple( pMan, &pPart0, &pPart1 ) )
2714  if ( !Saig_ManDemiterDual( pMan, &pPart0, &pPart1 ) )
2715  {
2716  Abc_Print( 1, "Demitering has failed.\n" );
2717  return 0;
2718  }
2719  // create new AIG
2720  ABC_FREE( pPart0->pName );
2721  pPart0->pName = Abc_UtilStrsav( "part0" );
2722  // create new AIGs
2723  ABC_FREE( pPart1->pName );
2724  pPart1->pName = Abc_UtilStrsav( "part1" );
2725  // create file names
2726  pFileNameGeneric = Extra_FileNameGeneric( pNtk->pSpec );
2727 // sprintf( pFileName0, "%s%s", pFileNameGeneric, "_part0.aig" );
2728 // sprintf( pFileName1, "%s%s", pFileNameGeneric, "_part1.aig" );
2729  sprintf( pFileName0, "%s", "part0.aig" );
2730  sprintf( pFileName1, "%s", "part1.aig" );
2731  ABC_FREE( pFileNameGeneric );
2732  Ioa_WriteAiger( pPart0, pFileName0, 0, 0 );
2733  Ioa_WriteAiger( pPart1, pFileName1, 0, 0 );
2734  Abc_Print( 1, "Demitering produced two files \"%s\" and \"%s\".\n", pFileName0, pFileName1 );
2735  // dump files
2736  if ( fVerbose )
2737  {
2738 // Abc_Print( 1, "Init: " );
2739  Aig_ManPrintStats( pMan );
2740 // Abc_Print( 1, "Part1: " );
2741  Aig_ManPrintStats( pPart0 );
2742 // Abc_Print( 1, "Part2: " );
2743  Aig_ManPrintStats( pPart1 );
2744  }
2745  // create two-level miter
2746 // pMiter = Saig_ManCreateMiterTwo( pPart0, pPart1, 2 );
2747 // Aig_ManDumpBlif( pMiter, "miter01.blif", NULL, NULL );
2748 // Aig_ManStop( pMiter );
2749 // Abc_Print( 1, "The new miter is written into file \"%s\".\n", "miter01.blif" );
2750  Aig_ManStop( pPart0 );
2751  Aig_ManStop( pPart1 );
2752  Aig_ManStop( pMan );
2753  return 1;
2754 }
2755 
2756 /**Function*************************************************************
2757 
2758  Synopsis [Gives the current ABC network to AIG manager for processing.]
2759 
2760  Description []
2761 
2762  SideEffects []
2763 
2764  SeeAlso []
2765 
2766 ***********************************************************************/
2767 int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar, int nBmcFramesMax, int nBmcConfMax )
2768 {
2769  Aig_Man_t * pMan;
2770  int iFrame = -1, RetValue = -1;
2771  abctime clkTotal = Abc_Clock();
2772  if ( pSecPar->fTryComb || Abc_NtkLatchNum(pNtk) == 0 )
2773  {
2774  Prove_Params_t Params, * pParams = &Params;
2775  Abc_Ntk_t * pNtkComb;
2776  int RetValue;
2777  abctime clk = Abc_Clock();
2778  if ( Abc_NtkLatchNum(pNtk) == 0 )
2779  Abc_Print( 1, "The network has no latches. Running CEC.\n" );
2780  // create combinational network
2781  pNtkComb = Abc_NtkDup( pNtk );
2782  Abc_NtkMakeComb( pNtkComb, 1 );
2783  // solve it using combinational equivalence checking
2784  Prove_ParamsSetDefault( pParams );
2785  pParams->fVerbose = 1;
2786  RetValue = Abc_NtkIvyProve( &pNtkComb, pParams );
2787  // transfer model if given
2788 // pNtk->pModel = pNtkComb->pModel; pNtkComb->pModel = NULL;
2789  if ( RetValue == 0 && (Abc_NtkLatchNum(pNtk) == 0) )
2790  {
2791  pNtk->pModel = pNtkComb->pModel; pNtkComb->pModel = NULL;
2792  Abc_Print( 1, "Networks are not equivalent.\n" );
2793  ABC_PRT( "Time", Abc_Clock() - clk );
2794  if ( pSecPar->fReportSolution )
2795  {
2796  Abc_Print( 1, "SOLUTION: FAIL " );
2797  ABC_PRT( "Time", Abc_Clock() - clkTotal );
2798  }
2799  return RetValue;
2800  }
2801  Abc_NtkDelete( pNtkComb );
2802  // return the result, if solved
2803  if ( RetValue == 1 )
2804  {
2805  Abc_Print( 1, "Networks are equivalent after CEC. " );
2806  ABC_PRT( "Time", Abc_Clock() - clk );
2807  if ( pSecPar->fReportSolution )
2808  {
2809  Abc_Print( 1, "SOLUTION: PASS " );
2810  ABC_PRT( "Time", Abc_Clock() - clkTotal );
2811  }
2812  return RetValue;
2813  }
2814  }
2815  // derive the AIG manager
2816  pMan = Abc_NtkToDar( pNtk, 0, 1 );
2817  if ( pMan == NULL )
2818  {
2819  Abc_Print( 1, "Converting miter into AIG has failed.\n" );
2820  return -1;
2821  }
2822  assert( pMan->nRegs > 0 );
2823 
2824  if ( pSecPar->fTryBmc )
2825  {
2826  RetValue = Saig_BmcPerform( pMan, 0, nBmcFramesMax, 2000, 0, nBmcConfMax, 0, pSecPar->fVerbose, 0, &iFrame, 0 );
2827  if ( RetValue == 0 )
2828  {
2829  Abc_Print( 1, "Networks are not equivalent.\n" );
2830  if ( pSecPar->fReportSolution )
2831  {
2832  Abc_Print( 1, "SOLUTION: FAIL " );
2833  ABC_PRT( "Time", Abc_Clock() - clkTotal );
2834  }
2835  // return the counter-example generated
2836  ABC_FREE( pNtk->pModel );
2837  ABC_FREE( pNtk->pSeqModel );
2838  pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
2839  Aig_ManStop( pMan );
2840  return RetValue;
2841  }
2842  }
2843  // perform verification
2844  if ( pSecPar->fUseNewProver )
2845  {
2846  RetValue = Ssw_SecGeneralMiter( pMan, NULL );
2847  }
2848  else
2849  {
2850  RetValue = Fra_FraigSec( pMan, pSecPar, NULL );
2851  ABC_FREE( pNtk->pModel );
2852  ABC_FREE( pNtk->pSeqModel );
2853  pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
2854  if ( pNtk->pSeqModel )
2855  {
2856  Abc_Cex_t * pCex = pNtk->pSeqModel;
2857  Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d.\n", pCex->iPo, pNtk->pName, pCex->iFrame );
2858  if ( !Saig_ManVerifyCex( pMan, pNtk->pSeqModel ) )
2859  Abc_Print( 1, "Abc_NtkDarProve(): Counter-example verification has FAILED.\n" );
2860  }
2861  }
2862  Aig_ManStop( pMan );
2863  return RetValue;
2864 }
2865 
2866 /**Function*************************************************************
2867 
2868  Synopsis [Gives the current ABC network to AIG manager for processing.]
2869 
2870  Description []
2871 
2872  SideEffects []
2873 
2874  SeeAlso []
2875 
2876 ***********************************************************************/
2877 int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Fra_Sec_t * pSecPar )
2878 {
2879 // Fraig_Params_t Params;
2880  Aig_Man_t * pMan;
2881  Abc_Ntk_t * pMiter;//, * pTemp;
2882  int RetValue;
2883 
2884  // get the miter of the two networks
2885  pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0, 0, 0, 0 );
2886  if ( pMiter == NULL )
2887  {
2888  Abc_Print( 1, "Miter computation has failed.\n" );
2889  return 0;
2890  }
2891  RetValue = Abc_NtkMiterIsConstant( pMiter );
2892  if ( RetValue == 0 )
2893  {
2894  extern void Abc_NtkVerifyReportErrorSeq( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel, int nFrames );
2895  Abc_Print( 1, "Networks are NOT EQUIVALENT after structural hashing.\n" );
2896  // report the error
2897  pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, pSecPar->nFramesMax );
2898 // Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, pMiter->pModel, pSecPar->nFramesMax );
2899  ABC_FREE( pMiter->pModel );
2900  Abc_NtkDelete( pMiter );
2901  return 0;
2902  }
2903  if ( RetValue == 1 )
2904  {
2905  Abc_NtkDelete( pMiter );
2906  Abc_Print( 1, "Networks are equivalent after structural hashing.\n" );
2907  return 1;
2908  }
2909 
2910  // commented out because sometimes the problem became non-inductive
2911 /*
2912  // preprocess the miter by fraiging it
2913  // (note that for each functional class, fraiging leaves one representative;
2914  // so fraiging does not reduce the number of functions represented by nodes
2915  Fraig_ParamsSetDefault( &Params );
2916  Params.nBTLimit = 100000;
2917  pMiter = Abc_NtkFraig( pTemp = pMiter, &Params, 0, 0 );
2918  Abc_NtkDelete( pTemp );
2919  RetValue = Abc_NtkMiterIsConstant( pMiter );
2920  if ( RetValue == 0 )
2921  {
2922  extern void Abc_NtkVerifyReportErrorSeq( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel, int nFrames );
2923  Abc_Print( 1, "Networks are NOT EQUIVALENT after structural hashing.\n" );
2924  // report the error
2925  pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, nFrames );
2926  Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, pMiter->pModel, nFrames );
2927  ABC_FREE( pMiter->pModel );
2928  Abc_NtkDelete( pMiter );
2929  return 0;
2930  }
2931  if ( RetValue == 1 )
2932  {
2933  Abc_NtkDelete( pMiter );
2934  Abc_Print( 1, "Networks are equivalent after structural hashing.\n" );
2935  return 1;
2936  }
2937 */
2938  // derive the AIG manager
2939  pMan = Abc_NtkToDar( pMiter, 0, 1 );
2940  Abc_NtkDelete( pMiter );
2941  if ( pMan == NULL )
2942  {
2943  Abc_Print( 1, "Converting miter into AIG has failed.\n" );
2944  return -1;
2945  }
2946  assert( pMan->nRegs > 0 );
2947 
2948  // perform verification
2949  RetValue = Fra_FraigSec( pMan, pSecPar, NULL );
2950  Aig_ManStop( pMan );
2951  return RetValue;
2952 }
2953 
2954 /**Function*************************************************************
2955 
2956  Synopsis [Gives the current ABC network to AIG manager for processing.]
2957 
2958  Description []
2959 
2960  SideEffects []
2961 
2962  SeeAlso []
2963 
2964 ***********************************************************************/
2965 int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars )
2966 {
2967  int RetValue = -1;
2968  abctime clk = Abc_Clock();
2969  Aig_Man_t * pMan;
2970  pMan = Abc_NtkToDar( pNtk, 0, 1 );
2971  if ( pMan == NULL )
2972  {
2973  Abc_Print( 1, "Converting network into AIG has failed.\n" );
2974  return -1;
2975  }
2976  RetValue = Pdr_ManSolve( pMan, pPars );
2977  pPars->nDropOuts = Saig_ManPoNum(pMan) - pPars->nProveOuts - pPars->nFailOuts;
2978  if ( !pPars->fSilent )
2979  {
2980  if ( pPars->fSolveAll )
2981  Abc_Print( 1, "Properties: All = %d. Proved = %d. Disproved = %d. Undecided = %d. ",
2982  Saig_ManPoNum(pMan), pPars->nProveOuts, pPars->nFailOuts, pPars->nDropOuts );
2983  else if ( RetValue == 1 )
2984  Abc_Print( 1, "Property proved. " );
2985  else
2986  {
2987  if ( RetValue == 0 )
2988  {
2989  if ( pMan->pSeqModel == NULL )
2990  Abc_Print( 1, "Abc_NtkDarPdr(): Counter-example is not available.\n" );
2991  else
2992  {
2993  Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pMan->pSeqModel->iPo, pNtk->pName, pMan->pSeqModel->iFrame );
2994  if ( !Saig_ManVerifyCex( pMan, pMan->pSeqModel ) )
2995  Abc_Print( 1, "Abc_NtkDarPdr(): Counter-example verification has FAILED.\n" );
2996  }
2997  }
2998  else if ( RetValue == -1 )
2999  Abc_Print( 1, "Property UNDECIDED. " );
3000  else
3001  assert( 0 );
3002  }
3003  ABC_PRT( "Time", Abc_Clock() - clk );
3004 /*
3005  Abc_Print( 1, "Status: " );
3006  if ( pPars->pOutMap )
3007  {
3008  int i;
3009  for ( i = 0; i < Saig_ManPoNum(pMan); i++ )
3010  if ( pPars->pOutMap[i] == 1 )
3011  Abc_Print( 1, "%d=%s ", i, "unsat" );
3012  else if ( pPars->pOutMap[i] == 0 )
3013  Abc_Print( 1, "%d=%s ", i, "sat" );
3014  else if ( pPars->pOutMap[i] < 0 )
3015  Abc_Print( 1, "%d=%s ", i, "undec" );
3016  else assert( 0 );
3017  }
3018  Abc_Print( 1, "\n" );
3019 */
3020  }
3021  ABC_FREE( pNtk->pSeqModel );
3022  pNtk->pSeqModel = pMan->pSeqModel;
3023  pMan->pSeqModel = NULL;
3024  if ( pNtk->vSeqModelVec )
3025  Vec_PtrFreeFree( pNtk->vSeqModelVec );
3026  pNtk->vSeqModelVec = pMan->vSeqModelVec;
3027  pMan->vSeqModelVec = NULL;
3028  Aig_ManStop( pMan );
3029  return RetValue;
3030 }
3031 
3032 /**Function*************************************************************
3033 
3034  Synopsis [Performs BDD-based reachability analysis.]
3035 
3036  Description []
3037 
3038  SideEffects []
3039 
3040  SeeAlso []
3041 
3042 ***********************************************************************/
3043 int Abc_NtkDarAbSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fVerbose )
3044 {
3045  Aig_Man_t * pMan1, * pMan2 = NULL;
3046  int RetValue;
3047  // derive AIG manager
3048  pMan1 = Abc_NtkToDar( pNtk1, 0, 1 );
3049  if ( pMan1 == NULL )
3050  {
3051  Abc_Print( 1, "Converting miter into AIG has failed.\n" );
3052  return -1;
3053  }
3054  assert( Aig_ManRegNum(pMan1) > 0 );
3055  // derive AIG manager
3056  if ( pNtk2 )
3057  {
3058  pMan2 = Abc_NtkToDar( pNtk2, 0, 1 );
3059  if ( pMan2 == NULL )
3060  {
3061  Aig_ManStop( pMan1 );
3062  Abc_Print( 1, "Converting miter into AIG has failed.\n" );
3063  return -1;
3064  }
3065  assert( Aig_ManRegNum(pMan2) > 0 );
3066  if ( Saig_ManPiNum(pMan1) != Saig_ManPiNum(pMan2) )
3067  {
3068  Aig_ManStop( pMan1 );
3069  Aig_ManStop( pMan2 );
3070  Abc_Print( 1, "The networks have different number of PIs.\n" );
3071  return -1;
3072  }
3073  if ( Saig_ManPoNum(pMan1) != Saig_ManPoNum(pMan2) )
3074  {
3075  Aig_ManStop( pMan1 );
3076  Aig_ManStop( pMan2 );
3077  Abc_Print( 1, "The networks have different number of POs.\n" );
3078  return -1;
3079  }
3080  if ( Aig_ManRegNum(pMan1) != Aig_ManRegNum(pMan2) )
3081  {
3082  Aig_ManStop( pMan1 );
3083  Aig_ManStop( pMan2 );
3084  Abc_Print( 1, "The networks have different number of flops.\n" );
3085  return -1;
3086  }
3087  }
3088  // perform verification
3089  RetValue = Ssw_SecSpecialMiter( pMan1, pMan2, nFrames, fVerbose );
3090  Aig_ManStop( pMan1 );
3091  if ( pMan2 )
3092  Aig_ManStop( pMan2 );
3093  return RetValue;
3094 }
3095 
3096 
3097 /**Function*************************************************************
3098 
3099  Synopsis [Gives the current ABC network to AIG manager for processing.]
3100 
3101  Description []
3102 
3103  SideEffects []
3104 
3105  SeeAlso []
3106 
3107 ***********************************************************************/
3108 int Abc_NtkDarSimSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Ssw_Pars_t * pPars )
3109 {
3110  Aig_Man_t * pMan1, * pMan2 = NULL;
3111  int RetValue;
3112  // derive AIG manager
3113  pMan1 = Abc_NtkToDar( pNtk1, 0, 1 );
3114  if ( pMan1 == NULL )
3115  {
3116  Abc_Print( 1, "Converting miter into AIG has failed.\n" );
3117  return -1;
3118  }
3119  assert( Aig_ManRegNum(pMan1) > 0 );
3120  // derive AIG manager
3121  if ( pNtk2 )
3122  {
3123  pMan2 = Abc_NtkToDar( pNtk2, 0, 1 );
3124  if ( pMan2 == NULL )
3125  {
3126  Abc_Print( 1, "Converting miter into AIG has failed.\n" );
3127  return -1;
3128  }
3129  assert( Aig_ManRegNum(pMan2) > 0 );
3130  }
3131 
3132  // perform verification
3133  RetValue = Ssw_SecWithSimilarity( pMan1, pMan2, pPars );
3134  Aig_ManStop( pMan1 );
3135  if ( pMan2 )
3136  Aig_ManStop( pMan2 );
3137  return RetValue;
3138 }
3139 
3140 /**Function*************************************************************
3141 
3142  Synopsis []
3143 
3144  Description []
3145 
3146  SideEffects []
3147 
3148  SeeAlso []
3149 
3150 ***********************************************************************/
3151 Abc_Ntk_t * Abc_NtkDarMatch( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nDist, int fVerbose )
3152 {
3153  extern Vec_Int_t * Saig_StrSimPerformMatching( Aig_Man_t * p0, Aig_Man_t * p1, int nDist, int fVerbose, Aig_Man_t ** ppMiter );
3154  Abc_Ntk_t * pNtkAig;
3155  Aig_Man_t * pMan1, * pMan2 = NULL, * pManRes;
3156  Vec_Int_t * vPairs;
3157  assert( Abc_NtkIsStrash(pNtk1) );
3158  // derive AIG manager
3159  pMan1 = Abc_NtkToDar( pNtk1, 0, 1 );
3160  if ( pMan1 == NULL )
3161  {
3162  Abc_Print( 1, "Converting miter into AIG has failed.\n" );
3163  return NULL;
3164  }
3165  assert( Aig_ManRegNum(pMan1) > 0 );
3166  // derive AIG manager
3167  if ( pNtk2 )
3168  {
3169  pMan2 = Abc_NtkToDar( pNtk2, 0, 1 );
3170  if ( pMan2 == NULL )
3171  {
3172  Abc_Print( 1, "Converting miter into AIG has failed.\n" );
3173  return NULL;
3174  }
3175  assert( Aig_ManRegNum(pMan2) > 0 );
3176  }
3177 
3178  // perform verification
3179  vPairs = Saig_StrSimPerformMatching( pMan1, pMan2, nDist, 1, &pManRes );
3180  pNtkAig = Abc_NtkFromAigPhase( pManRes );
3181  if ( vPairs )
3182  Vec_IntFree( vPairs );
3183  if ( pManRes )
3184  Aig_ManStop( pManRes );
3185  Aig_ManStop( pMan1 );
3186  if ( pMan2 )
3187  Aig_ManStop( pMan2 );
3188  return pNtkAig;
3189 }
3190 
3191 
3192 /**Function*************************************************************
3193 
3194  Synopsis [Gives the current ABC network to AIG manager for processing.]
3195 
3196  Description []
3197 
3198  SideEffects []
3199 
3200  SeeAlso []
3201 
3202 ***********************************************************************/
3203 Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fLatchConst, int fLatchEqual, int fSaveNames, int fUseMvSweep, int nFramesSymb, int nFramesSatur, int fVerbose, int fVeryVerbose )
3204 {
3205  extern void Aig_ManPrintControlFanouts( Aig_Man_t * p );
3206  Abc_Ntk_t * pNtkAig;
3207  Aig_Man_t * pMan, * pTemp;
3208  pMan = Abc_NtkToDar( pNtk, 0, 1 );
3209  if ( pMan == NULL )
3210  return NULL;
3211  if ( fSaveNames )
3212  {
3213  Aig_ManSeqCleanup( pMan );
3214  if ( fLatchConst && pMan->nRegs )
3215  pMan = Aig_ManConstReduce( pMan, fUseMvSweep, nFramesSymb, nFramesSatur, fVerbose, fVeryVerbose );
3216  if ( fLatchEqual && pMan->nRegs )
3217  pMan = Aig_ManReduceLaches( pMan, fVerbose );
3218  }
3219  else
3220  {
3221  if ( pMan->vFlopNums )
3222  Vec_IntFree( pMan->vFlopNums );
3223  pMan->vFlopNums = NULL;
3224  pMan = Aig_ManScl( pTemp = pMan, fLatchConst, fLatchEqual, fUseMvSweep, nFramesSymb, nFramesSatur, fVerbose, fVeryVerbose );
3225  Aig_ManStop( pTemp );
3226  }
3227 
3228  pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
3229 //Aig_ManPrintControlFanouts( pMan );
3230  Aig_ManStop( pMan );
3231  return pNtkAig;
3232 }
3233 
3234 /**Function*************************************************************
3235 
3236  Synopsis [Gives the current ABC network to AIG manager for processing.]
3237 
3238  Description []
3239 
3240  SideEffects []
3241 
3242  SeeAlso []
3243 
3244 ***********************************************************************/
3245 Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose )
3246 {
3247  Abc_Ntk_t * pNtkAig;
3248  Aig_Man_t * pMan, * pTemp;
3249  pMan = Abc_NtkToDar( pNtk, 0, 1 );
3250  if ( pMan == NULL )
3251  return NULL;
3252 // Aig_ManReduceLachesCount( pMan );
3253  if ( pMan->vFlopNums )
3254  Vec_IntFree( pMan->vFlopNums );
3255  pMan->vFlopNums = NULL;
3256 
3257  pMan = Rtm_ManRetime( pTemp = pMan, 1, nStepsMax, fVerbose );
3258  Aig_ManStop( pTemp );
3259 
3260 // pMan = Aig_ManReduceLaches( pMan, 1 );
3261 // pMan = Aig_ManConstReduce( pMan, 1, 0 );
3262 
3263  pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
3264  Aig_ManStop( pMan );
3265  return pNtkAig;
3266 }
3267 
3268 /**Function*************************************************************
3269 
3270  Synopsis [Gives the current ABC network to AIG manager for processing.]
3271 
3272  Description []
3273 
3274  SideEffects []
3275 
3276  SeeAlso []
3277 
3278 ***********************************************************************/
3279 Abc_Ntk_t * Abc_NtkDarRetimeF( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose )
3280 {
3281  Abc_Ntk_t * pNtkAig;
3282  Aig_Man_t * pMan, * pTemp;
3283  pMan = Abc_NtkToDar( pNtk, 0, 1 );
3284  if ( pMan == NULL )
3285  return NULL;
3286 // Aig_ManReduceLachesCount( pMan );
3287  if ( pMan->vFlopNums )
3288  Vec_IntFree( pMan->vFlopNums );
3289  pMan->vFlopNums = NULL;
3290 
3291  pMan = Aig_ManRetimeFrontier( pTemp = pMan, nStepsMax );
3292  Aig_ManStop( pTemp );
3293 
3294 // pMan = Aig_ManReduceLaches( pMan, 1 );
3295 // pMan = Aig_ManConstReduce( pMan, 1, 0 );
3296 
3297  pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
3298  Aig_ManStop( pMan );
3299  return pNtkAig;
3300 }
3301 
3302 /**Function*************************************************************
3303 
3304  Synopsis [Gives the current ABC network to AIG manager for processing.]
3305 
3306  Description []
3307 
3308  SideEffects []
3309 
3310  SeeAlso []
3311 
3312 ***********************************************************************/
3313 Abc_Ntk_t * Abc_NtkDarRetimeMostFwd( Abc_Ntk_t * pNtk, int nMaxIters, int fVerbose )
3314 {
3315  extern Aig_Man_t * Saig_ManRetimeForward( Aig_Man_t * p, int nIters, int fVerbose );
3316 
3317  Abc_Ntk_t * pNtkAig;
3318  Aig_Man_t * pMan, * pTemp;
3319  pMan = Abc_NtkToDar( pNtk, 0, 1 );
3320  if ( pMan == NULL )
3321  return NULL;
3322 // Aig_ManReduceLachesCount( pMan );
3323  if ( pMan->vFlopNums )
3324  Vec_IntFree( pMan->vFlopNums );
3325  pMan->vFlopNums = NULL;
3326 
3327  pMan = Saig_ManRetimeForward( pTemp = pMan, nMaxIters, fVerbose );
3328  Aig_ManStop( pTemp );
3329 
3330 // pMan = Aig_ManReduceLaches( pMan, 1 );
3331 // pMan = Aig_ManConstReduce( pMan, 1, 0 );
3332 
3333  pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
3334  Aig_ManStop( pMan );
3335  return pNtkAig;
3336 }
3337 
3338 /**Function*************************************************************
3339 
3340  Synopsis [Gives the current ABC network to AIG manager for processing.]
3341 
3342  Description []
3343 
3344  SideEffects []
3345 
3346  SeeAlso []
3347 
3348 ***********************************************************************/
3349 Abc_Ntk_t * Abc_NtkDarRetimeMinArea( Abc_Ntk_t * pNtk, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose )
3350 {
3351  extern Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose );
3352  Abc_Ntk_t * pNtkAig;
3353  Aig_Man_t * pMan, * pTemp;
3354  pMan = Abc_NtkToDar( pNtk, 0, 1 );
3355  if ( pMan == NULL )
3356  return NULL;
3357  if ( pMan->vFlopNums )
3358  Vec_IntFree( pMan->vFlopNums );
3359  pMan->vFlopNums = NULL;
3360 
3361  pMan = Saig_ManRetimeMinArea( pTemp = pMan, nMaxIters, fForwardOnly, fBackwardOnly, fInitial, fVerbose );
3362  Aig_ManStop( pTemp );
3363 
3364  pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
3365  Aig_ManStop( pMan );
3366  return pNtkAig;
3367 }
3368 
3369 /**Function*************************************************************
3370 
3371  Synopsis [Gives the current ABC network to AIG manager for processing.]
3372 
3373  Description []
3374 
3375  SideEffects []
3376 
3377  SeeAlso []
3378 
3379 ***********************************************************************/
3380 Abc_Ntk_t * Abc_NtkDarRetimeStep( Abc_Ntk_t * pNtk, int fVerbose )
3381 {
3382  Abc_Ntk_t * pNtkAig;
3383  Aig_Man_t * pMan;
3384  assert( Abc_NtkIsStrash(pNtk) );
3385  pMan = Abc_NtkToDar( pNtk, 0, 1 );
3386  if ( pMan == NULL )
3387  return NULL;
3388  if ( pMan->vFlopNums )
3389  Vec_IntFree( pMan->vFlopNums );
3390  pMan->vFlopNums = NULL;
3391 
3392  Aig_ManPrintStats(pMan);
3393  Saig_ManRetimeSteps( pMan, 1000, 1, 0 );
3394  Aig_ManPrintStats(pMan);
3395 
3396  pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
3397  Aig_ManStop( pMan );
3398  return pNtkAig;
3399 }
3400 
3401 /**Function*************************************************************
3402 
3403  Synopsis [Gives the current ABC network to AIG manager for processing.]
3404 
3405  Description []
3406 
3407  SideEffects []
3408 
3409  SeeAlso []
3410 
3411 ***********************************************************************/
3412 /*
3413 Abc_Ntk_t * Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk, int nIters, int nSteps, int fRetimingOnly, int fAddBugs, int fUseCnf, int fVerbose )
3414 {
3415  Abc_Ntk_t * pNtkAig;
3416  Aig_Man_t * pMan, * pTemp;
3417  pMan = Abc_NtkToDar( pNtk, 0, 1 );
3418  if ( pMan == NULL )
3419  return NULL;
3420  if ( pMan->vFlopNums )
3421  Vec_IntFree( pMan->vFlopNums );
3422  pMan->vFlopNums = NULL;
3423 
3424  pMan = Saig_ManHaigRecord( pTemp = pMan, nIters, nSteps, fRetimingOnly, fAddBugs, fUseCnf, fVerbose );
3425  Aig_ManStop( pTemp );
3426 
3427  pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
3428  Aig_ManStop( pMan );
3429  return pNtkAig;
3430 }
3431 */
3432 
3433 /**Function*************************************************************
3434 
3435  Synopsis [Performs random simulation.]
3436 
3437  Description []
3438 
3439  SideEffects []
3440 
3441  SeeAlso []
3442 
3443 ***********************************************************************/
3444 int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, int fNew, int fMiter, int fVerbose, char * pFileSim )
3445 {
3446  Aig_Man_t * pMan;
3447  Abc_Cex_t * pCex;
3448  int status, RetValue = -1;
3449  abctime clk = Abc_Clock();
3450  if ( Abc_NtkGetChoiceNum(pNtk) )
3451  {
3452  Abc_Print( 1, "Removing %d choices from the AIG.\n", Abc_NtkGetChoiceNum(pNtk) );
3453  Abc_AigCleanup((Abc_Aig_t *)pNtk->pManFunc);
3454  }
3455  pMan = Abc_NtkToDar( pNtk, 0, 1 );
3456  if ( fNew )
3457  {
3458  Gia_Man_t * pGia;
3459  Gia_ParSim_t Pars, * pPars = &Pars;
3460  Gia_ManSimSetDefaultParams( pPars );
3461  pPars->nWords = nWords;
3462  pPars->nIters = nFrames;
3463  pPars->TimeLimit = TimeOut;
3464  pPars->fCheckMiter = fMiter;
3465  pPars->fVerbose = fVerbose;
3466  pGia = Gia_ManFromAig( pMan );
3467  if ( Gia_ManSimSimulate( pGia, pPars ) )
3468  {
3469  if ( pGia->pCexSeq )
3470  {
3471  Abc_Print( 1, "Simulation of %d frames with %d words asserted output %d in frame %d. ",
3472  nFrames, nWords, pGia->pCexSeq->iPo, pGia->pCexSeq->iFrame );
3473  status = Saig_ManVerifyCex( pMan, pGia->pCexSeq );
3474  if ( status == 0 )
3475  Abc_Print( 1, "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" );
3476  }
3477  ABC_FREE( pNtk->pModel );
3478  ABC_FREE( pNtk->pSeqModel );
3479  pNtk->pSeqModel = pGia->pCexSeq; pGia->pCexSeq = NULL;
3480  RetValue = 0;
3481  }
3482  else
3483  {
3484  Abc_Print( 1, "Simulation of %d frames with %d words did not assert the outputs. ",
3485  nFrames, nWords );
3486  }
3487  Gia_ManStop( pGia );
3488  }
3489  else // comb/seq simulator
3490  {
3491  Fra_Sml_t * pSml;
3492  if ( pFileSim != NULL )
3493  {
3494  assert( Abc_NtkLatchNum(pNtk) == 0 );
3495  pSml = Fra_SmlSimulateCombGiven( pMan, pFileSim, fMiter, fVerbose );
3496  }
3497  else if ( Abc_NtkLatchNum(pNtk) == 0 )
3498  pSml = Fra_SmlSimulateComb( pMan, nWords, fMiter );
3499  else
3500  pSml = Fra_SmlSimulateSeq( pMan, 0, nFrames, nWords, fMiter );
3501  if ( pSml->fNonConstOut )
3502  {
3503  pCex = Fra_SmlGetCounterExample( pSml );
3504  if ( pCex )
3505  {
3506  Abc_Print( 1, "Simulation of %d frame%s with %d word%s asserted output %d in frame %d. ",
3507  pSml->nFrames, pSml->nFrames == 1 ? "": "s",
3508  pSml->nWordsFrame, pSml->nWordsFrame == 1 ? "": "s",
3509  pCex->iPo, pCex->iFrame );
3510  status = Saig_ManVerifyCex( pMan, pCex );
3511  if ( status == 0 )
3512  Abc_Print( 1, "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" );
3513  }
3514  ABC_FREE( pNtk->pModel );
3515  ABC_FREE( pNtk->pSeqModel );
3516  pNtk->pSeqModel = pCex;
3517  RetValue = 0;
3518  }
3519  else
3520  {
3521  Abc_Print( 1, "Simulation of %d frames with %d words did not assert the outputs. ",
3522  nFrames, nWords );
3523  }
3524  Fra_SmlStop( pSml );
3525  }
3526  ABC_PRT( "Time", Abc_Clock() - clk );
3527  Aig_ManStop( pMan );
3528  return RetValue;
3529 }
3530 
3531 /**Function*************************************************************
3532 
3533  Synopsis [Performs random simulation.]
3534 
3535  Description []
3536 
3537  SideEffects []
3538 
3539  SeeAlso []
3540 
3541 ***********************************************************************/
3543 {
3544  Aig_Man_t * pMan;
3545  int status, RetValue = -1;
3546 // abctime clk = Abc_Clock();
3547  if ( Abc_NtkGetChoiceNum(pNtk) )
3548  {
3549  Abc_Print( 1, "Removing %d choices from the AIG.\n", Abc_NtkGetChoiceNum(pNtk) );
3550  Abc_AigCleanup((Abc_Aig_t *)pNtk->pManFunc);
3551  }
3552  pMan = Abc_NtkToDar( pNtk, 0, 1 );
3553  if ( Ssw_RarSimulate( pMan, pPars ) == 0 )
3554  {
3555  if ( pMan->pSeqModel )
3556  {
3557 // Abc_Print( 1, "Simulation of %d frames with %d words asserted output %d in frame %d. ",
3558 // nFrames, nWords, pMan->pSeqModel->iPo, pMan->pSeqModel->iFrame );
3559  status = Saig_ManVerifyCex( pMan, pMan->pSeqModel );
3560  if ( status == 0 )
3561  Abc_Print( 1, "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" );
3562  }
3563  ABC_FREE( pNtk->pModel );
3564  ABC_FREE( pNtk->pSeqModel );
3565  pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
3566  RetValue = 0;
3567  }
3568  else
3569  {
3570 // Abc_Print( 1, "Simulation of %d frames with %d words did not assert the outputs. ",
3571 // nFrames, nWords );
3572  }
3573  if ( pNtk->vSeqModelVec )
3574  Vec_PtrFreeFree( pNtk->vSeqModelVec );
3575  pNtk->vSeqModelVec = pMan->vSeqModelVec; pMan->vSeqModelVec = NULL;
3576 // ABC_PRT( "Time", Abc_Clock() - clk );
3577  pNtk->pData = pMan->pData; pMan->pData = NULL;
3578  Aig_ManStop( pMan );
3579  return RetValue;
3580 }
3581 
3582 /**Function*************************************************************
3583 
3584  Synopsis [Gives the current ABC network to AIG manager for processing.]
3585 
3586  Description []
3587 
3588  SideEffects []
3589 
3590  SeeAlso []
3591 
3592 ***********************************************************************/
3593 int Abc_NtkDarClau( Abc_Ntk_t * pNtk, int nFrames, int nPref, int nClauses, int nLutSize, int nLevels, int nCutsMax, int nBatches, int fStepUp, int fBmc, int fRefs, int fTarget, int fVerbose, int fVeryVerbose )
3594 {
3595  extern int Fra_Clau( Aig_Man_t * pMan, int nIters, int fVerbose, int fVeryVerbose );
3596  extern int Fra_Claus( Aig_Man_t * pAig, int nFrames, int nPref, int nClauses, int nLutSize, int nLevels, int nCutsMax, int nBatches, int fStepUp, int fBmc, int fRefs, int fTarget, int fVerbose, int fVeryVerbose );
3597  Aig_Man_t * pMan;
3598  if ( fTarget && Abc_NtkPoNum(pNtk) != 1 )
3599  {
3600  Abc_Print( 1, "The number of outputs should be 1.\n" );
3601  return 1;
3602  }
3603  pMan = Abc_NtkToDar( pNtk, 0, 1 );
3604  if ( pMan == NULL )
3605  return 1;
3606 // Aig_ManReduceLachesCount( pMan );
3607  if ( pMan->vFlopNums )
3608  Vec_IntFree( pMan->vFlopNums );
3609  pMan->vFlopNums = NULL;
3610 
3611 // Fra_Clau( pMan, nStepsMax, fVerbose, fVeryVerbose );
3612  Fra_Claus( pMan, nFrames, nPref, nClauses, nLutSize, nLevels, nCutsMax, nBatches, fStepUp, fBmc, fRefs, fTarget, fVerbose, fVeryVerbose );
3613  Aig_ManStop( pMan );
3614  return 1;
3615 }
3616 
3617 /**Function*************************************************************
3618 
3619  Synopsis [Performs targe enlargement.]
3620 
3621  Description []
3622 
3623  SideEffects []
3624 
3625  SeeAlso []
3626 
3627 ***********************************************************************/
3628 Abc_Ntk_t * Abc_NtkDarEnlarge( Abc_Ntk_t * pNtk, int nFrames, int fVerbose )
3629 {
3630  Abc_Ntk_t * pNtkAig;
3631  Aig_Man_t * pMan, * pTemp;
3632  pMan = Abc_NtkToDar( pNtk, 0, 1 );
3633  if ( pMan == NULL )
3634  return NULL;
3635  pMan = Aig_ManFrames( pTemp = pMan, nFrames, 0, 1, 1, 1, NULL );
3636  Aig_ManStop( pTemp );
3637  pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
3638  Aig_ManStop( pMan );
3639  return pNtkAig;
3640 }
3641 
3642 /**Function*************************************************************
3643 
3644  Synopsis [Performs targe enlargement.]
3645 
3646  Description []
3647 
3648  SideEffects []
3649 
3650  SeeAlso []
3651 
3652 ***********************************************************************/
3653 Abc_Ntk_t * Abc_NtkDarTempor( Abc_Ntk_t * pNtk, int nFrames, int TimeOut, int nConfLimit, int fUseBmc, int fUseTransSigs, int fVerbose, int fVeryVerbose )
3654 {
3655  extern Aig_Man_t * Saig_ManTempor( Aig_Man_t * pAig, int nFrames, int TimeOut, int nConfLimit, int fUseBmc, int fUseTransSigs, int fVerbose, int fVeryVerbose );
3656  Abc_Ntk_t * pNtkAig;
3657  Aig_Man_t * pMan, * pTemp;
3658  pMan = Abc_NtkToDar( pNtk, 0, 1 );
3659  if ( pMan == NULL )
3660  return NULL;
3661  pTemp = Saig_ManTempor( pMan, nFrames, TimeOut, nConfLimit, fUseBmc, fUseTransSigs, fVerbose, fVeryVerbose );
3662  Aig_ManStop( pMan );
3663  if ( pTemp == NULL )
3664  return Abc_NtkDup( pNtk );
3665  pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pTemp );
3666  Aig_ManStop( pTemp );
3667  return pNtkAig;
3668 }
3669 
3670 /**Function*************************************************************
3671 
3672  Synopsis [Performs induction for property only.]
3673 
3674  Description []
3675 
3676  SideEffects []
3677 
3678  SeeAlso []
3679 
3680 ***********************************************************************/
3681 int Abc_NtkDarInduction( Abc_Ntk_t * pNtk, int nTimeOut, int nFramesMax, int nConfMax, int fUnique, int fUniqueAll, int fGetCex, int fVerbose, int fVeryVerbose )
3682 {
3683  Aig_Man_t * pMan;
3684  abctime clkTotal = Abc_Clock();
3685  int RetValue;
3686  pMan = Abc_NtkToDar( pNtk, 0, 1 );
3687  if ( pMan == NULL )
3688  return -1;
3689  RetValue = Saig_ManInduction( pMan, nTimeOut, nFramesMax, nConfMax, fUnique, fUniqueAll, fGetCex, fVerbose, fVeryVerbose );
3690  if ( RetValue == 1 )
3691  {
3692  Abc_Print( 1, "Networks are equivalent. " );
3693 ABC_PRT( "Time", Abc_Clock() - clkTotal );
3694  }
3695  else if ( RetValue == 0 )
3696  {
3697  Abc_Print( 1, "Networks are NOT EQUIVALENT. " );
3698 ABC_PRT( "Time", Abc_Clock() - clkTotal );
3699  }
3700  else
3701  {
3702  Abc_Print( 1, "Networks are UNDECIDED. " );
3703 ABC_PRT( "Time", Abc_Clock() - clkTotal );
3704  }
3705  if ( fGetCex )
3706  {
3707  ABC_FREE( pNtk->pModel );
3708  ABC_FREE( pNtk->pSeqModel );
3709  pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
3710  }
3711  Aig_ManStop( pMan );
3712  return RetValue;
3713 }
3714 
3715 
3716 /**Function*************************************************************
3717 
3718  Synopsis [Interplates two networks.]
3719 
3720  Description []
3721 
3722  SideEffects []
3723 
3724  SeeAlso []
3725 
3726 ***********************************************************************/
3727 Abc_Ntk_t * Abc_NtkInterOne( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fRelation, int fVerbose )
3728 {
3729  extern Aig_Man_t * Aig_ManInter( Aig_Man_t * pManOn, Aig_Man_t * pManOff, int fRelation, int fVerbose );
3730  Abc_Ntk_t * pNtkAig;
3731  Aig_Man_t * pManOn, * pManOff, * pManAig;
3732  if ( Abc_NtkCoNum(pNtkOn) != 1 || Abc_NtkCoNum(pNtkOff) != 1 )
3733  {
3734  Abc_Print( 1, "Currently works only for single-output networks.\n" );
3735  return NULL;
3736  }
3737  if ( Abc_NtkCiNum(pNtkOn) != Abc_NtkCiNum(pNtkOff) )
3738  {
3739  Abc_Print( 1, "The number of PIs should be the same.\n" );
3740  return NULL;
3741  }
3742  // create internal AIGs
3743  pManOn = Abc_NtkToDar( pNtkOn, 0, 0 );
3744  if ( pManOn == NULL )
3745  return NULL;
3746  pManOff = Abc_NtkToDar( pNtkOff, 0, 0 );
3747  if ( pManOff == NULL )
3748  return NULL;
3749  // derive the interpolant
3750  pManAig = Aig_ManInter( pManOn, pManOff, fRelation, fVerbose );
3751  if ( pManAig == NULL )
3752  {
3753  Abc_Print( 1, "Interpolant computation failed.\n" );
3754  return NULL;
3755  }
3756  Aig_ManStop( pManOn );
3757  Aig_ManStop( pManOff );
3758  // for the relation, add an extra input
3759  if ( fRelation )
3760  {
3761  Abc_Obj_t * pObj;
3762  pObj = Abc_NtkCreatePi( pNtkOff );
3763  Abc_ObjAssignName( pObj, "New", NULL );
3764  }
3765  // create logic network
3766  pNtkAig = Abc_NtkFromDar( pNtkOff, pManAig );
3767  Aig_ManStop( pManAig );
3768  return pNtkAig;
3769 }
3770 
3771 /**Function*************************************************************
3772 
3773  Synopsis [Fast interpolation.]
3774 
3775  Description []
3776 
3777  SideEffects []
3778 
3779  SeeAlso []
3780 
3781 ***********************************************************************/
3782 void Abc_NtkInterFast( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fVerbose )
3783 {
3784  extern void Aig_ManInterFast( Aig_Man_t * pManOn, Aig_Man_t * pManOff, int fVerbose );
3785  Aig_Man_t * pManOn, * pManOff;
3786  // create internal AIGs
3787  pManOn = Abc_NtkToDar( pNtkOn, 0, 0 );
3788  if ( pManOn == NULL )
3789  return;
3790  pManOff = Abc_NtkToDar( pNtkOff, 0, 0 );
3791  if ( pManOff == NULL )
3792  return;
3793  Aig_ManInterFast( pManOn, pManOff, fVerbose );
3794  Aig_ManStop( pManOn );
3795  Aig_ManStop( pManOff );
3796 }
3797 
3801 
3802 /**Function*************************************************************
3803 
3804  Synopsis [Interplates two networks.]
3805 
3806  Description []
3807 
3808  SideEffects []
3809 
3810  SeeAlso []
3811 
3812 ***********************************************************************/
3813 Abc_Ntk_t * Abc_NtkInter( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fRelation, int fVerbose )
3814 {
3815  Abc_Ntk_t * pNtkOn1, * pNtkOff1, * pNtkInter1, * pNtkInter;
3816  Abc_Obj_t * pObj;
3817  int i; //, clk = Abc_Clock();
3818  if ( Abc_NtkCoNum(pNtkOn) != Abc_NtkCoNum(pNtkOff) )
3819  {
3820  Abc_Print( 1, "Currently works only for networks with equal number of POs.\n" );
3821  return NULL;
3822  }
3823  // compute the fast interpolation time
3824 // Abc_NtkInterFast( pNtkOn, pNtkOff, fVerbose );
3825  // consider the case of one output
3826  if ( Abc_NtkCoNum(pNtkOn) == 1 )
3827  return Abc_NtkInterOne( pNtkOn, pNtkOff, fRelation, fVerbose );
3828  // start the new network
3829  pNtkInter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
3830  pNtkInter->pName = Extra_UtilStrsav(pNtkOn->pName);
3831  Abc_NtkForEachPi( pNtkOn, pObj, i )
3832  Abc_NtkDupObj( pNtkInter, pObj, 1 );
3833  // process each POs separately
3834 timeCnf = 0;
3835 timeSat = 0;
3836 timeInt = 0;
3837  Abc_NtkForEachCo( pNtkOn, pObj, i )
3838  {
3839  pNtkOn1 = Abc_NtkCreateCone( pNtkOn, Abc_ObjFanin0(pObj), Abc_ObjName(pObj), 1 );
3840  if ( Abc_ObjFaninC0(pObj) )
3841  Abc_ObjXorFaninC( Abc_NtkPo(pNtkOn1, 0), 0 );
3842 
3843  pObj = Abc_NtkCo(pNtkOff, i);
3844  pNtkOff1 = Abc_NtkCreateCone( pNtkOff, Abc_ObjFanin0(pObj), Abc_ObjName(pObj), 1 );
3845  if ( Abc_ObjFaninC0(pObj) )
3846  Abc_ObjXorFaninC( Abc_NtkPo(pNtkOff1, 0), 0 );
3847 
3848  if ( Abc_NtkNodeNum(pNtkOn1) == 0 )
3849  pNtkInter1 = Abc_NtkDup( pNtkOn1 );
3850  else if ( Abc_NtkNodeNum(pNtkOff1) == 0 )
3851  {
3852  pNtkInter1 = Abc_NtkDup( pNtkOff1 );
3853  Abc_ObjXorFaninC( Abc_NtkPo(pNtkInter1, 0), 0 );
3854  }
3855  else
3856  pNtkInter1 = Abc_NtkInterOne( pNtkOn1, pNtkOff1, 0, fVerbose );
3857  if ( pNtkInter1 )
3858  {
3859  Abc_NtkAppend( pNtkInter, pNtkInter1, 1 );
3860  Abc_NtkDelete( pNtkInter1 );
3861  }
3862 
3863  Abc_NtkDelete( pNtkOn1 );
3864  Abc_NtkDelete( pNtkOff1 );
3865  }
3866 // ABC_PRT( "CNF", timeCnf );
3867 // ABC_PRT( "SAT", timeSat );
3868 // ABC_PRT( "Int", timeInt );
3869 // ABC_PRT( "Slow interpolation time", Abc_Clock() - clk );
3870 
3871  // return the network
3872  if ( !Abc_NtkCheck( pNtkInter ) )
3873  Abc_Print( 1, "Abc_NtkAttachBottom(): Network check has failed.\n" );
3874  return pNtkInter;
3875 }
3876 
3877 /**Function*************************************************************
3878 
3879  Synopsis []
3880 
3881  Description []
3882 
3883  SideEffects []
3884 
3885  SeeAlso []
3886 
3887 ***********************************************************************/
3888 void Abc_NtkPrintSccs( Abc_Ntk_t * pNtk, int fVerbose )
3889 {
3890 // extern Vec_Ptr_t * Aig_ManRegPartitionLinear( Aig_Man_t * pAig, int nPartSize );
3891  Aig_Man_t * pMan;
3892  pMan = Abc_NtkToDar( pNtk, 0, 1 );
3893  if ( pMan == NULL )
3894  return;
3895  Aig_ManComputeSccs( pMan );
3896 // Aig_ManRegPartitionLinear( pMan, 1000 );
3897  Aig_ManStop( pMan );
3898 }
3899 
3900 /**Function*************************************************************
3901 
3902  Synopsis []
3903 
3904  Description []
3905 
3906  SideEffects []
3907 
3908  SeeAlso []
3909 
3910 ***********************************************************************/
3912 {
3913  extern void Saig_ManPrintCones( Aig_Man_t * pAig );
3914  Aig_Man_t * pMan;
3915  pMan = Abc_NtkToDar( pNtk, 0, 1 );
3916  if ( pMan == NULL )
3917  return 0;
3918  assert( Aig_ManRegNum(pMan) > 0 );
3919  Saig_ManPrintCones( pMan );
3920  Aig_ManStop( pMan );
3921  return 1;
3922 }
3923 
3924 /**Function*************************************************************
3925 
3926  Synopsis []
3927 
3928  Description []
3929 
3930  SideEffects []
3931 
3932  SeeAlso []
3933 
3934 ***********************************************************************/
3935 Abc_Ntk_t * Abc_NtkBalanceExor( Abc_Ntk_t * pNtk, int fUpdateLevel, int fVerbose )
3936 {
3937  extern void Dar_BalancePrintStats( Aig_Man_t * p );
3938  Abc_Ntk_t * pNtkAig;
3939  Aig_Man_t * pMan, * pTemp;//, * pTemp2;
3940  assert( Abc_NtkIsStrash(pNtk) );
3941  // derive AIG with EXORs
3942  pMan = Abc_NtkToDar( pNtk, 1, 0 );
3943  if ( pMan == NULL )
3944  return NULL;
3945 // Aig_ManPrintStats( pMan );
3946  if ( fVerbose )
3947  Dar_BalancePrintStats( pMan );
3948  // perform balancing
3949  pTemp = Dar_ManBalance( pMan, fUpdateLevel );
3950 // Aig_ManPrintStats( pTemp );
3951  // create logic network
3952  pNtkAig = Abc_NtkFromDar( pNtk, pTemp );
3953  Aig_ManStop( pTemp );
3954  Aig_ManStop( pMan );
3955  return pNtkAig;
3956 }
3957 
3958 /**Function*************************************************************
3959 
3960  Synopsis [Performs phase abstraction.]
3961 
3962  Description []
3963 
3964  SideEffects []
3965 
3966  SeeAlso []
3967 
3968 ***********************************************************************/
3969 Abc_Ntk_t * Abc_NtkPhaseAbstract( Abc_Ntk_t * pNtk, int nFrames, int nPref, int fIgnore, int fPrint, int fVerbose )
3970 {
3971  extern Aig_Man_t * Saig_ManPhaseAbstract( Aig_Man_t * p, Vec_Int_t * vInits, int nFrames, int nPref, int fIgnore, int fPrint, int fVerbose );
3972  Vec_Int_t * vInits;
3973  Abc_Ntk_t * pNtkAig;
3974  Aig_Man_t * pMan, * pTemp;
3975  pMan = Abc_NtkToDar( pNtk, 0, 1 );
3976  if ( pMan == NULL )
3977  return NULL;
3978  vInits = Abc_NtkGetLatchValues(pNtk);
3979  pMan = Saig_ManPhaseAbstract( pTemp = pMan, vInits, nFrames, nPref, fIgnore, fPrint, fVerbose );
3980  Vec_IntFree( vInits );
3981  Aig_ManStop( pTemp );
3982  if ( pMan == NULL )
3983  return NULL;
3984  pNtkAig = Abc_NtkFromAigPhase( pMan );
3985 // pNtkAig->pName = Extra_UtilStrsav(pNtk->pName);
3986 // pNtkAig->pSpec = Extra_UtilStrsav(pNtk->pSpec);
3987  Aig_ManStop( pMan );
3988  return pNtkAig;
3989 }
3990 
3991 /**Function*************************************************************
3992 
3993  Synopsis [Performs phase abstraction.]
3994 
3995  Description []
3996 
3997  SideEffects []
3998 
3999  SeeAlso []
4000 
4001 ***********************************************************************/
4003 {
4004  extern int Saig_ManPhaseFrameNum( Aig_Man_t * p, Vec_Int_t * vInits );
4005  Vec_Int_t * vInits;
4006  Aig_Man_t * pMan;
4007  int nFrames;
4008  pMan = Abc_NtkToDar( pNtk, 0, 1 );
4009  if ( pMan == NULL )
4010  return 1;
4011  vInits = Abc_NtkGetLatchValues(pNtk);
4012  nFrames = Saig_ManPhaseFrameNum( pMan, vInits );
4013  Vec_IntFree( vInits );
4014  Aig_ManStop( pMan );
4015  return nFrames;
4016 }
4017 
4018 /**Function*************************************************************
4019 
4020  Synopsis [Performs phase abstraction.]
4021 
4022  Description []
4023 
4024  SideEffects []
4025 
4026  SeeAlso []
4027 
4028 ***********************************************************************/
4029 Abc_Ntk_t * Abc_NtkDarSynchOne( Abc_Ntk_t * pNtk, int nWords, int fVerbose )
4030 {
4031  extern Aig_Man_t * Saig_SynchSequenceApply( Aig_Man_t * pAig, int nWords, int fVerbose );
4032  Abc_Ntk_t * pNtkAig;
4033  Aig_Man_t * pMan, * pTemp;
4034  pMan = Abc_NtkToDar( pNtk, 0, 1 );
4035  if ( pMan == NULL )
4036  return NULL;
4037  pMan = Saig_SynchSequenceApply( pTemp = pMan, nWords, fVerbose );
4038  Aig_ManStop( pTemp );
4039  if ( pMan == NULL )
4040  return NULL;
4041  pNtkAig = Abc_NtkFromDar( pNtk, pMan );
4042  Aig_ManStop( pMan );
4043  return pNtkAig;
4044 }
4045 
4046 /**Function*************************************************************
4047 
4048  Synopsis [Performs phase abstraction.]
4049 
4050  Description []
4051 
4052  SideEffects []
4053 
4054  SeeAlso []
4055 
4056 ***********************************************************************/
4057 Abc_Ntk_t * Abc_NtkDarSynch( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nWords, int fVerbose )
4058 {
4059  extern Aig_Man_t * Saig_Synchronize( Aig_Man_t * pAig1, Aig_Man_t * pAig2, int nWords, int fVerbose );
4060  Abc_Ntk_t * pNtkAig;
4061  Aig_Man_t * pMan1, * pMan2, * pMan;
4062  pMan1 = Abc_NtkToDar( pNtk1, 0, 1 );
4063  if ( pMan1 == NULL )
4064  return NULL;
4065  pMan2 = Abc_NtkToDar( pNtk2, 0, 1 );
4066  if ( pMan2 == NULL )
4067  {
4068  Aig_ManStop( pMan1 );
4069  return NULL;
4070  }
4071  pMan = Saig_Synchronize( pMan1, pMan2, nWords, fVerbose );
4072  Aig_ManStop( pMan1 );
4073  Aig_ManStop( pMan2 );
4074  if ( pMan == NULL )
4075  return NULL;
4076  pNtkAig = Abc_NtkFromAigPhase( pMan );
4077 // pNtkAig->pName = Extra_UtilStrsav("miter");
4078 // pNtkAig->pSpec = NULL;
4079  Aig_ManStop( pMan );
4080  return pNtkAig;
4081 }
4082 
4083 /**Function*************************************************************
4084 
4085  Synopsis [Performs phase abstraction.]
4086 
4087  Description []
4088 
4089  SideEffects []
4090 
4091  SeeAlso []
4092 
4093 ***********************************************************************/
4095 {
4096  Abc_Ntk_t * pNtkAig;
4097  Aig_Man_t * pMan1, * pMan2 = NULL, * pMan;
4098  pMan1 = Abc_NtkToDar( pNtk, 0, 1 );
4099  if ( pMan1 == NULL )
4100  return NULL;
4101  if ( pCare )
4102  {
4103  pMan2 = Abc_NtkToDar( pCare, 0, 0 );
4104  if ( pMan2 == NULL )
4105  {
4106  Aig_ManStop( pMan1 );
4107  return NULL;
4108  }
4109  }
4110  pMan = Cgt_ClockGating( pMan1, pMan2, pPars );
4111  Aig_ManStop( pMan1 );
4112  if ( pMan2 )
4113  Aig_ManStop( pMan2 );
4114  if ( pMan == NULL )
4115  return NULL;
4116  pNtkAig = Abc_NtkFromDar( pNtk, pMan );
4117  Aig_ManStop( pMan );
4118  return pNtkAig;
4119 }
4120 
4121 /**Function*************************************************************
4122 
4123  Synopsis [Performs phase abstraction.]
4124 
4125  Description []
4126 
4127  SideEffects []
4128 
4129  SeeAlso []
4130 
4131 ***********************************************************************/
4132 Abc_Ntk_t * Abc_NtkDarExtWin( Abc_Ntk_t * pNtk, int nObjId, int nDist, int fVerbose )
4133 {
4134  Abc_Ntk_t * pNtkAig;
4135  Aig_Man_t * pMan1, * pMan;
4136  Aig_Obj_t * pObj;
4137  pMan1 = Abc_NtkToDar( pNtk, 0, 1 );
4138  if ( pMan1 == NULL )
4139  return NULL;
4140  if ( nObjId == -1 )
4141  {
4142  pObj = Saig_ManFindPivot( pMan1 );
4143  Abc_Print( 1, "Selected object %d as a window pivot.\n", pObj->Id );
4144  }
4145  else
4146  {
4147  if ( nObjId >= Aig_ManObjNumMax(pMan1) )
4148  {
4149  Aig_ManStop( pMan1 );
4150  Abc_Print( 1, "The ID is too large.\n" );
4151  return NULL;
4152  }
4153  pObj = Aig_ManObj( pMan1, nObjId );
4154  if ( pObj == NULL )
4155  {
4156  Aig_ManStop( pMan1 );
4157  Abc_Print( 1, "Object with ID %d does not exist.\n", nObjId );
4158  return NULL;
4159  }
4160  if ( !Saig_ObjIsLo(pMan1, pObj) && !Aig_ObjIsNode(pObj) )
4161  {
4162  Aig_ManStop( pMan1 );
4163  Abc_Print( 1, "Object with ID %d is not a node or reg output.\n", nObjId );
4164  return NULL;
4165  }
4166  }
4167  pMan = Saig_ManWindowExtract( pMan1, pObj, nDist );
4168  Aig_ManStop( pMan1 );
4169  if ( pMan == NULL )
4170  return NULL;
4171  pNtkAig = Abc_NtkFromAigPhase( pMan );
4172  pNtkAig->pName = Extra_UtilStrsav(pNtk->pName);
4173  pNtkAig->pSpec = Extra_UtilStrsav(pNtk->pSpec);
4174  Aig_ManStop( pMan );
4175  return pNtkAig;
4176 }
4177 
4178 /**Function*************************************************************
4179 
4180  Synopsis [Performs phase abstraction.]
4181 
4182  Description []
4183 
4184  SideEffects []
4185 
4186  SeeAlso []
4187 
4188 ***********************************************************************/
4189 Abc_Ntk_t * Abc_NtkDarInsWin( Abc_Ntk_t * pNtk, Abc_Ntk_t * pCare, int nObjId, int nDist, int fVerbose )
4190 {
4191  Abc_Ntk_t * pNtkAig;
4192  Aig_Man_t * pMan1, * pMan2 = NULL, * pMan;
4193  Aig_Obj_t * pObj;
4194  pMan1 = Abc_NtkToDar( pNtk, 0, 1 );
4195  if ( pMan1 == NULL )
4196  return NULL;
4197  if ( nObjId == -1 )
4198  {
4199  pObj = Saig_ManFindPivot( pMan1 );
4200  Abc_Print( 1, "Selected object %d as a window pivot.\n", pObj->Id );
4201  }
4202  else
4203  {
4204  if ( nObjId >= Aig_ManObjNumMax(pMan1) )
4205  {
4206  Aig_ManStop( pMan1 );
4207  Abc_Print( 1, "The ID is too large.\n" );
4208  return NULL;
4209  }
4210  pObj = Aig_ManObj( pMan1, nObjId );
4211  if ( pObj == NULL )
4212  {
4213  Aig_ManStop( pMan1 );
4214  Abc_Print( 1, "Object with ID %d does not exist.\n", nObjId );
4215  return NULL;
4216  }
4217  if ( !Saig_ObjIsLo(pMan1, pObj) && !Aig_ObjIsNode(pObj) )
4218  {
4219  Aig_ManStop( pMan1 );
4220  Abc_Print( 1, "Object with ID %d is not a node or reg output.\n", nObjId );
4221  return NULL;
4222  }
4223  }
4224  if ( pCare )
4225  {
4226  pMan2 = Abc_NtkToDar( pCare, 0, 0 );
4227  if ( pMan2 == NULL )
4228  {
4229  Aig_ManStop( pMan1 );
4230  return NULL;
4231  }
4232  }
4233  pMan = Saig_ManWindowInsert( pMan1, pObj, nDist, pMan2 );
4234  Aig_ManStop( pMan1 );
4235  if ( pMan2 )
4236  Aig_ManStop( pMan2 );
4237  if ( pMan == NULL )
4238  return NULL;
4239  pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
4240  Aig_ManStop( pMan );
4241  return pNtkAig;
4242 }
4243 
4244 /**Function*************************************************************
4245 
4246  Synopsis [Performs phase abstraction.]
4247 
4248  Description []
4249 
4250  SideEffects []
4251 
4252  SeeAlso []
4253 
4254 ***********************************************************************/
4255 Abc_Ntk_t * Abc_NtkDarFrames( Abc_Ntk_t * pNtk, int nPrefix, int nFrames, int fInit, int fVerbose )
4256 {
4257  Abc_Ntk_t * pNtkAig;
4258  Aig_Man_t * pMan, * pTemp;
4259  pMan = Abc_NtkToDar( pNtk, 0, 1 );
4260  if ( pMan == NULL )
4261  return NULL;
4262  pMan = Saig_ManTimeframeSimplify( pTemp = pMan, nPrefix, nFrames, fInit, fVerbose );
4263  Aig_ManStop( pTemp );
4264  if ( pMan == NULL )
4265  return NULL;
4266  pNtkAig = Abc_NtkFromAigPhase( pMan );
4267  pNtkAig->pName = Extra_UtilStrsav(pNtk->pName);
4268  pNtkAig->pSpec = Extra_UtilStrsav(pNtk->pSpec);
4269  Aig_ManStop( pMan );
4270  return pNtkAig;
4271 }
4272 
4273 /**Function*************************************************************
4274 
4275  Synopsis [Performs phase abstraction.]
4276 
4277  Description []
4278 
4279  SideEffects []
4280 
4281  SeeAlso []
4282 
4283 ***********************************************************************/
4284 Abc_Ntk_t * Abc_NtkDarCleanupAig( Abc_Ntk_t * pNtk, int fCleanupPis, int fCleanupPos, int fVerbose )
4285 {
4286  Abc_Ntk_t * pNtkAig;
4287  Aig_Man_t * pMan;
4288  pMan = Abc_NtkToDar( pNtk, 0, 1 );
4289  if ( pMan == NULL )
4290  return NULL;
4291  if ( fCleanupPis )
4292  {
4293  int Temp = Aig_ManCiCleanup( pMan );
4294  if ( fVerbose )
4295  Abc_Print( 1, "Cleanup removed %d primary inputs without fanout.\n", Temp );
4296  }
4297  if ( fCleanupPos )
4298  {
4299  int Temp = Aig_ManCoCleanup( pMan );
4300  if ( fVerbose )
4301  Abc_Print( 1, "Cleanup removed %d primary outputs driven by const-0.\n", Temp );
4302  }
4303  pNtkAig = Abc_NtkFromAigPhase( pMan );
4304  pNtkAig->pName = Extra_UtilStrsav(pNtk->pName);
4305  pNtkAig->pSpec = Extra_UtilStrsav(pNtk->pSpec);
4306  Aig_ManStop( pMan );
4307  return pNtkAig;
4308 }
4309 
4310 /**Function*************************************************************
4311 
4312  Synopsis [Performs BDD-based reachability analysis.]
4313 
4314  Description []
4315 
4316  SideEffects []
4317 
4318  SeeAlso []
4319 
4320 ***********************************************************************/
4322 {
4323  Aig_Man_t * pMan;
4324  int RetValue;
4325  pMan = Abc_NtkToDar( pNtk, 0, 1 );
4326  if ( pMan == NULL )
4327  return -1;
4328  RetValue = Aig_ManVerifyUsingBdds( pMan, pPars );
4329  ABC_FREE( pNtk->pModel );
4330  ABC_FREE( pNtk->pSeqModel );
4331  pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
4332  Aig_ManStop( pMan );
4333  return RetValue;
4334 }
4335 
4337 
4338 #include "map/amap/amap.h"
4339 #include "map/mio/mio.h"
4340 
4342 
4343 
4344 /**Function*************************************************************
4345 
4346  Synopsis []
4347 
4348  Description []
4349 
4350  SideEffects []
4351 
4352  SeeAlso []
4353 
4354 ***********************************************************************/
4356 {
4357 // extern void * Abc_FrameReadLibGen();
4359  Amap_Out_t * pRes;
4360  Vec_Ptr_t * vNodesNew;
4361  Abc_Ntk_t * pNtkNew;
4362  Abc_Obj_t * pNodeNew, * pFaninNew;
4363  int i, k, iPis, iPos, nDupGates;
4364  // make sure gates exist in the current library
4365  Vec_PtrForEachEntry( Amap_Out_t *, vMapping, pRes, i )
4366  if ( pRes->pName && Mio_LibraryReadGateByName( pLib, pRes->pName, NULL ) == NULL )
4367  {
4368  Abc_Print( 1, "Current library does not contain gate \"%s\".\n", pRes->pName );
4369  return NULL;
4370  }
4371  // create the network
4372  pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_MAP );
4373  pNtkNew->pManFunc = pLib;
4374  iPis = iPos = 0;
4375  vNodesNew = Vec_PtrAlloc( Vec_PtrSize(vMapping) );
4376  Vec_PtrForEachEntry( Amap_Out_t *, vMapping, pRes, i )
4377  {
4378  if ( pRes->Type == -1 )
4379  pNodeNew = Abc_NtkCi( pNtkNew, iPis++ );
4380  else if ( pRes->Type == 1 )
4381  pNodeNew = Abc_NtkCo( pNtkNew, iPos++ );
4382  else
4383  {
4384  pNodeNew = Abc_NtkCreateNode( pNtkNew );
4385  pNodeNew->pData = Mio_LibraryReadGateByName( pLib, pRes->pName, NULL );
4386  }
4387  for ( k = 0; k < pRes->nFans; k++ )
4388  {
4389  pFaninNew = (Abc_Obj_t *)Vec_PtrEntry( vNodesNew, pRes->pFans[k] );
4390  Abc_ObjAddFanin( pNodeNew, pFaninNew );
4391  }
4392  Vec_PtrPush( vNodesNew, pNodeNew );
4393  }
4394  Vec_PtrFree( vNodesNew );
4395  assert( iPis == Abc_NtkCiNum(pNtkNew) );
4396  assert( iPos == Abc_NtkCoNum(pNtkNew) );
4397  // decouple the PO driver nodes to reduce the number of levels
4398  nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
4399 // if ( nDupGates && Map_ManReadVerbose(pMan) )
4400 // Abc_Print( 1, "Duplicated %d gates to decouple the CO drivers.\n", nDupGates );
4401  return pNtkNew;
4402 }
4403 
4404 /**Function*************************************************************
4405 
4406  Synopsis [Gives the current ABC network to AIG manager for processing.]
4407 
4408  Description []
4409 
4410  SideEffects []
4411 
4412  SeeAlso []
4413 
4414 ***********************************************************************/
4416 {
4417  extern Vec_Ptr_t * Amap_ManTest( Aig_Man_t * pAig, Amap_Par_t * pPars );
4418  Vec_Ptr_t * vMapping;
4419  Abc_Ntk_t * pNtkAig = NULL;
4420  Aig_Man_t * pMan;
4421  Aig_MmFlex_t * pMem;
4422 
4423  assert( Abc_NtkIsStrash(pNtk) );
4424  // convert to the AIG manager
4425  pMan = Abc_NtkToDarChoices( pNtk );
4426  if ( pMan == NULL )
4427  return NULL;
4428 
4429  // perform computation
4430  vMapping = Amap_ManTest( pMan, pPars );
4431  Aig_ManStop( pMan );
4432  if ( vMapping == NULL )
4433  return NULL;
4434  pMem = (Aig_MmFlex_t *)Vec_PtrPop( vMapping );
4435  pNtkAig = Amap_ManProduceNetwork( pNtk, vMapping );
4436  Aig_MmFlexStop( pMem, 0 );
4437  Vec_PtrFree( vMapping );
4438 
4439  // make sure everything is okay
4440  if ( pNtkAig && !Abc_NtkCheck( pNtkAig ) )
4441  {
4442  Abc_Print( 1, "Abc_NtkDar: The network check has failed.\n" );
4443  Abc_NtkDelete( pNtkAig );
4444  return NULL;
4445  }
4446  return pNtkAig;
4447 }
4448 
4449 /**Function*************************************************************
4450 
4451  Synopsis [Performs BDD-based reachability analysis.]
4452 
4453  Description []
4454 
4455  SideEffects []
4456 
4457  SeeAlso []
4458 
4459 ***********************************************************************/
4460 void Abc_NtkDarConstr( Abc_Ntk_t * pNtk, int nFrames, int nConfs, int nProps, int fStruct, int fOldAlgo, int fVerbose )
4461 {
4462  Aig_Man_t * pMan;//, * pMan2;//, * pTemp;
4463  assert( Abc_NtkIsStrash(pNtk) );
4464  pMan = Abc_NtkToDar( pNtk, 0, 1 );
4465  if ( pMan == NULL )
4466  return;
4467  if ( fStruct )
4468  Saig_ManDetectConstrTest( pMan );
4469  else
4470  Saig_ManDetectConstrFuncTest( pMan, nFrames, nConfs, nProps, fOldAlgo, fVerbose );
4471  Aig_ManStop( pMan );
4472 }
4473 
4474 /**Function*************************************************************
4475 
4476  Synopsis [Performs BDD-based reachability analysis.]
4477 
4478  Description []
4479 
4480  SideEffects []
4481 
4482  SeeAlso []
4483 
4484 ***********************************************************************/
4485 Abc_Ntk_t * Abc_NtkDarOutdec( Abc_Ntk_t * pNtk, int nLits, int fVerbose )
4486 {
4487  Abc_Ntk_t * pNtkAig;
4488  Aig_Man_t * pMan, * pTemp;
4489  assert( Abc_NtkIsStrash(pNtk) );
4490  pMan = Abc_NtkToDar( pNtk, 0, 1 );
4491  if ( pMan == NULL )
4492  return NULL;
4493  pMan = Saig_ManDecPropertyOutput( pTemp = pMan, nLits, fVerbose );
4494  Aig_ManStop( pTemp );
4495  if ( pMan == NULL )
4496  return NULL;
4497  pNtkAig = Abc_NtkFromAigPhase( pMan );
4498  pNtkAig->pName = Extra_UtilStrsav(pMan->pName);
4499  pNtkAig->pSpec = Extra_UtilStrsav(pMan->pSpec);
4500  Aig_ManStop( pMan );
4501  return pNtkAig;
4502 }
4503 
4504 /**Function*************************************************************
4505 
4506  Synopsis [Performs BDD-based reachability analysis.]
4507 
4508  Description []
4509 
4510  SideEffects []
4511 
4512  SeeAlso []
4513 
4514 ***********************************************************************/
4515 Abc_Ntk_t * Abc_NtkDarUnfold( Abc_Ntk_t * pNtk, int nFrames, int nConfs, int nProps, int fStruct, int fOldAlgo, int fVerbose )
4516 {
4517  Abc_Ntk_t * pNtkAig;
4518  Aig_Man_t * pMan, * pTemp;
4519  assert( Abc_NtkIsStrash(pNtk) );
4520  pMan = Abc_NtkToDar( pNtk, 0, 1 );
4521  if ( pMan == NULL )
4522  return NULL;
4523  if ( fStruct )
4524  pMan = Saig_ManDupUnfoldConstrs( pTemp = pMan );
4525  else
4526  pMan = Saig_ManDupUnfoldConstrsFunc( pTemp = pMan, nFrames, nConfs, nProps, fOldAlgo, fVerbose );
4527  Aig_ManStop( pTemp );
4528  if ( pMan == NULL )
4529  return NULL;
4530  pNtkAig = Abc_NtkFromAigPhase( pMan );
4531  pNtkAig->pName = Extra_UtilStrsav(pMan->pName);
4532  pNtkAig->pSpec = Extra_UtilStrsav(pMan->pSpec);
4533  Aig_ManStop( pMan );
4534  return pNtkAig;
4535 }
4536 
4537 /**Function*************************************************************
4538 
4539  Synopsis [Performs BDD-based reachability analysis.]
4540 
4541  Description []
4542 
4543  SideEffects []
4544 
4545  SeeAlso []
4546 
4547 ***********************************************************************/
4548 Abc_Ntk_t * Abc_NtkDarFold( Abc_Ntk_t * pNtk, int fCompl, int fVerbose )
4549 {
4550  Abc_Ntk_t * pNtkAig;
4551  Aig_Man_t * pMan, * pTemp;
4552  assert( Abc_NtkIsStrash(pNtk) );
4553  pMan = Abc_NtkToDar( pNtk, 0, 1 );
4554  if ( pMan == NULL )
4555  return NULL;
4556  pMan = Saig_ManDupFoldConstrsFunc( pTemp = pMan, fCompl, fVerbose );
4557  Aig_ManStop( pTemp );
4558  pNtkAig = Abc_NtkFromAigPhase( pMan );
4559  pNtkAig->pName = Extra_UtilStrsav(pMan->pName);
4560  pNtkAig->pSpec = Extra_UtilStrsav(pMan->pSpec);
4561  Aig_ManStop( pMan );
4562  return pNtkAig;
4563 }
4564 
4565 /**Function*************************************************************
4566 
4567  Synopsis [Performs BDD-based reachability analysis.]
4568 
4569  Description []
4570 
4571  SideEffects []
4572 
4573  SeeAlso []
4574 
4575 ***********************************************************************/
4576 void Abc_NtkDarConstrProfile( Abc_Ntk_t * pNtk, int fVerbose )
4577 {
4578  extern int Ssw_ManProfileConstraints( Aig_Man_t * p, int nWords, int nFrames, int fVerbose );
4579  extern Vec_Int_t * Saig_ManComputeSwitchProbs( Aig_Man_t * p, int nFrames, int nPref, int fProbOne );
4580  Aig_Man_t * pMan;
4581 // Vec_Int_t * vProbOne;
4582 // Aig_Obj_t * pObj;
4583 // int i, Entry;
4584  assert( Abc_NtkIsStrash(pNtk) );
4585  assert( Abc_NtkConstrNum(pNtk) );
4586  pMan = Abc_NtkToDar( pNtk, 0, 1 );
4587  if ( pMan == NULL )
4588  return;
4589  // value in the init state
4590 // Abc_AigSetNodePhases( pNtk );
4591 /*
4592  // derive probabilities
4593  vProbOne = Saig_ManComputeSwitchProbs( pMan, 48, 16, 1 );
4594  // iterate over the constraint outputs
4595  Saig_ManForEachPo( pMan, pObj, i )
4596  {
4597  Entry = Vec_IntEntry( vProbOne, Aig_ObjId(pObj) );
4598  if ( i < Saig_ManPoNum(pMan) - Saig_ManConstrNum(pMan) )
4599  Abc_Print( 1, "Primary output : ", i );
4600  else
4601  Abc_Print( 1, "Constraint %3d : ", i-(Saig_ManPoNum(pMan) - Saig_ManConstrNum(pMan)) );
4602  Abc_Print( 1, "ProbOne = %f ", Abc_Int2Float(Entry) );
4603  Abc_Print( 1, "AllZeroValue = %d ", Aig_ObjPhase(pObj) );
4604  Abc_Print( 1, "\n" );
4605  }
4606 */
4607  // double-check
4608  Ssw_ManProfileConstraints( pMan, 16, 64, 1 );
4609  Abc_Print( 1, "TwoFrameSatValue = %d.\n", Ssw_ManSetConstrPhases(pMan, 2, NULL) );
4610  // clean up
4611 // Vec_IntFree( vProbOne );
4612  Aig_ManStop( pMan );
4613 }
4614 
4615 /**Function*************************************************************
4616 
4617  Synopsis [Performs BDD-based reachability analysis.]
4618 
4619  Description []
4620 
4621  SideEffects []
4622 
4623  SeeAlso []
4624 
4625 ***********************************************************************/
4626 void Abc_NtkDarTest( Abc_Ntk_t * pNtk, int Num )
4627 {
4628 // extern void Saig_ManDetectConstr( Aig_Man_t * p );
4629 // extern void Saig_ManDetectConstrFuncTest( Aig_Man_t * p );
4630 // extern void Saig_ManFoldConstrTest( Aig_Man_t * pAig );
4631  extern void Llb_ManComputeDomsTest( Aig_Man_t * pAig, int Num );
4632 
4633 
4634 
4635 // extern void Fsim_ManTest( Aig_Man_t * pAig );
4636  extern Vec_Int_t * Saig_StrSimPerformMatching( Aig_Man_t * p0, Aig_Man_t * p1, int nDist, int fVerbose, Aig_Man_t ** ppMiter );
4637 // Vec_Int_t * vPairs;
4638  Aig_Man_t * pMan;//, * pMan2;//, * pTemp;
4639  assert( Abc_NtkIsStrash(pNtk) );
4640  pMan = Abc_NtkToDar( pNtk, 0, 1 );
4641  if ( pMan == NULL )
4642  return;
4643 /*
4644 Aig_ManSetRegNum( pMan, pMan->nRegs );
4645 Aig_ManPrintStats( pMan );
4646 Saig_ManDumpBlif( pMan, "_temp_.blif" );
4647 Aig_ManStop( pMan );
4648 pMan = Saig_ManReadBlif( "_temp_.blif" );
4649 Aig_ManPrintStats( pMan );
4650 */
4651 /*
4652  Aig_ManSetRegNum( pMan, pMan->nRegs );
4653  pTemp = Ssw_SignalCorrespondeceTestPairs( pMan );
4654  Aig_ManStop( pTemp );
4655 */
4656 
4657 /*
4658 // Ssw_SecSpecialMiter( pMan, NULL, 2, 1 );
4659  pMan2 = Aig_ManDupSimple(pMan);
4660  vPairs = Saig_StrSimPerformMatching( pMan, pMan2, 0, 1, NULL );
4661  Vec_IntFree( vPairs );
4662  Aig_ManStop( pMan );
4663  Aig_ManStop( pMan2 );
4664 */
4665 // Ioa_WriteAigerBufferTest( pMan, "test.aig", 0, 0 );
4666 // Saig_ManFoldConstrTest( pMan );
4667  {
4668  extern void Saig_ManBmcSectionsTest( Aig_Man_t * p );
4669  extern void Saig_ManBmcTerSimTest( Aig_Man_t * p );
4670  extern void Saig_ManBmcSupergateTest( Aig_Man_t * p );
4671  extern void Saig_ManBmcMappingTest( Aig_Man_t * p );
4672 // Saig_ManBmcSectionsTest( pMan );
4673 // Saig_ManBmcTerSimTest( pMan );
4674 // Saig_ManBmcSupergateTest( pMan );
4675 // Saig_ManBmcMappingTest( pMan );
4676  }
4677 
4678  {
4679 // void Pdr_ManEquivClasses( Aig_Man_t * pMan );
4680 // Pdr_ManEquivClasses( pMan );
4681  }
4682 
4683 // Llb_ManComputeDomsTest( pMan, Num );
4684  {
4685  extern void Llb_ManMinCutTest( Aig_Man_t * pMan, int Num );
4686  extern void Llb_BddStructAnalysis( Aig_Man_t * pMan );
4687  extern void Llb_NonlinExperiment( Aig_Man_t * pAig, int Num );
4688 // Llb_BddStructAnalysis( pMan );
4689  Llb_ManMinCutTest( pMan, Num );
4690 // Llb_NonlinExperiment( pMan, Num );
4691  }
4692 
4693 // Saig_MvManSimulate( pMan, 1 );
4694 // Saig_ManDetectConstr( pMan );
4695 // Saig_ManDetectConstrFuncTest( pMan );
4696 
4697 // Fsim_ManTest( pMan );
4698  Aig_ManStop( pMan );
4699 
4700 }
4701 
4702 /**Function*************************************************************
4703 
4704  Synopsis [Performs BDD-based reachability analysis.]
4705 
4706  Description []
4707 
4708  SideEffects []
4709 
4710  SeeAlso []
4711 
4712 ***********************************************************************/
4714 {
4715 // extern Aig_Man_t * Saig_ManDualRail( Aig_Man_t * p, int fMiter );
4716 
4717 /*
4718  extern Aig_Man_t * Ssw_SignalCorrespondeceTestPairs( Aig_Man_t * pAig );
4719 
4720  Abc_Ntk_t * pNtkAig;
4721  Aig_Man_t * pMan, * pTemp;
4722  assert( Abc_NtkIsStrash(pNtk) );
4723  pMan = Abc_NtkToDar( pNtk, 0, 1 );
4724  if ( pMan == NULL )
4725  return NULL;
4726 
4727  Aig_ManSetRegNum( pMan, pMan->nRegs );
4728  pMan = Ssw_SignalCorrespondeceTestPairs( pTemp = pMan );
4729  Aig_ManStop( pTemp );
4730  if ( pMan == NULL )
4731  return NULL;
4732 
4733  pNtkAig = Abc_NtkFromAigPhase( pMan );
4734  pNtkAig->pName = Extra_UtilStrsav(pNtk->pName);
4735  pNtkAig->pSpec = Extra_UtilStrsav(pNtk->pSpec);
4736  Aig_ManStop( pMan );
4737  return pNtkAig;
4738 */
4739  Abc_Ntk_t * pNtkAig;
4740  Aig_Man_t * pMan;//, * pTemp;
4741  assert( Abc_NtkIsStrash(pNtk) );
4742  pMan = Abc_NtkToDar( pNtk, 0, 1 );
4743  if ( pMan == NULL )
4744  return NULL;
4745 
4746 /*
4747  Aig_ManSetRegNum( pMan, pMan->nRegs );
4748  pMan = Saig_ManDualRail( pTemp = pMan, 1 );
4749  Aig_ManStop( pTemp );
4750  if ( pMan == NULL )
4751  return NULL;
4752 
4753  pNtkAig = Abc_NtkFromAigPhase( pMan );
4754  pNtkAig->pName = Extra_UtilStrsav(pNtk->pName);
4755  pNtkAig->pSpec = Extra_UtilStrsav(pNtk->pSpec);
4756  Aig_ManStop( pMan );
4757 */
4758 
4759  pNtkAig = Abc_NtkFromDar( pNtk, pMan );
4760  Aig_ManStop( pMan );
4761 
4762  return pNtkAig;
4763 
4764 }
4765 
4766 ////////////////////////////////////////////////////////////////////////
4767 /// END OF FILE ///
4768 ////////////////////////////////////////////////////////////////////////
4769 
4770 #include "abcDarUnfold2.c"
4772 
char * memset()
Aig_Obj_t * Aig_ObjCreateCo(Aig_Man_t *p, Aig_Obj_t *pDriver)
Definition: aigObj.c:66
abctime timeInt
Definition: abcDar.c:3800
static int Gia_ObjIsCellBuf(Gia_Man_t *p, int iLit)
Definition: gia.h:962
ABC_NAMESPACE_IMPL_START void Fra_ManPartitionTest(Aig_Man_t *p, int nComLim)
DECLARATIONS ///.
Definition: fraPart.c:45
Vec_Ptr_t * Amap_ManTest(Aig_Man_t *pAig, Amap_Par_t *pPars)
Definition: amapCore.c:70
int fNonConstOut
Definition: fra.h:179
static unsigned Abc_ObjId(Abc_Obj_t *pObj)
Definition: abc.h:329
Aig_Man_t * Saig_ManDupUnfoldConstrs(Aig_Man_t *pAig)
Definition: saigConstr.c:282
Mio_Gate_t * Mio_LibraryReadGateByName(Mio_Library_t *pLib, char *pName, char *pOutName)
Definition: mioApi.c:99
static void Aig_ObjSetEquiv(Aig_Man_t *p, Aig_Obj_t *pObj, Aig_Obj_t *pEqu)
Definition: aig.h:329
static Vec_Ptr_t * Vec_PtrStart(int nSize)
Definition: vecPtr.h:106
int fFraiging
Definition: fra.h:103
static int Gia_ObjFaninC2(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:453
int Nm_ManFindIdByName(Nm_Man_t *p, char *pName, int Type)
Definition: nmApi.c:219
static int Abc_NtkIsStrash(Abc_Ntk_t *pNtk)
Definition: abc.h:251
Vec_Ptr_t * Abc_NtkCollectCiNames(Abc_Ntk_t *pNtk)
Definition: abcDar.c:1243
char * pName
Definition: mio.h:49
static int Gia_ObjCellId(Gia_Man_t *p, int iLit)
Definition: gia.h:966
int Abc_NtkDarReach(Abc_Ntk_t *pNtk, Saig_ParBbr_t *pPars)
Definition: abcDar.c:4321
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Abc_Ntk_t * Abc_NtkDarFold(Abc_Ntk_t *pNtk, int fCompl, int fVerbose)
Definition: abcDar.c:4548
ABC_DLL int Aig_ManCheck(Aig_Man_t *p)
FUNCTION DECLARATIONS ///.
Definition: aigCheck.c:45
void Abc_CollectTopOr(Abc_Obj_t *pObj, Vec_Ptr_t *vSuper)
Definition: abcDar.c:88
ABC_DLL void Abc_NtkMakeComb(Abc_Ntk_t *pNtk, int fRemoveLatches)
Definition: abcNtk.c:1422
static Aig_Obj_t * Aig_ObjRepr(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:330
ABC_DLL void * Abc_FrameReadLibGen()
Definition: mainFrame.c:56
void Llb_NonlinExperiment(Aig_Man_t *pAig, int Num)
Definition: llb3Nonlin.c:806
unsigned Level
Definition: aig.h:82
int Abc_NtkDarBmcInter_int(Aig_Man_t *pMan, Inter_ManParams_t *pPars, Aig_Man_t **ppNtkRes)
Definition: abcDar.c:2443
int pFans[0]
Definition: amap.h:64
Vec_Int_t * Abc_NtkFindDcLatches(Abc_Ntk_t *pNtk)
Definition: abcDar.c:207
int nFrames
Definition: fra.h:175
int Saig_ManBmcScalable(Aig_Man_t *pAig, Saig_ParBmc_t *pPars)
Definition: bmcBmc3.c:1390
int nDropOuts
Definition: bmc.h:72
Nm_Man_t * pManName
Definition: abc.h:160
void Gia_ManStop(Gia_Man_t *p)
Definition: giaMan.c:77
Abc_Ntk_t * Abc_NtkDch(Abc_Ntk_t *pNtk, Dch_Pars_t *pPars)
Definition: abcDar.c:1584
Abc_Ntk_t * Abc_NtkFromDar(Abc_Ntk_t *pNtkOld, Aig_Man_t *pMan)
Definition: abcDar.c:414
int nWords
Definition: gia.h:241
Vec_Ptr_t * vSeqModelVec
Definition: abc.h:200
int Abc_NtkPartitionedSat(Abc_Ntk_t *pNtk, int nAlgo, int nPartSize, int nConfPart, int nConfTotal, int fAlignPol, int fSynthesize, int fVerbose)
Definition: abcDar.c:1829
#define Gia_ManForEachCo(p, pObj, i)
Definition: gia.h:1022
typedefABC_NAMESPACE_HEADER_START struct Vec_Vec_t_ Vec_Vec_t
INCLUDES ///.
Definition: vecVec.h:42
ABC_NAMESPACE_IMPL_START int Abc_ObjCompareById(Abc_Obj_t **pp1, Abc_Obj_t **pp2)
DECLARATIONS ///.
Definition: abcDar.c:61
static int Saig_ManPoNum(Aig_Man_t *p)
Definition: saig.h:74
ABC_DLL int * Abc_NtkVerifyGetCleanModel(Abc_Ntk_t *pNtk, int nFrames)
Definition: abcVerify.c:668
static int Saig_ObjIsLo(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:84
Aig_Man_t * Saig_ManRetimeMinArea(Aig_Man_t *p, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose)
Definition: saigRetMin.c:623
int Aig_ManCoCleanup(Aig_Man_t *p)
Definition: aigMan.c:345
static int Abc_ObjIsBo(Abc_Obj_t *pObj)
Definition: abc.h:350
ABC_DLL Abc_Obj_t * Abc_AigConst1(Abc_Ntk_t *pNtk)
Definition: abcAig.c:683
static int Gia_ManPoNum(Gia_Man_t *p)
Definition: gia.h:386
Abc_Ntk_t * Abc_NtkFromMappedGia(Gia_Man_t *p)
Definition: abcDar.c:714
static int Gia_ObjFaninC1(Gia_Obj_t *pObj)
Definition: gia.h:452
Cnf_Dat_t * Cnf_Derive(Aig_Man_t *pAig, int nOutputs)
Definition: cnfCore.c:165
Hop_Obj_t * Hop_And(Hop_Man_t *p, Hop_Obj_t *p0, Hop_Obj_t *p1)
Definition: hopOper.c:104
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
void Abc_NtkDarConstrProfile(Abc_Ntk_t *pNtk, int fVerbose)
Definition: abcDar.c:4576
Abc_Ntk_t * Abc_NtkDarEnlarge(Abc_Ntk_t *pNtk, int nFrames, int fVerbose)
Definition: abcDar.c:3628
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Abc_Ntk_t * Abc_NtkDarTestNtk(Abc_Ntk_t *pNtk)
Definition: abcDar.c:4713
int Saig_ManRetimeSteps(Aig_Man_t *p, int nSteps, int fForward, int fAddBugs)
Definition: saigRetStep.c:181
void Abc_NtkPrintSccs(Abc_Ntk_t *pNtk, int fVerbose)
Definition: abcDar.c:3888
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
void Aig_ManStop(Aig_Man_t *p)
Definition: aigMan.c:187
int Abc_NtkDarDemiterNew(Abc_Ntk_t *pNtk)
Definition: abcDar.c:2644
int Gia_ManSimSimulate(Gia_Man_t *pAig, Gia_ParSim_t *pPars)
Definition: giaSim.c:598
typedefABC_NAMESPACE_HEADER_START struct Pdr_Par_t_ Pdr_Par_t
INCLUDES ///.
Definition: pdr.h:40
void Cnf_DataWriteIntoFile(Cnf_Dat_t *p, char *pFileName, int fReadable, Vec_Int_t *vForAlls, Vec_Int_t *vExists)
Definition: cnfMan.c:318
Fra_Sml_t * Fra_SmlSimulateSeq(Aig_Man_t *pAig, int nPref, int nFrames, int nWords, int fCheckMiter)
Definition: fraSim.c:1021
int Abc_NtkDarSec(Abc_Ntk_t *pNtk1, Abc_Ntk_t *pNtk2, Fra_Sec_t *pSecPar)
Definition: abcDar.c:2877
int Aig_ManSeqCleanup(Aig_Man_t *p)
Definition: aigScl.c:158
Abc_Ntk_t * Abc_NtkDarFrames(Abc_Ntk_t *pNtk, int nPrefix, int nFrames, int fInit, int fVerbose)
Definition: abcDar.c:4255
int Abc_NtkDarProve(Abc_Ntk_t *pNtk, Fra_Sec_t *pSecPar, int nBmcFramesMax, int nBmcConfMax)
Definition: abcDar.c:2767
int nClauses
Definition: cnf.h:61
void Abc_NtkInterFast(Abc_Ntk_t *pNtkOn, Abc_Ntk_t *pNtkOff, int fVerbose)
Definition: abcDar.c:3782
static int Gia_ObjFaninLit0p(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:469
Aig_Man_t * Saig_ManPhaseAbstract(Aig_Man_t *p, Vec_Int_t *vInits, int nFrames, int nPref, int fIgnore, int fPrint, int fVerbose)
Definition: saigPhase.c:911
int Saig_ManVerifyCex(Aig_Man_t *pAig, Abc_Cex_t *p)
Definition: saigDup.c:279
Hop_Obj_t * Abc_ObjHopFromGia(Hop_Man_t *pHopMan, Gia_Man_t *p, int GiaId, Vec_Ptr_t *vCopies)
Definition: abcDar.c:689
static int Abc_ObjFanoutNum(Abc_Obj_t *pObj)
Definition: abc.h:365
int fUseNewProver
Definition: fra.h:136
void * pData
Definition: aig.h:87
ABC_NAMESPACE_IMPL_END ABC_NAMESPACE_IMPL_START Abc_Ntk_t * Amap_ManProduceNetwork(Abc_Ntk_t *pNtk, Vec_Ptr_t *vMapping)
Definition: abcDar.c:4355
typedefABC_NAMESPACE_HEADER_START struct Ssw_Pars_t_ Ssw_Pars_t
INCLUDES ///.
Definition: ssw.h:40
static int Abc_NtkBoxNum(Abc_Ntk_t *pNtk)
Definition: abc.h:289
Aig_Man_t * Fra_FraigLatchCorrespondence(Aig_Man_t *pAig, int nFramesP, int nConfMax, int fProve, int fVerbose, int *pnIter, float TimeLimit)
Definition: fraLcr.c:531
Aig_Man_t * Saig_ManDupFoldConstrsFunc(Aig_Man_t *pAig, int fCompl, int fVerbose)
Definition: saigConstr2.c:942
int Abc_NtkDarSimSec(Abc_Ntk_t *pNtk1, Abc_Ntk_t *pNtk2, Ssw_Pars_t *pPars)
Definition: abcDar.c:3108
Abc_Ntk_t * Abc_NtkDarExtWin(Abc_Ntk_t *pNtk, int nObjId, int nDist, int fVerbose)
Definition: abcDar.c:4132
Abc_Ntk_t * Abc_NtkDarOutdec(Abc_Ntk_t *pNtk, int nLits, int fVerbose)
Definition: abcDar.c:4485
int nBarBufs2
Definition: abc.h:175
int nVars
Definition: cnf.h:59
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
static void Vec_PtrFreeFree(Vec_Ptr_t *p)
Definition: vecPtr.h:569
static Abc_Obj_t * Abc_NtkFromCellRead(Abc_Ntk_t *p, Vec_Int_t *vCopyLits, int i, int c)
Definition: abcDar.c:854
ABC_DLL char * Abc_SopCreateAnd(Mem_Flex_t *pMan, int nVars, int *pfCompl)
Definition: abcSop.c:162
static int Abc_Var2Lit(int Var, int fCompl)
Definition: abc_global.h:263
Aig_Man_t * Aig_ManStart(int nNodesMax)
DECLARATIONS ///.
Definition: aigMan.c:47
Aig_Man_t * Aig_ManDupDfs(Aig_Man_t *p)
Definition: aigDup.c:563
static Abc_Obj_t * Abc_ObjChild1Copy(Abc_Obj_t *pObj)
Definition: abc.h:387
void Aig_ManPrintStats(Aig_Man_t *p)
Definition: aigMan.c:379
static int Abc_ObjIsBarBuf(Abc_Obj_t *pObj)
Definition: abc.h:360
ABC_DLL char * Abc_SopCreateFromIsop(Mem_Flex_t *pMan, int nVars, Vec_Int_t *vCover)
Definition: abcSop.c:416
Aig_Man_t * Ssw_SignalCorrespondence(Aig_Man_t *pAig, Ssw_Pars_t *pPars)
Definition: sswCore.c:414
abctime timeCnf
DECLARATIONS ///.
Definition: abcDar.c:3798
int Dar_ManRewrite(Aig_Man_t *pAig, Dar_RwrPar_t *pPars)
Definition: darCore.c:78
int nFramesMax
Definition: fra.h:118
int Fra_Clau(Aig_Man_t *pMan, int nIters, int fVerbose, int fVeryVerbose)
Definition: fraClau.c:637
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition: aig.h:393
int Saig_ManBmcSimple(Aig_Man_t *pAig, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fVerbose, int *piFrame, int nCofFanLit)
Definition: bmcBmc.c:186
ABC_DLL Abc_Obj_t * Abc_NtkDupObj(Abc_Ntk_t *pNtkNew, Abc_Obj_t *pObj, int fCopyName)
Definition: abcObj.c:337
unsigned * pMuxes
Definition: gia.h:104
void Cnf_DataTranformPolarity(Cnf_Dat_t *pCnf, int fTransformPos)
Definition: cnfMan.c:652
Abc_Ntk_t * Abc_NtkDarAmap(Abc_Ntk_t *pNtk, Amap_Par_t *pPars)
Definition: abcDar.c:4415
static int Gia_ObjValue(Gia_Obj_t *pObj)
Definition: gia.h:413
static int Abc_NtkLatchNum(Abc_Ntk_t *pNtk)
Definition: abc.h:294
char * pName
Definition: amap.h:61
ABC_DLL Abc_Obj_t * Abc_NtkCreateNodeConst1(Abc_Ntk_t *pNtk)
Definition: abcObj.c:633
Aig_Man_t * Aig_ManRetimeFrontier(Aig_Man_t *p, int nStepsMax)
Definition: aigRetF.c:125
Abc_Ntk_t * Abc_NtkDarRetime(Abc_Ntk_t *pNtk, int nStepsMax, int fVerbose)
Definition: abcDar.c:3245
static int Abc_ObjFaninC0(Abc_Obj_t *pObj)
Definition: abc.h:377
static int Abc_ObjIsPi(Abc_Obj_t *pObj)
Definition: abc.h:347
ABC_DLL Abc_Ntk_t * Abc_NtkDup(Abc_Ntk_t *pNtk)
Definition: abcNtk.c:419
Aig_Obj_t * Aig_ObjCreateCi(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigObj.c:45
int fVerbose
Definition: bmc.h:66
Abc_Ntk_t * Abc_NtkDarMatch(Abc_Ntk_t *pNtk1, Abc_Ntk_t *pNtk2, int nDist, int fVerbose)
Definition: abcDar.c:3151
int Saig_ManDemiterDual(Aig_Man_t *p, Aig_Man_t **ppAig0, Aig_Man_t **ppAig1)
Definition: saigMiter.c:708
Abc_Ntk_t * Abc_NtkDarSynch(Abc_Ntk_t *pNtk1, Abc_Ntk_t *pNtk2, int nWords, int fVerbose)
Definition: abcDar.c:4057
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
static Aig_Obj_t * Aig_ManConst0(Aig_Man_t *p)
Definition: aig.h:263
#define Aig_ManForEachCo(p, pObj, i)
Definition: aig.h:398
int Saig_BmcPerform(Aig_Man_t *pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int *piFrames, int fSilent)
Definition: bmcBmc2.c:761
static int Abc_NtkCiNum(Abc_Ntk_t *pNtk)
Definition: abc.h:287
static int Abc_LatchIsInit0(Abc_Obj_t *pLatch)
Definition: abc.h:422
Abc_Ntk_t * Abc_NtkBalanceExor(Abc_Ntk_t *pNtk, int fUpdateLevel, int fVerbose)
Definition: abcDar.c:3935
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
int nFailOuts
Definition: bmc.h:71
static Aig_Obj_t * Aig_ManObj(Aig_Man_t *p, int i)
Definition: aig.h:270
#define Abc_NtkForEachCo(pNtk, pCo, i)
Definition: abc.h:519
Vec_Int_t * Saig_StrSimPerformMatching(Aig_Man_t *p0, Aig_Man_t *p1, int nDist, int fVerbose, Aig_Man_t **ppMiter)
Definition: saigStrSim.c:873
static Abc_Obj_t * Abc_NtkCi(Abc_Ntk_t *pNtk, int i)
Definition: abc.h:317
int Abc_NtkDarPrintCone(Abc_Ntk_t *pNtk)
Definition: abcDar.c:3911
static Aig_Obj_t * Aig_Not(Aig_Obj_t *p)
Definition: aig.h:247
ABC_DLL int Abc_NtkCheck(Abc_Ntk_t *pNtk)
FUNCTION DEFINITIONS ///.
Definition: abcCheck.c:61
void Prove_ParamsSetDefault(Prove_Params_t *pParams)
FUNCTION DEFINITIONS ///.
Definition: fraigMan.c:46
typedefABC_NAMESPACE_HEADER_START struct Dch_Pars_t_ Dch_Pars_t
INCLUDES ///.
Definition: dch.h:43
ABC_DLL char * Abc_ObjAssignName(Abc_Obj_t *pObj, char *pName, char *pSuffix)
Definition: abcNames.c:68
int iFrame
Definition: bmc.h:70
ABC_DLL Vec_Ptr_t * Abc_NtkDfs(Abc_Ntk_t *pNtk, int fCollectAll)
Definition: abcDfs.c:81
static abctime Abc_Clock()
Definition: abc_global.h:279
int nConfLimit
Definition: bmc.h:50
static int Abc_MaxInt(int a, int b)
Definition: abc_global.h:238
Hop_Obj_t * Abc_ObjHopFromGia_rec(Hop_Man_t *pHopMan, Gia_Man_t *p, int Id, Vec_Ptr_t *vCopies)
Definition: abcDar.c:672
static Abc_Obj_t * Abc_NtkObj(Abc_Ntk_t *pNtk, int i)
Definition: abc.h:314
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
static Vec_Int_t * Vec_IntStartNatural(int nSize)
Definition: bblif.c:192
Definition: cnf.h:56
Aig_Man_t * Dar_ManChoice(Aig_Man_t *pAig, int fBalance, int fUpdateLevel, int fConstruct, int nConfMax, int nLevelMax, int fVerbose)
Definition: darScript.c:378
Abc_Ntk_t * Abc_NtkDarRetimeMinArea(Abc_Ntk_t *pNtk, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose)
Definition: abcDar.c:3349
static void * Vec_PtrPop(Vec_Ptr_t *p)
Definition: vecPtr.h:677
Abc_Ntk_t * Abc_NtkDarInsWin(Abc_Ntk_t *pNtk, Abc_Ntk_t *pCare, int nObjId, int nDist, int fVerbose)
Definition: abcDar.c:4189
Abc_Ntk_t * Abc_NtkDar(Abc_Ntk_t *pNtk)
Definition: abcDar.c:1318
static Vec_Int_t * Vec_IntStartFull(int nSize)
Definition: vecInt.h:119
Abc_Ntk_t * Abc_NtkDarRetimeStep(Abc_Ntk_t *pNtk, int fVerbose)
Definition: abcDar.c:3380
int nWords
Definition: abcNpn.c:127
static Abc_Obj_t * Abc_ObjFanin0(Abc_Obj_t *pObj)
Definition: abc.h:373
ABC_DLL int Abc_NtkGetChoiceNum(Abc_Ntk_t *pNtk)
Definition: abcUtil.c:430
ABC_NAMESPACE_IMPL_START Aig_Man_t * Dar_ManRwsat(Aig_Man_t *pAig, int fBalance, int fVerbose)
DECLARATIONS ///.
Definition: darScript.c:71
static Gia_Obj_t * Gia_ManObj(Gia_Man_t *p, int v)
Definition: gia.h:402
Abc_Ntk_t * Abc_NtkDarFraigPart(Abc_Ntk_t *pNtk, int nPartSize, int nConfLimit, int nLevelMax, int fVerbose)
Definition: abcDar.c:1393
Definition: hop.h:65
static int Abc_NtkCoNum(Abc_Ntk_t *pNtk)
Definition: abc.h:288
DECLARATIONS ///.
Definition: abcAig.c:52
Definition: gia.h:75
int fVerbose
Definition: gia.h:246
#define Gia_ManForEachLut(p, i)
Definition: gia.h:968
Aig_Man_t * Saig_ManTempor(Aig_Man_t *pAig, int nFrames, int TimeOut, int nConfLimit, int fUseBmc, int fUseTransSigs, int fVerbose, int fVeryVerbose)
Definition: saigTempor.c:186
ABC_DLL Abc_Ntk_t * Abc_NtkFraig(Abc_Ntk_t *pNtk, void *pParams, int fAllNodes, int fExdc)
FUNCTION DEFINITIONS ///.
Definition: abcFraig.c:58
Aig_Man_t * Saig_ManRetimeForward(Aig_Man_t *p, int nMaxIters, int fVerbose)
Definition: saigRetFwd.c:213
static int Abc_ObjIsNone(Abc_Obj_t *pObj)
Definition: abc.h:346
ABC_DLL void Abc_NtkDelete(Abc_Ntk_t *pNtk)
Definition: abcNtk.c:1233
unsigned Level
Definition: abc.h:142
short nFans
Definition: amap.h:63
char * Extra_UtilStrsav(const char *s)
Aig_Obj_t * Aig_And(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:104
int Abc_NtkDarInduction(Abc_Ntk_t *pNtk, int nTimeOut, int nFramesMax, int nConfMax, int fUnique, int fUniqueAll, int fGetCex, int fVerbose, int fVeryVerbose)
Definition: abcDar.c:3681
Abc_Ntk_t * Abc_NtkFromDarChoices(Abc_Ntk_t *pNtkOld, Aig_Man_t *pMan)
Definition: abcDar.c:1109
static Abc_Obj_t * Abc_NtkCo(Abc_Ntk_t *pNtk, int i)
Definition: abc.h:318
Abc_Ntk_t * Abc_NtkInterOne(Abc_Ntk_t *pNtkOn, Abc_Ntk_t *pNtkOff, int fRelation, int fVerbose)
Definition: abcDar.c:3727
int nTimeOut
Definition: bmc.h:53
Aig_Man_t * Aig_ManFrames(Aig_Man_t *pAig, int nFs, int fInit, int fOuts, int fRegs, int fEnlarge, Aig_Obj_t ***ppObjMap)
FUNCTION DEFINITIONS ///.
Definition: aigFrames.c:51
int Abc_NtkDarDemiter(Abc_Ntk_t *pNtk)
Definition: abcDar.c:2593
ABC_DLL void Abc_ObjAddFanin(Abc_Obj_t *pObj, Abc_Obj_t *pFanin)
Definition: abcFanio.c:84
int * pModel
Definition: abc.h:198
ABC_DLL Abc_Ntk_t * Abc_NtkAlloc(Abc_NtkType_t Type, Abc_NtkFunc_t Func, int fUseMemMan)
DECLARATIONS ///.
Definition: abcNtk.c:50
Vec_Int_t * vIsop[2]
Definition: cnf.h:76
void * pData
Definition: abc.h:203
static void Vec_PtrUniqify(Vec_Ptr_t *p, int(*Vec_PtrSortCompare)()) ___unused
Definition: vecPtr.h:875
static unsigned * Cnf_CutTruth(Cnf_Cut_t *pCut)
Definition: cnf.h:103
Abc_Ntk_t * Abc_NtkDarSynchOne(Abc_Ntk_t *pNtk, int nWords, int fVerbose)
Definition: abcDar.c:4029
ABC_DLL void Abc_SopComplementVar(char *pSop, int iVar)
Definition: abcSop.c:630
int Saig_ManDemiterSimpleDiff(Aig_Man_t *p, Aig_Man_t **ppAig0, Aig_Man_t **ppAig1)
Definition: saigMiter.c:660
int Saig_ManPhaseFrameNum(Aig_Man_t *p, Vec_Int_t *vInits)
Definition: saigPhase.c:841
ABC_DLL Abc_Obj_t * Abc_AigXor(Abc_Aig_t *pMan, Abc_Obj_t *p0, Abc_Obj_t *p1)
Definition: abcAig.c:735
int fVerbose
Definition: fra.h:139
static Abc_Obj_t * Abc_NtkCreateBo(Abc_Ntk_t *pNtk)
Definition: abc.h:306
static Abc_Obj_t * Abc_ObjChild0(Abc_Obj_t *pObj)
Definition: abc.h:383
Gia_Man_t * Gia_ManFromAig(Aig_Man_t *p)
INCLUDES ///.
Definition: giaAig.c:73
void Aig_ManPrintControlFanouts(Aig_Man_t *p)
Definition: aigUtil.c:1027
#define Gia_ManForEachRiRo(p, pObjRi, pObjRo, i)
Definition: gia.h:1042
static void Abc_PrintTime(int level, const char *pStr, abctime time)
Definition: abc_global.h:367
static int Aig_ManBufNum(Aig_Man_t *p)
Definition: aig.h:253
static int Aig_ObjIsNode(Aig_Obj_t *pObj)
Definition: aig.h:280
Abc_Ntk_t * Abc_NtkDarLatchSweep(Abc_Ntk_t *pNtk, int fLatchConst, int fLatchEqual, int fSaveNames, int fUseMvSweep, int nFramesSymb, int nFramesSatur, int fVerbose, int fVeryVerbose)
Definition: abcDar.c:3203
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
static Vec_Vec_t * Vec_VecDupInt(Vec_Vec_t *p)
Definition: vecVec.h:395
void * pManFunc
Definition: abc.h:191
static int Abc_ObjIsNode(Abc_Obj_t *pObj)
Definition: abc.h:355
int Abc_NtkDarDemiterDual(Abc_Ntk_t *pNtk, int fVerbose)
Definition: abcDar.c:2697
static int Abc_NtkNodeNum(Abc_Ntk_t *pNtk)
Definition: abc.h:293
static int Aig_ManCoNum(Aig_Man_t *p)
Definition: aig.h:252
Abc_Cex_t * Fra_SmlGetCounterExample(Fra_Sml_t *p)
Definition: fraSim.c:1043
Abc_Ntk_t * Abc_NtkDarRetimeF(Abc_Ntk_t *pNtk, int nStepsMax, int fVerbose)
Definition: abcDar.c:3279
ABC_DLL Abc_Obj_t * Abc_AigAnd(Abc_Aig_t *pMan, Abc_Obj_t *p0, Abc_Obj_t *p1)
Definition: abcAig.c:700
static int Aig_ObjIsBuf(Aig_Obj_t *pObj)
Definition: aig.h:277
ABC_DLL void Abc_NtkAddDummyPoNames(Abc_Ntk_t *pNtk)
Definition: abcNames.c:398
static Vec_Int_t * Vec_IntStart(int nSize)
Definition: bblif.c:172
static int Abc_LitIsCompl(int Lit)
Definition: abc_global.h:265
void Fra_ParamsDefault(Fra_Par_t *pParams)
DECLARATIONS ///.
Definition: fraMan.c:45
static Abc_Obj_t * Abc_ObjChild0Copy(Abc_Obj_t *pObj)
Definition: abc.h:386
static int Saig_ManConstrNum(Aig_Man_t *p)
Definition: saig.h:78
ABC_DLL Abc_Ntk_t * Abc_NtkStartFrom(Abc_Ntk_t *pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func)
Definition: abcNtk.c:106
static int Gia_ObjIsMuxId(Gia_Man_t *p, int iObj)
Definition: gia.h:424
int Abc_NtkDarSeqSim3(Abc_Ntk_t *pNtk, Ssw_RarPars_t *pPars)
Definition: abcDar.c:3542
static Gia_Obj_t * Gia_ObjFanin0(Gia_Obj_t *pObj)
Definition: gia.h:454
Abc_Obj_t * pCopy
Definition: abc.h:148
Aig_Man_t * Abc_NtkToDarChoices(Abc_Ntk_t *pNtk)
Definition: abcDar.c:354
ABC_DLL void Abc_NtkDeleteObj(Abc_Obj_t *pObj)
Definition: abcObj.c:167
#define Aig_ManForEachNode(p, pObj, i)
Definition: aig.h:413
Definition: cnf.h:71
int Abc_NtkDarPdr(Abc_Ntk_t *pNtk, Pdr_Par_t *pPars)
Definition: abcDar.c:2965
Aig_Man_t * Aig_ManReduceLaches(Aig_Man_t *p, int fVerbose)
Definition: aigScl.c:455
Aig_Man_t * Saig_Synchronize(Aig_Man_t *pAig1, Aig_Man_t *pAig2, int nWords, int fVerbose)
Definition: saigSynch.c:556
char * pName
Definition: gia.h:97
void Abc_CollectTopOr_rec(Abc_Obj_t *pObj, Vec_Ptr_t *vSuper)
Definition: abcDar.c:77
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
static int Gia_ObjLutSize(Gia_Man_t *p, int Id)
Definition: gia.h:953
void Aig_ObjPatchFanin0(Aig_Man_t *p, Aig_Obj_t *pObj, Aig_Obj_t *pFaninNew)
Definition: aigObj.c:282
int fCheckMiter
Definition: gia.h:245
ABC_DLL int Abc_AigCleanup(Abc_Aig_t *pMan)
Definition: abcAig.c:194
int Saig_ManDemiterNew(Aig_Man_t *pMan)
Definition: saigMiter.c:1230
Vec_Int_t * Saig_ManComputeSwitchProbs(Aig_Man_t *pAig, int nFrames, int nPref, int fProbOne)
Definition: giaSwitch.c:684
void Saig_ManPrintCones(Aig_Man_t *p)
FUNCTION DECLARATIONS ///.
Definition: saigCone.c:159
int Fra_FraigCecPartitioned(Aig_Man_t *pMan1, Aig_Man_t *pMan2, int nConfLimit, int nPartSize, int fSmart, int fVerbose)
Definition: fraCec.c:451
ABC_DLL Abc_Obj_t * Abc_NtkCreateNodeInv(Abc_Ntk_t *pNtk, Abc_Obj_t *pFanin)
Definition: abcObj.c:662
int Dar_ManRefactor(Aig_Man_t *pAig, Dar_RefPar_t *pPars)
Definition: darRefact.c:496
void Aig_ManSetRegNum(Aig_Man_t *p, int nRegs)
Definition: aigMan.c:438
void Cnf_ManFree()
Definition: cnfCore.c:58
ABC_DLL Abc_Ntk_t * Abc_NtkMiter(Abc_Ntk_t *pNtk1, Abc_Ntk_t *pNtk2, int fComb, int nPartSize, int fImplic, int fMulti)
FUNCTION DEFINITIONS ///.
Definition: abcMiter.c:56
Abc_Ntk_t * Abc_NtkDrwsat(Abc_Ntk_t *pNtk, int fBalance, int fVerbose)
Definition: abcDar.c:1631
Abc_Ntk_t * Abc_NtkCSweep(Abc_Ntk_t *pNtk, int nCutsMax, int nLeafMax, int fVerbose)
Definition: abcDar.c:1418
Aig_Man_t * Aig_ManScl(Aig_Man_t *pAig, int fLatchConst, int fLatchEqual, int fUseMvSweep, int nFramesSymb, int nFramesSatur, int fVerbose, int fVeryVerbose)
Definition: aigScl.c:650
static Aig_Obj_t * Aig_ManCi(Aig_Man_t *p, int i)
Definition: aig.h:266
#define Aig_ManForEachLiLoSeq(p, pObjLi, pObjLo, k)
Definition: aig.h:450
int Ssw_SecWithSimilarity(Aig_Man_t *p0, Aig_Man_t *p1, Ssw_Pars_t *pPars)
Definition: sswIslands.c:542
void Cnf_SopConvertToVector(char *pSop, int nCubes, Vec_Int_t *vCover)
Definition: cnfWrite.c:82
Aig_Man_t * Dar_ManCompress2(Aig_Man_t *pAig, int fBalance, int fUpdateLevel, int fFanout, int fPower, int fVerbose)
Definition: darScript.c:235
Fra_Sml_t * Fra_SmlSimulateComb(Aig_Man_t *pAig, int nWords, int fCheckMiter)
Definition: fraSim.c:856
int Inter_ManPerformInterpolation(Aig_Man_t *pAig, Inter_ManParams_t *pPars, int *piFrame)
Definition: intCore.c:79
ABC_DLL int Abc_NtkIvyProve(Abc_Ntk_t **ppNtk, void *pPars)
Definition: abcIvy.c:498
Cnf_Dat_t * Cnf_DeriveFast(Aig_Man_t *p, int nOutputs)
Definition: cnfFast.c:666
void Ssw_ManSetDefaultParams(Ssw_Pars_t *p)
DECLARATIONS ///.
Definition: sswCore.c:45
char * Extra_FileNameGeneric(char *FileName)
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
Aig_Man_t * Aig_ManConstReduce(Aig_Man_t *p, int fUseMvSweep, int nFramesSymb, int nFramesSatur, int fVerbose, int fVeryVerbose)
Definition: aigTsim.c:498
static int Aig_ManCiNum(Aig_Man_t *p)
Definition: aig.h:251
int Nm_ManFindIdByNameTwoTypes(Nm_Man_t *p, char *pName, int Type1, int Type2)
Definition: nmApi.c:239
static int Abc_Base10Log(unsigned n)
Definition: abc_global.h:252
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
static int Abc_LatchIsInitDc(Abc_Obj_t *pLatch)
Definition: abc.h:424
#define Cnf_CutForEachLeaf(p, pCut, pLeaf, i)
Definition: cnf.h:121
int Saig_ManDetectConstrTest(Aig_Man_t *p)
Definition: saigConstr.c:469
char * pSpec
Definition: gia.h:98
ABC_DLL char * Abc_SopCreateXor(Mem_Flex_t *pMan, int nVars)
Definition: abcSop.c:274
void Fraig_ParamsSetDefault(Fraig_Params_t *pParams)
Definition: fraigMan.c:122
static int Aig_ObjIsConst1(Aig_Obj_t *pObj)
Definition: aig.h:274
ABC_DLL char * Abc_ObjNameDummy(char *pPrefix, int Num, int nDigits)
Definition: abcNames.c:121
ABC_DLL Abc_Ntk_t * Abc_NtkCreateCone(Abc_Ntk_t *pNtk, Abc_Obj_t *pNode, char *pNodeName, int fUseAllCis)
Definition: abcNtk.c:819
static Aig_Obj_t * Aig_ObjEquiv(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:328
Definition: fra.h:92
static Aig_Obj_t * Aig_ObjChild1Copy(Aig_Obj_t *pObj)
Definition: aig.h:313
void Abc_NtkDarTest(Abc_Ntk_t *pNtk, int Num)
Definition: abcDar.c:4626
Gia_Man_t * Dar_NewChoiceSynthesis(Aig_Man_t *pAig, int fBalance, int fUpdateLevel, int fPower, int fLightSynth, int fVerbose)
Definition: darScript.c:632
static int Gia_ObjIsXor(Gia_Obj_t *pObj)
Definition: gia.h:423
Abc_Ntk_t * Abc_NtkAfterTrim(Aig_Man_t *pMan, Abc_Ntk_t *pNtkOld)
Definition: abcDar.c:1021
#define Gia_ManForEachAnd(p, pObj, i)
Definition: gia.h:1002
ABC_DLL void Abc_NtkAddDummyBoxNames(Abc_Ntk_t *pNtk)
Definition: abcNames.c:418
Abc_Ntk_t * Abc_NtkDarToCnf(Abc_Ntk_t *pNtk, char *pFileName, int fFastAlgo, int fChangePol, int fVerbose)
Definition: abcDar.c:1736
int nIters
Definition: gia.h:242
static Abc_Obj_t * Abc_NtkCreateLatch(Abc_Ntk_t *pNtk)
Definition: abc.h:309
Vec_Ptr_t * Aig_ManDfs(Aig_Man_t *p, int fNodesOnly)
Definition: aigDfs.c:145
STRUCTURE DEFINITIONS ///.
Definition: mioInt.h:61
static void Abc_NtkFromCellWrite(Vec_Int_t *vCopyLits, int i, int c, int Id)
Definition: abcDar.c:850
Definition: aig.h:69
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Abc_Ntk_t * Abc_NtkDarSeqSweep(Abc_Ntk_t *pNtk, Fra_Ssw_t *pPars)
Definition: abcDar.c:1971
ABC_DLL char * Abc_SopCreateMux(Mem_Flex_t *pMan)
Definition: abcSop.c:329
char * sprintf()
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:410
static int Counter
#define Saig_ManForEachLo(p, pObj, i)
Definition: saig.h:96
void Gia_ManFillValue(Gia_Man_t *p)
Definition: giaUtil.c:328
int nWordsFrame
Definition: fra.h:176
static Aig_Obj_t * Aig_ObjChild0Copy(Aig_Obj_t *pObj)
Definition: aig.h:312
#define Abc_NtkForEachLatch(pNtk, pObj, i)
Definition: abc.h:497
Abc_Cex_t * pSeqModel
Definition: abc.h:199
static int Abc_LatchIsInit1(Abc_Obj_t *pLatch)
Definition: abc.h:423
typedefABC_NAMESPACE_HEADER_START struct Cgt_Par_t_ Cgt_Par_t
INCLUDES ///.
Definition: cgt.h:48
static Abc_Obj_t * Abc_NtkCreatePi(Abc_Ntk_t *pNtk)
Definition: abc.h:303
void Aig_ManSetCioIds(Aig_Man_t *p)
Definition: aigUtil.c:965
static int Gia_ObjIsCellInv(Gia_Man_t *p, int iLit)
Definition: gia.h:961
static void Vec_IntFreeP(Vec_Int_t **p)
Definition: vecInt.h:289
Abc_Ntk_t * Abc_NtkDarLcorrNew(Abc_Ntk_t *pNtk, int nVarsMax, int nConfMax, int fVerbose)
Definition: abcDar.c:2200
Aig_Man_t * Cec_ComputeChoices(Gia_Man_t *pGia, Dch_Pars_t *pPars)
Definition: cecChoice.c:385
#define Gia_ManForEachPi(p, pObj, i)
Definition: gia.h:1034
int Abc_NtkDSat(Abc_Ntk_t *pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fAlignPol, int fAndOuts, int fNewSolver, int fVerbose)
Definition: abcDar.c:1804
Abc_Ntk_t * Abc_NtkDarClockGate(Abc_Ntk_t *pNtk, Abc_Ntk_t *pCare, Cgt_Par_t *pPars)
Definition: abcDar.c:4094
Fra_Sml_t * Fra_SmlSimulateCombGiven(Aig_Man_t *pAig, char *pFileName, int fCheckMiter, int fVerbose)
Definition: fraSim.c:981
Vec_Ptr_t * Abc_NtkCollectCoNames(Abc_Ntk_t *pNtk)
Definition: abcDar.c:1265
Aig_Man_t * Saig_SynchSequenceApply(Aig_Man_t *pAig, int nWords, int fVerbose)
Definition: saigSynch.c:502
static void Abc_Print(int level, const char *format,...)
Definition: abc_global.h:313
Abc_Ntk_t * Abc_NtkDarTempor(Abc_Ntk_t *pNtk, int nFrames, int TimeOut, int nConfLimit, int fUseBmc, int fUseTransSigs, int fVerbose, int fVeryVerbose)
Definition: abcDar.c:3653
ABC_NAMESPACE_HEADER_START Aig_Man_t * Csw_Sweep(Aig_Man_t *pAig, int nCutsMax, int nLeafMax, int fVerbose)
INCLUDES ///.
Definition: cswCore.c:45
void Ioa_WriteAiger(Aig_Man_t *pMan, char *pFileName, int fWriteSymbols, int fCompact)
Definition: ioaWriteAig.c:446
static int Vec_PtrCountZero(Vec_Ptr_t *p)
Definition: vecPtr.h:343
void Llb_ManMinCutTest(Aig_Man_t *pAig, int Num)
Definition: llb2Flow.c:1335
abctime timeSat
Definition: abcDar.c:3799
static int Aig_ObjFaninC0(Aig_Obj_t *pObj)
Definition: aig.h:306
void Aig_ManInterFast(Aig_Man_t *pManOn, Aig_Man_t *pManOff, int fVerbose)
FUNCTION DEFINITIONS ///.
Definition: aigInter.c:51
int Abc_NtkDarBmc(Abc_Ntk_t *pNtk, int nStart, int nFrames, int nSizeMax, int nNodeDelta, int nTimeOut, int nBTLimit, int nBTLimitAll, int fRewrite, int fNewAlgo, int fOrDecomp, int nCofFanLit, int fVerbose, int *piFrames)
Definition: abcDar.c:2255
static void Vec_PtrWriteEntry(Vec_Ptr_t *p, int i, void *Entry)
Definition: vecPtr.h:396
char * strcpy()
Vec_Int_t * Abc_NtkGetLatchValues(Abc_Ntk_t *pNtk)
Definition: abcDar.c:1287
static int Aig_ManObjNumMax(Aig_Man_t *p)
Definition: aig.h:259
int Aig_ManPartitionedSat(Aig_Man_t *p, int nAlgo, int nPartSize, int nConfPart, int nConfTotal, int fAlignPol, int fSynthesize, int fVerbose)
Definition: aigPartSat.c:491
#define Abc_NtkForEachNode(pNtk, pNode, i)
Definition: abc.h:461
static Abc_Obj_t * Abc_NtkBox(Abc_Ntk_t *pNtk, int i)
Definition: abc.h:319
static Gia_Obj_t * Gia_ObjFanin2(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:456
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
static int Gia_ObjIsTravIdCurrentId(Gia_Man_t *p, int Id)
Definition: gia.h:536
int fTryBmc
Definition: fra.h:117
Abc_Ntk_t * Abc_NtkFromCellMappedGia(Gia_Man_t *p)
Definition: abcDar.c:872
ABC_DLL Vec_Ptr_t * Abc_AigDfs(Abc_Ntk_t *pNtk, int fCollectAll, int fCollectCos)
Definition: abcDfs.c:1014
static int Abc_NtkConstrNum(Abc_Ntk_t *pNtk)
Definition: abc.h:299
static int Aig_ObjIsExor(Aig_Obj_t *pObj)
Definition: aig.h:279
int Fra_FraigSec(Aig_Man_t *p, Fra_Sec_t *pParSec, Aig_Man_t **ppResult)
Definition: fraSec.c:95
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
int Abc_NtkDarBmcInter(Abc_Ntk_t *pNtk, Inter_ManParams_t *pPars, Abc_Ntk_t **ppNtkRes)
Definition: abcDar.c:2552
Abc_Ntk_t * Abc_NtkDarFraig(Abc_Ntk_t *pNtk, int nConfLimit, int fDoSparse, int fProve, int fTransfer, int fSpeculate, int fChoicing, int fVerbose)
Definition: abcDar.c:1357
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
static Aig_Obj_t * Aig_ManCo(Aig_Man_t *p, int i)
Definition: aig.h:267
Aig_Man_t * Aig_ManDupUnsolvedOutputs(Aig_Man_t *p, int fAddRegs)
Definition: aigDup.c:1199
char * pSpec
Definition: abc.h:159
void Saig_ManDetectConstrFuncTest(Aig_Man_t *p, int nFrames, int nConfs, int nProps, int fOldAlgo, int fVerbose)
Definition: saigConstr2.c:856
ABC_DLL int Abc_NtkLogicMakeSimpleCos(Abc_Ntk_t *pNtk, int fDuplicate)
Definition: abcUtil.c:1047
int nPartSize
Definition: fra.h:94
void Saig_ManBmcSectionsTest(Aig_Man_t *p)
Definition: bmcBmc3.c:449
static int Abc_AigNodeIsChoice(Abc_Obj_t *pNode)
Definition: abc.h:398
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
static int Abc_LitNot(int Lit)
Definition: abc_global.h:266
int Pdr_ManSolve(Aig_Man_t *p, Pdr_Par_t *pPars)
Definition: pdrCore.c:886
static Abc_Obj_t * Abc_ObjEquiv(Abc_Obj_t *pObj)
Definition: abc.h:337
Aig_Man_t * Fra_FraigInduction(Aig_Man_t *p, Fra_Ssw_t *pPars)
Definition: fraInd.c:344
Aig_Man_t * Aig_ManInter(Aig_Man_t *pManOn, Aig_Man_t *pManOff, int fRelation, int fVerbose)
Definition: aigInter.c:149
static Abc_Obj_t * Abc_ObjRegular(Abc_Obj_t *p)
Definition: abc.h:323
Aig_Man_t * Saig_ManDecPropertyOutput(Aig_Man_t *pAig, int nLits, int fVerbose)
Definition: saigOutDec.c:150
Abc_Ntk_t * Abc_NtkFromDarSeqSweep(Abc_Ntk_t *pNtkOld, Aig_Man_t *pMan)
Definition: abcDar.c:468
void Abc_NtkPrintLatchEquivClasses(Abc_Ntk_t *pNtk, Aig_Man_t *pAig)
Definition: abcDar.c:2030
Aig_Obj_t * Saig_ManFindPivot(Aig_Man_t *p)
Definition: saigWnd.c:427
static int Abc_ObjIsBi(Abc_Obj_t *pObj)
Definition: abc.h:349
Abc_Ntk_t * Abc_NtkDarRetimeMostFwd(Abc_Ntk_t *pNtk, int nMaxIters, int fVerbose)
Definition: abcDar.c:3313
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
int fSilent
Definition: bmc.h:69
Definition: abc.h:89
void Dar_BalancePrintStats(Aig_Man_t *p)
Definition: darBalance.c:716
ABC_DLL int Abc_NtkMiterIsConstant(Abc_Ntk_t *pMiter)
Definition: abcMiter.c:679
short Type
Definition: amap.h:62
static int Gia_ManHasMapping(Gia_Man_t *p)
Definition: gia.h:951
void Abc_NtkDarConstr(Abc_Ntk_t *pNtk, int nFrames, int nConfs, int nProps, int fStruct, int fOldAlgo, int fVerbose)
Definition: abcDar.c:4460
static Abc_Obj_t * Abc_NtkPo(Abc_Ntk_t *pNtk, int i)
Definition: abc.h:316
#define Aig_ManForEachObj(p, pObj, i)
Definition: aig.h:403
#define Abc_NtkForEachCi(pNtk, pCi, i)
Definition: abc.h:515
int Ssw_ManSetConstrPhases(Aig_Man_t *p, int nFrames, Vec_Int_t **pvInits)
Definition: sswConstr.c:100
static int Abc_NtkPoNum(Abc_Ntk_t *pNtk)
Definition: abc.h:286
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
Abc_Ntk_t * Abc_NtkInter(Abc_Ntk_t *pNtkOn, Abc_Ntk_t *pNtkOff, int fRelation, int fVerbose)
Definition: abcDar.c:3813
Aig_Man_t * Saig_ManWindowExtract(Aig_Man_t *p, Aig_Obj_t *pObj, int nDist)
Definition: saigWnd.c:465
int fTryComb
Definition: fra.h:116
int Abc_NtkDarSeqSim(Abc_Ntk_t *pNtk, int nFrames, int nWords, int TimeOut, int fNew, int fMiter, int fVerbose, char *pFileSim)
Definition: abcDar.c:3444
int Ssw_SecSpecialMiter(Aig_Man_t *p0, Aig_Man_t *p1, int nFrames, int fVerbose)
Definition: saigMiter.c:1161
static int Saig_ManPiNum(Aig_Man_t *p)
MACRO DEFINITIONS ///.
Definition: saig.h:73
Aig_Man_t * Aig_ManDupOneOutput(Aig_Man_t *p, int iPoNum, int fAddRegs)
Definition: aigDup.c:1152
typedefABC_NAMESPACE_HEADER_START struct Fra_Par_t_ Fra_Par_t
INCLUDES ///.
Definition: fra.h:53
Abc_Ntk_t * Abc_NtkConstructFromCnf(Abc_Ntk_t *pNtk, Cnf_Man_t *p, Vec_Ptr_t *vMapped)
Definition: abcDar.c:1664
static Hop_Obj_t * Hop_NotCond(Hop_Obj_t *p, int c)
Definition: hop.h:128
ABC_DLL Abc_Ntk_t * Abc_NtkStartFromNoLatches(Abc_Ntk_t *pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func)
Definition: abcNtk.c:248
int nBarBufs
Definition: abc.h:174
Vec_Ptr_t * vOnehots
Definition: abc.h:211
Aig_Man_t * Gia_ManToAigSkip(Gia_Man_t *p, int nOutDelta)
Definition: giaAig.c:324
int Saig_ManInduction(Aig_Man_t *p, int nTimeOut, int nFramesMax, int nConfMax, int fUnique, int fUniqueAll, int fGetCex, int fVerbose, int fVeryVerbose)
Definition: saigInd.c:149
#define ABC_FREE(obj)
Definition: abc_global.h:232
ABC_DLL Abc_Obj_t * Abc_NtkCreateNodeConst0(Abc_Ntk_t *pNtk)
Definition: abcObj.c:604
int Aig_ManCiCleanup(Aig_Man_t *p)
Definition: aigMan.c:314
Definition: gia.h:95
static int Abc_NtkPiNum(Abc_Ntk_t *pNtk)
Definition: abc.h:285
ABC_DLL char * Abc_ObjName(Abc_Obj_t *pNode)
DECLARATIONS ///.
Definition: abcNames.c:48
#define ABC_PRT(a, t)
Definition: abc_global.h:220
void Aig_MmFlexStop(Aig_MmFlex_t *p, int fVerbose)
Definition: aigMem.c:337
static int Gia_ObjIsAnd(Gia_Obj_t *pObj)
Definition: gia.h:422
Abc_Ntk_t * Abc_NtkDarUnfold(Abc_Ntk_t *pNtk, int nFrames, int nConfs, int nProps, int fStruct, int fOldAlgo, int fVerbose)
Definition: abcDar.c:4515
typedefABC_NAMESPACE_HEADER_START struct Dar_RwrPar_t_ Dar_RwrPar_t
INCLUDES ///.
Definition: dar.h:42
int fReportSolution
Definition: fra.h:146
#define Abc_NtkForEachLatchInput(pNtk, pObj, i)
Definition: abc.h:500
static Gia_Obj_t * Gia_ManConst0(Gia_Man_t *p)
Definition: gia.h:400
void Aig_ManComputeSccs(Aig_Man_t *p)
Definition: aigScl.c:489
static Abc_Obj_t * Abc_NtkCreateNode(Abc_Ntk_t *pNtk)
Definition: abc.h:308
int Abc_NtkDarCec(Abc_Ntk_t *pNtk1, Abc_Ntk_t *pNtk2, int nConfLimit, int fPartition, int fVerbose)
Definition: abcDar.c:1854
Aig_Man_t * Aig_ManFraigPartitioned(Aig_Man_t *pAig, int nPartSize, int nConfMax, int nLevelMax, int fVerbose)
Definition: aigPart.c:1379
int Abc_NtkDarBmc3(Abc_Ntk_t *pNtk, Saig_ParBmc_t *pPars, int fOrDecomp)
Definition: abcDar.c:2337
void Gia_ManSimSetDefaultParams(Gia_ParSim_t *p)
Definition: giaSim.c:164
static int Abc_Lit2Var(int Lit)
Definition: abc_global.h:264
Aig_Man_t * Fra_FraigPerform(Aig_Man_t *pManAig, Fra_Par_t *pPars)
Definition: fraCore.c:375
static int Gia_ObjFaninId0p(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:463
Definition: abc.h:90
Abc_Ntk_t * Abc_NtkDRewrite(Abc_Ntk_t *pNtk, Dar_RwrPar_t *pPars)
Definition: abcDar.c:1444
void Cnf_DataFree(Cnf_Dat_t *p)
Definition: cnfMan.c:180
static void Abc_ObjXorFaninC(Abc_Obj_t *pObj, int i)
Definition: abc.h:381
static Gia_Obj_t * Gia_ObjFanin1(Gia_Obj_t *pObj)
Definition: gia.h:455
Mio_Cell_t * Mio_CollectRootsNewDefault(int nInputs, int *pnGates, int fVerbose)
Definition: mioUtils.c:498
int Fra_FraigCec(Aig_Man_t **ppAig, int nConfLimit, int fVerbose)
Definition: fraCec.c:320
static int Abc_ObjIsPo(Abc_Obj_t *pObj)
Definition: abc.h:348
#define Gia_ManForEachBuf(p, pObj, i)
Definition: gia.h:998
int Abc_NtkDarClau(Abc_Ntk_t *pNtk, int nFrames, int nPref, int nClauses, int nLutSize, int nLevels, int nCutsMax, int nBatches, int fStepUp, int fBmc, int fRefs, int fTarget, int fVerbose, int fVeryVerbose)
Definition: abcDar.c:3593
Definition: abc.h:92
Abc_Ntk_t * Abc_NtkDChoice(Abc_Ntk_t *pNtk, int fBalance, int fUpdateLevel, int fConstruct, int nConfMax, int nLevelMax, int fVerbose)
Definition: abcDar.c:1558
#define Saig_ManForEachPo(p, pObj, i)
Definition: saig.h:93
Aig_Man_t * Abc_NtkToDarBmc(Abc_Ntk_t *pNtk, Vec_Int_t **pvMap)
Definition: abcDar.c:111
static Abc_Obj_t * Abc_ObjNotCond(Abc_Obj_t *p, int c)
Definition: abc.h:325
Abc_Ntk_t * Abc_NtkFromDarSeq(Abc_Ntk_t *pNtkOld, Aig_Man_t *pMan)
Definition: abcDar.c:1169
void Saig_ManBmcMappingTest(Aig_Man_t *p)
Definition: bmcBmc3.c:666
#define assert(ex)
Definition: util_old.h:213
static void Vec_PtrClear(Vec_Ptr_t *p)
Definition: vecPtr.h:545
Aig_Man_t * Cgt_ClockGating(Aig_Man_t *pAig, Aig_Man_t *pCare, Cgt_Par_t *pPars)
Definition: cgtCore.c:298
int strlen()
#define Aig_ManForEachLiSeq(p, pObj, i)
Definition: aig.h:447
Abc_Ntk_t * Abc_NtkDC2(Abc_Ntk_t *pNtk, int fBalance, int fUpdateLevel, int fFanout, int fPower, int fVerbose)
Definition: abcDar.c:1525
unsigned Value
Definition: gia.h:87
ABC_DLL char * Abc_FrameReadFlag(char *pFlag)
Definition: mainFrame.c:64
static Abc_Obj_t * Abc_ObjNot(Abc_Obj_t *p)
Definition: abc.h:324
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition: utilCex.h:39
int Abc_NtkDarAbSec(Abc_Ntk_t *pNtk1, Abc_Ntk_t *pNtk2, int nFrames, int fVerbose)
Definition: abcDar.c:3043
static int Gia_ObjIsLut(Gia_Man_t *p, int Id)
Definition: gia.h:952
Aig_Man_t * Dch_ComputeChoices(Aig_Man_t *pAig, Dch_Pars_t *pPars)
Definition: dchCore.c:89
void Gia_ManIncrementTravId(Gia_Man_t *p)
Definition: giaUtil.c:149
static Abc_Obj_t * Abc_NtkPi(Abc_Ntk_t *pNtk, int i)
Definition: abc.h:315
static int Gia_ManHasCellMapping(Gia_Man_t *p)
Definition: gia.h:959
void * pData
Definition: abc.h:145
#define Gia_ManForEachCell(p, i)
Definition: gia.h:975
Aig_Man_t * Dar_ManBalance(Aig_Man_t *p, int fUpdateLevel)
Definition: darBalance.c:554
#define Abc_NtkForEachPo(pNtk, pPo, i)
Definition: abc.h:517
static Abc_Obj_t * Abc_NtkCreateBi(Abc_Ntk_t *pNtk)
Definition: abc.h:305
static int Gia_ObjFaninC0(Gia_Obj_t *pObj)
Definition: gia.h:451
char nFanins
Definition: cnf.h:73
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
int Abc_NtkPhaseFrameNum(Abc_Ntk_t *pNtk)
Definition: abcDar.c:4002
typedefABC_NAMESPACE_HEADER_START struct Cnf_Man_t_ Cnf_Man_t
INCLUDES ///.
Definition: cnf.h:51
static int Gia_ManPiNum(Gia_Man_t *p)
Definition: gia.h:385
Abc_Ntk_t * Abc_NtkDarCleanupAig(Abc_Ntk_t *pNtk, int fCleanupPis, int fCleanupPos, int fVerbose)
Definition: abcDar.c:4284
int fVerbose
Definition: fra.h:107
#define Aig_ManForEachPoSeq(p, pObj, i)
Definition: aig.h:444
static int Abc_ObjIsComplement(Abc_Obj_t *p)
Definition: abc.h:322
ABC_INT64_T abctime
Definition: abc_global.h:278
Aig_Man_t * Saig_ManDupUnfoldConstrsFunc(Aig_Man_t *pAig, int nFrames, int nConfs, int nProps, int fOldAlgo, int fVerbose)
Definition: saigConstr2.c:877
static void Gia_ObjSetTravIdCurrentId(Gia_Man_t *p, int Id)
Definition: gia.h:535
static int Abc_NtkObjNum(Abc_Ntk_t *pNtk)
Definition: abc.h:283
Abc_Cex_t * Abc_CexCreate(int nRegs, int nPis, int *pArray, int iFrame, int iPo, int fSkipRegs)
Definition: utilCex.c:110
ABC_DLL void Abc_NtkAddDummyPiNames(Abc_Ntk_t *pNtk)
Definition: abcNames.c:378
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
#define Gia_ManForEachPo(p, pObj, i)
Definition: gia.h:1036
Aig_Man_t * Saig_ManTimeframeSimplify(Aig_Man_t *pAig, int nFrames, int nFramesMax, int fInit, int fVerbose)
Definition: saigTrans.c:378
static int Gia_ObjFaninId1(Gia_Obj_t *pObj, int ObjId)
Definition: gia.h:461
#define Gia_CellForEachFanin(p, i, iFanLit, k)
Definition: gia.h:977
ABC_DLL void Abc_NtkOrderCisCos(Abc_Ntk_t *pNtk)
Definition: abcUtil.c:71
Aig_Obj_t * pFanin0
Definition: aig.h:75
void Aig_ManCleanData(Aig_Man_t *p)
Definition: aigUtil.c:205
static void Abc_LatchSetInit0(Abc_Obj_t *pLatch)
Definition: abc.h:418
static Abc_Obj_t * Abc_NtkCreatePo(Abc_Ntk_t *pNtk)
Definition: abc.h:304
int nLiterals
Definition: cnf.h:60
static Abc_Obj_t * Abc_ObjChild1(Abc_Obj_t *pObj)
Definition: abc.h:384
int Id
Definition: aig.h:85
void Abc_NtkVerifyReportErrorSeq(Abc_Ntk_t *pNtk1, Abc_Ntk_t *pNtk2, int *pModel, int nFrames)
Definition: abcVerify.c:853
int Ssw_SecGeneralMiter(Aig_Man_t *pMiter, Ssw_Pars_t *pPars)
Definition: sswPairs.c:452
int Aig_ManCleanup(Aig_Man_t *p)
Definition: aigMan.c:265
typedefABC_NAMESPACE_HEADER_START struct Hop_Man_t_ Hop_Man_t
INCLUDES ///.
Definition: hop.h:49
#define Gia_LutForEachFanin(p, i, iFan, k)
Definition: gia.h:970
ABC_DLL int Abc_NtkAppend(Abc_Ntk_t *pNtk1, Abc_Ntk_t *pNtk2, int fAddPos)
Definition: abcStrash.c:320
char * pName
Definition: abc.h:158
Hop_Obj_t * Hop_IthVar(Hop_Man_t *p, int i)
FUNCTION DEFINITIONS ///.
Definition: hopOper.c:63
Aig_Man_t * Saig_ManWindowInsert(Aig_Man_t *p, Aig_Obj_t *pObj, int nDist, Aig_Man_t *pWnd)
Definition: saigWnd.c:488
Abc_Ntk_t * Abc_NtkDarSeqSweep2(Abc_Ntk_t *pNtk, Ssw_Pars_t *pPars)
Definition: abcDar.c:2120
Aig_Man_t * Rtm_ManRetime(Aig_Man_t *p, int fForward, int nStepsMax, int fVerbose)
Definition: aigRet.c:834
Abc_Ntk_t * Abc_NtkDRefactor(Abc_Ntk_t *pNtk, Dar_RefPar_t *pPars)
Definition: abcDar.c:1488
Abc_Ntk_t * Abc_NtkFromAigPhase(Aig_Man_t *pMan)
Definition: abcDar.c:590
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
static Abc_Obj_t * Abc_ObjFanout0(Abc_Obj_t *pObj)
Definition: abc.h:371
int Fra_FraigSat(Aig_Man_t *pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fFlipBits, int fAndOuts, int fNewSolver, int fVerbose)
ITERATORS ///.
Definition: fraCec.c:47
#define Aig_ManForEachPiSeq(p, pObj, i)
SEQUENTIAL ITERATORS ///.
Definition: aig.h:438
Abc_Ntk_t * Abc_NtkPhaseAbstract(Abc_Ntk_t *pNtk, int nFrames, int nPref, int fIgnore, int fPrint, int fVerbose)
Definition: abcDar.c:3969
int nConstrs
Definition: abc.h:173
static int Aig_ObjCioId(Aig_Obj_t *pObj)
Definition: aig.h:285
int fSolveAll
Definition: bmc.h:57
#define Abc_NtkForEachPi(pNtk, pPi, i)
Definition: abc.h:513
int Ssw_RarSimulate(Aig_Man_t *pAig, Ssw_RarPars_t *pPars)
Definition: sswRarity.c:973
Aig_Man_t * Abc_NtkToDar(Abc_Ntk_t *pNtk, int fExors, int fRegisters)
DECLARATIONS ///.
Definition: abcDar.c:233
typedefABC_NAMESPACE_HEADER_START struct Inter_ManParams_t_ Inter_ManParams_t
INCLUDES ///.
Definition: int.h:48
void Saig_ManBmcSupergateTest(Aig_Man_t *p)
Definition: bmcBmc3.c:555
void Fra_SmlStop(Fra_Sml_t *p)
Definition: fraSim.c:839
int Aig_ManVerifyUsingBdds(Aig_Man_t *p, Saig_ParBbr_t *pPars)
Definition: bbrReach.c:544
int Fra_Claus(Aig_Man_t *pAig, int nFrames, int nPref, int nClausesMax, int nLutSize, int nLevels, int nCutsMax, int nBatches, int fStepUp, int fBmc, int fRefs, int fTarget, int fVerbose, int fVeryVerbose)
Definition: fraClaus.c:1682
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
int Ssw_ManProfileConstraints(Aig_Man_t *p, int nWords, int nFrames, int fVerbose)
FUNCTION DEFINITIONS ///.
Definition: saigConstr2.c:56
static int Gia_ObjFaninId0(Gia_Obj_t *pObj, int ObjId)
Definition: gia.h:460
Abc_Ntk_t * Abc_NtkDarLcorr(Abc_Ntk_t *pNtk, int nFramesP, int nConfMax, int fVerbose)
Definition: abcDar.c:2163
void Saig_ManBmcTerSimTest(Aig_Man_t *p)
Definition: bmcBmc3.c:238
Abc_Cex_t * pCexSeq
Definition: gia.h:136
static int Gia_ManRegNum(Gia_Man_t *p)
Definition: gia.h:387
int TimeLimit
Definition: gia.h:244