The old test tried to find two primes that are 7 apart. It is supposed to time
out after 1 second but on newer hardware the test completes too quickly. This
commit replaces it with a new test that tries to find a non-trivial solution to
the diophantine equation a**3 + b**3 == c**3, which is a lot more difficult.
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.
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.
The goal of this is to make sure that all backend flows are compatible
and we can map between them, so that e.g. the aiger model can be used to
minimize a counterexample trace produced by smtbmc. Reducing the parts
that differ per backend (including parts that receive different input
depending on the used backend) also makes testing more effective as the
common parts are easier to cover.
* Rename and move sbysrc/demo[123].sby to docs/examples/demos
* Make them use multiple tasks for multiple engines
* Scan docs/examples for sby files for make test
* `make ci` is now `NOSKIP` by default
* Skip scripts using `verific` w/o yosys verific support
* This does not fail even with NOSKIP set
Organize tests into subdirectories and use a new makefile that scans
.sby files and allows selecting tests by mode, engine, solver and/or
subdirectory. Automatically skips tests that use engines/solvers that
are not found in the PATH.
See `cd tests; make help` for a description of supported make targets.
This also changes the test Makefile to run `.check.py` files after
running the corresponding `.sby` file to allow more precise testing of
the keep going feature.
Jacob Lifshay