Verif Dialect

This dialect provides a collection of operations to express various verification concerns, such as assertions and interacting with a piece of hardware for the sake of verifying its proper functioning.

[TOC]

Contracts

Formal contracts are a key building block of the Verif dialect to help make formal verification scale to larger designs and deep module hierarchies. Contracts describe what a circuit expects from its inputs (verif.require) and what it guarantees its output to be (verif.ensure). The verif.contract op can be inserted into an SSA edge similar to an hw.wire, where the contract simply passes its operands through to its results. During formal verification the contract results are replaced by symbolic values that uphold the guarantees described in the contract's body. Conceptually, contracts are similar to Hoare triples used in software verification, where a piece of code is verified to produce a given set of postconditions when the given set of preconditions is met.

These contracts can then be used in two key ways:

A contract can be checked by turning requires into assumes and ensures into asserts. Doing so verifies that a circuit upholds the contract by placing asserts on the values it produces, and by placing assumes on the input values the circuit sees. In a nutshell, this checks that, assuming the inputs to the circuit honor the contract, the output from the circuit also upholds the contract. This check can be done very efficiently by creating verif.formal ops to verify each contract.
A contract can be applied by turning requires into asserts and ensures into assumes. Doing so verifies that the inputs fed into a circuit uphold the contract, such that the outputs can be assumed to have the promised values. In a nutshell, this checks that the inputs to a circuit honor the contract and therefore the circuit can be assumed to uphold the contract. Assuming a contract can often eliminate large parts of the circuit's actual implementation, since the contracts tend to be a simpler description of a circuit's functionality.

Multiply-by-9 Example

Consider the following example of a HW module that computes 9 * a using a left-shift and an addition. Note that this is using verif.ensure_equal as a standin for verif.ensure(comb.icmp eq). The module's output %z is the result of a verif.contract operation. Contracts can be completely ignored by simply passing through their operands, %1 in this case, to their results. This is their normal interpretation outside a formal verification flow, for example for synthesis.

hw.module @Mul9(in %a: i42, out z: i42) {
  // Compute 9*a as (a<<3)+a.
  %c3_i42 = hw.constant 3 : i42
  %0 = comb.shl %a, %c3_i42 : i42
  %1 = comb.add %a, %0 : i42

  // Contract to check that the circuit actually produces 9*a.
  %z = verif.contract %1 : i42 {
    %c9_i42 = hw.constant 9 : i42
    %a9 = comb.mul %a, %c9_i42 : i42
    verif.ensure_equal %z, %a9
  }

  hw.output %z : i42
}

To check that the contract holds, it can be pulled out into a verif.formal op along with all ops in its fan-in cone. The contract's results are then replaced with its operands, the body is inlined, and ensure ops are replaced with assert and require ops are replaced with assume. Running this formal test will check that the (a<<3)+a implemented by the module is indeed the same as the 9*a promised by the contract.

verif.formal @Mul9_CheckContract {
  %a = verif.symbolic_value : i42

  %c3_i42 = hw.constant 3 : i42
  %0 = comb.shl %a, %c3_i42 : i42
  %1 = comb.add %a, %0 : i42

  // Contract inlined with ensure -> assert, %z -> %1
  %c9_i42 = hw.constant 9 : i42
  %a9 = comb.mul %a, %c9_i42 : i42
  verif.assert_equal %1, %a9 : i42
}

Once the contract is checked, it can be assumed to hold everywhere. Assuming it holds can be done by inlining it into its parent block and replacing its results with symbolic values. At the same time, ensures are replaced with assumes and requires with asserts. Inlining the contract in this example and replacing the symbolic value with what it is assumed to be equal to will make the module produce the simple 9*a term. This means that the ops describing the original implementation become obsolete and will be DCEd. Making bits of a module's implementation unused is the key characteristic of contracts that makes them help formal verification scale. If all of a module's behavior can be described by one or more simpler contracts, its entire original implementation would simply disappear in favor of the simpler contracts.

hw.module @Mul9_ApplyContract(in %a: i42, out z: i42) {
  // The original implementation has become unused since the contract results
  // have been replaced with symbolic values. Dead code elimination will clean
  // this up.
  %c3_i42 = hw.constant 3 : i42
  %0 = comb.shl %a, %c3_i42 : i42
  %1 = comb.add %a, %0 : i42

  // Results of the contract are replaced with symbolic values.
  // Contract inlined with ensure -> assume, %z -> %any
  // assume(eq(any, x)) can be canonicalized to an any -> x replacement.
  %any = verif.symbolic_value : i42
  %c9_i42 = hw.constant 9 : i42
  %a9 = comb.mul %a, %c9_i42 : i42
  verif.assume_equal %any, %a9 : i42

  hw.output %any : i42
}

