verCore.c File Reference

#include "ver.h"
#include "map/mio/mio.h"
#include "base/main/main.h"

Include dependency graph for verCore.c:

Go to the source code of this file.

Classes
struct	Ver_Bundle_t_

Typedefs
typedef struct Ver_Bundle_t_	Ver_Bundle_t

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

Functions
Abc_Des_t *	Ver_ParseFile (char *pFileName, Abc_Des_t *pGateLib, int fCheck, int fUseMemMan)
	MACRO DEFINITIONS ///.
void	Ver_ParsePrintErrorMessage (Ver_Man_t *p)
Abc_Ntk_t *	Ver_ParseFindOrCreateNetwork (Ver_Man_t *pMan, char *pName)
Abc_Obj_t *	Ver_ParseFindNet (Abc_Ntk_t *pNtk, char *pName)
int	Ver_ParseConvertNetwork (Ver_Man_t *pMan, Abc_Ntk_t *pNtk, int fMapped)
int	Ver_ParseLookupSuffix (Ver_Man_t *pMan, char *pWord, int *pnMsb, int *pnLsb)
int	Ver_ParseInsertsSuffix (Ver_Man_t *pMan, char *pWord, int nMsb, int nLsb)
int	Ver_ParseSignalPrefix (Ver_Man_t *pMan, char **ppWord, int *pnMsb, int *pnLsb)
int	Ver_ParseSignalSuffix (Ver_Man_t *pMan, char *pWord, int *pnMsb, int *pnLsb)
int	Ver_ParseConstant (Ver_Man_t *pMan, char *pWord)
int	Ver_FindGateInput (Mio_Gate_t *pGate, char *pName)
void	Ver_ParseFreeBundle (Ver_Bundle_t *pBundle)
int	Ver_ParseConnectDefBoxes (Ver_Man_t *pMan)
Vec_Ptr_t *	Ver_ParseCollectUndefBoxes (Ver_Man_t *pMan)
void	Ver_ParseReportUndefBoxes (Ver_Man_t *pMan)
int	Ver_ParseCheckNondrivenNets (Vec_Ptr_t *vUndefs)
int	Ver_ParseFormalNetsAreDriven (Abc_Ntk_t *pNtk, char *pNameFormal)
Ver_Bundle_t *	Ver_ParseGetNondrivenBundle (Abc_Ntk_t *pNtk, int Counter)
int	Ver_ParseDriveFormal (Ver_Man_t *pMan, Abc_Ntk_t *pNtk, Ver_Bundle_t *pBundle0)
int	Ver_ParseDriveInputs (Ver_Man_t *pMan, Vec_Ptr_t *vUndefs)
int	Ver_ParseMaxBoxSize (Vec_Ptr_t *vUndefs)
void	Ver_ParsePrintLog (Ver_Man_t *pMan)

Variables
int	glo_fMapped = 0

Typedef Documentation

Ver_Bundle_t

typedef struct Ver_Bundle_t_ Ver_Bundle_t

Definition at line 82 of file verCore.c.

Enumeration Type Documentation

Ver_GateType_t

enum Ver_GateType_t

Enumerator
VER_GATE_AND
VER_GATE_OR
VER_GATE_XOR
VER_GATE_BUF
VER_GATE_NAND
VER_GATE_NOR
VER_GATE_XNOR
VER_GATE_NOT

Definition at line 43 of file verCore.c.

             { 
    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
} Ver_GateType_t;

Ver_SignalType_t

enum Ver_SignalType_t

DECLARATIONS ///.

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

FileName [verCore.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Verilog parser.]

Synopsis [Parses several flavors of structural Verilog.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id

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

]

Enumerator
VER_SIG_NONE
VER_SIG_INPUT
VER_SIG_OUTPUT
VER_SIG_INOUT
VER_SIG_REG
VER_SIG_WIRE

Definition at line 33 of file verCore.c.

             { 
    VER_SIG_NONE = 0,
    VER_SIG_INPUT,
    VER_SIG_OUTPUT,
    VER_SIG_INOUT,
    VER_SIG_REG,
    VER_SIG_WIRE
} Ver_SignalType_t;

Function Documentation

Ver_FindGateInput()

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

{
    Mio_Pin_t * pGatePin;
    int i;
    for ( i = 0, pGatePin = Mio_GateReadPins(pGate); pGatePin != NULL; pGatePin = Mio_PinReadNext(pGatePin), i++ )
        if ( strcmp(pName, Mio_PinReadName(pGatePin)) == 0 )
            return i;
    if ( strcmp(pName, Mio_GateReadOutName(pGate)) == 0 )
        return i;
    if ( Mio_GateReadTwin(pGate) && strcmp(pName, Mio_GateReadOutName(Mio_GateReadTwin(pGate))) == 0 )
        return i+1;
    return -1;
}

