[libre-riscv-dev] daily kan-ban update 25jun2020

[Luke Kenneth Casson Leighton]

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.

l.



-- 
---
crowd-funded eco-conscious hardware: https://www.crowdsupply.com/eoma68