Making alu 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
* Rewrite assignments of Dout_o & Overflow_o as GHDL synthesis don't
  support concatenation on left side of assignments
* Add some simple PSL assertions

alu/Makefile

@@ -1,6 +1,17 @@
-alu: alu.vhd alu_t.sv alu_f.sby
-	sby -f -d work alu_f.sby
+DUT := alu
 
+.PHONY: cover prove all clean
+
+all: cover bmc prove
+
+cover: ${DUT}.vhd symbiyosys.sby
+	sby --yosys "yosys -m ghdl" -f -d work/${DUT}-$@ symbiyosys.sby $@
+
+bmc: ${DUT}.vhd symbiyosys.sby
+	sby --yosys "yosys -m ghdl" -f -d work/${DUT}-$@ symbiyosys.sby $@
+
+prove: ${DUT}.vhd symbiyosys.sby
+	sby --yosys "yosys -m ghdl" -f -d work/${DUT}-$@ symbiyosys.sby $@
 
 clean:
 	rm -rf work

alu/alu.vhd

@@ -6,7 +6,8 @@ use ieee.numeric_std.all;
 
 entity alu is
   generic (
-    Width : natural := 8
+    Width  : natural := 8;
+    Formal : boolean := true
   );
   port (
     Reset_n_i  : in  std_logic;
@@ -24,7 +25,7 @@ end entity alu;
 architecture rtl of alu is
 
 
-  subtype t_opc is std_logic_vector(Opc_i'length-1 downto 0);
+  subtype t_opc is std_logic_vector(Opc_i'range);
 
   constant c_add : t_opc := "00";
   constant c_sub : t_opc := "01";
@@ -36,24 +37,61 @@ begin
 
 
   process (Reset_n_i, Clk_i) is
+    variable v_result : std_logic_vector(Width downto 0);
   begin
     if (Reset_n_i = '0') then
-      Dout_o <= (others => '0');
+      v_result   := (others => '0');
+      Dout_o     <= (others => '0');
+      OverFlow_o <= '0';
     elsif (rising_edge(Clk_i)) then
       case Opc_i is
-        when c_add => (OverFlow_o, Dout_o) <=
-          std_logic_vector(resize(unsigned(DinA_i), Dout_o'length+1) +
-                           resize(unsigned(DinB_i), Dout_o'length+1));
-        when c_sub => (OverFlow_o, Dout_o) <=
-          std_logic_vector(resize(unsigned(DinA_i), Dout_o'length+1) -
-                           resize(unsigned(DinB_i), Dout_o'length+1));
-        when c_and => Dout_o <= DinA_i and DinB_i;
-        when c_or  => Dout_o <= DinA_i or DinB_i;
+        when c_add =>
+          v_result := std_logic_vector(unsigned('0' & DinA_i) +
+                                       unsigned('0' & DinB_i));
+        when c_sub =>
+          v_result := std_logic_vector(unsigned('0' & DinA_i) -
+                                       unsigned('0' & DinB_i));
+        when c_and => v_result := DinA_i and DinB_i;
+        when c_or  => v_result := DinA_i or  DinB_i;
         when others => null;
       end case;
+      Dout_o     <= v_result(Width-1 downto 0);
+      OverFlow_o <= v_result(Width);
     end if;
   end process;
 
 
-end architecture rtl;
+  FormalG : if Formal generate
+
+    signal s_dina : std_logic_vector(DinA_i'range);
+    signal s_dinb : std_logic_vector(DinB_i'range);
+
+  begin
+
+    -- VHDL helper logic
+    process is
+    begin
+      wait until rising_edge(Clk_i);
+      s_dina <= DinA_i;
+      s_dinb <= DinB_i;
+    end process;
+
+
+    default clock is rising_edge(Clk_i);
+
+    AFTER_RESET : assert always
+      not Reset_n_i -> Dout_o = x"00" and OverFlow_o = '0';
 
+
+    ADD_OP : assert Reset_n_i and Opc_i = c_add -> next unsigned(Dout_o) = unsigned(s_dina) + unsigned(s_dinb) abort not Reset_n_i;
+
+    SUB_OP : assert Reset_n_i and Opc_i = c_sub -> next unsigned(Dout_o) = unsigned(s_dina) - unsigned(s_dinb) abort not Reset_n_i;
+
+    AND_OP : assert Reset_n_i and Opc_i = c_and -> next Dout_o = (s_dina and s_dinb) abort not Reset_n_i;
+
+    OR_OP :  assert Reset_n_i and Opc_i = c_or  -> next Dout_o = (s_dina or s_dinb) abort not Reset_n_i;
+
+  end generate FormalG;
+
+
+end architecture rtl;

alu/alu_f.sby

@@ -1,18 +0,0 @@
-[options]
-depth 30
-wait on
-mode prove
-#mode bmc
-
-[engines]
-smtbmc
-abc pdr
-
-[script]
-verific -vhdl alu.vhd
-verific -formal alu_t.sv
-prep -top alu_t
-
-[files]
-alu.vhd
-alu_t.sv

alu/alu_t.sv

@@ -1,76 +0,0 @@
-`define WIDTH 8
-
-
-module alu_t (
-    input               Reset_n_i,
-    input               Clk_i,
-    input  [1:0]        Opc_i,
-    input  [`WIDTH-1:0] DinA_i,
-    input  [`WIDTH-1:0] DinB_i,
-    output [`WIDTH-1:0] Dout_o,
-    output              OverFlow_o
-);
-
-
-
-  `define OPC_ADD 0
-  `define OPC_SUB 1
-  `define OPC_AND 2
-  `define OPC_OR  3
-
-
-  alu #(.Width(`WIDTH)) alu_i (
-    .Reset_n_i(Reset_n_i),
-    .Clk_i(Clk_i),
-    .Opc_i(Opc_i),
-    .DinA_i(DinA_i[`WIDTH-1:0]),
-    .DinB_i(DinB_i[`WIDTH-1:0]),
-    .Dout_o(Dout_o[`WIDTH-1:0]),
-    .OverFlow_o(OverFlow_o)
-  );
-
-
-  reg init_state = 1;
-
-  // 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;
-
-  default clocking
-    @(posedge Clk_i);
-  endclocking
-
-  default disable iff (!Reset_n_i);
-
-
-  bit unsigned [`WIDTH:0] dina, dinb;
-
-  assign dina = DinA_i;
-  assign dinb = DinB_i;
-
-  assert property (Opc_i == `OPC_ADD |=> Dout_o == ($past(DinA_i) + $past(DinB_i)));
-  assert property (Opc_i == `OPC_ADD && (dina + dinb) > 2**`WIDTH-1 |=> OverFlow_o);
-  assert property (Opc_i == `OPC_SUB |=> Dout_o == ($past(DinA_i) - $past(DinB_i)));
-  assert property (Opc_i == `OPC_SUB && (dina - dinb) > 2**`WIDTH-1 |=> OverFlow_o);
-  assert property (Opc_i == `OPC_AND |=> Dout_o == ($past(DinA_i) & $past(DinB_i)));
-  assert property (Opc_i == `OPC_OR |=> Dout_o == ($past(DinA_i) | $past(DinB_i)));
-
-
-
-  property cover_opc (opc);
-    Opc_i == opc;
-  endproperty
-
-  cover property (cover_opc(`OPC_ADD));
-  cover property (cover_opc(`OPC_SUB));
-  cover property (cover_opc(`OPC_AND));
-  cover property (cover_opc(`OPC_OR));
-
-
-endmodule
-

alu/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: abc bmc3
+prove: abc pdr
+
+[script]
+ghdl --std=08 -fpsl alu.vhd -e alu
+prep -auto-top
+
+[files]
+alu.vhd