mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-04-07 22:55:18 +00:00
Code Activity
401 commits 7 branches 26 tags 1.3 MiB
Commit graph

213 commits

Author SHA1 Message Date
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