From 33d729aeb5198d833a0783a18dda8a38b28a2c61 Mon Sep 17 00:00:00 2001 From: Luke Kenneth Casson Leighton Date: Sat, 21 Mar 2020 19:02:18 +0000 Subject: [PATCH] set bigendian=1 in formal proofs of decoder (TODO: bigendian=0) --- src/soc/decoder/formal/proof_decoder.py | 3 ++- src/soc/decoder/formal/proof_decoder2.py | 3 ++- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/src/soc/decoder/formal/proof_decoder.py b/src/soc/decoder/formal/proof_decoder.py index a77b0e86..6aa1bc14 100644 --- 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 190e132d..fa128809 100644 --- 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() -- 2.30.2