abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
giaTim.c File Reference
#include "gia.h"
#include "giaAig.h"
#include "misc/tim/tim.h"
#include "proof/cec/cec.h"
#include "proof/fra/fra.h"

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START int Gia_ManBoxNum (Gia_Man_t *p)
 DECLARATIONS ///. More...
 
int Gia_ManRegBoxNum (Gia_Man_t *p)
 
int Gia_ManNonRegBoxNum (Gia_Man_t *p)
 
int Gia_ManBoxCiNum (Gia_Man_t *p)
 
int Gia_ManBoxCoNum (Gia_Man_t *p)
 
int Gia_ManClockDomainNum (Gia_Man_t *p)
 
int Gia_ManIsSeqWithBoxes (Gia_Man_t *p)
 
int Gia_ManIsNormalized (Gia_Man_t *p)
 
Gia_Man_tGia_ManDupNormalize (Gia_Man_t *p)
 
Gia_Man_tGia_ManDupUnshuffleInputs (Gia_Man_t *p)
 
int Gia_ManOrderWithBoxes_rec (Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vNodes)
 
Vec_Int_tGia_ManOrderWithBoxes (Gia_Man_t *p)
 
Gia_Man_tGia_ManDupUnnormalize (Gia_Man_t *p)
 
void Gia_ManCleanupRemap (Gia_Man_t *p, Gia_Man_t *pGia)
 
int Gia_ManLevelWithBoxes_rec (Gia_Man_t *p, Gia_Obj_t *pObj)
 
int Gia_ManLevelWithBoxes (Gia_Man_t *p)
 
int Gia_ManLutLevelWithBoxes_rec (Gia_Man_t *p, Gia_Obj_t *pObj)
 
int Gia_ManLutLevelWithBoxes (Gia_Man_t *p)
 
void * Gia_ManUpdateTimMan (Gia_Man_t *p, Vec_Int_t *vBoxPres)
 
void * Gia_ManUpdateTimMan2 (Gia_Man_t *p, Vec_Int_t *vBoxesLeft, int nTermsDiff)
 
Gia_Man_tGia_ManUpdateExtraAig (void *pTime, Gia_Man_t *p, Vec_Int_t *vBoxPres)
 
Gia_Man_tGia_ManUpdateExtraAig2 (void *pTime, Gia_Man_t *p, Vec_Int_t *vBoxesLeft)
 
void Gia_ManDupCollapse_rec (Gia_Man_t *p, Gia_Obj_t *pObj, Gia_Man_t *pNew)
 
Gia_Man_tGia_ManDupCollapse (Gia_Man_t *p, Gia_Man_t *pBoxes, Vec_Int_t *vBoxPres, int fSeq)
 
int Gia_ManVerifyWithBoxes (Gia_Man_t *pGia, int nBTLimit, int nTimeLim, int fSeq, int fVerbose, char *pFileSpec)
 

Function Documentation

int Gia_ManBoxCiNum ( Gia_Man_t p)

Definition at line 61 of file giaTim.c.

62 {
63  return p->pManTime ? Gia_ManCiNum(p) - Tim_ManPiNum((Tim_Man_t *)p->pManTime) : 0;
64 }
int Tim_ManPiNum(Tim_Man_t *p)
Definition: timMan.c:688
void * pManTime
Definition: gia.h:165
static int Gia_ManCiNum(Gia_Man_t *p)
Definition: gia.h:383
typedefABC_NAMESPACE_HEADER_START struct Tim_Man_t_ Tim_Man_t
INCLUDES ///.
Definition: tim.h:92
int Gia_ManBoxCoNum ( Gia_Man_t p)

Definition at line 65 of file giaTim.c.

66 {
67  return p->pManTime ? Gia_ManCoNum(p) - Tim_ManPoNum((Tim_Man_t *)p->pManTime) : 0;
68 }
void * pManTime
Definition: gia.h:165
typedefABC_NAMESPACE_HEADER_START struct Tim_Man_t_ Tim_Man_t
INCLUDES ///.
Definition: tim.h:92
int Tim_ManPoNum(Tim_Man_t *p)
Definition: timMan.c:694
static int Gia_ManCoNum(Gia_Man_t *p)
Definition: gia.h:384
ABC_NAMESPACE_IMPL_START int Gia_ManBoxNum ( Gia_Man_t p)

DECLARATIONS ///.

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

FileName [giaTim.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Scalable AIG package.]

Synopsis [Procedures with hierarchy/timing manager.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id:
giaTim.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

]FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [Returns the number of boxes in the AIG with boxes.]

Description []

SideEffects []

SeeAlso []

Definition at line 49 of file giaTim.c.

50 {
51  return p->pManTime ? Tim_ManBoxNum((Tim_Man_t *)p->pManTime) : 0;
52 }
void * pManTime
Definition: gia.h:165
int Tim_ManBoxNum(Tim_Man_t *p)
Definition: timMan.c:702
typedefABC_NAMESPACE_HEADER_START struct Tim_Man_t_ Tim_Man_t
INCLUDES ///.
Definition: tim.h:92
void Gia_ManCleanupRemap ( Gia_Man_t p,
Gia_Man_t pGia 
)

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

