From: Luke Kenneth Casson Leighton Date: Sat, 18 Jul 2020 10:03:00 +0000 (+0100) Subject: add comment and copy of pseudo-code for OP_RFID into trap proof_main_stage.py X-Git-Tag: semi_working_ecp5~693 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7afe0b03d655baddc54cb2ff4ae64d53714e44fa;p=soc.git add comment and copy of pseudo-code for OP_RFID into trap proof_main_stage.py --- diff --git a/src/soc/fu/trap/formal/proof_main_stage.py b/src/soc/fu/trap/formal/proof_main_stage.py index d4a4ad28..189b2f80 100644 --- a/src/soc/fu/trap/formal/proof_main_stage.py +++ b/src/soc/fu/trap/formal/proof_main_stage.py @@ -86,6 +86,33 @@ class Driver(Elaboratable): # This code is just short of a raw cut-and-paste of the # production code. This should be bit-for-bit identical. # GTKWave waveforms do not appear to be helpful. + """ + + strongly recommend doing exactly what this does which + is from the pseudo-code. + + it then becomes possible to verify that the formal proof + is exactly the same as the pseudo-code by doing simple + side-by-side comparisons, line-by-line + + then if the proof passes we know that the (garbled) + main_stage.py code is "correct" + + MSR[51] <- (MSR[3] & SRR1[51]) | ((¬MSR[3] & MSR[51])) + MSR[3] <- (MSR[3] & SRR1[3]) + if (MSR[29:31] != 0b010) | (SRR1[29:31] != 0b000) then + MSR[29:31] <- SRR1[29:31] + MSR[48] <- SRR1[48] | SRR1[49] + MSR[58] <- SRR1[58] | SRR1[49] + MSR[59] <- SRR1[59] | SRR1[49] + MSR[0:2] <- SRR1[0:2] + MSR[4:28] <- SRR1[4:28] + MSR[32] <- SRR1[32] + MSR[37:41] <- SRR1[37:41] + MSR[49:50] <- SRR1[49:50] + MSR[52:57] <- SRR1[52:57] + MSR[60:63] <- SRR1[60:63] + """ comb += [ desired_msr[0:16].eq(srr1_i[0:16]), desired_msr[22:27].eq(srr1_i[22:27]),