Merge pull request #264 from YosysHQ/krys/vhd_example

Add formal_bind example

docs/examples/vhd/.gitignore

@@ -0,0 +1 @@
+formal_bind*/

docs/examples/vhd/formal_bind.sby

@@ -0,0 +1,20 @@
+[tasks]
+bmc
+cover
+
+[options]
+bmc: mode bmc
+cover: mode cover
+depth 16
+
+[engines]
+smtbmc bitwuzla
+
+[script]
+verific -vhdl updowncount.vhd
+verific -sv formal_bind.sv
+prep -top updowncount
+
+[files]
+updowncount.vhd
+formal_bind.sv

docs/examples/vhd/formal_bind.sv

@@ -0,0 +1,10 @@
+module formal_bind(input clk, rst, up, down, [3:0] count);
+
+    initial assume(rst);
+
+    assert property(@(posedge clk) count != 4'd15);
+    cover property(@(posedge clk) count == 4'd10);
+
+endmodule
+
+bind updowncount formal_bind fb_inst(.*);

docs/examples/vhd/updowncount.vhd

@@ -0,0 +1,33 @@
+library IEEE;
+use IEEE.STD_LOGIC_1164.ALL;
+use IEEE.STD_LOGIC_ARITH.all;
+use IEEE.STD_LOGIC_UNSIGNED.all;
+
+entity updowncount is
+    port (
+        rst, clk : in std_logic ;
+        up, down : in std_logic ;
+        o: out std_logic_vector(0 to 3)
+    );
+end updowncount;
+
+architecture rtl of updowncount is
+    signal count : std_logic_vector(0 to 3) := "0000";
+    begin
+        process(clk)
+        begin
+            if (rising_edge(clk)) then
+                if (rst = '1') then
+                    count <= "0000";
+                else
+                    if (up = '1' and count <= "1010") then
+                        count <= count + "0001";
+                    end if;
+                    if (down = '1' and count > "0000") then
+                        count <= count - "0001";
+                    end if;
+                end if;
+            end if;
+        end process;
+    o <= count;
+end rtl;

docs/source/verific.rst

@@ -140,3 +140,28 @@ multiple different clock domains are currently unsupported.
   * ``@(negedge`` *clock* ``iff`` *enable* ``)``
   * ``disable iff (`` *expression* ``)``
 
+SVA properties in a VHDL design
+-------------------------------
+
+The below code snippet, taken from an example SBY configuration included in
+|vhd_example|_, shows a VHDL design ``updowncount.vhd`` being loaded, followed
+by a SystemVerilog file ``formal_bind.sv``.
+
+.. |vhd_example| replace:: ``docs/examples/vhd``
+.. _vhd_example: https://github.com/YosysHQ/sby/tree/master/docs/examples/vhd
+
+.. literalinclude:: ../examples/vhd/formal_bind.sby
+  :language: yoscrypt
+  :start-after: [script]
+  :end-before: [files]
+  :caption: ``formal_bind.sby`` script section
+
+.. literalinclude:: ../examples/vhd/formal_bind.sv
+  :language: SystemVerilog
+  :caption: ``formal_bind.sv``
+
+As you can see, the ``formal_bind.sv`` file includes a ``formal_bind`` module
+and makes use of the ``bind`` keyword in SystemVerilog to create an instance of
+this module connecting the inputs to the signals of the same name in the VHDL
+design.  SVA properties can then be applied to those signals as if the whole
+design was in SystemVerilog.