Question on Assertions

SystemVerilog
1

Write at least 4 System Verilog Assertions for validating a 4bit bidirectional shift register
with active low synchronous reset.

2

In reply to Chandrika Ummidi:

Sounds like a good interview Q or a classroom quiz, please attempt answers and seek help if you are stuck.

Good luck

3

In reply to Chandrika Ummidi:

  1. Assert that the shift register initializes to all zeroes after reset:
property reset_initialization;
  reg [3:0] shift_register;
  @(posedge clk) disable iff (!reset_n)
    (shift_register == 4'b0000);
endproperty
  1. Assert that the data shifts correctly to the left when the shift_left signal is active:
property shift_left_operation;
  reg [3:0] shift_register;
  @(posedge clk) disable iff (!reset_n)
    (shift_left && !shift_right) |-> (shift_register == {shift_register[2:0], 1'b0});
endproperty

  1. Same as 2nd for right_shift_operation

  2. Assert that the shift register maintains its value when neither shift_left nor shift_right is active:

property no_shift_operation;
  reg [3:0] shift_register;
  @(posedge clk) disable iff (!reset_n)
    (!shift_left && !shift_right) |-> (shift_register == shift_register);
endproperty
4

Taking clues from what @verif_guy12 mentioned before, is this the correct implementation of properties for the below 5 scenarios.

  1. At reset the shift_register initializes to '0.
property reset_init;
  @(negedge reset_n) (shift_reg == 4h'0);
endproperty
  1. Value is maintained when neither shift_left or shift_right is set
property no_shift_op;
  @(posedge clk) disable iff (!reset_n)
  (!shift_left && !shift_right) |=> $stable(shift_reg);
endproperty
  1. Shift left
property shift_left_op;
  @(posedge clk) disable iff (!reset_n)
  (shift_left && !shift_right) |=> shift_reg == ($past(shift_reg) << 1);
endproperty
  1. Shift right
property shift_right_op;
  @(posedge clk) disable iff (!reset_n)
  (!shift_left && shift_right) |=> shift_reg == ($past(shift_reg) >> 1);
endproperty
  1. Both shift_left and shift_right cannot be active simultaneously
property no_simultaneous_shift_op;
  @(posedge clk) disable iff (!reset_n)
  !(shift_left && shift_right)
endproperty
5

Since the op mentions active low synchronous reset, the disable iff ( !reset_n ) should be removed.

property reset_initialization;
    @(posedge clk) !reset_n  |=>  shift_register == 4'b0000 ;
endproperty

For scenarios 2-5 , boolean_expression ‘reset_n && …’ should be added in the antecedent.
For example:

// 2. Value is maintained when neither shift_left or shift_right is set
property no_shift_op;
  @(posedge clk)  ( reset_n && !shift_left && !shift_right ) |=> $stable(shift_reg);
//                 ============
endproperty

Similarly ‘reset_n &&’ should be added for scenarios 3-5