I’m working on a Formal and Working on writing a particular sequence as assumption values for a given address input but it’s leading to Error/ Over constraint issue.
//So, the sequence looks like this-
//Start any Formal stimulus input to this address in this manner -
rmbus_addr: assume property (
@(posedge clk) disable iff (~rst_n)(
1'b1 |-> //To trigger is from the get-go
// Give Value A ##Wait 10 clk cycles next Value 0 for 20 clk cycles
(addr == 'hA) [*10] ##1 (addr == 0) [*20] ##1
// Next Value B ##Wait 10 clk cycles next Value 0 for 20 clk cycles
(addr == 'hB) [*10] ##1 (addr == 0) [*20] ##1
//Next value C ## wait 10 clk cycles next value 0 for 20 clk cycles
(addr == 'hC) [*10] ##1 (addr == 0) [*20] ##1
//Finally, value should be picked from inside {set of addresses} till the end of simulation
(addr inside {
'h0,'h1,'hD...etc..etc }) [*0:$] ) ); // till the end of the bounds
I tried many things in the place of 1’b1 like using (rst == 1) etc ; i need suggestions.