Skip to content

Commit

Permalink
Verilog: fix for synthesis of continuous assignments
Browse files Browse the repository at this point in the history
The LHS expression of continuous assignments needs to be synthesized.
  • Loading branch information
kroening committed Oct 18, 2024
1 parent 88a0e54 commit c9e186e
Show file tree
Hide file tree
Showing 7 changed files with 61 additions and 4 deletions.
7 changes: 7 additions & 0 deletions regression/verilog/synthesis/continuous_assignment1.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
CORE
continuous_assignment1.sv
--module main --bound 0
^EXIT=0$
^SIGNAL=0$
--
^warning: ignoring
9 changes: 9 additions & 0 deletions regression/verilog/synthesis/continuous_assignment1.sv
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
module main;

wire [31:0] a;
assign a[7:0] = 1;
assign a[8+:24] = 1;

assert final (a == 'h101);

endmodule
7 changes: 7 additions & 0 deletions regression/verilog/synthesis/continuous_assignment2.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
CORE
continuous_assignment2.sv
--module main --bound 0
^EXIT=0$
^SIGNAL=0$
--
^warning: ignoring
15 changes: 15 additions & 0 deletions regression/verilog/synthesis/continuous_assignment2.sv
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
module main;

typedef struct {
bit [31:0] f1, f2;
} my_struct;

wire my_struct s;

assign s.f1 = 1;
assign s.f2 = 2;

assert final (s.f1 == 1);
assert final (s.f2 == 2);

endmodule
7 changes: 7 additions & 0 deletions regression/verilog/synthesis/continuous_assignment3.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
CORE
continuous_assignment3.sv
--module main --bound 0
^EXIT=0$
^SIGNAL=0$
--
^warning: ignoring
11 changes: 11 additions & 0 deletions regression/verilog/synthesis/continuous_assignment3.sv
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
module main;

wire [31:0] array[10];

assign array[0] = 0;
assign array[1] = 1;

assert final (array[0] == 0);
assert final (array[1] == 1);

endmodule
9 changes: 5 additions & 4 deletions src/verilog/verilog_synthesis.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -2439,8 +2439,6 @@ void verilog_synthesist::synth_force_rec(
else
DATA_INVARIANT(false, "unexpected assignment type");

auto rhs_synth = synth_expr(rhs, symbol_statet::CURRENT);

// If the symbol is marked as a state variable,
// turn it into a wire now.
if(symbol.is_state_var)
Expand All @@ -2451,8 +2449,11 @@ void verilog_synthesist::synth_force_rec(
writeable_symbol.is_state_var = false;
}

equal_exprt equality{lhs, rhs_synth};
invars.push_back(equality);
auto lhs_synth = synth_expr(lhs, symbol_statet::CURRENT);
auto rhs_synth = synth_expr(rhs, symbol_statet::CURRENT);

equal_exprt equality{std::move(lhs_synth), std::move(rhs_synth)};
invars.push_back(std::move(equality));
}

/*******************************************************************\
Expand Down

0 comments on commit c9e186e

Please sign in to comment.