diff --git a/docs/examples/amba/apb.fl b/docs/examples/amba/apb.fl new file mode 100644 index 0000000..e69de29 diff --git a/docs/examples/amba/apb2sram.fl b/docs/examples/amba/apb2sram.fl new file mode 100644 index 0000000..7d14451 --- /dev/null +++ b/docs/examples/amba/apb2sram.fl @@ -0,0 +1,170 @@ +module apb2sram (apb: APB, sram: ! SRAMBus) { + fsm { + + fork { + apb.read(addr, data); + sram.read(addr, data); + } + + fork { + apb.write(addr, data); + sram.write(addr, data); + } + } +} + +struct APB { + addr : int32; + rdata : ! int32; + wdata : int32; + en : int1; + strb : int4; + ready : ! int1; + write : int1; + sel : int1; +} + +struct SRAM { + addr : int32; + rdata : ! int32; + wdata : int32; + wen : int; +} + +trans read (addr : int32, data : int32) on APB { + self.sel = 1; + self.en = 0; + self.write = 0; + self.addr = addr; + addr = self.addr; + clk; + self.en = 1; + self.ready = 1; + self.rdata = data; + while !self.ready { clk; } + data = self.rdata; + clk; +} + +trans write (addr : int32, data : int32) on APB { + self.sel = 1; + self.en = 0; + self.write = 1; + self.wdata = data; + self.addr = addr; + self.strb = 15; + addr = self.addr; + data = self.wdata; + clk; + self.en = 1; + self.ready = 1; + while !self.ready { clk; } + clk; +} + +# "Formal" description +trans read (addr: int32, data: int32) on APB { + nop { clk; } + property self.sel == 1; + property self.en == 0; + property self.write == 0; + property self.addr == addr; + clk; + property self.en == 1; + nop { clk; } + property self.ready == 1; + property self.rdata == data; + clk; + release; +} + +trans write (addr: int32, data: int32) on APB { + nop { clk; } + property self.sel == 1; + property self.en == 0; + property self.write == 1; + property self.addr == addr; + property self.wdata == data; + clk; + property self.en == 1; + nop { clk; } + property self.ready == 1; + clk; + release; +} + +trans read (addr : int32, data : int32) on SRAM { + self.addr = addr; + addr = self.addr; + self.we = 0; + clk; + self.data = rdata; + data = self.rdata; +} + +trans write (addr : int32, data : int32) on SRAM { + self.addr = addr; + addr = self.addr; + self.we = 1; + self.wdata = data; + data = self.wdata; + clk; +} + +struct Reg { + value: T, +} + +tran set (value: const T) on Reg { + let tmp = value; + clk; + self.value = tmp; +} + +tran get (value: T) on Reg { + value = self.value; +} + +module MyMagicSRAM (bus: in SRAM) { + let words: [Reg; 1024]; + + fsm { + INITIAL: { + let addr; + let data; + with bus.read(addr, data) { + let tmp = addr; + clk; + data = words[tmp]; + } + with bus.write(addr, data) { + let tmpA = addr; + let tmpD = data; + clk; + words[tmpA] = tmpD; + } + with epsilon { clk; } + } + } +} + +# READ +Req (Master): + +self.addr = addr; +self.we = 0; +clk; +data = self.rdata; + +1. Assignments to outputs +2. Reads from inputs + +Resp (Slave): + +addr = self.addr; +self.we = 0; +clk; +data = self.rdata; + +1. Assignment to inputs +2. diff --git a/docs/examples/amba/apb_a.txt b/docs/examples/amba/apb_a.txt new file mode 100644 index 0000000..c5eafdd --- /dev/null +++ b/docs/examples/amba/apb_a.txt @@ -0,0 +1,40 @@ +module MyMagicSRAM ( + input logic clk, + input logic rst_n, + input logic [31:0] bus_addr, + output logic [31:0] bus_rdata, + input logic [31:0] bus_wdata, + input logic bus_wen +); + + + +endmodule + + +/* +INITIAL: + -- bus.read --> INITIAL (A) + -- bus.write --> INITIAL (B) + +INITIAL: + self.addr = addr; (A) + addr = self.addr; (A) + self.we = 0; (A) + -> A2; (A) +A2: + self.data = rdata; (A) + data = self.rdata; (A) + -> INITIAL; (A) + +INITIAL: + self.addr = addr; (B) + addr = self.addr; (B) + self.we = 1; (B) + self.wdata = data; (B) + data = self.wdata; (B) + -> B2; (B) +B2: + -> INITIAL; (B) + +*/ diff --git a/docs/examples/amba/apb_b.txt b/docs/examples/amba/apb_b.txt new file mode 100644 index 0000000..1403470 --- /dev/null +++ b/docs/examples/amba/apb_b.txt @@ -0,0 +1,47 @@ +module MyMagicSRAM ( + input logic clk, + input logic rst_n, + input logic [31:0] bus_addr, + output logic [31:0] bus_rdata, + input logic [31:0] bus_wdata, + input logic bus_wen +); + + + +endmodule + + +/* +INITIAL: + -- bus.read --> INITIAL (A) + -- bus.write --> INITIAL (B) + +--------------------------- + +INITIAL: + self.addr = addrA; (A) + addrA = self.addr; (A) + let tmpA = addrA; (A) + self.we = 0; (A) + --- + dataA = words[tmpA]; (A) + self.rdata = dataA; (A) + dataA = self.rdata; (A) + -> INITIAL; (A) + +--------------------------- + +INITIAL: + self.addr = addrB; (B) + addrB = self.addr; (B) + let tmpAB = addrB; (B) + self.we = 1; (B) + self.wdata = dataB; (B) + dataB = self.wdata; (B) + let tmpDB = dataB; (B) + --- + words[tmpAB] = tmpDB; (B) + -> INITIAL; (B) + +*/ diff --git a/docs/examples/amba/apb_c.txt b/docs/examples/amba/apb_c.txt new file mode 100644 index 0000000..b024bfa --- /dev/null +++ b/docs/examples/amba/apb_c.txt @@ -0,0 +1,79 @@ +read_master { + sel <= 1; + en <= 0; + write <= 0; + addr <= @ADDR; + clk; + en <= 1; + while !ready { clk; } + let @DATA = rdata; + clk; + // sel <= 0; + // en <= 0; + // addr <= X; +} + +write_master { + sel <= 1; + en <= 0; + write <= 1; + addr <= @ADDR; + wdata <= @DATA; + clk; + en <= 1; + while !ready { clk; } + clk; + // sel <= 0; + // en <= 0; + // addr <= X; +} + +read_slave { + while sel != 1 && en != 0 && write != 0 { clk; } + let @ADDR = addr; + clk; + assert(en == 1); + ready <= 1; + rdata <= @DATA; + clk; + // ready <= 0; + // rdata <= X; +} + +write_slave { + while sel != 1 && en != 0 && write != 1 { clk; } + let @ADDR = addr; + let @DATA = wdata; + clk; + assert(en == 1); + ready <= 1; + clk; + // ready <= 0; +} + +rw_slave { + while sel != 1 && en != 0 { clk; } + let @ADDR = addr; + if write == 0 {} + if write == 1 { + let @DATA = wdata; + } + clk; + assert(en == 1); + ready <= 1; + if write == 0 { + rdata <= @DATA; + } + if write == 1 {} + clk; + // ready <= 0; + // rdata <= X; +} + +read_monitor { + while sel != 1 && en != 0 && write != 0 { clk; } + clk; + assert(en == 1); + while !ready { clk; } + clk; +} diff --git a/docs/examples/axi/axi.fl b/docs/examples/amba/axi.fl similarity index 100% rename from docs/examples/axi/axi.fl rename to docs/examples/amba/axi.fl