Questions tagged [system-verilog-assertions]

An assertion sub-language within SystemVerilog. These assertions can be use in simulation and formal analysis. The syntax and usage is described in IEEE Std 1800-2017 § 16

SystemVerilog assertions is a sub-language within system-verilog that provides assertion functionality. These assertions can be use in simulation and formal analysis. The syntax and usage of SystemVerilog assertions is described in IEEE Std 1800-2017 § 16 Assertions

The two main flavors of these assertions are immediate and concurrent. Immediate assertions can be placed inline to procedural blocks (such as always and initial blocks). Concurrent assertions run outside procedural blocks and evaluate over a span of time based on a clocking signal.

181 questions

votes

2 answers

Handing reset in SystemVerilog assertions

How are the following two properties different? property p1; @(posedge clk) disable iff (Reset) b ##1 c; endproperty property p2; @(posedge clk) (~Reset & b) ##1 c; endproperty assert property (p1); assert property (p2);

system-verilog system-verilog-assertions

asked Feb 20 '14 at 19:11

Ari

7,251
11
40
70

votes

1 answer

when are assertion "disable iff" values evaluated?

For this code, I see both assertions fail. It seems that disable iff (value) is evaluated later than the expression itself. Can someone explain this. module tb(); reg clk = 1; always #5 clk = !clk; reg rst = 1; always @ (posedge clk) rst <=…

system-verilog system-verilog-assertions

asked Apr 18 '18 at 01:40

nachum

votes

1 answer

How to use throughout operator in systemverilog assertions

Here is a spec: If signal a is asserted then it must be asserted till signal b is asserted and then it should de-assert on next clock edge. I'm reading through 16.9.9 of LRM (as well as http://www.testbench.in/AS_06_SEQUENCES.html) and the way I…

system-verilog assertions system-verilog-assertions

asked Jun 08 '15 at 00:35

wisemonkey

votes

2 answers

SystemVerilog: implies operator vs. |->

Recently the question came up what the difference is between the usual implication operator (|->) and the implies operator in SystemVerilog. Unfortunately I couldn't find a clear answer yet. However, I collected the following information: From…

system-verilog system-verilog-assertions implication

asked Jul 23 '14 at 13:48

sebs

votes

1 answer

Using queues in recursive properties

I have some data from a 1 bit serial port which comes in multiples of bytes of variant lengths as such: byte expected_1 [$] = {8'hBA, 8'hDD, 8'hC0, 8'hDE}; byte expected_2 [$] = {8'h01, 8'h23, 8'h45, 8'h67, 8'h89, 8'hAB, 8'hCD, 8'hEF}; At each…

verilog system-verilog verification assertions system-verilog-assertions

asked Jun 17 '13 at 00:11

N8TRO

3,348
3
22
40

votes

3 answers

what is the difference between -> and => in system verilog assertions?

I wanted to know when to use -> and => in SVA ? Are there any differences between sequence A; req |-> ##1 gnt; endsequence and sequence B; req |=> ##1 gnt; endsequence Please let me know.. Thank you.

system-verilog assertions system-verilog-assertions

asked Oct 18 '15 at 19:22

vivek M

votes

2 answers

SVA for handshake

i am trying to write a SVA assertion for a handshake procedure. In my searches I have found the following: property p_handshake(clk,req,ack); @(posedge clk) req |=> !req [*1:max] ##0 ack; endproperty assert…

system-verilog system-verilog-assertions

asked Jul 08 '13 at 13:48

user1220086

votes

2 answers

Can I generate a number of SystemVerilog properties within a loop?

I have two packed arrays of signals and I need to create a property and associated assertion for that property that proves that the two arrays are identical under certain conditions. I am formally verifying and the tool cannot prove both full…

properties verilog system-verilog formal-verification system-verilog-assertions

asked Oct 17 '12 at 08:12

WestHamster

1,297
2
11
16

votes

1 answer

PSL assertion for variable delay pipeline

I am trying to write a PSL assertion that checks that the amount of assertions on the input match the amount of assertions on the output. For example: . On the input anything can happen at any time and the output can be asserted on any time as well.…

vhdl system-verilog verification system-verilog-assertions psl

asked Jun 04 '20 at 11:16

Maurice

votes

3 answers

how to use assertoff from test to disable assertion in side uvm object

I am looking for way to disable assert in side uvm component for certain test. Below simple code represent my env, with comment for requirement. I thought I can use $assertoff. I can modify uvm component if required additional instrumentation to…

system-verilog uvm system-verilog-assertions

asked Dec 21 '17 at 19:06

albert waissman

votes

2 answers

Scope of `define macros

This question is regarding system verilog macros. I have a top-module, sub-module and a sub-sub module. sub-sub module instantiated in sub-module instantiated in top module. If I define a macro `define abc in the sub module, will the code written…

verilog system-verilog hdl system-verilog-assertions

asked Nov 08 '16 at 10:49

vishnu varkala

votes

1 answer

Distributivity of 'or' operation in SVA

Given the two properties P1 = (R1 or R2) |-> P and P2 = (R1 |-> P) or (R2 |-> P), where R1 and R2 are sequences and P is a property, is it correct to say that P1 is equivalent to P2? I did the calculations based on the definitions of tight and…

system-verilog system-verilog-assertions

asked Aug 30 '16 at 21:44

Tudor Timi

7,453
1
24
53

votes

2 answers

system verilog assertions: Using a reg value in a repition operator

I am trying to do something like this: assert property (@(posedge clk) disable iff (!rst) a[*c] -> $rose(b)) Here c is not a 'constant' but a value coming from some bits of a register. eg: reg[4:0] which is written only once. The check is to see if…

system-verilog system-verilog-assertions

asked Jan 18 '16 at 22:07

Gaurav Gupte

votes

1 answer

Multiple Clock Assertion in Systemverilog

Here is the Design Code : module mul_clock (input clkA, clkB, in, output out); bit temp; reg x[2:0]; always @ (posedge clkA) temp <= temp ^ in; always @ (posedge clkB) x <= {x[1:0], temp}; assign out = x[2] ^…

verilog system-verilog system-verilog-assertions

asked Oct 14 '15 at 06:50

Karan Shah

1,912
1
29
42

votes

1 answer

repeating a sequence in system verilog assertion

I need to check for a sequence till end of simulation, after the initial match. property check_at_fall; @(posedge clk) $rose(enable) ##[1:$] $fell(enable) |-> ##[0:2] ch_sel_seq [*1000] ; endproperty assert_TELEMETRY : assert property…

system-verilog assertion system-verilog-assertions

asked Sep 22 '15 at 10:05

Sini

2 3

…

12 13 Next