From ecfc453af51bf5fc9cbbaa0ae09766c74cc9a38f Mon Sep 17 00:00:00 2001
From: TaoBi22 <beahealy22@gmail.com>
Date: Tue, 19 Sep 2023 16:50:50 +0100
Subject: [PATCH] Support `seq.clock`

---
 include/circt/LogicalEquivalence/Circuit.h |  1 +
 integration_test/circt-mc/seq.mlir         |  7 ++++---
 lib/LogicalEquivalence/Circuit.cpp         | 14 ++++++++++++--
 lib/LogicalEquivalence/LogicExporter.cpp   | 12 ++++++++++++
 4 files changed, 29 insertions(+), 5 deletions(-)

diff --git a/include/circt/LogicalEquivalence/Circuit.h b/include/circt/LogicalEquivalence/Circuit.h
index 7a792b6a64a8..5e5ea361ad86 100644
--- a/include/circt/LogicalEquivalence/Circuit.h
+++ b/include/circt/LogicalEquivalence/Circuit.h
@@ -85,6 +85,7 @@ class Solver::Circuit {
                       mlir::Value reset, mlir::Value resetValue);
   void performFirReg(mlir::Value next, mlir::Value clk, mlir::Value data,
                      mlir::Value reset, mlir::Value resetValue);
+  void performFromClock(mlir::Value result, mlir::Value input);
 
   // `verif` dialect operations.
   void performAssert(mlir::Value property);
diff --git a/integration_test/circt-mc/seq.mlir b/integration_test/circt-mc/seq.mlir
index dbbef8383d4a..b64e44a44c63 100644
--- a/integration_test/circt-mc/seq.mlir
+++ b/integration_test/circt-mc/seq.mlir
@@ -4,11 +4,12 @@
 //  RUN: circt-mc %s -b 10 --module ClkProp | FileCheck %s --check-prefix=CLKPROP
 //  CLKPROP: Success!
 
-hw.module @ClkProp(%i0: i1, %clk: i1) {
+hw.module @ClkProp(%clk: !seq.clock, %i0: i1) {
   %reg = seq.compreg %i0, %clk : i1
   // Condition (equivalent to %clk -> %reg == %i0)
-  %c-1_i1 = hw.constant -1 : i1 
-  %nclk = comb.xor bin %clk, %c-1_i1 : i1
+  %c-1_i1 = hw.constant -1 : i1
+  %clk_i1 = seq.from_clock %clk
+  %nclk = comb.xor bin %clk_i1, %c-1_i1 : i1
   %eq = comb.icmp bin eq %i0, %reg : i1
   %imp = comb.or bin %nclk, %eq : i1
   verif.assert %imp : i1
diff --git a/lib/LogicalEquivalence/Circuit.cpp b/lib/LogicalEquivalence/Circuit.cpp
index 3287b9bca907..f329960a6057 100644
--- a/lib/LogicalEquivalence/Circuit.cpp
+++ b/lib/LogicalEquivalence/Circuit.cpp
@@ -486,8 +486,9 @@ z3::expr Solver::Circuit::fetchOrAllocateExpr(Value value) {
     auto nameInsertion = nameTable.insert(std::pair(value, valueName));
     assert(nameInsertion.second && "Name not inserted in state table");
     Type type = value.getType();
-    assert(type.isSignlessInteger() && "Unsupported type");
-    unsigned int width = type.getIntOrFloatBitWidth();
+    auto isClockType = hw::type_isa<seq::ClockType>(type);
+    assert((type.isSignlessInteger() || isClockType) && "Unsupported type");
+    unsigned int width = isClockType ? 1 : type.getIntOrFloatBitWidth();
     // Technically allowed for the `hw` dialect but
     // disallowed for `comb` operations; should check separately.
     assert(width > 0 && "0-width integers are not supported"); // NOLINT
@@ -845,6 +846,15 @@ void Solver::Circuit::performFirReg(mlir::Value next, mlir::Value clk,
   addClk(clk);
 }
 
+void Solver::Circuit::performFromClock(mlir::Value result, mlir::Value input) {
+  z3::expr resultState = fetchOrAllocateExpr(result);
+  z3::expr inputState = fetchOrAllocateExpr(input);
+  // Constrain the result directly to the input's value
+  constrainResult(result, inputState);
+  combTransformTable.insert(std::pair(
+      result, std::pair(std::make_tuple(input), [](auto op1) { return op1; })));
+}
+
 //===----------------------------------------------------------------------===//
 // `seq` dialect operations
 //===----------------------------------------------------------------------===//
diff --git a/lib/LogicalEquivalence/LogicExporter.cpp b/lib/LogicalEquivalence/LogicExporter.cpp
index de48a152f880..9e0e97845c3f 100644
--- a/lib/LogicalEquivalence/LogicExporter.cpp
+++ b/lib/LogicalEquivalence/LogicExporter.cpp
@@ -270,6 +270,9 @@ struct Visitor : public hw::StmtVisitor<Visitor, LogicalResult>,
             .Case<circt::seq::FirRegOp>([&](circt::seq::FirRegOp &op) {
               return visitSeqOp(op, circuit);
             })
+            .Case<circt::seq::FromClockOp>([&](circt::seq::FromClockOp &op) {
+              return visitSeqOp(op, circuit);
+            })
             .Default([&](mlir::Operation *op) { return visitUnhandledOp(op); });
     return outcome;
   }
@@ -296,6 +299,15 @@ struct Visitor : public hw::StmtVisitor<Visitor, LogicalResult>,
     circuit->performCompReg(next, clk, data, reset, resetValue);
     return mlir::success();
   }
+
+  mlir::LogicalResult visitSeqOp(circt::seq::FromClockOp &op,
+                                 Solver::Circuit *circuit) {
+    mlir::Value result = op.getResult();
+    mlir::Value input = op.getInput();
+    // circuit->performCompReg(next, clk, data, reset, resetValue);
+    circuit->performFromClock(result, input);
+    return mlir::success();
+  }
 };
 } // namespace