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
07d19b202b
Merge pull request #195 from jix/sbyproc-truncated-output
...
Fix a race-condition SbyProc that could truncate output
2022-07-13 17:30:36 +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
92e7eb2e32
abc pdr: Enable log output by default
...
This makes it consistent with the other abc solvers and shows whether
abc pdr is making progress.
2022-07-08 12:36:44 +02:00
Jannis Harder
de43a4c936
Merge pull request #191 from jix/early-readconfig
...
Read config before creating a workdir
2022-07-06 12:05:13 +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
566edad13c
Read config before creating a workdir
...
When using a task name not defined in the config, this now produces an
error before creating an unnecessary workdir for that non-existing task.
2022-07-05 17:20:55 +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
Jannis Harder
157bb156c0
Merge pull request #185 from georgerennie/prefix_empty_taskname
...
Use default prefix directory when no task is specified
2022-06-24 12:40:09 +02:00
Jannis Harder
3dcf7766ea
smtbmc: Fix induction trace filename with --keep-going for the basecase
...
--keep-going only applies to the basecase and induction runs without that
option, so the trace filename for induction should have no placeholder.
2022-06-23 13:15:58 +02:00
Jacob Lifshay
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
George Rennie
0308142fa4
Use default prefix directory when no task is specified
2022-06-19 00:49:12 +01: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
141ffd34a5
btor pono: improve option handling
...
Fail on the unsupported skip option and pass solver args to pono.
2022-06-15 11:35:22 +02:00
Jannis Harder
05d963b0df
aiger: check supported modes and aigbmc fixes
2022-06-14 17:41:06 +02:00
Jannis Harder
499371fd39
Use the test Makefile for all examples
...
* Rename and move sbysrc/demo[123].sby to docs/examples/demos
* Make them use multiple tasks for multiple engines
* Scan docs/examples for sby files for make test
* `make ci` is now `NOSKIP` by default
* Skip scripts using `verific` w/o yosys verific support
* This does not fail even with NOSKIP set
2022-06-13 13:42:58 +02:00
Jannis Harder
8e87b0f7f4
Suggest -f when the workdir already exists
2022-05-30 16:18:37 +02:00
Jannis Harder
6daa434d85
Add --dumptaskinfo option to output some .sby metadata as json
2022-04-11 17:44:10 +02:00
Jannis Harder
a190994098
Add envvar to enable automatic .gitignore creation for workdirs
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
Jannis Harder
25e982c238
Merge pull request #154 from jix/sby_design-fixes
...
sby_design fixes
2022-03-31 16:35:40 +02:00
Jannis Harder
4b512668b2
Fix design_hierarchy handling of $paramod cells
2022-03-31 15:51:58 +02:00
Jannis Harder
a78eaa57db
Fix variable name in find_property_by_cellname's error path
2022-03-31 13:12:15 +02:00
Jannis Harder
b725bfed0c
Prefer the first tracefile for each failing assertion
2022-03-30 13:47:14 +02:00
N. Engelhardt
2e0087fd2f
Merge pull request #150 from nakengelhardt/fix_junit_type_assignment
...
note unexpected return statuses in junit
2022-03-30 12:53:48 +02:00
Jannis Harder
81e8b6737b
Merge pull request #147 from jix/smtbmc-keepgoing
...
Support and tests for smtbmc `--keep-going`
2022-03-30 11:42:48 +02:00
N. Engelhardt
008d020c4d
note unexpected return statuses in junit
2022-03-29 19:10:29 +02:00
N. Engelhardt
53abf14514
Merge pull request #145 from nakengelhardt/fix_junit_tracefile
...
junit: handle multiple asserts failing with the same trace
2022-03-28 16:32:54 +02:00
N. Engelhardt
3d8f56b89a
Merge pull request #142 from nakengelhardt/fix_backslash_smt2
...
translate backslashes in cell names the same way as smt2 backend does
2022-03-28 16:32:10 +02:00
Jannis Harder
079df4d95f
Use -no-startoffset, avoiding index mismatch between aiger and smt2
2022-03-25 11:41:08 +01:00
Jannis Harder
7824460e27
Initial support for the new smtbmc --keep-going option
...
So far this only passes on the option and adjusts the trace_prefix to
support multiple numbered traces. Further changes are needed to
correctly associate individual traces with the assertions failing in
that trace.
2022-03-24 16:57:16 +01:00
N. Engelhardt
c7e4785a8a
junit: handle multiple asserts failing with the same trace
2022-03-22 16:16:02 +01:00
N. Engelhardt
5dc7fc9a4d
translate backslashes in cell names the same way as smt2 backend does
2022-03-22 11:14:48 +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
9168b0163b
handle status of cover properties
2022-02-06 09:15:44 +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
Jacob Lifshay
