summaryrefslogtreecommitdiffstats
path: root/src/aig
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2013-03-05 13:13:15 -0800
committerAlan Mishchenko <alanmi@berkeley.edu>2013-03-05 13:13:15 -0800
commit4ff5203f4c8b341eb717b742bf1af51f64f31ccd (patch)
treed3e814bd980de2c87db542d7e0929fded9db25b8 /src/aig
parent0c9337f6276f8a56960f697b7361c978e3e50a41 (diff)
downloadabc-4ff5203f4c8b341eb717b742bf1af51f64f31ccd.tar.gz
abc-4ff5203f4c8b341eb717b742bf1af51f64f31ccd.tar.bz2
abc-4ff5203f4c8b341eb717b742bf1af51f64f31ccd.zip
Improvements to the hierarchy/timing manager.
Diffstat (limited to 'src/aig')
-rw-r--r--src/aig/gia/gia.h2
-rw-r--r--src/aig/gia/giaAiger.c23
-rw-r--r--src/aig/gia/giaIf.c11
-rw-r--r--src/aig/gia/giaSweep.c2
-rw-r--r--src/aig/gia/giaTim.c82
5 files changed, 82 insertions, 38 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 6ba68a55..2083f8ea 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -1019,7 +1019,7 @@ extern float Gia_ManComputeSwitching( Gia_Man_t * p, int nFrames,
/*=== giaTim.c ===========================================================*/
extern Gia_Man_t * Gia_ManDupNormalize( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManDupUnnormalize( Gia_Man_t * p );
-extern Gia_Man_t * Gia_ManDupCollapse( Gia_Man_t * p, Gia_Man_t * pBoxes );
+extern Gia_Man_t * Gia_ManDupCollapse( Gia_Man_t * p, Gia_Man_t * pBoxes, Vec_Int_t * vBoxPres );
extern int Gia_ManLevelWithBoxes( Gia_Man_t * p );
extern int Gia_ManVerifyWithBoxes( Gia_Man_t * pGia, void * pParsInit );
extern void * Gia_ManUpdateTimMan( Gia_Man_t * p, Vec_Int_t * vBoxPres );
diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c
index 29bcddfa..ee90784e 100644
--- a/src/aig/gia/giaAiger.c
+++ b/src/aig/gia/giaAiger.c
@@ -1113,22 +1113,23 @@ void Gia_AigerWrite( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int
}
if ( p->pManTime )
{
- Vec_Flt_t * vArrTimes, * vReqTimes;
- if ( Tim_ManGetArrsReqs( (Tim_Man_t *)p->pManTime, &vArrTimes, &vReqTimes ) )
+ float * pTimes;
+ pTimes = Tim_ManGetArrTimes( p->pManTime );
+ if ( pTimes )
{
fprintf( pFile, "i" );
Gia_FileWriteBufferSize( pFile, 4*Tim_ManPiNum((Tim_Man_t *)p->pManTime) );
- assert( Vec_FltSize(vArrTimes) == Tim_ManPiNum((Tim_Man_t *)p->pManTime) );
- fwrite( Vec_FltArray(vArrTimes), 1, 4*Tim_ManPiNum((Tim_Man_t *)p->pManTime), pFile );
-
+ fwrite( pTimes, 1, 4*Tim_ManPiNum((Tim_Man_t *)p->pManTime), pFile );
+ ABC_FREE( pTimes );
+ if ( fVerbose ) printf( "Finished writing extension \"i\".\n" );
+ }
+ pTimes = Tim_ManGetReqTimes( p->pManTime );
+ if ( pTimes )
+ {
fprintf( pFile, "o" );
Gia_FileWriteBufferSize( pFile, 4*Tim_ManPoNum((Tim_Man_t *)p->pManTime) );
- assert( Vec_FltSize(vReqTimes) == Tim_ManPoNum((Tim_Man_t *)p->pManTime) );
- fwrite( Vec_FltArray(vReqTimes), 1, 4*Tim_ManPoNum((Tim_Man_t *)p->pManTime), pFile );
-
- Vec_FltFree( vArrTimes );
- Vec_FltFree( vReqTimes );
- if ( fVerbose ) printf( "Finished writing extension \"i\".\n" );
+ fwrite( pTimes, 1, 4*Tim_ManPoNum((Tim_Man_t *)p->pManTime), pFile );
+ ABC_FREE( pTimes );
if ( fVerbose ) printf( "Finished writing extension \"o\".\n" );
}
}
diff --git a/src/aig/gia/giaIf.c b/src/aig/gia/giaIf.c
index 1d4373a3..dc16b886 100644
--- a/src/aig/gia/giaIf.c
+++ b/src/aig/gia/giaIf.c
@@ -82,7 +82,7 @@ void Gia_ManSetIfParsDefault( void * pp )
p->fUseCoAttrs = 1; // use CO attributes
p->pLutLib = NULL;
p->pTimesArr = NULL;
- p->pTimesArr = NULL;
+ p->pTimesReq = NULL;
p->pFuncCost = NULL;
}
@@ -1143,8 +1143,11 @@ Gia_Man_t * Gia_ManPerformMapping( Gia_Man_t * p, void * pp )
If_Man_t * pIfMan;
If_Par_t * pPars = (If_Par_t *)pp;
// reconstruct GIA according to the hierarchy manager
+ assert( pPars->pTimesArr == NULL );
+ assert( pPars->pTimesReq == NULL );
if ( p->pManTime )
{
+ Vec_Flt_t * vArrTimes = NULL, * vReqTimes = NULL;
pNew = Gia_ManDupUnnormalize( p );
if ( pNew == NULL )
return NULL;
@@ -1152,12 +1155,12 @@ Gia_Man_t * Gia_ManPerformMapping( Gia_Man_t * p, void * pp )
pNew->pAigExtra = p->pAigExtra; p->pAigExtra = NULL;
pNew->nAnd2Delay = p->nAnd2Delay; p->nAnd2Delay = 0;
p = pNew;
+ // set arrival and required times
+ pPars->pTimesArr = Tim_ManGetArrTimes( (Tim_Man_t *)p->pManTime );
+ pPars->pTimesReq = Tim_ManGetReqTimes( (Tim_Man_t *)p->pManTime );
}
else
p = Gia_ManDup( p );
- // set the arrival times
- assert( pPars->pTimesArr == NULL );
- pPars->pTimesArr = ABC_CALLOC( float, Gia_ManCiNum(p) );
// translate into the mapper
pIfMan = Gia_ManToIf( p, pPars );
if ( pIfMan == NULL )
diff --git a/src/aig/gia/giaSweep.c b/src/aig/gia/giaSweep.c
index 4ef8725e..994aedc1 100644
--- a/src/aig/gia/giaSweep.c
+++ b/src/aig/gia/giaSweep.c
@@ -304,7 +304,7 @@ Gia_Man_t * Gia_ManFraigSweep( Gia_Man_t * p, void * pPars )
return NULL;
// find global equivalences
pNew->pManTime = p->pManTime;
- pGia = Gia_ManDupCollapse( pNew, p->pAigExtra );
+ pGia = Gia_ManDupCollapse( pNew, p->pAigExtra, NULL );
pNew->pManTime = NULL;
Gia_ManFraigSweepPerform( pGia, pPars );
// transfer equivalences
diff --git a/src/aig/gia/giaTim.c b/src/aig/gia/giaTim.c
index e3841856..01601625 100644
--- a/src/aig/gia/giaTim.c
+++ b/src/aig/gia/giaTim.c
@@ -285,7 +285,7 @@ void Gia_ManDupCollapse_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Man_t * pNew )
if ( Gia_ObjSibl(p, Gia_ObjId(p, pObj)) )
pNew->pSibls[Abc_Lit2Var(pObj->Value)] = Abc_Lit2Var(Gia_ObjSiblObj(p, Gia_ObjId(p, pObj))->Value);
}
-Gia_Man_t * Gia_ManDupCollapse( Gia_Man_t * p, Gia_Man_t * pBoxes )
+Gia_Man_t * Gia_ManDupCollapse( Gia_Man_t * p, Gia_Man_t * pBoxes, Vec_Int_t * vBoxPres )
{
Tim_Man_t * pTime = (Tim_Man_t *)p->pManTime;
Gia_Man_t * pNew, * pTemp;
@@ -320,28 +320,46 @@ Gia_Man_t * Gia_ManDupCollapse( Gia_Man_t * p, Gia_Man_t * pBoxes )
Gia_ObjSetTravIdCurrent( pBoxes, Gia_ManConst0(pBoxes) );
Gia_ManConst0(pBoxes)->Value = 0;
// add internal nodes
- for ( k = 0; k < Tim_ManBoxInputNum(pTime, i); k++ )
+ if ( Tim_ManBoxIsBlack(pTime, i) )
{
- // build logic
- pObj = Gia_ManPo( p, curCo + k );
- Gia_ManDupCollapse_rec( p, Gia_ObjFanin0(pObj), pNew );
- // transfer to the PI
- pObjBox = Gia_ManPi( pBoxes, k );
- pObjBox->Value = Gia_ObjFanin0Copy(pObj);
- Gia_ObjSetTravIdCurrent( pBoxes, pObjBox );
+ int fSkip = (vBoxPres != NULL && !Vec_IntEntry(vBoxPres, i));
+ for ( k = 0; k < Tim_ManBoxInputNum(pTime, i); k++ )
+ {
+ pObj = Gia_ManPo( p, curCo + k );
+ Gia_ManDupCollapse_rec( p, Gia_ObjFanin0(pObj), pNew );
+ pObj->Value = fSkip ? -1 : Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+ }
+ for ( k = 0; k < Tim_ManBoxOutputNum(pTime, i); k++ )
+ {
+ pObj = Gia_ManPi( p, curCi + k );
+ pObj->Value = fSkip ? 0 : Gia_ManAppendCi(pNew);
+ Gia_ObjSetTravIdCurrent( p, pObj );
+ }
}
- curCo += Tim_ManBoxInputNum(pTime, i);
- // add internal nodes
- for ( k = 0; k < Tim_ManBoxOutputNum(pTime, i); k++ )
+ else
{
- // build logic
- pObjBox = Gia_ManPo( pBoxes, curCi - Tim_ManPiNum(pTime) + k );
- Gia_ManDupCollapse_rec( pBoxes, Gia_ObjFanin0(pObjBox), pNew );
- // transfer to the PI
- pObj = Gia_ManPi( p, curCi + k );
- pObj->Value = Gia_ObjFanin0Copy(pObjBox);
- Gia_ObjSetTravIdCurrent( p, pObj );
+ for ( k = 0; k < Tim_ManBoxInputNum(pTime, i); k++ )
+ {
+ // build logic
+ pObj = Gia_ManPo( p, curCo + k );
+ Gia_ManDupCollapse_rec( p, Gia_ObjFanin0(pObj), pNew );
+ // transfer to the PI
+ pObjBox = Gia_ManPi( pBoxes, k );
+ pObjBox->Value = Gia_ObjFanin0Copy(pObj);
+ Gia_ObjSetTravIdCurrent( pBoxes, pObjBox );
+ }
+ for ( k = 0; k < Tim_ManBoxOutputNum(pTime, i); k++ )
+ {
+ // build logic
+ pObjBox = Gia_ManPo( pBoxes, curCi - Tim_ManPiNum(pTime) + k );
+ Gia_ManDupCollapse_rec( pBoxes, Gia_ObjFanin0(pObjBox), pNew );
+ // transfer to the PI
+ pObj = Gia_ManPi( p, curCi + k );
+ pObj->Value = Gia_ObjFanin0Copy(pObjBox);
+ Gia_ObjSetTravIdCurrent( p, pObj );
+ }
}
+ curCo += Tim_ManBoxInputNum(pTime, i);
curCi += Tim_ManBoxOutputNum(pTime, i);
}
// add remaining nodes
@@ -481,6 +499,7 @@ int Gia_ManVerifyWithBoxes( Gia_Man_t * pGia, void * pParsInit )
int fVerbose = 1;
int Status = -1;
Gia_Man_t * pSpec, * pGia0, * pGia1, * pMiter;
+ Vec_Int_t * vBoxPres = NULL;
if ( pGia->pSpec == NULL )
{
printf( "Spec file is not given. Use standard flow.\n" );
@@ -508,8 +527,29 @@ int Gia_ManVerifyWithBoxes( Gia_Man_t * pGia, void * pParsInit )
printf( "Spec has no box logic. Use standard flow.\n" );
return Status;
}
- pGia0 = Gia_ManDupCollapse( pSpec, pSpec->pAigExtra );
- pGia1 = Gia_ManDupCollapse( pGia, pGia->pAigExtra );
+ // if timing managers have different number of black boxes,
+ // it is possible that some of the boxes are swept away
+ // but specification cannot have fewer boxes than implementation
+ if ( Tim_ManBoxNum( (Tim_Man_t *)pSpec->pManTime ) < Tim_ManBoxNum( (Tim_Man_t *)pGia->pManTime ) )
+ {
+ printf( "Spec has more boxes than the design. Cannot proceed.\n" );
+ return Status;
+ }
+ // in this case, it is expected that the boxes can be aligned
+ // find what boxes of pSpec are dropped in pGia
+ if ( Tim_ManBoxNum( (Tim_Man_t *)pSpec->pManTime ) != Tim_ManBoxNum( (Tim_Man_t *)pGia->pManTime ) )
+ {
+ vBoxPres = Tim_ManAlignTwo( (Tim_Man_t *)pSpec->pManTime, (Tim_Man_t *)pGia->pManTime );
+ if ( vBoxPres == NULL )
+ {
+ printf( "Boxes of spec and design cannot be aligned. Cannot proceed.\n" );
+ return Status;
+ }
+ }
+ // collapse two designs
+ pGia0 = Gia_ManDupCollapse( pSpec, pSpec->pAigExtra, vBoxPres );
+ pGia1 = Gia_ManDupCollapse( pGia, pGia->pAigExtra, NULL );
+ Vec_IntFreeP( &vBoxPres );
// compute the miter
pMiter = Gia_ManMiter( pGia0, pGia1, 1, 0, fVerbose );
if ( pMiter )