Skip to content

Commit b2b8a05

Browse files
kroeningkroening
authored
Merge pull request #618 from diffblue/sva-abort-properties
SystemVerilog: SVA abort properties
2 parents dfca8ce + 59d332b commit b2b8a05

File tree

11 files changed

+137
-36
lines changed

11 files changed

+137
-36
lines changed

‎regression/verilog/SVA/sva_abort1.desc

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CORE
2+
sva_abort1.sv
3+
--module main --bound 10
4+
^\[main\.p0\] always \(accept_on \(main\.counter == 0\) main\.counter != 0\): PROVED up to bound 10$
5+
^\[main\.p1\] always \(accept_on \(1\) 0\): PROVED up to bound 10$
6+
^\[main\.p2\] always \(accept_on \(main\.counter == 1\) main\.counter == 0\): REFUTED$
7+
^\[main\.p3\] always \(reject_on \(main\.counter != 0\) 1\): REFUTED$
8+
^\[main\.p4\] always \(reject_on \(1\) 1\): REFUTED$
9+
^EXIT=10$
10+
^SIGNAL=0$
11+
--
12+
^warning: ignoring
13+
--

‎regression/verilog/SVA/sva_abort1.sv

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
module main(input clk);
2+
3+
// count up
4+
reg [7:0] counter = 0;
5+
6+
always_ff @(posedge clk)
7+
counter++;
8+
9+
// expected to pass
10+
p0: assert property (@(posedge clk) accept_on (counter == 0) counter != 0);
11+
12+
// expected to pass vacuously
13+
p1: assert property (@(posedge clk) accept_on (1) 0);
14+
15+
// expected to fail when counter reaches 2
16+
p2: assert property (@(posedge clk) accept_on (counter == 1) counter == 0);
17+
18+
// expected to fail when counter reaches 2
19+
p3: assert property (@(posedge clk) reject_on (counter != 0) 1);
20+
21+
// expected to fail
22+
p4: assert property (@(posedge clk) reject_on (1) 1);
23+
24+
endmodule

‎src/hw_cbmc_irep_ids.h

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,10 @@ IREP_ID_ONE(F)
1515
IREP_ID_ONE(E)
1616
IREP_ID_ONE(G)
1717
IREP_ID_ONE(X)
18+
IREP_ID_ONE(sva_accept_on)
19+
IREP_ID_ONE(sva_reject_on)
20+
IREP_ID_ONE(sva_sync_accept_on)
21+
IREP_ID_ONE(sva_sync_reject_on)
1822
IREP_ID_ONE(sva_strong)
1923
IREP_ID_ONE(sva_weak)
2024
IREP_ID_ONE(sva_if)

