<cr1901>
Tomorrow's plans: Review temporal induction and how to represent assumptions in SMTv2... because... I forget what yosys does :P.
<cr1901>
cc: q3k, thoughtpolice You both should be interested in this
<cr1901>
thoughtpolice: A long time ago, I asked "how does temporal induction (where the base case spans over "n" steps/states) relate to mathematical induction (where the base case only considers one step)?" Do you remember a convo like that? If not, I'll check my logs and see if I can find it.
<sorear>
if your assumes imply your asserts at time t, and your asserts at time t imply your assumes at time t+1, then your asserts will hold for all time by mathematical induction
<digshadow>
1) Does this CLI look correct: yosys -p 'synth_ice40 -vpr -top top -nocarry my.eblif
<digshadow>
2) what is a yosys full design?
<cr1901>
sorear: Uhhh, what :)?
<digshadow>
fully selected design
<cr1901>
digshadow: "fully selected" means "yosys will currently apply transformations on everything in the hierarchy starting from the top level module"
<cr1901>
you're able to use the "select" command to force yosys to only apply transformations/passes to only parts of your design
<digshadow>
is that not the default?
<cr1901>
Yes, but I've never used the -vpr flag
<digshadow>
I think the people who have used that flag is around 2 or 3
<cr1901>
In any case, firefox takes forever toload on this netbook, so I'll see the gist in about 10 mins or so
<digshadow>
uh...are on the 286 or w/e it was
<cr1901>
No, I would be signed in as cr1901_286 if I was :). It's an Atom netbook from 2007. I use it when I travel b/c I'm too cheapass to purchase a new "burner".
<cr1901>
And I wish firefox ran on 286. Or any browser, really.
nonlinear has joined #yosys
<mithro>
digshadow: I have no idea if the order or arguments in Yosys matter
<cr1901>
What's weird to me is... I don't know how read_verilog can operate only on fully-selected designs b/c that's how you load a design into yosys in the first place
<mithro>
digshadow: If you remove the "-vpr" does the command work?
<digshadow>
mithro: I tried moving them around
<cr1901>
sorear: More helpfully, I'll need some time to really parse what you said...
<cr1901>
As it is, I forget how to represent the concept of an assume in smtv2
<digshadow>
ah wait I think there is a typo
<sorear>
i don't actually know what "temporal induction" is in any great detail. i think it's close to that
<digshadow>
mithro: fixed! works now
<mithro>
?
<mithro>
What was the typo?
<digshadow>
I accidentally deleted -blif
<mithro>
Oh
<cr1901>
oops...
<digshadow>
I'm not sure what it was doing, but it wasn't what I was trying to do
<mithro>
digshadow: Looks like you hit the exact same issue that both myself and cr1901 have hit
<cr1901>
what issue was that again?
<digshadow>
mithro: issue between keyboard and chair?