Use SVA defaults for clock & reset; minor RTL optimizations for bettrer readability

README.md

@@ -1,16 +1,15 @@
-The original repository is located on my own git-server at [https://git.goodcleanfun.de/tmeissner/formal_verification](https://git.goodcleanfun.de/tmeissner/formal_verification)
+The original repository is located on my own git-server at [https://git.goodcleanfun.de/tmeissner/formal_hw_verification](https://git.goodcleanfun.de/tmeissner/formal_hw_verification)
 
 It is mirrored to github with every push, so both should be in sync.
 
 
 # formal_verification
 
-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 parser 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.
+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.
 
 ### 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
 A simple counter 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.
 

alu/alu.vhd

@@ -24,10 +24,12 @@ end entity alu;
 architecture rtl of alu is
 
 
-  constant c_add : std_logic_vector(1 downto 0) := "00";
-  constant c_sub : std_logic_vector(1 downto 0) := "01";
-  constant c_and : std_logic_vector(1 downto 0) := "10";
-  constant c_or  : std_logic_vector(1 downto 0) := "11";
+  subtype t_opc is std_logic_vector(Opc_i'length-1 downto 0);
+
+  constant c_add : t_opc := "00";
+  constant c_sub : t_opc := "01";
+  constant c_and : t_opc := "10";
+  constant c_or  : t_opc := "11";
 
 
 begin
@@ -40,14 +42,14 @@ begin
     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));
+          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 others => null;
+          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 others => null;
       end case;
     end if;
   end process;

alu/alu_t.sv

@@ -41,24 +41,29 @@ module alu_t (
   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 (@(posedge Clk_i) disable iff (!Reset_n_i) Opc_i == `OPC_ADD |=> Dout_o == ($past(DinA_i) + $past(DinB_i)));
-  assert property (@(posedge Clk_i) disable iff (!Reset_n_i) Opc_i == `OPC_ADD && (dina + dinb) > 2**`WIDTH-1 |=> OverFlow_o);
-  assert property (@(posedge Clk_i) disable iff (!Reset_n_i) Opc_i == `OPC_SUB |=> Dout_o == ($past(DinA_i) - $past(DinB_i)));
-  assert property (@(posedge Clk_i) disable iff (!Reset_n_i) Opc_i == `OPC_SUB && (dina - dinb) > 2**`WIDTH-1 |=> OverFlow_o);
-  assert property (@(posedge Clk_i) disable iff (!Reset_n_i) Opc_i == `OPC_AND |=> Dout_o == ($past(DinA_i) & $past(DinB_i)));
-  assert property (@(posedge Clk_i) disable iff (!Reset_n_i) Opc_i == `OPC_OR |=> Dout_o == ($past(DinA_i) | $past(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);
-    @(posedge Clk_i)
-      disable iff (!Reset_n_i) Opc_i == opc;
+    Opc_i == opc;
   endproperty
 
   cover property (cover_opc(`OPC_ADD));

counter/counter_t.sv

@@ -38,19 +38,23 @@ module counter_t (
 
   // Use global clock to constrain the DUT clock
   always @($global_clock) begin
-    assume(Clk_i != $past(Clk_i));
+    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);
 
-  // Fails with unbounded prove using SMTBMC, maybe
-  // the assumptions/assertions have to be more strict.
-  // With abc pdr this can be successfully proved.
-  assert property (@(posedge Clk_i) disable iff (!Reset_n_i) Data_o <  `ENDVAL |=> Data_o == $past(Data_o) + 1);
-  assert property (@(posedge Clk_i) disable iff (!Reset_n_i) Data_o == `ENDVAL |=> $stable(Data_o));
-  assert property (@(posedge Clk_i) Data_o >= `INITVAL && Data_o <= `ENDVAL);
+  // 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