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.
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.
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.
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.
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.
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.
* 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
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.
