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         result = self.op(*operands)
 362         if isinstance(result, PartitionedSignal):
 363             comb += output.eq(result.sig)
 364         # TODO: remove when all operations return PartitionedSignal
 365         else:
 366             comb += output.eq(result)
 367         # instantiate the partitioned gate generator and connect the gates
 368         m.submodules.gen = gen = GateGenerator(mwidth)
 369         comb += gates.eq(gen.gates)
 370         p_offset = gen.p_offset
 371         p_width = gen.p_width
 372         # generate shifted down inputs and outputs
 373         p_operands = list()
 374         for i in range(nops):
 375             p_i = Signal(width, name=f"p_{i+1}")
 376             p_operands.append(p_i)
 377             for pos in range(mwidth):
 378                 with m.If(p_offset == pos):
 379                     comb += p_i.eq(operands[i].sig[pos * step:])
 380         p_output = Signal(out_width)
 381         for pos in range(mwidth):
 382             with m.If(p_offset == pos):
 383                 comb += p_output.eq(output[pos * out_step:])
 384         # generate and check expected values for all possible partition sizes
 385         all_operands_non_zero = Signal()
 386         for w in range(1, mwidth+1):
 387             with m.If(p_width == w):
 388                 # calculate the expected output, for the given bit width,
 389                 # truncating the inputs to the partition size
 390                 input_bit_width = w * step
 391                 output_bit_width = w * out_step
 392                 expected = Signal(output_bit_width, name=f"expected_{w}")
 393                 trunc_operands = list()
 394                 for i in range(nops):
 395                     t_i = Signal(input_bit_width, name=f"t{w}_{i+1}")
 396                     trunc_operands.append(t_i)
 397                     comb += t_i.eq(p_operands[i][:input_bit_width])
 398                 if part_out:
 399                     # for partition-like outputs, calculate the LSB
 400                     # and replicate it on the partition
 401                     lsb = Signal(name=f"lsb_{w}")
 402                     comb += lsb.eq(self.op(*trunc_operands))
 403                     comb += expected.eq(Repl(lsb, output_bit_width))
 404                 else:
 405                     # otherwise, just take the operation result
 406                     comb += expected.eq(self.op(*trunc_operands))
 407                 # truncate the output, compare and assert
 408                 comb += Assert(p_output[:output_bit_width] == expected)
 409                 # ensure a test case with all non-zero operands
 410                 non_zero_op = Signal(nops)
 411                 for i in range(nops):
 412                     comb += non_zero_op[i].eq(trunc_operands[i].any())
 413                 comb += all_operands_non_zero.eq(non_zero_op.all())
 414         # output a test case
 415         comb += Cover((p_offset != 0) & (p_width == 3) & (sum(output) > 1) &
 416                       (p_output != 0) & all_operands_non_zero)
 417         return m
 418
 419
 420 class PartitionTestCase(FHDLTestCase):
 421     def test_formal(self):
 422         style = {
 423             'dec': {'base': 'dec'},
 424             'bin': {'base': 'bin'}
 425         }
 426         traces = [
 427             ('p_offset[2:0]', 'dec'),
 428             ('p_width[3:0]', 'dec'),
 429             ('p_finish[3:0]', 'dec'),
 430             ('p_gates[8:0]', 'bin'),
 431             ('dut', {'submodule': 'dut'}, [
 432                 ('gates[6:0]', 'bin'),
 433                 'output[63:0]']),
 434             'p_output[63:0]', 'expected_3[21:0]']
 435         write_gtkw(
 436             'proof_partition_cover.gtkw',
 437             os.path.dirname(__file__) +
 438             '/proof_partition_formal/engine_0/trace0.vcd',
 439             traces, style,
 440             module='top',
 441             zoom=-3
 442         )
 443         write_gtkw(
 444             'proof_partition_bmc.gtkw',
 445             os.path.dirname(__file__) +
 446             '/proof_partition_formal/engine_0/trace.vcd',
 447             traces, style,
 448             module='top',
 449             zoom=-3
 450         )
 451         module = Driver()
 452         self.assertFormal(module, mode="bmc", depth=1)
 453         self.assertFormal(module, mode="cover", depth=1)
 454
 455     def test_generator(self):
 456         style = {
 457             'dec': {'base': 'dec'},
 458             'bin': {'base': 'bin'}
 459         }
 460         traces = [
 461             ('p_offset[2:0]', 'dec'),
 462             ('p_width[3:0]', 'dec'),
 463             ('p_finish[3:0]', 'dec'),
 464             ('p_gates[8:0]', 'bin'),
 465             ('dut', {'submodule': 'dut'}, [
 466                 ('gates[6:0]', 'bin'),
 467                 'output[63:0]']),
 468             'p_output[63:0]', 'expected_3[21:0]',
 469             'a_3[23:0]', 'b_3[32:0]', 'expected_3[2:0]']
 470         write_gtkw(
 471             'proof_partition_generator_cover.gtkw',
 472             os.path.dirname(__file__) +
 473             '/proof_partition_generator/engine_0/trace0.vcd',
 474             traces, style,
 475             module='top',
 476             zoom=-3
 477         )
 478         write_gtkw(
 479             'proof_partition_generator_bmc.gtkw',
 480             os.path.dirname(__file__) +
 481             '/proof_partition_generator/engine_0/trace.vcd',
 482             traces, style,
 483             module='top',
 484             zoom=-3
 485         )
 486         module = GeneratorDriver()
 487         self.assertFormal(module, mode="bmc", depth=1)
 488         self.assertFormal(module, mode="cover", depth=1)
 489
 490     def test_partsig_eq(self):
 491         style = {
 492             'dec': {'base': 'dec'},
 493             'bin': {'base': 'bin'}
 494         }
 495         traces = [
 496             ('p_offset[2:0]', 'dec'),
 497             ('p_width[3:0]', 'dec'),
 498             ('p_gates[8:0]', 'bin'),
 499             'i_1[63:0]', 'i_2[63:0]',
 500             ('eq_1', {'submodule': 'eq_1'}, [
 501                 ('gates[6:0]', 'bin'),
 502                 'a[63:0]', 'b[63:0]',
 503                 ('output[7:0]', 'bin')]),
 504             'p_1[63:0]', 'p_2[63:0]',
 505             ('p_output[7:0]', 'bin'),
 506             't3_1[23:0]', 't3_2[23:0]', 'lsb_3',
 507             ('expected_3[2:0]', 'bin')]
 508         write_gtkw(
 509             'proof_partsig_eq_cover.gtkw',
 510             os.path.dirname(__file__) +
 511             '/proof_partition_partsig_eq/engine_0/trace0.vcd',
 512             traces, style,
 513             module='top',
 514             zoom=-3
 515         )
 516         write_gtkw(
 517             'proof_partsig_eq_bmc.gtkw',
 518             os.path.dirname(__file__) +
 519             '/proof_partition_partsig_eq/engine_0/trace.vcd',
 520             traces, style,
 521             module='top',
 522             zoom=-3
 523         )
 524         module = OpDriver(operator.eq)
 525         self.assertFormal(module, mode="bmc", depth=1)
 526         self.assertFormal(module, mode="cover", depth=1)
 527
 528     def test_partsig_ne(self):
 529         module = OpDriver(operator.ne)
 530         self.assertFormal(module, mode="bmc", depth=1)
 531
 532     def test_partsig_gt(self):
 533         module = OpDriver(operator.gt)
 534         self.assertFormal(module, mode="bmc", depth=1)
 535
 536     def test_partsig_ge(self):
 537         module = OpDriver(operator.ge)
 538         self.assertFormal(module, mode="bmc", depth=1)
 539
 540     def test_partsig_lt(self):
 541         module = OpDriver(operator.lt)
 542         self.assertFormal(module, mode="bmc", depth=1)
 543
 544     def test_partsig_le(self):
 545         module = OpDriver(operator.le)
 546         self.assertFormal(module, mode="bmc", depth=1)
 547
 548     def test_partsig_all(self):
 549         style = {
 550             'dec': {'base': 'dec'},
 551             'bin': {'base': 'bin'}
 552         }
 553         traces = [
 554             ('p_offset[2:0]', 'dec'),
 555             ('p_width[3:0]', 'dec'),
 556             ('p_gates[8:0]', 'bin'),
 557             'i_1[63:0]',
 558             ('eq_1', {'submodule': 'eq_1'}, [
 559                 ('gates[6:0]', 'bin'),
 560                 'a[63:0]', 'b[63:0]',
 561                 ('output[7:0]', 'bin')]),
 562             'p_1[63:0]',
 563             ('p_output[7:0]', 'bin'),
 564             't3_1[23:0]', 'lsb_3',
 565             ('expected_3[2:0]', 'bin')]
 566         write_gtkw(
 567             'proof_partsig_all_cover.gtkw',
 568             os.path.dirname(__file__) +
 569             '/proof_partition_partsig_all/engine_0/trace0.vcd',
 570             traces, style,
 571             module='top',
 572             zoom=-3
 573         )
 574
 575         def op_all(obj):
 576             return obj.all()
 577
 578         module = OpDriver(op_all, nops=1)
 579         self.assertFormal(module, mode="bmc", depth=1)
 580         self.assertFormal(module, mode="cover", depth=1)
 581
 582     def test_partsig_any(self):
 583
 584         def op_any(obj):
 585             return obj.any()
 586
 587         module = OpDriver(op_any, nops=1)
 588         self.assertFormal(module, mode="bmc", depth=1)
 589
 590     def test_partsig_xor(self):
 591
 592         def op_xor(obj):
 593             return obj.xor()
 594
 595         module = OpDriver(op_xor, nops=1)
 596         # yices2 is slow on this test for some reason
 597         # use z3 instead
 598         self.assertFormal(module, mode="bmc", depth=1, solver="z3")
 599
 600     def test_partsig_add(self):
 601         style = {
 602             'dec': {'base': 'dec'},
 603             'bin': {'base': 'bin'}
 604         }
 605         traces = [
 606             ('p_offset[2:0]', 'dec'),
 607             ('p_width[3:0]', 'dec'),
 608             ('p_gates[8:0]', 'bin'),
 609             'i_1[63:0]', 'i_2[63:0]',
 610             ('add_1', {'submodule': 'add_1'}, [
 611                 ('gates[6:0]', 'bin'),
 612                 'a[63:0]', 'b[63:0]',
 613                 'output[63:0]']),
 614             'p_1[63:0]', 'p_2[63:0]',
 615             'p_output[63:0]',
 616             't3_1[23:0]', 't3_2[23:0]',
 617             'expected_3[23:0]']
 618         write_gtkw(
 619             'proof_partsig_add_cover.gtkw',
 620             os.path.dirname(__file__) +
 621             '/proof_partition_partsig_add/engine_0/trace0.vcd',
 622             traces, style,
 623             module='top',
 624             zoom=-3
 625         )
 626
 627         module = OpDriver(operator.add, part_out=False)
 628         self.assertFormal(module, mode="bmc", depth=1)
 629         self.assertFormal(module, mode="cover", depth=1)
 630
 631     def test_partsig_sub(self):
 632         module = OpDriver(operator.sub, part_out=False)
 633         self.assertFormal(module, mode="bmc", depth=1)
 634
 635     def test_partsig_neg(self):
 636         style = {
 637             'dec': {'base': 'dec'},
 638             'bin': {'base': 'bin'}
 639         }
 640         traces = [
 641             ('p_offset[2:0]', 'dec'),
 642             ('p_width[3:0]', 'dec'),
 643             ('p_gates[8:0]', 'bin'),
 644             'i_1[63:0]',
 645             ('add_1', {'submodule': 'add_1'}, [
 646                 ('gates[6:0]', 'bin'),
 647                 'a[63:0]', 'b[63:0]',
 648                 'output[63:0]']),
 649             'p_1[63:0]',
 650             'p_output[63:0]',
 651             't3_1[23:0]',
 652             'expected_3[23:0]']
 653         write_gtkw(
 654             'proof_partsig_neg_bmc.gtkw',
 655             os.path.dirname(__file__) +
 656             '/proof_partition_partsig_neg/engine_0/trace.vcd',
 657             traces, style,
 658             module='top',
 659             zoom=-3
 660         )
 661
 662         module = OpDriver(operator.neg, nops=1, part_out=False)
 663         self.assertFormal(module, mode="bmc", depth=1)
 664
 665     def test_partsig_and(self):
 666         module = OpDriver(operator.and_, part_out=False)
 667         self.assertFormal(module, mode="bmc", depth=1)
 668
 669     def test_partsig_or(self):
 670         module = OpDriver(operator.or_, part_out=False)
 671         self.assertFormal(module, mode="bmc", depth=1)
 672
 673     def test_partsig_logical_xor(self):
 674         module = OpDriver(operator.xor, part_out=False)
 675         self.assertFormal(module, mode="bmc", depth=1)
 676
 677     def test_partsig_not(self):
 678         module = OpDriver(operator.inv, nops=1, part_out=False)
 679         self.assertFormal(module, mode="bmc", depth=1)
 680
 681     def test_partsig_implies(self):
 682
 683         def op_implies(a, b):
 684             return a.implies(b)
 685
 686         module = OpDriver(op_implies, part_out=False)
 687         # yices2 is slow on this test for some reason
 688         # use z3 instead
 689         self.assertFormal(module, mode="bmc", depth=1, solver="z3")
 690
 691
 692 if __name__ == '__main__':
 693     unittest.main()