-
Notifications
You must be signed in to change notification settings - Fork 122
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[SV_backend] Move global signals to the sail_toplevel
module
#886
base: sail2
Are you sure you want to change the base?
[SV_backend] Move global signals to the sail_toplevel
module
#886
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looks like the change we want in the output, but I don't think we need to pass a prepend_globals
flag through all the pretty printing functions, and we shouldn't use a global variable to track the set of global identifiers.
That does mean we need to either:
- Pass
spec_info
through the pretty printing functions - Add a separate toplevel id constructor to the SVIR AST
let global_names : StringSet.t = | ||
NameSet.fold (fun name acc -> StringSet.add (string_of_name ~zencode:false name) acc) global_lets StringSet.empty | ||
in | ||
sv_globals := Some global_names; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The point of packaging all the information this function gathers into a spec_info
structure is specifically to avoid the use of global state.
@@ -402,17 +406,19 @@ let collect_spec_info ctx cdefs = | |||
) | |||
IdSet.empty cdefs | |||
in | |||
let global_lets, global_let_numbers = | |||
let global_lets, global_let_numbers, globals = |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
If we need the ctyp
here, it would be cleaner to just turn global_lets
into a NameMap
and refactor that way rather than duplicating everything.
let pp_id_string id = | ||
let is_sv_global s = | ||
match !sv_globals with | ||
| None -> failwith "USED is_sv_global BUT sv_globals IS UNSET" |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This should use the Sail error reporting mechanism raise (Reporting.err_general l <msg>)
so it prints a message formatted in the standard way with location information.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
(Although without the global variable this function shouldn't exist)
| None -> failwith "USED is_sv_global BUT sv_globals IS UNSET" | ||
| Some smap -> StringSet.mem s smap | ||
|
||
let pp_id_string ?(prepend_globals = true) id = |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think this prepend_globals flag is pointless because Config.no_toplevel_globals
handles this.
let s = string_of_id id in | ||
if | ||
valid_sv_identifier s | ||
&& (not (has_bad_prefix s)) | ||
&& (not (StringSet.mem s Keywords.sv_reserved_words)) | ||
&& not (StringSet.mem s Keywords.sv_used_words) | ||
then s | ||
then if Config.no_toplevel_globals && is_sv_global s && prepend_globals then "`SAIL_GLOBALS." ^ s else s |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Rather than using the prepend_globals
flag and is_sv_global
this function should take spec_info
as an argument to get the information placed there (in line 553 of this PR).
let params = if m.recursive then space ^^ string "#(parameter RECURSION_DEPTH = 10)" ^^ space else empty in | ||
let prepend_globals = |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Doesn't make sense to take prepend_globals
as a parameter then immediately redefine it. I'm not sure I understand what this is trying to do anyway?
(fun last -> pp_statement ?prepend_globals:None ~terminator:(block_terminator last)) | ||
statements | ||
) | ||
| statement -> pp_statement ?prepend_globals:None ~terminator:semi statement |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
There's no need to do ?optional_argument:None
in OCaml (just omit it). I'm actually very surprised this even compiles, as I thought an optional argument was only implicitly an option type if you don't give a default value.
Thinking about it more, distinguishing toplevel ids from regular ids in the abstract syntax tree is probably the right approach, and it fits most cleanly with how the code is currently set up. |
Hello Alasdair ! When rewriting the IDs, we need to know in which module we currently are so we can decide whether to prepend references or not, there are 3 cases : Consequently, I brought this info indirectly in the I agree with separating ids vs toplevel ids with 2 different AST nodes, I think the meaning is more explicit and it also solves the above issue - in cases A and B we don't prepend simply because these are not toplevel references, and in case C they are. This way, we simply prepend all toplevel ids and don't prepend the local one and that's it, no need for However I don't know where to do this separation.
So, to implement your solution, do you think we should go with 1 or 2, or maybe something else ? Many thanks |
Issue
The Sail global variables are emitted as signals defined at the top level of the generated SystemVerilog (SV) code, rather than within an SV module. These signals are then referenced without a hierarchical path.
This can cause issues in some formal EDA tools, as these tools fail to resolve the references to these signals. Consequently, this leads to errors in signal connectivity and results in numerous waveform issues.
This problem is discussed in detail in Sail Issue #851.
Example
In the example below, the
zero_reg
signal is declared at the top level and referenced in therX
module.However, the EDA tool cannot resolve
zero_reg
because it is neither declared nor driven withinrX
.Proposed Fix
To resolve the issue, the following changes are suggested:
zero_reg
declaration from the top level.sail_toplevel
module.zero_reg
to use the hierarchical pathSAIL_GLOBALS.zero_reg
.By defining a macro like
define SAIL_GLOBALS hier.path.to.sail_toplevel.instance
, all signals can be found under thesail_toplevel module
, eliminating the unresolved hierarchical reference errors in EDA tools.Resulting Diff:
This approach ensures all global signals are encapsulated within the
sail_toplevel module
, making them accessible to the EDA tools via a defined hierarchical path.This fix can be enabled or disabled using the
--sv-no-toplevel-globals
flag.Let me know if further clarification or details are required!