Artifact [87d2fd007e]

Artifact 87d2fd007e0169426ef2a2fee413edef2325572f08d9842185812be44337c867:

#!/usr/bin/env python
# Implements the tests for the add/store unit.  The add/store unit
# consists of two halves: the function unit (FU) and the computation
# unit (CU).

import inspect

from import FHDLTestCase
from nmigen.back.pysim import Simulator, Delay
from nmigen import (
    Signal, Module, ClockDomain, Elaboratable, ResetSignal, Const, Repl, Cat,
from nmigen.hdl.ast import Assume, Past, Assert, Stable, Rose, Fell

SRC2_IMM12 = 0
SRC2_REG2 = 1
SRC2_unused = 2

def create_cu_interface(self, xlen=64, fumax=7, xmax=31):
    """Creates the computation unit interface for the add/store unit.

    If specified, xlen specifies the maximum register width.  If not
    specified, xlen defaults to 64.

    If specified, fumax specifies the largest integer that can
    uniquely identify a FU.  If not specified, fumax defaults to 7.

    xmax specifies the highest addressable X-register.  If left
    unspecified, this defaults to 31.  Don't change this unless you
    know exactly what you're doing!

    # The following signals come from the corresponding function unit.

    self.i_go_write = Signal()
    self.i_go_sum = Signal()
    self.i_inst_src2 = Signal(min=0, max=SRC2_NOT_REG2)
    self.i_inst_imm12 = Signal(min=-2048, max=2047)
    self.i_inst_cin = Signal(1)

    # The following come from the "trunk" (really, the register file).

    self.i_trunk_data1 = Signal(xlen)
    self.i_trunk_data2 = Signal(xlen)
    self.o_trunk_data = Signal(xlen)

    # The following are diagnostic outputs only.

    self.o_fv_addend1 = Signal(xlen)
    self.o_fv_addend2 = Signal(xlen)
    self.o_fv_ea = Signal(xlen)
    self.o_fv_src2 = Signal(self.i_inst_src2.nbits)
    self.o_fv_imm12 = Signal(self.i_inst_imm12.nbits)
    self.o_fv_cin = Signal(self.i_inst_cin.nbits)

class AddStoreCU(Elaboratable):
    """Implements the data flow logic for one add/store unit.  See also
    the AddStoreFU class for the function unit that drives instances
    of this class.

    NOTE: All signals in the fv_ bus are reserved for external formal
    verification.  DO NOT use these signals for production purposes.

    def __init__(self):
        Instantiates a new add/store computation unit.


    def elaborate(self, platform):
        m = Module()
        comb = m.d.comb
        sync = m.d.sync

        xlen = self.o_trunk_data.nbits

        # The 2nd addend to the adder can be taken from one of three
        # sources, as set by the instruction's src2 bits.

        addend2 = Signal(xlen)

        comb += [

        with m.If(self.i_inst_src2 == SRC2_IMM12):
            comb += addend2.eq(Cat(
                Repl(self.i_inst_imm12[11], xlen-12)

        with m.If(self.i_inst_src2 == SRC2_REG2):
            comb += addend2.eq(self.i_trunk_data2)

        with m.If(self.i_inst_src2 == SRC2_NOT_REG2):
            comb += addend2.eq(~self.i_trunk_data2)

        # The adder passively produces a sum from its two inputs.

        sum = Signal(xlen)
        comb += [
                (self.i_trunk_data1 + addend2 + self.i_inst_cin)[0:xlen]

        # The adder places its results in the effective address
        # register, reg_ea.

        reg_ea = Signal(xlen)

        with m.If(self.i_go_sum):
            sync += reg_ea.eq(sum)

        comb += self.o_fv_ea.eq(reg_ea)

        # If we don't have permission to drive the trunk, then make
        # sure we don't drive it.  In an FPGA, at least, the trunk
        # is implemented using a giant OR network, so that means a
        # quiet trunk is a zero trunk.

        comb += [
                reg_ea & Repl(self.i_go_write, self.o_trunk_data.nbits)

        return m

class AddStoreCUFormal(Elaboratable):
    def __init__(self):

    def elaborate(self, platform):
        m = Module()
        sync = m.d.sync
        comb = m.d.comb

        dut = AddStoreCU()
        m.submodules.dut = dut
        comb += [



        xlen = self.o_trunk_data.nbits

        # Create a flag that helps prevent making assertions and
        # assumptions that spans before simulation time began.

        z_past_valid = Signal(1, reset=0)
        sync += z_past_valid.eq(1)

        # Everything must be reset before we can do anything else.

        rst = ResetSignal()
        with m.If(~z_past_valid):
            sync += Assume(rst)

        # The first addend of the adder should always reflect the
        # first source register on the trunk.

        comb += Assert(self.o_fv_addend1 == self.i_trunk_data1)

        # The second addend depends on the precise instruction
        # being executed.  For ADDI and store instructions,
        # the immediate input should be reflected.  For ADD
        # instructions, it should come from the second source
        # register.  Additionally, if being taken from the 2nd
        # source register, it may optionally be inverted so as
        # to effect a subtraction.

        with m.If(self.o_fv_src2 == SRC2_IMM12):
            comb += [
                Assert(self.o_fv_addend2[0:12] == self.o_fv_imm12),
                    self.o_fv_addend2[12:xlen] == Repl(self.o_fv_imm12[11], xlen-12)

        with m.If(self.o_fv_src2 == SRC2_REG2):
            comb += Assert(self.o_fv_addend2 == self.i_trunk_data2)

        with m.If(self.o_fv_src2 == SRC2_NOT_REG2):
            comb += Assert(self.o_fv_addend2 == ~self.i_trunk_data2)

        with m.If(self.o_fv_src2 == SRC2_unused):
            comb += Assert(self.o_fv_addend2 == Const(0, xlen))

        # If GO_SUM is asserted, then the sum computed by the
        # adder must be preserved.  We don't really care about
        # 32-bit sign extension here, as that'll be located at
        # the register file data input.

        with m.If(z_past_valid & Stable(rst) & ~rst & Past(self.i_go_sum)):
            sync += [
                    self.o_fv_ea == (
                        Past(self.o_fv_addend1) +
                        Past(self.o_fv_addend2) +

        with m.If(z_past_valid & Stable(rst) & ~rst & ~Past(self.i_go_sum)):
            sync += Assert(Stable(self.o_fv_ea))

        # If GO_WRITE is negated, then we don't drive the trunk.

        with m.If(z_past_valid & Stable(rst) & ~rst & ~self.i_go_write):
            sync += [
                Assert(self.o_trunk_data == Const(0, xlen)),

        # If GO_WRITE is asserted, however, we must drive the trunk.

        with m.If(z_past_valid & Stable(rst) & ~rst & self.i_go_write):
            sync += [
                Assert(self.o_trunk_data == self.o_fv_ea),

        return m

class AddStoreCUTestCase(FHDLTestCase):

    # "P"eriod -- how long the clock is high or low.  You might not
    # think so, but for my wretched joints, I find typing "self.P"
    # easier than "10e-9" all the time.
    P = 10e-9

    def stdfiles(self):
        """Opens correctly named VCD and GTKWave files for writing."""

        caller = inspect.currentframe().f_back.f_code.co_name
        return {
            'vcd_file': open("{}.vcd".format(caller), "w"),
            'gtkw_file': open("{}.gtkw".format(caller), "w"),

    def setup_cu(self, reset_pc=0):
        ports = [
        ports = [self.__getattribute__(p) for p in ports]

        self.dut = AddStoreCU()
        self.m = Module()
        self.sync = ClockDomain() += self.sync
        self.m.submodules += self.dut

        self.m.d.comb += [

        return ports

    def tick(self):
        yield self.sync.clk.eq(1)
        yield Delay(self.P)
        yield self.sync.clk.eq(0)
        yield Delay(self.P)

    def reset(self):
        yield self.sync.rst.eq(1)
        yield from self.tick()
        yield self.sync.rst.eq(0)
        yield from self.tick()

    def test_add_store_cu_formally(self):
        self.assertFormal(AddStoreCUFormal(), mode="bmc", depth=100)
        self.assertFormal(AddStoreCUFormal(), mode="prove", depth=100)

    #def test_idle_state(self):
    #    traces = self.setup_cu()
    #    with Simulator(
    #        self.m.elaborate(platform=None), traces=traces, **(self.stdfiles())
    #    ) as sim:
    #        def process():
    #            yield from self.reset()
    #            self.assertEqual((yield self.o_trunk_rd), 0)
    #            self.assertEqual((yield self.o_trunk_rd_dat), 0)
    #            self.assertEqual((yield self.o_trunk_fuid), 0)
    #        sim.add_process(process)