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

[LowerToHW] Emission Option for verification flavors (#6885) 

This commits replaces `--emit-chisel-asserts-as-sva` with an option with more fine grained control.
Specifically an option `--verification-flavor={none, if-else-fatal, immediate, sva}` is added. `none` is the option for the current behaviour that uses per-op configuration (which must be deprecated once after `has_been_reset` is properly used for assertions that are expected to be disabled while pre-resets). 

Close https://github.com/llvm/circt/issues/6543
This commit is contained in:
Hideto Ueno 2024-04-02 14:09:38 +09:00 committed by GitHub
parent e55c5d56a6
commit de58c5f911
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
11 changed files with 182 additions and 94 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
include/circt-c/Firtool/Firtool.h
View File

@ -60,6 +60,14 @@ typedef enum CirctFirtoolRandomKind {
CIRCT_FIRTOOL_RANDOM_KIND_ALL,
} CirctFirtoolRandomKind;
// NOLINTNEXTLINE(modernize-use-using)
typedef enum CirctFirtoolVerificationFlavor {
CIRCT_FIRTOOL_VERIFICATION_FLAVOR_NONE,
CIRCT_FIRTOOL_VERIFICATION_FLAVOR_IF_ELSE_FATAL,
CIRCT_FIRTOOL_VERIFICATION_FLAVOR_IMMEDIATE,
CIRCT_FIRTOOL_VERIFICATION_FLAVOR_SVA,
} CirctFirtoolVerificationFlavor;
MLIR_CAPI_EXPORTED CirctFirtoolFirtoolOptions
circtFirtoolOptionsCreateDefault(void);
MLIR_CAPI_EXPORTED void
@ -166,8 +174,8 @@ circtFirtoolOptionsSetAddMuxPragmas(CirctFirtoolFirtoolOptions options,
bool value);
MLIR_CAPI_EXPORTED void
circtFirtoolOptionsSetEmitChiselAssertsAsSVA(CirctFirtoolFirtoolOptions options,
bool value);
circtFirtoolOptionsSetVerificationFlavor(CirctFirtoolFirtoolOptions options,
CirctFirtoolVerificationFlavor value);
MLIR_CAPI_EXPORTED void circtFirtoolOptionsSetEmitSeparateAlwaysBlocks(
CirctFirtoolFirtoolOptions options, bool value);

16
include/circt/Conversion/FIRRTLToHW.h
View File

@ -22,10 +22,24 @@ class Pass;
} // namespace mlir
namespace circt {
namespace firrtl {
enum class VerificationFlavor {
// Use the flavor specified by the op.
// TOOD: Drop this option once the migration finished.
None,
// Use `if(cond) else $fatal(..)` format.
IfElseFatal,
// Use immediate form.
Immediate,
// Use SVA.
SVA
};
} // namespace firrtl
std::unique_ptr<mlir::Pass>
createLowerFIRRTLToHWPass(bool enableAnnotationWarning = false,
bool emitChiselAssertsAsSVA = false);
firrtl::VerificationFlavor assertionFlavor =
firrtl::VerificationFlavor::None);
} // namespace circt

16
include/circt/Conversion/Passes.td
View File

@ -438,8 +438,20 @@ def LowerFIRRTLToHW : Pass<"lower-firrtl-to-hw", "mlir::ModuleOp"> {
Option<"enableAnnotationWarning", "warn-on-unprocessed-annotations",
"bool", "false",
"Emit warnings on unprocessed annotations during lower-to-hw pass">,
Option<"emitChiselAssertsAsSVA", "emit-chisel-asserts-as-sva",
"bool", "false","Convert all Chisel asserts to SVA">
Option<"verificationFlavor", "verification-flavor",
"circt::firrtl::VerificationFlavor",
"circt::firrtl::VerificationFlavor::None",
"Specify a verification flavor used in the lowering",
[{::llvm::cl::values(
clEnumValN(circt::firrtl::VerificationFlavor::None,
"none", "Use the flavor specified by the op"),
clEnumValN(circt::firrtl::VerificationFlavor::IfElseFatal,
"if-else-fatal", "Use Use `if(cond) else $fatal(..)` format"),
clEnumValN(circt::firrtl::VerificationFlavor::Immediate,
"immediate", "Use immediate verif statements"),
clEnumValN(circt::firrtl::VerificationFlavor::SVA, "sva", "Use SVA")
)}]
>
];
}

