[ImportVerilog] Modify sampled value functions to use Comb operators (llvm#9656)

Author: Arya-Golkari

lib/Conversion/ImportVerilog/AssertionExpr.cpp

@@ -309,27 +309,26 @@ FailureOr<Value> Context::convertAssertionSystemCallArity1(
                   auto past =
                       ltl::PastOp::create(builder, loc, value, 1, Value{})
                           .getResult();
-                  auto notCurrent =
-                      ltl::NotOp::create(builder, loc, current).getResult();
-                  auto pastAndNotCurrent =
-                      ltl::AndOp::create(builder, loc, {notCurrent, past})
-                          .getResult();
-                  return pastAndNotCurrent;
+                  auto fell = comb::ICmpOp::create(builder, loc,
+                                                   comb::ICmpPredicate::ugt,
+                                                   past, current, false)
+                                  .getResult();
+                  return fell;
                 })
           // Translate $rose to x[0] ∧ ¬x[-1]
           .Case("$rose",
                 [&]() -> Value {
                   auto past =
                       ltl::PastOp::create(builder, loc, value, 1, Value{})
                           .getResult();
-                  auto notPast = comb::createOrFoldNot(loc, past, builder);
                   auto current = value;
-                  auto notPastAndCurrent =
-                      ltl::AndOp::create(builder, loc, {current, notPast})
-                          .getResult();
-                  return notPastAndCurrent;
+                  auto rose = comb::ICmpOp::create(builder, loc,
+                                                   comb::ICmpPredicate::ult,
+                                                   past, current, false)
+                                  .getResult();
+                  return rose;
                 })
-          // Translate $changed to x[0] != x[-1]
+          // Translate $changed to ( ¬x[0] ∧ x[-1] ) ⋁ ( x[0] ∧ ¬x[-1] )
           .Case("$changed",
                 [&]() -> Value {
                   auto past =
@@ -338,7 +337,8 @@ FailureOr<Value> Context::convertAssertionSystemCallArity1(
                   auto current = value;
                   auto changed = comb::ICmpOp::create(builder, loc,
                                                       comb::ICmpPredicate::ne,
-                                                      past, current, false);
+                                                      past, current, false)
+                                     .getResult();
                   return changed;
                 })
           // Translate $stable to ( x[0] ∧ x[-1] ) ⋁ ( ¬x[0] ∧ ¬x[-1] )
