abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
Data Structures | Typedefs | Enumerations | Functions | Variables
verCore.c File Reference
#include "ver.h"
#include "map/mio/mio.h"
#include "base/main/main.h"

Go to the source code of this file.

Data Structures

struct  Ver_Bundle_t_
 

Typedefs

typedef struct Ver_Bundle_t_ Ver_Bundle_t
 

Enumerations

enum  Ver_SignalType_t {
  VER_SIG_NONE = 0, VER_SIG_INPUT, VER_SIG_OUTPUT, VER_SIG_INOUT,
  VER_SIG_REG, VER_SIG_WIRE
}
 DECLARATIONS ///. More...
 
enum  Ver_GateType_t {
  VER_GATE_AND = 0, VER_GATE_OR, VER_GATE_XOR, VER_GATE_BUF,
  VER_GATE_NAND, VER_GATE_NOR, VER_GATE_XNOR, VER_GATE_NOT
}
 

Functions

static Ver_Man_t * Ver_ParseStart (char *pFileName, Abc_Des_t *pGateLib)
 FUNCTION DEFINITIONS ///. More...
 
static void Ver_ParseStop (Ver_Man_t *p)
 
static void Ver_ParseFreeData (Ver_Man_t *p)
 
static void Ver_ParseInternal (Ver_Man_t *p)
 
static int Ver_ParseModule (Ver_Man_t *p)
 
static int Ver_ParseSignal (Ver_Man_t *p, Abc_Ntk_t *pNtk, Ver_SignalType_t SigType)
 
static int Ver_ParseAlways (Ver_Man_t *p, Abc_Ntk_t *pNtk)
 
static int Ver_ParseInitial (Ver_Man_t *p, Abc_Ntk_t *pNtk)
 
static int Ver_ParseAssign (Ver_Man_t *p, Abc_Ntk_t *pNtk)
 
static int Ver_ParseGateStandard (Ver_Man_t *pMan, Abc_Ntk_t *pNtk, Ver_GateType_t GateType)
 
static int Ver_ParseFlopStandard (Ver_Man_t *pMan, Abc_Ntk_t *pNtk)
 
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 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 int Ver_NtkIsDefined (Abc_Ntk_t *pNtkBox)
 
static int Ver_ObjIsConnected (Abc_Obj_t *pObj)
 
Abc_Des_t * Ver_ParseFile (char *pFileName, Abc_Des_t *pGateLib, int fCheck, int fUseMemMan)
 MACRO DEFINITIONS ///. More...
 
void Ver_ParsePrintErrorMessage (Ver_Man_t *p)
 
Abc_Ntk_t * Ver_ParseFindOrCreateNetwork (Ver_Man_t *pMan, char *pName)
 
Abc_Obj_t * Ver_ParseFindNet (Abc_Ntk_t *pNtk, char *pName)
 
int Ver_ParseConvertNetwork (Ver_Man_t *pMan, Abc_Ntk_t *pNtk, int fMapped)
 
int Ver_ParseLookupSuffix (Ver_Man_t *pMan, char *pWord, int *pnMsb, int *pnLsb)
 
int Ver_ParseInsertsSuffix (Ver_Man_t *pMan, char *pWord, int nMsb, int nLsb)
 
int Ver_ParseSignalPrefix (Ver_Man_t *pMan, char **ppWord, int *pnMsb, int *pnLsb)
 
int Ver_ParseSignalSuffix (Ver_Man_t *pMan, char *pWord, int *pnMsb, int *pnLsb)
 
int Ver_ParseConstant (Ver_Man_t *pMan, char *pWord)
 
int Ver_FindGateInput (Mio_Gate_t *pGate, char *pName)
 
void Ver_ParseFreeBundle (Ver_Bundle_t *pBundle)
 
int Ver_ParseConnectDefBoxes (Ver_Man_t *pMan)
 
Vec_Ptr_t * Ver_ParseCollectUndefBoxes (Ver_Man_t *pMan)
 
void Ver_ParseReportUndefBoxes (Ver_Man_t *pMan)
 
int Ver_ParseCheckNondrivenNets (Vec_Ptr_t *vUndefs)
 
int Ver_ParseFormalNetsAreDriven (Abc_Ntk_t *pNtk, char *pNameFormal)
 
Ver_Bundle_t * Ver_ParseGetNondrivenBundle (Abc_Ntk_t *pNtk, int Counter)
 
int Ver_ParseDriveFormal (Ver_Man_t *pMan, Abc_Ntk_t *pNtk, Ver_Bundle_t *pBundle0)
 
int Ver_ParseDriveInputs (Ver_Man_t *pMan, Vec_Ptr_t *vUndefs)
 
int Ver_ParseMaxBoxSize (Vec_Ptr_t *vUndefs)
 
void Ver_ParsePrintLog (Ver_Man_t *pMan)
 

Variables

int glo_fMapped = 0
 

Typedef Documentation

typedef struct Ver_Bundle_t_ Ver_Bundle_t

Definition at line 82 of file verCore.c.

Enumeration Type Documentation

enum Ver_GateType_t
Enumerator
VER_GATE_AND 
VER_GATE_OR 
VER_GATE_XOR 
VER_GATE_BUF 
VER_GATE_NAND 
VER_GATE_NOR 
VER_GATE_XNOR 
VER_GATE_NOT 

Definition at line 43 of file verCore.c.

43  {
44  VER_GATE_AND = 0,
45  VER_GATE_OR,
46  VER_GATE_XOR,
47  VER_GATE_BUF,
48  VER_GATE_NAND,
49  VER_GATE_NOR,
50  VER_GATE_XNOR,
51  VER_GATE_NOT
52 } Ver_GateType_t;
Ver_GateType_t
Ver_GateType_t
Definition: verCore.c:43
enum Ver_SignalType_t

DECLARATIONS ///.

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

FileName [verCore.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Verilog parser.]

Synopsis [Parses several flavors of structural Verilog.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - August 19, 2006.]

Revision [

Id:
verCore.c,v 1.00 2006/08/19 00:00:00 alanmi Exp

]

Enumerator
VER_SIG_NONE 
VER_SIG_INPUT 
VER_SIG_OUTPUT 
VER_SIG_INOUT 
VER_SIG_REG 
VER_SIG_WIRE 

Definition at line 33 of file verCore.c.

33  {
34  VER_SIG_NONE = 0,
35  VER_SIG_INPUT,
36  VER_SIG_OUTPUT,
37  VER_SIG_INOUT,
38  VER_SIG_REG,
39  VER_SIG_WIRE
40 } Ver_SignalType_t;
Ver_SignalType_t
Ver_SignalType_t
DECLARATIONS ///.
Definition: verCore.c:33

Function Documentation

int Ver_FindGateInput ( Mio_Gate_t *  pGate,
char *  pName 
)

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

Synopsis [Returns the index of the given pin the gate.]

Description []

SideEffects []

SeeAlso []

Definition at line 1525 of file verCore.c.

1526 {
1527  Mio_Pin_t * pGatePin;
1528  int i;
1529  for ( i = 0, pGatePin = Mio_GateReadPins(pGate); pGatePin != NULL; pGatePin = Mio_PinReadNext(pGatePin), i++ )
1530  if ( strcmp(pName, Mio_PinReadName(pGatePin)) == 0 )
1531  return i;
1532  if ( strcmp(pName, Mio_GateReadOutName(pGate)) == 0 )
1533  return i;
1534  if ( Mio_GateReadTwin(pGate) && strcmp(pName, Mio_GateReadOutName(Mio_GateReadTwin(pGate))) == 0 )
1535  return i+1;
1536  return -1;
1537 }
Mio_GateReadPins
Mio_Pin_t * Mio_GateReadPins(Mio_Gate_t *pGate)
Definition: mioApi.c:147
Mio_GateReadOutName
char * Mio_GateReadOutName(Mio_Gate_t *pGate)
Definition: mioApi.c:144
Mio_PinReadName
char * Mio_PinReadName(Mio_Pin_t *pPin)
Definition: mioApi.c:170
Mio_PinStruct_t_
Definition: mioInt.h:103
Mio_PinReadNext
Mio_Pin_t * Mio_PinReadNext(Mio_Pin_t *pPin)
Definition: mioApi.c:179
strcmp
int strcmp()
Mio_GateReadTwin
Mio_Gate_t * Mio_GateReadTwin(Mio_Gate_t *pGate)
Definition: mioApi.c:150
static int Ver_NtkIsDefined ( Abc_Ntk_t *  pNtkBox)
inlinestatic

Definition at line 77 of file verCore.c.

77 { assert( pNtkBox->pName ); return Abc_NtkPiNum(pNtkBox) || Abc_NtkPoNum(pNtkBox); }
Abc_NtkPoNum
static int Abc_NtkPoNum(Abc_Ntk_t *pNtk)
Definition: abc.h:286
Abc_NtkPiNum
static int Abc_NtkPiNum(Abc_Ntk_t *pNtk)
Definition: abc.h:285
assert
#define assert(ex)
Definition: util_old.h:213
Abc_Ntk_t_::pName
char * pName
Definition: abc.h:158
static int Ver_ObjIsConnected ( Abc_Obj_t *  pObj)
inlinestatic

Definition at line 78 of file verCore.c.

78 { assert( Abc_ObjIsBox(pObj) ); return Abc_ObjFaninNum(pObj) || Abc_ObjFanoutNum(pObj); }
Abc_ObjFanoutNum
static int Abc_ObjFanoutNum(Abc_Obj_t *pObj)
Definition: abc.h:365
Abc_ObjFaninNum
static int Abc_ObjFaninNum(Abc_Obj_t *pObj)
Definition: abc.h:364
assert
#define assert(ex)
Definition: util_old.h:213
Abc_ObjIsBox
static int Abc_ObjIsBox(Abc_Obj_t *pObj)
Definition: abc.h:357
int Ver_ParseAlways ( Ver_Man_t *  pMan,
Abc_Ntk_t *  pNtk 
)
static

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

Synopsis [Parses one directive.]

Description []

SideEffects []

SeeAlso []

Definition at line 892 of file verCore.c.

893 {
894  Ver_Stream_t * p = pMan->pReader;
895  Abc_Obj_t * pNet, * pNet2;
896  int fStopAfterOne;
897  char * pWord, * pWord2;
898  char Symbol;
899  // parse the directive
900  pWord = Ver_ParseGetName( pMan );
901  if ( pWord == NULL )
902  return 0;
903  if ( pWord[0] == '@' )
904  {
905  Ver_StreamSkipToChars( p, ")" );
906  Ver_StreamPopChar(p);
907  // parse the directive
908  pWord = Ver_ParseGetName( pMan );
909  if ( pWord == NULL )
910  return 0;
911  }
912  // decide how many statements to parse
913  fStopAfterOne = 0;
914  if ( strcmp( pWord, "begin" ) )
915  fStopAfterOne = 1;
916  // iterate over the initial states
917  while ( 1 )
918  {
919  if ( !fStopAfterOne )
920  {
921  // get the name of the output signal
922  pWord = Ver_ParseGetName( pMan );
923  if ( pWord == NULL )
924  return 0;
925  // look for the end of directive
926  if ( !strcmp( pWord, "end" ) )
927  break;
928  }
929  // get the fanout net
930  pNet = Ver_ParseFindNet( pNtk, pWord );
931  if ( pNet == NULL )
932  {
933  sprintf( pMan->sError, "Cannot read the always statement for %s (output wire is not defined).", pWord );
934  Ver_ParsePrintErrorMessage( pMan );
935  return 0;
936  }
937  // get the equality sign
938  Symbol = Ver_StreamPopChar(p);
939  if ( Symbol != '<' && Symbol != '=' )
940  {
941  sprintf( pMan->sError, "Cannot read the assign statement for %s (expected <= or =).", pWord );
942  Ver_ParsePrintErrorMessage( pMan );
943  return 0;
944  }
945  if ( Symbol == '<' )
946  Ver_StreamPopChar(p);
947  // skip the comments
948  if ( !Ver_ParseSkipComments( pMan ) )
949  return 0;
950  // get the second name
951  pWord2 = Ver_ParseGetName( pMan );
952  if ( pWord2 == NULL )
953  return 0;
954  // check if the name is complemented
955  if ( pWord2[0] == '~' )
956  {
957  pNet2 = Ver_ParseFindNet( pNtk, pWord2+1 );
958  pNet2 = Ver_ParseCreateInv( pNtk, pNet2 );
959  }
960  else
961  pNet2 = Ver_ParseFindNet( pNtk, pWord2 );
962  if ( pNet2 == NULL )
963  {
964  sprintf( pMan->sError, "Cannot read the always statement for %s (input wire is not defined).", pWord2 );
965  Ver_ParsePrintErrorMessage( pMan );
966  return 0;
967  }
968  // create the latch
969  Ver_ParseCreateLatch( pNtk, pNet2, pNet );
970  // remove the last symbol
971  Symbol = Ver_StreamPopChar(p);
972  assert( Symbol == ';' );
973  // quit if only one directive
974  if ( fStopAfterOne )
975  break;
976  }
977  return 1;
978 }
Ver_ParseCreateInv
static Abc_Obj_t * Ver_ParseCreateInv(Abc_Ntk_t *pNtk, Abc_Obj_t *pNet)
Definition: verCore.c:3021
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Ver_StreamPopChar
char Ver_StreamPopChar(Ver_Stream_t *p)
Definition: verStream.c:275
Ver_ParseSkipComments
int Ver_ParseSkipComments(Ver_Man_t *p)
DECLARATIONS ///.
Definition: verParse.c:45
strcmp
int strcmp()
Ver_Stream_t_
Definition: verStream.c:36
Abc_Obj_t_
Definition: abc.h:128
Ver_ParseCreateLatch
static Abc_Obj_t * Ver_ParseCreateLatch(Abc_Ntk_t *pNtk, Abc_Obj_t *pNetLI, Abc_Obj_t *pNetLO)
Definition: verCore.c:2990
Ver_StreamSkipToChars
void Ver_StreamSkipToChars(Ver_Stream_t *p, char *pCharsToStop)
Definition: verStream.c:349
Ver_ParseGetName
char * Ver_ParseGetName(Ver_Man_t *p)
Definition: verParse.c:91
sprintf
char * sprintf()
Ver_ParsePrintErrorMessage
void Ver_ParsePrintErrorMessage(Ver_Man_t *p)
Definition: verCore.c:278
assert
#define assert(ex)
Definition: util_old.h:213
Ver_ParseFindNet
Abc_Obj_t * Ver_ParseFindNet(Abc_Ntk_t *pNtk, char *pName)
Definition: verCore.c:328
int Ver_ParseAssign ( Ver_Man_t *  pMan,
Abc_Ntk_t *  pNtk 
)
static

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

Synopsis [Parses one directive.]

Description []

SideEffects []

SeeAlso []

Definition at line 1087 of file verCore.c.

1088 {
1089  char Buffer[1000], Buffer2[1000];
1090  Ver_Stream_t * p = pMan->pReader;
1091  Abc_Obj_t * pNode, * pNet;
1092  char * pWord, * pName, * pEquation;
1093  Hop_Obj_t * pFunc;
1094  char Symbol;
1095  int i, Bit, Limit, Length, fReduction;
1096  int nMsb, nLsb;
1097 
1098 // if ( Ver_StreamGetLineNumber(p) == 2756 )
1099 // {
1100 // int x = 0;
1101 // }
1102 
1103  // convert from the blackbox into the network with local functions representated by AIGs
1104  if ( !Ver_ParseConvertNetwork( pMan, pNtk, pMan->fMapped ) )
1105  return 0;
1106 
1107  while ( 1 )
1108  {
1109  // get the name of the output signal
1110  pWord = Ver_ParseGetName( pMan );
1111  if ( pWord == NULL )
1112  return 0;
1113  if ( strcmp(pWord, "#1") == 0 )
1114  continue;
1115  // check for vector-inputs
1116  if ( !Ver_ParseLookupSuffix( pMan, pWord, &nMsb, &nLsb ) )
1117  return 0;
1118  // handle special case of constant assignment
1119  Limit = nMsb > nLsb? nMsb - nLsb + 1: nLsb - nMsb + 1;
1120  if ( nMsb >= 0 && nLsb >= 0 && Limit > 1 )
1121  {
1122  // save the fanout name
1123  if ( !strcmp(pWord, "1\'h0") )
1124  strcpy( Buffer, "1\'b0" );
1125  else if ( !strcmp(pWord, "1\'h1") )
1126  strcpy( Buffer, "1\'b1" );
1127  else
1128  strcpy( Buffer, pWord );
1129  // get the equality sign
1130  if ( Ver_StreamPopChar(p) != '=' )
1131  {
1132  sprintf( pMan->sError, "Cannot read the assign statement for %s (expected equality sign).", pWord );
1133  Ver_ParsePrintErrorMessage( pMan );
1134  return 0;
1135  }
1136  // get the constant
1137  pWord = Ver_ParseGetName( pMan );
1138  if ( pWord == NULL )
1139  return 0;
1140  // check if it is indeed a constant
1141  if ( !(pWord[0] >= '0' && pWord[0] <= '9') )
1142  {
1143  sprintf( pMan->sError, "Currently can only assign vector-signal \"%s\" to be a constant.", Buffer );
1144  Ver_ParsePrintErrorMessage( pMan );
1145  return 0;
1146  }
1147 
1148  // get individual bits of the constant
1149  if ( !Ver_ParseConstant( pMan, pWord ) )
1150  return 0;
1151  // check that the constant has the same size
1152  Limit = nMsb > nLsb? nMsb - nLsb + 1: nLsb - nMsb + 1;
1153  if ( Limit != Vec_PtrSize(pMan->vNames) )
1154  {
1155  sprintf( pMan->sError, "The constant size (%d) is different from the signal\"%s\" size (%d).",
1156  Vec_PtrSize(pMan->vNames), Buffer, Limit );
1157  Ver_ParsePrintErrorMessage( pMan );
1158  return 0;
1159  }
1160  // iterate through the bits
1161  for ( i = 0, Bit = nLsb; i < Limit; i++, Bit = nMsb > nLsb ? Bit + 1: Bit - 1 )
1162  {
1163  // get the fanin net
1164  if ( Vec_PtrEntry( pMan->vNames, Limit-1-i ) )
1165  pNet = Ver_ParseFindNet( pNtk, "1\'b1" );
1166  else
1167  pNet = Ver_ParseFindNet( pNtk, "1\'b0" );
1168  assert( pNet != NULL );
1169 
1170  // create the buffer
1171  pNode = Abc_NtkCreateNodeBuf( pNtk, pNet );
1172 
1173  // get the fanout net
1174  sprintf( Buffer2, "%s[%d]", Buffer, Bit );
1175  pNet = Ver_ParseFindNet( pNtk, Buffer2 );
1176  if ( pNet == NULL )
1177  {
1178  sprintf( pMan->sError, "Cannot read the assign statement for %s (output wire is not defined).", pWord );
1179  Ver_ParsePrintErrorMessage( pMan );
1180  return 0;
1181  }
1182  Abc_ObjAddFanin( pNet, pNode );
1183  }
1184  // go to the end of the line
1185  Ver_ParseSkipComments( pMan );
1186  }
1187  else
1188  {
1189  // consider the case of reduction operations
1190  fReduction = 0;
1191  if ( pWord[0] == '{' && !pMan->fNameLast )
1192  fReduction = 1;
1193  if ( fReduction )
1194  {
1195  pWord++;
1196  pWord[strlen(pWord)-1] = 0;
1197  assert( pWord[0] != '\\' );
1198  }
1199  // get the fanout net
1200  pNet = Ver_ParseFindNet( pNtk, pWord );
1201  if ( pNet == NULL )
1202  {
1203  sprintf( pMan->sError, "Cannot read the assign statement for %s (output wire is not defined).", pWord );
1204  Ver_ParsePrintErrorMessage( pMan );
1205  return 0;
1206  }
1207  // get the equality sign
1208  if ( Ver_StreamPopChar(p) != '=' )
1209  {
1210  sprintf( pMan->sError, "Cannot read the assign statement for %s (expected equality sign).", pWord );
1211  Ver_ParsePrintErrorMessage( pMan );
1212  return 0;
1213  }
1214  // skip the comments
1215  if ( !Ver_ParseSkipComments( pMan ) )
1216  return 0;
1217  // get the second name
1218  if ( fReduction )
1219  pEquation = Ver_StreamGetWord( p, ";" );
1220  else
1221  pEquation = Ver_StreamGetWord( p, ",;" );
1222  if ( pEquation == NULL )
1223  {
1224  sprintf( pMan->sError, "Cannot read the equation for %s.", Abc_ObjName(pNet) );
1225  Ver_ParsePrintErrorMessage( pMan );
1226  return 0;
1227  }
1228 
1229  // consider the case of mapped network
1230  Vec_PtrClear( pMan->vNames );
1231  if ( pMan->fMapped )
1232  {
1233  if ( !strcmp( pEquation, "1\'b0" ) )
1234  pFunc = (Hop_Obj_t *)Mio_LibraryReadConst0((Mio_Library_t *)Abc_FrameReadLibGen());
1235  else if ( !strcmp( pEquation, "1\'b1" ) )
1236  pFunc = (Hop_Obj_t *)Mio_LibraryReadConst1((Mio_Library_t *)Abc_FrameReadLibGen());
1237  else
1238  {
1239  // "assign foo = \bar ;"
1240  if ( *pEquation == '\\' )
1241  {
1242  pEquation++;
1243  pEquation[strlen(pEquation) - 1] = 0;
1244  }
1245  if ( Ver_ParseFindNet(pNtk, pEquation) == NULL )
1246  {
1247  sprintf( pMan->sError, "Cannot read Verilog with non-trivial assignments in the mapped netlist." );
1248  Ver_ParsePrintErrorMessage( pMan );
1249  return 0;
1250  }
1251  Vec_PtrPush( pMan->vNames, (void *)(ABC_PTRUINT_T)strlen(pEquation) );
1252  Vec_PtrPush( pMan->vNames, pEquation );
1253  // get the buffer
1254  pFunc = (Hop_Obj_t *)Mio_LibraryReadBuf((Mio_Library_t *)Abc_FrameReadLibGen());
1255  if ( pFunc == NULL )
1256  {
1257  sprintf( pMan->sError, "Reading assign statement for node %s has failed because the genlib library has no buffer.", Abc_ObjName(pNet) );
1258  Ver_ParsePrintErrorMessage( pMan );
1259  return 0;
1260  }
1261  }
1262  }
1263  else
1264  {
1265  if ( !strcmp(pEquation, "0") || !strcmp(pEquation, "1\'b0") || !strcmp(pEquation, "1\'bx") )
1266  pFunc = Hop_ManConst0((Hop_Man_t *)pNtk->pManFunc);
1267  else if ( !strcmp(pEquation, "1") || !strcmp(pEquation, "1\'b1") )
1268  pFunc = Hop_ManConst1((Hop_Man_t *)pNtk->pManFunc);
1269  else if ( fReduction )
1270  pFunc = (Hop_Obj_t *)Ver_FormulaReduction( pEquation, pNtk->pManFunc, pMan->vNames, pMan->sError );
1271  else
1272  pFunc = (Hop_Obj_t *)Ver_FormulaParser( pEquation, pNtk->pManFunc, pMan->vNames, pMan->vStackFn, pMan->vStackOp, pMan->sError );
1273  if ( pFunc == NULL )
1274  {
1275  Ver_ParsePrintErrorMessage( pMan );
1276  return 0;
1277  }
1278  }
1279 
1280  // create the node with the given inputs
1281  pNode = Abc_NtkCreateNode( pNtk );
1282  pNode->pData = pFunc;
1283  Abc_ObjAddFanin( pNet, pNode );
1284  // connect to fanin nets
1285  for ( i = 0; i < Vec_PtrSize(pMan->vNames)/2; i++ )
1286  {
1287  // get the name of this signal
1288  Length = (int)(ABC_PTRUINT_T)Vec_PtrEntry( pMan->vNames, 2*i );
1289  pName = (char *)Vec_PtrEntry( pMan->vNames, 2*i + 1 );
1290  pName[Length] = 0;
1291  // try name
1292 // pNet = Ver_ParseFindNet( pNtk, pName );
1293  if ( !strcmp(pName, "1\'h0") )
1294  pNet = Ver_ParseFindNet( pNtk, "1\'b0" );
1295  else if ( !strcmp(pName, "1\'h1") )
1296  pNet = Ver_ParseFindNet( pNtk, "1\'b1" );
1297  else
1298  pNet = Ver_ParseFindNet( pNtk, pName );
1299  // find the corresponding net
1300  if ( pNet == NULL )
1301  {
1302  sprintf( pMan->sError, "Cannot read the assign statement for %s (input wire %s is not defined).", pWord, pName );
1303  Ver_ParsePrintErrorMessage( pMan );
1304  return 0;
1305  }
1306  Abc_ObjAddFanin( pNode, pNet );
1307  }
1308  }
1309 
1310  Symbol = Ver_StreamPopChar(p);
1311  if ( Symbol == ',' )
1312  continue;
1313  if ( Symbol == ';' )
1314  return 1;
1315  }
1316  return 1;
1317 }
Mio_LibraryReadBuf
Mio_Gate_t * Mio_LibraryReadBuf(Mio_Library_t *pLib)
Definition: mioApi.c:47
Ver_FormulaParser
void * Ver_FormulaParser(char *pFormula, void *pMan, Vec_Ptr_t *vNames, Vec_Ptr_t *vStackFn, Vec_Int_t *vStackOp, char *pErrorMessage)
FUNCTION DEFINITIONS ///.
Definition: verFormula.c:76
Abc_FrameReadLibGen
ABC_DLL void * Abc_FrameReadLibGen()
Definition: mainFrame.c:56
Hop_ManConst1
static Hop_Obj_t * Hop_ManConst1(Hop_Man_t *p)
Definition: hop.h:132
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Ver_StreamPopChar
char Ver_StreamPopChar(Ver_Stream_t *p)
Definition: verStream.c:275
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
Ver_ParseConvertNetwork
int Ver_ParseConvertNetwork(Ver_Man_t *pMan, Abc_Ntk_t *pNtk, int fMapped)
Definition: verCore.c:351
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Ver_ParseSkipComments
int Ver_ParseSkipComments(Ver_Man_t *p)
DECLARATIONS ///.
Definition: verParse.c:45
Hop_Obj_t_
Definition: hop.h:65
Ver_StreamGetWord
char * Ver_StreamGetWord(Ver_Stream_t *p, char *pCharsToStop)
Definition: verStream.c:397
Abc_ObjAddFanin
ABC_DLL void Abc_ObjAddFanin(Abc_Obj_t *pObj, Abc_Obj_t *pFanin)
Definition: abcFanio.c:84
strcmp
int strcmp()
Ver_Stream_t_
Definition: verStream.c:36
Abc_Obj_t_
Definition: abc.h:128
Mio_LibraryReadConst1
Mio_Gate_t * Mio_LibraryReadConst1(Mio_Library_t *pLib)
Definition: mioApi.c:50
Abc_Ntk_t_::pManFunc
void * pManFunc
Definition: abc.h:191
Ver_ParseLookupSuffix
int Ver_ParseLookupSuffix(Ver_Man_t *pMan, char *pWord, int *pnMsb, int *pnLsb)
Definition: verCore.c:563
Ver_ParseConstant
int Ver_ParseConstant(Ver_Man_t *pMan, char *pWord)
Definition: verCore.c:753
Abc_NtkCreateNodeBuf
ABC_DLL Abc_Obj_t * Abc_NtkCreateNodeBuf(Abc_Ntk_t *pNtk, Abc_Obj_t *pFanin)
Definition: abcObj.c:692
Ver_ParseGetName
char * Ver_ParseGetName(Ver_Man_t *p)
Definition: verParse.c:91
Mio_LibraryStruct_t_
STRUCTURE DEFINITIONS ///.
Definition: mioInt.h:61
sprintf
char * sprintf()
strcpy
char * strcpy()
Vec_PtrEntry
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
Abc_ObjName
ABC_DLL char * Abc_ObjName(Abc_Obj_t *pNode)
DECLARATIONS ///.
Definition: abcNames.c:48
Abc_NtkCreateNode
static Abc_Obj_t * Abc_NtkCreateNode(Abc_Ntk_t *pNtk)
Definition: abc.h:308
Ver_ParsePrintErrorMessage
void Ver_ParsePrintErrorMessage(Ver_Man_t *p)
Definition: verCore.c:278
assert
#define assert(ex)
Definition: util_old.h:213
Vec_PtrClear
static void Vec_PtrClear(Vec_Ptr_t *p)
Definition: vecPtr.h:545
strlen
int strlen()
Ver_FormulaReduction
void * Ver_FormulaReduction(char *pFormula, void *pMan, Vec_Ptr_t *vNames, char *pErrorMessage)
Definition: verFormula.c:435
Hop_ManConst0
static Hop_Obj_t * Hop_ManConst0(Hop_Man_t *p)
Definition: hop.h:131
Abc_Obj_t_::pData
void * pData
Definition: abc.h:145
Mio_LibraryReadConst0
Mio_Gate_t * Mio_LibraryReadConst0(Mio_Library_t *pLib)
Definition: mioApi.c:49
Hop_Man_t
typedefABC_NAMESPACE_HEADER_START struct Hop_Man_t_ Hop_Man_t
INCLUDES ///.
Definition: hop.h:49
Ver_ParseFindNet
Abc_Obj_t * Ver_ParseFindNet(Abc_Ntk_t *pNtk, char *pName)
Definition: verCore.c:328
int Ver_ParseAttachBoxes ( Ver_Man_t *  pMan)
static

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 []

Definition at line 2870 of file verCore.c.

2871 {
2872  int fPrintLog = 1;
2873  Abc_Ntk_t * pNtk = NULL;
2874  Ver_Bundle_t * pBundle;
2875  Vec_Ptr_t * vUndefs;
2876  int i, RetValue, Counter, nMaxBoxSize;
2877 
2878  // print the log file
2879  if ( fPrintLog && pMan->pDesign->vModules && Vec_PtrSize(pMan->pDesign->vModules) > 1 )
2880  Ver_ParsePrintLog( pMan );
2881 
2882  // connect defined boxes
2883  RetValue = Ver_ParseConnectDefBoxes( pMan );
2884  if ( RetValue < 2 )
2885  return RetValue;
2886 
2887  // report the boxes
2888  Ver_ParseReportUndefBoxes( pMan );
2889 
2890  // collect undef box types and their actual instances
2891  vUndefs = Ver_ParseCollectUndefBoxes( pMan );
2892  assert( Vec_PtrSize( vUndefs ) > 0 );
2893 
2894  // go through all undef box types
2895  Counter = 0;
2896  nMaxBoxSize = Ver_ParseMaxBoxSize( vUndefs );
2897  while ( Ver_ParseCheckNondrivenNets(vUndefs) && Counter < nMaxBoxSize )
2898  {
2899  // go through undef box types
2900  pBundle = NULL;
2901  Vec_PtrForEachEntry( Abc_Ntk_t *, vUndefs, pNtk, i )
2902  if ( (pBundle = Ver_ParseGetNondrivenBundle( pNtk, Counter )) )
2903  break;
2904  if ( pBundle == NULL )
2905  {
2906  Counter++;
2907  continue;
2908  }
2909  // drive this bundle by this box
2910  if ( !Ver_ParseDriveFormal( pMan, pNtk, pBundle ) )
2911  return 0;
2912  }
2913 
2914  // make all the remaining bundles the drivers of undefs
2915  if ( !Ver_ParseDriveInputs( pMan, vUndefs ) )
2916  return 0;
2917 
2918  // cleanup
2919  Vec_PtrForEachEntry( Abc_Ntk_t *, vUndefs, pNtk, i )
2920  {
2921  Vec_PtrFree( (Vec_Ptr_t *)pNtk->pData );
2922  pNtk->pData = NULL;
2923  }
2924  Vec_PtrFree( vUndefs );
2925  return 1;
2926 }
Ver_ParseGetNondrivenBundle
Ver_Bundle_t * Ver_ParseGetNondrivenBundle(Abc_Ntk_t *pNtk, int Counter)
Definition: verCore.c:2509
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Ver_ParseDriveInputs
int Ver_ParseDriveInputs(Ver_Man_t *pMan, Vec_Ptr_t *vUndefs)
Definition: verCore.c:2616
Abc_Ntk_t_
Definition: abc.h:153
Ver_ParseCollectUndefBoxes
Vec_Ptr_t * Ver_ParseCollectUndefBoxes(Ver_Man_t *pMan)
Definition: verCore.c:2356
Ver_ParseDriveFormal
int Ver_ParseDriveFormal(Ver_Man_t *pMan, Abc_Ntk_t *pNtk, Ver_Bundle_t *pBundle0)
Definition: verCore.c:2542
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Abc_Ntk_t_::pData
void * pData
Definition: abc.h:203
if
if(last==0)
Definition: sparse_int.h:34
Ver_ParseCheckNondrivenNets
int Ver_ParseCheckNondrivenNets(Vec_Ptr_t *vUndefs)
Definition: verCore.c:2440
Ver_ParsePrintLog
void Ver_ParsePrintLog(Ver_Man_t *pMan)
Definition: verCore.c:2735
Counter
static int Counter
Definition: extraBddMisc.c:1877
Ver_Bundle_t_
Definition: verCore.c:83
Ver_ParseReportUndefBoxes
void Ver_ParseReportUndefBoxes(Ver_Man_t *pMan)
Definition: verCore.c:2400
assert
#define assert(ex)
Definition: util_old.h:213
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
Ver_ParseMaxBoxSize
int Ver_ParseMaxBoxSize(Vec_Ptr_t *vUndefs)
Definition: verCore.c:2709
Ver_ParseConnectDefBoxes
int Ver_ParseConnectDefBoxes(Ver_Man_t *pMan)
Definition: verCore.c:2310
Vec_PtrFree
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
int Ver_ParseBox ( Ver_Man_t *  pMan,
Abc_Ntk_t *  pNtk,
Abc_Ntk_t *  pNtkBox 
)
static

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

Synopsis [Parses one directive.]

Description []

SideEffects []

SeeAlso []

Definition at line 1732 of file verCore.c.

1733 {
1734  char Buffer[1000];
1735  Ver_Stream_t * p = pMan->pReader;
1736  Ver_Bundle_t * pBundle;
1737  Vec_Ptr_t * vBundles;
1738  Abc_Obj_t * pNetActual;
1739  Abc_Obj_t * pNode;
1740  char * pWord, Symbol;
1741  int fCompl, fFormalIsGiven;
1742  int i, k, Bit, Limit, nMsb, nLsb, fQuit, flag;
1743 
1744  // gate the name of the box
1745  pWord = Ver_ParseGetName( pMan );
1746  if ( pWord == NULL )
1747  return 0;
1748 
1749  // create a box with this name
1750  pNode = Abc_NtkCreateBlackbox( pNtk );
1751  pNode->pData = pNtkBox;
1752  Abc_ObjAssignName( pNode, pWord, NULL );
1753 
1754  // continue parsing the box
1755  if ( Ver_StreamPopChar(p) != '(' )
1756  {
1757  sprintf( pMan->sError, "Cannot parse box %s (expected opening paranthesis).", Abc_ObjName(pNode) );
1758  Ver_ParsePrintErrorMessage( pMan );
1759  return 0;
1760  }
1761  Ver_ParseSkipComments( pMan );
1762 
1763  // parse pairs of formal/actual inputs
1764  vBundles = Vec_PtrAlloc( 16 );
1765  pNode->pCopy = (Abc_Obj_t *)vBundles;
1766  while ( 1 )
1767  {
1768  // allocate the bundle (formal name + array of actual nets)
1769  pBundle = ABC_ALLOC( Ver_Bundle_t, 1 );
1770  pBundle->pNameFormal = NULL;
1771  pBundle->vNetsActual = Vec_PtrAlloc( 4 );
1772  Vec_PtrPush( vBundles, pBundle );
1773 
1774  // process one pair of formal/actual parameters
1775  fFormalIsGiven = 0;
1776  if ( Ver_StreamScanChar(p) == '.' )
1777  {
1778  fFormalIsGiven = 1;
1779  if ( Ver_StreamPopChar(p) != '.' )
1780  {
1781  sprintf( pMan->sError, "Cannot parse box %s (expected .).", Abc_ObjName(pNode) );
1782  Ver_ParsePrintErrorMessage( pMan );
1783  return 0;
1784  }
1785 
1786  // parse the formal name
1787  pWord = Ver_ParseGetName( pMan );
1788  if ( pWord == NULL )
1789  return 0;
1790 
1791  // save the name
1792  pBundle->pNameFormal = Extra_UtilStrsav( pWord );
1793 
1794  // open the paranthesis
1795  if ( Ver_StreamPopChar(p) != '(' )
1796  {
1797  sprintf( pMan->sError, "Cannot formal parameter %s of box %s (expected opening paranthesis).", pWord, Abc_ObjName(pNode));
1798  Ver_ParsePrintErrorMessage( pMan );
1799  return 0;
1800  }
1801  Ver_ParseSkipComments( pMan );
1802  }
1803 
1804  // check if this is the beginning of {} expression
1805  Symbol = Ver_StreamScanChar(p);
1806 
1807  // consider the case of vector-inputs
1808  if ( Symbol == '{' )
1809  {
1810  // skip this char
1811  Ver_StreamPopChar(p);
1812 
1813  // read actual names
1814  i = 0;
1815  fQuit = 0;
1816  while ( 1 )
1817  {
1818  // parse the formal name
1819  Ver_ParseSkipComments( pMan );
1820  pWord = Ver_ParseGetName( pMan );
1821  if ( pWord == NULL )
1822  return 0;
1823 
1824  // check if the last char is a closing brace
1825  if ( pWord[strlen(pWord)-1] == '}' )
1826  {
1827  pWord[strlen(pWord)-1] = 0;
1828  fQuit = 1;
1829  }
1830  if ( pWord[0] == 0 )
1831  break;
1832 
1833  // check for constant
1834  if ( pWord[0] >= '1' && pWord[0] <= '9' )
1835  {
1836  if ( !Ver_ParseConstant( pMan, pWord ) )
1837  return 0;
1838  // add constant MSB to LSB
1839  for ( k = 0; k < Vec_PtrSize(pMan->vNames); k++, i++ )
1840  {
1841  // get the actual net
1842  sprintf( Buffer, "1\'b%d", (int)(Vec_PtrEntry(pMan->vNames,k) != NULL) );
1843  pNetActual = Ver_ParseFindNet( pNtk, Buffer );
1844  if ( pNetActual == NULL )
1845  {
1846  sprintf( pMan->sError, "Actual net \"%s\" is missing in gate \"%s\".", Buffer, Abc_ObjName(pNode) );
1847  Ver_ParsePrintErrorMessage( pMan );
1848  return 0;
1849  }
1850  Vec_PtrPush( pBundle->vNetsActual, pNetActual );
1851  }
1852  }
1853  else
1854  {
1855  // get the suffix of the form [m:n]
1856  if ( pWord[strlen(pWord)-1] == ']' && !pMan->fNameLast )
1857  Ver_ParseSignalSuffix( pMan, pWord, &nMsb, &nLsb );
1858  else
1859  Ver_ParseLookupSuffix( pMan, pWord, &nMsb, &nLsb );
1860 
1861  // generate signals
1862  if ( nMsb == -1 && nLsb == -1 )
1863  {
1864  // get the actual net
1865  pNetActual = Ver_ParseFindNet( pNtk, pWord );
1866  if ( pNetActual == NULL )
1867  {
1868  if ( !strncmp(pWord, "Open_", 5) ||
1869  !strncmp(pWord, "dct_unconnected", 15) )
1870  pNetActual = Abc_NtkCreateNet( pNtk );
1871  else
1872  {
1873  sprintf( pMan->sError, "Actual net \"%s\" is missing in box \"%s\".", pWord, Abc_ObjName(pNode) );
1874  Ver_ParsePrintErrorMessage( pMan );
1875  return 0;
1876  }
1877  }
1878  Vec_PtrPush( pBundle->vNetsActual, pNetActual );
1879  i++;
1880  }
1881  else
1882  {
1883  // go from MSB to LSB
1884  assert( nMsb >= 0 && nLsb >= 0 );
1885  Limit = (nMsb > nLsb) ? nMsb - nLsb + 1: nLsb - nMsb + 1;
1886  for ( Bit = nMsb, k = Limit - 1; k >= 0; Bit = (nMsb > nLsb ? Bit - 1: Bit + 1), k--, i++ )
1887  {
1888  // get the actual net
1889  sprintf( Buffer, "%s[%d]", pWord, Bit );
1890  pNetActual = Ver_ParseFindNet( pNtk, Buffer );
1891  if ( pNetActual == NULL )
1892  {
1893  if ( !strncmp(pWord, "Open_", 5) ||
1894  !strncmp(pWord, "dct_unconnected", 15) )
1895  pNetActual = Abc_NtkCreateNet( pNtk );
1896  else
1897  {
1898  sprintf( pMan->sError, "Actual net \"%s\" is missing in box \"%s\".", pWord, Abc_ObjName(pNode) );
1899  Ver_ParsePrintErrorMessage( pMan );
1900  return 0;
1901  }
1902  }
1903  Vec_PtrPush( pBundle->vNetsActual, pNetActual );
1904  }
1905  }
1906  }
1907 
1908  if ( fQuit )
1909  break;
1910 
1911  // skip comma
1912  Ver_ParseSkipComments( pMan );
1913  Symbol = Ver_StreamPopChar(p);
1914  if ( Symbol == '}' )
1915  break;
1916  if ( Symbol != ',' )
1917  {
1918  sprintf( pMan->sError, "Cannot parse formal parameter %s of gate %s (expected comma).", pWord, Abc_ObjName(pNode) );
1919  Ver_ParsePrintErrorMessage( pMan );
1920  return 0;
1921  }
1922  }
1923  }
1924  else
1925  {
1926  // get the next word
1927  pWord = Ver_ParseGetName( pMan );
1928  if ( pWord == NULL )
1929  return 0;
1930  // consider the case of empty name
1931  fCompl = 0;
1932  if ( pWord[0] == 0 )
1933  {
1934  pNetActual = Abc_NtkCreateNet( pNtk );
1935  Vec_PtrPush( pBundle->vNetsActual, Abc_ObjNotCond( pNetActual, fCompl ) );
1936  }
1937  else
1938  {
1939  // get the actual net
1940  flag=0;
1941  pNetActual = Ver_ParseFindNet( pNtk, pWord );
1942  if ( pNetActual == NULL )
1943  {
1944  Ver_ParseLookupSuffix( pMan, pWord, &nMsb, &nLsb );
1945  if ( nMsb == -1 && nLsb == -1 )
1946  {
1947  Ver_ParseSignalSuffix( pMan, pWord, &nMsb, &nLsb );
1948  if ( nMsb == -1 && nLsb == -1 )
1949  {
1950  if ( !strncmp(pWord, "Open_", 5) ||
1951  !strncmp(pWord, "dct_unconnected", 15) )
1952  {
1953  pNetActual = Abc_NtkCreateNet( pNtk );
1954  Vec_PtrPush( pBundle->vNetsActual, pNetActual );
1955  }
1956  else
1957  {
1958  sprintf( pMan->sError, "Actual net \"%s\" is missing in box \"%s\".", pWord, Abc_ObjName(pNode) );
1959  Ver_ParsePrintErrorMessage( pMan );
1960  return 0;
1961  }
1962  }
1963  else
1964  {
1965  flag=1;
1966  }
1967  }
1968  else
1969  {
1970  flag=1;
1971  }
1972  if (flag)
1973  {
1974  Limit = (nMsb > nLsb) ? nMsb - nLsb + 1: nLsb - nMsb + 1;
1975  for ( Bit = nMsb, k = Limit - 1; k >= 0; Bit = (nMsb > nLsb ? Bit - 1: Bit + 1), k--)
1976  {
1977  // get the actual net
1978  sprintf( Buffer, "%s[%d]", pWord, Bit );
1979  pNetActual = Ver_ParseFindNet( pNtk, Buffer );
1980  if ( pNetActual == NULL )
1981  {
1982  if ( !strncmp(pWord, "Open_", 5) ||
1983  !strncmp(pWord, "dct_unconnected", 15))
1984  pNetActual = Abc_NtkCreateNet( pNtk );
1985  else
1986  {
1987  sprintf( pMan->sError, "Actual net \"%s\" is missing in box \"%s\".", pWord, Abc_ObjName(pNode) );
1988  Ver_ParsePrintErrorMessage( pMan );
1989  return 0;
1990  }
1991  }
1992  Vec_PtrPush( pBundle->vNetsActual, pNetActual );
1993  }
1994  }
1995  }
1996  else
1997  {
1998  Vec_PtrPush( pBundle->vNetsActual, Abc_ObjNotCond( pNetActual, fCompl ) );
1999  }
2000  }
2001  }
2002 
2003  if ( fFormalIsGiven )
2004  {
2005  // close the paranthesis
2006  Ver_ParseSkipComments( pMan );
2007  if ( Ver_StreamPopChar(p) != ')' )
2008  {
2009  sprintf( pMan->sError, "Cannot parse formal parameter %s of box %s (expected closing paranthesis).", pWord, Abc_ObjName(pNode) );
2010  Ver_ParsePrintErrorMessage( pMan );
2011  return 0;
2012  }
2013  Ver_ParseSkipComments( pMan );
2014  }
2015 
2016  // check if it is the end of gate
2017  Symbol = Ver_StreamPopChar(p);
2018  if ( Symbol == ')' )
2019  break;
2020  // skip comma
2021  if ( Symbol != ',' )
2022  {
2023  sprintf( pMan->sError, "Cannot parse formal parameter %s of box %s (expected comma).", pWord, Abc_ObjName(pNode) );
2024  Ver_ParsePrintErrorMessage( pMan );
2025  return 0;
2026  }
2027  Ver_ParseSkipComments( pMan );
2028  }
2029 
2030  // check if it is the end of gate
2031  Ver_ParseSkipComments( pMan );
2032  if ( Ver_StreamPopChar(p) != ';' )
2033  {
2034  sprintf( pMan->sError, "Cannot read box %s (expected closing semicolumn).", Abc_ObjName(pNode) );
2035  Ver_ParsePrintErrorMessage( pMan );
2036  return 0;
2037  }
2038 
2039  return 1;
2040 }
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Ver_ParseSignalSuffix
int Ver_ParseSignalSuffix(Ver_Man_t *pMan, char *pWord, int *pnMsb, int *pnLsb)
Definition: verCore.c:699
Ver_StreamPopChar
char Ver_StreamPopChar(Ver_Stream_t *p)
Definition: verStream.c:275
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Abc_ObjAssignName
ABC_DLL char * Abc_ObjAssignName(Abc_Obj_t *pObj, char *pName, char *pSuffix)
Definition: abcNames.c:68
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Ver_ParseSkipComments
int Ver_ParseSkipComments(Ver_Man_t *p)
DECLARATIONS ///.
Definition: verParse.c:45
Extra_UtilStrsav
char * Extra_UtilStrsav(const char *s)
Definition: extraUtilUtil.c:169
Ver_Stream_t_
Definition: verStream.c:36
Abc_Obj_t_
Definition: abc.h:128
Ver_StreamScanChar
char Ver_StreamScanChar(Ver_Stream_t *p)
Definition: verStream.c:258
Ver_ParseLookupSuffix
int Ver_ParseLookupSuffix(Ver_Man_t *pMan, char *pWord, int *pnMsb, int *pnLsb)
Definition: verCore.c:563
Abc_Obj_t_::pCopy
Abc_Obj_t * pCopy
Definition: abc.h:148
Ver_ParseConstant
int Ver_ParseConstant(Ver_Man_t *pMan, char *pWord)
Definition: verCore.c:753
Ver_ParseGetName
char * Ver_ParseGetName(Ver_Man_t *p)
Definition: verParse.c:91
Ver_Bundle_t_::pNameFormal
char * pNameFormal
Definition: verCore.c:85
sprintf
char * sprintf()
Abc_NtkCreateBlackbox
static Abc_Obj_t * Abc_NtkCreateBlackbox(Abc_Ntk_t *pNtk)
Definition: abc.h:311
Ver_Bundle_t_::vNetsActual
Vec_Ptr_t * vNetsActual
Definition: verCore.c:86
Ver_Bundle_t_
Definition: verCore.c:83
Vec_PtrEntry
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
Vec_PtrAlloc
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
Abc_ObjName
ABC_DLL char * Abc_ObjName(Abc_Obj_t *pNode)
DECLARATIONS ///.
Definition: abcNames.c:48
Ver_ParsePrintErrorMessage
void Ver_ParsePrintErrorMessage(Ver_Man_t *p)
Definition: verCore.c:278
strncmp
int strncmp()
Abc_ObjNotCond
static Abc_Obj_t * Abc_ObjNotCond(Abc_Obj_t *p, int c)
Definition: abc.h:325
assert
#define assert(ex)
Definition: util_old.h:213
strlen
int strlen()
Abc_Obj_t_::pData
void * pData
Definition: abc.h:145
Abc_NtkCreateNet
static Abc_Obj_t * Abc_NtkCreateNet(Abc_Ntk_t *pNtk)
Definition: abc.h:307
Ver_ParseFindNet
Abc_Obj_t * Ver_ParseFindNet(Abc_Ntk_t *pNtk, char *pName)
Definition: verCore.c:328
int Ver_ParseCheckNondrivenNets ( Vec_Ptr_t *  vUndefs)

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

Synopsis [Returns 1 if there are non-driven nets.]

Description []

SideEffects []

SeeAlso []

Definition at line 2440 of file verCore.c.

2441 {
2442  Abc_Ntk_t * pNtk;
2443  Ver_Bundle_t * pBundle;
2444  Abc_Obj_t * pBox, * pNet;
2445  int i, k, j, m;
2446  // go through undef box types
2447  Vec_PtrForEachEntry( Abc_Ntk_t *, vUndefs, pNtk, i )
2448  // go through instances of this type
2449  Vec_PtrForEachEntry( Abc_Obj_t *, (Vec_Ptr_t *)pNtk->pData, pBox, k )
2450  // go through the bundles of this instance
2451  Vec_PtrForEachEntryReverse( Ver_Bundle_t *, (Vec_Ptr_t *)pBox->pCopy, pBundle, j )
2452  // go through the actual nets of this bundle
2453  if ( pBundle )
2454  Vec_PtrForEachEntry( Abc_Obj_t *, pBundle->vNetsActual, pNet, m )
2455  {
2456  if ( Abc_ObjFaninNum(pNet) == 0 ) // non-driven
2457  if ( strcmp(Abc_ObjName(pNet), "1\'b0") && strcmp(Abc_ObjName(pNet), "1\'b1") ) // diff from a const
2458  return 1;
2459  }
2460  return 0;
2461 }
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Vec_PtrForEachEntryReverse
#define Vec_PtrForEachEntryReverse(Type, vVec, pEntry, i)
Definition: vecPtr.h:63
Abc_Ntk_t_
Definition: abc.h:153
Abc_ObjFaninNum
static int Abc_ObjFaninNum(Abc_Obj_t *pObj)
Definition: abc.h:364
strcmp
int strcmp()
Abc_Obj_t_
Definition: abc.h:128
if
if(last==0)
Definition: sparse_int.h:34
Ver_Bundle_t_
Definition: verCore.c:83
Abc_ObjName
ABC_DLL char * Abc_ObjName(Abc_Obj_t *pNode)
DECLARATIONS ///.
Definition: abcNames.c:48
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
Vec_Ptr_t* Ver_ParseCollectUndefBoxes ( Ver_Man_t *  pMan)

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

Synopsis [Collects the undef boxes and maps them into their instances.]

Description []

SideEffects []

SeeAlso []

Definition at line 2356 of file verCore.c.

2357 {
2358  Vec_Ptr_t * vUndefs;
2359  Abc_Ntk_t * pNtk, * pNtkBox;
2360  Abc_Obj_t * pBox;
2361  int i, k;
2362  // clear the module structures
2363  Vec_PtrForEachEntry( Abc_Ntk_t *, pMan->pDesign->vModules, pNtk, i )
2364  pNtk->pData = NULL;
2365  // go through all the blackboxes
2366  vUndefs = Vec_PtrAlloc( 16 );
2367  Vec_PtrForEachEntry( Abc_Ntk_t *, pMan->pDesign->vModules, pNtk, i )
2368  {
2369  Abc_NtkForEachBlackbox( pNtk, pBox, k )
2370  {
2371  pNtkBox = (Abc_Ntk_t *)pBox->pData;
2372  if ( pNtkBox == NULL )
2373  continue;
2374  if ( Ver_NtkIsDefined(pNtkBox) )
2375  continue;
2376  if ( pNtkBox->pData == NULL )
2377  {
2378  // save the box
2379  Vec_PtrPush( vUndefs, pNtkBox );
2380  pNtkBox->pData = Vec_PtrAlloc( 16 );
2381  }
2382  // save the instance
2383  Vec_PtrPush( (Vec_Ptr_t *)pNtkBox->pData, pBox );
2384  }
2385  }
2386  return vUndefs;
2387 }
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Abc_Ntk_t_
Definition: abc.h:153
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
Abc_Ntk_t_::pData
void * pData
Definition: abc.h:203
Abc_Obj_t_
Definition: abc.h:128
Abc_NtkForEachBlackbox
#define Abc_NtkForEachBlackbox(pNtk, pObj, i)
Definition: abc.h:509
if
if(last==0)
Definition: sparse_int.h:34
Vec_PtrAlloc
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
Abc_Des_t_::vModules
Vec_Ptr_t * vModules
Definition: abc.h:223
Abc_Obj_t_::pData
void * pData
Definition: abc.h:145
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
Abc_Ntk_t_::pDesign
Abc_Des_t * pDesign
Definition: abc.h:180
Ver_NtkIsDefined
static int Ver_NtkIsDefined(Abc_Ntk_t *pNtkBox)
Definition: verCore.c:77
int Ver_ParseConnectBox ( Ver_Man_t *  pMan,
Abc_Obj_t *  pBox 
)
static

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

Synopsis [Connects one box to the network]

Description []

SideEffects []

SeeAlso []

Definition at line 2071 of file verCore.c.

2072 {
2073  Vec_Ptr_t * vBundles = (Vec_Ptr_t *)pBox->pCopy;
2074  Abc_Ntk_t * pNtk = pBox->pNtk;
2075  Abc_Ntk_t * pNtkBox = (Abc_Ntk_t *)pBox->pData;
2076  Abc_Obj_t * pTerm, * pTermNew, * pNetAct;
2077  Ver_Bundle_t * pBundle;
2078  char * pNameFormal;
2079  int i, k, j, iBundle, Length;
2080 
2081  assert( !Ver_ObjIsConnected(pBox) );
2082  assert( Ver_NtkIsDefined(pNtkBox) );
2083  assert( !Abc_NtkHasBlackbox(pNtkBox) || Abc_NtkBoxNum(pNtkBox) == 1 );
2084 
2085 /*
2086  // clean the PI/PO nets
2087  Abc_NtkForEachPi( pNtkBox, pTerm, i )
2088  Abc_ObjFanout0(pTerm)->pCopy = NULL;
2089  Abc_NtkForEachPo( pNtkBox, pTerm, i )
2090  Abc_ObjFanin0(pTerm)->pCopy = NULL;
2091 */
2092 
2093  // check the number of actual nets is the same as the number of formal nets
2094  if ( Vec_PtrSize(vBundles) > Abc_NtkPiNum(pNtkBox) + Abc_NtkPoNum(pNtkBox) )
2095  {
2096  sprintf( pMan->sError, "The number of actual IOs (%d) is bigger than the number of formal IOs (%d) when instantiating network %s in box %s.",
2097  Vec_PtrSize(vBundles), Abc_NtkPiNum(pNtkBox) + Abc_NtkPoNum(pNtkBox), pNtkBox->pName, Abc_ObjName(pBox) );
2098  // free the bundling
2099  Vec_PtrForEachEntry( Ver_Bundle_t *, vBundles, pBundle, k )
2100  Ver_ParseFreeBundle( pBundle );
2101  Vec_PtrFree( vBundles );
2102  pBox->pCopy = NULL;
2103  Ver_ParsePrintErrorMessage( pMan );
2104  return 0;
2105  }
2106 
2107  // check if some of them do not have formal names
2108  Vec_PtrForEachEntry( Ver_Bundle_t *, vBundles, pBundle, k )
2109  if ( pBundle->pNameFormal == NULL )
2110  break;
2111  if ( k < Vec_PtrSize(vBundles) )
2112  {
2113  printf( "Warning: The instance %s of network %s will be connected without using formal names.\n", pNtkBox->pName, Abc_ObjName(pBox) );
2114  // add all actual nets in the bundles
2115  iBundle = 0;
2116  Vec_PtrForEachEntry( Ver_Bundle_t *, vBundles, pBundle, j )
2117  iBundle += Vec_PtrSize(pBundle->vNetsActual);
2118 
2119  // check the number of actual nets is the same as the number of formal nets
2120  if ( iBundle != Abc_NtkPiNum(pNtkBox) + Abc_NtkPoNum(pNtkBox) )
2121  {
2122  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.",
2123  Vec_PtrSize(vBundles), Abc_NtkPiNum(pNtkBox) + Abc_NtkPoNum(pNtkBox), pNtkBox->pName, Abc_ObjName(pBox) );
2124  // free the bundling
2125  Vec_PtrForEachEntry( Ver_Bundle_t *, vBundles, pBundle, k )
2126  Ver_ParseFreeBundle( pBundle );
2127  Vec_PtrFree( vBundles );
2128  pBox->pCopy = NULL;
2129  Ver_ParsePrintErrorMessage( pMan );
2130  return 0;
2131  }
2132  // connect bundles in the natural order
2133  iBundle = 0;
2134  Abc_NtkForEachPi( pNtkBox, pTerm, i )
2135  {
2136  pBundle = (Ver_Bundle_t *)Vec_PtrEntry( vBundles, iBundle++ );
2137  // the bundle is found - add the connections - using order LSB to MSB
2138  Vec_PtrForEachEntryReverse( Abc_Obj_t *, pBundle->vNetsActual, pNetAct, k )
2139  {
2140  pTermNew = Abc_NtkCreateBi( pNtk );
2141  Abc_ObjAddFanin( pBox, pTermNew );
2142  Abc_ObjAddFanin( pTermNew, pNetAct );
2143  i++;
2144  }
2145  i--;
2146  }
2147  // create fanins of the box
2148  Abc_NtkForEachPo( pNtkBox, pTerm, i )
2149  {
2150  pBundle = (Ver_Bundle_t *)Vec_PtrEntry( vBundles, iBundle++ );
2151  // the bundle is found - add the connections - using order LSB to MSB
2152  Vec_PtrForEachEntryReverse( Abc_Obj_t *, pBundle->vNetsActual, pNetAct, k )
2153  {
2154  pTermNew = Abc_NtkCreateBo( pNtk );
2155  Abc_ObjAddFanin( pTermNew, pBox );
2156  Abc_ObjAddFanin( pNetAct, pTermNew );
2157  i++;
2158  }
2159  i--;
2160  }
2161 
2162  // free the bundling
2163  Vec_PtrForEachEntry( Ver_Bundle_t *, vBundles, pBundle, k )
2164  Ver_ParseFreeBundle( pBundle );
2165  Vec_PtrFree( vBundles );
2166  pBox->pCopy = NULL;
2167  return 1;
2168  }
2169 
2170  // bundles arrive in any order - but inside each bundle the order is MSB to LSB
2171  // make sure every formal PI has a corresponding net
2172  Abc_NtkForEachPi( pNtkBox, pTerm, i )
2173  {
2174  // get the name of this formal net
2175  pNameFormal = Abc_ObjName( Abc_ObjFanout0(pTerm) );
2176  // try to find the bundle with this formal net
2177  pBundle = NULL;
2178  Vec_PtrForEachEntry( Ver_Bundle_t *, vBundles, pBundle, k )
2179  if ( !strcmp(pBundle->pNameFormal, pNameFormal) )
2180  break;
2181  assert( pBundle != NULL );
2182  // if the bundle is not found, try without parantheses
2183  if ( k == Vec_PtrSize(vBundles) )
2184  {
2185  pBundle = NULL;
2186  Length = strlen(pNameFormal);
2187  if ( pNameFormal[Length-1] == ']' )
2188  {
2189  // find the opening brace
2190  for ( Length--; Length >= 0; Length-- )
2191  if ( pNameFormal[Length] == '[' )
2192  break;
2193  // compare names before brace
2194  if ( Length > 0 )
2195  {
2196  Vec_PtrForEachEntry( Ver_Bundle_t *, vBundles, pBundle, j )
2197  if ( !strncmp(pBundle->pNameFormal, pNameFormal, Length) && (int)strlen(pBundle->pNameFormal) == Length )
2198  break;
2199  if ( j == Vec_PtrSize(vBundles) )
2200  pBundle = NULL;
2201  }
2202  }
2203  if ( pBundle == NULL )
2204  {
2205  sprintf( pMan->sError, "Cannot find an actual net for the formal net %s when instantiating network %s in box %s.",
2206  pNameFormal, pNtkBox->pName, Abc_ObjName(pBox) );
2207  Ver_ParsePrintErrorMessage( pMan );
2208  return 0;
2209  }
2210  }
2211  // the bundle is found - add the connections - using order LSB to MSB
2212  Vec_PtrForEachEntryReverse( Abc_Obj_t *, pBundle->vNetsActual, pNetAct, k )
2213  {
2214  pTermNew = Abc_NtkCreateBi( pNtk );
2215  Abc_ObjAddFanin( pBox, pTermNew );
2216  Abc_ObjAddFanin( pTermNew, pNetAct );
2217  i++;
2218  }
2219  i--;
2220  }
2221 
2222  // connect those formal POs that do have nets
2223  Abc_NtkForEachPo( pNtkBox, pTerm, i )
2224  {
2225  // get the name of this PI
2226  pNameFormal = Abc_ObjName( Abc_ObjFanin0(pTerm) );
2227  // try to find this formal net in the bundle
2228  pBundle = NULL;
2229  Vec_PtrForEachEntry( Ver_Bundle_t *, vBundles, pBundle, k )
2230  if ( !strcmp(pBundle->pNameFormal, pNameFormal) )
2231  break;
2232  assert( pBundle != NULL );
2233  // if the name is not found, try without parantheses
2234  if ( k == Vec_PtrSize(vBundles) )
2235  {
2236  pBundle = NULL;
2237  Length = strlen(pNameFormal);
2238  if ( pNameFormal[Length-1] == ']' )
2239  {
2240  // find the opening brace
2241  for ( Length--; Length >= 0; Length-- )
2242  if ( pNameFormal[Length] == '[' )
2243  break;
2244  // compare names before brace
2245  if ( Length > 0 )
2246  {
2247  Vec_PtrForEachEntry( Ver_Bundle_t *, vBundles, pBundle, j )
2248  if ( !strncmp(pBundle->pNameFormal, pNameFormal, Length) && (int)strlen(pBundle->pNameFormal) == Length )
2249  break;
2250  if ( j == Vec_PtrSize(vBundles) )
2251  pBundle = NULL;
2252  }
2253  }
2254  if ( pBundle == NULL )
2255  {
2256  char Buffer[1000];
2257 // printf( "Warning: The formal output %s is not driven when instantiating network %s in box %s.",
2258 // pNameFormal, pNtkBox->pName, Abc_ObjName(pBox) );
2259  pTermNew = Abc_NtkCreateBo( pNtk );
2260  sprintf( Buffer, "_temp_net%d", Abc_ObjId(pTermNew) );
2261  pNetAct = Abc_NtkFindOrCreateNet( pNtk, Buffer );
2262  Abc_ObjAddFanin( pTermNew, pBox );
2263  Abc_ObjAddFanin( pNetAct, pTermNew );
2264  continue;
2265  }
2266  }
2267  // the bundle is found - add the connections
2268  Vec_PtrForEachEntryReverse( Abc_Obj_t *, pBundle->vNetsActual, pNetAct, k )
2269  {
2270  if ( !strcmp(Abc_ObjName(pNetAct), "1\'b0") || !strcmp(Abc_ObjName(pNetAct), "1\'b1") )
2271  {
2272  sprintf( pMan->sError, "It looks like formal output %s is driving a constant net (%s) when instantiating network %s in box %s.",
2273  pBundle->pNameFormal, Abc_ObjName(pNetAct), pNtkBox->pName, Abc_ObjName(pBox) );
2274  // free the bundling
2275  Vec_PtrForEachEntry( Ver_Bundle_t *, vBundles, pBundle, k )
2276  Ver_ParseFreeBundle( pBundle );
2277  Vec_PtrFree( vBundles );
2278  pBox->pCopy = NULL;
2279  Ver_ParsePrintErrorMessage( pMan );
2280  return 0;
2281  }
2282  pTermNew = Abc_NtkCreateBo( pNtk );
2283  Abc_ObjAddFanin( pTermNew, pBox );
2284  Abc_ObjAddFanin( pNetAct, pTermNew );
2285  i++;
2286  }
2287  i--;
2288  }
2289 
2290  // free the bundling
2291  Vec_PtrForEachEntry( Ver_Bundle_t *, vBundles, pBundle, k )
2292  Ver_ParseFreeBundle( pBundle );
2293  Vec_PtrFree( vBundles );
2294  pBox->pCopy = NULL;
2295  return 1;
2296 }
Abc_ObjId
static unsigned Abc_ObjId(Abc_Obj_t *pObj)
Definition: abc.h:329
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Ver_ObjIsConnected
static int Ver_ObjIsConnected(Abc_Obj_t *pObj)
Definition: verCore.c:78
Vec_PtrForEachEntryReverse
#define Vec_PtrForEachEntryReverse(Type, vVec, pEntry, i)
Definition: vecPtr.h:63
Abc_Ntk_t_
Definition: abc.h:153
Abc_NtkBoxNum
static int Abc_NtkBoxNum(Abc_Ntk_t *pNtk)
Definition: abc.h:289
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Abc_ObjFanin0
static Abc_Obj_t * Abc_ObjFanin0(Abc_Obj_t *pObj)
Definition: abc.h:373
Abc_ObjAddFanin
ABC_DLL void Abc_ObjAddFanin(Abc_Obj_t *pObj, Abc_Obj_t *pFanin)
Definition: abcFanio.c:84
strcmp
int strcmp()
Abc_Obj_t_
Definition: abc.h:128
Abc_NtkCreateBo
static Abc_Obj_t * Abc_NtkCreateBo(Abc_Ntk_t *pNtk)
Definition: abc.h:306
Abc_Obj_t_::pCopy
Abc_Obj_t * pCopy
Definition: abc.h:148
Abc_NtkHasBlackbox
static int Abc_NtkHasBlackbox(Abc_Ntk_t *pNtk)
Definition: abc.h:258
if
if(last==0)
Definition: sparse_int.h:34
sprintf
char * sprintf()
Ver_Bundle_t_
Definition: verCore.c:83
Abc_NtkFindOrCreateNet
ABC_DLL Abc_Obj_t * Abc_NtkFindOrCreateNet(Abc_Ntk_t *pNtk, char *pName)
Definition: abcObj.c:579
Vec_PtrEntry
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
Abc_Obj_t_::pNtk
Abc_Ntk_t * pNtk
Definition: abc.h:130
Abc_NtkPoNum
static int Abc_NtkPoNum(Abc_Ntk_t *pNtk)
Definition: abc.h:286
Abc_NtkPiNum
static int Abc_NtkPiNum(Abc_Ntk_t *pNtk)
Definition: abc.h:285
Abc_ObjName
ABC_DLL char * Abc_ObjName(Abc_Obj_t *pNode)
DECLARATIONS ///.
Definition: abcNames.c:48
Ver_ParsePrintErrorMessage
void Ver_ParsePrintErrorMessage(Ver_Man_t *p)
Definition: verCore.c:278
strncmp
int strncmp()
Ver_ParseFreeBundle
void Ver_ParseFreeBundle(Ver_Bundle_t *pBundle)
Definition: verCore.c:2053
assert
#define assert(ex)
Definition: util_old.h:213
strlen
int strlen()
Abc_Obj_t_::pData
void * pData
Definition: abc.h:145
Abc_NtkForEachPo
#define Abc_NtkForEachPo(pNtk, pPo, i)
Definition: abc.h:517
Abc_NtkCreateBi
static Abc_Obj_t * Abc_NtkCreateBi(Abc_Ntk_t *pNtk)
Definition: abc.h:305
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
Ver_NtkIsDefined
static int Ver_NtkIsDefined(Abc_Ntk_t *pNtkBox)
Definition: verCore.c:77
Abc_ObjFanout0
static Abc_Obj_t * Abc_ObjFanout0(Abc_Obj_t *pObj)
Definition: abc.h:371
Abc_NtkForEachPi
#define Abc_NtkForEachPi(pNtk, pPi, i)
Definition: abc.h:513
Vec_PtrFree
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
int Ver_ParseConnectDefBoxes ( Ver_Man_t *  pMan)

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

