* [libre-riscv-dev] [Bug 331] New: Formal Correctness Proof for LOGICAL pipeline
@ 2020-05-20 15:20 bugzilla-daemon
2020-05-20 15:20 ` [libre-riscv-dev] [Bug 331] " bugzilla-daemon
` (9 more replies)
0 siblings, 10 replies; 11+ messages in thread
From: bugzilla-daemon @ 2020-05-20 15:20 UTC (permalink / raw)
To: libre-riscv-dev
https://bugs.libre-soc.org/show_bug.cgi?id=331
Bug ID: 331
Summary: Formal Correctness Proof for LOGICAL pipeline
Product: Libre-SOC's first SoC
Version: unspecified
Hardware: PC
OS: Mac OS
Status: CONFIRMED
Severity: enhancement
Priority: ---
Component: Formal Verification
Assignee: lkcl@lkcl.net
Reporter: lkcl@lkcl.net
CC: libre-riscv-dev@lists.libre-riscv.org
NLnet milestone: ---
a formal correctness proof is needed for the POWER9 Logical pipeline
--
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev
^ permalink raw reply [flat|nested] 11+ messages in thread
* [libre-riscv-dev] [Bug 331] Formal Correctness Proof for LOGICAL pipeline
2020-05-20 15:20 [libre-riscv-dev] [Bug 331] New: Formal Correctness Proof for LOGICAL pipeline bugzilla-daemon
@ 2020-05-20 15:20 ` " bugzilla-daemon
2020-05-20 15:20 ` bugzilla-daemon
` (8 subsequent siblings)
9 siblings, 0 replies; 11+ messages in thread
From: bugzilla-daemon @ 2020-05-20 15:20 UTC (permalink / raw)
To: libre-riscv-dev
https://bugs.libre-soc.org/show_bug.cgi?id=331
Luke Kenneth Casson Leighton <lkcl@lkcl.net> changed:
What |Removed |Added
----------------------------------------------------------------------------
See Also| |https://bugs.libre-soc.org/
| |show_bug.cgi?id=306
--
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev
^ permalink raw reply [flat|nested] 11+ messages in thread
* [libre-riscv-dev] [Bug 331] Formal Correctness Proof for LOGICAL pipeline
2020-05-20 15:20 [libre-riscv-dev] [Bug 331] New: Formal Correctness Proof for LOGICAL pipeline bugzilla-daemon
2020-05-20 15:20 ` [libre-riscv-dev] [Bug 331] " bugzilla-daemon
@ 2020-05-20 15:20 ` bugzilla-daemon
2020-05-20 15:21 ` bugzilla-daemon
` (7 subsequent siblings)
9 siblings, 0 replies; 11+ messages in thread
From: bugzilla-daemon @ 2020-05-20 15:20 UTC (permalink / raw)
To: libre-riscv-dev
https://bugs.libre-soc.org/show_bug.cgi?id=331
Luke Kenneth Casson Leighton <lkcl@lkcl.net> changed:
What |Removed |Added
----------------------------------------------------------------------------
parent task for| |198
budget allocation| |
NLnet milestone|--- |NLNet.2019.10.Formal
--
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev
^ permalink raw reply [flat|nested] 11+ messages in thread
* [libre-riscv-dev] [Bug 331] Formal Correctness Proof for LOGICAL pipeline
2020-05-20 15:20 [libre-riscv-dev] [Bug 331] New: Formal Correctness Proof for LOGICAL pipeline bugzilla-daemon
2020-05-20 15:20 ` [libre-riscv-dev] [Bug 331] " bugzilla-daemon
2020-05-20 15:20 ` bugzilla-daemon
@ 2020-05-20 15:21 ` bugzilla-daemon
2020-05-20 15:22 ` bugzilla-daemon
` (6 subsequent siblings)
9 siblings, 0 replies; 11+ messages in thread
From: bugzilla-daemon @ 2020-05-20 15:21 UTC (permalink / raw)
To: libre-riscv-dev
https://bugs.libre-soc.org/show_bug.cgi?id=331
Luke Kenneth Casson Leighton <lkcl@lkcl.net> changed:
What |Removed |Added
----------------------------------------------------------------------------
total budget (EUR)|0 |400
for completion of| |
task and all| |
subtasks| |
--
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev
^ permalink raw reply [flat|nested] 11+ messages in thread
* [libre-riscv-dev] [Bug 331] Formal Correctness Proof for LOGICAL pipeline
2020-05-20 15:20 [libre-riscv-dev] [Bug 331] New: Formal Correctness Proof for LOGICAL pipeline bugzilla-daemon
` (2 preceding siblings ...)
2020-05-20 15:21 ` bugzilla-daemon
@ 2020-05-20 15:22 ` bugzilla-daemon
2020-05-20 15:59 ` bugzilla-daemon
` (5 subsequent siblings)
9 siblings, 0 replies; 11+ messages in thread
From: bugzilla-daemon @ 2020-05-20 15:22 UTC (permalink / raw)
To: libre-riscv-dev
https://bugs.libre-soc.org/show_bug.cgi?id=331
--- Comment #1 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
* OP_POPCOUNT proof
https://git.libre-soc.org/?p=soc.git;a=commitdiff;h=0bf0e9b743aac05f25669a0891c638958f01360c
* OP_PARITY proof
https://git.libre-soc.org/?p=soc.git;a=commitdiff;h=8dd3c64cbd6b6112894f990a2cdd6661e79dd9bf
--
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev
^ permalink raw reply [flat|nested] 11+ messages in thread
* [libre-riscv-dev] [Bug 331] Formal Correctness Proof for LOGICAL pipeline
2020-05-20 15:20 [libre-riscv-dev] [Bug 331] New: Formal Correctness Proof for LOGICAL pipeline bugzilla-daemon
` (3 preceding siblings ...)
2020-05-20 15:22 ` bugzilla-daemon
@ 2020-05-20 15:59 ` bugzilla-daemon
2020-05-20 16:28 ` bugzilla-daemon
` (4 subsequent siblings)
9 siblings, 0 replies; 11+ messages in thread
From: bugzilla-daemon @ 2020-05-20 15:59 UTC (permalink / raw)
To: libre-riscv-dev
https://bugs.libre-soc.org/show_bug.cgi?id=331
Michael Nolan <mtnolan2640@gmail.com> changed:
What |Removed |Added
----------------------------------------------------------------------------
Assignee|lkcl@lkcl.net |mtnolan2640@gmail.com
CC| |mtnolan2640@gmail.com
--
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev
^ permalink raw reply [flat|nested] 11+ messages in thread
* [libre-riscv-dev] [Bug 331] Formal Correctness Proof for LOGICAL pipeline
2020-05-20 15:20 [libre-riscv-dev] [Bug 331] New: Formal Correctness Proof for LOGICAL pipeline bugzilla-daemon
` (4 preceding siblings ...)
2020-05-20 15:59 ` bugzilla-daemon
@ 2020-05-20 16:28 ` bugzilla-daemon
2020-05-21 13:01 ` bugzilla-daemon
` (3 subsequent siblings)
9 siblings, 0 replies; 11+ messages in thread
From: bugzilla-daemon @ 2020-05-20 16:28 UTC (permalink / raw)
To: libre-riscv-dev
https://bugs.libre-soc.org/show_bug.cgi?id=331
--- Comment #2 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
* OP_CNTLZ proof
https://git.libre-soc.org/?p=soc.git;a=commitdiff;h=fcc9bc0960283f91288a17eb0eb672ac5fdcc6f0
--
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev
^ permalink raw reply [flat|nested] 11+ messages in thread
* [libre-riscv-dev] [Bug 331] Formal Correctness Proof for LOGICAL pipeline
2020-05-20 15:20 [libre-riscv-dev] [Bug 331] New: Formal Correctness Proof for LOGICAL pipeline bugzilla-daemon
` (5 preceding siblings ...)
2020-05-20 16:28 ` bugzilla-daemon
@ 2020-05-21 13:01 ` bugzilla-daemon
2020-05-24 18:21 ` bugzilla-daemon
` (2 subsequent siblings)
9 siblings, 0 replies; 11+ messages in thread
From: bugzilla-daemon @ 2020-05-21 13:01 UTC (permalink / raw)
To: libre-riscv-dev
https://bugs.libre-soc.org/show_bug.cgi?id=331
Luke Kenneth Casson Leighton <lkcl@lkcl.net> changed:
What |Removed |Added
----------------------------------------------------------------------------
parent task for|198 |195
budget allocation| |
--
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev
^ permalink raw reply [flat|nested] 11+ messages in thread
* [libre-riscv-dev] [Bug 331] Formal Correctness Proof for LOGICAL pipeline
2020-05-20 15:20 [libre-riscv-dev] [Bug 331] New: Formal Correctness Proof for LOGICAL pipeline bugzilla-daemon
` (6 preceding siblings ...)
2020-05-21 13:01 ` bugzilla-daemon
@ 2020-05-24 18:21 ` bugzilla-daemon
2020-05-24 19:25 ` bugzilla-daemon
2020-05-28 15:41 ` bugzilla-daemon
9 siblings, 0 replies; 11+ messages in thread
From: bugzilla-daemon @ 2020-05-24 18:21 UTC (permalink / raw)
To: libre-riscv-dev
https://bugs.libre-soc.org/show_bug.cgi?id=331
--- Comment #3 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
* OP_BPERMD proof
https://git.libre-soc.org/?p=soc.git;a=commitdiff;h=2d0d5fb047fb6d88ec24c2cca695332c76d35fc1
--
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev
^ permalink raw reply [flat|nested] 11+ messages in thread
* [libre-riscv-dev] [Bug 331] Formal Correctness Proof for LOGICAL pipeline
2020-05-20 15:20 [libre-riscv-dev] [Bug 331] New: Formal Correctness Proof for LOGICAL pipeline bugzilla-daemon
` (7 preceding siblings ...)
2020-05-24 18:21 ` bugzilla-daemon
@ 2020-05-24 19:25 ` bugzilla-daemon
2020-05-28 15:41 ` bugzilla-daemon
9 siblings, 0 replies; 11+ messages in thread
From: bugzilla-daemon @ 2020-05-24 19:25 UTC (permalink / raw)
To: libre-riscv-dev
https://bugs.libre-soc.org/show_bug.cgi?id=331
--- Comment #4 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
* OP_CMPB proof
https://git.libre-soc.org/?p=soc.git;a=commitdiff;h=f8a96863b7614421c22e1c4b4a336b37bcc79e4c
--
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev
^ permalink raw reply [flat|nested] 11+ messages in thread
* [libre-riscv-dev] [Bug 331] Formal Correctness Proof for LOGICAL pipeline
2020-05-20 15:20 [libre-riscv-dev] [Bug 331] New: Formal Correctness Proof for LOGICAL pipeline bugzilla-daemon
` (8 preceding siblings ...)
2020-05-24 19:25 ` bugzilla-daemon
@ 2020-05-28 15:41 ` bugzilla-daemon
9 siblings, 0 replies; 11+ messages in thread
From: bugzilla-daemon @ 2020-05-28 15:41 UTC (permalink / raw)
To: libre-riscv-dev
https://bugs.libre-soc.org/show_bug.cgi?id=331
--- Comment #5 from Michael Nolan <mtnolan2640@gmail.com> ---
OP_SETB proof -
https://git.libre-soc.org/?p=soc.git;a=commitdiff;h=6b9d6a743b69bb9370ef1ed06cd89d10114edcf4
OP_ISEL proof -
https://git.libre-soc.org/?p=soc.git;a=commitdiff;h=27440addbb83c3c13949246b495b8c474b1c2c90
--
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev
^ permalink raw reply [flat|nested] 11+ messages in thread
end of thread, back to index
Thread overview: 11+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2020-05-20 15:20 [libre-riscv-dev] [Bug 331] New: Formal Correctness Proof for LOGICAL pipeline bugzilla-daemon
2020-05-20 15:20 ` [libre-riscv-dev] [Bug 331] " bugzilla-daemon
2020-05-20 15:20 ` bugzilla-daemon
2020-05-20 15:21 ` bugzilla-daemon
2020-05-20 15:22 ` bugzilla-daemon
2020-05-20 15:59 ` bugzilla-daemon
2020-05-20 16:28 ` bugzilla-daemon
2020-05-21 13:01 ` bugzilla-daemon
2020-05-24 18:21 ` bugzilla-daemon
2020-05-24 19:25 ` bugzilla-daemon
2020-05-28 15:41 ` bugzilla-daemon
Libre RISC-V Mailing list Archives (accessible via public-inbox)
Archives are clonable: git clone --mirror https://inbox.libre-soc.org/libre-riscv-dev
Example config snippet for mirrors
AGPL code for this site: git clone https://public-inbox.org/public-inbox.git