- Add `btor2aig_yw.py` to wrap btor2aiger calls, splitting the symbol map into a
`.aim` file and building (and approximation of) the `.ywa` file.
- Currently not tracking asserts/assumes in the `.ywa`, and yosys-witness isn't
the biggest fan of the btor2aiger style of unitialised latches. As such, the
latches are declared but the `.yw` output doesn't do anything with them so
it's incomplete. But the vcd output seems fine (for `vcd_sim=on|off`).
- Add a try/except to catch property matching with an incomplete property list.
- Add `-x` flag to `write_btor` call since aiw2yw gets confused without them.
- Includes some TODO reminders for me to fix things, but as far as I can tell it
is working.
Add `btor_aig` option, which uses `model("btor_nomem")` and btor2aiger to generate an aiger file via btor.
Seems to run fine, until it tries to access design_aiger.ywa for trace conversion.
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.
When using the -f argument be more forgiving with the expectation of a clean
workspace and the expectation of the new sby run being responsible for
directory creation.
This is a usability and quality of life improvement for Windows users where
the OS can implement file and directory locking implicitly. In the EDA world
it is common to have multiple tools in use at any one time and it can become
tortious to have to close files / exit 3rd party applications to release
locking so sby is happy to rerun.
This change will prevent sby claiming a terminal error has occurred when it
fails to create a directory that already exists. It also now considers the
environment to be 'clean' (as per -f) if all the non-directory elements of
the file tree have been deleted, leaving potentially an empty a skeleton of
directories.
Only implements the POSIX jobserver and will break on windows.
Unbreaking it on windows will be done as a follow up.
Not used for autotune, that needs some more changes.
