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
168d667b6d
Add vcd option to make VCD writing optional
2022-09-05 15:42:24 +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
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
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
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
a5f67ed904
Merge branch 'master' into fifo_example
2022-07-01 11:46:02 +12:00
KrystalDelusion
de5b9b7821
Changed phrasing to avoid confusion on witnesses
2022-07-01 11:29:33 +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
Jannis Harder
685457915a
docs: add missing autotune.rst
2022-06-30 17:50:05 +02: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
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
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
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
N. Engelhardt
41cd8e5b5e
update install instructions for btorsim
2022-06-01 16:51:28 +02:00
KrystalDelusion
b18f22cf43
Removing install details for optional engines
2022-05-31 11:18:05 +12:00
N. Engelhardt
ad2c33dd37
docs: add instructions for newer btorsim version required
2022-05-24 11:39:10 +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
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
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
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
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
