by Ajay Daga, CEO, FishTail Design Automation, and Benoit Nadeau-Dostie, Chief Architect, Mentor Graphics
Built-In Self-Test (BIST) is widely used to test embedded memories. This is necessary because of the large number of embedded memories in a circuit which could be in the thousands or even tens of thousands. It is impractical to provide access to all these memories and apply a high quality test. The memory BIST (MBIST) tool reads in user RTL, finds memories and clock sources, generates a test plan that the user can customize if needed, generates MBIST IP, timing constraints, simulation test benches and manufacturing test patterns adapted to end-user circuit.
Multi-cycle paths (MCPs) are used to improve the performance of the circuit without having to use expensive pipelining which would be required when testing memories at Gigahertz frequencies. Most registers of the MBIST controller only update every two clock cycles. Only a few registers need to operate at full speed to perform the test operations. The architecture takes advantage of the fact that most memory test algorithms require complex operations such as Read-Modify-Write.
MBIST IP has a large number of MCP sources with tens or even hundreds of destinations. Some of the MCP sources also have single-cycle path destinations. The identification and classification of MCPs is done by analysis based on experience acquired over the years. Timing constraints are verified in-house using SystemVerilog assertions (SVA) on representative benchmark circuits. The benchmark circuits must be chosen carefully because they correspond to specific instances derived from a highly parameterizable RTL template. The timing constraints are implemented in a way to minimize the number of parameter combinations affecting the constraints. Nevertheless, there is always a small possibility that a combination was missed.
End users currently don’t have a mechanism to run formal verification of all constraints (MBIST and functional). They need to assume that MBIST constraints are correct by construction and waive violations causing a disruption of the design flow. Timing simulations need to be used if desired to validate MBIST constraints. This is very difficult because of the large number of memories in a circuit.
It is well known that simulation-based methods (using either full timing or assertions) are limited by the quality of test benches which might not exercise all useful signal transitions and by simulation time which might be prohibitive. Formal verification of timing constraints is clearly a better alternative although there are a number of obstacles to overcome before it can be used effectively.
There is a learning curve involved in using such verification tools and new scripts need to be generated and maintained to integrate the tools in the design-for-test flow. Until now, there were also a number of limitations of the formal verification tools that made it difficult to use on our MBIST IP. A first limitation was that these tools generally analyze constraints individually. However, the MBIST constraints are not all self-contained and were causing a large number of false alarms. For example, take the following set of constraints:
set_multicycle_path 2 -setup -from STEP_COUNTER*
set_multicycle_path 1 -setup -from STEP_COUNTER*
The first constraint declares MCPs from the counter to all destinations but the second constraint resets some of the paths to be SCPs. The first constraint is not true when analyzed in isolation.
A second issue is correctly understanding the coded RTL, so that false violations are not flagged by the formal tool.
Noisy results are a legitimate concern when deploying a formal solution, so we needed to be convinced that the results from the tool are consistent with the information provided to it. The third challenge is the ability to provide architectural input to the tool in situations where MCPs are not completely supported by the RTL. This architectural input (waivers) needs to be specified in a way that accounts for the parameterizable nature of the design. Common waivers need to be specified for hundreds of MBIST controllers, each using a different set of circuit parameters which might affect the composition of the timing constraints.
FISHTAIL’S MCP VERIFICATION METHODOLOGY
FishTail’s Confirm product performs MCP verification. The tool requires the following information for a design:
- Synthesizable RTL
- Tcl MBIST constraints
- Simulation models for standard cells instantiated in the RTL
- Liberty models for hard macros, memories
Figure 1: Example MCP
With this information the tool formally establishes the correctness of the multi-cycle paths without requiring any stimulus. For any paths that fail verification the tool generates a waveform that shows why the path fails and provides aids for an engineer to debug the failure.
In addition, the tool generates SVA assertions for all failing paths. These assertions may be imported into RTL functional simulation to obtain third-party confirmation of the failure. Engineers can provide architectural input to the tool (information that is not available in the synthesizable RTL) that support the timing exceptions. For example, the fact that configuration registers are static, or expected to be programmed in a certain way, or that failures to certain endpoints can be ignored, etc. With this additional input the tool is often able to prove the correctness of a timing exception that was earlier flagged as incorrect. Engineers decide on the effort they want to spend in getting the tool to formally prove a timing exception, or whether they want to reduce this effort and instead establish the correctness of the exceptions based on the feedback they get from running RTL simulations on the assertions generated for failing paths.
The formal verification of an MCP requires proving that it is impossible for a change at a startpoint to propagate to an endpoint in a single cycle. Consider the example design in Figure 1. Consider that an engineer has specified a two-cycle MCP from FF1 to FF2. Formally proving this MCP requires establishing that in the clock cycle that FF1 transitions, it is impossible to propagate this transition to FF2. Proving the MCP requires establishing the condition when FF1 can transition. We refer to this as the Startpoint Transition Condition (STC) and it takes into account any enable logic in the clock and data path that control when the startpoint is allowed to transition.
In Figure 1, FF1 receives a clock without gating and the only enable logic is on the datapath. If valid is low the old value is maintained on FF1 and when valid goes high a new value is sampled by FF1. So, the STC is “valid”, i.e. valid must be high for FF1 to transition in the next cycle. Next, we consider the condition necessary for the transition to propagate from startpoint to endpoint. We refer to this as the Path Propagation Condition (PPC). In Figure 1, there is no interesting enable logic on the datapath, the only enable that controls the propagation of a path from FF1 to FF2 is the clock-gate enable for the clock pin on FF2. FF2 only receives a clock when valid is high. As a result the PPC is “valid”. The STC establishes the condition for the startpoint to transition, and the PPC establishes the condition for the transition to propagate to the endpoint in the subsequent cycle. Formally proving an MCP requires proving that if the STC is true in a cycle, then in the next cycle it is impossible for the PPC to be true.
Performing this proof requires working logic cones back over as many clock cycles as required to reach a definitive answer. For the circuit in Figure 1, proving the MCP requires proving that it is impossible for valid to be high in two consecutive clock cycles and this proof passes as valid toggles every clock cycle.
FishTail’s strength in MCP verification comes from its ability to prove MCPs as correct when the provided collateral supports the MCP without requiring an engineer to fiddle with settings that control the sequential depth for the formal proof, or the runtime allowed to prove an MCP. Inconclusive or noisy results are the bane of formal tools, and it is important for a user to have the confidence that when an MCP fails FishTail formal proves it is most likely because of missing architectural information and not because the tool ran into complexity issues. The ability to prove MCPs while minimizing complexity issues comes from FishTail’s ability to accurately separate signals on a design into either data or control. Data signals play no role in the STC and PPC established by the tool, allowing the tool to scale and work back more cycles during formal proof than would otherwise be possible.
For every failing timing exception the tool generates a report explaining why the path is not multi-cycle. An example report is shown in Figure 2.
Figure 2: Example report for failing multi-cycle path
The report in Figure 2 shows the start and endpoint that the failure applies to and the launch and capture clocks associated with the path. Clicking on the PPC/STC shows you these conditions. Clicking on the red path in Figure 2 shows you more detail on the timing path from the startpoint to endpoint, as well as any gating along the path. The path may be viewed in schematic form using FishTail’s integration with Verdi ® .
The intent of reviewing the PPC/STC and the path detail is to establish if things are as expected, or if a path is being traversed that is not intended, or if the necessary gating conditions are not in place to control when the startpoint can transition and when this change is allowed to propagate to the endpoint. If everything is as expected, then the next step is to review the stimulus the tool generates showing how the failure happens. An example failure stimulus is shown in Figure 3. This stimulus, similar to a VCD dump from a simulation tool, shows signal values in clock cycles leading up to a failure. The cycle where the failure happens is shown in red. In this cycle, the startpoint changes and the change propagates to the endpoint.
Figure 3: Example failure stimulus
Using FishTail’s integration with Verdi this stimulus may be viewed as a digital waveform but the benefit of the tabular display is that you can ask the tool to justify a signal value in a given clock cycle. For example, clicking on the value 1 shown for RESET_REG_DEFAULT_MODE in the failure cycle results in the tool highlighting signal values that cause RESET_REG_DEFAULT_MODE to go high when the startpoint changes. Since RESET_REG_ DEFAULT_MODE is a combinational signal the values that are highlighted are in the current cycle on the registers STATE and BIST_EN_RETIME2. You can then click on values on these registers, for example, the value 1 on BIST_EN_RETIME2 to see what values in the previous cycle cause this signal to be high in the failure cycle. In this manner you can keep working backward from the failure cycle to understand how the failure happens. As part of this process if you see a transition or a value that is impossible based on architectural considerations (for example, the way configuration registers, such as LVISION_WTAP_IR_REG/ INST_INT are programmed) then this information can be communicated to the tool. At this point, rather than redo the entire MCP verification run you can reverify just the specific failing path you have been debugging to see if the additional input resolves the failure.
Formal MCP verification debug requires the involvement of a designer who is familiar with the RTL and the motivation for the MCP. It requires time, and the benefit is a 100% result. When time is short, an IP is not well understood, or designer time is scarce an alternate strategy is to take the assertions generated for failing MCPs and run them through RTL functional simulation. If an assertion fails then it is a strong indicator that an MCP is incorrect. If an assertion is checked and it always passes then it builds confidence that the MCP is correct. Figure 4 shows an example assertion generated by FishTail. Essentially, the assertion checks that when a startpoint changes then in that clock cycle the PPC must be false, or in the next cycle the endpoint must not change.
In this article we have motivated the need to formally verify MBIST MCPs, discussed FishTail’s methodology for MCP verification and the approach used to debug formal MCP verification failures or generate assertions for import into RTL functional simulation. The methodology was applied to a small MBIST IP with 59 MCPs. The MCPs applied to a total of 2090 paths. Initially, after providing the tool just RTL and constraints as input, 92% of the constrained paths were confirmed as good and 167 paths failed formal MCP verification. The runtime was less than a minute. We then debugged the failures and provided additional architectural information to the tool regarding the way LVISION_WTAP_ INST/LVISION_WTAP_IR_REG is programmed, that LV_ WRCK, LV_SelectWIR and LV_ShiftWR are static. With this additional input the number of failing paths dropped to 15 (so 99% of the paths constrained by MCPs were verified to be good). Legitimate MCP issues were flagged by the tool, some that were expected and some that were surprises.
The formal verification of MBIST MCPs using RTL input guarantees the correctness of MBIST MCPS at the time they are written, and then ensures that while revisions to RTL and constraints are being made, the MBIST MCPs are continually verified to be good. Customers who receive MBIST IP are able to verify MCPs delivered along with this IP, accounting for any customization they make.
Figure 4: Example assertion for a failing MCP
// Path propagation condition:
// ( TARGET1_CK100_MBIST1_MBIST_I1/RESET_REG_DEFAULT_MODE )
// Launch Clock: CK100 (rise)
// Startpoint: TARGET1_CK100_MBIST1_MBIST_I1/ALGO_SEL_CNT_REG_reg
// Capture Clock: CK100 (rise)
// Endpoint: TARGET1_CK100_MBIST1_MBIST_I1/MBISTPG_DATA_GEN/WDATA_REG_reg
module u_mcp449_1 (input bit clk, input logic from_reg, input logic [1:0]
to_reg, input bit v12122);
wire path_propagation_condition =
( v12122 );
@(posedge clk) `FT_DISABLE (`FT_TRANSITIONS_AND_NOT_UNKNOWN(from_reg))
|-> ((##0 (!path_propagation_condition)) or
mcp449_1: assert property(e_mcp449_1);
bind TARGET1_CK100_MBIST1_LVISION_MBISTPG_CTRL u_mcp449_1
sva_u_mcp449_1(.clk(BIST_CLK), .from_reg(ALGO_SEL_CNT_REG), .
Back to Top