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 08fc073
Show file tree
Hide file tree
Showing 7 changed files with 60 additions and 3 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
7 changes: 4 additions & 3 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,7 +2449,10 @@ void verilog_synthesist::synth_force_rec(
writeable_symbol.is_state_var = false;
}

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

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

Expand Down

0 comments on commit 08fc073

Please sign in to comment.