src/ieee754/fsgnj/formal/proof_fsgnj_mod.py

   1 # Proof of correctness for FSGNJ module
   2 # Copyright (C) 2020 Michael Nolan <mtnolan2640@gmail.com>
   3
   4 from nmigen import Module, Signal, Elaboratable
   5 from nmigen.asserts import Assert, Assume
   6 from nmigen.cli import rtlil
   7
   8 from ieee754.fsgnj.fsgnj import FSGNJPipeMod
   9 from ieee754.pipeline import PipelineSpec
  10 import subprocess
  11
  12
  13 # This defines a module to drive the device under test and assert
  14 # properties about its outputs
  15 class FSGNJDriver(Elaboratable):
  16     def __init__(self, pspec):
  17         # inputs and outputs
  18         self.pspec = pspec
  19         self.a = Signal(pspec.width)
  20         self.b = Signal(pspec.width)
  21         self.z = Signal(pspec.width)
  22         self.opc = Signal(pspec.op_wid)
  23         self.muxid = Signal(pspec.id_wid)
  24
  25     def elaborate(self, platform):
  26         m = Module()
  27
  28         m.submodules.dut = dut = FSGNJPipeMod(self.pspec)
  29
  30         # connect up the inputs and outputs. I think these could
  31         # theoretically be $anyconst/$anysync but I'm not sure nmigen
  32         # has support for that
  33         m.d.comb += dut.i.a.eq(self.a)
  34         m.d.comb += dut.i.b.eq(self.b)
  35         m.d.comb += dut.i.ctx.op.eq(self.opc)
  36         m.d.comb += dut.i.muxid.eq(self.muxid)
  37         m.d.comb += self.z.eq(dut.o.z)
  38
  39         # Since the RISCV spec doesn't define what FSGNJ with a funct3
  40         # field of 0b011 throug 0b111 does, they should be ignored.
  41         m.d.comb += Assume(self.opc != 0b11)
  42
  43         # The RISCV spec (page 70) says FSGNJ "produces a result that
  44         # takes all buts except the sign bit from [operand 1]". This
  45         # asserts that that holds true
  46         m.d.comb += Assert(self.z[0:31] == self.a[0:31])
  47
  48         with m.Switch(self.opc):
  49
  50             # The RISCV Spec (page 70) states that for FSGNJ (opcode
  51             # 0b00 in this case) "the result's sign bit is [operand
  52             # 2's] sign bit"
  53             with m.Case(0b00):
  54                 m.d.comb += Assert(self.z[-1] == self.b[-1])
  55
  56             # The RISCV Spec (page 70) states that for FSGNJN (opcode
  57             # 0b01 in this case) "the result's sign bit is the opposite
  58             # of [operand 2's] sign bit"
  59             with m.Case(0b01):
  60                 m.d.comb += Assert(self.z[-1] == ~self.b[-1])
  61             # The RISCV Spec (page 70) states that for FSGNJX (opcode
  62             # 0b10 in this case) "the result's sign bit is the XOR of
  63             # the sign bits of [operand 1] and [operand 2]"
  64             with m.Case(0b10):
  65                 m.d.comb += Assert(self.z[-1] == (self.a[-1] ^ self.b[-1]))
  66
  67         return m
  68
  69     def ports(self):
  70         return [self.a, self.b, self.z, self.opc, self.muxid]
  71
  72
  73 def run_test():
  74     m = FSGNJDriver(PipelineSpec(32, 2, 2))
  75
  76     il = rtlil.convert(m, ports=m.ports())
  77     with open("proof.il", "w") as f:
  78         f.write(il)
  79     p = subprocess.Popen(['sby', '-f', 'proof.sby'],
  80                          stdout=subprocess.PIPE,
  81                          stderr=subprocess.PIPE)
  82     if p.wait() == 0:
  83         out, err = p.communicate()
  84         print("Proof successful!")
  85         print(out.decode('utf-8'))
  86     else:
  87         print("Proof failed")
  88         out, err = p.communicate()
  89         print(out.decode('utf-8'))
  90         print(err.decode('utf-8'))
  91
  92
  93 if __name__ == "__main__":
  94     run_test()