[libre-riscv-dev] [Bug 174] NLNet 2019 Formal Standards proposal 2019-10-046

[bugzilla-daemon at libre-riscv.org]

http://bugs.libre-riscv.org/show_bug.cgi?id=174

--- Comment #3 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
(In reply to Luke Kenneth Casson Leighton from comment #1)
> TODO on here:
> 
> * actual development of standards, these have been partially informally
>   written up and are tagged (ikiwiki) here:
> https://libre-riscv.org/standards/
> * all of the above need to be adopted (sigh) to PowerISA
> * a software simulator needs to be rewritten (probably http://www.m5sim.org)
> * communication with the relevant OpenPower Foundation members needs to be
>   established and our existence and status as a peer contributor "asserted"
>   (if you know what i mean)
> * formal write-up of the (informal) standards needed, followed by
> presentation
>   (and walking through "acceptance" process) with OpenPower Foundation
> * creating a suitable "Formal Correctness Proof" of the augmentations to
>   the standard(s), which is marginally complicated by the fact that IBM /
>   Freescale / NXP as part of the OpenPower Foundation don't *have* a process
>   in place for this... yet.  they know they need one.
> 
> budgets for standards writeup:
> 
> * SimpleV EUR 8000
> * ISAMUX/NS 2500
> * Atomics 2500
> * Variable Encoding 2500
> * Compressed 5000
> * FP16 2500
> * ISA Switch (POWER-RV64GC) 3000
> 
> total EUR 26000
> 
> * openpower simulator: EUR 12000
> * unit tests under simulator: EUR 6000
> * communications budget for OpenPower Member discussion and proposals: EUR
> 6000
> * formal proofs: leave off because it still needs discussion with OpenPower
> Foundation

-- 
You are receiving this mail because:
You are on the CC list for the bug.