src/base/ver/verCore.c File Reference

#include "ver.h"
#include "mio.h"
#include "main.h"
Include dependency graph for verCore.c:

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
}
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_tVer_ParseStart (char *pFileName, Abc_Lib_t *pGateLib)
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_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_tVer_ParseCreatePi (Abc_Ntk_t *pNtk, char *pName)
static Abc_Obj_tVer_ParseCreatePo (Abc_Ntk_t *pNtk, char *pName)
static Abc_Obj_tVer_ParseCreateLatch (Abc_Ntk_t *pNtk, Abc_Obj_t *pNetLI, Abc_Obj_t *pNetLO)
static Abc_Obj_tVer_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_Lib_tVer_ParseFile (char *pFileName, Abc_Lib_t *pGateLib, int fCheck, int fUseMemMan)
void Ver_ParsePrintErrorMessage (Ver_Man_t *p)
Abc_Ntk_tVer_ParseFindOrCreateNetwork (Ver_Man_t *pMan, char *pName)
Abc_Obj_tVer_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_tVer_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_tVer_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 78 of file verCore.c.


Enumeration Type Documentation

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 40 of file verCore.c.

00040              { 
00041     VER_GATE_AND = 0,
00042     VER_GATE_OR,
00043     VER_GATE_XOR,
00044     VER_GATE_BUF,
00045     VER_GATE_NAND,
00046     VER_GATE_NOR,
00047     VER_GATE_XNOR,
00048     VER_GATE_NOT
00049 } Ver_GateType_t;

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

] DECLARATIONS ///

Enumerator:
VER_SIG_NONE 
VER_SIG_INPUT 
VER_SIG_OUTPUT 
VER_SIG_INOUT 
VER_SIG_REG 
VER_SIG_WIRE 

Definition at line 30 of file verCore.c.

00030              { 
00031     VER_SIG_NONE = 0,
00032     VER_SIG_INPUT,
00033     VER_SIG_OUTPUT,
00034     VER_SIG_INOUT,
00035     VER_SIG_REG,
00036     VER_SIG_WIRE
00037 } Ver_SignalType_t;


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 1378 of file verCore.c.

01379 {
01380     Mio_Pin_t * pGatePin;
01381     int i;
01382     for ( i = 0, pGatePin = Mio_GateReadPins(pGate); pGatePin != NULL; pGatePin = Mio_PinReadNext(pGatePin), i++ )
01383         if ( strcmp(pName, Mio_PinReadName(pGatePin)) == 0 )
01384             return i;
01385     if ( strcmp(pName, Mio_GateReadOutName(pGate)) == 0 )
01386         return i;
01387     return -1;
01388 }

static int Ver_NtkIsDefined ( Abc_Ntk_t pNtkBox  )  [inline, static]

Definition at line 73 of file verCore.c.

00073 { assert( pNtkBox->pName );     return Abc_NtkPiNum(pNtkBox) || Abc_NtkPoNum(pNtkBox);  }

static int Ver_ObjIsConnected ( Abc_Obj_t pObj  )  [inline, static]

Definition at line 74 of file verCore.c.

00074 { assert( Abc_ObjIsBox(pObj) ); return Abc_ObjFaninNum(pObj) || Abc_ObjFanoutNum(pObj); }

int Ver_ParseAlways ( Ver_Man_t pMan,
Abc_Ntk_t pNtk 
) [static]

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

Synopsis [Parses one directive.]

Description []

SideEffects []

SeeAlso []

Definition at line 859 of file verCore.c.

00860 {
00861     Ver_Stream_t * p = pMan->pReader;
00862     Abc_Obj_t * pNet, * pNet2;
00863     int fStopAfterOne;
00864     char * pWord, * pWord2;
00865     char Symbol;
00866     // parse the directive 
00867     pWord = Ver_ParseGetName( pMan );
00868     if ( pWord == NULL )
00869         return 0;
00870     if ( pWord[0] == '@' )
00871     {
00872         Ver_StreamSkipToChars( p, ")" );
00873         Ver_StreamPopChar(p);
00874         // parse the directive 
00875         pWord = Ver_ParseGetName( pMan );
00876         if ( pWord == NULL )
00877             return 0;
00878     }
00879     // decide how many statements to parse
00880     fStopAfterOne = 0;
00881     if ( strcmp( pWord, "begin" ) )
00882         fStopAfterOne = 1;
00883     // iterate over the initial states
00884     while ( 1 )
00885     {
00886         if ( !fStopAfterOne )
00887         {
00888             // get the name of the output signal
00889             pWord = Ver_ParseGetName( pMan );
00890             if ( pWord == NULL )
00891                 return 0;
00892             // look for the end of directive
00893             if ( !strcmp( pWord, "end" ) )
00894                 break;
00895         }
00896         // get the fanout net
00897         pNet = Ver_ParseFindNet( pNtk, pWord );
00898         if ( pNet == NULL )
00899         {
00900             sprintf( pMan->sError, "Cannot read the always statement for %s (output wire is not defined).", pWord );
00901             Ver_ParsePrintErrorMessage( pMan );
00902             return 0;
00903         }
00904         // get the equality sign
00905         Symbol = Ver_StreamPopChar(p);
00906         if ( Symbol != '<' && Symbol != '=' )
00907         {
00908             sprintf( pMan->sError, "Cannot read the assign statement for %s (expected <= or =).", pWord );
00909             Ver_ParsePrintErrorMessage( pMan );
00910             return 0;
00911         }
00912         if ( Symbol == '<' )
00913             Ver_StreamPopChar(p);
00914         // skip the comments
00915         if ( !Ver_ParseSkipComments( pMan ) )
00916             return 0;
00917         // get the second name
00918         pWord2 = Ver_ParseGetName( pMan );
00919         if ( pWord2 == NULL )
00920             return 0;
00921         // check if the name is complemented
00922         if ( pWord2[0] == '~' )
00923         {
00924             pNet2 = Ver_ParseFindNet( pNtk, pWord2+1 );
00925             pNet2 = Ver_ParseCreateInv( pNtk, pNet2 );
00926         }
00927         else
00928             pNet2 = Ver_ParseFindNet( pNtk, pWord2 );
00929         if ( pNet2 == NULL )
00930         {
00931             sprintf( pMan->sError, "Cannot read the always statement for %s (input wire is not defined).", pWord2 );
00932             Ver_ParsePrintErrorMessage( pMan );
00933             return 0;
00934         }
00935         // create the latch
00936         Ver_ParseCreateLatch( pNtk, pNet2, pNet );
00937         // remove the last symbol
00938         Symbol = Ver_StreamPopChar(p);
00939         assert( Symbol == ';' );
00940         // quit if only one directive
00941         if ( fStopAfterOne )
00942             break;
00943     }
00944     return 1;
00945 }

int Ver_ParseAssign ( Ver_Man_t pMan,
Abc_Ntk_t pNtk 
) [static]

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

Synopsis [Parses one directive.]

Description []

SideEffects []

SeeAlso []

Definition at line 1054 of file verCore.c.

01055 {
01056     char Buffer[1000], Buffer2[1000];
01057     Ver_Stream_t * p = pMan->pReader;
01058     Abc_Obj_t * pNode, * pNet;
01059     char * pWord, * pName, * pEquation;
01060     Hop_Obj_t * pFunc;
01061     char Symbol;
01062     int i, Bit, Limit, Length, fReduction;
01063     int nMsb, nLsb;
01064 
01065 //    if ( Ver_StreamGetLineNumber(p) == 2756 )
01066 //    {
01067 //        int x = 0;
01068 //    }
01069 
01070     // convert from the blackbox into the network with local functions representated by AIGs
01071     if ( !Ver_ParseConvertNetwork( pMan, pNtk, pMan->fMapped ) )
01072         return 0;
01073 
01074     while ( 1 )
01075     {
01076         // get the name of the output signal
01077         pWord = Ver_ParseGetName( pMan );
01078         if ( pWord == NULL )
01079             return 0;
01080         // check for vector-inputs
01081         if ( !Ver_ParseLookupSuffix( pMan, pWord, &nMsb, &nLsb ) )
01082             return 0;
01083         // handle special case of constant assignment
01084         if ( nMsb >= 0 && nLsb >= 0 )
01085         {
01086             // save the fanout name
01087             strcpy( Buffer, pWord );
01088             // get the equality sign
01089             if ( Ver_StreamPopChar(p) != '=' )
01090             {
01091                 sprintf( pMan->sError, "Cannot read the assign statement for %s (expected equality sign).", pWord );
01092                 Ver_ParsePrintErrorMessage( pMan );
01093                 return 0;
01094             }
01095             // get the constant
01096             pWord = Ver_ParseGetName( pMan );
01097             if ( pWord == NULL )
01098                 return 0;
01099             // check if it is indeed a constant
01100             if ( !(pWord[0] >= '0' && pWord[0] <= '9') )
01101             {
01102                 sprintf( pMan->sError, "Currently can only assign vector-signal \"%s\" to be a constant.", Buffer );
01103                 Ver_ParsePrintErrorMessage( pMan );
01104                 return 0;
01105             }
01106 
01107             // get individual bits of the constant
01108             if ( !Ver_ParseConstant( pMan, pWord ) )
01109                 return 0;
01110             // check that the constant has the same size
01111             Limit = nMsb > nLsb? nMsb - nLsb + 1: nLsb - nMsb + 1;
01112             if ( Limit != Vec_PtrSize(pMan->vNames) )
01113             {
01114                 sprintf( pMan->sError, "The constant size (%d) is different from the signal\"%s\" size (%d).", 
01115                     Vec_PtrSize(pMan->vNames), Buffer, Limit );
01116                 Ver_ParsePrintErrorMessage( pMan );
01117                 return 0;
01118             }
01119             // iterate through the bits
01120             for ( i = 0, Bit = nLsb; i < Limit; i++, Bit = nMsb > nLsb ? Bit + 1: Bit - 1  )
01121             {
01122                 // get the fanin net
01123                 if ( Vec_PtrEntry( pMan->vNames, Limit-1-i ) )
01124                     pNet = Ver_ParseFindNet( pNtk, "1\'b1" );
01125                 else
01126                     pNet = Ver_ParseFindNet( pNtk, "1\'b0" );
01127                 assert( pNet != NULL );
01128 
01129                 // create the buffer
01130                 pNode = Abc_NtkCreateNodeBuf( pNtk, pNet );
01131 
01132                 // get the fanout net
01133                 sprintf( Buffer2, "%s[%d]", Buffer, Bit );
01134                 pNet = Ver_ParseFindNet( pNtk, Buffer2 );
01135                 if ( pNet == NULL )
01136                 {
01137                     sprintf( pMan->sError, "Cannot read the assign statement for %s (output wire is not defined).", pWord );
01138                     Ver_ParsePrintErrorMessage( pMan );
01139                     return 0;
01140                 }
01141                 Abc_ObjAddFanin( pNet, pNode );
01142             }
01143             // go to the end of the line
01144             Ver_ParseSkipComments( pMan );
01145         }
01146         else
01147         {
01148             // consider the case of reduction operations
01149             fReduction = 0;
01150             if ( pWord[0] == '{' && !pMan->fNameLast )
01151                 fReduction = 1;
01152             if ( fReduction )
01153             {
01154                 pWord++;
01155                 pWord[strlen(pWord)-1] = 0;
01156                 assert( pWord[0] != '\\' );
01157             }
01158             // get the fanout net
01159             pNet = Ver_ParseFindNet( pNtk, pWord );
01160             if ( pNet == NULL )
01161             {
01162                 sprintf( pMan->sError, "Cannot read the assign statement for %s (output wire is not defined).", pWord );
01163                 Ver_ParsePrintErrorMessage( pMan );
01164                 return 0;
01165             }
01166             // get the equality sign
01167             if ( Ver_StreamPopChar(p) != '=' )
01168             {
01169                 sprintf( pMan->sError, "Cannot read the assign statement for %s (expected equality sign).", pWord );
01170                 Ver_ParsePrintErrorMessage( pMan );
01171                 return 0;
01172             }
01173             // skip the comments
01174             if ( !Ver_ParseSkipComments( pMan ) )
01175                 return 0;
01176             // get the second name
01177             if ( fReduction )
01178                 pEquation = Ver_StreamGetWord( p, ";" );
01179             else
01180                 pEquation = Ver_StreamGetWord( p, ",;" );
01181             if ( pEquation == NULL )
01182             {
01183                 sprintf( pMan->sError, "Cannot read the equation for %s.", Abc_ObjName(pNet) );
01184                 Ver_ParsePrintErrorMessage( pMan );
01185                 return 0;
01186             }
01187 
01188             // consider the case of mapped network
01189             Vec_PtrClear( pMan->vNames );
01190             if ( pMan->fMapped )
01191             {
01192                 if ( !strcmp( pEquation, "1\'b0" ) )
01193                     pFunc = (Hop_Obj_t *)Mio_LibraryReadConst0(Abc_FrameReadLibGen());
01194                 else if ( !strcmp( pEquation, "1\'b1" ) )
01195                     pFunc = (Hop_Obj_t *)Mio_LibraryReadConst1(Abc_FrameReadLibGen());
01196                 else
01197                 {
01198                     // "assign foo = \bar ;"
01199                     if ( *pEquation == '\\' )
01200                     {
01201                         pEquation++;
01202                         pEquation[strlen(pEquation) - 1] = 0;
01203                     }
01204                     if ( Ver_ParseFindNet(pNtk, pEquation) == NULL )
01205                     {
01206                         sprintf( pMan->sError, "Cannot read Verilog with non-trivial assignments in the mapped netlist." );
01207                         Ver_ParsePrintErrorMessage( pMan );
01208                         return 0;
01209                     }
01210                     Vec_PtrPush( pMan->vNames, (void *)strlen(pEquation) );
01211                     Vec_PtrPush( pMan->vNames, pEquation );
01212                     // get the buffer
01213                     pFunc = (Hop_Obj_t *)Mio_LibraryReadBuf(Abc_FrameReadLibGen());
01214                     if ( pFunc == NULL )
01215                     {
01216                         sprintf( pMan->sError, "Reading assign statement for node %s has failed because the genlib library has no buffer.", Abc_ObjName(pNet) );
01217                         Ver_ParsePrintErrorMessage( pMan );
01218                         return 0;
01219                     }
01220                 }
01221             }
01222             else
01223             {
01224                 if ( !strcmp(pEquation, "0") || !strcmp(pEquation, "1\'b0") || !strcmp(pEquation, "1\'bx") )
01225                     pFunc = Hop_ManConst0(pNtk->pManFunc);
01226                 else if ( !strcmp(pEquation, "1") || !strcmp(pEquation, "1\'b1") )
01227                     pFunc = Hop_ManConst1(pNtk->pManFunc);
01228                 else if ( fReduction )
01229                     pFunc = Ver_FormulaReduction( pEquation, pNtk->pManFunc, pMan->vNames, pMan->sError );  
01230                 else
01231                     pFunc = Ver_FormulaParser( pEquation, pNtk->pManFunc, pMan->vNames, pMan->vStackFn, pMan->vStackOp, pMan->sError );  
01232                 if ( pFunc == NULL )
01233                 {
01234                     Ver_ParsePrintErrorMessage( pMan );
01235                     return 0;
01236                 }
01237             }
01238 
01239             // create the node with the given inputs
01240             pNode = Abc_NtkCreateNode( pNtk );
01241             pNode->pData = pFunc;
01242             Abc_ObjAddFanin( pNet, pNode );
01243             // connect to fanin nets
01244             for ( i = 0; i < Vec_PtrSize(pMan->vNames)/2; i++ )
01245             {
01246                 // get the name of this signal
01247                 Length = (int)Vec_PtrEntry( pMan->vNames, 2*i );
01248                 pName  = Vec_PtrEntry( pMan->vNames, 2*i + 1 );
01249                 pName[Length] = 0;
01250                 // find the corresponding net
01251                 pNet = Ver_ParseFindNet( pNtk, pName );
01252                 if ( pNet == NULL )
01253                 {
01254                     sprintf( pMan->sError, "Cannot read the assign statement for %s (input wire %s is not defined).", pWord, pName );
01255                     Ver_ParsePrintErrorMessage( pMan );
01256                     return 0;
01257                 }
01258                 Abc_ObjAddFanin( pNode, pNet );
01259             }
01260         }
01261 
01262         Symbol = Ver_StreamPopChar(p);
01263         if ( Symbol == ',' )
01264             continue;
01265         if ( Symbol == ';' )
01266             return 1;
01267     }
01268     return 1;
01269 }

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 2676 of file verCore.c.

