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

@@ -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<AstNodeExpr*>(
-                               new AstOneHot0{nodep->fileline(), propp})
-                                      : static_cast<AstNodeExpr*>(
-                                          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);
                 }
             }
         }

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

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]";

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...

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...

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...

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...

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;

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