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

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

Merge pull request #96 from YosysHQ/claire/btorscript

Be more conservative in btor ys script

Merge pull request #95 from adumont/patch-1

Typo: missing * in Global Clock example

Tipo missing * in Global Clock example

Be more conservative in btor ys script

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

ignore race condition in killing already-terminated process

Merge pull request #88 from YosysHQ/claire/cosa2

Add support for cosa2 BTOR solver

Add support for cosa2 BTOR solver

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

btor engine: handle models with 0 properties

Merge pull request #87 from nakengelhardt/cover_trace_summary

Trace generation improvements

fix trace summary printing

call job.terminate at end of btor engine run to kill other engines in case of whoever-gets-there-first runs

start btorsim as soon as a witness is ready, print summary when multiple traces are produced

Add silent mode to SbyTask

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

fix return code check in btor engine

Merge pull request #85 from nakengelhardt/new_btorsim

Note that the btor engine now requires changes not upstreamed to btor2tools yet, see btor2tools/pull/4

Update wolf_goat_cabbage.sv

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

Merge pull request #86 from mattvenn/master

make wolf goat cabbage puzzle gender neutral