3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-10-08 18:51:57 +00:00
Commit graph

369 commits

Author SHA1 Message Date
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
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
1d233405bf
Warn on --livecsv in --status* block 2025-07-08 15:47:32 +12:00
Krystine Sherwin
48a5859a1e
Add kind to csv (and database) 2025-07-08 15:47:32 +12:00
Krystine Sherwin
4a14207b37
statuscsv: Better error handling 2025-07-08 15:47:32 +12:00
Krystine Sherwin
0fa5715909
Add --statuscsv
Prints summary of properties for each task, selecting only a single row for each unique status/property/task.  Prefers the earliest FAIL or the latest non-FAIL, using the same formatting as the `--livecsv`.
2025-07-08 15:47:32 +12:00
Krystine Sherwin
e2b1e85090
Add --livecsv
Gate csv dump on status updates.
Format 'csv' heading in yellow.
2025-07-08 15:47:32 +12:00
Krystine Sherwin
e9f4f06fe9
smtbmc updates db at each step
All properties marked UNKNOWN get dumped to the db for the previous step, each time the current step is updated.
2025-07-08 15:47:32 +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
Krystine Sherwin
0367db76f5
Initial live csv dumping
Currently unconditional, and only for aiger and smtbmc.
Uses task.name from intertask cancellation.
Stores `time.time()` when calling `SbyStatusDb::create_task()` in order to calculate time since start of task (consider reducing to integer seconds).
2025-07-08 15:47:31 +12:00
Krystine Sherwin
f63cd46d12
Store task name in task and statusdb 2025-07-08 15:47:31 +12:00
Krystine Sherwin
de59dcc9c4
statusdb: Safer setup
Always call `_setup()`, but use `CREATE TABLE IF NOT EXISTS`. The sql schema doesn't include this, so inject it during the setup instead of adding it to the `SQLSCRIPT`.
2025-07-08 15:44:02 +12:00
Krystine Sherwin
3493f2152f
statusdb: Retry backoff for PRAGMAs 2025-07-08 15:44:02 +12:00
Krystine Sherwin
bd0d615b2a
Fix raw string 2025-07-08 15:44:02 +12:00
Krystine Sherwin
233d5f1264
Actually use foreign key constraints 2025-07-08 15:44:02 +12:00
Krystine Sherwin
a64f29de6c
Add note to bad schema exception
Requires python >= 3.11 (oss-cad-suite is 3.11.6, but there isn't any minimum python version given for SBY that I can find).
Makes the error less opaque (even though it still has the trace), which I think is necessary given that using the status db is totally optional and otherwise using a different version of SBY with an extra db field in a directory where a previous version has run will just crash with an obscure sqlite3.OperationalError.
2025-07-08 15:44:02 +12:00