Date: Wed, 03 Feb 2021 02:06:46 +0000
To: Luke Kenneth Casson Leighton <lkcl@lkcl.net>,
 Bitcoin Protocol Discussion <bitcoin-dev@lists.linuxfoundation.org>
From: ZmnSCPxj <ZmnSCPxj@protonmail.com>
Reply-To: ZmnSCPxj <ZmnSCPxj@protonmail.com>
Message-ID: <oCNGbVElAQCJ1bEmwLXLzIVec0ZoOA2Ar3vkOc1a0GW12h78bhMi_W4n3pCdDt7hJyPFoMRb0U1T5Wx5uQl4oo6zeQtjKs0MdAXGtvLw1SQ=@protonmail.com>
In-Reply-To: <CAPweEDx4wH_PG8=wqLgM_+RfTQEUSGfax=SOkgTZhe1FagXF9g@mail.gmail.com>
References: <CAPweEDx4wH_PG8=wqLgM_+RfTQEUSGfax=SOkgTZhe1FagXF9g@mail.gmail.com>
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8
Content-Transfer-Encoding: quoted-printable
Subject: Re: [bitcoin-dev] Libre/Open blockchain / cryptographic ASICs
Precedence: list

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 ge=
ometries, you also start approaching analog design.
In our case we were already manually laying out gates and flip-flops (or re=
placing flip-flops with level-triggered latches and being extra careful wit=
h clocks) to squeeze performance (and area) for some of the more boring par=
ts (i.e. just deserialization of data from a high-frequency low bus width t=
o a lower-frequency wide bus width).

Formal correctness proofs are nice, but we were impeded from using those be=
cause 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 equivale=
nce of the netlist to the RTL; the correctness of the RTL was "proved" by s=
imulation 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 cove=
rage 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 Ass=
ertions / PSL assertions and validate that your RTL conformed to the assert=
ions, 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 / ene=
rgy 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 fas=
t or cheap, just very accurate to the required specification, the larger ge=
ometries should be fine and you would be able to live almost entirely in RT=
L-land without diving into netlist and layout specifications.

