From: colepoirier Date: Tue, 19 May 2020 20:43:13 +0000 (-0700) Subject: Renamed bperm files in fu/logical and fu/logical formal to correct name X-Git-Tag: div_pipeline~1061 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c49d316610ff0b35241203013fb551a87e62d0c8;p=soc.git Renamed bperm files in fu/logical and fu/logical formal to correct name of operation 'bpermd', added up-to-date docstring from spec v3.1 --- diff --git a/src/soc/fu/logical/bperm.py b/src/soc/fu/logical/bperm.py deleted file mode 100644 index 674555b8..00000000 --- a/src/soc/fu/logical/bperm.py +++ /dev/null @@ -1,55 +0,0 @@ -from nmigen import Elaboratable, Signal, Module, Repl, Cat, Const, Array -from nmigen.cli import main - - -class Bpermd(Elaboratable): - """This class does a Bit Permute on a Doubleword - - X-form bpermd RA,RS,RB] - - Eight permuted bits are produced. For each permuted bit i where i ranges - from 0 to 7 and for each byte i of RS, do the following. If byte i of RS - is less than 64, permuted bit i is setto the bit of RB specified by byte - i of RS; otherwise permuted bit i is set to 0. The permuted bits are - placed in the least-significantbyte of RA, and the remaining bits are - filled with 0s. - Special Registers Altered: None - - Programming note: - The fact that the permuted bit is 0 if the corresponding index value - exceeds 63 permits the permuted bits to be selected from a 128-bit - quantity, using a single index register. For example, assume that the - 128-bit quantity Q, from which the permuted bits are to be selected, is - in registers r2(high-order 64 bits of Q) and r3 (low-order 64 bits of Q), - that the index values are in register r1, with each byte of r1 containing - a value in the range 0:127, and that each byte of register r4 contains - the value 64. The following code sequence selects eight permuted bits - from Q and places them into the low-order byte of r6. - """ - - def __init__(self, width): - self.width = width - self.rs = Signal(width, reset_less=True) - self.ra = Signal(width, reset_less=True) - self.rb = Signal(width, reset_less=True) - - def elaborate(self, platform): - m = Module() - perm = Signal(self.width, reset_less=True) - rb64 = [Signal(1, reset_less=True, name=f"rb64_{i}") for i in range(64)] - for i in range(64): - m.d.comb += rb64[i].eq(self.rb[i]) - rb64 = Array(rb64) - for i in range(8): - index = self.rs[8*i:8*i+8] - idx = Signal(8, name=f"idx_{i}", reset_less=True) - m.d.comb += idx.eq(index) - with m.If(idx < 64): - m.d.comb += perm[i].eq(rb64[idx]) - m.d.comb += self.ra[0:8].eq(perm) - return m - - -if __name__ == "__main__": - bperm = Bpermd(width=64) - main(bperm, ports=[bperm.rs, bperm.ra, bperm.rb]) diff --git a/src/soc/fu/logical/bpermd.py b/src/soc/fu/logical/bpermd.py new file mode 100644 index 00000000..1fc50e97 --- /dev/null +++ b/src/soc/fu/logical/bpermd.py @@ -0,0 +1,92 @@ +from nmigen import Elaboratable, Signal, Module, Repl, Cat, Const, Array +from nmigen.cli import main + + +class Bpermd(Elaboratable): + """ + from POWERISA v3.1 p105, chaper 3 + + This class does a Bit Permute on a Doubleword + + permd RA,RS,RB + + do i = 0 to 7 + index ← (RS)[8*i:8*i+7] + If index < 64 + then perm[i] ← (RB)[index] + else permi[i] ← 0 + RA ←56[0] || perm[0:7] + + Eight permuted bits are produced. + For each permutedbit i where i + ranges from 0 to 7 and for each + byte i of RS, do the following. + + If byte i of RS is less than + 64, permuted bit i is set to + the bit of RB specified by + byte i of RS; otherwise + permuted bit i is set to 0. + + The permuted bits are placed in + the least-significant byte of RA, + and the remaining bits are filled + with 0s. + + Special Registers Altered: + None + + Programming Note: + + The fact that the permuted bit is + 0 if the corresponding index value + exceeds 63 permits the permuted + bits to be selected from a 128-bit + quantity, using a single index + register. For example, assume that + the 128-bit quantity Q, from which + the permuted bits are to be + selected, is in registers r2 + (high-order 64 bits of Q) and r3 + (low-order 64 bits of Q), that the + index values are in register r1, + with each byte of r1 containing a + value in the range 0:127, and that + each byte of register r4 contains + the value 64. The following code + sequence selects eight permuted + bits from Q and places them into + the low-order byteof r6. + + bpermd r6,r1,r2 # select from high-order half of Q + xor r0,r1,r4 # adjust index values + bpermd r5,r0,r3 # select from low-order half of Q + or r6,r6,r5 # merge the two selections + """ + + def __init__(self, width): + self.width = width + self.rs = Signal(width, reset_less=True) + self.ra = Signal(width, reset_less=True) + self.rb = Signal(width, reset_less=True) + + def elaborate(self, platform): + m = Module() + perm = Signal(self.width, reset_less=True) + rb64 = [Signal(1, reset_less=True, name=f"rb64_{i}") for i in range(64)] + for i in range(64): + m.d.comb += rb64[i].eq(self.rb[i]) + rb64 = Array(rb64) + for i in range(8): + index = self.rs[8*i:8*i+8] + idx = Signal(8, name=f"idx_{i}", reset_less=True) + m.d.comb += idx.eq(index) + with m.If(idx < 64): + m.d.comb += perm[i].eq(rb64[idx]) + m.d.comb += self.ra[0:8].eq(perm) + return m + + +if __name__ == "__main__": + bperm = Bpermd(width=64) + main(bperm, ports=[bperm.rs, bperm.ra, bperm.rb]) diff --git a/src/soc/fu/logical/formal/proof_bperm.py b/src/soc/fu/logical/formal/proof_bperm.py deleted file mode 100644 index 11b8e487..00000000 --- a/src/soc/fu/logical/formal/proof_bperm.py +++ /dev/null @@ -1,132 +0,0 @@ -# Proof of correctness for bit permute module -# Copyright (C) 2020 Michael Nolan - -from nmigen import (Module, Signal, Elaboratable, Mux, Cat, Repl, - signed) -from nmigen.asserts import Assert, AnyConst, Assume, Cover -from nmigen.test.utils import FHDLTestCase -from nmigen.cli import rtlil - -from soc.fu.logical.bperm import Bpermd - -import unittest - - -# So formal verification is a little different than writing a test -# case, as you're actually generating logic around your module to -# check that it behaves a certain way. So here, I'm going to create a -# module to put my formal assertions in -class Driver(Elaboratable): - def __init__(self): - # We don't need any inputs and outputs here, so I won't - # declare any - pass - - def elaborate(self, platform): - # standard stuff - m = Module() - comb = m.d.comb - - # instantiate the device under test as a submodule - m.submodules.bperm = bperm = Bpermd(64) - - # Grab the inputs and outputs of the DUT to make them more - # convenient to access - rs = bperm.rs - rb = bperm.rb - ra = bperm.ra - - # Before we prove any properties about the DUT, we need to set - # up its inputs. There's a couple ways to do this, you could - # define some inputs and outputs for the driver module and - # wire them up to the DUT, but that's kind of a pain. The - # other option is to use AnyConst/AnySeq, which tells yosys - # that those inputs can take on any value. - - # AnyConst should be used when the input should take on a - # random value, but that value should be constant throughout - # the test. - # AnySeq should be used when the input can change on every - # cycle - - # Since this is a combinatorial circuit, it really doesn't - # matter which one you choose, so I chose AnyConst. If this - # was a sequential circuit, (especially a state machine) you'd - # want to use AnySeq - comb += [rs.eq(AnyConst(64)), - rb.eq(AnyConst(64))] - - # The pseudocode in the Power ISA manual (v3.1) is as follows: - # do i = 0 to 7 - # index <- RS[8*i:8*i+8] - # if index < 64: - # perm[i] <- RB[index] - # else: - # perm[i] <- 0 - # RA <- 56'b0 || perm[0:8] # big endian though - - # Looking at this, I can identify 3 properties that the bperm - # module should keep: - # 1. RA[8:64] should always equal 0 - # 2. If RB[i*8:i*8+8] >= 64 then RA[i] should equal 0 - # 3. If RB[i*8:i*8+8] < 64 then RA[i] should RS[index] - - # Now we need to Assert that the properties above hold: - - # Property 1: RA[8:64] should always equal 0 - comb += Assert(ra[8:] == 0) - # Notice how we're adding Assert to comb like it's a circuit? - # That's because it kind of is. If you run this proof and have - # yosys graph the ilang, you'll be able to see an equals - # comparison cell feeding into an assert cell - - # Now we need to prove property #2. I'm going to leave this to - # you Cole. I'd start by writing a for loop and extracting the - # 8 indices into signals. Then I'd write an if statement - # checking if the index is >= 64 (it's hardware, so use an - # m.If()). Finally, I'd add an assert that checks whether - # ra[i] is equal to 0 - for i in range(8): - index = rs[i*8:i*8+8] - with m.If(index >= 64): - comb += Assert(ra[i] == 0) - with m.Else(): - # to avoid having to create an Array of rb, - # cycle through from 0-63 on the index *whistle nonchalantly* - for j in range(64): - with m.If(index == j): - comb += Assert(ra[i] == rb[j]) - - return m - - -class TestCase(FHDLTestCase): - # This bit here is actually in charge of running the formal - # proof. It has nmigen spit out the ilang, and feeds it to - # SymbiYosys to run the proof. If the proof fails, yosys will - # generate a .vcd file showing how it was able to violate your - # assertions in proof_bperm_formal/engine_0/trace.vcd. From that - # you should be able to figure out what went wrong, and either - # correct the assertion or fix the DUT - def test_formal(self): - module = Driver() - # This runs a Bounded Model Check on the driver module - # above. What that does is it starts at some initial state, - # and steps it through `depth` cycles, checking that the - # assertions hold at every cycle. Since this is a - # combinatorial module, it only needs 1 cycle to prove - # everything. - self.assertFormal(module, mode="bmc", depth=2) - self.assertFormal(module, mode="cover", depth=2) - - # As mentioned above, you can look at the graph in yosys and see - # all the assertion cells - def test_ilang(self): - dut = Driver() - vl = rtlil.convert(dut, ports=[]) - with open("bperm.il", "w") as f: - f.write(vl) - - -if __name__ == '__main__': - unittest.main() diff --git a/src/soc/fu/logical/formal/proof_bpermd.py b/src/soc/fu/logical/formal/proof_bpermd.py new file mode 100644 index 00000000..ba93a0ef --- /dev/null +++ b/src/soc/fu/logical/formal/proof_bpermd.py @@ -0,0 +1,132 @@ +# Proof of correctness for bit permute module +# Copyright (C) 2020 Michael Nolan + +from nmigen import (Module, Signal, Elaboratable, Mux, Cat, Repl, + signed) +from nmigen.asserts import Assert, AnyConst, Assume, Cover +from nmigen.test.utils import FHDLTestCase +from nmigen.cli import rtlil + +from soc.fu.logical.bpermd import Bpermd + +import unittest + + +# So formal verification is a little different than writing a test +# case, as you're actually generating logic around your module to +# check that it behaves a certain way. So here, I'm going to create a +# module to put my formal assertions in +class Driver(Elaboratable): + def __init__(self): + # We don't need any inputs and outputs here, so I won't + # declare any + pass + + def elaborate(self, platform): + # standard stuff + m = Module() + comb = m.d.comb + + # instantiate the device under test as a submodule + m.submodules.bperm = bperm = Bpermd(64) + + # Grab the inputs and outputs of the DUT to make them more + # convenient to access + rs = bperm.rs + rb = bperm.rb + ra = bperm.ra + + # Before we prove any properties about the DUT, we need to set + # up its inputs. There's a couple ways to do this, you could + # define some inputs and outputs for the driver module and + # wire them up to the DUT, but that's kind of a pain. The + # other option is to use AnyConst/AnySeq, which tells yosys + # that those inputs can take on any value. + + # AnyConst should be used when the input should take on a + # random value, but that value should be constant throughout + # the test. + # AnySeq should be used when the input can change on every + # cycle + + # Since this is a combinatorial circuit, it really doesn't + # matter which one you choose, so I chose AnyConst. If this + # was a sequential circuit, (especially a state machine) you'd + # want to use AnySeq + comb += [rs.eq(AnyConst(64)), + rb.eq(AnyConst(64))] + + # The pseudocode in the Power ISA manual (v3.1) is as follows: + # do i = 0 to 7 + # index <- RS[8*i:8*i+8] + # if index < 64: + # perm[i] <- RB[index] + # else: + # perm[i] <- 0 + # RA <- 56'b0 || perm[0:8] # big endian though + + # Looking at this, I can identify 3 properties that the bperm + # module should keep: + # 1. RA[8:64] should always equal 0 + # 2. If RB[i*8:i*8+8] >= 64 then RA[i] should equal 0 + # 3. If RB[i*8:i*8+8] < 64 then RA[i] should RS[index] + + # Now we need to Assert that the properties above hold: + + # Property 1: RA[8:64] should always equal 0 + comb += Assert(ra[8:] == 0) + # Notice how we're adding Assert to comb like it's a circuit? + # That's because it kind of is. If you run this proof and have + # yosys graph the ilang, you'll be able to see an equals + # comparison cell feeding into an assert cell + + # Now we need to prove property #2. I'm going to leave this to + # you Cole. I'd start by writing a for loop and extracting the + # 8 indices into signals. Then I'd write an if statement + # checking if the index is >= 64 (it's hardware, so use an + # m.If()). Finally, I'd add an assert that checks whether + # ra[i] is equal to 0 + for i in range(8): + index = rs[i*8:i*8+8] + with m.If(index >= 64): + comb += Assert(ra[i] == 0) + with m.Else(): + # to avoid having to create an Array of rb, + # cycle through from 0-63 on the index *whistle nonchalantly* + for j in range(64): + with m.If(index == j): + comb += Assert(ra[i] == rb[j]) + + return m + + +class TestCase(FHDLTestCase): + # This bit here is actually in charge of running the formal + # proof. It has nmigen spit out the ilang, and feeds it to + # SymbiYosys to run the proof. If the proof fails, yosys will + # generate a .vcd file showing how it was able to violate your + # assertions in proof_bperm_formal/engine_0/trace.vcd. From that + # you should be able to figure out what went wrong, and either + # correct the assertion or fix the DUT + def test_formal(self): + module = Driver() + # This runs a Bounded Model Check on the driver module + # above. What that does is it starts at some initial state, + # and steps it through `depth` cycles, checking that the + # assertions hold at every cycle. Since this is a + # combinatorial module, it only needs 1 cycle to prove + # everything. + self.assertFormal(module, mode="bmc", depth=2) + self.assertFormal(module, mode="cover", depth=2) + + # As mentioned above, you can look at the graph in yosys and see + # all the assertion cells + def test_ilang(self): + dut = Driver() + vl = rtlil.convert(dut, ports=[]) + with open("bpermd.il", "w") as f: + f.write(vl) + + +if __name__ == '__main__': + unittest.main()