Merge remote-tracking branch 'upstream/master' into yosys-experimental

Makefile

@@ -37,7 +37,7 @@ MODULES := \
 	src/base/abc src/base/abci src/base/cmd src/base/io src/base/main src/base/exor \
 	src/base/ver src/base/wlc src/base/wln src/base/acb src/base/bac src/base/cba src/base/pla src/base/test \
 	src/map/mapper src/map/mio src/map/super src/map/if src/map/if/acd \
-	src/map/amap src/map/cov src/map/scl src/map/mpm \
+	src/map/amap src/map/cov src/map/scl src/map/mpm src/map/emap \
 	src/misc/extra src/misc/mvc src/misc/st src/misc/util src/misc/nm \
 	src/misc/vec src/misc/hash src/misc/tim src/misc/bzlib src/misc/zlib \
 	src/misc/mem src/misc/bar src/misc/bbl src/misc/parse src/misc/btor \
@@ -185,32 +185,32 @@ DEP := $(OBJ:.o=.d)
 %.o: %.c
 	@mkdir -p $(dir $@)
 	@echo "$(MSG_PREFIX)\`\` Compiling:" $(LOCAL_PATH)/$<
-	$(VERBOSE)$(CC) -c $(OPTFLAGS) $(INCLUDES) $(CFLAGS) $< -o $@
+	$(VERBOSE)$(CC) -c $(OPTFLAGS) $(INCLUDES) $(CPPFLAGS) $(CFLAGS) $< -o $@
 
 %.o: %.cc
 	@mkdir -p $(dir $@)
 	@echo "$(MSG_PREFIX)\`\` Compiling:" $(LOCAL_PATH)/$<
-	$(VERBOSE)$(CXX) -c $(OPTFLAGS) $(INCLUDES) $(CXXFLAGS) $< -o $@
+	$(VERBOSE)$(CXX) -c $(OPTFLAGS) $(INCLUDES) $(CPPFLAGS) $(CXXFLAGS) $< -o $@
 
 %.o: %.cpp
 	@mkdir -p $(dir $@)
 	@echo "$(MSG_PREFIX)\`\` Compiling:" $(LOCAL_PATH)/$<
-	$(VERBOSE)$(CXX) -c $(OPTFLAGS) $(INCLUDES) $(CXXFLAGS) $< -o $@
+	$(VERBOSE)$(CXX) -c $(OPTFLAGS) $(INCLUDES) $(CPPFLAGS) $(CXXFLAGS) $< -o $@
 
 %.d: %.c
 	@mkdir -p $(dir $@)
 	@echo "$(MSG_PREFIX)\`\` Generating dependency:" $(LOCAL_PATH)/$<
-	$(VERBOSE)$(ABCSRC)/depends.sh "$(CC)" `dirname $*.c` $(OPTFLAGS) $(INCLUDES) $(CFLAGS) $< > $@
+	$(VERBOSE)$(ABCSRC)/depends.sh "$(CC)" `dirname $*.c` $(OPTFLAGS) $(INCLUDES) $(CPPFLAGS) $(CFLAGS) $< > $@
 
 %.d: %.cc
 	@mkdir -p $(dir $@)
 	@echo "$(MSG_PREFIX)\`\` Generating dependency:" $(LOCAL_PATH)/$<
-	$(VERBOSE)$(ABCSRC)/depends.sh "$(CXX)" `dirname $*.cc` $(OPTFLAGS) $(INCLUDES) $(CXXFLAGS) $< > $@
+	$(VERBOSE)$(ABCSRC)/depends.sh "$(CXX)" `dirname $*.cc` $(OPTFLAGS) $(INCLUDES) $(CPPFLAGS) $(CXXFLAGS) $< > $@
 
 %.d: %.cpp
 	@mkdir -p $(dir $@)
 	@echo "$(MSG_PREFIX)\`\` Generating dependency:" $(LOCAL_PATH)/$<
-	$(VERBOSE)$(ABCSRC)/depends.sh "$(CXX)" `dirname $*.cpp` $(OPTFLAGS) $(INCLUDES) $(CXXFLAGS) $< > $@
+	$(VERBOSE)$(ABCSRC)/depends.sh "$(CXX)" `dirname $*.cpp` $(OPTFLAGS) $(INCLUDES) $(CPPFLAGS) $(CXXFLAGS) $< > $@
 
 ifndef ABC_MAKE_NO_DEPS
 -include $(DEP)

abclib.dsp

@@ -4801,6 +4801,22 @@ SOURCE=.\src\map\mpm\mpmTruth.c
 SOURCE=.\src\map\mpm\mpmUtil.c
 # End Source File
 # End Group
+# Begin Group "emap"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\map\emap\emap.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\emap\emap.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\emap\emapCore.c
+# End Source File
+# End Group
 # End Group
 # Begin Group "misc"
 
@@ -6665,6 +6681,10 @@ SOURCE=.\src\proof\cec\cecCorr.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\proof\cec\cecCorrIncr.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\proof\cec\cecInt.h
 # End Source File
 # Begin Source File

src/aig/gia/giaAiger.c

@@ -428,9 +428,6 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fGiaSi
                 }
                 else if ( *pType == 'l' )
                 {
-                    char Buffer[1000];
-                    assert( strlen(pName) < 995 );
-                    sprintf( Buffer, "%s_in", pName );
                     if ( vNamesRegIn == NULL )
                         vNamesRegIn = Vec_PtrStart( nLatches );
                     if ( vNamesRegOut == NULL )
@@ -440,7 +437,7 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fGiaSi
                         fError = 1;
                         break;
                     }
-                    Vec_PtrWriteEntry( vNamesRegIn,  iTerm, Abc_UtilStrsav(Buffer) );
+                    Vec_PtrWriteEntry( vNamesRegIn,  iTerm, Abc_UtilStrsavTwo(pName, (char *)"_in") );
                     Vec_PtrWriteEntry( vNamesRegOut, iTerm, Abc_UtilStrsav(pName) );
                 }
                 else if ( *pType == 'n' )

src/aig/gia/giaDup.c

