ChanServ changed the topic of #yosys to: Yosys Open SYnthesis Suite: https://github.com/YosysHQ/yosys/ | Channel logs: https://libera.irclog.whitequark.org/yosys/
tpb has quit [Remote host closed the connection]
tpb has joined #yosys
kristianpaul has quit [Ping timeout: 272 seconds]
kristianpaul has joined #yosys
peeps[zen] has joined #yosys
peepsalot has quit [Ping timeout: 260 seconds]
citypw has joined #yosys
emeb_mac has quit [Ping timeout: 272 seconds]
cr1901_ has joined #yosys
cr1901 has quit [Ping timeout: 260 seconds]
emeb has joined #yosys
citypw has quit [Ping timeout: 240 seconds]
FabM has joined #yosys
FabM has joined #yosys
FabM has quit [Changing host]
cr1901_ is now known as cr1901
preyalone has joined #yosys
kristianpaul has quit [Ping timeout: 256 seconds]
kristianpaul has joined #yosys
<josuah> wow, wow, wow, hang-on!
<josuah> all suddenly, yosys asks me if I have been adopted
<josuah> is it something every hardware developer run through?
<josuah> it seems like one of these corner stone in circuit design is k-induction for verifying designs
<josuah> and a frequent problem ran into is: how do I enforce a "reset" to happen in the proof
<josuah> I can imagine "if (i_reset) reset_done <= 1;", and then "assume(i_reset || reset_done);"
<josuah> but what if at system startup, "reset_done = 1" and "i_reset = 0"? then "i_reset" never becomes 1
<josuah> whichever "reset_done" variable that states "now I am initialised, you can carry on"...
<josuah> it might be fooled by having the system initialise directly with "yes, I'm sure now" == 1
<josuah> likewise, one could imagine: "I remember my parents taking care of me as a child" (akin to "reset_done = 1")
<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")
<josuah> trying to find some "early verification point" is the common challenge to both "have I been adopted" and "have the system been reseted"
<josuah> so maybe if I can solve "have I been adopted" I can manage to make SymbiYosys behave as I wish (verify! verify! verify!)
* josuah imagines researchers constantly walking from the faculty of science to faculty of philosophy to find an answer to their math/IT questions :P
<josuah> "asks my mother, she knows for sure"?
<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
<josuah> but not for verification: no hardware there
ec has joined #yosys
<josuah> assert() -> cover()
<josuah> assume() -> what_i_need()
<josuah> "I do not know whether I was adopted, but it certainly does not look like so to me"
<josuah> "I do not know whether a reset did happen, but all variables look like being at '0'"
<josuah> `assume({ state, tx_shift_reg, tx_counter, o_wb_ack } == 0 || state > 0);
<josuah> heh, I'll figure out :)
<josuah> ^ skip this monologue unless you are bored :)
preyalone has quit [Quit: Connection closed for inactivity]
Guest81 has joined #yosys
Guest81 has quit [Client Quit]
Guest57 has joined #yosys
<qball> :grin:
FabM has quit [Quit: Leaving]
kraiskil has joined #yosys
preyalone has joined #yosys
emeb_mac has joined #yosys
adjtm_ has quit [Read error: Connection reset by peer]
adjtm has joined #yosys
kraiskil has quit [Ping timeout: 240 seconds]
nelgau_ has joined #yosys
nelgau__ has joined #yosys
nelgau has quit [Ping timeout: 246 seconds]
nelgau_ has quit [Ping timeout: 268 seconds]
preyalone has quit [Quit: Connection closed for inactivity]
emeb has quit [Quit: Leaving.]
GenTooMan has quit [Quit: Leaving]
ec has quit [Quit: ec]