Include verilog source files for demo1.sby

Signed-off-by: Claire Wolf <claire@symbioticeda.com>

Makefile

@@ -47,13 +47,13 @@ test: \
   test_quickstart_demo test_quickstart_cover test_quickstart_prove test_quickstart_memory
 
 test_demo1:
-	python3 sbysrc/sby.py -f sbysrc/demo1.sby
+	cd sbysrc && python3 sby.py -f demo1.sby
 
 test_demo2:
-	python3 sbysrc/sby.py -f sbysrc/demo2.sby
+	cd sbysrc && python3 sby.py -f demo2.sby
 
 test_demo3:
-	python3 sbysrc/sby.py -f sbysrc/demo3.sby
+	cd sbysrc && python3 sby.py -f demo3.sby
 
 test_abstract_abstr:
 	cd docs/examples/abstract && python3 ../../../sbysrc/sby.py -f abstr.sby

extern/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

sbysrc/demo1.sby

@@ -16,6 +16,6 @@ read_verilog -formal axicheck.v
 prep -top testbench
 
 [files]
-picorv32.v ~/Work/picorv32/picorv32.v
+picorv32.v ../extern/picorv32.v
-axicheck.v ~/Work/picorv32/scripts/smtbmc/axicheck.v
+axicheck.v ../extern/axicheck.v