@@ -6964,6 +6964,591 @@ void Gia_ManDupSplit( Gia_Man_t * p, int nParts, int nCutLevel )
     Vec_PtrFreeFree( vCutNames );
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Gia_ManDupPipelineMapPos( int nStages, int iObj, int iStage )
+{
+    return iObj * nStages + iStage;
+}
+
+static int Gia_ManDupPipelineDelayLit( Gia_Man_t * pNew, Vec_Int_t * vLitMap, Vec_Int_t * vStages, Vec_Int_t * vRegDrivers, Vec_Int_t * vRegStages, int nStages, int iObj, int iStage )
+{
+    int iPos, iStageBase, iLitPrev, iLit;
+    if ( iObj == 0 )
+        return 0;
+    iPos = Gia_ManDupPipelineMapPos( nStages, iObj, iStage );
+    iLit = Vec_IntEntry( vLitMap, iPos );
+    if ( iLit >= 0 )
+        return iLit;
+    iStageBase = Vec_IntEntry( vStages, iObj );
+    assert( iStage >= iStageBase );
+    assert( iStage > 0 );
+    iLitPrev = Gia_ManDupPipelineDelayLit( pNew, vLitMap, vStages, vRegDrivers, vRegStages, nStages, iObj, iStage - 1 );
+    iLit = Gia_ManAppendCi( pNew );
+    Vec_IntWriteEntry( vLitMap, iPos, iLit );
+    Vec_IntPush( vRegDrivers, iLitPrev );
+    Vec_IntPush( vRegStages, iStage - 1 );
+    return iLit;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static char * Gia_ManDupPipelineNameCopy( Vec_Ptr_t * vNames, int iName, char * pPrefix, int i )
+{
+    char * pName = (vNames && iName < Vec_PtrSize(vNames)) ? (char *)Vec_PtrEntry(vNames, iName) : NULL;
+    return pName ? Abc_UtilStrsav( pName ) : Abc_UtilStrsavNum( pPrefix, i );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManDupPipeline( Gia_Man_t * p, int nLevels, int fVerbose )
+{
+    Gia_Man_t * pNew;
+    Gia_Obj_t * pObj;
+    Vec_Int_t * vStages, * vLitMap, * vRegDrivers, * vRegStages, * vStageCounts;
+    Vec_Ptr_t * vNamesIn, * vNamesOut;
+    char * pNameRo;
+    int nObjs, nLevelMax, nStageMax, nStageCols, i, iStage, iLit0, iLit1, iLit, iFlop;
+
+    if ( nLevels <= 0 )
+        return NULL;
+    if ( Gia_ManRegNum(p) > 0 )
+        return NULL;
+
+    Gia_ManLevelNum( p );
+    nObjs      = Gia_ManObjNum( p );
+    nLevelMax  = Gia_ManLevelNum( p );
+    nStageMax  = nLevelMax ? (nLevelMax - 1) / nLevels : 0;
+    nStageCols = nStageMax + 1;
+
+    vStages     = Vec_IntStart( nObjs );
+    vLitMap     = Vec_IntStartFull( nObjs * nStageCols );
+    vRegDrivers = Vec_IntAlloc( 1000 );
+    vRegStages  = Vec_IntAlloc( 1000 );
+
+    Gia_ManForEachAnd( p, pObj, i )
+        Vec_IntWriteEntry( vStages, Gia_ObjId(p, pObj), (Gia_ObjLevel(p, pObj) - 1) / nLevels );
+
+    pNew = Gia_ManStart( Gia_ManObjNum(p) + 2 * Gia_ManAndNum(p) );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    pNew->nConstrs = p->nConstrs;
+    Gia_ManHashAlloc( pNew );
+
+    Gia_ManForEachPi( p, pObj, i )
+    {
+        iLit = Gia_ManAppendCi( pNew );
+        Vec_IntWriteEntry( vLitMap, Gia_ManDupPipelineMapPos(nStageCols, Gia_ObjId(p, pObj), 0), iLit );
+    }
+
+    Gia_ManForEachAnd( p, pObj, i )
+    {
+        iStage = Vec_IntEntry( vStages, Gia_ObjId(p, pObj) );
+        iLit0 = Gia_ManDupPipelineDelayLit( pNew, vLitMap, vStages, vRegDrivers, vRegStages, nStageCols, Gia_ObjFaninId0p(p, pObj), iStage );
+        iLit1 = Gia_ManDupPipelineDelayLit( pNew, vLitMap, vStages, vRegDrivers, vRegStages, nStageCols, Gia_ObjFaninId1p(p, pObj), iStage );
+        iLit = Gia_ManHashAnd( pNew, Abc_LitNotCond(iLit0, Gia_ObjFaninC0(pObj)), Abc_LitNotCond(iLit1, Gia_ObjFaninC1(pObj)) );
+        Vec_IntWriteEntry( vLitMap, Gia_ManDupPipelineMapPos(nStageCols, Gia_ObjId(p, pObj), iStage), iLit );
+    }
+
+    Gia_ManForEachPo( p, pObj, i )
+    {
+        iLit = Gia_ManDupPipelineDelayLit( pNew, vLitMap, vStages, vRegDrivers, vRegStages, nStageCols, Gia_ObjFaninId0p(p, pObj), nStageMax );
+        Gia_ManAppendCo( pNew, Abc_LitNotCond(iLit, Gia_ObjFaninC0(pObj)) );
+    }
+
+    Vec_IntForEachEntry( vRegDrivers, iLit, i )
+        Gia_ManAppendCo( pNew, iLit );
+    Gia_ManSetRegNum( pNew, Vec_IntSize(vRegDrivers) );
+
+    vNamesIn = Vec_PtrAlloc( Gia_ManCiNum(pNew) );
+    vNamesOut = Vec_PtrAlloc( Gia_ManCoNum(pNew) );
+    vStageCounts = Vec_IntStart( nStageCols );
+    Gia_ManForEachPi( p, pObj, i )
+        Vec_PtrPush( vNamesIn, Gia_ManDupPipelineNameCopy(p->vNamesIn, i, (char *)"pi", i) );
+    Gia_ManForEachPo( p, pObj, i )
+        Vec_PtrPush( vNamesOut, Gia_ManDupPipelineNameCopy(p->vNamesOut, i, (char *)"po", i) );
+    Vec_IntForEachEntry( vRegStages, iStage, i )
+    {
+        char Buffer[64], BufferIn[64];
+        iFlop = Vec_IntEntry( vStageCounts, iStage );
+        Vec_IntWriteEntry( vStageCounts, iStage, iFlop + 1 );
+        snprintf( Buffer, sizeof(Buffer), "cut%d[%d]", iStage, iFlop );
+        snprintf( BufferIn, sizeof(BufferIn), "cut%d_in[%d]", iStage, iFlop );
+        pNameRo = Abc_UtilStrsav( Buffer );
+        Vec_PtrPush( vNamesIn, pNameRo );
+        Vec_PtrPush( vNamesOut, Abc_UtilStrsav( BufferIn ) );
+    }
+    pNew->vNamesIn = vNamesIn;
+    pNew->vNamesOut = vNamesOut;
+    Gia_ManHashStop( pNew );
+
+    if ( fVerbose )
+        Abc_Print( 1, "Inserted %d fixed-cut pipeline registers using D = %d.\n", Gia_ManRegNum(pNew), nLevels );
+
+    Vec_IntFree( vStages );
+    Vec_IntFree( vLitMap );
+    Vec_IntFree( vRegDrivers );
+    Vec_IntFree( vRegStages );
+    Vec_IntFree( vStageCounts );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static Vec_Ptr_t * Gia_ManDupUnpipelineNames( Vec_Ptr_t * vNames, int nNames )
+{
+    Vec_Ptr_t * vRes;
+    char * pName;
+    int i;
+    if ( vNames == NULL )
+        return NULL;
+    vRes = Vec_PtrAlloc( nNames );
+    for ( i = 0; i < nNames; i++ )
+    {
+        pName = i < Vec_PtrSize(vNames) ? (char *)Vec_PtrEntry( vNames, i ) : NULL;
+        Vec_PtrPush( vRes, pName ? Abc_UtilStrsav(pName) : NULL );
+    }
+    return vRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates selected names if present.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static Vec_Ptr_t * Gia_ManDupUnpipelineNamesUsed( Vec_Ptr_t * vNames, Vec_Bit_t * vUsed, int nNames )
+{
+    Vec_Ptr_t * vRes;
+    char * pName;
+    int i;
+    if ( vNames == NULL )
+        return NULL;
+    vRes = Vec_PtrAlloc( Vec_BitCount(vUsed) );
+    for ( i = 0; i < nNames; i++ )
+    {
+        if ( !Vec_BitEntry(vUsed, i) )
+            continue;
+        pName = i < Vec_PtrSize(vNames) ? (char *)Vec_PtrEntry( vNames, i ) : NULL;
+        Vec_PtrPush( vRes, pName ? Abc_UtilStrsav(pName) : NULL );
+    }
+    return vRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static int Gia_ManDupUnpipeline_rec( Gia_Man_t * pNew, Gia_Man_t * p, Vec_Int_t * vCopies, int iObj, int * piCycle )
+{
+    Gia_Obj_t * pObj = Gia_ManObj( p, iObj );
+    int iLit, iLit0, iLit1;
+
+    iLit = Vec_IntEntry( vCopies, iObj );
+    if ( iLit >= 0 )
+        return iLit;
+    if ( iLit == -2 )
+    {
+        if ( piCycle )
+            *piCycle = iObj;
+        return -1;
+    }
+    Vec_IntWriteEntry( vCopies, iObj, -2 );
+
+    if ( !p->fGiaSimple && Gia_ObjIsBuf(pObj) )
+    {
+        iLit0 = Gia_ManDupUnpipeline_rec( pNew, p, vCopies, Gia_ObjFaninId0p(p, pObj), piCycle );
+        if ( iLit0 < 0 )
+            return -1;
+        iLit = Abc_LitNotCond( iLit0, Gia_ObjFaninC0(pObj) );
+    }
+    else if ( Gia_ObjIsAnd(pObj) )
+    {
+        iLit0 = Gia_ManDupUnpipeline_rec( pNew, p, vCopies, Gia_ObjFaninId0p(p, pObj), piCycle );
+        if ( iLit0 < 0 )
+            return -1;
+        iLit1 = Gia_ManDupUnpipeline_rec( pNew, p, vCopies, Gia_ObjFaninId1p(p, pObj), piCycle );
+        if ( iLit1 < 0 )
+            return -1;
+        iLit = Gia_ManHashAnd( pNew, Abc_LitNotCond(iLit0, Gia_ObjFaninC0(pObj)), Abc_LitNotCond(iLit1, Gia_ObjFaninC1(pObj)) );
+    }
+    else if ( Gia_ObjIsRo(p, pObj) )
+    {
+        Gia_Obj_t * pObjRi = Gia_ObjRoToRi( p, pObj );
+        iLit0 = Gia_ManDupUnpipeline_rec( pNew, p, vCopies, Gia_ObjFaninId0p(p, pObjRi), piCycle );
+        if ( iLit0 < 0 )
+            return -1;
+        iLit = Abc_LitNotCond( iLit0, Gia_ObjFaninC0(pObjRi) );
+    }
+    else
+    {
+        assert( 0 );
+        return -1;
+    }
+
+    Vec_IntWriteEntry( vCopies, iObj, iLit );
+    return iLit;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Marks objects reachable after bypassing flops.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static int Gia_ManDupUnpipelineMark_rec( Gia_Man_t * p, Vec_Str_t * vMarks, Vec_Bit_t * vPisUsed, int iObj, int * piCycle )
+{
+    Gia_Obj_t * pObj = Gia_ManObj( p, iObj );
+    int Mark = Vec_StrEntry( vMarks, iObj );
+    if ( Mark == 2 )
+        return 0;
+    if ( Mark == 1 )
+    {
+        if ( piCycle )
+            *piCycle = iObj;
+        return -1;
+    }
+    if ( Gia_ObjIsConst0(pObj) )
+    {
+        Vec_StrWriteEntry( vMarks, iObj, 2 );
+        return 0;
+    }
+    if ( Gia_ObjIsPi(p, pObj) )
+    {
+        Vec_BitWriteEntry( vPisUsed, Gia_ObjCioId(pObj), 1 );
+        Vec_StrWriteEntry( vMarks, iObj, 2 );
+        return 0;
+    }
+
+    Vec_StrWriteEntry( vMarks, iObj, 1 );
+    if ( !p->fGiaSimple && Gia_ObjIsBuf(pObj) )
+    {
+        if ( Gia_ManDupUnpipelineMark_rec( p, vMarks, vPisUsed, Gia_ObjFaninId0p(p, pObj), piCycle ) < 0 )
+            return -1;
+    }
+    else if ( Gia_ObjIsAnd(pObj) )
+    {
+        if ( Gia_ManDupUnpipelineMark_rec( p, vMarks, vPisUsed, Gia_ObjFaninId0p(p, pObj), piCycle ) < 0 )
+            return -1;
+        if ( Gia_ManDupUnpipelineMark_rec( p, vMarks, vPisUsed, Gia_ObjFaninId1p(p, pObj), piCycle ) < 0 )
+            return -1;
+    }
+    else if ( Gia_ObjIsRo(p, pObj) )
+    {
+        Gia_Obj_t * pObjRi = Gia_ObjRoToRi( p, pObj );
+        if ( Gia_ManDupUnpipelineMark_rec( p, vMarks, vPisUsed, Gia_ObjFaninId0p(p, pObjRi), piCycle ) < 0 )
+            return -1;
+    }
+    else
+    {
+        assert( 0 );
+        return -1;
+    }
+    Vec_StrWriteEntry( vMarks, iObj, 2 );
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManDupUnpipeline( Gia_Man_t * p, int fVerbose )
+{
+    Gia_Man_t * pNew;
+    Gia_Obj_t * pObj;
+    Vec_Bit_t * vPisUsed;
+    Vec_Int_t * vCopies;
+    Vec_Str_t * vMarks;
+    int i, iLit, iCycle = -1, nRegs, nPisUsed = 0;
+
+    if ( Gia_ManRegNum(p) == 0 )
+        return Gia_ManDup( p );
+
+    nRegs = Gia_ManRegNum( p );
+    vPisUsed = Vec_BitStart( Gia_ManPiNum(p) );
+    vMarks = Vec_StrStart( Gia_ManObjNum(p) );
+    Gia_ManForEachPo( p, pObj, i )
+        if ( Gia_ManDupUnpipelineMark_rec( p, vMarks, vPisUsed, Gia_ObjFaninId0p(p, pObj), &iCycle ) < 0 )
+            break;
+    Vec_StrFree( vMarks );
+    if ( iCycle >= 0 )
+    {
+        if ( fVerbose )
+            Abc_Print( 1, "Bypassing flops creates a combinational cycle at object %d.\n", iCycle );
+        Vec_BitFree( vPisUsed );
+        return NULL;
+    }
+
+    vCopies = Vec_IntStartFull( Gia_ManObjNum(p) );
+    Vec_IntWriteEntry( vCopies, 0, 0 );
+
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    pNew->nConstrs = p->nConstrs;
+    pNew->vNamesIn = Gia_ManDupUnpipelineNamesUsed( p->vNamesIn, vPisUsed, Gia_ManPiNum(p) );
+    pNew->vNamesOut = Gia_ManDupUnpipelineNames( p->vNamesOut, Gia_ManPoNum(p) );
+    Gia_ManHashAlloc( pNew );
+
+    Gia_ManForEachPi( p, pObj, i )
+        if ( Vec_BitEntry(vPisUsed, i) )
+        {
+            Vec_IntWriteEntry( vCopies, Gia_ObjId(p, pObj), Gia_ManAppendCi(pNew) );
+            nPisUsed++;
+        }
+
+    Gia_ManForEachPo( p, pObj, i )
+    {
+        iLit = Gia_ManDupUnpipeline_rec( pNew, p, vCopies, Gia_ObjFaninId0p(p, pObj), &iCycle );
+        if ( iLit < 0 )
+            break;
+        Gia_ManAppendCo( pNew, Abc_LitNotCond(iLit, Gia_ObjFaninC0(pObj)) );
+    }
+    Gia_ManHashStop( pNew );
+    Vec_IntFree( vCopies );
+    Vec_BitFree( vPisUsed );
+
+    Gia_ManSetRegNum( pNew, 0 );
+    if ( fVerbose )
+        Abc_Print( 1, "Removed %d pipeline registers and kept %d primary inputs.\n", nRegs, nPisUsed );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static char * Gia_ManDupRegioNameCopy( Vec_Ptr_t * vNames, int iName )
+{
+    char * pName = (vNames && iName < Vec_PtrSize(vNames)) ? (char *)Vec_PtrEntry(vNames, iName) : NULL;
+    return pName ? Abc_UtilStrsav(pName) : NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static char * Gia_ManDupRegioNameNew( Vec_Ptr_t * vNames, int iName, char * pSuffix, char * pPrefix, int i )
+{
+    char * pName = (vNames && iName < Vec_PtrSize(vNames)) ? (char *)Vec_PtrEntry(vNames, iName) : NULL;
+    return pName ? Abc_UtilStrsavTwo( pName, pSuffix ) : Abc_UtilStrsavNum( pPrefix, i );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManDupRegio( Gia_Man_t * p, int fRegIns, int fRegOuts, int fVerbose )
+{
+    Gia_Man_t * pNew;
+    Gia_Obj_t * pObj;
+    Vec_Int_t * vInRos = NULL, * vOutRos = NULL;
+    Vec_Ptr_t * vNamesIn = NULL, * vNamesOut = NULL;
+    int nPis = Gia_ManPiNum(p), nPos = Gia_ManPoNum(p), nRegs = Gia_ManRegNum(p);
+    int nRegIns = fRegIns ? nPis : 0;
+    int nRegOuts = fRegOuts ? nPos : 0;
+    int nRegsNew = nRegs + nRegIns + nRegOuts;
+    int i;
+
+    if ( !fRegIns && !fRegOuts )
+        return Gia_ManDup( p );
+
+    pNew = Gia_ManStart( Gia_ManObjNum(p) + 2 * (nRegIns + nRegOuts) );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    pNew->nConstrs = p->nConstrs;
+
+    if ( p->vRegClasses )
+    {
+        pNew->vRegClasses = Vec_IntAlloc( nRegsNew );
+        for ( i = 0; i < nRegs; i++ )
+            Vec_IntPush( pNew->vRegClasses, Vec_IntEntry(p->vRegClasses, i) );
+        for ( ; i < nRegsNew; i++ )
+            Vec_IntPush( pNew->vRegClasses, 0 );
+    }
+    if ( p->vFlopClasses )
+    {
+        pNew->vFlopClasses = Vec_IntAlloc( nRegsNew );
+        for ( i = 0; i < nRegs; i++ )
+            Vec_IntPush( pNew->vFlopClasses, Vec_IntEntry(p->vFlopClasses, i) );
+        for ( ; i < nRegsNew; i++ )
+            Vec_IntPush( pNew->vFlopClasses, 0 );
+    }
+    if ( p->vRegInits )
+    {
+        pNew->vRegInits = Vec_IntAlloc( nRegsNew );
+        for ( i = 0; i < nRegs; i++ )
+            Vec_IntPush( pNew->vRegInits, Vec_IntEntry(p->vRegInits, i) );
+        for ( ; i < nRegsNew; i++ )
+            Vec_IntPush( pNew->vRegInits, 0 );
+    }
+
+    if ( p->vNamesIn )
+    {
+        vNamesIn = Vec_PtrAlloc( nPis + nRegsNew );
+        for ( i = 0; i < nPis; i++ )
+            Vec_PtrPush( vNamesIn, Gia_ManDupRegioNameCopy(p->vNamesIn, i) );
+        for ( i = 0; i < nRegs; i++ )
+            Vec_PtrPush( vNamesIn, Gia_ManDupRegioNameCopy(p->vNamesIn, nPis + i) );
+        if ( fRegIns )
+            for ( i = 0; i < nPis; i++ )
+                Vec_PtrPush( vNamesIn, Gia_ManDupRegioNameNew(p->vNamesIn, i, (char *)"_i_ro", (char *)"inro", i) );
+        if ( fRegOuts )
+            for ( i = 0; i < nPos; i++ )
+                Vec_PtrPush( vNamesIn, Gia_ManDupRegioNameNew(p->vNamesOut, i, (char *)"_o_ro", (char *)"outro", i) );
+        pNew->vNamesIn = vNamesIn;
+    }
+    if ( p->vNamesOut )
+    {
+        vNamesOut = Vec_PtrAlloc( nPos + nRegsNew );
+        for ( i = 0; i < nPos; i++ )
+            Vec_PtrPush( vNamesOut, Gia_ManDupRegioNameCopy(p->vNamesOut, i) );
+        for ( i = 0; i < nRegs; i++ )
+            Vec_PtrPush( vNamesOut, Gia_ManDupRegioNameCopy(p->vNamesOut, nPos + i) );
+        if ( fRegIns )
+            for ( i = 0; i < nPis; i++ )
+                Vec_PtrPush( vNamesOut, Gia_ManDupRegioNameNew(p->vNamesIn, i, (char *)"_i_ri", (char *)"inri", i) );
+        if ( fRegOuts )
+            for ( i = 0; i < nPos; i++ )
+                Vec_PtrPush( vNamesOut, Gia_ManDupRegioNameNew(p->vNamesOut, i, (char *)"_o_ri", (char *)"outri", i) );
+        pNew->vNamesOut = vNamesOut;
+    }
+
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManForEachPi( p, pObj, i )
+        pObj->Value = Gia_ManAppendCi( pNew );
+    Gia_ManForEachRo( p, pObj, i )
+        pObj->Value = Gia_ManAppendCi( pNew );
+
+    if ( fRegIns )
+    {
+        vInRos = Vec_IntAlloc( nPis );
+        Gia_ManForEachPi( p, pObj, i )
+            Vec_IntPush( vInRos, Gia_ManAppendCi( pNew ) );
+        Gia_ManForEachPi( p, pObj, i )
+            pObj->Value = Vec_IntEntry( vInRos, i );
+    }
+    if ( fRegOuts )
+    {
+        vOutRos = Vec_IntAlloc( nPos );
+        for ( i = 0; i < nPos; i++ )
+            Vec_IntPush( vOutRos, Gia_ManAppendCi( pNew ) );
+    }
+
+    Gia_ManForEachObj1( p, pObj, i )
+    {
+        if ( !p->fGiaSimple && Gia_ObjIsBuf(pObj) )
+            pObj->Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) );
+        else if ( Gia_ObjIsAnd(pObj) )
+            pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    }
+
+    Gia_ManForEachPo( p, pObj, i )
+    {
+        if ( fRegOuts )
+            Gia_ManAppendCo( pNew, Vec_IntEntry(vOutRos, i) );
+        else
+            Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    }
+    Gia_ManForEachRi( p, pObj, i )
+        Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    if ( fRegIns )
+        for ( i = 0; i < nPis; i++ )
+            Gia_ManAppendCo( pNew, Gia_ManCiLit(pNew, i) );
+    if ( fRegOuts )
+        Gia_ManForEachPo( p, pObj, i )
+            Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+
+    Gia_ManSetRegNum( pNew, nRegsNew );
+    Vec_IntFreeP( &vInRos );
+    Vec_IntFreeP( &vOutRos );
+
+    if ( fVerbose )
+        Abc_Print( 1, "Added %d input flops and %d output flops (total regs = %d).\n", nRegIns, nRegOuts, nRegsNew );
+    return pNew;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/aig/gia/giaIf.c

@@ -3010,9 +3010,19 @@ Gia_Man_t * Gia_ManPerformMappingInt( Gia_Man_t * p, If_Par_t * pPars )
     if ( p->pManTime && pPars->pTimesReq == NULL )
     {
         Tim_Man_t * pManTime = (Tim_Man_t *)p->pManTime;
-        pPars->pTimesReq = ABC_CALLOC( float, Gia_ManCoNum(p) );
+        int fHasFiniteReq = 0;
         for ( i = 0; i < Gia_ManCoNum(p); i++ )
-            pPars->pTimesReq[i] = Tim_ManGetCoRequired( pManTime, i );
+            if ( Tim_ManGetCoRequired( pManTime, i ) < TIM_ETERNITY )
+            {
+                fHasFiniteReq = 1;
+                break;
+            }
+        if ( fHasFiniteReq )
+        {
+            pPars->pTimesReq = ABC_CALLOC( float, Gia_ManCoNum(p) );
+            for ( i = 0; i < Gia_ManCoNum(p); i++ )
+                pPars->pTimesReq[i] = Tim_ManGetCoRequired( pManTime, i );
+        }
     }
     ABC_FREE( p->pCellStr );
     Vec_IntFreeP( &p->vConfigs );

src/base/abc/abcHieGia.c

@@ -686,6 +686,32 @@ static Vec_Int_t * GiaHie_CountSymbsAll( Vec_Ptr_t * vNames )
     }
     return vArray;
 }
+static Vec_Int_t * GiaHie_CountSymbsSome( Vec_Ptr_t * vNames, int nNames )
+{
+    char * pNameLast, * pName;
+    int i, nSymbsLast;
+    Vec_Int_t * vArray;
+    assert( vNames != NULL );
+    assert( nNames >= 0 && nNames <= Vec_PtrSize(vNames) );
+    if ( nNames == 0 )
+        return Vec_IntAlloc( 0 );
+    pNameLast = (char *)Vec_PtrEntry( vNames, 0 );
+    nSymbsLast = GiaHie_CountSymbs( pNameLast );
+    vArray = Vec_IntAlloc( nNames * 2 );
+    Vec_IntPush( vArray, 0 );
+    Vec_IntPush( vArray, nSymbsLast );
+    for ( i = 1; i < nNames; i++ )
+    {
+        pName = (char *)Vec_PtrEntry( vNames, i );
+        if ( GiaHie_CountSymbs(pName) == nSymbsLast && !strncmp(pName, pNameLast, nSymbsLast) )
+            continue;
+        nSymbsLast = GiaHie_CountSymbs( pName );
+        Vec_IntPush( vArray, i );
+        Vec_IntPush( vArray, nSymbsLast );
+        pNameLast = pName;
+    }
+    return vArray;
+}
 static void GiaHie_DumpIoList( Gia_Man_t * p, FILE * pFile, int fOuts, int fReverse )
 {
     Vec_Ptr_t * vNames = fOuts ? p->vNamesOut : p->vNamesIn;
@@ -1013,6 +1039,88 @@ static int GiaHie_IsBitLevelNames( Vec_Ptr_t * vNames )
     Vec_IntFree( vArray );
     return 1;
 }
+static int GiaHie_IsBitLevelNamesSome( Vec_Ptr_t * vNames, int nNames )
+{
+    int nGroups, idx;
+    Vec_Int_t * vArray;
+    if ( vNames == NULL )
+        return 1;
+    if ( nNames == 0 )
+        return 1;
+    vArray = GiaHie_CountSymbsSome( vNames, nNames );
+    nGroups = Vec_IntSize(vArray) / 2;
+    for ( idx = 0; idx < nGroups; idx++ )
+    {
+        int iName = Vec_IntEntry( vArray, 2*idx );
+        int iNameNext = (idx + 1 < nGroups) ? Vec_IntEntry(vArray, 2*(idx + 1)) : nNames;
+        if ( iNameNext - iName > 1 )
+        {
+            Vec_IntFree( vArray );
+            return 0;
+        }
+    }
+    Vec_IntFree( vArray );
+    return 1;
+}
+static void GiaHie_DumpPortDeclsOneSome( Vec_Ptr_t * vNames, int nBits, FILE * pFile, int fOuts, int * pfFirst )
+{
+    int fUsePiPo = (nBits > 2) && GiaHie_IsBitLevelNamesSome( vNames, nBits );
+    if ( nBits == 0 )
+        return;
+    if ( fUsePiPo )
+    {
+        int nDigits = Abc_Base10Log( nBits );
+        if ( nDigits < 2 )
+            nDigits = 2;
+        if ( !(*pfFirst) )
+            fprintf( pFile, ",\n" );
+        fprintf( pFile, "  %s ", fOuts ? "output" : "input" );
+        GiaHie_WritePiPoNames( pFile, fOuts ? "po" : "pi", nBits, nDigits, 8, 4, 0 );
+        *pfFirst = 0;
+        return;
+    }
+    if ( vNames == NULL )
+    {
+        if ( !(*pfFirst) )
+            fprintf( pFile, ",\n" );
+        fprintf( pFile, "  %s [%d:0] _%c_", fOuts ? "output" : "input", nBits-1, fOuts ? 'o' : 'i' );
+        *pfFirst = 0;
+        return;
+    }
+    {
+        Vec_Int_t * vArray = GiaHie_CountSymbsSome( vNames, nBits );
+        int iName, Size, i;
+        Vec_IntForEachEntryDouble( vArray, iName, Size, i )
+        {
+            int iNameNext = Vec_IntSize(vArray) > i+2 ? Vec_IntEntry(vArray, i+2) : nBits;
+            char * pName = (char *)Vec_PtrEntry(vNames, iName);
+            char * pNameLast = (char *)Vec_PtrEntry(vNames, iNameNext-1);
+            int NumBeg, NumEnd;
+            assert( !strncmp(pName, pNameLast, Size) );
+            NumBeg = GiaHie_ReadRangeNum( pName, Size );
+            NumEnd = GiaHie_ReadRangeNum( pNameLast, Size );
+            if ( !(*pfFirst) )
+                fprintf( pFile, ",\n" );
+            fprintf( pFile, "  %s ", fOuts ? "output" : "input" );
+            if ( NumBeg != -1 && iName < iNameNext-1 )
+                fprintf( pFile, "[%d:%d] ", NumEnd, NumBeg );
+            GiaHie_PrintOneName( pFile, pName, Size );
+            *pfFirst = 0;
+        }
+        Vec_IntFree( vArray );
+    }
+}
+static void GiaHie_DumpPortDeclsSeq( Gia_Man_t * p, FILE * pFile, int fUseCtrlPis )
+{
+    int fFirst = fUseCtrlPis ? 1 : 0;
+    if ( !fUseCtrlPis )
+    {
+        fprintf( pFile, "  input clk,\n" );
+        fprintf( pFile, "  input rst" );
+    }
+    GiaHie_DumpPortDeclsOneSome( p->vNamesIn, Gia_ManPiNum(p), pFile, 0, &fFirst );
+    GiaHie_DumpPortDeclsOneSome( p->vNamesOut, Gia_ManPoNum(p), pFile, 1, &fFirst );
+}
 static void GiaHie_DumpPortDeclsOne( Gia_Man_t * p, FILE * pFile, int fOuts, int * pfFirst )
 {
     Vec_Ptr_t * vNames = fOuts ? p->vNamesOut : p->vNamesIn;
@@ -1205,6 +1313,224 @@ static void GiaHie_DumpOutputAssigns( Gia_Man_t * p, FILE * pFile, int nDigits )
         Vec_IntFree( vArray );
     }
 }
+static void GiaHie_DumpInputAssignsSome( Gia_Man_t * p, FILE * pFile, int nDigits, int nCis )
+{
+    Vec_Ptr_t * vNames = p->vNamesIn;
+    int fUsePiPo = (nCis > 2) && GiaHie_IsBitLevelNamesSome( vNames, nCis );
+    if ( nCis == 0 )
+        return;
+    if ( fUsePiPo )
+    {
+        int nDigitsPi = Abc_Base10Log( nCis );
+        if ( nDigitsPi < 2 )
+            nDigitsPi = 2;
+        fprintf( pFile, "  assign { " );
+        GiaHie_WriteObjRange( pFile, p, 0, nCis, nDigits, 11, 4, 1, 1 );
+        fprintf( pFile, " } =\n    { " );
+        GiaHie_WritePiPoNames( pFile, "pi", nCis, nDigitsPi, 18, 4, 1 );
+        fprintf( pFile, " };\n" );
+        return;
+    }
+    if ( vNames == NULL )
+    {
+        if ( nCis == 1 )
+        {
+            fprintf( pFile, "  assign " );
+            GiaHie_PrintObjName( pFile, Gia_ManCiIdToId(p, 0), nDigits );
+            fprintf( pFile, " = _i_;\n" );
+        }
+        else
+        {
+            fprintf( pFile, "  assign { " );
+            GiaHie_WriteObjRange( pFile, p, 0, nCis, nDigits, 11, 4, 1, 1 );
+            fprintf( pFile, " } = { _i_ };\n" );
+        }
+        return;
+    }
+    {
+        Vec_Int_t * vArray = GiaHie_CountSymbsSome( vNames, nCis );
+        int iName, Size, i;
+        Vec_IntForEachEntryDouble( vArray, iName, Size, i )
+        {
+            int iNameNext = Vec_IntSize(vArray) > i+2 ? Vec_IntEntry(vArray, i+2) : nCis;
+            int nBits = iNameNext - iName;
+            char * pName = (char *)Vec_PtrEntry(vNames, iName);
+            if ( nBits > 1 )
+            {
+                fprintf( pFile, "  assign { " );
+                GiaHie_WriteObjRange( pFile, p, iName, iNameNext, nDigits, 11, 4, 1, 1 );
+                fprintf( pFile, " } =\n    { " );
+                GiaHie_PrintOneName( pFile, pName, Size );
+                fprintf( pFile, " };\n" );
+            }
+            else
+            {
+                fprintf( pFile, "  assign " );
+                GiaHie_PrintObjName( pFile, Gia_ManCiIdToId(p, iName), nDigits );
+                fprintf( pFile, " = " );
+                GiaHie_PrintOneName( pFile, pName, Size );
+                fprintf( pFile, ";\n" );
+            }
+        }
+        Vec_IntFree( vArray );
+    }
+}
+static void GiaHie_DumpOutputAssignsSome( Gia_Man_t * p, FILE * pFile, int nDigits, int nCos )
+{
+    Vec_Ptr_t * vNames = p->vNamesOut;
+    int fUsePiPo = (nCos > 2) && GiaHie_IsBitLevelNamesSome( vNames, nCos );
+    if ( nCos == 0 )
+        return;
+    if ( fUsePiPo )
+    {
+        int nDigitsPo = Abc_Base10Log( nCos );
+        if ( nDigitsPo < 2 )
+            nDigitsPo = 2;
+        fprintf( pFile, "  assign { " );
+        GiaHie_WritePiPoNames( pFile, "po", nCos, nDigitsPo, 11, 4, 1 );
+        fprintf( pFile, " } =\n    { " );
+        GiaHie_WriteObjRange( pFile, p, 0, nCos, nDigits, 18, 4, 1, 0 );
+        fprintf( pFile, " };\n" );
+        return;
+    }
+    if ( vNames == NULL )
+    {
+        if ( nCos == 1 )
+        {
+            fprintf( pFile, "  assign _o_ = " );
+            GiaHie_PrintObjName( pFile, Gia_ManCoIdToId(p, 0), nDigits );
+            fprintf( pFile, ";\n" );
+        }
+        else
+        {
+            fprintf( pFile, "  assign { _o_ } = { " );
+            GiaHie_WriteObjRange( pFile, p, 0, nCos, nDigits, 18, 4, 1, 0 );
+            fprintf( pFile, " };\n" );
+        }
+        return;
+    }
+    {
+        Vec_Int_t * vArray = GiaHie_CountSymbsSome( vNames, nCos );
+        int iName, Size, i;
+        Vec_IntForEachEntryDouble( vArray, iName, Size, i )
+        {
+            int iNameNext = Vec_IntSize(vArray) > i+2 ? Vec_IntEntry(vArray, i+2) : nCos;
+            int nBits = iNameNext - iName;
+            char * pName = (char *)Vec_PtrEntry(vNames, iName);
+            if ( nBits > 1 )
+            {
+                fprintf( pFile, "  assign { " );
+                GiaHie_PrintOneName( pFile, pName, Size );
+                fprintf( pFile, " } =\n    { " );
+                GiaHie_WriteObjRange( pFile, p, iName, iNameNext, nDigits, 18, 4, 1, 0 );
+                fprintf( pFile, " };\n" );
+            }
+            else
+            {
+                fprintf( pFile, "  assign " );
+                GiaHie_PrintOneName( pFile, pName, Size );
+                fprintf( pFile, " = " );
+                GiaHie_PrintObjName( pFile, Gia_ManCoIdToId(p, iName), nDigits );
+                fprintf( pFile, ";\n" );
+            }
+        }
+        Vec_IntFree( vArray );
+    }
+}
+static void GiaHie_DumpInterfaceAssignsSeq( Gia_Man_t * p, char * pFileName, int fUseCtrlPis )
+{
+    Gia_Obj_t * pObj, * pObjRi, * pObjRo;
+    int nDigits = Abc_Base10Log( Gia_ManObjNum(p) );
+    int nPerLine = 4, nOnLine = 0;
+    int i;
+    FILE * pFile;
+    if ( fUseCtrlPis && Gia_ManPiNum(p) < 2 )
+    {
+        printf( "Sequential Verilog with \"-c\" expects at least 2 primary inputs.\n" );
+        return;
+    }
+    pFile = fopen( pFileName, "wb" );
+    if ( pFile == NULL )
+    {
+        printf( "Cannot open output file \"%s\".\n", pFileName );
+        return;
+    }
+
+    fprintf( pFile, "module " );
+    GiaHie_DumpModuleName( pFile, p->pName );
+    fprintf( pFile, " (\n" );
+    GiaHie_DumpPortDeclsSeq( p, pFile, fUseCtrlPis );
+    fprintf( pFile, "\n);\n\n" );
+
+    if ( Gia_ManPiNum(p) )
+    {
+        fprintf( pFile, "  wire " );
+        GiaHie_WriteObjRange( pFile, p, 0, Gia_ManPiNum(p), nDigits, 7, 4, 0, 1 );
+        fprintf( pFile, ";\n\n" );
+        GiaHie_DumpInputAssignsSome( p, pFile, nDigits, Gia_ManPiNum(p) );
+        fprintf( pFile, "\n" );
+    }
+    if ( Gia_ManCoNum(p) )
+    {
+        fprintf( pFile, "  wire " );
+        GiaHie_WriteObjRange( pFile, p, 0, Gia_ManCoNum(p), nDigits, 7, 4, 0, 0 );
+        fprintf( pFile, ";\n\n" );
+    }
+    if ( Gia_ManRegNum(p) )
+    {
+        fprintf( pFile, "  reg  " );
+        GiaHie_WriteObjRange( pFile, p, Gia_ManPiNum(p), Gia_ManCiNum(p), nDigits, 7, 4, 0, 1 );
+        fprintf( pFile, ";\n\n" );
+    }
+
+    if ( GiaHie_ConstUsed(p) )
+        fprintf( pFile, "  wire n%0*d = 1'b0;\n\n", nDigits, 0 );
+
+    Gia_ManForEachAnd( p, pObj, i )
+    {
+        if ( nOnLine == 0 )
+            fprintf( pFile, "  " );
+        fprintf( pFile, "wire n%0*d = ", nDigits, i );
+        GiaHie_PrintObjLit( pFile, Gia_ObjFaninId0(pObj, i), Gia_ObjFaninC0(pObj), nDigits );
+        fprintf( pFile, " & " );
+        GiaHie_PrintObjLit( pFile, Gia_ObjFaninId1(pObj, i), Gia_ObjFaninC1(pObj), nDigits );
+        fprintf( pFile, "; " );
+        nOnLine++;
+        if ( nOnLine == nPerLine )
+        {
+            fprintf( pFile, "\n" );
+            nOnLine = 0;
+        }
+        else
+            fprintf( pFile, " " );
+    }
+    if ( nOnLine != 0 )
+        fprintf( pFile, "\n" );
+    if ( Gia_ManAndNum(p) )
+        fprintf( pFile, "\n" );
+
+    Gia_ManForEachCo( p, pObj, i )
+    {
+        fprintf( pFile, "  assign n%0*d = ", nDigits, Gia_ManCoIdToId(p, i) );
+        GiaHie_PrintObjLit( pFile, Gia_ObjFaninId0p(p, pObj), Gia_ObjFaninC0(pObj), nDigits );
+        fprintf( pFile, ";\n" );
+    }
+    fprintf( pFile, "\n" );
+    GiaHie_DumpOutputAssignsSome( p, pFile, nDigits, Gia_ManPoNum(p) );
+    fprintf( pFile, "\n" );
+
+    fprintf( pFile, "  always @(posedge " );
+    if ( fUseCtrlPis )
+        GiaHie_PrintObjName( pFile, Gia_ManCiIdToId(p, 0), nDigits );
+    else
+        fprintf( pFile, "clk" );
+    fprintf( pFile, ") begin\n" );
+    Gia_ManForEachRiRo( p, pObjRi, pObjRo, i )
+        fprintf( pFile, "      n%0*d <= n%0*d;\n", nDigits, Gia_ObjId(p, pObjRo), nDigits, Gia_ObjId(p, pObjRi) );
+    fprintf( pFile, "  end\n\n" );
+    fprintf( pFile, "endmodule\n\n" );
+    fclose( pFile );
+}
 
 /**Function*************************************************************
 
@@ -1217,13 +1543,18 @@ static void GiaHie_DumpOutputAssigns( Gia_Man_t * p, FILE * pFile, int nDigits )
   SeeAlso     []
 
 ***********************************************************************/
-static void GiaHie_DumpInterfaceAssigns( Gia_Man_t * p, char * pFileName )
+static void GiaHie_DumpInterfaceAssigns( Gia_Man_t * p, char * pFileName, int fUseCtrlPis )
 {
     Gia_Obj_t * pObj;
     int nDigits = Abc_Base10Log( Gia_ManObjNum(p) );
     int nPerLine = 4;
     int nOnLine = 0;
     int i;
+    if ( Gia_ManRegNum(p) > 0 )
+    {
+        GiaHie_DumpInterfaceAssignsSeq( p, pFileName, fUseCtrlPis );
+        return;
+    }
     FILE * pFile = fopen( pFileName, "wb" );
     if ( pFile == NULL )
     {
@@ -1494,7 +1825,7 @@ static void GiaHie_DumpMappedLuts( Gia_Man_t * p, char * pFileName )
   SeeAlso     []
 
 ***********************************************************************/
-void Gia_WriteVerilog( char * pFileName, Gia_Man_t * pGia, int fUseGates, int fVerbose )
+void Gia_WriteVerilogInt( char * pFileName, Gia_Man_t * pGia, int fUseGates, int fVerbose, int fUseCtrlPis )
 {
     (void)fVerbose;
     if ( pFileName == NULL || pGia == NULL )
@@ -1502,7 +1833,12 @@ void Gia_WriteVerilog( char * pFileName, Gia_Man_t * pGia, int fUseGates, int fV
     if ( fUseGates )
         GiaHie_DumpInterfaceGates( pGia, pFileName );
     else
-        GiaHie_DumpInterfaceAssigns( pGia, pFileName );
+        GiaHie_DumpInterfaceAssigns( pGia, pFileName, fUseCtrlPis );
+}
+
+void Gia_WriteVerilog( char * pFileName, Gia_Man_t * pGia, int fUseGates, int fVerbose )
+{
+    Gia_WriteVerilogInt( pFileName, pGia, fUseGates, fVerbose, 0 );
 }
 
 /**Function*************************************************************

src/base/abc/abcNtk.c

@@ -39,6 +39,86 @@ ABC_NAMESPACE_IMPL_START
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+static int Abc_NtkDupDfsSameFanins( Abc_Obj_t * pObj0, Abc_Obj_t * pObj1 )
+{
+    Abc_Obj_t * pFanin0, * pFanin1;
+    int i;
+    if ( pObj0 == NULL || pObj1 == NULL || Abc_ObjFaninNum(pObj0) != Abc_ObjFaninNum(pObj1) )
+        return 0;
+    Abc_ObjForEachFanin( pObj0, pFanin0, i )
+    {
+        pFanin1 = Abc_ObjFanin( pObj1, i );
+        if ( pFanin0 != pFanin1 )
+            return 0;
+    }
+    return 1;
+}
+static Abc_Obj_t * Abc_NtkDupDfsFindTwin( Vec_Ptr_t * vNodes, Vec_Int_t * vSeen, Abc_Obj_t * pObj )
+{
+    Mio_Gate_t * pGate = (Mio_Gate_t *)pObj->pData;
+    Abc_Obj_t * pObj2;
+    int i;
+    if ( pGate == NULL || Mio_GateReadTwin(pGate) == NULL )
+        return NULL;
+    Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj2, i )
+    {
+        if ( pObj2 == pObj || Vec_IntEntry(vSeen, Abc_ObjId(pObj2)) )
+            continue;
+        if ( (Mio_Gate_t *)pObj2->pData != Mio_GateReadTwin(pGate) )
+            continue;
+        if ( Abc_NtkDupDfsSameFanins(pObj, pObj2) )
+            return pObj2;
+    }
+    return NULL;
+}
+static Vec_Ptr_t * Abc_NtkDupDfsOrderTwinNodes( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes )
+{
+    Vec_Int_t * vSeen;
+    Vec_Ptr_t * vRes;
+    Abc_Obj_t * pObj, * pTwin;
+    Mio_Gate_t * pGate, * pGateBase;
+    int i;
+    if ( !Abc_NtkHasMapping(pNtk) || pNtk->pManFunc == NULL )
+        return vNodes;
+    vSeen = Vec_IntStart( Abc_NtkObjNumMax(pNtk) );
+    vRes = Vec_PtrAlloc( Vec_PtrSize(vNodes) );
+    Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
+    {
+        if ( Vec_IntEntry(vSeen, Abc_ObjId(pObj)) )
+            continue;
+        pGate = (Mio_Gate_t *)pObj->pData;
+        if ( pGate == NULL || Mio_GateReadTwin(pGate) == NULL )
+        {
+            Vec_PtrPush( vRes, pObj );
+            Vec_IntWriteEntry( vSeen, Abc_ObjId(pObj), 1 );
+            continue;
+        }
+        pTwin = Abc_NtkDupDfsFindTwin( vNodes, vSeen, pObj );
+        if ( pTwin == NULL )
+        {
+            Vec_PtrPush( vRes, pObj );
+            Vec_IntWriteEntry( vSeen, Abc_ObjId(pObj), 1 );
+            continue;
+        }
+        pGateBase = Mio_LibraryReadGateByName( (Mio_Library_t *)pNtk->pManFunc, Mio_GateReadName(pGate), NULL );
+        if ( pGateBase == (Mio_Gate_t *)pTwin->pData )
+        {
+            Vec_PtrPush( vRes, pTwin );
+            Vec_PtrPush( vRes, pObj );
+        }
+        else
+        {
+            Vec_PtrPush( vRes, pObj );
+            Vec_PtrPush( vRes, pTwin );
+        }
+        Vec_IntWriteEntry( vSeen, Abc_ObjId(pObj), 1 );
+        Vec_IntWriteEntry( vSeen, Abc_ObjId(pTwin), 1 );
+    }
+    Vec_IntFree( vSeen );
+    Vec_PtrFree( vNodes );
+    return vRes;
+}
+
 /**Function*************************************************************
 
   Synopsis    [Creates a new Ntk.]
@@ -548,6 +628,7 @@ Abc_Ntk_t * Abc_NtkDupDfs( Abc_Ntk_t * pNtk )
     pNtkNew = Abc_NtkStartFrom( pNtk, pNtk->ntkType, pNtk->ntkFunc );
     // copy the internal nodes
     vNodes = Abc_NtkDfs( pNtk, 0 );
+    vNodes = Abc_NtkDupDfsOrderTwinNodes( pNtk, vNodes );
     Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
         Abc_NtkDupObj( pNtkNew, pObj, 0 );
     Vec_PtrFree( vNodes );
@@ -2621,4 +2702,3 @@ Abc_Ntk_t * Abc_NtkCreateFromGias( char * pName, Vec_Ptr_t * vGias, Gia_Man_t *
 
 
 ABC_NAMESPACE_IMPL_END
-

src/base/abci/abc.c

@@ -662,6 +662,9 @@ static int Abc_CommandAbc9BsFind             ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandAbc9AndCare            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Cuts               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Divide             ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Pipeline           ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Unpipeline         ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Regio              ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandAbc9Test               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
@@ -687,7 +690,7 @@ extern void Extra_BitMatrixTransposeP( Vec_Wrd_t * vSimsIn, int nWordsIn, Vec_Wr
 typedef struct Wlc_Ntk_t_    Wlc_Ntk_t;
 typedef struct Wlc_BstPar_t_ Wlc_BstPar_t;
 extern Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pPars );
-extern int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, int nTimeOut3, int fUseUif, Wlc_Ntk_t * pWlc, int fVerbose, int fVeryVerbose, int fSilent, char * pReplayFile );
+extern int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, int nTimeOut3, int fUseUif, Wlc_Ntk_t * pWlc, int fVerbose, int fVeryVerbose, int fSilent, char * pReplayFile, char * pUfarArgs );
 extern int Cec_GiaReplayReadParams( char * pFileName, int * pnProcs, int * pnTimeOut, int * pnTimeOut2, int * pnTimeOut3, int * pfUseUif );
 extern int Cec_GiaReplayTest( Gia_Man_t * p, Wlc_Ntk_t * pWlc, char * pFileName, int fVerbose, int fVeryVerbose, int fSilent );
 
@@ -1515,6 +1518,9 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC9",         "&andcare",      Abc_CommandAbc9AndCare,                0 );   
     Cmd_CommandAdd( pAbc, "ABC9",         "&cuts",         Abc_CommandAbc9Cuts,                   0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&divide",       Abc_CommandAbc9Divide,                 0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&pipe",         Abc_CommandAbc9Pipeline,               0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&unpipe",       Abc_CommandAbc9Unpipeline,             0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&regio",        Abc_CommandAbc9Regio,                  0 );
 
     Cmd_CommandAdd( pAbc, "ABC9",         "&test",         Abc_CommandAbc9Test,                   0 );
 
@@ -35155,18 +35161,19 @@ usage:
 ***********************************************************************/
 int Abc_CommandAbc9WriteVer( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    extern void Gia_WriteVerilog( char * pFileName, Gia_Man_t * pGia, int fUseGates, int fVerbose );
+    extern void Gia_WriteVerilogInt( char * pFileName, Gia_Man_t * pGia, int fUseGates, int fVerbose, int fUseCtrlPis );
     extern void Gia_WriteMappedVerilog( char * pFileName, Gia_Man_t * pGia, int fVerbose );
     char * pFileSpec = NULL;
     Abc_Ntk_t * pNtkSpec = NULL;
     char * pFileName;
     char ** pArgvNew;
     int c, nArgcNew;
+    int fUseCtrlPis = 0;
     int fUseGates = 0;
     int fUseLuts = 0;
     int fVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Sglvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Scglvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -35179,6 +35186,9 @@ int Abc_CommandAbc9WriteVer( Abc_Frame_t * pAbc, int argc, char ** argv )
             pFileSpec = argv[globalUtilOptind];
             globalUtilOptind++;
             break;
+        case 'c':
+            fUseCtrlPis ^= 1;
+            break;
         case 'g':
             fUseGates ^= 1;
             break;
@@ -35222,7 +35232,7 @@ int Abc_CommandAbc9WriteVer( Abc_Frame_t * pAbc, int argc, char ** argv )
         }
         else
         {
-            Gia_WriteVerilog( pFileName, pAbc->pGia, fUseGates, fVerbose );
+            Gia_WriteVerilogInt( pFileName, pAbc->pGia, fUseGates, fVerbose, fUseCtrlPis );
         }
     }
     else
@@ -35245,9 +35255,10 @@ int Abc_CommandAbc9WriteVer( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &write_ver [-S <file>] [-glvh] <file>\n" );
+    Abc_Print( -2, "usage: &write_ver [-S <file>] [-cglvh] <file>\n" );
     Abc_Print( -2, "\t          writes hierarchical Verilog\n" );
     Abc_Print( -2, "\t-S file : file name for the original design (required when hierarchy is present)\n" );
+    Abc_Print( -2, "\t-c      : add clk/rst ports for seq AIGs [default = %s]\n", fUseCtrlPis? "no": "yes" );
     Abc_Print( -2, "\t-g      : toggle output gates vs assign-statements [default = %s]\n", fUseGates? "gates": "assigns" );
     Abc_Print( -2, "\t-l      : write LUT6-based Verilog for mapped AIGs [default = %s]\n", fUseLuts? "yes": "no" );
     Abc_Print( -2, "\t-v      : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
@@ -41171,7 +41182,7 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
     Cec_ManCorSetDefaultParams( pPars );
     pPars->nProcs = 1;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "FCGXPSZpkrecqowvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FCGXPSZpkrecqiowvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -41270,6 +41281,9 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'q':
             pPars->fStopWhenGone ^= 1;
             break;
+        case 'i':
+            pPars->fIncremental ^= 1;
+            break;
         case 'o':
             fUseOld ^= 1;
             break;
@@ -41343,7 +41357,7 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &scorr [-FCGXPSZ num] [-pkrecqowvh]\n" );
+    Abc_Print( -2, "usage: &scorr [-FCGXPSZ num] [-pkrecqiowvh]\n" );
     Abc_Print( -2, "\t         performs signal correpondence computation\n" );
     Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
     Abc_Print( -2, "\t-F num : the number of timeframes in inductive case [default = %d]\n", pPars->nFrames );
@@ -41358,6 +41372,7 @@ usage:
     Abc_Print( -2, "\t-e     : toggle using equivalences as choices [default = %s]\n", pPars->fMakeChoices? "yes": "no" );
     Abc_Print( -2, "\t-c     : toggle using circuit-based SAT solver [default = %s]\n", pPars->fUseCSat? "yes": "no" );
     Abc_Print( -2, "\t-q     : toggle quitting when PO is not a constant candidate [default = %s]\n", pPars->fStopWhenGone? "yes": "no" );
+    Abc_Print( -2, "\t-i     : toggle incremental TFO-triggered re-proof in main loop [default = %s] by Xiran ZHao at University of Chinese Academy of Sciences\n", pPars->fIncremental? "yes": "no" );
     Abc_Print( -2, "\t-o     : toggle calling old engine [default = %s]\n", fUseOld? "yes": "no" );
     Abc_Print( -2, "\t-w     : toggle printing verbose info about equivalent flops [default = %s]\n", pPars->fVerboseFlops? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
@@ -51574,10 +51589,10 @@ int Abc_CommandAbc9SProve( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Gia_Man_t * pGiaUse = pAbc->pGia, * pGiaTemp = NULL;
     Wlc_Ntk_t * pWlc = (Wlc_Ntk_t *)pAbc->pAbcWlc;
-    char * pReplayFile = NULL;
+    char * pReplayFile = NULL, * pUfarArgs = NULL, * pUfarArgsAlloc = NULL;
     int c, nProcs = 6, nProcsNew = 0, nTimeOut = 3, nTimeOut2 = 10, nTimeOut3 = 100, fUseUif = 0, fVerbose = 0, fVeryVerbose = 0, fSilent = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "PTUWRusvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "PTUCWRusvwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -51614,7 +51629,30 @@ int Abc_CommandAbc9SProve( Abc_Frame_t * pAbc, int argc, char ** argv )
             globalUtilOptind++;
             if ( nTimeOut2 <= 0 )
                 goto usage;
-            break;    
+            break;
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-C\" should be followed by a string.\n" );
+                goto usage;
+            }
+            {
+                int iArg, nChars = 0;
+                ABC_FREE( pUfarArgsAlloc );
+                for ( iArg = globalUtilOptind; iArg < argc; iArg++ )
+                    nChars += (int)strlen(argv[iArg]) + 1;
+                pUfarArgsAlloc = ABC_ALLOC( char, nChars + 1 );
+                pUfarArgsAlloc[0] = 0;
+                for ( iArg = globalUtilOptind; iArg < argc; iArg++ )
+                {
+                    if ( iArg > globalUtilOptind )
+                        strcat( pUfarArgsAlloc, " " );
+                    strcat( pUfarArgsAlloc, argv[iArg] );
+                }
+                pUfarArgs = pUfarArgsAlloc;
+                globalUtilOptind = argc;
+            }
+            break;
         case 'W':
             if ( globalUtilOptind >= argc )
             {
@@ -51659,27 +51697,37 @@ int Abc_CommandAbc9SProve( Abc_Frame_t * pAbc, int argc, char ** argv )
         if ( pWlc == NULL )
         {
             Abc_Print( -1, "Abc_CommandAbc9SProve(): There is no word-level design for option \"-u\".\n" );
+            ABC_FREE( pUfarArgsAlloc );
             return 1;
         }
         pGiaTemp = Wlc_NtkBitBlast( pWlc, NULL );
         if ( pGiaTemp == NULL )
         {
             Abc_Print( -1, "Abc_CommandAbc9SProve(): Word-level bit-blasting has failed.\n" );
+            ABC_FREE( pUfarArgsAlloc );
             return 1;
         }
         if ( (Gia_ManPoNum(pGiaTemp) & 1) == 1 )
         {
             Abc_Print( -1, "Abc_CommandAbc9SProve(): Internal \"&miter -x\" requires even number of bit-level outputs.\n" );
             Gia_ManStop( pGiaTemp );
+            ABC_FREE( pUfarArgsAlloc );
             return 1;
         }
         pGiaUse = Gia_ManTransformMiter2( pGiaTemp );
         Gia_ManStop( pGiaTemp );
         pGiaTemp = NULL;
     }
+    else if ( pUfarArgs != NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9SProve(): Option \"-C\" requires \"-u\".\n" );
+        ABC_FREE( pUfarArgsAlloc );
+        return 1;
+    }
     if ( pGiaUse == NULL )
     {
         Abc_Print( -1, "Abc_CommandAbc9SProve(): There is no AIG.\n" );
+        ABC_FREE( pUfarArgsAlloc );
         return 1;
     }
     if ( Gia_ManRegNum(pGiaUse) == 0 )
@@ -51687,20 +51735,23 @@ int Abc_CommandAbc9SProve( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Abc_CommandAbc9SProve(): The problem is combinational.\n" );
         if ( fUseUif )
             Gia_ManStop( pGiaUse );
+        ABC_FREE( pUfarArgsAlloc );
         return 1;
     }
-    pAbc->Status = Cec_GiaProveTest( pGiaUse, nProcs, nTimeOut, nTimeOut2, nTimeOut3, fUseUif, pWlc, fVerbose, fVeryVerbose, fSilent, pReplayFile );
+    pAbc->Status = Cec_GiaProveTest( pGiaUse, nProcs, nTimeOut, nTimeOut2, nTimeOut3, fUseUif, pWlc, fVerbose, fVeryVerbose, fSilent, pReplayFile, pUfarArgs );
     Abc_FrameReplaceCex( pAbc, &pGiaUse->pCexSeq ); 
     if ( fUseUif )
         Gia_ManStop( pGiaUse );
+    ABC_FREE( pUfarArgsAlloc );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &sprove [-PTUW num] [-R file] [-usvwh]\n" );
+    Abc_Print( -2, "usage: &sprove [-PTUW num] [-C str] [-R file] [-usvwh]\n" );
     Abc_Print( -2, "\t         proves CEC problem by case-splitting\n" );
     Abc_Print( -2, "\t-P num : the number of concurrent processes (1 <= num <= 6) [default = %d]\n", nProcs );
     Abc_Print( -2, "\t-T num : runtime limit in seconds per subproblem [default = %d]\n",     nTimeOut );
-    Abc_Print( -2, "\t-U num : runtime limit in seconds per subproblem [default = %d]\n",     nTimeOut2 );
+    Abc_Print( -2, "\t-U num : second-stage timeout in seconds [default = %d]\n", nTimeOut2 );
+    Abc_Print( -2, "\t-C str : with -u, pass this option string to internal %%ufar\n" );
     Abc_Print( -2, "\t-W num : runtime limit in seconds per subproblem [default = %d]\n",     nTimeOut3 );
     Abc_Print( -2, "\t-R str : dump replay/trace file for later execution by &sprove2\n" );
     Abc_Print( -2, "\t-u     : enable concurrent UFAR on word-level design (uses internal %%blast + &miter -x)\n" );
@@ -51708,6 +51759,7 @@ usage:
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n",         fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-w     : toggle printing more verbose information [default = %s]\n",    fVeryVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
+    ABC_FREE( pUfarArgsAlloc );
     return 1;
 }
 
@@ -59869,6 +59921,213 @@ usage:
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc9Pipeline( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern Gia_Man_t * Gia_ManDupPipeline( Gia_Man_t * p, int nLevels, int fVerbose );
+    Gia_Man_t * pGiaNew;
+    int nLevels = 20;
+    int nDelayMax, c, fVerbose = 0;
+
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Dvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'D':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-D\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            nLevels = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nLevels <= 0 )
+                goto usage;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9Pipeline(): There is no AIG.\n" );
+        return 1;
+    }
+    if ( Gia_ManRegNum(pAbc->pGia) > 0 )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9Pipeline(): This command expects a combinational AIG.\n" );
+        return 1;
+    }
+
+    pGiaNew = Gia_ManDupPipeline( pAbc->pGia, nLevels, fVerbose );
+    if ( pGiaNew == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9Pipeline(): Pipelining has failed.\n" );
+        return 1;
+    }
+    nDelayMax = Gia_ManLevelNum( pGiaNew );
+    if ( nDelayMax > nLevels )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9Pipeline(): Seed pipeline delay (%d) exceeds target D = %d.\n", nDelayMax, nLevels );
+        Gia_ManStop( pGiaNew );
+        return 1;
+    }
+    Abc_FrameUpdateGia( pAbc, pGiaNew );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &pipe [-D num] [-vh]\n" );
+    Abc_Print( -2, "\t         inserts pipeline stages\n" );
+    Abc_Print( -2, "\t-D num : max AIG levels between the flops [default = %d]\n", nLevels );
+    Abc_Print( -2, "\t-v     : toggle verbose output [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_CommandAbc9Unpipeline( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern Gia_Man_t * Gia_ManDupUnpipeline( Gia_Man_t * p, int fVerbose );
+    Gia_Man_t * pGiaNew;
+    int c, fVerbose = 0;
+
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9Unpipeline(): There is no AIG.\n" );
+        return 1;
+    }
+    if ( Gia_ManRegNum(pAbc->pGia) == 0 )
+    {
+        if ( fVerbose )
+            Abc_Print( 1, "Abc_CommandAbc9Unpipeline(): The current AIG is already combinational.\n" );
+        return 0;
+    }
+
+    pGiaNew = Gia_ManDupUnpipeline( pAbc->pGia, fVerbose );
+    if ( pGiaNew == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9Unpipeline(): Removing pipeline flops has failed.\n" );
+        return 1;
+    }
+    Abc_FrameUpdateGia( pAbc, pGiaNew );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &unpipe [-vh]\n" );
+    Abc_Print( -2, "\t         removes the flops to derive a combinational AIG\n" );
+    Abc_Print( -2, "\t-v     : toggle verbose output [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_CommandAbc9Regio( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern Gia_Man_t * Gia_ManDupRegio( Gia_Man_t * p, int fRegIns, int fRegOuts, int fVerbose );
+    Gia_Man_t * pGiaNew;
+    int c, fRegIns = 1, fRegOuts = 1, fVerbose = 0;
+
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "iovh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'i':
+            fRegIns ^= 1;
+            break;
+        case 'o':
+            fRegOuts ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9Regio(): There is no AIG.\n" );
+        return 1;
+    }
+    if ( !fRegIns && !fRegOuts )
+    {
+        if ( fVerbose )
+            Abc_Print( 1, "Abc_CommandAbc9Regio(): No boundary flops are requested.\n" );
+        return 0;
+    }
+
+    pGiaNew = Gia_ManDupRegio( pAbc->pGia, fRegIns, fRegOuts, fVerbose );
+    if ( pGiaNew == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9Regio(): Adding boundary flops has failed.\n" );
+        return 1;
+    }
+    Abc_FrameUpdateGia( pAbc, pGiaNew );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &regio [-iovh]\n" );
+    Abc_Print( -2, "\t         adds PI/PO flops while preserving the current AIG\n" );
+    Abc_Print( -2, "\t-i     : toggle adding PI flops [default = %s]\n", fRegIns ? "yes" : "no" );
+    Abc_Print( -2, "\t-o     : toggle adding PO flops [default = %s]\n", fRegOuts ? "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");
+    return 1;
+}
+
 /**Function*************************************************************
 
   Synopsis    []

src/base/io/ioJsonc.c

@@ -108,6 +108,8 @@ void json_print_string(json_t *json, json_value_t val, FILE *fp);
 void json_debug_value(json_t *json, json_value_t val, int indent);
 
 extern Abc_Ntk_t * Abc_NtkFromMiniMapping( int * pArray );
+static json_value_t * Jsonc_ObjectLookup( json_t * pJson, json_value_t object, const char * pKey );
+static char * Jsonc_StringDup( json_t * pJson, json_value_t value );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -671,6 +673,68 @@ static const char * Jsonc_GetNodeOutName( Abc_Obj_t * pObj )
     snprintf( Buffer, sizeof(Buffer), "n%d", Abc_ObjId(pObj) );
     return Buffer;
 }
+static char * Jsonc_GetInstanceOutName( json_t * pJson, json_value_t Node )
+{
+    json_value_t * pOutName = Jsonc_ObjectLookup( pJson, Node, "pin" );
+    if ( pOutName == NULL )
+        pOutName = Jsonc_ObjectLookup( pJson, Node, "output" );
+    return pOutName && pOutName->type == JSON_STRING ? Jsonc_StringDup( pJson, *pOutName ) : NULL;
+}
+static int Jsonc_IsPrevTwinNode( Abc_Obj_t * pObj, Abc_Obj_t ** ppPrev )
+{
+    Abc_Obj_t * pPrev;
+    Mio_Gate_t * pGate = (Mio_Gate_t *)pObj->pData;
+    if ( ppPrev )
+        *ppPrev = NULL;
+    if ( pGate == NULL || Mio_GateReadTwin(pGate) == NULL || Abc_ObjId(pObj) == 0 )
+        return 0;
+    pPrev = Abc_NtkObj( pObj->pNtk, Abc_ObjId(pObj) - 1 );
+    if ( pPrev == NULL || !Abc_ObjIsNode(pPrev) || Abc_ObjFaninNum(pPrev) != Abc_ObjFaninNum(pObj) )
+        return 0;
+    if ( Mio_GateReadTwin(pGate) != (Mio_Gate_t *)pPrev->pData )
+        return 0;
+    if ( ppPrev )
+        *ppPrev = pPrev;
+    return 1;
+}
+static Vec_Ptr_t * Jsonc_OrderTwinNodes( Abc_Ntk_t * p, Vec_Ptr_t * vNodes )
+{
+    Vec_Int_t * vInDfs = Vec_IntStart( Abc_NtkObjNumMax(p) );
+    Vec_Int_t * vSeen = Vec_IntStart( Abc_NtkObjNumMax(p) );
+    Vec_Ptr_t * vRes = Vec_PtrAlloc( Vec_PtrSize(vNodes) );
+    Abc_Obj_t * pObj, * pTwin;
+    int i;
+    Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
+        Vec_IntWriteEntry( vInDfs, Abc_ObjId(pObj), 1 );
+    Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
+    {
+        if ( Vec_IntEntry(vSeen, Abc_ObjId(pObj)) )
+            continue;
+        if ( Jsonc_IsPrevTwinNode( pObj, &pTwin ) && Vec_IntEntry(vInDfs, Abc_ObjId(pTwin)) )
+        {
+            if ( !Vec_IntEntry(vSeen, Abc_ObjId(pTwin)) )
+            {
+                Vec_PtrPush( vRes, pTwin );
+                Vec_IntWriteEntry( vSeen, Abc_ObjId(pTwin), 1 );
+            }
+            Vec_PtrPush( vRes, pObj );
+            Vec_IntWriteEntry( vSeen, Abc_ObjId(pObj), 1 );
+            continue;
+        }
+        Vec_PtrPush( vRes, pObj );
+        Vec_IntWriteEntry( vSeen, Abc_ObjId(pObj), 1 );
+        pTwin = Abc_NtkFetchTwinNode( pObj );
+        if ( pTwin && Vec_IntEntry(vInDfs, Abc_ObjId(pTwin)) && !Vec_IntEntry(vSeen, Abc_ObjId(pTwin)) )
+        {
+            Vec_PtrPush( vRes, pTwin );
+            Vec_IntWriteEntry( vSeen, Abc_ObjId(pTwin), 1 );
+        }
+    }
+    assert( Vec_PtrSize(vRes) == Vec_PtrSize(vNodes) );
+    Vec_IntFree( vInDfs );
+    Vec_IntFree( vSeen );
+    return vRes;
+}
 
 /**Function*************************************************************
 
@@ -692,8 +756,18 @@ void Jsonc_WriteTest( Abc_Ntk_t * p, char * pFileName )
     int i, Counter, Total;
     assert( Abc_NtkHasMapping(p) );
     vNodes   = Abc_NtkDfs2( p );
+    {
+        Vec_Ptr_t * vTemp = Jsonc_OrderTwinNodes( p, vNodes );
+        Vec_PtrFree( vNodes );
+        vNodes = vTemp;
+    }
     vObj2Num = Vec_IntStartFull( Abc_NtkObjNumMax(p) );
     Total    = Abc_NtkPiNum(p) + Vec_PtrSize(vNodes) + Abc_NtkPoNum(p);
+    Counter  = 0;
+    Abc_NtkForEachPi( p, pObj, i )
+        Vec_IntWriteEntry( vObj2Num, Abc_ObjId(pObj), Counter++ );
+    Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
+        Vec_IntWriteEntry( vObj2Num, Abc_ObjId(pObj), Counter++ );
     pFile    = fopen( pFileName, "wb" );
     if ( pFile == NULL )
     {
@@ -727,6 +801,8 @@ void Jsonc_WriteTest( Abc_Ntk_t * p, char * pFileName )
         fprintf( pFile, "    {\n" );
         fprintf( pFile, "      \"type\": \"%s\",\n", "instance" );
         fprintf( pFile, "      \"name\": \"%s\",\n", Mio_GateReadName(pGate) );
+        if ( Mio_GateReadTwin(pGate) != NULL )
+            fprintf( pFile, "      \"pin\": \"%s\",\n", Mio_GateReadOutName(pGate) );
         fprintf( pFile, "      \"fanins\":\n" );
         fprintf( pFile, "        {\n" );
         for ( pPin = Mio_GateReadPins(pGate), k = 0; pPin; pPin = Mio_PinReadNext(pPin), k++ )
@@ -897,9 +973,10 @@ static void Jsonc_AppendPortNames( Vec_Str_t * vNames, Vec_Ptr_t * vBases, Vec_I
     Vec_IntFree( vCounts );
     Vec_IntFree( vBaseIds );
 }
-static Vec_Int_t * Jsonc_ConvertToMiniMapping( json_t * pJson, Mio_Library_t * pLib, char ** ppDesignName )
+static Vec_Int_t * Jsonc_ConvertToMiniMapping( json_t * pJson, Mio_Library_t * pLib, char ** ppDesignName, Vec_Ptr_t ** pvNodeOutNames )
 {
     Vec_Ptr_t * vPiBases = NULL, * vPoBases = NULL;
+    Vec_Ptr_t * vNodeOutNames = NULL;
     Vec_Int_t * vPiBits = NULL, * vPoBits = NULL;
     Vec_Int_t * vNodeMap = NULL, * vGateIdx = NULL, * vPoIdx = NULL;
     Vec_Int_t * vMapping = NULL, * vPoDrivers = NULL;
@@ -911,6 +988,8 @@ static Vec_Int_t * Jsonc_ConvertToMiniMapping( json_t * pJson, Mio_Library_t * p
     int fSuccess = 0;
     if ( ppDesignName )
         *ppDesignName = NULL;
+    if ( pvNodeOutNames )
+        *pvNodeOutNames = NULL;
     if ( pLib == NULL )
     {
         printf( "Genlib library is not available.\n" );
@@ -943,6 +1022,7 @@ static Vec_Int_t * Jsonc_ConvertToMiniMapping( json_t * pJson, Mio_Library_t * p
     vPiBits    = Vec_IntAlloc( pNodes->count );
     vPoBases   = Vec_PtrAlloc( pNodes->count );
     vPoBits    = Vec_IntAlloc( pNodes->count );
+    vNodeOutNames = Vec_PtrAlloc( pNodes->count );
     // first pass: collect object types and names
     for ( i = 0; i < (int)pNodes->count; i++ )
     {
@@ -1020,7 +1100,7 @@ static Vec_Int_t * Jsonc_ConvertToMiniMapping( json_t * pJson, Mio_Library_t * p
             json_container_t * pFanObj;
             Mio_Gate_t * pGate;
             Mio_Pin_t * pPin;
-            char * pGateStr;
+            char * pGateStr, * pOutStr;
             if ( pGateName == NULL || pGateName->type != JSON_STRING )
             {
                 printf( "Gate node %d is missing a name.\n", i );
@@ -1032,16 +1112,19 @@ static Vec_Int_t * Jsonc_ConvertToMiniMapping( json_t * pJson, Mio_Library_t * p
                 printf( "Gate node %d has an invalid name.\n", i );
                 goto cleanup;
             }
-            pGate = Mio_LibraryReadGateByName( pLib, pGateStr, NULL );
+            pOutStr = Jsonc_GetInstanceOutName( pJson, Node );
+            pGate = Mio_LibraryReadGateByName( pLib, pGateStr, pOutStr );
             if ( pGate == NULL )
             {
-                printf( "Gate \"%s\" is not found in the current library.\n", pGateStr );
+                printf( "Gate \"%s\"%s%s%s is not found in the current library.\n", pGateStr, pOutStr ? " with output pin \"" : "", pOutStr ? pOutStr : "", pOutStr ? "\"" : "" );
+                ABC_FREE( pOutStr );
                 ABC_FREE( pGateStr );
                 goto cleanup;
             }
             if ( pFanins == NULL || pFanins->type != JSON_OBJECT )
             {
                 printf( "Gate \"%s\" is missing \"fanins\" description.\n", pGateStr );
+                ABC_FREE( pOutStr );
                 ABC_FREE( pGateStr );
                 goto cleanup;
             }
@@ -1049,6 +1132,7 @@ static Vec_Int_t * Jsonc_ConvertToMiniMapping( json_t * pJson, Mio_Library_t * p
             if ( pFanObj == NULL )
             {
                 printf( "Gate \"%s\" has incomplete fanin information.\n", pGateStr );
+                ABC_FREE( pOutStr );
                 ABC_FREE( pGateStr );
                 goto cleanup;
             }
@@ -1061,6 +1145,7 @@ static Vec_Int_t * Jsonc_ConvertToMiniMapping( json_t * pJson, Mio_Library_t * p
                 if ( pPinInfo == NULL || pPinInfo->type != JSON_OBJECT )
                 {
                     printf( "Gate \"%s\" is missing connection for pin \"%s\".\n", pGateStr, Mio_PinReadName(pPin) );
+                    ABC_FREE( pOutStr );
                     ABC_FREE( pGateStr );
                     goto cleanup;
                 }
@@ -1068,12 +1153,14 @@ static Vec_Int_t * Jsonc_ConvertToMiniMapping( json_t * pJson, Mio_Library_t * p
                 if ( pNodeLit == NULL || !Jsonc_ParseInt( pJson, *pNodeLit, &NodeId ) )
                 {
                     printf( "Gate \"%s\" has invalid node reference on pin \"%s\".\n", pGateStr, Mio_PinReadName(pPin) );
+                    ABC_FREE( pOutStr );
                     ABC_FREE( pGateStr );
                     goto cleanup;
                 }
                 if ( NodeId < 0 || NodeId >= Vec_IntSize(vNodeMap) )
                 {
                     printf( "Gate \"%s\" references out-of-range node %d.\n", pGateStr, NodeId );
+                    ABC_FREE( pOutStr );
                     ABC_FREE( pGateStr );
                     goto cleanup;
                 }
@@ -1081,6 +1168,7 @@ static Vec_Int_t * Jsonc_ConvertToMiniMapping( json_t * pJson, Mio_Library_t * p
                 if ( MapId < 0 )
                 {
                     printf( "Gate \"%s\" refers to unsupported node %d.\n", pGateStr, NodeId );
+                    ABC_FREE( pOutStr );
                     ABC_FREE( pGateStr );
                     goto cleanup;
                 }
@@ -1088,6 +1176,7 @@ static Vec_Int_t * Jsonc_ConvertToMiniMapping( json_t * pJson, Mio_Library_t * p
             }
             Vec_StrPrintStr( vNames, pGateStr );
             Vec_StrPush( vNames, '\0' );
+            Vec_PtrPush( vNodeOutNames, pOutStr );
             ABC_FREE( pGateStr );
         }
         else if ( Jsonc_StringEqual( pJson, *pType, "PO" ) || Jsonc_StringEqual( pJson, *pType, "po" ) )
@@ -1148,6 +1237,18 @@ cleanup:
     Vec_IntFreeP( &vPoBits );
     if ( vNames )
         Vec_StrFree( vNames );
+    if ( vNodeOutNames )
+    {
+        if ( fSuccess && pvNodeOutNames )
+            *pvNodeOutNames = vNodeOutNames;
+        else
+        {
+            char * pOutName;
+            Vec_PtrForEachEntry( char *, vNodeOutNames, pOutName, i )
+                ABC_FREE( pOutName );
+            Vec_PtrFree( vNodeOutNames );
+        }
+    }
     if ( vPiBases )
     {
         Vec_PtrForEachEntry( char *, vPiBases, pBase, i )
@@ -1171,8 +1272,12 @@ Abc_Ntk_t * Jsonc_ReadNetwork( char * pFileName )
 {
     Mio_Library_t * pLib = (Mio_Library_t *)Abc_FrameReadLibGen();
     Vec_Int_t * vMapping;
+    Vec_Ptr_t * vNodeOutNames = NULL;
     Abc_Ntk_t * pNtk;
+    Abc_Obj_t * pObj;
     char * pDesignName = NULL;
+    char * pOutName;
+    int i;
     json_t * pJson = json_create();
     if ( pJson == NULL )
     {
@@ -1185,7 +1290,7 @@ Abc_Ntk_t * Jsonc_ReadNetwork( char * pFileName )
         json_destroy( pJson );
         return NULL;
     }
-    vMapping = Jsonc_ConvertToMiniMapping( pJson, pLib, &pDesignName );
+    vMapping = Jsonc_ConvertToMiniMapping( pJson, pLib, &pDesignName, &vNodeOutNames );
     json_destroy( pJson );
     if ( vMapping == NULL )
         return NULL;
@@ -1193,9 +1298,35 @@ Abc_Ntk_t * Jsonc_ReadNetwork( char * pFileName )
     Vec_IntFree( vMapping );
     if ( pNtk == NULL )
     {
+        if ( vNodeOutNames )
+        {
+            Vec_PtrForEachEntry( char *, vNodeOutNames, pOutName, i )
+                ABC_FREE( pOutName );
+            Vec_PtrFree( vNodeOutNames );
+        }
         ABC_FREE( pDesignName );
         return NULL;
     }
+    if ( vNodeOutNames )
+    {
+        Vec_PtrForEachEntry( char *, vNodeOutNames, pOutName, i )
+        {
+            Mio_Gate_t * pGate;
+            pObj = Abc_NtkObj( pNtk, Abc_NtkCiNum(pNtk) + i + 1 );
+            if ( pObj == NULL )
+                continue;
+            pGate = (Mio_Gate_t *)pObj->pData;
+            if ( pOutName && pGate )
+            {
+                Mio_Gate_t * pGateOut = Mio_LibraryReadGateByName( pLib, Mio_GateReadName(pGate), pOutName );
+                if ( pGateOut )
+                    pObj->pData = pGateOut;
+            }
+        }
+        Vec_PtrForEachEntry( char *, vNodeOutNames, pOutName, i )
+            ABC_FREE( pOutName );
+        Vec_PtrFree( vNodeOutNames );
+    }
     ABC_FREE( pNtk->pName );
     pNtk->pName = pDesignName ? pDesignName : Extra_FileNameGeneric( pFileName );
     ABC_FREE( pNtk->pSpec );

src/base/io/ioReadBlif.c

@@ -622,46 +622,65 @@ int Io_ReadBlifReorderFormalNames( Vec_Ptr_t * vTokens, Mio_Gate_t * pGate, Mio_
     }
     else
     {
-        if ( i != Mio_GateReadPinNum(pGate) ) // expect the correct order of input pins in the network with twin gates
+        int nInputs = Mio_GateReadPinNum(pGate);
+        int nOutputs = nSize - 2 - nInputs;
+        int nMatched = 0;
+        if ( nOutputs != 1 && nOutputs != 2 )
             return 0;
-        // check the last two entries
-        if ( nSize - 3 == Mio_GateReadPinNum(pGate) ) // only one output is available
+        // reorder the input pins to be in the same order as in the gate
+        for ( pGatePin = Mio_GateReadPins(pGate), i = 0; pGatePin; pGatePin = Mio_PinReadNext(pGatePin), i++ )
         {
-            pNamePin = Mio_GateReadOutName(pGate);
+            pNamePin = Mio_PinReadName(pGatePin);
             Length = strlen(pNamePin);
-            pName = (char *)Vec_PtrEntry(vTokens, nSize - 1);
-            if ( !strncmp( pNamePin, pName, Length ) && pName[Length] == '=' ) // the last entry is pGate
+            for ( k = 2; k < nSize; k++ )
             {
-                Vec_PtrPush( vTokens, NULL );
-                return 1;
+                pName = (char *)Vec_PtrEntry(vTokens, k);
+                if ( !strncmp( pNamePin, pName, Length ) && pName[Length] == '=' )
+                {
+                    Vec_PtrPush( vTokens, pName );
+                    nMatched++;
+                    break;
+                }
             }
-            pNamePin = Mio_GateReadOutName(pTwin);
-            Length = strlen(pNamePin);
-            pName = (char *)Vec_PtrEntry(vTokens, nSize - 1);
-            if ( !strncmp( pNamePin, pName, Length ) && pName[Length] == '=' ) // the last entry is pTwin
+            if ( k == nSize )
+                return 0;
+        }
+        // add the outputs in the base/twin order, with NULL for a missing output
+        pNamePin = Mio_GateReadOutName(pGate);
+        Length = strlen(pNamePin);
+        for ( k = 2; k < nSize; k++ )
+        {
+            pName = (char *)Vec_PtrEntry(vTokens, k);
+            if ( !strncmp( pNamePin, pName, Length ) && pName[Length] == '=' )
             {
-                pName = (char *)Vec_PtrPop( vTokens );
-                Vec_PtrPush( vTokens, NULL );
                 Vec_PtrPush( vTokens, pName );
-                return 1;
+                nMatched++;
+                break;
             }
-            return 0;
         }
-        if ( nSize - 4 == Mio_GateReadPinNum(pGate) ) // two outputs are available
+        if ( k == nSize )
+            Vec_PtrPush( vTokens, NULL );
+        pNamePin = Mio_GateReadOutName(pTwin);
+        Length = strlen(pNamePin);
+        for ( k = 2; k < nSize; k++ )
         {
-            pNamePin = Mio_GateReadOutName(pGate);
-            Length = strlen(pNamePin);
-            pName = (char *)Vec_PtrEntry(vTokens, nSize - 2);
-            if ( !(!strncmp( pNamePin, pName, Length ) && pName[Length] == '=') )
-                return 0;
-            pNamePin = Mio_GateReadOutName(pTwin);
-            Length = strlen(pNamePin);
-            pName = (char *)Vec_PtrEntry(vTokens, nSize - 1);
-            if ( !(!strncmp( pNamePin, pName, Length ) && pName[Length] == '=') )
-                return 0;
-            return 1;
+            pName = (char *)Vec_PtrEntry(vTokens, k);
+            if ( !strncmp( pNamePin, pName, Length ) && pName[Length] == '=' )
+            {
+                Vec_PtrPush( vTokens, pName );
+                nMatched++;
+                break;
+            }
         }
-        assert( 0 );
+        if ( k == nSize )
+            Vec_PtrPush( vTokens, NULL );
+        if ( Vec_PtrEntry(vTokens, nSize + nInputs) == NULL && Vec_PtrEntry(vTokens, nSize + nInputs + 1) == NULL )
+            return 0;
+        if ( nMatched != nSize - 2 )
+            return 0;
+        Vec_PtrForEachEntryStart( char *, vTokens, pName, k, nSize )
+            Vec_PtrWriteEntry( vTokens, k - nSize + 2, pName );
+        Vec_PtrShrink( vTokens, 2 + nInputs + 2 );
     }
     return 1;
 }
@@ -1713,4 +1732,3 @@ int Io_ReadBlifNetworkConnectBoxes( Io_ReadBlif_t * p, Abc_Ntk_t * pNtkMaster )
 
 
 ABC_NAMESPACE_IMPL_END
-

src/base/io/ioWriteBlif.c

@@ -573,6 +573,17 @@ void Io_NtkWriteSubcktFanins( FILE * pFile, Abc_Obj_t * pNode )
   SeeAlso     []
 
 ***********************************************************************/
+static int Io_NtkNodesHaveSameFanins( Abc_Obj_t * pNode, Abc_Obj_t * pNode2 )
+{
+    Abc_Obj_t * pFanin;
+    int i;
+    if ( Abc_ObjFaninNum(pNode) != Abc_ObjFaninNum(pNode2) )
+        return 0;
+    Abc_ObjForEachFanin( pNode, pFanin, i )
+        if ( pFanin != Abc_ObjFanin(pNode2, i) )
+            return 0;
+    return 1;
+}
 int Io_NtkWriteNodeGate( FILE * pFile, Abc_Obj_t * pNode, int Length )
 {
     static int fReport = 0;
@@ -594,6 +605,8 @@ int Io_NtkWriteNodeGate( FILE * pFile, Abc_Obj_t * pNode, int Length )
             fReport = 1, printf( "Warning: Missing second output of gate(s) \"%s\".\n", Mio_GateReadName(pGate) );
         return 0;
     }
+    if ( !Io_NtkNodesHaveSameFanins( pNode, pNode2 ) )
+        return 0;
     fprintf( pFile, " %s=%s", Mio_GateReadOutName((Mio_Gate_t *)pNode2->pData), Abc_ObjName( Abc_ObjFanout0(pNode2) ) );
     return 1;
 }
@@ -1407,4 +1420,3 @@ void Io_WriteBlifSpecial( Abc_Ntk_t * pNtk, char * FileName, char * pLutStruct,
 
 
 ABC_NAMESPACE_IMPL_END
-

src/base/io/ioWritePla.c

@@ -174,7 +174,7 @@ int Io_WritePla( Abc_Ntk_t * pNtk, char * pFileName )
     FILE * pFile;
 
     assert( Abc_NtkIsSopNetlist(pNtk) );
-    assert( Abc_NtkLevel(pNtk) == 1 );
+    assert( Abc_NtkLevel(pNtk) <= 1 );
 
     pFile = fopen( pFileName, "w" );
     if ( pFile == NULL )

src/base/io/ioWriteVerilog.c

@@ -39,6 +39,8 @@ static void Io_WriteVerilogLatches( FILE * pFile, Abc_Ntk_t * pNtk );
 static void Io_WriteVerilogObjects( FILE * pFile, Abc_Ntk_t * pNtk, int fOnlyAnds );
 static int  Io_WriteVerilogWiresCount( Abc_Ntk_t * pNtk );
 static char * Io_WriteVerilogGetName( char * pName );
+static int Io_WriteVerilogNodesHaveSameFanins( Abc_Obj_t * pNode, Abc_Obj_t * pNode2 );
+static int Io_WriteVerilogIsPrevTwinNode( Abc_Obj_t * pNode );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -512,6 +514,54 @@ void Io_WriteVerilogLatches( FILE * pFile, Abc_Ntk_t * pNtk )
     fprintf( pFile, "  end\n" );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Checks whether two mapped nodes have the same fanins.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static int Io_WriteVerilogNodesHaveSameFanins( Abc_Obj_t * pNode, Abc_Obj_t * pNode2 )
+{
+    Abc_Obj_t * pFanin;
+    int i;
+    if ( Abc_ObjFaninNum(pNode) != Abc_ObjFaninNum(pNode2) )
+        return 0;
+    Abc_ObjForEachFanin( pNode, pFanin, i )
+        if ( pFanin != Abc_ObjFanin(pNode2, i) )
+            return 0;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks whether this mapped node is the second output of a twin.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static int Io_WriteVerilogIsPrevTwinNode( Abc_Obj_t * pNode )
+{
+    Abc_Obj_t * pPrev;
+    Mio_Gate_t * pGate = (Mio_Gate_t *)pNode->pData;
+    if ( pGate == NULL || Mio_GateReadTwin(pGate) == NULL || Abc_ObjId(pNode) == 0 )
+        return 0;
+    pPrev = Abc_NtkObj( pNode->pNtk, Abc_ObjId(pNode) - 1 );
+    if ( pPrev == NULL || !Abc_ObjIsNode(pPrev) )
+        return 0;
+    if ( Mio_GateReadTwin(pGate) != (Mio_Gate_t *)pPrev->pData )
+        return 0;
+    return Io_WriteVerilogNodesHaveSameFanins( pPrev, pNode );
+}
+
 /**Function*************************************************************
 
   Synopsis    [Writes the nodes and boxes.]
@@ -563,12 +613,18 @@ void Io_WriteVerilogObjects( FILE * pFile, Abc_Ntk_t * pNtk, int fOnlyAnds )
         Abc_NtkForEachNode( pNtk, pObj, k )
         {
             Mio_Gate_t * pGate = (Mio_Gate_t *)pObj->pData;
+            Abc_Obj_t * pNode2 = NULL;
             Mio_Pin_t * pGatePin;
+            if ( Io_WriteVerilogIsPrevTwinNode( pObj ) )
+                continue;
             if ( Abc_ObjFaninNum(pObj) == 0 && (!strcmp(Mio_GateReadName(pGate), "_const0_") || !strcmp(Mio_GateReadName(pGate), "_const1_")) )
             {
                 fprintf( pFile, "  %-*s %s = 1\'b%d;\n", Length, "assign", Io_WriteVerilogGetName(Abc_ObjName( Abc_ObjFanout0(pObj) )), !strcmp(Mio_GateReadName(pGate), "_const1_") );
                 continue;
             }
+            pNode2 = Abc_NtkFetchTwinNode( pObj );
+            if ( pNode2 && !Io_WriteVerilogNodesHaveSameFanins( pObj, pNode2 ) )
+                pNode2 = NULL;
             // write the node
             if ( fUseSimpleGateNames )
             {
@@ -591,6 +647,12 @@ void Io_WriteVerilogObjects( FILE * pFile, Abc_Ntk_t * pNtk, int fOnlyAnds )
                 assert ( i == Abc_ObjFaninNum(pObj) );
                 fprintf( pFile, ".%s", Io_WriteVerilogGetName(Mio_GateReadOutName(pGate)) );
                 fprintf( pFile, "(%s)", Io_WriteVerilogGetName(Abc_ObjName( Abc_ObjFanout0(pObj) )) );
+                if ( pNode2 )
+                {
+                    fprintf( pFile, ", " );
+                    fprintf( pFile, ".%s", Io_WriteVerilogGetName(Mio_GateReadOutName((Mio_Gate_t *)pNode2->pData)) );
+                    fprintf( pFile, "(%s)", Io_WriteVerilogGetName(Abc_ObjName( Abc_ObjFanout0(pNode2) )) );
+                }
                 fprintf( pFile, ");\n" );
             }
         }
@@ -972,4 +1034,3 @@ void Io_WriteVerilogLut( Abc_Ntk_t * pNtk, char * pFileName, int nLutSize, int f
 
 
 ABC_NAMESPACE_IMPL_END
-

src/base/main/mainInit.c

@@ -47,6 +47,8 @@ extern void Load_Init( Abc_Frame_t * pAbc );
 extern void Load_End( Abc_Frame_t * pAbc );
 extern void Scl_Init( Abc_Frame_t * pAbc );
 extern void Scl_End( Abc_Frame_t * pAbc );
+extern void Emap_Init( Abc_Frame_t * pAbc );
+extern void Emap_End( Abc_Frame_t * pAbc );
 extern void Wlc_Init( Abc_Frame_t * pAbc );
 extern void Wlc_End( Abc_Frame_t * pAbc );
 extern void Wln_Init( Abc_Frame_t * pAbc );
@@ -118,6 +120,7 @@ void Abc_FrameInit( Abc_Frame_t * pAbc )
     Libs_Init( pAbc );
     Load_Init( pAbc );
     Scl_Init( pAbc );
+    Emap_Init( pAbc );
     Wlc_Init( pAbc );
     Wln_Init( pAbc );
     Bac_Init( pAbc );
@@ -159,6 +162,7 @@ void Abc_FrameEnd( Abc_Frame_t * pAbc )
     Super_End( pAbc );
     Libs_End( pAbc );
     Load_End( pAbc );
+    Emap_End( pAbc );
     Scl_End( pAbc );
     Wlc_End( pAbc );
     Wln_End( pAbc );

src/map/emap/emap.c

@@ -0,0 +1,158 @@
+/**CFile****************************************************************
+
+  FileName    [emap.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Multi-output gate mapper.]
+
+  Synopsis    [ABC command entry points.]
+
+***********************************************************************/
+
+#include "emap.h"
+
+#include "base/abc/abc.h"
+#include "base/cmd/cmd.h"
+#include "base/main/mainInt.h"
+#include "map/mio/mio.h"
+#include "misc/extra/extra.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static int Emap_CommandCountMogPairs( Mio_Library_t * pLib );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the package.]
+
+***********************************************************************/
+void Emap_Init( Abc_Frame_t * pAbc )
+{
+    Cmd_CommandAdd( pAbc, "SC mapping", "emap", Emap_Command, 1 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the package.]
+
+***********************************************************************/
+void Emap_End( Abc_Frame_t * pAbc )
+{
+    (void)pAbc;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts physical two-output gates represented as twin gates.]
+
+***********************************************************************/
+static int Emap_CommandCountMogPairs( Mio_Library_t * pLib )
+{
+    Mio_Gate_t * pGate;
+    int nTwinOutputs = 0;
+    if ( pLib == NULL )
+        return 0;
+    Mio_LibraryForEachGate( pLib, pGate )
+        nTwinOutputs += (Mio_GateReadTwin(pGate) != NULL);
+    return nTwinOutputs / 2;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Runs the ABC-native exact mapper.]
+
+***********************************************************************/
+int Emap_Command( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
+    Mio_Library_t * pLib = (Mio_Library_t *)Abc_FrameReadLibGen();
+    Abc_Ntk_t * pNtkRes;
+    int c, fUseMogs = 1, fAreaMode = 0, fVerbose = 0;
+
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "amvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'a':
+            fAreaMode ^= 1;
+            break;
+        case 'm':
+            fUseMogs ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( argc != globalUtilOptind )
+        goto usage;
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pAbc->Err, "There is no current network.\n" );
+        return 1;
+    }
+    if ( pLib == NULL )
+    {
+        fprintf( pAbc->Err, "There is no current GENLIB library. Use read_genlib/read_lib first.\n" );
+        return 1;
+    }
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( pAbc->Err, "The current network is not an AIG. Run strash first.\n" );
+        return 1;
+    }
+
+    if ( fVerbose )
+    {
+        int nMogPairs = fUseMogs ? Emap_CommandCountMogPairs( pLib ) : 0;
+        fprintf( pAbc->Out, "ABC-native emap setup: PI = %d  PO = %d  AND = %d\n",
+            Abc_NtkPiNum(pNtk), Abc_NtkPoNum(pNtk), Abc_NtkNodeNum(pNtk) );
+        fprintf( pAbc->Out, "GENLIB \"%s\": gates = %d  MOG pairs = %d  MOG use = %s  mode = %s\n",
+            Mio_LibraryReadName(pLib), Mio_LibraryReadGateNum(pLib), nMogPairs, fUseMogs ? "yes" : "no", fAreaMode ? "area" : "delay" );
+    }
+
+    pNtkRes = Emap_ManMapAigStructural( pNtk, pLib, fUseMogs, fAreaMode, fVerbose );
+    if ( pNtkRes == NULL )
+    {
+        fprintf( pAbc->Err, "ABC-native emap structural mapping has failed.\n" );
+        return 1;
+    }
+
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pAbc->Err, "usage: emap [-amvh]\n" );
+    fprintf( pAbc->Err, "\t         maps the current AIG using the current GENLIB library\n" );
+    fprintf( pAbc->Err, "\t-a     : toggle area-oriented mode without required-time pruning [default = %s]\n", fAreaMode ? "yes" : "no" );
+    fprintf( pAbc->Err, "\t-m     : toggle using multi-output gates when present [default = %s]\n", fUseMogs ? "yes" : "no" );
+    fprintf( pAbc->Err, "\t-v     : toggle verbose output [default = %s]\n", fVerbose ? "yes" : "no" );
+    fprintf( pAbc->Err, "\t-h     : prints the command summary\n\n" );
+    fprintf( pAbc->Err, "\tThe mapper is inspired by \"emap\" in Mockturtle developed by Alessandro Tempia Calvino\n" );
+    fprintf( pAbc->Err, "\tavailable at https://mockturtle.readthedocs.io/en/latest/algorithms/mapper.html\n" );
+    fprintf( pAbc->Err, "\tand described in A. T. Calvino and G. De Micheli, \"Technology mapping using multi-output\n" );
+    fprintf( pAbc->Err, "\tlibrary cells\", Proc. ICCAD\'23, https://aletempiac.github.io/publication/2023_006\n" );
+    return 1;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END

src/map/emap/emap.h

@@ -0,0 +1,31 @@
+/**CFile****************************************************************
+
+  FileName    [emap.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Multi-output gate mapper.]
+
+  Synopsis    [External declarations.]
+
+***********************************************************************/
+
+#ifndef ABC__map__emap__emap_h
+#define ABC__map__emap__emap_h
+
+#include "base/main/main.h"
+
+ABC_NAMESPACE_HEADER_START
+
+typedef struct Abc_Ntk_t_ Abc_Ntk_t;
+typedef struct Mio_LibraryStruct_t_ Mio_Library_t;
+
+extern void Emap_Init   ( Abc_Frame_t * pAbc );
+extern void Emap_End    ( Abc_Frame_t * pAbc );
+extern int  Emap_Command( Abc_Frame_t * pAbc, int argc, char ** argv );
+
+extern Abc_Ntk_t * Emap_ManMapAigStructural( Abc_Ntk_t * pNtk, Mio_Library_t * pLib, int fUseMogs, int fAreaMode, int fVerbose );
+
+ABC_NAMESPACE_HEADER_END
+
+#endif

src/map/emap/module.make

@@ -0,0 +1,2 @@
+SRC += src/map/emap/emap.c \
+    src/map/emap/emapCore.c

src/map/scl/sclDnsize.c

@@ -149,7 +149,7 @@ p->timeSize += Abc_Clock() - clk;
     {
         pCellNew = SC_LibCell( p->pLib, gateBest );
         Abc_SclObjSetCell( pObj, pCellNew );
-        p->SumArea += pCellNew->area - pCellOld->area;
+        p->SumArea += Abc_SclObjAreaDelta( pObj, pCellOld, pCellNew );
 //        printf( "%f   %f -> %f\n", pCellNew->area - pCellOld->area, p->SumArea - (pCellNew->area - pCellOld->area), p->SumArea );
 //        printf( "%6d  %20s -> %20s  %f -> %f\n", Abc_ObjId(pObj), pCellOld->pName, pCellNew->pName, pCellOld->area, pCellNew->area );
         // mark used nodes with the current trav ID
@@ -376,4 +376,3 @@ void Abc_SclDnsizePerform( SC_Lib * pLib, Abc_Ntk_t * pNtk, SC_SizePars * pPars,
 
 
 ABC_NAMESPACE_IMPL_END
-

src/map/scl/sclLib.h

@@ -656,12 +656,13 @@ static inline void Scl_LibPinRequiredI( SC_Timing * pTime, SC_PairI * pReqIn, SC
   SeeAlso     []
 
 ***********************************************************************/
-static inline SC_Timing * Scl_CellPinTime( SC_Cell * pCell, int iPin )
+static inline SC_Timing * Scl_CellPinOutTime( SC_Cell * pCell, int iOut, int iPin )
 {
     SC_Pin * pPin;
     SC_Timings * pRTime;
+    assert( iOut >= 0 && iOut < pCell->n_outputs );
     assert( iPin >= 0 && iPin < pCell->n_inputs );
-    pPin = SC_CellPin( pCell, pCell->n_inputs );
+    pPin = SC_CellPin( pCell, pCell->n_inputs + iOut );
     assert( Vec_PtrSize(&pPin->vRTimings) == pCell->n_inputs );
     pRTime = (SC_Timings *)Vec_PtrEntry( &pPin->vRTimings, iPin );
     if ( Vec_PtrSize(&pRTime->vTimings) == 0 )
@@ -669,6 +670,10 @@ static inline SC_Timing * Scl_CellPinTime( SC_Cell * pCell, int iPin )
     assert( Vec_PtrSize(&pRTime->vTimings) == 1 );
     return (SC_Timing *)Vec_PtrEntry( &pRTime->vTimings, 0 );
 }
+static inline SC_Timing * Scl_CellPinTime( SC_Cell * pCell, int iPin )
+{
+    return Scl_CellPinOutTime( pCell, 0, iPin );
+}
 static inline float Scl_LibPinArrivalEstimate( SC_Cell * pCell, int iPin, float Slew, float Load )
 {
     SC_Pair LoadIn = { Load, Load };

src/map/scl/sclSize.c

@@ -103,6 +103,35 @@ Abc_Obj_t * Abc_SclFindMostCriticalFanin( SC_Man * p, int * pfRise, Abc_Obj_t *
     return pPivot;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Find the output pin represented by this mapped node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Abc_SclObjOutputIndex( Abc_Obj_t * pObj, SC_Cell * pCell )
+{
+    Mio_Gate_t * pGate;
+    char * pOutName;
+    int i;
+    if ( pCell->n_outputs == 1 )
+        return 0;
+    pGate = (Mio_Gate_t *)pObj->pData;
+    assert( pGate != NULL );
+    pOutName = Mio_GateReadOutName( pGate );
+    assert( pOutName != NULL );
+    for ( i = 0; i < pCell->n_outputs; i++ )
+        if ( !strcmp( pOutName, SC_CellPinName(pCell, pCell->n_inputs + i) ) )
+            return i;
+    assert( 0 );
+    return 0;
+}
+
 /**Function*************************************************************
 
   Synopsis    [Printing timing information for the node/network.]
@@ -299,10 +328,20 @@ static inline void Abc_SclDeptObj( SC_Man * p, Abc_Obj_t * pObj )
     SC_PairClean( Abc_SclObjDept(p, pObj) );
     Abc_ObjForEachFanout( pObj, pFanout, i )
     {
+        SC_Cell * pFanoutCell;
+        int iFanin, iOut;
         if ( Abc_ObjIsCo(pFanout) || Abc_ObjIsLatch(pFanout) )
             continue;
-        pTime = Scl_CellPinTime( Abc_SclObjCell(pFanout), Abc_NodeFindFanin(pFanout, pObj) );
-        Abc_SclDeptFanin( p, pTime, pFanout, pObj, Abc_NodeFindFanin(pFanout, pObj) );
+        pFanoutCell = Abc_SclObjCell( pFanout );
+        iFanin = Abc_NodeFindFanin( pFanout, pObj );
+        iOut = Abc_SclObjOutputIndex( pFanout, pFanoutCell );
+        pTime = Scl_CellPinOutTime( pFanoutCell, iOut, iFanin );
+        if ( pTime == NULL )
+        {
+            assert( pFanoutCell->n_outputs > 1 );
+            continue;
+        }
+        Abc_SclDeptFanin( p, pTime, pFanout, pObj, iFanin );
     }
 }
 static inline float Abc_SclObjLoadValue( SC_Man * p, Abc_Obj_t * pObj )
@@ -370,7 +409,13 @@ void Abc_SclTimeNode( SC_Man * p, Abc_Obj_t * pObj, int fDept )
     // compute for each fanin
     Abc_ObjForEachFanin( pObj, pFanin, k )
     {
-        pTime = Scl_CellPinTime( pCell, k );
+        int iOut = Abc_SclObjOutputIndex( pObj, pCell );
+        pTime = Scl_CellPinOutTime( pCell, iOut, k );
+        if ( pTime == NULL )
+        {
+            assert( pCell->n_outputs > 1 );
+            continue;
+        }
         if ( fDept )
             Abc_SclDeptFanin( p, pTime, pObj, pFanin, k );
         else
@@ -928,4 +973,3 @@ void Abc_SclPrintBuffers( SC_Lib * pLib, Abc_Ntk_t * pNtk, int fVerbose )
 
 ABC_NAMESPACE_IMPL_END
 
-

src/map/scl/sclSize.h

@@ -27,6 +27,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 #include "base/abc/abc.h"
+#include "map/mio/mio.h"
 #include "misc/vec/vecQue.h"
 #include "misc/vec/vecWec.h"
 #include "sclLib.h"
@@ -130,6 +131,64 @@ static inline float     Abc_SclObjInDrive( SC_Man * p, Abc_Obj_t * pObj )
 static inline void      Abc_SclObjSetInDrive( SC_Man * p, Abc_Obj_t * pObj, float c){ Vec_FltWriteEntry( p->vInDrive, pObj->iData, c );                                   }
 static inline void      Abc_SclManSetFaninCallBack( SC_Man * p, void * pCallBack )  { p->pFuncFanin = (float (*)(void *, Abc_Obj_t *, Abc_Obj_t *, int, int))pCallBack;   } 
 
+static inline int       Abc_SclObjsHaveSameFanins( Abc_Obj_t * pObj0, Abc_Obj_t * pObj1 )
+{
+    Abc_Obj_t * pFanin0, * pFanin1;
+    int i;
+    if ( pObj0 == NULL || pObj1 == NULL || Abc_ObjFaninNum(pObj0) != Abc_ObjFaninNum(pObj1) )
+        return 0;
+    Abc_ObjForEachFanin( pObj0, pFanin0, i )
+    {
+        pFanin1 = Abc_ObjFanin( pObj1, i );
+        if ( pFanin0 != pFanin1 )
+            return 0;
+    }
+    return 1;
+}
+static inline int       Abc_SclObjIsMogOutput( Abc_Obj_t * pObj )
+{
+    Mio_Gate_t * pGate;
+    if ( pObj == NULL || !Abc_ObjIsNode(pObj) )
+        return 0;
+    pGate = (Mio_Gate_t *)pObj->pData;
+    return pGate != NULL && Mio_GateReadTwin(pGate) != NULL;
+}
+static inline int       Abc_SclObjIsSecondTwin( Abc_Obj_t * pObj )
+{
+    Abc_Obj_t * pPrev;
+    Mio_Gate_t * pGate;
+    if ( !Abc_SclObjIsMogOutput(pObj) || Abc_ObjId(pObj) == 0 )
+        return 0;
+    pPrev = Abc_NtkObj( pObj->pNtk, Abc_ObjId(pObj) - 1 );
+    if ( pPrev == NULL || !Abc_ObjIsNode(pPrev) )
+        return 0;
+    pGate = (Mio_Gate_t *)pObj->pData;
+    if ( Mio_GateReadTwin(pGate) != (Mio_Gate_t *)pPrev->pData )
+        return 0;
+    return Abc_SclObjsHaveSameFanins( pObj, pPrev );
+}
+static inline Abc_Obj_t * Abc_SclObjTwin( Abc_Obj_t * pObj )
+{
+    if ( Abc_SclObjIsSecondTwin(pObj) )
+        return Abc_NtkObj( pObj->pNtk, Abc_ObjId(pObj) - 1 );
+    return Abc_NtkFetchTwinNode( pObj );
+}
+static inline int       Abc_SclObjTwinFaninsMatch( Abc_Obj_t * pObj )
+{
+    Abc_Obj_t * pTwin = Abc_SclObjTwin( pObj );
+    return pTwin != NULL && Abc_SclObjsHaveSameFanins( pObj, pTwin );
+}
+static inline int       Abc_SclObjIsCanonicalMog( Abc_Obj_t * pObj )
+{
+    return Abc_SclObjIsMogOutput(pObj) && !Abc_SclObjIsSecondTwin(pObj);
+}
+static inline float     Abc_SclObjAreaDelta( Abc_Obj_t * pObj, SC_Cell * pCellOld, SC_Cell * pCellNew )
+{
+    if ( Abc_SclObjIsSecondTwin(pObj) )
+        return 0.0;
+    return pCellNew->area - pCellOld->area;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -450,7 +509,11 @@ static inline float Abc_SclGetTotalArea( Abc_Ntk_t * pNtk )
     Abc_Obj_t * pObj;
     int i;
     Abc_NtkForEachNodeNotBarBuf1( pNtk, pObj, i )
+    {
+        if ( Abc_SclObjIsSecondTwin(pObj) )
+            continue;
         Area += Abc_SclObjCell(pObj)->area;
+    }
     return Area;
 }
 static inline float Abc_SclGetMaxDelay( SC_Man * p )

src/map/scl/sclUpsize.c

@@ -489,7 +489,7 @@ int Abc_SclFindBypasses( SC_Man * p, Vec_Int_t * vPathNodes, int Ratio, int Notc
         // update cell
         pCellOld = Abc_SclObjCell( pFanin );
         pCellNew = SC_LibCell( p->pLib, Vec_IntEntry(p->vNode2Gate, iNode) );
-        p->SumArea += pCellNew->area - pCellOld->area;
+        p->SumArea += Abc_SclObjAreaDelta( pFanin, pCellOld, pCellNew );
         Abc_SclObjSetCell( pFanin, pCellNew );
         Abc_SclUpdateLoad( p, pFanin, pCellOld, pCellNew );
         // record the update
@@ -646,7 +646,7 @@ int Abc_SclFindUpsizes( SC_Man * p, Vec_Int_t * vPathNodes, int Ratio, int Notch
         //printf( "gain is %f\n", Vec_FltEntry(p->vNode2Gain, Abc_ObjId(pObj)) );
         // update gate
         Abc_SclUpdateLoad( p, pObj, pCellOld, pCellNew );
-        p->SumArea += pCellNew->area - pCellOld->area;
+        p->SumArea += Abc_SclObjAreaDelta( pObj, pCellOld, pCellNew );
         Abc_SclObjSetCell( pObj, pCellNew );
         // record the update
         Vec_IntPush( p->vUpdates, Abc_ObjId(pObj) );
@@ -686,7 +686,7 @@ return Limit;
 //        if ( pCellOld->Order > 0 )
 //            printf( "%.2f  %d -> %d(%d)   ", Vec_FltEntry(p->vNode2Gain, iNode), pCellOld->Order, pCellNew->Order, pCellNew->nGates );
         // update gate
-        p->SumArea += pCellNew->area - pCellOld->area;
+        p->SumArea += Abc_SclObjAreaDelta( pObj, pCellOld, pCellNew );
         Abc_SclObjSetCell( pObj, pCellNew );
         Abc_SclUpdateLoad( p, pObj, pCellOld, pCellNew );
         // record the update
@@ -1043,4 +1043,3 @@ void Abc_SclUpsizePerform( SC_Lib * pLib, Abc_Ntk_t * pNtk, SC_SizePars * pPars,
 
 
 ABC_NAMESPACE_IMPL_END
-

src/map/scl/sclUtil.c

@@ -75,9 +75,11 @@ void Abc_SclSclGates2MioGates( SC_Lib * pLib, Abc_Ntk_t * p )
     assert( p->vGates != NULL );
     Abc_NtkForEachNodeNotBarBuf1( p, pObj, i )
     {
+        Mio_Gate_t * pGateOld = (Mio_Gate_t *)pObj->pData;
+        char * pOutName = Abc_SclObjIsMogOutput(pObj) ? Mio_GateReadOutName(pGateOld) : NULL;
         pCell = Abc_SclObjCell(pObj);
         assert( pCell->n_inputs == Abc_ObjFaninNum(pObj) );
-        pObj->pData = Mio_LibraryReadGateByName( (Mio_Library_t *)p->pManFunc, pCell->pName, NULL );
+        pObj->pData = Mio_LibraryReadGateByName( (Mio_Library_t *)p->pManFunc, pCell->pName, pOutName );
         Counter += (pObj->pData == NULL);
         assert( pObj->fMarkA == 0 && pObj->fMarkB == 0 );
         CounterAll++;
@@ -317,4 +319,3 @@ void Abc_SclInsertBarBufs( Abc_Ntk_t * pNtk, Vec_Int_t * vBufs )
 
 
 ABC_NAMESPACE_IMPL_END
-

src/misc/extra/extraUtilFile.c

@@ -23,6 +23,9 @@
 #define PATH_MAX MAX_PATH
 #else
 #include <limits.h>
+#  ifndef PATH_MAX
+#    define PATH_MAX 4096
+#  endif
 #endif
 
 #include "extra.h"

src/opt/fret/fretMain.c

@@ -202,8 +202,9 @@ Abc_FlowRetime_MinReg( Abc_Ntk_t * pNtk, int fVerbose,
     pNtk = Abc_FlowRetime_NtkSilentRestrash( pNtk, 1 );
   }
   
+  i = Abc_NtkLevel(pNtk);
   vprintf("\tfinal reg count = %d\n", Abc_NtkLatchNum(pNtk));
-  vprintf("\tfinal levels = %d\n", Abc_NtkLevel(pNtk));
+  vprintf("\tfinal levels = %d\n", i);
 
 #if defined(DEBUG_CHECK)
   Abc_NtkDoCheck( pNtk );
@@ -1380,4 +1381,3 @@ void Abc_ObjPrintNeighborhood( Abc_Obj_t *pObj, int depth ) {
   Vec_PtrFree(vNodes);
 }
 ABC_NAMESPACE_IMPL_END
-

src/opt/fret/fretTime.c

@@ -94,14 +94,13 @@ void Abc_FlowRetime_ConstrainConserv( Abc_Ntk_t * pNtk ) {
 
   // clear all exact constraints
   pManMR->nExactConstraints = 0;
-  while( Vec_PtrSize( pManMR->vExactNodes )) {
-    pObj = (Abc_Obj_t*)Vec_PtrPop( pManMR->vExactNodes );
-    
+  Abc_NtkForEachObj( pNtk, pObj, i ) {
     if ( Vec_PtrSize( FTIMEEDGES(pObj) )) {
       pArray =  Vec_PtrReleaseArray( FTIMEEDGES(pObj) );
       ABC_FREE( pArray );
     }
   }
+  Vec_PtrClear( pManMR->vExactNodes );
 
 #if !defined(IGNORE_TIMING)
   if (pManMR->fIsForward) {

src/opt/lpk/lpkCut.c

@@ -141,7 +141,7 @@ unsigned * Lpk_CutTruth_rec( Hop_Man_t * pMan, Hop_Obj_t * pObj, int nVars, Vec_
     assert( !Hop_IsComplement(pObj) );
     if ( pObj->pData )
     {
-        assert( ((unsigned)(ABC_PTRUINT_T)pObj->pData) & 0xffff0000 );
+        assert( ((ABC_PTRUINT_T)pObj->pData) > 0xffff ); // catch small int values
         return (unsigned *)pObj->pData;
     }
     // get the plan for a new truth table
@@ -197,7 +197,7 @@ unsigned * Lpk_CutTruth( Lpk_Man_t * p, Lpk_Cut_t * pCut, int fInv )
         // set the initial truth tables at the fanins
         Abc_ObjForEachFanin( pObj, pFanin, k )
         {
-            assert( ((unsigned)(ABC_PTRUINT_T)pFanin->pCopy) & 0xffff0000 );
+            assert( ((ABC_PTRUINT_T)pFanin->pCopy) > 0xffff ); // catch small int values or NULL
             Hop_ManPi( pManHop, k )->pData = pFanin->pCopy;
         }
         // compute the truth table of internal nodes

src/opt/ufar/UfarCmd.cpp

@@ -17,6 +17,7 @@
 #include <regex>
 #include <cstdlib>
 #include <cstdio>
+#include <cctype>
 
 #include "base/wlc/wlc.h"
 #include "aig/gia/giaAig.h"
@@ -30,6 +31,22 @@ ABC_NAMESPACE_IMPL_START
 using namespace std;
 
 static UFAR::UfarManager ufar_manager;
+typedef struct Ufar_StopCtx_t_
+{
+    int (*pFuncStop)(int);
+    int nTimeOut;
+    int fActive;
+    timeval TimeStart;
+} Ufar_StopCtx_t;
+#if defined(_MSC_VER)
+__declspec(thread) static Ufar_StopCtx_t g_UfarStopCtx = { NULL, 0, 0, {0, 0} };
+#elif defined(__cplusplus) && __cplusplus >= 201103L
+static thread_local Ufar_StopCtx_t g_UfarStopCtx = { NULL, 0, 0, {0, 0} };
+#elif defined(__STDC_VERSION__) && __STDC_VERSION__ >= 201112L
+static _Thread_local Ufar_StopCtx_t g_UfarStopCtx = { NULL, 0, 0, {0, 0} };
+#else
+static __thread Ufar_StopCtx_t g_UfarStopCtx = { NULL, 0, 0, {0, 0} };
+#endif
 
 static int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAnalyzeCex( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -40,6 +57,38 @@ static int Abc_CommandProveUsingUif( Abc_Frame_t * pAbc, int argc, char ** argv
 static inline Wlc_Ntk_t * Wlc_AbcGetNtk( Abc_Frame_t * pAbc )                       { return (Wlc_Ntk_t *)pAbc->pAbcWlc;                      }
 static inline void        Wlc_AbcFreeNtk( Abc_Frame_t * pAbc )                      { if ( pAbc->pAbcWlc ) Wlc_NtkFree(Wlc_AbcGetNtk(pAbc));  }
 static inline void        Wlc_AbcUpdateNtk( Abc_Frame_t * pAbc, Wlc_Ntk_t * pNtk )  { Wlc_AbcFreeNtk(pAbc); pAbc->pAbcWlc = pNtk;             }
+static inline long long   Ufar_ElapsedUsec( const timeval & Start, const timeval & Stop ) { return 1000000ll * (long long)(Stop.tv_sec - Start.tv_sec) + (long long)(Stop.tv_usec - Start.tv_usec); }
+
+static int Ufar_StopWithTimeout( int RunId )
+{
+    if ( g_UfarStopCtx.pFuncStop && g_UfarStopCtx.pFuncStop(RunId) )
+        return 1;
+    if ( g_UfarStopCtx.fActive && g_UfarStopCtx.nTimeOut > 0 )
+    {
+        timeval Now;
+        gettimeofday( &Now, NULL );
+        if ( Ufar_ElapsedUsec(g_UfarStopCtx.TimeStart, Now) >= 1000000ll * (long long)g_UfarStopCtx.nTimeOut )
+            return 1;
+    }
+    return 0;
+}
+
+struct Ufar_StopScope_t
+{
+    Ufar_StopCtx_t Saved;
+    Ufar_StopScope_t( int (*pFuncStop)(int), int nTimeOut )
+    {
+        Saved = g_UfarStopCtx;
+        g_UfarStopCtx.pFuncStop = pFuncStop;
+        g_UfarStopCtx.nTimeOut = nTimeOut;
+        g_UfarStopCtx.fActive = 1;
+        gettimeofday( &g_UfarStopCtx.TimeStart, NULL );
+    }
+    ~Ufar_StopScope_t()
+    {
+        g_UfarStopCtx = Saved;
+    }
+};
 
 static string Ufar_GetStatusName( Wlc_Ntk_t * pNtk )
 {
@@ -74,6 +123,292 @@ static void Ufar_DumpStatusLog( const string & FileName, int RetValue, const str
     fclose( pFile );
 }
 
+static void Ufar_SetDefaultParams( UFAR::UfarManager::Params & Params, int nTimeOut, int fVerbose, int (*pFuncStop)(int), int RunId )
+{
+    Params = UFAR::UfarManager::Params();
+    Params.RunId = RunId;
+    Params.pFuncStop = pFuncStop;
+    if ( nTimeOut > 0 )
+        Params.nTimeout = nTimeOut;
+    Params.iVerbosity = fVerbose ? 1 : 0;
+}
+static void Ufar_AddOptions( OptMgr & opt_mgr, const UFAR::UfarManager::Params & Params )
+{
+    opt_mgr.AddOpt("--norm", Params.fNorm ? "yes" : "no", "", "toggle using data type normalization");
+    opt_mgr.AddOpt("--adder", "no", "", "toggle including adders");
+    opt_mgr.AddOpt("--cexmin", Params.fCexMin ? "yes" : "no", "", "toggle using CEX minimization");
+    opt_mgr.AddOpt("--sim", "none", "str", "use simulation and specify its setting");
+    opt_mgr.AddOpt("-v", to_string(Params.iVerbosity), "num", "specify verbosity level");
+    opt_mgr.AddOpt("--seq", to_string(Params.nSeqLookBack), "num", "specify the number of look-back frames (0 = no sequential UIF)");
+    opt_mgr.AddOpt("--profile", "no", "", "dump time distribution");
+    opt_mgr.AddOpt("--pba_uif", Params.fPbaUif ? "yes" : "no", "", "toggle using proof-based refinement for UIF pairs");
+    opt_mgr.AddOpt("--lazysim", Params.fLazySim ? "yes" : "no", "", "toggle applying UIF pairs based on simulation");
+    opt_mgr.AddOpt("--pbasim", Params.fPbaSim ? "yes" : "no", "", "toggle combining pba and sim");
+    opt_mgr.AddOpt("--pbacex", Params.fPbaCex ? "yes" : "no", "", "toggle combining pba and cex");
+    opt_mgr.AddOpt("--satmin", Params.fSatMin ? "yes" : "no", "", "toggle using sat-min in pba");
+    opt_mgr.AddOpt("--cbawb", Params.fCbaWb ? "yes" : "no", "", "toggle using cex-based refinement for white boxing");
+    opt_mgr.AddOpt("--grey", Params.fGrey ? "yes" : "no", "", "toggle using grey-box constraints");
+    opt_mgr.AddOpt("--grey2", to_string(Params.nGrey), "float", "specify the greyness threshold");
+    opt_mgr.AddOpt("--allwb", Params.fAllWb ? "yes" : "no", "", "start with all operators white-boxed (no initial abstraction)");
+    opt_mgr.AddOpt("--crossonly", Params.fCrossOnly ? "yes" : "no", "", "allow UIF pairs only across LHS/RHS cones of the miter");
+    opt_mgr.AddOpt("--crossstats", "no", "", "print multiplier counts in LHS/RHS/shared cones and exit");
+    opt_mgr.AddOpt("--dump", "none", "str", "specify file name");
+    opt_mgr.AddOpt("--dump-log", "none", "str", "write status log");
+    opt_mgr.AddOpt("--dump-first-aig", "none", "str", "dump first internal bit-blasted AIG and exit");
+    opt_mgr.AddOpt("--dump-abs", "none", "str", "specify file name");
+    opt_mgr.AddOpt("--par", "none", "str", "use parallel solvers");
+    opt_mgr.AddOpt("--solver", "none", "str", "external solver command line");
+    opt_mgr.AddOpt("--dump_states", "none", "str", "specify the name for the states file");
+    opt_mgr.AddOpt("--read_states", "none", "str", "specify the name for the states file");
+    opt_mgr.AddOpt("--sp", Params.fSuper_prove ? "yes" : "no", "", "toggle using super_prove");
+    opt_mgr.AddOpt("--simp", Params.fSimple ? "yes" : "no", "", "toggle using simple (prove)");
+    opt_mgr.AddOpt("--syn", Params.fSyn ? "yes" : "no", "", "toggle using simple synthesis");
+    opt_mgr.AddOpt("--pth", Params.fPthread ? "yes" : "no", "", "toggle using pthreads");
+    opt_mgr.AddOpt("--onewb", to_string(Params.iOneWb), "int", "specify the mode for one-white-boxing");
+    opt_mgr.AddOpt("--initallpairs", to_string(Params.nInitAllPairsLimit), "num", "pre-seed all compatible UIF pairs when #ops <= this limit (0=off)");
+    opt_mgr.AddOpt("--initnear", to_string(Params.nInitNearMults), "num", "pre-seed UIF pairs among up to this many multipliers closest to output");
+    opt_mgr.AddOpt("--timeout", to_string(Params.nTimeout), "num", "specify the timeout (sec)");
+    opt_mgr.AddOpt("--exp", to_string(Params.iExp), "int", "specify the exp mode");
+    opt_mgr.AddOpt("--miter", "yes", "", "toggle mitering the problem");
+    opt_mgr.AddOpt("--under", "-1", "num", "try under-approximation with the given size");
+}
+static void Ufar_ApplyOptions( OptMgr & opt_mgr, UFAR::UfarManager::Params & Params, set<unsigned> & set_op_types, string & firstAigDumpFile, string & dumpLogFile, int & fNeedMiter, int & fCrossStats, int & UnderSize )
+{
+    firstAigDumpFile = "";
+    dumpLogFile = opt_mgr["--dump-log"] ? opt_mgr.GetOptVal("--dump-log") : "";
+    fNeedMiter = !opt_mgr["--miter"];
+    fCrossStats = opt_mgr["--crossstats"] ? 1 : 0;
+    UnderSize = opt_mgr["--under"] ? stoi(opt_mgr.GetOptVal("--under")) : -1;
+
+    if(opt_mgr["--norm"])
+        Params.fNorm ^= 1;
+    if(opt_mgr["--cexmin"])
+        Params.fCexMin ^= 1;
+    if(opt_mgr["--pba_uif"])
+        Params.fPbaUif ^= 1;
+    if(opt_mgr["--pbasim"])
+        Params.fPbaSim ^= 1;
+    if(opt_mgr["--pbacex"])
+        Params.fPbaCex ^= 1;
+    if(opt_mgr["--satmin"])
+        Params.fSatMin ^= 1;
+    if(opt_mgr["--cbawb"])
+        Params.fCbaWb ^= 1;
+    if(opt_mgr["--grey"])
+        Params.fGrey ^= 1;
+    if(opt_mgr["--allwb"])
+        Params.fAllWb ^= 1;
+    if(opt_mgr["--crossonly"])
+        Params.fCrossOnly ^= 1;
+    if(opt_mgr["--grey2"])
+        Params.nGrey = stof(opt_mgr.GetOptVal("--grey2"));
+    if(opt_mgr["--sp"])
+        Params.fSuper_prove ^= 1;
+    if(opt_mgr["--simp"])
+        Params.fSimple ^= 1;
+    if(opt_mgr["--syn"])
+        Params.fSyn ^= 1;
+    if(opt_mgr["--pth"])
+        Params.fPthread ^= 1;
+    if(opt_mgr["--onewb"])
+        Params.iOneWb = stoi(opt_mgr.GetOptVal("--onewb"));
+    if(opt_mgr["--initallpairs"])
+        Params.nInitAllPairsLimit = stoi(opt_mgr.GetOptVal("--initallpairs"));
+    if(opt_mgr["--initnear"])
+        Params.nInitNearMults = stoi(opt_mgr.GetOptVal("--initnear"));
+    if(opt_mgr["--exp"])
+        Params.iExp = stoi(opt_mgr.GetOptVal("--exp"));
+    if(opt_mgr["--par"])
+        Params.parSetting = opt_mgr.GetOptVal("--par");
+    if(opt_mgr["--solver"])
+        Params.solverSetting = opt_mgr.GetOptVal("--solver");
+    if(opt_mgr["--sim"])
+        Params.simSetting = opt_mgr.GetOptVal("--sim");
+    if(opt_mgr["--dump_states"]) {
+        smatch sub_match;
+        string option = opt_mgr.GetOptVal("--dump_states");
+        if(regex_search(option, sub_match, regex(R"(/?(\w+\.v)$)")))
+            Params.fileStatesOut = sub_match[1].str();
+        else
+            Params.fileStatesOut = opt_mgr.GetOptVal("--dump_states");
+    }
+    if(opt_mgr["--read_states"])
+        Params.fileStatesIn = opt_mgr.GetOptVal("--read_states");
+    if(opt_mgr["--lazysim"])
+        Params.fLazySim ^= 1;
+    if(opt_mgr["-v"])
+        Params.iVerbosity = stoi(opt_mgr.GetOptVal("-v"));
+    if(opt_mgr["--timeout"])
+        Params.nTimeout = stoi(opt_mgr.GetOptVal("--timeout"));
+    if(opt_mgr["--seq"])
+        Params.nSeqLookBack = stoi(opt_mgr.GetOptVal("--seq"));
+    if(opt_mgr["--dump-abs"]) {
+        smatch sub_match;
+        string option = opt_mgr.GetOptVal("--dump-abs");
+        if(regex_search(option, sub_match, regex(R"(/?(\w+)\.v$)")))
+            Params.fileAbs = sub_match[1].str();
+        else
+            Params.fileAbs = opt_mgr.GetOptVal("--dump-abs");
+    }
+    if(opt_mgr["--dump"]) {
+        smatch sub_match;
+        string option = opt_mgr.GetOptVal("--dump");
+        if(regex_search(option, sub_match, regex(R"(/?(\w+\.v)$)")))
+            Params.fileName = sub_match[1].str();
+        else
+            Params.fileName = opt_mgr.GetOptVal("--dump");
+    }
+    if ( opt_mgr["--dump-first-aig"] )
+        firstAigDumpFile = opt_mgr.GetOptVal("--dump-first-aig");
+    set_op_types.insert(WLC_OBJ_ARI_MULTI);
+    if (opt_mgr["--adder"])
+        set_op_types.insert(WLC_OBJ_ARI_ADD);
+}
+static bool Ufar_TokenizeArgs( const char * pArgs, vector<string> & Tokens )
+{
+    string Cur;
+    char Quote = 0;
+    if ( pArgs == NULL )
+        return true;
+    for ( ; *pArgs; ++pArgs )
+    {
+        unsigned char c = (unsigned char)*pArgs;
+        if ( Quote )
+        {
+            if ( c == (unsigned char)Quote )
+                Quote = 0;
+            else if ( c == '\\' && pArgs[1] )
+                Cur += *++pArgs;
+            else
+                Cur += (char)c;
+            continue;
+        }
+        if ( c == '"' || c == '\'' )
+        {
+            Quote = (char)c;
+            continue;
+        }
+        if ( isspace(c) )
+        {
+            if ( !Cur.empty() )
+            {
+                Tokens.push_back( Cur );
+                Cur.clear();
+            }
+            continue;
+        }
+        if ( c == '\\' && pArgs[1] )
+        {
+            Cur += *++pArgs;
+            continue;
+        }
+        Cur += (char)c;
+    }
+    if ( Quote )
+        return false;
+    if ( !Cur.empty() )
+        Tokens.push_back( Cur );
+    return true;
+}
+
+static inline void Ufar_TrimString( string & s )
+{
+    while ( !s.empty() && isspace((unsigned char)s.front()) )
+        s.erase( s.begin() );
+    while ( !s.empty() && isspace((unsigned char)s.back()) )
+        s.pop_back();
+}
+
+static bool Ufar_ExtractSolverArg( const char * pArgs, string & ArgsWithoutSolver, string & SolverArg )
+{
+    string Args = pArgs ? pArgs : "";
+    size_t i = 0, n = Args.size();
+    ArgsWithoutSolver = Args;
+    SolverArg.clear();
+    while ( i < n )
+    {
+        while ( i < n && isspace((unsigned char)Args[i]) )
+            i++;
+        if ( i == n )
+            break;
+        size_t TokenStart = i;
+        char Quote = 0;
+        string Token;
+        while ( i < n )
+        {
+            unsigned char c = (unsigned char)Args[i];
+            if ( Quote )
+            {
+                if ( c == (unsigned char)Quote )
+                    Quote = 0;
+                else if ( c == '\\' && i + 1 < n )
+                    Token += Args[++i];
+                else
+                    Token += (char)c;
+                i++;
+                continue;
+            }
+            if ( c == '"' || c == '\'' )
+            {
+                Quote = (char)c;
+                i++;
+                continue;
+            }
+            if ( isspace(c) )
+                break;
+            if ( c == '\\' && i + 1 < n )
+            {
+                Token += Args[++i];
+                i++;
+                continue;
+            }
+            Token += (char)c;
+            i++;
+        }
+        if ( Token == "--solver" )
+        {
+            size_t ValueStart = i;
+            while ( ValueStart < n && isspace((unsigned char)Args[ValueStart]) )
+                ValueStart++;
+            if ( ValueStart == n )
+                return false;
+            string Prefix = Args.substr( 0, TokenStart );
+            string Suffix;
+            if ( Args[ValueStart] == '"' || Args[ValueStart] == '\'' )
+            {
+                char ValueQuote = Args[ValueStart++];
+                size_t k = ValueStart;
+                while ( k < n )
+                {
+                    unsigned char c = (unsigned char)Args[k];
+                    if ( c == (unsigned char)ValueQuote )
+                    {
+                        k++;
+                        break;
+                    }
+                    if ( c == '\\' && k + 1 < n )
+                        SolverArg += Args[++k];
+                    else
+                        SolverArg += (char)c;
+                    k++;
+                }
+                Suffix = Args.substr( k );
+            }
+            else
+            {
+                SolverArg = Args.substr( ValueStart );
+            }
+            Ufar_TrimString( SolverArg );
+            ArgsWithoutSolver = Prefix + Suffix;
+            Ufar_TrimString( ArgsWithoutSolver );
+            return !SolverArg.empty();
+        }
+        while ( i < n && isspace((unsigned char)Args[i]) )
+            i++;
+    }
+    return false;
+}
+
 
 void Ufar_Init(Abc_Frame_t *pAbc)
 {
@@ -84,39 +419,169 @@ void Ufar_Init(Abc_Frame_t *pAbc)
     //Cmd_CommandAdd( pAbc, "Word level Prove", "%%miter",          Abc_CommandCreateMiter,     0 );
 }
 
-int Ufar_ProveWithTimeout( Wlc_Ntk_t * pNtk, int nTimeOut, int fVerbose, int (*pFuncStop)(int), int RunId )
+int Ufar_ProveWithTimeout( Wlc_Ntk_t * pNtk, int nTimeOut, int fVerbose, int (*pFuncStop)(int), int RunId, const char * pArgs )
 {
     UFAR::UfarManager manager;
     timeval t1;
+    vector<string> Tokens;
+    vector<char *> Argv;
     set<unsigned> set_op_types;
-    Wlc_Ntk_t * pUse = pNtk;
+    string ArgsWithoutSolver, SolverArg;
+    string firstAigDumpFile, dumpLogFile;
+    string statusName;
+    int fNeedMiter = 1, fCrossStats = 0, UnderSize = -1;
+    Wlc_Ntk_t * pUse = pNtk, * pNew = NULL;
     int RetValue = -1;
     if ( pNtk == NULL )
         return -1;
-    if ( Wlc_NtkPoNum(pUse) == 2 )
+    Ufar_SetDefaultParams( manager.params, nTimeOut, fVerbose, pFuncStop, RunId );
+    if ( pArgs && pArgs[0] )
     {
-        pUse = UFAR::CreateMiter( pUse, 0 );
-        if ( pUse == NULL )
+        const char * pParseArgs = pArgs;
+        if ( Ufar_ExtractSolverArg(pArgs, ArgsWithoutSolver, SolverArg) )
+            pParseArgs = ArgsWithoutSolver.c_str();
+        OptMgr opt_mgr("%ufar");
+        Ufar_AddOptions( opt_mgr, manager.params );
+        if ( !Ufar_TokenizeArgs(pParseArgs, Tokens) )
+        {
+            cout << "Cannot parse internal %ufar option string." << endl;
             return -1;
+        }
+        Argv.reserve( Tokens.size() + 1 );
+        Argv.push_back( (char *)"%ufar" );
+        for ( size_t i = 0; i < Tokens.size(); i++ )
+            Argv.push_back( (char *)Tokens[i].c_str() );
+        if ( !opt_mgr.Parse((int)Argv.size(), Argv.data()) )
+        {
+            opt_mgr.PrintUsage();
+            return -1;
+        }
+        Ufar_ApplyOptions( opt_mgr, manager.params, set_op_types, firstAigDumpFile, dumpLogFile, fNeedMiter, fCrossStats, UnderSize );
+        if ( !SolverArg.empty() )
+            manager.params.solverSetting = SolverArg;
+    }
+    else
+        set_op_types.insert( WLC_OBJ_ARI_MULTI );
+    Ufar_StopScope_t StopScope( manager.params.pFuncStop, (int)manager.params.nTimeout );
+    manager.params.pFuncStop = Ufar_StopWithTimeout;
+    if ( fNeedMiter )
+    {
+        if ( Wlc_NtkPoNum(pUse) == 2 )
+        {
+            pNew = UFAR::CreateMiter( pUse, 0 );
+            if ( pUse != pNtk )
+                Wlc_NtkFree( pUse );
+            pUse = pNew;
+            if ( pUse == NULL )
+                return -1;
+        }
+        else if ( Wlc_NtkPoNum(pUse) != 1 )
+        {
+            return -1;
+        }
     }
     else if ( Wlc_NtkPoNum(pUse) != 1 )
         return -1;
-    set_op_types.insert( WLC_OBJ_ARI_MULTI );
+    statusName = Ufar_GetStatusName( pUse );
+    if ( manager.params.fNorm )
+    {
+        pNew = UFAR::NormalizeDataTypes( pUse, set_op_types, true );
+        if ( pUse != pNtk )
+            Wlc_NtkFree( pUse );
+        pUse = pNew;
+    }
+    if ( fCrossStats )
+    {
+        Wlc_Ntk_t * pCur = pUse;
+        if ( Wlc_NtkPoNum(pCur) != 2 )
+        {
+            cout << "CrossStats requires dual outputs before mitering.\n";
+            if ( pUse != pNtk )
+                Wlc_NtkFree( pUse );
+            return -1;
+        }
+        int nObjs = Wlc_NtkObjNumMax(pCur);
+        vector<char> vConeL(nObjs, 0), vConeR(nObjs, 0);
+        auto mark_cone = [&]( int iStart, vector<char>& vMark )
+        {
+            if ( iStart < 0 || iStart >= nObjs )
+                return;
+            vector<int> stack(1, iStart);
+            while ( !stack.empty() )
+            {
+                int iObj = stack.back();
+                stack.pop_back();
+                if ( iObj < 0 || iObj >= nObjs || vMark[iObj] )
+                    continue;
+                vMark[iObj] = 1;
+                Wlc_Obj_t * pObjT = Wlc_NtkObj(pCur, iObj);
+                if ( pObjT->Type == WLC_OBJ_FO )
+                {
+                    Wlc_Obj_t * pFi = Wlc_ObjFo2Fi(pCur, pObjT);
+                    stack.push_back( Wlc_ObjId(pCur, pFi) );
+                }
+                int iFanin, k;
+                Wlc_ObjForEachFanin( pObjT, iFanin, k )
+                    stack.push_back(iFanin);
+            }
+        };
+        int iRootL = Wlc_ObjFaninId0( Wlc_NtkPo(pCur, 0) );
+        int iRootR = Wlc_ObjFaninId0( Wlc_NtkPo(pCur, 1) );
+        mark_cone(iRootL, vConeL);
+        mark_cone(iRootR, vConeR);
+
+        int nL = 0, nR = 0, nB = 0, nN = 0;
+        Wlc_Obj_t * pObjT; int iObj;
+        Wlc_NtkForEachObj( pCur, pObjT, iObj )
+        {
+            if ( pObjT->Type != WLC_OBJ_ARI_MULTI )
+                continue;
+            bool fL = vConeL[iObj] != 0;
+            bool fR = vConeR[iObj] != 0;
+            if ( fL && fR ) nB++;
+            else if ( fL )  nL++;
+            else if ( fR )  nR++;
+            else            nN++;
+        }
+        cout << "UIF_PROVE : CrossStats: L=" << nL
+             << " R=" << nR
+             << " BOTH=" << nB
+             << " NONE=" << nN
+             << " TOTAL=" << (nL + nR + nB + nN) << endl;
+        if ( pUse != pNtk )
+            Wlc_NtkFree( pUse );
+        return -1;
+    }
     if ( !UFAR::HasOperator( pUse, set_op_types ) )
     {
         if ( pUse != pNtk )
             Wlc_NtkFree( pUse );
         return -1;
     }
-    manager.params = UFAR::UfarManager::Params();
-    manager.params.RunId = RunId;
-    manager.params.pFuncStop = pFuncStop;
-    if ( nTimeOut > 0 )
-        manager.params.nTimeout = nTimeOut;
-    manager.params.iVerbosity = fVerbose ? 1 : 0;
+    if ( UnderSize >= 0 )
+    {
+        pNew = UFAR::MakeUnderApprox( pUse, UnderSize );
+        if ( pUse != pNtk )
+            Wlc_NtkFree( pUse );
+        pUse = pNew;
+        pNew = UFAR::MakeUnderApprox2( pUse, set_op_types, UnderSize );
+        if ( pUse != pNtk )
+            Wlc_NtkFree( pUse );
+        pUse = pNew;
+    }
+    if ( !firstAigDumpFile.empty() && firstAigDumpFile != "none" )
+    {
+        Gia_Man_t * pGia = UFAR::BitBlast( pUse );
+        Gia_AigerWriteSimple( pGia, (char *)firstAigDumpFile.c_str() );
+        Gia_ManStop( pGia );
+        if ( pUse != pNtk )
+            Wlc_NtkFree( pUse );
+        return -1;
+    }
     gettimeofday( &t1, NULL );
     manager.Initialize( pUse, set_op_types );
     RetValue = manager.PerformUIFProve( t1 );
+    Ufar_DumpStatusLog( dumpLogFile, RetValue, statusName );
     if ( pUse != pNtk )
         Wlc_NtkFree( pUse );
     return RetValue;
@@ -160,141 +625,22 @@ static int Abc_CommandProveUsingUif( Abc_Frame_t * pAbc, int argc, char ** argv
     ufar_manager.params = UFAR::UfarManager::Params();
 
     OptMgr opt_mgr(argv[0]);
-    opt_mgr.AddOpt("--norm", ufar_manager.params.fNorm ? "yes" : "no", "", "toggle using data type normalization");
-    opt_mgr.AddOpt("--adder", "no", "", "toggle including adders");
-    opt_mgr.AddOpt("--cexmin", ufar_manager.params.fCexMin ? "yes" : "no", "", "toggle using CEX minimization");
-    opt_mgr.AddOpt("--sim", "none", "str", "use simulation and specify its setting");
-    opt_mgr.AddOpt("-v", to_string(ufar_manager.params.iVerbosity), "num", "specify verbosity level");
-    opt_mgr.AddOpt("--seq", to_string(ufar_manager.params.nSeqLookBack), "num", "specify the number of look-back frames (0 = no sequential UIF)");
-    opt_mgr.AddOpt("--profile", "no", "", "dump time distribution");
-    opt_mgr.AddOpt("--pba_uif", ufar_manager.params.fPbaUif ? "yes" : "no", "", "toggle using proof-based refinement for UIF pairs");
-    opt_mgr.AddOpt("--lazysim", ufar_manager.params.fLazySim ? "yes" : "no", "", "toggle applying UIF pairs based on simulation");
-    opt_mgr.AddOpt("--pbasim", ufar_manager.params.fPbaSim ? "yes" : "no", "", "toggle combining pba and sim");
-    opt_mgr.AddOpt("--pbacex", ufar_manager.params.fPbaCex ? "yes" : "no", "", "toggle combining pba and cex");
-    opt_mgr.AddOpt("--satmin", ufar_manager.params.fSatMin ? "yes" : "no", "", "toggle using sat-min in pba");
-    opt_mgr.AddOpt("--cbawb", ufar_manager.params.fCbaWb ? "yes" : "no", "", "toggle using cex-based refinement for white boxing");
-    opt_mgr.AddOpt("--grey", ufar_manager.params.fGrey ? "yes" : "no", "", "toggle using grey-box constraints");
-    opt_mgr.AddOpt("--grey2", to_string(ufar_manager.params.nGrey), "float", "specify the greyness threshold");
-    opt_mgr.AddOpt("--allwb", ufar_manager.params.fAllWb ? "yes" : "no", "", "start with all operators white-boxed (no initial abstraction)");
-    opt_mgr.AddOpt("--crossonly", ufar_manager.params.fCrossOnly ? "yes" : "no", "", "allow UIF pairs only across LHS/RHS cones of the miter");
-    opt_mgr.AddOpt("--crossstats", "no", "", "print multiplier counts in LHS/RHS/shared cones and exit");
-    opt_mgr.AddOpt("--dump", "none", "str", "specify file name");
-    opt_mgr.AddOpt("--dump-log", "none", "str", "write status log");
-    opt_mgr.AddOpt("--dump-first-aig", "none", "str", "dump first internal bit-blasted AIG and exit");
-    opt_mgr.AddOpt("--dump-abs", "none", "str", "specify file name");
-    opt_mgr.AddOpt("--par", "none", "str", "use parallel solvers");
-    opt_mgr.AddOpt("--solver", "none", "str", "external solver command line");
-    opt_mgr.AddOpt("--dump_states", "none", "str", "specify the name for the states file");
-    opt_mgr.AddOpt("--read_states", "none", "str", "specify the name for the states file");
-    opt_mgr.AddOpt("--sp", ufar_manager.params.fSuper_prove ? "yes" : "no", "", "toggle using super_prove");
-    opt_mgr.AddOpt("--simp", ufar_manager.params.fSimple ? "yes" : "no", "", "toggle using simple (prove)");
-    opt_mgr.AddOpt("--syn", ufar_manager.params.fSyn ? "yes" : "no", "", "toggle using simple synthesis");
-    opt_mgr.AddOpt("--pth", ufar_manager.params.fPthread ? "yes" : "no", "", "toggle using pthreads");
-    opt_mgr.AddOpt("--onewb", to_string(ufar_manager.params.iOneWb), "int", "specify the mode for one-white-boxing");
-    opt_mgr.AddOpt("--initallpairs", to_string(ufar_manager.params.nInitAllPairsLimit), "num", "pre-seed all compatible UIF pairs when #ops <= this limit (0=off)");
-    opt_mgr.AddOpt("--initnear", to_string(ufar_manager.params.nInitNearMults), "num", "pre-seed UIF pairs among up to this many multipliers closest to output");
-    opt_mgr.AddOpt("--timeout", to_string(ufar_manager.params.nTimeout), "num", "specify the timeout (sec)");
-    opt_mgr.AddOpt("--exp", to_string(ufar_manager.params.iExp), "int", "specify the exp mode");
-    opt_mgr.AddOpt("--miter", "yes", "", "toggle mitering the problem");
-    opt_mgr.AddOpt("--under", "-1", "num", "try under-approximation with the given size");
+    set<unsigned> set_op_types;
+    string firstAigDumpFile = "";
+    string dumpLogFile = "";
+    int fNeedMiter = 1, fCrossStats = 0, UnderSize = -1;
+    Ufar_AddOptions( opt_mgr, ufar_manager.params );
     if(!opt_mgr.Parse(argc, argv)) {
         opt_mgr.PrintUsage();
         cout << "\n       This command was developed by Yen-Sheng Ho at UC Berkeley in 2015.\n";
         cout << "       https://people.eecs.berkeley.edu/~alanmi/publications/2016/fmcad16_uif.pdf \n"; 
         return 0;
     }
-
-    if(opt_mgr["--norm"])
-        ufar_manager.params.fNorm ^= 1;
-    if(opt_mgr["--cexmin"])
-        ufar_manager.params.fCexMin ^= 1;
-    if(opt_mgr["--pba_uif"])
-        ufar_manager.params.fPbaUif ^= 1;
-    if(opt_mgr["--pbasim"])
-        ufar_manager.params.fPbaSim ^= 1;
-    if(opt_mgr["--pbacex"])
-        ufar_manager.params.fPbaCex ^= 1;
-    if(opt_mgr["--satmin"])
-        ufar_manager.params.fSatMin ^= 1;
-    if(opt_mgr["--cbawb"])
-        ufar_manager.params.fCbaWb ^= 1;
-    if(opt_mgr["--grey"])
-        ufar_manager.params.fGrey ^= 1;
-    if(opt_mgr["--allwb"])
-        ufar_manager.params.fAllWb ^= 1;
-    if(opt_mgr["--crossonly"])
-        ufar_manager.params.fCrossOnly ^= 1;
-    if(opt_mgr["--grey2"])
-        ufar_manager.params.nGrey = stof(opt_mgr.GetOptVal("--grey2"));
-    if(opt_mgr["--sp"])
-        ufar_manager.params.fSuper_prove ^= 1;
-    if(opt_mgr["--simp"])
-        ufar_manager.params.fSimple ^= 1;
-    if(opt_mgr["--syn"])
-        ufar_manager.params.fSyn ^= 1;
-    if(opt_mgr["--pth"])
-        ufar_manager.params.fPthread ^= 1;
-    if(opt_mgr["--onewb"])
-        ufar_manager.params.iOneWb = stoi(opt_mgr.GetOptVal("--onewb"));
-    if(opt_mgr["--initallpairs"])
-        ufar_manager.params.nInitAllPairsLimit = stoi(opt_mgr.GetOptVal("--initallpairs"));
-    if(opt_mgr["--initnear"])
-        ufar_manager.params.nInitNearMults = stoi(opt_mgr.GetOptVal("--initnear"));
-    if(opt_mgr["--exp"])
-        ufar_manager.params.iExp = stoi(opt_mgr.GetOptVal("--exp"));
-    if(opt_mgr["--par"])
-        ufar_manager.params.parSetting = opt_mgr.GetOptVal("--par");
-    if(opt_mgr["--solver"])
-        ufar_manager.params.solverSetting = opt_mgr.GetOptVal("--solver");
-    if(opt_mgr["--sim"])
-        ufar_manager.params.simSetting = opt_mgr.GetOptVal("--sim");
-    if(opt_mgr["--dump_states"]) {
-        smatch sub_match;
-        string option = opt_mgr.GetOptVal("--dump_states");
-        if(regex_search(option, sub_match, regex(R"(/?(\w+\.v)$)")))
-            ufar_manager.params.fileStatesOut = sub_match[1].str();
-        else
-            ufar_manager.params.fileStatesOut = opt_mgr.GetOptVal("--dump_states");
-    }
-    if(opt_mgr["--read_states"])
-        ufar_manager.params.fileStatesIn = opt_mgr.GetOptVal("--read_states");
-    if(opt_mgr["--lazysim"])
-        ufar_manager.params.fLazySim ^= 1;
-    if(opt_mgr["-v"])
-        ufar_manager.params.iVerbosity = stoi(opt_mgr.GetOptVal("-v"));
-    if(opt_mgr["--timeout"])
-        ufar_manager.params.nTimeout = stoi(opt_mgr.GetOptVal("--timeout"));
-    if(opt_mgr["--seq"])
-        ufar_manager.params.nSeqLookBack = stoi(opt_mgr.GetOptVal("--seq"));
-    if(opt_mgr["--dump-abs"]) {
-        smatch sub_match;
-        string option = opt_mgr.GetOptVal("--dump-abs");
-        if(regex_search(option, sub_match, regex(R"(/?(\w+)\.v$)")))
-            ufar_manager.params.fileAbs = sub_match[1].str();
-        else
-            ufar_manager.params.fileAbs = opt_mgr.GetOptVal("--dump-abs");
-    }
-    if(opt_mgr["--dump"]) {
-        smatch sub_match;
-        string option = opt_mgr.GetOptVal("--dump");
-        if(regex_search(option, sub_match, regex(R"(/?(\w+\.v)$)")))
-            ufar_manager.params.fileName = sub_match[1].str();
-        else
-            ufar_manager.params.fileName = opt_mgr.GetOptVal("--dump");
-    }
-    string firstAigDumpFile = "";
-    if ( opt_mgr["--dump-first-aig"] )
-        firstAigDumpFile = opt_mgr.GetOptVal("--dump-first-aig");
+    Ufar_ApplyOptions( opt_mgr, ufar_manager.params, set_op_types, firstAigDumpFile, dumpLogFile, fNeedMiter, fCrossStats, UnderSize );
 
     // ufar_manager.DumpParams();
     LogT::prefix = "UIF_PROVE";
-    string dumpLogFile = opt_mgr["--dump-log"] ? opt_mgr.GetOptVal("--dump-log") : "";
     string statusName = Ufar_GetStatusName( Wlc_AbcGetNtk(pAbc) );
-
-    set<unsigned> set_op_types;
-    set_op_types.insert(WLC_OBJ_ARI_MULTI);
-    if (opt_mgr["--adder"])
-        set_op_types.insert(WLC_OBJ_ARI_ADD);
     if (!UFAR::HasOperator(Wlc_AbcGetNtk(pAbc), set_op_types)) {
         cout << "There is no operator for UIF.\n";
         return 0;
@@ -304,7 +650,7 @@ static int Abc_CommandProveUsingUif( Abc_Frame_t * pAbc, int argc, char ** argv
     timeval t1, t2;
     gettimeofday(&t1, NULL);
 
-    if (!opt_mgr["--miter"]) {
+    if (fNeedMiter) {
         if (Wlc_NtkPoNum(Wlc_AbcGetNtk(pAbc)) != 2) {
             cout << "The current design doesn't have dual outputs.\n";
             return 0;
@@ -318,7 +664,7 @@ static int Abc_CommandProveUsingUif( Abc_Frame_t * pAbc, int argc, char ** argv
         Wlc_AbcUpdateNtk(pAbc, pNew);
     }
 
-    if ( opt_mgr["--crossstats"] )
+    if ( fCrossStats )
     {
         Wlc_Ntk_t * pCur = Wlc_AbcGetNtk(pAbc);
         if ( Wlc_NtkPoNum(pCur) != 2 )
@@ -380,10 +726,10 @@ static int Abc_CommandProveUsingUif( Abc_Frame_t * pAbc, int argc, char ** argv
         return 0;
     }
 
-    if (opt_mgr["--under"]) {
-        pNew = UFAR::MakeUnderApprox(Wlc_AbcGetNtk(pAbc), stoi(opt_mgr.GetOptVal("--under")));
+    if ( UnderSize >= 0 ) {
+        pNew = UFAR::MakeUnderApprox(Wlc_AbcGetNtk(pAbc), UnderSize);
         Wlc_AbcUpdateNtk(pAbc, pNew);
-        pNew = UFAR::MakeUnderApprox2(Wlc_AbcGetNtk(pAbc), set_op_types, stoi(opt_mgr.GetOptVal("--under")));
+        pNew = UFAR::MakeUnderApprox2(Wlc_AbcGetNtk(pAbc), set_op_types, UnderSize);
         Wlc_AbcUpdateNtk(pAbc, pNew);
         Wlc_WriteVer(Wlc_AbcGetNtk(pAbc), "UND.v", 0, 0);
     }

src/opt/ufar/UfarCmd.h

@@ -15,7 +15,7 @@ ABC_NAMESPACE_HEADER_START
 void Ufar_Init(Abc_Frame_t *pAbc);
 
 typedef struct Wlc_Ntk_t_ Wlc_Ntk_t;
-extern int Ufar_ProveWithTimeout( Wlc_Ntk_t * pNtk, int nTimeOut, int fVerbose, int (*pFuncStop)(int), int RunId );
+extern int Ufar_ProveWithTimeout( Wlc_Ntk_t * pNtk, int nTimeOut, int fVerbose, int (*pFuncStop)(int), int RunId, const char * pArgs );
 
 ABC_NAMESPACE_HEADER_END
 

src/opt/untk/NtkNtk.cpp

@@ -805,7 +805,8 @@ Wlc_Ntk_t * AddConstFlops( Wlc_Ntk_t * pNtk, const set<unsigned>& types )
     Wlc_Ntk_t * p = Wlc_NtkDupDfsSimple(pNtk);
     Wlc_NtkCleanCopy( p );
     int nOrigObjNum = Wlc_NtkObjNumMax(p);
-    Wlc_NtkTransferNames( p, pNtk );
+    if ( !Wlc_NtkHasNameId(p) && Wlc_NtkHasNameId(pNtk) )
+        Wlc_NtkTransferNames( p, pNtk );
 
     Wlc_Obj_t * pObj;
     int i, iObjConst0;
@@ -872,7 +873,8 @@ Wlc_Ntk_t * AddConstFlops( Wlc_Ntk_t * pNtk, const set<unsigned>& types )
     ModifyMarkedNodes(p, nOrigObjNum, create_ff_and_mux);
 
     Wlc_Ntk_t * pNew = Wlc_NtkDupDfsSimple( p );
-    Wlc_NtkTransferNames( pNew, p );
+    if ( !Wlc_NtkHasNameId(pNew) && Wlc_NtkHasNameId(p) )
+        Wlc_NtkTransferNames( pNew, p );
 
     Wlc_NtkFree( p );
 
@@ -1058,7 +1060,8 @@ Wlc_Ntk_t * NormalizeDataTypes(Wlc_Ntk_t * p, const set<unsigned>& types, bool f
     Wlc_Ntk_t *pNtk, *pNew;
 
     pNtk = Wlc_NtkDupDfsSimple(p);
-    Wlc_NtkTransferNames( pNtk, p );
+    if ( !Wlc_NtkHasNameId(pNtk) && Wlc_NtkHasNameId(p) )
+        Wlc_NtkTransferNames( pNtk, p );
 
     Wlc_Obj_t *pObj;
     int i, iFanin0, iFanin1;
@@ -1117,7 +1120,8 @@ Wlc_Ntk_t * NormalizeDataTypes(Wlc_Ntk_t * p, const set<unsigned>& types, bool f
     Vec_IntFree(vFanins);
 
     pNew = Wlc_NtkDupDfsSimple(pNtk);
-    Wlc_NtkTransferNames( pNew, pNtk );
+    if ( !Wlc_NtkHasNameId(pNew) && Wlc_NtkHasNameId(pNtk) )
+        Wlc_NtkTransferNames( pNew, pNtk );
     Wlc_NtkFree(pNtk);
 
     return pNew;
@@ -1266,11 +1270,15 @@ static inline int run_external_solver_on_aig( Abc_Ntk_t * pAbcNtk, const string&
     Io_Write( pAbcNtk, (char *)pAigFile, IO_FILE_AIGER );
     std::remove( "status.txt" );
     std::remove( "log.txt" );
-    string command = solverCmd;
-    if ( command.find(pAigFile) == string::npos )
-        command += string(" ") + pAigFile;
+    string solverCall = solverCmd;
+    string command;
+    if ( solverCall.find(pAigFile) == string::npos )
+        solverCall += string(" ") + pAigFile;
     if ( nRuntimeLimitSec > 0 )
-        command += " " + to_string(nRuntimeLimitSec);
+        solverCall += " " + to_string(nRuntimeLimitSec);
+    command = solverCall;
+    if ( nRuntimeLimitSec > 0 )
+        command = "timeout " + to_string(nRuntimeLimitSec) + " " + command;
     command += " > log.txt 2>&1";
     LOG(1) << "UFAR external solver: launching command instead of PDR: " << command;
 #ifdef __wasm

src/proof/abs/absGla.c

@@ -1847,7 +1847,8 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars )
         }
     }
 finish:
-    Prf_ManStopP( &p->pSat->pPrf2 );
+    if ( p->pSat )
+        Prf_ManStopP( &p->pSat->pPrf2 );
     // cancel old one if it is proving
     if ( iFrameTryToProve >= 0 )
         Gia_GlaProveCancel( pPars->fVerbose );
@@ -1860,9 +1861,9 @@ finish:
     {
         Vec_IntFreeP( &pAig->vGateClasses );
         pAig->vGateClasses = Ga2_ManAbsTranslate( p );
-        if ( p->pPars->nTimeOut && Abc_Clock() >= p->pSat->nRuntimeLimit ) 
+        if ( p->pSat && p->pPars->nTimeOut && Abc_Clock() >= p->pSat->nRuntimeLimit ) 
             Abc_Print( 1, "GLA reached timeout %d sec in frame %d with a %d-stable abstraction.    ", p->pPars->nTimeOut, p->pPars->iFrameProved+1, p->pPars->nFramesNoChange );
-        else if ( pPars->nConfLimit && sat_solver2_nconflicts(p->pSat) >= pPars->nConfLimit )
+        else if ( p->pSat && pPars->nConfLimit && sat_solver2_nconflicts(p->pSat) >= pPars->nConfLimit )
             Abc_Print( 1, "GLA exceeded %d conflicts in frame %d with a %d-stable abstraction.  ", pPars->nConfLimit, p->pPars->iFrameProved+1, p->pPars->nFramesNoChange );
         else if ( pPars->nRatioMin2 && Vec_IntSize(p->vAbs) >= p->nMarked * pPars->nRatioMin2 / 100 )
             Abc_Print( 1, "GLA found that the size of abstraction exceeds %d %% in frame %d during refinement.  ", pPars->nRatioMin2, p->pPars->iFrameProved+1 );
@@ -1893,7 +1894,8 @@ finish:
         ABC_PRTP( "Runtime: Refinement  ", p->timeCex,    Abc_Clock() - clk );
         ABC_PRTP( "Runtime: Other       ", p->timeOther,  Abc_Clock() - clk );
         ABC_PRTP( "Runtime: TOTAL       ", Abc_Clock() - clk, Abc_Clock() - clk );
-        Ga2_ManReportMemory( p );
+        if ( p->pSat )
+            Ga2_ManReportMemory( p );
     }
 //    Ga2_ManDumpStats( p->pGia, p->pPars, p->pSat, p->pPars->iFrameProved, 0 );
     Ga2_ManStop( p );

src/proof/cec/cec.h

@@ -167,6 +167,7 @@ struct Cec_ParCor_t_
 //    int              fFirstStop;    // stop on the first sat output
     int              fUseSmartCnf;  // use smart CNF computation
     int              fStopWhenGone; // quit when PO is not a candidate constant
+    int              fIncremental;  // active-list/TFO-triggered reproof in main loop
     int              fVerboseFlops; // verbose stats
     int              fVeryVerbose;  // verbose stats
     int              fVerbose;      // verbose stats

src/proof/cec/cecCorr.c

@@ -34,7 +34,10 @@ static inline int Cec_ParCorShouldStop( Cec_ParCor_t * pPars )
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static void Gia_ManCorrSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix );
+// Shared with cecCorrIncr.c (declared in cecInt.h).
+extern void Gia_ManCorrSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix );
+extern int  Gia_ManCorrSpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix );
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -45,13 +48,13 @@ static void Gia_ManCorrSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_
   Synopsis    [Computes the real value of the literal w/o spec reduction.]
 
   Description []
-               
+
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-static inline int Gia_ManCorrSpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix )
+int Gia_ManCorrSpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix )
 {
     if ( Gia_ObjIsAnd(pObj) )
     {
@@ -762,6 +765,7 @@ void Cec_ManRefinedClassPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIte
     Abc_Print( 1, "p =%6d  d =%6d  f =%6d  ", nProve, nDispr, nFail );
     Abc_Print( 1, "%c  ", Gia_ObjIsConst( p, Gia_ObjFaninId0p(p, Gia_ManPo(p, 0)) ) ? '+' : '-' );
     Abc_PrintTime( 1, "T", Time );
+    fflush( stdout );
 }
 int Cec_ManCountLits( Gia_Man_t * p )
 { 
@@ -791,7 +795,7 @@ int Cec_ManCountLits( Gia_Man_t * p )
 
 ***********************************************************************/
 void Cec_ManLSCorrespondenceBmc( Gia_Man_t * pAig, Cec_ParCor_t * pPars, int nPrefs )
-{  
+{
     Cec_ParSim_t ParsSim, * pParsSim = &ParsSim;
     Cec_ParSat_t ParsSat, * pParsSat = &ParsSat;
     Vec_Str_t * vStatus;
@@ -800,6 +804,7 @@ void Cec_ManLSCorrespondenceBmc( Gia_Man_t * pAig, Cec_ParCor_t * pPars, int nPr
     Cec_ManSim_t * pSim;
     Gia_Man_t * pSrm;
     int fChanges, RetValue, i;
+    Cec_IncrMgr_t * pBmcMgr = NULL;
     // prepare simulation manager
     Cec_ManSimSetDefaultParams( pParsSim );
     pParsSim->nWords     = pPars->nWords;
@@ -812,20 +817,44 @@ void Cec_ManLSCorrespondenceBmc( Gia_Man_t * pAig, Cec_ParCor_t * pPars, int nPr
     Cec_ManSatSetDefaultParams( pParsSat );
     pParsSat->nBTLimit = pPars->nBTLimit;
     pParsSat->fVerbose = pPars->fVerbose;
+    if ( pPars->fIncremental )
+    {
+        pBmcMgr = Cec_IncrMgrAlloc( pAig, pPars->nFrames + nPrefs );
+        Cec_IncrMgrSnapshotClasses( pBmcMgr );
+    }
     fChanges = 1;
     for ( i = 0; fChanges && (!pPars->nLimitMax || i < pPars->nLimitMax); i++ )
     {
+        int * pTfoMask = NULL;
+        int nReprSeeds = 0, nTotalPairs = 0, nActivePairs = 0, fConverged = 0;
         if ( Cec_ParCorShouldStop( pPars ) )
             break;
         abctime clkBmc = Abc_Clock();
         fChanges = 0;
-        pSrm = Gia_ManCorrSpecReduceInit( pAig, pPars->nFrames, nPrefs, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings );
+        // BMC SRM is non-ring (Gia_ManCorrSpecReduceInit ignores fRings);
+        // the incremental mask filters on pReprs-derived endpoints only.
+        if ( pBmcMgr && i > 0 )
+        {
+            pTfoMask = Cec_IncrMgrDecideMask( pBmcMgr, 0, &fConverged,
+                                              &nReprSeeds, NULL, &nTotalPairs, &nActivePairs );
+            if ( fConverged )
+                break;
+        }
+        if ( pTfoMask )
+            pSrm = Gia_ManCorrSpecReduceInit_Active( pAig, pPars->nFrames, nPrefs, !pPars->fLatchCorr, &vOutputs, pTfoMask );
+        else
+            pSrm = Gia_ManCorrSpecReduceInit( pAig, pPars->nFrames, nPrefs, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings );
+        if ( pTfoMask && pPars->fVeryVerbose )
+            Abc_Print( 1, "  [bmc-incr i=%d repr=%d active=%d/%d POs=%d]\n",
+                       i, nReprSeeds, nActivePairs, nTotalPairs, Gia_ManCoNum(pSrm) );
+        if ( pBmcMgr )
+            Cec_IncrMgrSnapshotClasses( pBmcMgr );
         if ( Gia_ManPoNum(pSrm) == 0 )
         {
             Gia_ManStop( pSrm );
             Vec_IntFree( vOutputs );
             break;
-        } 
+        }
         pParsSat->nBTLimit *= 10;
         if ( pPars->fUseCSat )
             vCexStore = Tas_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 );
@@ -848,6 +877,7 @@ void Cec_ManLSCorrespondenceBmc( Gia_Man_t * pAig, Cec_ParCor_t * pPars, int nPr
         if ( Cec_ParCorShouldStop( pPars ) )
             break;
     }
+    Cec_IncrMgrFree( pBmcMgr );
     Cec_ManSimStop( pSim );
 }
 
@@ -948,6 +978,9 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
     abctime clkTotal = Abc_Clock();
     abctime clkSat = 0, clkSim = 0, clkSrm = 0;
     abctime clk2, clk = Abc_Clock();
+    Cec_IncrMgr_t * pMgr = NULL;     // incremental manager (NULL when -i is off)
+    abctime clkIncr = 0;
+    int nIncrSkipped = 0, nIncrFallback = 0;
     if ( Gia_ManRegNum(pAig) == 0 )
     {
         Abc_Print( 1, "Cec_ManLatchCorrespondence(): Not a sequential AIG.\n" );
@@ -994,27 +1027,69 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
     if ( pPars->nStepsMax == 0 )
     {
         Abc_Print( 1, "Stopped signal correspondence after BMC.\n" );
+        fflush( stdout );
         Cec_ManSimStop( pSim );
         return 1;
     }
+    if ( pPars->fIncremental )
+    {
+        pMgr = Cec_IncrMgrAlloc( pAig, pPars->nFrames );
+        Cec_IncrMgrSnapshotClasses( pMgr );
+    }
     // perform refinement of equivalence classes
     for ( r = 0; r < nIterMax; r++ )
-    { 
+    {
         if ( Cec_ParCorShouldStop( pPars ) )
         {
             Cec_ManSimStop( pSim );
+            Cec_IncrMgrFree( pMgr );
             return 1;
         }
         if ( pPars->nStepsMax == r )
         {
             Cec_ManSimStop( pSim );
+            Cec_IncrMgrFree( pMgr );
             Abc_Print( 1, "Stopped signal correspondence after %d refiment iterations.\n", r );
+            fflush( stdout );
             return 1;
         }
         clk = Abc_Clock();
-        // perform speculative reduction
+        // perform speculative reduction (with optional active-list filter)
         clk2 = Abc_Clock();
-        pSrm = Gia_ManCorrSpecReduce( pAig, pPars->nFrames, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings );
+        {
+            int * pTfoMask = NULL;
+            int nReprSeeds = 0, nNextChanges = 0, nTotalPairs = 0, nActivePairs = 0;
+            int fConverged = 0;
+            if ( pMgr && r > 0 )
+            {
+                abctime clkI = Abc_Clock();
+                pTfoMask = Cec_IncrMgrDecideMask( pMgr, pPars->fUseRings, &fConverged,
+                                                  &nReprSeeds, &nNextChanges,
+                                                  &nTotalPairs, &nActivePairs );
+                clkIncr += Abc_Clock() - clkI;
+                if ( fConverged )
+                {
+                    clkSrm += Abc_Clock() - clk2;
+                    break;
+                }
+                if ( pTfoMask == NULL )
+                    nIncrFallback++;
+                else
+                    nIncrSkipped += nTotalPairs - nActivePairs;
+            }
+            if ( pTfoMask )
+                pSrm = Gia_ManCorrSpecReduce_Active( pAig, pPars->nFrames, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings, pTfoMask, pMgr );
+            else
+                pSrm = Gia_ManCorrSpecReduce( pAig, pPars->nFrames, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings );
+            if ( pTfoMask && pPars->fVeryVerbose )
+                Abc_Print( 1, "  [incr r=%d repr=%d next=%d tfo=%d active=%d/%d POs=%d]\n",
+                           r, nReprSeeds, nNextChanges, Vec_IntSize(pMgr->vTfoNodes),
+                           nActivePairs, nTotalPairs, Gia_ManCoNum(pSrm) );
+            // Snapshot AFTER SRM build: the active builder still reads the
+            // previous pNexts to recognise newly-created ring edges.
+            if ( pMgr )
+                Cec_IncrMgrSnapshotClasses( pMgr );
+        }
         assert( Gia_ManRegNum(pSrm) == 0 && Gia_ManPiNum(pSrm) == Gia_ManRegNum(pAig)+(pPars->nFrames+!pPars->fLatchCorr)*Gia_ManPiNum(pAig) );
         clkSrm += Abc_Clock() - clk2;
         if ( Gia_ManCoNum(pSrm) == 0 )
@@ -1055,6 +1130,7 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
         if ( Cec_ParCorShouldStop( pPars ) )
         {
             Cec_ManSimStop( pSim );
+            Cec_IncrMgrFree( pMgr );
             return 1;
         }
         // quit if const is no longer there
@@ -1062,7 +1138,9 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
         {
             printf( "Iterative refinement is stopped after iteration %d\n", r );
             printf( "because the property output is no longer a candidate constant.\n" );
+            fflush( stdout );
             Cec_ManSimStop( pSim );
+            Cec_IncrMgrFree( pMgr );
             return 0;
         }
         if ( pPars->nLimitMax )
@@ -1072,7 +1150,9 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
             {
                 printf( "Iterative refinement is stopped after iteration %d\n", r );
                 printf( "because refinement does not proceed quickly.\n" );
+                fflush( stdout );
                 Cec_ManSimStop( pSim );
+                Cec_IncrMgrFree( pMgr );
                 ABC_FREE( pAig->pReprs );
                 ABC_FREE( pAig->pNexts );
                 return 0;
@@ -1100,10 +1180,17 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
         ABC_PRTP( "Sat  ", clkSat,                        clkTotal );
         ABC_PRTP( "Sim  ", clkSim,                        clkTotal );
         ABC_PRTP( "Other", clkTotal-clkSat-clkSrm-clkSim, clkTotal );
+        if ( pMgr )
+        {
+            ABC_PRTP( "Incr ", clkIncr, clkTotal );
+            Abc_Print( 1, "Incr: fallback rounds = %d, skipped candidate pairs = %d\n", nIncrFallback, nIncrSkipped );
+        }
         Abc_PrintTime( 1, "TOTAL",  clkTotal );
+        fflush( stdout );
     }
+    Cec_IncrMgrFree( pMgr );
     return 1;
-}    
+}
 
 /**Function*************************************************************
 
@@ -1299,42 +1386,107 @@ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Wec_t * Gia_ManCreateRegSupps( Gia_Man_t * p, int fVerbose )
+static inline void Gia_ManStopFlopSuppAdd( int * pReg0, int * pReg1, int * pnRegs, int Reg )
 {
-    abctime clk = Abc_Clock();
-    Gia_Obj_t * pObj; int i, Id;
-    Vec_Wec_t * vSuppsR = Vec_WecStart( Gia_ManRegNum(p) );
-    Vec_Wec_t * vSupps  = Vec_WecStart( Gia_ManObjNum(p) );
-    Gia_ManForEachRo( p, pObj, i )
-        Vec_IntPush( Vec_WecEntry(vSupps, Gia_ObjId(p, pObj)), i );
-    Gia_ManForEachAnd( p, pObj, Id )
-        Vec_IntTwoMerge2( Vec_WecEntry(vSupps, Gia_ObjFaninId0(pObj, Id)), 
-                          Vec_WecEntry(vSupps, Gia_ObjFaninId1(pObj, Id)), 
-                          Vec_WecEntry(vSupps, Id) ); 
-    Gia_ManForEachRi( p, pObj, i )
-        Vec_IntAppend( Vec_WecEntry(vSuppsR, i), Vec_WecEntry(vSupps, Gia_ObjFaninId0p(p, pObj)) );
-    Vec_WecFree( vSupps );
-    if ( fVerbose )
-        Abc_PrintTime( 1, "Support computation", Abc_Clock() - clk );
-    return vSuppsR;
+    if ( *pnRegs == 3 )
+        return;
+    if ( *pnRegs == 0 )
+    {
+        *pReg0 = Reg;
+        *pnRegs = 1;
+        return;
+    }
+    if ( *pnRegs == 1 )
+    {
+        if ( *pReg0 == Reg )
+            return;
+        *pReg1 = Reg;
+        *pnRegs = 2;
+        return;
+    }
+    assert( *pnRegs == 2 );
+    if ( *pReg0 == Reg || *pReg1 == Reg )
+        return;
+    *pnRegs = 3;
 }
 Vec_Int_t * Gia_ManFindStopFlops( Gia_Man_t * p, int nFlopIncFreq, int fVerbose )
 {
-    Vec_Int_t * vRes = NULL, * vTemp;  int i, k, Spot, Temp, nItems = 0;
-    Vec_Wec_t * vSupps = Gia_ManCreateRegSupps( p, fVerbose );
+    abctime clk = Abc_Clock();
+    Gia_Obj_t * pObj;
+    Vec_Int_t * vRes = NULL;
     Vec_Int_t * vNexts = Vec_IntStartFull( Gia_ManRegNum(p) );
     Vec_Int_t * vAvail = Vec_IntStart( Gia_ManRegNum(p) );
     Vec_Int_t * vHeads = Vec_IntAlloc( 10 );
-    Vec_WecForEachLevel( vSupps, vTemp, i ) {
-        if ( Vec_IntSize(vTemp) > 2 )
-            continue;
-        if ( (Spot = Vec_IntFind(vTemp, i)) >= 0 )
-            Vec_IntDrop( vTemp, Spot );
-        if ( Vec_IntSize(vTemp) != 1 )
-            continue;
-        Vec_IntWriteEntry( vNexts, i, Vec_IntEntry(vTemp, 0) );
-        Vec_IntWriteEntry( vAvail, Vec_IntEntry(vTemp, 0), 1 );
+    unsigned char * pSuppN = ABC_CALLOC( unsigned char, Gia_ManObjNum(p) );
+    int * pSupp0 = ABC_ALLOC( int, Gia_ManObjNum(p) );
+    int * pSupp1 = ABC_ALLOC( int, Gia_ManObjNum(p) );
+    int i, k, Id, Fan0, Fan1, Count, Next, Spot, Temp, nItems = 0;
+
+    // Track at most two distinct flop supports per node; value 3 means "many".
+    Gia_ManForEachRo( p, pObj, i )
+    {
+        Id = Gia_ObjId( p, pObj );
+        pSuppN[Id] = 1;
+        pSupp0[Id] = i;
     }
+    Gia_ManForEachAnd( p, pObj, Id )
+    {
+        int Reg0 = -1, Reg1 = -1, nRegs = 0;
+        Fan0 = Gia_ObjFaninId0( pObj, Id );
+        Fan1 = Gia_ObjFaninId1( pObj, Id );
+        if ( pSuppN[Fan0] == 3 || pSuppN[Fan1] == 3 )
+        {
+            pSuppN[Id] = 3;
+            continue;
+        }
+        if ( pSuppN[Fan0] > 0 )
+        {
+            Gia_ManStopFlopSuppAdd( &Reg0, &Reg1, &nRegs, pSupp0[Fan0] );
+            if ( pSuppN[Fan0] > 1 )
+                Gia_ManStopFlopSuppAdd( &Reg0, &Reg1, &nRegs, pSupp1[Fan0] );
+        }
+        if ( pSuppN[Fan1] > 0 )
+        {
+            Gia_ManStopFlopSuppAdd( &Reg0, &Reg1, &nRegs, pSupp0[Fan1] );
+            if ( pSuppN[Fan1] > 1 )
+                Gia_ManStopFlopSuppAdd( &Reg0, &Reg1, &nRegs, pSupp1[Fan1] );
+        }
+        pSuppN[Id] = nRegs;
+        if ( nRegs > 0 )
+            pSupp0[Id] = Reg0;
+        if ( nRegs > 1 )
+            pSupp1[Id] = Reg1;
+    }
+    if ( fVerbose )
+    {
+        Abc_PrintTime( 1, "Support computation", Abc_Clock() - clk );
+        fflush( stdout );
+    }
+
+    Gia_ManForEachRi( p, pObj, i )
+    {
+        Id = Gia_ObjFaninId0p( p, pObj );
+        Count = pSuppN[Id];
+        Next = -1;
+        if ( Count == 1 )
+            Next = pSupp0[Id] == i ? -1 : pSupp0[Id];
+        else if ( Count == 2 )
+        {
+            if ( pSupp0[Id] == i && pSupp1[Id] != i )
+                Next = pSupp1[Id];
+            else if ( pSupp1[Id] == i && pSupp0[Id] != i )
+                Next = pSupp0[Id];
+        }
+        if ( Next >= 0 )
+        {
+            Vec_IntWriteEntry( vNexts, i, Next );
+            Vec_IntWriteEntry( vAvail, Next, 1 );
+        }
+    }
+    ABC_FREE( pSuppN );
+    ABC_FREE( pSupp0 );
+    ABC_FREE( pSupp1 );
+
     Vec_IntForEachEntry( vNexts, Spot, i )
         if ( Spot >= 0 && Vec_IntEntry(vAvail, i) == 0 )
             Vec_IntPush( vHeads, i );
@@ -1366,11 +1518,13 @@ Vec_Int_t * Gia_ManFindStopFlops( Gia_Man_t * p, int nFlopIncFreq, int fVerbose
         }
     }
     if ( fVerbose && vRes ) 
+    {
         printf( "Detected %d sequence%s containing %d flops.\n", nItems, nItems > 1 ? "s":"", Vec_IntSize(vRes) );
+        fflush( stdout );
+    }
     Vec_IntFree( vNexts );
     Vec_IntFree( vAvail );
     Vec_IntFree( vHeads );
-    Vec_WecFree( vSupps );
     return vRes;
 }
 Gia_Man_t * Gia_ManDupStopsAdd( Gia_Man_t * p, Vec_Int_t * vStops )

src/proof/cec/cecCorrIncr.c

@@ -0,0 +1,674 @@
+/**CFile****************************************************************
+
+  FileName    [cecCorrIncr.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Combinational equivalence checking.]
+
+  Synopsis    [Incremental active-list / TFO filter for &scorr.]
+
+  Author      [Xiran Zhao]
+
+  Affiliation [University of Chinese Academy of Sciences]
+
+  Date        [Ver. 1.0. Started - May 2026.]
+
+***********************************************************************/
+
+#include "cecInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates the incremental active-list manager.]
+
+  Description [The manager owns one snapshot of pReprs/pNexts plus the
+  TFO bookkeeping arrays.  pAig must outlive the manager; the manager
+  never duplicates the AIG, only references it.  If the host AIG does
+  not yet carry a static fanout, this routine builds it and remembers
+  to tear it down on Free.]
+
+  SideEffects [Builds static fanout on pAig if not already present.]
+
+  SeeAlso     []
+
+***********************************************************************/
+Cec_IncrMgr_t * Cec_IncrMgrAlloc( Gia_Man_t * pAig, int nFrames )
+{
+    Cec_IncrMgr_t * p = ABC_CALLOC( Cec_IncrMgr_t, 1 );
+    p->pAig      = pAig;
+    p->nFrames   = nFrames;
+    p->nObjs     = Gia_ManObjNum(pAig);
+    p->vReprPrev = Vec_IntStartFull( p->nObjs );
+    p->vNextPrev = Vec_IntStart( p->nObjs );
+    p->vSeeds    = Vec_IntAlloc( 64 );
+    p->vTfoNodes = Vec_IntAlloc( 1024 );
+    p->pTfoMark  = ABC_CALLOC( int, p->nObjs );
+    p->vBfsCur   = Vec_IntAlloc( 1024 );
+    p->vBfsNext  = Vec_IntAlloc( 1024 );
+    if ( pAig->vFanout == NULL )
+    {
+        Gia_ManStaticFanoutStart( pAig );
+        p->fOwnsFanout = 1;
+    }
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Frees the incremental manager.]
+
+  Description [Releases all internal vectors and the TFO mark array.
+  If the manager built the static fanout on Alloc, it is also torn
+  down here.  Safe to call with a NULL pointer.]
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_IncrMgrFree( Cec_IncrMgr_t * p )
+{
+    if ( p == NULL ) return;
+    if ( p->fOwnsFanout )
+        Gia_ManStaticFanoutStop( p->pAig );
+    Vec_IntFree( p->vReprPrev );
+    Vec_IntFree( p->vNextPrev );
+    Vec_IntFree( p->vSeeds );
+    Vec_IntFree( p->vTfoNodes );
+    Vec_IntFree( p->vBfsCur );
+    Vec_IntFree( p->vBfsNext );
+    ABC_FREE( p->pTfoMark );
+    ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Snapshots the current equivalence-class state.]
+
+  Description [Copies the per-node pReprs and pNexts arrays into the
+  manager so the next iteration can diff against the class state whose
+  pairs were just emitted into the SRM.  Should be called after SRM
+  construction and before SAT/sim refinement: the snapshot then reflects
+  exactly the pairs the SAT solver was asked to prove.  O(N).]
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_IncrMgrSnapshotClasses( Cec_IncrMgr_t * p )
+{
+    Gia_Man_t * pAig = p->pAig;
+    int i;
+    assert( pAig->pReprs != NULL );
+    for ( i = 0; i < p->nObjs; i++ )
+    {
+        Vec_IntWriteEntry( p->vReprPrev, i, Gia_ObjRepr(pAig, i) );
+        Vec_IntWriteEntry( p->vNextPrev, i, pAig->pNexts ? Gia_ObjNext(pAig, i) : 0 );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the seed set for the next TFO BFS.]
+
+  Description [Returns the number of nodes whose representative changed
+  since the last snapshot; the seeds themselves are stored in vSeeds and
+  consumed by Cec_IncrMgrComputeTfo.  Does not update the snapshot --
+  the caller decides when to snapshot.  pNexts changes are intentionally
+  excluded here: a ring-link rewrite is an edge-local event that creates
+  a new ring edge to reprove, not a new fanout cone, so it is handled by
+  Cec_IncrMgrRingEdgeChanged at SRM emission time.]
+
+  SideEffects []
+
+  SeeAlso     [Cec_IncrMgrComputeTfo Cec_IncrMgrRingEdgeChanged]
+
+***********************************************************************/
+int Cec_IncrMgrComputeSeeds( Cec_IncrMgr_t * p )
+{
+    Gia_Man_t * pAig = p->pAig;
+    int i, reprNew, reprOld;
+    Vec_IntClear( p->vSeeds );
+    for ( i = 1; i < p->nObjs; i++ )
+    {
+        reprNew = Gia_ObjRepr( pAig, i );
+        reprOld = Vec_IntEntry( p->vReprPrev, i );
+        if ( reprNew != reprOld )
+            Vec_IntPush( p->vSeeds, i );
+    }
+    return Vec_IntSize( p->vSeeds );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts nodes whose ring-list successor changed.]
+
+  Description [Used only for convergence and fallback decisions.  These
+  nodes are NOT TFO seeds, because a pNexts-only change creates a new
+  ring edge (proved edge-locally by the active SRM builder) rather than
+  a new fanout cone to re-prove.  Returns 0 when pNexts is unallocated,
+  i.e. when ring mode is off.]
+
+  SideEffects []
+
+  SeeAlso     [Cec_IncrMgrComputeSeeds]
+
+***********************************************************************/
+int Cec_IncrMgrCountNextChanges( Cec_IncrMgr_t * p )
+{
+    Gia_Man_t * pAig = p->pAig;
+    int i, nChanges = 0;
+    if ( pAig->pNexts == NULL )
+        return 0;
+    for ( i = 1; i < p->nObjs; i++ )
+        nChanges += Gia_ObjNext( pAig, i ) != Vec_IntEntry( p->vNextPrev, i );
+    return nChanges;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Detects whether a ring edge is new since the last snapshot.]
+
+  Description [Ring classes store list edges explicitly in pNexts, but
+  the SRM also proves the implicit closing edge tail -> head.  For an
+  explicit edge, the edge is unchanged iff the predecessor's pNexts slot
+  still names the same successor.  For the closing edge there is no
+  pNexts slot to compare, so we reconstruct whether the same tail/head
+  pair already existed in the previous snapshot: the tail must have been
+  pointing to the head (closing the ring) and the head must still have
+  been a class root.  Returns 1 to mean "must be re-proved".  Passing a
+  NULL manager or a non-ring AIG returns 0 (no edge work needed).]
+
+  SideEffects []
+
+  SeeAlso     [Cec_IncrMgrCountActivePairs]
+
+***********************************************************************/
+int Cec_IncrMgrRingEdgeChanged( Cec_IncrMgr_t * p, int iPrev, int iObj )
+{
+    Gia_Man_t * pAig;
+    int iNextCur, iNextOld;
+    if ( p == NULL )
+        return 0;
+    pAig = p->pAig;
+    if ( pAig->pNexts == NULL )
+        return 0;
+    iNextCur = Gia_ObjNext( pAig, iPrev );
+    iNextOld = Vec_IntEntry( p->vNextPrev, iPrev );
+    if ( iNextCur == iObj )
+        return iNextOld != iObj;
+    if ( iNextCur > 0 )
+        return 1; // conservative: should not happen for callers below
+    // Closing edge: prove if the previous snapshot did not already contain
+    // exactly this tail/head pair as a ring's closing edge.
+    return iNextOld > 0 ||
+           Vec_IntEntry( p->vReprPrev, iPrev ) != iObj ||
+           Vec_IntEntry( p->vReprPrev, iObj ) != GIA_VOID ||
+           Vec_IntEntry( p->vNextPrev, iObj ) <= 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts total and active candidate pairs before SRM build.]
+
+  Description [Mirrors the PO-emission loops in the active SRM builders
+  but stops before constructing the unrolled network: it walks every
+  candidate pair the SRM would emit and tallies how many would survive
+  the active filter (pTfoMark plus the ring-edge override).  The count
+  is approximate because SRM construction can still simplify a pair
+  away after the literal it represents collapses; it is used only to
+  decide whether the active filter saves enough work to be worth the
+  bookkeeping (the main loop falls back to the full SRM above ~70%
+  active pairs).  When pTfoMark is NULL every pair is counted active.]
+
+  SideEffects []
+
+  SeeAlso     [Gia_ManCorrSpecReduce_Active]
+
+***********************************************************************/
+void Cec_IncrMgrCountActivePairs( Cec_IncrMgr_t * p, int fRings, int * pTfoMark,
+                                  int * pnTotal, int * pnActive )
+{
+    Gia_Man_t * pAig = p->pAig;
+    Gia_Obj_t * pObj, * pRepr;
+    int i, iPrev, iObj;
+    *pnTotal = *pnActive = 0;
+    assert( pAig->pReprs != NULL );
+    if ( fRings )
+    {
+        Gia_ManForEachObj1( pAig, pObj, i )
+        {
+            if ( Gia_ObjIsConst( pAig, i ) )
+            {
+                (*pnTotal)++;
+                (*pnActive) += pTfoMark == NULL || pTfoMark[i];
+            }
+            else if ( Gia_ObjIsHead( pAig, i ) )
+            {
+                iPrev = i;
+                Gia_ClassForEachObj1( pAig, i, iObj )
+                {
+                    (*pnTotal)++;
+                    (*pnActive) += pTfoMark == NULL || pTfoMark[iPrev] || pTfoMark[iObj] ||
+                                   Cec_IncrMgrRingEdgeChanged( p, iPrev, iObj );
+                    iPrev = iObj;
+                }
+                iObj = i; // closing edge tail -> head
+                (*pnTotal)++;
+                (*pnActive) += pTfoMark == NULL || pTfoMark[iPrev] || pTfoMark[iObj] ||
+                               Cec_IncrMgrRingEdgeChanged( p, iPrev, iObj );
+            }
+        }
+    }
+    else
+    {
+        Gia_ManForEachObj1( pAig, pObj, i )
+        {
+            int idR;
+            pRepr = Gia_ObjReprObj( pAig, Gia_ObjId(pAig,pObj) );
+            if ( pRepr == NULL )
+                continue;
+            idR = Gia_ObjId( pAig, pRepr );
+            (*pnTotal)++;
+            (*pnActive) += pTfoMark == NULL || pTfoMark[i] || pTfoMark[idR];
+        }
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Forward TFO BFS from seeds across nFrames unrollings.]
+
+  Description [Marks pTfoMark[id]=1 for every AIG node reachable from
+  any seed within nFrames combinational+sequential steps.  Each frame
+  performs a combinational fanout BFS; RI fanouts cross to the next
+  frame by following Gia_ObjRiToRo to the corresponding register output.
+  After nFrames cross-frame jumps the search stops, since pairs deeper
+  than that cannot depend on the seeds within an nFrames-deep SRM.
+
+  RI nodes themselves are intentionally not marked: SRM emission is
+  keyed on AIG candidate nodes (ANDs and CIs) and never on COs, so
+  marking RIs would only inflate the active set without enabling any
+  additional pair.
+
+  Mark clearing is amortised: vTfoNodes records every id touched in
+  the previous round and is iterated to zero only those entries, so
+  the routine never sweeps the full N-sized array.  Cost per call is
+  O(|TFO_k| * avg_fanout).]
+
+  SideEffects []
+
+  SeeAlso     [Cec_IncrMgrComputeSeeds]
+
+***********************************************************************/
+void Cec_IncrMgrComputeTfo( Cec_IncrMgr_t * p )
+{
+    Gia_Man_t * pAig = p->pAig;
+    int * pMark = p->pTfoMark;
+    int f, i, k, Id, FanId, RoId;
+
+    Vec_IntForEachEntry( p->vTfoNodes, Id, i )
+        pMark[Id] = 0;
+    Vec_IntClear( p->vTfoNodes );
+    Vec_IntClear( p->vBfsCur );
+    Vec_IntClear( p->vBfsNext );
+
+    Vec_IntForEachEntry( p->vSeeds, Id, i )
+    {
+        if ( !pMark[Id] )
+        {
+            pMark[Id] = 1;
+            Vec_IntPush( p->vTfoNodes, Id );
+            Vec_IntPush( p->vBfsCur, Id );
+        }
+    }
+
+    for ( f = 0; f <= p->nFrames; f++ )
+    {
+        int head = 0;
+        while ( head < Vec_IntSize(p->vBfsCur) )
+        {
+            Gia_Obj_t * pFan;
+            Id = Vec_IntEntry( p->vBfsCur, head++ );
+            int nFan = Gia_ObjFanoutNumId( pAig, Id );
+            for ( k = 0; k < nFan; k++ )
+            {
+                FanId = Gia_ObjFanoutId( pAig, Id, k );
+                pFan  = Gia_ManObj( pAig, FanId );
+                if ( Gia_ObjIsRi(pAig, pFan) )
+                {
+                    if ( f < p->nFrames )
+                    {
+                        RoId = Gia_ObjRiToRoId( pAig, FanId );
+                        if ( !pMark[RoId] )
+                        {
+                            pMark[RoId] = 1;
+                            Vec_IntPush( p->vTfoNodes, RoId );
+                            Vec_IntPush( p->vBfsNext, RoId );
+                        }
+                    }
+                }
+                else if ( Gia_ObjIsCo(pFan) )
+                {
+                    // PO: not a candidate, skip
+                }
+                else
+                {
+                    if ( !pMark[FanId] )
+                    {
+                        pMark[FanId] = 1;
+                        Vec_IntPush( p->vTfoNodes, FanId );
+                        Vec_IntPush( p->vBfsCur, FanId );
+                    }
+                }
+            }
+        }
+        Vec_IntClear( p->vBfsCur );
+        Vec_IntAppend( p->vBfsCur, p->vBfsNext );
+        Vec_IntClear( p->vBfsNext );
+        if ( Vec_IntSize(p->vBfsCur) == 0 )
+            break;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Active-filter variant of Gia_ManCorrSpecReduce.]
+
+  Description [Identical to Gia_ManCorrSpecReduce in its SRM topology
+  and speculative reduction; the only difference is the PO emission
+  filter.  A candidate pair (a, b) is emitted iff pTfoMark[a] is set
+  or pTfoMark[b] is set, i.e. at least one endpoint lies in the TFO of
+  a recently-changed representative.  In ring mode, a ring edge that is
+  new or rewired since the last snapshot (Cec_IncrMgrRingEdgeChanged)
+  is also emitted even if neither endpoint is in the TFO -- the edge
+  has no prior UNSAT result to reuse and must be reproved on its own.
+
+  Walking the full ring is required (rather than skipping unmarked
+  members) so iPrev stays aligned with the live class order; the active
+  filter only suppresses the resulting PO when the edge is provably
+  not new and neither endpoint is reachable from a seed.  Passing
+  pTfoMark == NULL falls back to the unfiltered baseline behaviour.]
+
+  SideEffects []
+
+  SeeAlso     [Gia_ManCorrSpecReduce]
+
+***********************************************************************/
+Gia_Man_t * Gia_ManCorrSpecReduce_Active( Gia_Man_t * p, int nFrames, int fScorr,
+                                          Vec_Int_t ** pvOutputs, int fRings,
+                                          int * pTfoMark, Cec_IncrMgr_t * pIncr )
+{
+    Gia_Man_t * pNew, * pTemp;
+    Gia_Obj_t * pObj, * pRepr;
+    Vec_Int_t * vXorLits;
+    int f, i, iPrev, iObj, iPrevNew, iObjNew;
+    assert( nFrames > 0 );
+    assert( Gia_ManRegNum(p) > 0 );
+    assert( p->pReprs != NULL );
+    Vec_IntFill( &p->vCopies, (nFrames+fScorr)*Gia_ManObjNum(p), -1 );
+    Gia_ManSetPhase( p );
+    pNew = Gia_ManStart( nFrames * Gia_ManObjNum(p) );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    Gia_ManHashAlloc( pNew );
+    Gia_ObjSetCopyF( p, 0, Gia_ManConst0(p), 0 );
+    Gia_ManForEachRo( p, pObj, i )
+        Gia_ObjSetCopyF( p, 0, pObj, Gia_ManAppendCi(pNew) );
+    Gia_ManForEachRo( p, pObj, i )
+        if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
+            Gia_ObjSetCopyF( p, 0, pObj, Gia_ObjCopyF(p, 0, pRepr) );
+    for ( f = 0; f < nFrames+fScorr; f++ )
+    {
+        Gia_ObjSetCopyF( p, f, Gia_ManConst0(p), 0 );
+        Gia_ManForEachPi( p, pObj, i )
+            Gia_ObjSetCopyF( p, f, pObj, Gia_ManAppendCi(pNew) );
+    }
+    *pvOutputs = Vec_IntAlloc( 1000 );
+    vXorLits = Vec_IntAlloc( 1000 );
+    if ( fRings )
+    {
+        Gia_ManForEachObj1( p, pObj, i )
+        {
+            if ( Gia_ObjIsConst( p, i ) )
+            {
+                if ( pTfoMark && !pTfoMark[i] )
+                    continue;
+                iObjNew = Gia_ManCorrSpecReal( pNew, p, pObj, nFrames, 0 );
+                iObjNew = Abc_LitNotCond( iObjNew, Gia_ObjPhase(pObj) );
+                if ( iObjNew != 0 )
+                {
+                    Vec_IntPush( *pvOutputs, 0 );
+                    Vec_IntPush( *pvOutputs, i );
+                    Vec_IntPush( vXorLits, iObjNew );
+                }
+            }
+            else if ( Gia_ObjIsHead( p, i ) )
+            {
+                // Walk every ring edge so iPrev stays aligned with the class
+                // order; emit only when an endpoint is in TFO or the edge is
+                // new/rewired since the last snapshot.
+                iPrev = i;
+                Gia_ClassForEachObj1( p, i, iObj )
+                {
+                    int fEmit = (pTfoMark == NULL) || pTfoMark[iPrev] || pTfoMark[iObj] ||
+                                Cec_IncrMgrRingEdgeChanged( pIncr, iPrev, iObj );
+                    if ( fEmit )
+                    {
+                        iPrevNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iPrev), nFrames, 0 );
+                        iObjNew  = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iObj), nFrames, 0 );
+                        iPrevNew = Abc_LitNotCond( iPrevNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iPrev)) );
+                        iObjNew  = Abc_LitNotCond( iObjNew,  Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iObj)) );
+                        if ( iPrevNew != iObjNew && iPrevNew != 0 && iObjNew != 1 )
+                        {
+                            Vec_IntPush( *pvOutputs, iPrev );
+                            Vec_IntPush( *pvOutputs, iObj );
+                            Vec_IntPush( vXorLits, Gia_ManHashAnd(pNew, iPrevNew, Abc_LitNot(iObjNew)) );
+                        }
+                    }
+                    iPrev = iObj;
+                }
+                // Closing edge tail -> head
+                iObj = i;
+                {
+                    int fEmit = (pTfoMark == NULL) || pTfoMark[iPrev] || pTfoMark[iObj] ||
+                                Cec_IncrMgrRingEdgeChanged( pIncr, iPrev, iObj );
+                    if ( fEmit )
+                    {
+                        iPrevNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iPrev), nFrames, 0 );
+                        iObjNew  = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iObj), nFrames, 0 );
+                        iPrevNew = Abc_LitNotCond( iPrevNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iPrev)) );
+                        iObjNew  = Abc_LitNotCond( iObjNew,  Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iObj)) );
+                        if ( iPrevNew != iObjNew && iPrevNew != 0 && iObjNew != 1 )
+                        {
+                            Vec_IntPush( *pvOutputs, iPrev );
+                            Vec_IntPush( *pvOutputs, iObj );
+                            Vec_IntPush( vXorLits, Gia_ManHashAnd(pNew, iPrevNew, Abc_LitNot(iObjNew)) );
+                        }
+                    }
+                }
+            }
+        }
+    }
+    else
+    {
+        Gia_ManForEachObj1( p, pObj, i )
+        {
+            pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
+            if ( pRepr == NULL )
+                continue;
+            if ( pTfoMark )
+            {
+                int idR = Gia_ObjId(p, pRepr);
+                if ( !pTfoMark[i] && !pTfoMark[idR] )
+                    continue;
+            }
+            iPrevNew = Gia_ObjIsConst(p, i)? 0 : Gia_ManCorrSpecReal( pNew, p, pRepr, nFrames, 0 );
+            iObjNew  = Gia_ManCorrSpecReal( pNew, p, pObj, nFrames, 0 );
+            iObjNew  = Abc_LitNotCond( iObjNew, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
+            if ( iPrevNew != iObjNew )
+            {
+                Vec_IntPush( *pvOutputs, Gia_ObjId(p, pRepr) );
+                Vec_IntPush( *pvOutputs, Gia_ObjId(p, pObj) );
+                Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, iPrevNew, iObjNew) );
+            }
+        }
+    }
+    Vec_IntForEachEntry( vXorLits, iObjNew, i )
+        Gia_ManAppendCo( pNew, iObjNew );
+    Vec_IntFree( vXorLits );
+    Gia_ManHashStop( pNew );
+    Vec_IntErase( &p->vCopies );
+    pNew = Gia_ManCleanup( pTemp = pNew );
+    Gia_ManStop( pTemp );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Active-filter variant of Gia_ManCorrSpecReduceInit (BMC SRM).]
+
+  Description [Mirrors Gia_ManCorrSpecReduceInit but emits a candidate
+  PO (pRepr, pObj) only when at least one of the two endpoints lies in
+  pTfoMark.  The baseline BMC SRM accepts an fRings flag for symmetry
+  with the inductive builder but never inspects it -- its topology is
+  always (head, member) pairs derived from pReprs alone, with no ring
+  edges to close.  Therefore this active variant only needs pReprs-
+  driven seeds: pNexts changes cannot affect this SRM and there is no
+  closing edge to reprove.  Passing pTfoMark == NULL falls back to the
+  unfiltered baseline behaviour.]
+
+  SideEffects []
+
+  SeeAlso     [Gia_ManCorrSpecReduceInit]
+
+***********************************************************************/
+Gia_Man_t * Gia_ManCorrSpecReduceInit_Active( Gia_Man_t * p, int nFrames, int nPrefix, int fScorr,
+                                              Vec_Int_t ** pvOutputs, int * pTfoMark )
+{
+    Gia_Man_t * pNew, * pTemp;
+    Gia_Obj_t * pObj, * pRepr;
+    Vec_Int_t * vXorLits;
+    int f, i, iPrevNew, iObjNew;
+    assert( (!fScorr && nFrames > 1) || (fScorr && nFrames > 0) || nPrefix );
+    assert( Gia_ManRegNum(p) > 0 );
+    assert( p->pReprs != NULL );
+    Vec_IntFill( &p->vCopies, (nFrames+nPrefix+fScorr)*Gia_ManObjNum(p), -1 );
+    Gia_ManSetPhase( p );
+    pNew = Gia_ManStart( (nFrames+nPrefix) * Gia_ManObjNum(p) );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    Gia_ManHashAlloc( pNew );
+    Gia_ManForEachRo( p, pObj, i )
+    {
+        Gia_ManAppendCi(pNew);
+        Gia_ObjSetCopyF( p, 0, pObj, 0 );
+    }
+    for ( f = 0; f < nFrames+nPrefix+fScorr; f++ )
+    {
+        Gia_ObjSetCopyF( p, f, Gia_ManConst0(p), 0 );
+        Gia_ManForEachPi( p, pObj, i )
+            Gia_ObjSetCopyF( p, f, pObj, Gia_ManAppendCi(pNew) );
+    }
+    *pvOutputs = Vec_IntAlloc( 1000 );
+    vXorLits = Vec_IntAlloc( 1000 );
+    for ( f = nPrefix; f < nFrames+nPrefix; f++ )
+    {
+        Gia_ManForEachObj1( p, pObj, i )
+        {
+            pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
+            if ( pRepr == NULL )
+                continue;
+            if ( pTfoMark )
+            {
+                int idR = Gia_ObjId(p, pRepr);
+                if ( !pTfoMark[i] && !pTfoMark[idR] )
+                    continue;
+            }
+            iPrevNew = Gia_ObjIsConst(p, i)? 0 : Gia_ManCorrSpecReal( pNew, p, pRepr, f, nPrefix );
+            iObjNew  = Gia_ManCorrSpecReal( pNew, p, pObj, f, nPrefix );
+            iObjNew  = Abc_LitNotCond( iObjNew, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
+            if ( iPrevNew != iObjNew )
+            {
+                Vec_IntPush( *pvOutputs, Gia_ObjId(p, pRepr) );
+                Vec_IntPush( *pvOutputs, Gia_ObjId(p, pObj) );
+                Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, iPrevNew, iObjNew) );
+            }
+        }
+    }
+    Vec_IntForEachEntry( vXorLits, iObjNew, i )
+        Gia_ManAppendCo( pNew, iObjNew );
+    Vec_IntFree( vXorLits );
+    Gia_ManHashStop( pNew );
+    Vec_IntErase( &p->vCopies );
+    pNew = Gia_ManCleanup( pTemp = pNew );
+    Gia_ManStop( pTemp );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [One-shot incremental decision for the refinement loop.]
+
+  Description [Computes seeds, runs the TFO BFS, counts active candidate
+  pairs, and applies the fallback heuristic.  Returns the TFO mask to
+  pass to the active SRM builder, or NULL when either (a) classes have
+  converged since the last snapshot (in which case *pfConverged is set
+  to 1 and the caller should break the refinement loop), or (b) the
+  active-pair ratio is high enough that the full SRM is cheaper.  The
+  out parameters pnReprSeeds / pnNextChanges / pnTotalPairs /
+  pnActivePairs are filled when non-NULL and are useful for verbose
+  printing and progress counters.  fUseRings tells the helper whether
+  to track pNexts changes; the BMC SRM is non-ring and passes 0.]
+
+  SideEffects []
+
+  SeeAlso     [Cec_IncrMgrComputeSeeds Cec_IncrMgrComputeTfo
+               Cec_IncrMgrCountActivePairs]
+
+***********************************************************************/
+int * Cec_IncrMgrDecideMask( Cec_IncrMgr_t * p, int fUseRings, int * pfConverged,
+                             int * pnReprSeeds, int * pnNextChanges,
+                             int * pnTotalPairs, int * pnActivePairs )
+{
+    int nReprSeeds, nNextChanges = 0, nTotalPairs = 0, nActivePairs = 0;
+    *pfConverged = 0;
+    nReprSeeds = Cec_IncrMgrComputeSeeds( p );
+    if ( fUseRings )
+        nNextChanges = Cec_IncrMgrCountNextChanges( p );
+    if ( pnReprSeeds )   *pnReprSeeds   = nReprSeeds;
+    if ( pnNextChanges ) *pnNextChanges = nNextChanges;
+    if ( nReprSeeds == 0 && nNextChanges == 0 )
+    {
+        *pfConverged = 1;
+        return NULL;
+    }
+    Cec_IncrMgrComputeTfo( p );
+    Cec_IncrMgrCountActivePairs( p, fUseRings, p->pTfoMark, &nTotalPairs, &nActivePairs );
+    if ( pnTotalPairs )  *pnTotalPairs  = nTotalPairs;
+    if ( pnActivePairs ) *pnActivePairs = nActivePairs;
+    if ( nActivePairs == 0 )
+    {
+        *pfConverged = 1;
+        return NULL;
+    }
+    // Above ~70% active pairs, the mask plus emission filter costs more
+    // than just rebuilding the full SRM.  Return NULL to signal fallback.
+    if ( nTotalPairs > 0 && (ABC_INT64_T)10 * nActivePairs > (ABC_INT64_T)7 * nTotalPairs )
+        return NULL;
+    return p->pTfoMark;
+}
+
+ABC_NAMESPACE_IMPL_END
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////

