Added min-cut-based refinement of gate-level abstraction (command &gla_refine).

10 files changed, 690 insertions, 0 deletions

diff --git a/abclib.dsp b/abclib.dsp
index 82ab0dc2..71c3e22b 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -3351,6 +3351,10 @@ SOURCE=.\src\aig\gia\giaAbs.h
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\gia\giaAbsGla.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\gia\giaAbsVta.c
 # End Source File
 # Begin Source File
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 1bb883fa..b4ce11e6 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -691,6 +691,7 @@ extern Gia_Man_t *         Gia_ManDupWithConstraints( Gia_Man_t * p, Vec_Int_t *
 extern Gia_Man_t *         Gia_ManDupAbsFlops( Gia_Man_t * p, Vec_Int_t * vFlopClasses );
 extern Gia_Man_t *         Gia_ManDupAbsGates( Gia_Man_t * p, Vec_Int_t * vGateClasses );
 extern Vec_Int_t *         Gia_GlaCollectAssigned( Gia_Man_t * p, Vec_Int_t * vGateClasses );
+extern void                Gia_GlaCollectInputs( Gia_Man_t * p, Vec_Int_t * vGateClasses, Vec_Int_t ** pvPis, Vec_Int_t ** pvPPis );
 extern Gia_Man_t *         Gia_ManDupCones( Gia_Man_t * p, int * pPos, int nPos, int fTrimPis );
 /*=== giaEnable.c ==========================================================*/
 extern void                Gia_ManDetectSeqSignals( Gia_Man_t * p, int fSetReset, int fVerbose );
diff --git a/src/aig/gia/giaAbsGla.c b/src/aig/gia/giaAbsGla.c
new file mode 100644
index 00000000..5dac89a6
--- /dev/null
+++ b/src/aig/gia/giaAbsGla.c
@@ -0,0 +1,179 @@
+/**CFile****************************************************************
+
+  FileName    [giaAbsGla.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Scalable AIG package.]
+
+  Synopsis    [Gate-level abstraction.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: giaAbsGla.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "gia.h"
+#include "giaAig.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Derive a new counter-example.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Cex_t * Gia_ManCexRemap( Gia_Man_t * p, Gia_Man_t * pAbs, Abc_Cex_t * pCexAbs, Vec_Int_t * vPis )
+{
+    Abc_Cex_t * pCex;
+    int i, f, iPiNum;
+    assert( pCexAbs->iPo == 0 );
+    // start the counter-example
+    pCex = Abc_CexAlloc( Gia_ManRegNum(p), Gia_ManPiNum(p), pCexAbs->iFrame+1 );
+    pCex->iFrame = pCexAbs->iFrame;
+    pCex->iPo    = pCexAbs->iPo;
+    // copy the bit data
+    for ( f = 0; f <= pCexAbs->iFrame; f++ )
+        for ( i = 0; i < Vec_IntSize(vPis); i++ )
+        {
+            if ( Abc_InfoHasBit( pCexAbs->pData, pCexAbs->nRegs + pCexAbs->nPis * f + i ) )
+            {
+                iPiNum = Gia_ObjCioId( Gia_ManObj(p, Vec_IntEntry(vPis, i)) );
+                Abc_InfoSetBit( pCex->pData, pCex->nRegs + pCex->nPis * f + iPiNum );
+            }
+        }
+    // verify the counter example
+    if ( !Gia_ManVerifyCex( p, pCex, 0 ) )
+    {
+        printf( "Gia_ManCexRemap(): Counter-example is invalid.\n" );
+        Abc_CexFree( pCex );
+        pCex = NULL;
+    }
+    else
+    {
+        printf( "Counter-example verification is successful.\n" );
+        printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). \n", pCex->iPo, pCex->iFrame );
+    }
+    return pCex;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Refines gate-level abstraction using the counter-example.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManGlaRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int fMinCut, int fVerbose )
+{
+    extern void Nwk_ManDeriveMinCut( Gia_Man_t * p, int fVerbose );
+    extern Abc_Cex_t * Saig_ManCbaFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fVerbose );
+    Gia_Man_t * pAbs;
+    Aig_Man_t * pAig;
+    Abc_Cex_t * pCare;
+    Vec_Int_t * vPis, * vPPis;
+    int f, i, iObjId, nOnes = 0, Counter = 0;
+    if ( p->vGateClasses == NULL )
+    {
+        printf( "Gia_ManGlaRefine(): Abstraction gate map is missing.\n" );
+        return -1;
+    }
+    // derive abstraction
+    pAbs = Gia_ManDupAbsGates( p, p->vGateClasses );
+    Gia_ManStop( pAbs );
+    pAbs = Gia_ManDupAbsGates( p, p->vGateClasses );
+    if ( Gia_ManPiNum(pAbs) != pCex->nPis )
+    {
+        printf( "Gia_ManGlaRefine(): The PI counts in GLA and in CEX do not match.\n" );
+        Gia_ManStop( pAbs );
+        return -1;
+    }
+    if ( !Gia_ManVerifyCex( pAbs, pCex, 0 ) )
+    {
+        printf( "Gia_ManGlaRefine(): The initial counter-example is invalid.\n" );
+        Gia_ManStop( pAbs );
+        return -1;
+    }
+//    else
+//        printf( "Gia_ManGlaRefine(): The initial counter-example is correct.\n" );
+    // get inputs
+    Gia_GlaCollectInputs( p, p->vGateClasses, &vPis, &vPPis );
+    assert( Vec_IntSize(vPis) + Vec_IntSize(vPPis) == Gia_ManPiNum(pAbs) );
+    // minimize the CEX
+    pAig = Gia_ManToAigSimple( pAbs );
+    pCare = Saig_ManCbaFindCexCareBits( pAig, pCex, Vec_IntSize(vPis), fVerbose );
+    Aig_ManStop( pAig );
+    if ( pCare == NULL )
+        printf( "Counter-example minimization has failed.\n" );
+    // add new objects to the map
+    iObjId = -1;
+    for ( f = 0; f <= pCare->iFrame; f++ )
+        for ( i = 0; i < pCare->nPis; i++ )
+            if ( Abc_InfoHasBit( pCare->pData, pCare->nRegs + f * pCare->nPis + i ) )
+            {
+                nOnes++;
+                assert( i >= Vec_IntSize(vPis) );
+                iObjId = Vec_IntEntry( vPPis, i - Vec_IntSize(vPis) );
+                assert( iObjId > 0 && iObjId < Gia_ManObjNum(p) );
+                if ( Vec_IntEntry( p->vGateClasses, iObjId ) == 1 )
+                    continue;
+                assert( Vec_IntEntry( p->vGateClasses, iObjId ) == 0 );
+                Vec_IntWriteEntry( p->vGateClasses, iObjId, 1 );
+//                printf( "Adding object %d.\n", iObjId );
+//                Gia_ObjPrint( p, Gia_ManObj(p, iObjId) );
+                Counter++;
+            }
+    Abc_CexFree( pCare );
+    if ( fVerbose )
+        printf( "Essential bits = %d.  Additional objects = %d.\n", nOnes, Counter );
+    // consider the case of SAT
+    if ( iObjId == -1 )
+    {
+        ABC_FREE( p->pCexSeq );
+        p->pCexSeq = Gia_ManCexRemap( p, pAbs, pCex, vPis );
+        Vec_IntFree( vPis );
+        Vec_IntFree( vPPis );
+        Gia_ManStop( pAbs );
+        return 0;
+    }
+    Vec_IntFree( vPis );
+    Vec_IntFree( vPPis );
+    Gia_ManStop( pAbs );
+
+    // extract abstraction to include min-cut
+    if ( fMinCut )
+        Nwk_ManDeriveMinCut( p, fVerbose );
+    return -1;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index 7d11eff9..a5c246cb 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -1785,6 +1785,52 @@ Gia_Man_t * Gia_ManDupAbsGates( Gia_Man_t * p, Vec_Int_t * vGateClasses )
 
 /**Function*************************************************************
 
+  Synopsis    [Collects PIs and PPIs of the abstraction.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_GlaCollectInputs( Gia_Man_t * p, Vec_Int_t * vGateClasses, Vec_Int_t ** pvPis, Vec_Int_t ** pvPPis )
+{ 
+    Vec_Int_t * vAssigned, * vPis, * vPPis;
+    Gia_Obj_t * pObj;
+    int i;
+    assert( Gia_ManPoNum(p) == 1 );
+    assert( Vec_IntSize(vGateClasses) == Gia_ManObjNum(p) );
+    // create included objects and their fanins
+    vAssigned = Gia_GlaCollectAssigned( p, vGateClasses );
+    // create additional arrays
+    vPis   = Vec_IntAlloc( 1000 );
+    vPPis  = Vec_IntAlloc( 1000 );
+    Gia_ManForEachObjVec( vAssigned, p, pObj, i )
+    {
+        if ( Gia_ObjIsPi(p, pObj) )
+            Vec_IntPush( vPis, Gia_ObjId(p,pObj) );
+        else if ( !Vec_IntEntry(vGateClasses, Gia_ObjId(p,pObj)) )
+            Vec_IntPush( vPPis, Gia_ObjId(p,pObj) );
+        else if ( Gia_ObjIsAnd(pObj) )
+        {}
+        else if ( Gia_ObjIsRo(p, pObj) )
+        {}
+        else assert( Gia_ObjIsConst0(pObj) );
+    }
+    Vec_IntFree( vAssigned );
+    if ( pvPis )  
+        *pvPis  = vPis;
+    else
+        Vec_IntFree( vPis );
+    if ( pvPPis ) 
+        *pvPPis = vPPis;
+    else
+        Vec_IntFree( vPPis );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Returns the array of neighbors.]
 
   Description []
diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make
index aec38f40..e54a30d4 100644
--- a/src/aig/gia/module.make
+++ b/src/aig/gia/module.make
@@ -1,5 +1,6 @@
 SRC +=    src/aig/gia/gia.c \
     src/aig/gia/giaAbs.c \
+    src/aig/gia/giaAbsGla.c \
     src/aig/gia/giaAbsVta.c \
     src/aig/gia/giaAig.c \
     src/aig/gia/giaAiger.c \
diff --git a/src/aig/saig/saigAbsCba.c b/src/aig/saig/saigAbsCba.c
index 7863069f..55a429e1 100644
--- a/src/aig/saig/saigAbsCba.c
+++ b/src/aig/saig/saigAbsCba.c
@@ -761,11 +761,13 @@ if ( fVerbose )
 printf( "Care " );
 Abc_CexPrintStats( pCare );
 }
+/*
     // verify the reduced counter-example using ternary simulation
     if ( !Saig_ManCexVerifyUsingTernary( pAig, pCex, pCare ) )
         printf( "Saig_ManCbaFindCexCareBits(): Minimized counter-example verification has failed!!!\n" );
     else if ( fVerbose )
         printf( "Saig_ManCbaFindCexCareBits(): Minimized counter-example verification is successful.\n" );
+*/
     Aig_ManCleanMarkAB( pAig );
     return pCare;
 }
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index d3fb8d5a..c7c811f0 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -346,6 +346,7 @@ static int Abc_CommandAbc9AbsRefine          ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandAbc9AbsCba             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9AbsPba             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9GlaDerive          ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9GlaRefine          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9GlaCba             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9GlaPba             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Vta                ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -789,6 +790,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC9",         "&abs_cba",      Abc_CommandAbc9AbsCba,       0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&abs_pba",      Abc_CommandAbc9AbsPba,       0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&gla_derive",   Abc_CommandAbc9GlaDerive,    0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&gla_refine",   Abc_CommandAbc9GlaRefine,    0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&gla_cba",      Abc_CommandAbc9GlaCba,       0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&gla_pba",      Abc_CommandAbc9GlaPba,       0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&vta",          Abc_CommandAbc9Vta,          0 );
@@ -27013,6 +27015,8 @@ int Abc_CommandAbc9GlaDerive( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 0;
     }
     pTemp = Gia_ManDupAbsGates( pAbc->pGia, pAbc->pGia->vGateClasses );
