Commit Graph

220 Commits

Author SHA1 Message Date
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
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