src/soc/minerva/units/rvficon.py

   1 from functools import reduce
   2 from operator import or_
   3
   4 from nmigen import Elaboratable, Module, Signal, Record, Const
   5 from nmigen.hdl.rec import DIR_FANOUT
   6
   7 from ..wishbone import wishbone_layout
   8
   9
  10 __all__ = ["rvfi_layout", "RVFIController"]
  11
  12 # RISC-V Formal Interface
  13 # https://github.com/SymbioticEDA/riscv-formal/blob/master/docs/rvfi.md
  14
  15 rvfi_layout = [
  16     ("valid",      1, DIR_FANOUT),
  17     ("order",     64, DIR_FANOUT),
  18     ("insn",      32, DIR_FANOUT),
  19     ("trap",       1, DIR_FANOUT),
  20     ("halt",       1, DIR_FANOUT),
  21     ("intr",       1, DIR_FANOUT),
  22     ("mode",       2, DIR_FANOUT),
  23     ("ixl",        2, DIR_FANOUT),
  24
  25     ("rs1_addr",   5, DIR_FANOUT),
  26     ("rs2_addr",   5, DIR_FANOUT),
  27     ("rs1_rdata", 32, DIR_FANOUT),
  28     ("rs2_rdata", 32, DIR_FANOUT),
  29     ("rd_addr",    5, DIR_FANOUT),
  30     ("rd_wdata",  32, DIR_FANOUT),
  31
  32     ("pc_rdata",  32, DIR_FANOUT),
  33     ("pc_wdata",  32, DIR_FANOUT),
  34
  35     ("mem_addr",  32, DIR_FANOUT),
  36     ("mem_rmask",  4, DIR_FANOUT),
  37     ("mem_wmask",  4, DIR_FANOUT),
  38     ("mem_rdata", 32, DIR_FANOUT),
  39     ("mem_wdata", 32, DIR_FANOUT)
  40 ]
  41
  42
  43 class RVFIController(Elaboratable):
  44     def __init__(self):
  45         self.rvfi               = Record(rvfi_layout)
  46
  47         self.d_insn             = Signal.like(self.rvfi.insn)
  48         self.d_rs1_addr         = Signal.like(self.rvfi.rs1_addr)
  49         self.d_rs2_addr         = Signal.like(self.rvfi.rs2_addr)
  50         self.d_rs1_rdata        = Signal.like(self.rvfi.rs1_rdata)
  51         self.d_rs2_rdata        = Signal.like(self.rvfi.rs2_rdata)
  52         self.d_stall            = Signal()
  53         self.x_mem_addr         = Signal.like(self.rvfi.mem_addr)
  54         self.x_mem_wmask        = Signal.like(self.rvfi.mem_wmask)
  55         self.x_mem_rmask        = Signal.like(self.rvfi.mem_rmask)
  56         self.x_mem_wdata        = Signal.like(self.rvfi.mem_wdata)
  57         self.x_stall            = Signal()
  58         self.m_mem_rdata        = Signal.like(self.rvfi.mem_rdata)
  59         self.m_fetch_misaligned = Signal()
  60         self.m_illegal_insn     = Signal()
  61         self.m_load_misaligned  = Signal()
  62         self.m_store_misaligned = Signal()
  63         self.m_exception        = Signal()
  64         self.m_mret             = Signal()
  65         self.m_branch_taken     = Signal()
  66         self.m_branch_target    = Signal(32)
  67         self.m_pc_rdata         = Signal.like(self.rvfi.pc_rdata)
  68         self.m_stall            = Signal()
  69         self.m_valid            = Signal()
  70         self.w_rd_addr          = Signal.like(self.rvfi.rd_addr)
  71         self.w_rd_wdata         = Signal.like(self.rvfi.rd_wdata)
  72
  73         self.mtvec_r_base       = Signal(30)
  74         self.mepc_r_value       = Signal(32)
  75
  76     def elaborate(self, platform):
  77         m = Module()
  78
  79         # Instruction Metadata
  80
  81         with m.If(~self.m_stall):
  82             m.d.sync += self.rvfi.valid.eq(self.m_valid)
  83         with m.Elif(self.rvfi.valid):
  84             m.d.sync += self.rvfi.valid.eq(0)
  85
  86         with m.If(self.rvfi.valid):
  87             m.d.sync += self.rvfi.order.eq(self.rvfi.order + 1)
  88
  89         x_insn = Signal.like(self.rvfi.insn)
  90         m_insn = Signal.like(self.rvfi.insn)
  91
  92         with m.If(~self.d_stall):
  93             m.d.sync += x_insn.eq(self.d_insn)
  94         with m.If(~self.x_stall):
  95             m.d.sync += m_insn.eq(x_insn)
  96         with m.If(~self.m_stall):
  97             m.d.sync += self.rvfi.insn.eq(m_insn)
  98
  99         with m.If(~self.m_stall):
 100             m.d.sync += [
 101                 self.rvfi.trap.eq(reduce(or_, (
 102                     self.m_fetch_misaligned,
 103                     self.m_illegal_insn,
 104                     self.m_load_misaligned,
 105                     self.m_store_misaligned
 106                 ))),
 107                 self.rvfi.intr.eq(self.m_pc_rdata == self.mtvec_r_base << 2)
 108             ]
 109
 110         m.d.comb += [
 111             self.rvfi.mode.eq(Const(3)), # M-mode
 112             self.rvfi.ixl.eq(Const(1)) # XLEN=32
 113         ]
 114
 115         # Integer Register Read/Write
 116
 117         x_rs1_addr  = Signal.like(self.rvfi.rs1_addr)
 118         x_rs2_addr  = Signal.like(self.rvfi.rs2_addr)
 119         x_rs1_rdata = Signal.like(self.rvfi.rs1_rdata)
 120         x_rs2_rdata = Signal.like(self.rvfi.rs2_rdata)
 121
 122         m_rs1_addr  = Signal.like(self.rvfi.rs1_addr)
 123         m_rs2_addr  = Signal.like(self.rvfi.rs2_addr)
 124         m_rs1_rdata = Signal.like(self.rvfi.rs1_rdata)
 125         m_rs2_rdata = Signal.like(self.rvfi.rs2_rdata)
 126
 127         with m.If(~self.d_stall):
 128             m.d.sync += [
 129                 x_rs1_addr.eq(self.d_rs1_addr),
 130                 x_rs2_addr.eq(self.d_rs2_addr),
 131                 x_rs1_rdata.eq(self.d_rs1_rdata),
 132                 x_rs2_rdata.eq(self.d_rs2_rdata)
 133             ]
 134         with m.If(~self.x_stall):
 135             m.d.sync += [
 136                 m_rs1_addr.eq(x_rs1_addr),
 137                 m_rs2_addr.eq(x_rs2_addr),
 138                 m_rs1_rdata.eq(x_rs1_rdata),
 139                 m_rs2_rdata.eq(x_rs2_rdata)
 140             ]
 141         with m.If(~self.m_stall):
 142             m.d.sync += [
 143                 self.rvfi.rs1_addr.eq(m_rs1_addr),
 144                 self.rvfi.rs2_addr.eq(m_rs2_addr),
 145                 self.rvfi.rs1_rdata.eq(m_rs1_rdata),
 146                 self.rvfi.rs2_rdata.eq(m_rs2_rdata)
 147             ]
 148
 149         m.d.comb += [
 150             self.rvfi.rd_addr.eq(self.w_rd_addr),
 151             self.rvfi.rd_wdata.eq(self.w_rd_wdata)
 152         ]
 153
 154         # Program Counter
 155
 156         m_pc_wdata = Signal.like(self.rvfi.pc_wdata)
 157
 158         with m.If(self.m_exception):
 159             m.d.comb += m_pc_wdata.eq(self.mtvec_r_base << 2)
 160         with m.Elif(self.m_mret):
 161             m.d.comb += m_pc_wdata.eq(self.mepc_r_value)
 162         with m.Elif(self.m_branch_taken):
 163             m.d.comb += m_pc_wdata.eq(self.m_branch_target)
 164         with m.Else():
 165             m.d.comb += m_pc_wdata.eq(self.m_pc_rdata + 4)
 166
 167         with m.If(~self.m_stall):
 168             m.d.sync += [
 169                 self.rvfi.pc_rdata.eq(self.m_pc_rdata),
 170                 self.rvfi.pc_wdata.eq(m_pc_wdata)
 171             ]
 172
 173         # Memory Access
 174
 175         m_mem_addr  = Signal.like(self.rvfi.mem_addr)
 176         m_mem_wmask = Signal.like(self.rvfi.mem_wmask)
 177         m_mem_rmask = Signal.like(self.rvfi.mem_rmask)
 178         m_mem_wdata = Signal.like(self.rvfi.mem_wdata)
 179
 180         with m.If(~self.x_stall):
 181             m.d.sync += [
 182                 m_mem_addr.eq(self.x_mem_addr),
 183                 m_mem_wmask.eq(self.x_mem_wmask),
 184                 m_mem_rmask.eq(self.x_mem_rmask),
 185                 m_mem_wdata.eq(self.x_mem_wdata)
 186             ]
 187         with m.If(~self.m_stall):
 188             m.d.sync += [
 189                 self.rvfi.mem_addr.eq(m_mem_addr),
 190                 self.rvfi.mem_wmask.eq(m_mem_wmask),
 191                 self.rvfi.mem_rmask.eq(m_mem_rmask),
 192                 self.rvfi.mem_wdata.eq(m_mem_wdata),
 193                 self.rvfi.mem_rdata.eq(self.m_mem_rdata)
 194             ]
 195
 196         return m