mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-04-08 15:11:50 +00:00
Code Activity
562 commits 8 branches 26 tags 1.3 MiB
Commit graph

278 commits

Author SHA1 Message Date
Jannis Harder acaf6ef0c2 Use new memory_map -formal for aiger/_nomem 2022-08-05 16:31:15 +02:00
Jannis Harder 5265a52b65 Refactor flow to use a common prep model 
The goal of this is to make sure that all backend flows are compatible
and we can map between them, so that e.g. the aiger model can be used to
minimize a counterexample trace produced by smtbmc. Reducing the parts
that differ per backend (including parts that receive different input
depending on the used backend) also makes testing more effective as the
common parts are easier to cover.
 2022-08-05 16:31:15 +02:00
Jannis Harder edb068bff4 Fix print_junit_results failure during some error conditions 
There is a small window between setting self.precise_prop_status and
initializing self.design. I've only managed to produce an error within
that windows during development, but getting unrelated stacktraces from
print_junit_result failing distracts from debugging the issue at hand.
 2022-08-05 16:31:15 +02:00
Aki Van Ness 46ca20f8ec sby: core: ensured to strip the line of any uneeded whitespace 2022-08-04 06:13:28 -04:00
Aki Van Ness 9368f3f987 sby: core: explicitly split the the entries for the [options] section params to be at most one, 2022-08-04 06:13:28 -04:00
Aki Van Ness 10234fef00 sby: core: changed how the split for the section header and arguments are done, with a prior strip to remove and extra whitespace 2022-08-04 06:13:28 -04:00
Aki Van Ness 8133aaa8f8 sby: core: changed how the sections and their arguments are handled and cleared up the strangly worded error messages related to that 2022-08-04 06:13:28 -04:00
Aki Van Ness 59dc27ed73 sby: core: config: cleaned up the error messages to make them less opaque 2022-08-01 10:16:05 -04:00
N. Engelhardt 3ff2c9affc avoid erroring out when coarse-grain logic loops can be resolved by mapping to fine grain operators 2022-07-25 16:22:32 +02:00
Jannis Harder 07d19b202b
Merge pull request #195 from jix/sbyproc-truncated-output 
Fix a race-condition SbyProc that could truncate output
 2022-07-13 17:30:36 +02:00
Jannis Harder 5d3f784beb 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.
 2022-07-13 16:01:49 +02:00
Jannis Harder 92e7eb2e32 abc pdr: Enable log output by default 
This makes it consistent with the other abc solvers and shows whether
abc pdr is making progress.
 2022-07-08 12:36:44 +02:00
Jannis Harder de43a4c936
Merge pull request #191 from jix/early-readconfig 
Read config before creating a workdir
 2022-07-06 12:05:13 +02:00
Jannis Harder b3b315a473 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.
 2022-07-06 11:22:59 +02:00
Jannis Harder 566edad13c 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.
 2022-07-05 17:20:55 +02:00
Jannis Harder ff802086b4 test uninited FFs with const clks and fix btor script for this 2022-07-04 14:03:56 +02:00
Jannis Harder e3123283ea
Merge pull request #170 from programmerjake/add-simcheck-option 
switch to using hierarchy -smtcheck for smtlib2 solvers, allowing smtlib2_module modules
 2022-07-03 11:47:22 +02:00
Jannis Harder b4458d43d7 Automatic engine selection 2022-06-27 15:58:42 +02:00
Jannis Harder 5014d74023 sby_design: Extract total memory size and forall usage 2022-06-24 13:50:26 +02:00
Jannis Harder 157bb156c0
Merge pull request #185 from georgerennie/prefix_empty_taskname 
Use default prefix directory when no task is specified
 2022-06-24 12:40:09 +02:00
Jannis Harder 3dcf7766ea 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.
 2022-06-23 13:15:58 +02:00
Jacob Lifshay db740839b7 switch to using hierarchy -smtcheck for smtlib2 solvers, allowing smtlib2_module modules. 
Fixes: #168

Depends on: https://github.com/YosysHQ/yosys/pull/3391
 2022-06-22 21:17:29 -07:00
