src/ieee754/part/formal/proof_partition.py

   1 """Formal verification of partitioned operations
   2
   3 The approach is to take an arbitrary partition, by choosing its start point
   4 and size at random. Use ``Assume`` to ensure it is a whole unbroken partition
   5 (start and end points are one, with only zeros in between). Shift inputs and
   6 outputs down to zero. Loop over all possible partition sizes and, if it's the
   7 right size, compute the expected value, compare with the result, and assert.
   8
   9 We are turning the for-loops around (on their head), such that we start from
  10 the *lengths* (and positions) and perform the ``Assume`` on the resultant
  11 partition bits.
  12
  13 In other words, we have patterns as follows (assuming 32-bit words)::
  14
  15   8-bit offsets 0,1,2,3
  16   16-bit offsets 0,1,2
  17   24-bit offsets 0,1
  18   32-bit
  19
  20 * for 8-bit the partition bit is 1 and the previous is also 1
  21
  22 * for 16-bit the partition bit at the offset must be 0 and be surrounded by 1
  23
  24 * for 24-bit the partition bits at the offset and at offset+1 must be 0 and at
  25   offset+2 and offset-1 must be 1
  26
  27 * for 32-bit all 3 bits must be 0 and be surrounded by 1 (guard bits are added
  28   at each end for this purpose)
  29
  30 """
  31
  32 import os
  33 import unittest
  34 import operator
  35
  36 from nmigen import Elaboratable, Signal, Module, Const, Repl
  37 from nmigen.asserts import Assert, Cover
  38 from nmigen.hdl.ast import Assume
  39
  40 from nmutil.formaltest import FHDLTestCase
  41 from nmutil.gtkw import write_gtkw
  42
  43 from ieee754.part_mul_add.partpoints import PartitionPoints
  44 from ieee754.part.partsig import PartitionedSignal
  45
  46
  47 class PartitionedPattern(Elaboratable):
  48     """ Generate a unique pattern, depending on partition size.
  49
  50     * 1-byte partitions: 0x11
  51     * 2-byte partitions: 0x21 0x22
  52     * 3-byte partitions: 0x31 0x32 0x33
  53
  54     And so on.
  55
  56     Useful as a test vector for testing the formal prover
  57
  58     """
  59     def __init__(self, width, partition_points):
  60         self.width = width
  61         self.partition_points = PartitionPoints(partition_points)
  62         self.mwidth = len(self.partition_points)+1
  63         self.output = Signal(self.width, reset_less=True)
  64
  65     def elaborate(self, platform):
  66         m = Module()
  67         comb = m.d.comb
  68
  69         # Add a guard bit at each end
  70         positions = [0] + list(self.partition_points.keys()) + [self.width]
  71         gates = [Const(1)] + list(self.partition_points.values()) + [Const(1)]
  72         # Begin counting at one
  73         last_start = positions[0]
  74         last_end = positions[1]
  75         last_middle = (last_start+last_end)//2
  76         comb += self.output[last_start:last_middle].eq(1)
  77         # Build an incrementing cascade
  78         for i in range(1, self.mwidth):
  79             start = positions[i]
  80             end = positions[i+1]
  81             middle = (start + end) // 2
  82             # Propagate from the previous byte, adding one to it.
  83             with m.If(~gates[i]):
  84                 comb += self.output[start:middle].eq(
  85                     self.output[last_start:last_middle] + 1)
  86             with m.Else():
  87                 # ... unless it's a partition boundary. If so, start again.
  88                 comb += self.output[start:middle].eq(1)
  89             last_start = start
  90             last_middle = middle
  91         # Mirror the nibbles on the last byte
  92         last_start = positions[-2]
  93         last_end = positions[-1]
  94         last_middle = (last_start+last_end)//2
  95         comb += self.output[last_middle:last_end].eq(
  96             self.output[last_start:last_middle])
  97         for i in range(self.mwidth, 0, -1):
  98             start = positions[i-1]
  99             end = positions[i]
 100             middle = (start + end) // 2
 101             # Propagate from the previous byte.
 102             with m.If(~gates[i]):
 103                 comb += self.output[middle:end].eq(
 104                     self.output[last_middle:last_end])
 105             with m.Else():
 106                 # ... unless it's a partition boundary.
 107                 # If so, mirror the nibbles again.
 108                 comb += self.output[middle:end].eq(
 109                     self.output[start:middle])
 110             last_middle = middle
 111             last_end = end
 112
 113         return m
 114
 115
 116 def make_partitions(step, mwidth):
 117     """Make equally spaced partition points
 118
 119     :param step: smallest partition width
 120     :param mwidth: maximum number of partitions
 121     :returns: partition points, and corresponding gates"""
 122     gates = Signal(mwidth - 1)
 123     points = PartitionPoints()
 124     for i in range(mwidth-1):
 125         points[(i + 1) * step] = gates[i]
 126     return points, gates
 127
 128
 129 # This defines a module to drive the device under test and assert
 130 # properties about its outputs
 131 class Driver(Elaboratable):
 132     def __init__(self):
 133         # inputs and outputs
 134         pass
 135
 136     @staticmethod
 137     def elaborate(_):
 138         m = Module()
 139         comb = m.d.comb
 140         width = 64
 141         mwidth = 8
 142         # Setup partition points and gates
 143         step = int(width/mwidth)
 144         points, gates = make_partitions(step, mwidth)
 145         # Instantiate the partitioned pattern producer
 146         m.submodules.dut = dut = PartitionedPattern(width, points)
 147         # Directly check some cases
 148         with m.If(gates == 0):
 149             comb += Assert(dut.output == 0x_88_87_86_85_84_83_82_81)
 150         with m.If(gates == 0b1100101):
 151             comb += Assert(dut.output == 0x_11_11_33_32_31_22_21_11)
 152         with m.If(gates == 0b0001000):
 153             comb += Assert(dut.output == 0x_44_43_42_41_44_43_42_41)
 154         with m.If(gates == 0b0100001):
 155             comb += Assert(dut.output == 0x_22_21_55_54_53_52_51_11)
 156         with m.If(gates == 0b1000001):
 157             comb += Assert(dut.output == 0x_11_66_65_64_63_62_61_11)
 158         with m.If(gates == 0b0000001):
 159             comb += Assert(dut.output == 0x_77_76_75_74_73_72_71_11)
 160         # Choose a partition offset and width at random.
 161         p_offset = Signal(range(mwidth))
 162         p_width = Signal(range(mwidth+1))
 163         p_finish = Signal(range(mwidth+1))
 164         comb += p_finish.eq(p_offset + p_width)
 165         # Partition must not be empty, and fit within the signal.
 166         comb += Assume(p_width != 0)
 167         comb += Assume(p_offset + p_width <= mwidth)
 168
 169         # Build the corresponding partition
 170         # Use Assume to constraint the pattern to conform to the given offset
 171         # and width. For each gate bit it is:
 172         # 1) one, if on the partition boundary
 173         # 2) zero, if it's inside the partition
 174         # 3) don't care, otherwise
 175         p_gates = Signal(mwidth+1)
 176         for i in range(mwidth+1):
 177             with m.If(i == p_offset):
 178                 # Partitions begin with 1
 179                 comb += Assume(p_gates[i] == 1)
 180             with m.If((i > p_offset) & (i < p_finish)):
 181                 # The interior are all zeros
 182                 comb += Assume(p_gates[i] == 0)
 183             with m.If(i == p_finish):
 184                 # End with 1 again
 185                 comb += Assume(p_gates[i] == 1)
 186         # Check some possible partitions generating a given pattern
 187         with m.If(p_gates == 0b0100110):
 188             comb += Assert(((p_offset == 1) & (p_width == 1)) |
 189                            ((p_offset == 2) & (p_width == 3)))
 190         # Remove guard bits at each end and assign to the DUT gates
 191         comb += gates.eq(p_gates[1:])
 192         # Generate shifted down outputs:
 193         p_output = Signal(width)
 194         positions = [0] + list(points.keys()) + [width]
 195         for i in range(mwidth):
 196             with m.If(p_offset == i):
 197                 comb += p_output.eq(dut.output[positions[i]:])
 198         # Some checks on the shifted down output, irrespective of offset:
 199         with m.If(p_width == 2):
 200             comb += Assert(p_output[:16] == 0x_22_21)
 201         with m.If(p_width == 4):
 202             comb += Assert(p_output[:32] == 0x_44_43_42_41)
 203         # test zero shift
 204         with m.If(p_offset == 0):
 205             comb += Assert(p_output == dut.output)
 206         # Output an example.
 207         # Make it interesting, by having four partitions.
 208         # Make the selected partition not start at the very beginning.
 209         comb += Cover((sum(gates) == 3) & (p_offset != 0) & (p_width == 3))
 210         # Generate and check expected values for all possible partition sizes.
 211         # Here, we assume partition sizes are multiple of the smaller size.
 212         for w in range(1, mwidth+1):
 213             with m.If(p_width == w):
 214                 # calculate the expected output, for the given bit width
 215                 bit_width = w * step
 216                 expected = Signal(bit_width, name=f"expected_{w}")
 217                 for b in range(w):
 218                     # lower nibble is the position
 219                     comb += expected[b*8:b*8+4].eq(b+1)
 220                     # upper nibble is the partition width
 221                     comb += expected[b*8+4:b*8+8].eq(w)
 222                 # truncate the output, compare and assert
 223                 comb += Assert(p_output[:bit_width] == expected)
 224         return m
 225
 226
 227 class GateGenerator(Elaboratable):
 228     """Produces partition gates at random
 229
 230     `p_offset`, `p_width` and `p_finish` describe the selected partition
 231     """
 232     def __init__(self, mwidth):
 233         self.mwidth = mwidth
 234         """Number of partitions"""
 235         self.gates = Signal(mwidth-1)
 236         """Generated partition gates"""
 237         self.p_offset = Signal(range(mwidth))
 238         """Generated partition start point"""
 239         self.p_width = Signal(range(mwidth+1))
 240         """Generated partition width"""
 241         self.p_finish = Signal(range(mwidth+1))
 242         """Generated partition end point"""
 243
 244     def elaborate(self, _):
 245         m = Module()
 246         comb = m.d.comb
 247         mwidth = self.mwidth
 248         gates = self.gates
 249         p_offset = self.p_offset
 250         p_width = self.p_width
 251         p_finish = self.p_finish
 252         comb += p_finish.eq(p_offset + p_width)
 253         # Partition must not be empty, and fit within the signal.
 254         comb += Assume(p_width != 0)
 255         comb += Assume(p_offset + p_width <= mwidth)
 256
 257         # Build the corresponding partition
 258         # Use Assume to constraint the pattern to conform to the given offset
 259         # and width. For each gate bit it is:
 260         # 1) one, if on the partition boundary
 261         # 2) zero, if it's inside the partition
 262         # 3) don't care, otherwise
 263         p_gates = Signal(mwidth+1)
 264         for i in range(mwidth+1):
 265             with m.If(i == p_offset):
 266                 # Partitions begin with 1
 267                 comb += Assume(p_gates[i] == 1)
 268             with m.If((i > p_offset) & (i < p_finish)):
 269                 # The interior are all zeros
 270                 comb += Assume(p_gates[i] == 0)
 271             with m.If(i == p_finish):
 272                 # End with 1 again
 273                 comb += Assume(p_gates[i] == 1)
 274         # Remove guard bits at each end, before assigning to the output gates
 275         comb += gates.eq(p_gates[1:])
 276         return m
 277
 278
 279 class GeneratorDriver(Elaboratable):
 280     def __init__(self):
 281         # inputs and outputs
 282         pass
 283
 284     @staticmethod
 285     def elaborate(_):
 286         m = Module()
 287         comb = m.d.comb
 288         width = 64
 289         mwidth = 8
 290         # Setup partition points and gates
 291         step = int(width/mwidth)
 292         points, gates = make_partitions(step, mwidth)
 293         # Instantiate the partitioned pattern producer and the DUT
 294         m.submodules.dut = dut = PartitionedPattern(width, points)
 295         m.submodules.gen = gen = GateGenerator(mwidth)
 296         comb += gates.eq(gen.gates)
 297         # Generate shifted down outputs
 298         p_offset = gen.p_offset
 299         p_width = gen.p_width
 300         p_output = Signal(width)
 301         for i in range(mwidth):
 302             with m.If(p_offset == i):
 303                 comb += p_output.eq(dut.output[i*step:])
 304         # Generate and check expected values for all possible partition sizes.
 305         for w in range(1, mwidth+1):
 306             with m.If(p_width == w):
 307                 # calculate the expected output, for the given bit width
 308                 bit_width = w * step
 309                 expected = Signal(bit_width, name=f"expected_{w}")
 310                 for b in range(w):
 311                     # lower nibble is the position
 312                     comb += expected[b*8:b*8+4].eq(b+1)
 313                     # upper nibble is the partition width
 314                     comb += expected[b*8+4:b*8+8].eq(w)
 315                 # truncate the output, compare and assert
 316                 comb += Assert(p_output[:bit_width] == expected)
 317         # Output an example.
 318         # Make it interesting, by having four partitions.
 319         # Make the selected partition not start at the very beginning.
 320         comb += Cover((sum(gates) == 3) & (p_offset != 0) & (p_width == 3))
 321         return m
 322
 323
 324 class OpDriver(Elaboratable):
 325     """Checks operations on partitioned signals"""
 326     def __init__(self, op, width=64, mwidth=8, nops=2, part_out=True):
 327         self.op = op
 328         """Operation to perform"""
 329         self.width = width
 330         """Partition full width"""
 331         self.mwidth = mwidth
 332         """Maximum number of equally sized partitions"""
 333         self.nops = nops
 334         """Number of input operands"""
 335         self.part_out = part_out
 336         """True if output is partition-like"""
 337     def elaborate(self, _):
 338         m = Module()
 339         comb = m.d.comb
 340         width = self.width
 341         mwidth = self.mwidth
 342         nops = self.nops
 343         part_out = self.part_out
 344         # setup partition points and gates
 345         step = int(width/mwidth)
 346         points, gates = make_partitions(step, mwidth)
 347         # setup inputs and outputs
 348         operands = list()
 349         for i in range(nops):
 350             inp = PartitionedSignal(points, width, name=f"i_{i+1}")
 351             inp.set_module(m)
 352             operands.append(inp)
 353         if part_out:
 354             out_width = mwidth
 355             out_step = 1
 356         else:
 357             out_width = width
 358             out_step = step
 359         output = Signal(out_width)
 360         # perform the operation on the partitioned signals
 361         comb += output.eq(self.op(*operands))
 362         # instantiate the partitioned gate generator and connect the gates
 363         m.submodules.gen = gen = GateGenerator(mwidth)
 364         comb += gates.eq(gen.gates)
 365         p_offset = gen.p_offset
 366         p_width = gen.p_width
 367         # generate shifted down inputs and outputs
 368         p_operands = list()
 369         for i in range(nops):
 370             p_i = Signal(width, name=f"p_{i+1}")
 371             p_operands.append(p_i)
 372             for pos in range(mwidth):
 373                 with m.If(p_offset == pos):
 374                     comb += p_i.eq(operands[i].sig[pos * step:])
 375         p_output = Signal(out_width)
 376         for pos in range(mwidth):
 377             with m.If(p_offset == pos):
 378                 comb += p_output.eq(output[pos * out_step:])
 379         # generate and check expected values for all possible partition sizes
 380         all_operands_non_zero = Signal()
 381         for w in range(1, mwidth+1):
 382             with m.If(p_width == w):
 383                 # calculate the expected output, for the given bit width,
 384                 # truncating the inputs to the partition size
 385                 input_bit_width = w * step
 386                 output_bit_width = w * out_step
 387                 expected = Signal(output_bit_width, name=f"expected_{w}")
 388                 trunc_operands = list()
 389                 for i in range(nops):
 390                     t_i = Signal(input_bit_width, name=f"t{w}_{i+1}")
 391                     trunc_operands.append(t_i)
 392                     comb += t_i.eq(p_operands[i][:input_bit_width])
 393                 if part_out:
 394                     # for partition-like outputs, calculate the LSB
 395                     # and replicate it on the partition
 396                     lsb = Signal(name=f"lsb_{w}")
 397                     comb += lsb.eq(self.op(*trunc_operands))
 398                     comb += expected.eq(Repl(lsb, output_bit_width))
 399                 else:
 400                     # otherwise, just take the operation result
 401                     comb += expected.eq(self.op(*trunc_operands))
 402                 # truncate the output, compare and assert
 403                 comb += Assert(p_output[:output_bit_width] == expected)
 404                 # ensure a test case with all non-zero operands
 405                 non_zero_op = Signal(nops)
 406                 for i in range(nops):
 407                     comb += non_zero_op[i].eq(trunc_operands[i].any())
 408                 comb += all_operands_non_zero.eq(non_zero_op.all())
 409         # output a test case
 410         comb += Cover((p_offset != 0) & (p_width == 3) & (sum(output) > 1) &
 411                       (p_output != 0) & all_operands_non_zero)
 412         return m
 413
 414
 415 class PartitionTestCase(FHDLTestCase):
 416     def test_formal(self):
 417         style = {
 418             'dec': {'base': 'dec'},
 419             'bin': {'base': 'bin'}
 420         }
 421         traces = [
 422             ('p_offset[2:0]', 'dec'),
 423             ('p_width[3:0]', 'dec'),
 424             ('p_finish[3:0]', 'dec'),
 425             ('p_gates[8:0]', 'bin'),
 426             ('dut', {'submodule': 'dut'}, [
 427                 ('gates[6:0]', 'bin'),
 428                 'output[63:0]']),
 429             'p_output[63:0]', 'expected_3[21:0]']
 430         write_gtkw(
 431             'proof_partition_cover.gtkw',
 432             os.path.dirname(__file__) +
 433             '/proof_partition_formal/engine_0/trace0.vcd',
 434             traces, style,
 435             module='top',
 436             zoom=-3
 437         )
 438         write_gtkw(
 439             'proof_partition_bmc.gtkw',
 440             os.path.dirname(__file__) +
 441             '/proof_partition_formal/engine_0/trace.vcd',
 442             traces, style,
 443             module='top',
 444             zoom=-3
 445         )
 446         module = Driver()
 447         self.assertFormal(module, mode="bmc", depth=1)
 448         self.assertFormal(module, mode="cover", depth=1)
 449
 450     def test_generator(self):
 451         style = {
 452             'dec': {'base': 'dec'},
 453             'bin': {'base': 'bin'}
 454         }
 455         traces = [
 456             ('p_offset[2:0]', 'dec'),
 457             ('p_width[3:0]', 'dec'),
 458             ('p_finish[3:0]', 'dec'),
 459             ('p_gates[8:0]', 'bin'),
 460             ('dut', {'submodule': 'dut'}, [
 461                 ('gates[6:0]', 'bin'),
 462                 'output[63:0]']),
 463             'p_output[63:0]', 'expected_3[21:0]',
 464             'a_3[23:0]', 'b_3[32:0]', 'expected_3[2:0]']
 465         write_gtkw(
 466             'proof_partition_generator_cover.gtkw',
 467             os.path.dirname(__file__) +
 468             '/proof_partition_generator/engine_0/trace0.vcd',
 469             traces, style,
 470             module='top',
 471             zoom=-3
 472         )
 473         write_gtkw(
 474             'proof_partition_generator_bmc.gtkw',
 475             os.path.dirname(__file__) +
 476             '/proof_partition_generator/engine_0/trace.vcd',
 477             traces, style,
 478             module='top',
 479             zoom=-3
 480         )
 481         module = GeneratorDriver()
 482         self.assertFormal(module, mode="bmc", depth=1)
 483         self.assertFormal(module, mode="cover", depth=1)
 484
 485     def test_partsig_eq(self):
 486         style = {
 487             'dec': {'base': 'dec'},
 488             'bin': {'base': 'bin'}
 489         }
 490         traces = [
 491             ('p_offset[2:0]', 'dec'),
 492             ('p_width[3:0]', 'dec'),
 493             ('p_gates[8:0]', 'bin'),
 494             'i_1[63:0]', 'i_2[63:0]',
 495             ('eq_1', {'submodule': 'eq_1'}, [
 496                 ('gates[6:0]', 'bin'),
 497                 'a[63:0]', 'b[63:0]',
 498                 ('output[7:0]', 'bin')]),
 499             'p_1[63:0]', 'p_2[63:0]',
 500             ('p_output[7:0]', 'bin'),
 501             't3_1[23:0]', 't3_2[23:0]', 'lsb_3',
 502             ('expected_3[2:0]', 'bin')]
 503         write_gtkw(
 504             'proof_partsig_eq_cover.gtkw',
 505             os.path.dirname(__file__) +
 506             '/proof_partition_partsig_eq/engine_0/trace0.vcd',
 507             traces, style,
 508             module='top',
 509             zoom=-3
 510         )
 511         write_gtkw(
 512             'proof_partsig_eq_bmc.gtkw',
 513             os.path.dirname(__file__) +
 514             '/proof_partition_partsig_eq/engine_0/trace.vcd',
 515             traces, style,
 516             module='top',
 517             zoom=-3
 518         )
 519         module = OpDriver(operator.eq)
 520         self.assertFormal(module, mode="bmc", depth=1)
 521         self.assertFormal(module, mode="cover", depth=1)
 522
 523     def test_partsig_ne(self):
 524         module = OpDriver(operator.ne)
 525         self.assertFormal(module, mode="bmc", depth=1)
 526
 527     def test_partsig_gt(self):
 528         module = OpDriver(operator.gt)
 529         self.assertFormal(module, mode="bmc", depth=1)
 530
 531     def test_partsig_ge(self):
 532         module = OpDriver(operator.ge)
 533         self.assertFormal(module, mode="bmc", depth=1)
 534
 535     def test_partsig_lt(self):
 536         module = OpDriver(operator.lt)
 537         self.assertFormal(module, mode="bmc", depth=1)
 538
 539     def test_partsig_le(self):
 540         module = OpDriver(operator.le)
 541         self.assertFormal(module, mode="bmc", depth=1)
 542
 543     def test_partsig_all(self):
 544         style = {
 545             'dec': {'base': 'dec'},
 546             'bin': {'base': 'bin'}
 547         }
 548         traces = [
 549             ('p_offset[2:0]', 'dec'),
 550             ('p_width[3:0]', 'dec'),
 551             ('p_gates[8:0]', 'bin'),
 552             'i_1[63:0]',
 553             ('eq_1', {'submodule': 'eq_1'}, [
 554                 ('gates[6:0]', 'bin'),
 555                 'a[63:0]', 'b[63:0]',
 556                 ('output[7:0]', 'bin')]),
 557             'p_1[63:0]',
 558             ('p_output[7:0]', 'bin'),
 559             't3_1[23:0]', 'lsb_3',
 560             ('expected_3[2:0]', 'bin')]
 561         write_gtkw(
 562             'proof_partsig_all_cover.gtkw',
 563             os.path.dirname(__file__) +
 564             '/proof_partition_partsig_all/engine_0/trace0.vcd',
 565             traces, style,
 566             module='top',
 567             zoom=-3
 568         )
 569
 570         def op_all(obj):
 571             return obj.all()
 572
 573         module = OpDriver(op_all, nops=1)
 574         self.assertFormal(module, mode="bmc", depth=1)
 575         self.assertFormal(module, mode="cover", depth=1)
 576
 577     def test_partsig_any(self):
 578
 579         def op_any(obj):
 580             return obj.any()
 581
 582         module = OpDriver(op_any, nops=1)
 583         self.assertFormal(module, mode="bmc", depth=1)
 584
 585     def test_partsig_xor(self):
 586
 587         def op_xor(obj):
 588             return obj.xor()
 589
 590         # 8-bit partitions take a long time, for some reason
 591         module = OpDriver(op_xor, nops=1, width=32, mwidth=4)
 592         self.assertFormal(module, mode="bmc", depth=1)
 593
 594     def test_partsig_add(self):
 595         style = {
 596             'dec': {'base': 'dec'},
 597             'bin': {'base': 'bin'}
 598         }
 599         traces = [
 600             ('p_offset[2:0]', 'dec'),
 601             ('p_width[3:0]', 'dec'),
 602             ('p_gates[8:0]', 'bin'),
 603             'i_1[63:0]', 'i_2[63:0]',
 604             ('add_1', {'submodule': 'add_1'}, [
 605                 ('gates[6:0]', 'bin'),
 606                 'a[63:0]', 'b[63:0]',
 607                 'output[63:0]']),
 608             'p_1[63:0]', 'p_2[63:0]',
 609             'p_output[63:0]',
 610             't3_1[23:0]', 't3_2[23:0]',
 611             'expected_3[23:0]']
 612         write_gtkw(
 613             'proof_partsig_add_cover.gtkw',
 614             os.path.dirname(__file__) +
 615             '/proof_partition_partsig_add/engine_0/trace0.vcd',
 616             traces, style,
 617             module='top',
 618             zoom=-3
 619         )
 620
 621         module = OpDriver(operator.add, part_out=False)
 622         self.assertFormal(module, mode="bmc", depth=1)
 623         self.assertFormal(module, mode="cover", depth=1)
 624
 625     def test_partsig_sub(self):
 626         module = OpDriver(operator.sub, part_out=False)
 627         self.assertFormal(module, mode="bmc", depth=1)
 628
 629     def test_partsig_neg(self):
 630         style = {
 631             'dec': {'base': 'dec'},
 632             'bin': {'base': 'bin'}
 633         }
 634         traces = [
 635             ('p_offset[2:0]', 'dec'),
 636             ('p_width[3:0]', 'dec'),
 637             ('p_gates[8:0]', 'bin'),
 638             'i_1[63:0]',
 639             ('add_1', {'submodule': 'add_1'}, [
 640                 ('gates[6:0]', 'bin'),
 641                 'a[63:0]', 'b[63:0]',
 642                 'output[63:0]']),
 643             'p_1[63:0]',
 644             'p_output[63:0]',
 645             't3_1[23:0]',
 646             'expected_3[23:0]']
 647         write_gtkw(
 648             'proof_partsig_neg_bmc.gtkw',
 649             os.path.dirname(__file__) +
 650             '/proof_partition_partsig_neg/engine_0/trace.vcd',
 651             traces, style,
 652             module='top',
 653             zoom=-3
 654         )
 655
 656         module = OpDriver(operator.neg, nops=1, part_out=False)
 657         self.assertFormal(module, mode="bmc", depth=1)
 658
 659     def test_partsig_and(self):
 660         module = OpDriver(operator.and_, part_out=False)
 661         self.assertFormal(module, mode="bmc", depth=1)
 662
 663     def test_partsig_or(self):
 664         module = OpDriver(operator.or_, part_out=False)
 665         self.assertFormal(module, mode="bmc", depth=1)
 666
 667     def test_partsig_logical_xor(self):
 668         module = OpDriver(operator.xor, part_out=False)
 669         self.assertFormal(module, mode="bmc", depth=1)
 670
 671     def test_partsig_not(self):
 672         module = OpDriver(operator.inv, nops=1, part_out=False)
 673         self.assertFormal(module, mode="bmc", depth=1)
 674
 675     def test_partsig_implies(self):
 676
 677         def op_implies(a, b):
 678             return a.implies(b)
 679
 680         # 8 x 8-bit partitions take a long time, for some reason
 681         module = OpDriver(op_implies, part_out=False, width=32, mwidth=8)
 682         self.assertFormal(module, mode="bmc", depth=1)
 683
 684
 685 if __name__ == '__main__':
 686     unittest.main()