diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-04-18 00:05:11 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-04-18 00:05:11 -0700 |
| commit | 96b784ecd7cc05f99e12d52f36437c9bd9eb2375 (patch) | |
| tree | be730d9a80266baf0b3f664e58b5ab32784703c5 | |
| parent | 61ecc9c633d227160c720d6f0f611cf4e62a9602 (diff) | |
| download | abc-96b784ecd7cc05f99e12d52f36437c9bd9eb2375.tar.gz abc-96b784ecd7cc05f99e12d52f36437c9bd9eb2375.tar.bz2 abc-96b784ecd7cc05f99e12d52f36437c9bd9eb2375.zip | |
Fixing both AIGER readers (read_aiger and &r) to work with AIGER 1.9 (except for liveness properties).
| -rw-r--r-- | abc.rc | 6 | ||||
| -rw-r--r-- | src/aig/gia/giaAiger.c | 1 | ||||
| -rw-r--r-- | src/base/io/ioReadAiger.c | 10 |
3 files changed, 15 insertions, 2 deletions
@@ -129,6 +129,12 @@ alias src_rws "st; rw -l; rs -K 6 -N 2 -l; rwz -l; rs -K 9 -N 2 -l; rwz -l; alias resyn2rs "b; rs -K 6; rw; rs -K 6 -N 2; rf; rs -K 8; b; rs -K 8 -N 2; rw; rs -K 10; rwz; rs -K 10 -N 2; b; rs -K 12; rfz; rs -K 12 -N 2; rwz; b" alias compress2rs "b -l; rs -K 6 -l; rw -l; rs -K 6 -N 2 -l; rf -l; rs -K 8 -l; b -l; rs -K 8 -N 2 -l; rw -l; rs -K 10 -l; rwz -l; rs -K 10 -N 2 -l; b -l; rs -K 12 -l; rfz -l; rs -K 12 -N 2 -l; rwz -l; b -l" +# use this script to convert 1-valued and DC-valued flops for an AIG +alias fix_aig "logic; undc; strash; zero" + +# use this script to convert 1-valued and DC-valued flops for a logic network coming from BLIF +alias fix_blif "undc; strash; zero" + # lazy man's synthesis alias recadd3 "st; rec_add3; b; rec_add3; dc2; rec_add3; if -K 8; bidec; st; rec_add3; dc2; rec_add3; if -g -K 6; st; rec_add3" diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c index 44b0d51a..19ea1447 100644 --- a/src/aig/gia/giaAiger.c +++ b/src/aig/gia/giaAiger.c @@ -780,6 +780,7 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS else { assert( Vec_IntEntry(vInits, i) == Abc_Var2Lit(Gia_ObjId(pNew, pObj), 0) ); + // unitialized value of the latch is the latch literal according to http://fmv.jku.at/hwmcc11/beyond1.pdf pInit[i] = 'X'; } } diff --git a/src/base/io/ioReadAiger.c b/src/base/io/ioReadAiger.c index b936ceb2..5c31f56c 100644 --- a/src/base/io/ioReadAiger.c +++ b/src/base/io/ioReadAiger.c @@ -423,13 +423,19 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck ) uLit0 = atoi( pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++; if ( *pCur == ' ' ) // read initial value { + int Init; pCur++; - if ( atoi( pCur ) == 0 ) + Init = atoi( pCur ); + if ( Init == 0 ) Abc_LatchSetInit0( Abc_NtkBox(pNtkNew, i) ); - else if ( atoi( pCur ) == 1 ) + else if ( Init == 1 ) Abc_LatchSetInit1( Abc_NtkBox(pNtkNew, i) ); else + { + assert( Init == Abc_Var2Lit(1+Abc_NtkPiNum(pNtkNew)+i, 0) ); + // unitialized value of the latch is the latch literal according to http://fmv.jku.at/hwmcc11/beyond1.pdf Abc_LatchSetInitDc( Abc_NtkBox(pNtkNew, i) ); + } while ( *pCur != ' ' && *pCur != '\n' ) pCur++; } if ( *pCur != '\n' ) |