Basic Design of the Reusable Property Set

In most cases, we recommend defining any reusable property set as a standalone SystemVerilog module, which can be connected to the rest of the design using the bind construct. As we have seen in Chapter 3, the bind keyword in SystemVerilog allows a submodule to be instantiated in any module without having to modify that module’s code. Below is an example of the header code for our reusable property set, described as a standalone module.

module client_server_properties(

   input logic clk, rst,

   input logic req_valid,

   input logic [7:0] req_opcode,

   input logic [7:0] req_data,

   input logic rsp_valid,

   input logic [7:0] rsp_data);

   parameter SERVER_DELAY = 2;

...

Note that all the signals involved in the protocol are inputs here. This will usually be the case, since we are trying to observe the behavior of the protocol, not actually modify any behaviors of the design.

Another important detail of this design is the use of a SystemVerilog parameter to represent aspects of the protocol that may hold multiple possible values, but are constant for any given implementation. We could have made server_delay an input instead of a parameter, but this would potentially allow it to change at runtime in some implementation, which is specifically disallowed by the rules of the protocol. Another option would be to make it an input and use an assumption to hold it constant, but since each individual protocol-using product is likely being designed based on a single specified value, a parameter seems like a more natural choice here.

Once we have fully defined the module, we need to bind it with the design under test (DUT). We could be checking an RTL model of the client, of the server, or of the full system; in the next section we discuss some complications this can cause. But assuming for illustration purposes that we want to connect these properties to the module client_model, we could do it using a bind statement like this:

bind client_model client_server_properties (.*);

Note that the use of .* assumes that we have set the names of each interface signal to be the same in both our property module and in the design module client_model. If we have changed any signal names, we would need a standard set of port mappings in the form .<port>(<signal>), as in any submodule instantiation.

The above bind will create the same effect as if we had instantiated our module inside the design module.

Property Direction Issues

Now that we have described the outline of the module, we need to start writing the properties. But as we begin to write them, we encounter a basic issue: should they be assertions or assumptions? For example, rule 1 tells us “The opcode field has a nonzero opcode when making a request.” Which of the following is the correct implementation of this rule?

rule_1a: assert property (req_valid |-> req_opcode != 0) else $display(“opcode changed too soon”);

rule_1b: assume property (req_valid |-> req_opcode != 0) else $display(“opcode changed too soon”);

A bit of reflection will reveal that either of these might be correct. There are numerous modes in which we may want to use our properties:

The best answer is that the property might need to be either an assertion or assumption, depending on the particular application of our property set. One method we can use to provide this flexibility is through SystemVerilog parameters and macros. We need to add some parameters to define the mode in which we are building the property set, then use these flags to decide whether each property is an assertion or assumption, as in the following example:

parameter CLIENT_IS_DUT = 1;

parameter SERVER_IS_DUT = 0;

parameter SYSTEM_IS_DUT = 0;

parameter THIS_IS_DUT = 0;

`define CLIENT_ASSERT(name, prop, msg)

  generate if (CLIENT_IS_DUT | SYSTEM_IS_DUT) begin

   name: assert property (prop) else $error(msg);

  end else begin

   name: assume property (prop) else $error (msg);

  end

  endgenerate

`define SERVER_ASSERT(name, prop, msg)

  generate if (SERVER_IS_DUT | SYSTEM_IS_DUT) begin

   name: assert property (prop) else $error(msg);

  end else begin

   name: assume property (prop) else $error (msg);

  end

endgenerate

Once we have this basic infrastructure defined, our property then becomes:

`CLIENT_ASSERT(rule_1, req_valid |-> req_opcode != 0,

    “opcode changed too soon”);

Now, by choosing the proper set of parameter values to pass into our property module when invoking it, we can set up our bind statement to enable testing of the client RTL, server RTL, both, or neither. The properties for the remainder of our rules are then relatively straightforward to define, as long as we are careful to recognize which side is responsible for implementing each requirement:

`CLIENT_ASSERT(rule_2a, $rose(req_valid) |=> (

   ($stable(req_valid)) [*SERVER_DELAY]),

   “request changed too soon”);

`CLIENT_ASSERT(rule_2b, $rose(req_valid) |=> (

   ($stable(req_opcode))[*SERVER_DELAY]),

   “request changed too soon”);

`CLIENT_ASSERT(rule_2c, $rose(req_valid) |=> (

   ($stable(req_data))[*SERVER_DELAY]),

   “request changed too soon”);

