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 |
|
|
|
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 |
|
|
|
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 |
|
R
|
2d3a337795
|
json: Add help message for signed field
|
2022-02-21 21:59:25 -08:00 |
|
N. Engelhardt
|
8fd1b06249
|
fix handling of escaped chars in json backend and frontend
|
2022-02-18 17:13:09 +01:00 |
|
