N. Engelhardt
41cd8e5b5e
update install instructions for btorsim
2022-06-01 16:51:28 +02:00
Jannis Harder
de00dc71db
Merge pull request #161 from programmerjake/add-div-mod-floor-tests
...
add test for yosys's $divfloor and $modfloor cells
2022-05-26 12:00:05 +02:00
a87d21a802
add depth 1
2022-05-25 03:35:21 -07:00
3f32deb8c9
add test for yosys's $divfloor and $modfloor cells
...
Depends on: https://github.com/YosysHQ/yosys/pull/3335
2022-05-24 17:51:48 -07:00
N. Engelhardt
ad2c33dd37
docs: add instructions for newer btorsim version required
2022-05-24 11:39:10 +02:00
Jannis Harder
d10e472edf
Merge pull request #159 from jix/fix-dpmem-example
...
examples: Fix use of SVA value change expressions
2022-05-11 11:23:57 +02:00
Jannis Harder
fedfae0e9c
examples: Fix use of SVA value change expressions
...
The $stable value change expression cannot be true for a non-x signal in
the initial state. This is now correctly handled by the verific import,
so the dpmem example needs to start assuming `$stable` only after
leaving the initial state.
2022-05-11 10:38:54 +02:00
Jannis Harder
832888f0f0
Merge pull request #156 from jix/refactor-tests
...
Refactor tests
2022-04-25 11:21:21 +02:00
Jannis Harder
8da6f07cb3
Refactor tests
...
Organize tests into subdirectories and use a new makefile that scans
.sby files and allows selecting tests by mode, engine, solver and/or
subdirectory. Automatically skips tests that use engines/solvers that
are not found in the PATH.
See `cd tests; make help` for a description of supported make targets.
2022-04-11 17:50:38 +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
Miodrag Milanović
1e1aea0b1e
Merge pull request #140 from nakengelhardt/junit_jny
...
junit: use write_jny instead of write_json
2022-04-08 15:26:48 +02:00
N. Engelhardt
8ce526c22d
junit: use write_jny instead of write_json
2022-04-06 18:35:01 +02:00
Miodrag Milanović
4886ed7e19
Merge pull request #155 from jix/invalid_ff_dcinit_merge
...
Regression test: do not merge FFs with unconstrained initvals
2022-04-03 12:15:58 +02:00
Jannis Harder
ef236eeddc
Regression test: do not merge FFs with unconstrained initvals
...
Currently done by `opt -keepdc` via `opt_merge` but not valid in a
formal context.
2022-04-01 19:25:09 +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
43a79965c3
Merge pull request #151 from jix/prefer-first-trace
...
Prefer the first tracefile for each failing assertion
2022-03-30 14:48:04 +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
Jannis Harder
2d3d96478a
Tests for --keep-going
...
This also changes the test Makefile to run `.check.py` files after
running the corresponding `.sby` file to allow more precise testing of
the keep going feature.
2022-03-30 11:26:58 +02:00
N. Engelhardt
008d020c4d
note unexpected return statuses in junit
2022-03-29 19:10:29 +02:00
N. Engelhardt
adacad7908
Merge pull request #148 from nakengelhardt/docs_updates
...
documentation updates
2022-03-28 16:34:00 +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
Miodrag Milanović
7a4a8e6bf6
Merge pull request #146 from jix/aim_vs_smt2_nonzero_start_offset
...
Test and fix signals with nonzero start offsets in aim files with smtbmc
2022-03-26 08:20:57 +01:00
N. Engelhardt
3834fe7622
document btor engine, add overview of mode/engine/solver combinations, remove unimplemented modes
2022-03-25 18:01:09 +01:00
Jannis Harder
a434252ca1
Test signals with nonzero start offsets in aim files with smtbmc
2022-03-25 15:18:45 +01: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
Claire Xen
fa5d5ad831
Merge pull request #120 from ythoma/patch-1
...
Update install.rst
2022-03-15 16:33:46 +01:00
N. Engelhardt
b14270bedb
Merge pull request #139 from nakengelhardt/housekeeping
...
housekeeping
2022-03-15 16:06:52 +01:00
N. Engelhardt
2441940653
ci housekeeping
2022-03-15 15:12:59 +01:00
N. Engelhardt
419ef76f82
Merge pull request #133 from nakengelhardt/sby_junit
...
improve SBY JUnit report
2022-03-07 16:25:47 +01:00
N. Engelhardt
8a81b61321
fix ci
2022-03-07 08:34:01 +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
N. Engelhardt
a9d1972c47
add fallback if solver can't tell which property fails
2022-01-21 15:18:53 +01:00
N. Engelhardt
7f3c4137c1
create json export and read in properties
2022-01-19 19:34:11 +01:00
