search

YosysHQ / sby

SymbiYosys (sby) -- Front-end for Yosys-based formal verification flows
Other
379 stars 74 forks source link

Initial support for a multi-task property status database #262

Closed jix closed 4 months ago

jix commented 4 months ago

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.

jix commented 4 months ago

It seems Jenkins is running the tests with an older sqlite version than the one we currently ship, causing it to fail with an SQL syntax error due to the older version not having support for a feature I am using (cc @mmicko). I can reproduce that locally if I use an older release, but not with the latest tabby release.

KrystalDelusion commented 4 months ago

I am getting the same error using tabby-linux-x64-latest.tgz from the 5th of Feb (so I guess the 20240118 build?). Are you using the experimental build with Python3.11 @jix ?

mmicko commented 4 months ago

@jix CI machine is Ubuntu 20.04 based, so sqlite is bit older. Since it works with oss-cad-suite it should also work with latest tabbycad ( so maybe @KrystalDelusion is using older one). Maybe it is better to update according to change suggestion from @KrystalDelusion. We need to update CI machine, but it is risky.