N. Engelhardt
3d8f56b89a
Merge pull request #142 from nakengelhardt/fix_backslash_smt2
...
translate backslashes in cell names the same way as smt2 backend does
2022-03-28 16:32:10 +02: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
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
257a57d8ed
create only a single bad when using pono solver; workaround for #137
2022-01-12 13:18:54 +01:00
N. Engelhardt
5a04ac3fcc
use --witness option when calling pono
2022-01-12 10:55:08 +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
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 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
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 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
piegames
bb19bca77c
fixup! Allow to set a working directory even when having multiple tasks
2021-07-12 16:14:48 +02:00
piegames
874d13ff89
Better error message when tasks failed
2021-06-26 19:46:30 +02:00
piegames
2d7d48885b
Turn .format() strings into f-strings
2021-06-26 19:46:30 +02:00
piegames
1f6700f21d
Allow to set a working directory even when having multiple tasks
...
Fixes #125 .
2021-06-21 22:32:29 +02:00
piegames
99aca04638
Print paths as absolute
...
This generally makes debugging path issues easier.
2021-06-21 22:31:53 +02:00
Miodrag Milanovic
ecf7b8f1b0
Windows specific fixes
2021-03-22 16:48:33 +01:00
Miodrag Milanovic
605db98382
Fix syntax errors
2021-01-26 09:09:43 +01:00
whitequark
287e33a47f
Add a PROGRAM_PREFIX= Makefile option for packages with prefixed Yosys.
2020-08-22 14:45:47 +00:00
Marcelina Kościelnicka
b172357161
Run dffunmap before writing the design with aiger/btor/smt2 backends.
2020-07-31 16:37:25 +02:00
N. Engelhardt
8c5b65cf97
add tests directory with additional tests
2020-07-24 13:51:39 +02:00
N. Engelhardt
7bae1b8bba
fix error message formatting
2020-07-21 14:48:38 +02:00
Claire Wolf
494f84b0ab
Include verilog source files for demo1.sby
...
Signed-off-by: Claire Wolf <claire@symbioticeda.com>
2020-07-21 13:01:36 +02:00
Claire Wolf
0d98201dc7
Add "Unexpected response" handling to smtbmc engine
...
Signed-off-by: Claire Wolf <claire@symbioticeda.com>
2020-07-20 19:42:10 +02:00
whitequark
db0e5f3637
Inject executable dependencies from the environment
2020-07-05 10:20:35 +00:00
Miodrag Milanovic
a62fded391
cosa2 -> pono rename
2020-07-03 11:25:55 +02:00
clairexen
72e84cb320
Merge pull request #97 from nakengelhardt/seed_arg
...
add --seed option to smtbmc and btor engines
2020-07-01 19:20:06 +02:00
clairexen
18ce85eb02
Merge pull request #94 from nakengelhardt/fix_93
...
ignore race condition in killing already-terminated process
2020-07-01 19:19:08 +02:00
N. Engelhardt
ee5cfdef76
add --seed option to smtbmc and btor engines
2020-07-01 18:05:20 +02:00
Claire Wolf
655d9c6bcd
Be more conservative in btor ys script
...
Signed-off-by: Claire Wolf <claire@symbioticeda.com>
2020-06-23 14:32:59 +02:00
N. Engelhardt
25502e16ef
ignore race condition in killing already-terminated process
2020-06-16 12:41:26 +02:00
Claire Wolf
c7668de077
Add support for cosa2 BTOR solver
...
Signed-off-by: Claire Wolf <claire@symbioticeda.com>
2020-05-18 16:59:36 +02:00
N. Engelhardt
9fdece3dab
btor engine: handle models with 0 properties
2020-05-18 13:11:25 +02:00
N. Engelhardt
87eb47502d
Merge pull request #87 from nakengelhardt/cover_trace_summary
...
Trace generation improvements
2020-05-13 18:45:39 +02:00
