Tom Hawkins wrote:
Just another [not so small] Icarus request...
It would be great if I could extract comment pragmas -- particularly PSL assertions -- from Verilog source code. InFormal can process separate PSL files, but most designers prefer to embed PSL directly in the RTL, such as:
module my_module (clk, req, ack); input req; output ack;
/* RTL ... */
// psl CHECK_ACK: assert // always (req -> next[3] ack) @ (posedge clk);
/* psl CHECK_REQ : assert always {req; [*5:8]; req} @ (posedge clk); */
endmodule
All I would need from the associated scope object would be either one combined string of all pragmas in the module, or an array of strings, one for each pragma.
A preprocessor perhaps? Can you give an example of how you'd specify this as an external PSL file?
Evan
