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 (.*);