+ # Note: going through the spec pseudo-code, line-by-line,
+ # in order, with these assertions. idea is: compare
+ # *directly* against the pseudo-code. therefore, leave
+ # numbering in (from pseudo-code) and add *comments* about
+ # which field it is (3 == HV etc.)
+
+ # spec: MSR[51] <- (MSR[3] & SRR1[51]) | ((¬MSR[3] & MSR[51]))
+ with m.If(field(msr_i, 3)): # HV
+ comb += Assert(field(msr_o, 51) == field(srr1_i, 51)) # ME
+ with m.Else():
+ comb += Assert(field(msr_o, 51) == field(msr_i, 51)) # ME
+