a5e1d3b997
formalff: Set new replaced_by_gclk attribute on removed dff's clks
...
This attribute can be used by formal backends to indicate which clocks
were mapped to the global clock. Update the btor and smt2 backend which
already handle clock inputs to understand this attribute.
2022-08-16 13:37:30 +02:00
930bcf0e75
smt2, btor: Revert calling memory_map -rom-only
...
This approach had major issues with ROMs whose initialization was not
fully defined. If required, memory_map -rom-only -keepdc should be
called early in a formal flow instead. (This does require a careful
choice of optimization passes though. Sby's scripts will be updated
accordingly.)
2022-06-29 18:28:34 +02:00
d78d807a7f
memory_map: -keepdc option for formal
...
Use it when invoking memory_map -rom-only from write_{smt2,btor}.
2022-06-27 15:47:55 +02:00
de5c4bf523
btor: add support for $pos cell
2022-06-20 16:40:46 -07:00
4adef63cd4
smt2, btor: Use memory_map -rom-only to make ROMs usable for k-induction
...
This avoids provability regressions now that we infer more ROMs.
This fixes #3378
2022-06-17 17:23:13 +02:00
3fb32540ea
Add propagated clock signals into btor info file
2022-05-04 08:10:18 +02:00
d340f302f6
Fix handling of some formal cells in btor back-end
...
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2022-03-11 14:21:12 +01:00
ebe2ee431e
handle state names of $anyconst and $anyseq
2022-03-11 14:04:02 +01:00
93508d58da
Add $bmux and $demux cells.
2022-01-28 23:34:41 +01:00
e7d89e653c
Hook up $aldff support in various passes.
2021-10-02 21:01:21 +02:00
72787f52fc
Fixing old e-mail addresses and deadnames
...
s/((Claire|Xen|Xenia|Clifford)\s+)+(Wolf|Xen)\s+<(claire|clifford)@(symbioticeda.com|clifford.at|yosyshq.com)>/Claire Xenia Wolf <claire@yosyshq.com>/gi;
s/((Nina|Nak|N\.)\s+)+Engelhardt\s+<nak@(symbioticeda.com|yosyshq.com)>/N. Engelhardt <nak@yosyshq.com>/gi;
s/((David)\s+)+Shah\s+<(dave|david)@(symbioticeda.com|yosyshq.com|ds0.me)>/David Shah <dave@ds0.me>/gi;
s/((Miodrag)\s+)+Milanovic\s+<(miodrag|micko)@(symbioticeda.com|yosyshq.com)>/Miodrag Milanovic <micko@yosyshq.com>/gi;
s,https?://www.clifford.at/yosys/,http://yosyshq.net/yosys/,g ;
2021-06-08 00:39:36 +02:00
cbf6b719fe
Make a few passes auto-call Mem::narrow instead of rejecting wide ports.
...
This essentially adds wide port support for free in passes that don't
have a usefully better way of handling wide ports than just breaking
them up to narrow ports, avoiding "please run memory_narrow" annoyance.
2021-05-28 00:40:56 +02:00
69bf5c81c7
Reject wide ports in some passes that will never support them.
2021-05-25 02:07:25 +02:00
33513d923a
btor: Use is_mem_cell in one more place.
2021-05-23 20:34:52 +02:00
c4cc888b2c
kernel/rtlil: Extract some helpers for checking memory cell types.
...
There will soon be more (versioned) memory cells, so handle passes that
only care if a cell is memory-related by a simple helper call instead of
a hardcoded list.
2021-05-22 21:43:00 +02:00
979347999f
btor, smt2, smv: Add a hint on how to deal with funny FF types.
2021-02-25 22:04:04 +01:00
2d340cd355
btor: Use Mem helper.
2020-10-21 17:51:20 +02:00
6224fd9055
Add missing gitignores for test artifacts
2020-08-31 19:43:51 +02:00
928fd40c2e
Respect \A_SIGNED for $shift
...
This reflects the behaviour of $shr/$shl, which sign-extend their A
operands to the size of their output, then do a logical shift (shift in
0-bits).
2020-08-18 19:36:24 +02:00
7191dd16f9
Use C++11 final/override keywords.
2020-06-18 23:34:52 +00:00
82798ae575
btor backend: make not printing internal names default
2020-06-04 16:24:16 +02:00
5e8a9c61cd
Add printf format attributes to btorf/infof helper functions
...
Signed-off-by: Claire Wolf <claire@symbioticeda.com>
2020-06-04 15:53:28 +02:00
8ceb6686e0
btor backend: add option to not include internal names
2020-06-04 14:00:52 +02:00
edd8ff2c07
Add flooring division operator
...
The $div and $mod cells use truncating division semantics (rounding
towards 0), as defined by e.g. Verilog. Another rounding mode, flooring
(rounding towards negative infinity), can be used in e.g. VHDL. The
new $divfloor cell provides this flooring division.
This commit also fixes the handling of $div in opt_expr, which was
previously optimized as if it was $divfloor.
2020-05-28 22:59:04 +02:00
17163cf43a
Add flooring modulo operator
...
The $div and $mod cells use truncating division semantics (rounding
towards 0), as defined by e.g. Verilog. Another rounding mode, flooring
(rounding towards negative infinity), can be used in e.g. VHDL. The
new $modfloor cell provides this flooring modulo (also known as "remainder"
in several languages, but this name is ambiguous).
This commit also fixes the handling of $mod in opt_expr, which was
previously optimized as if it was $modfloor.
2020-05-28 22:59:03 +02:00
956ecd48f7
kernel: big fat patch to use more ID::*, otherwise ID(*)
2020-04-02 09:51:32 -07:00
dde3dfd72e
Update backends/btor/btor.cc; credit @boqwxp
...
Co-Authored-By: Alberto Gonzalez <61295559+boqwxp@users.noreply.github.com>
2020-04-02 07:14:08 -07:00
fdafb74eb7
kernel: use more ID::*
2020-04-02 07:14:08 -07:00
bf018b184d
Improve write_btor symbol handling
...
Signed-off-by: Claire Wolf <claire@symbioticeda.com>
2020-03-14 15:49:43 +01:00
29e2b2dc05
Add info-file and cover features to write_btor
...
Signed-off-by: Claire Wolf <claire@symbioticeda.com>
2020-03-13 13:46:32 +01:00
cd44826d50
Use cell name for btor bad state props when it is a public name
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-11-14 11:57:38 +01:00
d88cc139a0
Add an info string symbol for bad states in btor backend
2019-11-11 16:40:51 -08:00
a84a2d74c7
Fix btor back-end to use "state" instead of "input" for undef init bits
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-10-02 12:48:04 +02:00
5eebfabe42
Corrects btor2 backend
2019-09-27 12:40:17 -04:00
b88d2e5f30
Fix stupid bug in btor back-end
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-09-18 11:56:14 +02:00
046e1a5214
Use State::S{0,1}
2019-08-06 16:22:47 -07:00
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
1b49380f6b
Improve BTOR2 handling of undriven wires
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-06-26 17:42:00 +02:00
b7dd7c2dcd
Add proper error message for btor recursion_guard
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-05-24 16:22:34 +02:00
148caecca3
Change "ne" to "neq" in btor2 output
...
we need to do this because they changed the parser:
e97fc9ceda
2019-04-19 21:17:12 +02:00
1eff8be8f0
Add support for memory initialization to write_btor
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-03-23 14:40:01 +01:00
e78f5a3055
Fix BTOR output tags syntax in writye_btor
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-03-23 14:39:42 +01:00
23bb77867f
Minor style fixes
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-12-18 20:02:39 +01:00
abf5930a33
Add btor ops for $mul, $div, $mod and $concat
2018-12-17 10:45:17 -08:00
ed3c57fad3
Fix btor init value handling
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-12-08 06:21:31 +01:00
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
9804ebedbf
Add "no driver for signal bit" error msg to btor back-end
2017-12-24 17:30:36 +01:00
292984896b
Simple fix BTOR memory encoding
2017-12-17 18:57:54 +01:00
bbdcc1f9d4
Improve BTOR memory encoding
2017-12-17 18:55:17 +01:00
30f23281ed
Add array support to btor back-end
2017-12-15 02:19:06 +01:00
Jannis Harder
Kevin Läufer
Claire Xenia Wolf
Claire Xenia Wolf
Miodrag Milanovic
Marcelina Kościelnicka
Xiretza
whitequark
N. Engelhardt
Claire Wolf
Eddie Hung
Clifford Wolf
Makai Mann
Aman Goel
Henner Zeller