Bug 331

Summary: Formal Correctness Proof for LOGICAL pipeline
Product: Libre-SOC's first SoC Reporter: Luke Kenneth Casson Leighton <lkcl>
Component: Formal VerificationAssignee: Luke Kenneth Casson Leighton <lkcl>
Status: RESOLVED FIXED    
Severity: enhancement CC: libre-soc-bugs
Priority: ---    
Version: unspecified   
Hardware: PC   
OS: Mac OS   
See Also: https://bugs.libre-soc.org/show_bug.cgi?id=306
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}
Bug Depends on:    
Bug Blocks: 195, 330    

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