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.

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.

Print paths as absolute

This generally makes debugging path issues easier.

Update docs conf.py

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

New docs conf.py

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

Make readme of abstraction example more tutorial-like

Merge pull request #121 from YosysHQ/windows_fix

Windows specific fixes

Windows specific fixes

Update conf.py

Delete symbiotic_logo.png

Update conf.py

Update install.rst

On Ubuntu 20.04, I had to install curl as well:
sudo apt install curl
I guess that would be the same on other setups.

Fix syntax errors

Extract installation procedure to separate file

copyright

logo and links

Merge pull request #116 from nakengelhardt/sed_mac

make install: mac OS compatible sed usage

sed -i option is not posix, and argument syntax is incompatible between mac and linux. use redirects instead

Merge pull request #115 from nakengelhardt/rename_test

rename make test to make ci

rename make test to make ci

Merge pull request #101 from YosysHQ/program-prefix

Add a PROGRAM_PREFIX= Makefile option for packages with prefixed Yosys

Add a PROGRAM_PREFIX= Makefile option for packages with prefixed Yosys.

Run dffunmap before writing the design with aiger/btor/smt2 backends.

fix test rule

Remove redundant copy of picorv32

Signed-off-by: Claire Wolf <claire@symbioticeda.com>

Improvements in "make test"

Signed-off-by: Claire Wolf <claire@symbioticeda.com>

Merge pull request #104 from nakengelhardt/more_tests

add tests directory with additional tests

add tests directory with additional tests

fix error message formatting

Include verilog source files for demo1.sby

Signed-off-by: Claire Wolf <claire@symbioticeda.com>

Merge pull request #102 from YosysHQ/claire/maketest

Add "make test"

Add "Unexpected response" handling to smtbmc engine

Signed-off-by: Claire Wolf <claire@symbioticeda.com>

Add "make test"

Signed-off-by: Claire Wolf <claire@symbioticeda.com>

Merge pull request #99 from whitequark/patch-1

Inject executable dependencies from the environment

Merge pull request #100 from edbordin/master

Use latest windows python launcher from yosys

use latest win python launcher from yosys

Inject executable dependencies from the environment

Merge pull request #98 from YosysHQ/cosa2_to_pono

cosa2 -> pono rename

cosa2 -> pono rename

Merge pull request #97 from nakengelhardt/seed_arg

add --seed option to smtbmc and btor engines

Merge pull request #94 from nakengelhardt/fix_93

ignore race condition in killing already-terminated process

add --seed option to smtbmc and btor engines