New choice computation.

3 files changed, 197 insertions, 22 deletions

diff --git a/src/aig/gia/giaScript.c b/src/aig/gia/giaScript.c
index cf58f794..475dfea7 100644
--- a/src/aig/gia/giaScript.c
+++ b/src/aig/gia/giaScript.c
@@ -18,9 +18,11 @@
 
 ***********************************************************************/
 
-#include "gia.h"
+#include "giaAig.h"
 #include "base/main/main.h"
 #include "base/cmd/cmd.h"
+#include "proof/dch/dch.h"
+#include "opt/dau/dau.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -346,6 +348,35 @@ void Gia_ManPerformFlow( int fIsMapped, int nAnds, int nLevels, int nLutSize, in
 
 /**Function*************************************************************
 
+  Synopsis    [Duplicates the AIG manager.]
+
+  Description [This duplicator works for AIGs with choices.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Gia_ManOrderPios( Aig_Man_t * p, Gia_Man_t * pOrder )
+{
+    Vec_Ptr_t * vPios;
+    Gia_Obj_t * pObj;
+    int i;
+    assert( Aig_ManCiNum(p) == Gia_ManCiNum(pOrder) );
+    assert( Aig_ManCoNum(p) == Gia_ManCoNum(pOrder) );
+    vPios = Vec_PtrAlloc( Aig_ManCiNum(p) + Aig_ManCoNum(p) );
+    Gia_ManForEachObj( pOrder, pObj, i )
+    {
+        if ( Gia_ObjIsCi(pObj) )
+            Vec_PtrPush( vPios, Aig_ManCi(p, Gia_ObjCioId(pObj)) );
+        else if ( Gia_ObjIsCo(pObj) )
+            Vec_PtrPush( vPios, Aig_ManCo(p, Gia_ObjCioId(pObj)) );
+    }
+    return vPios;
+}
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []
@@ -355,9 +386,98 @@ void Gia_ManPerformFlow( int fIsMapped, int nAnds, int nLevels, int nLutSize, in
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Gia_ManAigSynch2( Gia_Man_t * p, int fVerbose )
+Gia_Man_t * Gia_ManAigSynch2Choices( Gia_Man_t * pGia1, Gia_Man_t * pGia2, Gia_Man_t * pGia3, Dch_Pars_t * pPars )
+{
+    Aig_Man_t * pMan, * pTemp;
+    Gia_Man_t * pGia, * pMiter;
+    // derive miter
+    Vec_Ptr_t * vPios, * vGias = Vec_PtrAlloc( 3 );
+    if ( pGia3 ) Vec_PtrPush( vGias, pGia3 );
+    if ( pGia2 ) Vec_PtrPush( vGias, pGia2 );
+    if ( pGia1 ) Vec_PtrPush( vGias, pGia1 );
+    pMiter = Gia_ManChoiceMiter( vGias );
+    Vec_PtrFree( vGias );
+    // transform into an AIG
+    pMan = Gia_ManToAigSkip( pMiter, 3 );
+    Gia_ManStop( pMiter );
+    // compute choices
+    pMan = Dch_ComputeChoices( pTemp = pMan, pPars );
+    Aig_ManStop( pTemp );
+    // reconstruct the network
+    vPios = Gia_ManOrderPios( pMan, pGia1 ); 
+    pMan = Aig_ManDupDfsGuided( pTemp = pMan, vPios );
+    Aig_ManStop( pTemp );
+    Vec_PtrFree( vPios );
+    // convert to GIA
+    pGia = Gia_ManFromAigChoices( pMan );
+    Aig_ManStop( pMan );
+    return pGia;
+}
+Gia_Man_t * Gia_ManAigSynch2( Gia_Man_t * pInit, void * pPars0, int nLutSize )
 {
-    return NULL;
+    extern Gia_Man_t * Gia_ManLutBalance( Gia_Man_t * p, int nLutSize, int fUseMuxes, int fRecursive, int fOptArea, int fVerbose );
+    Dch_Pars_t * pParsDch = (Dch_Pars_t *)pPars0;
+    Gia_Man_t * pGia1, * pGia2, * pGia3, * pNew, * pTemp;
+    int fVerbose = pParsDch->fVerbose;
+    Jf_Par_t Pars, * pPars = &Pars;
+    Lf_ManSetDefaultPars( pPars );
+    pPars->fCutMin     = 1;
+    pPars->fCoarsen    = 1;
+    pPars->nRelaxRatio = 20;
+    pPars->nAreaTuner  = 1;
+    pPars->nCutNum     = 4;
+    pPars->fVerbose    = fVerbose;
+    if ( fVerbose )  Gia_ManPrintStats( pInit, NULL );
+    pGia1 = Gia_ManDup( pInit );
+    if ( Gia_ManAndNum(pGia1) == 0 )
+    {
+        Gia_ManTransferTiming( pGia1, pInit );
+        return pGia1;
+    }
+    if ( pGia1->pManTime && pGia1->vLevels == NULL )
+        Gia_ManLevelWithBoxes( pGia1 );
+    // unmap if mapped
+    if ( Gia_ManHasMapping(pInit) )
+    {
+        Gia_ManTransferMapping( pGia1, pInit );
+        pGia1 = (Gia_Man_t *)Dsm_ManDeriveGia( pTemp = pGia1, 0 );
+        Gia_ManStop( pTemp );
+    }
+    // perform LUT balancing
+    pGia2 = Gia_ManLutBalance( pGia1, nLutSize, 1, 1, 1, 0 );
+    // perform balancing
+    pGia2 = Gia_ManAreaBalance( pTemp = pGia2, 0, ABC_INFINITY, 0, 0 );
+    if ( fVerbose )     Gia_ManPrintStats( pGia2, NULL );
+    Gia_ManStop( pTemp );
+    // perform mapping
+    pGia2 = Lf_ManPerformMapping( pTemp = pGia2, pPars );
+    if ( fVerbose )     Gia_ManPrintStats( pGia2, NULL );
+    if ( pTemp != pGia2 )
+        Gia_ManStop( pTemp );
+    // perform balancing
+    if ( pParsDch->fLightSynth )
+        pGia3 = Gia_ManAreaBalance( pGia2, 0, ABC_INFINITY, 0, 0 );
+    else
+    {
+        pGia2 = Gia_ManAreaBalance( pTemp = pGia2, 0, ABC_INFINITY, 0, 0 );
+        if ( fVerbose )     Gia_ManPrintStats( pGia2, NULL );
+        Gia_ManStop( pTemp );
+        // perform DSD balancing
+        pGia3 = Gia_ManPerformDsdBalance( pGia2, 6, 8, 0, 0 );
+    }
+    if ( fVerbose )     Gia_ManPrintStats( pGia3, NULL );
+    // perform choice computation
+    pNew = Gia_ManAigSynch2Choices( pGia1, pGia2, pGia3, pParsDch );
+    Gia_ManStop( pGia1 );
+    Gia_ManStop( pGia2 );
+    Gia_ManStop( pGia3 );
+    // copy names
+    ABC_FREE( pNew->pName );
+    ABC_FREE( pNew->pSpec );
+    pNew->pName = Abc_UtilStrsav(pInit->pName);
+    pNew->pSpec = Abc_UtilStrsav(pInit->pSpec);
+    Gia_ManTransferTiming( pNew, pInit );
+    return pNew;
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index ca7be1d9..dad29ae5 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -28453,16 +28453,66 @@ usage:
 ***********************************************************************/
 int Abc_CommandAbc9Synch2( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    extern Gia_Man_t * Gia_ManAigSynch2( Gia_Man_t * p, int fVerbose );
+    extern Gia_Man_t * Gia_ManAigSynch2( Gia_Man_t * p, void * pPars, int nLutSize );
     Gia_Man_t * pTemp;
-    int c, fVerbose  =  0;
+    Dch_Pars_t Pars, * pPars = &Pars;
+    int c, nLutSize = 6;
+    // set defaults
+    Dch_ManSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "WCSKfvh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'W':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-W\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nWords = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nWords < 0 )
+                goto usage;
+            break;
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nBTLimit = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nBTLimit < 0 )
+                goto usage;
+            break;
+        case 'S':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nSatVarMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nSatVarMax < 0 )
+                goto usage;
+            break;
+        case 'K':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-K\" should be followed by a char string.\n" );
+                goto usage;
+            }
+            nLutSize = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nLutSize < 0 )
+                goto usage;
+            break;
+        case 'f':
+            pPars->fLightSynth ^= 1;
+            break;
         case 'v':
