Jannis Harder
4ec278e6ec
Autotune example in docs
2022-07-26 16:35:57 +02:00
Jannis Harder
9293e66092
example for autotune
2022-07-26 16:06:02 +02:00
KrystalDelusion
ca3429e328
Autotune grammar/spelling check
2022-07-11 21:21:31 +12:00
matt venn
4ab610ce87
Update autotune.rst
2022-07-11 11:10:45 +02:00
Jannis Harder
bc2bb5c863
docs: Don't use linebreaks within inline code spans.
2022-07-08 14:31:57 +02:00
Jannis Harder
685457915a
docs: add missing autotune.rst
2022-06-30 17:50:05 +02:00
Jannis Harder
d038a7d35c
autotune: Initial documentation
2022-06-27 15:58:42 +02:00
Jannis Harder
d8ebd1eb9d
Reflect recent engine updates in the reference docs
2022-06-20 15:23:59 +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
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
N. Engelhardt
41cd8e5b5e
update install instructions for btorsim
2022-06-01 16:51:28 +02:00
N. Engelhardt
ad2c33dd37
docs: add instructions for newer btorsim version required
2022-05-24 11:39:10 +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
N. Engelhardt
3834fe7622
document btor engine, add overview of mode/engine/solver combinations, remove unimplemented modes
2022-03-25 18:01:09 +01:00
Claire Xen
fa5d5ad831
Merge pull request #120 from ythoma/patch-1
...
Update install.rst
2022-03-15 16:33:46 +01: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
Claire Xenia Wolf
b409b1179e
Update docs theme
...
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2021-11-30 10:47:43 +01:00
Claire Xenia Wolf
38562a5bb9
Update docs theme
...
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2021-11-29 16:51:54 +01:00
Claire Xenia Wolf
882d5b3a96
update docs theme
...
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2021-11-26 20:34:55 +01:00
Claire Xenia Wolf
1b3832cf92
Fixed names and links
2021-10-31 14:42:39 +01:00
Christian Krieg
21371fb7ac
Updated install instructions for super_prove
...
* Links were dead
* No binaries to download
* Updated with install information from super_prove github repository
* Augmented with additional commands to ease installation
2021-07-20 22:33:28 +02:00
Claire Xenia Wolf
66a458958d
Update docs conf.py
...
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2021-05-21 03:36:11 +02:00
Claire Xenia Wolf
dac0e1b69b
New docs conf.py
...
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2021-05-21 03:31:50 +02:00
N. Engelhardt
f5f1d9936f
Make readme of abstraction example more tutorial-like
2021-04-16 15:54:51 +02:00
Claire Xen
1ffef12cf1
Update conf.py
2021-03-04 16:49:31 +01:00
Claire Xen
ddd44fc30b
Delete symbiotic_logo.png
2021-02-24 17:52:54 +01:00
Claire Xen
9aa0963f26
Update conf.py
2021-02-24 17:48:13 +01:00
ythoma
0270359962
Update install.rst
...
On Ubuntu 20.04, I had to install curl as well:
sudo apt install curl
I guess that would be the same on other setups.
2021-02-05 09:46:04 +01:00
Miodrag Milanovic
091222b87f
Extract installation procedure to separate file
2020-10-23 14:03:55 +02:00
Matt Venn
37a1fec120
copyright
2020-10-15 18:02:03 +02:00
Matt Venn
81258745eb
logo and links
2020-10-15 17:02:52 +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
Alexandre Dumont aka Adlx
d29f7b9837
Tipo missing * in Global Clock example
2020-06-29 00:42:06 +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
9cb542ac7a
Fix YosysHQ links
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-08-13 17:25:10 +02:00
Clifford Wolf
ddbad8fd71
Documentation update: Boolector is using the MIT license now
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-07-23 15:24:04 +02:00