set bigendian=1 in formal proofs of decoder (TODO: bigendian=0)

[soc.git] / src / soc / decoder / formal / proof_decoder.py

diff --git a/src/soc/decoder/formal/proof_decoder.py b/src/soc/decoder/formal/proof_decoder.py
index a77b0e8681a7aee88bce37a97745422b9cdc3b59..6aa1bc145db5f8f667b7ddffa10777b8830358a5 100644 (file)
--- a/src/soc/decoder/formal/proof_decoder.py
+++ b/src/soc/decoder/formal/proof_decoder.py
@@ -29,7 +29,8 @@ class Driver(Elaboratable):
 
         self.m.submodules.pdecode2 = pdecode2 = PowerDecode2(pdecode)
         dec1 = pdecode2.dec
-        self.comb += pdecode2.dec.opcode_in.eq(self.instruction)
+        self.comb += pdecode2.dec.bigendian.eq(1) # TODO: bigendian=0
+        self.comb += pdecode2.dec.raw_opcode_in.eq(self.instruction)
 
         # ignore special decoding of nop
         self.comb += Assume(self.instruction != 0x60000000)