diff --git a/regression/verilog/arrays/array_literal1.desc b/regression/verilog/arrays/array_literal1.desc new file mode 100644 index 000000000..6bc2b4d42 --- /dev/null +++ b/regression/verilog/arrays/array_literal1.desc @@ -0,0 +1,6 @@ +CORE +array_literal1.sv +--bound 0 +^EXIT=0$ +^SIGNAL=0$ +-- diff --git a/regression/verilog/arrays/array_literal1.sv b/regression/verilog/arrays/array_literal1.sv new file mode 100644 index 000000000..1dea0aa46 --- /dev/null +++ b/regression/verilog/arrays/array_literal1.sv @@ -0,0 +1,8 @@ +module main; + + reg [7:0] my_array[10] = '{1, 2, 3, 4, 5, 6, 7, 8, 9, 10}; + + initial p0: assert property (my_array[0] == 1); + initial p1: assert property (my_array[9] == 10); + +endmodule diff --git a/regression/verilog/arrays/array_literal2.desc b/regression/verilog/arrays/array_literal2.desc new file mode 100644 index 000000000..5c610876a --- /dev/null +++ b/regression/verilog/arrays/array_literal2.desc @@ -0,0 +1,8 @@ +CORE +array_literal2.sv + +^file array_literal2\.sv line 3: number of expressions does not match number of array elements$ +^CONVERSION ERROR$ +^EXIT=2$ +^SIGNAL=0$ +-- diff --git a/regression/verilog/arrays/array_literal2.sv b/regression/verilog/arrays/array_literal2.sv new file mode 100644 index 000000000..50248eed2 --- /dev/null +++ b/regression/verilog/arrays/array_literal2.sv @@ -0,0 +1,5 @@ +module main; + + reg [7:0] my_array[10] = '{1, 2, 3, 4}; // too short + +endmodule diff --git a/regression/verilog/structs/structs5.desc b/regression/verilog/structs/structs5.desc new file mode 100644 index 000000000..366d29391 --- /dev/null +++ b/regression/verilog/structs/structs5.desc @@ -0,0 +1,9 @@ +CORE +structs5.sv +--bound 0 +^\[main\.p1\] always main\.s\.field1 == 1: PROVED up to bound 0$ +^\[main\.p2\] always main\.s\.field2 == 0: PROVED up to bound 0$ +^\[main\.p3\] always main\.s\.field3 == 115: PROVED up to bound 0$ +^EXIT=0$ +^SIGNAL=0$ +-- diff --git a/regression/verilog/structs/structs5.sv b/regression/verilog/structs/structs5.sv new file mode 100644 index 000000000..cf6fdee63 --- /dev/null +++ b/regression/verilog/structs/structs5.sv @@ -0,0 +1,13 @@ +module main; + + struct packed { + bit field1, field2; + bit [6:0] field3; + } s = '{ 1, 0, 'b1110011 }; + + // Expected to pass. + p1: assert property (s.field1 == 1); + p2: assert property (s.field2 == 0); + p3: assert property (s.field3 == 'b1110011); + +endmodule diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h index 98efbdb36..acf36036b 100644 --- a/src/hw_cbmc_irep_ids.h +++ b/src/hw_cbmc_irep_ids.h @@ -50,6 +50,7 @@ IREP_ID_TWO(C_little_endian, #little_endian) IREP_ID_ONE(ports) IREP_ID_ONE(inst) IREP_ID_ONE(Verilog) +IREP_ID_ONE(verilog_assignment_pattern) IREP_ID_ONE(verilog_explicit_cast) IREP_ID_ONE(verilog_size_cast) IREP_ID_ONE(verilog_implicit_typecast) diff --git a/src/verilog/parser.y b/src/verilog/parser.y index d655733ea..76a431e9f 100644 --- a/src/verilog/parser.y +++ b/src/verilog/parser.y @@ -3042,6 +3042,18 @@ case_item: mto($$, $2); } ; +// System Verilog standard 1800-2017 +// A.6.7.1 Patterns + +assignment_pattern: + '\'' '{' expression_brace '}' + { init($$, ID_verilog_assignment_pattern); swapop($$, $3); } + ; + +assignment_pattern_expression: + assignment_pattern + ; + // System Verilog standard 1800-2017 // A.6.8 Looping statements @@ -3364,6 +3376,7 @@ primary: primary_literal | '(' mintypmax_expression ')' { $$ = $2; } | cast + | assignment_pattern_expression | TOK_NULL { init($$, ID_NULL); } ; diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp index cc9c93b5e..1c72802c7 100644 --- a/src/verilog/verilog_typecheck_expr.cpp +++ b/src/verilog/verilog_typecheck_expr.cpp @@ -318,6 +318,20 @@ exprt verilog_typecheck_exprt::convert_expr_rec(exprt expr) { return convert_expr_function_call(to_function_call_expr(expr)); } + else if(expr.id() == ID_verilog_assignment_pattern) + { + // multi-ary -- may become a struct or array, depending + // on context. + for(auto &op : expr.operands()) + convert_expr(op); + + // Typechecking can only be completed once we know the type + // from the usage context. We record "verilog_assignment_pattern" + // to signal that. + expr.type() = typet(ID_verilog_assignment_pattern); + + return expr; + } else { std::size_t no_op; @@ -1814,6 +1828,64 @@ void verilog_typecheck_exprt::implicit_typecast( return; } } + else if(src_type.id() == ID_verilog_assignment_pattern) + { + DATA_INVARIANT( + expr.id() == ID_verilog_assignment_pattern, + "verilog_assignment_pattern expression expected"); + if(dest_type.id() == ID_struct) + { + auto &struct_type = to_struct_type(dest_type); + auto &components = struct_type.components(); + + if(expr.operands().size() != components.size()) + { + throw errort().with_location(expr.source_location()) + << "number of expressions does not match number of struct members"; + } + + for(std::size_t i = 0; i < components.size(); i++) + { + // rec. call + implicit_typecast(expr.operands()[i], components[i].type()); + } + + // turn into struct expression + expr.id(ID_struct); + expr.type() = dest_type; + return; + } + else if(dest_type.id() == ID_array) + { + auto &array_type = to_array_type(dest_type); + auto &element_type = array_type.element_type(); + auto array_size = + numeric_cast_v(to_constant_expr(array_type.size())); + + if(array_size != expr.operands().size()) + { + throw errort().with_location(expr.source_location()) + << "number of expressions does not match number of array elements"; + } + + for(std::size_t i = 0; i < array_size; i++) + { + // rec. call + implicit_typecast(expr.operands()[i], element_type); + } + + // turn into array expression + expr.id(ID_array); + expr.type() = dest_type; + return; + } + else + { + throw errort().with_location(expr.source_location()) + << "cannot convert assignment pattern to '" << to_string(dest_type) + << '\''; + } + } throw errort().with_location(expr.source_location()) << "failed to convert `" << to_string(src_type) << "' to `"