Marcelina Kościelnicka
69bf5c81c7
Reject wide ports in some passes that will never support them.
2021-05-25 02:07:25 +02:00
Marcelina Kościelnicka
33513d923a
btor: Use is_mem_cell in one more place.
2021-05-23 20:34:52 +02:00
Marcelina Kościelnicka
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
Marcelina Kościelnicka
979347999f
btor, smt2, smv: Add a hint on how to deal with funny FF types.
2021-02-25 22:04:04 +01:00
Marcelina Kościelnicka
2d340cd355
btor: Use Mem helper.
2020-10-21 17:51:20 +02:00
Xiretza
6224fd9055
Add missing gitignores for test artifacts
2020-08-31 19:43:51 +02:00
Xiretza
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
whitequark
7191dd16f9
Use C++11 final/override keywords.
2020-06-18 23:34:52 +00:00
N. Engelhardt
82798ae575
btor backend: make not printing internal names default
2020-06-04 16:24:16 +02:00
Claire Wolf
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
N. Engelhardt
8ceb6686e0
btor backend: add option to not include internal names
2020-06-04 14:00:52 +02:00
Xiretza
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
Xiretza
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
Eddie Hung
956ecd48f7
kernel: big fat patch to use more ID::*, otherwise ID(*)
2020-04-02 09:51:32 -07:00
Eddie Hung
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
Eddie Hung
fdafb74eb7
kernel: use more ID::*
2020-04-02 07:14:08 -07:00
Claire Wolf
bf018b184d
Improve write_btor symbol handling
...
Signed-off-by: Claire Wolf <claire@symbioticeda.com>
2020-03-14 15:49:43 +01:00
Claire Wolf
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
Clifford Wolf
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
Makai Mann
d88cc139a0
Add an info string symbol for bad states in btor backend
2019-11-11 16:40:51 -08:00
Clifford Wolf
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
Aman Goel
5eebfabe42
Corrects btor2 backend
2019-09-27 12:40:17 -04:00
Clifford Wolf
b88d2e5f30
Fix stupid bug in btor back-end
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-09-18 11:56:14 +02:00
Eddie Hung
046e1a5214
Use State::S{0,1}
2019-08-06 16:22:47 -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
1b49380f6b
Improve BTOR2 handling of undriven wires
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-06-26 17:42:00 +02:00
Clifford Wolf
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
Clifford Wolf
148caecca3
Change "ne" to "neq" in btor2 output
...
we need to do this because they changed the parser:
e97fc9ceda
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-04-19 21:17:12 +02:00
Clifford Wolf
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
Clifford Wolf
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
Clifford Wolf
23bb77867f
Minor style fixes
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-12-18 20:02:39 +01:00
makaimann
abf5930a33
Add btor ops for $mul, $div, $mod and $concat
2018-12-17 10:45:17 -08:00
Clifford Wolf
ed3c57fad3
Fix btor init value handling
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-12-08 06:21:31 +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
9804ebedbf
Add "no driver for signal bit" error msg to btor back-end
2017-12-24 17:30:36 +01:00
Clifford Wolf
292984896b
Simple fix BTOR memory encoding
2017-12-17 18:57:54 +01:00
Clifford Wolf
bbdcc1f9d4
Improve BTOR memory encoding
2017-12-17 18:55:17 +01:00
Clifford Wolf
30f23281ed
Add array support to btor back-end
2017-12-15 02:19:06 +01:00
Clifford Wolf
ad901671c5
Add $anyconst/$anyseq support to btor back-end
2017-12-15 00:40:24 +01:00
Clifford Wolf
546de7fa4f
Add "write_btor -s" mode
2017-12-13 00:15:44 +01:00
Clifford Wolf
0881bbf2e7
Add state initval handling to btor back-end
2017-12-12 23:44:08 +01:00
Clifford Wolf
f697282246
Add btor back-end support for 'x' constants
2017-12-12 21:48:55 +01:00
Clifford Wolf
82d1fd77de
Add btor $shift/$shiftx support
2017-12-11 14:24:19 +01:00
Clifford Wolf
cc119b5232
Fix btor back-end shift handling
2017-12-10 08:40:11 +01:00
Clifford Wolf
133a0f4978
Add support for $pmux in btor back-end
2017-12-10 08:11:08 +01:00
Clifford Wolf
83cf736309
Add support for more cell types to btor back-end
2017-12-10 07:16:47 +01:00
Clifford Wolf
63343aeaaa
Fix btor concat
2017-12-09 05:58:14 +01:00
Clifford Wolf
e3a51b3e87
Bugfixes in new BTOR back-end
2017-11-24 18:13:41 +01:00
Clifford Wolf
60d1129506
Progress in new BTOR back-end
2017-11-23 23:44:39 +01:00
Clifford Wolf
b3d6b277ea
Progress in new BTOR back-end
2017-11-23 18:50:10 +01:00