Jannis Harder [Wed, 6 Jul 2022 09:19:51 +0000 (11:19 +0200)]
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.
Jannis Harder [Tue, 5 Jul 2022 14:09:54 +0000 (16:09 +0200)]
Merge pull request #190 from jix/windows_fixes
tests: Windows fixes
Jannis Harder [Tue, 5 Jul 2022 13:34:27 +0000 (15:34 +0200)]
tests: Windows fixes
Make tests runnable on Windows, as long as a unix like environment as
e.g. provided by MSYS2 is available.
Jannis Harder [Mon, 4 Jul 2022 15:47:16 +0000 (17:47 +0200)]
Merge pull request #187 from jix/const_clocks
Test uninitialized FFs with constant clocks and fix btor script for this
Jannis Harder [Wed, 29 Jun 2022 16:00:52 +0000 (18:00 +0200)]
test uninited FFs with const clks and fix btor script for this
Jannis Harder [Mon, 4 Jul 2022 12:03:06 +0000 (14:03 +0200)]
Merge pull request #186 from jix/ff_xinit_opt
tests: Test for invalid x-value FF init optimizations
Jannis Harder [Wed, 29 Jun 2022 14:43:07 +0000 (16:43 +0200)]
tests: Test for invalid x-value FF init optimizations
Jannis Harder [Sun, 3 Jul 2022 09:47:22 +0000 (11:47 +0200)]
Merge pull request #170 from programmerjake/add-simcheck-option
switch to using hierarchy -smtcheck for smtlib2 solvers, allowing smtlib2_module modules
Jannis Harder [Thu, 30 Jun 2022 15:53:22 +0000 (17:53 +0200)]
Merge pull request #189 from jix/autotune_docs
docs: add missing autotune.rst
Jannis Harder [Thu, 30 Jun 2022 15:50:05 +0000 (17:50 +0200)]
docs: add missing autotune.rst
Jannis Harder [Wed, 29 Jun 2022 14:48:06 +0000 (16:48 +0200)]
Merge pull request #158 from jix/autotune
Autotune: Automatic engine selection
Jannis Harder [Mon, 27 Jun 2022 13:57:22 +0000 (15:57 +0200)]
autotune: Initial documentation
Jannis Harder [Thu, 23 Jun 2022 14:37:56 +0000 (16:37 +0200)]
Test autotune
Jannis Harder [Mon, 25 Apr 2022 10:27:18 +0000 (12:27 +0200)]
Automatic engine selection
Jannis Harder [Tue, 14 Jun 2022 16:04:24 +0000 (18:04 +0200)]
sby_design: Extract total memory size and forall usage
Jannis Harder [Fri, 24 Jun 2022 10:40:09 +0000 (12:40 +0200)]
Merge pull request #185 from georgerennie/prefix_empty_taskname
Use default prefix directory when no task is specified
Jannis Harder [Thu, 23 Jun 2022 14:39:32 +0000 (16:39 +0200)]
Merge pull request #183 from jix/engine-option-docs
Reflect recent engine updates in the reference docs
Jannis Harder [Thu, 23 Jun 2022 11:37:38 +0000 (13:37 +0200)]
Merge pull request #184 from jix/smtbmc-keepgoing-induction-trace-fix
smtbmc: Fix induction trace filename with --keep-going for the basecase
Jannis Harder [Thu, 23 Jun 2022 11:15:58 +0000 (13:15 +0200)]
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.
Jacob Lifshay [Thu, 23 Jun 2022 04:17:29 +0000 (21:17 -0700)]
switch to using hierarchy -smtcheck for smtlib2 solvers, allowing smtlib2_module modules.
Fixes: #168
Depends on: https://github.com/YosysHQ/yosys/pull/3391
Jannis Harder [Mon, 20 Jun 2022 12:59:00 +0000 (14:59 +0200)]
Reflect recent engine updates in the reference docs
George Rennie [Sat, 18 Jun 2022 23:49:12 +0000 (00:49 +0100)]
Use default prefix directory when no task is specified
Jannis Harder [Wed, 15 Jun 2022 14:41:39 +0000 (16:41 +0200)]
Merge pull request #182 from jix/taskloop
Decouple taskloop from task
Jannis Harder [Thu, 21 Apr 2022 14:22:32 +0000 (16:22 +0200)]
Decouple taskloop from task
Jannis Harder [Wed, 15 Jun 2022 14:27:23 +0000 (16:27 +0200)]
Merge pull request #181 from jix/monotonic
Use monotonic clock for timeouts
Jannis Harder [Mon, 25 Apr 2022 13:43:59 +0000 (15:43 +0200)]
Use monotonic clock for timeouts
Jannis Harder [Wed, 15 Jun 2022 12:08:15 +0000 (14:08 +0200)]
Merge pull request #180 from jix/sby-fewer-asserts
Don't use python asserts to handle unexpected solver output
Jannis Harder [Tue, 14 Jun 2022 15:59:08 +0000 (17:59 +0200)]
Don't use python asserts to handle unexpected solver output
Jannis Harder [Wed, 15 Jun 2022 10:10:52 +0000 (12:10 +0200)]
SbyProc: New error_callback instead of exit_callback for failing procs
Jannis Harder [Wed, 15 Jun 2022 11:24:36 +0000 (13:24 +0200)]
Merge pull request #179 from jix/btor-option-handling
btor pono: improve option handling
Jannis Harder [Tue, 14 Jun 2022 15:56:54 +0000 (17:56 +0200)]
btor pono: improve option handling
Fail on the unsupported skip option and pass solver args to pono.
Jannis Harder [Tue, 14 Jun 2022 15:52:33 +0000 (17:52 +0200)]
Merge pull request #178 from jix/aiger-aigbmc-fixes
aiger: check supported modes and aigbmc fixes
Jannis Harder [Tue, 14 Jun 2022 15:15:32 +0000 (17:15 +0200)]
aiger: check supported modes and aigbmc fixes
Jannis Harder [Tue, 14 Jun 2022 13:54:09 +0000 (15:54 +0200)]
Merge pull request #177 from mattvenn/tristate-example
Tristate example
Matt Venn [Tue, 14 Jun 2022 13:35:22 +0000 (15:35 +0200)]
add makefile for test
Matt Venn [Mon, 13 Jun 2022 12:00:08 +0000 (14:00 +0200)]
remove unused module port
Matt Venn [Mon, 13 Jun 2022 11:59:12 +0000 (13:59 +0200)]
expect fail
Matt Venn [Mon, 13 Jun 2022 11:51:04 +0000 (13:51 +0200)]
tristate example
Jannis Harder [Mon, 13 Jun 2022 12:05:37 +0000 (14:05 +0200)]
Merge pull request #172 from jix/smtbmc-unroll-noincr-traces-fix
Regression test for smtbmc --unroll --noincr
Jannis Harder [Mon, 13 Jun 2022 11:59:31 +0000 (13:59 +0200)]
Merge pull request #175 from jix/more-test-improvements
Use the test Makefile for all examples
Jannis Harder [Mon, 13 Jun 2022 11:20:33 +0000 (13:20 +0200)]
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
Jannis Harder [Wed, 8 Jun 2022 10:08:34 +0000 (12:08 +0200)]
Regression test for smtbmc --unroll --noincr
Jannis Harder [Fri, 10 Jun 2022 13:24:49 +0000 (15:24 +0200)]
Merge pull request #173 from jix/test-cvc
Test that cvc4 and cvc5 can be used
Jannis Harder [Fri, 10 Jun 2022 13:14:01 +0000 (15:14 +0200)]
Merge pull request #164 from jix/suggest_f_flag
Suggest -f when the workdir already exists
Jannis Harder [Wed, 8 Jun 2022 11:33:12 +0000 (13:33 +0200)]
Test that cvc4 and cvc5 can be used
Jannis Harder [Wed, 8 Jun 2022 09:43:43 +0000 (11:43 +0200)]
Merge pull request #171 from jix/make-remove-unused-tool-list
tests: Remove unused tool list in test Makefile
Jannis Harder [Wed, 8 Jun 2022 09:32:35 +0000 (11:32 +0200)]
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.
Jannis Harder [Wed, 8 Jun 2022 07:43:47 +0000 (09:43 +0200)]
Merge pull request #169 from jix/yices-forall
Test designs using $allconst
Jannis Harder [Tue, 7 Jun 2022 12:50:59 +0000 (14:50 +0200)]
Merge pull request #163 from jix/make_improvements
Test makefile improvements
Jannis Harder [Tue, 7 Jun 2022 12:29:25 +0000 (14:29 +0200)]
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.
Jannis Harder [Fri, 3 Jun 2022 15:16:01 +0000 (17:16 +0200)]
Don't fail tests when xmlschema is missing
Jannis Harder [Fri, 3 Jun 2022 14:48:21 +0000 (16:48 +0200)]
Test designs using $allconst
Jannis Harder [Thu, 2 Jun 2022 14:25:11 +0000 (16:25 +0200)]
tests: Fail on CI when any required tool is missing
Jannis Harder [Thu, 2 Jun 2022 14:24:30 +0000 (16:24 +0200)]
tests: Check for btorsim --vcd
N. Engelhardt [Wed, 1 Jun 2022 14:51:28 +0000 (16:51 +0200)]
update install instructions for btorsim
Jannis Harder [Mon, 30 May 2022 14:18:37 +0000 (16:18 +0200)]
Suggest -f when the workdir already exists
Jannis Harder [Mon, 30 May 2022 13:27:14 +0000 (15:27 +0200)]
Check for the tabby/oss cad suite before running make ci checks
Jannis Harder [Mon, 30 May 2022 12:37:20 +0000 (14:37 +0200)]
Better checking of available solvers
Check for required auxiliary tools and always regenerate the make rules
when the set of available tools changes.
Jannis Harder [Mon, 30 May 2022 11:35:57 +0000 (13:35 +0200)]
Makefile: Rename run_tests to test, update help, use .PHONY
Jannis Harder [Thu, 26 May 2022 10:00:05 +0000 (12:00 +0200)]
Merge pull request #161 from programmerjake/add-div-mod-floor-tests
add test for yosys's $divfloor and $modfloor cells
Jacob Lifshay [Wed, 25 May 2022 10:35:21 +0000 (03:35 -0700)]
add depth 1
Jacob Lifshay [Wed, 25 May 2022 00:51:48 +0000 (17:51 -0700)]
add test for yosys's $divfloor and $modfloor cells
Depends on: https://github.com/YosysHQ/yosys/pull/3335
N. Engelhardt [Tue, 24 May 2022 09:39:10 +0000 (11:39 +0200)]
docs: add instructions for newer btorsim version required
Jannis Harder [Wed, 11 May 2022 09:23:57 +0000 (11:23 +0200)]
Merge pull request #159 from jix/fix-dpmem-example
examples: Fix use of SVA value change expressions
Jannis Harder [Wed, 11 May 2022 08:38:54 +0000 (10:38 +0200)]
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.
Jannis Harder [Mon, 25 Apr 2022 09:21:21 +0000 (11:21 +0200)]
Merge pull request #156 from jix/refactor-tests
Refactor tests
Jannis Harder [Mon, 11 Apr 2022 15:39:05 +0000 (17:39 +0200)]
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.
Jannis Harder [Mon, 11 Apr 2022 15:37:27 +0000 (17:37 +0200)]
Add --dumptaskinfo option to output some .sby metadata as json
Jannis Harder [Mon, 11 Apr 2022 15:35:11 +0000 (17:35 +0200)]
Add envvar to enable automatic .gitignore creation for workdirs
Miodrag Milanović [Fri, 8 Apr 2022 13:26:48 +0000 (15:26 +0200)]
Merge pull request #140 from nakengelhardt/junit_jny
junit: use write_jny instead of write_json
N. Engelhardt [Thu, 10 Mar 2022 16:46:08 +0000 (17:46 +0100)]
junit: use write_jny instead of write_json
Miodrag Milanović [Sun, 3 Apr 2022 10:15:58 +0000 (12:15 +0200)]
Merge pull request #155 from jix/invalid_ff_dcinit_merge
Regression test: do not merge FFs with unconstrained initvals
Jannis Harder [Fri, 1 Apr 2022 17:25:09 +0000 (19:25 +0200)]
Regression test: do not merge FFs with unconstrained initvals
Currently done by `opt -keepdc` via `opt_merge` but not valid in a
formal context.
Jannis Harder [Thu, 31 Mar 2022 14:35:40 +0000 (16:35 +0200)]
Merge pull request #154 from jix/sby_design-fixes
sby_design fixes
Jannis Harder [Thu, 31 Mar 2022 13:51:58 +0000 (15:51 +0200)]
Fix design_hierarchy handling of $paramod cells
Jannis Harder [Thu, 31 Mar 2022 11:12:15 +0000 (13:12 +0200)]
Fix variable name in find_property_by_cellname's error path
Jannis Harder [Wed, 30 Mar 2022 12:48:04 +0000 (14:48 +0200)]
Merge pull request #151 from jix/prefer-first-trace
Prefer the first tracefile for each failing assertion
Jannis Harder [Wed, 30 Mar 2022 11:35:57 +0000 (13:35 +0200)]
Prefer the first tracefile for each failing assertion
N. Engelhardt [Wed, 30 Mar 2022 10:53:48 +0000 (12:53 +0200)]
Merge pull request #150 from nakengelhardt/fix_junit_type_assignment
note unexpected return statuses in junit
Jannis Harder [Wed, 30 Mar 2022 09:42:48 +0000 (11:42 +0200)]
Merge pull request #147 from jix/smtbmc-keepgoing
Support and tests for smtbmc `--keep-going`
Jannis Harder [Thu, 24 Mar 2022 15:36:59 +0000 (16:36 +0100)]
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.
N. Engelhardt [Tue, 29 Mar 2022 17:10:29 +0000 (19:10 +0200)]
note unexpected return statuses in junit
N. Engelhardt [Mon, 28 Mar 2022 14:34:00 +0000 (16:34 +0200)]
Merge pull request #148 from nakengelhardt/docs_updates
documentation updates
N. Engelhardt [Mon, 28 Mar 2022 14:32:54 +0000 (16:32 +0200)]
Merge pull request #145 from nakengelhardt/fix_junit_tracefile
junit: handle multiple asserts failing with the same trace
N. Engelhardt [Mon, 28 Mar 2022 14:32:10 +0000 (16:32 +0200)]
Merge pull request #142 from nakengelhardt/fix_backslash_smt2
translate backslashes in cell names the same way as smt2 backend does
Miodrag Milanović [Sat, 26 Mar 2022 07:20:57 +0000 (08:20 +0100)]
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
N. Engelhardt [Fri, 25 Mar 2022 17:01:09 +0000 (18:01 +0100)]
document btor engine, add overview of mode/engine/solver combinations, remove unimplemented modes
Jannis Harder [Thu, 24 Mar 2022 12:12:25 +0000 (13:12 +0100)]
Test signals with nonzero start offsets in aim files with smtbmc
Jannis Harder [Fri, 25 Mar 2022 10:38:22 +0000 (11:38 +0100)]
Use `-no-startoffset`, avoiding index mismatch between aiger and smt2
Jannis Harder [Mon, 21 Mar 2022 17:36:09 +0000 (18:36 +0100)]
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.
N. Engelhardt [Tue, 22 Mar 2022 15:16:02 +0000 (16:16 +0100)]
junit: handle multiple asserts failing with the same trace
N. Engelhardt [Fri, 18 Mar 2022 15:36:41 +0000 (16:36 +0100)]
translate backslashes in cell names the same way as smt2 backend does
Claire Xen [Tue, 15 Mar 2022 15:33:46 +0000 (16:33 +0100)]
Merge pull request #120 from ythoma/patch-1
Update install.rst
N. Engelhardt [Tue, 15 Mar 2022 15:06:52 +0000 (16:06 +0100)]
Merge pull request #139 from nakengelhardt/housekeeping
housekeeping
N. Engelhardt [Tue, 15 Mar 2022 14:12:59 +0000 (15:12 +0100)]
ci housekeeping
N. Engelhardt [Mon, 7 Mar 2022 15:25:47 +0000 (16:25 +0100)]
Merge pull request #133 from nakengelhardt/sby_junit
improve SBY JUnit report
N. Engelhardt [Mon, 7 Mar 2022 07:34:01 +0000 (08:34 +0100)]
fix ci
N. Engelhardt [Thu, 24 Feb 2022 21:44:11 +0000 (22:44 +0100)]
add testcase for overall run result
N. Engelhardt [Tue, 22 Feb 2022 15:16:37 +0000 (16:16 +0100)]
validate junit files (with extra attributes added to schema)
N. Engelhardt [Mon, 7 Feb 2022 21:01:52 +0000 (22:01 +0100)]
fix induction