Version abc90215

12 files changed, 1001 insertions, 53 deletions

diff --git a/src/map/amap/amap.h b/src/map/amap/amap.h
index ee845e7f..284af309 100644
--- a/src/map/amap/amap.h
+++ b/src/map/amap/amap.h
@@ -21,10 +21,6 @@
 #ifndef __AMAP_H__
 #define __AMAP_H__
 
-#ifdef __cplusplus
-extern "C" {
-#endif
-
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -33,6 +29,10 @@ extern "C" {
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                         BASIC TYPES                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -45,7 +45,7 @@ struct Amap_Par_t_
     int    nIterArea;   // iteratoins of exact area
     int    fUseMuxes;   // enables the use of MUXes
     int    fUseXors;    // enables the use of XORs
-    int    fFreeInvs;   // assume inverters are free (area = 0)
+    int    fFreeInvs;   // assume inverters are ABC_FREE (area = 0)
     float  fEpsilon;    // used to compare floating point numbers
     int    fVerbose;    // verbosity flag
 };
@@ -69,7 +69,10 @@ struct Amap_Out_t_
 
 /*=== amapCore.c ==========================================================*/
 extern void        Amap_ManSetDefaultParams( Amap_Par_t * pPars );
-extern Vec_Ptr_t * Amap_ManTest( Aig_Man_t * pAig, Amap_Par_t * pPars );
+//extern Vec_Ptr_t * Amap_ManTest( Aig_Man_t * pAig, Amap_Par_t * pPars );
+/*=== amapLiberty.c ==========================================================*/
+extern int         Amap_LibertyParse( char * pFileName, char * pFileGenlib, int fVerbose );
+
 
 #ifdef __cplusplus
 }
diff --git a/src/map/amap/amapCore.c b/src/map/amap/amapCore.c
index f1554862..7dedc067 100644
--- a/src/map/amap/amapCore.c
+++ b/src/map/amap/amapCore.c
@@ -46,7 +46,7 @@ void Amap_ManSetDefaultParams( Amap_Par_t * p )
     p->nIterArea = 4;            // iteratoins of exact area
     p->fUseMuxes = 0;            // enables the use of MUXes
     p->fUseXors  = 1;            // enables the use of XORs
-    p->fFreeInvs = 0;            // assume inverters are free (area = 0)
+    p->fFreeInvs = 0;            // assume inverters are ABC_FREE (area = 0)
     p->fEpsilon  = (float)0.001; // used to compare floating point numbers
     p->fVerbose  = 0;            // verbosity flag
 }
@@ -81,8 +81,8 @@ Vec_Ptr_t * Amap_ManTest( Aig_Man_t * pAig, Amap_Par_t * pPars )
     p->fAreaInv = pPars->fFreeInvs? 0.0 : pLib->pGateInv->dArea;
     p->fUseMux = pPars->fUseMuxes && pLib->fHasMux;
     p->fUseXor = pPars->fUseXors && pLib->fHasXor;
-    p->ppCutsTemp = CALLOC( Amap_Cut_t *, 2 * pLib->nNodes );
-    p->pMatsTemp = CALLOC( int, 2 * pLib->nNodes );
+    p->ppCutsTemp = ABC_CALLOC( Amap_Cut_t *, 2 * pLib->nNodes );
+    p->pMatsTemp = ABC_CALLOC( int, 2 * pLib->nNodes );
     Amap_ManCreate( p, pAig );
     Amap_ManMap( p );
     vRes = NULL;
@@ -90,7 +90,7 @@ Vec_Ptr_t * Amap_ManTest( Aig_Man_t * pAig, Amap_Par_t * pPars )
     Amap_ManStop( p );
 if ( pPars->fVerbose )
 {
-PRT( "Total runtime", clock() - clkTotal );
+ABC_PRT( "Total runtime", clock() - clkTotal );
 }
     return vRes;
 }
diff --git a/src/map/amap/amapInt.h b/src/map/amap/amapInt.h
index 954790c9..dec7e799 100644
--- a/src/map/amap/amapInt.h
+++ b/src/map/amap/amapInt.h
@@ -21,10 +21,6 @@
 #ifndef __AMAP_INT_H__
 #define __AMAP_INT_H__
 
