Skip to content

Commit 2384b44

Browse files
kroeningkroening
authored
Merge pull request #1130 from diffblue/buechi-sequence-repetition
SVA-to-Buechi: sequence repetition operators
2 parents 9223813 + 339ecda commit 2384b44

File tree

6 files changed

+144
-13
lines changed

6 files changed

+144
-13
lines changed

‎regression/ebmc-spot/sva-buechi/sequence_repetition4.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
../../verilog/SVA/sequence_repetition4.sv
3+
--buechi --bound 10
4+
^\[main\.p0\] \(main\.x == 0 ##1 main\.x == 1\) \[\*2\]: PROVED up to bound \d+$
5+
^\[main\.p1\] \(main\.x == 0 ##1 main\.x == 1 ##1 main\.x == 0\) \[\*2\]: REFUTED$
6+
^EXIT=10$
7+
^SIGNAL=0$
8+
--
9+
^warning: ignoring
10+
--

‎regression/ebmc-spot/sva-buechi/sequence_repetition5.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
../../verilog/SVA/sequence_repetition5.sv
3+
--buechi --bound 20
4+
^\[.*\] main\.pulse ##1 \!main\.pulse \[\*1:9\] ##1 main.pulse: PROVED up to bound 20$
5+
^\[.*\] main\.pulse ##1 \!main\.pulse \[\*1:8\] ##1 main.pulse: REFUTED$
6+
^EXIT=10$
7+
^SIGNAL=0$
8+
--
9+
^warning: ignoring
10+
--

‎regression/ebmc-spot/sva-buechi/sequence_repetition6.desc

Lines changed: 0 additions & 8 deletions
This file was deleted.

‎regression/ebmc-spot/sva-buechi/sequence_repetition7.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
../../verilog/SVA/sequence_repetition7.sv
3+
--buechi --bound 20
4+
^\[.*\] \(main\.a ##1 main\.b\) \[\*5\]: PROVED up to bound 20$
5+
^\[.*\] \(\!main\.b ##1 \!main\.a\) \[\*5\]: PROVED up to bound 20$
6+
^EXIT=0$
7+
^SIGNAL=0$
8+
--
9+
^warning: ignoring
10+
--

‎src/temporal-logic/ltl_sva_to_string.cpp

Lines changed: 99 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -433,6 +433,105 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
433433
auto a2 = and_exprt{not_exprt{if_expr.cond()}, if_expr.false_case()};
434434
return rec(or_exprt{a1, a2}, mode);
435435
}
436+
else if(
437+
expr.id() ==
438+
ID_sva_sequence_repetition_star) // [*] or [*n] or [*x:y] or [*x:$]
439+
{
440+
PRECONDITION(mode == SVA_SEQUENCE);
441+
auto &repetition = to_sva_sequence_repetition_star_expr(expr);
442+
unary_exprt new_expr{ID_sva_sequence_repetition_star, repetition.op()};
443+
if(!repetition.repetitions_given())
444+
{
445+
return suffix("[*]", new_expr, mode);
446+
}
447+
else if(repetition.is_empty_match())
448+
{
449+
throw ebmc_errort{} << "cannot convert [*0] to Buechi";
450+
}
451+
else if(repetition.is_singleton())
452+
{
453+
auto n = numeric_cast_v<mp_integer>(repetition.repetitions());
454+
return suffix("[*" + integer2string(n) + "]", new_expr, mode);
455+
}
456+
else if(repetition.is_bounded_range())
457+
{
458+
auto from = numeric_cast_v<mp_integer>(repetition.from());
459+
auto to = numeric_cast_v<mp_integer>(repetition.to());
460+
return suffix(
461+
"[*" + integer2string(from) + ".." + integer2string(to) + "]",
462+
new_expr,
463+
mode);
464+
}
465+
else if(repetition.is_unbounded())
466+
{
467+
auto from = numeric_cast_v<mp_integer>(repetition.from());
468+
return suffix("[*" + integer2string(from) + "..]", new_expr, mode);
469+
}
470+
else
471+
DATA_INVARIANT(false, "unexpected sva_sequence_repetition_star");
472+
}
473+
else if(expr.id() == ID_sva_sequence_repetition_plus) // something[+]
474+
{
475+
PRECONDITION(mode == SVA_SEQUENCE);
476+
return suffix("[+]", expr, mode);
477+
}
478+
else if(expr.id() == ID_sva_sequence_goto_repetition) // something[->n]
479+
{
480+
PRECONDITION(mode == SVA_SEQUENCE);
481+
auto &repetition = to_sva_sequence_goto_repetition_expr(expr);
482+
unary_exprt new_expr{ID_sva_sequence_goto_repetition, repetition.op()};
483+
if(repetition.is_singleton())
484+
{
485+
auto n = numeric_cast_v<mp_integer>(repetition.repetitions());
486+
return suffix("[->" + integer2string(n) + "]", new_expr, mode);
487+
}
488+
else if(repetition.is_bounded_range())
489+
{
490+
auto from = numeric_cast_v<mp_integer>(repetition.from());
491+
auto to = numeric_cast_v<mp_integer>(repetition.to());
492+
return suffix(
493+
"[->" + integer2string(from) + ".." + integer2string(to) + "]",
494+
new_expr,
495+
mode);
496+
}
497+
else if(repetition.is_unbounded())
498+
{
499+
auto from = numeric_cast_v<mp_integer>(repetition.from());
500+
return suffix("[->" + integer2string(from) + "..]", new_expr, mode);
501+
}
502+
else
503+
DATA_INVARIANT(false, "unexpected sva_sequence_goto_repetition");
504+
}
505+
else if(
506+
expr.id() == ID_sva_sequence_non_consecutive_repetition) // something[=n]
507+
{
508+
PRECONDITION(mode == SVA_SEQUENCE);
509+
auto &repetition = to_sva_sequence_non_consecutive_repetition_expr(expr);
510+
unary_exprt new_expr{
511+
ID_sva_sequence_non_consecutive_repetition, repetition.op()};
512+
if(repetition.is_singleton())
513+
{
514+
auto n = numeric_cast_v<mp_integer>(repetition.repetitions());
515+
return suffix("[=" + integer2string(n) + "]", new_expr, mode);
516+
}
517+
else if(repetition.is_bounded_range())
518+
{
519+
auto from = numeric_cast_v<mp_integer>(repetition.from());
520+
auto to = numeric_cast_v<mp_integer>(repetition.to());
521+
return suffix(
522+
"[=" + integer2string(from) + ".." + integer2string(to) + "]",
523+
new_expr,
524+
mode);
525+
}
526+
else if(repetition.is_unbounded())
527+
{
528+
auto from = numeric_cast_v<mp_integer>(repetition.from());
529+
return suffix("[=" + integer2string(from) + "..]", new_expr, mode);
530+
}
531+
else
532+
DATA_INVARIANT(
533+
false, "unexpected sva_sequence_non_consecutive_repetition");
534+
}
436535
else if(!is_temporal_operator(expr))
437536
{
438537
auto number = atoms.number(expr);

‎src/verilog/sva_expr.h

Lines changed: 15 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1456,19 +1456,19 @@ class sva_sequence_repetition_exprt : public ternary_exprt
14561456
/// op[*0] is a special case, denoting the empty match
14571457
bool is_empty_match() const
14581458
{
1459-
return !is_range() && repetitions_given() && op1().is_zero();
1459+
return is_singleton() && op1().is_zero();
14601460
}
14611461

14621462
// The number of repetitions must be a constant after elaboration.
14631463
const constant_exprt &repetitions() const
14641464
{
1465-
PRECONDITION(repetitions_given() && !is_range());
1465+
PRECONDITION(is_singleton());
14661466
return static_cast<const constant_exprt &>(op1());
14671467
}
14681468

14691469
constant_exprt &repetitions()
14701470
{
1471-
PRECONDITION(repetitions_given() && !is_range());
1471+
PRECONDITION(is_singleton());
14721472
return static_cast<constant_exprt &>(op1());
14731473
}
14741474

@@ -1477,6 +1477,16 @@ class sva_sequence_repetition_exprt : public ternary_exprt
14771477
return op2().is_not_nil();
14781478
}
14791479

1480+
bool is_bounded_range() const
1481+
{
1482+
return op2().is_not_nil() && op2().id() != ID_infinity;
1483+
}
1484+
1485+
bool is_singleton() const
1486+
{
1487+
return op1().is_not_nil() && op2().is_nil();
1488+
}
1489+
14801490
bool is_unbounded() const
14811491
{
14821492
return op2().id() == ID_infinity;
@@ -1496,13 +1506,13 @@ class sva_sequence_repetition_exprt : public ternary_exprt
14961506

14971507
const constant_exprt &to() const
14981508
{
1499-
PRECONDITION(is_range() && !is_unbounded());
1509+
PRECONDITION(is_bounded_range());
15001510
return static_cast<const constant_exprt &>(op2());
15011511
}
15021512

15031513
constant_exprt &to()
15041514
{
1505-
PRECONDITION(is_range() && !is_unbounded());
1515+
PRECONDITION(is_bounded_range());
15061516
return static_cast<constant_exprt &>(op2());
15071517
}
15081518

0 commit comments

Comments
 (0)