m_t has quit [Quit: Leaving]
digshadow has quit [Quit: Leaving.]
digshadow has joined ##openfpga
digshadow has quit [Quit: Leaving.]
m_w has joined ##openfpga
uwe_ has quit [Ping timeout: 256 seconds]
uwe_ has joined ##openfpga
digshadow has joined ##openfpga
digshadow has quit [Quit: Leaving.]
m_w has quit [Quit: leaving]
carl0s has joined ##openfpga
Amun_Ra has joined ##openfpga
amclain has quit [Quit: Leaving]
digshadow has joined ##openfpga
DocScrutinizer05 has quit [Disconnected by services]
DocScrutinizer05 has joined ##openfpga
digshadow has quit [Quit: Leaving.]
carl0s has quit [Quit: Leaving]
digshadow has joined ##openfpga
digshadow has quit [Quit: Leaving.]
digshadow has joined ##openfpga
<rqou> Belgian taxi drivers are so aggressive :P
digshadow has quit [Ping timeout: 246 seconds]
digshadow has joined ##openfpga
massi has joined ##openfpga
Bike has quit [Quit: leaving]
m_t has joined ##openfpga
m_t has quit [Read error: Connection reset by peer]
m_t has joined ##openfpga
kuldeep__ has joined ##openfpga
kuldeep_ has quit [Ping timeout: 248 seconds]
kuldeep__ has quit [Max SendQ exceeded]
kuldeep has joined ##openfpga
jrernst has joined ##openfpga
eduardo__ has joined ##openfpga
eduardo_ has quit [Ping timeout: 272 seconds]
<jrernst> Hi! What to do now?
<nats`> jump around !
<nats`> but don't break the channel :)
<jrernst> JUMP JUMP JUMP :-)
* nats` waves like only Maxwell coffe can !
<nats`> this fuck dual pun
<nats`> I write it on paper because I don't want to forget it :D
<Marex> jrernst: so uh, how far did you get with the C/III ?
<jrernst> I concentrated on making scripts for automatic generation and collecting data from the SOF file and the RCF file.
<jrernst> The main problem is multiple info in the data. I can not say for sure which bit is from LE or C$ or whatever.
<jrernst> So I came up with the idea to minimize the influence of different signals.
<jrernst> It's done by simply putting a "transmitter" in a LCCOMB. Think of it like a transmitter which is sending pulses to one output pin. It's simply made by backcoupling the output: out <= mem; mem <= not mem; With no FF involved, just combinatorics.
<jrernst> With this construct I can trace a route from the LCCOMB output to a pin. No clutter.
<jrernst> And with scripting I can place the LCCOMB in a targeted LAB (using e.g. set_location_assignment LCCOMB_X17_Y1_N8 -to out~1 in the QSF file)
<jrernst> With this I can generate a database with routing from any LAB to any pin.
<jrernst> But what doing then with this?
<jrernst> Ah by the way, in the RCF there is the route with the used connections verbosely named.
<Marex> jrernst: you are aware you can patch the value of LUT , right ?
<Marex> jrernst: that way, you can locate the LUT placement in the bitstream
<jrernst> The LUT was the first thing I discovered and it's no secret any more. If you mean that 16 bit table.
<Marex> jupp
* Marex reads the discussion again
<Marex> ah
<Marex> jrernst: look at C4, that's the simplest one
<Marex> jrernst: there's 12 of them routing up, 12 routing down and 8 which I dunno, there's always two down/one up/one unknown or two up/one down/one unknown in each two LEs
<Marex> jrernst: also, each C4 is configured with 8 bits , which is thus easy
<Marex> if you carefully place the C4s , you can figure out what they all mean
<Marex> jrernst: is your LAB also 70 bits tall on the CIII ?
<Marex> jrernst: mine is, from which 64bits are for LEs, 6 bits are for the LAB-wide control block
<jrernst> yes. It's 70 for EP3C5, EP3C16, EP4CE6 and EP4CE22 as far as I know.
<jrernst> And surprise it's 35 wide by them all.
<Marex> jupp
<azonenberg> woo looks like progress on the altera front? :0
<jrernst> Interestingly the bitstream is 1727 x 1654 for the EP4CE6 and the EP3C5. Both the smallest ones.
<Marex> jrernst: I suspect they;d be pretty compatible
<Marex> jrernst: look at http://git.bfuser.eu/?p=marex/typhoon.git;a=blob;f=doc/lab.txt;h=9a4c1b15c30f538f5511d7b901a3582897eb118a;hb=516902ff8eece954b8c70d5ce8430aa7f53caab4#l63
<Marex> jrernst: and http://git.bfuser.eu/?p=marex/typhoon.git;a=blob;f=doc/lab.txt;h=9a4c1b15c30f538f5511d7b901a3582897eb118a;hb=516902ff8eece954b8c70d5ce8430aa7f53caab4#l108
<Marex> jrernst: this should give you an idea where the LE bits are
<jrernst> yes, I read it but did not get it all.
<jrernst> If I make many vhdl files scan every sof then I will end up with these tables. But this is very time consuming. I'm thinking about a more automated process.
<jrernst> okay let me show you one more idea with results here.
<azonenberg> clifford: when you get a chance
<azonenberg> i'm trying to troubleshoot a SMT proof that is giving me confusing resjults
<azonenberg> in particular... yosys-smtbmc on the base case passes
<jrernst> at the beginning there was the question which bits were set and which are not set.
<azonenberg> yosys-smtbmc -i passes as well
<azonenberg> But when i run yosys-smtbmc -g it says "model is not available"
<azonenberg> which seems to imply my assertions are contradictor?
<azonenberg> contradictory?
<jrernst> I was trying to detect the coverage of bits when I use the data from all LABs in a project by ORing them together.
<jrernst> The pattern I got was this:
<jrernst> XXXXXXXXXXXXXXXXX...........XXXXXXX
<jrernst> XXXXXXXXXXXXXXXXX..............XXXX
<jrernst> XXXXXXXXXXXXXXXXXXXXXXXXXXX..X.XXXX
<jrernst> XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX
<jrernst> XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX
<jrernst> XXXXXXXXXXXXXXXXXXXXXXXXXXX....XXXX
<jrernst> XXXXXXXXXXXXXXXXX............X.XXXX
<jrernst> XXXXXXXXXXXXXXXXX...........XXXXXXX
<jrernst> Oops I forgot to mark the LUT. It's there in the middle where the zero bits "." are above and down the 4 lines with X.
<jrernst> XXXXXXXXXXXXXXXXXXXLLLLLLLL..X.XXXX
<jrernst> and the following 3 lines as well.
<jrernst> From this pattern I know I can reach all the bits with X from this project.
<jrernst> This only works if all LAB are constructed the same way. Only then it is possible to overlay one LAB over the other.
<clifford> azonenberg, is there code somewhere that I can look at?
<clifford> azonenberg, is it "yosys-smtbmc -g /tmp/rpcv3transceiver.smt2"?
<jrernst> I roughly try to reproduce the ansatz which is shown here: https://www.youtube.com/watch?v=61DQLzt7K1E (Reverse-engineering the bitstream of Altera's MAX-V CPLDs - Jean-François Nguyen - LSE Week 2016) Sorry it's in french. Does anyone know this approach?
<Marex> oh :)
<Marex> I'll have to watch that
<Marex> jrernst: the way I determined where each and every LUT is is that I just ran ECO and flipped every bit in every LUT , one after the other , and then generated a bitstream
<Marex> this is 16 changes for each LUT , and I did that for all LUTs in the EP4CE6 ...
<Marex> it ran overnight
<jrernst> over night? really?
<Marex> jrernst: jupp, there's not that much work
<jrernst> I had no ECO. Instead I made 16 logic equations with 4 inputs and ran the compiler 16 times -> there is was.
<Marex> jrernst: the ECO is real fast, it basically patches the LUT and re-generates the bitstream in seconds :)
<Marex> jrernst: you certainly do have ECO if you use quartus :)
<Marex> jrernst: go to chip planner, replace the LUT value, save the ECO
<jrernst> Unfortunately I only have the free version and there is no ECO.
<Marex> it can be scripted :)
<jrernst> Maybe I miss something here.
<Marex> there is ECO in the free version ;-)
<clifford> azonenberg, rpc_rx_ready in RPCv3Transceiver is constantly driven to '1' but initialized to '0'. No solution is found for the initial state that satisfies both constraints.
<jrernst> Okay, maybe it's the version. I'm using Quartus II 32-bit Version 13.1.0 Build 162 10/23/2013 SJ Web Edition
<jrernst> In the chip planner the editing mode is "ECO - EP4CE6E22C6" for example.
<Marex> jrernst: download there, see the build_eco() function
<Marex> jrernst: there's a reason I use the C/IV ;-)
<Marex> jrernst: maybe invest 30 bucks into that small C/IV kit and install new quartus to make your life easier ?
<jrernst> maybe...
<jrernst> build_eco(): damn, I should have learned the f***ing tcl. :-)
<jrernst> I once was in the shell (quartus_cdb -s) but didn't know much how to use it.
<azonenberg> clifford: let me see...
<azonenberg> clifford: that's interesting because in RPCv3Transceiver:473-479 it sure seems like it can toggle
<azonenberg> Might have to examine that in more detail
<clifford> this is the version on github:
<azonenberg> (also, any tips on how to find these contradictions better in the future? Is there a way to get them automatically flagged?)
<clifford> 466 //placeholder: always ready to receive
<clifford> 469 end
<clifford> 468 rpc_rx_ready <= 1;
<clifford> 467 always @(*) begin
<azonenberg> um
<azonenberg> interesting, thats not what i have
* azonenberg checks sync
<azonenberg> this is what i was testing with
<clifford> my version is old.
<azonenberg> So if this is what i was testing with
<azonenberg> can you explain the problem?
<azonenberg> (and again, how ccan i find these contradictions automatically?)
<azonenberg> i can easily identify an invalid state, but i cant tell what makes it inconsistent
<jrernst> Ah, I see what it's done in the build.sh. Pretty much the same I did from outside: compiling, backannotating, extracting from rcf. But one thing is very good: I don't have to change to QSF file any longer.
<azonenberg> clifford: also, last time i checked it was legal verilog to specify an initializer on a combinatorial "reg"
<azonenberg> however this was ignored for synthesis
<azonenberg> this lets you easily switch back and forth between synchronous and asynchronous implementations of a given piece of logic
<azonenberg> If yosys does strange things like generating contradictory states rather than simply ignoring the init attribute
<azonenberg> we should check the LRM and see what the correct behavior is
<clifford> sure it is legal verilog code.
<azonenberg> what i mean is
<clifford> but it still is a conflicting constraint if you initialization is different from the driver
<azonenberg> Is it, though?
<clifford> rpc_tx_data seems to be the problem
<azonenberg> Or does the LRM specify that the init is ignored during synthesis
<azonenberg> if the driver is combinatorial
<azonenberg> Because if that's the case it's a well-defined non-conflicting \case
<azonenberg> case*
<jrernst> Marex, can you explain the fanin_record use in the script?
<clifford> The LRM doesn't say anything about synthesis. Thats 1364.1
eric_j has quit [Read error: Connection reset by peer]
eric_j has joined ##openfpga
<clifford> And there is no 1364 std for formal verification semantics..
* azonenberg reads
<clifford> Sec B.11 of IEEE 1364.1-2002
<clifford> B.11 Assignments in variable declarationsA variable may be initialized in its declaration. Making assignments in the declaration forces the signal to aknown value for pre-synthesis simulations. In general, no such initialization occurs in an actual gate leveldesign. This can cause a mismatch between pre-synthesis and post-synthesis simulations and in generalshould be avoided.
<Marex> jrernst: I probably cannot , I think I was using that for fiddling with the fanins somehow ;-/
<azonenberg> Hmm, interesting
<lain> clifford: is there any effort/plan to support vhdl for yosys, or alterantively are you aware of any vhdl tools that support formal verification and don't cost more than my car?
<Marex> jrernst: it's been a while since I was digging in those parts
<Marex> jrernst: here's the whole project with the ECO http://www.bfuser.eu/tp/
<clifford> some synthesis tools actually ignore all initializations. (e.g. lattice iCEcube)
<azonenberg> clifford: because in the xilinx case, the "initial" statement is the *recommended* way of resetting registers
<azonenberg> they specifically recommend against use of external reset signals unless you need a partial runtime reset of the design
<clifford> most ASIC tools do. Most FPGA tools use them for reg initialization. But it's all implementation defined..
<azonenberg> Interesting
<Marex> jrernst: start at "bulktest.sh"
<Marex> jrernst: thinking about it, I recall running the ECOs in parallel to speed things up too :)
<jrernst> okay, I'll digging in that.
<azonenberg> clifford: So is there not an IEEE-defined set of semantics for verilog-for-FPGA synthesis?
<clifford> It would not be hard to make a Yosys pass that removes the "init" property from all wires that aren't driven by a FF. But I would assume that this would cause problems in other situations then where people would expect the initialization to actually effect the init state.
<azonenberg> clifford: when would it?
<azonenberg> in particular, according to the LRM
<clifford> azonenberg, there is. It is IEEE 1364.1, like for any other syntheis tasks.
<azonenberg> clifford: i meant for FPGA specifically
<azonenberg> and technically if you want to take a strict reading of 1364.1
<azonenberg> 7.7.9.1
<clifford> there are isn't one for ASICs specifically
<azonenberg> "The initial statement shall be supported only for ROM modeling as described in 5.6.2. It shall be ignored in all other contexts."
<Marex> jrernst: it's ugly as hell, sorry about that
<azonenberg> So it's technically *always* legal to discard an 'initial' statement
<azonenberg> unless it's writing to a rom
<Marex> jrernst: quartus is kinda sensitive to hand-patched ECO tcl files ;-/
<azonenberg> If you want to preserve the common FPGA semantics, it should be kept if attached to a LUT/FF
<azonenberg> to a latch/FF*
<azonenberg> but i cannot think of any case where an init attribute on a combinatorial wire makes any sense
<clifford> as I have said: in practice it is all implementation defined. different vendors support differnt stuff for different targets
<Marex> jrernst: I'd suggest you try building a project and running a chip planner, then doing the ECO, that's really the easiest way to check whether you can do it on your chip
<azonenberg> clifford: yeah but what i meant was
<azonenberg> you are fully compliant with the LRM and 1364.1 if you remove the init attribute from all non-FF/latch signals
<clifford> then don't initialize it :)
<azonenberg> And i cannot think of any situation where this is the wrong thing to do
<azonenberg> As a minimum, there should be a warning
<azonenberg> if the init attribute is discarded because there's no ff/latch inferred
<azonenberg> in particular silently producing contradictory output seems to *always* be the exact WRONG thing to do
<azonenberg> either produce sane output, or emit a warning/error
<azonenberg> Producing nonsense with no diagnostic is never what the user wants, right?
<clifford> If the user puts nonesense in.. Should I also ignore all assume statements on false constant expressions for the same reason? I think not.
<clifford> Sure, a warning would be nice. It's not entirely trivial though..
<azonenberg> clifford: INIT attribute on wire that is not connected to a ff/latch output
<azonenberg> seems easy enough
<azonenberg> also yes, I think that an assume() which turns out to be false after synthesis-time const folding should generate a warning
<clifford> How do I know if a cell is a ff/latch, including all vendor defined blackbox cells.
<azonenberg> clifford: if unknown, keep it
<azonenberg> But for straightforward RTL it should be easy enough
<clifford> azonenberg, as I'vbe said: warning is OK (although not trivial), but ignoring something is just wrong.
<clifford> Don't move the goal post! :)
<azonenberg> clifford: Maybe make it an optional flag then?
<azonenberg> Either way, warning at a minimum
<clifford> Then again: how do I know if a vendor cell is a FF?
<azonenberg> A warning that triggers on 80% of bad code is better than one that's not there
<azonenberg> as long as you avoid false positives
<azonenberg> And realistically unless the user explicitly puts (* INIT = 1 *) on a wire
<azonenberg> init attributes only come from behaviorally inferred reg's anyway
<azonenberg> right?
<clifford> But it would result in false positives because I cannot detect vendor FF cells, thus would have to assume that the vendor cell is not a FF.
<azonenberg> No, you'd assume it is a FF
<azonenberg> And not warn
<clifford> No.
<azonenberg> why?
<clifford> Because we usually first map the FFs to vendor cells and in a LATER STEP propagate the init values into the vendor cells IFF the vendor cell has a property for initialization.
<azonenberg> what i'm asking is for a warning when a RTLIL cell other than a $dff or $dlatch drives a wire with an INIT attribute
<azonenberg> ignore all explicit cell instantiations
<clifford> E.g. most ASIC libraries do not have a property for init value, so our output format is a vendor cell with an init attribute on the wire its driving.
<azonenberg> Well, maybe we could go stronger there
<azonenberg> if you are targeting an ASIC library that does not support FF initialization at all
<azonenberg> any init attributes outside of a ROM cell are an error
<clifford> what I am saying is that the $dff cell is CONVERTED into a vendor FF cell. I am not talking about explicit instantiations
<azonenberg> So if a DFF cell is converted to a non-initializable vendor cell
<azonenberg> you don't warn
<azonenberg> it's no worse than the current behavior
<clifford> No! because sometimes you WANT to be able to inizialize an FF during verification.
<azonenberg> You'd make that a configurable option, of course
<azonenberg> not the default
<clifford> The user can always thor away init attributes when he wants to. But when they are thrown away you can't simply wish it back..
<clifford> *throw
<azonenberg> who said anything about throwing away the attributes?
<azonenberg> all i want is, pre techmap
<azonenberg> a pass or synthesis option that lets me trigger a warning
<azonenberg> if a wire with an init attribute is driven by a $alu, $mux, $and, etc cell
<azonenberg> or, in general, anything but a $dff, $dlatch, or explicit cell instantiation
<azonenberg> If there's an additional option to discard the init in that case, that'd be nice too
<azonenberg> heck, you could even do it when writing the SMT file
<Marex> jrernst: I'll be off for a few hours ...
<azonenberg> clifford: in any case, really what i want primarily
<azonenberg> is an easy way to detect contradictions when doing a SMT proof
<azonenberg> rather than just "model is not available"
<clifford> that's something that you have to discuss with the SMT people
<azonenberg> That's the solver?
* azonenberg should write some passes to find obvious sanity errors
<clifford> I don't think SMT has a standard format for unsat kernels
<clifford> All the solver says is "unsat".
<azonenberg> Yeah, well it's one thing to know your proof doesn't hold
<azonenberg> it's another entirely to know it doesn't hold because X and Y conflict
<azonenberg> i have to get going to work soon but will look into this tonight
<azonenberg> i feel like at least some obvious cases, like multiple drivers and assertions const-folded to false, can be detected easily enough
<azonenberg> Also...
<azonenberg> If I run a temporal induction proof and it's successful at (say) step 12
<azonenberg> Does that mean I only need a 12-step BMC to complete the proof?
<azonenberg> iow, does it mean that the induction was successful with only the past 12 cycles of state?
amclain has joined ##openfpga
<clifford> right now: yes. However, in the future there might be exceptions to this when you have a more complex .smtc file.
<clifford> nope. I've already implemented it.. :) so with more complex .smtc files this isn't true already now.
<lain> quality service
<lain> :3
<clifford> azonenberg, imagine the following smtc file:
<clifford> always 10
<clifford> always 15
<clifford> assume [foo]
<clifford> assert [foo]
<clifford> This will need 10 steps in BMC to fail but induction will suceed in 1 step if -t is set to at least 15
<clifford> ("always N" will assert/assume starting with step N)
<clifford> azonenberg, see http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.5-r2015-06-28.pdf: (get-proof) has a solver specific return format, thus is not suitable, and (get-unsat-core) does not dig into the formulas itself, so its not such a big help.
<clifford> What I usually do is writing out the complete smt2 input to the solver (--dump-smt2) and then iteratively edit it to narrow down the cause of the unsat.
<clifford> It pretty fast and easy to do, iff you know SMT-LIB2 and understand how Yosys-SMTBMC is using it.. :)
azonenberg_work has joined ##openfpga
Ardeshir has joined ##openfpga
Bike has joined ##openfpga
<mIKEjONES> t/wuin 2
<mIKEjONES> whoops
azonenberg_work has quit [Ping timeout: 272 seconds]
m_t has quit [Quit: Leaving]
massi has quit [Quit: Leaving]
laintoo has quit [Ping timeout: 248 seconds]
laintoo has joined ##openfpga
azonenberg_work has joined ##openfpga
jrernst has quit [Quit: Leaving]
jrernst has joined ##openfpga
<jrernst> Marex: As I said before ECO doesn't work with my quartus. I can make ECO changes but when compiling they are all gone.
<jrernst> Marex: And I made a project with your files. When compiling the verilog file it deletes all LL_... lines from the QSF file. I think it's no surprise because on start up quartus reports "Warning (292013): Feature LogicLock is only available with a valid subscription license."
<azonenberg_work> clifford: i see
digshadow has quit [Ping timeout: 248 seconds]
<azonenberg_work> clifford: So assuming i do not have time-dependent stuff in my SMTC file
<azonenberg_work> How can i determine the number of cycles to run BMC and induction in order to get a proof that holds forever?
<clifford> with "no time-dependent stuff" you mean a combinational circuit?
<azonenberg_work> No i mean
<azonenberg_work> no constraints that say "do this after X cycles" in the SMTC
<azonenberg_work> only initial and always constraints, plus the RTL itself
<azonenberg_work> Is there any way to figure out the minimum cycle length to ensure full state coverage/
marex-cloud has quit [*.net *.split]
talsit has quit [*.net *.split]
digshadow-s has quit [*.net *.split]
martling has quit [*.net *.split]
martling has joined ##openfpga
digshadow-s has joined ##openfpga
<clifford> bc of induction step
talsit has joined ##openfpga
<azonenberg_work> clifford: basically my understanding is, if you create an inductive proof that works with (as in my above example) a 12-cycle depth
<clifford> you dont really need to know which bmc length covers the reachable state space, if that's what you mean
marex-cloud has joined ##openfpga
<azonenberg_work> that means you're saying, as long as you have 12 valid states in a row
<azonenberg_work> everything after that is valid
<azonenberg_work> Then if you do a 12-cycle BMC you can show that after reset you will get 12 valid states
<azonenberg_work> therefore the state is always valid
<clifford> yes
<azonenberg_work> So the only time this is untrue is if you have SMTC constraints that refer to specific numbers of cycles?
<clifford> but the number of states you need entirely depend on the asserts you have
<azonenberg_work> Or will the induction fail if it sees time delays that havent been met yet
<clifford> if your asserts describe the reachable state space exactly, then 1-cycle is enough to prove your circuit
<azonenberg_work> Yeah well typically my asserts are attached to sequential logic
<azonenberg_work> So it's going to take several
<clifford> the default value used by yosys-smtbmc (20) is usually pretty good.
<azonenberg_work> And the only reason to increase that is if the induction is inconclusive after 20 steps?
<azonenberg_work> i havent actually found anything it couldn't prove or find a counterexample for in 20 cycles so far
<clifford> in a 20 cycles counterexample for the induction you usually see enough to formulate a new assert that tells the solver the entire thing is unreachable
<azonenberg_work> Yeah
<azonenberg_work> Or you find a bug :p
<azonenberg_work> my current test case is a new NoC transceiver for antikernel
m_t has joined ##openfpga
<azonenberg_work> The old setup was fixed 32-bit data width and fairly bulky as far as internal state and flow control
<azonenberg_work> the new one is scalable 16 to 128 bit width and in some cases degenerates to like three FFs and a lut or two
<azonenberg_work> But i have to prove correct behavior across all widths hence all the fluff
<azonenberg_work> It's not finished yet, there's still properties i am not checking
<azonenberg_work> And i want to try to use generates or something to reduce some of the boilerplate
<azonenberg_work> But it already caught a couple of bugs where i pulled fields out of the wrong indexes on the packed data
digshadow has joined ##openfpga
<digshadow> azonenberg: btw SEM is moving in a few days
<digshadow> this ultimately may put it by my workshop where its more accessible
<digshadow> maybe in that abandoned warehouse building next to it
<azonenberg_work> digshadow: oh?
<azonenberg_work> Why so
<azonenberg_work> they kicking you out of the garage?
<digshadow> more or less
<azonenberg_work> or you just wanted it closer to the rest of the lab
<digshadow> all of the above?
<digshadow> its going into a POD moving thing
<digshadow> which I'll likely have moved to my workshop after the SEM is removed from the car barn
<azonenberg_work> ah i see
<Marex> jrernst: I dont think you need my logic lock hack
<Marex> the missing ECO support is surprising tho
<jrernst> hello again.
<jrernst> never the less it works 50%.
<jrernst> set_location_assignment worked, and worked before because I used it for fixing the parts to a particular position.
<jrernst> I will learn from your scripts (especially the tcl parts)
<Marex> :)
<Marex> hth
<Marex> ah btw I think if you do a full rebuild, the ECO stuff will be gone
<Marex> you need to do that ECO thing, not a full rebuild ... iirc
<jrernst> maybe you and I meaning different things. what do you mean by that ECO thing?
<Marex> jrernst: isn't there something where it applies ECO and spits out updated SOF ?
<Marex> I believe that's what my script did and you should be able to use the same on CIII
<Marex> I don't quite understand why you wouldn't be able to use ECO on CIII
* Marex is tired
<jrernst> yet i didn't find it. yet all changes (e.g. in the chip planner) had been rejected.
<Marex> jrernst: isn't there like "apply ECO" in the chip planner ?
<Marex> jrernst: there's such a small dialog somewhere, which allows you to add the ECO and then say "apply", which does all the magic
<Marex> and if you open TCL console, you'll see pretty much what's in my script
<Marex> errr, sorry, forget that last sentence
<Marex> and if you export the ECO as TCL, you'll see pretty much what's in my script ... is what I wanted to say
<jrernst> what I did before:
<jrernst> a) I opened chip planner
<jrernst> b) right clicked on a LE --> Locate --> Locate in Ressource Property Editor
<Marex> sec
<jrernst> c) there I can for example delete the DATAIN connection to the FF
<jrernst> d) go back to the chip planner first window
<jrernst> e) down in the change manager list is one entry (the change I made)
<Marex> I don't think I ever tried deleting any interconnect, that might not work
<jrernst> f) right click -> Check and Save All Netlist Changes
<Marex> that looks familiar
<jrernst> doesn't matter what change
<jrernst> tried just do find one change I can do easely
<Marex> ah, but I recall you can switch fanin from A to C and B to D
<Marex> you cannot switch from A to B or C to D because of the way the fanins are wired
<jrernst> wait on the bottom of the chang list theres a button (I forgot)
<jrernst> Buttons says "Checks the legality of ECO changes and saves them if all are legal"
<Marex> jrernst: check and save is imo what you want ...
<Marex> jrernst: jupp, if I ie change "Sum LUT Mask" and hit "check and save" , I get updated SOF file
<jrernst> there's the first problem. I don't see anything called "Sum LUT Mask"
<Marex> jrernst: in Resource Property Editor, on right side, select "Combinatorial" tab
<jrernst> yes, found it. But I cannot enter the field. Only mark it blue.
<Marex> jrernst: double-click the value ?
<jrernst> nope
<Marex> uh
<jrernst> it's not in the web edition
<Marex> jrernst: I started the web edition just now :)
<Marex> jrernst: I tested it just now ...
<Marex> jrernst: maybe it's C/IV and newer ... hmmm
<jrernst> you have version 15, mine is version 13 ... maybe
<Marex> well I have 16.1 now ...
<jrernst> at the mment I'm in your base_project with EP4CE6
<Marex> hummmmmmm
<jrernst> at the moment I'm in your base_project with EP4CE6
<jrernst> okay, I'll try a newer version. That's the task for tomorrow.
<jrernst> tonight I'll try another method
<Marex> jrernst: you can let it download overnight ;-/ The altera servers are slow as heck ...
<Marex> jrernst: hehehe :)
<jrernst> okay, good suggestion :-)
<Marex> jrernst: the ECO is reliable in that it allows you to precisely modify only single thing
<jrernst> In your tcl script you used set node_properties ....
<Marex> I had trouble when I rebuilt the whole project in that quartus added a lot of random bits all over the place
<Marex> the ECO was a blessing
<jrernst> Is there the opposite "get node_properties"?
<Marex> probably :)
<jrernst> okay, let me show you my thought:
<jrernst> when I make a verilog I can use a name with a code in it
<jrernst> maybe something like foo_nr455 and for every node I change the number
<jrernst> Then I can maybe get some properties from tcl and with the name I can correlate to my changes in the verilog
<jrernst> With this in mind I can skip all positioning code
<jrernst> Because I didn't mind anymore where the LE or LAB goes.
<jrernst> Okay later I can fine tune but ...
<jrernst> I will use big verilog (or vhdl) with many LEs in it and for example 50% I set change A and 50% I set change B
<jrernst> With this it must be possible by correlating A and B where the bit is
<Marex> what do you hope to achieve with this ? :)
<jrernst> It depends on the information I get from tcl by reading the node properties.
<jrernst> I hope to get a more automated method
<jrernst> Skipping most of the manual work
<Marex> yep
<jrernst> Having a method which works for nearly every bitstream
<Marex> if you can figure out how to dig out more than what quartusc_cdb tells us, that'd be awesome
<jrernst> It's like a side channel attack
<jrernst> do you know how that is made?
<Marex> how what is made ?
<jrernst> Many events where produced and then statistically correlated.
<jrernst> I saw such an side channel attack 2 years ago.
<jrernst> In an xilinx there was an AES running.
<Marex> well I know what side-channel is :)
<jrernst> Then by feeding thousends of keys one can find out at which time a bit of the key is generated.
<jrernst> The magic is in the high numbers. One can get information from below the noise floor.
<jrernst> I think in a same method suing the thousands of LEs
<jrernst> I think in a same method using the thousands of LEs
<Marex> and ... what information do you obtain from that ? :)
<jrernst> any info that I want
<Marex> which is ... ?
<jrernst> for example
<Marex> !!
<Marex> example, great :)
<jrernst> wait i'm thinking
<jrernst> okay
<jrernst> when i'm spamming mostly all LEs
<jrernst> and every LE is connected with only one pin
<jrernst> then there is only on path in the RCF file
<Marex> then you also run out of pins :)
<jrernst> okay, i have to limit it to the max pin count
<Marex> and thanks to the randomization in PnR, there are multiple possible paths :(
<jrernst> no problem.
<jrernst> i can keep track of all variations
<jrernst> in the end I get a map of all reachable routes from one LE
<Marex> oh, interesting
<Marex> although that might be a lot of bits
<jrernst> maybe
<Marex> by reachable, you mean on single hop or multiple hops ?
<Marex> if the later, that's pretty much the whole FPGA ...
<jrernst> depends on what info you want to get
<jrernst> maybe you look for LE_BUFFER in the RCF file then you get the position of the LE_BUFFERs
<jrernst> when you look for C$ then you'll get the C$ positions, right?
<jrernst> when you look for C$ then you'll get the C4 positions, right?
<jrernst> when you look for C4 then you'll get the C4 positions, right?
<jrernst> finally C4... damn
<Marex> jrernst: but wouldn't you have a lot of noise there , so wouldn't it be hard to figure out the meaning of the bits ?
<Marex> jrernst: I think I kinda get your idea though
<jrernst> yes, noise will be there but therefore we have to correlate. It's the method used from the french guy
<jrernst> Another idea is to reduce the noise to almost zero.
<jrernst> I mentioned it before. I'm using "probes". Think of the LE as a "probe" or a transmitter.
<jrernst> no FF and no CLK and no Comb-inputs. Then there is no noise by that routing.
<jrernst> Only foo <= not foo is generated from the Comb. And this foo is routed to a pin.
<jrernst> This reduces the noise to almost zero.
<Marex> ha
<jrernst> I did this today with two runs
<jrernst> first I set an LE and routed it to pin 53
<jrernst> second I set the same LE and routed it to pin 55
<jrernst> then I used both sof and generated an ASCII representation
<jrernst> from then I XORed the bits to get the changes.
<jrernst> Same thing will go zero for example the LUT mask and all the default bits which are set over the whole bitstream
<jrernst> Then I made the XOR output AND with the pin53 output and then with the pin55 output
<jrernst> and I saw only the routing bits
<Marex> ah, right
<jrernst> the route for the pin53 example and then the pin55 example
<jrernst> no clutter when i interprete this right
<jrernst> if you want i can send you files and you can see for yourself.
<Marex> yes please :)
<jrernst> hmm... over IRC as ZIP?
<Marex> over email as a tarball
<jrernst> okay
<jrernst> here it comes
<jrernst> first look at main.vhd it's the "toggler" sending pulses
digshadow has quit [Quit: Leaving.]
digshadow has joined ##openfpga
<jrernst> then look at pin53.qsf for fixating the LCCOMB the IOOBUF and the pin
<jrernst> the generated sof files were transformed with my scripts (not included) to sof.asc files. You can open them in an text editor.
<jrernst> 053-055.txt is the XOR result. In text editor go down to the last line and scroll to the middle.
<jrernst> 053.txt is the ANDed result showing only the 053 routing
<jrernst> and vice versa 055.txt showing the 055 routing
<jrernst> ah and in the RCF you get the involved elements
<Marex> jrernst: I was mostly interested in those scripts :)
<jrernst> I can send it too... wait
<jrernst> okay ... sending ...
<jrernst> first is scan-sof.pl it gives a human readable info of the SOF file
<Marex> jrernst: you're in DE I presume ? Insomnia much ?
* Marex is ready to just drop ...
<jrernst> Usage: perl scan-sof.pl <sof-file>
<jrernst> okay, then till next time...
<Marex> jrernst: please continue :)
<jrernst> okay
<Marex> looking through scan-sof, that looks familiar :)
<jrernst> next is conv-sof2asc.pl
<jrernst> or if you want conv-sof2pbm.pl if you want a bitmap file
<Marex> still looks kinda familiar :)
<jrernst> Usage: perl conv-sof2asc.pl <sof-file>
<jrernst> At the moment there are 4 types of devices supported. It's in the file chipdata.pm
<Marex> jupp
<Marex> so it seems they all use the same tile type with the same geometry, great
<jrernst> yep :-)
<jrernst> to investigate the huge asc files I use info-asc.pl
<jrernst> to cut out one particular LAB use the following commands:
<jrernst> perl info-asc.pl chip EP4CE6 cut <asc-file> <xpos> <ypos> <width> <height>
<jrernst> more easy this notation:
<Marex> jrernst: do you handle the obscure M4K and DSP tiles too ?
<jrernst> perl info-asc.pl chip EP4CE6 cut <asc-file> X7 Y3
<Marex> jrernst: their width is different than standard logic tiles
<jrernst> in the file EP4CE6.txt are the starting positions so I can skip over them
<Marex> jrernst: ah, how did you determine those ?
<jrernst> okay, not really the positions, the widths and the script calculates the x-positions. I had it fixed before but it's bad if I had to move the positions.
<jrernst> Ah, okay I looked at the ASC and looked for repeating patterns
<jrernst> The LAB layout is the same
<Marex> superb :)
<jrernst> The M9K layout is the same. Fortunately I began with the EP4CE22 with twi M9K and 2 DSP so I had references
<jrernst> The M9K layout is the same. Fortunately I began with the EP4CE22 with 2 M9K and 2 DSP so I had references
<Marex> oh :)
<jrernst> with the info-asc.pl you can output the different LABs and you see always the same output when you use an "empty" sof.
<jrernst> when you output the M9K tiles you see too the same output
<jrernst> Same with DSP but the bits are zero
<jrernst> Then I did some calculations fitting it in so that left IO and right IO have the same width.
<jrernst> same with top and bottom IO
<jrernst> And as you mentioned the annoying 4 column tile in the middle.
<Marex> jrernst: jupp, I did similar thing
<Marex> jrernst: IMO that might be clock routing
<jrernst> With the EP4CE22 there are TWO 4 bit column tiles
<Marex> oh
<jrernst> I was lucky so EP4CE6 was the easier
<jrernst> ah I forgot: EP3C16 has two 4 bit columns as well, look at the EP3C16.txt
<jrernst> any questions left before closing the session for tonight?
<jrernst> ANDing, ORing and XORing the ASC files is donw with info-asc.pl too
<jrernst> Usage: perl info-asc.pl chip EP4CE6 and <asc-file1> <asc-file2> ...
<jrernst> Usage: perl info-asc.pl chip EP4CE6 or <asc-file1> <asc-file2> ...
<jrernst> Usage: perl info-asc.pl chip EP4CE6 xor <asc-file1> <asc-file2> ...
<jrernst> And last info-rcl.pl does some regexp with RCF files. Same as you have done with sed in the tcl.
<jrernst> so?
<Marex> jrernst: I'm ready to wrap this for tonight :)
<jrernst> Marex: okay... bye
<Marex> jrernst: gnight !
jrernst has quit [Quit: Leaving]
Ardeshir has quit [Remote host closed the connection]