Jonathan Certes

Home / Research / Automated formal verification of hardware designs

Motivation

Back in 2021, we decided to formally verify a hardware device dedicated to the security of Remote Attestation. The hardware was described in Verilog HDL and had to be synthesized before its implementation in a FPGA Artix-7. Our objective was to ensure that the final implementation (in the FPGA) meets its specification.

State-of-the-art research has been dedicated to efficient and/or automatic abstraction for Register Transfer Level (RTL) Verilog. The authors take advantage of the high-level aspect of RTL to provide sound abstractions for the system and increase compositional model-checking efficiency.

Unfortunately, the synthesis process (before the implementation in the FPGA) is not proven to preserve semantics and verified property at RTL may not hold at the netlist level.

This weakness has been pointed out by more recent works, which suggested to verify the system after the synthesis step. The issue was that no automatic solution existed to tackle the state-space explosion problem at this level. The remaining solution was to manually abstract the system for each local property and manually verify that the resulting netlisted circuit was sound according to the final implementation.

We decided to provide an automated solution to:

• abstract the system at the netlist level
• provide a certificate that the results are sound according to the final implementation

Solution

Basically, the idea is to perform two synthesis of the circuit:

• one to generate the final implementation,
• one to generate an abstract model dedicated to the verification of one property (this is repeated for each property to verify).

Then, the results of the synthesis are converted to deterministic Büchi automata and a program establishes a simulation relation between the two models that preserves temporal logic properties. A certificate guarantees that the simulation relation can be established.

The solution conducts 4 steps:

1. a synthesis of the RTL is performed to generate the final implementation.
2. the property to verify is parsed from the AST of the model-checker, a Verilog wrapper is created where outputs that do not appear in the property are left unconnected.
3. a synthesis of the RTL encapsulated in the wrapper is performed to generate the abstract model.
4. two Büchi automata are generated from the results of the synthesis and compared. A certificate guarantees the soundness of the abstract model.

The strength of this approach is that it makes the verification process possible for any synthesis optimizations algorithm and configuration as soon as our certificate guarantees its soundness.

The only restriction is to use the same algorithm and configuration for generating both the final implementation and its abstract model.

Certificate

For both the concrete and the abstract model, the Verilog netlist is converted to a deterministic Büchi automaton.

• States are encoded using state variables.
• The transition function is partitioned as a conjunction of transitions for each state variable.

To establish a simulation relation between two models, we compare initial states and transitions. We verify that all partition from the abstract model exist and are identical in the concrete model. Same goes for initial states.

As consequence, we establish a simulation relation parameterized by a Galois connection between the two models, where a state from the abstract model is simulated by all states in the concrete model where the state variables have the same values.

The language of the abstract model is then included in the language of the concrete model and temporal properties are preserved.

Associated resources

This approach has been applied to the verification of RTL Verilog that is synthesized with yosys.

Wrapper is created from the results of Verilog parsing by icarus and properties parsing by NuSMV.

Büchi automata are described in SMV language and generated by Verilog2SMV.

The certificate is generated by a program based on pyNUSMV to manipulate the AST that results from a parsing by NuSMV.

Model-checking is performed by NuSMV.

• Here is the source code of the whole automated framework.
• Here is an example of how to compare two Büchi automata.
• Here , here and here are tools to automatize the creation of a wrapper from a Verilog model and a temporal property.
• Here is an example of how to convert a wrapped Verilog to a Büchi automaton.
• Here is an example of how to split replicated properties into a set of singled properties.
• Here is an example of how to convert NuSMV counterexamples into VCD.

Recorded presentation

• ERTS 2022: An Automated Framework Towards Widespread Formal Verification of Complex Hardware Designs (replay)

Associated publications

• Jonathan Certes, Benoît Morgan, An Automated Framework Towards Widespread Formal Verification of Complex Hardware Designs, ERTS 2022
• Jonathan Certes, Méthodes et modèles pour la vérification formelle de l'attestation à distance sur microprocesseur (French), 2023

---