abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
abcQuant.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [abcQuant.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Network and node package.]
8 
9  Synopsis [AIG-based variable quantification.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: abcQuant.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "base/abc/abc.h"
22 
24 
25 
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29 
30 ////////////////////////////////////////////////////////////////////////
31 /// FUNCTION DEFINITIONS ///
32 ////////////////////////////////////////////////////////////////////////
33 
34 /**Function*************************************************************
35 
36  Synopsis [Performs fast synthesis.]
37 
38  Description []
39 
40  SideEffects []
41 
42  SeeAlso []
43 
44 ***********************************************************************/
45 void Abc_NtkSynthesize( Abc_Ntk_t ** ppNtk, int fMoreEffort )
46 {
47  extern Abc_Ntk_t * Abc_NtkIvyFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, int fProve, int fTransfer, int fVerbose );
48 
49  Abc_Ntk_t * pNtk, * pNtkTemp;
50 
51  pNtk = *ppNtk;
52 
53  Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0 );
54  Abc_NtkRefactor( pNtk, 10, 16, 0, 0, 0, 0 );
55  pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 );
56  Abc_NtkDelete( pNtkTemp );
57 
58  if ( fMoreEffort )
59  {
60  Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0 );
61  Abc_NtkRefactor( pNtk, 10, 16, 0, 0, 0, 0 );
62  pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 );
63  Abc_NtkDelete( pNtkTemp );
64 
65  pNtk = Abc_NtkIvyFraig( pNtkTemp = pNtk, 100, 1, 0, 0, 0 );
66  Abc_NtkDelete( pNtkTemp );
67  }
68 
69  *ppNtk = pNtk;
70 }
71 
72 /**Function*************************************************************
73 
74  Synopsis [Existentially quantifies one variable.]
75 
76  Description []
77 
78  SideEffects [This procedure creates dangling nodes in the AIG.]
79 
80  SeeAlso []
81 
82 ***********************************************************************/
83 int Abc_NtkQuantify( Abc_Ntk_t * pNtk, int fUniv, int iVar, int fVerbose )
84 {
85  Vec_Ptr_t * vNodes;
86  Abc_Obj_t * pObj, * pNext, * pFanin;
87  int i;
88  assert( Abc_NtkIsStrash(pNtk) );
89  assert( iVar < Abc_NtkCiNum(pNtk) );
90 
91  // collect the internal nodes
92  pObj = Abc_NtkCi( pNtk, iVar );
93  vNodes = Abc_NtkDfsReverseNodes( pNtk, &pObj, 1 );
94 
95  // assign the cofactors of the CI node to be constants
96  pObj->pCopy = Abc_ObjNot( Abc_AigConst1(pNtk) );
97  pObj->pData = Abc_AigConst1(pNtk);
98 
99  // quantify the nodes
100  Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
101  {
102  for ( pNext = pObj? pObj->pCopy : pObj; pObj; pObj = pNext, pNext = pObj? pObj->pCopy : pObj )
103  {
104  pFanin = Abc_ObjFanin0(pObj);
105  if ( !Abc_NodeIsTravIdCurrent(pFanin) )
106  {
107  pFanin->pCopy = pFanin;
108  pFanin->pData = pFanin;
109  }
110  pFanin = Abc_ObjFanin1(pObj);
111  if ( !Abc_NodeIsTravIdCurrent(pFanin) )
112  {
113  pFanin->pCopy = pFanin;
114  pFanin->pData = pFanin;
115  }
116  pObj->pCopy = Abc_AigAnd( (Abc_Aig_t *)pNtk->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) );
117  pObj->pData = Abc_AigAnd( (Abc_Aig_t *)pNtk->pManFunc, Abc_ObjChild0Data(pObj), Abc_ObjChild1Data(pObj) );
118  }
119  }
120  Vec_PtrFree( vNodes );
121 
122  // update the affected COs
123  Abc_NtkForEachCo( pNtk, pObj, i )
124  {
125  if ( !Abc_NodeIsTravIdCurrent(pObj) )
126  continue;
127  pFanin = Abc_ObjFanin0(pObj);
128  // get the result of quantification
129  if ( fUniv )
130  pNext = Abc_AigAnd( (Abc_Aig_t *)pNtk->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild0Data(pObj) );
131  else
132  pNext = Abc_AigOr( (Abc_Aig_t *)pNtk->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild0Data(pObj) );
133  pNext = Abc_ObjNotCond( pNext, Abc_ObjFaninC0(pObj) );
134  if ( Abc_ObjRegular(pNext) == pFanin )
135  continue;
136  // update the fanins of the CO
137  Abc_ObjPatchFanin( pObj, pFanin, pNext );
138 // if ( Abc_ObjFanoutNum(pFanin) == 0 )
139 // Abc_AigDeleteNode( pNtk->pManFunc, pFanin );
140  }
141 
142  // make sure the node has no fanouts
143 // pObj = Abc_NtkCi( pNtk, iVar );
144 // assert( Abc_ObjFanoutNum(pObj) == 0 );
145  return 1;
146 }
147 
148 /**Function*************************************************************
149 
150  Synopsis [Constructs the transition relation.]
151 
152  Description []
153 
154  SideEffects []
155 
156  SeeAlso []
157 
158 ***********************************************************************/
159 Abc_Ntk_t * Abc_NtkTransRel( Abc_Ntk_t * pNtk, int fInputs, int fVerbose )
160 {
161  char Buffer[1000];
162  Vec_Ptr_t * vPairs;
163  Abc_Ntk_t * pNtkNew;
164  Abc_Obj_t * pObj, * pMiter;
165  int i, nLatches;
166  int fSynthesis = 1;
167 
168  assert( Abc_NtkIsStrash(pNtk) );
169  assert( Abc_NtkLatchNum(pNtk) );
170  nLatches = Abc_NtkLatchNum(pNtk);
171  // start the network
172  pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
173  // duplicate the name and the spec
174  sprintf( Buffer, "%s_TR", pNtk->pName );
175  pNtkNew->pName = Extra_UtilStrsav(pNtk->pName);
176 // pNtkNew->pSpec = Extra_UtilStrsav(pNtk->pSpec);
177  Abc_NtkCleanCopy( pNtk );
178  // create current state variables
179  Abc_NtkForEachLatchOutput( pNtk, pObj, i )
180  {
181  pObj->pCopy = Abc_NtkCreatePi(pNtkNew);
182  Abc_ObjAssignName( pObj->pCopy, Abc_ObjName(pObj), NULL );
183  }
184  // create next state variables
185  Abc_NtkForEachLatchInput( pNtk, pObj, i )
186  Abc_ObjAssignName( Abc_NtkCreatePi(pNtkNew), Abc_ObjName(pObj), NULL );
187  // create PI variables
188  Abc_NtkForEachPi( pNtk, pObj, i )
189  Abc_NtkDupObj( pNtkNew, pObj, 1 );
190  // create the PO
191  Abc_NtkCreatePo( pNtkNew );
192  // restrash the nodes (assuming a topological order of the old network)
193  Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(pNtkNew);
194  Abc_NtkForEachNode( pNtk, pObj, i )
195  pObj->pCopy = Abc_AigAnd( (Abc_Aig_t *)pNtkNew->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) );
196  // create the function of the primary output
197  assert( Abc_NtkBoxNum(pNtk) == Abc_NtkLatchNum(pNtk) );
198  vPairs = Vec_PtrAlloc( 2*nLatches );
199  Abc_NtkForEachLatchInput( pNtk, pObj, i )
200  {
201  Vec_PtrPush( vPairs, Abc_ObjChild0Copy(pObj) );
202  Vec_PtrPush( vPairs, Abc_NtkPi(pNtkNew, i+nLatches) );
203  }
204  pMiter = Abc_AigMiter( (Abc_Aig_t *)pNtkNew->pManFunc, vPairs, 0 );
205  Vec_PtrFree( vPairs );
206  // add the primary output
207  Abc_ObjAddFanin( Abc_NtkPo(pNtkNew,0), Abc_ObjNot(pMiter) );
208  Abc_ObjAssignName( Abc_NtkPo(pNtkNew,0), "rel", NULL );
209 
210  // quantify inputs
211  if ( fInputs )
212  {
213  assert( Abc_NtkPiNum(pNtkNew) == Abc_NtkPiNum(pNtk) + 2*nLatches );
214  for ( i = Abc_NtkPiNum(pNtkNew) - 1; i >= 2*nLatches; i-- )
215 // for ( i = 2*nLatches; i < Abc_NtkPiNum(pNtkNew); i++ )
216  {
217  Abc_NtkQuantify( pNtkNew, 0, i, fVerbose );
218 // if ( fSynthesis && (i % 3 == 2) )
219  if ( fSynthesis )
220  {
221  Abc_NtkCleanData( pNtkNew );
222  Abc_AigCleanup( (Abc_Aig_t *)pNtkNew->pManFunc );
223  Abc_NtkSynthesize( &pNtkNew, 1 );
224  }
225 // printf( "Var = %3d. Nodes = %6d. ", Abc_NtkPiNum(pNtkNew) - 1 - i, Abc_NtkNodeNum(pNtkNew) );
226 // printf( "Var = %3d. Nodes = %6d. ", i - 2*nLatches, Abc_NtkNodeNum(pNtkNew) );
227  }
228 // printf( "\n" );
229  Abc_NtkCleanData( pNtkNew );
230  Abc_AigCleanup( (Abc_Aig_t *)pNtkNew->pManFunc );
231  for ( i = Abc_NtkPiNum(pNtkNew) - 1; i >= 2*nLatches; i-- )
232  {
233  pObj = Abc_NtkPi( pNtkNew, i );
234  assert( Abc_ObjFanoutNum(pObj) == 0 );
235  Abc_NtkDeleteObj( pObj );
236  }
237  }
238 
239  // check consistency of the network
240  if ( !Abc_NtkCheck( pNtkNew ) )
241  {
242  printf( "Abc_NtkTransRel: The network check has failed.\n" );
243  Abc_NtkDelete( pNtkNew );
244  return NULL;
245  }
246  return pNtkNew;
247 }
248 
249 
250 /**Function*************************************************************
251 
252  Synopsis [Performs one image computation.]
253 
254  Description []
255 
256  SideEffects []
257 
258  SeeAlso []
259 
260 ***********************************************************************/
262 {
263  Abc_Ntk_t * pNtkNew;
264  Abc_Obj_t * pMiter;
265  int i, nVars = Abc_NtkPiNum(pNtk)/2;
266  assert( Abc_NtkIsStrash(pNtk) );
267  // start the new network
268  pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG );
269  // compute the all-zero state in terms of the CS variables
270  pMiter = Abc_AigConst1(pNtkNew);
271  for ( i = 0; i < nVars; i++ )
272  pMiter = Abc_AigAnd( (Abc_Aig_t *)pNtkNew->pManFunc, pMiter, Abc_ObjNot( Abc_NtkPi(pNtkNew, i) ) );
273  // add the PO
274  Abc_ObjAddFanin( Abc_NtkPo(pNtkNew,0), pMiter );
275  return pNtkNew;
276 }
277 
278 /**Function*************************************************************
279 
280  Synopsis [Swaps current state and next state variables.]
281 
282  Description []
283 
284  SideEffects []
285 
286  SeeAlso []
287 
288 ***********************************************************************/
290 {
291  Abc_Ntk_t * pNtkNew;
292  Abc_Obj_t * pMiter, * pObj, * pObj0, * pObj1;
293  int i, nVars = Abc_NtkPiNum(pNtk)/2;
294  assert( Abc_NtkIsStrash(pNtk) );
295  // start the new network
296  pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG );
297  // update the PIs
298  for ( i = 0; i < nVars; i++ )
299  {
300  pObj0 = Abc_NtkPi( pNtk, i );
301  pObj1 = Abc_NtkPi( pNtk, i+nVars );
302  pMiter = pObj0->pCopy;
303  pObj0->pCopy = pObj1->pCopy;
304  pObj1->pCopy = pMiter;
305  }
306  // restrash
307  Abc_NtkForEachNode( pNtk, pObj, i )
308  pObj->pCopy = Abc_AigAnd( (Abc_Aig_t *)pNtkNew->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) );
309  // add the PO
310  pMiter = Abc_ObjChild0Copy( Abc_NtkPo(pNtk,0) );
311  Abc_ObjAddFanin( Abc_NtkPo(pNtkNew,0), pMiter );
312  return pNtkNew;
313 }
314 
315 /**Function*************************************************************
316 
317  Synopsis [Performs reachability analisys.]
318 
319  Description [Assumes that the input is the transition relation.]
320 
321  SideEffects []
322 
323  SeeAlso []
324 
325 ***********************************************************************/
326 Abc_Ntk_t * Abc_NtkReachability( Abc_Ntk_t * pNtkRel, int nIters, int fVerbose )
327 {
328  Abc_Obj_t * pObj;
329  Abc_Ntk_t * pNtkFront, * pNtkReached, * pNtkNext, * pNtkTemp;
330  int i, v, nVars, nNodesOld, nNodesNew, nNodesPrev;
331  int fFixedPoint = 0;
332  int fSynthesis = 1;
333  int fMoreEffort = 1;
334  abctime clk;
335 
336  assert( Abc_NtkIsStrash(pNtkRel) );
337  assert( Abc_NtkLatchNum(pNtkRel) == 0 );
338  assert( Abc_NtkPiNum(pNtkRel) % 2 == 0 );
339 
340  // compute the network composed of the initial states
341  pNtkFront = Abc_NtkInitialState( pNtkRel );
342  pNtkReached = Abc_NtkDup( pNtkFront );
343 //Abc_NtkShow( pNtkReached, 0, 0, 0 );
344 
345 // if ( fVerbose )
346 // printf( "Transition relation = %6d.\n", Abc_NtkNodeNum(pNtkRel) );
347 
348  // perform iterations of reachability analysis
349  nNodesPrev = Abc_NtkNodeNum(pNtkFront);
350  nVars = Abc_NtkPiNum(pNtkRel)/2;
351  for ( i = 0; i < nIters; i++ )
352  {
353  clk = Abc_Clock();
354  // get the set of next states
355  pNtkNext = Abc_NtkMiterAnd( pNtkRel, pNtkFront, 0, 0 );
356  Abc_NtkDelete( pNtkFront );
357  // quantify the current state variables
358  for ( v = 0; v < nVars; v++ )
359  {
360  Abc_NtkQuantify( pNtkNext, 0, v, fVerbose );
361  if ( fSynthesis && (v % 3 == 2) )
362  {
363  Abc_NtkCleanData( pNtkNext );
364  Abc_AigCleanup( (Abc_Aig_t *)pNtkNext->pManFunc );
365  Abc_NtkSynthesize( &pNtkNext, fMoreEffort );
366  }
367  }
368  Abc_NtkCleanData( pNtkNext );
369  Abc_AigCleanup( (Abc_Aig_t *)pNtkNext->pManFunc );
370  if ( fSynthesis )
371  Abc_NtkSynthesize( &pNtkNext, 1 );
372  // map the next states into the current states
373  pNtkNext = Abc_NtkSwapVariables( pNtkTemp = pNtkNext );
374  Abc_NtkDelete( pNtkTemp );
375  // check the termination condition
376  if ( Abc_ObjFanin0(Abc_NtkPo(pNtkNext,0)) == Abc_AigConst1(pNtkNext) )
377  {
378  fFixedPoint = 1;
379  printf( "Fixed point is reached!\n" );
380  Abc_NtkDelete( pNtkNext );
381  break;
382  }
383  // compute new front
384  pNtkFront = Abc_NtkMiterAnd( pNtkNext, pNtkReached, 0, 1 );
385  Abc_NtkDelete( pNtkNext );
386  // add the reached states
387  pNtkReached = Abc_NtkMiterAnd( pNtkTemp = pNtkReached, pNtkFront, 1, 0 );
388  Abc_NtkDelete( pNtkTemp );
389  // compress the size of Front
390  nNodesOld = Abc_NtkNodeNum(pNtkFront);
391  if ( fSynthesis )
392  {
393  Abc_NtkSynthesize( &pNtkFront, fMoreEffort );
394  Abc_NtkSynthesize( &pNtkReached, fMoreEffort );
395  }
396  nNodesNew = Abc_NtkNodeNum(pNtkFront);
397  // print statistics
398  if ( fVerbose )
399  {
400  printf( "I = %3d : Reach = %6d Fr = %6d FrM = %6d %7.2f %% ",
401  i + 1, Abc_NtkNodeNum(pNtkReached), nNodesOld, nNodesNew, 100.0*(nNodesNew-nNodesPrev)/nNodesPrev );
402  ABC_PRT( "T", Abc_Clock() - clk );
403  }
404  nNodesPrev = Abc_NtkNodeNum(pNtkFront);
405  }
406  if ( !fFixedPoint )
407  fprintf( stdout, "Reachability analysis stopped after %d iterations.\n", nIters );
408 
409  // complement the output to represent the set of unreachable states
410  Abc_ObjXorFaninC( Abc_NtkPo(pNtkReached,0), 0 );
411 
412  // remove next state variables
413  for ( i = 2*nVars - 1; i >= nVars; i-- )
414  {
415  pObj = Abc_NtkPi( pNtkReached, i );
416  assert( Abc_ObjFanoutNum(pObj) == 0 );
417  Abc_NtkDeleteObj( pObj );
418  }
419 
420  // check consistency of the network
421  if ( !Abc_NtkCheck( pNtkReached ) )
422  {
423  printf( "Abc_NtkReachability: The network check has failed.\n" );
424  Abc_NtkDelete( pNtkReached );
425  return NULL;
426  }
427  return pNtkReached;
428 }
429 
430 ////////////////////////////////////////////////////////////////////////
431 /// END OF FILE ///
432 ////////////////////////////////////////////////////////////////////////
433 
434 
436 
static int Abc_NtkIsStrash(Abc_Ntk_t *pNtk)
Definition: abc.h:251
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
static Abc_Obj_t * Abc_ObjFanin1(Abc_Obj_t *pObj)
Definition: abc.h:374
ABC_DLL Abc_Obj_t * Abc_AigOr(Abc_Aig_t *pMan, Abc_Obj_t *p0, Abc_Obj_t *p1)
Definition: abcAig.c:719
ABC_DLL Abc_Obj_t * Abc_AigConst1(Abc_Ntk_t *pNtk)
Definition: abcAig.c:683
Abc_Ntk_t * Abc_NtkReachability(Abc_Ntk_t *pNtkRel, int nIters, int fVerbose)
Definition: abcQuant.c:326
static int Abc_ObjFanoutNum(Abc_Obj_t *pObj)
Definition: abc.h:365
static int Abc_NtkBoxNum(Abc_Ntk_t *pNtk)
Definition: abc.h:289
#define Abc_NtkForEachLatchOutput(pNtk, pObj, i)
Definition: abc.h:503
static Abc_Obj_t * Abc_ObjChild1Copy(Abc_Obj_t *pObj)
Definition: abc.h:387
ABC_DLL Abc_Obj_t * Abc_NtkDupObj(Abc_Ntk_t *pNtkNew, Abc_Obj_t *pObj, int fCopyName)
Definition: abcObj.c:337
static int Abc_NtkLatchNum(Abc_Ntk_t *pNtk)
Definition: abc.h:294
static int Abc_ObjFaninC0(Abc_Obj_t *pObj)
Definition: abc.h:377
ABC_DLL Abc_Ntk_t * Abc_NtkDup(Abc_Ntk_t *pNtk)
Definition: abcNtk.c:419
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
static int Abc_NtkCiNum(Abc_Ntk_t *pNtk)
Definition: abc.h:287
#define Abc_NtkForEachCo(pNtk, pCo, i)
Definition: abc.h:519
static Abc_Obj_t * Abc_NtkCi(Abc_Ntk_t *pNtk, int i)
Definition: abc.h:317
ABC_DLL int Abc_NtkCheck(Abc_Ntk_t *pNtk)
FUNCTION DEFINITIONS ///.
Definition: abcCheck.c:61
ABC_DLL char * Abc_ObjAssignName(Abc_Obj_t *pObj, char *pName, char *pSuffix)
Definition: abcNames.c:68
static abctime Abc_Clock()
Definition: abc_global.h:279
ABC_NAMESPACE_IMPL_START void Abc_NtkSynthesize(Abc_Ntk_t **ppNtk, int fMoreEffort)
DECLARATIONS ///.
Definition: abcQuant.c:45
static Abc_Obj_t * Abc_ObjFanin0(Abc_Obj_t *pObj)
Definition: abc.h:373
DECLARATIONS ///.
Definition: abcAig.c:52
ABC_DLL void Abc_NtkDelete(Abc_Ntk_t *pNtk)
Definition: abcNtk.c:1233
char * Extra_UtilStrsav(const char *s)
static Abc_Obj_t * Abc_ObjChild1Data(Abc_Obj_t *pObj)
Definition: abc.h:389
ABC_DLL void Abc_ObjAddFanin(Abc_Obj_t *pObj, Abc_Obj_t *pFanin)
Definition: abcFanio.c:84
ABC_DLL Abc_Ntk_t * Abc_NtkAlloc(Abc_NtkType_t Type, Abc_NtkFunc_t Func, int fUseMemMan)
DECLARATIONS ///.
Definition: abcNtk.c:50
ABC_DLL void Abc_ObjPatchFanin(Abc_Obj_t *pObj, Abc_Obj_t *pFaninOld, Abc_Obj_t *pFaninNew)
Definition: abcFanio.c:172
void * pManFunc
Definition: abc.h:191
Abc_Ntk_t * Abc_NtkIvyFraig(Abc_Ntk_t *pNtk, int nConfLimit, int fDoSparse, int fProve, int fTransfer, int fVerbose)
Definition: abcIvy.c:456
static int Abc_NtkNodeNum(Abc_Ntk_t *pNtk)
Definition: abc.h:293
ABC_DLL Abc_Obj_t * Abc_AigAnd(Abc_Aig_t *pMan, Abc_Obj_t *p0, Abc_Obj_t *p1)
Definition: abcAig.c:700
Abc_Ntk_t * Abc_NtkSwapVariables(Abc_Ntk_t *pNtk)
Definition: abcQuant.c:289
static Abc_Obj_t * Abc_ObjChild0Copy(Abc_Obj_t *pObj)
Definition: abc.h:386
ABC_DLL Abc_Ntk_t * Abc_NtkStartFrom(Abc_Ntk_t *pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func)
Definition: abcNtk.c:106
Abc_Obj_t * pCopy
Definition: abc.h:148
ABC_DLL void Abc_NtkDeleteObj(Abc_Obj_t *pObj)
Definition: abcObj.c:167
ABC_DLL int Abc_AigCleanup(Abc_Aig_t *pMan)
Definition: abcAig.c:194
ABC_DLL int Abc_NtkRewrite(Abc_Ntk_t *pNtk, int fUpdateLevel, int fUseZeros, int fVerbose, int fVeryVerbose, int fPlaceEnable)
FUNCTION DEFINITIONS ///.
Definition: abcRewrite.c:61
ABC_DLL Abc_Obj_t * Abc_AigMiter(Abc_Aig_t *pMan, Vec_Ptr_t *vPairs, int fImplic)
Definition: abcAig.c:789
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
ABC_DLL int Abc_NtkRefactor(Abc_Ntk_t *pNtk, int nNodeSizeMax, int nConeSizeMax, int fUpdateLevel, int fUseZeros, int fUseDcs, int fVerbose)
FUNCTION DEFINITIONS ///.
Definition: abcRefactor.c:89
char * sprintf()
static Abc_Obj_t * Abc_NtkCreatePi(Abc_Ntk_t *pNtk)
Definition: abc.h:303
Abc_Ntk_t * Abc_NtkTransRel(Abc_Ntk_t *pNtk, int fInputs, int fVerbose)
Definition: abcQuant.c:159
int Abc_NtkQuantify(Abc_Ntk_t *pNtk, int fUniv, int iVar, int fVerbose)
Definition: abcQuant.c:83
#define Abc_NtkForEachNode(pNtk, pNode, i)
Definition: abc.h:461
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
static Abc_Obj_t * Abc_ObjChild0Data(Abc_Obj_t *pObj)
Definition: abc.h:388
static int Abc_NodeIsTravIdCurrent(Abc_Obj_t *p)
Definition: abc.h:411
static Abc_Obj_t * Abc_ObjRegular(Abc_Obj_t *p)
Definition: abc.h:323
Abc_Ntk_t * Abc_NtkInitialState(Abc_Ntk_t *pNtk)
Definition: abcQuant.c:261
static Abc_Obj_t * Abc_NtkPo(Abc_Ntk_t *pNtk, int i)
Definition: abc.h:316
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
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
ABC_DLL void Abc_NtkCleanData(Abc_Ntk_t *pNtk)
Definition: abcUtil.c:534
#define Abc_NtkForEachLatchInput(pNtk, pObj, i)
Definition: abc.h:500
ABC_DLL Abc_Ntk_t * Abc_NtkBalance(Abc_Ntk_t *pNtk, int fDuplicate, int fSelective, int fUpdateLevel)
FUNCTION DEFINITIONS ///.
Definition: abcBalance.c:53
static void Abc_ObjXorFaninC(Abc_Obj_t *pObj, int i)
Definition: abc.h:381
ABC_DLL void Abc_NtkCleanCopy(Abc_Ntk_t *pNtk)
Definition: abcUtil.c:507
static Abc_Obj_t * Abc_ObjNotCond(Abc_Obj_t *p, int c)
Definition: abc.h:325
#define assert(ex)
Definition: util_old.h:213
static Abc_Obj_t * Abc_ObjNot(Abc_Obj_t *p)
Definition: abc.h:324
static Abc_Obj_t * Abc_NtkPi(Abc_Ntk_t *pNtk, int i)
Definition: abc.h:315
void * pData
Definition: abc.h:145
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
ABC_INT64_T abctime
Definition: abc_global.h:278
ABC_DLL Abc_Ntk_t * Abc_NtkMiterAnd(Abc_Ntk_t *pNtk1, Abc_Ntk_t *pNtk2, int fOr, int fCompl2)
Definition: abcMiter.c:384
ABC_DLL Vec_Ptr_t * Abc_NtkDfsReverseNodes(Abc_Ntk_t *pNtk, Abc_Obj_t **ppNodes, int nNodes)
Definition: abcDfs.c:263
static Abc_Obj_t * Abc_NtkCreatePo(Abc_Ntk_t *pNtk)
Definition: abc.h:304
char * pName
Definition: abc.h:158
#define Abc_NtkForEachPi(pNtk, pPi, i)
Definition: abc.h:513
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223