P3: BSDL completeness check (missing device power/ground pins)

check_bsdl_completeness(System*): for each BSDL-attached part, re-parse the
.bsd and report the device power/ground ports with no matching pin on the
netlist part (matched by port name or physical pad) — a rail the schematic
symbol is missing. One aggregated BsdlPinMissing per part; restricted to
power/ground so unused I/O balls don't create noise. Surfaced as a 7th verify
pass and in the analyze/dashboard model counts. 76 cases / 327 assertions
green; the real 8-card system reports 0 (all FPGA rails present). This closes
out P3.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

DESIGN.md

@@ -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` (seven 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); (7) **BSDL completeness** (`check_bsdl_completeness`): device power/ground ports (from the attached `.bsd`, re-parsed) with no matching pin on the netlist part — a rail the schematic symbol is missing (`BsdlPinMissing`, one aggregated finding per part). 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):
 
@@ -167,7 +167,7 @@ Exposed as the `analyze` shell command which prints groups (sorted by module + l
 
 **Analyze screen** (`screen_analyze.cpp`, dashboard shortcut `a`, `screen_idx = 7`): unified **verify + analyze** view with a tabbed layout — horizontal tab bar at the top (`Issues (…) │ Groups (…) │ Types: …`), and a single scrollable detail panel below showing the active tab's list. Tab swap is handled at the outer `CatchEvent` (`Tab` / `→` cycle forward, `Shift-Tab` / `←` cycle back). The detail uses `Container::Tab({issues_menu, groups_menu, types_menu}, &analyze_focus_idx)` so `↑/↓` always navigate the visible list; each tab preserves its own selection idx.
 
-- **Issues** pane merges: pin-role mismatches (typed pins whose actual signal type disagrees with the role from `connector_type`), bridged-net Power↔Gnd inconsistencies (the BFS check formerly in `verify` pass 2), and the structural anomalies from `analyze_system` (`DiffPairOrphan`, `BusGap`, `DiffBusGap`). Header counts each category.
+- **Issues** pane merges: pin-role mismatches (typed pins whose actual signal type disagrees with the role from `connector_type`), bridged-net Power↔Gnd inconsistencies (the BFS check formerly in `verify` pass 2), the structural anomalies from `analyze_system` (`DiffPairOrphan`, `BusGap`, `DiffBusGap`), and the model-driven checks (`check_pin_specs` / `check_jtag_chain` / `check_source_conflicts`, tagged `model` in the header). Header counts each category.
 - **Groups** pane lists every detected `SignalGroup` sorted by `module / label` with kind tag and member count.
 - **Types** pane lists per-signal Power decisions (`[Power confirmed]` / `[Power REFUTED]` / `[Gnd]`) plus a trailing `[NC]` orphan rollup line. The pane header summarises counts (`N pwr-ok, M refuted, K gnd`).
 
@@ -197,7 +197,7 @@ Today the only caller is `export` (`{"CSV", ".csv"}, {"ODS", ".ods"}` filters, k
 
 **Command palette** (`screen_palette.cpp`): a global modal launcher attached to the whole tab tree via `tab | Modal(BuildPaletteModal(), &palette_open)` in `Run()`. Trigger: `Event::CtrlP` (FTXUI Input does not consume Ctrl-P, so the outer `CatchEvent` reliably picks it up first). Behaviour: a single Input bound to `palette_query` plus a result list rebuilt on every frame. Indexes three kinds of entries: commands (from the `commands` map), modules and per-module signals (qualified as `module/signal`). Fuzzy match is subsequence-based, case-insensitive: lower score wins, computed as `first_match_position * 100 + sum_of_gaps`. Kinds are biased by a constant offset (commands +0, modules +1000, signals +2000) so command matches come first when scores tie. Output capped at 20 rows to keep render cheap on big systems. Activation (`Enter`): commands → `Dispatch(name)` (which dispatches like the shell, including opening interactive screens), module → prefill `explore_*` state and jump to `screen_idx = 4`, signal → prefill `net_modules` + seed `net_sig_filter` to the exact signal name and jump to `screen_idx = 5`. `Esc` closes the palette. While the palette is open, the outer `CatchEvent` cedes events to it so Tab/Esc/etc. don't leak into the underlying screen.
 
-**Dashboard** (`screen_dashboard.cpp`, `dashboard` command, `screen_idx = 4`): read-only system overview. Single Renderer, no Input child. Recomputes everything per frame (cheap on realistic sizes): counters (modules/parts/signals/connections), three health rows (verify pin-role mismatches, bridged-net inconsistencies, NC orphans — green check / yellow warning prefix), an analysis summary line (diff pairs / buses / anomaly count, coloured if non-zero), and a per-module table (parts / signals / `connector_type`-tagged parts). Letter shortcuts handled in the outer `CatchEvent`: `c`=console, `p`=plug (connect), `t`=set-connector-type, `e`=explore, `a`=analyze, `q`=quit. `Esc` is swallowed on the dashboard (home). The dashboard is `interactive = true`, `scriptable = false`; running `dashboard` inside `source` aborts the script.
+**Dashboard** (`screen_dashboard.cpp`, `dashboard` command, `screen_idx = 4`): read-only system overview. Single Renderer, no Input child. Recomputes everything per frame (cheap on realistic sizes): counters (modules/parts/signals/connections), four health rows (verify pin-role mismatches, bridged-net inconsistencies, NC orphans, and BSDL/JTAG model anomalies — green check / yellow warning prefix), an analysis summary line (diff pairs / buses / anomaly count, coloured if non-zero), and a per-module table (parts / signals / `connector_type`-tagged parts). Letter shortcuts handled in the outer `CatchEvent`: `c`=console, `p`=plug (connect), `t`=set-connector-type, `e`=explore, `a`=analyze, `q`=quit. `Esc` is swallowed on the dashboard (home). The dashboard is `interactive = true`, `scriptable = false`; running `dashboard` inside `source` aborts the script.
 
 **Screen titles** (shared idiom): every interactive screen renders a top bar in the form `" essim "` (bold) + `"→ "` (dim) + `"<screen-name>"` (bold) + `"  — <short description>"` (dim), followed by a `separator()`. The main screen has its own variant that adds a live `N module(s), M connection(s)` counter on the right. Aim is to make the breadcrumb between essim and the current mode visible at all times.
 
@@ -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`); `SourceConflict` (`check_source_conflicts` — a BSDL power/ground pin the netlist leaves unconnected); and `BsdlPinMissing` (`check_bsdl_completeness` — a device power/ground port absent from the netlist part, re-parsing the attached `.bsd`). They consume the BSDL-populated `PinSpec` plus `compute_all_nets`, and are surfaced in three places: the `verify` command, the analyze screen's Issues pane (counted as `… N model`), and a `model:` health row on the dashboard. `check_pin_specs`/`check_jtag_chain` accept an optional precomputed net list, so verify, analyze and the dashboard each compute the nets once and reuse them across checks.
 
 ### Component kind
 

