Krystine Sherwin
0bfda86687
tests: Support .skip file
...
SBY entires in a file named `.skip` are ignored from the current directory during collection.
Useful for when you want to skip a file, but don't want to use the `skip_` prefix, such as when it's a docs example.
2026-07-16 11:45:17 +12:00
Krystine Sherwin
62cd0028a0
tests: Don't collect folders that start with skip_
2026-07-16 11:45:17 +12:00
Krystine Sherwin
6a71a74ed8
tests: Add clean_rules target
...
Calling `make clean` can fail if a test folder has been collected but the source no longer exists. `make clean_rules` bypasses this by skipping the `include make/rules/collect.mk` in the same way as `make help`.
2026-07-16 11:45:17 +12:00
Krystine Sherwin
948a2caacb
Docs: regex tag matching
...
This feels cursed.
2026-07-16 11:45:16 +12:00
Krystine Sherwin
a31f3706ec
Docs: Add default tasks and alt tag assignment
...
Demonstrate `--dumpcfg` sans task in the complex code example (and how the empty task impacts tag matching).
2026-07-16 11:45:16 +12:00
Krystine Sherwin
6f212c47a4
Docs: Multi-line tag sections
2026-07-16 11:45:16 +12:00
Krystine Sherwin
2e74292d2a
Docs: Advanced tag use
...
Add complex pycode example, generating tasks and then parsing tags to select source files. Warn against doing it, and reiterate the usefulness of `--dumptasks` and `--dumpcfg`.
Modify gen.sh for modifiable script/task and to echo how it was called (in case they need to be regenerated, which isn't a problem for the regular example/task1 but is for the complex one).
2026-07-16 11:45:15 +12:00
Krystine Sherwin
c411a397de
Docs: Clarify tasks section
...
Move simple tasks example into an actual `.sby` file and use `literalinclude`.
Add `gen.sh` script for generating output log (currently using checked in log file so that we don't need to deal with having sby installed for readthedocs).
Remove more complex examples.
Remove "group aliases" in favor of "tags".
Refer to `<tag>:` instead of `<taskname>:`.
Introduce `--dumptags` and tasks being assigned a tag of the same name.
Split out tags into subsection.
Move "run specific task" example call in line, and add a task (so that it shows two tasks in one)
2026-07-16 11:45:15 +12:00
Krystine Sherwin
56268b128b
Dump active tags if a single task is given
2026-07-16 11:45:15 +12:00
Krystine Sherwin
6eb1ed39d3
Docs: Fixing double backticks
2026-07-16 11:45:14 +12:00
KrystalDelusion
fea6e467d0
Merge pull request #360 from YosysHQ/gus/multi-stage-verif-docs
...
Integrate multi-stage verification docs
2026-07-16 11:44:43 +12:00
Gus Smith
7702dd4423
Integrate multi-stage verification docs
2026-07-16 10:58:13 +12:00
KrystalDelusion
1d59cdb9c4
Merge pull request #369 from shivamtiwari020505/docs-mode-prep-task-tags
...
docs: document prep mode and skip_prep
2026-07-16 10:55:05 +12:00
shivamtiwari020505
4b4332556b
docs: document prep mode and skip_prep
2026-07-15 13:45:37 +05:30
Miodrag Milanović
8f8833c617
Merge pull request #368 from YosysHQ/cleanup
...
Move test to proper place and remove empty dir
2026-07-08 10:04:15 +02:00
Miodrag Milanovic
a1a0634b2f
Update actions
2026-07-08 09:56:51 +02:00
Miodrag Milanovic
985d7bdd3d
Move test to proper place and remove empty dir
2026-07-08 09:41:11 +02:00
Miodrag Milanović
6e3dc04d92
Merge pull request #367 from YosysHQ/ric3
...
Support rIC3 solver with btor engine
2026-07-07 17:40:35 +02:00
N. Engelhardt
39d17d1a2b
be more precise on supported rIC3 version
2026-07-07 17:33:17 +02:00
N. Engelhardt
b2b067757e
don't call yosys-witness on (unsupported) justice witnesses
2026-07-07 12:50:02 +02:00
N. Engelhardt
d11cc34cb3
fix aiger witness handling for combinational designs (empty newlines are semantically important for aiw output parsed from log)
2026-07-06 19:58:52 +02: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
N. Engelhardt
ca8d332ccb
make engine/solver reference more consistent
2026-07-06 18:09:43 +02:00
Miodrag Milanovic
29650804c1
catch subprocess crash as error
2026-06-23 12:21:28 +02:00
Miodrag Milanovic
c4ed754ff8
Fix documentation
2026-06-23 10:51:21 +02:00
Miodrag Milanovic
ff48d2b9fd
Fix aiger_options test
2026-06-23 10:11:10 +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
d17e524a1b
Update docs/source/reference.rst
...
Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>
2026-06-23 09:11:14 +02:00
Yuheng Su
5b48417823
Update docs/source/reference.rst
...
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
e57071a376
Add support for BTOR rIC3 engine in documentation
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
Yuheng Su
6943469018
Fix rIC3 BMC command
2026-06-23 09:11:14 +02:00
Miodrag Milanović
d3e72d26e8
Merge pull request #366 from YosysHQ/regression_5892
...
add regression test for memory name escaping in smt2 comments
2026-06-16 10:54:11 +02:00
N. Engelhardt
93d387d419
add regression test for memory name escaping in smt2 comments
2026-06-09 17:39:36 +02:00
Miodrag Milanović
0cb15210a8
Merge pull request #365 from YosysHQ/ci_cmake
...
Update CI to build with CMake
2026-06-03 13:59:31 +02:00
Miodrag Milanovic
ea52d88750
Update CI to build with CMake
2026-06-03 13:46:53 +02:00
Miodrag Milanović
f57802a166
Merge pull request #362 from UnknownDK/backportprint
...
fix: print Path as string
2026-04-24 07:41:17 +02:00
Bjørn Grevenkop-Castenskiold
b90de3c36d
fix: print Path as string
2026-04-14 13:34:43 +02:00
Gus Smith
6424d15aae
Merge pull request #358 from anzzyspeaksgit/fix/issue-356
...
fix: make SBY config parsing error messages less ambiguous
2026-03-30 12:31:42 -04:00
Gus Smith
ae9d4458ca
Merge pull request #353 from inquisitour/add-itp-engine
...
Add ITP engine: interpolation-based model checking via itp-bmc
2026-03-30 12:29:24 -04:00
Miodrag Milanović
ab5bf1c10b
Merge pull request #359 from YosysHQ/aigmap
...
use aigmap instead of abc for AIG mapping
2026-03-24 12:57:09 +01:00
Lofty
6d855c1090
use aigmap instead of abc for AIG mapping
2026-03-23 11:40:18 +01:00
anzzyspeaksgit
8e37ec13bf
fix: make SBY config parsing error messages less ambiguous
...
Closes #356
2026-03-23 02:02:53 +00:00
Miodrag Milanović
268502844e
Merge pull request #357 from YosysHQ/upgrade_ci
...
Upgrade CI actions
2026-03-19 17:50:33 +01:00
Miodrag Milanovic
3aadbc4f95
Upgrade CI actions
2026-03-19 11:17:23 +01:00
inquisitour
a6a42216f5
itp engine: use task.opt_depth and task.opt_skip directly
2026-03-15 23:44:26 +00:00