Synopsis [Remaps the AIG from the old manager into the new manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 424 of file giaTim.c.

425 {
426  Gia_Obj_t * pObj, * pObjGia;
427  int i, iPrev;
428  Gia_ManForEachObj1( p, pObj, i )
429  {
430  iPrev = Gia_ObjValue(pObj);
431  if ( iPrev == ~0 )
432  continue;
433  pObjGia = Gia_ManObj( pGia, Abc_Lit2Var(iPrev) );
434  if ( pObjGia->Value == ~0 )
435  Gia_ObjSetValue( pObj, pObjGia->Value );
436  else
437  Gia_ObjSetValue( pObj, Abc_LitNotCond(pObjGia->Value, Abc_LitIsCompl(iPrev)) );
438  }
439 }
static void Gia_ObjSetValue(Gia_Obj_t *pObj, int i)
Definition: gia.h:414
static int Gia_ObjValue(Gia_Obj_t *pObj)
Definition: gia.h:413
static Gia_Obj_t * Gia_ManObj(Gia_Man_t *p, int v)
Definition: gia.h:402
static int Abc_LitNotCond(int Lit, int c)
Definition: abc_global.h:267
Definition: gia.h:75
static int Abc_LitIsCompl(int Lit)
Definition: abc_global.h:265
static int Abc_Lit2Var(int Lit)
Definition: abc_global.h:264
unsigned Value
Definition: gia.h:87
#define Gia_ManForEachObj1(p, pObj, i)
Definition: gia.h:986
int Gia_ManClockDomainNum ( Gia_Man_t p)

Definition at line 69 of file giaTim.c.

70 {
71  int i, nDoms, Count = 0;
72  if ( p->vRegClasses == NULL )
73  return 0;
74  nDoms = Vec_IntFindMax(p->vRegClasses);
75  assert( Vec_IntCountEntry(p->vRegClasses, 0) == 0 );
76  for ( i = 1; i <= nDoms; i++ )
77  if ( Vec_IntCountEntry(p->vRegClasses, i) > 0 )
78  Count++;
79  return Count;
80 }
static int Vec_IntCountEntry(Vec_Int_t *p, int Entry)
Definition: vecInt.h:1156
Vec_Int_t * vRegClasses
Definition: gia.h:144
static int Vec_IntFindMax(Vec_Int_t *p)
Definition: vecInt.h:996
#define assert(ex)
Definition: util_old.h:213
Gia_Man_t* Gia_ManDupCollapse ( Gia_Man_t p,
Gia_Man_t pBoxes,
Vec_Int_t vBoxPres,
int  fSeq 
)

Definition at line 748 of file giaTim.c.

749 {
750  // this procedure assumes that sequential AIG with boxes is unshuffled to have valid boxes
751  Tim_Man_t * pManTime = (Tim_Man_t *)p->pManTime;
752  Gia_Man_t * pNew, * pTemp;
753  Gia_Obj_t * pObj, * pObjBox;
754  int i, k, curCi, curCo;
755  assert( !fSeq || p->vRegClasses );
756  //assert( Gia_ManRegNum(p) == 0 );
757  assert( Gia_ManCiNum(p) == Tim_ManPiNum(pManTime) + Gia_ManCoNum(pBoxes) );
758  pNew = Gia_ManStart( Gia_ManObjNum(p) );
759  pNew->pName = Abc_UtilStrsav( p->pName );
760  pNew->pSpec = Abc_UtilStrsav( p->pSpec );
761  if ( Gia_ManHasChoices(p) )
762  pNew->pSibls = ABC_CALLOC( int, Gia_ManObjNum(p) );
763  Gia_ManHashAlloc( pNew );
764  // copy const and real PIs
765  Gia_ManFillValue( p );
766  Gia_ManConst0(p)->Value = 0;
769  for ( i = 0; i < Tim_ManPiNum(pManTime); i++ )
770  {
771  pObj = Gia_ManCi( p, i );
772  pObj->Value = Gia_ManAppendCi(pNew);
773  Gia_ObjSetTravIdCurrent( p, pObj );
774  }
775  // create logic for each box
776  curCi = Tim_ManPiNum(pManTime);
777  curCo = 0;
778  for ( i = 0; i < Tim_ManBoxNum(pManTime); i++ )
779  {
780  // clean boxes
781  Gia_ManIncrementTravId( pBoxes );
782  Gia_ObjSetTravIdCurrent( pBoxes, Gia_ManConst0(pBoxes) );
783  Gia_ManConst0(pBoxes)->Value = 0;
784  // add internal nodes
785  if ( Tim_ManBoxIsBlack(pManTime, i) )
786  {
787  int fSkip = (vBoxPres != NULL && !Vec_IntEntry(vBoxPres, i));
788  for ( k = 0; k < Tim_ManBoxInputNum(pManTime, i); k++ )
789  {
790  pObj = Gia_ManCo( p, curCo + k );
791  Gia_ManDupCollapse_rec( p, Gia_ObjFanin0(pObj), pNew );
792  pObj->Value = fSkip ? -1 : Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
793  }
794  for ( k = 0; k < Tim_ManBoxOutputNum(pManTime, i); k++ )
795  {
796  pObj = Gia_ManCi( p, curCi + k );
797  pObj->Value = fSkip ? 0 : Gia_ManAppendCi(pNew);
798  Gia_ObjSetTravIdCurrent( p, pObj );
799  }
800  }
801  else
802  {
803  for ( k = 0; k < Tim_ManBoxInputNum(pManTime, i); k++ )
804  {
805  // build logic
806  pObj = Gia_ManCo( p, curCo + k );
807  Gia_ManDupCollapse_rec( p, Gia_ObjFanin0(pObj), pNew );
808  // transfer to the PI
809  pObjBox = Gia_ManCi( pBoxes, k );
810  pObjBox->Value = Gia_ObjFanin0Copy(pObj);
811  Gia_ObjSetTravIdCurrent( pBoxes, pObjBox );
812  }
813  for ( k = 0; k < Tim_ManBoxOutputNum(pManTime, i); k++ )
814  {
815  // build logic
816  pObjBox = Gia_ManCo( pBoxes, curCi - Tim_ManPiNum(pManTime) + k );
817  Gia_ManDupCollapse_rec( pBoxes, Gia_ObjFanin0(pObjBox), pNew );
818  // transfer to the PI
819  pObj = Gia_ManCi( p, curCi + k );
820  pObj->Value = Gia_ObjFanin0Copy(pObjBox);
821  Gia_ObjSetTravIdCurrent( p, pObj );
822  }
823  }
824  curCo += Tim_ManBoxInputNum(pManTime, i);
825  curCi += Tim_ManBoxOutputNum(pManTime, i);
826  }
827  // add remaining nodes
828  for ( i = Tim_ManCoNum(pManTime) - Tim_ManPoNum(pManTime); i < Tim_ManCoNum(pManTime); i++ )
829  {
830  pObj = Gia_ManCo( p, i );
831  Gia_ManDupCollapse_rec( p, Gia_ObjFanin0(pObj), pNew );
832  pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
833  }
834  curCo += Tim_ManPoNum(pManTime);
835  // verify counts
836  assert( curCi == Gia_ManCiNum(p) );
837  assert( curCo == Gia_ManCoNum(p) );
838  Gia_ManSetRegNum( pNew, (fSeq && p->vRegClasses) ? Vec_IntSize(p->vRegClasses) : Gia_ManRegNum(p) );
839  Gia_ManHashStop( pNew );
840  pNew = Gia_ManCleanup( pTemp = pNew );
841  Gia_ManCleanupRemap( p, pTemp );
842  Gia_ManStop( pTemp );
843  assert( Tim_ManPoNum(pManTime) == Gia_ManCoNum(pNew) );
844  assert( Tim_ManPiNum(pManTime) == Gia_ManCiNum(pNew) );
845  return pNew;
846 }
int Tim_ManCoNum(Tim_Man_t *p)
Definition: timMan.c:684
void Gia_ManDupCollapse_rec(Gia_Man_t *p, Gia_Obj_t *pObj, Gia_Man_t *pNew)
Definition: giaTim.c:733
void Gia_ManStop(Gia_Man_t *p)
Definition: giaMan.c:77
static Gia_Obj_t * Gia_ManCi(Gia_Man_t *p, int v)
Definition: gia.h:403
static int Gia_ManAppendCo(Gia_Man_t *p, int iLit0)
Definition: gia.h:703
Vec_Int_t * vRegClasses
Definition: gia.h:144
int * pSibls
Definition: gia.h:123
static int Gia_ManAppendCi(Gia_Man_t *p)
Definition: gia.h:583
int Tim_ManBoxOutputNum(Tim_Man_t *p, int iBox)
Definition: timBox.c:202
void Gia_ManSetRegNum(Gia_Man_t *p, int nRegs)
Definition: giaMan.c:628
void Gia_ManCleanupRemap(Gia_Man_t *p, Gia_Man_t *pGia)
Definition: giaTim.c:424
Definition: gia.h:75
static int Gia_ManHasChoices(Gia_Man_t *p)
Definition: gia.h:397
int Tim_ManPiNum(Tim_Man_t *p)
Definition: timMan.c:688
static Gia_Obj_t * Gia_ObjFanin0(Gia_Obj_t *pObj)
Definition: gia.h:454
char * pName
Definition: gia.h:97
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
static void Gia_ObjSetTravIdCurrent(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:531
char * pSpec
Definition: gia.h:98
Gia_Man_t * Gia_ManStart(int nObjsMax)
DECLARATIONS ///.
Definition: giaMan.c:52
void * pManTime
Definition: gia.h:165
void Gia_ManFillValue(Gia_Man_t *p)
Definition: giaUtil.c:328
int Tim_ManBoxNum(Tim_Man_t *p)
Definition: timMan.c:702
int Tim_ManBoxInputNum(Tim_Man_t *p, int iBox)
Definition: timBox.c:186
static int Gia_ObjFanin0Copy(Gia_Obj_t *pObj)
Definition: gia.h:481
static int Gia_ManCiNum(Gia_Man_t *p)
Definition: gia.h:383
int Tim_ManBoxIsBlack(Tim_Man_t *p, int iBox)
Definition: timBox.c:257
static Gia_Obj_t * Gia_ManCo(Gia_Man_t *p, int v)
Definition: gia.h:404
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Definition: gia.h:95
static Gia_Obj_t * Gia_ManConst0(Gia_Man_t *p)
Definition: gia.h:400
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
#define assert(ex)
Definition: util_old.h:213
unsigned Value
Definition: gia.h:87
typedefABC_NAMESPACE_HEADER_START struct Tim_Man_t_ Tim_Man_t
INCLUDES ///.
Definition: tim.h:92
void Gia_ManHashAlloc(Gia_Man_t *p)
Definition: giaHash.c:99
void Gia_ManIncrementTravId(Gia_Man_t *p)
Definition: giaUtil.c:149
Gia_Man_t * Gia_ManCleanup(Gia_Man_t *p)
Definition: giaScl.c:84
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
int Tim_ManPoNum(Tim_Man_t *p)
Definition: timMan.c:694
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
void Gia_ManHashStop(Gia_Man_t *p)
Definition: giaHash.c:142
static int Gia_ManCoNum(Gia_Man_t *p)
Definition: gia.h:384
static int Gia_ManRegNum(Gia_Man_t *p)
Definition: gia.h:387
void Gia_ManDupCollapse_rec ( Gia_Man_t p,
Gia_Obj_t pObj,
Gia_Man_t pNew 
)

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

Synopsis [Computes AIG with boxes.]

Description []

SideEffects []

SeeAlso []

Definition at line 733 of file giaTim.c.

734 {
735  if ( Gia_ObjIsTravIdCurrent(p, pObj) )
736  return;
737  Gia_ObjSetTravIdCurrent(p, pObj);
738  assert( Gia_ObjIsAnd(pObj) );
739  if ( Gia_ObjSibl(p, Gia_ObjId(p, pObj)) )
740  Gia_ManDupCollapse_rec( p, Gia_ObjSiblObj(p, Gia_ObjId(p, pObj)), pNew );
741  Gia_ManDupCollapse_rec( p, Gia_ObjFanin0(pObj), pNew );
742  Gia_ManDupCollapse_rec( p, Gia_ObjFanin1(pObj), pNew );
743 // assert( !~pObj->Value );
744  pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
745  if ( Gia_ObjSibl(p, Gia_ObjId(p, pObj)) )
746  pNew->pSibls[Abc_Lit2Var(pObj->Value)] = Abc_Lit2Var(Gia_ObjSiblObj(p, Gia_ObjId(p, pObj))->Value);
747 }
void Gia_ManDupCollapse_rec(Gia_Man_t *p, Gia_Obj_t *pObj, Gia_Man_t *pNew)
Definition: giaTim.c:733
static Gia_Obj_t * Gia_ObjSiblObj(Gia_Man_t *p, int Id)
Definition: gia.h:894
static int Gia_ObjIsTravIdCurrent(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:533
int * pSibls
Definition: gia.h:123
static int Gia_ObjSibl(Gia_Man_t *p, int Id)
Definition: gia.h:893
static Gia_Obj_t * Gia_ObjFanin0(Gia_Obj_t *pObj)
Definition: gia.h:454
static int Gia_ObjFanin1Copy(Gia_Obj_t *pObj)
Definition: gia.h:482
static void Gia_ObjSetTravIdCurrent(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:531
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:410
static int Gia_ObjFanin0Copy(Gia_Obj_t *pObj)
Definition: gia.h:481
static int Gia_ObjIsAnd(Gia_Obj_t *pObj)
Definition: gia.h:422
static int Abc_Lit2Var(int Lit)
Definition: abc_global.h:264
static Gia_Obj_t * Gia_ObjFanin1(Gia_Obj_t *pObj)
Definition: gia.h:455
#define assert(ex)
Definition: util_old.h:213
unsigned Value
Definition: gia.h:87
int Gia_ManHashAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition: giaHash.c:572
Gia_Man_t* Gia_ManDupNormalize ( Gia_Man_t p)

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

Synopsis [Duplicates AIG in the DFS order while putting CIs first.]

Description []

SideEffects []

SeeAlso []

Definition at line 134 of file giaTim.c.

135 {
136  Gia_Man_t * pNew;
137  Gia_Obj_t * pObj;
138  int i;
139  Gia_ManFillValue( p );
140  pNew = Gia_ManStart( Gia_ManObjNum(p) );
141  pNew->pName = Abc_UtilStrsav( p->pName );
142  pNew->pSpec = Abc_UtilStrsav( p->pSpec );
143  Gia_ManConst0(p)->Value = 0;
144  if ( !Gia_ManIsSeqWithBoxes(p) )
145  {
146  Gia_ManForEachCi( p, pObj, i )
147  pObj->Value = Gia_ManAppendCi(pNew);
148  }
149  else
150  {
151  // current CI order: PIs + FOs + NewCIs
152  // desired reorder: PIs + NewCIs + FOs
153  int nCIs = Tim_ManPiNum( (Tim_Man_t *)p->pManTime );
154  int nAll = Tim_ManCiNum( (Tim_Man_t *)p->pManTime );
155  int nPis = nCIs - Gia_ManRegNum(p);
156  assert( nAll == Gia_ManCiNum(p) );
157  assert( nPis > 0 );
158  // copy PIs first
159  for ( i = 0; i < nPis; i++ )
160  Gia_ManCi(p, i)->Value = Gia_ManAppendCi(pNew);
161  // copy new CIs second
162  for ( i = nCIs; i < nAll; i++ )
163  Gia_ManCi(p, i)->Value = Gia_ManAppendCi(pNew);
164  // copy flops last
165  for ( i = nCIs - Gia_ManRegNum(p); i < nCIs; i++ )
166  Gia_ManCi(p, i)->Value = Gia_ManAppendCi(pNew);
167  printf( "Warning: Shuffled CI order to be correct sequential AIG.\n" );
168  }
169  Gia_ManForEachAnd( p, pObj, i )
170  if ( Gia_ObjIsBuf(pObj) )
171  pObj->Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) );
172  else
173  pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
174  Gia_ManForEachCo( p, pObj, i )
175  pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
176  Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
177  pNew->nConstrs = p->nConstrs;
178  assert( Gia_ManIsNormalized(pNew) );
179  Gia_ManDupRemapEquiv( pNew, p );
180  return pNew;
181 }
static int Gia_ManAppendAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition: gia.h:592
#define Gia_ManForEachCo(p, pObj, i)
Definition: gia.h:1022
static Gia_Obj_t * Gia_ManCi(Gia_Man_t *p, int v)
Definition: gia.h:403
static int Gia_ManAppendCo(Gia_Man_t *p, int iLit0)
Definition: gia.h:703
static int Gia_ManAppendCi(Gia_Man_t *p)
Definition: gia.h:583
static int Gia_ObjIsBuf(Gia_Obj_t *pObj)
Definition: gia.h:427
void Gia_ManSetRegNum(Gia_Man_t *p, int nRegs)
Definition: giaMan.c:628
int Gia_ManIsNormalized(Gia_Man_t *p)
Definition: giaTim.c:109
Definition: gia.h:75
int Tim_ManPiNum(Tim_Man_t *p)
Definition: timMan.c:688
#define Gia_ManForEachCi(p, pObj, i)
Definition: gia.h:1016
int Gia_ManIsSeqWithBoxes(Gia_Man_t *p)
Definition: giaTim.c:93
char * pName
Definition: gia.h:97
static int Gia_ObjFanin1Copy(Gia_Obj_t *pObj)
Definition: gia.h:482
static int Gia_ManAppendBuf(Gia_Man_t *p, int iLit)
Definition: gia.h:694
int Tim_ManCiNum(Tim_Man_t *p)
Definition: timMan.c:680
if(last==0)
Definition: sparse_int.h:34
char * pSpec
Definition: gia.h:98
else
Definition: sparse_int.h:55
Gia_Man_t * Gia_ManStart(int nObjsMax)
DECLARATIONS ///.
Definition: giaMan.c:52
#define Gia_ManForEachAnd(p, pObj, i)
Definition: gia.h:1002
void * pManTime
Definition: gia.h:165
void Gia_ManFillValue(Gia_Man_t *p)
Definition: giaUtil.c:328
static int Gia_ObjFanin0Copy(Gia_Obj_t *pObj)
Definition: gia.h:481
static int Gia_ManCiNum(Gia_Man_t *p)
Definition: gia.h:383
Definition: gia.h:95
static Gia_Obj_t * Gia_ManConst0(Gia_Man_t *p)
Definition: gia.h:400
#define assert(ex)
Definition: util_old.h:213
unsigned Value
Definition: gia.h:87
typedefABC_NAMESPACE_HEADER_START struct Tim_Man_t_ Tim_Man_t
INCLUDES ///.
Definition: tim.h:92
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
void Gia_ManDupRemapEquiv(Gia_Man_t *pNew, Gia_Man_t *p)
DECLARATIONS ///.
Definition: giaDup.c:46
static int Gia_ManRegNum(Gia_Man_t *p)
Definition: gia.h:387
Gia_Man_t* Gia_ManDupUnnormalize ( Gia_Man_t p)

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

Synopsis [Duplicates AIG according to the timing manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 373 of file giaTim.c.

374 {
375  Vec_Int_t * vNodes;
376  Gia_Man_t * pNew;
377  Gia_Obj_t * pObj;
378  int i;
379  assert( !Gia_ManBufNum(p) );
380  vNodes = Gia_ManOrderWithBoxes( p );
381  if ( vNodes == NULL )
382  return NULL;
383  Gia_ManFillValue( p );
384  pNew = Gia_ManStart( Gia_ManObjNum(p) );
385  pNew->pName = Abc_UtilStrsav( p->pName );
386  pNew->pSpec = Abc_UtilStrsav( p->pSpec );
387  if ( Gia_ManHasChoices(p) )
388  pNew->pSibls = ABC_CALLOC( int, Gia_ManObjNum(p) );
389  Gia_ManForEachObjVec( vNodes, p, pObj, i )
390  {
391  if ( Gia_ObjIsBuf(pObj) )
392  pObj->Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) );
393  else if ( Gia_ObjIsAnd(pObj) )
394  {
395  pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
396  if ( Gia_ObjSibl(p, Gia_ObjId(p, pObj)) )
397  pNew->pSibls[Abc_Lit2Var(pObj->Value)] = Abc_Lit2Var(Gia_ObjSiblObj(p, Gia_ObjId(p, pObj))->Value);
398  }
399  else if ( Gia_ObjIsCi(pObj) )
400  pObj->Value = Gia_ManAppendCi( pNew );
401  else if ( Gia_ObjIsCo(pObj) )
402  pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
403  else if ( Gia_ObjIsConst0(pObj) )
404  pObj->Value = 0;
405  else assert( 0 );
406  }
407  Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
408  Vec_IntFree( vNodes );
409  return pNew;
410 }
static int Gia_ManAppendAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition: gia.h:592
Vec_Int_t * Gia_ManOrderWithBoxes(Gia_Man_t *p)
Definition: giaTim.c:277
static Gia_Obj_t * Gia_ObjSiblObj(Gia_Man_t *p, int Id)
Definition: gia.h:894
static int Gia_ManAppendCo(Gia_Man_t *p, int iLit0)
Definition: gia.h:703
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
int * pSibls
Definition: gia.h:123
static int Gia_ManAppendCi(Gia_Man_t *p)
Definition: gia.h:583
static int Gia_ObjIsConst0(Gia_Obj_t *pObj)
Definition: gia.h:430
static int Gia_ObjIsBuf(Gia_Obj_t *pObj)
Definition: gia.h:427
void Gia_ManSetRegNum(Gia_Man_t *p, int nRegs)
Definition: giaMan.c:628
Definition: gia.h:75
static int Gia_ManHasChoices(Gia_Man_t *p)
Definition: gia.h:397
static int Gia_ObjSibl(Gia_Man_t *p, int Id)
Definition: gia.h:893
char * pName
Definition: gia.h:97
static int Gia_ObjFanin1Copy(Gia_Obj_t *pObj)
Definition: gia.h:482
static int Gia_ManAppendBuf(Gia_Man_t *p, int iLit)
Definition: gia.h:694
char * pSpec
Definition: gia.h:98
Gia_Man_t * Gia_ManStart(int nObjsMax)
DECLARATIONS ///.
Definition: giaMan.c:52
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:410
void Gia_ManFillValue(Gia_Man_t *p)
Definition: giaUtil.c:328
static int Gia_ObjFanin0Copy(Gia_Obj_t *pObj)
Definition: gia.h:481
static int Gia_ObjIsCo(Gia_Obj_t *pObj)
Definition: gia.h:421
#define Gia_ManForEachObjVec(vVec, p, pObj, i)
Definition: gia.h:988
Definition: gia.h:95
static int Gia_ManBufNum(Gia_Man_t *p)
Definition: gia.h:392
static int Gia_ObjIsAnd(Gia_Obj_t *pObj)
Definition: gia.h:422
static int Abc_Lit2Var(int Lit)
Definition: abc_global.h:264
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
#define assert(ex)
Definition: util_old.h:213
unsigned Value
Definition: gia.h:87
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
static int Gia_ObjIsCi(Gia_Obj_t *pObj)
Definition: gia.h:420
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
static int Gia_ManRegNum(Gia_Man_t *p)
Definition: gia.h:387
Gia_Man_t* Gia_ManDupUnshuffleInputs ( Gia_Man_t p)

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

Synopsis [Reorders flops for sequential AIGs with boxes.]

Description []

SideEffects []

SeeAlso []

Definition at line 194 of file giaTim.c.

195 {
196  Gia_Man_t * pNew;
197  Gia_Obj_t * pObj;
198  int i, nCIs, nAll, nPis;
199  // sanity checks
202  Gia_ManFillValue( p );
203  pNew = Gia_ManStart( Gia_ManObjNum(p) );
204  pNew->pName = Abc_UtilStrsav( p->pName );
205  pNew->pSpec = Abc_UtilStrsav( p->pSpec );
206  Gia_ManConst0(p)->Value = 0;
207  // change input order
208  // desired reorder: PIs + NewCIs + FOs
209  // current CI order: PIs + FOs + NewCIs
210  nCIs = Tim_ManPiNum( (Tim_Man_t *)p->pManTime );
211  nAll = Tim_ManCiNum( (Tim_Man_t *)p->pManTime );
212  nPis = nCIs - Gia_ManRegNum(p);
213  assert( nAll == Gia_ManCiNum(p) );
214  assert( nPis > 0 );
215  // copy PIs first
216  for ( i = 0; i < nPis; i++ )
217  Gia_ManCi(p, i)->Value = Gia_ManAppendCi(pNew);
218  // copy flops second
219  for ( i = nAll - Gia_ManRegNum(p); i < nAll; i++ )
220  Gia_ManCi(p, i)->Value = Gia_ManAppendCi(pNew);
221  // copy new CIs last
222  for ( i = nPis; i < nAll - Gia_ManRegNum(p); i++ )
223  Gia_ManCi(p, i)->Value = Gia_ManAppendCi(pNew);
224  printf( "Warning: Unshuffled CI order to be correct AIG with boxes.\n" );
225  // other things
226  Gia_ManForEachAnd( p, pObj, i )
227  pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
228  Gia_ManForEachCo( p, pObj, i )
229  pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
230  Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
231  pNew->nConstrs = p->nConstrs;
232  assert( Gia_ManIsNormalized(pNew) );
233  Gia_ManDupRemapEquiv( pNew, p );
234  return pNew;
235 }
static int Gia_ManAppendAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition: gia.h:592
#define Gia_ManForEachCo(p, pObj, i)
Definition: gia.h:1022
static Gia_Obj_t * Gia_ManCi(Gia_Man_t *p, int v)
Definition: gia.h:403
static int Gia_ManAppendCo(Gia_Man_t *p, int iLit0)
Definition: gia.h:703
static int Gia_ManAppendCi(Gia_Man_t *p)
Definition: gia.h:583
void Gia_ManSetRegNum(Gia_Man_t *p, int nRegs)
Definition: giaMan.c:628
int Gia_ManIsNormalized(Gia_Man_t *p)
Definition: giaTim.c:109
Definition: gia.h:75
int Tim_ManPiNum(Tim_Man_t *p)
Definition: timMan.c:688
int Gia_ManIsSeqWithBoxes(Gia_Man_t *p)
Definition: giaTim.c:93
char * pName
Definition: gia.h:97
static int Gia_ObjFanin1Copy(Gia_Obj_t *pObj)
Definition: gia.h:482
int Tim_ManCiNum(Tim_Man_t *p)
Definition: timMan.c:680
char * pSpec
Definition: gia.h:98
Gia_Man_t * Gia_ManStart(int nObjsMax)
DECLARATIONS ///.
Definition: giaMan.c:52
#define Gia_ManForEachAnd(p, pObj, i)
Definition: gia.h:1002
void * pManTime
Definition: gia.h:165
void Gia_ManFillValue(Gia_Man_t *p)
Definition: giaUtil.c:328
static int Gia_ObjFanin0Copy(Gia_Obj_t *pObj)
Definition: gia.h:481
static int Gia_ManCiNum(Gia_Man_t *p)
Definition: gia.h:383
Definition: gia.h:95
static Gia_Obj_t * Gia_ManConst0(Gia_Man_t *p)
Definition: gia.h:400
#define assert(ex)
Definition: util_old.h:213
unsigned Value
Definition: gia.h:87
typedefABC_NAMESPACE_HEADER_START struct Tim_Man_t_ Tim_Man_t
INCLUDES ///.
Definition: tim.h:92
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
void Gia_ManDupRemapEquiv(Gia_Man_t *pNew, Gia_Man_t *p)
DECLARATIONS ///.
Definition: giaDup.c:46
static int Gia_ManRegNum(Gia_Man_t *p)
Definition: gia.h:387
int Gia_ManIsNormalized ( Gia_Man_t p)

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

Synopsis [Makes sure the manager is normalized.]

Description []

SideEffects []

SeeAlso []

Definition at line 109 of file giaTim.c.

110 {
111  int i, nOffset;
112  nOffset = 1;
113  for ( i = 0; i < Gia_ManCiNum(p); i++ )
114  if ( !Gia_ObjIsCi( Gia_ManObj(p, nOffset+i) ) )
115  return 0;
116  nOffset = 1 + Gia_ManCiNum(p) + Gia_ManAndNum(p);
117  for ( i = 0; i < Gia_ManCoNum(p); i++ )
118  if ( !Gia_ObjIsCo( Gia_ManObj(p, nOffset+i) ) )
119  return 0;
120  return 1;
121 }
static Gia_Obj_t * Gia_ManObj(Gia_Man_t *p, int v)
Definition: gia.h:402
static int Gia_ManAndNum(Gia_Man_t *p)
Definition: gia.h:389
static int Gia_ObjIsCo(Gia_Obj_t *pObj)
Definition: gia.h:421
static int Gia_ManCiNum(Gia_Man_t *p)
Definition: gia.h:383
static int Gia_ObjIsCi(Gia_Obj_t *pObj)
Definition: gia.h:420
static int Gia_ManCoNum(Gia_Man_t *p)
Definition: gia.h:384
int Gia_ManIsSeqWithBoxes ( Gia_Man_t p)

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

Synopsis [Returns one if this is a seq AIG with non-trivial boxes.]

Description []

SideEffects []

SeeAlso []

Definition at line 93 of file giaTim.c.

94 {
95  return (Gia_ManRegNum(p) > 0 && Gia_ManBoxNum(p) > 0);
96 }
ABC_NAMESPACE_IMPL_START int Gia_ManBoxNum(Gia_Man_t *p)
DECLARATIONS ///.
Definition: giaTim.c:49
static int Gia_ManRegNum(Gia_Man_t *p)
Definition: gia.h:387
int Gia_ManLevelWithBoxes ( Gia_Man_t p)

Definition at line 469 of file giaTim.c.

470 {
471  int nAnd2Delay = p->nAnd2Delay ? p->nAnd2Delay : 1;
472  Tim_Man_t * pManTime = (Tim_Man_t *)p->pManTime;
473  Gia_Obj_t * pObj, * pObjIn;
474  int i, k, j, curCi, curCo, LevelMax;
475  assert( Gia_ManRegNum(p) == 0 );
476  assert( Gia_ManBufNum(p) == 0 );
477  // copy const and real PIs
479  Gia_ObjSetLevel( p, Gia_ManConst0(p), 0 );
482  for ( i = 0; i < Tim_ManPiNum(pManTime); i++ )
483  {
484  pObj = Gia_ManCi( p, i );
485  Gia_ObjSetLevel( p, pObj, Tim_ManGetCiArrival(pManTime, i) / nAnd2Delay );
486  Gia_ObjSetTravIdCurrent( p, pObj );
487  }
488  // create logic for each box
489  curCi = Tim_ManPiNum(pManTime);
490  curCo = 0;
491  for ( i = 0; i < Tim_ManBoxNum(pManTime); i++ )
492  {
493  int nBoxInputs = Tim_ManBoxInputNum( pManTime, i );
494  int nBoxOutputs = Tim_ManBoxOutputNum( pManTime, i );
495  float * pDelayTable = Tim_ManBoxDelayTable( pManTime, i );
496  // compute level for TFI of box inputs
497  for ( k = 0; k < nBoxInputs; k++ )
498  {
499  pObj = Gia_ManCo( p, curCo + k );
500  if ( Gia_ManLevelWithBoxes_rec( p, Gia_ObjFanin0(pObj) ) )
501  {
502  printf( "Boxes are not in a topological order. Switching to level computation without boxes.\n" );
503  return Gia_ManLevelNum( p );
504  }
505  // set box input level
506  Gia_ObjSetCoLevel( p, pObj );
507  }
508  // compute level for box outputs
509  for ( k = 0; k < nBoxOutputs; k++ )
510  {
511  pObj = Gia_ManCi( p, curCi + k );
512  Gia_ObjSetTravIdCurrent( p, pObj );
513  // evaluate delay of this output
514  LevelMax = 0;
515  assert( nBoxInputs == (int)pDelayTable[1] );
516  for ( j = 0; j < nBoxInputs && (pObjIn = Gia_ManCo(p, curCo + j)); j++ )
517  if ( (int)pDelayTable[3+k*nBoxInputs+j] != -ABC_INFINITY )
518  LevelMax = Abc_MaxInt( LevelMax, Gia_ObjLevel(p, pObjIn) + ((int)pDelayTable[3+k*nBoxInputs+j] / nAnd2Delay) );
519  // set box output level
520  Gia_ObjSetLevel( p, pObj, LevelMax );
521  }
522  curCo += nBoxInputs;
523  curCi += nBoxOutputs;
524  }
525  // add remaining nodes
526  p->nLevels = 0;
527  for ( i = Tim_ManCoNum(pManTime) - Tim_ManPoNum(pManTime); i < Tim_ManCoNum(pManTime); i++ )
528  {
529  pObj = Gia_ManCo( p, i );
531  Gia_ObjSetCoLevel( p, pObj );
532  p->nLevels = Abc_MaxInt( p->nLevels, Gia_ObjLevel(p, pObj) );
533  }
534  curCo += Tim_ManPoNum(pManTime);
535  // verify counts
536  assert( curCi == Gia_ManCiNum(p) );
537  assert( curCo == Gia_ManCoNum(p) );
538 // printf( "Max level is %d.\n", p->nLevels );
539  return p->nLevels;
540 }
int Tim_ManCoNum(Tim_Man_t *p)
Definition: timMan.c:684
static Gia_Obj_t * Gia_ManCi(Gia_Man_t *p, int v)
Definition: gia.h:403
int Tim_ManBoxOutputNum(Tim_Man_t *p, int iBox)
Definition: timBox.c:202
int nLevels
Definition: gia.h:116
static int Abc_MaxInt(int a, int b)
Definition: abc_global.h:238
Definition: gia.h:75
int Tim_ManPiNum(Tim_Man_t *p)
Definition: timMan.c:688
static int Gia_ObjLevel(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:501
static Gia_Obj_t * Gia_ObjFanin0(Gia_Obj_t *pObj)
Definition: gia.h:454
static void Gia_ObjSetTravIdCurrent(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:531
void * pManTime
Definition: gia.h:165
void Gia_ManCleanLevels(Gia_Man_t *p, int Size)
Definition: giaUtil.c:470
int Tim_ManBoxNum(Tim_Man_t *p)
Definition: timMan.c:702
int Tim_ManBoxInputNum(Tim_Man_t *p, int iBox)
Definition: timBox.c:186
int nAnd2Delay
Definition: gia.h:173
static int Gia_ManCiNum(Gia_Man_t *p)
Definition: gia.h:383
static Gia_Obj_t * Gia_ManCo(Gia_Man_t *p, int v)
Definition: gia.h:404
static void Gia_ObjSetCoLevel(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:504
static int Gia_ManBufNum(Gia_Man_t *p)
Definition: gia.h:392
static Gia_Obj_t * Gia_ManConst0(Gia_Man_t *p)
Definition: gia.h:400
#define ABC_INFINITY
MACRO DEFINITIONS ///.
Definition: abc_global.h:216
#define assert(ex)
Definition: util_old.h:213
int Gia_ManLevelNum(Gia_Man_t *p)
Definition: giaUtil.c:505
typedefABC_NAMESPACE_HEADER_START struct Tim_Man_t_ Tim_Man_t
INCLUDES ///.
Definition: tim.h:92
void Gia_ManIncrementTravId(Gia_Man_t *p)
Definition: giaUtil.c:149
float Tim_ManGetCiArrival(Tim_Man_t *p, int iCi)
Definition: timTime.c:174
int Gia_ManLevelWithBoxes_rec(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: giaTim.c:452
int Tim_ManPoNum(Tim_Man_t *p)
Definition: timMan.c:694
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
static int Gia_ManCoNum(Gia_Man_t *p)
Definition: gia.h:384
static void Gia_ObjSetLevel(Gia_Man_t *p, Gia_Obj_t *pObj, int l)
Definition: gia.h:503
static int Gia_ManRegNum(Gia_Man_t *p)
Definition: gia.h:387
float * Tim_ManBoxDelayTable(Tim_Man_t *p, int iBox)
Definition: timBox.c:234
int Gia_ManLevelWithBoxes_rec ( Gia_Man_t p,
Gia_Obj_t pObj 
)

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

Synopsis [Computes level with boxes.]

Description []

SideEffects []

SeeAlso []

Definition at line 452 of file giaTim.c.

453 {
454  if ( Gia_ObjIsTravIdCurrent(p, pObj) )
455  return 0;
456  Gia_ObjSetTravIdCurrent(p, pObj);
457  if ( Gia_ObjIsCi(pObj) )
458  return 1;
459  assert( Gia_ObjIsAnd(pObj) );
460  if ( Gia_ObjSibl(p, Gia_ObjId(p, pObj)) )
462  if ( Gia_ManLevelWithBoxes_rec( p, Gia_ObjFanin0(pObj) ) )
463  return 1;
464  if ( Gia_ManLevelWithBoxes_rec( p, Gia_ObjFanin1(pObj) ) )
465  return 1;
466  Gia_ObjSetAndLevel( p, pObj );
467  return 0;
468 }
static Gia_Obj_t * Gia_ObjSiblObj(Gia_Man_t *p, int Id)
Definition: gia.h:894
static int Gia_ObjIsTravIdCurrent(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:533
static int Gia_ObjSibl(Gia_Man_t *p, int Id)
Definition: gia.h:893
static Gia_Obj_t * Gia_ObjFanin0(Gia_Obj_t *pObj)
Definition: gia.h:454
static void Gia_ObjSetAndLevel(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:506
static void Gia_ObjSetTravIdCurrent(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:531
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:410
static int Gia_ObjIsAnd(Gia_Obj_t *pObj)
Definition: gia.h:422
static Gia_Obj_t * Gia_ObjFanin1(Gia_Obj_t *pObj)
Definition: gia.h:455
#define assert(ex)
Definition: util_old.h:213
static int Gia_ObjIsCi(Gia_Obj_t *pObj)
Definition: gia.h:420
int Gia_ManLevelWithBoxes_rec(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: giaTim.c:452
int Gia_ManLutLevelWithBoxes ( Gia_Man_t p)

Definition at line 572 of file giaTim.c.

573 {
574 // int nAnd2Delay = p->nAnd2Delay ? p->nAnd2Delay : 1;
575  Tim_Man_t * pManTime = (Tim_Man_t *)p->pManTime;
576  Gia_Obj_t * pObj, * pObjIn;
577  int i, k, j, curCi, curCo, LevelMax;
578  assert( Gia_ManRegNum(p) == 0 );
579  // copy const and real PIs
581  Gia_ObjSetLevel( p, Gia_ManConst0(p), 0 );
584  for ( i = 0; i < Tim_ManPiNum(pManTime); i++ )
585  {
586  pObj = Gia_ManCi( p, i );
587 // Gia_ObjSetLevel( p, pObj, Tim_ManGetCiArrival(pManTime, i) / nAnd2Delay );
588  Gia_ObjSetLevel( p, pObj, 0 );
589  Gia_ObjSetTravIdCurrent( p, pObj );
590  }
591  // create logic for each box
592  curCi = Tim_ManPiNum(pManTime);
593  curCo = 0;
594  for ( i = 0; i < Tim_ManBoxNum(pManTime); i++ )
595  {
596  int nBoxInputs = Tim_ManBoxInputNum( pManTime, i );
597  int nBoxOutputs = Tim_ManBoxOutputNum( pManTime, i );
598  float * pDelayTable = Tim_ManBoxDelayTable( pManTime, i );
599  // compute level for TFI of box inputs
600  for ( k = 0; k < nBoxInputs; k++ )
601  {
602  pObj = Gia_ManCo( p, curCo + k );
604  {
605  printf( "Boxes are not in a topological order. Switching to level computation without boxes.\n" );
606  return Gia_ManLevelNum( p );
607  }
608  // set box input level
609  Gia_ObjSetCoLevel( p, pObj );
610  }
611  // compute level for box outputs
612  for ( k = 0; k < nBoxOutputs; k++ )
613  {
614  pObj = Gia_ManCi( p, curCi + k );
615  Gia_ObjSetTravIdCurrent( p, pObj );
616  // evaluate delay of this output
617  LevelMax = 0;
618  assert( nBoxInputs == (int)pDelayTable[1] );
619  for ( j = 0; j < nBoxInputs && (pObjIn = Gia_ManCo(p, curCo + j)); j++ )
620  if ( (int)pDelayTable[3+k*nBoxInputs+j] != -ABC_INFINITY )
621 // LevelMax = Abc_MaxInt( LevelMax, Gia_ObjLevel(p, pObjIn) + ((int)pDelayTable[3+k*nBoxInputs+j] / nAnd2Delay) );
622  LevelMax = Abc_MaxInt( LevelMax, Gia_ObjLevel(p, pObjIn) + 1 );
623  // set box output level
624  Gia_ObjSetLevel( p, pObj, LevelMax );
625  }
626  curCo += nBoxInputs;
627  curCi += nBoxOutputs;
628  }
629  // add remaining nodes
630  p->nLevels = 0;
631  for ( i = Tim_ManCoNum(pManTime) - Tim_ManPoNum(pManTime); i < Tim_ManCoNum(pManTime); i++ )
632  {
633  pObj = Gia_ManCo( p, i );
635  Gia_ObjSetCoLevel( p, pObj );
636  p->nLevels = Abc_MaxInt( p->nLevels, Gia_ObjLevel(p, pObj) );
637  }
638  curCo += Tim_ManPoNum(pManTime);
639  // verify counts
640  assert( curCi == Gia_ManCiNum(p) );
641  assert( curCo == Gia_ManCoNum(p) );
642 // printf( "Max level is %d.\n", p->nLevels );
643  return p->nLevels;
644 }
int Tim_ManCoNum(Tim_Man_t *p)
Definition: timMan.c:684
int Gia_ManLutLevelWithBoxes_rec(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: giaTim.c:553
static Gia_Obj_t * Gia_ManCi(Gia_Man_t *p, int v)
Definition: gia.h:403
int Tim_ManBoxOutputNum(Tim_Man_t *p, int iBox)
Definition: timBox.c:202
int nLevels
Definition: gia.h:116
static int Abc_MaxInt(int a, int b)
Definition: abc_global.h:238
Definition: gia.h:75
int Tim_ManPiNum(Tim_Man_t *p)
Definition: timMan.c:688
static int Gia_ObjLevel(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:501
static Gia_Obj_t * Gia_ObjFanin0(Gia_Obj_t *pObj)
Definition: gia.h:454
static void Gia_ObjSetTravIdCurrent(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:531
void * pManTime
Definition: gia.h:165
void Gia_ManCleanLevels(Gia_Man_t *p, int Size)
Definition: giaUtil.c:470
int Tim_ManBoxNum(Tim_Man_t *p)
Definition: timMan.c:702
int Tim_ManBoxInputNum(Tim_Man_t *p, int iBox)
Definition: timBox.c:186
static int Gia_ManCiNum(Gia_Man_t *p)
Definition: gia.h:383
static Gia_Obj_t * Gia_ManCo(Gia_Man_t *p, int v)
Definition: gia.h:404
static void Gia_ObjSetCoLevel(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:504
static Gia_Obj_t * Gia_ManConst0(Gia_Man_t *p)
Definition: gia.h:400
#define ABC_INFINITY
MACRO DEFINITIONS ///.
Definition: abc_global.h:216
#define assert(ex)
Definition: util_old.h:213
int Gia_ManLevelNum(Gia_Man_t *p)
Definition: giaUtil.c:505
typedefABC_NAMESPACE_HEADER_START struct Tim_Man_t_ Tim_Man_t
INCLUDES ///.
Definition: tim.h:92
void Gia_ManIncrementTravId(Gia_Man_t *p)
Definition: giaUtil.c:149
int Tim_ManPoNum(Tim_Man_t *p)
Definition: timMan.c:694
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
static int Gia_ManCoNum(Gia_Man_t *p)
Definition: gia.h:384
static void Gia_ObjSetLevel(Gia_Man_t *p, Gia_Obj_t *pObj, int l)
Definition: gia.h:503
static int Gia_ManRegNum(Gia_Man_t *p)
Definition: gia.h:387
float * Tim_ManBoxDelayTable(Tim_Man_t *p, int iBox)
Definition: timBox.c:234
int Gia_ManLutLevelWithBoxes_rec ( Gia_Man_t p,
Gia_Obj_t pObj 
)

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

Synopsis [Computes level with boxes.]

Description []

SideEffects []

SeeAlso []

Definition at line 553 of file giaTim.c.

554 {
555  int iObj, k, iFan, Level = 0;
556  if ( Gia_ObjIsTravIdCurrent(p, pObj) )
557  return 0;
558  Gia_ObjSetTravIdCurrent(p, pObj);
559  if ( Gia_ObjIsCi(pObj) )
560  return 1;
561  assert( Gia_ObjIsAnd(pObj) );
562  iObj = Gia_ObjId( p, pObj );
563  Gia_LutForEachFanin( p, iObj, iFan, k )
564  {
565  if ( Gia_ManLutLevelWithBoxes_rec( p, Gia_ManObj(p, iFan) ) )
566  return 1;
567  Level = Abc_MaxInt( Level, Gia_ObjLevelId(p, iFan) );
568  }
569  Gia_ObjSetLevelId( p, iObj, Level + 1 );
570  return 0;
571 }
static int Gia_ObjLevelId(Gia_Man_t *p, int Id)
Definition: gia.h:500
static void Gia_ObjSetLevelId(Gia_Man_t *p, int Id, int l)
Definition: gia.h:502
int Gia_ManLutLevelWithBoxes_rec(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: giaTim.c:553
static int Gia_ObjIsTravIdCurrent(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:533
static int Abc_MaxInt(int a, int b)
Definition: abc_global.h:238
static Gia_Obj_t * Gia_ManObj(Gia_Man_t *p, int v)
Definition: gia.h:402
static void Gia_ObjSetTravIdCurrent(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:531
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:410
static int Gia_ObjIsAnd(Gia_Obj_t *pObj)
Definition: gia.h:422
#define assert(ex)
Definition: util_old.h:213
static int Gia_ObjIsCi(Gia_Obj_t *pObj)
Definition: gia.h:420
#define Gia_LutForEachFanin(p, i, iFan, k)
Definition: gia.h:970
int Gia_ManNonRegBoxNum ( Gia_Man_t p)

Definition at line 57 of file giaTim.c.

58 {
59  return Gia_ManBoxNum(p) - Gia_ManRegBoxNum(p);
60 }
ABC_NAMESPACE_IMPL_START int Gia_ManBoxNum(Gia_Man_t *p)
DECLARATIONS ///.
Definition: giaTim.c:49
int Gia_ManRegBoxNum(Gia_Man_t *p)
Definition: giaTim.c:53
Vec_Int_t* Gia_ManOrderWithBoxes ( Gia_Man_t p)

Definition at line 277 of file giaTim.c.

278 {
279  Tim_Man_t * pManTime = (Tim_Man_t *)p->pManTime;
280  Vec_Int_t * vNodes;
281  Gia_Obj_t * pObj;
282  int i, k, curCi, curCo;
283  assert( pManTime != NULL );
284  assert( Gia_ManIsNormalized( p ) );
285  // start trav IDs
287  // start the array
288  vNodes = Vec_IntAlloc( Gia_ManObjNum(p) );
289  // include constant
290  Vec_IntPush( vNodes, 0 );
292  // include primary inputs
293  for ( i = 0; i < Tim_ManPiNum(pManTime); i++ )
294  {
295  pObj = Gia_ManCi( p, i );
296  Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
297  Gia_ObjSetTravIdCurrent( p, pObj );
298  assert( Gia_ObjId(p, pObj) == i+1 );
299  }
300  // for each box, include box nodes
301  curCi = Tim_ManPiNum(pManTime);
302  curCo = 0;
303  for ( i = 0; i < Tim_ManBoxNum(pManTime); i++ )
304  {
305  // add internal nodes
306  for ( k = 0; k < Tim_ManBoxInputNum(pManTime, i); k++ )
307  {
308  pObj = Gia_ManCo( p, curCo + k );
309  if ( Gia_ManOrderWithBoxes_rec( p, Gia_ObjFanin0(pObj), vNodes ) )
310  {
311  int iCiNum = p->iData2;
312  int iBoxNum = Tim_ManBoxFindFromCiNum( pManTime, iCiNum );
313  printf( "The command has to terminate. Boxes are not in a topological order.\n" );
314  printf( "The following information may help debugging (numbers are 0-based):\n" );
315  printf( "Input %d of BoxA %d (1stCI = %d; 1stCO = %d) has TFI with CI %d,\n",
316  k, i, Tim_ManBoxOutputFirst(pManTime, i), Tim_ManBoxInputFirst(pManTime, i), iCiNum );
317  printf( "which corresponds to output %d of BoxB %d (1stCI = %d; 1stCO = %d).\n",
318  iCiNum - Tim_ManBoxOutputFirst(pManTime, iBoxNum), iBoxNum,
319  Tim_ManBoxOutputFirst(pManTime, iBoxNum), Tim_ManBoxInputFirst(pManTime, iBoxNum) );
320  printf( "In a correct topological order, BoxB should precede BoxA.\n" );
321  Vec_IntFree( vNodes );
322  p->iData2 = 0;
323  return NULL;
324  }
325  }
326  // add POs corresponding to box inputs
327  for ( k = 0; k < Tim_ManBoxInputNum(pManTime, i); k++ )
328  {
329  pObj = Gia_ManCo( p, curCo + k );
330  Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
331  }
332  curCo += Tim_ManBoxInputNum(pManTime, i);
333  // add PIs corresponding to box outputs
334  for ( k = 0; k < Tim_ManBoxOutputNum(pManTime, i); k++ )
335  {
336  pObj = Gia_ManCi( p, curCi + k );
337  Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
338  Gia_ObjSetTravIdCurrent( p, pObj );
339  }
340  curCi += Tim_ManBoxOutputNum(pManTime, i);
341  }
342  // add remaining nodes
343  for ( i = Tim_ManCoNum(pManTime) - Tim_ManPoNum(pManTime); i < Tim_ManCoNum(pManTime); i++ )
344  {
345  pObj = Gia_ManCo( p, i );
346  Gia_ManOrderWithBoxes_rec( p, Gia_ObjFanin0(pObj), vNodes );
347  }
348  // add POs
349  for ( i = Tim_ManCoNum(pManTime) - Tim_ManPoNum(pManTime); i < Tim_ManCoNum(pManTime); i++ )
350  {
351  pObj = Gia_ManCo( p, i );
352  Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
353  }
354  curCo += Tim_ManPoNum(pManTime);
355  // verify counts
356  assert( curCi == Gia_ManCiNum(p) );
357  assert( curCo == Gia_ManCoNum(p) );
358  assert( Vec_IntSize(vNodes) == Gia_ManObjNum(p) );
359  return vNodes;
360 }
int Tim_ManBoxOutputFirst(Tim_Man_t *p, int iBox)
Definition: timBox.c:154
int Tim_ManCoNum(Tim_Man_t *p)
Definition: timMan.c:684
static Gia_Obj_t * Gia_ManCi(Gia_Man_t *p, int v)
Definition: gia.h:403
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
int Tim_ManBoxOutputNum(Tim_Man_t *p, int iBox)
Definition: timBox.c:202
int Gia_ManIsNormalized(Gia_Man_t *p)
Definition: giaTim.c:109
Definition: gia.h:75
int Tim_ManPiNum(Tim_Man_t *p)
Definition: timMan.c:688
int Gia_ManOrderWithBoxes_rec(Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vNodes)
Definition: giaTim.c:249
int Tim_ManBoxFindFromCiNum(Tim_Man_t *p, int iCiNum)
Definition: timBox.c:306
int iData2
Definition: gia.h:172
static Gia_Obj_t * Gia_ObjFanin0(Gia_Obj_t *pObj)
Definition: gia.h:454
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
static void Gia_ObjSetTravIdCurrent(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:531
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
void * pManTime
Definition: gia.h:165
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:410
int Tim_ManBoxNum(Tim_Man_t *p)
Definition: timMan.c:702
int Tim_ManBoxInputNum(Tim_Man_t *p, int iBox)
Definition: timBox.c:186
static int Gia_ManCiNum(Gia_Man_t *p)
Definition: gia.h:383
static Gia_Obj_t * Gia_ManCo(Gia_Man_t *p, int v)
Definition: gia.h:404
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
static Gia_Obj_t * Gia_ManConst0(Gia_Man_t *p)
Definition: gia.h:400
#define assert(ex)
Definition: util_old.h:213
typedefABC_NAMESPACE_HEADER_START struct Tim_Man_t_ Tim_Man_t
INCLUDES ///.
Definition: tim.h:92
void Gia_ManIncrementTravId(Gia_Man_t *p)
Definition: giaUtil.c:149
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
int Tim_ManBoxInputFirst(Tim_Man_t *p, int iBox)
Definition: timBox.c:122
int Tim_ManPoNum(Tim_Man_t *p)
Definition: timMan.c:694
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
static int Gia_ManCoNum(Gia_Man_t *p)
Definition: gia.h:384
int Gia_ManOrderWithBoxes_rec ( Gia_Man_t p,
Gia_Obj_t pObj,
Vec_Int_t vNodes 
)

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

Synopsis [Find the ordering of AIG objects.]

Description []

SideEffects []

SeeAlso []

Definition at line 249 of file giaTim.c.

250 {
251  if ( Gia_ObjIsTravIdCurrent(p, pObj) )
252  return 0;
253  Gia_ObjSetTravIdCurrent(p, pObj);
254  if ( Gia_ObjIsCi(pObj) )
255  {
256  p->iData2 = Gia_ObjCioId(pObj);
257  return 1;
258  }
259  assert( Gia_ObjIsAnd(pObj) );
260  if ( Gia_ObjIsBuf(pObj) )
261  {
262  if ( Gia_ManOrderWithBoxes_rec( p, Gia_ObjFanin0(pObj), vNodes ) )
263  return 1;
264  Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
265  return 0;
266  }
267  if ( Gia_ObjSibl(p, Gia_ObjId(p, pObj)) )
268  if ( Gia_ManOrderWithBoxes_rec( p, Gia_ObjSiblObj(p, Gia_ObjId(p, pObj)), vNodes ) )
269  return 1;
270  if ( Gia_ManOrderWithBoxes_rec( p, Gia_ObjFanin0(pObj), vNodes ) )
271  return 1;
272  if ( Gia_ManOrderWithBoxes_rec( p, Gia_ObjFanin1(pObj), vNodes ) )
273  return 1;
274  Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
275  return 0;
276 }
static Gia_Obj_t * Gia_ObjSiblObj(Gia_Man_t *p, int Id)
Definition: gia.h:894
static int Gia_ObjIsTravIdCurrent(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:533
static int Gia_ObjIsBuf(Gia_Obj_t *pObj)
Definition: gia.h:427
int Gia_ManOrderWithBoxes_rec(Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vNodes)
Definition: giaTim.c:249
static int Gia_ObjSibl(Gia_Man_t *p, int Id)
Definition: gia.h:893
int iData2
Definition: gia.h:172
static Gia_Obj_t * Gia_ObjFanin0(Gia_Obj_t *pObj)
Definition: gia.h:454
static void Gia_ObjSetTravIdCurrent(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:531
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:410
static int Gia_ObjIsAnd(Gia_Obj_t *pObj)
Definition: gia.h:422
static Gia_Obj_t * Gia_ObjFanin1(Gia_Obj_t *pObj)
Definition: gia.h:455
#define assert(ex)
Definition: util_old.h:213
static int Gia_ObjIsCi(Gia_Obj_t *pObj)
Definition: gia.h:420
static int Gia_ObjCioId(Gia_Obj_t *pObj)
Definition: gia.h:411
int Gia_ManRegBoxNum ( Gia_Man_t p)

Definition at line 53 of file giaTim.c.

54 {
55  return p->vRegClasses ? Vec_IntSize(p->vRegClasses) : 0;
56 }
Vec_Int_t * vRegClasses
Definition: gia.h:144
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Gia_Man_t* Gia_ManUpdateExtraAig ( void *  pTime,
Gia_Man_t p,
Vec_Int_t vBoxPres 
)

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

Synopsis [Update AIG of the holes.]

Description []

SideEffects []

SeeAlso []

Definition at line 683 of file giaTim.c.

684 {
685  Gia_Man_t * pNew;
686  Tim_Man_t * pManTime = (Tim_Man_t *)pTime;
687  Vec_Int_t * vOutPres = Vec_IntAlloc( 100 );
688  int i, k, curPo = 0;
689  assert( Vec_IntSize(vBoxPres) == Tim_ManBoxNum(pManTime) );
690  assert( Gia_ManCoNum(p) == Tim_ManCiNum(pManTime) - Tim_ManPiNum(pManTime) );
691  for ( i = 0; i < Tim_ManBoxNum(pManTime); i++ )
692  {
693  for ( k = 0; k < Tim_ManBoxOutputNum(pManTime, i); k++ )
694  Vec_IntPush( vOutPres, Vec_IntEntry(vBoxPres, i) );
695  curPo += Tim_ManBoxOutputNum(pManTime, i);
696  }
697  assert( curPo == Gia_ManCoNum(p) );
698  pNew = Gia_ManDupOutputVec( p, vOutPres );
699  Vec_IntFree( vOutPres );
700  return pNew;
701 }
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
int Tim_ManBoxOutputNum(Tim_Man_t *p, int iBox)
Definition: timBox.c:202
Gia_Man_t * Gia_ManDupOutputVec(Gia_Man_t *p, Vec_Int_t *vOutPres)
Definition: giaDup.c:232
int Tim_ManPiNum(Tim_Man_t *p)
Definition: timMan.c:688
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
int Tim_ManCiNum(Tim_Man_t *p)
Definition: timMan.c:680
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
int Tim_ManBoxNum(Tim_Man_t *p)
Definition: timMan.c:702
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Definition: gia.h:95
#define assert(ex)
Definition: util_old.h:213
typedefABC_NAMESPACE_HEADER_START struct Tim_Man_t_ Tim_Man_t
INCLUDES ///.
Definition: tim.h:92
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
static int Gia_ManCoNum(Gia_Man_t *p)
Definition: gia.h:384
Gia_Man_t* Gia_ManUpdateExtraAig2 ( void *  pTime,
Gia_Man_t p,
Vec_Int_t vBoxesLeft 
)

Definition at line 702 of file giaTim.c.

703 {
704  Gia_Man_t * pNew;
705  Tim_Man_t * pManTime = (Tim_Man_t *)pTime;
706  int nRealPis = Tim_ManPiNum(pManTime);
707  Vec_Int_t * vOutsLeft = Vec_IntAlloc( 100 );
708  int i, k, iBox, iOutFirst;
709  assert( Vec_IntSize(vBoxesLeft) <= Tim_ManBoxNum(pManTime) );
710  assert( Gia_ManCoNum(p) == Tim_ManCiNum(pManTime) - nRealPis );
711  Vec_IntForEachEntry( vBoxesLeft, iBox, i )
712  {
713  iOutFirst = Tim_ManBoxOutputFirst(pManTime, iBox) - nRealPis;
714  for ( k = 0; k < Tim_ManBoxOutputNum(pManTime, iBox); k++ )
715  Vec_IntPush( vOutsLeft, iOutFirst + k );
716  }
717  pNew = Gia_ManDupSelectedOutputs( p, vOutsLeft );
718  Vec_IntFree( vOutsLeft );
719  return pNew;
720 }
int Tim_ManBoxOutputFirst(Tim_Man_t *p, int iBox)
Definition: timBox.c:154
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
int Tim_ManBoxOutputNum(Tim_Man_t *p, int iBox)
Definition: timBox.c:202
int Tim_ManPiNum(Tim_Man_t *p)
Definition: timMan.c:688
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
int Tim_ManCiNum(Tim_Man_t *p)
Definition: timMan.c:680
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
int Tim_ManBoxNum(Tim_Man_t *p)
Definition: timMan.c:702
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Definition: gia.h:95
#define assert(ex)
Definition: util_old.h:213
typedefABC_NAMESPACE_HEADER_START struct Tim_Man_t_ Tim_Man_t
INCLUDES ///.
Definition: tim.h:92
Gia_Man_t * Gia_ManDupSelectedOutputs(Gia_Man_t *p, Vec_Int_t *vOutsLeft)
Definition: giaDup.c:266
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
static int Gia_ManCoNum(Gia_Man_t *p)
Definition: gia.h:384
void* Gia_ManUpdateTimMan ( Gia_Man_t p,
Vec_Int_t vBoxPres 
)

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

Synopsis [Update hierarchy/timing manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 657 of file giaTim.c.

658 {
659  Tim_Man_t * pManTime = (Tim_Man_t *)p->pManTime;
660  assert( pManTime != NULL );
661  assert( Vec_IntSize(vBoxPres) == Tim_ManBoxNum(pManTime) );
662  return Tim_ManTrim( pManTime, vBoxPres );
663 }
void * pManTime
Definition: gia.h:165
Tim_Man_t * Tim_ManTrim(Tim_Man_t *p, Vec_Int_t *vBoxPres)
Definition: timMan.c:163
int Tim_ManBoxNum(Tim_Man_t *p)
Definition: timMan.c:702
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
#define assert(ex)
Definition: util_old.h:213
typedefABC_NAMESPACE_HEADER_START struct Tim_Man_t_ Tim_Man_t
INCLUDES ///.
Definition: tim.h:92
void* Gia_ManUpdateTimMan2 ( Gia_Man_t p,
Vec_Int_t vBoxesLeft,
int  nTermsDiff 
)

Definition at line 664 of file giaTim.c.

665 {
666  Tim_Man_t * pManTime = (Tim_Man_t *)p->pManTime;
667  assert( pManTime != NULL );
668  assert( Vec_IntSize(vBoxesLeft) <= Tim_ManBoxNum(pManTime) );
669  return Tim_ManReduce( pManTime, vBoxesLeft, nTermsDiff );
670 }
Tim_Man_t * Tim_ManReduce(Tim_Man_t *p, Vec_Int_t *vBoxesLeft, int nTermsDiff)
Definition: timMan.c:251
void * pManTime
Definition: gia.h:165
int Tim_ManBoxNum(Tim_Man_t *p)
Definition: timMan.c:702
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
#define assert(ex)
Definition: util_old.h:213
typedefABC_NAMESPACE_HEADER_START struct Tim_Man_t_ Tim_Man_t
INCLUDES ///.
Definition: tim.h:92
int Gia_ManVerifyWithBoxes ( Gia_Man_t pGia,
int  nBTLimit,
int  nTimeLim,
int  fSeq,
int  fVerbose,
char *  pFileSpec 
)

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

Synopsis [Verify XAIG against its spec.]

Description []

SideEffects []

SeeAlso []

Definition at line 859 of file giaTim.c.

860 {
861  int Status = -1;
862  Gia_Man_t * pSpec, * pGia0, * pGia1, * pMiter;
863  Vec_Int_t * vBoxPres = NULL;
864  if ( pFileSpec == NULL && pGia->pSpec == NULL )
865  {
866  printf( "Spec file is not given. Use standard flow.\n" );
867  return Status;
868  }
869  if ( Gia_ManBoxNum(pGia) && pGia->pAigExtra == NULL )
870  {
871  printf( "Design has no box logic. Use standard flow.\n" );
872  return Status;
873  }
874  // read original AIG
875  pSpec = Gia_AigerRead( pFileSpec ? pFileSpec : pGia->pSpec, 0, 0 );
876  if ( Gia_ManBoxNum(pSpec) && pSpec->pAigExtra == NULL )
877  {
878  Gia_ManStop( pSpec );
879  printf( "Spec has no box logic. Use standard flow.\n" );
880  return Status;
881  }
882  // prepare miter
883  if ( pGia->pManTime == NULL && pSpec->pManTime == NULL )
884  {
885  pGia0 = Gia_ManDup( pSpec );
886  pGia1 = Gia_ManDup( pGia );
887  }
888  else
889  {
890  // if timing managers have different number of black boxes,
891  // it is possible that some of the boxes are swept away
892  if ( pSpec->pManTime && Tim_ManBlackBoxNum((Tim_Man_t *)pSpec->pManTime) > 0 && Gia_ManBoxNum(pGia) > 0 )
893  {
894  // specification cannot have fewer boxes than implementation
895  if ( Gia_ManBoxNum(pSpec) < Gia_ManBoxNum(pGia) )
896  {
897  printf( "Spec has less boxes than the design. Cannot proceed.\n" );
898  return Status;
899  }
900  // to align the boxes, find what boxes of pSpec are dropped in pGia
901  if ( Gia_ManBoxNum(pSpec) > Gia_ManBoxNum(pGia) )
902  {
903  vBoxPres = Tim_ManAlignTwo( (Tim_Man_t *)pSpec->pManTime, (Tim_Man_t *)pGia->pManTime );
904  if ( vBoxPres == NULL )
905  {
906  printf( "Boxes of spec and design cannot be aligned. Cannot proceed.\n" );
907  return Status;
908  }
909  }
910  }
911  // collapse two designs
912  if ( Gia_ManBoxNum(pSpec) > 0 )
913  pGia0 = Gia_ManDupCollapse( pSpec, pSpec->pAigExtra, vBoxPres, fSeq );
914  else
915  pGia0 = Gia_ManDup( pSpec );
916  if ( Gia_ManBoxNum(pGia) > 0 )
917  pGia1 = Gia_ManDupCollapse( pGia, pGia->pAigExtra, NULL, fSeq );
918  else
919  pGia1 = Gia_ManDup( pGia );
920  Vec_IntFreeP( &vBoxPres );
921  }
922  // compute the miter
923  if ( fSeq )
924  {
925  pMiter = Gia_ManMiter( pGia0, pGia1, 0, 0, 1, 0, fVerbose );
926  if ( pMiter )
927  {
928  Aig_Man_t * pMan;
929  Fra_Sec_t SecPar, * pSecPar = &SecPar;
930  Fra_SecSetDefaultParams( pSecPar );
931  pSecPar->fRetimeFirst = 0;
932  pSecPar->nBTLimit = nBTLimit;
933  pSecPar->TimeLimit = nTimeLim;
934  pSecPar->fVerbose = fVerbose;
935  pMan = Gia_ManToAig( pMiter, 0 );
936  Gia_ManStop( pMiter );
937  Status = Fra_FraigSec( pMan, pSecPar, NULL );
938  Aig_ManStop( pMan );
939  }
940  }
941  else
942  {
943  pMiter = Gia_ManMiter( pGia0, pGia1, 0, 1, 0, 0, fVerbose );
944  if ( pMiter )
945  {
946  Cec_ParCec_t ParsCec, * pPars = &ParsCec;
948  pPars->nBTLimit = nBTLimit;
949  pPars->TimeLimit = nTimeLim;
950  pPars->fVerbose = fVerbose;
951  Status = Cec_ManVerify( pMiter, pPars );
952  if ( pPars->iOutFail >= 0 )
953  Abc_Print( 1, "Verification failed for at least one output (%d).\n", pPars->iOutFail );
954  Gia_ManStop( pMiter );
955  }
956  }
957  Gia_ManStop( pGia0 );
958  Gia_ManStop( pGia1 );
959  Gia_ManStop( pSpec );
960  return Status;
961 }
Gia_Man_t * Gia_ManDup(Gia_Man_t *p)
Definition: giaDup.c:552
int TimeLimit
Definition: fra.h:141
void Gia_ManStop(Gia_Man_t *p)
Definition: giaMan.c:77
ABC_NAMESPACE_IMPL_START int Gia_ManBoxNum(Gia_Man_t *p)
DECLARATIONS ///.
Definition: giaTim.c:49
Gia_Man_t * pAigExtra
Definition: gia.h:149
Gia_Man_t * Gia_AigerRead(char *pFileName, int fSkipStrash, int fCheck)
Definition: giaAiger.c:821
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
int nBTLimit
Definition: cec.h:120
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
void Fra_SecSetDefaultParams(Fra_Sec_t *p)
DECLARATIONS ///.
Definition: fraSec.c:51
int fVerbose
Definition: fra.h:139
void Cec_ManCecSetDefaultParams(Cec_ParCec_t *p)
Definition: cecCore.c:157
char * pSpec
Definition: gia.h:98
Aig_Man_t * Gia_ManToAig(Gia_Man_t *p, int fChoices)
Definition: giaAig.c:277
void * pManTime
Definition: gia.h:165
int TimeLimit
Definition: cec.h:121
static void Vec_IntFreeP(Vec_Int_t **p)
Definition: vecInt.h:289
static void Abc_Print(int level, const char *format,...)
Definition: abc_global.h:313
int Fra_FraigSec(Aig_Man_t *p, Fra_Sec_t *pParSec, Aig_Man_t **ppResult)
Definition: fraSec.c:95
int nBTLimit
Definition: fra.h:119
int iOutFail
Definition: cec.h:128
int Tim_ManBlackBoxNum(Tim_Man_t *p)
Definition: timMan.c:706
Definition: gia.h:95
int Cec_ManVerify(Gia_Man_t *p, Cec_ParCec_t *pPars)
MACRO DEFINITIONS ///.
Definition: cecCec.c:308
int fVerbose
Definition: cec.h:127
typedefABC_NAMESPACE_HEADER_START struct Tim_Man_t_ Tim_Man_t
INCLUDES ///.
Definition: tim.h:92
Gia_Man_t * Gia_ManDupCollapse(Gia_Man_t *p, Gia_Man_t *pBoxes, Vec_Int_t *vBoxPres, int fSeq)
Definition: giaTim.c:748
int fRetimeFirst
Definition: fra.h:127
Vec_Int_t * Tim_ManAlignTwo(Tim_Man_t *pSpec, Tim_Man_t *pImpl)
Definition: timMan.c:344
Gia_Man_t * Gia_ManMiter(Gia_Man_t *pAig0, Gia_Man_t *pAig1, int nInsDup, int fDualOut, int fSeq, int fImplic, int fVerbose)
Definition: giaDup.c:2128