SVA: move rewrites for state-formula SVA into separate file

src/temporal-logic/Makefile

@@ -1,6 +1,7 @@
 SRC = nnf.cpp \
       normalize_property.cpp \
       temporal_logic.cpp \
+      trivial_sva.cpp \
       #empty line
 
 include ../config.inc

src/temporal-logic/normalize_property.cpp

@@ -16,6 +16,7 @@ Author: Daniel Kroening, dkr@amazon.com
 
 #include "temporal_expr.h"
 #include "temporal_logic.h"
+#include "trivial_sva.h"
 
 exprt normalize_pre_not(not_exprt expr)
 {
@@ -73,16 +74,6 @@ exprt normalize_pre_implies(implies_exprt expr)
   return or_exprt{not_exprt{expr.lhs()}, expr.rhs()};
 }
 
-exprt normalize_pre_sva_overlapped_implication(
-  sva_overlapped_implication_exprt expr)
-{
-  // Same as regular implication if lhs is not a sequence.
-  if(!is_SVA_sequence(expr.lhs()))
-    return or_exprt{not_exprt{expr.lhs()}, expr.rhs()};
-  else
-    return std::move(expr);
-}
-
 exprt normalize_pre_sva_non_overlapped_implication(
   sva_non_overlapped_implication_exprt expr)
 {
@@ -97,30 +88,6 @@ exprt normalize_pre_sva_non_overlapped_implication(
     return std::move(expr);
 }
 
-exprt normalize_pre_sva_not(sva_not_exprt expr)
-{
-  // Same as regular 'not'. These do not apply to sequences.
-  return normalize_pre_not(not_exprt{expr.op()});
-}
-
-exprt normalize_pre_sva_and(sva_and_exprt expr)
-{
-  // Same as a ∧ b if lhs and rhs are not sequences.
-  if(!is_SVA_sequence(expr.lhs()) && !is_SVA_sequence(expr.rhs()))
-    return and_exprt{expr.lhs(), expr.rhs()};
-  else
-    return std::move(expr);
-}
-
-exprt normalize_pre_sva_or(sva_or_exprt expr)
-{
-  // Same as a ∧ b if lhs or rhs are not sequences.
-  if(!is_SVA_sequence(expr.lhs()) && !is_SVA_sequence(expr.rhs()))
-    return or_exprt{expr.lhs(), expr.rhs()};
-  else
-    return std::move(expr);
-}
-
 exprt normalize_pre_sva_cycle_delay(sva_cycle_delay_exprt expr)
 {
   if(expr.is_unbounded())
@@ -143,37 +110,16 @@ exprt normalize_pre_sva_cycle_delay(sva_cycle_delay_exprt expr)
     return std::move(expr);
 }
 
-exprt normalize_property(exprt expr)
+exprt normalize_property_rec(exprt expr)
 {
   // pre-traversal
   if(expr.id() == ID_not)
     expr = normalize_pre_not(to_not_expr(expr));
   else if(expr.id() == ID_implies)
     expr = normalize_pre_implies(to_implies_expr(expr));
-  else if(expr.id() == ID_sva_cover)
-    expr = G_exprt{not_exprt{to_sva_cover_expr(expr).op()}};
-  else if(expr.id() == ID_sva_overlapped_implication)
-    expr = normalize_pre_sva_overlapped_implication(
-      to_sva_overlapped_implication_expr(expr));
   else if(expr.id() == ID_sva_non_overlapped_implication)
     expr = normalize_pre_sva_non_overlapped_implication(
       to_sva_non_overlapped_implication_expr(expr));
-  else if(expr.id() == ID_sva_iff)
-  {
-    expr =
-      equal_exprt{to_sva_iff_expr(expr).lhs(), to_sva_iff_expr(expr).rhs()};
-  }
-  else if(expr.id() == ID_sva_implies)
-  {
-    expr = implies_exprt{
-      to_sva_implies_expr(expr).lhs(), to_sva_implies_expr(expr).rhs()};
-  }
-  else if(expr.id() == ID_sva_and)
-    expr = normalize_pre_sva_and(to_sva_and_expr(expr));
-  else if(expr.id() == ID_sva_not)
-    expr = normalize_pre_sva_not(to_sva_not_expr(expr));
-  else if(expr.id() == ID_sva_or)
-    expr = normalize_pre_sva_or(to_sva_or_expr(expr));
   else if(expr.id() == ID_sva_nexttime)
   {
     auto one = natural_typet{}.one_expr();
@@ -209,40 +155,6 @@ exprt normalize_property(exprt expr)
   {
     expr = sva_s_eventually_exprt{to_sva_cycle_delay_star_expr(expr).op()};
   }
-  else if(expr.id() == ID_sva_sequence_concatenation)
-  {
-    auto &sequence_concatenation = to_sva_sequence_concatenation_expr(expr);
-    if(!is_SVA_sequence(sequence_concatenation.lhs()))
-    {
-      // a ##0 b --> a && b if a is not a sequence
-      expr =
-        and_exprt{sequence_concatenation.lhs(), sequence_concatenation.rhs()};
-    }
-  }
-  else if(expr.id() == ID_sva_if)
-  {
-    auto &sva_if_expr = to_sva_if_expr(expr);
-    auto false_case = sva_if_expr.false_case().is_nil()
-                        ? true_exprt{}
-                        : sva_if_expr.false_case();
-    expr = if_exprt{sva_if_expr.cond(), sva_if_expr.true_case(), false_case};
-  }
-  else if(expr.id() == ID_sva_disable_iff)
-  {
-    auto &disable_iff_expr = to_sva_disable_iff_expr(expr);
-    expr = or_exprt{disable_iff_expr.lhs(), disable_iff_expr.rhs()};
-  }
-  else if(expr.id() == ID_sva_accept_on || expr.id() == ID_sva_sync_accept_on)
-  {
-    auto &sva_abort_expr = to_sva_abort_expr(expr);
-    expr = or_exprt{sva_abort_expr.condition(), sva_abort_expr.property()};
-  }
-  else if(expr.id() == ID_sva_reject_on || expr.id() == ID_sva_sync_reject_on)
-  {
-    auto &sva_abort_expr = to_sva_abort_expr(expr);
-    expr = and_exprt{
-      not_exprt{sva_abort_expr.condition()}, sva_abort_expr.property()};
-  }
   else if(expr.id() == ID_sva_strong)
   {
     expr = to_sva_strong_expr(expr).op();
@@ -251,16 +163,26 @@ exprt normalize_property(exprt expr)
   {
     expr = to_sva_weak_expr(expr).op();
   }
-  else if(expr.id() == ID_sva_case)
-  {
-    expr = to_sva_case_expr(expr).lowering();
-  }
 
   // normalize the operands
   for(auto &op : expr.operands())
-    op = normalize_property(op);
+    op = normalize_property_rec(op); // recursive call
 
   // post-traversal
 
   return expr;
 }
+
+exprt normalize_property(exprt expr)
+{
+  // top-level only
+  if(expr.id() == ID_sva_cover)
+    expr = G_exprt{not_exprt{to_sva_cover_expr(expr).op()}};
+
+  expr = trivial_sva(expr);
+
+  // now do recursion
+  expr = normalize_property_rec(expr);
+
+  return expr;
+}

src/temporal-logic/normalize_property.h

@@ -21,30 +21,17 @@ Author: Daniel Kroening, dkr@amazon.com
 /// (a -> b) --> ¬a ∨ b
 ///
 /// -----SVA-----
-/// a sva_iff b --> a <-> b
-/// a sva_implies b --> a -> b
-/// sva_not a --> ¬a
-/// a sva_and b --> a ∧ b                                   if a and b are not SVA sequences
-/// a sva_or b --> a ∨ b                                    if a and b are not SVA sequences
-/// sva_overlapped_implication --> ¬a ∨ b                   if a is not an SVA sequence
 /// sva_non_overlapped_implication --> ¬a ∨ always[1:1] b   if a is not an SVA sequence
 /// sva_nexttime φ --> sva_always[1:1] φ
 /// sva_nexttime[i] φ --> sva_always[i:i] φ
 /// sva_s_nexttime φ --> sva_always[1:1] φ
 /// sva_s_nexttime[i] φ --> sva_s_always[i:i] φ
-/// sva_if --> ? :
 /// ##[0:$] φ --> s_eventually φ
 /// ##[i:$] φ --> s_nexttime[i] s_eventually φ
 /// ##[*] φ --> s_eventually φ
 /// ##[+] φ --> always[1:1] s_eventually φ
 /// strong(φ) --> φ
 /// weak(φ) --> φ
-/// sva_case --> ? :
-/// a sva_disable_iff b --> a ∨ b
-/// a sva_accept_on b --> a ∨ b
-/// a sva_reject_on b --> ¬a ∧ b
-/// a sva_sync_accept_on b --> a ∨ b
-/// a sva_sync_reject_on b --> ¬a ∧ b
 /// ¬ sva_s_eventually φ --> sva_always ¬φ
 /// ¬ sva_always φ --> sva_s_eventually ¬φ
 ///

src/temporal-logic/trivial_sva.cpp

@@ -0,0 +1,94 @@
+/*******************************************************************\
+
+Module: Trivial SVA
+
+Author: Daniel Kroening, dkr@amazon.com
+
+\*******************************************************************/
+
+#include "trivial_sva.h"
+
+#include <verilog/sva_expr.h>
+
+#include "temporal_logic.h"
+
+exprt trivial_sva(exprt expr)
+{
+  // pre-traversal
+  if(expr.id() == ID_sva_overlapped_implication)
+  {
+    // Same as regular implication if lhs and rhs are not sequences.
+    auto &sva_implication = to_sva_overlapped_implication_expr(expr);
+    if(
+      !is_SVA_sequence(sva_implication.lhs()) &&
+      !is_SVA_sequence(sva_implication.rhs()))
+    {
+      expr = implies_exprt{sva_implication.lhs(), sva_implication.rhs()};
+    }
+  }
+  else if(expr.id() == ID_sva_iff)
+  {
+    auto &sva_iff = to_sva_iff_expr(expr);
+    expr = equal_exprt{sva_iff.lhs(), sva_iff.rhs()};
+  }
+  else if(expr.id() == ID_sva_implies)
+  {
+    auto &sva_implies = to_sva_implies_expr(expr);
+    expr = implies_exprt{sva_implies.lhs(), sva_implies.rhs()};
+  }
+  else if(expr.id() == ID_sva_and)
+  {
+    // Same as a ∧ b if lhs and rhs are not sequences.
+    auto &sva_and = to_sva_and_expr(expr);
+    if(!is_SVA_sequence(sva_and.lhs()) && !is_SVA_sequence(sva_and.rhs()))
+      expr = and_exprt{sva_and.lhs(), sva_and.rhs()};
+  }
+  else if(expr.id() == ID_sva_or)
+  {
+    // Same as a ∧ b if lhs or rhs are not sequences.
+    auto &sva_or = to_sva_or_expr(expr);
+    if(!is_SVA_sequence(sva_or.lhs()) && !is_SVA_sequence(sva_or.rhs()))
+      expr = or_exprt{sva_or.lhs(), sva_or.rhs()};
+  }
+  else if(expr.id() == ID_sva_not)
+  {
+    // Same as regular 'not'. These do not apply to sequences.
+    expr = not_exprt{to_sva_not_expr(expr).op()};
+  }
+  else if(expr.id() == ID_sva_if)
+  {
+    auto &sva_if_expr = to_sva_if_expr(expr);
+    auto false_case = sva_if_expr.false_case().is_nil()
+                        ? true_exprt{}
+                        : sva_if_expr.false_case();
+    expr = if_exprt{sva_if_expr.cond(), sva_if_expr.true_case(), false_case};
+  }
+  else if(expr.id() == ID_sva_disable_iff)
+  {
+    auto &disable_iff_expr = to_sva_disable_iff_expr(expr);
+    expr = or_exprt{disable_iff_expr.lhs(), disable_iff_expr.rhs()};
+  }
+  else if(expr.id() == ID_sva_accept_on || expr.id() == ID_sva_sync_accept_on)
+  {
+    auto &sva_abort_expr = to_sva_abort_expr(expr);
+    expr = or_exprt{sva_abort_expr.condition(), sva_abort_expr.property()};
+  }
+  else if(expr.id() == ID_sva_reject_on || expr.id() == ID_sva_sync_reject_on)
+  {
+    auto &sva_abort_expr = to_sva_abort_expr(expr);
+    expr = and_exprt{
+      not_exprt{sva_abort_expr.condition()}, sva_abort_expr.property()};
+  }
+  else if(expr.id() == ID_sva_case)
+  {
+    expr = to_sva_case_expr(expr).lowering();
+  }
+
+  // rewrite the operands, recursively
+  for(auto &op : expr.operands())
+    op = trivial_sva(op);
+
+  // post-traversal
+
+  return expr;
+}

src/temporal-logic/trivial_sva.h

@@ -0,0 +1,32 @@
+/*******************************************************************\
+
+Module: Trivial SVA
+
+Author: Daniel Kroening, dkr@amazon.com
+
+\*******************************************************************/
+
+#ifndef CPROVER_TEMPORAL_LOGIC_TRIVIAL_SVA_H
+#define CPROVER_TEMPORAL_LOGIC_TRIVIAL_SVA_H
+
+#include <util/expr.h>
+
+/// This applies the following rewrites, removing SVA operators
+/// that trivial in the sense that they are state predicates only.
+///
+/// a sva_iff b --> a <-> b
+/// a sva_implies b --> a -> b
+/// sva_not a --> ¬a
+/// a sva_and b --> a ∧ b                     if a and b are not sequences
+/// a sva_or b --> a ∨ b                      if a and b are not sequences
+/// sva_overlapped_implication --> a -> b     if a and b are not sequences
+/// sva_if --> ? :
+/// sva_case --> ? :
+/// a sva_disable_iff b --> a ∨ b
+/// a sva_accept_on b --> a ∨ b
+/// a sva_reject_on b --> ¬a ∧ b
+/// a sva_sync_accept_on b --> a ∨ b
+/// a sva_sync_reject_on b --> ¬a ∧ b
+exprt trivial_sva(exprt);
+
+#endif