aboutsummaryrefslogtreecommitdiffstats
path: root/backends
Commit message (Expand)AuthorAgeFilesLines
* 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
|\ \
| * | 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
|/
* Use proper operatorMiodrag Milanovic2022-05-271-4/+4
* add $divfloor support to write_smt2Jacob Lifshay2022-05-241-0/+21
* Add propagated clock signals into btor info fileClaire Xenia Wolf2022-05-041-0/+2
* smt2: Make write port array stores conditional on nonzero write maskJannis Harder2022-04-201-2/+4
* pass jny: flipped the defaults for the inclusion of various bits of metadataAki Van Ness2022-04-081-30/+30
* pass jny: ensured the cell collection is cleared between modulesAki Van Ness2022-04-081-0/+1
* pass jny: fixed missing quotes around the type value for the cell sortAki Van Ness2022-04-081-1/+1
* pass jny: fixed the backslash escape for stringsAki Van Ness2022-04-081-2/+1
* pass jny: removed the invalid json escapesAki Van Ness2022-04-081-12/+0
* pass jny: added some todo comments about things that need to be done before a...Aki Van Ness2022-04-081-0/+5
* pass jny: changed the constructor initializers to use parens rather than curl...Aki Van Ness2022-04-081-2/+2
* pass jny: fixed the string escape method to be less jank and more properAki Van Ness2022-04-081-21/+58
* pass jny: fixed the signed output for param value outputAki Van Ness2022-04-081-1/+1
* pass jny: added connection outputAki Van Ness2022-04-081-4/+88
* pass jny: added filter options for including connections, attributes, and pro...Aki Van Ness2022-04-081-25/+125
* pass jny: large chunk of refactoring to make the JSON output more pretty and ...Aki Van Ness2022-04-081-75/+89