From b986265a14e5419d1074b03a1822ec2a6f39971c Mon Sep 17 00:00:00 2001 From: Steve Jenson Date: Tue, 29 Oct 2024 18:48:09 -0700 Subject: [PATCH] Dockerfile updates for latest iverilog --- .devcontainer/Dockerfile | 12 ++++++++++-- src/byte_transmitter.v | 21 +++++++++++++-------- test/test.py | 3 +-- 3 files changed, 24 insertions(+), 12 deletions(-) diff --git a/.devcontainer/Dockerfile b/.devcontainer/Dockerfile index 7de255b..34f223f 100644 --- a/.devcontainer/Dockerfile +++ b/.devcontainer/Dockerfile @@ -5,13 +5,21 @@ ENV DEBIAN_FRONTEND=noninteractive ENV PDK_ROOT=/home/vscode/ttsetup/pdk ENV PDK=sky130A -RUN apt update -RUN apt install -y iverilog python3 python3-pip python3-venv python3-tk python-is-python3 libcairo2 verilator libpng-dev libqhull-dev +RUN apt update && apt-get install build-essential -y && apt install -y autoconf gperf make gcc g++ bison flex +RUN apt install -y python3 python3-pip python3-venv python3-tk python-is-python3 libcairo2 verilator libpng-dev libqhull-dev wget # Clone tt-support-tools RUN mkdir -p /ttsetup RUN git clone -b tt09 https://github.com/TinyTapeout/tt-support-tools /ttsetup/tt-support-tools +# (stevej) Install bespoke iverilog +RUN wget https://github.com/htfab/iverilog/archive/refs/tags/13.0-git-d8c3c51.tar.gz +RUN tar zxf 13.0-git-d8c3c51.tar.gz && cd /iverilog-13.0-git-d8c3c51 && \ + sh autoconf.sh && ./configure && make && make install + +#RUN wget https://github.com/htfab/iverilog/releases/download/13.0-git-d8c3c51/iverilog_13.0-git-d8c3c51a-1_amd64.deb +#RUN apt-get install -y -q --no-install-recommends ./iverilog_13.0-git-d8c3c51a-1_amd64.deb + COPY test/requirements.txt /ttsetup/test_requirements.txt COPY .devcontainer/copy_tt_support_tools.sh /ttsetup diff --git a/src/byte_transmitter.v b/src/byte_transmitter.v index c04ea39..4c3f437 100644 --- a/src/byte_transmitter.v +++ b/src/byte_transmitter.v @@ -16,7 +16,9 @@ module byte_transmitter ( output wire done ); - reg [31:0] f_total_read; +`ifdef FORMAL + reg [5:0] f_total_written; +`endif reg [5:0] byte_count; reg r_out; assign out = r_out; @@ -28,15 +30,17 @@ module byte_transmitter ( byte_count <= 6'h20; r_done <= 0; r_out <= 0; - f_total_read <= 0; +`ifdef FORMAL + f_total_written <= 0; +`endif end else begin if (enable) begin if (byte_count > 0) begin - f_total_read <= f_total_read + 1; +`ifdef FORMAL + f_total_written <= f_total_written + 1; + assert(r_out != 1'bX); +`endif r_out <= in[byte_count - 1]; - `ifdef FORMAL - assert(r_out != 1'bX); - `endif byte_count <= byte_count - 1; end else begin byte_count <= 6'h20; @@ -59,13 +63,14 @@ module byte_transmitter ( assume(reset); if (f_past_valid && enable && done) begin - assert(f_total_read == 32); // We've drained the entire thing. + assert(f_total_written == 32); // We've drained the entire buffer. assert(byte_count == 0); - assert(r_out != 1'bX); // Learned from the paper: 'Being More Assertive with Your X' + assert(r_out != 1'bX); end if (f_past_valid && enable && byte_count == 0) begin assert(done); + assert(f_total_written == 32); end end diff --git a/test/test.py b/test/test.py index 077bfe5..1116265 100644 --- a/test/test.py +++ b/test/test.py @@ -118,8 +118,7 @@ async def test_idcode(dut): await ClockCycles(dut.clk, 1) dut.ui_in.value = 0b0000_1000 await ClockCycles(dut.clk, 1) - tdo = dut.uo_out.value[0] - print(tdo) + tdo = dut.uo_out.value[7] given_idcode = (given_idcode << 1) + int(tdo) assert given_idcode == expected_idcode