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

[LTL] Add ops that allow for most of SVA to be modeled with LTL (#7065) 

* Introduced new ltl ops

* added ops to visitor

* updated exportverilog

* added type inference for intersect

* updated tests

* added fold for trivial case

* Added FIRRTL intrinsics and test

* comments

* updated op requirements
This commit is contained in:
Amelia Dobis 2024-05-23 14:39:21 -07:00 committed by GitHub
parent efa6955a7d
commit ba67aa42b9
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
14 changed files with 369 additions and 73 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -1418,6 +1418,7 @@ class BinaryLTLIntrinsicOp<string mnemonic, list<Trait> traits = []> :
// Generic
def LTLAndIntrinsicOp : BinaryLTLIntrinsicOp<"and", [Commutative]>;
def LTLOrIntrinsicOp : BinaryLTLIntrinsicOp<"or", [Commutative]>;
def LTLIntersectIntrinsicOp : BinaryLTLIntrinsicOp<"intersect", [Commutative]>;
// Sequences
def LTLDelayIntrinsicOp : LTLIntrinsicOp<"delay"> {
@ -1440,6 +1441,26 @@ def LTLRepeatIntrinsicOp : LTLIntrinsicOp<"repeat"> {
}];
}
def LTLGoToRepeatIntrinsicOp : LTLIntrinsicOp<"goto_repeat"> {
let arguments = (ins UInt1Type:$input,
I64Attr:$base,
I64Attr:$more);
let assemblyFormat = [{
$input `,` $base `,` $more attr-dict `:`
functional-type(operands, results)
}];
}
def LTLNonConsecutiveRepeatIntrinsicOp : LTLIntrinsicOp<"non_consecutive_repeat"> {
let arguments = (ins UInt1Type:$input,
I64Attr:$base,
I64Attr:$more);
let assemblyFormat = [{
$input `,` $base `,` $more attr-dict `:`
functional-type(operands, results)
}];
}
// Properties
def LTLNotIntrinsicOp : UnaryLTLIntrinsicOp<"not">;
def LTLImplicationIntrinsicOp : BinaryLTLIntrinsicOp<"implication">;

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

@ -50,8 +50,10 @@ public:
IsXIntrinsicOp, PlusArgsValueIntrinsicOp, PlusArgsTestIntrinsicOp,
SizeOfIntrinsicOp, ClockGateIntrinsicOp, ClockInverterIntrinsicOp,
ClockDividerIntrinsicOp, LTLAndIntrinsicOp, LTLOrIntrinsicOp,
LTLDelayIntrinsicOp, LTLConcatIntrinsicOp, LTLRepeatIntrinsicOp,
LTLNotIntrinsicOp, LTLImplicationIntrinsicOp, LTLUntilIntrinsicOp,
LTLIntersectIntrinsicOp, LTLDelayIntrinsicOp, LTLConcatIntrinsicOp,
LTLRepeatIntrinsicOp, LTLGoToRepeatIntrinsicOp,
LTLNonConsecutiveRepeatIntrinsicOp, LTLNotIntrinsicOp,
LTLImplicationIntrinsicOp, LTLUntilIntrinsicOp,
LTLEventuallyIntrinsicOp, LTLClockIntrinsicOp,
LTLDisableIntrinsicOp, Mux2CellIntrinsicOp, Mux4CellIntrinsicOp,
HasBeenResetIntrinsicOp,
@ -170,9 +172,12 @@ public:
HANDLE(ClockDividerIntrinsicOp, Unhandled);
HANDLE(LTLAndIntrinsicOp, Unhandled);
HANDLE(LTLOrIntrinsicOp, Unhandled);
HANDLE(LTLIntersectIntrinsicOp, Unhandled);
HANDLE(LTLDelayIntrinsicOp, Unhandled);
HANDLE(LTLConcatIntrinsicOp, Unhandled);
HANDLE(LTLRepeatIntrinsicOp, Unhandled);
HANDLE(LTLGoToRepeatIntrinsicOp, Unhandled);
HANDLE(LTLNonConsecutiveRepeatIntrinsicOp, Unhandled);
HANDLE(LTLNotIntrinsicOp, Unhandled);
HANDLE(LTLImplicationIntrinsicOp, Unhandled);
HANDLE(LTLUntilIntrinsicOp, Unhandled);

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

