From: ZmnSCPxj <ZmnSCPxj@protonmail•com>
To: Luke Kenneth Casson Leighton <lkcl@lkcl•net>,
Bitcoin Protocol Discussion
<bitcoin-dev@lists•linuxfoundation.org>
Subject: Re: [bitcoin-dev] Libre/Open blockchain / cryptographic ASICs
Date: Wed, 03 Feb 2021 02:06:46 +0000 [thread overview]
Message-ID: <oCNGbVElAQCJ1bEmwLXLzIVec0ZoOA2Ar3vkOc1a0GW12h78bhMi_W4n3pCdDt7hJyPFoMRb0U1T5Wx5uQl4oo6zeQtjKs0MdAXGtvLw1SQ=@protonmail.com> (raw)
In-Reply-To: <CAPweEDx4wH_PG8=wqLgM_+RfTQEUSGfax=SOkgTZhe1FagXF9g@mail.gmail.com>
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 on. since then, fascinatingly, NLnet has obtained a new EU Horizon Grant and started their "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 and is along similar lines:
> https://betrusted.io/
>
> NLnet is even funding LibreSOC with a 180nm test chip tape-out of the LibreSOC Core, with help from Sorbonne University and https://chips4makers.io
> https://bugs.libre-soc.org/show_bug.cgi?id=199
>
> and we also have funding to do Formal Correctness Proofs for the low-level portions of the HDL (similar to c++ and python "assert", but for hardware)
> https://bugs.libre-soc.org/show_bug.cgi?id=158
>
> the point being that where even one year ago the idea of an open source developer creating and paying for an actual ASIC was so ridiculous they would be laughed at and viewed in a derisive fashion thereafter, reality is that things are opening up to the point where even Foundry PDKs are now open source:
> https://github.com/google/skywater-pdk
>
> technically it is possible to use Open Hardware to create commercial (closed) products. Richard Herveille, most well-known for his early involvement in Opencores, was the Open Hardware developer responsible for the HDL behind the first Antminer product by Bitmain, for example. It used his RV32 core and i believe he also developed the SHA256 HDL for them. 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 goal, now, to create fully transparently-openly-developed ASICs that could perform crytographic tasks such as mining and hardware wallet key protection *and have a full audit trail* even to the extent of having mathematical Formal Correctness Proofs.
>
> my question is - therefore - with all that background in mind - is: is this 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 $500k...
> * 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. where higher geometries are now easily within reach even of a hobbyist ASIC developer, USD 20 million is a bare minimum to design, develop and bring to manufacture a 7nm Custom ASIC. full-custom silicon, as carried out regularly by Intel, is USD 100 million.
>
> 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 compelling 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 hand-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 prefer to be involved in eco-conscious blockchain and crypto-currency products].
>
> so - as an open question: what would people really like to see happen, here, 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 actually 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
next prev parent reply other threads:[~2021-02-03 2:06 UTC|newest]
Thread overview: 13+ messages / expand[flat|nested] mbox.gz Atom feed top
2021-01-25 18:00 Luke Kenneth Casson Leighton
2021-01-26 10:47 ` Pavol Rusnak
2021-02-03 2:06 ` ZmnSCPxj [this message]
2021-02-03 13:24 ` Luke Kenneth Casson Leighton
2021-02-11 8:20 ` ZmnSCPxj
2021-02-13 6:10 ` ZmnSCPxj
2021-02-13 9:29 ` Luke Kenneth Casson Leighton
[not found] ` <CAPweEDymve0zRaqN9yEGHyOeuaSLEYWQ0K2h6usWbXiV=HkOzA@mail.gmail.com>
2021-02-13 14:59 ` Bryan Bishop
2021-02-13 16:44 ` Luke Kenneth Casson Leighton
2021-02-13 17:19 ` Luke Kenneth Casson Leighton
2021-02-14 0:27 ` ZmnSCPxj
2021-02-03 3:17 ` ZmnSCPxj
2021-02-03 14:07 ` Luke Kenneth Casson Leighton
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to='oCNGbVElAQCJ1bEmwLXLzIVec0ZoOA2Ar3vkOc1a0GW12h78bhMi_W4n3pCdDt7hJyPFoMRb0U1T5Wx5uQl4oo6zeQtjKs0MdAXGtvLw1SQ=@protonmail.com' \
--to=zmnscpxj@protonmail$(echo .)com \
--cc=bitcoin-dev@lists$(echo .)linuxfoundation.org \
--cc=lkcl@lkcl$(echo .)net \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox