Designers should verify that the lock functionality implements the expected behavior and that no unexpected information flows occur when the debug access port is in locked mode. When in locked mode the debugger should not be able to access 1) processor registers, or 2) processor data memory.
Radix-S can verify that a specific ARC configuration satisfies this assumption when in locked mode by creating two security rules to track the flow of the processor registers and data memory to the debug port. These rules are written using Tortuga Logic’s Sentinel language. A unique feature of Sentinel is the ability to express security requirements related to information flows in the design, which is essential for efficiently expressing and verifying confidentiality and integrity properties for design assets. The “no-flow” operator (=/=>) is the basic building block used to create rules for tracking information flows between design signals. The Sentinel keywords “when” and “unless” exist to specify conditions which must be met before flow tracking is performed, and conditions under which flows between signals are allowed, respectively.
Security Rule #1: CPU register contents should never flow to the debug interface when the debug access port is in locked mode.
u_regfile_2r2w.$all_outputs when (!dbg_unlock) =/=> dbg.$all_outputs
u_regfile_2r2w is the module that implements the ARC EM register file. dbg_unlock is the unlock signal from Figure 1, and dbg is the debug module itself. The “$all_outputs” keyword is shorthand for describing the set of all output signals for a particular module instance in the design hierarchy. Rule #1 will fail if register file contents flow to debug module outputs when debug is in locked mode.
Security Rule #2: Data memory should never flow to the debug interface when the debug access port is in locked mode.
dccm_data_out when (!dbg_unlock) =/=> dbg.$all_outputs
Rule #2 will fail if data memory contents (dccm_data_out) can exit the debug access port while debug is in locked mode. Note that ARC processors feature single-cycle access data closely coupled memories (DCCM for data and ICCM for instructions). Radix-S can verify both Rule #1 and #2 as part of the existing test flow in an ARC-based system to provide assurance that the debug port does not leak internal processor information when in locked mode. Designers can write additional Radix-S Sentinel rules to verify the custom unlock module itself.