Experiments with mapping plus small changes.

7 files changed, 124 insertions, 17 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 315d926b..ce649652 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -32150,7 +32150,7 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
             pPars->fDelayOptLut ^= 1;
             break;
         case 'd':
-            pPars->fBidec ^= 1;
+            pPars->fUse34Spec ^= 1;
             break;
         case 'b':
             pPars->fUseBat ^= 1;
@@ -32345,6 +32345,13 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
         pPars->fCutMin = 1;
     }
 
+    if ( pPars->fUse34Spec )
+    {
+        pPars->fTruth    = 1;
+        pPars->fCutMin   = 1;
+        pPars->nLutSize  = 4;
+    }
+
     // enable truth table computation if cut minimization is selected
     if ( pPars->fCutMin || pPars->fDeriveLuts )
     {
@@ -32487,7 +32494,7 @@ usage:
     Abc_Print( -2, "\t-p       : uses power-aware cut selection heuristics [default = %s]\n", pPars->fPower? "yes": "no" );
     Abc_Print( -2, "\t-m       : enables cut minimization by removing vacuous variables [default = %s]\n", pPars->fCutMin? "yes": "no" );
     Abc_Print( -2, "\t-s       : toggles delay-oriented mapping used with -S <NN> [default = %s]\n", pPars->fDelayOptLut? "yes": "no" );
-    Abc_Print( -2, "\t-d       : toggles deriving local AIGs using bi-decomposition [default = %s]\n", pPars->fBidec? "yes": "no" );
+    Abc_Print( -2, "\t-d       : toggles deriving specialized matching step [default = %s]\n", pPars->fUse34Spec? "yes": "no" );
     Abc_Print( -2, "\t-b       : toggles the use of one special feature [default = %s]\n", pPars->fUseBat? "yes": "no" );
     Abc_Print( -2, "\t-g       : toggles delay optimization by SOP balancing [default = %s]\n", pPars->fDelayOpt? "yes": "no" );
     Abc_Print( -2, "\t-x       : toggles delay optimization by DSD balancing [default = %s]\n", pPars->fDsdBalance? "yes": "no" );
diff --git a/src/base/cba/cba.h b/src/base/cba/cba.h
index 7dd1b8ac..a23c2bc7 100644
--- a/src/base/cba/cba.h
+++ b/src/base/cba/cba.h
@@ -69,6 +69,14 @@ typedef enum {
     CBA_BOX_MUX,  
     CBA_BOX_MAJ,  
 
+    CBA_BOX_ABC,
+    CBA_BOX_BA,
+    CBA_BOX_BO,
+    CBA_BOX_BX,
+    CBA_BOX_BN,
+    CBA_BOX_BAO,
+    CBA_BOX_BOA,
+
     CBA_BOX_RAND,
     CBA_BOX_RNAND,
     CBA_BOX_ROR,
@@ -95,6 +103,7 @@ typedef enum {
     CBA_BOX_ADD,
     CBA_BOX_SUB,
     CBA_BOX_MUL,
+    CBA_BOX_SMUL,
     CBA_BOX_DIV,
     CBA_BOX_MOD,
     CBA_BOX_REM,
@@ -102,6 +111,7 @@ typedef enum {
     CBA_BOX_MIN,
     CBA_BOX_ABS,
 
+    CBA_BOX_SLTHAN,
     CBA_BOX_LTHAN,
     CBA_BOX_LETHAN,
     CBA_BOX_METHAN,
@@ -111,6 +121,7 @@ typedef enum {
 
     CBA_BOX_SHIL,
     CBA_BOX_SHIR,
+    CBA_BOX_SHIRA,
     CBA_BOX_ROTL,
     CBA_BOX_ROTR,
 
@@ -124,6 +135,8 @@ typedef enum {
     CBA_BOX_RAMR,
     CBA_BOX_RAMW,
     CBA_BOX_RAMWC,
+    CBA_BOX_RAML,
+    CBA_BOX_RAMS,
     CBA_BOX_RAMBOX,
 
     CBA_BOX_LATCH,
@@ -1036,7 +1049,7 @@ extern int           Cba_ManIsTopoOrder( Cba_Man_t * p );
 extern Vec_Int_t *   Cba_NtkCollectDfs( Cba_Ntk_t * p );
 extern Cba_Man_t *   Cba_ManCollapse( Cba_Man_t * p, int TypeBuf );
 extern Cba_Man_t *   Cba_ManExtractGroup( Cba_Man_t * p, Vec_Int_t * vObjs );
-extern Cba_Man_t *   Cba_ManDeriveFromGia( Gia_Man_t * pGia );
+extern Cba_Man_t *   Cba_ManDeriveFromGia( Gia_Man_t * pGia, int fUseXor );
 extern Cba_Man_t *   Cba_ManInsertGroup( Cba_Man_t * p, Vec_Int_t * vObjs, Cba_Ntk_t * pSyn );
 /*=== cbaReadBlif.c ==========================================================*/
 extern void          Prs_ManReadBlifTest( char * pFileName );
diff --git a/src/base/cba/cbaNtk.c b/src/base/cba/cbaNtk.c
index f15df89a..6c312e88 100644
--- a/src/base/cba/cbaNtk.c
+++ b/src/base/cba/cbaNtk.c
@@ -700,7 +700,7 @@ Cba_Man_t * Cba_ManExtractGroup( Cba_Man_t * p, Vec_Int_t * vObjs )
   SeeAlso     []
 
 ***********************************************************************/
-static inline int Cba_NtkInsertGiaLit( Cba_Ntk_t * p, int iLit, Vec_Int_t * vLit2Fon )
+static inline int Cba_NtkInsertGiaLit( Cba_Ntk_t * p, int iLit, Vec_Int_t * vLit2Fon, int fUseXor )
 {
     int iObjNew;
     if ( iLit == 0 || iLit == 1 )
@@ -709,23 +709,34 @@ static inline int Cba_NtkInsertGiaLit( Cba_Ntk_t * p, int iLit, Vec_Int_t * vLit
         return Vec_IntEntry(vLit2Fon, iLit);
     assert( Abc_LitIsCompl(iLit) );
     assert( Vec_IntEntry(vLit2Fon, Abc_LitNot(iLit)) >= 0 );
-    iObjNew = Cba_ObjAlloc( p, CBA_BOX_INV, 1, 1 );
-    Cba_ObjSetFinFon( p, iObjNew, 0, Vec_IntEntry(vLit2Fon, Abc_LitNot(iLit)) );
+    // create inverter
+    if ( fUseXor )
+    {
+        iObjNew = Cba_ObjAlloc( p, CBA_BOX_XOR, 2, 1 );
+        Cba_ObjSetFinFon( p, iObjNew, 0, Vec_IntEntry(vLit2Fon, Abc_LitNot(iLit)) );
+        Cba_ObjSetFinFon( p, iObjNew, 1, Cba_FonFromConst(1) );
+    }
+    else
+    {
+        iObjNew = Cba_ObjAlloc( p, CBA_BOX_INV, 1, 1 );
+        Cba_ObjSetFinFon( p, iObjNew, 0, Vec_IntEntry(vLit2Fon, Abc_LitNot(iLit)) );
+    }
+    // save the result
     Vec_IntWriteEntry( vLit2Fon, iLit, Cba_ObjFon0(p, iObjNew) );
     return Cba_ObjFon0(p, iObjNew);
 }
-static inline int Cba_NtkInsertGiaObj( Cba_Ntk_t * p, Gia_Man_t * pGia, int iObj, Vec_Int_t * vLit2Fon )
+static inline int Cba_NtkInsertGiaObj( Cba_Ntk_t * p, Gia_Man_t * pGia, int iObj, Vec_Int_t * vLit2Fon, int fUseXor )
 {
     Gia_Obj_t * pObj = Gia_ManObj( pGia, iObj );
     int iLit0 = Gia_ObjFaninLit0( pObj, iObj );
     int iLit1 = Gia_ObjFaninLit1( pObj, iObj );
-    int iFon0 = Cba_NtkInsertGiaLit( p, iLit0, vLit2Fon );
-    int iFon1 = Cba_NtkInsertGiaLit( p, iLit1, vLit2Fon );
+    int iFon0 = Cba_NtkInsertGiaLit( p, iLit0, vLit2Fon, fUseXor );
+    int iFon1 = Cba_NtkInsertGiaLit( p, iLit1, vLit2Fon, fUseXor );
     int iObjNew;
     if ( Gia_ObjIsMux(pGia, pObj) )
     {
         int iLit2 = Gia_ObjFaninLit2( pGia, iObj );
-        int iFon2 = Cba_NtkInsertGiaLit( p, iLit2, vLit2Fon );
+        int iFon2 = Cba_NtkInsertGiaLit( p, iLit2, vLit2Fon, fUseXor );
         iObjNew = Cba_ObjAlloc( p, CBA_BOX_MUX, 3, 1 );
         Cba_ObjSetFinFon( p, iObjNew, 0, iFon2 );
         Cba_ObjSetFinFon( p, iObjNew, 1, iFon1 );
@@ -741,7 +752,7 @@ static inline int Cba_NtkInsertGiaObj( Cba_Ntk_t * p, Gia_Man_t * pGia, int iObj
     Vec_IntWriteEntry( vLit2Fon, Abc_Var2Lit(iObj, 0), Cba_ObjFon0(p, iObjNew) );
     return iObjNew;
 }
-Cba_Man_t * Cba_ManDeriveFromGia( Gia_Man_t * pGia )
+Cba_Man_t * Cba_ManDeriveFromGia( Gia_Man_t * pGia, int fUseXor )
 {
     Cba_Man_t * p = Cba_ManAlloc( pGia->pSpec, 1, NULL, NULL, NULL, NULL );
     Cba_Ntk_t * pNtk = Cba_NtkAlloc( p, Abc_NamStrFindOrAdd(p->pStrs, pGia->pName, NULL), Gia_ManCiNum(pGia), Gia_ManCoNum(pGia), 1000, 2000, 2000 );
@@ -759,19 +770,19 @@ Cba_Man_t * Cba_ManDeriveFromGia( Gia_Man_t * pGia )
         Vec_IntWriteEntry( vLit2Fon, Abc_Var2Lit(iObj, 0), Cba_ObjFon0(pNtk, iObjNew) );
     }
     Gia_ManForEachAndId( pGia, iObj )
-        Cba_NtkInsertGiaObj( pNtk, pGia, iObj, vLit2Fon );
+        Cba_NtkInsertGiaObj( pNtk, pGia, iObj, vLit2Fon, fUseXor );
     // create inverters if needed
     Gia_ManForEachCoId( pGia, iObj, i )
     {
         pObj = Gia_ManObj( pGia, iObj );
         iLit0 = Gia_ObjFaninLit0( pObj, iObj );
-        iFon0 = Cba_NtkInsertGiaLit( pNtk, iLit0, vLit2Fon ); // can be const!
+        iFon0 = Cba_NtkInsertGiaLit( pNtk, iLit0, vLit2Fon, fUseXor ); // can be const!
     }
     Gia_ManForEachCoId( pGia, iObj, i )
     {
         pObj = Gia_ManObj( pGia, iObj );
         iLit0 = Gia_ObjFaninLit0( pObj, iObj );
-        iFon0 = Cba_NtkInsertGiaLit( pNtk, iLit0, vLit2Fon ); // can be const!
+        iFon0 = Cba_NtkInsertGiaLit( pNtk, iLit0, vLit2Fon, fUseXor ); // can be const!
         iObjNew = Cba_ObjAlloc( pNtk, CBA_BOX_BUF, 1, 1 );
         Cba_ObjSetFinFon( pNtk, iObjNew, 0, iFon0 );
         iFon0 = Cba_ObjFon0(pNtk, iObjNew); // non-const fon unique for this output
diff --git a/src/map/if/if.h b/src/map/if/if.h
index 9c891c3d..214eda88 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -125,6 +125,7 @@ struct If_Par_t_
     int                fDsdBalance;   // special delay optimization
     int                fUserRecLib;   // use recorded library
     int                fBidec;        // use bi-decomposition
+    int                fUse34Spec;    // use specialized matching
     int                fUseBat;       // use one specialized feature
     int                fUseBuffs;     // use buffers to decouple outputs
     int                fEnableCheck07;// enable additional checking
diff --git a/src/map/if/ifCut.c b/src/map/if/ifCut.c
index adf00740..9e0c5a70 100644
--- a/src/map/if/ifCut.c
+++ b/src/map/if/ifCut.c
@@ -754,7 +754,7 @@ void If_CutSort( If_Man_t * p, If_Set_t * pCutSet, If_Cut_t * pCut )
     if ( !pCut->fUseless && 
          (p->pPars->fUseDsd || p->pPars->fUseBat || 
           p->pPars->pLutStruct || p->pPars->fUserRecLib || 
-          p->pPars->fEnableCheck07 || p->pPars->fUseCofVars || p->pPars->fUseAndVars || 
+          p->pPars->fEnableCheck07 || p->pPars->fUseCofVars || p->pPars->fUseAndVars || p->pPars->fUse34Spec || 
           p->pPars->fUseDsdTune || p->pPars->fEnableCheck75 || p->pPars->fEnableCheck75u) )
     {
         If_Cut_t * pFirst = pCutSet->ppCuts[0];
diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c
index 064494e0..c4053f52 100644
--- a/src/map/if/ifMap.c
+++ b/src/map/if/ifMap.c
@@ -99,7 +99,7 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
     If_Cut_t * pCut0R, * pCut1R;
     int fFunc0R, fFunc1R;
     int i, k, v, iCutDsd, fChange;
-    int fSave0 = p->pPars->fDelayOpt || p->pPars->fDelayOptLut || p->pPars->fDsdBalance || p->pPars->fUserRecLib || p->pPars->fUseDsdTune || p->pPars->fUseCofVars || p->pPars->fUseAndVars || p->pPars->pLutStruct != NULL;
+    int fSave0 = p->pPars->fDelayOpt || p->pPars->fDelayOptLut || p->pPars->fDsdBalance || p->pPars->fUserRecLib || p->pPars->fUseDsdTune || p->pPars->fUseCofVars || p->pPars->fUseAndVars || p->pPars->fUse34Spec || p->pPars->pLutStruct != NULL;
     int fUseAndCut = (p->pPars->nAndDelay > 0) || (p->pPars->nAndArea > 0);
     assert( !If_ObjIsAnd(pObj->pFanin0) || pObj->pFanin0->pCutSet->nCuts > 0 );
     assert( !If_ObjIsAnd(pObj->pFanin1) || pObj->pFanin1->pCutSet->nCuts > 0 );
@@ -275,6 +275,12 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
                 p->nCutsCountAll++;
                 p->nCutsCount[pCut->nLeaves]++;
             }
+            else if ( p->pPars->fUse34Spec )
+            {
+                assert( pCut->nLeaves <= 4 );
+                if ( pCut->nLeaves == 4 && !Abc_Tt4Check( (int)(0xFFFF & *If_CutTruth(p, pCut)) ) )
+                    pCut->fUseless = 1;
+            }
             else 
             {
                 if ( p->pPars->fUseAndVars )
@@ -415,7 +421,7 @@ void If_ObjPerformMappingChoice( If_Man_t * p, If_Obj_t * pObj, int Mode, int fP
     If_Set_t * pCutSet;
     If_Obj_t * pTemp;
     If_Cut_t * pCutTemp, * pCut;
-    int i, fSave0 = p->pPars->fDelayOpt || p->pPars->fDelayOptLut || p->pPars->fDsdBalance || p->pPars->fUserRecLib;
+    int i, fSave0 = p->pPars->fDelayOpt || p->pPars->fDelayOptLut || p->pPars->fDsdBalance || p->pPars->fUserRecLib || p->pPars->fUse34Spec;
     assert( pObj->pEquiv != NULL );
 
     // prepare
diff --git a/src/misc/util/utilTruth.h b/src/misc/util/utilTruth.h
index fab5e936..49f31da7 100644
--- a/src/misc/util/utilTruth.h
+++ b/src/misc/util/utilTruth.h
@@ -2567,6 +2567,75 @@ static inline void Abc_TtProcessBiDecExperiment()
     nVars = nSuppLim;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Truth table checking procedure.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     [] 
+
+***********************************************************************/
+static inline int Abc_Tt4Equal3( int c0, int c1, int c2, int c3 )
+{
+    if ( c0 == c1 && c0 == c2 ) return 3;
+    if ( c0 == c1 && c0 == c3 ) return 2;
+    if ( c0 == c3 && c0 == c2 ) return 1;
+    if ( c3 == c1 && c3 == c2 ) return 0;
+    return -1;
+}
+static inline int Abc_Tt4Check2( int t, int i, int j, int * f, int * r )
+{
+    int c0  =  t & r[j];
+    int c1  = (t & f[j]) >> (1 << j);
+    int c00 =  c0 & r[i];
+    int c01 = (c0 & f[i]) >> (1 << i);
+    int c10 =  c1 & r[i];
+    int c11 = (c1 & f[i]) >> (1 << i);
+    return Abc_Tt4Equal3( c00, c01, c10, c11 );
+}
+static inline int Abc_Tt4CheckTwoLevel( int t )
+{
+    int pair1, pair2;
+    int f[4] = { 0xAAAA, 0xCCCC, 0xF0F0, 0xFF00 };
+    int r[4] = { 0x5555, 0x3333, 0x0F0F, 0x00FF };
+    if ( (pair1 = Abc_Tt4Check2(t, 0, 1, f, r)) >= 0 && (pair2 = Abc_Tt4Check2(t, 2, 3, f, r)) >= 0 ) return (1 << 4) | (pair2 << 2) | pair1;
+    if ( (pair1 = Abc_Tt4Check2(t, 0, 2, f, r)) >= 0 && (pair2 = Abc_Tt4Check2(t, 1, 3, f, r)) >= 0 ) return (2 << 4) | (pair2 << 2) | pair1;
+    if ( (pair1 = Abc_Tt4Check2(t, 0, 3, f, r)) >= 0 && (pair2 = Abc_Tt4Check2(t, 1, 2, f, r)) >= 0 ) return (3 << 4) | (pair2 << 2) | pair1;
+    return -1;
+}
+static inline Abc_Tt4CountOnes( int t )
+{
+    t = (t & (0x5555)) + ((t >> 1) & (0x5555));
+    t = (t & (0x3333)) + ((t >> 2) & (0x3333));
+    t = (t & (0x0f0f)) + ((t >> 4) & (0x0f0f));
+    t = (t & (0x00ff)) + ((t >> 8) & (0x00ff));
+    return t;
+}
+static inline int Abc_Tt4FirstBit( int t )
+{
+    int n = 0;
+    if ( t == 0 ) return -1;
+    if ( (t & 0x00FF) == 0 ) { n +=  8; t >>=  8; }
+    if ( (t & 0x000F) == 0 ) { n +=  4; t >>=  4; }
+    if ( (t & 0x0003) == 0 ) { n +=  2; t >>=  2; }
+    if ( (t & 0x0001) == 0 ) { n++; }
+    return n;
+}
+static inline int Abc_Tt4Check( int t )
+{
+    int Count, tn = 0xFFFF & ~t;
+    if ( t == 0x6996 || tn == 0x6996 ) return 1;
+    if ( (t & (t-1)) == 0 )            return 1;
+    if ( (tn & (tn-1)) == 0 )          return 1;
+    Count = Abc_Tt4CountOnes( t );
+    if ( Count == 7 && Abc_Tt4CheckTwoLevel(t)  > 0 ) return 1;
+    if ( Count == 9 && Abc_Tt4CheckTwoLevel(tn) > 0 ) return 1;
+    return 0;
+}
+
 /*=== utilTruth.c ===========================================================*/