Skip to content
This repository has been archived by the owner on Aug 20, 2024. It is now read-only.

SMT: memory port inout fields cannot be used as RHS expressions #2105

Merged
merged 2 commits into from
Mar 8, 2021
Merged

SMT: memory port inout fields cannot be used as RHS expressions #2105

merged 2 commits into from
Mar 8, 2021

Conversation

ekiwi
Copy link
Contributor

@ekiwi ekiwi commented Mar 5, 2021 •
edited
Loading

Turns out I screwed up and the input fields of memory ports are not supposed to be read.
This doesn't actually impact the formal backend which is ok with this.
However, this misunderstanding resulted in a bug, where VerilogMemDelays would change the value of the read enable field which the UndefinedMemoryBehaviorSpecPass was relying on.

This is a fix to #2095

Contributor Checklist

  • Did you add Scaladoc to every public function/method?
  • Did you update the FIRRTL spec to include every new feature/behavior?
  • Did you add at least one test demonstrating the PR?
  • Did you delete any extraneous printlns/debugging code?
  • Did you specify the type of improvement?
  • Did you state the API impact?
  • Did you specify the code generation impact?
  • Did you request a desired merge strategy?
  • Did you add text to be included in the Release Notes for this change?

Type of Improvement

  • bug fix

API Impact

  • none

Backend Code Generation Impact

  • fix SMT emission which was broken through an interaction between VeriogMemDelays and the Memory Undefined Behavior Pass

Desired Merge Strategy

  • squash

Release Notes

n/a

Reviewer Checklist (only modified by reviewer)

  • Did you add the appropriate labels?
  • Did you mark the proper milestone (1.2.x, 1.3.0, 1.4.0) ?
  • Did you review?
  • Did you check whether all relevant Contributor checkboxes have been checked?
  • Did you mark as Please Merge?

@ekiwi ekiwi requested a review from jackkoenig March 5, 2021 04:02
@ekiwi ekiwi force-pushed the mem-undef-read-inputs-fix branch 2 times, most recently from d3ebce1 to 1e551d3 Compare March 5, 2021 04:57
jackkoenig
jackkoenig approved these changes Mar 8, 2021
View reviewed changes
Copy link
Contributor

@jackkoenig jackkoenig left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't completely understand but from what I do gather, looks good. A couple of comments.

src/test/scala/firrtl/backends/experimental/smt/end2end/MemorySpec.scala Show resolved Hide resolved
src/main/scala/firrtl/backends/experimental/smt/random/UndefinedMemoryBehaviorPass.scala Outdated
if (isLiteral(oldValue)) {
println("TODO: better code for literal")
}
// println(s"Making: ${wire.name}")
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Delete commented code

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

thanks, good catch!

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

fixed now

@ekiwi ekiwi added this to the 1.5.0 milestone Mar 8, 2021
@ekiwi ekiwi force-pushed the mem-undef-read-inputs-fix branch from 1e551d3 to 166d3fb Compare March 8, 2021 23:26
@ekiwi ekiwi added the Please Merge Accepted PRs that are ready to be merged. Useful when waiting on CI. label Mar 8, 2021
@mergify mergify bot merged commit 29d57a6 into chipsalliance:master Mar 8, 2021
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Reviewers

@jackkoenig jackkoenig jackkoenig approved these changes

Assignees
No one assigned
Labels
Please Merge Accepted PRs that are ready to be merged. Useful when waiting on CI.
Projects
None yet
Milestone
1.5.0
Development

Successfully merging this pull request may close these issues.
2 participants
@ekiwi @jackkoenig