Jonathan Certes

Home / Research / Open Hardware Logic Analyser empowered with Verilator

Abstract

This tool has been deployed during the following project: Attestation of the ARM cortex-A9 processor configuration; technical insights are provided here. It is an integrated logic analyser implemented from open hardware and free software. While permitting to plot the data, it also allows to use this data in a SystemC testbench and make it interact with models of the hardware compiled with Verilator.

Hardware description for the logic analyser, along with a program to plot the data and simulate hardware models, are available here . In this webpage, we list some available features.

Prerequisites

The source code of the software is written in C++ and uses the SystemC library. In order to work properly, the following commands must be available:

• verilator
• gtkwave

Debian package verilator provides verilator. Debian package gtkwave provides gtkwave. Also, the SystemC library must be available. Debian package libsystemc provides this library.

Finally, a solution to synth and implement the hardware on a dedicated FPGA must be available. A debugger must allow to read data from the internal memory of the logic analyser. In this project, we used Xilinx Vivado for synthesis and implementation and openOCD as an on-chip debugger.

Description

The logic analyser embeds a True Dual Port BRAM to store the traces.

• One port is connected to an integrated controller that reads data from a 32-bit vector and writes it to the BRAM interface. It starts writing when a trigger is received and ends when the BRAM is full.
• The other port is connected to an AXI BRAM controller that is connected to a ARM microprocessor. The on-chip debugger asks the microprocessor to retrieve data from the BRAM when the analysis is complete.

A GPIO is used to enable or disable the logic analyser from the microprocessor. While we debug, we can call a function to switch this GPIO. Also, the debugger is used to write the content of the RAM into a file. Let's imagine that the virtual address for the RAM is 0x42000000 and the RAM has 4KB of memory, here is a gdb script to read this data:

set logging off
set logging overwrite on
set logging redirect  on
set logging file ./hw/logic_analyzer/decode/data_fetch.gdb
set logging on
x /1024wx 0x42000000
set logging off

Once the file is written, a C++ program uses scanf to fill a table:

#define DATA_COUNT 1024
uint32_t theDataValue[DATA_COUNT] = {};

Then, a SystemC module reads the data at each rising edge of a clock:

SC_MODULE( stimulus ) {
  sc_in  <bool>     clk;
  sc_out <uint32_t> data;
  int32_t count = 0;

  void stimulusGen( void ) {
    if ( count < 0 ) {
      data.write(0x00000000);
    } else {
      data.write( theDataValue[count]);
    }
    count = count + 1;
    if ( count >= (int32_t)(sizeof(theDataValue)/sizeof(uint32_t)) ) {
      sc_stop();
    }
  }

  SC_CTOR(stimulus) {
    SC_METHOD(stimulusGen);
    sensitive << clk.pos();
  }
};

The decoding of the data is performed by a Verilog module that can be converted to SystemC with Verilator. Obviously, any other Verilog module can be instantiated too if we aim at post-processing the data or simulating a device with the data as input. Here is a decoding example:

module decode(
  input [31:0] data
);
  wire        sw_arvalid;
  wire [13:0] sw_araddr;
  wire        sw_arready;
  wire  [7:0] trace_data;
  wire        trace_ctl;

  assign { sw_arvalid, sw_araddr, sw_arready } = data[31:16];
  // bits data[15:9] are unused
  assign { trace_data, trace_ctl             } = data[8:0];
endmodule

In the end, the SystemC program writes the Value Change Dump into a file which we can open with gtkwave.

VerilatedVcdSc* theOutput = new VerilatedVcdSc;
Verilated::traceEverOn(true);
i_decode.trace(theOutput, 99); // depth in the hierarchy
theOutput->open("output.vcd");
sc_start();
theOutput->close();

A complete example that uses this open hardware logic analyser is available here . It allowed to retrieve the traces for publication Attaque et sécurisation d'un schéma d'attestation à distance vérifié formellement (French). To reproduce the experiment, a Digilent Cora Z7 development board is required.

Recorded presentations

• THCon 2022: Attacking formally verified hardware monitors
• SSTIC 2022: Attaque et sécurisation d'un schéma d'attestation à distance vérifié formellement (French)

Associated publications

• Jonathan Certes, Benoît Morgan, Attaque et sécurisation d'un schéma d'attestation à distance vérifié formellement (French), SSTIC 2022
• Jonathan Certes, Méthodes et modèles pour la vérification formelle de l'attestation à distance sur microprocesseur (French), 2023

---