diff --git a/monitor/tests/wishbone/reqwalker.vcd b/monitor/tests/wishbone/reqwalker.vcd new file mode 100644 index 00000000..f01a5a96 --- /dev/null +++ b/monitor/tests/wishbone/reqwalker.vcd @@ -0,0 +1,419 @@ +$version Generated by VerilatedVcd $end +$timescale 1ps $end + $scope module TOP $end + $var wire 1 # i_clk $end + $var wire 1 $ i_cyc $end + $var wire 1 % i_stb $end + $var wire 1 & i_we $end + $var wire 1 ' i_addr $end + $var wire 32 ( i_data [31:0] $end + $var wire 1 ) o_stall $end + $var wire 1 * o_ack $end + $var wire 32 + o_data [31:0] $end + $var wire 6 , o_led [5:0] $end + $scope module reqwalker $end + $var wire 1 # i_clk $end + $var wire 1 $ i_cyc $end + $var wire 1 % i_stb $end + $var wire 1 & i_we $end + $var wire 1 ' i_addr $end + $var wire 32 ( i_data [31:0] $end + $var wire 1 ) o_stall $end + $var wire 1 * o_ack $end + $var wire 32 + o_data [31:0] $end + $var wire 6 , o_led [5:0] $end + $var wire 1 - busy $end + $var wire 4 . state [3:0] $end + $var wire 34 / unused [33:0] $end + $upscope $end + $upscope $end +$enddefinitions $end + + +#8 +0# +1$ +1% +0& +0' +b00000000000000000000000000000000 ( +0) +0* +b00000000000000000000000000000000 + +b000000 , +0- +b0000 . +b1000000000000000000000000000000000 / +#10 +1# +1* +#15 +0# +#18 +0$ +0% +b0000000000000000000000000000000000 / +#20 +1# +0* +#25 +0# +#30 +1# +#35 +0# +#40 +1# +#45 +0# +#50 +1# +#55 +0# +#60 +1# +#65 +0# +#68 +1$ +1% +1& +b1000000000000000000000000000000000 / +#70 +1# +1) +1* +b00000000000000000000000000000001 + +1- +b0001 . +#75 +0# +#78 +0$ +0% +b0000000000000000000000000000000000 / +#80 +1# +0* +b00000000000000000000000000000010 + +b000001 , +b0010 . +#85 +0# +#88 +1$ +1% +0& +0) +b1000000000000000000000000000000000 / +#90 +1# +1* +b00000000000000000000000000000011 + +b000010 , +b0011 . +#95 +0# +#98 +0$ +0% +b0000000000000000000000000000000000 / +#100 +1# +0* +b00000000000000000000000000000100 + +b000100 , +b0100 . +#105 +0# +#108 +1$ +1% +b1000000000000000000000000000000000 / +#110 +1# +1* +b00000000000000000000000000000101 + +b001000 , +b0101 . +#115 +0# +#118 +0$ +0% +b0000000000000000000000000000000000 / +#120 +1# +0* +b00000000000000000000000000000110 + +b010000 , +b0110 . +#125 +0# +#128 +1$ +1% +b1000000000000000000000000000000000 / +#130 +1# +1* +b00000000000000000000000000000111 + +b100000 , +b0111 . +#135 +0# +#138 +0$ +0% +b0000000000000000000000000000000000 / +#140 +1# +0* +b00000000000000000000000000001000 + +b010000 , +b1000 . +#145 +0# +#148 +1$ +1% +b1000000000000000000000000000000000 / +#150 +1# +1* +b00000000000000000000000000001001 + +b001000 , +b1001 . +#155 +0# +#158 +0$ +0% +b0000000000000000000000000000000000 / +#160 +1# +0* +b00000000000000000000000000001010 + +b000100 , +b1010 . +#165 +0# +#168 +1$ +1% +b1000000000000000000000000000000000 / +#170 +1# +1* +b00000000000000000000000000001011 + +b000010 , +b1011 . +#175 +0# +#178 +0$ +0% +b0000000000000000000000000000000000 / +#180 +1# +0* +b00000000000000000000000000000000 + +b000001 , +0- +b0000 . +#185 +0# +#188 +1$ +1% +b1000000000000000000000000000000000 / +#190 +1# +1* +b000000 , +#195 +0# +#198 +0$ +0% +b0000000000000000000000000000000000 / +#200 +1# +0* +#205 +0# +#210 +1# +#215 +0# +#220 +1# +#225 +0# +#230 +1# +#235 +0# +#240 +1# +#245 +0# +#248 +1$ +1% +1& +b1000000000000000000000000000000000 / +#250 +1# +1) +1* +b00000000000000000000000000000001 + +1- +b0001 . +#255 +0# +#258 +0$ +0% +b0000000000000000000000000000000000 / +#260 +1# +0* +b00000000000000000000000000000010 + +b000001 , +b0010 . +#265 +0# +#268 +1$ +1% +0& +0) +b1000000000000000000000000000000000 / +#270 +1# +1* +b00000000000000000000000000000011 + +b000010 , +b0011 . +#275 +0# +#278 +0$ +0% +b0000000000000000000000000000000000 / +#280 +1# +0* +b00000000000000000000000000000100 + +b000100 , +b0100 . +#285 +0# +#288 +1$ +1% +b1000000000000000000000000000000000 / +#290 +1# +1* +b00000000000000000000000000000101 + +b001000 , +b0101 . +#295 +0# +#298 +0$ +0% +b0000000000000000000000000000000000 / +#300 +1# +0* +b00000000000000000000000000000110 + +b010000 , +b0110 . +#305 +0# +#308 +1$ +1% +b1000000000000000000000000000000000 / +#310 +1# +1* +b00000000000000000000000000000111 + +b100000 , +b0111 . +#315 +0# +#318 +0$ +0% +b0000000000000000000000000000000000 / +#320 +1# +0* +b00000000000000000000000000001000 + +b010000 , +b1000 . +#325 +0# +#328 +1$ +1% +b1000000000000000000000000000000000 / +#330 +1# +1* +b00000000000000000000000000001001 + +b001000 , +b1001 . +#335 +0# +#338 +0$ +0% +b0000000000000000000000000000000000 / +#340 +1# +0* +b00000000000000000000000000001010 + +b000100 , +b1010 . +#345 +0# +#348 +1$ +1% +b1000000000000000000000000000000000 / +#350 +1# +1* +b00000000000000000000000000001011 + +b000010 , +b1011 . +#355 +0# +#358 +0$ +0% +b0000000000000000000000000000000000 / +#360 +1# +0* +b00000000000000000000000000000000 + +b000001 , +0- +b0000 . +#365 +0# +#368 +1$ +1% +b1000000000000000000000000000000000 / +#370 +1# +1* +b000000 , +#375 +0# diff --git a/monitor/tests/wishbone/wishbone.out b/monitor/tests/wishbone/wishbone.out new file mode 100644 index 00000000..e69de29b diff --git a/monitor/tests/wishbone/wishbone.prot b/monitor/tests/wishbone/wishbone.prot new file mode 100644 index 00000000..bc7b1f2e --- /dev/null +++ b/monitor/tests/wishbone/wishbone.prot @@ -0,0 +1,144 @@ +// ARGS: --wave wishbone/reqwalker.vcd --instances TOP.reqwalker:WBSubordinate --sample-posedge TOP.reqwalker.i_clk + +// Wishbone B4 (Pipeline mode) subordinate + +// TODO: run the monitor on some existing waveforms +// Eventually put all the traces in a separate repo + +// For Wishbone, you can model everything using the same interface, +// whereas for AXI we can't do this (because responses can be out of order in AXI <---- is this true?) + +// See if there is already a thing which takes Wishbone inputs/outputs and outputs transaction trace +// ^^ such a thing might already exist and is hard-coded +// TODO: see https://github.com/wallento/cocotbext-wishbone for a possible monitor + +struct WBSubordinate { + // Cycle is high anytime an active pipeline session is occurring + in i_cyc: u1, + + // Strobe is high when there is a request to the subordinate + // (akin to Valid in AXI-Lite, i.e. they indicate the manager + // has something to transfer) + in i_stb: u1, + + // Write-enable (true for write-requests) + in i_we: u1, + + // Address of the request + in i_addr: u1, + + // Data to be written + in i_data: u32, + + // Response from the subordinate, indicating that the request + // has been fulfilled. + out o_ack: u1, + + // True on any cycle when the subordinate can't accept requests + // False when a request can be accepted + // (i.e. the opposite of Ready in AXI-Lite) + out o_stall: u1, + + // Data returned by the subordinate to the manager + // This is valid only when ACK is true + out o_data: u32, + + // LED output: one-hot encoding of the current walker state + out o_led: u6 +} + +// Both cyc & stb are low when the subordinate is low, +// everything else is DontCare +#[idle] +prot idle() { + DUT.i_cyc := 1'b0; + DUT.i_stb := 1'b0; + DUT.i_we := X; + DUT.i_addr := X; + DUT.i_data := X; + step(); +} + +// Writes a `data` value to the subordinate, and observes the +// resultant `led` state via an output parameter. +// Wishbone says to hold all request signals while stalled (stall=1), +// i.e. when the subordinate is busy processing a previous request. +prot write(in addr: u1, in data: u32, out led: u6) { + DUT.i_cyc := 1'b1; + DUT.i_stb := 1'b1; + DUT.i_we := 1'b1; + DUT.i_addr := addr; + DUT.i_data := data; + // For reqwalker, stall is combinational: o_stall = busy && i_we. + // When state=0 (idle, can accept), busy=0 so stall=0 before the accept posedge. + // Stall=1 only appears AT the accept posedge (state 0->1), so the loop + // is omitted here; the monitor samples posedge values where stall=1 already + // coincides with ack=1 (post-accept artifact). + // Request accepted on this cycle; ack registered next cycle + step(); + // i_stb goes to DontCare after acceptance: per Wishbone B4 the master may + // keep stb high for pipelined requests, and in VCDs the 0 only appears at + // the *next* posedge (testbench sets it after tick() returns). + DUT.i_cyc := X; + DUT.i_stb := X; + DUT.i_we := X; + DUT.i_addr := X; + DUT.i_data := X; + + // Based on the Verilog, there is a 1 cycle latency before the + // ack is registered. + while (DUT.o_ack == 1'b0) { + step(); + } + + // Ack is now 1, the data write is complete + // Note: During the ACK phase, we have i_cyc=1 (session still active) + // and i_stb=0 (no new request). + + // Observe resultant LED state + assert_eq(DUT.o_led, led); + + // Set to DontCare so the next protocol can decide whether to continue. + // No explicit fork(): using implicit fork so the next transaction starts + // at the *next* cycle (after i_cyc drops to 0 and the bus becomes idle). + DUT.i_stb := X; + DUT.i_cyc := X; + step(); +} + +// Reads a value and the LED state from the subordinate +// (the `data` and the `led` state are conveyed via output parameters) +prot read(in addr: u1, out data: u32, out led: u6) { + DUT.i_cyc := 1'b1; + DUT.i_stb := 1'b1; + DUT.i_we := 1'b0; + DUT.i_addr := addr; + DUT.i_data := X; + + // Wait while the subordinate stalls + while (DUT.o_stall == 1'b1) { + step(); + } + // Read request accepted, one cycle for data transfer. + // i_stb goes to DontCare after acceptance (same reasoning as write above). + step(); + DUT.i_stb := X; + DUT.i_we := X; + DUT.i_addr := X; + + // Wait for ack; data is valid to read when ack becomes 1 + while (DUT.o_ack == 1'b0) { + step(); + } + + // Observe resultant data value & LED state + assert_eq(DUT.o_data, data); + assert_eq(DUT.o_led, led); + + // Set to DontCare so the next protocol can decide whether to continue. + // No explicit fork(): using implicit fork so the next transaction starts + // at the *next* cycle (after i_cyc drops to 0 and the bus becomes idle). + DUT.i_stb := X; + DUT.i_cyc := X; + step(); +} diff --git a/protocols/tests/wishbone/.gitignore b/protocols/tests/wishbone/.gitignore new file mode 100644 index 00000000..aab72d1f --- /dev/null +++ b/protocols/tests/wishbone/.gitignore @@ -0,0 +1,3 @@ +obj_dir/* +reqwalker_tb +*.vcd diff --git a/protocols/tests/wishbone/Makefile b/protocols/tests/wishbone/Makefile new file mode 100644 index 00000000..ed5edc0c --- /dev/null +++ b/protocols/tests/wishbone/Makefile @@ -0,0 +1,53 @@ +################################################################################ +## +## Filename: Makefile +## +## Project: Verilog Tutorial Example file +## +## Purpose: Builds the Verilator request-walker bus slave example +## +## Targets: +## +## The (default) or all target will build a verilator simulation for the +## Request Walker. +## +## clean Removes all build products +## +## Creator: Dan Gisselquist, Ph.D. +## Gisselquist Technology, LLC +## +################################################################################ +## +## Written and distributed by Gisselquist Technology, LLC +## +## This program is hereby granted to the public domain. +## +## This program is distributed in the hope that it will be useful, but WITHOUT +## ANY WARRANTY; without even the implied warranty of MERCHANTIBILITY or +## FITNESS FOR A PARTICULAR PURPOSE. +## +################################################################################ +## +## +.PHONY: all +all: reqwalker_tb + +VERILATOR=verilator +VERILATOR_ROOT ?= $(shell bash -c 'verilator -V|grep VERILATOR_ROOT | head -1 | sed -e "s/^.*=\s*//"') +VINC := $(VERILATOR_ROOT)/include + +obj_dir/Vreqwalker.cpp: reqwalker.v + $(VERILATOR) --trace -Wall -cc reqwalker.v + +obj_dir/Vreqwalker__ALL.a: obj_dir/Vreqwalker.cpp + make --no-print-directory -C obj_dir -f Vreqwalker.mk + +reqwalker_tb: reqwalker.cpp obj_dir/Vreqwalker__ALL.a + g++ -I$(VINC) -I obj_dir $(VINC)/verilated.cpp \ + $(VINC)/verilated_vcd_c.cpp \ + $(VINC)/verilated_threads.cpp reqwalker.cpp \ + obj_dir/Vreqwalker__ALL.a -o reqwalker_tb + +.PHONY: clean +clean: + rm -rf obj_dir/ reqwalker_tb reqwalker.vcd reqwalker_cvr/ reqwalker_prf/ diff --git a/protocols/tests/wishbone/reqwalker.cpp b/protocols/tests/wishbone/reqwalker.cpp new file mode 100644 index 00000000..89316104 --- /dev/null +++ b/protocols/tests/wishbone/reqwalker.cpp @@ -0,0 +1,149 @@ +//////////////////////////////////////////////////////////////////////////////// +// +// Filename: redqalker.cpp +// +// Project: Verilog Tutorial Example file +// +// Purpose: This is an example Verilator test bench driver file reqwalker +// module. +// +// Creator: Dan Gisselquist, Ph.D. +// Gisselquist Technology, LLC +// +//////////////////////////////////////////////////////////////////////////////// +// +// Written and distributed by Gisselquist Technology, LLC +// +// This program is hereby granted to the public domain. +// +// This program is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTIBILITY or +// FITNESS FOR A PARTICULAR PURPOSE. +// +//////////////////////////////////////////////////////////////////////////////// +// +// +#include +#include +#include "Vreqwalker.h" +#include "verilated.h" +#include "verilated_vcd_c.h" + +// Required by Verilator when not using SystemC +double sc_time_stamp() { return 0; } + +int tickcount = 0; +Vreqwalker *tb; +VerilatedVcdC *tfp; + +void tick(void) { + tickcount++; + + tb->eval(); + if (tfp) + tfp->dump(tickcount * 10 - 2); + tb->i_clk = 1; + tb->eval(); + if (tfp) + tfp->dump(tickcount * 10); + tb->i_clk = 0; + tb->eval(); + if (tfp) { + tfp->dump(tickcount * 10 + 5); + tfp->flush(); + } +} + +unsigned wb_read(unsigned a) { + tb->i_cyc = tb->i_stb = 1; + tb->i_we = 0; + tb->eval(); // update o_stall, which depends combinationally on i_we + tb->i_addr= a; + // Make the request + while(tb->o_stall) + tick(); + tick(); + tb->i_stb = 0; + // Wait for the ACK + while(!tb->o_ack) + tick(); + // Idle the bus, and read the response + tb->i_cyc = 0; + return tb->o_data; +} + +void wb_write(unsigned a, unsigned v) { + tb->i_cyc = tb->i_stb = 1; + tb->i_we = 1; + tb->eval(); // update o_stall, which depends combinationally on i_we + tb->i_addr= a; + tb->i_data= v; + // Make the bus request + while(tb->o_stall) + tick(); + tick(); + tb->i_stb = 0; + // Wait for the acknowledgement + while(!tb->o_ack) + tick(); + // Idle the bus and return + tb->i_cyc = tb->i_stb = 0; +} + +int main(int argc, char **argv) { + int last_led, last_state = 0, state = 0; + + // Call commandArgs first! + Verilated::commandArgs(argc, argv); + + // Instantiate our design + tb = new Vreqwalker; + + // Generate a trace + Verilated::traceEverOn(true); + tfp = new VerilatedVcdC; + tb->trace(tfp, 99); + tfp->open("reqwalker.vcd"); + + last_led = tb->o_led; + + // Read from the current state + printf("Initial state is: 0x%02x\n", + wb_read(0)); + + for(int cycle=0; cycle<2; cycle++) { + // Wait five clocks + for(int i=0; i<5; i++) + tick(); + + // Start the LEDs cycling + wb_write(0,0); + tick(); + + while((state = wb_read(0))!=0) { + if ((state != last_state) + ||(tb->o_led != last_led)) { + printf("%6d: State #%2d ", + tickcount, state); + for(int j=0; j<6; j++) { + if(tb->o_led & (1<o_led; + + // Idle cycle between reads so the VCD captures i_stb=0, + // making each transaction visible as a separate event to the monitor + tb->i_cyc = tb->i_stb = 0; + tick(); + } + } + + tfp->close(); + delete tfp; + delete tb; +} diff --git a/protocols/tests/wishbone/reqwalker.sby b/protocols/tests/wishbone/reqwalker.sby new file mode 100644 index 00000000..9e9e41b9 --- /dev/null +++ b/protocols/tests/wishbone/reqwalker.sby @@ -0,0 +1,17 @@ +[tasks] +cvr +prf + +[options] +cvr: mode cover +prf: mode prove + +[engines] +smtbmc + +[script] +read -formal reqwalker.v +prep -top reqwalker + +[files] +reqwalker.v diff --git a/protocols/tests/wishbone/reqwalker.v b/protocols/tests/wishbone/reqwalker.v new file mode 100644 index 00000000..a18c589d --- /dev/null +++ b/protocols/tests/wishbone/reqwalker.v @@ -0,0 +1,168 @@ +//////////////////////////////////////////////////////////////////////////////// +// +// Filename: reqwalker.v +// +// Project: Verilog Tutorial Example file +// +// Purpose: To walk an active LED back and forth across a set of 8 LEDs +// upon request. This is a demo design. It should be easy enough +// to adjust it to "N" LED's, or whatever your hardware has. +// +// This demo design is also broken in several ways. This is on purpose. +// Follow the coursework, and we'll find and fix the bugs in this design. +// +// Creator: Dan Gisselquist, Ph.D. +// Gisselquist Technology, LLC +// +//////////////////////////////////////////////////////////////////////////////// +// +// Written and distributed by Gisselquist Technology, LLC +// +// This program is hereby granted to the public domain. +// +// This program is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTIBILITY or +// FITNESS FOR A PARTICULAR PURPOSE. +// +//////////////////////////////////////////////////////////////////////////////// +// +// +module reqwalker(i_clk, + i_cyc, i_stb, i_we, i_addr, i_data, + o_stall, o_ack, o_data, + o_led); + input wire i_clk; + // + // Our wishbone bus interface + input wire i_cyc, i_stb, i_we; + input wire i_addr; + input wire [31:0] i_data; + // + output wire o_stall; + output reg o_ack; + output wire [31:0] o_data; + // + // The output LED + output reg [5:0] o_led; + + wire busy; + reg [3:0] state; + + initial state = 0; + always @(posedge i_clk) + if ((i_stb)&&(i_we)&&(!o_stall)) + state <= 4'h1; + else if (state >= 4'd11) + state <= 4'h0; + else if (state != 0) + state <= state + 1'b1; + + always @(posedge i_clk) + case(state) + 4'h1: o_led <= 6'b00_0001; + 4'h2: o_led <= 6'b00_0010; + 4'h3: o_led <= 6'b00_0100; + 4'h4: o_led <= 6'b00_1000; + 4'h5: o_led <= 6'b01_0000; + 4'h6: o_led <= 6'b10_0000; + 4'h7: o_led <= 6'b01_0000; + 4'h8: o_led <= 6'b00_1000; + 4'h9: o_led <= 6'b00_0100; + 4'ha: o_led <= 6'b00_0010; + 4'hb: o_led <= 6'b00_0001; + default: o_led <= 6'b00_0000; + endcase + + assign busy = (state != 0); + + initial o_ack = 1'b0; + always @(posedge i_clk) + o_ack <= (i_stb)&&(!o_stall); + + assign o_stall = (busy)&&(i_we); + assign o_data = { 28'h0, state }; + + // Verilator lint_off UNUSED + wire [33:0] unused; + assign unused = { i_cyc, i_addr, i_data }; + // Verilator lint_on UNUSED + +`ifdef FORMAL + reg f_past_valid; + initial f_past_valid = 0; + always @(posedge i_clk) + f_past_valid <= 1'b1; + + ////// + // + // Bus properties + // + initial assume(!i_cyc); + + // i_stb is only allowed if i_cyc is also true + always @(*) + if (!i_cyc) + assume(!i_stb); + + // When i_cyc goes high, so too should i_stb + // Since this is an assumption, no f_past_valid is required + always @(posedge i_clk) + if ((!$past(i_cyc))&&(i_cyc)) + assume(i_stb); + + // All request signals (data, addr, we, stb) must remain stable when the + // subordinate stalls + always @(posedge i_clk) + if (($past(i_stb))&&($past(o_stall))) + begin + assume(i_stb); + assume(i_we == $past(i_we)); + assume(i_addr == $past(i_addr)); + if (i_we) + assume(i_data == $past(i_data)); + end + + always @(posedge i_clk) + if ((f_past_valid)&&($past(i_stb))&&(!$past(o_stall))) + assert(o_ack); + + ////// + // + // Design properties + // + always @(*) + assert(state <= 4'd11); + + always @(*) + begin + case(state) + 4'h1: assert(o_led == 6'b00_0001); + 4'h2: assert(o_led == 6'b00_0010); + 4'h3: assert(o_led == 6'b00_0100); + 4'h4: assert(o_led == 6'b00_1000); + 4'h5: assert(o_led == 6'b01_0000); + 4'h6: assert(o_led == 6'b10_0000); + 4'h7: assert(o_led == 6'b01_0000); + 4'h8: assert(o_led == 6'b00_1000); + 4'h9: assert(o_led == 6'b00_0100); + 4'ha: assert(o_led == 6'b00_0010); + 4'hb: assert(o_led == 6'b00_0001); + endcase + end + + always @(posedge i_clk) + if ((f_past_valid)&&($past(i_stb))&&($past(i_we))&&($past(!o_stall))) + begin + assert(state == 1); + assert(busy); + end + + always @(posedge i_clk) + if ((f_past_valid)&&($past(busy))&&($past(state < 4'hb))) + assert(state == $past(state)+1); + + always @(posedge i_clk) + if (f_past_valid) + cover((!busy)&&($past(busy))); +`endif +endmodule diff --git a/protocols/tests/wishbone/wishbone.out b/protocols/tests/wishbone/wishbone.out new file mode 100644 index 00000000..f5f6cb49 --- /dev/null +++ b/protocols/tests/wishbone/wishbone.out @@ -0,0 +1 @@ +Trace 0 executed successfully! diff --git a/protocols/tests/wishbone/wishbone.prot b/protocols/tests/wishbone/wishbone.prot new file mode 100644 index 00000000..e95f4f45 --- /dev/null +++ b/protocols/tests/wishbone/wishbone.prot @@ -0,0 +1,142 @@ +/// Wishbone B4 (Pipeline mode) subordinate + +// TODO: run the monitor on some existing waveforms +// Eventually put all the traces in a separate repo + +// For Wishbone, you can model everything using the same interface, +// whereas for AXI we can't do this (because responses can be out of order in AXI <---- is this true?) + +// See if there is already a thing which takes Wishbone inputs/outputs and outputs transaction trace +// ^^ such a thing might already exist and is hard-coded +// TODO: see https://github.com/wallento/cocotbext-wishbone for a possible monitor + +struct WBSubordinate { + // Cycle is high anytime an active pipeline session is occurring + in i_cyc: u1, + + // Strobe is high when there is a request to the subordinate + // (akin to Valid in AXI-Lite, i.e. they indicate the manager + // has something to transfer) + in i_stb: u1, + + // Write-enable (true for write-requests) + in i_we: u1, + + // Address of the request + in i_addr: u1, + + // Data to be written + in i_data: u32, + + // Response from the subordinate, indicating that the request + // has been fulfilled. + out o_ack: u1, + + // True on any cycle when the subordinate can't accept requests + // False when a request can be accepted + // (i.e. the opposite of Ready in AXI-Lite) + out o_stall: u1, + + // Data returned by the subordinate to the manager + // This is valid only when ACK is true + out o_data: u32, + + // LED output: one-hot encoding of the current walker state + out o_led: u6 +} + +// Both cyc & stb are low when the subordinate is low, +// everything else is DontCare +#[idle] +prot idle() { + DUT.i_cyc := 1'b0; + DUT.i_stb := 1'b0; + DUT.i_we := X; + DUT.i_addr := X; + DUT.i_data := X; + step(); +} + +// Writes a `data` value to the subordinate, and observes the +// resultant `led` state via an output parameter. +// Wishbone says to hold all request signals while stalled (stall=1), +// i.e. when the subordinate is busy processing a previous request. +prot write(in addr: u1, in data: u32, out led: u6) { + DUT.i_cyc := 1'b1; + DUT.i_stb := 1'b1; + DUT.i_we := 1'b1; + DUT.i_addr := addr; + DUT.i_data := data; + // For reqwalker, stall is combinational: o_stall = busy && i_we. + // When state=0 (idle, can accept), busy=0 so stall=0 before the accept posedge. + // Stall=1 only appears AT the accept posedge (state 0->1), so the loop + // is omitted here; the monitor samples posedge values where stall=1 already + // coincides with ack=1 (post-accept artifact). + // Request accepted on this cycle; ack registered next cycle + step(); + // i_stb goes to DontCare after acceptance: per Wishbone B4 the master may + // keep stb high for pipelined requests, and in VCDs the 0 only appears at + // the *next* posedge (testbench sets it after tick() returns). + DUT.i_cyc := X; + DUT.i_stb := X; + DUT.i_we := X; + DUT.i_addr := X; + DUT.i_data := X; + + // Based on the Verilog, there is a 1 cycle latency before the + // ack is registered. + while (DUT.o_ack == 1'b0) { + step(); + } + + // Ack is now 1, the data write is complete + // Note: During the ACK phase, we have i_cyc=1 (session still active) + // and i_stb=0 (no new request). + + // Observe resultant LED state + assert_eq(DUT.o_led, led); + + // Set to DontCare so the next protocol can decide whether to continue. + // No explicit fork(): using implicit fork so the next transaction starts + // at the *next* cycle (after i_cyc drops to 0 and the bus becomes idle). + DUT.i_stb := X; + DUT.i_cyc := X; + step(); +} + +// Reads a value and the LED state from the subordinate +// (the `data` and the `led` state are conveyed via output parameters) +prot read(in addr: u1, out data: u32, out led: u6) { + DUT.i_cyc := 1'b1; + DUT.i_stb := 1'b1; + DUT.i_we := 1'b0; + DUT.i_addr := addr; + DUT.i_data := X; + + // Wait while the subordinate stalls + while (DUT.o_stall == 1'b1) { + step(); + } + // Read request accepted, one cycle for data transfer. + // i_stb goes to DontCare after acceptance (same reasoning as write above). + step(); + DUT.i_stb := X; + DUT.i_we := X; + DUT.i_addr := X; + + // Wait for ack; data is valid to read when ack becomes 1 + while (DUT.o_ack == 1'b0) { + step(); + } + + // Observe resultant data value & LED state + assert_eq(DUT.o_data, data); + assert_eq(DUT.o_led, led); + + // Set to DontCare so the next protocol can decide whether to continue. + // No explicit fork(): using implicit fork so the next transaction starts + // at the *next* cycle (after i_cyc drops to 0 and the bus becomes idle). + DUT.i_stb := X; + DUT.i_cyc := X; + step(); +} diff --git a/protocols/tests/wishbone/wishbone.tx b/protocols/tests/wishbone/wishbone.tx new file mode 100644 index 00000000..e10d75ba --- /dev/null +++ b/protocols/tests/wishbone/wishbone.tx @@ -0,0 +1,43 @@ +// ARGS: --verilog wishbone/reqwalker.v --protocol=wishbone/wishbone.prot --module reqwalker +trace { + // Initial state register is 0; o_led=0 (default case for state=0) + read(0, 0, 0); + + // Trigger the LED animation: on the accept edge, state becomes 1. + // o_led still shows the old case 0 (from the previous cycle) due to a 1-cycle delay + write(0, 0, 0); + + // Read back `o_data` and `o_led` as the LED walks through states. + // `o_data` is the current state, `o_led` shows the LED state in the *previous* cycle + read(0, 2, 0b000001); // state 1->2, o_led=case(1) =0b00_0001 + read(0, 3, 0b000010); // state 2->3, o_led=case(2) =0b00_0010 + read(0, 4, 0b000100); // state 3->4, o_led=case(3) =0b00_0100 + read(0, 5, 0b001000); // state 4->5, o_led=case(4) =0b00_1000 + read(0, 6, 0b010000); // state 5->6, o_led=case(5) =0b01_0000 + read(0, 7, 0b100000); // state 6->7, o_led=case(6) =0b10_0000 + read(0, 8, 0b010000); // state 7->8, o_led=case(7) =0b01_0000 + read(0, 9, 0b001000); // state 8->9, o_led=case(8) =0b00_1000 + read(0, 10, 0b000100); // state 9->10, o_led=case(9) =0b00_0100 + read(0, 11, 0b000010); // state 10->11, o_led=case(10)=0b00_0010 + read(0, 0, 0b000001); // state 11->0, o_led=case(11)=0b00_0001 + + // State is back to 0; o_led now catches up to case(0)=0 + read(0, 0, 0b000000); +} + + +// +-------------+--------------+-------------+--------+-------------+ +// | Clock Cycle | state before | state after | o_data | o_led | +// +-------------+--------------+-------------+--------+-------------+ +// | 1 | 1 | 2 | 2 | 0b000001=1 | +// | 2 | 2 | 3 | 3 | 0b000010=2 | +// | 3 | 3 | 4 | 4 | 0b000100=4 | +// | 4 | 4 | 5 | 5 | 0b001000=8 | +// | 5 | 5 | 6 | 6 | 0b010000=16 | +// | 6 | 6 | 7 | 7 | 0b100000=32 | +// | 7 | 7 | 8 | 8 | 0b010000=16 | +// | 8 | 8 | 9 | 9 | 0b001000=8 | +// | 9 | 9 | 10 | 10 | 0b000100=4 | +// | 10 | 10 | 11 | 11 | 0b000010=2 | +// | 11 | 11 | 0 | 0 | 0b000001=1 | +// +-------------+--------------+-------------+--------+-------------+