cancel
Showing results for 
Show  only  | Search instead for 
Did you mean: 
rb@
Contributor
Contributor
718 Views
Registered: ‎09-28-2016

FPGA Verification

Jump to solution

Hello,

i am new in FPGA verfication. I know the typically simulation-based  approach with testbenches and the hardware-based approach with ChipScope from XILINX.

However, what is the state-of-the-art approach in FPGA verfication? And are there any formal methods for verification?

Thanks in advance!

0 Kudos
1 Solution

Accepted Solutions
dgisselq
Scholar
Scholar
681 Views
Registered: ‎05-21-2015

rb@,

Welcome to the world of FPGA verification!

Yes, formal methods are coming into their own and can be used for FPGA verification.  Formal methods, for example, have found several bugs in prominent Xilinx's cores as of late.  (I'm hoping for fixes in Vivado 2020.1,. but we'll see.)  These include their AXI4-lite demo slave core, their AXI4 demo slave core, their AXI Ethernet-lite core, and a couple of copy-cat bugs in other cores that had the exact same problems.  Intel's AXI3 demo core was also just as broken if not worse.  These bugs were found using SymbiYosys.  Unlike many of the other formal tools on the market, there's an open source version of SymbiYosys that can handle Verilog with some SVA extensions.  If you haven't tried it out, you might wish to consider doing so.

While I consider myself a designer, I'm also my only employee.  My credibility is at stake if I don't verify my own designs.  So, while not a verification engineer, I find myself doing a lot of verification work and tasks.

I also write a blog at zipcpu.com where I discuss verification, both with formal and simulation based approaches.  Lately, the blog has been dominated by formal methods posts simply because the formal methods just keep finding bugs that were missed by the simulation approaches.

Feel free to stop by and see what you think.  You might find the tutorial on the site interesting as well, since it starts from scratch and works through design, simulation, and formal verification using SymbiYosys.

Dan

View solution in original post

1 Reply
dgisselq
Scholar
Scholar
682 Views
Registered: ‎05-21-2015

rb@,

Welcome to the world of FPGA verification!

Yes, formal methods are coming into their own and can be used for FPGA verification.  Formal methods, for example, have found several bugs in prominent Xilinx's cores as of late.  (I'm hoping for fixes in Vivado 2020.1,. but we'll see.)  These include their AXI4-lite demo slave core, their AXI4 demo slave core, their AXI Ethernet-lite core, and a couple of copy-cat bugs in other cores that had the exact same problems.  Intel's AXI3 demo core was also just as broken if not worse.  These bugs were found using SymbiYosys.  Unlike many of the other formal tools on the market, there's an open source version of SymbiYosys that can handle Verilog with some SVA extensions.  If you haven't tried it out, you might wish to consider doing so.

While I consider myself a designer, I'm also my only employee.  My credibility is at stake if I don't verify my own designs.  So, while not a verification engineer, I find myself doing a lot of verification work and tasks.

I also write a blog at zipcpu.com where I discuss verification, both with formal and simulation based approaches.  Lately, the blog has been dominated by formal methods posts simply because the formal methods just keep finding bugs that were missed by the simulation approaches.

Feel free to stop by and see what you think.  You might find the tutorial on the site interesting as well, since it starts from scratch and works through design, simulation, and formal verification using SymbiYosys.

Dan

View solution in original post