Integrating GIA with LUT mapping.

src/aig/gia/gia.h

@@ -700,6 +700,7 @@ extern int                 Gia_ManCounterExampleValueLookup( Gia_Man_t * pGia, i
 extern void                Gia_ManVerifyChoices( Gia_Man_t * p );
 extern void                Gia_ManReverseClasses( Gia_Man_t * p, int fNowIncreasing );
 extern int                 Gia_ManHasChoices( Gia_Man_t * p );
+extern int                 Gia_ManChoiceLevel( Gia_Man_t * p );
 /*=== giaCsatOld.c ============================================================*/
 extern Vec_Int_t *         Cbs_ManSolveMiter( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int fVerbose );
 /*=== giaCsat.c ============================================================*/
@@ -810,7 +811,14 @@ extern Gia_Man_t *         Gia_ManRehash( Gia_Man_t * p, int fAddStrash );
 extern void                Gia_ManHashProfile( Gia_Man_t * p );
 extern int                 Gia_ManHashLookup( Gia_Man_t * p, Gia_Obj_t * p0, Gia_Obj_t * p1 );
 /*=== giaIf.c ===========================================================*/
-extern void                Gia_ManPrintNpnClasses( Gia_Man_t * p );
+extern void                Gia_ManPrintMappingStats( Gia_Man_t * p );
+extern int                 Gia_ManLutFaninCount( Gia_Man_t * p );
+extern int                 Gia_ManLutSizeMax( Gia_Man_t * p );
+extern int                 Gia_ManLutNum( Gia_Man_t * p );
+extern int                 Gia_ManLutLevel( Gia_Man_t * p );
+extern void                Gia_ManSetRefsMapped( Gia_Man_t * p );
+extern void                Gia_ManSetIfParsDefault( void * pIfPars );
+extern Gia_Man_t *         Gia_ManPerformMapping( Gia_Man_t * p, void * pIfPars );
 /*=== giaIso.c ===========================================================*/
 extern Gia_Man_t *         Gia_ManIsoCanonicize( Gia_Man_t * p, int fVerbose );
 extern Gia_Man_t *         Gia_ManIsoReduce( Gia_Man_t * p, Vec_Ptr_t ** pvPosEquivs, int fDualOut, int fVerbose );
@@ -826,12 +834,7 @@ extern void                Gia_ManPrintStatsShort( Gia_Man_t * p );
 extern void                Gia_ManPrintMiterStatus( Gia_Man_t * p ); 
 extern void                Gia_ManSetRegNum( Gia_Man_t * p, int nRegs );
 extern void                Gia_ManReportImprovement( Gia_Man_t * p, Gia_Man_t * pNew );
-/*=== giaMap.c ===========================================================*/
-extern void                Gia_ManPrintMappingStats( Gia_Man_t * p );
-extern int                 Gia_ManLutFaninCount( Gia_Man_t * p );
-extern int                 Gia_ManLutSizeMax( Gia_Man_t * p );
-extern int                 Gia_ManLutNum( Gia_Man_t * p );
-extern int                 Gia_ManLutLevel( Gia_Man_t * p );
+extern void                Gia_ManPrintNpnClasses( Gia_Man_t * p );
 /*=== giaMem.c ===========================================================*/
 extern Gia_MmFixed_t *     Gia_MmFixedStart( int nEntrySize, int nEntriesMax );
 extern void                Gia_MmFixedStop( Gia_MmFixed_t * p, int fVerbose );

src/aig/gia/giaChoice.c

@@ -20,6 +20,7 @@
 
 #include "gia.h"
 #include "giaAig.h"
+#include "misc/tim/tim.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -261,6 +262,108 @@ int Gia_ManHasChoices( Gia_Man_t * p )
     return 1;
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    [Computes levels for AIG with choices and white boxes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManChoiceLevel_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+    Tim_Man_t * pManTime = (Tim_Man_t *)p->pManTime;
+    Gia_Obj_t * pNext;
+    int i, iBox, iTerm1, nTerms, LevelMax = 0;
+    if ( Gia_ObjIsTravIdCurrent( p, pObj ) )
+        return;
+    Gia_ObjSetTravIdCurrent( p, pObj );
+    if ( Gia_ObjIsCi(pObj) )
+    {
+        if ( pManTime )
+        {
+            iBox = Tim_ManBoxForCi( pManTime, Gia_ObjCioId(pObj) );
+            if ( iBox >= 0 ) // this is not a true PI
+            {
+                iTerm1 = Tim_ManBoxInputFirst( pManTime, iBox );
+                nTerms = Tim_ManBoxInputNum( pManTime, iBox );
+                for ( i = 0; i < nTerms; i++ )
+                {
+                    pNext = Gia_ManCo( p, iTerm1 + i );
+                    Gia_ManChoiceLevel_rec( p, pNext );
+                    if ( LevelMax < Gia_ObjLevel(p, pNext) )
+                        LevelMax = Gia_ObjLevel(p, pNext);
+                }
+                LevelMax++;
+            }
+        }
+//        Abc_Print( 1, "%d ", pObj->Level );
+    }
+    else if ( Gia_ObjIsCo(pObj) )
+    {
+        pNext = Gia_ObjFanin0(pObj);
+        Gia_ManChoiceLevel_rec( p, pNext );
+        if ( LevelMax < Gia_ObjLevel(p, pNext) )
+            LevelMax = Gia_ObjLevel(p, pNext);
+    }
+    else if ( Gia_ObjIsAnd(pObj) )
+    { 
+        // get the maximum level of the two fanins
+        pNext = Gia_ObjFanin0(pObj);
+        Gia_ManChoiceLevel_rec( p, pNext );
+        if ( LevelMax < Gia_ObjLevel(p, pNext) )
+            LevelMax = Gia_ObjLevel(p, pNext);
+        pNext = Gia_ObjFanin1(pObj);
+        Gia_ManChoiceLevel_rec( p, pNext );
+        if ( LevelMax < Gia_ObjLevel(p, pNext) )
+            LevelMax = Gia_ObjLevel(p, pNext);
+        LevelMax++;
+
+        // get the level of the nodes in the choice node
+        if ( p->pSibls && (pNext = Gia_ObjSiblObj(p, Gia_ObjId(p, pObj))) )
+        {
+            Gia_ManChoiceLevel_rec( p, pNext );
+            if ( LevelMax < Gia_ObjLevel(p, pNext) )
+                LevelMax = Gia_ObjLevel(p, pNext);
+        }
+    }
+    else if ( !Gia_ObjIsConst0(pObj) )
+        assert( 0 );
+    Gia_ObjSetLevel( p, pObj, LevelMax );
+}
+int Gia_ManChoiceLevel( Gia_Man_t * p )
+{
+    Gia_Obj_t * pObj;
+    int i, LevelMax = 0;
+//    assert( Gia_ManRegNum(p) == 0 );
+    Gia_ManCleanLevels( p, Gia_ManObjNum(p) );
+    Gia_ManIncrementTravId( p );
+    Gia_ManForEachCo( p, pObj, i )
+    {
+        Gia_ManChoiceLevel_rec( p, pObj );
+        if ( LevelMax < Gia_ObjLevel(p, pObj) )
+            LevelMax = Gia_ObjLevel(p, pObj);
+    }
+    // account for dangling boxes
+    Gia_ManForEachCi( p, pObj, i )
+    {
+        Gia_ManChoiceLevel_rec( p, pObj );
+        if ( LevelMax < Gia_ObjLevel(p, pObj) )
+            LevelMax = Gia_ObjLevel(p, pObj);
+//        Abc_Print( 1, "%d ", Gia_ObjLevel(p, pObj) );
+    }
+//    Abc_Print( 1, "\n" );
+    Gia_ManForEachAnd( p, pObj, i )
+        assert( Gia_ObjLevel(p, pObj) > 0 );
+//    printf( "Max level %d\n", LevelMax );
+    return LevelMax;
+} 
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/aig/gia/giaMan.c

@@ -21,6 +21,7 @@
 #include "gia.h"
 #include "misc/tim/tim.h"
 #include "proof/abs/abs.h"
+#include "opt/dar/dar.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -277,6 +278,7 @@ void Gia_ManPrintChoiceStats( Gia_Man_t * p )
         assert( Gia_ObjIsAnd(Gia_ObjSiblObj(p, i)) );
     }
     Abc_Print( 1, "Choice stats: Equivs =%7d. Choices =%7d.\n", nEquivs, nChoices );
