Skip to content

A collection of formal properties for hardware buses, and cores using them.

License

Notifications You must be signed in to change notification settings

rlee287/hardware-bus-infrastructure

Repository files navigation

Hardware Bus Infrastructure

Introduction

The goal of this project is to develop formal verification properties for various bus standards, write documents to assist people in using these busses, and create verified example cores and infrastructure (e.g. interconnects) based on these properties. Lowering the entry barrier for formal verification will allow more people to write HDL modules with the guarantee that they will work properly.

Please see CONTRIBUTING.md before submitting issues or pull requests.

Status Table

Key to emojis:

  • ❌ : Item is not started
  • ➖ : Item is in progress
  • ➕ : Item is completed but has not been tested sufficiently
  • ✔️ : Item is completed and has been tested sufficiently

All entries may contain an issue number tracking progress on the item.

Item Wishbone 4 Classic Wishbone 4 Pipelined AXI4-Stream AXI4-Lite AXI4
Formal Property Set (SVA) ➖ (#1, #3, #4)
Formal Property Set (PSL) ➖ (#1, awaiting #3 merge)
Bus Summary
Example Cores (expand list later) ❌ (#5)

Bus Standards

This repository has (or will have) the following busses:

Document Types

Formal Property Sets

Formal property sets use a "monitor" type bus in which all bus signals are inputs, and assert properties over the inputs. These check whether an implementation of a bus is standards-compliant, so all assertions and assumptions must have a comment next to them pointing to the clause in the standards document justifying them. These modules may also have outputs tracking useful bus data (e.g. number of bytes transferred).

In order to support open source projects, SVA properties should work with the open-source version of Yosys, and PSL properties should work with GHDL. (PSL units should be written to work with other open-source tools that supports PSL, but I am not currently aware of any open-source tools besides GHDL that use PSL.)

Bus Summary

Bus summaries are non-code documents that summarize the signals of a bus and the properties that should hold on them, as well as recommendations on using the bus effectively. They are a quick reference document and should be easier to read than the original standards document. To ensure accuracy, descriptions of the bus should have a reference to the original specification.

Example Cores

Example cores demonstrate how to implement a core with bus interface(s) and must be formally verified using a formal property set. Because their goal is to help other developers use these bus standards, they should be written for readability. Example cores should be written for highest bus performance, but may also have options to trade performance against simplicity. For example, an AXI example core should be written for 100% throughput, but it can have a parameter to limit it to 50% throughput and remove the need for skid buffers.

About

A collection of formal properties for hardware buses, and cores using them.

Topics

Resources

License

Code of conduct

Stars

Watchers

Forks

Releases

No releases published