Here is the call graph for this function:

Ver_ParseCheckNondrivenNets()

int Ver_ParseCheckNondrivenNets

(

Vec_Ptr_t *

vUndefs

)

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 2442 of file verCore.c.

{
    Abc_Ntk_t * pNtk;
    Ver_Bundle_t * pBundle;
    Abc_Obj_t * pBox, * pNet;
    int i, k, j, m;
    // go through undef box types
    Vec_PtrForEachEntry( Abc_Ntk_t *, vUndefs, pNtk, i )
        // go through instances of this type
        Vec_PtrForEachEntry( Abc_Obj_t *, (Vec_Ptr_t *)pNtk->pData, pBox, k )
            // go through the bundles of this instance
            Vec_PtrForEachEntryReverse( Ver_Bundle_t *, (Vec_Ptr_t *)pBox->pCopy, pBundle, j )
                // go through the actual nets of this bundle
                if ( pBundle )
                Vec_PtrForEachEntry( Abc_Obj_t *, pBundle->vNetsActual, pNet, m )
                {
                    if ( Abc_ObjFaninNum(pNet) == 0 ) // non-driven
                        if ( strcmp(Abc_ObjName(pNet), "1\'b0") && strcmp(Abc_ObjName(pNet), "1\'b1") ) // diff from a const
                            return 1;
                }
    return 0;
}

Here is the call graph for this function:

Ver_ParseCollectUndefBoxes()

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

{
    Vec_Ptr_t * vUndefs;
    Abc_Ntk_t * pNtk, * pNtkBox;
    Abc_Obj_t * pBox;
    int i, k;
    // clear the module structures
    Vec_PtrForEachEntry( Abc_Ntk_t *, pMan->pDesign->vModules, pNtk, i )
        pNtk->pData = NULL;
    // go through all the blackboxes
    vUndefs = Vec_PtrAlloc( 16 );
    Vec_PtrForEachEntry( Abc_Ntk_t *, pMan->pDesign->vModules, pNtk, i )
    {
        Abc_NtkForEachBlackbox( pNtk, pBox, k )
        {
            pNtkBox = (Abc_Ntk_t *)pBox->pData;
            if ( pNtkBox == NULL )
                continue;
            if ( Ver_NtkIsDefined(pNtkBox) )
                continue;
            if ( pNtkBox->pData == NULL )
            {
                // save the box
                Vec_PtrPush( vUndefs, pNtkBox );
                pNtkBox->pData = Vec_PtrAlloc( 16 );
            }
            // save the instance
            Vec_PtrPush( (Vec_Ptr_t *)pNtkBox->pData, pBox );
        }
    }
    return vUndefs;
}

Ver_ParseConnectDefBoxes()

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

{
    Abc_Ntk_t * pNtk;
    Abc_Obj_t * pBox;
    int i, k, RetValue = 1;
    // go through all the modules
    Vec_PtrForEachEntry( Abc_Ntk_t *, pMan->pDesign->vModules, pNtk, i )
    {
        // go through all the boxes of this module
        Abc_NtkForEachBox( pNtk, pBox, k )
        {
            if ( Abc_ObjIsLatch(pBox) )
                continue;
            // skip internal boxes of the blackboxes
            if ( pBox->pData == NULL )
                continue;
            // if the network is undefined, it will be connected later
            if ( !Ver_NtkIsDefined((Abc_Ntk_t *)pBox->pData) )
            {
                RetValue = 2;
                continue;
            }
            // connect the box
            if ( !Ver_ParseConnectBox( pMan, pBox ) )
                return 0;
            // if the network is a true blackbox, skip
            if ( Abc_NtkHasBlackbox((Abc_Ntk_t *)pBox->pData) )
                continue;
            // convert the box to the whitebox
            Abc_ObjBlackboxToWhitebox( pBox );
        }
    }
    return RetValue;
}

Ver_ParseConstant()

int Ver_ParseConstant	(	Ver_Man_t *	pMan,
		char *	pWord )

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

Synopsis [Returns the values of constant bits.]

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

SideEffects []

SeeAlso []

Definition at line 753 of file verCore.c.

