P3.2: source precedence + model-vs-netlist conflict check

Rank the spec sources (spec_source_rank: UserOverride > Bsdl > ConnectorModel
> Inferred > Imported); apply_model now refuses to overwrite a spec owned by a
higher-rank source, so one model never clobbers a more authoritative one. New
check_source_conflicts(System*) emits SourceConflict for a pin the BSDL
declares power/ground (a must-connect rail) that the netlist leaves
unconnected — a rail floated in the schematic; surfaced as a sixth `verify`
pass. Unit tests (75 cases) green; the real 8-card system reports 0 conflicts
(its rails are all connected) while the JTAG findings remain.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
This commit is contained in:
2026-06-03 16:08:28 +02:00
parent cb61e9b084
commit fe5b2c3d96
10 changed files with 120 additions and 8 deletions

View File

@@ -129,9 +129,9 @@ The explore screen shows the type in the signal detail header.
**BSDL models (`attach-bsdl`)**: `attach-bsdl <module> <part> <file.bsd>` parses a BSDL device through `libbsdl` (wrapped by `BsdlModel`, `src/system/bsdl_model.{hpp,cpp}`), then `apply_bsdl(part, model)` binds each port to a Pin **by port name first, then by physical pad** — so a netlist that names IC pins either by signal or by package ball both bind. Each bound pin gets its `spec` set: `direction` (BSDL in/out/inout/linkage), `function` (TAP role → Jtag\*, `linkage` → Power/Ground/NoConnect by name, else Signal), `pad` (PIN_MAP ball), `source = Bsdl`. The `.bsd` path is stored on `Part::bsdl_path`, persisted via the `B` tag and re-applied on `restore`. Real-world check: an `xcku15p` FPGA in a VPX system binds 1517/1517 ports.
**Unified application (`apply_model`)**: connector layout and BSDL are two implementations of one `PinModel` interface (`src/system/pin_model.{hpp,cpp}`: `spec_for(pin_name)`, `layout()`, `source()`). `ConnectorModel` wraps `pin_role`/`pin_layout`; `BsdlPinModel` wraps a parsed `BsdlModel`, indexed by both port name and physical pad. A single `apply_model(Part*, const PinModel&)` materialises the layout pins missing from the netlist, then sets each pin's `spec` **only where the model speaks** (`spec.source != None`) — so one source never clobbers another's. `set-connector-type` and `attach-bsdl` both funnel through it (the latter via the thin `apply_bsdl` adapter); `verify` stays agnostic of where a spec came from. A future SPICE/Modelica source would be a third `PinModel`.
**Unified application (`apply_model`)**: connector layout and BSDL are two implementations of one `PinModel` interface (`src/system/pin_model.{hpp,cpp}`: `spec_for(pin_name)`, `layout()`, `source()`). `ConnectorModel` wraps `pin_role`/`pin_layout`; `BsdlPinModel` wraps a parsed `BsdlModel`, indexed by both port name and physical pad. A single `apply_model(Part*, const PinModel&)` materialises the layout pins missing from the netlist, then sets each pin's `spec` **only where the model speaks** (`spec.source != None`). Sources are ranked (`spec_source_rank` in `pin_spec.hpp`: UserOverride > Bsdl > ConnectorModel > Inferred > Imported) and apply_model refuses to overwrite a spec owned by a higher-rank source — so one source never clobbers a more authoritative one, which is also the basis for `check_source_conflicts`. `set-connector-type` and `attach-bsdl` both funnel through it (the latter via the thin `apply_bsdl` adapter); `verify` stays agnostic of where a spec came from. A future SPICE/Modelica source would be a third `PinModel`.
**`verify` (five passes)**: (1) typed pins — local mismatch between each pin's `expected_signal_type()` (derived from its `PinSpec`) and the actual signal type; (2) bridged nets — Power↔GndShield inconsistencies; (3) orphan summary `N orphan pin(s) at import (X imported NC, Y dropped singleton)` (filters out pins bridged via any `Connection::pin_map` — typically `FillIdentityNCs`-materialised); (4) **model-driven pin checks** (`check_pin_specs`): `DriveContention` (≥2 push-pull `Out` on a net), `UndrivenNet` (a **fully-modelled** net with input(s) but no driver — nets with any Unknown-direction pin are skipped, so un-modelled drivers don't cause false positives), `NcWired` (a no-connect pin on a multi-pin net); (5) **JTAG chain** (`check_jtag_chain`): collects TAP pins by `spec.function`, maps each to its net, emits `JtagTapIncomplete` / `JtagBusUnbridged` (TMS or TCK not common to all TAP devices) / `JtagChainBreak` (dangling TDO/TDI, chain fan-out, or not a single head→tail daisy chain). The BFS-reached `(module, signal)` set for any signal is shown live in `explore`'s detail pane when a signal entry is selected.
**`verify` (six passes)**: (1) typed pins — local mismatch between each pin's `expected_signal_type()` (derived from its `PinSpec`) and the actual signal type; (2) bridged nets — Power↔GndShield inconsistencies; (3) orphan summary `N orphan pin(s) at import (X imported NC, Y dropped singleton)` (filters out pins bridged via any `Connection::pin_map` — typically `FillIdentityNCs`-materialised); (4) **model-driven pin checks** (`check_pin_specs`): `DriveContention` (≥2 push-pull `Out` on a net), `UndrivenNet` (a **fully-modelled** net with input(s) but no driver — nets with any Unknown-direction pin are skipped, so un-modelled drivers don't cause false positives), `NcWired` (a no-connect pin on a multi-pin net); (5) **JTAG chain** (`check_jtag_chain`): collects TAP pins by `spec.function`, maps each to its net, emits `JtagTapIncomplete` / `JtagBusUnbridged` (TMS or TCK not common to all TAP devices) / `JtagChainBreak` (dangling TDO/TDI, chain fan-out, or not a single head→tail daisy chain); (6) **source conflicts** (`check_source_conflicts`): a pin the BSDL declares power/ground (a must-connect rail) that the netlist leaves unconnected — a rail floated in the schematic (`SourceConflict`; the reverse, a BSDL no-connect that *is* wired, is the `NcWired` check). The BFS-reached `(module, signal)` set for any signal is shown live in `explore`'s detail pane when a signal entry is selected.
**`analyze` (post-processing pass)**: `analyze_system(System*) → AnalysisReport` (`src/system/analysis.{hpp,cpp}`) is a stateless read-only pass that detects structural signal groups and anomalies. Per-module (signals are module-scoped):
@@ -299,7 +299,7 @@ The analyze screen additionally surfaces two "verify-class" issues, computed the
- **pin-role mismatch** — a pin whose `expected_signal_type()` (derived from its `PinSpec`, set by `set-connector-type` via `pin_role(connector_type, pin_name)`) disagrees with the actual signal type.
- **net-mix** — a bridged net (BFS over `Connection::pin_map`, ≥ 2 members) where `net_type_consistent(net, &dominant)` returns false. Specifically, the net contains both `Power` and `GndShield` signals.
The `verify` command (not the analyze screen, yet) also emits the **model-driven `AnomalyKind`s** from `bsdl_check.{hpp,cpp}`: `DriveContention` / `UndrivenNet` / `NcWired` (`check_pin_specs`) and `JtagTapIncomplete` / `JtagChainBreak` / `JtagBusUnbridged` (`check_jtag_chain`). They consume the BSDL-populated `PinSpec` plus `compute_all_nets`. Surfacing them in the analyze/dashboard Issues pane is a TODO.
The `verify` command (not the analyze screen, yet) also emits the **model-driven `AnomalyKind`s** from `bsdl_check.{hpp,cpp}`: `DriveContention` / `UndrivenNet` / `NcWired` (`check_pin_specs`) and `JtagTapIncomplete` / `JtagChainBreak` / `JtagBusUnbridged` (`check_jtag_chain`); and `SourceConflict` (`check_source_conflicts` — a BSDL power/ground pin the netlist leaves unconnected). They consume the BSDL-populated `PinSpec` plus `compute_all_nets`. Surfacing them in the analyze/dashboard Issues pane is a TODO.
### Component kind

