Adding &put -i to preserve special LUT mapping.

src/base/abci/abc.c

@@ -35234,16 +35234,18 @@ int Abc_CommandAbc9Put( Abc_Frame_t * pAbc, int argc, char ** argv )
     extern void Abc_NtkRedirectCiCo( Abc_Ntk_t * pNtk );
     extern Abc_Ntk_t * Abc_NtkFromCellMappedGia( Gia_Man_t * p, int fUseBuffs );
     extern Abc_Ntk_t * Abc_NtkFromMappedGia( Gia_Man_t * p, int fFindEnables, int fUseBuffs );
+    extern Abc_Ntk_t * Abc_NtkFromMappedGiaAnd5( Gia_Man_t * p, int fFindEnables, int fUseBuffs );
 
     Aig_Man_t * pMan;
     Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
     int fStatusClear = 1;
     int fFindEnables = 0;
     int fUseBuffs    = 0;
+    int fCheckAnd5   = 0;
     int c, fVerbose  = 0;
 
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "seovh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "seiovh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -35253,6 +35255,9 @@ int Abc_CommandAbc9Put( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'e':
             fFindEnables ^= 1;
             break;
+        case 'i':
+            fCheckAnd5 ^= 1;
+            break;
         case 'o':
             fUseBuffs ^= 1;
             break;
@@ -35275,7 +35280,7 @@ int Abc_CommandAbc9Put( Abc_Frame_t * pAbc, int argc, char ** argv )
     else if ( Gia_ManHasCellMapping(pAbc->pGia) )
         pNtk = Abc_NtkFromCellMappedGia( pAbc->pGia, fUseBuffs );
     else if ( Gia_ManHasMapping(pAbc->pGia) || pAbc->pGia->pMuxes )
-        pNtk = Abc_NtkFromMappedGia( pAbc->pGia, 0, fUseBuffs );
+        pNtk = fCheckAnd5 ? Abc_NtkFromMappedGiaAnd5( pAbc->pGia, 0, fUseBuffs ) : Abc_NtkFromMappedGia( pAbc->pGia, 0, fUseBuffs );
     else if ( Gia_ManHasDangling(pAbc->pGia) == 0 )
     {
         pMan = Gia_ManToAig( pAbc->pGia, 0 );
@@ -35298,6 +35303,8 @@ int Abc_CommandAbc9Put( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_NtkDelete( pNtkNoCh );
         Aig_ManStop( pMan );
     }
+    if ( pNtk == NULL )
+        return 1;
     // transfer the spec name to the pNtk
     if( pAbc->pGia->pSpec )
     {
@@ -35364,10 +35371,11 @@ int Abc_CommandAbc9Put( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &put [-seovh]\n" );
+    Abc_Print( -2, "usage: &put [-seiovh]\n" );
     Abc_Print( -2, "\t         transfer the current network into the old ABC\n" );
     Abc_Print( -2, "\t-s     : toggle clearning verification status [default = %s]\n", fStatusClear? "yes": "no" );
     Abc_Print( -2, "\t-e     : toggle extracting MUXes for flop enables [default = %s]\n", fFindEnables? "yes": "no" );
+    Abc_Print( -2, "\t-i     : toggle AND-decomposable polarity for 5-input LUTs [default = %s]\n", fCheckAnd5? "yes": "no" );
     Abc_Print( -2, "\t-o     : toggles using buffers to decouple combinational outputs [default = %s]\n", fUseBuffs? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");

src/base/abci/abcDar.c

@@ -38,6 +38,7 @@
 #include "opt/csw/csw.h"
 #include "proof/pdr/pdr.h"
 #include "sat/bmc/bmc.h"
+#include "misc/util/utilTruth.h"
 #include "map/mio/mio.h"
 #include "misc/vec/vecMem.h"
 
@@ -757,7 +758,7 @@ Hop_Obj_t * Abc_ObjHopFromGia_rec( Hop_Man_t * pHopMan, Gia_Man_t * p, int Id, V
     Vec_PtrWriteEntry( vCopies, Id, gFunc );
     return gFunc;
 }
-Hop_Obj_t * Abc_ObjHopFromGia( Hop_Man_t * pHopMan, Gia_Man_t * p, int GiaId, Vec_Ptr_t * vCopies )
+static Hop_Obj_t * Abc_ObjHopFromGia2( Hop_Man_t * pHopMan, Gia_Man_t * p, int GiaId, Vec_Ptr_t * vCopies, Vec_Bit_t * vCompls )
 {
     int k, iFan;
     assert( Gia_ObjIsLut(p, GiaId) );
@@ -766,10 +767,31 @@ Hop_Obj_t * Abc_ObjHopFromGia( Hop_Man_t * pHopMan, Gia_Man_t * p, int GiaId, Ve
     Gia_LutForEachFanin( p, GiaId, iFan, k )
     {
         Gia_ObjSetTravIdCurrentId(p, iFan);
-        Vec_PtrWriteEntry( vCopies, iFan, Hop_IthVar(pHopMan, k) );
+        Vec_PtrWriteEntry( vCopies, iFan, Hop_NotCond(Hop_IthVar(pHopMan, k), vCompls && Vec_BitEntry(vCompls, iFan)) );
     }
     return Abc_ObjHopFromGia_rec( pHopMan, p, GiaId, vCopies );
 }
+Hop_Obj_t * Abc_ObjHopFromGia( Hop_Man_t * pHopMan, Gia_Man_t * p, int GiaId, Vec_Ptr_t * vCopies )
+{
+    return Abc_ObjHopFromGia2( pHopMan, p, GiaId, vCopies, NULL );
+}
+
+static int Abc_Tt5HasAndDec( word Truth )
+{
+    int v;
+    for ( v = 0; v < 5; v++ )
+        if ( Abc_Tt6Cofactor0(Truth, v) == 0 || Abc_Tt6Cofactor1(Truth, v) == 0 )
+            return 1;
+    return 0;
+}
+static int Abc_Tt5AndDecPolarity( word Truth )
+{
+    if ( Abc_Tt5HasAndDec(Truth) )
+        return 0;
+    if ( Abc_Tt5HasAndDec(~Truth) )
+        return 1;
+    return -1;
+}
 
 /**Function*************************************************************
 
@@ -804,7 +826,7 @@ Abc_Obj_t * Abc_NtkFromMappedGia_rec( Abc_Ntk_t * pNtkNew, Gia_Man_t * p, int iO
         pObjNew = Abc_NtkCreateNodeInv(pNtkNew, pObjNew);
     return pObjNew;
 }
-Abc_Ntk_t * Abc_NtkFromMappedGia( Gia_Man_t * p, int fFindEnables, int fUseBuffs )
+Abc_Ntk_t * Abc_NtkFromMappedGiaInt( Gia_Man_t * p, int fFindEnables, int fUseBuffs, int fCheckAnd5 )
 {
     int fVerbose = 0;
     int fDuplicate = 0;
@@ -812,6 +834,7 @@ Abc_Ntk_t * Abc_NtkFromMappedGia( Gia_Man_t * p, int fFindEnables, int fUseBuffs
     Abc_Obj_t * pObjNew, * pObjNewLi, * pObjNewLo, * pConst0 = NULL;
     Gia_Obj_t * pObj, * pObjLi, * pObjLo;
     Vec_Ptr_t * vReflect;
+    Vec_Bit_t * vCompls = NULL;
     int i, k, iFan, nDupGates, nCountMux = 0; 
     assert( Gia_ManHasMapping(p) || p->pMuxes || fFindEnables );
     assert( !fFindEnables || !p->pMuxes );
@@ -820,6 +843,8 @@ Abc_Ntk_t * Abc_NtkFromMappedGia( Gia_Man_t * p, int fFindEnables, int fUseBuffs
     pNtkNew->pName = Extra_UtilStrsav(p->pName);
     pNtkNew->pSpec = Extra_UtilStrsav(p->pSpec);
     Gia_ManFillValue( p );
+    if ( fCheckAnd5 )
+        vCompls = Vec_BitStart( Gia_ManObjNum(p) );
     // create constant
     pConst0 = Abc_NtkCreateNodeConst0( pNtkNew );
     Gia_ManConst0(p)->Value = Abc_ObjId(pConst0);
@@ -917,6 +942,7 @@ Abc_Ntk_t * Abc_NtkFromMappedGia( Gia_Man_t * p, int fFindEnables, int fUseBuffs
         vReflect = Vec_PtrStart( Gia_ManObjNum(p) );
         Gia_ManForEachLut( p, i )
         {
+            Hop_Obj_t * pFunc;
             pObj = Gia_ManObj(p, i);
             assert( pObj->Value == ~0 );
             if ( Gia_ObjLutSize(p, i) == 0 )
@@ -924,10 +950,36 @@ Abc_Ntk_t * Abc_NtkFromMappedGia( Gia_Man_t * p, int fFindEnables, int fUseBuffs
                 pObj->Value = Abc_ObjId(pConst0);
                 continue;
             }
+            pFunc = Abc_ObjHopFromGia2( (Hop_Man_t *)pNtkNew->pManFunc, p, i, vReflect, vCompls );
+            if ( fCheckAnd5 && Gia_ObjLutSize(p, i) == 5 )
+            {
+                word Truth = Hop_ManComputeTruth6( (Hop_Man_t *)pNtkNew->pManFunc, pFunc, 5 );
+                int fCompl = Abc_Tt5AndDecPolarity( Truth );
+                if ( fCompl < 0 )
+                {
+                    Abc_Print( -1, "Abc_NtkFromMappedGia(): 5-input node %d does not have AND-decomposition in either polarity.\n", i );
+                    Vec_PtrFree( vReflect );
+                    Vec_BitFreeP( &vCompls );
+                    Abc_NtkDelete( pNtkNew );
+                    return NULL;
+                }
+                pFunc = Hop_NotCond( pFunc, fCompl );
+                Truth = fCompl ? ~Truth : Truth;
+                assert( Abc_Tt5HasAndDec(Truth) );
+                if ( !Abc_Tt5HasAndDec(Truth) )
+                {
+                    Abc_Print( -1, "Abc_NtkFromMappedGia(): Internal error: 5-input node %d failed AND-decomposition check.\n", i );
+                    Vec_PtrFree( vReflect );
+                    Vec_BitFreeP( &vCompls );
+                    Abc_NtkDelete( pNtkNew );
+                    return NULL;
+                }
+                Vec_BitWriteEntry( vCompls, i, fCompl );
+            }
             pObjNew = Abc_NtkCreateNode( pNtkNew );
             Gia_LutForEachFanin( p, i, iFan, k )
                 Abc_ObjAddFanin( pObjNew, Abc_NtkObj(pNtkNew, Gia_ObjValue(Gia_ManObj(p, iFan))) );
-            pObjNew->pData = Abc_ObjHopFromGia( (Hop_Man_t *)pNtkNew->pManFunc, p, i, vReflect );
+            pObjNew->pData = pFunc;
             pObjNew->fPersist = Gia_ObjLutIsMux(p, i) && Gia_ObjLutSize(p, i) == 3;
             pObj->Value = Abc_ObjId( pObjNew );
         }
@@ -939,8 +991,12 @@ Abc_Ntk_t * Abc_NtkFromMappedGia( Gia_Man_t * p, int fFindEnables, int fUseBuffs
     if ( !fFindEnables )
     Gia_ManForEachCo( p, pObj, i )
     {
+        int iFanin = Gia_ObjFaninId0p(p, pObj);
+        int fCompl = Gia_ObjFaninC0(pObj) ^ (vCompls && Vec_BitEntry(vCompls, iFanin));
         pObjNew = Abc_NtkObj( pNtkNew, Gia_ObjValue(Gia_ObjFanin0(pObj)) );
-        Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), Abc_ObjNotCond( pObjNew, Gia_ObjFaninC0(pObj) ) );
+        if ( fCheckAnd5 && fCompl && Gia_ObjIsLut(p, iFanin) && Gia_ObjLutSize(p, iFanin) == 5 )
+            pObjNew = Abc_NtkCreateNodeInv( pNtkNew, pObjNew ), fCompl = 0;
+        Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), Abc_ObjNotCond( pObjNew, fCompl ) );
     }
     // create names
     Abc_NtkAddDummyPiNames( pNtkNew );
@@ -967,8 +1023,17 @@ Abc_Ntk_t * Abc_NtkFromMappedGia( Gia_Man_t * p, int fFindEnables, int fUseBuffs
     // check the resulting AIG
     if ( !Abc_NtkCheck( pNtkNew ) )
         Abc_Print( 1, "Abc_NtkFromMappedGia(): Network check has failed.\n" );
+    Vec_BitFreeP( &vCompls );
     return pNtkNew;
 }
+Abc_Ntk_t * Abc_NtkFromMappedGia( Gia_Man_t * p, int fFindEnables, int fUseBuffs )
+{
+    return Abc_NtkFromMappedGiaInt( p, fFindEnables, fUseBuffs, 0 );
+}
+Abc_Ntk_t * Abc_NtkFromMappedGiaAnd5( Gia_Man_t * p, int fFindEnables, int fUseBuffs )
+{
+    return Abc_NtkFromMappedGiaInt( p, fFindEnables, fUseBuffs, 1 );
+}
 
 /**Function*************************************************************
 

src/map/if/ifDec07.c

@@ -1127,9 +1127,10 @@ int If_MatchCheck1( If_Man_t * p, unsigned * pTruth, int nVars, int nLeaves, cha
 }
 int If_MatchCheck2( If_Man_t * p, unsigned * pTruth, int nVars, int nLeaves, char * pStr )
 {
-    if ( nLeaves < nVars )
+    if ( nLeaves < p->pPars->nLutSize )
         return 1;
-    assert( nLeaves == nVars );
+    assert( nLeaves == p->pPars->nLutSize );
+    assert( nLeaves <= nVars );
     if ( Abc_Tt6Check2( ((word *)pTruth)[0], nLeaves ) )
         return 1;
     return 0;
@@ -1141,4 +1142,3 @@ int If_MatchCheck2( If_Man_t * p, unsigned * pTruth, int nVars, int nLeaves, cha
 
 
 ABC_NAMESPACE_IMPL_END
-