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
Jacob Lifshay
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
Jannis Harder
d0da57f54f
Test that cvc4 and cvc5 can be used
2022-06-08 13:33:12 +02:00
Jannis Harder
675dc03dfe
tests: Remove unused tool list in test Makefile
...
The checks for available tools moved to a python script, so need need to
have a copy of the tool list in the Makefile.
2022-06-08 11:32:35 +02:00
Jannis Harder
534ac21742
Merge pull request #169 from jix/yices-forall
...
Test designs using $allconst
2022-06-08 09:43:47 +02:00
Jannis Harder
34d6adf098
tests: Move required tool checks from rule generation to execution
...
This avoids regenerating the test makefile rules when the set of
installed tools changes and is a bit simpler overall.
2022-06-07 14:29:25 +02:00
Jannis Harder
80eacf34ca
Don't fail tests when xmlschema is missing
2022-06-03 17:22:45 +02:00
Jannis Harder
b4c110815c
Test designs using $allconst
2022-06-03 16:55:06 +02:00
Jannis Harder
d398a3c2df
tests: Fail on CI when any required tool is missing
2022-06-02 16:38:21 +02:00
Jannis Harder
00efdecb4b
tests: Check for btorsim --vcd
2022-06-02 16:38:21 +02:00
Jannis Harder
dc22d97362
Better checking of available solvers
...
Check for required auxiliary tools and always regenerate the make rules
when the set of available tools changes.
2022-05-30 15:02:26 +02:00
Jacob Lifshay
a87d21a802
add depth 1
2022-05-25 03:35:21 -07:00
Jacob Lifshay
3f32deb8c9
add test for yosys's $divfloor and $modfloor cells
...
Depends on: https://github.com/YosysHQ/yosys/pull/3335
2022-05-24 17:51:48 -07:00
Jannis Harder
8da6f07cb3
Refactor tests
...
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.
2022-04-11 17:50:38 +02:00
Jannis Harder
ef236eeddc
Regression test: do not merge FFs with unconstrained initvals
...
Currently done by `opt -keepdc` via `opt_merge` but not valid in a
formal context.
2022-04-01 19:25:09 +02:00
Jannis Harder
b725bfed0c
Prefer the first tracefile for each failing assertion
2022-03-30 13:47:14 +02:00
N. Engelhardt
2e0087fd2f
Merge pull request #150 from nakengelhardt/fix_junit_type_assignment
...
note unexpected return statuses in junit
2022-03-30 12:53:48 +02:00
Jacob Lifshay