mirror of https://github.com/llvm/circt.git
[SV] Add defer and message support to assertions (#1974)
Add an optional message and list of operands to be interpolated into the
message to the verification operations in the SV dialect (immediate and
concurrent). This message is expected to be printed when the assertion
fails, and is emitted as `... else $error(msg, operands...)`.
Also add a new `defer` field to immediate assertions which allows for
the emission of `assert #0` ("observed deferred assertion") and `assert
final` ("final deferred assertion"). There are use cases in the FIRRTL
dialect that will make use of this feature in a follow-up commit.
This commit also adjusts the parsing/printing of verification ops in the
SV dialect to accomodate the optional label and optional message parts
more easily.
This commit is contained in:
Fabian Schuiki
GitHub
parent
f2f7229c24
commit
ae55ca7ecd
|
|
@ -55,6 +55,7 @@ include "circt/Dialect/SV/SVTypes.td"
|
|||
include "circt/Dialect/SV/SVExpressions.td"
|
||||
include "circt/Dialect/SV/SVInOutOps.td"
|
||||
include "circt/Dialect/SV/SVStatements.td"
|
||||
include "circt/Dialect/SV/SVVerification.td"
|
||||
include "circt/Dialect/SV/SVTypeDecl.td"
|
||||
|
||||
#endif // SV_TD
|
||||
|
|
|
|||
|
|
@ -481,84 +481,9 @@ def VerbatimOp : SVOp<"verbatim"> {
|
|||
}
|
||||
|
||||
//===----------------------------------------------------------------------===//
|
||||
// Verification Statements
|
||||
// Bind Statements
|
||||
//===----------------------------------------------------------------------===//
|
||||
|
||||
class ImmediateAssertionOp<string mnemonic, list<OpTrait> traits = []> :
|
||||
SVOp<mnemonic, traits> {
|
||||
let arguments = (ins I1:$expression, StrAttr:$label);
|
||||
let results = (outs);
|
||||
let assemblyFormat =
|
||||
"custom<OmitEmptyStringAttr>($label) attr-dict $expression `:` type($expression)";
|
||||
}
|
||||
|
||||
def AssertOp : ImmediateAssertionOp<"assert", [ProceduralOp]> {
|
||||
let summary = "immediate assertion statement";
|
||||
let description = [{
|
||||
Specify that a Boolean expression is always true. This can be used to both
|
||||
document the behavior of the design and to test that the design behaves as
|
||||
expected. See Section 16.3 of the SystemVerilog 2017 specification.
|
||||
}];
|
||||
}
|
||||
|
||||
def AssumeOp : ImmediateAssertionOp<"assume", [ProceduralOp]> {
|
||||
let summary = "immediate assume statement";
|
||||
let description = [{
|
||||
Specify that a Boolean expression is assumed to always be true. This can
|
||||
either be used as an assertion-like check that the expression is, in fact,
|
||||
always true or to bound legal input values during testing. See Section 16.3
|
||||
of the SystemVerilog 2017 specification.
|
||||
}];
|
||||
}
|
||||
|
||||
def CoverOp : ImmediateAssertionOp<"cover", [ProceduralOp]> {
|
||||
let summary = "immediate cover statement";
|
||||
let description = [{
|
||||
Specify that a Boolean expression should be monitored for coverage, i.e., a
|
||||
simulator will watch if it occurs and how many times it occurs. See section
|
||||
16.3 of the SystemVerilog 2017 specification.
|
||||
}];
|
||||
}
|
||||
|
||||
class ConcurrentAssertionOp<string mnemonic, list<OpTrait> traits = []> :
|
||||
SVOp<mnemonic, traits> {
|
||||
let arguments =
|
||||
(ins EventControlAttr:$event, I1:$clock, I1:$property, StrAttr:$label);
|
||||
let results = (outs);
|
||||
let assemblyFormat =
|
||||
"custom<OmitEmptyStringAttr>($label) $event $clock $property attr-dict `:`"
|
||||
" type($property)";
|
||||
}
|
||||
|
||||
def AssertConcurrentOp : ConcurrentAssertionOp<"assert.concurrent"> {
|
||||
let summary = "concurrent assertion statement, i.e., assert property";
|
||||
let description = [{
|
||||
Specify that a property of the hardware design is true whenever the property
|
||||
is evaluated. This can be used to both document the behavior of the design
|
||||
and to test that the design behaves as expected. See section 16.5 of the
|
||||
SystemVerilog 2017 specification.
|
||||
}];
|
||||
}
|
||||
|
||||
def AssumeConcurrentOp : ConcurrentAssertionOp<"assume.concurrent"> {
|
||||
let summary = "concurrent assume statement, i.e., assume property";
|
||||
let description = [{
|
||||
Specify that a property is assumed to be true whenever the property is
|
||||
evaluated. This can be used to both document the behavior of the design and
|
||||
to test that the design behaves as expected. See section 16.5 of the
|
||||
SystemVerilog 2017 specification.
|
||||
}];
|
||||
}
|
||||
|
||||
def CoverConcurrentOp : ConcurrentAssertionOp<"cover.concurrent"> {
|
||||
let summary = "concurrent cover statement, i.e., cover property";
|
||||
let description = [{
|
||||
Specify that a specific property should be monitored for coverage, i.e., a
|
||||
simulation will watch if it occurrs and how many times it occurs. See
|
||||
section 16.5 of the SystemVerilog 2017 specification.
|
||||
}];
|
||||
}
|
||||
|
||||
def BindOp : SVOp<"bind", []> {
|
||||
let summary = "indirect instantiation statement";
|
||||
let description = [{
|
||||
|
|
|
|||
|
|
@ -0,0 +1,153 @@
|
|||
//===- SVVerification.td - SV verification ops -------------*- tablegen -*-===//
|
||||
//
|
||||
// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
|
||||
// See https://llvm.org/LICENSE.txt for license information.
|
||||
// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
|
||||
//
|
||||
//===----------------------------------------------------------------------===//
|
||||
//
|
||||
// This describes the ops for SystemVerilog verification statements and
|
||||
// declarations.
|
||||
//
|
||||
//===----------------------------------------------------------------------===//
|
||||
|
||||
/// Immediate assertions, like `assert`.
|
||||
def ImmediateAssert: I32EnumAttrCase<"Immediate", 0, "immediate">;
|
||||
/// Observed deferred assertions, like `assert #0`.
|
||||
def ObservedAssert: I32EnumAttrCase<"Observed", 1, "observed">;
|
||||
/// Final deferred assertions, like `assert final`.
|
||||
def FinalAssert: I32EnumAttrCase<"Final", 2, "final">;
|
||||
|
||||
/// A mode specifying how immediate/deferred assertions operate.
|
||||
def DeferAssertAttr : I32EnumAttr<
|
||||
"DeferAssert", "assertion deferring mode",
|
||||
[ImmediateAssert, ObservedAssert, FinalAssert]>
|
||||
{
|
||||
let cppNamespace = "circt::sv";
|
||||
}
|
||||
|
||||
/// A constraint forcing `cover` ops to have no message.
|
||||
def NoMessageVerif : PredOpTrait<"has no message",
|
||||
CPred<"!$message && $operands.empty()">>;
|
||||
|
||||
/// Immediate verification operations defined by the SV standard.
|
||||
class ImmediateVerifOp<string mnemonic, list<OpTrait> traits = []> :
|
||||
SVOp<mnemonic, [ProceduralOp] # traits> {
|
||||
let arguments = (ins
|
||||
I1:$expression,
|
||||
DeferAssertAttr:$defer,
|
||||
OptionalAttr<StrAttr>:$label,
|
||||
OptionalAttr<StrAttr>:$message, Variadic<AnyType>:$operands);
|
||||
|
||||
let assemblyFormat = [{
|
||||
$expression `,` $defer
|
||||
(`label` $label^)?
|
||||
(`message` $message^ (`(` $operands^ `)` `:` type($operands))?)?
|
||||
attr-dict
|
||||
}];
|
||||
|
||||
let builders = [
|
||||
// no label, no message
|
||||
OpBuilder<(ins "mlir::Value":$expression,
|
||||
DeferAssertAttr.storageType:$defer),
|
||||
[{ build(odsBuilder, odsState, expression, defer, StringAttr{},
|
||||
StringAttr{}, ValueRange{}); }]>,
|
||||
// no message
|
||||
OpBuilder<(ins "mlir::Value":$expression,
|
||||
DeferAssertAttr.storageType:$defer, StrAttr.storageType:$label),
|
||||
[{ build(odsBuilder, odsState, expression, defer, label, StringAttr{},
|
||||
ValueRange{}); }]>
|
||||
];
|
||||
}
|
||||
|
||||
def AssertOp : ImmediateVerifOp<"assert"> {
|
||||
let summary = "immediate assertion statement";
|
||||
let description = [{
|
||||
Specify that a Boolean expression is always true. This can be used to both
|
||||
document the behavior of the design and to test that the design behaves as
|
||||
expected. See Section 16.3 of the SystemVerilog 2017 specification.
|
||||
}];
|
||||
}
|
||||
|
||||
def AssumeOp : ImmediateVerifOp<"assume"> {
|
||||
let summary = "immediate assume statement";
|
||||
let description = [{
|
||||
Specify that a Boolean expression is assumed to always be true. This can
|
||||
either be used as an assertion-like check that the expression is, in fact,
|
||||
always true or to bound legal input values during testing. See Section 16.3
|
||||
of the SystemVerilog 2017 specification.
|
||||
}];
|
||||
}
|
||||
|
||||
def CoverOp : ImmediateVerifOp<"cover", [NoMessageVerif]> {
|
||||
let summary = "immediate cover statement";
|
||||
let description = [{
|
||||
Specify that a Boolean expression should be monitored for coverage, i.e., a
|
||||
simulator will watch if it occurs and how many times it occurs. See section
|
||||
16.3 of the SystemVerilog 2017 specification.
|
||||
}];
|
||||
}
|
||||
|
||||
/// Concurrent verification operations defined by the SV standard.
|
||||
class ConcurrentVerifOp<string mnemonic, list<OpTrait> traits = []> :
|
||||
SVOp<mnemonic, traits> {
|
||||
let arguments = (ins
|
||||
EventControlAttr:$event, I1:$clock, I1:$property,
|
||||
OptionalAttr<StrAttr>:$label,
|
||||
OptionalAttr<StrAttr>:$message, Variadic<AnyType>:$operands);
|
||||
|
||||
let assemblyFormat = [{
|
||||
$event $clock `,` $property
|
||||
(`label` $label^)?
|
||||
(`message` $message^ (`(` $operands^ `)` `:` type($operands))?)?
|
||||
attr-dict
|
||||
}];
|
||||
|
||||
let builders = [
|
||||
// no label, no message
|
||||
OpBuilder<(ins
|
||||
EventControlAttr.storageType:$event,
|
||||
"mlir::Value":$clock,
|
||||
"mlir::Value":$property),
|
||||
[{ build(odsBuilder, odsState, event, clock, property, StringAttr{},
|
||||
StringAttr{}, ValueRange{}); }]>,
|
||||
// no message
|
||||
OpBuilder<(ins
|
||||
EventControlAttr.storageType:$event,
|
||||
"mlir::Value":$clock,
|
||||
"mlir::Value":$property,
|
||||
StrAttr.storageType:$label),
|
||||
[{ build(odsBuilder, odsState, event, clock, property, label,
|
||||
StringAttr{}, ValueRange{}); }]>
|
||||
];
|
||||
}
|
||||
|
||||
def AssertConcurrentOp : ConcurrentVerifOp<"assert.concurrent"> {
|
||||
let summary = "concurrent assertion statement, i.e., assert property";
|
||||
let description = [{
|
||||
Specify that a property of the hardware design is true whenever the property
|
||||
is evaluated. This can be used to both document the behavior of the design
|
||||
and to test that the design behaves as expected. See section 16.5 of the
|
||||
SystemVerilog 2017 specification.
|
||||
}];
|
||||
}
|
||||
|
||||
def AssumeConcurrentOp : ConcurrentVerifOp<"assume.concurrent"> {
|
||||
let summary = "concurrent assume statement, i.e., assume property";
|
||||
let description = [{
|
||||
Specify that a property is assumed to be true whenever the property is
|
||||
evaluated. This can be used to both document the behavior of the design and
|
||||
to test that the design behaves as expected. See section 16.5 of the
|
||||
SystemVerilog 2017 specification.
|
||||
}];
|
||||
}
|
||||
|
||||
def CoverConcurrentOp : ConcurrentVerifOp<"cover.concurrent",
|
||||
[NoMessageVerif]> {
|
||||
let summary = "concurrent cover statement, i.e., cover property";
|
||||
let description = [{
|
||||
Specify that a specific property should be monitored for coverage, i.e., a
|
||||
simulation will watch if it occurrs and how many times it occurs. See
|
||||
section 16.5 of the SystemVerilog 2017 specification.
|
||||
}];
|
||||
}
|
||||
|
|
@ -1943,8 +1943,7 @@ void NameCollector::collectNames(Block &block) {
|
|||
// Notice and renamify the labels on verification statements.
|
||||
if (isa<AssertOp, AssumeOp, CoverOp, AssertConcurrentOp, AssumeConcurrentOp,
|
||||
CoverConcurrentOp>(op)) {
|
||||
auto labelAttr = op.getAttrOfType<StringAttr>("label");
|
||||
if (!labelAttr.getValue().empty())
|
||||
if (auto labelAttr = op.getAttrOfType<StringAttr>("label"))
|
||||
names.addName(&op, labelAttr);
|
||||
}
|
||||
|
||||
|
|
@ -2081,14 +2080,15 @@ private:
|
|||
LogicalResult visitSV(VerbatimOp op);
|
||||
|
||||
void emitAssertionLabel(Operation *op, StringRef opName);
|
||||
LogicalResult emitImmediateAssertion(Operation *op, StringRef opName,
|
||||
Value expression);
|
||||
void emitAssertionMessage(StringAttr message, ValueRange args,
|
||||
SmallPtrSet<Operation *, 8> &ops);
|
||||
template <typename Op>
|
||||
LogicalResult emitImmediateAssertion(Op op, StringRef opName);
|
||||
LogicalResult visitSV(AssertOp op);
|
||||
LogicalResult visitSV(AssumeOp op);
|
||||
LogicalResult visitSV(CoverOp op);
|
||||
LogicalResult emitConcurrentAssertion(Operation *op, StringRef opName,
|
||||
EventControl event, Value clock,
|
||||
Value property);
|
||||
template <typename Op>
|
||||
LogicalResult emitConcurrentAssertion(Op op, StringRef opName);
|
||||
LogicalResult visitSV(AssertConcurrentOp op);
|
||||
LogicalResult visitSV(AssumeConcurrentOp op);
|
||||
LogicalResult visitSV(CoverConcurrentOp op);
|
||||
|
|
@ -2430,70 +2430,94 @@ LogicalResult StmtEmitter::visitSV(FinishOp op) {
|
|||
/// `enforceVerifLabels` option is set, a temporary name for the operation is
|
||||
/// picked and uniquified through `addName`.
|
||||
void StmtEmitter::emitAssertionLabel(Operation *op, StringRef opName) {
|
||||
if (!op->getAttrOfType<StringAttr>("label").getValue().empty()) {
|
||||
if (op->getAttrOfType<StringAttr>("label")) {
|
||||
os << names.getName(op) << ": ";
|
||||
} else if (state.options.enforceVerifLabels) {
|
||||
os << names.addName(op, opName) << ": ";
|
||||
}
|
||||
}
|
||||
|
||||
LogicalResult StmtEmitter::emitImmediateAssertion(Operation *op,
|
||||
StringRef opName,
|
||||
Value expression) {
|
||||
/// Emit the optional ` else $error(...)` portion of an immediate or concurrent
|
||||
/// verification operation.
|
||||
void StmtEmitter::emitAssertionMessage(StringAttr message, ValueRange args,
|
||||
SmallPtrSet<Operation *, 8> &ops) {
|
||||
if (!message)
|
||||
return;
|
||||
os << " else $error(\"";
|
||||
os.write_escaped(message.getValue());
|
||||
os << "\"";
|
||||
for (auto arg : args) {
|
||||
os << ", ";
|
||||
emitExpression(arg, ops);
|
||||
}
|
||||
os << ")";
|
||||
}
|
||||
|
||||
template <typename Op>
|
||||
LogicalResult StmtEmitter::emitImmediateAssertion(Op op, StringRef opName) {
|
||||
SmallPtrSet<Operation *, 8> ops;
|
||||
ops.insert(op);
|
||||
indent();
|
||||
emitAssertionLabel(op, opName);
|
||||
os << opName << "(";
|
||||
emitExpression(expression, ops);
|
||||
os << ");";
|
||||
os << opName;
|
||||
switch (op.defer()) {
|
||||
case DeferAssert::Immediate:
|
||||
break;
|
||||
case DeferAssert::Observed:
|
||||
os << " #0 ";
|
||||
break;
|
||||
case DeferAssert::Final:
|
||||
os << " final ";
|
||||
break;
|
||||
}
|
||||
os << "(";
|
||||
emitExpression(op.expression(), ops);
|
||||
os << ")";
|
||||
emitAssertionMessage(op.messageAttr(), op.operands(), ops);
|
||||
os << ";";
|
||||
emitLocationInfoAndNewLine(ops);
|
||||
return success();
|
||||
}
|
||||
|
||||
LogicalResult StmtEmitter::visitSV(AssertOp op) {
|
||||
return emitImmediateAssertion(op, "assert", op.expression());
|
||||
return emitImmediateAssertion(op, "assert");
|
||||
}
|
||||
|
||||
LogicalResult StmtEmitter::visitSV(AssumeOp op) {
|
||||
return emitImmediateAssertion(op, "assume", op.expression());
|
||||
return emitImmediateAssertion(op, "assume");
|
||||
}
|
||||
|
||||
LogicalResult StmtEmitter::visitSV(CoverOp op) {
|
||||
return emitImmediateAssertion(op, "cover", op.expression());
|
||||
return emitImmediateAssertion(op, "cover");
|
||||
}
|
||||
|
||||
LogicalResult StmtEmitter::emitConcurrentAssertion(Operation *op,
|
||||
StringRef opName,
|
||||
EventControl event,
|
||||
Value clock,
|
||||
Value property) {
|
||||
template <typename Op>
|
||||
LogicalResult StmtEmitter::emitConcurrentAssertion(Op op, StringRef opName) {
|
||||
SmallPtrSet<Operation *, 8> ops;
|
||||
ops.insert(op);
|
||||
indent();
|
||||
emitAssertionLabel(op, opName);
|
||||
os << opName << " property (@(" << stringifyEventControl(event) << " ";
|
||||
emitExpression(clock, ops);
|
||||
os << opName << " property (@(" << stringifyEventControl(op.event()) << " ";
|
||||
emitExpression(op.clock(), ops);
|
||||
os << ") ";
|
||||
emitExpression(property, ops);
|
||||
os << ");";
|
||||
emitExpression(op.property(), ops);
|
||||
os << ")";
|
||||
emitAssertionMessage(op.messageAttr(), op.operands(), ops);
|
||||
os << ";";
|
||||
emitLocationInfoAndNewLine(ops);
|
||||
return success();
|
||||
}
|
||||
|
||||
LogicalResult StmtEmitter::visitSV(AssertConcurrentOp op) {
|
||||
return emitConcurrentAssertion(op, "assert", op.event(), op.clock(),
|
||||
op.property());
|
||||
return emitConcurrentAssertion(op, "assert");
|
||||
}
|
||||
|
||||
LogicalResult StmtEmitter::visitSV(AssumeConcurrentOp op) {
|
||||
return emitConcurrentAssertion(op, "assume", op.event(), op.clock(),
|
||||
op.property());
|
||||
return emitConcurrentAssertion(op, "assume");
|
||||
}
|
||||
|
||||
LogicalResult StmtEmitter::visitSV(CoverConcurrentOp op) {
|
||||
return emitConcurrentAssertion(op, "cover", op.event(), op.clock(),
|
||||
op.property());
|
||||
return emitConcurrentAssertion(op, "cover");
|
||||
}
|
||||
|
||||
LogicalResult StmtEmitter::emitIfDef(Operation *op, StringRef cond) {
|
||||
|
|
|
|||
|
|
@ -3034,17 +3034,19 @@ LogicalResult FIRRTLLowering::lowerVerificationStatement(AOpTy op,
|
|||
if (!clock || !enable || !predicate)
|
||||
return failure();
|
||||
StringAttr label;
|
||||
if (op.nameAttr())
|
||||
if (op.nameAttr() && !op.nameAttr().getValue().empty())
|
||||
label = op.nameAttr();
|
||||
else
|
||||
label = builder.getStringAttr("");
|
||||
Operation *svOp;
|
||||
|
||||
if (!op.isConcurrent())
|
||||
addToAlwaysBlock(clock, [&]() {
|
||||
addIfProceduralBlock(enable, [&]() {
|
||||
// Create BOpTy inside the always/if.
|
||||
svOp = builder.create<BOpTy>(predicate, label);
|
||||
svOp = builder.create<BOpTy>(
|
||||
predicate,
|
||||
circt::sv::DeferAssertAttr::get(builder.getContext(),
|
||||
circt::sv::DeferAssert::Immediate),
|
||||
label);
|
||||
});
|
||||
});
|
||||
else {
|
||||
|
|
@ -3063,7 +3065,7 @@ LogicalResult FIRRTLLowering::lowerVerificationStatement(AOpTy op,
|
|||
}
|
||||
svOp = builder.create<COpTy>(
|
||||
circt::sv::EventControlAttr::get(builder.getContext(), event), clock,
|
||||
predicate, label);
|
||||
predicate, label, StringAttr{}, ValueRange{});
|
||||
}
|
||||
return success();
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1205,31 +1205,6 @@ static LogicalResult verifyBindOp(BindOp op) {
|
|||
return success();
|
||||
}
|
||||
|
||||
//===----------------------------------------------------------------------===//
|
||||
// Custom printer/parsers to be used with custom<> ODS assembly formats.
|
||||
//===----------------------------------------------------------------------===//
|
||||
|
||||
static ParseResult parseOmitEmptyStringAttr(OpAsmParser &p, StringAttr &str) {
|
||||
// TODO: No OpAsmParser::parseOptionalAttribute(StringAttr &a, Type b) API
|
||||
// exists. OpAsmParser::parseAttribute(StringAttr &a, Type b) does exist, but
|
||||
// produces an opError during parsing. This should eventually be cleaned up
|
||||
// to avoid the need to use a dummy attribute list.
|
||||
NamedAttrList dummy;
|
||||
p.parseOptionalAttribute(str, p.getBuilder().getType<mlir::NoneType>(),
|
||||
"label", dummy);
|
||||
if (!str) {
|
||||
str = p.getBuilder().getStringAttr("");
|
||||
return success();
|
||||
}
|
||||
return success();
|
||||
}
|
||||
|
||||
static void printOmitEmptyStringAttr(OpAsmPrinter &p, Operation *op,
|
||||
StringAttr str) {
|
||||
if (str && !str.getValue().empty())
|
||||
p.printAttributeWithoutType(str);
|
||||
}
|
||||
|
||||
//===----------------------------------------------------------------------===//
|
||||
// BindInterfaceOp
|
||||
//===----------------------------------------------------------------------===//
|
||||
|
|
|
|||
|
|
@ -407,19 +407,19 @@ firrtl.circuit "Simple" attributes {annotations = [{class =
|
|||
in %cCond: !firrtl.uint<1>, in %cEn: !firrtl.uint<1>) {
|
||||
|
||||
// CHECK-NEXT: %0 = comb.and %aEn, %aCond : i1
|
||||
// CHECK-NEXT: sv.assert.concurrent posedge %clock %0 : i1
|
||||
// CHECK-NEXT: sv.assert.concurrent posedge %clock, %0
|
||||
// CHECK-NEXT: %1 = comb.and %aEn, %aCond : i1
|
||||
// CHECK-NEXT: sv.assert.concurrent "assert_0" posedge %clock %1 : i1
|
||||
// CHECK-NEXT: sv.assert.concurrent posedge %clock, %1 label "assert_0"
|
||||
// CHECK-NEXT: %2 = comb.and %bEn, %bCond : i1
|
||||
// CHECK-NEXT: sv.assume.concurrent posedge %clock %2 : i1
|
||||
// CHECK-NEXT: sv.assume.concurrent posedge %clock, %2
|
||||
// CHECK-NEXT: %3 = comb.and %bEn, %bCond : i1
|
||||
// CHECK-NEXT: sv.assume.concurrent "assume_0" posedge %clock %3 : i1
|
||||
// CHECK-NEXT: sv.assume.concurrent posedge %clock, %3 label "assume_0"
|
||||
// CHECK-NEXT: %4 = comb.and %cEn, %cCond : i1
|
||||
// CHECK-NEXT: sv.cover.concurrent posedge %clock %4 : i1
|
||||
// CHECK-NEXT: sv.cover.concurrent posedge %clock, %4
|
||||
// CHECK-NEXT: %5 = comb.and %cEn, %cCond : i1
|
||||
// CHECK-NEXT: sv.cover.concurrent "cover_0" posedge %clock %5 : i1
|
||||
// CHECK: sv.cover.concurrent "cover_1" negedge %clock
|
||||
// CHECK: sv.cover.concurrent "cover_2" edge %clock
|
||||
// CHECK-NEXT: sv.cover.concurrent posedge %clock, %5 label "cover_0"
|
||||
// CHECK: sv.cover.concurrent negedge %clock, {{%.+}} label "cover_1"
|
||||
// CHECK: sv.cover.concurrent edge %clock, {{%.+}} label "cover_2"
|
||||
firrtl.assert %clock, %aCond, %aEn, "assert0" {isConcurrent = true}
|
||||
firrtl.assert %clock, %aCond, %aEn, "assert0" {isConcurrent = true, name = "assert_0"}
|
||||
firrtl.assume %clock, %bCond, %bEn, "assume0" {isConcurrent = true}
|
||||
|
|
@ -431,16 +431,19 @@ firrtl.circuit "Simple" attributes {annotations = [{class =
|
|||
|
||||
// CHECK-NEXT: sv.always posedge %clock {
|
||||
// CHECK-NEXT: sv.if %aEn {
|
||||
// CHECK-NEXT: sv.assert %aCond : i1
|
||||
// CHECK-NEXT: sv.assert "assert_0" %aCond : i1
|
||||
// CHECK-NEXT: sv.assert %aCond, immediate
|
||||
// CHECK-NOT: label
|
||||
// CHECK-NEXT: sv.assert %aCond, immediate label "assert_0"
|
||||
// CHECK-NEXT: }
|
||||
// CHECK-NEXT: sv.if %bEn {
|
||||
// CHECK-NEXT: sv.assume %bCond : i1
|
||||
// CHECK-NEXT: sv.assume "assume_0" %bCond : i1
|
||||
// CHECK-NEXT: sv.assume %bCond, immediate
|
||||
// CHECK-NOT: label
|
||||
// CHECK-NEXT: sv.assume %bCond, immediate label "assume_0"
|
||||
// CHECK-NEXT: }
|
||||
// CHECK-NEXT: sv.if %cEn {
|
||||
// CHECK-NEXT: sv.cover %cCond : i1
|
||||
// CHECK-NEXT: sv.cover "cover_0" %cCond : i1
|
||||
// CHECK-NEXT: sv.cover %cCond, immediate
|
||||
// CHECK-NOT: label
|
||||
// CHECK-NEXT: sv.cover %cCond, immediate label "cover_0"
|
||||
// CHECK-NEXT: }
|
||||
// CHECK-NEXT: }
|
||||
firrtl.assert %clock, %aCond, %aEn, "assert0"
|
||||
|
|
|
|||
|
|
@ -141,19 +141,19 @@ hw.module @Wire() {
|
|||
// -----
|
||||
hw.module @Assert(%arg0: i1) {
|
||||
// expected-error @+1 {{sv.assert should be in a procedural region}}
|
||||
sv.assert %arg0: i1
|
||||
sv.assert %arg0, immediate
|
||||
}
|
||||
|
||||
// -----
|
||||
hw.module @Assume(%arg0: i1) {
|
||||
// expected-error @+1 {{sv.assume should be in a procedural region}}
|
||||
sv.assume %arg0: i1
|
||||
sv.assume %arg0, immediate
|
||||
}
|
||||
|
||||
// -----
|
||||
hw.module @Cover(%arg0: i1) {
|
||||
// expected-error @+1 {{sv.cover should be in a procedural region}}
|
||||
sv.cover %arg0: i1
|
||||
sv.cover %arg0, immediate
|
||||
}
|
||||
|
||||
// -----
|
||||
|
|
@ -179,4 +179,4 @@ sv.bind @A in @InternSrcMod
|
|||
hw.module @test() {
|
||||
// expected-error @+1 {{op invalid parameter value @test}}
|
||||
%param_x = sv.localparam : i42 {value = @test}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -36,9 +36,9 @@ module attributes {firrtl.extract.assert = #hw.output_file<"dir3/", excludeFrom
|
|||
sv.ifdef.procedural "SYNTHESIS" {
|
||||
} else {
|
||||
sv.if %2937 {
|
||||
sv.assert %clock : i1
|
||||
sv.assume %clock : i1
|
||||
sv.cover %clock : i1
|
||||
sv.assert %clock, immediate
|
||||
sv.assume %clock, immediate
|
||||
sv.cover %clock, immediate
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -139,7 +139,7 @@ hw.module @verif_renames(%cond: i1) {
|
|||
// CHECK: initial
|
||||
sv.initial {
|
||||
// CHECK: assert_0: assert(cond);
|
||||
sv.assert "assert" %cond : i1
|
||||
sv.assert %cond, immediate label "assert"
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -144,19 +144,35 @@ hw.module @M1<param1: i42>(%clock : i1, %cond : i1, %val : i8) {
|
|||
sv.fwrite "Bye %x\n"(%tmp) : i8
|
||||
|
||||
// CHECK-NEXT: assert(cond);
|
||||
sv.assert %cond : i1
|
||||
sv.assert %cond, immediate
|
||||
// CHECK-NEXT: assert #0 (cond);
|
||||
sv.assert %cond, observed
|
||||
// CHECK-NEXT: assert final (cond);
|
||||
sv.assert %cond, final
|
||||
// CHECK-NEXT: assert_0: assert(cond);
|
||||
sv.assert "assert_0" %cond : i1
|
||||
sv.assert %cond, immediate label "assert_0"
|
||||
// CHECK-NEXT: assert(cond) else $error("expected %d", val);
|
||||
sv.assert %cond, immediate message "expected %d"(%val) : i8
|
||||
|
||||
// CHECK-NEXT: assume(cond);
|
||||
sv.assume %cond : i1
|
||||
sv.assume %cond, immediate
|
||||
// CHECK-NEXT: assume #0 (cond);
|
||||
sv.assume %cond, observed
|
||||
// CHECK-NEXT: assume final (cond);
|
||||
sv.assume %cond, final
|
||||
// CHECK-NEXT: assume_0: assume(cond);
|
||||
sv.assume "assume_0" %cond : i1
|
||||
sv.assume %cond, immediate label "assume_0"
|
||||
// CHECK-NEXT: assume(cond) else $error("expected %d", val);
|
||||
sv.assume %cond, immediate message "expected %d"(%val) : i8
|
||||
|
||||
// CHECK-NEXT: cover(cond);
|
||||
sv.cover %cond : i1
|
||||
sv.cover %cond, immediate
|
||||
// CHECK-NEXT: cover #0 (cond);
|
||||
sv.cover %cond, observed
|
||||
// CHECK-NEXT: cover final (cond);
|
||||
sv.cover %cond, final
|
||||
// CHECK-NEXT: cover_0: cover(cond);
|
||||
sv.cover "cover_0" %cond : i1
|
||||
sv.cover %cond, immediate label "cover_0"
|
||||
|
||||
// CHECK-NEXT: $fatal
|
||||
sv.fatal
|
||||
|
|
@ -183,19 +199,23 @@ hw.module @M1<param1: i42>(%clock : i1, %cond : i1, %val : i8) {
|
|||
// CHECK-NEXT: end // initial
|
||||
|
||||
// CHECK-NEXT: assert property (@(posedge clock) cond);
|
||||
sv.assert.concurrent posedge %clock %cond : i1
|
||||
sv.assert.concurrent posedge %clock, %cond
|
||||
// CHECK-NEXT: assert_1: assert property (@(posedge clock) cond);
|
||||
sv.assert.concurrent "assert_1" posedge %clock %cond : i1
|
||||
sv.assert.concurrent posedge %clock, %cond label "assert_1"
|
||||
// CHECK-NEXT: assert property (@(posedge clock) cond) else $error("expected %d", val);
|
||||
sv.assert.concurrent posedge %clock, %cond message "expected %d"(%val) : i8
|
||||
|
||||
// CHECK-NEXT: assume property (@(posedge clock) cond);
|
||||
sv.assume.concurrent posedge %clock %cond : i1
|
||||
sv.assume.concurrent posedge %clock, %cond
|
||||
// CHECK-NEXT: assume_1: assume property (@(posedge clock) cond);
|
||||
sv.assume.concurrent "assume_1" posedge %clock %cond : i1
|
||||
sv.assume.concurrent posedge %clock, %cond label "assume_1"
|
||||
// CHECK-NEXT: assume property (@(posedge clock) cond) else $error("expected %d", val);
|
||||
sv.assume.concurrent posedge %clock, %cond message "expected %d"(%val) : i8
|
||||
|
||||
// CHECK-NEXT: cover property (@(posedge clock) cond);
|
||||
sv.cover.concurrent posedge %clock %cond : i1
|
||||
sv.cover.concurrent posedge %clock, %cond
|
||||
// CHECK-NEXT: cover_1: cover property (@(posedge clock) cond);
|
||||
sv.cover.concurrent "cover_1" posedge %clock %cond : i1
|
||||
sv.cover.concurrent posedge %clock, %cond label "cover_1"
|
||||
|
||||
// CHECK-NEXT: initial
|
||||
// CHECK-NOT: begin
|
||||
|
|
@ -373,7 +393,7 @@ hw.module @issue595(%arr: !hw.array<128xi1>) {
|
|||
|
||||
sv.initial {
|
||||
// CHECK: assert(_T_0);
|
||||
sv.assert %0 : i1
|
||||
sv.assert %0, immediate
|
||||
}
|
||||
|
||||
// CHECK: wire [63:0] _T_1 = arr[7'h0+:64];
|
||||
|
|
@ -396,7 +416,7 @@ hw.module @issue595_variant1(%arr: !hw.array<128xi1>) {
|
|||
|
||||
sv.initial {
|
||||
// CHECK: assert(_T_0);
|
||||
sv.assert %0 : i1
|
||||
sv.assert %0, immediate
|
||||
}
|
||||
|
||||
// CHECK: wire [63:0] _T_1 = arr[7'h0+:64];
|
||||
|
|
@ -418,7 +438,7 @@ hw.module @issue595_variant2_checkRedunctionAnd(%arr: !hw.array<128xi1>) {
|
|||
|
||||
sv.initial {
|
||||
// CHECK: assert(_T_0);
|
||||
sv.assert %0 : i1
|
||||
sv.assert %0, immediate
|
||||
}
|
||||
|
||||
// CHECK: wire [63:0] _T_1 = arr[7'h0+:64];
|
||||
|
|
|
|||
|
|
@ -73,7 +73,7 @@ module {
|
|||
// CHECK: $fwrite(32'h80000002, "valid: %d\n", iface.valid);
|
||||
sv.fwrite "valid: %d\n" (%validValue) : i1
|
||||
// CHECK: assert(iface.valid);
|
||||
sv.assert %validValue : i1
|
||||
sv.assert %validValue, immediate
|
||||
|
||||
sv.if %clk {
|
||||
%structDataSignal = sv.interface.signal.read %structIface(@struct_vr::@data) : !hw.struct<foo: i7, bar: !hw.array<5 x i16>>
|
||||
|
|
|
|||
|
|
@ -9,9 +9,9 @@ hw.module @foo(%clock: i1, %cond: i1) {
|
|||
// CHECK-ON: assert_0: assert(
|
||||
// CHECK-ON: assume_1: assume(
|
||||
// CHECK-ON: cover_2: cover(
|
||||
sv.assert %cond : i1
|
||||
sv.assume %cond : i1
|
||||
sv.cover %cond : i1
|
||||
sv.assert %cond, immediate
|
||||
sv.assume %cond, immediate
|
||||
sv.cover %cond, immediate
|
||||
}
|
||||
// CHECK-OFF: assert property
|
||||
// CHECK-OFF: assume property
|
||||
|
|
@ -19,9 +19,9 @@ hw.module @foo(%clock: i1, %cond: i1) {
|
|||
// CHECK-ON: assert_3: assert property
|
||||
// CHECK-ON: assume_4: assume property
|
||||
// CHECK-ON: cover_5: cover property
|
||||
sv.assert.concurrent posedge %clock %cond : i1
|
||||
sv.assume.concurrent posedge %clock %cond : i1
|
||||
sv.cover.concurrent posedge %clock %cond : i1
|
||||
sv.assert.concurrent posedge %clock, %cond
|
||||
sv.assume.concurrent posedge %clock, %cond
|
||||
sv.cover.concurrent posedge %clock, %cond
|
||||
|
||||
// Explicitly labeled ops should keep their label.
|
||||
sv.initial {
|
||||
|
|
@ -31,9 +31,9 @@ hw.module @foo(%clock: i1, %cond: i1) {
|
|||
// CHECK-ON: imm_assume: assume(
|
||||
// CHECK-OFF: imm_cover: cover(
|
||||
// CHECK-ON: imm_cover: cover(
|
||||
sv.assert "imm_assert" %cond : i1
|
||||
sv.assume "imm_assume" %cond : i1
|
||||
sv.cover "imm_cover" %cond : i1
|
||||
sv.assert %cond, immediate label "imm_assert"
|
||||
sv.assume %cond, immediate label "imm_assume"
|
||||
sv.cover %cond, immediate label "imm_cover"
|
||||
}
|
||||
// CHECK-OFF: con_assert: assert property
|
||||
// CHECK-ON: con_assert: assert property
|
||||
|
|
@ -41,9 +41,9 @@ hw.module @foo(%clock: i1, %cond: i1) {
|
|||
// CHECK-ON: con_assume: assume property
|
||||
// CHECK-OFF: con_cover: cover property
|
||||
// CHECK-ON: con_cover: cover property
|
||||
sv.assert.concurrent "con_assert" posedge %clock %cond : i1
|
||||
sv.assume.concurrent "con_assume" posedge %clock %cond : i1
|
||||
sv.cover.concurrent "con_cover" posedge %clock %cond : i1
|
||||
sv.assert.concurrent posedge %clock, %cond label "con_assert"
|
||||
sv.assume.concurrent posedge %clock, %cond label "con_assume"
|
||||
sv.cover.concurrent posedge %clock, %cond label "con_cover"
|
||||
|
||||
// Explicitly labeled ops that conflict with implicit labels should force the
|
||||
// implicit labels to change, even if they appear earlier in the output.
|
||||
|
|
@ -54,9 +54,9 @@ hw.module @foo(%clock: i1, %cond: i1) {
|
|||
// CHECK-ON: assume_2: assume(
|
||||
// CHECK-OFF: cover_4: cover(
|
||||
// CHECK-ON: cover_4: cover(
|
||||
sv.assert "assert_0" %cond : i1
|
||||
sv.assume "assume_2" %cond : i1
|
||||
sv.cover "cover_4" %cond : i1
|
||||
sv.assert %cond, immediate label "assert_0"
|
||||
sv.assume %cond, immediate label "assume_2"
|
||||
sv.cover %cond, immediate label "cover_4"
|
||||
}
|
||||
// CHECK-OFF: assert_6: assert property
|
||||
// CHECK-ON: assert_6: assert property
|
||||
|
|
@ -64,7 +64,7 @@ hw.module @foo(%clock: i1, %cond: i1) {
|
|||
// CHECK-ON: assume_8: assume property
|
||||
// CHECK-OFF: cover_10: cover property
|
||||
// CHECK-ON: cover_10: cover property
|
||||
sv.assert.concurrent "assert_6" posedge %clock %cond : i1
|
||||
sv.assume.concurrent "assume_8" posedge %clock %cond : i1
|
||||
sv.cover.concurrent "cover_10" posedge %clock %cond : i1
|
||||
sv.assert.concurrent posedge %clock, %cond label "assert_6"
|
||||
sv.assume.concurrent posedge %clock, %cond label "assume_8"
|
||||
sv.cover.concurrent posedge %clock, %cond label "cover_10"
|
||||
}
|
||||
|
|
|
|||
Loading…
Reference in New Issue