mirror of
https://github.com/supleed2/ELEC70056-HSV-CW2.git
synced 2024-12-22 21:55:48 +00:00
Fix GPIO assertions and test-bench coverage and constraints
This commit is contained in:
parent
f2b3a72a54
commit
128a2a9eaa
|
@ -97,8 +97,10 @@ module AHBGPIO
|
||||||
|
|
||||||
// Update input value
|
// Update input value
|
||||||
always_ff @(posedge HCLK, negedge HRESETn)
|
always_ff @(posedge HCLK, negedge HRESETn)
|
||||||
if(!HRESETn)
|
if(!HRESETn) begin
|
||||||
gpio_datain <= 16'h0000;
|
gpio_datain <= 16'h0000;
|
||||||
|
gpio_parityerr <= '0;
|
||||||
|
end
|
||||||
else if (gpio_dir == 16'h0000) begin
|
else if (gpio_dir == 16'h0000) begin
|
||||||
gpio_datain <= GPIOIN[15:0];
|
gpio_datain <= GPIOIN[15:0];
|
||||||
gpio_parityerr <= ~^{GPIOIN,PARITYSEL,INJECT_FAULT};
|
gpio_parityerr <= ~^{GPIOIN,PARITYSEL,INJECT_FAULT};
|
||||||
|
@ -111,7 +113,7 @@ module AHBGPIO
|
||||||
assign PARITYERR = gpio_parityerr;
|
assign PARITYERR = gpio_parityerr;
|
||||||
|
|
||||||
//check behaviour
|
//check behaviour
|
||||||
|
|
||||||
assert_parity: assert property
|
assert_parity: assert property
|
||||||
( @(posedge HCLK) disable iff (!HRESETn)
|
( @(posedge HCLK) disable iff (!HRESETn)
|
||||||
!PARITYERR
|
!PARITYERR
|
||||||
|
@ -119,23 +121,23 @@ module AHBGPIO
|
||||||
|
|
||||||
assert_gpio_write: assert property
|
assert_gpio_write: assert property
|
||||||
( @(posedge HCLK) disable iff (!HRESETn)
|
( @(posedge HCLK) disable iff (!HRESETn)
|
||||||
((gpio_dir == 16'h0001)
|
((HADDR[7:0] == gpio_data_addr)
|
||||||
&& (HADDR[7:0] == gpio_data_addr)
|
|
||||||
&& HSEL
|
&& HSEL
|
||||||
&& HWRITE
|
&& HWRITE
|
||||||
&& HTRANS[1])
|
&& HTRANS[1]
|
||||||
|-> (GPIOOUT[15:0] == $past(HWDATA[15:0], 1))
|
&& HREADY) |-> ##1
|
||||||
|
(gpio_dir == 16'h0001) |-> ##1
|
||||||
|
(GPIOOUT[15:0] == $past(HWDATA[15:0], 1))
|
||||||
);
|
);
|
||||||
|
|
||||||
assert_gpio_read: assert property
|
assert_gpio_read: assert property
|
||||||
( @(posedge HCLK) disable iff (!HRESETn)
|
( @(posedge HCLK) disable iff (!HRESETn)
|
||||||
((gpio_dir == 16'h0000)
|
((gpio_dir == 16'h0000)
|
||||||
&& (HADDR[7:0] == gpio_data_addr)
|
&& (HADDR[7:0] == gpio_data_addr)
|
||||||
// && HSEL // HSEL not used in Read always_ff
|
// && HSEL // HSEL not used in Read always_ff
|
||||||
&& !HWRITE
|
&& !HWRITE
|
||||||
&& HTRANS[1])
|
&& HTRANS[1]
|
||||||
|-> (HRDATA[15:0] == $past(GPIOIN[15:0], 1)
|
&& HREADY) |-> ##1
|
||||||
&& HREADYOUT)
|
((HRDATA[15:0]==$past(GPIOIN[15:0],1)) && HREADYOUT)
|
||||||
);
|
);
|
||||||
|
|
||||||
assert_gpio_dir: assert property
|
assert_gpio_dir: assert property
|
||||||
|
@ -143,12 +145,14 @@ module AHBGPIO
|
||||||
((HADDR[7:0] == gpio_dir_addr)
|
((HADDR[7:0] == gpio_dir_addr)
|
||||||
&& HSEL
|
&& HSEL
|
||||||
&& HWRITE
|
&& HWRITE
|
||||||
&& HTRANS[1])
|
&& HTRANS[1]
|
||||||
|-> (gpio_dir == $past(HWDATA[15:0], 1))
|
&& HREADY) |-> ##1
|
||||||
|
((HWDATA[7:0] == 8'h00 || HWDATA[7:0] == 8'h01)) ##1 (gpio_dir == $past(HWDATA[15:0], 1))
|
||||||
);
|
);
|
||||||
|
|
||||||
assume_initial_valid: assume
|
assume_initial_valid: assume property
|
||||||
( gpio_dir == 16'h0000
|
( @(posedge HCLK)
|
||||||
|
gpio_dir == 16'h0000
|
||||||
|| gpio_dir == 16'h0001
|
|| gpio_dir == 16'h0001
|
||||||
);
|
);
|
||||||
|
|
||||||
|
|
|
@ -1,172 +1,190 @@
|
||||||
//stub
|
//stub
|
||||||
interface ahb_gpio_if;
|
interface ahb_gpio_if;
|
||||||
|
|
||||||
typedef enum bit[1:0] {
|
typedef enum bit[1:0] {
|
||||||
IDLE = 2'b00,
|
IDLE = 2'b00,
|
||||||
BUSY = 2'b01,
|
BUSY = 2'b01,
|
||||||
NONSEQUENTIAL = 2'b10,
|
NONSEQUENTIAL = 2'b10,
|
||||||
SEQUENTIAL = 2'b11
|
SEQUENTIAL = 2'b11
|
||||||
} htrans_types;
|
} htrans_types;
|
||||||
|
|
||||||
logic HCLK;
|
logic HCLK;
|
||||||
logic HRESETn;
|
logic HRESETn;
|
||||||
logic [31:0] HADDR;
|
logic [31:0] HADDR;
|
||||||
logic [1:0] HTRANS;
|
logic [ 1:0] HTRANS;
|
||||||
logic [31:0] HWDATA;
|
logic [31:0] HWDATA;
|
||||||
logic HWRITE;
|
logic HWRITE;
|
||||||
logic HSEL;
|
logic HSEL;
|
||||||
logic HREADY;
|
logic HREADY;
|
||||||
logic HREADYOUT;
|
logic HREADYOUT;
|
||||||
logic [31:0] HRDATA;
|
logic [31:0] HRDATA;
|
||||||
|
|
||||||
logic [15:0] GPIOIN;
|
logic [16:0] GPIOIN;
|
||||||
logic [15:0] GPIOOUT;
|
logic [16:0] GPIOOUT;
|
||||||
|
|
||||||
modport DUT (input HCLK, HRESETn, HADDR, HTRANS, HWDATA, HWRITE, HSEL, HREADY, GPIOIN,
|
modport DUT
|
||||||
output HREADYOUT, HRDATA, GPIOOUT);
|
( input HCLK, HRESETn, HADDR, HTRANS, HWDATA, HWRITE, HSEL, HREADY, GPIOIN,
|
||||||
|
output HREADYOUT, HRDATA, GPIOOUT
|
||||||
|
);
|
||||||
|
|
||||||
modport TB (input HCLK, HREADYOUT, HRDATA, GPIOOUT,
|
modport TB
|
||||||
output HRESETn, HREADY, HADDR, HTRANS, HWDATA, HWRITE, HSEL, GPIOIN);
|
( input HCLK, HREADYOUT, HRDATA, GPIOOUT,
|
||||||
|
output HRESETn, HREADY, HADDR, HTRANS, HWDATA, HWRITE, HSEL, GPIOIN
|
||||||
|
);
|
||||||
endinterface
|
endinterface
|
||||||
|
|
||||||
|
module ahb_gpio_tb;
|
||||||
|
localparam [7:0] gpio_data_addr = 8'h00;
|
||||||
|
localparam [7:0] gpio_dir_addr = 8'h04;
|
||||||
|
localparam max_test_count = 1000;
|
||||||
|
|
||||||
program automatic ahb_gpio_tb
|
logic parity_sel = '0;
|
||||||
(ahb_gpio_if.TB gpioif);
|
integer test_count;
|
||||||
|
|
||||||
localparam [7:0] gpio_data_addr = 8'h00;
|
ahb_gpio_if gpioif();
|
||||||
localparam [7:0] gpio_dir_addr = 8'h04;
|
AHBGPIO gpio(
|
||||||
localparam max_test_count = 1000;
|
.HCLK (gpioif.HCLK),
|
||||||
integer test_count;
|
.HRESETn (gpioif.HRESETn),
|
||||||
|
.HADDR (gpioif.HADDR),
|
||||||
|
.HTRANS (gpioif.HTRANS),
|
||||||
|
.HWDATA (gpioif.HWDATA),
|
||||||
|
.HWRITE (gpioif.HWRITE),
|
||||||
|
.HSEL (gpioif.HSEL),
|
||||||
|
.HREADY (gpioif.HREADY),
|
||||||
|
.GPIOIN (gpioif.GPIOIN),
|
||||||
|
.PARITYSEL (parity_sel),
|
||||||
|
.INJECT_FAULT ('0),
|
||||||
|
.HREADYOUT (gpioif.HREADYOUT),
|
||||||
|
.HRDATA (gpioif.HRDATA),
|
||||||
|
.GPIOOUT (gpioif.GPIOOUT),
|
||||||
|
.PARITYERR ()
|
||||||
|
);
|
||||||
|
|
||||||
class gpio_stimulus;
|
class gpio_stimulus;
|
||||||
typedef enum bit[1:0] {
|
rand logic HSEL;
|
||||||
GPIO_WRITE = 2'b00,
|
rand logic HWRITE;
|
||||||
GPIO_READ = 2'b01,
|
rand logic HREADY;
|
||||||
GPIO_DIR = 2'b10,
|
rand logic [ 1:0] HTRANS;
|
||||||
RANDOM = 2'b11
|
rand logic [31:0] HWDATA;
|
||||||
} stimulus_op;
|
rand logic [31:0] HADDR;
|
||||||
rand stimulus_op gpio_op;
|
rand logic [16:0] GPIOIN;
|
||||||
|
|
||||||
rand logic HSEL;
|
logic [31:0] prev_haddr = '0;
|
||||||
rand logic HWRITE;
|
|
||||||
rand logic HREADY;
|
|
||||||
rand logic [1:0] HTRANS;
|
|
||||||
|
|
||||||
rand logic [31:0] HWDATA;
|
|
||||||
rand logic [31:0] HADDR;
|
|
||||||
|
|
||||||
rand logic [15:0] GPIOIN;
|
constraint c_hsel
|
||||||
|
{ HSEL dist { 1 :=99, 0:=1 }; }
|
||||||
|
constraint c_hready
|
||||||
|
{ HREADY dist { 1 :=99, 0:=1 }; }
|
||||||
|
constraint c_htrans
|
||||||
|
{ HTRANS dist { 2'b10 :=90, HTRANS :=10};}
|
||||||
|
constraint c_haddr
|
||||||
|
{ HSEL -> HADDR dist {gpio_data_addr:=40, gpio_dir_addr:=40, HADDR:=20};}
|
||||||
|
constraint c_gpio_dir_write
|
||||||
|
{
|
||||||
|
(prev_haddr[7:0]==gpio_dir_addr) -> (HWDATA==32'h0000 || HWDATA ==32'h0001);
|
||||||
|
}
|
||||||
|
constraint c_gpioin_parity
|
||||||
|
{ GPIOIN[16] == ~^{GPIOIN[15:0],parity_sel};}
|
||||||
|
|
||||||
constraint c_haddr {((gpio_op == GPIO_WRITE) && (HADDR == gpio_data_addr)) ||
|
function void post_randomize;
|
||||||
((gpio_op == GPIO_DIR) && (HADDR == gpio_dir_addr)) ||
|
prev_haddr = HADDR;
|
||||||
(gpio_op == GPIO_READ) ||
|
endfunction
|
||||||
(gpio_op == RANDOM);}
|
endclass
|
||||||
|
|
||||||
constraint c_write {((gpio_op == GPIO_WRITE)|| (gpio_op == GPIO_DIR)) -> (HSEL && HWRITE && HREADY && (HTRANS == 2'b10));}
|
gpio_stimulus stimulus_vals;
|
||||||
|
|
||||||
constraint c_read {(gpio_op == GPIO_READ) -> (HSEL && !HWRITE && HREADY);}
|
covergroup cover_ahb_transaction_vals;
|
||||||
endclass
|
cp_hsel: coverpoint gpioif.HSEL{
|
||||||
|
bins hi = {1};
|
||||||
|
bins lo = {0};
|
||||||
|
}
|
||||||
|
cp_hready: coverpoint gpioif.HREADY{
|
||||||
|
bins hi = {1};
|
||||||
|
bins lo = {0};
|
||||||
|
}
|
||||||
|
cp_hwrite: coverpoint gpioif.HWRITE{
|
||||||
|
bins write = {1};
|
||||||
|
bins read = {0};
|
||||||
|
}
|
||||||
|
cp_haddr: coverpoint gpioif.HADDR {
|
||||||
|
bins data_addr = {gpio_data_addr};
|
||||||
|
bins dir_addr = {gpio_dir_addr};
|
||||||
|
bins invalid_addr = default;
|
||||||
|
}
|
||||||
|
cp_ahb_transaction: cross cp_hsel, cp_hready, cp_hwrite, cp_haddr {
|
||||||
|
bins ahb_write = cp_ahb_transaction with (cp_hsel==1 && cp_hready==1 && cp_hwrite==1 && cp_haddr==gpio_data_addr);
|
||||||
|
bins ahb_read = cp_ahb_transaction with (cp_hsel==1 && cp_hready==1 && cp_hwrite==0);
|
||||||
|
bins ahb_dir = cp_ahb_transaction with (cp_hsel==1 && cp_hready==1 && cp_hwrite==1 && cp_haddr==gpio_dir_addr);
|
||||||
|
ignore_bins ignore_invalid = cp_ahb_transaction with (cp_hsel!=1);
|
||||||
|
}
|
||||||
|
|
||||||
gpio_stimulus stimulus_vals;
|
endgroup
|
||||||
|
|
||||||
covergroup cover_addr_values;
|
covergroup cover_ahb_write_values;
|
||||||
coverpoint gpioif.HADDR {
|
coverpoint gpioif.HWDATA;
|
||||||
bins data_addr = {gpio_data_addr};
|
endgroup
|
||||||
bins dir_addr = {gpio_dir_addr};
|
|
||||||
bins invalid_addr = default;
|
|
||||||
}
|
|
||||||
endgroup
|
|
||||||
|
|
||||||
covergroup cover_wr_vals;
|
covergroup cover_ahb_read_values;
|
||||||
coverpoint {HSEL,HWRITE,HREADY} {
|
coverpoint gpioif.HRDATA;
|
||||||
bins write = {{1,1,1}};
|
endgroup
|
||||||
bins read = {{1,0,1}};
|
|
||||||
bins invalid = default;
|
|
||||||
}
|
|
||||||
endgroup
|
|
||||||
|
|
||||||
covergroup cover_ahb_write_values;
|
covergroup cover_gpio_in_values;
|
||||||
coverpoint gpioif.HWDATA {
|
coverpoint gpioif.GPIOIN;
|
||||||
bins zero = {0};
|
endgroup
|
||||||
bins lo = {[1:7]};
|
|
||||||
bins med = {[8:23]};
|
|
||||||
bins hi = {[24:30]};
|
|
||||||
bins max = {32'hFFFF};
|
|
||||||
}
|
|
||||||
endgroup
|
|
||||||
|
|
||||||
covergroup cover_ahb_read_values;
|
covergroup cover_gpio_out_values;
|
||||||
coverpoint gpioif.HRDATA {
|
coverpoint gpioif.GPIOOUT;
|
||||||
bins zero = {0};
|
endgroup
|
||||||
bins lo = {[1:7]};
|
|
||||||
bins med = {[8:23]};
|
|
||||||
bins hi = {[24:30]};
|
|
||||||
bins max = {32'hFFFF};
|
|
||||||
}
|
|
||||||
endgroup
|
|
||||||
|
|
||||||
covergroup cover_gpio_in_values;
|
task deassert_reset();
|
||||||
coverpoint gpioif.GPIOIN {
|
begin
|
||||||
bins zero = {0};
|
gpioif.HRESETn = 0;
|
||||||
bins lo = {[1:4]};
|
@(posedge gpioif.HCLK);
|
||||||
bins med = {[5:9]};
|
@(posedge gpioif.HCLK);
|
||||||
bins high = {[10:14]};
|
gpioif.HRESETn = 1;
|
||||||
bins max = {16'hFF};
|
end
|
||||||
}
|
endtask
|
||||||
endgroup
|
|
||||||
|
|
||||||
covergroup cover_gpio_out_values;
|
initial begin
|
||||||
coverpoint gpioif.GPIOOUT {
|
cover_ahb_write_values covahbwrite;
|
||||||
bins zero = {0};
|
cover_ahb_read_values covahbread;
|
||||||
bins lo = {[1:4]};
|
cover_gpio_in_values covgpioin;
|
||||||
bins med = {[5:9]};
|
cover_gpio_out_values covgpioout;
|
||||||
bins high = {[10:14]};
|
cover_ahb_transaction_vals covahbtransactionvals;
|
||||||
bins max = {16'hFF};
|
covahbwrite = new();
|
||||||
}
|
covahbread = new();
|
||||||
endgroup
|
covgpioin = new();
|
||||||
task deassert_reset();
|
covgpioout = new();
|
||||||
begin
|
covahbtransactionvals = new();
|
||||||
gpioif.HRESETn = 0;
|
stimulus_vals = new();
|
||||||
@(posedge gpioif.HCLK);
|
deassert_reset();
|
||||||
@(posedge gpioif.HCLK);
|
|
||||||
gpioif.HRESETn = 1;
|
|
||||||
@(posedge gpioif.HCLK);
|
|
||||||
end
|
|
||||||
endtask
|
|
||||||
|
|
||||||
initial begin
|
for(test_count = 0; test_count < max_test_count;test_count++)
|
||||||
cover_addr_values covaddr;
|
begin
|
||||||
cover_ahb_write_values covahbwrite;
|
assert (stimulus_vals.randomize) else $fatal;
|
||||||
cover_ahb_read_values covahbread;
|
gpioif.HSEL = stimulus_vals.HSEL;
|
||||||
cover_gpio_in_values covgpioin;
|
gpioif.HWRITE = stimulus_vals.HWRITE;
|
||||||
cover_gpio_out_values covgpioout;
|
gpioif.HREADY = stimulus_vals.HREADY;
|
||||||
covaddr = new();
|
gpioif.HTRANS = stimulus_vals.HTRANS;
|
||||||
covahbwrite = new();
|
gpioif.HWDATA = stimulus_vals.HWDATA;
|
||||||
covahbread = new();
|
gpioif.HADDR = stimulus_vals.HADDR;
|
||||||
covgpioin = new();
|
gpioif.GPIOIN = stimulus_vals.GPIOIN;
|
||||||
covgpioout = new();
|
|
||||||
|
|
||||||
deassert_reset();
|
covahbwrite.sample();
|
||||||
|
covgpioin.sample();
|
||||||
|
covahbread.sample();
|
||||||
|
covgpioout.sample();
|
||||||
|
|
||||||
for(test_count = 0; test_count < max_test_count;test_count++)
|
covahbtransactionvals.sample();
|
||||||
begin
|
|
||||||
@(posedge gpioif.HCLK);
|
|
||||||
assert (stimulus_vals.randomize) else $fatal;
|
|
||||||
gpioif.HSEL = stimulus_vals.HSEL;
|
|
||||||
gpioif.HWRITE = stimulus_vals.HWRITE;
|
|
||||||
gpioif.HREADY = stimulus_vals.HREADY;
|
|
||||||
gpioif.HTRANS = stimulus_vals.HTRANS;
|
|
||||||
gpioif.HWDATA = stimulus_vals.HWDATA;
|
|
||||||
gpioif.HADDR = stimulus_vals.HADDR;
|
|
||||||
gpioif.GPIOIN = stimulus_vals.GPIOIN;
|
|
||||||
|
|
||||||
covaddr.sample();
|
@(posedge gpioif.HCLK);
|
||||||
covahbwrite.sample();
|
end
|
||||||
covgpioin.sample();
|
@(posedge gpioif.HCLK);
|
||||||
covahbread.sample();
|
$finish;
|
||||||
covgpioout.sample();
|
end
|
||||||
end
|
initial begin
|
||||||
@(posedge gpioif.HCLK);
|
gpioif.HCLK = 0;
|
||||||
$finish;
|
forever #1 gpioif.HCLK = ! gpioif.HCLK;
|
||||||
end
|
end
|
||||||
endprogram
|
endmodule
|
Loading…
Reference in a new issue