aboutsummaryrefslogtreecommitdiffstats
path: root/backends/smt2
Commit message (Expand)AuthorAgeFilesLines
* Add bwmuxmap passJannis Harder2022-11-301-0/+1
* 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
* smtbmc: Avoid unnecessary string copies when parsing solver outputJannis Harder2022-09-021-12/+9
* 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-161-2/+148
* smtbmc: Add native json based witness format + smt2 backend supportJannis Harder2022-08-166-113/+968
* 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
* Switched to utf-8 in smtio.pyMiodrag Milanovic2022-08-091-2/+2
* smt2: Fix $shift/$shiftx with negative shift ammountsJannis Harder2022-08-021-4/+4
* smt2, btor: Revert calling memory_map -rom-onlyJannis Harder2022-06-291-1/+0
* memory_map: -keepdc option for formalJannis Harder2022-06-271-1/+1
* smt2, btor: Use memory_map -rom-only to make ROMs usable for k-inductionJannis Harder2022-06-171-0/+1
* 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
|\ \
| * | smt2: Add smtlib2_comb_expr attribute to allow user-selected smtlib2 expressionsJacob Lifshay2022-06-021-6/+57
| |/
* / smtbmc: Force nonincremental mode when yices is used with forallJannis Harder2022-06-031-1/+4
|/
* add $divfloor support to write_smt2Jacob Lifshay2022-05-241-0/+21
* smt2: Make write port array stores conditional on nonzero write maskJannis Harder2022-04-201-2/+4
* smtbmc: fix bmc with no assertionsJannis Harder2022-03-291-0/+2
* Merge pull request #3253 from jix/smtbmc-nodeepcopyJannis Harder2022-03-281-6/+6
|\
| * smtbmc: Avoid unnecessary deep copies during unrollingJannis Harder2022-03-281-6/+6
* | Merge pull request #3247 from jix/smtbmc-keepgoingJannis Harder2022-03-281-50/+143
|\ \ | |/ |/|
| * yosys-smtbmc: Option to keep going after failed assertions in BMC modeJannis Harder2022-03-241-48/+141
| * yosys-smtbmc: Fix typo in help text, remove trailing whitespaceJannis Harder2022-03-241-2/+2
* | ignore # comment linesN. Engelhardt2022-03-241-1/+1
|/
* Merge pull request #3186 from nakengelhardt/smtbmc_sby_print_idMiodrag Milanović2022-03-042-4/+12
|\
| * print cell name for properties in yosys-smtbmcN. Engelhardt2022-02-222-4/+12
* | Add a bit of flexibilty re trace length when processing aiger witnesses in sm...Claire Xenia Wolf2022-02-111-1/+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
* yosys-smtbmc: Fix reused loop variable.Marcelina Kościelnicka2021-09-101-4/+4
* Add support for the Bitwuzla solverGCHQDeveloper5602021-07-121-5/+5
* Fixing old e-mail addresses and deadnamesClaire Xenia Wolf2021-06-083-3/+3
* Make a few passes auto-call Mem::narrow instead of rejecting wide ports.Marcelina Kościelnicka2021-05-281-6/+1
* 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
* 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
* smtbmc: escape identifiers in verilog testbenchJakob Wenzel2020-10-061-11/+29
* use the new isPublic() in a few placesN. Engelhardt2020-09-141-2/+2
* write_smt2: fix SMT-LIB tutorial URLwhitequark2020-08-291-1/+1
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-15 09:59:16 +0000