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.
- 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.
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.
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`.
`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).
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).
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`.
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.
`--status` reports if the schema doesn't match.
`--statusreset` is able to perform a hard reset, dropping all the existing tables and calling `_setup()`.
Use context manager to handle commit/rollback.
Use `sqlite3.Connection.in_transaction` property instead of rolling our own.
Read-only methods don't need the transaction wrapper and we never read-update-write.
* to address #296
* this also required some changes to the formatting of the output from
smtbmc to allow more unambiguous parsing, so corresponds to a matching
change in yosys
This commit removes an erroneous "if sbyfile" that would turn '-f' into a no-op
for stdin input files. Presumably this check was originally intended to handle
the case of stdin input file and no specified workdir (which uses a temporary
workdir). In the current version the check is redundant for this particular
case. The check is erroneous in the case of stdin input file and a specified
workdir, so we simply remove the check.
ABC will sometimes return negative frame numbers when proving by convergence, e.g.
```
engine_0: Proved output 1 in frame -698905656 (converged).
engine_0: Proved output 4 in frame -698905656 (converged).
```
This change fixes these properties being missed and causing the engine status to return UNKNOWN due to `proved_count != len(proved)`.
This adds initial support for an sqlite database that is shared across
multiple tasks of a single SBY file and that can track the status of
individual properties.
The amount of information tracked in the database is currently quite
minimal and depends on the engine and options used. This can be
incrementally extended in the future.
The ways in which the information in the database can be queries is even
more limited for this initial version, consisting of a single '--status'
option which lists all properties and their status.
