Bug 195 - Formal correctness framework is needed for Power ISA
Summary: Formal correctness framework is needed for Power ISA
Status: CONFIRMED
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 418 419 331 332
Blocks: 158
  Show dependency treegraph
 
Reported: 2020-03-02 13:13 GMT by Luke Kenneth Casson Leighton
Modified: 2020-09-06 20:16 BST (History)
2 users (show)

See Also:
NLnet milestone: NLNet.2019.10.Formal
total budget (EUR) for completion of task and all subtasks: 12000
budget (EUR) for this task, excluding subtasks' budget: 8500
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:


Attachments

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/