Skip to content

[FIRRTL][OM] Add property asserts#10093

Draft
seldridge wants to merge 6 commits intomainfrom
dev/seldridge/firrtl-property-asserts
Draft

[FIRRTL][OM] Add property asserts#10093
seldridge wants to merge 6 commits intomainfrom
dev/seldridge/firrtl-property-asserts

Conversation

@seldridge
Copy link
Copy Markdown
Member

Add support for a FIRRTL property assert and an OM property assert. This
is intended to allow for front-end language users to define metadata
constraints. These constraints are either compile-time known to be
true/false or they are evaluated at metadata evaluation time.

This is part of building towards adding FIRRTL domain constraints. At
present, FIRRTL only has maximally unsafe firrtl.unsafe_domain_cast
operations. We'd like to have the ability to do this unsafe cast, but
apply additional constraints. E.g., for a synchronous clock domain
crossing, we'd like to be able to say that the crossing must be between
two domains which are synchronous to each other. However, at present we
cannot do this and a synchronous crossing looks the same as an
asynchronous crossing. This is infrastructure to enable this kind of
check.

Commits are logical and should be reviewed independently.

AI-assisted-by: Claude Code (Claude Sonnet 4.6, Claude Haiku 4.5)

Add PropertyAssertOp to FIRRTLStatements.td. The operation asserts that a
boolean property holds, accepting a !firrtl.bool condition and a string
message. It is valid in firrtl.module and firrtl.class bodies (via
ParentOneOf), mirroring firrtl.propassign. Static evaluation and lowering
to the OM evaluator will follow in subsequent commits.

AI-assisted-by: Claude Code (Claude Sonnet 4.6)
Signed-off-by: Schuyler Eldridge <schuyler.eldridge@sifive.com>
If the condition operand is a statically-known false constant
(BoolConstantOp with value=false), the verifier reports an immediate
compile-time error. Statically-true conditions are left for a future
canonicalization to remove. Non-constant conditions are deferred to the
OM evaluator.

AI-assisted-by: Claude Code (Claude Sonnet 4.6)
Signed-off-by: Schuyler Eldridge <schuyler.eldridge@sifive.com>
Add a propassert keyword to the FIR text format. The syntax is:

  propassert <cond>, "<message>"
  propassert <cond>, "<message>" : <name>

The condition must be of Bool type. Parsing and emission follow the
same patterns as propassign. Feature-gated under missingSpecFIRVersion
as the operation is a CIRCT extension not yet in the FIRRTL spec.

AI-assisted-by: Claude Code (Claude Sonnet 4.6)
Signed-off-by: Schuyler Eldridge <schuyler.eldridge@sifive.com>
Add PropertyAssertOp to OMOps.td. The operation accepts a 1-bit integer
condition and a string message, producing no result. When the OM
evaluator resolves the condition to zero it will raise a runtime error.
Evaluator support follows in a subsequent commit.

AI-assisted-by: Claude Code (Claude Sonnet 4.6)
Signed-off-by: Schuyler Eldridge <schuyler.eldridge@sifive.com>
Lower FIRRTL property asserts to OM property asserts.  Map everything
one-to-one, except for the name which is merged into the OM property
assert message.

AI-assisted-by: Claude Code (Claude Sonnet 4.6)
Signed-off-by: Schuyler Eldridge <schuyler.eldridge@sifive.com>
Evaluate om.property_assert ops during object instantiation. After
resolving all field values, iterate over any PropertyAssertOps in the
class body and check the condition. If the condition evaluates to a
known-false i1 value, return an error with the assertion message.
Unknown (unevaluated) conditions are silently skipped (best-effort).

Adds C API tests in test/CAPI/om.c and Python integration tests.

AI-assisted-by: Claude Code (Claude Sonnet 4.6)
Signed-off-by: Schuyler Eldridge <schuyler.eldridge@sifive.com>
@fabianschuiki
Copy link
Copy Markdown
Contributor

Results of circt-tests run for 7eb04bf compared to results for 5dc62fe: no change to test results.

Copy link
Copy Markdown
Contributor

@mikeurbach mikeurbach left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The general boilerplate and plumbing of new ops through the pipeline looks good to me, as do the actual op definitions.

Just a couple comments on the evaluator and some edge cases that I don't think this handles.

// If the condition is unknown, skip silently (best-effort).
if (condValue->isUnknown())
continue;
if (auto *attrVal = dyn_cast<evaluator::AttributeValue>(condValue.get())) {
Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

besides constant attributes, this could also be a field of an object. we have to handle something like that in the arithmetic ops for example:

// Extract the integer attributes.
auto extractAttr = [](evaluator::EvaluatorValue *value) {
return std::move(
llvm::TypeSwitch<evaluator::EvaluatorValue *, om::IntegerAttr>(value)
.Case([](evaluator::AttributeValue *val) {
return val->getAs<om::IntegerAttr>();
})
.Case([](evaluator::ReferenceValue *val) {
return cast<evaluator::AttributeValue>(
val->getStrippedValue()->get())
->getAs<om::IntegerAttr>();
}));
};

i would add some evaluator unit tests for this change in general. a couple edge cases we test for the arithmetic operations is a) the evaluator value is from object fields, and b) the evaluator value is from object fields, and there are cycles such that the value isn't ready right away.

specifically for that latter b) case, we have this isFullyEvaluated handling, which I don't see here yet:

// Evaluate operands if necessary, and return the partially evaluated value if
// they aren't ready.
auto lhsResult = evaluateValue(op.getLhs(), actualParams, loc);
if (failed(lhsResult))
return lhsResult;
if (!lhsResult.value()->isFullyEvaluated())
return handle;
auto rhsResult = evaluateValue(op.getRhs(), actualParams, loc);
if (failed(rhsResult))
return rhsResult;
if (!rhsResult.value()->isFullyEvaluated())
return handle;

let arguments = (ins
BoolType:$condition,
StrAttr:$message,
OptionalAttr<StrAttr>:$name
Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is a label needed even wen OM assert doesn't have one?

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It's questionable. Probably not. This is now used in the lowering to the OM asserts, however, it's just used as a prefix if it exists.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants