Adding support for minimalistic representation of LUT mapping.

7 files changed, 500 insertions, 11 deletions

diff --git a/abclib.dsp b/abclib.dsp
index 8d33b15b..3ffe0e44 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -4577,6 +4577,10 @@ SOURCE=.\src\aig\gia\giaUtil.c
 
 SOURCE=.\src\aig\miniaig\miniaig.h
 # End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\miniaig\minilut.h
+# End Source File
 # End Group
 # End Group
 # Begin Group "bool"
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 3d2d84ae..bf7bf349 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -1382,6 +1382,8 @@ extern Gia_Man_t *         Mf_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pP
 /*=== giaMini.c ===========================================================*/
 extern Gia_Man_t *         Gia_ManReadMiniAig( char * pFileName );
 extern void                Gia_ManWriteMiniAig( Gia_Man_t * pGia, char * pFileName );
+extern Gia_Man_t *         Gia_ManReadMiniLut( char * pFileName );
+extern void                Gia_ManWriteMiniLut( Gia_Man_t * pGia, char * pFileName );
 /*=== giaMuxes.c ===========================================================*/
 extern void                Gia_ManCountMuxXor( Gia_Man_t * p, int * pnMuxes, int * pnXors );
 extern void                Gia_ManPrintMuxStats( Gia_Man_t * p );
diff --git a/src/aig/gia/giaMini.c b/src/aig/gia/giaMini.c
index 442be57c..77bb1b64 100644
--- a/src/aig/gia/giaMini.c
+++ b/src/aig/gia/giaMini.c
@@ -19,8 +19,10 @@
 ***********************************************************************/
 
 #include "gia.h"
+#include "opt/dau/dau.h"
 #include "base/main/main.h"
 #include "aig/miniaig/miniaig.h"
