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
Krystine Sherwin
b3f2889b9e
CSV tidying
...
Use the same function for csv formatting during live and status reporting. Reads back the row for live reporting to get the full JOIN data.
Remove unused/unnecessary arguments for setting task property status.
Drop transaction wrapper from read-only db access.
2025-07-08 15:47:33 +12:00
