1 # Proof of correctness for bit permute module

2 # Copyright (C) 2020 Michael Nolan <mtnolan2640@gmail.com>

5 signed)

12 import unittest

15 # So formal verification is a little different than writing a test

16 # case, as you're actually generating logic around your module to

17 # check that it behaves a certain way. So here, I'm going to create a

18 # module to put my formal assertions in

21 # We don't need any inputs and outputs here, so I won't

22 # declare any

23 pass

26 # standard stuff

30 # instantiate the device under test as a submodule

33 # Grab the inputs and outputs of the DUT to make them more

34 # convenient to access

39 # Before we prove any properties about the DUT, we need to set

40 # up its inputs. There's a couple ways to do this, you could

41 # define some inputs and outputs for the driver module and

42 # wire them up to the DUT, but that's kind of a pain. The

43 # other option is to use AnyConst/AnySeq, which tells yosys

44 # that those inputs can take on any value.

46 # AnyConst should be used when the input should take on a

47 # random value, but that value should be constant throughout

48 # the test.

49 # AnySeq should be used when the input can change on every

50 # cycle

52 # Since this is a combinatorial circuit, it really doesn't

53 # matter which one you choose, so I chose AnyConst. If this

54 # was a sequential circuit, (especially a state machine) you'd

55 # want to use AnySeq

59 # The pseudocode in the Power ISA manual (v3.1) is as follows:

60 # do i = 0 to 7

61 # index <- RS[8*i:8*i+8]

62 # if index < 64:

63 # perm[i] <- RB[index]

64 # else:

65 # perm[i] <- 0

66 # RA <- 56'b0 || perm[0:8] # big endian though

68 # Looking at this, I can identify 3 properties that the bperm

69 # module should keep:

70 # 1. RA[8:64] should always equal 0

71 # 2. If RB[i*8:i*8+8] >= 64 then RA[i] should equal 0

72 # 3. If RB[i*8:i*8+8] < 64 then RA[i] should RS[index]

74 # Now we need to Assert that the properties above hold:

76 # Property 1: RA[8:64] should always equal 0

78 # Notice how we're adding Assert to comb like it's a circuit?

79 # That's because it kind of is. If you run this proof and have

80 # yosys graph the ilang, you'll be able to see an equals

81 # comparison cell feeding into an assert cell

83 # Now we need to prove property #2. I'm going to leave this to

84 # you Cole. I'd start by writing a for loop and extracting the

85 # 8 indices into signals. Then I'd write an if statement

86 # checking if the index is >= 64 (it's hardware, so use an

87 # m.If()). Finally, I'd add an assert that checks whether

88 # ra[i] is equal to 0

94 # to avoid having to create an Array of rb,

95 # cycle through from 0-63 on the index *whistle nonchalantly*

100 return m

104 # This bit here is actually in charge of running the formal

105 # proof. It has nmigen spit out the ilang, and feeds it to

106 # SymbiYosys to run the proof. If the proof fails, yosys will

107 # generate a .vcd file showing how it was able to violate your

108 # assertions in proof_bperm_formal/engine_0/trace.vcd. From that

109 # you should be able to figure out what went wrong, and either

110 # correct the assertion or fix the DUT

113 # This runs a Bounded Model Check on the driver module

114 # above. What that does is it starts at some initial state,

115 # and steps it through `depth` cycles, checking that the

116 # assertions hold at every cycle. Since this is a

117 # combinatorial module, it only needs 1 cycle to prove

118 # everything.

122 # As mentioned above, you can look at the graph in yosys and see

123 # all the assertion cells