Experiments with word-level data structures.

abclib.dsp

@@ -1131,6 +1131,14 @@ SOURCE=.\src\base\wln\wlnBlast.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\base\wln\wlnCom.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\wln\wlnGuide.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\base\wln\wlnMem.c
 # End Source File
 # Begin Source File

src/base/main/mainInit.c

@@ -49,6 +49,8 @@ extern void Scl_Init( Abc_Frame_t * pAbc );
 extern void Scl_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 );
+extern void Wln_End( Abc_Frame_t * pAbc );
 extern void Bac_Init( Abc_Frame_t * pAbc );
 extern void Bac_End( Abc_Frame_t * pAbc );
 extern void Cba_Init( Abc_Frame_t * pAbc );
@@ -116,6 +118,7 @@ void Abc_FrameInit( Abc_Frame_t * pAbc )
     Load_Init( pAbc );
     Scl_Init( pAbc );
     Wlc_Init( pAbc );
+    Wln_Init( pAbc );
     Bac_Init( pAbc );
     Cba_Init( pAbc );
     Pla_Init( pAbc );
@@ -156,6 +159,7 @@ void Abc_FrameEnd( Abc_Frame_t * pAbc )
     Load_End( pAbc );
     Scl_End( pAbc );
     Wlc_End( pAbc );
+    Wln_End( pAbc );
     Bac_End( pAbc );
     Cba_End( pAbc );
     Pla_End( pAbc );

src/base/wln/module.make

 SRC +=    src/base/wln/wln.c \
     src/base/wln/wlnBlast.c \
+    src/base/wln/wlnCom.c \
+    src/base/wln/wlnGuide.c \
     src/base/wln/wlnMem.c \
     src/base/wln/wlnNdr.c \
     src/base/wln/wlnNtk.c \

src/base/wln/wlnGuide.c

+/**CFile****************************************************************
+
+  FileName    [wln.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Word-level network.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - September 23, 2018.]
+
+  Revision    [$Id: wln.c,v 1.00 2018/09/23 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "wln.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Wln_ReadGuidance( char * pFileName, Abc_Nam_t * p )
+{
+    char Buffer[1000] = {'\\'}, * pBuffer = Buffer+1;
+    Vec_Int_t * vTokens = Vec_IntAlloc( 100 );
+    FILE * pFile = fopen( pFileName, "rb" );
+    while ( fscanf( pFile, "%s", pBuffer ) == 1 )
+    {
+        if ( pBuffer[(int)strlen(pBuffer)-1] == '\r' )
+            pBuffer[(int)strlen(pBuffer)-1] = 0;
+        if ( !strcmp(pBuffer, "prove") && Vec_IntSize(vTokens) % 4 == 3 ) // account for "property"
+            Vec_IntPush( vTokens, -1 );
+        if ( Vec_IntSize(vTokens) % 4 == 2 || Vec_IntSize(vTokens) % 4 == 3 )
+            Vec_IntPush( vTokens, Abc_NamStrFindOrAdd(p, Buffer, NULL) );
+        else
+            Vec_IntPush( vTokens, Abc_NamStrFindOrAdd(p, pBuffer, NULL) );
+    }
+    fclose( pFile );
+    if ( Vec_IntSize(vTokens) % 4 == 3 ) // account for "property"
+        Vec_IntPush( vTokens, -1 );
+    assert( Vec_IntSize(vTokens) % 4 == 0 );
+    return vTokens;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+

src/base/wln/wlnRead.c

@@ -78,6 +78,8 @@ struct Rtl_Ntk_t_
 static inline int         Rtl_LibNtkNum( Rtl_Lib_t * pLib )                { return Vec_PtrSize(pLib->vNtks);                  }
 static inline Rtl_Ntk_t * Rtl_LibNtk( Rtl_Lib_t * pLib, int i )            { return (Rtl_Ntk_t *)Vec_PtrEntry(pLib->vNtks, i); }
 static inline Rtl_Ntk_t * Rtl_LibTop( Rtl_Lib_t * pLib )                   { return Rtl_LibNtk( pLib, Rtl_LibNtkNum(pLib)-1 ); }
+static inline char *      Rtl_LibStr( Rtl_Lib_t * pLib, int h )            { return Abc_NamStr(pLib->pManName, h);             }
+static inline int         Rtl_LibStrId( Rtl_Lib_t * pLib, char * s )       { return Abc_NamStrFind(pLib->pManName, s);         }
 
 static inline Rtl_Ntk_t * Rtl_NtkModule( Rtl_Ntk_t * p, int i )            { return Rtl_LibNtk( p->pLib, i );                  }
 
@@ -254,6 +256,50 @@ void Rtl_NtkPrintStats( Rtl_Ntk_t * p, int nNameSymbs )
   SeeAlso     []
 
 ***********************************************************************/
