Bug 406 - Use SAIL's PowerISA formal model to help catch errors
Summary: Use SAIL's PowerISA formal model to help catch errors
Status: CONFIRMED
Alias: None
Product: Libre-SOC's first SoC
Classification: Unclassified
Component: Formal Verification (show other bugs)
Version: unspecified
Hardware: Other Linux
: --- enhancement
Assignee: Luke Kenneth Casson Leighton
URL:
Depends on:
Blocks:
 
Reported: 2020-06-26 01:25 BST by Jacob Lifshay
Modified: 2020-06-26 02:02 BST (History)
2 users (show)

See Also:
NLnet milestone: ---
total budget (EUR) for completion of task and all subtasks: 0
budget (EUR) for this task, excluding subtasks' budget: 0
parent task for budget allocation:
child tasks for budget allocation:
The table of payments (in EUR) for this task; TOML format:

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 Jacob Lifshay 2020-06-26 01:25:22 BST 
Came up during the OpenPower virtual coffee call today.

https://github.com/rems-project/sail/blob/sail2/power/

I found a bug in the SAIL model already:
https://github.com/rems-project/sail/issues/75
Comment 1 Jacob Lifshay 2020-06-26 01:33:25 BST 
One interesting thing I discovered:
SAIL's model for Power is created using basically the same method we are: parsing the pseudo-code in the spec PDF.
Comment 2 Luke Kenneth Casson Leighton 2020-06-26 01:58:07 BST 
(In reply to Jacob Lifshay from comment #1)
> One interesting thing I discovered:
> SAIL's model for Power is created using basically the same method we are:
> parsing the pseudo-code in the spec PDF.

that's quite funny.  that would have saved some time.  oh well.

did you find where they extracted it to?
Comment 3 Jacob Lifshay 2020-06-26 02:02:25 BST 
(In reply to Luke Kenneth Casson Leighton from comment #2)
> (In reply to Jacob Lifshay from comment #1)
> > One interesting thing I discovered:
> > SAIL's model for Power is created using basically the same method we are:
> > parsing the pseudo-code in the spec PDF.
> 
> that's quite funny.  that would have sabed some time.  oh well.
> 
> did you find where they extracted it to?

I'd guess the parser is here: https://github.com/rems-project/extract