// ----- after canonicalization, CSE, and DCE ----- //

hw.module @Mul9_ApplyContract_Simplified(in %a: i42, out z: i42) {
  %c9_i42 = hw.constant 9 : i42
  %a9 = comb.mul %a, %c9_i42 : i42
  hw.output %a9 : i42
}

These two constructs can coexist in the IR. A contract can be turned into a verif.formal proof that it holds, and inlined everywhere else to leverage the fact that the contract holds.

Carry-Save Compressor Example

Consider the following slightly more involved example of a compression stage you would find in a carry-save adder. This module takes 3 input values and produces 2 output values that sum up to the same value as its inputs. However, the contract in the module does not specify which exact output values the module produces. Instead, it uses two symbolic values to express that the module can produce any output values that sum up to the inputs. In a sense, how exactly the compressor combines 3 values into 2 is left as an implementation detail that you can’t know about, but the guarantee you can work with is that the sum will be correct. This is different from the previous example, where the contract produced an exact replacement value for the module output. Also, note how this uses an assume to constrain the sum of the symbolic values instead of an ensure or require.

// A module that takes 3 input values and produces 2 output values that sum up
// to the same value as the inputs. Instead of just using add it uses a
// bit-parallel full adder that takes each 3-tuple of bits in the 3 inputs, runs
// them through a full adder, and treats the resulting sum and carry as the 2
// corresponding bits for its 2 output values.
hw.module @CarrySaveCompress3to2(
  in %a0: i42, in %a1: i42, in %a2: i42,
  out z0: i42, out z1: i42
) {
  %c1_i42 = hw.constant 1 : i42
  %0 = comb.xor %a0, %a1, %a2 : i42  // sum bits of FA (a0^a1^a2)
  %1 = comb.and %a0, %a1 : i42
  %2 = comb.or %a0, %a1 : i42
  %3 = comb.and %2, %a2 : i42
  %4 = comb.or %1, %3 : i42          // carry bits of FA (a0&a1 | a2&(a0|a1))
  %5 = comb.shl %4, %c1_i42 : i42    // %5 = carry << 1
  // At this point, %0+%5 is the same as %a0+%a1+%a2, but without creating a
  // long ripple-carry chain.

  // Contract to check that we output _some_ two numbers that sum up to the same
  // value as the sum of the three inputs. We don't say which exact numbers.
  %z0, %z1 = verif.contract %0, %5 {
    // The contract promises that its outputs will sum up to the same value as
    // the sum of the module inputs.
    %inputSum = comb.add %a0, %a1, %a2 : i42
    %outputSum = comb.add %z0, %z1 : i42
    verif.ensure_equal %inputSum, %outputSum : i42
  }

  hw.output %z0, %z1 : i42, i42
}

The contract can be checked by extracting it into a new verif.formal op alongside its entire fan-in cone. Again we pretend that the contract doesn't exist by passing its operands %0 and %5, the actual implementation, through to its results %z0 and %z1. Replacing ensures with asserts then verifies that the module's outputs do indeed sum up to the same value as the inputs.

verif.formal @CarrySaveCompress3to2_CheckContract {
  %a0 = verif.symbolic_value : i42
  %a1 = verif.symbolic_value : i42
  %a2 = verif.symbolic_value : i42

  %c1_i42 = hw.constant 1 : i42
  %0 = comb.xor %a0, %a1, %a2 : i42
  %1 = comb.and %a0, %a1 : i42
  %2 = comb.or %a0, %a1 : i42
  %3 = comb.and %2, %a2 : i42
  %4 = comb.or %1, %3 : i42
  %5 = comb.shl %4, %c1_i42 : i42

  // Contract inlined with ensure -> assert, (%z0, %z1) -> (%0, %5).
  %inputSum = comb.add %a0, %a1, %a2 : i42
  %outputSum = comb.add %0, %5 : i42
  verif.assert_equal %inputSum, %outputSum : i42
}

