Representing formula used in &fftest as a BLIF file.

src/base/abci/abc.c

@@ -42381,25 +42381,46 @@ int Abc_CommandAbc9FFTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     // read string from file
     if ( pFileName2 )
     {
-        FILE * pFile = fopen( pFileName2, "r" );
-        if ( pFile == NULL )
-        {
-            Abc_Print( -1, "Abc_CommandAbc9FFTest(): File name \"%s\" with formula is invalid.\n", pFileName2 );
-            return 0;
+        if ( !strcmp( Extra_FileNameExtension(pFileName2), "blif" ) )
+        {
+            extern char * Gia_DeriveFormula( Gia_Man_t * pGia, char ** ppNamesIn );
+            Abc_Ntk_t * pNtk2 = Io_Read( pFileName2, Io_ReadFileType(pFileName2), 1, 0 );
+            Abc_Ntk_t * pNtk3 = Abc_NtkStrash( pNtk2, 0, 0, 0 );
+            Gia_Man_t * pGia  = Abc_NtkClpGia( pNtk3 );
+            char ** ppNamesIn = Abc_NtkCollectCioNames( pNtk2, 0 );
+            if ( Gia_ManCoNum(pGia) == 1 )
+                pPars->pFormStr = Gia_DeriveFormula( pGia, ppNamesIn );
+            else
+                printf( "The formula BLIF file contains the network with more one output.\n" );
+            ABC_FREE( ppNamesIn );
+            Gia_ManStop( pGia );
+            Abc_NtkDelete( pNtk2 );
+            Abc_NtkDelete( pNtk3 );
+            if ( pPars->pFormStr == NULL )
+                goto usage;
         }
-        pPars->pFormStr = Extra_FileRead(pFile);
-        fclose( pFile );
-        // skip spaces
-        while ( 1 )
+        else
         {
-            int Len = strlen(pPars->pFormStr);
-            char Char = pPars->pFormStr[Len-1];
-            if ( Char == ' ' || Char == '\n' || Char == '\r' || Char == '\t' || Char == -51 )
-                pPars->pFormStr[Len-1] = '\0';
-            else
-                break;
+            FILE * pFile = fopen( pFileName2, "r" );
+            if ( pFile == NULL )
+            {
+                Abc_Print( -1, "Abc_CommandAbc9FFTest(): File name \"%s\" with formula is invalid.\n", pFileName2 );
+                return 0;
+            }
+            pPars->pFormStr = Extra_FileRead(pFile);
+            fclose( pFile );
+            // skip spaces
+            while ( 1 )
+            {
+                int Len = strlen(pPars->pFormStr);
+                char Char = pPars->pFormStr[Len-1];
+                if ( Char == ' ' || Char == '\n' || Char == '\r' || Char == '\t' || Char == -51 )
+                    pPars->pFormStr[Len-1] = '\0';
+                else
+                    break;
+            }
         }
-        printf( "Using formula \"%s\" form file \"%s\".\n", pPars->pFormStr, pFileName2 );
+        printf( "Using formula \"%s\" from file \"%s\".\n", pPars->pFormStr, pFileName2 );
     }
     if ( pPars->Algo == 0 && pPars->pFormStr == NULL )
     {
@@ -42496,7 +42517,7 @@ usage:
     Abc_Print( -2, "\t-h      : print the command usage\n");
     Abc_Print( -2, "\t<file>  : (optional) file name with input test patterns\n\n");
     Abc_Print( -2, "\t-G file : (optional) file name with the golden model\n\n");
-    Abc_Print( -2, "\t-F file : (optional) file name with the string representing the fault model\n");
+    Abc_Print( -2, "\t-F file : (optional) file name with the fault model in BLIF format\n");
     Abc_Print( -2, "\t-S str  : (optional) string representing the fault model\n");
     Abc_Print( -2, "\t          The following notations are used:\n");
     Abc_Print( -2, "\t            Functional variables: {a,b} (both a and b are always present)\n");
@@ -42513,6 +42534,11 @@ usage:
     Abc_Print( -2, "\t              (((a^p)&(b^q))^r)     complement at the inputs and at the output\n");
     Abc_Print( -2, "\t              (a?(b?~s:r):(b?q:p))  functionally observable fault at the output\n");
     Abc_Print( -2, "\t              (p?(a|b):(a&b))       replace AND by OR\n");
+    Abc_Print( -2, "\t           If the BLIF file is used for the formula with option \'-F\', following rules apply:\n");
+    Abc_Print( -2, "\t              - the network should be combinational and have exactly one primary output\n");
+    Abc_Print( -2, "\t              - input names should have only one character:\n");
+    Abc_Print( -2, "\t                {a, b} (for functional variables)\n");
+    Abc_Print( -2, "\t                {p,q,r,s,t,u,v,w} (for parameter variables)\n");
     return 1;
 }
 

src/sat/bmc/bmcFault.c

@@ -49,6 +49,62 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
+void Gia_DeriveFormula_rec( Gia_Man_t * pGia, char ** ppNamesIn, Vec_Str_t * vStr, int iLit )
+{
+    Gia_Obj_t * pObj = Gia_ManObj( pGia, Abc_Lit2Var(iLit) );
+    int fCompl = Abc_LitIsCompl(iLit);
+    if ( Gia_ObjIsAnd(pObj) )
+    {
+        Vec_StrPush( vStr, '(' );
+        if ( Gia_ObjIsMux(pGia, pObj) )
+        {
+            Gia_DeriveFormula_rec( pGia, ppNamesIn, vStr, Gia_ObjFaninLit0p(pGia, pObj) );
+            Vec_StrPush( vStr, '?' );
+            Gia_DeriveFormula_rec( pGia, ppNamesIn, vStr, Abc_LitNotCond( Gia_ObjFaninLit1p(pGia, pObj), fCompl ) );
+            Vec_StrPush( vStr, ':' );
+            Gia_DeriveFormula_rec( pGia, ppNamesIn, vStr, Abc_LitNotCond( Gia_ObjFaninLit2p(pGia, pObj), fCompl ) );
+        }
+        else
+        {
+            Gia_DeriveFormula_rec( pGia, ppNamesIn, vStr, Abc_LitNotCond( Gia_ObjFaninLit0p(pGia, pObj), fCompl ) );
+            Vec_StrPush( vStr, (char)(Gia_ObjIsXor(pObj) ? '^' : (char)(fCompl ? '|' : '&')) );
+            Gia_DeriveFormula_rec( pGia, ppNamesIn, vStr, Abc_LitNotCond( Gia_ObjFaninLit1p(pGia, pObj), fCompl ) );
+        }
+        Vec_StrPush( vStr, ')' );
+    }
+    else
+    {
+        if ( fCompl ) Vec_StrPush( vStr, '~' );
+        Vec_StrPrintF( vStr, "%s", ppNamesIn[Gia_ObjCioId(pObj)] );
+    }
+}
+char * Gia_DeriveFormula( Gia_Man_t * pGia, char ** ppNamesIn )
+{
+    char * pResult;
+    Vec_Str_t * vStr   = Vec_StrAlloc( 1000 );
+    Gia_Man_t * pMuxes = Gia_ManDupMuxes( pGia, 2 );
+    Gia_Obj_t * pObj   = Gia_ManCo( pGia, 0 );
+    Vec_StrPush( vStr, '(' );
+    Gia_DeriveFormula_rec( pGia, ppNamesIn, vStr, Gia_ObjFaninLit0p(pGia, pObj) );
+    Vec_StrPush( vStr, ')' );
+    Vec_StrPush( vStr, '\0' );
+    Gia_ManStop( pMuxes );
+    pResult = Vec_StrReleaseArray( vStr );
+    Vec_StrFree( vStr );
+    return pResult;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [This procedure sets default parameters.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Gia_ParFfSetDefault( Bmc_ParFf_t * p )
 {
     memset( p, 0, sizeof(Bmc_ParFf_t) );