[circt-lec] Register Verif dialects (#7744)

verif.assume can be used to annotate pre-condtion directly in the IR. This is quite useful when verifying transformation which involves undefined values. For example when lowering comb.shl to AIG, the conversion pass chooses arbitary values for out-of-bounds situation. So we cannot verify the equivalence unless we specify the pre-condtion with verif.assume
llvm · Oct 28, 2024 · b79242d · b79242d
1 parent c698369
commit b79242d
Show file tree

Hide file tree

Showing 3 changed files with 15 additions and 3 deletions.
diff --git a/integration_test/circt-lec/comb.mlir b/integration_test/circt-lec/comb.mlir
@@ -80,8 +80,10 @@ hw.module @divs(in %in1: i32, in %in2: i32, out out: i32) {
 // comb.divu
 // RUN: circt-lec %s -c1=divu_unsafe -c2=divu_unsafe --shared-libs=%libz3 | FileCheck %s --check-prefix=COMB_DIVU_UNSAFE
 // RUN: circt-lec %s -c1=divu -c2=divu --shared-libs=%libz3 | FileCheck %s --check-prefix=COMB_DIVU
+// RUN: circt-lec %s -c1=divu_assume -c2=divu_assume --shared-libs=%libz3 | FileCheck %s --check-prefix=COMB_DIVU_ASSUME
 // COMB_DIVU_UNSAFE: c1 != c2
 // COMB_DIVU: c1 == c2
+// COMB_DIVU_ASSUME: c1 == c2
 
 hw.module @divu_unsafe(in %in1: i32, in %in2: i32, out out: i32) {
   %0 = comb.divu %in1, %in2 : i32
@@ -96,6 +98,14 @@ hw.module @divu(in %in1: i32, in %in2: i32, out out: i32) {
   hw.output %3 : i32
 }
 
+hw.module @divu_assume(in %in1: i32, in %in2: i32, out out: i32) {
+  %0 = hw.constant 0 : i32
+  %1 = comb.icmp ne %in2, %0 : i32
+  verif.assume %1 : i1
+  %2 = comb.divu %in1, %in2 : i32
+  hw.output %2 : i32
+}
+
 // comb.extract
 // TODO
 

diff --git a/tools/circt-lec/CMakeLists.txt b/tools/circt-lec/CMakeLists.txt
@@ -21,6 +21,7 @@ target_link_libraries(circt-lec
   CIRCTHW
   CIRCTSMT
   CIRCTSupport
+  CIRCTVerif
   MLIRIR
   MLIRFuncDialect
   MLIRArithDialect

diff --git a/tools/circt-lec/circt-lec.cpp b/tools/circt-lec/circt-lec.cpp
@@ -19,6 +19,7 @@
 #include "circt/Dialect/Comb/CombDialect.h"
 #include "circt/Dialect/HW/HWDialect.h"
 #include "circt/Dialect/SMT/SMTDialect.h"
+#include "circt/Dialect/Verif/VerifDialect.h"
 #include "circt/Support/Passes.h"
 #include "circt/Support/Version.h"
 #include "circt/Tools/circt-lec/Passes.h"
@@ -352,9 +353,9 @@ int main(int argc, char **argv) {
   // Register the supported CIRCT dialects and create a context to work with.
   DialectRegistry registry;
   registry.insert<circt::comb::CombDialect, circt::hw::HWDialect,
-                  circt::smt::SMTDialect, mlir::func::FuncDialect,
-                  mlir::LLVM::LLVMDialect, mlir::arith::ArithDialect,
-                  mlir::BuiltinDialect>();
+                  circt::smt::SMTDialect, circt::verif::VerifDialect,
+                  mlir::func::FuncDialect, mlir::LLVM::LLVMDialect,
+                  mlir::arith::ArithDialect, mlir::BuiltinDialect>();
   mlir::func::registerInlinerExtension(registry);
   mlir::registerBuiltinDialectTranslation(registry);
   mlir::registerLLVMDialectTranslation(registry);