diff options
Diffstat (limited to 'src/base/io/ioWriteSmv.c')
| -rw-r--r-- | src/base/io/ioWriteSmv.c | 265 |
1 files changed, 265 insertions, 0 deletions
diff --git a/src/base/io/ioWriteSmv.c b/src/base/io/ioWriteSmv.c new file mode 100644 index 00000000..c767bcaa --- /dev/null +++ b/src/base/io/ioWriteSmv.c @@ -0,0 +1,265 @@ +/**CFile**************************************************************** + + FileName [ioWriteSmv.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Command processing package.] + + Synopsis [Procedures to write the network in SMV format.] + + Author [Satrajit Chatterjee] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: ioWriteSmv.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "ioAbc.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static int Io_WriteSmvCheckNames( Abc_Ntk_t * pNtk ); + +static int Io_WriteSmvOne( FILE * pFile, Abc_Ntk_t * pNtk ); +static int Io_WriteSmvOneNode( FILE * pFile, Abc_Obj_t * pNode ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +// This returns a pointer to a static area, so be careful in using results +// of this function i.e. don't call this twice in the same printf call. +// +// This function replaces '|' with '_' I think abc introduces '|' when +// flattening hierarchy. The '|' is interpreted as a or function by nusmv +// which is unfortunate. This probably should be fixed elsewhere. +static char *cleanUNSAFE( const char *s ) +{ + char *t; + static char buffer[1024]; + assert (strlen(s) < 1024); + strcpy(buffer, s); + for (t = buffer; *t != 0; ++t) *t = (*t == '|') ? '_' : *t; + return buffer; +} + +static int hasPrefix(const char *needle, const char *haystack) +{ + return (strncmp(haystack, needle, strlen(needle)) == 0); +} + +/**Function************************************************************* + + Synopsis [Writes the network in SMV format.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Io_WriteSmv( Abc_Ntk_t * pNtk, char * pFileName ) +{ + Abc_Ntk_t * pExdc; + FILE * pFile; + assert( Abc_NtkIsSopNetlist(pNtk) ); + if ( !Io_WriteSmvCheckNames(pNtk) ) + { + fprintf( stdout, "Io_WriteSmv(): Signal names in this benchmark contain parantheses making them impossible to reproduce in the SMV format. Use \"short_names\".\n" ); + return 0; + } + pFile = fopen( pFileName, "w" ); + if ( pFile == NULL ) + { + fprintf( stdout, "Io_WriteSmv(): Cannot open the output file.\n" ); + return 0; + } + fprintf( pFile, "-- benchmark \"%s\" written by ABC on %s\n", pNtk->pName, Extra_TimeStamp() ); + // write the network + Io_WriteSmvOne( pFile, pNtk ); + // write EXDC network if it exists + pExdc = Abc_NtkExdc( pNtk ); + if ( pExdc ) + printf( "Io_WriteSmv: EXDC is not written (warning).\n" ); + // finalize the file + fclose( pFile ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Writes the network in SMV format.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Io_WriteSmvOne( FILE * pFile, Abc_Ntk_t * pNtk ) +{ + ProgressBar * pProgress; + Abc_Obj_t * pNode; + int i; + + // write the PIs/POs/latches + fprintf( pFile, "MODULE main\n"); // nusmv needs top module to be main + fprintf ( pFile, "\n" ); + + fprintf( pFile, "VAR -- inputs\n"); + Abc_NtkForEachPi( pNtk, pNode, i ) + fprintf( pFile, " %s : boolean;\n", + cleanUNSAFE(Abc_ObjName(Abc_ObjFanout0(pNode))) ); + fprintf ( pFile, "\n" ); + + fprintf( pFile, "VAR -- state variables\n"); + Abc_NtkForEachLatch( pNtk, pNode, i ) + fprintf( pFile, " %s : boolean;\n", + cleanUNSAFE(Abc_ObjName(Abc_ObjFanout0(Abc_ObjFanout0(pNode)))) ); + fprintf ( pFile, "\n" ); + + // No outputs needed for NuSMV: + // TODO: Add sepcs by recognizing assume_.* and assert_.* + // + // Abc_NtkForEachPo( pNtk, pNode, i ) + // fprintf( pFile, "OUTPUT(%s)\n", Abc_ObjName(Abc_ObjFanin0(pNode)) ); + + // write internal nodes + fprintf( pFile, "DEFINE\n"); + pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pNtk) ); + Abc_NtkForEachNode( pNtk, pNode, i ) + { + Extra_ProgressBarUpdate( pProgress, i, NULL ); + Io_WriteSmvOneNode( pFile, pNode ); + } + Extra_ProgressBarStop( pProgress ); + fprintf ( pFile, "\n" ); + + fprintf( pFile, "ASSIGN\n"); + Abc_NtkForEachLatch( pNtk, pNode, i ) + { + int Reset = (int)(ABC_PTRUINT_T)Abc_ObjData( pNode ); + assert (Reset >= 1); + assert (Reset <= 3); + + if (Reset != 3) + { + fprintf( pFile, " init(%s) := %d;\n", + cleanUNSAFE(Abc_ObjName(Abc_ObjFanout0(Abc_ObjFanout0(pNode)))), + Reset - 1); + } + fprintf( pFile, " next(%s) := ", + cleanUNSAFE(Abc_ObjName(Abc_ObjFanout0(Abc_ObjFanout0(pNode)))) ); + fprintf( pFile, "%s;\n", + cleanUNSAFE(Abc_ObjName(Abc_ObjFanin0(Abc_ObjFanin0(pNode)))) ); + } + + fprintf ( pFile, "\n" ); + Abc_NtkForEachPo( pNtk, pNode, i ) + { + const char *n = cleanUNSAFE(Abc_ObjName(Abc_ObjFanin0(pNode))); + // fprintf( pFile, "-- output %s;\n", n ); + if (hasPrefix("assume_fair_", n)) + { + fprintf( pFile, "FAIRNESS %s;\n", n ); + } + else if (hasPrefix("Assert_", n) || + hasPrefix("assert_safety_", n)) + { + fprintf( pFile, "INVARSPEC %s;\n", n ); + } + else if (hasPrefix("assert_fair_", n)) + { + fprintf( pFile, "LTLSPEC G F %s;\n", n ); + } + } + + return 1; +} + +/**Function************************************************************* + + Synopsis [Writes the network in SMV format.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Io_WriteSmvOneNode( FILE * pFile, Abc_Obj_t * pNode ) +{ + int nFanins; + + assert( Abc_ObjIsNode(pNode) ); + nFanins = Abc_ObjFaninNum(pNode); + if ( nFanins == 0 ) + { // write the constant 1 node + assert( Abc_NodeIsConst1(pNode) ); + fprintf( pFile, " %s", cleanUNSAFE(Abc_ObjName(Abc_ObjFanout0(pNode)) ) ); + fprintf( pFile, " := 1;\n" ); + } + else if ( nFanins == 1 ) + { // write the interver/buffer + if ( Abc_NodeIsBuf(pNode) ) + { + fprintf( pFile, " %s := ", cleanUNSAFE(Abc_ObjName(Abc_ObjFanout0(pNode))) ); + fprintf( pFile, "%s;\n", cleanUNSAFE(Abc_ObjName(Abc_ObjFanin0(pNode))) ); + } + else + { + fprintf( pFile, " %s := !", cleanUNSAFE(Abc_ObjName(Abc_ObjFanout0(pNode))) ); + fprintf( pFile, "%s;\n", cleanUNSAFE(Abc_ObjName(Abc_ObjFanin0(pNode))) ); + } + } + else + { // write the AND gate + fprintf( pFile, " %s", cleanUNSAFE(Abc_ObjName(Abc_ObjFanout0(pNode))) ); + fprintf( pFile, " := %s & ", cleanUNSAFE(Abc_ObjName(Abc_ObjFanin0(pNode))) ); + fprintf( pFile, "%s;\n", cleanUNSAFE(Abc_ObjName(Abc_ObjFanin1(pNode))) ); + } + return 1; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if the names cannot be written into the bench file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Io_WriteSmvCheckNames( Abc_Ntk_t * pNtk ) +{ + Abc_Obj_t * pObj; + char * pName; + int i; + Abc_NtkForEachObj( pNtk, pObj, i ) + for ( pName = Nm_ManFindNameById(pNtk->pManName, i); pName && *pName; pName++ ) + if ( *pName == '(' || *pName == ')' ) + return 0; + return 1; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + |