Friday, 2020-05-01

*** tpb has joined #yosys00:00
*** Forty-Bot has joined #yosys00:21
*** N2TOH has quit IRC01:03
*** N2TOH has joined #yosys01:04
*** N2TOH has quit IRC01:30
*** N2TOH has joined #yosys01:32
*** nobodywasishere has joined #yosys01:42
*** citypw has joined #yosys02:07
*** captain_morgan has quit IRC02:14
*** captain_morgan has joined #yosys02:15
*** citypw has quit IRC02:19
*** citypw has joined #yosys02:20
*** nobodywasishere has quit IRC02:37
*** citypw has quit IRC03:13
*** awordnot has quit IRC03:18
*** awordnot has joined #yosys03:18
awygleis there a principled way of understanding when `abc pdr` will pass a proof which fails k-induction?03:25
*** Degi has quit IRC03:53
*** Degi has joined #yosys03:56
az0reawygle: You should probably ask Alan directly: Alan Mishchenko <[email protected]>05:35
awyglei am reading the paper now but i may do that too05:35
*** tmiw has quit IRC06:21
*** tmiw has joined #yosys06:22
awygleah I see, since pdr works forward from initial states it's a good escape hatch from problems with the inductive step06:40
*** emeb_mac has quit IRC06:57
*** Jybz has joined #yosys06:59
*** citypw has joined #yosys07:00
*** Jybz has quit IRC07:00
*** az0re has quit IRC07:18
*** adjtm_ has joined #yosys08:00
*** adjtm has quit IRC08:02
*** Jybz has joined #yosys08:10
*** proteusguy has quit IRC08:14
*** proteusguy has joined #yosys08:20
*** az0re has joined #yosys08:22
*** Jybz has quit IRC08:58
*** captain_morgan has quit IRC09:12
*** captain_morgan has joined #yosys09:13
*** Asu has joined #yosys09:38
*** Asuu has joined #yosys09:42
*** Asu has quit IRC09:43
*** citypw has quit IRC09:54
*** keith-man has joined #yosys09:55
keith-manis there any way to specify targer number of logic levels in yosys or abc?09:56
keith-man*a target*09:56
*** Jybz has joined #yosys10:04
ZirconiumXkeith-man: for gate or LUT synthesis?10:05
ZirconiumX... I'm not sure if this hack will work or not, so keep that in mind10:06
ZirconiumXBut ABC has the -D option to target a specific delay10:06
ZirconiumXAnd since delay is proportional to logic levels, it might work10:06
*** citypw has joined #yosys10:07
keith-manhmm, 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 that10:08
tpbTitle: ABC: A System for Sequential Synthesis and Verification (at
keith-manoh I see the executing abc inside yosys provides different inputs interesting10:17
keith-manhmm 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.genlib10:19
*** vidbina has joined #yosys10:26
keith-manah I think I figured it out how to provide that timing info interatively.10:29
*** craigo_ has quit IRC11:09
*** vidbina has quit IRC11:25
*** yosys-questions has quit IRC11:30
*** mirage335 has quit IRC12:45
*** mirage335 has joined #yosys13:15
*** vidbina has joined #yosys14:02
*** m4ssi has joined #yosys14:06
*** jfcaron has joined #yosys14:20
*** adjtm_ has quit IRC14:31
*** adjtm_ has joined #yosys14:32
*** vidbina has quit IRC16:00
*** keith-man has quit IRC16:05
*** citypw has quit IRC16:24
*** vidbina has joined #yosys17:34
*** emeb has joined #yosys18:12
*** yosys-questions has joined #yosys18:51
*** craigo_ has joined #yosys19:33
*** Cerpin has quit IRC19:39
*** Cerpin has joined #yosys19:39
*** N2TOH has quit IRC19:46
*** N2TOH has joined #yosys19:47
*** N2TOH_ has joined #yosys20:18
*** N2TOH has quit IRC20:19
*** Jybz has quit IRC20:25
*** Asu has joined #yosys20:45
*** Asuu has quit IRC20:46
*** N2TOH_ has quit IRC20:55
*** N2TOH has joined #yosys21:00
*** N2TOH has quit IRC21:16
*** N2TOH has joined #yosys21:18
*** indy has quit IRC21:21
*** jfcaron has quit IRC21:25
*** N2TOH has quit IRC21:25
*** indy has joined #yosys21:25
*** N2TOH has joined #yosys21:26
*** jfcaron has joined #yosys21:43
*** jfcaron has quit IRC21:43
cr1901_modern I love this21:43
*** jfcaron has joined #yosys21:44
*** jfcaron has quit IRC21:52
*** jfcaron has joined #yosys21:53
*** jfcaron has quit IRC22:01
*** FL4SHK has quit IRC22:07
*** Nazara has quit IRC22:07
*** sensille has quit IRC22:07
*** knielsen has quit IRC22:07
*** mirage335 has quit IRC22:07
*** Thorn has quit IRC22:07
*** _whitelogger has quit IRC22:07
*** MoeIcenowy has quit IRC22:07
*** GenTooMan has quit IRC22:07
*** tecepe has quit IRC22:07
*** noopwafel has quit IRC22:07
*** FFY00 has quit IRC22:07
*** Nazara has joined #yosys22:08
*** vidbina has quit IRC22:08
*** _whitelogger has joined #yosys22:09
*** MoeIcenowy has joined #yosys22:09
*** N2TOH has quit IRC22:10
*** FFY00 has joined #yosys22:11
*** N2TOH has joined #yosys22:16
*** mirage335 has joined #yosys22:16
*** Asuu has joined #yosys22:31
*** Asu has quit IRC22:34
*** m4ssi has quit IRC22:44
*** Thorn has joined #yosys23:01
*** jfierro has joined #yosys23:44
jfierroHi all. Is it a bug if yosys interprets '1 as a single bit 1 instead of a bit fill of 1's, even when passing the -sv option?23:45
ZirconiumXjfierro: I'm not sure it's a supported SV feature23:45
*** emeb has quit IRC23:51

Generated by 2.17.2 by Marius Gedminas - find it at!