Commit Graph

399 Commits

Author SHA1 Message Date
Clifford Wolf 2e244c2d8e Added yosys-smtbmc --noinfo and --dummy 2016-09-19 20:43:28 +02:00
Clifford Wolf d009cdd6ee Improved handling of SMT2 logics in yosys-smtbmc 2016-09-18 20:48:09 +02:00
Clifford Wolf 7bc88e8101 yosys-smtbmc: added -i support smtc files 2016-09-18 00:48:36 +02:00
Clifford Wolf d39db41df8 Work-around for boolector bug 2016-09-13 13:23:06 +02:00
Clifford Wolf 6f416c1953 Added missing :produce-models setting to smtio.py 2016-09-11 18:17:22 +02:00
Clifford Wolf 5199aafca0 Minor improvements to smtio.py vcd writer 2016-09-10 16:24:08 +02:00
Clifford Wolf b582f11074 fixed write_smt2 for (non-combinatorial) loops through hierarchical cells 2016-09-10 15:14:41 +02:00
Clifford Wolf 3ceba145d5 smt2 mem init bugfix 2016-09-08 18:08:15 +02:00
Clifford Wolf 14bfd3c5c1 yosys-smtbmc meminit support 2016-09-08 11:16:12 +02:00
Clifford Wolf 209a3d9ffc Bugfix in "yosys-smtbmc --unroll" 2016-09-07 21:01:51 +02:00
Clifford Wolf 6770d6e0f8 Added "yosys-smtbmc --unroll" 2016-09-07 20:57:56 +02:00
Clifford Wolf 97b449fe55 yosys-smtbmc: flush stdout after each log msg 2016-09-06 01:40:31 +02:00
Clifford Wolf 372d672c2a Minor bugfix in write_smt2 2016-09-04 16:32:47 +02:00
Clifford Wolf fa5565b606 Added boolector support to yosys-smtbmc 2016-09-03 14:26:00 +02:00
Clifford Wolf 948aac9e1e Don't re-create hex_dict for each value 2016-09-02 13:46:56 +02:00
Kaj Tuomi d88cd0ae7f More PEP 8 fixes. 2016-09-02 13:09:09 +03:00
Kaj Tuomi c4ba1965fd Indentation and PEP 8 fixes. CamelCase and white space after semicolon. 2016-09-02 13:01:31 +03:00
Kaj Tuomi 2343dda946 Use dict lookup instead of many ifs. 2016-09-02 12:50:23 +03:00
Kaj Tuomi 279298c0b8 Fix: Unresolved reference. 2016-09-02 11:12:30 +03:00
Kaj Tuomi 74dd36ad55 Some syntax fixes. Generator and comma separated list modifications. 2016-09-02 11:02:19 +03:00
Clifford Wolf aa25a4cec6 Added $anyconst support to yosys-smtbmc 2016-08-30 19:27:42 +02:00
Clifford Wolf a8124c137e Fixed memory bug in write_smt2 2016-08-30 14:49:47 +02:00
Clifford Wolf b04a40d9fe Made "write_smt2 -bv -mem" default, added "write_smt2 -nobv -nomem" 2016-08-30 12:40:09 +02:00
Clifford Wolf 39e4faa2e4 Added $anyconst support to smt2 back-end 2016-08-30 11:26:10 +02:00
Clifford Wolf c417421495 Added "yosys-smtbmc --dump-all" 2016-08-29 22:41:45 +02:00
Clifford Wolf b226893461 More yosys-smtbmc bugfixes 2016-08-29 14:53:32 +02:00
Clifford Wolf a2e2fc5980 Various fixes and improvements in yosys-smtbmc 2016-08-29 13:53:12 +02:00
Clifford Wolf f56dba8e20 Some changes to yosys-smtbmc cmd line options, add --final-only 2016-08-27 22:04:15 +02:00
Clifford Wolf adcda6817e Added smtc "final" statement 2016-08-27 14:30:36 +02:00
Clifford Wolf 17233b11e1 Various fixes and improvements in smt2 back-end 2016-08-26 17:33:02 +02:00
Clifford Wolf ad56ad44c3 More yosys-smtbmc smtc features 2016-08-24 23:18:29 +02:00
Clifford Wolf ee3e7a0e45 yosys-smtbmc --smtc -g 2016-08-24 22:09:50 +02:00
Clifford Wolf 6523023645 Minor yosys-smtbmc bugfix 2016-08-22 17:45:01 +02:00
Clifford Wolf 583ceee6eb Added "yosys-smtbmc --constr" 2016-08-22 17:27:43 +02:00
Clifford Wolf 2bd30e2026 Added "yosys-smtbmc --dump-constr" 2016-08-22 16:48:46 +02:00
Clifford Wolf 7a33b9892a yosys-smtbmc: improved --dump-vlogtb handling of memories 2016-08-21 15:56:22 +02:00
Clifford Wolf f7578b0239 Added "yosys-smtbmc --dump-vlogtb" 2016-08-20 18:43:39 +02:00
Clifford Wolf ed785194de Added support for memories to smtio.py 2016-08-20 18:42:32 +02:00
Clifford Wolf c325bae792 Deprecated "write_smt2 -regs" (by default on now), and some other smt2 back-end improvements 2016-08-20 18:41:57 +02:00
Clifford Wolf 28271e43c9 Added "yosys-smtbmc -g" 2016-08-20 16:32:50 +02:00
Clifford Wolf a889acb897 Added smtbmc longopt support 2016-08-20 16:07:59 +02:00
Clifford Wolf 75bf7416f0 Bugfix in partial mem write handling in verilog back-end 2016-08-20 13:06:06 +02:00
Clifford Wolf 9b8e06bee1 Added missing support for mem read enable ports to verilog back-end 2016-08-18 21:47:02 +02:00
Clifford Wolf de8ee412c3 Improved smtbmc vcd generation performance 2016-08-18 11:17:45 +02:00
Clifford Wolf dfcd30ea86 Added printing of code loc of failed asserts to yosys-smtbmc 2016-08-17 20:10:02 +02:00
Clifford Wolf f0a8713fea Fixed upto handling in verilog back-end 2016-08-15 08:26:20 +02:00
Clifford Wolf 21e1bac084 Merge branch 'master' of github.com:cliffordwolf/yosys 2016-07-30 12:50:39 +02:00
Clifford Wolf 5fe13a16ea Added "write_verilog -defparam" 2016-07-30 12:46:06 +02:00
Clifford Wolf 7fa61cba1b Added "write_verilog -nodec -nostr" 2016-07-30 12:38:40 +02:00
Clifford Wolf da56a5bbc6 Added $initstate support to smtbmc flow 2016-07-27 16:11:37 +02:00
whitequark 546233f0e1 write_json: also write module attributes. 2016-07-12 06:32:04 +00:00
Clifford Wolf c71785d65e Yosys-smtbmc: Support for hierarchical VCD dumping 2016-07-11 12:49:33 +02:00
Clifford Wolf 0153ad85d9 Moved smt2 yosys info parsing from smtbmc.py to smtio.py 2016-07-11 11:49:05 +02:00
Clifford Wolf 771c5fe000 Support for hierarchical designs in smt2 back-end 2016-07-10 18:11:25 +02:00
Clifford Wolf 27b5347a87 Restored blif "-true - .." behavior, use "-true + .." for eddiehung-vtr behavior 2016-07-08 11:51:04 +02:00
Clifford Wolf 72149aba2e In BLIF, a .names without entries already always outputs 0 2016-07-08 11:41:26 +02:00
Clifford Wolf f6b7cf23d6 Merge branch 'yosys-0.5-vtr' of https://github.com/eddiehung/yosys into eddiehung-vtr 2016-07-08 11:32:36 +02:00
Clifford Wolf 5ffad4e073 Added $sop support to BLIF back-end 2016-06-18 12:28:49 +02:00
Clifford Wolf f3983a0940 Also escape "=" in spice output 2016-05-20 16:43:13 +02:00
Clifford Wolf d10dfccabb Added "write_blif -noalias" 2016-05-06 15:05:53 +02:00
Clifford Wolf 60ac1bd178 Added support for "active high" and "active low" latches in BLIF back-end 2016-04-22 18:00:46 +02:00
Clifford Wolf 0bc95f1e04 Added "yosys -D" feature 2016-04-21 23:28:37 +02:00
Clifford Wolf 3920bf58d0 Fixed some typos 2016-04-05 08:18:21 +02:00
Clifford Wolf 1d0f0d668a Renamed opt_const to opt_expr 2016-03-31 08:46:56 +02:00
Clifford Wolf 2a8d5e64f5 Bugfix in write_verilog for RTLIL processes 2016-03-14 13:03:28 +01:00
Clifford Wolf d117893007 Added "write_edif -nogndvcc" 2016-03-08 21:30:45 +01:00
Clifford Wolf 5547fae4cf Be more conservative with net names in spice output 2016-03-02 12:02:59 +01:00
Sebastian Kuzminsky 7e6426a67d user-facing spelling fixes
"speciefied" -> "specified"
"unkown" -> "unknown"
2016-02-28 15:14:01 -07:00
Clifford Wolf 0d7fd2585e Added "int ceil_log2(int)" function 2016-02-13 16:52:16 +01:00
Clifford Wolf 4393a8ffbf Added "write_blif -cname" mode 2016-01-06 14:32:28 +01:00
Clifford Wolf 47fac573cf Added yosys-smtbmc -S 2015-12-20 09:58:54 +01:00
Clifford Wolf 207736b4ee Import more std:: stuff into Yosys namespace 2015-10-25 19:30:49 +01:00
Clifford Wolf 7f110e7018 renamed SigSpec::to_single_sigbit() to SigSpec::as_bit(), added is_bit() 2015-10-24 22:56:40 +02:00
Clifford Wolf 255bb914ba Progress in yosys-smtbmc 2015-10-15 15:54:59 +02:00
Clifford Wolf 302166dd59 Improvements in yosys-smtbmc 2015-10-15 15:10:33 +02:00
Clifford Wolf 5dd3e93e8f More "yosys-smtbmc -c" fixes 2015-10-14 23:23:25 +02:00
Clifford Wolf 9fd0f87059 Fixed yosys-smtbmc -c 2015-10-14 23:00:46 +02:00
Clifford Wolf 3c31572152 Added yosys-smtbmc copyright 2015-10-14 01:31:54 +02:00
Clifford Wolf d7de0f4bd1 Improvements in yosys-smtbmc 2015-10-14 01:27:55 +02:00
Clifford Wolf 821f1b8534 Added yosys-smtbmc 2015-10-14 00:47:04 +02:00
Clifford Wolf 7bcd2a4bb3 Implemented smtbmc.py -i 2015-10-14 00:18:38 +02:00
Clifford Wolf 29160525aa Added smtbmc.py 2015-10-13 17:17:23 +02:00
Clifford Wolf 3a22b31bda Added write_smt2 -wires 2015-10-13 17:17:12 +02:00
Clifford Wolf 4ac202e2a5 Bugfixes in writing of memories as Verilog 2015-09-25 13:49:26 +02:00
Clifford Wolf 09b51cb375 Added "yosys-smt2-wire" tag support to smt2 back-end 2015-08-31 02:05:58 +02:00
Clifford Wolf b659ffb457 Fixed generation of smt2 concat statements 2015-08-15 11:45:44 +02:00
Larry Doolittle 6c00704a5e Another block of spelling fixes
Smaller this time
2015-08-14 23:27:05 +02:00
Clifford Wolf 0350074819 Re-created command-reference-manual.tex, copied some doc fixes to online help 2015-08-14 11:27:19 +02:00
Clifford Wolf 84bf862f7c Spell check (by Larry Doolittle) 2015-08-14 10:56:05 +02:00
Clifford Wolf 698357dd9a Added "write_smt2 -regs" 2015-08-12 17:13:54 +02:00
Clifford Wolf f81bf9bdea Added SMV back-end 'test_cells.sh' script 2015-08-12 12:56:20 +02:00
Clifford Wolf 883e09d8ed Use MEMID as name for $mem cell 2015-08-09 13:35:44 +02:00
Clifford Wolf 6834461f65 Remove some very strange whitespace in btor.cc (by Larry Doolittle) 2015-08-05 22:11:26 +02:00
Clifford Wolf 5dc23975eb Bugfix in SMV back-end for partially unassigned wires 2015-08-05 11:36:26 +02:00
Clifford Wolf c7fd3fbb68 Added $assert support to SMV back-end 2015-08-04 20:05:37 +02:00
Clifford Wolf eac0bcd7d3 Improvements in BLIF back-end 2015-07-29 17:06:19 +02:00
Clifford Wolf 6c84341f22 Fixed trailing whitespaces 2015-07-02 11:14:30 +02:00
Clifford Wolf 3123c45415 Added init support to SMV back-end 2015-06-19 16:43:02 +02:00
Clifford Wolf 6c6bf4999e Progress in SMV back-end 2015-06-19 16:26:53 +02:00
Clifford Wolf 8c79765de5 Progress in SMV back-end 2015-06-19 14:08:46 +02:00
Clifford Wolf 8a86162ae9 Progress in SMV back-end 2015-06-18 16:29:11 +02:00
Clifford Wolf 8e84418225 Progress in SMV back-end 2015-06-17 09:56:42 +02:00
Clifford Wolf 9f7a5b4ef9 Progress in SMV back-end 2015-06-17 07:24:27 +02:00
Clifford Wolf b8c5e27006 Progress in SMV back-end 2015-06-16 19:05:26 +02:00
Clifford Wolf 52315039c5 Progress in SMV back-end 2015-06-15 17:01:01 +02:00
Clifford Wolf 0f01ef61ef Progress in SMV back-end 2015-06-15 13:24:17 +02:00
Clifford Wolf ea23bb8aa4 Added "write_smv" skeleton 2015-06-15 00:46:27 +02:00
Clifford Wolf 93685a77c6 Removed debug code from write_smt2 2015-06-14 16:22:06 +02:00
Clifford Wolf 255dcb27a0 Added write_smt2 -mem 2015-06-14 15:46:47 +02:00
Clifford Wolf 4c733301e6 Fixed cstr_buf for std::string with small string optimization 2015-06-11 13:39:49 +02:00
Clifford Wolf 3a6abc9bf6 Improvements in cellaigs.cc and "json -aig" 2015-06-11 10:48:16 +02:00
Clifford Wolf 1ae360cf72 AigMaker refactoring 2015-06-10 23:00:12 +02:00
Clifford Wolf e534881794 Added "json -aig" 2015-06-10 08:13:56 +02:00
luke whittlesey 2f90499e3d $mem cell in verilog backend : grouped writes by clock 2015-06-08 17:35:40 -04:00
luke whittlesey a8fe040906 Bug fix in $mem verilog backend + changed tests/bram flow of make test. 2015-06-04 16:12:40 -04:00
Clifford Wolf 08a4af3cde Improvements in BLIF front-end 2015-05-24 08:03:21 +02:00
Clifford Wolf 4744bb95fb Some fixes for $mem in verilog back-end 2015-05-20 13:55:50 +02:00
Clifford Wolf 42348cddd9 Merge pull request #63 from wluker/verilog-backend-mem
Fixed bug in $mem cell verilog code generation.
2015-05-11 21:38:06 +02:00
luke whittlesey 3bb5f064b8 Fixed bug in $mem cell verilog code generation. 2015-05-11 14:05:18 -04:00
Clifford Wolf 9e56739634 Disabled broken $mem support in verilog backend 2015-05-10 21:38:41 +02:00
luke whittlesey 6de8fea2c7 Made changes recommended by Clifford Wolf ...
Removed bit_check_equal(), used RTLIL::SigBit for individual bits, used
dict<> instead of std::map, and used RTLIL::SigSpec instead of
std::vector.
2015-05-10 11:33:24 -04:00
luke whittlesey 2c1e150297 Verilog backend for $mem cells should now be able to handle different
write-enable bits and RD_TRANSPARENT parameter settings.
2015-05-08 15:29:51 -04:00
luke whittlesey c0b68f4848 Added support for $mem cells in the verilog backend. 2015-05-07 13:03:09 -04:00
eddiehung 7c62318239 Fix for all zero mask 2015-05-03 12:53:09 +01:00
eddiehung 079c1205fe Escape '<' and '>' some more 2015-05-03 10:37:20 +01:00
eddiehung 872e13321c For vtr, escape angle brackets as well 2015-04-28 08:56:00 +01:00
eddiehung 058deb777e blifwriter: write out .names for true/false/undef type == '-' 2015-04-28 08:55:26 +01:00
Clifford Wolf d176e613c2 Minor fixes in handling of "init" attribute 2015-04-09 15:12:26 +02:00
Clifford Wolf aa0ab975b9 Removed "techmap -share_map" (use "-map +/filename" instead) 2015-04-08 12:13:53 +02:00
Clifford Wolf c0e2b3eb11 Added "port_directions" to write_json output 2015-04-06 01:49:58 +02:00
Clifford Wolf b0c0ede879 Added "init" attribute support to verilog backend 2015-04-04 18:06:52 +02:00
Ahmed Irfan 13e2e71ebe Update README
corrected url
2015-04-03 17:11:45 +02:00
Ahmed Irfan ed750f0a55 Delete btor.ys
.ys script not needed
2015-04-03 16:45:54 +02:00
Ahmed Irfan e82e4f7df4 Update README
pmux cell is implemented
2015-04-03 16:45:14 +02:00
Ahmed Irfan ea2e0297d5 separated memory next from write cell 2015-04-03 16:41:50 +02:00
Clifford Wolf 67e6dcd34a Added Verilog backend $dffsr support 2015-03-18 08:01:37 +01:00
Clifford Wolf 6c8fdb1829 Documentation for JSON format, added attributes 2015-03-06 10:21:21 +01:00
Clifford Wolf adc12ce46e Json bugfix 2015-03-03 09:41:41 +01:00
Clifford Wolf 4fc63f27a1 Json backend improvements 2015-03-03 09:28:44 +01:00
Clifford Wolf 795a6e1d04 Added write_blif -attr 2015-03-02 23:47:45 +01:00
Clifford Wolf 8b488983d0 Added JSON backend 2015-03-02 23:30:58 +01:00
Clifford Wolf 5d4f513c3b Added $assume support to write_smt2 2015-02-26 19:02:55 +01:00
Clifford Wolf ff3f2448b1 Minor "write_smt2" help msg change 2015-02-22 16:30:02 +01:00
Clifford Wolf 4b89dd983c Added "<mod>_a" and "<mod>_i" to write_smt2 output 2015-02-22 16:19:10 +01:00
Clifford Wolf 756b4064b2 Fixed "write_verilog -attr2comment" handling of "*/" in strings 2015-02-13 22:48:10 +01:00
Clifford Wolf 6978f3a77b Added EDIF backend support for multi-bit cell ports 2015-02-01 15:43:35 +01:00
Clifford Wolf fb8c755726 Shorter "dump" options 2015-01-31 23:52:36 +01:00
Clifford Wolf 2a9ad48eb6 Added ENABLE_NDEBUG makefile options 2015-01-24 12:16:46 +01:00
Clifford Wolf 43951099cf Added dict/pool.sort() 2015-01-24 00:13:27 +01:00
Clifford Wolf 146f769bee Cosmetic changes in verilog output format 2015-01-02 22:57:08 +01:00