ioWriteSmv.c File Reference

#include "ioAbc.h"

Go to the source code of this file.

Functions
static ABC_NAMESPACE_IMPL_START int	Io_WriteSmvCheckNames (Abc_Ntk_t *pNtk)
	DECLARATIONS ///. More...
static int	Io_WriteSmvOne (FILE *pFile, Abc_Ntk_t *pNtk)
static int	Io_WriteSmvOneNode (FILE *pFile, Abc_Obj_t *pNode)
static char *	cleanUNSAFE (const char *s)
	FUNCTION DEFINITIONS ///. More...
static int	hasPrefix (const char *needle, const char *haystack)
int	Io_WriteSmv (Abc_Ntk_t *pNtk, char *pFileName)

Function Documentation

static char* cleanUNSAFE ( const char *  s )

static

FUNCTION DEFINITIONS ///.

Definition at line 45 of file ioWriteSmv.c.

{
    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  )

static

Definition at line 55 of file ioWriteSmv.c.

{
    return (strncmp(haystack, needle, strlen(needle)) == 0);
}

int Io_WriteSmv	(	Abc_Ntk_t *	pNtk,
		char *	pFileName
	)

Function*************************************************************

Synopsis [Writes the network in SMV format.]

Description []

SideEffects []

SeeAlso []

Definition at line 71 of file ioWriteSmv.c.

{
    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;
}

int Io_WriteSmvCheckNames ( Abc_Ntk_t *  pNtk )

static

DECLARATIONS ///.

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

]

Function*************************************************************

Synopsis [Returns 1 if the names cannot be written into the bench file.]

Description []

SideEffects []

SeeAlso []

Definition at line 247 of file ioWriteSmv.c.

{
    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;
}

int Io_WriteSmvOne ( FILE *  pFile, Abc_Ntk_t *  pNtk  )

static

Function*************************************************************

Synopsis [Writes the network in SMV format.]

Description []

SideEffects []

SeeAlso []

Definition at line 110 of file ioWriteSmv.c.

{
    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;
}

int Io_WriteSmvOneNode ( FILE *  pFile, Abc_Obj_t *  pNode  )

static

Function*************************************************************

Synopsis [Writes the network in SMV format.]

Description []

SideEffects []

SeeAlso []

Definition at line 202 of file ioWriteSmv.c.

{
    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;
}