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
Yuheng Su
6943469018
Fix rIC3 BMC command
2026-06-23 09:11:14 +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
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
inquisitour
a6a42216f5
itp engine: use task.opt_depth and task.opt_skip directly
2026-03-15 23:44:26 +00:00
inquisitour
01a716bf2e
itp engine: address review feedback - use constants
2026-03-14 20:33:17 +00:00
inquisitour
7225ad24f1
itp engine: address review feedback - simplify arg parsing, fix status logic, use exe_paths
2026-03-14 18:07:04 +00:00
inquisitour
39670d6611
Add ITP engine: interpolation-based model checking via itp-bmc
2026-02-28 07:11:08 +00:00
Jannis Harder
6d0a1ed960
Add cycle_width option for sim's new -width option
2025-10-20 17:30:09 +02:00
Krystine Sherwin
db782815f2
More tests without properties
...
Used `sby --autotune` to find other engines which fail (though there aren't any other exceptions that I could find).
Parse errors from `abc bmc3` and `abc sim3` instead of returning UNKNOWN.
2025-09-30 10:32:49 +13:00
Krystine Sherwin
c06d8682cd
Fix abc crash when aiger_props is empty
...
Includes test reproducer from #338 , modified to also test `abc --keep-going pdr`.
2025-09-30 10:26:36 +13:00
KrystalDelusion
5fc7b93627
Merge branch 'main' into krys/fix_status_trace
2025-08-05 12:55:12 +12:00
Krystine Sherwin
5fffe7eda6
Fix heredoc in sub dir
...
Also change log to use absolute path for consistency with the copy/link logs.
2025-08-02 10:40:52 +12:00
Krystine Sherwin
ac419190d2
Use more pathlib.Path
2025-08-02 10:06:30 +12:00
Krystine Sherwin
b06781e19e
Fix directory mismatch
2025-08-02 09:17:55 +12:00
Krystine Sherwin
d4864994ca
statusfmt: Skip null fields in jsonl output
2025-08-01 10:34:08 +12:00
Jannis Harder
190ef86916
statusfmt: Skip missing fields in jsonl output
2025-07-29 17:31:38 +02:00
Jannis Harder
344236af41
statusfmt: Make JSONL self-contained and escape CSV values
2025-07-29 17:10:57 +02:00
Krystine Sherwin
5992167909
Fix comparing int with None
2025-07-29 10:33:59 +12:00
Krystine Sherwin
9cb368b9c8
Re-order status evaluation
...
Always add the current row to the status map if there's a key error instead of trying to be clever with `.get()` and `None`s.
2025-07-29 10:26:51 +12:00
Krystine Sherwin
990d8db9a2
Prefer traces even without depth
2025-07-29 10:12:15 +12:00
Krystine Sherwin
f05979a528
Fix for statusfmt not going into status block
2025-07-29 10:04:40 +12:00
Krystine Sherwin
3bf5be0637
Add jsonl status format
...
Replace `--statuscsv` and `--livecsv` with `--statusfmt <fmt>` and `--live <fmt` respectively.
Currently supports both csv and jsonl.
In the case of `--live`, updates can be printed in multiple formats, while `--statusfmt` only supports one at a time.
2025-07-29 10:00:52 +12:00
Krystine Sherwin
1518168aa0
Remove debug print
2025-07-09 10:47:55 +12:00
Krystine Sherwin
a6496d646f
Cancel shouldn't use timeout logic
2025-07-09 10:28:50 +12:00
Krystine Sherwin
de51db08ab
Fix typo
2025-07-09 10:06:56 +12:00
Krystine Sherwin
cb81a97808
Add --taskstatus
...
Used for checking tasks in the status db.
Change `SBYStatusDB.all_tasks_status()` to use a `LEFT JOIN` to get a status of `UNKNOWN` for pending or aborted tasks (e.g. because they were ctrl+c'ed).
2025-07-09 10:06:56 +12:00
Krystine Sherwin
1f3b418018
Fix autotune
2025-07-09 10:04:58 +12:00
Krystine Sherwin
67212a20e5
Add --statuscancels option
...
The statusdb is only used to check for task completions if this option is used, requiring the user to explicitly request the feature.
2025-07-09 10:04:37 +12:00
Krystine Sherwin
5fc8df43f8
Intertask cancellation via database
...
Task checking via database rated limited to once every 10s.
Rename killer.sby to cancelledby.sby and add Makefile for testing.
2025-07-09 10:03:54 +12:00
Krystine Sherwin
e7c756a43f
Add cancelledby config section
2025-07-09 10:03:54 +12:00
Krystine Sherwin
a153349ac8
Initial intertask cancellation
...
Taskloops store tasks_done, tasks can be cancelled, and if a task named "killer" is in tasks_done then any other tasks are cancelled.
2025-07-09 10:03:54 +12:00
KrystalDelusion
1130847901
Merge branch 'main' into krys/symlink
2025-07-09 10:01:30 +12:00
Krystine Sherwin
a251ec0524
Handle unreliable lock files
2025-07-09 09:59:23 +12:00
Krystine Sherwin
baf118c838
Try to remove database on -f
...
If the database is open (based on the presence of certain files), skip deletion.
There is a (very) small window where another process *could* try to open the database at the same time that it's being deleted, but it will then fail during the database setup with `sqlite3.OperationalError: disk I/O error`, but given the failure is immediate I think it's fine.
2025-07-09 09:59:22 +12: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
aa2d3ed025
Add and use --latest flag for statuses
...
Should fix CI problem of running tests twice and the verific and non verific
properties having different names when testing the statusdb.
2025-07-08 15:47:34 +12:00
Krystine Sherwin
f399acc22d
Update unknowns on timeout
2025-07-08 15:47:34 +12:00
Krystine Sherwin
ceaeac43f7
Use tasknames in --statuscsv
...
Also fix fallbacks for property statuses without a `task_property_status` entry.
2025-07-08 15:47:34 +12:00
Krystine Sherwin
2aa8d266ad
Update unknown covers as well as asserts
...
Currently only applicable to smtbmc.
Also don't update assert depth during `cover` mode.
2025-07-08 15:47:33 +12:00
Krystine Sherwin
488d25b625
Don't use induction step for depth
2025-07-08 15:47:33 +12:00
Krystine Sherwin
4fc23bebec
Fix prop.tracefiles
2025-07-08 15:47:33 +12:00
