<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'"