[HW to BTOR2] btor2 conversion pass

[dobios]

TLDR

This PR introduces a btor emission pass that converts flattened (as in with inlined sub-modules) designs from the hw dialect into the btor2 format used for bounded model checking. This PR is a first prototype implementation, my goal is to have this feature merged into CIRCT and not necessarily this code, and I am willing to make any changes (no matter how major) to my implementation to make that happen.

Motivation

CIRCT is well developed in terms of enabling high-level hardware description but seems to be lacking in verification functionalities, particularly when it comes to formal verification. My goal here is to allow for the emission of btor2 , something that is supported by yosys and the scala-firrtl compiler, from the core dialects thus enabling formal verification for circt’s frontends through the use of bounded model checking.

For context, btor2 is a format that is widely used for bounded model checking. It is used as the basis for the hardware model checking competition https://fmv.jku.at/hwmcc20/. The format is supported by a well maintained open-source model checker called btormc, which is part of the OSS CAD suite (https://github.com/YosysHQ/oss-cad-suite-build), and is detailed in the following paper (https://link.springer.com/chapter/10.1007/978-3-319-96145-3_32).

To illustrate this, here is a concrete example of what using this format conversion could enable in one of circt’s front-ends;
I could for example write something like :

class Inc extends Module {
    val en = IO(Input(Bool()))
    val a = IO(Input(UInt(32.W)))
    val b = IO(Output(UInt(32.W)))

    when(en) {
        b := a + 1.U
    }

    assert(b > a, “a+1 should be greater than a”)
}

And have a magical tool that simply tells me “this assertion can fail, here’s an example: if a = 2^32 - 1 then b = 0 thus your assertion fails”, otherwise known as “sat 01...1 0”, without having to write the test cases out myself.

Current PR

In this PR I have added a “lowering” pass to the hw dialect which directly converts the design into a state transition system and emits that system as a btor2 string. In order for this to be done, the submodules must first all be inlined, so I expect something like the --arc-inline-modules pass to be scheduled before the btor2 emission pass. This emission currently supports most design concepts, except for memories and asynchronous resets, which are still a work in progress. Here’s an example of what you would obtain from running the btor2 emission pass on a simple counter circuit described in Chisel:

// Original Chisel Circuit
class Counter extends Module {
    val en = IO(Input(Bool()))
    val count = RegInit(0.U(32.W))
    when(en && count === 22.U) { count := 0.U }
    when(en && count =/= 22.U) { count := count + 1.U }
    assert(count =/= 10.U, “Counter reached 10!“)
}

Which would yield the following firrtl:

circuit Counter :
  module Counter :
    input clock : Clock
    input reset : UInt<1>
    input en : UInt<1>

    reg count : UInt<32>, clock with :
      reset => (reset, UInt<32>(“h0”))

    when and(eq(count, UInt<32>(22)), en) :
      count <= UInt<1>(“h0")

    when and(neq(count, UInt<32>(22)), en) :
      count <= tail(add(count, UInt<1>(“h1”)), 1)

    assert(clock, neq(count, UInt<4>(“ha”)), en, “Counter reached 10!“)

Which is then converted to the following hw:

hw.module @Counter(in %clock : !seq.clock, in %reset : i1, in %en : i1) {
    %0 = seq.from_clock %clock
    %c0_i28 = hw.constant 0 : i28
    %false = hw.constant false
    %c22_i32 = hw.constant 22 : i32
    %true = hw.constant true
    %c-6_i4 = hw.constant -6 : i4
    %c0_i32 = hw.constant 0 : i32
    %count = seq.firreg %9 clock %clock reset sync %reset, %c0_i32 {firrtl.random_init_start = 0 : ui64} : i32
    %1 = comb.icmp bin eq %count, %c22_i32 : i32
    %2 = comb.and bin %1, %en : i1
    %3 = comb.mux bin %2, %c0_i32, %count : i32
    %4 = comb.icmp bin ne %count, %c22_i32 : i32
    %5 = comb.and bin %4, %en : i1
    %6 = comb.concat %false, %count : i1, i32
    %c1_i33 = hw.constant 1 : i33
    %7 = comb.add bin %6, %c1_i33 : i33
    %8 = comb.extract %7 from 0 : (i33) -> i32
    %9 = comb.mux bin %5, %8, %3 : i32
    %c10_i32 = hw.constant 10 : i32
    %10 = comb.icmp bin ne %count, %c10_i32 : i32
    sv.always posedge %0 {
        sv.if %en {
                sv.assert %10, immediate message “Counter reached 10!”
        }
    }
    hw.output
}

Which is converted by the new btor emission pass (using circt-opt --hw-lower-to-btor2):

1 sort bitvec 1
2 input 1 reset
3 input 1 en
4 sort bitvec 28
5 constd 4 0
6 constd 1 0
7 sort bitvec 32
8 constd 7 22
9 constd 1 -1
10 sort bitvec 4
11 constd 10 -6
12 constd 7 0
13 state 7 count
14 eq 1 13 8
15 and 1 14 3
16 ite 7 15 12 13
17 neq 1 13 8
18 and 1 17 3
19 sort bitvec 33
20 concat 19 6 13
21 constd 19 1
22 add 19 20 21
23 slice 7 22 31 0
24 ite 7 18 23 16
25 constd 7 10
26 neq 1 13 25
27 implies 1 3 26
28 not 1 27
29 bad 28
30 zero 7
31 ite 7 2 30 24
32 next 7 13 31

Given this format, I can run it in btormc using the default bound of 20 cycles to get the following result (using btormc counter.btor2):

sat
b0
#10
0 00000000000000000000000000001010 count#10
@0
0 0 reset@0
1 1 en@0
.

Which tells me that, in the case where count=10, en=1, and reset=0, the assertion no longer holds.

I currently use firrtl as an example, but as this is a pass for circt’s core dialects, it should be available more generally for all of its front-ends.

Feedback

I would really appreciate any feedback that you might have on this PR. Given my lack of CIRCT development experience, this PR is more of a first prototype than something that I expect to immediately be up-streamed. My goal is to have this feature available in CIRCT and not necessarily this specific code, so I am willing to make any necessary changes in order for that to happen. On that note, would you have any suggestions on how this emission should be better structured, or how I could write this differently for it to fit in the overall circt code-base? Any comments are appreciated!
Thank you for your time and let me know what you think!

[mikeurbach]

@dobios there has been a lot of recent interest in bounded model checking. I'm proposing we talk about this at the CIRCT ODM on 11/29 at 11am PST (19:00 UTC). Would you and anyone from your group who is interested on this be able to join, or have a different day / time in mind that would work?

[dobios]

@dobios there has been a lot of recent interest in bounded model checking. I'm proposing we talk about this at the CIRCT ODM on 11/29 at 11am PST (19:00 UTC). Would you and anyone from your group who is interested on this be able to join, or have a different day / time in mind that would work?

Yes that works for me, I will definitely be there.

[fabianschuiki]

The structure of the code looks good to me. Nice comments and clean.

There are a few hidden assumptions w.r.t. how the LIDs are handed out and incremented. It would be great if those could be asserts to ensure there's no subtle breakage that's hard to track down.

My main concern is that the code assumes the HW module bodies to be in SSA form and follow dominance/def-before-use. This is not the case for HW modules. They are MLIR graph regions, which follow the single static assignment paradigm, but have no dominance constraint. As such, you will see a lot of operations that use operands before they are define. (If you're coming from Chisel/FIRRTL these are rare because of how they lower to HW. That's a FIRRTL limitation though. They will still produce uses before defs. Other frontends will produce those more aggressively.) Does btor2 have a concept of forward declarations that you can use if an operation has not been emitted yet? Or does it support cyclic graphs where you refer to LIDs after the current line? If yes, you might be able to just do a pre-pass over the module, assign LIDs to values up front, and then just refer to those values. Otherwise you'd have to do a depth-first traversal of the ops in the module with a worklist, to ensure that the btor2 you emit is in def-before-use order. That could also be an easy way to flatten instance hierarchies.

[dobios]

Thanks for the detailed review @fabianschuiki !

The structure of the code looks good to me. Nice comments and clean.

There are a few hidden assumptions w.r.t. how the LIDs are handed out and incremented. It would be great if those could be asserts to ensure there's no subtle breakage that's hard to track down.

BTOR2 LIDs are completely arbitrary. I chose to have them mirror line numbers because it was the most straightforward thing I could implement to have each line have an ordered unique id.

My main concern is that the code assumes the HW module bodies to be in SSA form and follow dominance/def-before-use. This is not the case for HW modules. They are MLIR graph regions, which follow the single static assignment paradigm, but have no dominance constraint. As such, you will see a lot of operations that use operands before they are define. (If you're coming from Chisel/FIRRTL these are rare because of how they lower to HW. That's a FIRRTL limitation though. They will still produce uses before defs. Other frontends will produce those more aggressively.)

Could you provide an example of a front-end that often generates operations in a non def-berfore-use manner so that I might run some tests on my implementation?

Does btor2 have a concept of forward declarations that you can use if an operation has not been emitted yet? Or does it support cyclic graphs where you refer to LIDs after the current line? If yes, you might be able to just do a pre-pass over the module, assign LIDs to values up front, and then just refer to those values. Otherwise you'd have to do a depth-first traversal of the ops in the module with a worklist, to ensure that the btor2 you emit is in def-before-use order. That could also be an easy way to flatten instance hierarchies.

I see, this is definitely an assumption that I made when implementing this. Given that btor2 requires some ordering of lids unfortunately, I might have to opt for the work-list solution. I will just have to restructure my code quite a bit.

[fabianschuiki]

If you're free to pick LIDs, and they just have to be defined before they are used, I'd just make getOrCreateOpLID increment the lid counter and allocate IDs. The few skipped IDs or IDs slightly out of order sound like a worthwhile trade-off for the simplified implementation of the pass and handling of the IDs.

[fabianschuiki]

You can hand-write FIRRTL inputs to create use-before-def situations at the HW dialect. Specifically, the lowering from FIRRTL to HW will often try to look through wires and connects in order to more directly materialize values. For example:

FIRRTL version 3.0.0

circuit Foo:
    module Foo:
        input clk: Clock
        input a: UInt<42>
        input b: UInt<42>

        ; Creates an instance at the top.
        inst bar of Bar

        ; Creates a register after the instance, and hooks the instance's input
        ; up to the register. This becomes a forward use in HW.
        reg tmp0: UInt<42>, clk
        connect bar.x, tmp0

        ; Creates a wire after the register, and hooks the register's input up
        ; to the wire. This becomes another forward use in HW.
        wire tmp1: UInt<42>
        connect tmp0, tmp1

        ; Assign an expression to the wire. This will create a comb.xor op after
        ; the wire. The wire is inlined and the register directly uses the
        ; result of this op.
        connect tmp1, xor(a,b)

    extmodule Bar:
        input x: UInt<42>

If you run the above through firtool --ir-hw, you'll get something like the following:

hw.module @Foo(in %clk : !seq.clock, in %a : i42, in %b : i42) {
  hw.instance "bar" @Bar(x: %tmp0: i42) -> ()
  %tmp0 = seq.firreg %0 clock %clk {firrtl.random_init_start = 0 : ui64} : i42
  %0 = comb.xor bin %a, %b {sv.namehint = "tmp1"} : i42
  hw.output
}
hw.module.extern private @Bar(in %x : i42)

It has all the operations in reverse order. Since HW modules have graph regions, you can actually go in and reshuffle the lines pretty freely yourself. I think you already use Chisel to get a few HW results going; you should be able to open that HW MLIR file in your favorite text editor and ask it to shuffle the lines in an HW module. Should still work after that, but give you use-befor-def headaches 😏

[fabianschuiki]

For a worklist-driven approach, you could use something like the following:

SmallMapVector<Operation *, OperandRange::iterator, 16> worklist;
DenseSet<Operation *> handledOps;

module.walk([&](Operation *op) {
  if (handledOps.contains(op))
    return;
  worklist.insert({op, op->operand_begin()});

  while (!worklist.empty()) {
    auto &[op, operandIt] = worklist.back();
    if (operandIt == op->operand_end()) {
      // In here you are guaranteed to have processed all operands of `op`.
      // This should be where you can do a `dispatchTypeOpVisitor(...)` call.
      handledOps.insert(op);
      worklist.pop_back();
      continue;
    }
    Value operand = *(operandIt++);
    auto *defOp = operand.getDefiningOp();
    if (!defOp || handledOps.contains(defOp))
      continue;
    if (!worklist.insert({defOp, defOp->operand_begin()}).second) {
      // You get here if there's a dependency cycle (op already in the worklist).

      // Registers will likely depend on their own value to compute the next
      // value, e.g. to increment a counter or pick between holding the current
      // value or changing to a new one through a mux.
      //
      // However, for registers you have separate `state` and `next`
      // declarations in btor2. So one thing you could do is create the `state`
      // whenever you push a register onto the worklist (that is, before you
      // visit its operands), so you always have a LID to reference. And then
      // once you have visited all reg operands (above where you dispatch the
      // visitor), you can actually emit the `next` statement since you now have
      // both the LID for the reg and the LID for the next value available.
      //
      // If you do that, you could just simply ignore the cyclic dependency if
      // `defOp` is a register.

      // Instances will do a similar thing, since they consume all inputs as
      // operands and produce all outputs as results. So even if there's
      // technically no combinational loop, the IR ops will still have a loopy
      // dependency.
      return op->emitError("dependency cycle");
    }
  }
});

The worklist should allow you to later rework this to support instances as well. Instead of just storing the Operation * in the worklist, you could store a (Operation *, SomeInstancePath) pair. Whenever you hit an hw.instance op, you can go and push the operations inside the instantiated module onto the worklist, with the appropriate instance path. (There are likely more annoying details to figure out here, like finding all asserts and result-less ops in the instantiated module and ensuring that those get visited as well. But all that sounds like a future-me / future-you problem 😬.)

It would be good to throw an error if you encounter an instance, instead of silently failing. In the worklist, something like:

if (isa<hw::InstanceOp>(op))
  return op->emitOpError("not supported in BTOR2 conversion");

[darthscsi]

Thanks!

[darthscsi]

this can be folded into later code. A single lookup should be sufficient for all code paths.

[darthscsi]

Some of these seem like they will affect the correctness of the output if you don't handle them. If that is the case, the pass should fail gracefully with an error message.

[dobios]

I don't see which ones would affect correctness apart from IfDefOp which I only expect wrapping an sv.assert in which case I check for them in a bottom-up style (as they get directly integrated into the assertion in btor2 so it doesn't make sense to generate anything for them beforehand).

