mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-10-20 14:20:32 +00:00
Code Activity
15794 commits 121 branches 59 tags 69 MiB
Commit graph

123 commits

Author SHA1 Message Date
Alberto Gonzalez
07f0874779 Clean up pseudo-private member usage in backends/smt2/smt2.cc. 2020-03-13 21:49:12 +00:00
Alberto Gonzalez
0fda8308bc Add support for optimizing exists-forall problems. 
Modifies smt2 backend to recognize `$anyconst` etc. assigned to a wire with the `maximize` or `minimize` attribute and emit `; yosys-smt2-maximize` or `; yosys-smt2-minimize` directives as appropriate.
Modifies `backends/smt2/smtbmc.py` and `smtio.py` to recognize those directives and emit a `(maximize ...)` or `(minimize ...)` command at the end of `smt_forall_assert()`, as described in the paper "νZ - An Optimizing SMT Solver" by Nikolaj Bjørner et al.
Adds an example `examples/smtbmc/demo9.v` to show how it can be used.
 2020-03-13 17:10:29 +00:00
Eddie Hung
6d77236f38 substr() -> compare() 2019-08-07 12:20:08 -07:00
Eddie Hung
3486235338 Make liberal use of IdString.in() 2019-08-06 16:18:18 -07:00
Clifford Wolf
023086bd46 Add $_NMUX_, add "abc -g cmos", add proper cmos cell costs 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2019-08-06 04:47:55 +02:00
Clifford Wolf
f4abc21d8a Add "whitebox" attribute, add "read_verilog -wb" 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2019-04-18 17:45:47 +02:00
Clifford Wolf
94f995ee37 Fix signed $shift/$shiftx handling in write_smt2 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2019-03-09 13:19:41 -08:00
Clifford Wolf
5dfc7becca Use SVA label in smt export if available 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2019-03-07 11:31:46 -08:00
Clifford Wolf
f570aa5e1d Fix smt2 code generation for partially initialized memowy words, fixes #831 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2019-02-28 12:15:58 -08:00
Clifford Wolf
b6781c6f4b Add support for signed $shift/$shiftx in smt2 back-end 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-11-01 11:40:58 +01:00
Henner Zeller
3aa4484a3c Consistent use of 'override' for virtual methods in derived classes. 
o Not all derived methods were marked 'override', but it is a great
  feature of C++11 that we should make use of.
o While at it: touched header files got a -*- c++ -*- for emacs to
  provide support for that language.
o use YS_OVERRIDE for all override keywords (though we should probably
  use the plain keyword going forward now that C++11 is established)
 2018-07-20 23:51:06 -07:00
Clifford Wolf
25a864fc73 Fixed -stbv handling in SMT2 back-end 2018-04-04 17:28:07 +02:00
Clifford Wolf
77bd645c35 Add $mem support to SMT2 clock tagging 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-27 02:11:20 +02:00
Clifford Wolf
8b7602e660 Improve SMT2 encoding of $reduce_{and,or,bool} 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-04 21:22:20 +01:00
Clifford Wolf
b13e6bd375 Add smtbmc support for exist-forall problems 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-02-23 19:33:30 +01:00
Clifford Wolf
17583b6a21 Add support for mockup clock signals in yosys-smtbmc vcd output 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-02-20 17:45:22 +01:00
Clifford Wolf
c9672e2e2e Fix handling of zero-length cell connections in SMT2 back-end 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-02-08 19:12:12 +01:00
Clifford Wolf
9419de3e37 Add yosys-smtbmc VCD writer support for memories with async writes 2017-12-14 03:06:00 +01:00
Clifford Wolf
2625da6440 Add smt2 back-end support for async write memories 2017-12-14 02:07:10 +01:00
Clifford Wolf
455c1c9d97 Fix SMT2 handling of initstate in sub-modules 2017-10-29 13:21:20 +01:00
Clifford Wolf
c2d737457a Fix bug in write_smt2 (export logic driving hierarchical cells before exporting regs) 2017-08-25 11:44:48 +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
05cdd58c8d Add $_ANDNOT_ and $_ORNOT_ gates 2017-05-17 09:08:29 +02:00
Clifford Wolf
106e44f406 Add "write_smt2 -stdt" mode 2017-03-20 12:00:35 +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
80ecd7a26f Fix extra newline bug in write_smt2 2017-02-26 14:41:27 +01:00
Clifford Wolf
fd1cc0c73d Improve (and fix for stbv mode) SMT2 memory API 2017-02-26 10:58:34 +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
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
52c243cf05 Added support for partially initialized regs to smt2 back-end 2016-12-01 12:00:00 +01:00
Clifford Wolf
df2e5aad6f Bugfix in smt2 back-end for pure checker modules 2016-11-28 15:15:09 +01:00
Clifford Wolf
189fbd4cf8 cleanup in write_smt2 log messages (-bv and -mem are now default) 2016-10-16 23:02:51 +02:00
Clifford Wolf
bdc316db50 Added $anyseq cell type 2016-10-14 15:24:03 +02:00
Clifford Wolf
8ebba8a35f Added $ff and $_FF_ cell types 2016-10-12 01:18:39 +02:00
Clifford Wolf
d009cdd6ee Improved handling of SMT2 logics in yosys-smtbmc 2016-09-18 20:48:09 +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
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
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
17233b11e1 Various fixes and improvements in smt2 back-end 2016-08-26 17:33:02 +02:00
Clifford Wolf
7a33b9892a yosys-smtbmc: improved --dump-vlogtb handling of memories 2016-08-21 15:56:22 +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
dfcd30ea86 Added printing of code loc of failed asserts to yosys-smtbmc 2016-08-17 20:10:02 +02:00