Skip to content

Commit 80c64af

Browse files
tautschnigtautschnig
authored
Merge pull request #600 from diffblue/verilog_blocking_assign
SystemVerilog: compound blocking assignments
2 parents 23f9838 + f0258f4 commit 80c64af

File tree

9 files changed

+143
-58
lines changed

9 files changed

+143
-58
lines changed

‎regression/verilog/assignments/procedural_assignments1.desc‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,8 @@
1-
KNOWNBUG
1+
CORE
22
procedural_assignments1.sv
33
--bound 0
44
^EXIT=0$
55
^SIGNAL=0$
66
--
77
^warning: ignoring
88
--
9-
The += assignment is broken.

‎src/hw_cbmc_irep_ids.h‎

Lines changed: 14 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -88,8 +88,20 @@ IREP_ID_ONE(event_guard)
8888
IREP_ID_ONE(verilog_star_event)
8989
IREP_ID_ONE(verilog_cycle_delay)
9090
IREP_ID_ONE(delay)
91-
IREP_ID_ONE(non_blocking_assign)
92-
IREP_ID_ONE(blocking_assign)
91+
IREP_ID_ONE(verilog_non_blocking_assign)
92+
IREP_ID_ONE(verilog_blocking_assign)
93+
IREP_ID_ONE(verilog_blocking_assign_plus)
94+
IREP_ID_ONE(verilog_blocking_assign_minus)
95+
IREP_ID_ONE(verilog_blocking_assign_mult)
96+
IREP_ID_ONE(verilog_blocking_assign_div)
97+
IREP_ID_ONE(verilog_blocking_assign_mod)
98+
IREP_ID_ONE(verilog_blocking_assign_bitand)
99+
IREP_ID_ONE(verilog_blocking_assign_bitor)
100+
IREP_ID_ONE(verilog_blocking_assign_bitxor)
101+
IREP_ID_ONE(verilog_blocking_assign_lshr)
102+
IREP_ID_ONE(verilog_blocking_assign_lshl)
103+
IREP_ID_ONE(verilog_blocking_assign_ashr)
104+
IREP_ID_ONE(verilog_blocking_assign_ashl)
93105
IREP_ID_ONE(release)
94106
IREP_ID_ONE(force)
95107
IREP_ID_ONE(deassign)

‎src/verilog/parser.y‎

Lines changed: 17 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -2759,36 +2759,49 @@ final_construct: TOK_FINAL function_statement
27592759

27602760
blocking_assignment:
27612761
variable_lvalue '=' delay_or_event_control expression
2762-
{ init($$, ID_blocking_assign); mto($$, $1); mto($$, $4); }
2762+
{ init($$, ID_verilog_blocking_assign); mto($$, $1); mto($$, $4); }
27632763
| operator_assignment
27642764
;
27652765

27662766
operator_assignment:
27672767
variable_lvalue assignment_operator expression
2768-
{ init($$, ID_blocking_assign); mto($$, $1); mto($$, $3); }
2768+
{ $$ = $2; mto($$, $1); mto($$, $3); }
27692769
;
27702770

27712771
assignment_operator:
27722772
'='
2773+
{ init($$, ID_verilog_blocking_assign); }
27732774
| TOK_PLUSEQUAL
2775+
{ init($$, ID_verilog_blocking_assign_plus); }
27742776
| TOK_MINUSEQUAL
2777+
{ init($$, ID_verilog_blocking_assign_minus); }
27752778
| TOK_ASTERICEQUAL
2779+
{ init($$, ID_verilog_blocking_assign_mult); }
27762780
| TOK_SLASHEQUAL
2781+
{ init($$, ID_verilog_blocking_assign_div); }
27772782
| TOK_PERCENTEQUAL
2783+
{ init($$, ID_verilog_blocking_assign_mod); }
27782784
| TOK_AMPEREQUAL
2785+
{ init($$, ID_verilog_blocking_assign_bitand); }
27792786
| TOK_VERTBAREQUAL
2787+
{ init($$, ID_verilog_blocking_assign_bitor); }
27802788
| TOK_CARETEQUAL
2789+
{ init($$, ID_verilog_blocking_assign_bitxor); }
27812790
| TOK_LESSLESSEQUAL
2791+
{ init($$, ID_verilog_blocking_assign_lshl); }
27822792
| TOK_GREATERGREATEREQUAL
2793+
{ init($$, ID_verilog_blocking_assign_lshr); }
27832794
| TOK_LESSLESSLESSEQUAL
2795+
{ init($$, ID_verilog_blocking_assign_ashl); }
27842796
| TOK_GREATERGREATERGREATEREQUAL
2797+
{ init($$, ID_verilog_blocking_assign_ashr); }
27852798
;
27862799

27872800
nonblocking_assignment:
27882801
variable_lvalue TOK_LESSEQUAL expression
2789-
{ init($$, ID_non_blocking_assign); mto($$, $1); mto($$, $3); }
2802+
{ init($$, ID_verilog_non_blocking_assign); mto($$, $1); mto($$, $3); }
27902803
| variable_lvalue TOK_LESSEQUAL delay_or_event_control expression
2791-
{ init($$, ID_non_blocking_assign); mto($$, $1); mto($$, $4); }
2804+
{ init($$, ID_verilog_non_blocking_assign); mto($$, $1); mto($$, $4); }
27922805
;
27932806

27942807
procedural_continuous_assignment:

‎src/verilog/verilog_elaborate.cpp‎

Lines changed: 15 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -648,7 +648,20 @@ void verilog_typecheckt::collect_symbols(const verilog_statementt &statement)
648648
if(block_statement.is_named())
649649
named_blocks.pop_back();
650650
}
651-
else if(statement.id() == ID_blocking_assign)
651+
else if(
652+
statement.id() == ID_verilog_blocking_assign ||
653+
statement.id() == ID_verilog_blocking_assign_plus ||
654+
statement.id() == ID_verilog_blocking_assign_minus ||
655+
statement.id() == ID_verilog_blocking_assign_mult ||
656+
statement.id() == ID_verilog_blocking_assign_div ||
657+
statement.id() == ID_verilog_blocking_assign_mod ||
658+
statement.id() == ID_verilog_blocking_assign_bitand ||
659+
statement.id() == ID_verilog_blocking_assign_bitor ||
660+
statement.id() == ID_verilog_blocking_assign_bitxor ||
661+
statement.id() == ID_verilog_blocking_assign_lshr ||
662+
statement.id() == ID_verilog_blocking_assign_lshl ||
663+
statement.id() == ID_verilog_blocking_assign_ashr ||
664+
statement.id() == ID_verilog_blocking_assign_ashl)
652665
{
653666
}
654667
else if(
@@ -695,7 +708,7 @@ void verilog_typecheckt::collect_symbols(const verilog_statementt &statement)
695708
if(if_statement.has_else_case())
696709
collect_symbols(if_statement.else_case());
697710
}
698-
else if(statement.id() == ID_non_blocking_assign)
711+
else if(statement.id() == ID_verilog_non_blocking_assign)
699712
{
700713
}
701714
else if(

‎src/verilog/verilog_expr.h‎

Lines changed: 8 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -1613,48 +1613,44 @@ inline verilog_assignt &to_verilog_assign(exprt &expr)
16131613
class verilog_blocking_assignt:public verilog_assignt
16141614
{
16151615
public:
1616-
verilog_blocking_assignt():verilog_assignt(ID_blocking_assign)
1617-
{
1618-
}
1619-
1620-
verilog_blocking_assignt(
1621-
const exprt &_lhs, const exprt &_rhs):
1622-
verilog_assignt(ID_blocking_assign, _lhs, _rhs)
1616+
verilog_blocking_assignt(const exprt &_lhs, const exprt &_rhs)
1617+
: verilog_assignt(ID_verilog_blocking_assign, _lhs, _rhs)
16231618
{
16241619
}
16251620
};
16261621

16271622
inline const verilog_blocking_assignt &
16281623
to_verilog_blocking_assign(const exprt &expr)
16291624
{
1630-
PRECONDITION(expr.id() == ID_blocking_assign);
1625+
PRECONDITION(expr.id() == ID_verilog_blocking_assign);
16311626
return static_cast<const verilog_blocking_assignt &>(expr);
16321627
}
16331628

16341629
inline verilog_blocking_assignt &to_verilog_blocking_assign(exprt &expr)
16351630
{
1636-
PRECONDITION(expr.id() == ID_blocking_assign);
1631+
PRECONDITION(expr.id() == ID_verilog_blocking_assign);
16371632
return static_cast<verilog_blocking_assignt &>(expr);
16381633
}
16391634

16401635
class verilog_non_blocking_assignt:public verilog_assignt
16411636
{
16421637
public:
1643-
verilog_non_blocking_assignt():verilog_assignt(ID_non_blocking_assign)
1638+
verilog_non_blocking_assignt()
1639+
: verilog_assignt(ID_verilog_non_blocking_assign)
16441640
{
16451641
}
16461642
};
16471643

16481644
inline const verilog_non_blocking_assignt &
16491645
to_verilog_non_blocking_assign(const exprt &expr)
16501646
{
1651-
PRECONDITION(expr.id() == ID_non_blocking_assign);
1647+
PRECONDITION(expr.id() == ID_verilog_non_blocking_assign);
16521648
return static_cast<const verilog_non_blocking_assignt &>(expr);
16531649
}
16541650

16551651
inline verilog_non_blocking_assignt &to_verilog_non_blocking_assign(exprt &expr)
16561652
{
1657-
PRECONDITION(expr.id() == ID_non_blocking_assign);
1653+
PRECONDITION(expr.id() == ID_verilog_non_blocking_assign);
16581654
return static_cast<verilog_non_blocking_assignt &>(expr);
16591655
}
16601656

‎src/verilog/verilog_interpreter.cpp‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -26,7 +26,7 @@ Function: verilog_typecheckt::verilog_interpreter
2626
void verilog_typecheckt::verilog_interpreter(
2727
const verilog_statementt &statement)
2828
{
29-
if(statement.id()==ID_blocking_assign)
29+
if(statement.id() == ID_verilog_blocking_assign)
3030
{
3131
const verilog_blocking_assignt &assign=
3232
to_verilog_blocking_assign(statement);

‎src/verilog/verilog_synthesis.cpp‎

Lines changed: 69 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -573,9 +573,8 @@ exprt verilog_synthesist::expand_function_call(const function_call_exprt &call)
573573
for(unsigned i=0; i<parameters.size(); i++)
574574
{
575575
const symbolt &a_symbol=ns.lookup(parameters[i].get_identifier());
576-
verilog_blocking_assignt assignment;
577-
assignment.lhs() = a_symbol.symbol_expr().with_source_location(call);
578-
assignment.rhs()=actuals[i];
576+
verilog_blocking_assignt assignment{
577+
a_symbol.symbol_expr().with_source_location(call), actuals[i]};
579578
assignment.add_source_location()=call.source_location();
580579
synth_statement(assignment);
581580
}
@@ -2266,33 +2265,60 @@ Function: verilog_synthesist::synth_assign
22662265
22672266
\*******************************************************************/
22682267

2269-
void verilog_synthesist::synth_assign(
2270-
const verilog_statementt &statement,
2271-
bool blocking)
2268+
void verilog_synthesist::synth_assign(const verilog_assignt &statement)
22722269
{
2273-
if(statement.operands().size()!=2)
2274-
{
2275-
throw errort().with_location(statement.source_location())
2276-
<< "assign statement expected to have two operands";
2277-
}
2278-
22792270
if(construct == constructt::OTHER)
22802271
{
22812272
throw errort().with_location(statement.source_location())
22822273
<< "unexpected assignment statement";
22832274
}
22842275

2285-
const exprt &lhs = to_binary_expr(statement).op0();
2286-
exprt rhs = to_binary_expr(statement).op1();
2276+
const exprt &lhs = statement.lhs();
2277+
exprt rhs = statement.rhs();
22872278

22882279
rhs = synth_expr(rhs, symbol_statet::CURRENT);
22892280

2281+
irep_idt compound_id = irep_idt{};
2282+
2283+
if(statement.id() == ID_verilog_blocking_assign_plus)
2284+
compound_id = ID_plus;
2285+
else if(statement.id() == ID_verilog_blocking_assign_minus)
2286+
compound_id = ID_minus;
2287+
else if(statement.id() == ID_verilog_blocking_assign_mult)
2288+
compound_id = ID_mult;
2289+
else if(statement.id() == ID_verilog_blocking_assign_div)
2290+
compound_id = ID_div;
2291+
else if(statement.id() == ID_verilog_blocking_assign_mod)
2292+
compound_id = ID_mod;
2293+
else if(statement.id() == ID_verilog_blocking_assign_bitand)
2294+
compound_id = ID_bitand;
2295+
else if(statement.id() == ID_verilog_blocking_assign_bitor)
2296+
compound_id = ID_bitor;
2297+
else if(statement.id() == ID_verilog_blocking_assign_bitxor)
2298+
compound_id = ID_bitxor;
2299+
else if(statement.id() == ID_verilog_blocking_assign_lshr)
2300+
compound_id = ID_lshr;
2301+
else if(statement.id() == ID_verilog_blocking_assign_lshl)
2302+
compound_id = ID_shl;
2303+
else if(statement.id() == ID_verilog_blocking_assign_ashr)
2304+
compound_id = ID_ashr;
2305+
else if(statement.id() == ID_verilog_blocking_assign_ashl)
2306+
compound_id = ID_shl;
2307+
2308+
if(compound_id != irep_idt{})
2309+
{
2310+
auto lhs_synth = synth_expr(lhs, symbol_statet::CURRENT);
2311+
rhs = binary_exprt{std::move(lhs_synth), compound_id, rhs, rhs.type()};
2312+
}
2313+
22902314
// Can the rhs be simplified to a constant, for propagation?
22912315
auto rhs_simplified = simplify_expr(rhs, ns);
22922316

22932317
if(rhs_simplified.is_constant())
22942318
rhs = rhs_simplified;
22952319

2320+
bool blocking = statement.id() != ID_verilog_non_blocking_assign;
2321+
22962322
assignment_rec(lhs, rhs, blocking);
22972323
}
22982324

@@ -2961,19 +2987,19 @@ void verilog_synthesist::synth_prepostincdec(const verilog_statementt &statement
29612987
// stupid implementation
29622988
exprt one = from_integer(1, op.type());
29632989

2964-
bool increment=
2965-
statement.id()==ID_preincrement ||
2966-
statement.id()==ID_postincrement;
2967-
2968-
verilog_blocking_assignt assignment;
2969-
assignment.lhs() = op;
2990+
bool increment =
2991+
statement.id() == ID_preincrement || statement.id() == ID_postincrement;
2992+
2993+
exprt rhs;
29702994

29712995
if(increment)
2972-
assignment.rhs() = plus_exprt(op, one);
2996+
rhs = plus_exprt(op, one);
29732997
else
2974-
assignment.rhs() = minus_exprt(op, one);
2998+
rhs = minus_exprt(op, one);
29752999

3000+
verilog_blocking_assignt assignment{op, rhs};
29763001
assignment.add_source_location()=statement.source_location();
3002+
29773003
synth_statement(assignment);
29783004
}
29793005

@@ -3126,9 +3152,7 @@ void verilog_synthesist::synth_function_call_or_task_enable(
31263152
const symbolt &a_symbol=ns.lookup(parameters[i].get_identifier());
31273153
if(parameters[i].get_bool(ID_input))
31283154
{
3129-
verilog_blocking_assignt assignment;
3130-
assignment.lhs()=a_symbol.symbol_expr();
3131-
assignment.rhs()=actuals[i];
3155+
verilog_blocking_assignt assignment{a_symbol.symbol_expr(), actuals[i]};
31323156
assignment.add_source_location()=statement.source_location();
31333157
synth_statement(assignment);
31343158
}
@@ -3142,9 +3166,7 @@ void verilog_synthesist::synth_function_call_or_task_enable(
31423166
const symbolt &a_symbol=ns.lookup(parameters[i].get_identifier());
31433167
if(parameters[i].get_bool(ID_output))
31443168
{
3145-
verilog_blocking_assignt assignment;
3146-
assignment.lhs()=actuals[i];
3147-
assignment.rhs()=a_symbol.symbol_expr();
3169+
verilog_blocking_assignt assignment{actuals[i], a_symbol.symbol_expr()};
31483170
assignment.add_source_location()=statement.source_location();
31493171
synth_statement(assignment);
31503172
}
@@ -3173,8 +3195,23 @@ void verilog_synthesist::synth_statement(
31733195
statement.id()==ID_casex ||
31743196
statement.id()==ID_casez)
31753197
synth_case(statement);
3176-
else if(statement.id()==ID_blocking_assign)
3177-
synth_assign(statement, true);
3198+
else if(
3199+
statement.id() == ID_verilog_blocking_assign ||
3200+
statement.id() == ID_verilog_blocking_assign_plus ||
3201+
statement.id() == ID_verilog_blocking_assign_minus ||
3202+
statement.id() == ID_verilog_blocking_assign_mult ||
3203+
statement.id() == ID_verilog_blocking_assign_div ||
3204+
statement.id() == ID_verilog_blocking_assign_mod ||
3205+
statement.id() == ID_verilog_blocking_assign_bitand ||
3206+
statement.id() == ID_verilog_blocking_assign_bitor ||
3207+
statement.id() == ID_verilog_blocking_assign_bitxor ||
3208+
statement.id() == ID_verilog_blocking_assign_lshr ||
3209+
statement.id() == ID_verilog_blocking_assign_lshl ||
3210+
statement.id() == ID_verilog_blocking_assign_ashr ||
3211+
statement.id() == ID_verilog_blocking_assign_ashl)
3212+
{
3213+
synth_assign(to_verilog_assign(statement));
3214+
}
31783215
else if(statement.id() == ID_procedural_continuous_assign)
31793216
{
31803217
throw errort().with_location(statement.source_location())
@@ -3202,8 +3239,8 @@ void verilog_synthesist::synth_statement(
32023239
throw errort().with_location(statement.source_location())
32033240
<< "synthesis of expect property not supported";
32043241
}
3205-
else if(statement.id()==ID_non_blocking_assign)
3206-
synth_assign(statement, false);
3242+
else if(statement.id() == ID_verilog_non_blocking_assign)
3243+
synth_assign(to_verilog_assign(statement));
32073244
else if(statement.id()==ID_force)
32083245
synth_force(to_verilog_force(statement));
32093246
else if(statement.id()==ID_if)

‎src/verilog/verilog_synthesis_class.h‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -263,7 +263,7 @@ class verilog_synthesist:
263263
void synth_while(const verilog_whilet &);
264264
void synth_repeat(const verilog_repeatt &);
265265
void synth_function_call_or_task_enable(const verilog_function_callt &);
266-
void synth_assign(const verilog_statementt &, bool blocking);
266+
void synth_assign(const verilog_assignt &);
267267
void
268268
synth_assert_assume_cover(const verilog_assert_assume_cover_statementt &);
269269
void synth_assume(const verilog_assume_statementt &);

‎src/verilog/verilog_typecheck.cpp‎

Lines changed: 17 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1449,8 +1449,23 @@ void verilog_typecheckt::convert_statement(
14491449
statement.id()==ID_casex ||
14501450
statement.id()==ID_casez)
14511451
convert_case(to_verilog_case_base(statement));
1452-
else if(statement.id()==ID_blocking_assign)
1452+
else if(
1453+
statement.id() == ID_verilog_blocking_assign ||
1454+
statement.id() == ID_verilog_blocking_assign_plus ||
1455+
statement.id() == ID_verilog_blocking_assign_minus ||
1456+
statement.id() == ID_verilog_blocking_assign_mult ||
1457+
statement.id() == ID_verilog_blocking_assign_div ||
1458+
statement.id() == ID_verilog_blocking_assign_mod ||
1459+
statement.id() == ID_verilog_blocking_assign_bitand ||
1460+
statement.id() == ID_verilog_blocking_assign_bitor ||
1461+
statement.id() == ID_verilog_blocking_assign_bitxor ||
1462+
statement.id() == ID_verilog_blocking_assign_lshr ||
1463+
statement.id() == ID_verilog_blocking_assign_lshl ||
1464+
statement.id() == ID_verilog_blocking_assign_ashr ||
1465+
statement.id() == ID_verilog_blocking_assign_ashl)
1466+
{
14531467
convert_assign(to_verilog_assign(statement), true);
1468+
}
14541469
else if(statement.id() == ID_procedural_continuous_assign)
14551470
convert_procedural_continuous_assign(
14561471
to_verilog_procedural_continuous_assign(statement));
@@ -1476,7 +1491,7 @@ void verilog_typecheckt::convert_statement(
14761491
else if(statement.id() == ID_verilog_cover_property)
14771492
{
14781493
}
1479-
else if(statement.id()==ID_non_blocking_assign)
1494+
else if(statement.id() == ID_verilog_non_blocking_assign)
14801495
convert_assign(to_verilog_assign(statement), false);
14811496
else if(statement.id()==ID_if)
14821497
convert_if(to_verilog_if(statement));

0 commit comments

Comments
 (0)