From 615038cf4ff6ba3401ea78a2c56e95c0206721c8 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Thu, 20 Mar 2025 13:35:36 -0700 Subject: [PATCH] Bugfix: s_always is a temporal logic operator This adds SVA's s_always to the list of temporal logic operators. --- regression/verilog/SVA/initial1.desc | 2 +- src/temporal-logic/temporal_logic.cpp | 15 ++++++++------- 2 files changed, 9 insertions(+), 8 deletions(-) diff --git a/regression/verilog/SVA/initial1.desc b/regression/verilog/SVA/initial1.desc index 62831ad56..6d62c2ee3 100644 --- a/regression/verilog/SVA/initial1.desc +++ b/regression/verilog/SVA/initial1.desc @@ -5,7 +5,7 @@ initial1.sv ^\[main\.p1\] main\.counter == 100: REFUTED$ ^\[main\.p2\] ##1 main\.counter == 1: PROVED up to bound 5$ ^\[main\.p3\] ##1 main\.counter == 100: REFUTED$ -^\[main\.p4\] s_nexttime main\.counter == 1: PROVED$ +^\[main\.p4\] s_nexttime main\.counter == 1: PROVED up to bound 5$ ^EXIT=10$ ^SIGNAL=0$ -- diff --git a/src/temporal-logic/temporal_logic.cpp b/src/temporal-logic/temporal_logic.cpp index 668f6d862..0c0b2b758 100644 --- a/src/temporal-logic/temporal_logic.cpp +++ b/src/temporal-logic/temporal_logic.cpp @@ -117,13 +117,14 @@ bool is_SVA_operator(const exprt &expr) return is_SVA_sequence(expr) || id == ID_sva_disable_iff || id == ID_sva_accept_on || id == ID_sva_reject_on || id == ID_sva_sync_accept_on || id == ID_sva_sync_reject_on || - id == ID_sva_always || id == ID_sva_ranged_always || - id == ID_sva_nexttime || id == ID_sva_s_nexttime || - id == ID_sva_indexed_nexttime || id == ID_sva_until || - id == ID_sva_s_until || id == ID_sva_until_with || - id == ID_sva_s_until_with || id == ID_sva_eventually || - id == ID_sva_s_eventually || id == ID_sva_ranged_s_eventually || - id == ID_sva_cycle_delay || id == ID_sva_overlapped_followed_by || + id == ID_sva_always || id == ID_sva_s_always || + id == ID_sva_ranged_always || id == ID_sva_nexttime || + id == ID_sva_s_nexttime || id == ID_sva_indexed_nexttime || + id == ID_sva_until || id == ID_sva_s_until || + id == ID_sva_until_with || id == ID_sva_s_until_with || + id == ID_sva_eventually || id == ID_sva_s_eventually || + id == ID_sva_ranged_s_eventually || id == ID_sva_cycle_delay || + id == ID_sva_overlapped_followed_by || id == ID_sva_nonoverlapped_followed_by; }