Version abc80507

Makefile

@@ -20,7 +20,7 @@ MODULES := src/base/abc src/base/abci src/base/cmd \
 	src/aig/mem src/aig/dar src/aig/fra src/aig/cnf \
 	src/aig/csw src/aig/ioa src/aig/aig src/aig/kit \
 	src/aig/bdc src/aig/bar src/aig/ntl src/aig/nwk src/aig/mfx \
-	src/aig/tim src/aig/saig
+	src/aig/tim src/aig/saig src/aig/bbr
 
 default: $(PROG)
 

abc.dsp

@@ -42,7 +42,7 @@ RSC=rc.exe
 # PROP Ignore_Export_Lib 0
 # PROP Target_Dir ""
 # ADD BASE CPP /nologo /W3 /GX /O2 /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /c
-# ADD CPP /nologo /W3 /GX /O2 /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /I "src/aig/saig" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /c
+# ADD CPP /nologo /W3 /GX /O2 /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /I "src/aig/saig" /I "src/aig/bbr" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /c
 # ADD BASE RSC /l 0x409 /d "NDEBUG"
 # ADD RSC /l 0x409 /d "NDEBUG"
 BSC32=bscmake.exe
@@ -66,7 +66,7 @@ LINK32=link.exe
 # PROP Ignore_Export_Lib 0
 # PROP Target_Dir ""
 # ADD BASE CPP /nologo /W3 /Gm /GX /ZI /Od /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /GZ /c
-# ADD CPP /nologo /W3 /Gm /GX /ZI /Od /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /I "src/aig/saig" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /GZ /c
+# ADD CPP /nologo /W3 /Gm /GX /ZI /Od /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /I "src/aig/saig" /I "src/aig/bbr" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /GZ /c
 # SUBTRACT CPP /X
 # ADD BASE RSC /l 0x409 /d "_DEBUG"
 # ADD RSC /l 0x409 /d "_DEBUG"
@@ -3269,6 +3269,26 @@ SOURCE=.\src\aig\saig\saigRetMin.c
 SOURCE=.\src\aig\saig\saigScl.c
 # End Source File
 # End Group
+# Begin Group "bbr"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\aig\bbr\bbr.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\bbr\bbrImage.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\bbr\bbrNtbdd.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\bbr\bbrReach.c
+# End Source File
+# End Group
 # End Group
 # End Group
 # Begin Group "Header Files"

src/aig/bbr/bbr.h

+/**CFile****************************************************************
+
+  FileName    [bbr.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [BDD-based reachability analysis.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: bbr.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef __BBR_H__
+#define __BBR_H__
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include <stdio.h>
+#include "cuddInt.h"
+#include "aig.h"
+#include "saig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+static inline DdNode * Aig_ObjGlobalBdd( Aig_Obj_t * pObj )  { return pObj->pData; }
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== bbrImage.c ==========================================================*/
+typedef struct Bbr_ImageTree_t_  Bbr_ImageTree_t;
+extern Bbr_ImageTree_t * Bbr_bddImageStart( 
+    DdManager * dd, DdNode * bCare,
+    int nParts, DdNode ** pbParts,
+    int nVars, DdNode ** pbVars, int fVerbose );
+extern DdNode *    Bbr_bddImageCompute( Bbr_ImageTree_t * pTree, DdNode * bCare );
+extern void        Bbr_bddImageTreeDelete( Bbr_ImageTree_t * pTree );
+extern DdNode *    Bbr_bddImageRead( Bbr_ImageTree_t * pTree );
+typedef struct Bbr_ImageTree2_t_  Bbr_ImageTree2_t;
+extern Bbr_ImageTree2_t * Bbr_bddImageStart2( 
+    DdManager * dd, DdNode * bCare,
+    int nParts, DdNode ** pbParts,
+    int nVars, DdNode ** pbVars, int fVerbose );
+extern DdNode *    Bbr_bddImageCompute2( Bbr_ImageTree2_t * pTree, DdNode * bCare );
+extern void        Bbr_bddImageTreeDelete2( Bbr_ImageTree2_t * pTree );
+extern DdNode *    Bbr_bddImageRead2( Bbr_ImageTree2_t * pTree );
+/*=== bbrNtbdd.c ==========================================================*/
+extern void        Aig_ManFreeGlobalBdds( Aig_Man_t * p, DdManager * dd );
+extern int         Aig_ManSizeOfGlobalBdds( Aig_Man_t * p );
+extern DdManager * Aig_ManComputeGlobalBdds( Aig_Man_t * p, int nBddSizeMax, int fDropInternal, int fReorder, int fVerbose );
+/*=== bbrReach.c ==========================================================*/
+extern int         Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose );
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+

src/aig/bbr/bbrNtbdd.c