src/proof/cec/cecInt.h

@@ -149,7 +149,7 @@ struct Cec_ManFra_t_
 {
     // parameters
     Gia_Man_t *      pAig;           // the AIG to be used for simulation
-    Cec_ParFra_t *   pPars;          // SAT sweeping parameters 
+    Cec_ParFra_t *   pPars;          // SAT sweeping parameters
     // simulation patterns
     Vec_Int_t *      vXorNodes;      // nodes used in speculative reduction
     int              nAllProved;     // total number of proved nodes
@@ -165,6 +165,23 @@ struct Cec_ManFra_t_
     abctime          timeTotal;      // total runtime
 };
 
+// incremental active-list manager for &scorr -i
+typedef struct Cec_IncrMgr_t_ Cec_IncrMgr_t;
+struct Cec_IncrMgr_t_
+{
+    Gia_Man_t *  pAig;            // host AIG (immutable across iterations)
+    int          nFrames;         // unrolling depth used by the SRM builder
+    int          nObjs;           // cached Gia_ManObjNum(pAig)
+    Vec_Int_t *  vReprPrev;       // snapshot of pReprs from previous round
+    Vec_Int_t *  vNextPrev;       // snapshot of pNexts from previous round
+    Vec_Int_t *  vSeeds;          // nodes whose pReprs changed since snapshot
+    Vec_Int_t *  vTfoNodes;       // ids currently in TFO (for fast clearing)
+    int *        pTfoMark;        // dense mark array, size = nObjs
+    Vec_Int_t *  vBfsCur;         // BFS frontier for current frame
+    Vec_Int_t *  vBfsNext;        // BFS frontier carried to next frame
+    int          fOwnsFanout;     // 1 if we built static fanout (must free)
+};
+
 ////////////////////////////////////////////////////////////////////////
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
@@ -175,6 +192,20 @@ struct Cec_ManFra_t_
 
 /*=== cecCorr.c ============================================================*/
 extern void                 Cec_ManRefinedClassPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIter, abctime Time );
