Imperial College London > Talks@ee.imperial > CAS Talks > Blurring boundaries: using software verification methodologies in hardware design
Log inImperial users Other users No account?Information onFinding a talk Adding a talk Syndicating talks Who we are Everything else |
Blurring boundaries: using software verification methodologies in hardware designAdd 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. This talk is included in these lists:
Note that ex-directory lists are not shown. |
Other listsTalks Type the title of a new list here Complexity & Networks GroupOther talksContext-based vision processing system Control of CPS using Passivity and Symmetry Closing the loop with Networked Cyber-Physical Systems - CANCELLED |