[fabianschuiki]

What happens if you have for example a seq::FromClockOp in the input? Or an sv::AlwaysFFOp? Is the pass going to do the right thing and everything works when the op is ignored, or is it going to fail? (Like not including the logic in the alwaysff, or not tracking the clock through the FromClockOp?) If it fails in any way, or ignores part of the input, this should probably throw an error. Silent failures are very hard to track and fix later.

For example, if you don't support multiple clocks right now, or weird stuff like clock gates and clock muxes, I'd throw errors if any of those ops are detected, or if the module has more than one port that is of !seq.clock type. It's very valuable in practice to be explicit about which inputs are supported and which ones aren't. That's usually also a good hook to get people excited to contribute 🙂 If there's a clear error message that something is unsupported, you'll get people search for the place where the error is emitted, and starting to get baited into helping you develop stuff 😏

[fabianschuiki]

Btw, since your pass is caleld HWToBTOR2, it would be totally fine to just error out on any SV op that you see in the input. Or only support a few of them. But I also get that the current FIRRTL-to-HW lowering is annoying because it produces SV bits here and there, which isn't really ideal for reasoning about it. If you need to work around that, for example by saying that no SV macros are defined and all IfDefOps always go to the false branch, you could emit warnings about the cases where you had to make such assumptions to get your pass to work initially. Those are then also obvious things that we'll have to improve on the FIRRTL-to-HW side.

