aboutsummaryrefslogtreecommitdiffstats
path: root/backends
Commit message (Collapse)AuthorAgeFilesLines
* Merge pull request #3432 from YosysHQ/aki/jny_updatesMiodrag Milanović2022-08-031-10/+33
|\ | | | | jny: Added JNY schema and additional information to JNY output file
| * backend: jny: updated the `JnyWriter` to emite a new "invocation" entry as ↵Aki Van Ness2022-08-021-10/+33
| | | | | | | | well as a "$schema" entry to point to the location the schema will be at
* | smt2: Fix $shift/$shiftx with negative shift ammountsJannis Harder2022-08-021-4/+4
|/ | | | Fixes #3431, fixes #3344
* Add support for GHDL modfloor operatorMichael Nolan2022-07-052-1/+22
|
* smt2, btor: Revert calling memory_map -rom-onlyJannis Harder2022-06-292-2/+0
| | | | | | | | This approach had major issues with ROMs whose initialization was not fully defined. If required, memory_map -rom-only -keepdc should be called early in a formal flow instead. (This does require a careful choice of optimization passes though. Sby's scripts will be updated accordingly.)
* memory_map: -keepdc option for formalJannis Harder2022-06-272-2/+2
| | | | Use it when invoking memory_map -rom-only from write_{smt2,btor}.
* 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
| | | | | | This avoids provability regressions now that we infer more ROMs. This fixes #3378
* 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/cvc5
| * 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
|\ \ | | | | | | add smtlib2_comb_expr
| * | 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
| | | | Fixes: #3330
* 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 ↵Aki Van Ness2022-04-081-0/+5
| | | | a proper merge, but it should be enough for the PoC at the moment
* pass jny: changed the constructor initializers to use parens rather than ↵Aki Van Ness2022-04-081-2/+2
| | | | curly-braces to hopefully make GCC 4.8 happy
* 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 ↵Aki Van Ness2022-04-081-25/+125
| | | | properties
* pass jny: large chunk of refactoring to make the JSON output more pretty and ↵Aki Van Ness2022-04-081-75/+89
| | | | the internals less of a spaghetti nightmare
* metadata -> jny: migrated to the proper name for the passAki Van Ness2022-04-083-21/+19
|
* pass metadata: added the machinery to write param and attributesAki Van Ness2022-04-081-8/+27
|
* pass metadata: removed superfluous `stringf` callsAki Van Ness2022-04-081-37/+40
|
* pass metadata: some more rough work on dumping the parameters and attributesAki Van Ness2022-04-081-6/+6
|
* pass metadata: fixed the MetadataWriter object initializer so GCC 4.8 is happyAki Van Ness2022-04-081-1/+1
|
* pass metadata: added the output of parameters,Aki Van Ness2022-04-081-7/+35
| | | | it's kinda dumb at the moment and needs parsing based on type but it's a start
* pass metadata: fixed some of the output formattingAki Van Ness2022-04-081-0/+3
|
* pass metadata: initial commit of the metadata pass for exporting design ↵Aki Van Ness2022-04-082-0/+277
| | | | metadata for yosys assisted tooling
* smtbmc: fix bmc with no assertionsJannis Harder2022-03-291-0/+2
| | | | this was broken by the `--keep-going` changes
* Merge pull request #3253 from jix/smtbmc-nodeepcopyJannis Harder2022-03-281-6/+6
|\ | | | | smtbmc: Avoid unnecessary deep copies during unrolling
| * 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
|\ \ | |/ |/| smtbmc `--keep-going`
| * 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
| |
* | Add -no-startoffset option to write_aigerMiodrag Milanovic2022-03-251-8/+17
| |
* | ignore # comment linesN. Engelhardt2022-03-241-1/+1
|/
* Merge pull request #3226 from YosysHQ/micko/btor2witnessMiodrag Milanović2022-03-111-2/+2
|\ | | | | Sim support for btor2 witness files
| * Fix handling of some formal cells in btor back-endClaire Xenia Wolf2022-03-111-6/+2
| | | | | | | | Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
| * handle state names of $anyconst and $anyseqMiodrag Milanovic2022-03-111-1/+5
| |
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-08 14:26:44 +0000