+void Rtl_NtkPrintHieStats( Rtl_Ntk_t * p, int nOffset )
+{
+    Vec_Int_t * vFound = Vec_IntAlloc( 100 );
+    int i, * pCell;
+    for ( i = 0; i < 5*(nOffset-1); i++ )
+        printf( " " );
+    if ( nOffset )
+        printf( "|--> " );
+    printf( "%s\n", Rtl_NtkName(p) );
+    Rtl_NtkForEachCell( p, pCell, i )
+        if ( Rtl_CellModule(pCell) >= ABC_INFINITY )
+        {
+            Rtl_Ntk_t * pModel = Rtl_NtkModule( p, Rtl_CellModule(pCell)-ABC_INFINITY );
+            assert( pCell[6] == pModel->nInputs+pModel->nOutputs );
+            if ( Vec_IntFind(vFound, pModel->NameId) >= 0 )
+                continue;
+            Vec_IntPush( vFound, pModel->NameId );
+            Rtl_NtkPrintHieStats( pModel, nOffset+1 );
+        }
+    Vec_IntFree( vFound );
+}
+void Rtl_LibPrintHieStats( Rtl_Lib_t * p )
+{
+    Rtl_Ntk_t * pNtk; int i;
+    printf( "Hierarchy found in \"%s\":\n", p->pSpec );
+    Vec_PtrForEachEntry( Rtl_Ntk_t *, p->vNtks, pNtk, i )
+    {
+        printf( "\n" );
+        printf( "MODULE %d: ", i );
+        Rtl_NtkPrintHieStats( pNtk, 0 );  
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 Rtl_Lib_t * Rtl_LibAlloc()
 {
     Rtl_Lib_t * p = ABC_CALLOC( Rtl_Lib_t, 1 );
@@ -1398,6 +1444,7 @@ Rtl_Lib_t * Rtl_LibReadFile( char * pFileName, char * pFileSpec )
             i = Rtl_NtkReadAttribute2( p, i+1 );
     Rtl_LibSetParents( p );
     Rtl_LibReorderModules( p );
+    Rtl_LibOrderWires( p );
     return p;
 }
 
@@ -1733,7 +1780,7 @@ char * Rtl_ShortenName( char * pName, int nSize )
         return pName;
     Buffer[0] = 0;
     strcat( Buffer, pName );
-    Buffer[nSize-4] = ' ';
+    //Buffer[nSize-4] = ' ';
     Buffer[nSize-3] = '.';
     Buffer[nSize-2] = '.';
     Buffer[nSize-1] = '.';
@@ -1941,6 +1988,7 @@ void Rtl_NtkBlastPrepareInputs( Rtl_Ntk_t * p, int * pCell )
 }
 void Rtl_NtkBlast2_rec( Rtl_Ntk_t * p, int iBit, int * pDriver )
 {
+    //char * pName = Rtl_NtkName(p);
     assert( pDriver[0] != -1 );
     if ( pDriver[0] == -3 )
     {
@@ -1981,6 +2029,7 @@ Gia_Man_t * Rtl_NtkBlast2( Rtl_Ntk_t * p )
     int i, b, nBits = Rtl_NtkRangeWires( p );
     char Buffer[100]; static int counter = 0;
     Vec_IntFill( &p->vLits, nBits, -1 );
+printf( "Blasting %s...\r", Rtl_NtkName(p) );
     Rtl_NtkMapWires( p, 0 );
     Rtl_NtkBlastMap( p, nBits );
     assert( p->pGia == NULL );
@@ -2066,11 +2115,11 @@ finish:
     //Rtl_LibBlast( pLib );
     Rtl_LibBlast2( pLib );
 }
-void Rtl_LibSolve( Rtl_Lib_t * pLib )
+void Rtl_LibSolve( Rtl_Lib_t * pLib, void * pNtk )
 {
     extern Gia_Man_t * Cec4_ManSimulateTest3( Gia_Man_t * p, int nBTLimit, int fVerbose );
     abctime clk = Abc_Clock(); int Status;
-    Rtl_Ntk_t * pTop = Rtl_LibTop( pLib );
+    Rtl_Ntk_t * pTop = pNtk ? (Rtl_Ntk_t *)pNtk : Rtl_LibTop( pLib );
     Gia_Man_t * pSwp = Cec4_ManSimulateTest3( pTop->pGia, 1000000, 0 );
     int RetValue = Gia_ManAndNum(pSwp) == 0;
     Gia_ManStop( pSwp );
@@ -2092,6 +2141,83 @@ void Rtl_LibSolve( Rtl_Lib_t * pLib )
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Wln_SolveEqual( Rtl_Lib_t * p, int iNtk1, int iNtk2 )
+{
+    Rtl_Ntk_t * pNtk1 = Rtl_LibNtk( p, iNtk1 );
+    Rtl_Ntk_t * pNtk2 = Rtl_LibNtk( p, iNtk2 );
+    printf( "Proving equivalence of \"%s\" and \"%s\".\n", Rtl_NtkName(pNtk1), Rtl_NtkName(pNtk2) );
+/*
+    if ( Gia_ManCiNum(pNtk1->pGia) != Gia_ManCiNum(pNtk2->pGia) || 
+         Gia_ManCoNum(pNtk1->pGia) != Gia_ManCoNum(pNtk2->pGia) )
+    {
+        printf( "The number of inputs/outputs does not match.\n" );
+    }
+    else
+    {
+        int Status = Cec_ManVerifyTwo( pNtk1->pGia, pNtk2->pGia, 0 );
+        if ( Status == 1 )
+            printf( "The networks are equivalence.\n" );
+        else
+            printf( "The networks are NOT equivalent.\n" );
+    }
+*/
+}
+void Wln_SolveInverse( Rtl_Lib_t * p, int iNtk1, int iNtk2 )
+{
+    Rtl_Ntk_t * pNtk1 = Rtl_LibNtk( p, iNtk1 );
+    Rtl_Ntk_t * pNtk2 = Rtl_LibNtk( p, iNtk2 );
+    printf( "Proving inverse equivalence of \"%s\" and \"%s\".\n", Rtl_NtkName(pNtk1), Rtl_NtkName(pNtk2) );
+}
+void Wln_SolveProperty( Rtl_Lib_t * p, int iNtk )
+{
+    Rtl_Ntk_t * pNtk = Rtl_LibNtk( p, iNtk );
+    printf( "Proving property \"%s\".\n", Rtl_NtkName(pNtk) );
+    Rtl_LibSolve( p, pNtk );
+}
+void Wln_SolveWithGuidance( char * pFileName, Rtl_Lib_t * p )
+{
+    extern Vec_Int_t * Wln_ReadGuidance( char * pFileName, Abc_Nam_t * p );
+    Vec_Int_t * vGuide = Wln_ReadGuidance( pFileName, p->pManName ); int i;
+    Vec_IntFillExtra( p->vMap, Abc_NamObjNumMax(p->pManName), -1 );
+    Rtl_LibBlast2( p );
+    for ( i = 0; i < Vec_IntSize(vGuide); i += 4 )
+    {
+        int Prove = Vec_IntEntry( vGuide, i+0 );
+        int Type  = Vec_IntEntry( vGuide, i+1 );
+        int Name1 = Vec_IntEntry( vGuide, i+2 );
+        int Name2 = Vec_IntEntry( vGuide, i+3 );
+        int iNtk1 = Rtl_LibFindModule( p, Name1 );
+        int iNtk2 = Name2 == -1 ? -1 : Rtl_LibFindModule( p, Name2 );
+        if ( Prove != Rtl_LibStrId(p, "prove") )
+            printf( "Unknown task in line %d.\n", i/4 );
+        else if ( iNtk1 == -1 )
+            printf( "Network %s cannot be found in this design.\n", Rtl_LibStr(p, Name1) );
+        else
+        {
+            if ( Type == Rtl_LibStrId(p, "equal") )
+                Wln_SolveEqual( p, iNtk1, iNtk2 );
+            else if ( Type == Rtl_LibStrId(p, "inverse") )
+                Wln_SolveInverse( p, iNtk1, iNtk2 );
+            else if ( Type == Rtl_LibStrId(p, "property") )
+                Wln_SolveProperty( p, iNtk1 );
+            continue;
+        }
+        break;
+    }
+    Vec_IntFree( vGuide );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/base/wln/wlnRtl.c

@@ -145,7 +145,7 @@ Rtl_Lib_t * Wln_ReadSystemVerilog( char * pFileName, char * pTopModule, int fCol
         return Rtl_LibReadFile( pFileName, pFileName );
     sprintf( Command, "%s -qp \"read_verilog %s%s; hierarchy %s%s; %sproc; write_rtlil %s\"", 
         Wln_GetYosysName(), fSVlog ? "-sv ":"", pFileName, 
-        pTopModule ? "-top " : "-auto-top", 
+        pTopModule ? "-top "    : "", 
         pTopModule ? pTopModule : "", 
         fCollapse ? "flatten; " : "",
         pFileTemp );