`SERVER_ASSERT(rule_3, $rose(req_valid) |=>

   ##SERVER_DELAY rsp_valid,

   “rsp_valid failed to rise”);

`SERVER_ASSERT(rule_4, $rose(rsp_valid) |=>

   $fell(rsp_valid),

   “rsp_valid held too long.”);

`CLIENT_ASSERT(rule_5, $rose(rsp_valid) |=>

   $fell(req_valid),

   “req_valid held too long.”);

Note that for the rule 2 properties above, we also followed one of the tips in our earlier chapters and expressed the complex property as multiple simple properties, to separately check the stability of each field. This will likely make debug much simpler in cases where the assertions fail in simulation or FPV.

Verifying Property Set Consistency

Now that we have created an initial property set, we need to ask the question: is this property set consistent? In other words, does it enable the behaviors we associate with our protocol, in expected ways? We need to have a good answer to this question before we start binding it to RTL models for verification purposes. To do this, we need to prepare a self-checking environment where we will observe cover points and prove assertions implied by our protocol.

First, as with any FPV effort, and as discussed in the previous three chapters, we need to create a good set of cover points. In this case, there are a few obvious ones to start with:

req_possible: cover property (##1 $rose(req_valid));

rsp_possible: cover property (##1 $rose(rsp_valid));

req_done: cover property (##1 $fell(req_valid));

Note that we added an extra ##1 to the beginning of each of these, to avoid false coverage success due to possible bogus transitions at the end of reset, since it is likely that these external inputs would be unconstrained during reset.

We should also create more detailed sequence covers, so that we can see that our vision of the full flow of our protocol is possible. Often these will be inspired by waveforms we have seen in the specification. One example for our case might be:

full_req_with_data: cover property (($rose(req_valid) && (req_data != 0)) ##SERVER_DELAY $rose(rsp_valid) ##1 $fell(req_valid));

We also should create some additional assertions: properties we believe to be implicit in our protocol, which should be assured if our other properties are implemented correctly. These will be only for checking our checker, so they should be protected in a section of code that will be ignored except when the checker itself is the verification target. For example, in our protocol, we know that if the opcode changes, it cannot be during a valid request, so we might create the following assertion:

generate if (THIS_IS_DUT) begin

  self_check1: assert property ($changed(opcode) |->

                  !$past(req_valid));

end endgenerate

Now we have sufficient infrastructure that we can run our FPV tool on our property set module standalone, under the THIS_IS_DUT configuration. All our protocol-defining properties will be assumptions, so we will generate the space of behaviors that are permitted by our protocol. We can then view the cover traces and check the assertion proofs, to be sure that our set of properties is defining our protocol properly. We should spend some time looking at the generated cover waveforms, and make sure they are correctly depicting the protocol envisioned in our specification. If we see that some of the cover points are unreachable, or reachable only in ways we did not anticipate, this will indicate that there is some flaw or inconsistency in our property set that we need to further investigate.

Note that this self-consistency environment can also serve another purpose: it is a way to examine the behavior of our protocol independent of any particular RTL implementation. This can be very valuable in early protocol development and also can be a useful way to experiment with potential changes to the protocol before dealing with the complications of RTL. It can also help with judging whether behaviors described in external bug reports are truly permitted by the protocol, leading to better insight as to whether there is a core protocol bug or an issue with a particular RTL implementation. Thus, we strongly recommend that you closely collaborate with your protocol architects when developing this kind of property set and make sure to leverage it for future protocol analysis as well as RTL verification.

Checking Completeness

Another question that needs to be answered about any protocol property set is: is it complete? Does it fully capture the intent of the protocol? In many cases, this question cannot be answered except by a human who understands the protocol: most protocols we have seen are defined by plain English specifications, rather than something formal enough to be directly translatable into a set of assertions. In fact, we cheated a bit when we stated the requirements in terms of a set of well-specified rules a few subsections back. It is more likely that our requirements would initially arrive in a form something like this:

At first glance, it might appear that we are stuck with having to manually translate specifications into discrete rules for the purpose of creating assertions. However, if you can convince your architects and designers to annotate the specification, it might be possible to do slightly better. The idea is to add some known marker text, along with a stated rule, to parts of the specification that would indicate a potential assertion. If you are using a word processor with an annotation feature, you can avoid messing up the text directly. For example, the first sentence above would be connected to an annotation:

Each rule annotated in the specification has a tag, rsp_valid_delay in this case. Then we just need to ensure, using a script, that each tagged rule in the specification has a corresponding tagged assertion (with assertion tags indicated in a comment line above each assertion) in the property module. One SVA assertion might cover several rules from the specification, or several might cover the same rule; this is acceptable as long as each rule is covered. For example:

// RULES: rsp_valid_delay, opcode_valid_data_const

`CLIENT_ASSERT(rule_2a, $rose(req_valid) |=> (

     ($stable(req_valid)) [*SERVER_DELAY]),

     “request changed too soon”);