02677 {
02678     Abc_Ntk_t * pNtk;
02679     Ver_Bundle_t * pBundle;
02680     Vec_Ptr_t * vUndefs;
02681     int i, RetValue, Counter, nMaxBoxSize;
02682 
02683     // print the log file
02684     if ( pMan->pDesign->vModules && Vec_PtrSize(pMan->pDesign->vModules) > 1 )
02685         Ver_ParsePrintLog( pMan );
02686 
02687     // connect defined boxes
02688     RetValue = Ver_ParseConnectDefBoxes( pMan );
02689     if ( RetValue < 2 )
02690         return RetValue;
02691 
02692     // report the boxes
02693     Ver_ParseReportUndefBoxes( pMan );
02694 
02695     // collect undef box types and their actual instances
02696     vUndefs = Ver_ParseCollectUndefBoxes( pMan );
02697     assert( Vec_PtrSize( vUndefs ) > 0 );
02698 
02699     // go through all undef box types
02700     Counter = 0;
02701     nMaxBoxSize = Ver_ParseMaxBoxSize( vUndefs );
02702     while ( Ver_ParseCheckNondrivenNets(vUndefs) && Counter < nMaxBoxSize )
02703     {
02704         // go through undef box types
02705         pBundle = NULL;
02706         Vec_PtrForEachEntry( vUndefs, pNtk, i )
02707             if ( pBundle = Ver_ParseGetNondrivenBundle( pNtk, Counter ) )
02708                 break;
02709         if ( pBundle == NULL )
02710         {
02711             Counter++;
02712             continue;
02713         }
02714         // drive this bundle by this box
02715         if ( !Ver_ParseDriveFormal( pMan, pNtk, pBundle ) )
02716             return 0;
02717     }
02718 
02719     // make all the remaining bundles the drivers of undefs
02720     if ( !Ver_ParseDriveInputs( pMan, vUndefs ) )
02721         return 0;
02722 
02723     // cleanup
02724     Vec_PtrForEachEntry( vUndefs, pNtk, i )
02725     {
02726         Vec_PtrFree( pNtk->pData );
02727         pNtk->pData = NULL;
02728     }
02729     Vec_PtrFree( vUndefs ); 
02730     return 1;
02731 }

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 1573 of file verCore.c.

01574 {
01575     char Buffer[1000];
01576     Ver_Stream_t * p = pMan->pReader;
01577     Ver_Bundle_t * pBundle;
01578     Vec_Ptr_t * vBundles;
01579     Abc_Obj_t * pNetActual; 
01580     Abc_Obj_t * pNode;
01581     char * pWord, Symbol;
01582     int fCompl, fFormalIsGiven;
01583     int i, k, Bit, Limit, nMsb, nLsb, fQuit, flag;
01584 
01585     // gate the name of the box
01586     pWord = Ver_ParseGetName( pMan );
01587     if ( pWord == NULL )
01588         return 0;
01589 
01590     // create a box with this name
01591     pNode = Abc_NtkCreateBlackbox( pNtk );
01592     pNode->pData = pNtkBox;
01593     Abc_ObjAssignName( pNode, pWord, NULL );
01594 
01595     // continue parsing the box
01596     if ( Ver_StreamPopChar(p) != '(' )
01597     {
01598         sprintf( pMan->sError, "Cannot parse box %s (expected opening paranthesis).", Abc_ObjName(pNode) );
01599         Ver_ParsePrintErrorMessage( pMan );
01600         return 0;
01601     }
01602     Ver_ParseSkipComments( pMan );
01603  
01604     // parse pairs of formal/actual inputs
01605     vBundles = Vec_PtrAlloc( 16 );
01606     pNode->pCopy = (Abc_Obj_t *)vBundles;
01607     while ( 1 )
01608     {
01609         // allocate the bundle (formal name + array of actual nets)
01610         pBundle = ALLOC( Ver_Bundle_t, 1 );
01611         pBundle->pNameFormal = NULL;
01612         pBundle->vNetsActual = Vec_PtrAlloc( 4 );
01613         Vec_PtrPush( vBundles, pBundle );
01614 
01615         // process one pair of formal/actual parameters
01616         fFormalIsGiven = 0;
01617         if ( Ver_StreamScanChar(p) == '.' )
01618         {
01619             fFormalIsGiven = 1;
01620             if ( Ver_StreamPopChar(p) != '.' )
01621             {
01622                 sprintf( pMan->sError, "Cannot parse box %s (expected .).", Abc_ObjName(pNode) );
01623                 Ver_ParsePrintErrorMessage( pMan );
01624                 return 0;
01625             }
01626 
01627             // parse the formal name
01628             pWord = Ver_ParseGetName( pMan );
01629             if ( pWord == NULL )
01630                 return 0;
01631 
01632             // save the name
01633             pBundle->pNameFormal = Extra_UtilStrsav( pWord );
01634 
01635             // open the paranthesis
01636             if ( Ver_StreamPopChar(p) != '(' )
01637             {
01638                 sprintf( pMan->sError, "Cannot formal parameter %s of box %s (expected opening paranthesis).", pWord, Abc_ObjName(pNode));
01639                 Ver_ParsePrintErrorMessage( pMan );
01640                 return 0;
01641             }
01642             Ver_ParseSkipComments( pMan );
01643         }
01644 
01645         // check if this is the beginning of {} expression
01646         Symbol = Ver_StreamScanChar(p);
01647 
01648         // consider the case of vector-inputs
01649         if ( Symbol == '{' )
01650         {
01651             // skip this char
01652             Ver_StreamPopChar(p);
01653 
01654             // read actual names
01655             i = 0;
01656             fQuit = 0;
01657             while ( 1 )
01658             {
01659                 // parse the formal name
01660                 Ver_ParseSkipComments( pMan );
01661                 pWord = Ver_ParseGetName( pMan );
01662                 if ( pWord == NULL )
01663                     return 0;
01664 
01665                 // check if the last char is a closing brace
01666                 if ( pWord[strlen(pWord)-1] == '}' )
01667                 {
01668                     pWord[strlen(pWord)-1] = 0;
01669                     fQuit = 1;
01670                 }
01671                 if ( pWord[0] == 0 )
01672                     break;
01673 
01674                 // check for constant
01675                 if ( pWord[0] >= '1' && pWord[0] <= '9' )
01676                 {
01677                     if ( !Ver_ParseConstant( pMan, pWord ) )
01678                         return 0;
01679                     // add constant MSB to LSB
01680                     for ( k = 0; k < Vec_PtrSize(pMan->vNames); k++, i++ )
01681                     {
01682                         // get the actual net
01683                         sprintf( Buffer, "1\'b%d", (int)(Vec_PtrEntry(pMan->vNames,k) != NULL) );
01684                         pNetActual = Ver_ParseFindNet( pNtk, Buffer );
01685                         if ( pNetActual == NULL )
01686                         {
01687                             sprintf( pMan->sError, "Actual net \"%s\" is missing in gate \"%s\".", Buffer, Abc_ObjName(pNode) );
01688                             Ver_ParsePrintErrorMessage( pMan );
01689                             return 0;
01690                         }
01691                         Vec_PtrPush( pBundle->vNetsActual, pNetActual );
01692                     }
01693                 }
01694                 else
01695                 {
01696                     // get the suffix of the form [m:n]
01697                     if ( pWord[strlen(pWord)-1] == ']' && !pMan->fNameLast )
01698                         Ver_ParseSignalSuffix( pMan, pWord, &nMsb, &nLsb );
01699                     else
01700                         Ver_ParseLookupSuffix( pMan, pWord, &nMsb, &nLsb );
01701 
01702                     // generate signals
01703                     if ( nMsb == -1 && nLsb == -1 )
01704                     {
01705                         // get the actual net
01706                         pNetActual = Ver_ParseFindNet( pNtk, pWord );
01707                         if ( pNetActual == NULL )
01708                         {
01709                             if ( !strncmp(pWord, "Open_", 5) ||
01710                                 !strncmp(pWord, "dct_unconnected", 15) ) 
01711                                 pNetActual = Abc_NtkCreateNet( pNtk );
01712                             else
01713                             {
01714                                 sprintf( pMan->sError, "Actual net \"%s\" is missing in box \"%s\".", pWord, Abc_ObjName(pNode) );
01715                                 Ver_ParsePrintErrorMessage( pMan );
01716                                 return 0;
01717                             }
01718                         }
01719                         Vec_PtrPush( pBundle->vNetsActual, pNetActual );
01720                         i++;
01721                     }
01722                     else
01723                     {
01724                         // go from MSB to LSB
01725                         assert( nMsb >= 0 && nLsb >= 0 );
01726                         Limit = (nMsb > nLsb) ? nMsb - nLsb + 1: nLsb - nMsb + 1;  
01727                         for ( Bit = nMsb, k = Limit - 1; k >= 0; Bit = (nMsb > nLsb ? Bit - 1: Bit + 1), k--, i++ )
01728                         {
01729                             // get the actual net
01730                             sprintf( Buffer, "%s[%d]", pWord, Bit );
01731                             pNetActual = Ver_ParseFindNet( pNtk, Buffer );
01732                             if ( pNetActual == NULL )
01733                             {
01734                                 if ( !strncmp(pWord, "Open_", 5) ||
01735                                     !strncmp(pWord, "dct_unconnected", 15) ) 
01736                                     pNetActual = Abc_NtkCreateNet( pNtk );
01737                                 else
01738                                 {
01739                                     sprintf( pMan->sError, "Actual net \"%s\" is missing in box \"%s\".", pWord, Abc_ObjName(pNode) );
01740                                     Ver_ParsePrintErrorMessage( pMan );
01741                                     return 0;
01742                                 }
01743                             }
01744                             Vec_PtrPush( pBundle->vNetsActual, pNetActual );
01745                         }
01746                     }
01747                 }
01748 
01749                 if ( fQuit )
01750                     break;
01751 
01752                 // skip comma
01753                 Ver_ParseSkipComments( pMan );
01754                 Symbol = Ver_StreamPopChar(p);
01755                 if ( Symbol == '}' )
01756                     break;
01757                 if ( Symbol != ',' )
01758                 {
01759                     sprintf( pMan->sError, "Cannot parse formal parameter %s of gate %s (expected comma).", pWord, Abc_ObjName(pNode) );
01760                     Ver_ParsePrintErrorMessage( pMan );
01761                     return 0;
01762                 }
01763             }
01764         }
01765         else
01766         {
01767             // get the next word
01768             pWord = Ver_ParseGetName( pMan );
01769             if ( pWord == NULL )
01770                 return 0;
01771             // consider the case of empty name
01772             fCompl = 0;
01773             if ( pWord[0] == 0 )
01774             {
01775                 pNetActual = Abc_NtkCreateNet( pNtk );
01776                         Vec_PtrPush( pBundle->vNetsActual, Abc_ObjNotCond( pNetActual, fCompl ) );
01777             }
01778             else
01779             {
01780                 // get the actual net
01781                 flag=0;
01782                 pNetActual = Ver_ParseFindNet( pNtk, pWord );
01783                 if ( pNetActual == NULL ) 
01784                 {
01785                     Ver_ParseLookupSuffix( pMan, pWord, &nMsb, &nLsb );
01786                     if ( nMsb == -1 && nLsb == -1 ) 
01787                     {
01788                         Ver_ParseSignalSuffix( pMan, pWord, &nMsb, &nLsb );
01789                         if ( nMsb == -1 && nLsb == -1 ) 
01790                         {
01791                             if ( !strncmp(pWord, "Open_", 5) ||
01792                                 !strncmp(pWord, "dct_unconnected", 15) ) 
01793                             {
01794                                 pNetActual = Abc_NtkCreateNet( pNtk );
01795                                 Vec_PtrPush( pBundle->vNetsActual, pNetActual );
01796                             } 
01797                             else 
01798                             {
01799                                 sprintf( pMan->sError, "Actual net \"%s\" is missing in box \"%s\".", pWord, Abc_ObjName(pNode) );
01800                                 Ver_ParsePrintErrorMessage( pMan );
01801                                 return 0;
01802                             }
01803                         } 
01804                         else 
01805                         {
01806                             flag=1;
01807                         }
01808                     } 
01809                     else 
01810                     {
01811                         flag=1;
01812                     }
01813                     if (flag) 
01814                     {
01815                         Limit = (nMsb > nLsb) ? nMsb - nLsb + 1: nLsb - nMsb + 1;  
01816                         for ( Bit = nMsb, k = Limit - 1; k >= 0; Bit = (nMsb > nLsb ? Bit - 1: Bit + 1), k--)
01817                         {
01818                             // get the actual net
01819                             sprintf( Buffer, "%s[%d]", pWord, Bit );
01820                             pNetActual = Ver_ParseFindNet( pNtk, Buffer );
01821                             if ( pNetActual == NULL )
01822                             {
01823                                 if ( !strncmp(pWord, "Open_", 5) ||
01824                                     !strncmp(pWord, "dct_unconnected", 15)) 
01825                                     pNetActual = Abc_NtkCreateNet( pNtk );
01826                                 else
01827                                 {
01828                                     sprintf( pMan->sError, "Actual net \"%s\" is missing in box \"%s\".", pWord, Abc_ObjName(pNode) );
01829                                     Ver_ParsePrintErrorMessage( pMan );
01830                                     return 0;
01831                                 }
01832                             }
01833                             Vec_PtrPush( pBundle->vNetsActual, pNetActual );
01834                         }
01835                     }
01836                 } 
01837                 else 
01838                 {
01839                     Vec_PtrPush( pBundle->vNetsActual, Abc_ObjNotCond( pNetActual, fCompl ) );
01840                 }
01841             }
01842         }
01843 
01844         if ( fFormalIsGiven )
01845         {
01846             // close the paranthesis
01847             Ver_ParseSkipComments( pMan );
01848             if ( Ver_StreamPopChar(p) != ')' )
01849             {
01850                 sprintf( pMan->sError, "Cannot parse formal parameter %s of box %s (expected closing paranthesis).", pWord, Abc_ObjName(pNode) );
01851                 Ver_ParsePrintErrorMessage( pMan );
01852                 return 0;
01853             }
01854             Ver_ParseSkipComments( pMan );
01855         }
01856 
01857         // check if it is the end of gate
01858         Symbol = Ver_StreamPopChar(p);
01859         if ( Symbol == ')' )
01860             break;
01861         // skip comma
01862         if ( Symbol != ',' )
01863         {
01864             sprintf( pMan->sError, "Cannot parse formal parameter %s of box %s (expected comma).", pWord, Abc_ObjName(pNode) );
01865             Ver_ParsePrintErrorMessage( pMan );
01866             return 0;
01867         }
01868         Ver_ParseSkipComments( pMan );
01869     }
01870 
01871     // check if it is the end of gate
01872     Ver_ParseSkipComments( pMan );
01873     if ( Ver_StreamPopChar(p) != ';' )
01874     {
01875         sprintf( pMan->sError, "Cannot read box %s (expected closing semicolumn).", Abc_ObjName(pNode) );
01876         Ver_ParsePrintErrorMessage( pMan );
01877         return 0;
01878     }
01879 
01880     return 1;
01881 }

