Skip to content

Commit

Permalink
[Verif] Generalize Formal Contracts (#7495)
Browse files Browse the repository at this point in the history 
* Generalized verif contracts

* updated contract op description
  • Loading branch information
@dobios
dobios authored Aug 12, 2024
1 parent 7f366b0 commit bb6471f
Show file tree
Hide file tree
Showing 3 changed files with 78 additions and 153 deletions.
97 changes: 38 additions & 59 deletions include/circt/Dialect/Verif/VerifOps.td
View file
Original file line number Diff line number Diff line change
Expand Up @@ -251,7 +251,7 @@ def YieldOp : VerifOp<"yield", [
Terminator,
ParentOneOf<[
"verif::LogicEquivalenceCheckingOp", "verif::BoundedModelCheckingOp",
"verif::InstanceOp"
"verif::ContractOp"
]>
]> {
let summary = "yields values from a region";
Expand Down Expand Up @@ -313,7 +313,7 @@ def FormalOp : VerifOp<"formal", [
//===----------------------------------------------------------------------===//

def SymbolicInputOp : VerifOp<"symbolic_input", [
ParentOneOf<["verif::FormalOp", "verif::InstanceOp"]>
ParentOneOf<["verif::FormalOp"]>
]>{
let summary = "declare a symbolic input for formal verification";
let description = [{
Expand Down Expand Up @@ -354,70 +354,46 @@ def ConcreteInputOp : VerifOp<"concrete_input", [
// Formal Contract Ops
//===----------------------------------------------------------------------===//

class ContractLikeOp<string mnemonic, list<Trait> traits = []>
: VerifOp<mnemonic, traits # [
HasParent<"hw::HWModuleOp">, RegionKindInterface, IsolatedFromAbove
]> {

let arguments = (ins Variadic<AnyType>:$inputs);

let regions = (region SizedRegion<1>:$body);

let extraClassDeclaration = [{
/// Implement RegionKindInterface.
static RegionKind getRegionKind(unsigned index) {
return RegionKind::Graph;
}

/// Retrieves the region block arguments
BlockArgument getRegionArg(unsigned index) {
return getBody().front().getArguments()[index];
}

/// Retrieves the number of block arguments
unsigned getNumRegionArgs() {
return getBody().front().getNumArguments();
}
}];

let hasRegionVerifier = 1;
}


def ContractOp : ContractLikeOp<"contract", [NoTerminator]>{
def ContractOp : VerifOp<"contract", [
SingleBlockImplicitTerminator<"verif::YieldOp">,
HasParent<"hw::HWModuleOp">,
RegionKindInterface
]>{
let summary = "declare a formal contract";
let description = [{
This operation declares a formal contract that is used to create precondition
and postconditions on a parent module. These are used as an abstraction to
better modularize formal verification such that each module containing a contract
is checked exactly once. The contract contains a single block where the block arguments
represent the inputs and outputs in the same order as in the module signature.
represent the results of the code block that the contract is abstracting over. The
operands represent the SSA values that this contract's results will replace.

e.g.
```
hw.module @Bar(in %foo : i8, out "" : i8, out "1" : i8) {
verif.contract (%foo) : (i8) {
^bb0(%arg1 : i8, %bar.0 : i8, %bar.1 : i8):
%o0, %o1 = verif.contract (%to0, %to1) : (i8, i8) -> (i8, i8) {
^bb0(%bar.0 : i8, %bar.1 : i8):
%c0_8 = hw.constant 0 : i8
%prec = comb.icmp bin ugt %arg1, %c0_8 : i8
%prec = comb.icmp bin ugt %foo, %c0_8 : i8
verif.require %prec : i1

%post = comb.icmp bin ugt %bar.0, %arg1 : i8
%post1 = comb.icmp bin ult %bar.1, %arg1 : i8
%post = comb.icmp bin ugt %bar.0, %foo : i8
%post1 = comb.icmp bin ult %bar.1, %foo : i8
verif.ensure %post : i1
verif.ensure %post1 : i1
}
verif.yield %bar.0, %bar.1 : i8, i8
}
/* ... Module definition ... */
}
```

This later is used to replace any instance of Bar during verification:
```
%bar.0, %bar.1 = hw.instance "bar" @Bar("foo" : %foo : i8) -> ("" : i8, "1" : i8)
%bar.0, %bar.1 = hw.instance "bar" @Bar("foo" : %c42_8 : i8) -> ("" : i8, "1" : i8)

/* ... After PrepareForFormal Pass becomes ... */

%bar.0, %bar.1 = verif.instance (%c42_8) : (i8) -> (i8, i8) {
%bar.0, %bar.1 = verif.contract (%c42_8) : (i8) -> (i8, i8) {
^bb0(%arg1: i8):
%c0_8 = hw.constant 0 : i8
%prec = comb.icmp bin ugt %arg1, %c0_8 : i8
Expand All @@ -435,29 +411,32 @@ def ContractOp : ContractLikeOp<"contract", [NoTerminator]>{
```
}];

let arguments = (ins Variadic<AnyType>:$inputs);
let results = (outs Variadic<AnyType>:$results);
let regions = (region SizedRegion<1>:$body);

let assemblyFormat = [{
`(` $inputs `)` attr-dict `:` `(` type($inputs) `)` $body
`(` $inputs `)` attr-dict `:` `(` type($inputs) `)` `->` `(` type($results) `)` $body
}];
}

def InstanceOp : ContractLikeOp<"instance", [
SingleBlockImplicitTerminator<"verif::YieldOp">
]>{
let summary = "declare an instance of a formal contract (replace an hw.instance)";
let description = [{
This operation declares an instance of an `hw.module` that contains a
`verif.contract` definition. The body of this op will be a modified version
of the body of the referenced module's contract body, with `verif.require`
ops being reoplaced with `verif.assert` and `verif.ensure` being replaced
with `verif.assume`. The `verif.result` ops are converted into `verif.symbolic_input`
and are yielded as a result of the region to be used in the rest of the module.
}];
let extraClassDeclaration = [{
/// Implement RegionKindInterface.
static RegionKind getRegionKind(unsigned index) {
return RegionKind::Graph;
}

let results = (outs Variadic<AnyType>:$results);
/// Retrieves the region block arguments
BlockArgument getRegionArg(unsigned index) {
return getBody().front().getArguments()[index];
}

let assemblyFormat = [{
`(` $inputs `)` attr-dict `:` functional-type($inputs, $results) $body
/// Retrieves the number of block arguments
unsigned getNumRegionArgs() {
return getBody().front().getNumArguments();
}
}];

let hasRegionVerifier = 1;
}

class RequireLikeOp<string mnemonic, list<Trait> traits = [
Expand Down
62 changes: 19 additions & 43 deletions lib/Dialect/Verif/VerifOps.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -104,50 +104,26 @@ LogicalResult ContractOp::verifyRegions() {
if (!parent)
return emitOpError() << "parent of contract must be an hw.module!";

auto nInputsInModule = parent.getNumInputPorts();
auto nOutputsInModule = parent.getNumOutputPorts();
auto nOps = (*this)->getNumOperands();

// Check that the region block arguments match the op's inputs
if (nInputsInModule != nOps)
return emitOpError() << "contract must have the same number of arguments "
<< "as the number of inputs in the parent module!";

// Check that the region block arguments match the op's inputs
if (getNumRegionArgs() != (nOps + nOutputsInModule))
return emitOpError() << "region must have the same number of arguments "
<< "as the number of arguments in the parent module!";

// Check that the region block arguments share the same types as the inputs
if (getBody().front().getArgumentTypes() != parent.getPortTypes())
auto nRes = (*this)->getNumResults();
auto resTypes = (*this)->getResultTypes();
auto *yield = getBody().front().getTerminator();

// Check that the region terminator yields the same number of ops as the
// number of results
if (yield->getNumOperands() != nRes)
return emitOpError() << "region terminator must yield the same number of "
<< "operands as there are results!";

// Check that the region terminator yields the same types of ops as the
// types of results
if (yield->getOperandTypes() != resTypes)
return emitOpError() << "region terminator must yield the same types of "
<< "operands as the result types!";

// Check that the region block arguments share the same types as the results
if (getBody().front().getArgumentTypes() != resTypes)
return emitOpError() << "region must have the same type of arguments "
<< "as the type of inputs!";

return success();
}

LogicalResult InstanceOp::verifyRegions() {
// Check that the region block arguments match the op's inputs
if (getNumRegionArgs() != (*this)->getNumOperands())
return emitOpError() << "region must have the same number of arguments "
<< "as the number of inputs!";

// Check that the region block arguments share the same types as the inputs
if (getBody().front().getArgumentTypes() != (*this)->getOperandTypes())
return emitOpError() << "region must have the same type of arguments "
<< "as the type of inputs!";

// Check that verif.yield yielded the expected number of operations
if ((*this)->getNumResults() !=
getBody().front().getTerminator()->getNumOperands())
return emitOpError() << "region terminator must yield the same number"
<< "of operations as there are results!";

// Check that the yielded types match the result types
if ((*this)->getResultTypes() !=
getBody().front().getTerminator()->getOperandTypes())
return emitOpError() << "region terminator must yield the same types"
<< "as the result types!";
<< "as the type of results!";

return success();
}
Expand Down
72 changes: 21 additions & 51 deletions test/Dialect/Verif/basic.mlir
View file
Original file line number Diff line number Diff line change
Expand Up @@ -58,70 +58,40 @@ verif.formal @formal1(k = 20) {

// CHECK-LABEL: hw.module @Bar
hw.module @Bar(in %foo : i8, out "" : i8, out "1" : i8) {
// CHECK: verif.contract(%foo) : (i8) {
verif.contract (%foo) : (i8) {
// CHECK: ^bb0(%[[ARG:.+]]: i8, %[[OUT:.+]]: i8, %[[OUT1:.+]]: i8):
^bb0(%arg1 : i8, %bar.0 : i8, %bar.1 : i8):
// CHECK: %[[C1:.+]] = hw.constant
%c1_8 = hw.constant 1 : i8
// CHECK: %[[O1:.+]] = comb.add
%to0 = comb.add bin %foo, %c1_8 : i8
// CHECK: %[[O2:.+]] = comb.sub
%to1 = comb.sub bin %foo, %c1_8 : i8

// CHECK: %[[OUT:.+]]:2 = verif.contract(%[[O1]], %[[O2]]) : (i8, i8) -> (i8, i8) {
%o0, %o1 = verif.contract (%to0, %to1) : (i8, i8) -> (i8, i8) {
// CHECK: ^bb0(%[[BAR0:.+]]: i8, %[[BAR1:.+]]: i8):
^bb0(%bar.0 : i8, %bar.1 : i8):
// CHECK: %[[C0:.+]] = hw.constant 0 : i8
%c0_8 = hw.constant 0 : i8
// CHECK: %[[PREC:.+]] = comb.icmp bin ugt %[[ARG]], %[[C0]] : i8
%prec = comb.icmp bin ugt %arg1, %c0_8 : i8
// CHECK: %[[PREC:.+]] = comb.icmp bin ugt %foo, %[[C0]] : i8
%prec = comb.icmp bin ugt %foo, %c0_8 : i8
// CHECK: verif.require %[[PREC]] : i1
verif.require %prec : i1

// CHECK: %[[P0:.+]] = comb.icmp bin ugt %[[OUT]], %[[ARG]] : i8
%post = comb.icmp bin ugt %bar.0, %arg1 : i8
// CHECK: %[[P1:.+]] = comb.icmp bin ult %[[OUT1]], %[[ARG]] : i8
%post1 = comb.icmp bin ult %bar.1, %arg1 : i8
// CHECK: %[[P0:.+]] = comb.icmp bin ugt %[[BAR0]], %foo : i8
%post = comb.icmp bin ugt %bar.0, %foo : i8
// CHECK: %[[P1:.+]] = comb.icmp bin ult %[[BAR1]], %foo : i8
%post1 = comb.icmp bin ult %bar.1, %foo : i8
// CHECK: verif.ensure %[[P0]] : i1
verif.ensure %post : i1
// CHECK: verif.ensure %[[P1]] : i1
verif.ensure %post1 : i1
}
// CHECK: %[[C1:.+]] = hw.constant
%c1_8 = hw.constant 1 : i8
// CHECK: %[[O1:.+]] = comb.add
%o0 = comb.add bin %foo, %c1_8 : i8
// CHECK: %[[O2:.+]] = comb.sub
%o1 = comb.sub bin %foo, %c1_8 : i8
// CHECK: verif.yield %[[BAR0]], %[[BAR1]] : i8, i8
verif.yield %bar.0, %bar.1 : i8, i8
}

// CHECK-LABEL: hw.output
hw.output %o0, %o1 : i8, i8
}

// CHECK-LABEL: hw.module @Foo1
hw.module @Foo1(in %0 "0": i1, in %1 "1": i1, out "" : i8, out "1" : i8) {
// CHECK: %[[C42:.+]] = hw.constant 42 : i8
%c42_8 = hw.constant 42 : i8
// CHECK: %[[OUTS:.+]]:2 = verif.instance(%[[C42]]) : (i8) -> (i8, i8) {
%bar.0, %bar.1 = verif.instance (%c42_8) : (i8) -> (i8, i8) {
// CHECK: ^bb0(%[[ARG:.+]]: i8):
^bb0(%arg1: i8):
// CHECK: %[[C0:.+]] = hw.constant 0 : i8
%c0_8 = hw.constant 0 : i8
// CHECK: %[[PREC:.+]] = comb.icmp bin ugt %[[ARG]], %[[C0]] : i8
%prec = comb.icmp bin ugt %arg1, %c0_8 : i8
// CHECK: verif.assert %[[PREC]] : i1
verif.assert %prec : i1

// CHECK: %[[OUT0:.+]] = verif.symbolic_input : i8
%bar.0 = verif.symbolic_input : i8
// CHECK: %[[OUT1:.+]] = verif.symbolic_input : i8
%bar.1 = verif.symbolic_input : i8
// CHECK: %[[P0:.+]] = comb.icmp bin ugt %[[OUT0]], %[[ARG]] : i8
%post = comb.icmp bin ugt %bar.0, %arg1 : i8
// CHECK: %[[P1:.+]] = comb.icmp bin ult %[[OUT1]], %[[ARG]] : i8
%post1 = comb.icmp bin ult %bar.1, %arg1 : i8
// CHECK: verif.assume %[[P0]] : i1
verif.assume %post : i1
// CHECK: verif.assume %[[P1]] : i1
verif.assume %post1 : i1
// CHECK: verif.yield %[[OUT0]], %[[OUT1]] : i8, i8
verif.yield %bar.0, %bar.1 : i8, i8
}
// CHECK: hw.output %[[OUTS]]#0, %[[OUTS]]#1 : i8, i8
hw.output %bar.0, %bar.1 : i8, i8
}

//===----------------------------------------------------------------------===//
// Print-related
// Must be inside hw.module to ensure that the dialect is loaded.
Expand Down

0 comments on commit bb6471f

Please sign in to comment.