From 624d39669d4adc89a38d7adb6021a363d6e6cde8 Mon Sep 17 00:00:00 2001
From: Luke Wren <wren6991@gmail.com>
Date: Mon, 29 Aug 2022 19:20:09 +0100
Subject: [PATCH] Fix up new asserts in hazard3_power_ctrl. Add power signals
to formal TBs.
---
hdl/hazard3_power_ctrl.v | 46 ++++---
test/formal/bus_compliance_1port/tb.v | 156 +++++++++++++++--------
test/formal/bus_compliance_2port/tb.v | 69 ++++++++--
test/formal/instruction_fetch_match/tb.v | 13 ++
4 files changed, 207 insertions(+), 77 deletions(-)
diff --git a/hdl/hazard3_power_ctrl.v b/hdl/hazard3_power_ctrl.v
index 400fef9..bcf780c 100644
--- a/hdl/hazard3_power_ctrl.v
+++ b/hdl/hazard3_power_ctrl.v
@@ -116,24 +116,38 @@ always @ (posedge clk_always_on or negedge rst_n) begin
end
endcase
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
+`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
diff --git a/test/formal/bus_compliance_1port/tb.v b/test/formal/bus_compliance_1port/tb.v
index a19f8df..06afc8b 100644
--- a/test/formal/bus_compliance_1port/tb.v
+++ b/test/formal/bus_compliance_1port/tb.v
@@ -11,19 +11,25 @@ always @ (posedge clk)
// ----------------------------------------------------------------------------
// DUT
-(* keep *) wire [31:0] ahblm_haddr;
-(* keep *) wire ahblm_hwrite;
-(* keep *) wire ahblm_hexcl;
-(* keep *) wire [1:0] ahblm_htrans;
-(* keep *) wire [2:0] ahblm_hsize;
-(* keep *) wire [2:0] ahblm_hburst;
-(* keep *) wire [3:0] ahblm_hprot;
-(* keep *) wire ahblm_hmastlock;
-(* keep *) wire ahblm_hready;
-(* keep *) wire ahblm_hexokay;
-(* keep *) wire ahblm_hresp;
-(* keep *) wire [31:0] ahblm_hwdata;
-(* keep *) wire [31:0] ahblm_hrdata;
+(* keep *) wire pwrup_req;
+(* keep *) wire pwrup_ack;
+(* keep *) wire clk_en;
+(* keep *) wire unblock_out;
+(* keep *) wire unblock_in;
+
+(* keep *) wire [31:0] haddr;
+(* keep *) wire hwrite;
+(* keep *) wire hexcl;
+(* keep *) wire [1:0] htrans;
+(* keep *) wire [2:0] hsize;
+(* keep *) wire [2:0] hburst;
+(* 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;
@@ -56,21 +62,28 @@ localparam W_DATA = 32;
hazard3_cpu_1port dut (
.clk (clk),
+ .clk_always_on (clk),
.rst_n (rst_n),
- .ahblm_haddr (ahblm_haddr),
- .ahblm_hwrite (ahblm_hwrite),
- .ahblm_hexcl (ahblm_hexcl),
- .ahblm_htrans (ahblm_htrans),
- .ahblm_hsize (ahblm_hsize),
- .ahblm_hburst (ahblm_hburst),
- .ahblm_hprot (ahblm_hprot),
- .ahblm_hmastlock (ahblm_hmastlock),
- .ahblm_hready (ahblm_hready),
- .ahblm_hexokay (ahblm_hexokay),
- .ahblm_hresp (ahblm_hresp),
- .ahblm_hwdata (ahblm_hwdata),
- .ahblm_hrdata (ahblm_hrdata),
+ .pwrup_req (pwrup_req),
+ .pwrup_ack (pwrup_ack),
+ .clk_en (clk_en),
+ .unblock_out (unblock_out),
+ .unblock_in (unblock_in),
+
+ .haddr (haddr),
+ .hwrite (hwrite),
+ .hexcl (hexcl),
+ .htrans (htrans),
+ .hsize (hsize),
+ .hburst (hburst),
+ .hprot (hprot),
+ .hmastlock (hmastlock),
+ .hready (hready),
+ .hexokay (hexokay),
+ .hresp (hresp),
+ .hwdata (hwdata),
+ .hrdata (hrdata),
.dbg_req_halt (dbg_req_halt),
.dbg_req_halt_on_reset (dbg_req_halt_on_reset),
@@ -100,6 +113,43 @@ hazard3_cpu_1port dut (
.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
@@ -112,39 +162,39 @@ ahbl_slave_assumptions #(
.clk (clk),
.rst_n (rst_n),
- .dst_hready_resp (ahblm_hready),
- .dst_hready (ahblm_hready),
- .dst_hresp (ahblm_hresp),
- .dst_hexokay (ahblm_hexokay),
- .dst_haddr (ahblm_haddr),
- .dst_hwrite (ahblm_hwrite),
- .dst_htrans (ahblm_htrans),
- .dst_hsize (ahblm_hsize),
- .dst_hburst (ahblm_hburst),
- .dst_hprot (ahblm_hprot),
- .dst_hmastlock (ahblm_hmastlock),
- .dst_hexcl (ahblm_hexcl),
- .dst_hwdata (ahblm_hwdata),
- .dst_hrdata (ahblm_hrdata)
+ .dst_hready_resp (hready),
+ .dst_hready (hready),
+ .dst_hresp (hresp),
+ .dst_hexokay (hexokay),
+ .dst_haddr (haddr),
+ .dst_hwrite (hwrite),
+ .dst_htrans (htrans),
+ .dst_hsize (hsize),
+ .dst_hburst (hburst),
+ .dst_hprot (hprot),
+ .dst_hmastlock (hmastlock),
+ .dst_hexcl (hexcl),
+ .dst_hwdata (hwdata),
+ .dst_hrdata (hrdata)
);
ahbl_master_assertions d_assertions (
.clk (clk),
.rst_n (rst_n),
- .src_hready (ahblm_hready),
- .src_hresp (ahblm_hresp),
- .src_hexokay (ahblm_hexokay),
- .src_haddr (ahblm_haddr),
- .src_hwrite (ahblm_hwrite),
- .src_htrans (ahblm_htrans),
- .src_hsize (ahblm_hsize),
- .src_hburst (ahblm_hburst),
- .src_hprot (ahblm_hprot),
- .src_hmastlock (ahblm_hmastlock),
- .src_hexcl (ahblm_hexcl),
- .src_hwdata (ahblm_hwdata),
- .src_hrdata (ahblm_hrdata)
+ .src_hready (hready),
+ .src_hresp (hresp),
+ .src_hexokay (hexokay),
+ .src_haddr (haddr),
+ .src_hwrite (hwrite),
+ .src_htrans (htrans),
+ .src_hsize (hsize),
+ .src_hburst (hburst),
+ .src_hprot (hprot),
+ .src_hmastlock (hmastlock),
+ .src_hexcl (hexcl),
+ .src_hwdata (hwdata),
+ .src_hrdata (hrdata)
);
sbus_assumptions sbus_assumptions (
diff --git a/test/formal/bus_compliance_2port/tb.v b/test/formal/bus_compliance_2port/tb.v
index a6e83f4..887a4ab 100644
--- a/test/formal/bus_compliance_2port/tb.v
+++ b/test/formal/bus_compliance_2port/tb.v
@@ -1,6 +1,8 @@
// Assume bus responses to both ports are well-formed, assert that bus
// requests are well-formed.
+`default_nettype none
+
module tb;
reg clk;
@@ -11,6 +13,12 @@ always @ (posedge clk)
// ----------------------------------------------------------------------------
// 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 i_hwrite;
(* 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_ebreak;
-(*keep*) wire [31:0] dbg_sbus_addr;
-(*keep*) wire dbg_sbus_write;
-(*keep*) wire [1:0] dbg_sbus_size;
-(*keep*) wire dbg_sbus_vld;
-(*keep*) wire dbg_sbus_rdy;
-(*keep*) wire dbg_sbus_err;
-(*keep*) wire [31:0] dbg_sbus_wdata;
-(*keep*) wire [31:0] dbg_sbus_rdata;
+(* keep *) wire [31:0] dbg_sbus_addr;
+(* keep *) wire dbg_sbus_write;
+(* keep *) wire [1:0] dbg_sbus_size;
+(* keep *) wire dbg_sbus_vld;
+(* keep *) wire dbg_sbus_rdy;
+(* keep *) wire dbg_sbus_err;
+(* keep *) wire [31:0] dbg_sbus_wdata;
+(* keep *) wire [31:0] dbg_sbus_rdata;
(* keep *) wire [31:0] irq;
(* keep *) wire soft_irq;
@@ -68,8 +76,15 @@ localparam W_DATA = 32;
hazard3_cpu_2port dut (
.clk (clk),
+ .clk_always_on (clk),
.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_hwrite (i_hwrite),
.i_htrans (i_htrans),
@@ -124,6 +139,44 @@ hazard3_cpu_2port dut (
.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
diff --git a/test/formal/instruction_fetch_match/tb.v b/test/formal/instruction_fetch_match/tb.v
index 4a97f28..5ade286 100644
--- a/test/formal/instruction_fetch_match/tb.v
+++ b/test/formal/instruction_fetch_match/tb.v
@@ -11,6 +11,12 @@ always @ (posedge clk)
// ----------------------------------------------------------------------------
// 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 i_hwrite;
(* keep *) wire [1:0] i_htrans;
@@ -61,8 +67,15 @@ localparam W_DATA = 32;
hazard3_cpu_2port dut (
.clk (clk),
+ .clk_always_on (clk),
.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_hwrite (i_hwrite),
.i_htrans (i_htrans),