+#include "aig/miniaig/minilut.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -180,6 +182,186 @@ void Gia_ManWriteMiniAig( Gia_Man_t * pGia, char * pFileName )
     Mini_AigStop( p );
 }
 
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Converts MiniLUT into GIA.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManFromMiniLut( Mini_Lut_t * p )
+{
+    Gia_Man_t * pGia, * pTemp;
+    Vec_Int_t * vCopies;
+    Vec_Int_t * vCover = Vec_IntAlloc( 1000 );
+    Vec_Int_t * vLits = Vec_IntAlloc( 100 );
+    int i, k, Fan, iGiaLit, nNodes;
+    int LutSize = Abc_MaxInt( 2, Mini_LutSize(p) );
+    assert( LutSize <= 6 );
+    // get the number of nodes
+    nNodes = Mini_LutNodeNum(p);
+    // create ABC network
+    pGia = Gia_ManStart( 3 * nNodes );
+    pGia->pName = Abc_UtilStrsav( "MiniLut" );
+    // create mapping from MiniLUT objects into ABC objects
+    vCopies = Vec_IntAlloc( nNodes );
+    Vec_IntPush( vCopies, 0 );
+    Vec_IntPush( vCopies, 1 );
+    // iterate through the objects
+    Gia_ManHashAlloc( pGia );
+    for ( i = 2; i < nNodes; i++ )
+    {
+        if ( Mini_LutNodeIsPi( p, i ) )
+            iGiaLit = Gia_ManAppendCi(pGia);
+        else if ( Mini_LutNodeIsPo( p, i ) )
+            iGiaLit = Gia_ManAppendCo(pGia, Vec_IntEntry(vCopies, Mini_LutNodeFanin(p, i, 0)));
+        else if ( Mini_LutNodeIsNode( p, i ) )
+        {
+            unsigned * puTruth = Mini_LutNodeTruth( p, i );
+            word Truth = LutSize == 6 ? *(word *)puTruth : ((word)*puTruth << 32) | (word)*puTruth; 
+            Vec_IntClear( vLits );
+            Mini_LutForEachFanin( p, i, Fan, k )
+                Vec_IntPush( vLits, Vec_IntEntry(vCopies, Fan) );
+            iGiaLit = Dsm_ManTruthToGia( pGia, &Truth, vLits, vCover );
+        }
+        else assert( 0 );
+        Vec_IntPush( vCopies, iGiaLit );
+    }
+    Vec_IntFree( vCover );
+    Vec_IntFree( vLits );
+    Gia_ManHashStop( pGia );
+    assert( Vec_IntSize(vCopies) == nNodes );
+    Vec_IntFree( vCopies );
+    Gia_ManSetRegNum( pGia, Mini_LutRegNum(p) );
+    pGia = Gia_ManCleanup( pTemp = pGia );
+    Gia_ManStop( pTemp );
+    return pGia;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Converts GIA into MiniLUT.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Mini_Lut_t * Gia_ManToMiniLut( Gia_Man_t * pGia )
+{
+    Mini_Lut_t * p;
+    Vec_Wrd_t * vTruths;
+    Gia_Obj_t * pObj, * pFanin;
+    int i, k, LutSize, pVars[16];
+    word Truth;
+    assert( Gia_ManHasMapping(pGia) );
+    LutSize = Gia_ManLutSizeMax( pGia );
+    assert( LutSize >= 2 );
+    // create the manager
+    p = Mini_LutStart( LutSize );
+    // create primary inputs
+    Gia_ManFillValue( pGia );
+    Gia_ManForEachCi( pGia, pObj, i )
+        pObj->Value = Mini_LutCreatePi(p);
+    // create internal nodes
+    vTruths = Vec_WrdStart( Gia_ManObjNum(pGia) );
+    Gia_ManForEachLut( pGia, i )
+    {
+        pObj = Gia_ManObj( pGia, i );
+        Gia_LutForEachFaninObj( pGia, i, pFanin, k )
+            pVars[k] = pFanin->Value;
+        Truth = Gia_LutComputeTruth6( pGia, i, vTruths );
+        pObj->Value = Mini_LutCreateNode( p, Gia_ObjLutSize(pGia, i), pVars, (unsigned *)&Truth );
+    }
+    Vec_WrdFree( vTruths );
+    // create primary outputs
+    Gia_ManForEachCo( pGia, pObj, i )
+    {
+        if ( Gia_ObjFanin0(pObj) == Gia_ManConst0(pGia) )
+            pObj->Value = Mini_LutCreatePo( p, Gia_ObjFaninC0(pObj) );
+        else if ( !Gia_ObjFaninC0(pObj) )
+            pObj->Value = Mini_LutCreatePo( p, Gia_ObjFanin0(pObj)->Value );
+        else // add inverter LUT
+        {
+            word TruthInv = ABC_CONST(0x5555555555555555);
+            int Fanin = Gia_ObjFanin0(pObj)->Value;
+            int LutInv = Mini_LutCreateNode( p, 1, &Fanin, (unsigned *)&TruthInv );
+            pObj->Value = Mini_LutCreatePo( p, LutInv );
+        }
+    }
+    // set registers
+    Mini_LutSetRegNum( p, Gia_ManRegNum(pGia) );
+    Mini_LutPrintStats( p );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Procedures to input/output MiniAIG into/from internal GIA.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_FrameGiaInputMiniLut( Abc_Frame_t * pAbc, void * p )
+{
+    Gia_Man_t * pGia;
+    if ( pAbc == NULL )
+        printf( "ABC framework is not initialized by calling Abc_Start()\n" );
+    pGia = Gia_ManFromMiniLut( (Mini_Lut_t *)p );
+    Abc_FrameUpdateGia( pAbc, pGia );
+//    Gia_ManDelete( pGia );
+}
+void * Abc_FrameGiaOutputMiniLut( Abc_Frame_t * pAbc )
+{
+    Gia_Man_t * pGia;
+    if ( pAbc == NULL )
+        printf( "ABC framework is not initialized by calling Abc_Start()\n" );
+    pGia = Abc_FrameReadGia( pAbc );
+    if ( pGia == NULL )
+        printf( "Current network in ABC framework is not defined.\n" );
+    return Gia_ManToMiniLut( pGia );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Procedures to read/write GIA to/from MiniAIG file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManReadMiniLut( char * pFileName )
+{
+    Mini_Lut_t * p = Mini_LutLoad( pFileName );
+    Gia_Man_t * pGia = Gia_ManFromMiniLut( p );
+    ABC_FREE( pGia->pName );
+    pGia->pName = Extra_FileNameGeneric( pFileName ); 
+    Mini_LutStop( p );
+    return pGia;
+}
+void Gia_ManWriteMiniLut( Gia_Man_t * pGia, char * pFileName )
+{
+    Mini_Lut_t * p = Gia_ManToMiniLut( pGia );
+    Mini_LutDump( p, pFileName );
+    Mini_LutStop( p );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/miniaig/miniaig.h b/src/aig/miniaig/miniaig.h
index dadb578b..6843648e 100644
--- a/src/aig/miniaig/miniaig.h
+++ b/src/aig/miniaig/miniaig.h
@@ -78,6 +78,7 @@ static void Mini_AigPush( Mini_Aig_t * p, int Lit0, int Lit1 )
 {
     if ( p->nSize + 2 > p->nCap )
     {
+        assert( p->nSize < MINI_AIG_NULL/4 );
         if ( p->nCap < MINI_AIG_START_SIZE )
             Mini_AigGrow( p, MINI_AIG_START_SIZE );
         else
diff --git a/src/aig/miniaig/minilut.h b/src/aig/miniaig/minilut.h
new file mode 100644
index 00000000..953f0bd3
--- /dev/null
+++ b/src/aig/miniaig/minilut.h
@@ -0,0 +1,288 @@
+/**CFile****************************************************************
+
+  FileName    [minilut.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Minimalistic representation of LUT mapped network.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - September 29, 2012.]
+
+  Revision    [$Id: minilut.h,v 1.00 2012/09/29 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef MINI_LUT__mini_lut_h
+#define MINI_LUT__mini_lut_h
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <assert.h>
+
+ABC_NAMESPACE_HEADER_START
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+#define MINI_LUT_NULL       (0x7FFFFFFF)
+#define MINI_LUT_NULL2      (0x7FFFFFFE)
+#define MINI_LUT_START_SIZE (0x000000FF)
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Mini_Lut_t_       Mini_Lut_t;
+struct Mini_Lut_t_ 
+{
+    int           nCap;
+    int           nSize;
+    int           nRegs;
+    int           LutSize;
+    int *         pArray;
+    unsigned *    pTruths;
+};
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+// memory management
+#define MINI_LUT_ALLOC(type, num)     ((type *) malloc(sizeof(type) * (num)))
+#define MINI_LUT_CALLOC(type, num)    ((type *) calloc((num), sizeof(type)))
+#define MINI_LUT_FALLOC(type, num)    ((type *) memset(malloc(sizeof(type) * (num)), 0xff, sizeof(type) * (num)))
+#define MINI_LUT_FREE(obj)            ((obj) ? (free((char *) (obj)), (obj) = 0) : 0)
+#define MINI_LUT_REALLOC(type, obj, num) \
+        ((obj) ? ((type *) realloc((char *)(obj), sizeof(type) * (num))) : \
+         ((type *) malloc(sizeof(type) * (num))))
+
+// compute truth table size measured in unsigned's
+static int  Mini_LutWordNum( int LutSize ) 
+{
+    return LutSize > 5 ? 1 << (LutSize-5) : 1;
+}
+
+// internal procedures
+static void Mini_LutGrow( Mini_Lut_t * p, int nCapMin )
+{
+    if ( p->nCap >= nCapMin )
+        return;
+    p->pArray  = MINI_LUT_REALLOC( int,      p->pArray,  nCapMin * p->LutSize ); 
+    p->pTruths = MINI_LUT_REALLOC( unsigned, p->pTruths, nCapMin * Mini_LutWordNum(p->LutSize) ); 
+    p->nCap   = nCapMin;
+    assert( p->pArray );
+    assert( p->pTruths );
+}
+static void Mini_LutPush( Mini_Lut_t * p, int nVars, int * pVars, unsigned * pTruth )
+{
+    int i, nWords = Mini_LutWordNum(p->LutSize);
+    if ( p->nSize == p->nCap )
+    {
+        assert( p->LutSize*p->nSize < MINI_LUT_NULL/2 );
+        if ( p->nCap < MINI_LUT_START_SIZE )
+            Mini_LutGrow( p, MINI_LUT_START_SIZE );
+        else
+            Mini_LutGrow( p, 2 * p->nCap );
+    }
+    for ( i = 0; i < nVars; i++ )
+        p->pArray[p->LutSize * p->nSize + i] = pVars[i];
+    for ( ; i < p->LutSize; i++ )
+        p->pArray[p->LutSize * p->nSize + i] = MINI_LUT_NULL;
+    for ( i = 0; i < nWords; i++ )
+        p->pTruths[nWords * p->nSize + i] = pTruth? pTruth[i] : 0;
+    p->nSize++;
+}
+
+// accessing fanins
+static int Mini_LutNodeFanin( Mini_Lut_t * p, int Id, int k )
+{
+    assert( Id >= 0 && Id < p->nSize );
+    return p->pArray[p->LutSize*Id+k];
+}
+static unsigned * Mini_LutNodeTruth( Mini_Lut_t * p, int Id )    
+{ 
+    assert( Id >= 0 && Id < p->nSize ); 
+    return p->pTruths + Id * Mini_LutWordNum(p->LutSize);
+}
+
+// working with LUTs
+static int      Mini_LutNodeConst0()                           { return 0;                    }
+static int      Mini_LutNodeConst1()                           { return 1;                    }
+
+static int      Mini_LutNodeNum( Mini_Lut_t * p )              { return p->nSize;             }
+static int      Mini_LutNodeIsConst( Mini_Lut_t * p, int Id )  { assert( Id >= 0 ); return Id == 0 || Id == 1; }
+static int      Mini_LutNodeIsPi( Mini_Lut_t * p, int Id )     { assert( Id >= 0 ); return Id > 0 && Mini_LutNodeFanin( p, Id, 0 ) == MINI_LUT_NULL; }
+static int      Mini_LutNodeIsPo( Mini_Lut_t * p, int Id )     { assert( Id >= 0 ); return Id > 0 && Mini_LutNodeFanin( p, Id, 0 ) != MINI_LUT_NULL && Mini_LutNodeFanin( p, Id, 1 ) == MINI_LUT_NULL2; }
+static int      Mini_LutNodeIsNode( Mini_Lut_t * p, int Id )   { assert( Id >= 0 ); return Id > 0 && Mini_LutNodeFanin( p, Id, 0 ) != MINI_LUT_NULL && Mini_LutNodeFanin( p, Id, 1 ) != MINI_LUT_NULL2; }
+
+static int      Mini_LutSize( Mini_Lut_t * p )                 { return p->LutSize;           }
+
+// working with sequential AIGs
+static int      Mini_LutRegNum( Mini_Lut_t * p )               { return p->nRegs;             }
+static void     Mini_LutSetRegNum( Mini_Lut_t * p, int n )     { p->nRegs = n;                }
+
+// iterators through objects
+#define Mini_LutForEachPi( p, i )    for (i = 2; i < Mini_LutNodeNum(p); i++) if ( !Mini_LutNodeIsPi(p, i) )   {} else 
+#define Mini_LutForEachPo( p, i )    for (i = 2; i < Mini_LutNodeNum(p); i++) if ( !Mini_LutNodeIsPo(p, i) )   {} else 
+#define Mini_LutForEachNode( p, i )  for (i = 2; i < Mini_LutNodeNum(p); i++) if ( !Mini_LutNodeIsNode(p, i) ) {} else
+
+// iterator through fanins
+#define Mini_LutForEachFanin( p, i, Fan, k ) for (k = 0; (k < p->LutSize) && (Fan = Mini_LutNodeFanin(p, i, k)) < MINI_LUT_NULL2; k++) 
+
+// constructor/destructor
+static Mini_Lut_t * Mini_LutStart( int LutSize )
+{
+    Mini_Lut_t * p; int i;
+    assert( LutSize >= 2 && LutSize <= 16 );
+    p = MINI_LUT_CALLOC( Mini_Lut_t, 1 );
+    p->LutSize = LutSize;
+    p->nCap    = MINI_LUT_START_SIZE;
+    p->pArray  = MINI_LUT_ALLOC( int,      p->nCap * p->LutSize );
+    p->pTruths = MINI_LUT_ALLOC( unsigned, p->nCap * Mini_LutWordNum(p->LutSize) );
+    Mini_LutPush( p, 0, NULL, NULL ); // const0
+    Mini_LutPush( p, 0, NULL, NULL ); // const1
+    for ( i = 0; i < Mini_LutWordNum(p->LutSize); i++ )
+        p->pTruths[i] = 0;
+    for ( i = 0; i < Mini_LutWordNum(p->LutSize); i++ )
+        p->pTruths[Mini_LutWordNum(p->LutSize) + i] = ~0;
+    return p;
+}
+static void Mini_LutStop( Mini_Lut_t * p )
+{
+    MINI_LUT_FREE( p->pArray );
+    MINI_LUT_FREE( p->pTruths );
+    MINI_LUT_FREE( p );
+}
+static void Mini_LutPrintStats( Mini_Lut_t * p )
+{
+    int i, nPis, nPos, nNodes;
+    nPis = 0;
+    Mini_LutForEachPi( p, i )
+        nPis++;
+    nPos = 0;
+    Mini_LutForEachPo( p, i )
+        nPos++;
+    nNodes = 0;
+    Mini_LutForEachNode( p, i )
+        nNodes++;
+    printf( "PI = %d. PO = %d. LUT = %d.\n", nPis, nPos, nNodes );
+}
+
+// serialization
+static void Mini_LutDump( Mini_Lut_t * p, char * pFileName )
+{
+    FILE * pFile;
+    int RetValue;
+    pFile = fopen( pFileName, "wb" );
+    if ( pFile == NULL )
+    {
+        printf( "Cannot open file for writing \"%s\".\n", pFileName );
+        return;
+    }
+    RetValue = fwrite( &p->nSize,   sizeof(int), 1, pFile );
+    RetValue = fwrite( &p->nRegs,   sizeof(int), 1, pFile );
+    RetValue = fwrite( &p->LutSize, sizeof(int), 1, pFile );
+    RetValue = fwrite( p->pArray,   sizeof(int), p->nSize * p->LutSize, pFile );
+    RetValue = fwrite( p->pTruths,  sizeof(int), p->nSize * Mini_LutWordNum(p->LutSize), pFile );
+    fclose( pFile );
+}
+static Mini_Lut_t * Mini_LutLoad( char * pFileName )
+{
+    Mini_Lut_t * p;
+    FILE * pFile;
+    int RetValue, nSize;
+    pFile = fopen( pFileName, "rb" );
+    if ( pFile == NULL )
+    {
+        printf( "Cannot open file for reading \"%s\".\n", pFileName );
+        return NULL;
+    }
+    RetValue = fread( &nSize, sizeof(int), 1, pFile );
+    p = MINI_LUT_CALLOC( Mini_Lut_t, 1 );
+    p->nSize   = p->nCap = nSize;
+    RetValue = fread( &p->nRegs,   sizeof(int), 1, pFile );
+    RetValue = fread( &p->LutSize, sizeof(int), 1, pFile );
+    p->pArray  = MINI_LUT_ALLOC( int, p->nCap * p->LutSize );
+    p->pTruths = MINI_LUT_ALLOC( int, p->nCap * Mini_LutWordNum(p->LutSize) );
+    RetValue = fread( p->pArray,   sizeof(int), p->nCap * p->LutSize, pFile );
+    RetValue = fread( p->pTruths,  sizeof(int), p->nCap * Mini_LutWordNum(p->LutSize), pFile );
+    fclose( pFile );
+    return p;
+}
+
+
+// creating nodes 
+// (constant nodes are created when LUT manager is created)
+static int Mini_LutCreatePi( Mini_Lut_t * p )
+{
+    Mini_LutPush( p, 0, NULL, NULL );
+    return p->nSize - 1;
+}
+static int Mini_LutCreatePo( Mini_Lut_t * p, int Var0 )
+{
+    assert( Var0 >= 0 && Var0 < p->nSize );
+    Mini_LutPush( p, 1, &Var0, NULL );
+    // mark PO by setting its 2nd fanin to the special number
+    p->pArray[p->LutSize*(p->nSize - 1)+1] = MINI_LUT_NULL2;
+    return p->nSize - 1;
+}
+
+// create LUT
+static int Mini_LutCreateNode( Mini_Lut_t * p, int nVars, int * pVars, unsigned * pTruth )
+{
+    assert( nVars >= 0 && nVars <= p->LutSize );
+    Mini_LutPush( p, nVars, pVars, pTruth );
+    return p->nSize - 1;
+}
+
+// procedure to check the topological order during AIG construction
+static int Mini_LutCheck( Mini_Lut_t * p )
+{
+    int status = 1;
+    int i, k, iFaninVar;
+    Mini_LutForEachNode( p, i )
+    {
+        for ( k = 0; k < p->LutSize; k++ )
+        {
+            iFaninVar = Mini_LutNodeFanin( p, i, k );
+            if ( iFaninVar == MINI_LUT_NULL )
+                continue;
+            if ( iFaninVar >= p->LutSize * i )
+                printf( "Fanin %d of LUT node %d is not in a topological order.\n", k, i ), status = 0;
+        }
+    }
+    Mini_LutForEachPo( p, i )
+    {
+        iFaninVar = Mini_LutNodeFanin( p, i, 0 );
+        if ( iFaninVar >= p->LutSize * i )
+            printf( "Fanin %d of PO node %d is not in a topological order.\n", k, i ), status = 0;
+    }
+    return status;
+}
+
+
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+ABC_NAMESPACE_HEADER_END
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 1fdffd77..9f04926d 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -12074,8 +12074,6 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     {
 //        extern void Cba_PrsReadBlifTest();
 //        Cba_PrsReadBlifTest();
-        extern void Sfm_TimTest( Abc_Ntk_t * pNtk );
-        Sfm_TimTest( pNtk );
     }
     return 0;
 usage:
@@ -26998,12 +26996,13 @@ int Abc_CommandAbc9Read( Abc_Frame_t * pAbc, int argc, char ** argv )
     char ** pArgvNew;
     char * FileName, * pTemp;
     int c, nArgcNew;
-    int fUseMini = 0;
+    int fMiniAig = 0;
+    int fMiniLut = 0;
     int fVerbose = 0;
     int fGiaSimple = 0;
     int fSkipStrash = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "csmvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "csmlvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -27014,7 +27013,10 @@ int Abc_CommandAbc9Read( Abc_Frame_t * pAbc, int argc, char ** argv )
             fSkipStrash ^= 1;
             break;
         case 'm':
-            fUseMini ^= 1;
+            fMiniAig ^= 1;
+            break;
+        case 'l':
+            fMiniLut ^= 1;
             break;
         case 'v':
             fVerbose ^= 1;
@@ -27047,8 +27049,10 @@ int Abc_CommandAbc9Read( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     fclose( pFile );
 
-    if ( fUseMini )
+    if ( fMiniAig )
         pAig = Gia_ManReadMiniAig( FileName );
+    else if ( fMiniLut )
+        pAig = Gia_ManReadMiniLut( FileName );
 //    else if ( Extra_FileIsType( FileName, ".v", NULL, NULL ) )
 //        Abc3_ReadShowHie( FileName, fSkipStrash );
     else 
@@ -27058,11 +27062,12 @@ int Abc_CommandAbc9Read( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &r [-csmvh] <file>\n" );
+    Abc_Print( -2, "usage: &r [-csmlvh] <file>\n" );
     Abc_Print( -2, "\t         reads the current AIG from the AIGER file\n" );
     Abc_Print( -2, "\t-c     : toggles reading simple AIG [default = %s]\n", fGiaSimple? "yes": "no" );
     Abc_Print( -2, "\t-s     : toggles structural hashing while reading [default = %s]\n", !fSkipStrash? "yes": "no" );
-    Abc_Print( -2, "\t-m     : toggles reading MiniAIG rather than AIGER file [default = %s]\n", fUseMini? "yes": "no" );
+    Abc_Print( -2, "\t-m     : toggles reading MiniAIG rather than AIGER file [default = %s]\n", fMiniAig? "yes": "no" );
+    Abc_Print( -2, "\t-l     : toggles reading MiniLUT rather than AIGER file [default = %s]\n", fMiniLut? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggles additional verbose output [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     Abc_Print( -2, "\t<file> : the file name\n");
@@ -27843,9 +27848,10 @@ int Abc_CommandAbc9Write( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c, nArgcNew;
     int fUnique = 0;
     int fMiniAig = 0;
+    int fMiniLut = 0;
     int fVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "umvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "umlvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -27855,6 +27861,9 @@ int Abc_CommandAbc9Write( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'm':
             fMiniAig ^= 1;
             break;
+        case 'l':
+            fMiniLut ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -27885,15 +27894,18 @@ int Abc_CommandAbc9Write( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     else if ( fMiniAig )
         Gia_ManWriteMiniAig( pAbc->pGia, pFileName );
+    else if ( fMiniLut )
+        Gia_ManWriteMiniLut( pAbc->pGia, pFileName );
     else
         Gia_AigerWrite( pAbc->pGia, pFileName, 0, 0 );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &w [-umvh] <file>\n" );
+    Abc_Print( -2, "usage: &w [-umlvh] <file>\n" );
     Abc_Print( -2, "\t         writes the current AIG into the AIGER file\n" );
     Abc_Print( -2, "\t-u     : toggle writing canonical AIG structure [default = %s]\n", fUnique? "yes" : "no" );
     Abc_Print( -2, "\t-m     : toggle writing MiniAIG rather than AIGER [default = %s]\n", fMiniAig? "yes" : "no" );
+    Abc_Print( -2, "\t-l     : toggle writing MiniLUT rather than AIGER [default = %s]\n", fMiniLut? "yes" : "no" );
     Abc_Print( -2, "\t-v     : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     Abc_Print( -2, "\t<file> : the file name\n");
diff --git a/src/opt/dau/dauGia.c b/src/opt/dau/dauGia.c
index 6489cd86..5e74ad21 100644
--- a/src/opt/dau/dauGia.c
+++ b/src/opt/dau/dauGia.c
@@ -460,7 +460,7 @@ int Dsm_ManTruthToGia( void * p, word * pTruth, Vec_Int_t * vLeaves, Vec_Int_t *
     if ( nSizeNonDec )
         m_NonDsd++;
 //    printf( "%s\n", pDsd );
-    if ( fDelayBalance )
+    if ( fDelayBalance && pGia->vLevels )
         return Dau_DsdToGia( pGia, pDsd, Vec_IntArray(vLeaves), vCover );
     else
         return Dau_DsdToGia2( pGia, pDsd, Vec_IntArray(vLeaves), vCover );