From fb51057e4a36d2e5737bba8739b88140b55db7c7 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 19 Feb 2007 08:01:00 -0800 Subject: Version abc70219 --- src/base/ver/ver.h | 14 +- src/base/ver/verCore.c | 1461 +++++++++++++++++++++++++++++++-------------- src/base/ver/verFormula.c | 2 +- src/base/ver/verParse.c | 2 +- 4 files changed, 1010 insertions(+), 469 deletions(-) (limited to 'src/base/ver') diff --git a/src/base/ver/ver.h b/src/base/ver/ver.h index 575ae7bb..0ba081db 100644 --- a/src/base/ver/ver.h +++ b/src/base/ver/ver.h @@ -45,18 +45,18 @@ typedef struct Ver_Stream_t_ Ver_Stream_t; struct Ver_Man_t_ { + // internal parameters + int fMapped; // mapped verilog + int fUseMemMan; // allocate memory manager in the networks + int fCheck; // checks network for currectness // input file stream char * pFileName; Ver_Stream_t * pReader; int fNameLast; ProgressBar * pProgress; - // current network and library - Abc_Ntk_t * pNtkCur; // the network under construction - Abc_Lib_t * pDesign; // the current design - // parameters - int fUseMemMan; // allocate memory manager in the networks - int fCheck; // checks network for currectness - // error recovery + // current design + Abc_Lib_t * pDesign; + // error handling FILE * Output; int fTopLevel; int fError; diff --git a/src/base/ver/verCore.c b/src/base/ver/verCore.c index a8ac99e5..6c036288 100644 --- a/src/base/ver/verCore.c +++ b/src/base/ver/verCore.c @@ -19,6 +19,8 @@ ***********************************************************************/ #include "ver.h" +#include "mio.h" +#include "main.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -51,50 +53,29 @@ static void Ver_ParseStop( Ver_Man_t * p ); static void Ver_ParseFreeData( Ver_Man_t * p ); static void Ver_ParseInternal( Ver_Man_t * p ); static int Ver_ParseModule( Ver_Man_t * p ); -static int Ver_ParseSignal( Ver_Man_t * p, 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 int Ver_ParseGateStandard( Ver_Man_t * pMan, Ver_GateType_t GateType ); +static int Ver_ParseSignal( Ver_Man_t * p, Abc_Ntk_t * pNtk, Ver_SignalType_t SigType ); +static int Ver_ParseAlways( Ver_Man_t * p, Abc_Ntk_t * pNtk ); +static int Ver_ParseInitial( Ver_Man_t * p, Abc_Ntk_t * pNtk ); +static int Ver_ParseAssign( Ver_Man_t * p, Abc_Ntk_t * pNtk ); +static int Ver_ParseGateStandard( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Ver_GateType_t GateType ); +static int Ver_ParseGate( Ver_Man_t * p, Abc_Ntk_t * pNtk, Mio_Gate_t * pGate ); +static int Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox ); +static int Ver_ParseConnectBox( Ver_Man_t * pMan, Abc_Obj_t * pBox ); +static int Vec_ParseAttachBoxes( Ver_Man_t * pMan ); static Abc_Obj_t * Ver_ParseCreatePi( Abc_Ntk_t * pNtk, char * pName ); static Abc_Obj_t * Ver_ParseCreatePo( Abc_Ntk_t * pNtk, char * pName ); static Abc_Obj_t * Ver_ParseCreateLatch( Abc_Ntk_t * pNtk, Abc_Obj_t * pNetLI, Abc_Obj_t * pNetLO ); static Abc_Obj_t * Ver_ParseCreateInv( Abc_Ntk_t * pNtk, Abc_Obj_t * pNet ); +static inline int Ver_NtkIsDefined( Abc_Ntk_t * pNtkBox ) { assert( pNtkBox->pName ); return Abc_NtkPiNum(pNtkBox) || Abc_NtkPoNum(pNtkBox); } +static inline int Ver_ObjIsConnected( Abc_Obj_t * pObj ) { assert( Abc_ObjIsBox(pObj) ); return Abc_ObjFaninNum(pObj) || Abc_ObjFanoutNum(pObj); } + +int glo_fMapped = 0; // this is bad! + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [File parser.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Lib_t * Ver_ParseFile( char * pFileName, Abc_Lib_t * pGateLib, int fCheck, int fUseMemMan ) -{ - Ver_Man_t * p; - Abc_Lib_t * pDesign; - // start the parser - p = Ver_ParseStart( pFileName, pGateLib ); - p->fCheck = fCheck; - p->fUseMemMan = fUseMemMan; - // parse the file - Ver_ParseInternal( p ); - // save the result - pDesign = p->pDesign; - p->pDesign = NULL; - // stop the parser - Ver_ParseStop( p ); - return pDesign; -} /**Function************************************************************* @@ -114,6 +95,8 @@ Ver_Man_t * Ver_ParseStart( char * pFileName, Abc_Lib_t * pGateLib ) memset( p, 0, sizeof(Ver_Man_t) ); p->pFileName = pFileName; p->pReader = Ver_StreamAlloc( pFileName ); + if ( p->pReader == NULL ) + return NULL; p->Output = stdout; p->pProgress = Extra_ProgressBarStart( stdout, Ver_StreamGetFileSize(p->pReader) ); p->vNames = Vec_PtrAlloc( 100 ); @@ -122,6 +105,7 @@ Ver_Man_t * Ver_ParseStart( char * pFileName, Abc_Lib_t * pGateLib ) // create the design library and assign the technology library p->pDesign = Abc_LibCreate( pFileName ); p->pDesign->pLibrary = pGateLib; + p->pDesign->pGenlib = Abc_FrameReadLibGen(); return p; } @@ -138,7 +122,6 @@ Ver_Man_t * Ver_ParseStart( char * pFileName, Abc_Lib_t * pGateLib ) ***********************************************************************/ void Ver_ParseStop( Ver_Man_t * p ) { - assert( p->pNtkCur == NULL ); Ver_StreamFree( p->pReader ); Extra_ProgressBarStop( p->pProgress ); Vec_PtrFree( p->vNames ); @@ -146,6 +129,41 @@ void Ver_ParseStop( Ver_Man_t * p ) Vec_IntFree( p->vStackOp ); free( p ); } + +/**Function************************************************************* + + Synopsis [File parser.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Lib_t * Ver_ParseFile( char * pFileName, Abc_Lib_t * pGateLib, int fCheck, int fUseMemMan ) +{ + Ver_Man_t * p; + Abc_Lib_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(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; +} /**Function************************************************************* @@ -160,7 +178,11 @@ void Ver_ParseStop( Ver_Man_t * p ) ***********************************************************************/ void Ver_ParseInternal( Ver_Man_t * pMan ) { + Abc_Ntk_t * pNtk; char * pToken; + int i; + + // preparse the modeles while ( 1 ) { // get the next token @@ -173,30 +195,28 @@ void Ver_ParseInternal( Ver_Man_t * pMan ) Ver_ParsePrintErrorMessage( pMan ); return; } - // parse the module - if ( !Ver_ParseModule( pMan ) ) + if ( !Ver_ParseModule(pMan) ) return; + } + + // process defined and undefined boxes + if ( !Vec_ParseAttachBoxes( pMan ) ) + return; + // connect the boxes and check + Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i ) + { + // fix the dangling nets + Abc_NtkFinalizeRead( pNtk ); // check the network for correctness - if ( pMan->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->pDesign->tModules, pMan->pNtkCur->pName ) ) + if ( pMan->fCheck && !Abc_NtkCheckRead( pNtk ) ) { pMan->fTopLevel = 1; - sprintf( pMan->sError, "Module \"%s\" is defined more than once.", pMan->pNtkCur->pName ); + sprintf( pMan->sError, "The network check has failed.", pNtk->pName ); Ver_ParsePrintErrorMessage( pMan ); return; } - Vec_PtrPush( pMan->pDesign->vModules, pMan->pNtkCur ); - st_insert( pMan->pDesign->tModules, pMan->pNtkCur->pName, (char *)pMan->pNtkCur ); - pMan->pNtkCur = NULL; } } @@ -213,12 +233,6 @@ void Ver_ParseInternal( Ver_Man_t * pMan ) ***********************************************************************/ void Ver_ParseFreeData( Ver_Man_t * p ) { - if ( p->pNtkCur ) - { - p->pNtkCur->pManFunc = NULL; - Abc_NtkDelete( p->pNtkCur ); - p->pNtkCur = NULL; - } if ( p->pDesign ) { Abc_LibFree( p->pDesign, NULL ); @@ -249,7 +263,105 @@ void Ver_ParsePrintErrorMessage( Ver_Man_t * p ) Ver_ParseFreeData( p ); } +/**Function************************************************************* + + Synopsis [Finds the network by name or create a new blackbox network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Ver_ParseFindOrCreateNetwork( Ver_Man_t * pMan, char * pName ) +{ + Abc_Ntk_t * pNtkNew; + // check if the network exists + if ( pNtkNew = Abc_LibFindModelByName( 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_LibAddModel( pMan->pDesign, pNtkNew ); + return pNtkNew; +} + +/**Function************************************************************* + + Synopsis [Finds the network by name or create a new blackbox network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Obj_t * Ver_ParseFindNet( Abc_Ntk_t * pNtk, char * pName ) +{ + Abc_Obj_t * pObj; + if ( pObj = Abc_NtkFindNet(pNtk, pName) ) + return pObj; + if ( !strcmp( pName, "1\'b0" ) ) + return Abc_NtkFindOrCreateNet( pNtk, "1\'b0" ); + if ( !strcmp( pName, "1\'b1" ) ) + return Abc_NtkFindOrCreateNet( pNtk, "1\'b1" ); + return NULL; +} + +/**Function************************************************************* + + Synopsis [Converts the network from the blackbox type into a different one.] + + Description [] + + SideEffects [] + + SeeAlso [] +***********************************************************************/ +int Ver_ParseConvertNetwork( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, int fMapped ) +{ + 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; +} /**Function************************************************************* @@ -264,26 +376,17 @@ void Ver_ParsePrintErrorMessage( Ver_Man_t * p ) ***********************************************************************/ int Ver_ParseModule( Ver_Man_t * pMan ) { + Mio_Gate_t * pGate; Ver_Stream_t * p = pMan->pReader; Abc_Ntk_t * pNtk, * pNtkTemp; - Abc_Obj_t * pNet; char * pWord, Symbol; int RetValue; - // start the current network - assert( pMan->pNtkCur == NULL ); - pNtk = pMan->pNtkCur = Abc_NtkAlloc( ABC_NTK_NETLIST, ABC_FUNC_BLACKBOX, pMan->fUseMemMan ); - pNtk->ntkFunc = ABC_FUNC_AIG; - pNtk->pManFunc = pMan->pDesign->pManFunc; - // get the network name pWord = Ver_ParseGetName( pMan ); - pNtk->pName = Extra_UtilStrsav( pWord ); - pNtk->pSpec = NULL; - // create constant nets - Abc_NtkFindOrCreateNet( pNtk, "1\'b0" ); - Abc_NtkFindOrCreateNet( pNtk, "1\'b1" ); + // get the network with this name + pNtk = Ver_ParseFindOrCreateNetwork( pMan, pWord ); // make sure we stopped at the opening paranthesis if ( Ver_StreamPopChar(p) != '(' ) @@ -313,15 +416,15 @@ int Ver_ParseModule( Ver_Man_t * pMan ) if ( pWord == NULL ) return 0; if ( !strcmp( pWord, "input" ) ) - RetValue = Ver_ParseSignal( pMan, VER_SIG_INPUT ); + RetValue = Ver_ParseSignal( pMan, pNtk, VER_SIG_INPUT ); else if ( !strcmp( pWord, "output" ) ) - RetValue = Ver_ParseSignal( pMan, VER_SIG_OUTPUT ); + RetValue = Ver_ParseSignal( pMan, pNtk, VER_SIG_OUTPUT ); else if ( !strcmp( pWord, "reg" ) ) - RetValue = Ver_ParseSignal( pMan, VER_SIG_REG ); + RetValue = Ver_ParseSignal( pMan, pNtk, VER_SIG_REG ); else if ( !strcmp( pWord, "wire" ) ) - RetValue = Ver_ParseSignal( pMan, VER_SIG_WIRE ); + RetValue = Ver_ParseSignal( pMan, pNtk, VER_SIG_WIRE ); else if ( !strcmp( pWord, "inout" ) ) - RetValue = Ver_ParseSignal( pMan, VER_SIG_INOUT ); + RetValue = Ver_ParseSignal( pMan, pNtk, VER_SIG_INOUT ); else break; if ( RetValue == 0 ) @@ -334,43 +437,38 @@ int Ver_ParseModule( Ver_Man_t * pMan ) Extra_ProgressBarUpdate( pMan->pProgress, Ver_StreamGetCurPosition(p), NULL ); if ( !strcmp( pWord, "and" ) ) - RetValue = Ver_ParseGateStandard( pMan, VER_GATE_AND ); + RetValue = Ver_ParseGateStandard( pMan, pNtk, VER_GATE_AND ); else if ( !strcmp( pWord, "or" ) ) - RetValue = Ver_ParseGateStandard( pMan, VER_GATE_OR ); + RetValue = Ver_ParseGateStandard( pMan, pNtk, VER_GATE_OR ); else if ( !strcmp( pWord, "xor" ) ) - RetValue = Ver_ParseGateStandard( pMan, VER_GATE_XOR ); + RetValue = Ver_ParseGateStandard( pMan, pNtk, VER_GATE_XOR ); else if ( !strcmp( pWord, "buf" ) ) - RetValue = Ver_ParseGateStandard( pMan, VER_GATE_BUF ); + RetValue = Ver_ParseGateStandard( pMan, pNtk, VER_GATE_BUF ); else if ( !strcmp( pWord, "nand" ) ) - RetValue = Ver_ParseGateStandard( pMan, VER_GATE_NAND ); + RetValue = Ver_ParseGateStandard( pMan, pNtk, VER_GATE_NAND ); else if ( !strcmp( pWord, "nor" ) ) - RetValue = Ver_ParseGateStandard( pMan, VER_GATE_NOR ); + RetValue = Ver_ParseGateStandard( pMan, pNtk, VER_GATE_NOR ); else if ( !strcmp( pWord, "xnor" ) ) - RetValue = Ver_ParseGateStandard( pMan, VER_GATE_XNOR ); + RetValue = Ver_ParseGateStandard( pMan, pNtk, VER_GATE_XNOR ); else if ( !strcmp( pWord, "not" ) ) - RetValue = Ver_ParseGateStandard( pMan, VER_GATE_NOT ); + RetValue = Ver_ParseGateStandard( pMan, pNtk, VER_GATE_NOT ); else if ( !strcmp( pWord, "assign" ) ) - RetValue = Ver_ParseAssign( pMan ); + RetValue = Ver_ParseAssign( pMan, pNtk ); else if ( !strcmp( pWord, "always" ) ) - RetValue = Ver_ParseAlways( pMan ); + RetValue = Ver_ParseAlways( pMan, pNtk ); else if ( !strcmp( pWord, "initial" ) ) - RetValue = Ver_ParseInitial( pMan ); + RetValue = Ver_ParseInitial( pMan, pNtk ); else if ( !strcmp( pWord, "endmodule" ) ) break; - else if ( pMan->pDesign->pLibrary && st_lookup(pMan->pDesign->pLibrary->tModules, pWord, (char**)&pNtkTemp) ) // gate library - RetValue = Ver_ParseGate( pMan, pNtkTemp ); - else if ( pMan->pDesign && st_lookup(pMan->pDesign->tModules, pWord, (char**)&pNtkTemp) ) // current design - RetValue = Ver_ParseGate( pMan, pNtkTemp ); - else + else if ( pMan->pDesign->pGenlib && (pGate = Mio_LibraryReadGateByName(pMan->pDesign->pGenlib, pWord)) ) // current design + RetValue = Ver_ParseGate( pMan, pNtk, pGate ); +// else if ( pMan->pDesign->pLibrary && st_lookup(pMan->pDesign->pLibrary->tModules, pWord, (char**)&pNtkTemp) ) // gate library +// RetValue = Ver_ParseGate( pMan, pNtkTemp ); + else // assume this is the box used in the current design { - 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; + pNtkTemp = Ver_ParseFindOrCreateNetwork( pMan, pWord ); + RetValue = Ver_ParseBox( pMan, pNtk, pNtkTemp ); } if ( RetValue == 0 ) return 0; @@ -383,28 +481,33 @@ int Ver_ParseModule( Ver_Man_t * pMan ) return 0; } - // check if constant 0 net is used - pNet = Abc_NtkFindOrCreateNet( pNtk, "1\'b0" ); - if ( Abc_ObjFanoutNum(pNet) == 0 ) - Abc_NtkDeleteObj(pNet); - else - Abc_ObjAddFanin( pNet, Abc_NtkCreateNodeConst0(pNtk) ); - // check if constant 1 net is used - pNet = Abc_NtkFindOrCreateNet( pNtk, "1\'b1" ); - if ( Abc_ObjFanoutNum(pNet) == 0 ) - Abc_NtkDeleteObj(pNet); - else - Abc_ObjAddFanin( pNet, Abc_NtkCreateNodeConst1(pNtk) ); - - // check the functionality to blackbox if insides are not defined - if ( Abc_NtkNodeNum(pNtk) == 0 && Abc_NtkBoxNum(pNtk) == 0 ) + // convert from the blackbox into the network with local functions representated by AIGs + if ( pNtk->ntkFunc == ABC_FUNC_BLACKBOX ) { - pNtk->ntkFunc = ABC_FUNC_BLACKBOX; - pNtk->pManFunc = NULL; + if ( Abc_NtkNodeNum(pNtk) > 0 || Abc_NtkBoxNum(pNtk) > 0 ) + { + if ( !Ver_ParseConvertNetwork( pMan, pNtk, pMan->fMapped ) ) + return 0; + } + else + { + Abc_Obj_t * pObj, * pBox, * pTerm; + int i; + pBox = Abc_NtkCreateBlackbox(pNtk); + Abc_NtkForEachPi( pNtk, pObj, i ) + { + pTerm = Abc_NtkCreateBi(pNtk); + Abc_ObjAddFanin( pTerm, Abc_ObjFanout0(pObj) ); + Abc_ObjAddFanin( pBox, pTerm ); + } + Abc_NtkForEachPo( pNtk, pObj, i ) + { + pTerm = Abc_NtkCreateBo(pNtk); + Abc_ObjAddFanin( pTerm, pBox ); + Abc_ObjAddFanin( Abc_ObjFanin0(pObj), pTerm ); + } + } } - - // fix the dangling nets - Abc_NtkFinalizeRead( pNtk ); return 1; } @@ -419,19 +522,21 @@ int Ver_ParseModule( Ver_Man_t * pMan ) SeeAlso [] ***********************************************************************/ -int Ver_ParseSignal( Ver_Man_t * pMan, Ver_SignalType_t SigType ) +int Ver_ParseSignal( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Ver_SignalType_t SigType ) { Ver_Stream_t * p = pMan->pReader; - Abc_Ntk_t * pNtk = pMan->pNtkCur; char Buffer[1000]; int Lower, Upper, i; char * pWord; char Symbol; + Lower = Upper = 0; while ( 1 ) { pWord = Ver_ParseGetName( pMan ); if ( pWord == NULL ) return 0; + + // check if the range is specified if ( pWord[0] == '[' && !pMan->fNameLast ) { Lower = atoi( pWord + 1 ); @@ -472,6 +577,20 @@ int Ver_ParseSignal( Ver_Man_t * pMan, Ver_SignalType_t SigType ) if ( pWord == NULL ) return 0; } + } + + // create signals + if ( Lower == 0 && Upper == 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 ); + } + else + { for ( i = Lower; i <= Upper; i++ ) { sprintf( Buffer, "%s[%d]", pWord, i ); @@ -483,15 +602,7 @@ int Ver_ParseSignal( Ver_Man_t * pMan, Ver_SignalType_t SigType ) Abc_NtkFindOrCreateNet( pNtk, Buffer ); } } - else - { - 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; @@ -515,118 +626,90 @@ int Ver_ParseSignal( Ver_Man_t * pMan, Ver_SignalType_t SigType ) SeeAlso [] ***********************************************************************/ -int Ver_ParseAssign( Ver_Man_t * pMan ) +int Ver_ParseAlways( Ver_Man_t * pMan, Abc_Ntk_t * pNtk ) { Ver_Stream_t * p = pMan->pReader; - Abc_Ntk_t * pNtk = pMan->pNtkCur; - Abc_Obj_t * pNode, * pNet; - char * pWord, * pName, * pEquation; - Hop_Obj_t * pFunc; + Abc_Obj_t * pNet, * pNet2; + int fStopAfterOne; + char * pWord, * pWord2; char Symbol; - int i, Length, fReduction; - -// if ( Ver_StreamGetLineNumber(p) == 2756 ) -// { -// int x = 0; -// } - - // convert from the mapped netlist into the BDD netlist - if ( pNtk->ntkFunc == ABC_FUNC_BLACKBOX ) - { - pNtk->ntkFunc = ABC_FUNC_AIG; - assert( pNtk->pManFunc == NULL ); - pNtk->pManFunc = pMan->pDesign->pManFunc; - } - else if ( pNtk->ntkFunc != ABC_FUNC_AIG ) - { - 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 ); + // parse the directive + pWord = Ver_ParseGetName( pMan ); + if ( pWord == NULL ) return 0; - } - - while ( 1 ) + if ( pWord[0] == '@' ) { - // get the name of the output signal + Ver_StreamSkipToChars( p, ")" ); + Ver_StreamPopChar(p); + // parse the directive pWord = Ver_ParseGetName( pMan ); if ( pWord == NULL ) return 0; - // consider the case of reduction operations - fReduction = 0; - if ( pWord[0] == '{' && !pMan->fNameLast ) - fReduction = 1; - if ( fReduction ) + } + // decide how many statements to parse + fStopAfterOne = 0; + if ( strcmp( pWord, "begin" ) ) + fStopAfterOne = 1; + // iterate over the initial states + while ( 1 ) + { + if ( !fStopAfterOne ) { - pWord++; - pWord[strlen(pWord)-1] = 0; - assert( pWord[0] != '\\' ); + // 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 ); + pNet = Ver_ParseFindNet( pNtk, pWord ); if ( pNet == NULL ) { - sprintf( pMan->sError, "Cannot read the assign statement for %s (output wire is not defined).", pWord ); + sprintf( pMan->sError, "Cannot read the always statement for %s (output wire is not defined).", pWord ); Ver_ParsePrintErrorMessage( pMan ); return 0; } // get the equality sign - if ( Ver_StreamPopChar(p) != '=' ) + Symbol = Ver_StreamPopChar(p); + if ( Symbol != '<' && Symbol != '=' ) { - sprintf( pMan->sError, "Cannot read the assign statement for %s (expected equality sign).", pWord ); + sprintf( pMan->sError, "Cannot read the assign statement for %s (expected <= or =).", pWord ); Ver_ParsePrintErrorMessage( pMan ); return 0; } + if ( Symbol == '<' ) + Ver_StreamPopChar(p); // skip the comments if ( !Ver_ParseSkipComments( pMan ) ) return 0; // get the second name - if ( fReduction ) - pEquation = Ver_StreamGetWord( p, ";" ); - else - pEquation = Ver_StreamGetWord( p, ",;" ); - if ( pEquation == NULL ) - { - sprintf( pMan->sError, "Cannot read the equation for %s.", Abc_ObjName(pNet) ); - Ver_ParsePrintErrorMessage( pMan ); + pWord2 = Ver_ParseGetName( pMan ); + if ( pWord2 == NULL ) return 0; + // check if the name is complemented + if ( pWord2[0] == '~' ) + { + pNet2 = Ver_ParseFindNet( pNtk, pWord2+1 ); + pNet2 = Ver_ParseCreateInv( pNtk, pNet2 ); } - - // parse the formula - if ( fReduction ) - pFunc = Ver_FormulaReduction( pEquation, pNtk->pManFunc, pMan->vNames, pMan->sError ); else - pFunc = Ver_FormulaParser( pEquation, pNtk->pManFunc, pMan->vNames, pMan->vStackFn, pMan->vStackOp, pMan->sError ); - if ( pFunc == NULL ) + pNet2 = Ver_ParseFindNet( 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 node with the given inputs - pNode = Abc_NtkCreateNode( pMan->pNtkCur ); - pNode->pData = pFunc; - Abc_ObjAddFanin( pNet, pNode ); - // connect to fanin nets - for ( i = 0; i < Vec_PtrSize(pMan->vNames)/2; i++ ) - { - // get the name of this signal - Length = (int)Vec_PtrEntry( pMan->vNames, 2*i ); - pName = Vec_PtrEntry( pMan->vNames, 2*i + 1 ); - pName[Length] = 0; - // find the corresponding net - pNet = 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 ); - } + // create the latch + Ver_ParseCreateLatch( pNtk, pNet2, pNet ); + // remove the last symbol Symbol = Ver_StreamPopChar(p); - if ( Symbol == ',' ) - continue; - if ( Symbol == ';' ) - return 1; + assert( Symbol == ';' ); + // quit if only one directive + if ( fStopAfterOne ) + break; } return 1; } @@ -642,27 +725,17 @@ int Ver_ParseAssign( Ver_Man_t * pMan ) SeeAlso [] ***********************************************************************/ -int Ver_ParseAlways( Ver_Man_t * pMan ) +int Ver_ParseInitial( Ver_Man_t * pMan, Abc_Ntk_t * pNtk ) { Ver_Stream_t * p = pMan->pReader; - Abc_Ntk_t * pNtk = pMan->pNtkCur; - Abc_Obj_t * pNet, * pNet2; + Abc_Obj_t * pNode, * pNet; int fStopAfterOne; - char * pWord, * pWord2; + char * pWord, * pEquation; char Symbol; // parse the directive pWord = Ver_ParseGetName( pMan ); if ( pWord == NULL ) return 0; - if ( pWord[0] == '@' ) - { - Ver_StreamSkipToChars( p, ")" ); - Ver_StreamPopChar(p); - // parse the directive - pWord = Ver_ParseGetName( pMan ); - if ( pWord == NULL ) - return 0; - } // decide how many statements to parse fStopAfterOne = 0; if ( strcmp( pWord, "begin" ) ) @@ -681,10 +754,10 @@ int Ver_ParseAlways( Ver_Man_t * pMan ) break; } // get the fanout net - pNet = Abc_NtkFindNet( pNtk, pWord ); + pNet = Ver_ParseFindNet( pNtk, pWord ); if ( pNet == NULL ) { - sprintf( pMan->sError, "Cannot read the always statement for %s (output wire is not defined).", pWord ); + sprintf( pMan->sError, "Cannot read the initial statement for %s (output wire is not defined).", pWord ); Ver_ParsePrintErrorMessage( pMan ); return 0; } @@ -702,25 +775,31 @@ int Ver_ParseAlways( Ver_Man_t * pMan ) if ( !Ver_ParseSkipComments( pMan ) ) return 0; // get the second name - pWord2 = Ver_ParseGetName( pMan ); - if ( pWord2 == NULL ) + pEquation = Ver_StreamGetWord( p, ";" ); + if ( pEquation == NULL ) return 0; - // check if the name is complemented - if ( pWord2[0] == '~' ) + // find the corresponding latch + if ( Abc_ObjFaninNum(pNet) == 0 ) { - pNet2 = Abc_NtkFindNet( pNtk, pWord2+1 ); - pNet2 = Ver_ParseCreateInv( pNtk, pNet2 ); + sprintf( pMan->sError, "Cannot find the latch to assign the initial value." ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; } - else - pNet2 = Abc_NtkFindNet( pNtk, pWord2 ); - if ( pNet2 == NULL ) + pNode = Abc_ObjFanin0(Abc_ObjFanin0(pNet)); + assert( Abc_ObjIsLatch(pNode) ); + // set the initial state + if ( !strcmp(pEquation, "0") || !strcmp(pEquation, "1\'b0") ) + Abc_LatchSetInit0( pNode ); + else if ( !strcmp(pEquation, "1") || !strcmp(pEquation, "1\'b1") ) + Abc_LatchSetInit1( pNode ); +// else if ( !strcmp(pEquation, "2") ) +// Abc_LatchSetInitDc( pNode ); + else { - sprintf( pMan->sError, "Cannot read the always statement for %s (input wire is not defined).", pWord2 ); + sprintf( pMan->sError, "Incorrect initial value of the latch %s.", Abc_ObjName(pNet) ); Ver_ParsePrintErrorMessage( pMan ); return 0; } - // create the latch - Ver_ParseCreateLatch( pNtk, pNet2, pNet ); // remove the last symbol Symbol = Ver_StreamPopChar(p); assert( Symbol == ';' ); @@ -742,88 +821,397 @@ int Ver_ParseAlways( Ver_Man_t * pMan ) SeeAlso [] ***********************************************************************/ -int Ver_ParseInitial( Ver_Man_t * pMan ) +int Ver_ParseAssign( Ver_Man_t * pMan, Abc_Ntk_t * pNtk ) { Ver_Stream_t * p = pMan->pReader; - Abc_Ntk_t * pNtk = pMan->pNtkCur; Abc_Obj_t * pNode, * pNet; - int fStopAfterOne; - char * pWord, * pEquation; + char * pWord, * pName, * pEquation; + Hop_Obj_t * pFunc; char Symbol; - // parse the directive - pWord = Ver_ParseGetName( pMan ); - if ( pWord == NULL ) + int i, Length, fReduction; + +// if ( Ver_StreamGetLineNumber(p) == 2756 ) +// { +// int x = 0; +// } + + // convert from the blackbox into the network with local functions representated by AIGs + if ( !Ver_ParseConvertNetwork( pMan, pNtk, pMan->fMapped ) ) return 0; - // decide how many statements to parse - fStopAfterOne = 0; - if ( strcmp( pWord, "begin" ) ) - fStopAfterOne = 1; - // iterate over the initial states + while ( 1 ) { - if ( !fStopAfterOne ) + // get the name of the output signal + pWord = Ver_ParseGetName( pMan ); + if ( pWord == NULL ) + return 0; + // consider the case of reduction operations + fReduction = 0; + if ( pWord[0] == '{' && !pMan->fNameLast ) + fReduction = 1; + if ( fReduction ) { - // 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; + pWord++; + pWord[strlen(pWord)-1] = 0; + assert( pWord[0] != '\\' ); } // get the fanout net - pNet = Abc_NtkFindNet( pNtk, pWord ); + pNet = Ver_ParseFindNet( pNtk, pWord ); if ( pNet == NULL ) { - sprintf( pMan->sError, "Cannot read the initial statement for %s (output wire is not defined).", pWord ); + sprintf( pMan->sError, "Cannot read the assign statement for %s (output wire is not defined).", pWord ); Ver_ParsePrintErrorMessage( pMan ); return 0; } // get the equality sign - Symbol = Ver_StreamPopChar(p); - if ( Symbol != '<' && Symbol != '=' ) + if ( Ver_StreamPopChar(p) != '=' ) { - sprintf( pMan->sError, "Cannot read the assign statement for %s (expected <= or =).", pWord ); + sprintf( pMan->sError, "Cannot read the assign statement for %s (expected equality sign).", pWord ); Ver_ParsePrintErrorMessage( pMan ); return 0; } - if ( Symbol == '<' ) - Ver_StreamPopChar(p); // skip the comments if ( !Ver_ParseSkipComments( pMan ) ) return 0; // get the second name - pEquation = Ver_StreamGetWord( p, ";" ); + if ( fReduction ) + pEquation = Ver_StreamGetWord( p, ";" ); + else + pEquation = Ver_StreamGetWord( p, ",;" ); if ( pEquation == NULL ) + { + sprintf( pMan->sError, "Cannot read the equation for %s.", Abc_ObjName(pNet) ); + Ver_ParsePrintErrorMessage( pMan ); return 0; - // find the corresponding latch - if ( Abc_ObjFaninNum(pNet) == 0 ) + } + + // consider the case of mapped network + if ( pMan->fMapped ) { - sprintf( pMan->sError, "Cannot find the latch to assign the initial value." ); + Vec_PtrClear( pMan->vNames ); + if ( !strcmp( pEquation, "1\'b0" ) ) + pFunc = (Hop_Obj_t *)Mio_LibraryReadConst0(Abc_FrameReadLibGen()); + else if ( !strcmp( pEquation, "1\'b1" ) ) + pFunc = (Hop_Obj_t *)Mio_LibraryReadConst1(Abc_FrameReadLibGen()); + else + { + if ( Ver_ParseFindNet(pNtk, pEquation) == NULL ) + { + sprintf( pMan->sError, "Cannot read Verilog with non-trivail assignments in the mapped netlist.", pEquation ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + Vec_PtrPush( pMan->vNames, (void *)strlen(pEquation) ); + Vec_PtrPush( pMan->vNames, pEquation ); + // get the buffer + pFunc = (Hop_Obj_t *)Mio_LibraryReadBuf(Abc_FrameReadLibGen()); + } + } + else + { + // parse the formula + if ( fReduction ) + pFunc = Ver_FormulaReduction( pEquation, pNtk->pManFunc, pMan->vNames, pMan->sError ); + else + pFunc = Ver_FormulaParser( pEquation, pNtk->pManFunc, pMan->vNames, pMan->vStackFn, pMan->vStackOp, pMan->sError ); + if ( pFunc == NULL ) + { + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + } + + // create the node with the given inputs + pNode = Abc_NtkCreateNode( pNtk ); + pNode->pData = pFunc; + Abc_ObjAddFanin( pNet, pNode ); + // connect to fanin nets + for ( i = 0; i < Vec_PtrSize(pMan->vNames)/2; i++ ) + { + // get the name of this signal + Length = (int)Vec_PtrEntry( pMan->vNames, 2*i ); + pName = Vec_PtrEntry( pMan->vNames, 2*i + 1 ); + pName[Length] = 0; + // find the corresponding net + pNet = Ver_ParseFindNet( pNtk, pName ); + if ( pNet == NULL ) + { + sprintf( pMan->sError, "Cannot read the assign statement for %s (input wire %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_ParseGateStandard( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Ver_GateType_t GateType ) +{ + Ver_Stream_t * p = pMan->pReader; + Abc_Obj_t * pNet, * pNode; + char * pWord, Symbol; + + // convert from the blackbox into the network with local functions representated by AIGs + if ( !Ver_ParseConvertNetwork( pMan, pNtk, pMan->fMapped ) ) + return 0; + + // this is gate name - throw it away + if ( Ver_StreamPopChar(p) != '(' ) + { + sprintf( pMan->sError, "Cannot parse a standard gate (expected opening paranthesis)." ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + Ver_ParseSkipComments( pMan ); + + // create the node + pNode = Abc_NtkCreateNode( pNtk ); + + // parse pairs of formal/actural inputs + while ( 1 ) + { + // parse the output name + pWord = Ver_ParseGetName( pMan ); + if ( pWord == NULL ) + return 0; + // get the net corresponding to this output + pNet = Ver_ParseFindNet( pNtk, pWord ); + if ( pNet == NULL ) + { + sprintf( pMan->sError, "Net is missing in gate %s.", pWord ); Ver_ParsePrintErrorMessage( pMan ); return 0; } - pNode = Abc_ObjFanin0(Abc_ObjFanin0(pNet)); - assert( Abc_ObjIsLatch(pNode) ); - // set the initial state - if ( !strcmp(pEquation, "0") || !strcmp(pEquation, "1\'b0") ) - Abc_LatchSetInit0( pNode ); - else if ( !strcmp(pEquation, "1") || !strcmp(pEquation, "1\'b1") ) - Abc_LatchSetInit1( pNode ); -// else if ( !strcmp(pEquation, "2") ) -// Abc_LatchSetInitDc( pNode ); - else + // if this is the first net, add it as an output + if ( Abc_ObjFanoutNum(pNode) == 0 ) + Abc_ObjAddFanin( pNet, pNode ); + else + Abc_ObjAddFanin( pNode, pNet ); + // 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 parse a standard gate %s (expected closing paranthesis).", Abc_ObjName(Abc_ObjFanout0(pNode)) ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + Ver_ParseSkipComments( pMan ); + } + if ( (GateType == VER_GATE_BUF || GateType == VER_GATE_NOT) && Abc_ObjFaninNum(pNode) != 1 ) + { + sprintf( pMan->sError, "Buffer or interver with multiple fanouts %s (currently not supported).", Abc_ObjName(Abc_ObjFanout0(pNode)) ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + + // check if it is the end of gate + Ver_ParseSkipComments( pMan ); + if ( Ver_StreamPopChar(p) != ';' ) + { + sprintf( pMan->sError, "Cannot read standard gate %s (expected closing semicolumn).", Abc_ObjName(Abc_ObjFanout0(pNode)) ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + // add logic function + if ( GateType == VER_GATE_AND || GateType == VER_GATE_NAND ) + pNode->pData = Hop_CreateAnd( pNtk->pManFunc, Abc_ObjFaninNum(pNode) ); + else if ( GateType == VER_GATE_OR || GateType == VER_GATE_NOR ) + pNode->pData = Hop_CreateOr( pNtk->pManFunc, Abc_ObjFaninNum(pNode) ); + else if ( GateType == VER_GATE_XOR || GateType == VER_GATE_XNOR ) + pNode->pData = Hop_CreateExor( pNtk->pManFunc, Abc_ObjFaninNum(pNode) ); + else if ( GateType == VER_GATE_BUF || GateType == VER_GATE_NOT ) + pNode->pData = Hop_CreateAnd( pNtk->pManFunc, Abc_ObjFaninNum(pNode) ); + if ( GateType == VER_GATE_NAND || GateType == VER_GATE_NOR || GateType == VER_GATE_XNOR || GateType == VER_GATE_NOT ) + pNode->pData = Hop_Not( pNode->pData ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Parses one directive.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Mio_Gate_t * pGate ) +{ + Mio_Pin_t * pGatePin; + Ver_Stream_t * p = pMan->pReader; + Abc_Obj_t * pNetActual, * pNode; + char * pWord, Symbol; + + // convert from the blackbox into the network with local functions representated by gates + if ( 1 != pMan->fMapped ) + { + sprintf( pMan->sError, "The network appears to be mapped. Use \"r -m\" to read mapped Verilog." ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + + // update the network type if needed + if ( !Ver_ParseConvertNetwork( pMan, pNtk, 1 ) ) + return 0; + + // 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).", Mio_GateReadName(pGate) ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + + // start the node + pNode = Abc_NtkCreateNode( pNtk ); + pNode->pData = pGate; + + // parse pairs of formal/actural inputs + pGatePin = Mio_GateReadPins(pGate); + while ( 1 ) + { + // process one pair of formal/actual parameters + if ( Ver_StreamPopChar(p) != '.' ) + { + sprintf( pMan->sError, "Cannot parse gate %s (expected .).", Mio_GateReadName(pGate) ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + + // parse the formal name + pWord = Ver_ParseGetName( pMan ); + if ( pWord == NULL ) + return 0; + + // make sure that the formal name is the same as the gate's + if ( Mio_GateReadInputs(pGate) == Abc_ObjFaninNum(pNode) ) + { + if ( strcmp(pWord, Mio_GateReadOutName(pGate)) ) + { + sprintf( pMan->sError, "Formal output name listed %s is different from the name of the gate output %s.", pWord, Mio_GateReadOutName(pGate) ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + } + else + { + if ( strcmp(pWord, Mio_PinReadName(pGatePin)) ) + { + sprintf( pMan->sError, "Formal input name listed %s is different from the name of the corresponding pin %s.", pWord, Mio_PinReadName(pGatePin) ); + 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, Mio_GateReadName(pGate) ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + + // parse the actual name + pWord = Ver_ParseGetName( pMan ); + if ( pWord == NULL ) + return 0; + // check if the name is complemented + assert( pWord[0] != '~' ); +/* + fCompl = (pWord[0] == '~'); + if ( fCompl ) + { + fComplUsed = 1; + pWord++; + if ( pNtk->pData == NULL ) + pNtk->pData = Extra_MmFlexStart(); + } +*/ + // get the actual net + pNetActual = Ver_ParseFindNet( pNtk, pWord ); + if ( pNetActual == NULL ) + { + sprintf( pMan->sError, "Actual net %s is missing.", 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, Mio_GateReadName(pGate) ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + + // add the fanin + if ( Mio_GateReadInputs(pGate) == Abc_ObjFaninNum(pNode) ) + Abc_ObjAddFanin( pNetActual, pNode ); // fanout + else + Abc_ObjAddFanin( pNode, pNetActual ); // fanin + + // 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, "Incorrect initial value of the latch %s.", Abc_ObjName(pNet) ); + sprintf( pMan->sError, "Cannot formal parameter %s of gate %s (expected closing paranthesis).", pWord, Mio_GateReadName(pGate) ); Ver_ParsePrintErrorMessage( pMan ); return 0; } - // remove the last symbol - Symbol = Ver_StreamPopChar(p); - assert( Symbol == ';' ); - // quit if only one directive - if ( fStopAfterOne ) - break; + Ver_ParseSkipComments( pMan ); + + // get the next pin + pGatePin = Mio_PinReadNext(pGatePin); + } + + // check that the gate as the same number of input + if ( !(Abc_ObjFaninNum(pNode) == Mio_GateReadInputs(pGate) && Abc_ObjFanoutNum(pNode) == 1) ) + { + sprintf( pMan->sError, "Parsing of gate %s has failed.", Mio_GateReadName(pGate) ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + + // 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).", Mio_GateReadName(pGate) ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; } return 1; } @@ -839,40 +1227,42 @@ int Ver_ParseInitial( Ver_Man_t * pMan ) SeeAlso [] ***********************************************************************/ -int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtkGate ) +int Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox ) { Ver_Stream_t * p = pMan->pReader; - Abc_Ntk_t * pNtk = pMan->pNtkCur; + Vec_Ptr_t * vNetPairs; Abc_Obj_t * pNetFormal, * pNetActual; - Abc_Obj_t * pObj, * pNode, * pTerm; - char * pWord, Symbol, * pGateName; - int i, fCompl, fComplUsed = 0; - unsigned * pPolarity; - - // clean the PI/PO pointers - Abc_NtkForEachPi( pNtkGate, pObj, i ) - pObj->pCopy = NULL; - Abc_NtkForEachPo( pNtkGate, pObj, i ) - pObj->pCopy = NULL; + Abc_Obj_t * pNode; + char * pWord, Symbol; + int fCompl; + // 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 - pGateName = pWord; + + // create box to represent this gate + pNode = Abc_NtkCreateBlackbox( pNtk ); + pNode->pData = pNtkBox; + Abc_ObjAssignName( pNode, pWord, NULL ); + + // continue parsing the box if ( Ver_StreamPopChar(p) != '(' ) { - sprintf( pMan->sError, "Cannot parse gate %s (expected opening paranthesis).", pNtkGate->pName ); + sprintf( pMan->sError, "Cannot parse gate %s (expected opening paranthesis).", Abc_ObjName(pNode) ); Ver_ParsePrintErrorMessage( pMan ); return 0; } + // parse pairs of formal/actural inputs + vNetPairs = Vec_PtrAlloc( 16 ); + pNode->pCopy = (Abc_Obj_t *)vNetPairs; while ( 1 ) { // process one pair of formal/actual parameters if ( Ver_StreamPopChar(p) != '.' ) { - sprintf( pMan->sError, "Cannot parse gate %s (expected .).", pNtkGate->pName ); + sprintf( pMan->sError, "Cannot parse gate %s (expected .).", Abc_ObjName(pNode) ); Ver_ParsePrintErrorMessage( pMan ); return 0; } @@ -882,21 +1272,13 @@ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtkGate ) if ( pWord == NULL ) return 0; // get the formal net - if ( Abc_NtkIsNetlist(pNtkGate) ) - pNetFormal = Abc_NtkFindNet( pNtkGate, pWord ); - else // if ( Abc_NtkIsStrash(pNtkGate) ) - assert( 0 ); - if ( pNetFormal == NULL ) - { - sprintf( pMan->sError, "Formal net is missing in gate %s.", pWord ); - Ver_ParsePrintErrorMessage( pMan ); - return 0; - } + pNetFormal = Abc_NtkFindOrCreateNet( pNtkBox, pWord ); + Vec_PtrPush( vNetPairs, pNetFormal ); // open the paranthesis if ( Ver_StreamPopChar(p) != '(' ) { - sprintf( pMan->sError, "Cannot formal parameter %s of gate %s (expected opening paranthesis).", pWord, pNtkGate->pName ); + sprintf( pMan->sError, "Cannot formal parameter %s of gate %s (expected opening paranthesis).", pWord, Abc_ObjName(pNode)); Ver_ParsePrintErrorMessage( pMan ); return 0; } @@ -905,43 +1287,41 @@ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtkGate ) pWord = Ver_ParseGetName( pMan ); if ( pWord == NULL ) return 0; - // check if the name is complemented - fCompl = (pWord[0] == '~'); - if ( fCompl ) + // consider the case of empty name + fCompl = 0; + if ( pWord[0] == 0 ) { - fComplUsed = 1; - pWord++; - if ( pMan->pNtkCur->pData == NULL ) - pMan->pNtkCur->pData = Extra_MmFlexStart(); + // remove the formal net +// Vec_PtrPop( vNetPairs ); + pNetActual = Abc_NtkCreateObj( pNtk, ABC_OBJ_NET ); } - // get the actual net - pNetActual = Abc_NtkFindNet( pMan->pNtkCur, pWord ); - if ( pNetActual == NULL ) + else { - sprintf( pMan->sError, "Actual net is missing in gate %s.", pWord ); - Ver_ParsePrintErrorMessage( pMan ); - return 0; +/* + // check if the name is complemented + fCompl = (pWord[0] == '~'); + if ( fCompl ) + { + pWord++; + if ( pNtk->pData == NULL ) + pNtk->pData = Extra_MmFlexStart(); + } +*/ + // get the actual net + pNetActual = Ver_ParseFindNet( pNtk, pWord ); + if ( pNetActual == NULL ) + { + sprintf( pMan->sError, "Actual net is missing in gate %s.", Abc_ObjName(pNode) ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } } + Vec_PtrPush( vNetPairs, Abc_ObjNotCond( pNetActual, fCompl ) ); // 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_ObjFaninNum(pNetFormal) > 0 && Abc_ObjIsPi(Abc_ObjFanin0Ntk(pNetFormal)) ) // PI net (with polarity!) - Abc_ObjFanin0Ntk(pNetFormal)->pCopy = Abc_ObjNotCond( pNetActual, fCompl ); - else if ( Abc_ObjFanoutNum(pNetFormal) > 0 && 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 ); + sprintf( pMan->sError, "Cannot formal parameter %s of gate %s (expected closing paranthesis).", pWord, Abc_ObjName(pNode) ); Ver_ParsePrintErrorMessage( pMan ); return 0; } @@ -954,7 +1334,7 @@ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtkGate ) // skip comma if ( Symbol != ',' ) { - sprintf( pMan->sError, "Cannot formal parameter %s of gate %s (expected closing paranthesis).", pWord, pNtkGate->pName ); + sprintf( pMan->sError, "Cannot formal parameter %s of gate %s (expected closing paranthesis).", pWord, Abc_ObjName(pNode) ); Ver_ParsePrintErrorMessage( pMan ); return 0; } @@ -965,160 +1345,277 @@ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtkGate ) Ver_ParseSkipComments( pMan ); if ( Ver_StreamPopChar(p) != ';' ) { - sprintf( pMan->sError, "Cannot read gate %s (expected closing semicolumn).", pNtkGate->pName ); + sprintf( pMan->sError, "Cannot read gate %s (expected closing semicolumn).", Abc_ObjName(pNode) ); 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_ObjName(Abc_ObjFanout0(pObj)), 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_ObjName(Abc_ObjFanin0(pObj)), pNtkGate->pName ); - Ver_ParsePrintErrorMessage( pMan ); - return 0; - } -*/ + return 1; +} - // allocate memory to remember the phase - pPolarity = NULL; - if ( fComplUsed ) +/**Function************************************************************* + + Synopsis [Connects one box to the network] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ver_ParseConnectBox( Ver_Man_t * pMan, Abc_Obj_t * pBox ) +{ + Vec_Ptr_t * vNetPairs = (Vec_Ptr_t *)pBox->pCopy; + Abc_Ntk_t * pNtk = pBox->pNtk; + Abc_Ntk_t * pNtkBox = pBox->pData; + Abc_Obj_t * pNet, * pTerm, * pTermNew; + int i; + + assert( !Ver_ObjIsConnected(pBox) ); + assert( Ver_NtkIsDefined(pNtkBox) ); + assert( !Abc_NtkHasBlackbox(pNtkBox) || Abc_NtkBoxNum(pNtkBox) == 1 ); + + // clean the PI/PO nets + Abc_NtkForEachPi( pNtkBox, pTerm, i ) + Abc_ObjFanout0(pTerm)->pCopy = NULL; + Abc_NtkForEachPo( pNtkBox, pTerm, i ) + Abc_ObjFanin0(pTerm)->pCopy = NULL; + + // map formal nets into actual nets + Vec_PtrForEachEntry( vNetPairs, pNet, i ) { - int nBytes = 4 * Abc_BitWordNum( Abc_NtkPiNum(pNtkGate) ); - pPolarity = (unsigned *)Extra_MmFlexEntryFetch( pMan->pNtkCur->pData, nBytes ); - memset( pPolarity, 0, nBytes ); + // get the actual net corresponding to this formal net (pNet) + pNet->pCopy = Vec_PtrEntry( vNetPairs, ++i ); + // make sure the actual net is not complemented (otherwise need to use polarity) + assert( !Abc_ObjIsComplement(pNet->pCopy) ); } - // create box to represent this gate - if ( Abc_NtkHasBlackbox(pNtkGate) ) - pNode = Abc_NtkCreateBlackbox( pMan->pNtkCur ); - else - pNode = Abc_NtkCreateWhitebox( pMan->pNtkCur ); - pNode->pNext = (Abc_Obj_t *)pPolarity; - pNode->pData = pNtkGate; - // connect to fanin nets - Abc_NtkForEachPi( pNtkGate, pObj, i ) + + // make sure all PI nets are assigned + Abc_NtkForEachPi( pNtkBox, pTerm, i ) { - if ( pPolarity && Abc_ObjIsComplement(pObj->pCopy) ) + if ( Abc_ObjFanout0(pTerm)->pCopy == NULL ) { - Abc_InfoSetBit( pPolarity, i ); - pObj->pCopy = Abc_ObjRegular( pObj->pCopy ); + sprintf( pMan->sError, "Input formal net %s of network %s is not driven in box %s.", + Abc_ObjName(Abc_ObjFanout0(pTerm)), pNtkBox->pName, Abc_ObjName(pBox) ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; } - assert( !Abc_ObjIsComplement(pObj->pCopy) ); -// Abc_ObjAddFanin( pNode, pObj->pCopy ); - pTerm = Abc_NtkCreateBi( pNtk ); - Abc_ObjAddFanin( pTerm, pObj->pCopy ); - Abc_ObjAddFanin( pNode, pTerm ); + pTermNew = Abc_NtkCreateBi( pNtk ); + Abc_ObjAddFanin( pBox, pTermNew ); + Abc_ObjAddFanin( pTermNew, Abc_ObjFanout0(pTerm)->pCopy ); } - // connect to fanout nets - Abc_NtkForEachPo( pNtkGate, pObj, i ) + + // create fanins of the box + Abc_NtkForEachPo( pNtkBox, pTerm, i ) { - if ( pObj->pCopy == NULL ) - pObj->pCopy = Abc_NtkFindOrCreateNet(pNtk, NULL); -// Abc_ObjAddFanin( pObj->pCopy, pNode ); - pTerm = Abc_NtkCreateBo( pNtk ); - Abc_ObjAddFanin( pTerm, pNode ); - Abc_ObjAddFanin( pObj->pCopy, pTerm ); + if ( Abc_ObjFanin0(pTerm)->pCopy == NULL ) + Abc_ObjFanin0(pTerm)->pCopy = Abc_NtkCreateObj( pNtk, ABC_OBJ_NET ); + pTermNew = Abc_NtkCreateBo( pNtk ); + Abc_ObjAddFanin( Abc_ObjFanin0(pTerm)->pCopy, pTermNew ); + Abc_ObjAddFanin( pTermNew, pBox ); } + + // free the mapping + Vec_PtrFree( vNetPairs ); + pBox->pCopy = NULL; return 1; } - /**Function************************************************************* - Synopsis [Parses one directive.] + Synopsis [Attaches the boxes to the network.] - Description [] + Description [Makes sure that the undefined boxes are connected correctly.] SideEffects [] SeeAlso [] ***********************************************************************/ -int Ver_ParseGateStandard( Ver_Man_t * pMan, Ver_GateType_t GateType ) +int Vec_ParseAttachBoxes( Ver_Man_t * pMan ) { - Ver_Stream_t * p = pMan->pReader; - Hop_Man_t * pAig = pMan->pNtkCur->pManFunc; - Abc_Obj_t * pNet, * pNode; - char * pWord, Symbol; - // this is gate name - throw it away - if ( Ver_StreamPopChar(p) != '(' ) + Abc_Ntk_t * pNtk, * pNtkBox; + Vec_Ptr_t * vEnvoys, * vNetPairs, * vPivots; + Abc_Obj_t * pBox, * pTerm, * pNet, * pNetDr, * pNetAct; + int i, k, m, nBoxes; + + // connect defined boxes + Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i ) { - sprintf( pMan->sError, "Cannot parse a standard gate (expected opening paranthesis)." ); - Ver_ParsePrintErrorMessage( pMan ); - return 0; + Abc_NtkForEachBlackbox( pNtk, pBox, k ) + { + if ( pBox->pData && Ver_NtkIsDefined(pBox->pData) ) + if ( !Ver_ParseConnectBox( pMan, pBox ) ) + return 0; + } } - Ver_ParseSkipComments( pMan ); - // create the node - pNode = Abc_NtkCreateNode( pMan->pNtkCur ); - // parse pairs of formal/actural inputs - while ( 1 ) + + // convert blackboxes to whiteboxes + Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i ) + Abc_NtkForEachBlackbox( pNtk, pBox, k ) + { + pNtkBox = pBox->pData; + if ( pNtkBox == NULL ) + continue; + + if ( !strcmp( pNtkBox->pName, "ADDHX1" ) ) + { + int x = 0; + } + + if ( pBox->pData && !Abc_NtkHasBlackbox(pBox->pData) ) + Abc_ObjBlackboxToWhitebox( pBox ); + } + + + // search for undefined boxes + nBoxes = 0; + Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i ) + nBoxes += !Ver_NtkIsDefined(pNtk); + // quit if no undefined boxes are found + if ( nBoxes == 0 ) + return 1; + + // count how many times each box occurs + Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i ) { - // parse the output name - pWord = Ver_ParseGetName( pMan ); - if ( pWord == NULL ) - return 0; - // get the net corresponding to this output - pNet = Abc_NtkFindNet( pMan->pNtkCur, pWord ); - if ( pNet == NULL ) + assert( pNtk->pData == NULL ); + pNtk->pData = NULL; + } + Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i ) + Abc_NtkForEachBlackbox( pNtk, pBox, k ) { - sprintf( pMan->sError, "Net is missing in gate %s.", pWord ); - Ver_ParsePrintErrorMessage( pMan ); - return 0; + if ( pBox->pData == NULL ) + continue; + pNtkBox = pBox->pData; + pNtkBox->pData = (void *)((int)pNtkBox->pData + 1); } - // if this is the first net, add it as an output - if ( Abc_ObjFanoutNum(pNode) == 0 ) - Abc_ObjAddFanin( pNet, pNode ); - else - Abc_ObjAddFanin( pNode, pNet ); - // check if it is the end of gate - Ver_ParseSkipComments( pMan ); - Symbol = Ver_StreamPopChar(p); - if ( Symbol == ')' ) - break; - // skip comma - if ( Symbol != ',' ) + + // print the boxes + printf( "Warning: The design contains %d undefined objects interpreted as blackboxes:\n", nBoxes ); + Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i ) + if ( !Ver_NtkIsDefined(pNtk) ) + printf( "%s (%d) ", Abc_NtkName(pNtk), (int)pNtk->pData ); + printf( "\n" ); + + // clean the boxes + Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i ) + pNtk->pData = NULL; + + + // map actual nets into formal nets belonging to the undef boxes + vPivots = Vec_PtrAlloc( 100 ); + Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i ) + { + Abc_NtkForEachBlackbox( pNtk, pBox, k ) { - sprintf( pMan->sError, "Cannot parse a standard gate %s (expected closing paranthesis).", Abc_ObjName(Abc_ObjFanout0(pNode)) ); - Ver_ParsePrintErrorMessage( pMan ); - return 0; + if ( pBox->pData == NULL || Ver_NtkIsDefined(pBox->pData) ) + continue; + vNetPairs = (Vec_Ptr_t *)pBox->pCopy; + Vec_PtrForEachEntry( vNetPairs, pNet, m ) + { + pNetAct = Vec_PtrEntry( vNetPairs, ++m ); + // skip already driven nets and constants + if ( Abc_ObjFaninNum(pNetAct) == 1 ) + continue; + if ( !(strcmp(Abc_ObjName(pNetAct), "1\'b0") && strcmp(Abc_ObjName(pNetAct), "1\'b1")) ) // constant + continue; + // add this net + if ( pNetAct->pData == NULL ) + { + pNetAct->pData = Vec_PtrAlloc( 16 ); + Vec_PtrPush( vPivots, pNetAct ); + } + vEnvoys = pNetAct->pData; + Vec_PtrPush( vEnvoys, pNet ); + } } - Ver_ParseSkipComments( pMan ); } - if ( (GateType == VER_GATE_BUF || GateType == VER_GATE_NOT) && Abc_ObjFaninNum(pNode) != 1 ) + + // for each pivot net, find the driver + Vec_PtrForEachEntry( vPivots, pNetAct, i ) { - sprintf( pMan->sError, "Buffer or interver with multiple fanouts %s (currently not supported).", Abc_ObjName(Abc_ObjFanout0(pNode)) ); - Ver_ParsePrintErrorMessage( pMan ); - return 0; + char * pName = Abc_ObjName(pNetAct); +/* + if ( !strcmp( Abc_ObjName(pNetAct), "dma_fifo_ff_cnt[2]" ) ) + { + int x = 0; + } +*/ + assert( Abc_ObjFaninNum(pNetAct) == 0 ); + assert( strcmp(Abc_ObjName(pNetAct), "1\'b0") && strcmp(Abc_ObjName(pNetAct), "1\'b1") ); + vEnvoys = pNetAct->pData; pNetAct->pData = NULL; + // find the driver starting from the last nets + pNetDr = NULL; + for ( m = 0; m < 64; m++ ) + { + Vec_PtrForEachEntry( vEnvoys, pNet, k ) + { + if ( Abc_ObjId(pNet) == 0 ) + continue; + if ( (int)Abc_ObjId(pNet) == Abc_NtkObjNumMax(pNet->pNtk) - 1 - m ) + { + pNetDr = pNet; + break; + } + } + if ( pNetDr ) + break; + } + assert( pNetDr != NULL ); + Vec_PtrWriteEntry( vPivots, i, pNetDr ); + Vec_PtrFree( vEnvoys ); } - // check if it is the end of gate - Ver_ParseSkipComments( pMan ); - if ( Ver_StreamPopChar(p) != ';' ) + // for each pivot net, create driver + Vec_PtrForEachEntry( vPivots, pNetDr, i ) { - sprintf( pMan->sError, "Cannot read standard gate %s (expected closing semicolumn).", Abc_ObjName(Abc_ObjFanout0(pNode)) ); - Ver_ParsePrintErrorMessage( pMan ); - return 0; + if ( pNetDr == NULL ) + continue; + assert( Abc_ObjFaninNum(pNetDr) <= 1 ); + if ( Abc_ObjFaninNum(pNetDr) == 1 ) + continue; + // drive this net with the box + pTerm = Abc_NtkCreateBo( pNetDr->pNtk ); + assert( Abc_NtkBoxNum(pNetDr->pNtk) <= 1 ); + pBox = Abc_NtkBoxNum(pNetDr->pNtk)? Abc_NtkBox(pNetDr->pNtk,0) : Abc_NtkCreateBlackbox(pNetDr->pNtk); + Abc_ObjAddFanin( Abc_NtkCreatePo(pNetDr->pNtk), pNetDr ); + Abc_ObjAddFanin( pNetDr, pTerm ); + Abc_ObjAddFanin( pTerm, pBox ); + } + Vec_PtrFree( vPivots ); + + // connect the remaining boxes + Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i ) + { + if ( Abc_NtkPiNum(pNtk) ) + continue; + Abc_NtkForEachNet( pNtk, pNet, k ) + { + if ( Abc_ObjFaninNum(pNet) ) + continue; + // drive this net + pTerm = Abc_NtkCreateBi( pNet->pNtk ); + assert( Abc_NtkBoxNum(pNet->pNtk) <= 1 ); + pBox = Abc_NtkBoxNum(pNet->pNtk)? Abc_NtkBox(pNet->pNtk,0) : Abc_NtkCreateBlackbox(pNet->pNtk); + Abc_ObjAddFanin( pBox, pTerm ); + Abc_ObjAddFanin( pTerm, pNet ); + Abc_ObjAddFanin( pNet, Abc_NtkCreatePi(pNet->pNtk) ); + } + } + + // connect the remaining boxes + Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i ) + { + Abc_NtkForEachBlackbox( pNtk, pBox, k ) + { + char * pName = Abc_ObjName(pBox); + if ( !Ver_ObjIsConnected(pBox) ) + if ( !Ver_ParseConnectBox( pMan, pBox ) ) + return 0; + } } - // add logic function - if ( GateType == VER_GATE_AND || GateType == VER_GATE_NAND ) - pNode->pData = Hop_CreateAnd( pAig, Abc_ObjFaninNum(pNode) ); - else if ( GateType == VER_GATE_OR || GateType == VER_GATE_NOR ) - pNode->pData = Hop_CreateOr( pAig, Abc_ObjFaninNum(pNode) ); - else if ( GateType == VER_GATE_XOR || GateType == VER_GATE_XNOR ) - pNode->pData = Hop_CreateExor( pAig, Abc_ObjFaninNum(pNode) ); - else if ( GateType == VER_GATE_BUF || GateType == VER_GATE_NOT ) - pNode->pData = Hop_CreateAnd( pAig, Abc_ObjFaninNum(pNode) ); - if ( GateType == VER_GATE_NAND || GateType == VER_GATE_NOR || GateType == VER_GATE_XNOR || GateType == VER_GATE_NOT ) - pNode->pData = Hop_Not( pNode->pData ); return 1; } @@ -1138,9 +1635,9 @@ 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 = Ver_ParseFindNet( 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 ); @@ -1163,9 +1660,9 @@ 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 = Ver_ParseFindNet( 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 ); @@ -1224,6 +1721,50 @@ Abc_Obj_t * Ver_ParseCreateInv( Abc_Ntk_t * pNtk, Abc_Obj_t * pNet ) return pNet; } + + +/* + // allocate memory to remember the phase + pPolarity = NULL; + if ( fComplUsed ) + { + int nBytes = 4 * Abc_BitWordNum( Abc_NtkPiNum(pNtkBox) ); + pPolarity = (unsigned *)Extra_MmFlexEntryFetch( pNtk->pData, nBytes ); + memset( pPolarity, 0, nBytes ); + } + // create box to represent this gate + if ( Abc_NtkHasBlackbox(pNtkBox) ) + pNode = Abc_NtkCreateBlackbox( pNtk ); + else + pNode = Abc_NtkCreateWhitebox( pNtk ); + pNode->pNext = (Abc_Obj_t *)pPolarity; + pNode->pData = pNtkBox; + // connect to fanin nets + Abc_NtkForEachPi( pNtkBox, pObj, i ) + { + if ( pPolarity && Abc_ObjIsComplement(pObj->pCopy) ) + { + Abc_InfoSetBit( pPolarity, i ); + pObj->pCopy = Abc_ObjRegular( pObj->pCopy ); + } + assert( !Abc_ObjIsComplement(pObj->pCopy) ); +// Abc_ObjAddFanin( pNode, pObj->pCopy ); + pTerm = Abc_NtkCreateBi( pNtk ); + Abc_ObjAddFanin( pTerm, pObj->pCopy ); + Abc_ObjAddFanin( pNode, pTerm ); + } + // connect to fanout nets + Abc_NtkForEachPo( pNtkBox, pObj, i ) + { + if ( pObj->pCopy == NULL ) + pObj->pCopy = Abc_NtkFindOrCreateNet(pNtk, NULL); +// Abc_ObjAddFanin( pObj->pCopy, pNode ); + pTerm = Abc_NtkCreateBo( pNtk ); + Abc_ObjAddFanin( pTerm, pNode ); + Abc_ObjAddFanin( pObj->pCopy, pTerm ); + } +*/ + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/ver/verFormula.c b/src/base/ver/verFormula.c index 16192f6a..253754ae 100644 --- a/src/base/ver/verFormula.c +++ b/src/base/ver/verFormula.c @@ -72,8 +72,8 @@ static int Ver_FormulaParserFindVar( char * pString, Vec_Ptr_t * vNames ***********************************************************************/ void * Ver_FormulaParser( char * pFormula, void * pMan, Vec_Ptr_t * vNames, Vec_Ptr_t * vStackFn, Vec_Int_t * vStackOp, char * pErrorMessage ) { - Hop_Obj_t * bFunc, * bTemp; char * pTemp; + Hop_Obj_t * bFunc, * bTemp; int nParans, Flag; int Oper, Oper1, Oper2; int v; diff --git a/src/base/ver/verParse.c b/src/base/ver/verParse.c index f3afaca0..9462fc8b 100644 --- a/src/base/ver/verParse.c +++ b/src/base/ver/verParse.c @@ -100,7 +100,7 @@ char * Ver_ParseGetName( Ver_Man_t * pMan ) { pMan->fNameLast = 1; Ver_StreamPopChar( p ); - pWord = Ver_StreamGetWord( p, " " ); + pWord = Ver_StreamGetWord( p, " \r\n" ); } else pWord = Ver_StreamGetWord( p, " \t\n\r(),;" ); -- cgit v1.2.3