Hello.
On 07/10/2018 07:36 AM, David Lanzendörfer wrote:
And apparently AMD is giving us competition right now in producing back door free CPUs in China: https://www.golem.de/news/hygon-dhyana-china-baut-cpus-mit-amds-zen-technik-...
Well, from a verification point of view, you can not claim that a CPU is bug- and/or back-door free.
By formal verification techniques we can assure, that the CPU has a dedicated property like "reacting 3 clock cycles after reset is released".
Getting closer to your target, we would have to fully verify the whole CPU design by 100%. That is what Formal Verification is for.
And BTW, the best effort in that direction for RISC-V Clifford already did - he focus' his activities to verification [0] and published the stuff on github [1]
We need LibreSilicon here even more, 'cause only in that way with the right tools, costumers can verify that we did not put in new hidden "features" while manufacturing. Please check the classic paper from Ken Thompson [2]
Regards, Hagen.
[0] https://media.ccc.de/v/34c3-8768-end-to-end_formal_isa_verification_of_risc-... [1] https://github.com/cliffordwolf/riscv-formal [2[ https://dl.acm.org/citation.cfm?doid=358198.358210