[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 mailing list