diff --git a/include/circt/Dialect/SV/SV.td b/include/circt/Dialect/SV/SV.td index ae65162db3..d5ba1298e2 100644 --- a/include/circt/Dialect/SV/SV.td +++ b/include/circt/Dialect/SV/SV.td @@ -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 diff --git a/include/circt/Dialect/SV/SVStatements.td b/include/circt/Dialect/SV/SVStatements.td index d8848561ca..f3d76704c1 100644 --- a/include/circt/Dialect/SV/SVStatements.td +++ b/include/circt/Dialect/SV/SVStatements.td @@ -481,84 +481,9 @@ def VerbatimOp : SVOp<"verbatim"> { } //===----------------------------------------------------------------------===// -// Verification Statements +// Bind Statements //===----------------------------------------------------------------------===// -class ImmediateAssertionOp traits = []> : - SVOp { - let arguments = (ins I1:$expression, StrAttr:$label); - let results = (outs); - let assemblyFormat = - "custom($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 traits = []> : - SVOp { - let arguments = - (ins EventControlAttr:$event, I1:$clock, I1:$property, StrAttr:$label); - let results = (outs); - let assemblyFormat = - "custom($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 = [{ diff --git a/include/circt/Dialect/SV/SVVerification.td b/include/circt/Dialect/SV/SVVerification.td new file mode 100644 index 0000000000..88d6e79114 --- /dev/null +++ b/include/circt/Dialect/SV/SVVerification.td @@ -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 traits = []> : + SVOp { + let arguments = (ins + I1:$expression, + DeferAssertAttr:$defer, + OptionalAttr:$label, + OptionalAttr:$message, Variadic:$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 traits = []> : + SVOp { + let arguments = (ins + EventControlAttr:$event, I1:$clock, I1:$property, + OptionalAttr:$label, + OptionalAttr:$message, Variadic:$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. + }]; +} diff --git a/lib/Conversion/ExportVerilog/ExportVerilog.cpp b/lib/Conversion/ExportVerilog/ExportVerilog.cpp index 730d68bb66..ef73a42ef2 100644 --- a/lib/Conversion/ExportVerilog/ExportVerilog.cpp +++ b/lib/Conversion/ExportVerilog/ExportVerilog.cpp @@ -1943,8 +1943,7 @@ void NameCollector::collectNames(Block &block) { // Notice and renamify the labels on verification statements. if (isa(op)) { - auto labelAttr = op.getAttrOfType("label"); - if (!labelAttr.getValue().empty()) + if (auto labelAttr = op.getAttrOfType("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 &ops); + template + 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 + 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("label").getValue().empty()) { + if (op->getAttrOfType("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 &ops) { + if (!message) + return; + os << " else $error(\""; + os.write_escaped(message.getValue()); + os << "\""; + for (auto arg : args) { + os << ", "; + emitExpression(arg, ops); + } + os << ")"; +} + +template +LogicalResult StmtEmitter::emitImmediateAssertion(Op op, StringRef opName) { SmallPtrSet 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 +LogicalResult StmtEmitter::emitConcurrentAssertion(Op op, StringRef opName) { SmallPtrSet 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) { diff --git a/lib/Conversion/FIRRTLToHW/LowerToHW.cpp b/lib/Conversion/FIRRTLToHW/LowerToHW.cpp index 54b4978478..915fdefca5 100644 --- a/lib/Conversion/FIRRTLToHW/LowerToHW.cpp +++ b/lib/Conversion/FIRRTLToHW/LowerToHW.cpp @@ -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(predicate, label); + svOp = builder.create( + 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( circt::sv::EventControlAttr::get(builder.getContext(), event), clock, - predicate, label); + predicate, label, StringAttr{}, ValueRange{}); } return success(); } diff --git a/lib/Dialect/SV/SVOps.cpp b/lib/Dialect/SV/SVOps.cpp index d6b00d6664..2728c23caa 100644 --- a/lib/Dialect/SV/SVOps.cpp +++ b/lib/Dialect/SV/SVOps.cpp @@ -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(), - "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 //===----------------------------------------------------------------------===// diff --git a/test/Conversion/FIRRTLToHW/lower-to-hw.mlir b/test/Conversion/FIRRTLToHW/lower-to-hw.mlir index 33612647b4..b2200c3d1d 100644 --- a/test/Conversion/FIRRTLToHW/lower-to-hw.mlir +++ b/test/Conversion/FIRRTLToHW/lower-to-hw.mlir @@ -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" diff --git a/test/Dialect/SV/errors.mlir b/test/Dialect/SV/errors.mlir index 044b557a5c..2fbbada262 100644 --- a/test/Dialect/SV/errors.mlir +++ b/test/Dialect/SV/errors.mlir @@ -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} -} \ No newline at end of file +} diff --git a/test/Dialect/SV/hw-extract-test-code.mlir b/test/Dialect/SV/hw-extract-test-code.mlir index 095b2711bf..7e03abffc3 100644 --- a/test/Dialect/SV/hw-extract-test-code.mlir +++ b/test/Dialect/SV/hw-extract-test-code.mlir @@ -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 } } } diff --git a/test/ExportVerilog/name-legalize.mlir b/test/ExportVerilog/name-legalize.mlir index 5695097d1a..bbcaf3c775 100644 --- a/test/ExportVerilog/name-legalize.mlir +++ b/test/ExportVerilog/name-legalize.mlir @@ -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" } } diff --git a/test/ExportVerilog/sv-dialect.mlir b/test/ExportVerilog/sv-dialect.mlir index ac6ae26b45..ad0b1923bb 100644 --- a/test/ExportVerilog/sv-dialect.mlir +++ b/test/ExportVerilog/sv-dialect.mlir @@ -144,19 +144,35 @@ hw.module @M1(%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(%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]; diff --git a/test/ExportVerilog/sv-interfaces.mlir b/test/ExportVerilog/sv-interfaces.mlir index db3bca18e2..001ec66500 100644 --- a/test/ExportVerilog/sv-interfaces.mlir +++ b/test/ExportVerilog/sv-interfaces.mlir @@ -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> diff --git a/test/ExportVerilog/sv-verifLabels.mlir b/test/ExportVerilog/sv-verifLabels.mlir index 64a9d65b1e..c1df0ee9e6 100644 --- a/test/ExportVerilog/sv-verifLabels.mlir +++ b/test/ExportVerilog/sv-verifLabels.mlir @@ -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" }