Skip to content

Commit 9699e89

Browse files
kroeningkroening
committed
SVA: add cover sequence
1800-2012 has introduced the cover sequence statement, in addition to the cover property statement.
1 parent 7fe06e4 commit 9699e89

16 files changed

+171
-29
lines changed

‎CHANGELOG‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,7 @@
11
# EBMC 5.8
22

3+
* SystemVerilog: cover sequence
4+
35
# EBMC 5.7
46

57
* Verilog: --initial-zero changes the default value from nondet to zero

‎regression/verilog/SVA/cover_sequence1.sv‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -7,9 +7,9 @@ module main(input clk);
77
x++;
88

99
// expected to pass
10-
p0: cover property (x==2 ##1 x==3 ##1 x==4);
10+
p0: cover sequence (x==2 ##1 x==3 ##1 x==4);
1111

1212
// expected to fail
13-
p1: cover property (x==2 ##1 x==3 ##1 x==5);
13+
p1: cover sequence (x==2 ##1 x==3 ##1 x==5);
1414

1515
endmodule

‎src/hw_cbmc_irep_ids.h‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -69,6 +69,7 @@ IREP_ID_ONE(sva_cycle_delay)
6969
IREP_ID_ONE(sva_cycle_delay_star)
7070
IREP_ID_ONE(sva_cycle_delay_plus)
7171
IREP_ID_ONE(sva_disable_iff)
72+
IREP_ID_ONE(sva_sequence_disable_iff)
7273
IREP_ID_ONE(sva_sequence_first_match)
7374
IREP_ID_ONE(sva_sequence_goto_repetition)
7475
IREP_ID_ONE(sva_sequence_intersect)
@@ -210,6 +211,7 @@ IREP_ID_ONE(verilog_immediate_cover)
210211
IREP_ID_ONE(verilog_assert_property)
211212
IREP_ID_ONE(verilog_assume_property)
212213
IREP_ID_ONE(verilog_cover_property)
214+
IREP_ID_ONE(verilog_cover_sequence)
213215
IREP_ID_ONE(verilog_covergroup)
214216
IREP_ID_ONE(verilog_restrict_property)
215217
IREP_ID_ONE(verilog_expect_property)

‎src/temporal-logic/temporal_logic.cpp‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -112,7 +112,8 @@ bool is_SVA_sequence_operator(const exprt &expr)
112112
id == ID_sva_sequence_goto_repetition ||
113113
id == ID_sva_sequence_non_consecutive_repetition ||
114114
id == ID_sva_sequence_repetition_star ||
115-
id == ID_sva_sequence_repetition_plus || id == ID_sva_boolean;
115+
id == ID_sva_sequence_repetition_plus || id == ID_sva_boolean ||
116+
id == ID_sva_sequence_disable_iff;
116117
}
117118

118119
bool is_SVA_operator(const exprt &expr)

‎src/temporal-logic/trivial_sva.cpp‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -110,6 +110,14 @@ exprt trivial_sva(exprt expr)
110110
auto &disable_iff_expr = to_sva_disable_iff_expr(expr);
111111
expr = or_exprt{disable_iff_expr.lhs(), disable_iff_expr.rhs()};
112112
}
113+
else if(expr.id() == ID_sva_sequence_disable_iff)
114+
{
115+
auto &disable_iff_expr = to_sva_sequence_disable_iff_expr(expr);
116+
expr = sva_or_exprt{
117+
sva_boolean_exprt{disable_iff_expr.lhs(), verilog_sva_sequence_typet{}},
118+
disable_iff_expr.rhs(),
119+
verilog_sva_sequence_typet{}};
120+
}
113121
else if(expr.id() == ID_sva_accept_on || expr.id() == ID_sva_sync_accept_on)
114122
{
115123
auto &sva_abort_expr = to_sva_abort_expr(expr);

‎src/verilog/expr2verilog.cpp‎

Lines changed: 8 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -680,10 +680,10 @@ Function: expr2verilogt::convert_sva_abort
680680

681681
expr2verilogt::resultt expr2verilogt::convert_sva_abort(
682682
const std::string &text,
683-
const sva_abort_exprt &expr)
683+
const binary_exprt &expr)
684684
{
685-
auto op0 = convert_rec(expr.condition());
686-
auto op1 = convert_rec(expr.property());
685+
auto op0 = convert_rec(expr.op0());
686+
auto op1 = convert_rec(expr.op1());
687687

688688
return {verilog_precedencet::MIN, text + " (" + op0.s + ") " + op1.s};
689689
}
@@ -1937,6 +1937,11 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src)
19371937
return precedence = verilog_precedencet::MIN,
19381938
convert_sva_abort("disable iff", to_sva_abort_expr(src));
19391939

1940+
else if(src.id() == ID_sva_sequence_disable_iff)
1941+
return precedence = verilog_precedencet::MIN,
1942+
convert_sva_abort(
1943+
"disable iff", to_sva_sequence_disable_iff_expr(src));
1944+
19401945
else if(src.id()==ID_sva_eventually)
19411946
{
19421947
return precedence = verilog_precedencet::MIN,

‎src/verilog/expr2verilog_class.h‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com
1212
#include <util/bitvector_expr.h>
1313
#include <util/std_expr.h>
1414

15-
class sva_abort_exprt;
1615
class sva_case_exprt;
1716
class sva_if_exprt;
1817
class sva_ranged_predicate_exprt;
@@ -145,7 +144,7 @@ class expr2verilogt
145144
const std::string &name,
146145
const sva_sequence_repetition_exprt &);
147146

148-
resultt convert_sva_abort(const std::string &name, const sva_abort_exprt &);
147+
resultt convert_sva_abort(const std::string &name, const binary_exprt &);
149148

150149
resultt
151150
convert_sva_indexed_binary(const std::string &name, const binary_exprt &);

‎src/verilog/parser.y‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2408,6 +2408,7 @@ concurrent_assertion_statement:
24082408
assert_property_statement
24092409
| assume_property_statement
24102410
| cover_property_statement
2411+
| cover_sequence_statement
24112412
| restrict_property_statement
24122413
;
24132414

@@ -2470,6 +2471,15 @@ cover_property_statement: TOK_COVER TOK_PROPERTY '(' property_spec ')' action_bl
24702471
{ init($$, ID_verilog_cover_property); mto($$, $4); mto($$, $6); }
24712472
;
24722473

2474+
cover_sequence_statement:
2475+
TOK_COVER TOK_SEQUENCE '(' sequence_expr ')' action_block
2476+
{ init($$, ID_verilog_cover_sequence); mto2($$, $4, $6); }
2477+
| TOK_COVER TOK_SEQUENCE '(' clocking_event TOK_DISABLE TOK_IFF '(' expression ')' sequence_expr ')' action_block
2478+
{ init($5, ID_sva_sequence_disable_iff); mto2($5, $8, $10); init($$, ID_verilog_cover_sequence); mto2($$, $5, $12); }
2479+
| TOK_COVER TOK_SEQUENCE '(' TOK_DISABLE TOK_IFF '(' expression ')' sequence_expr ')' action_block
2480+
{ init($4, ID_sva_sequence_disable_iff); mto2($4, $7, $9); init($$, ID_verilog_cover_sequence); mto2($$, $4, $11); }
2481+
;
2482+
24732483
restrict_property_statement: TOK_RESTRICT TOK_PROPERTY '(' property_spec ')' ';'
24742484
{ init($$, ID_verilog_restrict_property); mto($$, $4); mto($$, $6); }
24752485
;

‎src/verilog/sva_expr.h‎

Lines changed: 52 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -36,6 +36,58 @@ static inline sva_boolean_exprt &to_sva_boolean_expr(exprt &expr)
3636
return static_cast<sva_boolean_exprt &>(expr);
3737
}
3838