9
include/circt/Firtool/Firtool.h
View File

@ -13,6 +13,7 @@
#ifndef CIRCT_FIRTOOL_FIRTOOL_H
#define CIRCT_FIRTOOL_FIRTOOL_H
#include "circt/Conversion/Passes.h"
#include "circt/Dialect/FIRRTL/Passes.h"
#include "circt/Dialect/Seq/SeqPasses.h"
#include "circt/Support/LLVM.h"
@ -119,7 +120,7 @@ public:
return disableAggressiveMergeConnections;
}
bool shouldEnableAnnotationWarning() const { return enableAnnotationWarning; }
bool shouldEmitChiselAssertsAsSVA() const { return emitChiselAssertsAsSVA; }
auto getVerificationFlavor() const { return verificationFlavor; }
bool shouldEmitSeparateAlwaysBlocks() const {
return emitSeparateAlwaysBlocks;
}
@ -274,8 +275,8 @@ public:
return *this;
}
FirtoolOptions &setEmitChiselAssertsAsSVA(bool value) {
emitChiselAssertsAsSVA = value;
FirtoolOptions &setVerificationFlavor(firrtl::VerificationFlavor value) {
verificationFlavor = value;
return *this;
}
@ -384,7 +385,7 @@ private:
std::string outputAnnotationFilename;
bool enableAnnotationWarning;
bool addMuxPragmas;
bool emitChiselAssertsAsSVA;
firrtl::VerificationFlavor verificationFlavor;
bool emitSeparateAlwaysBlocks;
bool etcDisableInstanceExtraction;
bool etcDisableRegisterExtraction;

6
lib/CAPI/Firtool/Firtool.cpp
View File

@ -253,9 +253,9 @@ void circtFirtoolOptionsSetAddMuxPragmas(CirctFirtoolFirtoolOptions options,
unwrap(options)->setAddMuxPragmas(value);
}
void circtFirtoolOptionsSetEmitChiselAssertsAsSVA(
CirctFirtoolFirtoolOptions options, bool value) {
unwrap(options)->setEmitChiselAssertsAsSVA(value);
void circtFirtoolOptionsSetVerificationFlavor(
CirctFirtoolFirtoolOptions options, firrtl::VerificationFlavor value) {
unwrap(options)->setVerificationFlavor(value);
}
void circtFirtoolOptionsSetEmitSeparateAlwaysBlocks(

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

@ -215,11 +215,11 @@ struct CircuitLoweringState {
std::atomic<bool> usedStopCond{false};
CircuitLoweringState(CircuitOp circuitOp, bool enableAnnotationWarning,
bool emitChiselAssertsAsSVA,
firrtl::VerificationFlavor verificationFlavor,
InstanceGraph &instanceGraph, NLATable *nlaTable)
: circuitOp(circuitOp), instanceGraph(instanceGraph),
enableAnnotationWarning(enableAnnotationWarning),
emitChiselAssertsAsSVA(emitChiselAssertsAsSVA), nlaTable(nlaTable) {
verificationFlavor(verificationFlavor), nlaTable(nlaTable) {
auto *context = circuitOp.getContext();
// Get the testbench output directory.
@ -369,7 +369,7 @@ private:
const bool enableAnnotationWarning;
std::mutex annotationPrintingMtx;
const bool emitChiselAssertsAsSVA;
const firrtl::VerificationFlavor verificationFlavor;
// Records any sv::BindOps that are found during the course of execution.
// This is unsafe to access directly and should only be used through addBind.
@ -549,7 +549,8 @@ struct FIRRTLModuleLowering : public LowerFIRRTLToHWBase<FIRRTLModuleLowering> {
void runOnOperation() override;
void setEnableAnnotationWarning() { enableAnnotationWarning = true; }
void setEmitChiselAssertAsSVA() { emitChiselAssertsAsSVA = true; }
using LowerFIRRTLToHWBase<FIRRTLModuleLowering>::verificationFlavor;
private:
void lowerFileHeader(CircuitOp op, CircuitLoweringState &loweringState);
@ -578,14 +579,13 @@ private:
} // end anonymous namespace
/// This is the pass constructor.
std::unique_ptr<mlir::Pass>
circt::createLowerFIRRTLToHWPass(bool enableAnnotationWarning,
bool emitChiselAssertsAsSVA) {
std::unique_ptr<mlir::Pass> circt::createLowerFIRRTLToHWPass(
bool enableAnnotationWarning,
firrtl::VerificationFlavor verificationFlavor) {
auto pass = std::make_unique<FIRRTLModuleLowering>();
if (enableAnnotationWarning)
pass->setEnableAnnotationWarning();
if (emitChiselAssertsAsSVA)
pass->setEmitChiselAssertAsSVA();
pass->verificationFlavor = verificationFlavor;
return pass;
}
@ -611,9 +611,9 @@ void FIRRTLModuleLowering::runOnOperation() {
// Keep track of the mapping from old to new modules. The result may be null
// if lowering failed.
CircuitLoweringState state(
circuit, enableAnnotationWarning, emitChiselAssertsAsSVA,
getAnalysis<InstanceGraph>(), &getAnalysis<NLATable>());
CircuitLoweringState state(circuit, enableAnnotationWarning,
verificationFlavor, getAnalysis<InstanceGraph>(),
&getAnalysis<NLATable>());
SmallVector<hw::HWModuleOp, 32> modulesToProcess;
@ -4397,6 +4397,29 @@ LogicalResult FIRRTLLowering::lowerVerificationStatement(
StringAttr message;
SmallVector<Value> messageOps;
VerificationFlavor flavor = circuitState.verificationFlavor;
// For non-assertion, rollback to per-op configuration.
if (flavor == VerificationFlavor::IfElseFatal && !isa<AssertOp>(op))
flavor = VerificationFlavor::None;
if (flavor == VerificationFlavor::None) {
// TODO: This should *not* be part of the op, but rather a lowering
// option that the user of this pass can choose.
auto format = op->getAttrOfType<StringAttr>("format");
// if-else-fatal iff concurrent and the format is specified.
if (isConcurrent && format && format.getValue() == "ifElseFatal") {
if (!isa<AssertOp>(op))
return op->emitError()
<< "ifElseFatal format cannot be used for non-assertions";
flavor = VerificationFlavor::IfElseFatal;
} else if (isConcurrent)
flavor = VerificationFlavor::SVA;
else
flavor = VerificationFlavor::Immediate;
}
if (!isCover && opMessageAttr && !opMessageAttr.getValue().empty()) {
message = opMessageAttr;
for (auto operand : opOperands) {
@ -4407,22 +4430,20 @@ LogicalResult FIRRTLLowering::lowerVerificationStatement(
return failure();
loweredValue = getOrCreateIntConstant(1, 0);
}
// Wrap any message ops in $sampled() to guarantee that these will print
// with the same value as when the assertion triggers. (See SystemVerilog
// 2017 spec section 16.9.3 for more information.) The custom
// "ifElseFatal" variant is special cased because this isn't actually a
// concurrent assertion.
auto format = op->getAttrOfType<StringAttr>("format");
if (isConcurrent && (!format || format.getValue() != "ifElseFatal" ||
circuitState.emitChiselAssertsAsSVA))
// For SVA assert/assume statements, wrap any message ops in $sampled() to
// guarantee that these will print with the same value as when the
// assertion triggers. (See SystemVerilog 2017 spec section 16.9.3 for
// more information.)
if (flavor == VerificationFlavor::SVA)
loweredValue = builder.create<sv::SampledOp>(loweredValue);
messageOps.push_back(loweredValue);
}
}
auto emit = [&]() {
// Handle the purely procedural flavor of the operation.
if (!isConcurrent && !circuitState.emitChiselAssertsAsSVA) {
switch (flavor) {
case VerificationFlavor::Immediate: {
// Handle the purely procedural flavor of the operation.
auto deferImmediate = circt::sv::DeferAssertAttr::get(
builder.getContext(), circt::sv::DeferAssert::Immediate);
addToAlwaysBlock(clock, [&]() {
@ -4433,16 +4454,11 @@ LogicalResult FIRRTLLowering::lowerVerificationStatement(
});
return;
}
auto boolType = IntegerType::get(builder.getContext(), 1);
// Handle the `ifElseFatal` format, which does not emit an SVA but
// rather a process that uses $error and $fatal to perform the checks.
// TODO: This should *not* be part of the op, but rather a lowering
// option that the user of this pass can choose.
auto format = op->template getAttrOfType<StringAttr>("format");
if (format && (format.getValue() == "ifElseFatal" &&
!circuitState.emitChiselAssertsAsSVA)) {
case VerificationFlavor::IfElseFatal: {
assert(isa<AssertOp>(op) && "only assert is expected");
// Handle the `ifElseFatal` format, which does not emit an SVA but
// rather a process that uses $error and $fatal to perform the checks.
auto boolType = IntegerType::get(builder.getContext(), 1);
predicate = comb::createOrFoldNot(predicate, builder, /*twoState=*/true);
predicate = builder.createOrFold<comb::AndOp>(enable, predicate, true);
@ -4468,35 +4484,42 @@ LogicalResult FIRRTLLowering::lowerVerificationStatement(
});
return;
}
case VerificationFlavor::SVA: {
// Formulate the `enable -> predicate` as `!enable | predicate`.
// Except for covers, combine them: enable & predicate
if (!isCover) {
auto notEnable =
comb::createOrFoldNot(enable, builder, /*twoState=*/true);
predicate =
builder.createOrFold<comb::OrOp>(notEnable, predicate, true);
} else {
predicate = builder.createOrFold<comb::AndOp>(enable, predicate, true);
}
// Formulate the `enable -> predicate` as `!enable | predicate`.
// Except for covers, combine them: enable & predicate
if (!isCover) {
auto notEnable =
comb::createOrFoldNot(enable, builder, /*twoState=*/true);
predicate = builder.createOrFold<comb::OrOp>(notEnable, predicate, true);
} else {
predicate = builder.createOrFold<comb::AndOp>(enable, predicate, true);
// Handle the regular SVA case.
sv::EventControl event;
switch (opEventControl) {
case EventControl::AtPosEdge:
event = circt::sv::EventControl::AtPosEdge;
break;
case EventControl::AtEdge:
event = circt::sv::EventControl::AtEdge;
break;
case EventControl::AtNegEdge:
event = circt::sv::EventControl::AtNegEdge;
break;
}
buildConcurrentVerifOp(
builder, opName,
circt::sv::EventControlAttr::get(builder.getContext(), event), clock,
predicate, prefixedLabel, message, messageOps);
return;
}
// Handle the regular SVA case.
sv::EventControl event;
switch (opEventControl) {
case EventControl::AtPosEdge:
event = circt::sv::EventControl::AtPosEdge;
break;
case EventControl::AtEdge:
event = circt::sv::EventControl::AtEdge;
break;
case EventControl::AtNegEdge:
event = circt::sv::EventControl::AtNegEdge;
break;
case VerificationFlavor::None:
llvm_unreachable(
"flavor `None` must be converted into one of concreate flavors");
}
buildConcurrentVerifOp(
builder, opName,
circt::sv::EventControlAttr::get(builder.getContext(), event), clock,
predicate, prefixedLabel, message, messageOps);
};
// Wrap the verification statement up in the optional preprocessor

1
lib/Conversion/PassDetail.h
View File

@ -10,6 +10,7 @@
#ifndef CONVERSION_PASSDETAIL_H
#define CONVERSION_PASSDETAIL_H
#include "circt/Conversion/FIRRTLToHW.h"
#include "circt/Support/LoweringOptions.h"
#include "mlir/IR/BuiltinOps.h"
#include "mlir/IR/DialectRegistry.h"

26
lib/Firtool/Firtool.cpp
View File

@ -247,7 +247,7 @@ LogicalResult firtool::populateLowFIRRTLToHW(mlir::PassManager &pm,
circt::firrtl::createLintingPass());
pm.addPass(createLowerFIRRTLToHWPass(opt.shouldEnableAnnotationWarning(),
opt.shouldEmitChiselAssertsAsSVA()));
opt.getVerificationFlavor()));
if (!opt.shouldDisableOptimization()) {
auto &modulePM = pm.nest<hw::HWModuleOp>();
@ -583,10 +583,18 @@ struct FirtoolCmdOptions {
llvm::cl::desc("Annotate mux pragmas for memory array access"),
llvm::cl::init(false)};
llvm::cl::opt<bool> emitChiselAssertsAsSVA{
"emit-chisel-asserts-as-sva",
llvm::cl::desc("Convert all chisel asserts into SVA"),
llvm::cl::init(false)};
llvm::cl::opt<firrtl::VerificationFlavor> verificationFlavor{
"verification-flavor",
llvm::cl::desc("Specify a verification flavor used in LowerFIRRTLToHW"),
llvm::cl::values(
clEnumValN(firrtl::VerificationFlavor::None, "none",
"Use the flavor specified by the op"),
clEnumValN(firrtl::VerificationFlavor::IfElseFatal, "if-else-fatal",
"Use Use `if(cond) else $fatal(..)` format"),
clEnumValN(firrtl::VerificationFlavor::Immediate, "immediate",
"Use immediate verif statements"),
clEnumValN(firrtl::VerificationFlavor::SVA, "sva", "Use SVA")),
llvm::cl::init(firrtl::VerificationFlavor::None)};
llvm::cl::opt<bool> emitSeparateAlwaysBlocks{
"emit-separate-always-blocks",
@ -697,9 +705,9 @@ circt::firtool::FirtoolOptions::FirtoolOptions()
replSeqMemFile(""), extractTestCode(false), ignoreReadEnableMem(false),
disableRandom(RandomKind::None), outputAnnotationFilename(""),
enableAnnotationWarning(false), addMuxPragmas(false),
emitChiselAssertsAsSVA(false), emitSeparateAlwaysBlocks(false),
etcDisableInstanceExtraction(false), etcDisableRegisterExtraction(false),
etcDisableModuleInlining(false),
verificationFlavor(firrtl::VerificationFlavor::None),
emitSeparateAlwaysBlocks(false), etcDisableInstanceExtraction(false),
etcDisableRegisterExtraction(false), etcDisableModuleInlining(false),
addVivadoRAMAddressConflictSynthesisBugWorkaround(false),
ckgModuleName("EICG_wrapper"), ckgInputName("in"), ckgOutputName("out"),
ckgEnableName("en"), ckgTestEnableName("test_en"), ckgInstName("ckg"),
@ -737,7 +745,7 @@ circt::firtool::FirtoolOptions::FirtoolOptions()
outputAnnotationFilename = clOptions->outputAnnotationFilename;
enableAnnotationWarning = clOptions->enableAnnotationWarning;
addMuxPragmas = clOptions->addMuxPragmas;
emitChiselAssertsAsSVA = clOptions->emitChiselAssertsAsSVA;
verificationFlavor = clOptions->verificationFlavor;
emitSeparateAlwaysBlocks = clOptions->emitSeparateAlwaysBlocks;
etcDisableInstanceExtraction = clOptions->etcDisableInstanceExtraction;
etcDisableRegisterExtraction = clOptions->etcDisableRegisterExtraction;

39
test/Conversion/FIRRTLToHW/emit-chisel-asserts-as-sva.mlir
View File

@ -1,4 +1,7 @@
// RUN: circt-opt -lower-firrtl-to-hw=emit-chisel-asserts-as-sva %s | FileCheck %s
// RUN: circt-opt --pass-pipeline='builtin.module(lower-firrtl-to-hw{verification-flavor=sva})' %s | FileCheck %s --check-prefixes=CHECK,SVA
// RUN: circt-opt --pass-pipeline='builtin.module(lower-firrtl-to-hw{verification-flavor=if-else-fatal})' %s | FileCheck %s --check-prefixes=CHECK,IF_ELSE_FATAL
// RUN: circt-opt --pass-pipeline='builtin.module(lower-firrtl-to-hw{verification-flavor=immediate})' %s | FileCheck %s --check-prefixes=CHECK,IMMEDIATE
firrtl.circuit "ifElseFatalToSVA" {
// CHECK-LABEL: hw.module @ifElseFatalToSVA
@ -10,20 +13,26 @@ firrtl.circuit "ifElseFatalToSVA" {
firrtl.assert %clock, %cond, %enable, "assert0" : !firrtl.clock, !firrtl.uint<1>, !firrtl.uint<1> {isConcurrent = true, format = "ifElseFatal"}
firrtl.assume %clock, %cond, %enable, "assert0" : !firrtl.clock, !firrtl.uint<1>, !firrtl.uint<1> {isConcurrent = true, guards = ["USE_PROPERTY_AS_CONSTRAINT"]}
// CHECK-NEXT: [[CLK:%.+]] = seq.from_clock %clock
// CHECK-NEXT: [[TRUE:%.+]] = hw.constant true
// CHECK-NEXT: [[TMP1:%.+]] = comb.xor bin %enable, [[TRUE]]
// CHECK-NEXT: [[TMP2:%.+]] = comb.or bin [[TMP1]], %cond
// CHECK-NEXT: sv.assert.concurrent posedge [[CLK]], [[TMP2]] message "assert0"
// CHECK-NEXT: sv.ifdef @USE_PROPERTY_AS_CONSTRAINT {
// CHECK-NEXT: [[TRUE:%.+]] = hw.constant true
// CHECK-NEXT: [[TMP1:%.+]] = comb.xor bin %enable, [[TRUE]]
// CHECK-NEXT: [[TMP2:%.+]] = comb.or bin [[TMP1]], %cond
// CHECK-NEXT: sv.assume.concurrent posedge [[CLK]], [[TMP2]]
// CHECK-NEXT: }
// SVA: sv.assert.concurrent posedge [[CLK]], {{%.+}} message "assert0"
// IF_ELSE_FATAL: sv.always posedge [[CLK]] {
// IF_ELSE_FATAL-NEXT: sv.if {{%.+}} {
// IF_ELSE_FATAL-NEXT: %ASSERT_VERBOSE_COND_ = sv.macro.ref @ASSERT_VERBOSE_COND_()
// IF_ELSE_FATAL-NEXT: sv.if %ASSERT_VERBOSE_COND_ {
// IF_ELSE_FATAL-NEXT: sv.error "assert0"
// IF_ELSE_FATAL-NEXT: }
// IMMEDIATE: sv.always posedge [[CLK]] {
// IMMEDIATE-NEXT: sv.if %enable {
// IMMEDIATE-NEXT: sv.assert %cond, immediate message "assert0"
// CHECK: sv.ifdef @USE_PROPERTY_AS_CONSTRAINT {
// SVA: sv.assume.concurrent posedge [[CLK]], {{%.+}}
// IF_ELSE_FATAL: sv.assume.concurrent posedge [[CLK]], {{%.+}}
// IMMEDIATE: sv.assume {{%.+}}
}
// Test that an immediate assertion is always converted to a concurrent
// assertion if the "emit-chisel-asserts-as-sva" option is enabled.
// Test that an immediate assertion is converted to an assertion with a specified flavor.
//
// CHECK-LABEL: hw.module @immediateToConcurrent
firrtl.module @immediateToConcurrent(
@ -32,6 +41,8 @@ firrtl.circuit "ifElseFatalToSVA" {
in %enable: !firrtl.uint<1>
) {
firrtl.assert %clock, %cond, %enable, "assert1" : !firrtl.clock, !firrtl.uint<1>, !firrtl.uint<1>
// CHECK: sv.assert.concurrent
// SVA: sv.assert.concurrent
// IF_ELSE_FATAL: sv.if
// IMMEDIATE: sv.assert
}
}

10
test/Conversion/FIRRTLToHW/lower-to-hw-errors.mlir
View File

@ -218,3 +218,13 @@ firrtl.circuit "InputSelfDriver" {
firrtl.connect %ip2_in, %ip2_in : !firrtl.uint<1>, !firrtl.uint<1>
}
}
// -----
firrtl.circuit "IfElseFatalOnAssume" {
firrtl.module @IfElseFatalOnAssume (in %clock: !firrtl.clock, in %pred: !firrtl.uint<1>, in %en: !firrtl.uint<1>) {
// expected-error @+2 {{ifElseFatal format cannot be used for non-assertions}}
// expected-error @below {{'firrtl.assume' op LowerToHW couldn't handle this operation}}
firrtl.assume %clock, %en, %pred, "foo" : !firrtl.clock, !firrtl.uint<1>, !firrtl.uint<1> {isConcurrent = true, format = "ifElseFatal"}
}
}

2
test/Dialect/FIRRTL/SFCTests/complex-asserts.fir
View File

@ -1,5 +1,5 @@
; RUN: firtool --verify-diagnostics --verilog %s --lowering-options=emittedLineLength=200 --add-companion-assume | FileCheck %s
; RUN: firtool --verify-diagnostics --verilog --emit-chisel-asserts-as-sva %s --lowering-options=emittedLineLength=200 --add-companion-assume | FileCheck %s --check-prefix=SVA
; RUN: firtool --verify-diagnostics --verilog --verification-flavor=sva %s --lowering-options=emittedLineLength=200 --add-companion-assume | FileCheck %s --check-prefix=SVA
; Tests extracted from:
; - test/scala/firrtl/extractverif/ExtractAssertsSpec.scala