Docs: Add section on changing properties

`veer_4.sby` introduces `chformal`, `cutpoint`, `prep -flatten` and `smtbmc --keep-going`.

docs/source/_examples/veer_4.sby

@@ -0,0 +1,101 @@
+[options]
+mode bmc
+multiclock on
+depth 40
+
+[engines]
+smtbmc --keep-going
+
+[script]
+exec -expect-return 0 -- bash -c 'RV_ROOT=$PWD ./configs/veer.config'
+read -f -formal veer.f
+prep -flatten -top veer_wrapper
+chformal -assert -assert2assume veer_wrapper/veer.dma_ctrl.assert_dma_axi_*
+cutpoint t:$mul t:$mem_v2
+
+tee -o ../props.txt log Cover cells:
+tee -a ../props.txt select t:$cover -list
+tee -a ../props.txt log
+tee -a ../props.txt log Assert cells:
+tee -a ../props.txt select t:$assert -list
+tee -a ../props.txt log
+tee -a ../props.txt log Assume cells:
+tee -a ../props.txt select t:$assume -list
+
+[file formal.sv]
+module formal_setup();
+    (* gclk *) reg gclk;
+    reg clk = '0;
+    always @(posedge gclk)
+        clk <= !clk;
+
+    reg [3:0] rst_counter = 2;
+    always @(posedge clk)
+        if (rst_counter)
+            rst_counter -= 1;
+
+    wire rst = rst_counter > 0;
+
+    always @* begin
+        setup_clk: assume (veer_wrapper.clk == clk);
+        setup_rst_l: assume (veer_wrapper.rst_l == !rst);
+        setup_dbg_rst_l: assume (veer_wrapper.dbg_rst_l == !rst);
+    end
+
+endmodule
+
+bind veer_wrapper formal_setup formal_setup_inst(.*);
+
+[file veer.f]
++incdir+design/include
++incdir+snapshots/default
+snapshots/default/common_defines.vh
+design/include/veer_types.sv
+design/lib/beh_lib.sv
+design/mem.sv
+design/pic_ctrl.sv
+design/dma_ctrl.sv
+design/ifu/ifu_aln_ctl.sv
+design/ifu/ifu_compress_ctl.sv
+design/ifu/ifu_ifc_ctl.sv
+design/ifu/ifu_bp_ctl.sv
+design/ifu/ifu_ic_mem.sv
+design/ifu/ifu_mem_ctl.sv
+design/ifu/ifu_iccm_mem.sv
+design/ifu/ifu.sv
+design/dec/dec_decode_ctl.sv
+design/dec/dec_gpr_ctl.sv
+design/dec/dec_ib_ctl.sv
+design/dec/dec_tlu_ctl.sv
+design/dec/dec_trigger.sv
+design/dec/dec.sv
+design/exu/exu_alu_ctl.sv
+design/exu/exu_mul_ctl.sv
+design/exu/exu_div_ctl.sv
+design/exu/exu.sv
+design/lsu/lsu.sv
+design/lsu/lsu_bus_buffer.sv
+design/lsu/lsu_clkdomain.sv
+design/lsu/lsu_addrcheck.sv
+design/lsu/lsu_lsc_ctl.sv
+design/lsu/lsu_stbuf.sv
+design/lsu/lsu_bus_intf.sv
+design/lsu/lsu_ecc.sv
+design/lsu/lsu_dccm_mem.sv
+design/lsu/lsu_dccm_ctl.sv
+design/lsu/lsu_trigger.sv
+design/dbg/dbg.sv
+design/dmi/dmi_wrapper.v
+design/dmi/dmi_jtag_to_core_sync.v
+design/dmi/rvjtag_tap.sv
+design/lib/mem_lib.sv
+design/lib/ahb_to_axi4.sv
+design/lib/axi4_to_ahb.sv
+design/veer.sv
+design/veer_wrapper.sv
+formal.sv
+
+[files]
+Cores-VeeR-EH1/design
+Cores-VeeR-EH1/configs
+Cores-VeeR-EH1/tools

docs/source/veer.rst

@@ -159,3 +159,63 @@ We can see from this that the ``dma_ctrl`` module is expecting a valid AXI
 connection, which is currently missing.  We could add assumptions on the inputs
 that match the assertions, but we already have perfectly good properties that we
 can use: the assertions themselves.
+
+Changing properties
+~~~~~~~~~~~~~~~~~~~
+
+The ``chformal`` command in Yosys enables formal properties to be changed at run
+time.  With this command we can convert assertions to assumptions (as well as
+the reverse), or entirely remove properties that we are not currently interested
+in.
+
+From our previous run we know that the assert cell
+``dma_ctrl_default/assert_dma_axi_awlen_check`` fails.  We could add the
+following line after calling ``prep`` to remove it:
+
+.. code-block:: yoscrypt
+
+    chformal -remove dma_ctrl_default/assert_dma_axi_awlen_check
+
+But then we would just be left with another assertion in the same module
+failing.  This also has the side effect that if anything else in the design is
+relying on the (now missing) assertion being correct, it will also fail.
+Instead, let's add the following:
+
+.. code-block:: yoscrypt
+
+    chformal -assert -assert2assume dma_ctrl_default/assert_dma_axi_*
+
+We can see from the |cmdref for chformal|_ (or by running calling ``help
+chformal`` within Yosys) that we can specify the type of formal property to
+target, and that the final argument is a ``selection`` rather than simply the
+name of a property.  Thus we use a wildcard to match all of the ``dma_ctrl``
+properties related to AXI, limited to just assert cells, and then convert them
+to assume cells.  Provided the AXI is properly connected and valid, this ensures
+that any other properties relying on the ``dma_ctrl`` can also be verified.
+
+.. |cmdref for chformal| replace:: command reference page for ``chformal``
+.. _cmdref for chformal: https://yosyshq.readthedocs.io/projects/yosys/en/latest/cmd/chformal.html
+
+The keep-going flag
+~~~~~~~~~~~~~~~~~~~
+
+At this stage of the process we may be ready to run the solver against all of
+our properties rather than stopping at the first failure, and increasing the
+depth of BMC.  We can do this by adding the ``--keep-going`` flag to our engine,
+e.g. ``smtbmc --keep-going``. In order to keep run time down there are a few
+things worth considering.  First is the ``-flatten`` flag for ``prep``.  This
+will flatten the circuit and allow additional course grain optimizations.  The
+next is adding cutpoints for elements which are computationally difficult to
+prove.  This could look like the following:
+
+.. literalinclude:: _examples/veer_4.sby
+    :language: sby
+    :end-before: tee -o
+
+Note that flattening the hierarchy means we have the ``dma_ctrl`` assertions
+need to be referenced slightly differently.  Rather than
+``dma_ctrl_default/assert...`` we now see
+``veer_wrapper/veer.dma_ctrl.assert...``.  We have also added cutpoints for all
+``$mul`` and ``$mem_v2`` cells, i.e. multipliers and memory blocks.  This does
+of course mean that any properties which rely on correct and valid multipliers
+or memories will now fail, but we can verify those separately.