Formal Co-Validation of Low-Level Hardware/Software Interfaces

Abstract

Today's microelectronics industry is increasingly confronted with the challenge of developing and validating software that closely interacts with hardware. These interactions make it difficult to design and validate the hardware and software separately; instead, a verifiable co-design is required that takes them into account. This paper demonstrates a new approach to co-validation of hardware/software interfaces by formal, symbolic co-execution of an executable hardware model combined with the software that interacts with it.

We illustrate and evaluate our technique on three realistic benchmarks in which software I/O is subject to hardware-specific protocol rules: a real-time clock, a temperature sensor on an I2C bus, and an Ethernet MAC. We provide experimental results that show our approach is both feasible as a bug-finding technique and scales to handle a significant degree of concurrency in the combined hardware/software model.


Benchmarks

RTC

The RTC benchmark illustrates the hardware/software interface for a real-time clock. The focus is on Register B and the ten time/calendar and alarm bytes:

RTC Registers

For more information about the RTC hardware, see MC146818 data sheet.

I2C

The I2C benchmark illustrates hardware/software interface for a temperature sensor on a serial bus. Thus, this benchmark goes beyond fixed-sized register updates as illustrated by the following waveform:

MP105 I2C Write Word Protocol

For more information about the temperature sensor hardware, see TMP105 data sheet.

ETHOC

Our final benchmark concerns interrupt-driven software for an Ethernet MAC with a direct-memory access (DMA) ring. This OpenCores Ethernet MAC features 128 DMA buffer descriptors, each of which determines the memory that holds an Ethernet frame. In the case of RX frames (i.e. incoming frames), the software sets bit 15 in a buffer descriptor to 1 when the associated DMA buffer can be overwritten by the hardware. The hardware clears bit 15 to signal to the software that the DMA buffer associated with a buffer descriptor contains a new RX frame.

Ethoc Architecture Overview

For more information about the temperature sensor hardware, see ETHOC data sheet.

The Ethernet MAC can be configured to generate a hardware interrupt for each RX frame. When interrupts are disabled but RX frames should still be processed, the software polls for incoming data. Switching between polling and interrupt mode is known to be error-prone, so this benchmark is a good exemplar for concurrency bugs due to interrupts in a producer-consumer scenario (see our experimental results).


Tool usage

Our benchmarks can be downloaded here. Extract the archive and rename Makefile.in to Makefile for each benchmark. We perform our experiments using CBMC and KLEE.

RTC

To run the experiments on the RTC HW/SW model using CBMC, you can do the following steps from within the folder sw-hw/linux/rtc_x86:

  1. Set the environment variables GTCC, GTINST and CBMC in Makefile to locations of the goto-cc, goto-instrument and cbmc binaries.
  2. (Optional) If you want to expose the bug, add -D__EXPOSE_BUG__ to variable VERDEF in Makefile.
  3. Then execute the following command:
    $./run_expt.sh [Num of Runs] [Experiment Name] [Property No.(1 to 11)]

To get the total runtime and runtime spent on the decision procedure produced by the script run_expt.sh, run the command:

$./get_result.sh [(Relative) Path to the Data Folder]

You can also run the experiment from propery i to j once by exectuing the following command within the same folder:

$./run_expt_all.sh [Experiment Name] [ i ] [ j ]

Note: get_result.sh does not work with the script run_expt_all.sh

Use the same commands in the folder qemu-hw/rtc to run the experiments on the standalone HW model with CBMC.

Outputs of CBMC can be found in file data/data-[Experiment Name]-prop[Property No.].txt

To run experiments with KLEE, do the following:

  1. In Makefile set varialbes LLVM_GCC, LLVM_LD and KLEE to locations of binaries llvm-gcc, llvm-ld and klee
  2. (Optional) If you want to expose the bug, add -D__EXPOSE_BUG__ to variable PROP in Makefile.
  3. Run command
    $ make klee

The output of KLEE can be found in folder klee-last.

I2C

Run the same commands as the RTC benchmach with CBMC and KLEE. Go to folder sw-hw/linux/tmp105_x86 for the HW/SW model (property no. 1 to 17) and qemu-hw/tmp105 for the QEMU HW model (property no. 1 to 8 and 10 to 20).

ETHOC

We performed all our experiments on the ETHOC benchmark using the CPROVER benchmarking toolkit and an implementation of a partial-order based approach built into CBMC. Until a new version of CBMC is released, the binary (compiled for Linux, 64bit) can be found here. The corresponding source code patch is available as well.

To run CBMC, do the following:

  1. Set the environment variables GOTO_CC, GOTO_INSTRUMENT and CBMC in experiments.sh to locations of goto-cc, goto-instrument and the partial-order based cbmc binary.
  2. Run the command below from within the folder sw-hw/linux/ethoc and qemu-hw/ethoc to perform experiments on the HW/SW model and the QEMU HW model, repsectively.
    $./experiments.sh

Run the following command from within the folder sw-hw/linux/ethoc and qemu-hw/ethoc to perform experiments on the HW/SW model and the QEMU HW model with KLEE, repsectively.

$ make klee


Experimental Results

RTC

We found a real bug in the QEMU RTC hardware model. The bug is exposed through a test that first writes a time or calendar register and then writes to one of the control registers of the device. The CBMC logs for exposing the bug in the HW/SW model can be found here. For the QEMU HW model, look see here.

For more information about our experimental results of RTC benchmarks, see here for CBMC and here for KLEE.

I2C

The temperature sensor benchmark also helped to expose a bug in the QEMU hardware model. The bug causes data on the I2C bus to be lost because of an off-by-one error. The CBMC logs for exposing the bug in the HW/SW model can be found here.

For the combined driver code and hardware model, the idea was to simulate all possible fixed-length sequences of invocations of the driver API, such as might arise in a typical interrupt-driven setting. Our experiments with a bound of 15 driver API calls in the test harness failed to expose a property violation. CBMC timed out after 1800s when the number of API function calls was set to 20.

For more information about our experimental results of I2C benchmarks, see here for CBMC and here for KLEE.

ETHOC

The ETHOC benchmark exemplifies a known concurrency bug in a NAPI-enabled driver for an Ethernet MAC. The following figure shows an example, in which an RX frame (i.e. incoming frame) arrives just after the check for new RX frames but before the RX interrupt sources are cleared. This RX frame will not trigger an interrupt until another one arrives. If there are no other ones, the delayed RX frame will not be promoted to the socket layer. This happens when the driver is stopped, for example due to standby.

Incorrect handling of an empty RX buffer descriptor causes potential package loss

The figure below shows how the developer for the `ethoc' driver in the Linux 2.6.38 kernel release fixed the bug.

A second buffer descriptor check, after the RX interrupt sources have been cleared, detects intermittent RX frame arrivals.

The concurrent interactions of software and hardware are best clarified in the graphs showing the interleaving of software and hardware model threads that reveals the bug. These are available in PNG and SVG format (the corresponding partial orders used by CBMC are also available in graphical form, as SVG or PDF).

Summary tables and full log files of these experiments are available at ethoc-hw for the hardware model, and ethoc-sw-hw for the combined hardware+software implementation. These tables and results were generated using our benchmarking framework.


People