abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
saigRetMin.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [saigRetMin.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Sequential AIG package.]
8 
9  Synopsis [Min-area retiming for the AIG.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: saigRetMin.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "saig.h"
22 
23 #include "opt/nwk/nwk.h"
24 #include "sat/cnf/cnf.h"
25 #include "sat/bsat/satSolver.h"
26 #include "sat/bsat/satStore.h"
27 
28 ABC_NAMESPACE_IMPL_START
29 
30 
31 ////////////////////////////////////////////////////////////////////////
32 /// DECLARATIONS ///
33 ////////////////////////////////////////////////////////////////////////
34 
35 ////////////////////////////////////////////////////////////////////////
36 /// FUNCTION DEFINITIONS ///
37 ////////////////////////////////////////////////////////////////////////
38 
39 /**Function*************************************************************
40 
41  Synopsis [Derives the initial state after backward retiming.]
42 
43  Description []
44 
45  SideEffects []
46 
47  SeeAlso []
48 
49 ***********************************************************************/
50 Vec_Int_t * Saig_ManRetimeInitState( Aig_Man_t * p )
51 {
52  int nConfLimit = 1000000;
53  Vec_Int_t * vCiIds, * vInit = NULL;
54  Cnf_Dat_t * pCnf;
55  sat_solver * pSat;
56  Aig_Obj_t * pObj;
57  int i, RetValue, * pModel;
58  // solve the SAT problem
59  pCnf = Cnf_DeriveSimpleForRetiming( p );
60  pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
61  if ( pSat == NULL )
62  {
63  Cnf_DataFree( pCnf );
64  return NULL;
65  }
66  RetValue = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
67  assert( RetValue != l_Undef );
68  // create counter-example
69  if ( RetValue == l_True )
70  {
71  // accumulate SAT variables of the CIs
72  vCiIds = Vec_IntAlloc( Aig_ManCiNum(p) );
73  Aig_ManForEachCi( p, pObj, i )
74  Vec_IntPush( vCiIds, pCnf->pVarNums[pObj->Id] );
75  // create the model
76  pModel = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize );
77  vInit = Vec_IntAllocArray( pModel, Aig_ManCiNum(p) );
78  Vec_IntFree( vCiIds );
79  }
80  sat_solver_delete( pSat );
81  Cnf_DataFree( pCnf );
82  return vInit;
83 }
84 
85 /**Function*************************************************************
86 
87  Synopsis [Uses UNSAT core to find the part of AIG to be excluded.]
88 
89  Description [Returns the number of the PO that appears in the UNSAT core.]
90 
91  SideEffects []
92 
93  SeeAlso []
94 
95 ***********************************************************************/
96 int Saig_ManRetimeUnsatCore( Aig_Man_t * p, int fVerbose )
97 {
98  int fVeryVerbose = 0;
99  int nConfLimit = 1000000;
100  void * pSatCnf = NULL;
101  Intp_Man_t * pManProof;
102  Vec_Int_t * vCore = NULL;
103  Cnf_Dat_t * pCnf;
104  sat_solver * pSat;
105  Aig_Obj_t * pObj;
106  int * pClause1, * pClause2, * pLit, * pVars;
107  int i, RetValue, iBadPo, iClause, nVars, nPos;
108  // create the SAT solver
109  pCnf = Cnf_DeriveSimpleForRetiming( p );
110  pSat = sat_solver_new();
111  sat_solver_store_alloc( pSat );
112  sat_solver_setnvars( pSat, pCnf->nVars );
113  for ( i = 0; i < pCnf->nClauses; i++ )
114  {
115  if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
116  {
117  Cnf_DataFree( pCnf );
118  sat_solver_delete( pSat );
119  return -1;
120  }
121  }
122  sat_solver_store_mark_roots( pSat );
123  // solve the problem
124  RetValue = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
125  assert( RetValue != l_Undef );
126  assert( RetValue == l_False );
127  pSatCnf = sat_solver_store_release( pSat );
128  sat_solver_delete( pSat );
129  // derive the UNSAT core
130  pManProof = Intp_ManAlloc();
131  vCore = (Vec_Int_t *)Intp_ManUnsatCore( pManProof, (Sto_Man_t *)pSatCnf, 0, fVeryVerbose );
132  Intp_ManFree( pManProof );
133  Sto_ManFree( (Sto_Man_t *)pSatCnf );
134  // derive the set of variables on which the core depends
135  // collect the variable numbers
136  nVars = 0;
137  pVars = ABC_ALLOC( int, pCnf->nVars );
138  memset( pVars, 0, sizeof(int) * pCnf->nVars );
139  Vec_IntForEachEntry( vCore, iClause, i )
140  {
141  pClause1 = pCnf->pClauses[iClause];
142  pClause2 = pCnf->pClauses[iClause+1];
143  for ( pLit = pClause1; pLit < pClause2; pLit++ )
144  {
145  if ( pVars[ (*pLit) >> 1 ] == 0 )
146  nVars++;
147  pVars[ (*pLit) >> 1 ] = 1;
148  if ( fVeryVerbose )
149  printf( "%s%d ", ((*pLit) & 1)? "-" : "+", (*pLit) >> 1 );
150  }
151  if ( fVeryVerbose )
152  printf( "\n" );
153  }
154  // collect the nodes
155  if ( fVeryVerbose ) {
156  Aig_ManForEachObj( p, pObj, i )
157  if ( pCnf->pVarNums[pObj->Id] >= 0 && pVars[ pCnf->pVarNums[pObj->Id] ] == 1 )
158  {
159  Aig_ObjPrint( p, pObj );
160  printf( "\n" );
161  }
162  }
163  // pick the first PO in the list
164  nPos = 0;
165  iBadPo = -1;
166  Aig_ManForEachCo( p, pObj, i )
167  if ( pCnf->pVarNums[pObj->Id] >= 0 && pVars[ pCnf->pVarNums[pObj->Id] ] == 1 )
168  {
169  if ( iBadPo == -1 )
170  iBadPo = i;
171  nPos++;
172  }
173  if ( fVerbose )
174  printf( "UNSAT core: %d clauses, %d variables, %d POs. ", Vec_IntSize(vCore), nVars, nPos );
175  ABC_FREE( pVars );
176  Vec_IntFree( vCore );
177  Cnf_DataFree( pCnf );
178  return iBadPo;
179 }
180 
181 /**Function*************************************************************
182 
183  Synopsis [Marks the TFI cone with the current traversal ID.]
184 
185  Description []
186 
187  SideEffects []
188 
189  SeeAlso []
190 
191 ***********************************************************************/
192 void Saig_ManMarkCone_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
193 {
194  if ( pObj == NULL )
195  return;
196  if ( Aig_ObjIsTravIdCurrent( p, pObj ) )
197  return;
198  Aig_ObjSetTravIdCurrent( p, pObj );
199  Saig_ManMarkCone_rec( p, Aig_ObjFanin0(pObj) );
200  Saig_ManMarkCone_rec( p, Aig_ObjFanin1(pObj) );
201 }
202 
203 /**Function*************************************************************
204 
205  Synopsis [Counts the number of nodes to get registers after retiming.]
206 
207  Description []
208 
209  SideEffects []
210 
211  SeeAlso []
212 
213 ***********************************************************************/
214 int Saig_ManRetimeCountCut( Aig_Man_t * p, Vec_Ptr_t * vCut )
215 {
216  Vec_Ptr_t * vNodes;
217  Aig_Obj_t * pObj, * pFanin;
218  int i, RetValue;
219  // mark the cones
220  Aig_ManIncrementTravId( p );
221  Vec_PtrForEachEntry( Aig_Obj_t *, vCut, pObj, i )
222  Saig_ManMarkCone_rec( p, pObj );
223  // collect the new cut
224  vNodes = Vec_PtrAlloc( 1000 );
225  Aig_ManForEachObj( p, pObj, i )
226  {
227  if ( Aig_ObjIsTravIdCurrent(p, pObj) )
228  continue;
229  pFanin = Aig_ObjFanin0( pObj );
230  if ( pFanin && !pFanin->fMarkA && Aig_ObjIsTravIdCurrent(p, pFanin) )
231  {
232  Vec_PtrPush( vNodes, pFanin );
233  pFanin->fMarkA = 1;
234  }
235  pFanin = Aig_ObjFanin1( pObj );
236  if ( pFanin && !pFanin->fMarkA && Aig_ObjIsTravIdCurrent(p, pFanin) )
237  {
238  Vec_PtrPush( vNodes, pFanin );
239  pFanin->fMarkA = 1;
240  }
241  }
242  Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
243  pObj->fMarkA = 0;
244  RetValue = Vec_PtrSize( vNodes );
245  Vec_PtrFree( vNodes );
246  return RetValue;
247 }
248 
249 /**Function*************************************************************
250 
251  Synopsis [Duplicates the AIG recursively.]
252 
253  Description []
254 
255  SideEffects []
256 
257  SeeAlso []
258 
259 ***********************************************************************/
260 void Saig_ManRetimeDup_rec( Aig_Man_t * pNew, Aig_Obj_t * pObj )
261 {
262  if ( pObj->pData )
263  return;
264  assert( Aig_ObjIsNode(pObj) );
265  Saig_ManRetimeDup_rec( pNew, Aig_ObjFanin0(pObj) );
266  Saig_ManRetimeDup_rec( pNew, Aig_ObjFanin1(pObj) );
267  pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
268 }
269 
270 /**Function*************************************************************
271 
272  Synopsis [Duplicates the AIG while retiming the registers to the cut.]
273 
274  Description []
275 
276  SideEffects []
277 
278  SeeAlso []
279 
280 ***********************************************************************/
281 Aig_Man_t * Saig_ManRetimeDupForward( Aig_Man_t * p, Vec_Ptr_t * vCut )
282 {
283  Aig_Man_t * pNew;
284  Aig_Obj_t * pObj, * pObjLi, * pObjLo;
285  int i;
286  // mark the cones under the cut
287 // assert( Vec_PtrSize(vCut) == Saig_ManRetimeCountCut(p, vCut) );
288  // create the new manager
289  pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
290  pNew->pName = Abc_UtilStrsav( p->pName );
291  pNew->pSpec = Abc_UtilStrsav( p->pSpec );
292  pNew->nRegs = Vec_PtrSize(vCut);
293  pNew->nTruePis = p->nTruePis;
294  pNew->nTruePos = p->nTruePos;
295  // create the true PIs
296  Aig_ManCleanData( p );
297  Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
298  Saig_ManForEachPi( p, pObj, i )
299  pObj->pData = Aig_ObjCreateCi( pNew );
300  // create the registers
301  Vec_PtrForEachEntry( Aig_Obj_t *, vCut, pObj, i )
302  pObj->pData = Aig_NotCond( Aig_ObjCreateCi(pNew), pObj->fPhase );
303  // duplicate logic above the cut
304  Aig_ManForEachCo( p, pObj, i )
305  Saig_ManRetimeDup_rec( pNew, Aig_ObjFanin0(pObj) );
306  // create the true POs
307  Saig_ManForEachPo( p, pObj, i )
308  Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
309  // remember value in LI
310  Saig_ManForEachLi( p, pObj, i )
311  pObj->pData = Aig_ObjChild0Copy(pObj);
312  // transfer values from the LIs to the LOs
313  Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
314  pObjLo->pData = pObjLi->pData;
315  // erase the data values on the internal nodes of the cut
316  Vec_PtrForEachEntry( Aig_Obj_t *, vCut, pObj, i )
317  if ( Aig_ObjIsNode(pObj) )
318  pObj->pData = NULL;
319  // duplicate logic below the cut
320  Vec_PtrForEachEntry( Aig_Obj_t *, vCut, pObj, i )
321  {
322  Saig_ManRetimeDup_rec( pNew, pObj );
323  Aig_ObjCreateCo( pNew, Aig_NotCond((Aig_Obj_t *)pObj->pData, pObj->fPhase) );
324  }
325  Aig_ManCleanup( pNew );
326  return pNew;
327 }
328 
329 /**Function*************************************************************
330 
331  Synopsis [Duplicates the AIG while retiming the registers to the cut.]
332 
333  Description []
334 
335  SideEffects []
336 
337  SeeAlso []
338 
339 ***********************************************************************/
340 Aig_Man_t * Saig_ManRetimeDupBackward( Aig_Man_t * p, Vec_Ptr_t * vCut, Vec_Int_t * vInit )
341 {
342  Aig_Man_t * pNew;
343  Aig_Obj_t * pObj, * pObjLi, * pObjLo;
344  int i;
345  // mark the cones under the cut
346 // assert( Vec_PtrSize(vCut) == Saig_ManRetimeCountCut(p, vCut) );
347  // create the new manager
348  pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
349  pNew->pName = Abc_UtilStrsav( p->pName );
350  pNew->pSpec = Abc_UtilStrsav( p->pSpec );
351  pNew->nRegs = Vec_PtrSize(vCut);
352  pNew->nTruePis = p->nTruePis;
353  pNew->nTruePos = p->nTruePos;
354  // create the true PIs
355  Aig_ManCleanData( p );
356  Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
357  Saig_ManForEachPi( p, pObj, i )
358  pObj->pData = Aig_ObjCreateCi( pNew );
359  // create the registers
360  Vec_PtrForEachEntry( Aig_Obj_t *, vCut, pObj, i )
361  pObj->pData = Aig_NotCond( Aig_ObjCreateCi(pNew), vInit?Vec_IntEntry(vInit,i):0 );
362  // duplicate logic above the cut and remember values
363  Saig_ManForEachLi( p, pObj, i )
364  {
365  Saig_ManRetimeDup_rec( pNew, Aig_ObjFanin0(pObj) );
366  pObj->pData = Aig_ObjChild0Copy(pObj);
367  }
368  // transfer values from the LIs to the LOs
369  Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
370  pObjLo->pData = pObjLi->pData;
371  // erase the data values on the internal nodes of the cut
372  Vec_PtrForEachEntry( Aig_Obj_t *, vCut, pObj, i )
373  if ( Aig_ObjIsNode(pObj) )
374  pObj->pData = NULL;
375  // replicate the data on the constant node and the PIs
376  pObj = Aig_ManConst1(p);
377  pObj->pData = Aig_ManConst1(pNew);
378  Saig_ManForEachPi( p, pObj, i )
379  pObj->pData = Aig_ManCi( pNew, i );
380  // duplicate logic below the cut
381  Saig_ManForEachPo( p, pObj, i )
382  {
383  Saig_ManRetimeDup_rec( pNew, Aig_ObjFanin0(pObj) );
384  Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
385  }
386  Vec_PtrForEachEntry( Aig_Obj_t *, vCut, pObj, i )
387  {
388  Saig_ManRetimeDup_rec( pNew, pObj );
389  Aig_ObjCreateCo( pNew, Aig_NotCond((Aig_Obj_t *)pObj->pData, vInit?Vec_IntEntry(vInit,i):0) );
390  }
391  Aig_ManCleanup( pNew );
392  return pNew;
393 }
394 
395 /**Function*************************************************************
396 
397  Synopsis [Derives AIG for the initial state computation.]
398 
399  Description []
400 
401  SideEffects []
402 
403  SeeAlso []
404 
405 ***********************************************************************/
406 Aig_Man_t * Saig_ManRetimeDupInitState( Aig_Man_t * p, Vec_Ptr_t * vCut )
407 {
408  Aig_Man_t * pNew;
409  Aig_Obj_t * pObj;
410  int i;
411  // mark the cones under the cut
412 // assert( Vec_PtrSize(vCut) == Saig_ManRetimeCountCut(p, vCut) );
413  // create the new manager
414  pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
415  // create the true PIs
416  Aig_ManCleanData( p );
417  Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
418  // create the registers
419  Vec_PtrForEachEntry( Aig_Obj_t *, vCut, pObj, i )
420  pObj->pData = Aig_ObjCreateCi(pNew);
421  // duplicate logic above the cut and create POs
422  Saig_ManForEachLi( p, pObj, i )
423  {
424  Saig_ManRetimeDup_rec( pNew, Aig_ObjFanin0(pObj) );
425  Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
426  }
427  return pNew;
428 }
429 
430 /**Function*************************************************************
431 
432  Synopsis [Returns the array of bad registers.]
433 
434  Description []
435 
436  SideEffects []
437 
438  SeeAlso []
439 
440 ***********************************************************************/
441 Vec_Ptr_t * Saig_ManGetRegistersToExclude( Aig_Man_t * p )
442 {
443  Vec_Ptr_t * vNodes;
444  Aig_Obj_t * pObj, * pFanin;
445  int i, Diffs;
446  assert( Saig_ManRegNum(p) > 0 );
447  Saig_ManForEachLi( p, pObj, i )
448  {
449  pFanin = Aig_ObjFanin0(pObj);
450  if ( !Aig_ObjFaninC0(pObj) )
451  pFanin->fMarkA = 1;
452  else
453  pFanin->fMarkB = 1;
454  }
455  Diffs = 0;
456  Saig_ManForEachLi( p, pObj, i )
457  {
458  pFanin = Aig_ObjFanin0(pObj);
459  Diffs += pFanin->fMarkA && pFanin->fMarkB;
460  }
461  vNodes = Vec_PtrAlloc( 100 );
462  if ( Diffs > 0 )
463  {
464  Saig_ManForEachLi( p, pObj, i )
465  {
466  pFanin = Aig_ObjFanin0(pObj);
467  if ( pFanin->fMarkA && pFanin->fMarkB )
468  Vec_PtrPush( vNodes, pObj );
469  }
470  assert( Vec_PtrSize(vNodes) == Diffs );
471  }
472  Saig_ManForEachLi( p, pObj, i )
473  {
474  pFanin = Aig_ObjFanin0(pObj);
475  pFanin->fMarkA = pFanin->fMarkB = 0;
476  }
477  return vNodes;
478 }
479 
480 /**Function*************************************************************
481 
482  Synopsis [Hides the registers that cannot be backward retimed.]
483 
484  Description []
485 
486  SideEffects []
487 
488  SeeAlso []
489 
490 ***********************************************************************/
491 int Saig_ManHideBadRegs( Aig_Man_t * p, Vec_Ptr_t * vBadRegs )
492 {
493  Vec_Ptr_t * vPisNew, * vPosNew;
494  Aig_Obj_t * pObjLi, * pObjLo;
495  int nTruePi, nTruePo, nBadRegs, i;
496  if ( Vec_PtrSize(vBadRegs) == 0 )
497  return 0;
498  // attached LOs to LIs
499  Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
500  pObjLi->pData = pObjLo;
501  // reorder them by putting bad registers first
502  vPisNew = Vec_PtrDup( p->vCis );
503  vPosNew = Vec_PtrDup( p->vCos );
504  nTruePi = Aig_ManCiNum(p) - Aig_ManRegNum(p);
505  nTruePo = Aig_ManCoNum(p) - Aig_ManRegNum(p);
506  assert( nTruePi == p->nTruePis );
507  assert( nTruePo == p->nTruePos );
508  Vec_PtrForEachEntry( Aig_Obj_t *, vBadRegs, pObjLi, i )
509  {
510  Vec_PtrWriteEntry( vPisNew, nTruePi++, pObjLi->pData );
511  Vec_PtrWriteEntry( vPosNew, nTruePo++, pObjLi );
512  pObjLi->fMarkA = 1;
513  }
514  Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
515  {
516  if ( pObjLi->fMarkA )
517  {
518  pObjLi->fMarkA = 0;
519  continue;
520  }
521  Vec_PtrWriteEntry( vPisNew, nTruePi++, pObjLo );
522  Vec_PtrWriteEntry( vPosNew, nTruePo++, pObjLi );
523  }
524  // check the sizes
525  assert( nTruePi == Aig_ManCiNum(p) );
526  assert( nTruePo == Aig_ManCoNum(p) );
527  // transfer the arrays
528  Vec_PtrFree( p->vCis ); p->vCis = vPisNew;
529  Vec_PtrFree( p->vCos ); p->vCos = vPosNew;
530  // update the PIs
531  nBadRegs = Vec_PtrSize(vBadRegs);
532  p->nRegs -= nBadRegs;
533  p->nTruePis += nBadRegs;
534  p->nTruePos += nBadRegs;
535  return nBadRegs;
536 }
537 
538 /**Function*************************************************************
539 
540  Synopsis [Exposes bad registers.]
541 
542  Description []
543 
544  SideEffects []
545 
546  SeeAlso []
547 
548 ***********************************************************************/
549 void Saig_ManExposeBadRegs( Aig_Man_t * p, int nBadRegs )
550 {
551  p->nRegs += nBadRegs;
552  p->nTruePis -= nBadRegs;
553  p->nTruePos -= nBadRegs;
554 }
555 
556 /**Function*************************************************************
557 
558  Synopsis [Performs min-area retiming backward with initial state.]
559 
560  Description []
561 
562  SideEffects []
563 
564  SeeAlso []
565 
566 ***********************************************************************/
567 Aig_Man_t * Saig_ManRetimeMinAreaBackward( Aig_Man_t * pNew, int fVerbose )
568 {
569  Aig_Man_t * pInit, * pFinal;
570  Vec_Ptr_t * vBadRegs, * vCut;
571  Vec_Int_t * vInit;
572  int iBadReg;
573  // transform the AIG to have no bad registers
574  vBadRegs = Saig_ManGetRegistersToExclude( pNew );
575  if ( fVerbose && Vec_PtrSize(vBadRegs) )
576  printf( "Excluding %d registers that cannot be backward retimed.\n", Vec_PtrSize(vBadRegs) );
577  while ( 1 )
578  {
579  Saig_ManHideBadRegs( pNew, vBadRegs );
580  Vec_PtrFree( vBadRegs );
581  // compute cut
582  vCut = Nwk_ManDeriveRetimingCut( pNew, 0, fVerbose );
583  if ( Vec_PtrSize(vCut) >= Aig_ManRegNum(pNew) )
584  {
585  Vec_PtrFree( vCut );
586  return NULL;
587  }
588  // derive the initial state
589  pInit = Saig_ManRetimeDupInitState( pNew, vCut );
590  vInit = Saig_ManRetimeInitState( pInit );
591  if ( vInit != NULL )
592  {
593  pFinal = Saig_ManRetimeDupBackward( pNew, vCut, vInit );
594  Vec_IntFree( vInit );
595  Vec_PtrFree( vCut );
596  Aig_ManStop( pInit );
597  return pFinal;
598  }
599  Vec_PtrFree( vCut );
600  // there is no initial state - find the offending output
601  iBadReg = Saig_ManRetimeUnsatCore( pInit, fVerbose );
602  Aig_ManStop( pInit );
603  if ( fVerbose )
604  printf( "Excluding register %d.\n", iBadReg );
605  // prepare to remove this output
606  vBadRegs = Vec_PtrAlloc( 1 );
607  Vec_PtrPush( vBadRegs, Aig_ManCo( pNew, Saig_ManPoNum(pNew) + iBadReg ) );
608  }
609  return NULL;
610 }
611 
612 /**Function*************************************************************
613 
614  Synopsis [Performs min-area retiming.]
615 
616  Description []
617 
618  SideEffects []
619 
620  SeeAlso []
621 
622 ***********************************************************************/
623 Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose )
624 {
625  Vec_Ptr_t * vCut;
626  Aig_Man_t * pNew, * pTemp, * pCopy;
627  int i, fChanges;
628  pNew = Aig_ManDupSimple( p );
629  // perform several iterations of forward retiming
630  fChanges = 0;
631  if ( !fBackwardOnly )
632  for ( i = 0; i < nMaxIters; i++ )
633  {
634  if ( Saig_ManRegNum(pNew) == 0 )
635  break;
636  vCut = Nwk_ManDeriveRetimingCut( pNew, 1, fVerbose );
637  if ( Vec_PtrSize(vCut) >= Aig_ManRegNum(pNew) )
638  {
639  if ( fVerbose && !fChanges )
640  printf( "Forward retiming cannot reduce registers.\n" );
641  Vec_PtrFree( vCut );
642  break;
643  }
644  pNew = Saig_ManRetimeDupForward( pTemp = pNew, vCut );
645  Aig_ManStop( pTemp );
646  Vec_PtrFree( vCut );
647  if ( fVerbose )
648  Aig_ManReportImprovement( p, pNew );
649  fChanges = 1;
650  }
651  // perform several iterations of backward retiming
652  fChanges = 0;
653  if ( !fForwardOnly && !fInitial )
654  for ( i = 0; i < nMaxIters; i++ )
655  {
656  if ( Saig_ManRegNum(pNew) == 0 )
657  break;
658  vCut = Nwk_ManDeriveRetimingCut( pNew, 0, fVerbose );
659  if ( Vec_PtrSize(vCut) >= Aig_ManRegNum(pNew) )
660  {
661  if ( fVerbose && !fChanges )
662  printf( "Backward retiming cannot reduce registers.\n" );
663  Vec_PtrFree( vCut );
664  break;
665  }
666  pNew = Saig_ManRetimeDupBackward( pTemp = pNew, vCut, NULL );
667  Aig_ManStop( pTemp );
668  Vec_PtrFree( vCut );
669  if ( fVerbose )
670  Aig_ManReportImprovement( p, pNew );
671  fChanges = 1;
672  }
673  else if ( !fForwardOnly && fInitial )
674  for ( i = 0; i < nMaxIters; i++ )
675  {
676  if ( Saig_ManRegNum(pNew) == 0 )
677  break;
678  pCopy = Aig_ManDupSimple( pNew );
679  pTemp = Saig_ManRetimeMinAreaBackward( pCopy, fVerbose );
680  Aig_ManStop( pCopy );
681  if ( pTemp == NULL )
682  {
683  if ( fVerbose && !fChanges )
684  printf( "Backward retiming cannot reduce registers.\n" );
685  break;
686  }
687  Saig_ManExposeBadRegs( pTemp, Saig_ManPoNum(pTemp) - Saig_ManPoNum(pNew) );
688  Aig_ManStop( pNew );
689  pNew = pTemp;
690  if ( fVerbose )
691  Aig_ManReportImprovement( p, pNew );
692  fChanges = 1;
693  }
694  if ( !fForwardOnly && !fInitial && fChanges )
695  printf( "Assuming const-0 init-state after backward retiming. Result will not verify.\n" );
696  return pNew;
697 }
698 
699 ////////////////////////////////////////////////////////////////////////
700 /// END OF FILE ///
701 ////////////////////////////////////////////////////////////////////////
702 
703 
704 ABC_NAMESPACE_IMPL_END
705 
memset
char * memset()
Aig_ObjCreateCo
Aig_Obj_t * Aig_ObjCreateCo(Aig_Man_t *p, Aig_Obj_t *pDriver)
Definition: aigObj.c:66
Saig_ManRetimeDup_rec
void Saig_ManRetimeDup_rec(Aig_Man_t *pNew, Aig_Obj_t *pObj)
Definition: saigRetMin.c:260
Intp_ManUnsatCore
void * Intp_ManUnsatCore(Intp_Man_t *p, Sto_Man_t *pCnf, int fLearned, int fVerbose)
Definition: satInterP.c:963
Intp_Man_t_
Definition: satInterP.c:40
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Sto_Man_t_
Definition: satStore.h:82
Saig_ManPoNum
static int Saig_ManPoNum(Aig_Man_t *p)
Definition: saig.h:74
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
sat_solver_addclause
int sat_solver_addclause(sat_solver *s, lit *begin, lit *end)
Definition: satSolver.c:1492
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Aig_ManStop
void Aig_ManStop(Aig_Man_t *p)
Definition: aigMan.c:187
Saig_ManGetRegistersToExclude
Vec_Ptr_t * Saig_ManGetRegistersToExclude(Aig_Man_t *p)
Definition: saigRetMin.c:441
l_Undef
#define l_Undef
Definition: SolverTypes.h:86
Aig_ObjIsTravIdCurrent
static int Aig_ObjIsTravIdCurrent(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:295
Saig_ManForEachLiLo
#define Saig_ManForEachLiLo(p, pObjLi, pObjLo, i)
Definition: saig.h:101
Cnf_Dat_t_::nClauses
int nClauses
Definition: cnf.h:61
Aig_Obj_t_::fMarkB
unsigned int fMarkB
Definition: aig.h:80
Vec_IntAllocArray
static Vec_Int_t * Vec_IntAllocArray(int *pArray, int nSize)
Definition: bblif.c:214
sat_solver_solve
int sat_solver_solve(sat_solver *s, lit *begin, lit *end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
Definition: satSolver.c:1700
Aig_Obj_t_::pData
void * pData
Definition: aig.h:87
Saig_ManRetimeDupInitState
Aig_Man_t * Saig_ManRetimeDupInitState(Aig_Man_t *p, Vec_Ptr_t *vCut)
Definition: saigRetMin.c:406
Saig_ManRetimeDupForward
Aig_Man_t * Saig_ManRetimeDupForward(Aig_Man_t *p, Vec_Ptr_t *vCut)
Definition: saigRetMin.c:281
Cnf_Dat_t_::nVars
int nVars
Definition: cnf.h:59
sat_solver_delete
void sat_solver_delete(sat_solver *s)
Definition: satSolver.c:1141
Aig_ObjFanin0
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
Aig_ManStart
Aig_Man_t * Aig_ManStart(int nNodesMax)
DECLARATIONS ///.
Definition: aigMan.c:47
sat_solver_store_release
void * sat_solver_store_release(sat_solver *s)
Definition: satSolver.c:1949
Aig_ManForEachCi
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition: aig.h:393
Cnf_Dat_t_::pVarNums
int * pVarNums
Definition: cnf.h:63
Aig_ObjCreateCi
Aig_Obj_t * Aig_ObjCreateCi(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigObj.c:45
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
Aig_Obj_t_::fMarkA
unsigned int fMarkA
Definition: aig.h:79
l_True
#define l_True
Definition: SolverTypes.h:84
Aig_ManForEachCo
#define Aig_ManForEachCo(p, pObj, i)
Definition: aig.h:398
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Vec_PtrDup
static Vec_Ptr_t * Vec_PtrDup(Vec_Ptr_t *pVec)
Definition: vecPtr.h:169
Aig_ObjFanin1
static Aig_Obj_t * Aig_ObjFanin1(Aig_Obj_t *pObj)
Definition: aig.h:309
Cnf_DeriveSimpleForRetiming
Cnf_Dat_t * Cnf_DeriveSimpleForRetiming(Aig_Man_t *p)
Definition: cnfWrite.c:709
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Cnf_Dat_t_
Definition: cnf.h:56
Saig_ManRetimeUnsatCore
int Saig_ManRetimeUnsatCore(Aig_Man_t *p, int fVerbose)
Definition: saigRetMin.c:96
Aig_ObjSetTravIdCurrent
static void Aig_ObjSetTravIdCurrent(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:293
Aig_And
Aig_Obj_t * Aig_And(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:104
Intp_ManAlloc
Intp_Man_t * Intp_ManAlloc()
FUNCTION DEFINITIONS ///.
Definition: satInterP.c:96
Aig_ObjPrint
void Aig_ObjPrint(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aigObj.c:316
Aig_ManIncrementTravId
void Aig_ManIncrementTravId(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigUtil.c:44
Aig_ObjIsNode
static int Aig_ObjIsNode(Aig_Obj_t *pObj)
Definition: aig.h:280
Intp_ManFree
void Intp_ManFree(Intp_Man_t *p)
Definition: satInterP.c:178
Saig_ManRetimeCountCut
int Saig_ManRetimeCountCut(Aig_Man_t *p, Vec_Ptr_t *vCut)
Definition: saigRetMin.c:214
Aig_ManCoNum
static int Aig_ManCoNum(Aig_Man_t *p)
Definition: aig.h:252
Cnf_Dat_t_::pClauses
int ** pClauses
Definition: cnf.h:62
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Saig_ManForEachLi
#define Saig_ManForEachLi(p, pObj, i)
Definition: saig.h:98
Saig_ManRetimeMinArea
Aig_Man_t * Saig_ManRetimeMinArea(Aig_Man_t *p, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose)
Definition: saigRetMin.c:623
Aig_ManReportImprovement
void Aig_ManReportImprovement(Aig_Man_t *p, Aig_Man_t *pNew)
Definition: aigMan.c:415
Aig_ManCi
static Aig_Obj_t * Aig_ManCi(Aig_Man_t *p, int i)
Definition: aig.h:266
sat_solver_store_alloc
void sat_solver_store_alloc(sat_solver *s)
Definition: satSolver.c:1916
sat_solver_setnvars
void sat_solver_setnvars(sat_solver *s, int n)
Definition: satSolver.c:1072
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
Aig_ManCiNum
static int Aig_ManCiNum(Aig_Man_t *p)
Definition: aig.h:251
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Saig_ManRetimeDupBackward
Aig_Man_t * Saig_ManRetimeDupBackward(Aig_Man_t *p, Vec_Ptr_t *vCut, Vec_Int_t *vInit)
Definition: saigRetMin.c:340
Aig_ObjChild1Copy
static Aig_Obj_t * Aig_ObjChild1Copy(Aig_Obj_t *pObj)
Definition: aig.h:313
Aig_Obj_t_
Definition: aig.h:69
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Nwk_ManDeriveRetimingCut
ABC_DLL Vec_Ptr_t * Nwk_ManDeriveRetimingCut(Aig_Man_t *p, int fForward, int fVerbose)
FUNCTION DECLARATIONS ///.
Definition: nwkAig.c:85
Aig_ObjChild0Copy
static Aig_Obj_t * Aig_ObjChild0Copy(Aig_Obj_t *pObj)
Definition: aig.h:312
Saig_ManMarkCone_rec
void Saig_ManMarkCone_rec(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saigRetMin.c:192
Aig_ObjFaninC0
static int Aig_ObjFaninC0(Aig_Obj_t *pObj)
Definition: aig.h:306
Saig_ManRegNum
static int Saig_ManRegNum(Aig_Man_t *p)
Definition: saig.h:77
Vec_PtrWriteEntry
static void Vec_PtrWriteEntry(Vec_Ptr_t *p, int i, void *Entry)
Definition: vecPtr.h:396
Aig_ManObjNumMax
static int Aig_ManObjNumMax(Aig_Man_t *p)
Definition: aig.h:259
Aig_ManConst1
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Aig_ManCo
static Aig_Obj_t * Aig_ManCo(Aig_Man_t *p, int i)
Definition: aig.h:267
sat_solver_store_mark_roots
void sat_solver_store_mark_roots(sat_solver *s)
Definition: satSolver.c:1939
Aig_ManRegNum
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
sat_solver_new
sat_solver * sat_solver_new(void)
Definition: satSolver.c:1001
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Aig_Obj_t_::fPhase
unsigned int fPhase
Definition: aig.h:78
Cnf_DataWriteIntoSolver
void * Cnf_DataWriteIntoSolver(Cnf_Dat_t *p, int nFrames, int fInit)
Definition: cnfMan.c:463
Aig_ManForEachObj
#define Aig_ManForEachObj(p, pObj, i)
Definition: aig.h:403
Vec_PtrAlloc
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
Sto_ManFree
void Sto_ManFree(Sto_Man_t *p)
Definition: satStore.c:143
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Saig_ManHideBadRegs
int Saig_ManHideBadRegs(Aig_Man_t *p, Vec_Ptr_t *vBadRegs)
Definition: saigRetMin.c:491
l_False
#define l_False
Definition: SolverTypes.h:85
Saig_ManExposeBadRegs
void Saig_ManExposeBadRegs(Aig_Man_t *p, int nBadRegs)
Definition: saigRetMin.c:549
Cnf_DataFree
void Cnf_DataFree(Cnf_Dat_t *p)
Definition: cnfMan.c:180
Saig_ManRetimeMinAreaBackward
Aig_Man_t * Saig_ManRetimeMinAreaBackward(Aig_Man_t *pNew, int fVerbose)
Definition: saigRetMin.c:567
Saig_ManRetimeInitState
ABC_NAMESPACE_IMPL_START Vec_Int_t * Saig_ManRetimeInitState(Aig_Man_t *p)
DECLARATIONS ///.
Definition: saigRetMin.c:50
sat_solver_t
Definition: satSolver.h:91
Saig_ManForEachPo
#define Saig_ManForEachPo(p, pObj, i)
Definition: saig.h:93
assert
#define assert(ex)
Definition: util_old.h:213
Aig_NotCond
static Aig_Obj_t * Aig_NotCond(Aig_Obj_t *p, int c)
Definition: aig.h:248
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
Abc_UtilStrsav
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Aig_ManCleanData
void Aig_ManCleanData(Aig_Man_t *p)
Definition: aigUtil.c:205
Aig_Obj_t_::Id
int Id
Definition: aig.h:85
Aig_ManCleanup
int Aig_ManCleanup(Aig_Man_t *p)
Definition: aigMan.c:265
Aig_ManDupSimple
Aig_Man_t * Aig_ManDupSimple(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigDup.c:46
Sat_SolverGetModel
int * Sat_SolverGetModel(sat_solver *p, int *pVars, int nVars)
Definition: satUtil.c:266
Vec_PtrFree
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
Saig_ManForEachPi
#define Saig_ManForEachPi(p, pObj, i)
Definition: saig.h:91