diff options
Diffstat (limited to 'src/temp/ver')
-rw-r--r-- | src/temp/ver/ver.h | 8 | ||||
-rw-r--r-- | src/temp/ver/verCore.c | 168 | ||||
-rw-r--r-- | src/temp/ver/verFormula.c | 69 |
3 files changed, 118 insertions, 127 deletions
diff --git a/src/temp/ver/ver.h b/src/temp/ver/ver.h index ea1613c0..3e351840 100644 --- a/src/temp/ver/ver.h +++ b/src/temp/ver/ver.h @@ -51,8 +51,8 @@ struct Ver_Man_t_ 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 + Abc_Lib_t * pDesign; // the current design + Abc_Lib_t * pGateLib; // the current technology library // error recovery FILE * Output; int fTopLevel; @@ -77,10 +77,10 @@ struct Ver_Man_t_ //////////////////////////////////////////////////////////////////////// /*=== verCore.c ========================================================*/ -extern st_table * Ver_ParseFile( char * pFileName, st_table * pGateLib, int fCheck ); +extern Abc_Lib_t * Ver_ParseFile( char * pFileName, Abc_Lib_t * 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 ); +extern void * Ver_FormulaParser( char * pFormula, void * pMan, 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 ); diff --git a/src/temp/ver/verCore.c b/src/temp/ver/verCore.c index 8ef38aad..e868c4e3 100644 --- a/src/temp/ver/verCore.c +++ b/src/temp/ver/verCore.c @@ -34,6 +34,8 @@ typedef enum { VER_SIG_WIRE } Ver_SignalType_t; +static Ver_Man_t * Ver_ParseStart( char * pFileName, Abc_Lib_t * pGateLib ); +static void Ver_ParseStop( Ver_Man_t * p ); static void Ver_ParseFreeData( Ver_Man_t * p ); static void Ver_ParseInternal( Ver_Man_t * p, int fCheck ); static int Ver_ParseModule( Ver_Man_t * p ); @@ -45,7 +47,6 @@ 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 ); //////////////////////////////////////////////////////////////////////// @@ -63,39 +64,25 @@ static Abc_Obj_t * Ver_ParseCreateLatch( Abc_Ntk_t * pNtk, char * pNetLI, char * SeeAlso [] ***********************************************************************/ -st_table * Ver_ParseFile( char * pFileName, st_table * pGateLib, int fCheck ) +Abc_Lib_t * Ver_ParseFile( char * pFileName, Abc_Lib_t * 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 ); + Abc_Lib_t * pDesign; + // start the parser + p = Ver_ParseStart( pFileName, pGateLib ); // parse the file Ver_ParseInternal( p, fCheck ); + // save the result + pDesign = p->pDesign; + p->pDesign = NULL; // 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; + Ver_ParseStop( p ); + return pDesign; } /**Function************************************************************* - Synopsis [File parser.] + Synopsis [Start parser.] Description [] @@ -104,19 +91,26 @@ st_table * Ver_ParseFile( char * pFileName, st_table * pGateLib, int fCheck ) SeeAlso [] ***********************************************************************/ -void Ver_ParseFreeLibrary( st_table * pLibVer ) +Ver_Man_t * Ver_ParseStart( char * pFileName, Abc_Lib_t * pGateLib ) { - 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 ); + Ver_Man_t * p; + p = ALLOC( Ver_Man_t, 1 ); + memset( p, 0, sizeof(Ver_Man_t) ); + p->pFileName = pFileName; + p->pReader = Ver_StreamAlloc( pFileName ); + p->pDesign = Abc_LibCreate( pFileName ); + 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 ); + return p; } /**Function************************************************************* - Synopsis [File parser.] + Synopsis [Stop parser.] Description [] @@ -125,18 +119,15 @@ void Ver_ParseFreeLibrary( st_table * pLibVer ) SeeAlso [] ***********************************************************************/ -void Ver_ParseFreeData( Ver_Man_t * p ) +void Ver_ParseStop( Ver_Man_t * p ) { - if ( p->pNtkCur ) - { - Abc_NtkDelete( p->pNtkCur ); - p->pNtkCur = NULL; - } - if ( p->pLibrary ) - { - Ver_ParseFreeLibrary( p->pLibrary ); - p->pLibrary = NULL; - } + assert( p->pNtkCur == NULL ); + Ver_StreamFree( p->pReader ); + Extra_ProgressBarStop( p->pProgress ); + Vec_PtrFree( p->vNames ); + Vec_PtrFree( p->vStackFn ); + Vec_IntFree( p->vStackOp ); + free( p ); } /**Function************************************************************* @@ -165,9 +156,11 @@ void Ver_ParseInternal( Ver_Man_t * pMan, int fCheck ) Ver_ParsePrintErrorMessage( pMan ); return; } + // parse the module if ( !Ver_ParseModule( pMan ) ) return; + // check the network for correctness if ( fCheck && !Abc_NtkCheckRead( pMan->pNtkCur ) ) { @@ -177,20 +170,45 @@ void Ver_ParseInternal( Ver_Man_t * pMan, int fCheck ) return; } // add the module to the hash table - if ( st_is_member( pMan->pLibrary, pMan->pNtkCur->pName ) ) + if ( st_is_member( pMan->pDesign->tModules, 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 ); + st_insert( pMan->pDesign->tModules, pMan->pNtkCur->pName, (char *)pMan->pNtkCur ); pMan->pNtkCur = NULL; } } /**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->pDesign ) + { + Abc_LibFree( p->pDesign ); + p->pDesign = NULL; + } +} + +/**Function************************************************************* + Synopsis [Prints the error message including the file name and line number.] Description [] @@ -229,26 +247,29 @@ int Ver_ParseModule( Ver_Man_t * pMan ) { Ver_Stream_t * p = pMan->pReader; Abc_Ntk_t * pNtk, * pNtkTemp; - char * pWord; + Abc_Obj_t * pNet; + char * pWord, Symbol; 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 ); + + pNtk->ntkFunc = ABC_FUNC_AIG; + assert( pNtk->pManFunc == NULL ); + pNtk->pManFunc = pMan->pDesign->pManFunc; // get the network name pWord = Ver_ParseGetName( pMan ); pNtk->pName = Extra_UtilStrsav( pWord ); - pNtk->pSpec = Extra_UtilStrsav( pMan->pFileName ); - + pNtk->pSpec = NULL; +/* // 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 ); - + pNet = Abc_NtkFindOrCreateNet( pNtk, "1'b0" ); + Abc_ObjAddFanin( pNet, xxxx AigAbc_AigConst1(pNtk) ); + pNet = Abc_NtkFindOrCreateNet( pNtk, "1'b1" ); + Abc_ObjAddFanin( pNet, Abc_AigConst1(pNtk) ); +*/ // make sure we stopped at the opening paranthesis if ( Ver_StreamScanChar(p) != '(' ) { @@ -313,9 +334,9 @@ int Ver_ParseModule( Ver_Man_t * pMan ) Abc_NtkFinalizeRead( pNtk ); break; } - else if ( pMan->pGateLib && st_lookup(pMan->pGateLib, pWord, (char**)&pNtkTemp) ) // gate library + else if ( pMan->pGateLib && st_lookup(pMan->pGateLib->tModules, pWord, (char**)&pNtkTemp) ) // gate library RetValue = Ver_ParseGate( pMan, pNtkTemp ); - else if ( pMan->pLibrary && st_lookup(pMan->pLibrary, pWord, (char**)&pNtkTemp) ) // current design + else if ( pMan->pDesign && st_lookup(pMan->pDesign->tModules, pWord, (char**)&pNtkTemp) ) // current design RetValue = Ver_ParseGate( pMan, pNtkTemp ); else { @@ -334,17 +355,6 @@ int Ver_ParseModule( Ver_Man_t * 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; } @@ -882,26 +892,6 @@ Abc_Obj_t * Ver_ParseCreatePo( Abc_Ntk_t * pNtk, char * pName ) /**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).] diff --git a/src/temp/ver/verFormula.c b/src/temp/ver/verFormula.c index 7edb5bd9..cfeb3e5f 100644 --- a/src/temp/ver/verFormula.c +++ b/src/temp/ver/verFormula.c @@ -38,23 +38,22 @@ #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_NEG 7 // negation (highest precedence) +#define VER_PARSE_OPER_AND 6 // logic AND +#define VER_PARSE_OPER_XOR 5 // logic EXOR (a'b | ab') +#define VER_PARSE_OPER_OR 4 // logic OR +#define VER_PARSE_OPER_EQU 3 // equvalence (a'b'| ab ) +#define VER_PARSE_OPER_MUX 2 // MUX(a,b,c) (ab | a'c ) #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 +#define VER_PARSE_FLAG_ERROR 4 // 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 ); +static Aig_Obj_t * Ver_FormulaParserTopOper( Aig_Man_t * pMan, Vec_Ptr_t * vStackFn, int Oper ); +static int Ver_FormulaParserFindVar( char * pString, Vec_Ptr_t * vNames ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -71,9 +70,9 @@ static int Ver_FormulaParserFindVar( char * pString, Vec_Ptr_t * vNames ); SeeAlso [] ***********************************************************************/ -DdNode * Ver_FormulaParser( char * pFormula, DdManager * dd, Vec_Ptr_t * vNames, Vec_Ptr_t * vStackFn, Vec_Int_t * vStackOp, char * pErrorMessage ) +void * Ver_FormulaParser( char * pFormula, void * pMan, Vec_Ptr_t * vNames, Vec_Ptr_t * vStackFn, Vec_Int_t * vStackOp, char * pErrorMessage ) { - DdNode * bFunc, * bTemp; + Aig_Obj_t * bFunc, * bTemp; char * pTemp; int nParans, Flag; int Oper, Oper1, Oper2; @@ -120,7 +119,7 @@ DdNode * Ver_FormulaParser( char * pFormula, DdManager * dd, Vec_Ptr_t * vNames, // treat Constant 0 as a variable case VER_PARSE_SYM_CONST0: - Vec_PtrPush( vStackFn, b0 ); Cudd_Ref( b0 ); + Vec_PtrPush( vStackFn, Aig_ManConst0(pMan) ); // Cudd_Ref( Aig_ManConst0(pMan) ); if ( Flag == VER_PARSE_FLAG_VAR ) { sprintf( pErrorMessage, "Parse_FormulaParser(): No operation symbol before constant 0." ); @@ -132,7 +131,7 @@ DdNode * Ver_FormulaParser( char * pFormula, DdManager * dd, Vec_Ptr_t * vNames, // the same for Constant 1 case VER_PARSE_SYM_CONST1: - Vec_PtrPush( vStackFn, b1 ); Cudd_Ref( b1 ); + Vec_PtrPush( vStackFn, Aig_ManConst1(pMan) ); // Cudd_Ref( Aig_ManConst1(pMan) ); if ( Flag == VER_PARSE_FLAG_VAR ) { sprintf( pErrorMessage, "Parse_FormulaParser(): No operation symbol before constant 1." ); @@ -211,7 +210,7 @@ DdNode * Ver_FormulaParser( char * pFormula, DdManager * dd, Vec_Ptr_t * vNames, // } // perform the given operation - if ( Ver_FormulaParserTopOper( dd, vStackFn, Oper ) == NULL ) + if ( Ver_FormulaParserTopOper( pMan, vStackFn, Oper ) == NULL ) { sprintf( pErrorMessage, "Parse_FormulaParser(): Unknown operation\n" ); return NULL; @@ -240,8 +239,8 @@ DdNode * Ver_FormulaParser( char * pFormula, DdManager * dd, Vec_Ptr_t * vNames, sprintf( pErrorMessage, "Parse_FormulaParser(): Incorrect state." ); return NULL; } - bTemp = Cudd_bddIthVar(dd, v); - Vec_PtrPush( vStackFn, bTemp ); Cudd_Ref( bTemp ); + bTemp = Aig_IthVar( pMan, v ); + Vec_PtrPush( vStackFn, bTemp ); // Cudd_Ref( bTemp ); Flag = VER_PARSE_FLAG_VAR; break; } @@ -263,7 +262,8 @@ DdNode * Ver_FormulaParser( char * pFormula, DdManager * dd, Vec_Ptr_t * vNames, } else { - Vec_PtrPush( vStackFn, Cudd_Not(Vec_PtrPop(vStackFn)) ); +// Vec_PtrPush( vStackFn, Cudd_Not(Vec_PtrPop(vStackFn)) ); + Vec_PtrPush( vStackFn, Aig_Not(Vec_PtrPop(vStackFn)) ); } } else // if ( Flag == VER_PARSE_FLAG_OPER ) @@ -279,7 +279,7 @@ DdNode * Ver_FormulaParser( char * pFormula, DdManager * dd, Vec_Ptr_t * vNames, 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 ) + if ( Ver_FormulaParserTopOper( pMan, vStackFn, Oper2 ) == NULL ) { sprintf( pErrorMessage, "Parse_FormulaParser(): Unknown operation\n" ); return NULL; @@ -303,7 +303,7 @@ DdNode * Ver_FormulaParser( char * pFormula, DdManager * dd, Vec_Ptr_t * vNames, if ( !Vec_PtrSize(vStackFn) ) if ( !Vec_IntSize(vStackOp) ) { - Cudd_Deref( bFunc ); +// Cudd_Deref( bFunc ); return bFunc; } else @@ -314,8 +314,8 @@ DdNode * Ver_FormulaParser( char * pFormula, DdManager * dd, Vec_Ptr_t * vNames, else sprintf( pErrorMessage, "Parse_FormulaParser(): The input string is empty\n" ); } - Cudd_Ref( bFunc ); - Cudd_RecursiveDeref( dd, bFunc ); +// Cudd_Ref( bFunc ); +// Cudd_RecursiveDeref( dd, bFunc ); return NULL; } @@ -330,32 +330,33 @@ DdNode * Ver_FormulaParser( char * pFormula, DdManager * dd, Vec_Ptr_t * vNames, SeeAlso [] ***********************************************************************/ -DdNode * Ver_FormulaParserTopOper( DdManager * dd, Vec_Ptr_t * vStackFn, int Oper ) +Aig_Obj_t * Ver_FormulaParserTopOper( Aig_Man_t * pMan, Vec_Ptr_t * vStackFn, int Oper ) { - DdNode * bArg0, * bArg1, * bArg2, * bFunc; + Aig_Obj_t * 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 ); + bFunc = Aig_And( pMan, bArg1, bArg2 ); else if ( Oper == VER_PARSE_OPER_XOR ) - bFunc = Cudd_bddXor( dd, bArg1, bArg2 ); + bFunc = Aig_Exor( pMan, bArg1, bArg2 ); else if ( Oper == VER_PARSE_OPER_OR ) - bFunc = Cudd_bddOr( dd, bArg1, bArg2 ); + bFunc = Aig_Or( pMan, bArg1, bArg2 ); else if ( Oper == VER_PARSE_OPER_EQU ) - bFunc = Cudd_bddXnor( dd, bArg1, bArg2 ); + bFunc = Aig_Not( Aig_Exor( pMan, 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 ); +// bFunc = Cudd_bddIte( dd, bArg0, bArg1, bArg2 ); Cudd_Ref( bFunc ); + bFunc = Aig_Mux( pMan, bArg0, bArg1, bArg2 ); +// Cudd_RecursiveDeref( dd, bArg0 ); +// Cudd_Deref( bFunc ); } else return NULL; - Cudd_Ref( bFunc ); - Cudd_RecursiveDeref( dd, bArg1 ); - Cudd_RecursiveDeref( dd, bArg2 ); +// Cudd_Ref( bFunc ); +// Cudd_RecursiveDeref( dd, bArg1 ); +// Cudd_RecursiveDeref( dd, bArg2 ); Vec_PtrPush( vStackFn, bFunc ); return bFunc; } |