module Properties (
|
|
// global
|
|
input clk,
|
|
input resetn,
|
|
input [1:0] sel,
|
|
input [3:0] we
|
|
);
|
|
|
|
|
|
// Constrain reset
|
|
|
|
reg init_flag = 1;
|
|
|
|
always @(*) begin
|
|
if (init_flag) assume (!resetn);
|
|
if (!init_flag) assume (resetn);
|
|
end
|
|
|
|
always @(posedge clk)
|
|
init_flag <= 0;
|
|
|
|
|
|
default clocking
|
|
@(posedge clk);
|
|
endclocking
|
|
|
|
default disable iff (!resetn);
|
|
|
|
|
|
assert property (we[0] |=> sel == 0);
|
|
|
|
|
|
endmodule
|
|
|
|
|
|
|
|
bind TestDesign Properties i_Properties (.*);
|