<promach_>
hi, have anyone used predicate logic proof simplication for yosys-smt formal verification purpose ?
jkiv has joined #yosys
[X-Scale] has joined #yosys
X-Scale has quit [Ping timeout: 256 seconds]
[X-Scale] is now known as X-Scale
<ZipCPU>
promach_: Your question makes no sense. Formal verification *is* a predicate logic proof.
digshadow has quit [Ping timeout: 252 seconds]
<promach_>
ZipCPU: huh ?
<promach_>
I thought it is using brute force to find out all possible combination of state-space of the coding
m_w has quit [Quit: Leaving]
kristianpaul has quit [Quit: Lost terminal]
kristianpaul has joined #yosys
digshadow has joined #yosys
FabM has quit [Ping timeout: 240 seconds]
m_w has joined #yosys
FabM has joined #yosys
jkiv has quit [Ping timeout: 256 seconds]
vinny has left #yosys [#yosys]
m_w has quit [Quit: leaving]
nrossi has joined #yosys
captain_morgan has quit [Remote host closed the connection]
captain_morgan has joined #yosys
captain_morgan has quit [Remote host closed the connection]
captain_morgan has joined #yosys
leviathanch has joined #yosys
eduardo__ has joined #yosys
eduardo_ has quit [Ping timeout: 240 seconds]
m_t has joined #yosys
leviathanch has quit [Remote host closed the connection]
FabM has quit [Ping timeout: 256 seconds]
<ZipCPU>
promach_: Yes and no. A good solver will use a lot of predicate logic to reduce the space of combinations to search.
FabM has joined #yosys
ravenexp has quit [Ping timeout: 276 seconds]
leviathanch has joined #yosys
mwk has joined #yosys
<ZipCPU>
Although .... thinking some more on it, even if it did reduce the space by brute force, it's still a predicate logic space it's working within.
jkiv has joined #yosys
m_t has quit [Quit: Leaving]
jkiv has quit [Ping timeout: 252 seconds]
sklv has quit [Read error: Connection reset by peer]
sklv has joined #yosys
<promach>
ZipCPU: predicate logic within BMC and induction ?
<ZipCPU>
Isn't that what they are? isn't an assertion or an assumption a statement of predicate logic?
FabM has quit [Quit: ChatZilla 0.9.93 [Firefox 52.5.0/20171114221957]]
<promach>
ZipCPU: not sure about that though
<ZipCPU>
assert(counter < 12); /// <<---- this is a statement of predicate logic
<cr1901_modern>
promach: A predicate is a function that returns a boolean
seldridge has joined #yosys
jhol has quit [Quit: Coyote finally caught me]
jhol has joined #yosys
jkiv has joined #yosys
jhol has quit [Quit: Coyote finally caught me]
jhol has joined #yosys
sunxi_fan has left #yosys [#yosys]
ravenexp has joined #yosys
jkiv has quit [Ping timeout: 240 seconds]
m_w has joined #yosys
seldridge has quit [Ping timeout: 240 seconds]
gnufan has joined #yosys
m_t has joined #yosys
dys has joined #yosys
dys has quit [Ping timeout: 256 seconds]
dys has joined #yosys
dys has quit [Ping timeout: 240 seconds]
dys has joined #yosys
dys has quit [Ping timeout: 256 seconds]
jkiv has joined #yosys
jkiv has quit [Ping timeout: 246 seconds]
jkiv has joined #yosys
jkiv has quit [Ping timeout: 260 seconds]
jkiv has joined #yosys
dys has joined #yosys
m_w has quit [Ping timeout: 268 seconds]
digshadow has quit [Ping timeout: 240 seconds]
sklv has quit [Ping timeout: 255 seconds]
sklv has joined #yosys
leviathanch has quit [Remote host closed the connection]
nrossi has quit [Quit: Connection closed for inactivity]