Verify: check diff pairs/buses crossing connections (swap, incomplete)

New pass 8 (core/domain/diff_check.{hpp,cpp}): every complete local diff
pair (X_P/X_N, name-based) resolves its legs to two bridged nets; peer
pairs on those nets must match leg for leg.
- DiffPolaritySwap: P legs meet N legs across a connection (sometimes
  intentional - reported for review), or both legs joined onto one net.
- DiffCrossIncomplete: pairs sharing only one leg, and diff-bus lanes
  crossing NOWHERE while sibling lanes cross (distributed/fan-out buses
  stay silent - validated against the real 7-card VPX system: 21 noisy
  findings down to 3 genuine dangling-lane reports, 0 false swaps).

diff_suffix/split_trailing_index/is_internal_name promoted out of
analysis.cpp's anonymous namespace for reuse. VerifyReport.diff_anomalies
wired into model_total() and all four renderers (TUI verify, script
engine, wx log, analyze Issues). 8 new test cases (466 assertions).

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
This commit is contained in:
2026-06-04 20:05:43 +02:00
parent 9cf43696a2
commit 0b10e1c1b7
11 changed files with 452 additions and 26 deletions

View File

@@ -0,0 +1,194 @@
#include "diff_check.hpp"
#include "modules.hpp"
#include "signals.hpp"
#include "system.hpp"
#include <algorithm>
#include <map>
#include <set>
#include <string>
#include <unordered_map>
#include <utility>
namespace {
// One complete local diff pair with the net ids of its two legs.
struct LocalPair {
Module *mod = nullptr;
std::string stem;
Signal *p = nullptr, *n = nullptr;
int np = -1, nn = -1;
};
std::string pair_label(const LocalPair &lp) {
return lp.mod->name + "/" + lp.stem + "_P/N";
}
} // namespace
std::vector<Anomaly> check_diff_crossings(System *sys,
const std::vector<Net> *nets)
{
std::vector<Anomaly> out;
if (!sys || !nets) return out;
// Signal → net id (compute_all_nets covers every signal, singletons too).
std::unordered_map<Signal *, int> net_of;
for (size_t i = 0; i < nets->size(); ++i)
for (const auto &mp : (*nets)[i].members)
net_of[mp.second] = (int)i;
// Complete local pairs, module by module. Orphan halves (X_P without
// X_N) are analysis's DiffPairOrphan business — skipped here.
std::vector<LocalPair> pairs;
std::unordered_map<Signal *, int> pair_of; // leg signal → index in `pairs`
for (auto &mkv : *sys->modules()) {
Module *mod = mkv.second;
std::map<std::string, LocalPair> by_stem;
for (auto &skv : *mod->signals) {
if (is_internal_name(skv.first)) continue;
std::string stem; char pol;
if (!diff_suffix(skv.first, stem, pol)) continue;
LocalPair &lp = by_stem[stem];
lp.mod = mod; lp.stem = stem;
if (pol == 'P') lp.p = skv.second;
else lp.n = skv.second;
}
for (auto &kv : by_stem) {
LocalPair lp = kv.second;
if (!lp.p || !lp.n) continue;
auto ip = net_of.find(lp.p), in = net_of.find(lp.n);
if (ip == net_of.end() || in == net_of.end()) continue;
lp.np = ip->second;
lp.nn = in->second;
int idx = (int)pairs.size();
pairs.push_back(lp);
pair_of[lp.p] = idx;
pair_of[lp.n] = idx;
}
}
// Pass 1 — pair against pair. Each unordered couple of pairs is judged
// once (dedup set), so A↔B is never also reported as B↔A.
std::set<std::pair<int, int>> seen;
for (int i = 0; i < (int)pairs.size(); ++i) {
const LocalPair &a = pairs[i];
if (a.np == a.nn) {
// Degenerate: both legs land on one net — only the connections
// can do that (two module-local signals are distinct by nature).
Anomaly an;
an.kind = AnomalyKind::DiffPolaritySwap;
an.module = a.mod;
an.message = a.mod->name + ": " + a.stem + "_P and " + a.stem
+ "_N join the same net (through the connections)";
an.involved = {a.p, a.n};
out.push_back(std::move(an));
continue;
}
// Candidate peers: pairs of OTHER modules with a leg on net np or nn.
std::set<int> cands;
for (int net : {a.np, a.nn})
for (const auto &mp : (*nets)[net].members) {
auto it = pair_of.find(mp.second);
if (it == pair_of.end()) continue;
const LocalPair &b = pairs[it->second];
if (b.mod == a.mod) continue; // intra-module: nothing to say
if (b.np == b.nn) continue; // degenerate: own anomaly above
cands.insert(it->second);
}
for (int j : cands) {
std::pair<int, int> key = std::minmax(i, j);
if (!seen.insert(key).second) continue;
const LocalPair &b = pairs[j];
if (a.np == b.np && a.nn == b.nn) continue; // straight: all good
Anomaly an;
an.module = a.mod;
an.involved = {a.p, a.n, b.p, b.n};
if (a.np == b.nn && a.nn == b.np) {
an.kind = AnomalyKind::DiffPolaritySwap;
an.message = pair_label(a) + " <-> " + pair_label(b)
+ ": polarity swapped (P legs meet N legs)";
} else {
an.kind = AnomalyKind::DiffCrossIncomplete;
std::string how;
if (a.np == b.np) how = "only the P legs are bridged";
else if (a.nn == b.nn) how = "only the N legs are bridged";
else if (a.np == b.nn) how = "P leg bridged to N leg; "
"the other legs are not";
else how = "N leg bridged to P leg; "
"the other legs are not";
an.message = pair_label(a) + " <-> " + pair_label(b)
+ ": " + how;
}
out.push_back(std::move(an));
}
}
// Pass 2 — diff buses at a crossing. Lanes grouped by outer stem. A lane
// is "dangling" when it crosses to NO module at all while sibling lanes
// do cross — distributed buses (lanes fanned out to different peers, a
// backplane classic) are legitimate and stay silent. Lanes crossing
// partially are already reported above, so they don't count as dangling.
// One aggregated anomaly per bus, per side (each side names its lanes).
std::map<std::pair<Module *, std::string>, std::map<int, int>> groups;
for (int i = 0; i < (int)pairs.size(); ++i) {
std::string outer; int idx;
if (!split_trailing_index(pairs[i].stem, outer, idx)) continue;
groups[{pairs[i].mod, outer}][idx] = i;
}
for (auto &gkv : groups) {
auto &lanes = gkv.second; // lane index → pair index
if (lanes.size() < 2) continue;
std::set<int> touching_any; // lanes sharing ≥1 net with a peer
std::set<int> complete_any; // lanes fully crossing somewhere
std::set<Module *> reached;
for (auto &lkv : lanes) {
const LocalPair &a = pairs[lkv.second];
if (a.np == a.nn) continue;
for (int net : {a.np, a.nn})
for (const auto &mp : (*nets)[net].members) {
auto it = pair_of.find(mp.second);
if (it == pair_of.end()) continue;
const LocalPair &b = pairs[it->second];
if (b.mod == a.mod) continue;
touching_any.insert(lkv.first);
bool straight = (a.np == b.np && a.nn == b.nn);
bool swapped = (a.np == b.nn && a.nn == b.np);
if (straight || swapped) {
complete_any.insert(lkv.first);
reached.insert(b.mod);
}
}
}
if (complete_any.empty()) continue; // fully local bus: fine
std::vector<int> dangling;
for (auto &lkv : lanes)
if (!touching_any.count(lkv.first))
dangling.push_back(lkv.first);
if (dangling.empty()) continue;
int lo = lanes.begin()->first;
int hi = lanes.rbegin()->first;
Anomaly an;
an.kind = AnomalyKind::DiffCrossIncomplete;
an.module = gkv.first.first;
std::string m = gkv.first.first->name + ": " + gkv.first.second
+ "[" + std::to_string(lo) + ".."
+ std::to_string(hi) + "]_P/N: lane(s)";
for (int ix : dangling) m += " " + std::to_string(ix);
m += " do not cross (others reach";
std::vector<std::string> names;
for (Module *mod : reached) names.push_back(mod->name);
std::sort(names.begin(), names.end());
for (const std::string &nm : names) m += " " + nm;
m += ")";
an.message = std::move(m);
for (auto &lkv : lanes) {
an.involved.push_back(pairs[lkv.second].p);
an.involved.push_back(pairs[lkv.second].n);
}
out.push_back(std::move(an));
}
return out;
}