Comments (5)
do you remember why this check is happening before rwire inlining and not after? is it for historical reasons because it happened in the dark ages when rwires were not being inlined?
conversely it seems that the inlining happens after astate, which seems like a pretty intentional place to do this; does it have to go after that?
from bsc.
Inlining happens in the Verilog backend (which starts with astate
). We perform the assertion check before the backend split, because we want to perform the check when generating Bluesim as well.
In the early days, the check for always_ready
was to look at the expression for the RDY signal and see that it is the constant 1. This only worked if BSC's optimization rules were powerful enough to reduce the expression to 1 (which it wasn't always able to do). (And we might even have done this only in the Verilog backend and not for Bluesim.) Now we use an SMT solver, and ask it whether the expression is implied to be always True by what we know of the design. (And this is a query that we can do right after scheduling.) The SMT solver is quite powerful, so it is not necessary to wait until later in BSC when optimizations may simplify the expression. However, the SMT solver doesn't have information about the internal connections of wire modules, which inlining would expose. It should be easy to provide to the SMT solver -- this isn't a big project.
I don't think that inlining can be brought forward, to before the backend split, because Bluesim operates on the design in terms of modules and rules. The astate
stage converts from rules into the wires that implement them. Inlining happens afterward because it is just creating a wire assignment RDY_out = EN_in
(and also out = in
for the data). The astate
stage has created the EN signals, as a combination of the conditions (CAN_FIRE) of rules that write to the module and the scheduling logic (WILL_FIRE). The RDY signal from wire is only discovered to be 1 when the enable signal is 1, which is when the combination of rule conditions and scheduling are brought together and simplify to 1. Fortunately, the SMT solver is doing this, but it's doing it at the abstraction level of rule conditions. It just needs to know the internal connections of wire/creg modules, which should be easy to provide.
from bsc.
ah right, i totally forgot about bluesim. and i guess bluesim needs this b/c it can't turn the rwire inside out and make it into an expression, which i guess is kinda the whole point of an rwire? hmm.
are you thinking of specialcasing this in the SMT generation (which would need to match the InlineWires code), or an annotation (or rewriting rule?) that would be common to both?
from bsc.
I was going to add special knowledge about the primitive modules RWire
, RWire0
, BypassWire
, BypassWire0
, CrossingBypassWire
, CRegN5
, CRegUN5
, and CRegA5
to the code that translates an ASyntax module into SMT equations. Yes, this would need to be kept in sync with the various other pieces that implement these primitives, such as the import-BVI, the Verilog module, and the inlining code. I don't have any ideas on how to unify these from a common source, but I don't think my proposal prevents doing that in the future if we figure out how. (An import-BVI already specifies pairs of in/out ports that have a combinational path; maybe that could be extended to optionally specify the exact logic along the path. Note, though, that for CReg and registers, there's of course more to inlining than just combinational paths --- reg, always block, initial block, etc.)
I do think that we'll want to allow users to specify additional information that they know about a design, to the SMT solver, to use in analysis (including scheduling). (For example, things like: two input ports never have the same value.) I have no idea what that would look like, but I wonder if this info about primitive submodules could be represented using that feature, if it existed. Here, again, I don't think that my proposal prevents doing that in the future.
from bsc.
IIRC Verilog-imported modules have a combinational path annotation that is used to detect combinational loops; I was musing that perhaps that could be extended to capture this as well. I guess the objectives are different, though: if you had some expression syntax you could convert to SMT, then in one case you'd be prepared to underapproximate and in the other to overapproximate (to stay conservative in each case), so maybe not?
But yeah I agree hacking it in for now as you suggest is the right thing to do; the issue is pretty ugly when one runs into it, and I think wires are probably the main use case anyway.
from bsc.
Related Issues (20)
- Verilog import fails in macro substitution HOT 2
- Unexpected syntax error HOT 1
- expandPorts.tcl has hardcoded paths which do not exist. HOT 1
- Unexpected behavior in Stmt sequence when using par HOT 2
- Bluesim divide-by-zero behavior is inconsistent on arm64 HOT 2
- Type synonyms with phantom parameters can lead to strange behaviors (E.g., compiler hang) HOT 4
- doc example for mkUniqueWrapper2 HOT 7
- -remove-unused-modules flag doesn't work with mkProbe module provided in std library HOT 2
- Failures with compilation on raspberry-pi 5 HOT 4
- GCC 14 emits extra warnings HOT 1
- Github's macos-11 runner is going away HOT 1
- [Bluesim] Simulation executable fails with `undefined symbol: _Z21vcd_write_scope_startP9tSimStatePKc` HOT 9
- `sqrtFP` is incorrect HOT 6
- compile to verilog, convert function to function, but not to modules. HOT 1
- Preserving structure at synthesis boundaries HOT 2
- Better control of wrapper generation HOT 6
- Incremental compilation model and UX improvements
- how does bsc disambiguate between V2K keywords and library functions? HOT 2
- Debugging with Bluetcl - displaying values
- implicit pack/unpack + custom Bits instance can result in extraneous logic. HOT 1
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from bsc.