summaryrefslogtreecommitdiffstats
path: root/src/temp/ver
diff options
context:
space:
mode:
Diffstat (limited to 'src/temp/ver')
-rw-r--r--src/temp/ver/ver.h8
-rw-r--r--src/temp/ver/verCore.c168
-rw-r--r--src/temp/ver/verFormula.c69
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;
}