riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity
11,649 Commits 81 Branches 48 Tags 64 MiB
Commit Graph

1310 Commits

Author SHA1 Message Date
Jannis Harder 930bcf0e75 smt2, btor: Revert calling memory_map -rom-only 
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.)
 2022-06-29 18:28:34 +02:00
Jannis Harder d78d807a7f memory_map: -keepdc option for formal 
Use it when invoking memory_map -rom-only from write_{smt2,btor}.
 2022-06-27 15:47:55 +02:00
Kevin Läufer de5c4bf523 btor: add support for $pos cell 2022-06-20 16:40:46 -07:00
Jannis Harder 4adef63cd4 smt2, btor: Use memory_map -rom-only to make ROMs usable for k-induction 
This avoids provability regressions now that we infer more ROMs.

This fixes #3378
 2022-06-17 17:23:13 +02:00
Jannis Harder 0c5f62f6ff smtbmc: noincr: keep solver running for post check-sat unrolling 2022-06-08 13:20:25 +02:00
Jannis Harder 6db2948938
Merge pull request #3357 from jix/smtbmc-cvc5 
smtbmc: recognize cvc5 and fix unrolling for cvc4/cvc5
 2022-06-08 12:52:51 +02:00
Jannis Harder ac22f1764d smt2: emit smtlib2_comb_expr outputs after all inputs 2022-06-07 19:06:45 +02:00
Jannis Harder 5f9a97d234
Merge pull request #3319 from programmerjake/smtlib2-expr-support 
add smtlib2_comb_expr
 2022-06-07 16:47:10 +02:00
Jannis Harder ab9e887dee smtbmc: Force nonincremental mode when yices is used with forall 2022-06-03 16:45:23 +02:00
Jannis Harder 0207d7b0cf smtbmc: recognize cvc5 and fix unrolling for cvc4/cvc5 2022-06-03 16:24:09 +02:00
Jacob Lifshay cd57c5adb3 smt2: Add smtlib2_comb_expr attribute to allow user-selected smtlib2 expressions 2022-06-02 22:37:29 -07:00
Miodrag Milanovic 7ee570a75e Use proper operator 2022-05-27 10:23:34 +02:00
Jacob Lifshay d53479a0d6 add $divfloor support to write_smt2 
Fixes: #3330
 2022-05-24 01:34:25 -07:00
Claire Xenia Wolf 3fb32540ea Add propagated clock signals into btor info file 2022-05-04 08:10:18 +02:00
Jannis Harder c7ef0f2932 smt2: Make write port array stores conditional on nonzero write mask 2022-04-20 17:49:48 +02:00
Aki Van Ness 1f1a403cce pass jny: flipped the defaults for the inclusion of various bits of metadata 2022-04-08 08:05:15 +02:00
Aki Van Ness 6053856f91 pass jny: ensured the cell collection is cleared between modules 2022-04-08 08:05:15 +02:00
Aki Van Ness 5a016713cc pass jny: fixed missing quotes around the type value for the cell sort 2022-04-08 08:05:15 +02:00
Aki Van Ness 2e792857e9 pass jny: fixed the backslash escape for strings 2022-04-08 08:05:15 +02:00
Aki Van Ness cae5ea8337 pass jny: removed the invalid json escapes 2022-04-08 08:05:15 +02:00
Aki Van Ness dccc89e8b3 pass jny: added some todo comments about things that need to be done before a proper merge, but it should be enough for the PoC at the moment 2022-04-08 08:05:15 +02:00
Aki Van Ness 1be9bef28b pass jny: changed the constructor initializers to use parens rather than curly-braces to hopefully make GCC 4.8 happy 2022-04-08 08:05:15 +02:00
Aki Van Ness 43b2fc5566 pass jny: fixed the string escape method to be less jank and more proper 2022-04-08 08:05:15 +02:00
Aki Van Ness 52ea944012 pass jny: fixed the signed output for param value output 2022-04-08 08:05:15 +02:00
Aki Van Ness 58e2870261 pass jny: added connection output 2022-04-08 08:05:15 +02:00
Aki Van Ness 167206f2f5 pass jny: added filter options for including connections, attributes, and properties 2022-04-08 08:05:15 +02:00
Aki Van Ness 587f31b9a3 pass jny: large chunk of refactoring to make the JSON output more pretty and the internals less of a spaghetti nightmare 2022-04-08 08:05:15 +02:00
Aki Van Ness 0e20619189 metadata -> jny: migrated to the proper name for the pass 2022-04-08 08:05:15 +02:00
Aki Van Ness bdf14557ca pass metadata: added the machinery to write param and attributes 2022-04-08 08:05:15 +02:00
Aki Van Ness 1876ed21e7 pass metadata: removed superfluous `stringf` calls 2022-04-08 08:05:15 +02:00
Aki Van Ness ca03fbdc6d pass metadata: some more rough work on dumping the parameters and attributes 2022-04-08 08:05:15 +02:00
Aki Van Ness 6a90b42c48 pass metadata: fixed the MetadataWriter object initializer so GCC 4.8 is happy 2022-04-08 08:05:15 +02:00
Aki Van Ness 7a275567df pass metadata: added the output of parameters, 
it's kinda dumb at the moment and needs parsing based on type but it's a start
 2022-04-08 08:05:15 +02:00
