These are the worked solutions. Compare the inputs and injected faults with your written hypothesis before running each block. Each block runs independently and prints one PASS line after its clean-data and failing-data assertions.
The boot checker stores fourteen timed entries. The full boot ledger has sixteen steps because it also lists the zero-duration POR starting point and final jump; those endpoints do not add time to the model. The total remains 12.581 ms.
MAP = [
("BOOTROM", 0x00000000, 0x4000),
("SRAM0", 0x20000000, 0x10000),
("SRAM1", 0x20010000, 0x10000),
("DMA", 0x40000000, 0x1000),
("SBR", 0x40001000, 0x1000),
("UART", 0x40002000, 0x1000),
("SPI", 0x40003000, 0x1000),
("GPIO", 0x40004000, 0x1000),
("INTC", 0x40005000, 0x1000),
("RSTPWR", 0x40006000, 0x1000),
]
SECURE_ONLY = {"SRAM1", "RSTPWR"}
SLOTS = ["DMA", "SBR", "UART", "SPI", "GPIO", "INTC", "RSTPWR"]
T_CPU, T_SYS, T_PER = 1e9 / 192e6, 1e9 / 96e6, 1e9 / 24e6
def end_of(base, size):
return base + size - 1
def overlaps(entries=MAP):
bad = []
xs = sorted(entries, key=lambda e: e[1])
for a, b in zip(xs, xs[1:]):
if b[1] < a[1] + a[2]:
bad.append((a[0], b[0]))
return bad
def misaligned(entries=MAP):
return [n for n, b, s in entries if b % s != 0]
def decode(addr, slots=SLOTS):
if addr >> 14 == 0:
return "BOOTROM"
if addr >> 16 == 0x2000:
return "SRAM0"
if addr >> 16 == 0x2001:
return "SRAM1"
if addr >> 16 == 0x4000:
slot = (addr >> 12) & 0xF
return slots[slot] if slot < 7 else "H3"
if addr < 0x20000000:
return "H1"
if addr < 0x40000000:
return "H2"
return "H4"
def response(addr, secure, slots=SLOTS):
t = decode(addr, slots)
if t in ("H1", "H2", "H4"):
return "DECERR"
if t == "H3":
return "SLVERR"
if t in SECURE_ONLY and not secure:
return "SLVERR"
return "OK"
def sustained(peak, beats):
return peak * beats / (beats + 1)
# ---- this lesson starts here ----
def latency(sync_per, ctrl, sync_cpu):
best = sync_per * T_PER + ctrl * T_PER + sync_cpu * T_CPU # two syncs, the INTC register, two syncs
return best, best + T_PER + T_CPU # worst adds one clk_per and one clk_cpu of alignment
best, worst = latency(2, 1, 2)
assert abs(best - 135.4) < 0.1 and abs(worst - 182.3) < 0.1
assert abs(latency(1, 1, 2)[0] - 135.4) > 0.1 # a missing flop moves the bound
ORACLE = {"irq_pwr": 0, "irq_dma": 1, "irq_sbr": 2, "irq_uart": 3, "irq_spi": 4, "irq_gpio": 5}
def intc_raw(wiring, active):
return sum(1 << wiring[s] for s in active) # RAW bit i is set when the line wired to input i is high
def conn_test(w):
return [s for s in ORACLE if intc_raw(w, [s]) != 1 << ORACLE[s]] # force one source at a time
wiring = dict(ORACLE)
assert conn_test(wiring) == []
assert intc_raw(wiring, ["irq_dma"]) == 0x02 and intc_raw(wiring, list(ORACLE)) == 0x3F # spares 6 and 7 stay 0
bad = dict(wiring, irq_dma=6) # bug 3
assert conn_test(bad) == ["irq_dma"] and intc_raw(bad, ["irq_dma"]) == 0x40 # RAW bit 6, not bit 1
swap = dict(wiring, irq_dma=2, irq_sbr=1)
assert conn_test(swap) == ["irq_dma", "irq_sbr"]
print("PASS: map wired 0-5, spares tied; IRQ latency 135.4 best, 182.3 worst ns")MAP = [
("BOOTROM", 0x00000000, 0x4000),
("SRAM0", 0x20000000, 0x10000),
("SRAM1", 0x20010000, 0x10000),
("DMA", 0x40000000, 0x1000),
("SBR", 0x40001000, 0x1000),
("UART", 0x40002000, 0x1000),
("SPI", 0x40003000, 0x1000),
("GPIO", 0x40004000, 0x1000),
("INTC", 0x40005000, 0x1000),
("RSTPWR", 0x40006000, 0x1000),
]
SECURE_ONLY = {"SRAM1", "RSTPWR"}
SLOTS = ["DMA", "SBR", "UART", "SPI", "GPIO", "INTC", "RSTPWR"]
T_CPU, T_SYS, T_PER = 1e9 / 192e6, 1e9 / 96e6, 1e9 / 24e6
def end_of(base, size):
return base + size - 1
def overlaps(entries=MAP):
bad = []
xs = sorted(entries, key=lambda e: e[1])
for a, b in zip(xs, xs[1:]):
if b[1] < a[1] + a[2]:
bad.append((a[0], b[0]))
return bad
def misaligned(entries=MAP):
return [n for n, b, s in entries if b % s != 0]
def decode(addr, slots=SLOTS):
if addr >> 14 == 0:
return "BOOTROM"
if addr >> 16 == 0x2000:
return "SRAM0"
if addr >> 16 == 0x2001:
return "SRAM1"
if addr >> 16 == 0x4000:
slot = (addr >> 12) & 0xF
return slots[slot] if slot < 7 else "H3"
if addr < 0x20000000:
return "H1"
if addr < 0x40000000:
return "H2"
return "H4"
def response(addr, secure, slots=SLOTS):
t = decode(addr, slots)
if t in ("H1", "H2", "H4"):
return "DECERR"
if t == "H3":
return "SLVERR"
if t in SECURE_ONLY and not secure:
return "SLVERR"
return "OK"
def sustained(peak, beats):
return peak * beats / (beats + 1)
# ---- this lesson starts here ----
class Dma: # the register behaviour of the DMA, one rule per line
def __init__(self):
self.busy = self.done = self.err = self.irq_en = False
self.key = self.len = self.count = self.stalls = 0
def irq(self):
return self.irq_en and (self.done or self.err) # a level, held until software clears it
def write_key(self, v):
self.key = self.key if self.busy else v # ignored while BUSY, no PSLVERR
def write_len(self, v):
self.len = self.len if self.busy else v & 0xFFFF # ignored while BUSY
def ctrl_write(self, v):
self.irq_en = bool(v & 2) # every CTRL write copies bit 1 into IRQ_EN
if v & 1 and not self.busy: # GO while BUSY is ignored
if self.len == 0:
self.done = True
else:
self.busy, self.done, self.count = True, False, 0 # GO clears DONE but not ERR
def status_write(self, v):
self.done = self.done and not v & 2 # W1C
self.err = self.err and not v & 4
def accept(self, last): # one stream word offered
if not self.busy:
self.stalls += 1 # s_tready is low when not BUSY
return False
self.count += 1
if last and self.count < self.len:
self.err, self.busy = True, False # early tlast: ERR, never DONE
elif self.count == self.len:
self.done, self.busy = True, False
return True
def stream(dma, n): # the SBR read engine; True means it is stuck BUSY
return not all(dma.accept(i == n - 1) for i in range(n))
def job(n_dma, n_sbr, key=0x5A):
d = Dma()
d.write_key(key)
d.write_len(n_dma)
d.ctrl_write(0x3) # DMA first
return d, stream(d, n_sbr) # SBR START last
def driver_ok(count, sbr_len, dma_len):
return count == sbr_len == dma_len and dma_len > 0
ok, stuck = job(64, 64)
assert ok.done and not ok.err and not stuck and ok.stalls == 0 and driver_ok(ok.count, 64, 64)
a, a_stuck = job(64, 32) # case A: SBR LEN 32, DMA LEN 64
assert a.err and not a.done and a.count == 32 and not a_stuck and not driver_ok(a.count, 32, 64)
b, b_stuck = job(32, 64) # case B: SBR LEN 64, DMA LEN 32
assert b.done and not b.err and b.count == 32 and b_stuck and not driver_ok(b.count, 64, 32)
early = Dma()
assert early.accept(False) is False and early.stalls == 1 # a word offered before GO is refused
class Good:
def start(self, d): d.ctrl_write(0x3)
def rekey(self, d, key, finish):
if d.busy:
finish(d) # wait for BUSY = 0 first
d.write_key(key)
def clear(self, d): d.status_write(0x6) # DONE and ERR together
class Naive:
def start(self, d): d.ctrl_write(0x1)
def rekey(self, d, key, finish): d.write_key(key)
def clear(self, d): d.status_write(0x2)
def contract_problems(drv):
found = []
a = Dma(); a.write_key(0xAA); a.write_len(4); a.ctrl_write(0x3); a.accept(False) # a job is in flight
drv.rekey(a, 0x55, lambda x: [x.accept(i == 2) for i in range(3)])
if a.key != 0x55:
found.append("stale_key")
b = Dma(); b.write_len(8); b.ctrl_write(0x3); b.accept(True) # a failed job leaves ERR set
drv.clear(b)
if b.irq():
found.append("irq_stuck")
c = Dma(); c.write_len(1); drv.start(c)
if not c.irq_en:
found.append("irq_disabled")
return found
assert contract_problems(Good()) == []
assert contract_problems(Naive()) == ["stale_key", "irq_stuck", "irq_disabled"]
print("PASS: length mismatch named both ways; careful driver clean, naive driver trips all 3 traps")MAP = [
("BOOTROM", 0x00000000, 0x4000),
("SRAM0", 0x20000000, 0x10000),
("SRAM1", 0x20010000, 0x10000),
("DMA", 0x40000000, 0x1000),
("SBR", 0x40001000, 0x1000),
("UART", 0x40002000, 0x1000),
("SPI", 0x40003000, 0x1000),
("GPIO", 0x40004000, 0x1000),
("INTC", 0x40005000, 0x1000),
("RSTPWR", 0x40006000, 0x1000),
]
SECURE_ONLY = {"SRAM1", "RSTPWR"}
SLOTS = ["DMA", "SBR", "UART", "SPI", "GPIO", "INTC", "RSTPWR"]
T_CPU, T_SYS, T_PER = 1e9 / 192e6, 1e9 / 96e6, 1e9 / 24e6
def end_of(base, size):
return base + size - 1
def overlaps(entries=MAP):
bad = []
xs = sorted(entries, key=lambda e: e[1])
for a, b in zip(xs, xs[1:]):
if b[1] < a[1] + a[2]:
bad.append((a[0], b[0]))
return bad
def misaligned(entries=MAP):
return [n for n, b, s in entries if b % s != 0]
def decode(addr, slots=SLOTS):
if addr >> 14 == 0:
return "BOOTROM"
if addr >> 16 == 0x2000:
return "SRAM0"
if addr >> 16 == 0x2001:
return "SRAM1"
if addr >> 16 == 0x4000:
slot = (addr >> 12) & 0xF
return slots[slot] if slot < 7 else "H3"
if addr < 0x20000000:
return "H1"
if addr < 0x40000000:
return "H2"
return "H4"
def response(addr, secure, slots=SLOTS):
t = decode(addr, slots)
if t in ("H1", "H2", "H4"):
return "DECERR"
if t == "H3":
return "SLVERR"
if t in SECURE_ONLY and not secure:
return "SLVERR"
return "OK"
def sustained(peak, beats):
return peak * beats / (beats + 1)
# ---- this lesson starts here ----
banner = "NanoSoC boot ok\n"
assert len(banner) == 16
baud = 24e6 / (16 * 13)
assert abs(baud - 115384.6) < 0.1 and abs(160 / baud * 1e6 - 1386.667) < 0.01
def boot_steps(cause, cause_first=True):
hw = [("osc", 1024 * T_PER), ("rst_per", 2 * T_PER), ("pll", 260 * T_PER), ("gates", 2 * T_PER),
("rst_sys", 18 * T_SYS), ("rst_cpu", 8 * T_SYS + 2 * T_CPU), ("fetch", 24 * T_CPU)]
rd, clr = ("read_cause", 54 * T_CPU), ("clear_sram0", 1024 * T_SYS)
if cause == "WAKE":
return hw + ([rd] if cause_first else [clr, rd]) # the clear before the read erases the retained image
rest = [("uart_init", 3 * 54 * T_CPU), ("banner", 160 / baud * 1e9),
("dma_selftest", 5 * 125 + 7 * 125 + 72 * T_SYS + 26 * T_CPU + 6000),
("spi_load", (8192 + 4) * 8 / 6e6 * 1e9), ("checksum", 2048 * 18 * T_CPU)]
return hw + ([rd, clr] if cause_first else [clr, rd]) + rest
def names(steps):
return [n for n, _ in steps]
cold = boot_steps("POR")
assert len(cold) == 14 and abs(sum(ns for _, ns in cold) / 1000 - 12580.917) < 0.01
assert names(cold).index("read_cause") < names(cold).index("clear_sram0")
assert "clear_sram0" not in names(boot_steps("WAKE")) # the retained image survives
assert "clear_sram0" in names(boot_steps("WAKE", cause_first=False)) # the wrong order would erase it
SBR_CTRL_RESET = 0x4 # CTRL.NS (bit 2) resets to 1
def sbr_ctrl_write(ctrl, wdata, writer_secure, ns_secure_only=False):
if ns_secure_only and not writer_secure:
wdata = (wdata & ~0x4) | (ctrl & 0x4) # the proposed fix: NS writable only from the secure side
return wdata & 0x6 # START self-clears
def sbr_reaches_sram1(ctrl):
return response(0x20010000, (ctrl >> 2) & 1 == 0) == "OK" # AxPROT[1] = NS: the access is secure when NS is 0
assert response(0x20010000, True) == "OK" and response(0x20000000, False) == "OK" and response(0x20010000, False) == "SLVERR"
assert not sbr_reaches_sram1(SBR_CTRL_RESET) # bug 7: the SBR is non-secure out of reset
assert sbr_reaches_sram1(sbr_ctrl_write(SBR_CTRL_RESET, 0x0, True)) # secure software clears NS: it works
assert sbr_reaches_sram1(sbr_ctrl_write(SBR_CTRL_RESET, 0x0, False)) # known weakness: non-secure software can too
assert not sbr_reaches_sram1(sbr_ctrl_write(SBR_CTRL_RESET, 0x0, False, ns_secure_only=True)) # closed by the fix
assert sbr_reaches_sram1(sbr_ctrl_write(SBR_CTRL_RESET, 0x0, True, ns_secure_only=True)) # secure copy still works
print("PASS: boot 12.581 ms over 14 steps, banner 16 chars; SBR blocked at reset, opened by NS = 0, hole shown and closed")The final PASS establishes consistency of the Python model and manifest. Record the known SBR attribute weakness and all implementation evidence still required in the readiness statement. The model reproduces an open partition in v1 and demonstrates a proposed secure-write guard; a model PASS alone does not close that finding.