| Commit message (Expand) | Author | Age | Files | Lines |
* | verilog_backend: Do not run bwmuxmap even if in expr mode | Jannis Harder | 2023-02-13 | 1 | -1/+0 |
* | backends/firrtl: Ensure `modInstance` is valid | Aki Van Ness | 2023-02-03 | 1 | -0/+6 |
* | Merge pull request #3655 from jix/smt2_fix_b_op_width | Jannis Harder | 2023-02-01 | 1 | -1/+4 |
|\ |
|
| * | smt2: Fix operation width computation for boolean producing cells | Jannis Harder | 2023-02-01 | 1 | -1/+4 |
* | | backends/rtlil: Do not shorten a value with z bits to 'x | Jannis Harder | 2023-01-29 | 1 | -1/+1 |
|/ |
|
* | Merge pull request #3624 from jix/sim_yw | Miodrag Milanović | 2023-01-23 | 5 | -72/+373 |
|\ |
|
| * | sim/formalff: Clock handling for yw cosim | Jannis Harder | 2023-01-11 | 2 | -10/+26 |
| * | sim: Improvements and fixes for yw cosim | Jannis Harder | 2023-01-11 | 3 | -47/+50 |
| * | Support for BTOR witness to Yosys witness conversion | Jannis Harder | 2023-01-11 | 3 | -8/+287 |
| * | aiger: Use new JSON code for writing aiger witness map files | Jannis Harder | 2023-01-11 | 1 | -49/+49 |
| * | smt2: Treat bweqx as xnor | Jannis Harder | 2023-01-11 | 1 | -0/+1 |
| * | smt2: Directly implement bwmux instead of using bwmuxmap | Jannis Harder | 2023-01-11 | 1 | -2/+4 |
* | | Fixes for some of clang scan-build detected issues | Miodrag Milanovic | 2023-01-17 | 4 | -6/+12 |
|/ |
|
* | Add bwmuxmap pass | Jannis Harder | 2022-11-30 | 5 | -0/+5 |
* | verilog_backend: Do not run bmuxmap or demuxmap in -noexpr mode. | Jannis Harder | 2022-11-30 | 1 | -2/+4 |
* | verilog_backend: Correctly sign extend output of signed `$modfloor` | Jannis Harder | 2022-11-30 | 1 | -2/+2 |
* | verilog_backend: Add -noparallelcase option | Jannis Harder | 2022-11-30 | 1 | -7/+31 |
* | smtbmc: Do not assume skipped assertions when loading a witness trace | Jannis Harder | 2022-10-20 | 1 | -3/+0 |
* | Temporal induction counterexample loop detection (#3504) | Emil J | 2022-10-19 | 1 | -1/+36 |
* | smtbmc: Fix witness handling for k-induction failures | Jannis Harder | 2022-10-18 | 1 | -1/+1 |
* | smt2/smtbmc: Fix FF witness data for fine grained or multi chunk FFs | Jannis Harder | 2022-10-12 | 3 | -5/+22 |
* | backends: protobuf: removed protobuf backend | Aki Van Ness | 2022-10-10 | 3 | -383/+0 |
* | smtbmc: Avoid unnecessary string copies when parsing solver output | Jannis Harder | 2022-09-02 | 1 | -12/+9 |
* | Fitting help messages to 80 character width | KrystalDelusion | 2022-08-24 | 4 | -9/+10 |
* | write_aiger: Fix non-$_FF_ FFs | Jannis Harder | 2022-08-18 | 1 | -1/+1 |
* | smtbmc: Set step range for --yw and dont skip steps for --check-witness | Jannis Harder | 2022-08-16 | 1 | -2/+14 |
* | yosys-witness: Add stats command | Jannis Harder | 2022-08-16 | 1 | -0/+18 |
* | smtbmc: Add --check-witness mode | Jannis Harder | 2022-08-16 | 1 | -1/+22 |
* | aiger: Add yosys-witness support | Jannis Harder | 2022-08-16 | 2 | -2/+317 |
* | smtbmc: Add native json based witness format + smt2 backend support | Jannis Harder | 2022-08-16 | 6 | -113/+968 |
* | btor: Support $anyinit cells | Jannis Harder | 2022-08-16 | 1 | -1/+1 |
* | aiger: Support $anyinit cells | Jannis Harder | 2022-08-16 | 1 | -0/+11 |
* | smt2: Support $anyinit cells | Jannis Harder | 2022-08-16 | 1 | -10/+11 |
* | formalff: Set new replaced_by_gclk attribute on removed dff's clks | Jannis Harder | 2022-08-16 | 2 | -0/+21 |
* | Switched to utf-8 in smtio.py | Miodrag Milanovic | 2022-08-09 | 1 | -2/+2 |
* | properly encode string in rtlil | Miodrag Milanovic | 2022-08-09 | 1 | -1/+1 |
* | Merge pull request #3432 from YosysHQ/aki/jny_updates | Miodrag Milanović | 2022-08-03 | 1 | -10/+33 |
|\ |
|
| * | backend: jny: updated the `JnyWriter` to emite a new "invocation" entry as we... | Aki Van Ness | 2022-08-02 | 1 | -10/+33 |
* | | smt2: Fix $shift/$shiftx with negative shift ammounts | Jannis Harder | 2022-08-02 | 1 | -4/+4 |
|/ |
|
* | Add support for GHDL modfloor operator | Michael Nolan | 2022-07-05 | 2 | -1/+22 |
* | smt2, btor: Revert calling memory_map -rom-only | Jannis Harder | 2022-06-29 | 2 | -2/+0 |
* | memory_map: -keepdc option for formal | Jannis Harder | 2022-06-27 | 2 | -2/+2 |
* | btor: add support for $pos cell | Kevin Läufer | 2022-06-20 | 1 | -8/+11 |
* | smt2, btor: Use memory_map -rom-only to make ROMs usable for k-induction | Jannis Harder | 2022-06-17 | 2 | -0/+2 |
* | smtbmc: noincr: keep solver running for post check-sat unrolling | Jannis Harder | 2022-06-08 | 1 | -2/+7 |
* | Merge pull request #3357 from jix/smtbmc-cvc5 | Jannis Harder | 2022-06-08 | 1 | -3/+13 |
|\ |
|
| * | smtbmc: recognize cvc5 and fix unrolling for cvc4/cvc5 | Jannis Harder | 2022-06-03 | 1 | -3/+13 |
* | | smt2: emit smtlib2_comb_expr outputs after all inputs | Jannis Harder | 2022-06-07 | 1 | -5/+9 |
* | | Merge pull request #3319 from programmerjake/smtlib2-expr-support | Jannis Harder | 2022-06-07 | 1 | -6/+57 |
|\ \ |
|
| * | | smt2: Add smtlib2_comb_expr attribute to allow user-selected smtlib2 expressions | Jacob Lifshay | 2022-06-02 | 1 | -6/+57 |
| |/ |
|