| *** tpb <[email protected]> has joined #yosys | 00:00 | |
| *** freemint <freemint!~freemint@2001:638:904:ffe8:339b:2f0c:7daf:5607> has quit IRC (Ping timeout: 252 seconds) | 01:13 | |
| *** peepsalot <peepsalot!~peepsalot@openscad/peepsalot> has quit IRC (Read error: Connection reset by peer) | 02:47 | |
| *** peepsalot <peepsalot!~peepsalot@openscad/peepsalot> has joined #yosys | 02:47 | |
| *** unkraut <[email protected]> has quit IRC (*.net *.split) | 05:57 | |
| *** lambda <[email protected]> has quit IRC (*.net *.split) | 05:57 | |
| *** AdamHorden <[email protected]> has quit IRC (*.net *.split) | 05:57 | |
| *** pbsds <[email protected]> has quit IRC (*.net *.split) | 05:57 | |
| *** jtf <jtf!~jtf@2601:285:8000:87::5c4> has quit IRC (*.net *.split) | 05:57 | |
| *** unkraut <[email protected]> has joined #yosys | 05:57 | |
| *** lambda <[email protected]> has joined #yosys | 05:57 | |
| *** AdamHorden <[email protected]> has joined #yosys | 05:57 | |
| *** jtf <jtf!~jtf@2601:285:8000:87::5c4> has joined #yosys | 05:57 | |
| *** pbsds <[email protected]> has joined #yosys | 06:00 | |
| *** Kamilion <[email protected]> has quit IRC (*.net *.split) | 06:21 | |
| *** Kamilion <[email protected]> has joined #yosys | 06:21 | |
| *** freemint <freemint!~freemint@2001:638:904:ffe8:339b:2f0c:7daf:5607> has joined #yosys | 08:02 | |
| *** Klotz <Klotz!~Klotzoman@gateway/tor-sasl/klotz> has joined #yosys | 09:54 | |
| *** Klotz_ <Klotz_!~Klotzoman@gateway/tor-sasl/klotz> has joined #yosys | 10:02 | |
| *** Klotz <Klotz!~Klotzoman@gateway/tor-sasl/klotz> has quit IRC (Ping timeout: 255 seconds) | 10:05 | |
| *** Klotz_ is now known as Klotz | 10:06 | |
| *** Klotz_ <Klotz_!~Klotzoman@gateway/tor-sasl/klotz> has joined #yosys | 10:10 | |
| *** Klotz <Klotz!~Klotzoman@gateway/tor-sasl/klotz> has quit IRC (Ping timeout: 255 seconds) | 10:13 | |
| *** Klotz <Klotz!~Klotzoman@gateway/tor-sasl/klotz> has joined #yosys | 10:18 | |
| *** Knarfian_____ <[email protected]> has quit IRC (Read error: Software caused connection abort) | 10:20 | |
| *** Knarfian_____ <[email protected]> has joined #yosys | 10:20 | |
| *** Klotz_ <Klotz_!~Klotzoman@gateway/tor-sasl/klotz> has quit IRC (Ping timeout: 255 seconds) | 10:21 | |
| *** Klotz__ <Klotz__!~Klotzoman@gateway/tor-sasl/klotz> has joined #yosys | 10:21 | |
| *** Klotz__ <Klotz__!~Klotzoman@gateway/tor-sasl/klotz> has quit IRC (Client Quit) | 10:22 | |
| *** Klotz_ <Klotz_!~Klotzoman@gateway/tor-sasl/klotz> has joined #yosys | 10:23 | |
| *** Klotz_ is now known as kl0tz | 10:24 | |
| *** Klotz <Klotz!~Klotzoman@gateway/tor-sasl/klotz> has quit IRC (Ping timeout: 255 seconds) | 10:24 | |
| *** mewt <[email protected]> has quit IRC (Read error: Software caused connection abort) | 10:30 | |
| *** mewt <[email protected]> has joined #yosys | 10:36 | |
| *** kl0tz is now known as Klotz | 11:07 | |
| *** Klotz_ <Klotz_!~Klotzoman@gateway/tor-sasl/klotz> has joined #yosys | 12:26 | |
| *** Klotz <Klotz!~Klotzoman@gateway/tor-sasl/klotz> has quit IRC (Ping timeout: 255 seconds) | 12:28 | |
| *** Klotz_ <Klotz_!~Klotzoman@gateway/tor-sasl/klotz> has quit IRC (Client Quit) | 12:29 | |
| *** freeemint <[email protected]> has joined #yosys | 12:48 | |
| *** freemint__ <[email protected]> has joined #yosys | 12:51 | |
| *** freemint <freemint!~freemint@2001:638:904:ffe8:339b:2f0c:7daf:5607> has quit IRC (Ping timeout: 260 seconds) | 12:51 | |
| *** freeemint <[email protected]> has quit IRC (Ping timeout: 268 seconds) | 12:54 | |
| *** ec_ <ec_!~ec@gateway/tor-sasl/ec> has quit IRC (Remote host closed the connection) | 12:57 | |
| *** ec_ <ec_!~ec@gateway/tor-sasl/ec> has joined #yosys | 12:59 | |
| *** freeemint <freeemint!~freemint@2001:638:904:ffe8:339b:2f0c:7daf:5607> has joined #yosys | 13:08 | |
| *** ec_ <ec_!~ec@gateway/tor-sasl/ec> has quit IRC (Remote host closed the connection) | 13:10 | |
| *** freemint__ <[email protected]> has quit IRC (Ping timeout: 256 seconds) | 13:11 | |
| *** ec_ <ec_!~ec@gateway/tor-sasl/ec> has joined #yosys | 13:11 | |
| *** freemint__ <freemint__!~freemint@2001:638:904:ffe8:339b:2f0c:7daf:5607> has joined #yosys | 18:16 | |
| *** freeemint <freeemint!~freemint@2001:638:904:ffe8:339b:2f0c:7daf:5607> has quit IRC (Read error: Connection reset by peer) | 18:17 | |
| *** leocassarani <leocassarani!~leocassar@cpc158785-hari22-2-0-cust327.20-2.cable.virginm.net> has joined #yosys | 18:59 | |
| 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 | 19:05 |
|---|---|---|
| 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 | 19:05 |
| 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? | 19:05 |
| *** leocassarani <leocassarani!~leocassar@cpc158785-hari22-2-0-cust327.20-2.cable.virginm.net> has quit IRC (Quit: Ping timeout (120 seconds)) | 19:50 | |
| *** leocassarani <leocassarani!~leocassar@cpc158785-hari22-2-0-cust327.20-2.cable.virginm.net> has joined #yosys | 19:55 | |
| *** leocassarani <leocassarani!~leocassar@cpc158785-hari22-2-0-cust327.20-2.cable.virginm.net> has quit IRC (Quit: Ping timeout (120 seconds)) | 20:04 | |
| *** leocassarani <leocassarani!~leocassar@cpc158785-hari22-2-0-cust327.20-2.cable.virginm.net> has joined #yosys | 20:09 | |
| *** freemint <freemint!~freemint@2001:638:904:ffe8:339b:2f0c:7daf:5607> has joined #yosys | 20:09 | |
| *** freemint__ <freemint__!~freemint@2001:638:904:ffe8:339b:2f0c:7daf:5607> has quit IRC (Ping timeout: 256 seconds) | 20:10 | |
| *** leocassarani <leocassarani!~leocassar@cpc158785-hari22-2-0-cust327.20-2.cable.virginm.net> has quit IRC (Quit: Ping timeout (120 seconds)) | 20:21 | |
| *** leocassarani <leocassarani!~leocassar@cpc158785-hari22-2-0-cust327.20-2.cable.virginm.net> has joined #yosys | 20:25 | |
| *** leocassarani <leocassarani!~leocassar@cpc158785-hari22-2-0-cust327.20-2.cable.virginm.net> has quit IRC (Quit: Client closed) | 20:31 | |
| *** leocassarani <leocassarani!~leocassar@cpc158785-hari22-2-0-cust327.20-2.cable.virginm.net> has joined #yosys | 20:40 | |
| *** leocassarani <leocassarani!~leocassar@cpc158785-hari22-2-0-cust327.20-2.cable.virginm.net> has quit IRC (Remote host closed the connection) | 22:27 | |
| *** leocassarani <leocassarani!~leocassar@cpc158785-hari22-2-0-cust327.20-2.cable.virginm.net> has joined #yosys | 22:28 | |
| *** leocassarani <leocassarani!~leocassar@cpc158785-hari22-2-0-cust327.20-2.cable.virginm.net> has quit IRC (Ping timeout: 260 seconds) | 22:33 | |
| *** leocassarani <leocassarani!~leocassar@cpc158785-hari22-2-0-cust327.20-2.cable.virginm.net> has joined #yosys | 22:39 | |
| *** leocassarani <leocassarani!~leocassar@cpc158785-hari22-2-0-cust327.20-2.cable.virginm.net> has quit IRC (Ping timeout: 240 seconds) | 22:43 | |
| *** leocassarani <leocassarani!~leocassar@cpc158785-hari22-2-0-cust327.20-2.cable.virginm.net> has joined #yosys | 22:46 | |
| *** leocassarani <leocassarani!~leocassar@cpc158785-hari22-2-0-cust327.20-2.cable.virginm.net> has quit IRC (Ping timeout: 268 seconds) | 22:53 | |
| *** leocassarani <leocassarani!~leocassar@cpc158785-hari22-2-0-cust327.20-2.cable.virginm.net> has joined #yosys | 22:56 | |
| *** nonchip <[email protected]> has quit IRC (Quit: https://quassel-irc.org - Chat comfortably. Anywhere.) | 23:04 | |
| *** nonchip <[email protected]> has joined #yosys | 23:04 | |
| *** leocassarani <leocassarani!~leocassar@cpc158785-hari22-2-0-cust327.20-2.cable.virginm.net> has quit IRC (Ping timeout: 260 seconds) | 23:04 | |
| *** leocassarani <leocassarani!~leocassar@cpc158785-hari22-2-0-cust327.20-2.cable.virginm.net> has joined #yosys | 23:06 | |
| *** leocassarani <leocassarani!~leocassar@cpc158785-hari22-2-0-cust327.20-2.cable.virginm.net> has quit IRC (Ping timeout: 268 seconds) | 23:11 | |
| *** leocassarani <leocassarani!~leocassar@cpc158785-hari22-2-0-cust327.20-2.cable.virginm.net> has joined #yosys | 23:15 | |
| *** leocassarani <leocassarani!~leocassar@cpc158785-hari22-2-0-cust327.20-2.cable.virginm.net> has quit IRC (Ping timeout: 268 seconds) | 23:22 | |
| *** leocassarani <leocassarani!~leocassar@cpc158785-hari22-2-0-cust327.20-2.cable.virginm.net> has joined #yosys | 23:23 | |
| *** leocassarani <leocassarani!~leocassar@cpc158785-hari22-2-0-cust327.20-2.cable.virginm.net> has quit IRC (Ping timeout: 268 seconds) | 23:28 | |
| *** leocassarani <leocassarani!~leocassar@cpc158785-hari22-2-0-cust327.20-2.cable.virginm.net> has joined #yosys | 23:28 | |
| *** leocassarani <leocassarani!~leocassar@cpc158785-hari22-2-0-cust327.20-2.cable.virginm.net> has quit IRC (Client Quit) | 23:29 | |
Generated by irclog2html.py 2.17.2 by Marius Gedminas - find it at https://mg.pov.lt/irclog2html/!