Optimize away proven redundant case statement assertions

This is still mostly refactoring of V3Case, but with functional changes.
Decouple the exhaustiveness/overlap analysis from the decision to
convert the case using the fast bitwise testing method. This enables
dropping the 'notParallel' assertions for those we can prove exhaustive
and unique, even if we decide to convert them using the generic if/else
ladder scheme.

src/V3Case.cpp

@@ -129,10 +129,8 @@ public:
 // Case state, as a visitor of each AstNode
 
 class CaseVisitor final : public VNVisitor {
-    // Maximum width we can check for overlaps/exhaustiveness
+    // Maximum width for detailed analysis
-    constexpr static int CASE_OVERLAP_WIDTH = 16;
+    constexpr static int CASE_DETAILS_MAX_WIDTH = 16;
-    // Maximum number of case values for exhaustive analysis/optimization
-    constexpr static int CASE_MAX_VALUES = 1 << CASE_OVERLAP_WIDTH;
     // Levels of priority to be ORed together in top IF tree
     constexpr static int CASE_ENCODER_GROUP_DEPTH = 8;
 
@@ -145,17 +143,37 @@ class CaseVisitor final : public VNVisitor {
     };
 
     // STATE
-    VDouble0 m_statCaseFast;  // Statistic tracking
+    // Statistics tracking, as a struct so can be passed to 'const' methods
-    VDouble0 m_statCaseSlow;  // Statistic tracking
+    struct Stats final {
+        VDouble0 caseFast;  // Cases using fast bit tree method
+        VDouble0 caseGeneric;  // Cases using generic if/else tree method
+        VDouble0 provenAssertions;  // Assertions proven to hold
+    } m_stats;
     const AstNode* m_alwaysp = nullptr;  // Always in which case is located
 
-    // Per-CASE
+    // STATE - per AstCase. Update by 'analyzeCase', treat 'const' otherwise
-    bool m_caseExhaustive = false;  // Proven exhaustive
+    bool m_caseOpaque = false;  // Case statement is opaque (non-packed, or non-const conditions)
-    bool m_caseNoOverlaps = false;  // Proven no overlaps between cases
+    size_t m_caseNConditions = 0;  // Number of conditions in the case statement
-    // Map from value (index) to the CaseRecord that covers this value
+    bool m_caseDetailsValid = false;  // Indicates m_caseDetails is valid
-    std::array<CaseRecord, CASE_MAX_VALUES> m_value2CaseRecord;
+    struct final {
+        bool exhaustive = false;  // Proven exhaustive
+        bool noOverlaps = false;  // Proven no overlaps between cases
+        // Map from value (index) to the CaseRecord that covers this value
+        std::array<CaseRecord, 1U << CASE_DETAILS_MAX_WIDTH> records;
+    } m_caseDetails;
 
     // METHODS
+
+    // Xs in case or casez are impossible due to two state simulations.
+    // Returns true if the item is never possible
+    static bool neverItem(const AstCase* casep, const AstNodeExpr* itemExprp) {
+        const AstConst* const constp = VN_CAST(itemExprp, Const);
+        if (!constp) return false;
+        if (casep->casex() || casep->caseInside()) return false;
+        if (casep->casez()) return constp->num().isAnyX();
+        return constp->num().isFourState();
+    }
+
     // Determine whether we should check case items are complete
     // Returns enum's dtype if should check, nullptr if shouldn't
     static const AstEnumDType* getEnumCompletionCheckDType(const AstCase* const nodep) {
@@ -185,7 +203,7 @@ class CaseVisitor final : public VNVisitor {
             // Check all cases to see if they cover this enum value/pattern
             for (uint32_t i = 0; i < numCases; ++i) {
                 if ((i & mask) != val) continue;  // This case is not for this enum value
-                if (m_value2CaseRecord[i].itemp) continue;  // Covered case
+                if (m_caseDetails.records[i].itemp) continue;  // Covered case
                 // Warn unless unique0 case which allows no-match
                 if (!nodep->unique0Pragma()) {
                     nodep->v3warn(CASEINCOMPLETE,
@@ -203,7 +221,7 @@ class CaseVisitor final : public VNVisitor {
     bool checkExhaustivePacked(AstCase* nodep) {
         const uint32_t numCases = 1UL << nodep->exprp()->width();
         for (uint32_t i = 0; i < numCases; ++i) {
-            if (m_value2CaseRecord[i].itemp) continue;  // Covered case
+            if (m_caseDetails.records[i].itemp) continue;  // Covered case
             if (!nodep->unique0Pragma()) {
                 nodep->v3warn(CASEINCOMPLETE,
                               "Case values incompletely covered (example pattern 0x" << std::hex
@@ -224,50 +242,28 @@ class CaseVisitor final : public VNVisitor {
         return checkExhaustivePacked(nodep);
     }
 
-    bool isCaseTreeFast(AstCase* nodep) {
+    // Analyze each value in the case statement. Updates 'm_caseDetails' and issues warnings.
-        m_caseExhaustive = true;  // TODO: we haven't proven this yet, but is as was before
+    void analyzeCaseDetails(AstCase* nodep) {
-        m_caseNoOverlaps = false;
+        const uint32_t numValues = 1UL << nodep->exprp()->width();
-
+        // Clear case records
-        AstNode* const caseExprp = nodep->exprp();
+        for (uint32_t i = 0; i < numValues; ++i) {
-        if (caseExprp->isDouble() || caseExprp->isString()) return false;
+            m_caseDetails.records[i].itemp = nullptr;
-
+            m_caseDetails.records[i].constp = nullptr;
-        const int caseWidth = caseExprp->width();
+            m_caseDetails.records[i].stmtsp = nullptr;
-        if (!caseWidth) return false;
-        if (caseWidth > CASE_OVERLAP_WIDTH) return false;
-
-        int caseConditions = 0;
-
-        for (AstCaseItem* cip = nodep->itemsp(); cip; cip = VN_AS(cip->nextp(), CaseItem)) {
-            for (AstNode* condp = cip->condsp(); condp; condp = condp->nextp()) {
-                // Can't do anything with non-constants
-                if (!VN_IS(condp, Const)) return false;
-                // Count conditions
-                ++caseConditions;
-            }
-        }
-
-        UINFO(8, "Simple case statement: " << nodep);
-        const uint32_t numCases = 1UL << caseWidth;
-        // Zero list of items for each value
-        for (uint32_t i = 0; i < numCases; ++i) {
-            m_value2CaseRecord[i].itemp = nullptr;
-            m_value2CaseRecord[i].constp = nullptr;
-            m_value2CaseRecord[i].stmtsp = nullptr;
         }
         // Now pick up the values for each assignment
         // We can cheat and use uint32_t's because we only support narrow case's
         bool reportedOverlap = false;
-        bool reportedSubcase = false;
         bool hasDefault = false;
-        m_caseNoOverlaps = true;
+        m_caseDetails.noOverlaps = true;
         for (AstCaseItem* itemp = nodep->itemsp(); itemp;
              itemp = VN_AS(itemp->nextp(), CaseItem)) {
 
             // Default case
             if (itemp->isDefault()) {
                 // Default was moved to be the last item by V3LinkDot. Fill remaining cases
-                for (uint32_t i = 0; i < numCases; ++i) {
+                for (uint32_t i = 0; i < numValues; ++i) {
-                    CaseRecord& caseRecord = m_value2CaseRecord[i];
+                    CaseRecord& caseRecord = m_caseDetails.records[i];
                     if (!caseRecord.itemp) {
                         caseRecord.itemp = itemp;
                         caseRecord.stmtsp = itemp->stmtsp();
@@ -293,10 +289,10 @@ class CaseVisitor final : public VNVisitor {
                 bool foundNewCase = false;
                 const AstConst* firstOverlapConstp = nullptr;
                 uint32_t firstOverlapValue = 0;
-                for (uint32_t i = 0; i < numCases; ++i) {
+                for (uint32_t i = 0; i < numValues; ++i) {
                     if ((i & mask) != val) continue;
 
-                    CaseRecord& caseRecord = m_value2CaseRecord[i];
+                    CaseRecord& caseRecord = m_caseDetails.records[i];
 
                     // If this is the first case that covers this value, record it
                     if (!caseRecord.itemp) {
@@ -314,15 +310,21 @@ class CaseVisitor final : public VNVisitor {
                     if (!firstOverlapConstp) {
                         firstOverlapConstp = caseRecord.constp;
                         firstOverlapValue = i;
-                        m_caseNoOverlaps = false;
+                        m_caseDetails.noOverlaps = false;
                     }
                 }
+
+                // Only report first overlap
+                if (reportedOverlap || !firstOverlapConstp) continue;
+
+                // Report first overlap
                 if (nodep->priorityPragma()) {
-                    // If this is a priority case, we only want to complain if every possible value
+                    // If this is a priority case, we only want to complain if every possible
-                    // for this item is already hit by some other item. This is true if
+                    // value for this item is already hit by some other item. This is true if
-                    // 'foundNewCase' is false. 'firstOverlapConstp' is null when the only covering
+                    // 'foundNewCase' is false. 'firstOverlapConstp' is null when the only
-                    // item is this item itself, which is legal overlap within one item.
+                    // covering item is this item itself, which is legal overlap within one
-                    if (!reportedSubcase && !foundNewCase && firstOverlapConstp) {
+                    // item.
+                    if (!foundNewCase) {
                         iconstp->v3warn(CASEOVERLAP,
                                         "Case item ignored: every matching value is covered "
                                         "by an earlier condition\n"
@@ -330,59 +332,76 @@ class CaseVisitor final : public VNVisitor {
                                             << firstOverlapConstp->warnOther()
                                             << "... Location of previous condition\n"
                                             << firstOverlapConstp->warnContextPrimary());
-                        reportedSubcase = true;
+                        reportedOverlap = true;
                     }
                 } else {
                     // If this case statement doesn't have the priority keyword,
                     // we want to warn on any overlap.
-                    if (!reportedOverlap && firstOverlapConstp) {
+                    std::ostringstream examplePattern;
-                        std::ostringstream examplePattern;
+                    if (iconstp->num().isAnyXZ()) {
-                        if (iconstp->num().isAnyXZ()) {
+                        examplePattern << " (example pattern 0x" << std::hex << firstOverlapValue
-                            examplePattern << " (example pattern 0x" << std::hex
+                                       << ")";
-                                           << firstOverlapValue << ")";
-                        }
-                        iconstp->v3warn(CASEOVERLAP,
-                                        "Case conditions overlap"
-                                            << examplePattern.str() << "\n"
-                                            << iconstp->warnContextPrimary() << '\n'
-                                            << firstOverlapConstp->warnOther()
-                                            << "... Location of overlapping condition\n"
-                                            << firstOverlapConstp->warnContextSecondary());
-                        reportedOverlap = true;
                     }
+                    iconstp->v3warn(CASEOVERLAP,
+                                    "Case conditions overlap"
+                                        << examplePattern.str() << "\n"
+                                        << iconstp->warnContextPrimary() << '\n'
+                                        << firstOverlapConstp->warnOther()
+                                        << "... Location of overlapping condition\n"
+                                        << firstOverlapConstp->warnContextSecondary());
+                    reportedOverlap = true;
                 }
             }
         }
 
         // If there was no default, check exhaustiveness
-        m_caseExhaustive = hasDefault || checkExhaustive(nodep);
+        m_caseDetails.exhaustive = hasDefault || checkExhaustive(nodep);
-        if (!m_caseExhaustive) {
+        // Records now valid
-            m_caseNoOverlaps = false;
+        m_caseDetailsValid = true;
-            return false;
+    }
+
+    // Analyze case statement. Updates 'm_case*' members. Reports warnings.
+    void analyzeCase(AstCase* nodep) {
+        // Reset all analysis results
+        m_caseOpaque = false;
+        m_caseNConditions = 0;
+        m_caseDetailsValid = false;
+
+        AstNode* const caseExprp = nodep->exprp();
+
+        // Mark opaque if not a packed value - TODO: can this be a class?
+        if (caseExprp->isDouble() || caseExprp->isString()) m_caseOpaque = true;
+
+        // Check each condition expression
+        for (AstCaseItem* cip = nodep->itemsp(); cip; cip = VN_AS(cip->nextp(), CaseItem)) {
+            for (AstNode* condp = cip->condsp(); condp; condp = condp->nextp()) {
+                // Count conditions
+                ++m_caseNConditions;
+                // Mark opaque if non-constant condition
+                if (!VN_IS(condp, Const)) m_caseOpaque = true;
+            }
         }
 
-        if (caseConditions <= 3
+        // Nothing else to do if not a packed type, or non-const conditions
-            // Avoid e.g. priority expanders from going crazy in expansion
+        if (m_caseOpaque) return;
-            || (caseWidth >= 8 && (caseConditions <= (caseWidth + 1)))) {
-            return false;  // Not worth simplifying
-        }
 
-        return true;  // All is fine
+        // If small enough, analyse details
+        if (caseExprp->width() <= CASE_DETAILS_MAX_WIDTH) analyzeCaseDetails(nodep);
     }
 
     // TODO: should return AstNodeStmt after #6280
-    AstNode* replaceCaseFastRecurse(AstNodeExpr* cexprp, int msb, uint32_t upperValue) {
+    AstNode* convertCaseFastRecurse(AstNodeExpr* cexprp, int msb, uint32_t upperValue) const {
         // Base case: If reached the last bit, upperValue equals an exact value, just return
         // the statements from that CaseItem. Note: Not cloning here as the caller will do
         // an identity check.
-        if (msb < 0) return m_value2CaseRecord[upperValue].stmtsp;
+        if (msb < 0) return m_caseDetails.records[upperValue].stmtsp;
 
         // Recursive case:
         // Make left and right subtrees assuming cexpr[msb] is 0 and 1 respectively
         const uint32_t upperValue0 = upperValue;
         const uint32_t upperValue1 = upperValue | (1UL << msb);
-        AstNode* tree0p = replaceCaseFastRecurse(cexprp, msb - 1, upperValue0);
+        AstNode* tree0p = convertCaseFastRecurse(cexprp, msb - 1, upperValue0);
-        AstNode* tree1p = replaceCaseFastRecurse(cexprp, msb - 1, upperValue1);
+        AstNode* tree1p = convertCaseFastRecurse(cexprp, msb - 1, upperValue1);
 
         // If same logic on both sides, we can just return one of them
         if (tree0p == tree1p) return tree0p;
@@ -391,7 +410,7 @@ class CaseVisitor final : public VNVisitor {
         {
             bool same = true;
             for (uint32_t a = upperValue0, b = upperValue1; a < upperValue1; ++a, ++b) {
-                if (m_value2CaseRecord[a].stmtsp != m_value2CaseRecord[b].stmtsp) {
+                if (m_caseDetails.records[a].stmtsp != m_caseDetails.records[b].stmtsp) {
                     same = false;
                     break;
                 }
@@ -414,23 +433,23 @@ class CaseVisitor final : public VNVisitor {
         return ifp;
     }
 
+    // CASEx(cexpr,....
+    // ->  tree of IF(msb,  IF(msb-1, 11, 10)
+    //                      IF(msb-1, 01, 00))
     // TODO: should return AstNodeStmt after #6280
-    AstNode* replaceCaseFast(AstCase* nodep) {
+    AstNode* convertCaseFast(AstCase* nodep) const {
-        // CASEx(cexpr,....
-        // ->  tree of IF(msb,  IF(msb-1, 11, 10)
-        //                      IF(msb-1, 01, 00))
         const int caseWidth = nodep->exprp()->width();
-        AstNode* const ifrootp = replaceCaseFastRecurse(nodep->exprp(), caseWidth - 1, 0UL);
+        AstNode* const ifrootp = convertCaseFastRecurse(nodep->exprp(), caseWidth - 1, 0UL);
         return ifrootp && ifrootp->backp() ? ifrootp->cloneTree(true) : ifrootp;
     }
 
+    // Convet case statement using generic if/else tree
+    // CASEx(cexpr,ITEM(icond1,istmts1),ITEM(icond2,istmts2),ITEM(default,istmts3))
+    // ->  IF((cexpr==icond1),istmts1,
+    //                       IF((EQ (AND MASK cexpr) (AND MASK icond1)
+    //                              ,istmts2, istmts3
     // TODO: should return AstNodeStmt after #6280
-    AstNode* replaceCaseComplicated(AstCase* nodep) {
+    AstNode* convertCaseGeneric(AstCase* nodep) const {
-        // CASEx(cexpr,ITEM(icond1,istmts1),ITEM(icond2,istmts2),ITEM(default,istmts3))
-        // ->  IF((cexpr==icond1),istmts1,
-        //                       IF((EQ (AND MASK cexpr) (AND MASK icond1)
-        //                              ,istmts2, istmts3
-
         // We'll do this in two stages.
         // First stage, convert the conditions to the appropriate IF AND terms.
         bool hasDefault = false;
@@ -567,13 +586,38 @@ class CaseVisitor final : public VNVisitor {
         return grouprootp;
     }
 
-    bool neverItem(const AstCase* casep, const AstNodeExpr* itemExprp) {
+    // Convert the given case statement to a representation not using AstCase
-        const AstConst* const constp = VN_CAST(itemExprp, Const);
+    // TODO: should return AstNodeStmt after #6280
-        if (!constp) return false;
+    AstNode* convertCase(AstCase* nodep, Stats& stats) const {
-        // Xs in case or casez are impossible due to two state simulations
+        // Determine if we should use the fast bitwise branching tree method
-        if (casep->casex() || casep->caseInside()) return false;
+        const bool useFastBitTree = [&]() {
-        if (casep->casez()) return constp->num().isAnyX();
+            // Not if disabled
-        return constp->num().isFourState();
+            if (!v3Global.opt.fCase()) return false;
+            // Can't do it without the detailed analysis
+            if (!m_caseDetailsValid) return false;
+            // Can't do it if not exhaustive
+            if (!m_caseDetails.exhaustive) return false;
+            // Not worth doing if there are few conditions
+            if (m_caseNConditions <= 3) return false;
+            // Avoid e.g. priority expanders from going crazy in expansion
+            const size_t caseWidth = nodep->exprp()->width();
+            if (caseWidth >= 8 && m_caseNConditions <= (caseWidth + 1)) return false;
+            // Otherwise use the bit tree
+            return true;
+        }();
+        if (useFastBitTree) {
+            ++stats.caseFast;
+            return convertCaseFast(nodep);
+        }
+
+        // Convert using the generic if/else tree method
+        ++stats.caseGeneric;
+        // If a case statement is exhaustive, presume signals involved aren't forming a latch
+        // TODO: this is broken, but it is as was before
+        if (m_alwaysp && (!m_caseDetailsValid || m_caseDetails.exhaustive)) {
+            m_alwaysp->fileline()->warnOff(V3ErrorCode::LATCH, true);
+        }
+        return convertCaseGeneric(nodep);
     }
 
     // VISITORS
@@ -586,34 +630,24 @@ class CaseVisitor final : public VNVisitor {
         // Convert any children first
         iterateChildren(nodep);
 
-        // Convert the case statement
+        // Analyze this case statement
-        AstNode* replacementp = nullptr;
+        analyzeCase(nodep);
-        if (isCaseTreeFast(nodep) && v3Global.opt.fCase()) {
-            // It's a simple priority encoder or complete statement
-            // we can make a tree of statements to avoid extra comparisons
-            ++m_statCaseFast;
-            replacementp = replaceCaseFast(nodep);
-        } else {
-            // If a case statement is exhaustive, presume signals involved aren't forming a latch
-            // TODO: this is broken, but it is as was before
-            if (m_alwaysp && m_caseExhaustive) {
-                m_alwaysp->fileline()->warnOff(V3ErrorCode::LATCH, true);
-            }
-            ++m_statCaseSlow;
-            m_caseExhaustive = false;
-            m_caseNoOverlaps = false;
-            replacementp = replaceCaseComplicated(nodep);
-        }
 
-        // Take the notParallelp tree under the case statement created by V3Assert
+        // Take the 'notParallelp' statements under the case statement created by V3Assert.
         // If the statement was proven to have no overlaps and all cases covered,
         // it can be removed. Otherwise insert the assertion after the case statement.
-        if (nodep->notParallelp() && (!m_caseExhaustive || !m_caseNoOverlaps)) {
+        if (AstNode* const stmtp = nodep->notParallelp()) {
-            nodep->addNextHere(nodep->notParallelp()->unlinkFrBackWithNext());
+            stmtp->unlinkFrBackWithNext();
+            if (m_caseDetailsValid && m_caseDetails.exhaustive && m_caseDetails.noOverlaps) {
+                ++m_stats.provenAssertions;
+                VL_DO_DANGLING(stmtp->deleteTree(), stmtp);
+            } else {
+                nodep->addNextHere(stmtp);
+            }
         }
 
-        // Replace/remove the case statement
+        // Convert the case statement and replace the original
-        if (replacementp) {
+        if (AstNode* const replacementp = convertCase(nodep, m_stats)) {
             nodep->replaceWith(replacementp);
         } else {
             nodep->unlinkFrBack();
@@ -632,8 +666,9 @@ public:
     // CONSTRUCTORS
     explicit CaseVisitor(AstNetlist* nodep) { iterate(nodep); }
     ~CaseVisitor() override {
-        V3Stats::addStat("Optimizations, Cases parallelized", m_statCaseFast);
+        V3Stats::addStat("Optimizations, Cases parallelized", m_stats.caseFast);
-        V3Stats::addStat("Optimizations, Cases complex", m_statCaseSlow);
+        V3Stats::addStat("Optimizations, Cases complex", m_stats.caseGeneric);
+        V3Stats::addStat("Optimizations, Cases proven assertions", m_stats.provenAssertions);
     }
 };
 

test_regress/t/t_case_unique_overlap.py

@@ -11,8 +11,10 @@ import vltest_bootstrap
 
 test.scenarios('simulator')
 
-test.compile()
+test.compile(verilator_flags2=['--stats'])
 
 test.execute()
 
+test.file_grep(test.stats, r'Optimizations, Cases proven assertions\s+(\d+)', 1)
+
 test.passes()