Good morning Luke,
I happen to have experience designing digital ASICs, mostly pipelined data
processing.
However my experience is limited to larger geometries and in SystemVerilog.
On the technical side, as I understand it (I have been out of that industry for
4 years now, so my knowledge may be obsolete) as you approach lower geometries,
you also start approaching analog design.
In our case we were already manually laying out gates and flip-flops (or
replacing flip-flops with level-triggered latches and being extra careful with
clocks) to squeeze performance (and area) for some of the more boring parts
(i.e. just deserialization of data from a high-frequency low bus width to a
lower-frequency wide bus width).
Formal correctness proofs are nice, but we were impeded from using those
because of the need to manually lay out devices, meaning the netlist did not
correspond exactly to an RTL that formal correctness could understand.
Though to be fair most of the circuit was standard RTL->synthesized netlist and
formal correctness proofs worked perfectly well for those.
Many of the formal correctness proofs were really about the formal equivalence
of the netlist to the RTL; the correctness of the RTL was "proved" by
simulation testing.
(to be fair, there were tools to force you to improve coverage by injecting
faults to your RTL, e.g. it would virtually flip an `&&` to an `||` and if none
of your tests signaled an error it would complain that your test coverage
sucked.)
Things might have changed.
A good RTL would embed SystemVerilog Assertions or PSL Assertions as well.
Some formal verification tools can understand a subset of SystemVerilog
Assertions / PSL assertions and validate that your RTL conformed to the
assertions, which would probably help cut down on the need for RTL simulation.
Overall, my understanding is that smaller geometries are needed only if you
want to target a really high performance / unit cost and performance / energy
consumption ratios.
That is, you would target smaller geometries for mining.
If you need a secure tr\*sted computing module that does not need to be fast or
cheap, just very accurate to the required specification, the larger geometries
should be fine and you would be able to live almost entirely in RTL-land
without diving into netlist and layout specifications.
A wrinkle here is that licenses for tools from tr\*sted vendors like Synopsys
or Cadence are ***expensive***.
What is more, you should really buy two sets of licenses, e.g. do logic
synthesis with Synopsys and then formal verification with Cadence, because you
do not want to fully tr\*st just one vendor.
Synthesis in particular is a black box and each vendor keeps their particular
implementations and tricks secret.
Pointing some funding at the open-source Icarus Verilog might also fit, as it
lost its ability to do synthesis more than a decade ago due to inability to
maintain.
Icarus Verilog only supports Verilog-2001 and only has very very partial
support for SystemVerilog (though to be fair, there is little that
SystemVerilog adds that can be used in RTL --- `always_comb` and `always_ff`
come to mind, as well as assertions, and I think recent Icarus has started
experimental support for those for `always` variants).
Note as well that I heard (at the time when I was in the industry) that some
foundries will not even accept a netlist unless it was created by a synthesis
tool from one of the major vendors (Synopsys, Cadence, Mentor Graphics, maybe
more I have forgotten since).
Regards,
ZmnSCPxj
> folks, hi, please do cc me as i am subscribed "digest", apologies for the
> inconvenience.
>
> i've been speaking on and off with kanzure, asking his advice about a libre /
> transparently-developed ASIC / SoC, for some time, since meeting a very
> interesting person at the Barcelona RISC-V Workshop in 2018.
>
> this person pointed out that FIPS-approved algorithms, implemented in
> FIPS-approved crypto-chips used in hardware wallets to protect billions to
> trillions in cryptocurrency assets world-wide are basically asking for
> trouble. i heard 3rd-hand that the constants used in the original bitcoin
> protocol were very deliberately changed from those approved by FIPS and the
> NSA for exactly the reasons that drive people to question whether it is a
> good idea to trust closed and secretive crypto-chips, no matter how
> well-intentioned the company that manufactures them. the person i met was
> there to "sound out" interested parties willing to help with such a venture,
> even to the extent of actually buying a Foundry, in order to guarantee that
> the crypto-chip they would like to see made had not been tampered with at any
> point during manufacturing.
>
> at FOSDEM2019 i was also approached by a team that also wanted to do a basic
> "embedded" processor, entirely libre-licensed, only in 350nm or 180nm, with
> just enough horsepower to do digital signing and so