src/system/analysis.cpp

@@ -29,6 +29,8 @@ 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";
+    case AnomalyKind::BsdlPinMissing:    return "bsdl-pin-missing";
     }
     return "?";
 }

src/system/analysis.hpp

@@ -37,6 +37,8 @@ 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).
+    BsdlPinMissing,    ///< A BSDL power/ground port has no pin on the netlist part.
 };
 
 struct Anomaly {

src/system/bsdl_check.cpp

@@ -1,5 +1,7 @@
 #include "bsdl_check.hpp"
 
+#include "bsdl_model.hpp"
+#include "connect.hpp"
 #include "modules.hpp"
 #include "nets.hpp"
 #include "parts.hpp"
@@ -10,6 +12,7 @@
 
 #include <string>
 #include <unordered_map>
+#include <unordered_set>
 #include <utility>
 #include <vector>
 
@@ -37,13 +40,16 @@ std::string join_labels(const std::vector<Pin *> &pins)
 
 }  // namespace
 
-std::vector<Anomaly> check_pin_specs(System *sys)
+std::vector<Anomaly> check_pin_specs(System *sys, const std::vector<Net> *nets)
 {
     std::vector<Anomaly> out;
     if (!sys)
         return out;
 
-    for (const Net &net : compute_all_nets(sys)) {
+    std::vector<Net> local;
+    if (!nets)
+        local = compute_all_nets(sys);
+    for (const Net &net : (nets ? *nets : local)) {
         std::vector<Pin *> pins;
         std::vector<Signal *> sigs;
         Module *mod = nullptr;
@@ -121,14 +127,17 @@ std::vector<Anomaly> check_pin_specs(System *sys)
     return out;
 }
 
-std::vector<Anomaly> check_jtag_chain(System *sys)
+std::vector<Anomaly> check_jtag_chain(System *sys, const std::vector<Net> *nets_in)
 {
     std::vector<Anomaly> out;
     if (!sys)
         return out;
 
     // Map every pin to the index of the net it sits on.
-    std::vector<Net> nets = compute_all_nets(sys);
+    std::vector<Net> local;
+    if (!nets_in)
+        local = compute_all_nets(sys);
+    const std::vector<Net> &nets = nets_in ? *nets_in : local;
     std::unordered_map<Pin *, int> net_of;
     for (size_t i = 0; i < nets.size(); ++i)
         for (auto &mp : nets[i].members)
@@ -277,3 +286,94 @@ 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;
+}
+
+std::vector<Anomaly> check_bsdl_completeness(System *sys)
+{
+    std::vector<Anomaly> out;
+    if (!sys)
+        return out;
+
+    for (auto &mkv : *sys->modules())
+        for (auto &pkv : *mkv.second) {
+            Part *part = pkv.second;
+            if (part->bsdl_path.empty())
+                continue;
+            BsdlModel model = BsdlModel::from_file(part->bsdl_path);
+            if (!model.valid())
+                continue;
+
+            std::vector<std::string> missing;  // absent power/ground ports
+            for (const auto &port : model.ports()) {
+                if (port.function != PinFunction::Power &&
+                    port.function != PinFunction::Ground)
+                    continue;  // only must-have rails — unused I/O may be absent
+                bool present = (!port.name.empty() && part->exists(port.name)) ||
+                               (!port.pad.empty() && part->exists(port.pad));
+                if (!present) {
+                    std::string lbl = port.name;
+                    if (!port.pad.empty())
+                        lbl += "@" + port.pad;
+                    missing.push_back(lbl);
+                }
+            }
+
+            if (!missing.empty()) {
+                std::string examples;
+                for (size_t i = 0; i < missing.size() && i < 5; ++i)
+                    examples += (examples.empty() ? "" : ", ") + missing[i];
+                if (missing.size() > 5)
+                    examples += ", …";
+
+                Anomaly a;
+                a.kind = AnomalyKind::BsdlPinMissing;
+                a.module = part->prnt;
+                a.message = mkv.first + "/" + part->name + ": "
+                          + std::to_string(missing.size())
+                          + " device power/ground pin(s) absent from the netlist ("
+                          + examples + ")";
+                out.push_back(std::move(a));
+            }
+        }
+
+    return out;
+}

src/system/bsdl_check.hpp

@@ -2,11 +2,16 @@
 #define _BSDL_CHECK_HPP_
 
 #include "analysis.hpp"  // Anomaly, AnomalyKind
+#include "nets.hpp"      // Net
 
 #include <vector>
 
 class System;
 
+// The net checks below accept an optional precomputed net list: callers that
+// already have one (verify, the analyze screen, the dashboard) pass it so the
+// transitive-closure pass isn't redone. Pass nullptr to compute it internally.
+
 // Model-driven pin checks over the system's nets, using the PinSpec
 // direction/function populated by connector or BSDL models. Emits:
 //   - DriveContention : a net with ≥2 push-pull output drivers;
@@ -14,7 +19,7 @@ class System;
 //   - NcWired         : a no-connect pin wired onto a multi-pin net.
 // Read-only; nets with no direction data are skipped (no false positives on
 // un-modelled parts).
-std::vector<Anomaly> check_pin_specs(System *sys);
+std::vector<Anomaly> check_pin_specs(System *sys, const std::vector<Net> *nets = nullptr);
 
 // JTAG boundary-scan chain integrity, using pins whose PinSpec.function is a TAP
 // role (JtagTdi/Tdo/Tms/Tck/Trst). Resolves each TAP pin to its net and checks:
@@ -23,6 +28,19 @@ std::vector<Anomaly> check_pin_specs(System *sys);
 //   - JtagChainBreak    : the TDO→TDI daisy chain dangles, fans out, or is not a
 //                         single path (≠1 head / ≠1 tail).
 // Empty when the system has no TAP pins.
-std::vector<Anomaly> check_jtag_chain(System *sys);
+std::vector<Anomaly> check_jtag_chain(System *sys, const std::vector<Net> *nets = nullptr);
+
+// 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);
+
+// Completeness: for every part with an attached BSDL, the device's power/ground
+// ports that have no matching pin on the netlist part (matched by port name or
+// physical pad) — i.e. a power/ground pin the schematic symbol is missing. One
+// aggregated anomaly per part. Re-parses each attached `.bsd` (no model cache on
+// Part yet), so it's bounded by the number of BSDL-attached parts.
+std::vector<Anomaly> check_bsdl_completeness(System *sys);
 
 #endif // _BSDL_CHECK_HPP_

src/system/pin_model.cpp

@@ -30,15 +30,18 @@ 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) {
+        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;
 }
 

src/system/pin_spec.hpp

@@ -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_

src/tui/commands.cpp

@@ -300,18 +300,32 @@ void Tui::RegisterCommands() {
 
         // Model-driven pin checks (drive contention / undriven net / NC-wired)
         // from the PinSpec direction/function populated by connector/BSDL models.
-        auto pin_anoms = check_pin_specs(sys.get());
+        auto pin_anoms = check_pin_specs(sys.get(), &nets);
         for (const auto &a : pin_anoms)
             Print("  [" + std::string(anomaly_kind_name(a.kind)) + "] " + a.message);
         Print("verify: " + std::to_string(pin_anoms.size())
               + " model-driven pin anomaly(ies).");
 
         // JTAG boundary-scan chain integrity (TAP pins → nets).
-        auto jtag_anoms = check_jtag_chain(sys.get());
+        auto jtag_anoms = check_jtag_chain(sys.get(), &nets);
         for (const auto &a : jtag_anoms)
             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).");
+
+        // BSDL completeness: device power/ground pins missing from the netlist.
+        auto missing_anoms = check_bsdl_completeness(sys.get());
+        for (const auto &a : missing_anoms)
+            Print("  [" + std::string(anomaly_kind_name(a.kind)) + "] " + a.message);
+        Print("verify: " + std::to_string(missing_anoms.size())
+              + " BSDL completeness issue(s).");
     }, true,
        "check pin roles, bridged-net consistency, and model-driven pin specs (contention/undriven/NC)" };
 

src/tui/screen_analyze.cpp

@@ -2,6 +2,7 @@
 #include "tui/tui_helpers.hpp"
 
 #include "system/analysis.hpp"
+#include "system/bsdl_check.hpp"
 #include "system/connect.hpp"
 #include "system/modules.hpp"
 #include "system/nets.hpp"
@@ -99,16 +100,35 @@ Component Tui::BuildAnalyzeScreen() {
                                      + anomaly_kind_name(a.kind) + "] "
                                      + a.message);
 
+        // Model-driven checks (same as `verify`), reusing the nets above.
+        std::vector<Anomaly> model_anoms;
+        {
+            auto a1 = check_pin_specs(sys.get(), &nets);
+            auto a2 = check_jtag_chain(sys.get(), &nets);
+            auto a3 = check_source_conflicts(sys.get());
+            auto a4 = check_bsdl_completeness(sys.get());
+            model_anoms.insert(model_anoms.end(), a1.begin(), a1.end());
+            model_anoms.insert(model_anoms.end(), a2.begin(), a2.end());
+            model_anoms.insert(model_anoms.end(), a3.begin(), a3.end());
+            model_anoms.insert(model_anoms.end(), a4.begin(), a4.end());
+        }
+        for (const auto &a : model_anoms)
+            analyze_issues.push_back(std::string("[")
+                                     + anomaly_kind_name(a.kind) + "] "
+                                     + a.message);
+        int n_model = (int)model_anoms.size();
+
         if (analyze_issues.empty()) analyze_issues.push_back("(no issue found)");
         if (analyze_issue_idx >= (int)analyze_issues.size())
             analyze_issue_idx = (int)analyze_issues.size() - 1;
 
         std::string issues_header = "Issues ("
             + std::to_string(n_role_mismatches + n_inconsistent
-                             + (int)rep.anomalies.size())
+                             + (int)rep.anomalies.size() + n_model)
             + ": " + std::to_string(n_role_mismatches) + " pin-role, "
             + std::to_string(n_inconsistent) + " net-mix, "
