aboutsummaryrefslogtreecommitdiffstats
path: root/backends
Commit message (Expand)AuthorAgeFilesLines
* yosys-smtbmc: support -h/--help (and exit with code 0).Catherine2023-02-271-4/+13
* verilog_backend: Do not run bwmuxmap even if in expr modeJannis Harder2023-02-131-1/+0
* backends/firrtl: Ensure `modInstance` is validAki Van Ness2023-02-031-0/+6
* Merge pull request #3655 from jix/smt2_fix_b_op_widthJannis Harder2023-02-011-1/+4
|\
| * smt2: Fix operation width computation for boolean producing cellsJannis Harder2023-02-011-1/+4
* | backends/rtlil: Do not shorten a value with z bits to 'xJannis Harder2023-01-291-1/+1
|/
* Merge pull request #3624 from jix/sim_ywMiodrag Milanović2023-01-235-72/+373
|\
| * sim/formalff: Clock handling for yw cosimJannis Harder2023-01-112-10/+26
| * sim: Improvements and fixes for yw cosimJannis Harder2023-01-113-47/+50
| * Support for BTOR witness to Yosys witness conversionJannis Harder2023-01-113-8/+287
| * aiger: Use new JSON code for writing aiger witness map filesJannis Harder2023-01-111-49/+49
| * smt2: Treat bweqx as xnorJannis Harder2023-01-111-0/+1
| * smt2: Directly implement bwmux instead of using bwmuxmapJannis Harder2023-01-111-2/+4
* | Fixes for some of clang scan-build detected issuesMiodrag Milanovic2023-01-174-6/+12
|/
* Add bwmuxmap passJannis Harder2022-11-305-0/+5
* verilog_backend: Do not run bmuxmap or demuxmap in -noexpr mode.Jannis Harder2022-11-301-2/+4
* verilog_backend: Correctly sign extend output of signed `$modfloor`Jannis Harder2022-11-301-2/+2
* verilog_backend: Add -noparallelcase optionJannis Harder2022-11-301-7/+31
* smtbmc: Do not assume skipped assertions when loading a witness traceJannis Harder2022-10-201-3/+0
* Temporal induction counterexample loop detection (#3504)Emil J2022-10-191-1/+36
* smtbmc: Fix witness handling for k-induction failuresJannis Harder2022-10-181-1/+1
* smt2/smtbmc: Fix FF witness data for fine grained or multi chunk FFsJannis Harder2022-10-123-5/+22
* backends: protobuf: removed protobuf backendAki Van Ness2022-10-103-383/+0
* smtbmc: Avoid unnecessary string copies when parsing solver outputJannis Harder2022-09-021-12/+9
* Fitting help messages to 80 character widthKrystalDelusion2022-08-244-9/+10
* write_aiger: Fix non-$_FF_ FFsJannis Harder2022-08-181-1/+1
* smtbmc: Set step range for --yw and dont skip steps for --check-witnessJannis Harder2022-08-161-2/+14
* yosys-witness: Add stats commandJannis Harder2022-08-161-0/+18
* smtbmc: Add --check-witness modeJannis Harder2022-08-161-1/+22
* aiger: Add yosys-witness supportJannis Harder2022-08-162-2/+317
* smtbmc: Add native json based witness format + smt2 backend supportJannis Harder2022-08-166-113/+968
* btor: Support $anyinit cellsJannis Harder2022-08-161-1/+1
* aiger: Support $anyinit cellsJannis Harder2022-08-161-0/+11
* smt2: Support $anyinit cellsJannis Harder2022-08-161-10/+11
* formalff: Set new replaced_by_gclk attribute on removed dff's clksJannis Harder2022-08-162-0/+21
* Switched to utf-8 in smtio.pyMiodrag Milanovic2022-08-091-2/+2
* properly encode string in rtlilMiodrag Milanovic2022-08-091-1/+1
* Merge pull request #3432 from YosysHQ/aki/jny_updatesMiodrag Milanović2022-08-031-10/+33
|\
| * backend: jny: updated the `JnyWriter` to emite a new "invocation" entry as we...Aki Van Ness2022-08-021-10/+33
* | smt2: Fix $shift/$shiftx with negative shift ammountsJannis Harder2022-08-021-4/+4
|/
* Add support for GHDL modfloor operatorMichael Nolan2022-07-052-1/+22
* smt2, btor: Revert calling memory_map -rom-onlyJannis Harder2022-06-292-2/+0
* memory_map: -keepdc option for formalJannis Harder2022-06-272-2/+2
* 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-172-0/+2
* smtbmc: noincr: keep solver running for post check-sat unrollingJannis Harder2022-06-081-2/+7
* Merge pull request #3357 from jix/smtbmc-cvc5Jannis Harder2022-06-081-3/+13
|\
| * smtbmc: recognize cvc5 and fix unrolling for cvc4/cvc5Jannis Harder2022-06-031-3/+13
* | smt2: emit smtlib2_comb_expr outputs after all inputsJannis Harder2022-06-071-5/+9
* | Merge pull request #3319 from programmerjake/smtlib2-expr-supportJannis Harder2022-06-071-6/+57
|\ \