-            fVerbose ^= 1;
+            pPars->fVerbose ^= 1;
             break;
         case 'h':
             goto usage;
@@ -28472,18 +28522,23 @@ int Abc_CommandAbc9Synch2( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( pAbc->pGia == NULL )
     {
-        Abc_Print( -1, "Abc_CommandAbc9Synch2(): There is no AIG.\n" );
+        Abc_Print( -1, "Abc_CommandAbc9Dch(): There is no AIG.\n" );
         return 1;
     }
-    pTemp = Gia_ManAigSynch2( pAbc->pGia, fVerbose );
+    pTemp = Gia_ManAigSynch2( pAbc->pGia, pPars, nLutSize );
     Abc_FrameUpdateGia( pAbc, pTemp );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &synch2 [-vh]\n" );
-    Abc_Print( -2, "\t           performs synthesis and computes structural choices\n" );
-    Abc_Print( -2, "\t-v       : toggles printing additional information [default = %s]\n", fVerbose? "yes": "no" );
-    Abc_Print( -2, "\t-h       : print the command usage\n");
+    Abc_Print( -2, "usage: &synch2 [-WCSK num] [-fvh]\n" );
+    Abc_Print( -2, "\t         computes structural choices using a new approach\n" );
+    Abc_Print( -2, "\t-W num : the max number of simulation words [default = %d]\n", pPars->nWords );
+    Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
+    Abc_Print( -2, "\t-S num : the max number of SAT variables [default = %d]\n", pPars->nSatVarMax );
+    Abc_Print( -2, "\t-K num : the target LUT size for downstream mapping [default = %d]\n", nLutSize );
+    Abc_Print( -2, "\t-f     : toggle using lighter logic synthesis [default = %s]\n", pPars->fLightSynth? "yes": "no" );
+    Abc_Print( -2, "\t-v     : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
 }
 
diff --git a/src/map/if/ifTune.c b/src/map/if/ifTune.c
index d21ebad0..400520e6 100644
--- a/src/map/if/ifTune.c
+++ b/src/map/if/ifTune.c
@@ -394,14 +394,14 @@ void Ift_TtComparisonConstr( word * pTruth, int nVars, int fMore, int fEqual )
 {
     word Cond[4], Equa[4], Temp[4];
     word s_TtElems[8][4] = {
-        ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),
-        ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),
-        ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),
-        ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),
-        ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),
-        ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),
-        ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),
-        ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF)
+        { ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA) },
+        { ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC) },
+        { ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0) },
+        { ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00) },
+        { ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000) },
+        { ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000) },
+        { ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF) },
+        { ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF) }
     };
     int i, nWords = Abc_TtWordNum(2*nVars);
     assert( nVars > 0 && nVars <= 4 );
@@ -528,7 +528,7 @@ int Ift_NtkAddClauses( Ift_Ntk_t * p, int * pValues, sat_solver * pSat )
     int nSatVars = sat_solver_nvars(pSat);
     for ( i = 0; i < p->nObjs-1; i++ )
         p->Nodes[i].Var = nSatVars++;
-    p->Nodes[p->nObjs-1].Var = -ABC_INFINITY;
+    p->Nodes[p->nObjs-1].Var = 0xFFFF;
     sat_solver_setnvars( pSat, nSatVars );
     // verify variable values
     for ( i = 0; i < p->nVars; i++ )