diff options
Diffstat (limited to 'scripts')
134 files changed, 5722 insertions, 0 deletions
diff --git a/scripts/csmith/.gitignore b/scripts/csmith/.gitignore new file mode 100644 index 0000000..efd00f7 --- /dev/null +++ b/scripts/csmith/.gitignore @@ -0,0 +1,13 @@ +obj_dir +riscv-fesvr +riscv-isa-sim +output_ref.txt +output_sim.txt +platform.info +test.c +test.ld +test.elf +test_ref +test.hex +testbench.vvp +testbench.vcd diff --git a/scripts/csmith/Makefile b/scripts/csmith/Makefile new file mode 100644 index 0000000..fd5107f --- /dev/null +++ b/scripts/csmith/Makefile @@ -0,0 +1,85 @@ +RISCV_TOOLS_DIR = /opt/riscv32imc +RISCV_TOOLS_PREFIX = $(RISCV_TOOLS_DIR)/bin/riscv32-unknown-elf- +CSMITH_INCDIR = $(shell ls -d /usr/local/include/csmith-* | head -n1) +CC = $(RISCV_TOOLS_PREFIX)gcc +SHELL = /bin/bash + +help: + @echo "Usage: make { loop | verilator | iverilog | spike }" + +loop: riscv-fesvr/build.ok riscv-isa-sim/build.ok obj_dir/Vtestbench + +set -e; x() { echo "$$*" >&2; "$$@"; }; i=1; j=1; while true; do echo; echo; \ + echo "---------------- $$((i++)) ($$j) ----------------"; \ + x rm -f test.hex test.elf test.c test_ref test.ld output_ref.txt output_sim.txt; \ + x make spike test.hex || { echo SKIP; continue; }; x rm -f output_sim.txt; \ + x obj_dir/Vtestbench | grep -v '$$finish' > output_sim.txt; \ + x diff -u output_ref.txt output_sim.txt; echo OK; ! ((j++)); \ + done + +verilator: test_ref test.hex obj_dir/Vtestbench + timeout 2 ./test_ref > output_ref.txt && cat output_ref.txt + obj_dir/Vtestbench | grep -v '$$finish' > output_sim.txt + diff -u output_ref.txt output_sim.txt + +iverilog: test_ref test.hex testbench.vvp + timeout 2 ./test_ref > output_ref.txt && cat output_ref.txt + vvp -N testbench.vvp > output_sim.txt + diff -u output_ref.txt output_sim.txt + +spike: riscv-fesvr/build.ok riscv-isa-sim/build.ok test_ref test.elf + timeout 2 ./test_ref > output_ref.txt && cat output_ref.txt + LD_LIBRARY_PATH="./riscv-isa-sim:./riscv-fesvr" ./riscv-isa-sim/spike test.elf > output_sim.txt + diff -u output_ref.txt output_sim.txt + +riscv-fesvr/build.ok: + rm -rf riscv-fesvr + git clone https://github.com/riscv/riscv-fesvr.git riscv-fesvr + +cd riscv-fesvr && git checkout 1c02bd6 && ./configure && make && touch build.ok + +riscv-isa-sim/build.ok: riscv-fesvr/build.ok + rm -rf riscv-isa-sim + git clone https://github.com/riscv/riscv-isa-sim.git riscv-isa-sim + cd riscv-isa-sim && git checkout 10ae74e + cd riscv-isa-sim && patch -p1 < ../riscv-isa-sim.diff + cd riscv-isa-sim && LDFLAGS="-L../riscv-fesvr" ./configure --with-isa=RV32IMC + +cd riscv-isa-sim && ln -s ../riscv-fesvr/fesvr . && make && touch build.ok + +testbench.vvp: testbench.v ../../picorv32.v + iverilog -o testbench.vvp testbench.v ../../picorv32.v + chmod -x testbench.vvp + +obj_dir/Vtestbench: testbench.v testbench.cc ../../picorv32.v + verilator --exe -Wno-fatal --cc --top-module testbench testbench.v ../../picorv32.v testbench.cc + $(MAKE) -C obj_dir -f Vtestbench.mk + +test.hex: test.elf + $(RISCV_TOOLS_PREFIX)objcopy -O verilog test.elf test.hex + +start.elf: start.S start.ld + $(CC) -nostdlib -o start.elf start.S -T start.ld + chmod -x start.elf + +test_ref: test.c + gcc -m32 -o test_ref -w -Os -I $(CSMITH_INCDIR) test.c + +test.elf: test.c syscalls.c start.S + sed -e '/SECTIONS/,+1 s/{/{ . = 0x00000000; .start : { *(.text.start) } application_entry_point = 0x00010000;/;' \ + $(RISCV_TOOLS_DIR)/riscv32-unknown-elf/lib/riscv.ld > test.ld + $(CC) -o test.elf -w -Os -I $(CSMITH_INCDIR) -T test.ld test.c syscalls.c start.S + chmod -x test.elf + +test.c: + echo "integer size = 4" > platform.info + echo "pointer size = 4" >> platform.info + csmith --no-packed-struct -o test.c + gawk '/Seed:/ {print$$2,$$3;}' test.c + +clean: + rm -rf platform.info test.c test.ld test.elf test.hex test_ref obj_dir + rm -rf testbench.vvp testbench.vcd output_ref.txt output_sim.txt + +mrproper: clean + rm -rf riscv-fesvr riscv-isa-sim + +.PHONY: help loop verilator iverilog spike clean mrproper + diff --git a/scripts/csmith/riscv-isa-sim.diff b/scripts/csmith/riscv-isa-sim.diff new file mode 100644 index 0000000..fd22280 --- /dev/null +++ b/scripts/csmith/riscv-isa-sim.diff @@ -0,0 +1,62 @@ +diff --git a/riscv/execute.cc b/riscv/execute.cc +index 5c3fdf7..4d914b3 100644 +--- a/riscv/execute.cc ++++ b/riscv/execute.cc +@@ -124,6 +124,10 @@ miss: + } + + state.minstret += instret; ++ if (state.minstret > 1000000) { ++ printf("Reached limit of 1000000 instructions.\n"); ++ exit(0); ++ } + n -= instret; + } + } +diff --git a/riscv/insns/c_ebreak.h b/riscv/insns/c_ebreak.h +index a17200f..f06d8d9 100644 +--- a/riscv/insns/c_ebreak.h ++++ b/riscv/insns/c_ebreak.h +@@ -1,2 +1,4 @@ + require_extension('C'); ++ ++exit(0); + throw trap_breakpoint(); +diff --git a/riscv/insns/sbreak.h b/riscv/insns/sbreak.h +index c22776c..d38bd22 100644 +--- a/riscv/insns/sbreak.h ++++ b/riscv/insns/sbreak.h +@@ -1 +1,2 @@ ++exit(0); + throw trap_breakpoint(); +diff --git a/riscv/mmu.h b/riscv/mmu.h +index b9948c5..bee1f8b 100644 +--- a/riscv/mmu.h ++++ b/riscv/mmu.h +@@ -67,7 +67,8 @@ public: + if (addr & (sizeof(type##_t)-1)) \ + throw trap_store_address_misaligned(addr); \ + reg_t vpn = addr >> PGSHIFT; \ +- if (likely(tlb_store_tag[vpn % TLB_ENTRIES] == vpn)) \ ++ if (addr == 0x10000000) putchar(val), fflush(stdout); \ ++ else if (likely(tlb_store_tag[vpn % TLB_ENTRIES] == vpn)) \ + *(type##_t*)(tlb_data[vpn % TLB_ENTRIES] + addr) = val; \ + else \ + store_slow_path(addr, sizeof(type##_t), (const uint8_t*)&val); \ +diff --git a/riscv/processor.cc b/riscv/processor.cc +index 3b834c5..f407543 100644 +--- a/riscv/processor.cc ++++ b/riscv/processor.cc +@@ -201,9 +201,9 @@ void processor_t::set_privilege(reg_t prv) + + void processor_t::take_trap(trap_t& t, reg_t epc) + { +- if (debug) +- fprintf(stderr, "core %3d: exception %s, epc 0x%016" PRIx64 "\n", +- id, t.name(), epc); ++ printf("core %3d: exception %s, epc 0x%016" PRIx64 "\n", ++ id, t.name(), epc); ++ exit(0); + + // by default, trap to M-mode, unless delegated to S-mode + reg_t bit = t.cause(); diff --git a/scripts/csmith/start.S b/scripts/csmith/start.S new file mode 100644 index 0000000..d8f110e --- /dev/null +++ b/scripts/csmith/start.S @@ -0,0 +1,51 @@ +.section .text.start +.global application_entry_point + +/* zero-initialize all registers */ +addi x1, zero, 0 +addi x2, zero, 0 +addi x3, zero, 0 +addi x4, zero, 0 +addi x5, zero, 0 +addi x6, zero, 0 +addi x7, zero, 0 +addi x8, zero, 0 +addi x9, zero, 0 +addi x10, zero, 0 +addi x11, zero, 0 +addi x12, zero, 0 +addi x13, zero, 0 +addi x14, zero, 0 +addi x15, zero, 0 +addi x16, zero, 0 +addi x17, zero, 0 +addi x18, zero, 0 +addi x19, zero, 0 +addi x20, zero, 0 +addi x21, zero, 0 +addi x22, zero, 0 +addi x23, zero, 0 +addi x24, zero, 0 +addi x25, zero, 0 +addi x26, zero, 0 +addi x27, zero, 0 +addi x28, zero, 0 +addi x29, zero, 0 +addi x30, zero, 0 +addi x31, zero, 0 + +/* set stack pointer */ +lui sp, %hi(4*1024*1024) +addi sp, sp, %lo(4*1024*1024) + +/* push zeros on the stack for argc and argv */ +/* (stack is aligned to 16 bytes in riscv calling convention) */ +addi sp,sp,-16 +sw zero,0(sp) +sw zero,4(sp) +sw zero,8(sp) +sw zero,12(sp) + +/* jump to libc init */ +j application_entry_point + diff --git a/scripts/csmith/syscalls.c b/scripts/csmith/syscalls.c new file mode 100644 index 0000000..8ea84ca --- /dev/null +++ b/scripts/csmith/syscalls.c @@ -0,0 +1,95 @@ +// An extremely minimalist syscalls.c for newlib +// Based on riscv newlib libgloss/riscv/sys_*.c +// Written by Clifford Wolf. + +#include <sys/stat.h> +#include <unistd.h> +#include <errno.h> + +#define UNIMPL_FUNC(_f) ".globl " #_f "\n.type " #_f ", @function\n" #_f ":\n" + +asm ( + ".text\n" + ".align 2\n" + UNIMPL_FUNC(_open) + UNIMPL_FUNC(_openat) + UNIMPL_FUNC(_lseek) + UNIMPL_FUNC(_stat) + UNIMPL_FUNC(_lstat) + UNIMPL_FUNC(_fstatat) + UNIMPL_FUNC(_isatty) + UNIMPL_FUNC(_access) + UNIMPL_FUNC(_faccessat) + UNIMPL_FUNC(_link) + UNIMPL_FUNC(_unlink) + UNIMPL_FUNC(_execve) + UNIMPL_FUNC(_getpid) + UNIMPL_FUNC(_fork) + UNIMPL_FUNC(_kill) + UNIMPL_FUNC(_wait) + UNIMPL_FUNC(_times) + UNIMPL_FUNC(_gettimeofday) + UNIMPL_FUNC(_ftime) + UNIMPL_FUNC(_utime) + UNIMPL_FUNC(_chown) + UNIMPL_FUNC(_chmod) + UNIMPL_FUNC(_chdir) + UNIMPL_FUNC(_getcwd) + UNIMPL_FUNC(_sysconf) + "j unimplemented_syscall\n" +); + +void unimplemented_syscall() +{ + const char *p = "Unimplemented system call called!\n"; + while (*p) + *(volatile int*)0x10000000 = *(p++); + asm volatile ("ebreak"); + __builtin_unreachable(); +} + +ssize_t _read(int file, void *ptr, size_t len) +{ + // always EOF + return 0; +} + +ssize_t _write(int file, const void *ptr, size_t len) +{ + const void *eptr = ptr + len; + while (ptr != eptr) + *(volatile int*)0x10000000 = *(char*)(ptr++); + return len; +} + +int _close(int file) +{ + // close is called before _exit() + return 0; +} + +int _fstat(int file, struct stat *st) +{ + // fstat is called during libc startup + errno = ENOENT; + return -1; +} + +void *_sbrk(ptrdiff_t incr) +{ + extern unsigned char _end[]; // Defined by linker + static unsigned long heap_end; + + if (heap_end == 0) + heap_end = (long)_end; + + heap_end += incr; + return (void *)(heap_end - incr); +} + +void _exit(int exit_status) +{ + asm volatile ("ebreak"); + __builtin_unreachable(); +} + diff --git a/scripts/csmith/testbench.cc b/scripts/csmith/testbench.cc new file mode 100644 index 0000000..2925d0b --- /dev/null +++ b/scripts/csmith/testbench.cc @@ -0,0 +1,18 @@ +#include "Vtestbench.h" +#include "verilated.h" + +int main(int argc, char **argv, char **env) +{ + Verilated::commandArgs(argc, argv); + Vtestbench* top = new Vtestbench; + + top->clk = 0; + while (!Verilated::gotFinish()) { + top->clk = !top->clk; + top->eval(); + } + + delete top; + exit(0); +} + diff --git a/scripts/csmith/testbench.v b/scripts/csmith/testbench.v new file mode 100644 index 0000000..9d9d8f6 --- /dev/null +++ b/scripts/csmith/testbench.v @@ -0,0 +1,100 @@ +`timescale 1 ns / 1 ps + +module testbench ( +`ifdef VERILATOR + input clk +`endif +); +`ifndef VERILATOR + reg clk = 1; + always #5 clk = ~clk; +`endif + + reg resetn = 0; + integer resetn_cnt = 0; + wire trap; + + initial begin + // $dumpfile("testbench.vcd"); + // $dumpvars(0, testbench); + end + + always @(posedge clk) begin + if (resetn_cnt < 100) + resetn_cnt <= resetn_cnt + 1; + else + resetn <= 1; + end + + wire mem_valid; + wire mem_instr; + wire mem_ready; + wire [31:0] mem_addr; + wire [31:0] mem_wdata; + wire [3:0] mem_wstrb; + wire [31:0] mem_rdata; + + reg [31:0] x32 = 314159265; + reg [31:0] next_x32; + + always @(posedge clk) begin + if (resetn) begin + next_x32 = x32; + next_x32 = next_x32 ^ (next_x32 << 13); + next_x32 = next_x32 ^ (next_x32 >> 17); + next_x32 = next_x32 ^ (next_x32 << 5); + x32 <= next_x32; + end + end + + picorv32 #( + .COMPRESSED_ISA(1), + .ENABLE_MUL(1), + .ENABLE_DIV(1) + ) uut ( + .clk (clk ), + .resetn (resetn ), + .trap (trap ), + .mem_valid (mem_valid ), + .mem_instr (mem_instr ), + .mem_ready (mem_ready ), + .mem_addr (mem_addr ), + .mem_wdata (mem_wdata ), + .mem_wstrb (mem_wstrb ), + .mem_rdata (mem_rdata ) + ); + + reg [7:0] memory [0:4*1024*1024-1]; + initial $readmemh("test.hex", memory); + + assign mem_ready = x32[0] && mem_valid; + + assign mem_rdata[ 7: 0] = memory[mem_addr + 0]; + assign mem_rdata[15: 8] = memory[mem_addr + 1]; + assign mem_rdata[23:16] = memory[mem_addr + 2]; + assign mem_rdata[31:24] = memory[mem_addr + 3]; + + always @(posedge clk) begin + if (mem_valid && mem_ready) begin + if (mem_wstrb && mem_addr == 'h10000000) begin + $write("%c", mem_wdata[ 7: 0]); +`ifndef VERILATOR + $fflush; +`endif + end else begin + if (mem_wstrb[0]) memory[mem_addr + 0] <= mem_wdata[ 7: 0]; + if (mem_wstrb[1]) memory[mem_addr + 1] <= mem_wdata[15: 8]; + if (mem_wstrb[2]) memory[mem_addr + 2] <= mem_wdata[23:16]; + if (mem_wstrb[3]) memory[mem_addr + 3] <= mem_wdata[31:24]; + end + end + end + + always @(posedge clk) begin + if (resetn && trap) begin + // repeat (10) @(posedge clk); + // $display("TRAP"); + $finish; + end + end +endmodule diff --git a/scripts/cxxdemo/.gitignore b/scripts/cxxdemo/.gitignore new file mode 100644 index 0000000..47e6b5c --- /dev/null +++ b/scripts/cxxdemo/.gitignore @@ -0,0 +1,9 @@ +firmware.d +firmware.elf +firmware.hex +firmware32.hex +firmware.o +syscalls.o +testbench.vvp +testbench.vcd +start.elf diff --git a/scripts/cxxdemo/Makefile b/scripts/cxxdemo/Makefile new file mode 100644 index 0000000..2d95019 --- /dev/null +++ b/scripts/cxxdemo/Makefile @@ -0,0 +1,38 @@ +RISCV_TOOLS_PREFIX = /opt/riscv32ic/bin/riscv32-unknown-elf- +CXX = $(RISCV_TOOLS_PREFIX)g++ +CC = $(RISCV_TOOLS_PREFIX)gcc +AS = $(RISCV_TOOLS_PREFIX)gcc +CXXFLAGS = -MD -Os -Wall -std=c++11 +CCFLAGS = -MD -Os -Wall -std=c++11 +LDFLAGS = -Wl,--gc-sections +LDLIBS = -lstdc++ + +test: testbench.vvp firmware32.hex + vvp -N testbench.vvp + +testbench.vvp: testbench.v ../../picorv32.v + iverilog -o testbench.vvp testbench.v ../../picorv32.v + chmod -x testbench.vvp + +firmware32.hex: firmware.elf start.elf hex8tohex32.py + $(RISCV_TOOLS_PREFIX)objcopy -O verilog start.elf start.tmp + $(RISCV_TOOLS_PREFIX)objcopy -O verilog firmware.elf firmware.tmp + cat start.tmp firmware.tmp > firmware.hex + python3 hex8tohex32.py firmware.hex > firmware32.hex + rm -f start.tmp firmware.tmp + +firmware.elf: firmware.o syscalls.o + $(CC) $(LDFLAGS) -o $@ $^ -T ../../firmware/riscv.ld $(LDLIBS) + chmod -x firmware.elf + +start.elf: start.S start.ld + $(CC) -nostdlib -o start.elf start.S -T start.ld $(LDLIBS) + chmod -x start.elf + +clean: + rm -f *.o *.d *.tmp start.elf + rm -f firmware.elf firmware.hex firmware32.hex + rm -f testbench.vvp testbench.vcd + +-include *.d +.PHONY: test clean diff --git a/scripts/cxxdemo/firmware.cc b/scripts/cxxdemo/firmware.cc new file mode 100644 index 0000000..638c0dd --- /dev/null +++ b/scripts/cxxdemo/firmware.cc @@ -0,0 +1,87 @@ +#include <stdio.h> +#include <iostream> +#include <vector> +#include <algorithm> + +class ExampleBaseClass +{ +public: + ExampleBaseClass() { + std::cout << "ExampleBaseClass()" << std::endl; + } + + virtual ~ExampleBaseClass() { + std::cout << "~ExampleBaseClass()" << std::endl; + } + + virtual void print_something_virt() { + std::cout << "ExampleBaseClass::print_something_virt()" << std::endl; + } + + void print_something_novirt() { + std::cout << "ExampleBaseClass::print_something_novirt()" << std::endl; + } +}; + +class ExampleSubClass : public ExampleBaseClass +{ +public: + ExampleSubClass() { + std::cout << "ExampleSubClass()" << std::endl; + } + + virtual ~ExampleSubClass() { + std::cout << "~ExampleSubClass()" << std::endl; + } + + virtual void print_something_virt() { + std::cout << "ExampleSubClass::print_something_virt()" << std::endl; + } + + void print_something_novirt() { + std::cout << "ExampleSubClass::print_something_novirt()" << std::endl; + } +}; + +int main() +{ + printf("Hello World, C!\n"); + + std::cout << "Hello World, C++!" << std::endl; + + ExampleBaseClass *obj = new ExampleBaseClass; + obj->print_something_virt(); + obj->print_something_novirt(); + delete obj; + + obj = new ExampleSubClass; + obj->print_something_virt(); + obj->print_something_novirt(); + delete obj; + + std::vector<unsigned int> some_ints; + some_ints.push_back(0x48c9b3e4); + some_ints.push_back(0x79109b6a); + some_ints.push_back(0x16155039); + some_ints.push_back(0xa3635c9a); + some_ints.push_back(0x8d2f4702); + some_ints.push_back(0x38d232ae); + some_ints.push_back(0x93924a17); + some_ints.push_back(0x62b895cc); + some_ints.push_back(0x6130d459); + some_ints.push_back(0x837c8b44); + some_ints.push_back(0x3d59b4fe); + some_ints.push_back(0x444914d8); + some_ints.push_back(0x3a3dc660); + some_ints.push_back(0xe5a121ef); + some_ints.push_back(0xff00866d); + some_ints.push_back(0xb843b879); + + std::sort(some_ints.begin(), some_ints.end()); + + for (auto n : some_ints) + std::cout << std::hex << n << std::endl; + + std::cout << "All done." << std::endl; + return 0; +} diff --git a/scripts/cxxdemo/hex8tohex32.py b/scripts/cxxdemo/hex8tohex32.py new file mode 100644 index 0000000..ae44101 --- /dev/null +++ b/scripts/cxxdemo/hex8tohex32.py @@ -0,0 +1,34 @@ +#!/usr/bin/env python3 + +import fileinput +import itertools + +ptr = 0 +data = [] + +def write_data(): + if len(data) != 0: + print("@%08x" % (ptr >> 2)) + while len(data) % 4 != 0: + data.append(0) + for word_bytes in zip(*([iter(data)]*4)): + print("".join(["%02x" % b for b in reversed(word_bytes)])) + +for line in fileinput.input(): + if line.startswith("@"): + addr = int(line[1:], 16) + if addr > ptr+4: + write_data() + ptr = addr + data = [] + while ptr % 4 != 0: + data.append(0) + ptr -= 1 + else: + while ptr + len(data) < addr: + data.append(0) + else: + data += [int(tok, 16) for tok in line.split()] + +write_data() + diff --git a/scripts/cxxdemo/start.S b/scripts/cxxdemo/start.S new file mode 100644 index 0000000..f872a14 --- /dev/null +++ b/scripts/cxxdemo/start.S @@ -0,0 +1,52 @@ +.section .text +.global _ftext +.global _pvstart + +_pvstart: +/* zero-initialize all registers */ +addi x1, zero, 0 +addi x2, zero, 0 +addi x3, zero, 0 +addi x4, zero, 0 +addi x5, zero, 0 +addi x6, zero, 0 +addi x7, zero, 0 +addi x8, zero, 0 +addi x9, zero, 0 +addi x10, zero, 0 +addi x11, zero, 0 +addi x12, zero, 0 +addi x13, zero, 0 +addi x14, zero, 0 +addi x15, zero, 0 +addi x16, zero, 0 +addi x17, zero, 0 +addi x18, zero, 0 +addi x19, zero, 0 +addi x20, zero, 0 +addi x21, zero, 0 +addi x22, zero, 0 +addi x23, zero, 0 +addi x24, zero, 0 +addi x25, zero, 0 +addi x26, zero, 0 +addi x27, zero, 0 +addi x28, zero, 0 +addi x29, zero, 0 +addi x30, zero, 0 +addi x31, zero, 0 + +/* set stack pointer */ +lui sp, %hi(4*1024*1024) +addi sp, sp, %lo(4*1024*1024) + +/* push zeros on the stack for argc and argv */ +/* (stack is aligned to 16 bytes in riscv calling convention) */ +addi sp,sp,-16 +sw zero,0(sp) +sw zero,4(sp) +sw zero,8(sp) +sw zero,12(sp) + +/* jump to libc init */ +j _ftext diff --git a/scripts/cxxdemo/start.ld b/scripts/cxxdemo/start.ld new file mode 100644 index 0000000..773eee2 --- /dev/null +++ b/scripts/cxxdemo/start.ld @@ -0,0 +1,5 @@ +SECTIONS { +. = 0x00000000; +.text : { *(.text) } +_ftext = 0x00010000; +} diff --git a/scripts/cxxdemo/syscalls.c b/scripts/cxxdemo/syscalls.c new file mode 100644 index 0000000..8ea84ca --- /dev/null +++ b/scripts/cxxdemo/syscalls.c @@ -0,0 +1,95 @@ +// An extremely minimalist syscalls.c for newlib +// Based on riscv newlib libgloss/riscv/sys_*.c +// Written by Clifford Wolf. + +#include <sys/stat.h> +#include <unistd.h> +#include <errno.h> + +#define UNIMPL_FUNC(_f) ".globl " #_f "\n.type " #_f ", @function\n" #_f ":\n" + +asm ( + ".text\n" + ".align 2\n" + UNIMPL_FUNC(_open) + UNIMPL_FUNC(_openat) + UNIMPL_FUNC(_lseek) + UNIMPL_FUNC(_stat) + UNIMPL_FUNC(_lstat) + UNIMPL_FUNC(_fstatat) + UNIMPL_FUNC(_isatty) + UNIMPL_FUNC(_access) + UNIMPL_FUNC(_faccessat) + UNIMPL_FUNC(_link) + UNIMPL_FUNC(_unlink) + UNIMPL_FUNC(_execve) + UNIMPL_FUNC(_getpid) + UNIMPL_FUNC(_fork) + UNIMPL_FUNC(_kill) + UNIMPL_FUNC(_wait) + UNIMPL_FUNC(_times) + UNIMPL_FUNC(_gettimeofday) + UNIMPL_FUNC(_ftime) + UNIMPL_FUNC(_utime) + UNIMPL_FUNC(_chown) + UNIMPL_FUNC(_chmod) + UNIMPL_FUNC(_chdir) + UNIMPL_FUNC(_getcwd) + UNIMPL_FUNC(_sysconf) + "j unimplemented_syscall\n" +); + +void unimplemented_syscall() +{ + const char *p = "Unimplemented system call called!\n"; + while (*p) + *(volatile int*)0x10000000 = *(p++); + asm volatile ("ebreak"); + __builtin_unreachable(); +} + +ssize_t _read(int file, void *ptr, size_t len) +{ + // always EOF + return 0; +} + +ssize_t _write(int file, const void *ptr, size_t len) +{ + const void *eptr = ptr + len; + while (ptr != eptr) + *(volatile int*)0x10000000 = *(char*)(ptr++); + return len; +} + +int _close(int file) +{ + // close is called before _exit() + return 0; +} + +int _fstat(int file, struct stat *st) +{ + // fstat is called during libc startup + errno = ENOENT; + return -1; +} + +void *_sbrk(ptrdiff_t incr) +{ + extern unsigned char _end[]; // Defined by linker + static unsigned long heap_end; + + if (heap_end == 0) + heap_end = (long)_end; + + heap_end += incr; + return (void *)(heap_end - incr); +} + +void _exit(int exit_status) +{ + asm volatile ("ebreak"); + __builtin_unreachable(); +} + diff --git a/scripts/cxxdemo/testbench.v b/scripts/cxxdemo/testbench.v new file mode 100644 index 0000000..ac9af70 --- /dev/null +++ b/scripts/cxxdemo/testbench.v @@ -0,0 +1,114 @@ +`timescale 1 ns / 1 ps +`undef VERBOSE_MEM +`undef WRITE_VCD +`undef MEM8BIT + +module testbench; + reg clk = 1; + reg resetn = 0; + wire trap; + + always #5 clk = ~clk; + + initial begin + repeat (100) @(posedge clk); + resetn <= 1; + end + + wire mem_valid; + wire mem_instr; + reg mem_ready; + wire [31:0] mem_addr; + wire [31:0] mem_wdata; + wire [3:0] mem_wstrb; + reg [31:0] mem_rdata; + + picorv32 #( + .COMPRESSED_ISA(1) + ) uut ( + .clk (clk ), + .resetn (resetn ), + .trap (trap ), + .mem_valid (mem_valid ), + .mem_instr (mem_instr ), + .mem_ready (mem_ready ), + .mem_addr (mem_addr ), + .mem_wdata (mem_wdata ), + .mem_wstrb (mem_wstrb ), + .mem_rdata (mem_rdata ) + ); + + localparam MEM_SIZE = 4*1024*1024; +`ifdef MEM8BIT + reg [7:0] memory [0:MEM_SIZE-1]; + initial $readmemh("firmware.hex", memory); +`else + reg [31:0] memory [0:MEM_SIZE/4-1]; + initial $readmemh("firmware32.hex", memory); +`endif + + always @(posedge clk) begin + mem_ready <= 0; + if (mem_valid && !mem_ready) begin + mem_ready <= 1; + mem_rdata <= 'bx; + case (1) + mem_addr < MEM_SIZE: begin +`ifdef MEM8BIT + if (|mem_wstrb) begin + if (mem_wstrb[0]) memory[mem_addr + 0] <= mem_wdata[ 7: 0]; + if (mem_wstrb[1]) memory[mem_addr + 1] <= mem_wdata[15: 8]; + if (mem_wstrb[2]) memory[mem_addr + 2] <= mem_wdata[23:16]; + if (mem_wstrb[3]) memory[mem_addr + 3] <= mem_wdata[31:24]; + end else begin + mem_rdata <= {memory[mem_addr+3], memory[mem_addr+2], memory[mem_addr+1], memory[mem_addr]}; + end +`else + if (|mem_wstrb) begin + if (mem_wstrb[0]) memory[mem_addr >> 2][ 7: 0] <= mem_wdata[ 7: 0]; + if (mem_wstrb[1]) memory[mem_addr >> 2][15: 8] <= mem_wdata[15: 8]; + if (mem_wstrb[2]) memory[mem_addr >> 2][23:16] <= mem_wdata[23:16]; + if (mem_wstrb[3]) memory[mem_addr >> 2][31:24] <= mem_wdata[31:24]; + end else begin + mem_rdata <= memory[mem_addr >> 2]; + end +`endif + end + mem_addr == 32'h 1000_0000: begin + $write("%c", mem_wdata[7:0]); + end + endcase + end + if (mem_valid && mem_ready) begin +`ifdef VERBOSE_MEM + if (|mem_wstrb) + $display("WR: ADDR=%x DATA=%x MASK=%b", mem_addr, mem_wdata, mem_wstrb); + else + $display("RD: ADDR=%x DATA=%x%s", mem_addr, mem_rdata, mem_instr ? " INSN" : ""); +`endif + if (^mem_addr === 1'bx || + (mem_wstrb[0] && ^mem_wdata[ 7: 0] == 1'bx) || + (mem_wstrb[1] && ^mem_wdata[15: 8] == 1'bx) || + (mem_wstrb[2] && ^mem_wdata[23:16] == 1'bx) || + (mem_wstrb[3] && ^mem_wdata[31:24] == 1'bx)) begin + $display("CRITICAL UNDEF MEM TRANSACTION"); + $finish; + end + end + end + +`ifdef WRITE_VCD + initial begin + $dumpfile("testbench.vcd"); + $dumpvars(0, testbench); + end +`endif + + always @(posedge clk) begin + if (resetn && trap) begin + repeat (10) @(posedge clk); + $display("TRAP"); + $finish; + end + end +endmodule diff --git a/scripts/icestorm/.gitignore b/scripts/icestorm/.gitignore new file mode 100644 index 0000000..9502e6b --- /dev/null +++ b/scripts/icestorm/.gitignore @@ -0,0 +1,5 @@ +synth.blif +synth.log +synth.bin +synth.txt +firmware.hex diff --git a/scripts/icestorm/Makefile b/scripts/icestorm/Makefile new file mode 100644 index 0000000..7672b41 --- /dev/null +++ b/scripts/icestorm/Makefile @@ -0,0 +1,104 @@ +TOOLCHAIN_PREFIX = riscv32-unknown-elf- + +ICE40_SIM_CELLS=$(shell yosys-config --datdir/ice40/cells_sim.v) + +# set to 4 for simulation +FIRMWARE_COUNTER_BITS=18 + +all: example.bin + +## ------------------- +## firmware generation + +firmware.elf: firmware.S firmware.c firmware.lds + $(TOOLCHAIN_PREFIX)gcc \ + -DSHIFT_COUNTER_BITS=$(FIRMWARE_COUNTER_BITS) \ + -march=rv32i -Os -ffreestanding -nostdlib \ + -o $@ firmware.S firmware.c \ + --std=gnu99 -Wl,-Bstatic,-T,firmware.lds,-Map,firmware.map,--strip-debug + chmod -x $@ + +firmware.bin: firmware.elf + $(TOOLCHAIN_PREFIX)objcopy -O binary $< $@ + chmod -x $@ + +firmware.hex: firmware.bin + python3 ../../firmware/makehex.py $< 128 > $@ + +## ------------------------------ +## main flow: synth/p&r/bitstream + +synth.json: example.v ../../picorv32.v firmware.hex + yosys -v3 -l synth.log -p 'synth_ice40 -top top -json $@; write_verilog -attr2comment synth.v' $(filter %.v, $^) + +example.asc: synth.json example.pcf + nextpnr-ice40 --hx8k --package ct256 --json $< --pcf example.pcf --asc $@ + +example.bin: example.asc + icepack $< $@ + +## ----------------- +## icarus simulation + +example_tb.vvp: example.v example_tb.v ../../picorv32.v firmware.hex + iverilog -o $@ -s testbench $(filter %.v, $^) + chmod -x $@ + +example_sim: example_tb.vvp + vvp -N $< + +example_sim_vcd: example_tb.vvp + vvp -N $< +vcd + +## --------------------- +## post-synth simulation + +synth_tb.vvp: example_tb.v synth.json + iverilog -o $@ -s testbench synth.v example_tb.v $(ICE40_SIM_CELLS) + chmod -x $@ + +synth_sim: synth_tb.vvp + vvp -N $< + +synth_sim_vcd: synth_tb.vvp + vvp -N $< +vcd + +## --------------------- +## post-route simulation + +route.v: example.asc example.pcf + icebox_vlog -L -n top -sp example.pcf $< > $@ + +route_tb.vvp: route.v example_tb.v + iverilog -o $@ -s testbench $^ $(ICE40_SIM_CELLS) + chmod -x $@ + +route_sim: route_tb.vvp + vvp -N $< + +route_sim_vcd: route_tb.vvp + vvp -N $< +vcd + +## --------------------- +## miscellaneous targets + +prog_sram: example.bin + iceprog -S $< + +timing: example.asc example.pcf + icetime -c 62 -tmd hx8k -P ct256 -p example.pcf -t $< + +view: example.vcd + gtkwave $< example.gtkw + +## ------ +## el fin + +clean: + rm -f firmware.elf firmware.map firmware.bin firmware.hex + rm -f synth.log synth.v synth.json route.v example.asc example.bin + rm -f example_tb.vvp synth_tb.vvp route_tb.vvp example.vcd + +.PHONY: all prog_sram view clean +.PHONY: example_sim synth_sim route_sim timing +.PHONY: example_sim_vcd synth_sim_vcd route_sim_vcd diff --git a/scripts/icestorm/example.pcf b/scripts/icestorm/example.pcf new file mode 100644 index 0000000..a5c7398 --- /dev/null +++ b/scripts/icestorm/example.pcf @@ -0,0 +1,9 @@ +set_io clk J3 +set_io LED0 B5 +set_io LED1 B4 +set_io LED2 A2 +set_io LED3 A1 +set_io LED4 C5 +set_io LED5 C4 +set_io LED6 B3 +set_io LED7 C3 diff --git a/scripts/icestorm/example.v b/scripts/icestorm/example.v new file mode 100644 index 0000000..e1c64b4 --- /dev/null +++ b/scripts/icestorm/example.v @@ -0,0 +1,80 @@ +`timescale 1 ns / 1 ps + +module top ( + input clk, + output reg LED0, LED1, LED2, LED3, LED4, LED5, LED6, LED7 +); + // ------------------------------- + // Reset Generator + + reg [7:0] resetn_counter = 0; + wire resetn = &resetn_counter; + + always @(posedge clk) begin + if (!resetn) + resetn_counter <= resetn_counter + 1; + end + + + // ------------------------------- + // PicoRV32 Core + + wire mem_valid; + wire [31:0] mem_addr; + wire [31:0] mem_wdata; + wire [3:0] mem_wstrb; + + reg mem_ready; + reg [31:0] mem_rdata; + + picorv32 #( + .ENABLE_COUNTERS(0), + .LATCHED_MEM_RDATA(1), + .TWO_STAGE_SHIFT(0), + .TWO_CYCLE_ALU(1), + .CATCH_MISALIGN(0), + .CATCH_ILLINSN(0) + ) cpu ( + .clk (clk ), + .resetn (resetn ), + .mem_valid(mem_valid), + .mem_ready(mem_ready), + .mem_addr (mem_addr ), + .mem_wdata(mem_wdata), + .mem_wstrb(mem_wstrb), + .mem_rdata(mem_rdata) + ); + + + // ------------------------------- + // Memory/IO Interface + + // 128 32bit words = 512 bytes memory + localparam MEM_SIZE = 128; + reg [31:0] memory [0:MEM_SIZE-1]; + initial $readmemh("firmware.hex", memory); + + always @(posedge clk) begin + mem_ready <= 0; + if (resetn && mem_valid && !mem_ready) begin + (* parallel_case *) + case (1) + !mem_wstrb && (mem_addr >> 2) < MEM_SIZE: begin + mem_rdata <= memory[mem_addr >> 2]; + mem_ready <= 1; + end + |mem_wstrb && (mem_addr >> 2) < MEM_SIZE: begin + if (mem_wstrb[0]) memory[mem_addr >> 2][ 7: 0] <= mem_wdata[ 7: 0]; + if (mem_wstrb[1]) memory[mem_addr >> 2][15: 8] <= mem_wdata[15: 8]; + if (mem_wstrb[2]) memory[mem_addr >> 2][23:16] <= mem_wdata[23:16]; + if (mem_wstrb[3]) memory[mem_addr >> 2][31:24] <= mem_wdata[31:24]; + mem_ready <= 1; + end + |mem_wstrb && mem_addr == 32'h1000_0000: begin + {LED7, LED6, LED5, LED4, LED3, LED2, LED1, LED0} <= mem_wdata; + mem_ready <= 1; + end + endcase + end + end +endmodule diff --git a/scripts/icestorm/example_tb.v b/scripts/icestorm/example_tb.v new file mode 100644 index 0000000..f04f8f8 --- /dev/null +++ b/scripts/icestorm/example_tb.v @@ -0,0 +1,30 @@ +`timescale 1 ns / 1 ps + +module testbench; + reg clk = 1; + always #5 clk = ~clk; + wire LED0, LED1, LED2, LED3, LED4, LED5, LED6, LED7; + + top uut ( + .clk(clk), + .LED0(LED0), + .LED1(LED1), + .LED2(LED2), + .LED3(LED3), + .LED4(LED4), + .LED5(LED5), + .LED6(LED6), + .LED7(LED7) + ); + + initial begin + if ($test$plusargs("vcd")) begin + $dumpfile("example.vcd"); + $dumpvars(0, testbench); + end + + $monitor(LED7, LED6, LED5, LED4, LED3, LED2, LED1, LED0); + repeat (10000) @(posedge clk); + $finish; + end +endmodule diff --git a/scripts/icestorm/firmware.S b/scripts/icestorm/firmware.S new file mode 100644 index 0000000..d19783d --- /dev/null +++ b/scripts/icestorm/firmware.S @@ -0,0 +1,12 @@ +.section .init +.global main + +/* set stack pointer */ +lui sp, %hi(512) +addi sp, sp, %lo(512) + +/* call main */ +jal ra, main + +/* break */ +ebreak diff --git a/scripts/icestorm/firmware.c b/scripts/icestorm/firmware.c new file mode 100644 index 0000000..80a4661 --- /dev/null +++ b/scripts/icestorm/firmware.c @@ -0,0 +1,58 @@ +#include <stdint.h> + +#ifndef SHIFT_COUNTER_BITS +#error SHIFT_COUNTER_BITS must be defined as 4 (for simulation) or 18 (for hardware bitstreams)! +#endif + +void output(uint8_t c) +{ + *(volatile char*)0x10000000 = c; +} + +uint8_t gray_encode_simple(uint8_t c) +{ + return c ^ (c >> 1); +} + +uint8_t gray_encode_bitwise(uint8_t c) +{ + unsigned int in_buf = c, out_buf = 0, bit = 1; + for (int i = 0; i < 8; i++) { + if ((in_buf & 1) ^ ((in_buf >> 1) & 1)) + out_buf |= bit; + in_buf = in_buf >> 1; + bit = bit << 1; + } + return out_buf; +} + +uint8_t gray_decode(uint8_t c) +{ + uint8_t t = c >> 1; + while (t) { + c = c ^ t; + t = t >> 1; + } + return c; +} + +void gray(uint8_t c) +{ + uint8_t gray_simple = gray_encode_simple(c); + uint8_t gray_bitwise = gray_encode_bitwise(c); + uint8_t gray_decoded = gray_decode(gray_simple); + + if (gray_simple != gray_bitwise || gray_decoded != c) + while (1) asm volatile ("ebreak"); + + output(gray_simple); +} + +void main() +{ + for (uint32_t counter = (2+4+32+64) << SHIFT_COUNTER_BITS;; counter++) { + asm volatile ("" : : "r"(counter)); + if ((counter & ~(~0 << SHIFT_COUNTER_BITS)) == 0) + gray(counter >> SHIFT_COUNTER_BITS); + } +} diff --git a/scripts/icestorm/firmware.lds b/scripts/icestorm/firmware.lds new file mode 100644 index 0000000..970000a --- /dev/null +++ b/scripts/icestorm/firmware.lds @@ -0,0 +1,11 @@ +SECTIONS { + .memory : { + . = 0x000000; + *(.init); + *(.text); + *(*); + . = ALIGN(4); + end = .; + } +} + diff --git a/scripts/icestorm/readme.md b/scripts/icestorm/readme.md new file mode 100644 index 0000000..101391f --- /dev/null +++ b/scripts/icestorm/readme.md @@ -0,0 +1,12 @@ +To build the example LED-blinking firmware for an HX8K Breakout Board and get +a timing report (checked against the default 12MHz oscillator): + + $ make clean example.bin timing + +To run all the simulation tests: + + $ make clean example_sim synth_sim route_sim FIRMWARE_COUNTER_BITS=4 + +(You must run the `clean` target to rebuild the firmware with the updated +`FIRMWARE_COUNTER_BITS` parameter; the firmware source must be recompiled for +simulation vs hardware, but this is not tracked as a Makefile dependency.) diff --git a/scripts/presyn/.gitignore b/scripts/presyn/.gitignore new file mode 100644 index 0000000..4281b17 --- /dev/null +++ b/scripts/presyn/.gitignore @@ -0,0 +1,7 @@ +firmware.bin +firmware.elf +firmware.hex +firmware.map +picorv32_presyn.v +testbench.vcd +testbench.vvp diff --git a/scripts/presyn/Makefile b/scripts/presyn/Makefile new file mode 100644 index 0000000..d1c367e --- /dev/null +++ b/scripts/presyn/Makefile @@ -0,0 +1,22 @@ + +TOOLCHAIN_PREFIX = /opt/riscv32ic/bin/riscv32-unknown-elf- + +run: testbench.vvp firmware.hex + vvp -N testbench.vvp + +firmware.hex: firmware.S firmware.c firmware.lds + $(TOOLCHAIN_PREFIX)gcc -Os -ffreestanding -nostdlib -o firmware.elf firmware.S firmware.c \ + --std=gnu99 -Wl,-Bstatic,-T,firmware.lds,-Map,firmware.map,--strip-debug -lgcc + $(TOOLCHAIN_PREFIX)objcopy -O binary firmware.elf firmware.bin + python3 ../../firmware/makehex.py firmware.bin 4096 > firmware.hex + +picorv32_presyn.v: picorv32_presyn.ys picorv32_regs.txt ../../picorv32.v + yosys -v0 picorv32_presyn.ys + +testbench.vvp: testbench.v picorv32_presyn.v + iverilog -o testbench.vvp testbench.v picorv32_presyn.v + +clean: + rm -f firmware.bin firmware.elf firmware.hex firmware.map + rm -f picorv32_presyn.v testbench.vvp testbench.vcd + diff --git a/scripts/presyn/README b/scripts/presyn/README new file mode 100644 index 0000000..14aea33 --- /dev/null +++ b/scripts/presyn/README @@ -0,0 +1,5 @@ +A simple example for how to use Yosys to "pre-synthesize" PicoRV32 in +a way that can utilize an external memory module for the register file. + +See also: +https://github.com/cliffordwolf/picorv32/issues/30 diff --git a/scripts/presyn/firmware.S b/scripts/presyn/firmware.S new file mode 100644 index 0000000..ec5caaa --- /dev/null +++ b/scripts/presyn/firmware.S @@ -0,0 +1,47 @@ +.section .init +.global main + +entry: + +/* zero-initialize all registers */ +addi x1, zero, 0 +addi x2, zero, 0 +addi x3, zero, 0 +addi x4, zero, 0 +addi x5, zero, 0 +addi x6, zero, 0 +addi x7, zero, 0 +addi x8, zero, 0 +addi x9, zero, 0 +addi x10, zero, 0 +addi x11, zero, 0 +addi x12, zero, 0 +addi x13, zero, 0 +addi x14, zero, 0 +addi x15, zero, 0 +addi x16, zero, 0 +addi x17, zero, 0 +addi x18, zero, 0 +addi x19, zero, 0 +addi x20, zero, 0 +addi x21, zero, 0 +addi x22, zero, 0 +addi x23, zero, 0 +addi x24, zero, 0 +addi x25, zero, 0 +addi x26, zero, 0 +addi x27, zero, 0 +addi x28, zero, 0 +addi x29, zero, 0 +addi x30, zero, 0 +addi x31, zero, 0 + +/* set stack pointer */ +lui sp, %hi(16*1024) +addi sp, sp, %lo(16*1024) + +/* call main */ +jal ra, main + +/* break */ +ebreak diff --git a/scripts/presyn/firmware.c b/scripts/presyn/firmware.c new file mode 100644 index 0000000..6c62169 --- /dev/null +++ b/scripts/presyn/firmware.c @@ -0,0 +1,43 @@ +void putc(char c) +{ + *(volatile char*)0x10000000 = c; +} + +void puts(const char *s) +{ + while (*s) putc(*s++); +} + +void *memcpy(void *dest, const void *src, int n) +{ + while (n) { + n--; + ((char*)dest)[n] = ((char*)src)[n]; + } + return dest; +} + +void main() +{ + char message[] = "$Uryyb+Jbeyq!+Vs+lbh+pna+ernq+guvf+zrffntr+gura$gur+CvpbEI32+PCH" + "+frrzf+gb+or+jbexvat+whfg+svar.$$++++++++++++++++GRFG+CNFFRQ!$$"; + for (int i = 0; message[i]; i++) + switch (message[i]) + { + case 'a' ... 'm': + case 'A' ... 'M': + message[i] += 13; + break; + case 'n' ... 'z': + case 'N' ... 'Z': + message[i] -= 13; + break; + case '$': + message[i] = '\n'; + break; + case '+': + message[i] = ' '; + break; + } + puts(message); +} diff --git a/scripts/presyn/firmware.lds b/scripts/presyn/firmware.lds new file mode 100644 index 0000000..970000a --- /dev/null +++ b/scripts/presyn/firmware.lds @@ -0,0 +1,11 @@ +SECTIONS { + .memory : { + . = 0x000000; + *(.init); + *(.text); + *(*); + . = ALIGN(4); + end = .; + } +} + diff --git a/scripts/presyn/picorv32_presyn.ys b/scripts/presyn/picorv32_presyn.ys new file mode 100644 index 0000000..5855a21 --- /dev/null +++ b/scripts/presyn/picorv32_presyn.ys @@ -0,0 +1,5 @@ +read_verilog ../../picorv32.v +chparam -set COMPRESSED_ISA 1 picorv32 +prep -top picorv32 +memory_bram -rules picorv32_regs.txt +write_verilog -noattr picorv32_presyn.v diff --git a/scripts/presyn/picorv32_regs.txt b/scripts/presyn/picorv32_regs.txt new file mode 100644 index 0000000..1cfbbeb --- /dev/null +++ b/scripts/presyn/picorv32_regs.txt @@ -0,0 +1,16 @@ +bram picorv32_regs + init 0 + abits 5 + dbits 32 + groups 2 + ports 2 1 + wrmode 0 1 + enable 0 1 + transp 0 0 + clocks 1 1 + clkpol 1 1 +endbram + +match picorv32_regs + make_transp +endmatch diff --git a/scripts/presyn/testbench.v b/scripts/presyn/testbench.v new file mode 100644 index 0000000..59ff66b --- /dev/null +++ b/scripts/presyn/testbench.v @@ -0,0 +1,81 @@ +module testbench; + reg clk = 1; + always #5 clk = ~clk; + + reg resetn = 0; + always @(posedge clk) resetn <= 1; + + wire trap; + wire mem_valid; + wire mem_instr; + reg mem_ready; + wire [31:0] mem_addr; + wire [31:0] mem_wdata; + wire [3:0] mem_wstrb; + reg [31:0] mem_rdata; + + picorv32 UUT ( + .clk (clk ), + .resetn (resetn ), + .trap (trap ), + .mem_valid(mem_valid), + .mem_instr(mem_instr), + .mem_ready(mem_ready), + .mem_addr (mem_addr ), + .mem_wdata(mem_wdata), + .mem_wstrb(mem_wstrb), + .mem_rdata(mem_rdata) + ); + + // 4096 32bit words = 16kB memory + localparam MEM_SIZE = 4096; + + reg [31:0] memory [0:MEM_SIZE-1]; + initial $readmemh("firmware.hex", memory); + + always @(posedge clk) begin + mem_ready <= 0; + mem_rdata <= 'bx; + + if (resetn && mem_valid && !mem_ready) begin + mem_ready <= 1; + if (mem_wstrb) begin + if (mem_addr == 32'h1000_0000) begin + $write("%c", mem_wdata[7:0]); + $fflush; + end else begin + if (mem_wstrb[0]) memory[mem_addr >> 2][ 7: 0] <= mem_wdata[ 7: 0]; + if (mem_wstrb[1]) memory[mem_addr >> 2][15: 8] <= mem_wdata[15: 8]; + if (mem_wstrb[2]) memory[mem_addr >> 2][23:16] <= mem_wdata[23:16]; + if (mem_wstrb[3]) memory[mem_addr >> 2][31:24] <= mem_wdata[31:24]; + end + end else begin + mem_rdata <= memory[mem_addr >> 2]; + end + end + + if (resetn && trap) begin + $display("TRAP."); + $finish; + end + end + + initial begin + $dumpfile("testbench.vcd"); + $dumpvars(0, testbench); + end +endmodule + +module picorv32_regs ( + input [4:0] A1ADDR, A2ADDR, B1ADDR, + output reg [31:0] A1DATA, A2DATA, + input [31:0] B1DATA, + input B1EN, CLK1 +); + reg [31:0] memory [0:31]; + always @(posedge CLK1) begin + A1DATA <= memory[A1ADDR]; + A2DATA <= memory[A2ADDR]; + if (B1EN) memory[B1ADDR] <= B1DATA; + end +endmodule diff --git a/scripts/quartus/.gitignore b/scripts/quartus/.gitignore new file mode 100644 index 0000000..d37ca0a --- /dev/null +++ b/scripts/quartus/.gitignore @@ -0,0 +1,11 @@ +firmware.bin +firmware.elf +firmware.hex +firmware.map +synth_*.log +synth_*.mmi +synth_*.bit +synth_system.v +table.txt +tab_*/ +system_tb diff --git a/scripts/quartus/Makefile b/scripts/quartus/Makefile new file mode 100644 index 0000000..c644609 --- /dev/null +++ b/scripts/quartus/Makefile @@ -0,0 +1,62 @@ + +export QUARTUS_ROOTDIR = /opt/altera_lite/16.0 +export QUARTUS_BIN = $(QUARTUS_ROOTDIR)/quartus/bin + +VLOG = iverilog +TOOLCHAIN_PREFIX = /opt/riscv32i/bin/riscv32-unknown-elf- + +help: + @echo "" + @echo "Simple synthesis tests:" + @echo " make synth_area_{small|regular|large}" + @echo " make synth_speed" + @echo "" + @echo "Example system:" + @echo " make synth_system" + @echo " make sim_system" + @echo "" + @echo "Timing and Utilization Evaluation:" + @echo " make table.txt" + @echo " make area" + @echo "" + +synth_%: + rm -f $@.log + mkdir -p $@_build + cp $@.qsf $@_build + cd $@_build && $(QUARTUS_BIN)/quartus_map $@.qsf + cd $@_build && $(QUARTUS_BIN)/quartus_fit --read_settings_files=off -write_settings_files=off $@ -c $@ + cd $@_build && $(QUARTUS_BIN)/quartus_sta $@ -c $@ + -cd $@_build && grep -A3 "Total logic elements" output_files/$@.fit.summary + -cd $@_build && grep -B1 "Slack" output_files/$@.sta.summary + +synth_system: firmware.hex + +sim_system: firmware.hex system_tb.v system.v ../../picorv32.v + $(VLOG) -o system_tb system_tb.v system.v ../../picorv32.v + ./system_tb + +firmware.hex: firmware.S firmware.c firmware.lds + $(TOOLCHAIN_PREFIX)gcc -Os -ffreestanding -nostdlib -o firmware.elf firmware.S firmware.c \ + --std=gnu99 -Wl,-Bstatic,-T,firmware.lds,-Map,firmware.map,--strip-debug -lgcc + $(TOOLCHAIN_PREFIX)objcopy -O binary firmware.elf firmware.bin + python3 ../../firmware/makehex.py firmware.bin 4096 > firmware.hex + +tab_%/results.txt: + bash tabtest.sh $@ + +area: synth_area_small synth_area_regular synth_area_large + -grep -A3 "Total logic elements" synth_area_*_build/output_files/synth_area_*.fit.summary + +table.txt: tab_small_ep4ce_c7/results.txt +table.txt: tab_small_ep4cgx_c7/results.txt +table.txt: tab_small_5cgx_c7/results.txt + +table.txt: + bash table.sh > table.txt + +clean: + rm -rf firmware.bin firmware.elf firmware.hex firmware.map synth_*.log + rm -rf table.txt tab_*/ + rm -rf synth_*_build + diff --git a/scripts/quartus/firmware.S b/scripts/quartus/firmware.S new file mode 100644 index 0000000..c55a3ba --- /dev/null +++ b/scripts/quartus/firmware.S @@ -0,0 +1,12 @@ +.section .init +.global main + +/* set stack pointer */ +lui sp, %hi(16*1024) +addi sp, sp, %lo(16*1024) + +/* call main */ +jal ra, main + +/* break */ +ebreak diff --git a/scripts/quartus/firmware.c b/scripts/quartus/firmware.c new file mode 100644 index 0000000..6c62169 --- /dev/null +++ b/scripts/quartus/firmware.c @@ -0,0 +1,43 @@ +void putc(char c) +{ + *(volatile char*)0x10000000 = c; +} + +void puts(const char *s) +{ + while (*s) putc(*s++); +} + +void *memcpy(void *dest, const void *src, int n) +{ + while (n) { + n--; + ((char*)dest)[n] = ((char*)src)[n]; + } + return dest; +} + +void main() +{ + char message[] = "$Uryyb+Jbeyq!+Vs+lbh+pna+ernq+guvf+zrffntr+gura$gur+CvpbEI32+PCH" + "+frrzf+gb+or+jbexvat+whfg+svar.$$++++++++++++++++GRFG+CNFFRQ!$$"; + for (int i = 0; message[i]; i++) + switch (message[i]) + { + case 'a' ... 'm': + case 'A' ... 'M': + message[i] += 13; + break; + case 'n' ... 'z': + case 'N' ... 'Z': + message[i] -= 13; + break; + case '$': + message[i] = '\n'; + break; + case '+': + message[i] = ' '; + break; + } + puts(message); +} diff --git a/scripts/quartus/firmware.lds b/scripts/quartus/firmware.lds new file mode 100644 index 0000000..970000a --- /dev/null +++ b/scripts/quartus/firmware.lds @@ -0,0 +1,11 @@ +SECTIONS { + .memory : { + . = 0x000000; + *(.init); + *(.text); + *(*); + . = ALIGN(4); + end = .; + } +} + diff --git a/scripts/quartus/synth_area.sdc b/scripts/quartus/synth_area.sdc new file mode 100644 index 0000000..3c3d5a1 --- /dev/null +++ b/scripts/quartus/synth_area.sdc @@ -0,0 +1 @@ +create_clock -period 20.00 [get_ports clk] diff --git a/scripts/quartus/synth_area_large.qsf b/scripts/quartus/synth_area_large.qsf new file mode 100644 index 0000000..c09700b --- /dev/null +++ b/scripts/quartus/synth_area_large.qsf @@ -0,0 +1,6 @@ +set_global_assignment -name DEVICE ep4ce40f29c7 +set_global_assignment -name PROJECT_OUTPUT_DIRECTORY output_files +set_global_assignment -name TOP_LEVEL_ENTITY top_large +set_global_assignment -name VERILOG_FILE ../synth_area_top.v +set_global_assignment -name VERILOG_FILE ../../../picorv32.v +set_global_assignment -name SDC_FILE ../synth_area.sdc diff --git a/scripts/quartus/synth_area_regular.qsf b/scripts/quartus/synth_area_regular.qsf new file mode 100644 index 0000000..8507413 --- /dev/null +++ b/scripts/quartus/synth_area_regular.qsf @@ -0,0 +1,6 @@ +set_global_assignment -name DEVICE ep4ce40f29c7 +set_global_assignment -name PROJECT_OUTPUT_DIRECTORY output_files +set_global_assignment -name TOP_LEVEL_ENTITY top_regular +set_global_assignment -name VERILOG_FILE ../synth_area_top.v +set_global_assignment -name VERILOG_FILE ../../../picorv32.v +set_global_assignment -name SDC_FILE ../synth_area.sdc diff --git a/scripts/quartus/synth_area_small.qsf b/scripts/quartus/synth_area_small.qsf new file mode 100644 index 0000000..048ff96 --- /dev/null +++ b/scripts/quartus/synth_area_small.qsf @@ -0,0 +1,6 @@ +set_global_assignment -name DEVICE ep4ce40f29c7 +set_global_assignment -name PROJECT_OUTPUT_DIRECTORY output_files +set_global_assignment -name TOP_LEVEL_ENTITY top_small +set_global_assignment -name VERILOG_FILE ../synth_area_top.v +set_global_assignment -name VERILOG_FILE ../../../picorv32.v +set_global_assignment -name SDC_FILE ../synth_area.sdc diff --git a/scripts/quartus/synth_area_top.v b/scripts/quartus/synth_area_top.v new file mode 100644 index 0000000..6298a86 --- /dev/null +++ b/scripts/quartus/synth_area_top.v @@ -0,0 +1,140 @@ + +module top_small ( + input clk, resetn, + + output mem_valid, + output mem_instr, + input mem_ready, + + output [31:0] mem_addr, + output [31:0] mem_wdata, + output [ 3:0] mem_wstrb, + input [31:0] mem_rdata +); + picorv32 #( + .ENABLE_COUNTERS(0), + .LATCHED_MEM_RDATA(1), + .TWO_STAGE_SHIFT(0), + .CATCH_MISALIGN(0), + .CATCH_ILLINSN(0) + ) picorv32 ( + .clk (clk ), + .resetn (resetn ), + .mem_valid(mem_valid), + .mem_instr(mem_instr), + .mem_ready(mem_ready), + .mem_addr (mem_addr ), + .mem_wdata(mem_wdata), + .mem_wstrb(mem_wstrb), + .mem_rdata(mem_rdata) + ); +endmodule + +module top_regular ( + input clk, resetn, + output trap, + + output mem_valid, + output mem_instr, + input mem_ready, + + output [31:0] mem_addr, + output [31:0] mem_wdata, + output [ 3:0] mem_wstrb, + input [31:0] mem_rdata, + + // Look-Ahead Interface + output mem_la_read, + output mem_la_write, + output [31:0] mem_la_addr, + output [31:0] mem_la_wdata, + output [ 3:0] mem_la_wstrb +); + picorv32 picorv32 ( + .clk (clk ), + .resetn (resetn ), + .trap (trap ), + .mem_valid (mem_valid ), + .mem_instr (mem_instr ), + .mem_ready (mem_ready ), + .mem_addr (mem_addr ), + .mem_wdata (mem_wdata ), + .mem_wstrb (mem_wstrb ), + .mem_rdata (mem_rdata ), + .mem_la_read (mem_la_read ), + .mem_la_write(mem_la_write), + .mem_la_addr (mem_la_addr ), + .mem_la_wdata(mem_la_wdata), + .mem_la_wstrb(mem_la_wstrb) + ); +endmodule + +module top_large ( + input clk, resetn, + output trap, + + output mem_valid, + output mem_instr, + input mem_ready, + + output [31:0] mem_addr, + output [31:0] mem_wdata, + output [ 3:0] mem_wstrb, + input [31:0] mem_rdata, + + // Look-Ahead Interface + output mem_la_read, + output mem_la_write, + output [31:0] mem_la_addr, + output [31:0] mem_la_wdata, + output [ 3:0] mem_la_wstrb, + + // Pico Co-Processor Interface (PCPI) + output pcpi_valid, + output [31:0] pcpi_insn, + output [31:0] pcpi_rs1, + output [31:0] pcpi_rs2, + input pcpi_wr, + input [31:0] pcpi_rd, + input pcpi_wait, + input pcpi_ready, + + // IRQ Interface + input [31:0] irq, + output [31:0] eoi +); + picorv32 #( + .COMPRESSED_ISA(1), + .BARREL_SHIFTER(1), + .ENABLE_PCPI(1), + .ENABLE_MUL(1), + .ENABLE_IRQ(1) + ) picorv32 ( + .clk (clk ), + .resetn (resetn ), + .trap (trap ), + .mem_valid (mem_valid ), + .mem_instr (mem_instr ), + .mem_ready (mem_ready ), + .mem_addr (mem_addr ), + .mem_wdata (mem_wdata ), + .mem_wstrb (mem_wstrb ), + .mem_rdata (mem_rdata ), + .mem_la_read (mem_la_read ), + .mem_la_write (mem_la_write ), + .mem_la_addr (mem_la_addr ), + .mem_la_wdata (mem_la_wdata ), + .mem_la_wstrb (mem_la_wstrb ), + .pcpi_valid (pcpi_valid ), + .pcpi_insn (pcpi_insn ), + .pcpi_rs1 (pcpi_rs1 ), + .pcpi_rs2 (pcpi_rs2 ), + .pcpi_wr (pcpi_wr ), + .pcpi_rd (pcpi_rd ), + .pcpi_wait (pcpi_wait ), + .pcpi_ready (pcpi_ready ), + .irq (irq ), + .eoi (eoi ) + ); +endmodule + diff --git a/scripts/quartus/synth_speed.qsf b/scripts/quartus/synth_speed.qsf new file mode 100644 index 0000000..64490d4 --- /dev/null +++ b/scripts/quartus/synth_speed.qsf @@ -0,0 +1,5 @@ +set_global_assignment -name DEVICE ep4ce40f29c7 +set_global_assignment -name PROJECT_OUTPUT_DIRECTORY output_files +set_global_assignment -name TOP_LEVEL_ENTITY picorv32_axi +set_global_assignment -name VERILOG_FILE ../../../picorv32.v +set_global_assignment -name SDC_FILE ../synth_speed.sdc diff --git a/scripts/quartus/synth_speed.sdc b/scripts/quartus/synth_speed.sdc new file mode 100644 index 0000000..fef5704 --- /dev/null +++ b/scripts/quartus/synth_speed.sdc @@ -0,0 +1 @@ +create_clock -period 2.5 [get_ports clk] diff --git a/scripts/quartus/synth_system.qsf b/scripts/quartus/synth_system.qsf new file mode 100644 index 0000000..1a84293 --- /dev/null +++ b/scripts/quartus/synth_system.qsf @@ -0,0 +1,6 @@ +set_global_assignment -name DEVICE ep4ce40f29c7 +set_global_assignment -name PROJECT_OUTPUT_DIRECTORY output_files +set_global_assignment -name TOP_LEVEL_ENTITY system +set_global_assignment -name VERILOG_FILE ../system.v +set_global_assignment -name VERILOG_FILE ../../../picorv32.v +set_global_assignment -name SDC_FILE ../synth_system.sdc diff --git a/scripts/quartus/synth_system.sdc b/scripts/quartus/synth_system.sdc new file mode 100644 index 0000000..90ee3a2 --- /dev/null +++ b/scripts/quartus/synth_system.sdc @@ -0,0 +1 @@ +create_clock -period 10.00 [get_ports clk] diff --git a/scripts/quartus/synth_system.tcl b/scripts/quartus/synth_system.tcl new file mode 100644 index 0000000..26ea01c --- /dev/null +++ b/scripts/quartus/synth_system.tcl @@ -0,0 +1,17 @@ + +read_verilog system.v +read_verilog ../../picorv32.v +read_xdc synth_system.xdc + +synth_design -part xc7a35t-cpg236-1 -top system +opt_design +place_design +route_design + +report_utilization +report_timing + +write_verilog -force synth_system.v +write_bitstream -force synth_system.bit +# write_mem_info -force synth_system.mmi + diff --git a/scripts/quartus/system.v b/scripts/quartus/system.v new file mode 100644 index 0000000..19a4b8d --- /dev/null +++ b/scripts/quartus/system.v @@ -0,0 +1,101 @@ +`timescale 1 ns / 1 ps + +module system ( + input clk, + input resetn, + output trap, + output reg [7:0] out_byte, + output reg out_byte_en +); + // set this to 0 for better timing but less performance/MHz + parameter FAST_MEMORY = 0; + + // 4096 32bit words = 16kB memory + parameter MEM_SIZE = 4096; + + wire mem_valid; + wire mem_instr; + reg mem_ready; + wire [31:0] mem_addr; + wire [31:0] mem_wdata; + wire [3:0] mem_wstrb; + reg [31:0] mem_rdata; + + wire mem_la_read; + wire mem_la_write; + wire [31:0] mem_la_addr; + wire [31:0] mem_la_wdata; + wire [3:0] mem_la_wstrb; + + picorv32 picorv32_core ( + .clk (clk ), + .resetn (resetn ), + .trap (trap ), + .mem_valid (mem_valid ), + .mem_instr (mem_instr ), + .mem_ready (mem_ready ), + .mem_addr (mem_addr ), + .mem_wdata (mem_wdata ), + .mem_wstrb (mem_wstrb ), + .mem_rdata (mem_rdata ), + .mem_la_read (mem_la_read ), + .mem_la_write(mem_la_write), + .mem_la_addr (mem_la_addr ), + .mem_la_wdata(mem_la_wdata), + .mem_la_wstrb(mem_la_wstrb) + ); + + reg [31:0] memory [0:MEM_SIZE-1]; + initial $readmemh("firmware.hex", memory); + + reg [31:0] m_read_data; + reg m_read_en; + + generate if (FAST_MEMORY) begin + always @(posedge clk) begin + mem_ready <= 1; + out_byte_en <= 0; + mem_rdata <= memory[mem_la_addr >> 2]; + if (mem_la_write && (mem_la_addr >> 2) < MEM_SIZE) begin + if (mem_la_wstrb[0]) memory[mem_la_addr >> 2][ 7: 0] <= mem_la_wdata[ 7: 0]; + if (mem_la_wstrb[1]) memory[mem_la_addr >> 2][15: 8] <= mem_la_wdata[15: 8]; + if (mem_la_wstrb[2]) memory[mem_la_addr >> 2][23:16] <= mem_la_wdata[23:16]; + if (mem_la_wstrb[3]) memory[mem_la_addr >> 2][31:24] <= mem_la_wdata[31:24]; + end + else + if (mem_la_write && mem_la_addr == 32'h1000_0000) begin + out_byte_en <= 1; + out_byte <= mem_la_wdata; + end + end + end else begin + always @(posedge clk) begin + m_read_en <= 0; + mem_ready <= mem_valid && !mem_ready && m_read_en; + + m_read_data <= memory[mem_addr >> 2]; + mem_rdata <= m_read_data; + + out_byte_en <= 0; + + (* parallel_case *) + case (1) + mem_valid && !mem_ready && !mem_wstrb && (mem_addr >> 2) < MEM_SIZE: begin + m_read_en <= 1; + end + mem_valid && !mem_ready && |mem_wstrb && (mem_addr >> 2) < MEM_SIZE: begin + if (mem_wstrb[0]) memory[mem_addr >> 2][ 7: 0] <= mem_wdata[ 7: 0]; + if (mem_wstrb[1]) memory[mem_addr >> 2][15: 8] <= mem_wdata[15: 8]; + if (mem_wstrb[2]) memory[mem_addr >> 2][23:16] <= mem_wdata[23:16]; + if (mem_wstrb[3]) memory[mem_addr >> 2][31:24] <= mem_wdata[31:24]; + mem_ready <= 1; + end + mem_valid && !mem_ready && |mem_wstrb && mem_addr == 32'h1000_0000: begin + out_byte_en <= 1; + out_byte <= mem_wdata; + mem_ready <= 1; + end + endcase + end + end endgenerate +endmodule diff --git a/scripts/quartus/system_tb.v b/scripts/quartus/system_tb.v new file mode 100644 index 0000000..a66d612 --- /dev/null +++ b/scripts/quartus/system_tb.v @@ -0,0 +1,38 @@ +`timescale 1 ns / 1 ps + +module system_tb; + reg clk = 1; + always #5 clk = ~clk; + + reg resetn = 0; + initial begin + if ($test$plusargs("vcd")) begin + $dumpfile("system.vcd"); + $dumpvars(0, system_tb); + end + repeat (100) @(posedge clk); + resetn <= 1; + end + + wire trap; + wire [7:0] out_byte; + wire out_byte_en; + + system uut ( + .clk (clk ), + .resetn (resetn ), + .trap (trap ), + .out_byte (out_byte ), + .out_byte_en(out_byte_en) + ); + + always @(posedge clk) begin + if (resetn && out_byte_en) begin + $write("%c", out_byte); + $fflush; + end + if (resetn && trap) begin + $finish; + end + end +endmodule diff --git a/scripts/quartus/table.sh b/scripts/quartus/table.sh new file mode 100644 index 0000000..f5e6efe --- /dev/null +++ b/scripts/quartus/table.sh @@ -0,0 +1,17 @@ +#!/bin/bash + +dashes="----------------------------------------------------------------" +printf '| %-25s | %-10s | %-20s |\n' "Device" "Speedgrade" "Clock Period (Freq.)" +printf '|:%.25s |:%.10s:| %.20s:|\n' $dashes $dashes $dashes + +for x in $( grep -H . tab_*/results.txt ) +do + read _ size device grade _ speed < <( echo "$x" | tr _/: ' ' ) + case "$device" in + ep4ce) d="Altera Cyclone IV E" ;; + ep4cgx) d="Altera Cyclone IV GX" ;; + 5cgx) d="Altera Cyclone V GX" ;; + esac + speedtxt=$( printf '%s.%s ns (%d MHz)' ${speed%?} ${speed#?} $((10000 / speed)) ) + printf '| %-25s | %-10s | %20s |\n' "$d" "-$grade" "$speedtxt" +done diff --git a/scripts/quartus/tabtest.sh b/scripts/quartus/tabtest.sh new file mode 100644 index 0000000..2fd1b40 --- /dev/null +++ b/scripts/quartus/tabtest.sh @@ -0,0 +1,78 @@ +#!/bin/bash + +set -e +read _ ip dev grade _ < <( echo $* | tr '_/' ' '; ) + +# rm -rf tab_${ip}_${dev}_${grade} +mkdir -p tab_${ip}_${dev}_${grade} +cd tab_${ip}_${dev}_${grade} + +max_speed=99 +min_speed=01 +best_speed=99 + +synth_case() { + if [ -f test_${1}.txt ]; then + echo "Reusing cached tab_${ip}_${dev}_${grade}/test_${1}." + return + fi + + case "${dev}" in + ep4ce) al_device="ep4ce30f23${grade}" ;; + ep4cgx) al_device="ep4cgx50df27${grade}" ;; + 5cgx) al_device="5cgxbc9c6f23${grade}" ;; + esac + + cat > test_${1}.qsf <<- EOT +set_global_assignment -name DEVICE ${al_device} +set_global_assignment -name PROJECT_OUTPUT_DIRECTORY output_files +set_global_assignment -name TOP_LEVEL_ENTITY top +set_global_assignment -name VERILOG_FILE ../tabtest.v +set_global_assignment -name VERILOG_FILE ../../../picorv32.v +set_global_assignment -name SDC_FILE test_${1}.sdc + EOT + + cat > test_${1}.sdc <<- EOT + create_clock -period ${speed%?}.${speed#?} [get_ports clk] + EOT + + echo "Running tab_${ip}_${dev}_${grade}/test_${1}.." + + if ! $QUARTUS_BIN/quartus_map test_${1}; then + exit 1 + fi + if ! $QUARTUS_BIN/quartus_fit --read_settings_files=off --write_settings_files=off test_${1} -c test_${1}; then + exit 1 + fi + if ! $QUARTUS_BIN/quartus_sta test_${1} -c test_${1}; then + exit 1 + fi + + cp output_files/test_${1}.sta.summary test_${1}.txt +} + +countdown=7 +while [ $countdown -gt 0 ]; do + speed=$(((max_speed+min_speed)/2)) + synth_case $speed + + if grep -q '^Slack : -' test_${speed}.txt; then + echo " tab_${ip}_${dev}_${grade}/test_${speed} VIOLATED" + min_speed=$((speed)) + elif grep -q '^Slack : [^-]' test_${speed}.txt; then + echo " tab_${ip}_${dev}_${grade}/test_${speed} MET" + [ $speed -lt $best_speed ] && best_speed=$speed + max_speed=$((speed)) + else + echo "ERROR: No slack line found in $PWD/test_${speed}.txt!" + exit 1 + fi + + countdown=$((countdown-1)) +done + +echo "-----------------------" +echo "Best speed for tab_${ip}_${dev}_${grade}: $best_speed" +echo "-----------------------" +echo $best_speed > results.txt + diff --git a/scripts/quartus/tabtest.v b/scripts/quartus/tabtest.v new file mode 100644 index 0000000..cdf2057 --- /dev/null +++ b/scripts/quartus/tabtest.v @@ -0,0 +1,118 @@ + +module top ( + input clk, io_resetn, + output io_trap, + + output io_mem_axi_awvalid, + input io_mem_axi_awready, + output [31:0] io_mem_axi_awaddr, + output [ 2:0] io_mem_axi_awprot, + + output io_mem_axi_wvalid, + input io_mem_axi_wready, + output [31:0] io_mem_axi_wdata, + output [ 3:0] io_mem_axi_wstrb, + + input io_mem_axi_bvalid, + output io_mem_axi_bready, + + output io_mem_axi_arvalid, + input io_mem_axi_arready, + output [31:0] io_mem_axi_araddr, + output [ 2:0] io_mem_axi_arprot, + + input io_mem_axi_rvalid, + output io_mem_axi_rready, + input [31:0] io_mem_axi_rdata, + + input [31:0] io_irq, + output [31:0] io_eoi +); + wire resetn; + wire trap; + wire mem_axi_awvalid; + wire mem_axi_awready; + wire [31:0] mem_axi_awaddr; + wire [2:0] mem_axi_awprot; + wire mem_axi_wvalid; + wire mem_axi_wready; + wire [31:0] mem_axi_wdata; + wire [3:0] mem_axi_wstrb; + wire mem_axi_bvalid; + wire mem_axi_bready; + wire mem_axi_arvalid; + wire mem_axi_arready; + wire [31:0] mem_axi_araddr; + wire [2:0] mem_axi_arprot; + wire mem_axi_rvalid; + wire mem_axi_rready; + wire [31:0] mem_axi_rdata; + wire [31:0] irq; + wire [31:0] eoi; + + delay4 #( 1) delay_resetn (clk, io_resetn , resetn ); + delay4 #( 1) delay_trap (clk, trap , io_trap ); + delay4 #( 1) delay_mem_axi_awvalid (clk, mem_axi_awvalid, io_mem_axi_awvalid); + delay4 #( 1) delay_mem_axi_awready (clk, io_mem_axi_awready, mem_axi_awready); + delay4 #(32) delay_mem_axi_awaddr (clk, mem_axi_awaddr , io_mem_axi_awaddr ); + delay4 #( 3) delay_mem_axi_awprot (clk, mem_axi_awprot , io_mem_axi_awprot ); + delay4 #( 1) delay_mem_axi_wvalid (clk, mem_axi_wvalid , io_mem_axi_wvalid ); + delay4 #( 1) delay_mem_axi_wready (clk, io_mem_axi_wready , mem_axi_wready ); + delay4 #(32) delay_mem_axi_wdata (clk, mem_axi_wdata , io_mem_axi_wdata ); + delay4 #( 4) delay_mem_axi_wstrb (clk, mem_axi_wstrb , io_mem_axi_wstrb ); + delay4 #( 1) delay_mem_axi_bvalid (clk, io_mem_axi_bvalid , mem_axi_bvalid ); + delay4 #( 1) delay_mem_axi_bready (clk, mem_axi_bready , io_mem_axi_bready ); + delay4 #( 1) delay_mem_axi_arvalid (clk, mem_axi_arvalid, io_mem_axi_arvalid); + delay4 #( 1) delay_mem_axi_arready (clk, io_mem_axi_arready, mem_axi_arready); + delay4 #(32) delay_mem_axi_araddr (clk, mem_axi_araddr , io_mem_axi_araddr ); + delay4 #( 3) delay_mem_axi_arprot (clk, mem_axi_arprot , io_mem_axi_arprot ); + delay4 #( 1) delay_mem_axi_rvalid (clk, io_mem_axi_rvalid , mem_axi_rvalid ); + delay4 #( 1) delay_mem_axi_rready (clk, mem_axi_rready , io_mem_axi_rready ); + delay4 #(32) delay_mem_axi_rdata (clk, io_mem_axi_rdata , mem_axi_rdata ); + delay4 #(32) delay_irq (clk, io_irq , irq ); + delay4 #(32) delay_eoi (clk, eoi , io_eoi ); + + picorv32_axi #( + .TWO_CYCLE_ALU(1) + ) cpu ( + .clk (clk ), + .resetn (resetn ), + .trap (trap ), + .mem_axi_awvalid(mem_axi_awvalid), + .mem_axi_awready(mem_axi_awready), + .mem_axi_awaddr (mem_axi_awaddr ), + .mem_axi_awprot (mem_axi_awprot ), + .mem_axi_wvalid (mem_axi_wvalid ), + .mem_axi_wready (mem_axi_wready ), + .mem_axi_wdata (mem_axi_wdata ), + .mem_axi_wstrb (mem_axi_wstrb ), + .mem_axi_bvalid (mem_axi_bvalid ), + .mem_axi_bready (mem_axi_bready ), + .mem_axi_arvalid(mem_axi_arvalid), + .mem_axi_arready(mem_axi_arready), + .mem_axi_araddr (mem_axi_araddr ), + .mem_axi_arprot (mem_axi_arprot ), + .mem_axi_rvalid (mem_axi_rvalid ), + .mem_axi_rready (mem_axi_rready ), + .mem_axi_rdata (mem_axi_rdata ), + .irq (irq ), + .eoi (eoi ) + ); +endmodule + +module delay4 #( + parameter WIDTH = 1 +) ( + input clk, + input [WIDTH-1:0] in, + output reg [WIDTH-1:0] out +); + reg [WIDTH-1:0] q1, q2, q3; + always @(posedge clk) begin + q1 <= in; + q2 <= q1; + q3 <= q2; + out <= q3; + end +endmodule + diff --git a/scripts/romload/.gitignore b/scripts/romload/.gitignore new file mode 100644 index 0000000..6f1295b --- /dev/null +++ b/scripts/romload/.gitignore @@ -0,0 +1,11 @@ +firmware.d +firmware.elf +firmware.hex +firmware32.hex +firmware.o +firmware_addr.txt +firmware_dbg.v +syscalls.o +testbench.vvp +testbench.vcd +start.elf diff --git a/scripts/romload/Makefile b/scripts/romload/Makefile new file mode 100644 index 0000000..d510fa8 --- /dev/null +++ b/scripts/romload/Makefile @@ -0,0 +1,41 @@ +ifndef RISCV_TOOLS_PREFIX +RISCV_TOOLS_PREFIX = /opt/riscv32ic/bin/riscv32-unknown-elf- +endif +CXX = $(RISCV_TOOLS_PREFIX)g++ -march=rv32i +CC = $(RISCV_TOOLS_PREFIX)gcc -march=rv32i +AS = $(RISCV_TOOLS_PREFIX)gcc -march=rv32i +CXXFLAGS = -MD -Os -Wall -std=c++11 +CCFLAGS = -MD -Os -Wall +#LDFLAGS = -Wl,--gc-sections,--no-relax +LDFLAGS = -Wl,--gc-sections +LDLIBS = + +test: testbench.vvp firmware32.hex + vvp -l testbench.log -N testbench.vvp + +testbench.vvp: testbench.v ../../picorv32.v firmware_dbg.v + iverilog -o testbench.vvp testbench.v ../../picorv32.v + chmod -x testbench.vvp + +firmware32.hex: firmware.elf hex8tohex32.py + $(RISCV_TOOLS_PREFIX)objcopy -O verilog firmware.elf firmware.tmp + python3 hex8tohex32.py firmware.tmp > firmware32.hex + + +firmware_dbg.v: firmware.map + python3 map2debug.py + +start.o: start.S + $(CC) -c -nostdlib start.S $(LDLIBS) + +firmware.elf: firmware.o syscalls.o start.o + $(CC) $(LDFLAGS),-Map=firmware.map -o $@ $^ -T sections.ld $(LDLIBS) + chmod -x firmware.elf + +clean: + rm -f *.o *.d *.tmp start.elf + rm -f firmware.elf firmware.hex firmware32.hex + rm -f testbench.vvp testbench.vcd + +-include *.d +.PHONY: test clean diff --git a/scripts/romload/firmware.c b/scripts/romload/firmware.c new file mode 100644 index 0000000..4bc9ed8 --- /dev/null +++ b/scripts/romload/firmware.c @@ -0,0 +1,21 @@ +#include <stdio.h> +#include <stdlib.h> + +int x1 = 1000; +int x2 = 2000; + +void main() +{ + int z; + x1 = 50; + x2 = 50; + + printf("hello\n"); + z = (x1 + x2); + if (z == 100) + printf("TEST PASSED\n"); + else + printf("TEST FAILED, z=%d\n", z); + exit(0); +} + diff --git a/scripts/romload/hex8tohex32.py b/scripts/romload/hex8tohex32.py new file mode 100644 index 0000000..ae44101 --- /dev/null +++ b/scripts/romload/hex8tohex32.py @@ -0,0 +1,34 @@ +#!/usr/bin/env python3 + +import fileinput +import itertools + +ptr = 0 +data = [] + +def write_data(): + if len(data) != 0: + print("@%08x" % (ptr >> 2)) + while len(data) % 4 != 0: + data.append(0) + for word_bytes in zip(*([iter(data)]*4)): + print("".join(["%02x" % b for b in reversed(word_bytes)])) + +for line in fileinput.input(): + if line.startswith("@"): + addr = int(line[1:], 16) + if addr > ptr+4: + write_data() + ptr = addr + data = [] + while ptr % 4 != 0: + data.append(0) + ptr -= 1 + else: + while ptr + len(data) < addr: + data.append(0) + else: + data += [int(tok, 16) for tok in line.split()] + +write_data() + diff --git a/scripts/romload/map2debug.py b/scripts/romload/map2debug.py new file mode 100644 index 0000000..fc5c97c --- /dev/null +++ b/scripts/romload/map2debug.py @@ -0,0 +1,30 @@ +#!/usr/bin/env python3 + +import re + +symbol = re.compile("\s*0x([0-9a-f]+)\s+([\w_]+)") +symbol_map = {} +with open("firmware.map", "r") as fh: + for fd in fh: + sym = symbol.match(fd) + if (sym): + addr = int(sym.group(1), 16) + symbol_map[addr] = sym.group(2) + +with open("firmware_dbg.v", "w") as fh: + for k, v in symbol_map.items(): + fh.write("`define C_SYM_{1:s} 32'h{0:08x}\n".format(k, v.upper())) + fh.write(" task firmware_dbg;\n") + fh.write(" input [31:0] addr;\n"); + fh.write(" begin\n"); + fh.write(" case (addr)\n"); + for k, v in symbol_map.items(): + fh.write(" 32'h{0:08x} : $display(\"%t: FCALL: {1:s}\", $time);\n".format(k, v)) + fh.write(" endcase\n"); + fh.write(" end\n"); + fh.write(" endtask\n"); + +with open("firmware_addr.txt", "w") as fh: + for k, v in symbol_map.items(): + fh.write("{0:08x} {1:s}\n".format(k,v)) + diff --git a/scripts/romload/sections.ld b/scripts/romload/sections.ld new file mode 100644 index 0000000..2ec3954 --- /dev/null +++ b/scripts/romload/sections.ld @@ -0,0 +1,45 @@ +/* +This is free and unencumbered software released into the public domain. + +Anyone is free to copy, modify, publish, use, compile, sell, or +distribute this software, either in source code form or as a compiled +binary, for any purpose, commercial or non-commercial, and by any +means. +*/ + +/* starting address needs to be > 0 due to known bug in RISCV/GNU linker */ +MEMORY { + rom(rwx) : ORIGIN = 0x00000100, LENGTH = 63k + ram(rwx) : ORIGIN = 0x00020000, LENGTH = 16k +} + +ENTRY(_pvstart); + +SECTIONS { + .rom : { + _pvstart*(.text); + start*(.text); + . = 0x100; + . = ALIGN(4); + *(.text); + } > rom + + .data : { + _data_lma = LOADADDR(.data); + _data = .; + __global_pointer$ = . ; + *(.data .data.* ) + *(.sdata .sdata.*) + . = ALIGN(4); + _edata = .; + } >ram AT>rom + + .bss : { + _bss_start = .; + *(.bss .bss.*) + . = ALIGN(4); + _bss_end = .; + _end = .; + } >ram + +} diff --git a/scripts/romload/start.S b/scripts/romload/start.S new file mode 100644 index 0000000..be59808 --- /dev/null +++ b/scripts/romload/start.S @@ -0,0 +1,52 @@ +.section .text +.global _start +.global _pvstart + +_pvstart: +/* zero-initialize all registers */ +addi x1, zero, 0 +addi x2, zero, 0 +addi x3, zero, 0 +addi x4, zero, 0 +addi x5, zero, 0 +addi x6, zero, 0 +addi x7, zero, 0 +addi x8, zero, 0 +addi x9, zero, 0 +addi x10, zero, 0 +addi x11, zero, 0 +addi x12, zero, 0 +addi x13, zero, 0 +addi x14, zero, 0 +addi x15, zero, 0 +addi x16, zero, 0 +addi x17, zero, 0 +addi x18, zero, 0 +addi x19, zero, 0 +addi x20, zero, 0 +addi x21, zero, 0 +addi x22, zero, 0 +addi x23, zero, 0 +addi x24, zero, 0 +addi x25, zero, 0 +addi x26, zero, 0 +addi x27, zero, 0 +addi x28, zero, 0 +addi x29, zero, 0 +addi x30, zero, 0 +addi x31, zero, 0 + +/* set stack pointer */ + +lui sp, %hi(4*1024*1024) +addi sp, sp, %lo(4*1024*1024) + +/* push zeros on the stack for argc and argv */ +/* (stack is aligned to 16 bytes in riscv calling convention) */ +addi sp,sp,-16 +sw zero,0(sp) +sw zero,4(sp) +sw zero,8(sp) +sw zero,12(sp) + +j _start diff --git a/scripts/romload/syscalls.c b/scripts/romload/syscalls.c new file mode 100644 index 0000000..8ea84ca --- /dev/null +++ b/scripts/romload/syscalls.c @@ -0,0 +1,95 @@ +// An extremely minimalist syscalls.c for newlib +// Based on riscv newlib libgloss/riscv/sys_*.c +// Written by Clifford Wolf. + +#include <sys/stat.h> +#include <unistd.h> +#include <errno.h> + +#define UNIMPL_FUNC(_f) ".globl " #_f "\n.type " #_f ", @function\n" #_f ":\n" + +asm ( + ".text\n" + ".align 2\n" + UNIMPL_FUNC(_open) + UNIMPL_FUNC(_openat) + UNIMPL_FUNC(_lseek) + UNIMPL_FUNC(_stat) + UNIMPL_FUNC(_lstat) + UNIMPL_FUNC(_fstatat) + UNIMPL_FUNC(_isatty) + UNIMPL_FUNC(_access) + UNIMPL_FUNC(_faccessat) + UNIMPL_FUNC(_link) + UNIMPL_FUNC(_unlink) + UNIMPL_FUNC(_execve) + UNIMPL_FUNC(_getpid) + UNIMPL_FUNC(_fork) + UNIMPL_FUNC(_kill) + UNIMPL_FUNC(_wait) + UNIMPL_FUNC(_times) + UNIMPL_FUNC(_gettimeofday) + UNIMPL_FUNC(_ftime) + UNIMPL_FUNC(_utime) + UNIMPL_FUNC(_chown) + UNIMPL_FUNC(_chmod) + UNIMPL_FUNC(_chdir) + UNIMPL_FUNC(_getcwd) + UNIMPL_FUNC(_sysconf) + "j unimplemented_syscall\n" +); + +void unimplemented_syscall() +{ + const char *p = "Unimplemented system call called!\n"; + while (*p) + *(volatile int*)0x10000000 = *(p++); + asm volatile ("ebreak"); + __builtin_unreachable(); +} + +ssize_t _read(int file, void *ptr, size_t len) +{ + // always EOF + return 0; +} + +ssize_t _write(int file, const void *ptr, size_t len) +{ + const void *eptr = ptr + len; + while (ptr != eptr) + *(volatile int*)0x10000000 = *(char*)(ptr++); + return len; +} + +int _close(int file) +{ + // close is called before _exit() + return 0; +} + +int _fstat(int file, struct stat *st) +{ + // fstat is called during libc startup + errno = ENOENT; + return -1; +} + +void *_sbrk(ptrdiff_t incr) +{ + extern unsigned char _end[]; // Defined by linker + static unsigned long heap_end; + + if (heap_end == 0) + heap_end = (long)_end; + + heap_end += incr; + return (void *)(heap_end - incr); +} + +void _exit(int exit_status) +{ + asm volatile ("ebreak"); + __builtin_unreachable(); +} + diff --git a/scripts/romload/testbench.v b/scripts/romload/testbench.v new file mode 100644 index 0000000..e38819d --- /dev/null +++ b/scripts/romload/testbench.v @@ -0,0 +1,140 @@ +`timescale 1 ns / 1 ps +`undef VERBOSE_MEM +//`undef WRITE_VCD +`undef MEM8BIT + +// define the size of our ROM +// simulates ROM by suppressing writes below this address +`define ROM_SIZE 32'h0001_00FF + +module testbench; + reg clk = 1; + reg resetn = 0; + wire trap; + + always #5 clk = ~clk; + + initial begin + repeat (100) @(posedge clk); + resetn <= 1; + end + + wire mem_valid; + wire mem_instr; + reg mem_ready; + wire [31:0] mem_addr; + wire [31:0] mem_wdata; + wire [3:0] mem_wstrb; + reg [31:0] mem_rdata; + +`include "firmware_dbg.v" + + picorv32 #( + .COMPRESSED_ISA(1), + .PROGADDR_RESET(32'h100) + ) uut ( + .clk (clk ), + .resetn (resetn ), + .trap (trap ), + .mem_valid (mem_valid ), + .mem_instr (mem_instr ), + .mem_ready (mem_ready ), + .mem_addr (mem_addr ), + .mem_wdata (mem_wdata ), + .mem_wstrb (mem_wstrb ), + .mem_rdata (mem_rdata ) + ); + + localparam MEM_SIZE = 4*1024*1024; +`ifdef MEM8BIT + reg [7:0] memory [0:MEM_SIZE-1]; + initial + $readmemh("firmware.hex", memory); + end +`else + reg [31:0] memory [0:MEM_SIZE/4-1]; + integer x; + + // simulate hardware assist of clearing RAM and copying ROM data into + // memory + initial + begin + // clear memory + for (x=0; x<MEM_SIZE/4; x=x+1) memory[x] = 0; + // load rom contents + $readmemh("firmware32.hex", memory); + // copy .data section + for (x=0; x<(`C_SYM__BSS_START - `C_SYM___GLOBAL_POINTER); x=x+4) + memory[(`C_SYM___GLOBAL_POINTER+x)/4] = memory[(`C_SYM__DATA_LMA+x)/4]; + end +`endif + + always @(posedge clk) begin + mem_ready <= 0; + if (mem_valid && !mem_ready) begin + mem_ready <= 1; + mem_rdata <= 'bx; + case (1) + mem_addr < MEM_SIZE: begin +`ifdef MEM8BIT + if (|mem_wstrb) begin + if (mem_wstrb[0]) memory[mem_addr + 0] <= mem_wdata[ 7: 0]; + if (mem_wstrb[1]) memory[mem_addr + 1] <= mem_wdata[15: 8]; + if (mem_wstrb[2]) memory[mem_addr + 2] <= mem_wdata[23:16]; + if (mem_wstrb[3]) memory[mem_addr + 3] <= mem_wdata[31:24]; + end else begin + mem_rdata <= {memory[mem_addr+3], memory[mem_addr+2], memory[mem_addr+1], memory[mem_addr]}; + end +`else + if ((|mem_wstrb) && (mem_addr >= `ROM_SIZE)) begin + if (mem_wstrb[0]) memory[mem_addr >> 2][ 7: 0] <= mem_wdata[ 7: 0]; + if (mem_wstrb[1]) memory[mem_addr >> 2][15: 8] <= mem_wdata[15: 8]; + if (mem_wstrb[2]) memory[mem_addr >> 2][23:16] <= mem_wdata[23:16]; + if (mem_wstrb[3]) memory[mem_addr >> 2][31:24] <= mem_wdata[31:24]; + end else begin + mem_rdata <= memory[mem_addr >> 2]; + end +`endif + end + mem_addr == 32'h 1000_0000: begin + $write("%c", mem_wdata[7:0]); + end + endcase + end + if (mem_valid && mem_ready) begin +`ifdef FIRMWARE_DEBUG_ADDR + firmware_dbg(mem_addr); +`endif + if ((mem_wstrb == 4'h0) && (mem_rdata === 32'bx)) $display("READ FROM UNITIALIZED ADDR=%x", mem_addr); +`ifdef VERBOSE_MEM + if (|mem_wstrb) + $display("WR: ADDR=%x DATA=%x MASK=%b", mem_addr, mem_wdata, mem_wstrb); + else + $display("RD: ADDR=%x DATA=%x%s", mem_addr, mem_rdata, mem_instr ? " INSN" : ""); +`endif + if (^mem_addr === 1'bx || + (mem_wstrb[0] && ^mem_wdata[ 7: 0] == 1'bx) || + (mem_wstrb[1] && ^mem_wdata[15: 8] == 1'bx) || + (mem_wstrb[2] && ^mem_wdata[23:16] == 1'bx) || + (mem_wstrb[3] && ^mem_wdata[31:24] == 1'bx)) begin + $display("CRITICAL UNDEF MEM TRANSACTION"); + $finish; + end + end + end + +`ifdef WRITE_VCD + initial begin + $dumpfile("testbench.vcd"); + $dumpvars(0, testbench); + end +`endif + + always @(posedge clk) begin + if (resetn && trap) begin + repeat (10) @(posedge clk); + $display("TRAP"); + $finish; + end + end +endmodule diff --git a/scripts/smtbmc/.gitignore b/scripts/smtbmc/.gitignore new file mode 100644 index 0000000..1ce906e --- /dev/null +++ b/scripts/smtbmc/.gitignore @@ -0,0 +1,18 @@ +tracecmp.smt2 +tracecmp.yslog +tracecmp2.smt2 +tracecmp2.yslog +tracecmp3.blif +tracecmp3.cex +tracecmp3.smt2 +tracecmp3.yslog +axicheck.smt2 +axicheck.yslog +axicheck2.smt2 +axicheck2.yslog +notrap_validop.smt2 +notrap_validop.yslog +mulcmp.smt2 +mulcmp.yslog +output.vcd +output.smtc diff --git a/scripts/smtbmc/axicheck.sh b/scripts/smtbmc/axicheck.sh new file mode 100644 index 0000000..732b3b8 --- /dev/null +++ b/scripts/smtbmc/axicheck.sh @@ -0,0 +1,13 @@ +#!/bin/bash + +set -ex + +yosys -ql axicheck.yslog \ + -p 'read_verilog -formal -norestrict -assume-asserts ../../picorv32.v' \ + -p 'read_verilog -formal axicheck.v' \ + -p 'prep -top testbench -nordff' \ + -p 'write_smt2 -wires axicheck.smt2' + +yosys-smtbmc -t 50 -s boolector --dump-vcd output.vcd --dump-smtc output.smtc axicheck.smt2 +# yosys-smtbmc -t 50 -i -s boolector --dump-vcd output.vcd --dump-smtc output.smtc axicheck.smt2 + diff --git a/scripts/smtbmc/axicheck.v b/scripts/smtbmc/axicheck.v new file mode 100644 index 0000000..80eda48 --- /dev/null +++ b/scripts/smtbmc/axicheck.v @@ -0,0 +1,210 @@ +module testbench ( + input clk, + output trap, + + output mem_axi_awvalid, + input mem_axi_awready, + output [31:0] mem_axi_awaddr, + output [ 2:0] mem_axi_awprot, + + output mem_axi_wvalid, + input mem_axi_wready, + output [31:0] mem_axi_wdata, + output [ 3:0] mem_axi_wstrb, + + input mem_axi_bvalid, + output mem_axi_bready, + + output mem_axi_arvalid, + input mem_axi_arready, + output [31:0] mem_axi_araddr, + output [ 2:0] mem_axi_arprot, + + input mem_axi_rvalid, + output mem_axi_rready, + input [31:0] mem_axi_rdata +); + reg resetn = 0; + + always @(posedge clk) + resetn <= 1; + + picorv32_axi #( + .ENABLE_COUNTERS(1), + .ENABLE_COUNTERS64(1), + .ENABLE_REGS_16_31(1), + .ENABLE_REGS_DUALPORT(1), + .BARREL_SHIFTER(1), + .TWO_CYCLE_COMPARE(0), + .TWO_CYCLE_ALU(0), + .COMPRESSED_ISA(0), + .CATCH_MISALIGN(1), + .CATCH_ILLINSN(1) + ) uut ( + .clk (clk ), + .resetn (resetn ), + .trap (trap ), + .mem_axi_awvalid (mem_axi_awvalid), + .mem_axi_awready (mem_axi_awready), + .mem_axi_awaddr (mem_axi_awaddr ), + .mem_axi_awprot (mem_axi_awprot ), + .mem_axi_wvalid (mem_axi_wvalid ), + .mem_axi_wready (mem_axi_wready ), + .mem_axi_wdata (mem_axi_wdata ), + .mem_axi_wstrb (mem_axi_wstrb ), + .mem_axi_bvalid (mem_axi_bvalid ), + .mem_axi_bready (mem_axi_bready ), + .mem_axi_arvalid (mem_axi_arvalid), + .mem_axi_arready (mem_axi_arready), + .mem_axi_araddr (mem_axi_araddr ), + .mem_axi_arprot (mem_axi_arprot ), + .mem_axi_rvalid (mem_axi_rvalid ), + .mem_axi_rready (mem_axi_rready ), + .mem_axi_rdata (mem_axi_rdata ) + ); + + reg expect_bvalid_aw = 0; + reg expect_bvalid_w = 0; + reg expect_rvalid = 0; + + reg [3:0] timeout_aw = 0; + reg [3:0] timeout_w = 0; + reg [3:0] timeout_b = 0; + reg [3:0] timeout_ar = 0; + reg [3:0] timeout_r = 0; + reg [3:0] timeout_ex = 0; + + always @(posedge clk) begin + timeout_aw <= !mem_axi_awvalid || mem_axi_awready ? 0 : timeout_aw + 1; + timeout_w <= !mem_axi_wvalid || mem_axi_wready ? 0 : timeout_w + 1; + timeout_b <= !mem_axi_bvalid || mem_axi_bready ? 0 : timeout_b + 1; + timeout_ar <= !mem_axi_arvalid || mem_axi_arready ? 0 : timeout_ar + 1; + timeout_r <= !mem_axi_rvalid || mem_axi_rready ? 0 : timeout_r + 1; + timeout_ex <= !{expect_bvalid_aw, expect_bvalid_w, expect_rvalid} ? 0 : timeout_ex + 1; + restrict(timeout_aw != 15); + restrict(timeout_w != 15); + restrict(timeout_b != 15); + restrict(timeout_ar != 15); + restrict(timeout_r != 15); + restrict(timeout_ex != 15); + restrict(!trap); + + end + + always @(posedge clk) begin + if (resetn) begin + if (!$past(resetn)) begin + assert(!mem_axi_awvalid); + assert(!mem_axi_wvalid ); + assume(!mem_axi_bvalid ); + assert(!mem_axi_arvalid); + assume(!mem_axi_rvalid ); + end else begin + // Only one read/write transaction in flight at each point in time + + if (expect_bvalid_aw) begin + assert(!mem_axi_awvalid); + end + + if (expect_bvalid_w) begin + assert(!mem_axi_wvalid); + end + + if (expect_rvalid) begin + assert(!mem_axi_arvalid); + end + + expect_bvalid_aw = expect_bvalid_aw || (mem_axi_awvalid && mem_axi_awready); + expect_bvalid_w = expect_bvalid_w || (mem_axi_wvalid && mem_axi_wready ); + expect_rvalid = expect_rvalid || (mem_axi_arvalid && mem_axi_arready); + + if (expect_bvalid_aw || expect_bvalid_w) begin + assert(!expect_rvalid); + end + + if (expect_rvalid) begin + assert(!expect_bvalid_aw); + assert(!expect_bvalid_w); + end + + if (!expect_bvalid_aw || !expect_bvalid_w) begin + assume(!mem_axi_bvalid); + end + + if (!expect_rvalid) begin + assume(!mem_axi_rvalid); + end + + if (mem_axi_bvalid && mem_axi_bready) begin + expect_bvalid_aw = 0; + expect_bvalid_w = 0; + end + + if (mem_axi_rvalid && mem_axi_rready) begin + expect_rvalid = 0; + end + + // Check AXI Master Streams + + if ($past(mem_axi_awvalid && !mem_axi_awready)) begin + assert(mem_axi_awvalid); + assert($stable(mem_axi_awaddr)); + assert($stable(mem_axi_awprot)); + end + if ($fell(mem_axi_awvalid)) begin + assert($past(mem_axi_awready)); + end + if ($fell(mem_axi_awready)) begin + assume($past(mem_axi_awvalid)); + end + + if ($past(mem_axi_arvalid && !mem_axi_arready)) begin + assert(mem_axi_arvalid); + assert($stable(mem_axi_araddr)); + assert($stable(mem_axi_arprot)); + end + if ($fell(mem_axi_arvalid)) begin + assert($past(mem_axi_arready)); + end + if ($fell(mem_axi_arready)) begin + assume($past(mem_axi_arvalid)); + end + + if ($past(mem_axi_wvalid && !mem_axi_wready)) begin + assert(mem_axi_wvalid); + assert($stable(mem_axi_wdata)); + assert($stable(mem_axi_wstrb)); + end + if ($fell(mem_axi_wvalid)) begin + assert($past(mem_axi_wready)); + end + if ($fell(mem_axi_wready)) begin + assume($past(mem_axi_wvalid)); + end + + // Check AXI Slave Streams + + if ($past(mem_axi_bvalid && !mem_axi_bready)) begin + assume(mem_axi_bvalid); + end + if ($fell(mem_axi_bvalid)) begin + assume($past(mem_axi_bready)); + end + if ($fell(mem_axi_bready)) begin + assert($past(mem_axi_bvalid)); + end + + if ($past(mem_axi_rvalid && !mem_axi_rready)) begin + assume(mem_axi_rvalid); + assume($stable(mem_axi_rdata)); + end + if ($fell(mem_axi_rvalid)) begin + assume($past(mem_axi_rready)); + end + if ($fell(mem_axi_rready)) begin + assert($past(mem_axi_rvalid)); + end + end + end + end +endmodule diff --git a/scripts/smtbmc/axicheck2.sh b/scripts/smtbmc/axicheck2.sh new file mode 100644 index 0000000..df20855 --- /dev/null +++ b/scripts/smtbmc/axicheck2.sh @@ -0,0 +1,12 @@ +#!/bin/bash + +set -ex + +yosys -ql axicheck2.yslog \ + -p 'read_verilog -formal -norestrict -assume-asserts ../../picorv32.v' \ + -p 'read_verilog -formal axicheck2.v' \ + -p 'prep -top testbench -nordff' \ + -p 'write_smt2 -wires axicheck2.smt2' + +yosys-smtbmc -t 6 -s yices --dump-vcd output.vcd --dump-smtc output.smtc --smtc axicheck2.smtc axicheck2.smt2 + diff --git a/scripts/smtbmc/axicheck2.smtc b/scripts/smtbmc/axicheck2.smtc new file mode 100644 index 0000000..1f8c5ea --- /dev/null +++ b/scripts/smtbmc/axicheck2.smtc @@ -0,0 +1,2 @@ +initial +assume (= [uut_0] [uut_1]) diff --git a/scripts/smtbmc/axicheck2.v b/scripts/smtbmc/axicheck2.v new file mode 100644 index 0000000..3d24a2e --- /dev/null +++ b/scripts/smtbmc/axicheck2.v @@ -0,0 +1,147 @@ +module testbench ( + input clk, + input resetn, + output trap_0, + output trap_1, + + output mem_axi_awvalid_0, + input mem_axi_awready_0, + output [31:0] mem_axi_awaddr_0, + output [ 2:0] mem_axi_awprot_0, + + output mem_axi_awvalid_1, + input mem_axi_awready_1, + output [31:0] mem_axi_awaddr_1, + output [ 2:0] mem_axi_awprot_1, + + output mem_axi_wvalid_0, + input mem_axi_wready_0, + output [31:0] mem_axi_wdata_0, + output [ 3:0] mem_axi_wstrb_0, + + output mem_axi_wvalid_1, + input mem_axi_wready_1, + output [31:0] mem_axi_wdata_1, + output [ 3:0] mem_axi_wstrb_1, + + input mem_axi_bvalid, + output mem_axi_bready_0, + output mem_axi_bready_1, + + output mem_axi_arvalid_0, + input mem_axi_arready_0, + output [31:0] mem_axi_araddr_0, + output [ 2:0] mem_axi_arprot_0, + + output mem_axi_arvalid_1, + input mem_axi_arready_1, + output [31:0] mem_axi_araddr_1, + output [ 2:0] mem_axi_arprot_1, + + input mem_axi_rvalid, + output mem_axi_rready_0, + output mem_axi_rready_1, + input [31:0] mem_axi_rdata +); + picorv32_axi #( + .ENABLE_COUNTERS(1), + .ENABLE_COUNTERS64(1), + .ENABLE_REGS_16_31(1), + .ENABLE_REGS_DUALPORT(1), + .BARREL_SHIFTER(1), + .TWO_CYCLE_COMPARE(0), + .TWO_CYCLE_ALU(0), + .COMPRESSED_ISA(0), + .CATCH_MISALIGN(1), + .CATCH_ILLINSN(1) + ) uut_0 ( + .clk (clk ), + .resetn (resetn ), + .trap (trap_0 ), + .mem_axi_awvalid (mem_axi_awvalid_0), + .mem_axi_awready (mem_axi_awready_0), + .mem_axi_awaddr (mem_axi_awaddr_0 ), + .mem_axi_awprot (mem_axi_awprot_0 ), + .mem_axi_wvalid (mem_axi_wvalid_0 ), + .mem_axi_wready (mem_axi_wready_0 ), + .mem_axi_wdata (mem_axi_wdata_0 ), + .mem_axi_wstrb (mem_axi_wstrb_0 ), + .mem_axi_bvalid (mem_axi_bvalid ), + .mem_axi_bready (mem_axi_bready_0 ), + .mem_axi_arvalid (mem_axi_arvalid_0), + .mem_axi_arready (mem_axi_arready_0), + .mem_axi_araddr (mem_axi_araddr_0 ), + .mem_axi_arprot (mem_axi_arprot_0 ), + .mem_axi_rvalid (mem_axi_rvalid ), + .mem_axi_rready (mem_axi_rready_0 ), + .mem_axi_rdata (mem_axi_rdata ) + ); + + picorv32_axi #( + .ENABLE_COUNTERS(1), + .ENABLE_COUNTERS64(1), + .ENABLE_REGS_16_31(1), + .ENABLE_REGS_DUALPORT(1), + .BARREL_SHIFTER(1), + .TWO_CYCLE_COMPARE(0), + .TWO_CYCLE_ALU(0), + .COMPRESSED_ISA(0), + .CATCH_MISALIGN(1), + .CATCH_ILLINSN(1) + ) uut_1 ( + .clk (clk ), + .resetn (resetn ), + .trap (trap_1 ), + .mem_axi_awvalid (mem_axi_awvalid_1), + .mem_axi_awready (mem_axi_awready_1), + .mem_axi_awaddr (mem_axi_awaddr_1 ), + .mem_axi_awprot (mem_axi_awprot_1 ), + .mem_axi_wvalid (mem_axi_wvalid_1 ), + .mem_axi_wready (mem_axi_wready_1 ), + .mem_axi_wdata (mem_axi_wdata_1 ), + .mem_axi_wstrb (mem_axi_wstrb_1 ), + .mem_axi_bvalid (mem_axi_bvalid ), + .mem_axi_bready (mem_axi_bready_1 ), + .mem_axi_arvalid (mem_axi_arvalid_1), + .mem_axi_arready (mem_axi_arready_1), + .mem_axi_araddr (mem_axi_araddr_1 ), + .mem_axi_arprot (mem_axi_arprot_1 ), + .mem_axi_rvalid (mem_axi_rvalid ), + .mem_axi_rready (mem_axi_rready_1 ), + .mem_axi_rdata (mem_axi_rdata ) + ); + + always @(posedge clk) begin + if (resetn && $past(resetn)) begin + assert(trap_0 == trap_1 ); + assert(mem_axi_awvalid_0 == mem_axi_awvalid_1); + assert(mem_axi_awaddr_0 == mem_axi_awaddr_1 ); + assert(mem_axi_awprot_0 == mem_axi_awprot_1 ); + assert(mem_axi_wvalid_0 == mem_axi_wvalid_1 ); + assert(mem_axi_wdata_0 == mem_axi_wdata_1 ); + assert(mem_axi_wstrb_0 == mem_axi_wstrb_1 ); + assert(mem_axi_bready_0 == mem_axi_bready_1 ); + assert(mem_axi_arvalid_0 == mem_axi_arvalid_1); + assert(mem_axi_araddr_0 == mem_axi_araddr_1 ); + assert(mem_axi_arprot_0 == mem_axi_arprot_1 ); + assert(mem_axi_rready_0 == mem_axi_rready_1 ); + + if (mem_axi_awvalid_0) assume(mem_axi_awready_0 == mem_axi_awready_1); + if (mem_axi_wvalid_0 ) assume(mem_axi_wready_0 == mem_axi_wready_1 ); + if (mem_axi_arvalid_0) assume(mem_axi_arready_0 == mem_axi_arready_1); + + if ($fell(mem_axi_awready_0)) assume($past(mem_axi_awvalid_0)); + if ($fell(mem_axi_wready_0 )) assume($past(mem_axi_wvalid_0 )); + if ($fell(mem_axi_arready_0)) assume($past(mem_axi_arvalid_0)); + + if ($fell(mem_axi_awready_1)) assume($past(mem_axi_awvalid_1)); + if ($fell(mem_axi_wready_1 )) assume($past(mem_axi_wvalid_1 )); + if ($fell(mem_axi_arready_1)) assume($past(mem_axi_arvalid_1)); + + if ($fell(mem_axi_bvalid)) assume($past(mem_axi_bready_0)); + if ($fell(mem_axi_rvalid)) assume($past(mem_axi_rready_0)); + + if (mem_axi_rvalid && $past(mem_axi_rvalid)) assume($stable(mem_axi_rdata)); + end + end +endmodule diff --git a/scripts/smtbmc/mulcmp.sh b/scripts/smtbmc/mulcmp.sh new file mode 100644 index 0000000..586d72a --- /dev/null +++ b/scripts/smtbmc/mulcmp.sh @@ -0,0 +1,12 @@ +#!/bin/bash + +set -ex + +yosys -ql mulcmp.yslog \ + -p 'read_verilog -formal -norestrict -assume-asserts ../../picorv32.v' \ + -p 'read_verilog -formal mulcmp.v' \ + -p 'prep -top testbench -nordff' \ + -p 'write_smt2 -wires mulcmp.smt2' + +yosys-smtbmc -s yices -t 100 --dump-vcd output.vcd --dump-smtc output.smtc mulcmp.smt2 + diff --git a/scripts/smtbmc/mulcmp.v b/scripts/smtbmc/mulcmp.v new file mode 100644 index 0000000..20c47f3 --- /dev/null +++ b/scripts/smtbmc/mulcmp.v @@ -0,0 +1,87 @@ +module testbench(input clk, mem_ready_0, mem_ready_1); + + reg resetn = 0; + + always @(posedge clk) + resetn <= 1; + + reg pcpi_valid_0 = 1; + reg pcpi_valid_1 = 1; + + wire [31:0] pcpi_insn = $anyconst; + wire [31:0] pcpi_rs1 = $anyconst; + wire [31:0] pcpi_rs2 = $anyconst; + + wire pcpi_wr_0; + wire [31:0] pcpi_rd_0; + wire pcpi_wait_0; + wire pcpi_ready_0; + + wire pcpi_wr_1; + wire [31:0] pcpi_rd_1; + wire pcpi_wait_1; + wire pcpi_ready_1; + + reg pcpi_wr_ref; + reg [31:0] pcpi_rd_ref; + reg pcpi_ready_ref = 0; + + picorv32_pcpi_mul mul_0 ( + .clk (clk ), + .resetn (resetn ), + .pcpi_valid(pcpi_valid_0), + .pcpi_insn (pcpi_insn ), + .pcpi_rs1 (pcpi_rs1 ), + .pcpi_rs2 (pcpi_rs2 ), + .pcpi_wr (pcpi_wr_0 ), + .pcpi_rd (pcpi_rd_0 ), + .pcpi_wait (pcpi_wait_0 ), + .pcpi_ready(pcpi_ready_0), + + ); + + picorv32_pcpi_fast_mul mul_1 ( + .clk (clk ), + .resetn (resetn ), + .pcpi_valid(pcpi_valid_1), + .pcpi_insn (pcpi_insn ), + .pcpi_rs1 (pcpi_rs1 ), + .pcpi_rs2 (pcpi_rs2 ), + .pcpi_wr (pcpi_wr_1 ), + .pcpi_rd (pcpi_rd_1 ), + .pcpi_wait (pcpi_wait_1 ), + .pcpi_ready(pcpi_ready_1), + + ); + + always @(posedge clk) begin + if (resetn) begin + if (pcpi_ready_0 && pcpi_ready_1) begin + assert(pcpi_wr_0 == pcpi_wr_1); + assert(pcpi_rd_0 == pcpi_rd_1); + end + + if (pcpi_ready_0) begin + pcpi_valid_0 <= 0; + pcpi_wr_ref <= pcpi_wr_0; + pcpi_rd_ref <= pcpi_rd_0; + pcpi_ready_ref <= 1; + if (pcpi_ready_ref) begin + assert(pcpi_wr_0 == pcpi_wr_ref); + assert(pcpi_rd_0 == pcpi_rd_ref); + end + end + + if (pcpi_ready_1) begin + pcpi_valid_1 <= 0; + pcpi_wr_ref <= pcpi_wr_1; + pcpi_rd_ref <= pcpi_rd_1; + pcpi_ready_ref <= 1; + if (pcpi_ready_ref) begin + assert(pcpi_wr_1 == pcpi_wr_ref); + assert(pcpi_rd_1 == pcpi_rd_ref); + end + end + end + end +endmodule diff --git a/scripts/smtbmc/notrap_validop.sh b/scripts/smtbmc/notrap_validop.sh new file mode 100644 index 0000000..95e0f92 --- /dev/null +++ b/scripts/smtbmc/notrap_validop.sh @@ -0,0 +1,13 @@ +#!/bin/bash + +set -ex + +yosys -ql notrap_validop.yslog \ + -p 'read_verilog -formal -norestrict -assume-asserts ../../picorv32.v' \ + -p 'read_verilog -formal notrap_validop.v' \ + -p 'prep -top testbench -nordff' \ + -p 'write_smt2 -wires notrap_validop.smt2' + +yosys-smtbmc -s yices -t 30 --dump-vcd output.vcd --dump-smtc output.smtc notrap_validop.smt2 +yosys-smtbmc -s yices -i -t 30 --dump-vcd output.vcd --dump-smtc output.smtc notrap_validop.smt2 + diff --git a/scripts/smtbmc/notrap_validop.v b/scripts/smtbmc/notrap_validop.v new file mode 100644 index 0000000..8e50304 --- /dev/null +++ b/scripts/smtbmc/notrap_validop.v @@ -0,0 +1,67 @@ +module testbench(input clk, mem_ready); + `include "opcode.v" + + reg resetn = 0; + always @(posedge clk) resetn <= 1; + + (* keep *) wire trap, mem_valid, mem_instr; + (* keep *) wire [3:0] mem_wstrb; + (* keep *) wire [31:0] mem_addr, mem_wdata, mem_rdata; + (* keep *) wire [35:0] trace_data; + + reg [31:0] mem [0:2**30-1]; + + assign mem_rdata = mem[mem_addr >> 2]; + + always @(posedge clk) begin + if (resetn && mem_valid && mem_ready) begin + if (mem_wstrb[3]) mem[mem_addr >> 2][31:24] <= mem_wdata[31:24]; + if (mem_wstrb[2]) mem[mem_addr >> 2][23:16] <= mem_wdata[23:16]; + if (mem_wstrb[1]) mem[mem_addr >> 2][15: 8] <= mem_wdata[15: 8]; + if (mem_wstrb[0]) mem[mem_addr >> 2][ 7: 0] <= mem_wdata[ 7: 0]; + end + end + + reg [1:0] mem_ready_stall = 0; + + always @(posedge clk) begin + mem_ready_stall <= {mem_ready_stall, mem_valid && !mem_ready}; + restrict(&mem_ready_stall == 0); + + if (mem_instr && mem_ready && mem_valid) begin + assume(opcode_valid(mem_rdata)); + assume(!opcode_branch(mem_rdata)); + assume(!opcode_load(mem_rdata)); + assume(!opcode_store(mem_rdata)); + end + + if (!mem_valid) + assume(!mem_ready); + + if (resetn) + assert(!trap); + end + + picorv32 #( + // change this settings as you like + .ENABLE_REGS_DUALPORT(1), + .TWO_STAGE_SHIFT(1), + .BARREL_SHIFTER(0), + .TWO_CYCLE_COMPARE(0), + .TWO_CYCLE_ALU(0), + .COMPRESSED_ISA(0), + .ENABLE_MUL(0), + .ENABLE_DIV(0) + ) cpu ( + .clk (clk ), + .resetn (resetn ), + .trap (trap ), + .mem_valid (mem_valid ), + .mem_instr (mem_instr ), + .mem_ready (mem_ready ), + .mem_addr (mem_addr ), + .mem_wdata (mem_wdata ), + .mem_wstrb (mem_wstrb ), + .mem_rdata (mem_rdata ) + ); +endmodule diff --git a/scripts/smtbmc/opcode.v b/scripts/smtbmc/opcode.v new file mode 100644 index 0000000..7a13bd2 --- /dev/null +++ b/scripts/smtbmc/opcode.v @@ -0,0 +1,104 @@ +function opcode_jump; + input [31:0] opcode; + begin + opcode_jump = 0; + if (opcode[6:0] == 7'b1101111) opcode_jump = 1; // JAL + if (opcode[14:12] == 3'b000 && opcode[6:0] == 7'b1100111) opcode_jump = 1; // JALR + end +endfunction + +function opcode_branch; + input [31:0] opcode; + begin + opcode_branch = 0; + if (opcode[14:12] == 3'b000 && opcode[6:0] == 7'b1100011) opcode_branch = 1; // BEQ + if (opcode[14:12] == 3'b001 && opcode[6:0] == 7'b1100011) opcode_branch = 1; // BNE + if (opcode[14:12] == 3'b100 && opcode[6:0] == 7'b1100011) opcode_branch = 1; // BLT + if (opcode[14:12] == 3'b101 && opcode[6:0] == 7'b1100011) opcode_branch = 1; // BGE + if (opcode[14:12] == 3'b110 && opcode[6:0] == 7'b1100011) opcode_branch = 1; // BLTU + if (opcode[14:12] == 3'b111 && opcode[6:0] == 7'b1100011) opcode_branch = 1; // BGEU + end +endfunction + +function opcode_load; + input [31:0] opcode; + begin + opcode_load = 0; + if (opcode[14:12] == 3'b000 && opcode[6:0] == 7'b0000011) opcode_load = 1; // LB + if (opcode[14:12] == 3'b001 && opcode[6:0] == 7'b0000011) opcode_load = 1; // LH + if (opcode[14:12] == 3'b010 && opcode[6:0] == 7'b0000011) opcode_load = 1; // LW + if (opcode[14:12] == 3'b100 && opcode[6:0] == 7'b0000011) opcode_load = 1; // LBU + if (opcode[14:12] == 3'b101 && opcode[6:0] == 7'b0000011) opcode_load = 1; // LHU + end +endfunction + +function opcode_store; + input [31:0] opcode; + begin + opcode_store = 0; + if (opcode[14:12] == 3'b000 && opcode[6:0] == 7'b0100011) opcode_store = 1; // SB + if (opcode[14:12] == 3'b001 && opcode[6:0] == 7'b0100011) opcode_store = 1; // SH + if (opcode[14:12] == 3'b010 && opcode[6:0] == 7'b0100011) opcode_store = 1; // SW + end +endfunction + +function opcode_alui; + input [31:0] opcode; + begin + opcode_alui = 0; + if (opcode[14:12] == 3'b000 && opcode[6:0] == 7'b0010011) opcode_alui = 1; // ADDI + if (opcode[14:12] == 3'b010 && opcode[6:0] == 7'b0010011) opcode_alui = 1; // SLTI + if (opcode[14:12] == 3'b011 && opcode[6:0] == 7'b0010011) opcode_alui = 1; // SLTIU + if (opcode[14:12] == 3'b100 && opcode[6:0] == 7'b0010011) opcode_alui = 1; // XORI + if (opcode[14:12] == 3'b110 && opcode[6:0] == 7'b0010011) opcode_alui = 1; // ORI + if (opcode[14:12] == 3'b111 && opcode[6:0] == 7'b0010011) opcode_alui = 1; // ANDI + if (opcode[31:25] == 7'b0000000 && opcode[14:12] == 3'b001 && opcode[6:0] == 7'b0010011) opcode_alui = 1; // SLLI + if (opcode[31:25] == 7'b0000000 && opcode[14:12] == 3'b101 && opcode[6:0] == 7'b0010011) opcode_alui = 1; // SRLI + if (opcode[31:25] == 7'b0100000 && opcode[14:12] == 3'b101 && opcode[6:0] == 7'b0010011) opcode_alui = 1; // SRAI + end +endfunction + +function opcode_alu; + input [31:0] opcode; + begin + opcode_alu = 0; + if (opcode[31:25] == 7'b0000000 && opcode[14:12] == 3'b000 && opcode[6:0] == 7'b0110011) opcode_alu = 1; // ADD + if (opcode[31:25] == 7'b0100000 && opcode[14:12] == 3'b000 && opcode[6:0] == 7'b0110011) opcode_alu = 1; // SUB + if (opcode[31:25] == 7'b0000000 && opcode[14:12] == 3'b001 && opcode[6:0] == 7'b0110011) opcode_alu = 1; // SLL + if (opcode[31:25] == 7'b0000000 && opcode[14:12] == 3'b010 && opcode[6:0] == 7'b0110011) opcode_alu = 1; // SLT + if (opcode[31:25] == 7'b0000000 && opcode[14:12] == 3'b011 && opcode[6:0] == 7'b0110011) opcode_alu = 1; // SLTU + if (opcode[31:25] == 7'b0000000 && opcode[14:12] == 3'b100 && opcode[6:0] == 7'b0110011) opcode_alu = 1; // XOR + if (opcode[31:25] == 7'b0000000 && opcode[14:12] == 3'b101 && opcode[6:0] == 7'b0110011) opcode_alu = 1; // SRL + if (opcode[31:25] == 7'b0100000 && opcode[14:12] == 3'b101 && opcode[6:0] == 7'b0110011) opcode_alu = 1; // SRA + if (opcode[31:25] == 7'b0000000 && opcode[14:12] == 3'b110 && opcode[6:0] == 7'b0110011) opcode_alu = 1; // OR + if (opcode[31:25] == 7'b0000000 && opcode[14:12] == 3'b111 && opcode[6:0] == 7'b0110011) opcode_alu = 1; // AND + end +endfunction + +function opcode_sys; + input [31:0] opcode; + begin + opcode_sys = 0; + if (opcode[31:20] == 12'hC00 && opcode[19:12] == 3'b010 && opcode[6:0] == 7'b1110011) opcode_sys = 1; // RDCYCLE + if (opcode[31:20] == 12'hC01 && opcode[19:12] == 3'b010 && opcode[6:0] == 7'b1110011) opcode_sys = 1; // RDTIME + if (opcode[31:20] == 12'hC02 && opcode[19:12] == 3'b010 && opcode[6:0] == 7'b1110011) opcode_sys = 1; // RDINSTRET + if (opcode[31:20] == 12'hC80 && opcode[19:12] == 3'b010 && opcode[6:0] == 7'b1110011) opcode_sys = 1; // RDCYCLEH + if (opcode[31:20] == 12'hC81 && opcode[19:12] == 3'b010 && opcode[6:0] == 7'b1110011) opcode_sys = 1; // RDTIMEH + if (opcode[31:20] == 12'hC82 && opcode[19:12] == 3'b010 && opcode[6:0] == 7'b1110011) opcode_sys = 1; // RDINSTRETH + end + +endfunction + +function opcode_valid; + input [31:0] opcode; + begin + opcode_valid = 0; + if (opcode_jump (opcode)) opcode_valid = 1; + if (opcode_branch(opcode)) opcode_valid = 1; + if (opcode_load (opcode)) opcode_valid = 1; + if (opcode_store (opcode)) opcode_valid = 1; + if (opcode_alui (opcode)) opcode_valid = 1; + if (opcode_alu (opcode)) opcode_valid = 1; + if (opcode_sys (opcode)) opcode_valid = 1; + end +endfunction diff --git a/scripts/smtbmc/tracecmp.gtkw b/scripts/smtbmc/tracecmp.gtkw new file mode 100644 index 0000000..09dd9b2 --- /dev/null +++ b/scripts/smtbmc/tracecmp.gtkw @@ -0,0 +1,71 @@ +[*] +[*] GTKWave Analyzer v3.3.65 (w)1999-2015 BSI +[*] Fri Aug 26 15:42:37 2016 +[*] +[dumpfile] "/home/clifford/Work/picorv32/scripts/smtbmc/output.vcd" +[dumpfile_mtime] "Fri Aug 26 15:33:18 2016" +[dumpfile_size] 80106 +[savefile] "/home/clifford/Work/picorv32/scripts/smtbmc/tracecmp.gtkw" +[timestart] 0 +[size] 1216 863 +[pos] -1 -1 +*-2.860312 10 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 +[treeopen] testbench. +[sst_width] 241 +[signals_width] 337 +[sst_expanded] 1 +[sst_vpaned_height] 252 +@28 +smt_clock +testbench.resetn +testbench.trap_0 +testbench.trap_1 +@200 +- +-Trace CMP +@28 +testbench.trace_valid_0 +testbench.trace_valid_1 +@22 +testbench.trace_data_0[35:0] +testbench.trace_data_1[35:0] +@420 +testbench.trace_balance[7:0] +@200 +- +-CPU #0 +@28 +testbench.mem_valid_0 +testbench.mem_ready_0 +testbench.mem_instr_0 +@22 +testbench.mem_addr_0[31:0] +testbench.mem_rdata_0[31:0] +testbench.mem_wdata_0[31:0] +@28 +testbench.mem_wstrb_0[3:0] +@22 +testbench.cpu_0.cpu_state[7:0] +@28 +testbench.cpu_0.mem_state[1:0] +@200 +- +-CPU #1 +@28 +testbench.mem_valid_1 +testbench.mem_ready_1 +testbench.mem_instr_1 +@22 +testbench.mem_addr_1[31:0] +testbench.mem_rdata_1[31:0] +testbench.mem_wdata_1[31:0] +@28 +testbench.mem_wstrb_1[3:0] +@22 +testbench.cpu_1.cpu_state[7:0] +@28 +testbench.cpu_1.mem_state[1:0] +@200 +- +[pattern_trace] 1 +[pattern_trace] 0 diff --git a/scripts/smtbmc/tracecmp.sh b/scripts/smtbmc/tracecmp.sh new file mode 100644 index 0000000..449af52 --- /dev/null +++ b/scripts/smtbmc/tracecmp.sh @@ -0,0 +1,12 @@ +#!/bin/bash + +set -ex + +yosys -ql tracecmp.yslog \ + -p 'read_verilog -formal -norestrict -assume-asserts ../../picorv32.v' \ + -p 'read_verilog -formal tracecmp.v' \ + -p 'prep -top testbench -nordff' \ + -p 'write_smt2 -wires tracecmp.smt2' + +yosys-smtbmc -s yices --smtc tracecmp.smtc --dump-vcd output.vcd --dump-smtc output.smtc tracecmp.smt2 + diff --git a/scripts/smtbmc/tracecmp.smtc b/scripts/smtbmc/tracecmp.smtc new file mode 100644 index 0000000..477c7d0 --- /dev/null +++ b/scripts/smtbmc/tracecmp.smtc @@ -0,0 +1,12 @@ +initial +assume (= [mem_0] [mem_1]) +assume (= [cpu_0.cpuregs] [cpu_1.cpuregs]) +assume (= [trace_data_0] [trace_data_1]) + +always +assume (=> (not [mem_valid_0]) (not [mem_ready_0])) +assume (=> (not [mem_valid_1]) (not [mem_ready_1])) +# assume (= [mem_ready_0] [mem_ready_1]) + +always -1 +assert (=> (= [trace_balance] #x00) (= [trace_data_0] [trace_data_1])) diff --git a/scripts/smtbmc/tracecmp.v b/scripts/smtbmc/tracecmp.v new file mode 100644 index 0000000..8ac4157 --- /dev/null +++ b/scripts/smtbmc/tracecmp.v @@ -0,0 +1,109 @@ +module testbench(input clk, mem_ready_0, mem_ready_1); + // set this to 1 to test generation of counter examples + localparam ENABLE_COUNTERS = 0; + + reg resetn = 0; + always @(posedge clk) resetn <= 1; + + (* keep *) wire trap_0, trace_valid_0, mem_valid_0, mem_instr_0; + (* keep *) wire [3:0] mem_wstrb_0; + (* keep *) wire [31:0] mem_addr_0, mem_wdata_0, mem_rdata_0; + (* keep *) wire [35:0] trace_data_0; + + (* keep *) wire trap_1, trace_valid_1, mem_valid_1, mem_instr_1; + (* keep *) wire [3:0] mem_wstrb_1; + (* keep *) wire [31:0] mem_addr_1, mem_wdata_1, mem_rdata_1; + (* keep *) wire [35:0] trace_data_1; + + reg [31:0] mem_0 [0:2**30-1]; + reg [31:0] mem_1 [0:2**30-1]; + + assign mem_rdata_0 = mem_0[mem_addr_0 >> 2]; + assign mem_rdata_1 = mem_1[mem_addr_1 >> 2]; + + always @(posedge clk) begin + if (resetn && mem_valid_0 && mem_ready_0) begin + if (mem_wstrb_0[3]) mem_0[mem_addr_0 >> 2][31:24] <= mem_wdata_0[31:24]; + if (mem_wstrb_0[2]) mem_0[mem_addr_0 >> 2][23:16] <= mem_wdata_0[23:16]; + if (mem_wstrb_0[1]) mem_0[mem_addr_0 >> 2][15: 8] <= mem_wdata_0[15: 8]; + if (mem_wstrb_0[0]) mem_0[mem_addr_0 >> 2][ 7: 0] <= mem_wdata_0[ 7: 0]; + end + if (resetn && mem_valid_1 && mem_ready_1) begin + if (mem_wstrb_1[3]) mem_1[mem_addr_1 >> 2][31:24] <= mem_wdata_1[31:24]; + if (mem_wstrb_1[2]) mem_1[mem_addr_1 >> 2][23:16] <= mem_wdata_1[23:16]; + if (mem_wstrb_1[1]) mem_1[mem_addr_1 >> 2][15: 8] <= mem_wdata_1[15: 8]; + if (mem_wstrb_1[0]) mem_1[mem_addr_1 >> 2][ 7: 0] <= mem_wdata_1[ 7: 0]; + end + end + + (* keep *) reg [7:0] trace_balance; + reg [7:0] trace_balance_q; + + always @* begin + trace_balance = trace_balance_q; + if (trace_valid_0) trace_balance = trace_balance + 1; + if (trace_valid_1) trace_balance = trace_balance - 1; + end + + always @(posedge clk) begin + trace_balance_q <= resetn ? trace_balance : 0; + end + + picorv32 #( + // do not change this settings + .ENABLE_COUNTERS(ENABLE_COUNTERS), + .ENABLE_TRACE(1), + + // change this settings as you like + .ENABLE_REGS_DUALPORT(1), + .TWO_STAGE_SHIFT(1), + .BARREL_SHIFTER(0), + .TWO_CYCLE_COMPARE(0), + .TWO_CYCLE_ALU(0), + .COMPRESSED_ISA(0), + .ENABLE_MUL(0), + .ENABLE_DIV(0) + ) cpu_0 ( + .clk (clk ), + .resetn (resetn ), + .trap (trap_0 ), + .mem_valid (mem_valid_0 ), + .mem_instr (mem_instr_0 ), + .mem_ready (mem_ready_0 ), + .mem_addr (mem_addr_0 ), + .mem_wdata (mem_wdata_0 ), + .mem_wstrb (mem_wstrb_0 ), + .mem_rdata (mem_rdata_0 ), + .trace_valid (trace_valid_0), + .trace_data (trace_data_0 ) + ); + + picorv32 #( + // do not change this settings + .ENABLE_COUNTERS(ENABLE_COUNTERS), + .ENABLE_TRACE(1), + + // change this settings as you like + .ENABLE_REGS_DUALPORT(1), + .TWO_STAGE_SHIFT(1), + .BARREL_SHIFTER(0), + .TWO_CYCLE_COMPARE(0), + .TWO_CYCLE_ALU(0), + .COMPRESSED_ISA(0), + .ENABLE_MUL(0), + .ENABLE_DIV(0) + ) cpu_1 ( + .clk (clk ), + .resetn (resetn ), + .trap (trap_1 ), + .mem_valid (mem_valid_1 ), + .mem_instr (mem_instr_1 ), + .mem_ready (mem_ready_1 ), + .mem_addr (mem_addr_1 ), + .mem_wdata (mem_wdata_1 ), + .mem_wstrb (mem_wstrb_1 ), + .mem_rdata (mem_rdata_1 ), + .trace_valid (trace_valid_1), + .trace_data (trace_data_1 ) + ); +endmodule diff --git a/scripts/smtbmc/tracecmp2.sh b/scripts/smtbmc/tracecmp2.sh new file mode 100644 index 0000000..ddaf285 --- /dev/null +++ b/scripts/smtbmc/tracecmp2.sh @@ -0,0 +1,12 @@ +#!/bin/bash + +set -ex + +yosys -ql tracecmp2.yslog \ + -p 'read_verilog -formal -norestrict -assume-asserts ../../picorv32.v' \ + -p 'read_verilog -formal tracecmp2.v' \ + -p 'prep -top testbench -nordff' \ + -p 'write_smt2 -wires tracecmp2.smt2' + +yosys-smtbmc -s boolector --smtc tracecmp2.smtc --dump-vcd output.vcd --dump-smtc output.smtc tracecmp2.smt2 + diff --git a/scripts/smtbmc/tracecmp2.smtc b/scripts/smtbmc/tracecmp2.smtc new file mode 100644 index 0000000..3b7fd0a --- /dev/null +++ b/scripts/smtbmc/tracecmp2.smtc @@ -0,0 +1,2 @@ +initial +assume (= [cpu_0.cpuregs] [cpu_1.cpuregs]) diff --git a/scripts/smtbmc/tracecmp2.v b/scripts/smtbmc/tracecmp2.v new file mode 100644 index 0000000..42f39a9 --- /dev/null +++ b/scripts/smtbmc/tracecmp2.v @@ -0,0 +1,196 @@ +module testbench( + input clk, mem_ready_0, mem_ready_1, + input [31:0] mem_rdata +); + // set this to 1 to test generation of counterexamples + localparam ENABLE_COUNTERS = 0; + + reg resetn = 0; + always @(posedge clk) resetn <= 1; + + (* keep *) wire trap_0, trace_valid_0, mem_valid_0, mem_instr_0; + (* keep *) wire [3:0] mem_wstrb_0; + (* keep *) wire [31:0] mem_addr_0, mem_wdata_0, mem_rdata_0; + (* keep *) wire [35:0] trace_data_0; + + (* keep *) wire trap_1, trace_valid_1, mem_valid_1, mem_instr_1; + (* keep *) wire [3:0] mem_wstrb_1; + (* keep *) wire [31:0] mem_addr_1, mem_wdata_1, mem_rdata_1; + (* keep *) wire [35:0] trace_data_1; + + reg [31:0] last_mem_rdata; + + assign mem_rdata_0 = mem_rdata; + assign mem_rdata_1 = mem_rdata; + + wire mem_xfer_0 = resetn && mem_valid_0 && mem_ready_0; + wire mem_xfer_1 = resetn && mem_valid_1 && mem_ready_1; + + reg [1:0] cmp_mem_state = 0; + reg [31:0] cmp_mem_addr; + reg [31:0] cmp_mem_wdata; + reg [3:0] cmp_mem_wstrb; + + always @* begin + if (mem_valid_0 == 0) + assume(!mem_ready_0 == 0); + if (mem_valid_1 == 0) + assume(mem_ready_1 == 0); + end + + always @(posedge clk) begin + if (cmp_mem_state) + assume(last_mem_rdata == mem_rdata); + last_mem_rdata <= mem_rdata; + end + + always @(posedge clk) begin + case (cmp_mem_state) + 2'b 00: begin + case ({mem_xfer_1, mem_xfer_0}) + 2'b 11: begin + assert(mem_addr_0 == mem_addr_1); + assert(mem_wstrb_0 == mem_wstrb_1); + if (mem_wstrb_0[3]) assert(mem_wdata_0[31:24] == mem_wdata_1[31:24]); + if (mem_wstrb_0[2]) assert(mem_wdata_0[23:16] == mem_wdata_1[23:16]); + if (mem_wstrb_0[1]) assert(mem_wdata_0[15: 8] == mem_wdata_1[15: 8]); + if (mem_wstrb_0[0]) assert(mem_wdata_0[ 7: 0] == mem_wdata_1[ 7: 0]); + end + 2'b 01: begin + cmp_mem_state <= 2'b 01; + cmp_mem_addr <= mem_addr_0; + cmp_mem_wdata <= mem_wdata_0; + cmp_mem_wstrb <= mem_wstrb_0; + end + 2'b 10: begin + cmp_mem_state <= 2'b 10; + cmp_mem_addr <= mem_addr_1; + cmp_mem_wdata <= mem_wdata_1; + cmp_mem_wstrb <= mem_wstrb_1; + end + endcase + end + 2'b 01: begin + assume(!mem_xfer_0); + if (mem_xfer_1) begin + cmp_mem_state <= 2'b 00; + assert(cmp_mem_addr == mem_addr_1); + assert(cmp_mem_wstrb == mem_wstrb_1); + if (cmp_mem_wstrb[3]) assert(cmp_mem_wdata[31:24] == mem_wdata_1[31:24]); + if (cmp_mem_wstrb[2]) assert(cmp_mem_wdata[23:16] == mem_wdata_1[23:16]); + if (cmp_mem_wstrb[1]) assert(cmp_mem_wdata[15: 8] == mem_wdata_1[15: 8]); + if (cmp_mem_wstrb[0]) assert(cmp_mem_wdata[ 7: 0] == mem_wdata_1[ 7: 0]); + end + end + 2'b 10: begin + assume(!mem_xfer_1); + if (mem_xfer_0) begin + cmp_mem_state <= 2'b 00; + assert(cmp_mem_addr == mem_addr_0); + assert(cmp_mem_wstrb == mem_wstrb_0); + if (cmp_mem_wstrb[3]) assert(cmp_mem_wdata[31:24] == mem_wdata_0[31:24]); + if (cmp_mem_wstrb[2]) assert(cmp_mem_wdata[23:16] == mem_wdata_0[23:16]); + if (cmp_mem_wstrb[1]) assert(cmp_mem_wdata[15: 8] == mem_wdata_0[15: 8]); + if (cmp_mem_wstrb[0]) assert(cmp_mem_wdata[ 7: 0] == mem_wdata_0[ 7: 0]); + end + end + endcase + end + + reg [1:0] cmp_trace_state = 0; + reg [35:0] cmp_trace_data; + + always @(posedge clk) begin + if (resetn) begin + case (cmp_trace_state) + 2'b 00: begin + case ({trace_valid_1, trace_valid_0}) + 2'b 11: begin + assert(trace_data_0 == trace_data_1); + end + 2'b 01: begin + cmp_trace_state <= 2'b 01; + cmp_trace_data <= trace_data_0; + end + 2'b 10: begin + cmp_trace_state <= 2'b 10; + cmp_trace_data <= trace_data_1; + end + endcase + end + 2'b 01: begin + assume(!trace_valid_0); + if (trace_valid_1) begin + cmp_trace_state <= 2'b 00; + assert(cmp_trace_data == trace_data_1); + end + end + 2'b 10: begin + assume(!trace_valid_1); + if (trace_valid_0) begin + cmp_trace_state <= 2'b 00; + assert(cmp_trace_data == trace_data_0); + end + end + endcase + end + end + + picorv32 #( + // do not change this settings + .ENABLE_COUNTERS(ENABLE_COUNTERS), + .ENABLE_TRACE(1), + + // change this settings as you like + .ENABLE_REGS_DUALPORT(1), + .TWO_STAGE_SHIFT(0), + .BARREL_SHIFTER(0), + .TWO_CYCLE_COMPARE(0), + .TWO_CYCLE_ALU(0), + .COMPRESSED_ISA(1), + .ENABLE_MUL(0), + .ENABLE_DIV(0) + ) cpu_0 ( + .clk (clk ), + .resetn (resetn ), + .trap (trap_0 ), + .mem_valid (mem_valid_0 ), + .mem_instr (mem_instr_0 ), + .mem_ready (mem_ready_0 ), + .mem_addr (mem_addr_0 ), + .mem_wdata (mem_wdata_0 ), + .mem_wstrb (mem_wstrb_0 ), + .mem_rdata (mem_rdata_0 ), + .trace_valid (trace_valid_0), + .trace_data (trace_data_0 ) + ); + + picorv32 #( + // do not change this settings + .ENABLE_COUNTERS(ENABLE_COUNTERS), + .ENABLE_TRACE(1), + + // change this settings as you like + .ENABLE_REGS_DUALPORT(1), + .TWO_STAGE_SHIFT(1), + .BARREL_SHIFTER(0), + .TWO_CYCLE_COMPARE(0), + .TWO_CYCLE_ALU(0), + .COMPRESSED_ISA(1), + .ENABLE_MUL(0), + .ENABLE_DIV(0) + ) cpu_1 ( + .clk (clk ), + .resetn (resetn ), + .trap (trap_1 ), + .mem_valid (mem_valid_1 ), + .mem_instr (mem_instr_1 ), + .mem_ready (mem_ready_1 ), + .mem_addr (mem_addr_1 ), + .mem_wdata (mem_wdata_1 ), + .mem_wstrb (mem_wstrb_1 ), + .mem_rdata (mem_rdata_1 ), + .trace_valid (trace_valid_1), + .trace_data (trace_data_1 ) + ); +endmodule diff --git a/scripts/smtbmc/tracecmp3.sh b/scripts/smtbmc/tracecmp3.sh new file mode 100644 index 0000000..bfa0b3c --- /dev/null +++ b/scripts/smtbmc/tracecmp3.sh @@ -0,0 +1,17 @@ +#!/bin/bash + +set -ex + +yosys -l tracecmp3.yslog \ + -p 'read_verilog ../../picorv32.v' \ + -p 'read_verilog -formal tracecmp3.v' \ + -p 'prep -top testbench -nordff' \ + -p 'write_smt2 -wires tracecmp3.smt2' \ + -p 'miter -assert -flatten testbench miter' \ + -p 'hierarchy -top miter; memory_map; opt -full' \ + -p 'techmap; opt; abc; opt -fast' \ + -p 'write_blif tracecmp3.blif' + +yosys-abc -c 'read_blif tracecmp3.blif; undc; strash; zero; sim3 -v; undc -c; write_cex -n tracecmp3.cex' +yosys-smtbmc -s yices --cex tracecmp3.cex --dump-vcd output.vcd --dump-smtc output.smtc tracecmp3.smt2 + diff --git a/scripts/smtbmc/tracecmp3.v b/scripts/smtbmc/tracecmp3.v new file mode 100644 index 0000000..a1bb63b --- /dev/null +++ b/scripts/smtbmc/tracecmp3.v @@ -0,0 +1,135 @@ +// Based on the benchmark from 2016 Yosys-SMTBMC presentation, which in turn is +// based on the tracecmp2 test from this directory. + +module testbench ( + input clk, + input [31:0] mem_rdata_in, + + input pcpi_wr, + input [31:0] pcpi_rd, + input pcpi_wait, + input pcpi_ready +); + reg resetn = 0; + + always @(posedge clk) + resetn <= 1; + + wire cpu0_trap; + wire cpu0_mem_valid; + wire cpu0_mem_instr; + wire cpu0_mem_ready; + wire [31:0] cpu0_mem_addr; + wire [31:0] cpu0_mem_wdata; + wire [3:0] cpu0_mem_wstrb; + wire [31:0] cpu0_mem_rdata; + wire cpu0_trace_valid; + wire [35:0] cpu0_trace_data; + + wire cpu1_trap; + wire cpu1_mem_valid; + wire cpu1_mem_instr; + wire cpu1_mem_ready; + wire [31:0] cpu1_mem_addr; + wire [31:0] cpu1_mem_wdata; + wire [3:0] cpu1_mem_wstrb; + wire [31:0] cpu1_mem_rdata; + wire cpu1_trace_valid; + wire [35:0] cpu1_trace_data; + + wire mem_ready; + wire [31:0] mem_rdata; + + assign mem_ready = cpu0_mem_valid && cpu1_mem_valid; + assign mem_rdata = mem_rdata_in; + + assign cpu0_mem_ready = mem_ready; + assign cpu0_mem_rdata = mem_rdata; + + assign cpu1_mem_ready = mem_ready; + assign cpu1_mem_rdata = mem_rdata; + + reg [ 2:0] trace_balance = 3'b010; + reg [35:0] trace_buffer_cpu0 = 0, trace_buffer_cpu1 = 0; + + always @(posedge clk) begin + if (resetn) begin + if (cpu0_trace_valid) + trace_buffer_cpu0 <= cpu0_trace_data; + + if (cpu1_trace_valid) + trace_buffer_cpu1 <= cpu1_trace_data; + + if (cpu0_trace_valid && !cpu1_trace_valid) + trace_balance <= trace_balance << 1; + + if (!cpu0_trace_valid && cpu1_trace_valid) + trace_balance <= trace_balance >> 1; + end + end + + always @* begin + if (resetn && cpu0_mem_ready) begin + assert(cpu0_mem_addr == cpu1_mem_addr); + assert(cpu0_mem_wstrb == cpu1_mem_wstrb); + if (cpu0_mem_wstrb[3]) assert(cpu0_mem_wdata[31:24] == cpu1_mem_wdata[31:24]); + if (cpu0_mem_wstrb[2]) assert(cpu0_mem_wdata[23:16] == cpu1_mem_wdata[23:16]); + if (cpu0_mem_wstrb[1]) assert(cpu0_mem_wdata[15: 8] == cpu1_mem_wdata[15: 8]); + if (cpu0_mem_wstrb[0]) assert(cpu0_mem_wdata[ 7: 0] == cpu1_mem_wdata[ 7: 0]); + end + if (trace_balance == 3'b010) begin + assert(trace_buffer_cpu0 == trace_buffer_cpu1); + end + end + + picorv32 #( + .ENABLE_COUNTERS(0), + .REGS_INIT_ZERO(1), + .COMPRESSED_ISA(1), + .ENABLE_TRACE(1), + + .TWO_STAGE_SHIFT(0), + .ENABLE_PCPI(1) + ) cpu0 ( + .clk (clk ), + .resetn (resetn ), + .trap (cpu0_trap ), + .mem_valid (cpu0_mem_valid ), + .mem_instr (cpu0_mem_instr ), + .mem_ready (cpu0_mem_ready ), + .mem_addr (cpu0_mem_addr ), + .mem_wdata (cpu0_mem_wdata ), + .mem_wstrb (cpu0_mem_wstrb ), + .mem_rdata (cpu0_mem_rdata ), + .pcpi_wr (pcpi_wr ), + .pcpi_rd (pcpi_rd ), + .pcpi_wait (pcpi_wait ), + .pcpi_ready (pcpi_ready ), + .trace_valid (cpu0_trace_valid), + .trace_data (cpu0_trace_data ) + ); + + picorv32 #( + .ENABLE_COUNTERS(0), + .REGS_INIT_ZERO(1), + .COMPRESSED_ISA(1), + .ENABLE_TRACE(1), + + .TWO_STAGE_SHIFT(1), + .TWO_CYCLE_COMPARE(1), + .TWO_CYCLE_ALU(1) + ) cpu1 ( + .clk (clk ), + .resetn (resetn ), + .trap (cpu1_trap ), + .mem_valid (cpu1_mem_valid ), + .mem_instr (cpu1_mem_instr ), + .mem_ready (cpu1_mem_ready ), + .mem_addr (cpu1_mem_addr ), + .mem_wdata (cpu1_mem_wdata ), + .mem_wstrb (cpu1_mem_wstrb ), + .mem_rdata (cpu1_mem_rdata ), + .trace_valid (cpu1_trace_valid), + .trace_data (cpu1_trace_data ) + ); +endmodule diff --git a/scripts/tomthumbtg/.gitignore b/scripts/tomthumbtg/.gitignore new file mode 100644 index 0000000..c1e6b04 --- /dev/null +++ b/scripts/tomthumbtg/.gitignore @@ -0,0 +1,15 @@ +testbench_a +testbench_b +testbench_c +testbench_d +testbench_e +testbench_f +testbench_g +testbench_h +testbench_i +testbench_j +testbench_k +testbench_l +testgen.tgz +testgen +tests diff --git a/scripts/tomthumbtg/README b/scripts/tomthumbtg/README new file mode 100644 index 0000000..4e12ba8 --- /dev/null +++ b/scripts/tomthumbtg/README @@ -0,0 +1,7 @@ + +Testing PicoRV32 using the test case generator from +the Tom Thumb RISC-V CPU project: + +https://github.com/maikmerten/riscv-tomthumb +https://github.com/maikmerten/riscv-tomthumb-testgen + diff --git a/scripts/tomthumbtg/run.sh b/scripts/tomthumbtg/run.sh new file mode 100644 index 0000000..63a6935 --- /dev/null +++ b/scripts/tomthumbtg/run.sh @@ -0,0 +1,43 @@ +#!/bin/bash + +set -ex + +if [ ! -f testgen.tgz ]; then + rm -f testgen.tgz.part + wget -O testgen.tgz.part http://maikmerten.de/testgen.tgz + mv testgen.tgz.part testgen.tgz +fi + +rm -rf tests testgen/ +tar xvzf testgen.tgz + +iverilog -o testbench_a -s testbench testbench.v ../../picorv32.v -DTWO_STAGE_SHIFT=0 -DBARREL_SHIFTER=0 -DTWO_CYCLE_COMPARE=0 -DTWO_CYCLE_ALU=0 +iverilog -o testbench_b -s testbench testbench.v ../../picorv32.v -DTWO_STAGE_SHIFT=1 -DBARREL_SHIFTER=0 -DTWO_CYCLE_COMPARE=0 -DTWO_CYCLE_ALU=0 +iverilog -o testbench_c -s testbench testbench.v ../../picorv32.v -DTWO_STAGE_SHIFT=0 -DBARREL_SHIFTER=1 -DTWO_CYCLE_COMPARE=0 -DTWO_CYCLE_ALU=0 + +iverilog -o testbench_d -s testbench testbench.v ../../picorv32.v -DTWO_STAGE_SHIFT=0 -DBARREL_SHIFTER=0 -DTWO_CYCLE_COMPARE=1 -DTWO_CYCLE_ALU=0 +iverilog -o testbench_e -s testbench testbench.v ../../picorv32.v -DTWO_STAGE_SHIFT=1 -DBARREL_SHIFTER=0 -DTWO_CYCLE_COMPARE=1 -DTWO_CYCLE_ALU=0 +iverilog -o testbench_f -s testbench testbench.v ../../picorv32.v -DTWO_STAGE_SHIFT=0 -DBARREL_SHIFTER=1 -DTWO_CYCLE_COMPARE=1 -DTWO_CYCLE_ALU=0 + +iverilog -o testbench_g -s testbench testbench.v ../../picorv32.v -DTWO_STAGE_SHIFT=0 -DBARREL_SHIFTER=0 -DTWO_CYCLE_COMPARE=0 -DTWO_CYCLE_ALU=1 +iverilog -o testbench_h -s testbench testbench.v ../../picorv32.v -DTWO_STAGE_SHIFT=1 -DBARREL_SHIFTER=0 -DTWO_CYCLE_COMPARE=0 -DTWO_CYCLE_ALU=1 +iverilog -o testbench_i -s testbench testbench.v ../../picorv32.v -DTWO_STAGE_SHIFT=0 -DBARREL_SHIFTER=1 -DTWO_CYCLE_COMPARE=0 -DTWO_CYCLE_ALU=1 + +iverilog -o testbench_j -s testbench testbench.v ../../picorv32.v -DTWO_STAGE_SHIFT=0 -DBARREL_SHIFTER=0 -DTWO_CYCLE_COMPARE=1 -DTWO_CYCLE_ALU=1 +iverilog -o testbench_k -s testbench testbench.v ../../picorv32.v -DTWO_STAGE_SHIFT=1 -DBARREL_SHIFTER=0 -DTWO_CYCLE_COMPARE=1 -DTWO_CYCLE_ALU=1 +iverilog -o testbench_l -s testbench testbench.v ../../picorv32.v -DTWO_STAGE_SHIFT=0 -DBARREL_SHIFTER=1 -DTWO_CYCLE_COMPARE=1 -DTWO_CYCLE_ALU=1 + +mkdir -p tests +for i in {0..999}; do + fn="tests/test_`printf '%03d' $i`" + + { + cat start.S + java -jar testgen/tomthumb-testgen-1.0-SNAPSHOT.jar + } > $fn.s + + riscv32-unknown-elf-gcc -ffreestanding -nostdlib -Wl,-Bstatic,-T,sections.lds -o $fn.elf $fn.s + riscv32-unknown-elf-objcopy -O binary $fn.elf $fn.bin + python3 ../../firmware/makehex.py $fn.bin 16384 > $fn.hex + for tb in testbench_{a,b,c,d,e,f,g,h,i,j,k,l}; do vvp -N $tb +hex=$fn.hex; done +done diff --git a/scripts/tomthumbtg/sections.lds b/scripts/tomthumbtg/sections.lds new file mode 100644 index 0000000..8962f5c --- /dev/null +++ b/scripts/tomthumbtg/sections.lds @@ -0,0 +1,7 @@ +SECTIONS { + .memory : { + . = 0; + *(.text); + *(*); + } +} diff --git a/scripts/tomthumbtg/start.S b/scripts/tomthumbtg/start.S new file mode 100644 index 0000000..541c8a4 --- /dev/null +++ b/scripts/tomthumbtg/start.S @@ -0,0 +1,57 @@ +.section .text.start +.global testcollection + +/* zero-initialize all registers */ +addi x1, zero, 0 +addi x2, zero, 0 +addi x3, zero, 0 +addi x4, zero, 0 +addi x5, zero, 0 +addi x6, zero, 0 +addi x7, zero, 0 +addi x8, zero, 0 +addi x9, zero, 0 +addi x10, zero, 0 +addi x11, zero, 0 +addi x12, zero, 0 +addi x13, zero, 0 +addi x14, zero, 0 +addi x15, zero, 0 +addi x16, zero, 0 +addi x17, zero, 0 +addi x18, zero, 0 +addi x19, zero, 0 +addi x20, zero, 0 +addi x21, zero, 0 +addi x22, zero, 0 +addi x23, zero, 0 +addi x24, zero, 0 +addi x25, zero, 0 +addi x26, zero, 0 +addi x27, zero, 0 +addi x28, zero, 0 +addi x29, zero, 0 +addi x30, zero, 0 +addi x31, zero, 0 + +/* set stack pointer */ +lui sp, %hi(64*1024) +addi sp, sp, %lo(64*1024) + +/* push zeros on the stack for argc and argv */ +/* (stack is aligned to 16 bytes in riscv calling convention) */ +addi sp,sp,-16 +sw zero,0(sp) +sw zero,4(sp) +sw zero,8(sp) +sw zero,12(sp) + +/* call test */ +call testcollection + +/* write test results */ +lui x1, %hi(0x10000000) +addi x1, x1, %lo(0x10000000) +sw x5, 0(x1) + +ebreak diff --git a/scripts/tomthumbtg/testbench.v b/scripts/tomthumbtg/testbench.v new file mode 100644 index 0000000..c39ebca --- /dev/null +++ b/scripts/tomthumbtg/testbench.v @@ -0,0 +1,83 @@ +`timescale 1 ns / 1 ps + +module testbench; + reg clk = 1; + reg resetn = 0; + wire trap; + + always #5 clk = ~clk; + + initial begin + repeat (100) @(posedge clk); + resetn <= 1; + end + + wire mem_valid; + wire mem_instr; + reg mem_ready; + wire [31:0] mem_addr; + wire [31:0] mem_wdata; + wire [3:0] mem_wstrb; + reg [31:0] mem_rdata; + + picorv32 #( + .TWO_STAGE_SHIFT(`TWO_STAGE_SHIFT), + .BARREL_SHIFTER(`BARREL_SHIFTER), + .TWO_CYCLE_COMPARE(`TWO_CYCLE_COMPARE), + .TWO_CYCLE_ALU(`TWO_CYCLE_ALU) + ) uut ( + .clk (clk ), + .resetn (resetn ), + .trap (trap ), + .mem_valid (mem_valid ), + .mem_instr (mem_instr ), + .mem_ready (mem_ready ), + .mem_addr (mem_addr ), + .mem_wdata (mem_wdata ), + .mem_wstrb (mem_wstrb ), + .mem_rdata (mem_rdata ) + ); + + reg [31:0] memory [0:16*1024-1]; + reg [1023:0] hex_filename; + + initial begin + if ($value$plusargs("hex=%s", hex_filename)) + $readmemh(hex_filename, memory); + end + + initial begin + // $dumpfile("testbench.vcd"); + // $dumpvars(0, testbench); + end + + always @(posedge clk) begin + if (resetn && trap) begin + repeat (10) @(posedge clk); + $display("TRAP"); + $stop; + end + end + + always @(posedge clk) begin + mem_ready <= 0; + if (mem_valid && !mem_ready) begin + mem_ready <= 1; + if (mem_addr == 32'h 1000_0000) begin + if (mem_wdata != -32'd1) begin + $display("Failed test case: %d", mem_wdata); + $stop; + end else begin + $display("OK."); + $finish; + end + end else begin + mem_rdata <= memory[mem_addr >> 2]; + if (mem_wstrb[0]) memory[mem_addr >> 2][ 7: 0] <= mem_wdata[ 7: 0]; + if (mem_wstrb[1]) memory[mem_addr >> 2][15: 8] <= mem_wdata[15: 8]; + if (mem_wstrb[2]) memory[mem_addr >> 2][23:16] <= mem_wdata[23:16]; + if (mem_wstrb[3]) memory[mem_addr >> 2][31:24] <= mem_wdata[31:24]; + end + end + end +endmodule diff --git a/scripts/torture/.gitignore b/scripts/torture/.gitignore new file mode 100644 index 0000000..b58f70b --- /dev/null +++ b/scripts/torture/.gitignore @@ -0,0 +1,14 @@ +.looplog +riscv-fesvr +riscv-isa-sim +riscv-torture +config.vh +obj_dir +tests +test.S +test.elf +test.bin +test.hex +test.ref +test.vvp +test.vcd diff --git a/scripts/torture/Makefile b/scripts/torture/Makefile new file mode 100644 index 0000000..4dd075c --- /dev/null +++ b/scripts/torture/Makefile @@ -0,0 +1,101 @@ + +# Icarus Verilog +#TESTBENCH_EXE = tests/testbench.vvp + +# Verilator +TESTBENCH_EXE = obj_dir/Vtestbench + +test: riscv-torture/build.ok riscv-isa-sim/build.ok + bash test.sh + +riscv-torture/build.ok: riscv-torture-rv32.diff + rm -rf riscv-torture + git clone https://github.com/ucb-bar/riscv-torture.git riscv-torture + cd riscv-torture && git checkout 2bc0c42 + cd riscv-torture && patch -p1 < ../riscv-torture-rv32.diff + cd riscv-torture && patch -p1 < ../riscv-torture-genloop.diff + cd riscv-torture && ./sbt generator/run && touch build.ok + +riscv-fesvr/build.ok: + rm -rf riscv-fesvr + git clone https://github.com/riscv/riscv-fesvr.git riscv-fesvr + +cd riscv-fesvr && git checkout 1c02bd6 && ./configure && make && touch build.ok + +riscv-isa-sim/build.ok: riscv-fesvr/build.ok + rm -rf riscv-isa-sim + git clone https://github.com/riscv/riscv-isa-sim.git riscv-isa-sim + cd riscv-isa-sim && git checkout 10ae74e + cd riscv-isa-sim && patch -p1 < ../riscv-isa-sim-sbreak.diff + cd riscv-isa-sim && patch -p1 < ../riscv-isa-sim-notrap.diff + cd riscv-isa-sim && LDFLAGS="-L../riscv-fesvr" ./configure --with-isa=RV32IMC + +cd riscv-isa-sim && ln -s ../riscv-fesvr/fesvr . && make && touch build.ok + +batch_size = 1000 +batch_list = $(shell bash -c 'for i in {0..$(shell expr $(batch_size) - 1)}; do printf "%03d\n" $$i; done') + +batch: $(addprefix tests/test_,$(addsuffix .ok,$(batch_list))) + +config.vh: config.py riscv-torture/build.ok + python3 config.py + +obj_dir/Vtestbench: testbench.v testbench.cc ../../picorv32.v config.vh + verilator --exe -Wno-fatal -DDEBUGASM --cc --top-module testbench testbench.v ../../picorv32.v testbench.cc + $(MAKE) -C obj_dir -f Vtestbench.mk + +tests/testbench.vvp: testbench.v ../../picorv32.v + mkdir -p tests + iverilog -o tests/testbench.vvp testbench.v ../../picorv32.v + +tests/generated.ok: config.vh riscv-torture/build.ok + mkdir -p tests + rm -f riscv-torture/output/test_* + cd riscv-torture && ./sbt 'generator/run -C config/test.config -n $(batch_size)' + touch tests/generated.ok + +define test_template +tests/test_$(1).S: tests/generated.ok + mv riscv-torture/output/test_$(1).S tests/ + touch tests/test_$(1).S + +tests/test_$(1).elf: tests/test_$(1).S + riscv32-unknown-elf-gcc `sed '/march=/ ! d; s,^// ,-,; y/RVIMC/rvimc/;' config.vh` -ffreestanding -nostdlib \ + -Wl,-Bstatic,-T,sections.lds -I. -o tests/test_$(1).elf tests/test_$(1).S + +tests/test_$(1).bin: tests/test_$(1).elf + riscv32-unknown-elf-objcopy -O binary tests/test_$(1).elf tests/test_$(1).bin + +tests/test_$(1).dmp: tests/test_$(1).elf + riscv32-unknown-elf-objdump -d tests/test_$(1).elf > tests/test_$(1).dmp + +tests/test_$(1).hex: tests/test_$(1).bin + python3 ../../firmware/makehex.py tests/test_$(1).bin 4096 > tests/test_$(1).hex + +tests/test_$(1).ref: tests/test_$(1).elf riscv-isa-sim/build.ok + LD_LIBRARY_PATH="./riscv-isa-sim:./riscv-fesvr" ./riscv-isa-sim/spike tests/test_$(1).elf > tests/test_$(1).ref + +tests/test_$(1).ok: $(TESTBENCH_EXE) tests/test_$(1).hex tests/test_$(1).ref tests/test_$(1).dmp + $(TESTBENCH_EXE) +hex=tests/test_$(1).hex +ref=tests/test_$(1).ref > tests/test_$(1).out + grep -q PASSED tests/test_$(1).out || { cat tests/test_$(1).out; false; } + python3 asmcheck.py tests/test_$(1).out tests/test_$(1).dmp + mv tests/test_$(1).out tests/test_$(1).ok +endef + +$(foreach id,$(batch_list),$(eval $(call test_template,$(id)))) + +loop: + date +"%s %Y-%m-%d %H:%M:%S START" >> .looplog + +set -ex; while true; do \ + rm -rf tests obj_dir config.vh; $(MAKE) batch; \ + date +"%s %Y-%m-%d %H:%M:%S NEXT" >> .looplog; \ + done + +clean: + rm -rf tests obj_dir + rm -f config.vh test.S test.elf test.bin + rm -f test.hex test.ref test.vvp test.vcd + +mrproper: clean + rm -rf riscv-torture riscv-fesvr riscv-isa-sim + +.PHONY: test batch loop clean mrproper + diff --git a/scripts/torture/README b/scripts/torture/README new file mode 100644 index 0000000..d62671d --- /dev/null +++ b/scripts/torture/README @@ -0,0 +1,6 @@ +Use UCB-BAR's RISC-V Torture Test Generator to test PicoRV32. + +You might need to install the following addition dependecies: + +sudo apt-get install python3-pip +pip3 install numpy diff --git a/scripts/torture/asmcheck.py b/scripts/torture/asmcheck.py new file mode 100644 index 0000000..8a22c67 --- /dev/null +++ b/scripts/torture/asmcheck.py @@ -0,0 +1,36 @@ +#!/usr/bin/env python3 + +import sys, re + +dmp_pattern = re.compile('^\s+([0-9a-f]+):\s+([0-9a-f]+)\s+(\S+)') +disassembled_elf = dict() + +def match_insns(s1, s2): + if s1 == "*" or s1 == s2: return True + if s1 == "jal" and s2.startswith("j"): return True + if s1 == "addi" and s2 in ["li", "mv"]: return True + if s1 == "xori" and s2 == "not": return True + if s1 == "sub" and s2 == "neg": return True + if s1.startswith("b") and s2.startswith("b"): return True + if s1.startswith("s") and s2.startswith("s"): return True + print(s1, s2) + return False + +with open(sys.argv[2], "r") as f: + for line in f: + match = dmp_pattern.match(line) + if match: + addr = match.group(1).rjust(8, '0') + opcode = match.group(2).rjust(8, '0') + insn = match.group(3) + disassembled_elf[addr] = (opcode, insn) + +with open(sys.argv[1], "r") as f: + for line in f: + line = line.split() + if len(line) < 1 or line[0] != "debugasm": + continue + assert(line[1] in disassembled_elf) + assert(line[2] == disassembled_elf[line[1]][0]) + assert(match_insns(line[3], disassembled_elf[line[1]][1])) + diff --git a/scripts/torture/config.py b/scripts/torture/config.py new file mode 100644 index 0000000..478f046 --- /dev/null +++ b/scripts/torture/config.py @@ -0,0 +1,35 @@ +#!/usr/bin/env python3 + +import numpy as np + +compressed_isa = np.random.randint(2) +enable_mul = np.random.randint(2) +enable_div = np.random.randint(2) + +with open("config.vh", "w") as f: + print("// march=RV32I%s%s" % ( + "M" if enable_mul or enable_div else "", + "C" if compressed_isa else ""), file=f) + print(".ENABLE_COUNTERS(%d)," % np.random.randint(2), file=f) + print(".ENABLE_COUNTERS64(%d)," % np.random.randint(2), file=f) + print(".ENABLE_REGS_DUALPORT(%d)," % np.random.randint(2), file=f) + print(".TWO_STAGE_SHIFT(%d)," % np.random.randint(2), file=f) + print(".BARREL_SHIFTER(%d)," % np.random.randint(2), file=f) + print(".TWO_CYCLE_COMPARE(%d)," % np.random.randint(2), file=f) + print(".TWO_CYCLE_ALU(%d)," % np.random.randint(2), file=f) + print(".CATCH_MISALIGN(%d)," % np.random.randint(2), file=f) + print(".CATCH_ILLINSN(%d)," % np.random.randint(2), file=f) + print(".COMPRESSED_ISA(%d)," % compressed_isa, file=f) + print(".ENABLE_MUL(%d)," % enable_mul, file=f) + print(".ENABLE_DIV(%d)" % enable_div, file=f) + +with open("riscv-torture/config/default.config", "r") as fi: + with open("riscv-torture/config/test.config", "w") as fo: + for line in fi: + line = line.strip() + if line.startswith("torture.generator.mul "): + line = "torture.generator.mul %s" % ("true" if enable_mul else "false") + if line.startswith("torture.generator.divider "): + line = "torture.generator.divider %s" % ("true" if enable_div else "false") + print(line, file=fo) + diff --git a/scripts/torture/riscv-isa-sim-notrap.diff b/scripts/torture/riscv-isa-sim-notrap.diff new file mode 100644 index 0000000..df7c059 --- /dev/null +++ b/scripts/torture/riscv-isa-sim-notrap.diff @@ -0,0 +1,16 @@ +diff --git a/riscv/processor.cc b/riscv/processor.cc +index 3b834c5..e112029 100644 +--- a/riscv/processor.cc ++++ b/riscv/processor.cc +@@ -201,9 +201,10 @@ void processor_t::set_privilege(reg_t prv) + + void processor_t::take_trap(trap_t& t, reg_t epc) + { +- if (debug) ++ // if (debug) + fprintf(stderr, "core %3d: exception %s, epc 0x%016" PRIx64 "\n", + id, t.name(), epc); ++ exit(1); + + // by default, trap to M-mode, unless delegated to S-mode + reg_t bit = t.cause(); diff --git a/scripts/torture/riscv-isa-sim-sbreak.diff b/scripts/torture/riscv-isa-sim-sbreak.diff new file mode 100644 index 0000000..9728fc8 --- /dev/null +++ b/scripts/torture/riscv-isa-sim-sbreak.diff @@ -0,0 +1,26 @@ +diff --git a/riscv/insns/c_ebreak.h b/riscv/insns/c_ebreak.h +index a17200f..af3a7ad 100644 +--- a/riscv/insns/c_ebreak.h ++++ b/riscv/insns/c_ebreak.h +@@ -1,2 +1,9 @@ + require_extension('C'); ++ ++for (int i = 0; i < 16*1024; i += 4) { ++ unsigned int dat = MMU.load_int32(i); ++ printf("%08x\n", dat); ++} ++exit(0); ++ + throw trap_breakpoint(); +diff --git a/riscv/insns/sbreak.h b/riscv/insns/sbreak.h +index c22776c..31397dd 100644 +--- a/riscv/insns/sbreak.h ++++ b/riscv/insns/sbreak.h +@@ -1 +1,7 @@ ++for (int i = 0; i < 16*1024; i += 4) { ++ unsigned int dat = MMU.load_int32(i); ++ printf("%08x\n", dat); ++} ++exit(0); ++ + throw trap_breakpoint(); diff --git a/scripts/torture/riscv-torture-genloop.diff b/scripts/torture/riscv-torture-genloop.diff new file mode 100644 index 0000000..a0a2fd1 --- /dev/null +++ b/scripts/torture/riscv-torture-genloop.diff @@ -0,0 +1,40 @@ +diff --git a/generator/src/main/scala/main.scala b/generator/src/main/scala/main.scala +index 7c78982..1572771 100644 +--- a/generator/src/main/scala/main.scala ++++ b/generator/src/main/scala/main.scala +@@ -8,7 +8,7 @@ import java.util.Properties + import scala.collection.JavaConversions._ + + case class Options(var outFileName: String = "test", +- var confFileName: String = "config/default.config") ++ var confFileName: String = "config/default.config", var numOutFiles: Int = 0) + + object Generator extends App + { +@@ -17,15 +17,25 @@ object Generator extends App + val parser = new OptionParser[Options]("generator/run") { + opt[String]('C', "config") valueName("<file>") text("config file") action {(s: String, c) => c.copy(confFileName = s)} + opt[String]('o', "output") valueName("<filename>") text("output filename") action {(s: String, c) => c.copy(outFileName = s)} ++ opt[Int]('n', "numfiles") valueName("<num_files>") text("number of output files") action {(n: Int, c) => c.copy(numOutFiles = n)} + } + parser.parse(args, Options()) match { + case Some(opts) => +- generate(opts.confFileName, opts.outFileName) ++ generate_loop(opts.confFileName, opts.outFileName, opts.numOutFiles) + case None => + System.exit(1) //error message printed by parser + } + } + ++ def generate_loop(confFile: String, outFileName: String, numOutFiles: Int) = { ++ if (numOutFiles > 0) { ++ for (i <- 0 to (numOutFiles-1)) ++ generate(confFile, outFileName + ("_%03d" format (i))) ++ } else { ++ generate(confFile, outFileName) ++ } ++ } ++ + def generate(confFile: String, outFileName: String): String = { + val config = new Properties() + val in = new FileInputStream(confFile) diff --git a/scripts/torture/riscv-torture-rv32.diff b/scripts/torture/riscv-torture-rv32.diff new file mode 100644 index 0000000..fef49b3 --- /dev/null +++ b/scripts/torture/riscv-torture-rv32.diff @@ -0,0 +1,141 @@ +diff --git a/config/default.config b/config/default.config +index b671223..c0b2bb4 100644 +--- a/config/default.config ++++ b/config/default.config +@@ -1,18 +1,18 @@ + torture.generator.nseqs 1000 + torture.generator.memsize 1024 + torture.generator.fprnd 0 +-torture.generator.amo true ++torture.generator.amo false + torture.generator.mul true + torture.generator.divider true + torture.generator.run_twice true + + torture.generator.mix.xmem 10 + torture.generator.mix.xbranch 20 +-torture.generator.mix.xalu 50 +-torture.generator.mix.fgen 10 +-torture.generator.mix.fpmem 5 +-torture.generator.mix.fax 3 +-torture.generator.mix.fdiv 2 ++torture.generator.mix.xalu 70 ++torture.generator.mix.fgen 0 ++torture.generator.mix.fpmem 0 ++torture.generator.mix.fax 0 ++torture.generator.mix.fdiv 0 + torture.generator.mix.vec 0 + + torture.generator.vec.vf 1 +diff --git a/generator/src/main/scala/HWRegPool.scala b/generator/src/main/scala/HWRegPool.scala +index de2ad8d..864bcc4 100644 +--- a/generator/src/main/scala/HWRegPool.scala ++++ b/generator/src/main/scala/HWRegPool.scala +@@ -86,7 +86,7 @@ trait PoolsMaster extends HWRegPool + + class XRegsPool extends ScalarRegPool + { +- val (name, regname, ldinst, stinst) = ("xreg", "reg_x", "ld", "sd") ++ val (name, regname, ldinst, stinst) = ("xreg", "reg_x", "lw", "sw") + + hwregs += new HWReg("x0", true, false) + for (i <- 1 to 31) +diff --git a/generator/src/main/scala/Prog.scala b/generator/src/main/scala/Prog.scala +index 6fb49e2..685c2f8 100644 +--- a/generator/src/main/scala/Prog.scala ++++ b/generator/src/main/scala/Prog.scala +@@ -385,7 +385,7 @@ class Prog(memsize: Int, veccfg: Map[String,String], run_twice: Boolean) + "\n" + + (if (using_vec) "RVTEST_RV64UV\n" + else if (using_fpu) "RVTEST_RV64UF\n" +- else "RVTEST_RV64U\n") + ++ else "RVTEST_RV32U\n") + + "RVTEST_CODE_BEGIN\n" + + (if (using_vec) init_vector() else "") + + "\n" + +diff --git a/generator/src/main/scala/Rand.scala b/generator/src/main/scala/Rand.scala +index a677d2d..ec0745f 100644 +--- a/generator/src/main/scala/Rand.scala ++++ b/generator/src/main/scala/Rand.scala +@@ -15,7 +15,7 @@ object Rand + low + Random.nextInt(span) + } + +- def rand_shamt() = rand_range(0, 63) ++ def rand_shamt() = rand_range(0, 31) + def rand_shamtw() = rand_range(0, 31) + def rand_seglen() = rand_range(0, 7) + def rand_imm() = rand_range(-2048, 2047) +diff --git a/generator/src/main/scala/SeqALU.scala b/generator/src/main/scala/SeqALU.scala +index a1f27a5..18d6d7b 100644 +--- a/generator/src/main/scala/SeqALU.scala ++++ b/generator/src/main/scala/SeqALU.scala +@@ -68,17 +68,12 @@ class SeqALU(xregs: HWRegPool, use_mul: Boolean, use_div: Boolean) extends InstS + candidates += seq_src1_immfn(SRAI, rand_shamt) + candidates += seq_src1_immfn(ORI, rand_imm) + candidates += seq_src1_immfn(ANDI, rand_imm) +- candidates += seq_src1_immfn(ADDIW, rand_imm) +- candidates += seq_src1_immfn(SLLIW, rand_shamtw) +- candidates += seq_src1_immfn(SRLIW, rand_shamtw) +- candidates += seq_src1_immfn(SRAIW, rand_shamtw) + + val oplist = new ArrayBuffer[Opcode] + + oplist += (ADD, SUB, SLL, SLT, SLTU, XOR, SRL, SRA, OR, AND) +- oplist += (ADDW, SUBW, SLLW, SRLW, SRAW) +- if (use_mul) oplist += (MUL, MULH, MULHSU, MULHU, MULW) +- if (use_div) oplist += (DIV, DIVU, REM, REMU, DIVW, DIVUW, REMW, REMUW) ++ if (use_mul) oplist += (MUL, MULH, MULHSU, MULHU) ++ if (use_div) oplist += (DIV, DIVU, REM, REMU) + + for (op <- oplist) + { +diff --git a/generator/src/main/scala/SeqBranch.scala b/generator/src/main/scala/SeqBranch.scala +index bba9895..0d257d7 100644 +--- a/generator/src/main/scala/SeqBranch.scala ++++ b/generator/src/main/scala/SeqBranch.scala +@@ -75,7 +75,7 @@ class SeqBranch(xregs: HWRegPool) extends InstSeq + val reg_mask = reg_write_visible(xregs) + + insts += ADDI(reg_one, reg_read_zero(xregs), Imm(1)) +- insts += SLL(reg_one, reg_one, Imm(63)) ++ insts += SLL(reg_one, reg_one, Imm(31)) + insts += ADDI(reg_mask, reg_read_zero(xregs), Imm(-1)) + insts += XOR(reg_mask, reg_mask, reg_one) + insts += AND(reg_dst1, reg_src, reg_mask) +@@ -95,7 +95,7 @@ class SeqBranch(xregs: HWRegPool) extends InstSeq + val reg_mask = reg_write_visible(xregs) + + insts += ADDI(reg_one, reg_read_zero(xregs), Imm(1)) +- insts += SLL(reg_one, reg_one, Imm(63)) ++ insts += SLL(reg_one, reg_one, Imm(31)) + insts += ADDI(reg_mask, reg_read_zero(xregs), Imm(-1)) + insts += XOR(reg_mask, reg_mask, reg_one) + insts += AND(reg_dst1, reg_src1, reg_mask) +diff --git a/generator/src/main/scala/SeqMem.scala b/generator/src/main/scala/SeqMem.scala +index 3c180ed..89200f6 100644 +--- a/generator/src/main/scala/SeqMem.scala ++++ b/generator/src/main/scala/SeqMem.scala +@@ -51,7 +51,7 @@ class SeqMem(xregs: HWRegPool, mem: Mem, use_amo: Boolean) extends InstSeq + + def getRandOpAndAddr (dw_addr: Int, is_store: Boolean): (Opcode, Int) = + { +- val typ = AccessType.values.toIndexedSeq(rand_range(0,6)) ++ val typ = AccessType.values.toIndexedSeq(rand_range(0,4)) + if (is_store) + { + if (typ == byte || typ ==ubyte) (SB, dw_addr + rand_addr_b(8)) +@@ -110,13 +110,10 @@ class SeqMem(xregs: HWRegPool, mem: Mem, use_amo: Boolean) extends InstSeq + candidates += seq_load_addrfn(LH, rand_addr_h) + candidates += seq_load_addrfn(LHU, rand_addr_h) + candidates += seq_load_addrfn(LW, rand_addr_w) +- candidates += seq_load_addrfn(LWU, rand_addr_w) +- candidates += seq_load_addrfn(LD, rand_addr_d) + + candidates += seq_store_addrfn(SB, rand_addr_b) + candidates += seq_store_addrfn(SH, rand_addr_h) + candidates += seq_store_addrfn(SW, rand_addr_w) +- candidates += seq_store_addrfn(SD, rand_addr_d) + + if (use_amo) + { diff --git a/scripts/torture/riscv_test.h b/scripts/torture/riscv_test.h new file mode 100644 index 0000000..36c5b54 --- /dev/null +++ b/scripts/torture/riscv_test.h @@ -0,0 +1,13 @@ +#ifndef RISCV_TEST_H +#define RISCV_TEST_H + +#define RVTEST_RV32U +#define RVTEST_CODE_BEGIN +#define RVTEST_CODE_END +#define RVTEST_DATA_BEGIN +#define RVTEST_DATA_END + +#define RVTEST_FAIL ebreak +#define RVTEST_PASS ebreak + +#endif diff --git a/scripts/torture/sections.lds b/scripts/torture/sections.lds new file mode 100644 index 0000000..a9487e2 --- /dev/null +++ b/scripts/torture/sections.lds @@ -0,0 +1,9 @@ +SECTIONS { + .memory : { + . = 0x000000; + *(.text); + *(*); + end = .; + } +} + diff --git a/scripts/torture/test.sh b/scripts/torture/test.sh new file mode 100644 index 0000000..17c5a7c --- /dev/null +++ b/scripts/torture/test.sh @@ -0,0 +1,32 @@ +#!/bin/bash + +set -ex + + +## Generate test case + +if ! test -f config.vh; then + python3 config.py +fi + +if ! test -f test.S; then + cd riscv-torture + ./sbt "generator/run -C config/test.config" + cp output/test.S ../test.S + cd .. +fi + + +## Compile test case and create reference + +riscv32-unknown-elf-gcc `sed '/march=/ ! d; s,^// ,-,; y/RVIMC/rvimc/;' config.vh` -ffreestanding -nostdlib -Wl,-Bstatic,-T,sections.lds -o test.elf test.S +LD_LIBRARY_PATH="./riscv-isa-sim:./riscv-fesvr" ./riscv-isa-sim/spike test.elf > test.ref +riscv32-unknown-elf-objcopy -O binary test.elf test.bin +python3 ../../firmware/makehex.py test.bin 4096 > test.hex + + +## Run test + +iverilog -o test.vvp testbench.v ../../picorv32.v +vvp test.vvp +vcd +hex=test.hex +ref=test.ref + diff --git a/scripts/torture/testbench.cc b/scripts/torture/testbench.cc new file mode 100644 index 0000000..2925d0b --- /dev/null +++ b/scripts/torture/testbench.cc @@ -0,0 +1,18 @@ +#include "Vtestbench.h" +#include "verilated.h" + +int main(int argc, char **argv, char **env) +{ + Verilated::commandArgs(argc, argv); + Vtestbench* top = new Vtestbench; + + top->clk = 0; + while (!Verilated::gotFinish()) { + top->clk = !top->clk; + top->eval(); + } + + delete top; + exit(0); +} + diff --git a/scripts/torture/testbench.v b/scripts/torture/testbench.v new file mode 100644 index 0000000..326de0e --- /dev/null +++ b/scripts/torture/testbench.v @@ -0,0 +1,134 @@ +module testbench ( +`ifdef VERILATOR + input clk +`endif +); +`ifndef VERILATOR + reg clk = 1; + always #5 clk = ~clk; +`endif + reg resetn = 0; + wire trap; + + wire mem_valid; + wire mem_instr; + reg mem_ready; + wire [31:0] mem_addr; + wire [31:0] mem_wdata; + wire [3:0] mem_wstrb; + reg [31:0] mem_rdata; + + wire mem_la_read; + wire mem_la_write; + wire [31:0] mem_la_addr; + wire [31:0] mem_la_wdata; + wire [3:0] mem_la_wstrb; + + reg [31:0] x32 = 314159265; + reg [31:0] next_x32; + + always @(posedge clk) begin + if (resetn) begin + next_x32 = x32; + next_x32 = next_x32 ^ (next_x32 << 13); + next_x32 = next_x32 ^ (next_x32 >> 17); + next_x32 = next_x32 ^ (next_x32 << 5); + x32 <= next_x32; + end + end + + picorv32 #( +`include "config.vh" + ) uut ( + .clk (clk ), + .resetn (resetn ), + .trap (trap ), + + .mem_valid (mem_valid ), + .mem_instr (mem_instr ), + .mem_ready (mem_ready ), + .mem_addr (mem_addr ), + .mem_wdata (mem_wdata ), + .mem_wstrb (mem_wstrb ), + .mem_rdata (mem_rdata ), + + .mem_la_read (mem_la_read ), + .mem_la_write(mem_la_write), + .mem_la_addr (mem_la_addr ), + .mem_la_wdata(mem_la_wdata), + .mem_la_wstrb(mem_la_wstrb) + ); + + localparam integer filename_len = 18; + reg [8*filename_len-1:0] hex_filename; + reg [8*filename_len-1:0] ref_filename; + + reg [31:0] memory [0:4095]; + reg [31:0] memory_ref [0:4095]; + integer i, errcount; + integer cycle = 0; + + initial begin + if ($value$plusargs("hex=%s", hex_filename)) $readmemh(hex_filename, memory); + if ($value$plusargs("ref=%s", ref_filename)) $readmemh(ref_filename, memory_ref); +`ifndef VERILATOR + if ($test$plusargs("vcd")) begin + $dumpfile("test.vcd"); + $dumpvars(0, testbench); + end +`endif + end + + always @(posedge clk) begin + mem_ready <= 0; + mem_rdata <= 'bx; + + if (!trap || !resetn) begin + if (x32[0] && resetn) begin + if (mem_la_read) begin + mem_ready <= 1; + mem_rdata <= memory[mem_la_addr >> 2]; + end else + if (mem_la_write) begin + mem_ready <= 1; + if (mem_la_wstrb[0]) memory[mem_la_addr >> 2][ 7: 0] <= mem_la_wdata[ 7: 0]; + if (mem_la_wstrb[1]) memory[mem_la_addr >> 2][15: 8] <= mem_la_wdata[15: 8]; + if (mem_la_wstrb[2]) memory[mem_la_addr >> 2][23:16] <= mem_la_wdata[23:16]; + if (mem_la_wstrb[3]) memory[mem_la_addr >> 2][31:24] <= mem_la_wdata[31:24]; + end else + if (mem_valid && !mem_ready) begin + mem_ready <= 1; + if (mem_wstrb) begin + if (mem_wstrb[0]) memory[mem_addr >> 2][ 7: 0] <= mem_wdata[ 7: 0]; + if (mem_wstrb[1]) memory[mem_addr >> 2][15: 8] <= mem_wdata[15: 8]; + if (mem_wstrb[2]) memory[mem_addr >> 2][23:16] <= mem_wdata[23:16]; + if (mem_wstrb[3]) memory[mem_addr >> 2][31:24] <= mem_wdata[31:24]; + end else begin + mem_rdata <= memory[mem_addr >> 2]; + end + end + end + end else begin + errcount = 0; + for (i=0; i < 4096; i=i+1) begin + if (memory[i] !== memory_ref[i]) begin + $display("Signature check failed at %04x: mem=%08x ref=%08x", i << 2, memory[i], memory_ref[i]); + errcount = errcount + 1; + end + end + if (errcount) + $display("FAILED: Got %1d errors for %1s => %1s!", errcount, hex_filename, ref_filename); + else + $display("PASSED %1s => %1s.", hex_filename, ref_filename); + $finish; + end + + if (cycle > 100000) begin + $display("FAILED: Timeout!"); + $finish; + end + + resetn <= cycle > 10; + cycle <= cycle + 1; + end +endmodule diff --git a/scripts/vivado/.gitignore b/scripts/vivado/.gitignore new file mode 100644 index 0000000..2374269 --- /dev/null +++ b/scripts/vivado/.gitignore @@ -0,0 +1,18 @@ +.Xil/ +firmware.bin +firmware.elf +firmware.hex +firmware.map +synth_*.log +synth_*.mmi +synth_*.bit +synth_system.v +table.txt +tab_*/ +webtalk.jou +webtalk.log +webtalk_*.jou +webtalk_*.log +xelab.* +xsim.* +xvlog.* diff --git a/scripts/vivado/Makefile b/scripts/vivado/Makefile new file mode 100644 index 0000000..3c92901 --- /dev/null +++ b/scripts/vivado/Makefile @@ -0,0 +1,69 @@ + +VIVADO_BASE = /opt/Xilinx/Vivado/2018.2 +VIVADO = $(VIVADO_BASE)/bin/vivado +XVLOG = $(VIVADO_BASE)/bin/xvlog +XELAB = $(VIVADO_BASE)/bin/xelab +GLBL = $(VIVADO_BASE)/data/verilog/src/glbl.v +TOOLCHAIN_PREFIX = riscv32-unknown-elf- + +export VIVADO + +# work-around for http://svn.clifford.at/handicraft/2016/vivadosig11 +export RDI_VERBOSE = False + +help: + @echo "" + @echo "Simple synthesis tests:" + @echo " make synth_area_{small|regular|large}" + @echo " make synth_speed" + @echo "" + @echo "Example system:" + @echo " make synth_system" + @echo " make sim_system" + @echo "" + @echo "Timing and Utilization Evaluation:" + @echo " make table.txt" + @echo " make area" + @echo "" + +synth_%: + rm -f $@.log + $(VIVADO) -nojournal -log $@.log -mode batch -source $@.tcl + rm -rf .Xil fsm_encoding.os synth_*.backup.log usage_statistics_webtalk.* + -grep -B4 -A10 'Slice LUTs' $@.log + -grep -B1 -A9 ^Slack $@.log && echo + +synth_system: firmware.hex + +sim_system: + $(XVLOG) system_tb.v synth_system.v + $(XVLOG) $(GLBL) + $(XELAB) -L unifast_ver -L unisims_ver -R system_tb glbl + +firmware.hex: firmware.S firmware.c firmware.lds + $(TOOLCHAIN_PREFIX)gcc -Os -ffreestanding -nostdlib -o firmware.elf firmware.S firmware.c \ + --std=gnu99 -Wl,-Bstatic,-T,firmware.lds,-Map,firmware.map,--strip-debug -lgcc + $(TOOLCHAIN_PREFIX)objcopy -O binary firmware.elf firmware.bin + python3 ../../firmware/makehex.py firmware.bin 4096 > firmware.hex + +tab_%/results.txt: + bash tabtest.sh $@ + +area: synth_area_small synth_area_regular synth_area_large + -grep -B4 -A10 'Slice LUTs' synth_area_small.log synth_area_regular.log synth_area_large.log + +table.txt: tab_small_xc7k_2/results.txt tab_small_xc7k_3/results.txt +table.txt: tab_small_xc7v_2/results.txt tab_small_xc7v_3/results.txt +table.txt: tab_small_xcku_2/results.txt tab_small_xcku_3/results.txt +table.txt: tab_small_xcvu_2/results.txt tab_small_xcvu_3/results.txt +table.txt: tab_small_xckup_2/results.txt tab_small_xckup_3/results.txt +table.txt: tab_small_xcvup_2/results.txt tab_small_xcvup_3/results.txt + +table.txt: + bash table.sh > table.txt + +clean: + rm -rf .Xil/ firmware.bin firmware.elf firmware.hex firmware.map synth_*.log + rm -rf synth_*.mmi synth_*.bit synth_system.v table.txt tab_*/ webtalk.jou + rm -rf webtalk.log webtalk_*.jou webtalk_*.log xelab.* xsim[._]* xvlog.* + diff --git a/scripts/vivado/firmware.S b/scripts/vivado/firmware.S new file mode 100644 index 0000000..c55a3ba --- /dev/null +++ b/scripts/vivado/firmware.S @@ -0,0 +1,12 @@ +.section .init +.global main + +/* set stack pointer */ +lui sp, %hi(16*1024) +addi sp, sp, %lo(16*1024) + +/* call main */ +jal ra, main + +/* break */ +ebreak diff --git a/scripts/vivado/firmware.c b/scripts/vivado/firmware.c new file mode 100644 index 0000000..6c62169 --- /dev/null +++ b/scripts/vivado/firmware.c @@ -0,0 +1,43 @@ +void putc(char c) +{ + *(volatile char*)0x10000000 = c; +} + +void puts(const char *s) +{ + while (*s) putc(*s++); +} + +void *memcpy(void *dest, const void *src, int n) +{ + while (n) { + n--; + ((char*)dest)[n] = ((char*)src)[n]; + } + return dest; +} + +void main() +{ + char message[] = "$Uryyb+Jbeyq!+Vs+lbh+pna+ernq+guvf+zrffntr+gura$gur+CvpbEI32+PCH" + "+frrzf+gb+or+jbexvat+whfg+svar.$$++++++++++++++++GRFG+CNFFRQ!$$"; + for (int i = 0; message[i]; i++) + switch (message[i]) + { + case 'a' ... 'm': + case 'A' ... 'M': + message[i] += 13; + break; + case 'n' ... 'z': + case 'N' ... 'Z': + message[i] -= 13; + break; + case '$': + message[i] = '\n'; + break; + case '+': + message[i] = ' '; + break; + } + puts(message); +} diff --git a/scripts/vivado/firmware.lds b/scripts/vivado/firmware.lds new file mode 100644 index 0000000..970000a --- /dev/null +++ b/scripts/vivado/firmware.lds @@ -0,0 +1,11 @@ +SECTIONS { + .memory : { + . = 0x000000; + *(.init); + *(.text); + *(*); + . = ALIGN(4); + end = .; + } +} + diff --git a/scripts/vivado/synth_area.tcl b/scripts/vivado/synth_area.tcl new file mode 100644 index 0000000..c222a00 --- /dev/null +++ b/scripts/vivado/synth_area.tcl @@ -0,0 +1,8 @@ +read_verilog ../../picorv32.v +read_xdc synth_area.xdc + +synth_design -part xc7k70t-fbg676 -top picorv32_axi +opt_design -resynth_seq_area + +report_utilization +report_timing diff --git a/scripts/vivado/synth_area.xdc b/scripts/vivado/synth_area.xdc new file mode 100644 index 0000000..3c3d5a1 --- /dev/null +++ b/scripts/vivado/synth_area.xdc @@ -0,0 +1 @@ +create_clock -period 20.00 [get_ports clk] diff --git a/scripts/vivado/synth_area_large.tcl b/scripts/vivado/synth_area_large.tcl new file mode 100644 index 0000000..af611b5 --- /dev/null +++ b/scripts/vivado/synth_area_large.tcl @@ -0,0 +1,10 @@ +read_verilog ../../picorv32.v +read_verilog synth_area_top.v +read_xdc synth_area.xdc + +synth_design -part xc7k70t-fbg676 -top top_large +opt_design -sweep -propconst -resynth_seq_area +opt_design -directive ExploreSequentialArea + +report_utilization +report_timing diff --git a/scripts/vivado/synth_area_regular.tcl b/scripts/vivado/synth_area_regular.tcl new file mode 100644 index 0000000..2bf6b4c --- /dev/null +++ b/scripts/vivado/synth_area_regular.tcl @@ -0,0 +1,10 @@ +read_verilog ../../picorv32.v +read_verilog synth_area_top.v +read_xdc synth_area.xdc + +synth_design -part xc7k70t-fbg676 -top top_regular +opt_design -sweep -propconst -resynth_seq_area +opt_design -directive ExploreSequentialArea + +report_utilization +report_timing diff --git a/scripts/vivado/synth_area_small.tcl b/scripts/vivado/synth_area_small.tcl new file mode 100644 index 0000000..11d2104 --- /dev/null +++ b/scripts/vivado/synth_area_small.tcl @@ -0,0 +1,10 @@ +read_verilog ../../picorv32.v +read_verilog synth_area_top.v +read_xdc synth_area.xdc + +synth_design -part xc7k70t-fbg676 -top top_small +opt_design -sweep -propconst -resynth_seq_area +opt_design -directive ExploreSequentialArea + +report_utilization +report_timing diff --git a/scripts/vivado/synth_area_top.v b/scripts/vivado/synth_area_top.v new file mode 100644 index 0000000..6298a86 --- /dev/null +++ b/scripts/vivado/synth_area_top.v @@ -0,0 +1,140 @@ + +module top_small ( + input clk, resetn, + + output mem_valid, + output mem_instr, + input mem_ready, + + output [31:0] mem_addr, + output [31:0] mem_wdata, + output [ 3:0] mem_wstrb, + input [31:0] mem_rdata +); + picorv32 #( + .ENABLE_COUNTERS(0), + .LATCHED_MEM_RDATA(1), + .TWO_STAGE_SHIFT(0), + .CATCH_MISALIGN(0), + .CATCH_ILLINSN(0) + ) picorv32 ( + .clk (clk ), + .resetn (resetn ), + .mem_valid(mem_valid), + .mem_instr(mem_instr), + .mem_ready(mem_ready), + .mem_addr (mem_addr ), + .mem_wdata(mem_wdata), + .mem_wstrb(mem_wstrb), + .mem_rdata(mem_rdata) + ); +endmodule + +module top_regular ( + input clk, resetn, + output trap, + + output mem_valid, + output mem_instr, + input mem_ready, + + output [31:0] mem_addr, + output [31:0] mem_wdata, + output [ 3:0] mem_wstrb, + input [31:0] mem_rdata, + + // Look-Ahead Interface + output mem_la_read, + output mem_la_write, + output [31:0] mem_la_addr, + output [31:0] mem_la_wdata, + output [ 3:0] mem_la_wstrb +); + picorv32 picorv32 ( + .clk (clk ), + .resetn (resetn ), + .trap (trap ), + .mem_valid (mem_valid ), + .mem_instr (mem_instr ), + .mem_ready (mem_ready ), + .mem_addr (mem_addr ), + .mem_wdata (mem_wdata ), + .mem_wstrb (mem_wstrb ), + .mem_rdata (mem_rdata ), + .mem_la_read (mem_la_read ), + .mem_la_write(mem_la_write), + .mem_la_addr (mem_la_addr ), + .mem_la_wdata(mem_la_wdata), + .mem_la_wstrb(mem_la_wstrb) + ); +endmodule + +module top_large ( + input clk, resetn, + output trap, + + output mem_valid, + output mem_instr, + input mem_ready, + + output [31:0] mem_addr, + output [31:0] mem_wdata, + output [ 3:0] mem_wstrb, + input [31:0] mem_rdata, + + // Look-Ahead Interface + output mem_la_read, + output mem_la_write, + output [31:0] mem_la_addr, + output [31:0] mem_la_wdata, + output [ 3:0] mem_la_wstrb, + + // Pico Co-Processor Interface (PCPI) + output pcpi_valid, + output [31:0] pcpi_insn, + output [31:0] pcpi_rs1, + output [31:0] pcpi_rs2, + input pcpi_wr, + input [31:0] pcpi_rd, + input pcpi_wait, + input pcpi_ready, + + // IRQ Interface + input [31:0] irq, + output [31:0] eoi +); + picorv32 #( + .COMPRESSED_ISA(1), + .BARREL_SHIFTER(1), + .ENABLE_PCPI(1), + .ENABLE_MUL(1), + .ENABLE_IRQ(1) + ) picorv32 ( + .clk (clk ), + .resetn (resetn ), + .trap (trap ), + .mem_valid (mem_valid ), + .mem_instr (mem_instr ), + .mem_ready (mem_ready ), + .mem_addr (mem_addr ), + .mem_wdata (mem_wdata ), + .mem_wstrb (mem_wstrb ), + .mem_rdata (mem_rdata ), + .mem_la_read (mem_la_read ), + .mem_la_write (mem_la_write ), + .mem_la_addr (mem_la_addr ), + .mem_la_wdata (mem_la_wdata ), + .mem_la_wstrb (mem_la_wstrb ), + .pcpi_valid (pcpi_valid ), + .pcpi_insn (pcpi_insn ), + .pcpi_rs1 (pcpi_rs1 ), + .pcpi_rs2 (pcpi_rs2 ), + .pcpi_wr (pcpi_wr ), + .pcpi_rd (pcpi_rd ), + .pcpi_wait (pcpi_wait ), + .pcpi_ready (pcpi_ready ), + .irq (irq ), + .eoi (eoi ) + ); +endmodule + diff --git a/scripts/vivado/synth_speed.tcl b/scripts/vivado/synth_speed.tcl new file mode 100644 index 0000000..f3874e4 --- /dev/null +++ b/scripts/vivado/synth_speed.tcl @@ -0,0 +1,13 @@ + +read_verilog ../../picorv32.v +read_xdc synth_speed.xdc + +synth_design -part xc7k70t-fbg676 -top picorv32_axi +opt_design +place_design +phys_opt_design +route_design + +report_utilization +report_timing + diff --git a/scripts/vivado/synth_speed.xdc b/scripts/vivado/synth_speed.xdc new file mode 100644 index 0000000..877ec8d --- /dev/null +++ b/scripts/vivado/synth_speed.xdc @@ -0,0 +1 @@ +create_clock -period 2.50 [get_ports clk] diff --git a/scripts/vivado/synth_system.tcl b/scripts/vivado/synth_system.tcl new file mode 100644 index 0000000..26ea01c --- /dev/null +++ b/scripts/vivado/synth_system.tcl @@ -0,0 +1,17 @@ + +read_verilog system.v +read_verilog ../../picorv32.v +read_xdc synth_system.xdc + +synth_design -part xc7a35t-cpg236-1 -top system +opt_design +place_design +route_design + +report_utilization +report_timing + +write_verilog -force synth_system.v +write_bitstream -force synth_system.bit +# write_mem_info -force synth_system.mmi + diff --git a/scripts/vivado/synth_system.xdc b/scripts/vivado/synth_system.xdc new file mode 100644 index 0000000..5748466 --- /dev/null +++ b/scripts/vivado/synth_system.xdc @@ -0,0 +1,34 @@ + +# XDC File for Basys3 Board +########################### + +set_property PACKAGE_PIN W5 [get_ports clk] +set_property IOSTANDARD LVCMOS33 [get_ports clk] +create_clock -period 10.00 [get_ports clk] + +# Pmod Header JA (JA0..JA7) +set_property PACKAGE_PIN J1 [get_ports {out_byte[0]}] +set_property IOSTANDARD LVCMOS33 [get_ports {out_byte[0]}] +set_property PACKAGE_PIN L2 [get_ports {out_byte[1]}] +set_property IOSTANDARD LVCMOS33 [get_ports {out_byte[1]}] +set_property PACKAGE_PIN J2 [get_ports {out_byte[2]}] +set_property IOSTANDARD LVCMOS33 [get_ports {out_byte[2]}] +set_property PACKAGE_PIN G2 [get_ports {out_byte[3]}] +set_property IOSTANDARD LVCMOS33 [get_ports {out_byte[3]}] +set_property PACKAGE_PIN H1 [get_ports {out_byte[4]}] +set_property IOSTANDARD LVCMOS33 [get_ports {out_byte[4]}] +set_property PACKAGE_PIN K2 [get_ports {out_byte[5]}] +set_property IOSTANDARD LVCMOS33 [get_ports {out_byte[5]}] +set_property PACKAGE_PIN H2 [get_ports {out_byte[6]}] +set_property IOSTANDARD LVCMOS33 [get_ports {out_byte[6]}] +set_property PACKAGE_PIN G3 [get_ports {out_byte[7]}] +set_property IOSTANDARD LVCMOS33 [get_ports {out_byte[7]}] + +# Pmod Header JB (JB0..JB2) +set_property PACKAGE_PIN A14 [get_ports {resetn}] +set_property IOSTANDARD LVCMOS33 [get_ports {resetn}] +set_property PACKAGE_PIN A16 [get_ports {trap}] +set_property IOSTANDARD LVCMOS33 [get_ports {trap}] +set_property PACKAGE_PIN B15 [get_ports {out_byte_en}] +set_property IOSTANDARD LVCMOS33 [get_ports {out_byte_en}] + diff --git a/scripts/vivado/system.v b/scripts/vivado/system.v new file mode 100644 index 0000000..c4882a1 --- /dev/null +++ b/scripts/vivado/system.v @@ -0,0 +1,101 @@ +`timescale 1 ns / 1 ps + +module system ( + input clk, + input resetn, + output trap, + output reg [7:0] out_byte, + output reg out_byte_en +); + // set this to 0 for better timing but less performance/MHz + parameter FAST_MEMORY = 1; + + // 4096 32bit words = 16kB memory + parameter MEM_SIZE = 4096; + + wire mem_valid; + wire mem_instr; + reg mem_ready; + wire [31:0] mem_addr; + wire [31:0] mem_wdata; + wire [3:0] mem_wstrb; + reg [31:0] mem_rdata; + + wire mem_la_read; + wire mem_la_write; + wire [31:0] mem_la_addr; + wire [31:0] mem_la_wdata; + wire [3:0] mem_la_wstrb; + + picorv32 picorv32_core ( + .clk (clk ), + .resetn (resetn ), + .trap (trap ), + .mem_valid (mem_valid ), + .mem_instr (mem_instr ), + .mem_ready (mem_ready ), + .mem_addr (mem_addr ), + .mem_wdata (mem_wdata ), + .mem_wstrb (mem_wstrb ), + .mem_rdata (mem_rdata ), + .mem_la_read (mem_la_read ), + .mem_la_write(mem_la_write), + .mem_la_addr (mem_la_addr ), + .mem_la_wdata(mem_la_wdata), + .mem_la_wstrb(mem_la_wstrb) + ); + + reg [31:0] memory [0:MEM_SIZE-1]; + initial $readmemh("firmware.hex", memory); + + reg [31:0] m_read_data; + reg m_read_en; + + generate if (FAST_MEMORY) begin + always @(posedge clk) begin + mem_ready <= 1; + out_byte_en <= 0; + mem_rdata <= memory[mem_la_addr >> 2]; + if (mem_la_write && (mem_la_addr >> 2) < MEM_SIZE) begin + if (mem_la_wstrb[0]) memory[mem_la_addr >> 2][ 7: 0] <= mem_la_wdata[ 7: 0]; + if (mem_la_wstrb[1]) memory[mem_la_addr >> 2][15: 8] <= mem_la_wdata[15: 8]; + if (mem_la_wstrb[2]) memory[mem_la_addr >> 2][23:16] <= mem_la_wdata[23:16]; + if (mem_la_wstrb[3]) memory[mem_la_addr >> 2][31:24] <= mem_la_wdata[31:24]; + end + else + if (mem_la_write && mem_la_addr == 32'h1000_0000) begin + out_byte_en <= 1; + out_byte <= mem_la_wdata; + end + end + end else begin + always @(posedge clk) begin + m_read_en <= 0; + mem_ready <= mem_valid && !mem_ready && m_read_en; + + m_read_data <= memory[mem_addr >> 2]; + mem_rdata <= m_read_data; + + out_byte_en <= 0; + + (* parallel_case *) + case (1) + mem_valid && !mem_ready && !mem_wstrb && (mem_addr >> 2) < MEM_SIZE: begin + m_read_en <= 1; + end + mem_valid && !mem_ready && |mem_wstrb && (mem_addr >> 2) < MEM_SIZE: begin + if (mem_wstrb[0]) memory[mem_addr >> 2][ 7: 0] <= mem_wdata[ 7: 0]; + if (mem_wstrb[1]) memory[mem_addr >> 2][15: 8] <= mem_wdata[15: 8]; + if (mem_wstrb[2]) memory[mem_addr >> 2][23:16] <= mem_wdata[23:16]; + if (mem_wstrb[3]) memory[mem_addr >> 2][31:24] <= mem_wdata[31:24]; + mem_ready <= 1; + end + mem_valid && !mem_ready && |mem_wstrb && mem_addr == 32'h1000_0000: begin + out_byte_en <= 1; + out_byte <= mem_wdata; + mem_ready <= 1; + end + endcase + end + end endgenerate +endmodule diff --git a/scripts/vivado/system_tb.v b/scripts/vivado/system_tb.v new file mode 100644 index 0000000..a66d612 --- /dev/null +++ b/scripts/vivado/system_tb.v @@ -0,0 +1,38 @@ +`timescale 1 ns / 1 ps + +module system_tb; + reg clk = 1; + always #5 clk = ~clk; + + reg resetn = 0; + initial begin + if ($test$plusargs("vcd")) begin + $dumpfile("system.vcd"); + $dumpvars(0, system_tb); + end + repeat (100) @(posedge clk); + resetn <= 1; + end + + wire trap; + wire [7:0] out_byte; + wire out_byte_en; + + system uut ( + .clk (clk ), + .resetn (resetn ), + .trap (trap ), + .out_byte (out_byte ), + .out_byte_en(out_byte_en) + ); + + always @(posedge clk) begin + if (resetn && out_byte_en) begin + $write("%c", out_byte); + $fflush; + end + if (resetn && trap) begin + $finish; + end + end +endmodule diff --git a/scripts/vivado/table.sh b/scripts/vivado/table.sh new file mode 100644 index 0000000..81e2cf4 --- /dev/null +++ b/scripts/vivado/table.sh @@ -0,0 +1,21 @@ +#!/bin/bash + +dashes="----------------------------------------------------------------" +printf '| %-25s | %-10s | %-20s |\n' "Device" "Speedgrade" "Clock Period (Freq.)" +printf '|:%.25s |:%.10s:| %.20s:|\n' $dashes $dashes $dashes + +for x in $( grep -H . tab_*/results.txt ) +do + read _ size device grade _ speed < <( echo "$x" | tr _/: ' ' ) + case "$device" in + xc7a) d="Xilinx Artix-7T" ;; + xc7k) d="Xilinx Kintex-7T" ;; + xc7v) d="Xilinx Virtex-7T" ;; + xcku) d="Xilinx Kintex UltraScale" ;; + xcvu) d="Xilinx Virtex UltraScale" ;; + xckup) d="Xilinx Kintex UltraScale+" ;; + xcvup) d="Xilinx Virtex UltraScale+" ;; + esac + speedtxt=$( printf '%s.%s ns (%d MHz)' ${speed%?} ${speed#?} $((10000 / speed)) ) + printf '| %-25s | %-10s | %20s |\n' "$d" "-$grade" "$speedtxt" +done diff --git a/scripts/vivado/tabtest.sh b/scripts/vivado/tabtest.sh new file mode 100644 index 0000000..bc3d840 --- /dev/null +++ b/scripts/vivado/tabtest.sh @@ -0,0 +1,103 @@ +#!/bin/bash + +set -e +read _ ip dev grade _ < <( echo $* | tr '_/' ' '; ) + +# rm -rf tab_${ip}_${dev}_${grade} +mkdir -p tab_${ip}_${dev}_${grade} +cd tab_${ip}_${dev}_${grade} + +best_speed=99 +speed=20 +step=16 + +synth_case() { + if [ -f test_${1}.txt ]; then + echo "Reusing cached tab_${ip}_${dev}_${grade}/test_${1}." + return + fi + + case "${dev}" in + xc7k) xl_device="xc7k70t-fbg676-${grade}" ;; + xc7v) xl_device="xc7v585t-ffg1761-${grade}" ;; + xcku) xl_device="xcku035-fbva676-${grade}-e" ;; + xcvu) xl_device="xcvu065-ffvc1517-${grade}-e" ;; + xckup) xl_device="xcku3p-ffva676-${grade}-e" ;; + xcvup) xl_device="xcvu3p-ffvc1517-${grade}-e" ;; + esac + + cat > test_${1}.tcl <<- EOT + read_verilog ../tabtest.v + read_verilog ../../../picorv32.v + read_xdc test_${1}.xdc + synth_design -flatten_hierarchy full -part ${xl_device} -top top + opt_design -sweep -remap -propconst + opt_design -directive Explore + place_design -directive Explore + phys_opt_design -retime -rewire -critical_pin_opt -placement_opt -critical_cell_opt + route_design -directive Explore + place_design -post_place_opt + phys_opt_design -retime + route_design -directive NoTimingRelaxation + report_utilization + report_timing + EOT + + cat > test_${1}.xdc <<- EOT + create_clock -period ${speed%?}.${speed#?} [get_ports clk] + EOT + + echo "Running tab_${ip}_${dev}_${grade}/test_${1}.." + if ! $VIVADO -nojournal -log test_${1}.log -mode batch -source test_${1}.tcl > /dev/null 2>&1; then + cat test_${1}.log + exit 1 + fi + mv test_${1}.log test_${1}.txt +} + +got_violated=false +got_met=false + +countdown=2 +while [ $countdown -gt 0 ]; do + synth_case $speed + + if grep -q '^Slack.*(VIOLATED)' test_${speed}.txt; then + echo " tab_${ip}_${dev}_${grade}/test_${speed} VIOLATED" + step=$((step / 2)) + speed=$((speed + step)) + got_violated=true + elif grep -q '^Slack.*(MET)' test_${speed}.txt; then + echo " tab_${ip}_${dev}_${grade}/test_${speed} MET" + [ $speed -lt $best_speed ] && best_speed=$speed + step=$((step / 2)) + speed=$((speed - step)) + got_met=true + else + echo "ERROR: No slack line found in $PWD/test_${speed}.txt!" + exit 1 + fi + + if [ $step -eq 0 ]; then + countdown=$((countdown - 1)) + speed=$((best_speed - 2)) + step=1 + fi +done + +if ! $got_violated; then + echo "ERROR: No timing violated in $PWD!" + exit 1 +fi + +if ! $got_met; then + echo "ERROR: No timing met in $PWD!" + exit 1 +fi + + +echo "-----------------------" +echo "Best speed for tab_${ip}_${dev}_${grade}: $best_speed" +echo "-----------------------" +echo $best_speed > results.txt + diff --git a/scripts/vivado/tabtest.v b/scripts/vivado/tabtest.v new file mode 100644 index 0000000..cdf2057 --- /dev/null +++ b/scripts/vivado/tabtest.v @@ -0,0 +1,118 @@ + +module top ( + input clk, io_resetn, + output io_trap, + + output io_mem_axi_awvalid, + input io_mem_axi_awready, + output [31:0] io_mem_axi_awaddr, + output [ 2:0] io_mem_axi_awprot, + + output io_mem_axi_wvalid, + input io_mem_axi_wready, + output [31:0] io_mem_axi_wdata, + output [ 3:0] io_mem_axi_wstrb, + + input io_mem_axi_bvalid, + output io_mem_axi_bready, + + output io_mem_axi_arvalid, + input io_mem_axi_arready, + output [31:0] io_mem_axi_araddr, + output [ 2:0] io_mem_axi_arprot, + + input io_mem_axi_rvalid, + output io_mem_axi_rready, + input [31:0] io_mem_axi_rdata, + + input [31:0] io_irq, + output [31:0] io_eoi +); + wire resetn; + wire trap; + wire mem_axi_awvalid; + wire mem_axi_awready; + wire [31:0] mem_axi_awaddr; + wire [2:0] mem_axi_awprot; + wire mem_axi_wvalid; + wire mem_axi_wready; + wire [31:0] mem_axi_wdata; + wire [3:0] mem_axi_wstrb; + wire mem_axi_bvalid; + wire mem_axi_bready; + wire mem_axi_arvalid; + wire mem_axi_arready; + wire [31:0] mem_axi_araddr; + wire [2:0] mem_axi_arprot; + wire mem_axi_rvalid; + wire mem_axi_rready; + wire [31:0] mem_axi_rdata; + wire [31:0] irq; + wire [31:0] eoi; + + delay4 #( 1) delay_resetn (clk, io_resetn , resetn ); + delay4 #( 1) delay_trap (clk, trap , io_trap ); + delay4 #( 1) delay_mem_axi_awvalid (clk, mem_axi_awvalid, io_mem_axi_awvalid); + delay4 #( 1) delay_mem_axi_awready (clk, io_mem_axi_awready, mem_axi_awready); + delay4 #(32) delay_mem_axi_awaddr (clk, mem_axi_awaddr , io_mem_axi_awaddr ); + delay4 #( 3) delay_mem_axi_awprot (clk, mem_axi_awprot , io_mem_axi_awprot ); + delay4 #( 1) delay_mem_axi_wvalid (clk, mem_axi_wvalid , io_mem_axi_wvalid ); + delay4 #( 1) delay_mem_axi_wready (clk, io_mem_axi_wready , mem_axi_wready ); + delay4 #(32) delay_mem_axi_wdata (clk, mem_axi_wdata , io_mem_axi_wdata ); + delay4 #( 4) delay_mem_axi_wstrb (clk, mem_axi_wstrb , io_mem_axi_wstrb ); + delay4 #( 1) delay_mem_axi_bvalid (clk, io_mem_axi_bvalid , mem_axi_bvalid ); + delay4 #( 1) delay_mem_axi_bready (clk, mem_axi_bready , io_mem_axi_bready ); + delay4 #( 1) delay_mem_axi_arvalid (clk, mem_axi_arvalid, io_mem_axi_arvalid); + delay4 #( 1) delay_mem_axi_arready (clk, io_mem_axi_arready, mem_axi_arready); + delay4 #(32) delay_mem_axi_araddr (clk, mem_axi_araddr , io_mem_axi_araddr ); + delay4 #( 3) delay_mem_axi_arprot (clk, mem_axi_arprot , io_mem_axi_arprot ); + delay4 #( 1) delay_mem_axi_rvalid (clk, io_mem_axi_rvalid , mem_axi_rvalid ); + delay4 #( 1) delay_mem_axi_rready (clk, mem_axi_rready , io_mem_axi_rready ); + delay4 #(32) delay_mem_axi_rdata (clk, io_mem_axi_rdata , mem_axi_rdata ); + delay4 #(32) delay_irq (clk, io_irq , irq ); + delay4 #(32) delay_eoi (clk, eoi , io_eoi ); + + picorv32_axi #( + .TWO_CYCLE_ALU(1) + ) cpu ( + .clk (clk ), + .resetn (resetn ), + .trap (trap ), + .mem_axi_awvalid(mem_axi_awvalid), + .mem_axi_awready(mem_axi_awready), + .mem_axi_awaddr (mem_axi_awaddr ), + .mem_axi_awprot (mem_axi_awprot ), + .mem_axi_wvalid (mem_axi_wvalid ), + .mem_axi_wready (mem_axi_wready ), + .mem_axi_wdata (mem_axi_wdata ), + .mem_axi_wstrb (mem_axi_wstrb ), + .mem_axi_bvalid (mem_axi_bvalid ), + .mem_axi_bready (mem_axi_bready ), + .mem_axi_arvalid(mem_axi_arvalid), + .mem_axi_arready(mem_axi_arready), + .mem_axi_araddr (mem_axi_araddr ), + .mem_axi_arprot (mem_axi_arprot ), + .mem_axi_rvalid (mem_axi_rvalid ), + .mem_axi_rready (mem_axi_rready ), + .mem_axi_rdata (mem_axi_rdata ), + .irq (irq ), + .eoi (eoi ) + ); +endmodule + +module delay4 #( + parameter WIDTH = 1 +) ( + input clk, + input [WIDTH-1:0] in, + output reg [WIDTH-1:0] out +); + reg [WIDTH-1:0] q1, q2, q3; + always @(posedge clk) begin + q1 <= in; + q2 <= q1; + q3 <= q2; + out <= q3; + end +endmodule + diff --git a/scripts/yosys-cmp/README.md b/scripts/yosys-cmp/README.md new file mode 100644 index 0000000..acb2c6c --- /dev/null +++ b/scripts/yosys-cmp/README.md @@ -0,0 +1,62 @@ + +Synthesis results for the PicoRV32 core (in its default configuration) with Yosys 0.5+383 (git sha1 8648089), Synplify Pro and Lattice LSE from iCEcube2.2014.08, and Xilinx Vivado 2015.3. + +No timing constraints were used for synthesis; only resource utilisation is compared. + +Last updated: 2015-10-30 + + +Results for iCE40 Synthesis +--------------------------- + +| Cell | Yosys | Synplify Pro | Lattice LSE | +|:--------------|------:|-------------:|------------:| +| `SB_CARRY` | 405 | 349 | 309 | +| `SB_DFF` | 125 | 256 | 114 | +| `SB_DFFE` | 251 | 268 | 76 | +| `SB_DFFESR` | 172 | 39 | 147 | +| `SB_DFFESS` | 1 | 0 | 69 | +| `SB_DFFSR` | 69 | 137 | 134 | +| `SB_DFFSS` | 0 | 0 | 36 | +| `SB_LUT4` | 1795 | 1657 | 1621 | +| `SB_RAM40_4K` | 4 | 4 | 4 | + +Summary: + +| Cell | Yosys | Synplify Pro | Lattice LSE | +|:--------------|------:|-------------:|------------:| +| `SB_CARRY` | 405 | 349 | 309 | +| `SB_DFF*` | 618 | 700 | 576 | +| `SB_LUT4` | 1795 | 1657 | 1621 | +| `SB_RAM40_4K` | 4 | 4 | 4 | + + +Results for Xilinx 7-Series Synthesis +------------------------------------- + +| Cell | Yosys | Vivado | +|:------------|------:|-------:| +| `FDRE` | 671 | 553 | +| `FDSE` | 0 | 21 | +| `LUT1` | 41 | 160 | +| `LUT2` | 517 | 122 | +| `LUT3` | 77 | 120 | +| `LUT4` | 136 | 204 | +| `LUT5` | 142 | 135 | +| `LUT6` | 490 | 405 | +| `MUXF7` | 54 | 0 | +| `MUXF8` | 15 | 0 | +| `MUXCY` | 420 | 0 | +| `XORCY` | 359 | 0 | +| `CARRY4` | 0 | 83 | +| `RAMD32` | 0 | 72 | +| `RAMS32` | 0 | 24 | +| `RAM64X1D` | 64 | 0 | + +Summary: + +| Cell | Yosys | Vivado | +|:------------|------:|-------:| +| `FD*` | 671 | 574 | +| `LUT*` | 1403 | 1146 | + diff --git a/scripts/yosys-cmp/lse.sh b/scripts/yosys-cmp/lse.sh new file mode 100644 index 0000000..a802c67 --- /dev/null +++ b/scripts/yosys-cmp/lse.sh @@ -0,0 +1,53 @@ +#!/bin/bash + +set -ex + +rm -rf lse.tmp +mkdir lse.tmp +cd lse.tmp + +cat > lse.prj << EOT +#device +-a SBTiCE40 +-d iCE40HX8K +-t CT256 +#constraint file + +#options +-frequency 200 +-optimization_goal Area +-twr_paths 3 +-bram_utilization 100.00 +-ramstyle Auto +-romstyle Auto +-use_carry_chain 1 +-carry_chain_length 0 +-resource_sharing 1 +-propagate_constants 1 +-remove_duplicate_regs 1 +-max_fanout 10000 +-fsm_encoding_style Auto +-use_io_insertion 1 +-use_io_reg auto +-ifd +-resolve_mixed_drivers 0 +-RWCheckOnRam 0 +-fix_gated_clocks 1 +-top picorv32 + +-ver "../../../picorv32.v" +-p "." + +#set result format/file last +-output_edif output.edf + +#set log file +-logfile "lse.log" +EOT + +icecubedir="${ICECUBEDIR:-/opt/lscc/iCEcube2.2014.08}" +export FOUNDRY="$icecubedir/LSE" +export LD_LIBRARY_PATH="$LD_LIBRARY_PATH${LD_LIBRARY_PATH:+:}$icecubedir/LSE/bin/lin" +"$icecubedir"/LSE/bin/lin/synthesis -f lse.prj + +grep 'viewRef.*cellRef' output.edf | sed 's,.*cellRef *,,; s,[ )].*,,;' | sort | uniq -c diff --git a/scripts/yosys-cmp/synplify.sh b/scripts/yosys-cmp/synplify.sh new file mode 100644 index 0000000..d0a2a08 --- /dev/null +++ b/scripts/yosys-cmp/synplify.sh @@ -0,0 +1,74 @@ +#!/bin/bash + +set -ex + +rm -rf synplify.tmp +mkdir synplify.tmp +cd synplify.tmp + +cat > impl_syn.prj << EOT +add_file -verilog -lib work ../../../picorv32.v +impl -add impl -type fpga + +# implementation attributes +set_option -vlog_std v2001 +set_option -project_relative_includes 1 + +# device options +set_option -technology SBTiCE40 +set_option -part iCE40HX8K +set_option -package CT256 +set_option -speed_grade +set_option -part_companion "" + +# compilation/mapping options +set_option -top_module "picorv32" + +# mapper_options +set_option -frequency auto +set_option -write_verilog 0 +set_option -write_vhdl 0 + +# Silicon Blue iCE40 +set_option -maxfan 10000 +set_option -disable_io_insertion 0 +set_option -pipe 1 +set_option -retiming 0 +set_option -update_models_cp 0 +set_option -fixgatedclocks 2 +set_option -fixgeneratedclocks 0 + +# NFilter +set_option -popfeed 0 +set_option -constprop 0 +set_option -createhierarchy 0 + +# sequential_optimization_options +set_option -symbolic_fsm_compiler 1 + +# Compiler Options +set_option -compiler_compatible 0 +set_option -resource_sharing 1 + +# automatic place and route (vendor) options +set_option -write_apr_constraint 1 + +# set result format/file last +project -result_format edif +project -result_file impl.edf +impl -active impl +project -run synthesis -clean +EOT + +icecubedir="${ICECUBEDIR:-/opt/lscc/iCEcube2.2014.08}" +export SBT_DIR="$icecubedir/sbt_backend" +export SYNPLIFY_PATH="$icecubedir/synpbase" +export LM_LICENSE_FILE="$icecubedir/license.dat" +export TCL_LIBRARY="$icecubedir/sbt_backend/bin/linux/lib/tcl8.4" +export LD_LIBRARY_PATH="$LD_LIBRARY_PATH${LD_LIBRARY_PATH:+:}$icecubedir/sbt_backend/bin/linux/opt" +export LD_LIBRARY_PATH="$LD_LIBRARY_PATH${LD_LIBRARY_PATH:+:}$icecubedir/sbt_backend/bin/linux/opt/synpwrap" +export LD_LIBRARY_PATH="$LD_LIBRARY_PATH${LD_LIBRARY_PATH:+:}$icecubedir/sbt_backend/lib/linux/opt" +export LD_LIBRARY_PATH="$LD_LIBRARY_PATH${LD_LIBRARY_PATH:+:}$icecubedir/LSE/bin/lin" +"$icecubedir"/sbt_backend/bin/linux/opt/synpwrap/synpwrap -prj impl_syn.prj -log impl.srr + +grep 'instance.*cellRef' impl/impl.edf | sed 's,.*cellRef *,,; s,[ )].*,,;' | sort | uniq -c diff --git a/scripts/yosys-cmp/vivado.tcl b/scripts/yosys-cmp/vivado.tcl new file mode 100644 index 0000000..560b880 --- /dev/null +++ b/scripts/yosys-cmp/vivado.tcl @@ -0,0 +1,3 @@ +read_verilog ../../picorv32.v +synth_design -part xc7k70t-fbg676 -top picorv32 +report_utilization diff --git a/scripts/yosys-cmp/yosys_ice40.ys b/scripts/yosys-cmp/yosys_ice40.ys new file mode 100644 index 0000000..b14b338 --- /dev/null +++ b/scripts/yosys-cmp/yosys_ice40.ys @@ -0,0 +1,2 @@ +read_verilog ../../picorv32.v +synth_ice40 -top picorv32 diff --git a/scripts/yosys-cmp/yosys_xilinx.ys b/scripts/yosys-cmp/yosys_xilinx.ys new file mode 100644 index 0000000..ead52a4 --- /dev/null +++ b/scripts/yosys-cmp/yosys_xilinx.ys @@ -0,0 +1,2 @@ +read_verilog ../../picorv32.v +synth_xilinx -top picorv32 diff --git a/scripts/yosys/.gitignore b/scripts/yosys/.gitignore new file mode 100644 index 0000000..d6fc3e3 --- /dev/null +++ b/scripts/yosys/.gitignore @@ -0,0 +1 @@ +osu018_stdcells.lib diff --git a/scripts/yosys/synth_gates.lib b/scripts/yosys/synth_gates.lib new file mode 100644 index 0000000..be706dd --- /dev/null +++ b/scripts/yosys/synth_gates.lib @@ -0,0 +1,38 @@ +library(gates) { + cell(NOT) { + area: 2; // 7404 hex inverter + pin(A) { direction: input; } + pin(Y) { direction: output; + function: "A'"; } + } + cell(BUF) { + area: 4; // 2x 7404 hex inverter + pin(A) { direction: input; } + pin(Y) { direction: output; + function: "A"; } + } + cell(NAND) { + area: 3; // 7400 quad 2-input NAND gate + pin(A) { direction: input; } + pin(B) { direction: input; } + pin(Y) { direction: output; + function: "(A*B)'"; } + } + cell(NOR) { + area: 3; // 7402 quad 2-input NOR gate + pin(A) { direction: input; } + pin(B) { direction: input; } + pin(Y) { direction: output; + function: "(A+B)'"; } + } + cell(DFF) { + area: 6; // 7474 dual D positive edge triggered flip-flop + ff(IQ, IQN) { clocked_on: C; + next_state: D; } + pin(C) { direction: input; + clock: true; } + pin(D) { direction: input; } + pin(Q) { direction: output; + function: "IQ"; } + } +} diff --git a/scripts/yosys/synth_gates.v b/scripts/yosys/synth_gates.v new file mode 100644 index 0000000..8e2504e --- /dev/null +++ b/scripts/yosys/synth_gates.v @@ -0,0 +1,30 @@ +module top ( + input clk, resetn, + + output mem_valid, + output mem_instr, + input mem_ready, + + output [31:0] mem_addr, + output [31:0] mem_wdata, + output [ 3:0] mem_wstrb, + input [31:0] mem_rdata +); + picorv32 #( + .ENABLE_COUNTERS(0), + .LATCHED_MEM_RDATA(1), + .TWO_STAGE_SHIFT(0), + .CATCH_MISALIGN(0), + .CATCH_ILLINSN(0) + ) picorv32 ( + .clk (clk ), + .resetn (resetn ), + .mem_valid(mem_valid), + .mem_instr(mem_instr), + .mem_ready(mem_ready), + .mem_addr (mem_addr ), + .mem_wdata(mem_wdata), + .mem_wstrb(mem_wstrb), + .mem_rdata(mem_rdata) + ); +endmodule diff --git a/scripts/yosys/synth_gates.ys b/scripts/yosys/synth_gates.ys new file mode 100644 index 0000000..311d767 --- /dev/null +++ b/scripts/yosys/synth_gates.ys @@ -0,0 +1,14 @@ +read_verilog synth_gates.v +read_verilog ../../picorv32.v + +hierarchy -top top +proc; flatten + +synth + +dfflibmap -prepare -liberty synth_gates.lib +abc -dff -liberty synth_gates.lib +dfflibmap -liberty synth_gates.lib + +stat +write_blif synth_gates.blif diff --git a/scripts/yosys/synth_osu018.sh b/scripts/yosys/synth_osu018.sh new file mode 100644 index 0000000..7a8693d --- /dev/null +++ b/scripts/yosys/synth_osu018.sh @@ -0,0 +1,8 @@ +#!/bin/bash +set -ex +if test ! -s osu018_stdcells.lib; then + wget --continue -O osu018_stdcells.lib.part http://vlsiarch.ecen.okstate.edu/flows/MOSIS_SCMOS/` + `latest/cadence/lib/tsmc018/signalstorm/osu018_stdcells.lib + mv osu018_stdcells.lib.part osu018_stdcells.lib +fi +yosys -p 'synth -top picorv32; dfflibmap -liberty osu018_stdcells.lib; abc -liberty osu018_stdcells.lib; stat' ../../picorv32.v diff --git a/scripts/yosys/synth_sim.ys b/scripts/yosys/synth_sim.ys new file mode 100644 index 0000000..ded89d9 --- /dev/null +++ b/scripts/yosys/synth_sim.ys @@ -0,0 +1,8 @@ +# yosys synthesis script for post-synthesis simulation (make test_synth) + +read_verilog picorv32.v +chparam -set COMPRESSED_ISA 1 -set ENABLE_MUL 1 -set ENABLE_DIV 1 \ + -set ENABLE_IRQ 1 -set ENABLE_TRACE 1 picorv32_axi +hierarchy -top picorv32_axi +synth +write_verilog synth.v |