diff options
| author | Peter Sewell | 2016-06-03 16:32:34 +0100 |
|---|---|---|
| committer | Peter Sewell | 2016-06-03 16:32:34 +0100 |
| commit | 0650c97b78da4efda0337192ca8fe765e38155ea (patch) | |
| tree | 9b301da1e1b3d2318ee5bf3a78bc78f04c4f3f9c /mips | |
| parent | 426dea43d87e423371095f7a35f4df82c8ad53a3 (diff) | |
| parent | a0447910fc93f98897d41b4ee48ccb888cda3113 (diff) | |
Merge branch 'master' of bitbucket.org:Peter_Sewell/l2
Diffstat (limited to 'mips')
| -rw-r--r-- | mips/mips_prelude.sail | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/mips/mips_prelude.sail b/mips/mips_prelude.sail index 4710167e..5847cecb 100644 --- a/mips/mips_prelude.sail +++ b/mips/mips_prelude.sail @@ -368,8 +368,8 @@ function unit incrementCP0Count() = { (* XXX Sail does not allow reading fields here :-( *) let (bit[32])status = CP0Status in let (bit[32])cause = CP0Cause in - let (bit[8]) ims = (status[15..8]) in - let (bit[8]) ips = (cause[15..8]) in + let (bit[8]) ims = status[15..8] in + let (bit[8]) ips = cause[15..8] in let ie = status[0] in let exl = status[1] in let erl = status[2] in @@ -379,14 +379,14 @@ function unit incrementCP0Count() = { function bool tlbEntryMatch(r, vpn2, asid, (TLBEntry) entry) = let entryVal = (bit[117]) entry in - let entryValid = (entryVal[62]) in - let entryR = (entryVal[100..99]) in - let entryMask = (entryVal[116..101]) in - let entryVPN = (entryVal[98..72]) in - let entryASID = (entryVal[71..64]) in - let entryG = (entryVal[63]) in - ((entryValid) & - (r == (entryR)) & + let entryValid = entryVal[62] in + let entryR = entryVal[100..99] in + let entryMask = entryVal[116..101] in + let entryVPN = entryVal[98..72] in + let entryASID = entryVal[71..64] in + let entryG = entryVal[63] in + (entryValid & + (r == entryR) & ((vpn2 & ~(EXTZ(entryMask))) == ((entryVPN) & ~(EXTZ(entryMask)))) & ((asid == (entryASID)) | (entryG))) |