View File

@@ -29,6 +29,7 @@ const char *anomaly_kind_name(AnomalyKind k) {
case AnomalyKind::JtagTapIncomplete: return "jtag-tap-incomplete";
case AnomalyKind::JtagChainBreak: return "jtag-chain-break";
case AnomalyKind::JtagBusUnbridged: return "jtag-bus-unbridged";
case AnomalyKind::SourceConflict: return "source-conflict";
}
return "?";
}

View File

@@ -37,6 +37,7 @@ enum class AnomalyKind {
JtagTapIncomplete, ///< A TAP device is missing one of TDI/TDO/TMS/TCK.
JtagChainBreak, ///< The TDO→TDI daisy chain is broken / not a single path.
JtagBusUnbridged, ///< TMS or TCK is not common to all TAP devices.
SourceConflict, ///< A model contradicts the netlist (e.g. BSDL power pin left NC).
};
struct Anomaly {

View File

@@ -1,5 +1,6 @@
#include "bsdl_check.hpp"
#include "connect.hpp"
#include "modules.hpp"
#include "nets.hpp"
#include "parts.hpp"
@@ -10,6 +11,7 @@
#include <string>
#include <unordered_map>
#include <unordered_set>
#include <utility>
#include <vector>
@@ -277,3 +279,43 @@ std::vector<Anomaly> check_jtag_chain(System *sys)
return out;
}
std::vector<Anomaly> check_source_conflicts(System *sys)
{
std::vector<Anomaly> out;
if (!sys)
return out;
// Pins bridged to a peer signal through a connection count as connected.
std::unordered_set<Pin *> bridged;
for (auto &ckv : *sys->connections())
for (auto &wp : ckv.second->pin_map) {
if (wp.first) bridged.insert(wp.first);
if (wp.second) bridged.insert(wp.second);
}
for (auto &mkv : *sys->modules())
for (auto &pkv : *mkv.second)
for (auto &nkv : *pkv.second) {
Pin *pin = nkv.second;
if (pin->spec.source != SpecSource::Bsdl)
continue;
PinFunction f = pin->spec.function;
if (f != PinFunction::Power && f != PinFunction::Ground)
continue; // only must-connect rails are a clear defect
if (pin->connected() || bridged.count(pin))
continue;
Anomaly a;
a.kind = AnomalyKind::SourceConflict;
a.module = (pin->prnt) ? pin->prnt->prnt : nullptr;
a.message = pin_label(pin) + ": BSDL says "
+ (f == PinFunction::Power ? "power" : "ground")
+ " but the netlist leaves it unconnected"
+ (pin->nc_origin == NcOrigin::ImportedUnconnected
? " (marked NC at import)" : "");
out.push_back(std::move(a));
}
return out;
}

