<pepijndevos>
I'm a bit perplexed how it can be not fully const when I just created it from a constant
<pepijndevos>
ohhhh I see... it's from something else
<pepijndevos>
oh no!
<pepijndevos>
Seems in yosys an adff takes a constant reset and in this case the reset value is not actually constant
<pepijndevos>
Would I have to do a dff+mux instead?
<daveshah>
Yosys doesn't have a first class primitive for a non constant *async* reset value
<daveshah>
A dff+mux would be the way to go for a *sync* non constant reset value
<daveshah>
But that wouldn't involve an adff in any case
<daveshah>
If you want a non constant async reset value then you'll need to use a dffsr and some steering logic
<pepijndevos>
Oh shit...
<pepijndevos>
So an Adff is an asynch d flip flop with a reset value?
<daveshah>
Yes, a dff with a constant async reset value
<daveshah>
A dffsr is a dff with both an async set and reset
<daveshah>
Not that most FPGAs that Yosys supports don't support such a primitive
emeb has joined #yosys
<pepijndevos>
If I use sync reset it's fine. Asynch reset with non-constant reset value is such an edge case I'll ignore it for now.
<daveshah>
Sounds good
<pepijndevos>
Maybe I should add a nice error message though. I see log_assert being used, but that doesn't have a message. Do I just do if() log_error?
<daveshah>
Basically, but if you have a filename and line number you should use log_file_error not log_error
<pepijndevos>
Ah, hmmm, so it'll tell the user which line... lemme check.
<daveshah>
Yeah, it's generally preferred for frontend errors
rohitksingh has joined #yosys
<GenTooMan>
Anyone know of an IDE that will work with Icarus and Yosys? I happen to be use to Eclipse but I don't expect anything their as Eclipse is SO Java centered it's hard to get a decent plugin for anything other than Java.
lutsabound has quit [Quit: Connection closed for inactivity]
<ZirconiumX>
GenTooMan: I think you expect too much of the Verilog tooling and ecosystem
rohitksingh has quit [Ping timeout: 245 seconds]
bwidawsk has quit [Quit: Always remember, and never forget; I'll be back.]
bwidawsk has joined #yosys
<pepijndevos>
How does one use symbiyosys with vhdl?
<daveshah>
I'm assuming you want to know behaviour in the commercial suite (SES). VHDL asserts are supported but at present there is no support for assumes
<daveshah>
They would have to be in a Verilog module (possibly using bind)
<pepijndevos>
I don't even know the difference between assert and assume yet. But yea, SES.
<pepijndevos>
Does VHDL have stuff like (* anyconst *)?
<daveshah>
It has attributes, yes
Laksen has quit [Quit: Leaving]
<pepijndevos>
Eh, so can you do useful stuff without assume, or do you practually have to write your testbenches in verilog?
<daveshah>
You pretty much need assume
<pepijndevos>
Alright, sad, but maybe I'll learn some actual verilog on the way...
<ZirconiumX>
What does SES provide over FOSS Yosys? Verific parser support, commercial support; what else? Out of pure curiosity.
<daveshah>
Verific and support are the main things, but also some things like extra formal verification IP for verifying things like AXI cores
<daveshah>
Plus everything is prebuilt in a distribution-independent way
<ZirconiumX>
That's fair enough. Presumably the money goes towards paying Clifford et al.
mithro has quit [Read error: Connection reset by peer]
mithro has joined #yosys
<pepijndevos>
I am so confused...
<pepijndevos>
Can I see a trace if the thing passed?
<daveshah>
There is no trace if the thing passed
<ZipCPU>
Unless you run cover
<daveshah>
This is true
<ZipCPU>
Using cover() you can get traces from when things pass
<pepijndevos>
How do I tell the thing to start in reset?
<daveshah>
Although it is important to remember that when FV passes, the solver has checked every possible path through the design
<ZipCPU>
You should be able to do: initial assume(i_reset);
<ZipCPU>
However, Verific doesn't support "initial" assumes or asserts (yet)
<ZipCPU>
An alternative would be to do something like: initial f_past_valid = 0; always @(posedge i_clk) f_past_valid <= 1; always @(*) if (!f_past_valid) assume(i_reset);
<pepijndevos>
Ehhhh, that's so ugly I wonder if I'm taking the wrong approach?
<ZipCPU>
The "right" answer here is to "fix" Verific.
<ZipCPU>
You could also write for the block with the assumption: assume property (@(posedge i_clk) !f_past_valid |-> i_reset);
<daveshah>
In general you need the f_past_valid for other stuff anyway, so it's not as bad is it looks
<daveshah>
Something I've thought would be fun would be a small Yosys pass that creates this logic automatically, just given the name of your reset port/signal
<pepijndevos>
Okay, I think I passed my first assertion... but without a trace how do I know it even left reset...
<ZipCPU>
daveshah: Yes. Clifford and I discussed this sort of thing last week
<ZipCPU>
I asked for an "asic" option that would throw out initial statements, assume an initial reset, and only check assertions on the next clock cycle
<daveshah>
You could also have something that automatically does the f_past_valid stuff whenever it sees $past etc
<ZipCPU>
We both agreed we *should* have an option like that, but the more we discussed it the more difficult the details turned out to be
<daveshah>
Ah
<daveshah>
pepijndevos: as ZipCPU says, this is where you probably want to use cover
<ZipCPU>
Yosys once had an option for generating a trace automatically. It might even still be there. The problem I found with that option was that the trace was typically quite irrelevant
<pepijndevos>
I see... but he also said you don't use them at the same time, so do you write two testbenches?
<ZipCPU>
No--you place cover() statements side by side with your assert()/assume() statements
<ZipCPU>
Then you run the tool twice--once in either bmc or prove mode, and once in cover mode
<pepijndevos>
ah
<pepijndevos>
So do you need to have two sby files? or can you have multiple modes?
<ZipCPU>
You can have multiple modes in the same sby file
<pepijndevos>
hm ok
<ZipCPU>
To do that, you need a [tasks] section--I typically place it at the top
<pepijndevos>
oh ok
<ZipCPU>
I also typically place two tasks under neath it. All the tasks have names you assign, but I like to pick "prf" and "cvr"
<ZipCPU>
Then on any line to be executed in prove mode, I prefix it with "prf:"
<ZipCPU>
So an assert() does anything it can to make the expression within false, a cover() is the opposite
<ZipCPU>
A cover statement will do anything to make the expression within the cover statement tru
<pepijndevos>
Right, so it'd just set the opcode to 000?
<ZipCPU>
(opcode == 3'b000) is a test for a clock cycle where thee opcode is 000
<ZipCPU>
##1 means go to the next clock cycle
<ZipCPU>
So the result would be a trace showing the opcode == 3'b000 on one cycle, but not ending 'til at least the next
<ZipCPU>
Further, the disable iff statement makes it so that it will have to pick a time when the reset value is low
<ZipCPU>
Err ... high in your case, since your resets are all using negative logic
<ZipCPU>
It'd be sort of like: always @(posedge i_clk) cover(initial_reset && $past(opcode != 3'b000) && $past(rst) && rst);
<pepijndevos>
It's bedtime for me, but my sleepy brain just doesn't get what it shows that opcode is 0, because it's just an input.
<ZipCPU>
No, sleepy brain probably gets
<ZipCPU>
gets it
<ZipCPU>
We can discuss more tomorrow if you'd like
<pepijndevos>
Gladly
<pepijndevos>
Have a nice day :)
<ZipCPU>
o/
<pepijndevos>
Last thought: In the whole CPU it would very much make sense to verify that the opcode can't change mid-instruction XD
emeb_mac has quit [Quit: Leaving.]
<ZipCPU>
Absolutely!
<ZipCPU>
Quoted from online: "I cannot understand your code because I learnt [sic] VHDL only". Poor guy. Even before I learned (some) VHDL (thanks daveshah!) I could still understand most of it.
bwidawsk has quit [Quit: Always remember, and never forget; I'll be back.]