Added symbiyosys to toolchains

Signed-off-by: Joppe Blondel <joppe@blondel.nl>

examples/formal/RTL/counter.vhd

@@ -24,12 +24,23 @@ begin
 
     cnt <= std_logic_vector(icnt);
 
-    process(ACLK, ARESETN)
+    f_counter : if formal generate
+    begin
+        -- Set clock source for all assertions
+        default clock is rising_edge(ACLK);
+        -- Counter is always under mxcnt if it started under max
+        a_never_exceeds_max : assert (always (icnt<mxcnt) -> always (icnt<mxcnt));
+        -- Counter is always reset to 0
+        a_counter_reset_to_zero : assert (always (ARESETN='0') -> (icnt=0));
+    end generate;
+
+    p_counter : process(ACLK, ARESETN)
     begin
         if ARESETN='0' then
             icnt <= (others=>'0');
         elsif rising_edge(ACLK) then
-            if icnt<mxcnt then
+            -- Without this -1 the assertion wont hold
+            if icnt<mxcnt-1 then
                 icnt <= icnt + 1;
             else 
                 icnt <= (others=>'0');

examples/formal/SIM/counter.sby

@@ -0,0 +1,22 @@
+[tasks]
+bmc d_12
+cover d_120
+prove d_4
+
+[options]
+bmc:mode bmc
+cover:mode cover
+prove:mode prove
+d_120:depth 120
+d_12:depth 12
+d_4:depth 4
+
+[engines]
+smtbmc
+
+[script]
+ghdl -fpsl --std=08 -gformal=true counter.vhd -e counter
+prep -top counter
+
+[files]
+RTL/counter.vhd

examples/formal/project.cfg

@@ -25,4 +25,17 @@ runtime             = all
 # Fileset
 files_vhdl          = RTL/counter.vhd 
                       SIM/tb_counter.vhd
+# ######################################
+
+# ######################################
+# Formal verification with symbiyosys
+[target.formal]
+toolchain           = symbiyosys
+
+# Toolchain settings
+sby_opts            =
+
+# Fileset
+files_sby           = SIM/counter.sby
+files_other         = RTL/counter.vhd 
 # ######################################