+/**CFile****************************************************************
+
+  FileName    [bbrNtbdd.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [BDD-based reachability analysis.]
+
+  Synopsis    [Procedures to construct global BDDs for the network.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: bbrNtbdd.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "bbr.h"
+//#include "bar.h"
+
+typedef char ProgressBar;
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static inline void     Aig_ObjSetGlobalBdd( Aig_Obj_t * pObj, DdNode * bFunc )   { pObj->pData = bFunc; }
+static inline void     Aig_ObjCleanGlobalBdd( DdManager * dd, Aig_Obj_t * pObj ) { Cudd_RecursiveDeref( dd, pObj->pData ); pObj->pData = NULL; }
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the global BDD for one AIG node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Bbr_NodeGlobalBdds_rec( DdManager * dd, Aig_Obj_t * pNode, int nBddSizeMax, int fDropInternal, ProgressBar * pProgress, int * pCounter, int fVerbose )
+{
+    DdNode * bFunc, * bFunc0, * bFunc1;
+    int fDetectMuxes = 1;
+    assert( !Aig_IsComplement(pNode) );
+    if ( Cudd_ReadKeys(dd)-Cudd_ReadDead(dd) > (unsigned)nBddSizeMax )
+    {
+//        Extra_ProgressBarStop( pProgress );
+        if ( fVerbose )
+        printf( "The number of live nodes reached %d.\n", nBddSizeMax );
+        fflush( stdout );
+        return NULL;
+    }
+    // if the result is available return
+    if ( Aig_ObjGlobalBdd(pNode) == NULL )
+    {
+        // compute the result for both branches
+        bFunc0 = Bbr_NodeGlobalBdds_rec( dd, Aig_ObjFanin0(pNode), nBddSizeMax, fDropInternal, pProgress, pCounter, fVerbose ); 
+        if ( bFunc0 == NULL )
+            return NULL;
+        Cudd_Ref( bFunc0 );
+        bFunc1 = Bbr_NodeGlobalBdds_rec( dd, Aig_ObjFanin1(pNode), nBddSizeMax, fDropInternal, pProgress, pCounter, fVerbose ); 
+        if ( bFunc1 == NULL )
+            return NULL;
+        Cudd_Ref( bFunc1 );
+        bFunc0 = Cudd_NotCond( bFunc0, Aig_ObjFaninC0(pNode) );
+        bFunc1 = Cudd_NotCond( bFunc1, Aig_ObjFaninC1(pNode) );
+        // get the final result
+        bFunc = Cudd_bddAnd( dd, bFunc0, bFunc1 );   Cudd_Ref( bFunc );
+        Cudd_RecursiveDeref( dd, bFunc0 );
+        Cudd_RecursiveDeref( dd, bFunc1 );
+        // add the number of used nodes
+        (*pCounter)++;
+        // set the result
+        assert( Aig_ObjGlobalBdd(pNode) == NULL );
+        Aig_ObjSetGlobalBdd( pNode, bFunc );
+        // increment the progress bar
+//        if ( pProgress )
+//            Extra_ProgressBarUpdate( pProgress, *pCounter, NULL );
+    }
+    // prepare the return value
+    bFunc = Aig_ObjGlobalBdd(pNode);
+    // dereference BDD at the node
+    if ( --pNode->nRefs == 0 && fDropInternal )
+    {
+        Cudd_Deref( bFunc );
+        Aig_ObjSetGlobalBdd( pNode, NULL );
+    }
+    return bFunc;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Frees the global BDDs of the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManFreeGlobalBdds( Aig_Man_t * p, DdManager * dd ) 
+{ 
+    Aig_Obj_t * pObj;
+    int i;
+    Aig_ManForEachObj( p, pObj, i )
+        if ( Aig_ObjGlobalBdd(pObj) )
+            Aig_ObjCleanGlobalBdd( dd, pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the shared size of global BDDs of the COs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ManSizeOfGlobalBdds( Aig_Man_t * p ) 
+{
+    Vec_Ptr_t * vFuncsGlob;
+    Aig_Obj_t * pObj;
+    int RetValue, i;
+    // complement the global functions
+    vFuncsGlob = Vec_PtrAlloc( Aig_ManPoNum(p) );
+    Aig_ManForEachPo( p, pObj, i )
+        Vec_PtrPush( vFuncsGlob, Aig_ObjGlobalBdd(pObj) );
+    RetValue = Cudd_SharingSize( (DdNode **)Vec_PtrArray(vFuncsGlob), Vec_PtrSize(vFuncsGlob) );
+    Vec_PtrFree( vFuncsGlob );
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Recursively computes global BDDs for the AIG in the manager.]
+
+  Description [On exit, BDDs are stored in the pNode->pData fields.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdManager * Aig_ManComputeGlobalBdds( Aig_Man_t * p, int nBddSizeMax, int fDropInternal, int fReorder, int fVerbose )
+{
+    ProgressBar * pProgress = NULL;
+    Aig_Obj_t * pObj;
+    DdManager * dd;
+    DdNode * bFunc;
+    int i, Counter;
+    // start the manager
+    dd = Cudd_Init( Aig_ManPiNum(p), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+    // set reordering
+    if ( fReorder )
+        Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
+    // prepare to construct global BDDs
+    Aig_ManCleanData( p );
+    // assign the constant node BDD
+    Aig_ObjSetGlobalBdd( Aig_ManConst1(p), dd->one );   Cudd_Ref( dd->one );
+    // set the elementary variables
+    Aig_ManForEachPi( p, pObj, i )
+    {
+        Aig_ObjSetGlobalBdd( pObj, dd->vars[i] );  Cudd_Ref( dd->vars[i] );
+    }
+
+    // collect the global functions of the COs
+    Counter = 0;
+    // construct the BDDs
+//    pProgress = Extra_ProgressBarStart( stdout, Aig_ManNodeNum(p) );
+    Aig_ManForEachPo( p, pObj, i )
+    {
+        bFunc = Bbr_NodeGlobalBdds_rec( dd, Aig_ObjFanin0(pObj), nBddSizeMax, fDropInternal, pProgress, &Counter, fVerbose );
+        if ( bFunc == NULL )
+        {
+            if ( fVerbose )
+            printf( "Constructing global BDDs is aborted.\n" );
+            Aig_ManFreeGlobalBdds( p, dd );
+            Cudd_Quit( dd ); 
+            // reset references
+            Aig_ManResetRefs( p );
+            return NULL;
+        }
+        bFunc = Cudd_NotCond( bFunc, Aig_ObjFaninC0(pObj) );  Cudd_Ref( bFunc ); 
+        Aig_ObjSetGlobalBdd( pObj, bFunc );
+    }
+//    Extra_ProgressBarStop( pProgress );
+    // reset references
+    Aig_ManResetRefs( p );
+    // reorder one more time
+    if ( fReorder )
+    {
+        Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 1 );
+        Cudd_AutodynDisable( dd );
+    }
+//    Cudd_PrintInfo( dd, stdout );
+    return dd;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/aig/bbr/bbr_.c

+/**CFile****************************************************************
+
+  FileName    [.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName []
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: .c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "__Int.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/aig/bbr/module.make

+SRC +=    src/aig/bbr/bbrImage.c \
+    src/aig/bbr/bbrNtbdd.c \
+    src/aig/bdr/bbrReach.c

src/aig/fra/fra.h

@@ -328,7 +328,7 @@ extern int                 Fra_NodesAreImp( Fra_Man_t * p, Aig_Obj_t * pOld, Aig
 extern int                 Fra_NodesAreClause( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew, int fComplL, int fComplR );
 extern int                 Fra_NodeIsConst( Fra_Man_t * p, Aig_Obj_t * pNew );
 /*=== fraSec.c ========================================================*/
