mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-04-23 00:55:32 +00:00
Code Activity
11815 commits 93 branches 53 tags 45 MiB
Commit graph

111 commits

Author SHA1 Message Date
Jannis Harder
96a1173598 btor: Support $anyinit cells 2022-08-16 13:37:30 +02:00
Jannis Harder
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
Jannis Harder
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
Jannis Harder
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
Kevin Läufer
de5c4bf523 btor: add support for $pos cell 2022-06-20 16:40:46 -07:00
Jannis Harder
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
Claire Xenia Wolf
3fb32540ea Add propagated clock signals into btor info file 2022-05-04 08:10:18 +02:00
Claire Xenia Wolf
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
Miodrag Milanovic
ebe2ee431e handle state names of $anyconst and $anyseq 2022-03-11 14:04:02 +01:00
Marcelina Kościelnicka
93508d58da Add $bmux and $demux cells. 2022-01-28 23:34:41 +01:00
Marcelina Kościelnicka
e7d89e653c Hook up $aldff support in various passes. 2021-10-02 21:01:21 +02:00
Claire Xenia Wolf
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
Marcelina Kościelnicka
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
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
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
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