@@ -347,21 +347,11 @@ FailureOr<Value> Context::convertAssertionSystemCallArity1(
                   auto past =
                       ltl::PastOp::create(builder, loc, value, 1, Value{})
                           .getResult();
-                  auto notPast =
-                      ltl::NotOp::create(builder, loc, past).getResult();
                   auto current = value;
-                  auto notCurrent =
-                      ltl::NotOp::create(builder, loc, value).getResult();
-                  auto pastAndCurrent =
-                      ltl::AndOp::create(builder, loc, {current, past})
-                          .getResult();
-                  auto notPastAndNotCurrent =
-                      ltl::AndOp::create(builder, loc, {notCurrent, notPast})
-                          .getResult();
-                  auto stable =
-                      ltl::OrOp::create(builder, loc,
-                                        {pastAndCurrent, notPastAndNotCurrent})
-                          .getResult();
+                  auto stable = comb::ICmpOp::create(builder, loc,
+                                                     comb::ICmpPredicate::eq,
+                                                     past, current, false)
+                                    .getResult();
                   return stable;
                 })
           .Case("$past",

test/Conversion/ImportVerilog/builtins.sv

@@ -387,9 +387,7 @@ module SampleValueBuiltins #() (
   // CHECK-NEXT: [[C2_INT:%.+]] = moore.logic_to_int [[C2]] : l1
   // CHECK-NEXT: [[CURRENT:%.+]] = moore.to_builtin_int [[C2_INT]] : i1
   // CHECK-NEXT: [[PAST:%.+]] = ltl.past [[CURRENT]], 1 : i1
-  // CHECK-NEXT: [[TRUE:%.+]] = hw.constant true
-  // CHECK-NEXT: [[NOTPAST:%.+]] = comb.xor [[PAST]], [[TRUE]] : i1
-  // CHECK-NEXT: [[NOTPASTANDCURRENT:%.+]] = ltl.and [[CURRENT]], [[NOTPAST]] : i1, i1
+  // CHECK-NEXT: [[ROSE:%.+]] = comb.icmp ult [[PAST]], [[CURRENT]] : i1
   rising_clk: assert property (@(posedge clk_i) clk_i |=> $rose(clk_i));
   // CHECK: moore.procedure always {
   // CHECK-NEXT: [[C:%.+]] = moore.read [[CLKWIRE]] : <l1>
@@ -399,8 +397,7 @@ module SampleValueBuiltins #() (
   // CHECK-NEXT: [[C2_INT:%.+]] = moore.logic_to_int [[C2]] : l1
   // CHECK-NEXT: [[CURRENT:%.+]] = moore.to_builtin_int [[C2_INT]] : i1
   // CHECK-NEXT: [[PAST:%.+]] = ltl.past [[CURRENT]], 1 : i1
-  // CHECK-NEXT: [[NOTCURRENT:%.+]] = ltl.not [[CURRENT]] : i1
-  // CHECK-NEXT: [[PASTANDNOTCURRENT:%.+]] = ltl.and [[NOTCURRENT]], [[PAST]] : !ltl.property, i1
+  // CHECK-NEXT: [[FELL:%.+]] = comb.icmp ugt [[PAST]], [[CURRENT]] : i1
   falling_clk: assert property (@(posedge clk_i) clk_i |=> $fell(clk_i));
   // CHECK: moore.procedure always {
   // CHECK-NEXT: [[C:%.+]] = moore.read [[CLKWIRE]] : <l1>
@@ -410,11 +407,7 @@ module SampleValueBuiltins #() (
   // CHECK-NEXT: [[C2_INT:%.+]] = moore.logic_to_int [[C2]] : l1
   // CHECK-NEXT: [[CURRENT:%.+]] = moore.to_builtin_int [[C2_INT]] : i1
   // CHECK-NEXT: [[PAST:%.+]] = ltl.past [[CURRENT]], 1 : i1
-  // CHECK-NEXT: [[NOTPAST:%.+]] = ltl.not [[PAST]] : i1
-  // CHECK-NEXT: [[NOTCURRENT:%.+]] = ltl.not [[CURRENT]] : i1
-  // CHECK-NEXT: [[PASTANDCURRENT:%.+]] = ltl.and [[CURRENT]], [[PAST]] : i1, i1
-  // CHECK-NEXT: [[NOTPASTANDNOTCURRENT:%.+]] = ltl.and [[NOTCURRENT]], [[NOTPAST]] : !ltl.property, !ltl.property
-  // CHECK-NEXT: [[STABLE:%.+]] = ltl.or [[PASTANDCURRENT]], [[NOTPASTANDNOTCURRENT]] : i1, !ltl.property
+  // CHECK-NEXT: [[STABLE:%.+]] = comb.icmp eq [[PAST]], [[CURRENT]] : i1
   stable_clk: assert property (@(posedge clk_i) clk_i |=> $stable(clk_i));
   // CHECK: moore.procedure always {
   // CHECK-NEXT: [[C:%.+]] = moore.read [[CLKWIRE]] : <l1>
@@ -424,7 +417,7 @@ module SampleValueBuiltins #() (
   // CHECK-NEXT: [[C2_INT:%.+]] = moore.logic_to_int [[C2]] : l1
   // CHECK-NEXT: [[CURRENT:%.+]] = moore.to_builtin_int [[C2_INT]] : i1
   // CHECK-NEXT: [[PAST:%.+]] = ltl.past [[CURRENT]], 1 : i1
-  // CHECK-NEXT: [[STABLE:%.+]] = comb.icmp ne [[PAST]], [[CURRENT]] : i1
+  // CHECK-NEXT: [[CHANGED:%.+]] = comb.icmp ne [[PAST]], [[CURRENT]] : i1
   changed_clk: assert property (@(posedge clk_i) clk_i |=> $changed(clk_i));
   // CHECK: moore.procedure always {
   // CHECK-NEXT: [[C:%.+]] = moore.read [[CLKWIRE]] : <l1>