Commit Graph

369 Commits

Author SHA1 Message Date
Clifford Wolf 106e44f406 Add "write_smt2 -stdt" mode 2017-03-20 12:00:35 +01:00
Clifford Wolf 0ac72e759d Add generation of logic cells to EDIF back-end runtest.py 2017-03-19 14:57:40 +01:00
Clifford Wolf 850f8299a9 Fix EDIF: portRef member 0 is always the MSB bit 2017-03-19 14:53:28 +01:00
Clifford Wolf 1390e9a0a7 Add simple EDIF test case generator and checker 2017-03-18 15:00:03 +01:00
Clifford Wolf c855353986 Improve smt2 encodings of assert/assume/cover, better wire_smt2 help msg 2017-03-04 23:41:54 +01:00
Clifford Wolf a6ca28276e Add write_aiger $anyseq support 2017-03-02 16:39:48 +01:00
Clifford Wolf fbd52ec6dd Use hex addresses in smtbmc vcd mem traces 2017-02-28 13:54:50 +01:00
Clifford Wolf 2203562268 Add smtbmc support for memory vcd dumping 2017-02-26 21:26:32 +01:00
Clifford Wolf 80ecd7a26f Fix extra newline bug in write_smt2 2017-02-26 14:41:27 +01:00
Clifford Wolf 6e152f7aa1 Fix bug in smtio unroll code 2017-02-26 14:39:07 +01:00
Clifford Wolf 66a1617b69 Fix assert checking in "yosys-smtbmc -c --append" 2017-02-26 11:06:26 +01:00
Clifford Wolf fd1cc0c73d Improve (and fix for stbv mode) SMT2 memory API 2017-02-26 10:58:34 +01:00
Clifford Wolf 38bf458037 Add support for "yosys-smtbmc -c --append" 2017-02-25 23:41:40 +01:00
Clifford Wolf c7d1286728 Improve "write_edif" help message 2017-02-25 16:35:53 +01:00
Clifford Wolf dfddf391f9 Move EdifNames out of double-private namespace 2017-02-25 16:29:27 +01:00
Clifford Wolf 8c61ecdd6e Clean up edif code, swap bit indexing of "upto" ports 2017-02-25 16:28:34 +01:00
Clifford Wolf b76c89a5dd Merge branch 'master' of https://github.com/klammerj/yosys into klammerj-master 2017-02-25 15:59:02 +01:00
Clifford Wolf dac0842d61 Add $live and $fair support to AIGER back-end. 2017-02-25 13:07:15 +01:00
Clifford Wolf 7af9727f78 Add "write_smt2 -stbv" 2017-02-24 18:24:53 +01:00
Clifford Wolf a9c3acf5a2 Add SMT2 statebv mode (inactive for now) 2017-02-24 14:04:52 +01:00
Johann Klammer 6d7a77dbf6 Did as you requested, /but/...
Now the nets are wired in reverse again because the netlister still uses zero-based indices.
2017-02-24 13:18:49 +01:00
Johann Klammer 06df86aae3 add options for edif flavors
*to force renames on wide ports
*to choose array delimiters
*to choose up or downwards indices
2017-02-23 19:42:37 +01:00
Clifford Wolf 242c5f01de Add "yosys-smtbmc -S <opt>" 2017-02-19 22:51:29 +01:00
Clifford Wolf 4e80ce97a8 Add warning about x/z bits left unconnected in EDIF output 2017-02-14 12:49:35 +01:00
Adam Izraelevitz 794cec0016 More progress on Firrtl backend.
Chisel -> Firrtl -> Verilog -> Firrtl -> Verilog is successful for a
simple rocket-chip design.
2017-02-13 11:17:53 -08:00
Clifford Wolf 5541b42159 Add assert check in "yosys-smtbmc -c" 2017-02-04 21:22:17 +01:00
Clifford Wolf adbecfee66 Improve yosys-smtbmc cover() support 2017-02-04 21:10:24 +01:00
Clifford Wolf 0c0784b6bf Partially implement cover() support in yosys-smtbmc 2017-02-04 18:17:08 +01:00
Clifford Wolf 6abf79eb28 Further improve cover() support 2017-02-04 17:02:13 +01:00
Clifford Wolf 18ea65ef04 Add "yosys-smtbmc --aig <aim_filename>:<aiw_filename>" support 2017-01-30 11:38:43 +01:00
Clifford Wolf e54c355b41 Add "yosys-smtbmc --aig-noheader" and AIGER mem init support 2017-01-28 15:15:02 +01:00
Clifford Wolf b7cfb7dbd2 Fix $initstate handling bug in yosys-smtbmc 2017-01-11 14:14:12 +01:00
Clifford Wolf b9ad91b93e Implicitly set "yosys-smtbmc --noprogress" on windows 2017-01-04 15:23:48 +01:00
Clifford Wolf ed812ea39c Fixed "yosys-smtbmc --noprogress" 2017-01-04 12:03:04 +01:00
Clifford Wolf 81bb952e5d Handle "always 1" like "always -1" in .smtc files 2017-01-02 20:08:03 +01:00
Clifford Wolf 2198948398 Improved write_json help message 2016-12-29 12:13:29 +01:00
Clifford Wolf a61c88f122 Added $anyconst support to AIGER back-end 2016-12-11 13:48:18 +01:00
Clifford Wolf a44cc7a3d1 Added $assert/$assume support to AIGER back-end 2016-12-03 13:20:29 +01:00
Clifford Wolf 37760541bd Improved yosys-smtbmc default -t/--assume-skipped for --cex and --aig 2016-12-03 12:37:20 +01:00
Clifford Wolf 88b9733253 Added "yosys-smtbmc --aig" 2016-12-01 13:16:57 +01:00
Clifford Wolf 52c243cf05 Added support for partially initialized regs to smt2 back-end 2016-12-01 12:00:00 +01:00
Clifford Wolf 5fa1fa1e6f Added "write_aiger -zinit -symbols -vmap" 2016-12-01 11:04:36 +01:00
Clifford Wolf c1f762ca56 Added "write_aiger" command 2016-11-30 21:30:24 +01:00
Clifford Wolf df2e5aad6f Bugfix in smt2 back-end for pure checker modules 2016-11-28 15:15:09 +01:00
Clifford Wolf c17d98f55c Removed shebang line from smtio.py, fixes #279 2016-11-27 12:11:04 +01:00
Clifford Wolf 5c2c78e2dd Added wire start_offset and upto handling BLIF back-end 2016-11-23 13:54:33 +01:00
Clifford Wolf f257ccf22e Added "yosys-smtbmc --append" 2016-11-22 21:21:13 +01:00
Adam Izraelevitz f77dc3bacc Bugfix: include assign to write-mask 2016-11-18 11:49:26 -08:00
Clifford Wolf e01382739d More progress in FIRRTL back-end 2016-11-18 02:41:29 +01:00
Clifford Wolf c051115e03 Progress in FIRRTL back-end 2016-11-18 00:32:35 +01:00