Bug 406

Summary: Use SAIL's PowerISA formal model to help catch errors
Product: Libre-SOC's first SoC Reporter: Jacob Lifshay <programmerjake>
Component: Formal VerificationAssignee: Luke Kenneth Casson Leighton <lkcl>
Status: CONFIRMED ---    
Severity: enhancement CC: libre-soc-bugs, programmerjake
Priority: ---    
Version: unspecified   
Hardware: Other   
OS: Linux   
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:

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