peepsalot has quit [Read error: Connection reset by peer]
peepsalot has joined #yosys
unkraut has quit [*.net *.split]
lambda has quit [*.net *.split]
AdamHorden has quit [*.net *.split]
pbsds has quit [*.net *.split]
jtf has quit [*.net *.split]
unkraut has joined #yosys
lambda has joined #yosys
AdamHorden has joined #yosys
jtf has joined #yosys
pbsds has joined #yosys
Kamilion has quit [*.net *.split]
Kamilion has joined #yosys
freemint has joined #yosys
Klotz has joined #yosys
Klotz_ has joined #yosys
Klotz has quit [Ping timeout: 255 seconds]
Klotz_ is now known as Klotz
Klotz_ has joined #yosys
Klotz has quit [Ping timeout: 255 seconds]
Klotz has joined #yosys
Knarfian_____ has quit [Read error: Software caused connection abort]
Knarfian_____ has joined #yosys
Klotz_ has quit [Ping timeout: 255 seconds]
Klotz__ has joined #yosys
Klotz__ has quit [Client Quit]
Klotz_ has joined #yosys
Klotz_ is now known as kl0tz
Klotz has quit [Ping timeout: 255 seconds]
mewt has quit [Read error: Software caused connection abort]
mewt has joined #yosys
kl0tz is now known as Klotz
Klotz_ has joined #yosys
Klotz has quit [Ping timeout: 255 seconds]
Klotz_ has quit [Client Quit]
freeemint has joined #yosys
freemint__ has joined #yosys
freemint has quit [Ping timeout: 260 seconds]
freeemint has quit [Ping timeout: 268 seconds]
ec_ has quit [Remote host closed the connection]
ec_ has joined #yosys
freeemint has joined #yosys
ec_ has quit [Remote host closed the connection]
freemint__ has quit [Ping timeout: 256 seconds]
ec_ has joined #yosys
freemint__ has joined #yosys
freeemint has quit [Read error: Connection reset by peer]
leocassarani has joined #yosys
<leocassarani>
Hey folks, I've been trying to get to grips with formal verification for my hobby CPU. I was asking this in the 1BitSquared Discord but I thought I'd try here too — basically I'm just not sure how to approach writing formal models for each of the instructions that my CPU supports, particularly when the instructions are multi-cycle or indeed
<leocassarani>
larger than a single word of memory (and therefore need multiple cycles just to read the operands). Originally I tried an approach where I would use $past(…), $past($past(…)) etc to specify the state of various signals from the point of view of the cycle when the instruction finally retired. But for example looking at riscv-formal, that doesn't
<leocassarani>
seem to be a common approach. So the alternative might be to write a model for each step of the instruction and define what the signals should be based on the cycle count. Does anyone have any thoughts or pointers on how I should approach this?
leocassarani has quit [Quit: Ping timeout (120 seconds)]
leocassarani has joined #yosys
leocassarani has quit [Quit: Ping timeout (120 seconds)]
leocassarani has joined #yosys
freemint has joined #yosys
freemint__ has quit [Ping timeout: 256 seconds]
leocassarani has quit [Quit: Ping timeout (120 seconds)]
leocassarani has joined #yosys
leocassarani has quit [Quit: Client closed]
leocassarani has joined #yosys
leocassarani has quit [Remote host closed the connection]