Bug 331 - Formal Correctness Proof for LOGICAL pipeline
Summary: Formal Correctness Proof for LOGICAL pipeline
Alias: None
Product: Libre-SOC's first SoC
Classification: Unclassified
Component: Formal Verification (show other bugs)
Version: unspecified
Hardware: PC Mac OS
: --- enhancement
Assignee: Luke Kenneth Casson Leighton
Depends on:
Blocks: 195 330
  Show dependency treegraph
Reported: 2020-05-20 16:20 BST by Luke Kenneth Casson Leighton
Modified: 2021-04-20 14:35 BST (History)
1 user (show)

See Also:
NLnet milestone: NLNet.2019.10.032.Formal
total budget (EUR) for completion of task and all subtasks: 400
budget (EUR) for this task, excluding subtasks' budget: 400
parent task for budget allocation: 195
child tasks for budget allocation:
The table of payments (in EUR) for this task; TOML format:
"lkcl"={amount=300, submitted=2020-12-06, paid=2020-12-09} "donated"={amount=100, submitted=2020-08-21, paid=2020-08-21}


Note You need to log in before you can comment on or make changes to this bug.
Description Luke Kenneth Casson Leighton 2020-05-20 16:20:37 BST
a formal correctness proof is needed for the POWER9 Logical pipeline

* OP_XOR       - done
* OP_AND       - done
* OP_OR        - done
* OP_PRTY      - done
* OP_POPCOUNT  - done
* OP_CMPB      - done
* OP_BPERMD    - done - copy taken from proof_bpermd.py (not ideal)
* OP_CNTLZ     - done
* OP_ISEL      - done
* OP_SETB      - done
Comment 2 Luke Kenneth Casson Leighton 2020-05-20 17:28:36 BST
* OP_CNTLZ proof https://git.libre-soc.org/?p=soc.git;a=commitdiff;h=fcc9bc0960283f91288a17eb0eb672ac5fdcc6f0
Comment 3 Luke Kenneth Casson Leighton 2020-05-24 19:21:43 BST
* OP_BPERMD proof https://git.libre-soc.org/?p=soc.git;a=commitdiff;h=2d0d5fb047fb6d88ec24c2cca695332c76d35fc1
Comment 4 Luke Kenneth Casson Leighton 2020-05-24 20:25:15 BST
* OP_CMPB proof https://git.libre-soc.org/?p=soc.git;a=commitdiff;h=f8a96863b7614421c22e1c4b4a336b37bcc79e4c