On Jan 28, 1:56 am, Paul Rubin <http://[EMAIL PROTECTED]> wrote: > Paddy <[EMAIL PROTECTED]> writes: > > I would rather advocate such random test generation methods as being > > more appropriate for testing software in safety critical systems when > > the programming language is dynamic. > > That method totally failed to find the Pentium FDIV bug, and they use > static proof checkers like ACL2 now.
I would doubt that they would use purely static methods to verify such large and complex chips. You need a spread of methods, and some techniques find more bugs at different stages of the design. When alerted to the existence of a bug then you have to create a test find it and might well choose to create assertions for formal proof on that section of the design. Given the complexity of current microprocessors i'm guessing that their previous testing methods would be too good to just junk in totality because the FDIV bug was not found. Similarly if they were not using formal methods then it makes sense to add it too your arsenal; and unfortunately it takes a mistake like that to allow different methods to be explored and incorporated. It's rarely either/or. More a question of the right, cost-effective, mix of tools to find bugs, and get the product released on time. - Paddy. -- http://mail.python.org/mailman/listinfo/python-list
