Add seq support

llvm · Oct 15, 2024 · 7e5a64f · 7e5a64f
1 parent 82ec180
commit 7e5a64f
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 5 deletions.
diff --git a/lib/Dialect/Verif/Transforms/LowerFormalToHW.cpp b/lib/Dialect/Verif/Transforms/LowerFormalToHW.cpp
@@ -9,6 +9,7 @@
 //
 //===----------------------------------------------------------------------===//
 #include "circt/Dialect/Comb/CombDialect.h"
+#include "circt/Dialect/Seq/SeqDialect.h"
 #include "circt/Dialect/Verif/VerifOps.h"
 #include "circt/Dialect/Verif/VerifPasses.h"
 
@@ -72,8 +73,8 @@ struct FormalOpConversionPattern : public OpConversionPattern<verif::FormalOp> {
 void LowerFormalToHW::runOnOperation() {
   auto &context = getContext();
   mlir::ConversionTarget target(context);
-  target
-      .addLegalDialect<hw::HWDialect, verif::VerifDialect, comb::CombDialect>();
+  target.addLegalDialect<hw::HWDialect, verif::VerifDialect, comb::CombDialect,
+                         seq::SeqDialect>();
   target.addIllegalOp<verif::FormalOp, verif::SymbolicValueOp>();
 
   RewritePatternSet patterns(&context);

diff --git a/test/Dialect/Verif/lower-formal-to-hw.mlir b/test/Dialect/Verif/lower-formal-to-hw.mlir
@@ -1,6 +1,6 @@
 // RUN: circt-opt --lower-formal-to-hw %s | FileCheck %s
 
-hw.module @Foo(in %bar : i32, in %baz : i16) {}
+hw.module @Foo(in %bar : i32, in %baz : i16, in %clk : !seq.clock) {}
 
 // CHECK-LABEL: hw.module @FormalTop(in %symbolic_value_0 : i32, in %symbolic_value_1 : i16)
 verif.formal @FormalTop {
@@ -9,6 +9,8 @@ verif.formal @FormalTop {
   %2 = comb.extract %0 from 16 :  (i32) -> i16
   // CHECK: [[RES:%[0-9]+]] = comb.xor
   %3 = comb.xor %1, %2 : i16
-  // CHECK-NEXT: hw.instance "foo" @Foo(bar: %symbolic_value_0: i32, baz: [[RES]]: i16)
-  hw.instance "foo" @Foo(bar: %0: i32, baz: %3: i16) -> ()
+  // CHECK: [[CLK:%[0-9]+]] = seq.const_clock high
+  %high = seq.const_clock high
+  // CHECK-NEXT: hw.instance "foo" @Foo(bar: %symbolic_value_0: i32, baz: [[RES]]: i16, clk: [[CLK]]: !seq.clock)
+  hw.instance "foo" @Foo(bar: %0: i32, baz: %3: i16, clk: %high: !seq.clock) -> ()
 }