ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
mfsCore.c
Go to the documentation of this file.
1
20
21#include "mfsInt.h"
22
23ABC_NAMESPACE_IMPL_START
24
25
29
30extern int Abc_NtkMfsSolveSatResub( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int fOnlyRemove, int fSkipUpdate );
31
35
47void Abc_NtkMfsParsDefault( Mfs_Par_t * pPars )
48{
49 memset( pPars, 0, sizeof(Mfs_Par_t) );
50 pPars->nWinTfoLevs = 2;
51 pPars->nFanoutsMax = 30;
52 pPars->nDepthMax = 20;
53 pPars->nWinMax = 300;
54 pPars->nGrowthLevel = 0;
55 pPars->nBTLimit = 5000;
56 pPars->fRrOnly = 0;
57 pPars->fResub = 1;
58 pPars->fArea = 0;
59 pPars->fMoreEffort = 0;
60 pPars->fSwapEdge = 0;
61 pPars->fOneHotness = 0;
62 pPars->fVerbose = 0;
63 pPars->fVeryVerbose = 0;
64}
65/*
66int Abc_NtkMfsEdgePower( Mfs_Man_t * p, Abc_Obj_t * pNode )
67{
68 Abc_Obj_t * pFanin;
69 int i;
70 // try replacing area critical fanins
71 Abc_ObjForEachFanin( pNode, pFanin, i )
72 {
73 if ( Abc_MfsObjProb(p, pFanin) >= 0.4 )
74 {
75 if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 0 ) )
76 return 1;
77 } else if ( Abc_MfsObjProb(p, pFanin) >= 0.3 )
78 {
79 if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 1, 0 ) )
80 return 1;
81 }
82 }
83 return 0;
84}
85*/
86
87int Abc_WinNode(Mfs_Man_t * p, Abc_Obj_t *pNode)
88{
89// abctime clk;
90// Abc_Obj_t * pFanin;
91// int i;
92
93 p->nNodesTried++;
94 // prepare data structure for this node
95 Mfs_ManClean( p );
96 // compute window roots, window support, and window nodes
97 p->vRoots = Abc_MfsComputeRoots( pNode, p->pPars->nWinTfoLevs, p->pPars->nFanoutsMax );
98 p->vSupp = Abc_NtkNodeSupport( p->pNtk, (Abc_Obj_t **)Vec_PtrArray(p->vRoots), Vec_PtrSize(p->vRoots) );
99 p->vNodes = Abc_NtkDfsNodes( p->pNtk, (Abc_Obj_t **)Vec_PtrArray(p->vRoots), Vec_PtrSize(p->vRoots) );
100 if ( p->pPars->nWinMax && Vec_PtrSize(p->vNodes) > p->pPars->nWinMax )
101 return 1;
102 // compute the divisors of the window
103 p->vDivs = Abc_MfsComputeDivisors( p, pNode, Abc_ObjRequiredLevel(pNode) - 1 );
104 p->nTotalDivs += Vec_PtrSize(p->vDivs) - Abc_ObjFaninNum(pNode);
105 // construct AIG for the window
106 p->pAigWin = Abc_NtkConstructAig( p, pNode );
107 // translate it into CNF
108 p->pCnf = Cnf_DeriveSimple( p->pAigWin, 1 + Vec_PtrSize(p->vDivs) );
109 // create the SAT problem
110 p->pSat = Abc_MfsCreateSolverResub( p, NULL, 0, 0 );
111 if ( p->pSat == NULL )
112 {
113 p->nNodesBad++;
114 return 1;
115 }
116 return 0;
117}
118
119/*
120int Abc_NtkMfsPowerResubNode( Mfs_Man_t * p, Abc_Obj_t * pNode )
121{
122 abctime clk;
123 Abc_Obj_t * pFanin;
124 int i;
125
126 if (Abc_WinNode(p, pNode) // something wrong
127 return 1;
128
129 // solve the SAT problem
130 // Abc_NtkMfsEdgePower( p, pNode );
131 // try replacing area critical fanins
132 Abc_ObjForEachFanin( pNode, pFanin, i )
133 if ( Abc_MfsObjProb(p, pFanin) >= 0.37 && Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 0 ) )
134 return 1;
135
136 Abc_ObjForEachFanin( pNode, pFanin, i )
137 if ( Abc_MfsObjProb(p, pFanin) >= 0.1 && Abc_NtkMfsSolveSatResub( p, pNode, i, 1, 0 ) )
138 return 1;
139
140 if ( Abc_ObjFaninNum(pNode) == p->nFaninMax )
141 return 0;
142
143 // try replacing area critical fanins while adding two new fanins
144 Abc_ObjForEachFanin( pNode, pFanin, i )
145 if ( Abc_MfsObjProb(p, pFanin) >= 0.37 && Abc_NtkMfsSolveSatResub2( p, pNode, i, -1 ) )
146 return 1;
147 }
148 return 0;
149
150 return 1;
151}
152*/
153
154void Abc_NtkMfsPowerResub( Mfs_Man_t * p, Mfs_Par_t * pPars)
155{
156 int i, k;
157 Abc_Obj_t *pFanin, *pNode;
158 Abc_Ntk_t *pNtk = p->pNtk;
159 int nFaninMax = Abc_NtkGetFaninMax(p->pNtk);
160
161 Abc_NtkForEachNode( pNtk, pNode, k )
162 {
163 if ( p->pPars->nDepthMax && (int)pNode->Level > p->pPars->nDepthMax )
164 continue;
165 if ( Abc_ObjFaninNum(pNode) < 2 || Abc_ObjFaninNum(pNode) > nFaninMax )
166 continue;
167 if (Abc_WinNode(p, pNode) ) // something wrong
168 continue;
169
170 // solve the SAT problem
171 // Abc_NtkMfsEdgePower( p, pNode );
172 // try replacing area critical fanins
173 Abc_ObjForEachFanin( pNode, pFanin, i )
174 if ( Abc_MfsObjProb(p, pFanin) >= 0.35 && Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 0 ) )
175 continue;
176 }
177
178 Abc_NtkForEachNode( pNtk, pNode, k )
179 {
180 if ( p->pPars->nDepthMax && (int)pNode->Level > p->pPars->nDepthMax )
181 continue;
182 if ( Abc_ObjFaninNum(pNode) < 2 || Abc_ObjFaninNum(pNode) > nFaninMax )
183 continue;
184 if (Abc_WinNode(p, pNode) ) // something wrong
185 continue;
186
187 // solve the SAT problem
188 // Abc_NtkMfsEdgePower( p, pNode );
189 // try replacing area critical fanins
190 Abc_ObjForEachFanin( pNode, pFanin, i )
191 if ( Abc_MfsObjProb(p, pFanin) >= 0.35 && Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 0 ) )
192 continue;
193 }
194
195 Abc_NtkForEachNode( pNtk, pNode, k )
196 {
197 if ( p->pPars->nDepthMax && (int)pNode->Level > p->pPars->nDepthMax )
198 continue;
199 if ( Abc_ObjFaninNum(pNode) < 2 || Abc_ObjFaninNum(pNode) > nFaninMax )
200 continue;
201 if (Abc_WinNode(p, pNode) ) // something wrong
202 continue;
203
204 Abc_ObjForEachFanin( pNode, pFanin, i )
205 if ( Abc_MfsObjProb(p, pFanin) >= 0.2 && Abc_NtkMfsSolveSatResub( p, pNode, i, 1, 0 ) )
206 continue;
207 }
208/*
209 Abc_NtkForEachNode( pNtk, pNode, k )
210 {
211 if ( p->pPars->nDepthMax && (int)pNode->Level > p->pPars->nDepthMax )
212 continue;
213 if ( Abc_ObjFaninNum(pNode) < 2 || Abc_ObjFaninNum(pNode) > nFaninMax - 2)
214 continue;
215 if (Abc_WinNode(p, pNode) ) // something wrong
216 continue;
217
218 Abc_ObjForEachFanin( pNode, pFanin, i )
219 if ( Abc_MfsObjProb(p, pFanin) >= 0.37 && Abc_NtkMfsSolveSatResub2( p, pNode, i, -1 ) )
220 continue;
221 }
222*/
223}
224
236int Abc_NtkMfsResub( Mfs_Man_t * p, Abc_Obj_t * pNode )
237{
238 abctime clk;
239 p->nNodesTried++;
240 // prepare data structure for this node
241 Mfs_ManClean( p );
242 // compute window roots, window support, and window nodes
243clk = Abc_Clock();
244 p->vRoots = Abc_MfsComputeRoots( pNode, p->pPars->nWinTfoLevs, p->pPars->nFanoutsMax );
245 p->vSupp = Abc_NtkNodeSupport( p->pNtk, (Abc_Obj_t **)Vec_PtrArray(p->vRoots), Vec_PtrSize(p->vRoots) );
246 p->vNodes = Abc_NtkDfsNodes( p->pNtk, (Abc_Obj_t **)Vec_PtrArray(p->vRoots), Vec_PtrSize(p->vRoots) );
247p->timeWin += Abc_Clock() - clk;
248 if ( p->pPars->nWinMax && Vec_PtrSize(p->vNodes) > p->pPars->nWinMax )
249 {
250 p->nMaxDivs++;
251 return 1;
252 }
253 // compute the divisors of the window
254clk = Abc_Clock();
255 p->vDivs = Abc_MfsComputeDivisors( p, pNode, Abc_ObjRequiredLevel(pNode) - 1 );
256 p->nTotalDivs += Vec_PtrSize(p->vDivs) - Abc_ObjFaninNum(pNode);
257p->timeDiv += Abc_Clock() - clk;
258 // construct AIG for the window
259clk = Abc_Clock();
260 p->pAigWin = Abc_NtkConstructAig( p, pNode );
261p->timeAig += Abc_Clock() - clk;
262 // translate it into CNF
263clk = Abc_Clock();
264 p->pCnf = Cnf_DeriveSimple( p->pAigWin, 1 + Vec_PtrSize(p->vDivs) );
265p->timeCnf += Abc_Clock() - clk;
266 // create the SAT problem
267clk = Abc_Clock();
268 p->pSat = Abc_MfsCreateSolverResub( p, NULL, 0, 0 );
269 if ( p->pSat == NULL )
270 {
271 p->nNodesBad++;
272 return 1;
273 }
274//clk = Abc_Clock();
275// if ( p->pPars->fGiaSat )
276// Abc_NtkMfsConstructGia( p );
277//p->timeGia += Abc_Clock() - clk;
278 // solve the SAT problem
279 if ( p->pPars->fPower )
280 Abc_NtkMfsEdgePower( p, pNode );
281 else if ( p->pPars->fSwapEdge )
282 Abc_NtkMfsEdgeSwapEval( p, pNode );
283 else
284 {
285 Abc_NtkMfsResubNode( p, pNode );
286 if ( p->pPars->fMoreEffort )
287 Abc_NtkMfsResubNode2( p, pNode );
288 }
289p->timeSat += Abc_Clock() - clk;
290// if ( p->pPars->fGiaSat )
291// Abc_NtkMfsDeconstructGia( p );
292 return 1;
293}
294
306int Abc_NtkMfsNode( Mfs_Man_t * p, Abc_Obj_t * pNode )
307{
308 Hop_Obj_t * pObj;
309 int RetValue;
310 float dProb;
311 extern Hop_Obj_t * Abc_NodeIfNodeResyn( Bdc_Man_t * p, Hop_Man_t * pHop, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth, unsigned * puCare, float dProb );
312
313 int nGain;
314 abctime clk;
315 p->nNodesTried++;
316 // prepare data structure for this node
317 Mfs_ManClean( p );
318 // compute window roots, window support, and window nodes
319clk = Abc_Clock();
320 p->vRoots = Abc_MfsComputeRoots( pNode, p->pPars->nWinTfoLevs, p->pPars->nFanoutsMax );
321 p->vSupp = Abc_NtkNodeSupport( p->pNtk, (Abc_Obj_t **)Vec_PtrArray(p->vRoots), Vec_PtrSize(p->vRoots) );
322 p->vNodes = Abc_NtkDfsNodes( p->pNtk, (Abc_Obj_t **)Vec_PtrArray(p->vRoots), Vec_PtrSize(p->vRoots) );
323p->timeWin += Abc_Clock() - clk;
324 // count the number of patterns
325// p->dTotalRatios += Abc_NtkConstraintRatio( p, pNode );
326 // construct AIG for the window
327clk = Abc_Clock();
328 p->pAigWin = Abc_NtkConstructAig( p, pNode );
329p->timeAig += Abc_Clock() - clk;
330 // translate it into CNF
331clk = Abc_Clock();
332 p->pCnf = Cnf_DeriveSimple( p->pAigWin, Abc_ObjFaninNum(pNode) );
333p->timeCnf += Abc_Clock() - clk;
334 // create the SAT problem
335clk = Abc_Clock();
336 p->pSat = (sat_solver *)Cnf_DataWriteIntoSolver( p->pCnf, 1, 0 );
337 if ( p->pSat && p->pPars->fOneHotness )
338 Abc_NtkAddOneHotness( p );
339 if ( p->pSat == NULL )
340 return 0;
341 // solve the SAT problem
342 RetValue = Abc_NtkMfsSolveSat( p, pNode );
343 p->nTotConfLevel += p->pSat->stats.conflicts;
344p->timeSat += Abc_Clock() - clk;
345 if ( RetValue == 0 )
346 {
347 p->nTimeOutsLevel++;
348 p->nTimeOuts++;
349 return 0;
350 }
351 // minimize the local function of the node using bi-decomposition
352 assert( p->nFanins == Abc_ObjFaninNum(pNode) );
353 dProb = p->pPars->fPower? ((float *)p->vProbs->pArray)[pNode->Id] : -1.0;
354 pObj = Abc_NodeIfNodeResyn( p->pManDec, (Hop_Man_t *)pNode->pNtk->pManFunc, (Hop_Obj_t *)pNode->pData, p->nFanins, p->vTruth, p->uCare, dProb );
355 nGain = Hop_DagSize((Hop_Obj_t *)pNode->pData) - Hop_DagSize(pObj);
356 if ( nGain >= 0 )
357 {
358 p->nNodesDec++;
359 p->nNodesGained += nGain;
360 p->nNodesGainedLevel += nGain;
361 pNode->pData = pObj;
362 }
363 return 1;
364}
365
377int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
378{
379 extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
380
381 Bdc_Par_t Pars = {0}, * pDecPars = &Pars;
382 ProgressBar * pProgress;
383 Mfs_Man_t * p;
384 Abc_Obj_t * pObj;
385 Vec_Vec_t * vLevels;
386 Vec_Ptr_t * vNodes;
387 int i, k, nNodes, nFaninMax;
388 abctime clk = Abc_Clock(), clk2;
389 int nTotalNodesBeg = Abc_NtkNodeNum(pNtk);
390 int nTotalEdgesBeg = Abc_NtkGetTotalFanins(pNtk);
391
392 assert( Abc_NtkIsLogic(pNtk) );
393 nFaninMax = Abc_NtkGetFaninMax(pNtk);
394 if ( pPars->fResub )
395 {
396 if ( nFaninMax > 8 )
397 {
398 printf( "Nodes with more than %d fanins will not be processed.\n", 8 );
399 nFaninMax = 8;
400 }
401 }
402 else
403 {
404 if ( nFaninMax > MFS_FANIN_MAX )
405 {
406 printf( "Nodes with more than %d fanins will not be processed.\n", MFS_FANIN_MAX );
407 nFaninMax = MFS_FANIN_MAX;
408 }
409 }
410 // perform the network sweep
411// Abc_NtkSweep( pNtk, 0 );
412 // convert into the AIG
413 if ( !Abc_NtkToAig(pNtk) )
414 {
415 fprintf( stdout, "Converting to AIGs has failed.\n" );
416 return 0;
417 }
418 assert( Abc_NtkHasAig(pNtk) );
419
420 // start the manager
421 p = Mfs_ManAlloc( pPars );
422 p->pNtk = pNtk;
423 p->nFaninMax = nFaninMax;
424
425 // precomputer power-aware metrics
426 if ( pPars->fPower )
427 {
428 extern Vec_Int_t * Abc_NtkPowerEstimate( Abc_Ntk_t * pNtk, int fProbOne );
429 if ( pPars->fResub )
430 p->vProbs = Abc_NtkPowerEstimate( pNtk, 0 );
431 else
432 p->vProbs = Abc_NtkPowerEstimate( pNtk, 1 );
433#if 0
434 printf( "Total switching before = %7.2f.\n", Abc_NtkMfsTotalSwitching(pNtk) );
435#else
436 p->TotalSwitchingBeg = Abc_NtkMfsTotalSwitching(pNtk);
437#endif
438 }
439
440 if ( pNtk->pExcare )
441 {
442 Abc_Ntk_t * pTemp;
443 if ( Abc_NtkPiNum((Abc_Ntk_t *)pNtk->pExcare) != Abc_NtkCiNum(pNtk) )
444 printf( "The PI count of careset (%d) and logic network (%d) differ. Careset is not used.\n",
445 Abc_NtkPiNum((Abc_Ntk_t *)pNtk->pExcare), Abc_NtkCiNum(pNtk) );
446 else
447 {
448 pTemp = Abc_NtkStrash( (Abc_Ntk_t *)pNtk->pExcare, 0, 0, 0 );
449 p->pCare = Abc_NtkToDar( pTemp, 0, 0 );
450 Abc_NtkDelete( pTemp );
451 p->vSuppsInv = Aig_ManSupportsInverse( p->pCare );
452 }
453 }
454 if ( p->pCare != NULL )
455 printf( "Performing optimization with %d external care clauses.\n", Aig_ManCoNum(p->pCare) );
456 // prepare the BDC manager
457 if ( !pPars->fResub )
458 {
459 pDecPars->nVarsMax = (nFaninMax < 3) ? 3 : nFaninMax;
460 pDecPars->fVerbose = pPars->fVerbose;
461 p->vTruth = Vec_IntAlloc( 0 );
462 p->pManDec = Bdc_ManAlloc( pDecPars );
463 }
464
465 // label the register outputs
466 if ( p->pCare )
467 {
468 Abc_NtkForEachCi( pNtk, pObj, i )
469 pObj->pData = (void *)(ABC_PTRUINT_T)i;
470 }
471
472 // compute levels
473 Abc_NtkLevel( pNtk );
474 Abc_NtkStartReverseLevels( pNtk, pPars->nGrowthLevel );
475
476 // compute don't-cares for each node
477 nNodes = 0;
478 p->nTotalNodesBeg = nTotalNodesBeg;
479 p->nTotalEdgesBeg = nTotalEdgesBeg;
480 if ( pPars->fResub )
481 {
482#if 0
483 printf( "TotalSwitching (%7.2f --> ", Abc_NtkMfsTotalSwitching(pNtk) );
484#endif
485 if (pPars->fPower)
486 {
487 Abc_NtkMfsPowerResub( p, pPars);
488 } else
489 {
490 pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pNtk) );
491 Abc_NtkForEachNode( pNtk, pObj, i )
492 {
493 if ( p->pPars->nDepthMax && (int)pObj->Level > p->pPars->nDepthMax )
494 continue;
495 if ( Abc_ObjFaninNum(pObj) < 2 || Abc_ObjFaninNum(pObj) > nFaninMax )
496 continue;
497 if ( !p->pPars->fVeryVerbose )
498 Extra_ProgressBarUpdate( pProgress, i, NULL );
499 if ( pPars->fResub )
500 Abc_NtkMfsResub( p, pObj );
501 else
502 Abc_NtkMfsNode( p, pObj );
503 }
504 Extra_ProgressBarStop( pProgress );
505#if 0
506 printf( " %7.2f )\n", Abc_NtkMfsTotalSwitching(pNtk) );
507#endif
508 }
509 } else
510 {
511#if 0
512 printf( "Total switching before = %7.2f, ----> ", Abc_NtkMfsTotalSwitching(pNtk) );
513#endif
514 pProgress = Extra_ProgressBarStart( stdout, Abc_NtkNodeNum(pNtk) );
515 vLevels = Abc_NtkLevelize( pNtk );
516 Vec_VecForEachLevelStart( vLevels, vNodes, k, 1 )
517 {
518 if ( !p->pPars->fVeryVerbose )
519 Extra_ProgressBarUpdate( pProgress, nNodes, NULL );
520 p->nNodesGainedLevel = 0;
521 p->nTotConfLevel = 0;
522 p->nTimeOutsLevel = 0;
523 clk2 = Abc_Clock();
524 Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
525 {
526 if ( p->pPars->nDepthMax && (int)pObj->Level > p->pPars->nDepthMax )
527 break;
528 if ( Abc_ObjFaninNum(pObj) < 2 || Abc_ObjFaninNum(pObj) > nFaninMax )
529 continue;
530 if ( pPars->fResub )
531 Abc_NtkMfsResub( p, pObj );
532 else
533 Abc_NtkMfsNode( p, pObj );
534 }
535 nNodes += Vec_PtrSize(vNodes);
536 if ( pPars->fVerbose )
537 {
538 /*
539 printf( "Lev = %2d. Node = %5d. Ave gain = %5.2f. Ave conf = %5.2f. T/o = %6.2f %% ",
540 k, Vec_PtrSize(vNodes),
541 1.0*p->nNodesGainedLevel/Vec_PtrSize(vNodes),
542 1.0*p->nTotConfLevel/Vec_PtrSize(vNodes),
543 100.0*p->nTimeOutsLevel/Vec_PtrSize(vNodes) );
544 ABC_PRT( "Time", Abc_Clock() - clk2 );
545 */
546 }
547 }
548 Extra_ProgressBarStop( pProgress );
549 Vec_VecFree( vLevels );
550#if 0
551 printf( " %7.2f.\n", Abc_NtkMfsTotalSwitching(pNtk) );
552#endif
553 }
554 Abc_NtkStopReverseLevels( pNtk );
555
556 // perform the sweeping
557 if ( !pPars->fResub )
558 {
559 extern void Abc_NtkBidecResyn( Abc_Ntk_t * pNtk, int fVerbose );
560// Abc_NtkSweep( pNtk, 0 );
561// Abc_NtkBidecResyn( pNtk, 0 );
562 }
563
564 p->nTotalNodesEnd = Abc_NtkNodeNum(pNtk);
565 p->nTotalEdgesEnd = Abc_NtkGetTotalFanins(pNtk);
566
567 // undo labesl
568 if ( p->pCare )
569 {
570 Abc_NtkForEachCi( pNtk, pObj, i )
571 pObj->pData = NULL;
572 }
573
574 if ( pPars->fPower )
575 {
576#if 1
577 p->TotalSwitchingEnd = Abc_NtkMfsTotalSwitching(pNtk);
578// printf( "Total switching after = %7.2f.\n", Abc_NtkMfsTotalSwitching(pNtk) );
579#else
580 printf( "Total switching after = %7.2f.\n", Abc_NtkMfsTotalSwitching(pNtk) );
581#endif
582 }
583
584 // free the manager
585 p->timeTotal = Abc_Clock() - clk;
586 Mfs_ManStop( p );
587 return 1;
588}
589
593
594
595ABC_NAMESPACE_IMPL_END
596
Abc_NtkBidecResyn
void Abc_NtkBidecResyn(Abc_Ntk_t *pNtk, int fVerbose)
Definition abcBidec.c:110
Abc_NodeIfNodeResyn
Hop_Obj_t * Abc_NodeIfNodeResyn(Bdc_Man_t *p, Hop_Man_t *pHop, Hop_Obj_t *pRoot, int nVars, Vec_Int_t *vTruth, unsigned *puCare, float dProb)
FUNCTION DEFINITIONS ///.
Definition abcBidec.c:49
Abc_NtkPowerEstimate
Vec_Int_t * Abc_NtkPowerEstimate(Abc_Ntk_t *pNtk, int fProbOne)
Definition abcSpeedup.c:669
Abc_Obj_t
struct Abc_Obj_t_ Abc_Obj_t
Definition abc.h:116
Abc_NtkMfsTotalSwitching
ABC_DLL float Abc_NtkMfsTotalSwitching(Abc_Ntk_t *pNtk)
Definition abcPrint.c:163
Abc_NtkLevelize
ABC_DLL Vec_Vec_t * Abc_NtkLevelize(Abc_Ntk_t *pNtk)
Definition abcDfs.c:1423
Abc_NtkGetFaninMax
ABC_DLL int Abc_NtkGetFaninMax(Abc_Ntk_t *pNtk)
Definition abcUtil.c:486
Abc_ObjRequiredLevel
ABC_DLL int Abc_ObjRequiredLevel(Abc_Obj_t *pObj)
Definition abcTiming.c:1214
Abc_ObjForEachFanin
#define Abc_ObjForEachFanin(pObj, pFanin, i)
Definition abc.h:527
Abc_Ntk_t
struct Abc_Ntk_t_ Abc_Ntk_t
Definition abc.h:115
Abc_NtkNodeSupport
ABC_DLL Vec_Ptr_t * Abc_NtkNodeSupport(Abc_Ntk_t *pNtk, Abc_Obj_t **ppNodes, int nNodes)
Definition abcDfs.c:890
Abc_NtkStopReverseLevels
ABC_DLL void Abc_NtkStopReverseLevels(Abc_Ntk_t *pNtk)
Definition abcTiming.c:1302
Abc_NtkLevel
ABC_DLL int Abc_NtkLevel(Abc_Ntk_t *pNtk)
Definition abcDfs.c:1449
Abc_NtkStartReverseLevels
ABC_DLL void Abc_NtkStartReverseLevels(Abc_Ntk_t *pNtk, int nMaxLevelIncrease)
Definition abcTiming.c:1274
Abc_NtkToAig
ABC_DLL int Abc_NtkToAig(Abc_Ntk_t *pNtk)
Definition abcFunc.c:1333
Abc_NtkStrash
ABC_DLL Abc_Ntk_t * Abc_NtkStrash(Abc_Ntk_t *pNtk, int fAllNodes, int fCleanup, int fRecord)
Definition abcStrash.c:265
Abc_NtkForEachCi
#define Abc_NtkForEachCi(pNtk, pCi, i)
Definition abc.h:518
Abc_NtkDelete
ABC_DLL void Abc_NtkDelete(Abc_Ntk_t *pNtk)
Definition abcNtk.c:1421
Abc_NtkDfsNodes
ABC_DLL Vec_Ptr_t * Abc_NtkDfsNodes(Abc_Ntk_t *pNtk, Abc_Obj_t **ppNodes, int nNodes)
Definition abcDfs.c:151
Abc_NtkGetTotalFanins
ABC_DLL int Abc_NtkGetTotalFanins(Abc_Ntk_t *pNtk)
Definition abcUtil.c:520
Abc_NtkForEachNode
#define Abc_NtkForEachNode(pNtk, pNode, i)
Definition abc.h:464
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition abc_namespaces.h:54
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition abc_namespaces.h:55
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition aig.h:50
Aig_ManSupportsInverse
Vec_Ptr_t * Aig_ManSupportsInverse(Aig_Man_t *p)
Definition aigPart.c:385
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
ProgressBar
ABC_NAMESPACE_IMPL_START typedef char ProgressBar
Definition bbrNtbdd.c:27
Bdc_Par_t
struct Bdc_Par_t_ Bdc_Par_t
Definition bdc.h:44
Bdc_Man_t
struct Bdc_Man_t_ Bdc_Man_t
Definition bdc.h:43
Bdc_ManAlloc
Bdc_Man_t * Bdc_ManAlloc(Bdc_Par_t *pPars)
MACRO DEFINITIONS ///.
Definition bdcCore.c:68
sat_solver
#define sat_solver
Definition cecSatG2.c:34
Cnf_DeriveSimple
Cnf_Dat_t * Cnf_DeriveSimple(Aig_Man_t *p, int nOutputs)
Definition cnfWrite.c:587
p
Cube * p
Definition exorList.c:222
Extra_ProgressBarStop
void Extra_ProgressBarStop(ProgressBar *p)
Definition extraUtilProgress.c:118
Extra_ProgressBarStart
ProgressBar * Extra_ProgressBarStart(FILE *pFile, int nItemsTotal)
FUNCTION DEFINITIONS ///.
Definition extraUtilProgress.c:62
Abc_NtkToDar
Aig_Man_t * Abc_NtkToDar(Abc_Ntk_t *pNtk, int fExors, int fRegisters)
Definition abcDar.c:237
Hop_Man_t
typedefABC_NAMESPACE_HEADER_START struct Hop_Man_t_ Hop_Man_t
INCLUDES ///.
Definition hop.h:49
Hop_DagSize
int Hop_DagSize(Hop_Obj_t *pObj)
Definition hopDfs.c:279
Hop_Obj_t
struct Hop_Obj_t_ Hop_Obj_t
Definition hop.h:50
Abc_NtkMfsParsDefault
void Abc_NtkMfsParsDefault(Mfs_Par_t *pPars)
FUNCTION DEFINITIONS ///.
Definition mfsCore.c:47
Abc_NtkMfsSolveSatResub
ABC_NAMESPACE_IMPL_START int Abc_NtkMfsSolveSatResub(Mfs_Man_t *p, Abc_Obj_t *pNode, int iFanin, int fOnlyRemove, int fSkipUpdate)
DECLARATIONS ///.
Definition mfsResub.c:165
Abc_WinNode
int Abc_WinNode(Mfs_Man_t *p, Abc_Obj_t *pNode)
Definition mfsCore.c:87
Abc_NtkMfsNode
int Abc_NtkMfsNode(Mfs_Man_t *p, Abc_Obj_t *pNode)
Definition mfsCore.c:306
Abc_NtkMfs
int Abc_NtkMfs(Abc_Ntk_t *pNtk, Mfs_Par_t *pPars)
Definition mfsCore.c:377
Abc_NtkMfsResub
int Abc_NtkMfsResub(Mfs_Man_t *p, Abc_Obj_t *pNode)
Definition mfsCore.c:236
Abc_NtkMfsPowerResub
void Abc_NtkMfsPowerResub(Mfs_Man_t *p, Mfs_Par_t *pPars)
Definition mfsCore.c:154
Abc_MfsComputeDivisors
Vec_Ptr_t * Abc_MfsComputeDivisors(Mfs_Man_t *p, Abc_Obj_t *pNode, int nLevDivMax)
BASIC TYPES ///.
Definition mfsDiv.c:193
Abc_NtkMfsResubNode
int Abc_NtkMfsResubNode(Mfs_Man_t *p, Abc_Obj_t *pNode)
Definition mfsResub.c:539
Abc_MfsComputeRoots
Vec_Ptr_t * Abc_MfsComputeRoots(Abc_Obj_t *pNode, int nWinTfoMax, int nFanoutLimit)
Definition mfsWin.c:99
Mfs_ManClean
void Mfs_ManClean(Mfs_Man_t *p)
Definition mfsMan.c:75
Mfs_ManAlloc
Mfs_Man_t * Mfs_ManAlloc(Mfs_Par_t *pPars)
DECLARATIONS ///.
Definition mfsMan.c:45
Abc_MfsCreateSolverResub
sat_solver * Abc_MfsCreateSolverResub(Mfs_Man_t *p, int *pCands, int nCands, int fInvert)
Definition mfsInter.c:88
Abc_NtkMfsEdgePower
int Abc_NtkMfsEdgePower(Mfs_Man_t *p, Abc_Obj_t *pNode)
Definition mfsResub.c:508
Abc_NtkMfsSolveSat
int Abc_NtkMfsSolveSat(Mfs_Man_t *p, Abc_Obj_t *pNode)
Definition mfsSat.c:95
Abc_NtkConstructAig
Aig_Man_t * Abc_NtkConstructAig(Mfs_Man_t *p, Abc_Obj_t *pNode)
Definition mfsStrash.c:233
Mfs_Man_t
struct Mfs_Man_t_ Mfs_Man_t
Definition mfsInt.h:49
Abc_NtkMfsEdgeSwapEval
int Abc_NtkMfsEdgeSwapEval(Mfs_Man_t *p, Abc_Obj_t *pNode)
Definition mfsResub.c:488
MFS_FANIN_MAX
#define MFS_FANIN_MAX
INCLUDES ///.
Definition mfsInt.h:47
Abc_NtkMfsResubNode2
int Abc_NtkMfsResubNode2(Mfs_Man_t *p, Abc_Obj_t *pNode)
Definition mfsResub.c:585
Mfs_ManStop
void Mfs_ManStop(Mfs_Man_t *p)
Definition mfsMan.c:170
Abc_NtkAddOneHotness
int Abc_NtkAddOneHotness(Mfs_Man_t *p)
Definition mfsSat.c:155
Mfs_Par_t
typedefABC_NAMESPACE_HEADER_START struct Mfs_Par_t_ Mfs_Par_t
INCLUDES ///.
Definition mfs.h:42
Cnf_DataWriteIntoSolver
void * Cnf_DataWriteIntoSolver(Cnf_Dat_t *p, int nFrames, int fInit)
Definition cnfMan.c:579
Abc_Ntk_t_::pManFunc
void * pManFunc
Definition abc.h:191
Abc_Ntk_t_::pExcare
void * pExcare
Definition abc.h:202
Abc_Obj_t_::pData
void * pData
Definition abc.h:145
Abc_Obj_t_::pNtk
Abc_Ntk_t * pNtk
Definition abc.h:130
Abc_Obj_t_::Id
int Id
Definition abc.h:132
Abc_Obj_t_::Level
unsigned Level
Definition abc.h:142
assert
#define assert(ex)
Definition util_old.h:213
memset
char * memset()
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition vecPtr.h:55
Vec_VecForEachLevelStart
#define Vec_VecForEachLevelStart(vGlob, vVec, i, LevelStart)
Definition vecVec.h:57
Vec_Vec_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Vec_t_ Vec_Vec_t
INCLUDES ///.
Definition vecVec.h:42