summaryrefslogtreecommitdiffstats
path: root/src/base/ver
diff options
context:
space:
mode:
Diffstat (limited to 'src/base/ver')
-rw-r--r--src/base/ver/ver.h2
-rw-r--r--src/base/ver/verCore.c1583
-rw-r--r--src/base/ver/verCore.zipbin0 -> 13275 bytes
-rw-r--r--src/base/ver/verFormula.c4
4 files changed, 1215 insertions, 374 deletions
diff --git a/src/base/ver/ver.h b/src/base/ver/ver.h
index 0ba081db..cf2b7497 100644
--- a/src/base/ver/ver.h
+++ b/src/base/ver/ver.h
@@ -56,6 +56,7 @@ struct Ver_Man_t_
ProgressBar * pProgress;
// current design
Abc_Lib_t * pDesign;
+ st_table * tName2Suffix;
// error handling
FILE * Output;
int fTopLevel;
@@ -67,6 +68,7 @@ struct Ver_Man_t_
Vec_Int_t * vStackOp;
};
+
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/base/ver/verCore.c b/src/base/ver/verCore.c
index 6c036288..89f9a689 100644
--- a/src/base/ver/verCore.c
+++ b/src/base/ver/verCore.c
@@ -61,18 +61,29 @@ static int Ver_ParseGateStandard( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Ver_GateT
static int Ver_ParseGate( Ver_Man_t * p, Abc_Ntk_t * pNtk, Mio_Gate_t * pGate );
static int Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox );
static int Ver_ParseConnectBox( Ver_Man_t * pMan, Abc_Obj_t * pBox );
-static int Vec_ParseAttachBoxes( Ver_Man_t * pMan );
+static int Ver_ParseAttachBoxes( Ver_Man_t * pMan );
static Abc_Obj_t * Ver_ParseCreatePi( Abc_Ntk_t * pNtk, char * pName );
static Abc_Obj_t * Ver_ParseCreatePo( Abc_Ntk_t * pNtk, char * pName );
static Abc_Obj_t * Ver_ParseCreateLatch( Abc_Ntk_t * pNtk, Abc_Obj_t * pNetLI, Abc_Obj_t * pNetLO );
static Abc_Obj_t * Ver_ParseCreateInv( Abc_Ntk_t * pNtk, Abc_Obj_t * pNet );
+static void Ver_ParseRemoveSuffixTable( Ver_Man_t * pMan );
+
static inline int Ver_NtkIsDefined( Abc_Ntk_t * pNtkBox ) { assert( pNtkBox->pName ); return Abc_NtkPiNum(pNtkBox) || Abc_NtkPoNum(pNtkBox); }
static inline int Ver_ObjIsConnected( Abc_Obj_t * pObj ) { assert( Abc_ObjIsBox(pObj) ); return Abc_ObjFaninNum(pObj) || Abc_ObjFanoutNum(pObj); }
+//static inline Abc_Obj_t * Abc_NtkCreateNet( Abc_Ntk_t * pNtk ) { return Abc_NtkCreateObj( pNtk, ABC_OBJ_NET ); }
+
int glo_fMapped = 0; // this is bad!
+typedef struct Ver_Bundle_t_ Ver_Bundle_t;
+struct Ver_Bundle_t_
+{
+ char * pNameFormal; // the name of the formal net
+ Vec_Ptr_t * vNetsActual; // the vector of actual nets (MSB to LSB)
+};
+
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@@ -201,7 +212,7 @@ void Ver_ParseInternal( Ver_Man_t * pMan )
}
// process defined and undefined boxes
- if ( !Vec_ParseAttachBoxes( pMan ) )
+ if ( !Ver_ParseAttachBoxes( pMan ) )
return;
// connect the boxes and check
@@ -213,7 +224,7 @@ void Ver_ParseInternal( Ver_Man_t * pMan )
if ( pMan->fCheck && !Abc_NtkCheckRead( pNtk ) )
{
pMan->fTopLevel = 1;
- sprintf( pMan->sError, "The network check has failed.", pNtk->pName );
+ sprintf( pMan->sError, "The network check has failed for network %s.", pNtk->pName );
Ver_ParsePrintErrorMessage( pMan );
return;
}
@@ -391,7 +402,7 @@ int Ver_ParseModule( Ver_Man_t * pMan )
// make sure we stopped at the opening paranthesis
if ( Ver_StreamPopChar(p) != '(' )
{
- sprintf( pMan->sError, "Cannot find \"(\" after \"module\".", pNtk->pName );
+ sprintf( pMan->sError, "Cannot find \"(\" after \"module\" in network %s.", pNtk->pName );
Ver_ParsePrintErrorMessage( pMan );
return 0;
}
@@ -406,7 +417,12 @@ int Ver_ParseModule( Ver_Man_t * pMan )
if ( !Ver_ParseSkipComments( pMan ) )
return 0;
Symbol = Ver_StreamPopChar(p);
- assert( Symbol == ';' );
+ if ( Symbol != ';' )
+ {
+ sprintf( pMan->sError, "Expected closing paranthesis after \"module\"." );
+ Ver_ParsePrintErrorMessage( pMan );
+ return 0;
+ }
// parse the inputs/outputs/registers/wires/inouts
while ( 1 )
@@ -508,12 +524,88 @@ int Ver_ParseModule( Ver_Man_t * pMan )
}
}
}
+
+ // remove the table if needed
+ Ver_ParseRemoveSuffixTable( pMan );
return 1;
}
+
/**Function*************************************************************
- Synopsis [Parses one directive.]
+ Synopsis [Lookups the suffix of the signal of the form [m:n].]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ver_ParseLookupSuffix( Ver_Man_t * pMan, char * pWord, int * pnMsb, int * pnLsb )
+{
+ unsigned Value;
+ *pnMsb = *pnLsb = -1;
+ if ( pMan->tName2Suffix == NULL )
+ return 1;
+ if ( !st_lookup( pMan->tName2Suffix, (char *)pWord, (char **)&Value ) )
+ return 1;
+ *pnMsb = (Value >> 8) & 0xff;
+ *pnLsb = Value & 0xff;
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Lookups the suffix of the signal of the form [m:n].]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ver_ParseInsertsSuffix( Ver_Man_t * pMan, char * pWord, int nMsb, int nLsb )
+{
+ unsigned Value;
+ if ( pMan->tName2Suffix == NULL )
+ pMan->tName2Suffix = st_init_table( strcmp, st_strhash );
+ if ( st_is_member( pMan->tName2Suffix, pWord ) )
+ return 1;
+ assert( nMsb >= 0 && nMsb < 128 );
+ assert( nLsb >= 0 && nLsb < 128 );
+ Value = (nMsb << 8) | nLsb;
+ st_insert( pMan->tName2Suffix, Extra_UtilStrsav(pWord), (char *)Value );
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Lookups the suffic of the signal of the form [m:n].]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ver_ParseRemoveSuffixTable( Ver_Man_t * pMan )
+{
+ st_generator * gen;
+ char * pKey, * pValue;
+ if ( pMan->tName2Suffix == NULL )
+ return;
+ st_foreach_item( pMan->tName2Suffix, gen, (char **)&pKey, (char **)&pValue )
+ free( pKey );
+ st_free_table( pMan->tName2Suffix );
+ pMan->tName2Suffix = NULL;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Determine signal prefix of the form [Beg:End].]
Description []
@@ -522,16 +614,172 @@ int Ver_ParseModule( Ver_Man_t * pMan )
SeeAlso []
***********************************************************************/
+int Ver_ParseSignalPrefix( Ver_Man_t * pMan, char ** ppWord, int * pnMsb, int * pnLsb )
+{
+ char * pWord = *ppWord;
+ int nMsb, nLsb;
+ assert( pWord[0] == '[' );
+ // get the beginning
+ nMsb = atoi( pWord + 1 );
+ // find the splitter
+ while ( *pWord && *pWord != ':' && *pWord != ']' )
+ pWord++;
+ if ( *pWord == 0 )
+ {
+ sprintf( pMan->sError, "Cannot find closing bracket in this line." );
+ Ver_ParsePrintErrorMessage( pMan );
+ return 0;
+ }
+ if ( *pWord == ']' )
+ nLsb = nMsb;
+ else
+ {
+ assert( *pWord == ':' );
+ nLsb = atoi( pWord + 1 );
+ // find the closing paranthesis
+ while ( *pWord && *pWord != ']' )
+ pWord++;
+ if ( *pWord == 0 )
+ {
+ sprintf( pMan->sError, "Cannot find closing bracket in this line." );
+ Ver_ParsePrintErrorMessage( pMan );
+ return 0;
+ }
+ assert( *pWord == ']' );
+ pWord++;
+ }
+ assert( nMsb >= 0 && nLsb >= 0 );
+ // return
+ *ppWord = pWord;
+ *pnMsb = nMsb;
+ *pnLsb = nLsb;
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Determine signal suffix of the form [m:n].]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ver_ParseSignalSuffix( Ver_Man_t * pMan, char * pWord, int * pnMsb, int * pnLsb )
+{
+ char * pCur;
+ int Length;
+ Length = strlen(pWord);
+ assert( pWord[Length-1] == ']' );
+ // walk backward
+ for ( pCur = pWord + Length - 2; pCur != pWord; pCur-- )
+ if ( *pCur == ':' || *pCur == '[' )
+ break;
+ if ( pCur == pWord )
+ {
+ sprintf( pMan->sError, "Cannot find opening bracket in signal name %s.", pWord );
+ Ver_ParsePrintErrorMessage( pMan );
+ return 0;
+ }
+ if ( *pCur == '[' )
+ {
+ *pnMsb = *pnLsb = atoi(pCur+1);
+ *pCur = 0;
+ return 1;
+ }
+ assert( *pCur == ':' );
+ // get the end of the interval
+ *pnLsb = atoi(pCur+1);
+ // find the beginning
+ for ( pCur = pWord + Length - 2; pCur != pWord; pCur-- )
+ if ( *pCur == '[' )
+ break;
+ if ( pCur == pWord )
+ {
+ sprintf( pMan->sError, "Cannot find opening bracket in signal name %s.", pWord );
+ Ver_ParsePrintErrorMessage( pMan );
+ return 0;
+ }
+ assert( *pCur == '[' );
+ // get the beginning of the interval
+ *pnMsb = atoi(pCur+1);
+ // cut the word
+ *pCur = 0;
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns the values of constant bits.]
+
+ Description [The resulting bits are in MSB to LSB order.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ver_ParseConstant( Ver_Man_t * pMan, char * pWord )
+{
+ int nBits, i;
+ assert( pWord[0] >= '1' && pWord[1] <= '9' );
+ nBits = atoi(pWord);
+ // find the next symbol \'
+ while ( *pWord && *pWord != '\'' )
+ pWord++;
+ if ( *pWord == 0 )
+ {
+ sprintf( pMan->sError, "Cannot find symbol \' in the constant." );
+ Ver_ParsePrintErrorMessage( pMan );
+ return 0;
+ }
+ assert( *pWord == '\'' );
+ pWord++;
+ if ( *pWord != 'b' )
+ {
+ sprintf( pMan->sError, "Currently can only handle binary constants." );
+ Ver_ParsePrintErrorMessage( pMan );
+ return 0;
+ }
+ pWord++;
+ // scan the bits
+ Vec_PtrClear( pMan->vNames );
+ for ( i = 0; i < nBits; i++ )
+ {
+ if ( pWord[i] != '0' && pWord[i] != '1' )
+ {
+ sprintf( pMan->sError, "Having problem parsing the binary constant." );
+ Ver_ParsePrintErrorMessage( pMan );
+ return 0;
+ }
+ Vec_PtrPush( pMan->vNames, (void *)(pWord[i]-'0') );
+ }
+ return 1;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Parses one directive.]
+
+ Description [The signals are added in the order from LSB to MSB.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Ver_ParseSignal( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Ver_SignalType_t SigType )
{
Ver_Stream_t * p = pMan->pReader;
- char Buffer[1000];
- int Lower, Upper, i;
- char * pWord;
- char Symbol;
- Lower = Upper = 0;
+ char Buffer[1000], Symbol, * pWord;
+ int nMsb, nLsb, Bit, Limit, i;
+ nMsb = nLsb = -1;
while ( 1 )
{
+ // get the next word
pWord = Ver_ParseGetName( pMan );
if ( pWord == NULL )
return 0;
@@ -539,39 +787,11 @@ int Ver_ParseSignal( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Ver_SignalType_t SigTyp
// check if the range is specified
if ( pWord[0] == '[' && !pMan->fNameLast )
{
- Lower = atoi( pWord + 1 );
- // find the splitter
- while ( *pWord && *pWord != ':' && *pWord != ']' )
- pWord++;
+ assert( nMsb == -1 && nLsb == -1 );
+ Ver_ParseSignalPrefix( pMan, &pWord, &nMsb, &nLsb );
+ // check the case when there is space between bracket and the next word
if ( *pWord == 0 )
{
- sprintf( pMan->sError, "Cannot find closing bracket in this line." );
- Ver_ParsePrintErrorMessage( pMan );
- return 0;
- }
- if ( *pWord == ']' )
- Upper = Lower;
- else
- {
- Upper = atoi( pWord + 1 );
- if ( Lower > Upper )
- i = Lower, Lower = Upper, Upper = i;
- // find the closing paranthesis
- while ( *pWord && *pWord != ']' )
- pWord++;
- if ( *pWord == 0 )
- {
- sprintf( pMan->sError, "Cannot find closing bracket in this line." );
- Ver_ParsePrintErrorMessage( pMan );
- return 0;
- }
- assert( *pWord == ']' );
- }
- // check the case of no space between bracket and the next word
- if ( *(pWord+1) != 0 )
- pWord++;
- else
- {
// get the signal name
pWord = Ver_ParseGetName( pMan );
if ( pWord == NULL )
@@ -580,7 +800,7 @@ int Ver_ParseSignal( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Ver_SignalType_t SigTyp
}
// create signals
- if ( Lower == 0 && Upper == 0 )
+ if ( nMsb == -1 && nLsb == -1 )
{
if ( SigType == VER_SIG_INPUT || SigType == VER_SIG_INOUT )
Ver_ParseCreatePi( pNtk, pWord );
@@ -591,9 +811,14 @@ int Ver_ParseSignal( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Ver_SignalType_t SigTyp
}
else
{
- for ( i = Lower; i <= Upper; i++ )
+ assert( nMsb >= 0 && nLsb >= 0 );
+ // add to the hash table
+ Ver_ParseInsertsSuffix( pMan, pWord, nMsb, nLsb );
+ // add signals from Lsb to Msb
+ Limit = nMsb > nLsb? nMsb - nLsb + 1: nLsb - nMsb + 1;
+ for ( i = 0, Bit = nLsb; i < Limit; i++, Bit = nMsb > nLsb ? Bit + 1: Bit - 1 )
{
- sprintf( Buffer, "%s[%d]", pWord, i );
+ sprintf( Buffer, "%s[%d]", pWord, Bit );
if ( SigType == VER_SIG_INPUT || SigType == VER_SIG_INOUT )
Ver_ParseCreatePi( pNtk, Buffer );
if ( SigType == VER_SIG_OUTPUT || SigType == VER_SIG_INOUT )
@@ -823,12 +1048,14 @@ int Ver_ParseInitial( Ver_Man_t * pMan, Abc_Ntk_t * pNtk )
***********************************************************************/
int Ver_ParseAssign( Ver_Man_t * pMan, Abc_Ntk_t * pNtk )
{
+ char Buffer[1000], Buffer2[1000];
Ver_Stream_t * p = pMan->pReader;
Abc_Obj_t * pNode, * pNet;
char * pWord, * pName, * pEquation;
Hop_Obj_t * pFunc;
char Symbol;
- int i, Length, fReduction;
+ int i, Bit, Limit, Length, fReduction;
+ int nMsb, nLsb;
// if ( Ver_StreamGetLineNumber(p) == 2756 )
// {
@@ -845,102 +1072,171 @@ int Ver_ParseAssign( Ver_Man_t * pMan, Abc_Ntk_t * pNtk )
pWord = Ver_ParseGetName( pMan );
if ( pWord == NULL )
return 0;
- // consider the case of reduction operations
- fReduction = 0;
- if ( pWord[0] == '{' && !pMan->fNameLast )
- fReduction = 1;
- if ( fReduction )
- {
- pWord++;
- pWord[strlen(pWord)-1] = 0;
- assert( pWord[0] != '\\' );
- }
- // get the fanout net
- pNet = Ver_ParseFindNet( pNtk, pWord );
- if ( pNet == NULL )
- {
- sprintf( pMan->sError, "Cannot read the assign statement for %s (output wire is not defined).", pWord );
- Ver_ParsePrintErrorMessage( pMan );
- return 0;
- }
- // get the equality sign
- if ( Ver_StreamPopChar(p) != '=' )
- {
- sprintf( pMan->sError, "Cannot read the assign statement for %s (expected equality sign).", pWord );
- Ver_ParsePrintErrorMessage( pMan );
- return 0;
- }
- // skip the comments
- if ( !Ver_ParseSkipComments( pMan ) )
+ // check for vector-inputs
+ if ( !Ver_ParseLookupSuffix( pMan, pWord, &nMsb, &nLsb ) )
return 0;
- // get the second name
- if ( fReduction )
- pEquation = Ver_StreamGetWord( p, ";" );
- else
- pEquation = Ver_StreamGetWord( p, ",;" );
- if ( pEquation == NULL )
+ // handle special case of constant assignment
+ if ( nMsb >= 0 && nLsb >= 0 )
{
- sprintf( pMan->sError, "Cannot read the equation for %s.", Abc_ObjName(pNet) );
- Ver_ParsePrintErrorMessage( pMan );
- return 0;
- }
+ // save the fanout name
+ strcpy( Buffer, pWord );
+ // get the equality sign
+ if ( Ver_StreamPopChar(p) != '=' )
+ {
+ sprintf( pMan->sError, "Cannot read the assign statement for %s (expected equality sign).", pWord );
+ Ver_ParsePrintErrorMessage( pMan );
+ return 0;
+ }
+ // get the constant
+ pWord = Ver_ParseGetName( pMan );
+ if ( pWord == NULL )
+ return 0;
+ // check if it is indeed a constant
+ if ( !(pWord[0] >= '0' && pWord[0] <= '9') )
+ {
+ sprintf( pMan->sError, "Currently can only assign vector-signal \"%s\" to be a constant.", Buffer );
+ Ver_ParsePrintErrorMessage( pMan );
+ return 0;
+ }
- // consider the case of mapped network
- if ( pMan->fMapped )
- {
- Vec_PtrClear( pMan->vNames );
- if ( !strcmp( pEquation, "1\'b0" ) )
- pFunc = (Hop_Obj_t *)Mio_LibraryReadConst0(Abc_FrameReadLibGen());
- else if ( !strcmp( pEquation, "1\'b1" ) )
- pFunc = (Hop_Obj_t *)Mio_LibraryReadConst1(Abc_FrameReadLibGen());
- else
+ // set individual bits of the constant
+ if ( !Ver_ParseConstant( pMan, pWord ) )
+ return 0;
+ // check that the constant has the same size
+ Limit = nMsb > nLsb? nMsb - nLsb + 1: nLsb - nMsb + 1;
+ if ( Limit != Vec_PtrSize(pMan->vNames) )
+ {
+ sprintf( pMan->sError, "The constant size (%d) is different from the signal\"%s\" size (%d).",
+ Vec_PtrSize(pMan->vNames), Buffer, Limit );
+ Ver_ParsePrintErrorMessage( pMan );
+ return 0;
+ }
+ // iterate through the bits
+ for ( i = 0, Bit = nLsb; i < Limit; i++, Bit = nMsb > nLsb ? Bit + 1: Bit - 1 )
{
- if ( Ver_ParseFindNet(pNtk, pEquation) == NULL )
+ // get the fanin net
+ if ( Vec_PtrEntry( pMan->vNames, Limit-1-i ) )
+ pNet = Ver_ParseFindNet( pNtk, "1\'b1" );
+ else
+ pNet = Ver_ParseFindNet( pNtk, "1\'b0" );
+ assert( pNet != NULL );
+
+ // create the buffer
+ pNode = Abc_NtkCreateNodeBuf( pNtk, pNet );
+
+ // get the fanout net
+ sprintf( Buffer2, "%s[%d]", Buffer, Bit );
+ pNet = Ver_ParseFindNet( pNtk, Buffer2 );
+ if ( pNet == NULL )
{
- sprintf( pMan->sError, "Cannot read Verilog with non-trivail assignments in the mapped netlist.", pEquation );
+ sprintf( pMan->sError, "Cannot read the assign statement for %s (output wire is not defined).", pWord );
Ver_ParsePrintErrorMessage( pMan );
return 0;
}
- Vec_PtrPush( pMan->vNames, (void *)strlen(pEquation) );
- Vec_PtrPush( pMan->vNames, pEquation );
- // get the buffer
- pFunc = (Hop_Obj_t *)Mio_LibraryReadBuf(Abc_FrameReadLibGen());
+ Abc_ObjAddFanin( pNet, pNode );
}
+ // go to the end of the line
+ Ver_ParseSkipComments( pMan );
}
else
{
- // parse the formula
+ // consider the case of reduction operations
+ fReduction = 0;
+ if ( pWord[0] == '{' && !pMan->fNameLast )
+ fReduction = 1;
if ( fReduction )
- pFunc = Ver_FormulaReduction( pEquation, pNtk->pManFunc, pMan->vNames, pMan->sError );
- else
- pFunc = Ver_FormulaParser( pEquation, pNtk->pManFunc, pMan->vNames, pMan->vStackFn, pMan->vStackOp, pMan->sError );
- if ( pFunc == NULL )
{
+ pWord++;
+ pWord[strlen(pWord)-1] = 0;
+ assert( pWord[0] != '\\' );
+ }
+ // get the fanout net
+ pNet = Ver_ParseFindNet( pNtk, pWord );
+ if ( pNet == NULL )
+ {
+ sprintf( pMan->sError, "Cannot read the assign statement for %s (output wire is not defined).", pWord );
Ver_ParsePrintErrorMessage( pMan );
return 0;
}
- }
-
- // create the node with the given inputs
- pNode = Abc_NtkCreateNode( pNtk );
- pNode->pData = pFunc;
- Abc_ObjAddFanin( pNet, pNode );
- // connect to fanin nets
- for ( i = 0; i < Vec_PtrSize(pMan->vNames)/2; i++ )
- {
- // get the name of this signal
- Length = (int)Vec_PtrEntry( pMan->vNames, 2*i );
- pName = Vec_PtrEntry( pMan->vNames, 2*i + 1 );
- pName[Length] = 0;
- // find the corresponding net
- pNet = Ver_ParseFindNet( pNtk, pName );
- if ( pNet == NULL )
+ // get the equality sign
+ if ( Ver_StreamPopChar(p) != '=' )
{
- sprintf( pMan->sError, "Cannot read the assign statement for %s (input wire %d is not defined).", pWord, pName );
+ sprintf( pMan->sError, "Cannot read the assign statement for %s (expected equality sign).", pWord );
Ver_ParsePrintErrorMessage( pMan );
return 0;
}
- Abc_ObjAddFanin( pNode, pNet );
+ // skip the comments
+ if ( !Ver_ParseSkipComments( pMan ) )
+ return 0;
+ // get the second name
+ if ( fReduction )
+ pEquation = Ver_StreamGetWord( p, ";" );
+ else
+ pEquation = Ver_StreamGetWord( p, ",;" );
+ if ( pEquation == NULL )
+ {
+ sprintf( pMan->sError, "Cannot read the equation for %s.", Abc_ObjName(pNet) );
+ Ver_ParsePrintErrorMessage( pMan );
+ return 0;
+ }
+
+ // consider the case of mapped network
+ if ( pMan->fMapped )
+ {
+ Vec_PtrClear( pMan->vNames );
+ if ( !strcmp( pEquation, "1\'b0" ) )
+ pFunc = (Hop_Obj_t *)Mio_LibraryReadConst0(Abc_FrameReadLibGen());
+ else if ( !strcmp( pEquation, "1\'b1" ) )
+ pFunc = (Hop_Obj_t *)Mio_LibraryReadConst1(Abc_FrameReadLibGen());
+ else
+ {
+ if ( Ver_ParseFindNet(pNtk, pEquation) == NULL )
+ {
+ sprintf( pMan->sError, "Cannot read Verilog with non-trivial assignments in the mapped netlist." );
+ Ver_ParsePrintErrorMessage( pMan );
+ return 0;
+ }
+ Vec_PtrPush( pMan->vNames, (void *)strlen(pEquation) );
+ Vec_PtrPush( pMan->vNames, pEquation );
+ // get the buffer
+ pFunc = (Hop_Obj_t *)Mio_LibraryReadBuf(Abc_FrameReadLibGen());
+ }
+ }
+ else
+ {
+ // parse the formula
+ if ( fReduction )
+ pFunc = Ver_FormulaReduction( pEquation, pNtk->pManFunc, pMan->vNames, pMan->sError );
+ else
+ pFunc = Ver_FormulaParser( pEquation, pNtk->pManFunc, pMan->vNames, pMan->vStackFn, pMan->vStackOp, pMan->sError );
+ if ( pFunc == NULL )
+ {
+ Ver_ParsePrintErrorMessage( pMan );
+ return 0;
+ }
+ }
+
+ // create the node with the given inputs
+ pNode = Abc_NtkCreateNode( pNtk );
+ pNode->pData = pFunc;
+ Abc_ObjAddFanin( pNet, pNode );
+ // connect to fanin nets
+ for ( i = 0; i < Vec_PtrSize(pMan->vNames)/2; i++ )
+ {
+ // get the name of this signal
+ Length = (int)Vec_PtrEntry( pMan->vNames, 2*i );
+ pName = Vec_PtrEntry( pMan->vNames, 2*i + 1 );
+ pName[Length] = 0;
+ // find the corresponding net
+ pNet = Ver_ParseFindNet( pNtk, pName );
+ if ( pNet == NULL )
+ {
+ sprintf( pMan->sError, "Cannot read the assign statement for %s (input wire %s is not defined).", pWord, pName );
+ Ver_ParsePrintErrorMessage( pMan );
+ return 0;
+ }
+ Abc_ObjAddFanin( pNode, pNet );
+ }
}
Symbol = Ver_StreamPopChar(p);
@@ -1229,19 +1525,21 @@ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Mio_Gate_t * pGate )
***********************************************************************/
int Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox )
{
+ char Buffer[1000];
Ver_Stream_t * p = pMan->pReader;
- Vec_Ptr_t * vNetPairs;
- Abc_Obj_t * pNetFormal, * pNetActual;
+ Ver_Bundle_t * pBundle;
+ Vec_Ptr_t * vBundles;
+ Abc_Obj_t * pNetActual;
Abc_Obj_t * pNode;
char * pWord, Symbol;
- int fCompl;
+ int fCompl, fFormalIsGiven;
- // parse the directive and set the pointers to the PIs/POs of the gate
+ // gate the name of the box
pWord = Ver_ParseGetName( pMan );
if ( pWord == NULL )
return 0;
- // create box to represent this gate
+ // create a box with this name
pNode = Abc_NtkCreateBlackbox( pNtk );
pNode->pData = pNtkBox;
Abc_ObjAssignName( pNode, pWord, NULL );
@@ -1253,50 +1551,174 @@ int Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox )
Ver_ParsePrintErrorMessage( pMan );
return 0;
}
-
+ Ver_ParseSkipComments( pMan );
+
// parse pairs of formal/actural inputs
- vNetPairs = Vec_PtrAlloc( 16 );
- pNode->pCopy = (Abc_Obj_t *)vNetPairs;
+ vBundles = Vec_PtrAlloc( 16 );
+ pNode->pCopy = (Abc_Obj_t *)vBundles;
while ( 1 )
{
+ // allocate the bundle (formal name + array of actual nets)
+ pBundle = ALLOC( Ver_Bundle_t, 1 );
+ pBundle->pNameFormal = NULL;
+ pBundle->vNetsActual = Vec_PtrAlloc( 4 );
+ Vec_PtrPush( vBundles, pBundle );
+
// process one pair of formal/actual parameters
- if ( Ver_StreamPopChar(p) != '.' )
+ fFormalIsGiven = 0;
+ if ( Ver_StreamScanChar(p) == '.' )
{
- sprintf( pMan->sError, "Cannot parse gate %s (expected .).", Abc_ObjName(pNode) );
- Ver_ParsePrintErrorMessage( pMan );
- return 0;
- }
+ fFormalIsGiven = 1;
+ if ( Ver_StreamPopChar(p) != '.' )
+ {
+ sprintf( pMan->sError, "Cannot parse gate %s (expected .).", Abc_ObjName(pNode) );
+ Ver_ParsePrintErrorMessage( pMan );
+ return 0;
+ }
- // parse the formal name
- pWord = Ver_ParseGetName( pMan );
- if ( pWord == NULL )
- return 0;
- // get the formal net
- pNetFormal = Abc_NtkFindOrCreateNet( pNtkBox, pWord );
- Vec_PtrPush( vNetPairs, pNetFormal );
+ // parse the formal name
+ pWord = Ver_ParseGetName( pMan );
+ if ( pWord == NULL )
+ return 0;
- // open the paranthesis
- if ( Ver_StreamPopChar(p) != '(' )
- {
- sprintf( pMan->sError, "Cannot formal parameter %s of gate %s (expected opening paranthesis).", pWord, Abc_ObjName(pNode));
- Ver_ParsePrintErrorMessage( pMan );
- return 0;
+ // save the name
+ pBundle->pNameFormal = Extra_UtilStrsav( pWord );
+
+ // open the paranthesis
+ if ( Ver_StreamPopChar(p) != '(' )
+ {
+ sprintf( pMan->sError, "Cannot formal parameter %s of gate %s (expected opening paranthesis).", pWord, Abc_ObjName(pNode));
+ Ver_ParsePrintErrorMessage( pMan );
+ return 0;
+ }
+ Ver_ParseSkipComments( pMan );
}
- // parse the actual name
- pWord = Ver_ParseGetName( pMan );
- if ( pWord == NULL )
- return 0;
- // consider the case of empty name
- fCompl = 0;
- if ( pWord[0] == 0 )
+ // check if this is the beginning of {} expression
+ Symbol = Ver_StreamScanChar(p);
+
+ // consider the case of vector-inputs
+ if ( Symbol == '{' )
{
- // remove the formal net
-// Vec_PtrPop( vNetPairs );
- pNetActual = Abc_NtkCreateObj( pNtk, ABC_OBJ_NET );
+ int i, k, Bit, Limit, nMsb, nLsb, fQuit;
+
+ // skip this char
+ Ver_ParseSkipComments( pMan );
+ Ver_StreamPopChar(p);
+
+ // read actual names
+ i = 0;
+ fQuit = 0;
+ while ( 1 )
+ {
+ // parse the formal name
+ Ver_ParseSkipComments( pMan );
+ pWord = Ver_ParseGetName( pMan );
+ if ( pWord == NULL )
+ return 0;
+
+ // check if the last char is a closing brace
+ if ( pWord[strlen(pWord)-1] == '}' )
+ {
+ pWord[strlen(pWord)-1] = 0;
+ fQuit = 1;
+ }
+ if ( pWord[0] == 0 )
+ break;
+
+ // check for constant
+ if ( pWord[0] >= '1' && pWord[0] <= '9' )
+ {
+ if ( !Ver_ParseConstant( pMan, pWord ) )
+ return 0;
+ // add constant MSB to LSB
+ for ( k = 0; k < Vec_PtrSize(pMan->vNames); k++, i++ )
+ {
+ // get the actual net
+ sprintf( Buffer, "1\'b%d", (int)(Vec_PtrEntry(pMan->vNames,k) != NULL) );
+ pNetActual = Ver_ParseFindNet( pNtk, Buffer );
+ if ( pNetActual == NULL )
+ {
+ sprintf( pMan->sError, "Actual net \"%s\" is missing in gate \"%s\".", Buffer, Abc_ObjName(pNode) );
+ Ver_ParsePrintErrorMessage( pMan );
+ return 0;
+ }
+ Vec_PtrPush( pBundle->vNetsActual, pNetActual );
+ }
+ }
+ else
+ {
+ // get the suffix of the form [m:n]
+ if ( pWord[strlen(pWord)-1] == ']' && !pMan->fNameLast )
+ Ver_ParseSignalSuffix( pMan, pWord, &nMsb, &nLsb );
+ else
+ Ver_ParseLookupSuffix( pMan, pWord, &nMsb, &nLsb );
+
+ // generate signals
+ if ( nMsb == -1 && nLsb == -1 )
+ {
+ // get the actual net
+ pNetActual = Ver_ParseFindNet( pNtk, pWord );
+ if ( pNetActual == NULL )
+ {
+ sprintf( pMan->sError, "Actual net \"%s\" is missing in gate \"%s\".", pWord, Abc_ObjName(pNode) );
+ Ver_ParsePrintErrorMessage( pMan );
+ return 0;
+ }
+ Vec_PtrPush( pBundle->vNetsActual, pNetActual );
+ i++;
+ }
+ else
+ {
+ // go from MSB to LSB
+ assert( nMsb >= 0 && nLsb >= 0 );
+ Limit = (nMsb > nLsb) ? nMsb - nLsb + 1: nLsb - nMsb + 1;
+ for ( Bit = nMsb, k = Limit - 1; k >= 0; Bit = (nMsb > nLsb ? Bit - 1: Bit + 1), k--, i++ )
+ {
+ // get the actual net
+ sprintf( Buffer, "%s[%d]", pWord, Bit );
+ pNetActual = Ver_ParseFindNet( pNtk, Buffer );
+ if ( pNetActual == NULL )
+ {
+ sprintf( pMan->sError, "Actual net \"%s\" is missing in gate \"%s\".", Buffer, Abc_ObjName(pNode) );
+ Ver_ParsePrintErrorMessage( pMan );
+ return 0;
+ }
+ Vec_PtrPush( pBundle->vNetsActual, pNetActual );
+ }
+ }
+ }
+
+ if ( fQuit )
+ break;
+
+ // skip comma
+ Ver_ParseSkipComments( pMan );
+ Symbol = Ver_StreamPopChar(p);
+ if ( Symbol == '}' )
+ break;
+ if ( Symbol != ',' )
+ {
+ sprintf( pMan->sError, "Cannot parse formal parameter %s of gate %s (expected comma).", pWord, Abc_ObjName(pNode) );
+ Ver_ParsePrintErrorMessage( pMan );
+ return 0;
+ }
+ }
}
else
{
+ // get the next word
+ pWord = Ver_ParseGetName( pMan );
+ if ( pWord == NULL )
+ return 0;
+ // consider the case of empty name
+ fCompl = 0;
+ if ( pWord[0] == 0 )
+ {
+ pNetActual = Abc_NtkCreateNet( pNtk );
+ }
+ else
+ {
/*
// check if the name is complemented
fCompl = (pWord[0] == '~');
@@ -1307,34 +1729,39 @@ int Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox )
pNtk->pData = Extra_MmFlexStart();
}
*/
- // get the actual net
- pNetActual = Ver_ParseFindNet( pNtk, pWord );
- if ( pNetActual == NULL )
- {
- sprintf( pMan->sError, "Actual net is missing in gate %s.", Abc_ObjName(pNode) );
- Ver_ParsePrintErrorMessage( pMan );
- return 0;
+ // get the actual net
+ pNetActual = Ver_ParseFindNet( pNtk, pWord );
+ if ( pNetActual == NULL )
+ {
+ sprintf( pMan->sError, "Actual net \"%s\" is missing in gate \"%s\".", pWord, Abc_ObjName(pNode) );
+ Ver_ParsePrintErrorMessage( pMan );
+ return 0;
+ }
}
+ Vec_PtrPush( pBundle->vNetsActual, Abc_ObjNotCond( pNetActual, fCompl ) );
}
- Vec_PtrPush( vNetPairs, Abc_ObjNotCond( pNetActual, fCompl ) );
- // close the paranthesis
- if ( Ver_StreamPopChar(p) != ')' )
+ if ( fFormalIsGiven )
{
- sprintf( pMan->sError, "Cannot formal parameter %s of gate %s (expected closing paranthesis).", pWord, Abc_ObjName(pNode) );
- Ver_ParsePrintErrorMessage( pMan );
- return 0;
+ // close the paranthesis
+ Ver_ParseSkipComments( pMan );
+ if ( Ver_StreamPopChar(p) != ')' )
+ {
+ sprintf( pMan->sError, "Cannot parse formal parameter %s of gate %s (expected closing paranthesis).", pWord, Abc_ObjName(pNode) );
+ Ver_ParsePrintErrorMessage( pMan );
+ return 0;
+ }
+ Ver_ParseSkipComments( pMan );
}
// check if it is the end of gate
- Ver_ParseSkipComments( pMan );
Symbol = Ver_StreamPopChar(p);
if ( Symbol == ')' )
break;
// skip comma
if ( Symbol != ',' )
{
- sprintf( pMan->sError, "Cannot formal parameter %s of gate %s (expected closing paranthesis).", pWord, Abc_ObjName(pNode) );
+ sprintf( pMan->sError, "Cannot parse formal parameter %s of gate %s (expected comma).", pWord, Abc_ObjName(pNode) );
Ver_ParsePrintErrorMessage( pMan );
return 0;
}
@@ -1364,258 +1791,713 @@ int Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox )
SeeAlso []
***********************************************************************/
+void Ver_ParseFreeBundle( Ver_Bundle_t * pBundle )
+{
+ FREE( pBundle->pNameFormal );
+ Vec_PtrFree( pBundle->vNetsActual );
+ free( pBundle );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Connects one box to the network]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Ver_ParseConnectBox( Ver_Man_t * pMan, Abc_Obj_t * pBox )
{
- Vec_Ptr_t * vNetPairs = (Vec_Ptr_t *)pBox->pCopy;
+ Vec_Ptr_t * vBundles = (Vec_Ptr_t *)pBox->pCopy;
Abc_Ntk_t * pNtk = pBox->pNtk;
Abc_Ntk_t * pNtkBox = pBox->pData;
- Abc_Obj_t * pNet, * pTerm, * pTermNew;
- int i;
+ Abc_Obj_t * pTerm, * pTermNew, * pNetAct;
+ Ver_Bundle_t * pBundle;
+ char * pNameFormal;
+ int i, k, j, iBundle, Length;
assert( !Ver_ObjIsConnected(pBox) );
assert( Ver_NtkIsDefined(pNtkBox) );
assert( !Abc_NtkHasBlackbox(pNtkBox) || Abc_NtkBoxNum(pNtkBox) == 1 );
-
+/*
// clean the PI/PO nets
Abc_NtkForEachPi( pNtkBox, pTerm, i )
Abc_ObjFanout0(pTerm)->pCopy = NULL;
Abc_NtkForEachPo( pNtkBox, pTerm, i )
Abc_ObjFanin0(pTerm)->pCopy = NULL;
-
- // map formal nets into actual nets
- Vec_PtrForEachEntry( vNetPairs, pNet, i )
+*/
+ // check if some of them do not have formal names
+ Vec_PtrForEachEntry( vBundles, pBundle, k )
+ if ( pBundle->pNameFormal == NULL )
+ break;
+ if ( k < Vec_PtrSize(vBundles) )
{
- // get the actual net corresponding to this formal net (pNet)
- pNet->pCopy = Vec_PtrEntry( vNetPairs, ++i );
- // make sure the actual net is not complemented (otherwise need to use polarity)
- assert( !Abc_ObjIsComplement(pNet->pCopy) );
+ printf( "Warning: The instance %s of network %s will be connected without using formal names.\n", pNtkBox->pName, Abc_ObjName(pBox) );
+ // add all actual nets in the bundles
+ iBundle = 0;
+ Vec_PtrForEachEntry( vBundles, pBundle, j )
+ iBundle += Vec_PtrSize(pBundle->vNetsActual);
+
+ // check the number of actual nets is the same as the number of formal nets
+ if ( iBundle != Abc_NtkPiNum(pNtkBox) + Abc_NtkPoNum(pNtkBox) )
+ {
+ sprintf( pMan->sError, "The number of actual IOs (%d) is different from the number of formal IOs (%d) when instantiating network %s in box %s.",
+ Vec_PtrSize(vBundles), Abc_NtkPiNum(pNtkBox) + Abc_NtkPoNum(pNtkBox), pNtkBox->pName, Abc_ObjName(pBox) );
+ Ver_ParsePrintErrorMessage( pMan );
+ return 0;
+ }
+ // connect bundles in the natural order
+ iBundle = 0;
+ Abc_NtkForEachPi( pNtkBox, pTerm, i )
+ {
+ pBundle = Vec_PtrEntry( vBundles, iBundle++ );
+ // the bundle is found - add the connections - using order LSB to MSB
+ Vec_PtrForEachEntryReverse( pBundle->vNetsActual, pNetAct, k )
+ {
+ pTermNew = Abc_NtkCreateBi( pNtk );
+ Abc_ObjAddFanin( pBox, pTermNew );
+ Abc_ObjAddFanin( pTermNew, pNetAct );
+ i++;
+ }
+ i--;
+ }
+ // create fanins of the box
+ Abc_NtkForEachPo( pNtkBox, pTerm, i )
+ {
+ pBundle = Vec_PtrEntry( vBundles, iBundle++ );
+ // the bundle is found - add the connections - using order LSB to MSB
+ Vec_PtrForEachEntryReverse( pBundle->vNetsActual, pNetAct, k )
+ {
+ pTermNew = Abc_NtkCreateBo( pNtk );
+ Abc_ObjAddFanin( pTermNew, pBox );
+ Abc_ObjAddFanin( pNetAct, pTermNew );
+ i++;
+ }
+ i--;
+ }
+
+ // free the bundling
+ Vec_PtrForEachEntry( vBundles, pBundle, k )
+ Ver_ParseFreeBundle( pBundle );
+ Vec_PtrFree( vBundles );
+ pBox->pCopy = NULL;
+ return 1;
}
- // make sure all PI nets are assigned
+ // bundles arrive in any order - but inside each bundle the order is MSB to LSB
+ // make sure every formal PI has a corresponding net
Abc_NtkForEachPi( pNtkBox, pTerm, i )
{
- if ( Abc_ObjFanout0(pTerm)->pCopy == NULL )
+ // get the name of this formal net
+ pNameFormal = Abc_ObjName( Abc_ObjFanout0(pTerm) );
+ // try to find the bundle with this formal net
+ pBundle = NULL;
+ Vec_PtrForEachEntry( vBundles, pBundle, k )
+ if ( !strcmp(pBundle->pNameFormal, pNameFormal) )
+ break;
+ assert( pBundle != NULL );
+ // if the bundle is not found, try without parantheses
+ if ( k == Vec_PtrSize(vBundles) )
{
- sprintf( pMan->sError, "Input formal net %s of network %s is not driven in box %s.",
- Abc_ObjName(Abc_ObjFanout0(pTerm)), pNtkBox->pName, Abc_ObjName(pBox) );
- Ver_ParsePrintErrorMessage( pMan );
- return 0;
+ pBundle = NULL;
+ Length = strlen(pNameFormal);
+ if ( pNameFormal[Length-1] == ']' )
+ {
+ // find the opening brace
+ for ( Length--; Length >= 0; Length-- )
+ if ( pNameFormal[Length] == '[' )
+ break;
+ // compare names before brace
+ if ( Length > 0 )
+ {
+ Vec_PtrForEachEntry( vBundles, pBundle, j )
+ if ( !strncmp(pBundle->pNameFormal, pNameFormal, Length) )
+ break;
+ if ( j == Vec_PtrSize(vBundles) )
+ pBundle = NULL;
+ }
+ }
+ if ( pBundle == NULL )
+ {
+ sprintf( pMan->sError, "Cannot find an actual net for the formal net %s when instantiating network %s in box %s.",
+ pNameFormal, pNtkBox->pName, Abc_ObjName(pBox) );
+ Ver_ParsePrintErrorMessage( pMan );
+ return 0;
+ }
+ }
+ // the bundle is found - add the connections - using order LSB to MSB
+ Vec_PtrForEachEntryReverse( pBundle->vNetsActual, pNetAct, k )
+ {
+ pTermNew = Abc_NtkCreateBi( pNtk );
+ Abc_ObjAddFanin( pBox, pTermNew );
+ Abc_ObjAddFanin( pTermNew, pNetAct );
+ i++;
}
- pTermNew = Abc_NtkCreateBi( pNtk );
- Abc_ObjAddFanin( pBox, pTermNew );
- Abc_ObjAddFanin( pTermNew, Abc_ObjFanout0(pTerm)->pCopy );
+ i--;
}
- // create fanins of the box
+ // connect those formal POs that do have nets
Abc_NtkForEachPo( pNtkBox, pTerm, i )
{
- if ( Abc_ObjFanin0(pTerm)->pCopy == NULL )
- Abc_ObjFanin0(pTerm)->pCopy = Abc_NtkCreateObj( pNtk, ABC_OBJ_NET );
- pTermNew = Abc_NtkCreateBo( pNtk );
- Abc_ObjAddFanin( Abc_ObjFanin0(pTerm)->pCopy, pTermNew );
- Abc_ObjAddFanin( pTermNew, pBox );
+ // get the name of this PI
+ pNameFormal = Abc_ObjName( Abc_ObjFanin0(pTerm) );
+ // try to find this formal net in the bundle
+ pBundle = NULL;
+ Vec_PtrForEachEntry( vBundles, pBundle, k )
+ if ( !strcmp(pBundle->pNameFormal, pNameFormal) )
+ break;
+ assert( pBundle != NULL );
+ // if the name is not found, try without parantheses
+ if ( k == Vec_PtrSize(vBundles) )
+ {
+ pBundle = NULL;
+ Length = strlen(pNameFormal);
+ if ( pNameFormal[Length-1] == ']' )
+ {
+ // find the opening brace
+ for ( Length--; Length >= 0; Length-- )
+ if ( pNameFormal[Length] == '[' )
+ break;
+ // compare names before brace
+ if ( Length > 0 )
+ {
+ Vec_PtrForEachEntry( vBundles, pBundle, j )
+ if ( !strncmp(pBundle->pNameFormal, pNameFormal, Length) )
+ break;
+ if ( j == Vec_PtrSize(vBundles) )
+ pBundle = NULL;
+ }
+ }
+ if ( pBundle == NULL )
+ {
+ printf( "Warning: The formal output %s is not driven when instantiating network %s in box %s.",
+ pNameFormal, pNtkBox->pName, Abc_ObjName(pBox) );
+ continue;
+ }
+ }
+ // the bundle is found - add the connections
+ Vec_PtrForEachEntryReverse( pBundle->vNetsActual, pNetAct, k )
+ {
+ if ( !strcmp(Abc_ObjName(pNetAct), "1\'b0") || !strcmp(Abc_ObjName(pNetAct), "1\'b1") )
+ {
+ sprintf( pMan->sError, "It looks like formal output %s is driving a constant net (%s) when instantiating network %s in box %s.",
+ pBundle->pNameFormal, Abc_ObjName(pNetAct), pNtkBox->pName, Abc_ObjName(pBox) );
+ Ver_ParsePrintErrorMessage( pMan );
+ return 0;
+ }
+ pTermNew = Abc_NtkCreateBo( pNtk );
+ Abc_ObjAddFanin( pTermNew, pBox );
+ Abc_ObjAddFanin( pNetAct, pTermNew );
+ i++;
+ }
+ i--;
}
- // free the mapping
- Vec_PtrFree( vNetPairs );
+ // free the bundling
+ Vec_PtrForEachEntry( vBundles, pBundle, k )
+ Ver_ParseFreeBundle( pBundle );
+ Vec_PtrFree( vBundles );
pBox->pCopy = NULL;
return 1;
}
+
/**Function*************************************************************
- Synopsis [Attaches the boxes to the network.]
+ Synopsis [Connects the defined boxes.]
- Description [Makes sure that the undefined boxes are connected correctly.]
+ Description [Returns 2 if there are any undef boxes.]
SideEffects []
SeeAlso []
***********************************************************************/
-int Vec_ParseAttachBoxes( Ver_Man_t * pMan )
+int Ver_ParseConnectDefBoxes( Ver_Man_t * pMan )
{
- Abc_Ntk_t * pNtk, * pNtkBox;
- Vec_Ptr_t * vEnvoys, * vNetPairs, * vPivots;
- Abc_Obj_t * pBox, * pTerm, * pNet, * pNetDr, * pNetAct;
- int i, k, m, nBoxes;
-
- // connect defined boxes
+ Abc_Ntk_t * pNtk;
+ Abc_Obj_t * pBox;
+ int i, k, RetValue = 1;
+ // go through all the modules
Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i )
{
- Abc_NtkForEachBlackbox( pNtk, pBox, k )
+ // go through all the boxes of this module
+ Abc_NtkForEachBox( pNtk, pBox, k )
{
- if ( pBox->pData && Ver_NtkIsDefined(pBox->pData) )
- if ( !Ver_ParseConnectBox( pMan, pBox ) )
- return 0;
+ if ( Abc_ObjIsLatch(pBox) )
+ continue;
+ // skip internal boxes of the blackboxes
+ if ( pBox->pData == NULL )
+ continue;
+ // if the network is undefined, it will be connected later
+ if ( !Ver_NtkIsDefined(pBox->pData) )
+ {
+ RetValue = 2;
+ continue;
+ }
+ // connect the box
+ if ( !Ver_ParseConnectBox( pMan, pBox ) )
+ return 0;
+ // if the network is a true blackbox, skip
+ if ( Abc_NtkHasBlackbox(pBox->pData) )
+ continue;
+ // convert the box to the whitebox
+ Abc_ObjBlackboxToWhitebox( pBox );
}
}
+ return RetValue;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Collects the undef boxes and maps them into their instances.]
- // convert blackboxes to whiteboxes
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Ptr_t * Ver_ParseCollectUndefBoxes( Ver_Man_t * pMan )
+{
+ Vec_Ptr_t * vUndefs;
+ Abc_Ntk_t * pNtk, * pNtkBox;
+ Abc_Obj_t * pBox;
+ int i, k;
+ // clear the module structures
Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i )
+ pNtk->pData = NULL;
+ // go through all the blackboxes
+ vUndefs = Vec_PtrAlloc( 16 );
+ Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i )
+ {
Abc_NtkForEachBlackbox( pNtk, pBox, k )
{
pNtkBox = pBox->pData;
if ( pNtkBox == NULL )
continue;
-
- if ( !strcmp( pNtkBox->pName, "ADDHX1" ) )
+ if ( Ver_NtkIsDefined(pNtkBox) )
+ continue;
+ if ( pNtkBox->pData == NULL )
{
- int x = 0;
+ // save the box
+ Vec_PtrPush( vUndefs, pNtkBox );
+ pNtkBox->pData = Vec_PtrAlloc( 16 );
}
+ // save the instance
+ Vec_PtrPush( pNtkBox->pData, pBox );
+ }
+ }
+ return vUndefs;
+}
- if ( pBox->pData && !Abc_NtkHasBlackbox(pBox->pData) )
- Abc_ObjBlackboxToWhitebox( pBox );
- }
+/**Function*************************************************************
+ Synopsis [Reports how many times each type of undefined box occurs.]
- // search for undefined boxes
- nBoxes = 0;
- Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i )
- nBoxes += !Ver_NtkIsDefined(pNtk);
- // quit if no undefined boxes are found
- if ( nBoxes == 0 )
- return 1;
+ Description []
+
+ SideEffects []
- // count how many times each box occurs
+ SeeAlso []
+
+***********************************************************************/
+void Ver_ParseReportUndefBoxes( Ver_Man_t * pMan )
+{
+ Abc_Ntk_t * pNtk;
+ Abc_Obj_t * pBox;
+ int i, k, nBoxes;
+ // clean
+ nBoxes = 0;
Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i )
{
- assert( pNtk->pData == NULL );
- pNtk->pData = NULL;
+ pNtk->fHiePath = 0;
+ if ( !Ver_NtkIsDefined(pNtk) )
+ nBoxes++;
}
+ // count
Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i )
Abc_NtkForEachBlackbox( pNtk, pBox, k )
- {
- if ( pBox->pData == NULL )
- continue;
- pNtkBox = pBox->pData;
- pNtkBox->pData = (void *)((int)pNtkBox->pData + 1);
- }
-
- // print the boxes
+ if ( pBox->pData && !Ver_NtkIsDefined(pBox->pData) )
+ ((Abc_Ntk_t *)pBox->pData)->fHiePath++;
+ // print the stats
printf( "Warning: The design contains %d undefined objects interpreted as blackboxes:\n", nBoxes );
Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i )
if ( !Ver_NtkIsDefined(pNtk) )
- printf( "%s (%d) ", Abc_NtkName(pNtk), (int)pNtk->pData );
+ printf( "%s (%d) ", Abc_NtkName(pNtk), pNtk->fHiePath );
printf( "\n" );
-
- // clean the boxes
+ // clean
Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i )
- pNtk->pData = NULL;
+ pNtk->fHiePath = 0;
+}
+/**Function*************************************************************
- // map actual nets into formal nets belonging to the undef boxes
- vPivots = Vec_PtrAlloc( 100 );
- Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i )
- {
- Abc_NtkForEachBlackbox( pNtk, pBox, k )
- {
- if ( pBox->pData == NULL || Ver_NtkIsDefined(pBox->pData) )
- continue;
- vNetPairs = (Vec_Ptr_t *)pBox->pCopy;
- Vec_PtrForEachEntry( vNetPairs, pNet, m )
- {
- pNetAct = Vec_PtrEntry( vNetPairs, ++m );
- // skip already driven nets and constants
- if ( Abc_ObjFaninNum(pNetAct) == 1 )
- continue;
- if ( !(strcmp(Abc_ObjName(pNetAct), "1\'b0") && strcmp(Abc_ObjName(pNetAct), "1\'b1")) ) // constant
- continue;
- // add this net
- if ( pNetAct->pData == NULL )
+ Synopsis [Returns 1 if there are non-driven nets.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ver_ParseCheckNondrivenNets( Vec_Ptr_t * vUndefs )
+{
+ Abc_Ntk_t * pNtk;
+ Ver_Bundle_t * pBundle;
+ Abc_Obj_t * pBox, * pNet;
+ int i, k, j, m;
+ // go through undef box types
+ Vec_PtrForEachEntry( vUndefs, pNtk, i )
+ // go through instances of this type
+ Vec_PtrForEachEntry( pNtk->pData, pBox, k )
+ // go through the bundles of this instance
+ Vec_PtrForEachEntryReverse( (Vec_Ptr_t *)pBox->pCopy, pBundle, j )
+ // go through the actual nets of this bundle
+ if ( pBundle )
+ Vec_PtrForEachEntry( pBundle->vNetsActual, pNet, m )
{
- pNetAct->pData = Vec_PtrAlloc( 16 );
- Vec_PtrPush( vPivots, pNetAct );
+ char * pName = Abc_ObjName(pNet);
+ if ( Abc_ObjFaninNum(pNet) == 0 ) // non-driven
+ if ( strcmp(Abc_ObjName(pNet), "1\'b0") && strcmp(Abc_ObjName(pNet), "1\'b1") ) // diff from a const
+ return 1;
}
- vEnvoys = pNetAct->pData;
- Vec_PtrPush( vEnvoys, pNet );
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Checks if formal nets with the given name are driven in any of the instances of undef boxes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ver_ParseFormalNetsAreDriven( Abc_Ntk_t * pNtk, char * pNameFormal )
+{
+ Ver_Bundle_t * pBundle;
+ Abc_Obj_t * pBox, * pNet;
+ int k, j, m;
+ // go through instances of this type
+ Vec_PtrForEachEntry( pNtk->pData, pBox, k )
+ {
+ // find a bundle with the given name in this instance
+ Vec_PtrForEachEntryReverse( (Vec_Ptr_t *)pBox->pCopy, pBundle, j )
+ if ( pBundle && !strcmp( pBundle->pNameFormal, pNameFormal ) )
+ break;
+ // skip non-driven bundles
+ if ( j == Vec_PtrSize((Vec_Ptr_t *)pBox->pCopy) )
+ continue;
+ // check if all nets are driven in this bundle
+ Vec_PtrForEachEntry( pBundle->vNetsActual, pNet, m )
+ if ( Abc_ObjFaninNum(pNet) > 0 )
+ return 1;
+ }
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns the non-driven bundle that is given distance from the end.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Ver_Bundle_t * Ver_ParseGetNondrivenBundle( Abc_Ntk_t * pNtk, int Counter )
+{
+ Ver_Bundle_t * pBundle;
+ Abc_Obj_t * pBox, * pNet;
+ int k, m;
+ // go through instances of this type
+ Vec_PtrForEachEntry( pNtk->pData, pBox, k )
+ {
+ if ( Counter >= Vec_PtrSize((Vec_Ptr_t *)pBox->pCopy) )
+ continue;
+ // get the bundle given distance away
+ pBundle = Vec_PtrEntry( (Vec_Ptr_t *)pBox->pCopy, Vec_PtrSize((Vec_Ptr_t *)pBox->pCopy) - 1 - Counter );
+ if ( pBundle == NULL )
+ continue;
+ // go through the actual nets of this bundle
+ Vec_PtrForEachEntry( pBundle->vNetsActual, pNet, m )
+ if ( !Abc_ObjFaninNum(pNet) && !Ver_ParseFormalNetsAreDriven(pNtk, pBundle->pNameFormal) ) // non-driven
+ return pBundle;
+ }
+ return NULL;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Drives the bundle in the given undef box.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ver_ParseDriveFormal( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Ver_Bundle_t * pBundle0 )
+{
+ char Buffer[200];
+ char * pName;
+ Ver_Bundle_t * pBundle;
+ Abc_Obj_t * pBox, * pTerm, * pTermNew, * pNetAct, * pNetFormal;
+ int k, j, m;
+
+ // drive this net in the undef box
+ Vec_PtrForEachEntry( pBundle0->vNetsActual, pNetAct, m )
+ {
+ // create the formal net
+ if ( Vec_PtrSize(pBundle0->vNetsActual) == 1 )
+ sprintf( Buffer, "%s", pBundle0->pNameFormal );
+ else
+ sprintf( Buffer, "%s[%d]", pBundle0->pNameFormal, m );
+ assert( Abc_NtkFindNet( pNtk, Buffer ) == NULL );
+ pNetFormal = Abc_NtkFindOrCreateNet( pNtk, Buffer );
+ // connect it to the box
+ pTerm = Abc_NtkCreateBo( pNtk );
+ assert( Abc_NtkBoxNum(pNtk) <= 1 );
+ pBox = Abc_NtkBoxNum(pNtk)? Abc_NtkBox(pNtk,0) : Abc_NtkCreateBlackbox(pNtk);
+ Abc_ObjAddFanin( Abc_NtkCreatePo(pNtk), pNetFormal );
+ Abc_ObjAddFanin( pNetFormal, pTerm );
+ Abc_ObjAddFanin( pTerm, pBox );
+ }
+
+ // go through instances of this type
+ pName = Extra_UtilStrsav(pBundle0->pNameFormal);
+ Vec_PtrForEachEntry( pNtk->pData, pBox, k )
+ {
+ // find a bundle with the given name in this instance
+ Vec_PtrForEachEntryReverse( (Vec_Ptr_t *)pBox->pCopy, pBundle, j )
+ if ( pBundle && !strcmp( pBundle->pNameFormal, pName ) )
+ break;
+ // skip non-driven bundles
+ if ( j == Vec_PtrSize((Vec_Ptr_t *)pBox->pCopy) )
+ continue;
+ // check if any nets are driven in this bundle
+ Vec_PtrForEachEntry( pBundle->vNetsActual, pNetAct, m )
+ if ( Abc_ObjFaninNum(pNetAct) > 0 )
+ {
+ sprintf( pMan->sError, "Internal error while trying to connect undefined boxes. It is likely that the algorithm currently used has its limitations." );
+ Ver_ParsePrintErrorMessage( pMan );
+ return 0;
}
+ // drive the nets by the undef box
+ Vec_PtrForEachEntryReverse( pBundle->vNetsActual, pNetAct, m )
+ {
+ pTermNew = Abc_NtkCreateBo( pNetAct->pNtk );
+ Abc_ObjAddFanin( pTermNew, pBox );
+ Abc_ObjAddFanin( pNetAct, pTermNew );
}
+ // remove the bundle
+ Ver_ParseFreeBundle( pBundle );
+ Vec_PtrWriteEntry( (Vec_Ptr_t *)pBox->pCopy, j, NULL );
}
+ free( pName );
+ return 1;
+}
+
- // for each pivot net, find the driver
- Vec_PtrForEachEntry( vPivots, pNetAct, i )
+/**Function*************************************************************
+
+ Synopsis [Drives the bundle in the given undef box.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ver_ParseDriveInputs( Ver_Man_t * pMan, Vec_Ptr_t * vUndefs )
+{
+ char Buffer[200];
+ Ver_Bundle_t * pBundle;
+ Abc_Ntk_t * pNtk;
+ Abc_Obj_t * pBox, * pBox2, * pTerm, * pTermNew, * pNetFormal, * pNetAct;
+ int i, k, j, m, CountCur, CountTotal = -1;
+ // iterate through the undef boxes
+ Vec_PtrForEachEntry( vUndefs, pNtk, i )
{
- char * pName = Abc_ObjName(pNetAct);
-/*
- if ( !strcmp( Abc_ObjName(pNetAct), "dma_fifo_ff_cnt[2]" ) )
+ // count the number of unconnected bundles for instances of this type of box
+ CountTotal = -1;
+ Vec_PtrForEachEntry( pNtk->pData, pBox, k )
{
- int x = 0;
+ CountCur = 0;
+ Vec_PtrForEachEntry( (Vec_Ptr_t *)pBox->pCopy, pBundle, j )
+ CountCur += (pBundle != NULL);
+ if ( CountTotal == -1 )
+ CountTotal = CountCur;
+ else if ( CountTotal != CountCur )
+ {
+ sprintf( pMan->sError, "The number of formal inputs (%d) is different from the expected one (%d) when instantiating network %s in box %s.",
+ CountCur, CountTotal, pNtk->pName, Abc_ObjName(pBox) );
+ Ver_ParsePrintErrorMessage( pMan );
+ return 0;
+ }
}
-*/
- assert( Abc_ObjFaninNum(pNetAct) == 0 );
- assert( strcmp(Abc_ObjName(pNetAct), "1\'b0") && strcmp(Abc_ObjName(pNetAct), "1\'b1") );
- vEnvoys = pNetAct->pData; pNetAct->pData = NULL;
- // find the driver starting from the last nets
- pNetDr = NULL;
- for ( m = 0; m < 64; m++ )
+
+ // create formals
+ pBox = Vec_PtrEntry( pNtk->pData, 0 );
+ Vec_PtrForEachEntry( (Vec_Ptr_t *)pBox->pCopy, pBundle, j )
{
- Vec_PtrForEachEntry( vEnvoys, pNet, k )
+ if ( pBundle == NULL )
+ continue;
+ Vec_PtrForEachEntry( pBundle->vNetsActual, pNetAct, m )
+ {
+ // find create the formal net
+ if ( Vec_PtrSize(pBundle->vNetsActual) == 1 )
+ sprintf( Buffer, "%s", pBundle->pNameFormal );
+ else
+ sprintf( Buffer, "%s[%d]", pBundle->pNameFormal, m );
+ assert( Abc_NtkFindNet( pNtk, Buffer ) == NULL );
+ pNetFormal = Abc_NtkFindOrCreateNet( pNtk, Buffer );
+ // connect
+ pTerm = Abc_NtkCreateBi( pNtk );
+ assert( Abc_NtkBoxNum(pNtk) <= 1 );
+ pBox2 = Abc_NtkBoxNum(pNtk)? Abc_NtkBox(pNtk,0) : Abc_NtkCreateBlackbox(pNtk);
+ Abc_ObjAddFanin( pNetFormal, Abc_NtkCreatePi(pNtk) );
+ Abc_ObjAddFanin( pTerm, pNetFormal );
+ Abc_ObjAddFanin( pBox2, pTerm );
+ }
+ }
+
+ // go through all the boxes
+ Vec_PtrForEachEntry( pNtk->pData, pBox, k )
+ {
+ // go through all the bundles
+ Vec_PtrForEachEntry( (Vec_Ptr_t *)pBox->pCopy, pBundle, j )
{
- if ( Abc_ObjId(pNet) == 0 )
+ if ( pBundle == NULL )
continue;
- if ( (int)Abc_ObjId(pNet) == Abc_NtkObjNumMax(pNet->pNtk) - 1 - m )
+ // drive the nets by the undef box
+ Vec_PtrForEachEntryReverse( pBundle->vNetsActual, pNetAct, m )
{
- pNetDr = pNet;
- break;
+ pTermNew = Abc_NtkCreateBi( pNetAct->pNtk );
+ Abc_ObjAddFanin( pBox, pTermNew );
+ Abc_ObjAddFanin( pTermNew, pNetAct );
}
+ // remove the bundle
+ Ver_ParseFreeBundle( pBundle );
+ Vec_PtrWriteEntry( (Vec_Ptr_t *)pBox->pCopy, j, NULL );
}
- if ( pNetDr )
- break;
+
+ // free the bundles
+ Vec_PtrFree( (Vec_Ptr_t *)pBox->pCopy );
+ pBox->pCopy = NULL;
}
- assert( pNetDr != NULL );
- Vec_PtrWriteEntry( vPivots, i, pNetDr );
- Vec_PtrFree( vEnvoys );
}
+ return 1;
+}
- // for each pivot net, create driver
- Vec_PtrForEachEntry( vPivots, pNetDr, i )
- {
- if ( pNetDr == NULL )
- continue;
- assert( Abc_ObjFaninNum(pNetDr) <= 1 );
- if ( Abc_ObjFaninNum(pNetDr) == 1 )
- continue;
- // drive this net with the box
- pTerm = Abc_NtkCreateBo( pNetDr->pNtk );
- assert( Abc_NtkBoxNum(pNetDr->pNtk) <= 1 );
- pBox = Abc_NtkBoxNum(pNetDr->pNtk)? Abc_NtkBox(pNetDr->pNtk,0) : Abc_NtkCreateBlackbox(pNetDr->pNtk);
- Abc_ObjAddFanin( Abc_NtkCreatePo(pNetDr->pNtk), pNetDr );
- Abc_ObjAddFanin( pNetDr, pTerm );
- Abc_ObjAddFanin( pTerm, pBox );
- }
- Vec_PtrFree( vPivots );
- // connect the remaining boxes
- Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i )
+/**Function*************************************************************
+
+ Synopsis [Returns the max size of any undef box.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ver_ParseMaxBoxSize( Vec_Ptr_t * vUndefs )
+{
+ Abc_Ntk_t * pNtk;
+ Abc_Obj_t * pBox;
+ int i, k, nMaxSize = 0;
+ // go through undef box types
+ Vec_PtrForEachEntry( vUndefs, pNtk, i )
+ // go through instances of this type
+ Vec_PtrForEachEntry( pNtk->pData, pBox, k )
+ // check the number of bundles of this instance
+ if ( nMaxSize < Vec_PtrSize((Vec_Ptr_t *)pBox->pCopy) )
+ nMaxSize = Vec_PtrSize((Vec_Ptr_t *)pBox->pCopy);
+ return nMaxSize;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Attaches the boxes to the network.]
+
+ Description [This procedure is called after the design is parsed.
+ At that point, all the defined models have their PIs present.
+ They are connected first. Next undef boxes are processed (if present).
+ Iteratively, one bundle is selected to be driven by the undef boxes in such
+ a way that there is no conflict (if it is driven by an instance of the box,
+ no other net will be driven twice by the same formal net of some other instance
+ of the same box). In the end, all the remaining nets that cannot be driven
+ by the undef boxes are connected to the undef boxes as inputs.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ver_ParseAttachBoxes( Ver_Man_t * pMan )
+{
+ Abc_Ntk_t * pNtk;
+ Ver_Bundle_t * pBundle;
+ Vec_Ptr_t * vUndefs;
+ int i, RetValue, Counter, nMaxBoxSize;
+
+ // connect defined boxes
+ RetValue = Ver_ParseConnectDefBoxes( pMan );
+ if ( RetValue < 2 )
+ return RetValue;
+
+ // report the boxes
+ Ver_ParseReportUndefBoxes( pMan );
+
+ // collect undef box types and their actual instances
+ vUndefs = Ver_ParseCollectUndefBoxes( pMan );
+ assert( Vec_PtrSize( vUndefs ) > 0 );
+
+ // go through all undef box types
+ Counter = 0;
+ nMaxBoxSize = Ver_ParseMaxBoxSize( vUndefs );
+ while ( Ver_ParseCheckNondrivenNets(vUndefs) && Counter < nMaxBoxSize )
{
- if ( Abc_NtkPiNum(pNtk) )
- continue;
- Abc_NtkForEachNet( pNtk, pNet, k )
+ // go through undef box types
+ pBundle = NULL;
+ Vec_PtrForEachEntry( vUndefs, pNtk, i )
+ if ( pBundle = Ver_ParseGetNondrivenBundle( pNtk, Counter ) )
+ break;
+ if ( pBundle == NULL )
{
- if ( Abc_ObjFaninNum(pNet) )
- continue;
- // drive this net
- pTerm = Abc_NtkCreateBi( pNet->pNtk );
- assert( Abc_NtkBoxNum(pNet->pNtk) <= 1 );
- pBox = Abc_NtkBoxNum(pNet->pNtk)? Abc_NtkBox(pNet->pNtk,0) : Abc_NtkCreateBlackbox(pNet->pNtk);
- Abc_ObjAddFanin( pBox, pTerm );
- Abc_ObjAddFanin( pTerm, pNet );
- Abc_ObjAddFanin( pNet, Abc_NtkCreatePi(pNet->pNtk) );
+ Counter++;
+ continue;
}
+ // drive this bundle by this box
+ if ( !Ver_ParseDriveFormal( pMan, pNtk, pBundle ) )
+ return 0;
}
- // connect the remaining boxes
- Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i )
+ // make all the remaining bundles the drivers of undefs
+ if ( !Ver_ParseDriveInputs( pMan, vUndefs ) )
+ return 0;
+
+ // cleanup
+ Vec_PtrForEachEntry( vUndefs, pNtk, i )
{
- Abc_NtkForEachBlackbox( pNtk, pBox, k )
- {
- char * pName = Abc_ObjName(pBox);
- if ( !Ver_ObjIsConnected(pBox) )
- if ( !Ver_ParseConnectBox( pMan, pBox ) )
- return 0;
- }
+ Vec_PtrFree( pNtk->pData );
+ pNtk->pData = NULL;
}
+ Vec_PtrFree( vUndefs );
return 1;
}
@@ -1716,55 +2598,12 @@ Abc_Obj_t * Ver_ParseCreateInv( Abc_Ntk_t * pNtk, Abc_Obj_t * pNet )
{
Abc_Obj_t * pObj;
pObj = Abc_NtkCreateNodeInv( pNtk, pNet );
- pNet = Abc_NtkCreateObj( pNtk, ABC_OBJ_NET );
+ pNet = Abc_NtkCreateNet( pNtk );
Abc_ObjAddFanin( pNet, pObj );
return pNet;
}
-
-/*
- // allocate memory to remember the phase
- pPolarity = NULL;
- if ( fComplUsed )
- {
- int nBytes = 4 * Abc_BitWordNum( Abc_NtkPiNum(pNtkBox) );
- pPolarity = (unsigned *)Extra_MmFlexEntryFetch( pNtk->pData, nBytes );
- memset( pPolarity, 0, nBytes );
- }
- // create box to represent this gate
- if ( Abc_NtkHasBlackbox(pNtkBox) )
- pNode = Abc_NtkCreateBlackbox( pNtk );
- else
- pNode = Abc_NtkCreateWhitebox( pNtk );
- pNode->pNext = (Abc_Obj_t *)pPolarity;
- pNode->pData = pNtkBox;
- // connect to fanin nets
- Abc_NtkForEachPi( pNtkBox, pObj, i )
- {
- if ( pPolarity && Abc_ObjIsComplement(pObj->pCopy) )
- {
- Abc_InfoSetBit( pPolarity, i );
- pObj->pCopy = Abc_ObjRegular( pObj->pCopy );
- }
- assert( !Abc_ObjIsComplement(pObj->pCopy) );
-// Abc_ObjAddFanin( pNode, pObj->pCopy );
- pTerm = Abc_NtkCreateBi( pNtk );
- Abc_ObjAddFanin( pTerm, pObj->pCopy );
- Abc_ObjAddFanin( pNode, pTerm );
- }
- // connect to fanout nets
- Abc_NtkForEachPo( pNtkBox, pObj, i )
- {
- if ( pObj->pCopy == NULL )
- pObj->pCopy = Abc_NtkFindOrCreateNet(pNtk, NULL);
-// Abc_ObjAddFanin( pObj->pCopy, pNode );
- pTerm = Abc_NtkCreateBo( pNtk );
- Abc_ObjAddFanin( pTerm, pNode );
- Abc_ObjAddFanin( pObj->pCopy, pTerm );
- }
-*/
-
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/base/ver/verCore.zip b/src/base/ver/verCore.zip
new file mode 100644
index 00000000..481f7e6a
--- /dev/null
+++ b/src/base/ver/verCore.zip
Binary files differ
diff --git a/src/base/ver/verFormula.c b/src/base/ver/verFormula.c
index 253754ae..19a2c523 100644
--- a/src/base/ver/verFormula.c
+++ b/src/base/ver/verFormula.c
@@ -120,7 +120,7 @@ void * Ver_FormulaParser( char * pFormula, void * pMan, Vec_Ptr_t * vNames, Vec_
case '\r':
case '\n':
continue;
-
+/*
// treat Constant 0 as a variable
case VER_PARSE_SYM_CONST0:
Vec_PtrPush( vStackFn, Hop_ManConst0(pMan) ); // Cudd_Ref( Hop_ManConst0(pMan) );
@@ -144,7 +144,7 @@ void * Ver_FormulaParser( char * pFormula, void * pMan, Vec_Ptr_t * vNames, Vec_
}
Flag = VER_PARSE_FLAG_VAR;
break;
-
+*/
case VER_PARSE_SYM_NEGBEF1:
case VER_PARSE_SYM_NEGBEF2:
if ( Flag == VER_PARSE_FLAG_VAR )
generated by cgit v1.2.3 (git 2.25.1) at 2024-08-03 21:19:44 +0000