Adding features related to the communication bridge.

src/base/abci/abc.c

@@ -379,6 +379,12 @@ extern int Abc_CommandAbcLivenessToSafetyWithLTL( Abc_Frame_t * pAbc, int argc,
 ***********************************************************************/
 void Abc_FrameReplaceCex( Abc_Frame_t * pAbc, Abc_Cex_t ** ppCex )
 {
+    // update bridge
+    if ( Abc_FrameIsBridgeMode() )
+    {
+        extern int Gia_ManToBridgeResult( FILE * pFile, int Result, Abc_Cex_t * pCex );
+        Gia_ManToBridgeResult( stdout, pAbc->Status, *ppCex );
+    }
     // update CEX
     ABC_FREE( pAbc->pCex );
     pAbc->pCex = *ppCex;
@@ -23473,8 +23479,7 @@ int Abc_CommandAbc9Equiv3( Abc_Frame_t * pAbc, int argc, char ** argv )
 //    else
 //        pAbc->Status = Ssw_RarSignalFilterGia2( pAbc->pGia, nFrames, nWords, nBinSize, nRounds, TimeOut, fUseCex? pAbc->pCex: NULL, fLatchOnly, fVerbose );
 //    pAbc->nFrames = pAbc->pGia->pCexSeq->iFrame;
-    if ( pAbc->pGia->pCexSeq )
+    Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
-        Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
     return 0;
 
 usage:

src/base/main/main.c

@@ -35,7 +35,7 @@ ABC_NAMESPACE_IMPL_START
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
- 
+
 static int TypeCheck( Abc_Frame_t * pAbc, const char * s);
 
 ////////////////////////////////////////////////////////////////////////
@@ -111,7 +111,7 @@ int Abc_RealMain( int argc, char * argv[] )
     sprintf( sWriteCmd, "write" );
     
     Extra_UtilGetoptReset();
-    while ((c = Extra_UtilGetopt(argc, argv, "c:hf:F:o:st:T:x")) != EOF) {
+    while ((c = Extra_UtilGetopt(argc, argv, "c:hf:F:o:st:T:xb")) != EOF) {
         switch(c) {
             case 'c':
                 strcpy( sCommandUsr, globalUtilOptarg );
@@ -177,10 +177,20 @@ int Abc_RealMain( int argc, char * argv[] )
                 fBatch = 1;
                 break;
                 
+            case 'b':
+                Abc_FrameSetBridgeMode();
+                break;
+                
             default:
                 goto usage;
         }
     }
+
+    if ( Abc_FrameIsBridgeMode() )
+    {
+        extern Gia_Man_t * Gia_ManFromBridge( FILE * pFile, Vec_Int_t ** pvInit );
+        pAbc->pGia = Gia_ManFromBridge( stdin, NULL );
+    }
     
     if ( fBatch )
     {

src/base/main/main.h

@@ -104,6 +104,8 @@ extern ABC_DLL void *          Abc_FrameReadManDd();
 extern ABC_DLL void *          Abc_FrameReadManDec();                    
 extern ABC_DLL char *          Abc_FrameReadFlag( char * pFlag ); 
 extern ABC_DLL int             Abc_FrameIsFlagEnabled( char * pFlag );
+extern ABC_DLL int             Abc_FrameIsBridgeMode();
+extern ABC_DLL void            Abc_FrameSetBridgeMode();
 
 extern ABC_DLL int             Abc_FrameReadBmcFrames( Abc_Frame_t * p );              
 extern ABC_DLL int             Abc_FrameReadProbStatus( Abc_Frame_t * p );              

src/base/main/mainFrame.c

@@ -78,6 +78,9 @@ void        Abc_FrameSetLibVer( void * pLib )                { s_GlobalFrame->pL
 void        Abc_FrameSetFlag( char * pFlag, char * pValue )  { Cmd_FlagUpdateValue( s_GlobalFrame, pFlag, pValue );         } 
 void        Abc_FrameSetCex( Abc_Cex_t * pCex )              { ABC_FREE( s_GlobalFrame->pCex ); s_GlobalFrame->pCex = pCex; }
 
+int         Abc_FrameIsBridgeMode()                          { return s_GlobalFrame->fBridgeMode;  } 
+void        Abc_FrameSetBridgeMode()                         { s_GlobalFrame->fBridgeMode = 0;     } 
+
 /**Function*************************************************************
 
   Synopsis    [Returns 1 if the flag is enabled without value or with value 1.]

src/base/main/mainInt.h

@@ -70,6 +70,7 @@ struct Abc_Frame_t_
     int             nSteps;      // the counter of different network processed
     int             fAutoexac;   // marks the autoexec mode
     int                fBatchMode;     // are we invoked in batch mode?
+    int             fBridgeMode; // are we invoked in bridge mode?
     // output streams
     FILE *          Out;
     FILE *          Err;

src/base/main/mainUtils.c

@@ -120,7 +120,7 @@ void Abc_UtilsPrintUsage( Abc_Frame_t * pAbc, char * ProgName )
 {
     fprintf( pAbc->Err, "\n" );
     fprintf( pAbc->Err,
-             "usage: %s [-c cmd] [-f script] [-h] [-o file] [-s] [-t type] [-T type] [-x] [file]\n", 
+             "usage: %s [-c cmd] [-f script] [-h] [-o file] [-s] [-t type] [-T type] [-x] [-b] [file]\n", 
              ProgName);
     fprintf( pAbc->Err, "    -c cmd\texecute commands `cmd'\n");
     fprintf( pAbc->Err, "    -F script\texecute commands from a script file and echo commands\n");
@@ -131,6 +131,7 @@ void Abc_UtilsPrintUsage( Abc_Frame_t * pAbc, char * ProgName )
     fprintf( pAbc->Err, "    -t type\tspecify input type (blif_mv (default), blif_mvs, blif, or none)\n");
     fprintf( pAbc->Err, "    -T type\tspecify output type (blif_mv (default), blif_mvs, blif, or none)\n");
     fprintf( pAbc->Err, "    -x\t\tequivalent to '-t none -T none'\n");
+    fprintf( pAbc->Err, "    -b\t\trunning in bridge mode\n");
     fprintf( pAbc->Err, "\n" );
 }
 

src/misc/util/abc_global.h

@@ -256,23 +256,19 @@ enum Abc_VerbLevel
     ABC_VERBOSE  =  2 
 }; 
 
-extern int Gia_ManToBridgeText( FILE * pFile, int Size, unsigned char * pBuffer );
-
-// string printing
-extern char * vnsprintf(const char* format, va_list args);
-extern char * nsprintf(const char* format, ...);
-
 static inline void Abc_Print( int level, const char * format, ... ) 
 {
-    extern int in_bridge_mode;
+    extern ABC_DLL int Abc_FrameIsBridgeMode();
     va_list args;
     if ( level == ABC_ERROR ) 
         printf( "Error: " );
     else if ( level == ABC_WARNING ) 
         printf( "Warning: " );
     va_start( args, format );
-    if ( in_bridge_mode )
+    if ( Abc_FrameIsBridgeMode() )
     {
+        extern int Gia_ManToBridgeText( FILE * pFile, int Size, unsigned char * pBuffer );
+        extern char * vnsprintf(const char* format, va_list args);
         unsigned char * tmp = vnsprintf( format, args );
         Gia_ManToBridgeText( stdout, strlen(tmp), tmp );
         free( tmp );
@@ -345,6 +341,10 @@ extern void   Abc_QuickSort3( word * pData, int nSize, int fDecrease );
 extern void   Abc_QuickSortCostData( int * pCosts, int nSize, int fDecrease, word * pData, int * pResult );
 extern int *  Abc_QuickSortCost( int * pCosts, int nSize, int fDecrease );
 
+// string printing
+extern char * vnsprintf(const char* format, va_list args);
+extern char * nsprintf(const char* format, ...);
+
 
 ABC_NAMESPACE_HEADER_END
 

src/misc/util/utilBridge.c

@@ -23,9 +23,7 @@
 #include <stdlib.h>
 #include <assert.h>
 
-#include "abc_global.h"
 #include "src/aig/gia/gia.h"
-#include "src/misc/vec/vec.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -33,14 +31,20 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+#define BRIDGE_TEXT_MESSAGE   999996
+#define BRIDGE_RESULTS           101
+#define BRIDGE_ABS_NETLIST       107
+#define BRIDGE_BAD_ABS           105
+
+#define BRIDGE_VALUE_X             0
+#define BRIDGE_VALUE_0             2
+#define BRIDGE_VALUE_1             3
+
 extern void Gia_WriteAigerEncodeStr( Vec_Str_t * vStr, unsigned x );
 
 extern unsigned Gia_ReadAigerDecode( unsigned char ** ppPos );
 extern void     Gia_WriteAigerEncodeStr( Vec_Str_t * vStr, unsigned x );
 
-// this variable determines where the output goes
-int in_bridge_mode = 0;
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -58,63 +62,52 @@ int in_bridge_mode = 0;
 ***********************************************************************/
 Vec_Str_t * Gia_ManToBridgeVec( Gia_Man_t * p )
 {
-    Vec_Str_t * vBuffer;
+    Vec_Str_t * vStr;
     Gia_Obj_t * pObj;
-    int nNodes = 0, i, uLit, uLit0, uLit1; 
+    int i, uLit0, uLit1, nNodes;
-    // set the node numbers to be used in the output file
+    assert( Gia_ManPoNum(p) > 0 );
-    Gia_ManConst0(p)->Value = nNodes++;
-    Gia_ManForEachCi( p, pObj, i )
-        pObj->Value = nNodes++;
-    Gia_ManForEachAnd( p, pObj, i )
-        pObj->Value = nNodes++;
 
-    // write the header "M I L O A" where M = I + L + A
+    // start with const1 node (number 1)
-    vBuffer = Vec_StrAlloc( 3*Gia_ManObjNum(p) );
+    nNodes = 1;
-    Vec_StrPrintStr( vBuffer, "aig " );
+    // assign literals(!!!) to the value field
-    Vec_StrPrintNum( vBuffer, Gia_ManCandNum(p) );
+    Gia_ManConst0(p)->Value = Abc_Var2Lit( nNodes++, 1 );
-    Vec_StrPrintStr( vBuffer, " " );
+    Gia_ManForEachCi( p, pObj, i )
-    Vec_StrPrintNum( vBuffer, Gia_ManPiNum(p) );
+        pObj->Value = Abc_Var2Lit( nNodes++, 0 );
-    Vec_StrPrintStr( vBuffer, " " );
+    Gia_ManForEachAnd( p, pObj, i )
-    Vec_StrPrintNum( vBuffer, Gia_ManRegNum(p) );
+        pObj->Value = Abc_Var2Lit( nNodes++, 0 );
-    Vec_StrPrintStr( vBuffer, " " );
+
-    Vec_StrPrintNum( vBuffer, Gia_ManPoNum(p) );
+    // write header
-    Vec_StrPrintStr( vBuffer, " " );
+    vStr = Vec_StrAlloc( 1000 );
-    Vec_StrPrintNum( vBuffer, Gia_ManAndNum(p) );
+    Gia_WriteAigerEncodeStr( vStr, Gia_ManPiNum(p) );
-    Vec_StrPrintStr( vBuffer, "\n" );
+    Gia_WriteAigerEncodeStr( vStr, Gia_ManRegNum(p) );
+    Gia_WriteAigerEncodeStr( vStr, Gia_ManAndNum(p) );
+
+    // write the nodes 
+    Gia_ManForEachAnd( p, pObj, i )
+    {
+        uLit0 = Gia_ObjFanin0Copy( pObj );
+        uLit1 = Gia_ObjFanin1Copy( pObj );
+        assert( uLit0 != uLit1 );
+        Gia_WriteAigerEncodeStr( vStr, uLit0 << 1 );
+        Gia_WriteAigerEncodeStr( vStr, uLit1 );
+    }
 
     // write latch drivers
     Gia_ManForEachRi( p, pObj, i )
     {
-        uLit = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj) );
+        uLit0 = Gia_ObjFanin0Copy( pObj );
-        Vec_StrPrintNum( vBuffer, uLit );
+        Gia_WriteAigerEncodeStr( vStr, (uLit0 << 2) | BRIDGE_VALUE_0 );
-        Vec_StrPrintStr( vBuffer, "\n" );
     }
 
     // write PO drivers
+    Gia_WriteAigerEncodeStr( vStr, Gia_ManPoNum(p) );
     Gia_ManForEachPo( p, pObj, i )
     {
-        uLit = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj) );
+        uLit0 = Gia_ObjFanin0Copy( pObj );
-        Vec_StrPrintNum( vBuffer, uLit );
+        // complement property output!!!
-        Vec_StrPrintStr( vBuffer, "\n" );
+        Gia_WriteAigerEncodeStr( vStr, Abc_LitNot(uLit0) );
     }
-    // write the nodes into the buffer
+    return vStr;
-    Gia_ManForEachAnd( p, pObj, i )
-    {
-        uLit  = Abc_Var2Lit( Gia_ObjValue(pObj), 0 );
-        uLit0 = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj) );
-        uLit1 = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin1(pObj)), Gia_ObjFaninC1(pObj) );
-        assert( uLit0 != uLit1 );
-        if ( uLit0 > uLit1 )
-        {
-            int Temp = uLit0;
-            uLit0 = uLit1;
-            uLit1 = Temp;
-        }
-        Gia_WriteAigerEncodeStr( vBuffer, uLit  - uLit1 );
-        Gia_WriteAigerEncodeStr( vBuffer, uLit1 - uLit0 );
-    }
-    Vec_StrPrintStr( vBuffer, "c" );
-    return vBuffer;
 }
 
 /**Function*************************************************************
@@ -130,33 +123,17 @@ Vec_Str_t * Gia_ManToBridgeVec( Gia_Man_t * p )
 ***********************************************************************/
 void Gia_CreateHeader( FILE * pFile, int Type, int Size, unsigned char * pBuffer )
 {
+    int RetValue;
     fprintf( pFile, "%.6d", Type );
     fprintf( pFile, " " );
     fprintf( pFile, "%.16d", Size );
     fprintf( pFile, " " );
-    fwrite( pBuffer, Size, 1, pFile );
+    RetValue = fwrite( pBuffer, Size, 1, pFile );
+    assert( RetValue == 1 );
     fflush( pFile );
 }
 
 
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-
-
-#define BRIDGE_TEXT_MESSAGE   999996
-#define BRIDGE_RESULTS           101
-#define BRIDGE_ABS_NETLIST       107
-#define BRIDGE_BAD_ABS           105
-
 /**Function*************************************************************
 
   Synopsis    []
@@ -187,24 +164,35 @@ int Gia_ManToBridgeBadAbs( FILE * pFile )
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Gia_ManFromBridgeHolds( FILE * pFile )
 {
-    fputc( (char)3, pFile ); // true
+    fputc( (char)BRIDGE_VALUE_1, pFile ); // true
     fputc( (char)1, pFile ); // size of vector (Armin's encoding)
     fputc( (char)0, pFile ); // number of the property (Armin's encoding)
     fputc( (char)0, pFile ); // no invariant
 }
 void Gia_ManFromBridgeUnknown( FILE * pFile )
 {
-    fputc( (char)0, pFile ); // undef
+    fputc( (char)BRIDGE_VALUE_X, pFile ); // undef
     fputc( (char)1, pFile ); // size of vector (Armin's encoding)
     fputc( (char)0, pFile ); // number of the property (Armin's encoding)
 }
 void Gia_ManFromBridgeCex( FILE * pFile, Abc_Cex_t * pCex )
 {
-    int i, f, iBit;
+    int i, f, iBit, RetValue;
     Vec_Str_t * vStr = Vec_StrAlloc( 1000 );
-    Vec_StrPush( vStr, (char)2 ); // false
+    Vec_StrPush( vStr, (char)BRIDGE_VALUE_0 ); // false
     Vec_StrPush( vStr, (char)1 ); // size of vector (Armin's encoding)
     Vec_StrPush( vStr, (char)0 ); // number of the property (Armin's encoding)
     Vec_StrPush( vStr, (char)1 ); // size of vector (Armin's encoding)
@@ -215,14 +203,15 @@ void Gia_ManFromBridgeCex( FILE * pFile, Abc_Cex_t * pCex )
     for ( f = 0; f <= pCex->iFrame; f++ )
     {
         Gia_WriteAigerEncodeStr( vStr, pCex->nPis ); // num of inputs
-        for ( i = 0; i < pCex->nPis; i++ )
+        for ( i = 0; i < pCex->nPis; i++, iBit++ )
-            Vec_StrPush( vStr, (char)(Abc_InfoHasBit(pCex->pData, iBit++)?3:2) ); // value
+            Vec_StrPush( vStr, (char)(Abc_InfoHasBit(pCex->pData, iBit) ? BRIDGE_VALUE_1:BRIDGE_VALUE_0) ); // value
     }
     assert( iBit == pCex->nBits );
     Vec_StrPush( vStr, (char)1 ); // the number of frames (for a concrete counter-example)
     for ( i = 0; i < pCex->nRegs; i++ )
-        Vec_StrPush( vStr, (char)2 ); // always zero ??????????????
+        Vec_StrPush( vStr, (char)BRIDGE_VALUE_0 ); // always zero!!!
-    fwrite( Vec_StrArray(vStr), Vec_StrSize(vStr), 1, pFile );
+    RetValue = fwrite( Vec_StrArray(vStr), Vec_StrSize(vStr), 1, pFile );
+    assert( RetValue == 1 );
     Vec_StrFree( vStr );
 }
 int Gia_ManToBridgeResult( FILE * pFile, int Result, Abc_Cex_t * pCex )
@@ -238,7 +227,6 @@ int Gia_ManToBridgeResult( FILE * pFile, int Result, Abc_Cex_t * pCex )
 }
 
 
-
 /**Function*************************************************************
 
   Synopsis    []
@@ -264,11 +252,11 @@ Gia_Man_t *  Gia_ManFromBridgeReadBody( int Size, unsigned char * pBuffer, Vec_I
     nGates  = Gia_ReadAigerDecode( &pBuffer );
 
     vLits = Vec_IntAlloc( 1000 );
-    Vec_IntPush( vLits, -1 );
+    Vec_IntPush( vLits, -999 );
     Vec_IntPush( vLits,  1 );
 
     // start the AIG package
-    p = Gia_ManStart( nInputs + nFlops * 2 + nGates + 1 + 1 );
+    p = Gia_ManStart( nInputs + nFlops * 2 + nGates + 1 + 1 ); // PI+FO+FI+AND+PO+1
     p->pName = Abc_UtilStrsav( "temp" );
 
     // create PIs
@@ -286,11 +274,10 @@ Gia_Man_t *  Gia_ManFromBridgeReadBody( int Size, unsigned char * pBuffer, Vec_I
     {
         iFan0 = Gia_ReadAigerDecode( &pBuffer );
         iFan1 = Gia_ReadAigerDecode( &pBuffer );
-        assert( (iFan0 & 1)==0 );
+        assert( !(iFan0 & 1) );
         iFan0 >>= 1;
-
         iFan0 = Abc_LitNotCond( Vec_IntEntry(vLits, iFan0 >> 1), iFan0 & 1 );
-        iFan1 = Abc_LitNotCond( Vec_IntEntry(vLits, iFan1 >> 1), iFan0 & 1 );
+        iFan1 = Abc_LitNotCond( Vec_IntEntry(vLits, iFan1 >> 1), iFan1 & 1 );
         if ( fHash )
             Vec_IntPush( vLits, Gia_ManHashAnd(p, iFan0, iFan1) );
         else 
@@ -302,7 +289,7 @@ Gia_Man_t *  Gia_ManFromBridgeReadBody( int Size, unsigned char * pBuffer, Vec_I
 
     // remember where flops begin
     pBufferPivot = pBuffer;
-    // stroll through flops
+    // scroll through flops
     for ( i = 0; i < nFlops; i++ )
         Gia_ReadAigerDecode( &pBuffer );
 
@@ -312,8 +299,9 @@ Gia_Man_t *  Gia_ManFromBridgeReadBody( int Size, unsigned char * pBuffer, Vec_I
     for ( i = 0; i < nProps; i++ )
     {
         iFan0 = Gia_ReadAigerDecode( &pBuffer );
-        iFan0 = Abc_LitNotCond( Vec_IntEntry(vLits, iFan0 >> 1), iFan0 & 1 );
+        iFan0 = Abc_LitNotCond( Vec_IntEntry(vLits, iFan0 >> 1), iFan0 & 1 ); 
-        Gia_ManAppendCo( p, iFan0 );
+        // complement property output!!!
+        Gia_ManAppendCo( p, Abc_LitNot(iFan0) );
     }
     // make sure the end of buffer is reached
     assert( pBufferEnd == pBuffer );
@@ -324,7 +312,7 @@ Gia_Man_t *  Gia_ManFromBridgeReadBody( int Size, unsigned char * pBuffer, Vec_I
     for ( i = 0; i < nFlops; i++ )
     {
         iFan0 = Gia_ReadAigerDecode( &pBuffer );
-        assert( (iFan0 & 3) == 2 );
+        assert( (iFan0 & 3) == BRIDGE_VALUE_0 );
         Vec_IntPush( vInits, iFan0 & 3 ); // 0 = X value; 1 = not used; 2 = false; 3 = true
         iFan0 >>= 2;
         iFan0 = Abc_LitNotCond( Vec_IntEntry(vLits, iFan0 >> 1), iFan0 & 1 );
@@ -349,6 +337,7 @@ Gia_Man_t *  Gia_ManFromBridgeReadBody( int Size, unsigned char * pBuffer, Vec_I
     return p;
 }
 
+
 /**Function*************************************************************
 
   Synopsis    []
@@ -430,10 +419,32 @@ Gia_Man_t * Gia_ManFromBridge( FILE * pFile, Vec_Int_t ** pvInit )
     {
         extern void Gia_ManFromBridgeTest( char * pFileName );
         Gia_ManFromBridgeTest( "C:\\_projects\\abc\\_TEST\\bug\\65\\par.dump" );
-
     }
 */
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManToBridgeAbsNetlistTest( char * pFileName, Gia_Man_t * p )
+{
+    FILE * pFile = fopen( pFileName, "wb" );
+    if ( pFile == NULL )
+    {
+        printf( "Cannot open output file \"%s\".\n", pFileName );
+        return;
+    }
+    Gia_ManToBridgeAbsNetlist( pFile, p );
+    fclose ( pFile );
+}
+
 /**Function*************************************************************
 
   Synopsis    []
@@ -459,7 +470,9 @@ void Gia_ManFromBridgeTest( char * pFileName )
     fclose ( pFile );
 
     Gia_ManPrintStats( p, 0, 0 );
-//    Gia_WriteAiger( p, "temp.aig", 0, 0 );
+    Gia_WriteAiger( p, "temp.aig", 0, 0 );
+   
+    Gia_ManToBridgeAbsNetlistTest( "par_.dump", p );
     Gia_ManStop( p );
 }