With the contract checked it can be assumed to hold by inlining it everywhere and replacing its results %z0 and %z1 with symbolic values. This provides the symbolic values as a replacement for the actual implementation of the module, which causes the entire original implementation to be DCEd.

hw.module @CarrySaveCompress3to2_ApplyContract(
  in %a0: i42, in %a1: i42, in %a2: i42,
  out z0: i42, out z1: i42
) {
  // The original implementation has become unused since the contract results
  // have been replaced with symbolic values. Dead code elimination will clean
  // this up.
  %c1_i42 = hw.constant 1 : i42
  %0 = comb.xor %a0, %a1, %a2 : i42
  %1 = comb.and %a0, %a1 : i42
  %2 = comb.or %a0, %a1 : i42
  %3 = comb.and %2, %a2 : i42
  %4 = comb.or %1, %3 : i42
  %5 = comb.shl %4, %c1_i42 : i42

  // Results of the contract are replaced with symbolic values.
  // Contract inlined with ensure -> assume, (%z0, %z1) -> (%any0, %any1).
  %any0 = verif.symbolic_value : i42
  %any1 = verif.symbolic_value : i42
  %inputSum = comb.add %a0, %a1, %a2 : i42
  %outputSum = comb.add %any0, %any1 : i42
  verif.assume_equal %inputSum, %outputSum : i42

  hw.output %any0, %any1 : i42, i42
}

// ----- after canonicalization, CSE, and DCE ----- //

hw.module @CarrySaveCompress3to2_ApplyContract_Simplified(
  in %a0: i42, in %a1: i42, in %a2: i42,
  out z0: i42, out z1: i42
) {
  %any0 = verif.symbolic_value : i42
  %any1 = verif.symbolic_value : i42
  %inputSum = comb.add %a0, %a1, %a2 : i42
  %outputSum = comb.add %any0, %any1 : i42
  verif.assume_equal %inputSum, %outputSum : i42
  hw.output %any0, %any1 : i42, i42
}

Carry-Save Adder Example

Consider the following carry-save adder built based on the compressor from the previous example. It takes 5 input values and sums them up. To do so, it uses multiple instances of the compressor to compress three of the input terms down to two iteratively, until only two terms are left. The remaining two terms are then summed up with a plain old adder to get the final result. This carry-save adder module has its own little contract which promises that the output is going to be the sum of all input terms.

// A module that takes 5 input values and sums them up using a carry save adder.
hw.module @CarrySaveAdder5(
  in %a0: i42, in %a1: i42, in %a2: i42, in %a3: i42, in %a4: i42,
  out z: i42
) {
  // Each stage takes 3 of the terms and compresses them to 2.
  // terms: [a0, a1, a2, a3, a4]
  %b0, %b1 = hw.instance "comp0" @CarrySaveCompress3to2(a0: %a0: i42, a1: %a1: i42, a2: %a2: i42) -> (z0: i42, z1: i42)
  // terms: [b0, b1, a3, a4]
  %c0, %c1 = hw.instance "comp1" @CarrySaveCompress3to2(a0: %b1: i42, a1: %a3: i42, a2: %a4: i42) -> (z0: i42, z1: i42)
  // terms: [b0, c0, c1]
  %d0, %d1 = hw.instance "comp2" @CarrySaveCompress3to2(a0: %b0: i42, a1: %c0: i42, a2: %c1: i42) -> (z0: i42, z1: i42)
  // terms: [d0, d1]
  %e = comb.add %d0, %d1 : i42
  // terms: [e]

  // Contract to check that the output is the sum of all inputs.
  %z = verif.contract %e {
    %inputSum = comb.add %a0, %a1, %a2, %a3, %a4, %a5 : i42
    verif.ensure_equal %z, %inputSum : i42
  }

  hw.output %z : i42
}

Checking the contract looks as follows. Note how the formal proof can already assume that contracts inside the compressor submodule hold. This is a neat example of recursive use of contracts, and how checking contracts in parent modules can benefit from contracts in child modules. Instead of having to include the compressor module implementation in this test again, potentially complicating the proof, we can already use the simplified version described by the compressor's contract. This turns the compressor instances basically into a few additions among symbolic values, which formal solvers are very good at working with.

