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
Krystine Sherwin
b1d9bcbb42
tests: Add statusdb test
...
Ensures that `--statusreset` doesn't break the schema.
2025-07-08 15:44:02 +12:00
Krystine Sherwin
10040ce859
Test status db schema
...
`--status` reports if the schema doesn't match.
`--statusreset` is able to perform a hard reset, dropping all the existing tables and calling `_setup()`.
2025-07-08 15:44:01 +12:00
Krystine Sherwin
ad9382d46c
Re-disable db debug mode
2025-07-08 15:44:01 +12:00
Krystine Sherwin
f84e648391
Better transaction control
...
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.
2025-07-08 15:44:01 +12:00
Krystine Sherwin
03244c4f96
Use a cursor for PRAGMAs
2025-07-08 15:44:01 +12:00
KrystalDelusion
236f0ec59c
Revert "work around pypy bug"
...
This reverts commit b47d2829f9
2025-07-08 15:44:01 +12:00
N. Engelhardt
17b74bf3d6
Merge pull request #320 from jix/aigcexmin-bump
2025-07-07 10:38:42 +02:00
KrystalDelusion
bea2fe55a2
Merge pull request #330 from YosysHQ/krys/cover_no_assert
...
Remove asserts during cover mode
2025-07-07 20:34:57 +12:00
KrystalDelusion
562a504709
Docs fix
2025-07-07 20:07:25 +12:00
Krystine Sherwin
ef8ca40a5d
Don't fail cover props on failed assert
2025-07-05 12:53:54 +12:00
Krystine Sherwin
911ae02ee5
Test property statuses for cover_assert
...
Cover properties shouldn't be marked fail when the test failed early due to an assertion.
This should fail without other changes.
2025-07-05 12:40:57 +12:00
Krystine Sherwin
4d8462b58e
Add cover_assert option
2025-07-05 11:17:05 +12:00
Krystine Sherwin
aa7d8ab4ce
Reapply "Remove asserts during cover mode"
...
This reverts commit 205245c827
2025-07-02 18:00:28 +12:00
Krystine Sherwin
205245c827
Revert "Remove asserts during cover mode"
...
This reverts commit 81873292c9
2025-07-02 17:59:46 +12:00
Krystine Sherwin
81873292c9
Remove asserts during cover mode
2025-07-02 17:57:31 +12:00
Robin Ole Heinemann
b47d2829f9
work around pypy bug
...
ref: https://github.com/pypy/pypy/issues/3183
2025-05-14 14:54:06 +01:00
Miodrag Milanovic
ab2003d90f
Update location of demo files
2025-05-06 12:54:18 +02:00
Miodrag Milanović
6dcde33cc2
Merge pull request #322 from jix/test_external_examples
...
allow running SBY tests with an external examples directory
2025-05-06 12:49:16 +02:00
Jannis Harder
c8800ecd34
allow running SBY tests with an external examples directory
2025-04-28 16:13:30 +02:00
Miodrag Milanović
18ff267c02
Merge pull request #319 from YosysHQ/blackbox_tests
...
add new blackbox test cases
2025-04-15 10:32:14 +02:00
Jannis Harder
7ea6618237
Bump aigcexmin dependencies
2025-04-08 16:54:57 +02:00
Jannis Harder
1b36b27d90
Merge pull request #301 from jix/cexenum-updates
...
Update cexenum tool to latest version
2025-04-08 16:50:21 +02:00
Emily Schmidt
8423d3e2c8
add new blackbox test cases
2025-04-08 13:47:59 +01:00
George Rennie
ff98e51c13
Merge pull request #317 from SeddonShen/main
...
feat(sby_engine_aiger): add rIC3 support for BMC mode
2025-03-26 10:17:15 +01:00
SeddonShen
ca93e43cec
feat(sby_engine_aiger): add rIC3 support for BMC mode
2025-03-18 16:06:16 +08:00
George Rennie
20ee439df9
Merge pull request #313 from gipsyh/rIC3
...
Support rIC3 model checker as backend
2025-03-14 15:13:06 +01:00
Yuheng Su
fc0afb04c5
Set minimum rIC3 version to 1.35
2025-03-14 22:00:09 +08:00
N. Engelhardt
9675d158ce
Merge pull request #264 from YosysHQ/krys/vhd_example
...
Add formal_bind example
2025-03-03 15:20:59 +00:00
Miodrag Milanović
b6be8ad0fc
Merge pull request #311 from sporniket/patch-2
...
[docs] Fixes instructions for installing boolector
2025-03-03 16:15:59 +01:00
N. Engelhardt
44c44097f8
Merge pull request #310 from sporniket/patch-1
...
[docs] instruct to clone yosys with '--recurse-submodules'
2025-03-03 15:11:05 +00:00
N. Engelhardt
4d92762d5a
Merge pull request #278 from YosysHQ/krys/docs_verific
...
Add note on docs to clarify verific support
2025-03-03 15:09:36 +00:00
Yuheng Su
8da7174b16
update rIC3 backend
...
Signed-off-by: Yuheng Su <gipsyh.icu@gmail.com>
2024-12-17 04:41:58 +00:00
Yuheng Su
daf4e4cb39
Support rIC3 as backend
...
Signed-off-by: Yuheng Su <gipsyh.icu@gmail.com>
2024-12-16 11:02:45 +00:00
David SPORN
8885582e3c
[docs] Fixes instructions for installing boolector
...
There is a `build` folder where `bin\btorsim` is generated
2024-11-19 07:20:08 +01:00
David SPORN
7fc7ed38ae
[docs] instruct to clone yosys with '--recurse-submodules'
...
Without using '--recurse-submodule', make fails to retrieve them before building.
2024-11-19 06:58:01 +01:00
N. Engelhardt
26b387466d
Merge pull request #308 from YosysHQ/krys/drop_ilang
2024-11-07 17:33:53 +01:00
Krystine Sherwin
176e59c3d8
Replace (read_)ilang with (read_)rtlil
2024-11-05 12:55:09 +13:00
N. Engelhardt
daed0e1544
Merge pull request #302 from YosysHQ/fix_mangle_lookup
2024-10-17 11:15:01 +02:00
Miodrag Milanovic
94d1d0aa2f
enable extensions
2024-10-16 17:14:42 +02:00
N. Engelhardt
e84cc443bd
add non-verific name mangling regression test
2024-10-16 15:05:02 +02:00
N. Engelhardt
0f13fc6bc7
fix lookup of mangled path names
2024-10-16 13:56:36 +02:00
