[libre-riscv-dev] daily kan-ban update 25jun2020
Luke Kenneth Casson Leighton
lkcl at lkcl.net
Fri Jun 26 10:37:10 BST 2020
was also on the virtual coffee call last night, the key aspect i think was
getting through to hugh the strategic importance of formal correctness
proofs, for the whole OpenPOWER community.
boris works on language proofs (c, c++) and fascinatingly uses the same
solvers as symbiyosys. he also is keenly aware that you cannot do a
language proof without a mathematical model of the actual instruction set.
i also yesterday did some work on the PortInterface to
LoadStoreUnitInterface adapter. this is going very slowly.
overall folks progress is at a near standstill.
crowd-funded eco-conscious hardware: https://www.crowdsupply.com/eoma68
More information about the libre-riscv-dev