From b5fd7debb7245ce8ed052733721f7efe20b9899c Mon Sep 17 00:00:00 2001 From: Cesar Strauss Date: Mon, 4 Jan 2021 17:26:35 -0300 Subject: [PATCH] Restart the pattern at partition boundaries --- src/ieee754/part/formal/proof_partition.py | 26 +++++++++++++++++----- 1 file changed, 20 insertions(+), 6 deletions(-) diff --git a/src/ieee754/part/formal/proof_partition.py b/src/ieee754/part/formal/proof_partition.py index 57abe4a3..25fc1ba4 100644 --- a/src/ieee754/part/formal/proof_partition.py +++ b/src/ieee754/part/formal/proof_partition.py @@ -75,8 +75,12 @@ class PartitionedPattern(Elaboratable): start = positions[i] end = positions[i+1] # Propagate from the previous byte, adding one to it - comb += self.output[start:end].eq( - self.output[last_start:last_end] + 1) + with m.If(~gates[i]): + comb += self.output[start:end].eq( + self.output[last_start:last_end] + 1) + with m.Else(): + # Unless it's a partition boundary, if so start again + comb += self.output[start:end].eq(1) last_start = start last_end = end return m @@ -93,10 +97,8 @@ class Driver(Elaboratable): def elaborate(_): m = Module() comb = m.d.comb - sync = m.d.sync width = 64 mwidth = 8 - out = Signal(width) # Setup partition points and gates points = PartitionPoints() gates = Signal(mwidth-1) @@ -106,8 +108,20 @@ class Driver(Elaboratable): # Instantiate the partitioned pattern producer m.submodules.dut = dut = PartitionedPattern(width, points) # Directly check some cases - comb += Assert(dut.output == 0x0807060504030201) - comb += Cover(1) + with m.If(gates == 0): + comb += Assert(dut.output == 0x0807060504030201) + with m.If(gates == 0b1100101): + comb += Assert(dut.output == 0x0101030201020101) + with m.If(gates == 0b0001000): + comb += Assert(dut.output == 0x0403020104030201) + with m.If(gates == 0b0100001): + comb += Assert(dut.output == 0x0201050403020101) + with m.If(gates == 0b1000001): + comb += Assert(dut.output == 0x0106050403020101) + with m.If(gates == 0b0000001): + comb += Assert(dut.output == 0x0706050403020101) + # Make it interesting, by having three partitions + comb += Cover(sum(gates) == 3) return m -- 2.30.2