+    Gia_ManStop( pTemp );
+    pTemp = Gia_ManDupAbsGates( pAbc->pGia, pAbc->pGia->vGateClasses );
     Abc_CommandUpdate9( pAbc, pTemp );
 //    printf( "This command is currently not enabled.\n" );
     return 0;
@@ -27036,6 +27040,67 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandAbc9GlaRefine( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern int Gia_ManGlaRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int fMinCut, int fVerbose );
+    int fMinCut = 1;
+    int c, fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "mvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'm':
+            fMinCut ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9GlaRefine(): There is no AIG.\n" );
+        return 1;
+    } 
+    if ( Gia_ManRegNum(pAbc->pGia) == 0 )
+    {
+        Abc_Print( -1, "The network is combinational.\n" );
+        return 0;
+    }
+    if ( pAbc->pCex == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9GlaRefine(): There is no counter-example.\n" );
+        return 1;
+    } 
+    pAbc->Status = Gia_ManGlaRefine( pAbc->pGia, pAbc->pCex, fMinCut, fVerbose );
+    Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &gla_refine [-mvh]\n" );
+    Abc_Print( -2, "\t         refines the pre-computed gate map using the counter-example\n" );
+    Abc_Print( -2, "\t-m     : toggle using min-cut to derive the refinements [default = %s]\n", fMinCut? "yes": "no" );
+    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    return 1;
+} 
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandAbc9GlaCba( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Saig_ParBmc_t Pars, * pPars = &Pars;
diff --git a/src/map/if/ifCheck.c b/src/map/if/ifCheck.c
new file mode 100644
index 00000000..317b6ffd
--- /dev/null
+++ b/src/map/if/ifCheck.c
@@ -0,0 +1,204 @@
+/**CFile****************************************************************
+
+  FileName    [ifCheck.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [FPGA mapping based on priority cuts.]
+
+  Synopsis    [Sequential mapping.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - November 21, 2006.]
+
+  Revision    [$Id: ifCheck.c,v 1.00 2006/11/21 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "if.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+#ifdef WIN32
+typedef unsigned __int64 word;
+#else
+typedef unsigned long long word;
+#endif
+
+// elementary truth tables
+static word Truths6[6] = {
+    0xAAAAAAAAAAAAAAAA,
+    0xCCCCCCCCCCCCCCCC,
+    0xF0F0F0F0F0F0F0F0,
+    0xFF00FF00FF00FF00,
+    0xFFFF0000FFFF0000,
+    0xFFFFFFFF00000000
+};
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the node Leaf is reachable on the path.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int If_ManCutReach_rec( If_Obj_t * pPath, If_Obj_t * pLeaf )
+{
+    if ( pPath == pLeaf )
+        return 1;
+    if ( pPath->fMark )
+        return 0;
+    assert( If_ObjIsAnd(pPath) );
+    if ( If_ManCutReach_rec( If_ObjFanin0(pPath), pLeaf ) )
+        return 1;
+    if ( If_ManCutReach_rec( If_ObjFanin1(pPath), pLeaf ) )
+        return 1;
+    return 0;
+}
+int If_ManCutReach( If_Man_t * p, If_Cut_t * pCut, If_Obj_t * pPath, If_Obj_t * pLeaf )
+{
+    If_Obj_t * pTemp;
+    int i, RetValue;
+    If_CutForEachLeaf( p, pCut, pTemp, i )
+        pTemp->fMark = 1;
+    RetValue = If_ManCutReach_rec( pPath, pLeaf );
+    If_CutForEachLeaf( p, pCut, pTemp, i )
+        pTemp->fMark = 0;
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derive truth table for each cofactor.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int If_ManCutTruthCheck_rec( If_Obj_t * pObj, word * pTruths )
+{
+    word T0, T1;
+    if ( pObj->fMark )
+        return pTruths[If_ObjId(pObj)];
+    assert( If_ObjIsAnd(pObj) );
+    T0 = If_ManCutTruthCheck_rec( If_ObjFanin0(pObj), pTruths );
+    T1 = If_ManCutTruthCheck_rec( If_ObjFanin1(pObj), pTruths );
+    T0 = If_ObjFaninC0(pObj) ? ~T0 : T0;
+    T1 = If_ObjFaninC1(pObj) ? ~T1 : T1;
+    return T0 & T1;
+}
+int If_ManCutTruthCheck( If_Man_t * p, If_Obj_t * pObj, If_Cut_t * pCut, If_Obj_t * pLeaf, int Cof, word * pTruths )
+{
+    word Truth;
+    If_Obj_t * pTemp;
+    int i, k = 0;
+    assert( Cof == 0 || Cof == 1 );
+    If_CutForEachLeaf( p, pCut, pTemp, i )
+    {
+        assert( pTemp->fMark == 0 );
+        pTemp->fMark = 1;
+        if ( pLeaf == pTemp )
+            pTruths[If_ObjId(pTemp)] = (Cof ? ~((word)0) : 0);
+        else
+            pTruths[If_ObjId(pTemp)] = Truths6[k++] ;
+    }
+    assert( k + 1 == If_CutLeaveNum(pCut) );
+    // compute truth table
+    Truth = If_ManCutTruthCheck_rec( pObj, pTruths );
+    If_CutForEachLeaf( p, pCut, pTemp, i )
+        pTemp->fMark = 0;
+    return Truth == 0 || Truth == ~((word)0);
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Checks if cut can be structurally/functionally decomposed.]
+
+  Description [The decomposition is Fn(a,b,c,...) = F2(a, Fn-1(b,c,...)).]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void If_ManCutCheck( If_Man_t * p, If_Obj_t * pObj, If_Cut_t * pCut )
+{
+    static int nDecCalls    = 0;
+    static int nDecStruct   = 0;
+    static int nDecStruct2  = 0;
+    static int nDecFunction = 0;
+    word * pTruths;
+    If_Obj_t * pLeaf, * pPath;
+    int i;
+    if ( pCut == NULL )
+    {
+        printf( "DecStr  = %9d (%6.2f %%).\n", nDecStruct,   100.0*nDecStruct/nDecCalls );
+        printf( "DecStr2 = %9d (%6.2f %%).\n", nDecStruct2,  100.0*nDecStruct2/nDecCalls );
+        printf( "DecFunc = %9d (%6.2f %%).\n", nDecFunction, 100.0*nDecFunction/nDecCalls );
+        printf( "Total   = %9d (%6.2f %%).\n", nDecCalls,    100.0*nDecCalls/nDecCalls );
+        return;
+    }
+    assert( If_ObjIsAnd(pObj) );
+    assert( pCut->nLeaves <= 7 );
+    nDecCalls++;
+    // check structural decomposition
+    If_CutForEachLeaf( p, pCut, pLeaf, i )
+        if ( pLeaf == If_ObjFanin0(pObj) || pLeaf == If_ObjFanin1(pObj) )
+            break;
+    if ( i < If_CutLeaveNum(pCut) )
+    {
+        pPath = (pLeaf == If_ObjFanin0(pObj)) ? If_ObjFanin1(pObj) : If_ObjFanin0(pObj);
+        if ( !If_ManCutReach( p, pCut, pPath, pLeaf ) )
+        {
+            nDecStruct++;
+//            nDecFunction++;
+//            return;
+        }
+        else
+            nDecStruct2++;
+    }
+    // check functional decomposition
+    pTruths = malloc( sizeof(word) * If_ManObjNum(p) );
+    If_CutForEachLeaf( p, pCut, pLeaf, i )
+    {
+        if ( If_ManCutTruthCheck( p, pObj, pCut, pLeaf, 0, pTruths ) )
+        {
+            nDecFunction++;
+            break;
+        }
+        if ( If_ManCutTruthCheck( p, pObj, pCut, pLeaf, 1, pTruths ) )
+        {
+            nDecFunction++;
+            break;
+        }
+    }
+    free( pTruths );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/opt/nwk/nwkAig.c b/src/opt/nwk/nwkAig.c
index 6254bc41..a4959c9a 100644
--- a/src/opt/nwk/nwkAig.c
+++ b/src/opt/nwk/nwkAig.c
@@ -103,6 +103,191 @@ Vec_Ptr_t * Nwk_ManDeriveRetimingCut( Aig_Man_t * p, int fForward, int fVerbose
     return vNodes;
 }
 
+
+
+#include "src/aig/gia/gia.h"
+
+/**Function*************************************************************
+
+  Synopsis    [Collects reachable nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ManColleacReached_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vNodes, Vec_Int_t * vLeaves )
+{
+    if ( Gia_ObjIsTravIdCurrent(p, pObj) )
+        return;
+    Gia_ObjSetTravIdCurrent(p, pObj);
+    if ( Gia_ObjIsCi(pObj) )
+    {
+        Vec_IntPush( vLeaves, Gia_ObjId(p, pObj) );
+        return;
+    }
+    assert( Gia_ObjIsAnd(pObj) );
+    Nwk_ManColleacReached_rec( p, Gia_ObjFanin0(pObj), vNodes, vLeaves );
+    Nwk_ManColleacReached_rec( p, Gia_ObjFanin1(pObj), vNodes, vLeaves );
+    Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Converts AIG into the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Nwk_Man_t * Nwk_ManCreateFromGia( Gia_Man_t * p, Vec_Int_t * vPPis, Vec_Int_t * vNodes, Vec_Int_t * vLeaves, Vec_Int_t ** pvMapInv )
+{
+    Nwk_Man_t * pNtk;
+    Nwk_Obj_t ** ppCopies;
+    Gia_Obj_t * pObj;
+    Vec_Int_t * vMaps;
+    int i;
+    assert( Vec_IntSize(vLeaves) >= Vec_IntSize(vPPis) );
+    Gia_ManCreateRefs( p );
+    pNtk = Nwk_ManAlloc();
+    pNtk->pName = Abc_UtilStrsav( p->pName );
+    pNtk->nFanioPlus = 0;
+    Hop_ManStop( pNtk->pManHop );
+    pNtk->pManHop = NULL;
+    // allocate
+    vMaps = Vec_IntAlloc( Vec_IntSize(vNodes) + Abc_MaxInt(Vec_IntSize(vPPis), Vec_IntSize(vLeaves)) + 1 );
+    ppCopies = ABC_ALLOC( Nwk_Obj_t *, Gia_ManObjNum(p) );
+    // copy objects
+    pObj = Gia_ManConst0(p);
+    ppCopies[Gia_ObjId(p,pObj)] = Nwk_ManCreateNode( pNtk, 0, Gia_ObjRefs(p,pObj) );
+    Vec_IntPush( vMaps, Gia_ObjId(p,pObj) );
+    Gia_ManForEachObjVec( vLeaves, p, pObj, i )
+    {
+        ppCopies[Gia_ObjId(p,pObj)] = Nwk_ManCreateCi( pNtk, Gia_ObjRefs(p,pObj) );
+        assert( Vec_IntSize(vMaps) == Nwk_ObjId(ppCopies[Gia_ObjId(p,pObj)]) );
+        Vec_IntPush( vMaps, Gia_ObjId(p,pObj) );
+    }
+/*
+    for ( i = Vec_IntSize(vLeaves); i < Vec_IntSize(vPPis); i++ )
+    {
+        pTemp = Nwk_ManCreateCi( pNtk, Gia_ObjRefs(p,pObj) );
+        Vec_IntPush( vMaps, 0 );// ???
+    }
+*/
+    Gia_ManForEachObjVec( vNodes, p, pObj, i )
+    {
+        ppCopies[Gia_ObjId(p,pObj)] = Nwk_ManCreateNode( pNtk, 2, Gia_ObjRefs(p,pObj) );
+        Nwk_ObjAddFanin( ppCopies[Gia_ObjId(p,pObj)], ppCopies[Gia_ObjFaninId0p(p,pObj)] );
+        Nwk_ObjAddFanin( ppCopies[Gia_ObjId(p,pObj)], ppCopies[Gia_ObjFaninId1p(p,pObj)] );
+        assert( Vec_IntSize(vMaps) == Nwk_ObjId(ppCopies[Gia_ObjId(p,pObj)]) );
+        Vec_IntPush( vMaps, Gia_ObjId(p,pObj) );
+    }
+    Gia_ManForEachObjVec( vPPis, p, pObj, i )
+    {
+        assert( ppCopies[Gia_ObjId(p,pObj)] != NULL );
+        Nwk_ObjAddFanin( Nwk_ManCreateCo(pNtk), ppCopies[Gia_ObjId(p,pObj)] );
+    }
+    for ( i = Vec_IntSize(vPPis); i < Vec_IntSize(vLeaves); i++ )
+        Nwk_ObjAddFanin( Nwk_ManCreateCo(pNtk), ppCopies[0] );
+    assert( Vec_IntSize(vMaps) == Vec_IntSize(vNodes) + Abc_MaxInt(Vec_IntSize(vPPis), Vec_IntSize(vLeaves)) + 1 );
+    ABC_FREE( ppCopies );
+    *pvMapInv = vMaps;
+    return pNtk;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Returns min-cut in the AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ManDeriveMinCut( Gia_Man_t * p, int fVerbose )
+{
+    Nwk_Man_t * pNtk;
+    Nwk_Obj_t * pNode;
+    Vec_Ptr_t * vMinCut;
+    Vec_Int_t * vPPis, * vNodes, * vLeaves, * vNodes2, * vLeaves2, * vMapInv;
+    Vec_Int_t * vCommon, * vDiff0, * vDiff1;
+    Gia_Obj_t * pObj;
+    int i, iObjId;
+    // get inputs
+    Gia_GlaCollectInputs( p, p->vGateClasses, NULL, &vPPis );
+    // collect nodes rechable from PPIs
+    vNodes = Vec_IntAlloc( 100 );
+    vLeaves = Vec_IntAlloc( 100 );
+    Gia_ManIncrementTravId( p );
+    Gia_ManForEachObjVec( vPPis, p, pObj, i )
+        Nwk_ManColleacReached_rec( p, pObj, vNodes, vLeaves );
+    // derive the new network
+    pNtk = Nwk_ManCreateFromGia( p, vPPis, vNodes, vLeaves, &vMapInv );
+    assert( Nwk_ManPiNum(pNtk) == Nwk_ManPoNum(pNtk) );
+    // create min-cut
+    vMinCut = Nwk_ManRetimeCutBackward( pNtk, Nwk_ManPiNum(pNtk), fVerbose );
+    // copy from the GIA back
+//    Aig_ManForEachObj( p, pObj, i )
+//        ((Nwk_Obj_t *)pObj->pData)->pCopy = pObj;
+    // mark min-cut nodes
+    vNodes2 = Vec_IntAlloc( 100 );
+    vLeaves2 = Vec_IntAlloc( 100 );
+    Gia_ManIncrementTravId( p );
+    Vec_PtrForEachEntry( Nwk_Obj_t *, vMinCut, pNode, i )
+    {
+        pObj = Gia_ManObj( p, Vec_IntEntry(vMapInv, Nwk_ObjId(pNode)) );
+        if ( Gia_ObjIsConst0(pObj) )
+            continue;
+        Nwk_ManColleacReached_rec( p, pObj, vNodes2, vLeaves2 );
+    }
+    if ( fVerbose )
+        printf( "Min-cut: %d -> %d.  Nodes %d -> %d.  ", Vec_IntSize(vPPis)+1, Vec_PtrSize(vMinCut), Vec_IntSize(vNodes), Vec_IntSize(vNodes2) );
+    Vec_IntFree( vPPis );
+    Vec_PtrFree( vMinCut );
+    Vec_IntFree( vMapInv );
+    Nwk_ManFree( pNtk );
+
+    // sort the results
+    Vec_IntSort( vNodes, 0 );
+    Vec_IntSort( vNodes2, 0 );
+    vCommon = Vec_IntAlloc( Vec_IntSize(vNodes) );
+    vDiff0 = Vec_IntAlloc( 100 );
+    vDiff1 = Vec_IntAlloc( 100 );
+    Vec_IntTwoSplit( vNodes, vNodes2, vCommon, vDiff0, vDiff1 );
+    if ( fVerbose )
+        printf( "Common = %d.  Diff0 = %d. Diff1 = %d.\n", Vec_IntSize(vCommon), Vec_IntSize(vDiff0), Vec_IntSize(vDiff1) );
+
+    // fill in
+    Vec_IntForEachEntry( vDiff0, iObjId, i )
+        Vec_IntWriteEntry( p->vGateClasses, iObjId, 1 );
+
+    Vec_IntFree( vLeaves );
+    Vec_IntFree( vNodes );
+    Vec_IntFree( vLeaves2 );
+    Vec_IntFree( vNodes2 );
+
+    Vec_IntFree( vCommon );
+    Vec_IntFree( vDiff0 );
+    Vec_IntFree( vDiff1 );
+
+    // check abstraction
+    Gia_ManForEachObj( p, pObj, i )
+    {
+        if ( Vec_IntEntry( p->vGateClasses, i ) == 0 )
+            continue;
+        assert( Gia_ObjIsConst0(pObj) || Gia_ObjIsRo(p, pObj) || Gia_ObjIsAnd(pObj) );
+    }
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c
index 3cf47a92..f863a881 100644
--- a/src/proof/pdr/pdrCore.c
+++ b/src/proof/pdr/pdrCore.c
@@ -706,6 +706,8 @@ int Pdr_ManSolve_( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t ** pvPrioInit,
 ***********************************************************************/
 int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex )
 {
+    if ( pPars->fVerbose )
+    {
 //    Abc_Print( 1, "Running PDR by Niklas Een (aka IC3 by Aaron Bradley) with these parameters:\n" );
     Abc_Print( 1, "VarMax = %d. FrameMax = %d. QueueMax = %d. TimeMax = %d. ", 
         pPars->nRecycle, pPars->nFrameMax, pPars->nRestLimit, pPars->nTimeOut );
@@ -713,6 +715,7 @@ int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex )
         Abc_Print( 1, "Output = %d. ", pPars->iOutput );
     Abc_Print( 1, "MonoCNF = %s. SkipGen = %s.\n", 
         pPars->fMonoCnf ? "yes" : "no", pPars->fSkipGeneral ? "yes" : "no" );
+    }
 
 /*
     Vec_Int_t * vPrioInit = NULL;