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
Clifford Wolf
da56a5bbc6
Added $initstate support to smtbmc flow
2016-07-27 16:11:37 +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
0bc95f1e04
Added "yosys -D" feature
2016-04-21 23:28:37 +02: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
302166dd59
Improvements in yosys-smtbmc
2015-10-15 15:10:33 +02:00
Clifford Wolf
3a22b31bda
Added write_smt2 -wires
2015-10-13 17:17:12 +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
Clifford Wolf
698357dd9a
Added "write_smt2 -regs"
2015-08-12 17:13:54 +02:00
Clifford Wolf
883e09d8ed
Use MEMID as name for $mem cell
2015-08-09 13:35:44 +02:00
Clifford Wolf
6c84341f22
Fixed trailing whitespaces
2015-07-02 11:14:30 +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
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
e8c12e5f0c
Various fixes and improvements in "write_smt2 -bv"
2014-12-25 20:28:34 +01:00
Clifford Wolf
68233baa1f
Various fixes and improvements in write_smt2
2014-12-25 17:52:31 +01:00
Clifford Wolf
95f17dbab0
Added support for most BV cell types to write_smt2
2014-12-25 15:37:02 +01:00
Clifford Wolf
1c3d51375f
Added "write_smt2 -bv" and other write_smt2 improvements
2014-12-25 13:30:20 +01:00
Clifford Wolf
e548483c91
Added write_smt2 (only gate level logic supported so far)
2014-12-24 16:17:57 +01:00