int Ver_ParseCheckNondrivenNets ( Vec_Ptr_t vUndefs  ) 

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 2249 of file verCore.c.

02250 {
02251     Abc_Ntk_t * pNtk;
02252     Ver_Bundle_t * pBundle;
02253     Abc_Obj_t * pBox, * pNet;
02254     int i, k, j, m;
02255     // go through undef box types
02256     Vec_PtrForEachEntry( vUndefs, pNtk, i )
02257         // go through instances of this type
02258         Vec_PtrForEachEntry( pNtk->pData, pBox, k )
02259             // go through the bundles of this instance
02260             Vec_PtrForEachEntryReverse( (Vec_Ptr_t *)pBox->pCopy, pBundle, j )
02261                 // go through the actual nets of this bundle
02262                 if ( pBundle )
02263                 Vec_PtrForEachEntry( pBundle->vNetsActual, pNet, m )
02264                 {
02265                     char * pName = Abc_ObjName(pNet);
02266                     if ( Abc_ObjFaninNum(pNet) == 0 ) // non-driven
02267                         if ( strcmp(Abc_ObjName(pNet), "1\'b0") && strcmp(Abc_ObjName(pNet), "1\'b1") ) // diff from a const
02268                             return 1;
02269                 }
02270     return 0;
02271 }

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 2165 of file verCore.c.

02166 {
02167     Vec_Ptr_t * vUndefs;
02168     Abc_Ntk_t * pNtk, * pNtkBox;
02169     Abc_Obj_t * pBox;
02170     int i, k;
02171     // clear the module structures
02172     Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i )
02173         pNtk->pData = NULL;
02174     // go through all the blackboxes
02175     vUndefs = Vec_PtrAlloc( 16 );
02176     Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i )
02177     {
02178         Abc_NtkForEachBlackbox( pNtk, pBox, k )
02179         {
02180             pNtkBox = pBox->pData;
02181             if ( pNtkBox == NULL )
02182                 continue;
02183             if ( Ver_NtkIsDefined(pNtkBox) )
02184                 continue;
02185             if ( pNtkBox->pData == NULL )
02186             {
02187                 // save the box
02188                 Vec_PtrPush( vUndefs, pNtkBox );
02189                 pNtkBox->pData = Vec_PtrAlloc( 16 );
02190             }
02191             // save the instance
02192             Vec_PtrPush( pNtkBox->pData, pBox );
02193         }
02194     }
02195     return vUndefs;
02196 }

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 1912 of file verCore.c.

01913 {
01914     Vec_Ptr_t * vBundles = (Vec_Ptr_t *)pBox->pCopy;
01915     Abc_Ntk_t * pNtk = pBox->pNtk;
01916     Abc_Ntk_t * pNtkBox = pBox->pData;
01917     Abc_Obj_t * pTerm, * pTermNew, * pNetAct;
01918     Ver_Bundle_t * pBundle;
01919     char * pNameFormal;
01920     int i, k, j, iBundle, Length;
01921 
01922     assert( !Ver_ObjIsConnected(pBox) );
01923     assert( Ver_NtkIsDefined(pNtkBox) );
01924     assert( !Abc_NtkHasBlackbox(pNtkBox) || Abc_NtkBoxNum(pNtkBox) == 1 );
01925 /*
01926     // clean the PI/PO nets
01927     Abc_NtkForEachPi( pNtkBox, pTerm, i )
01928         Abc_ObjFanout0(pTerm)->pCopy = NULL;
01929     Abc_NtkForEachPo( pNtkBox, pTerm, i )
01930         Abc_ObjFanin0(pTerm)->pCopy = NULL;
01931 */
01932     // check if some of them do not have formal names
01933     Vec_PtrForEachEntry( vBundles, pBundle, k )
01934         if ( pBundle->pNameFormal == NULL )
01935             break;
01936     if ( k < Vec_PtrSize(vBundles) )
01937     {
01938         printf( "Warning: The instance %s of network %s will be connected without using formal names.\n", pNtkBox->pName, Abc_ObjName(pBox) );
01939         // add all actual nets in the bundles
01940         iBundle = 0;
01941         Vec_PtrForEachEntry( vBundles, pBundle, j )
01942             iBundle += Vec_PtrSize(pBundle->vNetsActual);
01943 
01944         // check the number of actual nets is the same as the number of formal nets
01945         if ( iBundle != Abc_NtkPiNum(pNtkBox) + Abc_NtkPoNum(pNtkBox) )
01946         {
01947             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.", 
01948                 Vec_PtrSize(vBundles), Abc_NtkPiNum(pNtkBox) + Abc_NtkPoNum(pNtkBox), pNtkBox->pName, Abc_ObjName(pBox) );
01949             Ver_ParsePrintErrorMessage( pMan );
01950             return 0;
01951         }
01952         // connect bundles in the natural order
01953         iBundle = 0;
01954         Abc_NtkForEachPi( pNtkBox, pTerm, i )
01955         {
01956             pBundle = Vec_PtrEntry( vBundles, iBundle++ );
01957             // the bundle is found - add the connections - using order LSB to MSB
01958             Vec_PtrForEachEntryReverse( pBundle->vNetsActual, pNetAct, k )
01959             {
01960                 pTermNew = Abc_NtkCreateBi( pNtk );
01961                 Abc_ObjAddFanin( pBox, pTermNew );
01962                 Abc_ObjAddFanin( pTermNew, pNetAct );
01963                 i++;
01964             }
01965             i--;
01966         }
01967         // create fanins of the box
01968         Abc_NtkForEachPo( pNtkBox, pTerm, i )
01969         {
01970             pBundle = Vec_PtrEntry( vBundles, iBundle++ );
01971             // the bundle is found - add the connections - using order LSB to MSB
01972             Vec_PtrForEachEntryReverse( pBundle->vNetsActual, pNetAct, k )
01973             {
01974                 pTermNew = Abc_NtkCreateBo( pNtk );
01975                 Abc_ObjAddFanin( pTermNew, pBox );
01976                 Abc_ObjAddFanin( pNetAct, pTermNew );
01977                 i++;
01978             }
01979             i--;
01980         }
01981 
01982         // free the bundling
01983         Vec_PtrForEachEntry( vBundles, pBundle, k )
01984             Ver_ParseFreeBundle( pBundle );
01985         Vec_PtrFree( vBundles );
01986         pBox->pCopy = NULL;
01987         return 1;
01988     }
01989 
01990     // bundles arrive in any order - but inside each bundle the order is MSB to LSB
01991     // make sure every formal PI has a corresponding net
01992     Abc_NtkForEachPi( pNtkBox, pTerm, i )
01993     {
01994         // get the name of this formal net
01995         pNameFormal = Abc_ObjName( Abc_ObjFanout0(pTerm) );
01996         // try to find the bundle with this formal net
01997         pBundle = NULL;
01998         Vec_PtrForEachEntry( vBundles, pBundle, k )
01999             if ( !strcmp(pBundle->pNameFormal, pNameFormal) )
02000                 break;
02001         assert( pBundle != NULL );
02002         // if the bundle is not found, try without parantheses
02003         if ( k == Vec_PtrSize(vBundles) )
02004         {
02005             pBundle = NULL;
02006             Length = strlen(pNameFormal);
02007             if ( pNameFormal[Length-1] == ']' )
02008             {
02009                 // find the opening brace
02010                 for ( Length--; Length >= 0; Length-- )
02011                     if ( pNameFormal[Length] == '[' )
02012                         break;
02013                 // compare names before brace
02014                 if ( Length > 0 )
02015                 {
02016                     Vec_PtrForEachEntry( vBundles, pBundle, j )
02017                         if ( !strncmp(pBundle->pNameFormal, pNameFormal, Length) )
02018                             break;
02019                     if ( j == Vec_PtrSize(vBundles) )
02020                         pBundle = NULL;
02021                 }
02022             }
02023             if ( pBundle == NULL )
02024             {
02025                 sprintf( pMan->sError, "Cannot find an actual net for the formal net %s when instantiating network %s in box %s.", 
02026                     pNameFormal, pNtkBox->pName, Abc_ObjName(pBox) );
02027                 Ver_ParsePrintErrorMessage( pMan );
02028                 return 0;
02029             }
02030         }
02031         // the bundle is found - add the connections - using order LSB to MSB
02032         Vec_PtrForEachEntryReverse( pBundle->vNetsActual, pNetAct, k )
02033         {
02034             pTermNew = Abc_NtkCreateBi( pNtk );
02035             Abc_ObjAddFanin( pBox, pTermNew );
02036             Abc_ObjAddFanin( pTermNew, pNetAct );
02037             i++;
02038         }
02039         i--;
02040     }
02041 
02042     // connect those formal POs that do have nets
02043     Abc_NtkForEachPo( pNtkBox, pTerm, i )
02044     {
02045         // get the name of this PI
02046         pNameFormal = Abc_ObjName( Abc_ObjFanin0(pTerm) );
02047         // try to find this formal net in the bundle
02048         pBundle = NULL;
02049         Vec_PtrForEachEntry( vBundles, pBundle, k )
02050             if ( !strcmp(pBundle->pNameFormal, pNameFormal) )
02051                 break;
02052         assert( pBundle != NULL );
02053         // if the name is not found, try without parantheses
02054         if ( k == Vec_PtrSize(vBundles) )
02055         {
02056             pBundle = NULL;
02057             Length = strlen(pNameFormal);
02058             if ( pNameFormal[Length-1] == ']' )
02059             {
02060                 // find the opening brace
02061                 for ( Length--; Length >= 0; Length-- )
02062                     if ( pNameFormal[Length] == '[' )
02063                         break;
02064                 // compare names before brace
02065                 if ( Length > 0 )
02066                 {
02067                     Vec_PtrForEachEntry( vBundles, pBundle, j )
02068                         if ( !strncmp(pBundle->pNameFormal, pNameFormal, Length) )
02069                             break;
02070                     if ( j == Vec_PtrSize(vBundles) )
02071                         pBundle = NULL;
02072                 }
02073             }
02074             if ( pBundle == NULL )
02075             {
02076 //                printf( "Warning: The formal output %s is not driven when instantiating network %s in box %s.", 
02077 //                    pNameFormal, pNtkBox->pName, Abc_ObjName(pBox) );
02078                 continue;
02079             }
02080         }
02081         // the bundle is found - add the connections
02082         Vec_PtrForEachEntryReverse( pBundle->vNetsActual, pNetAct, k )
02083         {
02084             if ( !strcmp(Abc_ObjName(pNetAct), "1\'b0") || !strcmp(Abc_ObjName(pNetAct), "1\'b1") )
02085             {
02086                 sprintf( pMan->sError, "It looks like formal output %s is driving a constant net (%s) when instantiating network %s in box %s.", 
02087                     pBundle->pNameFormal, Abc_ObjName(pNetAct), pNtkBox->pName, Abc_ObjName(pBox) );
02088                 Ver_ParsePrintErrorMessage( pMan );
02089                 return 0;
02090             }
02091             pTermNew = Abc_NtkCreateBo( pNtk );
02092             Abc_ObjAddFanin( pTermNew, pBox );
02093             Abc_ObjAddFanin( pNetAct, pTermNew );
02094             i++;
02095         }
02096         i--;
02097     }
02098 
02099     // free the bundling
02100     Vec_PtrForEachEntry( vBundles, pBundle, k )
02101         Ver_ParseFreeBundle( pBundle );
02102     Vec_PtrFree( vBundles );
02103     pBox->pCopy = NULL;
02104     return 1;
02105 }

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 2119 of file verCore.c.

