Hacker News new | ask | show | jobs
by swiley 1809 days ago
IMO: the underlying architecture is mostly relevant to kernel/compiler authors and people doing aggressive optimization. For most application devs it's about as irrelevant as you can get (unless your language has a very hard to port compiler cough rust.)

What's good about this is that the source is available and can be verified to some degree against the hardware (by decapping it.) That puts a log of constraints on what kinds of secret back doors people can build that we didn't have before.

2 comments

Rust supports powerpc64le-unknown-linux-gnu, it is in-fact what we used to test a lot of POWER9's instructions to replicate the exact results that POWER9 gives, since the ISA spec doesn't specify the results for a lot of cases.

https://git.libre-soc.org/?p=power-instruction-analyzer.git;...

I was talking about new architectures in general, not just powerpc.
ultimately what we'd like to see is entirely NDA-free PDKs even for 12nm and below, and you can run the VLSI tools and generate the EXACT GDS-II yourself, then yes, de-cap the processor and do a digital comparison.

before you even get to that stage, you run the Formal Correctness Proofs and unit tests on the HDL, so that YOU have confidence that the HDL which you're about to generate the GDS-II files from is actually correct and does the damn job.

example of a Formal Correctness Proof for the fixed arithmetic Power ISA pipeline:

https://git.libre-soc.org/?p=soc.git;a=blob;f=src/soc/fu/alu...

runs with symbiyosys, so you end up running SAT Solvers like yices2 and z3.

basically we absolutely do not want to be the people you come to and say, "can we trust your ASIC?" and like Intel they lie to you and say "of course!", we want to say, "don't bloody well ask us, go run the damn tools yourself! oh, btw, if you want help with that we charge USD 5k per hour"