mirror of https://github.com/llvm/circt.git
[ExportVerilog] Add LTL and Verif dialect support (#5256)
Add support for emitting the assert, assume, and cover ops from the `verif` dialect, and property and sequence expressions from the `ltl` dialect directly in ExportVerilog. In the future we may want to build up AST-like ops in the SV dialect for this, simplify ExportVerilog, and add a lowering from Verif/LTL to SV separately. Doing so would allow us to do more involved conversions and leverage more syntactic sugar upon emission, and would declutter ExportVerilog. In their current form the LTL and Verif dialects are simple enough to emit directly though, so this is what this commit does for now. The new `verif` assert-like ops can be used either in a procedural region, where they will emit as immediate `assert(x)` when possible, or a graph region like a module, where they will emit as `assert property`. We'll be able to add lowering options later to have more control over which flavor of assertions we want. The properties and sequences in Verilog form a separate kind of expression tree that doesn't really mix with boolean expressions all that much. Therefore, this commit introduces a new `PropertyEmitter` inspired by the `ExprEmitter` which handles property and sequence expression trees.
This commit is contained in:
Fabian Schuiki
GitHub
parent
1460774177
commit
eb5090b4ba
|
|
@ -18,8 +18,10 @@ add_circt_translation_library(CIRCTExportVerilog
|
|||
LINK_LIBS PUBLIC
|
||||
CIRCTComb
|
||||
CIRCTHW
|
||||
CIRCTSupport
|
||||
CIRCTLTL
|
||||
CIRCTSV
|
||||
CIRCTSupport
|
||||
CIRCTVerif
|
||||
MLIRIR
|
||||
MLIRPass
|
||||
MLIRSideEffectInterfaces
|
||||
|
|
|
|||
|
|
@ -24,9 +24,11 @@
|
|||
#include "circt/Dialect/HW/HWOps.h"
|
||||
#include "circt/Dialect/HW/HWTypes.h"
|
||||
#include "circt/Dialect/HW/HWVisitors.h"
|
||||
#include "circt/Dialect/LTL/LTLVisitors.h"
|
||||
#include "circt/Dialect/SV/SVAttributes.h"
|
||||
#include "circt/Dialect/SV/SVOps.h"
|
||||
#include "circt/Dialect/SV/SVVisitors.h"
|
||||
#include "circt/Dialect/Verif/VerifVisitors.h"
|
||||
#include "circt/Support/LLVM.h"
|
||||
#include "circt/Support/LoweringOptions.h"
|
||||
#include "circt/Support/Path.h"
|
||||
|
|
@ -649,7 +651,7 @@ enum class BlockStatementCount { Zero, One, TwoOrMore };
|
|||
static BlockStatementCount countStatements(Block &block) {
|
||||
unsigned numStatements = 0;
|
||||
block.walk([&](Operation *op) {
|
||||
if (isVerilogExpression(op))
|
||||
if (isVerilogExpression(op) || isa<ltl::LTLDialect>(op->getDialect()))
|
||||
return WalkResult::advance();
|
||||
numStatements +=
|
||||
TypeSwitch<Operation *, unsigned>(op)
|
||||
|
|
@ -1794,6 +1796,11 @@ public:
|
|||
/// of any emitted expressions in the specified set.
|
||||
ExprEmitter(ModuleEmitter &emitter,
|
||||
SmallPtrSetImpl<Operation *> &emittedExprs)
|
||||
: ExprEmitter(emitter, emittedExprs, tokens) {}
|
||||
|
||||
ExprEmitter(ModuleEmitter &emitter,
|
||||
SmallPtrSetImpl<Operation *> &emittedExprs,
|
||||
BufferingPP::BufferVec &tokens)
|
||||
: EmitterBase(emitter.state), emitter(emitter),
|
||||
emittedExprs(emittedExprs), buffer(tokens), ps(buffer, state.saver) {
|
||||
assert(state.pp.getListener() == &state.saver);
|
||||
|
|
@ -1811,7 +1818,11 @@ public:
|
|||
/*signRequirement*/ NoRequirement,
|
||||
/*isSelfDeterminedUnsignedValue*/ false);
|
||||
});
|
||||
buffer.flush(state.pp);
|
||||
// If we are not using an external token buffer provided through the
|
||||
// constructor, but we're using the default `ExprEmitter`-scoped buffer,
|
||||
// flush it.
|
||||
if (&buffer.tokens == &tokens)
|
||||
buffer.flush(state.pp);
|
||||
}
|
||||
|
||||
private:
|
||||
|
|
@ -2953,6 +2964,294 @@ SubExprInfo ExprEmitter::visitUnhandledExpr(Operation *op) {
|
|||
}
|
||||
// NOLINTEND(misc-no-recursion)
|
||||
|
||||
//===----------------------------------------------------------------------===//
|
||||
// Property Emission
|
||||
//===----------------------------------------------------------------------===//
|
||||
|
||||
// NOLINTBEGIN(misc-no-recursion)
|
||||
|
||||
namespace {
|
||||
/// Precedence level of various property and sequence expressions. Lower numbers
|
||||
/// bind tighter.
|
||||
///
|
||||
/// See IEEE 1800-2017 section 16.12 "Declaring properties", specifically table
|
||||
/// 16-3 on "Sequence and property operator precedence and associativity".
|
||||
enum class PropertyPrecedence {
|
||||
Symbol, // Atomic symbol like `foo` and regular boolean expressions
|
||||
Repeat, // Sequence `[*]`, `[=]`, `[->]`
|
||||
Concat, // Sequence `##`
|
||||
Throughout, // Sequence `throughout`
|
||||
Within, // Sequence `within`
|
||||
Intersect, // Sequence `intersect`
|
||||
Unary, // Property `not`, `nexttime`-like
|
||||
And, // Sequence and property `and`
|
||||
Or, // Sequence and property `or`
|
||||
Iff, // Property `iff`
|
||||
Until, // Property `until`-like, `implies`
|
||||
Implication, // Property `|->`, `|=>`, `#-#`, `#=#`
|
||||
Qualifier, // Property `always`-like, `eventually`-like, `if`, `case`,
|
||||
// `accept`-like, `reject`-like
|
||||
Clocking, // `@(...)`, `disable iff` (not specified in the standard)
|
||||
Lowest, // Sentinel which is always the lowest precedence.
|
||||
};
|
||||
|
||||
/// Additional information on emitted property and sequence expressions.
|
||||
struct EmittedProperty {
|
||||
/// The precedence of this expression.
|
||||
PropertyPrecedence precedence;
|
||||
};
|
||||
|
||||
/// A helper to emit recursively nested property and sequence expressions for
|
||||
/// SystemVerilog assertions.
|
||||
class PropertyEmitter : public EmitterBase,
|
||||
public ltl::Visitor<PropertyEmitter, EmittedProperty> {
|
||||
public:
|
||||
/// Create a PropertyEmitter for the specified module emitter, and keeping
|
||||
/// track of any emitted expressions in the specified set.
|
||||
PropertyEmitter(ModuleEmitter &emitter,
|
||||
SmallPtrSetImpl<Operation *> &emittedOps)
|
||||
: PropertyEmitter(emitter, emittedOps, tokens) {}
|
||||
PropertyEmitter(ModuleEmitter &emitter,
|
||||
SmallPtrSetImpl<Operation *> &emittedOps,
|
||||
BufferingPP::BufferVec &tokens)
|
||||
: EmitterBase(emitter.state), emitter(emitter), emittedOps(emittedOps),
|
||||
buffer(tokens), ps(buffer, state.saver) {
|
||||
assert(state.pp.getListener() == &state.saver);
|
||||
}
|
||||
|
||||
/// Emit the specified value as an SVA property or sequence. This is the entry
|
||||
/// point to print an entire tree of property or sequence expressions in one
|
||||
/// go.
|
||||
void emitProperty(
|
||||
Value property,
|
||||
PropertyPrecedence parenthesizeIfLooserThan = PropertyPrecedence::Lowest);
|
||||
|
||||
private:
|
||||
using ltl::Visitor<PropertyEmitter, EmittedProperty>::visitLTL;
|
||||
friend class ltl::Visitor<PropertyEmitter, EmittedProperty>;
|
||||
|
||||
/// Emit the specified value as an SVA property or sequence.
|
||||
EmittedProperty
|
||||
emitNestedProperty(Value property,
|
||||
PropertyPrecedence parenthesizeIfLooserThan);
|
||||
|
||||
EmittedProperty visitUnhandledLTL(Operation *op);
|
||||
EmittedProperty visitLTL(ltl::AndOp op);
|
||||
EmittedProperty visitLTL(ltl::OrOp op);
|
||||
EmittedProperty visitLTL(ltl::DelayOp op);
|
||||
EmittedProperty visitLTL(ltl::ConcatOp op);
|
||||
EmittedProperty visitLTL(ltl::NotOp op);
|
||||
EmittedProperty visitLTL(ltl::ImplicationOp op);
|
||||
EmittedProperty visitLTL(ltl::EventuallyOp op);
|
||||
EmittedProperty visitLTL(ltl::ClockOp op);
|
||||
EmittedProperty visitLTL(ltl::DisableOp op);
|
||||
|
||||
void emitLTLConcat(ValueRange inputs);
|
||||
|
||||
public:
|
||||
ModuleEmitter &emitter;
|
||||
|
||||
private:
|
||||
/// Keep track of all operations emitted within this subexpression for
|
||||
/// location information tracking.
|
||||
SmallPtrSetImpl<Operation *> &emittedOps;
|
||||
|
||||
/// Tokens buffered for inserting casts/parens after emitting children.
|
||||
SmallVector<Token> tokens;
|
||||
|
||||
/// Stores tokens until told to flush. Uses provided buffer (tokens).
|
||||
BufferingPP buffer;
|
||||
|
||||
/// Stream to emit expressions into, will add to buffer.
|
||||
TokenStream<BufferingPP> ps;
|
||||
};
|
||||
} // end anonymous namespace
|
||||
|
||||
void PropertyEmitter::emitProperty(
|
||||
Value property, PropertyPrecedence parenthesizeIfLooserThan) {
|
||||
assert(tokens.empty());
|
||||
// Wrap to this column.
|
||||
ps.scopedBox(PP::ibox0,
|
||||
[&] { emitNestedProperty(property, parenthesizeIfLooserThan); });
|
||||
// If we are not using an external token buffer provided through the
|
||||
// constructor, but we're using the default `PropertyEmitter`-scoped buffer,
|
||||
// flush it.
|
||||
if (&buffer.tokens == &tokens)
|
||||
buffer.flush(state.pp);
|
||||
}
|
||||
|
||||
EmittedProperty PropertyEmitter::emitNestedProperty(
|
||||
Value property, PropertyPrecedence parenthesizeIfLooserThan) {
|
||||
// Emit the property as a plain expression if it doesn't have a property or
|
||||
// sequence type, in which case it is just a boolean expression.
|
||||
//
|
||||
// We use the `LowestPrecedence` for the boolean expression such that it never
|
||||
// gets parenthesized. According to IEEE 1800-2017, "the operators described
|
||||
// in Table 11-2 have higher precedence than the sequence and property
|
||||
// operators". Therefore any boolean expression behaves just like a
|
||||
// `PropertyPrecedence::Symbol` and needs no parantheses, which is equivalent
|
||||
// to `VerilogPrecedence::LowestPrecedence`.
|
||||
if (!isa<ltl::SequenceType, ltl::PropertyType>(property.getType())) {
|
||||
ExprEmitter(emitter, emittedOps, tokens)
|
||||
.emitExpression(property, LowestPrecedence);
|
||||
return {PropertyPrecedence::Symbol};
|
||||
}
|
||||
|
||||
unsigned startIndex = tokens.size();
|
||||
auto info = dispatchLTLVisitor(property.getDefiningOp());
|
||||
|
||||
// If this subexpression would bind looser than the expression it is bound
|
||||
// into, then we need to parenthesize it. Insert the parentheses
|
||||
// retroactively.
|
||||
if (info.precedence > parenthesizeIfLooserThan) {
|
||||
// Insert {"(", ibox0} before the subexpression.
|
||||
tokens.insert(tokens.begin() + startIndex, BeginToken(0));
|
||||
tokens.insert(tokens.begin() + startIndex, StringToken("("));
|
||||
// Insert {end, ")" } after the subexpression.
|
||||
ps << PP::end << ")";
|
||||
// Reset the precedence level.
|
||||
info.precedence = PropertyPrecedence::Symbol;
|
||||
}
|
||||
|
||||
// Remember that we emitted this.
|
||||
emittedOps.insert(property.getDefiningOp());
|
||||
return info;
|
||||
}
|
||||
|
||||
EmittedProperty PropertyEmitter::visitUnhandledLTL(Operation *op) {
|
||||
emitOpError(op, "emission as Verilog property or sequence not supported");
|
||||
ps << "<<unsupported: " << PPExtString(op->getName().getStringRef()) << ">>";
|
||||
return {PropertyPrecedence::Symbol};
|
||||
}
|
||||
|
||||
EmittedProperty PropertyEmitter::visitLTL(ltl::AndOp op) {
|
||||
llvm::interleave(
|
||||
op.getInputs(),
|
||||
[&](auto input) { emitNestedProperty(input, PropertyPrecedence::And); },
|
||||
[&]() { ps << PP::space << "and" << PP::nbsp; });
|
||||
return {PropertyPrecedence::And};
|
||||
}
|
||||
|
||||
EmittedProperty PropertyEmitter::visitLTL(ltl::OrOp op) {
|
||||
llvm::interleave(
|
||||
op.getInputs(),
|
||||
[&](auto input) { emitNestedProperty(input, PropertyPrecedence::Or); },
|
||||
[&]() { ps << PP::space << "or" << PP::nbsp; });
|
||||
return {PropertyPrecedence::Or};
|
||||
}
|
||||
|
||||
EmittedProperty PropertyEmitter::visitLTL(ltl::DelayOp op) {
|
||||
ps << "##";
|
||||
if (auto length = op.getLength()) {
|
||||
if (*length == 0) {
|
||||
ps.addAsString(op.getDelay());
|
||||
} else {
|
||||
ps << "[";
|
||||
ps.addAsString(op.getDelay());
|
||||
ps << ":";
|
||||
ps.addAsString(op.getDelay() + *length);
|
||||
ps << "]";
|
||||
}
|
||||
} else {
|
||||
if (op.getDelay() == 0) {
|
||||
ps << "[*]";
|
||||
} else if (op.getDelay() == 1) {
|
||||
ps << "[+]";
|
||||
} else {
|
||||
ps << "[";
|
||||
ps.addAsString(op.getDelay());
|
||||
ps << ":$]";
|
||||
}
|
||||
}
|
||||
ps << PP::space;
|
||||
emitNestedProperty(op.getInput(), PropertyPrecedence::Concat);
|
||||
return {PropertyPrecedence::Concat};
|
||||
}
|
||||
|
||||
void PropertyEmitter::emitLTLConcat(ValueRange inputs) {
|
||||
bool addSeparator = false;
|
||||
for (auto input : inputs) {
|
||||
if (addSeparator) {
|
||||
ps << PP::space;
|
||||
if (!input.getDefiningOp<ltl::DelayOp>())
|
||||
ps << "##0" << PP::space;
|
||||
}
|
||||
addSeparator = true;
|
||||
emitNestedProperty(input, PropertyPrecedence::Concat);
|
||||
}
|
||||
}
|
||||
|
||||
EmittedProperty PropertyEmitter::visitLTL(ltl::ConcatOp op) {
|
||||
emitLTLConcat(op.getInputs());
|
||||
return {PropertyPrecedence::Concat};
|
||||
}
|
||||
|
||||
EmittedProperty PropertyEmitter::visitLTL(ltl::NotOp op) {
|
||||
ps << "not" << PP::space;
|
||||
emitNestedProperty(op.getInput(), PropertyPrecedence::Unary);
|
||||
return {PropertyPrecedence::Unary};
|
||||
}
|
||||
|
||||
/// For a value `concat(..., delay(const(true), 1, 0))`, return `...`. This is
|
||||
/// useful for emitting `(seq ##1 true) |-> prop` as `seq |=> prop`.
|
||||
static ValueRange getNonOverlappingConcatSubrange(Value value) {
|
||||
auto concatOp = value.getDefiningOp<ltl::ConcatOp>();
|
||||
if (!concatOp || concatOp.getInputs().size() < 2)
|
||||
return {};
|
||||
auto delayOp = concatOp.getInputs().back().getDefiningOp<ltl::DelayOp>();
|
||||
if (!delayOp || delayOp.getDelay() != 1 || delayOp.getLength() != 0)
|
||||
return {};
|
||||
auto constOp = delayOp.getInput().getDefiningOp<ConstantOp>();
|
||||
if (!constOp || !constOp.getValue().isOne())
|
||||
return {};
|
||||
return concatOp.getInputs().drop_back();
|
||||
}
|
||||
|
||||
EmittedProperty PropertyEmitter::visitLTL(ltl::ImplicationOp op) {
|
||||
// Emit `(seq ##1 true) |-> prop` as `seq |=> prop`.
|
||||
if (auto range = getNonOverlappingConcatSubrange(op.getAntecedent());
|
||||
!range.empty()) {
|
||||
emitLTLConcat(range);
|
||||
ps << PP::space << "|=>" << PP::nbsp;
|
||||
} else {
|
||||
emitNestedProperty(op.getAntecedent(), PropertyPrecedence::Implication);
|
||||
ps << PP::space << "|->" << PP::nbsp;
|
||||
}
|
||||
emitNestedProperty(op.getConsequent(), PropertyPrecedence::Implication);
|
||||
return {PropertyPrecedence::Implication};
|
||||
}
|
||||
|
||||
EmittedProperty PropertyEmitter::visitLTL(ltl::EventuallyOp op) {
|
||||
ps << "s_eventually" << PP::space;
|
||||
emitNestedProperty(op.getInput(), PropertyPrecedence::Qualifier);
|
||||
return {PropertyPrecedence::Qualifier};
|
||||
}
|
||||
|
||||
EmittedProperty PropertyEmitter::visitLTL(ltl::ClockOp op) {
|
||||
ps << "@(";
|
||||
ps.scopedBox(PP::ibox2, [&] {
|
||||
ps << PPExtString(stringifyClockEdge(op.getEdge())) << PP::space;
|
||||
emitNestedProperty(op.getClock(), PropertyPrecedence::Lowest);
|
||||
ps << ")";
|
||||
});
|
||||
ps << PP::space;
|
||||
emitNestedProperty(op.getInput(), PropertyPrecedence::Clocking);
|
||||
return {PropertyPrecedence::Clocking};
|
||||
}
|
||||
|
||||
EmittedProperty PropertyEmitter::visitLTL(ltl::DisableOp op) {
|
||||
ps << "disable iff" << PP::nbsp << "(";
|
||||
ps.scopedBox(PP::ibox2, [&] {
|
||||
emitNestedProperty(op.getCondition(), PropertyPrecedence::Lowest);
|
||||
ps << ")";
|
||||
});
|
||||
ps << PP::space;
|
||||
emitNestedProperty(op.getInput(), PropertyPrecedence::Clocking);
|
||||
return {PropertyPrecedence::Clocking};
|
||||
}
|
||||
|
||||
// NOLINTEND(misc-no-recursion)
|
||||
|
||||
//===----------------------------------------------------------------------===//
|
||||
// NameCollector
|
||||
//===----------------------------------------------------------------------===//
|
||||
|
|
@ -2985,6 +3284,8 @@ void NameCollector::collectNames(Block &block) {
|
|||
// anyway.
|
||||
if (isa<InstanceOp, InterfaceInstanceOp>(op))
|
||||
continue;
|
||||
if (isa<ltl::LTLDialect>(op.getDialect()))
|
||||
continue;
|
||||
|
||||
bool isExpr = isVerilogExpression(&op);
|
||||
assert((!isExpr ||
|
||||
|
|
@ -3039,7 +3340,8 @@ namespace {
|
|||
// NOLINTBEGIN(misc-no-recursion)
|
||||
class StmtEmitter : public EmitterBase,
|
||||
public hw::StmtVisitor<StmtEmitter, LogicalResult>,
|
||||
public sv::Visitor<StmtEmitter, LogicalResult> {
|
||||
public sv::Visitor<StmtEmitter, LogicalResult>,
|
||||
public verif::Visitor<StmtEmitter, LogicalResult> {
|
||||
public:
|
||||
/// Create an ExprEmitter for the specified module emitter, and keeping track
|
||||
/// of any emitted expressions in the specified set.
|
||||
|
|
@ -3060,16 +3362,20 @@ private:
|
|||
VerilogPrecedence parenthesizeIfLooserThan = LowestPrecedence);
|
||||
void emitSVAttributes(Operation *op);
|
||||
|
||||
using StmtVisitor::visitStmt;
|
||||
using Visitor::visitSV;
|
||||
using hw::StmtVisitor<StmtEmitter, LogicalResult>::visitStmt;
|
||||
using sv::Visitor<StmtEmitter, LogicalResult>::visitSV;
|
||||
using verif::Visitor<StmtEmitter, LogicalResult>::visitVerif;
|
||||
friend class hw::StmtVisitor<StmtEmitter, LogicalResult>;
|
||||
friend class sv::Visitor<StmtEmitter, LogicalResult>;
|
||||
friend class verif::Visitor<StmtEmitter, LogicalResult>;
|
||||
|
||||
// Visitor methods.
|
||||
LogicalResult visitUnhandledStmt(Operation *op) { return failure(); }
|
||||
LogicalResult visitInvalidStmt(Operation *op) { return failure(); }
|
||||
LogicalResult visitUnhandledSV(Operation *op) { return failure(); }
|
||||
LogicalResult visitInvalidSV(Operation *op) { return failure(); }
|
||||
LogicalResult visitUnhandledVerif(Operation *op) { return failure(); }
|
||||
LogicalResult visitInvalidVerif(Operation *op) { return failure(); }
|
||||
|
||||
LogicalResult visitSV(sv::WireOp op) { return emitDeclaration(op); }
|
||||
LogicalResult visitSV(RegOp op) { return emitDeclaration(op); }
|
||||
|
|
@ -3159,6 +3465,12 @@ private:
|
|||
const SmallPtrSetImpl<Operation *> &locationOps,
|
||||
StringRef multiLineComment = StringRef());
|
||||
|
||||
LogicalResult emitVerifAssertLike(Operation *op, Value property,
|
||||
PPExtString opName);
|
||||
LogicalResult visitVerif(verif::AssertOp op);
|
||||
LogicalResult visitVerif(verif::AssumeOp op);
|
||||
LogicalResult visitVerif(verif::CoverOp op);
|
||||
|
||||
public:
|
||||
ModuleEmitter &emitter;
|
||||
|
||||
|
|
@ -3863,6 +4175,57 @@ LogicalResult StmtEmitter::visitSV(CoverConcurrentOp op) {
|
|||
return emitConcurrentAssertion(op, PPExtString("cover"));
|
||||
}
|
||||
|
||||
/// Emit an assert-like operation from the `verif` dialect. This covers
|
||||
/// `verif.assert`, `verif.assume`, and `verif.cover`.
|
||||
LogicalResult StmtEmitter::emitVerifAssertLike(Operation *op, Value property,
|
||||
PPExtString opName) {
|
||||
if (hasSVAttributes(op))
|
||||
emitError(op, "SV attributes emission is unimplemented for the op");
|
||||
|
||||
// If we are inside a procedural region we have the option of emitting either
|
||||
// an `assert` or `assert property`. If we are in a non-procedural region,
|
||||
// e.g., the body of a module, we have to use the concurrent form `assert
|
||||
// property` (which also supports plain booleans).
|
||||
//
|
||||
// See IEEE 1800-2017 section 16.14.5 "Using concurrent assertion statements
|
||||
// outside procedural code" and 16.14.6 "Embedding concurrent assertions in
|
||||
// procedural code".
|
||||
bool isTemporal = !property.getType().isSignlessInteger(1);
|
||||
bool isProcedural = op->getParentOp()->hasTrait<ProceduralRegion>();
|
||||
bool emitAsImmediate = !isTemporal && isProcedural;
|
||||
|
||||
startStatement();
|
||||
SmallPtrSet<Operation *, 8> ops;
|
||||
ops.insert(op);
|
||||
ps.scopedBox(PP::ibox2, [&]() {
|
||||
emitAssertionLabel(op, opName.str);
|
||||
ps.scopedBox(PP::cbox0, [&]() {
|
||||
if (emitAsImmediate)
|
||||
ps << opName << "(";
|
||||
else
|
||||
ps << opName << PP::nbsp << "property" << PP::nbsp << "(";
|
||||
ps.scopedBox(PP::ibox2, [&]() {
|
||||
PropertyEmitter(emitter, ops).emitProperty(property);
|
||||
ps << ");";
|
||||
});
|
||||
});
|
||||
});
|
||||
emitLocationInfoAndNewLine(ops);
|
||||
return success();
|
||||
}
|
||||
|
||||
LogicalResult StmtEmitter::visitVerif(verif::AssertOp op) {
|
||||
return emitVerifAssertLike(op, op.getProperty(), PPExtString("assert"));
|
||||
}
|
||||
|
||||
LogicalResult StmtEmitter::visitVerif(verif::AssumeOp op) {
|
||||
return emitVerifAssertLike(op, op.getProperty(), PPExtString("assume"));
|
||||
}
|
||||
|
||||
LogicalResult StmtEmitter::visitVerif(verif::CoverOp op) {
|
||||
return emitVerifAssertLike(op, op.getProperty(), PPExtString("cover"));
|
||||
}
|
||||
|
||||
LogicalResult StmtEmitter::emitIfDef(Operation *op, MacroIdentAttr cond) {
|
||||
if (hasSVAttributes(op))
|
||||
emitError(op, "SV attributes emission is unimplemented for the op");
|
||||
|
|
@ -4473,11 +4836,18 @@ void StmtEmitter::emitStatement(Operation *op) {
|
|||
if (isVerilogExpression(op))
|
||||
return;
|
||||
|
||||
// Handle HW statements, SV statements.
|
||||
if (succeeded(dispatchStmtVisitor(op)) || succeeded(dispatchSVVisitor(op)))
|
||||
// Ignore LTL expressions as they are emitted as part of verification
|
||||
// statements.
|
||||
if (isa<ltl::LTLDialect>(op->getDialect()))
|
||||
return;
|
||||
|
||||
emitOpError(op, "cannot emit this operation to Verilog");
|
||||
// Handle HW statements, SV statements.
|
||||
if (succeeded(dispatchStmtVisitor(op)) || succeeded(dispatchSVVisitor(op)) ||
|
||||
succeeded(dispatchVerifVisitor(op)))
|
||||
return;
|
||||
|
||||
emitOpError(op, "emission to Verilog not supported");
|
||||
emitPendingNewlineIfNeeded();
|
||||
ps << "unknown MLIR operation " << PPExtString(op->getName().getStringRef());
|
||||
setPendingNewline();
|
||||
}
|
||||
|
|
|
|||
|
|
@ -21,6 +21,8 @@
|
|||
#include "ExportVerilogInternals.h"
|
||||
#include "circt/Conversion/ExportVerilog.h"
|
||||
#include "circt/Dialect/Comb/CombOps.h"
|
||||
#include "circt/Dialect/LTL/LTLDialect.h"
|
||||
#include "circt/Dialect/Verif/VerifDialect.h"
|
||||
#include "mlir/IR/ImplicitLocOpBuilder.h"
|
||||
#include "llvm/ADT/DenseSet.h"
|
||||
#include "llvm/ADT/SmallPtrSet.h"
|
||||
|
|
@ -816,9 +818,11 @@ static LogicalResult legalizeHWModule(Block &block,
|
|||
opIterator != e;) {
|
||||
auto &op = *opIterator++;
|
||||
|
||||
if (!isa<CombDialect, SVDialect, HWDialect>(op.getDialect())) {
|
||||
op.emitError() << "this is an instance of unknown dialect detecetd. "
|
||||
"ExportVerilog cannot emit this operation so it needs "
|
||||
if (!isa<CombDialect, SVDialect, HWDialect, ltl::LTLDialect,
|
||||
verif::VerifDialect>(op.getDialect())) {
|
||||
auto d = op.emitError() << "dialect \"" << op.getDialect()->getNamespace()
|
||||
<< "\" not supported for direct Verilog emission";
|
||||
d.attachNote() << "ExportVerilog cannot emit this operation; it needs "
|
||||
"to be lowered before running ExportVerilog";
|
||||
return failure();
|
||||
}
|
||||
|
|
|
|||
|
|
@ -0,0 +1,248 @@
|
|||
// RUN: circt-opt %s --test-apply-lowering-options="options=emittedLineLength=9001" --export-verilog --verify-diagnostics | FileCheck %s
|
||||
|
||||
// CHECK-LABEL: module BasicEmissionNonTemporal
|
||||
hw.module @BasicEmissionNonTemporal(%a: i1, %b: i1) {
|
||||
%0 = comb.and %a, %b : i1
|
||||
%1 = comb.or %a, %b : i1
|
||||
// CHECK: assert property (a);
|
||||
// CHECK: assume property (a & b);
|
||||
// CHECK: cover property (a | b);
|
||||
verif.assert %a : i1
|
||||
verif.assume %0 : i1
|
||||
verif.cover %1 : i1
|
||||
|
||||
// CHECK: initial begin
|
||||
sv.initial {
|
||||
%2 = comb.xor %a, %b : i1
|
||||
%3 = comb.and %a, %b : i1
|
||||
// CHECK: assert(a);
|
||||
// CHECK: assume(a ^ b);
|
||||
// CHECK: cover(a & b);
|
||||
verif.assert %a : i1
|
||||
verif.assume %2 : i1
|
||||
verif.cover %3 : i1
|
||||
}
|
||||
// CHECK: end
|
||||
}
|
||||
|
||||
// CHECK-LABEL: module BasicEmissionTemporal
|
||||
hw.module @BasicEmissionTemporal(%a: i1) {
|
||||
%p = ltl.not %a : i1
|
||||
// CHECK: assert property (not a);
|
||||
// CHECK: assume property (not a);
|
||||
// CHECK: cover property (not a);
|
||||
verif.assert %p : !ltl.property
|
||||
verif.assume %p : !ltl.property
|
||||
verif.cover %p : !ltl.property
|
||||
|
||||
// CHECK: initial begin
|
||||
sv.initial {
|
||||
// CHECK: assert property (not a);
|
||||
// CHECK: assume property (not a);
|
||||
// CHECK: cover property (not a);
|
||||
verif.assert %p : !ltl.property
|
||||
verif.assume %p : !ltl.property
|
||||
verif.cover %p : !ltl.property
|
||||
}
|
||||
// CHECK: end
|
||||
}
|
||||
|
||||
// CHECK-LABEL: module Sequences
|
||||
hw.module @Sequences(%clk: i1, %a: i1, %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
|
||||
verif.assert %d1 : !ltl.sequence
|
||||
verif.assert %d2 : !ltl.sequence
|
||||
verif.assert %d3 : !ltl.sequence
|
||||
verif.assert %d4 : !ltl.sequence
|
||||
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
|
||||
verif.assert %c1 : !ltl.sequence
|
||||
verif.assert %c2 : !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
|
||||
verif.assert %g1 : !ltl.sequence
|
||||
verif.assert %g2 : !ltl.sequence
|
||||
verif.assert %g3 : !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
|
||||
verif.assert %k1 : !ltl.sequence
|
||||
verif.assert %k2 : !ltl.sequence
|
||||
verif.assert %k3 : !ltl.sequence
|
||||
verif.assert %k4 : !ltl.sequence
|
||||
}
|
||||
|
||||
// CHECK-LABEL: module Properties
|
||||
hw.module @Properties(%clk: i1, %a: i1, %b: i1) {
|
||||
%true = hw.constant true
|
||||
|
||||
// CHECK: assert property (not a);
|
||||
%n0 = ltl.not %a : i1
|
||||
verif.assert %n0 : !ltl.property
|
||||
|
||||
// CHECK: assert property (a |-> b);
|
||||
// CHECK: assert property (a ##1 b |-> not a);
|
||||
// CHECK: assert property (a ##1 b |=> not a);
|
||||
%i0 = ltl.implication %a, %b : i1, i1
|
||||
verif.assert %i0 : !ltl.property
|
||||
%i1 = ltl.delay %b, 1, 0 : i1
|
||||
%i2 = ltl.concat %a, %i1 : i1, !ltl.sequence
|
||||
%i3 = ltl.implication %i2, %n0 : !ltl.sequence, !ltl.property
|
||||
verif.assert %i3 : !ltl.property
|
||||
%i4 = ltl.delay %true, 1, 0 : i1
|
||||
%i5 = ltl.concat %a, %i1, %i4 : i1, !ltl.sequence, !ltl.sequence
|
||||
%i6 = ltl.implication %i5, %n0 : !ltl.sequence, !ltl.property
|
||||
verif.assert %i6 : !ltl.property
|
||||
|
||||
// CHECK: assert property (s_eventually a);
|
||||
%e0 = ltl.eventually %a : i1
|
||||
verif.assert %e0 : !ltl.property
|
||||
|
||||
// CHECK: assert property (@(posedge clk) a |-> b);
|
||||
// CHECK: assert property (@(posedge clk) a ##1 b |-> (@(negedge b) not a));
|
||||
// CHECK: assert property (disable iff (b) not a);
|
||||
// CHECK: assert property (disable iff (b) @(posedge clk) a |-> b);
|
||||
// CHECK: assert property (@(posedge clk) disable iff (b) not a);
|
||||
%k0 = ltl.clock %i0, posedge %clk : !ltl.property
|
||||
%k1 = ltl.clock %n0, negedge %b : !ltl.property
|
||||
%k2 = ltl.implication %i2, %k1 : !ltl.sequence, !ltl.property
|
||||
%k3 = ltl.clock %k2, posedge %clk : !ltl.property
|
||||
%k4 = ltl.disable %n0 if %b : !ltl.property
|
||||
%k5 = ltl.disable %k0 if %b : !ltl.property
|
||||
%k6 = ltl.clock %k4, posedge %clk : !ltl.property
|
||||
verif.assert %k0 : !ltl.property
|
||||
verif.assert %k3 : !ltl.property
|
||||
verif.assert %k4 : !ltl.property
|
||||
verif.assert %k5 : !ltl.property
|
||||
verif.assert %k6 : !ltl.property
|
||||
}
|
||||
|
||||
// CHECK-LABEL: module Precedence
|
||||
hw.module @Precedence(%a: i1, %b: i1) {
|
||||
// CHECK: assert property ((a or b) and b);
|
||||
%a0 = ltl.or %a, %b : i1, i1
|
||||
%a1 = ltl.and %a0, %b : !ltl.sequence, i1
|
||||
verif.assert %a1 : !ltl.sequence
|
||||
|
||||
// CHECK: assert property (##1 (a or b));
|
||||
%d0 = ltl.delay %a0, 1, 0 : !ltl.sequence
|
||||
verif.assert %d0 : !ltl.sequence
|
||||
|
||||
// CHECK: assert property (not (a or b));
|
||||
%n0 = ltl.not %a0 : !ltl.sequence
|
||||
verif.assert %n0 : !ltl.property
|
||||
|
||||
// CHECK: assert property (a and (a |-> b));
|
||||
%i0 = ltl.implication %a, %b : i1, i1
|
||||
%i1 = ltl.and %a, %i0 : i1, !ltl.property
|
||||
verif.assert %i1 : !ltl.property
|
||||
|
||||
// CHECK: assert property ((s_eventually a) and b);
|
||||
// CHECK: assert property (b and (s_eventually a));
|
||||
%e0 = ltl.eventually %a : i1
|
||||
%e1 = ltl.and %e0, %b : !ltl.property, i1
|
||||
%e2 = ltl.and %b, %e0 : i1, !ltl.property
|
||||
verif.assert %e1 : !ltl.property
|
||||
verif.assert %e2 : !ltl.property
|
||||
}
|
||||
|
||||
// CHECK-LABEL: module SystemVerilogSpecExamples
|
||||
hw.module @SystemVerilogSpecExamples(%clk: i1, %a: i1, %b: i1, %c: i1, %d: i1, %e: i1) {
|
||||
// Section 16.7 "Sequences"
|
||||
|
||||
// CHECK: assert property (a ##1 b ##0 c ##1 d);
|
||||
%a0 = ltl.delay %b, 1, 0 : i1
|
||||
%a1 = ltl.delay %d, 1, 0 : i1
|
||||
%a2 = ltl.concat %a, %a0 : i1, !ltl.sequence
|
||||
%a3 = ltl.concat %c, %a1 : i1, !ltl.sequence
|
||||
%a4 = ltl.concat %a2, %a3 : !ltl.sequence, !ltl.sequence
|
||||
verif.assert %a4 : !ltl.sequence
|
||||
|
||||
// Section 16.12.20 "Property examples"
|
||||
|
||||
// CHECK: assert property (@(posedge clk) a |-> b ##1 c ##1 d);
|
||||
%b0 = ltl.delay %c, 1, 0 : i1
|
||||
%b1 = ltl.concat %b, %b0, %a1 : i1, !ltl.sequence, !ltl.sequence
|
||||
%b2 = ltl.implication %a, %b1 : i1, !ltl.sequence
|
||||
%b3 = ltl.clock %b2, posedge %clk : !ltl.property
|
||||
verif.assert %b3 : !ltl.property
|
||||
|
||||
// CHECK: assert property (@(posedge clk) disable iff (e) a |-> not b ##1 c ##1 d);
|
||||
%c0 = ltl.not %b1 : !ltl.sequence
|
||||
%c1 = ltl.implication %a, %c0 : i1, !ltl.property
|
||||
%c2 = ltl.disable %c1 if %e : !ltl.property
|
||||
%c3 = ltl.clock %c2, posedge %clk : !ltl.property
|
||||
verif.assert %c3 : !ltl.property
|
||||
|
||||
// CHECK: assert property (##1 a |-> b);
|
||||
%d0 = ltl.delay %a, 1, 0 : i1
|
||||
%d1 = ltl.implication %d0, %b : !ltl.sequence, i1
|
||||
verif.assert %d1 : !ltl.property
|
||||
}
|
||||
|
||||
// CHECK-LABEL: module LivenessExample
|
||||
hw.module @LivenessExample(%clock: i1, %reset: i1, %isLive: i1) {
|
||||
%true = hw.constant true
|
||||
|
||||
// CHECK: wire _GEN = ~isLive;
|
||||
// CHECK: assert property (@(posedge clock) disable iff (reset) $fell(reset) & _GEN |-> (s_eventually isLive));
|
||||
// CHECK: assume property (@(posedge clock) disable iff (reset) $fell(reset) & _GEN |-> (s_eventually isLive));
|
||||
%not_isLive = comb.xor %isLive, %true : i1
|
||||
%fell_reset = sv.verbatim.expr "$fell({{0}})"(%reset) : (i1) -> i1
|
||||
%0 = comb.and %fell_reset, %not_isLive : i1
|
||||
%1 = ltl.eventually %isLive : i1
|
||||
%2 = ltl.implication %0, %1 : i1, !ltl.property
|
||||
%3 = ltl.disable %2 if %reset : !ltl.property
|
||||
%liveness_after_reset = ltl.clock %3, posedge %clock : !ltl.property
|
||||
verif.assert %liveness_after_reset : !ltl.property
|
||||
verif.assume %liveness_after_reset : !ltl.property
|
||||
|
||||
// CHECK: assert property (@(posedge clock) disable iff (reset) isLive ##1 _GEN |-> (s_eventually isLive));
|
||||
// CHECK: assume property (@(posedge clock) disable iff (reset) isLive ##1 _GEN |-> (s_eventually isLive));
|
||||
%4 = ltl.delay %not_isLive, 1, 0 : i1
|
||||
%5 = ltl.concat %isLive, %4 : i1, !ltl.sequence
|
||||
%6 = ltl.implication %5, %1 : !ltl.sequence, !ltl.property
|
||||
%7 = ltl.disable %6 if %reset : !ltl.property
|
||||
%liveness_after_fall = ltl.clock %7, posedge %clock : !ltl.property
|
||||
verif.assert %liveness_after_fall : !ltl.property
|
||||
verif.assume %liveness_after_fall : !ltl.property
|
||||
}
|
||||
Loading…
Reference in New Issue