Hardware Verification Coursework 2022-23

Verification Plan

The verification plan can be found here.

File map

• Makefile: commands to run simulation and coverage for VGA and GPIO unit-level testing and top-level testing
• Basic GPIO Coverage: Generated in Questa GUI
• Full GPIO Coverage: Generated using vcover command
• Basic VGA Coverage: Generated in Questa GUI
• Full VGA Coverage: Generated using vcover command
• Docs Folder: Folder of PDF resources provided
• GPIO Module
• GPIO Checker: Non-synthesizable version to check GPIO outputs against
• GPIO Assertions: SystemVerilog Assertions for module verification
• GPIO TCL Script: JasperGold script used to run formal verification on the GPIO module
• GPIO JasperGold Results: Image of JasperGold results table
• VGA Module
• VGA Checker: Non-synthesizable version to check VGA outputs against
• VGA Assertions: SystemVerilog Assertions for module verification
• VGA Comparator: Used to verify Dual lock-step operation of VGA modules
• VGA TCL Script: JasperGold script used to run formal verification on the VGA module
• VGA JasperGold Results: Image of JasperGold results table
• Questa Automation Script: Runs simulation, logs all waves and opens waveform viewer
• GPIO Unit-level Testbench
• VGA Font Map File
• VGA Unit-level Testbench
• Top-level Integration Testbench

VGA Bugs and Workarounds

• It is found that upon reaching the console text region part of the frame, the VGA pixel output will be invalid for the first two pixels and will instead start at pixel_x=2 to pixel_x=240 horizontally, thus there are only 238 pixels of valid console text region
• Some of the timing parameters and porch sizes in the documentation are incorrect, the correct ones were taken from the VGA block's local parameters
• Printing to the second character row of the VGA's console text region creates very unexpected behaviour:
  • The second line will start 2 characters to the left of the first line
  • Sometimes, errernous/extra characters may be printed
• The HRESETn signal does not properly reset the data in the console text register, when performing a reset in between test-cases, this may cause the new text on screen to have some characters from the old text (whereas some characters may be reset properly)
• For the VGA Tb, only the first line was tested (Printing a total of 30 random characters for the line)
• The VSYNC and HSYNC pulses after the HRESETn signal is asserted may sometimes only go low for a single cycle (this causes a few assertions to fail thus some special cases were included to these)

Running Instructions

• Run make (vga|gpio|sys) to run each of the testbenches and start Questa, along with selecting all pins and opening the waveform
• Run jg (gpio.tcl|vga.tcl) to run formal verification for the GPIO/VGA modules respectively

Formal Verification Results

It can be seen that all required assertions have been proven with an unbounded result.

The pixel coordinate values are proven unbounded, as well as the HSYNC pulse size, however the remaining assertions are shown to never fail within the given bound (599188 cycles).

Functional and Code Coverage

The GPIO coverage file can be found here, with the functional coverage results found near the bottom of the file.

The VGA coverage file can be found here, with the functional coverage results found near the bottom of the file.

VGA Testing

Using the debug output of $display commands to render a 1-bit image of the VGA block output, along with a unicode version (located near the bottom of the log) of the randomly selected symbols from the font RAM.

VGA Simulation Log: This contains the VGA Pixel output from the simulation.