Skip to content

Commit 716c755

Browse files
kroeningkroening
committed
SystemVerilog: disable iff
This adds SVA disable iff property specifications
1 parent e77063c commit 716c755

File tree

11 files changed

+141
-10
lines changed

11 files changed

+141
-10
lines changed

‎regression/verilog/SVA/disable_iff1.desc

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

‎regression/verilog/SVA/disable_iff1.sv

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
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) disable iff (counter == 0) counter != 0);
11+
12+
// expected to pass vacuously
13+
p1: assert property (@(posedge clk) disable iff (1) 0);
14+
15+
// expected to fail when counter reaches 2
16+
p2: assert property (@(posedge clk) disable iff (counter == 1) counter == 0);
17+
18+
endmodule

‎src/hw_cbmc_irep_ids.h

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -22,6 +22,7 @@ IREP_ID_ONE(sva_case)
2222
IREP_ID_ONE(sva_cycle_delay)
2323
IREP_ID_ONE(sva_cycle_delay_star)
2424
IREP_ID_ONE(sva_cycle_delay_plus)
25+
IREP_ID_ONE(sva_disable_iff)
2526
IREP_ID_ONE(sva_sequence_concatenation)
2627
IREP_ID_ONE(sva_sequence_first_match)
2728
IREP_ID_ONE(sva_sequence_intersect)

‎src/temporal-logic/normalize_property.cpp

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -115,6 +115,11 @@ exprt normalize_property(exprt expr)
115115
: sva_if_expr.false_case();
116116
expr = if_exprt{sva_if_expr.cond(), sva_if_expr.true_case(), false_case};
117117
}
118+
else if(expr.id() == ID_sva_disable_iff)
119+
{
120+
auto &disable_iff_expr = to_sva_disable_iff_expr(expr);
121+
expr = or_exprt{disable_iff_expr.lhs(), disable_iff_expr.rhs()};
122+
}
118123
else if(expr.id() == ID_sva_strong)
119124
{
120125
expr = to_sva_strong_expr(expr).op();

‎src/temporal-logic/normalize_property.h

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -19,6 +19,7 @@ Author: Daniel Kroening, [email protected]
1919
/// sva_nexttime φ --> Xφ
2020
/// sva_s_nexttime φ --> Xφ
2121
/// sva_if --> ? :
22+
/// a sva_disable_iff b --> a ∨ b
2223
/// ¬Xφ --> X¬φ
2324
/// ¬¬φ --> φ
2425
/// ¬Gφ --> F¬φ

‎src/temporal-logic/temporal_logic.cpp

Lines changed: 7 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -14,12 +14,13 @@ 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_always || expr.id() == ID_sva_always ||
18-
expr.id() == ID_sva_ranged_always || expr.id() == ID_sva_nexttime ||
19-
expr.id() == ID_sva_s_nexttime || expr.id() == ID_sva_until ||
20-
expr.id() == ID_sva_s_until || expr.id() == ID_sva_until_with ||
21-
expr.id() == ID_sva_s_until_with || expr.id() == ID_sva_eventually ||
22-
expr.id() == ID_sva_s_eventually || expr.id() == ID_sva_cycle_delay ||
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 ||
2324
expr.id() == ID_sva_overlapped_followed_by ||
2425
expr.id() == ID_sva_nonoverlapped_followed_by;
2526
}

‎src/verilog/expr2verilog.cpp

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