{
    int nBits, i;
    assert( pWord[0] >= '1' && pWord[1] <= '9' );
    nBits = atoi(pWord);
    // find the next symbol \'
    while ( *pWord && *pWord != '\'' )
        pWord++;
    if ( *pWord == 0 )
    {
        sprintf( pMan->sError, "Cannot find symbol \' in the constant." );
        Ver_ParsePrintErrorMessage( pMan );
        return 0;
    }
    assert( *pWord == '\'' );
    pWord++;
    if ( *pWord != 'b' )
    {
        sprintf( pMan->sError, "Currently can only handle binary constants." );
        Ver_ParsePrintErrorMessage( pMan );
        return 0;
    }
    pWord++;
    // scan the bits
    Vec_PtrClear( pMan->vNames );
    for ( i = 0; i < nBits; i++ )
    {
      if ( pWord[i] != '0' && pWord[i] != '1' && pWord[i] != 'x' )
      {
         sprintf( pMan->sError, "Having problem parsing the binary constant." );
         Ver_ParsePrintErrorMessage( pMan );
         return 0;
      }
      if ( pWord[i] == 'x' ) 
          Vec_PtrPush( pMan->vNames, (void *)0 );
      else 
          Vec_PtrPush( pMan->vNames, (void *)(ABC_PTRUINT_T)(pWord[i]-'0') );
    }
    return 1;
}

Here is the call graph for this function:

Ver_ParseConvertNetwork()

int Ver_ParseConvertNetwork	(	Ver_Man_t *	pMan,
		Abc_Ntk_t *	pNtk,
		int	fMapped )

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 351 of file verCore.c.

{
    if ( fMapped )
    {
        // convert from the blackbox into the network with local functions representated by AIGs
        if ( pNtk->ntkFunc == ABC_FUNC_BLACKBOX )
        {
            // change network type
            assert( pNtk->pManFunc == NULL );
            pNtk->ntkFunc = ABC_FUNC_MAP;
            pNtk->pManFunc = pMan->pDesign->pGenlib;
        }
        else if ( pNtk->ntkFunc != ABC_FUNC_MAP )
        {
            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 );
            Ver_ParsePrintErrorMessage( pMan );
            return 0;
        }
    }
    else
    {
        // convert from the blackbox into the network with local functions representated by AIGs
        if ( pNtk->ntkFunc == ABC_FUNC_BLACKBOX )
        {
            // change network type
            assert( pNtk->pManFunc == NULL );
            pNtk->ntkFunc = ABC_FUNC_AIG;
            pNtk->pManFunc = pMan->pDesign->pManFunc;
        }
        else if ( pNtk->ntkFunc != ABC_FUNC_AIG )
        {
            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 );
            Ver_ParsePrintErrorMessage( pMan );
            return 0;
        }
    }
    return 1;
}

Here is the call graph for this function:

Ver_ParseDriveFormal()

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

{
    char Buffer[200];
    char * pName;
    Ver_Bundle_t * pBundle = NULL;
    Abc_Obj_t * pBox, * pTerm, * pTermNew, * pNetAct, * pNetFormal;
    int k, j, m;
 
    // drive this net in the undef box
    Vec_PtrForEachEntry( Abc_Obj_t *, pBundle0->vNetsActual, pNetAct, m )
    {
        // create the formal net
        if ( Vec_PtrSize(pBundle0->vNetsActual) == 1 )
            sprintf( Buffer, "%s", pBundle0->pNameFormal );
        else
            sprintf( Buffer, "%s[%d]", pBundle0->pNameFormal, m );
        assert( Abc_NtkFindNet( pNtk, Buffer ) == NULL );
        pNetFormal = Abc_NtkFindOrCreateNet( pNtk, Buffer );
        // connect it to the box
        pTerm = Abc_NtkCreateBo( pNtk );
        assert( Abc_NtkBoxNum(pNtk) <= 1 );
        pBox = Abc_NtkBoxNum(pNtk)? Abc_NtkBox(pNtk,0) : Abc_NtkCreateBlackbox(pNtk);
        Abc_ObjAddFanin( Abc_NtkCreatePo(pNtk), pNetFormal );
        Abc_ObjAddFanin( pNetFormal, pTerm );
        Abc_ObjAddFanin( pTerm, pBox );
    }
 
    // go through instances of this type
    pName = Extra_UtilStrsav(pBundle0->pNameFormal);
    Vec_PtrForEachEntry( Abc_Obj_t *, (Vec_Ptr_t *)pNtk->pData, pBox, k )
    {
        // find a bundle with the given name in this instance
        Vec_PtrForEachEntryReverse( Ver_Bundle_t *, (Vec_Ptr_t *)pBox->pCopy, pBundle, j )
            if ( pBundle && !strcmp( pBundle->pNameFormal, pName ) )
                break;
        // skip non-driven bundles
        if ( j == Vec_PtrSize((Vec_Ptr_t *)pBox->pCopy) )
            continue;
        // check if any nets are driven in this bundle
        assert(pBundle); // Verify pBundle was assigned to.
        Vec_PtrForEachEntry( Abc_Obj_t *, pBundle->vNetsActual, pNetAct, m )
            if ( Abc_ObjFaninNum(pNetAct) > 0 )
            {
                sprintf( pMan->sError, "Missing specification of the I/Os of undefined box \"%s\".", Abc_NtkName(pNtk) );
                Ver_ParsePrintErrorMessage( pMan );
                return 0;
            }
        // drive the nets by the undef box
        Vec_PtrForEachEntryReverse( Abc_Obj_t *, pBundle->vNetsActual, pNetAct, m )
        {
            pTermNew = Abc_NtkCreateBo( pNetAct->pNtk );
            Abc_ObjAddFanin( pTermNew, pBox );
            Abc_ObjAddFanin( pNetAct, pTermNew );
        }
        // remove the bundle
        Ver_ParseFreeBundle( pBundle ); pBundle = NULL;
        Vec_PtrWriteEntry( (Vec_Ptr_t *)pBox->pCopy, j, NULL );
    }
    ABC_FREE( pName );
    return 1;
}

