| Commit message (Expand) | Author | Age | Files | Lines |
* | 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 |
| |/ |
|
* / | smtbmc: Force nonincremental mode when yices is used with forall | Jannis Harder | 2022-06-03 | 1 | -1/+4 |
|/ |
|
* | Use proper operator | Miodrag Milanovic | 2022-05-27 | 1 | -4/+4 |
* | add $divfloor support to write_smt2 | Jacob Lifshay | 2022-05-24 | 1 | -0/+21 |
* | Add propagated clock signals into btor info file | Claire Xenia Wolf | 2022-05-04 | 1 | -0/+2 |
* | smt2: Make write port array stores conditional on nonzero write mask | Jannis Harder | 2022-04-20 | 1 | -2/+4 |
* | pass jny: flipped the defaults for the inclusion of various bits of metadata | Aki Van Ness | 2022-04-08 | 1 | -30/+30 |
* | pass jny: ensured the cell collection is cleared between modules | Aki Van Ness | 2022-04-08 | 1 | -0/+1 |
* | pass jny: fixed missing quotes around the type value for the cell sort | Aki Van Ness | 2022-04-08 | 1 | -1/+1 |
* | pass jny: fixed the backslash escape for strings | Aki Van Ness | 2022-04-08 | 1 | -2/+1 |
* | pass jny: removed the invalid json escapes | Aki Van Ness | 2022-04-08 | 1 | -12/+0 |
* | pass jny: added some todo comments about things that need to be done before a... | Aki Van Ness | 2022-04-08 | 1 | -0/+5 |
* | pass jny: changed the constructor initializers to use parens rather than curl... | Aki Van Ness | 2022-04-08 | 1 | -2/+2 |
* | pass jny: fixed the string escape method to be less jank and more proper | Aki Van Ness | 2022-04-08 | 1 | -21/+58 |
* | pass jny: fixed the signed output for param value output | Aki Van Ness | 2022-04-08 | 1 | -1/+1 |
* | pass jny: added connection output | Aki Van Ness | 2022-04-08 | 1 | -4/+88 |
* | pass jny: added filter options for including connections, attributes, and pro... | Aki Van Ness | 2022-04-08 | 1 | -25/+125 |
* | pass jny: large chunk of refactoring to make the JSON output more pretty and ... | Aki Van Ness | 2022-04-08 | 1 | -75/+89 |
* | metadata -> jny: migrated to the proper name for the pass | Aki Van Ness | 2022-04-08 | 3 | -21/+19 |
* | pass metadata: added the machinery to write param and attributes | Aki Van Ness | 2022-04-08 | 1 | -8/+27 |
* | pass metadata: removed superfluous `stringf` calls | Aki Van Ness | 2022-04-08 | 1 | -37/+40 |
* | pass metadata: some more rough work on dumping the parameters and attributes | Aki Van Ness | 2022-04-08 | 1 | -6/+6 |
* | pass metadata: fixed the MetadataWriter object initializer so GCC 4.8 is happy | Aki Van Ness | 2022-04-08 | 1 | -1/+1 |
* | pass metadata: added the output of parameters, | Aki Van Ness | 2022-04-08 | 1 | -7/+35 |
* | pass metadata: fixed some of the output formatting | Aki Van Ness | 2022-04-08 | 1 | -0/+3 |