[Arc] Add basic support for assert operation. #6839

elhewaty · 2024-03-17T01:55:46Z

Adds basic Assertion support to ARC
Fixes: https://github.com/llvm/circt/issues/6810

We will implement this in two steps:

Support the assert operation in Arc by adding arc.assert, and make sure it generates the correct LLVM code.
Lower verif.assert and sv.assert.concurrent operations to Arc.

elhewaty · 2024-03-17T02:04:15Z

Aside from the conflicts, I will resolve them later:
Can you share your opinions?
how to generate the CHECK tests?
for basic-error.mlir : this is the error unexpected error: use of value '%in' expects different type than prior uses: 'i1' vs 'i4'
if I write expected-error @below {{use of value '%in' expects different type than prior uses: 'i1' vs 'i4'}} why doesn't it work?

for the print message before the abort, I want to make something like call i32 @puts(ptr @.str)
can you give some hints about converting the message to Value?
I tried LLVM::createPrintStrCall, but it didn't work here.

maerhart · 2024-03-17T07:39:42Z

how to generate the CHECK tests?

You typically write them by hand. You could, however, run the RUN command at the start of the file in the CLI, copy-paste it to the test file, and insert the CHECK prefixes, etc to save some typing. Don't forget to double check if the output actually matches what you expect.

for basic-error.mlir : this is the error unexpected error: use of value '%in' expects different type than prior uses: 'i1' vs 'i4' if I write expected-error @below {{use of value '%in' expects different type than prior uses: 'i1' vs 'i4'}} why doesn't it work?

Did you check the location of the error and insert the expected-error directly at the line before?

for the print message before the abort, I want to make something like call i32 @puts(ptr @.str) can you give some hints about converting the message to Value? I tried LLVM::createPrintStrCall, but it didn't work here.

Can you give more detail about why createPrintStrCall didn't work?
The rough procedure is: create a global constant for the string, insert the puts function declaration, insert a 'addressof' to get a pointer to the global, pass its result to a call to puts.
You could take a look at the lowering pattern for arc.sim.emit for an example (it uses printf instead though).

test/Dialect/Arc/basic-errors.mlir

include/circt/Dialect/Arc/ArcOps.td

lib/Conversion/ArcToLLVM/LowerArcToLLVM.cpp

seldridge · 2024-03-29T03:38:29Z

how to generate the CHECK tests?

There's a bit of an art to this. You're trying to balance:

Exactness/terseness of the test. Try to keep the test simple and only check what the test needs to test not unrelated features or those tested elsewhere.
Robustness of the test. Ideally, the test should only fail for patches which actually cause the test to fail, not due to name changes, SSA value changes, or later IR additions. This is not possible to guarantee always. That's fine.
Readability of the test. Hopefully, someone reading the test (or your future self) will understand what it is trying to test. Striving for (1) helps here. Comments may be necessary to explain what is going on.

Generally, your tests look good!

Usually the only thing to avoid is exact copy-pasting of output. As Martin suggests, this can be a great starting point. Sometimes it is a useful exercise to intentionally write the test from scratch to make sure you aren't inadvertently relying on incorrect output.

elhewaty · 2024-03-29T03:47:09Z

I think we need to implement like llvm update_test_checks.py for circt-opt.

elhewaty · 2024-03-30T13:20:57Z

@fabianschuiki, @maerhart ping 🔔 !!

maerhart · 2024-03-31T07:54:39Z

include/circt/Dialect/Arc/ArcOps.td

@@ -880,4 +880,22 @@ def VectorizeReturnOp : ArcOp<"vectorize.return", [
  let assemblyFormat = "operands attr-dict `:` qualified(type(operands))";
 }

