Induction example for https://imgur.com/a/MMr3c

shift_register_compare.v

/*
Assumption #1: assume(i_ce) requires 16 steps, 
Assumption #2: always @(posedge i_clk) if (!$past(i_ce)) assume(i_ce); should take 16*2, 
Assumption #3: always @(posedge i_clk) if ((!$past(i_ce))&&(!$past(i_ce,2))) assume(i_ce); should require 16 * 3 = 48 steps.
 
Here's what's going on: there are 16 values in that shift register.  It takes i_ce being high to flush one more stage through the assertion.  If assume(i_ce), then it will take about 16 clocks to flush the state in the shift register until sa == sb;                                                                                
 
if you do an always @(posedge i_ce) if (!$past(i_ce)) assume(i_ce); then there will never be more than one cycle between times when i_ce is high.                    
 
The induction engine is going to prove us wrong, so it will stretch out the distance between the i_ce's as far as it can.  If we require that it cannot stretch out by more than 2 samples, then it can only stretch out the time to prove all of the shift register elements to 32 clocks at the most (16 shift register elements, times maximum two clocks per i_ce)  
 
Imagine you have data coming in at a rate that isn't synchronous to your clock, although it has since been synchronized.
 
For example, suppose the data is coming in at somewhere between 50% and 100% of your clock rate.                                                                    Then the i_ce line will need to be high anytime you have new data, and that will be more than 50% of the time.                                                       
 
This is assumption #2.  Assumption #3 is the same, only the input clock rate would now be between 33% and 100% of the system clock rate.                             
Assumption #2 just means i_ce will be on somewhere between 50% and 100% of the time.                                                                                 Assumption #3: 33-100%  
 
*/

module shift_register_compare(clk, i_ce, i_bit);

input clk;
input i_ce;
input i_bit;

parameter SHIFT_REG_LENGTH = 15;

reg[SHIFT_REG_LENGTH:0] sa;
reg[SHIFT_REG_LENGTH:0] sb;

initial sa = 0;
initial sb = 0;

always @(posedge clk)
	if(i_ce)
		sa <= { sa[(SHIFT_REG_LENGTH-1):0] , i_bit };

always @(posedge clk)
	if(i_ce)
		sb <= { sb[(SHIFT_REG_LENGTH-1):0] , i_bit };

always @(*)
	assert(sa[SHIFT_REG_LENGTH] == sb[SHIFT_REG_LENGTH]);

always @(*) 
//	if (!$past(i_ce)) 
	assume(i_ce); 

endmodule