Synopsis [Connects the defined boxes.]

Description [Returns 2 if there are any undef boxes.]

SideEffects []

SeeAlso []

Definition at line 2310 of file verCore.c.

2311 {
2312  Abc_Ntk_t * pNtk;
2313  Abc_Obj_t * pBox;
2314  int i, k, RetValue = 1;
2315  // go through all the modules
2316  Vec_PtrForEachEntry( Abc_Ntk_t *, pMan->pDesign->vModules, pNtk, i )
2317  {
2318  // go through all the boxes of this module
2319  Abc_NtkForEachBox( pNtk, pBox, k )
2320  {
2321  if ( Abc_ObjIsLatch(pBox) )
2322  continue;
2323  // skip internal boxes of the blackboxes
2324  if ( pBox->pData == NULL )
2325  continue;
2326  // if the network is undefined, it will be connected later
2327  if ( !Ver_NtkIsDefined((Abc_Ntk_t *)pBox->pData) )
2328  {
2329  RetValue = 2;
2330  continue;
2331  }
2332  // connect the box
2333  if ( !Ver_ParseConnectBox( pMan, pBox ) )
2334  return 0;
2335  // if the network is a true blackbox, skip
2336  if ( Abc_NtkHasBlackbox((Abc_Ntk_t *)pBox->pData) )
2337  continue;
2338  // convert the box to the whitebox
2339  Abc_ObjBlackboxToWhitebox( pBox );
2340  }
2341  }
2342  return RetValue;
2343 }
Abc_ObjIsLatch
static int Abc_ObjIsLatch(Abc_Obj_t *pObj)
Definition: abc.h:356
Abc_Ntk_t_
Definition: abc.h:153
Abc_Obj_t_
Definition: abc.h:128
Ver_ParseConnectBox
static int Ver_ParseConnectBox(Ver_Man_t *pMan, Abc_Obj_t *pBox)
Definition: verCore.c:2071
Abc_NtkHasBlackbox
static int Abc_NtkHasBlackbox(Abc_Ntk_t *pNtk)
Definition: abc.h:258
Abc_ObjBlackboxToWhitebox
static void Abc_ObjBlackboxToWhitebox(Abc_Obj_t *pObj)
Definition: abc.h:361
Abc_NtkForEachBox
#define Abc_NtkForEachBox(pNtk, pObj, i)
Definition: abc.h:495
Abc_Des_t_::vModules
Vec_Ptr_t * vModules
Definition: abc.h:223
Abc_Obj_t_::pData
void * pData
Definition: abc.h:145
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
Abc_Ntk_t_::pDesign
Abc_Des_t * pDesign
Definition: abc.h:180
Ver_NtkIsDefined
static int Ver_NtkIsDefined(Abc_Ntk_t *pNtkBox)
Definition: verCore.c:77
int Ver_ParseConstant ( Ver_Man_t *  pMan,
char *  pWord 
)

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

Synopsis [Returns the values of constant bits.]

Description [The resulting bits are in MSB to LSB order.]

SideEffects []

SeeAlso []

Definition at line 753 of file verCore.c.

754 {
755  int nBits, i;
756  assert( pWord[0] >= '1' && pWord[1] <= '9' );
757  nBits = atoi(pWord);
758  // find the next symbol \'
759  while ( *pWord && *pWord != '\'' )
760  pWord++;
761  if ( *pWord == 0 )
762  {
763  sprintf( pMan->sError, "Cannot find symbol \' in the constant." );
764  Ver_ParsePrintErrorMessage( pMan );
765  return 0;
766  }
767  assert( *pWord == '\'' );
768  pWord++;
769  if ( *pWord != 'b' )
770  {
771  sprintf( pMan->sError, "Currently can only handle binary constants." );
772  Ver_ParsePrintErrorMessage( pMan );
773  return 0;
774  }
775  pWord++;
776  // scan the bits
777  Vec_PtrClear( pMan->vNames );
778  for ( i = 0; i < nBits; i++ )
779  {
780  if ( pWord[i] != '0' && pWord[i] != '1' && pWord[i] != 'x' )
781  {
782  sprintf( pMan->sError, "Having problem parsing the binary constant." );
783  Ver_ParsePrintErrorMessage( pMan );
784  return 0;
785  }
786  if ( pWord[i] == 'x' )
787  Vec_PtrPush( pMan->vNames, (void *)0 );
788  else
789  Vec_PtrPush( pMan->vNames, (void *)(ABC_PTRUINT_T)(pWord[i]-'0') );
790  }
791  return 1;
792 }
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
sprintf
char * sprintf()
Ver_ParsePrintErrorMessage
void Ver_ParsePrintErrorMessage(Ver_Man_t *p)
Definition: verCore.c:278
assert
#define assert(ex)
Definition: util_old.h:213
Vec_PtrClear
static void Vec_PtrClear(Vec_Ptr_t *p)
Definition: vecPtr.h:545
int Ver_ParseConvertNetwork ( Ver_Man_t *  pMan,
Abc_Ntk_t *  pNtk,
int  fMapped 
)

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

Synopsis [Converts the network from the blackbox type into a different one.]

Description []

SideEffects []

SeeAlso []

Definition at line 351 of file verCore.c.

352 {
353  if ( fMapped )
354  {
355  // convert from the blackbox into the network with local functions representated by AIGs
356  if ( pNtk->ntkFunc == ABC_FUNC_BLACKBOX )
357  {
358  // change network type
359  assert( pNtk->pManFunc == NULL );
360  pNtk->ntkFunc = ABC_FUNC_MAP;
361  pNtk->pManFunc = pMan->pDesign->pGenlib;
362  }
363  else if ( pNtk->ntkFunc != ABC_FUNC_MAP )
364  {
365  sprintf( pMan->sError, "The network %s appears to have both gates and assign statements. Currently such network are not allowed. One way to fix this problem might be to replace assigns by buffers from the library.", pNtk->pName );
366  Ver_ParsePrintErrorMessage( pMan );
367  return 0;
368  }
369  }
370  else
371  {
372  // convert from the blackbox into the network with local functions representated by AIGs
373  if ( pNtk->ntkFunc == ABC_FUNC_BLACKBOX )
374  {
375  // change network type
376  assert( pNtk->pManFunc == NULL );
377  pNtk->ntkFunc = ABC_FUNC_AIG;
378  pNtk->pManFunc = pMan->pDesign->pManFunc;
379  }
380  else if ( pNtk->ntkFunc != ABC_FUNC_AIG )
381  {
382  sprintf( pMan->sError, "The network %s appears to have both gates and assign statements. Currently such network are not allowed. One way to fix this problem might be to replace assigns by buffers from the library.", pNtk->pName );
383  Ver_ParsePrintErrorMessage( pMan );
384  return 0;
385  }
386  }
387  return 1;
388 }
Abc_Ntk_t_::pManFunc
void * pManFunc
Definition: abc.h:191
sprintf
char * sprintf()
Abc_Ntk_t_::ntkFunc
Abc_NtkFunc_t ntkFunc
Definition: abc.h:157
Ver_ParsePrintErrorMessage
void Ver_ParsePrintErrorMessage(Ver_Man_t *p)
Definition: verCore.c:278
assert
#define assert(ex)
Definition: util_old.h:213
Abc_Ntk_t_::pName
char * pName
Definition: abc.h:158
Abc_Obj_t * Ver_ParseCreateInv ( Abc_Ntk_t *  pNtk,
Abc_Obj_t *  pNet 
)
static

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

Synopsis [Creates inverter and returns its net.]

Description []

SideEffects []

SeeAlso []

Definition at line 3021 of file verCore.c.

3022 {
3023  Abc_Obj_t * pObj;
3024  pObj = Abc_NtkCreateNodeInv( pNtk, pNet );
3025  pNet = Abc_NtkCreateNet( pNtk );
3026  Abc_ObjAddFanin( pNet, pObj );
3027  return pNet;
3028 }
Abc_ObjAddFanin
ABC_DLL void Abc_ObjAddFanin(Abc_Obj_t *pObj, Abc_Obj_t *pFanin)
Definition: abcFanio.c:84
Abc_Obj_t_
Definition: abc.h:128
Abc_NtkCreateNodeInv
ABC_DLL Abc_Obj_t * Abc_NtkCreateNodeInv(Abc_Ntk_t *pNtk, Abc_Obj_t *pFanin)
Definition: abcObj.c:662
Abc_NtkCreateNet
static Abc_Obj_t * Abc_NtkCreateNet(Abc_Ntk_t *pNtk)
Definition: abc.h:307
Abc_Obj_t * Ver_ParseCreateLatch ( Abc_Ntk_t *  pNtk,
Abc_Obj_t *  pNetLI,
Abc_Obj_t *  pNetLO 
)
static

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

Synopsis [Create a latch with the given input/output.]

