Formal ISA Verification for Custom-designed Processors

We live in a world where the shift towards software-defined everything demands key components of a System-on-Chip (SoC) to be highly programmable, driving unprecedented flexibility and adaptability in response to rapidly evolving requirements, while still achieving stringent power and area efficiency targets. To meet these pressing challenges, many embedded designs incorporate custom-designed processors that are fully programmable yet carefully tailored to the specific workloads of their target applications. This approach allows designers to balance programmability with optimized resource usage, empowering them to tackle the growing complexity of modern systems.

ASIP Designer™ accelerates the process for engineers in designing such custom Application-Specific Instruction-Set Processors (ASIPs). By modeling their processor architecture in the high-level nML language, ASIP Designer automatically generates synthesizable RTL as well as a comprehensive software development kit (SDK), including a compiler, simulator, and profiler. This integrated tool suite enables rapid architectural exploration, helping designers identify the best performing processor for their application.

As you approach tape out, thorough verification of your custom processor becomes critical. Common processor verification strategies combine simulation-based and formal-based approaches. While simulation-based approaches can be used at the processor level, using regression suites and constrained random program verification, formal verification is often limited to the module level. For example, Data Path Validation (DPV) is used for verifying data path functions such as the ALU.

In this blog post, we explore how ASIP Designer enables you to extend the power of formal verification beyond the module level, using it for Instruction Set Architecture (ISA) verification. This advanced approach addresses the limitations of conventional methods, offering a more comprehensive and rigorous validation of your processor’s behavior before final silicon implementation.

In order to formally verify that programs are correctly executed on your custom processor, it is necessary to divide the overall verification task into smaller pieces for obtaining convergence of the formal engines. At a high-level view, it can be split into four major parts:

1. Correct program flow, e.g. correct instruction order
2. Instruction advances through the instruction pipeline
3. Result correctness under any parallel activity
4. Assumptions to mimic compiler behavior

A simplified overview of the formal testbench is sketched in the Figure below. While assumptions mimic scheduling rules of the compiler, the other parts verify different aspects in the lifetime of an instruction. Each part can be further divided into multiple subproblems. In this blog post, we provide a brief summary of each part.

Program flow verification checks that the ASIP fetches and issues the correct instruction. Next, we need to verify that the instruction advances through the instruction pipeline and reaches the write-back stage within a limited number of cycles, unless it is explicitly killed. The cycle limit depends on the number of pipeline stages and the number of potential stalls. In theory, it is possible that a processor stalls forever, e.g. waiting for a memory response. Here, we need to assume a finite number of stall cycles. This assumption is reasonable since a processor that behaves correctly for N stalls also behaves correctly for N+1 stalls if N is large enough. Once it is proven that the instruction reaches the write-back stage, we need to check that it produces the correct result.

In this step, we run a simple but very effective test. The formal testbench is structured around three components:

1. For each instruction, a purely functional, unpipelined SystemVerilog reference model generated from nML.
2. A constrained instance of the ASIP (CPU 1) where only a single instruction is issued. All other pipeline stages as well as parallel slots are filled with NOPs.
3. An unconstrained version of the ASIP (CPU 2).

For each instruction of the ISA, we check that all three components create the same outputs if the input operands of the instruction are equal. If an instruction can be corrupted by any parallel activity, the formal engines will be able to create different results. For example, if a hazard protection between two instructions is missing, the bug won’t occur in CPU 1 since a single instruction runs in isolation and, therefore, hazards won’t occur. In CPU 2, however, the formal engines can find a sequence that triggers the missing hazard protection and hence creates a different (wrong) result.

By default, the formal engines are free to pick an arbitrary input sequence to find a counterexample opposing expected behavior. However, some input sequences can be illegal, i.e. they are not allowed to occur in reality. For example, the compiler might implement software stall rules to avoid sequences that yield data hazards. ASIPs often use unprotected pipelines, relying on the compiler to resolve conflicts, which allows removal of hazard-handling logic and optimizes core size and energy consumption. The same compiler rules are implemented for the formal testbench in the form of assumptions. Without these assumptions, formal engines can come up with counter examples that are invalid scenarios, so-called false negatives.

Since buggy assumptions are dangerous as they can potentially mask bugs by excluding legal states, it is crucial to check their correctness. This can be done in a formal over-constraint analysis, where it is formally proven that the complete design is still reachable, and by asserting the assumptions in simulation.

In the world of software-defined everything, ASIPs offer an optimal balance between flexibility and efficiency. ASIP Designer significantly accelerates the design process by allowing engineers to describe the processor architecture in a high-level language called nML. Based on this abstract model, the tool automatically generates both synthesizable RTL and a complete software development kit, streamlining the transition from architectural concept to implementation and software support. Before tape out, ASIPs require rigorous verification to ensure correctness and reliability. Traditional simulation-based verification, while effective for catching many common case bugs, can struggle to expose subtle corner cases or issues that arise under rare or highly parallel conditions.

ASIP Designer provides an advanced formal verification technique that addresses these gaps by exhaustively validating processor behavior at the ISA level. This includes the automatic generation of properties to check correct program flow, instruction pipeline integrity, and result accuracy, all while adhering compiler constraints. Combining Formal ISA Verification with other well established verification techniques such as DPV leads to a robust verification strategy. 

For more detailed information about Formal ISA Verification, please contact us to obtain access to the full white paper.