KrystalDelusion
562a504709
Docs fix
2025-07-07 20:07:25 +12:00
Krystine Sherwin
4d8462b58e
Add cover_assert option
2025-07-05 11:17:05 +12:00
Miodrag Milanovic
ab2003d90f
Update location of demo files
2025-05-06 12:54:18 +02:00
Jannis Harder
c8800ecd34
allow running SBY tests with an external examples directory
2025-04-28 16:13:30 +02:00
George Rennie
20ee439df9
Merge pull request #313 from gipsyh/rIC3
...
Support rIC3 model checker as backend
2025-03-14 15:13:06 +01:00
Yuheng Su
fc0afb04c5
Set minimum rIC3 version to 1.35
2025-03-14 22:00:09 +08:00
N. Engelhardt
9675d158ce
Merge pull request #264 from YosysHQ/krys/vhd_example
...
Add formal_bind example
2025-03-03 15:20:59 +00:00
Miodrag Milanović
b6be8ad0fc
Merge pull request #311 from sporniket/patch-2
...
[docs] Fixes instructions for installing boolector
2025-03-03 16:15:59 +01:00
N. Engelhardt
44c44097f8
Merge pull request #310 from sporniket/patch-1
...
[docs] instruct to clone yosys with '--recurse-submodules'
2025-03-03 15:11:05 +00:00
N. Engelhardt
4d92762d5a
Merge pull request #278 from YosysHQ/krys/docs_verific
...
Add note on docs to clarify verific support
2025-03-03 15:09:36 +00:00
Yuheng Su
8da7174b16
update rIC3 backend
...
Signed-off-by: Yuheng Su <gipsyh.icu@gmail.com>
2024-12-17 04:41:58 +00:00
Yuheng Su
daf4e4cb39
Support rIC3 as backend
...
Signed-off-by: Yuheng Su <gipsyh.icu@gmail.com>
2024-12-16 11:02:45 +00:00
David SPORN
8885582e3c
[docs] Fixes instructions for installing boolector
...
There is a `build` folder where `bin\btorsim` is generated
2024-11-19 07:20:08 +01:00
David SPORN
7fc7ed38ae
[docs] instruct to clone yosys with '--recurse-submodules'
...
Without using '--recurse-submodule', make fails to retrieve them before building.
2024-11-19 06:58:01 +01:00
Jannis Harder
62d17081bf
Merge pull request #276 from YosysHQ/krys/test-furo-ys
...
Use furo-ys
2024-09-27 14:21:07 +02:00
George Rennie
07b9b7cbb8
docs: fix reference to aigbmc engine option
2024-08-01 17:34:54 +01:00
Krystine Sherwin
0fab912005
Docs: Use sby role shortcut
2024-06-10 18:46:31 +12:00
Krystine Sherwin
a3844d4a30
Docs: Use sby lexer
2024-06-10 18:41:15 +12:00
Krystine Sherwin
5426bee107
Use furo-ys
2024-05-14 12:54:30 +12:00
Krystine Sherwin
7f1853bd78
Add note on docs to clarify verific support
...
Having a verific license does not provide access to the verific frontend. This helps to make that clearer.
2024-05-14 12:25:29 +12:00
Krystine Sherwin
549c5f33f5
Add formal_bind example
...
Demonstrate binding SVA properties to a VHDL design.
Mention example code (with snippets) in section on Verific.
2024-03-05 15:29:08 +13:00
Jannis Harder
8581bd3171
Add dft/data_diode example
...
This requires YosysHQ/yosys#3961 and YosysHQ/sby#249 to work
2023-09-28 18:59:27 +02:00
Claire Xen
ffa53a32c1
Merge branch 'master' into krys/argparse_docs
2023-07-18 16:27:12 +02:00
Jannis Harder
c52acf2a1f
docs: Make sphinx-argparse work independently of sphinx's cwd
2023-06-19 11:39:37 +02:00
Krystine Sherwin
1a4c2a57ad
Add sbysrc to path during docs build
2023-06-19 21:39:07 +12:00
Krystine Sherwin
27e20fd5c3
Add sphinx-argparse to generate usage
...
Move parser generation into a seperate file to avoid import issues with bad python modules during docs gen.
With the requirements.txt provided to readthedocs, there shouldn't need to be any other changes?
Also I've never been able to run `make test` so I'm not actually sure if the changes break sby, but they shouldn't.
2023-06-13 11:40:28 +12:00
Jannis Harder
513d0d4288
Change Sphinx theme to "furo"
2023-05-03 16:56:09 +02:00
N. Engelhardt
81ee5fdd5a
update prerequisites
2023-02-08 17:59:26 +01:00
Jannis Harder
c5dce57067
append_assume: Make append_assume on the default for now
...
Having `append_assume off` needs `vcd_sim on` to not be ignored with a
warning and `vcd_sim off` is still the default.
2023-02-08 14:18:52 +01:00
Jannis Harder
7a3b88ca67
docs: Document new sim related options
2023-02-06 16:55:19 +01:00
Jannis Harder
6d1ef8b5a0
docs: Yices is still recommended
2023-02-06 16:54:37 +01:00
Jannis Harder
90616c280b
tests: Do not run the same SBY task multiple times in parallel
2022-10-20 14:18:51 +02:00
KrystalDelusion
37140e7e81
Fixing golden/fifo.sv
...
Had missed a change from (non golden) fifo.sv.
2022-09-07 09:52:52 +12:00
Jannis Harder
168d667b6d
Add vcd option to make VCD writing optional
2022-09-05 15:42:24 +02:00
Jannis Harder
326247fdef
tests: Skip broken tests
2022-09-03 00:04:40 +02:00
N. Engelhardt
4adb99ea30
Merge pull request #174 from KrystalDelusion/fifo_example
2022-08-22 11:34:51 +02:00
KrystalDelusion
82a6edf295
Moving newstart to replace quickstart
2022-08-22 21:20:59 +12:00
KrystalDelusion
df2610d598
Fixes before merge
2022-08-22 21:18:40 +12:00
Aki Van Ness
e8b8816143
docs: removed empty line
2022-08-18 05:36:11 -04:00
Aki Van Ness
a6c220dd5d
docs: Cut out the in-progress docs in preperation for a merge
2022-08-18 05:36:11 -04:00
Aki Van Ness
da56a3c6d1
docs: started working on a rough draft of the docs for the new sections and changes to existing sections
2022-08-18 05:36:11 -04:00
KrystalDelusion
d6d7119cd5
Rewrite of non verific underfill/overfill
...
w_underfill should provide identical results regardless of whether
or not Verific is used. w_overfill doesn't have the extra check
for prettiness without Verific because I'm too lazy to do it.
Replaced $past function with past_nwen register to ensure correct
operation.
Expanded w_underfill under Verific to use a property block to more
easily compare the two versions side by side.
Changed Concurrent assertions section of doc to compare the two
implementations of w_underfill. Should provide a better example
for why using verific makes it easier.
2022-08-09 11:48:40 +12:00
KrystalDelusion
1d4716a5f9
Add noverific task to test the non verific code
...
Mostly for CI to ensure fallback code still functions as intended.a
Also reverted the change in the grep command to 1 line after.
2022-08-09 11:32:59 +12:00
KrystalDelusion
ad8730fa44
Fix typo
2022-08-08 21:30:31 +12:00
Jannis Harder
3412ea859b
New "none" engine to be used with the "make_model" option
2022-08-05 16:31:15 +02:00
Jannis Harder
231f0b80aa
Add make_model option to generate models not required by the task
...
Useful to do custom things (like counter example minimization) but still
use sby's flow to prepare models.
2022-08-05 16:31:15 +02:00
KrystalDelusion
cfa4352bae
Changes to reset
...
Active high.
Removed init.
Better over/underfill cover properties for verific. Moved basic cover statement to only be used when there is no verific.
Other general tidy up.
Also updated/fixed a couple minor things in newstart.rst.
2022-08-02 12:11:09 +12:00
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
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