George Rennie 0308142fa4 Use default prefix directory when no task is specified 2022-06-19 00:49:12 +01:00
Jannis Harder 0fe8c223cf Decouple taskloop from task 2022-06-15 16:28:09 +02:00
Jannis Harder d1c04f79d6 Use monotonic clock for timeouts 2022-06-15 14:11:25 +02:00
Jannis Harder d0c59a3155 Don't use python asserts to handle unexpected solver output 2022-06-15 13:25:21 +02:00
Jannis Harder e99884e319 SbyProc: New error_callback instead of exit_callback for failing procs 2022-06-15 13:25:21 +02:00
Jannis Harder 141ffd34a5 btor pono: improve option handling 
Fail on the unsupported skip option and pass solver args to pono.
 2022-06-15 11:35:22 +02:00
Jannis Harder 05d963b0df aiger: check supported modes and aigbmc fixes 2022-06-14 17:41:06 +02:00
Jannis Harder 499371fd39 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
 2022-06-13 13:42:58 +02:00
Jannis Harder 8e87b0f7f4 Suggest -f when the workdir already exists 2022-05-30 16:18:37 +02:00
Jannis Harder 6daa434d85 Add --dumptaskinfo option to output some .sby metadata as json 2022-04-11 17:44:10 +02:00
Jannis Harder a190994098 Add envvar to enable automatic .gitignore creation for workdirs 2022-04-11 17:44:10 +02:00
N. Engelhardt 8ce526c22d junit: use write_jny instead of write_json 2022-04-06 18:35:01 +02:00
Jannis Harder 25e982c238
Merge pull request #154 from jix/sby_design-fixes 
sby_design fixes
 2022-03-31 16:35:40 +02:00
Jannis Harder 4b512668b2 Fix design_hierarchy handling of $paramod cells 2022-03-31 15:51:58 +02:00
Jannis Harder a78eaa57db Fix variable name in find_property_by_cellname's error path 2022-03-31 13:12:15 +02:00
Jannis Harder b725bfed0c Prefer the first tracefile for each failing assertion 2022-03-30 13:47:14 +02:00
N. Engelhardt 2e0087fd2f
Merge pull request #150 from nakengelhardt/fix_junit_type_assignment 
note unexpected return statuses in junit
 2022-03-30 12:53:48 +02:00
Jannis Harder 81e8b6737b
Merge pull request #147 from jix/smtbmc-keepgoing 
Support and tests for smtbmc `--keep-going`
 2022-03-30 11:42:48 +02:00
N. Engelhardt 008d020c4d note unexpected return statuses in junit 2022-03-29 19:10:29 +02:00
N. Engelhardt 53abf14514
Merge pull request #145 from nakengelhardt/fix_junit_tracefile 
junit: handle multiple asserts failing with the same trace
 2022-03-28 16:32:54 +02:00
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
N. Engelhardt 6a95ef33c8 fix trace summary printing 2020-05-13 18:15:33 +02:00
N. Engelhardt 842e9a121a call job.terminate at end of btor engine run to kill other engines in case of whoever-gets-there-first runs 2020-05-13 12:42:30 +02:00
N. Engelhardt b3d766bf89 start btorsim as soon as a witness is ready, print summary when multiple traces are produced 2020-05-12 16:48:58 +02:00
Claire Wolf ca9c188e3c Add silent mode to SbyTask 
Signed-off-by: Claire Wolf <claire@symbioticeda.com>
 2020-05-08 18:49:08 +02:00
N. Engelhardt cb01f8469c fix return code check in btor engine 2020-04-29 16:09:18 +02:00
N. Engelhardt 5d6323147d
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
 2020-04-29 11:47:20 +02:00
Claire Wolf 69ef444464 Add task pattern matching, closes #76 
Signed-off-by: Claire Wolf <claire@symbioticeda.com>
 2020-04-14 19:55:14 +02:00
Claire Wolf c91efe15a3 Add a status message when one or more tasks returned a non-zero return code, closes #78 
Signed-off-by: Claire Wolf <claire@symbioticeda.com>
 2020-04-14 19:54:24 +02:00