Krystine Sherwin
73c5e5cae6
timeout.sby: Add non-timeout equivalents
...
Number of properties reported should be consistent whether the task times out or finishes.
Currently fails `btor_fin_cover`.
2025-07-08 17:10:01 +12:00
Krystine Sherwin
83723696c7
Update failing test
...
Each property can have more than one status, but we only need to test the last one.
Also fix the warning about `\c` being an invalid escape.
2025-07-08 16:04:45 +12:00
Krystine Sherwin
aa2d3ed025
Add and use --latest flag for statuses
...
Should fix CI problem of running tests twice and the verific and non verific
properties having different names when testing the statusdb.
2025-07-08 15:47:34 +12:00
Krystine Sherwin
4adf5e5259
timeout.sby: Increase depth
...
CI was too fast
2025-07-08 15:47:34 +12:00
Krystine Sherwin
41bd894eff
Test property statuses after timeout
2025-07-08 15:47:34 +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
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
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
Emily Schmidt
8423d3e2c8
add new blackbox test cases
2025-04-08 13:47:59 +01: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
Emily Schmidt
725038d315
Replace the 'primes' test in junit_timeout_error.sby with a new test that solves a**3 + b**3 == c**3.
...
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.
2024-04-02 11:28:54 +01:00
Jannis Harder
6ba762db4c
Support for "abc --keep-going pdr" via new "pdr -X" mode
2024-02-20 14:06:43 +01:00
Jannis Harder
52184e5bf0
Initial support for a multi-task property status database
...
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.
2024-02-20 13:34:58 +01:00
Jannis Harder
6f0f2645c2
tests: Support testing an installed SBY using the SBY_CMD make variable
2024-01-19 14:51:16 +01:00
Jannis Harder
6d3b5aa960
Unified trace generation using yosys's sim across all engines
...
Currently opt-in using the `fst` or `vcd_sim` options.
2023-01-10 18:42:26 +01:00
Jannis Harder
90616c280b
tests: Do not run the same SBY task multiple times in parallel
2022-10-20 14:18:51 +02:00
Jannis Harder
83a1aa23c8
Merge pull request #218 from jix/fix_engine_list
...
Fix engine_list's return value
2022-09-15 17:59:25 +02:00
Jannis Harder
a0e3dd3d9a
Fix engine_list's return value
...
This fixes #216
2022-09-15 15:47:27 +02:00
Jannis Harder
168d667b6d
Add vcd option to make VCD writing optional
2022-09-05 15:42:24 +02:00
Jannis Harder
586be8ba96
tests: Fix test_rules.py after sby config parser changes
2022-09-03 00:03:28 +02:00
Jannis Harder
bd88454d7d
Merge pull request #196 from jix/parallel_jobserver
...
Run tasks in parallel and integrate with the make jobserver
2022-08-19 14:21:53 +02:00
Jannis Harder
353fac4db3
Merge pull request #211 from jix/skip_tests
...
tests: Ignore .sby files starting with skip_
2022-08-19 14:21:23 +02:00
Jannis Harder
b0786aea43
Make jobserver integration
...
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.
2022-08-18 14:40:00 +02:00
Jannis Harder
ea84c67f95
tests: Ignore .sby files starting with skip_
2022-08-18 14:07:13 +02:00
Aki Van Ness
841e0cb797
sby: core: Added unsupported messages to the new sections
2022-08-18 05:36:11 -04:00
Aki Van Ness
da56a3c6d1
docs: started working on a rough draft of the docs for the new sections and changes to existing sections
2022-08-18 05:36:11 -04:00
Aki Van Ness
987e439967
tests: parser: added the stages option to the options test file
2022-08-18 05:36:10 -04:00
Aki Van Ness
4abd8a7d69
tests: parser: updated the parser tests that caused a failure due to the lack of engines section
2022-08-18 05:36:10 -04:00
Aki Van Ness
a0d366e58a
some cleanup, added some rough parser tests, and started altering the engines section
2022-08-18 05:36:09 -04:00
Jannis Harder
5265a52b65
Refactor flow to use a common prep model
...
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.
2022-08-05 16:31:15 +02:00
Jannis Harder
523b7a252e
Regression test for YosysHQ/yosys#3433
2022-08-03 16:08:19 +02:00
N. Engelhardt
1cf206fc1c
add cvc5 executable to required tool mapping
2022-07-25 17:01:17 +02:00
N. Engelhardt
3ff2c9affc
avoid erroring out when coarse-grain logic loops can be resolved by mapping to fine grain operators
2022-07-25 16:22:32 +02:00
Jannis Harder
ea7fc7dc2c
tests: Windows fixes
...
Make tests runnable on Windows, as long as a unix like environment as
e.g. provided by MSYS2 is available.
2022-07-05 15:34:27 +02:00
Jannis Harder
ff802086b4
test uninited FFs with const clks and fix btor script for this
2022-07-04 14:03:56 +02:00
Jannis Harder
e01ac8b848
tests: Test for invalid x-value FF init optimizations
2022-07-04 13:33:39 +02:00
Jannis Harder
e3123283ea
Merge pull request #170 from programmerjake/add-simcheck-option
...
switch to using hierarchy -smtcheck for smtlib2 solvers, allowing smtlib2_module modules
2022-07-03 11:47:22 +02:00
Jannis Harder
48a02f9cc4
Test autotune
2022-06-27 15:58:42 +02:00
db740839b7
switch to using hierarchy -smtcheck for smtlib2 solvers, allowing smtlib2_module modules.
...
Fixes : #168
Depends on: https://github.com/YosysHQ/yosys/pull/3391
2022-06-22 21:17:29 -07:00
Jannis Harder
05d963b0df
aiger: check supported modes and aigbmc fixes
2022-06-14 17:41:06 +02:00
Jannis Harder
a200043709
Merge pull request #172 from jix/smtbmc-unroll-noincr-traces-fix
...
Regression test for smtbmc --unroll --noincr
2022-06-13 14:05:37 +02:00
Jannis Harder
499371fd39
Use the test Makefile for all examples
...
* 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
2022-06-13 13:42:58 +02:00
Jannis Harder
4ef02d2c5c
Regression test for smtbmc --unroll --noincr
2022-06-13 13:36:42 +02:00
