Merge pull request #594 from diffblue/assert-final

tautschnig · web-flow · commit e2f7b6053421 · 2024-07-15T12:08:14.000+02:00
SystemVerilog: final immediate assertions
diff --git a/regression/ebmc/example1/example1.sv b/regression/ebmc/example1/example1.sv
@@ -11,6 +11,6 @@ module main(input a, input b);
 
   my_add adder(a, b, result);
 
-  assert property (a+b==result);
+  assert final (a+b==result);
 
 endmodule
diff --git a/regression/verilog/Array1/main.sv b/regression/verilog/Array1/main.sv
@@ -4,7 +4,7 @@ module top (input clk, input reset);
 
    assign x[4][5][3] = 1;
    
-   p1: assert property (x[4][5][3] == 1);
+   p1: assert final (x[4][5][3] == 1);
 
 endmodule
    
diff --git a/regression/verilog/SVA/immediate3.desc b/regression/verilog/SVA/immediate3.desc
@@ -0,0 +1,9 @@
+CORE
+immediate3.sv
+--bound 0
+^\[full_adder\.assert\.1\] always \(\{ full_adder\.carry, full_adder\.sum \}\) == full_adder\.a \+ full_adder\.b \+ full_adder\.c: PROVED up to bound 0$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/regression/verilog/SVA/immediate3.sv b/regression/verilog/SVA/immediate3.sv
@@ -0,0 +1,9 @@
+module full_adder(input a, b, c, output sum, carry);
+
+  assign sum = a ^ b ^ c;
+  assign carry = a & b | (a ^ b) & c;
+
+  always @(*)
+    assert final({carry, sum} == a + b + c);
+
+endmodule
diff --git a/regression/verilog/SVA/static_final1.desc b/regression/verilog/SVA/static_final1.desc
@@ -0,0 +1,9 @@
+CORE
+static_final1.sv
+--bound 0
+^\[full_adder\.p0\] always \(\{ full_adder\.carry, full_adder\.sum \}\) == full_adder\.a \+ full_adder\.b \+ full_adder\.c: PROVED up to bound 0$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/regression/verilog/SVA/static_final1.sv b/regression/verilog/SVA/static_final1.sv
@@ -0,0 +1,10 @@
+module full_adder(input a, b, c, output sum, carry);
+
+  assign sum = a ^ b ^ c;
+  assign carry = a & b | (a ^ b) & c;
+
+  // 1800-2017
+  // 16.4.3 Deferred assertions outside procedural code
+  p0: assert final ({carry, sum} == a + b + c);
+
+endmodule
diff --git a/regression/verilog/SVA/system_verilog_assertion3.sv b/regression/verilog/SVA/system_verilog_assertion3.sv
@@ -1,10 +1,10 @@
 module main();
 
