import os
import unittest
+import operator
-from nmigen import Elaboratable, Signal, Module, Const
+from nmigen import Elaboratable, Signal, Module, Const, Repl
from nmigen.asserts import Assert, Cover
from nmigen.hdl.ast import Assume
from nmutil.gtkw import write_gtkw
from ieee754.part_mul_add.partpoints import PartitionPoints
+from ieee754.part.partsig import PartitionedSignal
class PartitionedPattern(Elaboratable):
return m
+def make_partitions(step, mwidth):
+ """Make equally spaced partition points
+
+ :param step: smallest partition width
+ :param mwidth: maximum number of partitions
+ :returns: partition points, and corresponding gates"""
+ gates = Signal(mwidth - 1)
+ points = PartitionPoints()
+ for i in range(mwidth-1):
+ points[(i + 1) * step] = gates[i]
+ return points, gates
+
+
# This defines a module to drive the device under test and assert
# properties about its outputs
class Driver(Elaboratable):
width = 64
mwidth = 8
# Setup partition points and gates
- points = PartitionPoints()
- gates = Signal(mwidth-1)
step = int(width/mwidth)
- for i in range(mwidth-1):
- points[(i+1)*step] = gates[i]
+ points, gates = make_partitions(step, mwidth)
# Instantiate the partitioned pattern producer
m.submodules.dut = dut = PartitionedPattern(width, points)
# Directly check some cases
# Output an example.
# Make it interesting, by having four partitions.
# Make the selected partition not start at the very beginning.
- comb += Cover((sum(gates) == 3) & (p_offset != 0))
+ comb += Cover((sum(gates) == 3) & (p_offset != 0) & (p_width == 3))
+ # Generate and check expected values for all possible partition sizes.
+ # Here, we assume partition sizes are multiple of the smaller size.
+ for w in range(1, mwidth+1):
+ with m.If(p_width == w):
+ # calculate the expected output, for the given bit width
+ bit_width = w * step
+ expected = Signal(bit_width, name=f"expected_{w}")
+ for b in range(w):
+ # lower nibble is the position
+ comb += expected[b*8:b*8+4].eq(b+1)
+ # upper nibble is the partition width
+ comb += expected[b*8+4:b*8+8].eq(w)
+ # truncate the output, compare and assert
+ comb += Assert(p_output[:bit_width] == expected)
+ return m
+
+
+class GateGenerator(Elaboratable):
+ """Produces partition gates at random
+
+ `p_offset`, `p_width` and `p_finish` describe the selected partition
+ """
+ def __init__(self, mwidth):
+ self.mwidth = mwidth
+ """Number of partitions"""
+ self.gates = Signal(mwidth-1)
+ """Generated partition gates"""
+ self.p_offset = Signal(range(mwidth))
+ """Generated partition start point"""
+ self.p_width = Signal(range(mwidth+1))
+ """Generated partition width"""
+ self.p_finish = Signal(range(mwidth+1))
+ """Generated partition end point"""
+
+ def elaborate(self, _):
+ m = Module()
+ comb = m.d.comb
+ mwidth = self.mwidth
+ gates = self.gates
+ p_offset = self.p_offset
+ p_width = self.p_width
+ p_finish = self.p_finish
+ comb += p_finish.eq(p_offset + p_width)
+ # Partition must not be empty, and fit within the signal.
+ comb += Assume(p_width != 0)
+ comb += Assume(p_offset + p_width <= mwidth)
+
+ # Build the corresponding partition
+ # Use Assume to constraint the pattern to conform to the given offset
+ # and width. For each gate bit it is:
+ # 1) one, if on the partition boundary
+ # 2) zero, if it's inside the partition
+ # 3) don't care, otherwise
+ p_gates = Signal(mwidth+1)
+ for i in range(mwidth+1):
+ with m.If(i == p_offset):
+ # Partitions begin with 1
+ comb += Assume(p_gates[i] == 1)
+ with m.If((i > p_offset) & (i < p_finish)):
+ # The interior are all zeros
+ comb += Assume(p_gates[i] == 0)
+ with m.If(i == p_finish):
+ # End with 1 again
+ comb += Assume(p_gates[i] == 1)
+ # Remove guard bits at each end, before assigning to the output gates
+ comb += gates.eq(p_gates[1:])
+ return m
+
+
+class GeneratorDriver(Elaboratable):
+ def __init__(self):
+ # inputs and outputs
+ pass
+
+ @staticmethod
+ def elaborate(_):
+ m = Module()
+ comb = m.d.comb
+ width = 64
+ mwidth = 8
+ # Setup partition points and gates
+ step = int(width/mwidth)
+ points, gates = make_partitions(step, mwidth)
+ # Instantiate the partitioned pattern producer and the DUT
+ m.submodules.dut = dut = PartitionedPattern(width, points)
+ m.submodules.gen = gen = GateGenerator(mwidth)
+ comb += gates.eq(gen.gates)
+ # Generate shifted down outputs
+ p_offset = gen.p_offset
+ p_width = gen.p_width
+ p_output = Signal(width)
+ for i in range(mwidth):
+ with m.If(p_offset == i):
+ comb += p_output.eq(dut.output[i*step:])
+ # Generate and check expected values for all possible partition sizes.
+ for w in range(1, mwidth+1):
+ with m.If(p_width == w):
+ # calculate the expected output, for the given bit width
+ bit_width = w * step
+ expected = Signal(bit_width, name=f"expected_{w}")
+ for b in range(w):
+ # lower nibble is the position
+ comb += expected[b*8:b*8+4].eq(b+1)
+ # upper nibble is the partition width
+ comb += expected[b*8+4:b*8+8].eq(w)
+ # truncate the output, compare and assert
+ comb += Assert(p_output[:bit_width] == expected)
+ # Output an example.
+ # Make it interesting, by having four partitions.
+ # Make the selected partition not start at the very beginning.
+ comb += Cover((sum(gates) == 3) & (p_offset != 0) & (p_width == 3))
+ return m
+
+
+class ComparisonOpDriver(Elaboratable):
+ """Checks comparison operations on partitioned signals"""
+ def __init__(self, op, width=64, mwidth=8, nops=2):
+ self.op = op
+ """Operation to perform. Must accept two integer-like inputs and give
+ a predicate-like output (1-bit partitions in case of
+ PartitionedSignal types)"""
+ self.width = width
+ """Partition full width"""
+ self.mwidth = mwidth
+ """Maximum number of equally sized partitions"""
+ self.nops = nops
+ """Number of input operands"""
+ def elaborate(self, _):
+ m = Module()
+ comb = m.d.comb
+ width = self.width
+ mwidth = self.mwidth
+ nops = self.nops
+ # setup partition points and gates
+ step = int(width/mwidth)
+ points, gates = make_partitions(step, mwidth)
+ # setup inputs and outputs
+ operands = list()
+ for i in range(nops):
+ inp = PartitionedSignal(points, width, name=f"i_{i+1}")
+ inp.set_module(m)
+ operands.append(inp)
+ output = Signal(mwidth)
+ # perform the operation on the partitioned signals
+ comb += output.eq(self.op(*operands))
+ # instantiate the partitioned gate generator and connect the gates
+ m.submodules.gen = gen = GateGenerator(mwidth)
+ comb += gates.eq(gen.gates)
+ p_offset = gen.p_offset
+ p_width = gen.p_width
+ # generate shifted down inputs and outputs
+ p_operands = list()
+ for i in range(nops):
+ p_i = Signal(width, name=f"p_{i+1}")
+ p_operands.append(p_i)
+ for pos in range(mwidth):
+ with m.If(p_offset == pos):
+ comb += p_i.eq(operands[i].sig[pos * step:])
+ p_output = Signal(mwidth)
+ for pos in range(mwidth):
+ with m.If(p_offset == pos):
+ comb += p_output.eq(output[pos:])
+ # generate and check expected values for all possible partition sizes
+ for w in range(1, mwidth+1):
+ with m.If(p_width == w):
+ # calculate the expected output, for the given bit width,
+ # truncating the inputs to the partition size
+ input_bit_width = w * step
+ output_bit_width = w
+ expected = Signal(output_bit_width, name=f"expected_{w}")
+ trunc_operands = list()
+ for i in range(nops):
+ t_i = Signal(input_bit_width, name=f"t{w}_{i+1}")
+ trunc_operands.append(t_i)
+ comb += t_i.eq(p_operands[i][:input_bit_width])
+ lsb = Signal(name=f"lsb_{w}")
+ comb += lsb.eq(self.op(*trunc_operands))
+ comb += expected.eq(Repl(lsb, output_bit_width))
+ # truncate the output, compare and assert
+ comb += Assert(p_output[:output_bit_width] == expected)
+ # output a test case
+ comb += Cover((p_offset != 0) & (p_width == 3) & (sum(output) > 1) &
+ (p_output != 0))
return m
class PartitionTestCase(FHDLTestCase):
def test_formal(self):
+ style = {
+ 'dec': {'base': 'dec'},
+ 'bin': {'base': 'bin'}
+ }
traces = [
+ ('p_offset[2:0]', 'dec'),
+ ('p_width[3:0]', 'dec'),
+ ('p_finish[3:0]', 'dec'),
+ ('p_gates[8:0]', 'bin'),
('dut', {'submodule': 'dut'}, [
- 'output[63:0]',
- ('gates[6:0]', {'base': 'bin'})]),
- ('p_offset[2:0]', {'base': 'dec'}),
- ('p_width[3:0]', {'base': 'dec'}),
- ('p_finish[3:0]', {'base': 'dec'}),
- ('p_gates[8:0]', {'base': 'bin'}),
- 'p_output[63:0]']
+ ('gates[6:0]', 'bin'),
+ 'output[63:0]']),
+ 'p_output[63:0]', 'expected_3[21:0]']
write_gtkw(
'proof_partition_cover.gtkw',
os.path.dirname(__file__) +
'/proof_partition_formal/engine_0/trace0.vcd',
- traces,
+ traces, style,
module='top',
zoom=-3
)
'proof_partition_bmc.gtkw',
os.path.dirname(__file__) +
'/proof_partition_formal/engine_0/trace.vcd',
- traces,
+ traces, style,
module='top',
zoom=-3
)
self.assertFormal(module, mode="bmc", depth=1)
self.assertFormal(module, mode="cover", depth=1)
+ def test_generator(self):
+ style = {
+ 'dec': {'base': 'dec'},
+ 'bin': {'base': 'bin'}
+ }
+ traces = [
+ ('p_offset[2:0]', 'dec'),
+ ('p_width[3:0]', 'dec'),
+ ('p_finish[3:0]', 'dec'),
+ ('p_gates[8:0]', 'bin'),
+ ('dut', {'submodule': 'dut'}, [
+ ('gates[6:0]', 'bin'),
+ 'output[63:0]']),
+ 'p_output[63:0]', 'expected_3[21:0]',
+ 'a_3[23:0]', 'b_3[32:0]', 'expected_3[2:0]']
+ write_gtkw(
+ 'proof_partition_generator_cover.gtkw',
+ os.path.dirname(__file__) +
+ '/proof_partition_generator/engine_0/trace0.vcd',
+ traces, style,
+ module='top',
+ zoom=-3
+ )
+ write_gtkw(
+ 'proof_partition_generator_bmc.gtkw',
+ os.path.dirname(__file__) +
+ '/proof_partition_generator/engine_0/trace.vcd',
+ traces, style,
+ module='top',
+ zoom=-3
+ )
+ module = GeneratorDriver()
+ self.assertFormal(module, mode="bmc", depth=1)
+ self.assertFormal(module, mode="cover", depth=1)
+
+ def test_partsig_eq(self):
+ style = {
+ 'dec': {'base': 'dec'},
+ 'bin': {'base': 'bin'}
+ }
+ traces = [
+ ('p_offset[2:0]', 'dec'),
+ ('p_width[3:0]', 'dec'),
+ ('p_gates[8:0]', 'bin'),
+ 'i_1[63:0]', 'i_2[63:0]',
+ ('eq_1', {'submodule': 'eq_1'}, [
+ ('gates[6:0]', 'bin'),
+ 'a[63:0]', 'b[63:0]',
+ ('output[7:0]', 'bin')]),
+ 'p_1[63:0]', 'p_2[63:0]',
+ ('p_output[7:0]', 'bin'),
+ 't3_1[23:0]', 't3_2[23:0]', 'lsb_3',
+ ('expected_3[2:0]', 'bin')]
+ write_gtkw(
+ 'proof_partsig_eq_cover.gtkw',
+ os.path.dirname(__file__) +
+ '/proof_partition_partsig_eq/engine_0/trace0.vcd',
+ traces, style,
+ module='top',
+ zoom=-3
+ )
+ write_gtkw(
+ 'proof_partsig_eq_bmc.gtkw',
+ os.path.dirname(__file__) +
+ '/proof_partition_partsig_eq/engine_0/trace.vcd',
+ traces, style,
+ module='top',
+ zoom=-3
+ )
+ module = ComparisonOpDriver(operator.eq)
+ self.assertFormal(module, mode="bmc", depth=1)
+ self.assertFormal(module, mode="cover", depth=1)
+
+ def test_partsig_ne(self):
+ module = ComparisonOpDriver(operator.ne)
+ self.assertFormal(module, mode="bmc", depth=1)
+
+ def test_partsig_gt(self):
+ module = ComparisonOpDriver(operator.gt)
+ self.assertFormal(module, mode="bmc", depth=1)
+
+ def test_partsig_ge(self):
+ module = ComparisonOpDriver(operator.ge)
+ self.assertFormal(module, mode="bmc", depth=1)
+
+ def test_partsig_lt(self):
+ module = ComparisonOpDriver(operator.lt)
+ self.assertFormal(module, mode="bmc", depth=1)
+
+ def test_partsig_le(self):
+ module = ComparisonOpDriver(operator.le)
+ self.assertFormal(module, mode="bmc", depth=1)
+
+ def test_partsig_all(self):
+ style = {
+ 'dec': {'base': 'dec'},
+ 'bin': {'base': 'bin'}
+ }
+ traces = [
+ ('p_offset[2:0]', 'dec'),
+ ('p_width[3:0]', 'dec'),
+ ('p_gates[8:0]', 'bin'),
+ 'i_1[63:0]',
+ ('eq_1', {'submodule': 'eq_1'}, [
+ ('gates[6:0]', 'bin'),
+ 'a[63:0]', 'b[63:0]',
+ ('output[7:0]', 'bin')]),
+ 'p_1[63:0]',
+ ('p_output[7:0]', 'bin'),
+ 't3_1[23:0]', 'lsb_3',
+ ('expected_3[2:0]', 'bin')]
+ write_gtkw(
+ 'proof_partsig_all_cover.gtkw',
+ os.path.dirname(__file__) +
+ '/proof_partition_partsig_all/engine_0/trace0.vcd',
+ traces, style,
+ module='top',
+ zoom=-3
+ )
+
+ def op_all(obj):
+ return obj.all()
+
+ module = ComparisonOpDriver(op_all, nops=1)
+ self.assertFormal(module, mode="bmc", depth=1)
+ self.assertFormal(module, mode="cover", depth=1)
+
if __name__ == '__main__':
unittest.main()
projects / ieee754fpu.git / blobdiff