[Arc] Add basic assertion support

[fabianschuiki]

Add support for verif.assert and sv.assert.concurrent operations to the Arc dialect and passes. When lowering towards LLVM, the asserts should lower to an scf.if operation that checks whether their condition holds, and if it does not, calls a callback function (or aborts with a message for starters).

This is likely to uncover a lot of details about how clocked and unclocked asserts need to be handled, and where they have to be scheduled and checked in the simulation model.

[elhewaty]

Please assign me.

[elhewaty]

I will share what I have noticed till now:

Add support for verif.assert and sv.assert.concurrent operations to the Arc dialect and passes.

for this part, I am thinking of adding struct VerifAssertionConversion: public OpConversionPattern<AssertOp> to ConvertToArc, and overriding the match function.
can you give more hints?

[fabianschuiki]

That sounds like a great idea! Take a look at the https://github.com/llvm/circt/blob/main/lib/Dialect/Arc/Transforms/LowerArcsToFuncs.cpp file to see how you can setup a bunch of conversion patterns and then run them on the IR. You probably want to run your conversion patterns as the very first thing in the ConvertToArcsPass, before the arc converter itself is run.

[elhewaty]

That sounds like a great idea! Take a look at the https://github.com/llvm/circt/blob/main/lib/Dialect/Arc/Transforms/LowerArcsToFuncs.cpp file to see how you can setup a bunch of conversion patterns and then run them on the IR.

What is the difference between patterns in this file and ones in ArcToLLVM.cpp ?

You probably want to run your conversion patterns as the very first thing in the ConvertToArcsPass, before the arc converter itself is run.

Yes, that is what I thought of. BTW, we discussed this issue on circt channel.
We have now to approaches:

• Add arc.assert op and then convert assertions from other dialects to it
• Not to add the op because there's no reason to do so, and convert the assertions at the end of the pipeline into LLVM IR (@Moxinilian's idea)

The reason for the second idea is that Arc should only model the arcs.

Please share your thoughts.

[Moxinilian]

I like the idea of that Moxinilian guy. I think you can do all this by just adding one pattern in the Arc to LLVM conversion. The assertion will end up at the end of the eval function, which seems like a good place to have it.

[fabianschuiki]

The tricky thing is that assertions interact with a clock: verif.assert is very likely to have an operand defined by ltl.clock, which limits the checking of the condition to a clock edge, and sv.assert.concurrent has an explicit clock operand. Arcilator needs to reason about these at some point in its pipeline. Similar to how we have registers or arc.state ops with a clock, at some point these get absorbed into a clock function and the clock operand gets dropped from the arc.state op. A similar thing has to happen with clocked asserts: Arcilator needs to move them into a region that is only executed on the correpsonding clock edge, and drop the clock on the assertion. Then the simple lowering in ArcToLLVM can take over.

[maerhart]

I'm wondering if it makes sense to restrict this first task to only verif.assert with i1 operands? It'll probably be easier for @elhewaty to implement and provide a smoother onboarding experience. The task would almost only affect the lowering from Verif to LLVM.

In a follow-up step, we could look at lowering the LTL dialect to an automaton. If I understand correctly, the assert should then trigger when a certain state in the automaton is reached, which can be indicated by an i1 value that can be fed to a verif.assert for which we then already have a lowering to LLVM. Just introducing an arc.assert with a clock operand (like arc.state) doesn't seem to be sufficient to support full LTL, right? Or what would you lower the verif.assert to in ConvertToArcs?

@fabianschuiki I'm not quite sure why sv.assert.concurrent has to be supported separately and cannot be expressed as a verif.assert. Could you provide a bit more context on that?

[Moxinilian]

The tricky thing is that assertions interact with a clock: verif.assert is very likely to have an operand defined by ltl.clock, which limits the checking of the condition to a clock edge, and sv.assert.concurrent has an explicit clock operand. Arcilator needs to reason about these at some point in its pipeline. Similar to how we have registers or arc.state ops with a clock, at some point these get absorbed into a clock function and the clock operand gets dropped from the arc.state op. A similar thing has to happen with clocked asserts: Arcilator needs to move them into a region that is only executed on the correpsonding clock edge, and drop the clock on the assertion. Then the simple lowering in ArcToLLVM can take over.

Could you detail in what way clocks need to be processed differently than any other value?

