slang::analysis::CaseDecisionDag class

A helper class for building a decision DAG (directed acyclic graph) for case statement exhaustiveness analysis.

The DAG is "built" from a set of case statement clauses, where each clause is an integral constant value.

The DAG is used to determine if a set of clauses covers all possible input values for a given case expression bit width, as well as to identify overlapping and redundant clauses for issuing diagnostics.

Constructors, destructors, conversion operators

CaseDecisionDag(std::span<const SVInt> clauses, uint32_t bitWidth, bool wildcardX, uint32_t maxSteps = UINT32_MAX)
Constructs a new case decision DAG.

Public functions

auto isExhaustive() const -> bool
Indicates whether the DAG is exhaustive, meaning that all possible input values are covered by the case statement clauses.

Public variables

flat_hash_set<ClauseIndex> unreachableClauses
Contains the indices of clauses that are never reachable because some earlier clause subsumes it.
flat_hash_set<std::pair<ClauseIndex, ClauseIndex>> overlappingClauses
Contains pairs of indices that overlap, meaning that some inputs match both clauses.
std::optional<SVInt> counterexample
If the DAG is not exhaustive, this contains a counterexample that demonstrates a value that is not covered by any of the clauses.
bool gaveUp
If true, analyzing the case clauses took more than maxSteps and so the analysis was halted.

Variable documentation

flat_hash_set<std::pair<ClauseIndex, ClauseIndex>> slang::analysis::CaseDecisionDag::overlappingClauses

Contains pairs of indices that overlap, meaning that some inputs match both clauses.

Clauses that are deemed unreachable are not included here.

std::optional<SVInt> slang::analysis::CaseDecisionDag::counterexample

If the DAG is not exhaustive, this contains a counterexample that demonstrates a value that is not covered by any of the clauses.

Otherwise, this is empty.