lutsabound has quit [Quit: Connection closed for inactivity]
dh73 has joined #yosys
dh73 has quit [Quit: Leaving.]
_whitelogger has joined #yosys
_whitelogger has joined #yosys
emeb_mac has quit [Quit: Leaving.]
Twix has quit [Ping timeout: 265 seconds]
Jybz has joined #yosys
kraiskil has quit [Ping timeout: 258 seconds]
_whitelogger has joined #yosys
_whitelogger has joined #yosys
kraiskil has joined #yosys
kraiskil has quit [Ping timeout: 258 seconds]
kraiskil has joined #yosys
_whitelogger has joined #yosys
kraiskil has quit [Ping timeout: 260 seconds]
rombik_su has joined #yosys
kraiskil has joined #yosys
rombik_su has quit [Ping timeout: 265 seconds]
vidbina has joined #yosys
maikmerten has joined #yosys
<maikmerten>
it's that season of the year where the blessings of formal verification look particularly bright - finally trying to prove some properties of my designs.
<maikmerten>
starting with an ALU
<maikmerten>
I find that some checks on combinatorial logic is easier than I thought
<maikmerten>
('result' is a reg[31:0] that receives values on posedge)
<maikmerten>
s/is easier/are easier
<ZipCPU>
maikmerten: I'm not sure that second block checked what you wanted
<ZipCPU>
The key issue is the idea of $past() --- you want to assert if I_en was true on one clock cycle and I_aluop == `ALUOP_ADD on that same cycle, then result == I_dataS1+I_dataS2 on the next cycle
<ZipCPU>
Or ... am I missing something? 'Cause that's not what you've written
kraiskil has quit [Ping timeout: 265 seconds]
<maikmerten>
ZipCPU, yeah, basically if on the preceding posedge I_en was asserted with an ADD-aluop and with values dataS1 and dataS2, then on the current posedge the result should be the sum of the previous input values
<maikmerten>
and yes, multiclock, for no particular reason...
<maikmerten>
so much copy paste, so little insight ;)
<ZipCPU>
Ok, let's take that back out, so remove "multiclock on" and remove any assumptions about your clock within your design. This works if 1) you only have one clock, and 2) you only transition on it's positive edge
<ZipCPU>
If you do otherwise, then we'll need to work a little harder
<ZipCPU>
Are you using $global_clock in your design at all?
<ZipCPU>
If so ... I'd have you remove that as well. (Again, assuming only one continuous clock, and all transitions on its positive edge)
<maikmerten>
no $global_clock
<ZipCPU>
How about clocks and clock edges? Are you using only the one edge of one clock?
<maikmerten>
in that design, I only use posedge I_clk to do stuff
<ZipCPU>
Ok, good ... let's keep going with removing "multiclock on" then
<maikmerten>
it's constant zero, which is ALUOP_ADD
<ZipCPU>
Also be aware, when using a test in a clocked logic block, the error will be one step prior to the final step of the trace. In this case, your error is that the MSB is set.
<ZipCPU>
How about I_reset?
<maikmerten>
constant zero
<ZipCPU>
Hmm ...
<ZipCPU>
How old is your Yosys distro?
<maikmerten>
git master from ~2 days ago
<maikmerten>
but quite frankly, I'll assume I messed up before assuming this really is a yosys thing
<ZipCPU>
And your yices distro?
<ZipCPU>
... a not unlikely assumption ...
<maikmerten>
Yices 2.6.1
<maikmerten>
Copyright Free Software Foundation, Inc.
<maikmerten>
Copyright SRI International.
<maikmerten>
Linked with GMP 6.1.2
<maikmerten>
Build date: 2019-05-17
<ZipCPU>
Ok, your yices is more recent than mine, so I'll assume that's not a problem then
<maikmerten>
fresh bugs, fresh bugs ;-)
<maikmerten>
(nah)
<ZipCPU>
Lol
<ZipCPU>
How about a verilator -Wall check, to see if you are missing anything?
* ZipCPU
steps away for lunch --will look back again later
<ZipCPU>
Also ... adding `default_nettype none should find a couple bugs too
fsasm has joined #yosys
<maikmerten>
enjoy your lunch :)
<maikmerten>
(it's not verilator, but iverilog -Wall is perfectly happy)