Generation of plain AIG after mapping.

8 files changed, 323 insertions, 6 deletions

diff --git a/abclib.dsp b/abclib.dsp
index 9efdb000..848b2c8a 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -2071,6 +2071,10 @@ SOURCE=.\src\opt\dau\dauEnum.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\opt\dau\dauGia.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\opt\dau\dauInt.h
 # End Source File
 # Begin Source File
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 5a6148d0..eef8675f 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -248,6 +248,7 @@ struct Jf_Par_t_
     int            fCutMin;
     int            fUseTts;
     int            fGenCnf;
+    int            fPureAig;
     int            fVerbose;
     int            fVeryVerbose;
     int            nLutSizeMax;
diff --git a/src/aig/gia/giaJf.c b/src/aig/gia/giaJf.c
index 87a05f2b..8ca16f29 100644
--- a/src/aig/gia/giaJf.c
+++ b/src/aig/gia/giaJf.c
@@ -24,6 +24,7 @@
 #include "misc/extra/extra.h"
 #include "bool/kit/kit.h"
 #include "misc/util/utilTruth.h"
+#include "opt/dau/dau.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -1428,6 +1429,82 @@ void Jf_ManDeriveMapping( Jf_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Derive GIA without mapping.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Jf_ManDeriveGia( Jf_Man_t * p )
+{
+    Gia_Man_t * pNew;
+    Gia_Obj_t * pObj; 
+    Vec_Int_t * vCopies   = Vec_IntStartFull( Gia_ManObjNum(p->pGia) );
+    Vec_Int_t * vCover    = Vec_IntAlloc( 1 << 16 );
+    Vec_Int_t * vLeaves   = Vec_IntAlloc( 16 );
+    int i, k, iLit, Class, * pCut;
+    word uTruth;
+    assert( p->pPars->fCutMin );
+    // create new manager
+    pNew = Gia_ManStart( Gia_ManObjNum(p->pGia) );
+    pNew->pName = Abc_UtilStrsav( p->pGia->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pGia->pSpec );
+    // map primary inputs
+    Vec_IntWriteEntry( vCopies, 0, 0 );
+    Gia_ManForEachCi( p->pGia, pObj, i )
+        Vec_IntWriteEntry( vCopies, Gia_ObjId(p->pGia, pObj), Gia_ManAppendCi(pNew) );
+    // iterate through nodes used in the mapping
+    Gia_ManHashStart( pNew );
+    Gia_ManForEachAnd( p->pGia, pObj, i )
+    {
+       if ( Gia_ObjIsBuf(pObj) || Gia_ObjRefNum(p->pGia, pObj) == 0 )
+            continue;
+        pCut = Jf_ObjCutBest( p, i );
+//        printf( "Best cut of node %d:  ", i );  Jf_CutPrint(pCut);
+        Class = Jf_CutFuncClass( pCut );
+        uTruth = p->pPars->fUseTts ? *Vec_MemReadEntry(p->vTtMem, Class) : Sdm_ManReadDsdTruth(p->pDsd, Class);
+        assert( p->pDsd == NULL || Sdm_ManReadDsdVarNum(p->pDsd, Class) == Jf_CutSize(pCut) );
+        if ( Jf_CutSize(pCut) == 0 )
+        {
+            assert( Class == 0 );
+            Vec_IntWriteEntry( vCopies, i, Jf_CutFunc(pCut) );
+            continue;
+        }
+        if ( Jf_CutSize(pCut) == 1 )
+        {
+            assert( Class == 1 );
+            iLit = Abc_LitNotCond( Jf_CutLit(pCut, 1) , Jf_CutFuncCompl(pCut) );
+            iLit = Abc_Lit2LitL( Vec_IntArray(vCopies), iLit );
+            Vec_IntWriteEntry( vCopies, i, iLit );
+            continue;
+        }
+        // collect leaves
+        Vec_IntClear( vLeaves );
+        Jf_CutForEachLit( pCut, iLit, k )
+            Vec_IntPush( vLeaves, Abc_Lit2LitL(Vec_IntArray(vCopies), iLit) );
+        // create GIA
+        iLit = Dsm_ManDeriveGia( pNew, uTruth, vLeaves, vCover );
+        iLit = Abc_LitNotCond( iLit, Jf_CutFuncCompl(pCut) );
+        Vec_IntWriteEntry( vCopies, i, iLit );
+    }
+    Gia_ManForEachCo( p->pGia, pObj, i )
+    {
+        iLit = Vec_IntEntry( vCopies, Gia_ObjFaninId0p(p->pGia, pObj) );
+        Gia_ManAppendCo( pNew, Abc_LitNotCond(iLit, Gia_ObjFaninC0(pObj)) );
+    }
+    Vec_IntFree( vCopies );
+    Vec_IntFree( vLeaves );
+    Vec_IntFree( vCover );
+    Gia_ManHashStop( pNew );
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p->pGia) );
+    return pNew;
+}
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []
@@ -1451,6 +1528,7 @@ void Jf_ManSetDefaultPars( Jf_Par_t * pPars )
     pPars->fCutMin      =  0;
     pPars->fUseTts      =  0;
     pPars->fGenCnf      =  0;
