summaryrefslogtreecommitdiffstats
path: root/src/base
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2012-03-02 00:57:48 -0800
committerAlan Mishchenko <alanmi@berkeley.edu>2012-03-02 00:57:48 -0800
commit7926d75ecb4ffd4441bea0c2d731e5b533534ee3 (patch)
tree42bd5aa54fe84a6f1e635c8a77a412beb1b4258c /src/base
parenta6f363d4615d01484af29cf8dcc53c87faeb2f3b (diff)
downloadabc-7926d75ecb4ffd4441bea0c2d731e5b533534ee3.tar.gz
abc-7926d75ecb4ffd4441bea0c2d731e5b533534ee3.tar.bz2
abc-7926d75ecb4ffd4441bea0c2d731e5b533534ee3.zip
Adding features related to the communication bridge.
Diffstat (limited to 'src/base')
-rw-r--r--src/base/abci/abc.c9
-rw-r--r--src/base/main/main.c14
-rw-r--r--src/base/main/main.h2
-rw-r--r--src/base/main/mainFrame.c3
-rw-r--r--src/base/main/mainInt.h1
-rw-r--r--src/base/main/mainUtils.c3
6 files changed, 27 insertions, 5 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index c8090460..c4d5df4c 100644
--- a/src/base/abci/abc.c
+++ b/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:
diff --git a/src/base/main/main.c b/src/base/main/main.c
index 0e2ff9f4..1572af91 100644
--- a/src/base/main/main.c
+++ b/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 )
{
diff --git a/src/base/main/main.h b/src/base/main/main.h
index ac30f358..5d777b23 100644
--- a/src/base/main/main.h
+++ b/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 );
diff --git a/src/base/main/mainFrame.c b/src/base/main/mainFrame.c
index 6a63cdd6..fe9aff6a 100644
--- a/src/base/main/mainFrame.c
+++ b/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.]
diff --git a/src/base/main/mainInt.h b/src/base/main/mainInt.h
index 2eca004e..d8a6c93e 100644
--- a/src/base/main/mainInt.h
+++ b/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;
diff --git a/src/base/main/mainUtils.c b/src/base/main/mainUtils.c
index e263bc94..5b6dc893 100644
--- a/src/base/main/mainUtils.c
+++ b/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" );
}