-extern int                 Fra_FraigSec( Aig_Man_t * p, int nFrames, int fRetimeFirst, int fFraiging, int fVerbose, int fVeryVerbose );
+extern int                 Fra_FraigSec( Aig_Man_t * p, int nFrames, int fPhaseAbstract, int fRetimeFirst, int fRetimeRegs, int fFraiging, int fVerbose, int fVeryVerbose );
 /*=== fraSim.c ========================================================*/
 extern int                 Fra_SmlNodeHash( Aig_Obj_t * pObj, int nTableSize );
 extern int                 Fra_SmlNodeIsConst( Aig_Obj_t * pObj );

src/aig/fra/fraSec.c

@@ -40,7 +40,7 @@
   SeeAlso     []
 
 ***********************************************************************/
-int Fra_FraigSec( Aig_Man_t * p, int nFramesMax, int fRetimeFirst, int fFraiging, int fVerbose, int fVeryVerbose )
+int Fra_FraigSec( Aig_Man_t * p, int nFramesMax, int fPhaseAbstract, int fRetimeFirst, int fRetimeRegs, int fFraiging, int fVerbose, int fVeryVerbose )
 {
     Fra_Ssw_t Pars, * pPars = &Pars;
     Fra_Sml_t * pSml;
@@ -79,6 +79,23 @@ clk = clock();
 PRT( "Time", clock() - clk );
     }
 
+    // perform phase abstraction
+clk = clock();
+    if ( fPhaseAbstract )
+    {
+        extern Aig_Man_t * Saig_ManPhaseAbstractAuto( Aig_Man_t * p, int fVerbose );
+        pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); 
+        pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew); 
+        pNew = Saig_ManPhaseAbstractAuto( pTemp = pNew, 0 );
+        Aig_ManStop( pTemp );
+        if ( fVerbose )
+        {
+            printf( "Phase abstraction:    Latches = %5d. Nodes = %6d. ", 
+                Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
+PRT( "Time", clock() - clk );
+        }
+    }
+
     // perform forward retiming
     if ( fRetimeFirst && pNew->nRegs )
     {
@@ -133,6 +150,26 @@ PRT( "Time", clock() - clk );
     }
     }
 
+    // perform min-area retiming
+    if ( fRetimeRegs && pNew->nRegs )
+    {
+    extern Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose );
+clk = clock();
+    pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); 
+    pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew); 
+//        pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 );
+    pNew = Saig_ManRetimeMinArea( pTemp = pNew, 1000, 0, 0, 1, 0 );
+    Aig_ManStop( pTemp );
+    pNew = Aig_ManDupOrdered( pTemp = pNew );
+    Aig_ManStop( pTemp );
+    if ( fVerbose )
+    {
+    printf( "Min-reg retiming:     Latches = %5d. Nodes = %6d. ", 
+        Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
+PRT( "Time", clock() - clk );
+    }
+    }
+
     // perform seq sweeping while increasing the number of frames
     RetValue = Fra_FraigMiterStatus( pNew );
     if ( RetValue == -1 )
@@ -152,31 +189,22 @@ PRT( "Time", clock() - clk );
         if ( RetValue != -1 )
             break;
 
