supleed2/ELEC70056-HSV-CW2
1
0
Fork 0
mirror of https://github.com/supleed2/ELEC70056-HSV-CW2.git synced 2024-12-22 21:55:48 +00:00
Code Issues Packages Projects Releases Wiki Activity

Add initial assume to AHBGPIO.sv

Browse source
This commit is contained in:
Alden0012 2022-11-08 17:27:39 +00:00
parent 0f8578e1b8
commit 4edfce0e03
1 changed files with 32 additions and 29 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

61
rtl/AHB_GPIO/AHBGPIO.sv
View file

@ -68,8 +68,6 @@ module AHBGPIO
reg last_HWRITE; reg last_HWRITE;
reg last_HSEL; reg last_HSEL;
integer i;
assign HREADYOUT = 1'b1; assign HREADYOUT = 1'b1;
// Set Registers from address phase // Set Registers from address phase
@ -115,38 +113,43 @@ module AHBGPIO
//check behaviour //check behaviour
assert_parity: assert property assert_parity: assert property
( @posedge(HCLK) disable iff (!HRESETn) ( @(posedge HCLK) disable iff (!HRESETn)
!PARITYERR; !PARITYERR
); );
assert_gpio_write: assert property assert_gpio_write: assert property
( @posedge(HCLK) disable iff (!HRESETn) ( @(posedge HCLK) disable iff (!HRESETn)
((gpio_dir == 16'h0001) ((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)) |-> (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) |-> (HRDATA[15:0] == $past(GPIOIN[15:0], 1)
&& HREADYOUT) && HREADYOUT)
); );
assert_gpio_dir: assert property assert_gpio_dir: assert property
( @posedge(HCLK) disable iff (!HRESETn) ( @(posedge HCLK) disable iff (!HRESETn)
((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)) |-> (gpio_dir == $past(HWDATA[15:0], 1))
); );
assume_initial_valid: assume
( gpio_dir == 16'h0000
|| gpio_dir == 16'h0001
);
endmodule endmodule