Imperial College London > Talks@ee.imperial > CAS Talks > Blurring boundaries: using software verification methodologies in hardware design

Blurring boundaries: using software verification methodologies in hardware design

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Grigorios Mingas.

Tools producing termination proofs have successfully been used to search for bugs in systems code. However, these tools have in general focused on arithmetic over the integers, the reals, or the rationals. This means that subtle bugs arising from the use of floating-point number representation, and its inherent finite precision, are not always detectable. Loop termination is similarly imperative as part of a custom hardware high-level design flow to ensure the implementation will work in practice. However, rarely is this considered formally; usually simulation is used to explore numerical behaviour.

This talk will present traditional techniques to prove loop termination, alonside new techniques to prove the termination of a floating-point algorithm. Finally, we investigate their use to create customise the precision throughout a hardware design. We show that using this technique, we can create a custom hardware design that is still guaranteed to terminate with a much lower precision than using an IEEE standard; this translates to significant hardware savings on an FPGA .

This talk is part of the CAS Talks series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

Changes to Talks@imperial | Privacy and Publicity