Michael Nolan
24b895778a
Add support for GHDL modfloor operator
2022-07-05 15:15:54 -04:00
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
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