+def AssertOp : ArcOp<"assert"> {
+  let summary = "assert that a property holds.";


Suggested change

let summary = "assert that a property holds.";

let summary = "assert that a property holds";

include/circt/Dialect/Arc/ArcOps.td

maerhart · 2024-03-31T07:57:32Z

include/circt/Dialect/Arc/ArcOps.td

+    assert %proberty, %clock, "Some error message in case of failure!"
+    ```
+  }];
+  let arguments = (ins I1:$property, Optional<I1>:$clock, 


Can you add a paragrph in the description explaining why the clock operand is optional?

verif.assert doesn't have a clock operand. But I think I will need to give it a default value. verif.assert 0, has no clock operand. what do you think?

lib/Conversion/ArcToLLVM/LowerArcToLLVM.cpp

test/Conversion/ArcToLLVM/lower-arc-to-llvm.mlir

maerhart · 2024-03-31T08:31:25Z

test/Conversion/ArcToLLVM/lower-arc-to-llvm.mlir

+  // CHECK-NEXT:  }
+  %cond = hw.constant 0 : i1
+  %clock = hw.constant 1: i1
+  arc.assert %cond, %clock


I think at this stage of the Arc lowering pipeline, the clock operand should not be present anymore. Either it is folded into the cond operand or it is gone because the assert is in a function that is called only at the posedge of this clock. So the lowering pass to LLVM would just error out. But the clock operand will be useful in the lowering from verif and be dealt with in the passes between those two lowerings.
Also, shouldn't the clock operand be of seq.clock type?
@fabianschuiki What do you think?

I put a clock operand so we can make use of it for further steps, I am not sure why we need it in assert which checks the condition.

Yes, having the optional clock operand makes sense. But the clock operand just provides the raw value of the clock signal, but the assert is typically only checked at one or both of the clock edges (see ltl.clock operation). This behavior needs to be lowered and will probably happen before the ArcToLLVM pass. During this process this edge-checking logic could be folded into the condition.

the clock operand should not be present anymore. Either it is folded into the cond operand or it is gone because the assert is in a function that is called only at the posedge of this clock.

@maerhart, can you explain this a little further?

test/Dialect/Arc/basic-errors.mlir

maerhart · 2024-05-07T07:25:59Z

This operation looks a lot like the one proposed in #6982
We should discuss with @fabianschuiki if the TableGen declaration should be moved to the Verif dialect, or if it makes sense to have two almost identical operations in both dialects.

include/circt/Dialect/Arc/ArcOps.td

lib/Conversion/ArcToLLVM/LowerArcToLLVM.cpp

maerhart · 2024-05-07T07:37:50Z

lib/Conversion/ArcToLLVM/LowerArcToLLVM.cpp

+            std::string msgGlobalName =
+                std::string("Arc_Assert_Op_Msg: ") + message.str();


Maybe adding the source location to the message could be useful.

@maerhart I can't think of a way to get the location of the here are two cases:

If the message is provided directly to the operation (arc.assert bool, clock, "some message"), so the location of it is the location of the operation (aka arc.assert), here we map the same message contents to the same global string(address) which is very useful.

If the message is provided as a variable (arc.assert bool, clock, StrTypeOperand), I need to find a way to get the location of the operand and then map all users to the same message, as the location will be different for different messages, and maybe they have the same contents, but in different locations.

Is there any way to convert Location to StringRef?

@maerhart ping!

Yes, I mean the location that you get from assertOp.getLoc(). The Location class has a print function that you can use. Something like this:

std::string str; llvm::raw_string_ostream(str); loc.print(stream); // use str here

Because the message is a string attribute, you can just concatenate them at compile-time and still merge globals referring to the same string.

This is not super important, so if you're having issues with it, we can also just leave it away.

That's great, but I tried it now it generates a location like this:

/Path/To/circt/test/Conversion/ArcToLLVM/lower-arc-to-llvm.mlir:276:3

I can use some regex matching and the output will be lower-arc-to-llvm.mlir:276:3, but I think it will differ from path to path, I tried but I couldn't match it so I ignored this part!
If you have further suggestions, I will address them.

lib/Conversion/ArcToLLVM/LowerArcToLLVM.cpp

lib/Dialect/Arc/ArcOps.cpp

elhewaty · 2024-05-14T11:43:43Z

@maerhart I don't know what's wrong with the checker! I run clang-format on my local repo and I don't get any errors!!

maerhart · 2024-05-14T11:53:12Z

In the github actions summary you can download a patch it produced.

Here it is:

diff --git a/lib/Conversion/ArcToLLVM/LowerArcToLLVM.cpp b/lib/Conversion/ArcToLLVM/LowerArcToLLVM.cpp
index 120a140..7e06ed8 100644
--- a/lib/Conversion/ArcToLLVM/LowerArcToLLVM.cpp
+++ b/lib/Conversion/ArcToLLVM/LowerArcToLLVM.cpp
@@ -185,8 +185,7 @@ struct AssertOpLowering : public OpConversionPattern<arc::AssertOp> {
                                            rewriter.getBoolAttr(true)));
 
     rewriter.replaceOpWithNewOp<scf::IfOp>(
-        op, negateCondition,
-        [&](OpBuilder &builder, Location loc) {
+        op, negateCondition, [&](OpBuilder &builder, Location loc) {
           // If the condition doesn't hold then print the message and abort
           auto message = op.getMsg().value_or("");
           auto module = op->getParentOfType<ModuleOp>();

dtzSiFive · 2024-04-29T13:37:38Z

include/circt/Dialect/Arc/ArcOps.td

+    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, %clock, "Some error message in case of failure!"


Suggested change

assert %proberty, %clock, "Some error message in case of failure!"

assert %property, %clock, "Some error message in case of failure!"

dtzSiFive · 2024-05-14T12:19:29Z

lib/Conversion/ArcToLLVM/LowerArcToLLVM.cpp

@@ -624,7 +690,8 @@ void LowerArcToLLVMPass::runOnOperation() {
    StateReadOpLowering,
    StateWriteOpLowering,
    StorageGetOpLowering,
-    ZeroCountOpLowering
+    ZeroCountOpLowering,
+    AssertOpLowering


Maintain alpha-sort?

dtzSiFive · 2024-05-14T12:36:52Z

include/circt/Dialect/Arc/ArcOps.td

+    ```mlir
+    assert %property
+    assert %property, %clock
+    assert %property, %clock, "Some error message in case of failure!"


Can an assert have a message but no clock ("is that something we want to support")?

Consider differentiating these somehow, as-is this makes the parser do strange things if you omit the clock operand (arc.assert %in0, "Oops").

dtzSiFive · 2024-05-14T12:37:38Z

lib/Conversion/ArcToLLVM/LowerArcToLLVM.cpp

+            {
+              OpBuilder::InsertionGuard guard(rewriter);
+              rewriter.setInsertionPointToStart(module.getBody());
+              putsFunc = lookupOrCreateFn(


This looks unsafe, and should go through rewriter?

While looking into what to suggest, looks like there are various useful helpers for basically exactly this flow.

Additionally, cf.assert has an LLVM lowering -- was wondering if makes sense to lower to/use cf.assert since this seems rather similar?

Regardless, the lowering there uses the rewriter-aware and useful helpers for grabbing a print-like method as well as global strings:

https://github.com/llvm/llvm-project/blob/9d4f7f44b64d87d1068859906f43b7ce03a7388b/mlir/lib/Conversion/ControlFlowToLLVM/ControlFlowToLLVM.cpp#L52

It doesn't re-use the global string definition, FWIW, but anyway interesting related bits if not already on your radar.

And actually, looks like it ultimately just calls lookupOrCreateFn (or wrappers) anyway: https://github.com/llvm/llvm-project/blob/cc54129b983799e1aaea77aa0ff3040dc30cbc8c/mlir/lib/Conversion/LLVMCommon/PrintCallHelper.cpp#L63 . Not sure how creating a global is safe?

Seems like could do what this is doing using rewriter (instead of the builder it creates)?
https://github.com/llvm/llvm-project/blob/cc54129b983799e1aaea77aa0ff3040dc30cbc8c/mlir/lib/Dialect/LLVMIR/IR/FunctionCallUtils.cpp#L51
(possible upstream patch, but if nothing else locally if looking to address that...)

dtzSiFive · 2024-05-14T12:46:08Z

include/circt/Dialect/Arc/ArcOps.td

+    assert %property, %clock, "Some error message in case of failure!"
+    ```
+  }];
+  let arguments = (ins I1:$property, Optional<ClockType>:$clock,


Just curious, should this be using ClockedOpInterface?

Also the clock isn't used in this PR, what role might if have / why not needed to be part of the lowering?

dtzSiFive · 2024-05-14T12:46:48Z

lib/Conversion/ArcToLLVM/LowerArcToLLVM.cpp

+              Type int8Type = rewriter.getI8Type();
+
+              // Generate new names for global strings.
+              // Messgaes with the same contents, and the same locations


Suggested change

// Messgaes with the same contents, and the same locations

// Messages with the same contents, and the same locations

dtzSiFive · 2024-05-14T13:02:30Z

lib/Conversion/ArcToLLVM/LowerArcToLLVM.cpp

+              // Messgaes with the same contents, and the same locations
+              // are mapped to the same names
+              std::string msgGlobalName =
+                  std::string("Arc_Assert_Op_Msg: ") + message.str();


Especially with the colon and space it seems unlikely, but can we rely on that symbol not being defined?

Symbol name having the entire message seems like a lot? 🤔

elhewaty requested review from fabianschuiki and maerhart as code owners March 17, 2024 01:55

elhewaty marked this pull request as draft March 17, 2024 01:56

maerhart reviewed Mar 17, 2024

View reviewed changes

elhewaty force-pushed the arc-assert branch from 04ce087 to 796dd62 Compare March 28, 2024 21:41

elhewaty marked this pull request as ready for review March 28, 2024 21:50

elhewaty requested a review from maerhart March 28, 2024 21:50

elhewaty force-pushed the arc-assert branch from 796dd62 to 919b8b9 Compare March 29, 2024 00:22

maerhart reviewed Mar 31, 2024

View reviewed changes

elhewaty force-pushed the arc-assert branch 3 times, most recently from bbf58ea to a71c648 Compare May 5, 2024 01:42

elhewaty requested a review from maerhart May 5, 2024 01:43

elhewaty force-pushed the arc-assert branch from a71c648 to 672cf3f Compare May 5, 2024 19:31

maerhart reviewed May 7, 2024

View reviewed changes

elhewaty force-pushed the arc-assert branch from 672cf3f to f4344ad Compare May 11, 2024 16:45

elhewaty requested a review from maerhart May 11, 2024 16:46

[Arc] Add basic support for assert operation.

121a3d7

elhewaty force-pushed the arc-assert branch from f4344ad to 121a3d7 Compare May 14, 2024 11:58

dtzSiFive reviewed May 14, 2024

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Arc] Add basic support for assert operation. #6839

[Arc] Add basic support for assert operation. #6839

elhewaty commented Mar 17, 2024 •

edited

elhewaty commented Mar 17, 2024

maerhart commented Mar 17, 2024

seldridge commented Mar 29, 2024

elhewaty commented Mar 29, 2024

elhewaty commented Mar 30, 2024

maerhart Mar 31, 2024

maerhart Mar 31, 2024

elhewaty Apr 1, 2024

maerhart Mar 31, 2024

elhewaty Apr 1, 2024

maerhart Apr 2, 2024

elhewaty May 5, 2024

maerhart commented May 7, 2024

maerhart May 7, 2024

elhewaty May 8, 2024 •

edited

elhewaty May 10, 2024

maerhart May 11, 2024

elhewaty May 11, 2024

elhewaty commented May 14, 2024

maerhart commented May 14, 2024

dtzSiFive Apr 29, 2024

dtzSiFive May 14, 2024

dtzSiFive May 14, 2024

dtzSiFive May 14, 2024

dtzSiFive May 14, 2024

dtzSiFive May 14, 2024

dtzSiFive May 14, 2024

dtzSiFive May 14, 2024

	let summary = "assert that a property holds.";
	let summary = "assert that a property holds";

		std::string msgGlobalName =
		std::string("Arc_Assert_Op_Msg: ") + message.str();

	assert %proberty, %clock, "Some error message in case of failure!"
	assert %property, %clock, "Some error message in case of failure!"

	// Messgaes with the same contents, and the same locations
	// Messages with the same contents, and the same locations

[Arc] Add basic support for assert operation. #6839

Are you sure you want to change the base?

[Arc] Add basic support for assert operation. #6839

Conversation

elhewaty commented Mar 17, 2024 • edited

elhewaty commented Mar 17, 2024

maerhart commented Mar 17, 2024

seldridge commented Mar 29, 2024

elhewaty commented Mar 29, 2024

elhewaty commented Mar 30, 2024

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

maerhart commented May 7, 2024

Choose a reason for hiding this comment

elhewaty May 8, 2024 • edited

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

elhewaty commented May 14, 2024

maerhart commented May 14, 2024

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

elhewaty commented Mar 17, 2024 •

edited

elhewaty May 8, 2024 •

edited