abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
res.h File Reference

Go to the source code of this file.

Data Structures

struct  Res_Par_t_
 

Typedefs

typedef
typedefABC_NAMESPACE_HEADER_START
struct Res_Par_t_ 
Res_Par_t
 INCLUDES ///. More...
 

Functions

int Abc_NtkResynthesize (Abc_Ntk_t *pNtk, Res_Par_t *pPars)
 MACRO DEFINITIONS ///. More...
 

Typedef Documentation

typedef typedefABC_NAMESPACE_HEADER_START struct Res_Par_t_ Res_Par_t

INCLUDES ///.

CFile****************************************************************

FileName [res.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Resynthesis package.]

Synopsis [External declarations.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - January 15, 2007.]

Revision [

Id:
res.h,v 1.00 2007/01/15 00:00:00 alanmi Exp

]PARAMETERS ///BASIC TYPES ///

Definition at line 42 of file res.h.

Function Documentation

int Abc_NtkResynthesize ( Abc_Ntk_t pNtk,
Res_Par_t pPars 
)

MACRO DEFINITIONS ///.

FUNCTION DECLARATIONS ///

Function*************************************************************

Synopsis [Entrace into the resynthesis package.]

Description []

SideEffects []

SeeAlso []

Definition at line 213 of file resCore.c.

