Version abc80729

16 files changed, 1079 insertions, 10 deletions

diff --git a/src/aig/dch/dch.h b/src/aig/dch/dch.h
new file mode 100644
index 00000000..a9949821
--- /dev/null
+++ b/src/aig/dch/dch.h
@@ -0,0 +1,72 @@
+/**CFile****************************************************************
+
+  FileName    [dch.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Choice computation for tech-mapping.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 29, 2008.]
+
+  Revision    [$Id: dch.h,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef __DCH_H__
+#define __DCH_H__
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+// choicing parameters
+typedef struct Dch_Pars_t_ Dch_Pars_t;
+struct Dch_Pars_t_
+{
+    int              nWords;       // the number of simulation words
+    int              nBTLimit;     // conflict limit at a node
+    int              nSatVarMax;   // the max number of SAT variables
+    int              fVerbose;     // verbose stats
+};
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== dchCore.c ==========================================================*/
+extern void             Dch_ManSetDefaultParams( Dch_Pars_t * p );
+extern Aig_Man_t *      Dch_ComputeChoices( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars );
+
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/aig/dch/dchAig.c b/src/aig/dch/dchAig.c
new file mode 100644
index 00000000..31b1eea3
--- /dev/null
+++ b/src/aig/dch/dchAig.c
@@ -0,0 +1,186 @@
+/**CFile****************************************************************
+
+  FileName    [dchAig.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Choice computation for tech-mapping.]
+
+  Synopsis    [AIG manipulation.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 29, 2008.]
+
+  Revision    [$Id: dchAig.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "dchInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the cumulative AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dch_DeriveTotalAig_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+    if ( pObj->pData )
+        return;
+    Dch_DeriveTotalAig_rec( p, Aig_ObjFanin0(pObj) );
+    Dch_DeriveTotalAig_rec( p, Aig_ObjFanin1(pObj) );
+    pObj->pData = Aig_And( p, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the cumulative AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Dch_DeriveTotalAig( Vec_Ptr_t * vAigs )
+{
+    Aig_Man_t * pAig, * pAig2, * pAigTotal;
+    Aig_Obj_t * pObj, * pObjPi, * pObjPo;
+    int i, k, nNodes;
+    assert( Vec_PtrSize(vAigs) > 0 );
+    // make sure they have the same number of PIs/POs
+    nNodes = 0;
+    pAig = Vec_PtrEntry( vAigs, 0 );
+    Vec_PtrForEachEntry( vAigs, pAig2, i )
+    {
+        assert( Aig_ManPiNum(pAig) == Aig_ManPiNum(pAig2) );
+        assert( Aig_ManPoNum(pAig) == Aig_ManPoNum(pAig2) );
+        nNodes += Aig_ManNodeNum(pAig);
+        Aig_ManCleanData( pAig2 );
+    }
+    // map constant nodes
+    pAigTotal = Aig_ManStart( nNodes );
+    Vec_PtrForEachEntry( vAigs, pAig2, k )
+        Aig_ManConst1(pAig2)->pData = Aig_ManConst1(pAigTotal);
+    // map primary inputs
+    Aig_ManForEachPi( pAig, pObj, i )
+    {
+        pObjPi = Aig_ObjCreatePi( pAigTotal );
+        Vec_PtrForEachEntry( vAigs, pAig2, k )
+            Aig_ManPi( pAig2, i )->pData = pObjPi;
+    }
+    // construct the AIG in the order of POs
+    Aig_ManForEachPo( pAig, pObj, i )
+    {
+        Vec_PtrForEachEntry( vAigs, pAig2, k )
+        {
+            pObjPo = Aig_ManPo( pAig2, i );
+            Dch_DeriveTotalAig_rec( pAigTotal, Aig_ObjFanin0(pObjPo) );
+        }
+        Aig_ObjCreatePo( pAigTotal, Aig_ObjChild0Copy(pObj) );
+    }
+    // mark the cone of the first AIG
+    Aig_ManIncrementTravId( pAigTotal );
+    Aig_ManForEachObj( pAig, pObj, i )
+        if ( pObj->pData ) 
+            Aig_ObjSetTravIdCurrent( pAigTotal, pObj->pData );
+    // cleanup should not be done
+    return pAigTotal;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the AIG with choices from representatives.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dch_DeriveChoiceAig_rec( Aig_Man_t * pNew, Aig_Man_t * pOld, Aig_Obj_t * pObj )
+{
+    Aig_Obj_t * pRepr, * pObjNew, * pReprNew;
+    if ( pObj->pData )
+        return;
+    // construct AIG for the representative
+    pRepr = pOld->pReprs[pObj->Id];
+    if ( pRepr != NULL )
+        Dch_DeriveChoiceAig_rec( pNew, pOld, pRepr );
+    // skip choices with combinatinal loops
+    if ( Aig_ObjCheckTfi( pOld, pObj, pRepr ) )
+    {
+        pOld->pReprs[pObj->Id] = NULL;
+        return;
+    }
+    Dch_DeriveChoiceAig_rec( pNew, pOld, Aig_ObjFanin0(pObj) );
+    Dch_DeriveChoiceAig_rec( pNew, pOld, Aig_ObjFanin1(pObj) );
+    pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+    if ( pRepr == NULL )
+        return;
+    // add choice
+    assert( pObj->nRefs == 0 );
+    pObjNew = pObj->pData;
+    pReprNew = pRepr->pData;
+    pNew->pEquivs[pObjNew->Id] = pNew->pEquivs[pReprNew->Id];
+    pNew->pEquivs[pReprNew->Id] = pObjNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the AIG with choices from representatives.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Dch_DeriveChoiceAig( Aig_Man_t * pAig )
+{
+    Aig_Man_t * pChoices;
+    Aig_Obj_t * pObj;
+    int i;
+    // start recording equivalences
+    pChoices = Aig_ManStart( Aig_ManObjNumMax(pAig) );
+    pChoices->pEquivs = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) );
+    // map constants and PIs
+    Aig_ManCleanData( pAig );
+    Aig_ManConst1(pAig)->pData = Aig_ManConst1(pChoices);
+    Aig_ManForEachPi( pAig, pObj, i )
+        pObj->pData = Aig_ObjCreatePi( pChoices );
+     // construct choice nodes from the POs
+    assert( pAig->pReprs != NULL );
+    Aig_ManForEachPo( pAig, pObj, i )
+    {
+        Dch_DeriveChoiceAig_rec( pChoices, pAig, Aig_ObjFanin0(pObj) );
+        Aig_ObjCreatePo( pChoices, Aig_ObjChild0Copy(pObj) );
+    }
+    // there is no need for cleanup
+    return pChoices;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/dch/dchCore.c b/src/aig/dch/dchCore.c
new file mode 100644
index 00000000..cdac853f
--- /dev/null
+++ b/src/aig/dch/dchCore.c
@@ -0,0 +1,98 @@
+/**CFile****************************************************************
+
+  FileName    [dchCore.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Choice computation for tech-mapping.]
+
+  Synopsis    [The core procedures.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 29, 2008.]
+
+  Revision    [$Id: dchCore.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "dchInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [This procedure sets default parameters.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dch_ManSetDefaultParams( Dch_Pars_t * p )
+{
+    memset( p, 0, sizeof(Dch_Pars_t) );
+    p->nWords     =     4;    // the number of simulation words
+    p->nBTLimit   =  1000;    // conflict limit at a node
+    p->nSatVarMax =  5000;    // the max number of SAT variables
+    p->fVerbose   =     1;    // verbose stats
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs computation of AIGs with choices.]
+
+  Description [Takes several AIGs and performs choicing.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Dch_ComputeChoices( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars )
+{
+    Dch_Man_t * p;
+    Aig_Man_t * pResult;
+    int i;
+
+    assert( Vec_PtrSize(vAigs) > 0 );
+
+    printf( "AIGs considered for choicing:\n" );
+    Vec_PtrForEachEntry( vAigs, pResult, i )
+    {
+        Aig_ManPrintStats( pResult );
+    }
+
+    // start the choicing manager
+    p = Dch_ManCreate( vAigs, pPars );
+    // compute candidate equivalence classes
+    p->ppClasses = Dch_CreateCandEquivClasses( p->pAigTotal, pPars->nWords, pPars->fVerbose );
+
+    
+
+
+
+    // create choices
+//    pResult = Dch_DeriveChoiceAig( p->pAigTotal );
+    Aig_ManCleanup( p->pAigTotal );
+    pResult = Aig_ManDupSimpleDfs( p->pAigTotal );
+
+    Dch_ManStop( p );
+    return pResult;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/dch/dchInt.h b/src/aig/dch/dchInt.h
new file mode 100644
index 00000000..e35f8111
--- /dev/null
+++ b/src/aig/dch/dchInt.h
@@ -0,0 +1,102 @@
+/**CFile****************************************************************
+
+  FileName    [dchInt.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Choice computation for tech-mapping.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 29, 2008.]
+
+  Revision    [$Id: dchInt.h,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef __DCH_INT_H__
+#define __DCH_INT_H__
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include "aig.h"
+#include "satSolver.h"
+#include "dch.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+// equivalence classes
+typedef struct Dch_Cla_t_ Dch_Cla_t;
+struct Dch_Cla_t_
+{
+    int              nNodes;       // the number of nodes in the class
+    int              pNodes[0];    // the nodes of the class
+};
+
+// choicing manager
+typedef struct Dch_Man_t_ Dch_Man_t;
+struct Dch_Man_t_
+{
+    // parameters
+    Dch_Pars_t *     pPars;
+    // AIGs used in the package
+    Vec_Ptr_t *      vAigs;        // user-given AIGs
+    Aig_Man_t *      pAigTotal;    // intermediate AIG
+    Aig_Man_t *      pAigFraig;    // final AIG
+    // equivalence classes
+    Dch_Cla_t **     ppClasses;    // classes for representative nodes
+    // SAT solving
+    sat_solver *     pSat;         // recyclable SAT solver
+    Vec_Int_t **     ppSatVars;    // SAT variables for used nodes
+    Vec_Ptr_t *      vUsedNodes;   // nodes whose SAT vars are assigned
+    // runtime stats
+};
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== dchAig.c =====================================================*/
+extern Aig_Man_t *     Dch_DeriveTotalAig( Vec_Ptr_t * vAigs );
+extern Aig_Man_t *     Dch_DeriveChoiceAig( Aig_Man_t * pAig );
+
+/*=== dchMan.c =====================================================*/
+extern Dch_Man_t *     Dch_ManCreate( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars );
+extern void            Dch_ManStop( Dch_Man_t * p );
+
+/*=== dchSat.c =====================================================*/
+ 
+/*=== dchSim.c =====================================================*/
+extern Dch_Cla_t **    Dch_CreateCandEquivClasses( Aig_Man_t * pAig, int nWords, int fVerbose );
+
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/aig/dch/dchMan.c b/src/aig/dch/dchMan.c
new file mode 100644
index 00000000..2fc739f1
--- /dev/null
+++ b/src/aig/dch/dchMan.c
@@ -0,0 +1,102 @@
+/**CFile****************************************************************
+
+  FileName    [dchMan.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Computation of equivalence classes using simulation.]
+
+  Synopsis    [Calls to the SAT solver.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 29, 2008.]
+
+  Revision    [$Id: dchMan.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "dchInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the interpolation manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Dch_Man_t * Dch_ManCreate( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars )
+{
+    Dch_Man_t * p;
+    // create interpolation manager
+    p = ALLOC( Dch_Man_t, 1 );
+    memset( p, 0, sizeof(Dch_Man_t) );
+    p->pPars      = pPars;
+    // AIGs
+    p->vAigs      = vAigs;
+    p->pAigTotal  = Dch_DeriveTotalAig( vAigs );
+    // equivalence classes
+    Aig_ManReprStart( p->pAigTotal, Aig_ManObjNumMax(p->pAigTotal) );
+    // SAT solving
+    p->ppSatVars  = CALLOC( Vec_Int_t *, Aig_ManObjNumMax(p->pAigTotal) );
+    p->vUsedNodes = Vec_PtrAlloc( 1000 );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Frees the interpolation manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dch_ManStop( Dch_Man_t * p )
+{
+    if ( p->pPars->fVerbose )
+    {
+/*
+        p->timeOther = p->timeTotal-p->timeRwr-p->timeCnf-p->timeSat-p->timeInt-p->timeEqu;
+        printf( "Runtime statistics:\n" );
+        PRTP( "Rewriting  ", p->timeRwr,   p->timeTotal );
+        PRTP( "CNF mapping", p->timeCnf,   p->timeTotal );
+        PRTP( "SAT solving", p->timeSat,   p->timeTotal );
+        PRTP( "Interpol   ", p->timeInt,   p->timeTotal );
+        PRTP( "Containment", p->timeEqu,   p->timeTotal );
+        PRTP( "Other      ", p->timeOther, p->timeTotal );
+        PRTP( "TOTAL      ", p->timeTotal, p->timeTotal );
+*/
+    }
+    if ( p->pAigTotal )
+        Aig_ManStop( p->pAigTotal );
+    if ( p->pAigFraig )
+        Aig_ManStop( p->pAigFraig );
+    FREE( p->ppClasses );
+    FREE( p->ppSatVars );
+    Vec_PtrFree( p->vUsedNodes );
+    free( p );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/dch/dchSat.c b/src/aig/dch/dchSat.c
new file mode 100644
index 00000000..0d81991f
--- /dev/null
+++ b/src/aig/dch/dchSat.c
@@ -0,0 +1,47 @@
+/**CFile****************************************************************
+
+  FileName    [dchSat.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Choice computation for tech-mapping.]
+
+  Synopsis    [Calls to the SAT solver.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 29, 2008.]
+
+  Revision    [$Id: dchSat.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "dchInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/dch/dchSim.c b/src/aig/dch/dchSim.c
new file mode 100644
index 00000000..f11b701f
--- /dev/null
+++ b/src/aig/dch/dchSim.c
@@ -0,0 +1,225 @@
+/**CFile****************************************************************
+
+  FileName    [dchSim.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Computation of equivalence classes using simulation.]
+
+  Synopsis    [Calls to the SAT solver.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 29, 2008.]
+
+  Revision    [$Id: dchSim.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "dchInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static inline unsigned * Dch_ObjSim( Vec_Ptr_t * vSims, Aig_Obj_t * pObj )
+{ 
+    return Vec_PtrEntry( vSims, pObj->Id ); 
+}
+static inline unsigned Dch_ObjRandomSim()    
+{ 
+    return Aig_ManRandom(0);               
+}
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Perform random simulation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dch_PerformRandomSimulation( Aig_Man_t * pAig, Vec_Ptr_t * vSims, int nWords )
+{
+    unsigned * pSim, * pSim0, * pSim1;
+    Aig_Obj_t * pObj;
+    int i, k;
+
+    // assign const 1 sim info
+    pObj = Aig_ManConst1(pAig);
+    pSim = Dch_ObjSim( vSims, pObj );
+    memset( pSim, 0xff, sizeof(unsigned) * nWords );
+
+    // assign primary input random sim info
+    Aig_ManForEachPi( pAig, pObj, i )
+    {
+        pSim = Dch_ObjSim( vSims, pObj );
+        for ( k = 0; k < nWords; k++ )
+            pSim[k] = Dch_ObjRandomSim();
+    }
+
+    // simulate AIG in the topological order
+    Aig_ManForEachNode( pAig, pObj, i )
+    {
+        pSim0 = Dch_ObjSim( vSims, Aig_ObjFanin0(pObj) ); 
+        pSim1 = Dch_ObjSim( vSims, Aig_ObjFanin1(pObj) ); 
+        pSim  = Dch_ObjSim( vSims, pObj );
+
+        if ( Aig_ObjFaninC0(pObj) && Aig_ObjFaninC1(pObj) ) // both are compls
+        {
+            for ( k = 0; k < nWords; k++ )
+                pSim[k] = ~pSim0[k] & ~pSim1[k];
+        }
+        else if ( Aig_ObjFaninC0(pObj) && !Aig_ObjFaninC1(pObj) ) // first one is compl
+        {
+            for ( k = 0; k < nWords; k++ )
+                pSim[k] = ~pSim0[k] & pSim1[k];
+        }
+        else if ( !Aig_ObjFaninC0(pObj) && Aig_ObjFaninC1(pObj) ) // second one is compl
+        {
+            for ( k = 0; k < nWords; k++ )
+                pSim[k] = pSim0[k] & ~pSim1[k];
+        }
+        else // if ( Aig_ObjFaninC0(pObj) && Aig_ObjFaninC1(pObj) ) // none is compl
+        {
+            for ( k = 0; k < nWords; k++ )
+                pSim[k] = pSim0[k] & pSim1[k];
+        }
+    }
+
+    // get simulation information for primary outputs
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Hashing nodes by sim info.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dch_HashNodesBySimulationInfo( Aig_Man_t * pAig, Vec_Ptr_t * vSims, int nWords )
+{
+    unsigned * pSim0, * pSim1;
+    Aig_Obj_t * pObj, * pUnique;
+    int i, k, j, nodeId, Counter, c, CountNodes;
+
+    Vec_Int_t * vUniqueNodes, * vNodeCounters;
+
+    vUniqueNodes  = Vec_IntAlloc( 1000 );
+    vNodeCounters = Vec_IntStart( Aig_ManObjNumMax(pAig) );
+
+    Aig_ManForEachObj( pAig, pObj, i )
+    {
+        if ( Aig_ObjIsPo(pObj) )
+            continue;
+
+        // node's sim info
+        pSim0 = Dch_ObjSim( vSims, pObj );
+
+        Vec_IntForEachEntry( vUniqueNodes, nodeId, j )
+        {
+            pUnique = Aig_ManObj( pAig, nodeId );
+            // unique node's sim info
+            pSim1 = Dch_ObjSim( vSims, pUnique );
+
+            for ( k = 0; k < nWords; k++ )
+                if ( pSim0[k] != pSim1[k] )
+                    break;
+            if ( k == nWords ) // sim info is same as this node
+            {
+                Counter = Vec_IntEntry( vNodeCounters, nodeId );
+                Vec_IntWriteEntry( vNodeCounters, nodeId, Counter+1 );
+                break;
+            }
+        }
+
+        if ( j == Vec_IntSize(vUniqueNodes) ) // sim info of pObj is unique
+        {
+            Vec_IntPush( vUniqueNodes, pObj->Id );
+
+            Counter = Vec_IntEntry( vNodeCounters, pObj->Id );
+            assert( Counter == 0 );
+            Vec_IntWriteEntry( vNodeCounters, pObj->Id, Counter+1 );
+        }
+    }
+
+    Counter = 0;
+    Vec_IntForEachEntry( vNodeCounters, c, k )
+        if ( c > 1 )
+            Counter++;
+
+
+    printf( "Detected %d non-trivial candidate equivalence classes for %d nodes.\n", 
+        Counter, Vec_IntSize(vUniqueNodes) );
+
+    CountNodes = 0;
+    Vec_IntForEachEntry( vUniqueNodes, nodeId, k )
+    {
+        if (  Vec_IntEntry( vNodeCounters, nodeId ) == 1 )
+            continue;
+//        printf( "%d ", Vec_IntEntry( vNodeCounters, nodeId ) );
+        CountNodes += Vec_IntEntry( vNodeCounters, nodeId );
+    }
+//    printf( "\n" );
+    printf( "Nodes participating in non-trivial classes = %d.\n", CountNodes );
+
+
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives candidate equivalence classes of AIG nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Dch_Cla_t ** Dch_CreateCandEquivClasses( Aig_Man_t * pAig, int nWords, int fVerbose )
+{
+    Dch_Cla_t ** ppClasses;  // place for equivalence classes
+    Aig_MmFlex_t * pMemCla;  // memory for equivalence classes
+    Vec_Ptr_t * vSims;
+
+    // start storage for equivalence classes
+    ppClasses  = CALLOC( Dch_Cla_t *, Aig_ManObjNumMax(pAig) );
+    pMemCla = Aig_MmFlexStart();
+
+    // allocate simulation information
+    vSims = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(pAig), nWords );
+
+    // run simulation
+    Dch_PerformRandomSimulation( pAig, vSims, nWords );
+
+    // hash nodes by sim info
+    Dch_HashNodesBySimulationInfo( pAig, vSims, nWords );
+
+    // collect equivalence classes
+//    ppClasses = NULL;
+
+    // clean up and return
+    Aig_MmFlexStop( pMemCla, 0 );
+    Vec_PtrFree( vSims );
+    return ppClasses;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/dch/module.make b/src/aig/dch/module.make
new file mode 100644
index 00000000..ebe1ba7f
--- /dev/null
+++ b/src/aig/dch/module.make
@@ -0,0 +1,5 @@
+SRC +=    src/aig/dch/dchAig.c \
+    src/aig/dch/dchCore.c \
+    src/aig/dch/dchMan.c \
+    src/aig/dch/dchSat.c \
+    src/aig/dch/dchSim.c
diff --git a/src/aig/fra/fraCore.c b/src/aig/fra/fraCore.c
index 92a3f00b..fad8c7bf 100644
--- a/src/aig/fra/fraCore.c
+++ b/src/aig/fra/fraCore.c
@@ -38,7 +38,7 @@
     SAT solver run may return a counter-ex that  distinguishes the given 
     representative node from the constant-1 node but this counter-ex
     does not distinguish the nodes in the non-costant class... This is why 
-    there is no check of refinment after a counter-ex in the sequential case.
+    there is no check of refinement after a counter-ex in the sequential case.
 */
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index 41f3ac59..668c20cb 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -410,7 +410,7 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, Fra_Ssw_t * pParams )
     }
     // perform partitioning
     if ( (pParams->nPartSize > 0 && pParams->nPartSize < Aig_ManRegNum(pManAig))
-         || (pManAig->vClockDoms && Vec_VecSize(pManAig->vClockDoms) > 1)  )
+         || (pManAig->vClockDoms && Vec_VecSize(pManAig->vClockDoms) > 0)  )
         return Fra_FraigInductionPart( pManAig, pParams );
  
     nNodesBeg = Aig_ManNodeNum(pManAig);
