Skip to content
Hallway
0:00 / 0:00

#axi#formalverification#symbiyosys

Formally Verifying AXI Interfaces - Dan Gisselquist - ORConf 2019

FOSSi Foundation

6.8K subscribers • 4 videos on Hallway

YouTube
  • Recommended by 1 person: 1 in engineering communities.
  • Presented by Dan Gisselquist, owner of Gisselquist Technology

Advanced. Deep dive for people who know the field.

3.1K views7 years ago1 recommendation

HardwareSoftware designFormal methods and verificationEmbedded systemsSoftware architecture

Dan Gisselquist discusses using formal properties to verify AXI and AXI-lite interactions and highlights bugs found in open-source projects.

Gisselquist Technology, LLC, has recently developed a set of formal properties for verifying both AXI and AXI-lite interactions. The properties were then applied to many open source projects. In this talk, Dr. Gisselquist will discuss both how the property set works and some of the bugs he has found using it. Presenter: Dan Gisselquist Dr. Gisselquist is the owner of Gisselquist Technology, LLC, a services based microbusiness focused on providing superior computer engineering and signal processing services to our customers. Dr. Gisselquist has an M.D. in Computer Engineering and a Ph.D. in Electrical Engineering both from the U.S. Air Force Institute of Technology. His most recent work has involved formally verifying bus components using SymbiYosys. Talk recorded at ORConf 2019, the Open Source Digital Design conference, held in Bordeaux, France and organized by the FOSSi Foundation.

Why it's here

1 person recommends this

What people say. Recommended for understanding the complexities of the AXI bus and how to use formal verification to find bugs in hardware designs.

u/ZipCPUin r/FPGA • Recommends

On “Sending and reading data from PS to PL”

I would recommend that you get used to working with the AXI bus. The Zynq chips are built around it, with the idea that all interaction between the ARM and the programming logic is to take place using the AXI bus. Unfortunately, Xilinx's AXI demonstration designs are quite broken, and much of their non-demonstration designs are so proprietary that they become difficult to work with. Perhaps I may offer some alternatives. - This article discusses how to build an AXI-lite core, without the bugs found in Xilinx's demo AXI-lite core - This article discusses how to build an AXI4 (full) core, again without the bugs found in Xilinx's demo core - This article discusses a series of open source…
21View on Reddit

u/ZipCPUin r/FPGA • Recommends

On “[SV] I'm trying to improve how I write testbenches, and have some questions about best practices.”

I would highly discourage the use of blocking assignments in clocked blocks such as you have above--even in simulation. For an ugly, but still fairly simple, example--see this twitter thread. My own experience with test benches has been less than satisfactory--I seem to keep missing critical issues. This has left me wondering whether or not I am able to write good test benches in the first place, or for that matter how hard it is to write a good test bench in the first place. Digging further, I've discovered several examples of severe AXI protocol errors, within a certain major vendors AXI protocol interactions. Given that these bugs passed a "best in class" simulation test bench, conta…
3View on Reddit

u/ZipCPUin r/FPGA • Recommends

On “Is AXI too complicated?”

1. Both their AXI-lite and AXI demos have bugs in them. These have been reported, and I expect fixes in another 4-months or so. Xilinx claims these bugs are only in the demonstration IP created by the IP packager, but these same bugs have crept into their own IP. (Intel's AXI3 demo's are just as buggy, if not worse--you can find those documented on my twitter feed.) I've written about these bugs on my blog, described them in my latest ORCONF presentation (see Youtube for the video), and even searched Xilinx's forums for evidences of folks struggling with these bugs. (Lots of evidences of design lockups that could be due to this.) 2. Their AXI ethernet-lite IP has a bug where 1) if yo…
2View on Reddit