Jannis Harder
4ef02d2c5c
Regression test for smtbmc --unroll --noincr
2022-06-13 13:36:42 +02:00
Jannis Harder
1d21513a47
Merge pull request #173 from jix/test-cvc
...
Test that cvc4 and cvc5 can be used
2022-06-10 15:24:49 +02:00
Jannis Harder
d7686ca698
Merge pull request #164 from jix/suggest_f_flag
...
Suggest -f when the workdir already exists
2022-06-10 15:14:01 +02:00
Jannis Harder
d0da57f54f
Test that cvc4 and cvc5 can be used
2022-06-08 13:33:12 +02:00
Jannis Harder
4a9511b80b
Merge pull request #171 from jix/make-remove-unused-tool-list
...
tests: Remove unused tool list in test Makefile
2022-06-08 11:43:43 +02:00
Jannis Harder
675dc03dfe
tests: Remove unused tool list in test Makefile
...
The checks for available tools moved to a python script, so need need to
have a copy of the tool list in the Makefile.
2022-06-08 11:32:35 +02:00
Jannis Harder
534ac21742
Merge pull request #169 from jix/yices-forall
...
Test designs using $allconst
2022-06-08 09:43:47 +02:00
Jannis Harder
2b1a588589
Merge pull request #163 from jix/make_improvements
...
Test makefile improvements
2022-06-07 14:50:59 +02:00
Jannis Harder
34d6adf098
tests: Move required tool checks from rule generation to execution
...
This avoids regenerating the test makefile rules when the set of
installed tools changes and is a bit simpler overall.
2022-06-07 14:29:25 +02:00
Jannis Harder
80eacf34ca
Don't fail tests when xmlschema is missing
2022-06-03 17:22:45 +02:00
Jannis Harder
b4c110815c
Test designs using $allconst
2022-06-03 16:55:06 +02:00
Jannis Harder
d398a3c2df
tests: Fail on CI when any required tool is missing
2022-06-02 16:38:21 +02:00
Jannis Harder
00efdecb4b
tests: Check for btorsim --vcd
2022-06-02 16:38:21 +02:00
N. Engelhardt
41cd8e5b5e
update install instructions for btorsim
2022-06-01 16:51:28 +02:00
Jannis Harder
8e87b0f7f4
Suggest -f when the workdir already exists
2022-05-30 16:18:37 +02:00
Jannis Harder
206562e5de
Check for the tabby/oss cad suite before running make ci checks
2022-05-30 15:52:30 +02:00
Jannis Harder
dc22d97362
Better checking of available solvers
...
Check for required auxiliary tools and always regenerate the make rules
when the set of available tools changes.
2022-05-30 15:02:26 +02:00
Jannis Harder
939e000036
Makefile: Rename run_tests to test, update help, use .PHONY
2022-05-30 15:02:26 +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
Jacob Lifshay
a87d21a802
add depth 1
2022-05-25 03:35:21 -07:00
Jacob Lifshay
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
Jacob Lifshay
