Add sources

source/bus_mux.sby

@@ -0,0 +1,15 @@
+# To run formal verification call SymbiYosys:
+# $ sby -f bus_mux.sby
+
+[options]
+mode prove
+
+[engines]
+smtbmc boolector
+
+[script]
+read -vlog95 -formal bus_mux.v
+prep -top bus_mux
+
+[files]
+bus_mux.v

source/bus_mux.v

@@ -0,0 +1,114 @@
+// This file is auto-generated. Do not edit
+
+// Slaves address ranges:
+//   0 - 0x00000000-0x0000ffff
+//   1 - 0x01000000-0x01000fff
+
+// i_slave_rdata bits:
+//   0: i_slave_rdata[31:0]
+//   1: i_slave_rdata[63:32]
+
+module bus_mux
+  (input wire clock,
+   input wire reset,
+
+   // PicoRV32 memory interface
+   // Look-ahead address and multiplexed signals
+   // Some bits of address may not be used
+   /* verilator lint_off UNUSED */
+   input wire [31:0] i_la_addr,
+   /* verilator lint_on UNUSED */
+   output wire [31:0] o_rdata,
+   input wire i_valid,
+   output wire o_ready,
+
+   // Slaves interface
+   input wire [63:0] i_slave_rdata,
+   output wire [1:0] o_slave_valid,
+   input wire [1:0] i_slave_ready);
+
+  wire [1:0] selector;
+  reg [1:0] selector_reg;
+
+  always @(posedge clock)
+    if (reset)
+      selector_reg <= 2'd0;
+    else
+      if (!i_valid)
+        selector_reg <= selector;
+
+  assign selector[0] =
+    i_la_addr[24] == 1'b0;
+
+  assign selector[1] =
+    i_la_addr[24] == 1'b1;
+
+  assign o_slave_valid = selector_reg & {2{i_valid}};
+  assign o_ready = |(i_slave_ready & selector_reg);
+
+  assign o_rdata =
+    (i_slave_rdata[31:0] & {32{selector_reg[0]}}) |
+    (i_slave_rdata[63:32] & {32{selector_reg[1]}});
+
+`ifdef FORMAL
+
+  always @(*) begin : formal_selector
+    integer ones, n;
+    ones = 0;
+
+    // Check for selector is zero or one-hot value
+    for (n = 0; n < 2; n = n + 1)
+      if (selector[n] == 1'b1)
+        ones = ones + 1;
+
+    assert(ones < 2);
+
+    // Check for correct address ranges decode
+    if (i_la_addr >= 32'h0 && i_la_addr <= 32'hffff)
+      assert(selector[0] == 1'b1);
+    if (i_la_addr >= 32'h1000000 && i_la_addr <= 32'h1000fff)
+      assert(selector[1] == 1'b1);
+  end
+
+  // Check multiplexer
+  always @(*) begin : formal_mux
+    case (selector_reg)
+      2'b01: begin
+        assert(o_rdata == i_slave_rdata[31:0]);
+        assert(o_ready == i_slave_ready[0]);
+        assert(o_slave_valid[0] == i_valid);
+      end
+      2'b10: begin
+        assert(o_rdata == i_slave_rdata[63:32]);
+        assert(o_ready == i_slave_ready[1]);
+        assert(o_slave_valid[1] == i_valid);
+      end
+      2'b00: begin
+        assert(o_rdata == 32'd0);
+        assert(o_ready == 1'b0);
+        assert(o_slave_valid == 2'd0);
+      end
+    endcase
+  end
+
+  // Assume module is not in reset state
+  always @(*) assume(reset == 1'b0);
+
+  // Make flag that the past is valid
+  reg have_past = 1'b0;
+  always @(posedge clock) have_past <= 1'b1;
+
+  // Check for selector_reg is valid and stable when i_valid is 1
+  always @(posedge clock) begin
+    if (have_past)
+      if (i_valid)
+        if ($rose(i_valid))
+          assert(selector_reg == $past(selector));
+        else
+          assert($stable(selector_reg));
+  end
+
+`endif // FORMAL
+
+endmodule // bus_mux
+`default_nettype wire

source/firmware/.clang-format

@@ -0,0 +1,38 @@
+BasedOnStyle: LLVM
+IndentWidth: 4
+UseTab: false
+
+AlignAfterOpenBracket: Align
+AlignConsecutiveAssignments: true
+AlignConsecutiveMacros: true
+AlignEscapedNewlines: Left
+AlignOperands: Align
+
+AlignTrailingComments: true
+AllowShortBlocksOnASingleLine: Empty
+AllowShortCaseLabelsOnASingleLine: false
+AllowShortFunctionsOnASingleLine: Empty
+AllowShortIfStatementsOnASingleLine: WithoutElse
+
+BinPackArguments: true
+
+BreakBeforeBraces: Custom
+BraceWrapping:
+    AfterCaseLabel: false
+    AfterControlStatement: MultiLine
+    AfterFunction: true
+    AfterStruct: true
+    BeforeElse: true
+    BeforeWhile: false
+    IndentBraces: false
+    SplitEmptyFunction: false
+
+IncludeBlocks: Regroup
+SpaceBeforeParens: ControlStatements
+SpaceBeforeSquareBrackets: false
+SpaceInEmptyBlock: false
+SpacesBeforeTrailingComments: 4
+SpacesInCStyleCastParentheses: false
+SpacesInContainerLiterals: false
+SpacesInParentheses: false
+SpacesInSquareBrackets: false

source/firmware/.gitignore

@@ -0,0 +1,4 @@
+*.elf
+*.bin
+*.map
+*.asm

source/firmware/Makefile

@@ -0,0 +1,44 @@
+PROJECT := fw
+SOURCES := crt0.s main.c uprintf.c
+CPU_RAM_REG := ram_reg
+
+ARCH    := riscv32-none-elf
+CFLAGS  := -O2 -Wall -march=rv32i -mabi=ilp32 -mstrict-align \
+           -nostartfiles \
+           -ffunction-sections -lgcc \
+           -Wl,-Tpicorv32-minimal.ld,-static,-Map,$(PROJECT).map
+
+# CFLAGS  := -O3 -Wall -march=rv32i -mabi=ilp32 -mstrict-align \
+# 	   -nostartfiles \
+#            -ffunction-sections \
+# 	   -ffreestanding -lgcc \
+#            -Wl,-T,picorv32-minimal.ld,-static,-Map,$(PROJECT).map
+
+#           -nostdlib
+
+ELF = $(PROJECT).elf
+BIN = $(PROJECT).bin
+ASM = $(PROJECT).asm
+SVH = $(PROJECT).svh
+MEM = $(PROJECT).mem
+
+all: $(ELF) $(BIN) $(MEM) Makefile
+
+$(ELF): $(SOURCES) picorv32-minimal.ld Makefile
+	$(ARCH)-gcc $(CFLAGS) -o $(ELF) $(SOURCES)
+
+$(BIN): $(ELF)
+	$(ARCH)-objcopy -O binary $(ELF) $(BIN)
+
+$(SVH): $(BIN)
+	../../scripts/bin2initial.scm $(BIN) $(CPU_RAM_REG) > $(SVH)
+
+$(MEM): $(BIN)
+	../../scripts/bin2mem.scm $(BIN) 65536 > $(MEM)
+
+disasm: $(ASM)
+$(ASM): $(ELF)
+	$(ARCH)-objdump -d $(ELF) > $(ASM)
+
+clean:
+	rm -f $(ELF) $(BIN) $(PROJECT).map $(SVH) $(MEM)

source/firmware/crt0.s

@@ -0,0 +1,7 @@
+        .section .init, "ax"
+        .global _start
+_start:
+        la sp, __stack_top
+        add s0, sp, zero
+        jal zero, main
+        .end

source/firmware/main.c

@@ -0,0 +1,86 @@
+#include "../io_reg.h"
+#include "uprintf.h"
+
+#include <stdint.h>
+
+void put_char(char c)
+{
+    IO_REG_CONSOLE = c | IO_REG_CONSOLE_SEND;
+}
+
+#define N       50
+#define CHUNK   4
+#define ARR_LEN (10 * N / 3 + 1)
+
+static int arr[ARR_LEN];
+
+void print_digit(int d)
+{
+    static int cnt = 0;
+
+    p("%d", d);
+    cnt++;
+
+    if (cnt == CHUNK) {
+        p("\n");
+        cnt = 0;
+    }
+}
+
+/* See: https://en.wikipedia.org/wiki/Spigot_algorithm */
+
+int main()
+{
+    p("\nComputation of %d first digits of PI\n", N);
+
+    for (int i = 0; i < ARR_LEN; i++)
+        arr[i] = 2;
+
+    int nines    = 0;
+    int predigit = 0;
+
+    for (int j = 1; j < N + 1; j++) {
+        int q = 0;
+
+        for (int i = ARR_LEN; i > 0; i--) {
+            int x      = 10 * arr[i - 1] + q * i;
+            arr[i - 1] = x % (2 * i - 1);
+            q          = x / (2 * i - 1);
+        }
+
+        arr[0] = q % 10;
+        q      = q / 10;
+
+        if (9 == q)
+            nines++;
+        else if (10 == q) {
+            print_digit(predigit + 1);
+
+            for (int k = 0; k < nines; k++)
+                print_digit(0);
+
+            predigit = 0;
+            nines    = 0;
+        }
+        else {
+            print_digit(predigit);
+            predigit = q;
+
+            if (0 != nines) {
+                for (int k = 0; k < nines; k++)
+                    print_digit(9);
+
+                nines = 0;
+            }
+        }
+    }
+    p("%d", predigit);
+
+    p("\nDONE\n");
+
+    /* Stop simulation */
+    IO_REG_CTRL = IO_REG_CTRL_STOP;
+
+    for (;;) {
+    };
+}

source/firmware/picorv32-minimal.ld

@@ -0,0 +1,34 @@
+MEMORY { ram (rx) : ORIGIN = 0, LENGTH = 65536 }
+
+SECTIONS
+{
+    . = 0x00;
+
+    .text : {
+        *(.init*)
+        *(.text*)
+    } > ram
+
+    .bss (NOLOAD) :
+    {
+        *(.bss*)
+        *(COMMON)
+    } > ram
+
+    .data :
+    {
+        *(.data*)
+    } > ram
+
+    .stack (NOLOAD) :
+    {
+        /*
+        . = ALIGN(4);
+        . = . + STACK_SIZE;
+        */
+
+        . = ORIGIN(ram) + LENGTH(ram) - 4;
+        . = ALIGN(4);
+        __stack_top = .;
+    } > ram
+}

source/firmware/shell.nix

@@ -0,0 +1,16 @@
+{ nixpkgs ? import <nixpkgs> {} }:
+
+let cross-rv5 = import <nixpkgs> {
+      crossSystem = {
+        config = "riscv32-none-elf";
+        gcc = { arch = "rv32i"; abi = "ilp32"; };
+        libc = "newlib";
+      };
+    };
+in
+cross-rv5.mkShell {
+  nativeBuildInputs = [ nixpkgs.gnumake nixpkgs.guile_3_0 ];
+  shellHook = ''
+    export NIX_SHELL_NAME="riscv"
+  '';
+}

source/firmware/uprintf.c

@@ -0,0 +1,396 @@
+#include "uprintf.h"
+
+#include <stdarg.h>
+#include <stdint.h>
+
+/*
+ * ------------------- Простая замена printf ------------------------
+ *
+ * Спецификаторы в форматной строке так же как и в printf начинаются
+ * со знака %. После этого знака может идти спецификатор типа с
+ * опциональным указанием ширины выравнивания, символа для
+ * выравнивания и направления выравнивания.
+ *
+ * Первым должен идти спецификатор символа выравнивания - знак '
+ * (одинарная скобка). После него - символ для выравнивания.
+ *
+ * По умолчанию числа выравниваются символом '0' по правому краю, а
+ * строки пробелом по левому краю.
+ *
+ * Далее идет указатель ширины - десятичное число со знаком,
+ * обозначающее минимальную длину выводимой строки. Если строка
+ * получается меньше этого числа, недостающая длина добирается
+ * символами выравнивания. Если ширина указана в виде отрицательного
+ * числа, то выравнивание выполняется по правому краю. Если для числа
+ * не указан символ выравнивания, то оно всегда выравнивается символом
+ * '0' по правому краю. Вместо числа может стоять символ '*',
+ * говоряший о том, что ширину нужно брать из аргумента функции.
+ *
+ * Спецификатор типа может иметь префикс 'l', обозначающий длинное целое
+ * (64 бита) и/или префикс 'u', обозначающий беззнаковое число.
+ *
+ * Спецификаторы типа:
+ *   d, i      Десятичное целое.
+ *   o         Восьмиричное целое.
+ *   b         Двоичное целое.
+ *   x         Шестнадцатиричное целое (строчными).
+ *   X         Шестнадцатиричное целое (прописные).
+ *   c         Символ.
+ *   s         Строка. Если указана ширина, то выравнивание по левому краю.
+ *
+ * Пример:
+ *   p("I:+%'=-6i+\n", 10);
+ *   Вывод: I:+====10+
+ *
+ */
+
+static const char abet[2][16] = {{'0', '1', '2', '3', '4', '5', '6', '7', '8',
+                                  '9', 'A', 'B', 'C', 'D', 'E', 'F'},
+                                 {'0', '1', '2', '3', '4', '5', '6', '7', '8',
+                                  '9', 'a', 'b', 'c', 'd', 'e', 'f'}};
+
+typedef enum {
+    PS_REGULAR = 0,
+    PS_JSYM_SPEC,
+    PS_JSYM,
+    PS_WIDTH_SIGN,
+    PS_WIDTH_ARG,
+    PS_WIDTH,
+    PS_TYPE,
+} pstate;
+
+static int l_strlen(const char *str)
+{
+    int l = 0;
+    while (*str++)
+        l++;
+    return l;
+}
+
+/* Helper functions for p() */
+static void print_string(put_char_func pc, const char *str, int width,
+                         char wchr)
+{
+    int sl, w;
+
+    if (width < 0) {
+        sl = l_strlen(str);
+        for (w = -width; w > sl; w--)
+            pc(wchr);
+    }
+
+    for (sl = 0; *str; str++, sl++)
+        pc(*str);
+
+    if (width > 0) {
+        for (w = width; w > sl; w--)
+            pc(wchr);
+    }
+}
+
+/*
+static void div(uint32_t n, uint32_t d, uint32_t *q, uint32_t *r)
+{
+    uint32_t _q = 0;
+    uint32_t _r = 0;
+    uint32_t b  = 0x80000000L;
+
+    if (d == 0) return;
+
+    while (b) {
+        _r <<= 1;
+        _r |= (n & b) ? 1 : 0;
+
+        if (_r >= d) {
+            _r -= d;
+            _q |= b;
+        }
+
+        b >>= 1;
+    }
+
+    *q = _q;
+    *r = _r;
+}
+*/
+
+static void print_decimal(put_char_func pc, uint32_t u, int negative,
+                          unsigned int base, int width, int lcase, char wchr)
+{
+    if (base > 16) base = 16;
+    if (base < 2) base = 2;
+    if (lcase != 0) lcase = 1;
+
+    char s[66];
+    int si = 64;
+    uint32_t l;
+
+    s[si--] = 0;
+
+    do {
+        // div(u, base, &u, &l);
+        l = u % base;
+        u = u / base;
+        s[si--] = abet[lcase][l];
+    } while (u > 0);
+
+    if (negative) {
+        if (wchr == '0') {
+            pc('-');
+
+            if (width > 0)
+                width--;
+            else if (width < 0)
+                width++;
+        }
+        else
+            s[si--] = '-';
+    }
+
+    si++;
+
+    print_string(pc, s + si, width, wchr);
+}
+
+static void print_unsigned(put_char_func pc, uint32_t s, unsigned int base,
+                           int width, int lcase, char wchr)
+{
+    print_decimal(pc, s, 0, base, width, lcase, wchr);
+}
+
+static void print_signed(put_char_func pc, int64_t s, unsigned int base,
+                         int width, int lcase, char wchr)
+{
+    if (s < 0)
+        print_decimal(pc, (uint32_t)-s, 1, base, width, lcase, wchr);
+    else
+        print_decimal(pc, (uint32_t)s, 0, base, width, lcase, wchr);
+}
+
+static int l_isdigit(char c)
+{
+    return (c >= '0' && c <= '9') ? 1 : 0;
+}
+
+/* Like a vprintf */
+void pv(put_char_func pc, const char *fmt, va_list ap)
+{
+    /* Initialization for supress gcc warnings */
+    int width = 0, wsign = 1, lng = 0, sgn = 0, ab = 0;
+
+    /* Width adjustment character */
+    char wchr = 0;
+
+    unsigned int base = 0;
+    char c;
+    int64_t d;
+
+    pstate st = PS_REGULAR;
+
+    for (;;) {
+        c = *fmt;
+
+        if (c == 0) break;
+
+        switch (st) {
+            /* ---------------------------------------------------------- */
+        case PS_REGULAR:
+            fmt++;
+
+            if (c == '%') {
+                st    = PS_JSYM_SPEC;
+                lng   = 0;
+                sgn   = 1;
+                width = 0;
+                wsign = 1;
+                base  = 10;
+                ab    = 0;
+                wchr  = 0;
+            }
+            else
+                pc(c);
+
+            break;
+
+            /* ---------------------------------------------------------- */
+        case PS_JSYM_SPEC:
+            if (c == '\'') {
+                fmt++;
+                st = PS_JSYM;
+            }
+            else
+                st = PS_WIDTH_SIGN;
+            break;
+
+            /* ---------------------------------------------------------- */
+        case PS_JSYM:
+            fmt++;
+            wchr = c;
+
+            st = PS_WIDTH_SIGN;
+            break;
+
+            /* ---------------------------------------------------------- */
+        case PS_WIDTH_SIGN:
+            if (c == '-') {
+                fmt++;
+                wsign = -1;
+            }
+
+            st = PS_WIDTH_ARG;
+            break;
+
+            /* ---------------------------------------------------------- */
+        case PS_WIDTH_ARG:
+            if (c == '*') {
+                fmt++;
+                width = va_arg(ap, int);
+                st    = PS_TYPE;
+            }
+            else
+                st = PS_WIDTH;
+            break;
+
+            /* ---------------------------------------------------------- */
+        case PS_WIDTH:
+            if (l_isdigit(c)) {
+                fmt++;
+                width = width * 10 + (c - '0');
+            }
+            else
+                st = PS_TYPE;
+            break;
+
+            /* ---------------------------------------------------------- */
+        case PS_TYPE:
+            fmt++;
+
+            switch (c) {
+            case 'l':
+                lng = 1;
+                continue;
+
+            case 'u':
+                sgn = 0;
+                continue;
+
+            case 'd':
+            case 'i':
+            case 'b':
+            case 'o':
+            case 'x':
+            case 'X':
+                if ((lng) && (sgn))
+                    d = (int64_t)va_arg(ap, long long);
+                else if ((lng) && (!sgn))
+                    d = (int64_t)va_arg(ap, unsigned long long);
+                else if ((!lng) && (sgn))
+                    d = (int64_t)va_arg(ap, int);
+                else
+                    d = (int64_t)va_arg(ap, unsigned int);
+
+                ab = 0;
+
+                switch (c) {
+                case 'd':
+                case 'i':
+                    base = 10;
+                    break;
+                case 'b':
+                    base = 2;
+                    break;
+                case 'o':
+                    base = 8;
+                    break;
+                case 'x':
+                    ab = 1;
+                case 'X':
+                    base = 16;
+                    break;
+                default:
+                    break;
+                }
+
+                if (!wchr) {
+                    wchr  = '0';
+                    wsign = -1;
+                }
+
+                if (sgn)
+                    print_signed(pc, d, base, (wsign > 0) ? width : -width, ab,
+                                 wchr);
+                else
+                    print_unsigned(pc, (uint32_t)d, base,
+                                   (wsign > 0) ? width : -width, ab, wchr);
+                break;
+
+            case 'c':
+                pc((char)va_arg(ap, int));
+                break;
+
+            case 's':
+                if (!wchr) wchr = ' ';
+                print_string(pc, va_arg(ap, char *),
+                             (wsign > 0) ? width : -width, wchr);
+                break;
+
+            case '%':
+                pc('%');
+                break;
+
+            default:
+                pc('%');
+                pc(c);
+            }
+
+            st = PS_REGULAR;
+            break;
+
+            /* ---------------------------------------------------------- */
+        default:
+            st = PS_REGULAR;
+        }
+    }
+}
+
+/* Universal printf */
+void pp(put_char_func pc, const char *fmt, ...)
+{
+    va_list ap;
+    va_start(ap, fmt);
+    pv(pc, fmt, ap);
+    va_end(ap);
+}
+
+/* Print to console */
+void p(const char *fmt, ...)
+{
+    va_list ap;
+    va_start(ap, fmt);
+    pv(put_char, fmt, ap);
+    va_end(ap);
+}
+
+/* Print to string */
+int psn(char *str, int size, const char *fmt, ...)
+{
+    va_list ap;
+    va_start(ap, fmt);
+
+    int n = 0;
+
+    /* Nested function. GCC specific */
+    void put_char_str(char c)
+    {
+        if (n < size) {
+            *str++ = c;
+            n++;
+        }
+    }
+
+    pv(put_char_str, fmt, ap);
+
+    va_end(ap);
+
+    return n;
+}

source/firmware/uprintf.h

@@ -0,0 +1,15 @@
+#ifndef _UPRINTF
+#define _UPRINTF
+#include <stdint.h>
+#include <stdarg.h>
+
+typedef void (*put_char_func)(char c);
+extern void put_char(char c);
+
+void pv(put_char_func pc, const char *fmt, va_list ap);
+void pp(put_char_func pc, const char *fmt, ...);
+
+void p(const char *fmt, ...);
+int psn(char *str, int size, const char *fmt, ...);
+
+#endif /* _UPRINTF */

source/generate.sh

@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+set -e
+
+../scripts/register-gen.scm io.reg > io_reg.v
+../scripts/register-gen.scm -c io.reg > io_reg.h
+../scripts/register-gen.scm -t io.reg > io_reg.txt
+../scripts/picorv32-bus-mux-gen.scm -s 0+0x10000 -s 0x01000000+0x1000 -m bus_mux > bus_mux.v
+../scripts/picorv32-bus-mux-gen.scm -s 0+0x10000 -s 0x01000000+0x1000 -m bus_mux -f > bus_mux.sby

source/io.reg

@@ -0,0 +1,16 @@
+;; -*- lisp -*-
+
+((base #x01000000)
+ (address-width 32)
+ (data-width 32)
+ byte-enable
+
+ (reg "ctrl"
+      (info "Control register")
+      (bits 1 "stop" w (reset #b0)))
+
+ (reg "console" read-notify
+      (info "Virtual console port")
+      (bits 8 "data" rw (info "Read/write char from/to console"))
+      (bits 1 "send" hs (info "Write 1 to send symbol"))
+      (bits 1 "valid" r (info "Symbol in DATA is valid"))))

source/io_reg.h

@@ -0,0 +1,17 @@
+#ifndef _IO_REG_H_
+#define _IO_REG_H_
+
+#define IO_REG_BASE 0x1000000
+
+/* -- Register 'CTRL' -- */
+#define IO_REG_CTRL (*(volatile uint32_t*)(IO_REG_BASE + 0x00000000))
+#define IO_REG_CTRL_STOP (1 << 0)
+
+/* -- Register 'CONSOLE' -- */
+#define IO_REG_CONSOLE (*(volatile uint32_t*)(IO_REG_BASE + 0x00000004))
+#define IO_REG_CONSOLE_DATA__MASK 0x000000ff
+#define IO_REG_CONSOLE_DATA__SHIFT 0
+#define IO_REG_CONSOLE_SEND (1 << 8)
+#define IO_REG_CONSOLE_VALID (1 << 9)
+
+#endif // _IO_REG_H_

source/io_reg.txt

@@ -0,0 +1,30 @@
+Register map of IO_REG (base: 0x1000000)
+========================================
+
+  |   Offset   |   Name  |     Description      |
+  |------------+---------+----------------------|
+  | 0x00000000 | CTRL    | Control register     |
+  | 0x00000004 | CONSOLE | Virtual console port |
+
+
+CTRL Register (0x00000000)
+--------------------------
+
+  Control register
+
+  | Bits | Name | Mode | Reset | Description |
+  |------+------+------+-------+-------------|
+  |    0 | STOP | WO   | 0     |             |
+
+
+CONSOLE Register (0x00000004)
+-----------------------------
+
+  Virtual console port
+
+  | Bits | Name  | Mode | Reset |           Description           |
+  |------+-------+------+-------+---------------------------------|
+  |    9 | VALID | RO   | 0     | Symbol in DATA is valid         |
+  |    8 | SEND  | HS   | 0     | Write 1 to send symbol          |
+  |  7:0 | DATA  | RW   | 0     | Read/write char from/to console |
+

source/io_reg.v

@@ -0,0 +1,98 @@
+// This file is auto-generated. Do not edit
+
+module io_reg
+  (input wire clock,
+   input wire reset,
+
+   /* ---- Access bus ---- */
+   /* verilator lint_off UNUSED */
+   input wire [31:0] i_addr,
+   input wire [31:0] i_data,
+   output wire [31:0] o_data,
+   input wire [3:0] i_ben,
+   input wire i_write,
+   input wire i_read,
+   /* verilator lint_on UNUSED */
+
+   /* ---- 'ctrl' ---- */
+   output wire o_ctrl_stop,
+
+   /* ---- 'console' ---- */
+   output wire o_console__rnotify,
+   input wire [7:0] i_console_data,
+   output wire [7:0] o_console_data,
+   output wire o_console_send_hsreq,
+   input wire i_console_send_hsack,
+   input wire i_console_send,
+   input wire i_console_valid);
+
+  /* ---- Address decoder ---- */
+  wire ctrl_select;
+  wire console_select;
+
+  assign ctrl_select =
+    i_addr[2] == 1'b0;
+
+  assign console_select =
+    i_addr[2] == 1'b1;
+
+
+  /* ---- 'ctrl' ---- */
+  reg ctrl_stop;
+  assign o_ctrl_stop = ctrl_stop;
+
+  always @(posedge clock)
+    if (reset)
+      ctrl_stop <= 1'b0;
+    else
+      if (ctrl_select && i_write) begin
+        if (i_ben[0]) ctrl_stop <= i_data[0];
+      end
+
+
+  /* ---- 'console' ---- */
+  reg [7:0] console_data;
+  assign o_console_data = console_data;
+
+  always @(posedge clock)
+    if (reset)
+      console_data <= 8'b0;
+    else
+      if (console_select && i_write) begin
+        if (i_ben[0]) console_data[7:0] <= i_data[7:0];
+      end
+
+  reg console_send_hsreq;
+  assign o_console_send_hsreq = console_send_hsreq;
+
+  always @(posedge clock)
+    if (reset)
+      console_send_hsreq <= 1'b0;
+    else begin
+      if (console_select && i_write && i_ben[1]) console_send_hsreq <= i_data[8];
+      else console_send_hsreq <= console_send_hsreq & (~i_console_send_hsack);
+    end
+
+  assign o_console__rnotify = console_select & i_read;
+
+  /* ---- Read multiplexer ---- */
+  reg [31:0] data_ctrl;
+  reg [31:0] data_console;
+
+  assign o_data = 
+    data_ctrl |
+    data_console;
+
+  always @(*) begin
+    data_ctrl = 32'd0;
+    data_console = 32'd0;
+
+    if (console_select) begin
+      data_console[7:0] = i_console_data;
+      data_console[8] = i_console_send;
+      data_console[9] = i_console_valid;
+    end
+
+  end
+
+endmodule // io_reg

source/picorv32_tcm.sv

@@ -0,0 +1,179 @@
+`timescale 1ps/1ps
+
+module picorv32_tcm #(parameter ADDR_WIDTH = 8,
+                      parameter USE_LOOK_AHEAD = 0,
+                      parameter USE_ADDR_MUX = 1,
+                      parameter MEM_INIT_FILE = "")
+    (input wire clock,
+     /* verilator lint_off UNUSED */
+     // Not used in look-ahead mode
+     input wire reset,
+     /* verilator lint_on UNUSED */
+
+     /* PicoRV32 bus interface */
+     input  wire                  mem_valid,
+     output wire                  mem_ready,
+     input  wire [ADDR_WIDTH-1:0] mem_addr,
+     input  wire           [31:0] mem_wdata,
+     input  wire            [3:0] mem_wstrb,
+     output reg            [31:0] mem_rdata,
+
+     // PicoRV32 look-ahead address.
+     // Not used in non-look-ahead mode.
+     /* verilator lint_off UNUSED */
+     input  wire [ADDR_WIDTH-1:0] mem_la_addr
+     /* verilator lint_off UNUSED */
+     );
+
+    logic [31:0] ram[0:(2 ** (ADDR_WIDTH-2))-1];
+    if (MEM_INIT_FILE != "")
+      initial $readmemh(MEM_INIT_FILE, ram);
+
+    /* verilator lint_off UNUSED */
+    // Bits [1:0] are not used
+    logic [ADDR_WIDTH-1:0] byte_addr;
+    /* verilator lint_on UNUSED */
+    logic [ADDR_WIDTH-3:0] word_addr;
+    logic write;
+
+    assign word_addr = byte_addr[ADDR_WIDTH-1:2];
+
+    always_ff @(posedge clock) begin
+        for (int n = 0; n < 4; n += 1)
+          if (write && mem_wstrb[n])
+            ram[word_addr][n*8 +: 8] <= mem_wdata[n*8 +: 8];
+
+        mem_rdata <= ram[word_addr];
+    end
+
+    if (USE_LOOK_AHEAD == 0) begin : no_look_ahead
+        logic data_ready;
+
+        always_ff @(posedge clock)
+          if (reset) data_ready <= 1'b0;
+          else
+            // Don't use ternary operator to prevent
+            // X-propagation from PicoRV32 core
+            // data_ready <= mem_valid & ~(|mem_wstrb);
+            if (mem_valid && mem_wstrb == '0)
+              data_ready <= 1'b1;
+            else
+              data_ready <= 1'b0;
+
+
+        assign byte_addr = mem_addr;
+        assign write = mem_valid & (|mem_wstrb);
+        assign mem_ready = data_ready | write;
+    end
+    else begin : look_ahead
+        logic data_ready;
+
+        always_ff @(posedge clock)
+          if (reset) data_ready <= 1'b0;
+          else
+            // Don't use ternary operator to prevent
+            // X-propagation from PicoRV32 core
+            // data_ready <= ~(mem_valid && (|mem_wstrb));
+            if (mem_valid && mem_wstrb != '0)
+              data_ready <= 1'b0;
+            else
+              data_ready <= 1'b1;
+
+        /* mem_la_addr валиден как минимум один такт после поднятия mem_valid.
+         * Т.е. в принципе можно обойтись без мультиплескора. В формальной части
+         * добавлено соответствуюшее утверждение. */
+        if (USE_ADDR_MUX == 0)
+          assign byte_addr = mem_la_addr[ADDR_WIDTH-1:0];
+        else
+          assign byte_addr = mem_valid ?
+                             mem_addr[ADDR_WIDTH-1:0] :
+                             mem_la_addr[ADDR_WIDTH-1:0];
+
+        assign write = mem_valid & (|mem_wstrb);
+        assign mem_ready = data_ready;
+    end
+
+`ifdef FORMAL
+    // Past valid flag
+    logic have_past = 1'b0;
+    always_ff @(posedge clock) have_past <= 1'b1;
+
+    // Assumptions
+    always @(*) assume(reset == 1'b0);
+
+    always @(posedge clock)
+      if (have_past) begin
+          // mem_addr <= mem_la_addr
+          if ($rose(mem_valid))
+            assume(mem_addr == $past(mem_la_addr));
+
+          // Stable mem_addr and mem_data when mem_valid is active
+          if (mem_valid) begin
+              assume($stable(mem_addr));
+              assume($stable(mem_wdata));
+              assume($stable(mem_wstrb));
+          end
+
+          // Assume mem_valid will not cleared while mem_ready is not active
+          if ($past(mem_valid) && !$past(mem_ready))
+            assume(mem_valid == 1'b1);
+
+          // Assume mem_valid will cleared after memory transaction complete
+          if ($past(mem_valid) && $past(mem_ready))
+            assume(mem_valid == 1'b0);
+
+          // WARN: May be wrong assumption
+          // Assume mem_add == mem_la_addr on first clock cycle of mem_valid activity
+          if ($rose(mem_valid))
+            assume(mem_addr == mem_la_addr);
+      end
+      else begin
+          // Initial mem_valid = 1'b0
+          assume(mem_valid == 1'b0);
+      end
+
+    // Data read
+    always_ff @(posedge clock)
+      if (have_past)
+        if (mem_valid && mem_ready && mem_wstrb == '0)
+          assert(mem_rdata == ram[mem_addr[ADDR_WIDTH-1:2]]);
+
+    // Data write
+    always_ff @(posedge clock) begin
+        logic [3:0] mem_wstrb_past;
+
+        if (have_past) begin
+            mem_wstrb_past = $past(mem_wstrb);
+
+            if ($past(mem_valid) && $past(mem_ready) && mem_wstrb_past != '0)
+              for (int n = 0; n < 4; n += 1)
+                if (mem_wstrb_past[n])
+                  assert(ram[$past(mem_addr[ADDR_WIDTH-1:2])][n*8 +: 8] == $past(mem_wdata[n*8 +: 8]));
+        end
+    end
+
+    // Mem ready
+    always_ff @(posedge clock)
+      if (have_past)
+        if (USE_LOOK_AHEAD == 0) begin
+            // Write transaction
+            if (mem_wstrb != '0 && mem_valid)
+              assert(mem_ready);
+
+            // First cycle of read transaction
+            if (mem_wstrb == '0 && !$past(mem_valid)&& mem_valid)
+              assert(!mem_ready);
+
+            // Second cycle of read transaction
+            if ($past(mem_wstrb) == '0 && $past(mem_valid) && mem_valid)
+              assert(mem_ready);
+        end
+        else begin
+            // In look-ahead mode mem_ready always active
+            if (mem_valid)
+              assert(mem_ready);
+        end
+
+`endif
+
+endmodule // picorv32_tcm

source/sources.f

@@ -0,0 +1,5 @@
+../source/bus_mux.v
+../source/io_reg.v
+../source/picorv32_tcm.sv
+../source/picorv32.v
+../source/testbench.sv

source/testbench.sv

@@ -0,0 +1,211 @@
+`timescale 1ps/1ps
+
+module testbench (input clock);
+    parameter MEM_ADDR_WIDTH = 16;
+
+    logic reset = 1'b1;
+
+    /* verilator lint_off UNUSED */
+    logic        cpu_mem_valid;
+    logic        cpu_mem_instr;
+    logic        cpu_mem_ready;
+    logic [31:0] cpu_mem_addr;
+    logic [31:0] cpu_mem_wdata;
+    logic [ 3:0] cpu_mem_wstrb;
+    logic [31:0] cpu_mem_rdata;
+
+    // Look-Ahead Interface
+    logic        cpu_mem_la_read;
+    logic        cpu_mem_la_write;
+    logic [31:0] cpu_mem_la_addr;
+    logic [31:0] cpu_mem_la_wdata;
+    logic [ 3:0] cpu_mem_la_wstrb;
+    /* verilator lint_on UNUSED */
+
+    // PicoRV32                                 // Defaults
+    picorv32 #(.ENABLE_COUNTERS(0),             // = 1,
+	       .ENABLE_COUNTERS64(0),           // = 1,
+	       .ENABLE_REGS_16_31(1),           // = 1,
+	       .ENABLE_REGS_DUALPORT(1),        // = 1,
+	       .LATCHED_MEM_RDATA(0),           // = 0,
+	       .TWO_STAGE_SHIFT(1),             // = 1,
+	       .BARREL_SHIFTER(0),              // = 0,
+	       .TWO_CYCLE_COMPARE(0),           // = 0,
+	       .TWO_CYCLE_ALU(0),               // = 0,
+	       .COMPRESSED_ISA(0),              // = 0,
+	       .CATCH_MISALIGN(1),              // = 1,
+	       .CATCH_ILLINSN(1),               // = 1,
+	       .ENABLE_PCPI(0),                 // = 0,
+	       .ENABLE_MUL(0),                  // = 0,
+	       .ENABLE_FAST_MUL(0),             // = 0,
+	       .ENABLE_DIV(0),                  // = 0,
+	       .ENABLE_IRQ(0),                  // = 0,
+	       .ENABLE_IRQ_QREGS(0),            // = 1,
+	       .ENABLE_IRQ_TIMER(0),            // = 1,
+	       .ENABLE_TRACE(0),                // = 0,
+	       .REGS_INIT_ZERO(0),              // = 0,
+	       .MASKED_IRQ(32'h 0000_0000),     // = 32'h 0000_0000,
+	       .LATCHED_IRQ(32'h ffff_ffff),    // = 32'h ffff_ffff,
+	       .PROGADDR_RESET(32'h 0000_0000), // = 32'h 0000_0000,
+	       .PROGADDR_IRQ(32'h 0000_0010),   // = 32'h 0000_0010,
+	       .STACKADDR(32'h ffff_ffff))      // = 32'h ffff_ffff
+    picorv32
+      (.clk(clock),
+       .resetn(~reset),
+
+       .mem_valid(cpu_mem_valid),       // output reg
+       .mem_instr(cpu_mem_instr),       // output reg
+       .mem_ready(cpu_mem_ready),       // input
+       .mem_addr(cpu_mem_addr),         // output reg [31:0]
+       .mem_wdata(cpu_mem_wdata),       // output reg [31:0]
+       .mem_wstrb(cpu_mem_wstrb),       // output reg [ 3:0]
+       .mem_rdata(cpu_mem_rdata),       // input      [31:0]
+
+       // Look-Ahead Interface
+       .mem_la_read(cpu_mem_la_read),   // output
+       .mem_la_write(cpu_mem_la_write), // output
+       .mem_la_addr(cpu_mem_la_addr),   // output     [31:0]
+       .mem_la_wdata(cpu_mem_la_wdata), // output reg [31:0]
+       .mem_la_wstrb(cpu_mem_la_wstrb), // output reg [ 3:0]
+
+       // Unused
+       /* verilator lint_off PINCONNECTEMPTY */
+       .pcpi_valid(),                   // output reg
+       .pcpi_insn(),                    // output reg [31:0]
+       .pcpi_rs1(),                     // output     [31:0]
+       .pcpi_rs2(),                     // output     [31:0]
+       .pcpi_wr(1'b0),                  // input
+       .pcpi_rd(32'd0),                 // input      [31:0]
+       .pcpi_wait(1'b0),                // input
+       .pcpi_ready(1'b0),               // input
+       .irq(32'd0),                     // input      [31:0]
+       .eoi(),                          // output reg [31:0]
+       .trap(),                         // output reg
+       .trace_valid(),                  // output reg
+       .trace_data()                    // output reg [35:0]
+       /* verilator lint_on PINCONNECTEMPTY */
+       );
+
+    // -- Bus multiplexer
+    // Slaves address ranges:
+    //   0 - 0x00000000-0x0000ffff
+    //   1 - 0x01000000-0x01000fff
+
+    // i_slave_rdata bits:
+    //   0: i_slave_rdata[31:0]
+    //   1: i_slave_rdata[63:32]
+
+    logic [31:0] rdata_ram;
+    logic [31:0] rdata_reg;
+    logic valid_ram;
+    logic ready_ram;
+    logic valid_reg;
+    logic ready_reg;
+
+    bus_mux bus_mux
+      (.clock, .reset,
+       // CPU
+       .i_la_addr(cpu_mem_la_addr),
+       .o_rdata(cpu_mem_rdata),
+       .i_valid(cpu_mem_valid),
+       .o_ready(cpu_mem_ready),
+       // Slaves
+       .i_slave_rdata({rdata_reg, rdata_ram}),
+       .o_slave_valid({valid_reg, valid_ram}),
+       .i_slave_ready({ready_reg, ready_ram}));
+
+    // -- CPU memory
+    picorv32_tcm #(.ADDR_WIDTH(MEM_ADDR_WIDTH),
+                   .USE_LOOK_AHEAD(1),
+                   .USE_ADDR_MUX(0),
+                   .MEM_INIT_FILE("../source/firmware/fw.mem"))
+    picorv32_tcm
+      (.clock, .reset,
+
+       /* PicoRV32 bus interface */
+       .mem_valid(valid_ram),
+       .mem_ready(ready_ram),
+       .mem_addr(cpu_mem_addr[MEM_ADDR_WIDTH-1:0]),
+       .mem_wdata(cpu_mem_wdata),
+       .mem_wstrb(cpu_mem_wstrb),
+       .mem_rdata(rdata_ram),
+       .mem_la_addr(cpu_mem_la_addr[MEM_ADDR_WIDTH-1:0]));
+
+    // -- Registers
+    // Reg 'ctrl'
+    logic ctrl_stop;
+
+    // Reg 'console'
+    logic [7:0] i_console_data;
+    logic [7:0] o_console_data;
+    logic console_send;
+
+    logic reg_write;
+    logic reg_read;
+
+    assign ready_reg = 1'b1;
+    assign reg_write = valid_reg & |(cpu_mem_wdata);
+    assign reg_read = valid_reg & &(~cpu_mem_wdata);
+    assign i_console_data = 8'ha5;
+
+    io_reg io_reg
+      (.clock, .reset,
+
+       // CPU
+       .i_addr({16'd0, cpu_mem_addr[15:0]}),
+       .i_data(cpu_mem_wdata),
+       .o_data(rdata_reg),
+       .i_ben(cpu_mem_wstrb),
+       .i_write(reg_write),
+       .i_read(reg_read),
+
+       // Reg 'ctrl'
+       .o_ctrl_stop(ctrl_stop),
+
+       // Reg 'console'
+       .i_console_data(i_console_data),
+       .o_console_data(o_console_data),
+       .o_console_send_hsreq(console_send),
+
+       // Unused
+       /* verilator lint_off PINCONNECTEMPTY */
+       .o_console__rnotify(),
+       .i_console_send_hsack(1'b1),
+       .i_console_send(1'b0),
+       .i_console_valid(1'b1)
+       /* verilator lint_on PINCONNECTEMPTY */
+       );
+
+    // Reset
+    localparam RESET_DURATION = 5;
+    int reset_counter = RESET_DURATION;
+
+    always_ff @(posedge clock)
+      if (reset_counter == 0)
+        reset <= 1'b0;
+      else
+        reset_counter <= reset_counter - 1;
+
+    // Print console output
+    // always_ff @(posedge clock)
+    //   if (!reset && console_send)
+    //     $write("%c", o_console_data);
+
+    initial
+      forever begin
+          @(posedge clock);
+          if (!reset && console_send) begin
+              $write("%c", o_console_data);
+              $fflush;
+          end
+      end
+
+    // Wait for complete
+    initial begin
+        while (reset || ctrl_stop == 1'b0) @(posedge clock);
+
+        @(posedge clock);
+        $finish;
+    end
+
+endmodule // testbench