From 66ef51d846bcbebaee0579bafe728737f2bb269f Mon Sep 17 00:00:00 2001
From: KrystalDelusion <krystinedawn@yosyshq.com>
Date: Tue, 7 Jun 2022 11:50:26 +1200
Subject: [PATCH] Verification properties in doc

---
 docs/source/newstart.rst | 79 +++++++++++++++++++++++++++++++++++++++-
 1 file changed, 77 insertions(+), 2 deletions(-)

diff --git a/docs/source/newstart.rst b/docs/source/newstart.rst
index 0f13f2b..bf8dd19 100644
--- a/docs/source/newstart.rst
+++ b/docs/source/newstart.rst
@@ -7,7 +7,7 @@ Getting started
     `GTKWave <http://gtkwave.sourceforge.net/>`_, an open source VCD viewer.
 
 First In, First Out (FIFO) buffer
-********************************
+*********************************
 
 From `Wikipedia <https://en.wikipedia.org/wiki/FIFO_(computing_and_electronics)>`_,
 a FIFO is 
@@ -33,4 +33,79 @@ address generator module will be instantiated twice; once for the write address
 and once for the read address.  In both cases, the address will start at and
 reset to 0, and will increment by 1 when an enable signal is received.  When the
 address pointers increment from the maximum storage value they reset back to 0,
-providing a circular queue.
+providing a circular queue.  The top level design implemented, can be found in
+``top.sv``.  
+
+Verification properties
+***********************
+
+In order to verify our design we must first define properties that it must
+satisfy.  For example, there must never be a negative number of values in the
+FIFO.  Similarly, there must never be more than there is memory available.  By
+assigning a signal to count the number of values in the buffer, we can make the
+following assertions in the code:
+
+.. code-block:: systemverilog
+
+    a_uflow:  assert (count >= 0);
+    a_oflow:  assert (count <= MAX_DATA);
+
+It is also possible to use the prior value of a signal for comparison.  This can
+be used, for example, to ensure that the count is only able to increase or
+decrease by 1.  A case must be added to handle resetting the count directly to
+0, as well as if the count does not change.  This can be seen in the following
+code; at least one of these conditions must be true at all times if our design
+is to be correct.
+
+.. code-block:: systemverilog
+
+    a_counts: assert (count == 0
+                   || count == $past(count)
+                   || count == $past(count) + 1
+                   || count == $past(count) - 1);
+
+As our count signal is used independently of the read and write pointers, we
+must verify that the count is always correct.  While the write pointer will
+always be at the same point or *after* the read pointer, the circular buffer
+means that the write *address* could wrap around and appear *less than* the read
+address.  So we must first perform some simple arithmetic to find the absolute
+difference in addresses, and then compare with the count signal.
+
+.. code-block:: systemverilog
+
+    assign addr_diff = waddr >= raddr 
+                     ? waddr - raddr 
+                     : waddr + MAX_DATA - raddr;
+                     
+    a_count_diff: assert  (count == addr_diff 
+                        || count == MAX_DATA && addr_diff == 0);
+
+Concurrent assertions
+*********************
+
+Until this point, all of the properties described have been *immediate*
+assertions.  As the name suggests, immediate assertions are evaluated
+immediately whereas concurrent assertions allow for the capture of sequences of
+events which occur across time.  The use of concurrent assertions requires a
+more advanced parser, such as Verific.  Verific is included for use in the
+*Tabby CAD Suite*.  
+
+With concurrent assertions we are able to verify more fully that our enables and
+status flags work as desired.  For example, we can assert that if the read
+enable signal is high then the address of the read pointer *must* change.
+Because of our earlier *immediate* assertions that the pointer address can only
+increment or remain the same we do not need to specify that here.  We can also
+assert that if the enable is low, and the buffer is not full and potentially
+requires a skip in the read address, then the read address will *not* change.
+
+.. code-block:: systemverilog
+
+    ap_raddr2: assert property (ren |=> $changed(raddr));
+    ap_raddr3: assert property (!ren && !full  |=> $stable(raddr));
+
+
+Further information
+*******************
+For more information on the uses of assertions and the difference between
+immediate and concurrent assertions, refer to appnote 109: Property Checking
+with SystemVerilog Assertions.