Bug 195 - Formal correctness framework is needed for Power ISA
Summary: Formal correctness framework is needed for Power ISA
Status: RESOLVED FIXED
Alias: None
Product: Libre-SOC's first SoC
Classification: Unclassified
Component: Formal Verification (show other bugs)
Version: unspecified
Hardware: PC Linux
: --- enhancement
Assignee: Luke Kenneth Casson Leighton
URL:
Depends on: 211 306 331 332 418 419
Blocks: 158
  Show dependency tree / graph
 
Reported: 2020-03-02 13:13 GMT by Luke Kenneth Casson Leighton
Modified: 2022-07-04 17:17 BST (History)
2 users (show)

See Also:
NLnet milestone: NLNet.2019.10.032.Formal
total budget (EUR) for completion of task and all subtasks: 12000
budget (EUR) for this task, excluding subtasks' budget: 6550
parent task for budget allocation: 158
child tasks for budget allocation: 306 331 332 335 340 418 419 421
The table of payments (in EUR) for this task; TOML format:
red={amount=6550, submitted=2022-07-04}

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-03-02 13:13:25 GMT 
A general-purpose Formal correctness test suite is needed for
Power ISA, similar in characteristics to bug #194.  A good
first processor to try testing is Microwatt:
https://github.com/antonblanchard/microwatt/
Comment 1 Luke Kenneth Casson Leighton 2022-07-04 17:17:25 BST 
The Power ISA pipelines are done: ALU, Logical, CR, Branch, Shift, SPR,
Mul, Trap - this can be considered completed.