476476
/*******************************************************************\
477477
478+
Function: expr2verilogt::convert_sva_disable_iff
479+
480+
Inputs:
481+
482+
Outputs:
483+
484+
Purpose:
485+
486+
\*******************************************************************/
487+
488+
std::string
489+
expr2verilogt::convert_sva_disable_iff(const sva_disable_iff_exprt &expr)
490+
{
491+
verilog_precedencet p0;
492+
auto s0 = convert(expr.condition(), p0);
493+
494+
verilog_precedencet p1;
495+
auto s1 = convert(expr.rhs(), p1);
496+
497+
return "disable iff (" + s0 + ") " + s1;
498+
}
499+
500+
/*******************************************************************\
501+
478502
Function: expr2verilogt::convert_sva_indexed_binary
479503
480504
Inputs:
@@ -1408,6 +1432,10 @@ expr2verilogt::convert(const exprt &src, verilog_precedencet &precedence)
14081432
return precedence = verilog_precedencet::MIN,
14091433
convert_sva_indexed_binary("nexttime", to_sva_nexttime_expr(src));
14101434

1435+
else if(src.id() == ID_sva_disable_iff)
1436+
return precedence = verilog_precedencet::MIN,
1437+
convert_sva_disable_iff(to_sva_disable_iff_expr(src));
1438+
14111439
else if(src.id()==ID_sva_s_nexttime)
14121440
return precedence = verilog_precedencet::MIN,
14131441
convert_sva_indexed_binary(

‎src/verilog/expr2verilog_class.h

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,7 @@ Author: Daniel Kroening, [email protected]
1313
#include <util/std_expr.h>
1414

1515
class sva_case_exprt;
16+
class sva_disable_iff_exprt;
1617
class sva_if_exprt;
1718
class sva_ranged_predicate_exprt;
1819

@@ -122,6 +123,8 @@ class expr2verilogt
122123
std::string
123124
convert_sva_indexed_binary(const std::string &name, const binary_exprt &);
124125

126+
std::string convert_sva_disable_iff(const sva_disable_iff_exprt &);
127+
125128
virtual std::string
126129
convert_replication(const replication_exprt &, verilog_precedencet);
127130

‎src/verilog/parser.y

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -527,7 +527,7 @@ int yyverilogerror(const char *error)
527527
// whereas the table gives them in decreasing order.
528528
// The precendence of the assertion operators is lower than
529529
// those in Table 11-2.
530-
%nonassoc "property_expr_event_control" // @(...) property_expr
530+
%nonassoc "property_expr_clocking_event" // @(...) property_expr
531531
%nonassoc "always" "s_always" "eventually" "s_eventually"
532532
%nonassoc "accept_on" "reject_on"
533533
%nonassoc "sync_accept_on" "sync_reject_on"
@@ -2077,8 +2077,10 @@ property_formal_type:
20772077
;
20782078

20792079
property_spec:
2080-
TOK_DISABLE TOK_IFF '(' expression ')' property_expr
2081-
{ $$=$6; }
2080+
clocking_event TOK_DISABLE TOK_IFF '(' expression ')' property_expr
2081+
{ init($$, ID_sva_disable_iff); mto($$, $5); mto($$, $7); }
2082+
| TOK_DISABLE TOK_IFF '(' expression ')' property_expr
2083+
{ init($$, ID_sva_disable_iff); mto($$, $4); mto($$, $6); }
20822084
| property_expr
20832085
;
20842086

@@ -2159,7 +2161,7 @@ property_expr_proper:
21592161
{ init($$, "sva_sync_accept_on"); mto($$, $3); }
21602162
| "sync_reject_on" '(' expression_or_dist ')'
21612163
{ init($$, "sva_sync_reject_on"); mto($$, $3); }
2162-
| event_control property_expr { $$=$2; } %prec "property_expr_event_control"
2164+
| clocking_event property_expr { $$=$2; } %prec "property_expr_clocking_event"
21632165
;
21642166

21652167
property_case_item_brace:

‎src/verilog/sva_expr.h

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

1212
#include <util/std_expr.h>
1313

14+
class sva_disable_iff_exprt : public binary_predicate_exprt
15+
{
16+
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))
22+
{
23+
}
24+
25+
const exprt &condition() const
26+
{
27+
return op0();
28+
}
29+
30+
exprt &condition()
31+
{
32+
return op0();
33+
}
34+
35+
const exprt &property() const
36+
{
37+
return op1();
38+
}
39+
40+
exprt &property()
41+
{
42+
return op1();
43+
}
44+
45+
protected:
46+
using binary_predicate_exprt::op0;
47+
using binary_predicate_exprt::op1;
48+
};
49+
50+
static inline const sva_disable_iff_exprt &
51+
to_sva_disable_iff_expr(const exprt &expr)
52+
{
53+
PRECONDITION(expr.id() == ID_sva_disable_iff);
54+
sva_disable_iff_exprt::check(expr, validation_modet::INVARIANT);
55+
return static_cast<const sva_disable_iff_exprt &>(expr);
56+
}
57+
58+
static inline sva_disable_iff_exprt &to_sva_disable_iff_expr(exprt &expr)
59+
{
60+
PRECONDITION(expr.id() == ID_sva_disable_iff);
61+
sva_disable_iff_exprt::check(expr, validation_modet::INVARIANT);
62+
return static_cast<sva_disable_iff_exprt &>(expr);
63+
}
64+
1465
class sva_nexttime_exprt : public binary_predicate_exprt
1566
{
1667
public:

‎src/verilog/verilog_typecheck_expr.cpp

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2517,6 +2517,15 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr)
25172517

25182518
return std::move(expr);
25192519
}
2520+
else if(expr.id() == ID_sva_disable_iff)
2521+
{
2522+
convert_expr(to_sva_disable_iff_expr(expr).condition());
2523+
make_boolean(to_sva_disable_iff_expr(expr).condition());
2524+
convert_expr(to_sva_disable_iff_expr(expr).property());
2525+
make_boolean(to_sva_disable_iff_expr(expr).property());
2526+
expr.type() = bool_typet();
2527+
return std::move(expr);
2528+
}
25202529
else if(expr.id() == ID_sva_nexttime)
25212530
{
25222531
if(to_sva_nexttime_expr(expr).is_indexed())

0 commit comments

Comments
 (0)