(WIP) Buggy Wishbone subordinate example

protocols/tests/wishbone/.gitignore

@@ -0,0 +1,2 @@
+obj_dir/*
+reqwalker_tb

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/

protocols/tests/wishbone/reqwalker.cpp

@@ -0,0 +1,144 @@
+////////////////////////////////////////////////////////////////////////////////
+//
+// 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 <stdio.h>
+#include <stdlib.h>
+#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 combinatorially 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 combinatorially 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<<j))
+						printf("O");
+					else
+						printf("-");
+				} printf("\n");
+			}
+
+			last_state = state;
+			last_led = tb->o_led;
+		}
+	}
+
+	tfp->close();
+	delete tfp;
+	delete tb;
+}

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

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

protocols/tests/wishbone/wishbone.out

@@ -0,0 +1 @@
+Trace 0 executed successfully!