Aki Van Ness d8b85e1247 pass metadata: fixed some of the output formatting 2022-04-08 08:05:15 +02:00
Aki Van Ness f6bb238051 pass metadata: initial commit of the metadata pass for exporting design metadata for yosys assisted tooling 2022-04-08 08:05:15 +02:00
Jannis Harder 8b15f3a548 smtbmc: fix bmc with no assertions 
this was broken by the `--keep-going` changes
 2022-03-29 20:41:50 +02:00
Jannis Harder 8cc8c5efde
Merge pull request #3253 from jix/smtbmc-nodeepcopy 
smtbmc: Avoid unnecessary deep copies during unrolling
 2022-03-28 16:59:26 +02:00
Jannis Harder 17e2a3048c
Merge pull request #3247 from jix/smtbmc-keepgoing 
smtbmc `--keep-going`
 2022-03-28 16:58:41 +02:00
Jannis Harder d25daa6203 smtbmc: Avoid unnecessary deep copies during unrolling 2022-03-28 13:03:48 +02:00
Miodrag Milanovic 4fd8b38d7a Add -no-startoffset option to write_aiger 2022-03-25 08:44:45 +01:00
Jannis Harder 5e4d804e53 yosys-smtbmc: Option to keep going after failed assertions in BMC mode 2022-03-24 16:01:14 +01:00
Jannis Harder e43ebf8527 yosys-smtbmc: Fix typo in help text, remove trailing whitespace 2022-03-24 16:01:14 +01:00
N. Engelhardt a7ee01065a ignore # comment lines 2022-03-24 10:19:17 +01:00
Miodrag Milanović 2f44683f4f
Merge pull request #3226 from YosysHQ/micko/btor2witness 
Sim support for btor2 witness files
 2022-03-11 15:29:34 +01:00
Claire Xenia Wolf d340f302f6 Fix handling of some formal cells in btor back-end 
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
 2022-03-11 14:21:12 +01:00
Miodrag Milanovic ebe2ee431e handle state names of $anyconst and $anyseq 2022-03-11 14:04:02 +01:00
Miodrag Milanović 4ccc2adbda
Merge pull request #3210 from rqou/json-signed 
json: Add help message for `signed` field
 2022-03-07 09:41:25 +01:00
Miodrag Milanović a95e5d505b
Merge pull request #3186 from nakengelhardt/smtbmc_sby_print_id 
add argument for printing cell names in yosys-smtbmc
 2022-03-04 16:39:12 +01:00
Miodrag Milanović c3124023e4
Merge pull request #3207 from nakengelhardt/json_escape_quotes 
fix handling of escaped chars in json backend and frontend (mostly)
 2022-03-04 13:57:32 +01:00
N. Engelhardt dc739362c7 print cell name for properties in yosys-smtbmc 2022-02-22 17:00:10 +01:00