Version abc60825

6 files changed, 142 insertions, 16 deletions

diff --git a/src/temp/aig/aig.h b/src/temp/aig/aig.h
index e489d978..5166d0c3 100644
--- a/src/temp/aig/aig.h
+++ b/src/temp/aig/aig.h
@@ -137,7 +137,7 @@ static inline int          Aig_ManObjNum( Aig_Man_t * p )         { return p->nC
 
 static inline Aig_Type_t   Aig_ObjType( Aig_Obj_t * pObj )        { return pObj->Type;               }
 static inline int          Aig_ObjIsNone( Aig_Obj_t * pObj )      { return pObj->Type == AIG_NONE;   }
-static inline int          Aig_ObjIsConst1( Aig_Obj_t * pObj )    { return pObj->Type == AIG_CONST1; }
+static inline int          Aig_ObjIsConst1( Aig_Obj_t * pObj )    { assert(!Aig_IsComplement(pObj)); return pObj->Type == AIG_CONST1; }
 static inline int          Aig_ObjIsPi( Aig_Obj_t * pObj )        { return pObj->Type == AIG_PI;     }
 static inline int          Aig_ObjIsPo( Aig_Obj_t * pObj )        { return pObj->Type == AIG_PO;     }
 static inline int          Aig_ObjIsAnd( Aig_Obj_t * pObj )       { return pObj->Type == AIG_AND;    }
diff --git a/src/temp/aig/aigDfs.c b/src/temp/aig/aigDfs.c
index e289f6ec..2fe8b2ef 100644
--- a/src/temp/aig/aigDfs.c
+++ b/src/temp/aig/aigDfs.c
@@ -325,9 +325,12 @@ Aig_Obj_t * Aig_Transfer( Aig_Man_t * pSour, Aig_Man_t * pDest, Aig_Obj_t * pRoo
     if ( Aig_ObjIsConst1( Aig_Regular(pRoot) ) )
         return Aig_NotCond( Aig_ManConst1(pDest), Aig_IsComplement(pRoot) );
     // set the PI mapping
-    Aig_ManForEachPi( pDest, pObj, i )
-        if ( i < nVars )
-            Aig_IthVar(pSour, i)->pData = Aig_IthVar(pDest, i);
+    Aig_ManForEachPi( pSour, pObj, i )
+    {
+        if ( i == nVars )
+           break;
+        pObj->pData = Aig_IthVar(pDest, i);
+    }
     // transfer and set markings
     Aig_Transfer_rec( pDest, Aig_Regular(pRoot) );
     // clear the markings
diff --git a/src/temp/aig/aigMan.c b/src/temp/aig/aigMan.c
index af6df62d..bb39712f 100644
--- a/src/temp/aig/aigMan.c
+++ b/src/temp/aig/aigMan.c
@@ -56,6 +56,7 @@ Aig_Man_t * Aig_ManStart()
     Aig_ManStartMemory( p );
     // create the constant node
     p->pConst1 = Aig_ManFetchMemory( p );
+    p->pConst1->Type = AIG_CONST1;
     p->pConst1->fPhase = 1;
     p->nCreated = 1;
     // start the table
diff --git a/src/temp/aig/aigOper.c b/src/temp/aig/aigOper.c
index cad240ae..9985093e 100644
--- a/src/temp/aig/aigOper.c
+++ b/src/temp/aig/aigOper.c
@@ -183,6 +183,7 @@ Aig_Obj_t * Aig_Or( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1 )
 ***********************************************************************/
 Aig_Obj_t * Aig_Mux( Aig_Man_t * p, Aig_Obj_t * pC, Aig_Obj_t * p1, Aig_Obj_t * p0 )
 {
+/*    
     Aig_Obj_t * pTempA1, * pTempA2, * pTempB1, * pTempB2, * pTemp;
     int Count0, Count1;
     // consider trivial cases
@@ -190,6 +191,9 @@ Aig_Obj_t * Aig_Mux( Aig_Man_t * p, Aig_Obj_t * pC, Aig_Obj_t * p1, Aig_Obj_t *
         return Aig_Exor( p, pC, p0 );
     // other cases can be added
     // implement the first MUX (F = C * x1 + C' * x0)
+
+    // check for constants here!!!
+
     pTempA1 = Aig_TableLookup( p, Aig_ObjCreateGhost(p, pC,          p1, AIG_AND) );
     pTempA2 = Aig_TableLookup( p, Aig_ObjCreateGhost(p, Aig_Not(pC), p0, AIG_AND) );
     if ( pTempA1 && pTempA2 )
@@ -217,8 +221,8 @@ Aig_Obj_t * Aig_Mux( Aig_Man_t * p, Aig_Obj_t * pC, Aig_Obj_t * p1, Aig_Obj_t *
     pTempB1 = pTempB1? pTempB1 : Aig_And(p, pC,          Aig_Not(p1));
     pTempB2 = pTempB2? pTempB2 : Aig_And(p, Aig_Not(pC), Aig_Not(p0));
     return Aig_Not( Aig_Or( p, pTempB1, pTempB2 ) );
-
-//    return Aig_Or( Aig_And(pC, p1), Aig_And(Aig_Not(pC), p0) );
+*/
+    return Aig_Or( p, Aig_And(p, pC, p1), Aig_And(p, Aig_Not(pC), p0) );
 }
 
 /**Function*************************************************************
diff --git a/src/temp/ver/verCore.c b/src/temp/ver/verCore.c
index 303fe7d1..6c8192f5 100644
--- a/src/temp/ver/verCore.c
+++ b/src/temp/ver/verCore.c
@@ -34,6 +34,18 @@ typedef enum {
     VER_SIG_WIRE
 } Ver_SignalType_t;
 
+// types of verilog gates
+typedef enum { 
+    VER_GATE_AND = 0,
+    VER_GATE_OR,
+    VER_GATE_XOR,
+    VER_GATE_BUF,
+    VER_GATE_NAND,
+    VER_GATE_NOR,
+    VER_GATE_XNOR,
+    VER_GATE_NOT
+} Ver_GateType_t;
+
 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 );
@@ -44,6 +56,7 @@ 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 Abc_Obj_t * Ver_ParseCreatePi( Abc_Ntk_t * pNtk, char * pName );
 static Abc_Obj_t * Ver_ParseCreatePo( Abc_Ntk_t * pNtk, char * pName );
@@ -201,6 +214,7 @@ void Ver_ParseFreeData( Ver_Man_t * p )
 {
     if ( p->pNtkCur )
     {
+        p->pNtkCur->pManFunc = NULL;
         Abc_NtkDelete( p->pNtkCur );
         p->pNtkCur = NULL;
     }
@@ -324,7 +338,25 @@ int Ver_ParseModule( Ver_Man_t * pMan )
     while ( 1 )
     {
         Extra_ProgressBarUpdate( pMan->pProgress, Ver_StreamGetCurPosition(p), NULL );
-        if ( !strcmp( pWord, "assign" ) )
+
+        if ( !strcmp( pWord, "and" ) )
+            RetValue = Ver_ParseGateStandard( pMan, VER_GATE_AND );
+        else if ( !strcmp( pWord, "or" ) )
+            RetValue = Ver_ParseGateStandard( pMan, VER_GATE_OR );
+        else if ( !strcmp( pWord, "xor" ) )
+            RetValue = Ver_ParseGateStandard( pMan, VER_GATE_XOR );
+        else if ( !strcmp( pWord, "buf" ) )
+            RetValue = Ver_ParseGateStandard( pMan, VER_GATE_BUF );
+        else if ( !strcmp( pWord, "nand" ) )
+            RetValue = Ver_ParseGateStandard( pMan, VER_GATE_NAND );
+        else if ( !strcmp( pWord, "nor" ) )
+            RetValue = Ver_ParseGateStandard( pMan, VER_GATE_NOR );
+        else if ( !strcmp( pWord, "xnor" ) )
+            RetValue = Ver_ParseGateStandard( pMan, VER_GATE_XNOR );
+        else if ( !strcmp( pWord, "not" ) )
+            RetValue = Ver_ParseGateStandard( pMan, VER_GATE_NOT );
+
+        else if ( !strcmp( pWord, "assign" ) )
             RetValue = Ver_ParseAssign( pMan );
         else if ( !strcmp( pWord, "always" ) )
             RetValue = Ver_ParseAlways( pMan );
@@ -348,6 +380,9 @@ int Ver_ParseModule( Ver_Man_t * pMan )
         }
         if ( RetValue == 0 )
             return 0;
+        // skip the comments
+        if ( !Ver_ParseSkipComments( pMan ) )
+            return 0;
         // get new word
         pWord = Ver_ParseGetName( pMan );
         if ( pWord == NULL )
@@ -469,14 +504,6 @@ int Ver_ParseAssign( Ver_Man_t * pMan )
             Ver_ParsePrintErrorMessage( pMan );
             return 0;
         }
-        // get the fanout net
-        pNet = Abc_NtkFindNet( pNtk, pWord );
-        if ( pNet == NULL )
-        {
-            sprintf( pMan->sError, "Cannot read the assign statement for %s (output wire is not defined).", pWord );
-            Ver_ParsePrintErrorMessage( pMan );
-            return 0;
-        }
         // get the equal sign
         if ( Ver_StreamPopChar(p) != '=' )
         {
@@ -893,6 +920,97 @@ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtkGate )
 
 /**Function*************************************************************
 
+  Synopsis    [Parses one directive.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ver_ParseGateStandard( Ver_Man_t * pMan, Ver_GateType_t GateType )
+{
+    Ver_Stream_t * p = pMan->pReader;
+    Aig_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) != '(' )
+    {
+        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( pMan->pNtkCur );
+    // 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 = Abc_NtkFindNet( pMan->pNtkCur, pWord );
+        if ( pNet == NULL )
+        {
+            sprintf( pMan->sError, "Net is missing in gate %s.", pWord );
+            Ver_ParsePrintErrorMessage( pMan );
+            return 0;
+        }
+        // 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 = Aig_CreateAnd( pAig, Abc_ObjFaninNum(pNode) );
+    else if ( GateType == VER_GATE_OR || GateType == VER_GATE_NOR )
+        pNode->pData = Aig_CreateOr( pAig, Abc_ObjFaninNum(pNode) );
+    else if ( GateType == VER_GATE_XOR || GateType == VER_GATE_XNOR )
+        pNode->pData = Aig_CreateExor( pAig, Abc_ObjFaninNum(pNode) );
+    else if ( GateType == VER_GATE_BUF || GateType == VER_GATE_NOT )
+        pNode->pData = Aig_CreateAnd( pAig, Abc_ObjFaninNum(pNode) );
+    if ( GateType == VER_GATE_NAND || GateType == VER_GATE_NOR || GateType == VER_GATE_XNOR || GateType == VER_GATE_NOT )
+        pNode->pData = Aig_Not( pNode->pData );
+    return 1;
+}
+
+
+/**Function*************************************************************
+
   Synopsis    [Creates PI terminal and net.]
 
   Description []
diff --git a/src/temp/ver/verFormula.c b/src/temp/ver/verFormula.c
index 2c2881c0..8bb21547 100644
--- a/src/temp/ver/verFormula.c
+++ b/src/temp/ver/verFormula.c
@@ -392,7 +392,7 @@ int Ver_FormulaParserFindVar( char * pString, Vec_Ptr_t * vNames )
         if ( nLength2 != nLength )
             continue;
         pTemp2   = Vec_PtrEntry( vNames, 2*i + 1 );
-        if ( strncmp( pTemp, pTemp2, nLength ) )
+        if ( strncmp( pString, pTemp2, nLength ) )
             continue;
         return i;
     }