A wrinkle here is that licenses for tools from tr\*sted vendors like Synops=
ys or Cadence are ***expensive***.
What is more, you should really buy two sets of licenses, e.g. do logic syn=
thesis 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 particul=
ar 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 su=
pport for SystemVerilog (though to be fair, there is little that SystemVeri=
log 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 experime=
ntal support for those for `always` variants).
Note as well that I heard (at the time when I was in the industry) that som=
e foundries will not even accept a netlist unless it was created by a synth=
esis 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 lib=
re / transparently-developed ASIC / SoC, for some time, since meeting a ver=
y interesting person at the Barcelona RISC-V Workshop in 2018.
>
> this person pointed out that FIPS-approved algorithms, implemented in FIP=
S-approved crypto-chips used in hardware wallets to protect billions to tri=
llions in cryptocurrency assets world-wide are basically asking for trouble=
.=C2=A0 i heard 3rd-hand that the constants used in the original bitcoin pr=
otocol were very deliberately changed from those approved by FIPS and the N=
SA for exactly the reasons that drive people to question whether it is a go=
od idea to trust closed and secretive crypto-chips, no matter how well-inte=
ntioned the company that manufactures them.=C2=A0 the person i met was ther=
e to "sound out" interested parties willing to help with such a venture, ev=
en to the extent of actually buying a Foundry, in order to guarantee that t=
he crypto-chip they would like to see made had not been tampered with at an=
y point during manufacturing.
>
> at FOSDEM2019 i was also approached by a team that also wanted to do a ba=
sic "embedded" processor, entirely libre-licensed, only in 350nm or 180nm, =
with just enough horsepower to do digital signing and so on.=C2=A0 since th=
en, fascinatingly, NLnet has obtained a new EU Horizon Grant and started th=
eir "Assure" Programme:
> https://nlnet.nl/assure/
>
> (our application may be found here):
> https://libre-soc.org/nlnet_2021_crypto_router/
>
> in addition, betrusted (headed by Bunnie Huang) is also funded by NLnet a=
nd is along similar lines:
> https://betrusted.io/
>
> NLnet is even funding LibreSOC with a 180nm test chip tape-out of the Lib=
reSOC Core, with help from Sorbonne University and https://chips4makers.io
> https://bugs.libre-soc.org/show_bug.cgi?id=3D199
>
> and we also have funding to do Formal Correctness Proofs for the low-leve=
l portions of the HDL (similar to c++ and python "assert", but for hardware=
)
> https://bugs.libre-soc.org/show_bug.cgi?id=3D158
>
> the point being that where even one year ago the idea of an open source d=
eveloper creating and paying for an actual ASIC was so ridiculous they woul=
d be laughed at and viewed in a derisive fashion thereafter, reality is tha=
t things are opening up to the point where even Foundry PDKs are now open s=
ource:
> https://github.com/google/skywater-pdk
>
> technically it is possible to use Open Hardware to create commercial (clo=
sed) products.=C2=A0 Richard Herveille, most well-known for his early invol=
vement in Opencores, was the Open Hardware developer responsible for the HD=
L behind the first Antminer product by Bitmain, for example.=C2=A0 It used =
his RV32 core and i believe he also developed the SHA256 HDL for them.=
=C2=A0 however that is different in that it was a closed product, not open =
for independent public audit and review.
>
> what i am therefore trying to say is that it is a genuinely achievable go=
al, now, to create fully transparently-openly-developed ASICs that could pe=
rform crytographic tasks such as mining and hardware wallet key protection =
*and have a full audit trail* even to the extent of having mathematical For=
mal Correctness Proofs.
>
> my question is - therefore - with all that background in mind - is: is th=
is something that is of interest?
>
> now, before getting all excited about the possibilities, it's critically =
important to provide a reality-check on the costs involved:
>
> * 350nm ASICs: https://chips4makers.io - EUR 1750 for 20 samples
> * 180nm ASICs: EUR $600 per mm^2 MPW Shuttle (test ASICs) and EUR 50,000 =
for production masks
> * ... exponential curve going through 130nm, 65nm, 45nm gets to around $5=
00k...
> * 28nm ASICs: USD 100,000 for MPW and USD $1 million for production masks
> * 22nm ASICs: double 28nm
> * 14nm: double 22nm
> * 7nm: quadruple 14nm
>
> you get where that is going.=C2=A0 where higher geometries are now easily=
 within reach even of a hobbyist ASIC developer, USD 20 million is a bare m=
inimum to design, develop and bring to manufacture a 7nm Custom ASIC.=C2=
=A0 full-custom silicon, as carried out regularly by Intel, is USD 100 mill=
ion.
>
> this is not to say that it is completely outside the realm of possibility=
 to do something in these lower geometries: you either simply have to have =
a damn good reason, or a hell of a lot of money, or a product that's so com=
pelling that customers really *really* want it, or you have OEMs lining up =
to sign LOIs or put up cash-with-preorder.
>
> [my personal favourite is a focus on power-efficiency: battery-operated h=
and-held devices at or below 3.5 watts (thus not requiring thermal pipes or=
 fans - which tend to break). i have to admit i am a little alarmed at the =
world-wide energy consumption of bitcoin: personally i would very much pref=
er to be involved in eco-conscious blockchain and crypto-currency products]=
.
>
> so - as an open question: what would people really like to see happen, he=
re, what do people feel would be of interest to the wider bitcoin community=
, and, crucially, is there a realistic way to bridge (fund) the gap and act=
ually deliver to the bitcoin user community?
>
> best,
>
> l.
>
> ---
> crowd-funded eco-conscious hardware: https://www.crowdsupply.com/eoma68
>
> --
> ---
> crowd-funded eco-conscious hardware: https://www.crowdsupply.com/eoma68