Merge pull request #175 from jix/more-test-improvements

Use the test Makefile for all examples

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

Merge pull request #173 from jix/test-cvc

Test that cvc4 and cvc5 can be used

Merge pull request #164 from jix/suggest_f_flag

Suggest -f when the workdir already exists

Test that cvc4 and cvc5 can be used

Merge pull request #171 from jix/make-remove-unused-tool-list

tests: Remove unused tool list in test Makefile

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.

Merge pull request #169 from jix/yices-forall

Test designs using $allconst

Merge pull request #163 from jix/make_improvements

Test makefile improvements

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.

Don't fail tests when xmlschema is missing

Test designs using $allconst

tests: Fail on CI when any required tool is missing

tests: Check for btorsim --vcd

update install instructions for btorsim

Suggest -f when the workdir already exists

Check for the tabby/oss cad suite before running make ci checks

Better checking of available solvers

Check for required auxiliary tools and always regenerate the make rules
when the set of available tools changes.

Makefile: Rename run_tests to test, update help, use .PHONY

Merge pull request #161 from programmerjake/add-div-mod-floor-tests

add test for yosys's $divfloor and $modfloor cells

add depth 1

add test for yosys's $divfloor and $modfloor cells

Depends on: https://github.com/YosysHQ/yosys/pull/3335

docs: add instructions for newer btorsim version required

Merge pull request #159 from jix/fix-dpmem-example

examples: Fix use of SVA value change expressions

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.

Merge pull request #156 from jix/refactor-tests

Refactor tests

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.

Add --dumptaskinfo option to output some .sby metadata as json

Add envvar to enable automatic .gitignore creation for workdirs

Merge pull request #140 from nakengelhardt/junit_jny

junit: use write_jny instead of write_json

junit: use write_jny instead of write_json

Merge pull request #155 from jix/invalid_ff_dcinit_merge

Regression test: do not merge FFs with unconstrained initvals

Regression test: do not merge FFs with unconstrained initvals

Currently done by `opt -keepdc` via `opt_merge` but not valid in a
formal context.

Merge pull request #154 from jix/sby_design-fixes

sby_design fixes

Fix design_hierarchy handling of $paramod cells

Fix variable name in find_property_by_cellname's error path

Merge pull request #151 from jix/prefer-first-trace

Prefer the first tracefile for each failing assertion

Prefer the first tracefile for each failing assertion

Merge pull request #150 from nakengelhardt/fix_junit_type_assignment

note unexpected return statuses in junit

Merge pull request #147 from jix/smtbmc-keepgoing

Support and tests for smtbmc `--keep-going`

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.

note unexpected return statuses in junit

Merge pull request #148 from nakengelhardt/docs_updates

documentation updates

Merge pull request #145 from nakengelhardt/fix_junit_tracefile

junit: handle multiple asserts failing with the same trace

Merge pull request #142 from nakengelhardt/fix_backslash_smt2

translate backslashes in cell names the same way as smt2 backend does

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

document btor engine, add overview of mode/engine/solver combinations, remove unimplemented modes

Test signals with nonzero start offsets in aim files with smtbmc

Use `-no-startoffset`, avoiding index mismatch between aiger and smt2

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.

junit: handle multiple asserts failing with the same trace

translate backslashes in cell names the same way as smt2 backend does

Merge pull request #120 from ythoma/patch-1

Update install.rst

Merge pull request #139 from nakengelhardt/housekeeping

housekeeping

ci housekeeping

Merge pull request #133 from nakengelhardt/sby_junit

improve SBY JUnit report

fix ci

add testcase for overall run result

validate junit files (with extra attributes added to schema)

fix induction

fix junit error/failure/skipped count

handle unreached cover properties

refactor junit print into own function

handle status of cover properties

refactor model to have single base

parse solver location output for assert failures (cover not functional yet)

add fallback if solver can't tell which property fails

create json export and read in properties

WIP change junit print to conform to schema; needs additional data, currently printing dummy info

Signed-off-by: N. Engelhardt <nak@yosyshq.com>

add JUnit schema and validator

Signed-off-by: N. Engelhardt <nak@yosyshq.com>

Merge pull request #138 from YosysHQ/mmicko/ci

Added CI

Added CI

Merge pull request #136 from nakengelhardt/fix_pono

use --witness option when calling pono

create only a single bad when using pono solver; workaround for #137

add testcase exposing #137

use --witness option when calling pono

Merge pull request #135 from nakengelhardt/rename_task

Rename SbyJob to SbyTask and SbyTask to SbyProc to reduce confusion

Merge pull request #134 from nakengelhardt/advertise_suite_in_readme

mention tabby+oss cad suite in readme

Rename SbyJob to SbyTask and SbyTask to SbyProc to reduce confusion. Config file tasks now correspond to SbyTasks.

mention tabby+oss cad suite in readme

Improvements and cleanups in tasks handling

Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>

Fixed [tasks] section parsing

Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>

Update README.md

Update README.md

Add inductive invariants example

Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>

Add ":"-syntax for [tasks] section

Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>

Update docs theme

Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>

Update docs theme

Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>

update docs theme

Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>

Add support for directories in [files] section

Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>

Fixed names and links

Merge pull request #127 from christian-krieg/feat/update-docs_super-prove

Updated install instructions for super_prove

Fix regression

Initialize variable

Merge pull request #126 from piegamesde/master

Various improvements and fixes

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

fixup! Allow to set a working directory even when having multiple tasks

Better error message when tasks failed

Turn .format() strings into f-strings

Allow to set a working directory even when having multiple tasks

Fixes #125.