Here is the call graph for this function:

Ver_ParseDriveInputs()

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

{
    char Buffer[200];
    Ver_Bundle_t * pBundle;
    Abc_Ntk_t * pNtk;
    Abc_Obj_t * pBox, * pBox2, * pTerm, * pTermNew, * pNetFormal, * pNetAct;
    int i, k, j, m, CountCur, CountTotal = -1;
    // iterate through the undef boxes
    Vec_PtrForEachEntry( Abc_Ntk_t *, vUndefs, pNtk, i )
    {
        // count the number of unconnected bundles for instances of this type of box
        CountTotal = -1;
        Vec_PtrForEachEntry( Abc_Obj_t *, (Vec_Ptr_t *)pNtk->pData, pBox, k )
        {
            CountCur = 0;
            Vec_PtrForEachEntry( Ver_Bundle_t *, (Vec_Ptr_t *)pBox->pCopy, pBundle, j )
                CountCur += (pBundle != NULL);
            if ( CountTotal == -1 )
                CountTotal = CountCur;
            else if ( CountTotal != CountCur )
            {
                sprintf( pMan->sError, "The number of formal inputs (%d) is different from the expected one (%d) when instantiating network %s in box %s.", 
                    CountCur, CountTotal, pNtk->pName, Abc_ObjName(pBox) );
                Ver_ParsePrintErrorMessage( pMan );
                return 0;
            }
        }
 
        // create formals
        pBox = (Abc_Obj_t *)Vec_PtrEntry( (Vec_Ptr_t *)pNtk->pData, 0 );
        Vec_PtrForEachEntry( Ver_Bundle_t *, (Vec_Ptr_t *)pBox->pCopy, pBundle, j )
        {
            if ( pBundle == NULL )
                continue;
            Vec_PtrForEachEntry( Abc_Obj_t *, pBundle->vNetsActual, pNetAct, m )
            {
                // find create the formal net
                if ( Vec_PtrSize(pBundle->vNetsActual) == 1 )
                    sprintf( Buffer, "%s", pBundle->pNameFormal );
                else
                    sprintf( Buffer, "%s[%d]", pBundle->pNameFormal, m );
                assert( Abc_NtkFindNet( pNtk, Buffer ) == NULL );
                pNetFormal = Abc_NtkFindOrCreateNet( pNtk, Buffer );
                // connect
                pTerm = Abc_NtkCreateBi( pNtk );
                assert( Abc_NtkBoxNum(pNtk) <= 1 );
                pBox2 = Abc_NtkBoxNum(pNtk)? Abc_NtkBox(pNtk,0) : Abc_NtkCreateBlackbox(pNtk);
                Abc_ObjAddFanin( pNetFormal, Abc_NtkCreatePi(pNtk) );
                Abc_ObjAddFanin( pTerm, pNetFormal );
                Abc_ObjAddFanin( pBox2, pTerm );
            }
        }
 
        // go through all the boxes
        Vec_PtrForEachEntry( Abc_Obj_t *, (Vec_Ptr_t *)pNtk->pData, pBox, k )
        {
            // go through all the bundles
            Vec_PtrForEachEntry( Ver_Bundle_t *, (Vec_Ptr_t *)pBox->pCopy, pBundle, j )
            {
                if ( pBundle == NULL )
                    continue;
                // drive the nets by the undef box
                Vec_PtrForEachEntryReverse( Abc_Obj_t *, pBundle->vNetsActual, pNetAct, m )
                {
                    pTermNew = Abc_NtkCreateBi( pNetAct->pNtk );
                    Abc_ObjAddFanin( pBox, pTermNew );
                    Abc_ObjAddFanin( pTermNew, pNetAct );
                }
                // remove the bundle
                Ver_ParseFreeBundle( pBundle );
                Vec_PtrWriteEntry( (Vec_Ptr_t *)pBox->pCopy, j, NULL );
            }
 
            // free the bundles
            Vec_PtrFree( (Vec_Ptr_t *)pBox->pCopy );
            pBox->pCopy = NULL;
        }
    }
    return 1;
}

