Xprova: Formal Verification Tool with Built-in Metastability Modeling

# Xprova: Formal Verification Tool with Built-in Metastability Modeling

Ghaith Tarawneh.red[*], Andrey Mokhov

Newcastle University, UK

.footer.venue[ACSD 2017 - Zaragoza, Spain - June 29th 2017]

---

.footer.venue[ACSD 2017 - Zaragoza, Spain - June 29th 2017]

---

## POETS Project Team

---

## Outline

.active.circle[1] .big[Overview]

.active.circle[2] .big[What is Metastability?]

.active.circle[3] .big[Clock Domain Crossing Verification]

.active.circle[4] .big[Presented Tool (Xprova)]

.active.circle[5] .big[Conclusion]

---

## Overview

- We present a model checker, .emph[Xprova], that can simulate metastability
effects digitally and discover errors in clock domain crossing circuits.

- Based on the approach described in:

.graybox.citation.extrapad.paperoverlay[Tarawneh, G, Mokhov, A and Yakovlev, A. ".emph[Formal Verification of Clock Domain Crossing Using Gate-level Models of Metastable Flip-flops]". In Design, Automation & Test in Europe Conference & Exhibition (DATE) 2016.]

---

# What is Metastability?

---

## Metastability

Synchronous circuits are designed such that .blue.emph[data transitions] always arrive at their destination flip-flops before the next .red.emph[clock edge].

---

## Metastability

But transitions coming from .emph[other clock domains] are .emph[asynchronous] and their arrival time relative to the local clock .emph[cannot be constrained].

---

## Metastability

When an asynchronous transition arrives close to the sampling clock edge, the receiving flip-flop may get marginally triggered and become .emph[metastable].

---

## Metastability

A metastable flip-flop can take .emph[longer time] to resolve to a stable state, like a ball gently nudged to arrive at the top of a hill before rolling off.

---

## Metastability

Taking a long time to settle means that the flip-flop output transition gets .emph[delayed] and may not reach all destinations in time.

---

## Metastability

This may cause receipient flip-flops to sample different values of the delayed signal, causing a .emph[misinterpretation error].

---

## Metastability

Delayed transitions can also marginally-trigger subsequent flip-flops, causing metastability to .emph[propagate].

---

## Can it be avoided?

- Metastability is a .emph[fundamental property] of all physical systems that attempt to make a discrete decision based on analog input.

- It cannot be avoided, but its probability can be .emph[exponentially reduced] by allowing the system more time to settle.

- Failure rate is typically expressed as the Mean Time Between Failures (MTBF):

.center[
<img class="equation" src="https://latex.codecogs.com/svg.latex?\text{MTBF}=\frac{e^{t_s/\tau}}{f_c f_d T_w}" border="0"/>
]

---

## Synchronization

- In digital systems, flip-flop chains known as .emph[synchronizers] are often used to allocate settling time (usually one clock cycle).

- This typically gives a MTBF in excess of thousands of years.

---

# Clock Domain Crossing Verification

---

## Clock Domain Crossing

Clock Domain Crossing (CDC) is the transfer of signals between clock domains.

---

## Clock Domain Crossing

How do we verify that a CDC design works correctly?

- In general, designers follow certain .emph[rules of thumb] when designing CDC circuits. These rules are derived form theory.

- Synchronization is a common patterns but there are many .emph.green[Do's] and .emph.red[Dont's].

---

## Clock Domain Crossing Verification

- Verifying CDC circuits is very challenging because

.graybox.attentionoverlay[
  Metastability is .emph[completely transparent] in digital simulation.
  ]

- Most digital simulation and verification tools model flip-flops as ideal storage devices. This abstraction does not capture the conditions and functional consequences of metastablity.

- Therefore, designs that pass (conventional) testbench and formal verification may still fail catastrophically when implemented in silicon.

---

## Clock Domain Crossing Verification

- State of the art CDC verification:

.graybox.center[
  Lint designs against lists of pre-programmad .emph[bad design patterns]
  ]

where ".emph[bad design patterns]" are any structural or functional properties that may cause problems (e.g. missing synchronizers)

- This is a .emph[safe] but .emph[conservative] approach that has several disadvantages:

1. .red.emph[High rate of false positives]
  2. .red.emph[Poor generality]
  3. .red.emph[Poor debuggability]

- Can we do better?

---

# Xprova

---

## The Basic Idea

Solve the problem directly: .emph[make metastability observable in digital simulation!]

- Xprova reads a gate-level netlist and generates .emph[an augmented netlist] that can simulate metastability effects but is otherwise functionally identical.

- The augmented netlist can then be used in digital simulation to observe, identify and fix metastability-related design issues.

---

## Netlist Transformation

Given an input netlist ...

---

## Netlist Transformation

Identify flip-flops that can become metastable..red[*]

---

## Netlist Transformation

Replace identified flip-flops with models that can simulate metastability effects.

Also duplicate combinational logic and insert connections as necessary.

---

## With Formal Verification

- Metastability onset, propagation and resolution are .emph[non-deterministic] events

- Non-determinism is modeled using .emph[random-bits] in flip-flop model cells

- Combined with formal verification, netlist augmentation can be used to .emph[exhaustively explore] the functional impact of metastability on a given circuit

---

## Example

Can Assertion 1 be violated?

---

## Example

Can Assertion 1 be violated?

---

## Example

Can Assertion 1 be violated?

---

## Example

Can Assertion 1 be violated?

---

## Example

Can Assertion 1 be violated?

---

## Feature Overview

- Xprova consists of a .emph.underlined[netlist preprocessor] and a .emph.underlined[model checker]

- Reads gate-level netlists in .emph.underlined[Verilog 2001]

- Supports a subset of .emph.underlined[SystemVerilog Assertions]

- Supports .emph.underlined[safety and liveness properties]

- Integrates with free tools including yosys, dot and gtkwave

---

## Internally ...

---

## Example Usage

```ruby
# load cell libraries
library load gates90nm.v
library load lib/xprova.v

# load design
read examples/fifo/fifo.v

# define assumptions and assertions
assume full |=> ~write
assume empty |=> ~read

assert ~(empty & full)
assert write |=> ~empty
assert read |=> ~full

# start verification
prove

```

---

## Use Cases

The two papers present detailed use cases and comparisons with commercial CDC
verification tools that rely on linting:

.graybox.citation.extrapad.paperoverlay[Tarawneh, G and Mokhov, A. ".emph[Xprova: Formal Verification Tool with Built-in Metastability Modeling]". In International Conference on Application of Concurrency to System Design (ACSD) 2017.]

---

## Conclusion

- Clock domain crossing verification is challenging because digital simulation and verification tools cannot model metastability.

- We presented a model checker (Xprova) that can simulate metastability effects and detect specification violations caused by metastable states

- Xprova is .emph[open source] and available under an .emph[MIT License]:

➜ .fancylink[https://github.com/xprova/xprova]

➜ .fancylink[https://xprova.net]