The DMA copy that fails on its first beat, the non-secure master reaching a secure slave, the stream bridge that cannot see the memory it was told to fill: all three are connectivity facts, knowable without a single simulation cycle. On NanoSoC the stream bridge resets as a non-secure master (its CTRL.NS bit is 1) while SRAM1 is secure-only, so a DMA job that copies into SRAM1 is a failed transfer the day the software is written. A reachability table that carries the secure attribute says so in milliseconds. The table is the subject of this lesson: what each row states, and the reachability proof it must support.
Each table row names the source instance and port, the destination instance and port, the net, the width, and the intent: which master-slave paths it serves, which protection sideband travels with it, and which clock and reset domains it crosses. The NanoSoC rows that earn their keep are the awkward ones: the sliced apb_paddr with its four dropped bits, the stream link that carries only TDATA, TVALID, TREADY and TLAST with a row recording that no sideband exists on either end, the two interrupts through isolation into the always-on controller, the tied-off reserved interrupt inputs 6 and 7, and the AxPROT sideband from each master to both filters. Ordinary data wiring needs no commentary; these rows carry the integration decisions.
Reachability is the proof the table owes, and it has two halves: a path must exist, and the master's security attribute must be allowed on it. On NanoSoC the CPU reaches ROM, both SRAMs and the APB bridge. The stream bridge (M1) reaches both SRAMs for data and ROM only if boot needs it; it has no reason to reach the APB bridge, because its registers are programmed by the CPU. SRAM1 is secure-only, and the stream bridge's CTRL.NS bit resets to 1 (non-secure), so by default its path to SRAM1 is refused with SLVERR. The checker below carries that attribute in the table, plants the failure, and shows the proof reports it by name. It also deletes a path to prove a missing wire is caught.
# NanoSoC teaching values: per-master reachability with the secure attribute.
PATHS = { # (master, slave): who may use the path
("cpu", "rom"): "open", ("cpu", "sram0"): "open",
("cpu", "sram1"): "secure-only", ("cpu", "apb"): "open",
("sbr", "rom"): "open", ("sbr", "sram0"): "open",
("sbr", "sram1"): "secure-only", # no sbr -> apb row: not needed
}
REQUIRED = {"cpu": ["rom", "sram0", "sram1", "apb"],
"sbr": ["sram0", "sram1"]}
NOT_WANTED = [("sbr", "apb")] # the CPU programs the SBR registers
def prove(paths, master_ns):
"""Return the list of problems; master_ns: 1 = non-secure attribute."""
problems = []
for master, slaves in REQUIRED.items():
for slave in slaves:
rule = paths.get((master, slave))
if rule is None:
problems.append(f"no path: {master}->{slave}")
elif rule == "secure-only" and master_ns[master] == 1:
problems.append(f"blocked: NS master, secure-only slave: {master}->{slave}")
problems += [f"unwanted path: {m}->{s}" for m, s in NOT_WANTED if (m, s) in paths]
return problems
assert prove(PATHS, {"cpu": 0, "sbr": 0}) == [] # secure job: clean
# reset state of the stream bridge: CTRL.NS = 1 (non-secure)
assert prove(PATHS, {"cpu": 0, "sbr": 1}) == [
"blocked: NS master, secure-only slave: sbr->sram1"]
# a deleted path is caught as well
broken = {k: v for k, v in PATHS.items() if k != ("sbr", "sram0")}
assert prove(broken, {"cpu": 0, "sbr": 0}) == ["no path: sbr->sram0"]
# a path nobody asked for is caught
extra = dict(PATHS); extra[("sbr", "apb")] = "open"
assert prove(extra, {"cpu": 0, "sbr": 0}) == ["unwanted path: sbr->apb"]
print("PASS: secure job clean; reset-state SBR to SRAM1 reported; missing and unwanted paths caught")The proof says the path and the attribute agree for a given NS value. It does not say who may change NS. NanoSoC v1 has a known weakness here: the SBR register slot is non-secure, so non-secure software can write CTRL.NS = 0 and make the stream bridge issue secure accesses into SRAM1. Until the NS field is writable only from the secure side (or the SBR slot becomes secure-only), the SRAM1 partition is not closed, and a green reachability table must not be read as saying it is.
The table current against the RTL, diffed mechanically on every build, with the awkward rows above present and commented.
The reachability proof passing for every master, with the secure attribute per path encoded in the table and the reset value of every master's attribute used, not just the wires.
No row whose intent column is blank: a connection nobody can justify is a connection waiting to be cut or fixed.
When an integrated test fails with an access error, look up the path in the table before opening a waveform: the usual finding is a path that was never a row, a bridge added late whose sideband nobody carried. Regenerate the table diff after every redelivery; a new block version that renames one port orphans its rows, and orphaned rows are how silent ties are born.
The wire proof passes and the protection proof qualifies it: SRAM1 is reachable and filtered, so non-secure accesses return SLVERR by design, and the proof reports the stream bridge at its reset value as blocked. Reachability without the protection story is how security holes ship.