-        // perform rewriting
-clk = clock();
-        pNew = Aig_ManDupOrdered( pTemp = pNew );
-        Aig_ManStop( pTemp );
-        pNew = Dar_ManRewriteDefault( pTemp = pNew );
-        Aig_ManStop( pTemp );
-        if ( fVerbose )
-        {
-            printf( "Rewriting:            Latches = %5d. Nodes = %6d. ", 
-                Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
-PRT( "Time", clock() - clk );
-        } 
-
         // perform retiming
-        if ( fRetimeFirst && pNew->nRegs )
-//        if ( pNew->nRegs )
+//        if ( fRetimeFirst && pNew->nRegs )
+        if ( pNew->nRegs )
         {
+        extern Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose );
 clk = clock();
-        pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 );
+        pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); 
+        pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew); 
+//        pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 );
+        pNew = Saig_ManRetimeMinArea( pTemp = pNew, 1000, 0, 0, 1, 0 );
         Aig_ManStop( pTemp );
         pNew = Aig_ManDupOrdered( pTemp = pNew );
         Aig_ManStop( pTemp );
         if ( fVerbose )
         {
-            printf( "Forward retiming:     Latches = %5d. Nodes = %6d. ", 
+            printf( "Min-reg retiming:     Latches = %5d. Nodes = %6d. ", 
                 Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
 PRT( "Time", clock() - clk );
         }
@@ -185,6 +213,20 @@ PRT( "Time", clock() - clk );
         if ( pNew->nRegs )
             pNew = Aig_ManConstReduce( pNew, 0 );
 
+        // perform rewriting
+clk = clock();
+        pNew = Aig_ManDupOrdered( pTemp = pNew );
+        Aig_ManStop( pTemp );
+//        pNew = Dar_ManRewriteDefault( pTemp = pNew );
+        pNew = Dar_ManCompress2( pTemp = pNew, 1, 0, 1, 0 ); 
+        Aig_ManStop( pTemp );
+        if ( fVerbose )
+        {
+            printf( "Rewriting:            Latches = %5d. Nodes = %6d. ", 
+                Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
+PRT( "Time", clock() - clk );
+        } 
+
         // perform sequential simulation
         if ( pNew->nRegs )
         {
@@ -213,6 +255,18 @@ PRT( "Time", clock() - clkTotal );
     // get the miter status
     RetValue = Fra_FraigMiterStatus( pNew );
 
+    // try reachability analysis
+    if ( RetValue == -1 && Aig_ManRegNum(pNew) < 200 )
+    {
+        extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose );
+        assert( Aig_ManRegNum(pNew) > 0 );
+        pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); 
+        pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew); 
+clk = clock();
+        RetValue = Aig_ManVerifyUsingBdds( pNew, 100000, 1000, 1, 1, 0 );
+PRT( "Time", clock() - clk );
+    }
+
 finish:
     // report the miter
     if ( RetValue == 1 )

src/aig/hop/hop.h

@@ -188,7 +188,7 @@ static inline Hop_Obj_t *  Hop_ObjChild0Copy( Hop_Obj_t * pObj ) { assert( !Hop_
 static inline Hop_Obj_t *  Hop_ObjChild1Copy( Hop_Obj_t * pObj ) { assert( !Hop_IsComplement(pObj) ); return Hop_ObjFanin1(pObj)? Hop_NotCond((Hop_Obj_t *)Hop_ObjFanin1(pObj)->pData, Hop_ObjFaninC1(pObj)) : NULL;  }
 static inline int          Hop_ObjLevel( Hop_Obj_t * pObj )       { return pObj->nRefs;                            }
 static inline int          Hop_ObjLevelNew( Hop_Obj_t * pObj )    { return 1 + Hop_ObjIsExor(pObj) + AIG_MAX(Hop_ObjFanin0(pObj)->nRefs, Hop_ObjFanin1(pObj)->nRefs);       }
-static inline int          Hop_ObjFaninPhase( Hop_Obj_t * pObj )  { return Hop_IsComplement(pObj)? !Hop_Regular(pObj)->fPhase : pObj->fPhase; }
+static inline int          Hop_ObjPhaseCompl( Hop_Obj_t * pObj )  { return Hop_IsComplement(pObj)? !Hop_Regular(pObj)->fPhase : pObj->fPhase; }
 static inline void         Hop_ObjClean( Hop_Obj_t * pObj )       { memset( pObj, 0, sizeof(Hop_Obj_t) ); }
 static inline int          Hop_ObjWhatFanin( Hop_Obj_t * pObj, Hop_Obj_t * pFanin )    
 { 
@@ -284,6 +284,7 @@ extern int             Hop_DagSize( Hop_Obj_t * pObj );
 extern void            Hop_ConeUnmark_rec( Hop_Obj_t * pObj );
 extern Hop_Obj_t *     Hop_Transfer( Hop_Man_t * pSour, Hop_Man_t * pDest, Hop_Obj_t * pObj, int nVars );
 extern Hop_Obj_t *     Hop_Compose( Hop_Man_t * p, Hop_Obj_t * pRoot, Hop_Obj_t * pFunc, int iVar );
+extern Hop_Obj_t *     Hop_Remap( Hop_Man_t * p, Hop_Obj_t * pRoot, unsigned uSupp, int nVars );
 /*=== hopMan.c ==========================================================*/
 extern Hop_Man_t *     Hop_ManStart();
 extern Hop_Man_t *     Hop_ManDup( Hop_Man_t * p );

src/aig/hop/hopDfs.c

@@ -392,6 +392,74 @@ Hop_Obj_t * Hop_Compose( Hop_Man_t * p, Hop_Obj_t * pRoot, Hop_Obj_t * pFunc, in
     return Hop_NotCond( Hop_Regular(pRoot)->pData, Hop_IsComplement(pRoot) );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Composes the AIG (pRoot) with the function (pFunc) using PI var (iVar).]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Hop_Remap_rec( Hop_Man_t * p, Hop_Obj_t * pObj )
+{
+    assert( !Hop_IsComplement(pObj) );
+    if ( !Hop_ObjIsNode(pObj) || Hop_ObjIsMarkA(pObj) )
+        return;
+    Hop_Remap_rec( p, Hop_ObjFanin0(pObj) ); 
+    Hop_Remap_rec( p, Hop_ObjFanin1(pObj) );
+    pObj->pData = Hop_And( p, Hop_ObjChild0Copy(pObj), Hop_ObjChild1Copy(pObj) );
+    assert( !Hop_ObjIsMarkA(pObj) ); // loop detection
+    Hop_ObjSetMarkA( pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Composes the AIG (pRoot) with the function (pFunc) using PI var (iVar).]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Hop_Obj_t * Hop_Remap( Hop_Man_t * p, Hop_Obj_t * pRoot, unsigned uSupp, int nVars )
+{
+    Hop_Obj_t * pObj;
+    int i, k;
+    // quit if the PI variable is not defined
+    if ( nVars > Hop_ManPiNum(p) )
+    {
+        printf( "Hop_Remap(): The number of variables (%d) is more than the manager size (%d).\n", nVars, Hop_ManPiNum(p) );
+        return NULL;
+    }
+    // return if constant
+    if ( Hop_ObjIsConst1( Hop_Regular(pRoot) ) )
+        return pRoot;
+    if ( uSupp == 0 )
+        return Hop_NotCond( Hop_ManConst0(p), Hop_ObjPhaseCompl(pRoot) );
+    // set the PI mapping
+    k = 0;
+    Hop_ManForEachPi( p, pObj, i )
+    {
+        if ( i == nVars )
+           break;
+        if ( uSupp & (1 << i) )
+            pObj->pData = Hop_IthVar(p, k++);
+        else
+            pObj->pData = Hop_ManConst0(p);
+    }
+    assert( k > 0 && k < nVars );
+    // recursively perform composition
+    Hop_Remap_rec( p, Hop_Regular(pRoot) );
+    // clear the markings
+    Hop_ConeUnmark_rec( Hop_Regular(pRoot) );
+    return Hop_NotCond( Hop_Regular(pRoot)->pData, Hop_IsComplement(pRoot) );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/aig/hop/hopObj.c

@@ -73,7 +73,7 @@ Hop_Obj_t * Hop_ObjCreatePo( Hop_Man_t * p, Hop_Obj_t * pDriver )
     else
         pObj->nRefs = Hop_ObjLevel( Hop_Regular(pDriver) );
     // set the phase
-    pObj->fPhase = Hop_ObjFaninPhase(pDriver);
+    pObj->fPhase = Hop_ObjPhaseCompl(pDriver);
     // update node counters of the manager
     p->nObjs[AIG_PO]++;
     return pObj;
@@ -136,7 +136,7 @@ void Hop_ObjConnect( Hop_Man_t * p, Hop_Obj_t * pObj, Hop_Obj_t * pFan0, Hop_Obj
     else
         pObj->nRefs = Hop_ObjLevelNew( pObj );
     // set the phase
-    pObj->fPhase = Hop_ObjFaninPhase(pFan0) & Hop_ObjFaninPhase(pFan1);
+    pObj->fPhase = Hop_ObjPhaseCompl(pFan0) & Hop_ObjPhaseCompl(pFan1);
     // add the node to the structural hash table
     Hop_TableInsert( p, pObj );
 }

src/aig/ntl/ntl.h

@@ -52,7 +52,7 @@ typedef enum {
     NTL_OBJ_NONE,                      // 0: non-existent object
     NTL_OBJ_PI,                        // 1: primary input
     NTL_OBJ_PO,                        // 2: primary output
-    NTL_OBJ_LATCH,                     // 3: latch node
+    NTL_OBJ_LATCH,                     // 3: latch 
     NTL_OBJ_NODE,                      // 4: logic node
     NTL_OBJ_LUT1,                      // 5: inverter/buffer
     NTL_OBJ_BOX,                       // 6: white box or black box

src/aig/ntl/ntlFraig.c

@@ -76,6 +76,8 @@ Aig_Obj_t ** Ntl_ManFraigDeriveClasses( Aig_Man_t * pAig, Ntl_Man_t * pNew, Aig_
         if ( Aig_ObjIsPo(pObj) )
             continue;
         pObjCol = pObj->pData;
+        if ( pObjCol == NULL )
+            continue;
         if ( pMapBack[pObjCol->Id] == NULL )
             pMapBack[pObjCol->Id] = pObj;
     }
@@ -89,6 +91,8 @@ Aig_Obj_t ** Ntl_ManFraigDeriveClasses( Aig_Man_t * pAig, Ntl_Man_t * pNew, Aig_
             continue;
         // get the collapsed node
         pObjCol = pObj->pData;
+        if ( pObjCol == NULL )
+            continue;
         // get the representative of the collapsed node
         pObjColRepr = pAigCol->pReprs[pObjCol->Id];
         if ( pObjColRepr == NULL )

src/aig/ntl/ntlInsert.c

@@ -82,6 +82,8 @@ Ntl_Man_t * Ntl_ManInsertMapping( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t
                 Ntl_ObjSetFanin( pNode, pNet, k );
             }
         }
+        else
+            pNode->nFanins = 0;
         sprintf( Buffer, "lut%0*d", nDigits, i );
         if ( (pNet = Ntl_ModelFindNet( pRoot, Buffer )) )
         {
@@ -302,6 +304,8 @@ Ntl_Man_t * Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk )
                 Ntl_ObjSetFanin( pNode, pNet, k );
             }
         }
+        else
+            pNode->nFanins = 0;
         sprintf( Buffer, "lut%0*d", nDigits, i );
         if ( (pNet = Ntl_ModelFindNet( pRoot, Buffer )) )
         {
@@ -341,13 +345,16 @@ Ntl_Man_t * Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk )
         if ( !Ntl_ModelSetNetDriver( pNode, pNetCo ) )
         {
             printf( "Ntl_ManInsertNtk(): Internal error: PO net has more than one fanin.\n" );
-            return 0;
+            return NULL;
         }
     }
     // clean CI/CO marks
     Ntl_ManUnmarkCiCoNets( p );
     if ( !Ntl_ManCheck( p ) )
+    {
         printf( "Ntl_ManInsertNtk: The check has failed for design %s.\n", p->pName );
+        return NULL;
+    }
     return p;
 }
 

src/aig/ntl/ntlObj.c

@@ -103,7 +103,7 @@ Ntl_Obj_t * Ntl_ModelCreateLatch( Ntl_Mod_t * pModel )
     Vec_PtrPush( pModel->vObjs, p );
     p->pModel   = pModel;
     p->Type     = NTL_OBJ_LATCH;
-    p->nFanins  = 2;
+    p->nFanins  = 1;
     p->nFanouts = 1;
     pModel->nObjs[NTL_OBJ_LATCH]++;
     return p;

src/aig/ntl/ntlReadBlif.c

@@ -825,7 +825,7 @@ static int Ioa_ReadParseLineLatch( Ioa_ReadMod_t * p, char * pLine )
     {
         pToken = Vec_PtrEntry(vTokens,Vec_PtrSize(vTokens)-2);
         pNetLi = Ntl_ModelFindOrCreateNet( p->pNtk, pToken );
-        pObj->pFanio[1] = pNetLi;
+//        pObj->pFanio[1] = pNetLi;
     }
     return 1;
 }

src/aig/ntl/ntlWriteBlif.c

@@ -28,7 +28,7 @@
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
-
+ 
 /**Function*************************************************************
 
   Synopsis    [Writes one model into the BLIF file.]

src/aig/nwk/nwk.h

@@ -285,6 +285,7 @@ extern void            Nwk_ObjPrint( Nwk_Obj_t * pObj );
 extern void            Nwk_ManDumpBlif( Nwk_Man_t * pNtk, char * pFileName, Vec_Ptr_t * vCiNames, Vec_Ptr_t * vCoNames );
 extern void            Nwk_ManPrintFanioNew( Nwk_Man_t * pNtk );
 extern void            Nwk_ManCleanMarks( Nwk_Man_t * pNtk );
+extern void            Nwk_ManMinimumBase( Nwk_Man_t * pNtk, int fVerbose );
 
 #ifdef __cplusplus
 }

src/aig/nwk/nwkMap.c

@@ -146,7 +146,7 @@ If_Man_t * Nwk_ManToIf( Aig_Man_t * p, If_Par_t * pPars, Vec_Ptr_t * vAigToIf )
 
 /**Function*************************************************************
 
-  Synopsis    [Recursively derives the truth table for the cut.]
+  Synopsis    [Recursively derives the local AIG for the cut.]
 
   Description []
                
@@ -193,7 +193,7 @@ Hop_Obj_t * Nwk_NodeIfToHop2_rec( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Obj
 
 /**Function*************************************************************
 
-  Synopsis    [Derives the truth table for one cut.]
+  Synopsis    [Derives the local AIG for the cut.]
 
   Description []
                
@@ -309,6 +309,7 @@ Nwk_Man_t * Nwk_ManFromIf( If_Man_t * pIfMan, Aig_Man_t * p, Vec_Ptr_t * vAigToI
     }
     Vec_PtrFree( vIfToAig );
     pNtk->pManTime = Tim_ManDup( pIfMan->pManTim, 0 );
+    Nwk_ManMinimumBase( pNtk, 0 );
     assert( Nwk_ManCheck( pNtk ) );
     return pNtk;
 }

src/aig/nwk/nwkUtil.c

@@ -56,7 +56,7 @@ void Nwk_ManIncrementTravId( Nwk_Man_t * pNtk )
 
 /**Function*************************************************************
 
-  Synopsis    [Reads the maximum number of fanins.]
+  Synopsis    [Reads the maximum number of fanins of a node.]
 
   Description []
                
@@ -100,7 +100,7 @@ int Nwk_ManGetTotalFanins( Nwk_Man_t * pNtk )
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Returns the number of true PIs.]
 
   Description []
                
@@ -120,7 +120,7 @@ int Nwk_ManPiNum( Nwk_Man_t * pNtk )
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Returns the number of true POs.]
 
   Description []
                
@@ -140,7 +140,7 @@ int Nwk_ManPoNum( Nwk_Man_t * pNtk )
 
 /**Function*************************************************************
 
-  Synopsis    [Reads the number of BDD nodes.]
+  Synopsis    [Reads the number of AIG nodes.]
 
   Description []
                
@@ -211,7 +211,7 @@ int Nwk_NodeCompareLevelsDecrease( Nwk_Obj_t ** pp1, Nwk_Obj_t ** pp2 )
 
 /**Function*************************************************************
 
-  Synopsis    [Deletes the node.]
+  Synopsis    [Prints the objects.]
 
   Description []
                
@@ -242,7 +242,7 @@ void Nwk_ObjPrint( Nwk_Obj_t * pObj )
 
 /**Function*************************************************************
 
-  Synopsis    [Deletes the node.]
+  Synopsis    [Dumps the BLIF file for the network.]
 
   Description []
                
@@ -449,7 +449,7 @@ void Nwk_ManPrintFanioNew( Nwk_Man_t * pNtk )
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Cleans the temporary marks of the nodes.]
 
   Description []
                
@@ -466,6 +466,48 @@ void Nwk_ManCleanMarks( Nwk_Man_t * pMan )
         pObj->MarkA = pObj->MarkB = 0;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Minimizes the support of all nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ManMinimumBase( Nwk_Man_t * pNtk, int fVerbose )
+{
+    unsigned * pTruth;
+    Vec_Int_t * vTruth;
+    Nwk_Obj_t * pObj, * pFanin, * pObjNew;
+    int uSupp, nSuppSize, i, k, Counter = 0;
+    vTruth = Vec_IntAlloc( 1 << 16 );
+    Nwk_ManForEachNode( pNtk, pObj, i )
+    {
+        pTruth = Hop_ManConvertAigToTruth( pNtk->pManHop, Hop_Regular(pObj->pFunc), Nwk_ObjFaninNum(pObj), vTruth, 0 );
+        nSuppSize = Kit_TruthSupportSize(pTruth, Nwk_ObjFaninNum(pObj));
+        if ( nSuppSize == Nwk_ObjFaninNum(pObj) )
+            continue;
+        Counter++;
+        uSupp = Kit_TruthSupport( pTruth, Nwk_ObjFaninNum(pObj) );
+        // create new node with the given support
+        pObjNew = Nwk_ManCreateNode( pNtk, nSuppSize, Nwk_ObjFanoutNum(pObj) );
+        Nwk_ObjForEachFanin( pObj, pFanin, k )
+            if ( uSupp & (1 << k) )
+                Nwk_ObjAddFanin( pObjNew, pFanin );
+        pObjNew->pFunc = Hop_Remap( pNtk->pManHop, pObj->pFunc, uSupp, Nwk_ObjFaninNum(pObj) );
+        if ( fVerbose )
+            printf( "Reducing node %d fanins from %d to %d.\n", 
+                pObj->Id, Nwk_ObjFaninNum(pObj), Nwk_ObjFaninNum(pObjNew) );
+        Nwk_ObjReplace( pObj, pObjNew );
+    }
+    if ( fVerbose && Counter )
+        printf( "Support minimization reduced support of %d nodes.\n", Counter );
+    Vec_IntFree( vTruth );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/aig/saig/saig.h

@@ -45,6 +45,8 @@ extern "C" {
 
 static inline int          Saig_ManPiNum( Aig_Man_t * p )          { return p->nTruePis;                     }
 static inline int          Saig_ManPoNum( Aig_Man_t * p )          { return p->nTruePos;                     }
+static inline int          Saig_ManCiNum( Aig_Man_t * p )          { return p->nTruePis + p->nRegs;          }
+static inline int          Saig_ManCoNum( Aig_Man_t * p )          { return p->nTruePos + p->nRegs;          }
 static inline int          Saig_ManRegNum( Aig_Man_t * p )         { return p->nRegs;                        }
 static inline Aig_Obj_t *  Saig_ManLo( Aig_Man_t * p, int i )      { return (Aig_Obj_t *)Vec_PtrEntry(p->vPis, Saig_ManPiNum(p)+i);   }
 static inline Aig_Obj_t *  Saig_ManLi( Aig_Man_t * p, int i )      { return (Aig_Obj_t *)Vec_PtrEntry(p->vPos, Saig_ManPoNum(p)+i);   }

src/aig/saig/saigPhase.c

@@ -800,7 +800,7 @@ Aig_Man_t * Saig_ManPhaseAbstract( Aig_Man_t * p, Vec_Int_t * vInits, int nFrame
         printf( "Print-out finished. Phase assignment is not performed.\n" );
     else if ( nFrames < 2 )
         printf( "The number of frames is less than 2. Phase assignment is not performed.\n" );
-    else if ( pTsi->nCycle == 0 )
+    else if ( pTsi->nCycle == 1 )
         printf( "The cycle of ternary states is trivial. Phase abstraction cannot be done.\n" );
     else if ( pTsi->nCycle % nFrames != 0 )
         printf( "The cycle (%d) is not modulo the number of frames (%d). Phase abstraction cannot be done.\n", pTsi->nCycle, nFrames );
@@ -814,6 +814,75 @@ Aig_Man_t * Saig_ManPhaseAbstract( Aig_Man_t * p, Vec_Int_t * vInits, int nFrame
     return pNew;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Performs automated phase abstraction.]
+
+  Description [Takes the AIG manager and the array of initial states.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManPhaseAbstractAuto( Aig_Man_t * p, int fVerbose )
+{
+    Aig_Man_t * pNew = NULL;
+    Saig_Tsim_t * pTsi;
+    int fPrint = 0;
+    int nFrames;
+    assert( Saig_ManRegNum(p) );
+    assert( Saig_ManPiNum(p) );
+    assert( Saig_ManPoNum(p) );
+    // perform terminary simulation
+    pTsi = Saig_ManReachableTernary( p, NULL );
+    if ( pTsi == NULL )
+        return NULL;
+    // derive information
+    pTsi->nPrefix = Saig_TsiComputePrefix( pTsi, Vec_PtrEntryLast(pTsi->vStates), pTsi->nWords );
+    pTsi->nCycle = Vec_PtrSize(pTsi->vStates) - 1 - pTsi->nPrefix;
+    pTsi->nNonXRegs = Saig_TsiCountNonXValuedRegisters(pTsi, pTsi->nWords);
+    // print statistics
+    if ( fVerbose )
+    {
+        printf( "Prefix = %5d. Cycle = %5d.  Total = %5d. Non-ternary = %5d.\n", 
+            pTsi->nPrefix, pTsi->nCycle, p->nRegs, pTsi->nNonXRegs );
+        if ( pTsi->nNonXRegs < 100 )
+            Saig_TsiPrintTraces( pTsi, pTsi->nWords, pTsi->nPrefix );
+    }
+    nFrames = pTsi->nCycle;
+    if ( fPrint )
+    {
+        printf( "Print-out finished. Phase assignment is not performed.\n" );
+    }
+    else if ( nFrames < 2 )
+    {
+//        printf( "The number of frames is less than 2. Phase assignment is not performed.\n" );
+    }
+    else if ( pTsi->nCycle == 1 )
+    {
+//        printf( "The cycle of ternary states is trivial. Phase abstraction cannot be done.\n" );
+    }
+    else if ( pTsi->nCycle % nFrames != 0 )
+    {
+//        printf( "The cycle (%d) is not modulo the number of frames (%d). Phase abstraction cannot be done.\n", pTsi->nCycle, nFrames );
+    }
+    else if ( pTsi->nNonXRegs == 0 )
+    {
+//        printf( "All registers have X-valued states. Phase abstraction cannot be done.\n" );
+    }
+    else if ( !Saig_ManFindRegisters( pTsi, nFrames, 0, fVerbose ) )
+    {
+//        printf( "There is no registers to abstract with %d frames.\n", nFrames );
+    }
+    else
+        pNew = Saig_ManPerformAbstraction( pTsi, nFrames, fVerbose );
+    Saig_TsiStop( pTsi );
+    if ( pNew == NULL )
+        pNew = Aig_ManDup( p );
+    return pNew;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/base/abci/abcDar.c

@@ -1239,7 +1239,7 @@ PRT( "Time", clock() - clk );
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int nFrames, int fRetimeFirst, int fFraiging, int fVerbose, int fVeryVerbose )
+int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int nFrames, int fPhaseAbstract, int fRetimeFirst, int fRetimeRegs, int fFraiging, int fVerbose, int fVeryVerbose )
 {
     Aig_Man_t * pMan;
     int RetValue;
@@ -1252,7 +1252,7 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int nFrames, int fRetimeFirst, int fFraig
     }
     assert( pMan->nRegs > 0 );
     // perform verification
-    RetValue = Fra_FraigSec( pMan, nFrames, fRetimeFirst, fFraiging, fVerbose, fVeryVerbose );
+    RetValue = Fra_FraigSec( pMan, nFrames, fPhaseAbstract, fRetimeFirst, fRetimeRegs, fFraiging, fVerbose, fVeryVerbose );
     pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
     if ( pNtk->pSeqModel )
     {
@@ -1274,7 +1274,7 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int nFrames, int fRetimeFirst, int fFraig
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fRetimeFirst, int fFraiging, int fVerbose, int fVeryVerbose )
+int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fPhaseAbstract, int fRetimeFirst, int fRetimeRegs, int fFraiging, int fVerbose, int fVeryVerbose )
 {
 //    Fraig_Params_t Params;
     Aig_Man_t * pMan;
@@ -1346,7 +1346,7 @@ int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fRetim
     assert( pMan->nRegs > 0 );
 
     // perform verification
-    RetValue = Fra_FraigSec( pMan, nFrames, fRetimeFirst, fFraiging, fVerbose, fVeryVerbose );
+    RetValue = Fra_FraigSec( pMan, nFrames, fPhaseAbstract, fRetimeFirst, fRetimeRegs, fFraiging, fVerbose, fVeryVerbose );
     Aig_ManStop( pMan );
     return RetValue;
 }
@@ -1909,6 +1909,31 @@ Abc_Ntk_t * Abc_NtkPhaseAbstract( Abc_Ntk_t * pNtk, int nFrames, int fIgnore, in
     return pNtkAig;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Performs BDD-based reachability analysis.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkDarReach( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose )
+{
+    extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose );
+    Aig_Man_t * pMan;
+    pMan = Abc_NtkToDar( pNtk, 0, 0 );
+    pMan->nRegs = Abc_NtkLatchNum(pNtk);
+    pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan); 
+    pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan); 
+    if ( pMan == NULL )
+        return;
+    Aig_ManVerifyUsingBdds( pMan, nBddMax, nIterMax, fPartition, fReorder, fVerbose );
+    Aig_ManStop( pMan );
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///

src/base/main/main.c

@@ -217,7 +217,7 @@ int main( int argc, char * argv[] )
                 break;
         }
     }
-      
+    
     // if the memory should be freed, quit packages
     if ( fStatus < 0 ) 
     {

src/map/if/ifMap.c

@@ -89,7 +89,7 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
         // recompute the parameters of the best cut
         pCut->Delay = If_CutDelay( p, pCut );
 //        assert( pCut->Delay <= pObj->Required + p->fEpsilon );
-        if ( pCut->Delay > pObj->Required + p->fEpsilon )
+        if ( pCut->Delay > pObj->Required + 2*p->fEpsilon )
             printf( "If_ObjPerformMappingAnd(): Warning! Delay of node %d (%f) exceeds the required times (%f).\n", 
                 pObj->Id, pCut->Delay, pObj->Required + p->fEpsilon );
         pCut->Area = (Mode == 2)? If_CutAreaDerefed( p, pCut ) : If_CutAreaFlow( p, pCut );

src/misc/extra/extraBddMisc.c

@@ -281,6 +281,7 @@ void Extra_bddPrint( DdManager * dd, DdNode * F )
 
 //  printf("\n");
 }
+
 /**Function********************************************************************
 
   Synopsis    [Returns the size of the support.]