‎src/temporal-logic/normalize_property.cpp

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -120,6 +120,17 @@ exprt normalize_property(exprt expr)
120120
auto &disable_iff_expr = to_sva_disable_iff_expr(expr);
121121
expr = or_exprt{disable_iff_expr.lhs(), disable_iff_expr.rhs()};
122122
}
123+
else if(expr.id() == ID_sva_accept_on || expr.id() == ID_sva_sync_accept_on)
124+
{
125+
auto &sva_abort_expr = to_sva_abort_expr(expr);
126+
expr = or_exprt{sva_abort_expr.condition(), sva_abort_expr.property()};
127+
}
128+
else if(expr.id() == ID_sva_reject_on || expr.id() == ID_sva_sync_reject_on)
129+
{
130+
auto &sva_abort_expr = to_sva_abort_expr(expr);
131+
expr = and_exprt{
132+
not_exprt{sva_abort_expr.condition()}, sva_abort_expr.property()};
133+
}
123134
else if(expr.id() == ID_sva_strong)
124135
{
125136
expr = to_sva_strong_expr(expr).op();

‎src/temporal-logic/normalize_property.h

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,10 @@ Author: Daniel Kroening, [email protected]
2020
/// sva_s_nexttime φ --> Xφ
2121
/// sva_if --> ? :
2222
/// a sva_disable_iff b --> a ∨ b
23+
/// a sva_accept_on b --> a ∨ b
24+
/// a sva_reject_on b --> ¬a ∧ b
25+
/// a sva_sync_accept_on b --> a ∨ b
26+
/// a sva_sync_reject_on b --> ¬a ∧ b
2327
/// ¬Xφ --> X¬φ
2428
/// ¬¬φ --> φ
2529
/// ¬Gφ --> F¬φ

‎src/temporal-logic/temporal_logic.cpp

Lines changed: 8 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -14,13 +14,14 @@ bool is_temporal_operator(const exprt &expr)
1414
{
1515
return is_CTL_operator(expr) || is_LTL_operator(expr) ||
1616
is_SVA_sequence(expr) || expr.id() == ID_A || expr.id() == ID_E ||
17-
expr.id() == ID_sva_disable_iff || expr.id() == ID_sva_always ||
18-
expr.id() == ID_sva_always || expr.id() == ID_sva_ranged_always ||
19-
expr.id() == ID_sva_nexttime || expr.id() == ID_sva_s_nexttime ||
20-
expr.id() == ID_sva_until || expr.id() == ID_sva_s_until ||
21-
expr.id() == ID_sva_until_with || expr.id() == ID_sva_s_until_with ||
22-
expr.id() == ID_sva_eventually || expr.id() == ID_sva_s_eventually ||
23-
expr.id() == ID_sva_cycle_delay ||
17+
expr.id() == ID_sva_disable_iff || expr.id() == ID_sva_accept_on ||
18+
expr.id() == ID_sva_reject_on || expr.id() == ID_sva_sync_accept_on ||
19+
expr.id() == ID_sva_sync_reject_on || expr.id() == ID_sva_always ||
20+
expr.id() == ID_sva_ranged_always || expr.id() == ID_sva_nexttime ||
21+
expr.id() == ID_sva_s_nexttime || expr.id() == ID_sva_until ||
22+
expr.id() == ID_sva_s_until || expr.id() == ID_sva_until_with ||
23+
expr.id() == ID_sva_s_until_with || expr.id() == ID_sva_eventually ||
24+
expr.id() == ID_sva_s_eventually || expr.id() == ID_sva_cycle_delay ||
2425
expr.id() == ID_sva_overlapped_followed_by ||
2526
expr.id() == ID_sva_nonoverlapped_followed_by;
2627
}

‎src/verilog/expr2verilog.cpp

Lines changed: 23 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -475,7 +475,7 @@ std::string expr2verilogt::convert_sva_binary(
475475

476476
/*******************************************************************\
477477
478-
Function: expr2verilogt::convert_sva_disable_iff
478+
Function: expr2verilogt::convert_sva_abort
479479
480480
Inputs:
481481
@@ -485,16 +485,17 @@ Function: expr2verilogt::convert_sva_disable_iff
485485
486486
\*******************************************************************/
487487

488-
std::string
489-
expr2verilogt::convert_sva_disable_iff(const sva_disable_iff_exprt &expr)
488+
std::string expr2verilogt::convert_sva_abort(
489+
const std::string &text,
490+
const sva_abort_exprt &expr)
490491
{
491492
verilog_precedencet p0;
492493
auto s0 = convert(expr.condition(), p0);
493494

494495
verilog_precedencet p1;
495-
auto s1 = convert(expr.rhs(), p1);
496+
auto s1 = convert(expr.property(), p1);
496497

497-
return "disable iff (" + s0 + ") " + s1;
498+
return text + " (" + s0 + ") " + s1;
498499
}
499500

500501
/*******************************************************************\
@@ -1428,13 +1429,29 @@ expr2verilogt::convert(const exprt &src, verilog_precedencet &precedence)
14281429
return precedence = verilog_precedencet::MIN,
14291430
convert_sva_unary("assume", to_sva_assume_expr(src));
14301431

1432+
else if(src.id() == ID_sva_accept_on)
1433+
return precedence = verilog_precedencet::MIN,
1434+
convert_sva_abort("accept_on", to_sva_abort_expr(src));
1435+
1436+
else if(src.id() == ID_sva_reject_on)
1437+
return precedence = verilog_precedencet::MIN,
1438+
convert_sva_abort("reject_on", to_sva_abort_expr(src));
1439+
1440+
else if(src.id() == ID_sva_sync_accept_on)
1441+
return precedence = verilog_precedencet::MIN,
1442+
convert_sva_abort("sync_accept_on", to_sva_abort_expr(src));
1443+
1444+
else if(src.id() == ID_sva_sync_reject_on)
1445+
return precedence = verilog_precedencet::MIN,
1446+
convert_sva_abort("sync_reject_on", to_sva_abort_expr(src));
1447+
14311448
else if(src.id()==ID_sva_nexttime)
14321449
return precedence = verilog_precedencet::MIN,
14331450
convert_sva_indexed_binary("nexttime", to_sva_nexttime_expr(src));
14341451

14351452
else if(src.id() == ID_sva_disable_iff)
14361453
return precedence = verilog_precedencet::MIN,
1437-
convert_sva_disable_iff(to_sva_disable_iff_expr(src));
1454+
convert_sva_abort("disable iff", to_sva_abort_expr(src));
14381455

14391456
else if(src.id()==ID_sva_s_nexttime)
14401457
return precedence = verilog_precedencet::MIN,

‎src/verilog/expr2verilog_class.h

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -12,8 +12,8 @@ Author: Daniel Kroening, [email protected]
1212
#include <util/bitvector_expr.h>
1313
#include <util/std_expr.h>
1414

15+
class sva_abort_exprt;
1516
class sva_case_exprt;
16-
class sva_disable_iff_exprt;
1717
class sva_if_exprt;
1818
class sva_ranged_predicate_exprt;
1919

@@ -121,9 +121,10 @@ class expr2verilogt
121121
std::string convert_sva_binary(const std::string &name, const binary_exprt &);
122122

123123
std::string
124-
convert_sva_indexed_binary(const std::string &name, const binary_exprt &);
124+
convert_sva_abort(const std::string &name, const sva_abort_exprt &);
125125

126-
std::string convert_sva_disable_iff(const sva_disable_iff_exprt &);
126+
std::string
127+
convert_sva_indexed_binary(const std::string &name, const binary_exprt &);
127128

128129
virtual std::string
129130
convert_replication(const replication_exprt &, verilog_precedencet);

‎src/verilog/parser.y

Lines changed: 9 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -531,6 +531,7 @@ int yyverilogerror(const char *error)
531531
// whereas the table gives them in decreasing order.
532532
// The precendence of the assertion operators is lower than
533533
// those in Table 11-2.
534+
%nonassoc "property_expr_abort" // accept_on, reject_on, ...
534535
%nonassoc "property_expr_clocking_event" // @(...) property_expr
535536
%nonassoc "always" "s_always" "eventually" "s_eventually"
536537
%nonassoc "accept_on" "reject_on"
@@ -2157,14 +2158,14 @@ property_expr_proper:
21572158
{ init($$, ID_implies); mto($$, $1); mto($$, $3); }
21582159
| property_expr "iff" property_expr
21592160
{ init($$, ID_iff); mto($$, $1); mto($$, $3); }
2160-
| "accept_on" '(' expression_or_dist ')'
2161-
{ init($$, "sva_accept_on"); mto($$, $3); }
2162-
| "reject_on" '(' expression_or_dist ')'
2163-
{ init($$, "sva_reject_on"); mto($$, $3); }
2164-
| "sync_accept_on" '(' expression_or_dist ')'
2165-
{ init($$, "sva_sync_accept_on"); mto($$, $3); }
2166-
| "sync_reject_on" '(' expression_or_dist ')'
2167-
{ init($$, "sva_sync_reject_on"); mto($$, $3); }
2161+
| "accept_on" '(' expression_or_dist ')' property_expr %prec "property_expr_abort"
2162+
{ init($$, ID_sva_accept_on); mto($$, $3); mto($$, $5); }
2163+
| "reject_on" '(' expression_or_dist ')' property_expr %prec "property_expr_abort"
2164+
{ init($$, ID_sva_reject_on); mto($$, $3); mto($$, $5); }
2165+
| "sync_accept_on" '(' expression_or_dist ')' property_expr %prec "property_expr_abort"
2166+
{ init($$, ID_sva_sync_accept_on); mto($$, $3); mto($$, $5); }
2167+
| "sync_reject_on" '(' expression_or_dist ')' property_expr %prec "property_expr_abort"
2168+
{ init($$, ID_sva_sync_reject_on); mto($$, $3); mto($$, $5); }
21682169
| clocking_event property_expr { $$=$2; } %prec "property_expr_clocking_event"
21692170
;
21702171

‎src/verilog/sva_expr.h

Lines changed: 28 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -11,14 +11,12 @@ Author: Daniel Kroening, [email protected]
1111

1212
#include <util/std_expr.h>
1313

14-
class sva_disable_iff_exprt : public binary_predicate_exprt
14+
/// accept_on, reject_on, sync_accept_on, sync_reject_on, disable_iff
15+
class sva_abort_exprt : public binary_predicate_exprt
1516
{
1617
public:
17-
explicit sva_disable_iff_exprt(exprt condition, exprt property)
18-
: binary_predicate_exprt(
19-
std::move(condition),
20-
ID_sva_disable_iff,
21-
std::move(property))
18+
sva_abort_exprt(irep_idt id, exprt condition, exprt property)
19+
: binary_predicate_exprt(std::move(condition), id, std::move(property))
2220
{
2321
}
2422

@@ -47,6 +45,30 @@ class sva_disable_iff_exprt : public binary_predicate_exprt
4745
using binary_predicate_exprt::op1;
4846
};
4947

48+
static inline const sva_abort_exprt &to_sva_abort_expr(const exprt &expr)
49+
{
50+
sva_abort_exprt::check(expr, validation_modet::INVARIANT);
51+
return static_cast<const sva_abort_exprt &>(expr);
52+
}
53+
54+
static inline sva_abort_exprt &to_sva_abort_expr(exprt &expr)
55+
{
56+
sva_abort_exprt::check(expr, validation_modet::INVARIANT);
57+
return static_cast<sva_abort_exprt &>(expr);
58+
}
59+
60+
class sva_disable_iff_exprt : public sva_abort_exprt
61+
{
62+
public:
63+
sva_disable_iff_exprt(exprt condition, exprt property)
64+
: sva_abort_exprt(
65+
ID_sva_disable_iff,
66+
std::move(condition),
67+
std::move(property))
68+
{
69+
}
70+
};
71+
5072
static inline const sva_disable_iff_exprt &
5173
to_sva_disable_iff_expr(const exprt &expr)
5274
{

0 commit comments

Comments
 (0)