verif.formal @CarrySaveAdder5_CheckContract {
  %a0 = verif.symbolic_value : i42
  %a1 = verif.symbolic_value : i42
  %a2 = verif.symbolic_value : i42
  %a3 = verif.symbolic_value : i42
  %a4 = verif.symbolic_value : i42

  // The following instances are just two symbolic values each, constrained to
  // sum up to the instance inputs. This makes for a more trivial solve.
  %b0, %b1 = hw.instance "comp0" @CarrySaveCompress3to2_ApplyContract(a0: %a0: i42, a1: %a1: i42, a2: %a2: i42) -> (z0: i42, z1: i42)
  %c0, %c1 = hw.instance "comp1" @CarrySaveCompress3to2_ApplyContract(a0: %b1: i42, a1: %a3: i42, a2: %a4: i42) -> (z0: i42, z1: i42)
  %d0, %d1 = hw.instance "comp2" @CarrySaveCompress3to2_ApplyContract(a0: %b0: i42, a1: %c0: i42, a2: %c1: i42) -> (z0: i42, z1: i42)
  %e = comb.add %d0, %d1 : i42

  // Contract inlined with ensure -> assert, %z -> %e.
  %inputSum = comb.add %a0, %a1, %a2, %a3, %a4, %a5 : i42
  verif.assert_equal %e, %inputSum : i42
}

The contract can then be assumed to hold by inlining it into the carry-save adder as follows.

hw.module @CarrySaveAdder5_ApplyContract(
  in %a0: i42, in %a1: i42, in %a2: i42, in %a3: i42, in %a4: i42,
  out z: i42
) {
  // The original implementation has become unused since the contract results
  // have been replaced with symbolic values. Dead code elimination will clean
  // this up.
  %b0, %b1 = hw.instance "comp0" @CarrySaveCompress3to2_ApplyContract(a0: %a0: i42, a1: %a1: i42, a2: %a2: i42) -> (z0: i42, z1: i42)
  %c0, %c1 = hw.instance "comp1" @CarrySaveCompress3to2_ApplyContract(a0: %b1: i42, a1: %a3: i42, a2: %a4: i42) -> (z0: i42, z1: i42)
  %d0, %d1 = hw.instance "comp2" @CarrySaveCompress3to2_ApplyContract(a0: %b0: i42, a1: %c0: i42, a2: %c1: i42) -> (z0: i42, z1: i42)
  %e = comb.add %d0, %d1 : i42

  // Results of the contract are replaced with symbolic values.
  // Contract inlined with ensure -> assume, %z -> %any.
  %any = verif.symbolic_value : i42
  %inputSum = comb.add %a0, %a1, %a2, %a3, %a4, %a5 : i42
  // assume(eq(any, x)) can be canonicalized to an any -> x replacement.
  verif.assume_equal %any, %inputSum : i42

  hw.output %any : i42
}

// ----- after canonicalization, CSE, and DCE ----- //

hw.module @CarrySaveAdder5_ApplyContract_Simplified(
  in %a0: i42, in %a1: i42, in %a2: i42, in %a3: i42, in %a4: i42,
  out z: i42
) {
  %inputSum = comb.add %a0, %a1, %a2, %a3, %a4, %a5 : i42
  hw.output %inputSum : i42
}

Multiplexer-based Shifter

Consider the following module that left-shifts a value. It uses a multiplexer tree to perform the shift, which cannot shift out the value completely. Therefore, a require is placed in its contract to force the users of the shifter to never provide shift amounts outside the valid range.

hw.module @ShiftLeft(in %a: i8, in %b: i8, out z: i8) {
  %c4_i8 = hw.constant 4 : i8
  %c2_i8 = hw.constant 2 : i8
  %c1_i8 = hw.constant 1 : i8
  %b2 = comb.extract %b, 2 : i8 -> i1
  %b1 = comb.extract %b, 1 : i8 -> i1
  %b0 = comb.extract %b, 0 : i8 -> i1
  %0 = comb.shl %a, %c4_i8 : i8
  %1 = comb.mux %b2, %0, %a : i8
  %2 = comb.shl %1, %c2_i8 : i8
  %3 = comb.mux %b1, %2, %1 : i8
  %4 = comb.shl %3, %c1_i8 : i8
  %5 = comb.mux %b0, %4, %3 : i8

  // Contract to check that the multiplexers and constant shifts above indeed
  // produce the correct shift by 0 to 7 places, assuming the shift amount is
  // less than 8 (we can't shift a number out).
  %z = verif.contract %5 {
    // Shift amount must be less than 8.
    %c8_i8 = hw.constant 8 : i8
    %blt8 = comb.icmp ult %b, %c8_i8 : i8
    verif.require %blt8

    // In that case the mux tree computes the correct left-shift.
    %ashl = comb.shl %a, %b : i8
    verif.ensure_equal %z, %ashl : i42
  }

  hw.output %z : i8
}

