KrystalDelusion
a76286ed34
Check output of fifo.sby
...
False positive exit 0 if fifo.sby was giving returncode=2.
2022-08-02 10:28:06 +12:00
KrystalDelusion
93d8ef9663
Fixed bigtest
...
Accidentally broke it in cc27d27
(this is why regular testing is important).
2022-08-02 10:12:33 +12:00
KrystalDelusion
b2d0368e26
Testing fifo things in CI
...
Turns out the bigtest golden ref is failing a_count_diff, need to fix that before removing the default statement.
Base example code is fine. New shell script to run default case and then nofullskip.
Expects returncode=2 after running nofullskip.
2022-08-01 22:06:03 +12:00
KrystalDelusion
ed9b291d2b
Remove redundancies in certain logic checks
...
A | A' === True, A | (A' & B) === A | B
2022-08-01 20:36:19 +12:00
KrystalDelusion
672a559b92
Merge branch 'YosysHQ:master' into fifo_example
2022-08-01 20:25:15 +12:00
Jannis Harder
9293e66092
example for autotune
2022-07-26 16:06:02 +02:00
KrystalDelusion
cc27d27c05
More literalincludes
...
Tidying up of newstart.rst and fifo.sv to include as much code as possible by reference.
Should reduce repetition and make it easier if changes occur in source.
2022-07-04 11:53:40 +12:00
KrystalDelusion
c9fbfa3684
Adding makefile for fifo
2022-07-04 10:32:55 +12:00
KrystalDelusion
a5f67ed904
Merge branch 'master' into fifo_example
2022-07-01 11:46:02 +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
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
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
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
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
KrystalDelusion
a808a0738c
Merge branch 'master' into fifo_example
...
Abbreviates additional btor instructions.
2022-06-07 12:00:10 +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
KrystalDelusion
f5257011f6
Specifying z3 to support minimum required install
2022-05-31 11:31:20 +12: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
7468e7655d
Alignment fixing
2022-05-10 11:03:40 +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
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
Claire Xenia Wolf
ac9001b22c
Improvements and cleanups in tasks handling
...
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2021-12-18 11:36:34 +01:00
Claire Xen
f7f5135508
Update README.md
2021-12-17 15:50:57 +01:00
Claire Xen
7f2c4189dc
Update README.md
2021-12-17 15:48:01 +01:00
Claire Xenia Wolf
4a07e026dd
Add inductive invariants example
...
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2021-12-17 15:42:04 +01:00
N. Engelhardt
f5f1d9936f
Make readme of abstraction example more tutorial-like
2021-04-16 15:54:51 +02:00
Claire Wolf
5a9efba584
Improvements in "make test"
...
Signed-off-by: Claire Wolf <claire@symbioticeda.com>
2020-07-24 14:58:23 +02:00
Claire Wolf
0d98201dc7
Add "Unexpected response" handling to smtbmc engine
...
Signed-off-by: Claire Wolf <claire@symbioticeda.com>
2020-07-20 19:42:10 +02:00
Claire Wolf
b26d4e6362
Update wolf_goat_cabbage.sv
...
Signed-off-by: Claire Wolf <claire@symbioticeda.com>
2020-04-22 19:21:15 +02:00
matt venn
68127a3706
consistent naming and put person moving line at the top
2020-04-22 19:11:23 +02:00
matt venn
94ce8e1288
Merge branch 'master' of https://github.com/YosysHQ/SymbiYosys
2020-04-22 17:54:53 +02:00
matt venn
9d69f8a518
change order of statements and make gender neutral
2020-04-22 17:54:39 +02:00
Claire Wolf
3ec2b6b4e4
Add djb2hash example
...
Signed-off-by: Claire Wolf <claire@symbioticeda.com>
2020-04-09 19:46:19 +02:00
Claire Wolf
a4885ce494
Get rid of verific warning in abstraction example
...
Signed-off-by: Claire Wolf <claire@symbioticeda.com>
2020-04-03 15:28:23 +02:00
Claire Wolf
d18656084c
Fix typo
...
Signed-off-by: Claire Wolf <claire@symbioticeda.com>
2020-04-03 15:18:52 +02:00
Claire Wolf
8a62780b9d
Fix primegen example
...
Signed-off-by: Claire Wolf <claire@symbioticeda.com>
2020-03-24 17:12:12 +01:00
Clifford Wolf
5ef5187673
Add docs/examples/abstract/.gitignore
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-06-18 10:31:55 +02:00
Clifford Wolf
59f4f29fdc
Fix quickstart demo to work with verific
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-06-18 10:30:04 +02:00
Clifford Wolf
79b1ac9570
Minor improvements in docs/examples/abstract/abstr.sv
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-03-27 14:49:35 +01:00
Clifford Wolf
afe6960ffe
Add docs/examples/abstract
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-03-27 14:45:30 +01:00