+extern int                  Gia_ManCorrSpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix );
+extern void                 Gia_ManCorrSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix );
+/*=== cecCorrIncr.c ============================================================*/
+extern Cec_IncrMgr_t *      Cec_IncrMgrAlloc( Gia_Man_t * pAig, int nFrames );
+extern void                 Cec_IncrMgrFree( Cec_IncrMgr_t * p );
+extern void                 Cec_IncrMgrSnapshotClasses( Cec_IncrMgr_t * p );
+extern int                  Cec_IncrMgrComputeSeeds( Cec_IncrMgr_t * p );
+extern int                  Cec_IncrMgrCountNextChanges( Cec_IncrMgr_t * p );
+extern int                  Cec_IncrMgrRingEdgeChanged( Cec_IncrMgr_t * p, int iPrev, int iObj );
+extern void                 Cec_IncrMgrCountActivePairs( Cec_IncrMgr_t * p, int fRings, int * pTfoMark, int * pnTotal, int * pnActive );
+extern void                 Cec_IncrMgrComputeTfo( Cec_IncrMgr_t * p );
+extern Gia_Man_t *          Gia_ManCorrSpecReduce_Active( Gia_Man_t * p, int nFrames, int fScorr, Vec_Int_t ** pvOutputs, int fRings, int * pTfoMark, Cec_IncrMgr_t * pIncr );
+extern Gia_Man_t *          Gia_ManCorrSpecReduceInit_Active( Gia_Man_t * p, int nFrames, int nPrefix, int fScorr, Vec_Int_t ** pvOutputs, int * pTfoMark );
+extern int *                Cec_IncrMgrDecideMask( Cec_IncrMgr_t * p, int fUseRings, int * pfConverged, int * pnReprSeeds, int * pnNextChanges, int * pnTotalPairs, int * pnActivePairs );
 /*=== cecClass.c ============================================================*/
 extern int                  Cec_ManSimClassRemoveOne( Cec_ManSim_t * p, int i );
 extern int                  Cec_ManSimClassesPrepare( Cec_ManSim_t * p, int LevelMax );

