mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-11-04 05:19:11 +00:00
Code Activity
6685 commits 124 branches 59 tags 44 MiB
Commit graph

746 commits

Author SHA1 Message Date
Clifford Wolf
10c7709e68 Generate FSM-style testbenches in smtbmc 2017-07-12 15:57:04 +02:00
Clifford Wolf
4a8c131fa7 Fix the fixed handling of x-bits in EDIF back-end 2017-07-11 17:45:29 +02:00
Clifford Wolf
479be3cec7 Fix handling of x-bits in EDIF back-end 2017-07-11 17:38:19 +02:00
Clifford Wolf
9557fd2a36 Add attributes and parameter support to JSON front-end 2017-07-10 13:17:38 +02:00
Clifford Wolf
3c693b6561 Change s/asserts/assertions/ in yosys-smtbmc log messages 2017-07-07 11:52:25 +02:00
Clifford Wolf
8f7404f82c Add "yosys-smtbmc --presat" 2017-07-07 02:47:30 +02:00
Clifford Wolf
5442554e6f Fix generation of multiple outputs for same AIG node in write_aiger 2017-07-05 14:23:54 +02:00
Clifford Wolf
37af6294bd Add write_table command 2017-07-05 12:13:53 +02:00
Clifford Wolf
3e0948e16f Remove unneeded delays in smtbmc vlogtb 2017-07-03 15:37:17 +02:00
Clifford Wolf
287831dca3 Include output ports with constant driver in AIGER output 2017-07-03 14:53:17 +02:00
Clifford Wolf
ea805af6f5 Add "yosys-smtbmc --vlogtb-top" 2017-07-01 18:19:23 +02:00
Clifford Wolf
7d2fb6e2fc Fix smtbmc vlogtb bug in $anyseq handling 2017-07-01 02:13:32 +02:00
Clifford Wolf
8f8baccfde Fix generation of vlogtb output in yosys-smtbmc for "rand reg" and "rand const reg" 2017-06-07 12:30:24 +02:00
Clifford Wolf
c365e33fd7 Fix AIGER back-end for multiple symbols per input/latch/output/property 2017-05-30 19:09:11 +02:00
Clifford Wolf
9ed4c9d710 Improve write_aiger handling of unconnected nets and constants 2017-05-28 11:31:35 +02:00
Clifford Wolf
d9201b85f3 Change default smt2 solver to yices (Yices 2 has switched its license to GPL) 2017-05-27 11:56:01 +02:00
Clifford Wolf
2122ae69b3 Add workaround for CBMC bug to SimpleC back-end 2017-05-17 21:07:54 +02:00
Clifford Wolf
05cdd58c8d Add $_ANDNOT_ and $_ORNOT_ gates 2017-05-17 09:08:29 +02:00
Clifford Wolf
9f4fbc5e74 Add <modname>_init() function generator to simpleC back-end 2017-05-16 19:34:07 +02:00
Clifford Wolf
35be567605 Improve simplec back-end 2017-05-16 08:50:23 +02:00
Clifford Wolf
8d3c706459 Improve simplec back-end 2017-05-15 13:21:59 +02:00
Clifford Wolf
9c397ea78b Improve simplec back-end 2017-05-14 13:14:49 +02:00
Clifford Wolf
628daab277 Improve simplec back-end 2017-05-13 18:47:31 +02:00
Clifford Wolf
ef7594ce3d Improve simplec back-end 2017-05-12 22:39:16 +02:00
Clifford Wolf
7931e1ebb4 Added support for more gate types to simplec back-end 2017-05-12 17:42:31 +02:00
Clifford Wolf
bd4ed19887 Add first draft of simple C back-end 2017-05-12 14:13:33 +02:00
Clifford Wolf
1a4b7c6bfa Fix boolector support in yosys-smtbmc 2017-05-08 14:33:22 +02:00
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