Arcilator and the Arc dialect had a similar issue, where it had to look through the SV cruft that FIRRTL-to-HW emits to get something going. It silently ignores some of that stuff, which comes back to bite us over and over again now 😛 Better to be explicit and verbose about it.

[dobios]

Well I noticed that a ton of SV macros were often generated and used in a way that didn't impact the output model. So in order to not reject half of what firrtool gave me I opted for ignoring those specific ops.

[fabianschuiki]

Yeah that makes sense. This is probably also something we can figure out iteratively as time progresses -- and the Arc dialect also still needs to figure some of this out. It's good to have multiple use cases where the SV stuff is a challenge

[dobios]

I updated the implementation so that it supports the def-after-use case that @fabianschuiki pointed out. I also took into account most of the comments. Let me know if there's anything else !

[fabianschuiki]

Love the worklist approach and that you are doing a pre-pass to declare all the registers! Just a few remaining comments on some of the defensiveness of the code, and possible silent failures that should probably be very load blow-ups 🙂

[fabianschuiki]

What happens if you have for example a seq::FromClockOp in the input? Or an sv::AlwaysFFOp? Is the pass going to do the right thing and everything works when the op is ignored, or is it going to fail? (Like not including the logic in the alwaysff, or not tracking the clock through the FromClockOp?) If it fails in any way, or ignores part of the input, this should probably throw an error. Silent failures are very hard to track and fix later.

