A couple of differences between The Verific/Yosys parser and slang

[kendroe]

Consider parsing the following assertion:

gpt_update_tag_and_content: assert property (
@(posedge clk_i) disable iff (!rst_ni)
update_i.valid |=> (
$past(replace_en, 1)[0] |-> (tlb.tags_n[0] == '{asid: update_i.asid, vpn2: update_i.vpn[18+riscv::VPN2:18], vpn1: update_i.vpn[17:9], vpn0: update_i.vpn[8:0], is_1G: update_i.is_1G, is_2M: update_i.is_2M, valid: 1'b1})
&& tlb.content_n[0] == update_i.content
)
);

The construct $past(replace_en, 1)[0] causes problems in Yosys but not slang. However, I get an error flagged by slang but not Yosys for the '{said: ...} construct (error: assignment pattern target type cannot be deduced in this context). What is the issue here?

                    - Ken
                    - 

[MikePopoloski]

Can you provide a full example that reproduces the problem? Otherwise it's just random guessing on my part.

[kendroe]

Here is a sample showing the issue. Just execute run.sh. Look at the first error and the corresponding lines in sva.sh. - Ken

…

________________________________ From: Michael Popoloski ***@***.***> Sent: Monday, July 8, 2024 8:59 PM To: MikePopoloski/slang ***@***.***> Cc: Ken Roe ***@***.***>; Author ***@***.***> Subject: Re: [MikePopoloski/slang] A couple of differences between The Verific/Yosys parser and slang (Discussion #1050) Can you provide a full example that reproduces the problem? Otherwise it's just random guessing on my part. — Reply to this email directly, view it on GitHub<#1050 (comment)>, or unsubscribe<https://github.com/notifications/unsubscribe-auth/AB2KXSCAQQK4AQZDNFDVI6TZLKLMBAVCNFSM6AAAAABKNX4RFOVHI2DSMVQWIX3LMV43SRDJONRXK43TNFXW4Q3PNVWWK3TUHM4TSOBXHE3DI>. You are receiving this because you authored the thread.

[MikePopoloski]

I don't see the sample. Please just post a minimized snippet of code that I can pass to slang and observe the result.

[kendroe]

Here is a small example that illustrates the problem. I hacked the real test case to shrink it down. The assertion shown is meaningless.

        - Ken

module tlb_checker;

    logic clk_i;
    logic rst_ni;
    logic flush_i;
    logic lu_access_i;
    logic[0:0] lu_asid_i;
    logic[63:0] lu_vaddr_i;
    logic[0:0] asid_to_be_flushed_i;
    logic[63:0] vaddr_to_be_flushed_i;
    logic lu_is_2M_o;
    logic lu_is_1G_o;
    logic lu_hit_o;

    tlb tlb_i(
        .clk_i(clk_i),
        .rst_ni(rst_ni),
        .flush_i(flush_i),
        .update_i(update_i),
        .lu_access_i(lu_access_i),
        .lu_asid_i(lu_asid_i),
        .lu_vaddr_i(lu_vaddr_i),
        .asid_to_be_flushed_i(asid_to_be_flushed_i),
        .vaddr_to_be_flushed_i(vaddr_to_be_flushed_i),
        .lu_is_2M_o(lu_is_2M_o),
        .lu_is_1G_o(lu_is_1G_o),
        .lu_hit_o(lu_hit_o)
    );


// Test 1: Check for correct tag and content update on a TLB entry following an update trigger with a valid incoming update signal
gpt_update_tag_and_content: assert property (
    @(posedge clk_i) disable iff (!rst_ni) 
    lu_is_2M_o |=> (
        $past(vaddr_to_be_flushed_i, 1)[0] |-> (vaddr_to_be_flushed_i[0] == '{asid: vaddr_to_be_flushed, vpn2: vaddr_to_be_flushed[18+riscv::VPN2:18], vpn1: update_i.vpn[17:9], vpn0: update_i.vpn[8:0], is_1G: update_i.is_1G, is_2M: update_i.is_2M, valid: 1'b1})
        && tlb_i.content_n[0] == update_i.content
    )
);

endmodule

module tlb import #(
      parameter int unsigned TLB_ENTRIES = 4,
      parameter int unsigned ASID_WIDTH  = 1
  )(
    input  logic                    clk_i,    // Clock
    input  logic                    rst_ni,   // Asynchronous reset active low
    input  logic                    flush_i,  // Flush signal
    // Update TLB
    input  tlb_update_t             update_i,
    // Lookup signals
    input  logic                    lu_access_i,
    input  logic [ASID_WIDTH-1:0]   lu_asid_i,
    input  logic [riscv::VLEN-1:0]  lu_vaddr_i,
    input  logic [ASID_WIDTH-1:0]   asid_to_be_flushed_i,
    input  logic [riscv::VLEN-1:0]  vaddr_to_be_flushed_i,
    output logic                    lu_is_2M_o,
    output logic                    lu_is_1G_o,
    output logic                    lu_hit_o
);

endmodule

[MikePopoloski]

It seems like there are numerous problems with this example. I will not address them all, but the error related to assignment pattern target type cannot be deduced in this context is because you're using an assignment pattern in a context where there is no target type to create. What should be the type of the assignment pattern expression? Where do these field names (like "asid") come from? The code is not valid SystemVerilog.

[kendroe]

I suspect what you are saying is correct and Yosys for some reason doesn't flag an error. A second issue that I would like to resolve with the above example is that no error is flagged for the subexpression $past(vaddr_to_be_flushed_i, 1)[0]. This occurs before the point of the first error generated. Is this legal Verilog code? - Ken

…

________________________________ From: Michael Popoloski ***@***.***> Sent: Wednesday, July 10, 2024 8:33 AM To: MikePopoloski/slang ***@***.***> Cc: Ken Roe ***@***.***>; Author ***@***.***> Subject: Re: [MikePopoloski/slang] A couple of differences between The Verific/Yosys parser and slang (Discussion #1050) It seems like there are numerous problems with this example. I will not address them all, but the error related to assignment pattern target type cannot be deduced in this context is because you're using an assignment pattern in a context where there is no target type to create. What should be the type of the assignment pattern expression? Where do these field names (like "asid") come from? The code is not valid SystemVerilog. — Reply to this email directly, view it on GitHub<#1050 (reply in thread)>, or unsubscribe<https://github.com/notifications/unsubscribe-auth/AB2KXSD32ECDTARDOFATPWTZLSFNLAVCNFSM6AAAAABKNX4RFOVHI2DSMVQWIX3LMV43URDJONRXK43TNFXW4Q3PNVWWK3TUHMYTAMBQGQYDKNY>. You are receiving this because you authored the thread.Message ID: ***@***.***>

[MikePopoloski]

It is legal as of SystemVerilog 2023. slang allows it even when not explicitly setting the language version because it supported it from the beginning as an extension.