Merge pull request #195 from jix/sbyproc-truncated-output

Fix a race-condition SbyProc that could truncate output

Merge pull request #193 from jix/abc_pdr_v

abc pdr: Enable log output by default

Fix a race-condition SbyProc that could truncate output

Present for a long time, but was not easy to hit. Some of my work in
progress changes made this much more likely and running the complete
test suite in parallel had a good chance of reproducing this for at
least one of the tests.

Update autotune.rst

Merge pull request #194 from jix/autotune_rst_fixes

docs: Don't use linebreaks within inline code spans.

docs: Don't use linebreaks within inline code spans.

abc pdr: Enable log output by default

This makes it consistent with the other abc solvers and shows whether
abc pdr is making progress.

Merge pull request #191 from jix/early-readconfig

Read config before creating a workdir

Merge pull request #192 from jix/win_retcode

Make SbyProc hide Windows differences in retcode handling

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.

Read config before creating a workdir

When using a task name not defined in the config, this now produces an
error before creating an unnecessary workdir for that non-existing task.

Merge pull request #190 from jix/windows_fixes

tests: Windows fixes

tests: Windows fixes

Make tests runnable on Windows, as long as a unix like environment as
e.g. provided by MSYS2 is available.

Merge pull request #187 from jix/const_clocks

Test uninitialized FFs with constant clocks and fix btor script for this

test uninited FFs with const clks and fix btor script for this

Merge pull request #186 from jix/ff_xinit_opt

tests: Test for invalid x-value FF init optimizations

tests: Test for invalid x-value FF init optimizations

Merge pull request #170 from programmerjake/add-simcheck-option

switch to using hierarchy -smtcheck for smtlib2 solvers, allowing smtlib2_module modules

Merge pull request #189 from jix/autotune_docs

docs: add missing autotune.rst

docs: add missing autotune.rst

Merge pull request #158 from jix/autotune

Autotune: Automatic engine selection

autotune: Initial documentation

Test autotune

Automatic engine selection

sby_design: Extract total memory size and forall usage

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.

switch to using hierarchy -smtcheck for smtlib2 solvers, allowing smtlib2_module modules.

Fixes: #168
Depends on: https://github.com/YosysHQ/yosys/pull/3391

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.