View File

@@ -25,4 +25,10 @@ std::vector<Anomaly> check_pin_specs(System *sys);
// Empty when the system has no TAP pins.
std::vector<Anomaly> check_jtag_chain(System *sys);
// Conflicts between a device model and the netlist's own view of a pin. Today:
// a pin the BSDL declares power/ground (a must-connect rail) that the netlist
// leaves unconnected (no signal and not bridged) — i.e. a rail floated in the
// schematic. The reverse (BSDL no-connect wired in the netlist) is `NcWired`.
std::vector<Anomaly> check_source_conflicts(System *sys);
#endif // _BSDL_CHECK_HPP_

View File

@@ -30,14 +30,17 @@ ApplyReport apply_model(Part *part, const PinModel &model)
}
}
// 2. Set each pin's spec where the model speaks for it.
// 2. Set each pin's spec where the model speaks for it — but never overwrite
// a spec already owned by a higher-precedence source (see spec_source_rank).
r.pins_total = (int)part->size();
for (auto &kv : *part) {
PinSpec s = model.spec_for(kv.first);
if (s.source != SpecSource::None) {
kv.second->spec = s;
++r.set;
}
if (s.source == SpecSource::None)
continue;
if (spec_source_rank(s.source) < spec_source_rank(kv.second->spec.source))
continue;
kv.second->spec = s;
++r.set;
}
return r;
}

