summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/aig/gia/gia.h11
-rw-r--r--src/aig/gia/giaAig.c10
-rw-r--r--src/aig/gia/giaAiger.c18
-rw-r--r--src/aig/gia/giaDup.c265
-rw-r--r--src/aig/gia/giaIf.c22
-rw-r--r--src/aig/gia/giaTim.c550
-rw-r--r--src/aig/gia/module.make1
-rw-r--r--src/base/abci/abc.c79
-rw-r--r--src/misc/tim/timMan.c2
9 files changed, 674 insertions, 284 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index f87a88fa..7ea38cda 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -806,6 +806,7 @@ extern int Gia_ManConeSize( Gia_Man_t * p, int * pNodes, int nNo
extern Vec_Vec_t * Gia_ManLevelize( Gia_Man_t * p );
extern Vec_Int_t * Gia_ManOrderReverse( Gia_Man_t * p );
/*=== giaDup.c ============================================================*/
+extern void Gia_ManDupRemapEquiv( Gia_Man_t * pNew, Gia_Man_t * p );
extern Gia_Man_t * Gia_ManDupOrderDfs( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManDupOrderDfsChoices( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManDupOrderDfsReverse( Gia_Man_t * p );
@@ -824,9 +825,6 @@ extern Gia_Man_t * Gia_ManDupDfs( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManDupDfsSkip( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManDupDfsCone( Gia_Man_t * p, Gia_Obj_t * pObj );
extern Gia_Man_t * Gia_ManDupDfsLitArray( Gia_Man_t * p, Vec_Int_t * vLits );
-extern Gia_Man_t * Gia_ManDupNormalize( Gia_Man_t * p );
-extern Gia_Man_t * Gia_ManDupUnnomalize( Gia_Man_t * p );
-extern Gia_Man_t * Gia_ManDupWithHierarchy( Gia_Man_t * p, Vec_Int_t ** pvNodes );
extern Gia_Man_t * Gia_ManDupTrimmed( Gia_Man_t * p, int fTrimCis, int fTrimCos, int fDualOut, int OutValue );
extern Gia_Man_t * Gia_ManDupOntop( Gia_Man_t * p, Gia_Man_t * p2 );
extern Gia_Man_t * Gia_ManDupWithNewPo( Gia_Man_t * p1, Gia_Man_t * p2 );
@@ -970,6 +968,13 @@ extern Gia_Man_t * Gia_ManSpeedup( Gia_Man_t * p, int Percentage, int De
/*=== giaSwitch.c ============================================================*/
extern float Gia_ManEvaluateSwitching( Gia_Man_t * p );
extern float Gia_ManComputeSwitching( Gia_Man_t * p, int nFrames, int nPref, int fProbOne );
+/*=== giaTim.c ===========================================================*/
+extern Gia_Man_t * Gia_ManDupNormalize( Gia_Man_t * p );
+extern Gia_Man_t * Gia_ManDupUnnomalize( Gia_Man_t * p );
+extern Gia_Man_t * Gia_ManDupWithHierarchy( Gia_Man_t * p, Vec_Int_t ** pvNodes );
+extern Gia_Man_t * Gia_ManDupWithBoxes( Gia_Man_t * p, Gia_Man_t * pBoxes );
+extern int Gia_ManLevelWithBoxes( Gia_Man_t * p );
+extern int Gia_ManVerifyWithBoxes( Gia_Man_t * pGia, void * pParsInit );
/*=== giaTruth.c ===========================================================*/
extern word Gia_ObjComputeTruthTable6( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSupp, Vec_Wrd_t * vTruths );
extern int Gia_ObjCollectInternal( Gia_Man_t * p, Gia_Obj_t * pObj );
diff --git a/src/aig/gia/giaAig.c b/src/aig/gia/giaAig.c
index 5dcc6038..d523c46e 100644
--- a/src/aig/gia/giaAig.c
+++ b/src/aig/gia/giaAig.c
@@ -284,6 +284,7 @@ Aig_Man_t * Gia_ManToAig( Gia_Man_t * p, int fChoices )
// create the new manager
pNew = Aig_ManStart( Gia_ManAndNum(p) );
pNew->pName = Abc_UtilStrsav( p->pName );
+ pNew->pSpec = Abc_UtilStrsav( p->pSpec );
pNew->nConstrs = p->nConstrs;
// pNew->pSpec = Abc_UtilStrsav( p->pName );
// duplicate representation of choice nodes
@@ -331,6 +332,7 @@ Aig_Man_t * Gia_ManToAigSkip( Gia_Man_t * p, int nOutDelta )
// create the new manager
pNew = Aig_ManStart( Gia_ManAndNum(p) );
pNew->pName = Abc_UtilStrsav( p->pName );
+ pNew->pSpec = Abc_UtilStrsav( p->pSpec );
pNew->nConstrs = p->nConstrs;
// pNew->pSpec = Abc_UtilStrsav( p->pName );
// create the PIs
@@ -372,6 +374,7 @@ Aig_Man_t * Gia_ManToAigSimple( Gia_Man_t * p )
// create the new manager
pNew = Aig_ManStart( Gia_ManObjNum(p) );
pNew->pName = Abc_UtilStrsav( p->pName );
+ pNew->pSpec = Abc_UtilStrsav( p->pSpec );
pNew->nConstrs = p->nConstrs;
// create the PIs
Gia_ManForEachObj( p, pObj, i )
@@ -550,11 +553,16 @@ Gia_Man_t * Gia_ManCompress2( Gia_Man_t * p, int fUpdateLevel, int fVerbose )
// extern Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fFanout, int fPower, int fVerbose );
Gia_Man_t * pGia;
Aig_Man_t * pNew, * pTemp;
+ if ( p->pManTime && p->vLevels == NULL )
+ Gia_ManLevelWithBoxes( p );
pNew = Gia_ManToAig( p, 0 );
pNew = Dar_ManCompress2( pTemp = pNew, 1, fUpdateLevel, 1, 0, fVerbose );
Aig_ManStop( pTemp );
pGia = Gia_ManFromAig( pNew );
Aig_ManStop( pNew );
+ pGia->pManTime = p->pManTime; p->pManTime = NULL;
+ pGia->pAigExtra = p->pAigExtra; p->pAigExtra = NULL;
+// Gia_ManLevelWithBoxes( pGia );
return pGia;
}
@@ -578,6 +586,8 @@ Gia_Man_t * Gia_ManPerformDch( Gia_Man_t * p, void * pPars )
// pGia = Gia_ManFromAig( pNew );
pGia = Gia_ManFromAigChoices( pNew );
Aig_ManStop( pNew );
+ pGia->pManTime = p->pManTime; p->pManTime = NULL;
+ pGia->pAigExtra = p->pAigExtra; p->pAigExtra = NULL;
return pGia;
}
diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c
index 48204e8b..476a9d36 100644
--- a/src/aig/gia/giaAiger.c
+++ b/src/aig/gia/giaAiger.c
@@ -495,7 +495,7 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS
// check if there are other types of information to read
if ( pCur + 1 < (unsigned char *)pContents + nFileSize && *pCur == 'c' )
{
- int fVerbose = 1;
+ int fVerbose = 0;
Vec_Str_t * vStr;
unsigned char * pCurTemp;
pCur++;
@@ -619,7 +619,6 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS
pNew->pName = Abc_UtilStrsav( (char *)pCur ); pCur += strlen(pNew->pName) + 1;
assert( pCur == pCurTemp );
}
- if ( fVerbose ) printf( "Finished reading extension \"n\".\n" );
}
// read placement
else if ( *pCur == 'p' )
@@ -708,7 +707,7 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS
{
Tim_ManCreate( (Tim_Man_t *)pNew->pManTime, Abc_FrameReadLibBox(), pNew->vInArrs, pNew->vOutReqs );
// Tim_ManPrint( (Tim_Man_t *)pNew->pManTime );
- printf( "Created timing manager using Tim_ManCreate().\n" );
+// printf( "Created timing manager using Tim_ManCreate().\n" );
}
}
Vec_FltFreeP( &pNew->vInArrs );
@@ -767,11 +766,11 @@ Gia_Man_t * Gia_AigerRead( char * pFileName, int fSkipStrash, int fCheck )
ABC_FREE( pNew->pName );
pName = Gia_FileNameGeneric( pFileName );
pNew->pName = Abc_UtilStrsav( pName );
-// pNew->pSpec = Ioa_UtilStrsav( pFileName );
ABC_FREE( pName );
+
+ assert( pNew->pSpec == NULL );
+ pNew->pSpec = Abc_UtilStrsav( pFileName );
}
- assert( pNew->pSpec == NULL );
- pNew->pSpec = Abc_UtilStrsav( pFileName );
return pNew;
}
@@ -949,6 +948,7 @@ Vec_Str_t * Gia_AigerWriteIntoMemoryStrPart( Gia_Man_t * p, Vec_Int_t * vCis, Ve
***********************************************************************/
void Gia_AigerWrite( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int fCompact )
{
+ int fVerbose = 0;
FILE * pFile;
Gia_Man_t * p;
Gia_Obj_t * pObj;
@@ -1071,6 +1071,7 @@ void Gia_AigerWrite( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int
Gia_FileWriteBufferSize( pFile, Vec_StrSize(vStrExt) );
fwrite( Vec_StrArray(vStrExt), 1, Vec_StrSize(vStrExt), pFile );
Vec_StrFree( vStrExt );
+ if ( fVerbose ) printf( "Finished writing extension \"a\".\n" );
}
/*
// write constraints
@@ -1099,6 +1100,8 @@ void Gia_AigerWrite( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int
Vec_FltFree( vArrTimes );
Vec_FltFree( vReqTimes );
+ if ( fVerbose ) printf( "Finished writing extension \"i\".\n" );
+ if ( fVerbose ) printf( "Finished writing extension \"o\".\n" );
}
}
// write equivalences
@@ -1135,6 +1138,7 @@ void Gia_AigerWrite( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int
Gia_FileWriteBufferSize( pFile, Vec_StrSize(vStrExt) );
fwrite( Vec_StrArray(vStrExt), 1, Vec_StrSize(vStrExt), pFile );
Vec_StrFree( vStrExt );
+ if ( fVerbose ) printf( "Finished writing extension \"h\".\n" );
}
// write packing
if ( p->vPacking )
@@ -1145,6 +1149,7 @@ void Gia_AigerWrite( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int
Gia_FileWriteBufferSize( pFile, Vec_StrSize(vStrExt) );
fwrite( Vec_StrArray(vStrExt), 1, Vec_StrSize(vStrExt), pFile );
Vec_StrFree( vStrExt );
+ if ( fVerbose ) printf( "Finished writing extension \"k\".\n" );
}
// write mapping
if ( p->pMapping )
@@ -1156,6 +1161,7 @@ void Gia_AigerWrite( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int
Gia_FileWriteBufferSize( pFile, Vec_StrSize(vStrExt) );
fwrite( Vec_StrArray(vStrExt), 1, Vec_StrSize(vStrExt), pFile );
Vec_StrFree( vStrExt );
+ if ( fVerbose ) printf( "Finished writing extension \"m\".\n" );
}
// write placement
if ( p->pPlacement )
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index bc1e59f6..14db2492 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -1009,271 +1009,6 @@ Gia_Man_t * Gia_ManDupDfsLitArray( Gia_Man_t * p, Vec_Int_t * vLits )
/**Function*************************************************************
- Synopsis [Duplicates AIG in the DFS order while putting CIs first.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Gia_Man_t * Gia_ManDupNormalize( Gia_Man_t * p )
-{
- Gia_Man_t * pNew;
- Gia_Obj_t * pObj;
- int i;
- Gia_ManFillValue( p );
- pNew = Gia_ManStart( Gia_ManObjNum(p) );
- pNew->pName = Abc_UtilStrsav( p->pName );
- pNew->pSpec = Abc_UtilStrsav( p->pSpec );
- Gia_ManConst0(p)->Value = 0;
- Gia_ManForEachCi( p, pObj, i )
- pObj->Value = Gia_ManAppendCi(pNew);
- Gia_ManForEachAnd( p, pObj, i )
- pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
- Gia_ManForEachCo( p, pObj, i )
- pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
- Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
- assert( Gia_ManIsNormalized(pNew) );
- Gia_ManDupRemapEquiv( pNew, p );
- return pNew;
-}
-
-/**Function*************************************************************
-
- Synopsis [Duplicates AIG according to the timing manager.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Gia_Man_t * Gia_ManDupUnnomalize( Gia_Man_t * p )
-{
- Tim_Man_t * pTime = (Tim_Man_t *)p->pManTime;
- Gia_Man_t * pNew;
- Gia_Obj_t * pObj;
- int i, k, curCi, curCo, curNo, nodeLim;
-//Gia_ManPrint( p );
- assert( pTime != NULL );
- assert( Gia_ManIsNormalized(p) );
- Gia_ManFillValue( p );
- pNew = Gia_ManStart( Gia_ManObjNum(p) );
- pNew->pName = Abc_UtilStrsav( p->pName );
- pNew->pSpec = Abc_UtilStrsav( p->pSpec );
- Gia_ManConst0(p)->Value = 0;
- // copy primary inputs
- for ( k = 0; k < Tim_ManPiNum(pTime); k++ )
- Gia_ManPi(p, k)->Value = Gia_ManAppendCi(pNew);
- curCi = Tim_ManPiNum(pTime);
- curCo = 0;
- curNo = Gia_ManPiNum(p)+1;
- for ( i = 0; i < Tim_ManBoxNum(pTime); i++ )
- {
- // find the latest node feeding into inputs of this box
- nodeLim = -1;
- for ( k = 0; k < Tim_ManBoxInputNum(pTime, i); k++ )
- {
- pObj = Gia_ManPo( p, curCo + k );
- nodeLim = Abc_MaxInt( nodeLim, Gia_ObjFaninId0p(p, pObj)+1 );
- }
- // copy nodes up to the given node
- for ( k = curNo; k < nodeLim; k++ )
- {
- pObj = Gia_ManObj( p, k );
- assert( Gia_ObjIsAnd(pObj) );
- pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
- }
- curNo = Abc_MaxInt( curNo, nodeLim );
- // copy COs
- for ( k = 0; k < Tim_ManBoxInputNum(pTime, i); k++ )
- {
- pObj = Gia_ManPo( p, curCo + k );
- pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
- }
- curCo += Tim_ManBoxInputNum(pTime, i);
- // copy CIs
- for ( k = 0; k < Tim_ManBoxOutputNum(pTime, i); k++ )
- {
- pObj = Gia_ManPi( p, curCi + k );
- pObj->Value = Gia_ManAppendCi(pNew);
- }
- curCi += Tim_ManBoxOutputNum(pTime, i);
- }
- // copy remaining nodes
- nodeLim = Gia_ManObjNum(p) - Gia_ManPoNum(p);
- for ( k = curNo; k < nodeLim; k++ )
- {
- pObj = Gia_ManObj( p, k );
- assert( Gia_ObjIsAnd(pObj) );
- pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
- }
- curNo = Abc_MaxInt( curNo, nodeLim );
- curNo += Gia_ManPoNum(p);
- // copy primary outputs
- for ( k = 0; k < Tim_ManPoNum(pTime); k++ )
- {
- pObj = Gia_ManPo( p, curCo + k );
- pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
- }
- curCo += Tim_ManPoNum(pTime);
- assert( curCi == Gia_ManPiNum(p) );
- assert( curCo == Gia_ManPoNum(p) );
- assert( curNo == Gia_ManObjNum(p) );
- Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
- Gia_ManDupRemapEquiv( pNew, p );
-//Gia_ManPrint( pNew );
- // pass the timing manager
- pNew->pManTime = pTime; p->pManTime = NULL;
- return pNew;
-}
-
-
-/**Function*************************************************************
-
- Synopsis [Find the ordering of AIG objects.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Gia_ManDupFindOrderWithHie_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vNodes )
-{
- if ( Gia_ObjIsTravIdCurrent(p, pObj) )
- return;
- Gia_ObjSetTravIdCurrent(p, pObj);
- assert( Gia_ObjIsAnd(pObj) );
- Gia_ManDupFindOrderWithHie_rec( p, Gia_ObjFanin0(pObj), vNodes );
- Gia_ManDupFindOrderWithHie_rec( p, Gia_ObjFanin1(pObj), vNodes );
- Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
-}
-Vec_Int_t * Gia_ManDupFindOrderWithHie( Gia_Man_t * p )
-{
- Tim_Man_t * pTime = (Tim_Man_t *)p->pManTime;
- Vec_Int_t * vNodes;
- Gia_Obj_t * pObj;
- int i, k, curCi, curCo;
- assert( p->pManTime != NULL );
- assert( Gia_ManIsNormalized( p ) );
- // start trav IDs
- Gia_ManIncrementTravId( p );
- // start the array
- vNodes = Vec_IntAlloc( Gia_ManObjNum(p) );
- // include constant
- Vec_IntPush( vNodes, 0 );
- Gia_ObjSetTravIdCurrent( p, Gia_ManConst0(p) );
- // include primary inputs
- for ( i = 0; i < Tim_ManPiNum(pTime); i++ )
- {
- pObj = Gia_ManPi( p, i );
- Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
- Gia_ObjSetTravIdCurrent( p, pObj );
- assert( Gia_ObjId(p, pObj) == i+1 );
-//printf( "%d ", Gia_ObjId(p, pObj) );
- }
- // for each box, include box nodes
- curCi = Tim_ManPiNum(pTime);
- curCo = 0;
- for ( i = 0; i < Tim_ManBoxNum(pTime); i++ )
- {
-//printf( "Box %d:\n", i );
- // add internal nodes
- for ( k = 0; k < Tim_ManBoxInputNum(pTime, i); k++ )
- {
- pObj = Gia_ManPo( p, curCo + k );
-//Gia_ObjPrint( p, pObj );
-//printf( "Fanin " );
-//Gia_ObjPrint( p, Gia_ObjFanin0(pObj) );
- Gia_ManDupFindOrderWithHie_rec( p, Gia_ObjFanin0(pObj), vNodes );
- }
- // add POs corresponding to box inputs
- for ( k = 0; k < Tim_ManBoxInputNum(pTime, i); k++ )
- {
- pObj = Gia_ManPo( p, curCo + k );
- Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
- }
- curCo += Tim_ManBoxInputNum(pTime, i);
- // add PIs corresponding to box outputs
- for ( k = 0; k < Tim_ManBoxOutputNum(pTime, i); k++ )
- {
- pObj = Gia_ManPi( p, curCi + k );
-//Gia_ObjPrint( p, pObj );
- Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
- Gia_ObjSetTravIdCurrent( p, pObj );
- }
- curCi += Tim_ManBoxOutputNum(pTime, i);
- }
- // add remaining nodes
- for ( i = Tim_ManCoNum(pTime) - Tim_ManPoNum(pTime); i < Tim_ManCoNum(pTime); i++ )
- {
- pObj = Gia_ManPo( p, i );
- Gia_ManDupFindOrderWithHie_rec( p, Gia_ObjFanin0(pObj), vNodes );
- }
- // add POs
- for ( i = Tim_ManCoNum(pTime) - Tim_ManPoNum(pTime); i < Tim_ManCoNum(pTime); i++ )
- {
- pObj = Gia_ManPo( p, i );
- Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
- }
- curCo += Tim_ManPoNum(pTime);
- // verify counts
- assert( curCi == Gia_ManPiNum(p) );
- assert( curCo == Gia_ManPoNum(p) );
- assert( Vec_IntSize(vNodes) == Gia_ManObjNum(p) );
- return vNodes;
-}
-
-/**Function*************************************************************
-
- Synopsis [Duplicates AIG according to the timing manager.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Gia_Man_t * Gia_ManDupWithHierarchy( Gia_Man_t * p, Vec_Int_t ** pvNodes )
-{
- Vec_Int_t * vNodes;
- Gia_Man_t * pNew;
- Gia_Obj_t * pObj;
- int i;
- Gia_ManFillValue( p );
- pNew = Gia_ManStart( Gia_ManObjNum(p) );
- pNew->pName = Abc_UtilStrsav( p->pName );
- pNew->pSpec = Abc_UtilStrsav( p->pSpec );
- vNodes = Gia_ManDupFindOrderWithHie( p );
- Gia_ManForEachObjVec( vNodes, p, pObj, i )
- {
- if ( Gia_ObjIsAnd(pObj) )
- pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
- else if ( Gia_ObjIsCi(pObj) )
- pObj->Value = Gia_ManAppendCi( pNew );
- else if ( Gia_ObjIsCo(pObj) )
- pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
- else if ( Gia_ObjIsConst0(pObj) )
- pObj->Value = 0;
- else assert( 0 );
- }
- Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
- if ( pvNodes )
- *pvNodes = vNodes;
- else
- Vec_IntFree( vNodes );
- return pNew;
-}
-
-
-/**Function*************************************************************
-
Synopsis [Returns the array of non-const-0 POs of the dual-output miter.]
Description []
diff --git a/src/aig/gia/giaIf.c b/src/aig/gia/giaIf.c
index 19c2fe0b..b05e9106 100644
--- a/src/aig/gia/giaIf.c
+++ b/src/aig/gia/giaIf.c
@@ -720,7 +720,7 @@ void Gia_ManTransferMapping( Gia_Man_t * pGia, Gia_Man_t * p )
SideEffects []
- SeeAlso []
+ SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManPerformMapping( Gia_Man_t * p, void * pp )
@@ -733,7 +733,8 @@ Gia_Man_t * Gia_ManPerformMapping( Gia_Man_t * p, void * pp )
if ( p->pManTime )
{
pNew = Gia_ManDupWithHierarchy( p, &vNodes );
- pNew->pManTime = p->pManTime; p->pManTime = NULL;
+ pNew->pManTime = p->pManTime; p->pManTime = NULL;
+ pNew->pAigExtra = p->pAigExtra; p->pAigExtra = NULL;
p = pNew;
}
else
@@ -769,13 +770,20 @@ Gia_Man_t * Gia_ManPerformMapping( Gia_Man_t * p, void * pp )
// if ( pIfMan->pPars->fDelayOpt )
// Vec_IntFreeP( &pNew->vMapping );
// return the original (unmodified by the mapper) timing manager
- pNew->pManTime = p->pManTime; p->pManTime = NULL;
+ pNew->pManTime = p->pManTime; p->pManTime = NULL;
+ pNew->pAigExtra = p->pAigExtra; p->pAigExtra = NULL;
Gia_ManStop( p );
// normalize and transfer mapping
- p = Gia_ManDupNormalize( pNew );
- Gia_ManTransferMapping( pNew, p );
- Gia_ManStop( pNew );
- return p;
+ pNew = Gia_ManDupNormalize( p = pNew );
+ Gia_ManTransferMapping( p, pNew );
+ pNew->pManTime = p->pManTime; p->pManTime = NULL;
+ pNew->pAigExtra = p->pAigExtra; p->pAigExtra = NULL;
+ Gia_ManStop( p );
+
+// printf( "PERFORMING VERIFICATION:\n" );
+// Gia_ManVerifyWithBoxes( pNew, NULL );
+
+ return pNew;
}
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/gia/giaTim.c b/src/aig/gia/giaTim.c
new file mode 100644
index 00000000..10841216
--- /dev/null
+++ b/src/aig/gia/giaTim.c
@@ -0,0 +1,550 @@
+/**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 $]
+
+***********************************************************************/
+
+#include "gia.h"
+#include "misc/tim/tim.h"
+#include "proof/cec/cec.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Duplicates AIG in the DFS order while putting CIs first.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManDupNormalize( Gia_Man_t * p )
+{
+ Gia_Man_t * pNew;
+ Gia_Obj_t * pObj;
+ int i;
+ Gia_ManFillValue( p );
+ pNew = Gia_ManStart( Gia_ManObjNum(p) );
+ pNew->pName = Abc_UtilStrsav( p->pName );
+ pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+ Gia_ManConst0(p)->Value = 0;
+ Gia_ManForEachCi( p, pObj, i )
+ pObj->Value = Gia_ManAppendCi(pNew);
+ Gia_ManForEachAnd( p, pObj, i )
+ pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+ Gia_ManForEachCo( p, pObj, i )
+ pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+ Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+ assert( Gia_ManIsNormalized(pNew) );
+ Gia_ManDupRemapEquiv( pNew, p );
+ return pNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Duplicates AIG according to the timing manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManDupUnnomalize( Gia_Man_t * p )
+{
+ Tim_Man_t * pTime = (Tim_Man_t *)p->pManTime;
+ Gia_Man_t * pNew;
+ Gia_Obj_t * pObj;
+ int i, k, curCi, curCo, curNo, nodeLim;
+//Gia_ManPrint( p );
+ assert( pTime != NULL );
+ assert( Gia_ManIsNormalized(p) );
+ Gia_ManFillValue( p );
+ pNew = Gia_ManStart( Gia_ManObjNum(p) );
+ pNew->pName = Abc_UtilStrsav( p->pName );
+ pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+ Gia_ManConst0(p)->Value = 0;
+ // copy primary inputs
+ for ( k = 0; k < Tim_ManPiNum(pTime); k++ )
+ Gia_ManPi(p, k)->Value = Gia_ManAppendCi(pNew);
+ curCi = Tim_ManPiNum(pTime);
+ curCo = 0;
+ curNo = Gia_ManPiNum(p)+1;
+ for ( i = 0; i < Tim_ManBoxNum(pTime); i++ )
+ {
+ // find the latest node feeding into inputs of this box
+ nodeLim = -1;
+ for ( k = 0; k < Tim_ManBoxInputNum(pTime, i); k++ )
+ {
+ pObj = Gia_ManPo( p, curCo + k );
+ nodeLim = Abc_MaxInt( nodeLim, Gia_ObjFaninId0p(p, pObj)+1 );
+ }
+ // copy nodes up to the given node
+ for ( k = curNo; k < nodeLim; k++ )
+ {
+ pObj = Gia_ManObj( p, k );
+ assert( Gia_ObjIsAnd(pObj) );
+ pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+ }
+ curNo = Abc_MaxInt( curNo, nodeLim );
+ // copy COs
+ for ( k = 0; k < Tim_ManBoxInputNum(pTime, i); k++ )
+ {
+ pObj = Gia_ManPo( p, curCo + k );
+ pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+ }
+ curCo += Tim_ManBoxInputNum(pTime, i);
+ // copy CIs
+ for ( k = 0; k < Tim_ManBoxOutputNum(pTime, i); k++ )
+ {
+ pObj = Gia_ManPi( p, curCi + k );
+ pObj->Value = Gia_ManAppendCi(pNew);
+ }
+ curCi += Tim_ManBoxOutputNum(pTime, i);
+ }
+ // copy remaining nodes
+ nodeLim = Gia_ManObjNum(p) - Gia_ManPoNum(p);
+ for ( k = curNo; k < nodeLim; k++ )
+ {
+ pObj = Gia_ManObj( p, k );
+ assert( Gia_ObjIsAnd(pObj) );
+ pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+ }
+ curNo = Abc_MaxInt( curNo, nodeLim );
+ curNo += Gia_ManPoNum(p);
+ // copy primary outputs
+ for ( k = 0; k < Tim_ManPoNum(pTime); k++ )
+ {
+ pObj = Gia_ManPo( p, curCo + k );
+ pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+ }
+ curCo += Tim_ManPoNum(pTime);
+ assert( curCi == Gia_ManPiNum(p) );
+ assert( curCo == Gia_ManPoNum(p) );
+ assert( curNo == Gia_ManObjNum(p) );
+ Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+ Gia_ManDupRemapEquiv( pNew, p );
+//Gia_ManPrint( pNew );
+ // pass the timing manager
+ pNew->pManTime = pTime; p->pManTime = NULL;
+ return pNew;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Find the ordering of AIG objects.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Gia_ManDupFindOrderWithHie_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vNodes )
+{
+ if ( Gia_ObjIsTravIdCurrent(p, pObj) )
+ return;
+ Gia_ObjSetTravIdCurrent(p, pObj);
+ assert( Gia_ObjIsAnd(pObj) );
+ Gia_ManDupFindOrderWithHie_rec( p, Gia_ObjFanin0(pObj), vNodes );
+ Gia_ManDupFindOrderWithHie_rec( p, Gia_ObjFanin1(pObj), vNodes );
+ Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
+}
+Vec_Int_t * Gia_ManDupFindOrderWithHie( Gia_Man_t * p )
+{
+ Tim_Man_t * pTime = (Tim_Man_t *)p->pManTime;
+ Vec_Int_t * vNodes;
+ Gia_Obj_t * pObj;
+ int i, k, curCi, curCo;
+ assert( p->pManTime != NULL );
+ assert( Gia_ManIsNormalized( p ) );
+ // start trav IDs
+ Gia_ManIncrementTravId( p );
+ // start the array
+ vNodes = Vec_IntAlloc( Gia_ManObjNum(p) );
+ // include constant
+ Vec_IntPush( vNodes, 0 );
+ Gia_ObjSetTravIdCurrent( p, Gia_ManConst0(p) );
+ // include primary inputs
+ for ( i = 0; i < Tim_ManPiNum(pTime); i++ )
+ {
+ pObj = Gia_ManPi( p, i );
+ Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
+ Gia_ObjSetTravIdCurrent( p, pObj );
+ assert( Gia_ObjId(p, pObj) == i+1 );
+//printf( "%d ", Gia_ObjId(p, pObj) );
+ }
+ // for each box, include box nodes
+ curCi = Tim_ManPiNum(pTime);
+ curCo = 0;
+ for ( i = 0; i < Tim_ManBoxNum(pTime); i++ )
+ {
+//printf( "Box %d:\n", i );
+ // add internal nodes
+ for ( k = 0; k < Tim_ManBoxInputNum(pTime, i); k++ )
+ {
+ pObj = Gia_ManPo( p, curCo + k );
+//Gia_ObjPrint( p, pObj );
+//printf( "Fanin " );
+//Gia_ObjPrint( p, Gia_ObjFanin0(pObj) );
+ Gia_ManDupFindOrderWithHie_rec( p, Gia_ObjFanin0(pObj), vNodes );
+ }
+ // add POs corresponding to box inputs
+ for ( k = 0; k < Tim_ManBoxInputNum(pTime, i); k++ )
+ {
+ pObj = Gia_ManPo( p, curCo + k );
+ Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
+ }
+ curCo += Tim_ManBoxInputNum(pTime, i);
+ // add PIs corresponding to box outputs
+ for ( k = 0; k < Tim_ManBoxOutputNum(pTime, i); k++ )
+ {
+ pObj = Gia_ManPi( p, curCi + k );
+//Gia_ObjPrint( p, pObj );
+ Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
+ Gia_ObjSetTravIdCurrent( p, pObj );
+ }
+ curCi += Tim_ManBoxOutputNum(pTime, i);
+ }
+ // add remaining nodes
+ for ( i = Tim_ManCoNum(pTime) - Tim_ManPoNum(pTime); i < Tim_ManCoNum(pTime); i++ )
+ {
+ pObj = Gia_ManPo( p, i );
+ Gia_ManDupFindOrderWithHie_rec( p, Gia_ObjFanin0(pObj), vNodes );
+ }
+ // add POs
+ for ( i = Tim_ManCoNum(pTime) - Tim_ManPoNum(pTime); i < Tim_ManCoNum(pTime); i++ )
+ {
+ pObj = Gia_ManPo( p, i );
+ Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
+ }
+ curCo += Tim_ManPoNum(pTime);
+ // verify counts
+ assert( curCi == Gia_ManPiNum(p) );
+ assert( curCo == Gia_ManPoNum(p) );
+ assert( Vec_IntSize(vNodes) == Gia_ManObjNum(p) );
+ return vNodes;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Duplicates AIG according to the timing manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManDupWithHierarchy( Gia_Man_t * p, Vec_Int_t ** pvNodes )
+{
+ Vec_Int_t * vNodes;
+ Gia_Man_t * pNew;
+ Gia_Obj_t * pObj;
+ int i;
+ Gia_ManFillValue( p );
+ pNew = Gia_ManStart( Gia_ManObjNum(p) );
+ pNew->pName = Abc_UtilStrsav( p->pName );
+ pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+ vNodes = Gia_ManDupFindOrderWithHie( p );
+ Gia_ManForEachObjVec( vNodes, p, pObj, i )
+ {
+ if ( Gia_ObjIsAnd(pObj) )
+ pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+ else if ( Gia_ObjIsCi(pObj) )
+ pObj->Value = Gia_ManAppendCi( pNew );
+ else if ( Gia_ObjIsCo(pObj) )
+ pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+ else if ( Gia_ObjIsConst0(pObj) )
+ pObj->Value = 0;
+ else assert( 0 );
+ }
+ Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+ if ( pvNodes )
+ *pvNodes = vNodes;
+ else
+ Vec_IntFree( vNodes );
+ return pNew;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Gia_ManDupWithBoxes_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Man_t * pNew )
+{
+ if ( Gia_ObjIsTravIdCurrent(p, pObj) )
+ return;
+ Gia_ObjSetTravIdCurrent(p, pObj);
+ assert( Gia_ObjIsAnd(pObj) );
+ Gia_ManDupWithBoxes_rec( p, Gia_ObjFanin0(pObj), pNew );
+ Gia_ManDupWithBoxes_rec( p, Gia_ObjFanin1(pObj), pNew );
+// assert( !~pObj->Value );
+ pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+}
+Gia_Man_t * Gia_ManDupWithBoxes( Gia_Man_t * p, Gia_Man_t * pBoxes )
+{
+ Tim_Man_t * pTime = (Tim_Man_t *)p->pManTime;
+ Gia_Man_t * pNew, * pTemp;
+ Gia_Obj_t * pObj, * pObjBox;
+ int i, k, curCi, curCo;
+ assert( Gia_ManRegNum(p) == 0 );
+ assert( Gia_ManPiNum(p) == Tim_ManPiNum(pTime) + Gia_ManPoNum(pBoxes) );
+ pNew = Gia_ManStart( Gia_ManObjNum(p) );
+ pNew->pName = Abc_UtilStrsav( p->pName );
+ pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+ Gia_ManHashAlloc( pNew );
+ // copy const and real PIs
+ Gia_ManFillValue( p );
+ Gia_ManConst0(p)->Value = 0;
+ Gia_ManIncrementTravId( p );
+ Gia_ObjSetTravIdCurrent( p, Gia_ManConst0(p) );
+ for ( i = 0; i < Tim_ManPiNum(pTime); i++ )
+ {
+ pObj = Gia_ManPi( p, i );
+ pObj->Value = Gia_ManAppendCi(pNew);
+ Gia_ObjSetTravIdCurrent( p, pObj );
+ }
+ // create logic for each box
+ curCi = Tim_ManPiNum(pTime);
+ curCo = 0;
+ for ( i = 0; i < Tim_ManBoxNum(pTime); i++ )
+ {
+ // clean boxes
+ Gia_ManIncrementTravId( pBoxes );
+ Gia_ObjSetTravIdCurrent( pBoxes, Gia_ManConst0(pBoxes) );
+ Gia_ManConst0(pBoxes)->Value = 0;
+ // add internal nodes
+ for ( k = 0; k < Tim_ManBoxInputNum(pTime, i); k++ )
+ {
+ // build logic
+ pObj = Gia_ManPo( p, curCo + k );
+ Gia_ManDupWithBoxes_rec( p, Gia_ObjFanin0(pObj), pNew );
+ // transfer to the PI
+ pObjBox = Gia_ManPi( pBoxes, k );
+ pObjBox->Value = Gia_ObjFanin0Copy(pObj);
+ Gia_ObjSetTravIdCurrent( pBoxes, pObjBox );
+ }
+ curCo += Tim_ManBoxInputNum(pTime, i);
+ // add internal nodes
+ for ( k = 0; k < Tim_ManBoxOutputNum(pTime, i); k++ )
+ {
+ // build logic
+ pObjBox = Gia_ManPo( pBoxes, curCi - Tim_ManPiNum(pTime) + k );
+ Gia_ManDupWithBoxes_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 );
+ }
+ curCi += Tim_ManBoxOutputNum(pTime, i);
+ }
+ // add remaining nodes
+ for ( i = Tim_ManCoNum(pTime) - Tim_ManPoNum(pTime); i < Tim_ManCoNum(pTime); i++ )
+ {
+ pObj = Gia_ManPo( p, i );
+ Gia_ManDupWithBoxes_rec( p, Gia_ObjFanin0(pObj), pNew );
+ pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+ }
+ curCo += Tim_ManPoNum(pTime);
+ // verify counts
+ assert( curCi == Gia_ManPiNum(p) );
+ assert( curCo == Gia_ManPoNum(p) );
+ Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+ Gia_ManHashStop( pNew );
+ pNew = Gia_ManCleanup( pTemp = pNew );
+ Gia_ManStop( pTemp );
+ assert( Tim_ManPoNum(pTime) == Gia_ManPoNum(pNew) );
+ assert( Tim_ManPiNum(pTime) == Gia_ManPiNum(pNew) );
+ return pNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Gia_ManLevelWithBoxes_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+ if ( Gia_ObjIsTravIdCurrent(p, pObj) )
+ return;
+ Gia_ObjSetTravIdCurrent(p, pObj);
+ assert( Gia_ObjIsAnd(pObj) );
+ Gia_ManLevelWithBoxes_rec( p, Gia_ObjFanin0(pObj) );
+ Gia_ManLevelWithBoxes_rec( p, Gia_ObjFanin1(pObj) );
+ Gia_ObjSetAndLevel( p, pObj );
+}
+int Gia_ManLevelWithBoxes( Gia_Man_t * p )
+{
+ Tim_Man_t * pTime = (Tim_Man_t *)p->pManTime;
+ Gia_Obj_t * pObj;
+ int i, k, curCi, curCo, LevelMax;
+ assert( Gia_ManRegNum(p) == 0 );
+ // copy const and real PIs
+ Gia_ManCleanLevels( p, Gia_ManObjNum(p) );
+ Gia_ObjSetLevel( p, Gia_ManConst0(p), 0 );
+ Gia_ManIncrementTravId( p );
+ Gia_ObjSetTravIdCurrent( p, Gia_ManConst0(p) );
+ for ( i = 0; i < Tim_ManPiNum(pTime); i++ )
+ {
+ pObj = Gia_ManPi( p, i );
+// Gia_ObjSetLevel( p, pObj, Tim_ManGetCiArrival(pTime, i) );
+ Gia_ObjSetLevel( p, pObj, 0 );
+ Gia_ObjSetTravIdCurrent( p, pObj );
+ }
+ // create logic for each box
+ curCi = Tim_ManPiNum(pTime);
+ curCo = 0;
+ for ( i = 0; i < Tim_ManBoxNum(pTime); i++ )
+ {
+ LevelMax = 0;
+ for ( k = 0; k < Tim_ManBoxInputNum(pTime, i); k++ )
+ {
+ pObj = Gia_ManPo( p, curCo + k );
+ Gia_ManLevelWithBoxes_rec( p, Gia_ObjFanin0(pObj) );
+ Gia_ObjSetCoLevel( p, pObj );
+ LevelMax = Abc_MaxInt( LevelMax, Gia_ObjLevel(p, pObj) );
+ }
+ curCo += Tim_ManBoxInputNum(pTime, i);
+ LevelMax++;
+ for ( k = 0; k < Tim_ManBoxOutputNum(pTime, i); k++ )
+ {
+ pObj = Gia_ManPi( p, curCi + k );
+ Gia_ObjSetLevel( p, pObj, LevelMax );
+ Gia_ObjSetTravIdCurrent( p, pObj );
+ }
+ curCi += Tim_ManBoxOutputNum(pTime, i);
+ }
+ // add remaining nodes
+ p->nLevels = 0;
+ for ( i = Tim_ManCoNum(pTime) - Tim_ManPoNum(pTime); i < Tim_ManCoNum(pTime); i++ )
+ {
+ pObj = Gia_ManPo( p, i );
+ Gia_ManLevelWithBoxes_rec( p, Gia_ObjFanin0(pObj) );
+ Gia_ObjSetCoLevel( p, pObj );
+ p->nLevels = Abc_MaxInt( p->nLevels, Gia_ObjLevel(p, pObj) );
+ }
+ curCo += Tim_ManPoNum(pTime);
+ // verify counts
+ assert( curCi == Gia_ManPiNum(p) );
+ assert( curCo == Gia_ManPoNum(p) );
+// printf( "Max level is %d.\n", p->nLevels );
+ return p->nLevels;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Gia_ManVerifyWithBoxes( Gia_Man_t * pGia, void * pParsInit )
+{
+ int fVerbose = 1;
+ int Status = -1;
+ Gia_Man_t * pSpec, * pGia0, * pGia1, * pMiter;
+ if ( pGia->pSpec == NULL )
+ {
+ printf( "Spec file is not given. Use standard flow.\n" );
+ return Status;
+ }
+ if ( pGia->pManTime == NULL )
+ {
+ printf( "Design has no tim manager. Use standard flow.\n" );
+ return Status;
+ }
+ if ( pGia->pAigExtra == NULL )
+ {
+ printf( "Design has no box logic. Use standard flow.\n" );
+ return Status;
+ }
+ // read original AIG
+ pSpec = Gia_AigerRead( pGia->pSpec, 0, 0 );
+ if ( pSpec->pManTime == NULL )
+ {
+ printf( "Spec has no tim manager. Use standard flow.\n" );
+ return Status;
+ }
+ if ( pSpec->pAigExtra == NULL )
+ {
+ printf( "Spec has no box logic. Use standard flow.\n" );
+ return Status;
+ }
+ pGia0 = Gia_ManDupWithBoxes( pSpec, pSpec->pAigExtra );
+ pGia1 = Gia_ManDupWithBoxes( pGia, pGia->pAigExtra );
+ // compute the miter
+ pMiter = Gia_ManMiter( pGia0, pGia1, 1, 0, fVerbose );
+ if ( pMiter )
+ {
+ Cec_ParCec_t ParsCec, * pPars = &ParsCec;
+ Cec_ManCecSetDefaultParams( pPars );
+ pPars->fVerbose = fVerbose;
+ if ( pParsInit )
+ memcpy( pPars, pParsInit, sizeof(Cec_ParCec_t) );
+ Status = Cec_ManVerify( pMiter, pPars );
+ Gia_ManStop( pMiter );
+ if ( pPars->iOutFail >= 0 )
+ Abc_Print( 1, "Verification failed for at least one output (%d).\n", pPars->iOutFail );
+ }
+ Gia_ManStop( pGia0 );
+ Gia_ManStop( pGia1 );
+ Gia_ManStop( pSpec );
+ return Status;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make
index 947cdc08..169b71e7 100644
--- a/src/aig/gia/module.make
+++ b/src/aig/gia/module.make
@@ -38,6 +38,7 @@ SRC += src/aig/gia/gia.c \
src/aig/gia/giaSupMin.c \
src/aig/gia/giaSwitch.c \
src/aig/gia/giaTest.c \
+ src/aig/gia/giaTim.c \
src/aig/gia/giaTruth.c \
src/aig/gia/giaTsim.c \
src/aig/gia/giaUtil.c
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index aca047c4..b35eab98 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -351,6 +351,7 @@ static int Abc_CommandAbc9Filter ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandAbc9Reduce ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9EquivMark ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Cec ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Verify ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Force ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Embed ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9If ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -811,6 +812,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&reduce", Abc_CommandAbc9Reduce, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&equiv_mark", Abc_CommandAbc9EquivMark, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&cec", Abc_CommandAbc9Cec, 0 );
+ Cmd_CommandAdd( pAbc, "ABC9", "&verify", Abc_CommandAbc9Verify, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&force", Abc_CommandAbc9Force, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&embed", Abc_CommandAbc9Embed, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&if", Abc_CommandAbc9If, 0 );
@@ -27221,6 +27223,71 @@ usage:
SeeAlso []
***********************************************************************/
+int Abc_CommandAbc9Verify( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ Cec_ParCec_t ParsCec, * pPars = &ParsCec;
+ int c;
+ Cec_ManCecSetDefaultParams( pPars );
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "CTvh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'C':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nBTLimit = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nBTLimit < 0 )
+ goto usage;
+ break;
+ case 'T':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->TimeLimit = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->TimeLimit < 0 )
+ goto usage;
+ break;
+ case 'v':
+ pPars->fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ Gia_ManVerifyWithBoxes( pAbc->pGia, pPars );
+ return 0;
+
+usage:
+ Abc_Print( -2, "usage: &verify [-CT num] [-vh]\n" );
+ Abc_Print( -2, "\t performs verification of combinational design\n" );
+ Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
+ Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", pPars->TimeLimit );
+ Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes":"no");
+ Abc_Print( -2, "\t-h : print the command usage\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Abc_CommandAbc9Force( Abc_Frame_t * pAbc, int argc, char ** argv )
{
int nIters = 20;
@@ -27399,6 +27466,7 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "LUT library is not given. Using default LUT library.\n" );
pAbc->pLibLut = If_LibLutSetSimple( 6 );
}
+ pPars->pLutLib = pAbc->pLibLut;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "KCFAGDEWSqaflepmrsdbgyojikcvh" ) ) != EOF )
{
@@ -27716,6 +27784,11 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Truth tables cannot be computed for LUT larger than %d inputs.\n", IF_MAX_FUNC_LUTSIZE );
return 1;
}
+ if ( pAbc->pGia->pManTime && pAbc->pLibBox == NULL )
+ {
+ Abc_Print( -1, "Design has boxes but box library is not entered.\n" );
+ return 1;
+ }
// perform mapping
pNew = Gia_ManPerformMapping( pAbc->pGia, pPars );
@@ -30418,7 +30491,8 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
// extern void Bmc_CexTest( Gia_Man_t * p, Abc_Cex_t * pCex, int fVerbose );
// extern void Gia_IsoTest( Gia_Man_t * p, Abc_Cex_t * pCex, int fVerbose );
// extern void Unr_ManTest( Gia_Man_t * pGia );
- extern void Mig_ManTest( Gia_Man_t * pGia );
+// extern void Mig_ManTest( Gia_Man_t * pGia );
+// extern int Gia_ManVerify( Gia_Man_t * pGia );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "svh" ) ) != EOF )
@@ -30468,7 +30542,8 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
// Bmc_CexTest( pAbc->pGia, pAbc->pCex, fVerbose );
// Gia_IsoTest( pAbc->pGia, pAbc->pCex, 0 );
// Unr_ManTest( pAbc->pGia );
- Mig_ManTest( pAbc->pGia );
+// Mig_ManTest( pAbc->pGia );
+// Gia_ManVerifyWithBoxes( pAbc->pGia );
return 0;
usage:
Abc_Print( -2, "usage: &test [-svh]\n" );
diff --git a/src/misc/tim/timMan.c b/src/misc/tim/timMan.c
index 8900fda4..f2245a6a 100644
--- a/src/misc/tim/timMan.c
+++ b/src/misc/tim/timMan.c
@@ -132,7 +132,7 @@ Tim_Man_t * Tim_ManDup( Tim_Man_t * p, int fUnitDelay )
// assert( (int)pDelayTableNew[0] == Vec_PtrSize(pNew->vDelayTables) );
assert( Vec_PtrEntry(pNew->vDelayTables, i) == NULL );
Vec_PtrWriteEntry( pNew->vDelayTables, i, pDelayTableNew );
-printf( "Finished duplicating delay table %d.\n", i );
+//printf( "Finished duplicating delay table %d.\n", i );
}
}
// duplicate boxes
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-04 12:42:00 +0000