“Phalanx” – Greek warfare strategy for Formal Property Verification

When running Formal Property Verification, we often see goals that are neither proven nor failing (especially on complex properties), which implies inconclusive goals, also referred to as bounded proofs. In these scenarios, what we have at hand is the Formal bounded depth (in terms of clock cycles), associated with such inconclusive properties.

As hard working engineers, we are analogous to warriors and we fight the enemy i.e. nonconvergence in this case by employing all our Formal powers – abstractions, helper assertions, Formal tool help to name a few. If we win the battle – achieve full convergence, we can rejoice in the victory parade.

However, the other outcome of the battle is the loss whereby you still don’t have a full convergence and the only possible upside is that you get a higher Formal depth.

At this stage, not only have you depleted your arsenal but are also being mandated by the management to achieve signoff.

I am sure by now you must have figured out that I am drawing an analogy between a war setting and Formal verification.

This is where I draw parallelism to the ancient Greek warfare strategy called “Phalanx”.

Phalanx was a formation of warriors armed with spears and interlocking shields in Ancient Greek warfare.

Once the Phalanx was formed, soldiers advanced as one entity, fighting off attacks from enemy soldiers with their shields. The tight formation also allowed them to break through the ranks of the enemy army. The success of the Phalanx was dependent on the strength and discipline of the soldiers who made up the closely packed formation. This implies that the Phalanx was only as strong as the weakest soldier in the group. For any movie buffs, see the film 300.

Formal Verification is nothing but a “Phalanx” formation. In the presence of a group of inconclusive properties, your “Phalanx” (Formal verification) can be argued to be as strong (confidence in signoff) as the weakest soldier (Formal bounded depth). This is especially true if there is limited design know how.

The next hurdle is – How do you gauge the strength (Formal signoff) of your weakest (Formal bounded depth) soldier?

This is where VC Formal helps.

Coverage metrics like line, condition, toggle, FSM are a de facto standard for verification signoff. They are the backbone of simulation based verification. So, it makes sense to use the same metrics for Formal-based verification signoff as well.

VC Formal Property Verification allows you to run “Bounded Coverage Analysis” to a specific depth (in this case the Formal bounded depth) using Formal Property Verification results and targeting the same de facto coverage metrics.

The outcome of such a bounded analysis lets the user know what part of design is covered within the stipulated number of clock cycles, but more importantly what part of design logic is unreachable.

The key to coverage driven analysis is the ability to visualize the RTL. VC Formal enables visualization of the RTL in Formal aware Verdi Coverage. Not only does VC Formal identify unreachable code, but it goes one step further and identifies the constraints responsible for unreachability (if applicable).

The RTL coverage score along with critical information on what part of the RTL is unreachable and which constraints are responsible, help gauge the strength of your Formal verification (Phalanx formation).

Employ the “Phalanx” in VC Formal to understand how strong your Formal verification is.