RE: [sc] Use of floating point arithmetic in embedded control software



Date view Thread view Subject view Author view Attachment view

From: David Crocker (dcrocker(at)eschertech.com)
Date: Tue 29 Oct 2002 - 00:24:39 GMT


Roger & list,

We did some investigation into the issue of correctness of programs
involving floating point operations when we came to design the floating
point model in our formal methods product (Perfect Developer). We came to
the conclusion that for very simple systems, we can track the error bound in
the formal model; but for anything more complicated (e.g. matrix inversion),
numerical analysis has to be used to determine the error bound, because the
formal model gives a worst-case error bound far worse than reality (and too
bad to be of any use in practice). We are hoping in the future to do some
research in conjunction with an organisation having numerical methods
expertise, so that we can add a more comprehensive treatment of floatng
point maths to our product. For now we support a very simple floating point
model that is correct but of limited use (e.g. we don't assume addition is
associative, because it isn't when working to a finite precision).

I don't see much problem in using the hardware floating point unit of a
popular processor rather than libraries, providing one avoids very recent
processors (or new steppings of processors), since the bugs in a popular
processor tend to be found quite quickly (and quality management has
doubtless been tightened up since the Pentium FDIV bug, including I believe
the introduction of formal methods). In this respect I would generally trust
hardware more than software (unless then software is very mature and
well-understood), since hardware manufacturers have a much greater financial
incentive to get it right first time. Naturally, one should seek evidence of
correctness.

David Crocker
Escher Technologies Ltd.
www.eschertech.com


-----Original Message-----
From: safety-critical-request(at)cs.york.ac.uk
[mailto:safety-critical-request(at)cs.york.ac.uk]On Behalf Of Rivett, Roger
(R.S.)
Sent: 28 October 2002 17:33
To: 'safety-critical(at)cs.york.ac.uk'
Subject: [sc] Use of floating point arithmetic in embedded control
software


Dear list members

We have been having a debate within my department as to the appropriateness,
or otherwise, of using floating arithmetic if the target microprocessor has
a hardware floating point unit allowing the use of software libraries to be
banned. I thought this is just the sort of topic to stir a quiescent mailing
list into life.

Date view Thread view Subject view Author view Attachment view