colin
/
Hazard3
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Fix up new asserts in hazard3_power_ctrl. Add power signals to formal TBs.

This commit is contained in:
Luke Wren 2022-08-29 19:20:09 +01:00
parent 1c2249dbef
commit 624d39669d
4 changed files with 207 additions and 77 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

46
hdl/hazard3_power_ctrl.v
View File

@ -116,24 +116,38 @@ always @ (posedge clk_always_on or negedge rst_n) begin
end end
endcase endcase
end end
`ifdef HAZARD3_ASSERTIONS
// These must always be mutually exclusive.
assert(!(sleeping_on_wfi && sleeping_on_block));
if (stall_release) begin
// Presumably there was a stall which we just released
assert($past(sleeping_on_wfi) || $past(sleeping_on_block));
// Presumably we are still in that stall
assert(sleeping_on_wfi|| sleeping_on_block);
// It takes one cycle to do a release and enter a new sleep state, so a
// double release should be impossible.
assert(!$past(stall_release));
end
if (state == S_ASLEEP) begin
assert(allow_power_down || allow_sleep);
end
`endif
end end
`ifdef HAZARD3_ASSERTIONS
// Regs are a workaround for the non-constant reset value issue with
// $past() in yosys-smtbmc.
reg past_sleeping;
reg past_stall_release;
always @ (posedge clk_always_on or negedge rst_n) begin
if (!rst_n) begin
past_sleeping <= 1'b0;
past_stall_release <= 1'b0;
end else begin
past_sleeping <= sleeping_on_wfi || sleeping_on_block;
past_stall_release <= stall_release;
// These must always be mutually exclusive.
assert(!(sleeping_on_wfi && sleeping_on_block));
if (stall_release) begin
// Presumably there was a stall which we just released
assert(past_sleeping);
// Presumably we are still in that stall
assert(sleeping_on_wfi|| sleeping_on_block);
// It takes one cycle to do a release and enter a new sleep state, so a
// double release should be impossible.
assert(!past_stall_release);
end
if (state == S_ASLEEP) begin
assert(allow_power_down || allow_sleep);
end
end
end
`endif
// ---------------------------------------------------------------------------- // ----------------------------------------------------------------------------
// Pulse->level for block wakeup // Pulse->level for block wakeup

156
test/formal/bus_compliance_1port/tb.v
View File