+    pPars->fPureAig     =  0;
     pPars->fVerbose     =  0;
     pPars->fVeryVerbose =  0;
     pPars->nLutSizeMax  =  JF_LEAF_MAX;
@@ -1491,7 +1569,9 @@ Gia_Man_t * Jf_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pPars )
         Jf_ManPropagateEla( p, 0 );                 Jf_ManPrintStats( p, "Area " );
         Jf_ManPropagateEla( p, 1 );                 Jf_ManPrintStats( p, "Edge " );
     }
-    if ( p->pPars->fCutMin )
+    if ( p->pPars->fPureAig )
+        pNew = Jf_ManDeriveGia(p);
+    else if ( p->pPars->fCutMin )
         pNew = Jf_ManDeriveMappingGia(p);
     else
         Jf_ManDeriveMapping(p);
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 30be411f..10b9e72e 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -29874,11 +29874,10 @@ int Abc_CommandAbc9Jf( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     char Buffer[200];
     Jf_Par_t Pars, * pPars = &Pars;
-    Gia_Man_t * pNew;
-    int c;
+    Gia_Man_t * pNew; int c;
     Jf_ManSetDefaultPars( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "KCRDWaekmtcvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "KCRDWaekmtcgvwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -29961,6 +29960,9 @@ int Abc_CommandAbc9Jf( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'c':
             pPars->fGenCnf ^= 1;
             break;
+        case 'g':
+            pPars->fPureAig ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -29999,7 +30001,7 @@ usage:
         sprintf(Buffer, "best possible" );
     else
         sprintf(Buffer, "%d", pPars->DelayTarget );
-    Abc_Print( -2, "usage: &jf [-KCRDW num] [-akmtcvwh]\n" );
+    Abc_Print( -2, "usage: &jf [-KCRDW num] [-akmtcgvwh]\n" );
     Abc_Print( -2, "\t           performs technology mapping of the network\n" );
     Abc_Print( -2, "\t-K num   : LUT size for the mapping (2 <= K <= %d) [default = %d]\n", pPars->nLutSizeMax, pPars->nLutSize );
     Abc_Print( -2, "\t-C num   : the max number of priority cuts (1 <= C <= %d) [default = %d]\n", pPars->nCutNumMax, pPars->nCutNum );
@@ -30012,6 +30014,7 @@ usage:
     Abc_Print( -2, "\t-m       : toggles cut minimization [default = %s]\n", pPars->fCutMin? "yes": "no" );
     Abc_Print( -2, "\t-t       : toggles truth tables for minimization [default = %s]\n", pPars->fUseTts? "yes": "no" );
     Abc_Print( -2, "\t-c       : toggles mapping for CNF generation [default = %s]\n", pPars->fGenCnf? "yes": "no" );
+    Abc_Print( -2, "\t-g       : toggles generating AIG without mapping [default = %s]\n", pPars->fPureAig? "yes": "no" );
     Abc_Print( -2, "\t-v       : toggles verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-w       : toggles very verbose output [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h       : prints the command usage\n");
diff --git a/src/opt/dau/dau.h b/src/opt/dau/dau.h
index 0f332b26..0ee50007 100644
--- a/src/opt/dau/dau.h
+++ b/src/opt/dau/dau.h
@@ -87,6 +87,9 @@ extern int           Dau_DsdCountAnds( char * pDsd );
 extern void          Dau_DsdTruthCompose_rec( word * pFunc, word pFanins[DAU_MAX_VAR][DAU_MAX_WORD], word * pRes, int nVars, int nWordsR );
 extern int           Dau_DsdCheck1Step( word * pTruth, int nVarsInit );
 
+/*=== dauGia.c  ==========================================================*/
+extern int           Dsm_ManDeriveGia( void * p, word uTruth, Vec_Int_t * vLeaves, Vec_Int_t * vCover );
+
 /*=== dauMerge.c  ==========================================================*/
 extern void          Dau_DsdRemoveBraces( char * pDsd, int * pMatches );
 extern char *        Dau_DsdMerge( char * pDsd0i, int * pPerm0, char * pDsd1i, int * pPerm1, int fCompl0, int fCompl1, int nVars );
diff --git a/src/opt/dau/dauDsd.c b/src/opt/dau/dauDsd.c
index 2aeeb958..05cfc485 100644
--- a/src/opt/dau/dauDsd.c
+++ b/src/opt/dau/dauDsd.c
@@ -1021,7 +1021,7 @@ static inline int Dau_DsdWritePrime( Dau_Dsd_t * p, word * pTruth, int * pVars,
             int nNonDecSize;
             // compose the result
             Dau_DsdWriteString( p, "<" );
-            Dau_DsdWriteVar( p, pVars[vBest], 0 );
+            Dau_DsdWriteVar( p, vBest, 0 );
             // split decomposition
             Abc_TtCofactor1p( pCofTemp, pTruth, nWords, vBest );
             nNonDecSize = Dau_DsdDecompose( pCofTemp, nVars, 0, p->fWriteTruth, pRes );
diff --git a/src/opt/dau/dauGia.c b/src/opt/dau/dauGia.c
new file mode 100644
index 00000000..4ced55e6
--- /dev/null
+++ b/src/opt/dau/dauGia.c
@@ -0,0 +1,225 @@
+/**CFile****************************************************************
+
+  FileName    [dauGia.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [DAG-aware unmapping.]
+
+  Synopsis    [Coverting DSD into GIA.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: dauGia.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "dauInt.h"
+#include "aig/gia/gia.h"
+#include "misc/util/utilTruth.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+extern int Kit_TruthToGia( Gia_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t * vMemory, Vec_Int_t * vLeaves, int fHash );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+ 
+/**Function*************************************************************
+
+  Synopsis    [Derives GIA for the truth table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Dau_DsdToGiaCompose_rec( Gia_Man_t * pGia, word Func, int * pFanins, int nVars )
+{
+    int t0, t1;
+    if ( Func == 0 )
+        return 0;
+    if ( Func == ~(word)0 )
+        return 1;
+    assert( nVars > 0 );
+    if ( --nVars == 0 )
+    {
+        assert( Func == s_Truths6[0] || Func == s_Truths6Neg[0] );
+        return Abc_LitNotCond( pFanins[0], (int)(Func == s_Truths6Neg[0]) );
+    }
+    if ( !Abc_Tt6HasVar(Func, nVars) )
+        return Dau_DsdToGiaCompose_rec( pGia, Func, pFanins, nVars );
+    t0 = Dau_DsdToGiaCompose_rec( pGia, Abc_Tt6Cofactor0(Func, nVars), pFanins, nVars );
+    t1 = Dau_DsdToGiaCompose_rec( pGia, Abc_Tt6Cofactor1(Func, nVars), pFanins, nVars );
+    return Gia_ManHashMux( pGia, pFanins[nVars], t1, t0 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives GIA for the DSD formula.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Dau_DsdToGia_rec( Gia_Man_t * pGia, char * pStr, char ** p, int * pMatches, int * pLits, Vec_Int_t * vCover )
+{
+    int fCompl = 0;
+    if ( **p == '!' )
+        (*p)++, fCompl = 1;
+    if ( **p >= 'a' && **p <= 'f' ) // var
+    {
+        assert( **p - 'a' >= 0 && **p - 'a' < 6 );
+        return Abc_LitNotCond( pLits[**p - 'a'], fCompl );
+    }
+    if ( **p == '(' ) // and/or
+    {
+        char * q = pStr + pMatches[ *p - pStr ];
+        int Res = 1, Lit;
+        assert( **p == '(' && *q == ')' );
+        for ( (*p)++; *p < q; (*p)++ )
+        {
+            Lit = Dau_DsdToGia_rec( pGia, pStr, p, pMatches, pLits, vCover );
+            Res = Gia_ManHashAnd( pGia, Res, Lit );
+        }
+        assert( *p == q );
+        return Abc_LitNotCond( Res, fCompl );
+    }
+    if ( **p == '[' ) // xor
+    {
+        char * q = pStr + pMatches[ *p - pStr ];
+        int Res = 0, Lit;
+        assert( **p == '[' && *q == ']' );
+        for ( (*p)++; *p < q; (*p)++ )
+        {
+            Lit = Dau_DsdToGia_rec( pGia, pStr, p, pMatches, pLits, vCover );
+            Res = Gia_ManHashXor( pGia, Res, Lit );
+        }
+        assert( *p == q );
+        return Abc_LitNotCond( Res, fCompl );
+    }
+    if ( **p == '<' ) // mux
+    {
+        int nVars = 0;
+        int Temp[3], * pTemp = Temp, Res;
+        int Fanins[6], * pLits2;
+        char * pOld = *p;
+        char * q = pStr + pMatches[ *p - pStr ];
+        // read fanins
+        if ( *(q+1) == '{' )
+        {
+            char * q2;
+            *p = q+1;
+            q2 = pStr + pMatches[ *p - pStr ];
+            assert( **p == '{' && *q2 == '}' );
+            for ( nVars = 0, (*p)++; *p < q2; (*p)++, nVars++ )
+                Fanins[nVars] = Dau_DsdToGia_rec( pGia, pStr, p, pMatches, pLits, vCover );
+            assert( *p == q2 );
+            pLits2 = Fanins;
+        }
+        else
+            pLits2 = pLits;
+        // read MUX
+        *p = pOld;
+        q = pStr + pMatches[ *p - pStr ];
+        assert( **p == '<' && *q == '>' );
+        // verify internal variables
+        if ( nVars )
+            for ( ; pOld < q; pOld++ )
+                if ( *pOld >= 'a' && *pOld <= 'z' )
+                    assert( *pOld - 'a' < nVars );
+        // derive MUX components
+        for ( (*p)++; *p < q; (*p)++ )
+            *pTemp++ = Dau_DsdToGia_rec( pGia, pStr, p, pMatches, pLits2, vCover );
+        assert( pTemp == Temp + 3 );
+        assert( *p == q );
+        if ( *(q+1) == '{' ) // and/or
+        {
+            char * q = pStr + pMatches[ ++(*p) - pStr ];
+            assert( **p == '{' && *q == '}' );
+            *p = q;
+        }
+        Res = Gia_ManHashMux( pGia, Temp[0], Temp[1], Temp[2] );
+        return Abc_LitNotCond( Res, fCompl );
+    }
+    if ( (**p >= 'A' && **p <= 'F') || (**p >= '0' && **p <= '9') )
+    {
+        word Func;
+        int Fanins[6], Res; 
+        Vec_Int_t vLeaves;
+        char * q;
+        int i, nVars = Abc_TtReadHex( &Func, *p );
+        *p += Abc_TtHexDigitNum( nVars );
+        q = pStr + pMatches[ *p - pStr ];
+        assert( **p == '{' && *q == '}' );
+        for ( i = 0, (*p)++; *p < q; (*p)++, i++ )
+            Fanins[i] = Dau_DsdToGia_rec( pGia, pStr, p, pMatches, pLits, vCover );
+        assert( i == nVars );
+        assert( *p == q );
+//        Res = Dau_DsdToGiaCompose_rec( pGia, Func, Fanins, nVars );
+        vLeaves.nCap = nVars;
+        vLeaves.nSize = nVars;
+        vLeaves.pArray = Fanins;        
+        Res = Kit_TruthToGia( pGia, (unsigned *)&Func, nVars, vCover, &vLeaves, 1 );
+        return Abc_LitNotCond( Res, fCompl );
+    }
+    assert( 0 );
+    return 0;
+}
+int Dau_DsdToGia( Gia_Man_t * pGia, char * p, int * pLits, Vec_Int_t * vCover )
+{
+    int Res;
+    if ( *p == '0' && *(p+1) == 0 )
+        Res = 0;
+    else if ( *p == '1' && *(p+1) == 0 )
+        Res = 1;
+    else
+        Res = Dau_DsdToGia_rec( pGia, p, &p, Dau_DsdComputeMatches(p), pLits, vCover );
+    assert( *++p == 0 );
+    return Res;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Convert TT to GIA via DSD.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Dsm_ManDeriveGia( void * p, word uTruth, Vec_Int_t * vLeaves, Vec_Int_t * vCover )
+{
+    Gia_Man_t * pGia = (Gia_Man_t *)p;
+    char pDsd[1000];
+    int nSizeNonDec;
+//    static int Counter = 0; Counter++;
+    nSizeNonDec = Dau_DsdDecompose( &uTruth, Vec_IntSize(vLeaves), 1, 1, pDsd );
+//    printf( "%s\n", pDsd );
+    return Dau_DsdToGia( pGia, pDsd, Vec_IntArray(vLeaves), vCover );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/opt/dau/module.make b/src/opt/dau/module.make
index 5a3df1d5..f339810b 100644
--- a/src/opt/dau/module.make
+++ b/src/opt/dau/module.make
@@ -3,5 +3,6 @@ SRC +=    src/opt/dau/dauCanon.c \
     src/opt/dau/dauDivs.c \
     src/opt/dau/dauDsd.c \
     src/opt/dau/dauEnum.c \
+    src/opt/dau/dauGia.c \
     src/opt/dau/dauMerge.c \
     src/opt/dau/dauTree.c