Jannis Harder
5142fb3b5c
write_aiger: Fix non-$_FF_ FFs
...
This broke while switching sby's formal flows to always use $_FF_'s.
2022-08-18 13:56:22 +02:00
Jannis Harder
66f761a8c5
smtbmc: Set step range for --yw and dont skip steps for --check-witness
2022-08-16 13:37:30 +02:00
Jannis Harder
b156fe903f
yosys-witness: Add stats command
2022-08-16 13:37:30 +02:00
Jannis Harder
475267ac25
smtbmc: Add --check-witness mode
...
This verifies that the given constraints force an assertion failure.
This is useful to debug witness trace conversion (and minimization).
2022-08-16 13:37:30 +02:00
Jannis Harder
efd5b86eb9
aiger: Add yosys-witness support
...
Adds a new json based aiger map file and yosys-witness converters to us
this to convert between native and AIGER witness files.
2022-08-16 13:37:30 +02:00
Jannis Harder
f041e36c6e
smtbmc: Add native json based witness format + smt2 backend support
...
This adds a native json based witness trace format. By having a common
format that includes everything we support, and providing a conversion
utility (yosys-witness) we no longer need to implement every format for
every tool that deals with witness traces, avoiding a quadratic
opportunity to introduce subtle bugs.
Included:
* smt2: New yosys-smt2-witness info lines containing full hierarchical
paths without lossy escaping.
* yosys-smtbmc --dump-yw trace.yw: Dump results in the new format.
* yosys-smtbmc --yw trace.yw: Read new format as constraints.
* yosys-witness: New tool to convert witness formats.
Currently this can only display traces in a human-readable-only
format and do a passthrough read/write of the new format.
* ywio.py: Small python lib for reading and writing the new format.
Used by yosys-smtbmc and yosys-witness to avoid duplication.
2022-08-16 13:37:30 +02:00
Jannis Harder
96a1173598
btor: Support $anyinit cells
2022-08-16 13:37:30 +02:00
Jannis Harder
5893cae647
aiger: Support $anyinit cells
2022-08-16 13:37:30 +02:00
Jannis Harder
021c3c8da5
smt2: Support $anyinit cells
2022-08-16 13:37:30 +02:00
Jannis Harder
a5e1d3b997
formalff: Set new replaced_by_gclk attribute on removed dff's clks
...
This attribute can be used by formal backends to indicate which clocks
were mapped to the global clock. Update the btor and smt2 backend which
already handle clock inputs to understand this attribute.
2022-08-16 13:37:30 +02:00
Miodrag Milanovic
4444d5cf68
Switched to utf-8 in smtio.py
2022-08-09 12:54:48 +02:00
Miodrag Milanovic
99f1c71582
properly encode string in rtlil
2022-08-09 12:45:32 +02:00
Miodrag Milanović
3705d8414e
Merge pull request #3432 from YosysHQ/aki/jny_updates
...
jny: Added JNY schema and additional information to JNY output file
2022-08-03 13:33:10 +02:00
Jannis Harder
6af5e74f95
smt2: Fix $shift/$shiftx with negative shift ammounts
...
Fixes #3431 , fixes #3344
2022-08-02 20:16:41 +02:00
Aki Van Ness
4f0ee383c9
backend: jny: updated the JnyWriter to emite a new "invocation" entry as well as a "$schema" entry to point to the location the schema will be at
2022-08-02 06:58:41 -04:00
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