214 {
215  ProgressBar * pProgress;
216  Res_Man_t * p;
217  Abc_Obj_t * pObj;
218  Hop_Obj_t * pFunc;
219  Kit_Graph_t * pGraph;
220  Vec_Ptr_t * vFanins;
221  unsigned * puTruth;
222  int i, k, RetValue, nNodesOld, nFanins, nFaninsMax;
223  abctime clk, clkTotal = Abc_Clock();
224 
225  // start the manager
226  p = Res_ManAlloc( pPars );
227  p->nTotalNets = Abc_NtkGetTotalFanins(pNtk);
228  p->nTotalNodes = Abc_NtkNodeNum(pNtk);
229  nFaninsMax = Abc_NtkGetFaninMax(pNtk);
230  if ( nFaninsMax > 8 )
231  nFaninsMax = 8;
232 
233  // perform the network sweep
234  Abc_NtkSweep( pNtk, 0 );
235 
236  // convert into the AIG
237  if ( !Abc_NtkToAig(pNtk) )
238  {
239  fprintf( stdout, "Converting to BDD has failed.\n" );
240  Res_ManFree( p );
241  return 0;
242  }
243  assert( Abc_NtkHasAig(pNtk) );
244 
245  // set the number of levels
246  Abc_NtkLevel( pNtk );
247  Abc_NtkStartReverseLevels( pNtk, pPars->nGrowthLevel );
248 
249  // try resynthesizing nodes in the topological order
250  nNodesOld = Abc_NtkObjNumMax(pNtk);
251  pProgress = Extra_ProgressBarStart( stdout, nNodesOld );
252  Abc_NtkForEachObj( pNtk, pObj, i )
253  {
254  Extra_ProgressBarUpdate( pProgress, i, NULL );
255  if ( !Abc_ObjIsNode(pObj) )
256  continue;
257  if ( Abc_ObjFaninNum(pObj) > 8 )
258  continue;
259  if ( pObj->Id > nNodesOld )
260  break;
261 
262  // create the window for this node
263 clk = Abc_Clock();
264  RetValue = Res_WinCompute( pObj, p->pPars->nWindow/10, p->pPars->nWindow%10, p->pWin );
265 p->timeWin += Abc_Clock() - clk;
266  if ( !RetValue )
267  continue;
268  p->nWinsTriv += Res_WinIsTrivial( p->pWin );
269 
270  if ( p->pPars->fVeryVerbose )
271  {
272  printf( "%5d (lev=%2d) : ", pObj->Id, pObj->Level );
273  printf( "Win = %3d/%3d/%4d/%3d ",
274  Vec_PtrSize(p->pWin->vLeaves),
275  Vec_PtrSize(p->pWin->vBranches),
276  Vec_PtrSize(p->pWin->vNodes),
277  Vec_PtrSize(p->pWin->vRoots) );
278  }
279 
280  // collect the divisors
281 clk = Abc_Clock();
282  Res_WinDivisors( p->pWin, Abc_ObjRequiredLevel(pObj) - 1 );
283 p->timeDiv += Abc_Clock() - clk;
284 
285  p->nWins++;
286  p->nWinNodes += Vec_PtrSize(p->pWin->vNodes);
287  p->nDivNodes += Vec_PtrSize( p->pWin->vDivs);
288 
289  if ( p->pPars->fVeryVerbose )
290  {
291  printf( "D = %3d ", Vec_PtrSize(p->pWin->vDivs) );
292  printf( "D+ = %3d ", p->pWin->nDivsPlus );
293  }
294 
295  // create the AIG for the window
296 clk = Abc_Clock();
297  if ( p->pAig ) Abc_NtkDelete( p->pAig );
298  p->pAig = Res_WndStrash( p->pWin );
299 p->timeAig += Abc_Clock() - clk;
300 
301  if ( p->pPars->fVeryVerbose )
302  {
303  printf( "AIG = %4d ", Abc_NtkNodeNum(p->pAig) );
304  printf( "\n" );
305  }
306 
307  // prepare simulation info
308 clk = Abc_Clock();
309  RetValue = Res_SimPrepare( p->pSim, p->pAig, Vec_PtrSize(p->pWin->vLeaves), 0 ); //p->pPars->fVerbose );
310 p->timeSim += Abc_Clock() - clk;
311  if ( !RetValue )
312  {
313  p->nSimEmpty++;
314  continue;
315  }
316 
317  // consider the case of constant node
318  if ( p->pSim->fConst0 || p->pSim->fConst1 )
319  {
320  p->nConstsUsed++;
321 
322  pFunc = p->pSim->fConst1? Hop_ManConst1((Hop_Man_t *)pNtk->pManFunc) : Hop_ManConst0((Hop_Man_t *)pNtk->pManFunc);
323  vFanins = Vec_VecEntry( p->vResubsW, 0 );
324  Vec_PtrClear( vFanins );
325  Res_UpdateNetwork( pObj, vFanins, pFunc, p->vLevels );
326  continue;
327  }
328 
329 // printf( " " );
330 
331  // find resub candidates for the node
332 clk = Abc_Clock();
333  if ( p->pPars->fArea )
334  RetValue = Res_FilterCandidates( p->pWin, p->pAig, p->pSim, p->vResubs, p->vResubsW, nFaninsMax, 1 );
335  else
336  RetValue = Res_FilterCandidates( p->pWin, p->pAig, p->pSim, p->vResubs, p->vResubsW, nFaninsMax, 0 );
337 p->timeCand += Abc_Clock() - clk;
338  p->nCandSets += RetValue;
339  if ( RetValue == 0 )
340  continue;
341 
342 // printf( "%d(%d) ", Vec_PtrSize(p->pWin->vDivs), RetValue );
343 
344  p->nWinsUsed++;
345 
346  // iterate through candidate resubstitutions
347  Vec_VecForEachLevel( p->vResubs, vFanins, k )
348  {
349  if ( Vec_PtrSize(vFanins) == 0 )
350  break;
351 
352  // solve the SAT problem and get clauses
353 clk = Abc_Clock();
354  if ( p->pCnf ) Sto_ManFree( p->pCnf );
355  p->pCnf = (Sto_Man_t *)Res_SatProveUnsat( p->pAig, vFanins );
356  if ( p->pCnf == NULL )
357  {
358 p->timeSatSat += Abc_Clock() - clk;
359 // printf( " Sat\n" );
360 // printf( "-" );
361  continue;
362  }
363 p->timeSatUnsat += Abc_Clock() - clk;
364 // printf( "+" );
365 
366  p->nProvedSets++;
367 // printf( " Unsat\n" );
368 // continue;
369 // printf( "Proved %d.\n", k );
370 
371  // write it into a file
372 // Sto_ManDumpClauses( p->pCnf, "trace.cnf" );
373 
374  // interpolate the problem if it was UNSAT
375 clk = Abc_Clock();
376  nFanins = Int_ManInterpolate( p->pMan, p->pCnf, 0, &puTruth );
377 p->timeInt += Abc_Clock() - clk;
378  if ( nFanins != Vec_PtrSize(vFanins) - 2 )
379  continue;
380  assert( puTruth );
381 // Extra_PrintBinary( stdout, puTruth, 1 << nFanins ); printf( "\n" );
382 
383  // transform interpolant into the AIG
384  pGraph = Kit_TruthToGraph( puTruth, nFanins, p->vMem );
385 
386  // derive the AIG for the decomposition tree
387  pFunc = Kit_GraphToHop( (Hop_Man_t *)pNtk->pManFunc, pGraph );
388  Kit_GraphFree( pGraph );
389 
390  // update the network
391 clk = Abc_Clock();
392  Res_UpdateNetwork( pObj, Vec_VecEntry(p->vResubsW, k), pFunc, p->vLevels );
393 p->timeUpd += Abc_Clock() - clk;
394  break;
395  }
396 // printf( "\n" );
397  }
398  Extra_ProgressBarStop( pProgress );
399  Abc_NtkStopReverseLevels( pNtk );
400 
401 p->timeSatSim += p->pSim->timeSat;
402 p->timeSatTotal = p->timeSatSat + p->timeSatUnsat + p->timeSatSim;
403 
404  p->nTotalNets2 = Abc_NtkGetTotalFanins(pNtk);
405  p->nTotalNodes2 = Abc_NtkNodeNum(pNtk);
406 
407  // quit resubstitution manager
408 p->timeTotal = Abc_Clock() - clkTotal;
409  Res_ManFree( p );
410 
411 s_ResynTime += Abc_Clock() - clkTotal;
412  // check the resulting network
413  if ( !Abc_NtkCheck( pNtk ) )
414  {
415  fprintf( stdout, "Abc_NtkResynthesize(): Network check has failed.\n" );
416  return 0;
417  }
418  return 1;
419 }
#define Vec_VecForEachLevel(vGlob, vVec, i)
MACRO DEFINITIONS ///.
Definition: vecVec.h:55
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
int Int_ManInterpolate(Int_Man_t *p, Sto_Man_t *pCnf, int fVerbose, unsigned **ppResult)
Definition: satInter.c:1005
static int Abc_NtkObjNumMax(Abc_Ntk_t *pNtk)
Definition: abc.h:284
static Hop_Obj_t * Hop_ManConst1(Hop_Man_t *p)
Definition: hop.h:132
static Llb_Mgr_t * p
Definition: llb3Image.c:950
int Res_WinIsTrivial(Res_Win_t *p)
Definition: resWin.c:435
void Res_WinDivisors(Res_Win_t *p, int nLevDivMax)
FUNCTION DEFINITIONS ///.
Definition: resDivs.c:48
Abc_Ntk_t * Res_WndStrash(Res_Win_t *p)
FUNCTION DEFINITIONS ///.
Definition: resStrash.c:49
abctime s_ResynTime
Definition: abcPrint.c:47
static int Abc_ObjFaninNum(Abc_Obj_t *pObj)
Definition: abc.h:364
ABC_DLL int Abc_NtkGetFaninMax(Abc_Ntk_t *pNtk)
Definition: abcUtil.c:453
void Res_ManFree(Res_Man_t *p)
Definition: resCore.c:125
int Res_WinCompute(Abc_Obj_t *pNode, int nWinTfiMax, int nWinTfoMax, Res_Win_t *p)
Definition: resWin.c:451
int Res_SimPrepare(Res_Sim_t *p, Abc_Ntk_t *pAig, int nTruePis, int fVerbose)
Definition: resSim.c:731
ABC_DLL int Abc_NtkCheck(Abc_Ntk_t *pNtk)
FUNCTION DEFINITIONS ///.
Definition: abcCheck.c:61
static abctime Abc_Clock()
Definition: abc_global.h:279
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
ABC_DLL int Abc_NtkGetTotalFanins(Abc_Ntk_t *pNtk)
Definition: abcUtil.c:487
Res_Man_t * Res_ManAlloc(Res_Par_t *pPars)
FUNCTION DEFINITIONS ///.
Definition: resCore.c:96
Definition: hop.h:65
ABC_DLL void Abc_NtkStopReverseLevels(Abc_Ntk_t *pNtk)
Definition: abcTiming.c:1190
ABC_DLL void Abc_NtkDelete(Abc_Ntk_t *pNtk)
Definition: abcNtk.c:1233
unsigned Level
Definition: abc.h:142
Hop_Obj_t * Kit_GraphToHop(Hop_Man_t *pMan, Kit_Graph_t *pGraph)
Definition: kitHop.c:136
void * pManFunc
Definition: abc.h:191
static int Abc_ObjIsNode(Abc_Obj_t *pObj)
Definition: abc.h:355
static int Abc_NtkNodeNum(Abc_Ntk_t *pNtk)
Definition: abc.h:293
DECLARATIONS ///.
ABC_DLL int Abc_ObjRequiredLevel(Abc_Obj_t *pObj)
Definition: abcTiming.c:1102
void Kit_GraphFree(Kit_Graph_t *pGraph)
Definition: kitGraph.c:131
void Res_UpdateNetwork(Abc_Obj_t *pObj, Vec_Ptr_t *vFanins, Hop_Obj_t *pFunc, Vec_Vec_t *vLevels)
Definition: resCore.c:185
ABC_DLL void Abc_NtkStartReverseLevels(Abc_Ntk_t *pNtk, int nMaxLevelIncrease)
Definition: abcTiming.c:1162
void Extra_ProgressBarStop(ProgressBar *p)
typedefABC_NAMESPACE_IMPL_START struct Res_Man_t_ Res_Man_t
DECLARATIONS ///.
Definition: resCore.c:33
void * Res_SatProveUnsat(Abc_Ntk_t *pAig, Vec_Ptr_t *vFanins)
FUNCTION DEFINITIONS ///.
Definition: resSat.c:52
void Sto_ManFree(Sto_Man_t *p)
Definition: satStore.c:143
ABC_DLL int Abc_NtkSweep(Abc_Ntk_t *pNtk, int fVerbose)
Definition: abcSweep.c:574
int Id
Definition: abc.h:132
int Res_FilterCandidates(Res_Win_t *pWin, Abc_Ntk_t *pAig, Res_Sim_t *pSim, Vec_Vec_t *vResubs, Vec_Vec_t *vResubsW, int nFaninsMax, int fArea)
FUNCTION DEFINITIONS ///.
Definition: resFilter.c:49
ProgressBar * Extra_ProgressBarStart(FILE *pFile, int nItemsTotal)
FUNCTION DEFINITIONS ///.
ABC_DLL int Abc_NtkToAig(Abc_Ntk_t *pNtk)
Definition: abcFunc.c:1192
#define assert(ex)
Definition: util_old.h:213
static void Extra_ProgressBarUpdate(ProgressBar *p, int nItemsCur, char *pString)
Definition: extra.h:243
static void Vec_PtrClear(Vec_Ptr_t *p)
Definition: vecPtr.h:545
static int Abc_NtkHasAig(Abc_Ntk_t *pNtk)
Definition: abc.h:255
static Hop_Obj_t * Hop_ManConst0(Hop_Man_t *p)
Definition: hop.h:131
static Vec_Ptr_t * Vec_VecEntry(Vec_Vec_t *p, int i)
Definition: vecVec.h:271
ABC_INT64_T abctime
Definition: abc_global.h:278
#define Abc_NtkForEachObj(pNtk, pObj, i)
ITERATORS ///.
Definition: abc.h:446
ABC_DLL int Abc_NtkLevel(Abc_Ntk_t *pNtk)
Definition: abcDfs.c:1265
Kit_Graph_t * Kit_TruthToGraph(unsigned *pTruth, int nVars, Vec_Int_t *vMemory)
Definition: kitGraph.c:355
typedefABC_NAMESPACE_HEADER_START struct Hop_Man_t_ Hop_Man_t
INCLUDES ///.
Definition: hop.h:49