`CLIENT_ASSERT(rule_2b, $rose(req_valid) |=> (

     ($stable(req_opcode))[*SERVER_DELAY]),

     “request changed too soon”);

`CLIENT_ASSERT(rule_2c, $rose(req_valid) |=> (

     ($stable(req_data))[*SERVER_DELAY]),

     “request changed too soon”);

This method will not ensure total completeness—there is still a major human factor involved—but it does help ensure that your property module will attempt to cover each of the rules thought important by the protocol architects.

The Role of Assertions in UCE

While we can get some decent information from a simple assumption-free UCE FPV run, we can do even better if we are using a design that contains assertions. Since our premise is that if you are doing UCE, you are late in the project cycle and trying to close simulation coverage, we are probably safe in assuming that you have high confidence (resulting from many simulation runs) in the assertions that are present in your code. Since this is the case, we can create a much better UCE FPV run by converting many of those assertions to assumptions. Most modern FPV tools have commands allowing such a conversion.

This might seem a bit strange at first, since we are likely constraining many noninput nodes for testing. But remember that in FPV, an assumption is a constraint on the universe of legal simulations: in effect, we are telling the FPV tool that in any simulation, it should only consider inputs that will result in our assertions being true. This is exactly what we want since we know that none of the valid simulation tests are violating any assertions. In effect, we have further restricted our space of possible simulations, which may now allow us to prove even more cover points unreachable, as shown in Figure 7.3.

We should point out that since simulation-focused assertions are not usually created with formal rigor in mind, they are not likely to provide the full set of assumptions that defines all legal behaviors. This is why the central oval in Figure 7.3 does not coincide with the assertions-as-assumptions region around it. However, simulation-focused assertions can do an excellent job of constraining the behaviors considered by UCE FPV and better enabling a validation team to stop wasting time trying to hit truly unreachable coverage points.

One other issue to be aware of is the fact that too many assumptions can create a complexity issue for FPV. If you find that blindly converting all assumptions to assertions creates performance problems, you may want to instead manually select an interesting subset to use in your UCE FPV run.

Covergroups and Other Coverage Types

We have focused our discussion on SVA cover points, the straightforward assertion-like coverage constructs that are automatically evaluated by any FPV tool. But what about other coverage types such as SystemVerilog covergroups, or line/statement/branch coverage? In the best case, your FPV tool will have features to evaluate these kinds of coverage as well, and detect some subset of unreachable coverage constructs, such as dead code, automatically. But in cases where it does not, you will need to consider using scripts (or manual work) to create SVA cover points logically equivalent to your other constructs.

Model Build for Connectivity

The first issue that you need to think about when setting up connectivity FPV is: building the model. Until now, we have emphasized in most discussions of FPV that you will typically run on a unit or partial cluster model, due to known limitations of tool capacity. However, connectivity FPV usually makes the most sense if run at a full-chip level. Fortunately, this is not usually a major obstacle, since in most cases the full-chip connectivity models can blackbox almost all logic blocks: remember that we are just verifying the paths from top-level pins to major block boundaries. Figure 7.4 illustrates a typical full-chip model after blackboxing for connectivity verification:

As you can see in Figure 7.4, most major logic blocks can be blackboxed, with only a small subset actually needed for connectivity verification.

One common mistake when first building such a model is to start by trying to build a full-chip model with no blackboxes, then blackbox what is needed for simplification. This may be a reasonable strategy with typical simulation or floor planning tools, but tends to cause major problems with FV tools. Due to the inherent limitations of FPV capacity, such a tool will often not even be able to compile an un-blackboxed full-chip model. It is much better to start by building a “shell” model, with just the top level of your chip represented and all its submodules blackboxed. Once this is built, gradually un-blackbox elements of your design that you know are participating in top-level connectivity: control registers, MUXing blocks, and so on.

