10 ms·
AMD was a major user of ACL2 and verified AMD Athlon FPU using ACL2. Their case study is IMO an approachable presentation of what realistic verification of FPU
by sanxiyn 9y ago
AMD was a major user of ACL2 and verified AMD Athlon FPU using ACL2. Their case study is IMO an approachable presentation of what realistic verification of FPU looks like in practice.
http://www.russinoff.com/papers/fadd.html http://www.russinoff.com/papers/fadd.html