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

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)

diff --git a/src/soc/decoder/formal/proof_decoder2.py b/src/soc/decoder/formal/proof_decoder2.py
index 190e132d6647d61a9e890c11b974c5bff88943a2..fa128809703862f6739f4c5f6c0299b5f3f243a7 100644 (file)
--- a/src/soc/decoder/formal/proof_decoder2.py
+++ b/src/soc/decoder/formal/proof_decoder2.py
@@ -26,7 +26,8 @@ class Driver(Elaboratable):
         pdecode = create_pdecode()
 
         self.m.submodules.pdecode2 = pdecode2 = PowerDecode2(pdecode)
-        self.comb += pdecode2.dec.opcode_in.eq(self.instruction)
+        self.comb += pdecode2.dec.bigendian.eq(1) # XXX TODO: bigendian=0
+        self.comb += pdecode2.dec.raw_opcode_in.eq(self.instruction)
 
         self.test_in1(pdecode2, pdecode)
         self.test_in2()