diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 273c530ec..b2b499eae 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -387,6 +387,7 @@ struct Jf_Par_t_
     float          Epsilon;
     float *        pTimesArr;
     float *        pTimesReq;
+    char *         ZFile;
 };
 
 static inline unsigned     Gia_ObjCutSign( unsigned ObjId )       { return (1 << (ObjId & 31));                                 }
diff --git a/src/aig/gia/giaNf.c b/src/aig/gia/giaNf.c
index 8bcf76b33..b38093f23 100644
--- a/src/aig/gia/giaNf.c
+++ b/src/aig/gia/giaNf.c
@@ -2161,6 +2161,90 @@ void Nf_ManFixPoDrivers( Nf_Man_t * p )
     //printf( "Fixed %d PO drivers.\n", Count );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Dump matches.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nf_ManDumpMatches( Nf_Man_t * p )
+{
+    FILE * pFile = fopen( p->pPars->ZFile, "wb" );
+    Gia_Obj_t * pObj; int n, iObj;
+    // output matches
+    Gia_ManForEachCi( p->pGia, pObj, n )
+        fprintf( pFile, "%d input %.2f\n", Abc_Var2Lit(Gia_ObjId(p->pGia, pObj), 0), 0.0 );
+    Gia_ManForEachAnd( p->pGia, pObj, iObj ) {
+        assert( !Gia_ObjIsBuf(pObj) );
+        for ( n = 0; n < 2; n++ ) {
+            int c, * pCut, * pCutSet = Nf_ObjCutSet( p, iObj );
+            Nf_SetForEachCut( pCutSet, pCut, c ) {
+                if ( Abc_Lit2Var(Nf_CutFunc(pCut)) >= Vec_WecSize(p->vTt2Match) )
+                    continue;
+                assert( !Nf_CutIsTriv(pCut, iObj) );
+                assert( Nf_CutSize(pCut) <= p->pPars->nLutSize );
+                assert( Abc_Lit2Var(Nf_CutFunc(pCut)) < Vec_WecSize(p->vTt2Match) );
+                int iFuncLit  = Nf_CutFunc(pCut);
+                int fComplExt = Abc_LitIsCompl(iFuncLit);
+                Vec_Int_t * v = Vec_WecEntry( p->vTt2Match, Abc_Lit2Var(iFuncLit) );
+                int j, k, Info, Offset, iFanin, fComplF;
+                Vec_IntForEachEntryDouble( v, Info, Offset, j ) {
+                    Nf_Cfg_t Cfg = Nf_Int2Cfg(Offset);
+                    int fCompl   = Cfg.fCompl ^ fComplExt;
+                    if ( fCompl != n )
+                        continue;
+                    Mio_Cell2_t*pC = Nf_ManCell( p, Info );
+                    assert( Nf_CutSize(pCut) == (int)pC->nFanins );
+                    fprintf( pFile, "%d ", Abc_Var2Lit(iObj, n) );
+                    fprintf( pFile, "%s ", pC->pName );
+                    fprintf( pFile, "%.2f", pC->AreaF );
+                    Nf_CutForEachVarCompl( pCut, Cfg, iFanin, fComplF, k )
+                        fprintf( pFile, " %d", Abc_Var2Lit(iFanin, fComplF) );
+                    fprintf( pFile, "\n" );
+                }
+            }
+        }
+    }
+    Gia_ManForEachCo( p->pGia, pObj, n )
+        fprintf( pFile, "%d output %.2f %d\n", Abc_Var2Lit(Gia_ObjId(p->pGia, pObj), 0), 0.0, Gia_ObjFaninLit0p(p->pGia, pObj) );
+    // output levels
+    extern int Gia_ManChoiceLevel( Gia_Man_t * p );
+    int LevelMax = Gia_ManChoiceLevel( p->pGia );
+    Gia_ManForEachCiId( p->pGia, iObj, n )
+        fprintf( pFile, "L%d %d\n", Abc_Var2Lit(iObj, 0), 0 );
+    Gia_ManForEachAnd( p->pGia, pObj, iObj )
+        fprintf( pFile, "L%d %d\n", Abc_Var2Lit(iObj, 0), Gia_ObjLevelId(p->pGia, iObj) );
+    Gia_ManForEachCoId( p->pGia, iObj, n )
+        fprintf( pFile, "L%d %d\n", Abc_Var2Lit(iObj, 0), LevelMax+1 );
+    // output mapping
+    Gia_ManForEachCiId( p->pGia, iObj, n )
+        if ( Nf_ObjMapRefNum(p, iObj, 1) )
+            fprintf( pFile, "M%d %s %.2f %d\n", Abc_Var2Lit(iObj, 1), p->pCells[3].pName, p->pCells[3].AreaF, Abc_Var2Lit(iObj, 0) );
+    Gia_ManForEachAnd( p->pGia, pObj, iObj )
+        for ( n = 0; n < 2; n++ )
+            if ( Nf_ObjMapRefNum(p, iObj, n) ) {
+                Nf_Mat_t * pM = Nf_ObjMatchBest(p, iObj, n);
+                if ( pM->fCompl ) {
+                    fprintf( pFile, "M%d %s %.2f %d\n", Abc_Var2Lit(iObj, n), p->pCells[3].pName, p->pCells[3].AreaF, Abc_Var2Lit(iObj, !n) );
+                    continue;
+                }
+                int k, iVar, fCompl, * pCut = Nf_CutFromHandle( Nf_ObjCutSet(p, iObj), pM->CutH );
+                Mio_Cell2_t*pC = Nf_ManCell( p, pM->Gate );
+                fprintf( pFile, "M%d ", Abc_Var2Lit(iObj, n) );
+                fprintf( pFile, "%s ", pC->pName );
+                fprintf( pFile, "%.2f", pC->AreaF );
+                Nf_CutForEachVarCompl( pCut, pM->Cfg, iVar, fCompl, k )
+                    fprintf( pFile, " %d", Abc_Var2Lit(iVar, fCompl) );
+                fprintf( pFile, "\n" );
+            }
+    fclose( pFile );
+}
+
 /**Function*************************************************************
 
   Synopsis    [Deriving mapping.]
@@ -2216,6 +2300,8 @@ Gia_Man_t * Nf_ManDeriveMapping( Nf_Man_t * p )
     }
 //    assert( Vec_IntCap(vMapping) == 16 || Vec_IntSize(vMapping) == Vec_IntCap(vMapping) );
     p->pGia->vCellMapping = vMapping;
+    if ( p->pPars->ZFile )
+        Nf_ManDumpMatches( p );
     return p->pGia;
 }
 void Nf_ManUpdateStats( Nf_Man_t * p )
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index d9af50b8e..c90c2f7d3 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -44574,7 +44574,7 @@ int Abc_CommandAbc9Nf( Abc_Frame_t * pAbc, int argc, char ** argv )
     Gia_Man_t * pNew; int c;
     Nf_ManSetDefaultPars( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "KCFARLEDQWakpqfvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "KCFARLEDQWZakpqfvwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -44694,6 +44694,15 @@ int Abc_CommandAbc9Nf( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nVerbLimit < 0 )
                 goto usage;
             break;
+        case 'Z':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-Z\" should be followed by an output file name.\n" );
+                goto usage;
+            }
+            pPars->ZFile = argv[globalUtilOptind];
+            globalUtilOptind++;
+            break;
         case 'a':
             pPars->fAreaOnly ^= 1;
             break;
@@ -44747,7 +44756,7 @@ usage:
         sprintf(Buffer, "best possible" );
     else
         sprintf(Buffer, "%d", pPars->DelayTarget );
-    Abc_Print( -2, "usage: &nf [-KCFARLEDQ num] [-akpqfvwh]\n" );
+    Abc_Print( -2, "usage: &nf [-KCFARLEDQ num] [-Z file] [-akpqfvwh]\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 );
@@ -44758,6 +44767,7 @@ usage:
     Abc_Print( -2, "\t-E num   : the area/edge tradeoff parameter (0 <= num <= 100) [default = %d]\n",       pPars->nAreaTuner );
     Abc_Print( -2, "\t-D num   : sets the delay constraint for the mapping [default = %s]\n",                Buffer );
     Abc_Print( -2, "\t-Q num   : internal parameter impacting area of the mapping [default = %d]\n",         pPars->nReqTimeFlex );
+    Abc_Print( -2, "\t-Z file  : the output file name to dump internal match info [default = unused]\n" );
     Abc_Print( -2, "\t-a       : toggles SAT-based area-oriented mapping (experimental) [default = %s]\n",   pPars->fAreaOnly? "yes": "no" );
     Abc_Print( -2, "\t-k       : toggles coarsening the subject graph [default = %s]\n",                     pPars->fCoarsen? "yes": "no" );
     Abc_Print( -2, "\t-p       : toggles pin permutation (more matches - better quality) [default = %s]\n",  pPars->fPinPerm? "yes": "no" );