+    Gia_ManCleanMark0( p );
 }
 
 /**Function*************************************************************
@@ -459,6 +461,96 @@ void Gia_ManReportImprovement( Gia_Man_t * p, Gia_Man_t * pNew )
     printf( "\n" );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Prints NPN class statistics.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManPrintNpnClasses( Gia_Man_t * p )
+{
+    extern char ** Kit_DsdNpn4ClassNames();
+    char ** pNames = Kit_DsdNpn4ClassNames();
+    Vec_Int_t * vLeaves, * vTruth, * vVisited;
+    int * pLutClass, ClassCounts[222] = {0};
+    int i, k, iFan, Class, OtherClasses, OtherClasses2, nTotal, Counter, Counter2;
+    unsigned * pTruth;
+    assert( p->pMapping != NULL );
+    assert(  Gia_ManLutSizeMax( p ) <= 4 );
+    vLeaves   = Vec_IntAlloc( 100 );
+    vVisited  = Vec_IntAlloc( 100 );
+    vTruth    = Vec_IntAlloc( (1<<16) );
+    pLutClass = ABC_CALLOC( int, Gia_ManObjNum(p) );
+    Gia_ManCleanTruth( p );
+    Gia_ManForEachLut( p, i )
+    {
+        if ( Gia_ObjLutSize(p,i) > 4 )
+            continue;
+        Vec_IntClear( vLeaves );
+        Gia_LutForEachFanin( p, i, iFan, k )
+            Vec_IntPush( vLeaves, iFan );
+        for ( ; k < 4; k++ )
+            Vec_IntPush( vLeaves, 0 );
+        pTruth = Gia_ManConvertAigToTruth( p, Gia_ManObj(p, i), vLeaves, vTruth, vVisited );
+        Class = Dar_LibReturnClass( *pTruth );
+        ClassCounts[ Class ]++;
+        pLutClass[i] = Class;
+    }
+    Vec_IntFree( vLeaves );
+    Vec_IntFree( vTruth );
+    Vec_IntFree( vVisited );
+    Vec_IntFreeP( &p->vTruths );
+    nTotal = 0;
+    for ( i = 0; i < 222; i++ )
+        nTotal += ClassCounts[i];
+    Abc_Print( 1, "NPN CLASS STATISTICS (for %d LUT4 present in the current mapping):\n", nTotal );
+    OtherClasses = 0;
+    for ( i = 0; i < 222; i++ )
+    {
+        if ( ClassCounts[i] == 0 )
+            continue;
+        if ( 100.0 * ClassCounts[i] / (nTotal+1) < 0.1 ) // do not show anything below 0.1 percent
+            continue;
+        OtherClasses += ClassCounts[i];
+        Abc_Print( 1, "Class %3d :  Count = %6d   (%7.2f %%)   %s\n", 
+            i, ClassCounts[i], 100.0 * ClassCounts[i] / (nTotal+1), pNames[i] );
+    }
+    OtherClasses = nTotal - OtherClasses;
+    Abc_Print( 1, "Other     :  Count = %6d   (%7.2f %%)\n", 
+        OtherClasses, 100.0 * OtherClasses / (nTotal+1) );
+    // count the number of LUTs that have MUX function and two fanins with MUX functions
+    OtherClasses = OtherClasses2 = 0;
+    ABC_FREE( p->pRefs );
+    Gia_ManSetRefsMapped( p );
+    Gia_ManForEachLut( p, i )
+    {
+        if ( pLutClass[i] != 109 )
+            continue;
+        Counter = Counter2 = 0;
+        Gia_LutForEachFanin( p, i, iFan, k )
+        {
+            Counter  += (pLutClass[iFan] == 109);
+            Counter2 += (pLutClass[iFan] == 109) && (Gia_ObjRefNumId(p, iFan) == 1);
+        }
+        OtherClasses  += (Counter > 1);
+        OtherClasses2 += (Counter2 > 1);
+//            Abc_Print( 1, "%d -- ", pLutClass[i] );
+//            Gia_LutForEachFanin( p, i, iFan, k )
+//                Abc_Print( 1, "%d ", pLutClass[iFan] );
+//            Abc_Print( 1, "\n" );
+    }
+    ABC_FREE( p->pRefs );
+    Abc_Print( 1, "Approximate number of 4:1 MUX structures: All = %6d  (%7.2f %%)  MFFC = %6d  (%7.2f %%)\n", 
+        OtherClasses,  100.0 * OtherClasses  / (nTotal+1),
+        OtherClasses2, 100.0 * OtherClasses2 / (nTotal+1) );
+    ABC_FREE( pLutClass );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/base/abc/abcCheck.c

@@ -377,12 +377,12 @@ int Abc_NtkCheckPos( Abc_Ntk_t * pNtk )
         }
         if ( Abc_ObjFaninNum(pObj) != 1 )
         {
-            fprintf( stdout, "NetworkCheck: A PO \"%s\" does not have one fanin.\n", Abc_ObjName(pObj) );
+            fprintf( stdout, "NetworkCheck: A PO \"%s\" does not have one fanin (but %d).\n", Abc_ObjName(pObj), Abc_ObjFaninNum(pObj) );
             return 0;
         }
         if ( Abc_ObjFanoutNum(pObj) > 0 )
         {
-            fprintf( stdout, "NetworkCheck: A PO \"%s\" has fanouts.\n", Abc_ObjName(pObj) );
+            fprintf( stdout, "NetworkCheck: A PO \"%s\" has %d fanout(s).\n", Abc_ObjName(pObj), Abc_ObjFanoutNum(pObj) );
             return 0;
         }
         pObj->pCopy = (Abc_Obj_t *)1;

src/base/abc/abcFanio.c

@@ -87,20 +87,13 @@ void Abc_ObjAddFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin )
     assert( !Abc_ObjIsComplement(pObj) );
     assert( pObj->pNtk == pFaninR->pNtk );
     assert( pObj->Id >= 0 && pFaninR->Id >= 0 );
+    assert( !Abc_ObjIsPi(pObj) && !Abc_ObjIsPo(pFanin) );    // fanin of PI or fanout of PO
+    assert( !Abc_ObjIsCo(pObj) || !Abc_ObjFaninNum(pObj) );  // CO with two fanins
+    assert( !Abc_ObjIsNet(pObj) || !Abc_ObjFaninNum(pObj) ); // net with two fanins
     Vec_IntPushMem( pObj->pNtk->pMmStep, &pObj->vFanins,     pFaninR->Id );
     Vec_IntPushMem( pObj->pNtk->pMmStep, &pFaninR->vFanouts, pObj->Id    );
     if ( Abc_ObjIsComplement(pFanin) )
         Abc_ObjSetFaninC( pObj, Abc_ObjFaninNum(pObj)-1 );
-    if ( Abc_ObjIsNet(pObj) && Abc_ObjFaninNum(pObj) > 1 )
-    {
-        printf( "Abc_ObjAddFanin(): Error! Creating net \"%s\" with two fanins.\n", Abc_ObjName(pObj) );
-    }
-/*
-    if ( Abc_ObjIsCo(pFanin) )
-    {
-        printf( "Abc_ObjAddFanin(): Error! Creating fanout of a CO.\n", Abc_ObjName(pFanin) );
-    }
-*/
 }
 
 

