terapines
/
circt
mirror of https://github.com/llvm/circt.git
2
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

[FIRRTL][Verif][LTL] Replace `ltl.disable` with an enable folded into `verif.assert` (#7150) 

This PR gets rid of the `ltl.disable` op and intrinsic in favor of having an enable operand on the verif assert like ops. This made it trivial to fix an incorrect when condition folding for `AssertProperty`. Most of the PR relates to fixing the chaos that was caused by removing `ltl.disable`.
This commit is contained in:
Amelia Dobis 2024-06-20 11:24:37 -07:00 committed by GitHub
parent a3f726dc7f
commit ef30e1f20a
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
30 changed files with 499 additions and 587 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
include/circt/Dialect/FIRRTL/FIRRTLExpressions.td
View File

@ -1474,6 +1474,5 @@ def LTLClockIntrinsicOp : LTLIntrinsicOp<"clock"> {
$input `,` $clock attr-dict `:` functional-type(operands, results)
}];
}
def LTLDisableIntrinsicOp : BinaryLTLIntrinsicOp<"disable">;
#endif // CIRCT_DIALECT_FIRRTL_FIRRTLEXPRESSIONS_TD

3
include/circt/Dialect/FIRRTL/FIRRTLIntrinsics.h
View File

@ -34,7 +34,8 @@ struct GenericIntrinsic {
// Input checking
//===--------------------------------------------------------------------===//
ParseResult hasNInputs(unsigned n);
ParseResult hasNInputs(unsigned n, unsigned c);
unsigned getNumInputs();
template <typename C>
ParseResult checkInputType(unsigned n, const Twine &msg, C &&call) {

2
include/circt/Dialect/FIRRTL/FIRRTLStatements.td
View File

@ -357,7 +357,7 @@ class VerifIntrinsicOp<string mnemonic, list<Trait> traits = []> :
FIRRTLOp<"int.verif." # mnemonic, traits> {
let summary = "FIRRTL variant of `verif." # mnemonic # "`";
let description = "See `verif." # mnemonic # "` op in the Verif dialect.";
let arguments = (ins UInt1Type:$property, OptionalAttr<StrAttr>:$label);
let arguments = (ins UInt1Type:$property, Optional<UInt1Type>:$enable, OptionalAttr<StrAttr>:$label);
let assemblyFormat = [{
operands attr-dict `:` type(operands)
}];

6
include/circt/Dialect/FIRRTL/FIRRTLVisitors.h
View File

@ -55,9 +55,8 @@ public:
LTLRepeatIntrinsicOp, LTLGoToRepeatIntrinsicOp,
LTLNonConsecutiveRepeatIntrinsicOp, LTLNotIntrinsicOp,
LTLImplicationIntrinsicOp, LTLUntilIntrinsicOp,
LTLEventuallyIntrinsicOp, LTLClockIntrinsicOp,
LTLDisableIntrinsicOp, Mux2CellIntrinsicOp, Mux4CellIntrinsicOp,
HasBeenResetIntrinsicOp,
LTLEventuallyIntrinsicOp, LTLClockIntrinsicOp, Mux2CellIntrinsicOp,
Mux4CellIntrinsicOp, HasBeenResetIntrinsicOp,
// Miscellaneous.
BitsPrimOp, HeadPrimOp, MuxPrimOp, PadPrimOp, ShlPrimOp, ShrPrimOp,
TailPrimOp, VerbatimExprOp, HWStructCastOp, BitCastOp, RefSendOp,
@ -186,7 +185,6 @@ public:
HANDLE(LTLUntilIntrinsicOp, Unhandled);
HANDLE(LTLEventuallyIntrinsicOp, Unhandled);
HANDLE(LTLClockIntrinsicOp, Unhandled);
HANDLE(LTLDisableIntrinsicOp, Unhandled);
HANDLE(Mux4CellIntrinsicOp, Unhandled);
HANDLE(Mux2CellIntrinsicOp, Unhandled);
HANDLE(HasBeenResetIntrinsicOp, Unhandled);

82
include/circt/Dialect/LTL/LTLOps.td
View File

@ -160,10 +160,7 @@ def ConcatOp : LTLOp<"concat", [Pure]> {
}];
}
def RepeatOp : LTLOp<"repeat", [
Pure,
PredOpTrait<"'base' must be >= 0", CPred<"$base >= 0">>
]> {
def RepeatOp : LTLOp<"repeat", [Pure]> {
let arguments = (ins
LTLAnySequenceType:$input,
I64Attr:$base,
@ -188,11 +185,7 @@ def RepeatOp : LTLOp<"repeat", [
}];
}
def GoToRepeatOp : LTLOp<"goto_repeat", [
Pure,
PredOpTrait<"'base' must be >= 0", CPred<"$base >= 0">>,
PredOpTrait<"'more' must be >= 0", CPred<"$more >= 0">>
]> {
def GoToRepeatOp : LTLOp<"goto_repeat", [Pure]> {
let arguments = (ins
LTLAnySequenceType:$input,
I64Attr:$base,
@ -214,11 +207,7 @@ def GoToRepeatOp : LTLOp<"goto_repeat", [
}];
}
def NonConsecutiveRepeatOp : LTLOp<"non_consecutive_repeat", [
Pure,
PredOpTrait<"'base' must be >= 0", CPred<"$base >= 0">>,
PredOpTrait<"'more' must be >= 0", CPred<"$more >= 0">>
]> {
def NonConsecutiveRepeatOp : LTLOp<"non_consecutive_repeat", [Pure]> {
let arguments = (ins
LTLAnySequenceType:$input,
I64Attr:$base,
@ -356,69 +345,4 @@ def ClockOp : LTLOp<"clock", [
}];
}
def DisableOp : LTLOp<"disable", [Pure]> {
let arguments = (ins LTLAnyPropertyType:$input, I1:$condition);
let results = (outs LTLPropertyType:$result);
let assemblyFormat = [{
$input `if` $condition attr-dict `:` type($input)
}];
let hasFolder = 1;
let summary = "Disable the evaluation of a property based on a condition.";
let description = [{
Creates a new property which evaluates the given `$input` property only if
the given disable `$condition` is false throughout the entire evaluation. If
the `$condition` is true at any point in time during the evaluation of
`$input`, the resulting property is disabled.
The disabling is "infectious". If a property is disabled, it also implicitly
disables all properties that use it. Consider the following example:
```
%0 = ltl.disable %prop if %cond
%1 = ltl.or %0, %otherProp
```
If the property `%0` is disabled, the derived property `%1` is also
disabled.
As a result, it is always legal to canonicalize the IR into a form where
there is only one `ltl.disable` operation at the root of a property
expression.
Note that a property being disabled based on a condition is different from a
property that trivially evaluates to true if the condition does not hold.
The former ensures that a property is only checked when a certain condition
is true, but the number of cases in which the property holds or doesn't hold
remains unchanged. The latter adds additional cases where the property
holds, which can offer a solver unintended ways to make assertions or
coverage proofs derived from the property pass. For example:
```
%p0 = ltl.or %prop, %cond
%p1 = ltl.disable %prop if %cond
```
`$cond` being true would disable the evaluation of `%p0` and would make
`%p1` evaluate to true. These are subtly different. If used in an assertion
during simulation, `$cond` would adequately disable triggering of the
assertion in both cases. However, if used in a formal verification setting
where proofs for `%p0` and `%p1` always holding or never holding are sought,
a solver might use `%cond = true` to trivially make `%p0` hold, which is not
possible for `%p1`. Consider the following more concrete example:
```
%p2 = ltl.or %protocolCorrectProperty, %reset
%p3 = ltl.disable %protocolCorrectProperty if %reset
verif.cover %p2
verif.cover %p3
```
The intent is to formally prove coverage for `%protocolCorrectProperty`
while the circuit is in regular operation (i.e., out of reset). A formal
solver would trivially prove coverage for `%p2` by assigning
`%reset = true`, but would have to actually prove coverage for the
underlying `%protocolCorrectProperty` for `%p3`. The latter is almost always
the intended behavior.
}];
}
#endif // CIRCT_DIALECT_LTL_LTLOPS_TD

3
include/circt/Dialect/LTL/LTLVisitors.h
View File

@ -22,7 +22,7 @@ public:
auto *thisCast = static_cast<ConcreteType *>(this);
return TypeSwitch<Operation *, ResultType>(op)
.template Case<AndOp, OrOp, DelayOp, ConcatOp, RepeatOp, NotOp,
ImplicationOp, UntilOp, EventuallyOp, ClockOp, DisableOp,
ImplicationOp, UntilOp, EventuallyOp, ClockOp,
IntersectOp, NonConsecutiveRepeatOp, GoToRepeatOp>(
[&](auto op) -> ResultType {
return thisCast->visitLTL(op, args...);
@ -59,7 +59,6 @@ public:
HANDLE(UntilOp, Unhandled);
HANDLE(EventuallyOp, Unhandled);
HANDLE(ClockOp, Unhandled);
HANDLE(DisableOp, Unhandled);
HANDLE(IntersectOp, Unhandled);
HANDLE(NonConsecutiveRepeatOp, Unhandled);
HANDLE(GoToRepeatOp, Unhandled);

16
include/circt/Dialect/Verif/VerifOps.td
View File

@ -28,11 +28,13 @@ class VerifOp<string mnemonic, list<Trait> traits = []> :
class AssertLikeOp<string mnemonic, list<Trait> traits = []> :
VerifOp<mnemonic, traits> {
let arguments = (ins LTLAnyPropertyType:$property,
let arguments = (ins LTLAnyPropertyType:$property, Optional<I1>:$enable,
OptionalAttr<StrAttr>:$label);
let assemblyFormat = [{
$property (`label` $label^)? attr-dict `:` type($property)
$property (`if` $enable^)? (`label` $label^)? attr-dict `:` type($property)
}];
let hasCanonicalizeMethod = true;
}
def AssertOp : AssertLikeOp<"assert"> {
@ -64,11 +66,11 @@ def ClockEdgeAttr : I32EnumAttr<"ClockEdge", "clock edge",
class ClockedAssertLikeOp<string mnemonic, list<Trait> traits = []> :
VerifOp<mnemonic, traits> {
let arguments = (ins LTLAnyPropertyType:$property,
I1:$disable,
ClockEdgeAttr:$edge, I1:$clock,
Optional<I1>:$enable,
OptionalAttr<StrAttr>:$label);
let assemblyFormat = [{
$property `disable` $disable `clock` $edge $clock
$property (`if` $enable^)? `,` $edge $clock
(`label` $label^)? attr-dict `:` type($property)
}];
}
@ -76,7 +78,7 @@ class ClockedAssertLikeOp<string mnemonic, list<Trait> traits = []> :
def ClockedAssertOp : ClockedAssertLikeOp<"clocked_assert"> {
let summary = [{
Assert that a property holds, checked on a given clock's
ticks and disabled if a given condition holds. Only supports
ticks and enabled if a given condition holds. Only supports
a single clock and a single disable.
}];
}
@ -84,7 +86,7 @@ def ClockedAssertOp : ClockedAssertLikeOp<"clocked_assert"> {
def ClockedAssumeOp : ClockedAssertLikeOp<"clocked_assume"> {
let summary = [{
Assume that a property holds, checked on a given clock's
ticks and disabled if a given condition holds. Only supports
ticks and enabled if a given condition holds. Only supports
a single clock and a single disable.
}];
}
@ -92,7 +94,7 @@ def ClockedAssumeOp : ClockedAssertLikeOp<"clocked_assume"> {
def ClockedCoverOp : ClockedAssertLikeOp<"clocked_cover"> {
let summary = [{
Cover on the holding of a property, checked on a given clock's
ticks and disabled if a given condition holds. Only supports
ticks and enabled if a given condition holds. Only supports
a single clock and a single disable.
}];
}

106
lib/Conversion/ExportVerilog/ExportVerilog.cpp
View File

@ -779,9 +779,6 @@ static bool isExpressionUnableToInline(Operation *op,
// Helper to determine if the use will be part of "event control",
// based on what the operation using it is and as which operand.
auto usedInExprControl = [user, &use]() {
// "disable iff" condition must be a name.
if (auto disableOp = dyn_cast<ltl::DisableOp>(user))
return disableOp.getCondition() == use.get();
// LTL Clock up's clock operand must be a name.
if (auto clockOp = dyn_cast<ltl::ClockOp>(user))
return clockOp.getClock() == use.get();
@ -3453,15 +3450,15 @@ public:
assert(state.pp.getListener() == &state.saver);
}
/// Emit the specified value as an SVA property or sequence. This is the entry
/// point to print an entire tree of property or sequence expressions in one
/// go.
void emitProperty(
Value property,
/// Emit the specified value as an SVA property or sequence with an enable
/// signal. This is the entry point to print an entire tree of property or
/// sequence expressions in one go.
void emitEnabledProperty(
Value property, Value enable,
PropertyPrecedence parenthesizeIfLooserThan = PropertyPrecedence::Lowest);
// Emits a property that is directly associated to a single clock and a single
// disable. Note that it is illegal to nest disable or clock operations in the
// enable. Note that it is illegal to nest clock operations in the
// property itself here.
void emitClockedProperty(
Value property, Value clock, ltl::ClockEdge edge, Value disable,
@ -3490,7 +3487,6 @@ private:
EmittedProperty visitLTL(ltl::UntilOp op);
EmittedProperty visitLTL(ltl::EventuallyOp op);
EmittedProperty visitLTL(ltl::ClockOp op);
EmittedProperty visitLTL(ltl::DisableOp op);
void emitLTLConcat(ValueRange inputs);
@ -3513,10 +3509,20 @@ private:
};
} // end anonymous namespace
void PropertyEmitter::emitProperty(
Value property, PropertyPrecedence parenthesizeIfLooserThan) {
void PropertyEmitter::emitEnabledProperty(
Value property, Value enable, PropertyPrecedence parenthesizeIfLooserThan) {
assert(localTokens.empty());
// Wrap to this column.
// If the property is tied to an enable, emit that.
if (enable) {
ps << "disable iff" << PP::nbsp << "(~(";
ps.scopedBox(PP::ibox2, [&] {
emitNestedProperty(enable, PropertyPrecedence::Unary);
ps << "))";
});
ps << PP::space;
}
ps.scopedBox(PP::ibox0,
[&] { emitNestedProperty(property, parenthesizeIfLooserThan); });
// If we are not using an external token buffer provided through the
@ -3527,7 +3533,7 @@ void PropertyEmitter::emitProperty(
}
void PropertyEmitter::emitClockedProperty(
Value property, Value clock, ltl::ClockEdge edge, Value disable,
Value property, Value clock, ltl::ClockEdge edge, Value enable,
PropertyPrecedence parenthesizeIfLooserThan) {
assert(localTokens.empty());
// Wrap to this column.
@ -3538,12 +3544,15 @@ void PropertyEmitter::emitClockedProperty(
ps << ")";
});
ps << PP::space;
ps << "disable iff" << PP::nbsp << "(";
ps.scopedBox(PP::ibox2, [&] {
emitNestedProperty(disable, PropertyPrecedence::Lowest);
ps << ")";
});
// If the property is tied to an enable, emit that.
if (enable) {
ps << PP::space;
ps << "disable iff" << PP::nbsp << "(~(";
ps.scopedBox(PP::ibox2, [&] {
emitNestedProperty(enable, PropertyPrecedence::Lowest);
ps << "))";
});
}
ps << PP::space;
ps.scopedBox(PP::ibox0,
@ -3786,17 +3795,6 @@ EmittedProperty PropertyEmitter::visitLTL(ltl::ClockOp op) {
return {PropertyPrecedence::Clocking};
}
EmittedProperty PropertyEmitter::visitLTL(ltl::DisableOp op) {
ps << "disable iff" << PP::nbsp << "(";
ps.scopedBox(PP::ibox2, [&] {
emitNestedProperty(op.getCondition(), PropertyPrecedence::Lowest);
ps << ")";
});
ps << PP::space;
emitNestedProperty(op.getInput(), PropertyPrecedence::Clocking);
return {PropertyPrecedence::Clocking};
}
// NOLINTEND(misc-no-recursion)
//===----------------------------------------------------------------------===//
@ -4010,16 +4008,15 @@ private:
const SmallPtrSetImpl<Operation *> &locationOps,
StringRef multiLineComment = StringRef());
LogicalResult emitVerifAssertLike(Operation *op, Value property,
LogicalResult emitVerifAssertLike(Operation *op, Value property, Value enable,
PPExtString opName);
LogicalResult visitVerif(verif::AssertOp op);
LogicalResult visitVerif(verif::AssumeOp op);
LogicalResult visitVerif(verif::CoverOp op);
LogicalResult emitVerifClockedAssertLike(Operation *op, Value property,
Value disable, Value clock,
verif::ClockEdge edge,
PPExtString opName);
Value clock, verif::ClockEdge edge,
Value enable, PPExtString opName);
LogicalResult visitVerif(verif::ClockedAssertOp op);
LogicalResult visitVerif(verif::ClockedAssumeOp op);
LogicalResult visitVerif(verif::ClockedCoverOp op);
@ -4887,6 +4884,7 @@ LogicalResult StmtEmitter::visitSV(CoverConcurrentOp op) {
/// Emit an assert-like operation from the `verif` dialect. This covers
/// `verif.assert`, `verif.assume`, and `verif.cover`.
LogicalResult StmtEmitter::emitVerifAssertLike(Operation *op, Value property,
Value enable,
PPExtString opName) {
if (hasSVAttributes(op))
emitError(op, "SV attributes emission is unimplemented for the op");
@ -4899,8 +4897,9 @@ LogicalResult StmtEmitter::emitVerifAssertLike(Operation *op, Value property,
// See IEEE 1800-2017 section 16.14.5 "Using concurrent assertion statements
// outside procedural code" and 16.14.6 "Embedding concurrent assertions in
// procedural code".
Operation *parent = op->getParentOp();
bool isTemporal = !property.getType().isSignlessInteger(1);
bool isProcedural = op->getParentOp()->hasTrait<ProceduralRegion>();
bool isProcedural = parent->hasTrait<ProceduralRegion>();
bool emitAsImmediate = !isTemporal && isProcedural;
startStatement();
@ -4915,7 +4914,7 @@ LogicalResult StmtEmitter::emitVerifAssertLike(Operation *op, Value property,
else
ps << opName << PP::nbsp << "property" << PP::nbsp << "(";
ps.scopedBox(PP::ibox2, [&]() {
PropertyEmitter(emitter, ops).emitProperty(property);
PropertyEmitter(emitter, ops).emitEnabledProperty(property, enable);
ps << ");";
});
});
@ -4926,22 +4925,26 @@ LogicalResult StmtEmitter::emitVerifAssertLike(Operation *op, Value property,
}
LogicalResult StmtEmitter::visitVerif(verif::AssertOp op) {
return emitVerifAssertLike(op, op.getProperty(), PPExtString("assert"));
return emitVerifAssertLike(op, op.getProperty(), op.getEnable(),
PPExtString("assert"));
}
LogicalResult StmtEmitter::visitVerif(verif::AssumeOp op) {
return emitVerifAssertLike(op, op.getProperty(), PPExtString("assume"));
return emitVerifAssertLike(op, op.getProperty(), op.getEnable(),
PPExtString("assume"));
}
LogicalResult StmtEmitter::visitVerif(verif::CoverOp op) {
return emitVerifAssertLike(op, op.getProperty(), PPExtString("cover"));
return emitVerifAssertLike(op, op.getProperty(), op.getEnable(),
PPExtString("cover"));
}
/// Emit an assert-like operation from the `verif` dialect. This covers
/// `verif.clocked_assert`, `verif.clocked_assume`, and `verif.clocked_cover`.
LogicalResult StmtEmitter::emitVerifClockedAssertLike(
Operation *op, Value property, Value disable, Value clock,
verif::ClockEdge edge, PPExtString opName) {
LogicalResult
StmtEmitter::emitVerifClockedAssertLike(Operation *op, Value property,
Value clock, verif::ClockEdge edge,
Value enable, PPExtString opName) {
if (hasSVAttributes(op))
emitError(op, "SV attributes emission is unimplemented for the op");
@ -4953,8 +4956,9 @@ LogicalResult StmtEmitter::emitVerifClockedAssertLike(
// See IEEE 1800-2017 section 16.14.5 "Using concurrent assertion statements
// outside procedural code" and 16.14.6 "Embedding concurrent assertions in
// procedural code".
Operation *parent = op->getParentOp();
bool isTemporal = !property.getType().isSignlessInteger(1);
bool isProcedural = op->getParentOp()->hasTrait<ProceduralRegion>();
bool isProcedural = parent->hasTrait<ProceduralRegion>();
bool emitAsImmediate = !isTemporal && isProcedural;
startStatement();
@ -4971,7 +4975,7 @@ LogicalResult StmtEmitter::emitVerifClockedAssertLike(
ps.scopedBox(PP::ibox2, [&]() {
PropertyEmitter(emitter, ops)
.emitClockedProperty(property, clock, verifToltlClockEdge(edge),
disable);
enable);
ps << ");";
});
});
@ -4983,20 +4987,20 @@ LogicalResult StmtEmitter::emitVerifClockedAssertLike(
// FIXME: emit property assertion wrapped in a clock and disabled
LogicalResult StmtEmitter::visitVerif(verif::ClockedAssertOp op) {
return emitVerifClockedAssertLike(op, op.getProperty(), op.getDisable(),
op.getClock(), op.getEdge(),
return emitVerifClockedAssertLike(op, op.getProperty(), op.getClock(),
op.getEdge(), op.getEnable(),
PPExtString("assert"));
}
LogicalResult StmtEmitter::visitVerif(verif::ClockedAssumeOp op) {
return emitVerifClockedAssertLike(op, op.getProperty(), op.getDisable(),
op.getClock(), op.getEdge(),
return emitVerifClockedAssertLike(op, op.getProperty(), op.getClock(),
op.getEdge(), op.getEnable(),
PPExtString("assume"));
}
LogicalResult StmtEmitter::visitVerif(verif::ClockedCoverOp op) {
return emitVerifClockedAssertLike(op, op.getProperty(), op.getDisable(),
op.getClock(), op.getEdge(),
return emitVerifClockedAssertLike(op, op.getProperty(), op.getClock(),
op.getEdge(), op.getEnable(),
PPExtString("cover"));
}

26
lib/Conversion/FIRRTLToHW/LowerToHW.cpp
View File

@ -1632,7 +1632,9 @@ struct FIRRTLLowering : public FIRRTLVisitor<FIRRTLLowering, LogicalResult> {
LogicalResult visitExpr(LTLUntilIntrinsicOp op);
LogicalResult visitExpr(LTLEventuallyIntrinsicOp op);
LogicalResult visitExpr(LTLClockIntrinsicOp op);
LogicalResult visitExpr(LTLDisableIntrinsicOp op);
template <typename TargetOp, typename IntrinsicOp>
LogicalResult lowerVerifIntrinsicOp(IntrinsicOp op);
LogicalResult visitStmt(VerifAssertIntrinsicOp op);
LogicalResult visitStmt(VerifAssumeIntrinsicOp op);
LogicalResult visitStmt(VerifCoverIntrinsicOp op);
@ -3791,28 +3793,24 @@ LogicalResult FIRRTLLowering::visitExpr(LTLClockIntrinsicOp op) {
getLoweredNonClockValue(op.getClock()));
}
LogicalResult FIRRTLLowering::visitExpr(LTLDisableIntrinsicOp op) {
return setLoweringToLTL<ltl::DisableOp>(
op,
ValueRange{getLoweredValue(op.getLhs()), getLoweredValue(op.getRhs())});
template <typename TargetOp, typename IntrinsicOp>
LogicalResult FIRRTLLowering::lowerVerifIntrinsicOp(IntrinsicOp op) {
auto property = getLoweredValue(op.getProperty());
auto enable = op.getEnable() ? getLoweredValue(op.getEnable()) : Value();
builder.create<TargetOp>(property, enable, op.getLabelAttr());
return success();
}
LogicalResult FIRRTLLowering::visitStmt(VerifAssertIntrinsicOp op) {
builder.create<verif::AssertOp>(getLoweredValue(op.getProperty()),
op.getLabelAttr());
return success();
return lowerVerifIntrinsicOp<verif::AssertOp>(op);
}
LogicalResult FIRRTLLowering::visitStmt(VerifAssumeIntrinsicOp op) {
builder.create<verif::AssumeOp>(getLoweredValue(op.getProperty()),
op.getLabelAttr());
return success();
return lowerVerifIntrinsicOp<verif::AssumeOp>(op);
}
LogicalResult FIRRTLLowering::visitStmt(VerifCoverIntrinsicOp op) {
builder.create<verif::CoverOp>(getLoweredValue(op.getProperty()),
op.getLabelAttr());
return success();
return lowerVerifIntrinsicOp<verif::CoverOp>(op);
}
LogicalResult FIRRTLLowering::visitExpr(HasBeenResetIntrinsicOp op) {

245
lib/Conversion/HWToBTOR2/HWToBTOR2.cpp
View File

@ -26,6 +26,9 @@
#include "circt/Dialect/SV/SVVisitors.h"
#include "circt/Dialect/Seq/SeqDialect.h"
#include "circt/Dialect/Seq/SeqOps.h"
#include "circt/Dialect/Verif/VerifDialect.h"
#include "circt/Dialect/Verif/VerifOps.h"
#include "circt/Dialect/Verif/VerifVisitors.h"
#include "mlir/Pass/Pass.h"
#include "llvm/ADT/MapVector.h"
#include "llvm/ADT/TypeSwitch.h"
@ -46,7 +49,8 @@ struct ConvertHWToBTOR2Pass
: public circt::impl::ConvertHWToBTOR2Base<ConvertHWToBTOR2Pass>,
public comb::CombinationalVisitor<ConvertHWToBTOR2Pass>,
public sv::Visitor<ConvertHWToBTOR2Pass>,
public hw::TypeOpVisitor<ConvertHWToBTOR2Pass> {
public hw::TypeOpVisitor<ConvertHWToBTOR2Pass>,
public verif::Visitor<ConvertHWToBTOR2Pass> {
public:
ConvertHWToBTOR2Pass(raw_ostream &os) : os(os) {}
// Executes the pass
@ -218,8 +222,8 @@ private:
// Generates a constant declaration given a value, a width and a name.
void genConst(int64_t value, size_t width, Operation *op) {
// For now we're going to assume that the name isn't taken, given that hw is
// already in SSA form
// For now we're going to assume that the name isn't taken, given that hw
// is already in SSA form
size_t opLID = getOpLID(op);
// Retrieve the lid associated with the sort (sid)
@ -258,15 +262,15 @@ private:
size_t sid = sortToLIDMap.at(width);
size_t initValLID = getOpLID(initVal);
// Build and emit the string (the lid here doesn't need to be associated to
// an op as it won't be used)
// Build and emit the string (the lid here doesn't need to be associated
// to an op as it won't be used)
os << lid++ << " "
<< "init"
<< " " << sid << " " << regLID << " " << initValLID << "\n";
}
// Generates a binary operation instruction given an op name, two operands and
// a result width.
// Generates a binary operation instruction given an op name, two operands
// and a result width.
void genBinOp(StringRef inst, Operation *binop, Value op1, Value op2,
size_t width) {
// Set the LID for this operation
@ -320,18 +324,48 @@ private:
os << opLID << " " << inst << " " << sid << " " << op0LID << "\n";
}
// Generates a constant declaration given a value, a width and a name
// Generates a constant declaration given a value, a width and a name and
// returns the LID associated to it
void genUnaryOp(Operation *srcop, Value op0, StringRef inst, size_t width) {
genUnaryOp(srcop, op0.getDefiningOp(), inst, width);
}
// Generates a constant declaration given a operand lid, a width and a name
size_t genUnaryOp(size_t op0LID, StringRef inst, size_t width) {
// Register the source operation with the current line id
size_t curLid = lid++;
// Retrieve the lid associated with the sort (sid)
size_t sid = sortToLIDMap.at(width);
os << curLid << " " << inst << " " << sid << " " << op0LID << "\n";
return curLid;
}
// Generates a constant declaration given a value, a width and a name
size_t genUnaryOp(Operation *op0, StringRef inst, size_t width) {
return genUnaryOp(getOpLID(op0), inst, width);
}
// Generates a constant declaration given a value, a width and a name and
// returns the LID associated to it
size_t genUnaryOp(Value op0, StringRef inst, size_t width) {
return genUnaryOp(getOpLID(op0), inst, width);
}
// Generate a btor2 assertion given an assertion operation
// Note that a predicate inversion must have already been generated at this
// point
void genBad(Operation *assertop) {
// Start by finding the expression lid
size_t assertLID = getOpLID(assertop);
genBad(assertLID);
}
// Generate a btor2 assertion given an assertion operation's LID
// Note that a predicate inversion must have already been generated at this
// point
void genBad(size_t assertLID) {
// Build and return the btor2 string
// Also update the lid as this instruction is not associated to an mlir op
os << lid++ << " "
@ -386,26 +420,29 @@ private:
}
// Generate a logical implication given a lhs and a rhs
void genImplies(Operation *srcop, Value lhs, Value rhs) {
size_t genImplies(Operation *srcop, Value lhs, Value rhs) {
// Retrieve LIDs for the lhs and rhs
size_t lhsLID = getOpLID(lhs);
size_t rhsLID = getOpLID(rhs);
genImplies(srcop, lhsLID, rhsLID);
return genImplies(srcop, lhsLID, rhsLID);
}
// Generate a logical implication given a lhs and a rhs
void genImplies(Operation *srcop, size_t lhsLID, size_t rhsLID) {
size_t genImplies(Operation *srcop, size_t lhsLID, size_t rhsLID) {
// Register the source operation with the current line id
size_t opLID = getOpLID(srcop);
return genImplies(opLID, lhsLID, rhsLID);
}
size_t genImplies(size_t opLID, size_t lhsLID, size_t rhsLID) {
// Retrieve the lid associated with the sort (sid)
size_t sid = sortToLIDMap.at(1);
// Build and emit the implies operation
os << opLID << " "
<< "implies"
<< " " << sid << " " << lhsLID << " " << rhsLID << "\n";
return opLID;
}
// Generates a state instruction given a width and a name
@ -422,8 +459,8 @@ private:
<< " " << sid << " " << name << "\n";
}
// Generates a next instruction, given a width, a state LID, and a next value
// LID
// Generates a next instruction, given a width, a state LID, and a next
// value LID
void genNext(Value next, Operation *reg, int64_t width) {
// Retrieve the lid associated with the sort (sid)
size_t sid = sortToLIDMap.at(width);
@ -445,13 +482,13 @@ private:
// Start by figuring out what sort needs to be generated
int64_t width = hw::getBitWidth(type);
// Sanity check: getBitWidth can technically return -1 it is a type with no
// width (like a clock). This shouldn't be allowed as width is required to
// generate a sort
// Sanity check: getBitWidth can technically return -1 it is a type with
// no width (like a clock). This shouldn't be allowed as width is required
// to generate a sort
assert(width != noWidth);
// Generate the sort regardles of resulting width (nothing will be added if
// the sort already exists)
// Generate the sort regardles of resulting width (nothing will be added
// if the sort already exists)
genSort("bitvec", width);
return width;
}
@ -506,7 +543,8 @@ private:
// with next)
size_t resetLID = noLID;
if (BlockArgument barg = dyn_cast<BlockArgument>(reset)) {
// Extract the block argument index and use that to get the line number
// Extract the block argument index and use that to get the line
// number
size_t argIdx = barg.getArgNumber();
// Check that the extracted argument is in range before using it
@ -534,9 +572,12 @@ private:
// i.e. reg <= reset ? 0 : next
genIte(next.getDefiningOp(), resetLID, resetValLID, nextLID, width);
} else {
// Assign a new LID to next and perform a sanity check
setOpLID(next.getDefiningOp());
assert(nextLID != noLID);
// Sanity check: next should have been assigned
if (nextLID == noLID) {
next.getDefiningOp()->emitError(
"Register input does not point to a valid op!");
return;
}
}
// Finally generate the next statement
@ -565,8 +606,8 @@ public:
// Save lid for later
size_t inlid = lid;
// Record the defining operation's line ID (the module itself in the case
// of ports)
// Record the defining operation's line ID (the module itself in the
// case of ports)
inputLIDs[port.argNum] = lid;
// Increment the lid to keep it unique
@ -605,58 +646,36 @@ public:
// Binary operations are all emitted the same way, so we can group them into
// a single method.
void visitBinOp(Operation *op, StringRef inst, int64_t w) {
template <typename Op>
void visitBinOp(Op op, StringRef inst) {
// Generete the sort
int64_t w = requireSort(op.getType());
// Start by extracting the operands
Value op1 = op->getOperand(0);
Value op2 = op->getOperand(1);
Value op1 = op.getOperand(0);
Value op2 = op.getOperand(1);
// Generate the line
genBinOp(inst, op, op1, op2, w);
}
// Visitors for the binary ops
void visitComb(comb::AddOp op) {
visitBinOp(op, "add", requireSort(op.getType()));
}
void visitComb(comb::SubOp op) {
visitBinOp(op, "sub", requireSort(op.getType()));
}
void visitComb(comb::MulOp op) {
visitBinOp(op, "mul", requireSort(op.getType()));
}
void visitComb(comb::DivSOp op) {
visitBinOp(op, "sdiv", requireSort(op.getType()));
}
void visitComb(comb::DivUOp op) {
visitBinOp(op, "udiv", requireSort(op.getType()));
}
void visitComb(comb::ModSOp op) {
visitBinOp(op, "smod", requireSort(op.getType()));
}
void visitComb(comb::ShlOp op) {
visitBinOp(op, "sll", requireSort(op.getType()));
}
void visitComb(comb::ShrUOp op) {
visitBinOp(op, "srl", requireSort(op.getType()));
}
void visitComb(comb::ShrSOp op) {
visitBinOp(op, "sra", requireSort(op.getType()));
}
void visitComb(comb::AndOp op) {
visitBinOp(op, "and", requireSort(op.getType()));
}
void visitComb(comb::OrOp op) {
visitBinOp(op, "or", requireSort(op.getType()));
}
void visitComb(comb::XorOp op) {
visitBinOp(op, "xor", requireSort(op.getType()));
}
void visitComb(comb::ConcatOp op) {
visitBinOp(op, "concat", requireSort(op.getType()));
}
void visitComb(comb::AddOp op) { visitBinOp(op, "add"); }
void visitComb(comb::SubOp op) { visitBinOp(op, "sub"); }
void visitComb(comb::MulOp op) { visitBinOp(op, "mul"); }
void visitComb(comb::DivSOp op) { visitBinOp(op, "sdiv"); }
void visitComb(comb::DivUOp op) { visitBinOp(op, "udiv"); }
void visitComb(comb::ModSOp op) { visitBinOp(op, "smod"); }
void visitComb(comb::ShlOp op) { visitBinOp(op, "sll"); }
void visitComb(comb::ShrUOp op) { visitBinOp(op, "srl"); }
void visitComb(comb::ShrSOp op) { visitBinOp(op, "sra"); }
void visitComb(comb::AndOp op) { visitBinOp(op, "and"); }
void visitComb(comb::OrOp op) { visitBinOp(op, "or"); }
void visitComb(comb::XorOp op) { visitBinOp(op, "xor"); }
void visitComb(comb::ConcatOp op) { visitBinOp(op, "concat"); }
// Extract ops translate to a slice operation in btor2 in a one-to-one manner
// Extract ops translate to a slice operation in btor2 in a one-to-one
// manner
void visitComb(comb::ExtractOp op) {
int64_t w = requireSort(op.getType());
@ -750,7 +769,75 @@ public:
void visitSV(Operation *op) { visitInvalidSV(op); }
// Once SV Ops are visited, we need to check for seq ops
void visitInvalidSV(Operation *op) { visit(op); }
void visitInvalidSV(Operation *op) { dispatchVerifVisitor(op); }
template <typename Op>
void visitAssertLike(Op op) {
// Expression is what we will try to invert for our assertion
Value prop = op.getProperty();
Value en = op.getEnable();
// This sort is for assertion inversion and potential implies
genSort("bitvec", 1);
size_t assertLID = noLID;
// Check for a related enable signal
if (en) {
// Generate the implication
genImplies(op, en, prop);
// Generate the implies inversion
assertLID = genUnaryOp(op, "not", 1);
} else {
// Generate the expression inversion
assertLID = genUnaryOp(prop.getDefiningOp(), "not", 1);
}
// Genrate the bad btor2 intruction
genBad(assertLID);
}
template <typename Op>
void visitAssumeLike(Op op) {
// Expression is what we will try to invert for our assertion
Value prop = op.getProperty();
Value en = op.getEnable();
size_t assumeLID = getOpLID(prop);
// Check for a related enable signal
if (en) {
// This sort is for assertion inversion and potential implies
genSort("bitvec", 1);
// Generate the implication
assumeLID = genImplies(op, en, prop);
}
// Genrate the bad btor2 intruction
genConstraint(assumeLID);
}
// Folds the enable signal into the property and converts the result into a
// bad instruction.
void visitVerif(verif::AssertOp op) { visitAssertLike(op); }
void visitVerif(verif::ClockedAssertOp op) { visitAssertLike(op); }
// Fold the enable into the property and convert the assumption into a
// constraint instruction.
void visitVerif(verif::AssumeOp op) { visitAssumeLike(op); }
void visitVerif(verif::ClockedAssumeOp op) { visitAssumeLike(op); }
// Cover is not supported in btor2
void visitVerif(verif::CoverOp op) {
op->emitError("Cover is not supprted in btor2!");
return signalPassFailure();
}
void visitVerif(verif::ClockedCoverOp op) {
op->emitError("Cover is not supprted in btor2!");
return signalPassFailure();
}
void visitInvalidVerif(Operation *op) { visit(op); }
// Seq operation visitor, that dispatches to other seq ops
// Also handles all remaining operations that should be explicitly ignored
@ -758,7 +845,7 @@ public:
// Typeswitch is used here because other seq types will be supported
// like all operations relating to memories and CompRegs
TypeSwitch<Operation *, void>(op)
.Case<seq::FirRegOp, hw::WireOp>([&](auto expr) { visit(expr); })
.Case<seq::FirRegOp, seq::CompRegOp>([&](auto expr) { visit(expr); })
.Default([&](auto expr) { visitUnsupportedOp(op); });
}
@ -785,8 +872,13 @@ public:
StringRef regName = reg.getName().value();
int64_t w = requireSort(reg.getType());
// Check for initial values which must be emitted before the state in btor2
// Check for initial values which must be emitted before the state in
// btor2
Value pov = reg.getPowerOnValue();
// Generate state instruction (represents the register declaration)
genState(reg, w, regName);
if (pov) {
// Check that the powerOn value is a non-null constant
if (!isa_and_nonnull<hw::ConstantOp>(pov.getDefiningOp()))
@ -798,15 +890,8 @@ public:
// Add it to the list of visited operations
handledOps.insert(pov.getDefiningOp());
// Generate state instruction (represents the register declaration)
genState(reg, w, regName);
// Finally generate the init statement
genInit(reg, pov, w);
} else {
// Only generate the state instruction and nothing else
genState(reg, w, regName);
}
// Record the operation for future `next` instruction generation
@ -860,7 +945,7 @@ void ConvertHWToBTOR2Pass::runOnOperation() {
visit(port);
}
// Previsit all registers in the module in order to avoid dependency cylcles
// Previsit all registers in the module in order to avoid dependency cycles
module.walk([&](Operation *op) {
TypeSwitch<Operation *, void>(op)
.Case<seq::FirRegOp, seq::CompRegOp>([&](auto reg) {
@ -910,7 +995,7 @@ void ConvertHWToBTOR2Pass::runOnOperation() {
// This is triggered if our operand is already in the worklist and
// wasn't handled
if (!worklist.insert({defOp, defOp->operand_begin()}).second) {
op->emitError("dependency cycle");
defOp->emitError("dependency cycle");
return;
}
}

125
lib/Conversion/LTLToCore/LTLToCore.cpp
View File

@ -38,68 +38,11 @@ using namespace mlir;
using namespace circt;
using namespace hw;
static sv::EventControl ltlToSVEventControl(ltl::ClockEdge ce) {
switch (ce) {
case ltl::ClockEdge::Pos:
return sv::EventControl::AtPosEdge;
case ltl::ClockEdge::Neg:
return sv::EventControl::AtNegEdge;
case ltl::ClockEdge::Both:
return sv::EventControl::AtEdge;
}
llvm_unreachable("Unknown event control kind");
}
//===----------------------------------------------------------------------===//
// Conversion patterns
//===----------------------------------------------------------------------===//
namespace {
// Custom pattern matchers
// Matches and records a boolean attribute
struct I1ValueMatcher {
Value *what;
I1ValueMatcher(Value *what) : what(what) {}
bool match(Value op) const {
if (!op.getType().isSignlessInteger(1))
return false;
*what = op;
return true;
}
};
static inline I1ValueMatcher mBool(Value *const val) {
return I1ValueMatcher(val);
}
// Matches and records an arbitrary op
template <typename OpType, typename... OperandMatchers>
struct BindingRecursivePatternMatcher
: mlir::detail::RecursivePatternMatcher<OpType, OperandMatchers...> {
using BaseMatcher =
mlir::detail::RecursivePatternMatcher<OpType, OperandMatchers...>;
BindingRecursivePatternMatcher(OpType *bop, OperandMatchers... matchers)
: BaseMatcher(matchers...), opBind(bop) {}
bool match(Operation *op) {
if (BaseMatcher::match(op)) {
*opBind = llvm::cast<OpType>(op);
return true;
}
return false;
}
OpType *opBind;
};
template <typename OpType, typename... Matchers>
static inline auto mOpWithBind(OpType *op, Matchers... matchers) {
return BindingRecursivePatternMatcher<OpType, Matchers...>(op, matchers...);
}
struct HasBeenResetOpConversion : OpConversionPattern<verif::HasBeenResetOp> {
using OpConversionPattern<verif::HasBeenResetOp>::OpConversionPattern;
@ -147,68 +90,6 @@ struct HasBeenResetOpConversion : OpConversionPattern<verif::HasBeenResetOp> {
}
};
struct AssertOpConversionPattern : OpConversionPattern<verif::AssertOp> {
using OpConversionPattern<verif::AssertOp>::OpConversionPattern;
Value visit(ltl::DisableOp op, ConversionPatternRewriter &rewriter,
Value operand = nullptr) const {
// Replace the ltl::DisableOp with an OR op as it represents a disabling
// implication: (implies (not condition) input) is equivalent to
// (or (not (not condition)) input) which becomes (or condition input)
return rewriter.replaceOpWithNewOp<comb::OrOp>(
op, op.getCondition(), operand ? operand : op.getInput());
}
// Special case : we want to detect the Non-overlapping implication,
// Overlapping Implication or simply AssertProperty patterns and reject
// everything else for now: antecedent : ltl::concatOp || immediate predicate
// consequent : any other non-sequence op
// We want to support a ##n true |-> b and a |-> b
LogicalResult
matchAndRewrite(verif::AssertOp op, OpAdaptor adaptor,
ConversionPatternRewriter &rewriter) const override {
Value ltlClock, disableCond, disableInput, disableVal;
ltl::ClockOp clockOp;
ltl::DisableOp disableOp;
// Look for the Assert Property pattern
bool matchedProperty = matchPattern(
op.getProperty(),
mOpWithBind<ltl::ClockOp>(
&clockOp,
mOpWithBind<ltl::DisableOp>(&disableOp, mBool(&disableInput),
mBool(&disableCond)),
mBool(&ltlClock)));
if (!matchedProperty)
return rewriter.notifyMatchFailure(
op, " verif.assert used outside of an assert property!");
// Then visit the disable op
disableVal = visit(disableOp, rewriter, disableInput);
// Generate the parenting sv.always posedge clock from the ltl
// clock, containing the generated sv.assert
rewriter.create<sv::AlwaysOp>(
clockOp.getLoc(), ltlToSVEventControl(clockOp.getEdge()), ltlClock,
[&] {
// Generate the sv assertion using the input to the
// parenting clock
rewriter.replaceOpWithNewOp<sv::AssertOp>(
op, disableVal,
sv::DeferAssertAttr::get(getContext(),
sv::DeferAssert::Immediate),
op.getLabelAttr());
});
// Erase Converted Ops
rewriter.eraseOp(clockOp);
return success();
}
};
} // namespace
//===----------------------------------------------------------------------===//
@ -234,7 +115,8 @@ void LowerLTLToCorePass::runOnOperation() {
target.addLegalDialect<sv::SVDialect>();
target.addLegalDialect<seq::SeqDialect>();
target.addLegalDialect<ltl::LTLDialect>();
target.addIllegalDialect<verif::VerifDialect>();
target.addLegalDialect<verif::VerifDialect>();
target.addIllegalOp<verif::HasBeenResetOp>();
// Create type converters, mostly just to convert an ltl property to a bool
mlir::TypeConverter converter;
@ -269,8 +151,7 @@ void LowerLTLToCorePass::runOnOperation() {
// Create the operation rewrite patters
RewritePatternSet patterns(&getContext());
patterns.add<AssertOpConversionPattern, HasBeenResetOpConversion>(
converter, patterns.getContext());
patterns.add<HasBeenResetOpConversion>(converter, patterns.getContext());
// Apply the conversions
if (failed(

32
lib/Dialect/FIRRTL/FIRRTLIntrinsics.cpp
View File

@ -18,13 +18,25 @@ using namespace firrtl;
// GenericIntrinsic
//===----------------------------------------------------------------------===//
ParseResult GenericIntrinsic::hasNInputs(unsigned n) {
if (op.getNumOperands() != n)
return emitError() << " has " << op.getNumOperands()
<< " inputs instead of " << n;
// Checks for a number of operands between n and n+c (allows for c optional
// inputs)
ParseResult GenericIntrinsic::hasNInputs(unsigned n, unsigned c = 0U) {
auto numOps = op.getNumOperands();
unsigned m = n + c;
if (!(n <= numOps && numOps <= m)) {
auto err = emitError() << " has " << numOps << " inputs instead of ";
if (c == 0)
err << n;
else
err << " between " << n << " and " << m;
return failure();
}
return success();
}
// Accessor method for the number of inputs
unsigned GenericIntrinsic::getNumInputs() { return op.getNumOperands(); }
ParseResult GenericIntrinsic::hasNOutputElements(unsigned n) {
auto b = getOutputBundle();
if (!b)
@ -447,7 +459,7 @@ public:
using IntrinsicConverter::IntrinsicConverter;
bool check(GenericIntrinsic gi) override {
return gi.hasNInputs(1) || gi.sizedInput<UIntType>(0, 1) ||
return gi.hasNInputs(1, 2) || gi.sizedInput<UIntType>(0, 1) ||
gi.namedParam("label", true) || gi.hasNParam(0, 1) ||
gi.hasNoOutput();
}
@ -455,8 +467,14 @@ public:
void convert(GenericIntrinsic gi, GenericIntrinsicOpAdaptor adaptor,
PatternRewriter &rewriter) override {
auto label = gi.getParamValue<StringAttr>("label");
auto operands = adaptor.getOperands();
rewriter.replaceOpWithNewOp<Op>(gi.op, adaptor.getOperands()[0], label);
// Check if an enable was provided
Value enable;
if (gi.getNumInputs() == 2)
enable = operands[1];
rewriter.replaceOpWithNewOp<Op>(gi.op, operands[0], enable, label);
}
};
@ -708,8 +726,6 @@ void FIRRTLIntrinsicLoweringDialectInterface::populateIntrinsicLowerings(
"circt.ltl.implication", "circt_ltl_implication");
lowering.add<CirctLTLBinaryConverter<LTLUntilIntrinsicOp>>("circt.ltl.until",
"circt_ltl_until");
lowering.add<CirctLTLBinaryConverter<LTLDisableIntrinsicOp>>(
"circt.ltl.disable", "circt_ltl_disable");
lowering.add<CirctLTLUnaryConverter<LTLNotIntrinsicOp>>("circt.ltl.not",
"circt_ltl_not");
lowering.add<CirctLTLUnaryConverter<LTLEventuallyIntrinsicOp>>(

32
lib/Dialect/FIRRTL/Transforms/ExpandWhens.cpp
View File

@ -548,15 +548,21 @@ private:
condition.getLoc(), condition.getType(), condition, value);
}
// Create an implication from the condition to the given value
// This is implemented as (or (not condition) value) to avoid
// the corner case where value is an implication.
Value impliesLTLCondition(Operation *op, Value value) {
OpBuilder builder = OpBuilder(op);
Value notCond = builder.createOrFold<LTLNotIntrinsicOp>(
condition.getLoc(), condition.getType(), condition);
return builder.createOrFold<LTLOrIntrinsicOp>(
condition.getLoc(), condition.getType(), notCond, value);
/// Concurrent and of a property with the current condition. If we are in
/// the outer scope, i.e. not in a WhenOp region, then there is no condition.
Value ltlAndWithCondition(Operation *op, Value value) {
// 'ltl.and' the value with the current condition.
return OpBuilder(op).createOrFold<LTLAndIntrinsicOp>(
condition.getLoc(), condition.getType(), condition, value);
}
/// Overlapping implication with the condition as its antecedent and a given
/// property as the consequent. If we are in the outer scope, i.e. not in a
/// WhenOp region, then there is no condition.
Value ltlImplicationWithCondition(Operation *op, Value value) {
// 'and' the value with the current condition.
return OpBuilder(op).createOrFold<LTLImplicationIntrinsicOp>(
condition.getLoc(), condition.getType(), condition, value);
}
private:
@ -580,15 +586,17 @@ void WhenOpVisitor::visitStmt(StopOp op) {
}
void WhenOpVisitor::visitStmt(VerifAssertIntrinsicOp op) {
op.getPropertyMutable().assign(impliesLTLCondition(op, op.getProperty()));
op.getPropertyMutable().assign(
ltlImplicationWithCondition(op, op.getProperty()));
}
void WhenOpVisitor::visitStmt(VerifAssumeIntrinsicOp op) {
op.getPropertyMutable().assign(impliesLTLCondition(op, op.getProperty()));
op.getPropertyMutable().assign(
ltlImplicationWithCondition(op, op.getProperty()));
}
void WhenOpVisitor::visitStmt(VerifCoverIntrinsicOp op) {
op.getPropertyMutable().assign(impliesLTLCondition(op, op.getProperty()));
op.getPropertyMutable().assign(ltlAndWithCondition(op, op.getProperty()));
}
void WhenOpVisitor::visitStmt(AssertOp op) {

12
lib/Dialect/LTL/LTLFolds.cpp
View File

@ -121,15 +121,3 @@ OpFoldResult GoToRepeatOp::fold(FoldAdaptor adaptor) {
OpFoldResult NonConsecutiveRepeatOp::fold(FoldAdaptor adaptor) {
return RepeatLikeOp::fold(adaptor.getBase(), adaptor.getMore(), getInput());
}
//===----------------------------------------------------------------------===//
// DisableOp
//===----------------------------------------------------------------------===//
OpFoldResult DisableOp::fold(FoldAdaptor adaptor) {
// disable(p, false) -> p
if (isConstantZero(adaptor.getCondition()))
return getInput();
return {};
}

1
lib/Dialect/Verif/Transforms/CMakeLists.txt
View File

@ -1,6 +1,7 @@
add_circt_dialect_library(CIRCTVerifTransforms
PrepareForFormal.cpp
VerifyClockedAssertLike.cpp
PrepareForFormal.cpp
DEPENDS
CIRCTVerifTransformsIncGen

9
lib/Dialect/Verif/Transforms/VerifyClockedAssertLike.cpp
View File

@ -65,7 +65,7 @@ private:
if (operandIt == op->operand_end()) {
// Check that our property doesn't contain any illegal ops
if (isa<ltl::ClockOp, ltl::DisableOp>(op)) {
if (isa<ltl::ClockOp>(op)) {
op->emitError("Nested clock or disable operations are not "
"allowed for clock_assertlike operations.");
return;
@ -86,12 +86,7 @@ private:
if (!defOp || handledOps.contains(defOp))
continue;
// This is triggered if our operand is already in the worklist and
// wasn't handled
if (!worklist.insert({defOp, defOp->operand_begin()}).second) {
op->emitError("dependency cycle");
return;
}
worklist.insert({defOp, defOp->operand_begin()});
}
// Clear worklist and such

49
lib/Dialect/Verif/VerifOps.cpp
View File

@ -23,6 +23,18 @@ using namespace circt;
using namespace verif;
using namespace mlir;
static ClockEdge ltlToVerifClockEdge(ltl::ClockEdge ce) {
switch (ce) {
case ltl::ClockEdge::Pos:
return ClockEdge::Pos;
case ltl::ClockEdge::Neg:
return ClockEdge::Neg;
case ltl::ClockEdge::Both:
return ClockEdge::Both;
}
llvm_unreachable("Unknown event control kind");
}
//===----------------------------------------------------------------------===//
// HasBeenResetOp
//===----------------------------------------------------------------------===//
@ -42,6 +54,43 @@ OpFoldResult HasBeenResetOp::fold(FoldAdaptor adaptor) {
return {};
}
//===----------------------------------------------------------------------===//
// AssertLikeOps Canonicalizations
//===----------------------------------------------------------------------===//
namespace AssertLikeOp {
// assertlike(ltl.clock(prop, clk), en) -> clocked_assertlike(prop, en, clk)
template <typename TargetOp, typename Op>
static LogicalResult canonicalize(Op op, PatternRewriter &rewriter) {
// If the property is a block argument, then no canonicalization is possible
Value property = op.getProperty();
auto clockOp = property.getDefiningOp<ltl::ClockOp>();
if (!clockOp)
return failure();
// Check for clock operand
// If it exists, fold it into a clocked assertlike
rewriter.replaceOpWithNewOp<TargetOp>(
op, clockOp.getInput(), ltlToVerifClockEdge(clockOp.getEdge()),
clockOp.getClock(), op.getEnable(), op.getLabelAttr());
return success();
}
} // namespace AssertLikeOp
LogicalResult AssertOp::canonicalize(AssertOp op, PatternRewriter &rewriter) {
return AssertLikeOp::canonicalize<ClockedAssertOp>(op, rewriter);
}
LogicalResult AssumeOp::canonicalize(AssumeOp op, PatternRewriter &rewriter) {
return AssertLikeOp::canonicalize<ClockedAssumeOp>(op, rewriter);
}
LogicalResult CoverOp::canonicalize(CoverOp op, PatternRewriter &rewriter) {
return AssertLikeOp::canonicalize<ClockedCoverOp>(op, rewriter);
}
//===----------------------------------------------------------------------===//
// LogicalEquivalenceCheckingOp
//===----------------------------------------------------------------------===//

22
test/Conversion/ExportVerilog/prepare-for-emission.mlir
View File

@ -148,26 +148,6 @@ module attributes {circt.loweringOptions = "disallowExpressionInliningInPorts"}
// -----
module attributes {circt.loweringOptions = "disallowExpressionInliningInPorts"} {
// CHECK-LABEL: @DisableIff(
hw.module @DisableIff(in %clk: i1, in %a: i1, in %b: i1) {
%b_xor_b = comb.xor %b, %b : i1
// CHECK: %[[XOR:.+]] = comb.xor
// CHECK: %[[WIRE:.+]] = sv.wire
// CHECK: sv.assign %[[WIRE]], %[[XOR]]
// CHECK: %[[READ:.+]] = sv.read_inout %[[WIRE]]
// CHECK: ltl.disable %{{.+}} if %[[READ]]
%i0 = ltl.implication %a, %b : i1, i1
%k0 = ltl.clock %i0, posedge %clk : !ltl.property
%k5 = ltl.disable %k0 if %b_xor_b : !ltl.property
verif.assert %k5: !ltl.property
}
}
// -----
module attributes {circt.loweringOptions = "disallowExpressionInliningInPorts"} {
// CHECK-LABEL: @ClockExpr(
hw.module @ClockExpr(in %clk: i1, in %a: i1, in %b: i1) {
@ -181,7 +161,7 @@ module attributes {circt.loweringOptions = "disallowExpressionInliningInPorts"}
%i0 = ltl.implication %a, %b : i1, i1
%k0 = ltl.clock %i0, posedge %clk_xor_b : !ltl.property
verif.assert %k0: !ltl.property
verif.assert %k0 : !ltl.property
}
}

55
test/Conversion/ExportVerilog/verif.mlir
View File

@ -195,21 +195,17 @@ hw.module @Properties(in %clk: i1, in %a: i1, in %b: i1) {
// CHECK: assert property (@(posedge clk) a |-> b);
// CHECK: assert property (@(posedge clk) a ##1 b |-> (@(negedge b) not a));
// CHECK: assert property (disable iff (b) not a);
// CHECK: assert property (disable iff (b) @(posedge clk) a |-> b);
// CHECK: assert property (@(posedge clk) disable iff (b) not a);
// CHECK: assert property (disable iff (~(b)) not a);
// CHECK: assert property (disable iff (~(b)) @(posedge clk) not a);
%k0 = ltl.clock %i0, posedge %clk : !ltl.property
%k1 = ltl.clock %n0, negedge %b : !ltl.property
%k2 = ltl.implication %i2, %k1 : !ltl.sequence, !ltl.property
%k3 = ltl.clock %k2, posedge %clk : !ltl.property
%k4 = ltl.disable %n0 if %b : !ltl.property
%k5 = ltl.disable %k0 if %b : !ltl.property
%k6 = ltl.clock %k4, posedge %clk : !ltl.property
%k6 = ltl.clock %n0, posedge %clk : !ltl.property
verif.assert %k0 : !ltl.property
verif.assert %k3 : !ltl.property
verif.assert %k4 : !ltl.property
verif.assert %k5 : !ltl.property
verif.assert %k6 : !ltl.property
verif.assert %n0 if %b : !ltl.property
verif.assert %k6 if %b : !ltl.property
}
// CHECK-LABEL: module Precedence
@ -267,12 +263,11 @@ hw.module @SystemVerilogSpecExamples(in %clk: i1, in %a: i1, in %b: i1, in %c: i
%b3 = ltl.clock %b2, posedge %clk : !ltl.property
verif.assert %b3 : !ltl.property
// CHECK: assert property (@(posedge clk) disable iff (e) a |-> not b ##1 c ##1 d);
// CHECK: assert property (disable iff (~(e)) @(posedge clk) a |-> not b ##1 c ##1 d);
%c0 = ltl.not %b1 : !ltl.sequence
%c1 = ltl.implication %a, %c0 : i1, !ltl.property
%c2 = ltl.disable %c1 if %e : !ltl.property
%c3 = ltl.clock %c2, posedge %clk : !ltl.property
verif.assert %c3 : !ltl.property
%c3 = ltl.clock %c1, posedge %clk : !ltl.property
verif.assert %c3 if %e : !ltl.property
// CHECK: assert property (##1 a |-> b);
%d0 = ltl.delay %a, 1, 0 : i1
@ -285,27 +280,25 @@ hw.module @LivenessExample(in %clock: i1, in %reset: i1, in %isLive: i1) {
%true = hw.constant true
// CHECK: wire _GEN = ~isLive;
// CHECK: assert property (@(posedge clock) disable iff (reset) $fell(reset) & _GEN |-> (s_eventually isLive));
// CHECK: assume property (@(posedge clock) disable iff (reset) $fell(reset) & _GEN |-> (s_eventually isLive));
// CHECK: assert property (disable iff (~(reset)) @(posedge clock) $fell(reset) & _GEN |-> (s_eventually isLive));
// CHECK: assume property (disable iff (~(reset)) @(posedge clock) $fell(reset) & _GEN |-> (s_eventually isLive));
%not_isLive = comb.xor %isLive, %true : i1
%fell_reset = sv.verbatim.expr "$fell({{0}})"(%reset) : (i1) -> i1
%0 = comb.and %fell_reset, %not_isLive : i1
%1 = ltl.eventually %isLive : i1
%2 = ltl.implication %0, %1 : i1, !ltl.property
%3 = ltl.disable %2 if %reset : !ltl.property
%liveness_after_reset = ltl.clock %3, posedge %clock : !ltl.property
verif.assert %liveness_after_reset : !ltl.property
verif.assume %liveness_after_reset : !ltl.property
%liveness_after_reset = ltl.clock %2, posedge %clock : !ltl.property
verif.assert %liveness_after_reset if %reset : !ltl.property
verif.assume %liveness_after_reset if %reset : !ltl.property
// CHECK: assert property (@(posedge clock) disable iff (reset) isLive ##1 _GEN |-> (s_eventually isLive));
// CHECK: assume property (@(posedge clock) disable iff (reset) isLive ##1 _GEN |-> (s_eventually isLive));
// CHECK: assert property (disable iff (~(reset)) @(posedge clock) isLive ##1 _GEN |-> (s_eventually isLive));
// CHECK: assume property (disable iff (~(reset)) @(posedge clock) isLive ##1 _GEN |-> (s_eventually isLive));
%4 = ltl.delay %not_isLive, 1, 0 : i1
%5 = ltl.concat %isLive, %4 : i1, !ltl.sequence
%6 = ltl.implication %5, %1 : !ltl.sequence, !ltl.property
%7 = ltl.disable %6 if %reset : !ltl.property
%liveness_after_fall = ltl.clock %7, posedge %clock : !ltl.property
verif.assert %liveness_after_fall : !ltl.property
verif.assume %liveness_after_fall : !ltl.property
%liveness_after_fall = ltl.clock %6, posedge %clock : !ltl.property
verif.assert %liveness_after_fall if %reset : !ltl.property
verif.assume %liveness_after_fall if %reset : !ltl.property
}
// https://github.com/llvm/circt/issues/5763
@ -325,12 +318,12 @@ hw.module @ClockedAsserts(in %clk: i1, in %a: i1, in %b: i1) {
%true = hw.constant true
%n0 = ltl.not %a : i1
// CHECK: assert property (@(posedge clk) disable iff (b) not a);
verif.clocked_assert %n0 disable %b clock posedge %clk : !ltl.property
// CHECK: assert property (@(posedge clk) disable iff (~(b)) not a);
verif.clocked_assert %n0 if %b, posedge %clk : !ltl.property
// CHECK: assume property (@(posedge clk) disable iff (b) not a);
verif.clocked_assume %n0 disable %b clock posedge %clk : !ltl.property
// CHECK: assume property (@(posedge clk) disable iff (~(b)) not a);
verif.clocked_assume %n0 if %b, posedge %clk : !ltl.property
// CHECK: cover property (@(posedge clk) disable iff (b) not a);
verif.clocked_cover %n0 disable %b clock posedge %clk : !ltl.property
// CHECK: cover property (@(posedge clk) disable iff (~(b)) not a);
verif.clocked_cover %n0 if %b, posedge %clk : !ltl.property
}

3
test/Conversion/FIRRTLToHW/intrinsics.mlir
View File

@ -107,9 +107,6 @@ firrtl.circuit "Intrinsics" {
// CHECK-NEXT: [[K0:%.+]] = ltl.clock [[I0]], posedge [[CLK]] : !ltl.property
%k0 = firrtl.int.ltl.clock %i0, %clk : (!firrtl.uint<1>, !firrtl.clock) -> !firrtl.uint<1>
// CHECK-NEXT: [[D2:%.+]] = ltl.disable [[K0]] if %b : !ltl.property
%d2 = firrtl.int.ltl.disable %k0, %b : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1>
// CHECK-NEXT: verif.assert %a : i1
firrtl.int.verif.assert %a : !firrtl.uint<1>
// CHECK-NEXT: verif.assert %a label "hello" : i1

5
test/Conversion/HWToBTOR2/init.mlir
View File

@ -4,11 +4,12 @@ module {
//CHECK: [[NID0:[0-9]+]] sort bitvec 1
//CHECK: [[NID1:[0-9]+]] input [[NID0]] reset
hw.module @test(in %clock : !seq.clock, in %reset : i1) {
// Register states get pregenerated
//CHECK: [[NID2:[0-9]+]] state [[NID0]] reg
%0 = seq.from_clock %clock
//CHECK: [[NID3:[0-9]+]] constd [[NID0]] 0
%false = hw.constant false
//CHECK: [[NID2:[0-9]+]] state [[NID0]] reg
//CHECK: [[NID9:[0-9]+]] init [[NID0]] [[NID2]] [[NID3]]
//CHECK: [[INIT:[0-9]+]] init [[NID0]] [[NID2]] [[NID3]]
%reg = seq.compreg %false, %clock reset %reset, %false powerOn %false : i1
//CHECK: [[NID4:[0-9]+]] eq [[NID0]] [[NID2]] [[NID3]]

36
test/Conversion/LTLToCore/assertproperty.mlir
View File

@ -2,35 +2,21 @@
// Tests that an Assert Property high level statement can be converted correctly
module {
//CHECK: hw.module @test(in %clock : !seq.clock, in %reset : i1, in %0 "" : i1)
hw.module @test(in %clock : !seq.clock, in %reset : i1, in %8 : i1) {
//CHECK: %1 = seq.from_clock %clock
//CHECK: hw.module @test(in %clock : !seq.clock, in %reset : i1, in %a : i1)
hw.module @test(in %clock : !seq.clock, in %reset : i1, in %a : i1) {
//CHECK: [[CLK:%.+]] = seq.from_clock %clock
%0 = seq.from_clock %clock
//CHECK: %true = hw.constant true
%true = hw.constant true
//CHECK: %false = hw.constant false
//CHECK: %true_0 = hw.constant true
//CHECK: %2 = comb.or %reset, %hbr : i1
//CHECK: %hbr = seq.compreg %2, %clock powerOn %false : i1
%9 = verif.has_been_reset %0, sync %reset
//CHECK: %true = hw.constant true
//CHECK: [[TMP:%.+]] = comb.or %reset, %hbr : i1
//CHECK: %hbr = seq.compreg [[TMP]], %clock powerOn %false : i1
%1 = verif.has_been_reset %0, sync %reset
//CHECK: %3 = comb.xor %reset, %true_0 : i1
//CHECK: %4 = comb.and %hbr, %3 : i1
//CHECK: %5 = comb.xor bin %4, %true : i1
%10 = comb.xor bin %9, %true : i1
//CHECK: %6 = hw.wire %5 : i1
%12 = hw.wire %10 : i1
//CHECK: %7 = comb.or %6, %0 : i1
%13 = ltl.disable %8 if %12 : i1
//CHECK: sv.always posedge %1 {
//CHECK: sv.assert %7, immediate
//CHECK: }
%14 = ltl.clock %13, posedge %0 : !ltl.property
verif.assert %14 : !ltl.property
//CHECK: [[TMP1:%.+]] = comb.xor %reset, %true : i1
//CHECK: [[TMP2:%.+]] = comb.and %hbr, [[TMP1]] : i1
//CHECK: verif.clocked_assert %a if [[TMP2]], posedge [[CLK]] : i1
verif.clocked_assert %a if %1, posedge %0 : i1
//CHECK: hw.output
hw.output

89
test/Dialect/FIRRTL/expand-whens.mlir
View File

@ -637,38 +637,69 @@ firrtl.module @ModuleWithObjectWire(in %in: !firrtl.class<@ClassWithInput(in in:
}
// Test all verif assert/assume/cover constructs
// CHECK: firrtl.module @verif(in %clock: !firrtl.clock, in %cond: !firrtl.uint<1>, in %prop: !firrtl.uint<1>, in %enable: !firrtl.uint<1>, in %reset: !firrtl.uint<1>) {
firrtl.module @verif(
in %clock : !firrtl.clock, in %cond : !firrtl.uint<1>, in %prop : !firrtl.uint<1>,
in %enable : !firrtl.uint<1>, in %reset : !firrtl.uint<1>
// CHECK-LABEL: firrtl.module @verifassert
firrtl.module @verifassert(
in %clock : !firrtl.clock, in %cond : !firrtl.uint<1>, in %prop : !firrtl.uint<1>, in %prop1 : !firrtl.uint<1>,
in %enable : !firrtl.uint<1>, in %enable1 : !firrtl.uint<1>, in %reset : !firrtl.uint<1>
) {
firrtl.when %cond : !firrtl.uint<1> {
// CHECK: [[TMP0:%.+]] = firrtl.int.ltl.not %cond : (!firrtl.uint<1>) -> !firrtl.uint<1>
// CHECK: [[TMP1:%.+]] = firrtl.int.ltl.or [[TMP0]], %prop : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1>
// CHECK: firrtl.int.verif.assert [[TMP1]] : !firrtl.uint<1>
firrtl.int.verif.assert %prop : !firrtl.uint<1>
// CHECK: %2 = firrtl.int.ltl.not %cond : (!firrtl.uint<1>) -> !firrtl.uint<1>
// CHECK: %3 = firrtl.int.ltl.or %2, %prop : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1>
// CHECK: firrtl.int.verif.assume %3 : !firrtl.uint<1>
firrtl.int.verif.assume %prop : !firrtl.uint<1>
// CHECK: %4 = firrtl.int.ltl.not %cond : (!firrtl.uint<1>) -> !firrtl.uint<1>
// CHECK: %5 = firrtl.int.ltl.or %4, %prop : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1>
// CHECK: firrtl.int.verif.cover %5 : !firrtl.uint<1>
firrtl.int.verif.cover %prop : !firrtl.uint<1>
// CHECK: [[TMP2A:%.+]] = firrtl.int.ltl.clock %prop, %clock : (!firrtl.uint<1>, !firrtl.clock) -> !firrtl.uint<1>
// CHECK: [[TMP0A:%.+]] = firrtl.int.ltl.implication %cond, [[TMP2A]] : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1>
// CHECK: firrtl.int.verif.assert [[TMP0A]], %enable : !firrtl.uint<1>, !firrtl.uint<1>
%clk_prop = firrtl.int.ltl.clock %prop, %clock : (!firrtl.uint<1>, !firrtl.clock) -> !firrtl.uint<1>
firrtl.int.verif.assert %clk_prop, %enable : !firrtl.uint<1>, !firrtl.uint<1>
} else {
// CHECK: %6 = firrtl.not %cond : (!firrtl.uint<1>) -> !firrtl.uint<1>
// CHECK: %7 = firrtl.int.ltl.not %6 : (!firrtl.uint<1>) -> !firrtl.uint<1>
// CHECK: %8 = firrtl.int.ltl.or %7, %prop : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1>
// CHECK: firrtl.int.verif.assert %8 : !firrtl.uint<1>
firrtl.int.verif.assert %prop : !firrtl.uint<1>
// CHECK: %9 = firrtl.int.ltl.not %6 : (!firrtl.uint<1>) -> !firrtl.uint<1>
// CHECK: %10 = firrtl.int.ltl.or %9, %prop : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1>
// CHECK: firrtl.int.verif.assume %10 : !firrtl.uint<1>
firrtl.int.verif.assume %prop : !firrtl.uint<1>
// CHECK: %11 = firrtl.int.ltl.not %6 : (!firrtl.uint<1>) -> !firrtl.uint<1>
// CHECK: %12 = firrtl.int.ltl.or %11, %prop : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1>
// CHECK: firrtl.int.verif.cover %12 : !firrtl.uint<1>
firrtl.int.verif.cover %prop : !firrtl.uint<1>
// CHECK: [[TMP3A:%.+]] = firrtl.not %cond : (!firrtl.uint<1>) -> !firrtl.uint<1>
// CHECK: [[TMP6A:%.+]] = firrtl.int.ltl.clock %prop1, %clock : (!firrtl.uint<1>, !firrtl.clock) -> !firrtl.uint<1>
// CHECK: [[TMP4A:%.+]] = firrtl.int.ltl.implication [[TMP3A]], [[TMP6A]] : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1>
// CHECK: firrtl.int.verif.assert [[TMP4A]], %enable1 : !firrtl.uint<1>, !firrtl.uint<1>
%clk_prop = firrtl.int.ltl.clock %prop1, %clock : (!firrtl.uint<1>, !firrtl.clock) -> !firrtl.uint<1>
firrtl.int.verif.assert %clk_prop, %enable1 : !firrtl.uint<1>, !firrtl.uint<1>
}
}
// CHECK-LABEL: firrtl.module @verifassume
firrtl.module @verifassume(
in %clock : !firrtl.clock, in %cond : !firrtl.uint<1>, in %prop : !firrtl.uint<1>, in %prop1 : !firrtl.uint<1>,
in %enable : !firrtl.uint<1>, in %enable1 : !firrtl.uint<1>, in %reset : !firrtl.uint<1>
) {
firrtl.when %cond : !firrtl.uint<1> {
// CHECK: [[TMP2A:%.+]] = firrtl.int.ltl.clock %prop, %clock : (!firrtl.uint<1>, !firrtl.clock) -> !firrtl.uint<1>
// CHECK: [[TMP0A:%.+]] = firrtl.int.ltl.implication %cond, [[TMP2A]] : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1>
// CHECK: firrtl.int.verif.assume [[TMP0A]], %enable : !firrtl.uint<1>, !firrtl.uint<1>
%clk_prop = firrtl.int.ltl.clock %prop, %clock : (!firrtl.uint<1>, !firrtl.clock) -> !firrtl.uint<1>
firrtl.int.verif.assume %clk_prop, %enable : !firrtl.uint<1>, !firrtl.uint<1>
} else {
// CHECK: [[TMP3A:%.+]] = firrtl.not %cond : (!firrtl.uint<1>) -> !firrtl.uint<1>
// CHECK: [[TMP6A:%.+]] = firrtl.int.ltl.clock %prop1, %clock : (!firrtl.uint<1>, !firrtl.clock) -> !firrtl.uint<1>
// CHECK: [[TMP4A:%.+]] = firrtl.int.ltl.implication [[TMP3A]], [[TMP6A]] : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1>
// CHECK: firrtl.int.verif.assume [[TMP4A]], %enable1 : !firrtl.uint<1>, !firrtl.uint<1>
%clk_prop = firrtl.int.ltl.clock %prop1, %clock : (!firrtl.uint<1>, !firrtl.clock) -> !firrtl.uint<1>
firrtl.int.verif.assume %clk_prop, %enable1 : !firrtl.uint<1>, !firrtl.uint<1>
}
}
// CHECK-LABEL: firrtl.module @verifcover
firrtl.module @verifcover(
in %clock : !firrtl.clock, in %cond : !firrtl.uint<1>, in %prop : !firrtl.uint<1>, in %prop1 : !firrtl.uint<1>,
in %enable : !firrtl.uint<1>, in %enable1 : !firrtl.uint<1>, in %reset : !firrtl.uint<1>
) {
firrtl.when %cond : !firrtl.uint<1> {
// CHECK: [[TMP2A:%.+]] = firrtl.int.ltl.clock %prop, %clock : (!firrtl.uint<1>, !firrtl.clock) -> !firrtl.uint<1>
// CHECK: [[TMP0A:%.+]] = firrtl.int.ltl.and %cond, [[TMP2A]] : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1>
// CHECK: firrtl.int.verif.cover [[TMP0A]], %enable : !firrtl.uint<1>, !firrtl.uint<1>
%clk_prop = firrtl.int.ltl.clock %prop, %clock : (!firrtl.uint<1>, !firrtl.clock) -> !firrtl.uint<1>
firrtl.int.verif.cover %clk_prop, %enable : !firrtl.uint<1>, !firrtl.uint<1>
} else {
// CHECK: [[TMP3A:%.+]] = firrtl.not %cond : (!firrtl.uint<1>) -> !firrtl.uint<1>
// CHECK: [[TMP6A:%.+]] = firrtl.int.ltl.clock %prop1, %clock : (!firrtl.uint<1>, !firrtl.clock) -> !firrtl.uint<1>
// CHECK: [[TMP4A:%.+]] = firrtl.int.ltl.and [[TMP3A]], [[TMP6A]] : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1>
// CHECK: firrtl.int.verif.cover [[TMP4A]], %enable1 : !firrtl.uint<1>, !firrtl.uint<1>
%clk_prop = firrtl.int.ltl.clock %prop1, %clock : (!firrtl.uint<1>, !firrtl.clock) -> !firrtl.uint<1>
firrtl.int.verif.cover %clk_prop, %enable1 : !firrtl.uint<1>, !firrtl.uint<1>
}
}

2
test/Dialect/FIRRTL/lower-intrinsics.mlir
View File

@ -79,8 +79,6 @@ firrtl.circuit "Foo" {
// CHECK-NEXT: firrtl.int.ltl.clock %in0, %clk :
firrtl.int.generic "circt_ltl_clock" %in0, %clk : (!firrtl.uint<1>, !firrtl.clock) -> !firrtl.uint<1>
// CHECK-NEXT: firrtl.int.ltl.disable %in0, %in1 :
firrtl.int.generic "circt_ltl_disable" %in0, %in1: (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1>
}
// CHECK-LABEL: firrtl.module @Verif(

2
test/Dialect/LTL/basic.mlir
View File

@ -114,5 +114,3 @@ unrealized_conversion_cast %clk0 : !ltl.sequence to index
unrealized_conversion_cast %clk1 : !ltl.sequence to index
unrealized_conversion_cast %clk2 : !ltl.property to index
// CHECK: ltl.disable {{%.+}} if {{%.+}} : !ltl.property
ltl.disable %p if %true : !ltl.property

10
test/Dialect/LTL/canonicalization.mlir
View File

@ -128,13 +128,3 @@ func.func @NonConsecutiveRepeatFolds(%arg0: !ltl.sequence) {
return
}
// CHECK-LABEL: @ClockingFolds
func.func @ClockingFolds(%arg0: !ltl.property) {
// disable(p, false) -> p
// CHECK-NEXT: call @Prop(%arg0)
%false = hw.constant false
%0 = ltl.disable %arg0 if %false : !ltl.property
call @Prop(%0) : (!ltl.property) -> ()
return
}

21
test/Dialect/Verif/canonicalization.mlir
View File

@ -35,3 +35,24 @@ hw.module @HasBeenReset(in %clock: i1, in %reset: i1) {
%constClockS0 = hw.wire %c2 sym @constClockS0 : i1
%constClockS1 = hw.wire %c3 sym @constClockS1 : i1
}
// CHECK-LABEL: @clockedAssert
hw.module @clockedAssert(in %clock : i1, in %a : i1, in %en : i1) {
// CHECK: verif.clocked_assert %a if %en, posedge %clock : i1
%clk = ltl.clock %a, posedge %clock : i1
verif.assert %clk if %en : !ltl.sequence
}
// CHECK-LABEL: @clockedAssume
hw.module @clockedAssume(in %clock : i1, in %a : i1, in %en : i1) {
// CHECK: verif.clocked_assume %a if %en, posedge %clock : i1
%clk = ltl.clock %a, posedge %clock : i1
verif.assume %clk if %en : !ltl.sequence
}
// CHECK-LABEL: @clockedCover
hw.module @clockedCover(in %clock : i1, in %a : i1, in %en : i1) {
// CHECK: verif.clocked_cover %a if %en, posedge %clock : i1
%clk = ltl.clock %a, posedge %clock : i1
verif.cover %clk if %en : !ltl.sequence
}

38
test/Dialect/Verif/verify.mlir
View File

@ -1,33 +1,5 @@
// RUN: circt-opt --verify-clocked-assert-like %s --split-input-file --verify-diagnostics | circt-opt
hw.module @verifyDisables(in %clk: i1, in %a: i1, in %b: i1) {
%n0 = ltl.not %a : i1
// expected-error @below {{Nested clock or disable operations are not allowed for clock_assertlike operations.}}
%disabled0 = ltl.disable %n0 if %b : !ltl.property
verif.clocked_assert %disabled0 disable %b clock posedge %clk : !ltl.property
}
// -----
hw.module @verifyDisables1(in %clk: i1, in %a: i1, in %b: i1) {
%n0 = ltl.not %a : i1
// expected-error @below {{Nested clock or disable operations are not allowed for clock_assertlike operations.}}
%disabled1 = ltl.disable %n0 if %b : !ltl.property
verif.clocked_assume %disabled1 disable %b clock posedge %clk : !ltl.property
}
// -----
hw.module @verifyDisables2(in %clk: i1, in %a: i1, in %b: i1) {
%n0 = ltl.not %a : i1
// expected-error @below {{Nested clock or disable operations are not allowed for clock_assertlike operations.}}
%disabled2 = ltl.disable %n0 if %b : !ltl.property
verif.clocked_cover %disabled2 disable %b clock posedge %clk : !ltl.property
}
// -----
hw.module @verifyClocks(in %clk: i1, in %a: i1, in %b: i1) {
@ -35,7 +7,7 @@ hw.module @verifyClocks(in %clk: i1, in %a: i1, in %b: i1) {
// expected-error @below {{Nested clock or disable operations are not allowed for clock_assertlike operations.}}
%clocked = ltl.clock %n0, posedge %clk : !ltl.property
verif.clocked_assert %clocked disable %b clock posedge %clk : !ltl.property
verif.clocked_assert %clocked if %b, posedge %clk : !ltl.property
}
// -----
@ -45,7 +17,7 @@ hw.module @verifyClocks1(in %clk: i1, in %a: i1, in %b: i1) {
// expected-error @below {{Nested clock or disable operations are not allowed for clock_assertlike operations.}}
%clocked = ltl.clock %n0, posedge %clk : !ltl.property
verif.clocked_assume %clocked disable %b clock posedge %clk : !ltl.property
verif.clocked_assume %clocked if %b, posedge %clk : !ltl.property
}
// -----
@ -55,7 +27,7 @@ hw.module @verifyClocks2(in %clk: i1, in %a: i1, in %b: i1) {
// expected-error @below {{Nested clock or disable operations are not allowed for clock_assertlike operations.}}
%clocked = ltl.clock %n0, posedge %clk : !ltl.property
verif.clocked_cover %clocked disable %b clock posedge %clk : !ltl.property
verif.clocked_cover %clocked if %b, posedge %clk : !ltl.property
}
// -----
@ -70,5 +42,5 @@ hw.module @deeplynested(in %clk: i1, in %a: i1, in %b: i1) {
%a1 = ltl.and %b, %i1 : i1, !ltl.property
%o1 = ltl.or %b, %a1 : i1, !ltl.property
verif.clocked_assert %o1 disable %b clock posedge %clk : !ltl.property
}
verif.clocked_assert %o1 if %b, posedge %clk : !ltl.property
}

44
test/firtool/btor2-assertproperty.fir
View File

@ -17,35 +17,31 @@ circuit Counter :
connect count, _count_T_1
node _T_2 = neq(count, UInt<4>(0ha))
node hbr = intrinsic(circt_has_been_reset : UInt<1>, clock, reset)
node disable = eq(hbr, UInt<1>(0h0))
node ltl_disable = intrinsic(circt_ltl_disable : UInt<1>, _T_2, disable)
node ltl_clock = intrinsic(circt_ltl_clock : UInt<1>, ltl_disable, clock)
intrinsic(circt_verif_assert, ltl_clock)
node ltl_clock = intrinsic(circt_ltl_clock : UInt<1>, _T_2, clock)
intrinsic(circt_verif_assert, ltl_clock, hbr)
; CHECK: 1 sort bitvec 1
; CHECK: 2 input 1 reset
; CHECK: 3 sort bitvec 32
; CHECK: 4 state 3 count
; CHECK: 5 constd 1 0
; CHECK: 6 state 1 hbr
; CHECK: 7 init 1 6 5
; CHECK: 5 state 1 hbr
; CHECK: 6 constd 1 0
; CHECK: 7 init 1 5 6
; CHECK: 8 constd 3 1
; CHECK: 9 constd 3 10
; CHECK: 10 constd 3 22
; CHECK: 11 constd 1 -1
; CHECK: 12 constd 3 0
; CHECK: 13 eq 1 4 10
; CHECK: 14 add 3 4 8
; CHECK: 15 ite 3 13 12 14
; CHECK: 16 neq 1 4 9
; CHECK: 17 constd 1 -1
; CHECK: 18 or 1 2 6
; CHECK: 19 xor 1 2 17
; CHECK: 20 and 1 6 19
; CHECK: 21 xor 1 20 11
; CHECK: 22 or 1 21 16
; CHECK: 23 not 1 22
; CHECK: 24 bad 23
; CHECK: 25 ite 3 2 12 15
; CHECK: 26 next 3 4 25
; CHECK: 28 next 1 6 27
; CHECK: 11 constd 3 0
; CHECK: 12 eq 1 4 10
; CHECK: 13 add 3 4 8
; CHECK: 14 ite 3 12 11 13
; CHECK: 15 neq 1 4 9
; CHECK: 16 constd 1 -1
; CHECK: 17 or 1 2 5
; CHECK: 18 xor 1 2 16
; CHECK: 19 and 1 5 18
; CHECK: 20 implies 1 19 15
; CHECK: 21 not 1 20
; CHECK: 22 bad 21
; CHECK: 23 ite 3 2 11 14
; CHECK: 24 next 3 4 23
; CHECK: 25 next 1 5 17

9
test/firtool/extract-test-code.fir
View File

@ -44,13 +44,14 @@ circuit Top:
; CHECK: module Top_assert(
; CHECK-NOT: endmodule
; CHECK: foo: assert property (cond);
; CHECK: foo: assert property (disable iff (~(en)) cond);
; CHECK: endmodule
public module Top:
input clock : Clock
input cond : UInt<1>
output out : UInt<1>
input cond : UInt<1>
input en : UInt<1>
output out : UInt<1>
inst instance_extracted of InstanceExtracted
connect instance_extracted.clock, clock
@ -61,4 +62,4 @@ circuit Top:
connect input_only.clock, clock
connect input_only.cond, cond
intrinsic(circt_verif_assert<label="foo">, cond)
intrinsic(circt_verif_assert<label="foo">, cond, en)