mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-04-07 22:55:18 +00:00
Code Activity
575 commits 7 branches 26 tags 1.3 MiB
Commit graph

575 commits

This branch
This branch
All branches
Author SHA1 Message Date
KrystalDelusion a5f67ed904 Merge branch 'master' into fifo_example 2022-07-01 11:46:02 +12:00
KrystalDelusion de5b9b7821 Changed phrasing to avoid confusion on witnesses 2022-07-01 11:29:33 +12:00
KrystalDelusion aab2c3c2e0 New exercise section 
Worked exercise using the MAX_DATA parameter, highlighting its
incompleteness.  Includes completed examples in /golden subdirectory.

Also some formatting changes for spacing and extra links.
 2022-07-01 11:19:01 +12:00
KrystalDelusion 7ba67ef260 Removing unnecessary underflow assertions 2022-07-01 11:15:47 +12:00
Jannis Harder 4d858a1b9c
Merge pull request #189 from jix/autotune_docs 
docs: add missing autotune.rst
 2022-06-30 17:53:22 +02:00
Jannis Harder 685457915a docs: add missing autotune.rst 2022-06-30 17:50:05 +02:00
KrystalDelusion 907db48ac9 Updating from feedback 
Primarily addressing Nak's comments on the PR first.
Of note is the change from separate files to a single file.
Changed to boolector engine and bmc by default.
Updated install instructions to move z3 to optional and boolector to
recommended.
Literal code includes use :lines: option.
 2022-06-30 12:06:12 +12:00
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
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 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
KrystalDelusion 069197aeaa Add section on sby to newstart 
List tasks and run through failing noskip example.
Includes pictures (both fail and pass) plus .gtkw file for setting up.
 2022-06-09 14:29:21 +12:00
KrystalDelusion 41e427640a Adding noskip task 
Demonstrate failing model check by disabling rskip and wskip.
 2022-06-09 14:26:17 +12: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
KrystalDelusion a808a0738c Merge branch 'master' into fifo_example 
Abbreviates additional btor instructions.
 2022-06-07 12:00:10 +12:00