How to write an SV Assertion to check if a particular DUT register is stable when a signal say “enable” is high.
enable signal can be high for multiple clocks and might go low and become high again during the simulation.
I wanted this assertion to be alive for whole simulation time.
This assertion has to be checked on Multiple such DUT registers lets say for 2000 registers. All the 2000 registers are supposed to stay stable when enable signal is high.
can we use “generate” kind of statements here ? how to give direct access to DUT register in the assertion definition.?
do we need to replicate/copy the same assertion for 2000 registers seperately (making it bulk code) or any generic way to do this?
also can we have this assertion like
if enable is high , all 2000 registers are supposed to be stable (or)
if any register is changing , then at that point enable should be low.
// How to write an SV Assertion to check if a particular DUT register is stable when a signal say “enable” is high.
// enabble 0 0 0 1 1 1 1 1 0 1
// sig b y b b b b b b y y q q //b, y,q are values
property p_stable(sig);
@(posedge clk) enable |=> $stable(sig);
endproperty
assert property (pstable(sig));
If you have some 2000 registers declared separately, rather than in an array of regs, then you’ll to write 2000 separate assert statements.
You can use a program like AWK; AWK is a specialized language designed for text processing and typically used to extract and manipulate data from text files.
I used AWK some 30+ years ago, but perpelexity.ai maybe able to help you if you ask the right questions. Below is a link for an example. I also copied the results. I don’t know if this is correct, but the concepts is there.
EDIT: The property is declared once. AWK will duplicate the assertion statement.
Certainly! You can use AWK to search for SystemVerilog register declarations in a file and generate the required property and assert statements. Below is an example AWK script that accomplishes this task:
```awk
#!/usr/bin/awk -f
# This script searches for SystemVerilog register declarations and generates
# property and assert statements for each register.
# Regular expression to match SystemVerilog register declarations
# Assuming register declarations are in the form: "reg [width] reg_name;"
BEGIN {
# Define a pattern to match register declarations
reg_pattern = /^[ \t]*reg[ \t]+[^\[]*\[[^]]*\][ \t]+([a-zA-Z_][a-zA-Z0-9_]*)[ \t]*;/
}
{
# Check if the current line matches the register declaration pattern
if ($0 ~ reg_pattern) {
# Extract the register name using the match function
match($0, reg_pattern, matches)
reg_name = matches[1]
# Generate the property and assert statements
E*DIT: MUST DELETE THE NEXT 3 PRINT LINES*
* because the property needs to be declared once.*
print "property p_stable(" reg_name ");"
print " @(posedge clk) enable |=> $stable(" reg_name ");"
print "endproperty"
print "assert property (p_stable(" reg_name "));"
print ""
}
}
How to Use the Script
Save the Script: Save the above AWK script to a file, e.g., generate_properties.awk.
Make the Script Executable: Run the following command to make the script executable:
chmod +x generate_properties.awk
Run the Script: Use the script to process a SystemVerilog file containing register declarations:
Pattern Matching: The script uses a regular expression to match lines that declare registers. The pattern assumes that registers are declared in the format reg [width] reg_name;.
Extracting Register Name: The match function extracts the register name from the matched line.
Generating Output: For each matched register, the script prints the required property and assert statements, substituting sig with the actual register name.
Note
Assumptions: This script assumes a specific format for register declarations. You may need to adjust the regular expression if your declarations differ.
Complex Declarations: If your SystemVerilog files contain more complex register declarations (e.g., multi-line declarations or packed arrays), you may need to modify the script accordingly.
It might help to explain how the register get instantiated into the DUT. If they use a common model, you might be able to bind your assertion into every instance.