39+
/// disable_iff for cover sequence
40+
class sva_sequence_disable_iff_exprt : public binary_exprt
41+
{
42+
public:
43+
sva_sequence_disable_iff_exprt(exprt condition, exprt sequence)
44+
: binary_exprt(
45+
std::move(condition),
46+
ID_sva_sequence_disable_iff,
47+
std::move(sequence),
48+
verilog_sva_sequence_typet{})
49+
{
50+
}
51+
52+
const exprt &condition() const
53+
{
54+
return op0();
55+
}
56+
57+
exprt &condition()
58+
{
59+
return op0();
60+
}
61+
62+
const exprt &sequence() const
63+
{
64+
return op1();
65+
}
66+
67+
exprt &sequence()
68+
{
69+
return op1();
70+
}
71+
72+
protected:
73+
using binary_exprt::op0;
74+
using binary_exprt::op1;
75+
};
76+
77+
static inline const sva_sequence_disable_iff_exprt &
78+
to_sva_sequence_disable_iff_expr(const exprt &expr)
79+
{
80+
sva_sequence_disable_iff_exprt::check(expr, validation_modet::INVARIANT);
81+
return static_cast<const sva_sequence_disable_iff_exprt &>(expr);
82+
}
83+
84+
static inline sva_sequence_disable_iff_exprt &
85+
to_sva_sequence_disable_iff_expr(exprt &expr)
86+
{
87+
sva_sequence_disable_iff_exprt::check(expr, validation_modet::INVARIANT);
88+
return static_cast<sva_sequence_disable_iff_exprt &>(expr);
89+
}
90+
3991
/// accept_on, reject_on, sync_accept_on, sync_reject_on, disable_iff
4092
class sva_abort_exprt : public binary_exprt
4193
{

‎src/verilog/verilog_elaborate.cpp‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -671,6 +671,7 @@ void verilog_typecheckt::collect_symbols(const verilog_statementt &statement)
671671
statement.id() == ID_verilog_assume_property ||
672672
statement.id() == ID_verilog_restrict_property ||
673673
statement.id() == ID_verilog_cover_property ||
674+
statement.id() == ID_verilog_cover_sequence ||
674675
statement.id() == ID_verilog_expect_property)
675676
{
676677
}
@@ -850,7 +851,8 @@ void verilog_typecheckt::collect_symbols(
850851
module_item.id() == ID_verilog_assert_property ||
851852
module_item.id() == ID_verilog_assume_property ||
852853
module_item.id() == ID_verilog_restrict_property ||
853-
module_item.id() == ID_verilog_cover_property)
854+
module_item.id() == ID_verilog_cover_property ||
855+
module_item.id() == ID_verilog_cover_sequence)
854856
{
855857
}
856858
else if(module_item.id() == ID_verilog_assertion_item)

0 commit comments

Comments
 (0)