| *** tpb <[email protected]> has joined #yosys | 00:00 | |
| *** kristianpaul <kristianpaul!~paul@user/kristianpaul> has quit IRC (Ping timeout: 272 seconds) | 00:31 | |
| *** kristianpaul <kristianpaul!~paul@user/kristianpaul> has joined #yosys | 00:38 | |
| *** peeps[zen] <peeps[zen]!~peepsalot@openscad/peepsalot> has joined #yosys | 00:39 | |
| *** peepsalot <peepsalot!~peepsalot@openscad/peepsalot> has quit IRC (Ping timeout: 260 seconds) | 00:40 | |
| *** citypw <citypw!~citypw@gateway/tor-sasl/citypw> has joined #yosys | 02:17 | |
| *** emeb_mac <[email protected]> has quit IRC (Ping timeout: 272 seconds) | 07:04 | |
| *** cr1901_ <cr1901_!~cr1901@2601:8d:8600:911:d8c8:bf0c:2650:c47e> has joined #yosys | 08:53 | |
| *** cr1901 <cr1901!~cr1901@2601:8d:8600:911:d4a9:3ad0:fd2b:5df9> has quit IRC (Ping timeout: 260 seconds) | 08:57 | |
| *** emeb <[email protected]> has joined #yosys | 14:04 | |
| *** citypw <citypw!~citypw@gateway/tor-sasl/citypw> has quit IRC (Ping timeout: 240 seconds) | 14:08 | |
| *** FabM <FabM!~FabM@2a03:d604:103:600:f3e:3e6c:372d:a535> has joined #yosys | 14:19 | |
| *** cr1901_ is now known as cr1901 | 14:35 | |
| *** preyalone <[email protected]> has joined #yosys | 15:10 | |
| *** kristianpaul <kristianpaul!~paul@user/kristianpaul> has quit IRC (Ping timeout: 256 seconds) | 15:31 | |
| *** kristianpaul <kristianpaul!~paul@user/kristianpaul> has joined #yosys | 16:47 | |
| josuah | wow, wow, wow, hang-on! | 17:02 |
|---|---|---|
| josuah | all suddenly, yosys asks me if I have been adopted | 17:02 |
| josuah | is it something every hardware developer run through? | 17:03 |
| josuah | it seems like one of these corner stone in circuit design is k-induction for verifying designs | 17:04 |
| josuah | and a frequent problem ran into is: how do I enforce a "reset" to happen in the proof | 17:06 |
| josuah | I can imagine "if (i_reset) reset_done <= 1;", and then "assume(i_reset || reset_done);" | 17:06 |
| josuah | but what if at system startup, "reset_done = 1" and "i_reset = 0"? then "i_reset" never becomes 1 | 17:07 |
| josuah | whichever "reset_done" variable that states "now I am initialised, you can carry on"... | 17:10 |
| josuah | it might be fooled by having the system initialise directly with "yes, I'm sure now" == 1 | 17:12 |
| josuah | likewise, one could imagine: "I remember my parents taking care of me as a child" (akin to "reset_done = 1") | 17:13 |
| josuah | there could have been another past I do not remember with "different parents taking care of me" (akin to system that started at "reset_done = 1" but "i_reset = 0") | 17:16 |
| josuah | trying to find some "early verification point" is the common challenge to both "have I been adopted" and "have the system been reseted" | 17:18 |
| josuah | so maybe if I can solve "have I been adopted" I can manage to make SymbiYosys behave as I wish (verify! verify! verify!) | 17:19 |
| * josuah imagines researchers constantly walking from the faculty of science to faculty of philosophy to find an answer to their math/IT questions :P | 17:21 | |
| josuah | "asks my mother, she knows for sure"? | 17:28 |
| josuah | well that would work: ask the mother*board* to issue a i_reset signal, like it can be done on FPGA, iirc with a reset signal issued early | 17:29 |
| josuah | but not for verification: no hardware there | 17:29 |
| *** ec <ec!~ec@gateway/tor-sasl/ec> has joined #yosys | 17:43 | |
| josuah | assert() -> cover() | 17:49 |
| josuah | assume() -> what_i_need() | 17:49 |
| josuah | "I do not know whether I was adopted, but it certainly does not look like so to me" | 17:55 |
| josuah | "I do not know whether a reset did happen, but all variables look like being at '0'" | 17:56 |
| josuah | `assume({ state, tx_shift_reg, tx_counter, o_wb_ack } == 0 || state > 0); | 17:56 |
| josuah | heh, I'll figure out :) | 17:56 |
| josuah | ^ skip this monologue unless you are bored :) | 17:57 |
| *** preyalone <[email protected]> has quit IRC (Quit: Connection closed for inactivity) | 18:10 | |
| *** Guest81 <[email protected]> has joined #yosys | 18:33 | |
| *** Guest81 <[email protected]> has quit IRC (Client Quit) | 18:34 | |
| *** Guest57 <[email protected]> has joined #yosys | 18:41 | |
| qball | :grin: | 18:45 |
| *** FabM <FabM!~FabM@armadeus/team/FabM> has quit IRC (Quit: Leaving) | 19:12 | |
| *** kraiskil <kraiskil!~kraiskil@10.121.104.92.dynamic.wline.res.cust.swisscom.ch> has joined #yosys | 19:16 | |
| *** preyalone <[email protected]> has joined #yosys | 20:21 | |
| *** emeb_mac <[email protected]> has joined #yosys | 20:44 | |
| *** adjtm_ <[email protected]> has quit IRC (Read error: Connection reset by peer) | 20:44 | |
| *** adjtm <[email protected]> has joined #yosys | 20:55 | |
| *** kraiskil <kraiskil!~kraiskil@10.121.104.92.dynamic.wline.res.cust.swisscom.ch> has quit IRC (Ping timeout: 240 seconds) | 20:58 | |
| *** nelgau_ <[email protected]> has joined #yosys | 22:23 | |
| *** nelgau__ <[email protected]> has joined #yosys | 22:25 | |
| *** nelgau <[email protected]> has quit IRC (Ping timeout: 246 seconds) | 22:25 | |
| *** nelgau_ <[email protected]> has quit IRC (Ping timeout: 268 seconds) | 22:28 | |
| *** preyalone <[email protected]> has quit IRC (Quit: Connection closed for inactivity) | 22:41 | |
| *** emeb <[email protected]> has quit IRC (Quit: Leaving.) | 22:58 | |
| *** GenTooMan <GenTooMan!~cyberman@2601:547:437f:e5c6:21f:5bff:fefe:a883> has quit IRC (Quit: Leaving) | 23:44 | |
| *** ec <ec!~ec@gateway/tor-sasl/ec> has quit IRC (Quit: ec) | 23:51 | |
Generated by irclog2html.py 2.17.2 by Marius Gedminas - find it at https://mg.pov.lt/irclog2html/!