diff --git a/src/aig/int/intInt.h b/src/aig/int/intInt.h
index ea2c48b8..dbb4301e 100644
--- a/src/aig/int/intInt.h
+++ b/src/aig/int/intInt.h
@@ -43,7 +43,7 @@ extern "C" {
 ///                         BASIC TYPES                              ///
 ////////////////////////////////////////////////////////////////////////
 
-// simulation manager
+// interpolation manager
 typedef struct Inter_Man_t_ Inter_Man_t;
 struct Inter_Man_t_
 {
diff --git a/src/aig/int/intMan.c b/src/aig/int/intMan.c
index b9b2bce9..ec5d06d3 100644
--- a/src/aig/int/intMan.c
+++ b/src/aig/int/intMan.c
@@ -30,7 +30,7 @@
 
 /**Function*************************************************************
 
-  Synopsis    [Frees the interpolation manager.]
+  Synopsis    [Creates the interpolation manager.]
 
   Description []
                
@@ -54,7 +54,7 @@ Inter_Man_t * Inter_ManCreate( Aig_Man_t * pAig, Inter_ManParams_t * pPars )
 
 /**Function*************************************************************
 
-  Synopsis    [Frees the interpolation manager.]
+  Synopsis    [Cleans the interpolation manager.]
 
   Description []
                
diff --git a/src/aig/ntl/ntlExtract.c b/src/aig/ntl/ntlExtract.c
index 3ef1d60e..56710a25 100644
--- a/src/aig/ntl/ntlExtract.c
+++ b/src/aig/ntl/ntlExtract.c
@@ -649,7 +649,11 @@ Aig_Man_t * Ntl_ManCollapseSeq( Ntl_Man_t * p, int nMinDomSize )
     if ( pAig->vClockDoms )
     {
         if ( Vec_VecSize(pAig->vClockDoms) == 0 )
-            printf( "Register classes are small. Seq synthesis is not performed.\n" );
+        {
+            printf( "Register classes are below the limit (%d). Seq synthesis is not performed.\n", nMinDomSize );
+            Aig_ManStop( pAig );
+            pAig = NULL;
+        }
         else
             printf( "Performing seq synthesis for %d register classes.\n", Vec_VecSize(pAig->vClockDoms) );
         printf( "\n" );
diff --git a/src/aig/ntl/ntlFraig.c b/src/aig/ntl/ntlFraig.c
index 38568d26..1f6a28ef 100644
--- a/src/aig/ntl/ntlFraig.c
+++ b/src/aig/ntl/ntlFraig.c
@@ -31,6 +31,80 @@
 
 /**Function*************************************************************
 
+  Synopsis    [Remaps representatives of the equivalence classes.]
+
+  Description [For each equivalence class, if the current representative 
+  of the class cannot be used because its corresponding net has no-merge 
+  attribute, find the topologically-shallowest node, which can be used 
+  as a representative.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntl_ManUpdateNoMergeReprs( Aig_Man_t * pAig, Aig_Obj_t ** pReprs )
+{
+    Aig_Obj_t ** pReprsNew = NULL;
+    Aig_Obj_t * pObj, * pRepres, * pRepresNew;
+    Ntl_Net_t * pNet, * pNetObj;
+    int i;
+
+    // allocate room for the new representative
+    pReprsNew = ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) );
+    memset( pReprsNew, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(pAig) );
+    Aig_ManForEachObj( pAig, pObj, i )
+    {
+        // get the old representative node
+        pRepres = pReprs[pObj->Id];
+        if ( pRepres == NULL )
+            continue;
+        // if this representative node is already remapped, skip it
+        pRepresNew = pReprsNew[ pRepres->Id ];
+        if ( pRepresNew != NULL )
+            continue;
+        // get the net of the representative node
+        pNet = pRepres->pData;
+        assert( pRepres->pData != NULL );
+        if ( Ntl_ObjIsBox(pNet->pDriver) && pNet->pDriver->pImplem->attrNoMerge )
+        {
+            // the net belongs to the no-merge box
+            pNetObj = pObj->pData;
+            if ( Ntl_ObjIsBox(pNetObj->pDriver) && pNetObj->pDriver->pImplem->attrNoMerge )
+                continue;
+            // the object's net does not belong to the no-merge box
+            // pObj can be used instead of pRepres
+            pReprsNew[ pRepres->Id ] = pObj;
+        }
+        else
+        {
+            // otherwise, it is fine to use pRepres
+            pReprsNew[ pRepres->Id ] = pRepres;
+        }
+    }
+    // update the representatives
+    Aig_ManForEachObj( pAig, pObj, i )
+    {
+        // get the representative node
+        pRepres = pReprs[ pObj->Id ];
+        if ( pRepres == NULL )
+            continue;
+        // if the representative has no mapping, undo the mapping of the node
+        pRepresNew = pReprsNew[ pRepres->Id ];
+        if ( pRepresNew == NULL || pRepresNew == pObj )
+        {
+            pReprs[ pObj->Id ] = NULL;
+            continue;
+        }
+        // remap the representative
+        assert( pObj->Id > pRepresNew->Id );        
+        pReprs[ pObj->Id ] = pRepresNew;
+    }
+    free( pReprsNew );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Transfers equivalence class info from pAigCol to pAig.]
 
   Description [pAig points to the nodes of netlist (pNew) derived using it.
@@ -112,6 +186,10 @@ Aig_Obj_t ** Ntl_ManFraigDeriveClasses( Aig_Man_t * pAig, Ntl_Man_t * pNew, Aig_
     // recall pointers to the nets of pNew
     Aig_ManForEachObj( pAig, pObj, i )
         pObj->pData = pObj->pNext, pObj->pNext = NULL;
+
+    // remap no-merge representatives to point to 
+    // the shallowest nodes in the class without no-merge
+    Ntl_ManUpdateNoMergeReprs( pAig, pReprs );
     return pReprs;
 }
 
@@ -156,7 +234,8 @@ void Ntl_ManReduce( Ntl_Man_t * p, Aig_Man_t * pAig )
             if ( pNet->pDriver->pImplem->attrNoMerge )
                 continue;
             // do not reduce the net if the replacement net has no-merge attribute
-            if ( pNetRepr != NULL && pNetRepr->pDriver->pImplem->attrNoMerge )
+            if ( pNetRepr != NULL && Ntl_ObjIsBox(pNetRepr->pDriver) && 
+                 pNetRepr->pDriver->pImplem->attrNoMerge )
                 continue;
         }
         if ( pNetRepr == NULL )
@@ -393,6 +472,11 @@ Ntl_Man_t * Ntl_ManSsw( Ntl_Man_t * p, Fra_Ssw_t * pPars )
     pAig = Ntl_ManExtract( p );
     pNew = Ntl_ManInsertAig( p, pAig );
     pAigCol = Ntl_ManCollapseSeq( pNew, pPars->nMinDomSize );
+    if ( pAigCol == NULL )
+    {
+        Aig_ManStop( pAig );
+        return pNew;
+    }
 
     // perform SCL for the given design
     pTemp = Fra_FraigInduction( pAigCol, pPars );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 8ca8e23f..45510e62 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -5,7 +5,7 @@
   SystemName  [ABC: Logic synthesis and verification system.]
 
   PackageName [Network and node package.]
-
+ 
   Synopsis    [Command file.]
 
   Author      [Alan Mishchenko]
@@ -35,6 +35,7 @@
 #include "saig.h"
 #include "nwkMerge.h"
 #include "int.h"
+#include "dch.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -135,6 +136,7 @@ static int Abc_CommandDRewrite       ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandDRefactor      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandDCompress2     ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandDChoice        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandDch            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandDrwsat         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandIRewriteSeq    ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandIResyn         ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -398,6 +400,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "New AIG",      "drf",           Abc_CommandDRefactor,        1 );
     Cmd_CommandAdd( pAbc, "New AIG",      "dcompress2",    Abc_CommandDCompress2,       1 );
     Cmd_CommandAdd( pAbc, "New AIG",      "dchoice",       Abc_CommandDChoice,          1 );
+    Cmd_CommandAdd( pAbc, "New AIG",      "dch",           Abc_CommandDch,              1 );
     Cmd_CommandAdd( pAbc, "New AIG",      "drwsat",        Abc_CommandDrwsat,           1 );
     Cmd_CommandAdd( pAbc, "New AIG",      "irws",          Abc_CommandIRewriteSeq,      1 );
     Cmd_CommandAdd( pAbc, "New AIG",      "iresyn",        Abc_CommandIResyn,           1 );
@@ -8943,6 +8946,110 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandDch( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Dch_Pars_t Pars, * pPars = &Pars;
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtkRes;
+    int c;
+
+    extern Abc_Ntk_t * Abc_NtkDch( Abc_Ntk_t * pNtk, Dch_Pars_t * pPars );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    Dch_ManSetDefaultParams( pPars );
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "WCSvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'W':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "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 )
+            {
+                fprintf( pErr, "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 )
+            {
+                fprintf( pErr, "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 'v':
+            pPars->fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( pErr, "This command works only for strashed networks.\n" );
+        return 1;
+    }
+    pNtkRes = Abc_NtkDch( pNtk, pPars );
+    if ( pNtkRes == NULL )
+    {
+        fprintf( pErr, "Command has failed.\n" );
+        return 0;
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: dch [-WCS num] [-vh]\n" );
+    fprintf( pErr, "\t         performs computation of structural choices\n" );
+    fprintf( pErr, "\t-W num : the max number of simulation words [default = %d]\n", pPars->nWords );
+    fprintf( pErr, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
+    fprintf( pErr, "\t-S num : the max number of SAT variables [default = %d]\n", pPars->nSatVarMax );
+    fprintf( pErr, "\t-v     : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandDrwsat( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
@@ -16328,7 +16435,7 @@ int Abc_CommandAbc8Write( Abc_Frame_t * pAbc, int argc, char ** argv )
     extern void * Ntl_ManInsertAig( void * p, Aig_Man_t * pAig );
     extern void * Ntl_ManDup( void * pOld );
     extern void Ntl_ManFree( void * p );
-    extern Aig_Man_t * Ntl_ManCollapseSeq( void * p );
+    extern Aig_Man_t * Ntl_ManCollapseSeq( void * p, int nMinDomSize );
 
     // set defaults
     fAig = 0;
@@ -16361,7 +16468,7 @@ int Abc_CommandAbc8Write( Abc_Frame_t * pAbc, int argc, char ** argv )
     {
         if ( fCollapsed )
         {
-            pTemp = Ntl_ManCollapseSeq( pAbc->pAbc8Ntl );
+            pTemp = Ntl_ManCollapseSeq( pAbc->pAbc8Ntl, 0 );
             Saig_ManDumpBlif( pTemp, pFileName );
             Aig_ManStop( pTemp );
         }
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 71f84272..c7e0df30 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -26,6 +26,7 @@
 #include "fra.h"
 #include "fraig.h"
 #include "int.h"
+#include "dch.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -826,6 +827,42 @@ Abc_Ntk_t * Abc_NtkDChoice( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, in
   SeeAlso     []
 
 ***********************************************************************/
+Abc_Ntk_t * Abc_NtkDch( Abc_Ntk_t * pNtk, Dch_Pars_t * pPars )
+{
+    extern Vec_Ptr_t * Dar_ManChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose );
+
+    Vec_Ptr_t * vAigs;
+    Aig_Man_t * pMan, * pTemp;
+    Abc_Ntk_t * pNtkAig;
+    int i;
+    assert( Abc_NtkIsStrash(pNtk) );
+    pMan = Abc_NtkToDar( pNtk, 0, 0 );
+    if ( pMan == NULL )
+        return NULL;
+    vAigs = Dar_ManChoiceSynthesis( pMan, 1, 1, pPars->fVerbose );
+    Aig_ManStop( pMan );
+    pMan = Dch_ComputeChoices( vAigs, pPars );
+//    pNtkAig = Abc_NtkFromDarChoices( pNtk, pMan );
+    pNtkAig = Abc_NtkFromDar( pNtk, pMan );
+    Aig_ManStop( pMan );
+    // cleanup
+    Vec_PtrForEachEntry( vAigs, pTemp, i )
+        Aig_ManStop( pTemp );
+    Vec_PtrFree( vAigs );
+    return pNtkAig;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Gives the current ABC network to AIG manager for processing.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 Abc_Ntk_t * Abc_NtkDrwsat( Abc_Ntk_t * pNtk, int fBalance, int fVerbose )
 {
     Aig_Man_t * pMan, * pTemp;