It is okay if you accidentally leave something blackboxed unnecessarily at the end of this process, since you will ultimately catch this while debugging your failing connectivity assertions. If some blackboxed element happens to fall inside a connectivity path, your FPV tool will report a bogus connectivity bug (due to treating the output of the blackboxed block as a free output), and you will discover the issue. There is no way such an extra blackbox could create a false positive, where a real error is missed. Figure 7.5 illustrates this situation.

Specifying the Connectivity

Aside from building the proper model, the other major component of the connectivity FPV setup is specifying the actual connectivity requirements. Essentially, for each top-level signal that is to be connected to the boundaries of one or more IP blocks, and each value of the relevant control registers, we need:

Most teams find it convenient to express this in some kind of spreadsheet format, as in Table 7.1.

Many EDA tools define spreadsheet formats like this that can be natively read by their tools and implicitly converted to assertions, and later back-annotated during debug to simplify the overall process. However, even without such a feature, it is relatively easy to create a script that would translate the table above into assertions like the following:

s1_conn_0: assert property ((regblk.r1 == 0) |->

   ##2 top.blk1.s1 == $past(top.s1,2));

s1_conn_1: assert property (

   (regblk.r1 == 1) && (!top.scan) |->

   ##3 (top.blk2.s1 == $past(top.s1,3));

These assertions can then be proven like any standard FPV assertions. The logic to connect SOC signals tends to be a rather simple set of MUXes and delay elements, so assertions like these are typically proven very quickly by most modern FPV tools.

Possible Connectivity FPV Complications

As mentioned above, the connectivity properties tend to involve very simple logic compared to typical FPV runs. However, there are still various complications that users of this type of flow have tended to encounter. The most common ones we have seen are low-level pad cells, complex interface protocols, and top-level constraints.

The first issue involves the fact that the top-level interface signals of a typical SOC design need to pass through pad cells to reach the outside world. These cells are often excluded by design teams from most RTL logic flows, because they represent very simple logic but possibly complex electrical and physical issues. Thus their authors, who are usually backend experts, tend to use nonsynthesizable SystemVerilog constructs such as explicit transistors and weak assignments. (If you usually work at a logic level like the authors, there is a good chance you have never seen these constructs. That is okay—at least one of the authors first learned about some of these while debugging connectivity FPV!) Since FPV tools cannot handle such constructs, they will result either in compilation errors or in bogus reports of combinational loops. Thus, to enable sensible connectivity FPV, you may need to replace low-level pad cell SystemVerilog modules with simpler logical representations. For example, you may see a cell like this, probably with less helpful comments:

module ugly_pad(vcc,vss,in1,out1)

  // Transistor structure that doesn’t change logic

  bufif1(tmp,in1,vcc);

  // Weakpull for cases when pad not in use

  assign (weak0,weak1) out1 = vss;

  // Real action of pad

  assign out1 = tmp;

end

To enable connectivity FPV, you will need to modify it so you can get a synthesizable logical view when needed:

module ugly_pad(vcc,vss,in1,out1)

  `ifdef FPV

   assign out1 = in1;

  `else

   // Transistor structure that doesn’t change

   bufif1(tmp,in1,vcc);

   // Weakpull for cases when pad not in use

   assign (weak0,weak1) out1 = vss;

   // Real action of pad

   assign out1 = tmp;

`endif

end

In general, you need to be careful when modifying any logic as part of an FPV effort, but usually the logic of these types of cells is conceptually simple. Be sure to review any changes with the cell’s original author or an equivalent expert, of course, to be sure your modifications are logically sound.

The second common challenge of connectivity FPV is the issue of programming the control registers. Normally we expect that connectivity logic will be relatively simple and not require very deep reasoning by formal engines. However, if testing conditional connectivity based on control register values, there may be more complexity due to some logical protocol being needed to program the values of these registers. You may find that you already have a good set of assumptions for this protocol, especially if using a common protocol assertion set as discussed earlier in this chapter, reducing the effort needed to create more assumptions. This could still leave you with a high-effort run by the formal engines to analyze the programming of the control registers in every connectivity proof though.

A key insight that can help to address this issue is that, when doing connectivity FPV, your goal is not really to prove the correctness of the control register programming. Presumably other parts of your validation effort, either formal or simulation runs, are already focusing on this area in greater generality anyway. When running connectivity FPV, you are just trying to prove correctness of the connectivity logic. Thus, it is likely acceptable to abstract the control registers: make them cut points, telling the FPV tool to ignore their fanins and let them take on an arbitrary value, then add assumptions to hold them constant for each formal run. This way you will prove that for any given constant value of the control registers, the connectivity is correct, even though you are not spending effort in this run to prove the correctness of the register programming logic.

The last common complication with connectivity FPV that we discuss is the problem of top-level constraints. As with any FPV run, you will often find that the first time you attempt it, you will get false failures reported due to lack of assumptions. There is really nothing special about this problem in the connectivity context; the only difference is that you may need to deal with top-level mode pins that did not affect your block-level runs. Often you will have to assume that a top-level scan or debug mode is off, or that high-level “vss” and “vcc” pins actually do represent a logical 0 and 1. You may also face issues due to multiple clocks in the design; if some IP blocks use different clock domains or clocks that have passed through a blackbox, you need to correctly inform the FPV tool of their frequency in relation to the model’s main clock. Treat this like any other FPV run and work with experts in the proper area to examine your initial counterexamples and identify relevant top-level assumptions or clocking specifications.

Specifying Control Register Requirements

Typically, a simple spreadsheet format can be used to specify the requirements on control registers. For each register, you need to specify

Then, for each field, you need

There are a number of access types supported for typical registers. Here are some of the most common ones:

In Figure 7.7, we illustrate a few lines of a typical control register specification spreadsheet.

In this example, we have two registers, each with two fields. The first, ARCH_VERSION, is at address 0010 and has security authorization code 05. It has two 16-bit fields. The arch_major field, with default value 1, is RO, probably used to communicate a hardcoded chip version to the user. The os_version field is RW, probably so it can be modified by software, and has default value 7. The second, FAULT_LOGGING, is a 17-bit register at address 0020 with security authorization code 01. It contains a 16-bit fault_status, through which the design can communicate some status information to a user, with default value 0. Its type is RWC, so the user can clear it with a write attempt. It also contains a WO fault_logging_on bit, through which a user can activate or deactivate fault logging, defaulting to 1.

We should probably comment here on why there is a spot in the table in Figure 7.7 for the internal RTL signal for each register. If we are trying to verify correct accesses through the register interface as shown in Figure 7.6, why should we care about the internal nodes? While verifying externally is the ideal, we need to keep in mind the fact that for many register types, there are major limitations to what we can verify through the external interface. For example, if a register is WO, we can never externally see the result of the write that sets its value, so what kind of assertion could we write on its correctness? Thus, whitebox style assertions, which look at the internal register node as part of the verification, often make the most sense for control registers.

Once you have decided on the specification of your control registers, you can use this information to generate SVA assertions.

SVA Assertions for Control Registers

There are many types of assertions that can be generated to check the correctness of control register accesses. Here we describe the ones that we typically use to check registers with the common access types described above (RW, RO, WO, and RWC). Each of the assertion classes below is generated for every applicable register and field. With each, we illustrate one of the assertions that correspond to the specification in Figure 7.7.

In general, you should be examining your company’s specification for its control registers, and generating assertions related to each defined operation for each register type. Don’t forget to include assertions both that correct operations succeed, and that incorrect operations do not modify the register value.

We are also assuming here that our design only allows writes at a field granularity (we should enforce this with separate assertions/assumptions), so we don’t have to account for messiness due to differing bit masks. Thus, for a given access attempt, each field is either totally enabled or totally disabled.

assign write_os_version = (opcode == WRITE) &&

    (Addr == 0010) &&

    (BitMask[31:16] != 0);

assign write_os_version_val = (DataIn[31:16]);

always @(posedge clk) begin

 if (write_os_version) begin

  write_os_version_val_last = write_os_version_val;

end end

assign read_os_version = (opcode == WRITE) &&

              (Addr == 0010) &&

              (BitMask[31:16] != 0);

assert property (write_os_version ##1

 (!write_os_version throughout read_os_version[->1]) |=>

    DataOut[31:16] == write_os_version_val_last);

The list above is not fully exhaustive, because many designs offer other register access types, locking mechanisms to limit access to certain registers, security policies that require additional inputs, and similar features. But the set of assertions we recommend here is a good starting point. Also, since most of these are expressed as triggered assertions, in most FPV tools they will automatically generate a good set of cover points showing that we can cover each typical access type.

Major Challenges of Control Register Verification

There are a number of challenges you are likely to face when setting up control register FPV. You need to properly select the verification level and the initial FPV environment for the control register FPV run. In addition, you need to account for multiple register widths and internal hardware writes.

The simplest method is to add an assumption that the internal hardware interface is inactive during control register FPV, in order to verify that the register specifications are correct with respect to the external interface. Alternatively, you can do more comprehensive verification by creating reference models of your registers that account for this alternate access path.

Building the FPV Environment

We are assuming here that you have reached a point in your initial post-silicon debug efforts where you have developed a basic understanding of your defect observation, and suspect a logic bug in a particular area of your design. As with any FPV effort, you must now choose a hierarchy level in your RTL at which to run FPV. The usual capacity limitations need to be considered here, such as being unable to run at a full cluster or chip level. Of course, you should employ the standard methods used to make designs more tractable for FPV: blackboxing large memories, reducing parameters, turning off scan modes, and so forth. However, you do have a slight advantage over general FPV runs in this case: you can take into account specific characteristics of the bug you are observing. For example, you might normally be unable to run FPV at a cluster level due to the large amount of logic. But if you know from the bug you are observing that a particular functional block is involved, you may be able to blackbox unrelated blocks.

In the case of our ALU, we are told that our sighting occurs after a series of add operations. Thus, it is likely that we do not need the logical subunit, so we should blackbox this for FPV purposes. So our first step is to blackbox the logical subunit and use FPV to try to cover the point. Here we create a cover point to look for cases where the result signal is seen without having resulted from a valid ALU uop:

c1: cover property (resultv&& !$past(uopv,ALU_DELAY));

When we run this cover point, FPV will quickly come back with a waveform that shows the blackboxed logical subunit generating a logresultv value of 1. This is because, as we have seen in previous chapters, when a unit is blackboxed, its outputs are freely generated by the FPV environment. This shows that we need to add an assumption to keep the blackboxed unit quiescent and avoid bogus traces. This is a common situation when we are blackboxing large parts of the logic while chasing a specific bug: rather than a pure blackbox, we need to make sure the ignored parts of the logic are not generating bogus traces that look like our bug but are unrealistic. Just as in regular FPV runs, you should expect a few iterations of wiggling as you fix your assumptions to avoid incorrect traces.

Now suppose we have made this fix and are attempting to run our cover point c1 again, but hit an FPV complexity issue. We should take a closer look at other ways we can narrow the proof space that the FPV tool is examining. In particular, in this case we were told that a series of add operations is triggering the bug. This means that in addition to eliminating the logical subunit, we should also constrain the arithmetic subunit to only consider OPADD operations:

 fv_overconstrain_add:

  assume property (Uopcode == OPADD);

While this might be too overconstraining for a general-purpose proof, again we need to keep in mind that we are trying to focus on a particular bug we have observed in the post-silicon lab. In general, we should not be afraid to add very specific assumptions to help narrow down the proof space to correspond to the bug we are chasing.

Once we have added this assumption, we are focusing more directly on our suspected bug. Now when we attempt the FPV proof on our cover point, we are much more likely to be able to see a real waveform that corresponds to our problem from the lab. Once we have reproduced this in an FPV environment, it will probably be very easy to find its root cause in the RTL logic.

The Paradox of Too Much Information

One tricky issue that is sometimes faced by those performing post-silicon FPV is the paradox of having much more information than is needed. For example, suppose our debug lab has sent us a set of scan traces from our ALU, showing the values of thousands of signals over the course of thousands of cycles. In theory, we could convert these to thousands of assumptions, in line with the principle above of overconstraining our design to focus on the bug. But will this help our FPV run?

Actually, adding large numbers of assumptions can often increase the complexity of the state space, reducing rather than increasing the efficiency of FPV. While a small number of assumptions can help to reduce the problem space, having lots of assumptions can make it a more computationally difficult problem to explore that smaller space. Since we are working with heuristics and provably complex problems, there are no hard-and-fast rules here, but in general, you should avoid converting a full scan dump into FPV assumptions.

Figure 7.10 illustrates this issue in an abstract way. The oval on the left represents the full behavioral space of a design. The one in the middle shows the space with a small, clean set of assumptions: for any given point, it is fairly easy to determine whether it is in the acceptable proof space. The one on the right illustrates the situation with a complex set of assumptions. While the overall legal proof space that must be analyzed may be smaller, it now is very complex to determine whether any given behavior is inside or outside the acceptable space, due to the irregular boundaries created by the large number of assumptions.

Thus, instead of blindly translating all your scan data to assumptions, use your scan dump as a source of information and just choose a handful of significant signals based on your knowledge of the most important parts of the design for your particular bug. For those signals that you have identified as important, use the scan dump values to create assumptions. It can be difficult when you do not know exactly where the bug is, but try to be sparing in your choice of significant signals, to avoid a complexity blowup due to assumption handling.

Using Semiformal Design Exploration

One other important technique you are likely to make use of in post-silicon analysis is semiformal verification. This refers to the idea of running FV starting from a known active state, a “waypoint,” rather than starting from a reset point. This makes the verification less general, but when trying to reproduce or hunt for bugs, can enable you to reach a bug much faster if the proper waypoints are chosen.

In the case of our ALU example, suppose we find that FPV always hits complexity issues after reaching a proof bound that encompasses two complete ADD operations. We can set our first waypoint to be a cover point indicating the completion of the first operation:

waypoint1: cover property ( resultv &&

  $past(uop,ALU_DELAY)==OP_ADD);

When we get a cover trace for this property, we can then save that and use it as the reset phase for our next FPV run. This means we will be doing a less general analysis that full FPV—starting from the trace of one particular completed ADD operation rather than a fully general one—but this may allow the formal engine to reach a depth where it has analyzed three ADD operations instead of just two.

In cases of greater complexity, it is often beneficial to define several waypoints: use FPV to cover the first one, then use the first waypoint to start an FPV run that reaches the second, and so on. For example, perhaps we might need to define a second waypoint, indicating the completion of the next ADD operation, in order to generate a run that reaches the bug on the ALU. On some models, the use of multiple waypoints can enable successful FPV bug hunting at a significantly greater depth than might initially seem feasible.

We will discuss semiformal verification in more detail in Chapter 10, where we describe many techniques for dealing with complexity. But we highlight it here because it is a method that has shown itself to be particularly valuable in the context of using FPV to analyze post-silicon bugs.

Proving your Bug Fixes Correct

Once you have successfully reproduced a post-silicon bug by generating a trace with FPV, you will hopefully be able to examine the RTL operations involved and come up with a bug fix. Then you will face another issue, similar to the diagnosis problem but with some important differences: proving the bug fix correct. This is actually one of the really powerful arguments for using FPV in post-silicon: the ability to not only replicate a bug, but to then prove that a proposed fix really fixes the bug, for traces more general than the particular one that triggered the initial issue. As you have probably seen if you have been involved in real-life post-silicon debug challenges, it is often the case that an initially proposed bug fix for a tough post-silicon issue will overlook some detail and not be a fully general fix.

The most obvious way to check the completeness of a bug fix is to load your modified RTL into the same FPV environment that you used to diagnose the bug and make sure it proves that your bug-related cover point can no longer be reached. This is an important sanity-check, and if the models you are using are very complex for FPV, or required techniques such as semiformal verification to enable a usable run, it may be the best you can do to gain confidence in the fix. But you should not stop at this point if you can avoid it.

Remember that for diagnosing the issue, we stressed the need to overconstrain the design to focus on the particular bug. But when trying to prove the bug fix fully general and correct, you need to reexamine the overconstraints, and make sure they were each truly necessary. For example, in our ALU model, we might ask ourselves:

To answer these questions, we need to either remove some of the assumptions and blackboxes or create special-case FPV environments with a different set of assumptions to check the parts of the logic we skipped: check operations other than OPADD, or switch the blackbox to the arithmetic subunit while un-blackboxing the logical one.

Conceptually, it is often much easier to generalize an FPV environment than it would be to generalize a simulation environment, when trying to provide more complete checking of a proposed bug fix. The challenge is to recognize that you need to pay extra attention to this problem; after a grueling high-pressure post-silicon debug session, there is often an inclination to declare victory as soon as FPV first passes. FPV has a lot of power, but you must remember to use it correctly.

Practical Tips from this Chapter