N. Engelhardt
3834fe7622
document btor engine, add overview of mode/engine/solver combinations, remove unimplemented modes
2022-03-25 18:01:09 +01:00
Jannis Harder
a434252ca1
Test signals with nonzero start offsets in aim files with smtbmc
2022-03-25 15:18:45 +01:00
Jannis Harder
079df4d95f
Use -no-startoffset, avoiding index mismatch between aiger and smt2
2022-03-25 11:41:08 +01:00
Jannis Harder
7824460e27
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.
2022-03-24 16:57:16 +01:00
N. Engelhardt
c7e4785a8a
junit: handle multiple asserts failing with the same trace
2022-03-22 16:16:02 +01:00
N. Engelhardt
5dc7fc9a4d
translate backslashes in cell names the same way as smt2 backend does
2022-03-22 11:14:48 +01:00
Claire Xen
fa5d5ad831
Merge pull request #120 from ythoma/patch-1
...
Update install.rst
2022-03-15 16:33:46 +01:00
N. Engelhardt
b14270bedb
Merge pull request #139 from nakengelhardt/housekeeping
...
housekeeping
2022-03-15 16:06:52 +01:00
N. Engelhardt
2441940653
ci housekeeping
2022-03-15 15:12:59 +01:00
N. Engelhardt
419ef76f82
Merge pull request #133 from nakengelhardt/sby_junit
...
improve SBY JUnit report
2022-03-07 16:25:47 +01:00
N. Engelhardt
8a81b61321
fix ci
2022-03-07 08:34:01 +01:00
N. Engelhardt
7142f790e4
add testcase for overall run result
2022-02-24 22:44:11 +01:00
N. Engelhardt
89ed843ff1
validate junit files (with extra attributes added to schema)
2022-02-22 16:16:37 +01:00
N. Engelhardt
7ee357fcc8
fix induction
2022-02-07 22:01:52 +01:00
N. Engelhardt
7d3545dc86
fix junit error/failure/skipped count
2022-02-07 19:20:29 +01:00
N. Engelhardt
53eb25fcae
handle unreached cover properties
2022-02-07 15:29:36 +01:00
N. Engelhardt
5abaccab69
refactor junit print into own function
2022-02-07 12:29:27 +01:00
N. Engelhardt
9168b0163b
handle status of cover properties
2022-02-06 09:15:44 +01:00
N. Engelhardt
d7e7f2c530
refactor model to have single base
2022-01-31 12:35:56 +01:00
N. Engelhardt
1cf27e7c31
parse solver location output for assert failures (cover not functional yet)
2022-01-27 13:41:07 +01:00
N. Engelhardt
a9d1972c47
add fallback if solver can't tell which property fails
2022-01-21 15:18:53 +01:00
N. Engelhardt
7f3c4137c1
create json export and read in properties
2022-01-19 19:34:11 +01:00
N. Engelhardt
6ec2df34e3
WIP change junit print to conform to schema; needs additional data, currently printing dummy info
...
Signed-off-by: N. Engelhardt <nak@yosyshq.com>
2022-01-13 13:45:54 +01:00
N. Engelhardt
cdf5650c12
add JUnit schema and validator
...
Signed-off-by: N. Engelhardt <nak@yosyshq.com>
2022-01-13 13:43:38 +01:00
Miodrag Milanović
02a5b71982
Merge pull request #138 from YosysHQ/mmicko/ci
...
Added CI
2022-01-12 14:24:51 +01:00
Miodrag Milanovic
ab5ff32b31
Added CI
2022-01-12 14:18:17 +01:00
Miodrag Milanović
f878a0e517
Merge pull request #136 from nakengelhardt/fix_pono
...
use --witness option when calling pono
2022-01-12 13:46:25 +01:00
N. Engelhardt
257a57d8ed
create only a single bad when using pono solver; workaround for #137
2022-01-12 13:18:54 +01:00
N. Engelhardt
ad07ea0e85
add testcase exposing #137
2022-01-12 11:06:05 +01:00
N. Engelhardt
5a04ac3fcc
use --witness option when calling pono
2022-01-12 10:55:08 +01:00
N. Engelhardt
f5a41e5ab1
Merge pull request #135 from nakengelhardt/rename_task
...
Rename SbyJob to SbyTask and SbyTask to SbyProc to reduce confusion
2022-01-12 10:52:42 +01:00
N. Engelhardt
63bf8457d7
Merge pull request #134 from nakengelhardt/advertise_suite_in_readme
...
mention tabby+oss cad suite in readme
2022-01-11 17:34:35 +01:00
N. Engelhardt
7c9e5b026b
Rename SbyJob to SbyTask and SbyTask to SbyProc to reduce confusion. Config file tasks now correspond to SbyTasks.
2022-01-11 17:08:56 +01:00
N. Engelhardt
9af6e220f9
mention tabby+oss cad suite in readme
2022-01-04 16:32:59 +01:00
Claire Xenia Wolf
ac9001b22c
Improvements and cleanups in tasks handling
...
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2021-12-18 11:36:34 +01:00
Claire Xenia Wolf
f1d3be3914
Fixed [tasks] section parsing
...
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2021-12-17 20:57:19 +01:00
Claire Xen
f7f5135508
Update README.md
2021-12-17 15:50:57 +01:00
Claire Xen
7f2c4189dc
Update README.md
2021-12-17 15:48:01 +01:00
Claire Xenia Wolf
4a07e026dd
Add inductive invariants example
...
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2021-12-17 15:42:04 +01:00
Claire Xenia Wolf
ab9d4fd3cf
Add ":"-syntax for [tasks] section
...
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2021-12-17 15:36:35 +01:00
Claire Xenia Wolf
b409b1179e
Update docs theme
...
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2021-11-30 10:47:43 +01:00
Claire Xenia Wolf
38562a5bb9
Update docs theme
...
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2021-11-29 16:51:54 +01:00
Claire Xenia Wolf
882d5b3a96
update docs theme
...
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2021-11-26 20:34:55 +01:00
Claire Xenia Wolf
5d19e4641a
Add support for directories in [files] section
...
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2021-10-31 14:43:02 +01:00
Claire Xenia Wolf
1b3832cf92
Fixed names and links
2021-10-31 14:42:39 +01:00
Miodrag Milanović
15278f1346
Merge pull request #127 from christian-krieg/feat/update-docs_super-prove
...
Updated install instructions for super_prove
2021-09-13 16:21:18 +02:00
Miodrag Milanovic
863a53b312
Fix regression
2021-08-25 12:10:18 +02:00
Miodrag Milanovic
156cc5d8c9
Initialize variable
2021-08-25 11:38:24 +02:00
Claire Xen
dd60141f0d
Merge pull request #126 from piegamesde/master
...
Various improvements and fixes
2021-08-23 16:03:03 +02:00
Christian Krieg
21371fb7ac
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
2021-07-20 22:33:28 +02:00
