mirror of https://github.com/llvm/circt.git
[ImportVerilog] Add support for concurrent assertions (#8559)
Initial setup for handling SystemVerilog Assertions by adding AssertionExpr class and integrating LTL dialect. This enables the foundation for converting SVA expressions to LTL. Handle concurrent assertion statements by inserting Verif operations assert and assume operations. Use `AssertionExpr` to parse the expression. Add a helper function to convert values to MLIR i1 type for LTL operations. The function validates that moore::IntType inputs are 1-bit wide and creates a ConversionOp to handle the conversion from SystemVerilog logic types. SystemVerilog assertions evaluate expressions to Boolean values where only 'true' results in true, with 'unknown' and 'high impedance' values both evaluating to false. This conversion is needed for LTL operations, which only work with i1 types. Add support for simple assertion expressions. Simple assertions consist of an expression, handled by 'Expression.h', and an optional repetition. Add conversion of the expression type to i1, which is the required input value of LTL operations. Add additional timing visitor to add LTL clock operation.
This commit is contained in:
Tobias Wölfel
GitHub
parent
71dda6038f
commit
b6b1ced097
|
|
@ -0,0 +1,305 @@
|
|||
//===- AssertionExpr.cpp - Slang assertion expression conversion ----------===//
|
||||
//
|
||||
// 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
|
||||
//
|
||||
//===----------------------------------------------------------------------===//
|
||||
|
||||
#include "slang/ast/expressions/AssertionExpr.h"
|
||||
#include "ImportVerilogInternals.h"
|
||||
#include "circt/Dialect/LTL/LTLOps.h"
|
||||
#include "circt/Dialect/Moore/MooreOps.h"
|
||||
#include "circt/Support/LLVM.h"
|
||||
#include "mlir/IR/BuiltinAttributes.h"
|
||||
#include "mlir/Support/LLVM.h"
|
||||
|
||||
#include <optional>
|
||||
#include <utility>
|
||||
|
||||
using namespace circt;
|
||||
using namespace ImportVerilog;
|
||||
|
||||
// NOLINTBEGIN(misc-no-recursion)
|
||||
namespace {
|
||||
struct AssertionExprVisitor {
|
||||
Context &context;
|
||||
Location loc;
|
||||
OpBuilder &builder;
|
||||
|
||||
AssertionExprVisitor(Context &context, Location loc)
|
||||
: context(context), loc(loc), builder(context.builder) {}
|
||||
|
||||
/// Helper to convert a range (min, optional max) to MLIR integer attributes
|
||||
std::pair<mlir::IntegerAttr, mlir::IntegerAttr>
|
||||
convertRangeToAttrs(uint32_t min,
|
||||
std::optional<uint32_t> max = std::nullopt) {
|
||||
auto minAttr = builder.getI64IntegerAttr(min);
|
||||
mlir::IntegerAttr rangeAttr;
|
||||
if (max.has_value()) {
|
||||
rangeAttr = builder.getI64IntegerAttr(max.value() - min);
|
||||
}
|
||||
return {minAttr, rangeAttr};
|
||||
}
|
||||
|
||||
/// Add repetition operation to a sequence
|
||||
Value createRepetition(Location loc,
|
||||
const slang::ast::SequenceRepetition &repetition,
|
||||
Value &inputSequence) {
|
||||
// Extract cycle range
|
||||
auto [minRepetitions, repetitionRange] =
|
||||
convertRangeToAttrs(repetition.range.min, repetition.range.max);
|
||||
|
||||
using slang::ast::SequenceRepetition;
|
||||
|
||||
// Check if repetition range is required
|
||||
if ((repetition.kind == SequenceRepetition::Nonconsecutive ||
|
||||
repetition.kind == SequenceRepetition::GoTo) &&
|
||||
!repetitionRange) {
|
||||
mlir::emitError(loc,
|
||||
repetition.kind == SequenceRepetition::Nonconsecutive
|
||||
? "Nonconsecutive repetition requires a maximum value"
|
||||
: "GoTo repetition requires a maximum value");
|
||||
return {};
|
||||
}
|
||||
|
||||
switch (repetition.kind) {
|
||||
case SequenceRepetition::Consecutive:
|
||||
return builder.create<ltl::RepeatOp>(loc, inputSequence, minRepetitions,
|
||||
repetitionRange);
|
||||
case SequenceRepetition::Nonconsecutive:
|
||||
return builder.create<ltl::NonConsecutiveRepeatOp>(
|
||||
loc, inputSequence, minRepetitions, repetitionRange);
|
||||
case SequenceRepetition::GoTo:
|
||||
return builder.create<ltl::GoToRepeatOp>(loc, inputSequence,
|
||||
minRepetitions, repetitionRange);
|
||||
}
|
||||
llvm_unreachable("All enum values handled in switch");
|
||||
}
|
||||
|
||||
Value visit(const slang::ast::SimpleAssertionExpr &expr) {
|
||||
// A Simple Assertion expression has the following members:
|
||||
// - Expression
|
||||
// - Optional repetition
|
||||
|
||||
// The expression needs to have the type `i1` for the LTL operations.
|
||||
// Convert first to a moore type and then add a conversion to `i1`.
|
||||
auto value = context.convertRvalueExpression(expr.expr);
|
||||
auto loc = context.convertLocation(expr.expr.sourceRange);
|
||||
value = context.convertToI1(value);
|
||||
if (!value)
|
||||
return {};
|
||||
|
||||
// The optional repetition is empty, return the converted expression
|
||||
if (!expr.repetition.has_value()) {
|
||||
return value;
|
||||
}
|
||||
|
||||
// There is a repetition, embed the expression into the kind of given
|
||||
// repetition
|
||||
return createRepetition(loc, expr.repetition.value(), value);
|
||||
}
|
||||
|
||||
Value visit(const slang::ast::SequenceConcatExpr &expr) {
|
||||
// Create a sequence of delayed operations, combined with a concat operation
|
||||
assert(!expr.elements.empty());
|
||||
|
||||
SmallVector<Value> sequenceElements;
|
||||
|
||||
for (const auto &concatElement : expr.elements) {
|
||||
Value sequenceValue =
|
||||
context.convertAssertionExpression(*concatElement.sequence, loc);
|
||||
if (!sequenceValue)
|
||||
return {};
|
||||
|
||||
Type valueType = sequenceValue.getType();
|
||||
assert(valueType.isInteger(1) || mlir::isa<ltl::SequenceType>(valueType));
|
||||
|
||||
auto [delayMin, delayRange] =
|
||||
convertRangeToAttrs(concatElement.delay.min, concatElement.delay.max);
|
||||
auto delayedSequence = builder.create<ltl::DelayOp>(loc, sequenceValue,
|
||||
delayMin, delayRange);
|
||||
sequenceElements.push_back(delayedSequence);
|
||||
}
|
||||
|
||||
return builder.createOrFold<ltl::ConcatOp>(loc, sequenceElements);
|
||||
}
|
||||
|
||||
Value visit(const slang::ast::UnaryAssertionExpr &expr) {
|
||||
auto value = context.convertAssertionExpression(expr.expr, loc);
|
||||
if (!value)
|
||||
return {};
|
||||
using slang::ast::UnaryAssertionOperator;
|
||||
switch (expr.op) {
|
||||
case UnaryAssertionOperator::Not:
|
||||
return builder.create<ltl::NotOp>(loc, value);
|
||||
case UnaryAssertionOperator::SEventually:
|
||||
if (expr.range.has_value()) {
|
||||
mlir::emitError(loc, "Strong eventually with range not supported");
|
||||
return {};
|
||||
} else {
|
||||
return builder.create<ltl::EventuallyOp>(loc, value);
|
||||
}
|
||||
case UnaryAssertionOperator::Always: {
|
||||
std::pair<mlir::IntegerAttr, mlir::IntegerAttr> attr = {
|
||||
builder.getI64IntegerAttr(0), mlir::IntegerAttr{}};
|
||||
if (expr.range.has_value()) {
|
||||
attr =
|
||||
convertRangeToAttrs(expr.range.value().min, expr.range.value().max);
|
||||
}
|
||||
return builder.create<ltl::RepeatOp>(loc, value, attr.first, attr.second);
|
||||
}
|
||||
case UnaryAssertionOperator::NextTime: {
|
||||
auto minRepetitions = builder.getI64IntegerAttr(1);
|
||||
if (expr.range.has_value()) {
|
||||
minRepetitions = builder.getI64IntegerAttr(expr.range.value().min);
|
||||
}
|
||||
return builder.create<ltl::DelayOp>(loc, value, minRepetitions,
|
||||
builder.getI64IntegerAttr(0));
|
||||
}
|
||||
case UnaryAssertionOperator::Eventually:
|
||||
case UnaryAssertionOperator::SNextTime:
|
||||
case UnaryAssertionOperator::SAlways:
|
||||
mlir::emitError(loc, "unsupported unary operator: ")
|
||||
<< slang::ast::toString(expr.op);
|
||||
return {};
|
||||
}
|
||||
llvm_unreachable("All enum values handled in switch");
|
||||
}
|
||||
|
||||
Value visit(const slang::ast::BinaryAssertionExpr &expr) {
|
||||
auto lhs = context.convertAssertionExpression(expr.left, loc);
|
||||
auto rhs = context.convertAssertionExpression(expr.right, loc);
|
||||
if (!lhs || !rhs)
|
||||
return {};
|
||||
SmallVector<Value, 2> operands = {lhs, rhs};
|
||||
using slang::ast::BinaryAssertionOperator;
|
||||
switch (expr.op) {
|
||||
case BinaryAssertionOperator::And:
|
||||
return builder.create<ltl::AndOp>(loc, operands);
|
||||
case BinaryAssertionOperator::Or:
|
||||
return builder.create<ltl::OrOp>(loc, operands);
|
||||
case BinaryAssertionOperator::Intersect:
|
||||
return builder.create<ltl::IntersectOp>(loc, operands);
|
||||
case BinaryAssertionOperator::Throughout: {
|
||||
auto lhsRepeat = builder.create<ltl::RepeatOp>(
|
||||
loc, lhs, builder.getI64IntegerAttr(0), mlir::IntegerAttr{});
|
||||
return builder.create<ltl::IntersectOp>(
|
||||
loc, SmallVector<Value, 2>{lhsRepeat, rhs});
|
||||
}
|
||||
case BinaryAssertionOperator::Within: {
|
||||
auto constOne =
|
||||
builder.create<hw::ConstantOp>(loc, builder.getI1Type(), 1);
|
||||
auto oneRepeat = builder.create<ltl::RepeatOp>(
|
||||
loc, constOne, builder.getI64IntegerAttr(0), mlir::IntegerAttr{});
|
||||
auto repeatDelay = builder.create<ltl::DelayOp>(
|
||||
loc, oneRepeat, builder.getI64IntegerAttr(1),
|
||||
builder.getI64IntegerAttr(0));
|
||||
auto lhsDelay = builder.create<ltl::DelayOp>(
|
||||
loc, lhs, builder.getI64IntegerAttr(1), builder.getI64IntegerAttr(0));
|
||||
auto combined = builder.create<ltl::ConcatOp>(
|
||||
loc, SmallVector<Value, 3>{repeatDelay, lhsDelay, constOne});
|
||||
return builder.create<ltl::IntersectOp>(
|
||||
loc, SmallVector<Value, 2>{combined, rhs});
|
||||
}
|
||||
case BinaryAssertionOperator::Iff: {
|
||||
auto ored = builder.create<ltl::OrOp>(loc, operands);
|
||||
auto notOred = builder.create<ltl::NotOp>(loc, ored);
|
||||
auto anded = builder.create<ltl::AndOp>(loc, operands);
|
||||
return builder.create<ltl::OrOp>(loc,
|
||||
SmallVector<Value, 2>{notOred, anded});
|
||||
}
|
||||
case BinaryAssertionOperator::Until:
|
||||
return builder.create<ltl::UntilOp>(loc, operands);
|
||||
case BinaryAssertionOperator::UntilWith: {
|
||||
auto untilOp = builder.create<ltl::UntilOp>(loc, operands);
|
||||
auto andOp = builder.create<ltl::AndOp>(loc, operands);
|
||||
auto notUntil = builder.create<ltl::NotOp>(loc, untilOp);
|
||||
return builder.create<ltl::OrOp>(loc,
|
||||
SmallVector<Value, 2>{notUntil, andOp});
|
||||
}
|
||||
case BinaryAssertionOperator::Implies: {
|
||||
auto notLhs = builder.create<ltl::NotOp>(loc, lhs);
|
||||
return builder.create<ltl::OrOp>(loc, SmallVector<Value, 2>{notLhs, rhs});
|
||||
}
|
||||
case BinaryAssertionOperator::OverlappedImplication:
|
||||
return builder.create<ltl::ImplicationOp>(loc, operands);
|
||||
case BinaryAssertionOperator::NonOverlappedImplication: {
|
||||
auto constOne =
|
||||
builder.create<hw::ConstantOp>(loc, builder.getI1Type(), 1);
|
||||
auto lhsDelay = builder.create<ltl::DelayOp>(
|
||||
loc, lhs, builder.getI64IntegerAttr(1), builder.getI64IntegerAttr(0));
|
||||
auto antecedent = builder.create<ltl::ConcatOp>(
|
||||
loc, SmallVector<Value, 2>{lhsDelay, constOne});
|
||||
return builder.create<ltl::ImplicationOp>(
|
||||
loc, SmallVector<Value, 2>{antecedent, rhs});
|
||||
}
|
||||
case BinaryAssertionOperator::OverlappedFollowedBy: {
|
||||
auto notRhs = builder.create<ltl::NotOp>(loc, rhs);
|
||||
auto implication = builder.create<ltl::ImplicationOp>(
|
||||
loc, SmallVector<Value, 2>{lhs, notRhs});
|
||||
return builder.create<ltl::NotOp>(loc, implication);
|
||||
}
|
||||
case BinaryAssertionOperator::NonOverlappedFollowedBy: {
|
||||
auto constOne =
|
||||
builder.create<hw::ConstantOp>(loc, builder.getI1Type(), 1);
|
||||
auto notRhs = builder.create<ltl::NotOp>(loc, rhs);
|
||||
auto lhsDelay = builder.create<ltl::DelayOp>(
|
||||
loc, lhs, builder.getI64IntegerAttr(1), builder.getI64IntegerAttr(0));
|
||||
auto antecedent = builder.create<ltl::ConcatOp>(
|
||||
loc, SmallVector<Value, 2>{lhsDelay, constOne});
|
||||
auto implication = builder.create<ltl::ImplicationOp>(
|
||||
loc, SmallVector<Value, 2>{antecedent, notRhs});
|
||||
return builder.create<ltl::NotOp>(loc, implication);
|
||||
}
|
||||
case BinaryAssertionOperator::SUntil:
|
||||
case BinaryAssertionOperator::SUntilWith:
|
||||
mlir::emitError(loc, "unsupported binary operator: ")
|
||||
<< slang::ast::toString(expr.op);
|
||||
return {};
|
||||
}
|
||||
llvm_unreachable("All enum values handled in switch");
|
||||
}
|
||||
|
||||
Value visit(const slang::ast::ClockingAssertionExpr &expr) {
|
||||
auto assertionExpr = context.convertAssertionExpression(expr.expr, loc);
|
||||
if (!assertionExpr)
|
||||
return {};
|
||||
return context.convertLTLTimingControl(expr.clocking, assertionExpr);
|
||||
}
|
||||
|
||||
/// Emit an error for all other expressions.
|
||||
template <typename T>
|
||||
Value visit(T &&node) {
|
||||
mlir::emitError(loc, "unsupported expression: ")
|
||||
<< slang::ast::toString(node.kind);
|
||||
return {};
|
||||
}
|
||||
|
||||
Value visitInvalid(const slang::ast::AssertionExpr &expr) {
|
||||
mlir::emitError(loc, "invalid expression");
|
||||
return {};
|
||||
}
|
||||
};
|
||||
} // namespace
|
||||
|
||||
Value Context::convertAssertionExpression(const slang::ast::AssertionExpr &expr,
|
||||
Location loc) {
|
||||
AssertionExprVisitor visitor{*this, loc};
|
||||
return expr.visit(visitor);
|
||||
}
|
||||
// NOLINTEND(misc-no-recursion)
|
||||
|
||||
/// Helper function to convert a value to an i1 value.
|
||||
Value Context::convertToI1(Value value) {
|
||||
if (!value)
|
||||
return {};
|
||||
auto type = dyn_cast<moore::IntType>(value.getType());
|
||||
if (!type || type.getBitSize() != 1) {
|
||||
mlir::emitError(value.getLoc(), "expected a 1-bit integer");
|
||||
return {};
|
||||
}
|
||||
|
||||
return builder.create<moore::ConversionOp>(value.getLoc(),
|
||||
builder.getI1Type(), value);
|
||||
}
|
||||
|
|
@ -1,6 +1,7 @@
|
|||
include(SlangCompilerOptions)
|
||||
|
||||
add_circt_translation_library(CIRCTImportVerilog
|
||||
AssertionExpr.cpp
|
||||
Expressions.cpp
|
||||
FormatStrings.cpp
|
||||
HierarchicalNames.cpp
|
||||
|
|
@ -16,7 +17,9 @@ add_circt_translation_library(CIRCTImportVerilog
|
|||
LINK_LIBS PUBLIC
|
||||
CIRCTDebug
|
||||
CIRCTHW
|
||||
CIRCTLTL
|
||||
CIRCTMoore
|
||||
CIRCTVerif
|
||||
MLIRFuncDialect
|
||||
MLIRSCFDialect
|
||||
MLIRTranslateLib
|
||||
|
|
|
|||
|
|
@ -266,7 +266,8 @@ LogicalResult ImportDriver::importVerilog(ModuleOp module) {
|
|||
// Traverse the parsed Verilog AST and map it to the equivalent CIRCT ops.
|
||||
mlirContext
|
||||
->loadDialect<moore::MooreDialect, hw::HWDialect, cf::ControlFlowDialect,
|
||||
func::FuncDialect, debug::DebugDialect>();
|
||||
func::FuncDialect, verif::VerifDialect, ltl::LTLDialect,
|
||||
debug::DebugDialect>();
|
||||
auto conversionTimer = ts.nest("Verilog to dialect mapping");
|
||||
Context context(options, *compilation, module, driver.sourceManager,
|
||||
bufferFilePaths);
|
||||
|
|
|
|||
|
|
@ -13,7 +13,9 @@
|
|||
#include "circt/Conversion/ImportVerilog.h"
|
||||
#include "circt/Dialect/Debug/DebugOps.h"
|
||||
#include "circt/Dialect/HW/HWOps.h"
|
||||
#include "circt/Dialect/LTL/LTLOps.h"
|
||||
#include "circt/Dialect/Moore/MooreOps.h"
|
||||
#include "circt/Dialect/Verif/VerifOps.h"
|
||||
#include "mlir/Dialect/ControlFlow/IR/ControlFlowOps.h"
|
||||
#include "mlir/Dialect/Func/IR/FuncOps.h"
|
||||
#include "slang/ast/ASTVisitor.h"
|
||||
|
|
@ -118,6 +120,10 @@ struct Context {
|
|||
Type requiredType = {});
|
||||
Value convertLvalueExpression(const slang::ast::Expression &expr);
|
||||
|
||||
// Convert an assertion expression AST node to MLIR ops.
|
||||
Value convertAssertionExpression(const slang::ast::AssertionExpr &expr,
|
||||
Location loc);
|
||||
|
||||
// Traverse the whole AST to collect hierarchical names.
|
||||
LogicalResult
|
||||
collectHierarchicalValues(const slang::ast::Expression &expr,
|
||||
|
|
@ -128,6 +134,13 @@ struct Context {
|
|||
LogicalResult convertTimingControl(const slang::ast::TimingControl &ctrl,
|
||||
const slang::ast::Statement &stmt);
|
||||
|
||||
/// Helper function to convert a value to a MLIR I1 value.
|
||||
Value convertToI1(Value value);
|
||||
|
||||
// Convert a slang timing control for LTL
|
||||
Value convertLTLTimingControl(const slang::ast::TimingControl &ctrl,
|
||||
const Value &seqOrPro);
|
||||
|
||||
/// Helper function to convert a value to its "truthy" boolean value.
|
||||
Value convertToBool(Value value);
|
||||
|
||||
|
|
|
|||
|
|
@ -642,6 +642,36 @@ struct StmtVisitor {
|
|||
return success();
|
||||
}
|
||||
|
||||
// Handle concurrent assertion statements.
|
||||
LogicalResult visit(const slang::ast::ConcurrentAssertionStatement &stmt) {
|
||||
auto loc = context.convertLocation(stmt.sourceRange);
|
||||
auto property = context.convertAssertionExpression(stmt.propertySpec, loc);
|
||||
if (!property)
|
||||
return failure();
|
||||
|
||||
// Handle assertion statements that don't have an action block.
|
||||
if (stmt.ifTrue && stmt.ifTrue->as_if<slang::ast::EmptyStatement>()) {
|
||||
switch (stmt.assertionKind) {
|
||||
case slang::ast::AssertionKind::Assert:
|
||||
builder.create<verif::AssertOp>(loc, property, Value(), StringAttr{});
|
||||
return success();
|
||||
case slang::ast::AssertionKind::Assume:
|
||||
builder.create<verif::AssumeOp>(loc, property, Value(), StringAttr{});
|
||||
return success();
|
||||
default:
|
||||
break;
|
||||
}
|
||||
mlir::emitError(loc) << "unsupported concurrent assertion kind: "
|
||||
<< slang::ast::toString(stmt.assertionKind);
|
||||
return failure();
|
||||
}
|
||||
|
||||
mlir::emitError(loc)
|
||||
<< "concurrent assertion statements with action blocks "
|
||||
"are not supported yet";
|
||||
return failure();
|
||||
}
|
||||
|
||||
/// Handle the subset of system calls that return no result value. Return
|
||||
/// true if the called system task could be handled, false otherwise. Return
|
||||
/// failure if an error occurred.
|
||||
|
|
|
|||
|
|
@ -13,6 +13,23 @@
|
|||
using namespace circt;
|
||||
using namespace ImportVerilog;
|
||||
|
||||
static ltl::ClockEdge convertEdgeKindLTL(const slang::ast::EdgeKind edge) {
|
||||
using slang::ast::EdgeKind;
|
||||
switch (edge) {
|
||||
case EdgeKind::NegEdge:
|
||||
return ltl::ClockEdge::Neg;
|
||||
case EdgeKind::PosEdge:
|
||||
return ltl::ClockEdge::Pos;
|
||||
case EdgeKind::None:
|
||||
// TODO: SV 16.16, what to do when no edge is specified?
|
||||
// For now, assume all changes (two-valued should be the same as both
|
||||
// edges)
|
||||
case EdgeKind::BothEdges:
|
||||
return ltl::ClockEdge::Both;
|
||||
}
|
||||
llvm_unreachable("all edge kinds handled");
|
||||
}
|
||||
|
||||
static moore::Edge convertEdgeKind(const slang::ast::EdgeKind edge) {
|
||||
using slang::ast::EdgeKind;
|
||||
switch (edge) {
|
||||
|
|
@ -87,6 +104,38 @@ struct DelayControlVisitor {
|
|||
}
|
||||
};
|
||||
|
||||
struct LTLClockControlVisitor {
|
||||
Context &context;
|
||||
Location loc;
|
||||
OpBuilder &builder;
|
||||
Value seqOrPro;
|
||||
|
||||
Value visit(const slang::ast::SignalEventControl &ctrl) {
|
||||
auto edge = convertEdgeKindLTL(ctrl.edge);
|
||||
auto expr = context.convertRvalueExpression(ctrl.expr);
|
||||
if (!expr)
|
||||
return Value{};
|
||||
Value condition;
|
||||
if (ctrl.iffCondition) {
|
||||
condition = context.convertRvalueExpression(*ctrl.iffCondition);
|
||||
condition = context.convertToBool(condition, Domain::TwoValued);
|
||||
if (!condition)
|
||||
return Value{};
|
||||
}
|
||||
expr = context.convertToI1(expr);
|
||||
if (!expr)
|
||||
return Value{};
|
||||
return builder.create<ltl::ClockOp>(loc, seqOrPro, edge, expr);
|
||||
}
|
||||
|
||||
template <typename T>
|
||||
Value visit(T &&ctrl) {
|
||||
mlir::emitError(loc, "unsupported LTL clock control: ")
|
||||
<< slang::ast::toString(ctrl.kind);
|
||||
return Value{};
|
||||
}
|
||||
};
|
||||
|
||||
} // namespace
|
||||
|
||||
// Entry point to timing control handling. This deals with the layer of repeats
|
||||
|
|
@ -201,4 +250,12 @@ Context::convertTimingControl(const slang::ast::TimingControl &ctrl,
|
|||
|
||||
return success();
|
||||
}
|
||||
|
||||
Value Context::convertLTLTimingControl(const slang::ast::TimingControl &ctrl,
|
||||
const Value &seqOrPro) {
|
||||
auto &builder = this->builder;
|
||||
auto loc = this->convertLocation(ctrl.sourceRange);
|
||||
LTLClockControlVisitor visitor{*this, loc, builder, seqOrPro};
|
||||
return ctrl.visit(visitor);
|
||||
}
|
||||
// NOLINTEND(misc-no-recursion)
|
||||
|
|
|
|||
|
|
@ -15,6 +15,7 @@
|
|||
#include "circt/Dialect/Debug/DebugOps.h"
|
||||
#include "circt/Dialect/HW/HWOps.h"
|
||||
#include "circt/Dialect/LLHD/IR/LLHDOps.h"
|
||||
#include "circt/Dialect/LTL/LTLOps.h"
|
||||
#include "circt/Dialect/Moore/MooreOps.h"
|
||||
#include "circt/Dialect/Sim/SimOps.h"
|
||||
#include "circt/Dialect/Verif/VerifOps.h"
|
||||
|
|
@ -1630,6 +1631,7 @@ static void populateLegality(ConversionTarget &target,
|
|||
target.addLegalDialect<comb::CombDialect>();
|
||||
target.addLegalDialect<hw::HWDialect>();
|
||||
target.addLegalDialect<llhd::LLHDDialect>();
|
||||
target.addLegalDialect<ltl::LTLDialect>();
|
||||
target.addLegalDialect<mlir::BuiltinDialect>();
|
||||
target.addLegalDialect<sim::SimDialect>();
|
||||
target.addLegalDialect<verif::VerifDialect>();
|
||||
|
|
|
|||
|
|
@ -2315,6 +2315,295 @@ module ImmediateAssertiWithActionBlock;
|
|||
assert (x) a = 1; else a = 0;
|
||||
endmodule
|
||||
|
||||
// CHECK-LABEL: moore.module @ConcurrentAssert(in %clk : !moore.l1)
|
||||
module ConcurrentAssert(input clk);
|
||||
// CHECK: [[CLK:%.+]] = moore.net name "clk" wire : <l1>
|
||||
// CHECK: [[A:%.+]] = moore.variable : <i1>
|
||||
bit a;
|
||||
// CHECK: [[B:%.+]] = moore.variable : <l1>
|
||||
logic b;
|
||||
|
||||
// Simple
|
||||
// CHECK: moore.procedure always
|
||||
// CHECK: [[READ_A:%.+]] = moore.read [[A]] : <i1>
|
||||
// CHECK: [[CONV_A:%.+]] = moore.conversion [[READ_A]] : !moore.i1 -> i1
|
||||
// CHECK: verif.assert [[CONV_A]] : i1
|
||||
// CHECK: moore.return
|
||||
// CHECK: }
|
||||
assert property (a);
|
||||
|
||||
// Sequence Concat
|
||||
// CHECK: moore.procedure always
|
||||
// CHECK: [[READ_A:%.+]] = moore.read [[A]] : <i1>
|
||||
// CHECK: [[CONV_A:%.+]] = moore.conversion [[READ_A]] : !moore.i1 -> i1
|
||||
// CHECK: [[REPEAT_OP:%.+]] = ltl.repeat [[CONV_A]], 1 : i1
|
||||
// CHECK: verif.assert [[REPEAT_OP]] : !ltl.sequence
|
||||
// CHECK: moore.return
|
||||
// CHECK: }
|
||||
assert property (a [*]);
|
||||
// CHECK: moore.procedure always
|
||||
// CHECK: [[READ_A:%.+]] = moore.read [[A]] : <i1>
|
||||
// CHECK: [[CONV_A:%.+]] = moore.conversion [[READ_A]] : !moore.i1 -> i1
|
||||
// CHECK: [[NONCONCATREPEAT_OP:%.+]] = ltl.non_consecutive_repeat [[CONV_A]], 2, 0 : i1
|
||||
// CHECK: verif.assert [[NONCONCATREPEAT_OP]] : !ltl.sequence
|
||||
// CHECK: moore.return
|
||||
// CHECK: }
|
||||
assert property (a [= 2]);
|
||||
// CHECK: moore.procedure always
|
||||
// CHECK: [[READ_A:%.+]] = moore.read [[A]] : <i1>
|
||||
// CHECK: [[CONV_A:%.+]] = moore.conversion [[READ_A]] : !moore.i1 -> i1
|
||||
// CHECK: [[GOTO_OP:%.+]] = ltl.goto_repeat [[CONV_A]], 2, 2 : i1
|
||||
// CHECK: verif.assert [[GOTO_OP]] : !ltl.sequence
|
||||
// CHECK: moore.return
|
||||
// CHECK: }
|
||||
assert property (a [-> 2:4]);
|
||||
// CHECK: moore.procedure always
|
||||
// CHECK: [[READ_A:%.+]] = moore.read [[A]] : <i1>
|
||||
// CHECK: [[CONV_A:%.+]] = moore.conversion [[READ_A]] : !moore.i1 -> i1
|
||||
// CHECK: [[DELAY_A:%.+]] = ltl.delay [[CONV_A]], 0, 0 : i1
|
||||
// CHECK: [[READ_B:%.+]] = moore.read [[B]] : <l1>
|
||||
// CHECK: [[CONV_B:%.+]] = moore.conversion [[READ_B]] : !moore.l1 -> i1
|
||||
// CHECK: [[DELAY_B:%.+]] = ltl.delay [[CONV_B]], 0, 0 : i1
|
||||
// CHECK: [[CONCAT_OP:%.+]] = ltl.concat [[DELAY_A]], [[DELAY_B]] : !ltl.sequence, !ltl.sequence
|
||||
// CHECK: verif.assert [[CONCAT_OP]] : !ltl.sequence
|
||||
// CHECK: moore.return
|
||||
// CHECK: }
|
||||
assert property (a ##0 b);
|
||||
// CHECK: moore.procedure always
|
||||
// CHECK: [[READ_A:%.+]] = moore.read [[A]] : <i1>
|
||||
// CHECK: [[CONV_A:%.+]] = moore.conversion [[READ_A]] : !moore.i1 -> i1
|
||||
// CHECK: [[DELAY_A:%.+]] = ltl.delay [[CONV_A]], 0, 0 : i1
|
||||
// CHECK: [[READ_B:%.+]] = moore.read [[B]] : <l1>
|
||||
// CHECK: [[CONV_B:%.+]] = moore.conversion [[READ_B]] : !moore.l1 -> i1
|
||||
// CHECK: [[DELAY_B:%.+]] = ltl.delay [[CONV_B]], 1 : i1
|
||||
// CHECK: [[READ_A2:%.+]] = moore.read [[A]] : <i1>
|
||||
// CHECK: [[CONV_A2:%.+]] = moore.conversion [[READ_A2]] : !moore.i1 -> i1
|
||||
// CHECK: [[DELAY_A2:%.+]] = ltl.delay [[CONV_A2]], 3, 2 : i1
|
||||
// CHECK: [[CONCAT_OP:%.+]] = ltl.concat [[DELAY_A]], [[DELAY_B]], [[DELAY_A2]] : !ltl.sequence, !ltl.sequence, !ltl.sequence
|
||||
// CHECK: verif.assert [[CONCAT_OP]] : !ltl.sequence
|
||||
// CHECK: moore.return
|
||||
// CHECK: }
|
||||
assert property (a ##[+] b ##[3:5] a);
|
||||
|
||||
// Unary
|
||||
// CHECK: moore.procedure always
|
||||
// CHECK: [[READ_A:%.+]] = moore.read [[A]] : <i1>
|
||||
// CHECK: [[CONV_A:%.+]] = moore.conversion [[READ_A]] : !moore.i1 -> i1
|
||||
// CHECK: [[NOT_OP:%.+]] = ltl.not [[CONV_A]] : i1
|
||||
// CHECK: verif.assert [[NOT_OP]] : !ltl.property
|
||||
// CHECK: moore.return
|
||||
// CHECK: }
|
||||
assert property (not a);
|
||||
// CHECK: moore.procedure always
|
||||
// CHECK: [[READ_A:%.+]] = moore.read [[A]] : <i1>
|
||||
// CHECK: [[CONV_A:%.+]] = moore.conversion [[READ_A]] : !moore.i1 -> i1
|
||||
// CHECK: [[EVEN_OP:%.+]] = ltl.eventually [[CONV_A]] : i1
|
||||
// CHECK: verif.assert [[EVEN_OP]] : !ltl.property
|
||||
// CHECK: moore.return
|
||||
// CHECK: }
|
||||
assert property (s_eventually a);
|
||||
// CHECK: moore.procedure always
|
||||
// CHECK: [[READ_A:%.+]] = moore.read [[A]] : <i1>
|
||||
// CHECK: [[CONV_A:%.+]] = moore.conversion [[READ_A]] : !moore.i1 -> i1
|
||||
// CHECK: [[REPEAT_OP:%.+]] = ltl.repeat [[CONV_A]], 0 : i1
|
||||
// CHECK: verif.assert [[REPEAT_OP]] : !ltl.sequence
|
||||
// CHECK: moore.return
|
||||
// CHECK: }
|
||||
assert property (always a);
|
||||
// CHECK: moore.procedure always
|
||||
// CHECK: [[READ_A:%.+]] = moore.read [[A]] : <i1>
|
||||
// CHECK: [[CONV_A:%.+]] = moore.conversion [[READ_A]] : !moore.i1 -> i1
|
||||
// CHECK: [[REPEAT_OP:%.+]] = ltl.repeat [[CONV_A]], 2, 1 : i1
|
||||
// CHECK: verif.assert [[REPEAT_OP]] : !ltl.sequence
|
||||
// CHECK: moore.return
|
||||
// CHECK: }
|
||||
assert property (always [2:3] a);
|
||||
// CHECK: moore.procedure always
|
||||
// CHECK: [[READ_A:%.+]] = moore.read [[A]] : <i1>
|
||||
// CHECK: [[CONV_A:%.+]] = moore.conversion [[READ_A]] : !moore.i1 -> i1
|
||||
// CHECK: [[DELAY_OP:%.+]] = ltl.delay [[CONV_A]], 1, 0 : i1
|
||||
// CHECK: verif.assert [[DELAY_OP]] : !ltl.sequence
|
||||
// CHECK: moore.return
|
||||
// CHECK: }
|
||||
assert property (nexttime a);
|
||||
// CHECK: moore.procedure always
|
||||
// CHECK: [[READ_A:%.+]] = moore.read [[A]] : <i1>
|
||||
// CHECK: [[CONV_A:%.+]] = moore.conversion [[READ_A]] : !moore.i1 -> i1
|
||||
// CHECK: [[DELAY_OP:%.+]] = ltl.delay [[CONV_A]], 5, 0 : i1
|
||||
// CHECK: verif.assert [[DELAY_OP]] : !ltl.sequence
|
||||
// CHECK: moore.return
|
||||
// CHECK: }
|
||||
assert property (nexttime [5] a);
|
||||
|
||||
// Binary
|
||||
// CHECK: moore.procedure always
|
||||
// CHECK: [[READ_A:%.+]] = moore.read [[A]] : <i1>
|
||||
// CHECK: [[CONV_A:%.+]] = moore.conversion [[READ_A]] : !moore.i1 -> i1
|
||||
// CHECK: [[READ_B:%.+]] = moore.read [[B]] : <l1>
|
||||
// CHECK: [[CONV_B:%.+]] = moore.conversion [[READ_B]] : !moore.l1 -> i1
|
||||
// CHECK: [[AND_OP:%.+]] = ltl.and [[CONV_A]], [[CONV_B]] : i1, i1
|
||||
// CHECK: verif.assert [[AND_OP]] : i1
|
||||
// CHECK: moore.return
|
||||
// CHECK: }
|
||||
assert property (a and b);
|
||||
// CHECK: moore.procedure always
|
||||
// CHECK: [[READ_A:%.+]] = moore.read [[A]] : <i1>
|
||||
// CHECK: [[CONV_A:%.+]] = moore.conversion [[READ_A]] : !moore.i1 -> i1
|
||||
// CHECK: [[READ_B:%.+]] = moore.read [[B]] : <l1>
|
||||
// CHECK: [[CONV_B:%.+]] = moore.conversion [[READ_B]] : !moore.l1 -> i1
|
||||
// CHECK: [[OR_OP:%.+]] = ltl.or [[CONV_A]], [[CONV_B]] : i1, i1
|
||||
// CHECK: verif.assert [[OR_OP]] : i1
|
||||
// CHECK: moore.return
|
||||
// CHECK: }
|
||||
assert property (a or b);
|
||||
// CHECK: moore.procedure always
|
||||
// CHECK: [[READ_A:%.+]] = moore.read [[A]] : <i1>
|
||||
// CHECK: [[CONV_A:%.+]] = moore.conversion [[READ_A]] : !moore.i1 -> i1
|
||||
// CHECK: [[READ_B:%.+]] = moore.read [[B]] : <l1>
|
||||
// CHECK: [[CONV_B:%.+]] = moore.conversion [[READ_B]] : !moore.l1 -> i1
|
||||
// CHECK: [[INTER_OP:%.+]] = ltl.intersect [[CONV_A]], [[CONV_B]] : i1, i1
|
||||
// CHECK: verif.assert [[INTER_OP]] : i1
|
||||
// CHECK: moore.return
|
||||
// CHECK: }
|
||||
assert property (a intersect b);
|
||||
// CHECK: moore.procedure always
|
||||
// CHECK: [[READ_A:%.+]] = moore.read [[A]] : <i1>
|
||||
// CHECK: [[CONV_A:%.+]] = moore.conversion [[READ_A]] : !moore.i1 -> i1
|
||||
// CHECK: [[READ_B:%.+]] = moore.read [[B]] : <l1>
|
||||
// CHECK: [[CONV_B:%.+]] = moore.conversion [[READ_B]] : !moore.l1 -> i1
|
||||
// CHECK: [[REPEAT_A:%.+]] = ltl.repeat [[CONV_A]], 0 : i1
|
||||
// CHECK: [[INTER_OP:%.+]] = ltl.intersect [[REPEAT_A]], [[CONV_B]] : !ltl.sequence, i1
|
||||
// CHECK: verif.assert [[INTER_OP]] : !ltl.sequence
|
||||
// CHECK: moore.return
|
||||
// CHECK: }
|
||||
assert property (a throughout b);
|
||||
// CHECK: moore.procedure always
|
||||
// CHECK: [[READ_A:%.+]] = moore.read [[A]] : <i1>
|
||||
// CHECK: [[CONV_A:%.+]] = moore.conversion [[READ_A]] : !moore.i1 -> i1
|
||||
// CHECK: [[READ_B:%.+]] = moore.read [[B]] : <l1>
|
||||
// CHECK: [[CONV_B:%.+]] = moore.conversion [[READ_B]] : !moore.l1 -> i1
|
||||
// CHECK: [[CONST_T:%.+]] = hw.constant true
|
||||
// CHECK: [[REPEAT_T:%.+]] = ltl.repeat [[CONST_T]], 0 : i1
|
||||
// CHECK: [[DELAY_RT:%.+]] = ltl.delay [[REPEAT_T]], 1, 0 : !ltl.sequence
|
||||
// CHECK: [[DELAY_A:%.+]] = ltl.delay [[CONV_A]], 1, 0 : i1
|
||||
// CHECK: [[CONCAT_OP:%.+]] = ltl.concat [[DELAY_RT]], [[DELAY_A]], [[CONST_T]] : !ltl.sequence, !ltl.sequence, i1
|
||||
// CHECK: [[INTER_OP:%.+]] = ltl.intersect [[CONCAT_OP]], [[CONV_B]] : !ltl.sequence, i1
|
||||
// CHECK: verif.assert [[INTER_OP]] : !ltl.sequence
|
||||
// CHECK: moore.return
|
||||
// CHECK: }
|
||||
assert property (a within b);
|
||||
// CHECK: moore.procedure always
|
||||
// CHECK: [[READ_A:%.+]] = moore.read [[A]] : <i1>
|
||||
// CHECK: [[CONV_A:%.+]] = moore.conversion [[READ_A]] : !moore.i1 -> i1
|
||||
// CHECK: [[READ_B:%.+]] = moore.read [[B]] : <l1>
|
||||
// CHECK: [[CONV_B:%.+]] = moore.conversion [[READ_B]] : !moore.l1 -> i1
|
||||
// CHECK: [[OR_OP:%.+]] = ltl.or [[CONV_A]], [[CONV_B]] : i1, i1
|
||||
// CHECK: [[NOT_OP:%.+]] = ltl.not [[OR_OP]] : i1
|
||||
// CHECK: [[AND_OP:%.+]] = ltl.and [[CONV_A]], [[CONV_B]] : i1, i1
|
||||
// CHECK: [[IFF:%.+]] = ltl.or [[NOT_OP]], [[AND_OP]] : !ltl.property, i1
|
||||
// CHECK: verif.assert [[IFF]] : !ltl.property
|
||||
// CHECK: moore.return
|
||||
// CHECK: }
|
||||
assert property (a iff b);
|
||||
// CHECK: moore.procedure always
|
||||
// CHECK: [[READ_A:%.+]] = moore.read [[A]] : <i1>
|
||||
// CHECK: [[CONV_A:%.+]] = moore.conversion [[READ_A]] : !moore.i1 -> i1
|
||||
// CHECK: [[READ_B:%.+]] = moore.read [[B]] : <l1>
|
||||
// CHECK: [[CONV_B:%.+]] = moore.conversion [[READ_B]] : !moore.l1 -> i1
|
||||
// CHECK: [[UNTIL_OP:%.+]] = ltl.until [[CONV_A]], [[CONV_B]] : i1, i1
|
||||
// CHECK: verif.assert [[UNTIL_OP]] : !ltl.property
|
||||
// CHECK: moore.return
|
||||
// CHECK: }
|
||||
assert property (a until b);
|
||||
// CHECK: moore.procedure always
|
||||
// CHECK: [[READ_A:%.+]] = moore.read [[A]] : <i1>
|
||||
// CHECK: [[CONV_A:%.+]] = moore.conversion [[READ_A]] : !moore.i1 -> i1
|
||||
// CHECK: [[READ_B:%.+]] = moore.read [[B]] : <l1>
|
||||
// CHECK: [[CONV_B:%.+]] = moore.conversion [[READ_B]] : !moore.l1 -> i1
|
||||
// CHECK: [[UNTIL_OP:%.+]] = ltl.until [[CONV_A]], [[CONV_B]] : i1, i1
|
||||
// CHECK: [[AND_OP:%.+]] = ltl.and [[CONV_A]], [[CONV_B]] : i1, i1
|
||||
// CHECK: [[NOT_OP:%.+]] = ltl.not [[UNTIL_OP]] : !ltl.property
|
||||
// CHECK: [[OR_OP:%.+]] = ltl.or [[NOT_OP]], [[AND_OP]] : !ltl.property, i1
|
||||
// CHECK: verif.assert [[OR_OP]] : !ltl.property
|
||||
// CHECK: moore.return
|
||||
// CHECK: }
|
||||
assert property (a until_with b);
|
||||
// CHECK: moore.procedure always
|
||||
// CHECK: [[READ_A:%.+]] = moore.read [[A]] : <i1>
|
||||
// CHECK: [[CONV_A:%.+]] = moore.conversion [[READ_A]] : !moore.i1 -> i1
|
||||
// CHECK: [[READ_B:%.+]] = moore.read [[B]] : <l1>
|
||||
// CHECK: [[CONV_B:%.+]] = moore.conversion [[READ_B]] : !moore.l1 -> i1
|
||||
// CHECK: [[NOT_OP:%.+]] = ltl.not [[CONV_A]] : i1
|
||||
// CHECK: [[OR_OP:%.+]] = ltl.or [[NOT_OP]], [[CONV_B]] : !ltl.property, i1
|
||||
// CHECK: verif.assert [[OR_OP]] : !ltl.property
|
||||
// CHECK: moore.return
|
||||
// CHECK: }
|
||||
assert property (a implies b);
|
||||
// CHECK: moore.procedure always
|
||||
// CHECK: [[READ_A:%.+]] = moore.read [[A]] : <i1>
|
||||
// CHECK: [[CONV_A:%.+]] = moore.conversion [[READ_A]] : !moore.i1 -> i1
|
||||
// CHECK: [[READ_B:%.+]] = moore.read [[B]] : <l1>
|
||||
// CHECK: [[CONV_B:%.+]] = moore.conversion [[READ_B]] : !moore.l1 -> i1
|
||||
// CHECK: [[IMPLICATION_OP:%.+]] = ltl.implication [[CONV_A]], [[CONV_B]] : i1, i1
|
||||
// CHECK: verif.assert [[IMPLICATION_OP]] : !ltl.property
|
||||
// CHECK: moore.return
|
||||
// CHECK: }
|
||||
assert property (a |-> b);
|
||||
// CHECK: moore.procedure always
|
||||
// CHECK: [[READ_A:%.+]] = moore.read [[A]] : <i1>
|
||||
// CHECK: [[CONV_A:%.+]] = moore.conversion [[READ_A]] : !moore.i1 -> i1
|
||||
// CHECK: [[READ_B:%.+]] = moore.read [[B]] : <l1>
|
||||
// CHECK: [[CONV_B:%.+]] = moore.conversion [[READ_B]] : !moore.l1 -> i1
|
||||
// CHECK: [[CONST_T:%.+]] = hw.constant true
|
||||
// CHECK: [[DELAY_OP:%.+]] = ltl.delay [[CONV_A]], 1, 0 : i1
|
||||
// CHECK: [[CONCAT_OP:%.+]] = ltl.concat [[DELAY_OP]], [[CONST_T]] : !ltl.sequence, i1
|
||||
// CHECK: [[IMPLICATION_OP:%.+]] = ltl.implication [[CONCAT_OP]], [[CONV_B]] : !ltl.sequence, i1
|
||||
// CHECK: verif.assert [[IMPLICATION_OP]] : !ltl.property
|
||||
// CHECK: moore.return
|
||||
// CHECK: }
|
||||
assert property (a |=> b);
|
||||
// CHECK: moore.procedure always
|
||||
// CHECK: [[READ_A:%.+]] = moore.read [[A]] : <i1>
|
||||
// CHECK: [[CONV_A:%.+]] = moore.conversion [[READ_A]] : !moore.i1 -> i1
|
||||
// CHECK: [[READ_B:%.+]] = moore.read [[B]] : <l1>
|
||||
// CHECK: [[CONV_B:%.+]] = moore.conversion [[READ_B]] : !moore.l1 -> i1
|
||||
// CHECK: [[NOT_OP:%.+]] = ltl.not [[CONV_B]] : i1
|
||||
// CHECK: [[IMPLICATION_OP:%.+]] = ltl.implication [[CONV_A]], [[NOT_OP]] : i1, !ltl.property
|
||||
// CHECK: [[NOT_IMPLI_OP:%.+]] = ltl.not [[IMPLICATION_OP]] : !ltl.property
|
||||
// CHECK: verif.assert [[NOT_IMPLI_OP]] : !ltl.property
|
||||
// CHECK: moore.return
|
||||
// CHECK: }
|
||||
assert property (a #-# b);
|
||||
// CHECK: moore.procedure always
|
||||
// CHECK: [[READ_A:%.+]] = moore.read [[A]] : <i1>
|
||||
// CHECK: [[CONV_A:%.+]] = moore.conversion [[READ_A]] : !moore.i1 -> i1
|
||||
// CHECK: [[READ_B:%.+]] = moore.read [[B]] : <l1>
|
||||
// CHECK: [[CONV_B:%.+]] = moore.conversion [[READ_B]] : !moore.l1 -> i1
|
||||
// CHECK: [[CONST_T:%.+]] = hw.constant true
|
||||
// CHECK: [[NOT_OP:%.+]] = ltl.not [[CONV_B]] : i1
|
||||
// CHECK: [[DELAY_OP:%.+]] = ltl.delay [[CONV_A]], 1, 0 : i1
|
||||
// CHECK: [[CONCAT_OP:%.+]] = ltl.concat [[DELAY_OP]], [[CONST_T]] : !ltl.sequence, i1
|
||||
// CHECK: [[IMPLICATION_OP:%.+]] = ltl.implication [[CONCAT_OP]], [[NOT_OP]] : !ltl.sequence, !ltl.property
|
||||
// CHECK: [[NOT_IMPLI_OP:%.+]] = ltl.not [[IMPLICATION_OP]] : !ltl.property
|
||||
// CHECK: verif.assert [[NOT_IMPLI_OP]] : !ltl.property
|
||||
// CHECK: moore.return
|
||||
// CHECK: }
|
||||
assert property (a #=# b);
|
||||
|
||||
// Clocking
|
||||
// CHECK: moore.procedure always
|
||||
// CHECK: [[READ_A:%.+]] = moore.read [[A]] : <i1>
|
||||
// CHECK: [[CONV_A:%.+]] = moore.conversion [[READ_A]] : !moore.i1 -> i1
|
||||
// CHECK: [[READ_CLK:%.+]] = moore.read [[CLK]] : <l1>
|
||||
// CHECK: [[CONV_CLK:%.+]] = moore.conversion [[READ_CLK]] : !moore.l1 -> i1
|
||||
// CHECK: [[CLK_OP:%.+]] = ltl.clock [[CONV_A]], posedge [[CONV_CLK]] : i1
|
||||
// CHECK: verif.assert [[CLK_OP]] : !ltl.sequence
|
||||
// CHECK: moore.return
|
||||
// CHECK: }
|
||||
assert property (@(posedge clk) a);
|
||||
|
||||
endmodule
|
||||
|
||||
// CHECK: [[TMP:%.+]] = moore.constant 42 : i32
|
||||
// CHECK: dbg.variable "rootParam1", [[TMP]] : !moore.i32
|
||||
parameter int rootParam1 = 42;
|
||||
|
|
|
|||
Loading…
Reference in New Issue