Experiments with stuck-at fault testing.

1 files changed, 62 insertions, 6 deletions

diff --git a/src/map/if/ifTune.c b/src/map/if/ifTune.c
index dd4c4eb6..1893814e 100644
--- a/src/map/if/ifTune.c
+++ b/src/map/if/ifTune.c
@@ -27,6 +27,17 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+// network types
+typedef enum { 
+    IF_DSD_NONE = 0,               // 0:  unknown
+    IF_DSD_CONST0,                 // 1:  constant
+    IF_DSD_VAR,                    // 2:  variable
+    IF_DSD_AND,                    // 3:  AND
+    IF_DSD_XOR,                    // 4:  XOR
+    IF_DSD_MUX,                    // 5:  MUX
+    IF_DSD_PRIME                   // 6:  PRIME
+} If_DsdType_t;
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -42,9 +53,9 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
-int If_ManStrCheck( char * pStr )
+int If_ManStrCheck( char * pStr, int * pnVars, int * pnObjs )
 {
-    int i, Marks[32] = {0}, MaxVar = 0, MaxDef = 0;
+    int i, Marks[32] = {0}, MaxVar = 0, MaxDef = 0, RetValue = 1;
     for ( i = 0; pStr[i]; i++ )
     {
         if ( pStr[i] == '=' || pStr[i] == ';' || 
@@ -62,16 +73,54 @@ int If_ManStrCheck( char * pStr )
             continue;
         }
         printf( "String \"%s\" contains unrecognized symbol (%c).\n", pStr, pStr[i] );
+        RetValue = 0;
     }
     for ( i = 0; i < MaxDef; i++ )
         if ( Marks[i] == 0 )
-            printf( "String \"%s\" has no symbol (%c).\n", pStr, 'a' + Marks[i] );
+            printf( "String \"%s\" has no symbol (%c).\n", pStr, 'a' + Marks[i] ), RetValue = 0;
     for ( i = 0; i < MaxVar; i++ )
         if ( Marks[i] == 2 )
-            printf( "String \"%s\" defined input symbol (%c).\n", pStr, 'a' + Marks[i] );
+            printf( "String \"%s\" has definition of input variable (%c).\n", pStr, 'a' + Marks[i] ), RetValue = 0;
     for ( i = MaxVar; i < MaxDef; i++ )
         if ( Marks[i] == 1 )
-            printf( "String \"%s\" has no definition for symbol (%c).\n", pStr, 'a' + Marks[i] );
+            printf( "String \"%s\" has no definition for internal variable (%c).\n", pStr, 'a' + Marks[i] ), RetValue = 0;
+    *pnVars = RetValue ? MaxVar : 0;
+    *pnObjs = RetValue ? MaxDef : 0;
+    return RetValue;
+}
+int If_ManStrParse( char * pStr, int nVars, int nObjs, int * pTypes, int * pnFans, int ppFans[][6] )
+{
+    int i, k, n, f;
+    char Next = 0;
+    assert( nVars < nObjs );
+    for ( i = nVars; i < nObjs; i++ )
+    {
+        for ( k = 0; pStr[k]; k++ )
+            if ( pStr[k] == 'a' + i && pStr[k+1] == '=' )
+                break;
+        assert( pStr[k] );
+        if ( pStr[k+2] == '(' )
+            pTypes[i] = IF_DSD_AND, Next = ')';
+        else if ( pStr[k+2] == '[' )
+            pTypes[i] = IF_DSD_XOR, Next = ']';
+        else if ( pStr[k+2] == '<' )
+            pTypes[i] = IF_DSD_MUX, Next = '>';
+        else if ( pStr[k+2] == '{' )
+            pTypes[i] = IF_DSD_PRIME, Next = '}';
+        else assert( 0 );
+        for ( n = k + 3; pStr[n]; n++ )
+            if ( pStr[n] == Next )
+                break;
+        assert( pStr[k] );
+        pnFans[i] = n - k - 3;
+        assert( pnFans[i] > 0 && pnFans[i] <= 6 );
+        for ( f = 0; f < pnFans[i]; f++ )
+        {
+            ppFans[i][f] = pStr[k + 3 + f] - 'a';
+            if ( ppFans[i][f] < 0 || ppFans[i][f] >= nObjs )
+                printf( "Error!\n" );
+        }
+    }
     return 1;
 }
 
@@ -88,8 +137,15 @@ int If_ManStrCheck( char * pStr )
 ***********************************************************************/
 sat_solver * If_ManSatBuild( char * pStr )
 {
+    int nVars, nObjs;
+    int pTypes[32] = {0};
+    int pnFans[32] = {0};
+    int ppFans[32][6] = {{0}};
     sat_solver * pSat = NULL;
-
+    if ( !If_ManStrCheck(pStr, &nVars, &nObjs) )
+        return NULL;
+    if ( !If_ManStrParse(pStr, nVars, nObjs, pTypes, pnFans, ppFans) )
+        return NULL;
     return pSat;
 }