Merge pull request #185 from georgerennie/prefix_empty_taskname

Use default prefix directory when no task is specified

Merge pull request #183 from jix/engine-option-docs

Reflect recent engine updates in the reference docs

Merge pull request #184 from jix/smtbmc-keepgoing-induction-trace-fix

smtbmc: Fix induction trace filename with --keep-going for the basecase

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.

Reflect recent engine updates in the reference docs

Use default prefix directory when no task is specified

Merge pull request #182 from jix/taskloop

Decouple taskloop from task

Decouple taskloop from task

Merge pull request #181 from jix/monotonic

Use monotonic clock for timeouts

Use monotonic clock for timeouts

Merge pull request #180 from jix/sby-fewer-asserts

Don't use python asserts to handle unexpected solver output

Don't use python asserts to handle unexpected solver output

SbyProc: New error_callback instead of exit_callback for failing procs

Merge pull request #179 from jix/btor-option-handling

btor pono: improve option handling

btor pono: improve option handling

Fail on the unsupported skip option and pass solver args to pono.

Merge pull request #178 from jix/aiger-aigbmc-fixes

aiger: check supported modes and aigbmc fixes

aiger: check supported modes and aigbmc fixes

Merge pull request #177 from mattvenn/tristate-example

Tristate example

add makefile for test

remove unused module port

expect fail

tristate example

Merge pull request #172 from jix/smtbmc-unroll-noincr-traces-fix

Regression test for smtbmc --unroll --noincr

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

Regression test for smtbmc --unroll --noincr

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