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 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
N. Engelhardt [Mon, 7 Feb 2022 18:20:29 +0000 (19:20 +0100)]
fix junit error/failure/skipped count
N. Engelhardt [Mon, 7 Feb 2022 14:29:36 +0000 (15:29 +0100)]
handle unreached cover properties
N. Engelhardt [Mon, 7 Feb 2022 11:29:27 +0000 (12:29 +0100)]
refactor junit print into own function
N. Engelhardt [Sun, 6 Feb 2022 08:15:44 +0000 (09:15 +0100)]
handle status of cover properties
N. Engelhardt [Mon, 31 Jan 2022 11:35:56 +0000 (12:35 +0100)]
refactor model to have single base
N. Engelhardt [Thu, 27 Jan 2022 12:41:07 +0000 (13:41 +0100)]
parse solver location output for assert failures (cover not functional yet)
N. Engelhardt [Fri, 21 Jan 2022 14:18:53 +0000 (15:18 +0100)]
add fallback if solver can't tell which property fails
N. Engelhardt [Wed, 19 Jan 2022 18:34:11 +0000 (19:34 +0100)]
create json export and read in properties
N. Engelhardt [Tue, 7 Dec 2021 19:16:15 +0000 (20:16 +0100)]
WIP change junit print to conform to schema; needs additional data, currently printing dummy info
Signed-off-by: N. Engelhardt <nak@yosyshq.com>
N. Engelhardt [Tue, 7 Dec 2021 19:14:06 +0000 (20:14 +0100)]
add JUnit schema and validator
Signed-off-by: N. Engelhardt <nak@yosyshq.com>
Miodrag Milanović [Wed, 12 Jan 2022 13:24:51 +0000 (14:24 +0100)]
Merge pull request #138 from YosysHQ/mmicko/ci
Added CI
Miodrag Milanovic [Wed, 12 Jan 2022 13:18:17 +0000 (14:18 +0100)]
Added CI
Miodrag Milanović [Wed, 12 Jan 2022 12:46:25 +0000 (13:46 +0100)]
Merge pull request #136 from nakengelhardt/fix_pono
use --witness option when calling pono
N. Engelhardt [Wed, 12 Jan 2022 12:18:54 +0000 (13:18 +0100)]
create only a single bad when using pono solver; workaround for #137
N. Engelhardt [Wed, 12 Jan 2022 10:06:05 +0000 (11:06 +0100)]
add testcase exposing #137
N. Engelhardt [Wed, 12 Jan 2022 09:48:32 +0000 (10:48 +0100)]
use --witness option when calling pono
N. Engelhardt [Wed, 12 Jan 2022 09:52:42 +0000 (10:52 +0100)]
Merge pull request #135 from nakengelhardt/rename_task
Rename SbyJob to SbyTask and SbyTask to SbyProc to reduce confusion
N. Engelhardt [Tue, 11 Jan 2022 16:34:35 +0000 (17:34 +0100)]
Merge pull request #134 from nakengelhardt/advertise_suite_in_readme
mention tabby+oss cad suite in readme
N. Engelhardt [Tue, 11 Jan 2022 15:12:23 +0000 (16:12 +0100)]
Rename SbyJob to SbyTask and SbyTask to SbyProc to reduce confusion. Config file tasks now correspond to SbyTasks.
N. Engelhardt [Tue, 4 Jan 2022 15:32:59 +0000 (16:32 +0100)]
mention tabby+oss cad suite in readme
Claire Xenia Wolf [Sat, 18 Dec 2021 10:36:34 +0000 (11:36 +0100)]
Improvements and cleanups in tasks handling
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
Claire Xenia Wolf [Fri, 17 Dec 2021 19:57:19 +0000 (20:57 +0100)]
Fixed [tasks] section parsing
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
Claire Xen [Fri, 17 Dec 2021 14:50:57 +0000 (15:50 +0100)]
Update README.md
Claire Xen [Fri, 17 Dec 2021 14:48:01 +0000 (15:48 +0100)]
Update README.md
Claire Xenia Wolf [Fri, 17 Dec 2021 14:42:04 +0000 (15:42 +0100)]
Add inductive invariants example
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
Claire Xenia Wolf [Fri, 17 Dec 2021 14:36:35 +0000 (15:36 +0100)]
Add ":"-syntax for [tasks] section
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
Claire Xenia Wolf [Tue, 30 Nov 2021 09:47:43 +0000 (10:47 +0100)]
Update docs theme
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
Claire Xenia Wolf [Mon, 29 Nov 2021 15:51:54 +0000 (16:51 +0100)]
Update docs theme
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
Claire Xenia Wolf [Fri, 26 Nov 2021 19:34:55 +0000 (20:34 +0100)]
update docs theme
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
Claire Xenia Wolf [Sun, 31 Oct 2021 13:43:02 +0000 (14:43 +0100)]
Add support for directories in [files] section
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
Claire Xenia Wolf [Sun, 31 Oct 2021 13:42:39 +0000 (14:42 +0100)]
Fixed names and links
Miodrag Milanović [Mon, 13 Sep 2021 14:21:18 +0000 (16:21 +0200)]
Merge pull request #127 from christian-krieg/feat/update-docs_super-prove
Updated install instructions for super_prove
Miodrag Milanovic [Wed, 25 Aug 2021 10:10:18 +0000 (12:10 +0200)]
Fix regression
Miodrag Milanovic [Wed, 25 Aug 2021 09:38:24 +0000 (11:38 +0200)]
Initialize variable
Claire Xen [Mon, 23 Aug 2021 14:03:03 +0000 (16:03 +0200)]
Merge pull request #126 from piegamesde/master
Various improvements and fixes
Christian Krieg [Tue, 20 Jul 2021 20:33:03 +0000 (22:33 +0200)]
Updated install instructions for super_prove
* Links were dead
* No binaries to download
* Updated with install information from super_prove github repository
* Augmented with additional commands to ease installation
piegames [Thu, 8 Jul 2021 18:48:23 +0000 (20:48 +0200)]
fixup! Allow to set a working directory even when having multiple tasks
piegames [Thu, 24 Jun 2021 22:03:05 +0000 (00:03 +0200)]
Better error message when tasks failed
piegames [Thu, 24 Jun 2021 22:02:22 +0000 (00:02 +0200)]
Turn .format() strings into f-strings
piegames [Mon, 21 Jun 2021 20:32:29 +0000 (22:32 +0200)]
Allow to set a working directory even when having multiple tasks
Fixes #125.
piegames [Mon, 21 Jun 2021 20:31:51 +0000 (22:31 +0200)]
Print paths as absolute
This generally makes debugging path issues easier.
Claire Xenia Wolf [Fri, 21 May 2021 01:36:11 +0000 (03:36 +0200)]
Update docs conf.py
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
Claire Xenia Wolf [Fri, 21 May 2021 01:31:50 +0000 (03:31 +0200)]
New docs conf.py
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
N. Engelhardt [Fri, 16 Apr 2021 13:54:51 +0000 (15:54 +0200)]
Make readme of abstraction example more tutorial-like
Miodrag Milanović [Mon, 22 Mar 2021 15:51:11 +0000 (16:51 +0100)]
Merge pull request #121 from YosysHQ/windows_fix
Windows specific fixes