02120 {
02121     Abc_Ntk_t * pNtk;
02122     Abc_Obj_t * pBox;
02123     int i, k, RetValue = 1;
02124     // go through all the modules
02125     Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i )
02126     {
02127         // go through all the boxes of this module
02128         Abc_NtkForEachBox( pNtk, pBox, k )
02129         {
02130             if ( Abc_ObjIsLatch(pBox) )
02131                 continue;
02132             // skip internal boxes of the blackboxes
02133             if ( pBox->pData == NULL )
02134                 continue;
02135             // if the network is undefined, it will be connected later
02136             if ( !Ver_NtkIsDefined(pBox->pData) )
02137             {
02138                 RetValue = 2;
02139                 continue;
02140             }
02141             // connect the box
02142             if ( !Ver_ParseConnectBox( pMan, pBox ) )
02143                 return 0;
02144             // if the network is a true blackbox, skip
02145             if ( Abc_NtkHasBlackbox(pBox->pData) )
02146                 continue;
02147             // convert the box to the whitebox
02148             Abc_ObjBlackboxToWhitebox( pBox );
02149         }
02150     }
02151     return RetValue;
02152 }

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 727 of file verCore.c.

00728 {
00729     int nBits, i;
00730     assert( pWord[0] >= '1' && pWord[1] <= '9' );
00731     nBits = atoi(pWord);
00732     // find the next symbol \'
00733     while ( *pWord && *pWord != '\'' )
00734         pWord++;
00735     if ( *pWord == 0 )
00736     {
00737         sprintf( pMan->sError, "Cannot find symbol \' in the constant." );
00738         Ver_ParsePrintErrorMessage( pMan );
00739         return 0;
00740     }
00741     assert( *pWord == '\'' );
00742     pWord++;
00743     if ( *pWord != 'b' )
00744     {
00745         sprintf( pMan->sError, "Currently can only handle binary constants." );
00746         Ver_ParsePrintErrorMessage( pMan );
00747         return 0;
00748     }
00749     pWord++;
00750     // scan the bits
00751     Vec_PtrClear( pMan->vNames );
00752     for ( i = 0; i < nBits; i++ )
00753     {
00754       if ( pWord[i] != '0' && pWord[i] != '1' && pWord[i] != 'x' )
00755       {
00756          sprintf( pMan->sError, "Having problem parsing the binary constant." );
00757          Ver_ParsePrintErrorMessage( pMan );
00758          return 0;
00759       }
00760       if ( pWord[i] == 'x' ) 
00761           Vec_PtrPush( pMan->vNames, (void *)0 );
00762       else 
00763           Vec_PtrPush( pMan->vNames, (void *)(pWord[i]-'0') );
00764     }
00765     return 1;
00766 }

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 341 of file verCore.c.

00342 {
00343     if ( fMapped )
00344     {
00345         // convert from the blackbox into the network with local functions representated by AIGs
00346         if ( pNtk->ntkFunc == ABC_FUNC_BLACKBOX )
00347         {
00348             // change network type
00349             assert( pNtk->pManFunc == NULL );
00350             pNtk->ntkFunc = ABC_FUNC_MAP;
00351             pNtk->pManFunc = pMan->pDesign->pGenlib;
00352         }
00353         else if ( pNtk->ntkFunc != ABC_FUNC_MAP )
00354         {
00355             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 );
00356             Ver_ParsePrintErrorMessage( pMan );
00357             return 0;
00358         }
00359     }
00360     else
00361     {
00362         // convert from the blackbox into the network with local functions representated by AIGs
00363         if ( pNtk->ntkFunc == ABC_FUNC_BLACKBOX )
00364         {
00365             // change network type
00366             assert( pNtk->pManFunc == NULL );
00367             pNtk->ntkFunc = ABC_FUNC_AIG;
00368             pNtk->pManFunc = pMan->pDesign->pManFunc;
00369         }
00370         else if ( pNtk->ntkFunc != ABC_FUNC_AIG )
00371         {
00372             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 );
00373             Ver_ParsePrintErrorMessage( pMan );
00374             return 0;
00375         }
00376     }
00377     return 1;
00378 }

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 2826 of file verCore.c.

02827 {
02828     Abc_Obj_t * pObj;
02829     pObj = Abc_NtkCreateNodeInv( pNtk, pNet );
02830     pNet = Abc_NtkCreateNet( pNtk );
02831     Abc_ObjAddFanin( pNet, pObj );
02832     return pNet;
02833 }

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 2795 of file verCore.c.

02796 {
02797     Abc_Obj_t * pLatch, * pTerm;
02798     // add the BO terminal
02799     pTerm = Abc_NtkCreateBi( pNtk );
02800     Abc_ObjAddFanin( pTerm, pNetLI );
02801     // add the latch box
02802     pLatch = Abc_NtkCreateLatch( pNtk );
02803     Abc_ObjAddFanin( pLatch, pTerm  );
02804     // add the BI terminal
02805     pTerm = Abc_NtkCreateBo( pNtk );
02806     Abc_ObjAddFanin( pTerm, pLatch );
02807     // get the LO net
02808     Abc_ObjAddFanin( pNetLO, pTerm );
02809     // set latch name
02810     Abc_ObjAssignName( pLatch, Abc_ObjName(pNetLO), "L" );
02811     Abc_LatchSetInitDc( pLatch );
02812     return pLatch;
02813 }

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 2745 of file verCore.c.

02746 {
02747     Abc_Obj_t * pNet, * pTerm;
02748     // get the PI net
02749 //    pNet  = Ver_ParseFindNet( pNtk, pName );
02750 //    if ( pNet )
02751 //        printf( "Warning: PI \"%s\" appears twice in the list.\n", pName );
02752     pNet  = Abc_NtkFindOrCreateNet( pNtk, pName );
02753     // add the PI node
02754     pTerm = Abc_NtkCreatePi( pNtk );
02755     Abc_ObjAddFanin( pNet, pTerm );
02756     return pTerm;
02757 }

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 2770 of file verCore.c.

02771 {
02772     Abc_Obj_t * pNet, * pTerm;
02773     // get the PO net
02774 //    pNet  = Ver_ParseFindNet( pNtk, pName );
02775 //    if ( pNet && Abc_ObjFaninNum(pNet) == 0 )
02776 //        printf( "Warning: PO \"%s\" appears twice in the list.\n", pName );
02777     pNet  = Abc_NtkFindOrCreateNet( pNtk, pName );
02778     // add the PO node
02779     pTerm = Abc_NtkCreatePo( pNtk );
02780     Abc_ObjAddFanin( pTerm, pNet );
02781     return pTerm;
02782 }

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 2351 of file verCore.c.

02352 {
02353     char Buffer[200];
02354     char * pName;
02355     Ver_Bundle_t * pBundle;
02356     Abc_Obj_t * pBox, * pTerm, * pTermNew, * pNetAct, * pNetFormal;
02357     int k, j, m;
02358 
02359     // drive this net in the undef box
02360     Vec_PtrForEachEntry( pBundle0->vNetsActual, pNetAct, m )
02361     {
02362         // create the formal net
02363         if ( Vec_PtrSize(pBundle0->vNetsActual) == 1 )
02364             sprintf( Buffer, "%s", pBundle0->pNameFormal );
02365         else
02366             sprintf( Buffer, "%s[%d]", pBundle0->pNameFormal, m );
02367         assert( Abc_NtkFindNet( pNtk, Buffer ) == NULL );
02368         pNetFormal = Abc_NtkFindOrCreateNet( pNtk, Buffer );
02369         // connect it to the box
02370         pTerm = Abc_NtkCreateBo( pNtk );
02371         assert( Abc_NtkBoxNum(pNtk) <= 1 );
02372         pBox = Abc_NtkBoxNum(pNtk)? Abc_NtkBox(pNtk,0) : Abc_NtkCreateBlackbox(pNtk);
02373         Abc_ObjAddFanin( Abc_NtkCreatePo(pNtk), pNetFormal );
02374         Abc_ObjAddFanin( pNetFormal, pTerm );
02375         Abc_ObjAddFanin( pTerm, pBox );
02376     }
02377 
02378     // go through instances of this type
02379     pName = Extra_UtilStrsav(pBundle0->pNameFormal);
02380     Vec_PtrForEachEntry( pNtk->pData, pBox, k )
02381     {
02382         // find a bundle with the given name in this instance
02383         Vec_PtrForEachEntryReverse( (Vec_Ptr_t *)pBox->pCopy, pBundle, j )
02384             if ( pBundle && !strcmp( pBundle->pNameFormal, pName ) )
02385                 break;
02386         // skip non-driven bundles
02387         if ( j == Vec_PtrSize((Vec_Ptr_t *)pBox->pCopy) )
02388             continue;
02389         // check if any nets are driven in this bundle
02390         Vec_PtrForEachEntry( pBundle->vNetsActual, pNetAct, m )
02391             if ( Abc_ObjFaninNum(pNetAct) > 0 )
02392             {
02393                 sprintf( pMan->sError, "Internal error while trying to connect undefined boxes. It is likely that the algorithm currently used has its limitations." );
02394                 Ver_ParsePrintErrorMessage( pMan );
02395                 return 0;
02396             }
02397         // drive the nets by the undef box
02398         Vec_PtrForEachEntryReverse( pBundle->vNetsActual, pNetAct, m )
02399         {
02400             pTermNew = Abc_NtkCreateBo( pNetAct->pNtk );
02401             Abc_ObjAddFanin( pTermNew, pBox );
02402             Abc_ObjAddFanin( pNetAct, pTermNew );
02403         }
02404         // remove the bundle
02405         Ver_ParseFreeBundle( pBundle );
02406         Vec_PtrWriteEntry( (Vec_Ptr_t *)pBox->pCopy, j, NULL );
02407     }
02408     free( pName );
02409     return 1;
02410 }

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 2424 of file verCore.c.

