<awygle>
am i supposed to run yosys-smtbmc on a _testbench_, or on my actual _module_?
AlexDaniel has quit [Read error: Connection reset by peer]
<cr1901_modern>
awygle: It can be either; I used a testbench for spi_tb b/c standalone tests didn't prove all the things I wanted to prove
<awygle>
so i have a design which passes both bmc and temporal induction
<cr1901_modern>
do they pass them both with the same number of timesteps?
<awygle>
an excellent question.
<awygle>
it seems so? i wasn't passing -i so it was defaulting to 20, if i explicitly pass -t 20 both still pass
<cr1901_modern>
then congrats, you've proven a property holds for all time :D
<awygle>
that's exciting. so i'm not going to get false positives?
<cr1901_modern>
Nope
<cr1901_modern>
It's fine if temporal induction passes before t == 20, but BMC needs to pass with _at least_ the number of steps temporal induction got through before the design passed
<awygle>
but false negatives are possible, right? "this is actually correct but i can't prove it because maybe you didn't give me enough timesteps"?
<cr1901_modern>
Not sure. I haven't yet run into a case where the solver couldn't prove it
<awygle>
i managed to make induction fail by running it for 1 timestep, so i guess the answer is yes
<cr1901_modern>
If induction passed for a chain of, say, 7 states, your BMC needs to be at least length 7 to prove that a property holds for all time
<awygle>
that makes sense
<cr1901_modern>
Induction proves: _Assuming the first n states pass, does the n+1 state pass_
<cr1901_modern>
for any n+1th state
<cr1901_modern>
you could theoretically make a design where induction passes, but you can't actually get a chain of "n" states from the initial state where your property holds
<cr1901_modern>
properties hold*
<awygle>
right
<awygle>
an aside: i'm using the "does the past exist" signal from zipcpu's blog post to make this work but it feels inelegant, do you know of a better way to do that?
<cr1901_modern>
$past() is a systemverilog task, you're expected to use it
<awygle>
sorry, i'm specifically talking about the signal he calls "f_past_valid", which is set to true at the beginning of time to avoid the solver using arbitrary values for $past on the first clock tick
<cr1901_modern>
Oh. I don't think so, tbh
<cr1901_modern>
that's probably the "correct" way to do it
<awygle>
hrmph. ok lol
* cr1901_modern
needs to sit down and view some SMTv2 traces sometime soon- too busy lately and my mind is shot lol
<awygle>
so does if (signal) assert(property); mean the same as assert property (signal |-> property);?
<awygle>
(modulo some stuff about always blocks)
<cr1901_modern>
awygle: It is unfortunately more complicated than that
<cr1901_modern>
I don't actually fully undestand it myself. I just know it's different
<awygle>
cr1901_modern: interesting, thanks
<awygle>
well, i now have a formally verified... counter module :P baby steps
indy has quit [Ping timeout: 248 seconds]
indy has joined #yosys
mbuf has joined #yosys
azonenberg has quit [Ping timeout: 246 seconds]
pie_ has quit [Ping timeout: 255 seconds]
dys has joined #yosys
nrossi has joined #yosys
leviathanch has joined #yosys
svenn has quit [Read error: Connection reset by peer]
svenn has joined #yosys
dys has quit [Ping timeout: 240 seconds]
m_t has joined #yosys
AlexDaniel has joined #yosys
<ZipCPU>
awygle: The mathematical definition of an implication if (A) then (B) is (!A)||(B).
<ZipCPU>
The difference between the implies keyword and |-> is a clock.
<ZipCPU>
I use always @(posedge i_clk) if (A) assert(B) often for implies. However, A and B are tested on the same clock within that always block.
<ZipCPU>
If I wanted "if (A) was true on the last clock" I'd do "if ((f_past_valid)&&($past(A)) assert(B);"
<ZipCPU>
I agree with both of you that this is a *very* inelegant solution.
pie_ has joined #yosys
leviathanch has quit [Remote host closed the connection]
mbuf has quit [Quit: Leaving]
AlexDaniel has quit [Ping timeout: 248 seconds]
leviathanch has joined #yosys
leviathanch has quit [Read error: Connection reset by peer]
pie_ has quit [Ping timeout: 252 seconds]
eduardo_ has joined #yosys
eduardo__ has quit [Ping timeout: 240 seconds]
pie_ has joined #yosys
AlexDaniel has joined #yosys
jhol has joined #yosys
pie_ has quit [Ping timeout: 240 seconds]
FabM has quit [Quit: ChatZilla 0.9.93 [Firefox 52.3.0/20170811091919]]
<thoughtpolice>
ZipCPU: For $WORK on our Altera boards, we do memory mapping between ARM/FPGA with a convenient driver, udmabuf: https://github.com/ikwzm/udmabuf -- really useful. Also works on Xilinx too, so it can help for designs if you plan to port them.
<thoughtpolice>
It basically just reserves a contiguous memory buffer in the kernel you can then mmap() (with optional cache disable) from userspace and read/write to. You probably still want/need some Avalon/kernel stuff though, just for things like poking/configuring design registers, stuff like that, but much easier overall than doing it for everything. (We control the design regs/parameters through a sysfs/platform driver and mmap pages
<thoughtpolice>
in after)
AlexDaniel has quit [Ping timeout: 240 seconds]
digshadow has quit [Ping timeout: 240 seconds]
digshadow has joined #yosys
AlexDaniel has joined #yosys
ravenexp has quit [Quit: WeeChat 1.9.1]
sklv has quit [Remote host closed the connection]
sklv has joined #yosys
ravenexp has joined #yosys
gnufan has joined #yosys
gnufan has left #yosys [#yosys]
gnufan1 has joined #yosys
nrossi has quit [Quit: Connection closed for inactivity]
clifford has joined #yosys
m_t has quit [Quit: Leaving]
gnufan1 has quit [Quit: Leaving.]
<awygle>
ZipCPU: have you done any playing with assert() in Verilator?