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