02425 {
02426     char Buffer[200];
02427     Ver_Bundle_t * pBundle;
02428     Abc_Ntk_t * pNtk;
02429     Abc_Obj_t * pBox, * pBox2, * pTerm, * pTermNew, * pNetFormal, * pNetAct;
02430     int i, k, j, m, CountCur, CountTotal = -1;
02431     // iterate through the undef boxes
02432     Vec_PtrForEachEntry( vUndefs, pNtk, i )
02433     {
02434         // count the number of unconnected bundles for instances of this type of box
02435         CountTotal = -1;
02436         Vec_PtrForEachEntry( pNtk->pData, pBox, k )
02437         {
02438             CountCur = 0;
02439             Vec_PtrForEachEntry( (Vec_Ptr_t *)pBox->pCopy, pBundle, j )
02440                 CountCur += (pBundle != NULL);
02441             if ( CountTotal == -1 )
02442                 CountTotal = CountCur;
02443             else if ( CountTotal != CountCur )
02444             {
02445                 sprintf( pMan->sError, "The number of formal inputs (%d) is different from the expected one (%d) when instantiating network %s in box %s.", 
02446                     CountCur, CountTotal, pNtk->pName, Abc_ObjName(pBox) );
02447                 Ver_ParsePrintErrorMessage( pMan );
02448                 return 0;
02449             }
02450         }
02451 
02452         // create formals
02453         pBox = Vec_PtrEntry( pNtk->pData, 0 );
02454         Vec_PtrForEachEntry( (Vec_Ptr_t *)pBox->pCopy, pBundle, j )
02455         {
02456             if ( pBundle == NULL )
02457                 continue;
02458             Vec_PtrForEachEntry( pBundle->vNetsActual, pNetAct, m )
02459             {
02460                 // find create the formal net
02461                 if ( Vec_PtrSize(pBundle->vNetsActual) == 1 )
02462                     sprintf( Buffer, "%s", pBundle->pNameFormal );
02463                 else
02464                     sprintf( Buffer, "%s[%d]", pBundle->pNameFormal, m );
02465                 assert( Abc_NtkFindNet( pNtk, Buffer ) == NULL );
02466                 pNetFormal = Abc_NtkFindOrCreateNet( pNtk, Buffer );
02467                 // connect
02468                 pTerm = Abc_NtkCreateBi( pNtk );
02469                 assert( Abc_NtkBoxNum(pNtk) <= 1 );
02470                 pBox2 = Abc_NtkBoxNum(pNtk)? Abc_NtkBox(pNtk,0) : Abc_NtkCreateBlackbox(pNtk);
02471                 Abc_ObjAddFanin( pNetFormal, Abc_NtkCreatePi(pNtk) );
02472                 Abc_ObjAddFanin( pTerm, pNetFormal );
02473                 Abc_ObjAddFanin( pBox2, pTerm );
02474             }
02475         }
02476 
02477         // go through all the boxes
02478         Vec_PtrForEachEntry( pNtk->pData, pBox, k )
02479         {
02480             // go through all the bundles
02481             Vec_PtrForEachEntry( (Vec_Ptr_t *)pBox->pCopy, pBundle, j )
02482             {
02483                 if ( pBundle == NULL )
02484                     continue;
02485                 // drive the nets by the undef box
02486                 Vec_PtrForEachEntryReverse( pBundle->vNetsActual, pNetAct, m )
02487                 {
02488                     pTermNew = Abc_NtkCreateBi( pNetAct->pNtk );
02489                     Abc_ObjAddFanin( pBox, pTermNew );
02490                     Abc_ObjAddFanin( pTermNew, pNetAct );
02491                 }
02492                 // remove the bundle
02493                 Ver_ParseFreeBundle( pBundle );
02494                 Vec_PtrWriteEntry( (Vec_Ptr_t *)pBox->pCopy, j, NULL );
02495             }
02496 
02497             // free the bundles
02498             Vec_PtrFree( (Vec_Ptr_t *)pBox->pCopy );
02499             pBox->pCopy = NULL;
02500         }
02501     }
02502     return 1;
02503 }

Abc_Lib_t* Ver_ParseFile ( char *  pFileName,
Abc_Lib_t pGateLib,
int  fCheck,
int  fUseMemMan 
)

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

Synopsis [File parser.]

Description []

SideEffects []

SeeAlso []

Definition at line 155 of file verCore.c.

00156 {
00157     Ver_Man_t * p;
00158     Abc_Lib_t * pDesign;
00159     // start the parser
00160     p = Ver_ParseStart( pFileName, pGateLib );
00161     p->fMapped    = glo_fMapped;
00162     p->fCheck     = fCheck;
00163     p->fUseMemMan = fUseMemMan;
00164     if ( glo_fMapped )
00165     {
00166         Hop_ManStop(p->pDesign->pManFunc);
00167         p->pDesign->pManFunc = NULL;
00168     }
00169     // parse the file
00170     Ver_ParseInternal( p );
00171     // save the result
00172     pDesign = p->pDesign;
00173     p->pDesign = NULL;
00174     // stop the parser
00175     Ver_ParseStop( p );
00176     return pDesign;
00177 }

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 318 of file verCore.c.

00319 {
00320     Abc_Obj_t * pObj;
00321     if ( pObj = Abc_NtkFindNet(pNtk, pName) )
00322         return pObj;
00323     if ( !strcmp( pName, "1\'b0" ) || !strcmp( pName, "1\'bx" ) )
00324         return Abc_NtkFindOrCreateNet( pNtk, "1\'b0" );
00325     if ( !strcmp( pName, "1\'b1" ) )
00326         return Abc_NtkFindOrCreateNet( pNtk, "1\'b1" );
00327     return NULL;
00328 }

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 291 of file verCore.c.

00292 {
00293     Abc_Ntk_t * pNtkNew;
00294     // check if the network exists
00295     if ( pNtkNew = Abc_LibFindModelByName( pMan->pDesign, pName ) )
00296         return pNtkNew;
00297 //printf( "Creating network %s.\n", pName );
00298     // create new network
00299     pNtkNew = Abc_NtkAlloc( ABC_NTK_NETLIST, ABC_FUNC_BLACKBOX, pMan->fUseMemMan );
00300     pNtkNew->pName = Extra_UtilStrsav( pName );
00301     pNtkNew->pSpec = NULL;
00302     // add module to the design
00303     Abc_LibAddModel( pMan->pDesign, pNtkNew );
00304     return pNtkNew;
00305 }

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 2284 of file verCore.c.

02285 {
02286     Ver_Bundle_t * pBundle;
02287     Abc_Obj_t * pBox, * pNet;
02288     int k, j, m;
02289     // go through instances of this type
02290     Vec_PtrForEachEntry( pNtk->pData, pBox, k )
02291     {
02292         // find a bundle with the given name in this instance
02293         Vec_PtrForEachEntryReverse( (Vec_Ptr_t *)pBox->pCopy, pBundle, j )
02294             if ( pBundle && !strcmp( pBundle->pNameFormal, pNameFormal ) )
02295                 break;
02296         // skip non-driven bundles
02297         if ( j == Vec_PtrSize((Vec_Ptr_t *)pBox->pCopy) )
02298             continue;
02299         // check if all nets are driven in this bundle
02300         Vec_PtrForEachEntry( pBundle->vNetsActual, pNet, m )
02301             if ( Abc_ObjFaninNum(pNet) > 0 )
02302                 return 1;
02303     }
02304     return 0;
02305 }

void Ver_ParseFreeBundle ( Ver_Bundle_t pBundle  ) 

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

Synopsis [Connects one box to the network]

Description []

SideEffects []

SeeAlso []

Definition at line 1894 of file verCore.c.

01895 {
01896     FREE( pBundle->pNameFormal );
01897     Vec_PtrFree( pBundle->vNetsActual );
01898     free( pBundle );
01899 }

void Ver_ParseFreeData ( Ver_Man_t p  )  [static]

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

Synopsis [File parser.]

Description []

SideEffects []

SeeAlso []

Definition at line 248 of file verCore.c.

00249 {
00250     if ( p->pDesign )
00251     {
00252         Abc_LibFree( p->pDesign, NULL );
00253         p->pDesign = NULL;
00254     }
00255 }

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 1401 of file verCore.c.

01402 {
01403     Ver_Stream_t * p = pMan->pReader;
01404     Abc_Obj_t * pNetActual, * pNode;
01405     char * pWord, Symbol;
01406     int Input, i, nFanins = Mio_GateReadInputs(pGate);
01407 
01408     // convert from the blackbox into the network with local functions representated by gates
01409     if ( 1 != pMan->fMapped )
01410     {
01411         sprintf( pMan->sError, "The network appears to be mapped. Use \"r -m\" to read mapped Verilog." );
01412         Ver_ParsePrintErrorMessage( pMan );
01413         return 0;
01414     }
01415 
01416     // update the network type if needed
01417     if ( !Ver_ParseConvertNetwork( pMan, pNtk, 1 ) )
01418         return 0;
01419 
01420     // parse the directive and set the pointers to the PIs/POs of the gate
01421     pWord = Ver_ParseGetName( pMan );
01422     if ( pWord == NULL )
01423         return 0;
01424     // this is gate name - throw it away
01425     if ( Ver_StreamPopChar(p) != '(' )
01426     {
01427         sprintf( pMan->sError, "Cannot parse gate %s (expected opening paranthesis).", Mio_GateReadName(pGate) );
01428         Ver_ParsePrintErrorMessage( pMan );
01429         return 0;
01430     }
01431     Ver_ParseSkipComments( pMan );
01432 
01433     // start the node
01434     pNode = Abc_NtkCreateNode( pNtk );
01435     pNode->pData = pGate;
01436 
01437     // parse pairs of formal/actural inputs
01438     Vec_IntClear( pMan->vPerm );
01439     while ( 1 )
01440     {
01441         // process one pair of formal/actual parameters
01442         if ( Ver_StreamPopChar(p) != '.' )
01443         {
01444             sprintf( pMan->sError, "Cannot parse gate %s (expected .).", Mio_GateReadName(pGate) );
01445             Ver_ParsePrintErrorMessage( pMan );
01446             return 0;
01447         }
01448 
01449         // parse the formal name
01450         pWord = Ver_ParseGetName( pMan );
01451         if ( pWord == NULL )
01452             return 0;
01453 
01454         // find the corresponding pin of the gate
01455         Input = Ver_FindGateInput( pGate, pWord );
01456         if ( Input == -1 )
01457         {
01458             sprintf( pMan->sError, "Formal input name %s cannot be found in the gate %s.", pWord, Mio_GateReadOutName(pGate) );
01459             Ver_ParsePrintErrorMessage( pMan );
01460             return 0;
01461         }
01462 
01463         // open the paranthesis
01464         if ( Ver_StreamPopChar(p) != '(' )
01465         {
01466             sprintf( pMan->sError, "Cannot formal parameter %s of gate %s (expected opening paranthesis).", pWord, Mio_GateReadName(pGate) );
01467             Ver_ParsePrintErrorMessage( pMan );
01468             return 0;
01469         }
01470 
01471         // parse the actual name
01472         pWord = Ver_ParseGetName( pMan );
01473         if ( pWord == NULL )
01474             return 0;
01475         // check if the name is complemented
01476         assert( pWord[0] != '~' );
01477 /*
01478         fCompl = (pWord[0] == '~');
01479         if ( fCompl )
01480         {
01481             fComplUsed = 1;
01482             pWord++;
01483             if ( pNtk->pData == NULL )
01484                 pNtk->pData = Extra_MmFlexStart();
01485         }
01486 */
01487         // get the actual net
01488         pNetActual = Ver_ParseFindNet( pNtk, pWord );
01489         if ( pNetActual == NULL )
01490         {
01491             sprintf( pMan->sError, "Actual net %s is missing.", pWord );
01492             Ver_ParsePrintErrorMessage( pMan );
01493             return 0;
01494         }
01495 
01496         // close the paranthesis
01497         if ( Ver_StreamPopChar(p) != ')' )
01498         {
01499             sprintf( pMan->sError, "Cannot formal parameter %s of gate %s (expected closing paranthesis).", pWord, Mio_GateReadName(pGate) );
01500             Ver_ParsePrintErrorMessage( pMan );
01501             return 0;
01502         }
01503 
01504         // add the fanin
01505         if ( Input < nFanins )
01506         {
01507             Vec_IntPush( pMan->vPerm, Input );
01508             Abc_ObjAddFanin( pNode, pNetActual ); // fanin
01509         }
01510         else
01511             Abc_ObjAddFanin( pNetActual, pNode ); // fanout
01512 
01513         // check if it is the end of gate
01514         Ver_ParseSkipComments( pMan );
01515         Symbol = Ver_StreamPopChar(p);
01516         if ( Symbol == ')' )
01517             break;
01518 
01519         // skip comma
01520         if ( Symbol != ',' )
01521         {
01522             sprintf( pMan->sError, "Cannot formal parameter %s of gate %s (expected closing paranthesis).", pWord, Mio_GateReadName(pGate) );
01523             Ver_ParsePrintErrorMessage( pMan );
01524             return 0;
01525         }
01526         Ver_ParseSkipComments( pMan );
01527     }
01528 
01529     // check that the gate as the same number of input
01530     if ( !(Abc_ObjFaninNum(pNode) == nFanins && Abc_ObjFanoutNum(pNode) == 1) )
01531     {
01532         sprintf( pMan->sError, "Parsing of gate %s has failed.", Mio_GateReadName(pGate) );
01533         Ver_ParsePrintErrorMessage( pMan );
01534         return 0;
01535     }
01536 
01537     // check if it is the end of gate
01538     Ver_ParseSkipComments( pMan );
01539     if ( Ver_StreamPopChar(p) != ';' )
01540     {
01541         sprintf( pMan->sError, "Cannot read gate %s (expected closing semicolumn).", Mio_GateReadName(pGate) );
01542         Ver_ParsePrintErrorMessage( pMan );
01543         return 0;
01544     }
01545     
01546     // check if we need to permute the inputs
01547     Vec_IntForEachEntry( pMan->vPerm, Input, i )
01548         if ( Input != i )
01549             break;
01550     if ( i < Vec_IntSize(pMan->vPerm) )
01551     {
01552         // add the fanin numnbers to the end of the permuation array
01553         for ( i = 0; i < nFanins; i++ )
01554             Vec_IntPush( pMan->vPerm, Abc_ObjFaninId(pNode, i) );
01555         // write the fanin numbers into their corresponding places (according to the gate) 
01556         for ( i = 0; i < nFanins; i++ )
01557             Vec_IntWriteEntry( &pNode->vFanins, Vec_IntEntry(pMan->vPerm, i), Vec_IntEntry(pMan->vPerm, i+nFanins) );
01558     }
01559     return 1;
01560 }

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 1282 of file verCore.c.

