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
KrystalDelusion
66ef51d846
Verification properties in doc
2022-06-07 11:50:26 +12:00
KrystalDelusion
fef6d3a8a6
Adding USE_VERIFIC flag
...
Adding variations in .sby file where tabby uses verific and oss doesn't.
2022-06-07 11:49:25 +12:00
KrystalDelusion
aed5a33bef
Add init check
...
Prevent rst_n from going low once it has gone high.
2022-06-07 10:22:04 +12: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
KrystalDelusion
f5257011f6
Specifying z3 to support minimum required install
2022-05-31 11:31:20 +12:00
KrystalDelusion
b18f22cf43
Removing install details for optional engines
2022-05-31 11:18:05 +12: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
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
KrystalDelusion
fc9ff3d733
Initial FIFO description
2022-05-10 12:08:49 +12:00
KrystalDelusion
21dfd35516
Adding new Getting started guide
2022-05-10 11:41:15 +12:00
KrystalDelusion
7ec35dc425
Adding (small) intro to installation guide
...
Also a cross reference link.
2022-05-10 11:41:01 +12:00
KrystalDelusion
ee15ebd0f1
Title case for license.rst
2022-05-10 11:40:17 +12:00
KrystalDelusion
7468e7655d
Alignment fixing
2022-05-10 11:03:40 +12:00
KrystalDelusion
12b854b554
Headings for optional/required installs
2022-05-04 10:50:38 +12:00
KrystalDelusion
8f22733698
Revert change from yosyshq.net to yosyshq.com
2022-05-04 10:07:31 +12:00
KrystalDelusion
60de15293d
Now actually fills up properly
...
As opposed to only storing MAX-1
2022-05-02 12:34:57 +12:00
KrystalDelusion
48d846d529
Adjusting for use with OSS
...
i.e. doesn't use concurrent assertions
2022-05-02 12:20:27 +12:00
KrystalDelusion
f33c2eda52
Updating/rearranging links
2022-05-02 10:44:28 +12:00
KrystalDelusion
e8c5ae678d
Adding instructions for CAD
...
Currently taken verbatim from this repo's README.md
2022-05-02 10:31:51 +12:00
KrystalDelusion
e106d5c161
Adjusting assumptions
2022-04-27 09:36:44 +12:00
KrystalDelusion
ec02e25f5c
Split fifo.sv into two files
...
fifo.sv contains the components, top.sv for toplevel design.
2022-04-27 09:24:14 +12:00
KrystalDelusion
679df4d898
Fixing .gitignore to ignore just directories
2022-04-27 09:05:16 +12:00
KrystalDelusion
ee769996d0
Initial add of fifo example
...
Has tests which pass, committing before messing with it while tidying.
2022-04-27 09:02:16 +12: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
