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
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