src/proof/cec/cecProve.c

@@ -62,16 +62,16 @@ static int Cec_SProveCallback( void * pUser, int fSolved, unsigned Result );
 static Gia_Man_t * Cec_GiaScorrOld( Gia_Man_t * p, int nTimeOut, Par_Share_t * pShare, struct Cec_ScorrStop_t_ * pStopOut );
 static Gia_Man_t * Cec_GiaScorrNew( Gia_Man_t * p, int nTimeOut, Par_Share_t * pShare, struct Cec_ScorrStop_t_ * pStopOut );
 #ifdef ABC_USE_PTHREADS
-static void Cec_GiaInitThreads( Par_ThData_t * ThData, int nWorkers, Gia_Man_t * p, int nTimeOut, int nTimeOutU, Wlc_Ntk_t * pWlc, int fVerbose, pthread_t * WorkerThread, Par_Share_t * pShare, int * pEngines, int StageId, int NetId, struct Cec_SproveTrace_t_ * pTrace );
+static void Cec_GiaInitThreads( Par_ThData_t * ThData, int nWorkers, Gia_Man_t * p, int nTimeOut, int nTimeOutU, Wlc_Ntk_t * pWlc, const char * pUfarArgs, int fVerbose, pthread_t * WorkerThread, Par_Share_t * pShare, int * pEngines, int StageId, int NetId, struct Cec_SproveTrace_t_ * pTrace );
 static void Cec_GiaStopThreads( Par_ThData_t * ThData, pthread_t * WorkerThread, int nWorkers );
 #endif
 static int Cec_GiaWaitThreads( Par_ThData_t * ThData, int nWorkers, Gia_Man_t * p, int RetValue, int * pRetEngine );
 
