Compare commits
11 Commits
Author | SHA1 | Date |
---|---|---|
Jean-François Nguyen | c90e8fc496 | 2 years ago |
Jean-François Nguyen | a3dd57ac46 | 2 years ago |
Jean-François Nguyen | 96878c73da | 2 years ago |
Jean-François Nguyen | eb314fcbf0 | 2 years ago |
Jean-François Nguyen | dfcfa3a68b | 2 years ago |
Jean-François Nguyen | be7fdd7aa6 | 2 years ago |
Jean-François Nguyen | 85a061474e | 2 years ago |
Jean-François Nguyen | f091fd1977 | 2 years ago |
Jean-François Nguyen | 139eb488cf | 2 years ago |
Jean-François Nguyen | 0d82a3d13a | 2 years ago |
Jean-François Nguyen | d611d8c5e1 | 2 years ago |
@ -0,0 +1,111 @@
|
|||||||
|
check unique --depth=15 --skip=10
|
||||||
|
check gpr --depth=15
|
||||||
|
#check cia --depth=15
|
||||||
|
check causal --depth=15
|
||||||
|
|
||||||
|
check insn:add --depth=15
|
||||||
|
check insn:add_ --depth=15
|
||||||
|
check insn:addc --depth=15
|
||||||
|
check insn:addc_ --depth=15
|
||||||
|
check insn:adde --depth=15
|
||||||
|
check insn:adde_ --depth=15
|
||||||
|
check insn:addex --depth=15
|
||||||
|
check insn:addi --depth=15
|
||||||
|
check insn:addic --depth=15
|
||||||
|
check insn:addic_ --depth=15
|
||||||
|
check insn:addis --depth=15
|
||||||
|
check insn:addme --depth=15
|
||||||
|
check insn:addme_ --depth=15
|
||||||
|
check insn:addze --depth=15
|
||||||
|
check insn:addze_ --depth=15
|
||||||
|
check insn:neg --depth=15
|
||||||
|
check insn:neg_ --depth=15
|
||||||
|
check insn:subf --depth=15
|
||||||
|
check insn:subf_ --depth=15
|
||||||
|
check insn:subfc --depth=15
|
||||||
|
check insn:subfc_ --depth=15
|
||||||
|
check insn:subfe --depth=15
|
||||||
|
check insn:subfe_ --depth=15
|
||||||
|
check insn:subfic --depth=15
|
||||||
|
check insn:subfme --depth=15
|
||||||
|
check insn:subfme_ --depth=15
|
||||||
|
check insn:subfze --depth=15
|
||||||
|
check insn:subfze_ --depth=15
|
||||||
|
|
||||||
|
check insn:and --depth=15
|
||||||
|
check insn:and_ --depth=15
|
||||||
|
check insn:andc --depth=15
|
||||||
|
check insn:andc_ --depth=15
|
||||||
|
check insn:andi_ --depth=15
|
||||||
|
check insn:andis_ --depth=15
|
||||||
|
check insn:eqv --depth=15
|
||||||
|
check insn:eqv_ --depth=15
|
||||||
|
check insn:nand --depth=15
|
||||||
|
check insn:nand_ --depth=15
|
||||||
|
check insn:nor --depth=15
|
||||||
|
check insn:nor_ --depth=15
|
||||||
|
check insn:or --depth=15
|
||||||
|
check insn:or_ --depth=15
|
||||||
|
check insn:orc --depth=15
|
||||||
|
check insn:orc_ --depth=15
|
||||||
|
check insn:ori --depth=15
|
||||||
|
check insn:oris --depth=15
|
||||||
|
check insn:xor --depth=15
|
||||||
|
check insn:xor_ --depth=15
|
||||||
|
check insn:xori --depth=15
|
||||||
|
check insn:xoris --depth=15
|
||||||
|
|
||||||
|
check insn:brh --depth=15
|
||||||
|
check insn:brw --depth=15
|
||||||
|
check insn:extsb --depth=15
|
||||||
|
check insn:extsb_ --depth=15
|
||||||
|
check insn:extsh --depth=15
|
||||||
|
check insn:extsh_ --depth=15
|
||||||
|
|
||||||
|
check insn:crand --depth=15
|
||||||
|
check insn:crandc --depth=15
|
||||||
|
check insn:creqv --depth=15
|
||||||
|
check insn:crnand --depth=15
|
||||||
|
check insn:crnor --depth=15
|
||||||
|
check insn:cror --depth=15
|
||||||
|
check insn:crorc --depth=15
|
||||||
|
check insn:crxor --depth=15
|
||||||
|
|
||||||
|
check insn:mcrf --depth=15
|
||||||
|
|
||||||
|
check insn:b --depth=15
|
||||||
|
check insn:ba --depth=15
|
||||||
|
|
||||||
|
check insn:cmpi --depth=15
|
||||||
|
check insn:cmpli --depth=15
|
||||||
|
check insn:cmp --depth=15
|
||||||
|
check insn:cmpl --depth=15
|
||||||
|
|
||||||
|
check insn:lbz --depth=15
|
||||||
|
check insn:lbzx --depth=15
|
||||||
|
check insn:lha --depth=15
|
||||||
|
check insn:lhax --depth=15
|
||||||
|
check insn:lhz --depth=15
|
||||||
|
check insn:lhzx --depth=15
|
||||||
|
check insn:lwz --depth=15
|
||||||
|
check insn:lwbrx --depth=15
|
||||||
|
check insn:stb --depth=15
|
||||||
|
check insn:sth --depth=15
|
||||||
|
check insn:stw --depth=15
|
||||||
|
|
||||||
|
check insn:rlwimi --depth=15
|
||||||
|
check insn:rlwimi_ --depth=15
|
||||||
|
check insn:rlwinm --depth=15
|
||||||
|
check insn:rlwinm_ --depth=15
|
||||||
|
check insn:rlwnm --depth=15
|
||||||
|
check insn:rlwnm_ --depth=15
|
||||||
|
check insn:slw --depth=15
|
||||||
|
check insn:slw_ --depth=15
|
||||||
|
check insn:sraw --depth=15
|
||||||
|
check insn:sraw_ --depth=15
|
||||||
|
check insn:srawi --depth=15
|
||||||
|
check insn:srawi_ --depth=15
|
||||||
|
check insn:srw --depth=15
|
||||||
|
check insn:srw_ --depth=15
|
||||||
|
|
||||||
|
build --build-dir=./build
|
@ -0,0 +1,14 @@
|
|||||||
|
from pathlib import PurePath
|
||||||
|
from power_fv.session import PowerFVSession
|
||||||
|
|
||||||
|
from .core import DinoflyCore
|
||||||
|
from .check.storage import *
|
||||||
|
|
||||||
|
|
||||||
|
class DinoflySession(PowerFVSession, core_cls=DinoflyCore):
|
||||||
|
pass
|
||||||
|
|
||||||
|
|
||||||
|
if __name__ == "__main__":
|
||||||
|
PROG = "python -m {}".format(PurePath(__file__).parent.name)
|
||||||
|
DinoflySession().main(prog=PROG)
|
@ -0,0 +1,166 @@
|
|||||||
|
from amaranth import *
|
||||||
|
from amaranth.asserts import *
|
||||||
|
from amaranth.utils import log2_int
|
||||||
|
|
||||||
|
from amaranth_soc import wishbone
|
||||||
|
|
||||||
|
from power_fv.check.storage import *
|
||||||
|
|
||||||
|
from ..core import *
|
||||||
|
|
||||||
|
|
||||||
|
__all__ = [
|
||||||
|
"InsnStorageCheck_Dinofly", "InsnStorageTestbench_Dinofly", "InsnStorageModel_Dinofly",
|
||||||
|
"DataStorageCheck_Dinofly", "DataStorageTestbench_Dinofly", "DataStorageModel_Dinofly",
|
||||||
|
]
|
||||||
|
|
||||||
|
|
||||||
|
class InsnStorageCheck_Dinofly(InsnStorageCheck, name=("dinofly", "storage", "insn")):
|
||||||
|
def __init__(self, *, depth, skip, core, **kwargs):
|
||||||
|
if not isinstance(core, DinoflyCore):
|
||||||
|
raise TypeError("Core must be an instance of DinoflyCore, not {!r}"
|
||||||
|
.format(core))
|
||||||
|
super().__init__(depth=depth, skip=skip, core=core, **kwargs)
|
||||||
|
|
||||||
|
def testbench(self):
|
||||||
|
return InsnStorageTestbench_Dinofly(self)
|
||||||
|
|
||||||
|
|
||||||
|
class InsnStorageTestbench_Dinofly(InsnStorageTestbench):
|
||||||
|
def __init__(self, check):
|
||||||
|
if not isinstance(check, InsnStorageCheck_Dinofly):
|
||||||
|
raise TypeError("Check must be an instance of InsnStorageCheck_Dinofly, not {!r}"
|
||||||
|
.format(check))
|
||||||
|
super().__init__(check)
|
||||||
|
|
||||||
|
def storage(self):
|
||||||
|
return InsnStorageModel_Dinofly(
|
||||||
|
ibus_addr_width=self.check.dut.ibus.addr_width,
|
||||||
|
ibus_data_width=self.check.dut.ibus.data_width,
|
||||||
|
ibus_granularity=self.check.dut.ibus.granularity,
|
||||||
|
)
|
||||||
|
|
||||||
|
|
||||||
|
class InsnStorageModel_Dinofly(InsnStorageModel, Elaboratable):
|
||||||
|
def __init__(self, *, ibus_addr_width=30, ibus_data_width=32, ibus_granularity=8):
|
||||||
|
self.addr = Signal(64)
|
||||||
|
self.data = Signal(32)
|
||||||
|
self._ibus = wishbone.Interface(addr_width=ibus_addr_width, data_width=ibus_data_width,
|
||||||
|
granularity=ibus_granularity)
|
||||||
|
|
||||||
|
def connect(self, dut):
|
||||||
|
assert isinstance(dut, DinoflyWrapper)
|
||||||
|
assert dut.ibus.addr_width == self._ibus.addr_width
|
||||||
|
assert dut.ibus.data_width == self._ibus.data_width
|
||||||
|
assert dut.ibus.granularity == self._ibus.granularity
|
||||||
|
|
||||||
|
return self._ibus.eq(dut.ibus)
|
||||||
|
|
||||||
|
def elaborate(self, platform):
|
||||||
|
m = Module()
|
||||||
|
|
||||||
|
with m.If(self._ibus.ack):
|
||||||
|
m.d.comb += [
|
||||||
|
Assume(self._ibus.cyc & Past(self._ibus.cyc)),
|
||||||
|
Assume(self._ibus.stb & Past(self._ibus.stb)),
|
||||||
|
Assume(~Past(self._ibus.ack)),
|
||||||
|
]
|
||||||
|
|
||||||
|
gran_bits = log2_int(self._ibus.data_width // self._ibus.granularity)
|
||||||
|
|
||||||
|
m.d.comb += [
|
||||||
|
self.addr.eq(AnyConst(self._ibus.addr_width + gran_bits)),
|
||||||
|
self.data.eq(AnyConst(32)),
|
||||||
|
]
|
||||||
|
|
||||||
|
with m.If(self._ibus.cyc & self._ibus.stb & self._ibus.ack & ~ResetSignal("sync")):
|
||||||
|
if self._ibus.data_width == 32:
|
||||||
|
with m.If(self.addr == Cat(Const(0b00, 2), self._ibus.adr)):
|
||||||
|
m.d.comb += Assume(self._ibus.dat_r == self.data)
|
||||||
|
elif self._ibus.data_width == 64:
|
||||||
|
with m.If(self.addr == Cat(Const(0b000, 3), self._ibus.adr)):
|
||||||
|
m.d.comb += Assume(self._ibus.dat_r[:32] == self.data)
|
||||||
|
with m.If(self.addr == Cat(Const(0b100, 3), self._ibus.adr)):
|
||||||
|
m.d.comb += Assume(self._ibus.dat_r[32:] == self.data)
|
||||||
|
else:
|
||||||
|
assert False
|
||||||
|
|
||||||
|
return m
|
||||||
|
|
||||||
|
|
||||||
|
class DataStorageCheck_Dinofly(DataStorageCheck, name=("dinofly", "storage", "data")):
|
||||||
|
def __init__(self, *, depth, skip, core, **kwargs):
|
||||||
|
if not isinstance(core, DinoflyCore):
|
||||||
|
raise TypeError("Core must be an instance of DinoflyCore, not {!r}"
|
||||||
|
.format(core))
|
||||||
|
super().__init__(depth=depth, skip=skip, core=core, **kwargs)
|
||||||
|
|
||||||
|
def testbench(self):
|
||||||
|
return DataStorageTestbench_Dinofly(self)
|
||||||
|
|
||||||
|
|
||||||
|
class DataStorageTestbench_Dinofly(DataStorageTestbench):
|
||||||
|
def __init__(self, check):
|
||||||
|
if not isinstance(check, DataStorageCheck_Dinofly):
|
||||||
|
raise TypeError("Check must be an instance of DataStorageCheck_Dinofly, not {!r}"
|
||||||
|
.format(check))
|
||||||
|
super().__init__(check)
|
||||||
|
|
||||||
|
def storage(self):
|
||||||
|
return DataStorageModel_Dinofly(
|
||||||
|
dbus_addr_width=self.check.dut.dbus.addr_width,
|
||||||
|
dbus_data_width=self.check.dut.dbus.data_width,
|
||||||
|
dbus_granularity=self.check.dut.dbus.granularity,
|
||||||
|
)
|
||||||
|
|
||||||
|
|
||||||
|
class DataStorageModel_Dinofly(DataStorageModel, Elaboratable):
|
||||||
|
def __init__(self, *, dbus_addr_width=30, dbus_data_width=32, dbus_granularity=8):
|
||||||
|
self.addr = Signal(64)
|
||||||
|
self._dbus = wishbone.Interface(addr_width=dbus_addr_width, data_width=dbus_data_width,
|
||||||
|
granularity=dbus_granularity)
|
||||||
|
|
||||||
|
def connect(self, dut):
|
||||||
|
assert isinstance(dut, DinoflyWrapper)
|
||||||
|
assert dut.dbus.addr_width == self._dbus.addr_width
|
||||||
|
assert dut.dbus.data_width == self._dbus.data_width
|
||||||
|
assert dut.dbus.granularity == self._dbus.granularity
|
||||||
|
|
||||||
|
return self._dbus.eq(dut.dbus)
|
||||||
|
|
||||||
|
def elaborate(self, platform):
|
||||||
|
m = Module()
|
||||||
|
|
||||||
|
dbus_read = Signal()
|
||||||
|
dbus_write = Signal()
|
||||||
|
|
||||||
|
m.d.comb += [
|
||||||
|
dbus_read .eq(self._dbus.cyc & self._dbus.stb & self._dbus.ack),
|
||||||
|
dbus_write.eq(self._dbus.cyc & self._dbus.stb & self._dbus.ack & self._dbus.we),
|
||||||
|
]
|
||||||
|
|
||||||
|
with m.If(self._dbus.ack):
|
||||||
|
m.d.comb += [
|
||||||
|
Assume(self._dbus.cyc & Past(self._dbus.cyc)),
|
||||||
|
Assume(self._dbus.stb & Past(self._dbus.stb)),
|
||||||
|
Assume(~Past(self._dbus.ack)),
|
||||||
|
]
|
||||||
|
|
||||||
|
gran_bits = log2_int(self._dbus.data_width // self._dbus.granularity)
|
||||||
|
addr_hit = Signal()
|
||||||
|
value = Signal(self._dbus.data_width)
|
||||||
|
|
||||||
|
m.d.comb += [
|
||||||
|
self.addr.eq(AnyConst(self._dbus.addr_width + gran_bits)),
|
||||||
|
addr_hit .eq(self._dbus.adr == self.addr[gran_bits:]),
|
||||||
|
]
|
||||||
|
|
||||||
|
with m.If(dbus_read & addr_hit & ~ResetSignal("sync")):
|
||||||
|
m.d.comb += Assume(self._dbus.dat_r == value)
|
||||||
|
|
||||||
|
with m.If(dbus_write & addr_hit):
|
||||||
|
for i, sel_bit in enumerate(self._dbus.sel):
|
||||||
|
with m.If(sel_bit):
|
||||||
|
m.d.sync += value[i*8:i*8+8].eq(self._dbus.dat_w[i*8:i*8+8])
|
||||||
|
|
||||||
|
return m
|
@ -0,0 +1,40 @@
|
|||||||
|
from amaranth import *
|
||||||
|
from amaranth.asserts import *
|
||||||
|
|
||||||
|
from dinofly.core import DinoflyCPU
|
||||||
|
|
||||||
|
from power_fv.core import PowerFVCore
|
||||||
|
|
||||||
|
|
||||||
|
__all__ = ["DinoflyWrapper"]
|
||||||
|
|
||||||
|
|
||||||
|
class DinoflyWrapper(Elaboratable):
|
||||||
|
def __init__(self, **kwargs):
|
||||||
|
self._cpu = DinoflyCPU(with_pfv=True)
|
||||||
|
self.pfv = self._cpu.pfv
|
||||||
|
self.ibus = self._cpu.ibus
|
||||||
|
self.dbus = self._cpu.dbus
|
||||||
|
|
||||||
|
def elaborate(self, platform):
|
||||||
|
m = Module()
|
||||||
|
|
||||||
|
m.submodules.cpu = self._cpu
|
||||||
|
|
||||||
|
m.d.comb += [
|
||||||
|
self.ibus.dat_r.eq(AnySeq(self.ibus.data_width)),
|
||||||
|
self.ibus.ack .eq(AnySeq(1)),
|
||||||
|
self.ibus.err .eq(AnySeq(1)),
|
||||||
|
|
||||||
|
self.dbus.dat_r.eq(AnySeq(self.dbus.data_width)),
|
||||||
|
self.dbus.ack .eq(AnySeq(1)),
|
||||||
|
self.dbus.err .eq(AnySeq(1)),
|
||||||
|
]
|
||||||
|
|
||||||
|
return m
|
||||||
|
|
||||||
|
|
||||||
|
class DinoflyCore(PowerFVCore):
|
||||||
|
@classmethod
|
||||||
|
def wrapper(cls, **kwargs):
|
||||||
|
return DinoflyWrapper(**kwargs)
|
Loading…
Reference in New Issue