-            + std::to_string(rep.anomalies.size()) + " struct.)";
+            + std::to_string(rep.anomalies.size()) + " struct, "
+            + std::to_string(n_model) + " model)";
 
         // ============================================================ Groups
         analyze_groups.clear();

src/tui/screen_dashboard.cpp

@@ -2,6 +2,7 @@
 #include "tui/tui_helpers.hpp"
 
 #include "system/analysis.hpp"
+#include "system/bsdl_check.hpp"
 #include "system/connect.hpp"
 #include "system/modules.hpp"
 #include "system/nets.hpp"
@@ -149,6 +150,15 @@ Component Tui::BuildDashboardScreen() {
           + std::to_string(orph_imported) + " imported, "
           + std::to_string(orph_dropped) + " dropped)"));
 
+      // Model-driven checks (BSDL pin specs, JTAG chain, source conflicts),
+      // reusing the nets computed above.
+      int n_model = (int)(check_pin_specs(sys.get(), &nets).size()
+                          + check_jtag_chain(sys.get(), &nets).size()
+                          + check_source_conflicts(sys.get()).size()
+                          + check_bsdl_completeness(sys.get()).size());
+      health_rows.push_back(health_line(n_model == 0,
+          "model:   " + std::to_string(n_model) + " BSDL/JTAG anomaly(ies)"));
+
       // ---- analysis summary ----
       AnalysisReport rep = analyze_system(sys.get());
       int n_diff = 0, n_diff_bus = 0, n_bus = 0;