-extern int Ufar_ProveWithTimeout( Wlc_Ntk_t * pNtk, int nTimeOut, int fVerbose, int (*pFuncStop)(int), int RunId );
+extern int Ufar_ProveWithTimeout( Wlc_Ntk_t * pNtk, int nTimeOut, int fVerbose, int (*pFuncStop)(int), int RunId, const char * pArgs );
 
 #ifndef ABC_USE_PTHREADS
 
-int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, int nTimeOut3, int fUseUif, Wlc_Ntk_t * pWlc, int fVerbose, int fVeryVerbose, int fSilent, char * pReplayFile ) { return -1; }
+int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, int nTimeOut3, int fUseUif, Wlc_Ntk_t * pWlc, int fVerbose, int fVeryVerbose, int fSilent, char * pReplayFile, char * pUfarArgs ) { return -1; }
 int Cec_GiaReplayReadParams( char * pFileName, int * pnProcs, int * pnTimeOut, int * pnTimeOut2, int * pnTimeOut3, int * pfUseUif ) { return 0; }
 int Cec_GiaReplayTest( Gia_Man_t * p, Wlc_Ntk_t * pWlc, char * pFileName, int fVerbose, int fVeryVerbose, int fSilent ) { return -1; }
 
@@ -106,6 +106,7 @@ typedef struct Par_ThData_t_
     int         fVerbose;
     int         nTimeOutU;
     Wlc_Ntk_t * pWlc;