Here is the call graph for this function:

Ver_ParseFile()

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

MACRO DEFINITIONS ///.

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

Synopsis [File parser.]

Description []

SideEffects []

SeeAlso []

Definition at line 165 of file verCore.c.

{
    Ver_Man_t * p;
    Abc_Des_t * pDesign;
    // start the parser
    p = Ver_ParseStart( pFileName, pGateLib );
    p->fMapped    = glo_fMapped;
    p->fCheck     = fCheck;
    p->fUseMemMan = fUseMemMan;
    if ( glo_fMapped )
    {
        Hop_ManStop((Hop_Man_t *)p->pDesign->pManFunc);
        p->pDesign->pManFunc = NULL;
    }
    // parse the file
    Ver_ParseInternal( p );
    // save the result
    pDesign = p->pDesign;
    p->pDesign = NULL;
    // stop the parser
    Ver_ParseStop( p );
    return pDesign;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ver_ParseFindNet()

Abc_Obj_t * Ver_ParseFindNet	(	Abc_Ntk_t *	pNtk,
		char *	pName )

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 328 of file verCore.c.

{
    Abc_Obj_t * pObj;
    if ( (pObj = Abc_NtkFindNet(pNtk, pName)) )
        return pObj;
    if ( !strcmp( pName, "1\'b0" ) || !strcmp( pName, "1\'bx" ) )
        return Abc_NtkFindOrCreateNet( pNtk, "1\'b0" );
    if ( !strcmp( pName, "1\'b1" ) )
        return Abc_NtkFindOrCreateNet( pNtk, "1\'b1" );
    return NULL;
}

Here is the call graph for this function:

Ver_ParseFindOrCreateNetwork()

Abc_Ntk_t * Ver_ParseFindOrCreateNetwork	(	Ver_Man_t *	pMan,
		char *	pName )

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 301 of file verCore.c.

{
    Abc_Ntk_t * pNtkNew;
    // check if the network exists
    if ( (pNtkNew = Abc_DesFindModelByName( pMan->pDesign, pName )) )
        return pNtkNew;
//printf( "Creating network %s.\n", pName );
    // create new network
    pNtkNew = Abc_NtkAlloc( ABC_NTK_NETLIST, ABC_FUNC_BLACKBOX, pMan->fUseMemMan );
    pNtkNew->pName = Extra_UtilStrsav( pName );
    pNtkNew->pSpec = NULL;
    // add module to the design
    Abc_DesAddModel( pMan->pDesign, pNtkNew );
    return pNtkNew;
}

Here is the call graph for this function:

Ver_ParseFormalNetsAreDriven()

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

{
    Ver_Bundle_t * pBundle = NULL;
    Abc_Obj_t * pBox, * pNet;
    int k, j, m;
    // go through instances of this type
    Vec_PtrForEachEntry( Abc_Obj_t *, (Vec_Ptr_t *)pNtk->pData, pBox, k )
    {
        // find a bundle with the given name in this instance
        Vec_PtrForEachEntryReverse( Ver_Bundle_t *, (Vec_Ptr_t *)pBox->pCopy, pBundle, j )
            if ( pBundle && !strcmp( pBundle->pNameFormal, pNameFormal ) )
                break;
        // skip non-driven bundles
        if ( j == Vec_PtrSize((Vec_Ptr_t *)pBox->pCopy) )
            continue;
        // check if all nets are driven in this bundle
        assert(pBundle); // Verify that pBundle was assigned to.
        Vec_PtrForEachEntry( Abc_Obj_t *, pBundle->vNetsActual, pNet, m )
            if ( Abc_ObjFaninNum(pNet) > 0 )
                return 1;
    }
    return 0;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ver_ParseFreeBundle()

void Ver_ParseFreeBundle

(

Ver_Bundle_t *

pBundle

)

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

Synopsis [Connects one box to the network]

Description []

SideEffects []

SeeAlso []

Definition at line 2055 of file verCore.c.

{
    ABC_FREE( pBundle->pNameFormal );
    Vec_PtrFree( pBundle->vNetsActual );
    ABC_FREE( pBundle );
}

Here is the caller graph for this function:

Ver_ParseGetNondrivenBundle()

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

{
    Ver_Bundle_t * pBundle;
    Abc_Obj_t * pBox, * pNet;
    int k, m;
    // go through instances of this type
    Vec_PtrForEachEntry( Abc_Obj_t *, (Vec_Ptr_t *)pNtk->pData, pBox, k )
    {
        if ( Counter >= Vec_PtrSize((Vec_Ptr_t *)pBox->pCopy) )
            continue;
        // get the bundle given distance away
        pBundle = (Ver_Bundle_t *)Vec_PtrEntry( (Vec_Ptr_t *)pBox->pCopy, Vec_PtrSize((Vec_Ptr_t *)pBox->pCopy) - 1 - Counter );
        if ( pBundle == NULL )
            continue;
        // go through the actual nets of this bundle
        Vec_PtrForEachEntry( Abc_Obj_t *, pBundle->vNetsActual, pNet, m )
            if ( !Abc_ObjFaninNum(pNet) && !Ver_ParseFormalNetsAreDriven(pNtk, pBundle->pNameFormal) ) // non-driven
                return pBundle;
    }
    return NULL;
}

Here is the call graph for this function:

Ver_ParseInsertsSuffix()

int Ver_ParseInsertsSuffix	(	Ver_Man_t *	pMan,
		char *	pWord,
		int	nMsb,
		int	nLsb )

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 587 of file verCore.c.

{
    unsigned Value;
    if ( pMan->tName2Suffix == NULL )
        pMan->tName2Suffix = st__init_table( strcmp, st__strhash );
    if ( st__is_member( pMan->tName2Suffix, pWord ) )
        return 1;
    assert( nMsb >= 0 && nMsb < 128 );
    assert( nLsb >= 0 && nLsb < 128 );
    Value = (nMsb << 8) | nLsb;
    st__insert( pMan->tName2Suffix, Extra_UtilStrsav(pWord), (char *)(ABC_PTRUINT_T)Value );
    return 1;
}

Here is the call graph for this function:

Ver_ParseLookupSuffix()

int Ver_ParseLookupSuffix	(	Ver_Man_t *	pMan,
		char *	pWord,
		int *	pnMsb,
		int *	pnLsb )

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 563 of file verCore.c.

{
    unsigned Value;
    *pnMsb = *pnLsb = -1;
    if ( pMan->tName2Suffix == NULL )
        return 1;
    if ( ! st__lookup( pMan->tName2Suffix, (char *)pWord, (char **)&Value ) )
        return 1;
    *pnMsb = (Value >> 8) & 0xff;
    *pnLsb = Value & 0xff;
    return 1;
}

Here is the call graph for this function:

Ver_ParseMaxBoxSize()

int Ver_ParseMaxBoxSize

(

Vec_Ptr_t *

vUndefs

)

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 2711 of file verCore.c.

{
    Abc_Ntk_t * pNtk;
    Abc_Obj_t * pBox;
    int i, k, nMaxSize = 0;
    // go through undef box types
    Vec_PtrForEachEntry( Abc_Ntk_t *, vUndefs, pNtk, i )
        // go through instances of this type
        Vec_PtrForEachEntry( Abc_Obj_t *, (Vec_Ptr_t *)pNtk->pData, pBox, k )
            // check the number of bundles of this instance
            if ( nMaxSize < Vec_PtrSize((Vec_Ptr_t *)pBox->pCopy) )
                nMaxSize = Vec_PtrSize((Vec_Ptr_t *)pBox->pCopy);
    return nMaxSize;
}

Ver_ParsePrintErrorMessage()

void Ver_ParsePrintErrorMessage

(

Ver_Man_t *

p

)

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 278 of file verCore.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Ver_ParsePrintLog()

void Ver_ParsePrintLog

(

Ver_Man_t *

pMan

)

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 2737 of file verCore.c.

{
    Abc_Ntk_t * pNtk, * pNtkBox;
    Abc_Obj_t * pBox;
    FILE * pFile;
    char * pNameGeneric;
    char Buffer[1000];
    int i, k, Count1 = 0;
 
    // open the log file
    pNameGeneric = Extra_FileNameGeneric( pMan->pFileName );
    sprintf( Buffer, "%s.log", pNameGeneric );
    ABC_FREE( pNameGeneric );
    pFile = fopen( Buffer, "w" );
 
    // count the total number of instances and how many times they occur
    Vec_PtrForEachEntry( Abc_Ntk_t *, pMan->pDesign->vModules, pNtk, i )
        pNtk->fHieVisited = 0;
    Vec_PtrForEachEntry( Abc_Ntk_t *, pMan->pDesign->vModules, pNtk, i )
        Abc_NtkForEachBox( pNtk, pBox, k )
        {
            if ( Abc_ObjIsLatch(pBox) )
                continue;
            pNtkBox = (Abc_Ntk_t *)pBox->pData;
            if ( pNtkBox == NULL )
                continue;
            pNtkBox->fHieVisited++;
        }
    // print each box and its stats
    fprintf( pFile, "The hierarhical design %s contains %d modules:\n", pMan->pFileName, Vec_PtrSize(pMan->pDesign->vModules) );
    Vec_PtrForEachEntry( Abc_Ntk_t *, pMan->pDesign->vModules, pNtk, i )
    {
        fprintf( pFile, "%-50s : ", Abc_NtkName(pNtk) );
        if ( !Ver_NtkIsDefined(pNtk) )
            fprintf( pFile, "undefbox" );
        else if ( Abc_NtkHasBlackbox(pNtk) )
            fprintf( pFile, "blackbox" );
        else
            fprintf( pFile, "logicbox" );
        fprintf( pFile, " instantiated %6d times ", pNtk->fHieVisited );
//        fprintf( pFile, "\n   " );
        fprintf( pFile, " pi = %4d", Abc_NtkPiNum(pNtk) );
        fprintf( pFile, " po = %4d", Abc_NtkPoNum(pNtk) );
        fprintf( pFile, " nd = %8d",  Abc_NtkNodeNum(pNtk) );
        fprintf( pFile, " lat = %6d",  Abc_NtkLatchNum(pNtk) );
        fprintf( pFile, " box = %6d", Abc_NtkBoxNum(pNtk)-Abc_NtkLatchNum(pNtk) );
        fprintf( pFile, "\n" );
        Count1 += (Abc_NtkPoNum(pNtk) == 1);
    }
    Vec_PtrForEachEntry( Abc_Ntk_t *, pMan->pDesign->vModules, pNtk, i )
        pNtk->fHieVisited = 0;
    fprintf( pFile, "The number of modules with one output = %d (%.2f %%).\n", Count1, 100.0 * Count1/Vec_PtrSize(pMan->pDesign->vModules) ); 
 
    // report instances with dangling outputs
    if ( Vec_PtrSize(pMan->pDesign->vModules) > 1 )
    {
        Vec_Ptr_t * vBundles;
        Ver_Bundle_t * pBundle;
        int j, nActNets, Counter = 0;
        // count the number of instances with dangling outputs
        Vec_PtrForEachEntry( Abc_Ntk_t *, pMan->pDesign->vModules, pNtk, i )
        {
            Abc_NtkForEachBox( pNtk, pBox, k )
            {
                if ( Abc_ObjIsLatch(pBox) )
                    continue;
                vBundles = (Vec_Ptr_t *)pBox->pCopy;
                pNtkBox = (Abc_Ntk_t *)pBox->pData;
                if ( pNtkBox == NULL )
                    continue;
                if ( !Ver_NtkIsDefined(pNtkBox) )
                    continue;
                // count the number of actual nets
                nActNets = 0;
                Vec_PtrForEachEntry( Ver_Bundle_t *, vBundles, pBundle, j )
                    nActNets += Vec_PtrSize(pBundle->vNetsActual);
                // the box is defined and will be connected
                if ( nActNets != Abc_NtkPiNum(pNtkBox) + Abc_NtkPoNum(pNtkBox) )
                    Counter++;
            }
        }
        if ( Counter == 0 )
            fprintf( pFile, "The outputs of all box instances are connected.\n" );
        else
        {
            fprintf( pFile, "\n" );
            fprintf( pFile, "The outputs of %d box instances are not connected:\n", Counter );
            // enumerate through the boxes
            Vec_PtrForEachEntry( Abc_Ntk_t *, pMan->pDesign->vModules, pNtk, i )
            {
                Abc_NtkForEachBox( pNtk, pBox, k )
                {
                    if ( Abc_ObjIsLatch(pBox) )
                        continue;
                    vBundles = (Vec_Ptr_t *)pBox->pCopy;
                    pNtkBox = (Abc_Ntk_t *)pBox->pData;
                    if ( pNtkBox == NULL )
                        continue;
                    if ( !Ver_NtkIsDefined(pNtkBox) )
                        continue;
                    // count the number of actual nets
                    nActNets = 0;
                    Vec_PtrForEachEntry( Ver_Bundle_t *, vBundles, pBundle, j )
                        nActNets += Vec_PtrSize(pBundle->vNetsActual);
                    // the box is defined and will be connected
                    if ( nActNets != Abc_NtkPiNum(pNtkBox) + Abc_NtkPoNum(pNtkBox) )
                        fprintf( pFile, "In module \"%s\" instance \"%s\" of box \"%s\" has different numbers of actual/formal nets (%d/%d).\n",
                            Abc_NtkName(pNtk), Abc_ObjName(pBox), Abc_NtkName(pNtkBox), nActNets, Abc_NtkPiNum(pNtkBox) + Abc_NtkPoNum(pNtkBox) );
                }
            }
        }
    }
    fclose( pFile );
    printf( "Hierarchy statistics can be found in log file \"%s\".\n", Buffer );
}

Here is the call graph for this function:

Ver_ParseReportUndefBoxes()

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

{
    Abc_Ntk_t * pNtk;
    Abc_Obj_t * pBox;
    int i, k, nBoxes;
    // clean 
    nBoxes = 0;
    Vec_PtrForEachEntry( Abc_Ntk_t *, pMan->pDesign->vModules, pNtk, i )
    {
        pNtk->fHiePath = 0;
        if ( !Ver_NtkIsDefined(pNtk) )
            nBoxes++;
    }
    // count
    Vec_PtrForEachEntry( Abc_Ntk_t *, pMan->pDesign->vModules, pNtk, i )
        Abc_NtkForEachBlackbox( pNtk, pBox, k )
            if ( pBox->pData && !Ver_NtkIsDefined((Abc_Ntk_t *)pBox->pData) )
                ((Abc_Ntk_t *)pBox->pData)->fHiePath++;
    // print the stats
    printf( "Warning: The design contains %d undefined object types interpreted as blackboxes:\n", nBoxes );
    Vec_PtrForEachEntry( Abc_Ntk_t *, pMan->pDesign->vModules, pNtk, i )
        if ( !Ver_NtkIsDefined(pNtk) )
            printf( "%s (%d)  ", Abc_NtkName(pNtk), pNtk->fHiePath );
    printf( "\n" );
    // clean 
    Vec_PtrForEachEntry( Abc_Ntk_t *, pMan->pDesign->vModules, pNtk, i )
        pNtk->fHiePath = 0;
}

Ver_ParseSignalPrefix()

int Ver_ParseSignalPrefix	(	Ver_Man_t *	pMan,
		char **	ppWord,
		int *	pnMsb,
		int *	pnLsb )

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 635 of file verCore.c.

{
    char * pWord = *ppWord, * pTemp;
    int nMsb, nLsb;
    assert( pWord[0] == '[' );
    // get the beginning
    nMsb = atoi( pWord + 1 );
    // find the splitter
    while ( *pWord && *pWord != ':' && *pWord != ']' )
        pWord++;
    if ( *pWord == 0 )
    {
        sprintf( pMan->sError, "Cannot find closing bracket in this line." );
        Ver_ParsePrintErrorMessage( pMan );
        return 0;
    }
    if ( *pWord == ']' )
        nLsb = nMsb;
    else
    {
        assert( *pWord == ':' );
        nLsb = atoi( pWord + 1 );
        // find the closing parenthesis
        while ( *pWord && *pWord != ']' )
            pWord++;
        if ( *pWord == 0 )
        {
            sprintf( pMan->sError, "Cannot find closing bracket in this line." );
            Ver_ParsePrintErrorMessage( pMan );
            return 0;
        }
        assert( *pWord == ']' );
        pWord++;
 
        // fix the case when <name> follows after [] without space
        if ( *pWord == '\\' )
        {
            pWord++;
            pTemp = pWord;
            while ( *pTemp && *pTemp != ' ' )
                pTemp++;
            if ( *pTemp == ' ' )
                *pTemp = 0;
        }
    }
    assert( nMsb >= 0 && nLsb >= 0 );
    // return
    *ppWord = pWord;
    *pnMsb = nMsb;
    *pnLsb = nLsb;
    return 1;
}

Here is the call graph for this function:

Ver_ParseSignalSuffix()

int Ver_ParseSignalSuffix	(	Ver_Man_t *	pMan,
		char *	pWord,
		int *	pnMsb,
		int *	pnLsb )

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 699 of file verCore.c.

{
    char * pCur;
    int Length;
    Length = strlen(pWord);
    assert( pWord[Length-1] == ']' );
    // walk backward
    for ( pCur = pWord + Length - 2; pCur != pWord; pCur-- )
        if ( *pCur == ':' || *pCur == '[' )
            break;
    if ( pCur == pWord )
    {
        sprintf( pMan->sError, "Cannot find opening bracket in signal name %s.", pWord );
        Ver_ParsePrintErrorMessage( pMan );
        return 0;
    }
    if ( *pCur == '[' )
    {
        *pnMsb = *pnLsb = atoi(pCur+1);
        *pCur = 0;
        return 1;
    }
    assert( *pCur == ':' );
    // get the end of the interval
    *pnLsb = atoi(pCur+1);
    // find the beginning
    for ( pCur = pWord + Length - 2; pCur != pWord; pCur-- )
        if ( *pCur == '[' )
            break;
    if ( pCur == pWord )
    {
        sprintf( pMan->sError, "Cannot find opening bracket in signal name %s.", pWord );
        Ver_ParsePrintErrorMessage( pMan );
        return 0;
    }
    assert( *pCur == '[' );
    // get the beginning of the interval
    *pnMsb = atoi(pCur+1);
    // cut the word
    *pCur = 0;
    return 1;
}

Here is the call graph for this function:

Variable Documentation

glo_fMapped

int glo_fMapped = 0

Definition at line 80 of file verCore.c.