aboutsummaryrefslogtreecommitdiffstats
path: root/backends/smt2/smt2.cc
Commit message (Collapse)AuthorAgeFilesLines
* smt2: Fix operation width computation for boolean producing cellsJannis Harder2023-02-011-1/+4
| | | | | | | | | | The output width for the boolean value should not influence the operation width. The previous incorrect width extension would still produce correct results, but could produce invalid smt2 output for reduction operators when the output width was larger than the width of the vector to which the reduction was applied. This fixes #3654
* sim/formalff: Clock handling for yw cosimJannis Harder2023-01-111-1/+1
|
* smt2: Treat bweqx as xnorJannis Harder2023-01-111-0/+1
| | | | Without x-bits they are equivalent
* smt2: Directly implement bwmux instead of using bwmuxmapJannis Harder2023-01-111-2/+4
|
* Add bwmuxmap passJannis Harder2022-11-301-0/+1
|
* smt2/smtbmc: Fix FF witness data for fine grained or multi chunk FFsJannis Harder2022-10-121-3/+10
| | | | | | | The witness metadata was missing fine grained FFs completely and for coarse grained FFs where the output connection has multiple chunks it lacked the offset of the chunk within the SMT expression. This fixes both, the later by adding an "smtoffset" field to the metadata.
* smtbmc: Add native json based witness format + smt2 backend supportJannis Harder2022-08-161-3/+117
| | | | | | | | | | | | | | | | | | | | This adds a native json based witness trace format. By having a common format that includes everything we support, and providing a conversion utility (yosys-witness) we no longer need to implement every format for every tool that deals with witness traces, avoiding a quadratic opportunity to introduce subtle bugs. Included: * smt2: New yosys-smt2-witness info lines containing full hierarchical paths without lossy escaping. * yosys-smtbmc --dump-yw trace.yw: Dump results in the new format. * yosys-smtbmc --yw trace.yw: Read new format as constraints. * yosys-witness: New tool to convert witness formats. Currently this can only display traces in a human-readable-only format and do a passthrough read/write of the new format. * ywio.py: Small python lib for reading and writing the new format. Used by yosys-smtbmc and yosys-witness to avoid duplication.
* smt2: Support $anyinit cellsJannis Harder2022-08-161-10/+11
|
* formalff: Set new replaced_by_gclk attribute on removed dff's clksJannis Harder2022-08-161-0/+11
| | | | | | 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: Fix $shift/$shiftx with negative shift ammountsJannis Harder2022-08-021-4/+4
| | | | Fixes #3431, fixes #3344
* 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}.
* 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
* smt2: emit smtlib2_comb_expr outputs after all inputsJannis Harder2022-06-071-5/+9
|
* smt2: Add smtlib2_comb_expr attribute to allow user-selected smtlib2 expressionsJacob Lifshay2022-06-021-6/+57
|
* add $divfloor support to write_smt2Jacob Lifshay2022-05-241-0/+21
| | | | Fixes: #3330
* smt2: Make write port array stores conditional on nonzero write maskJannis Harder2022-04-201-2/+4
|
* print cell name for properties in yosys-smtbmcN. Engelhardt2022-02-221-2/+4
|
* 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-1/+1
| | | | | | | | 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-6/+1
| | | | | | 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-0/+6
|
* kernel/rtlil: Extract some helpers for checking memory cell types.Marcelina Kościelnicka2021-05-221-2/+2
| | | | | | 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-0/+12
|
* smt2: Use Mem helper.Marcelina Kościelnicka2020-10-211-186/+244
|
* use the new isPublic() in a few placesN. Engelhardt2020-09-141-2/+2
|
* write_smt2: fix SMT-LIB tutorial URLwhitequark2020-08-291-1/+1
|
* Ensure smt2 comments are associated with accessorsNoah Moroze2020-08-201-9/+20
|
* smt2: Add `-solver-option` option.Alberto Gonzalez2020-07-201-0/+13
|
* Use C++11 final/override keywords.whitequark2020-06-181-2/+2
|
* Add flooring modulo operatorXiretza2020-05-281-0/+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-135/+135
|
* kernel: use more ID::*Eddie Hung2020-04-021-37/+37
|
* Update `RTLIL::id2cstr()` usage to `log_id`.Alberto Gonzalez2020-04-011-2/+2
|
* fix typo in `write_smt2` helpTeguh Hofstee2020-03-231-1/+1
|
* Merge pull request #1768 from boqwxp/smt2_cleanupN. Engelhardt2020-03-161-5/+5
|\ | | | | Clean up pseudo-private member usage in `backends/smt2/smt2.cc`.
| * Clean up pseudo-private member usage in `backends/smt2/smt2.cc`.Alberto Gonzalez2020-03-131-5/+5
| |
* | Add support for optimizing exists-forall problems.Alberto Gonzalez2020-03-131-0/+8
|/ | | | | | Modifies smt2 backend to recognize `$anyconst` etc. assigned to a wire with the `maximize` or `minimize` attribute and emit `; yosys-smt2-maximize` or `; yosys-smt2-minimize` directives as appropriate. Modifies `backends/smt2/smtbmc.py` and `smtio.py` to recognize those directives and emit a `(maximize ...)` or `(minimize ...)` command at the end of `smt_forall_assert()`, as described in the paper "νZ - An Optimizing SMT Solver" by Nikolaj Bjørner et al. Adds an example `examples/smtbmc/demo9.v` to show how it can be used.
* substr() -> compare()Eddie Hung2019-08-071-1/+1
|
* Make liberal use of IdString.in()Eddie Hung2019-08-061-1/+1
|
* Add $_NMUX_, add "abc -g cmos", add proper cmos cell costsClifford Wolf2019-08-061-0/+1
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Add "whitebox" attribute, add "read_verilog -wb"Clifford Wolf2019-04-181-1/+1
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Fix signed $shift/$shiftx handling in write_smt2Clifford Wolf2019-03-091-1/+2
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Use SVA label in smt export if availableClifford Wolf2019-03-071-2/+2
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Fix smt2 code generation for partially initialized memowy words, fixes #831Clifford Wolf2019-02-281-4/+11
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Add support for signed $shift/$shiftx in smt2 back-endClifford Wolf2018-11-011-1/+3
| | | | 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)
* Fixed -stbv handling in SMT2 back-endClifford Wolf2018-04-041-1/+1
|
* Add $mem support to SMT2 clock taggingClifford Wolf2018-03-271-0/+18
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
generated by cgit v1.2.3 (git 2.25.1) at 2024-09-12 11:56:01 +0000