[Verification Target Generation] Failure to support JasperGold backend

[xfzhou01]

Describe the bug I tried to add ready signal in refinement relation file cond.json, some errors are encountered when I use JasperGold as backend.

{
    "instructions": [
        {
            "instruction" : "instr_0",
            "ready signal" : "ap_done",
            "ready bound" : 100000
        }
    ],
    "global invariants": []
}

ap_done is a ready signal output by the RTL design indicating that the execution of RTL design is finished.

However, in JasperGold, the error pop out

Summary of errors detected:
    [ERROR (VERI-1128)] wrapper.v(89): 'ap_done' is not declared
    [ERROR (VERI-1128)] wrapper.v(90): 'ap_done' is not declared
    [ERROR (VERI-1072)] wrapper.v(118): module 'wrapper' is ignored due to previous errors
ERROR (ENL034): 3 errors detected in the design file(s).

Looking into wrapper.v, I find that the ap_done signal, which is expected to be connect from output of RTL design to the signal which construct the safety property, is not connected.

top top(
    .a(__ILA_I_input_a),
    .ap_clk(clk),
    .ap_done(),
    .ap_idle(),
    .ap_ready(),
    .ap_return(ap_return),
    .ap_rst(dummy_reset),
    .ap_start(__ILA_I_ap_start),
    .b(__ILA_I_input_b),
    .c(__ILA_I_input_c)
);

To Reproduce Steps to reproduce the behavior:

1. Define a ready signal of a certain instruction in cond.json
2. Set JasperGold as backend when configuring VerilogVerificationTargetGenerator
3. Compile, generate Verilog verification target, feed it into JasperGold fpv.

Environment (please complete the following information):

• OS: Ubuntu 20.04
• Compiler gcc 9.4.0, clang 10.0.0
• Other dependencies N.A.

Additional context In do.tcl, a "prove -all" can be added to automatically run the solver.

[zhanghongce]

Try RTL.ap_done instead.

[xfzhou01]

Try RTL.ap_done instead.

Thank you for your help, I changed the cond.json to

{
    "instructions": [
        {
            "instruction" : "instr_0",
            "ready signal" : "RTL.ap_done"
        }
    ],
    "global invariants": []
}

But in wrapper.v, it comes out that it only changes the name of signal from "ap_done" to "RTL.ap_done"

89,90c89,90
< assign __EDCOND__ = (`false|| (RTL.ap_done)) && __STARTED__  ;
< assign __IEND__ = (`false|| (RTL.ap_done)) && __STARTED__ && __RESETED__ && (~ __ENDED__) ;
---
> assign __EDCOND__ = (`false|| (ap_done)) && __STARTED__  ;
> assign __IEND__ = (`false|| (ap_done)) && __STARTED__ && __RESETED__ && (~ __ENDED__) ;

[zhanghongce]

It seems that the Verilog parser didn't recognize the ap_done signal in the Verilog. I'm not sure whether you have anything like

"models": { "ILA": xxx , "VERILOG":  "top" }

in varmap.json?

I guess this might interfere with the name resolution. It seems that you use top as the instance name for Verilog? Meanwhile, the top module name is also top? Please consider change the instance name to something different from the module name, then you can try instanceName.ap_done in cond.json

If that does not work, there are other workarounds: I thought JasperGold will accept 'top.ap_done', right? If so, you can temporarily replace all occurances of ap_done to top.ap_done in wrapper.v

You can also try COSA backend, but enable the flag CosaGenJgTesterScript in _vtg_config , which will generate a jaspergold script and the wrapper.v for COSA is also usable for JasperGold.

In the long run, please consider migrating to the new target generator in this branch https://github.com/zhanghongce/ILA-Tools/tree/refinement-upgrade

[xfzhou01]

It seems that the Verilog parser didn't recognize the ap_done signal in the Verilog. I'm not sure whether you have anything like

"models": { "ILA": xxx , "VERILOG":  "top" }

in varmap.json?

I guess this might interfere with the name resolution. It seems that you use top as the instance name for Verilog? Meanwhile, the top module name is also top? Please consider change the instance name to something different from the module name, then you can try instanceName.ap_done in cond.json

If that does not work, there are other workarounds: I thought JasperGold will accept 'top.ap_done', right? If so, you can temporarily replace all occurances of ap_done to top.ap_done in wrapper.v

You can also try COSA backend, but enable the flag CosaGenJgTesterScript in _vtg_config , which will generate a jaspergold script and the wrapper.v for COSA is also usable for JasperGold.

In the long run, please consider migrating to the new target generator in this branch https://github.com/zhanghongce/ILA-Tools/tree/refinement-upgrade

Thank you so much for your help! My design is actually topped by module "top", after changing "ap_done" to "top.ap_done", the name changing happened and there will be no syntax error in JasperGold.