> A NASA Langley presentation [2] mentions formal verification of the FCP-2002. I think that if it is formally verified, it is probably not a 286. A 286 would be a poor choice for a formally verified microprocessor for embedded applications since it has a huge number of extraneous features that would complicate the verification process while yielding no benefit for the embedded application.
That's an interesting observation. The presentation specifically mentions verification of the microcode, which I think would be feasible to do for a 286?
> I'm not sure where this "286" stuff comes from. I think maybe, FCP-2002 is a 16-bit CPU, and then people say a 16-bit CPU is "like a 286", and then maybe that gets corrupted in the retelling, and "like a 286" turns into "a 286"?
Yeah, I'm not sure where the rumour came from either. But I do think it's plausible. According to "Computers take flight" [1], the 777 uses (among others) a 486 for its control system:
> Boeing finally built an airliner with fly-by-wire controls, the 777. The control system is more straightforward than that used by Airbus. It contains three “lanes” of three different computers each: an AMD 29050, a Motorola 68043, and an Intel 80486.
The source given is "Primary flight computers for the Boeing 777" [2], which doesn't seem publicly available.
Given the closeness in time for the 777 and the 737 NG, it seems somewhat unlikely (to me) that the 777 would go for the most popular options, while the 737 would use a bespoke CPU design. The A320 used 80186 and 68K processors [3], so the 737 would really be the odd one out in that case.
1: https://ntrs.nasa.gov/archive/nasa/casi.ntrs.nasa.gov/200501...
2: https://www.sciencedirect.com/science/article/abs/pii/S01419...
3: https://books.google.se/books?id=KDX0BwAAQBAJ&pg=PA214&lpg=P...