Description [By default, the latch value is a don't-care.]

SideEffects []

SeeAlso []

Definition at line 2990 of file verCore.c.

2991 {
2992  Abc_Obj_t * pLatch, * pTerm;
2993  // add the BO terminal
2994  pTerm = Abc_NtkCreateBi( pNtk );
2995  Abc_ObjAddFanin( pTerm, pNetLI );
2996  // add the latch box
2997  pLatch = Abc_NtkCreateLatch( pNtk );
2998  Abc_ObjAddFanin( pLatch, pTerm );
2999  // add the BI terminal
3000  pTerm = Abc_NtkCreateBo( pNtk );
3001  Abc_ObjAddFanin( pTerm, pLatch );
3002  // get the LO net
3003  Abc_ObjAddFanin( pNetLO, pTerm );
3004  // set latch name
3005  Abc_ObjAssignName( pLatch, Abc_ObjName(pNetLO), "L" );
3006  Abc_LatchSetInitDc( pLatch );
3007  return pLatch;
3008 }
Abc_ObjAssignName
ABC_DLL char * Abc_ObjAssignName(Abc_Obj_t *pObj, char *pName, char *pSuffix)
Definition: abcNames.c:68
Abc_LatchSetInitDc
static void Abc_LatchSetInitDc(Abc_Obj_t *pLatch)
Definition: abc.h:420
Abc_ObjAddFanin
ABC_DLL void Abc_ObjAddFanin(Abc_Obj_t *pObj, Abc_Obj_t *pFanin)
Definition: abcFanio.c:84
Abc_Obj_t_
Definition: abc.h:128
Abc_NtkCreateBo
static Abc_Obj_t * Abc_NtkCreateBo(Abc_Ntk_t *pNtk)
Definition: abc.h:306
Abc_NtkCreateLatch
static Abc_Obj_t * Abc_NtkCreateLatch(Abc_Ntk_t *pNtk)
Definition: abc.h:309
Abc_ObjName
ABC_DLL char * Abc_ObjName(Abc_Obj_t *pNode)
DECLARATIONS ///.
Definition: abcNames.c:48
Abc_NtkCreateBi
static Abc_Obj_t * Abc_NtkCreateBi(Abc_Ntk_t *pNtk)
Definition: abc.h:305
Abc_Obj_t * Ver_ParseCreatePi ( Abc_Ntk_t *  pNtk,
char *  pName 
)
static

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

Synopsis [Creates PI terminal and net.]

Description []

SideEffects []

SeeAlso []

Definition at line 2940 of file verCore.c.

2941 {
2942  Abc_Obj_t * pNet, * pTerm;
2943  // get the PI net
2944 // pNet = Ver_ParseFindNet( pNtk, pName );
2945 // if ( pNet )
2946 // printf( "Warning: PI \"%s\" appears twice in the list.\n", pName );
2947  pNet = Abc_NtkFindOrCreateNet( pNtk, pName );
2948  // add the PI node
2949  pTerm = Abc_NtkCreatePi( pNtk );
2950  Abc_ObjAddFanin( pNet, pTerm );
2951  return pTerm;
2952 }
Abc_ObjAddFanin
ABC_DLL void Abc_ObjAddFanin(Abc_Obj_t *pObj, Abc_Obj_t *pFanin)
Definition: abcFanio.c:84
Abc_Obj_t_
Definition: abc.h:128
Abc_NtkCreatePi
static Abc_Obj_t * Abc_NtkCreatePi(Abc_Ntk_t *pNtk)
Definition: abc.h:303
Abc_NtkFindOrCreateNet
ABC_DLL Abc_Obj_t * Abc_NtkFindOrCreateNet(Abc_Ntk_t *pNtk, char *pName)
Definition: abcObj.c:579
Abc_Obj_t * Ver_ParseCreatePo ( Abc_Ntk_t *  pNtk,
char *  pName 
)
static

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

Synopsis [Creates PO terminal and net.]

Description []

SideEffects []

SeeAlso []

Definition at line 2965 of file verCore.c.

2966 {
2967  Abc_Obj_t * pNet, * pTerm;
2968  // get the PO net
2969 // pNet = Ver_ParseFindNet( pNtk, pName );
2970 // if ( pNet && Abc_ObjFaninNum(pNet) == 0 )
2971 // printf( "Warning: PO \"%s\" appears twice in the list.\n", pName );
2972  pNet = Abc_NtkFindOrCreateNet( pNtk, pName );
2973  // add the PO node
2974  pTerm = Abc_NtkCreatePo( pNtk );
2975  Abc_ObjAddFanin( pTerm, pNet );
2976  return pTerm;
2977 }
Abc_ObjAddFanin
ABC_DLL void Abc_ObjAddFanin(Abc_Obj_t *pObj, Abc_Obj_t *pFanin)
Definition: abcFanio.c:84
Abc_Obj_t_
Definition: abc.h:128
Abc_NtkFindOrCreateNet
ABC_DLL Abc_Obj_t * Abc_NtkFindOrCreateNet(Abc_Ntk_t *pNtk, char *pName)
Definition: abcObj.c:579
Abc_NtkCreatePo
static Abc_Obj_t * Abc_NtkCreatePo(Abc_Ntk_t *pNtk)
Definition: abc.h:304
int Ver_ParseDriveFormal ( Ver_Man_t *  pMan,
Abc_Ntk_t *  pNtk,
Ver_Bundle_t *  pBundle0 
)

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

Synopsis [Drives the bundle in the given undef box.]

Description []

SideEffects []

SeeAlso []

Definition at line 2542 of file verCore.c.

2543 {
2544  char Buffer[200];
2545  char * pName;
2546  Ver_Bundle_t * pBundle = NULL;
2547  Abc_Obj_t * pBox, * pTerm, * pTermNew, * pNetAct, * pNetFormal;
2548  int k, j, m;
2549 
2550  // drive this net in the undef box
2551  Vec_PtrForEachEntry( Abc_Obj_t *, pBundle0->vNetsActual, pNetAct, m )
2552  {
2553  // create the formal net
2554  if ( Vec_PtrSize(pBundle0->vNetsActual) == 1 )
2555  sprintf( Buffer, "%s", pBundle0->pNameFormal );
2556  else
2557  sprintf( Buffer, "%s[%d]", pBundle0->pNameFormal, m );
2558  assert( Abc_NtkFindNet( pNtk, Buffer ) == NULL );
2559  pNetFormal = Abc_NtkFindOrCreateNet( pNtk, Buffer );
2560  // connect it to the box
2561  pTerm = Abc_NtkCreateBo( pNtk );
2562  assert( Abc_NtkBoxNum(pNtk) <= 1 );
2563  pBox = Abc_NtkBoxNum(pNtk)? Abc_NtkBox(pNtk,0) : Abc_NtkCreateBlackbox(pNtk);
2564  Abc_ObjAddFanin( Abc_NtkCreatePo(pNtk), pNetFormal );
2565  Abc_ObjAddFanin( pNetFormal, pTerm );
2566  Abc_ObjAddFanin( pTerm, pBox );
2567  }
2568 
2569  // go through instances of this type
2570  pName = Extra_UtilStrsav(pBundle0->pNameFormal);
2571  Vec_PtrForEachEntry( Abc_Obj_t *, (Vec_Ptr_t *)pNtk->pData, pBox, k )
2572  {
2573  // find a bundle with the given name in this instance
2574  Vec_PtrForEachEntryReverse( Ver_Bundle_t *, (Vec_Ptr_t *)pBox->pCopy, pBundle, j )
2575  if ( pBundle && !strcmp( pBundle->pNameFormal, pName ) )
2576  break;
2577  // skip non-driven bundles
2578  if ( j == Vec_PtrSize((Vec_Ptr_t *)pBox->pCopy) )
2579  continue;
2580  // check if any nets are driven in this bundle
2581  assert(pBundle); // Verify pBundle was assigned to.
2582  Vec_PtrForEachEntry( Abc_Obj_t *, pBundle->vNetsActual, pNetAct, m )
2583  if ( Abc_ObjFaninNum(pNetAct) > 0 )
2584  {
2585  sprintf( pMan->sError, "Missing specification of the I/Os of undefined box \"%s\".", Abc_NtkName(pNtk) );
2586  Ver_ParsePrintErrorMessage( pMan );
2587  return 0;
2588  }
2589  // drive the nets by the undef box
2590  Vec_PtrForEachEntryReverse( Abc_Obj_t *, pBundle->vNetsActual, pNetAct, m )
2591  {
2592  pTermNew = Abc_NtkCreateBo( pNetAct->pNtk );
2593  Abc_ObjAddFanin( pTermNew, pBox );
2594  Abc_ObjAddFanin( pNetAct, pTermNew );
2595  }
2596  // remove the bundle
2597  Ver_ParseFreeBundle( pBundle ); pBundle = NULL;
2598  Vec_PtrWriteEntry( (Vec_Ptr_t *)pBox->pCopy, j, NULL );
2599  }
2600  ABC_FREE( pName );
2601  return 1;
2602 }
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Vec_PtrForEachEntryReverse
#define Vec_PtrForEachEntryReverse(Type, vVec, pEntry, i)
Definition: vecPtr.h:63
Abc_NtkBoxNum
static int Abc_NtkBoxNum(Abc_Ntk_t *pNtk)
Definition: abc.h:289
Abc_ObjFaninNum
static int Abc_ObjFaninNum(Abc_Obj_t *pObj)
Definition: abc.h:364
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Extra_UtilStrsav
char * Extra_UtilStrsav(const char *s)
Definition: extraUtilUtil.c:169
Abc_ObjAddFanin
ABC_DLL void Abc_ObjAddFanin(Abc_Obj_t *pObj, Abc_Obj_t *pFanin)
Definition: abcFanio.c:84
strcmp
int strcmp()
Abc_Ntk_t_::pData
void * pData
Definition: abc.h:203
Abc_Obj_t_
Definition: abc.h:128
Abc_NtkCreateBo
static Abc_Obj_t * Abc_NtkCreateBo(Abc_Ntk_t *pNtk)
Definition: abc.h:306
Abc_Obj_t_::pCopy
Abc_Obj_t * pCopy
Definition: abc.h:148
Abc_NtkFindNet
ABC_DLL Abc_Obj_t * Abc_NtkFindNet(Abc_Ntk_t *pNtk, char *pName)
Definition: abcObj.c:507
if
if(last==0)
Definition: sparse_int.h:34
Ver_Bundle_t_::pNameFormal
char * pNameFormal
Definition: verCore.c:85
sprintf
char * sprintf()
Abc_NtkCreateBlackbox
static Abc_Obj_t * Abc_NtkCreateBlackbox(Abc_Ntk_t *pNtk)
Definition: abc.h:311
Ver_Bundle_t_::vNetsActual
Vec_Ptr_t * vNetsActual
Definition: verCore.c:86
Ver_Bundle_t_
Definition: verCore.c:83
Abc_NtkFindOrCreateNet
ABC_DLL Abc_Obj_t * Abc_NtkFindOrCreateNet(Abc_Ntk_t *pNtk, char *pName)
Definition: abcObj.c:579
Vec_PtrWriteEntry
static void Vec_PtrWriteEntry(Vec_Ptr_t *p, int i, void *Entry)
Definition: vecPtr.h:396
Abc_NtkBox
static Abc_Obj_t * Abc_NtkBox(Abc_Ntk_t *pNtk, int i)
Definition: abc.h:319
Abc_NtkName
static char * Abc_NtkName(Abc_Ntk_t *pNtk)
Definition: abc.h:270
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Ver_ParsePrintErrorMessage
void Ver_ParsePrintErrorMessage(Ver_Man_t *p)
Definition: verCore.c:278
Ver_ParseFreeBundle
void Ver_ParseFreeBundle(Ver_Bundle_t *pBundle)
Definition: verCore.c:2053
assert
#define assert(ex)
Definition: util_old.h:213
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
Abc_NtkCreatePo
static Abc_Obj_t * Abc_NtkCreatePo(Abc_Ntk_t *pNtk)
Definition: abc.h:304
int Ver_ParseDriveInputs ( Ver_Man_t *  pMan,
Vec_Ptr_t *  vUndefs 
)

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

Synopsis [Drives the bundle in the given undef box.]

Description []

SideEffects []

SeeAlso []

Definition at line 2616 of file verCore.c.

2617 {
2618  char Buffer[200];
2619  Ver_Bundle_t * pBundle;
2620  Abc_Ntk_t * pNtk;
2621  Abc_Obj_t * pBox, * pBox2, * pTerm, * pTermNew, * pNetFormal, * pNetAct;
2622  int i, k, j, m, CountCur, CountTotal = -1;
2623  // iterate through the undef boxes
2624  Vec_PtrForEachEntry( Abc_Ntk_t *, vUndefs, pNtk, i )
2625  {
2626  // count the number of unconnected bundles for instances of this type of box
2627  CountTotal = -1;
2628  Vec_PtrForEachEntry( Abc_Obj_t *, (Vec_Ptr_t *)pNtk->pData, pBox, k )
2629  {
2630  CountCur = 0;
2631  Vec_PtrForEachEntry( Ver_Bundle_t *, (Vec_Ptr_t *)pBox->pCopy, pBundle, j )
2632  CountCur += (pBundle != NULL);
2633  if ( CountTotal == -1 )
2634  CountTotal = CountCur;
2635  else if ( CountTotal != CountCur )
2636  {
2637  sprintf( pMan->sError, "The number of formal inputs (%d) is different from the expected one (%d) when instantiating network %s in box %s.",
2638  CountCur, CountTotal, pNtk->pName, Abc_ObjName(pBox) );
2639  Ver_ParsePrintErrorMessage( pMan );
2640  return 0;
2641  }
2642  }
2643 
2644  // create formals
2645  pBox = (Abc_Obj_t *)Vec_PtrEntry( (Vec_Ptr_t *)pNtk->pData, 0 );
2646  Vec_PtrForEachEntry( Ver_Bundle_t *, (Vec_Ptr_t *)pBox->pCopy, pBundle, j )
2647  {
2648  if ( pBundle == NULL )
2649  continue;
2650  Vec_PtrForEachEntry( Abc_Obj_t *, pBundle->vNetsActual, pNetAct, m )
2651  {
2652  // find create the formal net
2653  if ( Vec_PtrSize(pBundle->vNetsActual) == 1 )
2654  sprintf( Buffer, "%s", pBundle->pNameFormal );
2655  else
2656  sprintf( Buffer, "%s[%d]", pBundle->pNameFormal, m );
2657  assert( Abc_NtkFindNet( pNtk, Buffer ) == NULL );
2658  pNetFormal = Abc_NtkFindOrCreateNet( pNtk, Buffer );
2659  // connect
2660  pTerm = Abc_NtkCreateBi( pNtk );
2661  assert( Abc_NtkBoxNum(pNtk) <= 1 );
2662  pBox2 = Abc_NtkBoxNum(pNtk)? Abc_NtkBox(pNtk,0) : Abc_NtkCreateBlackbox(pNtk);
2663  Abc_ObjAddFanin( pNetFormal, Abc_NtkCreatePi(pNtk) );
2664  Abc_ObjAddFanin( pTerm, pNetFormal );
2665  Abc_ObjAddFanin( pBox2, pTerm );
2666  }
2667  }
2668 
2669  // go through all the boxes
2670  Vec_PtrForEachEntry( Abc_Obj_t *, (Vec_Ptr_t *)pNtk->pData, pBox, k )
2671  {
2672  // go through all the bundles
2673  Vec_PtrForEachEntry( Ver_Bundle_t *, (Vec_Ptr_t *)pBox->pCopy, pBundle, j )
2674  {
2675  if ( pBundle == NULL )
2676  continue;
2677  // drive the nets by the undef box
2678  Vec_PtrForEachEntryReverse( Abc_Obj_t *, pBundle->vNetsActual, pNetAct, m )
2679  {
2680  pTermNew = Abc_NtkCreateBi( pNetAct->pNtk );
2681  Abc_ObjAddFanin( pBox, pTermNew );
2682  Abc_ObjAddFanin( pTermNew, pNetAct );
2683  }
2684  // remove the bundle
2685  Ver_ParseFreeBundle( pBundle );
2686  Vec_PtrWriteEntry( (Vec_Ptr_t *)pBox->pCopy, j, NULL );
2687  }
2688 
2689  // free the bundles
2690  Vec_PtrFree( (Vec_Ptr_t *)pBox->pCopy );
2691  pBox->pCopy = NULL;
2692  }
2693  }
2694  return 1;
2695 }
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Vec_PtrForEachEntryReverse
#define Vec_PtrForEachEntryReverse(Type, vVec, pEntry, i)
Definition: vecPtr.h:63
Abc_Ntk_t_
Definition: abc.h:153
Abc_NtkBoxNum
static int Abc_NtkBoxNum(Abc_Ntk_t *pNtk)
Definition: abc.h:289
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Abc_ObjAddFanin
ABC_DLL void Abc_ObjAddFanin(Abc_Obj_t *pObj, Abc_Obj_t *pFanin)
Definition: abcFanio.c:84
Abc_Ntk_t_::pData
void * pData
Definition: abc.h:203
Abc_Obj_t_
Definition: abc.h:128
Abc_Obj_t_::pCopy
Abc_Obj_t * pCopy
Definition: abc.h:148
Abc_NtkFindNet
ABC_DLL Abc_Obj_t * Abc_NtkFindNet(Abc_Ntk_t *pNtk, char *pName)
Definition: abcObj.c:507
if
if(last==0)
Definition: sparse_int.h:34
else
else
Definition: sparse_int.h:55
Ver_Bundle_t_::pNameFormal
char * pNameFormal
Definition: verCore.c:85
sprintf
char * sprintf()
Abc_NtkCreateBlackbox
static Abc_Obj_t * Abc_NtkCreateBlackbox(Abc_Ntk_t *pNtk)
Definition: abc.h:311
Ver_Bundle_t_::vNetsActual
Vec_Ptr_t * vNetsActual
Definition: verCore.c:86
Abc_NtkCreatePi
static Abc_Obj_t * Abc_NtkCreatePi(Abc_Ntk_t *pNtk)
Definition: abc.h:303
Ver_Bundle_t_
Definition: verCore.c:83
Abc_NtkFindOrCreateNet
ABC_DLL Abc_Obj_t * Abc_NtkFindOrCreateNet(Abc_Ntk_t *pNtk, char *pName)
Definition: abcObj.c:579
Vec_PtrWriteEntry
static void Vec_PtrWriteEntry(Vec_Ptr_t *p, int i, void *Entry)
Definition: vecPtr.h:396
Abc_NtkBox
static Abc_Obj_t * Abc_NtkBox(Abc_Ntk_t *pNtk, int i)
Definition: abc.h:319
Vec_PtrEntry
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
Abc_Obj_t_::pNtk
Abc_Ntk_t * pNtk
Definition: abc.h:130
Abc_ObjName
ABC_DLL char * Abc_ObjName(Abc_Obj_t *pNode)
DECLARATIONS ///.
Definition: abcNames.c:48
Ver_ParsePrintErrorMessage
void Ver_ParsePrintErrorMessage(Ver_Man_t *p)
Definition: verCore.c:278
Ver_ParseFreeBundle
void Ver_ParseFreeBundle(Ver_Bundle_t *pBundle)
Definition: verCore.c:2053
assert
#define assert(ex)
Definition: util_old.h:213
Abc_NtkCreateBi
static Abc_Obj_t * Abc_NtkCreateBi(Abc_Ntk_t *pNtk)
Definition: abc.h:305
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
Abc_Ntk_t_::pName
char * pName
Definition: abc.h:158
Vec_PtrFree
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
Abc_Des_t* Ver_ParseFile ( char *  pFileName,
Abc_Des_t *  pGateLib,
int  fCheck,
int  fUseMemMan 
)

MACRO DEFINITIONS ///.

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

Synopsis [File parser.]

Description []

SideEffects []

SeeAlso []

Definition at line 165 of file verCore.c.

166 {
167  Ver_Man_t * p;
168  Abc_Des_t * pDesign;
169  // start the parser
170  p = Ver_ParseStart( pFileName, pGateLib );
171  p->fMapped = glo_fMapped;
172  p->fCheck = fCheck;
173  p->fUseMemMan = fUseMemMan;
174  if ( glo_fMapped )
175  {
176  Hop_ManStop((Hop_Man_t *)p->pDesign->pManFunc);
177  p->pDesign->pManFunc = NULL;
178  }
179  // parse the file
180  Ver_ParseInternal( p );
181  // save the result
182  pDesign = p->pDesign;
183  p->pDesign = NULL;
184  // stop the parser
185  Ver_ParseStop( p );
186  return pDesign;
187 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
glo_fMapped
int glo_fMapped
Definition: verCore.c:80
Ver_ParseInternal
static void Ver_ParseInternal(Ver_Man_t *p)
Definition: verCore.c:200
Ver_ParseStop
static void Ver_ParseStop(Ver_Man_t *p)
Definition: verCore.c:142
Hop_ManStop
void Hop_ManStop(Hop_Man_t *p)
Definition: hopMan.c:84
Ver_Man_t
typedefABC_NAMESPACE_HEADER_START struct Ver_Man_t_ Ver_Man_t
INCLUDES ///.
Definition: ver.h:45
Ver_ParseStart
static Ver_Man_t * Ver_ParseStart(char *pFileName, Abc_Des_t *pGateLib)
FUNCTION DEFINITIONS ///.
Definition: verCore.c:104
Hop_Man_t
typedefABC_NAMESPACE_HEADER_START struct Hop_Man_t_ Hop_Man_t
INCLUDES ///.
Definition: hop.h:49
Abc_Des_t_
Definition: abc.h:218
Abc_Obj_t* Ver_ParseFindNet ( Abc_Ntk_t *  pNtk,
char *  pName 
)

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

Synopsis [Finds the network by name or create a new blackbox network.]

Description []

SideEffects []

SeeAlso []

Definition at line 328 of file verCore.c.

329 {
330  Abc_Obj_t * pObj;
331  if ( (pObj = Abc_NtkFindNet(pNtk, pName)) )
332  return pObj;
333  if ( !strcmp( pName, "1\'b0" ) || !strcmp( pName, "1\'bx" ) )
334  return Abc_NtkFindOrCreateNet( pNtk, "1\'b0" );
335  if ( !strcmp( pName, "1\'b1" ) )
336  return Abc_NtkFindOrCreateNet( pNtk, "1\'b1" );
337  return NULL;
338 }
strcmp
int strcmp()
Abc_Obj_t_
Definition: abc.h:128
Abc_NtkFindNet
ABC_DLL Abc_Obj_t * Abc_NtkFindNet(Abc_Ntk_t *pNtk, char *pName)
Definition: abcObj.c:507
Abc_NtkFindOrCreateNet
ABC_DLL Abc_Obj_t * Abc_NtkFindOrCreateNet(Abc_Ntk_t *pNtk, char *pName)
Definition: abcObj.c:579
Abc_Ntk_t* Ver_ParseFindOrCreateNetwork ( Ver_Man_t *  pMan,
char *  pName 
)

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

Synopsis [Finds the network by name or create a new blackbox network.]

Description []

SideEffects []

SeeAlso []

Definition at line 301 of file verCore.c.

302 {
303  Abc_Ntk_t * pNtkNew;
304  // check if the network exists
305  if ( (pNtkNew = Abc_DesFindModelByName( pMan->pDesign, pName )) )
306  return pNtkNew;
307 //printf( "Creating network %s.\n", pName );
308  // create new network
309  pNtkNew = Abc_NtkAlloc( ABC_NTK_NETLIST, ABC_FUNC_BLACKBOX, pMan->fUseMemMan );
310  pNtkNew->pName = Extra_UtilStrsav( pName );
311  pNtkNew->pSpec = NULL;
312  // add module to the design
313  Abc_DesAddModel( pMan->pDesign, pNtkNew );
314  return pNtkNew;
315 }
Abc_Ntk_t_
Definition: abc.h:153
Abc_DesAddModel
ABC_DLL int Abc_DesAddModel(Abc_Des_t *p, Abc_Ntk_t *pNtk)
Definition: abcLib.c:226
Extra_UtilStrsav
char * Extra_UtilStrsav(const char *s)
Definition: extraUtilUtil.c:169
Abc_NtkAlloc
ABC_DLL Abc_Ntk_t * Abc_NtkAlloc(Abc_NtkType_t Type, Abc_NtkFunc_t Func, int fUseMemMan)
DECLARATIONS ///.
Definition: abcNtk.c:50
Abc_Ntk_t_::pSpec
char * pSpec
Definition: abc.h:159
Abc_DesFindModelByName
ABC_DLL Abc_Ntk_t * Abc_DesFindModelByName(Abc_Des_t *p, char *pName)
Definition: abcLib.c:249
Abc_Ntk_t_::pName
char * pName
Definition: abc.h:158
int Ver_ParseFlopStandard ( Ver_Man_t *  pMan,
Abc_Ntk_t *  pNtk 
)
static

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

Synopsis [Parses one directive.]

Description []

SideEffects []

SeeAlso []

Definition at line 1426 of file verCore.c.

1427 {
1428  Ver_Stream_t * p = pMan->pReader;
1429  Abc_Obj_t * pNetLi, * pNetLo, * pLatch;
1430  char * pWord, Symbol;
1431 
1432  // convert from the blackbox into the network with local functions representated by AIGs
1433  if ( !Ver_ParseConvertNetwork( pMan, pNtk, pMan->fMapped ) )
1434  return 0;
1435 
1436  // this is gate name - throw it away
1437  if ( Ver_StreamPopChar(p) != '(' )
1438  {
1439  sprintf( pMan->sError, "Cannot parse a standard gate (expected opening paranthesis)." );
1440  Ver_ParsePrintErrorMessage( pMan );
1441  return 0;
1442  }
1443  Ver_ParseSkipComments( pMan );
1444 
1445  // parse the output name
1446  pWord = Ver_ParseGetName( pMan );
1447  if ( pWord == NULL )
1448  return 0;
1449  // get the net corresponding to this output
1450  pNetLo = Ver_ParseFindNet( pNtk, pWord );
1451  if ( pNetLo == NULL )
1452  {
1453  sprintf( pMan->sError, "Net is missing in gate %s.", pWord );
1454  Ver_ParsePrintErrorMessage( pMan );
1455  return 0;
1456  }
1457 
1458  // check if it is the end of gate
1459  Ver_ParseSkipComments( pMan );
1460  Symbol = Ver_StreamPopChar(p);
1461  if ( Symbol == ')' )
1462  {
1463  sprintf( pMan->sError, "Cannot parse the flop." );
1464  Ver_ParsePrintErrorMessage( pMan );
1465  return 0;
1466  }
1467  // skip comma
1468  if ( Symbol != ',' )
1469  {
1470  sprintf( pMan->sError, "Cannot parse the flop." );
1471  Ver_ParsePrintErrorMessage( pMan );
1472  return 0;
1473  }
1474  Ver_ParseSkipComments( pMan );
1475 
1476  // parse the output name
1477  pWord = Ver_ParseGetName( pMan );
1478  if ( pWord == NULL )
1479  return 0;
1480  // get the net corresponding to this output
1481  pNetLi = Ver_ParseFindNet( pNtk, pWord );
1482  if ( pNetLi == NULL )
1483  {
1484  sprintf( pMan->sError, "Net is missing in gate %s.", pWord );
1485  Ver_ParsePrintErrorMessage( pMan );
1486  return 0;
1487  }
1488 
1489  // check if it is the end of gate
1490  Ver_ParseSkipComments( pMan );
1491  Symbol = Ver_StreamPopChar(p);
1492  if ( Symbol != ')' )
1493  {
1494  sprintf( pMan->sError, "Cannot parse the flop." );
1495  Ver_ParsePrintErrorMessage( pMan );
1496  return 0;
1497  }
1498 
1499  // check if it is the end of gate
1500  Ver_ParseSkipComments( pMan );
1501  if ( Ver_StreamPopChar(p) != ';' )
1502  {
1503  sprintf( pMan->sError, "Cannot parse the flop." );
1504  Ver_ParsePrintErrorMessage( pMan );
1505  return 0;
1506  }
1507 
1508  // create the latch
1509  pLatch = Ver_ParseCreateLatch( pNtk, pNetLi, pNetLo );
1510  Abc_LatchSetInit0( pLatch );
1511  return 1;
1512 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Ver_StreamPopChar
char Ver_StreamPopChar(Ver_Stream_t *p)
Definition: verStream.c:275
Ver_ParseConvertNetwork
int Ver_ParseConvertNetwork(Ver_Man_t *pMan, Abc_Ntk_t *pNtk, int fMapped)
Definition: verCore.c:351
Ver_ParseSkipComments
int Ver_ParseSkipComments(Ver_Man_t *p)
DECLARATIONS ///.
Definition: verParse.c:45
Ver_Stream_t_
Definition: verStream.c:36
Abc_Obj_t_
Definition: abc.h:128
Ver_ParseCreateLatch
static Abc_Obj_t * Ver_ParseCreateLatch(Abc_Ntk_t *pNtk, Abc_Obj_t *pNetLI, Abc_Obj_t *pNetLO)
Definition: verCore.c:2990
Ver_ParseGetName
char * Ver_ParseGetName(Ver_Man_t *p)
Definition: verParse.c:91
sprintf
char * sprintf()
Ver_ParsePrintErrorMessage
void Ver_ParsePrintErrorMessage(Ver_Man_t *p)
Definition: verCore.c:278
Abc_LatchSetInit0
static void Abc_LatchSetInit0(Abc_Obj_t *pLatch)
Definition: abc.h:418
Ver_ParseFindNet
Abc_Obj_t * Ver_ParseFindNet(Abc_Ntk_t *pNtk, char *pName)
Definition: verCore.c:328
int Ver_ParseFormalNetsAreDriven ( Abc_Ntk_t *  pNtk,
char *  pNameFormal 
)

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

Synopsis [Checks if formal nets with the given name are driven in any of the instances of undef boxes.]

Description []

SideEffects []

SeeAlso []

Definition at line 2474 of file verCore.c.

2475 {
2476  Ver_Bundle_t * pBundle = NULL;
2477  Abc_Obj_t * pBox, * pNet;
2478  int k, j, m;
2479  // go through instances of this type
2480  Vec_PtrForEachEntry( Abc_Obj_t *, (Vec_Ptr_t *)pNtk->pData, pBox, k )
2481  {
2482  // find a bundle with the given name in this instance
2483  Vec_PtrForEachEntryReverse( Ver_Bundle_t *, (Vec_Ptr_t *)pBox->pCopy, pBundle, j )
2484  if ( pBundle && !strcmp( pBundle->pNameFormal, pNameFormal ) )
2485  break;
2486  // skip non-driven bundles
2487  if ( j == Vec_PtrSize((Vec_Ptr_t *)pBox->pCopy) )
2488  continue;
2489  // check if all nets are driven in this bundle
2490  assert(pBundle); // Verify that pBundle was assigned to.
2491  Vec_PtrForEachEntry( Abc_Obj_t *, pBundle->vNetsActual, pNet, m )
2492  if ( Abc_ObjFaninNum(pNet) > 0 )
2493  return 1;
2494  }
2495  return 0;
2496 }
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Vec_PtrForEachEntryReverse
#define Vec_PtrForEachEntryReverse(Type, vVec, pEntry, i)
Definition: vecPtr.h:63
Abc_ObjFaninNum
static int Abc_ObjFaninNum(Abc_Obj_t *pObj)
Definition: abc.h:364
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
strcmp
int strcmp()
Abc_Ntk_t_::pData
void * pData
Definition: abc.h:203
Abc_Obj_t_
Definition: abc.h:128
Abc_Obj_t_::pCopy
Abc_Obj_t * pCopy
Definition: abc.h:148
if
if(last==0)
Definition: sparse_int.h:34
Ver_Bundle_t_
Definition: verCore.c:83
assert
#define assert(ex)
Definition: util_old.h:213
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
void Ver_ParseFreeBundle ( Ver_Bundle_t *  pBundle)

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

Synopsis [Connects one box to the network]

Description []

SideEffects []

SeeAlso []

Definition at line 2053 of file verCore.c.

2054 {
2055  ABC_FREE( pBundle->pNameFormal );
2056  Vec_PtrFree( pBundle->vNetsActual );
2057  ABC_FREE( pBundle );
2058 }
Ver_Bundle_t_::pNameFormal
char * pNameFormal
Definition: verCore.c:85
Ver_Bundle_t_::vNetsActual
Vec_Ptr_t * vNetsActual
Definition: verCore.c:86
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Vec_PtrFree
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
void Ver_ParseFreeData ( Ver_Man_t *  p)
static

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

Synopsis [File parser.]

Description []

SideEffects []

SeeAlso []

Definition at line 258 of file verCore.c.

259 {
260  if ( p->pDesign )
261  {
262  Abc_DesFree( p->pDesign, NULL );
263  p->pDesign = NULL;
264  }
265 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Abc_DesFree
ABC_DLL void Abc_DesFree(Abc_Des_t *p, Abc_Ntk_t *pNtk)
Definition: abcLib.c:94
int Ver_ParseGate ( Ver_Man_t *  pMan,
Abc_Ntk_t *  pNtk,
Mio_Gate_t *  pGate 
)
static

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

Synopsis [Parses one directive.]

Description []

SideEffects []

SeeAlso []

Definition at line 1550 of file verCore.c.

1551 {
1552  Ver_Stream_t * p = pMan->pReader;
1553  Abc_Obj_t * pNetActual, * pNode, * pNode2 = NULL;
1554  char * pWord, Symbol;
1555  int Input, i, nFanins = Mio_GateReadPinNum(pGate);
1556 
1557  // convert from the blackbox into the network with local functions representated by gates
1558  if ( 1 != pMan->fMapped )
1559  {
1560  sprintf( pMan->sError, "The network appears to be mapped. Use \"r -m\" to read mapped Verilog." );
1561  Ver_ParsePrintErrorMessage( pMan );
1562  return 0;
1563  }
1564 
1565  // update the network type if needed
1566  if ( !Ver_ParseConvertNetwork( pMan, pNtk, 1 ) )
1567  return 0;
1568 
1569  // parse the directive and set the pointers to the PIs/POs of the gate
1570  pWord = Ver_ParseGetName( pMan );
1571  if ( pWord == NULL )
1572  return 0;
1573  // this is gate name - throw it away
1574  if ( Ver_StreamPopChar(p) != '(' )
1575  {
1576  sprintf( pMan->sError, "Cannot parse gate %s (expected opening paranthesis).", Mio_GateReadName(pGate) );
1577  Ver_ParsePrintErrorMessage( pMan );
1578  return 0;
1579  }
1580  Ver_ParseSkipComments( pMan );
1581 
1582  // start the node
1583  pNode = Abc_NtkCreateNode( pNtk );
1584  pNode->pData = pGate;
1585  if ( Mio_GateReadTwin(pGate) )
1586  {
1587  pNode2 = Abc_NtkCreateNode( pNtk );
1588  pNode2->pData = Mio_GateReadTwin(pGate);
1589  }
1590  // parse pairs of formal/actural inputs
1591  Vec_IntClear( pMan->vPerm );
1592  while ( 1 )
1593  {
1594  // process one pair of formal/actual parameters
1595  if ( Ver_StreamPopChar(p) != '.' )
1596  {
1597  sprintf( pMan->sError, "Cannot parse gate %s (expected .).", Mio_GateReadName(pGate) );
1598  Ver_ParsePrintErrorMessage( pMan );
1599  return 0;
1600  }
1601 
1602  // parse the formal name
1603  pWord = Ver_ParseGetName( pMan );
1604  if ( pWord == NULL )
1605  return 0;
1606 
1607  // find the corresponding pin of the gate
1608  Input = Ver_FindGateInput( pGate, pWord );
1609  if ( Input == -1 )
1610  {
1611  sprintf( pMan->sError, "Formal input name %s cannot be found in the gate %s.", pWord, Mio_GateReadOutName(pGate) );
1612  Ver_ParsePrintErrorMessage( pMan );
1613  return 0;
1614  }
1615 
1616  // open the paranthesis
1617  if ( Ver_StreamPopChar(p) != '(' )
1618  {
1619  sprintf( pMan->sError, "Cannot formal parameter %s of gate %s (expected opening paranthesis).", pWord, Mio_GateReadName(pGate) );
1620  Ver_ParsePrintErrorMessage( pMan );
1621  return 0;
1622  }
1623 
1624  // parse the actual name
1625  pWord = Ver_ParseGetName( pMan );
1626  if ( pWord == NULL )
1627  return 0;
1628  // check if the name is complemented
1629  assert( pWord[0] != '~' );
1630 /*
1631  fCompl = (pWord[0] == '~');
1632  if ( fCompl )
1633  {
1634  fComplUsed = 1;
1635  pWord++;
1636  if ( pNtk->pData == NULL )
1637  pNtk->pData = Extra_MmFlexStart();
1638  }
1639 */
1640  // get the actual net
1641  pNetActual = Ver_ParseFindNet( pNtk, pWord );
1642  if ( pNetActual == NULL )
1643  {
1644  sprintf( pMan->sError, "Actual net %s is missing.", pWord );
1645  Ver_ParsePrintErrorMessage( pMan );
1646  return 0;
1647  }
1648 
1649  // close the paranthesis
1650  if ( Ver_StreamPopChar(p) != ')' )
1651  {
1652  sprintf( pMan->sError, "Cannot formal parameter %s of gate %s (expected closing paranthesis).", pWord, Mio_GateReadName(pGate) );
1653  Ver_ParsePrintErrorMessage( pMan );
1654  return 0;
1655  }
1656 
1657  // add the fanin
1658  if ( Input < nFanins )
1659  {
1660  Vec_IntPush( pMan->vPerm, Input );
1661  Abc_ObjAddFanin( pNode, pNetActual ); // fanin
1662  if ( pNode2 )
1663  Abc_ObjAddFanin( pNode2, pNetActual ); // fanin
1664  }
1665  else if ( Input == nFanins )
1666  Abc_ObjAddFanin( pNetActual, pNode ); // fanout
1667  else if ( Input == nFanins + 1 )
1668  Abc_ObjAddFanin( pNetActual, pNode2 ); // fanout
1669  else
1670  assert( 0 );
1671 
1672  // check if it is the end of gate
1673  Ver_ParseSkipComments( pMan );
1674  Symbol = Ver_StreamPopChar(p);
1675  if ( Symbol == ')' )
1676  break;
1677 
1678  // skip comma
1679  if ( Symbol != ',' )
1680  {
1681  sprintf( pMan->sError, "Cannot formal parameter %s of gate %s (expected closing paranthesis).", pWord, Mio_GateReadName(pGate) );
1682  Ver_ParsePrintErrorMessage( pMan );
1683  return 0;
1684  }
1685  Ver_ParseSkipComments( pMan );
1686  }
1687 
1688  // check that the gate as the same number of input
1689  if ( !(Abc_ObjFaninNum(pNode) == nFanins && Abc_ObjFanoutNum(pNode) == 1) )
1690  {
1691  sprintf( pMan->sError, "Parsing of gate %s has failed.", Mio_GateReadName(pGate) );
1692  Ver_ParsePrintErrorMessage( pMan );
1693  return 0;
1694  }
1695 
1696  // check if it is the end of gate
1697  Ver_ParseSkipComments( pMan );
1698  if ( Ver_StreamPopChar(p) != ';' )
1699  {
1700  sprintf( pMan->sError, "Cannot read gate %s (expected closing semicolumn).", Mio_GateReadName(pGate) );
1701  Ver_ParsePrintErrorMessage( pMan );
1702  return 0;
1703  }
1704 
1705  // check if we need to permute the inputs
1706  Vec_IntForEachEntry( pMan->vPerm, Input, i )
1707  if ( Input != i )
1708  break;
1709  if ( i < Vec_IntSize(pMan->vPerm) )
1710  {
1711  // add the fanin numnbers to the end of the permuation array
1712  for ( i = 0; i < nFanins; i++ )
1713  Vec_IntPush( pMan->vPerm, Abc_ObjFaninId(pNode, i) );
1714  // write the fanin numbers into their corresponding places (according to the gate)
1715  for ( i = 0; i < nFanins; i++ )
1716  Vec_IntWriteEntry( &pNode->vFanins, Vec_IntEntry(pMan->vPerm, i), Vec_IntEntry(pMan->vPerm, i+nFanins) );
1717  }
1718  return 1;
1719 }
Ver_FindGateInput
int Ver_FindGateInput(Mio_Gate_t *pGate, char *pName)
Definition: verCore.c:1525
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Abc_ObjFanoutNum
static int Abc_ObjFanoutNum(Abc_Obj_t *pObj)
Definition: abc.h:365
Abc_ObjFaninNum
static int Abc_ObjFaninNum(Abc_Obj_t *pObj)
Definition: abc.h:364
Ver_StreamPopChar
char Ver_StreamPopChar(Ver_Stream_t *p)
Definition: verStream.c:275
Mio_GateReadOutName
char * Mio_GateReadOutName(Mio_Gate_t *pGate)
Definition: mioApi.c:144
Abc_Obj_t_::vFanins
Vec_Int_t vFanins
Definition: abc.h:143
Ver_ParseConvertNetwork
int Ver_ParseConvertNetwork(Ver_Man_t *pMan, Abc_Ntk_t *pNtk, int fMapped)
Definition: verCore.c:351
Ver_ParseSkipComments
int Ver_ParseSkipComments(Ver_Man_t *p)
DECLARATIONS ///.
Definition: verParse.c:45
Abc_ObjAddFanin
ABC_DLL void Abc_ObjAddFanin(Abc_Obj_t *pObj, Abc_Obj_t *pFanin)
Definition: abcFanio.c:84
Ver_Stream_t_
Definition: verStream.c:36
Abc_Obj_t_
Definition: abc.h:128
Mio_GateReadPinNum
int Mio_GateReadPinNum(Mio_Gate_t *pGate)
Definition: mioApi.c:151
Vec_IntWriteEntry
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
if
if(last==0)
Definition: sparse_int.h:34
Ver_ParseGetName
char * Ver_ParseGetName(Ver_Man_t *p)
Definition: verParse.c:91
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
sprintf
char * sprintf()
Mio_GateReadTwin
Mio_Gate_t * Mio_GateReadTwin(Mio_Gate_t *pGate)
Definition: mioApi.c:150
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Abc_NtkCreateNode
static Abc_Obj_t * Abc_NtkCreateNode(Abc_Ntk_t *pNtk)
Definition: abc.h:308
Ver_ParsePrintErrorMessage
void Ver_ParsePrintErrorMessage(Ver_Man_t *p)
Definition: verCore.c:278
assert
#define assert(ex)
Definition: util_old.h:213
Abc_ObjFaninId
static int Abc_ObjFaninId(Abc_Obj_t *pObj, int i)
Definition: abc.h:366
Abc_Obj_t_::pData
void * pData
Definition: abc.h:145
Vec_IntClear
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Mio_GateReadName
char * Mio_GateReadName(Mio_Gate_t *pGate)
Definition: mioApi.c:143
Ver_ParseFindNet
Abc_Obj_t * Ver_ParseFindNet(Abc_Ntk_t *pNtk, char *pName)
Definition: verCore.c:328
int Ver_ParseGateStandard ( Ver_Man_t *  pMan,
Abc_Ntk_t *  pNtk,
Ver_GateType_t  GateType 
)
static

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

Synopsis [Parses one directive.]

Description []

SideEffects []

SeeAlso []

Definition at line 1330 of file verCore.c.

1331 {
1332  Ver_Stream_t * p = pMan->pReader;
1333  Abc_Obj_t * pNet, * pNode;
1334  char * pWord, Symbol;
1335 
1336  // convert from the blackbox into the network with local functions representated by AIGs
1337  if ( !Ver_ParseConvertNetwork( pMan, pNtk, pMan->fMapped ) )
1338  return 0;
1339 
1340  // this is gate name - throw it away
1341  if ( Ver_StreamPopChar(p) != '(' )
1342  {
1343  sprintf( pMan->sError, "Cannot parse a standard gate (expected opening paranthesis)." );
1344  Ver_ParsePrintErrorMessage( pMan );
1345  return 0;
1346  }
1347  Ver_ParseSkipComments( pMan );
1348 
1349  // create the node
1350  pNode = Abc_NtkCreateNode( pNtk );
1351 
1352  // parse pairs of formal/actural inputs
1353  while ( 1 )
1354  {
1355  // parse the output name
1356  pWord = Ver_ParseGetName( pMan );
1357  if ( pWord == NULL )
1358  return 0;
1359  // get the net corresponding to this output
1360  pNet = Ver_ParseFindNet( pNtk, pWord );
1361  if ( pNet == NULL )
1362  {
1363  sprintf( pMan->sError, "Net is missing in gate %s.", pWord );
1364  Ver_ParsePrintErrorMessage( pMan );
1365  return 0;
1366  }
1367  // if this is the first net, add it as an output
1368  if ( Abc_ObjFanoutNum(pNode) == 0 )
1369  Abc_ObjAddFanin( pNet, pNode );
1370  else
1371  Abc_ObjAddFanin( pNode, pNet );
1372  // check if it is the end of gate
1373  Ver_ParseSkipComments( pMan );
1374  Symbol = Ver_StreamPopChar(p);
1375  if ( Symbol == ')' )
1376  break;
1377  // skip comma
1378  if ( Symbol != ',' )
1379  {
1380  sprintf( pMan->sError, "Cannot parse a standard gate %s (expected closing paranthesis).", Abc_ObjName(Abc_ObjFanout0(pNode)) );
1381  Ver_ParsePrintErrorMessage( pMan );
1382  return 0;
1383  }
1384  Ver_ParseSkipComments( pMan );
1385  }
1386  if ( (GateType == VER_GATE_BUF || GateType == VER_GATE_NOT) && Abc_ObjFaninNum(pNode) != 1 )
1387  {
1388  sprintf( pMan->sError, "Buffer or interver with multiple fanouts %s (currently not supported).", Abc_ObjName(Abc_ObjFanout0(pNode)) );
1389  Ver_ParsePrintErrorMessage( pMan );
1390  return 0;
1391  }
1392 
1393  // check if it is the end of gate
1394  Ver_ParseSkipComments( pMan );
1395  if ( Ver_StreamPopChar(p) != ';' )
1396  {
1397  sprintf( pMan->sError, "Cannot read standard gate %s (expected closing semicolumn).", Abc_ObjName(Abc_ObjFanout0(pNode)) );
1398  Ver_ParsePrintErrorMessage( pMan );
1399  return 0;
1400  }
1401  // add logic function
1402  if ( GateType == VER_GATE_AND || GateType == VER_GATE_NAND )
1403  pNode->pData = Hop_CreateAnd( (Hop_Man_t *)pNtk->pManFunc, Abc_ObjFaninNum(pNode) );
1404  else if ( GateType == VER_GATE_OR || GateType == VER_GATE_NOR )
1405  pNode->pData = Hop_CreateOr( (Hop_Man_t *)pNtk->pManFunc, Abc_ObjFaninNum(pNode) );
1406  else if ( GateType == VER_GATE_XOR || GateType == VER_GATE_XNOR )
1407  pNode->pData = Hop_CreateExor( (Hop_Man_t *)pNtk->pManFunc, Abc_ObjFaninNum(pNode) );
1408  else if ( GateType == VER_GATE_BUF || GateType == VER_GATE_NOT )
1409  pNode->pData = Hop_CreateAnd( (Hop_Man_t *)pNtk->pManFunc, Abc_ObjFaninNum(pNode) );
1410  if ( GateType == VER_GATE_NAND || GateType == VER_GATE_NOR || GateType == VER_GATE_XNOR || GateType == VER_GATE_NOT )
1411  pNode->pData = Hop_Not( (Hop_Obj_t *)pNode->pData );
1412  return 1;
1413 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Abc_ObjFanoutNum
static int Abc_ObjFanoutNum(Abc_Obj_t *pObj)
Definition: abc.h:365
Abc_ObjFaninNum
static int Abc_ObjFaninNum(Abc_Obj_t *pObj)
Definition: abc.h:364
Ver_StreamPopChar
char Ver_StreamPopChar(Ver_Stream_t *p)
Definition: verStream.c:275
Hop_CreateExor
Hop_Obj_t * Hop_CreateExor(Hop_Man_t *p, int nVars)
Definition: hopOper.c:362
Ver_ParseConvertNetwork
int Ver_ParseConvertNetwork(Ver_Man_t *pMan, Abc_Ntk_t *pNtk, int fMapped)
Definition: verCore.c:351
GateType
GateType
Definition: csat_apis.h:49
Hop_Not
static Hop_Obj_t * Hop_Not(Hop_Obj_t *p)
Definition: hop.h:127
Ver_ParseSkipComments
int Ver_ParseSkipComments(Ver_Man_t *p)
DECLARATIONS ///.
Definition: verParse.c:45
Hop_Obj_t_
Definition: hop.h:65
Abc_ObjAddFanin
ABC_DLL void Abc_ObjAddFanin(Abc_Obj_t *pObj, Abc_Obj_t *pFanin)
Definition: abcFanio.c:84
Ver_Stream_t_
Definition: verStream.c:36
Abc_Obj_t_
Definition: abc.h:128
Abc_Ntk_t_::pManFunc
void * pManFunc
Definition: abc.h:191
Hop_CreateAnd
Hop_Obj_t * Hop_CreateAnd(Hop_Man_t *p, int nVars)
Definition: hopOper.c:320
Ver_ParseGetName
char * Ver_ParseGetName(Ver_Man_t *p)
Definition: verParse.c:91
sprintf
char * sprintf()
Hop_CreateOr
Hop_Obj_t * Hop_CreateOr(Hop_Man_t *p, int nVars)
Definition: hopOper.c:341
Abc_ObjName
ABC_DLL char * Abc_ObjName(Abc_Obj_t *pNode)
DECLARATIONS ///.
Definition: abcNames.c:48
Abc_NtkCreateNode
static Abc_Obj_t * Abc_NtkCreateNode(Abc_Ntk_t *pNtk)
Definition: abc.h:308
Ver_ParsePrintErrorMessage
void Ver_ParsePrintErrorMessage(Ver_Man_t *p)
Definition: verCore.c:278
Abc_Obj_t_::pData
void * pData
Definition: abc.h:145
Hop_Man_t
typedefABC_NAMESPACE_HEADER_START struct Hop_Man_t_ Hop_Man_t
INCLUDES ///.
Definition: hop.h:49
Abc_ObjFanout0
static Abc_Obj_t * Abc_ObjFanout0(Abc_Obj_t *pObj)
Definition: abc.h:371
Ver_ParseFindNet
Abc_Obj_t * Ver_ParseFindNet(Abc_Ntk_t *pNtk, char *pName)
Definition: verCore.c:328
Ver_Bundle_t* Ver_ParseGetNondrivenBundle ( Abc_Ntk_t *  pNtk,
int  Counter 
)

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

Synopsis [Returns the non-driven bundle that is given distance from the end.]

Description []

SideEffects []

SeeAlso []

Definition at line 2509 of file verCore.c.

2510 {
2511  Ver_Bundle_t * pBundle;
2512  Abc_Obj_t * pBox, * pNet;
2513  int k, m;
2514  // go through instances of this type
2515  Vec_PtrForEachEntry( Abc_Obj_t *, (Vec_Ptr_t *)pNtk->pData, pBox, k )
2516  {
2517  if ( Counter >= Vec_PtrSize((Vec_Ptr_t *)pBox->pCopy) )
2518  continue;
2519  // get the bundle given distance away
2520  pBundle = (Ver_Bundle_t *)Vec_PtrEntry( (Vec_Ptr_t *)pBox->pCopy, Vec_PtrSize((Vec_Ptr_t *)pBox->pCopy) - 1 - Counter );
2521  if ( pBundle == NULL )
2522  continue;
2523  // go through the actual nets of this bundle
2524  Vec_PtrForEachEntry( Abc_Obj_t *, pBundle->vNetsActual, pNet, m )
2525  if ( !Abc_ObjFaninNum(pNet) && !Ver_ParseFormalNetsAreDriven(pNtk, pBundle->pNameFormal) ) // non-driven
2526  return pBundle;
2527  }
2528  return NULL;
2529 }
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Abc_ObjFaninNum
static int Abc_ObjFaninNum(Abc_Obj_t *pObj)
Definition: abc.h:364
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Abc_Ntk_t_::pData
void * pData
Definition: abc.h:203
Abc_Obj_t_
Definition: abc.h:128
Ver_ParseFormalNetsAreDriven
int Ver_ParseFormalNetsAreDriven(Abc_Ntk_t *pNtk, char *pNameFormal)
Definition: verCore.c:2474
Abc_Obj_t_::pCopy
Abc_Obj_t * pCopy
Definition: abc.h:148
if
if(last==0)
Definition: sparse_int.h:34
Counter
static int Counter
Definition: extraBddMisc.c:1877
Ver_Bundle_t_::vNetsActual
Vec_Ptr_t * vNetsActual
Definition: verCore.c:86
Ver_Bundle_t_
Definition: verCore.c:83
Vec_PtrEntry
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
int Ver_ParseInitial ( Ver_Man_t *  pMan,
Abc_Ntk_t *  pNtk 
)
static

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

Synopsis [Parses one directive.]

Description []

SideEffects []

SeeAlso []

Definition at line 991 of file verCore.c.

992 {
993  Ver_Stream_t * p = pMan->pReader;
994  Abc_Obj_t * pNode, * pNet;
995  int fStopAfterOne;
996  char * pWord, * pEquation;
997  char Symbol;
998  // parse the directive
999  pWord = Ver_ParseGetName( pMan );
1000  if ( pWord == NULL )
1001  return 0;
1002  // decide how many statements to parse
1003  fStopAfterOne = 0;
1004  if ( strcmp( pWord, "begin" ) )
1005  fStopAfterOne = 1;
1006  // iterate over the initial states
1007  while ( 1 )
1008  {
1009  if ( !fStopAfterOne )
1010  {
1011  // get the name of the output signal
1012  pWord = Ver_ParseGetName( pMan );
1013  if ( pWord == NULL )
1014  return 0;
1015  // look for the end of directive
1016  if ( !strcmp( pWord, "end" ) )
1017  break;
1018  }
1019  // get the fanout net
1020  pNet = Ver_ParseFindNet( pNtk, pWord );
1021  if ( pNet == NULL )
1022  {
1023  sprintf( pMan->sError, "Cannot read the initial statement for %s (output wire is not defined).", pWord );
1024  Ver_ParsePrintErrorMessage( pMan );
1025  return 0;
1026  }
1027  // get the equality sign
1028  Symbol = Ver_StreamPopChar(p);
1029  if ( Symbol != '<' && Symbol != '=' )
1030  {
1031  sprintf( pMan->sError, "Cannot read the assign statement for %s (expected <= or =).", pWord );
1032  Ver_ParsePrintErrorMessage( pMan );
1033  return 0;
1034  }
1035  if ( Symbol == '<' )
1036  Ver_StreamPopChar(p);
1037  // skip the comments
1038  if ( !Ver_ParseSkipComments( pMan ) )
1039  return 0;
1040  // get the second name
1041  pEquation = Ver_StreamGetWord( p, ";" );
1042  if ( pEquation == NULL )
1043  return 0;
1044  // find the corresponding latch
1045  if ( Abc_ObjFaninNum(pNet) == 0 )
1046  {
1047  sprintf( pMan->sError, "Cannot find the latch to assign the initial value." );
1048  Ver_ParsePrintErrorMessage( pMan );
1049  return 0;
1050  }
1051  pNode = Abc_ObjFanin0(Abc_ObjFanin0(pNet));
1052  assert( Abc_ObjIsLatch(pNode) );
1053  // set the initial state
1054  if ( !strcmp(pEquation, "0") || !strcmp(pEquation, "1\'b0") )
1055  Abc_LatchSetInit0( pNode );
1056  else if ( !strcmp(pEquation, "1") || !strcmp(pEquation, "1\'b1") )
1057  Abc_LatchSetInit1( pNode );
1058 // else if ( !strcmp(pEquation, "2") )
1059 // Abc_LatchSetInitDc( pNode );
1060  else
1061  {
1062  sprintf( pMan->sError, "Incorrect initial value of the latch %s.", Abc_ObjName(pNet) );
1063  Ver_ParsePrintErrorMessage( pMan );
1064  return 0;
1065  }
1066  // remove the last symbol
1067  Symbol = Ver_StreamPopChar(p);
1068  assert( Symbol == ';' );
1069  // quit if only one directive
1070  if ( fStopAfterOne )
1071  break;
1072  }
1073  return 1;
1074 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Abc_ObjIsLatch
static int Abc_ObjIsLatch(Abc_Obj_t *pObj)
Definition: abc.h:356
Abc_ObjFaninNum
static int Abc_ObjFaninNum(Abc_Obj_t *pObj)
Definition: abc.h:364
Ver_StreamPopChar
char Ver_StreamPopChar(Ver_Stream_t *p)
Definition: verStream.c:275
Abc_ObjFanin0
static Abc_Obj_t * Abc_ObjFanin0(Abc_Obj_t *pObj)
Definition: abc.h:373
Ver_ParseSkipComments
int Ver_ParseSkipComments(Ver_Man_t *p)
DECLARATIONS ///.
Definition: verParse.c:45
Ver_StreamGetWord
char * Ver_StreamGetWord(Ver_Stream_t *p, char *pCharsToStop)
Definition: verStream.c:397
strcmp
int strcmp()
Ver_Stream_t_
Definition: verStream.c:36
Abc_Obj_t_
Definition: abc.h:128
Ver_ParseGetName
char * Ver_ParseGetName(Ver_Man_t *p)
Definition: verParse.c:91
sprintf
char * sprintf()
Abc_LatchSetInit1
static void Abc_LatchSetInit1(Abc_Obj_t *pLatch)
Definition: abc.h:419
Abc_ObjName
ABC_DLL char * Abc_ObjName(Abc_Obj_t *pNode)
DECLARATIONS ///.
Definition: abcNames.c:48
Ver_ParsePrintErrorMessage
void Ver_ParsePrintErrorMessage(Ver_Man_t *p)
Definition: verCore.c:278
assert
#define assert(ex)
Definition: util_old.h:213
Abc_LatchSetInit0
static void Abc_LatchSetInit0(Abc_Obj_t *pLatch)
Definition: abc.h:418
Ver_ParseFindNet
Abc_Obj_t * Ver_ParseFindNet(Abc_Ntk_t *pNtk, char *pName)
Definition: verCore.c:328
int Ver_ParseInsertsSuffix ( Ver_Man_t *  pMan,
char *  pWord,
int  nMsb,
int  nLsb 
)

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

Synopsis [Lookups the suffix of the signal of the form [m:n].]

Description []

SideEffects []

SeeAlso []

Definition at line 587 of file verCore.c.

588 {
589  unsigned Value;
590  if ( pMan->tName2Suffix == NULL )
591  pMan->tName2Suffix = st__init_table( strcmp, st__strhash );
592  if ( st__is_member( pMan->tName2Suffix, pWord ) )
593  return 1;
594  assert( nMsb >= 0 && nMsb < 128 );
595  assert( nLsb >= 0 && nLsb < 128 );
596  Value = (nMsb << 8) | nLsb;
597  st__insert( pMan->tName2Suffix, Extra_UtilStrsav(pWord), (char *)(ABC_PTRUINT_T)Value );
598  return 1;
599 }
st__insert
int st__insert(st__table *table, const char *key, char *value)
Definition: st.c:171
st__is_member
#define st__is_member(table, key)
Definition: st.h:70
Extra_UtilStrsav
char * Extra_UtilStrsav(const char *s)
Definition: extraUtilUtil.c:169
strcmp
int strcmp()
st__init_table
st__table * st__init_table(st__compare_func_type compare, st__hash_func_type hash)
Definition: st.c:72
st__strhash
int st__strhash(const char *string, int modulus)
Definition: st.c:449
assert
#define assert(ex)
Definition: util_old.h:213
void Ver_ParseInternal ( Ver_Man_t *  pMan)
static

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

Synopsis [File parser.]

Description []

SideEffects []

SeeAlso []

Definition at line 200 of file verCore.c.

201 {
202  Abc_Ntk_t * pNtk;
203  char * pToken;
204  int i;
205 
206  // preparse the modeles
207  pMan->pProgress = Extra_ProgressBarStart( stdout, Ver_StreamGetFileSize(pMan->pReader) );
208  while ( 1 )
209  {
210  // get the next token
211  pToken = Ver_ParseGetName( pMan );
212  if ( pToken == NULL )
213  break;
214  if ( strcmp( pToken, "module" ) )
215  {
216  sprintf( pMan->sError, "Cannot read \"module\" directive." );
217  Ver_ParsePrintErrorMessage( pMan );
218  return;
219  }
220  // parse the module
221  if ( !Ver_ParseModule(pMan) )
222  return;
223  }
224  Extra_ProgressBarStop( pMan->pProgress );
225  pMan->pProgress = NULL;
226 
227  // process defined and undefined boxes
228  if ( !Ver_ParseAttachBoxes( pMan ) )
229  return;
230 
231  // connect the boxes and check
232  Vec_PtrForEachEntry( Abc_Ntk_t *, pMan->pDesign->vModules, pNtk, i )
233  {
234  // fix the dangling nets
235  Abc_NtkFinalizeRead( pNtk );
236  // check the network for correctness
237  if ( pMan->fCheck && !Abc_NtkCheckRead( pNtk ) )
238  {
239  pMan->fTopLevel = 1;
240  sprintf( pMan->sError, "The network check has failed for network %s.", pNtk->pName );
241  Ver_ParsePrintErrorMessage( pMan );
242  return;
243  }
244  }
245 }
Abc_Ntk_t_
Definition: abc.h:153
Abc_NtkFinalizeRead
ABC_DLL void Abc_NtkFinalizeRead(Abc_Ntk_t *pNtk)
Definition: abcNtk.c:360
strcmp
int strcmp()
Ver_ParseAttachBoxes
static int Ver_ParseAttachBoxes(Ver_Man_t *pMan)
Definition: verCore.c:2870
Abc_NtkCheckRead
ABC_DLL int Abc_NtkCheckRead(Abc_Ntk_t *pNtk)
Definition: abcCheck.c:77
Ver_ParseGetName
char * Ver_ParseGetName(Ver_Man_t *p)
Definition: verParse.c:91
sprintf
char * sprintf()
Extra_ProgressBarStop
void Extra_ProgressBarStop(ProgressBar *p)
Definition: extraUtilProgress.c:118
Ver_ParsePrintErrorMessage
void Ver_ParsePrintErrorMessage(Ver_Man_t *p)
Definition: verCore.c:278
Extra_ProgressBarStart
ProgressBar * Extra_ProgressBarStart(FILE *pFile, int nItemsTotal)
FUNCTION DEFINITIONS ///.
Definition: extraUtilProgress.c:62
Abc_Des_t_::vModules
Vec_Ptr_t * vModules
Definition: abc.h:223
Ver_ParseModule
static int Ver_ParseModule(Ver_Man_t *p)
Definition: verCore.c:401
Ver_StreamGetFileSize
int Ver_StreamGetFileSize(Ver_Stream_t *p)
Definition: verStream.c:192
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
Abc_Ntk_t_::pDesign
Abc_Des_t * pDesign
Definition: abc.h:180
Abc_Ntk_t_::pName
char * pName
Definition: abc.h:158
int Ver_ParseLookupSuffix ( Ver_Man_t *  pMan,
char *  pWord,
int *  pnMsb,
int *  pnLsb 
)

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

Synopsis [Lookups the suffix of the signal of the form [m:n].]

Description []

SideEffects []

SeeAlso []

Definition at line 563 of file verCore.c.

564 {
565  unsigned Value;
566  *pnMsb = *pnLsb = -1;
567  if ( pMan->tName2Suffix == NULL )
568  return 1;
569  if ( ! st__lookup( pMan->tName2Suffix, (char *)pWord, (char **)&Value ) )
570  return 1;
571  *pnMsb = (Value >> 8) & 0xff;
572  *pnLsb = Value & 0xff;
573  return 1;
574 }
st__lookup
int st__lookup(st__table *table, const char *key, char **value)
Definition: st.c:114
int Ver_ParseMaxBoxSize ( Vec_Ptr_t *  vUndefs)

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

Synopsis [Returns the max size of any undef box.]

Description []

SideEffects []

SeeAlso []

Definition at line 2709 of file verCore.c.

2710 {
2711  Abc_Ntk_t * pNtk;
2712  Abc_Obj_t * pBox;
2713  int i, k, nMaxSize = 0;
2714  // go through undef box types
2715  Vec_PtrForEachEntry( Abc_Ntk_t *, vUndefs, pNtk, i )
2716  // go through instances of this type
2717  Vec_PtrForEachEntry( Abc_Obj_t *, (Vec_Ptr_t *)pNtk->pData, pBox, k )
2718  // check the number of bundles of this instance
2719  if ( nMaxSize < Vec_PtrSize((Vec_Ptr_t *)pBox->pCopy) )
2720  nMaxSize = Vec_PtrSize((Vec_Ptr_t *)pBox->pCopy);
2721  return nMaxSize;
2722 }
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Abc_Ntk_t_
Definition: abc.h:153
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Abc_Obj_t_
Definition: abc.h:128
if
if(last==0)
Definition: sparse_int.h:34
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
int Ver_ParseModule ( Ver_Man_t *  pMan)
static

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

Synopsis [Parses one Verilog module.]

Description []

SideEffects []

SeeAlso []

Definition at line 401 of file verCore.c.

402 {
403  Mio_Gate_t * pGate;
404  Ver_Stream_t * p = pMan->pReader;
405  Abc_Ntk_t * pNtk, * pNtkTemp;
406  char * pWord, Symbol;
407  int RetValue;
408 
409  // get the network name
410  pWord = Ver_ParseGetName( pMan );
411 
412  // get the network with this name
413  pNtk = Ver_ParseFindOrCreateNetwork( pMan, pWord );
414 
415  // make sure we stopped at the opening paranthesis
416  if ( Ver_StreamPopChar(p) != '(' )
417  {
418  sprintf( pMan->sError, "Cannot find \"(\" after \"module\" in network %s.", pNtk->pName );
419  Ver_ParsePrintErrorMessage( pMan );
420  return 0;
421  }
422 
423  // skip to the end of parantheses
424  do {
425  if ( Ver_ParseGetName( pMan ) == NULL )
426  return 0;
427  Symbol = Ver_StreamPopChar(p);
428  } while ( Symbol == ',' );
429  assert( Symbol == ')' );
430  if ( !Ver_ParseSkipComments( pMan ) )
431  return 0;
432  Symbol = Ver_StreamPopChar(p);
433  if ( Symbol != ';' )
434  {
435  sprintf( pMan->sError, "Expected closing paranthesis after \"module\"." );
436  Ver_ParsePrintErrorMessage( pMan );
437  return 0;
438  }
439 
440  // parse the inputs/outputs/registers/wires/inouts
441  while ( 1 )
442  {
443  Extra_ProgressBarUpdate( pMan->pProgress, Ver_StreamGetCurPosition(p), NULL );
444  pWord = Ver_ParseGetName( pMan );
445  if ( pWord == NULL )
446  return 0;
447  if ( !strcmp( pWord, "input" ) )
448  RetValue = Ver_ParseSignal( pMan, pNtk, VER_SIG_INPUT );
449  else if ( !strcmp( pWord, "output" ) )
450  RetValue = Ver_ParseSignal( pMan, pNtk, VER_SIG_OUTPUT );
451  else if ( !strcmp( pWord, "reg" ) )
452  RetValue = Ver_ParseSignal( pMan, pNtk, VER_SIG_REG );
453  else if ( !strcmp( pWord, "wire" ) )
454  RetValue = Ver_ParseSignal( pMan, pNtk, VER_SIG_WIRE );
455  else if ( !strcmp( pWord, "inout" ) )
456  RetValue = Ver_ParseSignal( pMan, pNtk, VER_SIG_INOUT );
457  else
458  break;
459  if ( RetValue == 0 )
460  return 0;
461  }
462 
463  // parse the remaining statements
464  while ( 1 )
465  {
466  Extra_ProgressBarUpdate( pMan->pProgress, Ver_StreamGetCurPosition(p), NULL );
467 
468  if ( !strcmp( pWord, "and" ) )
469  RetValue = Ver_ParseGateStandard( pMan, pNtk, VER_GATE_AND );
470  else if ( !strcmp( pWord, "or" ) )
471  RetValue = Ver_ParseGateStandard( pMan, pNtk, VER_GATE_OR );
472  else if ( !strcmp( pWord, "xor" ) )
473  RetValue = Ver_ParseGateStandard( pMan, pNtk, VER_GATE_XOR );
474  else if ( !strcmp( pWord, "buf" ) )
475  RetValue = Ver_ParseGateStandard( pMan, pNtk, VER_GATE_BUF );
476  else if ( !strcmp( pWord, "nand" ) )
477  RetValue = Ver_ParseGateStandard( pMan, pNtk, VER_GATE_NAND );
478  else if ( !strcmp( pWord, "nor" ) )
479  RetValue = Ver_ParseGateStandard( pMan, pNtk, VER_GATE_NOR );
480  else if ( !strcmp( pWord, "xnor" ) )
481  RetValue = Ver_ParseGateStandard( pMan, pNtk, VER_GATE_XNOR );
482  else if ( !strcmp( pWord, "not" ) )
483  RetValue = Ver_ParseGateStandard( pMan, pNtk, VER_GATE_NOT );
484 
485  else if ( !strcmp( pWord, "dff" ) )
486  RetValue = Ver_ParseFlopStandard( pMan, pNtk );
487 
488  else if ( !strcmp( pWord, "assign" ) )
489  RetValue = Ver_ParseAssign( pMan, pNtk );
490  else if ( !strcmp( pWord, "always" ) )
491  RetValue = Ver_ParseAlways( pMan, pNtk );
492  else if ( !strcmp( pWord, "initial" ) )
493  RetValue = Ver_ParseInitial( pMan, pNtk );
494  else if ( !strcmp( pWord, "endmodule" ) )
495  break;
496  else if ( pMan->pDesign->pGenlib && (pGate = Mio_LibraryReadGateByName((Mio_Library_t *)pMan->pDesign->pGenlib, pWord, NULL)) ) // current design
497  RetValue = Ver_ParseGate( pMan, pNtk, pGate );
498 // else if ( pMan->pDesign->pLibrary && st__lookup(pMan->pDesign->pLibrary->tModules, pWord, (char**)&pNtkTemp) ) // gate library
499 // RetValue = Ver_ParseGate( pMan, pNtkTemp );
500  else if ( !strcmp( pWord, "wire" ) )
501  RetValue = Ver_ParseSignal( pMan, pNtk, VER_SIG_WIRE );
502  else // assume this is the box used in the current design
503  {
504  pNtkTemp = Ver_ParseFindOrCreateNetwork( pMan, pWord );
505  RetValue = Ver_ParseBox( pMan, pNtk, pNtkTemp );
506  }
507  if ( RetValue == 0 )
508  return 0;
509  // skip the comments
510  if ( !Ver_ParseSkipComments( pMan ) )
511  return 0;
512  // get new word
513  pWord = Ver_ParseGetName( pMan );
514  if ( pWord == NULL )
515  return 0;
516  }
517 
518  // convert from the blackbox into the network with local functions representated by AIGs
519  if ( pNtk->ntkFunc == ABC_FUNC_BLACKBOX )
520  {
521  if ( Abc_NtkNodeNum(pNtk) > 0 || Abc_NtkBoxNum(pNtk) > 0 )
522  {
523  if ( !Ver_ParseConvertNetwork( pMan, pNtk, pMan->fMapped ) )
524  return 0;
525  }
526  else
527  {
528  Abc_Obj_t * pObj, * pBox, * pTerm;
529  int i;
530  pBox = Abc_NtkCreateBlackbox(pNtk);
531  Abc_NtkForEachPi( pNtk, pObj, i )
532  {
533  pTerm = Abc_NtkCreateBi(pNtk);
534  Abc_ObjAddFanin( pTerm, Abc_ObjFanout0(pObj) );
535  Abc_ObjAddFanin( pBox, pTerm );
536  }
537  Abc_NtkForEachPo( pNtk, pObj, i )
538  {
539  pTerm = Abc_NtkCreateBo(pNtk);
540  Abc_ObjAddFanin( pTerm, pBox );
541  Abc_ObjAddFanin( Abc_ObjFanin0(pObj), pTerm );
542  }
543  }
544  }
545 
546  // remove the table if needed
547  Ver_ParseRemoveSuffixTable( pMan );
548  return 1;
549 }
Mio_LibraryReadGateByName
Mio_Gate_t * Mio_LibraryReadGateByName(Mio_Library_t *pLib, char *pName, char *pOutName)
Definition: mioApi.c:99
Ver_ParseAssign
static int Ver_ParseAssign(Ver_Man_t *p, Abc_Ntk_t *pNtk)
Definition: verCore.c:1087
Ver_ParseInitial
static int Ver_ParseInitial(Ver_Man_t *p, Abc_Ntk_t *pNtk)
Definition: verCore.c:991
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Abc_Ntk_t_
Definition: abc.h:153
Abc_NtkBoxNum
static int Abc_NtkBoxNum(Abc_Ntk_t *pNtk)
Definition: abc.h:289
Ver_ParseBox
static int Ver_ParseBox(Ver_Man_t *pMan, Abc_Ntk_t *pNtk, Abc_Ntk_t *pNtkBox)
Definition: verCore.c:1732
Ver_StreamPopChar
char Ver_StreamPopChar(Ver_Stream_t *p)
Definition: verStream.c:275
Ver_ParseSignal
static int Ver_ParseSignal(Ver_Man_t *p, Abc_Ntk_t *pNtk, Ver_SignalType_t SigType)
Definition: verCore.c:805
Ver_ParseConvertNetwork
int Ver_ParseConvertNetwork(Ver_Man_t *pMan, Abc_Ntk_t *pNtk, int fMapped)
Definition: verCore.c:351
Abc_ObjFanin0
static Abc_Obj_t * Abc_ObjFanin0(Abc_Obj_t *pObj)
Definition: abc.h:373
Ver_ParseSkipComments
int Ver_ParseSkipComments(Ver_Man_t *p)
DECLARATIONS ///.
Definition: verParse.c:45
Ver_ParseFlopStandard
static int Ver_ParseFlopStandard(Ver_Man_t *pMan, Abc_Ntk_t *pNtk)
Definition: verCore.c:1426
Abc_ObjAddFanin
ABC_DLL void Abc_ObjAddFanin(Abc_Obj_t *pObj, Abc_Obj_t *pFanin)
Definition: abcFanio.c:84
strcmp
int strcmp()
Ver_Stream_t_
Definition: verStream.c:36
Abc_Obj_t_
Definition: abc.h:128
Abc_NtkCreateBo
static Abc_Obj_t * Abc_NtkCreateBo(Abc_Ntk_t *pNtk)
Definition: abc.h:306
Abc_NtkNodeNum
static int Abc_NtkNodeNum(Abc_Ntk_t *pNtk)
Definition: abc.h:293
Ver_ParseGateStandard
static int Ver_ParseGateStandard(Ver_Man_t *pMan, Abc_Ntk_t *pNtk, Ver_GateType_t GateType)
Definition: verCore.c:1330
Ver_ParseRemoveSuffixTable
static void Ver_ParseRemoveSuffixTable(Ver_Man_t *pMan)
Definition: verCore.c:612
Ver_ParseGetName
char * Ver_ParseGetName(Ver_Man_t *p)
Definition: verParse.c:91
Mio_LibraryStruct_t_
STRUCTURE DEFINITIONS ///.
Definition: mioInt.h:61
sprintf
char * sprintf()
Abc_NtkCreateBlackbox
static Abc_Obj_t * Abc_NtkCreateBlackbox(Abc_Ntk_t *pNtk)
Definition: abc.h:311
Ver_ParseAlways
static int Ver_ParseAlways(Ver_Man_t *p, Abc_Ntk_t *pNtk)
Definition: verCore.c:892
Mio_GateStruct_t_
Definition: mioInt.h:79
Ver_ParseGate
static int Ver_ParseGate(Ver_Man_t *p, Abc_Ntk_t *pNtk, Mio_Gate_t *pGate)
Definition: verCore.c:1550
Abc_Ntk_t_::ntkFunc
Abc_NtkFunc_t ntkFunc
Definition: abc.h:157
Ver_StreamGetCurPosition
int Ver_StreamGetCurPosition(Ver_Stream_t *p)
Definition: verStream.c:208
Ver_ParsePrintErrorMessage
void Ver_ParsePrintErrorMessage(Ver_Man_t *p)
Definition: verCore.c:278
assert
#define assert(ex)
Definition: util_old.h:213
Extra_ProgressBarUpdate
static void Extra_ProgressBarUpdate(ProgressBar *p, int nItemsCur, char *pString)
Definition: extra.h:243
Ver_ParseFindOrCreateNetwork
Abc_Ntk_t * Ver_ParseFindOrCreateNetwork(Ver_Man_t *pMan, char *pName)
Definition: verCore.c:301
Abc_NtkForEachPo
#define Abc_NtkForEachPo(pNtk, pPo, i)
Definition: abc.h:517
Abc_NtkCreateBi
static Abc_Obj_t * Abc_NtkCreateBi(Abc_Ntk_t *pNtk)
Definition: abc.h:305
Abc_Ntk_t_::pName
char * pName
Definition: abc.h:158
Abc_ObjFanout0
static Abc_Obj_t * Abc_ObjFanout0(Abc_Obj_t *pObj)
Definition: abc.h:371
Abc_NtkForEachPi
#define Abc_NtkForEachPi(pNtk, pPi, i)
Definition: abc.h:513
void Ver_ParsePrintErrorMessage ( Ver_Man_t *  p)

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

Synopsis [Prints the error message including the file name and line number.]

Description []

SideEffects []

SeeAlso []

Definition at line 278 of file verCore.c.

279 {
280  p->fError = 1;
281  if ( p->fTopLevel ) // the line number is not given
282  fprintf( p->Output, "%s: %s\n", p->pFileName, p->sError );
283  else // print the error message with the line number
284  fprintf( p->Output, "%s (line %d): %s\n",
285  p->pFileName, Ver_StreamGetLineNumber(p->pReader), p->sError );
286  // free the data
287  Ver_ParseFreeData( p );
288 }
Ver_StreamGetLineNumber
int Ver_StreamGetLineNumber(Ver_Stream_t *p)
Definition: verStream.c:224
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Ver_ParseFreeData
static void Ver_ParseFreeData(Ver_Man_t *p)
Definition: verCore.c:258
void Ver_ParsePrintLog ( Ver_Man_t *  pMan)

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

Synopsis [Prints the comprehensive report into a log file.]

Description []

SideEffects []

SeeAlso []

Definition at line 2735 of file verCore.c.

2736 {
2737  Abc_Ntk_t * pNtk, * pNtkBox;
2738  Abc_Obj_t * pBox;
2739  FILE * pFile;
2740  char * pNameGeneric;
2741  char Buffer[1000];
2742  int i, k, Count1 = 0;
2743 
2744  // open the log file
2745  pNameGeneric = Extra_FileNameGeneric( pMan->pFileName );
2746  sprintf( Buffer, "%s.log", pNameGeneric );
2747  ABC_FREE( pNameGeneric );
2748  pFile = fopen( Buffer, "w" );
2749 
2750  // count the total number of instances and how many times they occur
2751  Vec_PtrForEachEntry( Abc_Ntk_t *, pMan->pDesign->vModules, pNtk, i )
2752  pNtk->fHieVisited = 0;
2753  Vec_PtrForEachEntry( Abc_Ntk_t *, pMan->pDesign->vModules, pNtk, i )
2754  Abc_NtkForEachBox( pNtk, pBox, k )
2755  {
2756  if ( Abc_ObjIsLatch(pBox) )
2757  continue;
2758  pNtkBox = (Abc_Ntk_t *)pBox->pData;
2759  if ( pNtkBox == NULL )
2760  continue;
2761  pNtkBox->fHieVisited++;
2762  }
2763  // print each box and its stats
2764  fprintf( pFile, "The hierarhical design %s contains %d modules:\n", pMan->pFileName, Vec_PtrSize(pMan->pDesign->vModules) );
2765  Vec_PtrForEachEntry( Abc_Ntk_t *, pMan->pDesign->vModules, pNtk, i )
2766  {
2767  fprintf( pFile, "%-50s : ", Abc_NtkName(pNtk) );
2768  if ( !Ver_NtkIsDefined(pNtk) )
2769  fprintf( pFile, "undefbox" );
2770  else if ( Abc_NtkHasBlackbox(pNtk) )
2771  fprintf( pFile, "blackbox" );
2772  else
2773  fprintf( pFile, "logicbox" );
2774  fprintf( pFile, " instantiated %6d times ", pNtk->fHieVisited );
2775 // fprintf( pFile, "\n " );
2776  fprintf( pFile, " pi = %4d", Abc_NtkPiNum(pNtk) );
2777  fprintf( pFile, " po = %4d", Abc_NtkPoNum(pNtk) );
2778  fprintf( pFile, " nd = %8d", Abc_NtkNodeNum(pNtk) );
2779  fprintf( pFile, " lat = %6d", Abc_NtkLatchNum(pNtk) );
2780  fprintf( pFile, " box = %6d", Abc_NtkBoxNum(pNtk)-Abc_NtkLatchNum(pNtk) );
2781  fprintf( pFile, "\n" );
2782  Count1 += (Abc_NtkPoNum(pNtk) == 1);
2783  }
2784  Vec_PtrForEachEntry( Abc_Ntk_t *, pMan->pDesign->vModules, pNtk, i )
2785  pNtk->fHieVisited = 0;
2786  fprintf( pFile, "The number of modules with one output = %d (%.2f %%).\n", Count1, 100.0 * Count1/Vec_PtrSize(pMan->pDesign->vModules) );
2787 
2788  // report instances with dangling outputs
2789  if ( Vec_PtrSize(pMan->pDesign->vModules) > 1 )
2790  {
2791  Vec_Ptr_t * vBundles;
2792  Ver_Bundle_t * pBundle;
2793  int j, nActNets, Counter = 0;
2794  // count the number of instances with dangling outputs
2795  Vec_PtrForEachEntry( Abc_Ntk_t *, pMan->pDesign->vModules, pNtk, i )
2796  {
2797  Abc_NtkForEachBox( pNtk, pBox, k )
2798  {
2799  if ( Abc_ObjIsLatch(pBox) )
2800  continue;
2801  vBundles = (Vec_Ptr_t *)pBox->pCopy;
2802  pNtkBox = (Abc_Ntk_t *)pBox->pData;
2803  if ( pNtkBox == NULL )
2804  continue;
2805  if ( !Ver_NtkIsDefined(pNtkBox) )
2806  continue;
2807  // count the number of actual nets
2808  nActNets = 0;
2809  Vec_PtrForEachEntry( Ver_Bundle_t *, vBundles, pBundle, j )
2810  nActNets += Vec_PtrSize(pBundle->vNetsActual);
2811  // the box is defined and will be connected
2812  if ( nActNets != Abc_NtkPiNum(pNtkBox) + Abc_NtkPoNum(pNtkBox) )
2813  Counter++;
2814  }
2815  }
2816  if ( Counter == 0 )
2817  fprintf( pFile, "The outputs of all box instances are connected.\n" );
2818  else
2819  {
2820  fprintf( pFile, "\n" );
2821  fprintf( pFile, "The outputs of %d box instances are not connected:\n", Counter );
2822  // enumerate through the boxes
2823  Vec_PtrForEachEntry( Abc_Ntk_t *, pMan->pDesign->vModules, pNtk, i )
2824  {
2825  Abc_NtkForEachBox( pNtk, pBox, k )
2826  {
2827  if ( Abc_ObjIsLatch(pBox) )
2828  continue;
2829  vBundles = (Vec_Ptr_t *)pBox->pCopy;
2830  pNtkBox = (Abc_Ntk_t *)pBox->pData;
2831  if ( pNtkBox == NULL )
2832  continue;
2833  if ( !Ver_NtkIsDefined(pNtkBox) )
2834  continue;
2835  // count the number of actual nets
2836  nActNets = 0;
2837  Vec_PtrForEachEntry( Ver_Bundle_t *, vBundles, pBundle, j )
2838  nActNets += Vec_PtrSize(pBundle->vNetsActual);
2839  // the box is defined and will be connected
2840  if ( nActNets != Abc_NtkPiNum(pNtkBox) + Abc_NtkPoNum(pNtkBox) )
2841  fprintf( pFile, "In module \"%s\" instance \"%s\" of box \"%s\" has different numbers of actual/formal nets (%d/%d).\n",
2842  Abc_NtkName(pNtk), Abc_ObjName(pBox), Abc_NtkName(pNtkBox), nActNets, Abc_NtkPiNum(pNtkBox) + Abc_NtkPoNum(pNtkBox) );
2843  }
2844  }
2845  }
2846  }
2847  fclose( pFile );
2848  printf( "Hierarchy statistics can be found in log file \"%s\".\n", Buffer );
2849 }
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Abc_ObjIsLatch
static int Abc_ObjIsLatch(Abc_Obj_t *pObj)
Definition: abc.h:356
Abc_Ntk_t_
Definition: abc.h:153
Abc_NtkBoxNum
static int Abc_NtkBoxNum(Abc_Ntk_t *pNtk)
Definition: abc.h:289
Abc_NtkLatchNum
static int Abc_NtkLatchNum(Abc_Ntk_t *pNtk)
Definition: abc.h:294
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
nets
ConcreteNet * nets
Definition: abcPlace.c:35
Abc_Ntk_t_::pData
void * pData
Definition: abc.h:203
Abc_Obj_t_
Definition: abc.h:128
Abc_NtkNodeNum
static int Abc_NtkNodeNum(Abc_Ntk_t *pNtk)
Definition: abc.h:293
one
static DdNode * one
Definition: cuddDecomp.c:112
Abc_NtkHasBlackbox
static int Abc_NtkHasBlackbox(Abc_Ntk_t *pNtk)
Definition: abc.h:258
Extra_FileNameGeneric
char * Extra_FileNameGeneric(char *FileName)
Definition: extraUtilFile.c:165
if
if(last==0)
Definition: sparse_int.h:34
else
else
Definition: sparse_int.h:55
sprintf
char * sprintf()
Counter
static int Counter
Definition: extraBddMisc.c:1877
Ver_Bundle_t_
Definition: verCore.c:83
Abc_NtkForEachBox
#define Abc_NtkForEachBox(pNtk, pObj, i)
Definition: abc.h:495
Abc_NtkName
static char * Abc_NtkName(Abc_Ntk_t *pNtk)
Definition: abc.h:270
Abc_NtkPoNum
static int Abc_NtkPoNum(Abc_Ntk_t *pNtk)
Definition: abc.h:286
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Abc_NtkPiNum
static int Abc_NtkPiNum(Abc_Ntk_t *pNtk)
Definition: abc.h:285
Abc_ObjName
ABC_DLL char * Abc_ObjName(Abc_Obj_t *pNode)
DECLARATIONS ///.
Definition: abcNames.c:48
Abc_Des_t_::vModules
Vec_Ptr_t * vModules
Definition: abc.h:223
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
Abc_Ntk_t_::pDesign
Abc_Des_t * pDesign
Definition: abc.h:180
Ver_NtkIsDefined
static int Ver_NtkIsDefined(Abc_Ntk_t *pNtkBox)
Definition: verCore.c:77
Abc_Ntk_t_::fHieVisited
int fHieVisited
Definition: abc.h:182
void Ver_ParseRemoveSuffixTable ( Ver_Man_t *  pMan)
static

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

Synopsis [Lookups the suffic of the signal of the form [m:n].]

Description []

SideEffects []

SeeAlso []

Definition at line 612 of file verCore.c.

613 {
614  st__generator * gen;
615  char * pKey, * pValue;
616  if ( pMan->tName2Suffix == NULL )
617  return;
618  st__foreach_item( pMan->tName2Suffix, gen, (const char **)&pKey, (char **)&pValue )
619  ABC_FREE( pKey );
620  st__free_table( pMan->tName2Suffix );
621  pMan->tName2Suffix = NULL;
622 }
st__free_table
void st__free_table(st__table *table)
Definition: st.c:81
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
st__foreach_item
#define st__foreach_item(table, gen, key, value)
Definition: st.h:107
st__generator
Definition: st.h:64
void Ver_ParseReportUndefBoxes ( Ver_Man_t *  pMan)

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

Synopsis [Reports how many times each type of undefined box occurs.]

Description []

SideEffects []

SeeAlso []

Definition at line 2400 of file verCore.c.

2401 {
2402  Abc_Ntk_t * pNtk;
2403  Abc_Obj_t * pBox;
2404  int i, k, nBoxes;
2405  // clean
2406  nBoxes = 0;
2407  Vec_PtrForEachEntry( Abc_Ntk_t *, pMan->pDesign->vModules, pNtk, i )
2408  {
2409  pNtk->fHiePath = 0;
2410  if ( !Ver_NtkIsDefined(pNtk) )
2411  nBoxes++;
2412  }
2413  // count
2414  Vec_PtrForEachEntry( Abc_Ntk_t *, pMan->pDesign->vModules, pNtk, i )
2415  Abc_NtkForEachBlackbox( pNtk, pBox, k )
2416  if ( pBox->pData && !Ver_NtkIsDefined((Abc_Ntk_t *)pBox->pData) )
2417  ((Abc_Ntk_t *)pBox->pData)->fHiePath++;
2418  // print the stats
2419  printf( "Warning: The design contains %d undefined object types interpreted as blackboxes:\n", nBoxes );
2420  Vec_PtrForEachEntry( Abc_Ntk_t *, pMan->pDesign->vModules, pNtk, i )
2421  if ( !Ver_NtkIsDefined(pNtk) )
2422  printf( "%s (%d) ", Abc_NtkName(pNtk), pNtk->fHiePath );
2423  printf( "\n" );
2424  // clean
2425  Vec_PtrForEachEntry( Abc_Ntk_t *, pMan->pDesign->vModules, pNtk, i )
2426  pNtk->fHiePath = 0;
2427 }
Abc_Ntk_t_
Definition: abc.h:153
Abc_Obj_t_
Definition: abc.h:128
Abc_NtkForEachBlackbox
#define Abc_NtkForEachBlackbox(pNtk, pObj, i)
Definition: abc.h:509
if
if(last==0)
Definition: sparse_int.h:34
Abc_NtkName
static char * Abc_NtkName(Abc_Ntk_t *pNtk)
Definition: abc.h:270
Abc_Des_t_::vModules
Vec_Ptr_t * vModules
Definition: abc.h:223
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
Abc_Ntk_t_::pDesign
Abc_Des_t * pDesign
Definition: abc.h:180
Ver_NtkIsDefined
static int Ver_NtkIsDefined(Abc_Ntk_t *pNtkBox)
Definition: verCore.c:77
Abc_Ntk_t_::fHiePath
int fHiePath
Definition: abc.h:183
int Ver_ParseSignal ( Ver_Man_t *  pMan,
Abc_Ntk_t *  pNtk,
Ver_SignalType_t  SigType 
)
static

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

Synopsis [Parses one directive.]

Description [The signals are added in the order from LSB to MSB.]

SideEffects []

SeeAlso []

Definition at line 805 of file verCore.c.

806 {
807  Ver_Stream_t * p = pMan->pReader;
808  char Buffer[1000], Symbol, * pWord;
809  int nMsb, nLsb, Bit, Limit, i;
810  nMsb = nLsb = -1;
811  while ( 1 )
812  {
813  // get the next word
814  pWord = Ver_ParseGetName( pMan );
815  if ( pWord == NULL )
816  return 0;
817 
818  if ( !strcmp(pWord, "wire") )
819  continue;
820 
821  // check if the range is specified
822  if ( pWord[0] == '[' && !pMan->fNameLast )
823  {
824  assert( nMsb == -1 && nLsb == -1 );
825  Ver_ParseSignalPrefix( pMan, &pWord, &nMsb, &nLsb );
826  // check the case when there is space between bracket and the next word
827  if ( *pWord == 0 )
828  {
829  // get the signal name
830  pWord = Ver_ParseGetName( pMan );
831  if ( pWord == NULL )
832  return 0;
833  }
834  }
835 
836  // create signals
837  if ( nMsb == -1 && nLsb == -1 )
838  {
839  if ( SigType == VER_SIG_INPUT || SigType == VER_SIG_INOUT )
840  Ver_ParseCreatePi( pNtk, pWord );
841  if ( SigType == VER_SIG_OUTPUT || SigType == VER_SIG_INOUT )
842  Ver_ParseCreatePo( pNtk, pWord );
843  if ( SigType == VER_SIG_WIRE || SigType == VER_SIG_REG )
844  Abc_NtkFindOrCreateNet( pNtk, pWord );
845  }
846  else
847  {
848  assert( nMsb >= 0 && nLsb >= 0 );
849  // add to the hash table
850  Ver_ParseInsertsSuffix( pMan, pWord, nMsb, nLsb );
851  // add signals from Lsb to Msb
852  Limit = nMsb > nLsb? nMsb - nLsb + 1: nLsb - nMsb + 1;
853  for ( i = 0, Bit = nLsb; i < Limit; i++, Bit = nMsb > nLsb ? Bit + 1: Bit - 1 )
854  {
855 // sprintf( Buffer, "%s[%d]", pWord, Bit );
856  if ( Limit > 1 )
857  sprintf( Buffer, "%s[%d]", pWord, Bit );
858  else
859  sprintf( Buffer, "%s", pWord );
860  if ( SigType == VER_SIG_INPUT || SigType == VER_SIG_INOUT )
861  Ver_ParseCreatePi( pNtk, Buffer );
862  if ( SigType == VER_SIG_OUTPUT || SigType == VER_SIG_INOUT )
863  Ver_ParseCreatePo( pNtk, Buffer );
864  if ( SigType == VER_SIG_WIRE || SigType == VER_SIG_REG )
865  Abc_NtkFindOrCreateNet( pNtk, Buffer );
866  }
867  }
868 
869  Symbol = Ver_StreamPopChar(p);
870  if ( Symbol == ',' )
871  continue;
872  if ( Symbol == ';' )
873  return 1;
874  break;
875  }
876  sprintf( pMan->sError, "Cannot parse signal line (expected , or ;)." );
877  Ver_ParsePrintErrorMessage( pMan );
878  return 0;
879 }
Ver_ParseSignalPrefix
int Ver_ParseSignalPrefix(Ver_Man_t *pMan, char **ppWord, int *pnMsb, int *pnLsb)
Definition: verCore.c:635
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Ver_StreamPopChar
char Ver_StreamPopChar(Ver_Stream_t *p)
Definition: verStream.c:275
Ver_ParseCreatePi
static Abc_Obj_t * Ver_ParseCreatePi(Abc_Ntk_t *pNtk, char *pName)
Definition: verCore.c:2940
strcmp
int strcmp()
Ver_Stream_t_
Definition: verStream.c:36
Ver_ParseGetName
char * Ver_ParseGetName(Ver_Man_t *p)
Definition: verParse.c:91
Ver_ParseCreatePo
static Abc_Obj_t * Ver_ParseCreatePo(Abc_Ntk_t *pNtk, char *pName)
Definition: verCore.c:2965
sprintf
char * sprintf()
Abc_NtkFindOrCreateNet
ABC_DLL Abc_Obj_t * Abc_NtkFindOrCreateNet(Abc_Ntk_t *pNtk, char *pName)
Definition: abcObj.c:579
Ver_ParseInsertsSuffix
int Ver_ParseInsertsSuffix(Ver_Man_t *pMan, char *pWord, int nMsb, int nLsb)
Definition: verCore.c:587
Ver_ParsePrintErrorMessage
void Ver_ParsePrintErrorMessage(Ver_Man_t *p)
Definition: verCore.c:278
assert
#define assert(ex)
Definition: util_old.h:213
int Ver_ParseSignalPrefix ( Ver_Man_t *  pMan,
char **  ppWord,
int *  pnMsb,
int *  pnLsb 
)

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

Synopsis [Determine signal prefix of the form [Beg:End].]

Description []

SideEffects []

SeeAlso []

Definition at line 635 of file verCore.c.

636 {
637  char * pWord = *ppWord, * pTemp;
638  int nMsb, nLsb;
639  assert( pWord[0] == '[' );
640  // get the beginning
641  nMsb = atoi( pWord + 1 );
642  // find the splitter
643  while ( *pWord && *pWord != ':' && *pWord != ']' )
644  pWord++;
645  if ( *pWord == 0 )
646  {
647  sprintf( pMan->sError, "Cannot find closing bracket in this line." );
648  Ver_ParsePrintErrorMessage( pMan );
649  return 0;
650  }
651  if ( *pWord == ']' )
652  nLsb = nMsb;
653  else
654  {
655  assert( *pWord == ':' );
656  nLsb = atoi( pWord + 1 );
657  // find the closing paranthesis
658  while ( *pWord && *pWord != ']' )
659  pWord++;
660  if ( *pWord == 0 )
661  {
662  sprintf( pMan->sError, "Cannot find closing bracket in this line." );
663  Ver_ParsePrintErrorMessage( pMan );
664  return 0;
665  }
666  assert( *pWord == ']' );
667  pWord++;
668 
669  // fix the case when <name> follows after [] without space
670  if ( *pWord == '\\' )
671  {
672  pWord++;
673  pTemp = pWord;
674  while ( *pTemp && *pTemp != ' ' )
675  pTemp++;
676  if ( *pTemp == ' ' )
677  *pTemp = 0;
678  }
679  }
680  assert( nMsb >= 0 && nLsb >= 0 );
681  // return
682  *ppWord = pWord;
683  *pnMsb = nMsb;
684  *pnLsb = nLsb;
685  return 1;
686 }
sprintf
char * sprintf()
Ver_ParsePrintErrorMessage
void Ver_ParsePrintErrorMessage(Ver_Man_t *p)
Definition: verCore.c:278
assert
#define assert(ex)
Definition: util_old.h:213
int Ver_ParseSignalSuffix ( Ver_Man_t *  pMan,
char *  pWord,
int *  pnMsb,
int *  pnLsb 
)

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

Synopsis [Determine signal suffix of the form [m:n].]

Description []

SideEffects []

SeeAlso []

Definition at line 699 of file verCore.c.

700 {
701  char * pCur;
702  int Length;
703  Length = strlen(pWord);
704  assert( pWord[Length-1] == ']' );
705  // walk backward
706  for ( pCur = pWord + Length - 2; pCur != pWord; pCur-- )
707  if ( *pCur == ':' || *pCur == '[' )
708  break;
709  if ( pCur == pWord )
710  {
711  sprintf( pMan->sError, "Cannot find opening bracket in signal name %s.", pWord );
712  Ver_ParsePrintErrorMessage( pMan );
713  return 0;
714  }
715  if ( *pCur == '[' )
716  {
717  *pnMsb = *pnLsb = atoi(pCur+1);
718  *pCur = 0;
719  return 1;
720  }
721  assert( *pCur == ':' );
722  // get the end of the interval
723  *pnLsb = atoi(pCur+1);
724  // find the beginning
725  for ( pCur = pWord + Length - 2; pCur != pWord; pCur-- )
726  if ( *pCur == '[' )
727  break;
728  if ( pCur == pWord )
729  {
730  sprintf( pMan->sError, "Cannot find opening bracket in signal name %s.", pWord );
731  Ver_ParsePrintErrorMessage( pMan );
732  return 0;
733  }
734  assert( *pCur == '[' );
735  // get the beginning of the interval
736  *pnMsb = atoi(pCur+1);
737  // cut the word
738  *pCur = 0;
739  return 1;
740 }
sprintf
char * sprintf()
Ver_ParsePrintErrorMessage
void Ver_ParsePrintErrorMessage(Ver_Man_t *p)
Definition: verCore.c:278
assert
#define assert(ex)
Definition: util_old.h:213
strlen
int strlen()
Ver_Man_t * Ver_ParseStart ( char *  pFileName,
Abc_Des_t *  pGateLib 
)
static

FUNCTION DEFINITIONS ///.

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

Synopsis [Start parser.]

Description []

SideEffects []

SeeAlso []

Definition at line 104 of file verCore.c.

105 {
106  Ver_Man_t * p;
107  p = ABC_ALLOC( Ver_Man_t, 1 );
108  memset( p, 0, sizeof(Ver_Man_t) );
109  p->pFileName = pFileName;
110  p->pReader = Ver_StreamAlloc( pFileName );
111  if ( p->pReader == NULL )
112  {
113  ABC_FREE( p );
114  return NULL;
115  }
116  p->Output = stdout;
117  p->vNames = Vec_PtrAlloc( 100 );
118  p->vStackFn = Vec_PtrAlloc( 100 );
119  p->vStackOp = Vec_IntAlloc( 100 );
120  p->vPerm = Vec_IntAlloc( 100 );
121  // create the design library and assign the technology library
122  p->pDesign = Abc_DesCreate( pFileName );
123  p->pDesign->pLibrary = pGateLib;
124  // derive library from SCL
125 // if ( Abc_FrameReadLibScl() )
126 // Abc_SclInstallGenlib( Abc_FrameReadLibScl(), 0, 0, 0 );
127  p->pDesign->pGenlib = Abc_FrameReadLibGen();
128  return p;
129 }
memset
char * memset()
Abc_FrameReadLibGen
ABC_DLL void * Abc_FrameReadLibGen()
Definition: mainFrame.c:56
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Abc_DesCreate
ABC_DLL Abc_Des_t * Abc_DesCreate(char *pName)
DECLARATIONS ///.
Definition: abcLib.c:45
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Ver_Man_t
typedefABC_NAMESPACE_HEADER_START struct Ver_Man_t_ Ver_Man_t
INCLUDES ///.
Definition: ver.h:45
Abc_Des_t_::pGenlib
void * pGenlib
Definition: abc.h:226
Vec_PtrAlloc
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Ver_StreamAlloc
Ver_Stream_t * Ver_StreamAlloc(char *pFileName)
FUNCTION DEFINITIONS ///.
Definition: verStream.c:74
void Ver_ParseStop ( Ver_Man_t *  p)
static

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

Synopsis [Stop parser.]

Description []

SideEffects []

SeeAlso []

Definition at line 142 of file verCore.c.

143 {
144  if ( p->pProgress )
145  Extra_ProgressBarStop( p->pProgress );
146  Ver_StreamFree( p->pReader );
147  Vec_PtrFree( p->vNames );
148  Vec_PtrFree( p->vStackFn );
149  Vec_IntFree( p->vStackOp );
150  Vec_IntFree( p->vPerm );
151  ABC_FREE( p );
152 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Extra_ProgressBarStop
void Extra_ProgressBarStop(ProgressBar *p)
Definition: extraUtilProgress.c:118
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Ver_StreamFree
void Ver_StreamFree(Ver_Stream_t *p)
Definition: verStream.c:157
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
Vec_PtrFree
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223

Variable Documentation

int glo_fMapped = 0

Definition at line 80 of file verCore.c.