Fully Verified Open Silicon

Marno van der Maas - lowRISC

Open Silicon = Hard

Apache License 2.0

Learn from Open Software

Open Source

Coverage

Test coverage is a well-known concept in software, for example code coverage. Test pass rate and functional coverage also increase confidence in this area.

We can also learn from formal verification as applied in for example functional programming languages. Formal analysis can prove mathematical properties in code, which is a great tool alongside the standard coverage-based testing.

We can use these concepts in silicon as well, on top of which we add things like:

Finite state machine coverage
Toggle coverage

Governance

OpenTitan does it right

High speed domain

DUAL LOCKSTEP Ibex Core (RV32IMCB) Interrupt Controller ROM Debug Module Main
SRAM TL-UL
Crossbar Key Manager KMAC EDN SPI
Host 0 OTBN HMAC CSRNG SPI
Host 1 AES Flash Entropy Source USB

Peripheral domain

TL-UL Crossbar OTP (Fuse) Controller Life
Cycle Alert Handler 4 x UART Timers GPIO 3 x I²C SPI
Device Pattern Generators

Always-on domain

PWM Retention SRAM Power Manager Sysrst Controller AON
Timers Clk/Rst Managers Pinmux / Padctrl ADC Controller Sensor Control

Padring (only wire and pad instances) Analog Sensor Top

~100 MHz

96 MHz

48 MHz

24 HMz

200 kHz

Logic Only

	Design	Verification
Specified	D0	V0
Developed	D1	V1
Functional	D2	V2
Secure	D2S	V2S
Complete	D3	V3

Verification in OpenTitan

High speed domain

DUAL LOCKSTEP Ibex Core (RV32IMCB) Interrupt Controller ROM Debug Module Main
SRAM TL-UL
Crossbar Key Manager KMAC EDN SPI
Host 0 OTBN HMAC CSRNG SPI
Host 1 AES Flash Entropy Source USB

Peripheral domain

TL-UL Crossbar OTP (Fuse) Controller Life
Cycle Alert Handler 4 x UART Timers GPIO 3 x I²C SPI
Device Pattern Generators

Always-on domain

PWM Retention SRAM Power Manager Sysrst Controller AON
Timers Clk/Rst Managers Pinmux / Padctrl ADC Controller Sensor Control

Padring (only wire and pad instances) Analog Sensor Top

~100 MHz

96 MHz

48 MHz

24 HMz

200 kHz

Logic Only

DUAL LOCKSTEP Ibex Core (RV32IMCB)

/lowRISC/ibex

Enhanced Physical Memory Protection

Machine Mode Lockdown
Machine Mode Whitelist Policy
Rule Lock Bypass

ePMP stands for enhances physical memory protection. A number of entries, 16 in Ibex. Each entry has address, permissions and region size. The table shows the different types of regions that exist. What does ePMP add on top of PMP?

MML: machine mode lockdown
MMWP: machine mode whitelist policy
RLB: rule lock bypass

Some things to consider when testing ePMP:

Keep the trap handler and test code executable.
Permissions between M and S/U mode differ. For example, when MML is enabled and lock bit is 0, S/U have access while M mode does not.
Switching on MML may remove executable rights of the code you are currently running.
Getting stuck in faulting loops is expected and should not fail the test.
Timing out occurs more often and should not fail the test
Hitting small regions (e.g. 4 Byte) is unlikely without constraining addresses.


                            typedef enum logic [4:0] {
                                NONE        = 5'b00000, L           = 5'b01000,
                                R           = 5'b00001, LR          = 5'b01001,
                                W           = 5'b00010, LW          = 5'b01010,
                                WR          = 5'b00011, LWR         = 5'b01011,
                                X           = 5'b00100, LX          = 5'b01100,
                                XR          = 5'b00101, LXR         = 5'b01101,
                                XW          = 5'b00110, LXW         = 5'b01110,
                                XWR         = 5'b00111, LXWR        = 5'b01111,
                                MML_NONE    = 5'b10000, MML_L       = 5'b11000,
                                MML_RU      = 5'b10001, MML_RM      = 5'b11001,
                                MML_WRM_RU  = 5'b10010, MML_XM_XU   = 5'b11010,
                                MML_WRU     = 5'b10011, MML_WRM     = 5'b11011,
                                MML_XU      = 5'b10100, MML_XM      = 5'b11100,
                                MML_XRU     = 5'b10101, MML_XRM     = 5'b11101,
                                MML_WRM_WRU = 5'b10110, MML_XRM_XU  = 5'b11110,
                                MML_XWRU    = 5'b10111, MML_RM_RU   = 5'b11111
                            } pmp_priv_bits_e;

We took a number of steps to improve the functional coverage with our PMP tests.

Before->Static: Add some directed tests that add static ePMP configs with mseccfg modes. Before we never had MML, MMWP or RLB enabled.
Static->Random: Enable a test that randomly configured mseccfg as well as randomly configure all the ePMP entries. This configuration need to keep trap handler and code executable, and skipping faulting loads/stores. Before this we were not hitting many of the LRWX combinations possible for each PMP entry.
Random->Directed: On top of the random tests, we add some directed tests to improve coverage. For example, toggling execute permission in MML mode is rare to happen in the random test and attempting to execute instructions from regions with all the different LRWX permutations was also not hit reliably with the full random tests.

Primitive blocks

Alerts
Asserts
Clocks
FIFOs
Multi-bit encodings
RAM/ROM
Etc.


                        module prim_cdc_rand_delay (
                            input  logic                 clk_i,
                            input  logic                 rst_ni,
                            input  logic [DataWidth-1:0] prev_data_i,
                            input  logic [DataWidth-1:0] src_data_i,
                            output logic [DataWidth-1:0] dst_data_o
                        );
                            bit [DataWidth-1:0] data_sel;

                            // Set data_sel at random combinationally when the input changes.
                            always @(src_data_i) begin
                                data_sel = $urandom();
                            end

                            // Clear data_del on any cycle start.
                            always @(posedge clk_i or negedge rst_ni) begin
                                data_sel <= 0;
                            end

                            always_comb dst_data_o = (prev_data_i & data_sel) |
                                                     (src_data_i & ~data_sel);
                        endmodule

One reason to have this standard library of cells is that it can help with verification. For example, our primitive blocks automatically allow testbenches to introduce random clock domain crossing delays where appropriate. This is an example of chip-level verification in simulation. We do this in the prim_cdc_rand_delay module that effectively randomly delays any bit of the input to contain the previous value until the next clock or reset edge. These are changes that can happen in the real chip due to clock domain crossing and usually is quite difficult to replicate in simulation. Thus these tests are usually done using field programmable gate arrays or through simulations of the synthesized chips (gate-level simulation). With these primitives, we can do a part of that in higher-level simulations as well.

Frozen

[email protected]