captain_morgan has quit [Read error: Connection reset by peer]
captain_morgan has joined #yosys
citypw has quit [Remote host closed the connection]
citypw has joined #yosys
nobodywasishere has quit [Remote host closed the connection]
citypw has quit [Ping timeout: 240 seconds]
awordnot has quit [Ping timeout: 265 seconds]
awordnot has joined #yosys
<awygle>
is there a principled way of understanding when `abc pdr` will pass a proof which fails k-induction?
Degi has quit [Ping timeout: 260 seconds]
Degi has joined #yosys
<az0re>
awygle: You should probably ask Alan directly: Alan Mishchenko <alanmi@berkeley.edu>
<awygle>
i am reading the paper now but i may do that too
<awygle>
thanks
tmiw has quit [Ping timeout: 264 seconds]
tmiw has joined #yosys
<awygle>
ah I see, since pdr works forward from initial states it's a good escape hatch from problems with the inductive step
emeb_mac has quit [Quit: Leaving.]
Jybz has joined #yosys
citypw has joined #yosys
Jybz has quit [Remote host closed the connection]
az0re has quit [Remote host closed the connection]
adjtm_ has joined #yosys
adjtm has quit [Ping timeout: 256 seconds]
Jybz has joined #yosys
proteusguy has quit [Remote host closed the connection]
proteusguy has joined #yosys
az0re has joined #yosys
Jybz has quit [Ping timeout: 265 seconds]
captain_morgan has quit [Quit: Ping timeout (120 seconds)]
captain_morgan has joined #yosys
Asu has joined #yosys
Asuu has joined #yosys
Asu has quit [Ping timeout: 256 seconds]
citypw has quit [Ping timeout: 240 seconds]
keith-man has joined #yosys
<keith-man>
is there any way to specify targer number of logic levels in yosys or abc?
<keith-man>
*a target*
Jybz has joined #yosys
<ZirconiumX>
keith-man: for gate or LUT synthesis?
<keith-man>
gate
<ZirconiumX>
... I'm not sure if this hack will work or not, so keep that in mind
<ZirconiumX>
But ABC has the -D option to target a specific delay
<ZirconiumX>
And since delay is proportional to logic levels, it might work
citypw has joined #yosys
<keith-man>
hmm, how do I invoke that? when looking here, I ahve been able to have yosys generate a blif and then have ABC use a genlib file I wrote, but I can't really figure out how to specify contraints like that
<tpb>
Title: ABC: A System for Sequential Synthesis and Verification (at people.eecs.berkeley.edu)
<keith-man>
oh I see the executing abc inside yosys provides different inputs interesting
<ZirconiumX>
Yup
<keith-man>
hmm but it looks like I lose the ability to load a genlib file that way. Since running abc interactively I could go read_library my_lib.genlib
vidbina has joined #yosys
<keith-man>
ah I think I figured it out how to provide that timing info interatively.
craigo_ has quit [Ping timeout: 258 seconds]
vidbina has quit [Ping timeout: 246 seconds]
yosys-questions has quit [Remote host closed the connection]
mirage335 has quit [Ping timeout: 244 seconds]
mirage335 has joined #yosys
vidbina has joined #yosys
m4ssi has joined #yosys
jfcaron has joined #yosys
adjtm_ has quit [Remote host closed the connection]
adjtm_ has joined #yosys
vidbina has quit [Ping timeout: 264 seconds]
keith-man has quit [Read error: Connection reset by peer]
citypw has quit [Ping timeout: 240 seconds]
vidbina has joined #yosys
emeb has joined #yosys
yosys-questions has joined #yosys
craigo_ has joined #yosys
Cerpin has quit [Quit: leaving]
Cerpin has joined #yosys
N2TOH has quit [Ping timeout: 240 seconds]
N2TOH has joined #yosys
N2TOH_ has joined #yosys
N2TOH has quit [Ping timeout: 246 seconds]
Jybz has quit [Quit: Konversation terminated!]
Asu has joined #yosys
Asuu has quit [Ping timeout: 264 seconds]
N2TOH_ has quit [Ping timeout: 265 seconds]
N2TOH has joined #yosys
N2TOH has quit [Ping timeout: 265 seconds]
N2TOH has joined #yosys
indy has quit [Ping timeout: 244 seconds]
jfcaron has quit [Ping timeout: 246 seconds]
N2TOH has quit [Read error: Connection reset by peer]
indy has joined #yosys
N2TOH has joined #yosys
jfcaron has joined #yosys
jfcaron has quit [Read error: Connection reset by peer]