[Club2] talk by Alexander Schade: tomorrow, Wed., May 21, 15:00, Room: Turing (00.09.38)

[Andrei Popescu]

Dear All,  

Tomorrow at the usual time we have a BA presentation by Alexander Schade.  
 
Cheers, 
  Andrei  

Applying SMT to Hardware Verification
Alexander Schade
======================================================================
Wed., May 21, 15:00, Room: Turing (00.09.38)

In hardware model checking the correctness of a hardware system with respect to a specification is established using fully automated prover 
algorithms. The hardware system is created using a hardware
 description language Verilog or VHDL, and properties are specified using a property specification language, such as SystemVerilog assertions (SVA) or PSL. Sub-sequently a model checking tool is used to show the correctness or to find counter-examples. In my thesis, I implement an extension to a 
preexisting commercial bounded model checking system by OneSpin Solutions. My ex-tension adds support for external SMT-solvers software, interfacing via the SMT-LIB standard. SMT-solving is an emerging technology for automated reasoning, and is an extension of SAT-solving. Though the OneSpin tool supports an internal word level representation called Rt, OneSpin 
Solutions were not making use of SMT solvers yet. My implementation is a first at-tempt to use SMT technology. In my thesis, I explain in detail the procedure,that is required to translate expressions in a word-level algebra to the dif-ferent SMT-LIB logics QF
 BV, QF ABV, QF LIA, QF NIA, QF LRA andQF NRA. For the real number logics QF LRA and QF NRA my translation procedure performs an overapproximation of the original problem. The proof method with real numbers is thus sound but incomplete. Finally I evaluate my procedure in four different benchmarks, aiming at demonstrating applicability of arrays, linear arithmetic and real numbers to hardware model checking. I found, that my real number overapproximation enable us to prove correctness of a Newton-Raphson divider, which was not possible with any preexisting solver in the OneSpin system. In my benchmarks,array theories give performance benefits of 
about 50. Linear arithmetic theories are superior to model checking with QF BV, but cannot beat the OneSpin tool. QF BV showed some advantage in equivalence checking of circuits with arithmetic.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20140520/1b97046a/attachment.html>