src/base/abci/abcDar.c

@@ -620,6 +620,150 @@ Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan )
     return pNtkNew;
 }
 
+
+
+/**Function*************************************************************
+
+  Synopsis    [Creates local function of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Hop_Obj_t * Abc_ObjHopFromGia_rec( Hop_Man_t * pHopMan, Gia_Man_t * p, int Id, Vec_Ptr_t * vCopies )
+{
+    Gia_Obj_t * pObj;
+    Hop_Obj_t * gFunc, * gFunc0, * gFunc1;
+    if ( Gia_ObjIsTravIdCurrentId(p, Id) )
+        return (Hop_Obj_t *)Vec_PtrEntry( vCopies, Id );
+    Gia_ObjSetTravIdCurrentId(p, Id);
+    pObj = Gia_ManObj(p, Id);
+    assert( Gia_ObjIsAnd(pObj) );
+    // compute the functions of the children
+    gFunc0 = Abc_ObjHopFromGia_rec( pHopMan, p, Gia_ObjFaninId0(pObj, Id), vCopies );
+    gFunc1 = Abc_ObjHopFromGia_rec( pHopMan, p, Gia_ObjFaninId1(pObj, Id), vCopies );
+    // get the function of the cut
+    gFunc  = Hop_And( pHopMan, Hop_NotCond(gFunc0, Gia_ObjFaninC0(pObj)), Hop_NotCond(gFunc1, Gia_ObjFaninC1(pObj)) );  
+    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 )
+{
+    int k, iFan;
+    assert( Gia_ObjIsLut(p, GiaId) );
+    assert( Gia_ObjLutSize(p, GiaId) > 0 );
+    Gia_ManIncrementTravId( p );
+    Gia_LutForEachFanin( p, GiaId, iFan, k )
+    {
+        Gia_ObjSetTravIdCurrentId(p, iFan);
+        Vec_PtrWriteEntry( vCopies, iFan, Hop_IthVar(pHopMan, k) );
+    }
+    return Abc_ObjHopFromGia_rec( pHopMan, p, GiaId, vCopies );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Converts the network from the mapped GIA manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkFromMappedGia( Gia_Man_t * p )
+{
+    int fVerbose = 0;
+    int fDuplicate = 0;
+    Abc_Ntk_t * pNtkNew;
+    Abc_Obj_t * pObjNew, * pObjNewLi, * pObjNewLo, * pConst0 = NULL;
+    Gia_Obj_t * pObj, * pObjLi, * pObjLo;
+    Vec_Ptr_t * vReflect;
+    int i, k, iFan, nDupGates; 
+    assert( p->pMapping != NULL );
+    pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_AIG, 1 );
+    // duplicate the name and the spec
+    pNtkNew->pName = Extra_UtilStrsav(p->pName);
+    pNtkNew->pSpec = Extra_UtilStrsav(p->pSpec);
+    Gia_ManFillValue( p );
+    // create constant
+    pConst0 = Abc_NtkCreateNodeConst0( pNtkNew );
+    Gia_ManConst0(p)->Value = Abc_ObjId(pConst0);
+    // create PIs
+    Gia_ManForEachPi( p, pObj, i )
+        pObj->Value = Abc_ObjId( Abc_NtkCreatePi( pNtkNew ) );
+    // create POs
+    Gia_ManForEachPo( p, pObj, i )
+        pObj->Value = Abc_ObjId( Abc_NtkCreatePo( pNtkNew ) );
+    // create as many latches as there are registers in the manager
+    Gia_ManForEachRiRo( p, pObjLi, pObjLo, i )
+    {
+        pObjNew = Abc_NtkCreateLatch( pNtkNew );
+        pObjNewLi = Abc_NtkCreateBi( pNtkNew );
+        pObjNewLo = Abc_NtkCreateBo( pNtkNew );
+        Abc_ObjAddFanin( pObjNew, pObjNewLi );
+        Abc_ObjAddFanin( pObjNewLo, pObjNew );
+        pObjLi->Value = Abc_ObjId( pObjNewLi );
+        pObjLo->Value = Abc_ObjId( pObjNewLo );
+        Abc_LatchSetInit0( pObjNew );
+    }
+    // rebuild the AIG
+    vReflect = Vec_PtrStart( Gia_ManObjNum(p) );
+    Gia_ManForEachLut( p, i )
+    {
+        pObj = Gia_ManObj(p, i);
+        assert( pObj->Value == ~0 );
+        if ( Gia_ObjLutSize(p, i) == 0 )
+        {
+            pObj->Value = Abc_ObjId(pConst0);
+            continue;
+        }
+        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( pNtkNew->pManFunc, p, i, vReflect );
+        pObj->Value = Abc_ObjId( pObjNew );
+    }
+    Vec_PtrFree( vReflect );
+    // connect the PO nodes
+    Gia_ManForEachCo( p, pObj, i )
+    {
+        pObjNew = Abc_NtkObj( pNtkNew, Gia_ObjValue(Gia_ObjFanin0(pObj)) );
+        Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), Abc_ObjNotCond( pObjNew, Gia_ObjFaninC0(pObj) ) );
+    }
+    // create names
+    Abc_NtkAddDummyPiNames( pNtkNew );
+    Abc_NtkAddDummyPoNames( pNtkNew );
+    Abc_NtkAddDummyBoxNames( pNtkNew );
+
+    // decouple the PO driver nodes to reduce the number of levels
+    nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, fDuplicate );
+    if ( fVerbose && nDupGates && !Abc_FrameReadFlag("silentmode") )
+    {
+        if ( !fDuplicate )
+            printf( "Added %d buffers/inverters to decouple the CO drivers.\n", nDupGates );
+        else
+            printf( "Duplicated %d gates to decouple the CO drivers.\n", nDupGates );
+    }
+    // remove const node if it is not used
+    if ( Abc_ObjFanoutNum(pConst0) == 0 )
+        Abc_NtkDeleteObj( pConst0 );
+
+    assert( Gia_ManPiNum(p) == Abc_NtkPiNum(pNtkNew) );
+    assert( Gia_ManPoNum(p) == Abc_NtkPoNum(pNtkNew) );
+    assert( Gia_ManRegNum(p) == Abc_NtkLatchNum(pNtkNew) );
+
+    // check the resulting AIG
+    if ( !Abc_NtkCheck( pNtkNew ) )
+        Abc_Print( 1, "Abc_NtkFromMappedGia(): Network check has failed.\n" );
+    return pNtkNew;
+}
+
+
 /**Function*************************************************************
 
   Synopsis    [Converts the network from the AIG manager into ABC.]

src/base/abci/abcIf.c

@@ -228,7 +228,6 @@ If_Man_t * Abc_NtkToIf( Abc_Ntk_t * pNtk, If_Par_t * pPars )
         // set up the choice node
         if ( Abc_AigNodeIsChoice( pNode ) )
         {
-            pIfMan->nChoices++;
             for ( pPrev = pNode, pFanin = (Abc_Obj_t *)pNode->pData; pFanin; pPrev = pFanin, pFanin = (Abc_Obj_t *)pFanin->pData )
                 If_ObjSetChoice( (If_Obj_t *)pPrev->pCopy, (If_Obj_t *)pFanin->pCopy );
             If_ManCreateChoice( pIfMan, (If_Obj_t *)pNode->pCopy );

src/base/main/mainInt.h

@@ -111,7 +111,7 @@ struct Abc_Frame_t_
     void *          pAbc85Ntl2;
     void *          pAbc85Best;
     void *          pAbc85Delay;
-    If_Lib_t *      pAbc85Lib;
+//    If_Lib_t *      pAbc85Lib;
 
     EXT_ABC_FRAME   // plugin for external functionality
 };

src/map/if/if.h

@@ -333,7 +333,7 @@ static inline void *     If_ObjCopy( If_Obj_t * pObj )                       { r
 static inline int        If_ObjLevel( If_Obj_t * pObj )                      { return pObj->Level;                   }
 static inline void       If_ObjSetLevel( If_Obj_t * pObj, int Level )        { pObj->Level = Level;                  }
 static inline void       If_ObjSetCopy( If_Obj_t * pObj, void * pCopy )      { pObj->pCopy = pCopy;                  }
-static inline void       If_ObjSetChoice( If_Obj_t * pObj, If_Obj_t * pEqu ) { pObj->pEquiv = pEqu;                  }
+static inline void       If_ObjSetChoice( If_Obj_t * pObj, If_Obj_t * pEqu ) { assert( pObj->Id > pEqu->Id ); pObj->pEquiv = pEqu;                  }
 
 static inline If_Cut_t * If_ObjCutBest( If_Obj_t * pObj )                    { return &pObj->CutBest;                }
 static inline unsigned   If_ObjCutSign( unsigned ObjId )                     { return (1 << (ObjId % 31));           }

src/map/if/ifMan.c

@@ -337,6 +337,7 @@ void If_ManCreateChoice( If_Man_t * p, If_Obj_t * pObj )
     // mark the largest level
     if ( p->nLevelMax < (int)pObj->Level )
         p->nLevelMax = (int)pObj->Level;
+    p->nChoices++;
 }
 
 /**Function*************************************************************

src/opt/nwk/nwkMap.c

@@ -163,7 +163,6 @@ If_Man_t * Nwk_ManToIf( Aig_Man_t * p, If_Par_t * pPars, Vec_Ptr_t * vAigToIf )
         // set up the choice node
         if ( Aig_ObjIsChoice( p, pNode ) )
         {
-            pIfMan->nChoices++;
             for ( pPrev = pNode, pFanin = Aig_ObjEquiv(p, pNode); pFanin; pPrev = pFanin, pFanin = Aig_ObjEquiv(p, pFanin) )
                 If_ObjSetChoice( (If_Obj_t *)pPrev->pData, (If_Obj_t *)pFanin->pData );
             If_ManCreateChoice( pIfMan, (If_Obj_t *)pNode->pData );

src/proof/llb/llb4Map.c

@@ -48,7 +48,7 @@ Vec_Int_t * Llb_AigMap( Aig_Man_t * pAig, int nLutSize, int nLutMin )
 {
     extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan );
     extern If_Man_t *  Abc_NtkToIf( Abc_Ntk_t * pNtk, If_Par_t * pPars );
-    extern void        Gia_ManSetIfParsDefault( If_Par_t * pPars );
+    extern void        Gia_ManSetIfParsDefault( void * pPars );
     If_Par_t Pars, * pPars = &Pars;
     If_Man_t * pIfMan;
     If_Obj_t * pAnd;