From 65b632a7dd8927930c85c8236e73d0fb1d9a31d5 Mon Sep 17 00:00:00 2001 From: Yutetsu TAKATSUKASA Date: Tue, 13 Feb 2024 21:53:32 +0900 Subject: [PATCH] Improve assertion for unique case (#4892) - Use parallel_case, unique, and unique0 in error message - Distinguish multiple match and no match - Show the case value that triggers the assertion --- src/V3Assert.cpp | 46 ++++++++++++------- src/V3AstNodeOther.h | 1 + src/V3AstNodes.cpp | 16 +++++++ test_regress/t/t_assert_inside_cond_bad.out | 2 +- test_regress/t/t_assert_synth_parallel.out | 2 +- .../t/t_assert_synth_parallel_vlt.out | 2 +- test_regress/t/t_assert_unique_case_bad.out | 12 +++++ test_regress/t/t_assert_unique_case_bad.pl | 23 ++++++++++ test_regress/t/t_assert_unique_case_bad.v | 43 +++++++++++++++++ 9 files changed, 128 insertions(+), 19 deletions(-) create mode 100644 test_regress/t/t_assert_unique_case_bad.out create mode 100755 test_regress/t/t_assert_unique_case_bad.pl create mode 100644 test_regress/t/t_assert_unique_case_bad.v diff --git a/src/V3Assert.cpp b/src/V3Assert.cpp index 897fe5906..8da4e113a 100644 --- a/src/V3Assert.cpp +++ b/src/V3Assert.cpp @@ -118,19 +118,21 @@ class AssertVisitor final : public VNVisitor { return newp; } - AstNode* newFireAssertUnchecked(AstNode* nodep, const string& message) { + AstNode* newFireAssertUnchecked(AstNode* nodep, const string& message, + AstNodeExpr* exprsp = nullptr) { // Like newFireAssert() but omits the asserts-on check AstDisplay* const dispp = new AstDisplay{nodep->fileline(), VDisplayType::DT_ERROR, message, nullptr, nullptr}; dispp->fmtp()->timeunit(m_modp->timeunit()); AstNode* const bodysp = dispp; replaceDisplay(dispp, "%%Error"); // Convert to standard DISPLAY format + if (exprsp) dispp->fmtp()->exprsp()->addNext(exprsp); bodysp->addNext(new AstStop{nodep->fileline(), true}); return bodysp; } - AstNode* newFireAssert(AstNode* nodep, const string& message) { - AstNode* bodysp = newFireAssertUnchecked(nodep, message); + AstNode* newFireAssert(AstNode* nodep, const string& message, AstNodeExpr* exprsp = nullptr) { + AstNode* bodysp = newFireAssertUnchecked(nodep, message, exprsp); bodysp = newIfAssertOn(bodysp, false); return bodysp; } @@ -328,20 +330,32 @@ class AssertVisitor final : public VNVisitor { } // Empty case means no property if (!propp) propp = new AstConst{nodep->fileline(), AstConst::BitFalse{}}; - const bool allow_none = has_default || nodep->unique0Pragma(); - AstNodeExpr* const ohot - = (allow_none ? static_cast( - new AstOneHot0{nodep->fileline(), propp}) - : static_cast( - new AstOneHot{nodep->fileline(), propp})); - AstIf* const ifp = new AstIf{ - nodep->fileline(), new AstLogNot{nodep->fileline(), ohot}, - newFireAssert(nodep, - "synthesis parallel_case, but multiple matches found")}; - ifp->isBoundsCheck(true); // To avoid LATCH warning - ifp->branchPred(VBranchPred::BP_UNLIKELY); - nodep->addNotParallelp(ifp); + // The following assertion lools as below. + // if (!$onehot(propp)) begin + // if (propp == '0) begin if (!allow_none) $error("none match"); end + // else $error("multiple match"); + // end + AstNodeExpr* const ohot = new AstOneHot{nodep->fileline(), propp}; + AstIf* const ohotIfp + = new AstIf{nodep->fileline(), new AstLogNot{nodep->fileline(), ohot}}; + AstIf* const zeroIfp + = new AstIf{nodep->fileline(), + new AstLogNot{nodep->fileline(), propp->cloneTreePure(false)}}; + AstNodeExpr* const exprp = nodep->exprp(); + const string pragmaStr = nodep->pragmaString(); + const string valFmt = "'" + cvtToStr(exprp->dtypep()->widthMin()) + "'h%X'"; + if (!allow_none) + zeroIfp->addThensp( + newFireAssert(nodep, pragmaStr + ", but none matched for " + valFmt, + exprp->cloneTreePure(false))); + zeroIfp->addElsesp(newFireAssert( + nodep, pragmaStr + ", but multiple matches found for " + valFmt, + exprp->cloneTreePure(false))); + ohotIfp->addThensp(zeroIfp); + ohotIfp->isBoundsCheck(true); // To avoid LATCH warning + ohotIfp->branchPred(VBranchPred::BP_UNLIKELY); + nodep->addNotParallelp(ohotIfp); } } } diff --git a/src/V3AstNodeOther.h b/src/V3AstNodeOther.h index 15c010103..89481bd76 100644 --- a/src/V3AstNodeOther.h +++ b/src/V3AstNodeOther.h @@ -3560,6 +3560,7 @@ public: void unique0Pragma(bool flag) { m_unique0Pragma = flag; } bool priorityPragma() const { return m_priorityPragma; } void priorityPragma(bool flag) { m_priorityPragma = flag; } + string pragmaString() const; }; class AstGenCase final : public AstNodeCase { // Generate Case statement diff --git a/src/V3AstNodes.cpp b/src/V3AstNodes.cpp index ad9457ed0..b6c3aa1bf 100644 --- a/src/V3AstNodes.cpp +++ b/src/V3AstNodes.cpp @@ -2733,6 +2733,22 @@ AstAlways* AstAssignW::convertToAlways() { return newp; } +string AstCase::pragmaString() const { + if (fullPragma() && parallelPragma()) + return "synthesis full_case parallel_case"; + else if (fullPragma()) + return "synthesis full_case"; + else if (parallelPragma()) + return "synthesis parallel_case"; + else if (uniquePragma()) + return "unique case"; + else if (unique0Pragma()) + return "unique0 case"; + else if (priorityPragma()) + return "priority case"; + return ""; +} + void AstDelay::dump(std::ostream& str) const { this->AstNodeStmt::dump(str); if (isCycleDelay()) str << " [CYCLE]"; diff --git a/test_regress/t/t_assert_inside_cond_bad.out b/test_regress/t/t_assert_inside_cond_bad.out index 5defe9702..2705fd3e2 100644 --- a/test_regress/t/t_assert_inside_cond_bad.out +++ b/test_regress/t/t_assert_inside_cond_bad.out @@ -1,3 +1,3 @@ -[10] %Error: t_assert_inside_cond.v:39: Assertion failed in top.t: synthesis parallel_case, but multiple matches found +[10] %Error: t_assert_inside_cond.v:39: Assertion failed in top.t: unique case, but none matched for '12'h389' %Error: t/t_assert_inside_cond.v:39: Verilog $stop Aborting... diff --git a/test_regress/t/t_assert_synth_parallel.out b/test_regress/t/t_assert_synth_parallel.out index 6ba0e76e8..2958bbba9 100644 --- a/test_regress/t/t_assert_synth_parallel.out +++ b/test_regress/t/t_assert_synth_parallel.out @@ -1,6 +1,6 @@ [0] -Info: t_assert_synth.v:115: top.t.test_info: Start of $info test [0] -Info: t_assert_synth.v:116: top.t.test_info: Middle of $info test [0] -Info: t_assert_synth.v:117: top.t.test_info: End of $info test -[40] %Error: t_assert_synth.v:50: Assertion failed in top.t: synthesis parallel_case, but multiple matches found +[40] %Error: t_assert_synth.v:50: Assertion failed in top.t: synthesis full_case parallel_case, but multiple matches found for '1'h1' %Error: t/t_assert_synth.v:50: Verilog $stop Aborting... diff --git a/test_regress/t/t_assert_synth_parallel_vlt.out b/test_regress/t/t_assert_synth_parallel_vlt.out index b406ba1b3..41a1a77c4 100644 --- a/test_regress/t/t_assert_synth_parallel_vlt.out +++ b/test_regress/t/t_assert_synth_parallel_vlt.out @@ -1,6 +1,6 @@ [0] -Info: t_assert_synth.v:115: top.t.test_info: Start of $info test [0] -Info: t_assert_synth.v:116: top.t.test_info: Middle of $info test [0] -Info: t_assert_synth.v:117: top.t.test_info: End of $info test -[40] %Error: t_assert_synth.v:55: Assertion failed in top.t: synthesis parallel_case, but multiple matches found +[40] %Error: t_assert_synth.v:55: Assertion failed in top.t: synthesis parallel_case, but multiple matches found for '1'h1' %Error: t/t_assert_synth.v:55: Verilog $stop Aborting... diff --git a/test_regress/t/t_assert_unique_case_bad.out b/test_regress/t/t_assert_unique_case_bad.out new file mode 100644 index 000000000..109e2880c --- /dev/null +++ b/test_regress/t/t_assert_unique_case_bad.out @@ -0,0 +1,12 @@ +match_item0 +match_item0 +match_item0 +match_item0 +match_item0 +match_item0 +match_item0 +match_item0 +match_item0 +[90] %Error: t_assert_unique_case_bad.v:36: Assertion failed in top.t: unique case, but multiple matches found for '12'h388' +%Error: t/t_assert_unique_case_bad.v:36: Verilog $stop +Aborting... diff --git a/test_regress/t/t_assert_unique_case_bad.pl b/test_regress/t/t_assert_unique_case_bad.pl new file mode 100755 index 000000000..70f34a0e1 --- /dev/null +++ b/test_regress/t/t_assert_unique_case_bad.pl @@ -0,0 +1,23 @@ +#!/usr/bin/env perl +if (!$::Driver) { use FindBin; exec("$FindBin::Bin/bootstrap.pl", @ARGV, $0); die; } +# DESCRIPTION: Verilator: Verilog Test driver/expect definition +# +# Copyright 2024 by Wilson Snyder. This program is free software; you +# can redistribute it and/or modify it under the terms of either the GNU +# Lesser General Public License Version 3 or the Perl Artistic License +# Version 2.0. +# SPDX-License-Identifier: LGPL-3.0-only OR Artistic-2.0 + +scenarios(simulator => 1); + +compile( + verilator_flags2 => ["-x-assign 0 --assert"], + ); + +execute( + fails => 1, + expect_filename => $Self->{golden_filename}, + ); + +ok(1); +1; diff --git a/test_regress/t/t_assert_unique_case_bad.v b/test_regress/t/t_assert_unique_case_bad.v new file mode 100644 index 000000000..74f9dc775 --- /dev/null +++ b/test_regress/t/t_assert_unique_case_bad.v @@ -0,0 +1,43 @@ +// DESCRIPTION: Verilator: Verilog Test module +// +// This file ONLY is placed under the Creative Commons Public Domain, for +// any use, without warranty, 2024 by Yutetsu TAKATSUKASA. +// SPDX-License-Identifier: CC0-1.0 + +module t (/*AUTOARG*/ + // Outputs + hit, + // Inputs + clk + ); + + input clk; + output logic hit; + + logic [31:0] addr; + logic [11:0] match_item0, match_item1; + int cyc; + + initial addr = 32'h380; + + always @ (posedge clk) begin + cyc <= cyc + 1; + addr <= 32'h380 + cyc; + match_item0 = 12'h 380 + cyc[11:0]; + match_item1 = 12'h 390 - cyc[11:0]; + if (cyc == 9) begin + $write("*-* All Finished *-*\n"); + $finish; + end + end + + always_comb begin + hit = 1; + unique case (addr[11:0]) + match_item0: $display("match_item0"); + match_item1: $display("match_item1"); + default: hit = 0; + endcase + end + +endmodule