[Verif] LowerContractsPass (#7870)

Co-authored-by: Martin Erhart <martin.erhart@sifive.com>
Co-authored-by: Fabian Schuiki <fabian@schuiki.ch>

Author: 3 people

include/circt/Dialect/Verif/CMakeLists.txt

@@ -6,6 +6,7 @@ mlir_tablegen(VerifEnums.h.inc -gen-enum-decls)
 mlir_tablegen(VerifEnums.cpp.inc -gen-enum-defs)
 add_public_tablegen_target(CIRCTVerifEnumsIncGen)
 add_dependencies(circt-headers CIRCTVerifEnumsIncGen)
+add_circt_interface(VerifOpInterfaces)
 
 set(LLVM_TARGET_DEFINITIONS Passes.td)
 mlir_tablegen(Passes.h.inc -gen-pass-decls)

include/circt/Dialect/Verif/Passes.td

@@ -42,4 +42,33 @@ def LowerFormalToHWPass : Pass<"lower-formal-to-hw", "mlir::ModuleOp"> {
   }];
 }
 
+def LowerContractsPass : Pass<"lower-contracts", "mlir::ModuleOp"> {
+  let summary = "Lower contracts into formal tests";
+  let description = [{
+    For `hw.module` ops containing any `verif.contract` ops, apply the
+    contracts in the `hw.module` body and emit a `verif.formal` op that checks
+    each applied contract.
+
+    Contracts are checked by turning `require`s into `assume`s and `ensure`s
+    into `asserts`s.  Inputs to the `hw.module` op are replaced with
+    `verif.symbolic_value` ops and other contracts are assumed to hold by
+    inlining the contract body.
+
+    Contracts are applied by turning `require`s into `assert`s and `ensure`s
+    into `assume`s in the original `hw.module` op body.  Results of the
+    contract are replaced with `verif.symbolic_value` ops.  In some cases,
+    using the `SimplifyAssumeEqPass` after lowering contracts and before
+    canonicalization and cse can result in a greatly simplified `hw.module` op
+    body.
+  }];
+}
+
+def SimplifyAssumeEqPass : Pass<"simplify-assume-eq", "hw::HWModuleOp"> {
+  let summary = "Use assume equal statements to simplify symbolic values";
+  let description = [{
+    When a symbolic value is assumed equal to another value, the symbolic value
+    is replaced with its equal value to simplify.
+  }];
+}
+
 #endif // CIRCT_DIALECT_VERIF_PASSES_TD

include/circt/Dialect/Verif/VerifOpInterfaces.h

@@ -0,0 +1,28 @@
+//===- VerifOpInterfaces.h - TODO ---------------===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+//
+// This file contains the Object Model operation declarations.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef CIRCT_DIALECT_VERIF_VERIFOPINTERFACES_H
+#define CIRCT_DIALECT_VERIF_VERIFOPINTERFACES_H
+
+#include "circt/Dialect/LTL/LTLTypes.h"
+#include "mlir/IR/OpDefinition.h"
+#include "mlir/IR/OpImplementation.h"
+
+namespace circt {
+namespace verif {
+class RequireLike;
+} // namespace verif
+} // namespace circt
+
+#include "circt/Dialect/Verif/VerifOpInterfaces.h.inc"
+
+#endif // CIRCT_DIALECT_VERIF_VERIFOPINTERFACES_H

include/circt/Dialect/Verif/VerifOpInterfaces.td

@@ -0,0 +1,25 @@
+#ifndef CIRCT_DIALECT_VERIF_VERIFOPINTERFACES_TD
+#define CIRCT_DIALECT_VERIF_VERIFOPINTERFACES_TD
+
+include "mlir/IR/OpBase.td"
+
+def RequireLike : OpInterface<"RequireLike"> {
+  let cppNamespace = "circt::verif";
+
+  let description = [{
+    Common functionality for require-like operations.
+  }];
+
+  let methods = [
+    InterfaceMethod<"Get the label",
+      "std::optional<llvm::StringRef>", "getLabel", (ins)>,
+    InterfaceMethod<"Get the label attribute",
+      "mlir::StringAttr", "getLabelAttr", (ins)>,
+    InterfaceMethod<"Get the property",
+      "mlir::Value", "getProperty", (ins)>,
+    InterfaceMethod<"Get the enable",
+      "mlir::Value", "getEnable", (ins)>,
+  ];
+}
+
+#endif // CIRCT_DIALECT_VERIF_VERIFOPINTERFACES_TD

include/circt/Dialect/Verif/VerifOps.h

@@ -15,6 +15,7 @@
 #include "circt/Dialect/HW/HWTypes.h"
 #include "circt/Dialect/Seq/SeqTypes.h"
 #include "circt/Dialect/Verif/VerifDialect.h"
+#include "circt/Dialect/Verif/VerifOpInterfaces.h"
 #include "mlir/Bytecode/BytecodeOpInterface.h"
 #include "mlir/Interfaces/InferTypeOpInterface.h"
 

include/circt/Dialect/Verif/VerifOps.td

@@ -10,6 +10,7 @@
 #define CIRCT_DIALECT_VERIF_VERIFOPS_TD
 
 include "circt/Dialect/Verif/VerifDialect.td"
+include "circt/Dialect/Verif/VerifOpInterfaces.td"
 include "circt/Dialect/LTL/LTLDialect.td"
 include "circt/Dialect/LTL/LTLTypes.td"
 include "circt/Dialect/HW/HWTypes.td"
@@ -346,7 +347,7 @@ def FormalOp : VerifOp<"formal", [
 }
 
 def SymbolicValueOp : VerifOp<"symbolic_value", [
-  HasParent<"verif::FormalOp">,
+  ParentOneOf<["verif::FormalOp", "hw::HWModuleOp"]>,
 ]>{
   let summary = "Create a symbolic value for formal verification";
   let description = [{
@@ -405,6 +406,7 @@ def ContractOp : VerifOp<"contract", [
 class RequireLikeOp<string mnemonic> : VerifOp<mnemonic, [
   AttrSizedOperandSegments,
   HasParent<"verif::ContractOp">,
+  DeclareOpInterfaceMethods<RequireLike>
 ]> {
   let arguments = (ins
     LTLAnyPropertyType:$property,

include/circt/Dialect/Verif/VerifPasses.h

@@ -21,6 +21,7 @@
 namespace circt {
 namespace verif {
 class FormalOp;
+class RequireLike;
 } // namespace verif
 } // namespace circt
 

lib/Dialect/Verif/CMakeLists.txt

@@ -1,12 +1,14 @@
 add_circt_dialect_library(CIRCTVerif
   VerifDialect.cpp
   VerifOps.cpp
+  VerifOpInterfaces.cpp
 
   ADDITIONAL_HEADER_DIRS
   ${CIRCT_MAIN_INCLUDE_DIR}/circt/Dialect/Verif
 
   DEPENDS
   MLIRVerifIncGen
+  MLIRVerifOpInterfacesIncGen
 
   LINK_COMPONENTS
   Support

lib/Dialect/Verif/Transforms/CMakeLists.txt

@@ -2,6 +2,8 @@ add_circt_dialect_library(CIRCTVerifTransforms
   VerifyClockedAssertLike.cpp
   PrepareForFormal.cpp
   LowerFormalToHW.cpp
+  LowerContracts.cpp
+  SimplifyAssumeEq.cpp
 
   DEPENDS
   CIRCTVerifTransformsIncGen