Skip to content
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

Formal System: RTLIL Netlist Encoding #31

Open
ShinyKate opened this issue Jan 21, 2025 · 0 comments
Open

Formal System: RTLIL Netlist Encoding #31

ShinyKate opened this issue Jan 21, 2025 · 0 comments

Comments

@ShinyKate
Copy link
Collaborator

We need to specify how to get to a transition system starting from an RTLIL netlist. There are several corner cases that need to be considered to handle all common real world use cases:

  • Loops that are guarded by FFs
  • Loops that are guarded by multiple latches that can't be transparent simultaneously
  • Loops in word-level netlists that can disappear after bit-blasting
  • Combinational loops that will always converge to a unique value

We should define a way to represent a netlist structurally within our formal system and then define the transition system semantics of such netlists. Ideally the specified conditions under which we consider a netlists to have well defined behavior are relatively weak and well behaved under composition, even if we start out with a much more restrictive automated checks that can be easily and efficiently implemented in practice.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

1 participant