@ -11,19 +11,25 @@ always @ (posedge clk)
// ---------------------------------------------------------------------------- // ----------------------------------------------------------------------------
// DUT // DUT
(* keep *) wire [31:0] ahblm_haddr; (* keep *) wire pwrup_req;
(* keep *) wire ahblm_hwrite; (* keep *) wire pwrup_ack;
(* keep *) wire ahblm_hexcl; (* keep *) wire clk_en;
(* keep *) wire [1:0] ahblm_htrans; (* keep *) wire unblock_out;
(* keep *) wire [2:0] ahblm_hsize; (* keep *) wire unblock_in;
(* keep *) wire [2:0] ahblm_hburst;
(* keep *) wire [3:0] ahblm_hprot; (* keep *) wire [31:0] haddr;
(* keep *) wire ahblm_hmastlock; (* keep *) wire hwrite;
(* keep *) wire ahblm_hready; (* keep *) wire hexcl;
(* keep *) wire ahblm_hexokay; (* keep *) wire [1:0] htrans;
(* keep *) wire ahblm_hresp; (* keep *) wire [2:0] hsize;
(* keep *) wire [31:0] ahblm_hwdata; (* keep *) wire [2:0] hburst;
(* keep *) wire [31:0] ahblm_hrdata; (* keep *) wire [3:0] hprot;
(* keep *) wire hmastlock;
(* keep *) wire hready;
(* keep *) wire hexokay;
(* keep *) wire hresp;
(* keep *) wire [31:0] hwdata;
(* keep *) wire [31:0] hrdata;
localparam W_DATA = 32; localparam W_DATA = 32;
@ -56,21 +62,28 @@ localparam W_DATA = 32;
hazard3_cpu_1port dut ( hazard3_cpu_1port dut (
.clk (clk), .clk (clk),
.clk_always_on (clk),
.rst_n (rst_n), .rst_n (rst_n),
.ahblm_haddr (ahblm_haddr), .pwrup_req (pwrup_req),
.ahblm_hwrite (ahblm_hwrite), .pwrup_ack (pwrup_ack),
.ahblm_hexcl (ahblm_hexcl), .clk_en (clk_en),
.ahblm_htrans (ahblm_htrans), .unblock_out (unblock_out),
.ahblm_hsize (ahblm_hsize), .unblock_in (unblock_in),
.ahblm_hburst (ahblm_hburst),
.ahblm_hprot (ahblm_hprot), .haddr (haddr),
.ahblm_hmastlock (ahblm_hmastlock), .hwrite (hwrite),
.ahblm_hready (ahblm_hready), .hexcl (hexcl),
.ahblm_hexokay (ahblm_hexokay), .htrans (htrans),
.ahblm_hresp (ahblm_hresp), .hsize (hsize),
.ahblm_hwdata (ahblm_hwdata), .hburst (hburst),
.ahblm_hrdata (ahblm_hrdata), .hprot (hprot),
.hmastlock (hmastlock),
.hready (hready),
.hexokay (hexokay),
.hresp (hresp),
.hwdata (hwdata),
.hrdata (hrdata),
.dbg_req_halt (dbg_req_halt), .dbg_req_halt (dbg_req_halt),
.dbg_req_halt_on_reset (dbg_req_halt_on_reset), .dbg_req_halt_on_reset (dbg_req_halt_on_reset),
@ -100,6 +113,43 @@ hazard3_cpu_1port dut (
.timer_irq (timer_irq) .timer_irq (timer_irq)
); );
// ----------------------------------------------------------------------------
// Power signal properties
(* keep *) wire pwrup_ack_nxt;
always @ (posedge clk or negedge rst_n) begin
if (!rst_n) begin
pwrup_ack <= 1'b1;
end else begin
pwrup_ack <= 1'b1;
end
end
always @ (posedge clk) if (rst_n) begin
// Assume the testbench gives fair acks to the processor's reqs
if (pwrup_req && pwrup_ack) begin
assume(pwrup_ack_nxt);
end
if (!pwrup_req && !pwrup_ack) begin
assume(!pwrup_ack_nxt);
end
// Assume there is no sbus access when powered down
if (!(pwrup_req && pwrup_ack && clk_en)) begin
assume(!dbg_sbus_vld);
end
// Assert only one of pwrup_req and pwrup_ack changes on one cycle
// (processor upholds its side of the 4-phase handshake)
assert((pwrup_ack != $past(pwrup_ack)) + {1'b0, (pwrup_req != $past(pwrup_req))} < 2'd2);
// Assert rocessor doesn't access the bus whilst asleep
if (!(pwrup_req && pwrup_ack && clk_en)) begin
assert(htrans == 2'h0);
end
end
// ---------------------------------------------------------------------------- // ----------------------------------------------------------------------------
// Bus properties // Bus properties
@ -112,39 +162,39 @@ ahbl_slave_assumptions #(
.clk (clk), .clk (clk),
.rst_n (rst_n), .rst_n (rst_n),
.dst_hready_resp (ahblm_hready), .dst_hready_resp (hready),
.dst_hready (ahblm_hready), .dst_hready (hready),
.dst_hresp (ahblm_hresp), .dst_hresp (hresp),
.dst_hexokay (ahblm_hexokay), .dst_hexokay (hexokay),
.dst_haddr (ahblm_haddr), .dst_haddr (haddr),
.dst_hwrite (ahblm_hwrite), .dst_hwrite (hwrite),
.dst_htrans (ahblm_htrans), .dst_htrans (htrans),
.dst_hsize (ahblm_hsize), .dst_hsize (hsize),
.dst_hburst (ahblm_hburst), .dst_hburst (hburst),
.dst_hprot (ahblm_hprot), .dst_hprot (hprot),
.dst_hmastlock (ahblm_hmastlock), .dst_hmastlock (hmastlock),
.dst_hexcl (ahblm_hexcl), .dst_hexcl (hexcl),
.dst_hwdata (ahblm_hwdata), .dst_hwdata (hwdata),
.dst_hrdata (ahblm_hrdata) .dst_hrdata (hrdata)
); );
ahbl_master_assertions d_assertions ( ahbl_master_assertions d_assertions (
.clk (clk), .clk (clk),
.rst_n (rst_n), .rst_n (rst_n),
.src_hready (ahblm_hready), .src_hready (hready),
.src_hresp (ahblm_hresp), .src_hresp (hresp),
.src_hexokay (ahblm_hexokay), .src_hexokay (hexokay),
.src_haddr (ahblm_haddr), .src_haddr (haddr),
.src_hwrite (ahblm_hwrite), .src_hwrite (hwrite),
.src_htrans (ahblm_htrans), .src_htrans (htrans),
.src_hsize (ahblm_hsize), .src_hsize (hsize),
.src_hburst (ahblm_hburst), .src_hburst (hburst),
.src_hprot (ahblm_hprot), .src_hprot (hprot),
.src_hmastlock (ahblm_hmastlock), .src_hmastlock (hmastlock),
.src_hexcl (ahblm_hexcl), .src_hexcl (hexcl),
.src_hwdata (ahblm_hwdata), .src_hwdata (hwdata),
.src_hrdata (ahblm_hrdata) .src_hrdata (hrdata)
); );
sbus_assumptions sbus_assumptions ( sbus_assumptions sbus_assumptions (

69
test/formal/bus_compliance_2port/tb.v
View File

@ -1,6 +1,8 @@
// Assume bus responses to both ports are well-formed, assert that bus // Assume bus responses to both ports are well-formed, assert that bus
// requests are well-formed. // requests are well-formed.
`default_nettype none
module tb; module tb;
reg clk; reg clk;
@ -11,6 +13,12 @@ always @ (posedge clk)
// ---------------------------------------------------------------------------- // ----------------------------------------------------------------------------
// DUT // DUT
(* keep *) wire pwrup_req;
(* keep *) wire pwrup_ack;
(* keep *) wire clk_en;
(* keep *) wire unblock_out;
(* keep *) wire unblock_in;
(* keep *) wire [31:0] i_haddr; (* keep *) wire [31:0] i_haddr;
(* keep *) wire i_hwrite; (* keep *) wire i_hwrite;
(* keep *) wire [1:0] i_htrans; (* keep *) wire [1:0] i_htrans;
@ -53,14 +61,14 @@ localparam W_DATA = 32;
(* keep *) wire dbg_instr_caught_exception; (* keep *) wire dbg_instr_caught_exception;
(* keep *) wire dbg_instr_caught_ebreak; (* keep *) wire dbg_instr_caught_ebreak;
(*keep*) wire [31:0] dbg_sbus_addr; (* keep *) wire [31:0] dbg_sbus_addr;
(*keep*) wire dbg_sbus_write; (* keep *) wire dbg_sbus_write;
(*keep*) wire [1:0] dbg_sbus_size; (* keep *) wire [1:0] dbg_sbus_size;
(*keep*) wire dbg_sbus_vld; (* keep *) wire dbg_sbus_vld;
(*keep*) wire dbg_sbus_rdy; (* keep *) wire dbg_sbus_rdy;
(*keep*) wire dbg_sbus_err; (* keep *) wire dbg_sbus_err;
(*keep*) wire [31:0] dbg_sbus_wdata; (* keep *) wire [31:0] dbg_sbus_wdata;
(*keep*) wire [31:0] dbg_sbus_rdata; (* keep *) wire [31:0] dbg_sbus_rdata;
(* keep *) wire [31:0] irq; (* keep *) wire [31:0] irq;
(* keep *) wire soft_irq; (* keep *) wire soft_irq;
@ -68,8 +76,15 @@ localparam W_DATA = 32;
hazard3_cpu_2port dut ( hazard3_cpu_2port dut (
.clk (clk), .clk (clk),
.clk_always_on (clk),
.rst_n (rst_n), .rst_n (rst_n),
.pwrup_req (pwrup_req),
.pwrup_ack (pwrup_ack),
.clk_en (clk_en),
.unblock_out (unblock_out),
.unblock_in (unblock_in),
.i_haddr (i_haddr), .i_haddr (i_haddr),
.i_hwrite (i_hwrite), .i_hwrite (i_hwrite),
.i_htrans (i_htrans), .i_htrans (i_htrans),
@ -124,6 +139,44 @@ hazard3_cpu_2port dut (
.timer_irq (timer_irq) .timer_irq (timer_irq)
); );
// ----------------------------------------------------------------------------
// Power signal properties
(* keep *) wire pwrup_ack_nxt;
always @ (posedge clk or negedge rst_n) begin
if (!rst_n) begin
pwrup_ack <= 1'b1;
end else begin
pwrup_ack <= 1'b1;
end
end
always @ (posedge clk) if (rst_n) begin
// Assume the testbench gives fair acks to the processor's reqs
if (pwrup_req && pwrup_ack) begin
assume(pwrup_ack_nxt);
end
if (!pwrup_req && !pwrup_ack) begin
assume(!pwrup_ack_nxt);
end
// Assume there is no sbus access when powered down
if (!(pwrup_req && pwrup_ack && clk_en)) begin
assume(!dbg_sbus_vld);
end
// Assert only one of pwrup_req and pwrup_ack changes on one cycle
// (processor upholds its side of the 4-phase handshake)
assert((pwrup_ack != $past(pwrup_ack)) + {1'b0, (pwrup_req != $past(pwrup_req))} < 2'd2);
// Assert rocessor doesn't access the bus whilst asleep
if (!(pwrup_req && pwrup_ack && clk_en)) begin
assert(i_htrans == 2'h0);
assert(d_htrans == 2'h0);
end
end
// ---------------------------------------------------------------------------- // ----------------------------------------------------------------------------
// Bus properties // Bus properties

13
test/formal/instruction_fetch_match/tb.v
View File

@ -11,6 +11,12 @@ always @ (posedge clk)
// ---------------------------------------------------------------------------- // ----------------------------------------------------------------------------
// DUT // DUT
(* keep *) wire pwrup_req;
(* keep *) wire pwrup_ack;
(* keep *) wire clk_en;
(* keep *) wire unblock_out;
(* keep *) wire unblock_in;
(* keep *) wire [31:0] i_haddr; (* keep *) wire [31:0] i_haddr;
(* keep *) wire i_hwrite; (* keep *) wire i_hwrite;
(* keep *) wire [1:0] i_htrans; (* keep *) wire [1:0] i_htrans;
@ -61,8 +67,15 @@ localparam W_DATA = 32;
hazard3_cpu_2port dut ( hazard3_cpu_2port dut (
.clk (clk), .clk (clk),
.clk_always_on (clk),
.rst_n (rst_n), .rst_n (rst_n),
.pwrup_req (pwrup_req),
.pwrup_ack (pwrup_ack),
.clk_en (clk_en),
.unblock_out (unblock_out),
.unblock_in (unblock_in),
.i_haddr (i_haddr), .i_haddr (i_haddr),
.i_hwrite (i_hwrite), .i_hwrite (i_hwrite),
.i_htrans (i_htrans), .i_htrans (i_htrans),