-  assert property ($onehot('b0001000));
-  assert property (!$onehot('b0101000));
-  assert property (!$onehot('b00000));
-  assert property ($onehot0('b00000));
-  assert property ($onehot0('b000100));
-  assert property (!$onehot0('b010100));
+  assert final ($onehot('b0001000));
+  assert final (!$onehot('b0101000));
+  assert final (!$onehot('b00000));
+  assert final ($onehot0('b00000));
+  assert final ($onehot0('b000100));
+  assert final (!$onehot0('b010100));
 
 endmodule
diff --git a/regression/verilog/data-types/integer_atom_types1.sv b/regression/verilog/data-types/integer_atom_types1.sv
@@ -1,10 +1,10 @@
 module main;
 
-   p0: assert property ($bits(byte) == 8);
-   p1: assert property ($bits(shortint) == 16);
-   p2: assert property ($bits(int) == 32);
-   p3: assert property ($bits(longint) == 64);
-   p4: assert property ($bits(integer) == 32);
-   p5: assert property ($bits(time) == 64);
+   p0: assert final ($bits(byte) == 8);
+   p1: assert final ($bits(shortint) == 16);
+   p2: assert final ($bits(int) == 32);
+   p3: assert final ($bits(longint) == 64);
+   p4: assert final ($bits(integer) == 32);
+   p5: assert final ($bits(time) == 64);
 
 endmodule
diff --git a/regression/verilog/data-types/type_operator.sv b/regression/verilog/data-types/type_operator.sv
@@ -6,7 +6,7 @@ module main;
   typedef bit [31:0] some_type;
   wire some_type next_wire;
 
-  p0: assert property ($bits(other_wire) == 32);
-  p1: assert property ($bits(next_wire) == 32);
+  p0: assert final ($bits(other_wire) == 32);
+  p1: assert final ($bits(next_wire) == 32);
 
 endmodule
diff --git a/regression/verilog/data-types/vector_types1.sv b/regression/verilog/data-types/vector_types1.sv
@@ -11,14 +11,14 @@ module main;
   wire logic signed [7:0] some_logic_signed;
 
   // expected to pass
-  p0: assert property ($bits(implicit) == 8);
-  p1: assert property ($bits(some_bits) == 8);
-  p2: assert property ($bits(some_logic) == 8);
-  p3: assert property ($bits(implicit_unsigned) == 8);
-  p4: assert property ($bits(some_bits_unsigned) == 8);
-  p5: assert property ($bits(some_logic_unsigned) == 8);
-  p6: assert property ($bits(implicit_signed) == 8);
-  p7: assert property ($bits(some_bits_signed) == 8);
-  p8: assert property ($bits(some_logic_signed) == 8);
+  p0: assert final ($bits(implicit) == 8);
+  p1: assert final ($bits(some_bits) == 8);
+  p2: assert final ($bits(some_logic) == 8);
+  p3: assert final ($bits(implicit_unsigned) == 8);
+  p4: assert final ($bits(some_bits_unsigned) == 8);
+  p5: assert final ($bits(some_logic_unsigned) == 8);
+  p6: assert final ($bits(implicit_signed) == 8);
+  p7: assert final ($bits(some_bits_signed) == 8);
+  p8: assert final ($bits(some_logic_signed) == 8);
 
 endmodule
diff --git a/regression/verilog/elaboration/type_operator.sv b/regression/verilog/elaboration/type_operator.sv
@@ -5,6 +5,6 @@ module main;
 
   parameter param0 = $bits(other_wire);
 
-  p0: assert property (param0 == 32);
+  p0: assert final (param0 == 32);
 
 endmodule
diff --git a/regression/verilog/elaboration/var_bits.sv b/regression/verilog/elaboration/var_bits.sv
@@ -4,6 +4,6 @@ module main;
   var [$bits(some_var)-1:0] other_var;
   parameter param = $bits(other_var);
 
-  p0: assert property (param == 32);
+  p0: assert final (param == 32);
 
 endmodule
diff --git a/regression/verilog/enums/enum4.sv b/regression/verilog/enums/enum4.sv
@@ -3,6 +3,6 @@ module main;
   typedef enum bit [7:0] { A = 'h0101 } enum_t;
 
   // expected to pass
-  p1: assert property (A == enum_t'(1));
+  p1: assert final (A == enum_t'(1));
 
 endmodule
diff --git a/regression/verilog/enums/enum_base_type1.sv b/regression/verilog/enums/enum_base_type1.sv
@@ -3,6 +3,6 @@ module main;
   typedef enum bit [7:0] { A } enum_t;
 
   // expected to pass
-  p1: assert property ($bits(A) == 8);
+  p1: assert final ($bits(A) == 8);
 
 endmodule
diff --git a/regression/verilog/enums/enum_base_type2.sv b/regression/verilog/enums/enum_base_type2.sv
@@ -6,6 +6,6 @@ module main;
   parameter p = 8;
 
   // expected to pass
-  p1: assert property ($bits(A) == p);
+  p1: assert final ($bits(A) == p);
 
 endmodule
diff --git a/regression/verilog/enums/enum_cast1.sv b/regression/verilog/enums/enum_cast1.sv
@@ -3,7 +3,7 @@ module main;
   typedef enum { A = 1, B = 2 } enum_t;
 
   // expected to pass
-  p1: assert property (A == enum_t'(1));
-  p2: assert property (B == enum_t'(2));
+  p1: assert final (A == enum_t'(1));
+  p2: assert final (B == enum_t'(2));
 
 endmodule
diff --git a/regression/verilog/enums/enum_initializers1.sv b/regression/verilog/enums/enum_initializers1.sv
@@ -3,7 +3,7 @@ module main;
   enum { A = 1, B = A + 10 } my_enum;
 
   // expected to pass
-  pA: assert property (A == 1);
-  pB: assert property (B == 11);
+  pA: assert final (A == 1);
+  pB: assert final (B == 11);
 
 endmodule
diff --git a/regression/verilog/enums/enum_initializers2.sv b/regression/verilog/enums/enum_initializers2.sv
@@ -5,8 +5,8 @@ module main;
   enum { A = 1, C = B + 1 } my_enum;
 
   // expected to pass
-  pA: assert property (A == 1);
-  pB: assert property (B == 2);
-  pC: assert property (C == 3);
+  pA: assert final (A == 1);
+  pB: assert final (B == 2);
+  pC: assert final (C == 3);
 
 endmodule
diff --git a/regression/verilog/enums/enum_with_hierarchy1.sv b/regression/verilog/enums/enum_with_hierarchy1.sv
@@ -12,7 +12,7 @@ module main;
   sub #(1) sub1();
   sub #(2) sub2();
 
-  p1: assert property (sub1.E0 == 0 && sub1.E1 == 1 && sub1.E2 == 2);
-  p2: assert property (sub2.E0 == 0 && sub2.E2 == 2 && sub2.E2 == 4);
+  p1: assert final (sub1.E0 == 0 && sub1.E1 == 1 && sub1.E2 == 2);
+  p2: assert final (sub2.E0 == 0 && sub2.E2 == 2 && sub2.E2 == 4);
 
 endmodule
diff --git a/regression/verilog/expressions/bit-extract3.desc b/regression/verilog/expressions/bit-extract3.desc
@@ -3,10 +3,10 @@ bit-extract3.sv
 --module main --bound 0
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main\.property\.property1\] .*: PROVED up to bound 0$
-^\[main\.property\.property2\] .*: PROVED up to bound 0$
-^\[main\.property\.property3\] .*: PROVED up to bound 0$
-^\[main\.property\.property4\] .*: PROVED up to bound 0$
-^\[main\.property\.property5\] .*: PROVED up to bound 0$
+^\[main\.property1\] .*: PROVED up to bound 0$
+^\[main\.property2\] .*: PROVED up to bound 0$
+^\[main\.property3\] .*: PROVED up to bound 0$
+^\[main\.property4\] .*: PROVED up to bound 0$
+^\[main\.property5\] .*: PROVED up to bound 0$
 --
 ^warning: ignoring
diff --git a/regression/verilog/expressions/bit-extract3.sv b/regression/verilog/expressions/bit-extract3.sv
@@ -4,10 +4,10 @@ module main;
 
   // 1800-2017 sec 11.5.1: out-of-bounds bit-select is
   // x for 4-state and 0 for 2-state values.
-  always assert property1: x[7] == 1;
-  always assert property2: x[8] == 0;
-  always assert property3: x[-1] == 0;
-  always assert property4: x[8:7] == 1;
-  always assert property5: x[8:-1] == 'b0111111110;
+  property1: assert final (x[7] == 1);
+  property2: assert final (x[8] == 0);
+  property3: assert final (x[-1] == 0);
+  property4: assert final (x[8:7] == 1);
+  property5: assert final (x[8:-1] == 'b0111111110);
 
 endmodule
diff --git a/regression/verilog/expressions/bit-extract4.sv b/regression/verilog/expressions/bit-extract4.sv
@@ -2,6 +2,6 @@ module main;
 
   wire integer x = 'hff;
 
-  p0: assert property (x[7] == 1);
+  p0: assert final (x[7] == 1);
 
 endmodule
diff --git a/regression/verilog/expressions/bit-extract5.sv b/regression/verilog/expressions/bit-extract5.sv
@@ -5,9 +5,9 @@ module main;
   wire [0:31] w3 = 'b1;
   wire [1:32] w4 = 'b1;
 
-  p0: assert property (w1[0] and !w1[31]);
-  p1: assert property (w2[1] and !w2[32]);
-  p2: assert property (w3[31] and !w3[0]);
-  p3: assert property (w4[32] and !w4[1]);
+  p0: assert final (w1[0] && !w1[31]);
+  p1: assert final (w2[1] && !w2[32]);
+  p2: assert final (w3[31] && !w3[0]);
+  p3: assert final (w4[32] && !w4[1]);
 
 endmodule
diff --git a/regression/verilog/expressions/bit-extract6.sv b/regression/verilog/expressions/bit-extract6.sv
@@ -5,9 +5,9 @@ module main;
 
   // Non-constant index.
   // Note that index 8 is the least significant bit.
-  p0: assert property (index == 8 |-> vector[index] == 1);
+  p0: assert final (index == 8 -> vector[index] == 1);
 
   // Verilog guarantees that any out-of-bounds access is zero.
-  p1: assert property (index >= 1 && index <= 7 |-> vector[index] == 0);
+  p1: assert final (index >= 1 && index <= 7 -> vector[index] == 0);
 
 endmodule
diff --git a/regression/verilog/expressions/size_cast1.sv b/regression/verilog/expressions/size_cast1.sv
@@ -2,8 +2,8 @@ module main;
 
   parameter P = 20;
 
-  p0: assert property ($bits(10'(1)) == 10);
-  p1: assert property ($bits(P'(1)) == 20);
-  p2: assert property (10'(-1) == -1);
+  p0: assert final ($bits(10'(1)) == 10);
+  p1: assert final ($bits(P'(1)) == 20);
+  p2: assert final (10'(-1) == -1);
 
 endmodule
diff --git a/regression/verilog/expressions/static_cast1.sv b/regression/verilog/expressions/static_cast1.sv
@@ -2,6 +2,6 @@ module main;
 
   typedef bit [7:0] eight_bits;
 
-  p0: assert property (eight_bits'('hffff) == 'hff);
+  p0: assert final (eight_bits'('hffff) == 'hff);
 
 endmodule
diff --git a/regression/verilog/let/let1.sv b/regression/verilog/let/let1.sv
@@ -3,18 +3,18 @@
 module main;
 
   let some_let = 8'd123;
-  p0: assert property (some_let == 123 && $bits(some_let) == 8);
+  p0: assert final (some_let == 123 && $bits(some_let) == 8);
 
   // The standard doesn't say, but we allow these to be elaboration-time
   // constants.
   parameter some_parameter = some_let;
 
-  p1: assert property (some_parameter == 123 && $bits(some_parameter) == 8);
+  p1: assert final (some_parameter == 123 && $bits(some_parameter) == 8);
 
   // May depend on state.
   wire some_wire;
   let some_let_eq_wire = some_wire;
 
-  p2: assert property (some_let_eq_wire == some_wire);
+  p2: assert final (some_let_eq_wire == some_wire);
 
 endmodule
diff --git a/regression/verilog/let/let_ports1.sv b/regression/verilog/let/let_ports1.sv
@@ -3,6 +3,6 @@
 module main;
 
   let some_let_with_port(x) = x + 1;
-  p0: assert property (some_let_with_port(1) == 2);
+  p0: assert final (some_let_with_port(1) == 2);
 
 endmodule
diff --git a/regression/verilog/modules/parameter_ports4.sv b/regression/verilog/modules/parameter_ports4.sv
@@ -8,6 +8,6 @@ module main;
 
   sub #(byte) submodule();
 
-  p1: assert property ($bits(submodule.my_var) == 8);
+  p1: assert final ($bits(submodule.my_var) == 8);
 
 endmodule // main
diff --git a/regression/verilog/modules/parameters7.sv b/regression/verilog/modules/parameters7.sv
@@ -4,15 +4,15 @@ module main;
   // unless specified otherwise.
 
   parameter p1 = 8'h13;
-  assert property ($bits(p1) == 8);
+  assert final ($bits(p1) == 8);
 
   parameter p2 = 'h13;
-  assert property ($bits(p2) == 32);
+  assert final ($bits(p2) == 32);
 
   parameter [9:0] p3 = 'h13;
-  assert property ($bits(p3) == 10);
+  assert final ($bits(p3) == 10);
 
   parameter unsigned [31:0] p4 = -1;
-  assert property (p4 == 'hffffffff);
+  assert final (p4 == 'hffffffff);
 
 endmodule
diff --git a/regression/verilog/modules/ports5.sv b/regression/verilog/modules/ports5.sv
@@ -1,6 +1,6 @@
 // Ports may use SystemVerilog datatypes.
 module main(input logic [31:0] data);
 
-  always assert property1: $bits(data) == 32;
+  always assert final1: $bits(data) == 32;
 
 endmodule
diff --git a/regression/verilog/modules/type_parameters1.sv b/regression/verilog/modules/type_parameters1.sv
@@ -3,7 +3,7 @@ module main;
   parameter type T1 = bit;
   localparam type T2 = bit [31:0];
 
-  p1: assert property ($bits(T1) == 1);
-  p2: assert property ($bits(T2) == 32);
+  p1: assert final ($bits(T1) == 1);
+  p2: assert final ($bits(T2) == 32);
 
 endmodule
diff --git a/regression/verilog/modules/variable_module_port1.sv b/regression/verilog/modules/variable_module_port1.sv
@@ -12,6 +12,6 @@ module main;
 
   wire [7:0] comp = data0 + 1;
 
-  always assert property1: data1 == comp;
+  always assert final1: data1 == comp;
 
 endmodule
diff --git a/regression/verilog/part-select/indexed-part-select1.sv b/regression/verilog/part-select/indexed-part-select1.sv
@@ -9,6 +9,6 @@ module main(in);
     out[16 +: 16]=0;
   end
 
-  p1: assert property ({ in, { 8 { 1'b0 }} } == out);
+  p1: assert final ({ in, { 8 { 1'b0 }} } == out);
 
 endmodule
diff --git a/regression/verilog/part-select/indexed-part-select3.sv b/regression/verilog/part-select/indexed-part-select3.sv
@@ -4,6 +4,6 @@ module main(input [7:0] in, input [2:0] where);
   // does not need to be constant.
   wire out = in[where +: 1];
 
-  p0: assert property (out == in[where]);
+  p0: assert final (out == in[where]);
 
 endmodule
diff --git a/regression/verilog/synthesis/always_comb1.sv b/regression/verilog/synthesis/always_comb1.sv
diff --git a/regression/verilog/synthesis/always_comb2.sv b/regression/verilog/synthesis/always_comb2.sv
diff --git a/regression/verilog/synthesis/continuous_assignment_to_variable_systemverilog.sv b/regression/verilog/synthesis/continuous_assignment_to_variable_systemverilog.sv
diff --git a/regression/verilog/system-functions/array_functions1.sv b/regression/verilog/system-functions/array_functions1.sv
diff --git a/regression/verilog/typedef/global_typedef.sv b/regression/verilog/typedef/global_typedef.sv
diff --git a/regression/verilog/typedef/typedef1.sv b/regression/verilog/typedef/typedef1.sv
diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h
diff --git a/src/verilog/parser.y b/src/verilog/parser.y
diff --git a/src/verilog/verilog_elaborate.cpp b/src/verilog/verilog_elaborate.cpp
diff --git a/src/verilog/verilog_expr.h b/src/verilog/verilog_expr.h
diff --git a/src/verilog/verilog_interfaces.cpp b/src/verilog/verilog_interfaces.cpp
diff --git a/src/verilog/verilog_synthesis.cpp b/src/verilog/verilog_synthesis.cpp
diff --git a/src/verilog/verilog_synthesis_class.h b/src/verilog/verilog_synthesis_class.h
diff --git a/src/verilog/verilog_typecheck.cpp b/src/verilog/verilog_typecheck.cpp
