mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2026-07-14 07:15:42 +00:00
Code Activity
839 commits 16 branches 42 tags 1.8 MiB
Commit graph

44 commits

Author SHA1 Message Date
Gus Smith
69f2bb572a
Merge 2898c75fb0 into 8f8833c617 2026-07-09 19:20:19 +00:00
N. Engelhardt
97e47c471c fix incidental finding that return codes weren't being checked properly on witness conversion subprocesses 2026-07-06 18:54:23 +02:00
Miodrag Milanovic
29650804c1 catch subprocess crash as error 2026-06-23 12:21:28 +02:00
N. Engelhardt
e8bf66d4f0 small fixes + add regression tests for aiger and btor engines exercising all options 2026-06-23 09:11:14 +02:00
Yuheng Su
055a3b5d8b Update sbysrc/sby_engine_btor.py 
Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>
 2026-06-23 09:11:14 +02:00
Yuheng Su
87936dd03b Update rIC3 return codes to include UNKNOWN status 2026-06-23 09:11:14 +02:00
Yuheng Su
a8f3f4bba2 Update sbysrc/sby_engine_btor.py 
Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>
 2026-06-23 09:11:14 +02:00
Yuheng Su
a6069081c7 Enhance BTOR engine options with nomem and syn flags for improved model handling 2026-06-23 09:11:14 +02:00
Yuheng Su
222801e687 Support rIC3 engine for btor 2026-06-23 09:11:14 +02:00
Gus Smith
b4e66e3a33 Rename SymbiYosys to SBY 2026-02-24 09:03:49 -08:00
Krystine Sherwin
af511945a3
btor: Add unknown props 
First during the init, then again at the end.  Depth information isn't available, since there may be a pending trace job for that depth which would provide a known status.
 2025-07-08 17:26:55 +12:00
Krystine Sherwin
98ef1c4182
More status tracking unification 
- Status database only gets called from summary events instead of from engines.
- More trace witnesses (.aiw and .yw) are tracked as events.
- Multiple tracefiles can be included in the same trace summary, varying only by
  extension.  These are ordered by priority so that in the logfile only a single
  tracefile is listed.
- For engines where multiple properties can be collected for a single trace,
  these properties are now available for all traces until the next step.  If any
  properties are collected but never recorded with a trace, an error is raised.
- Fix formatting for events without steps (e.g. running abc with `vcd off`).
- Drop task_property_data table entirely, since it is now redundant and unused.
- Fix properties being skipped in all status dump if they don't have a trace.
 2025-07-08 15:47:33 +12:00
Krystine Sherwin
f0aca6c75e
Add traces to database 
Setting task property status accepts an optional trace id for associating a prop status with a trace.
Where relevant, delays adding prop status(es) to the database until the corresponding tracefile is known, similar to how tracefiles and prop statuses are linked during the summary.
 2025-07-08 15:47:33 +12:00
Krystine Sherwin
a332b017e4
More depth tracking 
`SbyTask::update_status()` optionally takes the current step/depth, which gets used for some solvers/engines when exiting to pass unknown properties.
btor engine tracks the current step, but it doesn't track/report which property triggered a CEX so it's only useful on exit.
Use data source as a fallback if engine isn't provided (such as when coming from the `task_status` instead of an engine update).
 2025-07-08 15:47:31 +12:00
Jannis Harder
6d3b5aa960 Unified trace generation using yosys's sim across all engines 
Currently opt-in using the `fst` or `vcd_sim` options.
 2023-01-10 18:42:26 +01:00
Claire Xenia Wolf
003ccf7197 Add color handling via click.style and click.echo 
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
 2022-10-31 20:29:32 +01:00
Jannis Harder
168d667b6d Add vcd option to make VCD writing optional 2022-09-05 15:42:24 +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
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
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
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
piegames
2d7d48885b Turn .format() strings into f-strings 2021-06-26 19:46:30 +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
Miodrag Milanovic
a62fded391 cosa2 -> pono rename 2020-07-03 11:25:55 +02:00
N. Engelhardt
ee5cfdef76 add --seed option to smtbmc and btor engines 2020-07-01 18:05:20 +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
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
N. Engelhardt
cb01f8469c fix return code check in btor engine 2020-04-29 16:09:18 +02:00
N. Engelhardt
1b8f3df8bd use info file for btorsim 2020-04-08 15:25:00 +02:00
N. Engelhardt
9aff36a3fe fix callback functions 2020-03-30 21:24:06 +02:00
N. Engelhardt
180e07f9c4 add btor cover mode; use btorsim for vcd generation 
Signed-off-by: N. Engelhardt <nak@symbioticeda.com>
 2020-03-30 21:24:06 +02:00
N. Engelhardt
30d7c32ec6 Use .format() instead of % 
Signed-off-by: N. Engelhardt <nak@symbioticeda.com>
 2020-03-25 13:09:37 +01:00
Clifford Wolf
0772456a15 Further improve BTOR cex handling 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-12-10 03:44:08 +01:00
Clifford Wolf
6878ba0a82 Improve BTOR cex handling 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-12-10 02:42:03 +01:00
Clifford Wolf
3d66e7cec5 Fixes and improvements in BTOR engine 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-12-08 07:16:19 +01:00
Clifford Wolf
150f30ae08 Working BTOR BMC engine 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-12-08 07:01:21 +01:00
Clifford Wolf
4c485766e2 Add btor engine 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-12-08 05:23:04 +01:00