3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-04-27 23:45:50 +00:00
Commit graph

157 commits

Author SHA1 Message Date
KrystalDelusion
df2610d598 Fixes before merge 2022-08-22 21:18:40 +12: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
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
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
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
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
KrystalDelusion
7ba67ef260 Removing unnecessary underflow assertions 2022-07-01 11:15:47 +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
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
66ef51d846 Verification properties in doc 2022-06-07 11:50:26 +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
N. Engelhardt
41cd8e5b5e update install instructions for btorsim 2022-06-01 16:51:28 +02:00
KrystalDelusion
f5257011f6 Specifying z3 to support minimum required install 2022-05-31 11:31:20 +12: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
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
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
7468e7655d Alignment fixing 2022-05-10 11:03:40 +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
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
f33c2eda52 Updating/rearranging links 2022-05-02 10:44:28 +12:00