aboutsummaryrefslogtreecommitdiffstats
path: root/backends/btor/btor.cc
Commit message (Collapse)AuthorAgeFilesLines
* sim/formalff: Clock handling for yw cosimJannis Harder2023-01-111-9/+25
|
* sim: Improvements and fixes for yw cosimJannis Harder2023-01-111-12/+1
| | | | | | * Fixed $cover handling * Improved sparse memory handling when writing traces * JSON summary output
* Support for BTOR witness to Yosys witness conversionJannis Harder2023-01-111-6/+153
|
* Add bwmuxmap passJannis Harder2022-11-301-0/+1
|
* btor: Support $anyinit cellsJannis Harder2022-08-161-1/+1
|
* formalff: Set new replaced_by_gclk attribute on removed dff's clksJannis Harder2022-08-161-0/+10
| | | | | | 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.
* smt2, btor: Revert calling memory_map -rom-onlyJannis Harder2022-06-291-1/+0
| | | | | | | | 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.)
* memory_map: -keepdc option for formalJannis Harder2022-06-271-1/+1
| | | | Use it when invoking memory_map -rom-only from write_{smt2,btor}.
* btor: add support for $pos cellKevin Läufer2022-06-201-8/+11
|
* smt2, btor: Use memory_map -rom-only to make ROMs usable for k-inductionJannis Harder2022-06-171-0/+1
| | | | | | This avoids provability regressions now that we infer more ROMs. This fixes #3378
* Add propagated clock signals into btor info fileClaire Xenia Wolf2022-05-041-0/+2
|
* Fix handling of some formal cells in btor back-endClaire Xenia Wolf2022-03-111-6/+2
| | | | Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
* handle state names of $anyconst and $anyseqMiodrag Milanovic2022-03-111-1/+5
|
* Add $bmux and $demux cells.Marcelina Kościelnicka2022-01-281-0/+5
|
* Hook up $aldff support in various passes.Marcelina Kościelnicka2021-10-021-1/+1
|
* Fixing old e-mail addresses and deadnamesClaire Xenia Wolf2021-06-081-2/+2
| | | | | | | | 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;
* Make a few passes auto-call Mem::narrow instead of rejecting wide ports.Marcelina Kościelnicka2021-05-281-9/+3
| | | | | | 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.
* Reject wide ports in some passes that will never support them.Marcelina Kościelnicka2021-05-251-2/+11
|
* btor: Use is_mem_cell in one more place.Marcelina Kościelnicka2021-05-231-1/+1
|
* kernel/rtlil: Extract some helpers for checking memory cell types.Marcelina Kościelnicka2021-05-221-1/+1
| | | | | | 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.
* btor, smt2, smv: Add a hint on how to deal with funny FF types.Marcelina Kościelnicka2021-02-251-1/+14
|
* btor: Use Mem helper.Marcelina Kościelnicka2020-10-211-93/+102
|
* Respect \A_SIGNED for $shiftXiretza2020-08-181-9/+17
| | | | | | 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).
* Use C++11 final/override keywords.whitequark2020-06-181-2/+2
|
* btor backend: make not printing internal names defaultN. Engelhardt2020-06-041-5/+5
|
* Add printf format attributes to btorf/infof helper functionsClaire Wolf2020-06-041-3/+3
| | | | Signed-off-by: Claire Wolf <claire@symbioticeda.com>
* btor backend: add option to not include internal namesN. Engelhardt2020-06-041-33/+42
|
* Add flooring modulo operatorXiretza2020-05-281-4/+10
| | | | | | | | | | | 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.
* kernel: big fat patch to use more ID::*, otherwise ID(*)Eddie Hung2020-04-021-106/+106
|
* Update backends/btor/btor.cc; credit @boqwxpEddie Hung2020-04-021-2/+1
| | | Co-Authored-By: Alberto Gonzalez <61295559+boqwxp@users.noreply.github.com>
* kernel: use more ID::*Eddie Hung2020-04-021-51/+51
|
* Improve write_btor symbol handlingClaire Wolf2020-03-141-36/+60
| | | | Signed-off-by: Claire Wolf <claire@symbioticeda.com>
* Add info-file and cover features to write_btorClaire Wolf2020-03-131-9/+113
| | | | Signed-off-by: Claire Wolf <claire@symbioticeda.com>
* Use cell name for btor bad state props when it is a public nameClifford Wolf2019-11-141-9/+5
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Add an info string symbol for bad states in btor backendMakai Mann2019-11-111-1/+10
|
* Fix btor back-end to use "state" instead of "input" for undef init bitsClifford Wolf2019-10-021-6/+9
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Corrects btor2 backendAman Goel2019-09-271-1/+4
|
* Fix stupid bug in btor back-endClifford Wolf2019-09-181-1/+1
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Use State::S{0,1}Eddie Hung2019-08-061-2/+2
|
* Add $_NMUX_, add "abc -g cmos", add proper cmos cell costsClifford Wolf2019-08-061-1/+7
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Improve BTOR2 handling of undriven wiresClifford Wolf2019-06-261-3/+27
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Add proper error message for btor recursion_guardClifford Wolf2019-05-241-1/+7
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Change "ne" to "neq" in btor2 outputClifford Wolf2019-04-191-1/+1
| | | | | | | we need to do this because they changed the parser: https://github.com/Boolector/btor2tools/commit/e97fc9cedabadeec4f621de22096e514f862c690 Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Add support for memory initialization to write_btorClifford Wolf2019-03-231-0/+53
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Fix BTOR output tags syntax in writye_btorClifford Wolf2019-03-231-2/+1
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Minor style fixesClifford Wolf2018-12-181-1/+1
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Add btor ops for $mul, $div, $mod and $concatmakaimann2018-12-171-2/+38
|
* Fix btor init value handlingClifford Wolf2018-12-081-9/+13
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Consistent use of 'override' for virtual methods in derived classes.Henner Zeller2018-07-201-2/+2
| | | | | | | | | 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)
* Add "no driver for signal bit" error msg to btor back-endClifford Wolf2017-12-241-0/+2
|
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-08 20:07:58 +0000