Skip to content

[ImportVerilog] Use Slang's LRM clock inference for assertion calls #10370

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
TaoBi22 merged 2 commits into from
May 5, 2026
Merged

[ImportVerilog] Use Slang's LRM clock inference for assertion calls #10370

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
9f43179
[ImportVerilog] Use Slang's LRM clock inference for assertion calls
TaoBi22 May 1, 2026
8d3b18d
Address review comments
TaoBi22 May 5, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
88 changes: 81 additions & 7 deletions lib/Conversion/ImportVerilog/AssertionExpr.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,9 @@
#include "circt/Support/LLVM.h"
#include "mlir/IR/BuiltinAttributes.h"
#include "mlir/Support/LLVM.h"
#include "slang/analysis/AnalysisManager.h"
#include "slang/analysis/AnalyzedAssertion.h"
#include "slang/ast/ASTVisitor.h"
#include "slang/ast/SystemSubroutine.h"
#include "slang/parsing/KnownSystemName.h"

Expand Down Expand Up @@ -301,7 +304,7 @@ struct AssertionExprVisitor {

FailureOr<Value> Context::convertAssertionSystemCallArity1(
const slang::ast::SystemSubroutine &subroutine, Location loc, Value value,
Type originalType) {
Type originalType, Value clockVal) {
using ksn = slang::parsing::KnownSystemName;
auto nameId = subroutine.knownNameId;

Expand All @@ -322,37 +325,37 @@ FailureOr<Value> Context::convertAssertionSystemCallArity1(
// Translate $fell to ¬x[0] ∧ x[-1]
case ksn::Fell: {
auto past =
ltl::PastOp::create(builder, loc, value, 1, Value{}).getResult();
ltl::PastOp::create(builder, loc, value, 1, clockVal).getResult();
return castToMoore(comb::ICmpOp::create(
builder, loc, comb::ICmpPredicate::ugt, past, value, false));
}

// Translate $rose to x[0] ∧ ¬x[-1]
case ksn::Rose: {
auto past =
ltl::PastOp::create(builder, loc, value, 1, Value{}).getResult();
ltl::PastOp::create(builder, loc, value, 1, clockVal).getResult();
return castToMoore(comb::ICmpOp::create(
builder, loc, comb::ICmpPredicate::ult, past, value, false));
}

// Translate $changed to x[0] ≠ x[-1]
case ksn::Changed: {
auto past =
ltl::PastOp::create(builder, loc, value, 1, Value{}).getResult();
ltl::PastOp::create(builder, loc, value, 1, clockVal).getResult();
return castToMoore(comb::ICmpOp::create(
builder, loc, comb::ICmpPredicate::ne, past, value, false));
}

// Translate $stable to x[0] = x[-1]
case ksn::Stable: {
auto past =
ltl::PastOp::create(builder, loc, value, 1, Value{}).getResult();
ltl::PastOp::create(builder, loc, value, 1, clockVal).getResult();
return castToMoore(comb::ICmpOp::create(
builder, loc, comb::ICmpPredicate::eq, past, value, false));
}

case ksn::Past:
return castToMoore(ltl::PastOp::create(builder, loc, value, 1, Value{}));
return castToMoore(ltl::PastOp::create(builder, loc, value, 1, clockVal));

default:
return Value{};
Expand All @@ -363,6 +366,37 @@ Value Context::convertAssertionCallExpression(
const slang::ast::CallExpression &expr,
const slang::ast::CallExpression::SystemCallInfo &info, Location loc) {

const slang::ast::TimingControl *clock = nullptr;
auto clockIt = assertionCallClocks.find(&expr);
if (clockIt != assertionCallClocks.end())
clock = clockIt->second;

Value clockVal;
if (clock) {
const slang::ast::SignalEventControl *signal = nullptr;
if (clock->kind == slang::ast::TimingControlKind::SignalEvent) {
signal = &clock->as<slang::ast::SignalEventControl>();
} else if (clock->kind == slang::ast::TimingControlKind::EventList) {
mlir::emitError(loc, "sampled value functions with multiple event "
"triggers are not supported");
return {};
} else {
llvm_unreachable("unexpected clock kind for assertion");
}

if (signal->edge != slang::ast::EdgeKind::PosEdge) {
mlir::emitError(
loc,
"sampled value functions are only supported with posedge clocks");
return {};
}
clockVal = convertRvalueExpression(signal->expr);
if (clockVal)
clockVal = convertToI1(clockVal);
if (!clockVal)
return {};
}

const auto &subroutine = *info.subroutine;
auto args = expr.arguments();

Expand Down Expand Up @@ -411,7 +445,7 @@ Value Context::convertAssertionCallExpression(
if (!intVal)
return {};
result = this->convertAssertionSystemCallArity1(subroutine, loc, intVal,
originalType);
originalType, clockVal);
break;

default:
Expand Down Expand Up @@ -449,3 +483,43 @@ Value Context::convertToI1(Value value) {
}
return moore::ToBuiltinIntOp::create(builder, loc, value);
}

namespace {
struct AssertionClockVisitor
: slang::ast::ASTVisitor<AssertionClockVisitor, true, true> {
Context &context;
const slang::analysis::AnalyzedAssertion &assertion;
const slang::ast::TimingControl *currentClock = nullptr;

AssertionClockVisitor(Context &context,
const slang::analysis::AnalyzedAssertion &assertion)
: context(context), assertion(assertion) {}

void handle(const slang::ast::CallExpression &node) {
if (currentClock)
context.assertionCallClocks[&node] = currentClock;
visitDefault(node);
}

template <typename T>
std::enable_if_t<std::is_base_of_v<slang::ast::AssertionExpr, T>>
handle(const T &node) {
auto *prevClock = currentClock;
if (auto *clk = assertion.getClock(node))
currentClock = clk;
visitDefault(node);
currentClock = prevClock;
}
};
} // namespace

void Context::populateAssertionClocks() {
compilation.freeze();
slang::analysis::AnalysisManager am;
am.addListener([this](const slang::analysis::AnalyzedAssertion &assertion) {
AssertionClockVisitor visitor{*this, assertion};
assertion.getRoot().visit(visitor);
});
am.analyze(compilation);
compilation.unfreeze();
}
10 changes: 9 additions & 1 deletion lib/Conversion/ImportVerilog/ImportVerilogInternals.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -267,6 +267,14 @@ struct Context {
return currentThisRef; // block arg added in declareFunction
}

/// Maps assertion system calls to their corresponding clocks
DenseMap<const slang::ast::CallExpression *,
const slang::ast::TimingControl *>
assertionCallClocks;

/// Generates a map from assertions to clocks using Slang's analysis
void populateAssertionClocks();

Value getIndexedQueue() const { return currentQueue; }

// Convert a statement AST node to MLIR ops.
Expand Down Expand Up @@ -386,7 +394,7 @@ struct Context {
/// single argument.
FailureOr<Value> convertAssertionSystemCallArity1(
const slang::ast::SystemSubroutine &subroutine, Location loc, Value value,
Type originalType);
Type originalType, Value clockVal);

/// Evaluate the constant value of an expression.
slang::ConstantValue evaluateConstant(const slang::ast::Expression &expr);
Expand Down
4 changes: 4 additions & 0 deletions lib/Conversion/ImportVerilog/Structure.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -933,6 +933,10 @@ LogicalResult Context::convertCompilation() {
for (auto *inst : root.topInstances)
traverseInstanceBody(inst->body);

// Analyze the compilation to infer clocks for assertion system calls
// using Slang's LRM clock inference.
populateAssertionClocks();

// Visit all top-level declarations in all compilation units. This does not
// include instantiable constructs like modules, interfaces, and programs,
// which are listed separately as top instances.
Expand Down
58 changes: 47 additions & 11 deletions test/Conversion/ImportVerilog/builtins.sv
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -417,6 +417,9 @@ module SampleValueBuiltins #() (
// CHECK-NEXT: [[C:%.+]] = moore.read [[CLKWIRE]] : <l1>
// CHECK-NEXT: [[C_INT:%.+]] = moore.logic_to_int [[C]] : l1
// CHECK-NEXT: [[CB:%.+]] = moore.to_builtin_int [[C_INT]] : i1
// CHECK-NEXT: [[CLK:%.+]] = moore.read [[CLKWIRE]] : <l1>
// CHECK-NEXT: [[CLK_INT:%.+]] = moore.logic_to_int [[CLK]] : l1
// CHECK-NEXT: [[CLK_I1:%.+]] = moore.to_builtin_int [[CLK_INT]] : i1
// CHECK-NEXT: [[C2:%.+]] = moore.read [[CLKWIRE]] : <l1>
// CHECK-NEXT: [[C2_INT:%.+]] = moore.logic_to_int [[C2]] : l1
// CHECK-NEXT: [[CURRENT:%.+]] = moore.to_builtin_int [[C2_INT]] : i1
Expand All @@ -426,19 +429,25 @@ module SampleValueBuiltins #() (
// CHECK-NEXT: [[C:%.+]] = moore.read [[CLKWIRE]] : <l1>
// CHECK-NEXT: [[C_INT:%.+]] = moore.logic_to_int [[C]] : l1
// CHECK-NEXT: [[CB:%.+]] = moore.to_builtin_int [[C_INT]] : i1
// CHECK-NEXT: [[CLK:%.+]] = moore.read [[CLKWIRE]] : <l1>
// CHECK-NEXT: [[CLK_INT:%.+]] = moore.logic_to_int [[CLK]] : l1
// CHECK-NEXT: [[CLK_I1:%.+]] = moore.to_builtin_int [[CLK_INT]] : i1
// CHECK-NEXT: [[C2:%.+]] = moore.read [[CLKWIRE]] : <l1>
// CHECK-NEXT: [[C2_INT:%.+]] = moore.logic_to_int [[C2]] : l1
// CHECK-NEXT: [[CURRENT:%.+]] = moore.to_builtin_int [[C2_INT]] : i1
// CHECK-NEXT: [[PAST:%.+]] = ltl.past [[CURRENT]], 1 : i1
// CHECK-NEXT: [[PAST:%.+]] = ltl.past [[CURRENT]], 1 clk [[CLK_I1]] : i1
// CHECK-NEXT: [[ROSE:%.+]] = comb.icmp ult [[PAST]], [[CURRENT]] : i1
rising_clk: assert property (@(posedge clk_i) clk_i |=> $rose(clk_i));
// Check that the output of rose can be used by non-LTL ops
// CHECK: moore.procedure always {
// CHECK-NEXT: [[C1:%.+]] = moore.read [[CLKWIRE]] : <l1>
// CHECK-NEXT: [[CLK:%.+]] = moore.read [[CLKWIRE]] : <l1>
// CHECK-NEXT: [[CLK_INT:%.+]] = moore.logic_to_int [[CLK]] : l1
// CHECK-NEXT: [[CLK_I1:%.+]] = moore.to_builtin_int [[CLK_INT]] : i1
// CHECK-NEXT: [[C2:%.+]] = moore.read [[CLKWIRE]] : <l1>
// CHECK-NEXT: [[C2_INT:%.+]] = moore.logic_to_int [[C2]] : l1
// CHECK-NEXT: [[CURRENT:%.+]] = moore.to_builtin_int [[C2_INT]] : i1
// CHECK-NEXT: [[PAST:%.+]] = ltl.past [[CURRENT]], 1 : i1
// CHECK-NEXT: [[PAST:%.+]] = ltl.past [[CURRENT]], 1 clk [[CLK_I1]] : i1
// CHECK-NEXT: [[ROSE:%.+]] = comb.icmp ult [[PAST]], [[CURRENT]] : i1
// CHECK-NEXT: [[ROSE_INT:%.+]] = moore.from_builtin_int [[ROSE]] : i1
// CHECK-NEXT: [[ROSE_LOGIC:%.+]] = moore.int_to_logic [[ROSE_INT]] : i1
Expand All @@ -448,19 +457,25 @@ module SampleValueBuiltins #() (
// CHECK-NEXT: [[C:%.+]] = moore.read [[CLKWIRE]] : <l1>
// CHECK-NEXT: [[C_INT:%.+]] = moore.logic_to_int [[C]] : l1
// CHECK-NEXT: [[CB:%.+]] = moore.to_builtin_int [[C_INT]] : i1
// CHECK-NEXT: [[CLK:%.+]] = moore.read [[CLKWIRE]] : <l1>
// CHECK-NEXT: [[CLK_INT:%.+]] = moore.logic_to_int [[CLK]] : l1
// CHECK-NEXT: [[CLK_I1:%.+]] = moore.to_builtin_int [[CLK_INT]] : i1
// CHECK-NEXT: [[C2:%.+]] = moore.read [[CLKWIRE]] : <l1>
// CHECK-NEXT: [[C2_INT:%.+]] = moore.logic_to_int [[C2]] : l1
// CHECK-NEXT: [[CURRENT:%.+]] = moore.to_builtin_int [[C2_INT]] : i1
// CHECK-NEXT: [[PAST:%.+]] = ltl.past [[CURRENT]], 1 : i1
// CHECK-NEXT: [[PAST:%.+]] = ltl.past [[CURRENT]], 1 clk [[CLK_I1]] : i1
// CHECK-NEXT: [[FELL:%.+]] = comb.icmp ugt [[PAST]], [[CURRENT]] : i1
falling_clk: assert property (@(posedge clk_i) clk_i |=> $fell(clk_i));
// Check that the output of fell can be used by non-LTL ops
// CHECK: moore.procedure always {
// CHECK-NEXT: [[C1:%.+]] = moore.read [[CLKWIRE]] : <l1>
// CHECK-NEXT: [[CLK:%.+]] = moore.read [[CLKWIRE]] : <l1>
// CHECK-NEXT: [[CLK_INT:%.+]] = moore.logic_to_int [[CLK]] : l1
// CHECK-NEXT: [[CLK_I1:%.+]] = moore.to_builtin_int [[CLK_INT]] : i1
// CHECK-NEXT: [[C2:%.+]] = moore.read [[CLKWIRE]] : <l1>
// CHECK-NEXT: [[C2_INT:%.+]] = moore.logic_to_int [[C2]] : l1
// CHECK-NEXT: [[CURRENT:%.+]] = moore.to_builtin_int [[C2_INT]] : i1
// CHECK-NEXT: [[PAST:%.+]] = ltl.past [[CURRENT]], 1 : i1
// CHECK-NEXT: [[PAST:%.+]] = ltl.past [[CURRENT]], 1 clk [[CLK_I1]] : i1
// CHECK-NEXT: [[FELL:%.+]] = comb.icmp ugt [[PAST]], [[CURRENT]] : i1
// CHECK-NEXT: [[FELL_INT:%.+]] = moore.from_builtin_int [[FELL]] : i1
// CHECK-NEXT: [[FELL_LOGIC:%.+]] = moore.int_to_logic [[FELL_INT]] : i1
Expand All @@ -470,19 +485,25 @@ module SampleValueBuiltins #() (
// CHECK-NEXT: [[C:%.+]] = moore.read [[CLKWIRE]] : <l1>
// CHECK-NEXT: [[C_INT:%.+]] = moore.logic_to_int [[C]] : l1
// CHECK-NEXT: [[CB:%.+]] = moore.to_builtin_int [[C_INT]] : i1
// CHECK-NEXT: [[CLK:%.+]] = moore.read [[CLKWIRE]] : <l1>
// CHECK-NEXT: [[CLK_INT:%.+]] = moore.logic_to_int [[CLK]] : l1
// CHECK-NEXT: [[CLK_I1:%.+]] = moore.to_builtin_int [[CLK_INT]] : i1
// CHECK-NEXT: [[C2:%.+]] = moore.read [[CLKWIRE]] : <l1>
// CHECK-NEXT: [[C2_INT:%.+]] = moore.logic_to_int [[C2]] : l1
// CHECK-NEXT: [[CURRENT:%.+]] = moore.to_builtin_int [[C2_INT]] : i1
// CHECK-NEXT: [[PAST:%.+]] = ltl.past [[CURRENT]], 1 : i1
// CHECK-NEXT: [[PAST:%.+]] = ltl.past [[CURRENT]], 1 clk [[CLK_I1]] : i1
// CHECK-NEXT: [[STABLE:%.+]] = comb.icmp eq [[PAST]], [[CURRENT]] : i1
stable_clk: assert property (@(posedge clk_i) clk_i |=> $stable(clk_i));
// Check that the output of stable can be used by non-LTL ops
// CHECK: moore.procedure always {
// CHECK-NEXT: [[C1:%.+]] = moore.read [[CLKWIRE]] : <l1>
// CHECK-NEXT: [[CLK:%.+]] = moore.read [[CLKWIRE]] : <l1>
// CHECK-NEXT: [[CLK_INT:%.+]] = moore.logic_to_int [[CLK]] : l1
// CHECK-NEXT: [[CLK_I1:%.+]] = moore.to_builtin_int [[CLK_INT]] : i1
// CHECK-NEXT: [[C2:%.+]] = moore.read [[CLKWIRE]] : <l1>
// CHECK-NEXT: [[C2_INT:%.+]] = moore.logic_to_int [[C2]] : l1
// CHECK-NEXT: [[CURRENT:%.+]] = moore.to_builtin_int [[C2_INT]] : i1
// CHECK-NEXT: [[PAST:%.+]] = ltl.past [[CURRENT]], 1 : i1
// CHECK-NEXT: [[PAST:%.+]] = ltl.past [[CURRENT]], 1 clk [[CLK_I1]] : i1
// CHECK-NEXT: [[STABLE:%.+]] = comb.icmp eq [[PAST]], [[CURRENT]] : i1
// CHECK-NEXT: [[STABLE_INT:%.+]] = moore.from_builtin_int [[STABLE]] : i1
// CHECK-NEXT: [[STABLE_LOGIC:%.+]] = moore.int_to_logic [[STABLE_INT]] : i1
Expand All @@ -492,19 +513,25 @@ module SampleValueBuiltins #() (
// CHECK-NEXT: [[C:%.+]] = moore.read [[CLKWIRE]] : <l1>
// CHECK-NEXT: [[C_INT:%.+]] = moore.logic_to_int [[C]] : l1
// CHECK-NEXT: [[CB:%.+]] = moore.to_builtin_int [[C_INT]] : i1
// CHECK-NEXT: [[CLK:%.+]] = moore.read [[CLKWIRE]] : <l1>
// CHECK-NEXT: [[CLK_INT:%.+]] = moore.logic_to_int [[CLK]] : l1
// CHECK-NEXT: [[CLK_I1:%.+]] = moore.to_builtin_int [[CLK_INT]] : i1
// CHECK-NEXT: [[C2:%.+]] = moore.read [[CLKWIRE]] : <l1>
// CHECK-NEXT: [[C2_INT:%.+]] = moore.logic_to_int [[C2]] : l1
// CHECK-NEXT: [[CURRENT:%.+]] = moore.to_builtin_int [[C2_INT]] : i1
// CHECK-NEXT: [[PAST:%.+]] = ltl.past [[CURRENT]], 1 : i1
// CHECK-NEXT: [[PAST:%.+]] = ltl.past [[CURRENT]], 1 clk [[CLK_I1]] : i1
// CHECK-NEXT: [[CHANGED:%.+]] = comb.icmp ne [[PAST]], [[CURRENT]] : i1
changed_clk: assert property (@(posedge clk_i) clk_i |=> $changed(clk_i));
// Check that the output of changed can be used by non-LTL ops
// CHECK: moore.procedure always {
// CHECK-NEXT: [[C1:%.+]] = moore.read [[CLKWIRE]] : <l1>
// CHECK-NEXT: [[CLK:%.+]] = moore.read [[CLKWIRE]] : <l1>
// CHECK-NEXT: [[CLK_INT:%.+]] = moore.logic_to_int [[CLK]] : l1
// CHECK-NEXT: [[CLK_I1:%.+]] = moore.to_builtin_int [[CLK_INT]] : i1
// CHECK-NEXT: [[C2:%.+]] = moore.read [[CLKWIRE]] : <l1>
// CHECK-NEXT: [[C2_INT:%.+]] = moore.logic_to_int [[C2]] : l1
// CHECK-NEXT: [[CURRENT:%.+]] = moore.to_builtin_int [[C2_INT]] : i1
// CHECK-NEXT: [[PAST:%.+]] = ltl.past [[CURRENT]], 1 : i1
// CHECK-NEXT: [[PAST:%.+]] = ltl.past [[CURRENT]], 1 clk [[CLK_I1]] : i1
// CHECK-NEXT: [[CHANGED:%.+]] = comb.icmp ne [[PAST]], [[CURRENT]] : i1
// CHECK-NEXT: [[CHANGED_INT:%.+]] = moore.from_builtin_int [[CHANGED]] : i1
// CHECK-NEXT: [[CHANGED_LOGIC:%.+]] = moore.int_to_logic [[CHANGED_INT]] : i1
Expand All @@ -514,29 +541,38 @@ module SampleValueBuiltins #() (
// CHECK-NEXT: [[C:%.+]] = moore.read [[CLKWIRE]] : <l1>
// CHECK-NEXT: [[C_INT:%.+]] = moore.logic_to_int [[C]] : l1
// CHECK-NEXT: [[CB:%.+]] = moore.to_builtin_int [[C_INT]] : i1
// CHECK-NEXT: [[CLK:%.+]] = moore.read [[CLKWIRE]] : <l1>
// CHECK-NEXT: [[CLK_INT:%.+]] = moore.logic_to_int [[CLK]] : l1
// CHECK-NEXT: [[CLK_I1:%.+]] = moore.to_builtin_int [[CLK_INT]] : i1
// CHECK-NEXT: [[C2:%.+]] = moore.read [[CLKWIRE]] : <l1>
// CHECK-NEXT: [[C2_INT:%.+]] = moore.logic_to_int [[C2]] : l1
// CHECK-NEXT: [[CURRENT:%.+]] = moore.to_builtin_int [[C2_INT]] : i1
// CHECK-NEXT: [[PAST:%.+]] = ltl.past [[CURRENT]], 1 : i1
// CHECK-NEXT: [[PAST:%.+]] = ltl.past [[CURRENT]], 1 clk [[CLK_I1]] : i1
past_clk: assert property (@(posedge clk_i) clk_i |=> $past(clk_i));
// Check that the output of past can be used by non-LTL ops
// CHECK: moore.procedure always {
// CHECK-NEXT: [[C1:%.+]] = moore.read [[CLKWIRE]] : <l1>
// CHECK-NEXT: [[CLK:%.+]] = moore.read [[CLKWIRE]] : <l1>
// CHECK-NEXT: [[CLK_INT:%.+]] = moore.logic_to_int [[CLK]] : l1
// CHECK-NEXT: [[CLK_I1:%.+]] = moore.to_builtin_int [[CLK_INT]] : i1
// CHECK-NEXT: [[C2:%.+]] = moore.read [[CLKWIRE]] : <l1>
// CHECK-NEXT: [[C2_INT:%.+]] = moore.logic_to_int [[C2]] : l1
// CHECK-NEXT: [[CB:%.+]] = moore.to_builtin_int [[C2_INT]] : i1
// CHECK-NEXT: [[PAST:%.+]] = ltl.past [[CB]], 1 : i1
// CHECK-NEXT: [[PAST:%.+]] = ltl.past [[CB]], 1 clk [[CLK_I1]] : i1
// CHECK-NEXT: [[PAST_INT:%.+]] = moore.from_builtin_int [[PAST]] : i1
// CHECK-NEXT: [[PAST_LOGIC:%.+]] = moore.int_to_logic [[PAST_INT]] : i1
// CHECK-NEXT: [[EQ:%.+]] = moore.eq [[C1]], [[PAST_LOGIC]] : l1 -> l1
past_eq: assert property (@(posedge clk_i) clk_i == $past(clk_i));
// Test $past on wider bitvectors
// CHECK: moore.procedure always {
// CHECK-NEXT: [[D1:%.+]] = moore.read [[DATAWIRE]] : <l8>
// CHECK-NEXT: [[CLK:%.+]] = moore.read [[CLKWIRE]] : <l1>
// CHECK-NEXT: [[CLK_INT:%.+]] = moore.logic_to_int [[CLK]] : l1
// CHECK-NEXT: [[CLK_I1:%.+]] = moore.to_builtin_int [[CLK_INT]] : i1
// CHECK-NEXT: [[D2:%.+]] = moore.read [[DATAWIRE]] : <l8>
// CHECK-NEXT: [[D2_INT:%.+]] = moore.logic_to_int [[D2]] : l8
// CHECK-NEXT: [[DB:%.+]] = moore.to_builtin_int [[D2_INT]] : i8
// CHECK-NEXT: [[PAST:%.+]] = ltl.past [[DB]], 1 : i8
// CHECK-NEXT: [[PAST:%.+]] = ltl.past [[DB]], 1 clk [[CLK_I1]] : i8
// CHECK-NEXT: [[PAST_INT:%.+]] = moore.from_builtin_int [[PAST]] : i8
// CHECK-NEXT: [[PAST_LOGIC:%.+]] = moore.int_to_logic [[PAST_INT]] : i8
// CHECK-NEXT: [[EQ:%.+]] = moore.eq [[D1]], [[PAST_LOGIC]] : l8 -> l1
Expand Down
14 changes: 14 additions & 0 deletions test/Conversion/ImportVerilog/errors.sv
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -185,6 +185,20 @@ module Foo;
assert property (@(posedge a) $past(b));
endmodule

// -----
module Foo;
logic a, clk;
// expected-error @below {{sampled value functions are only supported with posedge clocks}}
assert property (@(negedge clk) $rose(a));
endmodule

// -----
module Foo;
logic a, clk1, clk2;
// expected-error @below {{sampled value functions with multiple event triggers are not supported}}
assert property (@(posedge clk1 or posedge clk2) $rose(a));
endmodule

// -----
module Foo;
int a;
Expand Down
Loading