01283 {
01284     Ver_Stream_t * p = pMan->pReader;
01285     Abc_Obj_t * pNet, * pNode;
01286     char * pWord, Symbol;
01287 
01288     // convert from the blackbox into the network with local functions representated by AIGs
01289     if ( !Ver_ParseConvertNetwork( pMan, pNtk, pMan->fMapped ) )
01290         return 0;
01291 
01292     // this is gate name - throw it away
01293     if ( Ver_StreamPopChar(p) != '(' )
01294     {
01295         sprintf( pMan->sError, "Cannot parse a standard gate (expected opening paranthesis)." );
01296         Ver_ParsePrintErrorMessage( pMan );
01297         return 0;
01298     }
01299     Ver_ParseSkipComments( pMan );
01300 
01301     // create the node
01302     pNode = Abc_NtkCreateNode( pNtk );
01303 
01304     // parse pairs of formal/actural inputs
01305     while ( 1 )
01306     {
01307         // parse the output name
01308         pWord = Ver_ParseGetName( pMan );
01309         if ( pWord == NULL )
01310             return 0;
01311         // get the net corresponding to this output
01312         pNet = Ver_ParseFindNet( pNtk, pWord );
01313         if ( pNet == NULL )
01314         {
01315             sprintf( pMan->sError, "Net is missing in gate %s.", pWord );
01316             Ver_ParsePrintErrorMessage( pMan );
01317             return 0;
01318         }
01319         // if this is the first net, add it as an output
01320         if ( Abc_ObjFanoutNum(pNode) == 0 )
01321             Abc_ObjAddFanin( pNet, pNode );
01322         else
01323             Abc_ObjAddFanin( pNode, pNet );
01324         // check if it is the end of gate
01325         Ver_ParseSkipComments( pMan );
01326         Symbol = Ver_StreamPopChar(p);
01327         if ( Symbol == ')' )
01328             break;
01329         // skip comma
01330         if ( Symbol != ',' )
01331         {
01332             sprintf( pMan->sError, "Cannot parse a standard gate %s (expected closing paranthesis).", Abc_ObjName(Abc_ObjFanout0(pNode)) );
01333             Ver_ParsePrintErrorMessage( pMan );
01334             return 0;
01335         }
01336         Ver_ParseSkipComments( pMan );
01337     }
01338     if ( (GateType == VER_GATE_BUF || GateType == VER_GATE_NOT) && Abc_ObjFaninNum(pNode) != 1 )
01339     {
01340         sprintf( pMan->sError, "Buffer or interver with multiple fanouts %s (currently not supported).", Abc_ObjName(Abc_ObjFanout0(pNode)) );
01341         Ver_ParsePrintErrorMessage( pMan );
01342         return 0;
01343     }
01344 
01345     // check if it is the end of gate
01346     Ver_ParseSkipComments( pMan );
01347     if ( Ver_StreamPopChar(p) != ';' )
01348     {
01349         sprintf( pMan->sError, "Cannot read standard gate %s (expected closing semicolumn).", Abc_ObjName(Abc_ObjFanout0(pNode)) );
01350         Ver_ParsePrintErrorMessage( pMan );
01351         return 0;
01352     }
01353     // add logic function
01354     if ( GateType == VER_GATE_AND || GateType == VER_GATE_NAND )
01355         pNode->pData = Hop_CreateAnd( pNtk->pManFunc, Abc_ObjFaninNum(pNode) );
01356     else if ( GateType == VER_GATE_OR || GateType == VER_GATE_NOR )
01357         pNode->pData = Hop_CreateOr( pNtk->pManFunc, Abc_ObjFaninNum(pNode) );
01358     else if ( GateType == VER_GATE_XOR || GateType == VER_GATE_XNOR )
01359         pNode->pData = Hop_CreateExor( pNtk->pManFunc, Abc_ObjFaninNum(pNode) );
01360     else if ( GateType == VER_GATE_BUF || GateType == VER_GATE_NOT )
01361         pNode->pData = Hop_CreateAnd( pNtk->pManFunc, Abc_ObjFaninNum(pNode) );
01362     if ( GateType == VER_GATE_NAND || GateType == VER_GATE_NOR || GateType == VER_GATE_XNOR || GateType == VER_GATE_NOT )
01363         pNode->pData = Hop_Not( pNode->pData );
01364     return 1;
01365 }

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 2318 of file verCore.c.

02319 {
02320     Ver_Bundle_t * pBundle;
02321     Abc_Obj_t * pBox, * pNet;
02322     int k, m;
02323     // go through instances of this type
02324     Vec_PtrForEachEntry( pNtk->pData, pBox, k )
02325     {
02326         if ( Counter >= Vec_PtrSize((Vec_Ptr_t *)pBox->pCopy) )
02327             continue;
02328         // get the bundle given distance away
02329         pBundle = Vec_PtrEntry( (Vec_Ptr_t *)pBox->pCopy, Vec_PtrSize((Vec_Ptr_t *)pBox->pCopy) - 1 - Counter );
02330         if ( pBundle == NULL )
02331             continue;
02332         // go through the actual nets of this bundle
02333         Vec_PtrForEachEntry( pBundle->vNetsActual, pNet, m )
02334             if ( !Abc_ObjFaninNum(pNet) && !Ver_ParseFormalNetsAreDriven(pNtk, pBundle->pNameFormal) ) // non-driven
02335                 return pBundle;
02336     }
02337     return NULL;
02338 }

int Ver_ParseInitial ( Ver_Man_t pMan,
Abc_Ntk_t pNtk 
) [static]

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

Synopsis [Parses one directive.]

Description []

SideEffects []

SeeAlso []

Definition at line 958 of file verCore.c.

00959 {
00960     Ver_Stream_t * p = pMan->pReader;
00961     Abc_Obj_t * pNode, * pNet;
00962     int fStopAfterOne;
00963     char * pWord, * pEquation;
00964     char Symbol;
00965     // parse the directive 
00966     pWord = Ver_ParseGetName( pMan );
00967     if ( pWord == NULL )
00968         return 0;
00969     // decide how many statements to parse
00970     fStopAfterOne = 0;
00971     if ( strcmp( pWord, "begin" ) )
00972         fStopAfterOne = 1;
00973     // iterate over the initial states
00974     while ( 1 )
00975     {
00976         if ( !fStopAfterOne )
00977         {
00978             // get the name of the output signal
00979             pWord = Ver_ParseGetName( pMan );
00980             if ( pWord == NULL )
00981                 return 0;
00982             // look for the end of directive
00983             if ( !strcmp( pWord, "end" ) )
00984                 break;
00985         }
00986         // get the fanout net
00987         pNet = Ver_ParseFindNet( pNtk, pWord );
00988         if ( pNet == NULL )
00989         {
00990             sprintf( pMan->sError, "Cannot read the initial statement for %s (output wire is not defined).", pWord );
00991             Ver_ParsePrintErrorMessage( pMan );
00992             return 0;
00993         }
00994         // get the equality sign
00995         Symbol = Ver_StreamPopChar(p);
00996         if ( Symbol != '<' && Symbol != '=' )
00997         {
00998             sprintf( pMan->sError, "Cannot read the assign statement for %s (expected <= or =).", pWord );
00999             Ver_ParsePrintErrorMessage( pMan );
01000             return 0;
01001         }
01002         if ( Symbol == '<' )
01003             Ver_StreamPopChar(p);
01004         // skip the comments
01005         if ( !Ver_ParseSkipComments( pMan ) )
01006             return 0;
01007         // get the second name
01008         pEquation = Ver_StreamGetWord( p, ";" );
01009         if ( pEquation == NULL )
01010             return 0;
01011         // find the corresponding latch
01012         if ( Abc_ObjFaninNum(pNet) == 0 )
01013         {
01014             sprintf( pMan->sError, "Cannot find the latch to assign the initial value." );
01015             Ver_ParsePrintErrorMessage( pMan );
01016             return 0;
01017         }
01018         pNode = Abc_ObjFanin0(Abc_ObjFanin0(pNet));
01019         assert( Abc_ObjIsLatch(pNode) );
01020         // set the initial state
01021         if ( !strcmp(pEquation, "0") || !strcmp(pEquation, "1\'b0") )
01022             Abc_LatchSetInit0( pNode );
01023         else if ( !strcmp(pEquation, "1") || !strcmp(pEquation, "1\'b1") )
01024             Abc_LatchSetInit1( pNode );
01025 //        else if ( !strcmp(pEquation, "2") )
01026 //            Abc_LatchSetInitDc( pNode );
01027         else 
01028         {
01029             sprintf( pMan->sError, "Incorrect initial value of the latch %s.", Abc_ObjName(pNet) );
01030             Ver_ParsePrintErrorMessage( pMan );
01031             return 0;
01032         }
01033         // remove the last symbol
01034         Symbol = Ver_StreamPopChar(p);
01035         assert( Symbol == ';' );
01036         // quit if only one directive
01037         if ( fStopAfterOne )
01038             break;
01039     }
01040     return 1;
01041 }

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 572 of file verCore.c.

00573 {
00574     unsigned Value;
00575     if ( pMan->tName2Suffix == NULL )
00576         pMan->tName2Suffix = st_init_table( strcmp, st_strhash );
00577     if ( st_is_member( pMan->tName2Suffix, pWord ) )
00578         return 1;
00579     assert( nMsb >= 0 && nMsb < 128 );
00580     assert( nLsb >= 0 && nLsb < 128 );
00581     Value = (nMsb << 8) | nLsb;
00582     st_insert( pMan->tName2Suffix, Extra_UtilStrsav(pWord), (char *)Value );
00583     return 1;
00584 }

void Ver_ParseInternal ( Ver_Man_t pMan  )  [static]

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

Synopsis [File parser.]

Description []

SideEffects []

SeeAlso []

Definition at line 190 of file verCore.c.