-#ifdef __cplusplus
-extern "C" {
-#endif
-
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -36,6 +32,10 @@ extern "C" {
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 // the largest gate size in the library
 // (gates above this size will be ignored)
 #define AMAP_MAXINS 15
@@ -222,10 +222,10 @@ static inline int          Amap_LitNot( int Lit )               { return Lit ^ 1
 static inline int          Amap_LitNotCond( int Lit, int c )    { return Lit ^ (int)(c > 0); }
 static inline int          Amap_LitRegular( int Lit )           { return Lit & ~01;          }
 
-static inline Amap_Obj_t * Amap_Regular( Amap_Obj_t * p )                          { return (Amap_Obj_t *)((PORT_PTRUINT_T)(p) & ~01);  }
-static inline Amap_Obj_t * Amap_Not( Amap_Obj_t * p )                              { return (Amap_Obj_t *)((PORT_PTRUINT_T)(p) ^  01);  }
-static inline Amap_Obj_t * Amap_NotCond( Amap_Obj_t * p, int c )                   { return (Amap_Obj_t *)((PORT_PTRUINT_T)(p) ^ (c));  }
-static inline int          Amap_IsComplement( Amap_Obj_t * p )                     { return (int )(((PORT_PTRUINT_T)p) & 01);           }
+static inline Amap_Obj_t * Amap_Regular( Amap_Obj_t * p )                          { return (Amap_Obj_t *)((ABC_PTRUINT_T)(p) & ~01);  }
+static inline Amap_Obj_t * Amap_Not( Amap_Obj_t * p )                              { return (Amap_Obj_t *)((ABC_PTRUINT_T)(p) ^  01);  }
+static inline Amap_Obj_t * Amap_NotCond( Amap_Obj_t * p, int c )                   { return (Amap_Obj_t *)((ABC_PTRUINT_T)(p) ^ (c));  }
+static inline int          Amap_IsComplement( Amap_Obj_t * p )                     { return (int )(((ABC_PTRUINT_T)p) & 01);           }
 
 static inline int          Amap_ManPiNum( Amap_Man_t * p )                         { return p->nObjs[AMAP_OBJ_PI];                      }
 static inline int          Amap_ManPoNum( Amap_Man_t * p )                         { return p->nObjs[AMAP_OBJ_PO];                      }
diff --git a/src/map/amap/amapLib.c b/src/map/amap/amapLib.c
index 816f0703..f2e5113f 100644
--- a/src/map/amap/amapLib.c
+++ b/src/map/amap/amapLib.c
@@ -42,7 +42,7 @@
 Amap_Lib_t * Amap_LibAlloc()
 {
     Amap_Lib_t * p;
-    p = (Amap_Lib_t *)ALLOC( Amap_Lib_t, 1 );
+    p = (Amap_Lib_t *)ABC_ALLOC( Amap_Lib_t, 1 );
     memset( p, 0, sizeof(Amap_Lib_t) );
     p->vGates = Vec_PtrAlloc( 100 );
     p->pMemGates = Aig_MmFlexStart();
@@ -79,10 +79,10 @@ void Amap_LibFree( Amap_Lib_t * p )
         Vec_IntFree( p->vRules3 );
     Aig_MmFlexStop( p->pMemGates, 0 );
     Aig_MmFlexStop( p->pMemSet, 0 );
-    FREE( p->pRules );
-    FREE( p->pRulesX );
-    FREE( p->pNodes );
-    free( p );
+    ABC_FREE( p->pRules );
+    ABC_FREE( p->pRulesX );
+    ABC_FREE( p->pNodes );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
@@ -341,7 +341,7 @@ Amap_Lib_t * Amap_LibReadAndPrepare( char * pFileName, int fVerbose, int fVeryVe
     {
         printf( "Selected %d functionally unique gates. ",
             Vec_PtrSize(p->vSelect), Vec_PtrSize(p->vSorted) );
-        PRT( "Time", clock() - clk );
+        ABC_PRT( "Time", clock() - clk );
     }
     clk = clock();
     Amap_LibCreateRules( p, fVeryVerbose );
@@ -349,7 +349,7 @@ Amap_Lib_t * Amap_LibReadAndPrepare( char * pFileName, int fVerbose, int fVeryVe
     {
         printf( "Created %d rules and %d matches. ", 
             p->nNodes, p->nSets );
-        PRT( "Time", clock() - clk );
+        ABC_PRT( "Time", clock() - clk );
     }
     return p;
 }
diff --git a/src/map/amap/amapLiberty.c b/src/map/amap/amapLiberty.c
new file mode 100644
index 00000000..7f46ffdf
--- /dev/null
+++ b/src/map/amap/amapLiberty.c
@@ -0,0 +1,911 @@
+/**CFile****************************************************************
+
+  FileHead    [amapLiberty.c]
+
+  SystemHead  [ABC: Logic synthesis and verification system.]
+
+  PackageHead [Technology mapper for standard cells.]
+
+  Synopsis    [Liberty parser.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: amapLiberty.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "amapInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+// entry types
+typedef enum { 
+    AMAP_LIBERTY_NONE = 0,        // 0:  unknown
+    AMAP_LIBERTY_PROC,            // 1:  procedure :  key(head){body}
+    AMAP_LIBERTY_EQUA,            // 2:  equation  :  key:head;
+    AMAP_LIBERTY_LIST             // 3:  list      :  key(head) 
+} Amap_LibertyType_t;
+
+typedef struct Amap_Pair_t_ Amap_Pair_t;
+struct Amap_Pair_t_
+{
+    int             Beg;          // item beginning
+    int             End;          // item end
+};
+
+typedef struct Amap_Item_t_ Amap_Item_t;
+struct Amap_Item_t_
+{
+    int             Type;         // Amap_LibertyType_t
+    int             iLine;        // file line where the item's spec begins
+    Amap_Pair_t     Key;          // key part
+    Amap_Pair_t     Head;         // head part 
+    Amap_Pair_t     Body;         // body part
+    int             Next;         // next item in the list 
+    int             Child;        // first child item 
+};
+
+typedef struct Amap_Tree_t_ Amap_Tree_t;
+struct Amap_Tree_t_
+{
+    char *          pFileName;    // input Liberty file name
+    char *          pContents;    // file contents
+    int             nContents;    // file size
+    int             nLines;       // line counter
+    int             nItems;       // number of items
+    int             nItermAlloc;  // number of items allocated
+    Amap_Item_t *   pItems;       // the items
+    char *          pError;       // the error string
+};
+
+static inline Amap_Item_t *  Amap_LibertyRoot( Amap_Tree_t * p )                                       { return p->pItems;                                                 }
+static inline Amap_Item_t *  Amap_LibertyItem( Amap_Tree_t * p, int v )                                { assert( v < p->nItems ); return v < 0 ? NULL : p->pItems + v;     }
+static inline int            Amap_LibertyCompare( Amap_Tree_t * p, Amap_Pair_t Pair, char * pStr )     { return strncmp( p->pContents+Pair.Beg, pStr, Pair.End-Pair.Beg ); }
+static inline void           Amap_PrintWord( FILE * pFile, Amap_Tree_t * p, Amap_Pair_t Pair )         { char * pBeg = p->pContents+Pair.Beg, * pEnd = p->pContents+Pair.End; while ( pBeg < pEnd ) fputc( *pBeg++, pFile ); }
+static inline void           Amap_PrintSpace( FILE * pFile, int nOffset )                              { int i; for ( i = 0; i < nOffset; i++ ) fputc(' ', pFile);         }
+static inline int            Amap_LibertyItemId( Amap_Tree_t * p, Amap_Item_t * pItem )                { return pItem - p->pItems;                                         }
+
+#define Amap_ItemForEachChild( p, pItem, pChild ) \
+    for ( pChild = Amap_LibertyItem(p, pItem->Child); pChild; pChild = Amap_LibertyItem(p, pChild->Next) )
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Prints parse tree in Liberty format.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Amap_LibertyPrintLibertyItem( FILE * pFile, Amap_Tree_t * p, Amap_Item_t * pItem, int nOffset )
+{
+    if ( pItem->Type == AMAP_LIBERTY_PROC )
+    {
+        Amap_PrintSpace( pFile, nOffset );
+        Amap_PrintWord( pFile, p, pItem->Key );
+        fprintf( pFile, "(" );
+        Amap_PrintWord( pFile, p, pItem->Head );
+        fprintf( pFile, ") {\n" );
+        if ( Amap_LibertyItem(p, pItem->Child) )
+            Amap_LibertyPrintLibertyItem( pFile, p, Amap_LibertyItem(p, pItem->Child), nOffset + 1 );
+        Amap_PrintSpace( pFile, nOffset );
+        fprintf( pFile, "}\n" );
+    }
+    else if ( pItem->Type == AMAP_LIBERTY_EQUA )
+    {
+        Amap_PrintSpace( pFile, nOffset );
+        Amap_PrintWord( pFile, p, pItem->Key );
+        fprintf( pFile, " : " );
+        Amap_PrintWord( pFile, p, pItem->Head );
+        fprintf( pFile, ";\n" );
+    }
+    else if ( pItem->Type == AMAP_LIBERTY_LIST )
+    {
+        Amap_PrintSpace( pFile, nOffset );
+        Amap_PrintWord( pFile, p, pItem->Key );
+        fprintf( pFile, "(" );
+        Amap_PrintWord( pFile, p, pItem->Head );
+        fprintf( pFile, ");\n" );
+    }
+    else assert( 0 );
+    if ( Amap_LibertyItem(p, pItem->Next) )
+        Amap_LibertyPrintLibertyItem( pFile, p, Amap_LibertyItem(p, pItem->Next), nOffset );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints parse tree in Liberty format.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Amap_LibertyPrintLiberty( Amap_Tree_t * p, char * pFileName )
+{
+    FILE * pFile;
+    if ( pFileName == NULL )
+        pFile = stdout;
+    else
+    {
+        pFile = fopen( pFileName, "w" );
+        if ( pFile == NULL )
+        {
+            printf( "Amap_LibertyPrintLiberty(): The output file is unavailable (absent or open).\n" );
+            return 0;
+        }
+    }
+    Amap_LibertyPrintLibertyItem( pFile, p, Amap_LibertyRoot(p), 0 );
+    if ( pFile != stdout )
+        fclose( pFile );
+    return 1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the time stamp.]
+
+  Description [The file should be closed.]
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Amap_LibertyTimeStamp()
+{
+    static char Buffer[100];
+    char * TimeStamp;
+    time_t ltime;
+    // get the current time
+    time( &ltime );
+    TimeStamp = asctime( localtime( &ltime ) );
+    TimeStamp[ strlen(TimeStamp) - 1 ] = 0;
+    strcpy( Buffer, TimeStamp );
+    return Buffer;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns cell's function.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Amap_LibertyCellIsFlop( Amap_Tree_t * p, Amap_Item_t * pCell )
+{
+    Amap_Item_t * pAttr;
+    Amap_ItemForEachChild( p, pCell, pAttr )
+        if ( !Amap_LibertyCompare(p, pAttr->Key, "ff") ||
+             !Amap_LibertyCompare(p, pAttr->Key, "latch") )
+            return 1;
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns pin's function.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Amap_Item_t * Amap_LibertyPinFunction( Amap_Tree_t * p, Amap_Item_t * pPin )
+{
+    Amap_Item_t * pFunc;
+    Amap_ItemForEachChild( p, pPin, pFunc )
+        if ( !Amap_LibertyCompare(p, pFunc->Key, "function") )
+            return pFunc;
+    return NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns cell's function.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Amap_Item_t * Amap_LibertyCellOutput( Amap_Tree_t * p, Amap_Item_t * pCell )
+{
+    Amap_Item_t * pPin;
+    Amap_ItemForEachChild( p, pCell, pPin )
+    {
+        if ( Amap_LibertyCompare(p, pPin->Key, "pin") )
+            continue;
+        if ( Amap_LibertyPinFunction(p, pPin) )
+            return pPin;
+    }
+    return NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns cell's area.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Amap_Item_t * Amap_LibertyCellArea( Amap_Tree_t * p, Amap_Item_t * pCell )
+{
+    Amap_Item_t * pArea;
+    Amap_ItemForEachChild( p, pCell, pArea )
+    {
+        if ( Amap_LibertyCompare(p, pArea->Key, "area") )
+            continue;
+        return pArea;
+    }
+    return NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Count cell's output pins (pins with a logic function).]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Amap_LibertyCellCountOutputs( Amap_Tree_t * p, Amap_Item_t * pCell )
+{
+    Amap_Item_t * pPin;
+    int Counter = 0;
+    Amap_ItemForEachChild( p, pCell, pPin )
+    {
+        if ( Amap_LibertyCompare(p, pPin->Key, "pin") )
+            continue;
+        if ( Amap_LibertyPinFunction(p, pPin) )
+            Counter++;
+    }
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Gets the name to write.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Amap_LibertyGetString( Amap_Tree_t * p, Amap_Pair_t Pair )   
+{ 
+    static char Buffer[256]; 
+    strncpy( Buffer, p->pContents+Pair.Beg, Pair.End-Pair.Beg ); 
+    Buffer[Pair.End-Pair.Beg] = 0;
+    return Buffer;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Gets the name to write.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Amap_LibertyGetStringFormula( Amap_Tree_t * p, Amap_Pair_t Pair )   
+{ 
+    static char Buffer[256]; 
+    strncpy( Buffer, p->pContents+Pair.Beg+1, Pair.End-Pair.Beg-2 ); 
+    Buffer[Pair.End-Pair.Beg-2] = 0;
+    return Buffer;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints parse tree in Genlib format.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Amap_LibertyPrintGenlib( Amap_Tree_t * p, char * pFileName )
+{
+    FILE * pFile;
+    Amap_Item_t * pCell, * pArea, * pFunc, * pPin, * pOutput;
+    int Counter;
+    if ( pFileName == NULL )
+        pFile = stdout;
+    else
+    {
+        pFile = fopen( pFileName, "w" );
+        if ( pFile == NULL )
+        {
+            printf( "Amap_LibertyPrintGenlib(): The output file is unavailable (absent or open).\n" );
+            return 0;
+        }
+    }
+    fprintf( pFile, "# This Genlib file was generated by ABC on %s\n", Amap_LibertyTimeStamp() );
+    fprintf( pFile, "# The standard cell library \"%s\" is from Liberty file \"%s\"\n", Amap_LibertyGetString(p, Amap_LibertyRoot(p)->Head), p->pFileName );
+    fprintf( pFile, "# (To find out more about Genlib format, google for \"sis_paper.ps\")\n" );
+
+    fprintf( pFile, "GATE  " );
+    fprintf( pFile, "%16s  ", "_const0_" );
+    fprintf( pFile, "%f  ",   0.0 );
+    fprintf( pFile, "%s=",    "z" );
+    fprintf( pFile, "%s;\n",  "CONST0" );
+
+    fprintf( pFile, "GATE  " );
+    fprintf( pFile, "%16s  ", "_const1_" );
+    fprintf( pFile, "%f  ",   0.0 );
+    fprintf( pFile, "%s=",    "z" );
+    fprintf( pFile, "%s;\n",  "CONST1" );
+
+    Amap_ItemForEachChild( p, Amap_LibertyRoot(p), pCell )
+    {
+/*
+    if ( strcmp(Amap_LibertyGetString(p, pCell->Head), "HA1SVTX1") == 0 )
+    {
+        int s = 0;
+    }
+*/
+        if ( Amap_LibertyCompare(p, pCell->Key, "cell") )
+            continue;
+        if ( Amap_LibertyCellIsFlop(p, pCell) )
+        {
+            printf( "Amap_LibertyPrintGenlib() skipped sequential cell \"%s\".\n", Amap_LibertyGetString(p, pCell->Head) );
+            continue;
+        }
+        Counter = Amap_LibertyCellCountOutputs( p, pCell );
+        if ( Counter == 0 )
+        {
+            printf( "Amap_LibertyPrintGenlib() skipped cell \"%s\" without logic function.\n", Amap_LibertyGetString(p, pCell->Head) );
+            continue;
+        }
+        if ( Counter > 1 )
+        {
+            printf( "Amap_LibertyPrintGenlib() skipped multi-output cell \"%s\".\n", Amap_LibertyGetString(p, pCell->Head) );
+            continue;
+        }
+        pArea = Amap_LibertyCellArea( p, pCell );
+        if ( pArea == NULL )
+        {
+            printf( "Amap_LibertyPrintGenlib() skipped cell \"%s\" with unspecified area.\n", Amap_LibertyGetString(p, pCell->Head) );
+            continue;
+        }
+        pOutput = Amap_LibertyCellOutput( p, pCell );
+        pFunc   = Amap_LibertyPinFunction( p, pOutput );
+
+        fprintf( pFile, "GATE  " );
+        fprintf( pFile, "%16s  ", Amap_LibertyGetString(p, pCell->Head) );
+        fprintf( pFile, "%f  ",   atof(Amap_LibertyGetString(p, pArea->Head)) );
+        fprintf( pFile, "%s=",    Amap_LibertyGetString(p, pOutput->Head) );
+        fprintf( pFile, "%s;\n",  Amap_LibertyGetStringFormula(p, pFunc->Head) );
+
+        Amap_ItemForEachChild( p, pCell, pPin )
+            if ( pPin != pOutput && !Amap_LibertyCompare(p, pPin->Key, "pin") )
+                fprintf( pFile, "    PIN  %13s  UNKNOWN  1  999  1.00  0.00  1.00  0.00\n", Amap_LibertyGetString(p, pPin->Head) );
+    }
+    if ( pFile != stdout )
+        fclose( pFile );
+    return 1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the file size.]
+
+  Description [The file should be closed.]
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Amap_LibertyFileSize( char * pFileName )
+{
+    FILE * pFile;
+    int nFileSize;
+    pFile = fopen( pFileName, "rb" );
+    if ( pFile == NULL )
+    {
+        printf( "Amap_LibertyFileSize(): The input file is unavailable (absent or open).\n" );
+        return 0;
+    }
+    fseek( pFile, 0, SEEK_END );  
+    nFileSize = ftell( pFile ); 
+    fclose( pFile );
+    return nFileSize;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Amap_LibertyFixFileHead( char * pFileName )
+{
+    char * pHead;
+    for ( pHead = pFileName; *pHead; pHead++ )
+        if ( *pHead == '>' )
+            *pHead = '\\';
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Amap_LibertyCountItems( char * pBeg, char * pEnd )
+{
+    int Counter = 0;
+    for ( ; pBeg < pEnd; pBeg++ )
+        Counter += (*pBeg == '(' || *pBeg == ':');
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Removes C-style comments.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Amap_LibertyWipeOutComments( char * pBeg, char * pEnd )
+{
+    char * pCur, * pStart;
+    for ( pCur = pBeg; pCur < pEnd; pCur++ )
+    if ( pCur[0] == '/' && pCur[1] == '*' )
+        for ( pStart = pCur; pCur < pEnd; pCur++ )
+        if ( pCur[0] == '*' && pCur[1] == '/' )
+        {
+            for ( ; pStart < pCur + 2; pStart++ )
+            if ( *pStart != '\n' ) *pStart = ' ';
+            break;
+        }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the character is space.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Amap_LibertyCharIsSpace( char c )
+{
+    return c == ' ' || c == '\t' || c == '\r' || c == '\n' || c == '\\';
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Skips spaces.]
+
+  Description [Returns 1 if reached the end.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Amap_LibertySkipSpaces( Amap_Tree_t * p, char ** ppPos, char * pEnd )
+{
+    char * pPos = *ppPos;
+    for ( ; pPos < pEnd; pPos++ )
+    {
+        if ( *pPos == '\n' )
+            p->nLines++;
+        if ( !Amap_LibertyCharIsSpace(*pPos) )
+            break;
+    }
+    *ppPos = pPos;
+    return pPos == pEnd;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Skips entry delimited by " :;(){}" ]
+
+  Description [Returns 1 if reached the end.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Amap_LibertySkipEntry( char ** ppPos, char * pEnd )
+{
+    char * pPos = *ppPos;
+    if ( *pPos == '\"' )
+    {
+        for ( pPos++; pPos < pEnd; pPos++ )
+            if ( *pPos == '\"' )
+            {
+                pPos++;
+                break;
+            }
+    }
+    else
+    {
+        for ( ; pPos < pEnd; pPos++ )
+            if ( *pPos == ' ' ||
+                 *pPos == ':' || *pPos == ';' || 
+                 *pPos == '(' || *pPos == ')' || 
+                 *pPos == '{' || *pPos == '}' )
+                break;
+    }
+    *ppPos = pPos;
+    return pPos == pEnd;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Find the matching closing symbol.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline char * Amap_LibertyFindMatch( char * pPos, char * pEnd )
+{
+    int Counter = 0;
+    assert( *pPos == '(' || *pPos == '{' );
+    if ( *pPos == '(' )
+    {
+        for ( ; pPos < pEnd; pPos++ )
+        {
+            if ( *pPos == '(' )
+                Counter++;
+            if ( *pPos == ')' )
+                Counter--;
+            if ( Counter == 0 )
+                break;
+        }
+    }
+    else
+    {
+        for ( ; pPos < pEnd; pPos++ )
+        {
+            if ( *pPos == '{' )
+                Counter++;
+            if ( *pPos == '}' )
+                Counter--;
+            if ( Counter == 0 )
+                break;
+        }
+    }
+    assert( *pPos == ')' || *pPos == '}' );
+    return pPos;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Find the matching closing symbol.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Amap_Pair_t Amap_LibertyUpdateHead( Amap_Tree_t * p, Amap_Pair_t Head )
+{
+    Amap_Pair_t Res;
+    char * pBeg = p->pContents + Head.Beg;
+    char * pEnd = p->pContents + Head.End;
+    char * pFirstNonSpace = NULL;
+    char * pLastNonSpace = NULL;
+    char * pChar;
+    for ( pChar = pBeg; pChar < pEnd; pChar++ )
+    {
+        if ( *pChar == '\n' )
+            p->nLines++;
+        if ( Amap_LibertyCharIsSpace(*pChar) )
+            continue;
+        pLastNonSpace = pChar;
+        if ( pFirstNonSpace == NULL )
+            pFirstNonSpace = pChar;
+    }
+    if ( pFirstNonSpace == NULL || pLastNonSpace == NULL )
+        return Head;
+    assert( pFirstNonSpace && pLastNonSpace );
+    Res.Beg = pFirstNonSpace - p->pContents;
+    Res.End = pLastNonSpace  - p->pContents + 1;
+    return Res;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns free item.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Amap_Item_t * Amap_LibertyNewItem( Amap_Tree_t * p, int Type )
+{
+    p->pItems[p->nItems].iLine = p->nLines;
+    p->pItems[p->nItems].Type  = Type;
+    p->pItems[p->nItems].Child = -1;
+    p->pItems[p->nItems].Next  = -1;
+    return p->pItems + p->nItems++;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns free item.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Amap_LibertyBuildItem( Amap_Tree_t * p, char ** ppPos, char * pEnd )
+{
+    Amap_Item_t * pItem;
+    Amap_Pair_t Key, Head, Body;
+    char * pNext, * pStop;
+    if ( Amap_LibertySkipSpaces( p, ppPos, pEnd ) )
+        return -2;
+    Key.Beg = *ppPos - p->pContents;
+    if ( Amap_LibertySkipEntry( ppPos, pEnd ) )
+        goto exit;
+    Key.End = *ppPos - p->pContents;
+    if ( Amap_LibertySkipSpaces( p, ppPos, pEnd ) )
+        goto exit;
+    pNext = *ppPos;
+    if ( *pNext == ':' )
+    {
+        *ppPos = pNext + 1;
+        if ( Amap_LibertySkipSpaces( p, ppPos, pEnd ) )
+            goto exit;
+        Head.Beg = *ppPos - p->pContents;
+        if ( Amap_LibertySkipEntry( ppPos, pEnd ) )
+            goto exit;
+        Head.End = *ppPos - p->pContents;
+        if ( Amap_LibertySkipSpaces( p, ppPos, pEnd ) )
+            goto exit;
+        pNext = *ppPos;
+        if ( *pNext != ';' )
+            goto exit;
+        *ppPos = pNext + 1;
+        // end of equation
+        pItem = Amap_LibertyNewItem( p, AMAP_LIBERTY_EQUA );
+        pItem->Key  = Key;
+        pItem->Head = Amap_LibertyUpdateHead( p, Head );
+        pItem->Next = Amap_LibertyBuildItem( p, ppPos, pEnd );
+        if ( pItem->Next == -1 )
+            goto exit;
+        return Amap_LibertyItemId( p, pItem );
+    }
+    if ( *pNext == '(' )
+    {
+        pStop = Amap_LibertyFindMatch( pNext, pEnd );
+        Head.Beg = pNext - p->pContents + 1;
+        Head.End = pStop - p->pContents;
+        *ppPos = pStop + 1;
+        if ( Amap_LibertySkipSpaces( p, ppPos, pEnd ) )
+        {
+            // end of list
+            pItem = Amap_LibertyNewItem( p, AMAP_LIBERTY_LIST );
+            pItem->Key  = Key;
+            pItem->Head = Amap_LibertyUpdateHead( p, Head );
+            return Amap_LibertyItemId( p, pItem );
+        }
+        pNext = *ppPos;
+        if ( *pNext == '{' ) // beginning of body
+        {
+            pStop = Amap_LibertyFindMatch( pNext, pEnd );
+            Body.Beg = pNext - p->pContents + 1;
+            Body.End = pStop - p->pContents;
+            // end of body
+            pItem = Amap_LibertyNewItem( p, AMAP_LIBERTY_PROC );
+            pItem->Key  = Key;
+            pItem->Head = Amap_LibertyUpdateHead( p, Head );
+            pItem->Body = Body;
+            *ppPos = pNext + 1;
+            pItem->Child = Amap_LibertyBuildItem( p, ppPos, pStop );
+            if ( pItem->Child == -1 )
+                goto exit;
+            *ppPos = pStop + 1;
+            pItem->Next = Amap_LibertyBuildItem( p, ppPos, pEnd );
+            if ( pItem->Next == -1 )
+                goto exit;
+            return Amap_LibertyItemId( p, pItem );
+        }
+        // end of list
+        if ( *pNext == ';' )
+            *ppPos = pNext + 1;
+        pItem = Amap_LibertyNewItem( p, AMAP_LIBERTY_LIST );
+        pItem->Key  = Key;
+        pItem->Head = Amap_LibertyUpdateHead( p, Head );
+        pItem->Next = Amap_LibertyBuildItem( p, ppPos, pEnd );
+        if ( pItem->Next == -1 )
+            goto exit;
+        return Amap_LibertyItemId( p, pItem );
+    }
+exit:
+    if ( p->pError == NULL )
+    {
+        p->pError = ABC_ALLOC( char, 1000 );
+        sprintf( p->pError, "File \"%s\". Line %6d. Failed to parse entry \"%s\".\n", 
+            p->pFileName, p->nLines, Amap_LibertyGetString(p, Key) );
+    }
+    return -1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the parsing manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Amap_Tree_t * Amap_LibertyStart( char * pFileName )
+{
+    FILE * pFile;
+    Amap_Tree_t * p;
+    // start the manager
+    p = ABC_ALLOC( Amap_Tree_t, 1 );
+    memset( p, 0, sizeof(Amap_Tree_t) );
+    // read the file into the buffer
+    Amap_LibertyFixFileHead( pFileName );
+    p->nContents = Amap_LibertyFileSize( pFileName );
+    if ( p->nContents == 0 )
+    {
+        ABC_FREE( p );
+        return NULL;
+    }
+    pFile = fopen( pFileName, "rb" );
+    p->pContents = ABC_ALLOC( char, p->nContents+1 );
+    fread( p->pContents, p->nContents, 1, pFile );
+    fclose( pFile );
+    p->pContents[p->nContents] = 0;
+    // other 
+    p->pFileName = Aig_UtilStrsav( pFileName );
+    p->nItermAlloc = 10 + Amap_LibertyCountItems( p->pContents, p->pContents+p->nContents );
+    p->pItems = ABC_CALLOC( Amap_Item_t, p->nItermAlloc );
+    p->nItems = 0;
+    p->nLines = 1;
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the parsing manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Amap_LibertyStop( Amap_Tree_t * p )
+{
+    ABC_FREE( p->pFileName );
+    ABC_FREE( p->pContents );
+    ABC_FREE( p->pItems );
+    ABC_FREE( p->pError );
+    ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Parses the standard cell library in Liberty format.]
+
+  Description [Writes the resulting file in Genlib format.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Amap_LibertyParse( char * pFileName, char * pFileGenlib, int fVerbose )
+{
+    Amap_Tree_t * p;
+    char * pPos;
+    int clk = clock();
+    int RetValue;
+    p = Amap_LibertyStart( pFileName );
+    if ( p == NULL )
+        return 0;
+    pPos = p->pContents;
+    Amap_LibertyWipeOutComments( p->pContents, p->pContents+p->nContents );
+    if ( Amap_LibertyBuildItem( p, &pPos, p->pContents + p->nContents ) == 0 )
+    {
+        if ( fVerbose )
+        printf( "Parsing finished successfully.\n" );
+//        Amap_LibertyPrintLiberty( p, "temp.lib" );
+        Amap_LibertyPrintGenlib( p, "temp.genlib" );
+        RetValue = 1;
+    }
+    else
+    {
+        if ( p->pError )
+            printf( "%s", p->pError );
+        if ( fVerbose )
+        printf( "Parsing failed.\n" );
+        RetValue = 0;
+    }
+    if ( fVerbose )
+    {
+    printf( "Memory = %7.2f Mb. ", 1.0*(p->nContents+p->nItermAlloc*sizeof(Amap_Item_t))/(1<<20) );
+    ABC_PRT( "Time", clock() - clk );
+    }
+    Amap_LibertyStop( p );
+    return RetValue;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/map/amap/amapMan.c b/src/map/amap/amapMan.c
index 521b4ffd..a1a66869 100644
--- a/src/map/amap/amapMan.c
+++ b/src/map/amap/amapMan.c
@@ -43,7 +43,7 @@ Amap_Man_t * Amap_ManStart( int nNodes )
 {
     Amap_Man_t * p;
     // start the manager
-    p = ALLOC( Amap_Man_t, 1 );
+    p = ABC_ALLOC( Amap_Man_t, 1 );
     memset( p, 0, sizeof(Amap_Man_t) );
     p->fEpsilonInternal = (float)0.01;
     // allocate arrays for nodes
@@ -86,10 +86,10 @@ void Amap_ManStop( Amap_Man_t * p )
     Aig_MmFlexStop( p->pMemCuts, 0 );
     Aig_MmFlexStop( p->pMemCutBest, 0 );
     Aig_MmFlexStop( p->pMemTemp, 0 );
-    FREE( p->pMatsTemp );
-    FREE( p->ppCutsTemp );
-    FREE( p->pCutsPi );
-    free( p );
+    ABC_FREE( p->pMatsTemp );
+    ABC_FREE( p->ppCutsTemp );
+    ABC_FREE( p->pCutsPi );
+    ABC_FREE( p );
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/map/amap/amapMatch.c b/src/map/amap/amapMatch.c
index 0b15a931..0ea65219 100644
--- a/src/map/amap/amapMatch.c
+++ b/src/map/amap/amapMatch.c
@@ -122,7 +122,7 @@ void Amap_ManCleanData( Amap_Man_t * p )
     Amap_Obj_t * pObj;
     int i;
 //    Amap_ManForEachNode( p, pObj, i )
-//        FREE( pObj->pData );
+//        ABC_FREE( pObj->pData );
     Amap_ManForEachObj( p, pObj, i )
         pObj->pData = NULL;
 }
@@ -496,7 +496,7 @@ if ( p->pPars->fVerbose )
         Area + nInvs * p->fAreaInv, 
         Area, nInvs * p->fAreaInv, nInvs,
         Amap_ManMaxDelay(p) );
-PRT( "Time ", clock() - clk );
+ABC_PRT( "Time ", clock() - clk );
 }
     // test procedures
 //    Amap_ManForEachNode( p, pObj, i )
diff --git a/src/map/amap/amapMerge.c b/src/map/amap/amapMerge.c
index b024616e..1a6e3804 100644
--- a/src/map/amap/amapMerge.c
+++ b/src/map/amap/amapMerge.c
@@ -44,7 +44,7 @@ Amap_Cut_t * Amap_ManSetupPis( Amap_Man_t * p )
     Amap_Obj_t * pObj;
     Amap_Cut_t * pCut;
     int i, nBytes = sizeof(Amap_Cut_t) + sizeof(int);
-    char * pBuffer = ALLOC( char, Amap_ManPiNum(p) * nBytes );
+    char * pBuffer = ABC_ALLOC( char, Amap_ManPiNum(p) * nBytes );
     Amap_ManForEachPi( p, pObj, i )
     {
         pCut = (Amap_Cut_t *)( pBuffer + i*nBytes );
@@ -509,7 +509,7 @@ void Amap_ManMerge( Amap_Man_t * p )
         printf( "Node =%6d. Try =%9d. Try3 =%10d. Used =%7d. R =%6.2f.  ", 
             Amap_ManNodeNum(p), p->nCutsTried, p->nCutsTried3, p->nCutsUsed, 
             1.0*p->nCutsUsed/Amap_ManNodeNum(p) );
-PRT( "Time ", clock() - clk );
+ABC_PRT( "Time ", clock() - clk );
     }
 }
 
diff --git a/src/map/amap/amapParse.c b/src/map/amap/amapParse.c
index 262fbd5a..48dabca2 100644
--- a/src/map/amap/amapParse.c
+++ b/src/map/amap/amapParse.c
@@ -122,7 +122,7 @@ Hop_Obj_t * Amap_ParseFormula( FILE * pOutput, char * pFormInit, Vec_Ptr_t * vVa
     }
 
     // copy the formula
-    pFormula = ALLOC( char, strlen(pFormInit) + 3 );
+    pFormula = ABC_ALLOC( char, strlen(pFormInit) + 3 );
     sprintf( pFormula, "(%s)", pFormInit );
 
     // start the stacks
@@ -198,10 +198,10 @@ Hop_Obj_t * Amap_ParseFormula( FILE * pOutput, char * pFormInit, Vec_Ptr_t * vVa
         case AMAP_EQN_SYM_OPEN:
             if ( Flag == AMAP_EQN_FLAG_VAR )
             {
-//                Vec_IntPush( pStackOp, AMAP_EQN_OPER_AND );
-                fprintf( pOutput, "Amap_ParseFormula(): An opening paranthesis follows a var without operation sign.\n" ); 
-                Flag = AMAP_EQN_FLAG_ERROR; 
-                break; 
+                Vec_IntPush( pStackOp, AMAP_EQN_OPER_AND );
+//                fprintf( pOutput, "Amap_ParseFormula(): An opening paranthesis follows a var without operation sign.\n" ); 
+//                Flag = AMAP_EQN_FLAG_ERROR; 
+//              break; 
             }
             Vec_IntPush( pStackOp, AMAP_EQN_OPER_MARK );
             // after an opening bracket, it feels like starting over again
@@ -226,7 +226,7 @@ Hop_Obj_t * Amap_ParseFormula( FILE * pOutput, char * pFormInit, Vec_Ptr_t * vVa
                     if ( Amap_ParseFormulaOper( pMan, pStackFn, Oper ) == NULL )
                     {
                         fprintf( pOutput, "Amap_ParseFormula(): Unknown operation\n" );
-                        free( pFormula );
+                        ABC_FREE( pFormula );
                         return NULL;
                     }
                 }
@@ -247,7 +247,8 @@ Hop_Obj_t * Amap_ParseFormula( FILE * pOutput, char * pFormInit, Vec_Ptr_t * vVa
             for ( i = 0; pTemp[i] && 
                          pTemp[i] != ' ' && pTemp[i] != '\t' && pTemp[i] != '\r' && pTemp[i] != '\n' &&
                          pTemp[i] != AMAP_EQN_SYM_AND && pTemp[i] != AMAP_EQN_SYM_OR && 
-                         pTemp[i] != AMAP_EQN_SYM_XOR && pTemp[i] != AMAP_EQN_SYM_CLOSE; i++ )
+                         pTemp[i] != AMAP_EQN_SYM_XOR && pTemp[i] != AMAP_EQN_SYM_NEGAFT && 
+                         pTemp[i] != AMAP_EQN_SYM_CLOSE; i++ )
               {
                     if ( pTemp[i] == AMAP_EQN_SYM_NEG || pTemp[i] == AMAP_EQN_SYM_OPEN )
                     {
@@ -271,12 +272,17 @@ Hop_Obj_t * Amap_ParseFormula( FILE * pOutput, char * pFormInit, Vec_Ptr_t * vVa
                 Flag = AMAP_EQN_FLAG_ERROR; 
                 break; 
             }
+/*
             if ( Flag == AMAP_EQN_FLAG_VAR )
             {
                 fprintf( pOutput, "Amap_ParseFormula(): The variable name \"%s\" follows another var without operation sign.\n", pTemp ); 
                 Flag = AMAP_EQN_FLAG_ERROR; 
                 break; 
             }
+*/
+            if ( Flag == AMAP_EQN_FLAG_VAR )
+                Vec_IntPush( pStackOp, AMAP_EQN_OPER_AND );
+
             Vec_PtrPush( pStackFn, Hop_IthVar( pMan, v ) ); // Cudd_Ref( pbVars[v] );
             Flag = AMAP_EQN_FLAG_VAR; 
             break;
@@ -318,7 +324,7 @@ Hop_Obj_t * Amap_ParseFormula( FILE * pOutput, char * pFormInit, Vec_Ptr_t * vVa
                     if ( Amap_ParseFormulaOper( pMan, pStackFn, Oper2 ) == NULL )
                     {
                         fprintf( pOutput, "Amap_ParseFormula(): Unknown operation\n" );
-                        free( pFormula );
+                        ABC_FREE( pFormula );
                         return NULL;
                     }
                     Vec_IntPush( pStackOp,  Oper1 );     // push the last operation back
@@ -343,7 +349,7 @@ Hop_Obj_t * Amap_ParseFormula( FILE * pOutput, char * pFormInit, Vec_Ptr_t * vVa
                     Vec_PtrFree(pStackFn);
                     Vec_IntFree(pStackOp);
 //                    Cudd_Deref( gFunc );
-                    free( pFormula );
+                    ABC_FREE( pFormula );
                     return gFunc;
                 }
                 else
@@ -354,7 +360,7 @@ Hop_Obj_t * Amap_ParseFormula( FILE * pOutput, char * pFormInit, Vec_Ptr_t * vVa
         else
             fprintf( pOutput, "Amap_ParseFormula(): The input string is empty\n" );
     }
-    free( pFormula );
+    ABC_FREE( pFormula );
     return NULL;
 }
 
@@ -414,7 +420,7 @@ int Amap_LibParseEquations( Amap_Lib_t * p, int fVerbose )
         pTruth = Hop_ManConvertAigToTruth( pMan, pObj, pGate->nPins, vTruth, 0 );
         if ( Kit_TruthSupportSize(pTruth, pGate->nPins) < (int)pGate->nPins )
         {
-            printf( "Skipping gate \"%s\" because its formula \"%s\" does not depend on some pin variables.\n", pGate->pName, pGate->pForm );
+            printf( "Skipping gate \"%s\" because its output \"%s\" does not depend on all input variables.\n", pGate->pName, pGate->pForm );
             continue;
         }
         pGate->pFunc = (unsigned *)Aig_MmFlexEntryFetch( p->pMemGates, sizeof(unsigned)*Aig_TruthWordNum(pGate->nPins) );
@@ -447,7 +453,7 @@ void Amap_LibParseTest( char * pFileName )
         return;
     Amap_LibParseEquations( p, fVerbose );
     Amap_LibFree( p );
-    PRT( "Total time", clock() - clk );
+    ABC_PRT( "Total time", clock() - clk );
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/map/amap/amapRead.c b/src/map/amap/amapRead.c
index 182de5d1..7ebc239b 100644
--- a/src/map/amap/amapRead.c
+++ b/src/map/amap/amapRead.c
@@ -89,7 +89,7 @@ char * Amap_LoadFile( char * pFileName )
     // move the file current reading position to the beginning
     rewind( pFile ); 
     // load the contents of the file into memory
-    pBuffer = ALLOC( char, nFileSize + 10 );
+    pBuffer = ABC_ALLOC( char, nFileSize + 10 );
     fread( pBuffer, nFileSize, 1, pFile );
     // terminate the string with '\0'
     pBuffer[ nFileSize ] = '\0';
@@ -173,11 +173,11 @@ Vec_Ptr_t * Amap_DeriveTokens( char * pBuffer )
     Vec_Ptr_t * vTokens;
     char * pToken;
     vTokens = Vec_PtrAlloc( 1000 );
-    pToken = strtok( pBuffer, " ;=\t\r\n" );
+    pToken = strtok( pBuffer, " =\t\r\n" );
     while ( pToken )
     {
         Vec_PtrPush( vTokens, pToken );
-        pToken = strtok( NULL, " ;=\t\r\n" );
+        pToken = strtok( NULL, " =\t\r\n" );
     }
     return vTokens;
 }
@@ -288,6 +288,32 @@ Amap_Gat_t * Amap_ParseGateWithSamePins( Amap_Gat_t * p )
   SeeAlso     []
 
 ***********************************************************************/
+int Amap_CollectFormulaTokens( Vec_Ptr_t * vTokens, char * pToken, int iPos )
+{
+    char * pNext, * pPrev;
+    pPrev = pToken + strlen(pToken);
+    while ( *(pPrev-1) != ';' )
+    {
+        *pPrev++ = ' ';
+        pNext = Vec_PtrEntry(vTokens, iPos++);
+        while ( *pNext )
+            *pPrev++ = *pNext++;
+    }
+    *(pPrev-1) = 0;
+    return iPos;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 Amap_Lib_t * Amap_ParseTokens( Vec_Ptr_t * vTokens, int fVerbose )
 {
     Amap_Lib_t * p;
@@ -320,6 +346,7 @@ Amap_Lib_t * Amap_ParseTokens( Vec_Ptr_t * vTokens, int fVerbose )
         pToken = Vec_PtrEntry(vTokens, iPos++);
         pGate->pOutName = Amap_ParseStrsav( p->pMemGates, pToken ); 
         pToken = Vec_PtrEntry(vTokens, iPos++);
+        iPos = Amap_CollectFormulaTokens( vTokens, pToken, iPos );
         pGate->pForm = Amap_ParseStrsav( p->pMemGates, pToken ); 
         // read pins
         Amap_GateForEachPin( pGate, pPin )
@@ -401,7 +428,7 @@ Amap_Lib_t * Amap_LibReadFile( char * pFileName, int fVerbose )
         return NULL;
     pLib->pName = Amap_ParseStrsav( pLib->pMemGates, pFileName );
     Vec_PtrFree( vTokens );
-    free( pBuffer );
+    ABC_FREE( pBuffer );
     return pLib;
 }
 
diff --git a/src/map/amap/amapUniq.c b/src/map/amap/amapUniq.c
index 83fce6a2..e57161e4 100644
--- a/src/map/amap/amapUniq.c
+++ b/src/map/amap/amapUniq.c
@@ -134,7 +134,7 @@ Amap_Nod_t * Amap_LibCreateObj( Amap_Lib_t * p )
     Amap_Nod_t * pNode;
     if ( p->nNodes == p->nNodesAlloc )
     {
-        p->pNodes = REALLOC( Amap_Nod_t, p->pNodes, 2*p->nNodesAlloc );
+        p->pNodes = ABC_REALLOC( Amap_Nod_t, p->pNodes, 2*p->nNodesAlloc );
         p->nNodesAlloc *= 2;
     }
     pNode = Amap_LibNod( p, p->nNodes );
@@ -164,7 +164,7 @@ int Amap_LibCreateVar( Amap_Lib_t * p )
     // start the manager
     assert( p->pNodes == NULL );
     p->nNodesAlloc = 256;
-    p->pNodes = ALLOC( Amap_Nod_t, p->nNodesAlloc );
+    p->pNodes = ABC_ALLOC( Amap_Nod_t, p->nNodesAlloc );
     // create the first node
     pNode = Amap_LibCreateObj( p );
     p->pNodes->Type = AMAP_OBJ_PI;
@@ -281,7 +281,7 @@ int ** Amap_LibLookupTableAlloc( Vec_Ptr_t * vVec, int fVerbose )
     nEntries = nSize = Vec_PtrSize( vVec );
     Vec_PtrForEachEntry( vVec, vOne, i )
         nEntries += Vec_IntSize(vOne);
-    pBuffer = ALLOC( int, nSize * sizeof(void *) + nEntries );
+    pBuffer = ABC_ALLOC( int, nSize * sizeof(void *) + nEntries );
     pRes = (int **)pBuffer;
     pRes[0] = pBuffer + nSize * sizeof(void *);
     nTotal = 0;
diff --git a/src/map/amap/module.make b/src/map/amap/module.make
index d5edadb9..2d534009 100644
--- a/src/map/amap/module.make
+++ b/src/map/amap/module.make
@@ -1,6 +1,7 @@
 SRC +=  src/map/amap/amapCore.c \
     src/map/amap/amapGraph.c \
     src/map/amap/amapLib.c \
+    src/map/amap/amapLiberty.c \
     src/map/amap/amapMan.c \
     src/map/amap/amapMatch.c \
     src/map/amap/amapMerge.c \