For example, if you don't support multiple clocks right now, or weird stuff like clock gates and clock muxes, I'd throw errors if any of those ops are detected, or if the module has more than one port that is of !seq.clock type. It's very valuable in practice to be explicit about which inputs are supported and which ones aren't. That's usually also a good hook to get people excited to contribute 🙂 If there's a clear error message that something is unsupported, you'll get people search for the place where the error is emitted, and starting to get baited into helping you develop stuff 😏

[fabianschuiki]

Btw, since your pass is caleld HWToBTOR2, it would be totally fine to just error out on any SV op that you see in the input. Or only support a few of them. But I also get that the current FIRRTL-to-HW lowering is annoying because it produces SV bits here and there, which isn't really ideal for reasoning about it. If you need to work around that, for example by saying that no SV macros are defined and all IfDefOps always go to the false branch, you could emit warnings about the cases where you had to make such assumptions to get your pass to work initially. Those are then also obvious things that we'll have to improve on the FIRRTL-to-HW side.

Arcilator and the Arc dialect had a similar issue, where it had to look through the SV cruft that FIRRTL-to-HW emits to get something going. It silently ignores some of that stuff, which comes back to bite us over and over again now 😛 Better to be explicit and verbose about it.

[dobios]

I added an explicit check and fail for multiple clocks and also removed certain silent-fails that didn't make as much sense. I also added a test that is completely out of order for the DFS traversal. Let me know what you think @fabianschuiki !

[fabianschuiki]

Thanks a lot for all the reworking and tweaking! This looks like a great starting point for BTOR2 emission and future tweaks and expansion as we build out more of the verification flow 🥳. LGTM