diff options
Diffstat (limited to 'src/temp/ver')
| -rw-r--r-- | src/temp/ver/ver.h | 111 | ||||
| -rw-r--r-- | src/temp/ver/verCore.c | 933 | ||||
| -rw-r--r-- | src/temp/ver/verFormula.c | 408 | ||||
| -rw-r--r-- | src/temp/ver/verParse.c | 111 | ||||
| -rw-r--r-- | src/temp/ver/verStream.c | 435 | ||||
| -rw-r--r-- | src/temp/ver/verWords.c | 48 | ||||
| -rw-r--r-- | src/temp/ver/ver_.c | 48 |
7 files changed, 2094 insertions, 0 deletions
diff --git a/src/temp/ver/ver.h b/src/temp/ver/ver.h new file mode 100644 index 00000000..ea1613c0 --- /dev/null +++ b/src/temp/ver/ver.h @@ -0,0 +1,111 @@ +/**CFile**************************************************************** + + FileName [ver.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Verilog parser.] + + Synopsis [External declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - August 19, 2006.] + + Revision [$Id: ver.h,v 1.00 2006/08/19 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef __VER_H__ +#define __VER_H__ + +#ifdef __cplusplus +extern "C" { +#endif + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +#include <stdio.h> +#include "abc.h" + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Ver_Man_t_ Ver_Man_t; +typedef struct Ver_Stream_t_ Ver_Stream_t; + +struct Ver_Man_t_ +{ + // input file stream + char * pFileName; + Ver_Stream_t * pReader; + ProgressBar * pProgress; + // current network and library + Abc_Ntk_t * pNtkCur; // the network under construction + st_table * pLibrary; // the current design library + st_table * pGateLib; // the current technology library + // error recovery + FILE * Output; + int fTopLevel; + int fError; + char sError[2000]; + // intermediate structures + Vec_Ptr_t * vNames; + Vec_Ptr_t * vStackFn; + Vec_Int_t * vStackOp; +}; + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// ITERATORS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== verCore.c ========================================================*/ +extern st_table * Ver_ParseFile( char * pFileName, st_table * pGateLib, int fCheck ); +extern void Ver_ParsePrintErrorMessage( Ver_Man_t * p ); +/*=== verFormula.c ========================================================*/ +extern DdNode * Ver_FormulaParser( char * pFormula, DdManager * dd, Vec_Ptr_t * vNames, Vec_Ptr_t * vStackFn, Vec_Int_t * vStackOp, char * pErrorMessage ); +/*=== verParse.c ========================================================*/ +extern int Ver_ParseSkipComments( Ver_Man_t * p ); +extern char * Ver_ParseGetName( Ver_Man_t * p ); +/*=== verStream.c ========================================================*/ +extern Ver_Stream_t * Ver_StreamAlloc( char * pFileName ); +extern void Ver_StreamFree( Ver_Stream_t * p ); +extern char * Ver_StreamGetFileName( Ver_Stream_t * p ); +extern int Ver_StreamGetFileSize( Ver_Stream_t * p ); +extern int Ver_StreamGetCurPosition( Ver_Stream_t * p ); +extern int Ver_StreamGetLineNumber( Ver_Stream_t * p ); + +extern int Ver_StreamIsOkey( Ver_Stream_t * p ); +extern char Ver_StreamScanChar( Ver_Stream_t * p ); +extern char Ver_StreamPopChar( Ver_Stream_t * p ); +extern void Ver_StreamSkipChars( Ver_Stream_t * p, char * pCharsToSkip ); +extern void Ver_StreamSkipToChars( Ver_Stream_t * p, char * pCharsToStop ); +extern char * Ver_StreamGetWord( Ver_Stream_t * p, char * pCharsToStop ); + +#ifdef __cplusplus +} +#endif + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/temp/ver/verCore.c b/src/temp/ver/verCore.c new file mode 100644 index 00000000..8ef38aad --- /dev/null +++ b/src/temp/ver/verCore.c @@ -0,0 +1,933 @@ +/**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 $] + +***********************************************************************/ + +#include "ver.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +// types of verilog signals +typedef enum { + VER_SIG_NONE = 0, + VER_SIG_INPUT, + VER_SIG_OUTPUT, + VER_SIG_INOUT, + VER_SIG_REG, + VER_SIG_WIRE +} Ver_SignalType_t; + +static void Ver_ParseFreeData( Ver_Man_t * p ); +static void Ver_ParseInternal( Ver_Man_t * p, int fCheck ); +static int Ver_ParseModule( Ver_Man_t * p ); +static int Ver_ParseSignal( Ver_Man_t * p, Ver_SignalType_t SigType ); +static int Ver_ParseAssign( Ver_Man_t * p ); +static int Ver_ParseAlways( Ver_Man_t * p ); +static int Ver_ParseInitial( Ver_Man_t * p ); +static int Ver_ParseGate( Ver_Man_t * p, Abc_Ntk_t * pNtkGate ); + +static Abc_Obj_t * Ver_ParseCreatePi( Abc_Ntk_t * pNtk, char * pName ); +static Abc_Obj_t * Ver_ParseCreatePo( Abc_Ntk_t * pNtk, char * pName ); +static Abc_Obj_t * Ver_ParseCreateConst( Abc_Ntk_t * pNtk, char * pName, bool fConst1 ); +static Abc_Obj_t * Ver_ParseCreateLatch( Abc_Ntk_t * pNtk, char * pNetLI, char * pNetLO ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [File parser.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +st_table * Ver_ParseFile( char * pFileName, st_table * pGateLib, int fCheck ) +{ + Ver_Man_t * p; + st_table * pLibrary; + // start the file reader + p = ALLOC( Ver_Man_t, 1 ); + memset( p, 0, sizeof(Ver_Man_t) ); + p->pFileName = pFileName; + p->pReader = Ver_StreamAlloc( pFileName ); + p->pLibrary = st_init_table( st_ptrcmp, st_ptrhash ); + p->pGateLib = pGateLib; + p->Output = stdout; + p->pProgress = Extra_ProgressBarStart( stdout, Ver_StreamGetFileSize(p->pReader) ); + p->vNames = Vec_PtrAlloc( 100 ); + p->vStackFn = Vec_PtrAlloc( 100 ); + p->vStackOp = Vec_IntAlloc( 100 ); + // parse the file + Ver_ParseInternal( p, fCheck ); + // stop the parser + assert( p->pNtkCur == NULL ); + pLibrary = p->pLibrary; + Ver_StreamFree( p->pReader ); + Extra_ProgressBarStop( p->pProgress ); + Vec_PtrFree( p->vNames ); + Vec_PtrFree( p->vStackFn ); + Vec_IntFree( p->vStackOp ); + free( p ); + return pLibrary; +} + +/**Function************************************************************* + + Synopsis [File parser.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ver_ParseFreeLibrary( st_table * pLibVer ) +{ + st_generator * gen; + Abc_Ntk_t * pNtk; + char * pName; + st_foreach_item( pLibVer, gen, (char**)&pName, (char**)&pNtk ) + Abc_NtkDelete( pNtk ); + st_free_table( pLibVer ); +} + +/**Function************************************************************* + + Synopsis [File parser.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ver_ParseFreeData( Ver_Man_t * p ) +{ + if ( p->pNtkCur ) + { + Abc_NtkDelete( p->pNtkCur ); + p->pNtkCur = NULL; + } + if ( p->pLibrary ) + { + Ver_ParseFreeLibrary( p->pLibrary ); + p->pLibrary = NULL; + } +} + +/**Function************************************************************* + + Synopsis [File parser.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ver_ParseInternal( Ver_Man_t * pMan, int fCheck ) +{ + char * pToken; + while ( 1 ) + { + // get the next token + pToken = Ver_ParseGetName( pMan ); + if ( pToken == NULL ) + break; + if ( strcmp( pToken, "module" ) ) + { + sprintf( pMan->sError, "Cannot read \"module\" directive." ); + Ver_ParsePrintErrorMessage( pMan ); + return; + } + // parse the module + if ( !Ver_ParseModule( pMan ) ) + return; + // check the network for correctness + if ( fCheck && !Abc_NtkCheckRead( pMan->pNtkCur ) ) + { + pMan->fTopLevel = 1; + sprintf( pMan->sError, "The network check has failed.", pMan->pNtkCur->pName ); + Ver_ParsePrintErrorMessage( pMan ); + return; + } + // add the module to the hash table + if ( st_is_member( pMan->pLibrary, pMan->pNtkCur->pName ) ) + { + pMan->fTopLevel = 1; + sprintf( pMan->sError, "Module \"%s\" is defined more than once.", pMan->pNtkCur->pName ); + Ver_ParsePrintErrorMessage( pMan ); + return; + } + st_insert( pMan->pLibrary, pMan->pNtkCur->pName, (char *)pMan->pNtkCur ); + pMan->pNtkCur = NULL; + } +} + +/**Function************************************************************* + + Synopsis [Prints the error message including the file name and line number.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ver_ParsePrintErrorMessage( Ver_Man_t * p ) +{ + 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 ); +} + + + +/**Function************************************************************* + + Synopsis [Parses one Verilog module.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ver_ParseModule( Ver_Man_t * pMan ) +{ + Ver_Stream_t * p = pMan->pReader; + Abc_Ntk_t * pNtk, * pNtkTemp; + char * pWord; + int RetValue; + char Symbol; + + // start the current network + assert( pMan->pNtkCur == NULL ); + pNtk = pMan->pNtkCur = Abc_NtkAlloc( ABC_NTK_NETLIST, ABC_FUNC_BLACKBOX ); +// pNtk = pMan->pNtkCur = Abc_NtkAlloc( ABC_NTK_NETLIST, ABC_FUNC_BDD ); + + // get the network name + pWord = Ver_ParseGetName( pMan ); + pNtk->pName = Extra_UtilStrsav( pWord ); + pNtk->pSpec = Extra_UtilStrsav( pMan->pFileName ); + + // create constant nodes and nets + Abc_NtkFindOrCreateNet( pNtk, "1'b0" ); + Abc_NtkFindOrCreateNet( pNtk, "1'b1" ); + Ver_ParseCreateConst( pNtk, "1'b0", 0 ); + Ver_ParseCreateConst( pNtk, "1'b1", 1 ); + + // make sure we stopped at the opening paranthesis + if ( Ver_StreamScanChar(p) != '(' ) + { + sprintf( pMan->sError, "Cannot find \"(\" after \"module\".", pNtk->pName ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + + // skip to the end of parantheses + while ( 1 ) + { + Ver_StreamSkipToChars( p, ",/)" ); + while ( Ver_StreamScanChar(p) == '/' ) + { + Ver_ParseSkipComments( pMan ); + Ver_StreamSkipToChars( p, ",/)" ); + } + Symbol = Ver_StreamPopChar(p); + if ( Symbol== ')' ) + break; + } + if ( !Ver_ParseSkipComments( pMan ) ) + return 0; + Symbol = Ver_StreamPopChar(p); + assert( Symbol == ';' ); + + // parse the inputs/outputs/registers/wires/inouts + while ( 1 ) + { + pWord = Ver_ParseGetName( pMan ); + if ( pWord == NULL ) + return 0; + if ( !strcmp( pWord, "input" ) ) + RetValue = Ver_ParseSignal( pMan, VER_SIG_INPUT ); + else if ( !strcmp( pWord, "output" ) ) + RetValue = Ver_ParseSignal( pMan, VER_SIG_OUTPUT ); + else if ( !strcmp( pWord, "reg" ) ) + RetValue = Ver_ParseSignal( pMan, VER_SIG_REG ); + else if ( !strcmp( pWord, "wire" ) ) + RetValue = Ver_ParseSignal( pMan, VER_SIG_WIRE ); + else if ( !strcmp( pWord, "inout" ) ) + RetValue = Ver_ParseSignal( pMan, VER_SIG_INOUT ); + else + break; + if ( RetValue == 0 ) + return 0; + } + + // parse the remaining statements + while ( 1 ) + { + Extra_ProgressBarUpdate( pMan->pProgress, Ver_StreamGetCurPosition(p), NULL ); + if ( !strcmp( pWord, "assign" ) ) + RetValue = Ver_ParseAssign( pMan ); + else if ( !strcmp( pWord, "always" ) ) + RetValue = Ver_ParseAlways( pMan ); + else if ( !strcmp( pWord, "initial" ) ) + RetValue = Ver_ParseInitial( pMan ); + else if ( !strcmp( pWord, "endmodule" ) ) + { + // if nothing is known, set the functionality to be black box + Abc_NtkFinalizeRead( pNtk ); + break; + } + else if ( pMan->pGateLib && st_lookup(pMan->pGateLib, pWord, (char**)&pNtkTemp) ) // gate library + RetValue = Ver_ParseGate( pMan, pNtkTemp ); + else if ( pMan->pLibrary && st_lookup(pMan->pLibrary, pWord, (char**)&pNtkTemp) ) // current design + RetValue = Ver_ParseGate( pMan, pNtkTemp ); + else + { + printf( "Cannot find \"%s\".\n", pWord ); + Ver_StreamSkipToChars( p, ";" ); + Ver_StreamPopChar(p); + +// sprintf( pMan->sError, "Cannot find \"%s\" in the library.", pWord ); +// Ver_ParsePrintErrorMessage( pMan ); +// return 0; + } + if ( RetValue == 0 ) + return 0; + // get new word + pWord = Ver_ParseGetName( pMan ); + if ( pWord == NULL ) + return 0; + } + + if ( pNtk->ntkFunc == ABC_FUNC_BDD ) + { + Abc_Obj_t * pObj; + pObj = Abc_ObjFanin0( Abc_NtkFindNet( pNtk, "1'b0" ) ); + pObj->pData = Cudd_ReadLogicZero( pNtk->pManFunc ); + pObj = Abc_ObjFanin0( Abc_NtkFindNet( pNtk, "1'b1" ) ); + pObj->pData = Cudd_ReadOne( pNtk->pManFunc ); + Cudd_Ref( Cudd_ReadOne( pNtk->pManFunc ) ); + Cudd_Ref( Cudd_ReadOne( pNtk->pManFunc ) ); + } + return 1; +} + +/**Function************************************************************* + + Synopsis [Parses one directive.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ver_ParseSignal( Ver_Man_t * pMan, Ver_SignalType_t SigType ) +{ + Ver_Stream_t * p = pMan->pReader; + Abc_Ntk_t * pNtk = pMan->pNtkCur; + char * pWord; + char Symbol; + while ( 1 ) + { + pWord = Ver_ParseGetName( pMan ); + if ( pWord == NULL ) + return 0; + if ( SigType == VER_SIG_INPUT || SigType == VER_SIG_INOUT ) + Ver_ParseCreatePi( pNtk, pWord ); + if ( SigType == VER_SIG_OUTPUT || SigType == VER_SIG_INOUT ) + Ver_ParseCreatePo( pNtk, pWord ); + if ( SigType == VER_SIG_WIRE || SigType == VER_SIG_REG ) + Abc_NtkFindOrCreateNet( pNtk, pWord ); + Symbol = Ver_StreamPopChar(p); + if ( Symbol == ',' ) + continue; + if ( Symbol == ';' ) + return 1; + break; + } + sprintf( pMan->sError, "Cannot parse signal line (expected , or ;)." ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; +} + +/**Function************************************************************* + + Synopsis [Parses one directive.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ver_ParseAssign( Ver_Man_t * pMan ) +{ + Ver_Stream_t * p = pMan->pReader; + Abc_Ntk_t * pNtk = pMan->pNtkCur; + Abc_Obj_t * pNode, * pNet; + char * pWord, * pName, * pEquation; + DdNode * bFunc; + char Symbol; + int i, Length; + + // convert from the mapped netlist into the BDD netlist + if ( pNtk->ntkFunc == ABC_FUNC_BLACKBOX ) + { + pNtk->ntkFunc = ABC_FUNC_BDD; + pNtk->pManFunc = Cudd_Init( 20, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); + } + else if ( pNtk->ntkFunc != ABC_FUNC_BDD ) + { + sprintf( pMan->sError, "The network %s appears to mapped gates and assign statements. Currently such network are not allowed. One way to fix this problem is to replace assigns by buffers from the library.", pMan->pNtkCur ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + + while ( 1 ) + { + // get the name of the output signal + pWord = Ver_ParseGetName( pMan ); + if ( pWord == NULL ) + return 0; + // get the fanout net + pNet = Abc_NtkFindNet( pNtk, pWord ); + if ( pNet == NULL ) + { + sprintf( pMan->sError, "Cannot read the assign statement for %s (output wire is not defined).", pWord ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + // get the equal sign + if ( Ver_StreamPopChar(p) != '=' ) + { + sprintf( pMan->sError, "Cannot read the assign statement for %s (expected equality sign).", pWord ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + // skip the comments + if ( !Ver_ParseSkipComments( pMan ) ) + return 0; + // get the second name + pEquation = Ver_StreamGetWord( p, ",;" ); + if ( pEquation == NULL ) + return 0; + + // parse the formula + bFunc = Ver_FormulaParser( pEquation, pNtk->pManFunc, pMan->vNames, pMan->vStackFn, pMan->vStackOp, pMan->sError ); + if ( bFunc == NULL ) + { + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + Cudd_Ref( bFunc ); + // create the node with the given inputs + pNode = Abc_NtkCreateNode( pMan->pNtkCur ); + pNode->pData = bFunc; + Abc_ObjAddFanin( pNet, pNode ); + // connect to fanin nets + for ( i = 0; i < Vec_PtrSize(pMan->vNames)/2; i++ ) + { + // get the name of this signal + Length = (int)Vec_PtrEntry( pMan->vNames, 2*i ); + pName = Vec_PtrEntry( pMan->vNames, 2*i + 1 ); + pName[Length] = 0; + // find the corresponding net + pNet = Abc_NtkFindNet( pNtk, pName ); + if ( pNet == NULL ) + { + sprintf( pMan->sError, "Cannot read the assign statement for %s (input wire %d is not defined).", pWord, pName ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + Abc_ObjAddFanin( pNode, pNet ); + } + Symbol = Ver_StreamPopChar(p); + if ( Symbol == ',' ) + continue; + if ( Symbol == ';' ) + return 1; + } + return 1; +} + +/**Function************************************************************* + + Synopsis [Parses one directive.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ver_ParseAlways( Ver_Man_t * pMan ) +{ + Ver_Stream_t * p = pMan->pReader; + Abc_Ntk_t * pNtk = pMan->pNtkCur; + Abc_Obj_t * pNet, * pNet2; + char * pWord, * pWord2; + char Symbol; + // parse the directive + pWord = Ver_ParseGetName( pMan ); + if ( pWord == NULL ) + return 0; + if ( strcmp( pWord, "begin" ) ) + { + sprintf( pMan->sError, "Cannot parse the always statement (expected \"begin\")." ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + // iterate over the initial states + while ( 1 ) + { + // get the name of the output signal + pWord = Ver_ParseGetName( pMan ); + if ( pWord == NULL ) + return 0; + // look for the end of directive + if ( !strcmp( pWord, "end" ) ) + break; + // get the fanout net + pNet = Abc_NtkFindNet( pNtk, pWord ); + if ( pNet == NULL ) + { + sprintf( pMan->sError, "Cannot read the always statement for %s (output wire is not defined).", pWord ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + // get the equal sign + if ( Ver_StreamPopChar(p) != '=' ) + { + sprintf( pMan->sError, "Cannot read the always statement for %s (expected equality sign).", pWord ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + // skip the comments + if ( !Ver_ParseSkipComments( pMan ) ) + return 0; + // get the second name + pWord2 = Ver_ParseGetName( pMan ); + if ( pWord2 == NULL ) + return 0; + // get the fanin net + pNet2 = Abc_NtkFindNet( pNtk, pWord2 ); + if ( pNet2 == NULL ) + { + sprintf( pMan->sError, "Cannot read the always statement for %s (input wire is not defined).", pWord2 ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + // create the latch + Ver_ParseCreateLatch( pNtk, pNet2->pData, pNet->pData ); + // remove the last symbol + Symbol = Ver_StreamPopChar(p); + assert( Symbol == ';' ); + } + return 1; +} + +/**Function************************************************************* + + Synopsis [Parses one directive.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ver_ParseInitial( Ver_Man_t * pMan ) +{ + Ver_Stream_t * p = pMan->pReader; + Abc_Ntk_t * pNtk = pMan->pNtkCur; + Abc_Obj_t * pNode, * pNet; + char * pWord, * pEquation; + char Symbol; + // parse the directive + pWord = Ver_ParseGetName( pMan ); + if ( pWord == NULL ) + return 0; + if ( strcmp( pWord, "begin" ) ) + { + sprintf( pMan->sError, "Cannot parse the initial statement (expected \"begin\")." ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + // iterate over the initial states + while ( 1 ) + { + // get the name of the output signal + pWord = Ver_ParseGetName( pMan ); + if ( pWord == NULL ) + return 0; + // look for the end of directive + if ( !strcmp( pWord, "end" ) ) + break; + // get the fanout net + pNet = Abc_NtkFindNet( pNtk, pWord ); + if ( pNet == NULL ) + { + sprintf( pMan->sError, "Cannot read the initial statement for %s (output wire is not defined).", pWord ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + // get the equal sign + if ( Ver_StreamPopChar(p) != '=' ) + { + sprintf( pMan->sError, "Cannot read the initial statement for %s (expected equality sign).", pWord ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + // skip the comments + if ( !Ver_ParseSkipComments( pMan ) ) + return 0; + // get the second name + pEquation = Ver_StreamGetWord( p, ";" ); + if ( pEquation == NULL ) + return 0; + // find the corresponding latch + pNode = Abc_ObjFanin0(pNet); + assert( Abc_ObjIsLatch(pNode) ); + // set the initial state + if ( pEquation[0] == '2' ) + Abc_LatchSetInitDc( pNode ); + else if ( pEquation[0] == '1') + Abc_LatchSetInit1( pNode ); + else if ( pEquation[0] == '0' ) + Abc_LatchSetInit0( pNode ); + else + { + sprintf( pMan->sError, "Incorrect initial value of the latch %s (expected equality sign).", pWord ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + // remove the last symbol + Symbol = Ver_StreamPopChar(p); + assert( Symbol == ';' ); + } + return 1; +} + +/**Function************************************************************* + + Synopsis [Parses one directive.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtkGate ) +{ + Ver_Stream_t * p = pMan->pReader; + Abc_Ntk_t * pNtk = pMan->pNtkCur; + Abc_Obj_t * pNetFormal, * pNetActual; + Abc_Obj_t * pObj, * pNode; + char * pWord, Symbol; + int i, fCompl; + + // convert from the mapped netlist into the BDD netlist + if ( pNtk->ntkFunc == ABC_FUNC_BLACKBOX ) + { + pNtk->ntkFunc = ABC_FUNC_MAP; + pNtk->pManFunc = pMan->pGateLib; + } + else if ( pNtk->ntkFunc != ABC_FUNC_MAP ) + { + sprintf( pMan->sError, "The network %s appears to contain both mapped gates and assign statements. Currently such network are not allowed. One way to fix this problem is to replace assigns by buffers from the library.", pMan->pNtkCur ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + + // clean the PI/PO pointers + Abc_NtkForEachPi( pNtkGate, pObj, i ) + pObj->pCopy = NULL; + Abc_NtkForEachPo( pNtkGate, pObj, i ) + pObj->pCopy = NULL; + // parse the directive and set the pointers to the PIs/POs of the gate + pWord = Ver_ParseGetName( pMan ); + if ( pWord == NULL ) + return 0; + // this is gate name - throw it away + if ( Ver_StreamPopChar(p) != '(' ) + { + sprintf( pMan->sError, "Cannot parse gate %s (expected opening paranthesis).", pNtkGate->pName ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + // parse pairs of formal/actural inputs + while ( 1 ) + { + // process one pair of formal/actual parameters + if ( Ver_StreamPopChar(p) != '.' ) + { + sprintf( pMan->sError, "Cannot parse gate %s (expected .).", pNtkGate->pName ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + + // parse the formal name + pWord = Ver_ParseGetName( pMan ); + if ( pWord == NULL ) + return 0; + // get the formal net + if ( Abc_NtkIsNetlist(pNtkGate) ) + pNetFormal = Abc_NtkFindNet( pNtkGate, pWord ); + else // if ( Abc_NtkIsStrash(pNtkGate) ) + pNetFormal = Abc_NtkFindTerm( pNtkGate, pWord ); + if ( pNetFormal == NULL ) + { + sprintf( pMan->sError, "Formal net is missing in gate %s.", pWord ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + + // open the paranthesis + if ( Ver_StreamPopChar(p) != '(' ) + { + sprintf( pMan->sError, "Cannot formal parameter %s of gate %s (expected opening paranthesis).", pWord, pNtkGate->pName ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + + // parse the actual name + pWord = Ver_ParseGetName( pMan ); + if ( pWord == NULL ) + return 0; + // check if the name is complemented + fCompl = (pWord[0] == '~'); + if ( fCompl ) + pWord++; + // get the actual net + pNetActual = Abc_NtkFindNet( pMan->pNtkCur, pWord ); + if ( pNetActual == NULL ) + { + sprintf( pMan->sError, "Actual net is missing in gate %s.", pWord ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + + // close the paranthesis + if ( Ver_StreamPopChar(p) != ')' ) + { + sprintf( pMan->sError, "Cannot formal parameter %s of gate %s (expected closing paranthesis).", pWord, pNtkGate->pName ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + + // process the pair + if ( Abc_ObjIsPi(Abc_ObjFanin0Ntk(pNetFormal)) ) // PI net + Abc_ObjFanin0Ntk(pNetFormal)->pCopy = pNetActual; // Abc_ObjNotCond( pNetActual, fCompl ); + else if ( Abc_ObjIsPo(Abc_ObjFanout0Ntk(pNetFormal)) ) // P0 net + { + assert( fCompl == 0 ); + Abc_ObjFanout0Ntk(pNetFormal)->pCopy = pNetActual; // Abc_ObjNotCond( pNetActual, fCompl ); + } + else + { + sprintf( pMan->sError, "Cannot match formal net %s with PI or PO of the gate %s.", pWord, pNtkGate->pName ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + + // check if it is the end of gate + Ver_ParseSkipComments( pMan ); + Symbol = Ver_StreamPopChar(p); + if ( Symbol == ')' ) + break; + // skip comma + if ( Symbol != ',' ) + { + sprintf( pMan->sError, "Cannot formal parameter %s of gate %s (expected closing paranthesis).", pWord, pNtkGate->pName ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + Ver_ParseSkipComments( pMan ); + } + + // check if it is the end of gate + Ver_ParseSkipComments( pMan ); + if ( Ver_StreamPopChar(p) != ';' ) + { + sprintf( pMan->sError, "Cannot read gate %s (expected closing semicolumn).", pNtkGate->pName ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + + // make sure each input net is driven + Abc_NtkForEachPi( pNtkGate, pObj, i ) + if ( pObj->pCopy == NULL ) + { + sprintf( pMan->sError, "Formal input %s of gate %s has no actual input.", Abc_ObjFanout0(pObj)->pData, pNtkGate->pName ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } +/* + // make sure each output net is driving something + Abc_NtkForEachPo( pNtkGate, pObj, i ) + if ( pObj->pCopy == NULL ) + { + sprintf( pMan->sError, "Formal output %s of gate %s has no actual output.", Abc_ObjFanin0(pObj)->pData, pNtkGate->pName ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } +*/ + // create a new node + pNode = Abc_NtkCreateNode( pMan->pNtkCur ); + // connect to fanin nets + Abc_NtkForEachPi( pNtkGate, pObj, i ) + Abc_ObjAddFanin( pNode, pObj->pCopy ); + // connect to fanout nets + Abc_NtkForEachPo( pNtkGate, pObj, i ) + if ( pObj->pCopy ) + Abc_ObjAddFanin( pObj->pCopy, pNode ); + // set the functionality + pNode->pData = pNtkGate; + return 1; +} + + +/**Function************************************************************* + + Synopsis [Creates PI terminal and net.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Obj_t * Ver_ParseCreatePi( Abc_Ntk_t * pNtk, char * pName ) +{ + Abc_Obj_t * pNet, * pTerm; + // get the PI net + pNet = Abc_NtkFindNet( pNtk, pName ); + if ( pNet ) + printf( "Warning: PI \"%s\" appears twice in the list.\n", pName ); + pNet = Abc_NtkFindOrCreateNet( pNtk, pName ); + // add the PI node + pTerm = Abc_NtkCreatePi( pNtk ); + Abc_ObjAddFanin( pNet, pTerm ); + return pTerm; +} + +/**Function************************************************************* + + Synopsis [Creates PO terminal and net.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Obj_t * Ver_ParseCreatePo( Abc_Ntk_t * pNtk, char * pName ) +{ + Abc_Obj_t * pNet, * pTerm; + // get the PO net + pNet = Abc_NtkFindNet( pNtk, pName ); + if ( pNet && Abc_ObjFaninNum(pNet) == 0 ) + printf( "Warning: PO \"%s\" appears twice in the list.\n", pName ); + pNet = Abc_NtkFindOrCreateNet( pNtk, pName ); + // add the PO node + pTerm = Abc_NtkCreatePo( pNtk ); + Abc_ObjAddFanin( pTerm, pNet ); + return pTerm; +} + +/**Function************************************************************* + + Synopsis [Create a constant 0 node driving the net with this name.] + + Description [Assumes that the net already exists.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Obj_t * Ver_ParseCreateConst( Abc_Ntk_t * pNtk, char * pName, bool fConst1 ) +{ + Abc_Obj_t * pNet, * pTerm; + pTerm = fConst1? Abc_NodeCreateConst1(pNtk) : Abc_NodeCreateConst0(pNtk); + pNet = Abc_NtkFindNet(pNtk, pName); assert( pNet ); + Abc_ObjAddFanin( pNet, pTerm ); + return pTerm; +} + +/**Function************************************************************* + + Synopsis [Create a latch with the given input/output.] + + Description [By default, the latch value is unknown (ABC_INIT_NONE).] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Obj_t * Ver_ParseCreateLatch( Abc_Ntk_t * pNtk, char * pNetLI, char * pNetLO ) +{ + Abc_Obj_t * pLatch, * pNet; + // create a new latch and add it to the network + pLatch = Abc_NtkCreateLatch( pNtk ); + // get the LI net + pNet = Abc_NtkFindOrCreateNet( pNtk, pNetLI ); + Abc_ObjAddFanin( pLatch, pNet ); + // get the LO net + pNet = Abc_NtkFindOrCreateNet( pNtk, pNetLO ); + Abc_ObjAddFanin( pNet, pLatch ); + return pLatch; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/temp/ver/verFormula.c b/src/temp/ver/verFormula.c new file mode 100644 index 00000000..7edb5bd9 --- /dev/null +++ b/src/temp/ver/verFormula.c @@ -0,0 +1,408 @@ +/**CFile**************************************************************** + + FileName [verFormula.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Verilog parser.] + + Synopsis [Formula parser to read Verilog assign statements.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - August 19, 2006.] + + Revision [$Id: verFormula.c,v 1.00 2006/08/19 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "ver.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +// the list of operation symbols to be used in expressions +#define VER_PARSE_SYM_OPEN '(' // opening paranthesis +#define VER_PARSE_SYM_CLOSE ')' // closing paranthesis +#define VER_PARSE_SYM_CONST0 '0' // constant 0 +#define VER_PARSE_SYM_CONST1 '1' // constant 1 +#define VER_PARSE_SYM_NEGBEF1 '!' // negation before the variable +#define VER_PARSE_SYM_NEGBEF2 '~' // negation before the variable +#define VER_PARSE_SYM_AND '&' // logic AND +#define VER_PARSE_SYM_OR '|' // logic OR +#define VER_PARSE_SYM_XOR '^' // logic XOR +#define VER_PARSE_SYM_MUX1 '?' // first symbol of MUX +#define VER_PARSE_SYM_MUX2 ':' // second symbol of MUX + +// the list of opcodes (also specifying operation precedence) +#define VER_PARSE_OPER_NEG 10 // negation +#define VER_PARSE_OPER_AND 9 // logic AND +#define VER_PARSE_OPER_XOR 8 // logic EXOR (a'b | ab') +#define VER_PARSE_OPER_OR 7 // logic OR +#define VER_PARSE_OPER_EQU 6 // equvalence (a'b'| ab ) +#define VER_PARSE_OPER_MUX 5 // MUX (a'b | ac ) +#define VER_PARSE_OPER_MARK 1 // OpStack token standing for an opening paranthesis + +// these are values of the internal Flag +#define VER_PARSE_FLAG_START 1 // after the opening parenthesis +#define VER_PARSE_FLAG_VAR 2 // after operation is received +#define VER_PARSE_FLAG_OPER 3 // after operation symbol is received +#define VER_PARSE_FLAG_OPERMUX 4 // after operation symbol is received +#define VER_PARSE_FLAG_ERROR 5 // when error is detected + +static DdNode * Ver_FormulaParserTopOper( DdManager * dd, Vec_Ptr_t * vStackFn, int Oper ); +static int Ver_FormulaParserFindVar( char * pString, Vec_Ptr_t * vNames ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Parser of the formula encountered in assign statements.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Ver_FormulaParser( char * pFormula, DdManager * dd, Vec_Ptr_t * vNames, Vec_Ptr_t * vStackFn, Vec_Int_t * vStackOp, char * pErrorMessage ) +{ + DdNode * bFunc, * bTemp; + char * pTemp; + int nParans, Flag; + int Oper, Oper1, Oper2; + int v; + + // clear the stacks and the names + Vec_PtrClear( vNames ); + Vec_PtrClear( vStackFn ); + Vec_IntClear( vStackOp ); + + // make sure that the number of opening and closing parantheses is the same + nParans = 0; + for ( pTemp = pFormula; *pTemp; pTemp++ ) + if ( *pTemp == '(' ) + nParans++; + else if ( *pTemp == ')' ) + nParans--; + if ( nParans != 0 ) + { + sprintf( pErrorMessage, "Parse_FormulaParser(): Different number of opening and closing parantheses ()." ); + return NULL; + } + + // add parantheses + pTemp = pFormula + strlen(pFormula) + 2; + *pTemp-- = 0; *pTemp = ')'; + while ( --pTemp != pFormula ) + *pTemp = *(pTemp - 1); + *pTemp = '('; + + // perform parsing + Flag = VER_PARSE_FLAG_START; + for ( pTemp = pFormula; *pTemp; pTemp++ ) + { + switch ( *pTemp ) + { + // skip all spaces, tabs, and end-of-lines + case ' ': + case '\t': + case '\r': + case '\n': + case '\\': // skip name opening statement + continue; + + // treat Constant 0 as a variable + case VER_PARSE_SYM_CONST0: + Vec_PtrPush( vStackFn, b0 ); Cudd_Ref( b0 ); + if ( Flag == VER_PARSE_FLAG_VAR ) + { + sprintf( pErrorMessage, "Parse_FormulaParser(): No operation symbol before constant 0." ); + Flag = VER_PARSE_FLAG_ERROR; + break; + } + Flag = VER_PARSE_FLAG_VAR; + break; + + // the same for Constant 1 + case VER_PARSE_SYM_CONST1: + Vec_PtrPush( vStackFn, b1 ); Cudd_Ref( b1 ); + if ( Flag == VER_PARSE_FLAG_VAR ) + { + sprintf( pErrorMessage, "Parse_FormulaParser(): No operation symbol before constant 1." ); + Flag = VER_PARSE_FLAG_ERROR; + break; + } + Flag = VER_PARSE_FLAG_VAR; + break; + + case VER_PARSE_SYM_NEGBEF1: + case VER_PARSE_SYM_NEGBEF2: + if ( Flag == VER_PARSE_FLAG_VAR ) + {// if NEGBEF follows a variable, AND is assumed + sprintf( pErrorMessage, "Parse_FormulaParser(): Variable before negation." ); + Flag = VER_PARSE_FLAG_ERROR; + break; + } + Vec_IntPush( vStackOp, VER_PARSE_OPER_NEG ); + break; + + case VER_PARSE_SYM_AND: + case VER_PARSE_SYM_OR: + case VER_PARSE_SYM_XOR: + case VER_PARSE_SYM_MUX1: + case VER_PARSE_SYM_MUX2: + if ( Flag != VER_PARSE_FLAG_VAR ) + { + sprintf( pErrorMessage, "Parse_FormulaParser(): There is no variable before AND, EXOR, or OR." ); + Flag = VER_PARSE_FLAG_ERROR; + break; + } + if ( *pTemp == VER_PARSE_SYM_AND ) + Vec_IntPush( vStackOp, VER_PARSE_OPER_AND ); + else if ( *pTemp == VER_PARSE_SYM_OR ) + Vec_IntPush( vStackOp, VER_PARSE_OPER_OR ); + else if ( *pTemp == VER_PARSE_SYM_XOR ) + Vec_IntPush( vStackOp, VER_PARSE_OPER_XOR ); + else if ( *pTemp == VER_PARSE_SYM_MUX1 ) + Vec_IntPush( vStackOp, VER_PARSE_OPER_MUX ); +// else if ( *pTemp == VER_PARSE_SYM_MUX2 ) +// Vec_IntPush( vStackOp, VER_PARSE_OPER_MUX ); + Flag = VER_PARSE_FLAG_OPER; + break; + + case VER_PARSE_SYM_OPEN: + if ( Flag == VER_PARSE_FLAG_VAR ) + { + sprintf( pErrorMessage, "Parse_FormulaParser(): Variable before a paranthesis." ); + Flag = VER_PARSE_FLAG_ERROR; + break; + } + Vec_IntPush( vStackOp, VER_PARSE_OPER_MARK ); + // after an opening bracket, it feels like starting over again + Flag = VER_PARSE_FLAG_START; + break; + + case VER_PARSE_SYM_CLOSE: + if ( Vec_IntSize( vStackOp ) ) + { + while ( 1 ) + { + if ( !Vec_IntSize( vStackOp ) ) + { + sprintf( pErrorMessage, "Parse_FormulaParser(): There is no opening paranthesis\n" ); + Flag = VER_PARSE_FLAG_ERROR; + break; + } + Oper = Vec_IntPop( vStackOp ); + if ( Oper == VER_PARSE_OPER_MARK ) + break; + // skip the second MUX operation +// if ( Oper == VER_PARSE_OPER_MUX2 ) +// { +// Oper = Vec_IntPop( vStackOp ); +// assert( Oper == VER_PARSE_OPER_MUX1 ); +// } + + // perform the given operation + if ( Ver_FormulaParserTopOper( dd, vStackFn, Oper ) == NULL ) + { + sprintf( pErrorMessage, "Parse_FormulaParser(): Unknown operation\n" ); + return NULL; + } + } + } + else + { + sprintf( pErrorMessage, "Parse_FormulaParser(): There is no opening paranthesis\n" ); + Flag = VER_PARSE_FLAG_ERROR; + break; + } + if ( Flag != VER_PARSE_FLAG_ERROR ) + Flag = VER_PARSE_FLAG_VAR; + break; + + + default: + // scan the next name + v = Ver_FormulaParserFindVar( pTemp, vNames ); + pTemp += (int)Vec_PtrEntry( vNames, 2*v ) - 1; + + // assume operation AND, if vars follow one another + if ( Flag == VER_PARSE_FLAG_VAR ) + { + sprintf( pErrorMessage, "Parse_FormulaParser(): Incorrect state." ); + return NULL; + } + bTemp = Cudd_bddIthVar(dd, v); + Vec_PtrPush( vStackFn, bTemp ); Cudd_Ref( bTemp ); + Flag = VER_PARSE_FLAG_VAR; + break; + } + + if ( Flag == VER_PARSE_FLAG_ERROR ) + break; // error exit + else if ( Flag == VER_PARSE_FLAG_START ) + continue; // go on parsing + else if ( Flag == VER_PARSE_FLAG_VAR ) + while ( 1 ) + { // check if there are negations in the OpStack + if ( !Vec_IntSize(vStackOp) ) + break; + Oper = Vec_IntPop( vStackOp ); + if ( Oper != VER_PARSE_OPER_NEG ) + { + Vec_IntPush( vStackOp, Oper ); + break; + } + else + { + Vec_PtrPush( vStackFn, Cudd_Not(Vec_PtrPop(vStackFn)) ); + } + } + else // if ( Flag == VER_PARSE_FLAG_OPER ) + while ( 1 ) + { // execute all the operations in the OpStack + // with precedence higher or equal than the last one + Oper1 = Vec_IntPop( vStackOp ); // the last operation + if ( !Vec_IntSize(vStackOp) ) + { // if it is the only operation, push it back + Vec_IntPush( vStackOp, Oper1 ); + break; + } + Oper2 = Vec_IntPop( vStackOp ); // the operation before the last one + if ( Oper2 >= Oper1 ) + { // if Oper2 precedence is higher or equal, execute it + if ( Ver_FormulaParserTopOper( dd, vStackFn, Oper2 ) == NULL ) + { + sprintf( pErrorMessage, "Parse_FormulaParser(): Unknown operation\n" ); + return NULL; + } + Vec_IntPush( vStackOp, Oper1 ); // push the last operation back + } + else + { // if Oper2 precedence is lower, push them back and done + Vec_IntPush( vStackOp, Oper2 ); + Vec_IntPush( vStackOp, Oper1 ); + break; + } + } + } + + if ( Flag != VER_PARSE_FLAG_ERROR ) + { + if ( Vec_PtrSize(vStackFn) ) + { + bFunc = Vec_PtrPop(vStackFn); + if ( !Vec_PtrSize(vStackFn) ) + if ( !Vec_IntSize(vStackOp) ) + { + Cudd_Deref( bFunc ); + return bFunc; + } + else + sprintf( pErrorMessage, "Parse_FormulaParser(): Something is left in the operation stack\n" ); + else + sprintf( pErrorMessage, "Parse_FormulaParser(): Something is left in the function stack\n" ); + } + else + sprintf( pErrorMessage, "Parse_FormulaParser(): The input string is empty\n" ); + } + Cudd_Ref( bFunc ); + Cudd_RecursiveDeref( dd, bFunc ); + return NULL; +} + +/**Function************************************************************* + + Synopsis [Performs the operation on the top entries in the stack.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Ver_FormulaParserTopOper( DdManager * dd, Vec_Ptr_t * vStackFn, int Oper ) +{ + DdNode * bArg0, * bArg1, * bArg2, * bFunc; + // perform the given operation + bArg2 = Vec_PtrPop( vStackFn ); + bArg1 = Vec_PtrPop( vStackFn ); + if ( Oper == VER_PARSE_OPER_AND ) + bFunc = Cudd_bddAnd( dd, bArg1, bArg2 ); + else if ( Oper == VER_PARSE_OPER_XOR ) + bFunc = Cudd_bddXor( dd, bArg1, bArg2 ); + else if ( Oper == VER_PARSE_OPER_OR ) + bFunc = Cudd_bddOr( dd, bArg1, bArg2 ); + else if ( Oper == VER_PARSE_OPER_EQU ) + bFunc = Cudd_bddXnor( dd, bArg1, bArg2 ); + else if ( Oper == VER_PARSE_OPER_MUX ) + { + bArg0 = Vec_PtrPop( vStackFn ); + bFunc = Cudd_bddIte( dd, bArg0, bArg1, bArg2 ); Cudd_Ref( bFunc ); + Cudd_RecursiveDeref( dd, bArg0 ); + Cudd_Deref( bFunc ); + } + else + return NULL; + Cudd_Ref( bFunc ); + Cudd_RecursiveDeref( dd, bArg1 ); + Cudd_RecursiveDeref( dd, bArg2 ); + Vec_PtrPush( vStackFn, bFunc ); + return bFunc; +} + +/**Function************************************************************* + + Synopsis [Returns the index of the new variable found.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ver_FormulaParserFindVar( char * pString, Vec_Ptr_t * vNames ) +{ + char * pTemp, * pTemp2; + int nLength, nLength2, i; + // find the end of the string delimited by other characters + pTemp = pString; + while ( *pTemp && *pTemp != ' ' && *pTemp != '\t' && *pTemp != '\r' && *pTemp != '\n' && + *pTemp != VER_PARSE_SYM_OPEN && *pTemp != VER_PARSE_SYM_CLOSE && + *pTemp != VER_PARSE_SYM_NEGBEF1 && *pTemp != VER_PARSE_SYM_NEGBEF2 && + *pTemp != VER_PARSE_SYM_AND && *pTemp != VER_PARSE_SYM_OR && *pTemp != VER_PARSE_SYM_XOR && + *pTemp != VER_PARSE_SYM_MUX1 && *pTemp != VER_PARSE_SYM_MUX2 ) + pTemp++; + // look for this string in the array + nLength = pTemp - pString; + for ( i = 0; i < Vec_PtrSize(vNames)/2; i++ ) + { + nLength2 = (int)Vec_PtrEntry( vNames, 2*i + 0 ); + if ( nLength2 != nLength ) + continue; + pTemp2 = Vec_PtrEntry( vNames, 2*i + 1 ); + if ( strncmp( pTemp, pTemp2, nLength ) ) + continue; + return i; + } + // could not find - add and return the number + Vec_PtrPush( vNames, (void *)nLength ); + Vec_PtrPush( vNames, pString ); + return i; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/temp/ver/verParse.c b/src/temp/ver/verParse.c new file mode 100644 index 00000000..c8497932 --- /dev/null +++ b/src/temp/ver/verParse.c @@ -0,0 +1,111 @@ +/**CFile**************************************************************** + + FileName [verParse.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Verilog parser.] + + Synopsis [Performs some Verilog parsing tasks.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - August 19, 2006.] + + Revision [$Id: verParse.c,v 1.00 2006/08/19 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "ver.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Skips the comments of they are present.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ver_ParseSkipComments( Ver_Man_t * pMan ) +{ + Ver_Stream_t * p = pMan->pReader; + char Symbol; + // skip spaces + Ver_StreamSkipChars( p, " \t\n\r" ); + if ( !Ver_StreamIsOkey(pMan->pReader) ) + return 1; + // read the first symbol + Symbol = Ver_StreamScanChar( p ); + if ( Symbol != '/' ) + return 1; + Ver_StreamPopChar( p ); + // read the second symbol + Symbol = Ver_StreamScanChar( p ); + if ( Symbol == '/' ) + { // skip till the end of line + Ver_StreamSkipToChars( p, "\n" ); + return Ver_ParseSkipComments( pMan ); + } + if ( Symbol == '*' ) + { // skip till the next occurance of */ + Ver_StreamPopChar( p ); + do { + Ver_StreamSkipToChars( p, "*" ); + Ver_StreamPopChar( p ); + } while ( Ver_StreamScanChar( p ) != '/' ); + Ver_StreamPopChar( p ); + return Ver_ParseSkipComments( pMan ); + } + sprintf( pMan->sError, "Cannot parse after symbol \"/\"." ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; +} + +/**Function************************************************************* + + Synopsis [Parses a Verilog name that can be being with a slash.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +char * Ver_ParseGetName( Ver_Man_t * pMan ) +{ + Ver_Stream_t * p = pMan->pReader; + char Symbol; + char * pWord; + if ( !Ver_StreamIsOkey(p) ) + return NULL; + if ( !Ver_ParseSkipComments( pMan ) ) + return NULL; + Symbol = Ver_StreamScanChar( p ); + if ( Symbol == '\\' ) + Ver_StreamPopChar( p ); + pWord = Ver_StreamGetWord( p, " \t\n\r(),;" ); + if ( !Ver_ParseSkipComments( pMan ) ) + return NULL; + return pWord; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/temp/ver/verStream.c b/src/temp/ver/verStream.c new file mode 100644 index 00000000..7956b13c --- /dev/null +++ b/src/temp/ver/verStream.c @@ -0,0 +1,435 @@ +/**CFile**************************************************************** + + FileName [verStream.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Verilog parser.] + + Synopsis [Input file stream, which knows nothing about Verilog.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - August 19, 2006.] + + Revision [$Id: verStream.c,v 1.00 2006/08/19 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "ver.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +#define VER_BUFFER_SIZE 1048576 // 1M - size of the data chunk stored in memory +#define VER_OFFSET_SIZE 4096 // 4K - load new data when less than this is left +#define VER_WORD_SIZE 4096 // 4K - the largest token that can be returned + +#define VER_MINIMUM(a,b) (((a) < (b))? (a) : (b)) + +struct Ver_Stream_t_ +{ + // the input file + char * pFileName; // the input file name + FILE * pFile; // the input file pointer + int nFileSize; // the total number of bytes in the file + int nFileRead; // the number of bytes currently read from file + int nLineCounter; // the counter of lines processed + // temporary storage for data + char * pBuffer; // the buffer + int nBufferSize; // the size of the buffer + char * pBufferCur; // the current reading position + char * pBufferEnd; // the first position not used by currently loaded data + char * pBufferStop; // the position where loading new data will be done + // tokens given to the user + char pChars[VER_WORD_SIZE+5]; // temporary storage for a word (plus end-of-string and two parantheses) + int nChars; // the total number of characters in the word + // status of the parser + int fStop; // this flag goes high when the end of file is reached +}; + +static void Ver_StreamReload( Ver_Stream_t * p ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Starts the file reader for the given file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ver_Stream_t * Ver_StreamAlloc( char * pFileName ) +{ + Ver_Stream_t * p; + FILE * pFile; + int nCharsToRead; + // check if the file can be opened + pFile = fopen( pFileName, "rb" ); + if ( pFile == NULL ) + { + printf( "Ver_StreamAlloc(): Cannot open input file \"%s\".\n", pFileName ); + return NULL; + } + // start the file reader + p = ALLOC( Ver_Stream_t, 1 ); + memset( p, 0, sizeof(Ver_Stream_t) ); + p->pFileName = pFileName; + p->pFile = pFile; + // get the file size, in bytes + fseek( pFile, 0, SEEK_END ); + p->nFileSize = ftell( pFile ); + rewind( pFile ); + // allocate the buffer + p->pBuffer = ALLOC( char, VER_BUFFER_SIZE+1 ); + p->nBufferSize = VER_BUFFER_SIZE; + p->pBufferCur = p->pBuffer; + // determine how many chars to read + nCharsToRead = VER_MINIMUM(p->nFileSize, VER_BUFFER_SIZE); + // load the first part into the buffer + fread( p->pBuffer, nCharsToRead, 1, p->pFile ); + p->nFileRead = nCharsToRead; + // set the ponters to the end and the stopping point + p->pBufferEnd = p->pBuffer + nCharsToRead; + p->pBufferStop = (p->nFileRead == p->nFileSize)? p->pBufferEnd : p->pBuffer + VER_BUFFER_SIZE - VER_OFFSET_SIZE; + // start the arrays + p->nLineCounter = 1; // 1-based line counting + return p; +} + +/**Function************************************************************* + + Synopsis [Loads new data into the file reader.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ver_StreamReload( Ver_Stream_t * p ) +{ + int nCharsUsed, nCharsToRead; + assert( !p->fStop ); + assert( p->pBufferCur > p->pBufferStop ); + assert( p->pBufferCur < p->pBufferEnd ); + // figure out how many chars are still not processed + nCharsUsed = p->pBufferEnd - p->pBufferCur; + // move the remaining data to the beginning of the buffer + memmove( p->pBuffer, p->pBufferCur, nCharsUsed ); + p->pBufferCur = p->pBuffer; + // determine how many chars we will read + nCharsToRead = VER_MINIMUM( p->nBufferSize - nCharsUsed, p->nFileSize - p->nFileRead ); + // read the chars + fread( p->pBuffer + nCharsUsed, nCharsToRead, 1, p->pFile ); + p->nFileRead += nCharsToRead; + // set the ponters to the end and the stopping point + p->pBufferEnd = p->pBuffer + nCharsUsed + nCharsToRead; + p->pBufferStop = (p->nFileRead == p->nFileSize)? p->pBufferEnd : p->pBuffer + VER_BUFFER_SIZE - VER_OFFSET_SIZE; +} + +/**Function************************************************************* + + Synopsis [Stops the file reader.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ver_StreamFree( Ver_Stream_t * p ) +{ + if ( p->pFile ) + fclose( p->pFile ); + FREE( p->pBuffer ); + free( p ); +} + +/**Function************************************************************* + + Synopsis [Returns the file size.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +char * Ver_StreamGetFileName( Ver_Stream_t * p ) +{ + return p->pFileName; +} + +/**Function************************************************************* + + Synopsis [Returns the file size.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ver_StreamGetFileSize( Ver_Stream_t * p ) +{ + return p->nFileSize; +} + +/**Function************************************************************* + + Synopsis [Returns the current reading position.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ver_StreamGetCurPosition( Ver_Stream_t * p ) +{ + return p->nFileRead - (p->pBufferEnd - p->pBufferCur); +} + +/**Function************************************************************* + + Synopsis [Returns the line number for the given token.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ver_StreamGetLineNumber( Ver_Stream_t * p ) +{ + return p->nLineCounter; +} + + + +/**Function************************************************************* + + Synopsis [Returns current symbol.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ver_StreamIsOkey( Ver_Stream_t * p ) +{ + return !p->fStop; +} + +/**Function************************************************************* + + Synopsis [Returns current symbol.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +char Ver_StreamScanChar( Ver_Stream_t * p ) +{ + assert( !p->fStop ); + return *p->pBufferCur; +} + +/**Function************************************************************* + + Synopsis [Returns current symbol and moves to the next.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +char Ver_StreamPopChar( Ver_Stream_t * p ) +{ + assert( !p->fStop ); + // check if the new data should to be loaded + if ( p->pBufferCur > p->pBufferStop ) + Ver_StreamReload( p ); + // check if there are symbols left + if ( p->pBufferCur == p->pBufferEnd ) // end of file + { + p->fStop = 1; + return -1; + } + return *p->pBufferCur++; +} + +/**Function************************************************************* + + Synopsis [Skips the current symbol and all symbols from the list.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ver_StreamSkipChars( Ver_Stream_t * p, char * pCharsToSkip ) +{ + char * pChar, * pTemp; + assert( !p->fStop ); + assert( pCharsToSkip != NULL ); + // check if the new data should to be loaded + if ( p->pBufferCur > p->pBufferStop ) + Ver_StreamReload( p ); + // skip the symbols + for ( pChar = p->pBufferCur; pChar < p->pBufferEnd; pChar++ ) + { + // count the lines + if ( *pChar == '\n' ) + p->nLineCounter++; + // skip symbols as long as they are in the list + for ( pTemp = pCharsToSkip; *pTemp; pTemp++ ) + if ( *pChar == *pTemp ) + break; + if ( *pTemp == 0 ) // pChar is not found in the list + { + p->pBufferCur = pChar; + return; + } + } + // the file is finished or the last part continued + // through VER_OFFSET_SIZE chars till the end of the buffer + if ( p->pBufferStop == p->pBufferEnd ) // end of file + { + p->fStop = 1; + return; + } + printf( "Ver_StreamSkipSymbol() failed to parse the file \"%s\".\n", p->pFileName ); +} + +/**Function************************************************************* + + Synopsis [Skips all symbols until encountering one from the list.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ver_StreamSkipToChars( Ver_Stream_t * p, char * pCharsToStop ) +{ + char * pChar, * pTemp; + assert( !p->fStop ); + assert( pCharsToStop != NULL ); + // check if the new data should to be loaded + if ( p->pBufferCur > p->pBufferStop ) + Ver_StreamReload( p ); + // skip the symbols + for ( pChar = p->pBufferCur; pChar < p->pBufferEnd; pChar++ ) + { + // count the lines + if ( *pChar == '\n' ) + p->nLineCounter++; + // skip symbols as long as they are NOT in the list + for ( pTemp = pCharsToStop; *pTemp; pTemp++ ) + if ( *pChar == *pTemp ) + break; + if ( *pTemp == 0 ) // pChar is not found in the list + continue; + // the symbol is found - move position and return + p->pBufferCur = pChar; + return; + } + // the file is finished or the last part continued + // through VER_OFFSET_SIZE chars till the end of the buffer + if ( p->pBufferStop == p->pBufferEnd ) // end of file + { + p->fStop = 1; + return; + } + printf( "Ver_StreamSkipToSymbol() failed to parse the file \"%s\".\n", p->pFileName ); +} + +/**Function************************************************************* + + Synopsis [Returns current word delimited by the set of symbols.] + + Description [Modifies the stream by inserting 0 at the first encounter + of one of the symbols in the list.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +char * Ver_StreamGetWord( Ver_Stream_t * p, char * pCharsToStop ) +{ + char * pChar, * pTemp; + if ( p->fStop ) + return NULL; + assert( pCharsToStop != NULL ); + // check if the new data should to be loaded + if ( p->pBufferCur > p->pBufferStop ) + Ver_StreamReload( p ); + // skip the symbols + p->nChars = 0; + for ( pChar = p->pBufferCur; pChar < p->pBufferEnd; pChar++ ) + { + // count the lines + if ( *pChar == '\n' ) + p->nLineCounter++; + // skip symbols as long as they are NOT in the list + for ( pTemp = pCharsToStop; *pTemp; pTemp++ ) + if ( *pChar == *pTemp ) + break; + if ( *pTemp == 0 ) // pChar is not found in the list + { + p->pChars[p->nChars++] = *pChar; + if ( p->nChars == VER_WORD_SIZE ) + return NULL; + continue; + } + // the symbol is found - move the position, set the word end, return the word + p->pBufferCur = pChar; + p->pChars[p->nChars] = 0; + return p->pChars; + } + // the file is finished or the last part continued + // through VER_OFFSET_SIZE chars till the end of the buffer + if ( p->pBufferStop == p->pBufferEnd ) // end of file + { + p->fStop = 1; + p->pChars[p->nChars] = 0; + return p->pChars; + } + printf( "Ver_StreamGetWord() failed to parse the file \"%s\".\n", p->pFileName ); + return NULL; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/temp/ver/verWords.c b/src/temp/ver/verWords.c new file mode 100644 index 00000000..f9d27010 --- /dev/null +++ b/src/temp/ver/verWords.c @@ -0,0 +1,48 @@ +/**CFile**************************************************************** + + FileName [verWords.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Verilog parser.] + + Synopsis [Handles keywords that are currently supported.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - August 19, 2006.] + + Revision [$Id: verWords.c,v 1.00 2006/08/19 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "ver.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/temp/ver/ver_.c b/src/temp/ver/ver_.c new file mode 100644 index 00000000..76599dac --- /dev/null +++ b/src/temp/ver/ver_.c @@ -0,0 +1,48 @@ +/**CFile**************************************************************** + + FileName [ver_.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: ver_.c,v 1.00 2006/08/19 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "ver.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + |