Commit a25faed1 by Mathias Soeken

Merged alanmi/abc into default

parents f47a4377 76c4d222
......@@ -567,6 +567,10 @@ SOURCE=.\src\base\io\ioInt.h
# End Source File
# Begin Source File
SOURCE=.\src\base\io\ioJson.c
# End Source File
# Begin Source File
SOURCE=.\src\base\io\ioReadAiger.c
# End Source File
# Begin Source File
......@@ -779,6 +783,10 @@ SOURCE=.\src\base\wlc\wlcCom.c
# End Source File
# Begin Source File
SOURCE=.\src\base\wlc\wlcJson.c
# End Source File
# Begin Source File
SOURCE=.\src\base\wlc\wlcNtk.c
# End Source File
# Begin Source File
......
......@@ -48,6 +48,7 @@ static int IoCommandReadTruth ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadVerilog ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadStatus ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadGig ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadJson ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWrite ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteHie ( Abc_Frame_t * pAbc, int argc, char **argv );
......@@ -74,6 +75,7 @@ static int IoCommandWriteTruth ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteTruths ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteStatus ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteSmv ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteJson ( Abc_Frame_t * pAbc, int argc, char **argv );
extern void Abc_FrameCopyLTLDataBase( Abc_Frame_t *pAbc, Abc_Ntk_t * pNtk );
......@@ -114,6 +116,7 @@ void Io_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "I/O", "read_verilog", IoCommandReadVerilog, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_status", IoCommandReadStatus, 0 );
Cmd_CommandAdd( pAbc, "I/O", "&read_gig", IoCommandReadGig, 0 );
Cmd_CommandAdd( pAbc, "I/O", "read_json", IoCommandReadJson, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write", IoCommandWrite, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write_hie", IoCommandWriteHie, 0 );
......@@ -141,6 +144,7 @@ void Io_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "I/O", "&write_truths", IoCommandWriteTruths, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write_status", IoCommandWriteStatus, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write_smv", IoCommandWriteSmv, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write_json", IoCommandWriteJson, 0 );
}
/**Function*************************************************************
......@@ -1334,6 +1338,67 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int IoCommandReadJson( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern Vec_Wec_t * Json_Read( char * pFileName, Abc_Nam_t ** ppStrs );
Vec_Wec_t * vObjs;
Abc_Nam_t * pStrs;
char * pFileName;
FILE * pFile;
int c;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
{
switch ( c )
{
case 'h':
goto usage;
default:
goto usage;
}
}
if ( argc != globalUtilOptind + 1 )
{
goto usage;
}
// get the input file name
pFileName = argv[globalUtilOptind];
if ( (pFile = fopen( pFileName, "r" )) == NULL )
{
fprintf( pAbc->Err, "Cannot open input file \"%s\". \n", pFileName );
return 1;
}
fclose( pFile );
// set the new network
vObjs = Json_Read( pFileName, &pStrs );
if ( vObjs == NULL )
return 0;
Abc_FrameSetJsonStrs( pStrs );
Abc_FrameSetJsonObjs( vObjs );
return 0;
usage:
fprintf( pAbc->Err, "usage: read_json [-h] <file>\n" );
fprintf( pAbc->Err, "\t reads file in JSON format\n" );
fprintf( pAbc->Err, "\t-h : prints the command summary\n" );
fprintf( pAbc->Err, "\tfile : the name of a file to read\n" );
return 1;
}
/**Function*************************************************************
......@@ -2999,10 +3064,8 @@ usage:
int IoCommandWriteSmv( Abc_Frame_t * pAbc, int argc, char **argv )
{
char * pFileName;
int fUseLuts;
int c;
fUseLuts = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
{
......@@ -3034,6 +3097,56 @@ usage:
fprintf( pAbc->Err, "\tfile : the name of the file to write (extension .smv)\n" );
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int IoCommandWriteJson( Abc_Frame_t * pAbc, int argc, char **argv )
{
extern void Json_Write( char * pFileName, Abc_Nam_t * pStr, Vec_Wec_t * vObjs );
char * pFileName;
int c;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
{
switch ( c )
{
case 'h':
goto usage;
default:
goto usage;
}
}
if ( Abc_FrameReadJsonStrs(Abc_FrameReadGlobalFrame()) == NULL )
{
fprintf( pAbc->Out, "No JSON info is available.\n" );
return 0;
}
if ( argc != globalUtilOptind + 1 )
goto usage;
// get the output file name
pFileName = argv[globalUtilOptind];
// call the corresponding file writer
Json_Write( pFileName, Abc_FrameReadJsonStrs(Abc_FrameReadGlobalFrame()), Abc_FrameReadJsonObjs(Abc_FrameReadGlobalFrame()) );
return 0;
usage:
fprintf( pAbc->Err, "usage: write_json [-h] <file>\n" );
fprintf( pAbc->Err, "\t write the network in JSON format\n" );
fprintf( pAbc->Err, "\t-h : print the help message\n" );
fprintf( pAbc->Err, "\tfile : the name of the file to write (extension .json)\n" );
return 1;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
......
......@@ -28,6 +28,7 @@
#include "base/abc/abc.h"
#include "misc/extra/extra.h"
#include "misc/util/utilNam.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
......@@ -57,6 +58,7 @@ typedef enum {
IO_FILE_EDIF,
IO_FILE_EQN,
IO_FILE_GML,
IO_FILE_JSON,
IO_FILE_LIST,
IO_FILE_PLA,
IO_FILE_MOPLA,
......@@ -152,6 +154,9 @@ extern Abc_Obj_t * Io_ReadCreateInv( Abc_Ntk_t * pNtk, char * pNameIn, ch
extern Abc_Obj_t * Io_ReadCreateBuf( Abc_Ntk_t * pNtk, char * pNameIn, char * pNameOut );
extern FILE * Io_FileOpen( const char * FileName, const char * PathVar, const char * Mode, int fVerbose );
/*=== ioJson.c ===========================================================*/
extern void Io_ReadJson( char * pFileName );
extern void Io_WriteJson( char * pFileName );
......
/**CFile****************************************************************
FileName [ioJson.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Command processing package.]
Synopsis [Procedures to read JSON.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: ioJson.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "ioAbc.h"
#include "misc/vec/vecWec.h"
#include "misc/util/utilNam.h"
#include "misc/extra/extra.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static inline int Json_EntryIsName( int Fan ) { return Abc_LitIsCompl(Fan); }
static inline char * Json_EntryName( Abc_Nam_t * pStrs, int Fan ) { assert(Json_EntryIsName(Fan)); return Abc_NamStr( pStrs, Abc_Lit2Var(Fan) ); }
static inline Vec_Int_t * Json_EntryNode( Vec_Wec_t * vObjs, int Fan ) { assert(!Json_EntryIsName(Fan)); return Vec_WecEntry( vObjs, Abc_Lit2Var(Fan) ); }
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Parsing.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Json_CharIsSpace( char c )
{
return (c == ' ' || c == '\t' || c == '\r' || c == '\n');
}
static inline char * Json_SkipSpaces( char * pCur )
{
while ( Json_CharIsSpace(*pCur) )
pCur++;
return pCur;
}
static inline char * Json_SkipNonSpaces( char * pCur )
{
while ( !Json_CharIsSpace(*pCur) )
pCur++;
return pCur;
}
static inline int Json_TokenCompare( char * pCur, char * pNext, char ** ppCur2, char ** ppNext2 )
{
// int i;
if ( *pCur == '\"' )
pCur++;
if ( *(pNext-1) == ',' )
pNext--;
if ( *(pNext-1) == '\"' )
pNext--;
*ppCur2 = pCur;
*ppNext2 = pNext;
// for ( i = 1; i < JSON_NUM_LINES; i++ )
// if ( !strncmp( s_Types[i].pName, pCur, pNext - pCur ) )
// return i;
return 0;
}
/**Function*************************************************************
Synopsis [Writes JSON into a file.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Json_Write_rec( FILE * pFile, Abc_Nam_t * pStr, Vec_Wec_t * vObjs, Vec_Int_t * vArray, int Level, int fAddComma, int fSpaces )
{
int i, Entry1, Entry2, fComma;
if ( Vec_IntEntry(vArray, 0) ) // array
{
if ( Vec_IntSize(vArray) == 1 )
fprintf( pFile, "[]" );
else if ( Vec_IntSize(vArray) == 2 && Json_EntryIsName(Vec_IntEntry(vArray,1)) )
fprintf( pFile, "[ \"%s\" ]", Json_EntryName(pStr, Vec_IntEntry(vArray,1)) );
else
{
if ( fSpaces )
fprintf( pFile, "%*s", 3*(Level-1), "" );
fprintf( pFile, "[\n" );
Vec_IntForEachEntryStart( vArray, Entry1, i, 1 )
{
fComma = (i < Vec_IntSize(vArray) - 1);
if ( Json_EntryIsName(Entry1) )
fprintf( pFile, "%*s\"%s\"%s\n", 3*Level, "", Json_EntryName(pStr, Entry1), fComma ? ",":"" );
else
Json_Write_rec( pFile, pStr, vObjs, Json_EntryNode(vObjs, Entry1), Level+1, fComma, 1 );
}
fprintf( pFile, "%*s]", 3*(Level-1), "" );
}
fprintf( pFile, "%s\n", fAddComma ? ",":"" );
}
else // list of pairs
{
if ( fSpaces )
fprintf( pFile, "%*s", 3*(Level-1), "" );
fprintf( pFile, "{\n" );
assert( Vec_IntSize(vArray) % 2 != 0 );
Vec_IntForEachEntryDoubleStart( vArray, Entry1, Entry2, i, 1 )
{
fComma = (i < Vec_IntSize(vArray) - 3);
if ( Json_EntryIsName(Entry1) )
fprintf( pFile, "%*s\"%s\"", 3*Level, "", Json_EntryName(pStr, Entry1) );
else
Json_Write_rec( pFile, pStr, vObjs, Json_EntryNode(vObjs, Entry1), Level+1, 0, 1 );
fprintf( pFile, " : " );
if ( Json_EntryIsName(Entry2) )
fprintf( pFile, "\"%s\"%s\n", Json_EntryName(pStr, Entry2), fComma ? ",":"" );
else
Json_Write_rec( pFile, pStr, vObjs, Json_EntryNode(vObjs, Entry2), Level+1, fComma, 0 );
}
fprintf( pFile, "%*s}%s\n", 3*(Level-1), "", fAddComma ? ",":"" );
}
}
void Json_Write( char * pFileName, Abc_Nam_t * pStr, Vec_Wec_t * vObjs )
{
FILE * pFile = fopen( pFileName, "wb" );
if ( pFile == NULL )
{
printf( "Cannot open file \"%s\" for writing.\n", pFileName );
return;
}
Json_Write_rec( pFile, pStr, vObjs, Vec_WecEntry(vObjs, 0), 1, 0, 1 );
fclose( pFile );
}
/**Function*************************************************************
Synopsis [Reads JSON from a file.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Wec_t * Json_Read( char * pFileName, Abc_Nam_t ** ppStrs )
{
Abc_Nam_t * pStrs;
Vec_Wec_t * vObjs;
Vec_Int_t * vStack, * vTemp;
char * pContents, * pCur, * pNext, * pCur2, * pNext2;
int nFileSize, RetValue, iToken;
FILE * pFile;
// read the file into the buffer
pFile = fopen( pFileName, "rb" );
if ( pFile == NULL )
{
printf( "Cannot open file \"%s\" for reading.\n", pFileName );
return NULL;
}
nFileSize = Extra_FileSize( pFileName );
pContents = pCur = ABC_ALLOC( char, nFileSize+1 );
RetValue = fread( pContents, nFileSize, 1, pFile );
pContents[nFileSize] = 0;
fclose( pFile );
// start data-structures
vObjs = Vec_WecAlloc( 1000 );
vStack = Vec_IntAlloc( 100 );
pStrs = Abc_NamStart( 1000, 24 );
//Json_AddTypes( pStrs );
// read lines
assert( Vec_WecSize(vObjs) == 0 );
assert( Vec_IntSize(vStack) == 0 );
while ( pCur < pContents + nFileSize )
{
pCur = Json_SkipSpaces( pCur );
if ( *pCur == '\0' )
break;
pNext = Json_SkipNonSpaces( pCur );
if ( *pCur == '{' || *pCur == '[' )
{
// add fanin to node on the previous level
if ( Vec_IntSize(vStack) > 0 )
Vec_IntPush( Vec_WecEntry(vObjs, Vec_IntEntryLast(vStack)), Abc_Var2Lit(Vec_WecSize(vObjs), 0) );
// add node to the stack
Vec_IntPush( vStack, Vec_WecSize(vObjs) );
vTemp = Vec_WecPushLevel( vObjs );
Vec_IntGrow( vTemp, 4 );
// remember it as an array
Vec_IntPush( vTemp, (int)(*pCur == '[') );
pCur++;
continue;
}
if ( *pCur == '}' || *pCur == ']' )
{
Vec_IntPop( vStack );
pCur++;
continue;
}
if ( *pCur == ',' || *pCur == ':' )
{
pCur++;
continue;
}
iToken = Json_TokenCompare( pCur, pNext, &pCur2, &pNext2 );
if ( iToken == 0 )
iToken = Abc_NamStrFindOrAddLim( pStrs, pCur2, pNext2, NULL );
Vec_IntPush( Vec_WecEntry(vObjs, Vec_IntEntryLast(vStack)), Abc_Var2Lit(iToken, 1) );
pCur = pNext;
}
Vec_IntFree( vStack );
ABC_FREE( pContents );
*ppStrs = pStrs;
return vObjs;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Json_ReadTest( char * pFileName )
{
Abc_Nam_t * pStrs;
Vec_Wec_t * vObjs;
vObjs = Json_Read( pFileName, &pStrs );
if ( vObjs == NULL )
return;
Json_Write( "test.json", pStrs, vObjs );
Abc_NamDeref( pStrs );
Vec_WecFree( vObjs );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END
SRC += src/base/io/io.c \
src/base/io/ioJson.c \
src/base/io/ioReadAiger.c \
src/base/io/ioReadBaf.c \
src/base/io/ioReadBblif.c \
......
......@@ -122,6 +122,8 @@ extern ABC_DLL Vec_Int_t * Abc_FrameReadStatusVec( Abc_Frame_t * p );
extern ABC_DLL Vec_Ptr_t * Abc_FrameReadPoEquivs( Abc_Frame_t * p );
extern ABC_DLL Vec_Int_t * Abc_FrameReadPoStatuses( Abc_Frame_t * p );
extern ABC_DLL Vec_Int_t * Abc_FrameReadObjIds( Abc_Frame_t * p );
extern ABC_DLL Abc_Nam_t * Abc_FrameReadJsonStrs( Abc_Frame_t * p );
extern ABC_DLL Vec_Wec_t * Abc_FrameReadJsonObjs( Abc_Frame_t * p );
extern ABC_DLL int Abc_FrameReadCexPiNum( Abc_Frame_t * p );
extern ABC_DLL int Abc_FrameReadCexRegNum( Abc_Frame_t * p );
......@@ -145,6 +147,8 @@ extern ABC_DLL void Abc_FrameSetManDsd2( void * pMan );
extern ABC_DLL void Abc_FrameSetInv( Vec_Int_t * vInv );
extern ABC_DLL void Abc_FrameSetCnf( Vec_Int_t * vInv );
extern ABC_DLL void Abc_FrameSetStr( Vec_Str_t * vInv );
extern ABC_DLL void Abc_FrameSetJsonStrs( Abc_Nam_t * pStrs );
extern ABC_DLL void Abc_FrameSetJsonObjs( Vec_Wec_t * vObjs );
extern ABC_DLL int Abc_FrameCheckPoConst( Abc_Frame_t * p, int iPoNum );
......
......@@ -75,6 +75,8 @@ Vec_Int_t * Abc_FrameReadStatusVec( Abc_Frame_t * p ) { return s_GlobalFr
Vec_Ptr_t * Abc_FrameReadPoEquivs( Abc_Frame_t * p ) { return s_GlobalFrame->vPoEquivs; }
Vec_Int_t * Abc_FrameReadPoStatuses( Abc_Frame_t * p ) { return s_GlobalFrame->vStatuses; }
Vec_Int_t * Abc_FrameReadObjIds( Abc_Frame_t * p ) { return s_GlobalFrame->vAbcObjIds; }
Abc_Nam_t * Abc_FrameReadJsonStrs( Abc_Frame_t * p ) { return s_GlobalFrame->pJsonStrs; }
Vec_Wec_t * Abc_FrameReadJsonObjs( Abc_Frame_t * p ) { return s_GlobalFrame->vJsonObjs; }
int Abc_FrameReadCexPiNum( Abc_Frame_t * p ) { return s_GlobalFrame->pCex->nPis; }
int Abc_FrameReadCexRegNum( Abc_Frame_t * p ) { return s_GlobalFrame->pCex->nRegs; }
......@@ -95,6 +97,8 @@ void Abc_FrameSetManDsd2( void * pMan ) { if (s_GlobalFrame
void Abc_FrameSetInv( Vec_Int_t * vInv ) { Vec_IntFreeP(&s_GlobalFrame->pAbcWlcInv); s_GlobalFrame->pAbcWlcInv = vInv; }
void Abc_FrameSetCnf( Vec_Int_t * vCnf ) { Vec_IntFreeP(&s_GlobalFrame->pAbcWlcCnf); s_GlobalFrame->pAbcWlcCnf = vCnf; }
void Abc_FrameSetStr( Vec_Str_t * vStr ) { Vec_StrFreeP(&s_GlobalFrame->pAbcWlcStr); s_GlobalFrame->pAbcWlcStr = vStr; }
void Abc_FrameSetJsonStrs( Abc_Nam_t * pStrs ) { Abc_NamDeref( s_GlobalFrame->pJsonStrs ); s_GlobalFrame->pJsonStrs = pStrs; }
void Abc_FrameSetJsonObjs( Vec_Wec_t * vObjs ) { Vec_WecFreeP(&s_GlobalFrame->vJsonObjs ); s_GlobalFrame->vJsonObjs = vObjs; }
int Abc_FrameIsBatchMode() { return s_GlobalFrame ? s_GlobalFrame->fBatchMode : 0; }
......@@ -225,6 +229,8 @@ void Abc_FrameDeallocate( Abc_Frame_t * p )
Vec_IntFreeP( &p->pAbcWlcInv );
Vec_IntFreeP( &p->pAbcWlcCnf );
Vec_StrFreeP( &p->pAbcWlcStr );
Abc_NamDeref( s_GlobalFrame->pJsonStrs );
Vec_WecFreeP(&s_GlobalFrame->vJsonObjs );
ABC_FREE( p );
s_GlobalFrame = NULL;
}
......
......@@ -134,6 +134,8 @@ struct Abc_Frame_t_
void * pAbcBac;
void * pAbcCba;
void * pAbcPla;
Abc_Nam_t * pJsonStrs;
Vec_Wec_t * vJsonObjs;
#ifdef ABC_USE_CUDD
DdManager * dd; // temporary BDD package
#endif
......
......@@ -2,6 +2,7 @@ SRC += src/base/wlc/wlcAbs.c \
src/base/wlc/wlcAbc.c \
src/base/wlc/wlcBlast.c \
src/base/wlc/wlcCom.c \
src/base/wlc/wlcJson.c \
src/base/wlc/wlcNtk.c \
src/base/wlc/wlcReadSmt.c \
src/base/wlc/wlcReadVer.c \
......
/**CFile****************************************************************
FileName [wlcJson.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Experimental procedures.]
Synopsis [Parses several flavors of word-level Verilog.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - August 22, 2014.]
Revision [$Id: wlcJson.c,v 1.00 2014/09/12 00:00:00 alanmi Exp $]
***********************************************************************/
#include "wlc.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Wlc_JsonTest()
{
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment