Jannis Harder
abe0086ec1
Merge pull request #158 from jix/autotune
...
Autotune: Automatic engine selection
2022-06-29 16:48:06 +02:00
Jannis Harder
d038a7d35c
autotune: Initial documentation
2022-06-27 15:58:42 +02:00
Jannis Harder
48a02f9cc4
Test autotune
2022-06-27 15:58:42 +02:00
Jannis Harder
b4458d43d7
Automatic engine selection
2022-06-27 15:58:42 +02:00
Jannis Harder
5014d74023
sby_design: Extract total memory size and forall usage
2022-06-24 13:50:26 +02:00
Jannis Harder
157bb156c0
Merge pull request #185 from georgerennie/prefix_empty_taskname
...
Use default prefix directory when no task is specified
2022-06-24 12:40:09 +02:00
Jannis Harder
0d90e29ef3
Merge pull request #183 from jix/engine-option-docs
...
Reflect recent engine updates in the reference docs
2022-06-23 16:39:32 +02:00
Jannis Harder
f66436ce48
Merge pull request #184 from jix/smtbmc-keepgoing-induction-trace-fix
...
smtbmc: Fix induction trace filename with --keep-going for the basecase
2022-06-23 13:37:38 +02:00
Jannis Harder
3dcf7766ea
smtbmc: Fix induction trace filename with --keep-going for the basecase
...
--keep-going only applies to the basecase and induction runs without that
option, so the trace filename for induction should have no placeholder.
2022-06-23 13:15:58 +02:00
Jannis Harder
d8ebd1eb9d
Reflect recent engine updates in the reference docs
2022-06-20 15:23:59 +02:00
George Rennie
0308142fa4
Use default prefix directory when no task is specified
2022-06-19 00:49:12 +01:00
Jannis Harder
fb5705b5bd
Merge pull request #182 from jix/taskloop
...
Decouple taskloop from task
2022-06-15 16:41:39 +02:00
Jannis Harder
0fe8c223cf
Decouple taskloop from task
2022-06-15 16:28:09 +02:00
Jannis Harder
c944a9c99c
Merge pull request #181 from jix/monotonic
...
Use monotonic clock for timeouts
2022-06-15 16:27:23 +02:00
Jannis Harder
d1c04f79d6
Use monotonic clock for timeouts
2022-06-15 14:11:25 +02:00
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
a87d21a802
add depth 1
2022-05-25 03:35:21 -07:00
