I am trying to use constraint random data generator inside property as:
package my_pkg;
class tr_gen;
rand bit[1:0] bsz;
rand bit[31:0] s_addr[];
rand bit[31:0] e_addr[];
rand bit[2:0] bl;
bit[31:0] addr_4KB_msk = ~((32'('h1) << 12)-1);
rand bit[5:0] num;
constraint c_tr_n {
s_addr.size() == (num+1); // number of transactions
e_addr.size() == s_addr.size();
}
constraint c_s_addrs {
foreach(s_addr[it]) if(it>0) {
s_addr[it] == s_addr[it-1]+((bl+1)*(2**bsz)); // consecutive start addr = addr + total num bytes in transasction
}
}
constraint c_e_addrs {
foreach(e_addr[it]) if(it>0) {
e_addr[it] == e_addr[it-1]+((bl+1)*(2**bsz)-1); // end addr = start addr + total num bytes in transaction - 1
}
}
constraint c_4kb_boundary {
foreach(s_addr[it]) {
(s_addr[it] & addr_4KB_msk) == (e_addr[it] & addr_4KB_msk); // for every transaction ensure 4kb boundary
}
}
constraint c_s_addr_byte_align {
foreach(s_addr[it]) {
bsz == 1 -> s_addr[it][0:0] = 0; // 2 byte
bsz == 2 -> s_addr[it][1:0] = 0; // 4 byte
bsz == 3 -> s_addr[it][2:0] = 0; // 8 byte
}
}
endclass
typedef struct packed {
bit[1:0] bsz;
bit[31:0] addr;
bit[2:0] bl;
} pkt_t;
endpackage
module try(input[31:0] addr_in);
bit clk;
initial begin
clk = 1'b0;
end
always #5 clk = ~clk;
function my_pkg::pkt_t eval_pkt();
my_pkg::tr_gen tr;
my_pkg::pkt_t pkt;
tr = new();
tr.randomize with{ num == 5; };
pkt.bsz = tr.bsz;
pkt.addr = tr.s_addr[0];
pkt.bl = tr.bl;
return pkt;
endfunction
property p;
my_pkg::pkg_t local_pkt;
@(posedge clk)
((1, local_pkt=eval_pkt()) |-> (addr_in == local_pkt.addr));
endproperty
endmodule
Above code I am running in FORMAL, but seems I am unable to use class based randomization there.
If it’s a limitation by formal tool, any suggestion how to achieve above randomization using usual assumes?