Changes to PDR to compute f-inf clauses and import invariant (or clauses) as a network.

4 files changed, 221 insertions, 47 deletions

diff --git a/src/base/wlc/module.make b/src/base/wlc/module.make
index f3aa6871..7bc7aa39 100644
--- a/src/base/wlc/module.make
+++ b/src/base/wlc/module.make
@@ -1,4 +1,5 @@
 SRC +=    src/base/wlc/wlcAbs.c \
+    src/base/wlc/wlcAbc.c \
     src/base/wlc/wlcBlast.c \
     src/base/wlc/wlcCom.c \
     src/base/wlc/wlcNtk.c \
diff --git a/src/base/wlc/wlcAbc.c b/src/base/wlc/wlcAbc.c
new file mode 100644
index 00000000..0bf27f7b
--- /dev/null
+++ b/src/base/wlc/wlcAbc.c
@@ -0,0 +1,154 @@
+/**CFile****************************************************************
+
+  FileName    [wlcAbc.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Verilog parser.]
+
+  Synopsis    [Parses several flavors of word-level Verilog.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - August 22, 2014.]
+
+  Revision    [$Id: wlcAbc.c,v 1.00 2014/09/12 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "wlc.h"
+#include "base/abc/abc.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, int fVerbose )
+{
+    Wlc_Obj_t * pObj;
+    int i, k, nNum, nRange, nBits = 0;
+    Wlc_NtkForEachCi( pNtk, pObj, i )
+    {
+        if ( pObj->Type != WLC_OBJ_FO )
+            continue;
+        nRange = Wlc_ObjRange(pObj);
+        for ( k = 0; k < nRange; k++ )
+        {
+            nNum = Vec_IntEntry(vInv, nBits + k);
+            if ( nNum )
+                break;
+        }
+        if ( k == nRange )
+        {
+            nBits += nRange;
+            continue;
+        }
+        printf( "%s[%d:%d] : ", Wlc_ObjName(pNtk, Wlc_ObjId(pNtk, pObj)), pObj->End, pObj->Beg );
+        for ( k = 0; k < nRange; k++ )
+        {
+            nNum = Vec_IntEntry( vInv, nBits + k );
+            if ( nNum == 0 )
+                continue;
+            printf( "  [%d] -> %d", k, nNum );
+        }
+        printf( "\n");
+        nBits += nRange;
+    }
+    //printf( "%d %d\n", Vec_IntSize(vInv), nBits );
+    assert( Vec_IntSize(vInv) == nBits );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, Vec_Str_t * vSop, int fVerbose )
+{
+    Wlc_Obj_t * pObj;
+    int i, k, nNum, nRange, nBits = 0;
+    Abc_Ntk_t * pMainNtk = NULL;
+    Abc_Obj_t * pMainObj, * pMainTemp;
+    char Buffer[5000];
+    // start the network
+    pMainNtk = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP, 1 );
+    // duplicate the name and the spec
+    pMainNtk->pName = Extra_UtilStrsav(pNtk->pName);
+    // create primary inputs
+    Wlc_NtkForEachCi( pNtk, pObj, i )
+    {
+        if ( pObj->Type != WLC_OBJ_FO )
+            continue;
+        nRange = Wlc_ObjRange(pObj);
+        for ( k = 0; k < nRange; k++ )
+        {
+            nNum = Vec_IntEntry(vInv, nBits + k);
+            if ( nNum )
+                break;
+        }
+        if ( k == nRange )
+        {
+            nBits += nRange;
+            continue;
+        }
+        //printf( "%s[%d:%d] : ", Wlc_ObjName(pNtk, Wlc_ObjId(pNtk, pObj)), pObj->End, pObj->Beg );
+        for ( k = 0; k < nRange; k++ )
+        {
+            nNum = Vec_IntEntry( vInv, nBits + k );
+            if ( nNum == 0 )
+                continue;
+            //printf( "  [%d] -> %d", k, nNum );
+            pMainObj = Abc_NtkCreatePi( pMainNtk );
+            sprintf( Buffer, "%s[%d]", Wlc_ObjName(pNtk, Wlc_ObjId(pNtk, pObj)), k );
+            Abc_ObjAssignName( pMainObj, Buffer, NULL );
+
+        }
+        //printf( "\n");
+        nBits += nRange;
+    }
+    //printf( "%d %d\n", Vec_IntSize(vInv), nBits );
+    assert( Vec_IntSize(vInv) == nBits );
+    // create node
+    pMainObj = Abc_NtkCreateNode( pMainNtk );
+    Abc_NtkForEachPi( pMainNtk, pMainTemp, i )
+        Abc_ObjAddFanin( pMainObj, pMainTemp );
+    pMainObj->pData = Abc_SopRegister( (Mem_Flex_t *)pMainNtk->pManFunc, Vec_StrArray(vSop) );
+    // create PO
+    pMainTemp = Abc_NtkCreatePo( pMainNtk );
+    Abc_ObjAddFanin( pMainTemp, pMainObj );
+    Abc_ObjAssignName( pMainTemp, "inv", NULL );
+    return pMainNtk;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/wlc/wlcBlast.c b/src/base/wlc/wlcBlast.c
index 426d9bbf..f3e0af8a 100644
--- a/src/base/wlc/wlcBlast.c
+++ b/src/base/wlc/wlcBlast.c
@@ -1111,52 +1111,6 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds )
     return pNew;
 }
 
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, int fVerbose )
-{
-    Wlc_Obj_t * pObj;
-    int i, k, nNum, nRange, nBits = 0;
-    Wlc_NtkForEachCi( pNtk, pObj, i )
-    {
-        if ( pObj->Type != WLC_OBJ_FO )
-            continue;
-        nRange = Wlc_ObjRange(pObj);
-        for ( k = 0; k < nRange; k++ )
-        {
-            nNum = Vec_IntEntry(vInv, nBits + k);
-            if ( nNum )
-                break;
-        }
-        if ( k == nRange )
-        {
-            nBits += nRange;
-            continue;
-        }
-        printf( "%s[%d:%d] : ", Wlc_ObjName(pNtk, Wlc_ObjId(pNtk, pObj)), pObj->End, pObj->Beg );
-        for ( k = 0; k < nRange; k++ )
-        {
-            nNum = Vec_IntEntry( vInv, nBits + k );
-            if ( nNum == 0 )
-                continue;
-            printf( "  [%d] -> %d", k, nNum );
-        }
-        printf( "\n");
-        nBits += nRange;
-    }
-    //printf( "%d %d\n", Vec_IntSize(vInv), nBits );
-    assert( Vec_IntSize(vInv) == nBits );
-}
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c
index 3f8cc492..1584e346 100644
--- a/src/base/wlc/wlcCom.c
+++ b/src/base/wlc/wlcCom.c
@@ -33,6 +33,7 @@ static int  Abc_CommandWriteWlc ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int  Abc_CommandPs       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int  Abc_CommandBlast    ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int  Abc_CommandPsInv    ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int  Abc_CommandGetInv   ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int  Abc_CommandTest     ( 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;                      }
@@ -40,6 +41,8 @@ static inline void        Wlc_AbcFreeNtk( Abc_Frame_t * pAbc )
 static inline void        Wlc_AbcUpdateNtk( Abc_Frame_t * pAbc, Wlc_Ntk_t * pNtk )  { Wlc_AbcFreeNtk(pAbc); pAbc->pAbcWlc = pNtk;             }
 
 static inline Vec_Int_t * Wlc_AbcGetInv( Abc_Frame_t * pAbc )                       { return pAbc->pAbcWlcInv;                                }
+static inline Vec_Int_t * Wlc_AbcGetCnf( Abc_Frame_t * pAbc )                       { return pAbc->pAbcWlcCnf;                                }
+static inline Vec_Str_t * Wlc_AbcGetStr( Abc_Frame_t * pAbc )                       { return pAbc->pAbcWlcStr;                                }
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -63,6 +66,7 @@ void Wlc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Word level", "%ps",         Abc_CommandPs,        0 );
     Cmd_CommandAdd( pAbc, "Word level", "%blast",      Abc_CommandBlast,     0 );
     Cmd_CommandAdd( pAbc, "Word level", "%psinv",      Abc_CommandPsInv,     0 );
+    Cmd_CommandAdd( pAbc, "Word level", "%getinv",     Abc_CommandGetInv,    0 );
     Cmd_CommandAdd( pAbc, "Word level", "%test",       Abc_CommandTest,      0 );
 }
 
@@ -421,7 +425,68 @@ int Abc_CommandPsInv( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
     usage:
     Abc_Print( -2, "usage: %%psinv [-vh]\n" );
-    Abc_Print( -2, "\t         prints inductive invariant statistics\n" );
+    Abc_Print( -2, "\t         prints statistics for inductive invariant\n" );
+    Abc_Print( -2, "\t         (in the case of \'sat\' or \'undecided\', inifity clauses are used)\n" );
+    Abc_Print( -2, "\t-v     : toggle printing verbose information [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_CommandGetInv( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, Vec_Str_t * vSop, int fVerbose );
+    Abc_Ntk_t * pMainNtk;
+    Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
+    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 ( pNtk == NULL )
+    {
+        Abc_Print( 1, "Abc_CommandGetInv(): There is no current design.\n" );
+        return 0;
+    }
+    if ( Wlc_AbcGetNtk(pAbc) == NULL )
+    {
+        Abc_Print( 1, "Abc_CommandGetInv(): There is no saved invariant.\n" );
+        return 0;
+    }
+    if ( Wlc_AbcGetInv(pAbc) == NULL )
+    {
+        Abc_Print( 1, "Abc_CommandGetInv(): Invariant is not available.\n" );
+        return 0;
+    }
+    // derive the network
+    pMainNtk = Wlc_NtkGetInv( pNtk, Wlc_AbcGetInv(pAbc), Wlc_AbcGetStr(pAbc), fVerbose );
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pMainNtk );
+    return 0;
+    usage:
+    Abc_Print( -2, "usage: %%getinv [-vh]\n" );
+    Abc_Print( -2, "\t         places invariant found by PDR as the current network in the main-space\n" );
+    Abc_Print( -2, "\t         (in the case of \'sat\' or \'undecided\', inifity clauses are used)\n" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;