Add formal_bind example

Demonstrate binding SVA properties to a VHDL design.
Mention example code (with snippets) in section on Verific.

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;