Surelog Not Flagging Missing Time Delays, and Undefined Property References

[Divya2030]

Original Tests Link
clock_divider_original.zip

1. Property missing delay operator (##8) passes without error on line 39 clock_divider.sv
clock_divider_ex2.zip

property p_clk_out_toggle;
        @(posedge clk)
        !reset && clk_out |->  !clk_out;
endproperty

2. Surelog does not detect error for assertion of commented-out property
clock_divider_ex3.zip
I encountered unexpected behavior when working with a property in my clock_divider.sv code. Specifically, I had:
a. Commented out a property (p_clk_out_toggle in my code).
b. Left the corresponding assert property statement active and uncommented.
Given this configuration, I expected Surelog to raise an error due to the reference to the undefined (commented-out) property. However, Surelog did not flag any issues.

// Property: clk_out should toggle every 8 input clock cycles (assuming reset has not been asserted)
//property p_clk_out_toggle;
//  @(posedge clk)
//  !reset && clk_out |->  !clk_out;
// endproperty

assert property (p_clk_out_toggle);

[alaindargelas]

This is the UHDM tree generated by Surelog:

|uhdmtopModules:
\_module_inst: work@test (work@test), id:7, file:/home/alain/Surelog/tests/ScratchPad.sv, line:1:1, endln:3:10
  |vpiName:work@test
  |vpiDefName:work@test
  |vpiTop:1
  |vpiAssertion:
  \_assert_stmt: (work@test), id:8, line:2:2, endln:2:37
    |vpiParent:
    \_module_inst: work@test (work@test), id:7, file:/home/alain/Surelog/tests/ScratchPad.sv, line:1:1, endln:3:10
    |vpiFullName:work@test
    |vpiProperty:
    \_property_spec: , id:9, line:2:19, endln:2:35
      |vpiParent:
      \_assert_stmt: (work@test), id:8, line:2:2, endln:2:37
      |vpiPropertyExpr:
      \_ref_obj: (work@test.p_clk_out_toggle), id:10, line:2:19, endln:2:35
        |vpiParent:
        \_property_spec: , id:9, line:2:19, endln:2:35
        |vpiName:p_clk_out_toggle
        |vpiFullName:work@test.p_clk_out_toggle
        |vpiActual:
        \_logic_net: (work@test.p_clk_out_toggle), id:6, line:2:19, endln:2:35

You can see that in the absence of a property definition Surelog created a logic_net.
You can write a Linter rule in the UHDM Linter:
https://github.com/chipsalliance/UHDM/blob/master/templates/UhdmLint.cpp

To detect such an incorrect type binding.

[Divya2030]

@alaindargelas Thank you for pointing out the logic_net creation in the absence of a property definition. I understand that creating a linter rule in the UHDM Linter can help in detecting such incorrect type bindings.
Before starting with the creation of the Linter rule, I need to have a deep understanding of the functionalities and structures of UHDM and Surelog.

I'm currently working on providing additional examples to highlight and tackle several other Surelog issues.

Ex1.zip
Ex2.zip

[Divya2030]

Assertion Failures in Version 1.74 (Sep 13, 2023) During Property Verification with ##delay, assertions operators, sequences.

Surelog_Assertions_examples.zip

[alaindargelas]

Property_decls are now modeled.
Next are Sequence_Decls

[alaindargelas]

Sequence support has been added to UHDM.
Some tests are still failing (Unsupported expression), will address.

[alaindargelas]

@Divya2030 , please check the current support.

[alaindargelas]

@Divya2030 all examples provided generate the correct UHDM model.
surelog ..... -d uhdm to see the text (debug) output of UHDM

What is next?

[Divya2030]

@alaindargelas

Version: 1.75
Build Date: Oct 3, 2023

Examples that were expected to fail in Surelog during property verification with ##delay did not produce any failures. Additionally, an error with bind instance was encountered.

Examples:
Surelog_v1.75_examples.zip

[alaindargelas]

@Divya2030 ,

Regarding assert property (p_clk_out_toggle);, there is a new linting check that reports the missing property binding.

Regarding Ex1.zip, you forgot to give all the files on the command line, you need to specify all the verilog files, then the compilation error goes away.
Also Surelog is not a simulator, it cannot evaluate the assertion at runtime. Do not expect the kind of error you get from a simulator.

Regarding Ex2.zip, I added a new linting check that reports the same errror about misuse of sequence.