Skip to content

[ImportVerilog] Look through labels on module-level concurrent assertions #10796

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

Open
AmurG wants to merge 1 commit into
base: main
Choose a base branch
from
+113 −31
Open

[ImportVerilog] Look through labels on module-level concurrent assertions #10796

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
30 changes: 30 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 @@ -849,6 +849,36 @@ struct ModuleVisitor : public BaseVisitor {
const slang::ast::Statement &body) {
if (body.as_if<slang::ast::ConcurrentAssertionStatement>())
return context.convertStatement(body);

// A labeled module-level concurrent assertion (`CHK: assert property
// (p);`) arrives wrapped in a single-statement block, which used to
// fall through into the generic procedure path: the assertion then
// converted inside a `moore.procedure always` while its unlabeled twin
// converted at module scope, so a label silently changed which lowering
// an assertion got (and downstream consumers of module-scope assertions
// never saw the labeled one). Look through label blocks so labeled and
// unlabeled assertions take the same path. Only the `always` wrapper is
// treated this way -- for a body that reduces to a single concurrent
// assertion the two forms are equivalent (IEEE 1800-2017 16.14.6);
// concurrent assertions in initial/final procedures have one-attempt
// semantics and must not become continuous module-scope assertions.
if (kind == moore::ProcedureKind::Always) {
const slang::ast::Statement *stmt = &body;
while (true) {
if (auto *block = stmt->as_if<slang::ast::BlockStatement>()) {
stmt = &block->body;
continue;
}
if (auto *list = stmt->as_if<slang::ast::StatementList>();
list && list->list.size() == 1) {
stmt = list->list[0];
continue;
}
break;
}
if (stmt->as_if<slang::ast::ConcurrentAssertionStatement>())
return context.convertStatement(*stmt);
}
auto procOp = moore::ProcedureOp::create(builder, loc, kind);
OpBuilder::InsertionGuard guard(builder);
builder.setInsertionPointToEnd(&procOp.getBody().emplaceBlock());
Expand Down
76 changes: 45 additions & 31 deletions test/Conversion/ImportVerilog/builtins.sv
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -457,8 +457,7 @@ module SampleValueBuiltins #() (
// CHECK: [[CLKWIRE:%.+]] = moore.net name "clk_i" wire : <l1>
// CHECK: [[DATAWIRE:%.+]] = moore.net name "data_i" wire : <l8>
// CHECK: [[DATABITWIRE:%.+]] = moore.net name "data_bit_i" wire : <i8>
// CHECK: moore.procedure always {
// CHECK-NEXT: [[C:%.+]] = moore.read [[CLKWIRE]] : <l1>
// CHECK: [[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>
Expand All @@ -468,9 +467,10 @@ module SampleValueBuiltins #() (
// CHECK-NEXT: [[C2_INT:%.+]] = moore.logic_to_int [[C2]] : l1
// CHECK-NEXT: [[CURRENT:%.+]] = moore.to_builtin_int [[C2_INT]] : i1
// CHECK-NEXT: [[SAMPLED:%.+]] = ltl.sampled [[CURRENT]] : i1
// CHECK: ltl.clock
// CHECK: verif.assert
sampled_clk: assert property (@(posedge clk_i) clk_i |=> $sampled(clk_i));
// CHECK: moore.procedure always {
// CHECK-NEXT: [[C:%.+]] = moore.read [[CLKWIRE]] : <l1>
// CHECK: [[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>
Expand All @@ -481,10 +481,11 @@ module SampleValueBuiltins #() (
// CHECK-NEXT: [[CURRENT:%.+]] = moore.to_builtin_int [[C2_INT]] : i1
// CHECK-NEXT: [[PAST:%.+]] = ltl.past [[CURRENT]], 1 clk [[CLK_I1]] : i1
// CHECK-NEXT: [[ROSE:%.+]] = comb.icmp ult [[PAST]], [[CURRENT]] : i1
// CHECK: ltl.clock
// CHECK: verif.assert
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: [[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
Expand All @@ -496,9 +497,10 @@ module SampleValueBuiltins #() (
// CHECK-NEXT: [[ROSE_INT:%.+]] = moore.from_builtin_int [[ROSE]] : i1
// CHECK-NEXT: [[ROSE_LOGIC:%.+]] = moore.int_to_logic [[ROSE_INT]] : i1
// CHECK-NEXT: [[EQ:%.+]] = moore.eq [[C1]], [[ROSE_LOGIC]] : l1 -> l1
// CHECK: ltl.clock
// CHECK: verif.assert
rose_eq: assert property (@(posedge clk_i) clk_i == $rose(clk_i));
// CHECK: moore.procedure always {
// CHECK-NEXT: [[C:%.+]] = moore.read [[CLKWIRE]] : <l1>
// CHECK: [[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>
Expand All @@ -509,10 +511,11 @@ module SampleValueBuiltins #() (
// CHECK-NEXT: [[CURRENT:%.+]] = moore.to_builtin_int [[C2_INT]] : i1
// CHECK-NEXT: [[PAST:%.+]] = ltl.past [[CURRENT]], 1 clk [[CLK_I1]] : i1
// CHECK-NEXT: [[FELL:%.+]] = comb.icmp ugt [[PAST]], [[CURRENT]] : i1
// CHECK: ltl.clock
// CHECK: verif.assert
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: [[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
Expand All @@ -524,9 +527,10 @@ module SampleValueBuiltins #() (
// CHECK-NEXT: [[FELL_INT:%.+]] = moore.from_builtin_int [[FELL]] : i1
// CHECK-NEXT: [[FELL_LOGIC:%.+]] = moore.int_to_logic [[FELL_INT]] : i1
// CHECK-NEXT: [[EQ:%.+]] = moore.eq [[C1]], [[FELL_LOGIC]] : l1 -> l1
// CHECK: ltl.clock
// CHECK: verif.assert
fell_eq: assert property (@(posedge clk_i) clk_i == $fell(clk_i));
// CHECK: moore.procedure always {
// CHECK-NEXT: [[C:%.+]] = moore.read [[CLKWIRE]] : <l1>
// CHECK: [[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>
Expand All @@ -537,10 +541,11 @@ module SampleValueBuiltins #() (
// CHECK-NEXT: [[CURRENT:%.+]] = moore.to_builtin_int [[C2_INT]] : i1
// CHECK-NEXT: [[PAST:%.+]] = ltl.past [[CURRENT]], 1 clk [[CLK_I1]] : i1
// CHECK-NEXT: [[STABLE:%.+]] = comb.icmp eq [[PAST]], [[CURRENT]] : i1
// CHECK: ltl.clock
// CHECK: verif.assert
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: [[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
Expand All @@ -552,9 +557,10 @@ module SampleValueBuiltins #() (
// CHECK-NEXT: [[STABLE_INT:%.+]] = moore.from_builtin_int [[STABLE]] : i1
// CHECK-NEXT: [[STABLE_LOGIC:%.+]] = moore.int_to_logic [[STABLE_INT]] : i1
// CHECK-NEXT: [[EQ:%.+]] = moore.eq [[C1]], [[STABLE_LOGIC]] : l1 -> l1
// CHECK: ltl.clock
// CHECK: verif.assert
stable_eq: assert property (@(posedge clk_i) clk_i == $stable(clk_i));
// CHECK: moore.procedure always {
// CHECK-NEXT: [[C:%.+]] = moore.read [[CLKWIRE]] : <l1>
// CHECK: [[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>
Expand All @@ -565,10 +571,11 @@ module SampleValueBuiltins #() (
// CHECK-NEXT: [[CURRENT:%.+]] = moore.to_builtin_int [[C2_INT]] : i1
// CHECK-NEXT: [[PAST:%.+]] = ltl.past [[CURRENT]], 1 clk [[CLK_I1]] : i1
// CHECK-NEXT: [[CHANGED:%.+]] = comb.icmp ne [[PAST]], [[CURRENT]] : i1
// CHECK: ltl.clock
// CHECK: verif.assert
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: [[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
Expand All @@ -580,9 +587,10 @@ module SampleValueBuiltins #() (
// CHECK-NEXT: [[CHANGED_INT:%.+]] = moore.from_builtin_int [[CHANGED]] : i1
// CHECK-NEXT: [[CHANGED_LOGIC:%.+]] = moore.int_to_logic [[CHANGED_INT]] : i1
// CHECK-NEXT: [[EQ:%.+]] = moore.eq [[C1]], [[CHANGED_LOGIC]] : l1 -> l1
// CHECK: ltl.clock
// CHECK: verif.assert
changed_eq: assert property (@(posedge clk_i) clk_i == $changed(clk_i));
// CHECK: moore.procedure always {
// CHECK-NEXT: [[C:%.+]] = moore.read [[CLKWIRE]] : <l1>
// CHECK: [[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>
Expand All @@ -592,10 +600,11 @@ module SampleValueBuiltins #() (
// 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 clk [[CLK_I1]] : i1
// CHECK: ltl.clock
// CHECK: verif.assert
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: [[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
Expand All @@ -606,10 +615,11 @@ module SampleValueBuiltins #() (
// 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
// CHECK: ltl.clock
// CHECK: verif.assert
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: [[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
Expand All @@ -620,18 +630,19 @@ module SampleValueBuiltins #() (
// 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
// CHECK: ltl.clock
// CHECK: verif.assert
past_data: assert property (@(posedge clk_i) data_i == $past(data_i));

// CHECK: moore.procedure always {
// CHECK: [[D:%.+]] = moore.read [[DATAWIRE]] : <l8>
// CHECK: [[RED:%.+]] = moore.reduce_xor [[D]] : l8 -> l1
// CHECK: [[X:%.+]] = moore.constant bX : l1
// CHECK: [[CEQ:%.+]] = moore.case_eq [[RED]], [[X]] : l1
// CHECK: [[CEQ_I1:%.+]] = moore.to_builtin_int [[CEQ]] : i1
// CHECK: ltl.clock [[CEQ_I1]]
// CHECK: verif.assert
isunknown_data: assert property (@(posedge clk_i) $isunknown(data_i));

// CHECK: moore.procedure always {
// CHECK: [[D:%.+]] = moore.read [[DATAWIRE]] : <l8>
// CHECK: [[RED:%.+]] = moore.reduce_xor [[D]] : l8 -> l1
// CHECK: [[X:%.+]] = moore.constant bX : l1
Expand All @@ -650,9 +661,9 @@ module SampleValueBuiltins #() (
// CHECK: [[RES_LOGIC:%.+]] = moore.int_to_logic [[RES_INT]] : i1
// CHECK: [[RES_BUILTIN:%.+]] = moore.to_builtin_int [[RES_INT]] : i1
// CHECK: ltl.clock [[RES_BUILTIN]]
// CHECK: verif.assert
onehot0_data: assert property (@(posedge clk_i) $onehot0(data_i));

// CHECK: moore.procedure always {
// CHECK: [[D:%.+]] = moore.read [[DATAWIRE]] : <l8>
// CHECK: [[RED:%.+]] = moore.reduce_xor [[D]] : l8 -> l1
// CHECK: [[X:%.+]] = moore.constant bX : l1
Expand All @@ -673,9 +684,9 @@ module SampleValueBuiltins #() (
// CHECK: [[RES_LOGIC:%.+]] = moore.int_to_logic [[RES_INT]] : i1
// CHECK: [[RES_BUILTIN:%.+]] = moore.to_builtin_int [[RES_INT]] : i1
// CHECK: ltl.clock [[RES_BUILTIN]]
// CHECK: verif.assert
onehot_data: assert property (@(posedge clk_i) $onehot(data_i));

// CHECK: moore.procedure always {
// CHECK: [[D:%.+]] = moore.read [[DATABITWIRE]] : <i8>
// CHECK: [[DB:%.+]] = moore.to_builtin_int [[D]] : i8
// CHECK: [[ONE:%.+]] = hw.constant 1 : i8
Expand All @@ -686,9 +697,9 @@ module SampleValueBuiltins #() (
// CHECK: [[EQ_INT:%.+]] = moore.from_builtin_int [[EQ]] : i1
// CHECK: [[EQ_BUILTIN:%.+]] = moore.to_builtin_int [[EQ_INT]] : i1
// CHECK: ltl.clock [[EQ_BUILTIN]]
// CHECK: verif.assert
onehot0_bit_data: assert property (@(posedge clk_i) $onehot0(data_bit_i));

// CHECK: moore.procedure always {
// CHECK: [[D:%.+]] = moore.read [[DATABITWIRE]] : <i8>
// CHECK: [[DB:%.+]] = moore.to_builtin_int [[D]] : i8
// CHECK: [[ONE:%.+]] = hw.constant 1 : i8
Expand All @@ -701,9 +712,9 @@ module SampleValueBuiltins #() (
// CHECK: [[RES_INT:%.+]] = moore.from_builtin_int [[AND2]] : i1
// CHECK: [[RES_BUILTIN:%.+]] = moore.to_builtin_int [[RES_INT]] : i1
// CHECK: ltl.clock [[RES_BUILTIN]]
// CHECK: verif.assert
onehot_bit_data: assert property (@(posedge clk_i) $onehot(data_bit_i));

// CHECK: moore.procedure always {
// CHECK: [[D:%.+]] = moore.read [[DATAWIRE]] : <l8>
// CHECK: [[D_L2I:%.+]] = moore.logic_to_int [[D]] : l8
// CHECK: [[DB:%.+]] = moore.to_builtin_int [[D_L2I]] : i8
Expand All @@ -716,10 +727,11 @@ module SampleValueBuiltins #() (
// CHECK: [[SEXT:%.+]] = moore.zext [[RES_INT]] : i4 -> i32
// CHECK: [[ZERO:%.+]] = moore.constant 0 : i32
// CHECK: [[EQ:%.+]] = moore.eq [[SEXT]], [[ZERO]] : i32 -> i1
// CHECK: ltl.clock
// CHECK: verif.assert
countones_data:
assert property (@(posedge clk_i) $countones(data_i) == 0);

// CHECK: moore.procedure always {
// CHECK: [[D:%.+]] = moore.read [[DATABITWIRE]] : <i8>
// CHECK: [[DB:%.+]] = moore.to_builtin_int [[D]] : i8
// CHECK: [[Z3:%.+]] = hw.constant 0 : i3
Expand All @@ -732,6 +744,8 @@ module SampleValueBuiltins #() (
// CHECK: [[SEXT:%.+]] = moore.zext [[RES_INT]] : i4 -> i32
// CHECK: [[ZERO:%.+]] = moore.constant 0 : i32
// CHECK: [[EQ:%.+]] = moore.eq [[SEXT]], [[ZERO]] : i32 -> i1
// CHECK: ltl.clock
// CHECK: verif.assert
countones_bit_data:
assert property (@(posedge clk_i) $countones(data_bit_i) == 0);
endmodule
Expand Down
38 changes: 38 additions & 0 deletions test/Conversion/ImportVerilog/labeled-concurrent-assertions.sv
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,38 @@
// RUN: circt-translate --import-verilog %s | FileCheck %s
// REQUIRES: slang
// UNSUPPORTED: valgrind

// A statement label on a module-level concurrent assertion (`CHK: assert
// property (p);`) wraps the statement in a single-statement block, which
// used to defeat the module-scope conversion short-circuit: the labeled
// assertion converted inside a `moore.procedure always` while its unlabeled
// twin converted at module scope, so downstream consumers of module-scope
// assertions never saw the labeled one. A label must not change which
// lowering an assertion gets.

// CHECK-LABEL: moore.module @LabeledAssert
module LabeledAssert(input logic clk, input logic a, input logic b);
// Unlabeled and labeled convert identically, at module scope.
// CHECK: ltl.implication
// CHECK: ltl.clock
// CHECK: verif.assert
// CHECK: ltl.implication
// CHECK: ltl.clock
// CHECK: verif.assert
// CHECK-NOT: moore.procedure
assert property (@(posedge clk) a |-> b);
CHK: assert property (@(posedge clk) a |-> b);
endmodule

// Concurrent assertions written in an `initial` block have one-attempt
// semantics (IEEE 1800-2017 16.14.6) and must NOT be rerouted to a
// continuous module-scope assertion by the label look-through.
// CHECK-LABEL: moore.module @InitialNotRerouted
module InitialNotRerouted(input logic clk, input logic a);
// CHECK: moore.procedure initial
// CHECK: ltl.clock
// CHECK: verif.assert
initial begin
LBL2: assert property (@(posedge clk) a);
end
endmodule