tests/test_bsdl_apply.cpp

@@ -1,5 +1,7 @@
 #include <doctest/doctest.h>
 
+#include "system/analysis.hpp"
+#include "system/bsdl_check.hpp"
 #include "system/bsdl_model.hpp"
 #include "system/parts.hpp"
 #include "system/pins.hpp"
@@ -141,3 +143,27 @@ TEST_CASE("attached BSDL path persists and re-applies on restore") {
     std::remove(bsd);
     std::remove(snap);
 }
+
+TEST_CASE("check_bsdl_completeness flags a device power pin absent from the part") {
+    const char *bsd = "test_complete_demo.bsd";
+    { std::ofstream o(bsd); o << DEMO_BSDL; }
+
+    System sys;
+    Module *m = sys.modules()->merge("CARD");
+    Part *u = new Part("U1");
+    // All pins EXCEPT VDD (a power port at ball C1) → its port is unmatched.
+    for (const char *n : {"TCK", "TDI", "TDO", "TMS", "IO1", "GND"})
+        u->add(new Pin(n));
+    u->bsdl_path = bsd;
+    m->add(u);
+
+    auto a = check_bsdl_completeness(&sys);
+    REQUIRE(a.size() == 1);
+    CHECK(a[0].kind == AnomalyKind::BsdlPinMissing);
+
+    // With VDD present (by ball or by name), no completeness issue.
+    u->add(new Pin("VDD"));
+    CHECK(check_bsdl_completeness(&sys).empty());
+
+    std::remove(bsd);
+}

tests/test_bsdl_check.cpp

@@ -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);
+}

tests/test_pin_model.cpp

@@ -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);
+}