New command 'testnpn' to compare semi-canonical forms.

6 files changed, 337 insertions, 13 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 7461f443..dede6c51 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -109,6 +109,7 @@ static int Abc_CommandPowerdown              ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandAddBuffs               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 //static int Abc_CommandMerge                  ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandTestDec                ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandTestNpn                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandRewrite                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandRefactor               ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -571,6 +572,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Synthesis",    "addbuffs",      Abc_CommandAddBuffs,         1 );
 //    Cmd_CommandAdd( pAbc, "Synthesis",    "merge",         Abc_CommandMerge,            1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "testdec",       Abc_CommandTestDec,          0 );
+    Cmd_CommandAdd( pAbc, "Synthesis",    "testnpn",       Abc_CommandTestNpn,          0 );
 
     Cmd_CommandAdd( pAbc, "Synthesis",    "rewrite",       Abc_CommandRewrite,          1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "refactor",      Abc_CommandRefactor,         1 );
@@ -4865,6 +4867,73 @@ usage:
     return 1;
 } 
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandTestNpn( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern int Abc_NpnTest( char * pFileName, int NpnType, int fVerbose );
+    char * pFileName;
+    int c;
+    int fVerbose = 0;
+    int NpnType = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Avh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'A':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-A\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            NpnType = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( NpnType < 0 ) 
+                goto usage;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( argc != globalUtilOptind + 1 )
+    {
+        printf( "Input file is not given.\n" );
+        goto usage;
+    }
+    // get the output file name
+    pFileName = argv[globalUtilOptind];
+    // call the testbench
+    Abc_NpnTest( pFileName, NpnType, fVerbose );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: testnpn [-A <num>] [-vh] <file_name>\n" );
+    Abc_Print( -2, "\t           testbench for computing semi-canonical forms of Boolean functions\n" );
+    Abc_Print( -2, "\t-A <num> : semi-caninical form computation algorithm [default = %d]\n", NpnType );
+    Abc_Print( -2, "\t               0: none (reading and writing the file)\n" );
+    Abc_Print( -2, "\t               1: semi-canonical form by counting 1s in cofactors\n" );
+    Abc_Print( -2, "\t               2: semi-canonical form by minimizing truth table value\n" );
+    Abc_Print( -2, "\t               3: exact canonical form (slow for more than 6 variables)\n" );
+    Abc_Print( -2, "\t-v       : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h       : print the command usage\n");
+    return 1;
+} 
+
 
 /**Function*************************************************************
 
diff --git a/src/base/abci/abcDec.c b/src/base/abci/abcDec.c
index 8fce068d..eb17663e 100644
--- a/src/base/abci/abcDec.c
+++ b/src/base/abci/abcDec.c
@@ -42,10 +42,10 @@ ABC_NAMESPACE_IMPL_START
 typedef struct Abc_TtStore_t_  Abc_TtStore_t;
 struct Abc_TtStore_t_ 
 {
-    int      nVars;
-    int      nwords;
-    int      nFuncs;
-    word **  pFuncs;
+    int               nVars;
+    int               nWords;
+    int               nFuncs;
+    word **           pFuncs;
 };
 
 // read/write/flip i-th bit of a bit string table:
@@ -88,8 +88,8 @@ static inline void Abc_TruthWriteHexDigit( FILE * pFile, int HexDigit )
 // read one truth table in hexadecimal
 void Abc_TruthReadHex( word * pTruth, char * pString, int nVars )
 {
-    int nwords = (nVars < 7)? 1 : (1 << (nVars-6));
-    int k, Digit, nDigits = (nwords << 4);
+    int nWords = (nVars < 7)? 1 : (1 << (nVars-6));
+    int k, Digit, nDigits = (nWords << 4);
     char EndSymbol;
     // skip the first 2 symbols if they are "0x"
     if ( pString[0] == '0' && pString[1] == 'x' )
@@ -143,15 +143,15 @@ Abc_TtStore_t * Abc_TruthStoreAlloc( int nVars, int nFuncs )
     int i;
     p = (Abc_TtStore_t *)malloc( sizeof(Abc_TtStore_t) );
     p->nVars  =  nVars;
-    p->nwords = (nVars < 7) ? 1 : (1 << (nVars-6));
+    p->nWords = (nVars < 7) ? 1 : (1 << (nVars-6));
     p->nFuncs =  nFuncs;
     // alloc array of 'nFuncs' pointers to truth tables
     p->pFuncs = (word **)malloc( sizeof(word *) * p->nFuncs );
     // alloc storage for 'nFuncs' truth tables as one chunk of memory
-    p->pFuncs[0] = (word *)calloc( sizeof(word), p->nFuncs * p->nwords );
+    p->pFuncs[0] = (word *)calloc( sizeof(word), p->nFuncs * p->nWords );
     // split it up into individual truth tables
     for ( i = 1; i < p->nFuncs; i++ )
-        p->pFuncs[i] = p->pFuncs[i-1] + p->nwords;
+        p->pFuncs[i] = p->pFuncs[i-1] + p->nWords;
     return p;
 }
 void Abc_TruthStoreFree( Abc_TtStore_t * p )
@@ -338,23 +338,46 @@ void Abc_TruthStoreWrite( char * pFileName, Abc_TtStore_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_TruthStoreTest( char * pFileName )
+Abc_TtStore_t * Abc_TruthStoreLoad( char * pFileName )
 { 
     Abc_TtStore_t * p;
     char * pFileInput  = pFileName;
-    char * pFileOutput = "out.txt";
     int nVars, nTruths;
 
     // figure out how many truth table and how many variables
     Abc_TruthGetParams( pFileInput, &nVars, &nTruths );
     if ( nVars < 2 || nVars > 16 || nTruths == 0 )
-        return;
+        return NULL;
 
     // allocate data-structure
     p = Abc_TruthStoreAlloc( nVars, nTruths );
 
     // read info from file
     Abc_TruthStoreRead( pFileInput, p );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Read truth tables from input file and write them into output file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_TruthStoreTest( char * pFileName )
+{ 
+    Abc_TtStore_t * p;
+    char * pFileInput  = pFileName;
+    char * pFileOutput = "out.txt";
+
+    // read info from file
+    p = Abc_TruthStoreLoad( pFileInput );
+    if ( p == NULL )
+        return;
 
     // write into another file
     Abc_TruthStoreWrite( pFileOutput, p );
diff --git a/src/base/abci/abcNpn.c b/src/base/abci/abcNpn.c
new file mode 100644
index 00000000..c674dbbb
--- /dev/null
+++ b/src/base/abci/abcNpn.c
@@ -0,0 +1,230 @@
+/**CFile****************************************************************
+
+  FileName    [abcNpn.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Procedures for testing and comparing semi-canonical forms.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcNpn.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "misc/extra/extra.h"
+#include "misc/vec/vec.h"
+
+#include "bool/kit/kit.h"
+#include "bool/lucky/lucky.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+ 
+// semi-canonical form types
+// 0 - none
+// 1 - based on counting 1s in cofactors
+// 2 - based on minimum truth table value
+// 3 - exact NPN
+
+// data-structure to store a bunch of truth tables
+typedef struct Abc_TtStore_t_  Abc_TtStore_t;
+struct Abc_TtStore_t_ 
+{
+    int               nVars;
+    int               nWords;
+    int               nFuncs;
+    word **           pFuncs;
+};
+
+extern Abc_TtStore_t * Abc_TruthStoreLoad( char * pFileName );
+extern void            Abc_TruthStoreFree( Abc_TtStore_t * p );
+extern void            Abc_TruthStoreTest( char * pFileName );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of unique truth tables.]
+
+  Description []
+               
+  SideEffects [] 
+
+  SeeAlso     []
+
+***********************************************************************/
+int nWords = 0; // unfortunate global variable
+int Abc_TruthCompare( word * p1, word * p2 ) { return memcmp(p1, p2, sizeof(word) * nWords); }
+int Abc_TruthNpnCountUnique( Abc_TtStore_t * p )
+{
+    int i, nUnique;
+    // sort them by value
+    nWords = p->nWords;
+    assert( nWords > 0 );
+    qsort( (void *)p->pFuncs[0], p->nFuncs, nWords * sizeof(word), (int(*)(const void *,const void *))Abc_TruthCompare );
+    // count the number of unqiue functions
+    nUnique = p->nFuncs;
+    for ( i = 1; i < p->nFuncs; i++ )
+        if ( !memcmp( p->pFuncs[i-1], p->pFuncs[i], sizeof(word) * nWords ) )
+            nUnique--;
+    return nUnique;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Apply decomposition to the truth table.]
+
+  Description [Returns the number of AIG nodes.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_TruthNpnPerform( Abc_TtStore_t * p, int NpnType, int fVerbose )
+{
+    short pStore[16];
+    char pCanonPerm[16];
+    unsigned pAux[2048];
+
+    clock_t clk = clock();
+    int i, nFuncs = 0;
+
+    char * pAlgoName = NULL;
+    if ( NpnType == 1 )
+        pAlgoName = "counting 1s  ";
+    else if ( NpnType == 2 )
+        pAlgoName = "minimizing TT";
+    else if ( NpnType == 3 )
+        pAlgoName = "exact NPN    ";
+
+    assert( p->nVars <= 16 );
+    if ( pAlgoName )
+        printf( "Applying %-10s to %8d func%s of %2d vars...  ",  
+            pAlgoName, p->nFuncs, (p->nFuncs == 1 ? "":"s"), p->nVars );
+    if ( fVerbose )
+        printf( "\n" );
+
+    if ( NpnType == 1 )
+    {
+        for ( i = 0; i < p->nFuncs; i++ )
+        {
+            if ( fVerbose )
+                printf( "%7d : ", i );
+            Kit_TruthSemiCanonicize( (unsigned *)p->pFuncs[i], pAux, p->nVars, pCanonPerm, pStore );
+            if ( fVerbose )
+                Extra_PrintHex( stdout, (unsigned *)p->pFuncs[i], p->nVars ), printf( "\n" );
+        }
+    }
+    else if ( NpnType == 2 )
+    {
+        for ( i = 0; i < p->nFuncs; i++ )
+        {
+            if ( fVerbose )
+                printf( "%7d : ", i );
+            Kit_TruthSemiCanonicize_new( (unsigned *)p->pFuncs[i], pAux, p->nVars, pCanonPerm );
+            if ( fVerbose )
+                Extra_PrintHex( stdout, (unsigned *)p->pFuncs[i], p->nVars ), printf( "\n" );
+        }
+    }
+    else if ( NpnType == 3 )
+    {
+        int * pComp = Extra_GreyCodeSchedule( p->nVars );
+        int * pPerm = Extra_PermSchedule( p->nVars );
+        if ( p->nVars == 6 )
+        {
+            for ( i = 0; i < p->nFuncs; i++ )
+            {
+                if ( fVerbose )
+                    printf( "%7d : ", i );
+                *((word *)p->pFuncs[i]) = Extra_Truth6Minimum( *((word *)p->pFuncs[i]), pComp, pPerm );
+                if ( fVerbose )
+                    Extra_PrintHex( stdout, (unsigned *)p->pFuncs[i], p->nVars ), printf( "\n" );
+            }
+        }
+        else
+            printf( "This feature only works for 6-variable functions.\n" );
+        ABC_FREE( pComp );
+        ABC_FREE( pPerm );
+    }
+    else assert( 0 );
+
+    clk = clock() - clk;
+    printf( "Classes =%9d  ", Abc_TruthNpnCountUnique(p) );
+    Abc_PrintTime( 1, "Time", clk );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Apply decomposition to truth tables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_TruthNpnTest( char * pFileName, int NpnType, int fVerbose )
+{
+    Abc_TtStore_t * p;
+
+    // read info from file
+    p = Abc_TruthStoreLoad( pFileName );
+    if ( p == NULL )
+        return;
+
+    // consider functions from the file
+    Abc_TruthNpnPerform( p, NpnType, fVerbose );
+
+    // delete data-structure
+    Abc_TruthStoreFree( p );
+//    printf( "Finished computing canonical forms for functions from file \"%s\".\n", pFileName );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Testbench for decomposition algorithms.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NpnTest( char * pFileName, int NpnType, int fVerbose )
+{
+    if ( fVerbose )
+        printf( "Using truth tables from file \"%s\"...\n", pFileName );
+    if ( NpnType == 0 )
+        Abc_TruthStoreTest( pFileName );
+    else if ( NpnType >= 1 && NpnType <= 3 )
+        Abc_TruthNpnTest( pFileName, NpnType, fVerbose );
+    else
+        printf( "Unknown canonical form value (%d).\n", NpnType );
+    fflush( stdout );
+    return 0;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
index b88c253c..e25e497d 100644
--- a/src/base/abci/module.make
+++ b/src/base/abci/module.make
@@ -35,6 +35,7 @@ SRC +=    src/base/abci/abc.c \
     src/base/abci/abcMiter.c \
     src/base/abci/abcMulti.c \
     src/base/abci/abcNtbdd.c \
+    src/base/abci/abcNpn.c \
     src/base/abci/abcNpnSave.c \
     src/base/abci/abcOdc.c \
     src/base/abci/abcOrder.c \
diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h
index 50172691..f198c183 100644
--- a/src/misc/extra/extra.h
+++ b/src/misc/extra/extra.h
@@ -203,6 +203,7 @@ extern void        Extra_BubbleSort( int Order[], int Costs[], int nSize, int fI
 /* complementation/permutation generation */
 extern int *       Extra_GreyCodeSchedule( int n );
 extern int *       Extra_PermSchedule( int n );
+extern word        Extra_Truth6Minimum( word t, int * pComp, int * pPerm );
 
 /*=== extraUtilCanon.c ========================================================*/
 
diff --git a/src/misc/extra/extraUtilMisc.c b/src/misc/extra/extraUtilMisc.c
index 729d0c04..e484bcb2 100644
--- a/src/misc/extra/extraUtilMisc.c
+++ b/src/misc/extra/extraUtilMisc.c
@@ -2283,7 +2283,7 @@ static inline word Extra_Truth6ChangePhase( word t, int v )
     assert( v < 6 );
     return ((t & ~Truth6[v]) << (1 << v)) | ((t & Truth6[v]) >> (1 << v));
 }
-static inline word Extra_Truth6Minimum( word t, int * pComp, int * pPerm )
+word Extra_Truth6Minimum( word t, int * pComp, int * pPerm )
 {
     word tMin = ~(word)0;
     word tCur, tTemp1, tTemp2;