+    const char * pUfarArgs;
     int         WorkerId;
     int         StageId;
     int         NetId;
@@ -154,6 +155,9 @@ struct Cec_SprovePlan_t_
     int nTimeOut2;
     int nTimeOut3;
     int fUseUif;
+    int fPersistentUif;
+    int nTimeOutUif;
+    char * pUfarArgs;
     int nStages;
     Cec_SproveStage_t Stages[SPROVE_STAGE_MAX];
 };
@@ -307,13 +311,41 @@ static int Cec_SproveParseEngineName( const char * pName )
             return i;
     return -1;
 }
-static void Cec_SproveDeriveEngineList( int nProcs, int fUseUif, int * pEngines, int * pnEngines )
+static int Cec_SprovePlanTimeoutTotal( Cec_SprovePlan_t * pPlan )
 {
-    int i, nEngines = nProcs + (fUseUif ? 1 : 0);
+    int i, Total = 0;
+    for ( i = 0; i < pPlan->nStages; i++ )
+    {
+        Cec_SproveStage_t * pStage = &pPlan->Stages[i];
+        int RoundTime = pStage->fHasRound ? pStage->RoundTimeout : 0;
+        int ReduceTime = pStage->fHasReduce ? pStage->ReduceTimeout : 0;
+        Total += Abc_MaxInt( RoundTime, ReduceTime );
+    }
+    return Total;
+}
+static void Cec_SproveDeriveEngineList( int nProcs, int fUseUif, int fPersistentUif, int * pEngines, int * pnEngines )
+{
+    int i, nEngines = nProcs + ((fUseUif && !fPersistentUif) ? 1 : 0);
     assert( nEngines >= 1 && nEngines <= PAR_THR_MAX );
+    if ( fUseUif && nProcs == 6 )
+    {
+        if ( fPersistentUif )
+        {
+            int UifEngines[6] = { 0, 1, 2, 3, 4, PAR_ENGINE_GLA };
+            memcpy( pEngines, UifEngines, sizeof(UifEngines) );
+            *pnEngines = 6;
+        }
+        else
+        {
+            int UifEngines[7] = { 0, 1, 2, 3, 4, PAR_ENGINE_GLA, PAR_ENGINE_UFAR };
+            memcpy( pEngines, UifEngines, sizeof(UifEngines) );
+            *pnEngines = 7;
+        }
+        return;
+    }
     for ( i = 0; i < nEngines; i++ )
     {
-        if ( fUseUif && i == nEngines - 1 )
+        if ( fUseUif && !fPersistentUif && i == nEngines - 1 )
             pEngines[i] = PAR_ENGINE_UFAR;
         else if ( !fUseUif && nEngines == 6 && i == 5 )
             pEngines[i] = PAR_ENGINE_GLA;
@@ -322,7 +354,25 @@ static void Cec_SproveDeriveEngineList( int nProcs, int fUseUif, int * pEngines,
     }
     *pnEngines = nEngines;
 }
-static void Cec_SprovePlanDefault( Cec_SprovePlan_t * pPlan, int nProcs, int nTimeOut, int nTimeOut2, int nTimeOut3, int fUseUif )
+static void Cec_SproveTrimLineEnd( char * pLine )
+{
+    int nSize = strlen( pLine );
+    while ( nSize > 0 && (pLine[nSize - 1] == '\n' || pLine[nSize - 1] == '\r') )
+        pLine[--nSize] = 0;
+}
+static void Cec_SprovePlanSetUfarArgs( Cec_SprovePlan_t * pPlan, const char * pUfarArgs )
+{
+    ABC_FREE( pPlan->pUfarArgs );
+    pPlan->pUfarArgs = NULL;
+    if ( pUfarArgs && pUfarArgs[0] )
+        pPlan->pUfarArgs = Abc_UtilStrsav( (char *)pUfarArgs );
+}
+static void Cec_SprovePlanFree( Cec_SprovePlan_t * pPlan )
+{
+    ABC_FREE( pPlan->pUfarArgs );
+    pPlan->pUfarArgs = NULL;
+}
+static void Cec_SprovePlanDefault( Cec_SprovePlan_t * pPlan, int nProcs, int nTimeOut, int nTimeOut2, int nTimeOut3, int fUseUif, const char * pUfarArgs )
 {
     int nEngines;
     memset( pPlan, 0, sizeof(Cec_SprovePlan_t) );
@@ -336,8 +386,10 @@ static void Cec_SprovePlanDefault( Cec_SprovePlan_t * pPlan, int nProcs, int nTi
     pPlan->nTimeOut2 = nTimeOut2;
     pPlan->nTimeOut3 = nTimeOut3;
     pPlan->fUseUif = fUseUif;
+    pPlan->fPersistentUif = fUseUif ? 1 : 0;
+    Cec_SprovePlanSetUfarArgs( pPlan, pUfarArgs );
     pPlan->nStages = 4;
-    Cec_SproveDeriveEngineList( nProcs, fUseUif, pPlan->Stages[0].RoundEngines, &nEngines );
+    Cec_SproveDeriveEngineList( nProcs, fUseUif, pPlan->fPersistentUif, pPlan->Stages[0].RoundEngines, &nEngines );
 
     pPlan->Stages[0].Id = 1;
     pPlan->Stages[0].fHasRound = 1;
@@ -376,6 +428,7 @@ static void Cec_SprovePlanDefault( Cec_SprovePlan_t * pPlan, int nProcs, int nTi
     pPlan->Stages[3].RoundTimeout = nTimeOut3;
     pPlan->Stages[3].nRoundEngines = nEngines;
     memcpy( pPlan->Stages[3].RoundEngines, pPlan->Stages[0].RoundEngines, sizeof(int) * nEngines );
+    pPlan->nTimeOutUif = pPlan->fPersistentUif ? Cec_SprovePlanTimeoutTotal( pPlan ) : 0;
 }
 static void Cec_SproveTraceWrite( Cec_SproveTrace_t * pTrace, const char * pFormat, ... )
 {
@@ -410,6 +463,10 @@ static void Cec_SproveTraceOpen( Cec_SproveTrace_t * pTrace, Gia_Man_t * p, Cec_
     Cec_SproveTraceWrite( pTrace, "SPROVE_REPLAY 1" );
     Cec_SproveTraceWrite( pTrace, "CASE %s", pProbName ? pProbName : "(none)" );
     Cec_SproveTraceWrite( pTrace, "PARAMS P=%d T=%d U=%d W=%d UIF=%d", pPlan->nProcs, pPlan->nTimeOut, pPlan->nTimeOut2, pPlan->nTimeOut3, pPlan->fUseUif );
+    if ( pPlan->fUseUif )
+        Cec_SproveTraceWrite( pTrace, "UFAR mode=%s timeout=%d", pPlan->fPersistentUif ? "persistent" : "round", pPlan->nTimeOutUif );
+    if ( pPlan->pUfarArgs && pPlan->pUfarArgs[0] )
+        Cec_SproveTraceWrite( pTrace, "UFAR_ARGS %s", pPlan->pUfarArgs );
     Cec_SproveTraceWrite( pTrace, "" );
     Cec_SproveTraceWrite( pTrace, "PLAN_BEGIN" );
     for ( i = 0; i < pPlan->nStages; i++ )
@@ -481,12 +538,29 @@ static int Cec_SproveReplayReadParamsInt( char * pFileName, Cec_SprovePlan_t * p
             pPlan->nTimeOut3 = atoi(Value);
             if ( !Cec_SproveFindValue(Buffer, "UIF=", Value, sizeof(Value)) ) break;
             pPlan->fUseUif = atoi(Value);
+        }
+        else if ( strncmp(Buffer, "UFAR_ARGS ", 10) == 0 )
+        {
+            Cec_SproveTrimLineEnd( Buffer );
+            Cec_SprovePlanSetUfarArgs( pPlan, Buffer + 10 );
+        }
+        else if ( strncmp(Buffer, "UFAR ", 5) == 0 )
+        {
+            if ( Cec_SproveFindValue(Buffer, "mode=", Value, sizeof(Value)) )
+                pPlan->fPersistentUif = !strcmp(Value, "persistent");
+            if ( Cec_SproveFindValue(Buffer, "timeout=", Value, sizeof(Value)) )
+                pPlan->nTimeOutUif = atoi(Value);
+        }
+        else if ( pPlan->nProcs > 0 && (strncmp(Buffer, "PLAN_BEGIN", 10) == 0 || strncmp(Buffer, "OBSERVED_BEGIN", 14) == 0) )
+        {
+            if ( pPlan->fUseUif && pPlan->nTimeOutUif == 0 )
+                pPlan->nTimeOutUif = pPlan->fPersistentUif ? (pPlan->nTimeOut + pPlan->nTimeOut2 + 2 * pPlan->nTimeOut3) : 0;
             fclose( pFile );
             return 1;
         }
     }
     fclose( pFile );
-    return 0;
+    return pPlan->nProcs > 0;
 }
 static int Cec_SproveReplayReadPlan( char * pFileName, Cec_SprovePlan_t * pPlan )
 {
@@ -678,20 +752,35 @@ static Gia_Man_t * Cec_SproveRunReduce( Gia_Man_t * pInput, Cec_SproveStage_t *
     }
     return pOutput;
 }
+static void Cec_SproveTakeSharedResult( Par_Share_t * pShare, int * pRetValue, int * pRetEngine )
+{
+    if ( pShare == NULL || pRetValue == NULL || pRetEngine == NULL )
+        return;
+    if ( *pRetValue == -1 && pShare->fSolved )
+    {
+        *pRetValue = (int)pShare->Result;
+        *pRetEngine = pShare->iEngine;
+    }
+}
 static int Cec_SproveExecutePlan( Gia_Man_t * p, Cec_SprovePlan_t * pPlan, Wlc_Ntk_t * pWlc, int fVerbose, int fVeryVerbose, int fSilent, char * pReplayFile )
 {
     abctime clkTotal = Abc_Clock(), clkStage = 0;
     Par_ThData_t ThData[PAR_THR_MAX];
     pthread_t WorkerThread[PAR_THR_MAX];
+    Par_ThData_t UifData[1];
+    pthread_t UifThread[1];
     Par_Share_t Share;
     Cec_SproveTrace_t Trace;
     Gia_Man_t * pScorr = NULL, * pScorr2 = NULL;
-    int i, RetValue = -1, RetEngine = -1, fThreadsStarted = 0;
+    int UifEngines[1] = { PAR_ENGINE_UFAR };
+    int i, RetValue = -1, RetEngine = -1, fThreadsStarted = 0, fUifStarted = 0;
     (void)fVeryVerbose;
     memset( &Share, 0, sizeof(Par_Share_t) );
     memset( &Trace, 0, sizeof(Cec_SproveTrace_t) );
     memset( ThData, 0, sizeof(ThData) );
     memset( WorkerThread, 0, sizeof(WorkerThread) );
+    memset( UifData, 0, sizeof(UifData) );
+    memset( UifThread, 0, sizeof(UifThread) );
     Abc_CexFreeP( &p->pCexComb );
     Abc_CexFreeP( &p->pCexSeq );
     if ( !fSilent && fVerbose )
@@ -700,10 +789,19 @@ static int Cec_SproveExecutePlan( Gia_Man_t * p, Cec_SprovePlan_t * pPlan, Wlc_N
         printf( "Processes = %d   TimeOut = %d sec   Verbose = %d.\n", pPlan->nProcs, pPlan->nTimeOut, fVerbose );
     fflush( stdout );
     Cec_SproveTraceOpen( &Trace, p, pPlan, pReplayFile );
+    if ( pPlan->fUseUif && pPlan->fPersistentUif && pWlc != NULL )
+    {
+        Cec_SproveTraceWrite( &Trace, "START kind=ufar mode=persistent timeout=%d t=%llu",
+            pPlan->nTimeOutUif, Cec_SproveClockToMs( Cec_SproveTraceTime(&Trace) ) );
+        Cec_GiaInitThreads( UifData, 1, p, pPlan->nTimeOutUif, pPlan->nTimeOutUif, pWlc, pPlan->pUfarArgs, fVerbose,
+            UifThread, &Share, UifEngines, 0, SPROVE_NET_ORIG, &Trace );
+        fUifStarted = 1;
+    }
     for ( i = 0; i < pPlan->nStages; i++ )
     {
         Cec_SproveStage_t * pStage = &pPlan->Stages[i];
         Gia_Man_t * pRoundNet = NULL, * pReduceNet = NULL, * pReduceOut = NULL;
+        Cec_SproveTakeSharedResult( &Share, &RetValue, &RetEngine );
         if ( !Cec_SproveCheckGuard( pStage, RetValue, p, pScorr, pScorr2 ) )
         {
             Cec_SproveTraceWrite( &Trace, "SKIP stage=%d reason=guard", pStage->Id );
@@ -719,7 +817,7 @@ static int Cec_SproveExecutePlan( Gia_Man_t * p, Cec_SprovePlan_t * pPlan, Wlc_N
             }
             Cec_SproveTraceWrite( &Trace, "START kind=round stage=%d net=%s timeout=%d t=%llu",
                 pStage->Id, Cec_SproveNetName(pStage->RoundNet), pStage->RoundTimeout, Cec_SproveClockToMs( Cec_SproveTraceTime(&Trace) ) );
-            Cec_GiaInitThreads( ThData, pStage->nRoundEngines, pRoundNet, pStage->RoundTimeout, pPlan->nTimeOut3, pWlc, fVerbose,
+            Cec_GiaInitThreads( ThData, pStage->nRoundEngines, pRoundNet, pStage->RoundTimeout, pStage->RoundTimeout, pWlc, pPlan->pUfarArgs, fVerbose,
                 fThreadsStarted ? NULL : WorkerThread, &Share, pStage->RoundEngines, pStage->Id, pStage->RoundNet, &Trace );
             fThreadsStarted = 1;
         }
@@ -732,11 +830,13 @@ static int Cec_SproveExecutePlan( Gia_Man_t * p, Cec_SprovePlan_t * pPlan, Wlc_N
             {
                 pReduceOut = Cec_SproveRunReduce( pReduceNet, pStage, &Share, &Trace, &clkStage, &RetValue, &RetEngine );
                 Cec_SproveSetNet( pStage->ReduceNetOut, &pScorr, &pScorr2, pReduceOut );
+                Cec_SproveTakeSharedResult( &Share, &RetValue, &RetEngine );
             }
         }
         if ( pStage->fHasRound )
         {
             RetValue = Cec_GiaWaitThreads( ThData, pStage->nRoundEngines, p, RetValue, &RetEngine );
+            Cec_SproveTakeSharedResult( &Share, &RetValue, &RetEngine );
             Cec_SproveTraceWrite( &Trace, "STOP kind=round stage=%d net=%s result=%s winner=%s t=%llu",
                 pStage->Id, Cec_SproveNetName(pStage->RoundNet), Cec_SproveResultName(RetValue),
                 RetEngine >= 0 ? Cec_SolveEngineName(RetEngine) : "none", Cec_SproveClockToMs( Cec_SproveTraceTime(&Trace) ) );
@@ -752,8 +852,18 @@ static int Cec_SproveExecutePlan( Gia_Man_t * p, Cec_SprovePlan_t * pPlan, Wlc_N
             }
         }
     }
+    if ( fUifStarted )
+    {
+        RetValue = Cec_GiaWaitThreads( UifData, 1, p, RetValue, &RetEngine );
+        Cec_SproveTakeSharedResult( &Share, &RetValue, &RetEngine );
+        Cec_SproveTraceWrite( &Trace, "STOP kind=ufar mode=persistent result=%s winner=%s t=%llu",
+            Cec_SproveResultName(RetValue), RetEngine == PAR_ENGINE_UFAR ? "ufar" : "other",
+            Cec_SproveClockToMs( Cec_SproveTraceTime(&Trace) ) );
+    }
     if ( fThreadsStarted )
-        Cec_GiaStopThreads( ThData, WorkerThread, pPlan->Stages[0].nRoundEngines > 0 ? pPlan->Stages[0].nRoundEngines : pPlan->nProcs + (pPlan->fUseUif ? 1 : 0) );
+        Cec_GiaStopThreads( ThData, WorkerThread, pPlan->Stages[0].nRoundEngines );
+    if ( fUifStarted )
+        Cec_GiaStopThreads( UifData, UifThread, 1 );
     Gia_ManStopP( &pScorr2 );
     Gia_ManStopP( &pScorr );
     if ( !fSilent )
@@ -920,7 +1030,7 @@ int Cec_GiaProveOne( Gia_Man_t * p, int iEngine, int nTimeOut, int fVerbose, Par
         if ( pThData && pThData->pWlc )
         {
             g_pUfarShare = pThData->pShare;
-            RetValue = Ufar_ProveWithTimeout( pThData->pWlc, pThData->nTimeOutU, fVerbose, Cec_SProveStopUfar, 0 );
+            RetValue = Ufar_ProveWithTimeout( pThData->pWlc, pThData->nTimeOutU, fVerbose, Cec_SProveStopUfar, 0, pThData->pUfarArgs );
             g_pUfarShare = NULL;
         }
     }
@@ -1072,7 +1182,7 @@ static void Cec_GiaStartThreads( Par_ThData_t * ThData, int nWorkers )
         assert( status == 0 );
     }
 }
-static void Cec_GiaInitThreads( Par_ThData_t * ThData, int nWorkers, Gia_Man_t * p, int nTimeOut, int nTimeOutU, Wlc_Ntk_t * pWlc, int fVerbose, pthread_t * WorkerThread, Par_Share_t * pShare, int * pEngines, int StageId, int NetId, Cec_SproveTrace_t * pTrace )
+static void Cec_GiaInitThreads( Par_ThData_t * ThData, int nWorkers, Gia_Man_t * p, int nTimeOut, int nTimeOutU, Wlc_Ntk_t * pWlc, const char * pUfarArgs, int fVerbose, pthread_t * WorkerThread, Par_Share_t * pShare, int * pEngines, int StageId, int NetId, Cec_SproveTrace_t * pTrace )
 {
     int i, status;
     assert( nWorkers <= PAR_THR_MAX );
@@ -1090,6 +1200,7 @@ static void Cec_GiaInitThreads( Par_ThData_t * ThData, int nWorkers, Gia_Man_t *
             ThData[i].fVerbose = fVerbose;
             ThData[i].nTimeOutU= nTimeOutU;
             ThData[i].pWlc     = pWlc;
+            ThData[i].pUfarArgs= pUfarArgs;
             ThData[i].WorkerId = i;
             ThData[i].StageId  = StageId;
             ThData[i].NetId    = NetId;
@@ -1117,6 +1228,7 @@ static void Cec_GiaInitThreads( Par_ThData_t * ThData, int nWorkers, Gia_Man_t *
         ThData[i].fVerbose = fVerbose;
         ThData[i].nTimeOutU= nTimeOutU;
         ThData[i].pWlc     = pWlc;
+        ThData[i].pUfarArgs= pUfarArgs;
         ThData[i].WorkerId = i;
         ThData[i].StageId  = StageId;
         ThData[i].NetId    = NetId;
@@ -1190,22 +1302,29 @@ int Cec_GiaReplayReadParams( char * pFileName, int * pnProcs, int * pnTimeOut, i
         *pnTimeOut3 = Plan.nTimeOut3;
     if ( pfUseUif )
         *pfUseUif = Plan.fUseUif;
+    Cec_SprovePlanFree( &Plan );
     return 1;
 }
-int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, int nTimeOut3, int fUseUif, Wlc_Ntk_t * pWlc, int fVerbose, int fVeryVerbose, int fSilent, char * pReplayFile )
+int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, int nTimeOut3, int fUseUif, Wlc_Ntk_t * pWlc, int fVerbose, int fVeryVerbose, int fSilent, char * pReplayFile, char * pUfarArgs )
 {
     Cec_SprovePlan_t Plan;
-    Cec_SprovePlanDefault( &Plan, nProcs, nTimeOut, nTimeOut2, nTimeOut3, fUseUif );
+    int RetValue;
+    Cec_SprovePlanDefault( &Plan, nProcs, nTimeOut, nTimeOut2, nTimeOut3, fUseUif, pUfarArgs );
     assert( nProcs >= 1 && nProcs <= 6 );
     assert( nProcs + (fUseUif ? 1 : 0) <= PAR_THR_MAX );
-    return Cec_SproveExecutePlan( p, &Plan, pWlc, fVerbose, fVeryVerbose, fSilent, pReplayFile );
+    RetValue = Cec_SproveExecutePlan( p, &Plan, pWlc, fVerbose, fVeryVerbose, fSilent, pReplayFile );
+    Cec_SprovePlanFree( &Plan );
+    return RetValue;
 }
 int Cec_GiaReplayTest( Gia_Man_t * p, Wlc_Ntk_t * pWlc, char * pFileName, int fVerbose, int fVeryVerbose, int fSilent )
 {
     Cec_SprovePlan_t Plan;
+    int RetValue;
     if ( !Cec_SproveReplayReadPlan( pFileName, &Plan ) )
         return -1;
-    return Cec_SproveExecutePlan( p, &Plan, pWlc, fVerbose, fVeryVerbose, fSilent, NULL );
+    RetValue = Cec_SproveExecutePlan( p, &Plan, pWlc, fVerbose, fVeryVerbose, fSilent, NULL );
+    Cec_SprovePlanFree( &Plan );
+    return RetValue;
 }
 
 #endif // pthreads are used

src/proof/cec/module.make

@@ -3,6 +3,7 @@ SRC +=    src/proof/cec/cecCec.c \
     src/proof/cec/cecClass.c \
     src/proof/cec/cecCore.c \
     src/proof/cec/cecCorr.c \
+    src/proof/cec/cecCorrIncr.c \
     src/proof/cec/cecIso.c \
     src/proof/cec/cecMan.c \
     src/proof/cec/cecPat.c \

src/sat/bmc/bmcBmcG.c

@@ -362,6 +362,8 @@ int Bmcg_ManPerformOne( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
     Abc_CexFreeP( &pGia->pCexSeq );
     for ( f = 0; !pPars->nFramesMax || f < pPars->nFramesMax; f += pPars->nFramesAdd )
     {
+        if ( pPars->pFuncProgress && pPars->pFuncProgress( pPars->pProgress, 0, 0 ) )
+            break;
         Cnf_Dat_t * pCnf = Bmcg_ManAddNewCnf( p, f, pPars->nFramesAdd );
         if ( pCnf == NULL )
         {
@@ -378,15 +380,21 @@ int Bmcg_ManPerformOne( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
         assert( Gia_ManPoNum(p->pFrames) == (f + pPars->nFramesAdd) * Gia_ManPoNum(pGia) );
         for ( k = 0; k < pPars->nFramesAdd; k++ )
         {
+            if ( pPars->pFuncProgress && pPars->pFuncProgress( pPars->pProgress, 0, 0 ) )
+                break;
             for ( i = 0; i < Gia_ManPoNum(pGia); i++ )
             {
                 abctime clk = Abc_Clock();
                 int iObj = Gia_ObjId( p->pFrames, Gia_ManCo(p->pFrames, (f+k) * Gia_ManPoNum(pGia) + i) );
                 int iLit = Abc_Var2Lit( Vec_IntEntry(&p->vFr2Sat, iObj), 0 );
+                if ( pPars->pFuncProgress && pPars->pFuncProgress( pPars->pProgress, 0, 0 ) )
+                    break;
                 if ( pPars->nTimeOut && (Abc_Clock() - clkStart)/CLOCKS_PER_SEC >= pPars->nTimeOut )
                     break;
                 status = bmcg_sat_solver_solve( p->pSats[0], &iLit, 1 );
                 p->timeSat += Abc_Clock() - clk;
+                if ( pPars->pFuncProgress && pPars->pFuncProgress( pPars->pProgress, 0, 0 ) )
+                    break;
                 if ( status == -1 ) // unsat
                 {
                     if ( i == Gia_ManPoNum(pGia)-1 )

src/sat/cadical/cadical_file.cpp

@@ -41,7 +41,7 @@ extern "C" {
 
 #endif
 
-#if defined(__APPLE__) || defined(__MACH__)
+#if defined(__APPLE__) && defined(__MACH__)
 
 extern "C" {
 #include <libproc.h>
@@ -293,7 +293,7 @@ FILE *File::read_pipe (Internal *internal, const char *fmt, const int *sig,
 
 #if !defined(_WIN32) && !defined(__wasm)
 
-#if defined(__APPLE__) || defined(__MACH__)
+#if defined(__APPLE__) && defined(__MACH__)
 static std::mutex compressed_file_writing_mutex;
 #endif
 
@@ -312,7 +312,7 @@ FILE *File::write_pipe (Internal *internal, const char *command,
   char *absolute_command_path = find_program (argv[0]);
   int pipe_fds[2], out;
   FILE *res = 0;
-#if defined(__APPLE__) || defined(__MACH__)
+#if defined(__APPLE__) && defined(__MACH__)
   compressed_file_writing_mutex.lock ();
 #endif
   if (!absolute_command_path)
@@ -369,7 +369,7 @@ FILE *File::write_pipe (Internal *internal, const char *command,
 #ifdef CADICAL_QUIET
   (void) internal;
 #endif
-#if defined(__APPLE__) || defined(__MACH__)
+#if defined(__APPLE__) && defined(__MACH__)
   if (!res)
     compressed_file_writing_mutex.unlock ();
 #endif
@@ -475,7 +475,7 @@ void File::close (bool print) {
       MSG ("closing output pipe to write '%s'", name ());
     fclose (file);
     waitpid (child_pid, 0, 0);
-#if defined(__APPLE__) || defined(__MACH__)
+#if defined(__APPLE__) && defined(__MACH__)
     compressed_file_writing_mutex.unlock ();
 #endif
   }

src/sat/glucose/AbcGlucose.cpp

@@ -878,6 +878,9 @@ Vec_Int_t * Glucose_SolverFromAig( Gia_Man_t * p, SimpSolver& s )
     abctime clk = Abc_Clock();
     vec<Lit> * lits = &s.user_lits;
     Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8 /*nLutSize*/, 0 /*fCnfObjIds*/, 1/*fAddOrCla*/, 0, 0/*verbose*/ );
+    // CNF variable IDs are 1-based and may include unused variables.
+    // Create the full range so model[] can be indexed by pVarNums directly.
+    s.addVar( pCnf->nVars - 1 );
     for ( int i = 0; i < pCnf->nClauses; i++ )
     {
         lits->clear();

src/sat/glucose2/AbcGlucose2.cpp

@@ -896,6 +896,9 @@ Vec_Int_t * Glucose_SolverFromAig( Gia_Man_t * p, SimpSolver& s )
     abctime clk = Abc_Clock();
     vec<Lit> * lits = &s.user_lits;
     Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8 /*nLutSize*/, 0 /*fCnfObjIds*/, 1/*fAddOrCla*/, 0, 0/*verbose*/ );
+    // CNF variable IDs are 1-based and may include unused variables.
+    // Create the full range so model[] can be indexed by pVarNums directly.
+    s.addVar( pCnf->nVars - 1 );
     for ( int i = 0; i < pCnf->nClauses; i++ )
     {
         lits->clear();

test/write_cnf_dangling.sh

@@ -0,0 +1,60 @@
+#!/usr/bin/env bash
+# Regression test for berkeley-abc/abc#479
+#
+# After "strash", a primary input wired directly to a primary output becomes
+# a dangling PI: it shows up in the DIMACS header's variable count but the
+# Tseitin encoder emits no clause mentioning it.  Such a free variable
+# silently doubles the model count of the written formula, breaking #SAT
+# and uniform sampling.
+#
+# The fix in Cnf_DataWriteIntoFile() detects DIMACS variables that are
+# declared in the header but unreferenced in any clause, and emits a unit
+# clause pinning each of them to false.  The two cases below exercise that
+# behaviour against the abc binary.
+
+set -eu
+
+ABC=${ABC:-./abc}
+TMP=$(mktemp -d)
+trap 'rm -rf "$TMP"' EXIT
+
+fail() { echo "FAIL: $1" >&2; exit 1; }
+
+run_case() {
+    local name=$1 input=$2
+    local in="$TMP/$name.in.cnf" out="$TMP/$name.out.cnf"
+    printf '%s' "$input" > "$in"
+    "$ABC" -q "read_cnf $in; strash; write_cnf $out" > /dev/null
+
+    # Extract declared variable count from the header.
+    local header
+    header=$(grep -m1 '^p cnf ' "$out")
+    local nVars
+    nVars=$(echo "$header" | awk '{print $3}')
+
+    # Every variable 1..nVars must appear (positive or negated) in some clause.
+    local v
+    for v in $(seq 1 "$nVars"); do
+        if ! grep -Eq "(^|[ \t-])$v( |$)" "$out"; then
+            cat "$out" >&2
+            fail "$name: variable $v declared in header but never used in any clause"
+        fi
+    done
+    echo "PASS: $name ($header)"
+}
+
+# Case 1: original reproducer from issue #479 -- a single PI wired directly
+# to a single PO.  Before the fix, the output was "p cnf 3 2" with clauses
+# "-3 0" and "2 0", leaving variable 1 unconstrained.
+run_case "pi_to_po_direct" "p cnf 1 1
+1 0
+"
+
+# Case 2: two independent PIs, each a direct wire to its own PO.  Both PIs
+# end up dangling after strash.
+run_case "two_pis_two_pos" "p cnf 2 2
+1 0
+2 0
+"
+
+echo "All regression tests passed."