Aki Van Ness
98fdcd7772
sby: core: fixed up the [setup] section
2022-08-18 05:36:11 -04:00
Aki Van Ness
6c959577f3
sby: core: cleaned up the [stage] section parsing
2022-08-18 05:36:11 -04:00
Aki Van Ness
ad4f506d2a
sby: core: fixed up the engines section parser
2022-08-18 05:36:10 -04:00
Aki Van Ness
2f841e5d55
sby: core: updated the parsing to match the changes in PR #206
2022-08-18 05:36:10 -04:00
Aki Van Ness
e4a7f624c1
sby: core: config: fixed the engines section parsing where it was not setting the engine mode when parsing the section
2022-08-18 05:36:10 -04:00
Aki Van Ness
204869bfed
sby: core: config: updated the error messages for the new setctions to make them more descriptive
2022-08-18 05:36:10 -04:00
Aki Van Ness
9293081308
modified the mode runners to accept the modified engine layout in preperation for the per-mode engine sections
2022-08-18 05:36:10 -04:00
Aki Van Ness
f1a645bb18
sby: core: config: Updated the [stage] section to use commas for the parents
2022-08-18 05:36:09 -04:00
Aki Van Ness
a0d366e58a
some cleanup, added some rough parser tests, and started altering the engines section
2022-08-18 05:36:09 -04:00
Aki Van Ness
0ab158eea1
sby: core: minor update to the stage parsing
2022-08-18 05:36:09 -04:00
Aki Van Ness
ed82c78acc
sby: core: Added preliminary support for [stage] sections
2022-08-18 05:36:08 -04:00
Aki Van Ness
4cccbf77fa
sby: core: Added preliminary support for the [setup] section
2022-08-18 05:36:08 -04:00
Jannis Harder
0aebf0b4d0
aig model: Call memory_map late to avoid performance issues
...
This requires running simplemap on the output as memory_map produces
coarse-grained cells even though we already have a fine-grained design.
2022-08-17 16:41:32 +02:00
Jannis Harder
3412ea859b
New "none" engine to be used with the "make_model" option
2022-08-05 16:31:15 +02:00
Jannis Harder
231f0b80aa
Add make_model option to generate models not required by the task
...
Useful to do custom things (like counter example minimization) but still
use sby's flow to prepare models.
2022-08-05 16:31:15 +02:00
Jannis Harder
22585b33dc
Use 'rename -witness' instead of multiple 'rename -enumerate'
2022-08-05 16:31:15 +02:00
Jannis Harder
d3520037b9
Write native yosys witness traces
2022-08-05 16:31:15 +02:00
Jannis Harder
acaf6ef0c2
Use new memory_map -formal for aiger/_nomem
2022-08-05 16:31:15 +02:00
Jannis Harder
5265a52b65
Refactor flow to use a common prep model
...
The goal of this is to make sure that all backend flows are compatible
and we can map between them, so that e.g. the aiger model can be used to
minimize a counterexample trace produced by smtbmc. Reducing the parts
that differ per backend (including parts that receive different input
depending on the used backend) also makes testing more effective as the
common parts are easier to cover.
2022-08-05 16:31:15 +02:00
Jannis Harder
edb068bff4
Fix print_junit_results failure during some error conditions
...
There is a small window between setting self.precise_prop_status and
initializing self.design. I've only managed to produce an error within
that windows during development, but getting unrelated stacktraces from
print_junit_result failing distracts from debugging the issue at hand.
2022-08-05 16:31:15 +02:00
Aki Van Ness
46ca20f8ec
sby: core: ensured to strip the line of any uneeded whitespace
2022-08-04 06:13:28 -04:00
Aki Van Ness
9368f3f987
sby: core: explicitly split the the entries for the [options] section params to be at most one,
2022-08-04 06:13:28 -04:00
Aki Van Ness
10234fef00
sby: core: changed how the split for the section header and arguments are done, with a prior strip to remove and extra whitespace
2022-08-04 06:13:28 -04:00
Aki Van Ness
8133aaa8f8
sby: core: changed how the sections and their arguments are handled and cleared up the strangly worded error messages related to that
2022-08-04 06:13:28 -04:00
Aki Van Ness
59dc27ed73
sby: core: config: cleaned up the error messages to make them less opaque
2022-08-01 10:16:05 -04:00
N. Engelhardt
3ff2c9affc
avoid erroring out when coarse-grain logic loops can be resolved by mapping to fine grain operators
2022-07-25 16:22:32 +02:00
Jannis Harder
5d3f784beb
Fix a race-condition SbyProc that could truncate output
...
Present for a long time, but was not easy to hit. Some of my work in
progress changes made this much more likely and running the complete
test suite in parallel had a good chance of reproducing this for at
least one of the tests.
2022-07-13 16:01:49 +02:00
Jannis Harder
b3b315a473
Make SbyProc hide Windows differences in retcode handling
...
Without this, we don't properly detect missing solver binaries and do
not properly handle the return status of the pono solver.
2022-07-06 11:22:59 +02:00
Jannis Harder
ff802086b4
test uninited FFs with const clks and fix btor script for this
2022-07-04 14:03:56 +02:00
Jannis Harder
e3123283ea
Merge pull request #170 from programmerjake/add-simcheck-option
...
switch to using hierarchy -smtcheck for smtlib2 solvers, allowing smtlib2_module modules
2022-07-03 11:47:22 +02:00
Jannis Harder
b4458d43d7
Automatic engine selection
2022-06-27 15:58:42 +02:00
Jannis Harder
5014d74023
sby_design: Extract total memory size and forall usage
2022-06-24 13:50:26 +02:00
db740839b7
switch to using hierarchy -smtcheck for smtlib2 solvers, allowing smtlib2_module modules.
...
Fixes : #168
Depends on: https://github.com/YosysHQ/yosys/pull/3391
2022-06-22 21:17:29 -07:00
Jannis Harder
0fe8c223cf
Decouple taskloop from task
2022-06-15 16:28:09 +02:00
Jannis Harder
d1c04f79d6
Use monotonic clock for timeouts
2022-06-15 14:11:25 +02:00
Jannis Harder
d0c59a3155
Don't use python asserts to handle unexpected solver output
2022-06-15 13:25:21 +02:00
Jannis Harder
e99884e319
SbyProc: New error_callback instead of exit_callback for failing procs
2022-06-15 13:25:21 +02:00
Jannis Harder
6daa434d85
Add --dumptaskinfo option to output some .sby metadata as json
2022-04-11 17:44:10 +02:00
N. Engelhardt
8ce526c22d
junit: use write_jny instead of write_json
2022-04-06 18:35:01 +02:00
N. Engelhardt
008d020c4d
note unexpected return statuses in junit
2022-03-29 19:10:29 +02:00
Jannis Harder
079df4d95f
Use -no-startoffset, avoiding index mismatch between aiger and smt2
2022-03-25 11:41:08 +01:00
N. Engelhardt
7142f790e4
add testcase for overall run result
2022-02-24 22:44:11 +01:00
N. Engelhardt
89ed843ff1
validate junit files (with extra attributes added to schema)
2022-02-22 16:16:37 +01:00
N. Engelhardt
7ee357fcc8
fix induction
2022-02-07 22:01:52 +01:00
N. Engelhardt
7d3545dc86
fix junit error/failure/skipped count
2022-02-07 19:20:29 +01:00
N. Engelhardt
53eb25fcae
handle unreached cover properties
2022-02-07 15:29:36 +01:00
N. Engelhardt
5abaccab69
refactor junit print into own function
2022-02-07 12:29:27 +01:00
N. Engelhardt
d7e7f2c530
refactor model to have single base
2022-01-31 12:35:56 +01:00
N. Engelhardt
1cf27e7c31
parse solver location output for assert failures (cover not functional yet)
2022-01-27 13:41:07 +01:00
N. Engelhardt
7f3c4137c1
create json export and read in properties
2022-01-19 19:34:11 +01:00
