From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from hemlock.osuosl.org (smtp2.osuosl.org [140.211.166.133]) by lists.linuxfoundation.org (Postfix) with ESMTP id E29E1C013A for ; Wed, 3 Feb 2021 02:06:56 +0000 (UTC) Received: from localhost (localhost [127.0.0.1]) by hemlock.osuosl.org (Postfix) with ESMTP id CA8C485A46 for ; Wed, 3 Feb 2021 02:06:56 +0000 (UTC) X-Virus-Scanned: amavisd-new at osuosl.org Received: from hemlock.osuosl.org ([127.0.0.1]) by localhost (.osuosl.org [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id 2+-+RGEZ3Zs6 for ; Wed, 3 Feb 2021 02:06:54 +0000 (UTC) X-Greylist: domain auto-whitelisted by SQLgrey-1.7.6 Received: from mail-40140.protonmail.ch (mail-40140.protonmail.ch [185.70.40.140]) by hemlock.osuosl.org (Postfix) with ESMTPS id 58D5E85A25 for ; Wed, 3 Feb 2021 02:06:54 +0000 (UTC) Date: Wed, 03 Feb 2021 02:06:46 +0000 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=protonmail.com; s=protonmail; t=1612318010; bh=g/Eu+q0nJJZtByBrxfmu8k75zbSVkE/0rzEgjSNr8fw=; h=Date:To:From:Reply-To:Subject:In-Reply-To:References:From; b=Ax4JSQLt+DLsGFEWCs1cuOOEq1nmSuHu5Md5h92BVCIhA+2RiIyedRAmNtzfq4MGp 8xAsSNgmvKMehxulauaMJFi0jkfmy4ttwrUxaBHk/y4PHAwVoSmOcFPxPSF+st/s4o lUKZPg98vmdTGVS1kd/ReNMj6sMrqNVAu6UMRcfM= To: Luke Kenneth Casson Leighton , Bitcoin Protocol Discussion From: ZmnSCPxj Reply-To: ZmnSCPxj Message-ID: In-Reply-To: References: 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 X-BeenThere: bitcoin-dev@lists.linuxfoundation.org X-Mailman-Version: 2.1.15 Precedence: list List-Id: Bitcoin Protocol Discussion List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Wed, 03 Feb 2021 02:06:57 -0000 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