The contract in the shifter can be checked as follows. Note how the require is replaced by an assume in addition to the ensure being replaced by an assert.

verif.formal @ShiftLeft_CheckContract {
  %a = verif.symbolic_value : i8
  %b = verif.symbolic_value : i8

  %c4_i8 = hw.constant 4 : i8
  %c2_i8 = hw.constant 2 : i8
  %c1_i8 = hw.constant 1 : i8
  %b2 = comb.extract %b, 2 : i8 -> i1
  %b1 = comb.extract %b, 1 : i8 -> i1
  %b0 = comb.extract %b, 0 : i8 -> i1
  %0 = comb.shl %a, %c4_i8 : i8
  %1 = comb.mux %b2, %0, %a : i8
  %2 = comb.shl %1, %c2_i8 : i8
  %3 = comb.mux %b1, %2, %1 : i8
  %4 = comb.shl %3, %c1_i8 : i8
  %5 = comb.mux %b0, %4, %3 : i8

  // Contract inlined with ensure -> assert, require -> assume, %z -> %5.
  %c8_i8 = hw.constant 8 : i8
  %blt8 = comb.icmp ult %b, %c8_i8 : i8
  verif.assume %blt8
  %ashl = comb.shl %a, %b : i8
  verif.assert_equal %5, %ashl : i42
}

Once checked, the contract can be assumed to hold by inlining it into the shift-left module as follows. Note how the value of input b is now asserted to be less than 8. This causes the instantiation sites of this module to be checked to provide values for b that are less than 8, thus upholding the contract. At the same time, it allows those sites to use the simplified comb.shl %a, %b implementation described in the contract.

hw.module @ShiftLeft_ApplyContract(in %a: i8, in %b: i8, out z: i8) {
  // The original implementation has become unused since the contract results
  // have been replaced with symbolic values. Dead code elimination will clean
  // this up.
  %c4_i8 = hw.constant 4 : i8
  %c2_i8 = hw.constant 2 : i8
  %c1_i8 = hw.constant 1 : i8
  %b2 = comb.extract %b, 2 : i8 -> i1
  %b1 = comb.extract %b, 1 : i8 -> i1
  %b0 = comb.extract %b, 0 : i8 -> i1
  %0 = comb.shl %a, %c4_i8 : i8
  %1 = comb.mux %b2, %0, %a : i8
  %2 = comb.shl %1, %c2_i8 : i8
  %3 = comb.mux %b1, %2, %1 : i8
  %4 = comb.shl %3, %c1_i8 : i8
  %5 = comb.mux %b0, %4, %3 : i8

  // Results of the contract are replaced with symbolic values.
  // Contract inlined with ensure -> assume, require -> assert, %z -> %any
  // assume(eq(any, x)) can be canonicalized to an any -> x replacement.
  %any = verif.symbolic_value : i8
  %c8_i8 = hw.constant 8 : i8
  %blt8 = comb.icmp ult %b, %c8_i8 : i8
  verif.assert %blt8
  %ashl = comb.shl %a, %b : i8
  verif.assume_equal %any, %ashl : i42

  hw.output %any : i8
}

// ----- after canonicalization, CSE, and DCE ----- //

hw.module @ShiftLeft_ApplyContract_Simplified(in %a: i8, in %b: i8, out z: i8) {
  %c8_i8 = hw.constant 8 : i8
  %blt8 = comb.icmp ult %b, %c8_i8 : i8
  verif.assert %blt8
  %ashl = comb.shl %a, %b : i8
  hw.output %ashl : i8
}

Operations

[include "Dialects/VerifOps.md"]

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Verif Dialect

Contracts

Multiply-by-9 Example

Carry-Save Compressor Example

Carry-Save Adder Example

Multiplexer-based Shifter

Operations

FilesExpand file tree

Verif.md

Latest commit

History

Verif.md

File metadata and controls

Verif Dialect

Contracts

Multiply-by-9 Example

Carry-Save Compressor Example

Carry-Save Adder Example

Multiplexer-based Shifter

Operations