mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-10-30 20:42:30 +00:00
Code Activity
379 commits 9 branches 33 tags 2.7 MiB
Commit graph

379 commits

This branch
This branch
All branches
Author SHA1 Message Date
Jannis Harder
0df73ea666
Merge pull request #180 from jix/sby-fewer-asserts 
Don't use python asserts to handle unexpected solver output
 2022-06-15 14:08:15 +02:00
Jannis Harder
d0c59a3155 Don't use python asserts to handle unexpected solver output 2022-06-15 13:25:21 +02:00
Jannis Harder
e99884e319 SbyProc: New error_callback instead of exit_callback for failing procs 2022-06-15 13:25:21 +02:00
Jannis Harder
f131fe5b8f
Merge pull request #179 from jix/btor-option-handling 
btor pono: improve option handling
 2022-06-15 13:24:36 +02:00
Jannis Harder
141ffd34a5 btor pono: improve option handling 
Fail on the unsupported skip option and pass solver args to pono.
 2022-06-15 11:35:22 +02:00
Jannis Harder
98b0713597
Merge pull request #178 from jix/aiger-aigbmc-fixes 
aiger: check supported modes and aigbmc fixes
 2022-06-14 17:52:33 +02:00
Jannis Harder
05d963b0df aiger: check supported modes and aigbmc fixes 2022-06-14 17:41:06 +02:00
Jannis Harder
1e1402474a
Merge pull request #177 from mattvenn/tristate-example 
Tristate example
 2022-06-14 15:54:09 +02:00
Matt Venn
b88d7a13fb add makefile for test 2022-06-14 15:35:22 +02:00
Matt Venn
687ee0f011 remove unused module port 2022-06-14 15:31:42 +02:00
Matt Venn
7efabe828a expect fail 2022-06-14 15:31:42 +02:00
Matt Venn
b42b6445b8 tristate example 2022-06-14 15:31:42 +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
c50bd781ab
Merge pull request #175 from jix/more-test-improvements 
Use the test Makefile for all examples
 2022-06-13 13:59:31 +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
1d21513a47
Merge pull request #173 from jix/test-cvc 
Test that cvc4 and cvc5 can be used
 2022-06-10 15:24:49 +02:00
Jannis Harder
d7686ca698
Merge pull request #164 from jix/suggest_f_flag 
Suggest -f when the workdir already exists
 2022-06-10 15:14:01 +02:00
Jannis Harder
d0da57f54f Test that cvc4 and cvc5 can be used 2022-06-08 13:33:12 +02:00
Jannis Harder
4a9511b80b
Merge pull request #171 from jix/make-remove-unused-tool-list 
tests: Remove unused tool list in test Makefile
 2022-06-08 11:43:43 +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
2b1a588589
Merge pull request #163 from jix/make_improvements 
Test makefile improvements
 2022-06-07 14:50:59 +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
N. Engelhardt
41cd8e5b5e update install instructions for btorsim 2022-06-01 16:51:28 +02:00
Jannis Harder
8e87b0f7f4 Suggest -f when the workdir already exists 2022-05-30 16:18:37 +02:00
Jannis Harder
206562e5de Check for the tabby/oss cad suite before running make ci checks 2022-05-30 15:52:30 +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
Jannis Harder
939e000036 Makefile: Rename run_tests to test, update help, use .PHONY 2022-05-30 15:02:26 +02:00
Jannis Harder
de00dc71db
Merge pull request #161 from programmerjake/add-div-mod-floor-tests 
add test for yosys's $divfloor and $modfloor cells
 2022-05-26 12:00:05 +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
N. Engelhardt
ad2c33dd37 docs: add instructions for newer btorsim version required 2022-05-24 11:39:10 +02:00
Jannis Harder
d10e472edf
Merge pull request #159 from jix/fix-dpmem-example 
examples: Fix use of SVA value change expressions
 2022-05-11 11:23:57 +02:00
Jannis Harder
fedfae0e9c examples: Fix use of SVA value change expressions 
The $stable value change expression cannot be true for a non-x signal in
the initial state. This is now correctly handled by the verific import,
so the dpmem example needs to start assuming `$stable` only after
leaving the initial state.
 2022-05-11 10:38:54 +02:00
Jannis Harder
832888f0f0
Merge pull request #156 from jix/refactor-tests 
Refactor tests
 2022-04-25 11:21:21 +02: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
6daa434d85 Add --dumptaskinfo option to output some .sby metadata as json 2022-04-11 17:44:10 +02:00
Jannis Harder
a190994098 Add envvar to enable automatic .gitignore creation for workdirs 2022-04-11 17:44:10 +02:00
Miodrag Milanović
1e1aea0b1e
Merge pull request #140 from nakengelhardt/junit_jny 
junit: use write_jny instead of write_json
 2022-04-08 15:26:48 +02:00
N. Engelhardt
8ce526c22d junit: use write_jny instead of write_json 2022-04-06 18:35:01 +02:00
Miodrag Milanović
4886ed7e19
Merge pull request #155 from jix/invalid_ff_dcinit_merge 
Regression test: do not merge FFs with unconstrained initvals
 2022-04-03 12:15:58 +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
25e982c238
Merge pull request #154 from jix/sby_design-fixes 
sby_design fixes
 2022-03-31 16:35:40 +02:00
Jannis Harder
4b512668b2 Fix design_hierarchy handling of $paramod cells 2022-03-31 15:51:58 +02:00
Jannis Harder
a78eaa57db Fix variable name in find_property_by_cellname's error path 2022-03-31 13:12:15 +02:00