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

196 commits

Author SHA1 Message Date
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 (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 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