00191 {
00192     Abc_Ntk_t * pNtk;
00193     char * pToken;
00194     int i;
00195 
00196     // preparse the modeles
00197     pMan->pProgress = Extra_ProgressBarStart( stdout, Ver_StreamGetFileSize(pMan->pReader) );
00198     while ( 1 )
00199     {
00200         // get the next token
00201         pToken = Ver_ParseGetName( pMan );
00202         if ( pToken == NULL )
00203             break;
00204         if ( strcmp( pToken, "module" ) )
00205         {
00206             sprintf( pMan->sError, "Cannot read \"module\" directive." );
00207             Ver_ParsePrintErrorMessage( pMan );
00208             return;
00209         }
00210         // parse the module
00211         if ( !Ver_ParseModule(pMan) )
00212             return;
00213     }
00214     Extra_ProgressBarStop( pMan->pProgress );
00215     pMan->pProgress = NULL;
00216 
00217     // process defined and undefined boxes
00218     if ( !Ver_ParseAttachBoxes( pMan ) )
00219         return;
00220 
00221     // connect the boxes and check
00222     Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i )
00223     {
00224         // fix the dangling nets
00225         Abc_NtkFinalizeRead( pNtk );
00226         // check the network for correctness
00227         if ( pMan->fCheck && !Abc_NtkCheckRead( pNtk ) )
00228         {
00229             pMan->fTopLevel = 1;
00230             sprintf( pMan->sError, "The network check has failed for network %s.", pNtk->pName );
00231             Ver_ParsePrintErrorMessage( pMan );
00232             return;
00233         }
00234     }
00235 }

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 548 of file verCore.c.

00549 {
00550     unsigned Value;
00551     *pnMsb = *pnLsb = -1;
00552     if ( pMan->tName2Suffix == NULL )
00553         return 1;
00554     if ( !st_lookup( pMan->tName2Suffix, (char *)pWord, (char **)&Value ) )
00555         return 1;
00556     *pnMsb = (Value >> 8) & 0xff;
00557     *pnLsb = Value & 0xff;
00558     return 1;
00559 }

int Ver_ParseMaxBoxSize ( Vec_Ptr_t vUndefs  ) 

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 2517 of file verCore.c.

02518 {
02519     Abc_Ntk_t * pNtk;
02520     Abc_Obj_t * pBox;
02521     int i, k, nMaxSize = 0;
02522     // go through undef box types
02523     Vec_PtrForEachEntry( vUndefs, pNtk, i )
02524         // go through instances of this type
02525         Vec_PtrForEachEntry( pNtk->pData, pBox, k )
02526             // check the number of bundles of this instance
02527             if ( nMaxSize < Vec_PtrSize((Vec_Ptr_t *)pBox->pCopy) )
02528                 nMaxSize = Vec_PtrSize((Vec_Ptr_t *)pBox->pCopy);
02529     return nMaxSize;
02530 }

int Ver_ParseModule ( Ver_Man_t pMan  )  [static]

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

Synopsis [Parses one Verilog module.]

Description []

SideEffects []

SeeAlso []

Definition at line 391 of file verCore.c.

00392 {
00393     Mio_Gate_t * pGate;
00394     Ver_Stream_t * p = pMan->pReader;
00395     Abc_Ntk_t * pNtk, * pNtkTemp;
00396     char * pWord, Symbol;
00397     int RetValue;
00398 
00399     // get the network name
00400     pWord = Ver_ParseGetName( pMan );
00401 
00402     // get the network with this name
00403     pNtk = Ver_ParseFindOrCreateNetwork( pMan, pWord );
00404 
00405     // make sure we stopped at the opening paranthesis
00406     if ( Ver_StreamPopChar(p) != '(' )
00407     {
00408         sprintf( pMan->sError, "Cannot find \"(\" after \"module\" in network %s.", pNtk->pName );
00409         Ver_ParsePrintErrorMessage( pMan );
00410         return 0;
00411     }
00412 
00413     // skip to the end of parantheses
00414     do {
00415         if ( Ver_ParseGetName( pMan ) == NULL )
00416             return 0;
00417         Symbol = Ver_StreamPopChar(p);
00418     } while ( Symbol == ',' );
00419     assert( Symbol == ')' );
00420     if ( !Ver_ParseSkipComments( pMan ) )
00421         return 0;
00422     Symbol = Ver_StreamPopChar(p);
00423     if ( Symbol != ';' )
00424     {
00425         sprintf( pMan->sError, "Expected closing paranthesis after \"module\"." );
00426         Ver_ParsePrintErrorMessage( pMan );
00427         return 0;
00428     }
00429 
00430     // parse the inputs/outputs/registers/wires/inouts
00431     while ( 1 )
00432     {
00433         Extra_ProgressBarUpdate( pMan->pProgress, Ver_StreamGetCurPosition(p), NULL );
00434         pWord = Ver_ParseGetName( pMan );
00435         if ( pWord == NULL )
00436             return 0;
00437         if ( !strcmp( pWord, "input" ) )
00438             RetValue = Ver_ParseSignal( pMan, pNtk, VER_SIG_INPUT );
00439         else if ( !strcmp( pWord, "output" ) )
00440             RetValue = Ver_ParseSignal( pMan, pNtk, VER_SIG_OUTPUT );
00441         else if ( !strcmp( pWord, "reg" ) )
00442             RetValue = Ver_ParseSignal( pMan, pNtk, VER_SIG_REG );
00443         else if ( !strcmp( pWord, "wire" ) )
00444             RetValue = Ver_ParseSignal( pMan, pNtk, VER_SIG_WIRE );
00445         else if ( !strcmp( pWord, "inout" ) )
00446             RetValue = Ver_ParseSignal( pMan, pNtk, VER_SIG_INOUT );
00447         else 
00448             break;
00449         if ( RetValue == 0 )
00450             return 0;
00451     }
00452 
00453     // parse the remaining statements
00454     while ( 1 )
00455     {
00456         Extra_ProgressBarUpdate( pMan->pProgress, Ver_StreamGetCurPosition(p), NULL );
00457 
00458         if ( !strcmp( pWord, "and" ) )
00459             RetValue = Ver_ParseGateStandard( pMan, pNtk, VER_GATE_AND );
00460         else if ( !strcmp( pWord, "or" ) )
00461             RetValue = Ver_ParseGateStandard( pMan, pNtk, VER_GATE_OR );
00462         else if ( !strcmp( pWord, "xor" ) )
00463             RetValue = Ver_ParseGateStandard( pMan, pNtk, VER_GATE_XOR );
00464         else if ( !strcmp( pWord, "buf" ) )
00465             RetValue = Ver_ParseGateStandard( pMan, pNtk, VER_GATE_BUF );
00466         else if ( !strcmp( pWord, "nand" ) )
00467             RetValue = Ver_ParseGateStandard( pMan, pNtk, VER_GATE_NAND );
00468         else if ( !strcmp( pWord, "nor" ) )
00469             RetValue = Ver_ParseGateStandard( pMan, pNtk, VER_GATE_NOR );
00470         else if ( !strcmp( pWord, "xnor" ) )
00471             RetValue = Ver_ParseGateStandard( pMan, pNtk, VER_GATE_XNOR );
00472         else if ( !strcmp( pWord, "not" ) )
00473             RetValue = Ver_ParseGateStandard( pMan, pNtk, VER_GATE_NOT );
00474 
00475         else if ( !strcmp( pWord, "assign" ) )
00476             RetValue = Ver_ParseAssign( pMan, pNtk );
00477         else if ( !strcmp( pWord, "always" ) )
00478             RetValue = Ver_ParseAlways( pMan, pNtk );
00479         else if ( !strcmp( pWord, "initial" ) )
00480             RetValue = Ver_ParseInitial( pMan, pNtk );
00481         else if ( !strcmp( pWord, "endmodule" ) )
00482             break;
00483         else if ( pMan->pDesign->pGenlib && (pGate = Mio_LibraryReadGateByName(pMan->pDesign->pGenlib, pWord)) ) // current design
00484             RetValue = Ver_ParseGate( pMan, pNtk, pGate );
00485 //        else if ( pMan->pDesign->pLibrary && st_lookup(pMan->pDesign->pLibrary->tModules, pWord, (char**)&pNtkTemp) ) // gate library
00486 //            RetValue = Ver_ParseGate( pMan, pNtkTemp );
00487         else // assume this is the box used in the current design
00488         {
00489             pNtkTemp = Ver_ParseFindOrCreateNetwork( pMan, pWord );
00490             RetValue = Ver_ParseBox( pMan, pNtk, pNtkTemp );
00491         }
00492         if ( RetValue == 0 )
00493             return 0;
00494         // skip the comments
00495         if ( !Ver_ParseSkipComments( pMan ) )
00496             return 0;
00497         // get new word
00498         pWord = Ver_ParseGetName( pMan );
00499         if ( pWord == NULL )
00500             return 0;
00501     }
00502 
00503     // convert from the blackbox into the network with local functions representated by AIGs
00504     if ( pNtk->ntkFunc == ABC_FUNC_BLACKBOX )
00505     {
00506         if ( Abc_NtkNodeNum(pNtk) > 0 || Abc_NtkBoxNum(pNtk) > 0 )
00507         {
00508             if ( !Ver_ParseConvertNetwork( pMan, pNtk, pMan->fMapped ) )
00509                 return 0;
00510         }
00511         else
00512         {
00513             Abc_Obj_t * pObj, * pBox, * pTerm;
00514             int i; 
00515             pBox = Abc_NtkCreateBlackbox(pNtk);
00516             Abc_NtkForEachPi( pNtk, pObj, i )
00517             {
00518                 pTerm = Abc_NtkCreateBi(pNtk);
00519                 Abc_ObjAddFanin( pTerm, Abc_ObjFanout0(pObj) );
00520                 Abc_ObjAddFanin( pBox, pTerm );
00521             }
00522             Abc_NtkForEachPo( pNtk, pObj, i )
00523             {
00524                 pTerm = Abc_NtkCreateBo(pNtk);
00525                 Abc_ObjAddFanin( pTerm, pBox );
00526                 Abc_ObjAddFanin( Abc_ObjFanin0(pObj), pTerm );
00527             }
00528         }
00529     }
00530 
00531     // remove the table if needed
00532     Ver_ParseRemoveSuffixTable( pMan );
00533     return 1;
00534 }

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 268 of file verCore.c.

00269 {
00270     p->fError = 1;
00271     if ( p->fTopLevel ) // the line number is not given
00272         fprintf( p->Output, "%s: %s\n", p->pFileName, p->sError );
00273     else // print the error message with the line number
00274         fprintf( p->Output, "%s (line %d): %s\n", 
00275             p->pFileName, Ver_StreamGetLineNumber(p->pReader), p->sError );
00276     // free the data
00277     Ver_ParseFreeData( p );
00278 }

void Ver_ParsePrintLog ( Ver_Man_t pMan  ) 

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 2543 of file verCore.c.

