In reply to ben@SystemVerilog.us:
Hi Ben,
I have not seen any example with the always block inside the checker. This would help some as the checker would only be active after the qualifiers. Is there is an example you can send.
disable iff(t_rst|| !t_pwm_row_en)
$rose(t_pwm_start) |->
I build the simpler checker with an always block for a faction of the design and am waiting for it to complete simulation in order to see the memory usage, but it is really slowing down the simulation.
Many conditions are checked for the test cases with a known relationship of the low and high times for the PWM signal (property below). This might need to be good enough.
// BIT0, D*, DB* are localparam
property p_pwm_value(t_pwm_clk_misp, t_pwm_clk, t_pwm_start, t_pwm_pin, t_pwm_value) ;
@(posedge t_pwm_clk_misp)
disable iff(t_rst || !t_pwm_row_en)
$rose(t_pwm_start) |->
(t_pwm_pin==BIT0) [*D0] ##1 (t_pwm_pin==t_pwm_value[0]) [DB0] ##1
(t_pwm_pin==BIT0) [(D1-1):D1] ##1 (t_pwm_pin==t_pwm_value[1]) [*DB1] ##1
(t_pwm_pin==BIT0) [*D2] ##1 (t_pwm_pin==t_pwm_value[2]) [*DB2] ##1
(t_pwm_pin==BIT0) [*D3] ##1 (t_pwm_pin==t_pwm_value[3]) [DB3] ##1
(t_pwm_pin==BIT0) [(D4-1)] ##1 (t_pwm_pin==t_pwm_value[4]) [*DB4] ##1
(t_pwm_pin==BIT0) [*D5] ##1 (t_pwm_pin==t_pwm_value[5]) [DB5] ##1
(t_pwm_pin==BIT0) [(D6-1)] ##1 (t_pwm_pin==t_pwm_value[6]) [*DB6] ##1
(t_pwm_pin==BIT0) [*D7] ##1 (t_pwm_pin==t_pwm_value[7]) [DB7] ##1
(t_pwm_pin==BIT0) [(D8-1)] ##1 (t_pwm_pin==t_pwm_value[8]) [*DB8] ##1
(t_pwm_pin==BIT0) [*D9] ##1 (t_pwm_pin==t_pwm_value[9]) [DB9] ##1
(t_pwm_pin==BIT0) [(D10-1)] ##1 (t_pwm_pin==t_pwm_value[10]) [*DB10] ##1
(t_pwm_pin==BIT0) [*D11] ##1 (t_pwm_pin==t_pwm_value[11]) [*DB11]
endproperty