From: Luke Kenneth Casson Leighton Date: Sat, 21 Mar 2020 19:02:18 +0000 (+0000) Subject: set bigendian=1 in formal proofs of decoder (TODO: bigendian=0) X-Git-Tag: div_pipeline~1657 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=33d729aeb5198d833a0783a18dda8a38b28a2c61;p=soc.git 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 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()