Skip to content

Commit 3294afe

Browse files
kroeningkroening
committed
Verilog: introduce sva_and_exprt, sva_or_exprt, sva_not_exprt
The SVA operators and, or differ from their standard Boolean counterparts when applied to SVA sequences. This introduces a separate IR for them. This also introduces a separate IR for SVA not, for the benefit of pretty-printing SVA formulas.
1 parent e77063c commit 3294afe

File tree

10 files changed

+185
-8
lines changed

10 files changed

+185
-8
lines changed

‎regression/ebmc/ring_buffer_bdd/ring_buffer.sv‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -19,8 +19,8 @@ module ring_buffer(input clk, input read, input write);
1919
wire full=count==15;
2020
wire empty=count==0;
2121

22-
assume property (empty -> !read);
23-
assume property (full -> !write);
22+
assume property (empty |-> !read);
23+
assume property (full |-> !write);
2424

2525
assert property (((writeptr-readptr)&'b1111)==count);
2626

‎regression/ebmc/ring_buffer_induction/ring_buffer.sv‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -19,8 +19,8 @@ module ring_buffer(input clk, input read, input write);
1919
wire full=count==15;
2020
wire empty=count==0;
2121

22-
assume property (empty -> !read);
23-
assume property (full -> !write);
22+
assume property (empty |-> !read);
23+
assume property (full |-> !write);
2424

2525
assert property (((writeptr-readptr)&'b1111)==count);
2626

‎src/hw_cbmc_irep_ids.h‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -44,6 +44,9 @@ IREP_ID_ONE(sva_overlapped_followed_by)
4444
IREP_ID_ONE(sva_nonoverlapped_followed_by)
4545
IREP_ID_ONE(sva_overlapped_implication)
4646
IREP_ID_ONE(sva_non_overlapped_implication)
47+
IREP_ID_ONE(sva_and)
48+
IREP_ID_ONE(sva_not)
49+
IREP_ID_ONE(sva_or)
4750
IREP_ID_ONE(module_instance)
4851
IREP_ID_TWO(C_offset, #offset)
4952
IREP_ID_TWO(C_big_endian, #big_endian)

‎src/temporal-logic/normalize_property.cpp‎

Lines changed: 58 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@ Author: Daniel Kroening, dkr@amazon.com
1414
#include <verilog/sva_expr.h>
1515

1616
#include "temporal_expr.h"
17+
#include "temporal_logic.h"
1718

1819
exprt normalize_pre_not(not_exprt expr)
1920
{
@@ -61,6 +62,51 @@ exprt normalize_pre_implies(implies_exprt expr)
6162
return or_exprt{not_exprt{expr.lhs()}, expr.rhs()};
6263
}
6364

65+
exprt normalize_pre_sva_overlapped_implication(
66+
sva_overlapped_implication_exprt expr)
67+
{
68+
// Same as regular implication if lhs and rhs are not
69+
// sequences.
70+
if(!is_SVA_sequence(expr.lhs()) && !is_SVA_sequence(expr.rhs()))
71+
return or_exprt{not_exprt{expr.lhs()}, expr.rhs()};
72+
else
73+
return std::move(expr);
74+
}
75+
76+
exprt normalize_pre_sva_non_overlapped_implication(
77+
sva_non_overlapped_implication_exprt expr)
78+
{
79+
// Same as a->Xb if lhs and rhs are not sequences.
80+
if(!is_SVA_sequence(expr.lhs()) && !is_SVA_sequence(expr.rhs()))
81+
return or_exprt{not_exprt{expr.lhs()}, X_exprt{expr.rhs()}};
82+
else
83+
return std::move(expr);
84+
}
85+
86+
exprt normalize_pre_sva_not(sva_not_exprt expr)
87+
{
88+
// Same as regular 'not'. These do not apply to sequences.
89+
return not_exprt{expr.op()};
90+
}
91+
92+
exprt normalize_pre_sva_and(sva_and_exprt expr)
93+
{
94+
// Same as a ∧ b if lhs and rhs are not sequences.
95+
if(!is_SVA_sequence(expr.lhs()) && !is_SVA_sequence(expr.rhs()))
96+
return and_exprt{expr.lhs(), expr.rhs()};
97+
else
98+
return std::move(expr);
99+
}
100+
101+
exprt normalize_pre_sva_or(sva_or_exprt expr)
102+
{
103+
// Same as a ∧ b if lhs or rhs are not sequences.
104+
if(!is_SVA_sequence(expr.lhs()) && !is_SVA_sequence(expr.rhs()))
105+
return or_exprt{expr.lhs(), expr.rhs()};
106+
else
107+
return std::move(expr);
108+
}
109+
64110
exprt normalize_pre_sva_cycle_delay(sva_cycle_delay_exprt expr)
65111
{
66112
if(expr.is_unbounded())
@@ -91,6 +137,18 @@ exprt normalize_property(exprt expr)
91137
expr = normalize_pre_implies(to_implies_expr(expr));
92138
else if(expr.id() == ID_sva_cover)
93139
expr = G_exprt{not_exprt{to_sva_cover_expr(expr).op()}};
140+
else if(expr.id() == ID_sva_overlapped_implication)
141+
expr = normalize_pre_sva_overlapped_implication(
142+
to_sva_overlapped_implication_expr(expr));
143+
else if(expr.id() == ID_sva_non_overlapped_implication)
144+
expr = normalize_pre_sva_non_overlapped_implication(
145+
to_sva_non_overlapped_implication_expr(expr));
146+
else if(expr.id() == ID_sva_and)
147+
expr = normalize_pre_sva_and(to_sva_and_expr(expr));
148+
else if(expr.id() == ID_sva_not)
149+
expr = normalize_pre_sva_not(to_sva_not_expr(expr));
150+
else if(expr.id() == ID_sva_or)
151+
expr = normalize_pre_sva_or(to_sva_or_expr(expr));
94152
else if(expr.id() == ID_sva_nexttime)
95153
{
96154
if(!to_sva_nexttime_expr(expr).is_indexed())

‎src/temporal-logic/normalize_property.h‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,11 @@ Author: Daniel Kroening, dkr@amazon.com
1616
/// ¬(a ∨ b) --> ¬a ∧ ¬b
1717
/// ¬(a ∧ b) --> ¬a ∨ ¬b
1818
/// (a -> b) --> ¬a ∨ b
19+
/// sva_not a --> ¬a
20+
/// a sva_and b --> a ∧ b if a and b are not SVA sequences
21+
/// a sva_or b --> a ∨ b if a and b are not SVA sequences
22+
/// sva_overlapped_implication --> ¬a ∨ b if a and b are not SVA sequences
23+
/// sva_non_overlapped_implication --> ¬a ∨ Xb if a and b are not SVA sequences
1924
/// sva_nexttime φ --> Xφ
2025
/// sva_s_nexttime φ --> Xφ
2126
/// sva_if --> ? :

‎src/temporal-logic/temporal_logic.cpp‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -71,7 +71,9 @@ bool is_SVA_sequence(const exprt &expr)
7171
auto id = expr.id();
7272
// Note that ID_sva_overlapped_followed_by and ID_sva_nonoverlapped_followed_by
7373
// are property expressions, not sequence expressions.
74-
return id == ID_sva_overlapped_implication ||
74+
// Note that ID_sva_not does not yield a sequence expression.
75+
return id == ID_sva_and || id == ID_sva_or ||
76+
id == ID_sva_overlapped_implication ||
7577
id == ID_sva_non_overlapped_implication || id == ID_sva_cycle_delay ||
7678
id == ID_sva_sequence_concatenation ||
7779
id == ID_sva_sequence_intersect || id == ID_sva_sequence_first_match ||

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

Lines changed: 31 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com
99
#include "instantiate_word_level.h"
1010

1111
#include <util/ebmc_util.h>
12+
#include <util/expr_util.h>
1213

1314
#include <temporal-logic/temporal_expr.h>
1415
#include <temporal-logic/temporal_logic.h>
@@ -240,6 +241,7 @@ wl_instantiatet::instantiate_sequence(exprt expr, const mp_integer &t) const
240241
}
241242
else if(expr.id() == ID_sva_sequence_intersect)
242243
{
244+
// IEEE 1800-2017 16.9.6
243245
PRECONDITION(false);
244246
}
245247
else if(expr.id() == ID_sva_sequence_first_match)
@@ -254,6 +256,35 @@ wl_instantiatet::instantiate_sequence(exprt expr, const mp_integer &t) const
254256
{
255257
PRECONDITION(false);
256258
}
259+
else if(expr.id() == ID_sva_and)
260+
{
261+
// IEEE 1800-2017 16.9.5
262+
// 1. Both operands must match.
263+
// 2. Both sequences start at the same time.
264+
// 3. The end time of the composite sequence is
265+
// the end time of the operand sequence that completes last.
266+
// Condition (3) is TBD.
267+
exprt::operandst conjuncts;
268+
269+
for(auto &op : expr.operands())
270+
conjuncts.push_back(instantiate_rec(op, t).second);
271+
272+
exprt condition = conjunction(conjuncts);
273+
return {{t, condition}};
274+
}
275+
else if(expr.id() == ID_sva_or)
276+
{
277+
// IEEE 1800-2017 16.9.7
278+
// The set of matches of a or b is the set union of the matches of a
279+
// and the matches of b.
280+
std::vector<std::pair<mp_integer, exprt>> result;
281+
282+
for(auto &op : expr.operands())
283+
for(auto &match_point : instantiate_sequence(op, t))
284+
result.push_back(match_point);
285+
286+
return result;
287+
}
257288
else
258289
{
259290
// not a sequence, evaluate as state predicate

‎src/verilog/expr2verilog.cpp‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1217,6 +1217,9 @@ expr2verilogt::convert(const exprt &src, verilog_precedencet &precedence)
12171217
return convert_unary(
12181218
to_not_expr(src), "!", precedence = verilog_precedencet::NOT);
12191219

1220+
else if(src.id() == ID_sva_not)
1221+
return convert_sva_unary("not", to_sva_not_expr(src));
1222+
12201223
else if(src.id()==ID_bitnot)
12211224
return convert_unary(
12221225
to_bitnot_expr(src), "~", precedence = verilog_precedencet::NOT);
@@ -1228,6 +1231,9 @@ expr2verilogt::convert(const exprt &src, verilog_precedencet &precedence)
12281231
return convert_binary(
12291232
to_multi_ary_expr(src), "&&", precedence = verilog_precedencet::AND);
12301233

1234+
else if(src.id() == ID_sva_and)
1235+
return convert_sva_binary("and", to_sva_and_expr(src));
1236+
12311237
else if(src.id()==ID_power)
12321238
return convert_binary(
12331239
to_multi_ary_expr(src), "**", precedence = verilog_precedencet::POWER);
@@ -1252,6 +1258,9 @@ expr2verilogt::convert(const exprt &src, verilog_precedencet &precedence)
12521258
return convert_binary(
12531259
to_multi_ary_expr(src), "||", precedence = verilog_precedencet::OR);
12541260

1261+
else if(src.id() == ID_sva_or)
1262+
return convert_sva_binary("or", to_sva_or_expr(src));
1263+
12551264
else if(src.id()==ID_bitor)
12561265
return convert_binary(
12571266
to_multi_ary_expr(src), "|", precedence = verilog_precedencet::BITOR);

‎src/verilog/parser.y‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -2100,11 +2100,11 @@ property_expr_proper:
21002100
| '(' property_expr_proper ')'
21012101
{ $$ = $2; }
21022102
| "not" property_expr
2103-
{ init($$, ID_not); mto($$, $2); }
2103+
{ init($$, ID_sva_not); mto($$, $2); }
21042104
| property_expr "or" property_expr
2105-
{ init($$, ID_or); mto($$, $1); mto($$, $3); }
2105+
{ init($$, ID_sva_or); mto($$, $1); mto($$, $3); }
21062106
| property_expr "and" property_expr
2107-
{ init($$, ID_and); mto($$, $1); mto($$, $3); }
2107+
{ init($$, ID_sva_and); mto($$, $1); mto($$, $3); }
21082108
| property_expr "|->" property_expr
21092109
{ init($$, ID_sva_overlapped_implication); mto($$, $1); mto($$, $3); }
21102110
| property_expr "|=>" property_expr

‎src/verilog/sva_expr.h‎

Lines changed: 69 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -500,6 +500,75 @@ to_sva_non_overlapped_implication_expr(exprt &expr)
500500
return static_cast<sva_non_overlapped_implication_exprt &>(expr);
501501
}
502502

503+
class sva_not_exprt : public unary_predicate_exprt
504+
{
505+
public:
506+
explicit sva_not_exprt(exprt op)
507+
: unary_predicate_exprt(ID_sva_not, std::move(op))
508+
{
509+
}
510+
};
511+
512+
static inline const sva_not_exprt &to_sva_not_expr(const exprt &expr)
513+
{
514+
PRECONDITION(expr.id() == ID_sva_not);
515+
sva_not_exprt::check(expr);
516+
return static_cast<const sva_not_exprt &>(expr);
517+
}
518+
519+
static inline sva_not_exprt &to_sva_not_expr(exprt &expr)
520+
{
521+
PRECONDITION(expr.id() == ID_sva_not);
522+
sva_not_exprt::check(expr);
523+
return static_cast<sva_not_exprt &>(expr);
524+
}
525+
526+
class sva_and_exprt : public binary_predicate_exprt
527+
{
528+
public:
529+
explicit sva_and_exprt(exprt op0, exprt op1)
530+
: binary_predicate_exprt(std::move(op0), ID_sva_and, std::move(op1))
531+
{
532+
}
533+
};
534+
535+
static inline const sva_and_exprt &to_sva_and_expr(const exprt &expr)
536+
{
537+
PRECONDITION(expr.id() == ID_sva_and);
538+
sva_and_exprt::check(expr, validation_modet::INVARIANT);
539+
return static_cast<const sva_and_exprt &>(expr);
540+
}
541+
542+
static inline sva_and_exprt &to_sva_and_expr(exprt &expr)
543+
{
544+
PRECONDITION(expr.id() == ID_sva_and);
545+
sva_and_exprt::check(expr, validation_modet::INVARIANT);
546+
return static_cast<sva_and_exprt &>(expr);
547+
}
548+
549+
class sva_or_exprt : public binary_predicate_exprt
550+
{
551+
public:
552+
explicit sva_or_exprt(exprt op0, exprt op1)
553+
: binary_predicate_exprt(std::move(op0), ID_sva_or, std::move(op1))
554+
{
555+
}
556+
};
557+
558+
static inline const sva_or_exprt &to_sva_or_expr(const exprt &expr)
559+
{
560+
PRECONDITION(expr.id() == ID_sva_or);
561+
sva_or_exprt::check(expr, validation_modet::INVARIANT);
562+
return static_cast<const sva_or_exprt &>(expr);
563+
}
564+
565+
static inline sva_or_exprt &to_sva_or_expr(exprt &expr)
566+
{
567+
PRECONDITION(expr.id() == ID_sva_or);
568+
sva_or_exprt::check(expr, validation_modet::INVARIANT);
569+
return static_cast<sva_or_exprt &>(expr);
570+
}
571+
503572
class sva_cycle_delay_exprt : public ternary_exprt
504573
{
505574
public:

0 commit comments

Comments
 (0)