@ -49,6 +49,15 @@ def OrOp : AssocLTLOp<"or"> {
}];
}
def IntersectOp : AssocLTLOp<"intersect"> {
let summary = "The intersection of booleans sequences or properties.";
let description = [{
The intersection of two properties. This checks that both properties both hold
and have the same start and end times. This differs from `ltl.and` which doesn't
consider the timings of each operand, only their results.
}];
}
//===----------------------------------------------------------------------===//
// Sequences
//===----------------------------------------------------------------------===//
@ -151,7 +160,10 @@ def ConcatOp : LTLOp<"concat", [Pure]> {
}];
}
def RepeatOp : LTLOp<"repeat", [Pure]> {
def RepeatOp : LTLOp<"repeat", [
Pure,
PredOpTrait<"'base' must be >= 0", CPred<"$base >= 0">>
]> {
let arguments = (ins
LTLAnySequenceType:$input,
I64Attr:$base,
@ -176,6 +188,60 @@ def RepeatOp : LTLOp<"repeat", [Pure]> {
}];
}
def GoToRepeatOp : LTLOp<"goto_repeat", [
Pure,
PredOpTrait<"'base' must be >= 0", CPred<"$base >= 0">>,
PredOpTrait<"'more' must be >= 0", CPred<"$more >= 0">>
]> {
let arguments = (ins
LTLAnySequenceType:$input,
I64Attr:$base,
I64Attr:$more);
let results = (outs LTLSequenceType:$result);
let assemblyFormat = [{
$input `,` $base `,` $more attr-dict `:` type($input)
}];
let hasFolder = 1;
let summary = "`goto`-style non-consecutively repeating sequence.";
let description = [{
Non-consecutive repetition of the `$input` sequence. This must hold between `$base`
and `$base + $more` times in a finite number of evaluations. The final evaluation
in the sequence has to match. The `$base` must be greater than or equal to zero
and the range `$more` can't be omitted. For example, a !b b b !b !b b c represents
a matching observation of `ltl.goto_repeat %b, 1, 2`, but a !b b b !b !b b !b c doesn't.
}];
}
def NonConsecutiveRepeatOp : LTLOp<"non_consecutive_repeat", [
Pure,
PredOpTrait<"'base' must be >= 0", CPred<"$base >= 0">>,
PredOpTrait<"'more' must be >= 0", CPred<"$more >= 0">>
]> {
let arguments = (ins
LTLAnySequenceType:$input,
I64Attr:$base,
I64Attr:$more);
let results = (outs LTLSequenceType:$result);
let assemblyFormat = [{
$input `,` $base `,` $more attr-dict `:` type($input)
}];
let hasFolder = 1;
let summary = "`goto`-style non-consecutively repeating sequence.";
let description = [{
Non-consecutive repetition of the `$input` sequence. This must hold between `$base`
and `$base + $more` times in a finite number of evaluations. The final evaluation
in the sequence does not have to match. The `$base` must be greater than or equal to zero
and the range `$more` can't be omitted. For example, both a !b b b !b !b b c and
a !b b b !b !b b !b c represent matching observations of
`ltl.non_consecutive_repeat %b, 1, 2`.
}];
}
//===----------------------------------------------------------------------===//
// Properties
//===----------------------------------------------------------------------===//

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

@ -22,10 +22,11 @@ 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>([&](auto op) -> ResultType {
return thisCast->visitLTL(op, args...);
})
ImplicationOp, UntilOp, EventuallyOp, ClockOp, DisableOp,
IntersectOp, NonConsecutiveRepeatOp, GoToRepeatOp>(
[&](auto op) -> ResultType {
return thisCast->visitLTL(op, args...);
})
.Default([&](auto) -> ResultType {
return thisCast->visitInvalidLTL(op, args...);
});
@ -59,6 +60,9 @@ public:
HANDLE(EventuallyOp, Unhandled);
HANDLE(ClockOp, Unhandled);
HANDLE(DisableOp, Unhandled);
HANDLE(IntersectOp, Unhandled);
HANDLE(NonConsecutiveRepeatOp, Unhandled);
HANDLE(GoToRepeatOp, Unhandled);
#undef HANDLE
};

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

