summaryrefslogtreecommitdiffstats
path: root/src/aig
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig')
-rw-r--r--src/aig/aig/aigDfs.c7
-rw-r--r--src/aig/ntl/ntl.h5
-rw-r--r--src/aig/ntl/ntlEc.c7
-rw-r--r--src/aig/ntl/ntlExtract.c10
-rw-r--r--src/aig/ntl/ntlReadBlif.c42
-rw-r--r--src/aig/ntl/ntlSweep.c6
-rw-r--r--src/aig/ntl/ntlWriteBlif.c2
-rw-r--r--src/aig/nwk/nwkDfs.c12
8 files changed, 86 insertions, 5 deletions
diff --git a/src/aig/aig/aigDfs.c b/src/aig/aig/aigDfs.c
index 9f7d286d..47597f93 100644
--- a/src/aig/aig/aigDfs.c
+++ b/src/aig/aig/aigDfs.c
@@ -448,6 +448,13 @@ int Aig_ManChoiceLevel( Aig_Man_t * p )
if ( LevelMax < Aig_ObjLevel(pObj) )
LevelMax = Aig_ObjLevel(pObj);
}
+ // account for dangling boxes
+ Aig_ManForEachPi( p, pObj, i )
+ {
+ Aig_ManChoiceLevel_rec( p, pObj );
+ if ( LevelMax < Aig_ObjLevel(pObj) )
+ LevelMax = Aig_ObjLevel(pObj);
+ }
Aig_ManCleanPioNumbers( p );
// Aig_ManForEachNode( p, pObj, i )
// assert( Aig_ObjLevel(pObj) > 0 );
diff --git a/src/aig/ntl/ntl.h b/src/aig/ntl/ntl.h
index 1028bd97..659f6c60 100644
--- a/src/aig/ntl/ntl.h
+++ b/src/aig/ntl/ntl.h
@@ -86,6 +86,7 @@ struct Ntl_Mod_t_
Vec_Ptr_t * vPis; // the array of PI objects
Vec_Ptr_t * vPos; // the array of PO objects
int nObjs[NTL_OBJ_VOID]; // counter of objects of each type
+ int fKeep; // indicates persistant model
// hashing names into nets
Ntl_Net_t ** pTable; // the hash table of names into nets
int nTableSize; // the allocated table size
@@ -219,9 +220,9 @@ static inline void Ntl_ObjSetFanout( Ntl_Obj_t * p, Ntl_Net_t * pNet, int
for ( pNet = pNwk->pTable[i]; pNet; pNet = pNet->pNext )
#define Ntl_ObjForEachFanin( pObj, pFanin, i ) \
- for ( i = 0; (i < (pObj)->nFanins) && ((pFanin) = (pObj)->pFanio[i]); i++ )
+ for ( i = 0; (i < (pObj)->nFanins) && (((pFanin) = (pObj)->pFanio[i]), 1); i++ )
#define Ntl_ObjForEachFanout( pObj, pFanout, i ) \
- for ( i = 0; (i < (pObj)->nFanouts) && ((pFanout) = (pObj)->pFanio[(pObj)->nFanins+i]); i++ )
+ for ( i = 0; (i < (pObj)->nFanouts) && (((pFanout) = (pObj)->pFanio[(pObj)->nFanins+i]), 1); i++ )
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
diff --git a/src/aig/ntl/ntlEc.c b/src/aig/ntl/ntlEc.c
index 0cd75cbc..8c7f7156 100644
--- a/src/aig/ntl/ntlEc.c
+++ b/src/aig/ntl/ntlEc.c
@@ -226,6 +226,13 @@ void Ntl_ManPrepareCec( char * pFileName1, char * pFileName2, Aig_Man_t ** ppMan
}
// normalize inputs/outputs
Ntl_ManCreateMissingInputs( pModel1, pModel2, 0 );
+ if ( Ntl_ModelCiNum(pModel1) != Ntl_ModelCiNum(pModel2) )
+ {
+ if ( pMan1 ) Ntl_ManFree( pMan1 );
+ if ( pMan2 ) Ntl_ManFree( pMan2 );
+ printf( "Ntl_ManPrepareCec(): Cannot verify designs with too many different CIs.\n" );
+ return;
+ }
Ntl_ManDeriveCommonCis( pMan1, pMan2, 0 );
Ntl_ManDeriveCommonCos( pMan1, pMan2, 0 );
if ( Vec_PtrSize(pMan1->vCos) == 0 )
diff --git a/src/aig/ntl/ntlExtract.c b/src/aig/ntl/ntlExtract.c
index 69219282..a6fb58ae 100644
--- a/src/aig/ntl/ntlExtract.c
+++ b/src/aig/ntl/ntlExtract.c
@@ -289,6 +289,16 @@ Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p )
Vec_PtrPush( p->vCos, pNet );
Aig_ObjCreatePo( p->pAig, pNet->pCopy );
}
+ // visit dangling boxes
+ Ntl_ModelForEachBox( pRoot, pObj, i )
+ {
+ pNet = Ntl_ObjFanout0(pObj);
+ if ( !Ntl_ManExtract_rec( p, pNet ) )
+ {
+ printf( "Ntl_ManExtract(): Error: Combinational loop is detected.\n" );
+ return 0;
+ }
+ }
// report the number of dangling objects
nUselessObjects = Ntl_ModelNodeNum(pRoot) + Ntl_ModelLut1Num(pRoot) + Ntl_ModelBoxNum(pRoot) - Vec_PtrSize(p->vNodes);
// if ( nUselessObjects )
diff --git a/src/aig/ntl/ntlReadBlif.c b/src/aig/ntl/ntlReadBlif.c
index 13050047..cac53058 100644
--- a/src/aig/ntl/ntlReadBlif.c
+++ b/src/aig/ntl/ntlReadBlif.c
@@ -31,6 +31,7 @@ struct Ioa_ReadMod_t_
{
// file lines
char * pFirst; // .model line
+ char * pAttrib; // .attrib line
Vec_Ptr_t * vInputs; // .inputs lines
Vec_Ptr_t * vOutputs; // .outputs lines
Vec_Ptr_t * vLatches; // .latch lines
@@ -78,6 +79,7 @@ static void Ioa_ReadReadPreparse( Ioa_ReadMan_t * p );
static int Ioa_ReadReadInterfaces( Ioa_ReadMan_t * p );
static Ntl_Man_t * Ioa_ReadParse( Ioa_ReadMan_t * p );
static int Ioa_ReadParseLineModel( Ioa_ReadMod_t * p, char * pLine );
+static int Ioa_ReadParseLineAttrib( Ioa_ReadMod_t * p, char * pLine );
static int Ioa_ReadParseLineInputs( Ioa_ReadMod_t * p, char * pLine );
static int Ioa_ReadParseLineOutputs( Ioa_ReadMod_t * p, char * pLine );
static int Ioa_ReadParseLineLatch( Ioa_ReadMod_t * p, char * pLine );
@@ -519,6 +521,8 @@ static void Ioa_ReadReadPreparse( Ioa_ReadMan_t * p )
p->pLatest->pFirst = pCur;
p->pLatest->pMan = p;
}
+ else if ( !strncmp(pCur, "attrib", 6) )
+ p->pLatest->pAttrib = pCur;
else if ( !strncmp(pCur, "end", 3) )
{
if ( p->pLatest )
@@ -562,6 +566,9 @@ static int Ioa_ReadReadInterfaces( Ioa_ReadMan_t * p )
// parse the model
if ( !Ioa_ReadParseLineModel( pMod, pMod->pFirst ) )
return 0;
+ // parse the model attributes
+ if ( pMod->pAttrib && !Ioa_ReadParseLineAttrib( pMod, pMod->pAttrib ) )
+ return 0;
// parse the inputs
Vec_PtrForEachEntry( pMod->vInputs, pLine, k )
if ( !Ioa_ReadParseLineInputs( pMod, pLine ) )
@@ -651,7 +658,7 @@ static int Ioa_ReadParseLineModel( Ioa_ReadMod_t * p, char * pLine )
assert( !strcmp(pToken, "model") );
if ( Vec_PtrSize(vTokens) != 2 )
{
- sprintf( p->pMan->sError, "Line %d: The number of entries in .model line (%d) is different from two.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrSize(vTokens) );
+ sprintf( p->pMan->sError, "Line %d: The number of entries (%d) in .model line is different from two.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrSize(vTokens) );
return 0;
}
p->pNtk = Ntl_ModelAlloc( p->pMan->pDesign, Vec_PtrEntry(vTokens, 1) );
@@ -660,6 +667,39 @@ static int Ioa_ReadParseLineModel( Ioa_ReadMod_t * p, char * pLine )
/**Function*************************************************************
+ Synopsis [Parses the model line.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static int Ioa_ReadParseLineAttrib( Ioa_ReadMod_t * p, char * pLine )
+{
+ Vec_Ptr_t * vTokens = p->pMan->vTokens;
+ char * pToken;
+ Ioa_ReadSplitIntoTokens( vTokens, pLine, '\0' );
+ pToken = Vec_PtrEntry( vTokens, 0 );
+ assert( !strcmp(pToken, "attrib") );
+ if ( Vec_PtrSize(vTokens) != 2 )
+ {
+ sprintf( p->pMan->sError, "Line %d: The number of entries (%d) in .attrib line is different from two.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrSize(vTokens) );
+ return 0;
+ }
+ if ( strcmp( Vec_PtrEntry(vTokens, 1), "keep" ) == 0 )
+ p->pNtk->fKeep = 1;
+ else
+ {
+ sprintf( p->pMan->sError, "Line %d: Unknown attribute (%s) in the .attrib line of model %s.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens, 1), p->pNtk->pName );
+ return 0;
+ }
+ return 1;
+}
+
+/**Function*************************************************************
+
Synopsis [Parses the inputs line.]
Description []
diff --git a/src/aig/ntl/ntlSweep.c b/src/aig/ntl/ntlSweep.c
index 000b8f0a..ed602297 100644
--- a/src/aig/ntl/ntlSweep.c
+++ b/src/aig/ntl/ntlSweep.c
@@ -77,11 +77,15 @@ void Ntl_ManSweepMark( Ntl_Man_t * p )
// start from the primary outputs
Ntl_ModelForEachPo( pRoot, pObj, i )
Ntl_ManSweepMark_rec( p, pObj );
+ // start from the persistant boxes
+ Ntl_ModelForEachBox( pRoot, pObj, i )
+ if ( pObj->pImplem->fKeep )
+ Ntl_ManSweepMark_rec( p, pObj );
}
/**Function*************************************************************
- Synopsis [Derives new netlist by sweeping current netlist with the current AIG.]
+ Synopsis [Removes logic that does not fanout into POs.]
Description []
diff --git a/src/aig/ntl/ntlWriteBlif.c b/src/aig/ntl/ntlWriteBlif.c
index ed45fcaf..9814ed5d 100644
--- a/src/aig/ntl/ntlWriteBlif.c
+++ b/src/aig/ntl/ntlWriteBlif.c
@@ -47,6 +47,8 @@ void Ioa_WriteBlifModel( FILE * pFile, Ntl_Mod_t * pModel )
float Delay;
int i, k, fClockAdded = 0;
fprintf( pFile, ".model %s\n", pModel->pName );
+ if ( pModel->fKeep )
+ fprintf( pFile, ".attrib keep\n" );
fprintf( pFile, ".inputs" );
Ntl_ModelForEachPi( pModel, pObj, i )
fprintf( pFile, " %s", Ntl_ObjFanout0(pObj)->pName );
diff --git a/src/aig/nwk/nwkDfs.c b/src/aig/nwk/nwkDfs.c
index 90bab0dc..ec4ad440 100644
--- a/src/aig/nwk/nwkDfs.c
+++ b/src/aig/nwk/nwkDfs.c
@@ -222,6 +222,12 @@ int Nwk_ManLevel( Nwk_Man_t * pNtk )
if ( LevelMax < Nwk_ObjLevel(pObj) )
LevelMax = Nwk_ObjLevel(pObj);
}
+ Nwk_ManForEachCi( pNtk, pObj, i )
+ {
+ Nwk_ManLevel_rec( pObj );
+ if ( LevelMax < Nwk_ObjLevel(pObj) )
+ LevelMax = Nwk_ObjLevel(pObj);
+ }
return LevelMax;
}
@@ -297,7 +303,7 @@ void Nwk_ManDfs_rec( Nwk_Obj_t * pObj, Vec_Ptr_t * vNodes )
Nwk_ManDfs_rec( pNext, vNodes );
Vec_PtrPush( vNodes, pObj );
}
-
+
/**Function*************************************************************
Synopsis [Returns the DFS ordered array of all objects except latches.]
@@ -448,6 +454,10 @@ Vec_Ptr_t * Nwk_ManDfsReverse( Nwk_Man_t * pNtk )
vNodes = Vec_PtrAlloc( 100 );
Nwk_ManForEachPi( pNtk, pObj, i )
Nwk_ManDfsReverse_rec( pObj, vNodes );
+ // add nodes without fanins
+ Nwk_ManForEachNode( pNtk, pObj, i )
+ if ( Nwk_ObjFaninNum(pObj) == 0 && !Nwk_ObjIsTravIdCurrent(pObj) )
+ Vec_PtrPush( vNodes, pObj );
return vNodes;
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-08-18 10:39:36 +0000