View File

@@ -51,4 +51,21 @@ inline PinFunction function_from_signal_type(SignalType t)
}
}
// Precedence of spec sources: a higher rank wins when two sources speak for the
// same pin. A user override beats any model; a device model (BSDL) beats a
// connector layout; both beat plain import / inference. Used by apply_model to
// avoid clobbering a more authoritative spec.
inline int spec_source_rank(SpecSource s)
{
switch (s) {
case SpecSource::None: return 0;
case SpecSource::Imported: return 1;
case SpecSource::Inferred: return 2;
case SpecSource::ConnectorModel: return 3;
case SpecSource::Bsdl: return 4;
case SpecSource::UserOverride: return 5;
}
return 0;
}
#endif // _PIN_SPEC_HPP_

View File

@@ -312,6 +312,13 @@ void Tui::RegisterCommands() {
Print(" [" + std::string(anomaly_kind_name(a.kind)) + "] " + a.message);
Print("verify: " + std::to_string(jtag_anoms.size())
+ " JTAG chain anomaly(ies).");
// Model-vs-netlist conflicts (e.g. a BSDL power pin left unconnected).
auto conflict_anoms = check_source_conflicts(sys.get());
for (const auto &a : conflict_anoms)
Print(" [" + std::string(anomaly_kind_name(a.kind)) + "] " + a.message);
Print("verify: " + std::to_string(conflict_anoms.size())
+ " source-conflict(s).");
}, true,
"check pin roles, bridged-net consistency, and model-driven pin specs (contention/undriven/NC)" };

View File

@@ -159,3 +159,23 @@ TEST_CASE("check_jtag_chain reports an incomplete TAP") {
auto a = check_jtag_chain(&sys);
CHECK(count_kind(a, AnomalyKind::JtagTapIncomplete) == 1);
}
TEST_CASE("check_source_conflicts flags a BSDL rail left unconnected") {
System sys;
Module *m = sys.modules()->merge("M");
Part *u = new Part("U1");
m->add(u);
// A BSDL power pin with no signal → conflict (a rail floated in the netlist).
Pin *vcc = new Pin("VCC");
vcc->spec.function = PinFunction::Power;
vcc->spec.source = SpecSource::Bsdl;
u->add(vcc);
// A BSDL ground pin that IS connected → no conflict.
Pin *gnd = mkpin(u, "GND", PinDirection::Power, PinFunction::Ground);
wire(m, "GNDNET", {gnd, mkpin(u, "X", PinDirection::Out, PinFunction::Signal)});
auto a = check_source_conflicts(&sys);
CHECK(count_kind(a, AnomalyKind::SourceConflict) == 1);
}

View File

@@ -68,3 +68,18 @@ TEST_CASE("apply_model does not overwrite a spec the model is silent about") {
CHECK(part.get("DATA")->spec.function == PinFunction::Signal);
CHECK(part.get("DATA")->spec.source == SpecSource::Bsdl);
}
TEST_CASE("apply_model never overwrites a higher-precedence source") {
Part part("U3");
Pin *p = new Pin("VCC");
p->spec.function = PinFunction::Ground; // user-set, deliberately != the model
p->spec.source = SpecSource::UserOverride;
part.add(p);
FakeModel m; // would set VCC = Power / Bsdl
apply_model(&part, m);
// UserOverride (rank 5) outranks Bsdl (rank 4): kept untouched.
CHECK(part.get("VCC")->spec.source == SpecSource::UserOverride);
CHECK(part.get("VCC")->spec.function == PinFunction::Ground);
}