@ -3427,9 +3427,12 @@ private:
EmittedProperty visitUnhandledLTL(Operation *op);
EmittedProperty visitLTL(ltl::AndOp op);
EmittedProperty visitLTL(ltl::OrOp op);
EmittedProperty visitLTL(ltl::IntersectOp op);
EmittedProperty visitLTL(ltl::DelayOp op);
EmittedProperty visitLTL(ltl::ConcatOp op);
EmittedProperty visitLTL(ltl::RepeatOp op);
EmittedProperty visitLTL(ltl::GoToRepeatOp op);
EmittedProperty visitLTL(ltl::NonConsecutiveRepeatOp op);
EmittedProperty visitLTL(ltl::NotOp op);
EmittedProperty visitLTL(ltl::ImplicationOp op);
EmittedProperty visitLTL(ltl::UntilOp op);
@ -3561,6 +3564,16 @@ EmittedProperty PropertyEmitter::visitLTL(ltl::OrOp op) {
return {PropertyPrecedence::Or};
}
EmittedProperty PropertyEmitter::visitLTL(ltl::IntersectOp op) {
llvm::interleave(
op.getInputs(),
[&](auto input) {
emitNestedProperty(input, PropertyPrecedence::Intersect);
},
[&]() { ps << PP::space << "intersect" << PP::nbsp; });
return {PropertyPrecedence::Intersect};
}
EmittedProperty PropertyEmitter::visitLTL(ltl::DelayOp op) {
ps << "##";
if (auto length = op.getLength()) {
@ -3608,19 +3621,15 @@ EmittedProperty PropertyEmitter::visitLTL(ltl::ConcatOp op) {
}
EmittedProperty PropertyEmitter::visitLTL(ltl::RepeatOp op) {
emitNestedProperty(op.getInput(), PropertyPrecedence::Unary);
emitNestedProperty(op.getInput(), PropertyPrecedence::Repeat);
if (auto more = op.getMore()) {
if (*more == 0) {
ps << "[*";
ps.addAsString(op.getBase());
ps << "]";
} else {
ps << "[*";
ps.addAsString(op.getBase());
ps << "[*";
ps.addAsString(op.getBase());
if (*more != 0) {
ps << ":";
ps.addAsString(op.getBase() + *more);
ps << "]";
}
ps << "]";
} else {
if (op.getBase() == 0) {
ps << "[*]";
@ -3632,7 +3641,37 @@ EmittedProperty PropertyEmitter::visitLTL(ltl::RepeatOp op) {
ps << ":$]";
}
}
return {PropertyPrecedence::Unary};
return {PropertyPrecedence::Repeat};
}
EmittedProperty PropertyEmitter::visitLTL(ltl::GoToRepeatOp op) {
emitNestedProperty(op.getInput(), PropertyPrecedence::Repeat);
// More always exists
auto more = op.getMore();
ps << "[->";
ps.addAsString(op.getBase());
if (more != 0) {
ps << ":";
ps.addAsString(op.getBase() + more);
}
ps << "]";
return {PropertyPrecedence::Repeat};
}
EmittedProperty PropertyEmitter::visitLTL(ltl::NonConsecutiveRepeatOp op) {
emitNestedProperty(op.getInput(), PropertyPrecedence::Repeat);
// More always exists
auto more = op.getMore();
ps << "[=";
ps.addAsString(op.getBase());
if (more != 0) {
ps << ":";
ps.addAsString(op.getBase() + more);
}
ps << "]";
return {PropertyPrecedence::Repeat};
}
EmittedProperty PropertyEmitter::visitLTL(ltl::NotOp op) {

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

@ -1616,9 +1616,12 @@ struct FIRRTLLowering : public FIRRTLVisitor<FIRRTLLowering, LogicalResult> {
LogicalResult visitExpr(ClockGateIntrinsicOp op);
LogicalResult visitExpr(LTLAndIntrinsicOp op);
LogicalResult visitExpr(LTLOrIntrinsicOp op);
LogicalResult visitExpr(LTLIntersectIntrinsicOp op);
LogicalResult visitExpr(LTLDelayIntrinsicOp op);
LogicalResult visitExpr(LTLConcatIntrinsicOp op);
LogicalResult visitExpr(LTLRepeatIntrinsicOp op);
LogicalResult visitExpr(LTLGoToRepeatIntrinsicOp op);
LogicalResult visitExpr(LTLNonConsecutiveRepeatIntrinsicOp op);
LogicalResult visitExpr(LTLNotIntrinsicOp op);
LogicalResult visitExpr(LTLImplicationIntrinsicOp op);
LogicalResult visitExpr(LTLUntilIntrinsicOp op);
@ -3724,6 +3727,12 @@ LogicalResult FIRRTLLowering::visitExpr(LTLOrIntrinsicOp op) {
ValueRange{getLoweredValue(op.getLhs()), getLoweredValue(op.getRhs())});
}
LogicalResult FIRRTLLowering::visitExpr(LTLIntersectIntrinsicOp op) {
return setLoweringToLTL<ltl::IntersectOp>(
op,
ValueRange{getLoweredValue(op.getLhs()), getLoweredValue(op.getRhs())});
}
LogicalResult FIRRTLLowering::visitExpr(LTLDelayIntrinsicOp op) {
return setLoweringToLTL<ltl::DelayOp>(op, getLoweredValue(op.getInput()),
op.getDelayAttr(), op.getLengthAttr());
@ -3740,6 +3749,16 @@ LogicalResult FIRRTLLowering::visitExpr(LTLRepeatIntrinsicOp op) {
op.getBaseAttr(), op.getMoreAttr());
}
LogicalResult FIRRTLLowering::visitExpr(LTLGoToRepeatIntrinsicOp op) {
return setLoweringToLTL<ltl::GoToRepeatOp>(
op, getLoweredValue(op.getInput()), op.getBaseAttr(), op.getMoreAttr());
}
LogicalResult FIRRTLLowering::visitExpr(LTLNonConsecutiveRepeatIntrinsicOp op) {
return setLoweringToLTL<ltl::NonConsecutiveRepeatOp>(
op, getLoweredValue(op.getInput()), op.getBaseAttr(), op.getMoreAttr());
}
LogicalResult FIRRTLLowering::visitExpr(LTLNotIntrinsicOp op) {
return setLoweringToLTL<ltl::NotOp>(op, getLoweredValue(op.getInput()));
}

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

@ -357,6 +357,18 @@ public:
}
};
class CirctLTLClockConverter
: public IntrinsicOpConverter<LTLClockIntrinsicOp> {
public:
using IntrinsicOpConverter::IntrinsicOpConverter;
bool check(GenericIntrinsic gi) override {
return gi.hasNInputs(2) || gi.sizedInput<UIntType>(0, 1) ||
gi.typedInput<ClockType>(1) || gi.sizedOutput<UIntType>(1) ||
gi.hasNParam(0);
}
};
class CirctLTLRepeatConverter : public IntrinsicConverter {
public:
using IntrinsicConverter::IntrinsicConverter;
@ -381,15 +393,51 @@ public:
}
};
class CirctLTLClockConverter
: public IntrinsicOpConverter<LTLClockIntrinsicOp> {
class CirctLTLGoToRepeatConverter : public IntrinsicConverter {
public:
using IntrinsicOpConverter::IntrinsicOpConverter;
using IntrinsicConverter::IntrinsicConverter;
bool check(GenericIntrinsic gi) override {
return gi.hasNInputs(2) || gi.sizedInput<UIntType>(0, 1) ||
gi.typedInput<ClockType>(1) || gi.sizedOutput<UIntType>(1) ||
gi.hasNParam(0);
return gi.hasNInputs(1) || gi.sizedInput<UIntType>(0, 1) ||
gi.sizedOutput<UIntType>(1) || gi.namedIntParam("base") ||
gi.namedIntParam("more") || gi.hasNParam(1, 1);
}
void convert(GenericIntrinsic gi, GenericIntrinsicOpAdaptor adaptor,
PatternRewriter &rewriter) override {
auto getI64Attr = [&](IntegerAttr val) {
if (!val)
return IntegerAttr();
return rewriter.getI64IntegerAttr(val.getValue().getZExtValue());
};
auto base = getI64Attr(gi.getParamValue<IntegerAttr>("base"));
auto more = getI64Attr(gi.getParamValue<IntegerAttr>("more"));
rewriter.replaceOpWithNewOp<LTLGoToRepeatIntrinsicOp>(
gi.op, gi.op.getResultTypes(), adaptor.getOperands()[0], base, more);
}
};
class CirctLTLNonConsecutiveRepeatConverter : public IntrinsicConverter {
public:
using IntrinsicConverter::IntrinsicConverter;
bool check(GenericIntrinsic gi) override {
return gi.hasNInputs(1) || gi.sizedInput<UIntType>(0, 1) ||
gi.sizedOutput<UIntType>(1) || gi.namedIntParam("base") ||
gi.namedIntParam("more") || gi.hasNParam(1, 1);
}
void convert(GenericIntrinsic gi, GenericIntrinsicOpAdaptor adaptor,
PatternRewriter &rewriter) override {
auto getI64Attr = [&](IntegerAttr val) {
if (!val)
return IntegerAttr();
return rewriter.getI64IntegerAttr(val.getValue().getZExtValue());
};
auto base = getI64Attr(gi.getParamValue<IntegerAttr>("base"));
auto more = getI64Attr(gi.getParamValue<IntegerAttr>("more"));
rewriter.replaceOpWithNewOp<LTLNonConsecutiveRepeatIntrinsicOp>(
gi.op, gi.op.getResultTypes(), adaptor.getOperands()[0], base, more);
}
};
@ -613,6 +661,8 @@ void FIRRTLIntrinsicLoweringDialectInterface::populateIntrinsicLowerings(
"circt_ltl_and");
lowering.add<CirctLTLBinaryConverter<LTLOrIntrinsicOp>>("circt.ltl.or",
"circt_ltl_or");
lowering.add<CirctLTLBinaryConverter<LTLIntersectIntrinsicOp>>(
"circt.ltl.intersect", "circt_ltl_intersect");
lowering.add<CirctLTLBinaryConverter<LTLConcatIntrinsicOp>>(
"circt.ltl.concat", "circt_ltl_concat");
lowering.add<CirctLTLBinaryConverter<LTLImplicationIntrinsicOp>>(
@ -628,6 +678,10 @@ void FIRRTLIntrinsicLoweringDialectInterface::populateIntrinsicLowerings(
lowering.add<CirctLTLDelayConverter>("circt.ltl.delay", "circt_ltl_delay");
lowering.add<CirctLTLRepeatConverter>("circt.ltl.repeat", "circt_ltl_repeat");
lowering.add<CirctLTLGoToRepeatConverter>("circt.ltl.goto_repeat",
"circt_ltl_goto_repeat");
lowering.add<CirctLTLNonConsecutiveRepeatConverter>(
"circt.ltl.non_consecutive_repeat", "circt_ltl_non_consecutive_repeat");
lowering.add<CirctLTLClockConverter>("circt.ltl.clock", "circt_ltl_clock");
lowering.add<CirctVerifConverter<VerifAssertIntrinsicOp>>(

4
lib/Dialect/FIRRTL/FIRRTLOps.cpp
View File

@ -164,6 +164,8 @@ Flow firrtl::swapFlow(Flow flow) {
case Flow::Duplex:
return Flow::Duplex;
}
// Unreachable but silences warning
llvm_unreachable("Unsupported Flow type.");
}
constexpr const char *toString(Flow flow) {
@ -177,6 +179,8 @@ constexpr const char *toString(Flow flow) {
case Flow::Duplex:
return "duplex flow";
}
// Unreachable but silences warning
llvm_unreachable("Unsupported Flow type.");
}
Flow firrtl::foldFlow(Value val, Flow accumulatedFlow) {

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

@ -92,18 +92,36 @@ void ConcatOp::getCanonicalizationPatterns(RewritePatternSet &results,
}
//===----------------------------------------------------------------------===//
// RepeatOp
// RepeatLikeOps
//===----------------------------------------------------------------------===//
OpFoldResult RepeatOp::fold(FoldAdaptor adaptor) {
// repeat(s, 1, 0) -> s
if (adaptor.getBase() == 1 && adaptor.getMore() == 0 &&
isa<SequenceType>(getInput().getType()))
return getInput();
namespace {
struct RepeatLikeOp {
static OpFoldResult fold(uint64_t base, uint64_t more, Value input) {
// repeat(s, 1, 0) -> s
if (base == 1 && more == 0 && isa<SequenceType>(input.getType()))
return input;
return {};
}
};
} // namespace
OpFoldResult RepeatOp::fold(FoldAdaptor adaptor) {
auto more = adaptor.getMore();
if (more.has_value())
return RepeatLikeOp::fold(adaptor.getBase(), *more, getInput());
return {};
}
OpFoldResult GoToRepeatOp::fold(FoldAdaptor adaptor) {
return RepeatLikeOp::fold(adaptor.getBase(), adaptor.getMore(), getInput());
}
OpFoldResult NonConsecutiveRepeatOp::fold(FoldAdaptor adaptor) {
return RepeatLikeOp::fold(adaptor.getBase(), adaptor.getMore(), getInput());
}
//===----------------------------------------------------------------------===//
// DisableOp
//===----------------------------------------------------------------------===//

8
lib/Dialect/LTL/LTLOps.cpp
View File

@ -56,6 +56,14 @@ OrOp::inferReturnTypes(MLIRContext *context, std::optional<Location> loc,
return inferAndLikeReturnTypes(context, operands, inferredReturnTypes);
}
LogicalResult
IntersectOp::inferReturnTypes(MLIRContext *context, std::optional<Location> loc,
ValueRange operands, DictionaryAttr attributes,
OpaqueProperties properties, RegionRange regions,
SmallVectorImpl<Type> &inferredReturnTypes) {
return inferAndLikeReturnTypes(context, operands, inferredReturnTypes);
}
//===----------------------------------------------------------------------===//
// ClockOp
//===----------------------------------------------------------------------===//

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

@ -63,48 +63,48 @@ hw.module @BasicEmissionTemporal(in %a: i1) {
// CHECK-LABEL: module Sequences
hw.module @Sequences(in %clk: i1, in %a: i1, in %b: i1) {
// CHECK: assert property (##0 a);
// CHECK: assert property (##4 a);
// CHECK: assert property (##[5:6] a);
// CHECK: assert property (##[7:$] a);
// CHECK: assert property (##[*] a);
// CHECK: assert property (##[+] a);
%d0 = ltl.delay %a, 0, 0 : i1
%d1 = ltl.delay %a, 4, 0 : i1
%d2 = ltl.delay %a, 5, 1 : i1
%d3 = ltl.delay %a, 7 : i1
%d4 = ltl.delay %a, 0 : i1
%d5 = ltl.delay %a, 1 : i1
verif.assert %d0 : !ltl.sequence
// CHECK: assert property (##4 a);
%d1 = ltl.delay %a, 4, 0 : i1
verif.assert %d1 : !ltl.sequence
// CHECK: assert property (##[5:6] a);
%d2 = ltl.delay %a, 5, 1 : i1
verif.assert %d2 : !ltl.sequence
// CHECK: assert property (##[7:$] a);
%d3 = ltl.delay %a, 7 : i1
verif.assert %d3 : !ltl.sequence
// CHECK: assert property (##[*] a);
%d4 = ltl.delay %a, 0 : i1
verif.assert %d4 : !ltl.sequence
// CHECK: assert property (##[+] a);
%d5 = ltl.delay %a, 1 : i1
verif.assert %d5 : !ltl.sequence
// CHECK: assert property (a ##0 a);
// CHECK: assert property (a ##4 a);
// CHECK: assert property (a ##4 a ##[5:6] a);
// CHECK: assert property (##4 a ##[5:6] a ##[7:$] a);
%c0 = ltl.concat %a, %a : i1, i1
%c1 = ltl.concat %a, %d1 : i1, !ltl.sequence
%c2 = ltl.concat %a, %d1, %d2 : i1, !ltl.sequence, !ltl.sequence
%c3 = ltl.concat %d1, %d2, %d3 : !ltl.sequence, !ltl.sequence, !ltl.sequence
verif.assert %c0 : !ltl.sequence
// CHECK: assert property (a ##4 a);
%c1 = ltl.concat %a, %d1 : i1, !ltl.sequence
verif.assert %c1 : !ltl.sequence
// CHECK: assert property (a ##4 a ##[5:6] a);
%c2 = ltl.concat %a, %d1, %d2 : i1, !ltl.sequence, !ltl.sequence
verif.assert %c2 : !ltl.sequence
// CHECK: assert property (##4 a ##[5:6] a ##[7:$] a);
%c3 = ltl.concat %d1, %d2, %d3 : !ltl.sequence, !ltl.sequence, !ltl.sequence
verif.assert %c3 : !ltl.sequence
// CHECK: assert property (a and b);
// CHECK: assert property (a ##0 a and a ##4 a);
// CHECK: assert property (a or b);
// CHECK: assert property (a ##0 a or a ##4 a);
%g0 = ltl.and %a, %b : i1, i1
%g1 = ltl.and %c0, %c1 : !ltl.sequence, !ltl.sequence
%g2 = ltl.or %a, %b : i1, i1
%g3 = ltl.or %c0, %c1 : !ltl.sequence, !ltl.sequence
verif.assert %g0 : !ltl.sequence
// CHECK: assert property (a ##0 a and a ##4 a);
%g1 = ltl.and %c0, %c1 : !ltl.sequence, !ltl.sequence
verif.assert %g1 : !ltl.sequence
// CHECK: assert property (a or b);
%g2 = ltl.or %a, %b : i1, i1
verif.assert %g2 : !ltl.sequence
// CHECK: assert property (a ##0 a or a ##4 a);
%g3 = ltl.or %c0, %c1 : !ltl.sequence, !ltl.sequence
verif.assert %g3 : !ltl.sequence
// CHECK: assert property (a[*0]);
@ -126,20 +126,40 @@ hw.module @Sequences(in %clk: i1, in %a: i1, in %b: i1) {
%r5 = ltl.repeat %a, 1 : i1
verif.assert %r5 : !ltl.sequence
// CHECK: assert property (a[->0]);
%gtr0 = ltl.goto_repeat %a, 0, 0 : i1
verif.assert %gtr0 : !ltl.sequence
// CHECK: assert property (a[->4]);
%gtr1 = ltl.goto_repeat %a, 4, 0 : i1
verif.assert %gtr1 : !ltl.sequence
// CHECK: assert property (a[->5:6]);
%gtr2 = ltl.goto_repeat %a, 5, 1 : i1
verif.assert %gtr2 : !ltl.sequence
// CHECK: assert property (a[=0]);
%ncr0 = ltl.non_consecutive_repeat %a, 0, 0 : i1
verif.assert %ncr0 : !ltl.sequence
// CHECK: assert property (a[=4]);
%ncr1 = ltl.non_consecutive_repeat %a, 4, 0 : i1
verif.assert %ncr1 : !ltl.sequence
// CHECK: assert property (a[=5:6]);
%ncr2 = ltl.non_consecutive_repeat %a, 5, 1 : i1
verif.assert %ncr2 : !ltl.sequence
// CHECK: assert property (@(posedge clk) a);
// CHECK: assert property (@(negedge clk) a);
// CHECK: assert property (@(edge clk) a);
// CHECK: assert property (@(posedge clk) ##4 a);
// CHECK: assert property (b ##0 (@(posedge clk) a));
%k0 = ltl.clock %a, posedge %clk : i1
%k1 = ltl.clock %a, negedge %clk : i1
%k2 = ltl.clock %a, edge %clk : i1
%k3 = ltl.clock %d1, posedge %clk : !ltl.sequence
%k4 = ltl.concat %b, %k0 : i1, !ltl.sequence
verif.assert %k0 : !ltl.sequence
// CHECK: assert property (@(negedge clk) a);
%k1 = ltl.clock %a, negedge %clk : i1
verif.assert %k1 : !ltl.sequence
// CHECK: assert property (@(edge clk) a);
%k2 = ltl.clock %a, edge %clk : i1
verif.assert %k2 : !ltl.sequence
// CHECK: assert property (@(posedge clk) ##4 a);
%k3 = ltl.clock %d1, posedge %clk : !ltl.sequence
verif.assert %k3 : !ltl.sequence
// CHECK: assert property (b ##0 (@(posedge clk) a));
%k4 = ltl.concat %b, %k0 : i1, !ltl.sequence
verif.assert %k4 : !ltl.sequence
}

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

@ -63,23 +63,35 @@ firrtl.circuit "Intrinsics" {
firrtl.module @LTLAndVerif(in %clk: !firrtl.clock, in %a: !firrtl.uint<1>, in %b: !firrtl.uint<1>) {
// CHECK-NEXT: [[CLK:%.+]] = seq.from_clock %clk
// CHECK-NEXT: [[D0:%.+]] = ltl.delay %a, 42 : i1
// CHECK-NEXT: [[D1:%.+]] = ltl.delay %b, 42, 1337 : i1
%d0 = firrtl.int.ltl.delay %a, 42 : (!firrtl.uint<1>) -> !firrtl.uint<1>
// CHECK-NEXT: [[D1:%.+]] = ltl.delay %b, 42, 1337 : i1
%d1 = firrtl.int.ltl.delay %b, 42, 1337 : (!firrtl.uint<1>) -> !firrtl.uint<1>
// CHECK-NEXT: [[L0:%.+]] = ltl.and [[D0]], [[D1]] : !ltl.sequence, !ltl.sequence
// CHECK-NEXT: [[L1:%.+]] = ltl.or %a, [[L0]] : i1, !ltl.sequence
%l0 = firrtl.int.ltl.and %d0, %d1 : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1>
// CHECK-NEXT: [[L1:%.+]] = ltl.or %a, [[L0]] : i1, !ltl.sequence
%l1 = firrtl.int.ltl.or %a, %l0 : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1>
// CHECK-NEXT: [[L2:%.+]] = ltl.intersect [[D0]], [[D1]] : !ltl.sequence, !ltl.sequence
%l2 = firrtl.int.ltl.intersect %d0, %d1 : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1>
// CHECK-NEXT: [[C0:%.+]] = ltl.concat [[D0]], [[L1]] : !ltl.sequence, !ltl.sequence
%c0 = firrtl.int.ltl.concat %d0, %l1 : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1>
// CHECK-NEXT: [[R0:%.+]] = ltl.repeat %a, 42 : i1
// CHECK-NEXT: [[R1:%.+]] = ltl.repeat %b, 42, 1337 : i1
%r0 = firrtl.int.ltl.repeat %a, 42 : (!firrtl.uint<1>) -> !firrtl.uint<1>
// CHECK-NEXT: [[R1:%.+]] = ltl.repeat %b, 42, 1337 : i1
%r1 = firrtl.int.ltl.repeat %b, 42, 1337 : (!firrtl.uint<1>) -> !firrtl.uint<1>
// CHECK-NEXT: [[GTR0:%.+]] = ltl.goto_repeat %a, 42, 0 : i1
%gtr0 = firrtl.int.ltl.goto_repeat %a, 42, 0 : (!firrtl.uint<1>) -> !firrtl.uint<1>
// CHECK-NEXT: [[GTR1:%.+]] = ltl.goto_repeat %b, 1337, 9001 : i1
%gtr1 = firrtl.int.ltl.goto_repeat %b, 1337, 9001 : (!firrtl.uint<1>) -> !firrtl.uint<1>
// CHECK-NEXT: [[NCR0:%.+]] = ltl.non_consecutive_repeat %a, 42, 0 : i1
%ncr0 = firrtl.int.ltl.non_consecutive_repeat %a, 42, 0 : (!firrtl.uint<1>) -> !firrtl.uint<1>
// CHECK-NEXT: [[NCR1:%.+]] = ltl.non_consecutive_repeat %b, 1337, 9001 : i1
%ncr1 = firrtl.int.ltl.non_consecutive_repeat %b, 1337, 9001 : (!firrtl.uint<1>) -> !firrtl.uint<1>
// CHECK-NEXT: [[N0:%.+]] = ltl.not [[C0]] : !ltl.sequence
%n0 = firrtl.int.ltl.not %c0 : (!firrtl.uint<1>) -> !firrtl.uint<1>
@ -99,16 +111,16 @@ firrtl.circuit "Intrinsics" {
%d2 = firrtl.int.ltl.disable %k0, %b : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1>
// CHECK-NEXT: verif.assert %a : i1
// CHECK-NEXT: verif.assert %a label "hello" : i1
// CHECK-NEXT: verif.assume [[C0]] : !ltl.sequence
// CHECK-NEXT: verif.assume [[C0]] label "hello" : !ltl.sequence
// CHECK-NEXT: verif.cover [[K0]] : !ltl.property
// CHECK-NEXT: verif.cover [[K0]] label "hello" : !ltl.property
firrtl.int.verif.assert %a : !firrtl.uint<1>
// CHECK-NEXT: verif.assert %a label "hello" : i1
firrtl.int.verif.assert %a {label = "hello"} : !firrtl.uint<1>
// CHECK-NEXT: verif.assume [[C0]] : !ltl.sequence
firrtl.int.verif.assume %c0 : !firrtl.uint<1>
// CHECK-NEXT: verif.assume [[C0]] label "hello" : !ltl.sequence
firrtl.int.verif.assume %c0 {label = "hello"} : !firrtl.uint<1>
// CHECK-NEXT: verif.cover [[K0]] : !ltl.property
firrtl.int.verif.cover %k0 : !firrtl.uint<1>
// CHECK-NEXT: verif.cover [[K0]] label "hello" : !ltl.property
firrtl.int.verif.cover %k0 {label = "hello"} : !firrtl.uint<1>
}

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

@ -49,26 +49,32 @@ firrtl.circuit "Foo" {
firrtl.int.generic "circt_ltl_and" %in0, %in1: (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1>
// CHECK-NEXT: firrtl.int.ltl.or %in0, %in1 :
firrtl.int.generic "circt_ltl_or" %in0, %in1 : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1>
// CHECK-NEXT: firrtl.int.ltl.intersect %in0, %in1 :
firrtl.int.generic "circt_ltl_intersect" %in0, %in1 : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1>
// CHECK-NEXT: firrtl.int.ltl.delay %in0, 42 :
// CHECK-NEXT: firrtl.int.ltl.delay %in0, 42, 1337 :
firrtl.int.generic "circt_ltl_delay" <delay: i64 = 42> %in0 : (!firrtl.uint<1>) -> !firrtl.uint<1>
// CHECK-NEXT: firrtl.int.ltl.delay %in0, 42, 1337 :
firrtl.int.generic "circt_ltl_delay" <delay: i64 = 42, length: i64 = 1337> %in0 : (!firrtl.uint<1>) -> !firrtl.uint<1>
// CHECK-NEXT: firrtl.int.ltl.repeat %in0, 42 :
// CHECK-NEXT: firrtl.int.ltl.repeat %in0, 42, 1337 :
firrtl.int.generic "circt_ltl_repeat" <base: i64 = 42> %in0 : (!firrtl.uint<1>) -> !firrtl.uint<1>
// CHECK-NEXT: firrtl.int.ltl.repeat %in0, 42, 1337 :
firrtl.int.generic "circt_ltl_repeat" <base: i64 = 42, more: i64 = 1337> %in0 : (!firrtl.uint<1>) -> !firrtl.uint<1>
// CHECK-NEXT: firrtl.int.ltl.goto_repeat %in0, 42, 1337 :
firrtl.int.generic "circt_ltl_goto_repeat" <base: i64 = 42, more: i64 = 1337> %in0 : (!firrtl.uint<1>) -> !firrtl.uint<1>
// CHECK-NEXT: firrtl.int.ltl.non_consecutive_repeat %in0, 42, 1337 :
firrtl.int.generic "circt_ltl_non_consecutive_repeat" <base: i64 = 42, more: i64 = 1337> %in0 : (!firrtl.uint<1>) -> !firrtl.uint<1>
// CHECK-NEXT: firrtl.int.ltl.concat %in0, %in1 :
// CHECK-NEXT: firrtl.int.ltl.not %in0 :
// CHECK-NEXT: firrtl.int.ltl.implication %in0, %in1 :
// CHECK-NEXT: firrtl.int.ltl.until %in0, %in1 :
// CHECK-NEXT: firrtl.int.ltl.eventually %in0 :
firrtl.int.generic "circt_ltl_concat" %in0, %in1: (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1>
// CHECK-NEXT: firrtl.int.ltl.not %in0 :
firrtl.int.generic "circt_ltl_not" %in0 : (!firrtl.uint<1>) -> !firrtl.uint<1>
// CHECK-NEXT: firrtl.int.ltl.implication %in0, %in1 :
firrtl.int.generic "circt_ltl_implication" %in0, %in1 : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1>
// CHECK-NEXT: firrtl.int.ltl.until %in0, %in1 :
firrtl.int.generic "circt_ltl_until" %in0, %in1 : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1>
// CHECK-NEXT: firrtl.int.ltl.eventually %in0 :
firrtl.int.generic "circt_ltl_eventually" %in0 : (!firrtl.uint<1>) -> !firrtl.uint<1>
// CHECK-NEXT: firrtl.int.ltl.clock %in0, %clk :

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

@ -109,6 +109,26 @@ func.func @RepeatFolds(%arg0: !ltl.sequence) {
return
}
// CHECK-LABEL: @GoToRepeatFolds
func.func @GoToRepeatFolds(%arg0: !ltl.sequence) {
// repeat(s, 1, 0) -> s
// CHECK-NEXT: call @Seq(%arg0)
%0 = ltl.goto_repeat %arg0, 1, 0: !ltl.sequence
call @Seq(%0) : (!ltl.sequence) -> ()
return
}
// CHECK-LABEL: @NonConsecutiveRepeatFolds
func.func @NonConsecutiveRepeatFolds(%arg0: !ltl.sequence) {
// repeat(s, 1, 0) -> s
// CHECK-NEXT: call @Seq(%arg0)
%0 = ltl.non_consecutive_repeat %arg0, 1, 0: !ltl.sequence
call @Seq(%0) : (!ltl.sequence) -> ()
return
}
// CHECK-LABEL: @ClockingFolds
func.func @ClockingFolds(%arg0: !ltl.property) {
// disable(p, false) -> p