Skip to content

Commit 6d1a00a

Browse files
tautschnigtautschnig
authored
Merge pull request #615 from diffblue/sva_and_not_or
Verilog: introduce sva_and_exprt, sva_or_exprt, sva_not_exprt
2 parents 8709bb5 + 3294afe commit 6d1a00a

File tree

10 files changed

+185
-8
lines changed

10 files changed

+185
-8
lines changed

‎regression/ebmc/ring_buffer_bdd/ring_buffer.sv

+2-2
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

+2-2
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

+3
Original file line numberDiff line numberDiff line change
@@ -54,6 +54,9 @@ IREP_ID_ONE(sva_overlapped_followed_by)
5454
IREP_ID_ONE(sva_nonoverlapped_followed_by)
5555
IREP_ID_ONE(sva_overlapped_implication)
5656
IREP_ID_ONE(sva_non_overlapped_implication)
57+
IREP_ID_ONE(sva_and)
58+
IREP_ID_ONE(sva_not)
59+
IREP_ID_ONE(sva_or)
5760
IREP_ID_ONE(module_instance)
5861
IREP_ID_TWO(C_offset, #offset)
5962
IREP_ID_TWO(C_big_endian, #big_endian)

‎src/temporal-logic/normalize_property.cpp

+58
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
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

+5
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,11 @@ Author: Daniel Kroening, [email protected]
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

+3-1
Original file line numberDiff line numberDiff line change
@@ -73,7 +73,9 @@ bool is_SVA_sequence(const exprt &expr)
7373
auto id = expr.id();
7474
// Note that ID_sva_overlapped_followed_by and ID_sva_nonoverlapped_followed_by
7575
// are property expressions, not sequence expressions.
76-
return id == ID_sva_overlapped_implication ||
76+
// Note that ID_sva_not does not yield a sequence expression.
77+
return id == ID_sva_and || id == ID_sva_or ||
78+
id == ID_sva_overlapped_implication ||
7779
id == ID_sva_non_overlapped_implication || id == ID_sva_cycle_delay ||
7880
id == ID_sva_sequence_concatenation ||
7981
id == ID_sva_sequence_intersect || id == ID_sva_sequence_first_match ||

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

+31
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@ Author: Daniel Kroening, [email protected]
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

+9
Original file line numberDiff line numberDiff line change
@@ -1242,6 +1242,9 @@ expr2verilogt::convert(const exprt &src, verilog_precedencet &precedence)
12421242
return convert_unary(
12431243
to_not_expr(src), "!", precedence = verilog_precedencet::NOT);
12441244

1245+
else if(src.id() == ID_sva_not)
1246+
return convert_sva_unary("not", to_sva_not_expr(src));
1247+
12451248
else if(src.id()==ID_bitnot)
12461249
return convert_unary(
12471250
to_bitnot_expr(src), "~", precedence = verilog_precedencet::NOT);
@@ -1253,6 +1256,9 @@ expr2verilogt::convert(const exprt &src, verilog_precedencet &precedence)
12531256
return convert_binary(
12541257
to_multi_ary_expr(src), "&&", precedence = verilog_precedencet::AND);
12551258

1259+
else if(src.id() == ID_sva_and)
1260+
return convert_sva_binary("and", to_sva_and_expr(src));
1261+
12561262
else if(src.id()==ID_power)
12571263
return convert_binary(
12581264
to_multi_ary_expr(src), "**", precedence = verilog_precedencet::POWER);
@@ -1277,6 +1283,9 @@ expr2verilogt::convert(const exprt &src, verilog_precedencet &precedence)
12771283
return convert_binary(
12781284
to_multi_ary_expr(src), "||", precedence = verilog_precedencet::OR);
12791285

1286+
else if(src.id() == ID_sva_or)
1287+
return convert_sva_binary("or", to_sva_or_expr(src));
1288+
12801289
else if(src.id()==ID_bitor)
12811290
return convert_binary(
12821291
to_multi_ary_expr(src), "|", precedence = verilog_precedencet::BITOR);

‎src/verilog/parser.y

+3-3
Original file line numberDiff line numberDiff line change
@@ -2107,11 +2107,11 @@ property_expr_proper:
21072107
| '(' property_expr_proper ')'
21082108
{ $$ = $2; }
21092109
| "not" property_expr
2110-
{ init($$, ID_not); mto($$, $2); }
2110+
{ init($$, ID_sva_not); mto($$, $2); }
21112111
| property_expr "or" property_expr
2112-
{ init($$, ID_or); mto($$, $1); mto($$, $3); }
2112+
{ init($$, ID_sva_or); mto($$, $1); mto($$, $3); }
21132113
| property_expr "and" property_expr
2114-
{ init($$, ID_and); mto($$, $1); mto($$, $3); }
2114+
{ init($$, ID_sva_and); mto($$, $1); mto($$, $3); }
21152115
| property_expr "|->" property_expr
21162116
{ init($$, ID_sva_overlapped_implication); mto($$, $1); mto($$, $3); }
21172117
| property_expr "|=>" property_expr

‎src/verilog/sva_expr.h

+69
Original file line numberDiff line numberDiff line change
@@ -573,6 +573,75 @@ to_sva_non_overlapped_implication_expr(exprt &expr)
573573
return static_cast<sva_non_overlapped_implication_exprt &>(expr);
574574
}
575575

576+
class sva_not_exprt : public unary_predicate_exprt
577+
{
578+
public:
579+
explicit sva_not_exprt(exprt op)
580+
: unary_predicate_exprt(ID_sva_not, std::move(op))
581+
{
582+
}
583+
};
584+
585+
static inline const sva_not_exprt &to_sva_not_expr(const exprt &expr)
586+
{
587+
PRECONDITION(expr.id() == ID_sva_not);
588+
sva_not_exprt::check(expr);
589+
return static_cast<const sva_not_exprt &>(expr);
590+
}
591+
592+
static inline sva_not_exprt &to_sva_not_expr(exprt &expr)
593+
{
594+
PRECONDITION(expr.id() == ID_sva_not);
595+
sva_not_exprt::check(expr);
596+
return static_cast<sva_not_exprt &>(expr);
597+
}
598+
599+
class sva_and_exprt : public binary_predicate_exprt
600+
{
601+
public:
602+
explicit sva_and_exprt(exprt op0, exprt op1)
603+
: binary_predicate_exprt(std::move(op0), ID_sva_and, std::move(op1))
604+
{
605+
}
606+
};
607+
608+
static inline const sva_and_exprt &to_sva_and_expr(const exprt &expr)
609+
{
610+
PRECONDITION(expr.id() == ID_sva_and);
611+
sva_and_exprt::check(expr, validation_modet::INVARIANT);
612+
return static_cast<const sva_and_exprt &>(expr);
613+
}
614+
615+
static inline sva_and_exprt &to_sva_and_expr(exprt &expr)
616+
{
617+
PRECONDITION(expr.id() == ID_sva_and);
618+
sva_and_exprt::check(expr, validation_modet::INVARIANT);
619+
return static_cast<sva_and_exprt &>(expr);
620+
}
621+
622+
class sva_or_exprt : public binary_predicate_exprt
623+
{
624+
public:
625+
explicit sva_or_exprt(exprt op0, exprt op1)
626+
: binary_predicate_exprt(std::move(op0), ID_sva_or, std::move(op1))
627+
{
628+
}
629+
};
630+
631+
static inline const sva_or_exprt &to_sva_or_expr(const exprt &expr)
632+
{
633+
PRECONDITION(expr.id() == ID_sva_or);
634+
sva_or_exprt::check(expr, validation_modet::INVARIANT);
635+
return static_cast<const sva_or_exprt &>(expr);
636+
}
637+
638+
static inline sva_or_exprt &to_sva_or_expr(exprt &expr)
639+
{
640+
PRECONDITION(expr.id() == ID_sva_or);
641+
sva_or_exprt::check(expr, validation_modet::INVARIANT);
642+
return static_cast<sva_or_exprt &>(expr);
643+
}
644+
576645
class sva_cycle_delay_exprt : public ternary_exprt
577646
{
578647
public:

0 commit comments

Comments
 (0)