luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity
abc/src/base/io/ioWriteSmv.c

266 lines
8.2 KiB
C
Raw Blame History

/**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 parentheses 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
Reference in New Issue View Git Blame Copy Permalink