Skip to content

Commit 0a2ebe5

Browse files
kroeningkroening
committed
SVA: replace sva_sequence_concatenation_exprt
This replaces the sva_sequence_concatenation_exprt by multi-operand variants of sva_cycle_delay_exprt, sva_cycle_delay_plus_exprt and sva_cycle_delay_star_exprt. This simplifies the implementation of the SystemVerilog concatenation rules.
1 parent 8f220ab commit 0a2ebe5

File tree

7 files changed

+10
-100
lines changed

7 files changed

+10
-100
lines changed

‎src/hw_cbmc_irep_ids.h

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -60,7 +60,6 @@ IREP_ID_ONE(sva_cycle_delay)
6060
IREP_ID_ONE(sva_cycle_delay_star)
6161
IREP_ID_ONE(sva_cycle_delay_plus)
6262
IREP_ID_ONE(sva_disable_iff)
63-
IREP_ID_ONE(sva_sequence_concatenation)
6463
IREP_ID_ONE(sva_sequence_first_match)
6564
IREP_ID_ONE(sva_sequence_goto_repetition)
6665
IREP_ID_ONE(sva_sequence_intersect)

‎src/trans-word-level/sequence.cpp

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -160,6 +160,7 @@ sequence_matchest instantiate_sequence(
160160
return instantiate_sequence(
161161
cycle_delay_plus.lower(), semantics, t, no_timeframes);
162162
}
163+
#if 0
163164
else if(expr.id() == ID_sva_sequence_concatenation)
164165
{
165166
auto &implication = to_binary_expr(expr);
@@ -196,6 +197,7 @@ sequence_matchest instantiate_sequence(
196197

197198
return result;
198199
}
200+
#endif
199201
else if(expr.id() == ID_sva_sequence_intersect)
200202
{
201203
// IEEE 1800-2017 16.9.6

‎src/verilog/expr2verilog.cpp

Lines changed: 0 additions & 56 deletions
Original file line numberDiff line numberDiff line change
@@ -214,47 +214,6 @@ expr2verilogt::resultt expr2verilogt::convert_sva_cycle_delay(
214214

215215
/*******************************************************************\
216216
217-
Function: expr2verilogt::convert_sva_sequence_concatenation
218-
219-
Inputs:
220-
221-
Outputs:
222-
223-
Purpose:
224-
225-
\*******************************************************************/
226-
227-
expr2verilogt::resultt expr2verilogt::convert_sva_sequence_concatenation(
228-
const binary_exprt &src,
229-
verilog_precedencet precedence)
230-
{
231-
if(src.operands().size()!=2)
232-
return convert_norep(src);
233-
234-
std::string dest;
235-
236-
auto op0 = convert_rec(src.op0());
237-
auto op1 = convert_rec(src.op1());
238-
239-
if(precedence > op0.p)
240-
dest += '(';
241-
dest += op0.s;
242-
if(precedence > op0.p)
243-
dest += ')';
244-
245-
dest+=' ';
246-
247-
if(precedence > op0.p)
248-
dest += '(';
249-
dest += op1.s;
250-
if(precedence > op0.p)
251-
dest += ')';
252-
253-
return {precedence, dest};
254-
}
255-
256-
/*******************************************************************\
257-
258217
Function: expr2verilogt::convert_sva_sequence_first_match
259218
260219
Inputs:
@@ -1861,11 +1820,6 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src)
18611820
return convert_rec(to_sva_boolean_expr(src).op());
18621821
}
18631822

1864-
else if(src.id()==ID_sva_sequence_concatenation)
1865-
return convert_sva_sequence_concatenation(
1866-
to_binary_expr(src), precedence = verilog_precedencet::MIN);
1867-
// not sure about precedence
1868-
18691823
else if(src.id() == ID_sva_sequence_first_match)
18701824
return convert_sva_sequence_first_match(
18711825
to_sva_sequence_first_match_expr(src));
@@ -1885,16 +1839,6 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src)
18851839
convert_sva_binary("within", to_binary_expr(src));
18861840
// not sure about precedence
18871841

1888-
else if(src.id() == ID_sva_sequence_within)
1889-
return convert_sva_sequence_concatenation(
1890-
to_binary_expr(src), precedence = verilog_precedencet::MIN);
1891-
// not sure about precedence
1892-
1893-
else if(src.id() == ID_sva_sequence_throughout)
1894-
return convert_sva_sequence_concatenation(
1895-
to_binary_expr(src), precedence = verilog_precedencet::MIN);
1896-
// not sure about precedence
1897-
18981842
else if(src.id()==ID_sva_always)
18991843
return precedence = verilog_precedencet::MIN,
19001844
convert_sva_unary("always", to_sva_always_expr(src));

‎src/verilog/expr2verilog_class.h

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -161,9 +161,6 @@ class expr2verilogt
161161

162162
resultt convert_sva_if(const sva_if_exprt &);
163163

164-
resultt
165-
convert_sva_sequence_concatenation(const binary_exprt &, verilog_precedencet);
166-
167164
resultt
168165
convert_sva_sequence_first_match(const sva_sequence_first_match_exprt &);
169166

‎src/verilog/parser.y

Lines changed: 8 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -2538,11 +2538,10 @@ property_expr_proper:
25382538
mto($$, $2); }
25392539
// requires sequence_expr on the LHS
25402540
| property_expr cycle_delay_range sequence_expr %prec "##"
2541-
{ init($$, ID_sva_sequence_concatenation);
2542-
mto($$, $1);
2543-
stack_expr($2).operands().insert(stack_expr($2).operands().begin(), nil_exprt());
2544-
mto($2, $3);
2545-
mto($$, $2); }
2541+
{ $$=$2;
2542+
// preserve the operand ordering as in the source code
2543+
stack_expr($$).operands().insert(stack_expr($1).operands().begin(), stack_expr($1));
2544+
mto($$, $3); }
25462545
// requires sequence_expr on the LHS
25472546
| '(' property_expr_proper ')' sequence_abbrev
25482547
{ $$ = $4;
@@ -2646,11 +2645,10 @@ sequence_expr_proper:
26462645
stack_expr($$).operands().insert(stack_expr($$).operands().begin(), nil_exprt());
26472646
mto($$, $2); }
26482647
| sequence_expr cycle_delay_range sequence_expr %prec "##"
2649-
{ init($$, ID_sva_sequence_concatenation);
2650-
mto($$, $1);
2651-
stack_expr($2).operands().insert(stack_expr($2).operands().begin(), nil_exprt());
2652-
mto($2, $3);
2653-
mto($$, $2); }
2648+
{ $$=$2;
2649+
// preserve the operand ordering as in the source code
2650+
stack_expr($$).operands().insert(stack_expr($1).operands().begin(), stack_expr($1));
2651+
mto($$, $3); }
26542652
| '(' sequence_expr_proper ')'
26552653
{ $$ = $2; }
26562654
| '(' sequence_expr_proper ')' sequence_abbrev

‎src/verilog/sva_expr.h

Lines changed: 0 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -861,35 +861,6 @@ static inline sva_and_exprt &to_sva_and_expr(exprt &expr)
861861
return static_cast<sva_and_exprt &>(expr);
862862
}
863863

864-
class sva_sequence_concatenation_exprt : public binary_exprt
865-
{
866-
public:
867-
explicit sva_sequence_concatenation_exprt(exprt op0, exprt op1)
868-
: binary_exprt(
869-
std::move(op0),
870-
ID_sva_sequence_concatenation,
871-
std::move(op1),
872-
verilog_sva_sequence_typet{})
873-
{
874-
}
875-
};
876-
877-
static inline const sva_sequence_concatenation_exprt &
878-
to_sva_sequence_concatenation_expr(const exprt &expr)
879-
{
880-
PRECONDITION(expr.id() == ID_sva_sequence_concatenation);
881-
sva_sequence_concatenation_exprt::check(expr, validation_modet::INVARIANT);
882-
return static_cast<const sva_sequence_concatenation_exprt &>(expr);
883-
}
884-
885-
static inline sva_sequence_concatenation_exprt &
886-
to_sva_sequence_concatenation_expr(exprt &expr)
887-
{
888-
PRECONDITION(expr.id() == ID_sva_sequence_concatenation);
889-
sva_sequence_concatenation_exprt::check(expr, validation_modet::INVARIANT);
890-
return static_cast<sva_sequence_concatenation_exprt &>(expr);
891-
}
892-
893864
class sva_iff_exprt : public binary_predicate_exprt
894865
{
895866
public:

‎src/verilog/verilog_typecheck_sva.cpp

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -231,7 +231,6 @@ exprt verilog_typecheck_exprt::convert_binary_sva(binary_exprt expr)
231231
return std::move(expr);
232232
}
233233
else if(
234-
expr.id() == ID_sva_sequence_concatenation || // a ##b c
235234
expr.id() == ID_sva_sequence_intersect ||
236235
expr.id() == ID_sva_sequence_within)
237236
{

0 commit comments

Comments
 (0)