02544 {
02545     Abc_Ntk_t * pNtk, * pNtkBox;
02546     Abc_Obj_t * pBox;
02547     FILE * pFile;
02548     char * pNameGeneric;
02549     char Buffer[1000];
02550     int i, k;
02551 
02552     // open the log file
02553     pNameGeneric = Extra_FileNameGeneric( pMan->pFileName );
02554     sprintf( Buffer, "%s.log", pNameGeneric );
02555     free( pNameGeneric );
02556     pFile = fopen( Buffer, "w" );
02557 
02558     // count the total number of instances and how many times they occur
02559     Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i )
02560         pNtk->fHieVisited = 0;
02561     Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i )
02562         Abc_NtkForEachBox( pNtk, pBox, k )
02563         {
02564             if ( Abc_ObjIsLatch(pBox) )
02565                 continue;
02566             pNtkBox = pBox->pData;
02567             if ( pNtkBox == NULL )
02568                 continue;
02569             pNtkBox->fHieVisited++;
02570         }
02571     // print each box and its stats
02572     fprintf( pFile, "The hierarhical design %s contains %d modules:\n", pMan->pFileName, Vec_PtrSize(pMan->pDesign->vModules) );
02573     Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i )
02574     {
02575         fprintf( pFile, "%-24s : ", Abc_NtkName(pNtk) );
02576         if ( !Ver_NtkIsDefined(pNtk) )
02577             fprintf( pFile, "undefbox" );
02578         else if ( Abc_NtkHasBlackbox(pNtk) )
02579             fprintf( pFile, "blackbox" );
02580         else
02581             fprintf( pFile, "logicbox" );
02582         fprintf( pFile, " instantiated %6d times ", pNtk->fHieVisited );
02583 //        fprintf( pFile, "\n   " );
02584         fprintf( pFile, " pi = %4d", Abc_NtkPiNum(pNtk) );
02585         fprintf( pFile, " po = %4d", Abc_NtkPiNum(pNtk) );
02586         fprintf( pFile, " nd = %8d",  Abc_NtkNodeNum(pNtk) );
02587         fprintf( pFile, " lat = %6d",  Abc_NtkLatchNum(pNtk) );
02588         fprintf( pFile, " box = %6d", Abc_NtkBoxNum(pNtk)-Abc_NtkLatchNum(pNtk) );
02589         fprintf( pFile, "\n" );
02590     }
02591     Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i )
02592         pNtk->fHieVisited = 0;
02593 
02594     // report instances with dangling outputs
02595     if ( Vec_PtrSize(pMan->pDesign->vModules) > 1 )
02596     {
02597         Vec_Ptr_t * vBundles;
02598         Ver_Bundle_t * pBundle;
02599         int j, nActNets, Counter = 0, CounterBoxes = 0;
02600         // count the number of instances with dangling outputs
02601         Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i )
02602         {
02603             Abc_NtkForEachBox( pNtk, pBox, k )
02604             {
02605                 if ( Abc_ObjIsLatch(pBox) )
02606                     continue;
02607                 vBundles = (Vec_Ptr_t *)pBox->pCopy;
02608                 pNtkBox = pBox->pData;
02609                 if ( pNtkBox == NULL )
02610                     continue;
02611                 if ( !Ver_NtkIsDefined(pNtkBox) )
02612                     continue;
02613                 // count the number of actual nets
02614                 nActNets = 0;
02615                 Vec_PtrForEachEntry( vBundles, pBundle, j )
02616                     nActNets += Vec_PtrSize(pBundle->vNetsActual);
02617                 // the box is defined and will be connected
02618                 if ( nActNets != Abc_NtkPiNum(pNtkBox) + Abc_NtkPoNum(pNtkBox) )
02619                     Counter++;
02620             }
02621         }
02622         if ( Counter == 0 )
02623             fprintf( pFile, "The outputs of all box instances are connected.\n" );
02624         else
02625         {
02626             fprintf( pFile, "\n" );
02627             fprintf( pFile, "The outputs of %d box instances are not connected:\n", Counter );
02628             // enumerate through the boxes
02629             Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i )
02630             {
02631                 Abc_NtkForEachBox( pNtk, pBox, k )
02632                 {
02633                     if ( Abc_ObjIsLatch(pBox) )
02634                         continue;
02635                     vBundles = (Vec_Ptr_t *)pBox->pCopy;
02636                     pNtkBox = pBox->pData;
02637                     if ( pNtkBox == NULL )
02638                         continue;
02639                     if ( !Ver_NtkIsDefined(pNtkBox) )
02640                         continue;
02641                     // count the number of actual nets
02642                     nActNets = 0;
02643                     Vec_PtrForEachEntry( vBundles, pBundle, j )
02644                         nActNets += Vec_PtrSize(pBundle->vNetsActual);
02645                     // the box is defined and will be connected
02646                     if ( nActNets != Abc_NtkPiNum(pNtkBox) + Abc_NtkPoNum(pNtkBox) )
02647                         fprintf( pFile, "In module \"%s\" instance \"%s\" of box \"%s\" has different numbers of actual/formal nets (%d/%d).\n",
02648                             Abc_NtkName(pNtk), Abc_ObjName(pBox), Abc_NtkName(pNtkBox), nActNets, Abc_NtkPiNum(pNtkBox) + Abc_NtkPoNum(pNtkBox) );
02649                 }
02650             }
02651         }
02652     }
02653     fclose( pFile );
02654     printf( "Hierarchy statistics can be found in log file \"%s\".\n", Buffer );
02655 }

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 597 of file verCore.c.

00598 {
00599     st_generator * gen;
00600     char * pKey, * pValue;
00601     if ( pMan->tName2Suffix == NULL )
00602         return;
00603     st_foreach_item( pMan->tName2Suffix, gen, (char **)&pKey, (char **)&pValue )
00604         free( pKey );
00605     st_free_table( pMan->tName2Suffix );
00606     pMan->tName2Suffix = NULL;
00607 }

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 2209 of file verCore.c.

02210 {
02211     Abc_Ntk_t * pNtk;
02212     Abc_Obj_t * pBox;
02213     int i, k, nBoxes;
02214     // clean 
02215     nBoxes = 0;
02216     Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i )
02217     {
02218         pNtk->fHiePath = 0;
02219         if ( !Ver_NtkIsDefined(pNtk) )
02220             nBoxes++;
02221     }
02222     // count
02223     Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i )
02224         Abc_NtkForEachBlackbox( pNtk, pBox, k )
02225             if ( pBox->pData && !Ver_NtkIsDefined(pBox->pData) )
02226                 ((Abc_Ntk_t *)pBox->pData)->fHiePath++;
02227     // print the stats
02228     printf( "Warning: The design contains %d undefined objects interpreted as blackboxes:\n", nBoxes );
02229     Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i )
02230         if ( !Ver_NtkIsDefined(pNtk) )
02231             printf( "%s (%d)  ", Abc_NtkName(pNtk), pNtk->fHiePath );
02232     printf( "\n" );
02233     // clean 
02234     Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i )
02235         pNtk->fHiePath = 0;
02236 }

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 779 of file verCore.c.

00780 {
00781     Ver_Stream_t * p = pMan->pReader;
00782     char Buffer[1000], Symbol, * pWord;
00783     int nMsb, nLsb, Bit, Limit, i;
00784     nMsb = nLsb = -1;
00785     while ( 1 )
00786     {
00787         // get the next word
00788         pWord = Ver_ParseGetName( pMan );
00789         if ( pWord == NULL )
00790             return 0;
00791 
00792         // check if the range is specified
00793         if ( pWord[0] == '[' && !pMan->fNameLast )
00794         {
00795             assert( nMsb == -1 && nLsb == -1 );
00796             Ver_ParseSignalPrefix( pMan, &pWord, &nMsb, &nLsb );
00797             // check the case when there is space between bracket and the next word
00798             if ( *pWord == 0 )
00799             {
00800                 // get the signal name
00801                 pWord = Ver_ParseGetName( pMan );
00802                 if ( pWord == NULL )
00803                     return 0;
00804             }
00805         }
00806 
00807         // create signals
00808         if ( nMsb == -1 && nLsb == -1 )
00809         {
00810             if ( SigType == VER_SIG_INPUT || SigType == VER_SIG_INOUT )
00811                 Ver_ParseCreatePi( pNtk, pWord );
00812             if ( SigType == VER_SIG_OUTPUT || SigType == VER_SIG_INOUT )
00813                 Ver_ParseCreatePo( pNtk, pWord );
00814             if ( SigType == VER_SIG_WIRE || SigType == VER_SIG_REG )
00815                 Abc_NtkFindOrCreateNet( pNtk, pWord );
00816         }
00817         else
00818         {
00819             assert( nMsb >= 0 && nLsb >= 0 );
00820             // add to the hash table
00821             Ver_ParseInsertsSuffix( pMan, pWord, nMsb, nLsb );
00822             // add signals from Lsb to Msb
00823             Limit = nMsb > nLsb? nMsb - nLsb + 1: nLsb - nMsb + 1;
00824             for ( i = 0, Bit = nLsb; i < Limit; i++, Bit = nMsb > nLsb ? Bit + 1: Bit - 1  )
00825             {
00826                 sprintf( Buffer, "%s[%d]", pWord, Bit );
00827                 if ( SigType == VER_SIG_INPUT || SigType == VER_SIG_INOUT )
00828                     Ver_ParseCreatePi( pNtk, Buffer );
00829                 if ( SigType == VER_SIG_OUTPUT || SigType == VER_SIG_INOUT )
00830                     Ver_ParseCreatePo( pNtk, Buffer );
00831                 if ( SigType == VER_SIG_WIRE || SigType == VER_SIG_REG )
00832                     Abc_NtkFindOrCreateNet( pNtk, Buffer );
00833             }
00834         }
00835 
00836         Symbol = Ver_StreamPopChar(p);
00837         if ( Symbol == ',' )
00838             continue;
00839         if ( Symbol == ';' )
00840             return 1;
00841         break;
00842     }
00843     sprintf( pMan->sError, "Cannot parse signal line (expected , or ;)." );
00844     Ver_ParsePrintErrorMessage( pMan );
00845     return 0;
00846 }

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 620 of file verCore.c.

00621 {
00622     char * pWord = *ppWord;
00623     int nMsb, nLsb;
00624     assert( pWord[0] == '[' );
00625     // get the beginning
00626     nMsb = atoi( pWord + 1 );
00627     // find the splitter
00628     while ( *pWord && *pWord != ':' && *pWord != ']' )
00629         pWord++;
00630     if ( *pWord == 0 )
00631     {
00632         sprintf( pMan->sError, "Cannot find closing bracket in this line." );
00633         Ver_ParsePrintErrorMessage( pMan );
00634         return 0;
00635     }
00636     if ( *pWord == ']' )
00637         nLsb = nMsb;
00638     else
00639     {
00640         assert( *pWord == ':' );
00641         nLsb = atoi( pWord + 1 );
00642         // find the closing paranthesis
00643         while ( *pWord && *pWord != ']' )
00644             pWord++;
00645         if ( *pWord == 0 )
00646         {
00647             sprintf( pMan->sError, "Cannot find closing bracket in this line." );
00648             Ver_ParsePrintErrorMessage( pMan );
00649             return 0;
00650         }
00651         assert( *pWord == ']' );
00652         pWord++;
00653     }
00654     assert( nMsb >= 0 && nLsb >= 0 );
00655     // return
00656     *ppWord = pWord;
00657     *pnMsb = nMsb;
00658     *pnLsb = nLsb;
00659     return 1;
00660 }

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 673 of file verCore.c.

00674 {
00675     char * pCur;
00676     int Length;
00677     Length = strlen(pWord);
00678     assert( pWord[Length-1] == ']' );
00679     // walk backward
00680     for ( pCur = pWord + Length - 2; pCur != pWord; pCur-- )
00681         if ( *pCur == ':' || *pCur == '[' )
00682             break;
00683     if ( pCur == pWord )
00684     {
00685         sprintf( pMan->sError, "Cannot find opening bracket in signal name %s.", pWord );
00686         Ver_ParsePrintErrorMessage( pMan );
00687         return 0;
00688     }
00689     if ( *pCur == '[' )
00690     {
00691         *pnMsb = *pnLsb = atoi(pCur+1);
00692         *pCur = 0;
00693         return 1;
00694     }
00695     assert( *pCur == ':' );
00696     // get the end of the interval
00697     *pnLsb = atoi(pCur+1);
00698     // find the beginning
00699     for ( pCur = pWord + Length - 2; pCur != pWord; pCur-- )
00700         if ( *pCur == '[' )
00701             break;
00702     if ( pCur == pWord )
00703     {
00704         sprintf( pMan->sError, "Cannot find opening bracket in signal name %s.", pWord );
00705         Ver_ParsePrintErrorMessage( pMan );
00706         return 0;
00707     }
00708     assert( *pCur == '[' );
00709     // get the beginning of the interval
00710     *pnMsb = atoi(pCur+1);
00711     // cut the word
00712     *pCur = 0;
00713     return 1;
00714 }

Ver_Man_t * Ver_ParseStart ( char *  pFileName,
Abc_Lib_t pGateLib 
) [static]

FUNCTION DEFINITIONS ///Function*************************************************************

Synopsis [Start parser.]

Description []

SideEffects []

SeeAlso []

Definition at line 100 of file verCore.c.

00101 {
00102     Ver_Man_t * p;
00103     p = ALLOC( Ver_Man_t, 1 );
00104     memset( p, 0, sizeof(Ver_Man_t) );
00105     p->pFileName = pFileName;
00106     p->pReader   = Ver_StreamAlloc( pFileName );
00107     if ( p->pReader == NULL )
00108         return NULL;
00109     p->Output    = stdout;
00110     p->vNames    = Vec_PtrAlloc( 100 );
00111     p->vStackFn  = Vec_PtrAlloc( 100 );
00112     p->vStackOp  = Vec_IntAlloc( 100 );
00113     p->vPerm     = Vec_IntAlloc( 100 );
00114     // create the design library and assign the technology library
00115     p->pDesign   = Abc_LibCreate( pFileName );
00116     p->pDesign->pLibrary = pGateLib;
00117     p->pDesign->pGenlib = Abc_FrameReadLibGen();
00118     return p;
00119 }

void Ver_ParseStop ( Ver_Man_t p  )  [static]

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

Synopsis [Stop parser.]

Description []

SideEffects []

SeeAlso []

Definition at line 132 of file verCore.c.

00133 {
00134     if ( p->pProgress )
00135         Extra_ProgressBarStop( p->pProgress );
00136     Ver_StreamFree( p->pReader );
00137     Vec_PtrFree( p->vNames   );
00138     Vec_PtrFree( p->vStackFn );
00139     Vec_IntFree( p->vStackOp );
00140     Vec_IntFree( p->vPerm );
00141     free( p );
00142 }


Variable Documentation

int glo_fMapped = 0

Definition at line 76 of file verCore.c.


Generated on Tue Jan 5 12:18:50 2010 for abc70930 by  doxygen 1.6.1