Making counter design work with GHDL synthesis

* Remove unused SVA properties file
* Makefile optimizations
* Use prep auto-top option to prevent error with not founded top-level module
  when using generics
* Add some simple PSL assertions

README.md

@@ -7,7 +7,7 @@ It is mirrored to github with every push, so both should be in sync.
 
 Tests and examples of using formal verification to check correctness of digital hardware designs. All tests are done with SymbiYosys, a front-end for formal verification flows based on [Yosys](https://github.com/YosysHQ). Some examples use the VHDL/SystemVerilog frontend plugin by Verific which isn't free SW and not included in the free Yosys version. See on the [Symbiotic EDA website](https://www.symbioticeda.com) for more information.
 
-There is a branch named [ghdl-synth](https://github.com/tmeissner/formal_hw_verification/tree/ghdl-synth) which uses [ghdlsynth-beta](https://github.com/tgingold/ghdlsynth-beta) as VHDL frontend plugin for SymbiYosys. Furthermore using GHDL(synth) as synthesis frontend allows using PSL as verification language. Only the vai_reg design can be verified in this branch at the moment.
+There is a branch named [ghdl-synth](https://github.com/tmeissner/formal_hw_verification/tree/ghdl-synth) which uses [ghdlsynth-beta](https://github.com/tgingold/ghdlsynth-beta) as VHDL frontend plugin for SymbiYosys. Furthermore using GHDL(synth) as synthesis frontend allows using PSL as verification language. The alu, counter & vai_reg designs can be verified in this branch at the moment.
 
 ### alu
 A simple ALU design in VHDL, together with a formal testbench written in SystemVerilog. The testbench contains various simple SVA properties used by assert & cover directives which are proved with the SymbiYosys tool.

counter/Makefile

@@ -1,7 +1,11 @@
-.PHONY: counter
-counter: counter.vhd counter_t.sv counter_f.sby
-	sby -f -d work counter_f.sby
+DUT := counter
+
+.PHONY: cover bmc prove all clean
+
+all: cover bmc prove
+
+cover bmc prove: ${DUT}.vhd symbiyosys.sby
+	sby --yosys "yosys -m ghdl" -f -d work/${DUT}-$@ symbiyosys.sby $@
 
-.PHONY: clean
 clean:
 	rm -rf work

counter/counter.vhd

@@ -7,7 +7,8 @@ use ieee.numeric_std.all;
 entity counter is
   generic (
     InitVal : natural := 0;
-    EndVal  : natural := 64
+    EndVal  : natural := 16;
+    Formal  : boolean := true
   );
   port (
     Reset_n_i : in  std_logic;
@@ -36,5 +37,39 @@ begin
   end process;
 
 
+  FormalG : if Formal generate
+
+    signal s_data : unsigned(Data_o'range);
+
+  begin
+
+    -- VHDL helper logic
+    process is
+    begin
+      wait until rising_edge(Clk_i);
+      s_data <= unsigned(Data_o);
+    end process;
+
+    default clock is rising_edge(Clk_i);
+
+    -- Initial reset
+    INITIAL_RESET : restrict {Reset_n_i = '0'[*2]; Reset_n_i = '1'[+]}[*1];
+
+    AFTER_RESET : assert always
+      not Reset_n_i -> Data_o = (Data_o'range => '0');
+
+    COUNT_UP : assert always
+      Reset_n_i and unsigned(Data_o) < to_unsigned(EndVal, 32) -> next unsigned(Data_o) = s_data + 1;
+
+    END_VALUE : assert always
+      unsigned(Data_o) = to_unsigned(EndVal, 32) -> next unsigned(Data_o) = s_data;
+
+    VALID_RANGE : assert always
+      unsigned(Data_o) >= to_unsigned(InitVal, 32) and
+      unsigned(Data_o) <= to_unsigned(EndVal, 32);
+
+  end generate FormalG;
+
+
 end architecture rtl;
 

counter/counter_f.sby

@@ -1,17 +0,0 @@
-[options]
-mode prove
-depth 30
-wait on
-
-[engines]
-smtbmc
-abc pdr
-
-[script]
-verific -vhdl counter.vhd
-verific -formal counter_t.sv
-prep -top counter_t
-
-[files]
-counter.vhd
-counter_t.sv

counter/counter_t.sv

@@ -1,61 +0,0 @@
-module counter_t (
-    input         Reset_n_i,
-    input         Clk_i,
-    output [31:0] Data_o
-);
-
-
-  `define INITVAL 8
-  `define ENDVAL  64
-
-
-  counter #(
-    .InitVal(`INITVAL),
-    .EndVal(`ENDVAL)
-  ) counter_i (
-    .Reset_n_i(Reset_n_i),
-    .Clk_i(Clk_i),
-    .Data_o(Data_o)
-  );
-
-
-             reg  init_state = 1;
-  (* gclk *) wire gbl_clk;
-
-  // Initial reset
-  always @(*) begin
-    if (init_state) assume (!Reset_n_i);
-    if (!init_state) assume (Reset_n_i);
-  end
-
-  always @(posedge Clk_i)
-    init_state = 0;
-
-  // Generate global clock
-  global clocking
-    @(posedge gbl_clk);
-  endclocking
-
-  // Use global clock to constrain the DUT clock
-  always @($global_clock) begin
-    assume (Clk_i != $past(Clk_i));
-  end
-
-  default clocking
-    @(posedge Clk_i);
-  endclocking
-
-  default disable iff (!Reset_n_i);
-
-  // Immediate assertions
-  always @(*)
-    if (!Reset_n_i) assert (Data_o == `INITVAL);
-
-  // Concurrent assertions
-  assert property (Data_o <  `ENDVAL |=> Data_o == $past(Data_o) + 1);
-  assert property (Data_o == `ENDVAL |=> $stable(Data_o));
-  assert property (Data_o >= `INITVAL && Data_o <= `ENDVAL);
-
-
-endmodule
-

counter/symbiyosys.sby

@@ -0,0 +1,22 @@
+[tasks]
+cover
+bmc
+prove
+
+[options]
+depth 25
+cover: mode cover
+bmc: mode bmc
+prove: mode prove
+
+[engines]
+cover: smtbmc z3
+bmc: smtbmc z3
+prove: smtbmc z3
+
+[script]
+ghdl --std=08 -fpsl counter.vhd -e counter
+prep -auto-top
+
+[files]
+counter.vhd