I am trying to assert an output bit sequence of 8 bit (e.g. 11010101),its a serial communication ,so i don’t understand how to match it with expected data ,where clock used for assertion is of time period of 1 bit with respect to data
In reply to raghav kumar:
Your question is not clear please post some more details about the question .
1)Like what is the input the DUT.
2) What is the output from DUT.
Also please add some more details of this statement “clock used for assertion is of time period of 1 bit with respect to data”
In reply to raku:
1)Like what is the input the DUT.
2) What is the output from DUT.
if (reset_n && Enable)==1 output is 11010101
clock used for assertion is of time period of 1 bit with respect to data"
as the data is serial ,so one bit per clock, and i want to use same clock for assertions
In reply to raghav kumar:
I think you meant input is parallel of 8 bit data and output in serial and i assume enable will be high for continuous eight bits of data and then go low .
Class monitor
bit [7:0] cap_value;
virtual interface _intf;
scoreboard sb;
task run_phase (uvm_phase phase);
while(1) begin
wait(_intf.enable);
get_value();
sb.compare(cap_value);
end
endtask
task get_value();
for (int i=0;i<8;i++) begin
cap_value = cap_value << 1;
cap_value[0] = _intf.output_data;
@(posedge _intf.clk);
end
endtask
endclass
class scoreboard
task compare(bit [7:0] cap_value);
if(exp_value != cap_value) $display (“error”);
endtask
endclass
module par2ser;
bit[7:0] data;
bit clk, sync, serial;
property p_data_msb2lsb; // updated
bit[7:0] v_data, v_collected;
bit[2:0] i;
@(posedge clk)(sync, v_data=data, i=0) |=> // serial output is from lsb to msb
(1, v_collected[i]=serial, i=i+1'b1)[*8] ##1 v_collected==v_data;
endproperty
property p_data_lsb2msb; // updated
bit[7:0] v_data, v_collected;
bit[2:0] i;
@(posedge clk)(sync, v_data=data, i=7) |=> // serial output is from msb to lsb
(1, v_collected[i]=serial, i=i-1'b1)[*8] ##1 v_collected==v_data;
endproperty
ap_data_msb2lsb: assert property(p_data_msb2lsb);
a_data_lsb2msb: assert property(_data_lsb2msb);
endmodule
Ben Cohen http://www.systemverilog.us/
- SystemVerilog Assertions Handbook, 3rd Edition, 2013
- A Pragmatic Approach to VMM Adoption
- Using PSL/SUGAR … 2nd Edition
- Real Chip Design and Verification
- Cmpt Design by Example
- VHDL books
In reply to ben@SystemVerilog.us:
Thanks Ben for the answer but i have one doubt .
Please explain when or if sync is high thought 8 cycles does this assertion creates multiple threads or a single thread is created.Also if multiple thread are creates whether “i” value of assertion in each thread remains different from each or all will have same value
In reply to raku:
- I made a slight mistake, which I corrected above, I missed the “1” in
(1, v_collected[i]=serial, i=i-1’b1)
property p_data_lsb2msb; // Updated
bit[7:0] v_data, v_collected;
bit[2:0] i;
@(posedge clk)(sync, v_data=data, i=7) |=> // serial output is from msb to lsb
(1, v_collected[i]=serial, i=i-1'b1)[*8] ##1 v_collected==v_data;
endproperty
Please explain when or if sync is high thought 8 cycles does this assertion creates multiple threads or a single thread is created.Also if multiple thread are creates whether “i” value of assertion in each thread remains different from each or all will have same value
I assumed that sync was one pulse, indicating the start of the serial transmission, before the first bit of data, like the one in a UART. I don’t know your design, but if sync is high for all 8 bits, then you can do something like
module par2ser;
bit[7:0] data;
bit clk, sync, serial;
property p_data_msb2lsb;
bit[7:0] v_data, v_collected;
bit[2:0] i;
@(posedge clk)($rose(sync), v_data=data, i=0) |-> // serial output is from lsb to msb
(1, v_collected[i]=serial, i=i+1'b1)[*8] ##1 v_collected==v_data;
endproperty
property p_data_lsb2msb;
bit[7:0] v_data, v_collected;
bit[2:0] i;
@(posedge clk)($rose(sync), v_data=data, i=7) |-> // serial output is from msb to lsb
(1, v_collected[i]=serial, i=i-1'b1)[*8] ##1 v_collected==v_data;
endproperty
ap_data_msb2lsb: assert property(p_data_msb2lsb);
a_data_lsb2msb: assert property(_data_lsb2msb);
In this case, there is one thread for the successful attempt. The $rose insures one successful attempt, and one thread. You have multiple threads in a successful attempt if you have in the antecedent the ORing of sequences, like
a ##[1:4] b |-> c
a ##1 b[*1:4] |-> c
Here ypou would need a first_match() lile
first_match(a ##[1:4] b) |-> c
first_match(a ##1 b[*1:4]) |-> c
Each local variable for each atteempt, when the assertion is first sampled and started, is independent of other previously threads started at previous attempts.
Local variables are “local” to the property.
Ben SystemVerilog.us