Improve FSM Detection when state variables are non-enums (#7529)
This commit is contained in:
parent
d5f9385e9c
commit
ce34f1a070
|
|
@ -303,6 +303,19 @@ struct FsmCaseCandidate final {
|
|||
AstVarScope* stateVscp = nullptr; // FSM state variable associated with that candidate.
|
||||
};
|
||||
|
||||
struct StateConstLabel final {
|
||||
string text;
|
||||
bool fromParam = false;
|
||||
size_t stateIndex = 0;
|
||||
};
|
||||
|
||||
struct FsmStateSpace final {
|
||||
std::vector<std::pair<string, int>> states; // User label and encoded value.
|
||||
std::unordered_map<int, StateConstLabel> labels; // Encoded value to user label.
|
||||
string stateVarName; // Pretty tracked FSM state variable name.
|
||||
bool enumBacked = false; // Whether states came from an enum declaration.
|
||||
};
|
||||
|
||||
// Local shared state between the two adjacent FSM coverage phases. Detection
|
||||
// fills this with recovered FSM graphs; lowering consumes the completed graphs
|
||||
// immediately afterward without needing any AST serialization bridge.
|
||||
|
|
@ -606,7 +619,9 @@ class FsmDetectVisitor final : public VNVisitor {
|
|||
AstCond* const rhsp = VN_CAST(assp->rhsp(), Cond);
|
||||
if (!rhsp) return nullptr;
|
||||
AstVarRef* const elsep = VN_CAST(rhsp->elsep(), VarRef);
|
||||
if (!elsep || !exprConstValue(rhsp->thenp(), resetValue)) return nullptr;
|
||||
if (!elsep || constValueStatus(rhsp->thenp(), resetValue) != ConstValueStatus::OK) {
|
||||
return nullptr;
|
||||
}
|
||||
stateVscp = lhsp->varScopep();
|
||||
fromVscp = elsep->varScopep();
|
||||
condp = rhsp->condp();
|
||||
|
|
@ -620,7 +635,7 @@ class FsmDetectVisitor final : public VNVisitor {
|
|||
AstVarRef* const lhsp = VN_AS(assp->lhsp(), VarRef);
|
||||
UASSERT_OBJ(lhsp, assp,
|
||||
"direct constant state assignment lhs should be normalized to a VarRef");
|
||||
if (!exprConstValue(assp->rhsp(), value)) return nullptr;
|
||||
if (constValueStatus(assp->rhsp(), value) != ConstValueStatus::OK) return nullptr;
|
||||
stateVscp = lhsp->varScopep();
|
||||
return assp;
|
||||
}
|
||||
|
|
@ -716,8 +731,8 @@ class FsmDetectVisitor final : public VNVisitor {
|
|||
if (!assp) return false;
|
||||
AstCond* const condp = VN_CAST(assp->rhsp(), Cond);
|
||||
if (!condp) return false;
|
||||
return exprConstValue(condp->thenp(), thenValue)
|
||||
&& exprConstValue(condp->elsep(), elseValue);
|
||||
return constValueStatus(condp->thenp(), thenValue) == ConstValueStatus::OK
|
||||
&& constValueStatus(condp->elsep(), elseValue) == ConstValueStatus::OK;
|
||||
}
|
||||
|
||||
static AstNode* caseItemSupportedArcNode(AstCaseItem* itemp, AstVarScope* stateVscp,
|
||||
|
|
@ -728,7 +743,7 @@ class FsmDetectVisitor final : public VNVisitor {
|
|||
AstNodeAssign* const assp = directStateAssign(itemp->stmtsp(), stateVscp);
|
||||
if (assp) {
|
||||
int toValue = 0;
|
||||
if (exprConstValue(assp->rhsp(), toValue)) return assp;
|
||||
if (constValueStatus(assp->rhsp(), toValue) == ConstValueStatus::OK) return assp;
|
||||
}
|
||||
int thenValue = 0;
|
||||
int elseValue = 0;
|
||||
|
|
@ -753,34 +768,60 @@ class FsmDetectVisitor final : public VNVisitor {
|
|||
return nullptr;
|
||||
}
|
||||
|
||||
// Prefer enum labels in reports; fall back to synthetic labels for forced
|
||||
// non-enum FSMs so coverage points remain human-readable.
|
||||
static string labelForValue(const std::unordered_map<int, string>& labels, int value) {
|
||||
const std::unordered_map<int, string>::const_iterator it = labels.find(value);
|
||||
return it == labels.end() ? ("S" + cvtToStr(value)) : it->second;
|
||||
// Prefer user labels in reports. Forced non-enum FSMs prepopulate synthetic
|
||||
// labels, so all emitted arcs should already have a known label here.
|
||||
static string labelForValue(const std::unordered_map<int, StateConstLabel>& labels,
|
||||
int value) {
|
||||
return labels.at(value).text;
|
||||
}
|
||||
|
||||
// The extractor only models constant-valued state transitions, and by the
|
||||
// time detect runs those values have already been constant-folded.
|
||||
static bool exprConstValue(AstNodeExpr* exprp, int& value) {
|
||||
if (AstConst* const constp = VN_CAST(exprp, Const)) {
|
||||
value = constp->toSInt();
|
||||
return true;
|
||||
enum class ConstValueStatus : uint8_t { OK, NOT_CONST, XZ, WIDE };
|
||||
|
||||
static ConstValueStatus constValueStatus(AstNodeExpr* exprp, int& value) {
|
||||
const AstConst* const constp = VN_CAST(exprp, Const);
|
||||
if (!constp) return ConstValueStatus::NOT_CONST;
|
||||
const V3Number& num = constp->num();
|
||||
if (num.isAnyXZ()) return ConstValueStatus::XZ;
|
||||
// Some callers are still only probing candidate shapes, so wide constants
|
||||
// should reject the candidate instead of reporting a V3Number error.
|
||||
if (constp->width() > 32) return ConstValueStatus::WIDE;
|
||||
value = constp->toSInt();
|
||||
return ConstValueStatus::OK;
|
||||
}
|
||||
|
||||
// Enum-backed FSMs should only use values that were interned as known states.
|
||||
// If a constant transition references some other encoding, warn and skip FSM
|
||||
// instrumentation for that edge rather than silently dropping it or turning
|
||||
// optional coverage into a hard compile failure.
|
||||
static bool validateKnownStateValue(AstNode* nodep, const FsmStateSpace& stateSpace, int value,
|
||||
const string& role) {
|
||||
if (stateSpace.labels.find(value) != stateSpace.labels.end()) return true;
|
||||
if (stateSpace.enumBacked) {
|
||||
const string enumRole = role == "source" ? "case item value" : "assigned value";
|
||||
nodep->v3warn(COVERIGN, "Ignoring unsupported: FSM coverage on enum state variable "
|
||||
+ stateSpace.stateVarName + ": " + enumRole + " "
|
||||
+ cvtToStr(value)
|
||||
+ " is not present in the declared enum");
|
||||
return false;
|
||||
}
|
||||
nodep->v3warn(COVERIGN, "Ignoring unsupported: FSM coverage on non-enum state variable "
|
||||
+ stateSpace.stateVarName + ": " + role + " value "
|
||||
+ cvtToStr(value)
|
||||
+ " is not present in the inferred state space");
|
||||
return false;
|
||||
}
|
||||
|
||||
// Enum-backed FSMs should only transition to values that were interned as
|
||||
// known states. If a constant transition targets some other encoding, warn
|
||||
// and skip FSM instrumentation for that edge rather than silently dropping
|
||||
// it or turning optional coverage into a hard compile failure.
|
||||
static bool validateKnownStateValue(AstNode* nodep,
|
||||
const std::unordered_map<int, string>& labels, int value) {
|
||||
if (labels.find(value) != labels.end()) return true;
|
||||
nodep->v3warn(COVERIGN, "Ignoring unsupported: FSM coverage on enum state transitions "
|
||||
"that assign a constant that is not present in the declared "
|
||||
"enum");
|
||||
return false;
|
||||
static StateConstLabel stateLabelForConst(AstConst* constp) {
|
||||
const string name = constp->origParamName();
|
||||
if (!name.empty()) return StateConstLabel{AstNode::prettyName(name), true, 0};
|
||||
return StateConstLabel{constp->name(), false, 0};
|
||||
}
|
||||
|
||||
static void updateStateLabel(FsmStateSpace& stateSpace, int value,
|
||||
const StateConstLabel& label) {
|
||||
stateSpace.states.at(stateSpace.labels.at(value).stateIndex).first = label.text;
|
||||
}
|
||||
|
||||
// Strict Phase 1 matcher for register processes: either a bare state
|
||||
|
|
@ -839,42 +880,111 @@ class FsmDetectVisitor final : public VNVisitor {
|
|||
return true;
|
||||
}
|
||||
|
||||
// Helper: process a single condition expression and add it to the state space.
|
||||
// Returns true on success, false if the state space is invalid.
|
||||
static bool addCondToStateSpace(AstNodeExpr* condp, FsmStateSpace& stateSpace) {
|
||||
int value = 0;
|
||||
const ConstValueStatus status = constValueStatus(condp, value);
|
||||
if (status != ConstValueStatus::OK) {
|
||||
if (status == ConstValueStatus::XZ) {
|
||||
condp->v3warn(COVERIGN, "Ignoring unsupported: FSM coverage on non-enum "
|
||||
"state variable "
|
||||
+ stateSpace.stateVarName
|
||||
+ " with X/Z state encoding values");
|
||||
}
|
||||
return false;
|
||||
}
|
||||
AstConst* const constp = VN_AS(condp, Const);
|
||||
const StateConstLabel label = stateLabelForConst(constp);
|
||||
const auto labelIt = stateSpace.labels.find(value);
|
||||
if (labelIt != stateSpace.labels.end()) {
|
||||
StateConstLabel& existingLabel = labelIt->second;
|
||||
if (existingLabel.text != label.text && existingLabel.fromParam && label.fromParam) {
|
||||
condp->v3warn(COVERIGN, "Ignoring unsupported: FSM coverage on non-enum "
|
||||
"state variable "
|
||||
+ stateSpace.stateVarName
|
||||
+ " with multiple labels for the same value "
|
||||
+ cvtToStr(value) + ": " + existingLabel.text + " and "
|
||||
+ label.text);
|
||||
return false;
|
||||
}
|
||||
if (!existingLabel.fromParam && label.fromParam) {
|
||||
existingLabel.text = label.text;
|
||||
existingLabel.fromParam = label.fromParam;
|
||||
updateStateLabel(stateSpace, value, label);
|
||||
}
|
||||
} else {
|
||||
StateConstLabel storedLabel = label;
|
||||
storedLabel.stateIndex = stateSpace.states.size();
|
||||
stateSpace.states.emplace_back(label.text, value);
|
||||
stateSpace.labels.emplace(value, storedLabel);
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
// Build the Phase 1 state space from the tracked registered state
|
||||
// variable, not from whichever signal the transition case happened to use.
|
||||
static bool collectStateLabels(AstNode* nodep, AstVarScope* stateVscp,
|
||||
std::vector<std::pair<string, int>>& states,
|
||||
std::unordered_map<int, string>& labels) {
|
||||
static bool collectStateSpace(AstCase* casep, AstVarScope* stateVscp,
|
||||
FsmStateSpace& stateSpace) {
|
||||
AstVar* const stateVarp = stateVscp->varp();
|
||||
AstEnumDType* enump = VN_CAST(unwrapEnumCandidate(stateVscp->dtypep()), EnumDType);
|
||||
if (!enump) enump = VN_CAST(unwrapEnumCandidate(stateVarp->dtypep()), EnumDType);
|
||||
const bool forced = stateVarp->attrFsmState();
|
||||
if (!enump && !forced) return false;
|
||||
stateSpace.stateVarName = stateVscp->prettyNameQ();
|
||||
|
||||
if (enump) {
|
||||
if (stateVscp->width() > 32) {
|
||||
nodep->v3warn(COVERIGN, "Ignoring unsupported: FSM coverage on enum-typed state "
|
||||
"variables wider than 32 bits");
|
||||
casep->v3warn(COVERIGN, "Ignoring unsupported: FSM coverage on enum-typed state "
|
||||
"variable "
|
||||
+ stateSpace.stateVarName + " with width "
|
||||
+ cvtToStr(stateVscp->width())
|
||||
+ " wider than 32 bits");
|
||||
return false;
|
||||
}
|
||||
stateSpace.enumBacked = true;
|
||||
for (AstEnumItem* itemp = enump->itemsp(); itemp;
|
||||
itemp = VN_AS(itemp->nextp(), EnumItem)) {
|
||||
const AstConst* const constp = VN_AS(itemp->valuep(), Const);
|
||||
const int value = constp->toSInt();
|
||||
states.emplace_back(itemp->name(), value);
|
||||
labels.emplace(value, itemp->name());
|
||||
const size_t stateIndex = stateSpace.states.size();
|
||||
stateSpace.states.emplace_back(itemp->name(), value);
|
||||
stateSpace.labels.emplace(value,
|
||||
StateConstLabel{itemp->name(), false, stateIndex});
|
||||
}
|
||||
return states.size() >= 2;
|
||||
return stateSpace.states.size() >= 2;
|
||||
}
|
||||
|
||||
const int width = stateVarp->width();
|
||||
if (width >= 31) return false;
|
||||
const unsigned stateCount = 1U << width;
|
||||
for (unsigned value = 0; value < stateCount; ++value) {
|
||||
const string label = "S" + cvtToStr(value);
|
||||
states.emplace_back(label, static_cast<int>(value));
|
||||
labels.emplace(static_cast<int>(value), label);
|
||||
if (forced) {
|
||||
const int width = stateVarp->width();
|
||||
if (width >= 31) return false;
|
||||
const unsigned stateCount = 1U << width;
|
||||
for (unsigned value = 0; value < stateCount; ++value) {
|
||||
const string label = "S" + cvtToStr(value);
|
||||
const size_t stateIndex = stateSpace.states.size();
|
||||
stateSpace.states.emplace_back(label, static_cast<int>(value));
|
||||
stateSpace.labels.emplace(static_cast<int>(value),
|
||||
StateConstLabel{label, false, stateIndex});
|
||||
}
|
||||
return true;
|
||||
}
|
||||
return true;
|
||||
|
||||
if (stateVscp->width() > 32) {
|
||||
casep->v3warn(COVERIGN, "Ignoring unsupported: FSM coverage on non-enum state "
|
||||
"variable "
|
||||
+ stateSpace.stateVarName + " with width "
|
||||
+ cvtToStr(stateVscp->width()) + " wider than 32 bits");
|
||||
return false;
|
||||
}
|
||||
|
||||
for (AstCaseItem* itemp = casep->itemsp(); itemp;
|
||||
itemp = VN_AS(itemp->nextp(), CaseItem)) {
|
||||
if (itemp->isDefault()) continue;
|
||||
for (AstNodeExpr* condp = itemp->condsp(); condp;
|
||||
condp = VN_AS(condp->nextp(), NodeExpr)) {
|
||||
if (!addCondToStateSpace(condp, stateSpace)) return false;
|
||||
}
|
||||
}
|
||||
return stateSpace.states.size() >= 2;
|
||||
}
|
||||
|
||||
// Extract supported case-item transitions in one place so the conservative
|
||||
|
|
@ -882,25 +992,27 @@ class FsmDetectVisitor final : public VNVisitor {
|
|||
// this helper are deliberate subset boundaries: they document shapes we do
|
||||
// not yet model in this PR and that future FSM-detection work may widen.
|
||||
static bool emitCaseItemArcs(FsmGraph& graph, AstCaseItem* itemp, AstVarScope* stateVscp,
|
||||
const std::unordered_map<int, string>& labels, bool inclCond) {
|
||||
const FsmStateSpace& stateSpace, bool inclCond) {
|
||||
std::vector<std::pair<string, int>> froms;
|
||||
if (itemp->isDefault()) {
|
||||
if (!inclCond) return false;
|
||||
froms.emplace_back("default", 0);
|
||||
} else {
|
||||
for (AstNodeExpr* condp = itemp->condsp(); condp;
|
||||
condp = VN_CAST(condp->nextp(), NodeExpr)) {
|
||||
condp = VN_AS(condp->nextp(), NodeExpr)) {
|
||||
int value = 0;
|
||||
if (!exprConstValue(condp, value)) continue;
|
||||
froms.emplace_back(labelForValue(labels, value), value);
|
||||
if (constValueStatus(condp, value) != ConstValueStatus::OK) continue;
|
||||
if (!validateKnownStateValue(condp, stateSpace, value, "source")) return true;
|
||||
froms.emplace_back(labelForValue(stateSpace.labels, value), value);
|
||||
}
|
||||
if (froms.empty()) return false;
|
||||
}
|
||||
|
||||
if (AstNodeAssign* const assp = directStateAssign(itemp->stmtsp(), stateVscp)) {
|
||||
int toValue = 0;
|
||||
if (exprConstValue(assp->rhsp(), toValue)) {
|
||||
if (!validateKnownStateValue(assp, labels, toValue)) return true;
|
||||
const ConstValueStatus status = constValueStatus(assp->rhsp(), toValue);
|
||||
if (status == ConstValueStatus::OK) {
|
||||
if (!validateKnownStateValue(assp, stateSpace, toValue, "target")) return true;
|
||||
for (const std::pair<string, int>& from : froms) {
|
||||
graph.addArc(from.second, toValue, false, false, itemp->isDefault(),
|
||||
assp->fileline());
|
||||
|
|
@ -913,8 +1025,10 @@ class FsmDetectVisitor final : public VNVisitor {
|
|||
int elseValue = 0;
|
||||
if (directStateCondConstAssign(itemp->stmtsp(), stateVscp, thenValue, elseValue)
|
||||
|| ifStateConstAssign(itemp->stmtsp(), stateVscp, thenValue, elseValue)) {
|
||||
if (!validateKnownStateValue(itemp->stmtsp(), labels, thenValue)) return true;
|
||||
if (!validateKnownStateValue(itemp->stmtsp(), labels, elseValue)) return true;
|
||||
if (!validateKnownStateValue(itemp->stmtsp(), stateSpace, thenValue, "target"))
|
||||
return true;
|
||||
if (!validateKnownStateValue(itemp->stmtsp(), stateSpace, elseValue, "target"))
|
||||
return true;
|
||||
for (const int branchValue : {thenValue, elseValue}) {
|
||||
for (const std::pair<string, int>& from : froms) {
|
||||
graph.addArc(from.second, branchValue, false, true, itemp->isDefault(),
|
||||
|
|
@ -930,9 +1044,11 @@ class FsmDetectVisitor final : public VNVisitor {
|
|||
// Reset transitions are described separately because they live in the reset
|
||||
// branch outside the steady-state case statement.
|
||||
static void addResetArcs(FsmGraph& graph, const std::vector<FsmResetArcDesc>& resetArcs,
|
||||
const std::unordered_map<int, string>& labels) {
|
||||
const FsmStateSpace& stateSpace) {
|
||||
for (const FsmResetArcDesc& resetArc : resetArcs) {
|
||||
if (!validateKnownStateValue(resetArc.nodep(), labels, resetArc.toValue())) continue;
|
||||
if (!validateKnownStateValue(resetArc.nodep(), stateSpace, resetArc.toValue(),
|
||||
"target"))
|
||||
continue;
|
||||
graph.addArc(0, resetArc.toValue(), true, false, false, resetArc.nodep()->fileline());
|
||||
}
|
||||
}
|
||||
|
|
@ -943,9 +1059,8 @@ class FsmDetectVisitor final : public VNVisitor {
|
|||
void processCase(AstCase* casep, AstVarScope* assignVscp, const FsmRegisterCandidate& reg) {
|
||||
UASSERT_OBJ(assignVscp, casep, "FSM case processing requires a non-null assignment var");
|
||||
AstVarScope* const stateVscp = reg.stateVscp();
|
||||
std::vector<std::pair<string, int>> states;
|
||||
std::unordered_map<int, string> labels;
|
||||
if (!collectStateLabels(casep, stateVscp, states, labels)) return;
|
||||
FsmStateSpace stateSpace;
|
||||
if (!collectStateSpace(casep, stateVscp, stateSpace)) return;
|
||||
DetectedFsm& entry = m_state.fsms()[stateVscp];
|
||||
if (!entry.graphp) {
|
||||
entry.graphp.reset(new FsmGraph{});
|
||||
|
|
@ -960,14 +1075,15 @@ class FsmDetectVisitor final : public VNVisitor {
|
|||
entry.graphp->resetInclude(reg.resetInclude());
|
||||
entry.graphp->inclCond(reg.inclCond());
|
||||
entry.graphp->fileline(casep->fileline());
|
||||
for (const std::pair<string, int>& state : states) {
|
||||
for (const std::pair<string, int>& state : stateSpace.states) {
|
||||
entry.graphp->addStateVertex(state.first, state.second);
|
||||
}
|
||||
addResetArcs(*entry.graphp, reg.resetArcs(), labels);
|
||||
addResetArcs(*entry.graphp, reg.resetArcs(), stateSpace);
|
||||
}
|
||||
for (AstCaseItem* itemp = casep->itemsp(); itemp;
|
||||
itemp = VN_AS(itemp->nextp(), CaseItem)) {
|
||||
emitCaseItemArcs(*entry.graphp, itemp, assignVscp, labels, entry.graphp->inclCond());
|
||||
emitCaseItemArcs(*entry.graphp, itemp, assignVscp, stateSpace,
|
||||
entry.graphp->inclCond());
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
%Warning-COVERIGN: t/t_cover_fsm_enumwide_bad.v:26:7: Ignoring unsupported: FSM coverage on enum-typed state variables wider than 32 bits
|
||||
%Warning-COVERIGN: t/t_cover_fsm_enumwide_bad.v:26:7: Ignoring unsupported: FSM coverage on enum-typed state variable 't.state' with width 33 wider than 32 bits
|
||||
26 | case (state)
|
||||
| ^~~~
|
||||
... For warning description see https://verilator.org/warn/COVERIGN?v=latest
|
||||
|
|
|
|||
|
|
@ -1,15 +1,18 @@
|
|||
%Warning-COVERIGN: t/t_cover_fsm_if_unknown_enum_multi_bad.v:26:19: Ignoring unsupported: FSM coverage on enum state transitions that assign a constant that is not present in the declared enum
|
||||
%Warning-COVERIGN: t/t_cover_fsm_if_unknown_enum_multi_bad.v:26:19: Ignoring unsupported: FSM coverage on enum state variable 't.unknown_then_u.state_q': assigned value 3 is not present in the declared enum
|
||||
26 | S0: state_d = sel ? 2'd3 : S1;
|
||||
| ^
|
||||
... For warning description see https://verilator.org/warn/COVERIGN?v=latest
|
||||
... Use "/* verilator lint_off COVERIGN */" and lint_on around source to disable this message.
|
||||
%Warning-COVERIGN: t/t_cover_fsm_if_unknown_enum_multi_bad.v:53:19: Ignoring unsupported: FSM coverage on enum state transitions that assign a constant that is not present in the declared enum
|
||||
%Warning-COVERIGN: t/t_cover_fsm_if_unknown_enum_multi_bad.v:53:19: Ignoring unsupported: FSM coverage on enum state variable 't.unknown_else_u.state_q': assigned value 3 is not present in the declared enum
|
||||
53 | S0: state_d = sel ? S1 : 2'd3;
|
||||
| ^
|
||||
%Warning-COVERIGN: t/t_cover_fsm_if_unknown_enum_multi_bad.v:79:19: Ignoring unsupported: FSM coverage on enum state transitions that assign a constant that is not present in the declared enum
|
||||
%Warning-COVERIGN: t/t_cover_fsm_if_unknown_enum_multi_bad.v:79:19: Ignoring unsupported: FSM coverage on enum state variable 't.unknown_direct_u.state_q': assigned value 3 is not present in the declared enum
|
||||
79 | S0: state_d = 2'd3;
|
||||
| ^
|
||||
%Warning-COVERIGN: t/t_cover_fsm_if_unknown_enum_multi_bad.v:126:15: Ignoring unsupported: FSM coverage on enum state transitions that assign a constant that is not present in the declared enum
|
||||
%Warning-COVERIGN: t/t_cover_fsm_if_unknown_enum_multi_bad.v:126:15: Ignoring unsupported: FSM coverage on enum state variable 't.unknown_reset_u.state_q': assigned value 3 is not present in the declared enum
|
||||
126 | state_q <= 2'd3;
|
||||
| ^~
|
||||
%Warning-COVERIGN: t/t_cover_fsm_if_unknown_enum_multi_bad.v:150:7: Ignoring unsupported: FSM coverage on enum state variable 't.unknown_source_u.state_q': case item value 3 is not present in the declared enum
|
||||
150 | 2'd3: state_d = S0;
|
||||
| ^~~~
|
||||
%Error: Exiting due to
|
||||
|
|
|
|||
|
|
@ -132,10 +132,37 @@ module unknown_reset (
|
|||
end
|
||||
endmodule
|
||||
|
||||
module unknown_source (
|
||||
input logic clk
|
||||
);
|
||||
typedef enum logic [1:0] {
|
||||
S0 = 2'd0,
|
||||
S1 = 2'd1
|
||||
} state_t;
|
||||
|
||||
state_t state_q /*verilator fsm_state*/;
|
||||
state_t state_d;
|
||||
|
||||
always_comb begin
|
||||
state_d = state_q;
|
||||
case (state_q)
|
||||
/* verilator lint_off ENUMVALUE */
|
||||
2'd3: state_d = S0;
|
||||
/* verilator lint_on ENUMVALUE */
|
||||
default: state_d = S0;
|
||||
endcase
|
||||
end
|
||||
|
||||
always_ff @(posedge clk) begin
|
||||
state_q <= state_d;
|
||||
end
|
||||
endmodule
|
||||
|
||||
module t;
|
||||
logic clk;
|
||||
unknown_then unknown_then_u (.clk(clk));
|
||||
unknown_else unknown_else_u (.clk(clk));
|
||||
unknown_direct unknown_direct_u (.clk(clk));
|
||||
unknown_reset unknown_reset_u (.clk(clk));
|
||||
unknown_source unknown_source_u (.clk(clk));
|
||||
endmodule
|
||||
|
|
|
|||
|
|
@ -9,31 +9,35 @@
|
|||
input logic clk
|
||||
);
|
||||
|
||||
typedef enum logic [1:0] {
|
||||
S0 = 2'd0,
|
||||
S1 = 2'd1,
|
||||
S2 = 2'd2
|
||||
typedef enum logic [2:0] {
|
||||
S0 = 3'd0,
|
||||
S1 = 3'd1,
|
||||
S2 = 3'd2
|
||||
} state_t;
|
||||
|
||||
int cyc;
|
||||
logic side;
|
||||
logic [2:0] dyn_case;
|
||||
state_t state /*verilator fsm_reset_arc*/;
|
||||
|
||||
initial begin
|
||||
cyc = 0;
|
||||
side = 1'b0;
|
||||
dyn_case = 3'd7;
|
||||
end
|
||||
|
||||
always @(posedge clk) begin
|
||||
cyc <= cyc + 1;
|
||||
if (cyc == 1) side <= 1'b1;
|
||||
dyn_case <= {2'b11, side};
|
||||
if (cyc == 5) begin
|
||||
$write("*-* All Finished *-*\n");
|
||||
$finish;
|
||||
end
|
||||
end
|
||||
|
||||
// The S0 arm is the supported baseline. The S1 and default arms are
|
||||
// The grouped S0/dyn_case arm keeps the supported S0 baseline while the
|
||||
// non-constant case item is skipped. The S1 and default arms are
|
||||
// deliberately unsupported extractor shapes: one has two meaningful
|
||||
// statements, the other writes a different lhs first. Coverage should ignore
|
||||
// those arcs rather than guessing.
|
||||
|
|
@ -48,7 +52,7 @@
|
|||
%000001 // [fsm_state t.state::S0]
|
||||
%000002 // [fsm_state t.state::S1]
|
||||
%000002 // [fsm_state t.state::S2]
|
||||
S0: state <= S1;
|
||||
S0, state_t'(dyn_case): state <= S1;
|
||||
S1: begin
|
||||
side <= ~side;
|
||||
state <= S2;
|
||||
|
|
|
|||
|
|
@ -8,31 +8,35 @@ module t (
|
|||
input logic clk
|
||||
);
|
||||
|
||||
typedef enum logic [1:0] {
|
||||
S0 = 2'd0,
|
||||
S1 = 2'd1,
|
||||
S2 = 2'd2
|
||||
typedef enum logic [2:0] {
|
||||
S0 = 3'd0,
|
||||
S1 = 3'd1,
|
||||
S2 = 3'd2
|
||||
} state_t;
|
||||
|
||||
int cyc;
|
||||
logic side;
|
||||
logic [2:0] dyn_case;
|
||||
state_t state /*verilator fsm_reset_arc*/;
|
||||
|
||||
initial begin
|
||||
cyc = 0;
|
||||
side = 1'b0;
|
||||
dyn_case = 3'd7;
|
||||
end
|
||||
|
||||
always @(posedge clk) begin
|
||||
cyc <= cyc + 1;
|
||||
if (cyc == 1) side <= 1'b1;
|
||||
dyn_case <= {2'b11, side};
|
||||
if (cyc == 5) begin
|
||||
$write("*-* All Finished *-*\n");
|
||||
$finish;
|
||||
end
|
||||
end
|
||||
|
||||
// The S0 arm is the supported baseline. The S1 and default arms are
|
||||
// The grouped S0/dyn_case arm keeps the supported S0 baseline while the
|
||||
// non-constant case item is skipped. The S1 and default arms are
|
||||
// deliberately unsupported extractor shapes: one has two meaningful
|
||||
// statements, the other writes a different lhs first. Coverage should ignore
|
||||
// those arcs rather than guessing.
|
||||
|
|
@ -42,7 +46,7 @@ module t (
|
|||
end
|
||||
else begin
|
||||
case (state)
|
||||
S0: state <= S1;
|
||||
S0, state_t'(dyn_case): state <= S1;
|
||||
S1: begin
|
||||
side <= ~side;
|
||||
state <= S2;
|
||||
|
|
|
|||
|
|
@ -0,0 +1,69 @@
|
|||
#!/usr/bin/env python3
|
||||
# DESCRIPTION: Verilator: FSM coverage infers non-enum state space
|
||||
#
|
||||
# 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-FileCopyrightText: 2026 Wilson Snyder
|
||||
# SPDX-License-Identifier: LGPL-3.0-only OR Artistic-2.0
|
||||
|
||||
from pathlib import Path
|
||||
|
||||
import vltest_bootstrap
|
||||
|
||||
test.scenarios('vlt')
|
||||
|
||||
test.lint(v_flags=["--coverage-fsm", "--dump-tree"])
|
||||
|
||||
tree_files = [Path(filename) for filename in test.glob_some(test.obj_dir + "/*.tree")]
|
||||
tree_texts = [filename.read_text(encoding="utf8") for filename in tree_files]
|
||||
|
||||
assert any("COVEROTHERDECL" in text and " fv=t.literal_state" in text and " ft=2'h0" in text
|
||||
for text in tree_texts)
|
||||
assert any("COVEROTHERDECL" in text and " fv=t.literal_state" in text and " ft=2'h1" in text
|
||||
for text in tree_texts)
|
||||
assert any("COVEROTHERDECL" in text and " fv=t.literal_state" in text and " ft=2'h2" in text
|
||||
for text in tree_texts)
|
||||
|
||||
assert any("COVEROTHERDECL" in text and " fv=t.param_state" in text and " ft=IDLE" in text
|
||||
for text in tree_texts)
|
||||
assert any("COVEROTHERDECL" in text and " fv=t.param_state" in text and " ft=BUSY" in text
|
||||
for text in tree_texts)
|
||||
assert any("COVEROTHERDECL" in text and " fv=t.param_state" in text and " ft=DONE" in text
|
||||
for text in tree_texts)
|
||||
|
||||
assert any("COVEROTHERDECL" in text and " fv=t.unbased_state" in text and " ft=1'h0" in text
|
||||
for text in tree_texts)
|
||||
assert any("COVEROTHERDECL" in text and " fv=t.unbased_state" in text and " ft=1'h1" in text
|
||||
for text in tree_texts)
|
||||
|
||||
assert any("COVEROTHERDECL" in text and " fv=t.body_symbol_state" in text and " ft=BODY_ID" in text
|
||||
for text in tree_texts)
|
||||
assert any("COVEROTHERDECL" in text and " fv=t.body_symbol_state" in text and " ft=BODY$ID" in text
|
||||
for text in tree_texts)
|
||||
|
||||
assert any("COVEROTHERDECL" in text and " fv=t.multiline_expr_state" in text and " ft=2'h0" in text
|
||||
for text in tree_texts)
|
||||
assert any("COVEROTHERDECL" in text and " fv=t.multiline_expr_state" in text and " ft=2'h1" in text
|
||||
for text in tree_texts)
|
||||
|
||||
assert any("COVEROTHERDECL" in text and " fv=t.duplicate_expr_state" in text and " ft=IDLE" in text
|
||||
for text in tree_texts)
|
||||
assert any("COVEROTHERDECL" in text and " fv=t.duplicate_expr_state" in text and " ft=BUSY" in text
|
||||
for text in tree_texts)
|
||||
|
||||
assert any(
|
||||
"COVEROTHERDECL" in text and " fv=t.duplicate_same_label_state" in text and " ft=IDLE" in text
|
||||
for text in tree_texts)
|
||||
assert any(
|
||||
"COVEROTHERDECL" in text and " fv=t.duplicate_same_label_state" in text and " ft=BUSY" in text
|
||||
for text in tree_texts)
|
||||
|
||||
assert any(
|
||||
"COVEROTHERDECL" in text and " fv=t.duplicate_expr_first_state" in text and " ft=IDLE" in text
|
||||
for text in tree_texts)
|
||||
assert any(
|
||||
"COVEROTHERDECL" in text and " fv=t.duplicate_expr_first_state" in text and " ft=BUSY" in text
|
||||
for text in tree_texts)
|
||||
|
||||
test.passes()
|
||||
|
|
@ -0,0 +1,147 @@
|
|||
// DESCRIPTION: Verilator: FSM coverage infers non-enum state space
|
||||
//
|
||||
// This file ONLY is placed under the Creative Commons Public Domain.
|
||||
// SPDX-FileCopyrightText: 2026 Wilson Snyder
|
||||
// SPDX-License-Identifier: CC0-1.0
|
||||
|
||||
module t (
|
||||
input logic clk,
|
||||
input logic rst,
|
||||
input logic start
|
||||
);
|
||||
|
||||
localparam logic [1:0] IDLE = 2'h0;
|
||||
localparam logic [1:0] BUSY = 2'h1;
|
||||
localparam logic [1:0] DONE = 2'h2;
|
||||
localparam logic [1:0] BODY_ID = 2'h0;
|
||||
localparam logic [1:0] BODY$ID = 2'h1;
|
||||
|
||||
logic [1:0] literal_state;
|
||||
logic [1:0] param_state;
|
||||
logic unbased_state;
|
||||
logic [1:0] body_symbol_state;
|
||||
logic [1:0] multiline_expr_state;
|
||||
logic [1:0] duplicate_expr_state;
|
||||
logic [1:0] duplicate_same_label_state;
|
||||
logic [1:0] duplicate_expr_first_state;
|
||||
|
||||
always_ff @(posedge clk) begin
|
||||
if (rst) begin
|
||||
literal_state <= 2'h0;
|
||||
end
|
||||
else begin
|
||||
case (literal_state)
|
||||
2'h0: literal_state <= start ? 2'h1 : 2'h0;
|
||||
2'h1: literal_state <= 2'h2;
|
||||
2'h2: literal_state <= 2'h2;
|
||||
default: literal_state <= 2'h0;
|
||||
endcase
|
||||
end
|
||||
end
|
||||
|
||||
always_ff @(posedge clk) begin
|
||||
if (rst) begin
|
||||
param_state <= IDLE;
|
||||
end
|
||||
else begin
|
||||
case (param_state)
|
||||
IDLE: param_state <= start ? BUSY : IDLE;
|
||||
BUSY: param_state <= DONE;
|
||||
DONE: param_state <= DONE;
|
||||
default: param_state <= IDLE;
|
||||
endcase
|
||||
end
|
||||
end
|
||||
|
||||
always_ff @(posedge clk) begin
|
||||
if (rst) begin
|
||||
unbased_state <= '0;
|
||||
end
|
||||
else begin
|
||||
case (unbased_state)
|
||||
'0: unbased_state <= '1;
|
||||
'1: unbased_state <= '0;
|
||||
default: unbased_state <= '0;
|
||||
endcase
|
||||
end
|
||||
end
|
||||
|
||||
always_ff @(posedge clk) begin
|
||||
if (rst) begin
|
||||
body_symbol_state <= BODY_ID;
|
||||
end
|
||||
else begin
|
||||
case (body_symbol_state)
|
||||
BODY_ID
|
||||
: body_symbol_state <= BODY$ID;
|
||||
BODY$ID: body_symbol_state <= BODY_ID;
|
||||
default: body_symbol_state <= BODY_ID;
|
||||
endcase
|
||||
end
|
||||
end
|
||||
|
||||
always_ff @(posedge clk) begin
|
||||
if (rst) begin
|
||||
multiline_expr_state <= 2'h0;
|
||||
end
|
||||
else begin
|
||||
case (multiline_expr_state)
|
||||
(2'h0
|
||||
+ 2'h0): multiline_expr_state <= 2'h1;
|
||||
2'h1: multiline_expr_state <= 2'h0;
|
||||
default: multiline_expr_state <= 2'h0;
|
||||
endcase
|
||||
end
|
||||
end
|
||||
|
||||
always_ff @(posedge clk) begin
|
||||
if (rst) begin
|
||||
duplicate_expr_state <= IDLE;
|
||||
end
|
||||
else begin
|
||||
/* verilator lint_off CASEOVERLAP */
|
||||
case (duplicate_expr_state)
|
||||
IDLE: duplicate_expr_state <= BUSY;
|
||||
(2'h0
|
||||
+ 2'h0): duplicate_expr_state <= BUSY;
|
||||
BUSY: duplicate_expr_state <= IDLE;
|
||||
default: duplicate_expr_state <= IDLE;
|
||||
endcase
|
||||
/* verilator lint_on CASEOVERLAP */
|
||||
end
|
||||
end
|
||||
|
||||
always_ff @(posedge clk) begin
|
||||
if (rst) begin
|
||||
duplicate_same_label_state <= IDLE;
|
||||
end
|
||||
else begin
|
||||
/* verilator lint_off CASEOVERLAP */
|
||||
case (duplicate_same_label_state)
|
||||
IDLE: duplicate_same_label_state <= BUSY;
|
||||
IDLE: duplicate_same_label_state <= BUSY;
|
||||
BUSY: duplicate_same_label_state <= IDLE;
|
||||
default: duplicate_same_label_state <= IDLE;
|
||||
endcase
|
||||
/* verilator lint_on CASEOVERLAP */
|
||||
end
|
||||
end
|
||||
|
||||
always_ff @(posedge clk) begin
|
||||
if (rst) begin
|
||||
duplicate_expr_first_state <= 2'h0;
|
||||
end
|
||||
else begin
|
||||
/* verilator lint_off CASEOVERLAP */
|
||||
case (duplicate_expr_first_state)
|
||||
(2'h0
|
||||
+ 2'h0): duplicate_expr_first_state <= BUSY;
|
||||
IDLE: duplicate_expr_first_state <= BUSY;
|
||||
BUSY: duplicate_expr_first_state <= 2'h0;
|
||||
default: duplicate_expr_first_state <= 2'h0;
|
||||
endcase
|
||||
/* verilator lint_on CASEOVERLAP */
|
||||
end
|
||||
end
|
||||
|
||||
endmodule
|
||||
|
|
@ -0,0 +1,15 @@
|
|||
%Warning-COVERIGN: t/t_cover_fsm_nonenum_unsupported_bad.v:32:7: Ignoring unsupported: FSM coverage on non-enum state variable 't.wide_state' with width 33 wider than 32 bits
|
||||
32 | case (wide_state)
|
||||
| ^~~~
|
||||
... For warning description see https://verilator.org/warn/COVERIGN?v=latest
|
||||
... Use "/* verilator lint_off COVERIGN */" and lint_on around source to disable this message.
|
||||
%Warning-COVERIGN: t/t_cover_fsm_nonenum_unsupported_bad.v:47:28: Ignoring unsupported: FSM coverage on non-enum state variable 't.target_state': target value 2 is not present in the inferred state space
|
||||
47 | 2'h1: target_state <= 2'h2;
|
||||
| ^~
|
||||
%Warning-COVERIGN: t/t_cover_fsm_nonenum_unsupported_bad.v:61:9: Ignoring unsupported: FSM coverage on non-enum state variable 't.duplicate_state' with multiple labels for the same value 0: IDLE and RESET
|
||||
61 | RESET: duplicate_state <= IDLE;
|
||||
| ^~~~~
|
||||
%Warning-COVERIGN: t/t_cover_fsm_nonenum_unsupported_bad.v:77:9: Ignoring unsupported: FSM coverage on non-enum state variable 't.xz_case_state' with X/Z state encoding values
|
||||
77 | 2'b1x: xz_case_state <= 2'h0;
|
||||
| ^~~~~
|
||||
%Error: Exiting due to
|
||||
|
|
@ -0,0 +1,16 @@
|
|||
#!/usr/bin/env python3
|
||||
# DESCRIPTION: Verilator: FSM coverage warns on unsupported non-enum state spaces
|
||||
#
|
||||
# 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-FileCopyrightText: 2026 Wilson Snyder
|
||||
# SPDX-License-Identifier: LGPL-3.0-only OR Artistic-2.0
|
||||
|
||||
import vltest_bootstrap
|
||||
|
||||
test.scenarios('vlt')
|
||||
|
||||
test.lint(verilator_flags2=["--coverage-fsm"], fails=True, expect_filename=test.golden_filename)
|
||||
|
||||
test.passes()
|
||||
|
|
@ -0,0 +1,155 @@
|
|||
// DESCRIPTION: Verilator: FSM coverage warns on unsupported non-enum state spaces
|
||||
//
|
||||
// This file ONLY is placed under the Creative Commons Public Domain.
|
||||
// SPDX-FileCopyrightText: 2026 Wilson Snyder
|
||||
// SPDX-License-Identifier: CC0-1.0
|
||||
|
||||
module t (
|
||||
input logic clk,
|
||||
input logic rst,
|
||||
input logic start
|
||||
);
|
||||
|
||||
localparam logic [1:0] IDLE = 2'h0;
|
||||
localparam logic [1:0] RESET = 2'h0;
|
||||
localparam logic [1:0] BUSY = 2'h1;
|
||||
localparam logic [1:0] _IDLE = 2'h0;
|
||||
|
||||
logic [32:0] wide_state;
|
||||
logic [1:0] target_state;
|
||||
logic [1:0] duplicate_state;
|
||||
logic [1:0] xz_case_state;
|
||||
logic [1:0] duplicate_literal_state;
|
||||
logic [1:0] underscore_state;
|
||||
logic [1:0] xz_reset_probe_state;
|
||||
logic [1:0] xz_rhs_probe_state;
|
||||
|
||||
always_ff @(posedge clk) begin
|
||||
if (rst) begin
|
||||
wide_state <= 33'h0;
|
||||
end
|
||||
else begin
|
||||
case (wide_state)
|
||||
33'h0: wide_state <= 33'h1;
|
||||
33'h1: wide_state <= 33'h0;
|
||||
default: wide_state <= 33'h0;
|
||||
endcase
|
||||
end
|
||||
end
|
||||
|
||||
always_ff @(posedge clk) begin
|
||||
if (rst) begin
|
||||
target_state <= 2'h0;
|
||||
end
|
||||
else begin
|
||||
case (target_state)
|
||||
2'h0: target_state <= 2'h1;
|
||||
2'h1: target_state <= 2'h2;
|
||||
default: target_state <= 2'h0;
|
||||
endcase
|
||||
end
|
||||
end
|
||||
|
||||
always_ff @(posedge clk) begin
|
||||
if (rst) begin
|
||||
duplicate_state <= IDLE;
|
||||
end
|
||||
else begin
|
||||
/* verilator lint_off CASEOVERLAP */
|
||||
case (duplicate_state)
|
||||
IDLE: duplicate_state <= start ? BUSY : IDLE;
|
||||
RESET: duplicate_state <= IDLE;
|
||||
BUSY: duplicate_state <= IDLE;
|
||||
default: duplicate_state <= IDLE;
|
||||
endcase
|
||||
/* verilator lint_on CASEOVERLAP */
|
||||
end
|
||||
end
|
||||
|
||||
always_ff @(posedge clk) begin
|
||||
if (rst) begin
|
||||
xz_case_state <= 2'h0;
|
||||
end
|
||||
else begin
|
||||
/* verilator lint_off CASEWITHX */
|
||||
case (xz_case_state)
|
||||
2'h0: xz_case_state <= 2'h1;
|
||||
2'b1x: xz_case_state <= 2'h0;
|
||||
default: xz_case_state <= 2'h0;
|
||||
endcase
|
||||
/* verilator lint_on CASEWITHX */
|
||||
end
|
||||
end
|
||||
|
||||
always_ff @(posedge clk) begin
|
||||
if (rst) begin
|
||||
duplicate_literal_state <= 2'h0;
|
||||
end
|
||||
else begin
|
||||
/* verilator lint_off CASEOVERLAP */
|
||||
case (duplicate_literal_state)
|
||||
2'h0: duplicate_literal_state <= start ? 2'h1 : 2'h0;
|
||||
2'h0: duplicate_literal_state <= 2'h0;
|
||||
2'h1: duplicate_literal_state <= 2'h0;
|
||||
default: duplicate_literal_state <= 2'h0;
|
||||
endcase
|
||||
/* verilator lint_on CASEOVERLAP */
|
||||
end
|
||||
end
|
||||
|
||||
always_ff @(posedge clk) begin
|
||||
if (rst) begin
|
||||
underscore_state <= _IDLE;
|
||||
end
|
||||
else begin
|
||||
case (underscore_state)
|
||||
_IDLE: underscore_state <= BUSY;
|
||||
BUSY: underscore_state <= _IDLE;
|
||||
default: underscore_state <= _IDLE;
|
||||
endcase
|
||||
end
|
||||
end
|
||||
|
||||
always_ff @(posedge clk) begin
|
||||
if (rst) begin
|
||||
xz_reset_probe_state <= 2'b0x;
|
||||
end
|
||||
else begin
|
||||
case (xz_reset_probe_state)
|
||||
2'h0: xz_reset_probe_state <= 2'h1;
|
||||
2'h1: xz_reset_probe_state <= 2'h0;
|
||||
default: xz_reset_probe_state <= 2'h0;
|
||||
endcase
|
||||
end
|
||||
end
|
||||
|
||||
always_ff @(posedge clk) begin
|
||||
if (rst) begin
|
||||
xz_rhs_probe_state <= 2'h0;
|
||||
end
|
||||
else begin
|
||||
case (xz_rhs_probe_state)
|
||||
2'h0: xz_rhs_probe_state <= 2'b0x;
|
||||
2'h1: xz_rhs_probe_state <= 2'h0;
|
||||
default: xz_rhs_probe_state <= 2'h0;
|
||||
endcase
|
||||
end
|
||||
end
|
||||
|
||||
logic [1:0] not_const_item_state;
|
||||
|
||||
always_ff @(posedge clk) begin
|
||||
if (rst) begin
|
||||
not_const_item_state <= 2'h0;
|
||||
end
|
||||
else begin
|
||||
case (not_const_item_state)
|
||||
2'h0: not_const_item_state <= 2'h1;
|
||||
{1'b0, start}: not_const_item_state <= 2'h0;
|
||||
2'h1: not_const_item_state <= 2'h0;
|
||||
default: not_const_item_state <= 2'h0;
|
||||
endcase
|
||||
end
|
||||
end
|
||||
|
||||
endmodule
|
||||
Loading…
Reference in New Issue