[fabianschuiki]

Take sv.assert.concurrent as an example, which has a clock input. So something roughly like sv.assert.concurrent %clock, %condition (it probably also has a posedge in there some where, plus some formatting). The clock indicates when the condition should be checked.

The way arcilator does its thing is by creating separate functions for each clock. So instead of having each op have a clock operand, the clocking is expressed as control flow through the op being listed inside a clock function. This means registers get translated as following:

// initial
%x = seq.compreg %nextValue, %clock

// arc conversion
%x = arc.state @ComputeNextValue(...) clock %clock

// clock grouping (in lower states I think)
%0 = detected posedge on %clock
arc.clock_tree %0 {
  %x = arc.state @ComputeNextValue(...)  // no more clock operand
}

// clock function extraction
func.func @RocketClock() {
    %x = arc.state @ComputeNextValue(...)
}
arc.trigger_clock @RocketClock()  // or similar

Because Arcilator wants to create a simulation model, clocks get turned into function calls. This also means that ops which have clocks must be transformed in that pipeline, from an initial representation with a clock to a later immediate representation without a clock.

For asserts, this would look similar to the following:

// initial
sv.assert.concurrent %clock, %condition

// arc conversion (option 1)
arc.assert %condition clock %clock 
// arc conversion (option 2)
%0 = ltl.clock %clock, %condition
verif.assert %0

// clock grouping
%1 = detect clock edge
arc.clock_tree %1 {
  // option 1
  arc.assert %condition  // without clock
  // option 2
  verif.assert %condition  // without clock
}

Using verif.assert directly could be very nice, but may come with its own challenges. But it could also force us to deal with the LTL dialect directly in Arcilator, which would be a big win!

[Moxinilian]

I think I need to spend some time looking at what arcilator does before the backend because I fail to understand the point of doing all this lol

[elhewaty]

https://github.com/llvm/circt/blob/main/lib/Dialect/Arc/Transforms/LowerArcsToFuncs.cpp

What is the difference between patterns in this file and ones in ArcToLLVM.cpp?

[maerhart]

There is no difference (except the content of the matchAndRewrite method of course). The difference is the conversion target. ArcToLLVM.cpp uses LLVMConversionTarget, which inherits from ConversionTarget (used in LowerArcsToFuncs) and already sets up the target legality (in this case the LLVM dialect).

[elhewaty]

If they both lower to LLVM, why splitting them?
I am sorry for all these questions.

[fabianschuiki]

If they both lower to LLVM, why splitting them?

These do slightly different things: LowerArcstoFuncs takes clock groups and replaces them with func.func ops, that is, a function defined in MLIR's func dialect. (

circt/lib/Dialect/Arc/Transforms/LowerArcsToFuncs.cpp

Lines 45 to 46 in bea8510

	auto func = rewriter.create<mlir::func::FuncOp>(op.getLoc(), op.getName(),
	op.getFunctionType());

) The ArcToLLVM conversion then takes these standard MLIR functions, along with all the other arc ops, and converts them to LLVM. This intermediate step with func.func allows us to reason about functions at an intermediate level, no longer arc-specific, but also not totally lowered to LLVM yet.

[elhewaty]

this is the definition of arc.assert what do you think?

def AssertOp : ArcOp<"assert"> {
  let summary = "assert that a properity holds.";
  let description = [{
    Asserts that an operation holds at runtime, it takes a single boolean
    as an input, and an error message.
    If the property holds (= `true`) the operation has no effect. Otherwise, the
    execution aborts and provide an error message to the user.
    ```mlir
    assert %proberty, "Some error message in case of failure!"
    ```
  }];
  // I thought of making the string message optional.
  // Also should it take clock as parameters?
  let arguments = (ins I1: $property, StrAttr:$msg);
  let assemblyFormat = "$property `,` $msg attr-dict";
}

If this is fine, our implementation will have 2 steps:

• Lower the assert op to LLVM and test coverage to make sure it works well.
• Lower verif.assert, and sv.assert.concurrent to arc.assert in ConvertToArc pass.
  For the second point I need to the conversion to be done before arc extraction, so before
  this line (

  circt/lib/Conversion/ConvertToArcs/ConvertToArcs.cpp

  Line 452 in bea8510

  if (failed(converter.run(getOperation())))

  ) I need to run applyPartialConversion, right?