4 ms·

If doing the formal route, then Centaur's reports are worth looking at for using ACL2: https://www.researchgate.net/publication/267809758_Use_of_Formal_Verific

If doing the formal route, then Centaur's reports are worth looking at for using ACL2: https://www.researchgate.net/publication/267809758_Use_of_Formal_Verification_at_Centaur_Technology https://www.researchgate.net/publication/267809758_Use_of_Fo... https://www.cs.utexas.edu/users/hunt/talks/2021-11-Centaur.pdf https://www.cs.utexas.edu/users/hunt/talks/2021-11-Centaur.p... (Note: That one is kind of a marketing piece, too.) In high-assurance systems, both formal methods and exhaustive testing are supposed to be used. I'd be curious to see the results of the submitted tech on designs such as the VAMP processor and Rockwell Collins AAMP7G. https://www.researchgate.net/publication/220643416_Putting_it_all_together_-_Formal_Verification_of_the_VAMP https://www.researchgate.net/publication/220643416_Putting_i... https://www.khoury.northeastern.edu/home/pete/acl206/slides/hardin.pdf https://www.khoury.northeastern.edu/home/pete/acl206/slides/...

rowanG077 3y ago
Exhaustive testing is used? Only in some very special cases that can be done... Take the PMULLD instruction. It takes two 128-bit inputs. If you assume you can verify one input in 1ns. An exhaustive test will take 3.67 × 10^60 years. Orders of magnitude longer then the age of the universe.
- nickpsecurity 3y ago
  I meant it figuratively. Safety and security certification at high levels often required that every module and function be tested. That was on top of black box testing and pen testing. Some practitioners added fuzz testing, path-based, symbolic, combinatorial, etc. So, not literally exhaustive. They just covered every function, feature, interface, and combination that might trigger a bug. Although, some rare folks did do literally- exhaustive testing of algorithms and FSM’s on 8-bit MCU’s since they had 256 values per variable. Others and I put timers on loops to force it to be terminating and just analyzed those cases. One could use exhaustive testing in the small to justify modeling a function with a specific formula. If you have several of those, then methods like Cleanroom Software Engineering let you semiformally verify the correctness of upper layers. So, there’s some stuff like that which was used on an ad hoc basis. Most just tested values and combinations likely to trigger bugs since they were in ranges that cause effects.

rowanG077 3y ago

Exhaustive testing is used? Only in some very special cases that can be done... Take the PMULLD instruction. It takes two 128-bit inputs. If you assume you can verify one input in 1ns. An exhaustive test will take 3.67 × 10^60 years. Orders of magnitude longer then the age of the universe.

nickpsecurity 3y ago
I meant it figuratively. Safety and security certification at high levels often required that every module and function be tested. That was on top of black box testing and pen testing. Some practitioners added fuzz testing, path-based, symbolic, combinatorial, etc. So, not literally exhaustive. They just covered every function, feature, interface, and combination that might trigger a bug. Although, some rare folks did do literally- exhaustive testing of algorithms and FSM’s on 8-bit MCU’s since they had 256 values per variable. Others and I put timers on loops to force it to be terminating and just analyzed those cases. One could use exhaustive testing in the small to justify modeling a function with a specific formula. If you have several of those, then methods like Cleanroom Software Engineering let you semiformally verify the correctness of upper layers. So, there’s some stuff like that which was used on an ad hoc basis. Most just tested values and combinations likely to trigger bugs since they were in ranges that cause effects.