Bug 331 - Formal Correctness Proof for LOGICAL pipeline
Summary: Formal Correctness Proof for LOGICAL pipeline
Status: RESOLVED FIXED
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
URL:
Depends on:
Blocks: 195 330
  Show dependency tree / graph
 
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}

Attachments
Add an attachment (proposed patch, testcase, etc.)

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
https://git.libre-soc.org/?p=soc.git;a=blob;f=src/soc/fu/logical/formal/proof_main_stage.py;hb=HEAD

* 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